Generate code from interface (.epi) files

It includes the definition of types, constants
and prototypes defined in the interface.
This commit is contained in:
Cédric Pasteur 2011-09-06 11:54:03 +02:00 committed by Cédric Pasteur
parent ace0cec555
commit 8cc879be7a
18 changed files with 264 additions and 98 deletions

View file

@ -1215,13 +1215,9 @@ let program p =
{ p with p_desc = List.map program_desc p.p_desc }
let interface i =
let interface_decl i =
let desc = match i.interf_desc with
let interface_desc id = match id with
| Iconstdef c -> Iconstdef (typing_const_dec c)
| Itypedef t -> Itypedef (typing_typedec t)
| Isignature i -> Isignature (typing_signature i)
| id -> id
in
{ i with interf_desc = desc }
in
List.map interface_decl i
{ i with i_desc = List.map interface_desc i.i_desc }

View file

@ -183,14 +183,12 @@ type signature = {
sig_param_constraints : constrnt list;
sig_loc : location }
type interface = interface_decl list
and interface_decl = {
interf_desc : interface_desc;
interf_loc : location }
type interface =
{ i_modname : modul;
i_opened : modul list;
i_desc : interface_desc list }
and interface_desc =
| Iopen of modul
| Itypedef of type_dec
| Iconstdef of const_dec
| Isignature of signature

View file

@ -44,6 +44,7 @@ let parse_program modname lexbuf =
let parse_interface modname lexbuf =
(* Parsing of the file *)
let i = do_silent_pass "Parsing" (parse Hept_parser.interface) lexbuf in
let i = { i with Hept_parsetree.i_modname = modname } in
(* Fuse static exps together *)
let i = do_silent_pass "Static Scoping" Hept_static_scoping.interface i in

View file

@ -645,20 +645,13 @@ infx:
;
interface:
| interface_decls EOF { List.rev $1 }
| o=list(opens) i=list(interface_desc) EOF
{ { i_modname = ""; i_opened = o; i_desc = i } }
;
interface_decls:
| /* empty */ { [] }
| interface_decls interface_decl { $2 :: $1 }
;
interface_decl:
| id=_interface_decl { mk_interface_decl id (Loc($startpos,$endpos)) }
_interface_decl:
interface_desc:
| type_dec { Itypedef $1 }
| const_dec { Iconstdef $1 }
| OPEN modul { Iopen $2 }
| VAL n=node_or_fun f=ident pc=node_params LPAREN i=params_signature RPAREN
RETURNS LPAREN o=params_signature RPAREN
{ Isignature({ sig_name = f;

View file

@ -217,14 +217,12 @@ type signature =
sig_param_constraints : exp list;
sig_loc : location }
type interface = interface_decl list
and interface_decl =
{ interf_desc : interface_desc;
interf_loc : location }
type interface =
{ i_modname : dec_name;
i_opened : module_name list;
i_desc : interface_desc list }
and interface_desc =
| Iopen of module_name
| Itypedef of type_dec
| Iconstdef of const_dec
| Isignature of signature
@ -261,9 +259,6 @@ let mk_type_dec name desc loc =
let mk_equation desc loc =
{ eq_desc = desc; eq_loc = loc }
let mk_interface_decl desc loc =
{ interf_desc = desc; interf_loc = loc }
let mk_var_dec ?(linearity=Linearity.Ltop) name ty ck last loc =
{ v_name = name; v_type = ty; v_linearity = linearity;
v_clock =ck; v_last = last; v_loc = loc }

View file

@ -316,18 +316,14 @@ and interface_desc_it funs acc id =
try funs.interface_desc funs acc id
with Fallback -> interface_desc funs acc id
and interface_desc funs acc id = match id with
| Iopen _ -> id, acc
| Itypedef t -> let t, acc = type_dec_it funs acc t in Itypedef t, acc
| Iconstdef c -> let c, acc = const_dec_it funs acc c in Iconstdef c, acc
| Isignature s -> let s, acc = signature_it funs acc s in Isignature s, acc
and interface_it funs acc i = funs.interface funs acc i
and interface funs acc i =
let decl acc id =
let idc, acc = interface_desc_it funs acc id.interf_desc in
{ id with interf_desc = idc }, acc
in
mapfold decl acc i
let desc, acc = mapfold (interface_desc_it funs) acc i.i_desc in
{ i with i_desc = desc }, acc
and signature_it funs acc s = funs.signature funs acc s
and signature funs acc s =

View file

@ -166,7 +166,7 @@ end
let mk_app ?(params=[]) ?(unsafe=false) ?(inlined = false) op =
{ Heptagon.a_op = op;
{ Heptagon.a_op = op;
Heptagon.a_params = params;
Heptagon.a_unsafe = unsafe;
Heptagon.a_inlined = inlined }
@ -429,7 +429,7 @@ let translate_contract env opt_ct =
| Some ct ->
let env' = Rename.append env ct.c_controllables in
let b, env = translate_block env ct.c_block in
Some
Some
{ Heptagon.c_assume = translate_exp env ct.c_assume;
Heptagon.c_enforce = translate_exp env ct.c_enforce;
Heptagon.c_controllables = translate_vd_list env' ct.c_controllables;
@ -560,15 +560,12 @@ let translate_signature s =
let translate_interface_desc = function
| Iopen n -> open_module n; Heptagon.Iopen n
| Itypedef tydec -> Heptagon.Itypedef (translate_typedec tydec)
| Iconstdef const_dec -> Heptagon.Iconstdef (translate_const_dec const_dec)
| Isignature s -> Heptagon.Isignature (translate_signature s)
let translate_interface_decl idecl =
let desc = translate_interface_desc idecl.interf_desc in
{ Heptagon.interf_desc = desc;
Heptagon.interf_loc = idecl.interf_loc }
let translate_interface i = List.map translate_interface_decl i
let translate_interface i =
let desc = List.map translate_interface_desc i.i_desc in
{ Heptagon.i_modname = Names.modul_of_string i.i_modname;
Heptagon.i_opened = i.i_opened;
Heptagon.i_desc = desc; }

View file

@ -67,10 +67,6 @@ let const_dec funs local_const cd =
add_const c_name (Signature.mk_const_def Types.Tinvalid (Initial.mk_static_string "invalid"));
cd, local_const
let interface_desc _ local_const id = match id with
| Iopen n -> open_module n; id, local_const
| _ -> raise Errors.Fallback
let program p =
let funs = { Hept_parsetree_mapfold.defaults
with node_dec = node; exp = exp; static_exp = static_exp; const_dec = const_dec } in
@ -81,6 +77,7 @@ let program p =
let interface i =
let funs = { Hept_parsetree_mapfold.defaults
with node_dec = node; exp = exp; const_dec = const_dec } in
List.iter open_module i.i_opened;
let i, _ = Hept_parsetree_mapfold.interface_it funs Names.NamesSet.empty i in
i

View file

@ -44,8 +44,8 @@ struct
raise Errors.Error
end
let fresh = Idents.gen_fresh "hept2mls"
(function Heptagon.Enode f -> (shortname f)
let fresh = Idents.gen_fresh "hept2mls"
(function Heptagon.Enode f -> (shortname f)
| _ -> "n")
(* add an equation *)
@ -224,3 +224,22 @@ let program
p_format_version = minils_format_version;
p_opened = modules;
p_desc = List.map program_desc desc_list }
let signature s =
{ sig_name = s.Heptagon.sig_name;
sig_inputs = s.Heptagon.sig_inputs;
sig_stateful = s.Heptagon.sig_stateful;
sig_outputs = s.Heptagon.sig_outputs;
sig_params = s.Heptagon.sig_params;
sig_param_constraints = s.Heptagon.sig_param_constraints;
sig_loc = s.Heptagon.sig_loc }
let interface i =
let interface_decl id = match id with
| Heptagon.Itypedef td -> Itypedef (typedec td)
| Heptagon.Iconstdef cd -> Iconstdef (const_dec cd)
| Heptagon.Isignature s -> Isignature (signature s)
in
{ i_modname = i.Heptagon.i_modname;
i_opened = i.Heptagon.i_opened;
i_desc = List.map interface_decl i.Heptagon.i_desc }

View file

@ -32,10 +32,13 @@ let compile_interface modname source_f =
if !print_types then Global_printer.print_interface Format.std_formatter;
(* Process the interface *)
let _ = Hept_compiler.compile_interface p in
(* Output the .epci *)
let p = Hept_compiler.compile_interface p in
(* Output the .epci *)
output_value epci_c (Modules.current_module ());
(* Translate to Obc *)
let p = Hept2mls.interface p in
(* Generate the sequential code *)
Mls2seq.interface p;
close_all_files ()
with
| x -> close_all_files (); raise x

View file

@ -687,7 +687,7 @@ let translate_node
} as n) =
Idents.enter_node f;
let mem_var_tys = Mls_utils.node_memory_vars n in
let c_list, c_locals =
let c_list, c_locals =
match contract with
| None -> [], []
| Some c -> c.Minils.c_controllables, c.Minils.c_local in
@ -749,3 +749,22 @@ let program { Minils.p_modname = p_modname; Minils.p_opened = p_o; Minils.p_desc
p_opened = p_o;
p_desc = p_desc }
let signature s =
{ sig_name = s.Minils.sig_name;
sig_inputs = s.Minils.sig_inputs;
sig_stateful = s.Minils.sig_stateful;
sig_outputs = s.Minils.sig_outputs;
sig_params = s.Minils.sig_params;
sig_param_constraints = s.Minils.sig_param_constraints;
sig_loc = s.Minils.sig_loc }
let interface i =
let interface_decl id = match id with
| Minils.Itypedef td -> Itypedef (translate_ty_def td)
| Minils.Iconstdef cd -> Iconstdef (translate_const_def cd)
| Minils.Isignature s -> Isignature (signature s)
in
{ i_modname = i.Minils.i_modname;
i_opened = i.Minils.i_opened;
i_desc = List.map interface_decl i.Minils.i_desc }

View file

@ -16,12 +16,28 @@ open Misc
(** Definition of a target. A target starts either from
dataflow code (ie Minils) or sequential code (ie Obc),
with or without static parameters *)
type target =
type program_target =
| Obc of (Obc.program -> unit)
| Obc_no_params of (Obc.program -> unit)
| Minils of (Minils.program -> unit)
| Minils_no_params of (Minils.program -> unit)
type interface_target =
| IObc of (Obc.interface -> unit)
| IMinils of (Minils.interface -> unit)
type target =
{ t_name : string;
t_program : program_target;
t_interface : interface_target;
t_load_conf : unit -> unit }
let no_conf () = ()
let mk_target ?(interface=IMinils ignore) ?(load_conf = no_conf) name pt =
{ t_name = name; t_program = pt;
t_interface = interface; t_load_conf = load_conf }
(** Writes a .epo file for program [p]. *)
let write_object_file p =
let filename = (Names.modul_to_string p.Minils.p_modname)^".epo" in
@ -38,14 +54,19 @@ let write_obc_file p =
close_out obc;
comment "Generation of Obc code"
let no_conf () = ()
let targets =
[ mk_target ~interface:(IObc Cmain.interface) "c" (Obc_no_params Cmain.program);
mk_target "java" (Obc Java_main.program);
mk_target "z3z" (Minils_no_params Sigalimain.program);
mk_target "obc" (Obc write_obc_file);
mk_target "obc_np" (Obc_no_params write_obc_file);
mk_target "epo" (Minils write_object_file) ]
let targets = [ "c",(Obc_no_params Cmain.program, no_conf);
"java", (Obc Java_main.program, no_conf);
"z3z", (Minils_no_params Sigalimain.program, no_conf);
"obc", (Obc write_obc_file, no_conf);
"obc_np", (Obc_no_params write_obc_file, no_conf);
"epo", (Minils write_object_file, no_conf) ]
let find_target s =
try
List.find (fun t -> t.t_name = s) targets
with
Not_found -> language_error s; raise Errors.Error
let generate_target p s =
@ -53,9 +74,7 @@ let generate_target p s =
comment "Unfolding";
if !Compiler_options.verbose
then List.iter (Mls_printer.print stderr) p_list in*)
let target =
(try fst (List.assoc s targets)
with Not_found -> language_error s; raise Errors.Error) in
let target = (find_target s).t_program in
match target with
| Minils convert_fun ->
convert_fun p
@ -72,15 +91,16 @@ let generate_target p s =
let o_list = List.map Obc_compiler.compile_program o_list in
List.iter convert_fun o_list
let generate_interface i s =
let target = (find_target s).t_interface in
match target with
| IObc convert_fun ->
let o = Mls2obc.interface i in
convert_fun o
| IMinils convert_fun -> convert_fun i
let load_conf () =
let target_conf s =
try
let conf = snd (List.assoc s targets) in
conf ()
with
Not_found -> language_error s; raise Errors.Error
in
List.iter target_conf !target_languages
List.iter (fun s -> (find_target s).t_load_conf ()) !target_languages
(** Translation into dataflow and sequential languages, defaults to obc. *)
let program p =
@ -89,3 +109,9 @@ let program p =
| l -> l in
let targets = if !create_object_file then "epo"::targets else targets in
List.iter (generate_target p) targets
let interface i =
let targets = match !target_languages with
| [] -> [] (* by default, generate obc file *)
| l -> l in
List.iter (generate_interface i) targets

View file

@ -77,7 +77,7 @@ and edesc =
* extvalue list * extvalue list * var_ident option
(** map f <<n>> <(extvalue)> (extvalue) reset ident *)
and app = { a_op: op;
and app = { a_op: op;
a_params: static_exp list;
a_unsafe: bool;
a_id: ident option;
@ -156,6 +156,26 @@ and program_desc =
| Pconst of const_dec
| Ptype of type_dec
type signature = {
sig_name : qualname;
sig_inputs : arg list;
sig_stateful : bool;
sig_outputs : arg list;
sig_params : param list;
sig_param_constraints : constrnt list;
sig_loc : location }
type interface =
{ i_modname : modul;
i_opened : modul list;
i_desc : interface_desc list }
and interface_desc =
| Itypedef of type_dec
| Iconstdef of const_dec
| Isignature of signature
(*Helper functions to build the AST*)
let mk_extvalue ~ty ?(linearity = Ltop) ?(clock = fresh_clock()) ?(loc = no_location) desc =

View file

@ -107,7 +107,7 @@ let copname = function
| "=" -> "==" | "<>" -> "!=" | "&" -> "&&" | "or" -> "||" | "+" -> "+"
| "-" -> "-" | "*" -> "*" | "/" -> "/" | "*." -> "*" | "/." -> "/"
| "+." -> "+" | "-." -> "-" | "<" -> "<" | ">" -> ">" | "<=" -> "<="
| ">=" -> ">="
| ">=" -> ">=" | "<=." -> "<=" | "<." -> "<" | ">=." -> ">=" | ">." -> ">"
| "~-" -> "-" | "not" -> "!" | "%" -> "%"
| op -> op
@ -225,10 +225,11 @@ let rec cexpr_of_static_exp se =
(List.fold_left (fun cc n -> Carraylit (repeat_list cc (int_of_static_exp n)))
(cexpr_of_static_exp c) n_list)
| Svar ln ->
(try
(* (try
let cd = find_const ln in
cexpr_of_static_exp (Static.simplify QualEnv.empty cd.c_value)
with Not_found -> assert false)
with Not_found -> assert false) *)
Cvar (cname_of_qn ln)
| Sop _ ->
let se' = Static.simplify QualEnv.empty se in
if se = se' then
@ -258,14 +259,14 @@ and cexprs_of_exps out_env var_env exps =
and cop_of_op_aux op_name cexps = match op_name with
| { qual = Pervasives; name = op } ->
begin match op,cexps with
| "~-", [e] -> Cuop ("-", e)
| ("~-" | "~-."), [e] -> Cuop ("-", e)
| "not", [e] -> Cuop ("!", e)
| (
"=" | "<>"
| "&" | "or"
| "+" | "-" | "*" | "/"
| "*." | "/." | "+." | "-." | "%"
| "<" | ">" | "<=" | ">="), [el;er] ->
| "<" | ">" | "<=" | ">=" | "<=." | "<." | ">=." | ">."), [el;er] ->
Cbop (copname op, el, er)
| _ -> Cfun_call(op, cexps)
end
@ -775,20 +776,21 @@ let cdefs_and_cdecls_of_type_decl otd =
let decl = Cdecl_struct (name, decls) in
([], [decl])
(** [cfile_list_of_oprog oprog] translates the Obc program [oprog] to a list of
C source and header files. *)
let cfile_list_of_oprog_ty_decls name oprog =
let types = Obc_utils.program_types oprog in
let cdefs_and_cdecls = List.map cdefs_and_cdecls_of_type_decl types in
let cdefs_and_cdecls_of_const_decl cd =
let name = cname_of_qn cd.c_name in
let v = cexpr_of_static_exp cd.Obc.c_value in
let cty = ctype_of_otype cd.Obc.c_type in
[], [Cdecl_constant (name, cty, v)]
let (cty_defs, cty_decls) = List.split cdefs_and_cdecls in
let filename_types = name ^ "_types" in
let types_h = (filename_types ^ ".h",
Cheader (["stdbool"; "assert"; "pervasives"],
List.concat cty_decls)) in
let types_c = (filename_types ^ ".c", Csource (concat cty_defs)) in
let cdefs_and_cdecls_of_interface_decl id = match id with
| Itypedef td -> cdefs_and_cdecls_of_type_decl td
| Iconstdef cd -> cdefs_and_cdecls_of_const_decl cd
| _ -> [], []
filename_types, [types_h; types_c]
let cdefs_and_cdecls_of_program_decl id = match id with
| Ptype td -> cdefs_and_cdecls_of_type_decl td
| Pconst cd -> cdefs_and_cdecls_of_const_decl cd
| _ -> [], []
let global_file_header name prog =
let dependencies = ModulSet.elements (Obc_utils.Deps.deps_program prog) in
@ -800,10 +802,33 @@ let global_file_header name prog =
let decls = List.concat decls
and defs = List.concat defs in
let (ty_fname, ty_files) = cfile_list_of_oprog_ty_decls name prog in
let filename_types = name ^ "_types" in
let cdefs_and_cdecls = List.map cdefs_and_cdecls_of_program_decl prog.p_desc in
let (cty_defs, cty_decls) = List.split cdefs_and_cdecls in
let types_h = (filename_types ^ ".h",
Cheader ("stdbool"::"assert"::"pervasives"::dependencies,
List.concat cty_decls)) in
let types_c = (filename_types ^ ".c", Csource (concat cty_defs)) in
let header =
(name ^ ".h", Cheader (ty_fname :: dependencies, decls))
(name ^ ".h", Cheader (filename_types :: dependencies, decls))
and source =
(name ^ ".c", Csource defs) in
[header; source] @ ty_files
[header; source; types_h; types_c]
let interface_header name i =
let dependencies = ModulSet.elements (Obc_utils.Deps.deps_interface i) in
let dependencies =
List.map (fun m -> String.uncapitalize (modul_to_string m)) dependencies in
let cdefs_and_cdecls = List.map cdefs_and_cdecls_of_interface_decl i.i_desc in
let (cty_defs, cty_decls) = List.split cdefs_and_cdecls in
let types_h = (name ^ ".h",
Cheader ("stdbool"::"assert"::"pervasives"::dependencies,
List.concat cty_decls)) in
let types_c = (name ^ ".c", Csource (concat cty_defs)) in
[types_h; types_c]

View file

@ -344,3 +344,11 @@ let program p =
let dir = clean_dir dirname in
let c_ast = translate filename p in
C.output dir c_ast
let interface i =
let filename =
filename_of_name (cname_of_name (modul_to_string i.i_modname)) in
let dirname = build_path (filename ^ "_c") in
let dir = clean_dir dirname in
let c_ast = interface_header (Filename.basename filename) i in
C.output dir c_ast

View file

@ -130,3 +130,22 @@ and program_desc =
| Pconst of const_dec
| Ptype of type_dec
type signature = {
sig_name : qualname;
sig_inputs : arg list;
sig_stateful : bool;
sig_outputs : arg list;
sig_params : param list;
sig_param_constraints : constrnt list;
sig_loc : location }
type interface =
{ i_modname : modul;
i_opened : modul list;
i_desc : interface_desc list }
and interface_desc =
| Itypedef of type_dec
| Iconstdef of const_dec
| Isignature of signature

View file

@ -32,6 +32,9 @@ type 'a obc_it_funs = {
tdesc: 'a obc_it_funs -> 'a -> Obc.tdesc -> Obc.tdesc * 'a;
program: 'a obc_it_funs -> 'a -> Obc.program -> Obc.program * 'a;
program_desc: 'a obc_it_funs -> 'a -> Obc.program_desc -> Obc.program_desc * 'a;
interface: 'a obc_it_funs -> 'a -> Obc.interface -> Obc.interface * 'a;
interface_desc: 'a obc_it_funs -> 'a -> Obc.interface_desc -> Obc.interface_desc * 'a;
signature: 'a obc_it_funs -> 'a -> Obc.signature -> Obc.signature * 'a;
global_funs: 'a Global_mapfold.global_it_funs }
@ -202,6 +205,9 @@ and tdesc funs acc td = match td with
| Type_struct s ->
let s, acc = structure_it funs.global_funs acc s in
Type_struct s, acc
| Type_alias ty ->
let ty, acc = ty_it funs.global_funs acc ty in
Type_alias ty, acc
| _ -> td, acc
@ -218,6 +224,30 @@ and program_desc funs acc pd = match pd with
| Ptype td -> let td, acc = type_dec_it funs acc td in Ptype td, acc
| Pclass n -> let n, acc = class_def_it funs acc n in Pclass n, acc
and interface_it funs acc p = funs.interface funs acc p
and interface funs acc p =
let i_desc, acc = mapfold (interface_desc_it funs) acc p.i_desc in
{ p with i_desc = i_desc }, acc
and interface_desc_it funs acc pd =
try funs.interface_desc funs acc pd
with Fallback -> interface_desc funs acc pd
and interface_desc funs acc pd = match pd with
| Itypedef td -> let td, acc = type_dec_it funs acc td in Itypedef td, acc
| Iconstdef cd -> let cd, acc = const_dec_it funs acc cd in Iconstdef cd, acc
| Isignature s -> let s, acc = signature_it funs acc s in Isignature s, acc
and signature_it funs acc s = funs.signature funs acc s
and signature funs acc s =
let sig_params, acc = mapfold (param_it funs.global_funs) acc s.sig_params in
let sig_inputs, acc = mapfold (arg_it funs.global_funs) acc s.sig_inputs in
let sig_outputs, acc = mapfold (arg_it funs.global_funs) acc s.sig_outputs in
{ s with sig_params = sig_params; sig_inputs = sig_inputs; sig_outputs }, acc
let defaults = {
lhs = lhs;
lhsdesc = lhsdesc;
@ -238,4 +268,7 @@ let defaults = {
tdesc = tdesc;
program = program;
program_desc = program_desc;
interface = interface;
interface_desc = interface_desc;
signature = signature;
global_funs = Global_mapfold.defaults }

View file

@ -151,6 +151,10 @@ struct
| Module _ | QualModule _ -> ModulSet.add qn.qual deps
| _ -> deps
let deps_ty funs deps ty = match ty with
| Tid ln -> ty, deps_longname deps ln
| _ -> raise Errors.Fallback
let deps_static_exp_desc funs deps sedesc =
let (sedesc, deps) = Global_mapfold.static_exp_desc funs deps sedesc in
match sedesc with
@ -192,7 +196,8 @@ struct
let deps_program p =
let funs = { Obc_mapfold.defaults with
global_funs = { Global_mapfold.defaults with
static_exp_desc = deps_static_exp_desc; };
static_exp_desc = deps_static_exp_desc;
ty = deps_ty };
lhsdesc = deps_lhsdesc;
edesc = deps_edesc;
act = deps_act;
@ -200,6 +205,15 @@ struct
} in
let (_, deps) = Obc_mapfold.program funs ModulSet.empty p in
ModulSet.remove p.p_modname deps
let deps_interface i =
let funs = { Obc_mapfold.defaults with
global_funs = { Global_mapfold.defaults with
static_exp_desc = deps_static_exp_desc;
ty = deps_ty };
} in
let (_, deps) = Obc_mapfold.interface funs ModulSet.empty i in
ModulSet.remove i.i_modname deps
end
(** Creates a new for loop. Expects the size of the iteration
@ -238,6 +252,13 @@ let program_classes p =
in
List.fold_right add_class p.p_desc []
let interface_types i =
let add_type id acc = match id with
| Itypedef ty -> ty :: acc
| _ -> acc
in
List.fold_right add_type i.i_desc []
let rec ext_value_of_pattern patt =
let desc = match patt.pat_desc with
| Lvar id -> Wvar id