diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index 1c548648..d1a743dc 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/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); diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index 24c27336..01233bb0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/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 foundTokens = Arrays.asList(foundValue.split("[^a-zA-Z0-9_#]+")); + List 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; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java index 23176dfd..0527ab68 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java @@ -55,7 +55,7 @@ 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(); } @@ -63,7 +63,7 @@ public void 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 getAllVariables() { - List lvi = new ArrayList<>(); - for (List l : ctxVars) { - lvi.addAll(l); - } - return lvi; - } - public List getAllVariablesWithSupertypes() { List 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 getCtxVars() { + public List getAllCtxVars() { List lvi = new ArrayList<>(); for (List l : ctxVars) { lvi.addAll(l); @@ -243,37 +230,37 @@ public List 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 ovi = ((Variable) vi).getIfInstanceCombination(getCounter(), cond); if (ovi.isPresent()) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java index 0e4db162..5a47adcf 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java +++ b/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()); diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java index 03cfd94e..096a9b95 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java +++ b/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; diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index 96f32f66..c6bf6190 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/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> funcAppTranslation = new HashMap<>(); private final Map, 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> 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); }