extraction: simplified driver and test

parent 64dff8d3
......@@ -1650,38 +1650,15 @@ test-runstrat.opt: lib/why3/why3.cmxa lib/why3/META
test-runstrat: test-runstrat.$(OCAMLBEST)
test-ocaml-extraction: bin/why3.opt bin/why3extract.opt lib/why3/why3extract.cmxa
@echo "driver ocaml32"
@mkdir -p tests/test-extraction
@cd tests ; ../bin/why3extract.opt -D ocaml32 \
test_extraction.mlw -o test-extraction
@cd tests/test-extraction/ ; \
$(OCAMLOPT) @BIGINTINCLUDE@ -I ../../lib/why3 \
@BIGINTLIB@.cmxa why3extract.cmxa \
ref__Refint.ml test_extraction__TestExtraction.ml main.ml
@tests/test-extraction/a.out
test-ocaml-extraction: bin/why3.opt bin/why3extract.opt
@echo "driver ocaml64"
@cd tests ; ../bin/why3extract.opt -D ocaml64 \
test_extraction.mlw -o test-extraction
@cd tests/test-extraction/ ; \
$(OCAMLOPT) @BIGINTINCLUDE@ -I ../../lib/why3 \
@BIGINTLIB@.cmxa why3extract.cmxa \
ref__Refint.ml test_extraction__TestExtraction.ml main.ml
@bin/why3extract.opt -D ocaml64 -L tests \
test_extraction.TestExtraction -o tests/test-extraction/test.ml
@ocamlfind ocamlopt -package zarith -linkpkg -I tests/test-extraction/ \
tests/test-extraction/test.ml tests/test-extraction/main.ml \
-o tests/test-extraction/a.out
@tests/test-extraction/a.out
#######################################
# this should be removed in the future
#######################################
test-extraction: bin/why3.opt bin/why3extract.opt lib/why3/why3extract.cmxa
@mkdir -p tests/test-extraction-mario
@bin/why3extract.opt -D drivers/ocaml64.drv --modular --recursive \
-L tests/ test_extraction_mario.M -o tests/test-extraction-mario/
@ocamlfind ocamlopt -package zarith -linkpkg \
-I tests/test-extraction-mario/ \
tests/test-extraction-mario/test_extraction_mario__M.ml \
tests/test-extraction-mario/main.ml -o a.out
@tests/test-extraction-mario/a.out
################
# documentation
################
......
(* OCaml driver
Generic part, for both 32-bit and 64-bit architectures *)
printer "ocaml"
theory BuiltIn
syntax type int "Z.t"
syntax predicate (=) "%1 = %2"
end
import "ocaml-no-arith.drv"
(* int *)
module int.Int
syntax constant zero "Z.zero"
syntax constant one "Z.one"
syntax predicate (<) "Z.lt %1 %2"
syntax predicate (<=) "Z.leq %1 %2"
syntax predicate (>) "Z.gt %1 %2"
syntax predicate (>=) "Z.geq %1 %2"
syntax val (=) "Z.equal %1 %2"
syntax function (+) "Z.add %1 %2"
syntax function (-) "Z.sub %1 %2"
syntax function ( * ) "Z.mul %1 %2"
syntax function (-_) "Z.neg %1"
end
theory int.Abs
syntax function abs "Z.abs %1"
end
theory int.MinMax
syntax function min "Z.min %1 %2"
syntax function max "Z.max %1 %2"
end
(* TODO
theory int.Lex2
prelude "open Why3extract"
syntax predicate lt_nat "(Why3__BigInt.lt_nat %1 %2)"
syntax predicate lex "(Why3__BigInt.lex %1 %2)"
end
*)
theory int.EuclideanDivision
syntax function div "Z.ediv %1 %2"
syntax function mod "Z.erem %1 %2"
end
theory int.ComputerDivision
syntax function div "Z.div %1 %2"
syntax function mod "Z.rem %1 %2"
end
(* TODO Z.pow has type t -> int -> t, not t -> t -> t
theory int.Power
syntax function power "Z.pow %1 %2"
end
theory int.Fact
prelude "open Why3extract"
syntax function fact "(Why3__IntAux.fact %1)"
end
theory int.Fibonacci
prelude "open Why3extract"
syntax function fib "(Why3__IntAux.fib %1)"
end
*)
(* WhyML *)
module stack.Stack
syntax type t "%1 Stack.t"
syntax val create "Stack.create"
syntax val push "Stack.push"
syntax exception Empty "Stack.Empty"
syntax val pop "Stack.pop"
syntax val top "Stack.top"
syntax val safe_pop "Stack.pop"
syntax val safe_top "Stack.top"
syntax val clear "Stack.clear"
syntax val copy "Stack.copy"
syntax val is_empty "Stack.is_empty"
syntax val length "Z.of_int (Stack.length %1)"
end
module queue.Queue
syntax type t "%1 Queue.t"
syntax val create "Queue.create"
syntax val push "Queue.push"
syntax exception Empty "Queue.Empty"
syntax val pop "Queue.pop"
syntax val peek "Queue.peek"
syntax val safe_pop "Queue.pop"
syntax val safe_peek "Queue.peek"
syntax val clear "Queue.clear"
syntax val copy "Queue.copy"
syntax val is_empty "Queue.is_empty"
syntax val length "(Z.of_int (Queue.length %1))"
syntax val transfer "Queue.transfer"
end
module array.Array
syntax type array "%1 array"
syntax function ([]) "%1.(Z.to_int %2)"
(* syntax exception OutOfBounds "Why3__Array.OutOfBounds" *) (* FIXME *)
syntax val ([]) "%1.(Z.to_int %2)"
syntax val ([]<-) "%1.(Z.to_int %2) <- %3"
syntax val length "Z.of_int (Array.length %1)"
syntax val defensive_get "%1.(Z.to_int %2)"
syntax val defensive_set "%1.(Z.to_int %2) <- %3"
syntax val make "Array.make (Z.to_int %1) %2"
syntax val append "Array.append %1 %2"
syntax val sub "Array.sub %1 (Z.to_int %2) (Z.to_int %3)"
syntax val copy "Array.copy %1"
syntax val fill "Array.fill %1 (Z.to_int %2) (Z.to_int %3) %4"
syntax val blit "Array.blit %1 (Z.to_int %2) %3 (Z.to_int %4) (Z.to_int %5)"
end
module matrix.Matrix
prelude "open Why3extract"
syntax type matrix "(%1 Why3__Matrix.t)"
(* FIXME syntax function get "(Why3__Matrix.get %1 %2)" *)
syntax exception OutOfBounds "Why3__Matrix.OutOfBounds"
syntax val get "Why3__Matrix.get"
syntax val set "Why3__Matrix.set"
syntax val rows "Why3__Matrix.rows"
syntax val columns "Why3__Matrix.columns"
syntax val defensive_get "Why3__Matrix.defensive_get"
syntax val defensive_set "Why3__Matrix.defensive_set"
syntax val make "Why3__Matrix.make"
syntax val copy "Why3__Matrix.copy"
end
module mach.int.Int
syntax val ( / ) "Z.div %1 %2"
syntax val ( % ) "Z.rem %1 %2"
end
module mach.int.Int31
(* even on a 64-bit machine, it is safe to use type int for 31-bit integers *)
syntax val of_int "Why3extract.Why3__BigInt.to_int"
syntax converter of_int "%1"
syntax function to_int "(Why3extract.Why3__BigInt.of_int %1)"
syntax type int31 "int"
syntax val ( + ) "( + )"
syntax val ( - ) "( - )"
syntax val (-_) "( ~- )"
syntax val ( * ) "( * )"
syntax val ( / ) "( / )"
syntax val ( % ) "(mod)"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val (<=) "(<=)"
syntax val (<) "(<)"
syntax val (>=) "(>=)"
syntax val (>) "(>)"
end
module mach.int.UInt64
(* no OCaml library for unsigned 64-bit integers => we use BigInt *)
prelude "open Why3extract"
syntax val of_int "(fun x -> x)"
syntax converter of_int "(Why3__BigInt.of_string \"%1\")"
syntax function to_int "%1"
syntax type uint64 "Why3__BigInt.t"
syntax val ( + ) "Why3__BigInt.add"
syntax val ( - ) "Why3__BigInt.sub"
syntax val (-_) "Why3__BigInt.minus"
syntax val ( * ) "Why3__BigInt.mul"
syntax val ( / ) "Why3__BigInt.computer_div"
syntax val ( % ) "Why3__BigInt.computer_mod"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val (<=) "(<=)"
syntax val (<) "(<)"
syntax val (>=) "(>=)"
syntax val (>) "(>)"
end
module mach.array.Array31
syntax type array "(%1 array)"
syntax val make "Array.make"
syntax val ([]) "Array.get"
syntax val ([]<-) "Array.set"
syntax val length "Array.length"
syntax val append "Array.append"
syntax val sub "Array.sub"
syntax val copy "Array.copy"
syntax val fill "Array.fill"
syntax val blit "Array.blit"
syntax val self_blit "Array.blit"
end
module string.Char
prelude "open Why3extract"
syntax type char "Pervasives.char"
syntax val chr "Why3__BigInt.chr"
syntax val code "Why3__BigInt.code"
syntax function uppercase "Char.uppercase"
syntax function lowercase "Char.lowercase"
end
module io.StdIO
prelude "open Why3extract"
syntax val print_char "Pervasives.print_char"
syntax val print_int "Why3__BigInt.print"
syntax val print_newline "Pervasives.print_newline"
end
module random.Random
prelude "open Why3extract"
syntax val random_int "Why3__BigInt.random_int"
end
(** Arithmetic-independent OCaml driver *)
(* FIXME
theory HighOrd
syntax type func "(%1 -> %2)"
syntax type pred "(%1 -> bool)"
syntax function (@) "(%1 %2)"
end
*)
theory option.Option
syntax type option "%1 option"
syntax function None "None"
syntax function Some "Some %1"
end
(* bool *)
theory Bool
syntax type bool "bool"
syntax function True "true"
syntax function False "false"
end
theory bool.Ite
syntax function ite "(if %1 then %2 else %3)"
end
theory bool.Bool
syntax function andb "%1 && %2"
syntax function orb "%1 || %2"
syntax function xorb "%1 <> %2"
syntax function notb "not %1"
syntax function implb "not %1 || %2"
end
(* list *)
theory list.List
syntax type list "%1 list"
syntax function Nil "[]"
syntax function Cons "%1 :: %2"
syntax predicate is_nil "%1 = []"
end
theory list.Length
syntax function length "List.length %1"
end
theory list.Mem
syntax predicate mem "List.mem %1 %2"
end
theory list.Append
syntax function (++) "List.append %1 %2"
end
theory list.Reverse
syntax function reverse "List.rev %1"
end
theory list.RevAppend
syntax function rev_append "List.rev_append %1 %2"
end
theory list.Combine
syntax function combine "List.combine %1 %2"
end
(* WhyML *)
module ref.Ref
syntax type ref "%1 ref"
syntax function contents "!%1"
syntax val ref "ref %1"
syntax val (!_) "!%1"
syntax val (:=) "%1 := %2"
end
(* FIXME: once we extract ref.Refint, this module
will no longer be useful in the driver *)
module ref.Refint
syntax val incr "%1 := Z.succ (Pervasives.(!) %1)"
syntax val decr "%1 := Z.pred (Pervasives.(!) %1)"
syntax val (+=) "%1 := Z.add (Pervasives.(!) %1) %2"
syntax val (-=) "%1 := Z.sub (Pervasives.(!) %1) %2"
syntax val ( *= ) "%1 := Z.mul (Pervasives.(!) %1) %2"
end
module null.Null
syntax type t "%1"
syntax val create_null "(fun () -> Obj.magic (ref 0))"
syntax val eq_null "(==)"
syntax val create "(fun x -> x)"
syntax val get "(fun x -> x)"
end
This diff is collapsed.
......@@ -440,8 +440,6 @@ module Translate = struct
List.exists is_constructor its
| _ -> false
let is_private_record itd = itd.itd_its.its_private
let is_singleton_imutable itd =
let not_g e = not (rs_ghost e) in
let pjl = itd.itd_fields in
......@@ -452,18 +450,28 @@ module Translate = struct
| [is_mutable] -> not is_mutable
| _ -> false
let is_optimizable_record itd =
not (is_private_record itd) && is_singleton_imutable itd
let get_record info rs =
let get_record_itd info rs =
match Mid.find_opt rs.rs_name info.info_mo_known_map with
| Some {pd_node = PDtype itdl} ->
let f pjl_constr = List.exists (rs_equal rs) pjl_constr in
let itd = begin match rs.rs_field with
let itd = match rs.rs_field with
| Some _ -> List.find (fun itd -> f itd.itd_fields) itdl
| None -> List.find (fun itd -> f itd.itd_constructors) itdl end in
is_optimizable_record itd
| _ -> false
| None -> List.find (fun itd -> f itd.itd_constructors) itdl in
if itd.itd_fields = [] then None else Some itd
| _ -> None
let is_optimizable_record_itd itd =
not itd.itd_its.its_private && is_singleton_imutable itd
let is_optimizable_record_rs info rs =
Opt.fold (fun _ -> is_optimizable_record_itd) false (get_record_itd info rs)
let is_empty_record_itd itd =
let is_ghost rs = rs_ghost rs in
List.for_all is_ghost itd.itd_fields
let is_empty_record info rs =
Opt.fold (fun _ -> is_empty_record_itd) false (get_record_itd info rs)
let mk_eta_expansion rsc pvl cty_app =
(* FIXME : effects and types of the expression in this situation *)
......@@ -620,6 +628,8 @@ module Translate = struct
ML.mk_expr ml_letrec (ML.I e.e_ity) e.e_effect
| Eexec ({c_node = Capp (rs, [])}, _) when is_rs_tuple rs ->
ML.mk_unit
| Eexec ({c_node = Capp (rs, _)}, _) when is_empty_record info rs ->
ML.mk_unit
| Eexec ({c_node = Capp (rs, _)}, _) when rs_ghost rs ->
ML.mk_unit
| Eexec ({c_node = Capp (rs, pvl); c_cty = cty}, _)
......@@ -629,9 +639,7 @@ module Translate = struct
| Eexec ({c_node = Capp (rs, pvl); _}, _) ->
let pvl = app pvl rs.rs_cty.cty_args in
begin match pvl with
| [pv_expr] when get_record info rs ->
(* singleton public record type obtained by ghost fields erasure *)
pv_expr
| [pv_expr] when is_optimizable_record_rs info rs -> pv_expr
| _ -> ML.mk_expr (ML.Eapp (rs, pvl)) (ML.I e.e_ity) eff end
| Eexec ({c_node = Cfun e; c_cty = {cty_args = []}}, _) ->
(* abstract block *)
......@@ -720,10 +728,8 @@ module Translate = struct
let p e = not (rs_ghost e) in
let pjl = filter_ghost_params p drecord_fields pjl in
begin match pjl with
| [] -> ML.mk_its_defn id args is_private None
| [(is_mutable, _, ty_pj)]
when not s.its_private && not is_mutable ->
(* singleton public record with an imutable field *)
| [] -> ML.mk_its_defn id args is_private (Some (ML.Dalias ML.tunit))
| [_, _, ty_pj] when is_optimizable_record_itd itd ->
ML.mk_its_defn id args is_private (Some (ML.Dalias ty_pj))
| pjl -> ML.mk_its_defn id args is_private (Some (ML.Drecord pjl))
end
......
let () = Test_extraction_mario__M.main ()
(* main file for ../test_extraction.mlw so that we *run* the extracted code *)
let (=) = Z.eq
open Test
let (=) = Z.equal
let b42 = Z.of_int 42
let () = assert (test_int () = b42)
let () = assert (test_int32 () = b42)
let () = assert (test_uint32 () = b42)
let () = assert (test_int63 () = b42)
let () = assert (test_int64 () = b42)
let () = assert (test_uint64 () = b42)
let () = assert (test_ref () = b42)
let () = assert (test_array () = b42)
let () = assert (test_array31 () = b42)
let () = assert (test_array63 () = b42)
let () = main ()
let () = Format.printf " OCaml extraction test successful@."
......
......@@ -9,42 +9,12 @@ module TestExtraction
let f (x: int) : int = x+1
let test_int () = f 31 + (div 33 3 + 2 - 4) - -1
use import mach.int.Int31
let f31 (x: int31) : int31 = x + of_int 1
let test_int31 () =
to_int (f31 (of_int 31) +
(of_int 33 / of_int 3 + of_int 2 - of_int 4) - (- of_int 1))
use import mach.int.Int32
let f32 (x: int32) : int32 = x + of_int 1
let test_int32 () =
to_int (f32 (of_int 31) +
(of_int 33 / of_int 3 + of_int 2 - of_int 4) - (- of_int 1))
use import mach.int.UInt32
let fu32 (x: uint32) : uint32 = x + of_int 1
let test_uint32 () =
to_int (fu32 (of_int 31) +
(of_int 33 / of_int 3 + of_int 2 - of_int 4) - (- of_int 1))
use import mach.int.Int63
let f63 (x: int63) : int63 = x + of_int 1
let test_int63 () =
to_int (f63 (of_int 31) +
(of_int 33 / of_int 3 + of_int 2 - of_int 4) - (- of_int 1))
use import mach.int.Int64
let f64 (x: int64) : int64 = x + of_int 1
let test_int64 () =
to_int (f64 (of_int 31) +
(of_int 33 / of_int 3 + of_int 2 - of_int 4) - (- of_int 1))
use import mach.int.UInt64
let fu64 (x: uint64) : uint64 = x + of_int 1
let test_uint64 () =
to_int (fu64 (of_int 31) +
(of_int 33 / of_int 3 + of_int 2 - of_int 4) - (- of_int 1))
use import int.Int
use import ref.Ref
use import ref.Refint
......@@ -63,17 +33,226 @@ module TestExtraction
for i = 1 to 42 do a[i] <- a[i-1] + 1 done;
a[42]
use import mach.array.Array31
use import mach.array.Array63
let test_array63 () : int =
let a = Array63.make (Int63.of_int 43) 0 in
for i = 1 to 42 do a[Int63.of_int i] <- a[Int63.of_int (i - 1)] + 1 done;
a[Int63.of_int 42]
use import seq.Seq
use import int.Int
use import mach.int.Int
val test_val (x: int) : int
ensures { result > x }
let function f_function (y: int) (x: int) : int
requires { x >= 0 }
ensures { result >= 0 }
= x
let g (ghost z: int) (x: int) : int
requires { x > 0 }
ensures { result > 0 }
= let y = x in
y
type t 'a 'b 'c 'd
type list 'a = Nil | Cons 'a (list 'a)
type btree 'a = E | N (btree 'a) 'a (btree 'a)
type ntree 'a = Empty | Node 'a (list 'a)
type list_int = list int
type cursor 'a = {
collection : list 'a;
index : int;
mutable index2 : int;
ghost mutable v : seq 'a;
}
type r 'a = {
aa: 'a;
ghost i: int;
}
(* let create_cursor (l: list int) (i i2: int) : cursor int = *)
(* { collection = l; index = i; index2 = i2; v = empty } *)
let create_r (x: int) (y: int) : r int =
{ aa = x; i = y }
use import ref.Ref
let update (c: cursor int) : int
= c.index
exception Empty (list int, int)
exception Out_of_bounds int
(* exception are unary constructors *)
(*
let raise1 () =
raises { Empty -> true }
raise (Empty (Nil, 0))
let raise2 () =
raises { Empty -> true }
let p = (Nil, 0) in
raise (Empty p)
*)
let rec length (l: list 'a) : int
variant { l }
= match l with
| Nil -> 0
| Cons _ r -> 1 + length r
end
let t (x:int) : int
requires { false }
= absurd
let a () : unit
= assert { true }
let singleton (x: int) (l: list int) : list int =
let x = Nil in x
(* FIXME constructors in Why3 can be partially applied
=> an eta-expansion is needed
be careful with side-effects
"let c = Cons e in" should be translated to
"let c = let o = e in fun x -> Cons (o, x) in ..." in OCaml
Mário: I think A-normal form takes care of the side-effects problem
*)
let constructor1 () =
let x = Cons in
x 42
let foofoo (x: int) : int =
let ghost y = x + 1 in
x
let test (x: int) : int =
let y =
let z = x in
(ghost z) + 1
in 42
type list_ghost = Nil2 | Cons2 int list_ghost (ghost int)
let add_list_ghost (x: int) (l: list_ghost) : list_ghost =
match l with
| Cons2 _ Nil2 _ | Nil2 -> Cons2 x Nil2 (1+2)
| Cons2 _ _ n -> Cons2 x l (n+1)
end
let ggg () : int = 42
let call (x:int) : int =
ggg () + 42
(* functions with ghost arguments *)
let test_filter_ghost_args (x: int) (ghost y: int) =
1 / 0
let test_call (x: int) : int =
test_filter_ghost_args x 0 + 1
let constant test_partial : int =
let partial = test_filter_ghost_args 3 in
42
let test_filter_ghost_args2 (x: int) (ghost y: int) (z: int) : int =
x + z
let test_filter_ghost_args3 (ghost y: int) : int =
1 / 0
let many_args (a b c d e f g h i j k l m: int) : int = 42
let foo (x: int) : int =
let _ = 42 in (* FIXME? print _ in OCaml *)
x
let test_fun (x: int) : int -> int =
fun (y: int) -> x + y
let test_local (x: int) : int =
let fact (x: int) (y: int): int = x + y in
fact x 42
let test_lets (x: int) : int =
let y = x in
let z = y + 1 in
let yxz = y * x * z in
let xzy = x + z + y in
let res = yxz - xzy in
res
let test_partial2 (x: int) : int =
let sum : int -> int -> int = fun x y -> x + y in
let incr_a (a: int) = sum a in
incr_a x x
let constr_partial (x: int) : list int =
let x = Cons 42 in
x Nil
let filter_record (c: cursor 'a) : int =
match c with
| { collection = l; index = i; index2 = i2; v = v} -> i
end
(** for loops *)
let for_loop1 () =
let r = ref 0 in
for i = 0 to 10 do r := !r + i done;
!r
(** test the execution of the extracted code *)
use import ocaml.Pervasives
let test1 () raises { AssertFailure } =
ocaml_assert (1 + 1 = 2)
(** parallel assignement *)
type record1 = { mutable field: int }
let test_parallel_assign () raises { AssertFailure } =
let a = { field = 0 } in
let b = { field = 1 } in
(a.field, b.field) <- (b.field, a.field);
ocaml_assert (a.field = 1)
(** machine arithmetic *)
use import mach.int.Int63
let get_min_int63 (x: int63) : int
= min_int63
let test2 () raises { AssertFailure }
= ocaml_assert (of_int 1 + of_int 1 = of_int 2)
let test_array31 () : int =
let a = Array31.make (Int31.of_int 43) 0 in
for i = 1 to 42 do a[Int31.of_int i] <- a[Int31.of_int (i - 1)] + 1 done;
a[Int31.of_int 42]
let main () raises { AssertFailure } =
test1 ();
test2 ();
test_parallel_assign ()
end
(*