debugging

examples/selection_sort.mlw

@@ -14,11 +14,12 @@ module SelectionSort
   let selection_sort (a: array int)
     ensures { sorted a /\ permut (old a) a } =
 'L:
+    let min = ref 0 in
     for i = 0 to length a - 1 do
       (* a[0..i[ is sorted; now find minimum of a[i..n[ *)
       invariant { sorted_sub a 0 i /\ permut (at a 'L) a /\
           forall k1 k2: int. 0 <= k1 < i <= k2 < length a -> a[k1] <= a[k2] }
-      let min = ref i in
+      (* let min = ref i in *) min := i;
       for j = i + 1 to length a - 1 do
         invariant {
           i <= !min < j && forall k: int. i <= k < j -> a[!min] <= a[k] }
@@ -29,10 +30,17 @@ module SelectionSort
       assert { permut (at a 'L1) a }
     done
 
-  let test () =
+  let test1 () =
+    let a = make 3 0 in
+    a[0] <- 7; a[1] <- 3; a[2] <- 1; 
+    selection_sort a;
+    a
+
+  let test2 () =
     let a = make 8 0 in
     a[0] <- 3; a[1] <- 1; a[2] <- 7; a[3] <- 0;
     a[4] <- 4; a[5] <- 1; a[6] <- 6; a[7] <- 3;
-    selection_sort a
+    selection_sort a;
+    a
 
 end

modules/array.mlw

@@ -192,6 +192,7 @@ module ArraySwap
 
   let swap (a:array 'a) (i:int) (j:int) : unit
     requires { 0 <= i < length a /\ 0 <= j < length a }
+    writes   { a }
     ensures  { exchange (old a) a i j }
     =
     let v = a[i] in

src/whyml/mlw_interp.ml

@@ -171,6 +171,18 @@ let eval_int_rel op _ty ls l =
     end
   | _ -> assert false
 
+let is_true t =
+  match t.t_node with
+    | Ttrue -> true
+    | Tapp(ls,[]) when ls_equal ls fs_bool_true -> true
+    | _ -> false
+
+let is_false t =
+  match t.t_node with
+    | Tfalse -> true
+    | Tapp(ls,[]) when ls_equal ls fs_bool_false -> true
+    | _ -> false
+
 let term_equality t1 t2 =
   if t_equal t1 t2 then Some true
   else
@@ -179,23 +191,39 @@ let term_equality t1 t2 =
       let i2 = big_int_of_term t2 in
       Some (Big_int.eq_big_int i1 i2)
     with NotNum ->
-      match t1.t_node,t2.t_node with
-        | Ttrue, Tfalse | Tfalse, Ttrue -> Some false
-        | Tapp(ls1,[]),Tapp(ls2,[]) when
-            ls_equal ls1 fs_bool_true && ls_equal ls2 fs_bool_false
-            || ls_equal ls1 fs_bool_false && ls_equal ls2 fs_bool_true
-            -> Some false
-        | _ -> None
+      if is_true t1 && is_true t2 
+        || is_false t1 && is_false t2 
+      then Some true
+      else
+      if is_true t1 && is_false t2 
+        || is_false t1 && is_true t2 
+      then Some false
+      else None
 
 let eval_equ _ty _ls l =
+(*
+  Format.eprintf "[interp] eval_equ ? @.";
+*)
+  let res =
   match l with
   | [t1;t2] ->
     begin match term_equality t1 t2 with
       | Some true -> t_true
       | Some false -> t_false
-      | None -> t_equ t1 t2
+      | None -> 
+        try t_equ t1 t2 with TermExpected _ ->
+          Format.eprintf "t1 = %a, t2 = %a@." Pretty.print_term t1 Pretty.print_term t2;
+          assert false
     end
   | _ -> assert false
+  in
+(*
+  Format.eprintf "[interp] eval_equ: OK@.";
+*)
+  res
+
+let eval_now ty ls l =
+  t_app_infer_inst ls l ty
 
 (* functions on map.Map *)
 
@@ -296,6 +324,7 @@ let add_builtin_th env (l,n,t,d) =
 
 let get_builtins env =
   Hls.add builtins ps_equ eval_equ;
+  Hls.add builtins Mlw_wp.fs_now eval_now;
   List.iter (add_builtin_th env) built_in_theories
 
 
@@ -374,8 +403,9 @@ let exec_array_set env spec s args =
               with Not_found -> reg
             in
             let s' = Mreg.add reg t s in
-            eprintf "[interp] t[%a] <- %a@."
-              Pretty.print_term i Pretty.print_term v; 
+            eprintf "[interp] t[%a] <- %a (map = %a)@."
+              Pretty.print_term i Pretty.print_term v
+              Pretty.print_term t; 
             Normal (Mlw_expr.t_void),s'
           | _ -> assert false
       end
@@ -546,6 +576,14 @@ let rec eval_term env s ty t =
   | Ttrue
   | Tfalse -> t
 
+
+
+
+
+
+
+
+
 and eval_match env s ty u tbl =
   let rec iter tbl =
     match tbl with
@@ -750,21 +788,18 @@ let rec eval_expr env (s:state) (e : expr) : result * state =
 *)
   | Eif(e1,e2,e3) ->
     begin
+      eprintf "[interp] condition of the if : @?";
       match eval_expr env s e1 with
         | Normal t, s' ->
           begin
-            match t.t_node with
-              | Ttrue -> eval_expr env s' e2
-              | Tapp(ls,[]) when ls_equal ls fs_bool_true
-                -> eval_expr env s' e2
-              | Tfalse -> eval_expr env s' e3
-              | Tapp(ls,[]) when ls_equal ls fs_bool_false
-                  -> eval_expr env s' e3
-              | _ ->
+            if is_true t then eval_expr env s' e2 else
+            if is_false t then eval_expr env s' e3 else
+              begin
                 Format.eprintf
                   "@[[Exec] Cannot decide condition of if: @[%a@]@]@."
                   Pretty.print_term t;
                 Irred e, s
+              end
           end
         | r -> r
     end

src/whyml/mlw_wp.mli

@@ -31,6 +31,7 @@ val t_at_old : Term.term -> Term.term
 val th_mark_at  : Theory.theory
 val th_mark_old : Theory.theory
 
+val fs_now : Term.lsymbol
 val e_now : expr
 
 val pv_old : pvsymbol

tests/test-eval.why

@@ -22,6 +22,8 @@ theory T
 
   constant c5 : int = if 2 = 3 then 1 else 2
 
+  constant c5a : int = if 2 <> 3 then 1 else 2
+
   constant c6 : int = if 2 < 3 /\ 5 >= 6 /\ 7 > 8 \/ 9 <= 10 then 1 else 0
 
   use import int.Abs

tests/test_exec.mlw

@@ -6,6 +6,12 @@ module M
 
   let x () : int = 13 * 3 + 7 - 4
 
+  use import ref.Ref
+
+  let x0 () : int =
+    let x = ref 13 in
+    if !x <> 3 then 7 else 4
+
   use import list.Append
 
   let y () : list int =
@@ -183,7 +189,7 @@ module Array
      t[2] <- 67;
      t
 
-  let t1 () = 
+  let t1 () =
     let t = t () in
     t[0] + t[1] + t[2] (* 121 *)
 
@@ -194,5 +200,22 @@ module Array
   let test67 () = search (t ()) 67
   let test7 () = search (t ()) 7
 
+
+  use import array.ArraySwap
+
+  let test_swap () =
+     let t = Array.make 3 0 in
+     t[0] <- 12;
+     t[1] <- 42;
+     t[2] <- 67;
+     swap t 1 2;
+     t[1] (* 67 *)
+
+
+  let test_loop () =
+     let t = Array.make 3 0 in
+     for i=0 to 2 do t[i] <- i done;
+     t[0] + t[1] + t[2] (* 3 *)
+
 end