Skip to content

GitLab

Commit beb4b0b8 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

[extraction] two drivers for OCaml, namely ocaml32 and ocaml64 

support for 31/32/63/64-bit integers in extracted code
parent 45e16b14
Hide whitespace changes
Inline Side-by-side
Showing with 441 additions and 171 deletions
.gitignore
View file @ beb4b0b8
......@@ -181,6 +181,8 @@ pvsbin/
/tests/test-pgm-jcf/
/tests/test-claude/
/tests/test-and/
/tests/test-extraction/*
!/tests/test-extraction/main.ml
# /examples/
/examples/in_progress/course/
......
Makefile.in
View file @ beb4b0b8
......@@ -167,13 +167,13 @@ $(LIBDEP): $(LIBGENERATED)
ifeq (@enable_zarith@,yes)
lib/ocaml/why3__BigInt.ml: config.status lib/ocaml/bigInt_zarith.ml
cp lib/ocaml/bigInt_zarith.ml lib/ocaml/why3__BigInt.ml
lib/ocaml/why3__BigInt.ml: config.status lib/ocaml/why3__BigInt_zarith.ml
cp lib/ocaml/why3__BigInt_zarith.ml $@
else
lib/ocaml/why3__BigInt.ml: config.status src/util/bigInt.ml
cp lib/ocaml/bigInt_num.ml lib/ocaml/why3__BigInt.ml
lib/ocaml/why3__BigInt.ml: config.status lib/ocaml/why3__BigInt_num.ml
cp lib/ocaml/why3__BigInt_num.ml $@
endif
......@@ -1199,7 +1199,7 @@ clean::
# Ocaml realizations
#######################
OCAMLLIBS_FILES = why3__BigInt why3__Prelude why3__Map
OCAMLLIBS_FILES = why3__BigInt why3__IntAux why3__Array why3__Map
OCAMLLIBS_MODULES := $(addprefix lib/ocaml/, $(OCAMLLIBS_FILES))
......@@ -1364,10 +1364,11 @@ bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS)
$(MAKE) test-api-mlw-tree.@OCAMLBEST@
$(MAKE) test-api-mlw.@OCAMLBEST@
$(MAKE) test-session.@OCAMLBEST@
$(MAKE) test-ocaml-extraction
# desactivé car requiert findlib
# if test -d examples/runstrat ; then \
# $(MAKE) test-runstrat.@OCAMLBEST@ ; fi
sh bench/bench "bin/why3.@OCAMLBEST@"
bash bench/bench "bin/why3.@OCAMLBEST@"
@if test "@enable_coq_tactic@" = "yes"; then \
echo "=== checking the Coq tactic ==="; \
$(MAKE) test-coq-tactic.@OCAMLBEST@; fi
......@@ -1485,6 +1486,25 @@ test-runstrat.opt: lib/why3/why3.cmxa lib/why3/META
test-runstrat: test-runstrat.$(OCAMLBEST)
test-ocaml-extraction: bin/why3.opt lib/why3/why3extract.cmxa
@echo "driver ocaml32"
@mkdir -p tests/test-extraction
@cd tests ; ../bin/why3.opt -E 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
@echo "driver ocaml64"
@cd tests ; ../bin/why3.opt -E 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
@tests/test-extraction/a.out
################
# documentation
################
......
bench/bench
View file @ beb4b0b8
#!/bin/sh
#!/bin/bash
# auto bench for why
......@@ -40,7 +40,7 @@ bads () {
drivers () {
for f in $1/*.drv; do
if [ $f = "drivers/ocaml.drv" ]; then continue; fi
if [[ $f == drivers/ocaml*.drv ]]; then continue; fi
echo -n " $f... "
# running Why
if ! echo "theory Test goal G : 1=2 end" | $pgm -F why --driver $f - > /dev/null 2>&1; then
......@@ -96,8 +96,8 @@ extract_and_run () {
fi
else
echo "compilation failed!"
echo make -C $1
make -C $1
echo make -C $1
make -C $1
exit 1
fi
else
......@@ -119,7 +119,6 @@ list_stuff () {
fi
}
echo "=== Checking theories ==="
goods theories
echo ""
......
drivers/ocaml.drv → drivers/ocaml-gen.drv
View file @ beb4b0b8
(* OCaml driver
Generic part, for both 32-bit and 64-bit architectures *)
printer "ocaml"
theory BuiltIn
......@@ -84,11 +87,11 @@ theory int.Power
end
theory int.Fact
syntax function fact "(Why3__BigInt.fact %1)"
syntax function fact "(Why3__IntAux.fact %1)"
end
theory int.Fibonacci
syntax function fib "(Why3__BigInt.fib %1)"
syntax function fib "(Why3__IntAux.fib %1)"
end
(* TODO number.Gcd *)
......@@ -147,87 +150,61 @@ module ref.Ref
end
module array.Array
syntax type array "(%1 Why3__BigInt.Array.t)"
syntax function ([]) "(Why3__BigInt.Array.get %1 %2)"
syntax val ([]) "Why3__BigInt.Array.get"
syntax val ([]<-) "Why3__BigInt.Array.set"
syntax val length "Why3__BigInt.Array.length"
syntax exception OutOfBounds "Why3__BigInt.Array.OutOfBounds"
syntax val defensive_get "Why3__BigInt.Array.defensive_get"
syntax val defensive_set "Why3__BigInt.Array.defensive_set"
syntax val make "Why3__BigInt.Array.make"
syntax val append "Why3__BigInt.Array.append"
syntax val sub "Why3__BigInt.Array.sub"
syntax val copy "Why3__BigInt.Array.copy"
syntax val fill "Why3__BigInt.Array.fill"
syntax val blit "Why3__BigInt.Array.blit"
syntax type array "(%1 Why3__Array.t)"
syntax function ([]) "(Why3__Array.get %1 %2)"
syntax exception OutOfBounds "Why3__Array.OutOfBounds"
syntax val ([]) "Why3__Array.get"
syntax val ([]<-) "Why3__Array.set"
syntax val length "Why3__Array.length"
syntax val defensive_get "Why3__Array.defensive_get"
syntax val defensive_set "Why3__Array.defensive_set"
syntax val make "Why3__Array.make"
syntax val append "Why3__Array.append"
syntax val sub "Why3__Array.sub"
syntax val copy "Why3__Array.copy"
syntax val fill "Why3__Array.fill"
syntax val blit "Why3__Array.blit"
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 "Why3__BigInt.to_int"
syntax converter of_int "%1"
syntax function to_int "(Why3__BigInt.of_int %1)"
syntax type int31 "int"
syntax constant min_int31 "(- 0x4000_0000)"
syntax constant max_int31 "0x3fff_ffff"
syntax val of_int "(fun x -> int_of_string (Num.string_of_num x))"
(* FIXME: use a realization instead? *)
syntax val ( + ) "( + )"
syntax val ( - ) "( - )"
syntax val (-_) "( ~- )"
syntax val ( * ) "( * )"
syntax val ( / ) "( / )"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val (<=) "(<=)"
syntax val (<) "(<)"
syntax val (>=) "(>=)"
syntax val (>) "(>)"
end
module mach.int.Int32
syntax type int32 "Int32.t"
syntax constant min_int32 "Int32.min_int"
syntax constant max_int32 "Int32.max_int"
syntax val of_int "(fun x -> Int32.of_string (Num.string_of_num x))"
(* FIXME: use a realization instead? *)
syntax val (+) "Int32.add"
syntax val (-) "Int32.sub"
syntax val (-_) "Int32.neg"
syntax val ( * ) "Int32.mul"
syntax val (/) "Int32.div"
syntax val (<=) "(<=)"
syntax val (<) "(<)"
syntax val (>=) "(>=)"
syntax val (>) "(>)"
end
module mach.int.UInt64
(* no OCaml library for unsigned 64-bit integers => we use BigInt *)
syntax val of_int "%1"
syntax converter of_int "(Why3__BigInt.of_string \"%1\")"
module mach.int.Int63
(* only safe on a 64-bit machine *)
prelude "let () = assert (Sys.word_size = 64)"
syntax type int63 "int"
syntax constant min_int63 "(- 0x4000_0000_0000_0000)"
syntax constant max_int63 "0x3fff_ffff_ffff_ffff"
syntax val of_int "(fun x -> int_of_string (Num.string_of_num x))"
(* FIXME: use a realization instead? *)
syntax val ( + ) "( + )"
syntax val ( - ) "( - )"
syntax val (-_) "( ~- )"
syntax val ( * ) "( * )"
syntax val ( / ) "( / )"
syntax val (<=) "(<=)"
syntax val (<) "(<)"
syntax val (>=) "(>=)"
syntax val (>) "(>)"
end
syntax function to_int "%1"
module mach.int.Int64
syntax type int64 "Int64.t"
syntax constant min_int64 "Int64.min_int"
syntax constant max_int64 "Int64.max_int"
syntax val of_int "(fun x -> Int64.of_string (Num.string_of_num x))"
(* FIXME: use a realization instead? *)
syntax val (+) "Int64.add"
syntax val (-) "Int64.sub"
syntax val (-_) "Int64.neg"
syntax val ( * ) "Int64.mul"
syntax val (/) "Int64.div"
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 eq "(=)"
syntax val ne "(<>)"
syntax val (<=) "(<=)"
syntax val (<) "(<)"
syntax val (>=) "(>=)"
......@@ -235,7 +212,8 @@ module mach.int.Int64
end
module mach.array.Array31
syntax type array "array"
syntax type array "(%1 array)"
syntax val make "Array.make"
syntax val ([]) "Array.get"
syntax val ([]<-) "Array.set"
......@@ -249,6 +227,5 @@ module mach.array.Array31
end
(* TODO
- OutOfBounds, defensive_get, defensive_set in mach.array.in Array31
- mach.array.Array32 -> Bigarray sur 32-bit / Array sur 64-bit ?
*)
drivers/ocaml32.drv 0 → 100644
View file @ beb4b0b8
(* OCaml driver for 32-bit architecture *)
import "ocaml-gen.drv"
module mach.int.Int32
syntax val of_int "Why3__BigInt.to_int32"
syntax converter of_int "%1l"
syntax function to_int "(Why3__BigInt.of_int32 %1)"
syntax type int32 "Int32.t"
syntax val (+) "Int32.add"
syntax val (-) "Int32.sub"
syntax val (-_) "Int32.neg"
syntax val ( * ) "Int32.mul"
syntax val (/) "Int32.div"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val (<=) "(<=)"
syntax val (<) "(<)"
syntax val (>=) "(>=)"
syntax val (>) "(>)"
end
module mach.int.UInt32
syntax val of_int "Why3__BigInt.to_int64"
syntax converter of_int "%1L"
syntax function to_int "(Why3__BigInt.of_int64 %1)"
syntax type uint32 "Int64.t"
syntax val (+) "Int64.add"
syntax val (-) "Int64.sub"
syntax val (-_) "Int64.neg"
syntax val ( * ) "Int64.mul"
syntax val (/) "Int64.div"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val (<=) "(<=)"
syntax val (<) "(<)"
syntax val (>=) "(>=)"
syntax val (>) "(>)"
end
module mach.int.Int63
syntax val of_int "Why3__BigInt.to_int64"
syntax converter of_int "%1L"
syntax function to_int "(Why3__BigInt.of_int64 %1)"
syntax type int63 "Int64.t"
syntax val (+) "Int64.add"
syntax val (-) "Int64.sub"
syntax val (-_) "Int64.neg"
syntax val ( * ) "Int64.mul"
syntax val (/) "Int64.div"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val (<=) "(<=)"
syntax val (<) "(<)"
syntax val (>=) "(>=)"
syntax val (>) "(>)"
end
module mach.int.Int64
syntax val of_int "Why3__BigInt.to_int64"
syntax converter of_int "%1L"
syntax function to_int "(Why3__BigInt.of_int64 %1)"
syntax type int64 "Int64.t"
syntax val (+) "Int64.add"
syntax val (-) "Int64.sub"
syntax val (-_) "Int64.neg"
syntax val ( * ) "Int64.mul"
syntax val (/) "Int64.div"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val (<=) "(<=)"
syntax val (<) "(<)"
syntax val (>=) "(>=)"
syntax val (>) "(>)"
end
drivers/ocaml64.drv 0 → 100644
View file @ beb4b0b8
(* OCaml driver for 64-bit architecture *)
import "ocaml-gen.drv"
module mach.int.Int32
syntax val of_int "Why3__BigInt.to_int"
syntax converter of_int "%1"
syntax function to_int "(Why3__BigInt.of_int %1)"
syntax type int32 "int"
syntax val ( + ) "( + )"
syntax val ( - ) "( - )"
syntax val (-_) "( ~- )"
syntax val ( * ) "( * )"
syntax val ( / ) "( / )"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val (<=) "(<=)"
syntax val (<) "(<)"
syntax val (>=) "(>=)"
syntax val (>) "(>)"
end
module mach.int.UInt32
syntax val of_int "Why3__BigInt.to_int"
syntax converter of_int "%1"
syntax function to_int "(Why3__BigInt.of_int %1)"
syntax type uint32 "int"
syntax val ( + ) "( + )"
syntax val ( - ) "( - )"
syntax val (-_) "( ~- )"
syntax val ( * ) "( * )"
syntax val ( / ) "( / )"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val (<=) "(<=)"
syntax val (<) "(<)"
syntax val (>=) "(>=)"
syntax val (>) "(>)"
end
module mach.int.Int63
syntax val of_int "Why3__BigInt.to_int"
syntax converter of_int "%1"
syntax function to_int "(Why3__BigInt.of_int %1)"
syntax type int63 "int"
syntax val ( + ) "( + )"
syntax val ( - ) "( - )"
syntax val (-_) "( ~- )"
syntax val ( * ) "( * )"
syntax val ( / ) "( / )"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val (<=) "(<=)"
syntax val (<) "(<)"
syntax val (>=) "(>=)"
syntax val (>) "(>)"
end
module mach.int.Int64
syntax val of_int "Why3__BigInt.to_int64"
syntax converter of_int "%1L"
syntax function to_int "(Why3__BigInt.of_int64 %1)"
syntax type int64 "Int64.t"
syntax val (+) "Int64.add"
syntax val (-) "Int64.sub"
syntax val (-_) "Int64.neg"
syntax val ( * ) "Int64.mul"
syntax val (/) "Int64.div"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val (<=) "(<=)"
syntax val (<) "(<)"
syntax val (>=) "(>=)"
syntax val (>) "(>)"
end
examples/sudoku/Makefile
View file @ beb4b0b8
......@@ -30,7 +30,7 @@ $(MAIN).opt: $(CMX) $(MAIN).cmx
$(MAIN).cmx: $(CMX)
$(ML): ../sudoku.mlw
../../bin/why3 -E ocaml ../sudoku.mlw -o .
../../bin/why3 -E ocaml32 ../sudoku.mlw -o .
%.cmx: %.ml
$(OCAMLOPT) $(WHY3) -annot -c $<
......
lib/ocaml/why3__Array.ml 0 → 100644
View file @ beb4b0b8
open Why3__BigInt
type 'a t = 'a array
let get a i = a.(to_int i)
let set a i v = a.(to_int i) <- v
let length a = of_int (Array.length a)
exception OutOfBounds
let check_bounds a i = if i < 0 || i >= Array.length a then raise OutOfBounds
let defensive_get a i = let i = to_int i in check_bounds a i; a.(i)
let defensive_set a i v = let i = to_int i in check_bounds a i; a.(i) <- v
let make n v = Array.make (to_int n) v
let append = Array.append
let sub a ofs len = Array.sub a (to_int ofs) (to_int len)
let copy = Array.copy
let fill a ofs len v = Array.fill a (to_int ofs) (to_int len) v
let blit a1 ofs1 a2 ofs2 len =
Array.blit a1 (to_int ofs1) a2 (to_int ofs2) (to_int len)
lib/ocaml/bigInt_num.ml → lib/ocaml/why3__BigInt_num.ml
View file @ beb4b0b8
......@@ -16,7 +16,6 @@ let compare = compare_big_int
let zero = zero_big_int
let one = unit_big_int
let of_int = big_int_of_int
let succ = succ_big_int
let pred = pred_big_int
......@@ -67,48 +66,17 @@ let pow_int_pos = power_int_positive_int
let to_string = string_of_big_int
let of_string = big_int_of_string
let to_int = int_of_big_int
let of_int = big_int_of_int
let to_int32 = int32_of_big_int
let of_int32 = big_int_of_int32
(* the code below is to be used in OCaml extracted code (see ocaml.drv) *)
let to_int64 = int64_of_big_int
let of_int64 = big_int_of_int64
let power x y =
try power_big_int_positive_big_int x y
with Invalid_argument _ -> zero
let rec fact n = if le n one then one else mul n (fact (pred n))
let fib n =
let n = to_int n in
if n = 0 then zero else if n = 1 then one else
let a = Array.make (n + 1) zero in
a.(1) <- one; for i = 2 to n do a.(i) <- add a.(i-2) a.(i-1) done; a.(n)
let rec for_loop_to x1 x2 body =
if le x1 x2 then begin
body x1;
for_loop_to (succ x1) x2 body
end
let rec for_loop_downto x1 x2 body =
if ge x1 x2 then begin
body x1;
for_loop_downto (pred x1) x2 body
end
module Array = struct
type 'a t = 'a array
let get a i = a.(to_int i)
let set a i v = a.(to_int i) <- v
let length a = of_int (Array.length a)
exception OutOfBounds
let check_bounds a i = if i < 0 || i >= Array.length a then raise OutOfBounds
let defensive_get a i = let i = to_int i in check_bounds a i; a.(i)
let defensive_set a i v = let i = to_int i in check_bounds a i; a.(i) <- v
let make n v = Array.make (to_int n) v
let append = Array.append
let sub a ofs len = Array.sub a (to_int ofs) (to_int len)
let copy = Array.copy
let fill a ofs len v = Array.fill a (to_int ofs) (to_int len) v
let blit a1 ofs1 a2 ofs2 len =
Array.blit a1 (to_int ofs1) a2 (to_int ofs2) (to_int len)
end
lib/ocaml/bigInt_zarith.ml → lib/ocaml/why3__BigInt_zarith.ml
View file @ beb4b0b8
......@@ -6,7 +6,6 @@ let compare = compare_big_int
let zero = zero_big_int
let one = unit_big_int
let of_int = big_int_of_int
let succ = succ_big_int
let pred = pred_big_int
......@@ -57,46 +56,15 @@ let pow_int_pos = power_int_positive_int
let to_string = string_of_big_int
let of_string = big_int_of_string
let to_int = int_of_big_int
let of_int = big_int_of_int
let to_int32 = int32_of_big_int
let of_int32 = big_int_of_int32
(* the code below is to be used in OCaml extracted code (see ocaml.drv) *)
let to_int64 = int64_of_big_int
let of_int64 = big_int_of_int64
let power x y = try power_big x y with Invalid_argument _ -> zero
let rec fact n = if le n one then one else mul n (fact (pred n))
let fib n =
let n = to_int n in
if n = 0 then zero else if n = 1 then one else
let a = Array.make (n + 1) zero in
a.(1) <- one; for i = 2 to n do a.(i) <- add a.(i-2) a.(i-1) done; a.(n)
let rec for_loop_to x1 x2 body =
if le x1 x2 then begin
body x1;
for_loop_to (succ x1) x2 body
end
let rec for_loop_downto x1 x2 body =
if ge x1 x2 then begin
body x1;
for_loop_downto (pred x1) x2 body
end
module Array = struct
type 'a t = 'a array
let get a i = a.(to_int i)
let set a i v = a.(to_int i) <- v
let length a = of_int (Array.length a)
exception OutOfBounds
let check_bounds a i = if i < 0 || i >= Array.length a then raise OutOfBounds
let defensive_get a i = let i = to_int i in check_bounds a i; a.(i)
let defensive_set a i v = let i = to_int i in check_bounds a i; a.(i) <- v
let make n v = Array.make (to_int n) v
let append = Array.append
let sub a ofs len = Array.sub a (to_int ofs) (to_int len)
let copy = Array.copy
let fill a ofs len v = Array.fill a (to_int ofs) (to_int len) v
let blit a1 ofs1 a2 ofs2 len =
Array.blit a1 (to_int ofs1) a2 (to_int ofs2) (to_int len)
end
lib/ocaml/why3__IntAux.ml 0 → 100644
View file @ beb4b0b8
open Why3__BigInt
let rec fact n = if le n one then one else mul n (fact (pred n))
let fib n =
let n = to_int n in
if n = 0 then zero else if n = 1 then one else
let a = Array.make (n + 1) zero in
a.(1) <- one; for i = 2 to n do a.(i) <- add a.(i-2) a.(i-1) done; a.(n)
let rec for_loop_to x1 x2 body =
if le x1 x2 then begin
body x1;
for_loop_to (succ x1) x2 body
end
let rec for_loop_downto x1 x2 body =
if ge x1 x2 then begin
body x1;
for_loop_downto (pred x1) x2 body
end
share/emacs/why3.el
View file @ beb4b0b8
......@@ -29,7 +29,7 @@
'("(\\*\\([^*)]\\([^*]\\|\\*[^)]\\)*\\)?\\*)" . font-lock-comment-face)
; '("{}\\|{[^|]\\([^}]*\\)}" . font-lock-type-face)
`(,(why3-regexp-opt '("invariant" "variant" "diverges" "requires" "ensures" "returns" "raises" "reads" "writes" "assert" "assume" "check")) . font-lock-type-face)
`(,(why3-regexp-opt '("use" "clone" "namespace" "import" "export" "coinductive" "inductive" "external" "constant" "function" "predicate" "val" "exception" "axiom" "lemma" "goal" "type" "mutable" "model" "abstract" "private" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "for" "to" "downto" "do" "done" "loop" "absurd" "ghost" "try" "with" "theory" "uses" "module")) . font-lock-keyword-face)
`(,(why3-regexp-opt '("use" "clone" "namespace" "import" "export" "coinductive" "inductive" "external" "constant" "function" "predicate" "val" "exception" "axiom" "lemma" "goal" "type" "mutable" "model" "abstract" "private" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "for" "to" "downto" "do" "done" "loop" "absurd" "ghost" "try" "with" "theory" "uses" "module" "converter")) . font-lock-keyword-face)