jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity

Fix handling of nodes without actual controllers by ctrl2ept

Browse source 
These changes allow to handle the case where contracts are only used
for verification purposes, in which case the functions generated by
ReaX have no outputs and are not functions stricto sensu.  Indeed, in
this case the new controller module still needs to be declared and
compiled as we may have re-qualified types during the generation of
the Controllable-Nbac code: we moved all types declared in the
original module into the controller module to break cyclic module
dependencies that would otherwise be introduced if the controller is
expressed using data of such types.
This commit is contained in:
Nicolas Berthier 2015-09-18 09:51:41 +02:00
parent bb324eee17
commit 74b94c9718
2 changed files with 62 additions and 72 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

86
compiler/heptagon/ctrln/ctrlNbacAsEpt.ml
View file

@ -47,19 +47,21 @@ type 'f gen_data =
decls: ('f, 'f var_spec) decls;
ltyps: (typ * 'f option) SMap.t;
qname: string -> qualname;
mutable tdefs: type_name SMap.t;
typ_symbs: type_name SMap.t;
mutable env: var_dec Env.t;
mutable var_names: ident SMap.t;
}
let no_typ_symbs: type_name SMap.t = SMap.empty
(* --- *)
let mk_gen_data qual decls typdefs =
let mk_gen_data qualname typ_symbs decls typdefs =
{
decls;
ltyps = label_typs typdefs;
qname = (fun name -> { qual; name });
tdefs = SMap.empty;
qname = (fun name -> { qual = modul qualname; name });
typ_symbs;
env = Env.empty;
var_names = SMap.empty;
}
@ -72,7 +74,7 @@ let translate_typ gd vdecl = function
| `Bool -> Initial.tbool
| `Int -> Initial.tint
| `Real -> Initial.tfloat
| `Enum tn -> Tid (SMap.find tn gd.tdefs)
| `Enum tn -> Tid (SMap.find tn gd.typ_symbs)
| t -> raise (Untranslatable (asprintf "type %a" print_typ t,
opt_decl_loc gd vdecl))
@ -81,8 +83,6 @@ let symb_typ gd s = try match SMap.find s gd.decls with | typ, _, _ -> typ with
let symb_typ' gd s = translate_typ gd s (symb_typ gd s)
let translate_label gd l = gd.qname (Symb.to_string (label_symb l))
let ts gd v = try SMap.find v gd.var_names with Not_found ->
failwith (asprintf "Variable name `%a' unavailable; \
was it an output of the main node?" Symb.print v)
@ -241,56 +241,59 @@ let translate_expr gd e =
(* --- *)
(* let decl_typs typdefs gd = *)
(* fold_typdefs begin fun tname tdef typs -> *)
(* let name = gd.qname (Symb.to_string tname |> String.uncapitalize) in *)
(* match tdef with *)
(* | EnumDef labels -> *)
(* let constrs = List.map (fun (l, _) -> translate_label gd l) labels in *)
(* gd.tdefs <- SMap.add tname name gd.tdefs; *)
(* Ptype { t_name = name; *)
(* t_desc = Type_enum constrs; *)
(* t_loc = Location.no_location } :: typs *)
(* end typdefs [] *)
let decl_typs modul_name typdefs =
let qualify name = { qual = modul modul_name; name } in
fold_typdefs begin fun tname tdef (types, typ_symbs) ->
let name = qualify (Symb.to_string tname |> String.uncapitalize) in
match tdef with
| EnumDef labels, _ ->
let constrs = List.map (fun (l, _) ->
qualify (Symb.to_string (label_symb l))) labels in
(Ptype { t_name = name;
t_desc = Type_enum constrs;
t_loc = Location.no_location } :: types,
SMap.add tname name typ_symbs)
end typdefs ([], no_typ_symbs)
let decl_typs_from_module_itf gd =
let decl_typs_from_module_itf modul_name =
(* Note we need to sort type declarations according to their respective
dependencies; hence the implicit topological traversal of the type
definitions. *)
let rec decl_types rem types =
let rec decl_types rem acc =
if QualEnv.is_empty rem then
types
acc
else
let t_name, tdef = QualEnv.choose rem in
let rem, types = decl_typ t_name tdef rem types in
decl_types rem types
and decl_typ t_name tdef rem types =
let rem, acc = decl_typ t_name tdef rem acc in
decl_types rem acc
and decl_typ t_name tdef rem ((types, typ_symbs) as acc) =
let rem = QualEnv.remove t_name rem in
if tdef = Tabstract || t_name.qual = Names.Pervasives then
rem, types
if t_name.qual <> modul_name then
rem, acc
else
let t_desc, rem, types = match tdef with
let t_desc, rem, (types, typ_symbs) = match tdef with
| Tenum cl ->
(* Compiler_utils.info "declaring enum type %s" (shortname t_name); *)
let name = Symb.of_string (String.capitalize (shortname t_name)) in
gd.tdefs <- SMap.add name t_name gd.tdefs;
(Type_enum cl, rem, types)
(Type_enum cl, rem, (types, SMap.add name t_name typ_symbs))
| Talias (Tid tn) when tn.qual = t_name.qual -> (* declare deps 1st *)
(* Compiler_utils.info "declaring alias type %s" (shortname t_name); *)
let tdef = QualEnv.find tn rem in
let rem, types = decl_typ tn tdef (QualEnv.remove tn rem) types in
(Type_alias (Tid tn), rem, types)
let rem, acc = decl_typ tn tdef (QualEnv.remove tn rem) acc in
(Type_alias (Tid tn), rem, acc)
| Talias t ->
(* Compiler_utils.info "declaring alias type %s" (shortname t_name); *)
(Type_alias t, rem, types)
(Type_alias t, rem, acc)
| Tstruct _ ->
failwith (asprintf "Unexpected struct type `%s' in module interface"
(shortname t_name))
| Tabstract -> assert false
in
rem, Ptype { t_name; t_desc; t_loc = Location.no_location; } :: types
rem, (Ptype { t_name; t_desc; t_loc = Location.no_location } :: types,
typ_symbs)
in
decl_types Modules.g_env.Modules.types []
Modules.open_module modul_name;
decl_types Modules.g_env.Modules.types ([], no_typ_symbs)
(* --- *)
@ -391,19 +394,20 @@ let node_of_func gd ?node_sig n_name func =
(* --- *)
let gen_func ?node_sig ~node_name func =
let gen_func ?typ_symbs ?node_sig ~node_name func =
let { fn_typs; fn_decls } = func_desc func in
let modul = modul node_name in
let gd = mk_gen_data modul (fn_decls:> ('f, 'f var_spec) decls) fn_typs in
(* let typs = decl_typs fn_typs gd in *)
let typs = decl_typs_from_module_itf gd in
let fn_decls = (fn_decls :> ('f, 'f var_spec) decls) in
let typs, typ_symbs = match typ_symbs with
| None -> decl_typs node_name fn_typs
| Some typ_symbs -> [], typ_symbs
in
let gd = mk_gen_data node_name typ_symbs fn_decls fn_typs in
let node = node_of_func gd ?node_sig node_name func in
node, typs
node :: typs
(* --- *)
let create_prog ?(open_modul = []) modul =
Modules.open_module modul;
{
p_modname = modul;
p_opened = open_modul;

48
compiler/main/ctrl2ept.ml
View file

@ -118,33 +118,18 @@ let parse_input ?filename (parse: ?filename:string -> _) =
exception Error of string
(* let hack_filter_inputs = let open AST in function *)
(* | `Desc ({ fn_decls = decls } as f) -> *)
(* (\* TODO: we should actually _substitute_ these variables with ff in the *)
(* definitions; yet I think they are unlikely to appear anywhere in the *)
(* controller. *\) *)
(* let init_symb = Symb.of_string Ctrln_utils.init_cond_str *)
(* and sink_symb = Symb.of_string Ctrln_utils.sink_state_str in *)
(* let decls = SMap.remove init_symb decls in *)
(* let decls = SMap.remove sink_symb decls in *)
(* `Desc { f with fn_decls = decls } *)
(* | _ -> failwith "should be given an unchecked function!" *)
let parse_n_gen_ept_node ?filename ?node_name ?node_sig () =
let parse_n_gen_ept_node ?filename ?node_name ?node_sig ?typ_symbs () =
let name, func = parse_input ?filename CtrlNbac.Parser.Unsafe.parse_func in
let node_name = match node_name with Some n -> n
| None -> match name with None -> assert false
| Some n -> Names.local_qn (n ^ "_ctrlr")
in
(* let name = match name with None -> "ctrlr" | Some n -> n ^"_ctrlr" in *)
(* let func = hack_filter_inputs func in *)
name, CtrlNbacAsEpt.gen_func ~node_name ?node_sig func
name, CtrlNbacAsEpt.gen_func ?typ_symbs ~node_name ?node_sig func
let handle_ctrlf ?filename mk_oc =
let _, (node, typs) = parse_n_gen_ept_node ?filename () in
let _, decls = parse_n_gen_ept_node ?filename () in
let prog = CtrlNbacAsEpt.create_prog Names.LocalModule in (* don't care? *)
let prog = List.fold_right CtrlNbacAsEpt.add_to_prog typs prog in
let prog = CtrlNbacAsEpt.add_to_prog node prog in
let prog = List.fold_right CtrlNbacAsEpt.add_to_prog decls prog in
let oc, close = mk_oc.out_exec "ept" in
Hept_printer.print oc prog;
close ()
@ -162,27 +147,24 @@ let output_prog prog modul =
Hept_printer.print oc prog;
close_out oc
let input_function prog filename node_name node_sig =
let input_function prog typ_symbs filename node_name node_sig =
info "Reading function from `%s'…" filename;
let res = parse_n_gen_ept_node ~filename ~node_name ~node_sig () in
let node, typs = snd res in
(* XXX: check types are also in signature? maybe we should only use the types
let _, decls = parse_n_gen_ept_node ~filename ~node_name ~node_sig ~typ_symbs () in
(* XXX: check types are also in signature? actually, we only use the types
declared in the signature instead, as long as the controller synthesis tool
does not introduce new types. *)
let prog = List.fold_right CtrlNbacAsEpt.add_to_prog typs prog in
let prog = CtrlNbacAsEpt.add_to_prog node prog in
prog
List.fold_right CtrlNbacAsEpt.add_to_prog decls prog
let try_ctrlf nn prog =
let try_ctrlf typ_symbs nn prog =
let node_name = Ctrln_utils.controller_node nn in
if Modules.check_value node_name then
let filename = Ctrln_utils.ctrlf_for_node nn in
let node_sig = Modules.find_value node_name in
input_function prog filename node_name node_sig
input_function prog typ_symbs filename node_name node_sig
else
raise (Error "Unable to load any controller function.")
let try_ctrls nn prog =
let try_ctrls typ_symbs nn prog =
let rec try_ctrls num prog =
let node_name = Ctrln_utils.controller_node ~num nn in
if Modules.check_value node_name then
@ -190,7 +172,7 @@ let try_ctrls nn prog =
if num = 0 && not (Sys.file_exists filename) then
raise Exit; (* abort *)
let node_sig = Modules.find_value node_name in
let prog = input_function prog filename node_name node_sig in
let prog = input_function prog typ_symbs filename node_name node_sig in
try_ctrls (succ num) prog
else
prog
@ -207,8 +189,12 @@ let handle_node arg =
Modules.open_module Names.Pervasives;
info "Loading module of controllers for node %s…" (Names.fullname nn);
let om = Ctrln_utils.controller_modul mo in
info "Translating type declarations of module %s…" (Names.modul_to_string om);
let typs, typ_symbs = CtrlNbacAsEpt.decl_typs_from_module_itf om in
let prog = CtrlNbacAsEpt.create_prog ~open_modul:[ ] om in
let prog = try try_ctrls nn prog with Exit -> try_ctrlf nn prog in
let prog = List.fold_right CtrlNbacAsEpt.add_to_prog typs prog in
let prog = try try_ctrls typ_symbs nn prog with
| Exit -> try_ctrlf typ_symbs nn prog in
output_prog prog om
(* -------------------------------------------------------------------------- *)