Add VC Substitution Simplification (#249)

Author: rcosta358

liquidjava-verifier/pom.xml

@@ -301,16 +301,28 @@
 			<artifactId>junit-vintage-engine</artifactId>
 			<scope>test</scope>
 		</dependency>
-		<dependency>
-			<groupId>org.junit.jupiter</groupId>
-			<artifactId>junit-jupiter-params</artifactId>
-			<scope>test</scope>
-		</dependency>
-		<dependency>
-			<groupId>ch.qos.logback</groupId>
-			<artifactId>logback-classic</artifactId>
-			<version>1.4.12</version>
-		</dependency>
+		<dependency>
+			<groupId>org.junit.jupiter</groupId>
+			<artifactId>junit-jupiter-params</artifactId>
+			<scope>test</scope>
+		</dependency>
+		<dependency>
+			<groupId>com.pholser</groupId>
+			<artifactId>junit-quickcheck-core</artifactId>
+			<version>1.0</version>
+			<scope>test</scope>
+		</dependency>
+		<dependency>
+			<groupId>com.pholser</groupId>
+			<artifactId>junit-quickcheck-generators</artifactId>
+			<version>1.0</version>
+			<scope>test</scope>
+		</dependency>
+		<dependency>
+			<groupId>ch.qos.logback</groupId>
+			<artifactId>logback-classic</artifactId>
+			<version>1.4.12</version>
+		</dependency>
 		<dependency>
 			<groupId>org.mdkt.compiler</groupId>
 			<artifactId>InMemoryJavaCompiler</artifactId>

liquidjava-verifier/src/main/java/liquidjava/processor/SimplifiedVCImplication.java

@@ -0,0 +1,53 @@
+package liquidjava.processor;
+
+import java.util.Objects;
+
+import liquidjava.rj_language.Predicate;
+
+/**
+ * Represents a VC implication node whose refinement was simplified from another quantified VC shape.
+ */
+public class SimplifiedVCImplication extends VCImplication {
+
+    private final VCImplication origin;
+
+    public SimplifiedVCImplication(VCImplication implication, Predicate refinement, VCImplication origin) {
+        super(implication, refinement);
+        this.origin = origin.clone();
+    }
+
+    @Override
+    public VCImplication getOrigin() {
+        return origin;
+    }
+
+    @Override
+    public VCImplication copyWithRefinement(Predicate refinement) {
+        return new SimplifiedVCImplication(this, refinement, origin);
+    }
+
+    @Override
+    public SimplifiedVCImplication clone() {
+        SimplifiedVCImplication vc = new SimplifiedVCImplication(this, this.refinement.clone(), origin);
+        if (this.next != null)
+            vc.next = this.next.clone();
+        return vc;
+    }
+
+    @Override
+    public int hashCode() {
+        return Objects.hash(super.hashCode(), origin);
+    }
+
+    @Override
+    public boolean equals(Object obj) {
+        if (this == obj)
+            return true;
+        if (!(obj instanceof SimplifiedVCImplication))
+            return false;
+        if (!super.equals(obj))
+            return false;
+        SimplifiedVCImplication other = (SimplifiedVCImplication) obj;
+        return origin.equals(other.origin);
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java

@@ -1,5 +1,7 @@
 package liquidjava.processor;
 
+import java.util.Objects;
+
 import liquidjava.rj_language.Predicate;
 import liquidjava.utils.Utils;
 import spoon.reflect.reference.CtTypeReference;
@@ -23,6 +25,24 @@ public VCImplication(Predicate ref) {
         this.refinement = ref;
     }
 
+    public VCImplication(VCImplication implication, Predicate ref) {
+        this.name = implication.name;
+        this.type = implication.type;
+        this.refinement = ref;
+    }
+
+    public VCImplication getOrigin() {
+        return new VCImplication(this, refinement.clone());
+    }
+
+    public Predicate getOriginRefinement() {
+        return getOrigin().getRefinement().clone();
+    }
+
+    public VCImplication copyWithRefinement(Predicate refinement) {
+        return new VCImplication(this, refinement);
+    }
+
     public void setNext(VCImplication c) {
         next = c;
     }
@@ -47,6 +67,14 @@ public VCImplication getNext() {
         return next;
     }
 
+    public boolean hasNext() {
+        return next != null;
+    }
+
+    public boolean hasBinder() {
+        return name != null && type != null;
+    }
+
     public String toString() {
         if (name != null && type != null) {
             String qualType = type.getQualifiedName();
@@ -79,4 +107,26 @@ public VCImplication clone() {
             vc.next = this.next.clone();
         return vc;
     }
+
+    @Override
+    public int hashCode() {
+        return Objects.hash(name, typeName(), refinement, next);
+    }
+
+    @Override
+    public boolean equals(Object obj) {
+        if (this == obj)
+            return true;
+        if (obj == null)
+            return false;
+        if (getClass() != obj.getClass())
+            return false;
+        VCImplication other = (VCImplication) obj;
+        return Objects.equals(name, other.name) && Objects.equals(typeName(), other.typeName())
+                && Objects.equals(refinement, other.refinement) && Objects.equals(next, other.next);
+    }
+
+    private String typeName() {
+        return type == null ? null : type.getQualifiedName();
+    }
 }

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

@@ -235,6 +235,11 @@ public Predicate clone() {
         return new Predicate(exp.clone());
     }
 
+    @Override
+    public int hashCode() {
+        return exp.hashCode();
+    }
+
     @Override
     public boolean equals(Object obj) {
         if (this == obj)
@@ -251,6 +256,10 @@ public Expression getExpression() {
         return exp;
     }
 
+    public Predicate getOrigin() {
+        return this;
+    }
+
     public ValDerivationNode simplify(Context context) {
         // collect aliases from context
         Map<String, AliasDTO> aliases = new HashMap<>();

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

@@ -0,0 +1,42 @@
+package liquidjava.rj_language.opt;
+
+import liquidjava.processor.VCImplication;
+
+/**
+ * Simplifies VCImplication chains by applying various simplification steps
+ */
+public class VCSimplification {
+
+    /**
+     * Applies all available simplification steps to a VC chain
+     */
+    public static VCImplication simplifyToFixedPoint(VCImplication implication) {
+        if (implication == null)
+            return null;
+
+        // keep applying simplification steps until a fixed point is reached
+        VCImplication current = implication.clone();
+        while (true) {
+            VCImplication simplified = simplifyOnce(current);
+            if (current.equals(simplified)) // fixed point reached
+                return simplified;
+            current = simplified;
+        }
+    }
+
+    /**
+     * Applies one simplification step to a VC chain
+     */
+    public static VCImplication simplifyOnce(VCImplication implication) {
+        if (implication == null)
+            return null;
+
+        // first try to apply substitution, then folding
+        VCImplication substituted = VCSubstitution.apply(implication);
+        if (!implication.equals(substituted))
+            return substituted;
+
+        // TODO: add more simplification steps here (e.g., folding)
+        return substituted;
+    }
+}