Skip to content

GitLab

why3
why3
Commit 3b4dee5e authored by Raphaël Rieu-Helft's avatar Raphaël Rieu-Helft
Browse files
Options

Translation to C done for mp2.Main

parent a82e8491
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 1530 additions and 1372 deletions
drivers/c.drv
View file @ 3b4dee5e
printer "c"
module ref.Ref
syntax type ref "%1"
end
module mach.int.Int32
syntax val of_int "%1"
syntax converter of_int "%1"
syntax type int32 "int"
syntax val (+) "(%1 + %2)"
syntax val (-) "(%1 - %2)"
syntax val (*) "(%1 * %2)"
syntax val (/) "(%1 / %2)"
syntax val (%) "(%1 % %2)"
syntax val eq "(%1 = %2)"
syntax val ne "(%1 != %2)"
syntax val (<=) "(%1 <= %2)"
syntax val (<) "(%1 < %2)"
syntax val (>=) "(%1 >= %2)"
syntax val (>) "(%1 > %2)"
end
module mach.int.UInt32
syntax val of_int "%1"
syntax converter of_int "%1"
syntax constant zero_unsigned "0"
syntax type uint32 "unsigned int"
syntax val (+) "(%1 + %2)"
syntax val (-) "(%1 - %2)"
syntax val (*) "(%1 * %2)"
syntax val (/) "(%1 / %2)"
syntax val (%) "(%1 % %2)"
syntax val eq "(%1 = %2)"
syntax val ne "(%1 != %2)"
syntax val (<=) "(%1 <= %2)"
syntax val (<) "(%1 < %2)"
syntax val (>=) "(%1 >= %2)"
syntax val (>) "(%1 > %2)"
end
module mach.c.C
syntax type ptr "(%1 *)"
syntax val malloc "malloc(%1 * sizeof(%v0))" (* and not %t1 ? *)
syntax val free "free(%1)"
syntax val realloc "realloc(%1, %2 * sizeof(%v0))"
syntax val is_null "%1 == NULL"
syntax val null "NULL"
syntax val get "*(%1)"
syntax val set "*(%1) = %2"
syntax val p2i "%1"
syntax converter p2i "%1"
end
\ No newline at end of file
examples/in_progress/multiprecision/Makefile 0 → 100644
View file @ 3b4dee5e
extract:
why3 extract -D c -o build mp2.mlw -T Main
examples/in_progress/multiprecision/build/.gitignore 0 → 100644
View file @ 3b4dee5e
# Ignore everything in this directory
*
# Except this file
!.gitignore
examples/in_progress/multiprecision/mp2.mlw
View file @ 3b4dee5e
......@@ -54,15 +54,6 @@ module N
function value_sub_shift (x:t) (sz:int) : int =
value_sub (pelts x) x.offset (x.offset + sz)
let from_limb (l:limb) : t
ensures { is_null result \/ plength result = 1 }
ensures { is_null result \/ value_sub_shift result 1 = l2i l }
=
let p = malloc (UInt32.of_int 1) in
if not (is_null p)
then C.set p l;
p
use map.MapEq
use map.Const
......@@ -2121,11 +2112,26 @@ module N
assert { l2i !qh * l2i d + l2i !r = l2i ul + radix * l2i uh };
(!qh,!r)
let main () = from_limb (Limb.of_int 42)
end
module Main
use import mach.c.C
use import N
let from_limb (l:limb) : t
ensures { is_null result \/ plength result = 1 }
ensures { is_null result \/ value_sub_shift result 1 = l2i l }
=
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)
end
(*
......
examples/in_progress/multiprecision/mp2/why3session.xml
View file @ 3b4dee5e
......@@ -10,56 +10,13 @@
<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="M" sum="0603561430b9544178c14214fd469819" expanded="true">
<goal name="VC incr" expl="VC for incr">
<proof prover="3"><result status="valid" time="0.02" steps="69"/></proof>
</goal>
<goal name="VC get_ofs" expl="VC for get_ofs">
<proof prover="3"><result status="valid" time="0.02" steps="78"/></proof>
</goal>
<goal name="VC set_ofs" expl="VC for set_ofs">
<proof prover="3"><result status="valid" time="0.04" steps="81"/></proof>
</goal>
<goal name="VC valid_itv_to_shift" expl="VC for valid_itv_to_shift">
<proof prover="3"><result status="valid" time="0.04" steps="77"/></proof>
</goal>
</theory>
<theory name="N" sum="35626f1aeac1eb590f4fe0c42e90ce44" expanded="true">
<theory name="N" sum="0fd57e69a4e5a85538b534b92177aa8f" expanded="true">
<goal name="limb_max_bound">
<proof prover="3"><result status="valid" time="0.02" steps="69"/></proof>
</goal>
<goal name="VC value_sub" expl="VC for value_sub">
<proof prover="3"><result status="valid" time="0.02" steps="71"/></proof>
</goal>
<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">
<proof prover="3"><result status="valid" time="0.03" steps="71"/></proof>
</goal>
<goal name="VC from_limb.2" expl="2. precondition">
<transf name="split_goal_wp">
<goal name="VC from_limb.2.1" expl="1. VC for from_limb">
<proof prover="3"><result status="valid" time="0.03" steps="75"/></proof>
</goal>
<goal name="VC from_limb.2.2" expl="2. VC for from_limb">
<proof prover="3"><result status="valid" time="0.04" steps="75"/></proof>
</goal>
</transf>
</goal>
<goal name="VC from_limb.3" expl="3. postcondition">
<proof prover="3"><result status="valid" time="0.03" steps="82"/></proof>
</goal>
<goal name="VC from_limb.4" expl="4. postcondition">
<proof prover="3"><result status="valid" time="0.07" steps="116"/></proof>
</goal>
<goal name="VC from_limb.5" expl="5. postcondition">
<proof prover="3"><result status="valid" time="0.02" steps="74"/></proof>
</goal>
<goal name="VC from_limb.6" expl="6. postcondition">
<proof prover="3"><result status="valid" time="0.02" steps="74"/></proof>
</goal>
</transf>
</goal>
<goal name="VC map_eq_shift" expl="VC for map_eq_shift">
<proof prover="3"><result status="valid" time="0.02" steps="74"/></proof>
</goal>
......@@ -75,7 +32,15 @@
<proof prover="3"><result status="valid" time="0.04" steps="72"/></proof>
</goal>
<goal name="VC map_eq_shift_zero.4" expl="4. precondition">
<proof prover="3"><result status="valid" time="5.95" steps="511"/></proof>
<transf name="introduce_premises">
<goal name="VC map_eq_shift_zero.4.1" expl="1. precondition">
<transf name="inline_goal">
<goal name="VC map_eq_shift_zero.4.1.1" expl="1. precondition">
<proof prover="3"><result status="valid" time="1.41" steps="293"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC map_eq_shift_zero.5" expl="5. assertion">
<proof prover="3"><result status="valid" time="0.02" steps="72"/></proof>
......@@ -106,7 +71,7 @@
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC value_sub_frame_shift.5" expl="5. precondition">
<proof prover="3"><result status="valid" time="0.68" steps="163"/></proof>
<proof prover="3"><result status="valid" time="0.51" steps="163"/></proof>
</goal>
<goal name="VC value_sub_frame_shift.6" expl="6. assertion">
<proof prover="4"><result status="valid" time="0.01"/></proof>
......@@ -204,7 +169,7 @@
<goal name="VC value_sub_upper_bound" expl="VC for value_sub_upper_bound">
<transf name="split_goal_wp">
<goal name="VC value_sub_upper_bound.1" expl="1. assertion">
<proof prover="1"><result status="valid" time="0.88"/></proof>
<proof prover="1"><result status="valid" time="1.42"/></proof>
</goal>
<goal name="VC value_sub_upper_bound.2" expl="2. variant decrease">
<proof prover="4"><result status="valid" time="0.02"/></proof>
......@@ -1143,10 +1108,10 @@
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC sub_limbs.16.9" expl="9. VC for sub_limbs">
<proof prover="3"><result status="valid" time="0.60" steps="122"/></proof>
<proof prover="3"><result status="valid" time="0.79" steps="122"/></proof>
</goal>
<goal name="VC sub_limbs.16.10" expl="10. VC for sub_limbs">
<proof prover="3"><result status="valid" time="0.56" steps="121"/></proof>
<proof prover="3"><result status="valid" time="0.75" steps="121"/></proof>
</goal>
<goal name="VC sub_limbs.16.11" expl="11. VC for sub_limbs">
<proof prover="2"><result status="valid" time="0.07"/></proof>
......@@ -1252,10 +1217,10 @@
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC sub.16.8" expl="8. VC for sub">
<proof prover="3"><result status="valid" time="0.64" steps="128"/></proof>
<proof prover="3"><result status="valid" time="0.85" steps="128"/></proof>
</goal>
<goal name="VC sub.16.9" expl="9. VC for sub">
<proof prover="3"><result status="valid" time="0.57" steps="127"/></proof>
<proof prover="3"><result status="valid" time="0.80" steps="127"/></proof>
</goal>
<goal name="VC sub.16.10" expl="10. VC for sub">
<proof prover="0"><result status="valid" time="0.06"/></proof>
......@@ -1687,7 +1652,7 @@
<proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC addmul_limb.26" expl="26. loop invariant preservation">
<proof prover="0"><result status="valid" time="6.11"/></proof>
<proof prover="0"><result status="valid" time="5.29"/></proof>
</goal>
<goal name="VC addmul_limb.27" expl="27. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.19"/></proof>
......@@ -1821,7 +1786,7 @@
<proof prover="0"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="VC mul_limbs.23.2" expl="2. VC for mul_limbs">
<proof prover="0"><result status="valid" time="4.96"/></proof>
<proof prover="0"><result status="valid" time="4.10"/></proof>
</goal>
</transf>
</goal>
......@@ -2163,7 +2128,7 @@
<goal name="VC addmul_limbs.36.2" expl="2. VC for addmul_limbs">
<transf name="inline_all">
<goal name="VC addmul_limbs.36.2.1" expl="1. VC for addmul_limbs">
<proof prover="0"><result status="valid" time="0.62"/></proof>
<proof prover="0"><result status="valid" time="0.44"/></proof>
</goal>
</transf>
</goal>
......@@ -2897,7 +2862,7 @@
<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"><result status="timeout" time="9.50"/></proof>
<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>
......@@ -2951,7 +2916,7 @@
<goal name="VC lshift.44" expl="44. postcondition">
<transf name="inline_all">
<goal name="VC lshift.44.1" expl="1. postcondition">
<proof prover="1"><result status="valid" time="1.24"/></proof>
<proof prover="1"><result status="valid" time="0.58"/></proof>
</goal>
</transf>
</goal>
......@@ -3724,7 +3689,7 @@
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div2by1_inv.25.12" expl="12. VC for div2by1_inv">
<proof prover="2"><result status="valid" time="0.78"/></proof>
<proof prover="2"><result status="valid" time="1.01"/></proof>
</goal>
<goal name="VC div2by1_inv.25.13" expl="13. VC for div2by1_inv">
<proof prover="3"><result status="valid" time="0.15" steps="118"/></proof>
......@@ -4033,9 +3998,32 @@
</goal>
</transf>
</goal>
</theory>
<theory name="Main" sum="1b5018d2448537aeb1d3eb3e920619ba">
<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">
<proof prover="3"><result status="valid" time="0.03" steps="72"/></proof>
</goal>
<goal name="VC from_limb.2" expl="2. precondition">
<proof prover="3"><result status="valid" time="0.03" steps="76"/></proof>
</goal>
<goal name="VC from_limb.3" expl="3. postcondition">
<proof prover="3"><result status="valid" time="0.05" steps="83"/></proof>
</goal>
<goal name="VC from_limb.4" expl="4. postcondition">
<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>
</goal>
<goal name="VC from_limb.6" expl="6. 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" obsolete="true"><result status="valid" time="0.02" steps="72"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="72"/></proof>
</goal>
</theory>
</file>
......
src/mlw/cprinter.ml
View file @ 3b4dee5e
open Ident
exception Unsupported of string
exception NoSyntax of string
module C = struct
type ty =
......@@ -61,6 +64,7 @@ module C = struct
and definition =
| Dfun of ident * proto * body
| Dinclude of ident
| Ddecl of names
| Dtypedef of ty * ident
| Dstructural of names (* struct, union... *)
......@@ -84,6 +88,76 @@ module C = struct
| Sbreak -> raise NotAValue
| Sreturn _ -> raise NotAValue
let rec propagate_in_expr id (v:expr) = function
| Evar i when Ident.id_equal i id -> v
| Evar i -> Evar i
| Eunop (u,e) -> Eunop (u, propagate_in_expr id v e)
| Ebinop (b,e1,e2) -> Ebinop (b,
propagate_in_expr id v e1,
propagate_in_expr id v e2)
| Eternary (c,t,e) -> Eternary (propagate_in_expr id v c,
propagate_in_expr id v t,
propagate_in_expr id v e)
| Ecast (ty,e) -> Ecast (ty, propagate_in_expr id v e)
| Ecall (e, l) -> Ecall (propagate_in_expr id v e,
List.map (propagate_in_expr id v) l)
| Esize_expr e -> Esize_expr (propagate_in_expr id v e)
| Eindex (e1,e2) -> Eindex (propagate_in_expr id v e1,
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)
| Enothing -> Enothing
| Econst c -> Econst c
| Esize_type ty -> Esize_type ty
let rec propagate_in_stmt id v = function
| Sexpr e -> Sexpr (propagate_in_expr id v e)
| Sblock b -> Sblock(propagate_in_block id v b)
| Sseq (s1,s2) -> Sseq (propagate_in_stmt id v s1,
propagate_in_stmt id v s2)
| Sif (e,s1,s2) -> Sif (propagate_in_expr id v e,
propagate_in_stmt id v s1,
propagate_in_stmt id v s2)
| Swhile (e, s) -> Swhile (propagate_in_expr id v e,
propagate_in_stmt id v s)
| Sfor (e1,e2,e3,s) -> Sfor (propagate_in_expr id v e1,
propagate_in_expr id v e2,
propagate_in_expr id v e3,
propagate_in_stmt id v s)
| Sreturn e -> Sreturn (propagate_in_expr id v e)
| Snop -> Snop
| Sbreak -> Sbreak
and propagate_in_def id v d =
let rec aux = function
| [] -> [], true
| (i,e)::t ->
if Ident.id_equal i id then (i,e)::t, false
else let t,b = aux t in ((i,propagate_in_expr id v e)::t), b
in
match d with
| Ddecl (ty,l) ->
let l,b = aux l in
Ddecl (ty, l), b
| Dinclude i -> Dinclude i, true
| Dfun _ -> raise (Unsupported "nested function")
| Dtypedef _ -> raise (Unsupported "typedef inside body")
| Dstructural (ty,l) ->
let l,b = aux l in
Dstructural (ty, l), b
and propagate_in_block id v (dl, s) =
let dl, b = List.fold_left
(fun (dl, acc) d ->
if acc
then
let d, b = propagate_in_def id v d in
(d::dl, b)
else (d::dl, false))
([],true) dl in
(List.rev dl, if b then propagate_in_stmt id v s else s)
end
type info = Pdriver.printer_args = private {
......@@ -102,8 +176,7 @@ module Translate = struct
open Expr
open Term
open Printer
exception Unsupported of string
open Pmodule
let ty_of_ty info ty =
match ty.ty_node with
......@@ -117,14 +190,14 @@ module Translate = struct
begin match query_syntax info.syntax ts.ts_name
with
| Some s -> C.Tsyntax s (*TODO something with the %[tv][1-9] logic ?*)
| None -> assert false
| None -> raise (NoSyntax ts.ts_name.id_string)
end
let ty_of_ts info ts =
match query_syntax info.syntax ts.ts_name
with
| Some s -> C.Tsyntax s (*TODO something with the %[tv][1-9] logic ?*)
| None -> assert false
| None -> raise (NoSyntax ts.ts_name.id_string)
let ty_of_ity info ity =
match ity.ity_node with
......@@ -133,17 +206,18 @@ module Translate = struct
| Some s -> C.Tsyntax s
| None -> C.Tnamed (tv.tv_name)
end
| Ityapp (its,_,_) ->
ty_of_ts info its.its_ts
| Ityreg _ -> assert false
| Ityapp (its,_,_) | Ityreg {reg_its=its} -> ty_of_ts info its.its_ts
let pv_name pv = pv.pv_vs.vs_name
let rec expr info (e:expr) : C.body =
match e.e_node with
| Evar pv -> C.([], Sexpr(Evar (pv_name pv)))
| Econst c -> assert false (*TODO*)
| Eexec (ce, cty) ->
| Econst (Number.ConstInt ic) ->
let n = Number.compute_int ic in
C.([], Sexpr(Econst (Cint (BigInt.to_string n))))
| Econst _ -> assert false (*TODO*)
| Eexec (ce, _cty) ->
begin match ce.c_node with
| Cfun e -> expr info e
| Capp (rs, pvsl) ->
......@@ -157,12 +231,22 @@ module Translate = struct
| Elet (ld,e) ->
begin match ld with
| LDvar (pv,le) ->
Format.printf "let %s@." pv.pv_vs.vs_name.id_string;
if pv.pv_ghost then expr info e
else
let t = ty_of_ity info pv.pv_ity in
let initblock = expr info le in
[ C.Ddecl (t, [pv_name pv, C.Enothing]) ],
C.Sseq (C.Sblock initblock, C.Sblock (expr info e))
else if ((pv_name pv).id_string = "_" && ity_equal pv.pv_ity ity_unit)
then ([], C.Sseq (C.Sblock(expr info le), C.Sblock(expr info e)))
else begin
match le.e_node with
| Econst (Number.ConstInt ic) ->
let n = Number.compute_int ic in
let cexp = C.(Econst (Cint (BigInt.to_string n))) in
C.propagate_in_block (pv_name pv) cexp (expr info e)
| _->
let t = ty_of_ity info pv.pv_ity in
let initblock = expr info le in
[ C.Ddecl (t, [pv_name pv, C.Enothing]) ],
C.Sseq (C.Sblock initblock, C.Sblock (expr info e))
end
| _ -> assert false
end
| Eif (c, t, e) ->
......@@ -185,7 +269,7 @@ module Translate = struct
[C.Ddecl (C.Tsyntax "int", [cid, C.Enothing])],
C.Sseq (C.Sblock (cd, cs), C.Swhile (C.Evar cid, C.Sblock b))
end
| Etry _ | Eraise _ -> assert false (*TODO*)
| Etry _ | Eraise _ -> raise (Unsupported "try/exceptions") (*TODO*)
| Efor _ -> assert false (*TODO*)
| Eassert _ -> [], C.Snop
| Eghost _ | Epure _ | Ecase _ | Eabsurd -> assert false
......@@ -193,29 +277,64 @@ module Translate = struct
let pdecl info (pd:Pdecl.pdecl) : C.definition list =
match pd.pd_node with
| PDlet (LDsym (rs, ce)) ->
begin match ce.c_node with
| Cfun e ->
let fname = rs.rs_name in
let rtype = match rs.rs_cty.cty_result.ity_node with
| Ityapp (its, _,_) ->
ty_of_ts info its.its_ts
| _ -> assert false
in
let fname = rs.rs_name in
Format.printf "PDlet rsymbol %s@." fname.id_string;
begin try
if Mid.mem fname info.syntax then []
else
let params = List.map
(fun pv -> ty_of_ty info pv.pv_vs.vs_ty, pv_name pv)
(List.filter (fun pv -> not pv.pv_ghost) rs.rs_cty.cty_args) in
[C.Dfun (fname, (rtype,params), expr info e)]
| _ -> assert false
(List.filter
(fun pv -> not pv.pv_ghost && not (ity_equal pv.pv_ity ity_unit))
rs.rs_cty.cty_args) in
match ce.c_node with
| Cfun e ->
let rtype = match rs.rs_cty.cty_result.ity_node with
| Ityapp (its, _,_) ->
ty_of_ts info its.its_ts
| _ ->
raise (Unsupported "variable return type")
in
[C.Dfun (fname, (rtype,params), expr info e)]
| _ -> raise (Unsupported "Non-function with no syntax in toplevel let")
with
NoSyntax s ->
Format.printf "%s has no syntax : not extracted@." s;
[]
end
| PDtype [{itd_its = ity}] ->
let id = ity.its_ts.ts_name in
[C.Dtypedef (ty_of_ts info ity.its_ts, id)]
| _ -> assert false
let translate (info:info) (m:Pmodule.pmodule) : C.file =
assert false
Format.printf "PDtype %s@." id.id_string;
let def =
match ity.its_ts.ts_def with
| Some def -> ty_of_ty info def
| None ->
begin match query_syntax info.syntax id with
| Some s -> C.Tsyntax s
| None ->
raise (Unsupported "type declaration without syntax or alias")
end
in
[C.Dtypedef (def, id)]
| _ -> [] (*TODO exn ? *)
let munit info = function
| Udecl pd -> pdecl info pd
| Uuse _ -> []
| Uclone _ -> raise (Unsupported "clone")
| Umeta _ -> raise (Unsupported "meta")
| Uscope _ -> []
let translate (info:info) (m:pmodule) : C.file =
Format.printf "Translating module %s@."
m.mod_theory.Theory.th_name.id_string;
try List.flatten (List.map (munit info) m.mod_units)
with
| Unsupported s ->
Format.printf "Failed because of unsupported construct: %s@." s; []
| NoSyntax s ->
Format.printf "Failed because %s has no syntax@." s; []
end
let fg ?fname m =
......@@ -226,25 +345,9 @@ let fg ?fname m =
open Format
(*
decl : d:pdecl -> Cdefinition list
cas sur d.pd_node:
1: PDlet (LDsym (rs: routine symbol) (expr)
pr_unit : mod_unit -> Cdefinition list
cas numero 1: Udecl d -> appeler fonction decl
*)
let pr args ?old fmt m =
ignore(args);
ignore(old);
ignore(m);
let _ast = Translate.translate args m in
(* TODO:
iterer sur m.mod_units la fonction pr_unit
*)
......
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