various fixes

input/symb/test0.alk

@@ -0,0 +1,16 @@
+symbolic $a:array<int>;
+a = $a;
+assume a.size() < 2;
+min = a[0];
+i = 1;
+while (i < a.size())
+invariant a
+invariant b
+invariant c
+modifies i
+{
+    if (a[i] < min) min = a[i];
+    i = i+1;
+
+    assert d;
+}

input/symb/test1.alk

@@ -0,0 +1,23 @@
+plateau(a: array<int>)
+requires forall i:int :: 0 <= i && i < a.size() - 1 ==> a[i] <= a[i+1]
+ensures (forall k:int :: forall l:int :: 0 <= k && k <= l && l < a.size() && a[k] == a[l] ==> (l-k) <= result)
+{
+    lg = 1;
+    i = 1;
+    while (i < a.size())
+    invariant (forall k:int :: forall l:int ::
+        0 <= k && k <= l && l < i && a[k] == a[l]
+        ==>
+        (l-k) <= lg)
+    modifies lg
+    {
+        if (a[i] == a[i - lg]) lg = lg+1;
+        i = i + 1;
+    }
+}
+
+symbolic $a: array<int>;
+a = $a;
+assume a.size() < 4;
+assume forall i:int :: 0 <= i && i < a.size()-1 ==> a[i] <= a[i+1];
+x = plateau(a);

input/symb/test2.alk

@@ -0,0 +1,38 @@
+plateau(a: array<int>) : int
+requires forall i:int :: 0 <= i && i < a.size()-1 ==> a[i] <= a[i+1]
+ensures (forall k:int :: forall l:int ::
+    0 <= k && k <= l && l < a.size() && a[k] == a[l]
+    ==>
+    (l-k) <= result)
+{
+    lg = 1;
+    i = 1;
+    while (i < a.size())
+    invariant (forall k:int :: forall l:int ::
+        0 <= k && k <= l && l < i && a[k] == a[l]
+        ==>
+        (l-k) <= lg)
+    modifies lg
+    {
+        if (a[i] == a[i - lg]) lg = lg+1;
+        i = i + 1;
+    }
+    return lg;
+}
+
+symbolic $a: array<int>;
+a = $a;
+//assume a.size() < 4;
+assume forall i:int :: 0 <= i && i < a.size()-1 ==> a[i] <= a[i+1];
+//x = plateau(a);
+for (i = 0; i < 4; ++i)
+{
+    havoc a;
+    assume a.size() == i;
+    x[i] = plateau(a);
+}
+
+assert x[0] <= x[1] && x[1] <= x[2] && x[2] <= x[3];
+
+Internal error [0:0]
+Unknown Z3 check! [5:3]

input/symb/test3.alk

@@ -0,0 +1,11 @@
+symbolic $n: int;
+n = $n;
+sum = 0;
+i = 1;
+
+while (i <= n)
+invariant sum == (i-1)*i/2
+{
+    sum = sum + i;
+    i = i + 1;
+}

input/symb/test4.alk

@@ -0,0 +1,18 @@
+alg12(a: array<int>) : int
+{
+    lg = 1;
+    i = 1;
+    while (i < a.size())
+    {
+        if (a[i] == a[i - lg]) lg = lg+1;
+        i = i + 1;
+    }
+    return lg;
+}
+
+symbolic $a: array<int>;
+a = $a;
+assume forall i:int :: 0 <= i && i < a.size()-1 ==> a[i] <= a[i+1];
+assume a.size() == 3;
+
+x = alg12(a);

input/symb/test5.alk

@@ -0,0 +1,36 @@
+askIth(out a:array<int>, i:int) : int
+requires a.size() > 0 && 0 <= i && i < a.size()-1
+ensures a[i] <= a[i+1]
+ensures result > 0 ==> result == i
+{
+    if (a[i] > a[i+1]) {
+        temp = a[i];
+        a[i] = a[i+1];
+        a[i+1] = temp;
+        return i;
+    }
+    return 0;
+}
+
+sorted(out a) {
+    return forall j:int :: forall k:int ::
+           0 <= j && j <= last && last < k &&
+           k < a.size() ==> a[j] <= a[k];
+}
+
+bubbleSort(out a: array<int>) {
+    last = a.size()-1;
+    while (last > 0)
+    invariant sorted(a)
+    {
+        n1 = last;
+        i = 0;
+        while (i < n1)
+        invariant forall j:int ::
+        0 <= j && j < i ==> a[j] <= a[i]
+        {
+            last = askIth(a, i);
+            i = i + 1;
+        }
+    }
+}

input/symb/test6.alk

@@ -0,0 +1,17 @@
+@symbolic $a: array<int>;
+a = $a;
+@assume forall i:int :: 0 <= i && i < a.size()-1 ==> a[i] <= a[i+1];
+slp = 1;
+i = 1;
+while (i < a.size())
+@invariant i <= a.size()
+@invariant (forall k:int :: forall l:int ::
+    0 <= k && k <= l && l < i && a[k] == a[l]
+    ==>
+    (l-k) <= slp)
+@modifies slp
+@modifies i
+{
+    if (a[i] == a[i - slp]) slp = slp+1;
+    i = i + 1;
+}

input/symb/test7.alk

@@ -0,0 +1,16 @@
+@symbolic $a: array<int>;
+a = $a;
+@assume forall i:int :: 0 <= i && i < a.size()-1 ==> a[i] <= a[i+1];
+slp = 1;
+i = 1;
+while (i < a.size())
+@invariant slp <= i
+@invariant (forall k:int :: forall l:int ::
+    0 <= k && k <= l && l < i && a[k] == a[l]
+    ==>
+    (l-k) <= slp)
+@modifies slp, i
+{
+    if (a[i] == a[i - slp]) slp = slp+1;
+    i = i + 1;
+}

input/test5.alk

@@ -1,17 +1,7 @@
-a = { "a" |-> 5 };
-
-{} x = a.keys()
-
-// map-uri (keys)
-// invariantii trebuie procesati intr-o singura executie (nu o executie pentru fiecare invariant)
-
-// apel conditional la Z3 (-pr)
-// dataflow -> cautare secventiala si minim in tablou
-// conversia structurilor si a map-urilor in Z3
-
-// redenumit keyword-urile assert, assume, requires, ensures, symbolic, modifies -> @
-// operatorul : pentru apartenenta la un tip de date:
-    // @requires a : array<int> && x : int;  -> din gramatica
-    // @ensures  result : int;               -> din gramatica
-    // type assertions
-// @Trusted
+@symbolic $a : array<int>, $i : int;
+a = $a;
+@assume a.size() == 8;
+a.pushFront($i);
+@assert a.topFront() == $i;
+b = $a;
+@assert b.topFront() == b[0];

input/test7.alk

@@ -1,18 +1,16 @@
-a = [1, 2, 3, 4, 5];
-i = 0;
-minim = a[0];
+// map-urile au fost rezolvate
 
-while (i < a.size())
-// invariant i <= a.size()
-// invariant forall j : int :: 0 <= j && j < i ==> minim <= a[j]
-// modifies i, minim
-{
-    if (a[i] < minim)
-    {
-        minim = a[i];
-    }
-    i++;
-}
 
+// putem pune in orice ordine modifies, invariant !!!!!!!! nu se poate o lista
+// am formatat path condition -> de adaugat Type Constraints
 
+// functiile ce nu au ensures, nu sunt verificate
+// rezolvat problema cu bracket cand ambele valori sunt concrete dar array-ul are valori simbolice
+// rezolvat cazul cu UNKNOWN -> unkown Z3 check
+// tratat cazul in care nu se defineste tipul de return
+// tratat cazul in care avem result dar nu avem return
+// invariant poate fi valoare concreta booleana
+// invariantii sunt verificati intr-un singur thread
+// am adaugat optiunea -prover pentru a specifica proverul
 
+// executia simbolica a functiilor "predicat"

output.log

@@ -1,26 +1,16 @@
-Can't use return outside function scope.
-a |-> $a_0
-[result] |-> $minim_0
-minim |-> $minim_0
-i |-> $i_0
-j |-> $j_1
-
-Note that the execution was symbolic.
-Path condition: ($i_0<=$a_0.size()) && forall $j_1 : int :: ((0<=$j_1)&&($j_1<$i_0)) ==> ($minim_0<=$a_0[$j_1]) && !($i_0<$a_0.size()) ($j_0 : int, $i_0 : int, $j_1 : int, $minim_0 : int, $a_0 : array<int>)
-
-Can't use return outside function scope.
-a |-> $a_0
-[result] |-> $minim_0
-minim |-> $minim_0
-i |-> $i_0
-j |-> $j_1
-
-Note that the execution was symbolic.
-Path condition: ($i_0<=$a_0.size()) && forall $j_1 : int :: ((0<=$j_1)&&($j_1<$i_0)) ==> ($minim_0<=$a_0[$j_1]) && !($i_0<$a_0.size()) ($j_0 : int, $i_0 : int, $j_1 : int, $minim_0 : int, $a_0 : array<int>)
-
-Successfully verified: findMin
 a |-> $a
+slp |-> $slp_0
+i |-> $i_1
 
 Note that the execution was symbolic.
-Path condition: forall $j_4 : int :: ((0<=$j_4)&&($j_4<$a.size())) ==> ($[result]_0<=$a[$j_4]) && exists $j_5 : int :: ((0<=$j_5)&&($j_5<$a.size())) ==> ($[result]_0==$a[$j_5]) ($[result]_0 : int, $j_4 : int, $a : array<int>, $j_5 : int)
+Note that the Z3 engine was used for verification!
+Path condition: 
+   forall $i_0 : int :: ((0<=$i_0)&&($i_0<($a.size()-1))) ==> ($a[$i_0]<=$a[($i_0+1)]) &&
+   ($slp_0<=$i_1) &&
+   forall $k_1 : int :: forall $l_1 : int :: ((((0<=$k_1)&&($k_1<=$l_1))&&($l_1<$i_1))&&($a[$k_1]==$a[$l_1])) ==> (($l_1-$k_1)<=$slp_0) &&
+   !($i_1<$a.size())
+Type constraints: 
+   $slp_0 : int
+   $i_1 : int
+   $a : array<int>
 

src/main/java/ast/ASTHelper.java

@@ -12,7 +12,8 @@ public static List<FunctionDeclAST> getFunctions(AST root)
         List<FunctionDeclAST> lst = new ArrayList<>();
         ASTVisitor<List<FunctionDeclAST>> visitor = new ASTVisitor<>(lst);
         visitor.register((tree) -> tree instanceof FunctionDeclAST, (tree, payload) -> {
-            payload.add((FunctionDeclAST) tree);
+            if (!((FunctionDeclAST) tree).getEnsures().isEmpty())
+                payload.add((FunctionDeclAST) tree);
         });
         visitor.visit(root);
         return lst;

src/main/java/ast/ASTStack.java

@@ -88,7 +88,15 @@ private Result<?> makeStep()
             if (!stack.empty())
             {
                 top = stack.peek();
-                top.assign(result);
+                try
+                {
+                    top.assign(result);
+                }
+                catch (InternalException e)
+                {
+                    top.handle(e);
+                    return null;
+                }
             }
         }
         else

src/main/java/execution/Execution.java

@@ -7,6 +7,7 @@
 import ast.enums.ParamType;
 import ast.expr.SymIDAST;
 import ast.stmt.FunctionDeclAST;
+import ast.type.DataTypeAST;
 import execution.exhaustive.EnvironmentMapper;
 import execution.helpers.AnnoHelper;
 import execution.parser.env.*;
@@ -204,7 +205,25 @@ private void execute()
             if (config.hasStaticVerif())
             {
                 config.getIOManager().write("Note that the execution was symbolic.");
-                config.getIOManager().write("Path condition: " + conditionPath.toString());
+                if (conditionPath.verifies())
+                {
+                    config.getIOManager().write("Note that the " + config.getProver() + " engine was used for verification.");
+                }
+                config.getIOManager().write("Path condition: \n" + conditionPath.toString(3));
+                config.getIOManager().write("Type constraints: ");
+                Map<String, DataTypeAST> typesConstraints = conditionPath.getIdTypes(false);
+                StringBuilder sb = new StringBuilder();
+                for (int j=0; j < 3; j++)
+                {
+                    sb.append(" ");
+                }
+                List<String> types = new ArrayList<>();
+                for (Map.Entry<String, DataTypeAST> entry : typesConstraints.entrySet())
+                {
+                    types.add(entry.getKey() + " : " + entry.getValue());
+                }
+                sb.append(String.join("\n   ", types));
+                config.getIOManager().write(sb.toString());
                 config.getIOManager().write("");
             }
         }

src/main/java/execution/interpreter/SymbolicStatefulStmtInterpreter.java

@@ -1,6 +1,7 @@
 package execution.interpreter;
 
 import ast.AST;
+import ast.stmt.FunctionDeclAST;
 import execution.ExecutionPayload;
 import execution.ExecutionResult;
 import execution.exhaustive.SplitMapper;
@@ -84,6 +85,11 @@ public ExecutionState interpretForEach(AST ast, ExecutionPayload payload)
     @Override
     public ExecutionState interpretFunctionDecl(AST ast, ExecutionPayload payload)
     {
+        if (ast instanceof FunctionDeclAST && ((FunctionDeclAST) ast).getEnsures().isEmpty())
+        {
+            return baseDelegate.interpretFunctionDecl(ast, payload);
+        }
+
         return new ExecutionState(ast, payload)
         {
             @Override

src/main/java/execution/state/expression/IterableWithFilterSpecState.java

@@ -66,6 +66,7 @@ public ExecutionState makeStep()
         if (step == source.size())
         {
             setResult(new ExecutionResult(iterableValue));
+            getExec().deregisterEnv(env);
             return null;
         }
 

src/main/java/execution/state/expression/IterableWithMapSpecState.java

@@ -64,6 +64,7 @@ public ExecutionState makeStep()
         if (step == source.size())
         {
             setResult(new ExecutionResult(iterableValue));
+            getExec().deregisterEnv(env);
             return null;
         }
 

src/main/java/execution/state/function/DefinedFunctionCallState.java

@@ -89,6 +89,7 @@ public ExecutionState makeStep()
             return request(function.getBody(), env);
         }
 
+        getExec().deregisterEnv(env);
         return null;
     }