interp: improved bench

examples/euler001.mlw

@@ -171,6 +171,9 @@ module Euler001
   let run () = solve 1000
     (* should return 233168 *)
 
-  let bench () = if run () <> 233168 then absurd
+    exception BenchFailure
+
+  let bench () raises { BenchFailure -> true } =
+    if run () <> 233168 then raise BenchFailure
 
 end

examples/euler002.mlw

@@ -152,6 +152,9 @@ module Solve
 
   let run () = f 4000000 (* should be 4613732 *)
 
-  let bench () = if run () <> 4613732 then absurd
+  exception BenchFailure
+
+  let bench () raises { BenchFailure -> true } =
+    if run () <> 4613732 then raise BenchFailure
 
 end

examples/fibonacci.mlw

@@ -151,9 +151,11 @@ module FibonacciLogarithmic
   let test42 () = fibo 42
   let test2014 () = fibo 2014
 
-  let bench () =
-    if test42 () <> 267914296 then absurd;
+  exception BenchFailure
+
+  let bench () raises { BenchFailure -> true } =
+    if test42 () <> 267914296 then raise BenchFailure;
     if test2014 () <> 3561413997540486142674781564382874188700994538849211456995042891654110985470076818421080236961243875711537543388676277339875963824466334432403730750376906026741819889036464401788232213002522934897299928844192803507157647764542466327613134605502785287441134627457615461304177503249289874066244145666889138852687147544158443155204157950294129177785119464446668374163746700969372438526182906768143740891051274219441912520127
-    then absurd
+    then raise BenchFailure
 
 end

examples/insertion_sort.mlw

@@ -40,23 +40,25 @@ module InsertionSort
     insertion_sort a;
     a
 
-  let test2 () =
+  let test2 () ensures { result.length = 8 } =
     let a = make 8 0 in
     a[0] <- 53; a[1] <- 91; a[2] <- 17; a[3] <- -5;
     a[4] <- 413; a[5] <- 42; a[6] <- 69; a[7] <- 6;
     insertion_sort a;
     a
 
-  let bench () =
+  exception BenchFailure
+
+  let bench () raises { BenchFailure -> true } =
     let a = test2 () in
-    if a[0] <> -5 then absurd;
-    if a[1] <> 6 then absurd;
-    if a[2] <> 17 then absurd;
-    if a[3] <> 42 then absurd;
-    if a[4] <> 53 then absurd;
-    if a[5] <> 69 then absurd;
-    if a[6] <> 91 then absurd;
-    if a[7] <> 413 then absurd
+    if a[0] <> -5 then raise BenchFailure;
+    if a[1] <> 6 then raise BenchFailure;
+    if a[2] <> 17 then raise BenchFailure;
+    if a[3] <> 42 then raise BenchFailure;
+    if a[4] <> 53 then raise BenchFailure;
+    if a[5] <> 69 then raise BenchFailure;
+    if a[6] <> 91 then raise BenchFailure;
+    if a[7] <> 413 then raise BenchFailure
 
 end
 

examples/knuth_prime_numbers.mlw

@@ -62,6 +62,7 @@ module PrimeNumbers
 
   let prime_numbers (m: int)
     requires { m >= 2 }
+    ensures  { result.length = m }
     ensures  { first_primes result m }
   = let p = make m 0 in
     p[0] <- 2;
@@ -93,8 +94,10 @@ module PrimeNumbers
     done;
     p
 
-  let bench () =
+  exception BenchFailure
+
+  let bench () raises { BenchFailure -> true } =
      let t = prime_numbers 20 in
-     if t[0] <> 2 then absurd
+     if t[0] <> 2 then raise BenchFailure
 
 end

examples/same_fringe.mlw

@@ -72,7 +72,10 @@ module SameFringe
   let test4 () = same_fringe (Node (leaf a) b Empty) (Node Empty a (leaf b))
   let test5 () = same_fringe (Node (leaf a) b Empty) (Node Empty b (leaf a))
 
-  let bench () = if not (test4 ()) then absurd
+  exception BenchFailure
+
+  let bench () raises { BenchFailure -> true } =
+    if not (test4 ()) then raise BenchFailure
 
 end
 

examples/same_fringe/why3session.xml

@@ -7,6 +7,10 @@
   version="0.95.1"/>
  <prover
   id="1"
+  name="Alt-Ergo"
+  version="0.95.2"/>
+ <prover
+  id="2"
   name="CVC3"
   version="2.4.1"/>
  <file
@@ -131,7 +135,7 @@
        <result status="valid" time="0.02"/>
       </proof>
       <proof
-       prover="1"
+       prover="2"
        timelimit="10"
        memlimit="0"
        obsolete="false"
@@ -381,17 +385,37 @@
      <result status="valid" time="0.01"/>
     </proof>
    </goal>
+   <goal
+    name="WP_parameter bench"
+    locfile="../same_fringe.mlw"
+    loclnum="77" loccnumb="6" loccnume="11"
+    expl="VC for bench"
+    sum="9020315c47e71b0301c59e758be57eb8"
+    proved="true"
+    expanded="false"
+    shape="t">
+    <label
+     name="expl:VC for bench"/>
+    <proof
+     prover="1"
+     timelimit="5"
+     memlimit="4000"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.02"/>
+    </proof>
+   </goal>
   </theory>
   <theory
    name="Test"
    locfile="../same_fringe.mlw"
-   loclnum="77" loccnumb="7" loccnume="11"
+   loclnum="82" loccnumb="7" loccnume="11"
    verified="true"
    expanded="true">
    <goal
     name="WP_parameter test1"
     locfile="../same_fringe.mlw"
-    loclnum="82" loccnumb="6" loccnume="11"
+    loclnum="87" loccnumb="6" loccnume="11"
     expl="VC for test1"
     sum="d37ebc1cd434eba73675a2913c7a3548"
     proved="true"
@@ -411,7 +435,7 @@
    <goal
     name="WP_parameter test2"
     locfile="../same_fringe.mlw"
-    loclnum="83" loccnumb="6" loccnume="11"
+    loclnum="88" loccnumb="6" loccnume="11"
     expl="VC for test2"
     sum="d37ebc1cd434eba73675a2913c7a3548"
     proved="true"
@@ -431,7 +455,7 @@
    <goal
     name="WP_parameter test3"
     locfile="../same_fringe.mlw"
-    loclnum="84" loccnumb="6" loccnume="11"
+    loclnum="89" loccnumb="6" loccnume="11"
     expl="VC for test3"
     sum="d37ebc1cd434eba73675a2913c7a3548"
     proved="true"
@@ -451,7 +475,7 @@
    <goal
     name="WP_parameter leaf"
     locfile="../same_fringe.mlw"
-    loclnum="89" loccnumb="6" loccnume="10"
+    loclnum="94" loccnumb="6" loccnume="10"
     expl="VC for leaf"
     sum="cb3d58a8e5a4cd2167042439af66c371"
     proved="true"
@@ -471,7 +495,7 @@
    <goal
     name="WP_parameter test4"
     locfile="../same_fringe.mlw"
-    loclnum="91" loccnumb="6" loccnume="11"
+    loclnum="96" loccnumb="6" loccnume="11"
     expl="VC for test4"
     sum="cb3d58a8e5a4cd2167042439af66c371"
     proved="true"
@@ -491,7 +515,7 @@
    <goal
     name="WP_parameter test5"
     locfile="../same_fringe.mlw"
-    loclnum="92" loccnumb="6" loccnume="11"
+    loclnum="97" loccnumb="6" loccnume="11"
     expl="VC for test5"
     sum="cb3d58a8e5a4cd2167042439af66c371"
     proved="true"

examples/selection_sort.mlw

@@ -36,22 +36,24 @@ module SelectionSort
     selection_sort a;
     a
 
-  let test2 () =
+  let test2 () ensures { result.length = 8 } =
     let a = make 8 0 in
     a[0] <- 53; a[1] <- 91; a[2] <- 17; a[3] <- -5;
     a[4] <- 413; a[5] <- 42; a[6] <- 69; a[7] <- 6;
     selection_sort a;
     a
 
-  let bench () =
+  exception BenchFailure
+
+  let bench () raises { BenchFailure -> true } =
     let a = test2 () in
-    if a[0] <> -5 then absurd;
-    if a[1] <> 6 then absurd;
-    if a[2] <> 17 then absurd;
-    if a[3] <> 42 then absurd;
-    if a[4] <> 53 then absurd;
-    if a[5] <> 69 then absurd;
-    if a[6] <> 91 then absurd;
-    if a[7] <> 413 then absurd
+    if a[0] <> -5 then raise BenchFailure;
+    if a[1] <> 6 then raise BenchFailure;
+    if a[2] <> 17 then raise BenchFailure;
+    if a[3] <> 42 then raise BenchFailure;
+    if a[4] <> 53 then raise BenchFailure;
+    if a[5] <> 69 then raise BenchFailure;
+    if a[6] <> 91 then raise BenchFailure;
+    if a[7] <> 413 then raise BenchFailure
 
 end

examples/vacid_0_sparse_array.mlw

@@ -132,18 +132,20 @@ module Harness
     let get_b_0 = get b 0 in assert { get_b_0 = default };
     ()
 
-  let bench () =
+  exception BenchFailure
+
+  let bench () raises { BenchFailure -> true } =
     let a = create 10 default in
     let b = create 20 default in
-    if get a 5 <> default then absurd;
-    if get b 7 <> default then absurd;
+    if get a 5 <> default then raise BenchFailure;
+    if get b 7 <> default then raise BenchFailure;
     set a 5 c1;
     set b 7 c2;
-    if get a 5 <> c1 then absurd;
-    if get b 7 <> c2 then absurd;
-    if get a 7 <> default then absurd;
-    if get b 5 <> default then absurd;
-    if get a 0 <> default then absurd;
-    if get b 0 <> default then absurd
+    if get a 5 <> c1 then raise BenchFailure;
+    if get b 7 <> c2 then raise BenchFailure;
+    if get a 7 <> default then raise BenchFailure;
+    if get b 5 <> default then raise BenchFailure;
+    if get a 0 <> default then raise BenchFailure;
+    if get b 0 <> default then raise BenchFailure
 
 end

examples/vacid_0_sparse_array/why3session.xml

@@ -7,14 +7,18 @@
   version="0.95.1"/>
  <prover
   id="1"
+  name="Alt-Ergo"
+  version="0.95.2"/>
+ <prover
+  id="2"
   name="CVC3"
   version="2.4.1"/>
  <prover
-  id="2"
+  id="3"
   name="Coq"
   version="8.4pl2"/>
  <prover
-  id="3"
+  id="4"
   name="Z3"
   version="3.2"/>
  <file
@@ -96,7 +100,7 @@
     expanded="false"
     shape="ais_eltV0V1Iainfix &lt;V1alengthV0Aainfix &lt;=c0V1FIainfix =acardV0alengthV0Iainfix =amixfix []aindexV0amixfix []abackV0V2V2Aainfix &lt;amixfix []abackV0V2alengthavaluesV0Aainfix &lt;=c0amixfix []abackV0V2Iainfix &lt;V2acardV0Aainfix &lt;=c0V2FAainfix =alengthaindexV0alengthabackV0Aainfix =alengthavaluesV0alengthaindexV0Aainfix &lt;=alengthavaluesV0amaxlenAainfix &lt;=acardV0alengthavaluesV0Aainfix &lt;=c0acardV0F">
     <proof
-     prover="2"
+     prover="3"
      timelimit="5"
      memlimit="1000"
      edited="vacid_0_sparse_array_2_SparseArray_permutation_1.v"
@@ -220,7 +224,7 @@
        <result status="unknown" time="0.52"/>
       </proof>
       <proof
-       prover="1"
+       prover="2"
        timelimit="5"
        memlimit="1000"
        obsolete="false"
@@ -228,7 +232,7 @@
        <result status="valid" time="0.09"/>
       </proof>
       <proof
-       prover="3"
+       prover="4"
        timelimit="5"
        memlimit="1000"
        obsolete="false"
@@ -288,7 +292,7 @@
       <label
        name="expl:VC for set"/>
       <proof
-       prover="1"
+       prover="2"
        timelimit="17"
        memlimit="1000"
        obsolete="false"
@@ -296,7 +300,7 @@
        <result status="valid" time="0.05"/>
       </proof>
       <proof
-       prover="3"
+       prover="4"
        timelimit="17"
        memlimit="1000"
        obsolete="false"
@@ -399,7 +403,7 @@
          <result status="unknown" time="1.30"/>
         </proof>
         <proof
-         prover="1"
+         prover="2"
          timelimit="17"
          memlimit="1000"
          obsolete="false"
@@ -407,7 +411,7 @@
          <result status="valid" time="0.74"/>
         </proof>
         <proof
-         prover="3"
+         prover="4"
          timelimit="17"
          memlimit="1000"
          obsolete="false"
@@ -466,6 +470,26 @@
      <result status="valid" time="2.34"/>
     </proof>
    </goal>
+   <goal
+    name="WP_parameter bench"
+    locfile="../vacid_0_sparse_array.mlw"
+    loclnum="137" loccnumb="6" loccnume="11"
+    expl="VC for bench"
+    sum="0b932ae6e0b14ac60ad8732b7e96429e"
+    proved="true"
+    expanded="false"
+    shape="ainfix &lt;c0V9Aainfix &lt;=c0c0Iainfix =avalueV22c0adefaultAainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix =avalueV27c5adefaultAainfix &lt;c5V9Aainfix &lt;=c0c5Iainfix =avalueV22c7adefaultAainfix &lt;c7V0Aainfix &lt;=c0c7Iainfix =avalueV27c7ac2Aainfix &lt;c7V9Aainfix &lt;=c0c7Iainfix =avalueV22c5ac1Aainfix &lt;c5V0Aainfix &lt;=c0c5Iainfix =avalueV27V28avalueV17V28INainfix =V28c7FAainfix =avalueV27c7ac2Aainfix &lt;=c0V13Aainfix &lt;=c0V11Aainfix &lt;=c0V9Aainfix =agetV25agetV24V29V29Aainfix &lt;agetV24V29V9Aainfix &lt;=c0agetV24V29Iainfix &lt;V29V23Aainfix &lt;=c0V29FAainfix =V11V13Aainfix =V9V11Aainfix &lt;=V9amaxlenAainfix &lt;=V23V9Aainfix &lt;=c0V23Lamk sparse_arrayamk arrayV9V26amk arrayV11V25amk arrayV13V24V23V16FAainfix &lt;c7V9Aainfix &lt;=c0c7Iainfix =avalueV22V30avalueV8V30INainfix =V30c5FAainfix =avalueV22c5ac1Aainfix &lt;=c0V4Aainfix &lt;=c0V2Aainfix &lt;=c0V0Aainfix =agetV20agetV19V31V31Aainfix &lt;agetV19V31V0Aainfix &lt;=c0agetV19V31Iainfix &lt;V31V18Aainfix &lt;=c0V31FAainfix =V2V4Aainfix =V0V2Aainfix &lt;=V0amaxlenAainfix &lt;=V18V0Aainfix &lt;=c0V18Lamk sparse_arrayamk arrayV0V21amk arrayV2V20amk arrayV4V19V18V7FAainfix &lt;c5V0Aainfix &lt;=c0c5Iainfix =avalueV17c7adefaultAainfix &lt;c7V9Aainfix &lt;=c0c7Iainfix =avalueV8c5adefaultAainfix &lt;c5V0Aainfix &lt;=c0c5Iainfix =V9c20Aainfix =V16adefaultAainfix =V15c0Aainfix &lt;=c0V13Aainfix &lt;=c0V11Aainfix &lt;=c0V9Aainfix =agetV12agetV14V32V32Aainfix &lt;agetV14V32V9Aainfix &lt;=c0agetV14V32Iainfix &lt;V32V15Aainfix &lt;=c0V32FAainfix =V11V13Aainfix =V9V11Aainfix &lt;=V9amaxlenAainfix &lt;=V15V9Aainfix &lt;=c0V15Lamk sparse_arrayamk arrayV9V10amk arrayV11V12amk arrayV13V14V15V16FAainfix &lt;=c20amaxlenAainfix &lt;=c0c20Iainfix =V0c10Aainfix =V7adefaultAainfix =V6c0Aainfix &lt;=c0V4Aainfix &lt;=c0V2Aainfix &lt;=c0V0Aainfix =agetV3agetV5V33V33Aainfix &lt;agetV5V33V0Aainfix &lt;=c0agetV5V33Iainfix &lt;V33V6Aainfix &lt;=c0V33FAainfix =V2V4Aainfix =V0V2Aainfix &lt;=V0amaxlenAainfix &lt;=V6V0Aainfix &lt;=c0V6Lamk sparse_arrayamk arrayV0V1amk arrayV2V3amk arrayV4V5V6V7FAainfix &lt;=c10amaxlenAainfix &lt;=c0c10">
+    <label
+     name="expl:VC for bench"/>
+    <proof
+     prover="1"
+     timelimit="5"
+     memlimit="4000"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.06"/>
+    </proof>
+   </goal>
   </theory>
  </file>
 </why3session>

examples/verifythis_fm2012_LRS.mlw

@@ -177,11 +177,13 @@ let test () =
   check {x = 1}
 *)
 
-let bench () =
-  let arr = Array.make 4 0 in
-  arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5;
-  let x = lcp arr 1 2 in
-  if x <> 1 then absurd
+  exception BenchFailure
+
+  let bench () raises { BenchFailure -> true } =
+    let arr = Array.make 4 0 in
+    arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5;
+    let x = lcp arr 1 2 in
+    if x <> 1 then raise BenchFailure
 
 end
 
@@ -381,14 +383,16 @@ let test () =
   check {x = 0 (* TODO *)}
 *)
 
-let bench () =
-  let arr = Array.make 4 0 in
-  arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5;
-  let sa = create arr in
-  if sa.suffixes[0] <> 0 then absurd;
-  if sa.suffixes[1] <> 1 then absurd;
-  if sa.suffixes[2] <> 2 then absurd;
-  if sa.suffixes[3] <> 3 then absurd
+  exception BenchFailure
+
+  let bench () raises { BenchFailure -> true } =
+    let arr = Array.make 4 0 in
+    arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5;
+    let sa = create arr in
+    if sa.suffixes[0] <> 0 then raise BenchFailure;
+    if sa.suffixes[1] <> 1 then raise BenchFailure;
+    if sa.suffixes[2] <> 2 then raise BenchFailure;
+    if sa.suffixes[3] <> 3 then raise BenchFailure
 
 end
 

src/main.ml

@@ -600,14 +600,19 @@ let do_exec env fname cin exec =
               in
               begin
                 match res with
-                | Mlw_interp.Normal _ | Mlw_interp.Excep _ ->
+                | Mlw_interp.Normal _ ->
                   printf "@\nresult: %a@\nstate: %a@]@." 
                     Mlw_interp.print_result res
                     Mlw_interp.print_state st
+                | Mlw_interp.Excep _ ->
+                  printf "@\nexceptional result: %a@\nstate: %a@]@." 
+                    Mlw_interp.print_result res
+                    Mlw_interp.print_state st;
+                  exit 1
                 | Mlw_interp.Irred _ | Mlw_interp.Fun _ -> 
                   printf "@]@.";
                   eprintf "Execution error: %a@." Mlw_interp.print_result res;
-                  exit 1
+                  exit 2
               end
             | _ ->
               eprintf "Only functions with one unit argument can be executed.@.";