Skip to content

Improve Counterexamples #169

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
rcosta358 wants to merge 5 commits into
base: main
Choose a base branch
from
Open

Improve Counterexamples #169

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
f523621
Improve Counterexamples
rcosta358 Mar 4, 2026
f7f3709
Remove Details Color
rcosta358 Mar 4, 2026
ba28952
Formatting
rcosta358 Mar 4, 2026
bdbd8c0
Check All Variable Refinements
rcosta358 Mar 5, 2026
0d2d9e7
Only Get `ctxVars` in the Current Scope
rcosta358 Mar 5, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);

Expand Down
14 changes: 8 additions & 6 deletions liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,20 +27,22 @@ 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("");
// join assignements with &&
String counterexampleExp = String.join(" && ", counterexample.assignments());

// check if counterexample is trivial (same as the found value)
if (counterexampleExp.equals(found.getValue().toString()))
return "";
return null;

return counterexampleExp;
}
Expand Down
46 changes: 23 additions & 23 deletions liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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();
}
Expand All @@ -86,6 +86,19 @@ public Map<String, CtTypeReference<?>> getContext() {
return ret;
}

public Set<String> getVariableRefinements() {
Set<RefinedVariable> vars = new HashSet<>();
vars.addAll(ctxVars.peek());
vars.addAll(ctxInstanceVars);
vars.addAll(ctxGlobalVars);
Set<String> refinements = new HashSet<>();
for (RefinedVariable var : vars) {
if (var.getRefinement() != null)
refinements.add(var.getRefinement().toString());
}
return refinements;
}

// ---------------------- Global variables ----------------------
public void addGlobalVariableToContext(String simpleName, String location, CtTypeReference<?> type, Predicate c) {
RefinedVariable vi = new Variable(simpleName, location, type, c);
Expand Down Expand Up @@ -172,22 +185,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);
}
Expand Down Expand Up @@ -229,7 +229,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);
Expand All @@ -243,37 +243,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()) {
Expand Down
2 changes: 1 addition & 1 deletion liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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());
Expand Down
5 changes: 4 additions & 1 deletion liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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;
Expand Down Expand Up @@ -36,7 +38,8 @@ public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context conte
// subRef is not a subtype of supRef
if (result.equals(Status.SATISFIABLE)) {
Model model = solver.getModel();
Counterexample counterexample = tz3.getCounterexample(model);
Set<String> variableRefinements = context.getVariableRefinements();
Counterexample counterexample = tz3.getCounterexample(model, variableRefinements);
return SMTResult.error(counterexample);
}
}
Expand Down
28 changes: 16 additions & 12 deletions liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -20,6 +19,7 @@
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.stream.Collectors;

import liquidjava.diagnostics.errors.LJError;
Expand All @@ -41,12 +41,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")
Expand All @@ -59,24 +59,28 @@ public Solver makeSolverForExpression(Expr<?> e) {
/**
* Extracts the counterexample from the Z3 model
*/
public Counterexample getCounterexample(Model model) {
public Counterexample getCounterexample(Model model, Set<String> variableRefinements) {
List<String> assignments = new ArrayList<>();
// Extract constant variable assignments
for (FuncDecl<?> decl : model.getDecls()) {
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);
if (value.getSort().getSortKind() != Z3_sort_kind.Z3_UNINTERPRETED_SORT
&& !variableRefinements.contains(assignment))
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;
if (!variableRefinements.contains(assignment))
assignments.add(assignment);
}
return new Counterexample(assignments);
}
Expand Down