diff --git a/liquidjava-example/src/main/java/testSuite/CorrectPrimitiveNumbersTypes.java b/liquidjava-example/src/main/java/testSuite/ErrorPrimitiveNumbersTypes.java similarity index 78% rename from liquidjava-example/src/main/java/testSuite/CorrectPrimitiveNumbersTypes.java rename to liquidjava-example/src/main/java/testSuite/ErrorPrimitiveNumbersTypes.java index 87685b089..d7a4add51 100644 --- a/liquidjava-example/src/main/java/testSuite/CorrectPrimitiveNumbersTypes.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorPrimitiveNumbersTypes.java @@ -3,25 +3,25 @@ import liquidjava.specification.Refinement; @SuppressWarnings("unused") -public class CorrectPrimitiveNumbersTypes { +public class ErrorPrimitiveNumbersTypes { @Refinement("_ < i && _ > 0") private static double fromType(@Refinement("_ > 0") int i) { - return i * 0.1; + return i * 0.1; // Expect: SMT Unknown Error } @Refinement(" _ < i && _ > 0") private static double fromType(@Refinement("_ > 0") long i) { - return i * 0.1; + return i * 0.1; // Expect: SMT Unknown Error } @Refinement(" _ < i && _ > 0") private static double fromType(@Refinement("_ > 0") short i) { - return i * 0.1; + return i * 0.1; // Expect: SMT Unknown Error } @Refinement("_ > i") private static float twice(@Refinement("i > 0") short i) { - return i * 2f; + return i * 2f; // Expect: SMT Unknown Error } public static void main(String[] args) { diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSMTUnknown.java b/liquidjava-example/src/main/java/testSuite/ErrorSMTUnknown.java new file mode 100644 index 000000000..4067ca8b7 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorSMTUnknown.java @@ -0,0 +1,10 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorSMTUnknown { + @Refinement("_ > 2.0") + public static int aboveTwo(int value) { + return value; // Expect: SMT Unknown Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSMTUnknownState.java b/liquidjava-example/src/main/java/testSuite/ErrorSMTUnknownState.java new file mode 100644 index 000000000..e3454caca --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorSMTUnknownState.java @@ -0,0 +1,19 @@ +package testSuite; + +import liquidjava.specification.Ghost; +import liquidjava.specification.StateRefinement; + +@Ghost("int amount") +public class ErrorSMTUnknownState { + @StateRefinement(to = "amount(this) > 0") + public ErrorSMTUnknownState() {} + + @StateRefinement(from = "amount(this) < limit") + public void consume(int limit) {} + + public static void test(double limit) { + ErrorSMTUnknownState value = new ErrorSMTUnknownState(); + int boundary = (int) limit; + value.consume(boundary); // Expect: SMT Unknown Error + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java index 167a4560e..2580e2a8a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java @@ -21,7 +21,7 @@ * */ public final class DebugLog { @@ -400,16 +400,9 @@ private static String formatCounterexample(Object counterexample) { return sb.toString(); } - public static void smtUnknown() { - if (!enabled()) { - return; - } - System.out.println(SMT_TAG + " Result: " + Colors.YELLOW + "UNKNOWN (treated as OK)" + Colors.RESET); - } - /** * Print the result of an SMT check whose {@code smtStart} was emitted by the caller (e.g. VCChecker's structured - * print). {@link liquidjava.smt.SMTResult} doesn't preserve UNKNOWN, so this maps OK → UNSAT and ERROR → SAT. + * print). This maps OK → UNSAT and ERROR → SAT; UNKNOWN raises an error instead of returning a result. */ public static void smtResult(liquidjava.smt.SMTResult result) { if (!enabled()) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SMTUnknownError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SMTUnknownError.java new file mode 100644 index 000000000..5dd68be0e --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SMTUnknownError.java @@ -0,0 +1,28 @@ +package liquidjava.diagnostics.errors; + +import spoon.reflect.cu.SourcePosition; + +/** + * Error indicating that the SMT solver could not decide a verification condition + */ +public class SMTUnknownError extends LJError { + private SourcePosition declarationPosition; + + public SMTUnknownError(String reason) { + super("SMT Unknown Error", "Could not prove refinement", null, null); + String tacticFailure = "smt tactic failed to show goal to be sat/unsat "; + if (reason.startsWith(tacticFailure)) { + reason = reason.substring(tacticFailure.length()).replace("(", "").replace(")", ""); + } + setHint("Reason: " + reason); + } + + public void setDeclarationPosition(SourcePosition declarationPosition) { + this.declarationPosition = declarationPosition; + } + + @Override + public SourcePosition getDeclarationPosition() { + return declarationPosition; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java index 8e0a9295d..011bd95bd 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java @@ -70,6 +70,10 @@ public void processSubtyping(Predicate expectedType, List list, CtEl SMTResult result; try { result = dischargeToSMT(expected, premises, annotationValuePos, true); + } catch (SMTUnknownError error) { + error.setDeclarationPosition(declarationPosition); + DebugLog.smtError(error.getMessage()); + throw error; } catch (RuntimeException ex) { DebugLog.smtError(ex.getMessage()); throw ex; @@ -94,7 +98,13 @@ public void processSubtyping(Predicate expectedType, List list, CtEl */ public void processSubtyping(Predicate type, Predicate expectedType, List list, CtElement element, SourcePosition declarationPosition, Factory f) throws LJError { - SMTResult result = verifySMTSubtypeStates(type, expectedType, list, element.getPosition(), f); + SMTResult result; + try { + result = verifySMTSubtypeStates(type, expectedType, list, element.getPosition(), f); + } catch (SMTUnknownError error) { + error.setDeclarationPosition(declarationPosition); + throw error; + } if (result.isError()) throwRefinementError(element.getPosition(), declarationPosition, expectedType, type, result.getCounterexample(), null); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 03d14b807..e38cdb0d2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -7,6 +7,7 @@ import liquidjava.diagnostics.errors.IllegalConstructorTransitionError; import liquidjava.diagnostics.errors.InvalidRefinementError; import liquidjava.diagnostics.errors.LJError; +import liquidjava.diagnostics.errors.SMTUnknownError; import liquidjava.processor.context.*; import liquidjava.processor.refinement_checker.TypeChecker; import liquidjava.processor.refinement_checker.TypeCheckingUtils; @@ -433,7 +434,14 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) throws L Predicate expectState = stateChange.getFrom().substituteVariable(Keys.THIS, instanceName) .changeOldMentions(vi.getName(), instanceName); - if (!tc.checkStateSMT(prevState, expectState, fw.getPosition())) { // Invalid field transition + boolean validTransition; + try { + validTransition = tc.checkStateSMT(prevState, expectState, fw.getPosition()); + } catch (SMTUnknownError error) { + error.setDeclarationPosition(field.getDeclaringType().getPosition()); + throw error; + } + if (!validTransition) { // Invalid field transition tc.throwStateRefinementError(fw.getPosition(), field.getDeclaringType().getPosition(), prevState, expectState, stateChange.getMessage()); return; @@ -499,7 +507,12 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc } expectState = expectState.changeOldMentions(vi.getName(), instanceName); - found = tc.checkStateSMT(prevCheck, expectState, invocation.getPosition()); + try { + found = tc.checkStateSMT(prevCheck, expectState, invocation.getPosition()); + } catch (SMTUnknownError error) { + error.setDeclarationPosition(stateChange.getFromPosition()); + throw error; + } if (found && stateChange.hasTo()) { String newInstanceName = String.format(Formats.INSTANCE, name, tc.getContext().getCounter()); // Non-void: `_` is the return value; void: legacy alias for the new instance. diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java index c44c95793..f0658215b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java @@ -8,6 +8,7 @@ import com.microsoft.z3.Z3Exception; import liquidjava.diagnostics.DebugLog; +import liquidjava.diagnostics.errors.SMTUnknownError; import liquidjava.processor.context.Context; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.Expression; @@ -51,12 +52,15 @@ public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context conte } return SMTResult.error(counterexample); } - if (!silent) { - if (result.equals(Status.UNKNOWN)) { - DebugLog.smtUnknown(); - } else { - DebugLog.smtUnsat(); + if (result.equals(Status.UNKNOWN)) { + SMTUnknownError error = new SMTUnknownError(solver.getReasonUnknown()); + if (!silent) { + DebugLog.smtError(error.getMessage()); } + throw error; + } + if (!silent) { + DebugLog.smtUnsat(); } } } catch (SyntaxException e) {