Improve Counterexamples

liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java

@@ -129,7 +129,7 @@ public String getSnippet() {
 
                         // line number padding + pipe + column offset
                         String indent = " ".repeat(padding) + Colors.GREY + PIPE + Colors.RESET
-                            + " ".repeat(visualColStart - 1);
+                                + " ".repeat(visualColStart - 1);
                         String markers = accentColor + "^".repeat(Math.max(1, visualColEnd - visualColStart + 1));
                         sb.append(indent).append(markers);
 

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java

@@ -1,5 +1,9 @@
 package liquidjava.diagnostics.errors;
 
+import java.util.Arrays;
+import java.util.List;
+import java.util.stream.Collectors;
+
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
 import liquidjava.smt.Counterexample;
@@ -27,20 +31,33 @@ public RefinementError(SourcePosition position, ValDerivationNode expected, ValD
 
     @Override
     public String getDetails() {
-        return "Counterexample: " + getCounterExampleString();
+        String counterexampleString = getCounterExampleString();
+        if (counterexampleString == null)
+            return "";
+        return "Counterexample: " + counterexampleString;
     }
 
     public String getCounterExampleString() {
         if (counterexample == null || counterexample.assignments().isEmpty())
-            return "";
+            return null;
 
-        // filter fresh variables and join assignements with &&
-        String counterexampleExp = counterexample.assignments().stream().filter(a -> !a.startsWith("#fresh_"))
-                .reduce((a, b) -> a + " && " + b).orElse("");
+        // filter out assignments of variables that do not appear in the found value
+        String foundValue = found.getValue().toString();
+        List<String> foundTokens = Arrays.asList(foundValue.split("[^a-zA-Z0-9_#]+"));
+        List<String> relevantAssignments = counterexample.assignments().stream().filter(a -> {
+            String varName = a.contains(" == ") ? a.substring(0, a.indexOf(" == ")).trim() : a;
+            return foundTokens.contains(varName);
+        }).collect(Collectors.toList());
+
+        if (relevantAssignments.isEmpty())
+            return null;
+
+        // join assignements with &&
+        String counterexampleExp = String.join(" && ", relevantAssignments);
 
         // check if counterexample is trivial (same as the found value)
-        if (counterexampleExp.equals(found.getValue().toString()))
-            return "";
+        if (counterexampleExp.equals(foundValue))
+            return null;
 
         return counterexampleExp;
     }

liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java

@@ -55,15 +55,15 @@ public void reinitializeAllContext() {
     public void enterContext() {
         ctxVars.push(new ArrayList<>());
         // make each variable enter context
-        for (RefinedVariable vi : getAllVariables())
+        for (RefinedVariable vi : getAllCtxVars())
             if (vi instanceof Variable)
                 ((Variable) vi).enterContext();
     }
 
     public void exitContext() {
         ctxVars.pop();
         // make each variable exit context
-        for (RefinedVariable vi : getAllVariables())
+        for (RefinedVariable vi : getAllCtxVars())
             if (vi instanceof Variable)
                 ((Variable) vi).exitContext();
     }
@@ -172,22 +172,9 @@ public boolean hasVariable(String name) {
         return getVariableByName(name) != null;
     }
 
-    /**
-     * Lists all variables inside the stack
-     *
-     * @return list of all variables
-     */
-    public List<RefinedVariable> getAllVariables() {
-        List<RefinedVariable> lvi = new ArrayList<>();
-        for (List<RefinedVariable> l : ctxVars) {
-            lvi.addAll(l);
-        }
-        return lvi;
-    }
-
     public List<RefinedVariable> getAllVariablesWithSupertypes() {
         List<RefinedVariable> lvi = new ArrayList<>();
-        for (RefinedVariable rv : getAllVariables()) {
+        for (RefinedVariable rv : getAllCtxVars()) {
             if (!rv.getSuperTypes().isEmpty())
                 lvi.add(rv);
         }
@@ -229,7 +216,7 @@ public Variable getVariableFromInstance(VariableInstance vi) {
         return vi.getParent().orElse(null);
     }
 
-    public List<RefinedVariable> getCtxVars() {
+    public List<RefinedVariable> getAllCtxVars() {
         List<RefinedVariable> lvi = new ArrayList<>();
         for (List<RefinedVariable> l : ctxVars) {
             lvi.addAll(l);
@@ -243,37 +230,37 @@ public List<RefinedVariable> getCtxInstanceVars() {
 
     // ---------------------- Variables - if information storing ----------------------
     public void variablesSetBeforeIf() {
-        for (RefinedVariable vi : getAllVariables())
+        for (RefinedVariable vi : getAllCtxVars())
             if (vi instanceof Variable)
                 ((Variable) vi).saveInstanceBeforeIf();
     }
 
     public void variablesSetThenIf() {
-        for (RefinedVariable vi : getAllVariables())
+        for (RefinedVariable vi : getAllCtxVars())
             if (vi instanceof Variable)
                 ((Variable) vi).saveInstanceThen();
     }
 
     public void variablesSetElseIf() {
-        for (RefinedVariable vi : getAllVariables())
+        for (RefinedVariable vi : getAllCtxVars())
             if (vi instanceof Variable)
                 ((Variable) vi).saveInstanceElse();
     }
 
     public void variablesNewIfCombination() {
-        for (RefinedVariable vi : getAllVariables())
+        for (RefinedVariable vi : getAllCtxVars())
             if (vi instanceof Variable)
                 ((Variable) vi).newIfCombination();
     }
 
     public void variablesFinishIfCombination() {
-        for (RefinedVariable vi : getAllVariables())
+        for (RefinedVariable vi : getAllCtxVars())
             if (vi instanceof Variable)
                 ((Variable) vi).finishIfCombination();
     }
 
     public void variablesCombineFromIf(Predicate cond) {
-        for (RefinedVariable vi : getAllVariables()) {
+        for (RefinedVariable vi : getAllCtxVars()) {
             if (vi instanceof Variable) {
                 Optional<VariableInstance> ovi = ((Variable) vi).getIfInstanceCombination(getCounter(), cond);
                 if (ovi.isPresent()) {

liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java

@@ -49,7 +49,7 @@ public void saveContext(CtElement element, Context context) {
         String file = pos.getFile().getAbsolutePath();
         String scope = getScopePosition(element);
         fileScopeVars.putIfAbsent(file, new HashMap<>());
-        fileScopeVars.get(file).put(scope, new HashSet<>(context.getCtxVars()));
+        fileScopeVars.get(file).put(scope, new HashSet<>(context.getAllCtxVars()));
 
         // add other elements in context
         instanceVars.addAll(context.getCtxInstanceVars());

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

@@ -1,5 +1,7 @@
 package liquidjava.smt;
 
+import java.util.Set;
+
 import com.martiansoftware.jsap.SyntaxException;
 import com.microsoft.z3.Expr;
 import com.microsoft.z3.Model;

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

@@ -6,7 +6,6 @@
 import com.microsoft.z3.Expr;
 import com.microsoft.z3.FPExpr;
 import com.microsoft.z3.FuncDecl;
-import com.microsoft.z3.FuncInterp;
 import com.microsoft.z3.IntExpr;
 import com.microsoft.z3.IntNum;
 import com.microsoft.z3.RealExpr;
@@ -41,12 +40,12 @@ public class TranslatorToZ3 implements AutoCloseable {
     private final Map<String, Expr<?>> funcAppTranslation = new HashMap<>();
     private final Map<Expr<?>, String> exprToNameTranslation = new HashMap<>();
 
-    public TranslatorToZ3(liquidjava.processor.context.Context c) {
-        TranslatorContextToZ3.translateVariables(z3, c.getContext(), varTranslation);
-        TranslatorContextToZ3.storeVariablesSubtypes(z3, c.getAllVariablesWithSupertypes(), varSuperTypes);
-        TranslatorContextToZ3.addAliases(c.getAliases(), aliasTranslation);
-        TranslatorContextToZ3.addGhostFunctions(z3, c.getGhosts(), funcTranslation);
-        TranslatorContextToZ3.addGhostStates(z3, c.getGhostStates(), funcTranslation);
+    public TranslatorToZ3(liquidjava.processor.context.Context context) {
+        TranslatorContextToZ3.translateVariables(z3, context.getContext(), varTranslation);
+        TranslatorContextToZ3.storeVariablesSubtypes(z3, context.getAllVariablesWithSupertypes(), varSuperTypes);
+        TranslatorContextToZ3.addAliases(context.getAliases(), aliasTranslation);
+        TranslatorContextToZ3.addGhostFunctions(z3, context.getGhosts(), funcTranslation);
+        TranslatorContextToZ3.addGhostStates(z3, context.getGhostStates(), funcTranslation);
     }
 
     @SuppressWarnings("unchecked")
@@ -66,17 +65,19 @@ public Counterexample getCounterexample(Model model) {
             if (decl.getArity() == 0) {
                 Symbol name = decl.getName();
                 Expr<?> value = model.getConstInterp(decl);
+                String assignment = name + " == " + value;
                 // Skip values of uninterpreted sorts
                 if (value.getSort().getSortKind() != Z3_sort_kind.Z3_UNINTERPRETED_SORT)
-                    assignments.add(name + " == " + value);
+                    assignments.add(assignment);
             }
         }
         // Extract function application values
         for (Map.Entry<String, Expr<?>> entry : funcAppTranslation.entrySet()) {
-            String label = entry.getKey();
+            String name = entry.getKey();
             Expr<?> application = entry.getValue();
             Expr<?> value = model.eval(application, true);
-            assignments.add(label + " = " + value);
+            String assignment = name + " == " + value;
+            assignments.add(assignment);
         }
         return new Counterexample(assignments);
     }