Partially reinstate problem fail tests

examples/known-problems/others/DuplicateFieldName.java → examples/fixed-known-problems/DuplicateFieldName.java

@@ -1,6 +1,5 @@
 // -*- tab-width:4 ; indent-tabs-mode:nil -*-
 //:: cases DuplicateFieldName
-//:: suite problem-fail
 //:: tools silicon
 //:: verdict Pass
 
@@ -9,11 +8,15 @@
 public class A {
   int i;
 
+  //@ requires Perm(i, write);
   public void main() {
     B b = new B();
+    i = 3;
+    //@ assert i == 3;
 
-    b.testA()/*@ with {a = 9;} @*/;
-    b.testI()/*@ with {i = 9;} @*/;
+    b.testA()/*@ with { a = 9; } @*/;
+    b.testI()/*@ with { i = 9; } @*/;
+    //@ assert i == 3;
   }
 }
 
@@ -26,6 +29,7 @@ public void testA() {
 
   /*@
     given int i;
+    requires i == 9;
   @*/
   public void testI() {
   }

examples/fixed-known-problems/ParallelGCD.pvl

@@ -0,0 +1,93 @@
+//:: case ParallelGCD
+//:: tool silicon
+//:: option --check-history
+//:: verdict Pass
+
+class `Future` {
+  int x, y;
+
+  accessible x;
+  modifies y;
+  requires x > 0 && y > x;
+  ensures  y == \old(y) - \old(x);
+  process decr_y();
+
+  modifies x;
+  accessible y;
+  requires x > y && y > 0;
+  ensures  x == \old(x) - \old(y);
+  process decr_x();
+
+  accessible x;
+  accessible y;
+  requires x==y;
+  process done();
+
+  requires x > 0 && y > 0;
+  ensures  x == y && y == ParallelGCD.gcd(\old(x), \old(y));
+  process gcd() = tx() || ty();
+
+  process tx() = decr_x() * tx() + done();
+  process ty() = decr_y() * ty() + done();
+}
+
+class ParallelGCD {
+  requires a > 0 ** b > 0;
+  static int gcd(int a, int b) = a == b ? a : (a > b ? gcd(a - b, b) : gcd(a, b - a));
+
+  requires x > 0 ** y > 0 ;
+  ensures  \result == gcd(x,y);
+  int gcd2(int x, int y){
+    `Future` F = new `Future`();
+    F.x =x;
+    F.y =y;
+    create F, F.gcd();
+    split  F, 1\2, F.tx(), 1\2, F.ty();
+
+    invariant inv(HPerm(F.x,write) ** HPerm(F.y,write) ** F.x > 0 ** F.y > 0){
+      par T0()
+        requires Future(F, 1\2, F.tx());
+        ensures Future(F, 1\2, empty);
+      {
+        boolean run = true;
+        loop_invariant run? Future(F, 1\2, F.tx()) : Future(F, 1\2, empty);
+        while(run) {
+          atomic(inv){
+            if(F.x > F.y){
+              choose F, 1\2, F.tx(), F.decr_x() * F.tx();
+              action(F, 1\2, F.tx(), F.decr_x()){ F.x = F.x - F.y; }
+            }
+            if(F.x == F.y){
+              choose F, 1\2, F.tx(), F.done();
+              action(F, 1\2, empty, F.done()){ run = false; }
+        } } }
+      } and T1()
+        requires Future(F, 1\2, F.ty());
+        ensures Future(F, 1\2, empty);
+      {
+        boolean run = true;
+        loop_invariant run ? Future(F, 1\2, F.ty()) : Future(F, 1\2, empty);
+        while (run) {
+          atomic(inv) {
+            if (F.y>F.x)
+            {
+              choose F, 1\2, F.ty(), F.decr_y() * F.ty();
+              action(F, 1\2, F.ty(), F.decr_y()){
+                F.y = F.y - F.x;
+              }
+            }
+            if(F.x == F.y){
+              choose F, 1\2, F.ty(), F.done();
+              action(F, 1\2, empty, F.done()){
+                run = false;
+              }
+            }
+          }
+        }
+      }
+    }
+    merge F, 1\2, empty, 1\2, empty;
+    destroy F;
+    return F.x;
+  }
+}

examples/known-problems/others/array-problem.pvl → examples/fixed-known-problems/array-problem.pvl

@@ -1,15 +1,8 @@
-// -*- tab-width:2 ; indent-tabs-mode:nil -*-
-
 //:: cases ArrayProblemFull
-//:: suite problem-fail
 //:: tools silicon
 //:: verdict Pass
 
-// :: cases ArrayProblemGood
-// :: suite problem-pass
-// :: tools silicon
-// :: verdict Pass
-// :: options --skip problem
+// Used to be failing because of https://github.com/viperproject/silicon/issues/512, but fixed by now
 
 class Problem {
 
@@ -68,7 +61,7 @@ class Problem {
     assert xs==seq<int>{1,2};  
   }
 
-  void problem(){
+  void working_too_too(){
     int[] array=new int[2];
     array[0]=1;
     array[1]=2;
@@ -81,7 +74,7 @@ class Problem {
 
     assert (\forall int i ; 0 <= i && i < 2 ; xs[i]==array[i]);
 
-    assert xs==seq<int>{1,2};  
+    assert xs==seq<int>{1,2};
   }
 
 }

examples/fixed-known-problems/rewriterIssue6.pvl

@@ -0,0 +1,26 @@
+//:: cases RW6
+//:: tools silicon
+//:: verdict Pass
+
+// this test shows an example of a bug in VerCors. It is (to be) included in the test-suite to make sure we don't prove any nonsense
+// The listed verdict is what sound behavior should be.
+
+// The bug incompleteness: the forall in the contract below does not have a proper trigger.
+// By adding id(y) around y a trigger is allowed (id(y)), so viper can instantiatie the forall.
+// This might be a bad solution in a bigger example: id(y) can probably occur in lots of places, so it might slow
+// down verification.
+
+class rewriterIssue {
+  int x;
+
+  pure int myId(int i) {
+    return i;
+  }
+
+  // assume something identical to what we ensure
+  context (\forall int y;(i + 1) * i <= y && y < (i+1) * (i+1); myId(y) == i);
+  // It passes because of myId(y). Just "y" would not be verifiable.
+  void m(int i){
+  }
+}
+

examples/known-problems/carp/histogram-matrix.c

@@ -1,40 +1,50 @@
-// -*- tab-width:2 ; indent-tabs-mode:nil -*-
 //:: cases HistogramMatrix
-//:: suite problem-fail
+//:: suite problem-partial
 //:: tools silicon
 //:: verdict Pass
+//:: option --stop-before-backend
 
 // PB: I believe this example is incorrectly automatically paralellized, after
 // which of course there is insufficient permission to write to hist. Then again,
 // I'm not sure what then the point of the iteration contract style was for this
 // example, then.
 
-//begin(all)
 /*@
   given seq<seq<int> > data;
   context_everywhere M>0 ** N>0 ** P>0;
   context_everywhere |data| == M;
-  context_everywhere (\forall int d; 0 <= d && d < M; |data[d]| == N);
+  context_everywhere (\forall int d = 0 .. M; |data[d]| == N);
 
   context \pointer(matrix, M, 1\2);
-  context (\forall* int i; 0 <= i < M; (\forall* int j; 0 <= j < N; Perm(matrix[i][j], 1\2)));
+  context (\forall* int i = 0 .. M; (\forall* int j = 0 .. N; Perm(matrix[i][j], 1\2)));
   context \pointer(hist, P, write);
 
-  context (\forall int i1=0 .. M ; (\forall int j1=0 .. N ; matrix[i1][j1] == data[i1][j1] ));
-  context (\forall int i1=0 .. M ; (\forall int j1=0 .. N ; 0 <= matrix[i1][j1] < P));
-  ensures (\forall int k=0 .. P ; hist[k]==(\sum int i1 ; 0 <= i1 && i1 < M ;
-              (\sum int j1 ; 0 <= j1 && j1 < N ; data[i1][j1]==k?1:0)));
-  ensures (\forall int i1=0 .. M ; (\forall int j1=0 .. N ;  //skip(all)
-              matrix[i1][j1]==\old(matrix[i1][j1])));        //skip(all)
-@*/ void histogram(int M,int N,int matrix[M][N],int P,int hist[P]){
-  for(int k=0;k<P;k++)/*@ context hist != NULL ** Perm(hist[k],write); ensures hist[k]==0; @*/ { hist[k]=0; }
+  context (\forall int i1 = 0 .. M ; (\forall int j1 = 0 .. N; matrix[i1][j1] == data[i1][j1] ));
+  context (\forall int i1 = 0 .. M ; (\forall int j1 = 0 .. N; 0 <= matrix[i1][j1] && matrix[i1][j1] < P));
+  ensures (\forall int k = 0 .. P ; hist[k] == (\sum int i1; 0 <= i1 && i1 < M ;
+              (\sum int j1 ; 0 <= j1 && j1 < N ; data[i1][j1] == k ? 1 : 0)));
+  ensures (\forall int i1 = 0 .. M ; (\forall int j1=0 .. N;
+              matrix[i1][j1]==\old(matrix[i1][j1])));
+@*/
+void histogram(int M,int N,int matrix[M][N],int P,int hist[P]){
+  for(int k=0;k<P;k++)
+  /*@ context hist != NULL ** Perm(hist[k],write);
+      ensures hist[k]==0; @*/
+  {
+    hist[k]=0;
+  }
   for(int i=0;i<M;i++){
-    for(int j=0;j<N;j++) /*@
+    for(int j=0;j<N;j++)
+    /*@
       context hist != NULL && matrix != NULL;
       context Perm(hist[matrix[i][j]], write);
       requires (\forall* int k=0 .. P ; Reducible(hist[k],+));
-      context Perm(matrix[i][j],1\4) ** 0 <= matrix[i][j] < P ;
+      context Perm(matrix[i][j], 1\4) ** 0 <= matrix[i][j] ** matrix[i][j] < P ;
       context matrix[i][j] == data[i][j];
-      ensures (\forall* int k=0 .. P ; Contribution(hist[k],data[i][j]==k?1:0));
-    @*/ { hist[matrix[i][j]]+=1; } } }
-//end(all)
+      ensures (\forall* int k = 0 .. P ; Contribution(hist[k],data[i][j] == k ? 1 : 0));
+    @*/
+    {
+      hist[matrix[i][j]]+=1;
+    }
+  }
+}

examples/known-problems/carp/zero-sub-matrix-par.c

@@ -1,7 +1,5 @@
-// -*- tab-width:2 ; indent-tabs-mode:nil -*-
 //:: cases ZeroSubMatrixPar-C
 //:: tools silicon
-//:: suite problem-fail
 //:: verdict Pass
 
 /*@
@@ -33,7 +31,7 @@ void zero(int M,int N,int step,int matrix[M][step]){
     for(int j=0;j<N;j++)
     /*@
       requires matrix != NULL;
-      context Perm(matrix[i],1/N);
+      context Perm(matrix[i],1\N);
       context Perm(matrix[i][j], write);
       ensures matrix[i][j] == 0;
     @*/

examples/known-problems/domains/float.sil

@@ -1,7 +1,5 @@
-// -*- tab-width:2 ; indent-tabs-mode:nil -*-
 //:: case FloatDomain
 //:: tools silicon
-//:: suite problem-fail
 //:: verdict Pass
 
 domain Float {
@@ -54,8 +52,8 @@ method test(xs : Seq[Float]) {
 
 
     while(i<|xs|)
-      context_everywhere 0 <= i && i <= |xs|
-      context_everywhere S == fsum(xs[0..i])
+      invariant 0 <= i && i <= |xs|
+      invariant S == fsum(xs[0..i])
     {
       assert xs[0..i+1]==xs[0..i]++xs[i..i+1]
       //assert fsum(xs[0..i+1])==fadd(fsum(xs[0..i]),fsum(xs[i..i+1]))

examples/known-problems/futures/elect.pvl

@@ -1,9 +1,12 @@
 // -*- tab-width:2 ; indent-tabs-mode:nil -*-
 //:: case LeaderElect
 //:: tool silicon
-//:: option --check-history
+//:: options --check-history --stop-before-backend
+//:: suite problem-partial
 //:: verdict Pass
 
+// This files verification results are unstable. See https://github.com/utwente-fmt/vercors/issues/514
+
 class `Future` {
 
 	/* ** Communication primitives */