Don't Simplify Expected Type

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java

@@ -6,6 +6,7 @@
 
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.processor.VCImplication;
+import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.formatter.VariableFormatter;
 import liquidjava.smt.Counterexample;
@@ -18,15 +19,14 @@
  */
 public class RefinementError extends LJError {
 
-    private final VCImplication expected;
+    private final Predicate expected;
     private final VCImplication found;
     private final Counterexample counterexample;
 
-    public RefinementError(SourcePosition position, VCImplication expected, VCImplication found,
+    public RefinementError(SourcePosition position, Predicate expected, VCImplication found,
             TranslationTable translationTable, Counterexample counterexample, String customMessage) {
-        super("Refinement Error",
-                String.format("%s is not a subtype of %s", found.toPredicate().getExpression().toDisplayString(),
-                        expected.toPredicate().getExpression().toDisplayString()),
+        super("Refinement Error", String.format("%s is not a subtype of %s",
+                found.toPredicate().getExpression().toDisplayString(), expected.getExpression().toDisplayString()),
                 position, translationTable, customMessage);
         this.expected = expected;
         this.found = found;
@@ -47,7 +47,7 @@ public String getCounterExampleString() {
 
         List<String> foundVarNames = new ArrayList<>();
         Expression foundExpression = found.toPredicate().getExpression();
-        Expression expectedExpression = expected.toPredicate().getExpression();
+        Expression expectedExpression = expected.getExpression();
         foundExpression.getVariableNames(foundVarNames);
         // also keep resolved static-final constants (e.g. Integer.MAX_VALUE) referenced by either side of the
         // subtyping check, so the counterexample maps the symbolic name back to its compile-time value
@@ -73,7 +73,7 @@ public Counterexample getCounterexample() {
         return counterexample;
     }
 
-    public VCImplication getExpected() {
+    public Predicate getExpected() {
         return expected;
     }
 

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java

@@ -2,6 +2,7 @@
 
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.processor.VCImplication;
+import liquidjava.rj_language.Predicate;
 import spoon.reflect.cu.SourcePosition;
 
 /**
@@ -11,21 +12,20 @@
  */
 public class StateRefinementError extends LJError {
 
-    private final VCImplication expected;
+    private final Predicate expected;
     private final VCImplication found;
 
-    public StateRefinementError(SourcePosition position, VCImplication expected, VCImplication found,
+    public StateRefinementError(SourcePosition position, Predicate expected, VCImplication found,
             TranslationTable translationTable, String customMessage) {
         super("State Refinement Error",
-                String.format("Expected state %s but found %s",
-                        expected.toPredicate().getExpression().toDisplayString(),
+                String.format("Expected state %s but found %s", expected.getExpression().toDisplayString(),
                         found.toPredicate().getExpression().toDisplayString()),
                 position, translationTable, customMessage);
         this.expected = expected;
         this.found = found;
     }
 
-    public VCImplication getExpected() {
+    public Predicate getExpected() {
         return expected;
     }
 

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

@@ -82,8 +82,8 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
         }
         DebugLog.smtResult(result);
         if (result.isError()) {
-            throw new RefinementError(element.getPosition(), expectedType.simplify(context),
-                    implBeforeChange.simplify(), map, result.getCounterexample(), customMessage);
+            throw new RefinementError(element.getPosition(), expectedType, implBeforeChange.simplify(), map,
+                    result.getCounterexample(), customMessage);
         }
     }
 
@@ -407,15 +407,14 @@ protected void throwRefinementError(SourcePosition position, Predicate expected,
             Counterexample counterexample, String customMessage) throws RefinementError {
         TranslationTable map = new TranslationTable();
         VCImplication premises = buildPremiseChain(map, expected, found);
-        throw new RefinementError(position, expected.simplify(context), premises.simplify(), map, counterexample,
-                customMessage);
+        throw new RefinementError(position, expected, premises.simplify(), map, counterexample, customMessage);
     }
 
     protected void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected,
             String customMessage) throws StateRefinementError {
         TranslationTable map = new TranslationTable();
         VCImplication foundState = buildPremiseChain(map, expected, found);
-        throw new StateRefinementError(position, expected.simplify(context), foundState.simplify(), map, customMessage);
+        throw new StateRefinementError(position, expected, foundState.simplify(), map, customMessage);
     }
 
     protected void throwStateConflictError(SourcePosition position, Predicate expected) throws StateConflictError {

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

@@ -259,7 +259,7 @@ public Predicate getOrigin() {
         return this;
     }
 
-    public VCImplication simplify(Context context) {
+    public VCImplication simplify() {
         VCImplication result = new VCImplication(clone()).simplify();
         DebugLog.simplification(this.getExpression(), result.getRefinement().getExpression());
         return result;