Commit d35cf9c3 authored by MARCHE Claude's avatar MARCHE Claude

extraction: support for modulo in machine ints

parent eb088088
......@@ -203,6 +203,7 @@ module mach.int.Int31
syntax val (-_) "( ~- )"
syntax val ( * ) "( * )"
syntax val ( / ) "( / )"
syntax val ( % ) "(mod)"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val (<=) "(<=)"
......@@ -224,6 +225,7 @@ module mach.int.UInt64
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 (<=) "(<=)"
......
......@@ -17,6 +17,7 @@ module mach.int.Int32
syntax val (-_) "Int32.neg"
syntax val ( * ) "Int32.mul"
syntax val (/) "Int32.div"
syntax val (%) "Int32.mod"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val (<=) "(<=)"
......@@ -37,6 +38,7 @@ module mach.int.UInt32
syntax val (-_) "Int64.neg"
syntax val ( * ) "Int64.mul"
syntax val (/) "Int64.div"
syntax val (%) "Int64.mod"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val (<=) "(<=)"
......@@ -57,6 +59,7 @@ module mach.int.Int63
syntax val (-_) "Int64.neg"
syntax val ( * ) "Int64.mul"
syntax val (/) "Int64.div"
syntax val (%) "Int64.mod"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val (<=) "(<=)"
......@@ -77,6 +80,7 @@ module mach.int.Int64
syntax val (-_) "Int64.neg"
syntax val ( * ) "Int64.mul"
syntax val (/) "Int64.div"
syntax val (%) "Int64.mod"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val (<=) "(<=)"
......
......@@ -15,6 +15,7 @@ module mach.int.Int32
syntax val (-_) "( ~- )"
syntax val ( * ) "( * )"
syntax val ( / ) "( / )"
syntax val ( % ) "(mod)"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val (<=) "(<=)"
......@@ -35,6 +36,7 @@ module mach.int.UInt32
syntax val (-_) "( ~- )"
syntax val ( * ) "( * )"
syntax val ( / ) "( / )"
syntax val ( % ) "(mod)"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val (<=) "(<=)"
......@@ -55,6 +57,7 @@ module mach.int.Int63
syntax val (-_) "( ~- )"
syntax val ( * ) "( * )"
syntax val ( / ) "( / )"
syntax val ( % ) "(mod)"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val (<=) "(<=)"
......@@ -75,6 +78,7 @@ module mach.int.Int64
syntax val (-_) "Int64.neg"
syntax val ( * ) "Int64.mul"
syntax val (/) "Int64.div"
syntax val (%) "Int64.mod"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val (<=) "(<=)"
......
......@@ -86,3 +86,21 @@ module BinaryGcd
else binary_gcd ((u - v) / 2) v
end
module EuclideanAlgorithm31
use import mach.int.Int31
use import number.Gcd
let rec euclid (u v: int31) : int31
variant { to_int v }
requires { to_int u >= 0 /\ to_int v >= 0 }
ensures { to_int result = gcd (to_int u) (to_int v) }
=
if Int31.eq v (of_int 0) then
u
else
euclid v (u % v)
end
BENCH ?= no
ifeq ($(BENCH),yes)
WHY3=../../bin/why3
WHY3SHARE=../../share
else
ifeq ($(BINDIR),)
WHY3=why3
else
WHY3=$(BINDIR)/why3
endif
WHY3SHARE=$(shell $(WHY3) --print-datadir)
endif
include $(WHY3SHARE)/Makefile.config
ifeq ($(BENCH),yes)
INCLUDE += -I ../../lib/why3
endif
MAIN=main
GEN=gcd__EuclideanAlgorithm31
OBJ=$(GEN)
GENML = $(addsuffix .ml, $(GEN))
ML = $(addsuffix .ml, $(OBJ))
CMO = $(addsuffix .cmo, $(OBJ))
CMX = $(addsuffix .cmx, $(OBJ))
OCAMLOPT=ocamlopt -noassert -inline 1000
all: $(MAIN).$(OCAMLBEST)
extract: $(GENML)
$(MAIN).opt: $(CMX) $(MAIN).cmx
$(OCAMLOPT) $(INCLUDE) $(BIGINTLIB).cmxa why3extract.cmxa -o $@ $^
$(MAIN).cmx: $(CMX)
$(GENML): ../gcd.mlw
$(WHY3) -E ocaml32 $< -o .
%.cmx: %.ml
$(OCAMLOPT) $(INCLUDE) -annot -c $<
clean::
rm -f $(GENML) *.cm[xio] *.o *.annot $(MAIN).opt $(MAIN).byte
rm -f gcd__*.ml*
# javascript
JSMAIN=jsmain
JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \
-syntax camlp4o
$(JSMAIN).js: $(JSMAIN).byte
js_of_ocaml -pretty -noinline $(JSMAIN).byte
$(JSMAIN).byte: $(ML) jsmain.ml
$(JSOCAMLC) $(INCLUDE) -o $@ -linkpkg $^
%.cmo: %.ml
$(JSOCAMLC) $(INCLUDE) -annot -c $<
%.cmi: %.mli
$(JSOCAMLC) $(INCLUDE) -annot -c $<
clean::
rm -f *.cm[io] $(NAME).byte $(NAME).js
(* computation part *)
let compute_result text =
try
let a,b = Scanf.sscanf text "%d %d" (fun x y -> x,y) in
string_of_int (Gcd__EuclideanAlgorithm31.euclid a b)
with _ -> "exception"
(* HTML rendering *)
module Html = Dom_html
let node x = (x : #Dom.node Js.t :> Dom.node Js.t)
let (<|) e l = List.iter (fun c -> Dom.appendChild e c) l; node e
let html_of_string (d : Html.document Js.t) (s:string) =
d##createElement (Js.string "p") <|
[node (d##createTextNode (Js.string s))]
let replace_child p n =
Js.Opt.iter (p##firstChild) (fun c -> Dom.removeChild p c);
Dom.appendChild p n
let onload (_event : #Html.event Js.t) : bool Js.t =
let d = Html.document in
let body =
Js.Opt.get (d##getElementById(Js.string "test"))
(fun () -> assert false) in
let textbox = Html.createTextarea d in
textbox##rows <- 20; textbox##cols <- 100;
let preview = Html.createDiv d in
preview##style##border <- Js.string "1px black";
preview##style##padding <- Js.string "5px";
Dom.appendChild body textbox;
Dom.appendChild body (Html.createBr d);
Dom.appendChild body preview;
let rec dyn_preview old_text n =
let text = Js.to_string (textbox##value) in
let n =
if text <> old_text then
begin
begin try
let rendered =
html_of_string d (compute_result text)
in
replace_child preview rendered
with _ -> ()
end;
20
end
else
max 0 (n - 1)
in
Lwt.bind
(Lwt_js.sleep (if n = 0 then 0.5 else 0.1))
(fun () -> dyn_preview text n)
in
let (_ : 'a Lwt.t) = dyn_preview "" 0 in Js._false
let (_ : unit) = Html.window##onload <- Html.handler onload
open Why3extract
open Format
let () =
printf "%d@."
(Gcd__EuclideanAlgorithm31.euclid (int_of_string Sys.argv.(1)) (int_of_string Sys.argv.(2)))
(*
let usage () =
eprintf "Reduction of combinator terms@.";
eprintf "Usage: %s <combinator term>@." Sys.argv.(0);
exit 2
let input =
if Array.length Sys.argv <> 2 then usage ();
Sys.argv.(1)
let input_term =
if input = "go" then
let i = Vstte12_combinators__Combinators.i in
Vstte12_combinators__Combinators.App(i,i)
else
try Parse.parse_term input
with _ ->
begin
eprintf "syntax error@.";
usage ()
end
let () =
let a = Vstte12_combinators__Combinators.reduction input_term in
printf "The normal form of %a is %a@."
Parse.pr input_term Parse.pr a
*)
......@@ -1097,5 +1097,169 @@
</transf>
</goal>
</theory>
<theory
name="EuclideanAlgorithm31"
locfile="../gcd.mlw"
loclnum="91" loccnumb="7" loccnume="27"
verified="true"
expanded="true">
<goal
name="WP_parameter euclid"
locfile="../gcd.mlw"
loclnum="96" loccnumb="10" loccnume="16"
expl="VC for euclid"
sum="c97bf923efd7df0ba08c127d1a0a44fc"
proved="true"
expanded="false"
shape="iainfix =ato_intV5agcdato_intV0ato_intV1Iainfix =ato_intV5agcdato_intV1ato_intV4FAainfix &gt;=ato_intV4c0Aainfix &gt;=ato_intV1c0Aainfix &lt;ato_intV4ato_intV1Aainfix &lt;=c0ato_intV1Iainfix =ato_intV4amodato_intV0ato_intV1FAain_boundsamodato_intV0ato_intV1ANainfix =ato_intV1c0ainfix =ato_intV0agcdato_intV0ato_intV1ainfix =V3aTrueIainfix =ato_intV1ato_intV2qainfix =V3aTrueFIainfix =ato_intV2c0FAain_boundsc0Iainfix &gt;=ato_intV1c0Aainfix &gt;=ato_intV0c0F">
<label
name="expl:VC for euclid"/>
<transf
name="split_goal_wp"
proved="true"
expanded="false">
<goal
name="WP_parameter euclid.1"
locfile="../gcd.mlw"
loclnum="96" loccnumb="10" loccnume="16"
expl="1. integer overflow"
sum="77cb7de9c98c14363e1d0cccb3d93c23"
proved="true"
expanded="false"
shape="integer overflowain_boundsc0Iainfix &gt;=ato_intV1c0Aainfix &gt;=ato_intV0c0F">
<label
name="expl:VC for euclid"/>
<proof
prover="1"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter euclid.2"
locfile="../gcd.mlw"
loclnum="96" loccnumb="10" loccnume="16"
expl="2. postcondition"
sum="760a5c0647aa2b256c67fccd062a7c6d"
proved="true"
expanded="false"
shape="postconditionainfix =ato_intV0agcdato_intV0ato_intV1Iainfix =V3aTrueIainfix =ato_intV1ato_intV2qainfix =V3aTrueFIainfix =ato_intV2c0FIain_boundsc0Iainfix &gt;=ato_intV1c0Aainfix &gt;=ato_intV0c0F">
<label
name="expl:VC for euclid"/>
<proof
prover="1"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter euclid.3"
locfile="../gcd.mlw"
loclnum="96" loccnumb="10" loccnume="16"
expl="3. division by zero"
sum="d297b1886e36e60a476d4915f1f12e29"
proved="true"
expanded="false"
shape="division by zeroNainfix =ato_intV1c0INainfix =V3aTrueIainfix =ato_intV1ato_intV2qainfix =V3aTrueFIainfix =ato_intV2c0FIain_boundsc0Iainfix &gt;=ato_intV1c0Aainfix &gt;=ato_intV0c0F">
<label
name="expl:VC for euclid"/>
<proof
prover="1"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter euclid.4"
locfile="../gcd.mlw"
loclnum="96" loccnumb="10" loccnume="16"
expl="4. integer overflow"
sum="744c070a0346ebb17972e8560fac031a"
proved="true"
expanded="false"
shape="integer overflowain_boundsamodato_intV0ato_intV1INainfix =V3aTrueIainfix =ato_intV1ato_intV2qainfix =V3aTrueFIainfix =ato_intV2c0FIain_boundsc0Iainfix &gt;=ato_intV1c0Aainfix &gt;=ato_intV0c0F">
<label
name="expl:VC for euclid"/>
<proof
prover="1"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.10"/>
</proof>
</goal>
<goal
name="WP_parameter euclid.5"
locfile="../gcd.mlw"
loclnum="96" loccnumb="10" loccnume="16"
expl="5. variant decrease"
sum="d62333ee6c251f02089dbb510e0984e9"
proved="true"
expanded="false"
shape="variant decreaseainfix &lt;ato_intV4ato_intV1Aainfix &lt;=c0ato_intV1Iainfix =ato_intV4amodato_intV0ato_intV1FIain_boundsamodato_intV0ato_intV1ANainfix =ato_intV1c0INainfix =V3aTrueIainfix =ato_intV1ato_intV2qainfix =V3aTrueFIainfix =ato_intV2c0FIain_boundsc0Iainfix &gt;=ato_intV1c0Aainfix &gt;=ato_intV0c0F">
<label
name="expl:VC for euclid"/>
<proof
prover="1"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.52"/>
</proof>
</goal>
<goal
name="WP_parameter euclid.6"
locfile="../gcd.mlw"
loclnum="96" loccnumb="10" loccnume="16"
expl="6. precondition"
sum="fcf15f9a34b89b8036e0b220e14b7d19"
proved="true"
expanded="false"
shape="preconditionainfix &gt;=ato_intV4c0Aainfix &gt;=ato_intV1c0Iainfix =ato_intV4amodato_intV0ato_intV1FIain_boundsamodato_intV0ato_intV1ANainfix =ato_intV1c0INainfix =V3aTrueIainfix =ato_intV1ato_intV2qainfix =V3aTrueFIainfix =ato_intV2c0FIain_boundsc0Iainfix &gt;=ato_intV1c0Aainfix &gt;=ato_intV0c0F">
<label
name="expl:VC for euclid"/>
<proof
prover="1"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="WP_parameter euclid.7"
locfile="../gcd.mlw"
loclnum="96" loccnumb="10" loccnume="16"
expl="7. postcondition"
sum="f477c5b2208489e4d744cadca57ab81f"
proved="true"
expanded="false"
shape="postconditionainfix =ato_intV5agcdato_intV0ato_intV1Iainfix =ato_intV5agcdato_intV1ato_intV4FIainfix &gt;=ato_intV4c0Aainfix &gt;=ato_intV1c0Iainfix =ato_intV4amodato_intV0ato_intV1FIain_boundsamodato_intV0ato_intV1ANainfix =ato_intV1c0INainfix =V3aTrueIainfix =ato_intV1ato_intV2qainfix =V3aTrueFIainfix =ato_intV2c0FIain_boundsc0Iainfix &gt;=ato_intV1c0Aainfix &gt;=ato_intV0c0F">
<label
name="expl:VC for euclid"/>
<proof
prover="1"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.54"/>
</proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
......@@ -6,11 +6,16 @@ let compute_result text =
try
let t = Parse.parse_term text in
let u = Vstte12_combinators__Combinators.reduction t in
Format.fprintf Format.str_formatter
Format.fprintf Format.str_formatter
"the normal form is %a" Parse.pr u;
Format.flush_str_formatter ()
with Parse.SyntaxError -> "syntax error"
(* HTML rendering *)
module Html = Dom_html
......@@ -43,7 +48,7 @@ let onload (_event : #Html.event Js.t) : bool Js.t =
let rec dyn_preview old_text n =
let text = Js.to_string (textbox##value) in
let n =
if text <> old_text then
if text <> old_text then
begin
begin try
let rendered =
......@@ -53,7 +58,7 @@ let onload (_event : #Html.event Js.t) : bool Js.t =
with _ -> ()
end;
20
end
end
else
max 0 (n - 1)
in
......
......@@ -66,8 +66,8 @@ let of_int32 = big_int_of_int32
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
let power x y =
try power_big_int_positive_big_int x y
with Invalid_argument _ -> zero
let print n = Pervasives.print_string (to_string n)
......
......@@ -97,6 +97,11 @@ module Bounded_int
requires { "expl:integer overflow" in_bounds (div (to_int a) (to_int b)) }
ensures { to_int result = div (to_int a) (to_int b) }
val (%) (a:t) (b:t) : t
requires { "expl:division by zero" to_int b <> 0 }
requires { "expl:integer overflow" in_bounds (mod (to_int a) (to_int b)) }
ensures { to_int result = mod (to_int a) (to_int b) }
end
module Int31
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment