Simplify Expressions

liquidjava-verifier/pom.xml

@@ -188,6 +188,11 @@
 			<artifactId>antlr4-runtime</artifactId>
 			<version>4.7.1</version>
 		</dependency>
+		<dependency>
+			<groupId>com.google.code.gson</groupId>
+			<artifactId>gson</artifactId>
+			<version>2.10.1</version>
+		</dependency>
 
 	</dependencies>
 	<dependencyManagement>

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

@@ -26,7 +26,7 @@ public static <T> void printError(CtElement var, Predicate expectedType, Predica
     }
 
     public static <T> void printError(CtElement var, String moreInfo, Predicate expectedType, Predicate cSMT,
-            HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
+            HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
         String resumeMessage = "Type expected:" + expectedType.toString(); // + "; " +"Refinement found:" +
         // cSMT.toString();
 
@@ -41,16 +41,16 @@ public static <T> void printError(CtElement var, String moreInfo, Predicate expe
         // all message
         sb.append(sbtitle.toString() + "\n\n");
         sb.append("Type expected:" + expectedType.toString() + "\n");
-        sb.append("Refinement found:" + cSMT.toString() + "\n");
+        sb.append("Refinement found: " + cSMT.simplify().getValue() + "\n");
         sb.append(printMap(map));
         sb.append("Location: " + var.getPosition() + "\n");
         sb.append("______________________________________________________\n");
 
-        errorl.addError(resumeMessage, sb.toString(), var.getPosition(), 1, map);
+        ee.addError(resumeMessage, sb.toString(), var.getPosition(), 1, map);
     }
 
     public static void printStateMismatch(CtElement element, String method, VCImplication constraintForErrorMsg,
-            String states, HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
+            String states, HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
 
         String resumeMessage = "Failed to check state transitions. " + "Expected possible states:" + states; // + ";
         // Found
@@ -75,11 +75,11 @@ public static void printStateMismatch(CtElement element, String method, VCImplic
         sb.append("Location: " + element.getPosition() + "\n");
         sb.append("______________________________________________________\n");
 
-        errorl.addError(resumeMessage, sb.toString(), element.getPosition(), 1, map);
+        ee.addError(resumeMessage, sb.toString(), element.getPosition(), 1, map);
     }
 
     public static <T> void printErrorUnknownVariable(CtElement var, String et, String correctRefinement,
-            HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
+            HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
 
         String resumeMessage = "Encountered unknown variable";
 
@@ -94,11 +94,11 @@ public static <T> void printErrorUnknownVariable(CtElement var, String et, Strin
         sb.append("Location: " + var.getPosition() + "\n");
         sb.append("______________________________________________________\n");
 
-        errorl.addError(resumeMessage, sb.toString(), var.getPosition(), 2, map);
+        ee.addError(resumeMessage, sb.toString(), var.getPosition(), 2, map);
     }
 
     public static <T> void printNotFound(CtElement var, Predicate constraint, Predicate constraint2, String msg,
-            HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
+            HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
 
         StringBuilder sb = new StringBuilder();
         sb.append("______________________________________________________\n");
@@ -111,11 +111,11 @@ public static <T> void printNotFound(CtElement var, Predicate constraint, Predic
         sb.append("Location: " + var.getPosition() + "\n");
         sb.append("______________________________________________________\n");
 
-        errorl.addError(msg, sb.toString(), var.getPosition(), 2, map);
+        ee.addError(msg, sb.toString(), var.getPosition(), 2, map);
     }
 
     public static <T> void printErrorArgs(CtElement var, Predicate expectedType, String msg,
-            HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
+            HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
         StringBuilder sb = new StringBuilder();
         sb.append("______________________________________________________\n");
         String title = "Error in ghost invocation: " + msg + "\n";
@@ -125,11 +125,11 @@ public static <T> void printErrorArgs(CtElement var, Predicate expectedType, Str
         sb.append("Location: " + var.getPosition() + "\n");
         sb.append("______________________________________________________\n");
 
-        errorl.addError(title, sb.toString(), var.getPosition(), 2, map);
+        ee.addError(title, sb.toString(), var.getPosition(), 2, map);
     }
 
     public static void printErrorTypeMismatch(CtElement element, Predicate expectedType, String message,
-            HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
+            HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
         StringBuilder sb = new StringBuilder();
         sb.append("______________________________________________________\n");
         sb.append(message + "\n\n");
@@ -138,11 +138,11 @@ public static void printErrorTypeMismatch(CtElement element, Predicate expectedT
         sb.append("Location: " + element.getPosition() + "\n");
         sb.append("______________________________________________________\n");
 
-        errorl.addError(message, sb.toString(), element.getPosition(), 2, map);
+        ee.addError(message, sb.toString(), element.getPosition(), 2, map);
     }
 
     public static void printSameStateSetError(CtElement element, Predicate p, String name,
-            HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
+            HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
         String resume = "Error found multiple disjoint states from a State Set in a refinement";
 
         StringBuilder sb = new StringBuilder();
@@ -157,10 +157,10 @@ public static void printSameStateSetError(CtElement element, Predicate p, String
         sb.append("Location: " + element.getPosition() + "\n");
         sb.append("______________________________________________________\n");
 
-        errorl.addError(resume, sb.toString(), element.getPosition(), 1, map);
+        ee.addError(resume, sb.toString(), element.getPosition(), 1, map);
     }
 
-    public static void printErrorConstructorFromState(CtElement element, CtLiteral<String> from, ErrorEmitter errorl) {
+    public static void printErrorConstructorFromState(CtElement element, CtLiteral<String> from, ErrorEmitter ee) {
         StringBuilder sb = new StringBuilder();
         sb.append("______________________________________________________\n");
         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
         sb.append("Location: " + element.getPosition() + "\n");
         sb.append("______________________________________________________\n");
 
-        errorl.addError(s, sb.toString(), element.getPosition(), 1);
+        ee.addError(s, sb.toString(), element.getPosition(), 1);
     }
 
-    public static void printCostumeError(CtElement element, String msg, ErrorEmitter errorl) {
+    public static void printCustomError(CtElement element, String msg, ErrorEmitter ee) {
         StringBuilder sb = new StringBuilder();
         sb.append("______________________________________________________\n");
         String s = "Found Error: " + msg;
@@ -182,10 +182,10 @@ public static void printCostumeError(CtElement element, String msg, ErrorEmitter
         sb.append("Location: " + element.getPosition() + "\n");
         sb.append("______________________________________________________\n");
 
-        errorl.addError(s, sb.toString(), element.getPosition(), 1);
+        ee.addError(s, sb.toString(), element.getPosition(), 1);
     }
 
-    public static void printSyntaxError(String msg, String ref, CtElement element, ErrorEmitter errorl) {
+    public static void printSyntaxError(String msg, String ref, CtElement element, ErrorEmitter ee) {
         StringBuilder sb = new StringBuilder();
         sb.append("______________________________________________________\n");
         StringBuilder sbtitle = new StringBuilder();
@@ -199,10 +199,10 @@ public static void printSyntaxError(String msg, String ref, CtElement element, E
         sb.append("Location: " + element.getPosition() + "\n");
         sb.append("______________________________________________________\n");
 
-        errorl.addError(sbtitle.toString(), sb.toString(), element.getPosition(), 2);
+        ee.addError(sbtitle.toString(), sb.toString(), element.getPosition(), 2);
     }
 
-    public static void printSyntaxError(String msg, String ref, ErrorEmitter errorl) {
+    public static void printSyntaxError(String msg, String ref, ErrorEmitter ee) {
         StringBuilder sb = new StringBuilder();
         sb.append("______________________________________________________\n");
         StringBuilder sbtitle = new StringBuilder();
@@ -213,7 +213,7 @@ public static void printSyntaxError(String msg, String ref, ErrorEmitter errorl)
         sb.append(ref + "\n");
         sb.append("______________________________________________________\n");
 
-        errorl.addError(sbtitle.toString(), sb.toString(), 2);
+        ee.addError(sbtitle.toString(), sb.toString(), 2);
     }
 
     private static String printLine() {

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

@@ -95,8 +95,7 @@ protected void getGhostFunction(String value, CtElement element) {
             }
 
         } catch (ParsingException e) {
-            ErrorHandler.printCostumeError(element, "Could not parse the Ghost Function" + e.getMessage(),
-                    errorEmitter);
+            ErrorHandler.printCustomError(element, "Could not parse the Ghost Function" + e.getMessage(), errorEmitter);
             // e.printStackTrace();
         }
     }

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

@@ -119,7 +119,7 @@ private void createStateSet(CtNewArray<String> e, int set, CtElement element) {
                 CtLiteral<String> s = (CtLiteral<String>) ce;
                 String f = s.getValue();
                 if (Character.isUpperCase(f.charAt(0))) {
-                    ErrorHandler.printCostumeError(s, "State name must start with lowercase in '" + f + "'",
+                    ErrorHandler.printCustomError(s, "State name must start with lowercase in '" + f + "'",
                             errorEmitter);
                 }
             }
@@ -161,11 +161,11 @@ private void createStateGhost(String string, CtAnnotation<? extends Annotation>
         try {
             gd = RefinementsParser.getGhostDeclaration(string);
         } catch (ParsingException e) {
-            ErrorHandler.printCostumeError(ann, "Could not parse the Ghost Function" + e.getMessage(), errorEmitter);
+            ErrorHandler.printCustomError(ann, "Could not parse the Ghost Function" + e.getMessage(), errorEmitter);
             return;
         }
         if (gd.getParam_types().size() > 0) {
-            ErrorHandler.printCostumeError(ann, "Ghost States have the class as parameter "
+            ErrorHandler.printCustomError(ann, "Ghost States have the class as parameter "
                     + "by default, no other parameters are allowed in '" + string + "'", errorEmitter);
             return;
         }
@@ -224,8 +224,7 @@ protected void getGhostFunction(String value, CtElement element) {
                 context.addGhostFunction(gh);
             }
         } catch (ParsingException e) {
-            ErrorHandler.printCostumeError(element, "Could not parse the Ghost Function" + e.getMessage(),
-                    errorEmitter);
+            ErrorHandler.printCustomError(element, "Could not parse the Ghost Function" + e.getMessage(), errorEmitter);
             // e.printStackTrace();
             return;
         }
@@ -252,7 +251,7 @@ protected void handleAlias(String value, CtElement element) {
                 }
             }
         } catch (ParsingException e) {
-            ErrorHandler.printCostumeError(element, e.getMessage(), errorEmitter);
+            ErrorHandler.printCustomError(element, e.getMessage(), errorEmitter);
             return;
             // e.printStackTrace();
         }

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

@@ -364,7 +364,7 @@ private void printError(Exception e, Predicate premisesBeforeChange, Predicate e
         } else if (e instanceof NotFoundError) {
             ErrorHandler.printNotFound(element, cSMTMessageReady, etMessageReady, e.getMessage(), map, errorEmitter);
         } else {
-            ErrorHandler.printCostumeError(element, e.getMessage(), errorEmitter);
+            ErrorHandler.printCustomError(element, e.getMessage(), errorEmitter);
             // System.err.println("Unknown error:"+e.getMessage());
             // e.printStackTrace();
             // System.exit(7);

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

@@ -369,7 +369,7 @@ public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) {
             stateChange.setTo(toPredicate);
         } catch (ParsingException e) {
             ErrorHandler
-                    .printCostumeError(fw,
+                    .printCustomError(fw,
                             "ParsingException while constructing assignment update for `" + fw + "` in class `"
                                     + fw.getVariable().getDeclaringType() + "` : " + e.getMessage(),
                             tc.getErrorEmitter());

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

@@ -21,6 +21,9 @@
 import liquidjava.rj_language.ast.LiteralReal;
 import liquidjava.rj_language.ast.UnaryExpression;
 import liquidjava.rj_language.ast.Var;
+import liquidjava.rj_language.opt.derivation_node.DerivationNode;
+import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
+import liquidjava.rj_language.opt.ExpressionSimplifier;
 import liquidjava.rj_language.parsing.ParsingException;
 import liquidjava.rj_language.parsing.RefinementsParser;
 import liquidjava.utils.Utils;
@@ -212,6 +215,10 @@ public Expression getExpression() {
         return exp;
     }
 
+    public ValDerivationNode simplify() {
+        return ExpressionSimplifier.simplify(exp.clone());
+    }
+
     public static Predicate createConjunction(Predicate c1, Predicate c2) {
         return new Predicate(new BinaryExpression(c1.getExpression(), Utils.AND, c2.getExpression()));
     }

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

@@ -1,9 +1,11 @@
 package liquidjava.rj_language.ast;
 
-import com.microsoft.z3.Expr;
 import java.util.ArrayList;
 import java.util.List;
 import java.util.Map;
+
+import com.microsoft.z3.Expr;
+
 import liquidjava.processor.context.Context;
 import liquidjava.processor.facade.AliasDTO;
 import liquidjava.rj_language.ast.typing.TypeInfer;
@@ -47,6 +49,10 @@ public void setChild(int index, Expression element) {
         children.set(index, element);
     }
 
+    public boolean isLiteral() {
+        return this instanceof LiteralInt || this instanceof LiteralReal || this instanceof LiteralBoolean;
+    }
+
     /**
      * Substitutes the expression first given expression by the second
      *

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

@@ -25,6 +25,10 @@ public String toString() {
         return Integer.toString(value);
     }
 
+    public int getValue() {
+        return value;
+    }
+
     @Override
     public void getVariableNames(List<String> toAdd) {
         // end leaf

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

@@ -25,6 +25,10 @@ public String toString() {
         return Double.toString(value);
     }
 
+    public double getValue() {
+        return value;
+    }
+
     @Override
     public void getVariableNames(List<String> toAdd) {
         // end leaf