Skip to content

Commit 387e19b

Browse files
rcosta358rcosta358
committed
Merge branch 'main' into derive-states
2 parents 883c9ae + 6d1f086 commit 387e19b

8 files changed

Lines changed: 432 additions & 797 deletions

File tree

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

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
package liquidjava.rj_language.opt;
22

33
import liquidjava.rj_language.ast.BinaryExpression;
4+
import liquidjava.rj_language.ast.Enum;
45
import liquidjava.rj_language.ast.Expression;
56
import liquidjava.rj_language.ast.GroupExpression;
67
import liquidjava.rj_language.ast.Ite;
@@ -62,6 +63,16 @@ private static ValDerivationNode foldBinary(ValDerivationNode node) {
6263
Expression left = leftNode.getValue();
6364
Expression right = rightNode.getValue();
6465
String op = binExp.getOperator();
66+
67+
if (left instanceof Enum en && en.getResolvedLiteral() != null) {
68+
left = en.getResolvedLiteral().clone();
69+
leftNode = new ValDerivationNode(left, leftNode);
70+
}
71+
if (right instanceof Enum en && en.getResolvedLiteral() != null) {
72+
right = en.getResolvedLiteral().clone();
73+
rightNode = new ValDerivationNode(right, rightNode);
74+
}
75+
6576
binExp.setChild(0, left);
6677
binExp.setChild(1, right);
6778

@@ -146,6 +157,18 @@ else if (left instanceof LiteralBoolean && right instanceof LiteralBoolean) {
146157
return new ValDerivationNode(res, new BinaryDerivationNode(leftNode, rightNode, op));
147158
}
148159

160+
else if (left instanceof Enum leftEnum && right instanceof Enum rightEnum
161+
&& leftEnum.getTypeName().equals(rightEnum.getTypeName())) {
162+
boolean equal = leftEnum.getConstName().equals(rightEnum.getConstName());
163+
Expression res = switch (op) {
164+
case "==" -> new LiteralBoolean(equal);
165+
case "!=" -> new LiteralBoolean(!equal);
166+
default -> null;
167+
};
168+
if (res != null)
169+
return new ValDerivationNode(res, new BinaryDerivationNode(leftNode, rightNode, op));
170+
}
171+
149172
ValDerivationNode adjacentConstants = foldAdjacentIntegerConstants(leftNode, rightNode, op);
150173
if (adjacentConstants != null)
151174
return adjacentConstants;

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

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

33
import liquidjava.rj_language.ast.BinaryExpression;
4+
import liquidjava.rj_language.ast.Enum;
45
import liquidjava.rj_language.ast.Expression;
6+
import liquidjava.rj_language.ast.FunctionInvocation;
57
import liquidjava.rj_language.ast.UnaryExpression;
68
import liquidjava.rj_language.ast.Var;
79
import liquidjava.rj_language.opt.derivation_node.BinaryDerivationNode;
@@ -23,11 +25,11 @@ public class VariablePropagation {
2325
*/
2426
public static ValDerivationNode propagate(Expression exp, ValDerivationNode previousOrigin) {
2527
Map<String, Expression> substitutions = VariableResolver.resolve(exp);
26-
Map<String, Expression> directSubstitutions = new HashMap<>(); // var == literal or var == var
28+
Map<String, Expression> directSubstitutions = new HashMap<>(); // var == literal or var == var
2729
Map<String, Expression> expressionSubstitutions = new HashMap<>(); // var == expression
2830
for (Map.Entry<String, Expression> entry : substitutions.entrySet()) {
2931
Expression value = entry.getValue();
30-
if (value.isLiteral() || value instanceof Var) {
32+
if (value.isLiteral() || value instanceof Var || value instanceof Enum) {
3133
directSubstitutions.put(entry.getKey(), value);
3234
} else {
3335
expressionSubstitutions.put(entry.getKey(), value);
@@ -69,6 +71,12 @@ private static ValDerivationNode propagateRecursive(Expression exp, Map<String,
6971
return new ValDerivationNode(var, null);
7072
}
7173

74+
if (exp instanceof FunctionInvocation) {
75+
Expression value = subs.get(exp.toString());
76+
if (value != null)
77+
return new ValDerivationNode(value.clone(), new VarDerivationNode(exp.toString()));
78+
}
79+
7280
// lift unary origin
7381
if (exp instanceof UnaryExpression unary) {
7482
ValDerivationNode operand = propagateRecursive(unary.getChildren().get(0), subs, varOrigins);

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

Lines changed: 76 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,9 @@
66
import java.util.Set;
77

88
import liquidjava.rj_language.ast.BinaryExpression;
9+
import liquidjava.rj_language.ast.Enum;
910
import liquidjava.rj_language.ast.Expression;
11+
import liquidjava.rj_language.ast.FunctionInvocation;
1012
import liquidjava.rj_language.ast.Var;
1113

1214
public class VariableResolver {
@@ -25,7 +27,7 @@ public static Map<String, Expression> resolve(Expression exp) {
2527
resolveRecursive(exp, map);
2628

2729
// remove variables that were not used in the expression
28-
map.entrySet().removeIf(entry -> !hasUsage(exp, entry.getKey()));
30+
map.entrySet().removeIf(entry -> !hasUsage(exp, entry.getKey(), entry.getValue()));
2931

3032
// transitively resolve variables
3133
return resolveTransitive(map);
@@ -45,33 +47,49 @@ private static void resolveRecursive(Expression exp, Map<String, Expression> map
4547
if ("&&".equals(op)) {
4648
resolveRecursive(be.getFirstOperand(), map);
4749
resolveRecursive(be.getSecondOperand(), map);
48-
} else if ("==".equals(op)) {
49-
Expression left = be.getFirstOperand();
50-
Expression right = be.getSecondOperand();
51-
if (left instanceof Var var && right.isLiteral()) {
52-
map.put(var.getName(), right.clone());
53-
} else if (right instanceof Var var && left.isLiteral()) {
54-
map.put(var.getName(), left.clone());
55-
} else if (left instanceof Var leftVar && right instanceof Var rightVar) {
56-
// to substitute internal variable with user-facing variable
57-
if (isInternal(leftVar) && !isInternal(rightVar) && !isReturnVar(leftVar)) {
58-
map.put(leftVar.getName(), right.clone());
59-
} else if (isInternal(rightVar) && !isInternal(leftVar) && !isReturnVar(rightVar)) {
60-
map.put(rightVar.getName(), left.clone());
61-
} else if (isInternal(leftVar) && isInternal(rightVar)) {
62-
// to substitute the lower-counter variable with the higher-counter one
63-
boolean isLeftCounterLower = getCounter(leftVar) <= getCounter(rightVar);
64-
Var lowerVar = isLeftCounterLower ? leftVar : rightVar;
65-
Var higherVar = isLeftCounterLower ? rightVar : leftVar;
66-
if (!isReturnVar(lowerVar) && !isFreshVar(higherVar))
67-
map.putIfAbsent(lowerVar.getName(), higherVar.clone());
68-
}
69-
} else if (left instanceof Var var && !(right instanceof Var) && canSubstitute(var, right)) {
70-
map.put(var.getName(), right.clone());
50+
return;
51+
}
52+
if (!"==".equals(op))
53+
return;
54+
55+
Expression left = be.getFirstOperand();
56+
Expression right = be.getSecondOperand();
57+
String leftKey = substitutionKey(left);
58+
String rightKey = substitutionKey(right);
59+
60+
if (leftKey != null && isConstant(right)) {
61+
map.put(leftKey, right.clone());
62+
} else if (rightKey != null && isConstant(left)) {
63+
map.put(rightKey, left.clone());
64+
} else if (left instanceof Var leftVar && right instanceof Var rightVar) {
65+
// to substitute internal variable with user-facing variable
66+
if (isInternal(leftVar) && !isInternal(rightVar) && !isReturnVar(leftVar)) {
67+
map.put(leftVar.getName(), right.clone());
68+
} else if (isInternal(rightVar) && !isInternal(leftVar) && !isReturnVar(rightVar)) {
69+
map.put(rightVar.getName(), left.clone());
70+
} else if (isInternal(leftVar) && isInternal(rightVar)) {
71+
// to substitute the lower-counter variable with the higher-counter one
72+
boolean isLeftCounterLower = getCounter(leftVar) <= getCounter(rightVar);
73+
Var lowerVar = isLeftCounterLower ? leftVar : rightVar;
74+
Var higherVar = isLeftCounterLower ? rightVar : leftVar;
75+
if (!isReturnVar(lowerVar) && !isFreshVar(higherVar))
76+
map.putIfAbsent(lowerVar.getName(), higherVar.clone());
7177
}
78+
} else if (left instanceof Var var && canSubstitute(var, right)) {
79+
map.put(var.getName(), right.clone());
80+
} else if (left instanceof FunctionInvocation && !containsExpression(right, left)) {
81+
map.put(leftKey, right.clone());
7282
}
7383
}
7484

85+
private static String substitutionKey(Expression exp) {
86+
if (exp instanceof Var var)
87+
return var.getName();
88+
if (exp instanceof FunctionInvocation)
89+
return exp.toString();
90+
return null;
91+
}
92+
7593
/**
7694
* Handles transitive variable equalities in the map (e.g. map: x -> y, y -> 1 => map: x -> 1, y -> 1)
7795
*
@@ -98,10 +116,10 @@ private static Map<String, Expression> resolveTransitive(Map<String, Expression>
98116
* @return resolved expression
99117
*/
100118
private static Expression lookup(Expression exp, Map<String, Expression> map, Set<String> seen) {
101-
if (!(exp instanceof Var))
119+
String name = substitutionKey(exp);
120+
if (name == null)
102121
return exp;
103122

104-
String name = exp.toString();
105123
if (seen.contains(name))
106124
return exp; // circular reference
107125

@@ -121,27 +139,36 @@ private static Expression lookup(Expression exp, Map<String, Expression> map, Se
121139
*
122140
* @return true if used, false otherwise
123141
*/
124-
private static boolean hasUsage(Expression exp, String name) {
142+
private static boolean hasUsage(Expression exp, String name, Expression value) {
125143
// exclude own definitions
126144
if (exp instanceof BinaryExpression binary && "==".equals(binary.getOperator())) {
127145
Expression left = binary.getFirstOperand();
128146
Expression right = binary.getSecondOperand();
129-
if (left instanceof Var v && v.getName().equals(name)
130-
&& (right.isLiteral() || (!(right instanceof Var) && canSubstitute(v, right))))
147+
if (left instanceof Var v && v.getName().equals(name) && right.equals(value)
148+
&& (isConstant(right) || (!(right instanceof Var) && canSubstitute(v, right))))
149+
return false;
150+
if (left instanceof FunctionInvocation && left.toString().equals(name) && right.equals(value)
151+
&& (isConstant(right) || (!(right instanceof Var) && !containsExpression(right, left))))
152+
return false;
153+
if (right instanceof Var v && v.getName().equals(name) && left.equals(value) && isConstant(left))
131154
return false;
132-
if (right instanceof Var v && v.getName().equals(name) && left.isLiteral())
155+
if (right instanceof FunctionInvocation && right.toString().equals(name) && left.equals(value)
156+
&& isConstant(left))
133157
return false;
134158
}
135159

136160
// usage found
137161
if (exp instanceof Var var && var.getName().equals(name)) {
138162
return true;
139163
}
164+
if (exp instanceof FunctionInvocation && exp.toString().equals(name)) {
165+
return true;
166+
}
140167

141168
// recurse children
142169
if (exp.hasChildren()) {
143170
for (Expression child : exp.getChildren())
144-
if (hasUsage(child, name))
171+
if (hasUsage(child, name, value))
145172
return true;
146173
}
147174

@@ -172,6 +199,10 @@ private static boolean canSubstitute(Var var, Expression value) {
172199
return !isReturnVar(var) && !isFreshVar(var) && !containsVariable(value, var.getName());
173200
}
174201

202+
private static boolean isConstant(Expression exp) {
203+
return exp.isLiteral() || exp instanceof Enum;
204+
}
205+
175206
private static boolean containsVariable(Expression exp, String name) {
176207
if (exp instanceof Var var)
177208
return var.getName().equals(name);
@@ -185,4 +216,18 @@ private static boolean containsVariable(Expression exp, String name) {
185216
}
186217
return false;
187218
}
219+
220+
private static boolean containsExpression(Expression exp, Expression target) {
221+
if (exp.equals(target))
222+
return true;
223+
224+
if (!exp.hasChildren())
225+
return false;
226+
227+
for (Expression child : exp.getChildren()) {
228+
if (containsExpression(child, target))
229+
return true;
230+
}
231+
return false;
232+
}
188233
}

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RJErrorListener.java‎

Lines changed: 28 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -8,13 +8,15 @@
88
import org.antlr.v4.runtime.Parser;
99
import org.antlr.v4.runtime.RecognitionException;
1010
import org.antlr.v4.runtime.Recognizer;
11+
import org.antlr.v4.runtime.Token;
1112
import org.antlr.v4.runtime.atn.ATNConfigSet;
1213
import org.antlr.v4.runtime.dfa.DFA;
1314

1415
public class RJErrorListener implements ANTLRErrorListener {
1516

1617
private int errors;
1718
public List<String> msgs;
19+
private String hint;
1820

1921
public RJErrorListener() {
2022
super();
@@ -25,16 +27,30 @@ public RJErrorListener() {
2527
@Override
2628
public void syntaxError(Recognizer<?, ?> recognizer, Object offendingSymbol, int line, int charPositionInLine,
2729
String msg, RecognitionException e) {
28-
// Hint for == instead of =
29-
String hint = null;
30-
if (e instanceof LexerNoViableAltException l) {
31-
char c = l.getInputStream().toString().charAt(charPositionInLine);
32-
if (c == '=')
33-
hint = "Predicates must be compared with == instead of =";
30+
if (hint == null) {
31+
String input = inputFor(offendingSymbol, e);
32+
int pos = charPositionInLine;
33+
if (input != null && pos >= 0 && pos < input.length()) {
34+
char c = input.charAt(pos);
35+
// Hint for == instead of =
36+
if (c == '=')
37+
hint = "Predicates must be compared with == instead of =";
38+
// Hint for -> instead of --> (logical implication)
39+
else if (c == '>' && pos >= 1 && input.charAt(pos - 1) == '-'
40+
&& (pos < 2 || input.charAt(pos - 2) != '-'))
41+
hint = "Logical implication is --> (two dashes), not ->";
42+
}
3443
}
3544
errors++;
36-
String ms = "Error in " + msg + ", in the position " + charPositionInLine;
37-
msgs.add(ms + (hint == null ? "" : "\n\tHint: " + hint));
45+
msgs.add("Error in " + msg + ", in the position " + charPositionInLine);
46+
}
47+
48+
private static String inputFor(Object offendingSymbol, RecognitionException e) {
49+
if (e instanceof LexerNoViableAltException l)
50+
return l.getInputStream().toString();
51+
if (offendingSymbol instanceof Token t && t.getInputStream() != null)
52+
return t.getInputStream().toString();
53+
return null;
3854
}
3955

4056
@Override
@@ -56,6 +72,10 @@ public int getErrors() {
5672
return errors;
5773
}
5874

75+
public String getHint() {
76+
return hint;
77+
}
78+
5979
public String getMessages() {
6080
StringBuilder sb = new StringBuilder();
6181
String pl = errors == 1 ? "" : "s";

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java‎

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

3-
import java.util.Optional;
4-
53
import liquidjava.diagnostics.errors.SyntaxError;
64
import liquidjava.processor.facade.AliasDTO;
75
import liquidjava.processor.facade.GhostDTO;
@@ -56,25 +54,14 @@ public static AliasDTO parseAliasDefinition(String toParse) throws SyntaxError {
5654
* Compiles the given string into a parse tree
5755
*/
5856
private static ParseTree compile(String toParse, String errorMessage) throws SyntaxError {
59-
Optional<String> s = getErrors(toParse);
60-
if (s.isPresent())
61-
throw new SyntaxError(errorMessage, toParse);
62-
63-
RJErrorListener err = new RJErrorListener();
64-
RJParser parser = createParser(toParse, err);
65-
return parser.prog();
66-
}
67-
68-
/**
69-
* Checks if the given string can be parsed without syntax errors, returning the error messages if any
70-
*/
71-
private static Optional<String> getErrors(String toParse) {
7257
RJErrorListener err = new RJErrorListener();
73-
RJParser parser = createParser(toParse, err);
74-
parser.prog(); // all consumed
75-
if (err.getErrors() > 0)
76-
return Optional.of(err.getMessages());
77-
return Optional.empty();
58+
ParseTree tree = createParser(toParse, err).prog();
59+
if (err.getErrors() > 0) {
60+
SyntaxError e = new SyntaxError(errorMessage, toParse);
61+
e.setHint(err.getHint());
62+
throw e;
63+
}
64+
return tree;
7865
}
7966

8067
/**

0 commit comments

Comments
 (0)