Skip to content

Commit 1d79229

Browse files
rcosta358rcosta358
authored
Improve Counterexamples (#169)
1 parent 848eeb5 commit 1d79229

6 files changed

Lines changed: 50 additions & 45 deletions

File tree

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

Lines changed: 21 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,9 @@
11
package liquidjava.diagnostics.errors;
22

3+
import java.util.ArrayList;
4+
import java.util.List;
5+
import java.util.stream.Collectors;
6+
37
import liquidjava.diagnostics.TranslationTable;
48
import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
59
import liquidjava.smt.Counterexample;
@@ -27,22 +31,30 @@ public RefinementError(SourcePosition position, ValDerivationNode expected, ValD
2731

2832
@Override
2933
public String getDetails() {
30-
return "Counterexample: " + getCounterExampleString();
34+
String counterexampleString = getCounterExampleString();
35+
if (counterexampleString == null)
36+
return "";
37+
return "Counterexample: " + counterexampleString;
3138
}
3239

3340
public String getCounterExampleString() {
3441
if (counterexample == null || counterexample.assignments().isEmpty())
35-
return "";
42+
return null;
3643

37-
// filter fresh variables and join assignements with &&
38-
String counterexampleExp = counterexample.assignments().stream().filter(a -> !a.startsWith("#fresh_"))
39-
.reduce((a, b) -> a + " && " + b).orElse("");
44+
List<String> foundVarNames = new ArrayList<>();
45+
found.getValue().getVariableNames(foundVarNames);
46+
String counterexampleString = counterexample.assignments().stream()
47+
// only include variables that appear in the found value
48+
.filter(a -> foundVarNames.contains(a.first()))
49+
// format as "var == value"
50+
.map(a -> a.first() + " == " + a.second())
51+
// join with "&&"
52+
.collect(Collectors.joining(" && "));
4053

41-
// check if counterexample is trivial (same as the found value)
42-
if (counterexampleExp.equals(found.getValue().toString()))
43-
return "";
54+
if (counterexampleString.isEmpty() || counterexampleString.equals(found.getValue().toString()))
55+
return null;
4456

45-
return counterexampleExp;
57+
return counterexampleString;
4658
}
4759

4860
public Counterexample getCounterexample() {

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

Lines changed: 10 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -55,15 +55,15 @@ public void reinitializeAllContext() {
5555
public void enterContext() {
5656
ctxVars.push(new ArrayList<>());
5757
// make each variable enter context
58-
for (RefinedVariable vi : getAllVariables())
58+
for (RefinedVariable vi : getAllCtxVars())
5959
if (vi instanceof Variable)
6060
((Variable) vi).enterContext();
6161
}
6262

6363
public void exitContext() {
6464
ctxVars.pop();
6565
// make each variable exit context
66-
for (RefinedVariable vi : getAllVariables())
66+
for (RefinedVariable vi : getAllCtxVars())
6767
if (vi instanceof Variable)
6868
((Variable) vi).exitContext();
6969
}
@@ -172,22 +172,9 @@ public boolean hasVariable(String name) {
172172
return getVariableByName(name) != null;
173173
}
174174

175-
/**
176-
* Lists all variables inside the stack
177-
*
178-
* @return list of all variables
179-
*/
180-
public List<RefinedVariable> getAllVariables() {
181-
List<RefinedVariable> lvi = new ArrayList<>();
182-
for (List<RefinedVariable> l : ctxVars) {
183-
lvi.addAll(l);
184-
}
185-
return lvi;
186-
}
187-
188175
public List<RefinedVariable> getAllVariablesWithSupertypes() {
189176
List<RefinedVariable> lvi = new ArrayList<>();
190-
for (RefinedVariable rv : getAllVariables()) {
177+
for (RefinedVariable rv : getAllCtxVars()) {
191178
if (!rv.getSuperTypes().isEmpty())
192179
lvi.add(rv);
193180
}
@@ -229,7 +216,7 @@ public Variable getVariableFromInstance(VariableInstance vi) {
229216
return vi.getParent().orElse(null);
230217
}
231218

232-
public List<RefinedVariable> getCtxVars() {
219+
public List<RefinedVariable> getAllCtxVars() {
233220
List<RefinedVariable> lvi = new ArrayList<>();
234221
for (List<RefinedVariable> l : ctxVars) {
235222
lvi.addAll(l);
@@ -243,37 +230,37 @@ public List<RefinedVariable> getCtxInstanceVars() {
243230

244231
// ---------------------- Variables - if information storing ----------------------
245232
public void variablesSetBeforeIf() {
246-
for (RefinedVariable vi : getAllVariables())
233+
for (RefinedVariable vi : getAllCtxVars())
247234
if (vi instanceof Variable)
248235
((Variable) vi).saveInstanceBeforeIf();
249236
}
250237

251238
public void variablesSetThenIf() {
252-
for (RefinedVariable vi : getAllVariables())
239+
for (RefinedVariable vi : getAllCtxVars())
253240
if (vi instanceof Variable)
254241
((Variable) vi).saveInstanceThen();
255242
}
256243

257244
public void variablesSetElseIf() {
258-
for (RefinedVariable vi : getAllVariables())
245+
for (RefinedVariable vi : getAllCtxVars())
259246
if (vi instanceof Variable)
260247
((Variable) vi).saveInstanceElse();
261248
}
262249

263250
public void variablesNewIfCombination() {
264-
for (RefinedVariable vi : getAllVariables())
251+
for (RefinedVariable vi : getAllCtxVars())
265252
if (vi instanceof Variable)
266253
((Variable) vi).newIfCombination();
267254
}
268255

269256
public void variablesFinishIfCombination() {
270-
for (RefinedVariable vi : getAllVariables())
257+
for (RefinedVariable vi : getAllCtxVars())
271258
if (vi instanceof Variable)
272259
((Variable) vi).finishIfCombination();
273260
}
274261

275262
public void variablesCombineFromIf(Predicate cond) {
276-
for (RefinedVariable vi : getAllVariables()) {
263+
for (RefinedVariable vi : getAllCtxVars()) {
277264
if (vi instanceof Variable) {
278265
Optional<VariableInstance> ovi = ((Variable) vi).getIfInstanceCombination(getCounter(), cond);
279266
if (ovi.isPresent()) {

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,7 @@ public void saveContext(CtElement element, Context context) {
4949
String file = pos.getFile().getAbsolutePath();
5050
String scope = getScopePosition(element);
5151
fileScopeVars.putIfAbsent(file, new HashMap<>());
52-
fileScopeVars.get(file).put(scope, new HashSet<>(context.getCtxVars()));
52+
fileScopeVars.get(file).put(scope, new HashSet<>(context.getAllCtxVars()));
5353

5454
// add other elements in context
5555
instanceVars.addAll(context.getCtxInstanceVars());

‎liquidjava-verifier/src/main/java/liquidjava/smt/Counterexample.java‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,7 @@
22

33
import java.util.List;
44

5-
public record Counterexample(List<String> assignments) {
5+
import liquidjava.utils.Pair;
6+
7+
public record Counterexample(List<Pair<String, String>> assignments) {
68
}

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
package liquidjava.smt;
22

3+
import java.util.Set;
4+
35
import com.martiansoftware.jsap.SyntaxException;
46
import com.microsoft.z3.Expr;
57
import com.microsoft.z3.Model;

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

Lines changed: 13 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,6 @@
66
import com.microsoft.z3.Expr;
77
import com.microsoft.z3.FPExpr;
88
import com.microsoft.z3.FuncDecl;
9-
import com.microsoft.z3.FuncInterp;
109
import com.microsoft.z3.IntExpr;
1110
import com.microsoft.z3.IntNum;
1211
import com.microsoft.z3.RealExpr;
@@ -25,6 +24,7 @@
2524
import liquidjava.diagnostics.errors.LJError;
2625
import liquidjava.diagnostics.errors.NotFoundError;
2726
import liquidjava.processor.context.AliasWrapper;
27+
import liquidjava.utils.Pair;
2828
import liquidjava.utils.Utils;
2929
import liquidjava.utils.constants.Keys;
3030
import com.microsoft.z3.enumerations.Z3_sort_kind;
@@ -41,12 +41,12 @@ public class TranslatorToZ3 implements AutoCloseable {
4141
private final Map<String, Expr<?>> funcAppTranslation = new HashMap<>();
4242
private final Map<Expr<?>, String> exprToNameTranslation = new HashMap<>();
4343

44-
public TranslatorToZ3(liquidjava.processor.context.Context c) {
45-
TranslatorContextToZ3.translateVariables(z3, c.getContext(), varTranslation);
46-
TranslatorContextToZ3.storeVariablesSubtypes(z3, c.getAllVariablesWithSupertypes(), varSuperTypes);
47-
TranslatorContextToZ3.addAliases(c.getAliases(), aliasTranslation);
48-
TranslatorContextToZ3.addGhostFunctions(z3, c.getGhosts(), funcTranslation);
49-
TranslatorContextToZ3.addGhostStates(z3, c.getGhostStates(), funcTranslation);
44+
public TranslatorToZ3(liquidjava.processor.context.Context context) {
45+
TranslatorContextToZ3.translateVariables(z3, context.getContext(), varTranslation);
46+
TranslatorContextToZ3.storeVariablesSubtypes(z3, context.getAllVariablesWithSupertypes(), varSuperTypes);
47+
TranslatorContextToZ3.addAliases(context.getAliases(), aliasTranslation);
48+
TranslatorContextToZ3.addGhostFunctions(z3, context.getGhosts(), funcTranslation);
49+
TranslatorContextToZ3.addGhostStates(z3, context.getGhostStates(), funcTranslation);
5050
}
5151

5252
@SuppressWarnings("unchecked")
@@ -60,23 +60,25 @@ public Solver makeSolverForExpression(Expr<?> e) {
6060
* Extracts the counterexample from the Z3 model
6161
*/
6262
public Counterexample getCounterexample(Model model) {
63-
List<String> assignments = new ArrayList<>();
63+
List<Pair<String, String>> assignments = new ArrayList<>();
6464
// Extract constant variable assignments
6565
for (FuncDecl<?> decl : model.getDecls()) {
6666
if (decl.getArity() == 0) {
6767
Symbol name = decl.getName();
6868
Expr<?> value = model.getConstInterp(decl);
69+
Pair<String, String> assignment = new Pair<>(name.toString(), value.toString());
6970
// Skip values of uninterpreted sorts
7071
if (value.getSort().getSortKind() != Z3_sort_kind.Z3_UNINTERPRETED_SORT)
71-
assignments.add(name + " == " + value);
72+
assignments.add(assignment);
7273
}
7374
}
7475
// Extract function application values
7576
for (Map.Entry<String, Expr<?>> entry : funcAppTranslation.entrySet()) {
76-
String label = entry.getKey();
77+
String name = entry.getKey();
7778
Expr<?> application = entry.getValue();
7879
Expr<?> value = model.eval(application, true);
79-
assignments.add(label + " = " + value);
80+
Pair<String, String> assignment = new Pair<>(name, value.toString());
81+
assignments.add(assignment);
8082
}
8183
return new Counterexample(assignments);
8284
}

0 commit comments

Comments
 (0)