adding translation for fresh (#91)

some test cases fail

modules/core/src/edu/kit/iti/algover/parser/Dafny.g

@@ -81,6 +81,7 @@ ENSURES: 'ensures';
 EX: 'exists';
 FALSE: 'false';
 FREE: 'free';
+FRESH: 'fresh';
 FUNCTION: 'function';
 IF: 'if';
 IN : 'in';

modules/core/src/edu/kit/iti/algover/symbex/Symbex.java

@@ -259,6 +259,25 @@ private List<DafnyTree> handleMethodCall(Deque<SymbexPath> stack, SymbexPath sta
             // "heap := anon(heap, mod, ...)"
             state.addAssignment(ASTUtil.anonymiseHeap(state, mod));
 
+            // if result is reference type: it is created
+            if(returns != null) {
+                List<DafnyTree> allFresh = new ArrayList<>();
+                for (DafnyTree ret : returns.getChildren()) {
+                    DafnyTree type = ret.getFirstChildWithType(DafnyParser.TYPE).getChild(0);
+                    Sort sort = ASTUtil.toSort(type);
+                    if(sort.isReferenceSort()) {
+                        DafnyTree fresh = ASTUtil.call("$isCreated",
+                                ASTUtil.builtInVar("$heap"), ret.getChild(0));
+                        allFresh.add(fresh);
+                    }
+                }
+                if (!allFresh.isEmpty()) {
+                    DafnyTree cond = ASTUtil.and(allFresh);
+                    cond = ASTUtil.letCascade(subs, cond);
+                    state.addPathCondition(cond, refersTo, AssumptionType.IMPLICIT_ASSUMPTION);
+                }
+            }
+
         }
 
         // now assume the postcondition (and some free postconditions)

modules/core/src/edu/kit/iti/algover/term/Sort.java

@@ -301,15 +301,28 @@ public Sort getArgument(int index) {
     /**
      * Checks if this sort belongs to a Dafny class.
      *
-     * Checks if the name is a builtin name
+     * Checks if the name is a builtin name.
      *
-     * @return <code>true</code>, iff this objects reprsents the sort for a
+     * @return <code>true</code>, iff this objects represents the sort for a
      *         Dafny class
      */
     public boolean isClassSort() {
         return !BUILTIN_SORT_NAMES.contains(getName());
     }
 
+    /**
+     * Checks if this sort is a reference sort.
+     *
+     * This is the case for object, classes and arrays.
+     *
+     * Equivalent to calling {@code isSubtypeOf(OBJECT)}.
+     *
+     * @return <code>true</code>, iff this objects represents a ref type.
+     */
+    public boolean isReferenceSort() {
+        return isSubtypeOf(OBJECT);
+    }
+
     /**
      * Checks if this sort is a subtype/subsort of its argument.
      *

modules/core/src/edu/kit/iti/algover/term/builder/TermBuilder.java

@@ -254,4 +254,9 @@ public Term seqUpd(Term seqTerm, Term indexTerm, Term value) throws TermBuildExc
     }
 
 
+    public Term fresh(Term oldheap, Term newheap, Term object) throws TermBuildException {
+        ApplTerm o = new ApplTerm(BuiltinSymbols.IS_CREATED, oldheap, object);
+        ApplTerm n = new ApplTerm(BuiltinSymbols.IS_CREATED, newheap, object);
+        return and(negate(o), n);
+    }
 }

modules/core/src/edu/kit/iti/algover/term/builder/TreeTermTranslator.java

@@ -40,6 +40,7 @@
 import java.util.IdentityHashMap;
 import java.util.List;
 import java.util.Map;
+import java.util.Objects;
 
 /**
  * The Class TreeTermTranslator is used to create a {@link Term} object from a
@@ -58,6 +59,12 @@ public class TreeTermTranslator {
     private static final VariableTerm HEAP_VAR =
             new VariableTerm("$heap", Sort.HEAP);
 
+    /**
+     * This constant is used by old and fresh expressions.
+     */
+    private static final VariableTerm OLD_HEAP_VAR =
+            new VariableTerm("$oldheap", Sort.HEAP);
+
     /**
      * The symbol table from which the function symbols etc are to be taken.
      */
@@ -448,6 +455,10 @@ public Term build(DafnyTree tree) throws TermBuildException {
             result = buildNoetherLess(tree);
             break;
 
+        case DafnyParser.FRESH:
+            result = buildFresh(tree);
+            break;
+
         case DafnyParser.AT:
             result = buildExplicitHeapAccess(tree);
             break;
@@ -680,6 +691,21 @@ private Term buildFieldAccess(DafnyTree tree) throws TermBuildException {
         return tb.selectField(getHeap(), receiver, new ApplTerm(field));
     }
 
+    private Term buildFresh(DafnyTree tree) throws TermBuildException {
+        Term receiver = build(tree.getChild(0));
+
+        if(!receiver.getSort().isReferenceSort()) {
+            throw new TermBuildException("fresh can only be applied to objects, " +
+                    "not to " + receiver.getSort());
+        }
+
+        if (!Objects.equals(boundVars.get(OLD_HEAP_VAR.getName()), OLD_HEAP_VAR)) {
+            throw new TermBuildException("fresh-expression not allowed in single-state context");
+        }
+
+        return tb.fresh(OLD_HEAP_VAR, getHeap(), receiver);
+    }
+
 
     private Term buildLength(DafnyTree tree) throws TermBuildException {
         String functionName = tree.toString();
@@ -1001,11 +1027,15 @@ private Term buildExplicitHeapAccess(DafnyTree tree) throws TermBuildException {
 
     private Term buildOld(DafnyTree tree) throws TermBuildException {
 
+        if (!Objects.equals(boundVars.get(OLD_HEAP_VAR.getName()), OLD_HEAP_VAR)) {
+            throw new TermBuildException("old-expression not allowed in single-state context");
+        }
+
         boundVars.put(HEAP_VAR.getName(), HEAP_VAR);
         Term inner = build(tree.getChild(0));
         boundVars.pop();
 
-        return new LetTerm(HEAP_VAR, HEAP_VAR, inner);
+        return new LetTerm(HEAP_VAR, OLD_HEAP_VAR, inner);
     }
 
 

modules/core/test-res/edu/kit/iti/algover/symbex/methodCalls.dfy

@@ -51,4 +51,17 @@ method recursive(n: int) returns (r: int)
   } else {
     r := recursive(n - 1);
   }
+}
+
+method objectReturn(b: bool) returns (o : Clss)
+  ensures true;
+{
+  if(b)
+  {
+    o := new Clss;
+    o.field := 12;
+  } else
+  {
+    o := objectReturn(true);
+  }
 }

modules/core/test/edu/kit/iti/algover/symbex/SymbexTest.java

@@ -931,6 +931,55 @@ public void testRecursiveMethodCalls() throws Exception {
         }
     }
 
+    @Test
+    public void testObjectMethodCall() throws Exception {
+        InputStream stream = getClass().getResourceAsStream("methodCalls.dfy");
+        DafnyTree fileTree = ParserTest.parseFile(stream);
+
+        // performs type analysis etc:
+        Project project = TestUtil.mockProject(fileTree);
+
+        DafnyTree tree = project.getMethod("objectReturn").getRepresentation();
+        Symbex symbex = new Symbex();
+        List<SymbexPath> results = symbex.symbolicExecution(tree);
+        int index = 0;
+        {
+            SymbexPath path = results.get(index++);
+            assertEquals("else/Post", path.getPathIdentifier());
+
+            assertEquals("[(not b), " +
+                            "(LET (VAR o b) $res_objectReturn_1 true (CALL $isCreated (ARGS $heap o))), " +
+                            "(LET (VAR o b) $res_objectReturn_1 true true)]",
+                    path.getPathConditions().map(x -> x.getExpression().toStringTree()).toString());
+
+            assertEquals("[(ASSIGN $mod SETEX), (ASSIGN $decr 0), " +
+                            "(ASSIGN $heap (CALL $anon (ARGS $heap (LET (VAR o b) $res_objectReturn_1 true SETEX) $aheap_1))), " +
+                            "(ASSIGN o $res_objectReturn_1)]",
+                    path.getAssignmentHistory().map(x -> x.toStringTree()).toString());
+        }
+        {
+            SymbexPath path = results.get(index++);
+            assertEquals("then/Post", path.getPathIdentifier());
+        }
+        {
+            SymbexPath path = results.get(index++);
+            assertEquals("then/Modifies", path.getPathIdentifier());
+        }
+        {
+            SymbexPath path = results.get(index++);
+            assertEquals("else/Dec[objectReturn]", path.getPathIdentifier());
+        }
+        {
+            SymbexPath path = results.get(index++);
+            assertEquals("else/Modifies[objectReturn]", path.getPathIdentifier());
+        }
+        {
+            SymbexPath path = results.get(index++);
+            assertEquals("then/Null", path.getPathIdentifier());
+        }
+        assertEquals(index, results.size());
+    }
+
     @Test
     public void testFieldAssignment() throws Exception {
         InputStream stream = getClass().getResourceAsStream("fieldAssignment.dfy");

modules/core/test/edu/kit/iti/algover/term/builder/TreeTermTranslatorTest.java

@@ -154,17 +154,22 @@ public String[][] parametersForTestTermTranslation() {
             { "1*2*3", "$times($times(1, 2), 3)" },
             { "b1 ==> b2 ==> b3", "$imp(b1, $imp(b2, b3))" },
 
+            { "let $oldheap := loopHeap :: old(c.f)==c.f",
+              "(let $oldheap := loopHeap :: $eq<int>(" +
+                      "(let $heap := $oldheap :: $select<C,int>($heap, c, C$$f)), $select<C,int>($heap, c, C$$f)))" },
+
             // Heap accesses
             { "c.f", "$select<C,int>($heap, c, C$$f)" },
             { "c.f", "$select<C,int>($heap, c, C$$f)" },
             { "c.f@loopHeap", "$select<C,int>(loopHeap, c, C$$f)" },
             { "c.fct(1)", "C$$fct($heap, c, 1)"},
             { "c.fct(1)@loopHeap", "C$$fct(loopHeap, c, 1)" },
-            { "fresh(c)", "$not($created($heap,c))" },
-            { "fresh(c)@loopHeap", "$not($created($loopHeap,c))" },
+            { "let $oldheap := loopHeap :: fresh(c)",
+              "(let $oldheap := loopHeap :: $and($not($isCreated($oldheap, c)), $isCreated($heap, c)))" },
 
             // Heap updates
             { "$heap[c.f := 1]", "$store<C,int>($heap, c, C$$f, 1)" },
+            { "$heap[a[0] := 2]", "$array_store<int>($heap, a, 0, 2)" },
             { "$heap[$anon(mod, loopHeap)]", "$anon($heap, mod, loopHeap)" },
             { "$heap[$create(c)]", "$create($heap, c)" },
 
@@ -237,6 +242,11 @@ public String[][] parametersForFailingParser() {
             { "iseq + mod", "No common supertype for seq<int> and set<object>" },
             { "true + true", "'+' is not supported for these arguments" },
             { "c == 1", "No common supertype for C and int" },
+            { "old(c.f)", "old-expression not allowed in single-state context" },
+            { "fresh(c)", "fresh-expression not allowed in single-state context" },
+            { "fresh(1)", "fresh can only be applied to objects, not to int"},
+            { "|1|", "Unsupported sort for |...|: int" },
+            { "1@$heap", "heap suffixes are only allowed for heap select terms" },
         };
     }