Simplify Boolean Expressions By Removing Redundant Literals

Remove boolean literals from expressions like (true && x) and (false || x)

Author: rcosta358

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

@@ -27,21 +27,21 @@ 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) {
-        String resumeMessage = "Type expected:" + expectedType.toString(); // + "; " +"Refinement found:" +
+        String resumeMessage = "Type expected: " + expectedType.toString(); // + "; " +"Refinement found:" +
         // cSMT.toString();
 
         StringBuilder sb = new StringBuilder();
         sb.append("______________________________________________________\n");
         // title
         StringBuilder sbtitle = new StringBuilder();
-        sbtitle.append("Failed to check refinement at: \n\n");
+        sbtitle.append("Failed to check refinement at:\n\n");
         if (moreInfo != null)
             sbtitle.append(moreInfo + "\n");
         sbtitle.append(var.toString());
         // all message
         sb.append(sbtitle.toString() + "\n\n");
-        sb.append("Type expected:" + expectedType.toString() + "\n");
-        sb.append("Refinement found:" + cSMT.toString() + "\n");
+        sb.append("Type expected: " + expectedType.toString() + "\n");
+        sb.append("Refinement found: " + cSMT.toString() + "\n");
         sb.append(printMap(map));
         sb.append("Location: " + var.getPosition() + "\n");
         sb.append("______________________________________________________\n");
@@ -65,7 +65,7 @@ public static void printStateMismatch(CtElement element, String method, VCImplic
         sbtitle.append(element + "\n\n");
 
         sb.append(sbtitle.toString());
-        sb.append("Expected possible states:" + states + "\n");
+        sb.append("Expected possible states: " + states + "\n");
         sb.append("\nState found:\n");
         sb.append(printLine());
         sb.append("\n" + constraintForErrorMsg /* .toConjunctions() */.toString() + "\n");
@@ -120,7 +120,7 @@ public static <T> void printErrorArgs(CtElement var, Predicate expectedType, Str
         sb.append("______________________________________________________\n");
         String title = "Error in ghost invocation: " + msg + "\n";
         sb.append(title);
-        sb.append(var + "\nError in refinement:" + expectedType.toString() + "\n");
+        sb.append(var + "\nError in refinement: " + expectedType.toString() + "\n");
         sb.append(printMap(map));
         sb.append("Location: " + var.getPosition() + "\n");
         sb.append("______________________________________________________\n");
@@ -151,8 +151,8 @@ public static void printSameStateSetError(CtElement element, Predicate p, String
         sbtitle.append("Error found multiple disjoint states from a State Set in a refinement\n\n");
         sbtitle.append(element + "\n\n");
         sb.append(sbtitle.toString());
-        sb.append("In predicate:" + p.toString() + "\n");
-        sb.append("In class:" + name + "\n");
+        sb.append("In predicate: " + p.toString() + "\n");
+        sb.append("In class: " + name + "\n");
         sb.append(printMap(map));
         sb.append("Location: " + element.getPosition() + "\n");
         sb.append("______________________________________________________\n");
@@ -163,10 +163,10 @@ public static void printSameStateSetError(CtElement element, Predicate p, String
     public static void printErrorConstructorFromState(CtElement element, CtLiteral<String> from, ErrorEmitter errorl) {
         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";
+        String s = "Error found constructor with 'from' state (Constructors must only have a 'to' state)\n\n";
         sb.append(s);
         sb.append(element + "\n\n");
-        sb.append("State found:" + from + "\n");
+        sb.append("State found: " + from + "\n");
         sb.append("Location: " + element.getPosition() + "\n");
         sb.append("______________________________________________________\n");
 

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

@@ -13,6 +13,7 @@
 import liquidjava.processor.facade.AliasDTO;
 import liquidjava.rj_language.ast.BinaryExpression;
 import liquidjava.rj_language.ast.Expression;
+import liquidjava.rj_language.ast.LiteralBoolean;
 import liquidjava.rj_language.ast.FunctionInvocation;
 import liquidjava.rj_language.ast.GroupExpression;
 import liquidjava.rj_language.ast.Ite;
@@ -189,11 +190,25 @@ public Expression getExpression() {
         return exp;
     }
 
+    private static boolean isBooleanLiteral(Expression expr, boolean value) {
+        return expr instanceof LiteralBoolean && ((LiteralBoolean) expr).isBooleanTrue() == value;
+    }
+
     public static Predicate createConjunction(Predicate c1, Predicate c2) {
+        // simplification: (true && x) = x, (false && x) = false
+        if (isBooleanLiteral(c1.getExpression(), true)) return c2;
+        if (isBooleanLiteral(c2.getExpression(), true)) return c1;
+        if (isBooleanLiteral(c1.getExpression(), false)) return c1;
+        if (isBooleanLiteral(c2.getExpression(), false)) return c2;
         return new Predicate(new BinaryExpression(c1.getExpression(), Utils.AND, c2.getExpression()));
     }
 
     public static Predicate createDisjunction(Predicate c1, Predicate c2) {
+        // simplification: (false || x) = x, (true || x) = true
+        if (isBooleanLiteral(c1.getExpression(), false)) return c2;
+        if (isBooleanLiteral(c2.getExpression(), false)) return c1;
+        if (isBooleanLiteral(c1.getExpression(), true)) return c1;
+        if (isBooleanLiteral(c2.getExpression(), true)) return c2;
         return new Predicate(new BinaryExpression(c1.getExpression(), Utils.OR, c2.getExpression()));
     }