Skip to content

Commit d3c2dbb

Browse files
rcosta358rcosta358
authored
Simplify Expressions (#59)
1 parent 6018353 commit d3c2dbb

File tree

20 files changed

+955
-34
lines changed

20 files changed

+955
-34
lines changed

‎liquidjava-verifier/pom.xml‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -188,6 +188,11 @@
188188
<artifactId>antlr4-runtime</artifactId>
189189
<version>4.7.1</version>
190190
</dependency>
191+
<dependency>
192+
<groupId>com.google.code.gson</groupId>
193+
<artifactId>gson</artifactId>
194+
<version>2.10.1</version>
195+
</dependency>
191196

192197
</dependencies>
193198
<dependencyManagement>

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

Lines changed: 23 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ public static <T> void printError(CtElement var, Predicate expectedType, Predica
2626
}
2727

2828
public static <T> void printError(CtElement var, String moreInfo, Predicate expectedType, Predicate cSMT,
29-
HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
29+
HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
3030
String resumeMessage = "Type expected:" + expectedType.toString(); // + "; " +"Refinement found:" +
3131
// cSMT.toString();
3232

@@ -41,16 +41,16 @@ 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: " + cSMT.simplify().getValue() + "\n");
4545
sb.append(printMap(map));
4646
sb.append("Location: " + var.getPosition() + "\n");
4747
sb.append("______________________________________________________\n");
4848

49-
errorl.addError(resumeMessage, sb.toString(), var.getPosition(), 1, map);
49+
ee.addError(resumeMessage, sb.toString(), var.getPosition(), 1, map);
5050
}
5151

5252
public static void printStateMismatch(CtElement element, String method, VCImplication constraintForErrorMsg,
53-
String states, HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
53+
String states, HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
5454

5555
String resumeMessage = "Failed to check state transitions. " + "Expected possible states:" + states; // + ";
5656
// Found
@@ -75,11 +75,11 @@ public static void printStateMismatch(CtElement element, String method, VCImplic
7575
sb.append("Location: " + element.getPosition() + "\n");
7676
sb.append("______________________________________________________\n");
7777

78-
errorl.addError(resumeMessage, sb.toString(), element.getPosition(), 1, map);
78+
ee.addError(resumeMessage, sb.toString(), element.getPosition(), 1, map);
7979
}
8080

8181
public static <T> void printErrorUnknownVariable(CtElement var, String et, String correctRefinement,
82-
HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
82+
HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
8383

8484
String resumeMessage = "Encountered unknown variable";
8585

@@ -94,11 +94,11 @@ public static <T> void printErrorUnknownVariable(CtElement var, String et, Strin
9494
sb.append("Location: " + var.getPosition() + "\n");
9595
sb.append("______________________________________________________\n");
9696

97-
errorl.addError(resumeMessage, sb.toString(), var.getPosition(), 2, map);
97+
ee.addError(resumeMessage, sb.toString(), var.getPosition(), 2, map);
9898
}
9999

100100
public static <T> void printNotFound(CtElement var, Predicate constraint, Predicate constraint2, String msg,
101-
HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
101+
HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
102102

103103
StringBuilder sb = new StringBuilder();
104104
sb.append("______________________________________________________\n");
@@ -111,11 +111,11 @@ public static <T> void printNotFound(CtElement var, Predicate constraint, Predic
111111
sb.append("Location: " + var.getPosition() + "\n");
112112
sb.append("______________________________________________________\n");
113113

114-
errorl.addError(msg, sb.toString(), var.getPosition(), 2, map);
114+
ee.addError(msg, sb.toString(), var.getPosition(), 2, map);
115115
}
116116

117117
public static <T> void printErrorArgs(CtElement var, Predicate expectedType, String msg,
118-
HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
118+
HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
119119
StringBuilder sb = new StringBuilder();
120120
sb.append("______________________________________________________\n");
121121
String title = "Error in ghost invocation: " + msg + "\n";
@@ -125,11 +125,11 @@ public static <T> void printErrorArgs(CtElement var, Predicate expectedType, Str
125125
sb.append("Location: " + var.getPosition() + "\n");
126126
sb.append("______________________________________________________\n");
127127

128-
errorl.addError(title, sb.toString(), var.getPosition(), 2, map);
128+
ee.addError(title, sb.toString(), var.getPosition(), 2, map);
129129
}
130130

131131
public static void printErrorTypeMismatch(CtElement element, Predicate expectedType, String message,
132-
HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
132+
HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
133133
StringBuilder sb = new StringBuilder();
134134
sb.append("______________________________________________________\n");
135135
sb.append(message + "\n\n");
@@ -138,11 +138,11 @@ public static void printErrorTypeMismatch(CtElement element, Predicate expectedT
138138
sb.append("Location: " + element.getPosition() + "\n");
139139
sb.append("______________________________________________________\n");
140140

141-
errorl.addError(message, sb.toString(), element.getPosition(), 2, map);
141+
ee.addError(message, sb.toString(), element.getPosition(), 2, map);
142142
}
143143

144144
public static void printSameStateSetError(CtElement element, Predicate p, String name,
145-
HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
145+
HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
146146
String resume = "Error found multiple disjoint states from a State Set in a refinement";
147147

148148
StringBuilder sb = new StringBuilder();
@@ -157,10 +157,10 @@ public static void printSameStateSetError(CtElement element, Predicate p, String
157157
sb.append("Location: " + element.getPosition() + "\n");
158158
sb.append("______________________________________________________\n");
159159

160-
errorl.addError(resume, sb.toString(), element.getPosition(), 1, map);
160+
ee.addError(resume, sb.toString(), element.getPosition(), 1, map);
161161
}
162162

163-
public static void printErrorConstructorFromState(CtElement element, CtLiteral<String> from, ErrorEmitter errorl) {
163+
public static void printErrorConstructorFromState(CtElement element, CtLiteral<String> from, ErrorEmitter ee) {
164164
StringBuilder sb = new StringBuilder();
165165
sb.append("______________________________________________________\n");
166166
String s = " Error found constructor with FROM state (Constructor's should only have a TO state)\n\n";
@@ -170,10 +170,10 @@ public static void printErrorConstructorFromState(CtElement element, CtLiteral<S
170170
sb.append("Location: " + element.getPosition() + "\n");
171171
sb.append("______________________________________________________\n");
172172

173-
errorl.addError(s, sb.toString(), element.getPosition(), 1);
173+
ee.addError(s, sb.toString(), element.getPosition(), 1);
174174
}
175175

176-
public static void printCostumeError(CtElement element, String msg, ErrorEmitter errorl) {
176+
public static void printCustomError(CtElement element, String msg, ErrorEmitter ee) {
177177
StringBuilder sb = new StringBuilder();
178178
sb.append("______________________________________________________\n");
179179
String s = "Found Error: " + msg;
@@ -182,10 +182,10 @@ public static void printCostumeError(CtElement element, String msg, ErrorEmitter
182182
sb.append("Location: " + element.getPosition() + "\n");
183183
sb.append("______________________________________________________\n");
184184

185-
errorl.addError(s, sb.toString(), element.getPosition(), 1);
185+
ee.addError(s, sb.toString(), element.getPosition(), 1);
186186
}
187187

188-
public static void printSyntaxError(String msg, String ref, CtElement element, ErrorEmitter errorl) {
188+
public static void printSyntaxError(String msg, String ref, CtElement element, ErrorEmitter ee) {
189189
StringBuilder sb = new StringBuilder();
190190
sb.append("______________________________________________________\n");
191191
StringBuilder sbtitle = new StringBuilder();
@@ -199,10 +199,10 @@ public static void printSyntaxError(String msg, String ref, CtElement element, E
199199
sb.append("Location: " + element.getPosition() + "\n");
200200
sb.append("______________________________________________________\n");
201201

202-
errorl.addError(sbtitle.toString(), sb.toString(), element.getPosition(), 2);
202+
ee.addError(sbtitle.toString(), sb.toString(), element.getPosition(), 2);
203203
}
204204

205-
public static void printSyntaxError(String msg, String ref, ErrorEmitter errorl) {
205+
public static void printSyntaxError(String msg, String ref, ErrorEmitter ee) {
206206
StringBuilder sb = new StringBuilder();
207207
sb.append("______________________________________________________\n");
208208
StringBuilder sbtitle = new StringBuilder();
@@ -213,7 +213,7 @@ public static void printSyntaxError(String msg, String ref, ErrorEmitter errorl)
213213
sb.append(ref + "\n");
214214
sb.append("______________________________________________________\n");
215215

216-
errorl.addError(sbtitle.toString(), sb.toString(), 2);
216+
ee.addError(sbtitle.toString(), sb.toString(), 2);
217217
}
218218

219219
private static String printLine() {

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

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -95,8 +95,7 @@ protected void getGhostFunction(String value, CtElement element) {
9595
}
9696

9797
} catch (ParsingException e) {
98-
ErrorHandler.printCostumeError(element, "Could not parse the Ghost Function" + e.getMessage(),
99-
errorEmitter);
98+
ErrorHandler.printCustomError(element, "Could not parse the Ghost Function" + e.getMessage(), errorEmitter);
10099
// e.printStackTrace();
101100
}
102101
}

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

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -119,7 +119,7 @@ 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 + "'",
122+
ErrorHandler.printCustomError(s, "State name must start with lowercase in '" + f + "'",
123123
errorEmitter);
124124
}
125125
}
@@ -161,11 +161,11 @@ private void createStateGhost(String string, CtAnnotation<? extends Annotation>
161161
try {
162162
gd = RefinementsParser.getGhostDeclaration(string);
163163
} catch (ParsingException e) {
164-
ErrorHandler.printCostumeError(ann, "Could not parse the Ghost Function" + e.getMessage(), errorEmitter);
164+
ErrorHandler.printCustomError(ann, "Could not parse the Ghost Function" + e.getMessage(), errorEmitter);
165165
return;
166166
}
167167
if (gd.getParam_types().size() > 0) {
168-
ErrorHandler.printCostumeError(ann, "Ghost States have the class as parameter "
168+
ErrorHandler.printCustomError(ann, "Ghost States have the class as parameter "
169169
+ "by default, no other parameters are allowed in '" + string + "'", errorEmitter);
170170
return;
171171
}
@@ -224,8 +224,7 @@ protected void getGhostFunction(String value, CtElement element) {
224224
context.addGhostFunction(gh);
225225
}
226226
} catch (ParsingException e) {
227-
ErrorHandler.printCostumeError(element, "Could not parse the Ghost Function" + e.getMessage(),
228-
errorEmitter);
227+
ErrorHandler.printCustomError(element, "Could not parse the Ghost Function" + e.getMessage(), errorEmitter);
229228
// e.printStackTrace();
230229
return;
231230
}
@@ -252,7 +251,7 @@ protected void handleAlias(String value, CtElement element) {
252251
}
253252
}
254253
} catch (ParsingException e) {
255-
ErrorHandler.printCostumeError(element, e.getMessage(), errorEmitter);
254+
ErrorHandler.printCustomError(element, e.getMessage(), errorEmitter);
256255
return;
257256
// e.printStackTrace();
258257
}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -364,7 +364,7 @@ private void printError(Exception e, Predicate premisesBeforeChange, Predicate e
364364
} else if (e instanceof NotFoundError) {
365365
ErrorHandler.printNotFound(element, cSMTMessageReady, etMessageReady, e.getMessage(), map, errorEmitter);
366366
} else {
367-
ErrorHandler.printCostumeError(element, e.getMessage(), errorEmitter);
367+
ErrorHandler.printCustomError(element, e.getMessage(), errorEmitter);
368368
// System.err.println("Unknown error:"+e.getMessage());
369369
// e.printStackTrace();
370370
// System.exit(7);

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -369,7 +369,7 @@ public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) {
369369
stateChange.setTo(toPredicate);
370370
} catch (ParsingException e) {
371371
ErrorHandler
372-
.printCostumeError(fw,
372+
.printCustomError(fw,
373373
"ParsingException while constructing assignment update for `" + fw + "` in class `"
374374
+ fw.getVariable().getDeclaringType() + "` : " + e.getMessage(),
375375
tc.getErrorEmitter());

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

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,9 @@
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.derivation_node.DerivationNode;
25+
import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
26+
import liquidjava.rj_language.opt.ExpressionSimplifier;
2427
import liquidjava.rj_language.parsing.ParsingException;
2528
import liquidjava.rj_language.parsing.RefinementsParser;
2629
import liquidjava.utils.Utils;
@@ -212,6 +215,10 @@ public Expression getExpression() {
212215
return exp;
213216
}
214217

218+
public ValDerivationNode simplify() {
219+
return ExpressionSimplifier.simplify(exp.clone());
220+
}
221+
215222
public static Predicate createConjunction(Predicate c1, Predicate c2) {
216223
return new Predicate(new BinaryExpression(c1.getExpression(), Utils.AND, c2.getExpression()));
217224
}

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

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

3-
import com.microsoft.z3.Expr;
43
import java.util.ArrayList;
54
import java.util.List;
65
import java.util.Map;
6+
7+
import com.microsoft.z3.Expr;
8+
79
import liquidjava.processor.context.Context;
810
import liquidjava.processor.facade.AliasDTO;
911
import liquidjava.rj_language.ast.typing.TypeInfer;
@@ -47,6 +49,10 @@ public void setChild(int index, Expression element) {
4749
children.set(index, element);
4850
}
4951

52+
public boolean isLiteral() {
53+
return this instanceof LiteralInt || this instanceof LiteralReal || this instanceof LiteralBoolean;
54+
}
55+
5056
/**
5157
* Substitutes the expression first given expression by the second
5258
*

‎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

0 commit comments

Comments
 (0)