Skip to content

Commit 5c73350

Browse files
rcosta358rcosta358
committed
Use VC Implication Simplification
1 parent 935a168 commit 5c73350

5 files changed

Lines changed: 41 additions & 38 deletions

File tree

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

Lines changed: 16 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,9 @@
55
import java.util.stream.Collectors;
66

77
import liquidjava.diagnostics.TranslationTable;
8+
import liquidjava.processor.VCImplication;
89
import liquidjava.rj_language.ast.Expression;
910
import liquidjava.rj_language.ast.formatter.VariableFormatter;
10-
import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
1111
import liquidjava.smt.Counterexample;
1212
import spoon.reflect.cu.SourcePosition;
1313

@@ -18,14 +18,16 @@
1818
*/
1919
public class RefinementError extends LJError {
2020

21-
private final ValDerivationNode expected;
22-
private final ValDerivationNode found;
21+
private final VCImplication expected;
22+
private final VCImplication found;
2323
private final Counterexample counterexample;
2424

25-
public RefinementError(SourcePosition position, ValDerivationNode expected, ValDerivationNode found,
25+
public RefinementError(SourcePosition position, VCImplication expected, VCImplication found,
2626
TranslationTable translationTable, Counterexample counterexample, String customMessage) {
27-
super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue().toDisplayString(),
28-
expected.getValue().toDisplayString()), position, translationTable, customMessage);
27+
super("Refinement Error",
28+
String.format("%s is not a subtype of %s", found.toPredicate().getExpression().toDisplayString(),
29+
expected.toPredicate().getExpression().toDisplayString()),
30+
position, translationTable, customMessage);
2931
this.expected = expected;
3032
this.found = found;
3133
this.counterexample = counterexample;
@@ -44,12 +46,14 @@ public String getCounterExampleString() {
4446
return null;
4547

4648
List<String> foundVarNames = new ArrayList<>();
47-
found.getValue().getVariableNames(foundVarNames);
49+
Expression foundExpression = found.toPredicate().getExpression();
50+
Expression expectedExpression = expected.toPredicate().getExpression();
51+
foundExpression.getVariableNames(foundVarNames);
4852
// also keep resolved static-final constants (e.g. Integer.MAX_VALUE) referenced by either side of the
4953
// subtyping check, so the counterexample maps the symbolic name back to its compile-time value
50-
found.getValue().getResolvedConstantNames(foundVarNames);
51-
expected.getValue().getResolvedConstantNames(foundVarNames);
52-
List<String> foundAssignments = found.getValue().getConjuncts().stream().map(Expression::toString).toList();
54+
foundExpression.getResolvedConstantNames(foundVarNames);
55+
expectedExpression.getResolvedConstantNames(foundVarNames);
56+
List<String> foundAssignments = foundExpression.getConjuncts().stream().map(Expression::toString).toList();
5357
String counterexampleString = counterexample.assignments().stream()
5458
// only include variables that appear in the found value and are not already fixed there
5559
.filter(a -> foundVarNames.contains(a.first())
@@ -69,11 +73,11 @@ public Counterexample getCounterexample() {
6973
return counterexample;
7074
}
7175

72-
public ValDerivationNode getExpected() {
76+
public VCImplication getExpected() {
7377
return expected;
7478
}
7579

76-
public ValDerivationNode getFound() {
80+
public VCImplication getFound() {
7781
return found;
7882
}
7983
}

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

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

33
import liquidjava.diagnostics.TranslationTable;
4-
import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
4+
import liquidjava.processor.VCImplication;
55
import spoon.reflect.cu.SourcePosition;
66

77
/**
@@ -11,23 +11,25 @@
1111
*/
1212
public class StateRefinementError extends LJError {
1313

14-
private final ValDerivationNode expected;
15-
private final ValDerivationNode found;
14+
private final VCImplication expected;
15+
private final VCImplication found;
1616

17-
public StateRefinementError(SourcePosition position, ValDerivationNode expected, ValDerivationNode found,
17+
public StateRefinementError(SourcePosition position, VCImplication expected, VCImplication found,
1818
TranslationTable translationTable, String customMessage) {
19-
super("State Refinement Error", String.format("Expected state %s but found %s",
20-
expected.getValue().toDisplayString(), found.getValue().toDisplayString()), position, translationTable,
21-
customMessage);
19+
super("State Refinement Error",
20+
String.format("Expected state %s but found %s",
21+
expected.toPredicate().getExpression().toDisplayString(),
22+
found.toPredicate().getExpression().toDisplayString()),
23+
position, translationTable, customMessage);
2224
this.expected = expected;
2325
this.found = found;
2426
}
2527

26-
public ValDerivationNode getExpected() {
28+
public VCImplication getExpected() {
2729
return expected;
2830
}
2931

30-
public ValDerivationNode getFound() {
32+
public VCImplication getFound() {
3133
return found;
3234
}
3335
}

‎liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -93,6 +93,10 @@ public VCImplication simplify() {
9393
return VCSimplification.simplifyToFixedPoint(this);
9494
}
9595

96+
public Predicate toPredicate() {
97+
return hasBinder() || hasNext() ? toConjunctions() : refinement;
98+
}
99+
96100
public Predicate toConjunctions() {
97101
Predicate c = new Predicate();
98102
if (name == null && type == null && next == null)

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -53,6 +53,7 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
5353
TranslationTable map = new TranslationTable();
5454
String[] s = { Keys.WILDCARD, Keys.THIS };
5555
VCImplication impl = joinPredicates(expectedType, mainVars, lrv, map);
56+
VCImplication implBeforeChange = impl.clone();
5657
Predicate premisesBeforeChange = impl.toConjunctions();
5758
Predicate premises;
5859
Predicate expected;
@@ -82,7 +83,7 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
8283
DebugLog.smtResult(result);
8384
if (result.isError()) {
8485
throw new RefinementError(element.getPosition(), expectedType.simplify(context),
85-
premisesBeforeChange.simplify(context), map, result.getCounterexample(), customMessage);
86+
implBeforeChange.simplify(), map, result.getCounterexample(), customMessage);
8687
}
8788
}
8889

@@ -405,17 +406,16 @@ private VCImplication buildPremiseChain(TranslationTable map, Predicate... predi
405406
protected void throwRefinementError(SourcePosition position, Predicate expected, Predicate found,
406407
Counterexample counterexample, String customMessage) throws RefinementError {
407408
TranslationTable map = new TranslationTable();
408-
Predicate premises = buildPremiseChain(map, expected, found).toConjunctions();
409-
throw new RefinementError(position, expected.simplify(context), premises.simplify(context), map, counterexample,
409+
VCImplication premises = buildPremiseChain(map, expected, found);
410+
throw new RefinementError(position, expected.simplify(context), premises.simplify(), map, counterexample,
410411
customMessage);
411412
}
412413

413414
protected void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected,
414415
String customMessage) throws StateRefinementError {
415416
TranslationTable map = new TranslationTable();
416417
VCImplication foundState = buildPremiseChain(map, expected, found);
417-
throw new StateRefinementError(position, expected.simplify(context),
418-
foundState.toConjunctions().simplify(context), map, customMessage);
418+
throw new StateRefinementError(position, expected.simplify(context), foundState.simplify(), map, customMessage);
419419
}
420420

421421
protected void throwStateConflictError(SourcePosition position, Predicate expected) throws StateConflictError {

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java‎

Lines changed: 5 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@
99
import liquidjava.diagnostics.DebugLog;
1010
import liquidjava.diagnostics.errors.LJError;
1111
import liquidjava.diagnostics.errors.NotFoundError;
12+
import liquidjava.processor.VCImplication;
1213
import liquidjava.processor.context.AliasWrapper;
1314
import liquidjava.processor.context.Context;
1415
import liquidjava.processor.context.GhostFunction;
@@ -27,10 +28,8 @@
2728
import liquidjava.rj_language.ast.LiteralReal;
2829
import liquidjava.rj_language.ast.UnaryExpression;
2930
import liquidjava.rj_language.ast.Var;
30-
import liquidjava.utils.StaticConstants;
31-
import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
32-
import liquidjava.rj_language.opt.ExpressionSimplifier;
3331
import liquidjava.rj_language.parsing.RefinementsParser;
32+
import liquidjava.utils.StaticConstants;
3433
import liquidjava.utils.Utils;
3534
import liquidjava.utils.constants.Keys;
3635
import liquidjava.utils.constants.Ops;
@@ -260,15 +259,9 @@ public Predicate getOrigin() {
260259
return this;
261260
}
262261

263-
public ValDerivationNode simplify(Context context) {
264-
// collect aliases from context
265-
Map<String, AliasDTO> aliases = new HashMap<>();
266-
for (AliasWrapper aw : context.getAliases()) {
267-
aliases.put(aw.getName(), aw.createAliasDTO());
268-
}
269-
// simplify expression
270-
ValDerivationNode result = ExpressionSimplifier.simplify(exp.clone(), aliases);
271-
DebugLog.simplification(this.getExpression(), result.getValue());
262+
public VCImplication simplify(Context context) {
263+
VCImplication result = new VCImplication(clone()).simplify();
264+
DebugLog.simplification(this.getExpression(), result.getRefinement().getExpression());
272265
return result;
273266
}
274267

0 commit comments

Comments
 (0)