Skip to content

Commit bdbd8c0

Browse files
rcosta358rcosta358
committed
Check All Variable Refinements
In counterexample, check if assignment is already present in all variable refinements, not just instance variable refinements.
1 parent ba28952 commit bdbd8c0

File tree

4 files changed

+31
-33
lines changed

4 files changed

+31
-33
lines changed

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

Lines changed: 23 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
}
@@ -86,6 +86,19 @@ public Map<String, CtTypeReference<?>> getContext() {
8686
return ret;
8787
}
8888

89+
public Set<String> getAllVariableRefinements() {
90+
Set<RefinedVariable> vars = new HashSet<>();
91+
vars.addAll(getAllCtxVars());
92+
vars.addAll(ctxInstanceVars);
93+
vars.addAll(ctxGlobalVars);
94+
Set<String> refinements = new HashSet<>();
95+
for (RefinedVariable var : vars) {
96+
if (var.getRefinement() != null)
97+
refinements.add(var.getRefinement().toString());
98+
}
99+
return refinements;
100+
}
101+
89102
// ---------------------- Global variables ----------------------
90103
public void addGlobalVariableToContext(String simpleName, String location, CtTypeReference<?> type, Predicate c) {
91104
RefinedVariable vi = new Variable(simpleName, location, type, c);
@@ -172,22 +185,9 @@ public boolean hasVariable(String name) {
172185
return getVariableByName(name) != null;
173186
}
174187

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-
188188
public List<RefinedVariable> getAllVariablesWithSupertypes() {
189189
List<RefinedVariable> lvi = new ArrayList<>();
190-
for (RefinedVariable rv : getAllVariables()) {
190+
for (RefinedVariable rv : getAllCtxVars()) {
191191
if (!rv.getSuperTypes().isEmpty())
192192
lvi.add(rv);
193193
}
@@ -229,7 +229,7 @@ public Variable getVariableFromInstance(VariableInstance vi) {
229229
return vi.getParent().orElse(null);
230230
}
231231

232-
public List<RefinedVariable> getCtxVars() {
232+
public List<RefinedVariable> getAllCtxVars() {
233233
List<RefinedVariable> lvi = new ArrayList<>();
234234
for (List<RefinedVariable> l : ctxVars) {
235235
lvi.addAll(l);
@@ -243,37 +243,37 @@ public List<RefinedVariable> getCtxInstanceVars() {
243243

244244
// ---------------------- Variables - if information storing ----------------------
245245
public void variablesSetBeforeIf() {
246-
for (RefinedVariable vi : getAllVariables())
246+
for (RefinedVariable vi : getAllCtxVars())
247247
if (vi instanceof Variable)
248248
((Variable) vi).saveInstanceBeforeIf();
249249
}
250250

251251
public void variablesSetThenIf() {
252-
for (RefinedVariable vi : getAllVariables())
252+
for (RefinedVariable vi : getAllCtxVars())
253253
if (vi instanceof Variable)
254254
((Variable) vi).saveInstanceThen();
255255
}
256256

257257
public void variablesSetElseIf() {
258-
for (RefinedVariable vi : getAllVariables())
258+
for (RefinedVariable vi : getAllCtxVars())
259259
if (vi instanceof Variable)
260260
((Variable) vi).saveInstanceElse();
261261
}
262262

263263
public void variablesNewIfCombination() {
264-
for (RefinedVariable vi : getAllVariables())
264+
for (RefinedVariable vi : getAllCtxVars())
265265
if (vi instanceof Variable)
266266
((Variable) vi).newIfCombination();
267267
}
268268

269269
public void variablesFinishIfCombination() {
270-
for (RefinedVariable vi : getAllVariables())
270+
for (RefinedVariable vi : getAllCtxVars())
271271
if (vi instanceof Variable)
272272
((Variable) vi).finishIfCombination();
273273
}
274274

275275
public void variablesCombineFromIf(Predicate cond) {
276-
for (RefinedVariable vi : getAllVariables()) {
276+
for (RefinedVariable vi : getAllCtxVars()) {
277277
if (vi instanceof Variable) {
278278
Optional<VariableInstance> ovi = ((Variable) vi).getIfInstanceCombination(getCounter(), cond);
279279
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/SMTEvaluator.java‎

Lines changed: 4 additions & 1 deletion
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;
@@ -36,7 +38,8 @@ public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context conte
3638
// subRef is not a subtype of supRef
3739
if (result.equals(Status.SATISFIABLE)) {
3840
Model model = solver.getModel();
39-
Counterexample counterexample = tz3.getCounterexample(model);
41+
Set<String> variableRefinements = context.getAllVariableRefinements();
42+
Counterexample counterexample = tz3.getCounterexample(model, variableRefinements);
4043
return SMTResult.error(counterexample);
4144
}
4245
}

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

Lines changed: 3 additions & 8 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;
@@ -18,7 +17,6 @@
1817
import java.util.ArrayList;
1918
import java.util.Arrays;
2019
import java.util.HashMap;
21-
import java.util.HashSet;
2220
import java.util.List;
2321
import java.util.Map;
2422
import java.util.Set;
@@ -42,16 +40,13 @@ public class TranslatorToZ3 implements AutoCloseable {
4240
private final Map<String, FuncDecl<?>> funcTranslation = new HashMap<>();
4341
private final Map<String, Expr<?>> funcAppTranslation = new HashMap<>();
4442
private final Map<Expr<?>, String> exprToNameTranslation = new HashMap<>();
45-
private final Set<String> instanceVariableRefinements;
4643

4744
public TranslatorToZ3(liquidjava.processor.context.Context context) {
4845
TranslatorContextToZ3.translateVariables(z3, context.getContext(), varTranslation);
4946
TranslatorContextToZ3.storeVariablesSubtypes(z3, context.getAllVariablesWithSupertypes(), varSuperTypes);
5047
TranslatorContextToZ3.addAliases(context.getAliases(), aliasTranslation);
5148
TranslatorContextToZ3.addGhostFunctions(z3, context.getGhosts(), funcTranslation);
5249
TranslatorContextToZ3.addGhostStates(z3, context.getGhostStates(), funcTranslation);
53-
instanceVariableRefinements = context.getCtxInstanceVars().stream().map(v -> v.getRefinement().toString())
54-
.collect(Collectors.toSet());
5550
}
5651

5752
@SuppressWarnings("unchecked")
@@ -64,7 +59,7 @@ public Solver makeSolverForExpression(Expr<?> e) {
6459
/**
6560
* Extracts the counterexample from the Z3 model
6661
*/
67-
public Counterexample getCounterexample(Model model) {
62+
public Counterexample getCounterexample(Model model, Set<String> variableRefinements) {
6863
List<String> assignments = new ArrayList<>();
6964
// Extract constant variable assignments
7065
for (FuncDecl<?> decl : model.getDecls()) {
@@ -74,7 +69,7 @@ public Counterexample getCounterexample(Model model) {
7469
String assignment = name + " == " + value;
7570
// Skip values of uninterpreted sorts
7671
if (value.getSort().getSortKind() != Z3_sort_kind.Z3_UNINTERPRETED_SORT
77-
&& !instanceVariableRefinements.contains(assignment))
72+
&& !variableRefinements.contains(assignment))
7873
assignments.add(assignment);
7974
}
8075
}
@@ -84,7 +79,7 @@ public Counterexample getCounterexample(Model model) {
8479
Expr<?> application = entry.getValue();
8580
Expr<?> value = model.eval(application, true);
8681
String assignment = name + " == " + value;
87-
if (!instanceVariableRefinements.contains(assignment))
82+
if (!variableRefinements.contains(assignment))
8883
assignments.add(assignment);
8984
}
9085
return new Counterexample(assignments);

0 commit comments

Comments
 (0)