Merge #848

848: partial fix for #819 r=vakaras a=Pointerbender

In issue #819 the `prusti-tests/tests/verify/pass/arrays/selection_sort.rs` test was entirely disabled in anticipation of some future fixes. Those future fixes have not landed yet, but PRs #831 and #844 opened a window for a temporary work-around. I was curious if I could get it to work and was able to achieve a stable test run for `selection_sort` (consistently finishes in under 60 seconds on my PC). 

The changes I made were to selectively disable the `fix_quantifiers` and `optimize_folding` optimization passes and use wrapper functions for array accesses instead of using array indices directly (those are blocked by #812 for now).

I don't consider this a proper fix for #819, but I think it could still be a nice regression test and now that its execution time has stabilized I think it's safe to turn back on. Let's keep #819 open to track implementing a proper fix in the future.

Co-authored-by: Pointerbender <[email protected]>

prusti-tests/tests/verify/pass/arrays/selection_sort.rs

@@ -1,12 +1,16 @@
-// ignore-test: FIXME performance issue, see https://github.com/viperproject/prusti-dev/issues/819
-// compile-flags: -Pverification_deadline=180
+// FIXME performance issue, see https://github.com/viperproject/prusti-dev/issues/819
+// disabled `fix_quantifiers` and `optimize_folding` optimizations for now:
+// compile-flags: -Poptimizations=inline_constant_functions,delete_unused_predicates,remove_empty_if,purify_vars,remove_unused_vars,remove_trivial_assertions,clean_cfg -Pverification_deadline=180
 
 use prusti_contracts::*;
 
 fn main() {}
 
 
-fn selection_sort(mut a: [i32; 10]) {
+#[ensures(forall(|k1: usize, k2: usize|(0 <= k1 && k1 < k2 && k2 < 10)
+    ==> (get(a, k1) <= get(a, k2)),
+    triggers=[(get(a, k1),get(a, k2),)]))]
+fn selection_sort(a: &mut [i32; 10]) {
     let mut min;
     let mut i = 0;
 
@@ -15,61 +19,66 @@ fn selection_sort(mut a: [i32; 10]) {
 
         // sorted below i
         body_invariant!(forall(|k1: usize, k2: usize| (0 <= k1 && k1 < k2 && k2 < i)
-                               ==> a[k1] <= a[k2]));
+                                ==> get(a, k1) <= get(a, k2),
+                                triggers=[(get(a, k1),get(a, k2))]));
         // all below i are smaller than all above i
         body_invariant!(forall(|k1: usize, k2: usize| (0 <= k1 && k1 < i && i <= k2 && k2 < 10)
-                               ==> a[k1] <= a[k2]));
+                                ==> get(a, k1) <= get(a, k2),
+                                triggers=[(get(a, k1),get(a, k2))]));
 
         min = i;
         let mut j = i+1;
+
         while j < a.len() {
             // these three are the same as the outer loop
             body_invariant!(0 <= i && i < 10);
             body_invariant!(forall(|k1: usize, k2: usize| (0 <= k1 && k1 < k2 && k2 < i)
-                                   ==> a[k1] <= a[k2]));
+                                    ==> get(a, k1) <= get(a, k2),
+                                    triggers=[(get(a, k1),get(a, k2))]));
             body_invariant!(forall(|k1: usize, k2: usize| (0 <= k1 && k1 < i && i <= k2 && k2 < 10)
-                                   ==> a[k1] <= a[k2]));
+                                    ==> get(a, k1) <= get(a, k2),
+                                    triggers=[(get(a, k1),get(a, k2))]));
 
             // these are new
             body_invariant!(i < j && j < 10);
             body_invariant!(i <= min && min < 10);
             // all previously sorted are smaller than the current min
-            body_invariant!(forall(|k: usize| (0 <= k && k < i) ==> a[k] <= a[min]));
+            body_invariant!(forall(|k: usize| (0 <= k && k < i)
+                                    ==> get(a, k) <= get(a, min),
+                                    triggers=[(get(a, k))]));
 
             // all not-yet-sorted that we checked yet are bigger than the current min
             body_invariant!(forall(|k: usize| (i <= k && k < j && k < 10)
-                                   ==> a[min] <= a[k]));
+                                    ==> get(a, min) <= get(a, k),
+                                    triggers=[(get(a, k))]));
 
-            if a[j] < a[min] {
+            if get(a, j) < get(a, min) {
                 min = j;
             }
 
             j += 1;
         }
 
-        // let a_i = a[i];
-        // let a_min = a[min];
-        // a[i] = a_min;
-        // a[min] = a_i;
-        set_a(&mut a, i, min);
+        let a_i = get(a, i);
+        let a_min = get(a, min);
+        set(a, i,  a_min);
+        set(a, min, a_i);
 
         i += 1;
     }
 }
 
-#[requires(i < 10)]
-#[requires(min < 10)]
-#[requires(i <= min)]
-#[requires(forall(|k1: usize, k2: usize| (0 <= k1 && k1 < k2 && k2 < i) ==> a[k1] <= a[k2]))]
-#[requires(forall(|k1: usize, k2: usize| (0 <= k1 && k1 < i && i <= k2 && k2 < 10) ==> a[k1] <= a[k2]))]
-#[ensures(forall(|k1: usize| (0 <= k1 && k1 < 10 && k1 != i && k1 != min) ==> (a[k1] == old(a[k1]))))]
-#[ensures(a[i] == old(a[min]))]
-#[ensures(a[min] == old(a[i]))]
-#[ensures(forall(|k1: usize, k2: usize| (0 <= k1 && k1 < k2 && k2 <= i) ==> a[k1] <= a[k2]))]
-#[ensures(forall(|k1: usize, k2: usize| (0 <= k1 && k1 < i && i <= k2 && k2 < 10) ==> a[k1] <= a[k2]))]
-fn set_a(a: &mut [i32; 10], i: usize, min: usize) {
-    let a_i = a[i];
-    let a_min = a[min];
-    a[i] = a_min;
-    a[min] = a_i;
+// FIXME: replace all instances of get/set with array indices when #812 is fixed https://github.com/viperproject/prusti-dev/issues/812
+
+#[pure]
+#[requires(0 <= i && i < 10)]
+const fn get(a: &[i32; 10], i: usize) -> i32 {
+    a[i]
+}
+
+#[requires(0 <= i && i < 10)]
+#[ensures(forall(|j: usize| (0 <= j && j < 10 && j != old(i)) ==> (get(a, j) == old(get(a, j))), triggers=[(get(a, j),)]))]
+#[ensures(get(a, old(i)) == old(v))]
+fn set(a: &mut [i32; 10], i: usize, v: i32) {
+    a[i] = v;
 }

prusti-tests/tests/verify/pass/slices/slice-split.rs

@@ -1,4 +1,4 @@
-// compile-flags: -Pverification_deadline=20
+// compile-flags: -Pverification_deadline=25
 
 use prusti_contracts::*;