examples and changes to use refinements in if conds

Author: CatarinaGamboa

liquidjava-example/src/main/java/testSuite/classes/state_test_method_correct/AbstractUndoableEditRefinements.java

@@ -0,0 +1,29 @@
+package testSuite.classes.state_test_method_correct;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"aliveDone", "aliveNotDone", "notAlive"})
+@ExternalRefinementsFor("javax.swing.undo.AbstractUndoableEdit")
+public interface AbstractUndoableEditRefinements {
+
+    @StateRefinement(to = "aliveDone(this)")
+    void AbstractUndoableEdit();
+
+    @StateRefinement(from = "aliveNotDone(this)", to = "aliveDone(this)")
+    void redo();
+
+    @StateRefinement(from = "aliveDone(this)", to = "aliveNotDone(this)")
+    void undo();
+
+    @StateRefinement(from = "!notAlive(this)", to = "notAlive(this)")
+    void die();
+
+    @Refinement("_ == true --> aliveDone(this)")
+    boolean canUndo();
+
+    @Refinement("_ == true --> aliveNotDone(this)")
+    boolean canRedo();
+}

liquidjava-example/src/main/java/testSuite/classes/state_test_method_correct/EditCycler.java

@@ -0,0 +1,17 @@
+package testSuite.classes.state_test_method_correct;
+
+import javax.swing.undo.AbstractUndoableEdit;
+
+public class EditCycler {
+    public static void undoIfPossible(AbstractUndoableEdit edit) {
+        if (edit.canUndo()) {
+            edit.undo();
+        }
+    }
+
+    public static void redoIfPossible(AbstractUndoableEdit edit) {
+        if (edit.canRedo()) {
+            edit.redo();
+        }
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/AbstractUndoableEditRefinements.java

@@ -0,0 +1,26 @@
+package testSuite.classes.state_test_method_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"aliveDone", "aliveNotDone", "notAlive"})
+@ExternalRefinementsFor("javax.swing.undo.AbstractUndoableEdit")
+public interface AbstractUndoableEditRefinements {
+
+    @StateRefinement(to = "aliveDone(this)")
+    void AbstractUndoableEdit();
+
+    @StateRefinement(from = "aliveNotDone(this)", to = "aliveDone(this)")
+    void redo();
+
+    @StateRefinement(from = "aliveDone(this)", to = "aliveNotDone(this)")
+    void undo();
+
+    @Refinement("_ == true --> aliveDone(this)")
+    boolean canUndo();
+
+    @Refinement("_ == true --> aliveNotDone(this)")
+    boolean canRedo();
+}

liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/EditMisuse.java

@@ -0,0 +1,24 @@
+package testSuite.classes.state_test_method_error;
+
+import javax.swing.undo.AbstractUndoableEdit;
+
+public class EditMisuse {
+
+    public static void undoInElseBranch(AbstractUndoableEdit edit) {
+        if (edit.canUndo()) {
+        } else {
+            edit.undo(); // State Refinement Error
+        }
+    }
+
+    public static void undoNotInElse(AbstractUndoableEdit edit) {
+        if (!edit.canUndo()) {
+            edit.undo(); // State Refinement Error
+        } 
+    }
+    public static void wrongTesterForRedo(AbstractUndoableEdit edit) {
+        if (edit.canUndo()) {
+            edit.redo(); // State Refinement Error
+        }
+    }
+}

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

@@ -343,24 +343,47 @@ public void visitCtIf(CtIf ifElement) {
 
         String pathVarName = String.format(Formats.FRESH, context.getCounter());
         RefinedVariable freshRV;
+        // The condition's predicate may use Keys.WILDCARD as a stand-in for the boolean value of the condition
+        // (e.g. invocation post-conditions of the form `_ == true --> state(this)`, or variable reads `_ == k`).
+        // When that's the case the fresh path variable IS that boolean value, so we assert it true in the then
+        // branch and false in the else branch — instead of negating the whole predicate, which is unsound for
+        // implications and equality forms.
+        boolean valueIsCondition = false;
+        Predicate thenRefs;
+        Predicate elseRefs;
         if (isUninformativeCondition(expRefs, exp)) {
             // No refinement means the condition is unknown, not true: model it as a fresh
             // boolean so the SMT solver may pick either truth value for each branch.
             expRefs = Predicate.createVar(pathVarName);
+            thenRefs = expRefs;
+            elseRefs = expRefs.negate();
             freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, new Predicate(), exp);
         } else {
+            valueIsCondition = expRefs.getVariableNames().contains(Keys.WILDCARD);
             expRefs = expRefs.substituteVariable(Keys.WILDCARD, pathVarName);
             Predicate lastExpRefs = substituteAllVariablesForLastInstance(expRefs);
             expRefs = Predicate.createConjunction(expRefs, lastExpRefs);
 
-            freshRV = context.addInstanceToContext(pathVarName, factory.Type().INTEGER_PRIMITIVE, expRefs, exp);
-        }
+            // TODO Change in future
+            if (expRefs.getVariableNames().contains("null")) {
+                expRefs = new Predicate();
+                valueIsCondition = false;
+            }
 
-        // TODO Change in future
-        if (expRefs.getVariableNames().contains("null")) {
-            expRefs = new Predicate();
+            thenRefs = expRefs;
+            elseRefs = expRefs.negate();
+            if (valueIsCondition) {
+                Predicate freshIsTrue = Predicate.createEquals(Predicate.createVar(pathVarName),
+                        Predicate.createLit("true", Types.BOOLEAN));
+                Predicate freshIsFalse = Predicate.createEquals(Predicate.createVar(pathVarName),
+                        Predicate.createLit("false", Types.BOOLEAN));
+                thenRefs = Predicate.createConjunction(expRefs, freshIsTrue);
+                elseRefs = Predicate.createConjunction(expRefs, freshIsFalse);
+                freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, thenRefs, exp);
+            } else {
+                freshRV = context.addInstanceToContext(pathVarName, factory.Type().INTEGER_PRIMITIVE, expRefs, exp);
+            }
         }
-
         vcChecker.addPathVariable(freshRV);
 
         context.variablesNewIfCombination();
@@ -378,7 +401,8 @@ public void visitCtIf(CtIf ifElement) {
 
         // VISIT ELSE
         if (ifElement.getElseStatement() != null) {
-            context.newRefinementToVariableInContext(pathVarName, expRefs.negate());
+            context.getVariableByName(pathVarName);
+            context.newRefinementToVariableInContext(pathVarName, elseRefs);
 
             context.enterContext();
             visitCtBlock(ifElement.getElseStatement());