Add Documentation to Methods

Author: rcosta358

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

@@ -14,14 +14,18 @@
 
 public class ConstantFolding {
 
+    /**
+     * Performs constant folding on a derivation node by evaluating nodes with constant values. Returns a new derivation
+     * node representing the folding steps taken
+     */
     public static ValDerivationNode fold(ValDerivationNode node) {
         Expression exp = node.getValue();
-        if (exp instanceof BinaryExpression) {
+        if (exp instanceof BinaryExpression)
             return foldBinary(node);
-        }
-        if (exp instanceof UnaryExpression) {
+
+        if (exp instanceof UnaryExpression)
             return foldUnary(node);
-        }
+
         if (exp instanceof GroupExpression) {
             GroupExpression group = (GroupExpression) exp;
             if (group.getChildren().size() == 1) {
@@ -31,6 +35,9 @@ public static ValDerivationNode fold(ValDerivationNode node) {
         return node;
     }
 
+    /**
+     * Folds a binary expression node if both children are constant values (e.g. 1 + 2 => 3)
+     */
     private static ValDerivationNode foldBinary(ValDerivationNode node) {
         BinaryExpression binExp = (BinaryExpression) node.getValue();
         DerivationNode parent = node.getOrigin();
@@ -142,6 +149,9 @@ else if (left instanceof LiteralBoolean && right instanceof LiteralBoolean) {
         return new ValDerivationNode(binExp, origin);
     }
 
+    /**
+     * Folds a unary expression node if the child (operand) is a constant value (e.g. !true => false)
+     */
     private static ValDerivationNode foldUnary(ValDerivationNode node) {
         UnaryExpression unaryExp = (UnaryExpression) node.getValue();
         DerivationNode parent = node.getOrigin();

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

@@ -14,11 +14,19 @@
 
 public class ConstantPropagation {
 
+    /**
+     * Performs constant propagation on an expression, by substituting variables with their constant values. Uses the
+     * VariableResolver to extract variable equalities from the expression first. Returns a derivation node representing
+     * the propagation steps taken.
+     */
     public static ValDerivationNode propagate(Expression exp) {
         Map<String, Expression> substitutions = VariableResolver.resolve(exp);
         return propagateRecursive(exp, substitutions);
     }
 
+    /**
+     * Recursively performs constant propagation on an expression (e.g. x + y && x == 1 && y == 2 => 1 + 2)
+     */
     private static ValDerivationNode propagateRecursive(Expression exp, Map<String, Expression> subs) {
 
         // substitute variable

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java

@@ -9,14 +9,18 @@
 
 public class ExpressionSimplifier {
 
+    /**
+     * Simplifies an expression by applying constant propagation, constant folding and removing redundant conjuncts
+     * Returns a derivation node representing the tree of simplifications applied
+     */
     public static ValDerivationNode simplify(Expression exp) {
         ValDerivationNode prop = ConstantPropagation.propagate(exp);
         ValDerivationNode fold = ConstantFolding.fold(prop);
         return simplifyDerivationTree(fold);
     }
 
     /**
-     * Recursively simplify the derivation tree by removing redundant conjuncts
+     * Recursively simplifies the derivation tree by removing redundant conjuncts
      */
     private static ValDerivationNode simplifyDerivationTree(ValDerivationNode node) {
         Expression value = node.getValue();
@@ -49,7 +53,7 @@ private static ValDerivationNode simplifyDerivationTree(ValDerivationNode node)
     }
 
     /**
-     * Check if an expression is redundant
+     * Checks if an expression is redundant (e.g. true or x == x)
      */
     private static boolean isRedundant(Expression exp) {
         // true

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

@@ -11,12 +11,19 @@
 
 public class VariableResolver {
 
+    /**
+     * Extracts variables with constant values from an expression Returns a map from variable names to their values
+     */
     public static Map<String, Expression> resolve(Expression exp) {
         Map<String, Expression> map = new HashMap<>();
         resolveRecursive(exp, map);
         return resolveTransitive(map);
     }
 
+    /**
+     * Recursively extracts variable equalities from an expression (e.g. ... && x == 1 && y == 2 => map: x -> 1, y -> 2)
+     * Modifies the given map in place
+     */
     private static void resolveRecursive(Expression exp, Map<String, Expression> map) {
         if (!(exp instanceof BinaryExpression))
             return;
@@ -30,14 +37,16 @@ private static void resolveRecursive(Expression exp, Map<String, Expression> map
             Expression left = be.getFirstOperand();
             Expression right = be.getSecondOperand();
             if (left instanceof Var && (right.isLiteral() || right instanceof Var)) {
-                map.put(left.toString(), right.clone());
+                map.put(((Var) left).getName(), right.clone());
             } else if (right instanceof Var && left.isLiteral()) {
-                map.put(right.toString(), left.clone());
+                map.put(((Var) right).getName(), left.clone());
             }
         }
     }
 
-    // e.g. x == y && y == 1 => x == 1
+    /**
+     * Handles transitive variable equalities in the map (e.g. map: x -> y, y -> 1 => map: x -> 1, y -> 1)
+     */
     private static Map<String, Expression> resolveTransitive(Map<String, Expression> map) {
         Map<String, Expression> result = new HashMap<>();
         for (Map.Entry<String, Expression> entry : map.entrySet()) {
@@ -46,6 +55,10 @@ private static Map<String, Expression> resolveTransitive(Map<String, Expression>
         return result;
     }
 
+    /**
+     * Returns the value of a variable by looking up in the map recursively Uses the seen set to avoid circular
+     * references (e.g. x -> y, y -> x) which would cause infinite recursion
+     */
     private static Expression lookup(Expression exp, Map<String, Expression> map, Set<String> seen) {
         if (!(exp instanceof Var))
             return exp;

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/DerivationNode.java

@@ -5,10 +5,8 @@
 
 public abstract class DerivationNode {
 
-    private static final Gson gson = new GsonBuilder()
-        .setPrettyPrinting() // remove later
-        .disableHtmlEscaping() // to not escape characters like &, >, <, =, etc.
-        .create();
+    // disable html escaping to avoid escaping characters like &, >, <, =, etc.
+    private static final Gson gson = new GsonBuilder().setPrettyPrinting().disableHtmlEscaping().create();
 
     @Override
     public String toString() {

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java

@@ -34,6 +34,7 @@ public DerivationNode getOrigin() {
         return origin;
     }
 
+    // Custom serializer to handle Expression subclasses properly
     private static class ExpressionSerializer implements JsonSerializer<Expression> {
         @Override
         public JsonElement serialize(Expression exp, Type typeOfSrc, JsonSerializationContext context) {