Unsatisfiable Refinement Warning (#202)

Author: rcosta358

liquidjava-example/src/main/java/testSuite/ErrorWarningUnsatRefinement.java

@@ -0,0 +1,28 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorWarningUnsatRefinement {
+
+    public void example1() {
+        @Refinement("x == 1 && x != 1") // Unsat Refinement Warning
+        int x = 1; // Refinement Error
+    }
+
+    public void example2() {
+        @Refinement("x % 2 > 1") // Unsat Refinement Warning
+        int x = 5; // Refinement Error
+    }
+
+    public void example3() {
+        @Refinement("false") // Unsat Refinement Warning
+        int x = 0; // Refinement Error
+    }
+
+    public void example4(@Refinement("x > 0 && x < 0") int x) {} // Unsat Refinement Warning
+
+    @Refinement("_ == true && _ == false") // Unsat Refinement Warning
+    public boolean example5() {
+        return true; // Refinement Error
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/UnsatisfiableRefinementWarning.java

@@ -0,0 +1,22 @@
+package liquidjava.diagnostics.warnings;
+
+import spoon.reflect.cu.SourcePosition;
+
+/**
+ * Warning indicating that a refinement predicate is unsatisfiable
+ * 
+ * @see LJWarning
+ */
+public class UnsatisfiableRefinementWarning extends LJWarning {
+
+    private final String refinement;
+
+    public UnsatisfiableRefinementWarning(SourcePosition position, String refinement) {
+        super("This refinement can never be true", position);
+        this.refinement = refinement;
+    }
+
+    public String getRefinement() {
+        return refinement;
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java

@@ -6,7 +6,9 @@
 import java.util.Map;
 import java.util.Optional;
 
+import liquidjava.diagnostics.Diagnostics;
 import liquidjava.diagnostics.errors.*;
+import liquidjava.diagnostics.warnings.UnsatisfiableRefinementWarning;
 import liquidjava.processor.context.AliasWrapper;
 import liquidjava.processor.context.Context;
 import liquidjava.processor.context.GhostFunction;
@@ -16,6 +18,7 @@
 import liquidjava.processor.facade.GhostDTO;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.parsing.RefinementsParser;
+import liquidjava.smt.SMTEvaluator;
 import liquidjava.smt.SMTResult;
 import liquidjava.utils.Utils;
 import liquidjava.utils.constants.Formats;
@@ -29,6 +32,9 @@
 import spoon.reflect.declaration.CtClass;
 import spoon.reflect.declaration.CtElement;
 import spoon.reflect.declaration.CtInterface;
+import spoon.reflect.declaration.CtMethod;
+import spoon.reflect.declaration.CtTypedElement;
+import spoon.reflect.declaration.CtVariable;
 import spoon.reflect.declaration.CtType;
 import spoon.reflect.factory.Factory;
 import spoon.reflect.reference.CtTypeReference;
@@ -41,6 +47,7 @@ public abstract class TypeChecker extends CtScanner {
     protected final Context context;
     protected final Factory factory;
     protected final VCChecker vcChecker;
+    private final Diagnostics diagnostics = Diagnostics.getInstance();
 
     public TypeChecker(Context context, Factory factory) {
         this.context = context;
@@ -88,11 +95,53 @@ public Optional<Predicate> getRefinementFromAnnotation(CtElement element) throws
                 throw new InvalidRefinementError(position, "Refinement predicate must be a boolean expression",
                         ref.get());
             }
+            if (!Boolean.TRUE.equals(element.getMetadata(Keys.REFINEMENT_SAT_CHECK)))
+                checkRefinementSatisfiability(ref.get(), p, element);
             constr = Optional.of(p);
         }
         return constr;
     }
 
+    /**
+     * Performs a best-effort satisfiability check for a refinement reporting a warning if unsat. Runs an SMT check on a
+     * temporary scope and if the refinement mentions other names that are still unavailable at this point, the SMT
+     * check fails and that failure is ignored.
+     */
+    private void checkRefinementSatisfiability(String refinement, Predicate predicate, CtElement element) {
+        context.enterContext();
+        try {
+            Predicate p = new Predicate();
+            CtTypeReference<?> annotationType = element instanceof CtTypedElement<?> typedElement
+                    ? typedElement.getType() : null;
+            if (annotationType != null && !context.hasVariable(Keys.WILDCARD))
+                context.addVarToContext(Keys.WILDCARD, annotationType, p, element);
+
+            if (element instanceof CtVariable<?> variable && !context.hasVariable(variable.getSimpleName()))
+                context.addVarToContext(variable.getSimpleName(), variable.getType(), p, element);
+
+            if (element instanceof CtMethod<?> method && method.getType() != null && !context.hasVariable("return"))
+                context.addVarToContext("return", method.getType(), p, element);
+
+            String qualifiedClassName = getQualifiedClassName(element);
+            if (qualifiedClassName != null && !context.hasVariable(Keys.THIS))
+                context.addVarToContext(Keys.THIS, factory.Type().createReference(qualifiedClassName), p, element);
+
+            Predicate refinementPredicate = predicate.changeStatesToRefinements(context.getGhostStates(),
+                    new String[] { Keys.WILDCARD, Keys.THIS });
+            refinementPredicate = refinementPredicate.changeAliasToRefinement(context, factory);
+
+            if (new SMTEvaluator().isUnsatisfiable(refinementPredicate, context)) {
+                SourcePosition position = Utils.getLJAnnotationPosition(element, refinement);
+                diagnostics.add(new UnsatisfiableRefinementWarning(position, refinement));
+            }
+            element.putMetadata(Keys.REFINEMENT_SAT_CHECK, true); // for caching the satisfiability check result
+        } catch (Exception e) {
+            // ignore
+        } finally {
+            context.exitContext();
+        }
+    }
+
     @SuppressWarnings({ "rawtypes" })
     public Optional<String> getMessageFromAnnotation(CtElement element) {
         for (CtAnnotation<? extends Annotation> ann : element.getAnnotations()) {

liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java

@@ -48,4 +48,18 @@ public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context conte
         }
         return SMTResult.ok();
     }
+
+    public boolean isUnsatisfiable(Predicate predicate, Context context) throws Exception {
+        try {
+            Expression exp = predicate.getExpression();
+            try (TranslatorToZ3 tz3 = new TranslatorToZ3(context)) {
+                ExpressionToZ3Visitor visitor = new ExpressionToZ3Visitor(tz3);
+                Expr<?> e = exp.accept(visitor);
+                Solver solver = tz3.makeSolverForExpression(e);
+                return solver.check().equals(Status.UNSATISFIABLE);
+            }
+        } catch (Z3Exception e) {
+            throw new Z3Exception(e.getLocalizedMessage());
+        }
+    }
 }

liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java

@@ -2,6 +2,7 @@
 
 public final class Keys {
     public static final String REFINEMENT = "refinement";
+    public static final String REFINEMENT_SAT_CHECK = "refinement_sat_check";
     public static final String TARGET = "target";
     public static final String THIS = "this";
     public static final String WILDCARD = "_";

liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java

@@ -34,7 +34,7 @@ public class TestUtils {
      * @param path
      */
     public static boolean shouldPass(String path) {
-        return path.toLowerCase().contains("correct") || path.toLowerCase().contains("warning");
+        return path.toLowerCase().contains("correct");
     }
 
     /**