Skip to content

Commit 401725e

Browse files
rcosta358rcosta358
committed
Merge branch 'main' into constraint-simplification
2 parents 9b80418 + ec170de commit 401725e

14 files changed

Lines changed: 740 additions & 89 deletions

File tree

‎liquidjava-example/src/main/java/testSuite/ErrorAssignmentBeforeReturn.java‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
// Refinement Error
2+
package testSuite;
3+
4+
import liquidjava.specification.Refinement;
5+
6+
public class ErrorAssignmentBeforeReturn {
7+
@Refinement("_ > 0")
8+
static int example(int x) {
9+
x = x + 1;
10+
return x;
11+
}
12+
}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ public <T> void visitCtInterface(CtInterface<T> intrface) {
4747
this.prefix = literal.getValue();
4848
if (!classExists(prefix)) {
4949
String message = String.format("Could not find class '%s'", prefix);
50-
diagnostics.add(new ExternalClassNotFoundWarning(externalRef.get().getPosition(), message, prefix));
50+
diagnostics.add(new ExternalClassNotFoundWarning(literal.getPosition(), message, prefix));
5151
return;
5252
}
5353
getRefinementFromAnnotation(intrface);

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

Lines changed: 11 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -70,12 +70,14 @@ public Optional<Predicate> getRefinementFromAnnotation(CtElement element) throws
7070
ref = Optional.of(value);
7171

7272
} else if (an.contentEquals("liquidjava.specification.RefinementPredicate")) {
73-
String value = getStringFromAnnotation(ann.getValue("value"));
74-
getGhostFunction(value, element, ann.getPosition());
73+
CtExpression<String> rawValue = ann.getValue("value");
74+
String value = getStringFromAnnotation(rawValue);
75+
getGhostFunction(value, element, rawValue.getPosition());
7576

7677
} else if (an.contentEquals("liquidjava.specification.RefinementAlias")) {
77-
String value = getStringFromAnnotation(ann.getValue("value"));
78-
handleAlias(value, element, ann.getPosition());
78+
CtExpression<String> rawValue = ann.getValue("value");
79+
String value = getStringFromAnnotation(rawValue);
80+
handleAlias(value, element, rawValue.getPosition());
7981
}
8082
}
8183
if (ref.isPresent()) {
@@ -116,7 +118,7 @@ public void handleStateSetsFromAnnotation(CtElement element) throws LJError {
116118
}
117119
if (an.contentEquals("liquidjava.specification.Ghost")) {
118120
CtLiteral<String> s = (CtLiteral<String>) ann.getAllValues().get("value");
119-
createStateGhost(s.getValue(), element, ann.getPosition());
121+
createStateGhost(s.getValue(), element, s.getPosition());
120122
}
121123
}
122124
}
@@ -167,7 +169,8 @@ protected GhostDTO getGhostDeclaration(String value, SourcePosition position) th
167169
return RefinementsParser.parseGhostDeclaration(value);
168170
} catch (LJError e) {
169171
// add location info to error
170-
e.setPosition(position);
172+
if (e.getPosition() == null)
173+
e.setPosition(position);
171174
throw e;
172175
}
173176
}
@@ -259,7 +262,8 @@ protected void handleAlias(String ref, CtElement element, SourcePosition positio
259262
}
260263
} catch (LJError e) {
261264
// add location info to error
262-
e.setPosition(position);
265+
if (e.getPosition() == null)
266+
e.setPosition(position);
263267
throw e;
264268
}
265269
}

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

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

33
import java.util.ArrayList;
4+
import java.util.HashSet;
45
import java.util.List;
6+
import java.util.Optional;
57
import java.util.Set;
68
import java.util.Stack;
79
import java.util.function.Consumer;
@@ -12,9 +14,13 @@
1214
import liquidjava.processor.VCImplication;
1315
import liquidjava.processor.context.*;
1416
import liquidjava.rj_language.Predicate;
17+
import liquidjava.rj_language.ast.Expression;
18+
import liquidjava.rj_language.ast.Ite;
19+
import liquidjava.rj_language.ast.Var;
1520
import liquidjava.smt.Counterexample;
1621
import liquidjava.smt.SMTEvaluator;
1722
import liquidjava.smt.SMTResult;
23+
import liquidjava.utils.Utils;
1824
import liquidjava.utils.constants.Keys;
1925
import spoon.reflect.cu.SourcePosition;
2026
import spoon.reflect.declaration.CtElement;
@@ -53,13 +59,17 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
5359
expected = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f);
5460
} catch (LJError e) {
5561
// add location info to error
56-
e.setPosition(element.getPosition());
62+
if (e.getPosition() == null) {
63+
SourcePosition pos = Utils.getFirstLJAnnotationValuePosition(element);
64+
e.setPosition(pos);
65+
}
5766
throw e;
5867
}
59-
SMTResult result = verifySMTSubtype(expected, premises, element.getPosition());
68+
SourcePosition annotationValuePos = Utils.getFirstLJAnnotationValuePosition(element);
69+
SMTResult result = verifySMTSubtype(expected, premises, annotationValuePos);
6070
if (result.isError()) {
61-
throw new RefinementError(element.getPosition(), expectedType.simplify(), premisesBeforeChange.simplify(),
62-
map, result.getCounterexample(), customMessage);
71+
throw new RefinementError(element.getPosition(), expectedType.simplify(context),
72+
premisesBeforeChange.simplify(context), map, result.getCounterexample(), customMessage);
6373
}
6474
}
6575

@@ -94,7 +104,9 @@ public SMTResult verifySMTSubtype(Predicate expected, Predicate found, SourcePos
94104
try {
95105
return new SMTEvaluator().verifySubtype(found, expected, context);
96106
} catch (LJError e) {
97-
e.setPosition(position);
107+
if (e.getPosition() == null) {
108+
e.setPosition(position);
109+
}
98110
throw e;
99111
} catch (Exception e) {
100112
throw new CustomError(e.getMessage(), position);
@@ -191,7 +203,18 @@ private VCImplication joinPredicates(Predicate expectedType, List<RefinedVariabl
191203

192204
for (RefinedVariable var : vars) { // join refinements of vars
193205
addMap(var, map);
194-
VCImplication si = new VCImplication(var.getName(), var.getType(), var.getRefinement());
206+
207+
// if the last instance is already in vars, it is already in the premises
208+
// adding "var == lastInstance" would create a contradictory cycle (e.g. x == x + 1 for x = x + 1)
209+
// so we need to use main refinement to avoid this
210+
Predicate refinement = var.getRefinement();
211+
if (var instanceof Variable v) {
212+
Optional<VariableInstance> lastInst = v.getLastInstance();
213+
if (lastInst.isPresent() && vars.contains(lastInst.get())
214+
&& hasDependencyCycle(lastInst.get(), var.getName(), vars, new HashSet<>()))
215+
refinement = v.getMainRefinement();
216+
}
217+
VCImplication si = new VCImplication(var.getName(), var.getType(), refinement);
195218
if (lastSi != null) {
196219
lastSi.setNext(si);
197220
lastSi = si;
@@ -268,6 +291,22 @@ void removePathVariableThatIncludes(String otherVar) {
268291
.forEach(pathVariables::remove);
269292
}
270293

294+
private boolean hasDependencyCycle(RefinedVariable rv, String var, List<RefinedVariable> vars, Set<String> seen) {
295+
if (!seen.add(rv.getName()))
296+
return false;
297+
Expression e = rv.getRefinement().getExpression();
298+
return hasVariable(e, var) || vars.stream().filter(o -> hasVariable(e, o.getName()))
299+
.anyMatch(o -> hasDependencyCycle(o, var, vars, seen));
300+
}
301+
302+
private boolean hasVariable(Expression exp, String var) {
303+
if (exp instanceof Var v)
304+
return v.getName().equals(var);
305+
if (exp instanceof Ite ite)
306+
return hasVariable(ite.getThen(), var) || hasVariable(ite.getElse(), var);
307+
return exp.getChildren().stream().anyMatch(c -> hasVariable(c, var));
308+
}
309+
271310
// Errors---------------------------------------------------------------------------------------------------
272311

273312
protected void throwRefinementError(SourcePosition position, Predicate expected, Predicate found,
@@ -277,7 +316,7 @@ protected void throwRefinementError(SourcePosition position, Predicate expected,
277316
gatherVariables(found, lrv, mainVars);
278317
TranslationTable map = new TranslationTable();
279318
Predicate premises = joinPredicates(expected, mainVars, lrv, map).toConjunctions();
280-
throw new RefinementError(position, expected.simplify(), premises.simplify(), map, counterexample,
319+
throw new RefinementError(position, expected.simplify(context), premises.simplify(context), map, counterexample,
281320
customMessage);
282321
}
283322

@@ -288,7 +327,7 @@ protected void throwStateRefinementError(SourcePosition position, Predicate foun
288327
TranslationTable map = new TranslationTable();
289328
VCImplication foundState = joinPredicates(found, mainVars, lrv, map);
290329
throw new StateRefinementError(position, expected.getExpression(),
291-
foundState.toConjunctions().simplify().getValue(), map, customMessage);
330+
foundState.toConjunctions().simplify(context).getValue(), map, customMessage);
292331
}
293332

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

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -225,7 +225,8 @@ private static Predicate createStatePredicate(String value, String targetClass,
225225
c = c.changeOldMentions(nameOld, name);
226226
boolean ok = tc.checkStateSMT(new Predicate(), c.negate(), e.getPosition());
227227
if (ok) {
228-
tc.throwStateConflictError(e.getPosition(), p);
228+
SourcePosition pos = Utils.getLJAnnotationPosition(e, value);
229+
tc.throwStateConflictError(pos, p);
229230
}
230231
return c1;
231232
}

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

Lines changed: 47 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -86,8 +86,10 @@ protected Expression parse(String ref, CtElement element) throws LJError {
8686
return RefinementsParser.createAST(ref, prefix);
8787
} catch (LJError e) {
8888
// add location info to error
89-
SourcePosition pos = Utils.getLJAnnotationPosition(element, ref);
90-
e.setPosition(pos);
89+
if (e.getPosition() == null) {
90+
SourcePosition pos = Utils.getLJAnnotationPosition(element, ref);
91+
e.setPosition(pos);
92+
}
9193
throw e;
9294
}
9395
}
@@ -183,18 +185,52 @@ public Predicate clone() {
183185
return new Predicate(exp.clone());
184186
}
185187

188+
@Override
189+
public boolean equals(Object obj) {
190+
if (this == obj)
191+
return true;
192+
if (obj == null)
193+
return false;
194+
if (getClass() != obj.getClass())
195+
return false;
196+
Predicate other = (Predicate) obj;
197+
return exp.equals(other.exp);
198+
}
199+
186200
public Expression getExpression() {
187201
return exp;
188202
}
189203

190-
public ValDerivationNode simplify() {
191-
return ExpressionSimplifier.simplify(exp.clone());
204+
public ValDerivationNode simplify(Context context) {
205+
// collect aliases from context
206+
Map<String, AliasDTO> aliases = new HashMap<>();
207+
for (AliasWrapper aw : context.getAliases()) {
208+
aliases.put(aw.getName(), aw.createAliasDTO());
209+
}
210+
// simplify expression
211+
return ExpressionSimplifier.simplify(exp.clone(), aliases);
192212
}
193213

194214
private static boolean isBooleanLiteral(Expression expr, boolean value) {
195215
return expr instanceof LiteralBoolean && expr.isBooleanTrue() == value;
196216
}
197217

218+
/**
219+
* Checks if c2 is a conjunct in c1
220+
*/
221+
private static boolean containsConjunct(Predicate c1, Predicate c2) {
222+
if (c1.toString().equals(c2.toString()))
223+
return true;
224+
if (c1.getExpression()instanceof BinaryExpression be && be.getOperator().equals(Ops.AND))
225+
return containsConjunct(new Predicate(be.getFirstOperand()), c2)
226+
|| containsConjunct(new Predicate(be.getSecondOperand()), c2);
227+
return false;
228+
}
229+
230+
/**
231+
* Creates a new predicate representing the conjunction of c1 and c2 Contains simplification rules for redundant
232+
* conjuncts such as not adding conjunct if already present in conjunction
233+
*/
198234
public static Predicate createConjunction(Predicate c1, Predicate c2) {
199235
// simplification: (true && x) = x, (false && x) = false
200236
if (isBooleanLiteral(c1.getExpression(), true))
@@ -205,6 +241,13 @@ public static Predicate createConjunction(Predicate c1, Predicate c2) {
205241
return c1;
206242
if (isBooleanLiteral(c2.getExpression(), false))
207243
return c2;
244+
245+
// check if conjunct is already present in the conjunction
246+
if (containsConjunct(c1, c2))
247+
return c1;
248+
if (containsConjunct(c2, c1))
249+
return c2;
250+
208251
return new Predicate(new BinaryExpression(c1.getExpression(), Ops.AND, c2.getExpression()));
209252
}
210253

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/AliasExpansion.java‎

Lines changed: 91 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,91 @@
1+
package liquidjava.rj_language.opt;
2+
3+
import java.util.Map;
4+
5+
import liquidjava.processor.facade.AliasDTO;
6+
import liquidjava.rj_language.ast.AliasInvocation;
7+
import liquidjava.rj_language.ast.BinaryExpression;
8+
import liquidjava.rj_language.ast.Expression;
9+
import liquidjava.rj_language.ast.GroupExpression;
10+
import liquidjava.rj_language.ast.UnaryExpression;
11+
import liquidjava.rj_language.ast.Var;
12+
import liquidjava.rj_language.opt.derivation_node.BinaryDerivationNode;
13+
import liquidjava.rj_language.opt.derivation_node.DerivationNode;
14+
import liquidjava.rj_language.opt.derivation_node.UnaryDerivationNode;
15+
import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
16+
17+
public class AliasExpansion {
18+
19+
/**
20+
* Expands alias invocations in a derivation node to their definitions, storing the expanded body as the origin of
21+
* each alias invocation node.
22+
*/
23+
public static ValDerivationNode expand(ValDerivationNode node, Map<String, AliasDTO> aliases) {
24+
return expandRecursive(node, aliases);
25+
}
26+
27+
private static ValDerivationNode expandRecursive(ValDerivationNode node, Map<String, AliasDTO> aliases) {
28+
Expression exp = node.getValue();
29+
30+
// expand alias invocation
31+
if (exp instanceof AliasInvocation ai) {
32+
return expandAlias(ai, aliases);
33+
}
34+
35+
// recurse into binary expressions
36+
if (exp instanceof BinaryExpression binary) {
37+
ValDerivationNode leftNode;
38+
ValDerivationNode rightNode;
39+
if (node.getOrigin()instanceof BinaryDerivationNode binOrigin) {
40+
leftNode = expandRecursive(binOrigin.getLeft(), aliases);
41+
rightNode = expandRecursive(binOrigin.getRight(), aliases);
42+
} else {
43+
leftNode = expandRecursive(new ValDerivationNode(binary.getFirstOperand(), null), aliases);
44+
rightNode = expandRecursive(new ValDerivationNode(binary.getSecondOperand(), null), aliases);
45+
}
46+
boolean hasExpansion = leftNode.getOrigin() != null || rightNode.getOrigin() != null;
47+
DerivationNode origin = hasExpansion ? new BinaryDerivationNode(leftNode, rightNode, binary.getOperator())
48+
: node.getOrigin();
49+
return new ValDerivationNode(exp, origin);
50+
}
51+
52+
// recurse into unary expressions
53+
if (exp instanceof UnaryExpression unary) {
54+
ValDerivationNode operandNode;
55+
if (node.getOrigin()instanceof UnaryDerivationNode unaryOrigin) {
56+
operandNode = expandRecursive(unaryOrigin.getOperand(), aliases);
57+
} else {
58+
operandNode = expandRecursive(new ValDerivationNode(unary.getChildren().get(0), null), aliases);
59+
}
60+
DerivationNode origin = operandNode.getOrigin() != null
61+
? new UnaryDerivationNode(operandNode, unary.getOp()) : node.getOrigin();
62+
return new ValDerivationNode(exp, origin);
63+
}
64+
65+
// recurse into group expressions
66+
if (exp instanceof GroupExpression group && group.getChildren().size() == 1) {
67+
return expandRecursive(new ValDerivationNode(group.getChildren().get(0), node.getOrigin()), aliases);
68+
}
69+
70+
return node;
71+
}
72+
73+
private static ValDerivationNode expandAlias(AliasInvocation ai, Map<String, AliasDTO> aliases) {
74+
AliasDTO dto = aliases.get(ai.getName());
75+
76+
// no alias found
77+
if (dto == null || dto.getExpression() == null) {
78+
return new ValDerivationNode(ai, null);
79+
}
80+
81+
// substitute parameters in the body with the invocation arguments
82+
Expression body = dto.getExpression().clone();
83+
for (int i = 0; i < ai.getArgs().size() && i < dto.getVarNames().size(); i++) {
84+
body = body.substitute(new Var(dto.getVarNames().get(i)), ai.getArgs().get(i));
85+
}
86+
87+
// recursively expand the body
88+
ValDerivationNode expandedBody = expandRecursive(new ValDerivationNode(body, null), aliases);
89+
return new ValDerivationNode(ai, expandedBody);
90+
}
91+
}

0 commit comments

Comments
 (0)