Commit 3d0417e8 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

Fix session + merge

parent 7a677d7c
......@@ -41,9 +41,9 @@ module N
lemma limb_max_bound: 1 <= max_uint64
let ghost function l2i (x:limb) : int = Limb.to_int x
function l2i (x:limb) : int = Limb.to_int x
let ghost function p2i (i:int32) : int = Int32.to_int i
function p2i (i:int32) : int = Int32.to_int i
exception Break
exception Return32 int32
......@@ -182,7 +182,7 @@ module N
use import mach.c.C
type t = ptr limb
let ghost function value (x:t) (sz:int) : int =
function value (x:t) (sz:int) : int =
value_sub (pelts x) x.offset (x.offset + sz)
function compare_int (x y:int) : int =
......@@ -1556,8 +1556,8 @@ module N
else
begin
let (r:limb,d:limb) = lsld x cnt in
let p = power 2 (l2i cnt) in
let q = power 2 (Limb.length - l2i cnt) in
let ghost p = power 2 (l2i cnt) in
let ghost q = power 2 (Limb.length - l2i cnt) in
assert { p > 0 /\ q > 0 };
assert { radix = p * q by
radix = power 2 Limb.length = power 2 (cnt + (Limb.length - cnt))
......
......@@ -480,387 +480,7 @@ module Print = struct
fprintf fmt "@[<v>%a@]@." (print_list newline print_def) ast
end
(*
module Translate = struct
open Pdecl
open Ity
open Ty
open Expr
open Term
open Printer
open Pmodule
let rec ty_of_ty info ty =
match ty.ty_node with
| Tyvar v ->
begin match query_syntax info.syntax v.tv_name
with
| Some s -> C.Tsyntax (s, [])
| None -> C.Tnamed (v.tv_name)
end
| Tyapp (ts, tl) ->
begin match query_syntax info.syntax ts.ts_name
with
| Some s -> C.Tsyntax (s, List.map (ty_of_ty info) tl)
| None -> C.Tnosyntax
end
let pv_name pv = pv.pv_vs.vs_name
type syntax_env = { in_unguarded_loop : bool;
computes_return_value : bool;
returns_tuple: bool * ident list;
breaks : Sid.t;
returns : Sid.t; }
let rec expr info env (e:expr) : C.body =
if e_ghost e
then (if debug then Format.printf "translating ghost expr@."; C.([], Snop))
else if is_e_void e then
if env.computes_return_value
then C.([], Sreturn(Enothing))
else C.([], Snop)
else if is_e_true e then expr info env (e_nat_const 1)
else if is_e_false e then expr info env (e_nat_const 0)
else match e.e_node with
| Evar pv ->
let e = C.Evar(pv_name pv) in
C.([], if env.computes_return_value then Sreturn e else Sexpr e)
| Econst (Number.ConstInt ic) ->
let n = Number.compute_int ic in
let e = C.(Econst (Cint (BigInt.to_string n))) in
C.([], if env.computes_return_value then Sreturn e else Sexpr e)
| Econst _ -> raise (Unsupported "real constants")
| Eexec (ce, _cty) ->
begin match ce.c_node with
| Cfun e -> expr info env e
| Capp (rs, pvsl) ->
if is_rs_tuple rs && env.computes_return_value
then begin
match env.returns_tuple with
| true, rl ->
let args =
List.filter
(fun pv -> not (pv.pv_ghost
|| ity_equal pv.pv_ity ity_unit))
pvsl
in
assert (List.length rl = List.length args);
C.([],
List.fold_right2 (fun res arg acc ->
Sseq(Sexpr(Ebinop(Bassign,
Eunop(Ustar,Evar(res)),
Evar(pv_name arg))),
acc))
rl args (Sreturn(Enothing)))
| _ -> assert false
end
else
let e =
match
(query_syntax info.syntax rs.rs_name,
query_syntax info.converter rs.rs_name) with
| _, Some s
| Some s, _ ->
begin
try
let _ = Str.search_forward
(Str.regexp "[%]\\([tv]?\\)[0-9]+") s 0 in
let params =
List.map (fun pv -> (C.Evar(pv_name pv),
ty_of_ty info (ty_of_ity pv.pv_ity)))
pvsl in
let rty = ty_of_ity e.e_ity in
let rtyargs = match rty.ty_node with
| Tyvar _ -> [||]
| Tyapp (_,args) ->
Array.of_list (List.map (ty_of_ty info) args)
in
C.Esyntax(s,ty_of_ty info rty, rtyargs, params,
Mid.mem rs.rs_name info.converter)
with Not_found ->
let args = List.filter
(fun pv -> not (pv.pv_ghost
|| ity_equal pv.pv_ity ity_unit))
pvsl in
if pvsl=[]
then C.(Esyntax(s, Tnosyntax, [||], [], true)) (*constant*)
else
(*function defined in the prelude *)
C.(Ecall(Esyntax(s, Tnosyntax, [||], [], true),
List.map (fun pv -> Evar(pv_name pv)) args))
end
| _ ->
let args = List.filter
(fun pv -> not (pv.pv_ghost
|| ity_equal pv.pv_ity ity_unit))
pvsl in
C.(Ecall(Evar(rs.rs_name),
List.map (fun pv -> Evar(pv_name pv)) args))
in
C.([],
if env.computes_return_value
then
if (ity_equal rs.rs_cty.cty_result ity_unit)
then Sseq(Sexpr e, Sreturn Enothing)
else Sreturn e
else Sexpr e)
| _ -> raise (Unsupported "Cpur/Cany") (*TODO clarify*)
end
| Eassign _ -> raise (Unsupported "mutable field assign")
| Elet (ld,e) ->
begin match ld with
| LDvar (pv,le) ->
(*if debug then Format.printf "let %s@." pv.pv_vs.vs_name.id_string;*)
if pv.pv_ghost
(*TODO check it's actually unused *)
then expr info env e
else if ity_equal pv.pv_ity ity_unit
|| pv.pv_vs.vs_name.id_string = "_"
then let env' = {env with computes_return_value = false} in
([], C.Sseq (C.Sblock(expr info env' le),
C.Sblock(expr info env e)))
else begin
match le.e_node with
| Econst (Number.ConstInt ic) ->
let n = Number.compute_int ic in
let ce = C.(Econst (Cint (BigInt.to_string n))) in
if debug then Format.printf "propagate constant %s for var %s@."
(BigInt.to_string n) (pv_name pv).id_string;
C.propagate_in_block (pv_name pv) ce (expr info env e)
| Eexec ({c_node = Capp(rs,_); _},_)
when Mid.mem rs.rs_name info.converter ->
begin match expr info {env with computes_return_value = false} le
with
| [], C.Sexpr(se) ->
C.propagate_in_block (pv_name pv) se (expr info env e)
| _ -> assert false
end
| _->
let t = ty_of_ty info (ty_of_ity pv.pv_ity) in
match expr info {env with computes_return_value = false} le with
| [], C.Sexpr((C.Esyntax(_,_,_,_,b) as se))
when b (* converter *) ->
if debug then Format.printf "propagate converter for var %s@."
(pv_name pv).id_string;
C.propagate_in_block (pv_name pv) se (expr info env e)
| d,s ->
let initblock = d, C.assignify (C.Evar (pv_name pv)) s in
[ C.Ddecl (t, [pv_name pv, C.Enothing]) ],
C.Sseq (C.Sblock initblock, C.Sblock (expr info env e))
end
| LDsym _ -> raise (Unsupported "LDsym")
| LDrec _ -> raise (Unsupported "LDrec") (* TODO for rec at least*)
end
| Eif (cond, th, el) ->
let c = expr info {env with computes_return_value = false} cond in
let t = expr info env th in
let e = expr info env el in
begin match c with
| [], C.Sexpr c ->
if is_e_false th && is_e_true el
then C.([], Sexpr(Eunop(Unot, c)))
else [], C.Sif(c,C.Sblock t, C.Sblock e)
| cdef, cs ->
let cid = id_register (id_fresh "cond") in (* ? *)
C.Ddecl (C.Tsyntax ("int",[]), [cid, C.Enothing])::cdef,
C.Sseq (C.assignify (C.Evar cid) cs,
C.Sif (C.Evar cid, C.Sblock t, C.Sblock e))
(* TODO detect empty branches and replace with Snop, detect and/or*)
end
| Ewhile (c,_,_,b) ->
if debug then Format.printf "while@.";
let cd, cs = expr info {env with computes_return_value = false} c in
(* this is needed so that the extracted expression has all
needed variables in its scope *)
let cd, cs = C.flatten_defs cd cs in
let cd = C.group_defs_by_type cd in
let env' = { computes_return_value = false;
in_unguarded_loop = true;
returns_tuple = env.returns_tuple;
returns = env.returns;
breaks =
if env.in_unguarded_loop
then Sid.empty else env.breaks } in
let b = expr info env' b in
begin match cs with
| C.Sexpr ce -> cd, C.Swhile (ce, C.Sblock b)
| _ ->
begin match C.get_last_expr cs with
| C.Snop, e -> cd, C.(Swhile(e, C.Sblock b))
| s,e -> cd, C.(Swhile(Econst (Cint "1"),
Sseq(s,
Sseq(Sif(Eunop(Unot, e), Sbreak, Snop),
C.Sblock b))))
end
end
| Etry (b, exm) ->
if debug then Format.printf "TRY@.";
let is_while = match b.e_node with Ewhile _ -> true | _-> false in
let breaks,returns = Mxs.fold
(fun xs (pvsl,r) (bs,rs) ->
let id = xs.xs_name in
match pvsl, r.e_node with
| [pv], Evar pv' when pv_equal pv pv' && env.computes_return_value ->
(bs, Sid.add id rs)
| [], _ when is_e_void r && is_while (*FIXME*) ->
(Sid.add id bs, rs)
|_ -> raise (Unsupported "non break/return exception in try"))
exm (Sid.empty, env.returns)
in
let env' = { computes_return_value = env.computes_return_value;
in_unguarded_loop = false;
returns_tuple = env.returns_tuple;
breaks = breaks;
returns = returns;
} in
expr info env' b
| Eraise (xs,_) when Sid.mem xs.xs_name env.breaks ->
if debug then Format.printf "BREAK@.";
([], C.Sbreak)
| Eraise (xs,r) when Sid.mem xs.xs_name env.returns ->
if debug then Format.printf "RETURN@.";
expr info {env with computes_return_value = true} r
| Eraise _ -> raise (Unsupported "non break/return exception raised")
| Efor _ -> raise (Unsupported "for loops") (*TODO*)
| Eassert _ -> [], C.Snop
(* let (a,b) = f(...) in *)
| Ecase (e1,[{pp_pat = {pat_node = Papp(ls,rets)}}, e2])
when is_fs_tuple ls
&& List.for_all (fun p ->
match p.pat_node with Pvar _ -> true |_-> false)
rets
->
let rets, defs = List.fold_right
(fun p (r, d)-> match p.pat_node with
| Pvar vs -> (C.(Eunop(Uaddr,Evar(vs.vs_name)))::r,
C.Ddecl(ty_of_ty info vs.vs_ty, [vs.vs_name, C.Enothing])::d)
| _ -> assert false )
rets ([], []) in
let d,s = expr info {env with computes_return_value = false} e1 in
let s' = C.add_to_last_call rets s in
let b = expr info env e2 in
d@defs, C.(Sseq(s', Sblock b))
| Ecase _ -> raise (Unsupported "pattern matching")
| Eghost _ | Epure _ | Eabsurd -> assert false
let pdecl info (pd:Pdecl.pdecl) : C.definition list =
match pd.pd_node with
| PDlet (LDsym (rs, ce)) ->
let fname = rs.rs_name in
if debug then Format.printf "PDlet rsymbol %s@." fname.id_string;
if rs_ghost rs
then begin if debug then Format.printf "is ghost@."; [] end
else
begin try
if Mid.mem fname info.syntax
then (if debug then Format.printf "has syntax@."; [])
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
&& not (ity_equal pv.pv_ity ity_unit))
rs.rs_cty.cty_args) in
begin match ce.c_node with
| Cfun e ->
let env = { computes_return_value = true;
in_unguarded_loop = false;
returns_tuple = false, [];
returns = Sid.empty;
breaks = Sid.empty; } in
let rity = rs.rs_cty.cty_result in
let is_simple_tuple ity =
let arity_zero = function
| Ityapp(_,a,r) -> a = [] && r = []
| Ityreg { reg_args = a; reg_regs = r } ->
a = [] && r = []
| Ityvar _ -> true
in
(match ity.ity_node with
| Ityapp ({its_ts = s},_,_)
| Ityreg { reg_its = {its_ts = s}; }
-> is_ts_tuple s
| _ -> false)
&& (ity_fold
(fun acc ity ->
acc && arity_zero ity.ity_node) true ity)
in
(* FIXME is it necessary to have arity 0 in regions ?*)
let rtype =
if ity_equal rity ity_unit
then C.Tvoid
else ty_of_ty info (ty_of_ity rity) in
let env, rtype, params = match rtype with
| C.Tnosyntax when is_simple_tuple rity ->
(* instead of returning a tuple, return
void and assign the result to addresses
passed as parameters *)
let returns =
let f ity b acc =
if b.its_visible
then (C.Tptr(ty_of_ty info (ty_of_ity ity)),
id_register (id_fresh "result"))::acc
else acc
in
match rity.ity_node with
| Ityapp(s, tl,_)
| Ityreg { reg_its = s; reg_args = tl } ->
List.fold_right2 f tl s.its_arg_flg []
| Ityvar _ -> assert false
in
{env with returns_tuple = true, List.map snd returns},
C.Tvoid,
returns@params
| _ -> env, rtype, params
in
let d,s = expr info env e in
(*TODO check if we want this flatten*)
let d,s = C.flatten_defs d s in
let d = C.group_defs_by_type d in
let s = C.elim_nop s in
let s = C.elim_empty_blocks s in
[C.Dfun (fname, (rtype,params), (d,s))]
| _ ->
raise
(Unsupported
"Non-function with no syntax in toplevel let")
end
with Unsupported s -> Format.printf "Unsupported : %s@." s; []
end
| PDtype [{itd_its = its}] ->
let id = its.its_ts.ts_name in
if debug then Format.printf "PDtype %s@." id.id_string;
begin
match its.its_ts.ts_def with
| Alias def -> [C.Dtypedef (ty_of_ty info def, id)]
| Range _ | Float _ -> raise (Unsupported "range types")
| NoDef ->
begin match query_syntax info.syntax id with
| Some _ -> []
| None ->
raise (Unsupported "type declaration without syntax or alias")
end
end
| _ -> [] (*TODO exn ? *)
let munit info = function
| Udecl pd -> pdecl info pd
| Uuse _m -> (*[C.Dinclude m.mod_theory.Theory.th_name]*) []
| 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; []
end
*)
(*TODO simplifications : propagate constants, collapse blocks with only a statement and no def*)
module MLToC = struct
......@@ -963,7 +583,7 @@ module MLToC = struct
let e = C.Evar (pv_name pv) in
([], return_or_expr env e)
| Econst ic ->
let n = Number.compute_int ic in
let n = Number.compute_int_constant ic in
let e = C.(Econst (Cint (BigInt.to_string n))) in
([], return_or_expr env e)
| Eapp (rs, el) ->
......@@ -1073,7 +693,7 @@ module MLToC = struct
begin
match le.e_node with
| Econst ic ->
let n = Number.compute_int ic in
let n = Number.compute_int_constant ic in
let ce = C.(Econst (Cint (BigInt.to_string n))) in
if debug then Format.printf "propagate constant %s for var %s@."
(BigInt.to_string n) (pv_name pv).id_string;
......
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