Skip to content

Commit 52b9225

Browse files
rcosta358rcosta358
committed
Simplify Expressions
1 parent 368df95 commit 52b9225

15 files changed

Lines changed: 743 additions & 3 deletions

‎liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ public static <T> void printError(CtElement var, String moreInfo, Predicate expe
4141
// all message
4242
sb.append(sbtitle.toString() + "\n\n");
4343
sb.append("Type expected:" + expectedType.toString() + "\n");
44-
sb.append("Refinement found:" + cSMT.toString() + "\n");
44+
sb.append("Refinement found:\n" + cSMT.simplify() + "\n");
4545
sb.append(printMap(map));
4646
sb.append("Location: " + var.getPosition() + "\n");
4747
sb.append("______________________________________________________\n");
@@ -181,7 +181,7 @@ public static void printCostumeError(CtElement element, String msg, ErrorEmitter
181181
sb.append(element + "\n\n");
182182
sb.append("Location: " + element.getPosition() + "\n");
183183
sb.append("______________________________________________________\n");
184-
184+
185185
errorl.addError(s, sb.toString(), element.getPosition(), 1);
186186
}
187187

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -119,7 +119,8 @@ private void createStateSet(CtNewArray<String> e, int set, CtElement element) {
119119
CtLiteral<String> s = (CtLiteral<String>) ce;
120120
String f = s.getValue();
121121
if (Character.isUpperCase(f.charAt(0))) {
122-
ErrorHandler.printCostumeError(s, "State name must start with lowercase in '" + f + "'", errorEmitter);
122+
ErrorHandler.printCostumeError(s, "State name must start with lowercase in '" + f + "'",
123+
errorEmitter);
123124
}
124125
}
125126
}

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,8 @@
2121
import liquidjava.rj_language.ast.LiteralReal;
2222
import liquidjava.rj_language.ast.UnaryExpression;
2323
import liquidjava.rj_language.ast.Var;
24+
import liquidjava.rj_language.opt.ExpressionSimplifier;
25+
import liquidjava.rj_language.opt.derivation_node.DerivationNode;
2426
import liquidjava.rj_language.parsing.ParsingException;
2527
import liquidjava.rj_language.parsing.RefinementsParser;
2628
import liquidjava.utils.Utils;
@@ -212,6 +214,12 @@ public Expression getExpression() {
212214
return exp;
213215
}
214216

217+
public Expression simplify() {
218+
List<Expression> steps = ExpressionSimplifier.simplify(exp.clone());
219+
steps.forEach(System.out::println);
220+
return steps.isEmpty() ? exp : steps.get(steps.size() - 1);
221+
}
222+
215223
public static Predicate createConjunction(Predicate c1, Predicate c2) {
216224
return new Predicate(new BinaryExpression(c1.getExpression(), Utils.AND, c2.getExpression()));
217225
}

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralInt.java‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,10 @@ public String toString() {
2525
return Integer.toString(value);
2626
}
2727

28+
public int getValue() {
29+
return value;
30+
}
31+
2832
@Override
2933
public void getVariableNames(List<String> toAdd) {
3034
// end leaf

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralReal.java‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,10 @@ public String toString() {
2525
return Double.toString(value);
2626
}
2727

28+
public double getValue() {
29+
return value;
30+
}
31+
2832
@Override
2933
public void getVariableNames(List<String> toAdd) {
3034
// end leaf

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

Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,76 @@
1+
package liquidjava.rj_language.opt;
2+
3+
import java.util.HashMap;
4+
import java.util.Map;
5+
6+
import liquidjava.rj_language.ast.BinaryExpression;
7+
import liquidjava.rj_language.ast.Expression;
8+
import liquidjava.rj_language.ast.LiteralBoolean;
9+
import liquidjava.rj_language.ast.LiteralInt;
10+
import liquidjava.rj_language.ast.LiteralReal;
11+
import liquidjava.rj_language.ast.Var;
12+
13+
public class AssertionExtractor {
14+
15+
public static Map<String, Expression> extract(Expression exp) {
16+
Map<String, Expression> assertions = new HashMap<>();
17+
18+
// only extract assertions if the expression contains conjunctions (&&)
19+
if (containsConjunction(exp)) {
20+
extractRecursive(exp, assertions);
21+
}
22+
return assertions;
23+
}
24+
25+
private static boolean containsConjunction(Expression exp) {
26+
if (exp instanceof BinaryExpression) {
27+
BinaryExpression binExp = (BinaryExpression) exp;
28+
if (binExp.getOperator().equals("&&")) {
29+
return true;
30+
}
31+
// recursively check children
32+
return containsConjunction(binExp.getFirstOperand()) || containsConjunction(binExp.getSecondOperand());
33+
}
34+
if (exp.hasChildren()) {
35+
for (Expression child : exp.getChildren()) {
36+
if (containsConjunction(child)) {
37+
return true;
38+
}
39+
}
40+
}
41+
return false;
42+
}
43+
44+
private static void extractRecursive(Expression exp, Map<String, Expression> assertions) {
45+
if (exp instanceof BinaryExpression) {
46+
BinaryExpression binExp = (BinaryExpression) exp;
47+
String operator = binExp.getOperator();
48+
49+
if (operator.equals("&&")) {
50+
// for conjunctions recursively extract from both sides
51+
extractRecursive(binExp.getFirstOperand(), assertions);
52+
extractRecursive(binExp.getSecondOperand(), assertions);
53+
} else if (operator.equals("==")) {
54+
// for assertions check if one side is a variable and the other is a literal
55+
Expression left = binExp.getFirstOperand();
56+
Expression right = binExp.getSecondOperand();
57+
58+
if (left instanceof Var && isLiteral(right)) {
59+
assertions.put(((Var) left).getName(), right);
60+
} else if (right instanceof Var && isLiteral(left)) {
61+
assertions.put(((Var) right).getName(), left);
62+
}
63+
}
64+
}
65+
// for other expressions, recurse into children
66+
else if (exp.hasChildren()) {
67+
for (Expression child : exp.getChildren()) {
68+
extractRecursive(child, assertions);
69+
}
70+
}
71+
}
72+
73+
private static boolean isLiteral(Expression exp) {
74+
return exp instanceof LiteralInt || exp instanceof LiteralReal || exp instanceof LiteralBoolean;
75+
}
76+
}

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

Lines changed: 170 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,170 @@
1+
package liquidjava.rj_language.opt;
2+
3+
import liquidjava.rj_language.ast.BinaryExpression;
4+
import liquidjava.rj_language.ast.Expression;
5+
import liquidjava.rj_language.ast.LiteralBoolean;
6+
import liquidjava.rj_language.ast.LiteralInt;
7+
import liquidjava.rj_language.ast.LiteralReal;
8+
import liquidjava.rj_language.ast.UnaryExpression;
9+
10+
public class ConstantFolding {
11+
12+
public static Expression fold(Expression exp) {
13+
// recursively simplify in all children
14+
if (exp.hasChildren()) {
15+
for (int i = 0; i < exp.getChildren().size(); i++) {
16+
Expression child = exp.getChildren().get(i);
17+
Expression propagatedChild = fold(child);
18+
exp.setChild(i, propagatedChild);
19+
}
20+
}
21+
22+
// try to fold the current expression
23+
if (exp instanceof BinaryExpression) {
24+
return foldBinaryExpression((BinaryExpression) exp);
25+
} else if (exp instanceof UnaryExpression) {
26+
return foldUnaryExpression((UnaryExpression) exp);
27+
}
28+
return exp;
29+
}
30+
31+
private static Expression foldBinaryExpression(BinaryExpression binExp) {
32+
Expression left = binExp.getFirstOperand();
33+
Expression right = binExp.getSecondOperand();
34+
String op = binExp.getOperator();
35+
36+
// arithmetic operations with integer literals
37+
if (left instanceof LiteralInt && right instanceof LiteralInt) {
38+
int l = ((LiteralInt) left).getValue();
39+
int r = ((LiteralInt) right).getValue();
40+
41+
switch (op) {
42+
case "+":
43+
return new LiteralInt(l + r);
44+
case "-":
45+
return new LiteralInt(l - r);
46+
case "*":
47+
return new LiteralInt(l * r);
48+
case "/":
49+
if (r != 0)
50+
return new LiteralInt(l / r);
51+
break;
52+
case "%":
53+
if (r != 0)
54+
return new LiteralInt(l % r);
55+
break;
56+
case "<":
57+
return new LiteralBoolean(l < r);
58+
case "<=":
59+
return new LiteralBoolean(l <= r);
60+
case ">":
61+
return new LiteralBoolean(l > r);
62+
case ">=":
63+
return new LiteralBoolean(l >= r);
64+
case "==":
65+
return new LiteralBoolean(l == r);
66+
case "!=":
67+
return new LiteralBoolean(l != r);
68+
}
69+
}
70+
71+
// arithmetic operations with real literals
72+
else if (left instanceof LiteralReal && right instanceof LiteralReal) {
73+
double l = ((LiteralReal) left).getValue();
74+
double r = ((LiteralReal) right).getValue();
75+
switch (op) {
76+
case "+":
77+
return new LiteralReal(l + r);
78+
case "-":
79+
return new LiteralReal(l - r);
80+
case "*":
81+
return new LiteralReal(l * r);
82+
case "/":
83+
if (r != 0.0)
84+
return new LiteralReal(l / r);
85+
break;
86+
case "%":
87+
if (r != 0.0)
88+
return new LiteralReal(l % r);
89+
break;
90+
case "<":
91+
return new LiteralBoolean(l < r);
92+
case "<=":
93+
return new LiteralBoolean(l <= r);
94+
case ">":
95+
return new LiteralBoolean(l > r);
96+
case ">=":
97+
return new LiteralBoolean(l >= r);
98+
case "==":
99+
return new LiteralBoolean(l == r);
100+
case "!=":
101+
return new LiteralBoolean(l != r);
102+
}
103+
}
104+
105+
// mixed integer and real operations
106+
else if ((left instanceof LiteralInt && right instanceof LiteralReal) || (left instanceof LiteralReal && right instanceof LiteralInt)) {
107+
double l = left instanceof LiteralInt ? ((LiteralInt) left).getValue() : ((LiteralReal) left).getValue();
108+
double r = right instanceof LiteralInt ? ((LiteralInt) right).getValue() : ((LiteralReal) right).getValue();
109+
switch (op) {
110+
case "+":
111+
return new LiteralReal(l + r);
112+
case "-":
113+
return new LiteralReal(l - r);
114+
case "*":
115+
return new LiteralReal(l * r);
116+
case "/":
117+
if (r != 0.0)
118+
return new LiteralReal(l / r);
119+
break;
120+
case "%":
121+
if (r != 0.0)
122+
return new LiteralReal(l % r);
123+
break;
124+
case "<":
125+
return new LiteralBoolean(l < r);
126+
case "<=":
127+
return new LiteralBoolean(l <= r);
128+
case ">":
129+
return new LiteralBoolean(l > r);
130+
case ">=":
131+
return new LiteralBoolean(l >= r);
132+
case "==":
133+
return new LiteralBoolean(l == r);
134+
case "!=":
135+
return new LiteralBoolean(l != r);
136+
}
137+
}
138+
139+
// boolean operations with boolean literals
140+
else if (left instanceof LiteralBoolean && right instanceof LiteralBoolean) {
141+
boolean l = ((LiteralBoolean) left).isBooleanTrue();
142+
boolean r = ((LiteralBoolean) right).isBooleanTrue();
143+
switch (op) {
144+
case "&&":
145+
return new LiteralBoolean(l && r);
146+
case "||":
147+
return new LiteralBoolean(l || r);
148+
case "-->": // implication: !a || b
149+
return new LiteralBoolean(!l || r);
150+
case "==":
151+
return new LiteralBoolean(l == r);
152+
case "!=":
153+
return new LiteralBoolean(l != r);
154+
}
155+
}
156+
// no folding, return original
157+
return binExp;
158+
}
159+
160+
private static Expression foldUnaryExpression(UnaryExpression unaryExp) {
161+
Expression operand = unaryExp.getChildren().get(0);
162+
String operator = unaryExp.getOp();
163+
if (operator.equals("!") && operand instanceof LiteralBoolean) {
164+
// !true -> false, !false -> true
165+
boolean value = ((LiteralBoolean) operand).isBooleanTrue();
166+
return new LiteralBoolean(!value);
167+
}
168+
return unaryExp;
169+
}
170+
}

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

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
package liquidjava.rj_language.opt;
2+
3+
import liquidjava.rj_language.ast.Expression;
4+
import liquidjava.rj_language.ast.Var;
5+
import java.util.Map;
6+
7+
public class ConstantPropagation {
8+
9+
public static Expression propagate(Expression exp) {
10+
Map<String, Expression> substitutions = AssertionExtractor.extract(exp);
11+
return propagateRecursive(exp, substitutions);
12+
}
13+
14+
private static Expression propagateRecursive(Expression exp, Map<String, Expression> substitutions) {
15+
// apply substitutions to children for other expression types
16+
if (exp.hasChildren()) {
17+
Expression result = exp.clone();
18+
for (int i = 0; i < result.getChildren().size(); i++) {
19+
Expression child = result.getChildren().get(i);
20+
Expression substitutedChild = propagateRecursive(child, substitutions);
21+
result.setChild(i, substitutedChild);
22+
}
23+
return result;
24+
}
25+
// if the expression is a variable, substitute if in map
26+
if (exp instanceof Var) {
27+
Var var = (Var) exp;
28+
String varName = var.getName();
29+
if (substitutions.containsKey(varName)) {
30+
return substitutions.get(varName).clone();
31+
}
32+
}
33+
return exp;
34+
}
35+
}

0 commit comments

Comments
 (0)