Module Main now compiles

drivers/c.drv

-
 printer "c"
 
 module ref.Ref
 
   syntax type ref "%1"
+  syntax val ref "%1"
+  syntax converter ref "%1"
+  syntax val (!_) "%1"
+  syntax converter (!_) "%1"
+  syntax val (:=) "%1 = %2" 
 
 end
 
@@ -55,7 +59,10 @@ end
 
 module mach.c.C
 
-  syntax type ptr "(%1 *)"
+  prelude "#include <stdlib.h>"
+  prelude "#include <stdio.h>"
+
+  syntax type ptr "%1 *"
 
   syntax val malloc "malloc(%1 * sizeof(%v0))"  (* and not %t1 ? *)
   syntax val free   "free(%1)"
@@ -64,10 +71,19 @@ module mach.c.C
   syntax val is_null "%1 == NULL"
   syntax val null "NULL"
 
+  syntax val incr "%1+%2"
+
   syntax val get "*(%1)"
   syntax val set "*(%1) = %2"
 
   syntax val p2i "%1"
   syntax converter p2i "%1"
 
+  syntax val break "break"
+  syntax val return32 "return (%1)"
+
+  syntax val print_space "printf(\" \")"
+  syntax val print_newline "printf(\"\\n\")"
+  syntax val print_uint32 "printf(\"%#x\",%1)"
+
 end
\ No newline at end of file

examples/in_progress/multiprecision/mp2.mlw

@@ -199,8 +199,6 @@ module N
     ensures { c * a < c * b }
   = ()
 
-  exception Break32 int32
-
   use import ref.Refint
 
   function compare_int (x y:int) : int =
@@ -275,13 +273,13 @@ module N
                      };
             res := Int32.of_int (-1)
             end;
-         raise Break32 !res
+         return32 !res;
          end
        else ()
      done;
      value_sub_frame_shift (pelts x) (pelts y) x.offset y.offset (p2i sz);
      zero
-   with Break32 r -> r
+   with Return32 r -> r
    end
 
    (* [is_zero] checks if [x[0..sz-1]] is zero. It corresponds to [mpn_zero_p]. *)
@@ -307,14 +305,14 @@ module N
            value_sub_concat (pelts x) x.offset (x.offset+k) (x.offset + p2i sz);
            value_sub_lower_bound_tight (pelts x) x.offset (x.offset+k);
            value_sub_lower_bound (pelts x) (x.offset+k) (x.offset + p2i sz);
-           raise Break32 (Int32.of_int 0)
+           return32 (Int32.of_int 0);
          end
          else begin
            assert { 1+2=3 };
          end
        done;
        Int32.of_int 1
-     with Break32 r -> r
+     with Return32 r -> r
      end
 
   (** [zero r sz] sets [(r,sz)] to zero. Corresponds to [mpn_zero]. *)
@@ -335,8 +333,6 @@ module N
 
   (** {2 Addition} *)
 
-  exception Break
-
   (** [add_limb r x y sz] adds to [x] the value of the limb [y],
       writes the result in [r] and returns the carry. [r] and [x]
       have size [sz]. This corresponds to the function [mpn_add_1] *)
@@ -2112,24 +2108,71 @@ module N
     assert { l2i !qh * l2i d + l2i !r = l2i ul + radix * l2i uh };
     (!qh,!r)
 
-
 end
 
 module Main
 
   use import mach.c.C
   use import N
+  use import mach.int.Int32
+  use import int.Int
+  use import ref.Ref
+
+  let print (p:t) (m n:int32) : unit
+    requires { 0 <= p.offset + p2i m
+               <= p.offset + p2i n
+               <= plength p }
+  =
+    let i = ref m in
+    let q = ref (incr p m) in
+    let one = Int32.of_int 1 in
+    while (Int32.(<) !i n) do
+      invariant { p2i m <= p2i !i <= p2i n }
+      invariant { (!q).offset = p.offset + p2i !i }
+      invariant { plength !q = plength p }
+      variant { p2i n - p2i !i }
+      print_uint32 (get !q);
+      print_space ();
+      q := C.incr !q one;
+      i := Int32.(+) !i one;
+    done;
+    print_newline ()
 
   let from_limb (l:limb) : t
     ensures { is_null result \/ plength result = 1 }
     ensures { is_null result \/ value_sub_shift result 1 = l2i l }
+    ensures { result.offset = 0 }
   =
     let p = malloc (UInt32.of_int 1) in
     if not (is_null p)
     then C.set p l;
     p
 
-  let main () = from_limb (Limb.of_int 42)
+  let two_limbs (l1 l2: limb) : t
+    ensures { is_null result \/ plength result = 2 }
+    ensures { is_null result \/ value_sub_shift result 2 = l2i l1 + radix * l2i l2 }
+    ensures { result.offset = 0 }
+  =
+    let p = malloc (UInt32.of_int 2) in
+    if not (is_null p)
+    then begin
+      C.set p l1;
+      C.set (incr p (Int32.of_int 1)) l2
+      end;
+    p
+
+  let main () =
+    let p = from_limb (Limb.of_int 42) in
+    if not (is_null p)
+       then begin
+       print_uint32 (get p);
+       print_newline ();
+       end;
+    free p;
+    let q = two_limbs (Limb.of_int 42) (Limb.of_int 28) in
+    if not (is_null q)
+       then print q (Int32.of_int 0) (Int32.of_int 2);
+    free q;
 
 end
 

examples/in_progress/multiprecision/mp2/why3session.xml

@@ -10,7 +10,7 @@
 <prover id="5" name="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="6" name="Vampire" version="0.6" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../mp2.mlw" expanded="true">
-<theory name="N" sum="0fd57e69a4e5a85538b534b92177aa8f" expanded="true">
+<theory name="N" sum="c3d7d1839f13fa82e0c3d4dacce89969" expanded="true">
  <goal name="limb_max_bound">
  <proof prover="3"><result status="valid" time="0.02" steps="69"/></proof>
  </goal>
@@ -277,47 +277,65 @@
   <goal name="VC compare_same_size.21" expl="21. integer overflow">
   <proof prover="4"><result status="valid" time="0.03"/></proof>
   </goal>
-  <goal name="VC compare_same_size.22" expl="22. postcondition">
+  <goal name="VC compare_same_size.22" expl="22. loop invariant preservation">
+  <proof prover="3"><result status="valid" time="0.10" steps="70"/></proof>
+  </goal>
+  <goal name="VC compare_same_size.23" expl="23. loop invariant preservation">
+  <proof prover="3"><result status="valid" time="0.03" steps="70"/></proof>
+  </goal>
+  <goal name="VC compare_same_size.24" expl="24. loop variant decrease">
+  <proof prover="3"><result status="valid" time="0.10" steps="70"/></proof>
+  </goal>
+  <goal name="VC compare_same_size.25" expl="25. postcondition">
   <proof prover="4"><result status="valid" time="0.04"/></proof>
   </goal>
-  <goal name="VC compare_same_size.23" expl="23. assertion">
+  <goal name="VC compare_same_size.26" expl="26. assertion">
   <proof prover="4"><result status="valid" time="0.03"/></proof>
   </goal>
-  <goal name="VC compare_same_size.24" expl="24. precondition">
+  <goal name="VC compare_same_size.27" expl="27. precondition">
   <proof prover="4"><result status="valid" time="0.02"/></proof>
   </goal>
-  <goal name="VC compare_same_size.25" expl="25. assertion">
+  <goal name="VC compare_same_size.28" expl="28. assertion">
   <proof prover="3"><result status="valid" time="0.26" steps="117"/></proof>
   </goal>
-  <goal name="VC compare_same_size.26" expl="26. assertion">
+  <goal name="VC compare_same_size.29" expl="29. assertion">
   <transf name="split_goal_wp">
-   <goal name="VC compare_same_size.26.1" expl="1. VC for compare_same_size">
+   <goal name="VC compare_same_size.29.1" expl="1. VC for compare_same_size">
    <proof prover="1"><result status="valid" time="1.08"/></proof>
    </goal>
-   <goal name="VC compare_same_size.26.2" expl="2. VC for compare_same_size">
+   <goal name="VC compare_same_size.29.2" expl="2. VC for compare_same_size">
    <proof prover="4"><result status="valid" time="0.03"/></proof>
    </goal>
   </transf>
   </goal>
-  <goal name="VC compare_same_size.27" expl="27. integer overflow">
+  <goal name="VC compare_same_size.30" expl="30. integer overflow">
   <proof prover="4"><result status="valid" time="0.04"/></proof>
   </goal>
-  <goal name="VC compare_same_size.28" expl="28. postcondition">
+  <goal name="VC compare_same_size.31" expl="31. loop invariant preservation">
+  <proof prover="3"><result status="valid" time="0.10" steps="70"/></proof>
+  </goal>
+  <goal name="VC compare_same_size.32" expl="32. loop invariant preservation">
+  <proof prover="3"><result status="valid" time="0.03" steps="70"/></proof>
+  </goal>
+  <goal name="VC compare_same_size.33" expl="33. loop variant decrease">
+  <proof prover="3"><result status="valid" time="0.10" steps="70"/></proof>
+  </goal>
+  <goal name="VC compare_same_size.34" expl="34. postcondition">
   <proof prover="4"><result status="valid" time="0.04"/></proof>
   </goal>
-  <goal name="VC compare_same_size.29" expl="29. loop invariant preservation">
+  <goal name="VC compare_same_size.35" expl="35. loop invariant preservation">
   <proof prover="4"><result status="valid" time="0.03"/></proof>
   </goal>
-  <goal name="VC compare_same_size.30" expl="30. loop invariant preservation">
+  <goal name="VC compare_same_size.36" expl="36. loop invariant preservation">
   <proof prover="3"><result status="valid" time="0.04" steps="100"/></proof>
   </goal>
-  <goal name="VC compare_same_size.31" expl="31. loop variant decrease">
+  <goal name="VC compare_same_size.37" expl="37. loop variant decrease">
   <proof prover="4"><result status="valid" time="0.03"/></proof>
   </goal>
-  <goal name="VC compare_same_size.32" expl="32. precondition">
+  <goal name="VC compare_same_size.38" expl="38. precondition">
   <proof prover="3"><result status="valid" time="0.05" steps="90"/></proof>
   </goal>
-  <goal name="VC compare_same_size.33" expl="33. postcondition">
+  <goal name="VC compare_same_size.39" expl="39. postcondition">
   <proof prover="4"><result status="valid" time="0.03"/></proof>
   </goal>
  </transf>
@@ -358,31 +376,40 @@
   <goal name="VC is_zero.11" expl="11. integer overflow">
   <proof prover="4"><result status="valid" time="0.02"/></proof>
   </goal>
-  <goal name="VC is_zero.12" expl="12. postcondition">
+  <goal name="VC is_zero.12" expl="12. loop invariant preservation">
+  <proof prover="3"><result status="valid" time="0.03" steps="70"/></proof>
+  </goal>
+  <goal name="VC is_zero.13" expl="13. loop invariant preservation">
+  <proof prover="3"><result status="valid" time="0.03" steps="70"/></proof>
+  </goal>
+  <goal name="VC is_zero.14" expl="14. loop variant decrease">
+  <proof prover="3"><result status="valid" time="0.02" steps="70"/></proof>
+  </goal>
+  <goal name="VC is_zero.15" expl="15. postcondition">
   <proof prover="4"><result status="valid" time="0.02"/></proof>
   </goal>
-  <goal name="VC is_zero.13" expl="13. postcondition">
-  <proof prover="3"><result status="valid" time="0.21" steps="150"/></proof>
+  <goal name="VC is_zero.16" expl="16. postcondition">
+  <proof prover="3"><result status="valid" time="0.21" steps="157"/></proof>
   </goal>
-  <goal name="VC is_zero.14" expl="14. assertion">
+  <goal name="VC is_zero.17" expl="17. assertion">
   <proof prover="4"><result status="valid" time="0.02"/></proof>
   </goal>
-  <goal name="VC is_zero.15" expl="15. loop invariant preservation">
+  <goal name="VC is_zero.18" expl="18. loop invariant preservation">
   <proof prover="4"><result status="valid" time="0.03"/></proof>
   </goal>
-  <goal name="VC is_zero.16" expl="16. loop invariant preservation">
+  <goal name="VC is_zero.19" expl="19. loop invariant preservation">
   <proof prover="3"><result status="valid" time="0.06" steps="103"/></proof>
   </goal>
-  <goal name="VC is_zero.17" expl="17. loop variant decrease">
+  <goal name="VC is_zero.20" expl="20. loop variant decrease">
   <proof prover="4"><result status="valid" time="0.02"/></proof>
   </goal>
-  <goal name="VC is_zero.18" expl="18. integer overflow">
+  <goal name="VC is_zero.21" expl="21. integer overflow">
   <proof prover="4"><result status="valid" time="0.03"/></proof>
   </goal>
-  <goal name="VC is_zero.19" expl="19. postcondition">
+  <goal name="VC is_zero.22" expl="22. postcondition">
   <proof prover="4"><result status="valid" time="0.02"/></proof>
   </goal>
-  <goal name="VC is_zero.20" expl="20. postcondition">
+  <goal name="VC is_zero.23" expl="23. postcondition">
   <proof prover="3"><result status="valid" time="0.04" steps="85"/></proof>
   </goal>
  </transf>
@@ -1692,10 +1719,10 @@
   <proof prover="4"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC mul_limbs.8" expl="8. loop invariant init">
-  <proof prover="4"><result status="valid" time="0.02"/></proof>
+  <proof prover="3"><result status="valid" time="0.02" steps="70"/></proof>
   </goal>
   <goal name="VC mul_limbs.9" expl="9. loop invariant init">
-  <proof prover="3"><result status="valid" time="0.02" steps="70"/></proof>
+  <proof prover="4"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC mul_limbs.10" expl="10. loop invariant init">
   <proof prover="4"><result status="valid" time="0.04"/></proof>
@@ -2274,10 +2301,10 @@
   <proof prover="4"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="VC mul.8" expl="8. loop invariant init">
-  <proof prover="4"><result status="valid" time="0.01"/></proof>
+  <proof prover="4"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC mul.9" expl="9. loop invariant init">
-  <proof prover="4"><result status="valid" time="0.02"/></proof>
+  <proof prover="4"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="VC mul.10" expl="10. loop invariant init">
   <proof prover="4"><result status="valid" time="0.04"/></proof>
@@ -2862,7 +2889,6 @@
   <goal name="VC lshift.30" expl="30. loop invariant preservation">
   <transf name="inline_all">
    <goal name="VC lshift.30.1" expl="1. loop invariant preservation">
-   <proof prover="0" timelimit="10" obsolete="true"><result status="timeout" time="9.50"/></proof>
    <proof prover="6"><result status="valid" time="1.85"/></proof>
    </goal>
   </transf>
@@ -3999,7 +4025,7 @@
  </transf>
  </goal>
 </theory>
-<theory name="Main" sum="1b5018d2448537aeb1d3eb3e920619ba">
+<theory name="Main" sum="e3434722a0f609aed57855977bbc7d27">
  <goal name="VC from_limb" expl="VC for from_limb">
  <transf name="split_goal_wp">
   <goal name="VC from_limb.1" expl="1. integer overflow">
@@ -4015,15 +4041,28 @@
   <proof prover="3"><result status="valid" time="0.14" steps="123"/></proof>
   </goal>
   <goal name="VC from_limb.5" expl="5. postcondition">
-  <proof prover="3"><result status="valid" time="0.03" steps="75"/></proof>
+  <proof prover="3"><result status="valid" time="0.04" steps="79"/></proof>
   </goal>
   <goal name="VC from_limb.6" expl="6. postcondition">
   <proof prover="3"><result status="valid" time="0.03" steps="75"/></proof>
   </goal>
+  <goal name="VC from_limb.7" expl="7. postcondition">
+  <proof prover="3"><result status="valid" time="0.03" steps="75"/></proof>
+  </goal>
+  <goal name="VC from_limb.8" expl="8. postcondition">
+  <proof prover="3"><result status="valid" time="0.03" steps="75"/></proof>
+  </goal>
  </transf>
  </goal>
  <goal name="VC main" expl="VC for main">
- <proof prover="3"><result status="valid" time="0.03" steps="72"/></proof>
+ <transf name="split_goal_wp">
+  <goal name="VC main.1" expl="1. integer overflow">
+  <proof prover="3"><result status="valid" time="0.02" steps="72"/></proof>
+  </goal>
+  <goal name="VC main.2" expl="2. precondition">
+  <proof prover="3"><result status="valid" time="0.02" steps="73"/></proof>
+  </goal>
+ </transf>
  </goal>
 </theory>
 </file>

modules/mach/c.mlw

@@ -109,5 +109,25 @@ module C
                   !(result.data)[i] = !((old p).data)[i] }
     ensures { plength result <> Int32.to_int sz -> p = old p }
 
+  (** break/return*)
+
+  exception Break
+
+  val break () : unit
+    raises { Break }
+    returns { _ -> false }
+
+  exception Return32 int32
+
+  val return32 (x:int32) : unit
+    raises { Return32 n -> x = n }
+    returns { _ -> false }
+
+  (** Printing *)
+
+  val print_space () : unit
+  val print_newline () : unit
+
+  val print_uint32 (n:uint32):unit
 
 end

src/mlw/cprinter.ml

@@ -41,7 +41,9 @@ module C = struct
     | Eindex of expr * expr (* Array access *)
     | Edot of expr * ident (* Field access with dot *)
     | Earrow of expr * ident (* Pointer access with arrow *)
-    | Esyntax of string * ty * (ty array) * (expr*ty) list
+    | Esyntax of string * ty * (ty array) * (expr*ty) list * bool
+  (* template, type and type arguments of result, typed arguments,
+     is/is not converter*)
 
   and constant =
     | Cint of string
@@ -75,8 +77,9 @@ module C = struct
 
   (* [assignify id] transforms a statement that computes a value into
      a statement that assigns that value to id *)
-  let rec assignify id = function
-    | Snop -> raise NotAValue
+  let rec assignify id s =
+    match s with
+    | Snop -> (*Format.printf "assign snop@."; Snop*) raise NotAValue (* ? *)
     | Sexpr e -> Sexpr (Ebinop (Bassign, Evar id, e))
     | Sblock (ds, s) -> Sblock (ds, assignify id s)
     | Sseq (s1, s2) -> Sseq (s1, assignify id s2)
@@ -101,8 +104,8 @@ module C = struct
                                 propagate_in_expr id v e2)
     | Edot (e,i) -> Edot (propagate_in_expr id v e, i)
     | Earrow (e,i) -> Earrow (propagate_in_expr id v e, i)
-    | Esyntax (s,t,ta,l) ->
-      Esyntax (s,t,ta,List.map (fun (e,t) -> (propagate_in_expr id v e),t) l)
+    | Esyntax (s,t,ta,l,b) ->
+      Esyntax (s,t,ta,List.map (fun (e,t) -> (propagate_in_expr id v e),t) l,b)
     | Enothing -> Enothing
     | Econst c -> Econst c
     | Esize_type ty -> Esize_type ty
@@ -154,6 +157,19 @@ module C = struct
 
   let is_empty_block s = s = Sblock([], Snop)
   let block_of_expr e = [], Sexpr e