From 59020713a7a653418d2006f419e54cdb9b18687d Mon Sep 17 00:00:00 2001
From: ploc <ploc@garoche.net>
Date: Thu, 22 Nov 2018 18:32:51 -0800
Subject: [PATCH] Some progress on EMF bqckend. Refactoring machines code
---
src/backends/EMF/EMF_backend.ml | 80 ++++++++-
src/backends/EMF/EMF_common.ml | 302 +++++++++++++++++++++++---------
src/compiler_stages.ml | 3 +-
src/corelang.ml | 9 -
src/corelang.mli | 1 +
src/lustre_types.ml | 2 +-
src/machine_code.ml | 205 ++++++++++++++--------
src/machine_code_common.ml | 6 +-
src/machine_code_common.mli | 2 +-
src/machine_code_types.ml | 1 +
src/normalization.ml | 219 ++++++++++++++++-------
src/typing.ml | 13 +-
12 files changed, 608 insertions(+), 235 deletions(-)
diff --git a/src/backends/EMF/EMF_backend.ml b/src/backends/EMF/EMF_backend.ml
index 9f2c2f4a..4a4913be 100644
--- a/src/backends/EMF/EMF_backend.ml
+++ b/src/backends/EMF/EMF_backend.ml
@@ -375,14 +375,60 @@ let pp_emf_annot cpt fmt (key, ee) =
pp_emf_eexpr ee
in
incr cpt
+
+let pp_emf_spec_mode fmt m =
+ fprintf fmt "{@[";
+ fprintf fmt "\"mode_id\": \"%s\",@ "
+ m.mode_id;
+ fprintf fmt "\"require\": [%a],@ "
+ pp_emf_eexprs m.ensure;
+ fprintf fmt "\"require\": [%a],@ "
+ pp_emf_eexprs m.require;
+ fprintf fmt "@]}"
+
+let pp_emf_spec_modes = pp_emf_list pp_emf_spec_mode
+
+let pp_emf_spec_import fmt i =
+ fprintf fmt "{@[";
+ fprintf fmt "\"contract\": \"%s\",@ "
+ i.import_nodeid;
+ fprintf fmt "\"inputs\": [%a],@ "
+ pp_emf_exprs i.inputs;
+ fprintf fmt "\"outputs\": [%a],@ "
+ pp_emf_exprs i.outputs;
+ fprintf fmt "@]}"
+
+let pp_emf_spec_imports = pp_emf_list pp_emf_spec_import
+
+let pp_emf_spec fmt spec =
+ fprintf fmt "{ @[<hov 0>";
+ fprintf fmt "\"consts\": [%a],@ "
+ pp_emf_consts spec.consts;
+ fprintf fmt "\"locals\": [%a],@ "
+ pp_emf_vars_decl spec.locals;
+ fprintf fmt "\"stmts\": [%a],@ "
+ pp_emf_stmts spec.stmts;
+ fprintf fmt "\"assume\": [%a],@ "
+ pp_emf_eexprs spec.assume;
+ fprintf fmt "\"guarantees\": [%a],@ "
+ pp_emf_eexprs spec.guarantees;
+ fprintf fmt "\"modes\": [%a],@ "
+ pp_emf_spec_modes spec.modes;
+ fprintf fmt "\"imports\": [%a]@ "
+ pp_emf_spec_imports spec.imports;
+ fprintf fmt "@] }"
let pp_emf_annots cpt fmt annots = fprintf_list ~sep:",@ " (pp_emf_annot cpt) fmt annots.annots
let pp_emf_annots_list cpt fmt annots_list = fprintf_list ~sep:",@ " (pp_emf_annots cpt) fmt annots_list
+
+
+
let pp_machine fmt m =
let instrs = (*merge_branches*) m.mstep.step_instrs in
try
fprintf fmt "@[<v 2>\"%a\": {@ "
- print_protect (fun fmt -> pp_print_string fmt m.mname.node_id);
+ print_protect (fun fmt -> pp_print_string fmt m.mname.node_id);
+ fprintf fmt "\"imported\": \"false\",@ ";
fprintf fmt "\"kind\": %t,@ "
(fun fmt -> if not ( snd (get_stateless_status m) )
then fprintf fmt "\"stateful\""
@@ -399,6 +445,7 @@ let pp_machine fmt m =
fprintf fmt "\"original_name\": \"%s\",@ " m.mname.node_id;
fprintf fmt "\"instrs\": {@[<v 0> %a@]@ },@ "
(pp_emf_instrs m) instrs;
+ (match m.mspec with None -> () | Some spec -> fprintf fmt "\"spec\": %a,@ " pp_emf_spec spec);
fprintf fmt "\"annots\": {@[<v 0> %a@]@ }" (pp_emf_annots_list (ref 0)) m.mannot;
fprintf fmt "@]@ }"
with Unhandled msg -> (
@@ -408,6 +455,25 @@ let pp_machine fmt m =
eprintf "node skipped - no output generated@ @]@."
)
+let pp_emf_imported_node fmt top =
+ let ind = Corelang.imported_node_of_top top in
+ try
+ fprintf fmt "@[<v 2>\"%a\": {@ "
+ print_protect (fun fmt -> pp_print_string fmt ind.nodei_id);
+ fprintf fmt "\"imported\": \"true\",@ ";
+ fprintf fmt "\"inputs\": [%a],@ "
+ pp_emf_vars_decl ind.nodei_inputs;
+ fprintf fmt "\"outputs\": [%a],@ "
+ pp_emf_vars_decl ind.nodei_outputs;
+ fprintf fmt "\"original_name\": \"%s\",@ " ind.nodei_id;
+ (match ind.nodei_spec with None -> () | Some spec -> fprintf fmt "\"spec\": %a" pp_emf_spec spec);
+ fprintf fmt "@]@ }"
+ with Unhandled msg -> (
+ eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ "
+ ind.nodei_id;
+ eprintf "%s@ " msg;
+ eprintf "node skipped - no output generated@ @]@."
+ )
(****************************************************)
(* Main function: iterates over node and print them *)
(****************************************************)
@@ -425,13 +491,21 @@ let pp_meta fmt basename =
fprintf fmt "@ @]},@ "
let translate fmt basename prog machines =
- (* record_types prog; *)
+ (* record_types prog; *)
fprintf fmt "@[<v 0>{@ ";
pp_meta fmt basename;
+ (* Typedef *)
+ fprintf fmt "\"typedef\": [@[<v 0>%a@]],@ "
+ (pp_emf_list pp_emf_typedef) (Corelang.get_typedefs prog);
+ fprintf fmt "\"consts\": [@[<v 0>%a@]],@ "
+ (pp_emf_list pp_emf_top_const) (Corelang.get_consts prog);
+ fprintf fmt "\"imported_nodes\": @[<v 0>{@ ";
+ pp_emf_list pp_emf_imported_node fmt (Corelang.get_imported_nodes prog);
+ fprintf fmt "}@],@ ";
fprintf fmt "\"nodes\": @[<v 0>{@ ";
(* Previous alternative: mapping normalized lustre to EMF:
fprintf_list ~sep:",@ " pp_decl fmt prog; *)
- fprintf_list ~sep:",@ " pp_machine fmt (List.rev machines);
+ pp_emf_list pp_machine fmt (List.rev machines);
fprintf fmt "}@]@ }";
fprintf fmt "@]@ }"
diff --git a/src/backends/EMF/EMF_common.ml b/src/backends/EMF/EMF_common.ml
index dc95fa74..1f122f5f 100644
--- a/src/backends/EMF/EMF_common.ml
+++ b/src/backends/EMF/EMF_common.ml
@@ -76,105 +76,153 @@ let pp_var_name fmt v = print_protect fmt (fun fmt -> Printers.pp_var_name fmt v
*)
-let pp_tag_type fmt typ =
- let rec aux tydec_desc =
- match tydec_desc with
- | Tydec_int -> fprintf fmt "int"
- | Tydec_real -> fprintf fmt "real"
- | Tydec_bool -> fprintf fmt "bool"
- | Tydec_clock ty -> aux ty
- | Tydec_enum const_list -> (
- let size = List.length const_list in
- if size < 255 then
- fprintf fmt "uint8"
- else if size < 65535 then
- fprintf fmt "uint16"
- else
- assert false (* Too much states. This not reasonable *)
- )
- | Tydec_const _ | Tydec_struct _ | Tydec_array _ | Tydec_any -> eprintf "unhandled cst tag in EMF: %a@." Printers.pp_var_type_dec_desc tydec_desc; assert false
- in
- aux typ.tydef_desc
-
-let pp_cst_type fmt c (*infered_typ*) =
- match c with
- | Const_tag t ->
- let typ = (Corelang.typedef_of_top (Hashtbl.find Corelang.tag_table t)) in
- if typ.tydef_id = "bool" then
- fprintf fmt "bool"
- else
- pp_tag_type fmt typ
- | Const_int _ -> fprintf fmt "int" (*!Options.int_type*)
- | Const_real _ -> fprintf fmt "real" (*!Options.real_type*)
- | Const_string _ -> fprintf fmt "string"
- | _ -> eprintf "cst: %a@." Printers.pp_const c; assert false
+let rec pp_emf_dim fmt dim_expr =
+ fprintf fmt "{";
+ (let open Dimension in
+ match dim_expr.dim_desc with
+ | Dbool b -> fprintf fmt "\"kind\": \"bool\",@ \"value\": \"%b\"" b
+ | Dint i -> fprintf fmt "\"kind\": \"int\",@ \"value\": \"%i\"" i
+ | Dident s -> fprintf fmt "\"kind\": \"ident\",@ \"value\": \"%s\"" s
+ | Dappl(f, args) -> fprintf fmt "\"kind\": \"fun\",@ \"id\": \"%s\",@ \"args\": [@[%a@]]"
+ f (Utils.fprintf_list ~sep:",@ " pp_emf_dim) args
+ | Dite(i,t,e) -> fprintf fmt "\"kind\": \"ite\",@ \"guard\": \"%a\",@ \"then\": %a,@ \"else\": %a"
+ pp_emf_dim i pp_emf_dim t pp_emf_dim e
+ | Dlink e -> pp_emf_dim fmt e
+ | Dvar
+ | Dunivar -> assert false (* unresolved *)
+ );
+ fprintf fmt "}"
-let rec pp_infered_type fmt t =
- let open Types in
- if is_bool_type t then fprintf fmt "bool" else
- if is_int_type t then fprintf fmt "int" else (* !Options.int_type *)
- if is_real_type t then fprintf fmt "real" else (* !Options.real_type *)
- match t.tdesc with
- | Tclock t ->
- pp_infered_type fmt t
- | Tstatic (_, t) ->
- fprintf fmt "%a" pp_infered_type t
- | Tconst id ->
- (* This is a type id for a enumerated type, eg. introduced by automata *)
- let typ =
- (Corelang.typedef_of_top (Hashtbl.find Corelang.type_table (Tydec_const id)))
- in
- pp_tag_type fmt typ
- | Tlink ty ->
- pp_infered_type fmt ty
- | _ -> eprintf "unhandled type: %a@." Types.print_node_ty t; assert false
+
+
+(* First try to print the declared one *)
let rec pp_concrete_type dec_t infered_t fmt =
match dec_t with
- | Tydec_int -> fprintf fmt "int" (* !Options.int_type *)
- | Tydec_real -> fprintf fmt "real" (* !Options.real_type *)
+ | Tydec_any -> (* Dynamical built variable. No declared type. Shall
+ use the infered one. *)
+ pp_infered_type fmt infered_t
+ | Tydec_int -> fprintf fmt "{ \"kind\": \"int\" }" (* !Options.int_type *)
+ | Tydec_real -> fprintf fmt "{ \"kind\": \"real\" }" (* !Options.real_type *)
(* TODO we could add more concrete types here if they were available in
dec_t *)
- | Tydec_bool -> fprintf fmt "bool"
+ | Tydec_bool -> fprintf fmt "{ \"kind\": \"bool\" }"
| Tydec_clock t -> pp_concrete_type t infered_t fmt
| Tydec_const id -> (
- (* This is a type id for a enumerated type, eg. introduced by automata *)
+ (* This is an alias type *)
+
+ (* id for a enumerated type, eg. introduced by automata *)
let typ = (Corelang.typedef_of_top (Hashtbl.find Corelang.type_table dec_t)) in
- pp_tag_type fmt typ
+ (* Print the type name associated to this enumerated type. This is
+ basically an integer *)
+ pp_tag_type id typ infered_t fmt
+ )
+
+ | Tydec_struct _ | Tydec_enum _ ->
+ assert false (* should not happen. These type are only built when
+ declaring a type in the prefix of the lustre
+ file. They shall not be associated to variables
+ *)
+
+ | Tydec_array (dim, e) -> (
+ let inf_base = match infered_t.Typing.tdesc with
+ | Typing.Tarray(_,t) -> t
+ | _ -> (* returing something useless, hoping that the concrete
+ datatype will return something usefull *)
+ Typing.new_var ()
+ in
+ fprintf fmt "{ \"kind\": \"array\", \"base_type\": %t, \"dim\": %a }"
+ (pp_concrete_type e inf_base)
+ pp_emf_dim dim
)
- | Tydec_any -> pp_infered_type fmt infered_t
- | _ -> eprintf
- "unhandled construct in type printing for EMF backend: %a@."
- Printers.pp_var_type_dec_desc dec_t; raise (Failure "var")
+
+(* | _ -> eprintf
+ * "unhandled construct in type printing for EMF backend: %a@."
+ * Printers.pp_var_type_dec_desc dec_t; raise (Failure "var") *)
+and pp_tag_type id typ inf fmt =
+ (* We ought to represent these types as values: enum will become int, we keep the name for structs *)
+ let rec aux tydec_desc =
+ match tydec_desc with
+ | Tydec_int
+ | Tydec_real
+ | Tydec_bool
+ | Tydec_array _ -> pp_concrete_type tydec_desc inf fmt
+ | Tydec_const id ->
+ (* Alias of an alias: unrolling definitions *)
+ let typ = (Corelang.typedef_of_top
+ (Hashtbl.find Corelang.type_table tydec_desc))
+ in
+ pp_tag_type id typ inf fmt
+ | Tydec_clock ty -> aux ty
+ | Tydec_enum const_list -> ( (* enum can be mapped to int *)
+ let size = List.length const_list in
+ fprintf fmt "{ \"name\": \"%s\", \"kind\": \"enum\", \"size\": \"%i\" }" id size
+ )
+ | Tydec_struct _ ->
+ fprintf fmt "{ \"name\": \"%s\", \"kind\": \"struct\" }" id
+ | Tydec_any -> (* shall not happen: a declared type cannot be
+ bound to type any *)
+ assert false
+ in
+ aux typ.tydef_desc
+and pp_infered_type fmt t =
+ (* Shall only be used for variable types that were not properly declared. Ie generated at compile time. *)
+ let open Types in
+ if is_bool_type t then fprintf fmt "bool" else
+ if is_int_type t then fprintf fmt "int" else (* !Options.int_type *)
+ if is_real_type t then fprintf fmt "real" else (* !Options.real_type *)
+ match t.tdesc with
+ | Tclock t ->
+ pp_infered_type fmt t
+ | Tstatic (_, t) ->
+ fprintf fmt "%a" pp_infered_type t
+ | Tconst id ->
+ (* This is a type id for a enumerated type, eg. introduced by automata *)
+ let typ =
+ (Corelang.typedef_of_top
+ (Hashtbl.find Corelang.type_table (Tydec_const id)))
+ in
+ pp_tag_type id typ t fmt
+ | Tlink ty ->
+ pp_infered_type fmt ty
+ | _ -> eprintf "unhandled type: %a@." Types.print_node_ty t; assert false
(*let pp_cst_type fmt v =
match v.value_desc with
| Cst c-> pp_cst_type c v.value_type fmt (* constants do not have declared type (yet) *)
| _ -> assert false
*)
-
+
+(* Provide both the declared type and the infered one. *)
let pp_var_type fmt v =
try
if Machine_types.is_specified v then
Machine_types.pp_var_type fmt v
else
pp_concrete_type v.var_dec_type.ty_dec_desc v.var_type fmt
- with Failure _ -> eprintf "failed var: %a@." Printers.pp_var v; assert false
+ with Failure msg -> eprintf "failed var: %a@.%s@." Printers.pp_var v msg; assert false
(******** Other print functions *)
-
+
+let pp_emf_list ?(eol:('a, formatter, unit) Pervasives.format="") pp fmt l =
+ match l with
+ [] -> ()
+ | _ -> fprintf fmt "@[";
+ Utils.fprintf_list ~sep:",@ " pp fmt l;
+ fprintf fmt "@]%(%)" eol
+
+(* Print the variable declaration *)
let pp_emf_var_decl fmt v =
fprintf fmt "@[{\"name\": \"%a\", \"datatype\":\"%a\", \"original_name\": \"%a\"}@]"
pp_var_name v
pp_var_type v
Printers.pp_var_name v
-
-let pp_emf_vars_decl fmt vl =
- fprintf fmt "@[";
- Utils.fprintf_list ~sep:",@ " pp_emf_var_decl fmt vl;
- fprintf fmt "@]"
+
+let pp_emf_vars_decl = pp_emf_list pp_emf_var_decl
+
+
let reset_name id =
"reset_" ^ id
@@ -187,7 +235,26 @@ let pp_tag_id fmt t =
let const_list = match typ.tydef_desc with Tydec_enum tl -> tl | _ -> assert false in
fprintf fmt "%i" (get_idx t const_list)
-let pp_emf_cst fmt c =
+let pp_cst_type c inf fmt (*infered_typ*) =
+ match c with
+ | Const_tag t ->
+ let typ = (Corelang.typedef_of_top (Hashtbl.find Corelang.tag_table t)) in
+ if typ.tydef_id = "bool" then
+ fprintf fmt "bool"
+ else
+ pp_tag_type t typ inf fmt
+ | Const_int _ -> fprintf fmt "int" (*!Options.int_type*)
+ | Const_real _ -> fprintf fmt "real" (*!Options.real_type*)
+ | Const_string _ -> fprintf fmt "string"
+ | _ -> eprintf "cst: %a@." Printers.pp_const c; assert false
+
+
+let pp_emf_cst c inf fmt =
+ let pp_typ fmt =
+ fprintf fmt "\"datatype\": \"";
+ pp_cst_type c inf fmt;
+ fprintf fmt "\"@ "
+ in
match c with
| Const_tag t->
let typ = (Corelang.typedef_of_top (Hashtbl.find Corelang.tag_table t)) in
@@ -195,7 +262,7 @@ let pp_emf_cst fmt c =
fprintf fmt "{@[\"type\": \"constant\",@ ";
fprintf fmt"\"value\": \"%a\",@ "
Printers.pp_const c;
- fprintf fmt "\"datatype\": \"%a\"@ " pp_cst_type c;
+ pp_typ fmt;
fprintf fmt "@]}"
)
else (
@@ -203,25 +270,25 @@ let pp_emf_cst fmt c =
pp_tag_id t;
fprintf fmt "\"origin_type\": \"%s\",@ \"origin_value\": \"%s\",@ "
typ.tydef_id t;
- fprintf fmt "\"datatype\": \"%a\"@ " pp_cst_type c;
+ pp_typ fmt;
fprintf fmt "@]}"
)
| Const_string s ->
- fprintf fmt "{@[\"type\": \"constant\",@ \"value\": \"%s\",@ " s;
- fprintf fmt "\"datatype\": \"%a\"@ " pp_cst_type c;
- fprintf fmt "@]}"
+ fprintf fmt "{@[\"type\": \"constant\",@ \"value\": \"%s\",@ " s;
+ pp_typ fmt;
+ fprintf fmt "@]}"
| _ -> (
fprintf fmt "{@[\"type\": \"constant\",@ \"value\": \"%a\",@ "
Printers.pp_const c;
- fprintf fmt "\"datatype\": \"%a\"@ " pp_cst_type c;
+ pp_typ fmt;
fprintf fmt "@]}"
)
-
+(* Print a value: either a constant or a variable value *)
let pp_emf_cst_or_var m fmt v =
match v.value_desc with
- | Cst c -> pp_emf_cst fmt c
+ | Cst c -> pp_emf_cst c v.value_type fmt
| Var v -> (
fprintf fmt "{@[\"type\": \"variable\",@ \"value\": \"%a\",@ "
pp_var_name v;
@@ -239,7 +306,7 @@ let pp_emf_cst_or_var_list m =
let rec pp_emf_expr fmt e =
match e.expr_desc with
- | Expr_const c -> pp_emf_cst fmt c
+ | Expr_const c -> pp_emf_cst c e.expr_type fmt
| Expr_ident id ->
fprintf fmt "{@[\"type\": \"variable\",@ \"value\": \"%a\",@ "
print_protect (fun fmt -> pp_print_string fmt id);
@@ -254,6 +321,18 @@ let rec pp_emf_expr fmt e =
| Expr_tuple el ->
fprintf fmt "[@[<hov 0>%a@ @]]"
(Utils.fprintf_list ~sep:",@ " pp_emf_expr) el
+ (* Missing these
+ | Expr_ite of expr * expr * expr
+ | Expr_arrow of expr * expr
+ | Expr_fby of expr * expr
+ | Expr_array of expr list
+ | Expr_access of expr * Dimension.dim_expr
+ | Expr_power of expr * Dimension.dim_expr
+ | Expr_pre of expr
+ | Expr_when of expr * ident * label
+ | Expr_merge of ident * (label * expr) list
+ | Expr_appl of call_t
+ *)
| _ -> (
Log.report ~level:2
(fun fmt ->
@@ -274,14 +353,75 @@ let rec pp_emf_expr fmt e =
(* | Expr_when of expr * ident * label *)
(* | Expr_merge of ident * (label * expr) list *)
(* | Expr_appl of call_t *)
-
+let pp_emf_exprs = pp_emf_list pp_emf_expr
+
+let pp_emf_const fmt v =
+ fprintf fmt "@[{\"name\": \"%a\", \"datatype\":\"%a\", \"original_name\": \"%a\", \"value\": \"%a\"}@]"
+ pp_var_name v
+ pp_var_type v
+ Printers.pp_var_name v
+ pp_emf_expr (match v.var_dec_value with None -> assert false | Some e -> e)
+
+let pp_emf_consts = pp_emf_list pp_emf_const
+
let pp_emf_eexpr fmt ee =
fprintf fmt "{@[<hov 0>\"quantifiers\": \"%a\",@ \"qfexpr\": @[%a@]@] }"
(Utils.fprintf_list ~sep:"; " Printers.pp_quantifiers) ee.eexpr_quantifiers
pp_emf_expr ee.eexpr_qfexpr
-
-
+
+let pp_emf_eexprs = pp_emf_list pp_emf_eexpr
+
+(*
+ TODO Thanksgiving
+
+ trouver un moyen de transformer en machine code les instructions de chaque spec
+ peut etre associer a chaque imported node une minimachine
+ et rajouter un champ a spec dans machine code pour stoquer memoire et instr
+ *)
+
+let pp_emf_stmt fmt stmt =
+ match stmt with
+ | Aut _ -> assert false
+ | Eq eq -> (
+ fprintf fmt "@[ @[<v 2>\"%a\": {@ " (Utils.fprintf_list ~sep:"_" pp_print_string) eq.eq_lhs;
+ fprintf fmt "\"lhs\": [%a],@ " (Utils.fprintf_list ~sep:", " (fun fmt vid -> fprintf fmt "\"%s\"" vid)) eq.eq_lhs;
+ fprintf fmt "\"rhs\": \"%a\",@ " pp_emf_expr eq.eq_rhs;
+ fprintf fmt "@]@]@ }"
+ )
+
+let pp_emf_stmts = pp_emf_list pp_emf_stmt
+
+(* Printing the type declaration, not its use *)
+let rec pp_emf_typ_dec fmt tydef_dec =
+ fprintf fmt "{";
+ (match tydef_dec with
+ | Tydec_any -> fprintf fmt "\"kind\": \"any\""
+ | Tydec_int -> fprintf fmt "\"kind\": \"int\""
+ | Tydec_real -> fprintf fmt "\"kind\": \"real\""
+ | Tydec_bool-> fprintf fmt "\"kind\": \"bool\""
+ | Tydec_clock ck -> pp_emf_typ_dec fmt ck
+ | Tydec_const c -> fprintf fmt "\"kind\": \"alias\",@ \"value\": \"%s\"" c
+ | Tydec_enum el -> fprintf fmt "\"kind\": \"enum\",@ \"elements\": [%a]"
+ (Utils.fprintf_list ~sep:", " (fun fmt e -> fprintf fmt "\"%s\"" e)) el
+ | Tydec_struct s -> fprintf fmt "\"kind\": \"struct\",@ \"fields\": [%a]"
+ (Utils.fprintf_list ~sep:", " (fun fmt (id,typ) ->
+ fprintf fmt "\"%s\": %a" id pp_emf_typ_dec typ)) s
+ | Tydec_array (dim, typ) -> fprintf fmt "\"kind\": \"array\",@ \"dim\": @[%a@],@ \"base\": %a"
+ pp_emf_dim dim
+ pp_emf_typ_dec typ
+ );
+ fprintf fmt "}"
+
+let pp_emf_typedef fmt typdef_top =
+ let typedef = Corelang.typedef_of_top typdef_top in
+ fprintf fmt "\"%s\": @[%a@]" typedef.tydef_id pp_emf_typ_dec typedef.tydef_desc
+
+let pp_emf_top_const fmt const_top =
+ let const = Corelang.const_of_top const_top in
+ fprintf fmt "\"%s\": " const.const_id;
+ pp_emf_cst const.const_value const.const_type fmt
+
(* Local Variables: *)
(* compile-command: "make -C ../.." *)
(* End: *)
diff --git a/src/compiler_stages.ml b/src/compiler_stages.ml
index d312a874..a6ac6272 100644
--- a/src/compiler_stages.ml
+++ b/src/compiler_stages.ml
@@ -188,12 +188,13 @@ let stage1 params prog dirname basename extension =
Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
let prog = Normalization.normalize_prog params prog in
Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
-
+
(* Compatibility with Lusi *)
(* If compiling a lusi, generate the lusic. If this is a lus file, Check the existence of a lusi (Lustre Interface file) *)
compile_source_to_header
prog !Global.type_env !Global.clock_env dirname basename extension;
+
let prog =
if !Options.mpfr
then
diff --git a/src/corelang.ml b/src/corelang.ml
index 6d5ad318..48ea8745 100644
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -220,7 +220,6 @@ let mkeexpr loc expr =
eexpr_quantifiers = [];
eexpr_type = Types.new_var ();
eexpr_clock = Clocks.new_var true;
- eexpr_normalized = None;
eexpr_loc = loc }
let extend_eexpr q e = { e with eexpr_quantifiers = q@e.eexpr_quantifiers }
@@ -805,13 +804,6 @@ and rename_eexpr f_node f_var ee =
eexpr_tag = Utils.new_tag ();
eexpr_qfexpr = rename_expr f_node f_var ee.eexpr_qfexpr;
eexpr_quantifiers = List.map (fun (typ,vdecls) -> typ, rename_vars f_node f_var vdecls) ee.eexpr_quantifiers;
- eexpr_normalized = Utils.option_map
- (fun (vdecl, eqs, vdecls) ->
- rename_var f_node f_var vdecl,
- List.map (rename_eq f_node f_var) eqs,
- rename_vars f_node f_var vdecls
- ) ee.eexpr_normalized;
-
}
@@ -1035,7 +1027,6 @@ let rec substitute_expr vars_to_replace defs e =
eexpr_type = expr.expr_type;
eexpr_clock = expr.expr_clock;
eexpr_loc = expr.expr_loc;
- eexpr_normalized = None
}
(* and expr_desc_to_eexpr_desc expr_desc = *)
(* let conv = expr_to_eexpr in *)
diff --git a/src/corelang.mli b/src/corelang.mli
index 20dd55e1..bb9675b3 100644
--- a/src/corelang.mli
+++ b/src/corelang.mli
@@ -86,6 +86,7 @@ val const_and: constant -> constant -> constant
val const_xor: constant -> constant -> constant
val const_impl: constant -> constant -> constant
+val get_var: ident -> var_decl list -> var_decl
val get_node_vars: node_desc -> var_decl list
val get_node_var: ident -> node_desc -> var_decl
val get_node_eqs: node_desc -> eq list * automata_desc list
diff --git a/src/lustre_types.ml b/src/lustre_types.ml
index d3bc43dc..829a9344 100644
--- a/src/lustre_types.ml
+++ b/src/lustre_types.ml
@@ -118,7 +118,7 @@ and eexpr =
eexpr_quantifiers: (quantifier_type * var_decl list) list;
mutable eexpr_type: Types.type_expr;
mutable eexpr_clock: Clocks.clock_expr;
- mutable eexpr_normalized: (var_decl * eq list * var_decl list) option;
+ (* mutable eexpr_normalized: (var_decl * eq list * var_decl list) option; *)
eexpr_loc: Location.t}
and expr_annot =
diff --git a/src/machine_code.ml b/src/machine_code.ml
index f8b88619..143d7d43 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -20,40 +20,44 @@ exception NormalizationError
-(* translate_<foo> : node -> context -> <foo> -> machine code/expression *)
+(* translate_<foo> : vars -> context -> <foo> -> machine code/expression *)
(* the context contains m : state aka memory variables *)
(* si : initialization instructions *)
(* j : node aka machine instances *)
(* d : local variables *)
(* s : step instructions *)
-let translate_ident node (m, si, j, d, s) id =
+let translate_ident vars _ (* (m, si, j, d, s) *) id =
(* Format.eprintf "trnaslating ident: %s@." id; *)
- try (* id is a node var *)
- let var_id = get_node_var id node in
+ try (* id is a var that shall be visible here , ie. in vars *)
+ let var_id = get_var id vars in
mk_val (Var var_id) var_id.var_type
with Not_found ->
try (* id is a constant *)
- let vdecl = (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))) in
+ let vdecl = (Corelang.var_decl_of_const
+ (const_of_top (Hashtbl.find Corelang.consts_table id)))
+ in
mk_val (Var vdecl) vdecl.var_type
with Not_found ->
(* id is a tag *)
- (* DONE construire une liste des enum declarés et alors chercher dedans la liste
- qui contient id *)
+ (* DONE construire une liste des enum declarés et alors chercher
+ dedans la liste qui contient id *)
try
let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in
mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)
- with Not_found -> (Format.eprintf "internal error: Machine_code.translate_ident %s" id;
+ with Not_found -> (Format.eprintf
+ "internal error: Machine_code.translate_ident %s"
+ id;
assert false)
-let rec control_on_clock node ((m, si, j, d, s) as args) ck inst =
+let rec control_on_clock vars ((m, si, j, d, s) as args) ck inst =
match (Clocks.repr ck).cdesc with
| Con (ck1, cr, l) ->
let id = Clocks.const_of_carrier cr in
- control_on_clock node args ck1 (mkinstr
+ control_on_clock vars args ck1 (mkinstr
(* TODO il faudrait prendre le lustre
associé à instr et rajouter print_ck_suffix
ck) de clocks.ml *)
- (MBranch (translate_ident node args id,
+ (MBranch (translate_ident vars args id,
[l, [inst]] )))
| _ -> inst
@@ -79,31 +83,44 @@ let specialize_op expr =
| "C" -> specialize_to_c expr
| _ -> expr
-let rec translate_expr node ((m, si, j, d, s) as args) expr =
+let rec translate_expr vars ((m, si, j, d, s) as args) expr =
let expr = specialize_op expr in
+ (* all calls are using the same arguments (vars for the variable
+ enviroment and args for computed memories). No fold constructs
+ here. We can do partial evaluation of translate_expr *)
+ let translate_expr = translate_expr vars args in
let value_desc =
match expr.expr_desc with
| Expr_const v -> Cst v
- | Expr_ident x -> (translate_ident node args x).value_desc
- | Expr_array el -> Array (List.map (translate_expr node args) el)
- | Expr_access (t, i) -> Access (translate_expr node args t, translate_expr node args (expr_of_dimension i))
- | Expr_power (e, n) -> Power (translate_expr node args e, translate_expr node args (expr_of_dimension n))
+ | Expr_ident x -> (translate_ident vars args x).value_desc
+ | Expr_array el -> Array (List.map translate_expr el)
+ | Expr_access (t, i) -> Access (translate_expr t,
+ translate_expr
+ (expr_of_dimension i))
+ | Expr_power (e, n) -> Power (translate_expr e,
+ translate_expr
+ (expr_of_dimension n))
| Expr_tuple _
- | Expr_arrow _
- | Expr_fby _
- | Expr_pre _ -> (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
- | Expr_when (e1, _, _) -> (translate_expr node args e1).value_desc
+ | Expr_arrow _
+ | Expr_fby _
+ | Expr_pre _ -> (Printers.pp_expr
+ Format.err_formatter expr;
+ Format.pp_print_flush
+ Format.err_formatter ();
+ raise NormalizationError)
+
+ | Expr_when (e1, _, _) -> (translate_expr e1).value_desc
| Expr_merge (x, _) -> raise NormalizationError
| Expr_appl (id, e, _) when Basic_library.is_expr_internal_fun expr ->
- let nd = node_from_name id in
- Fun (node_name nd, List.map (translate_expr node args) (expr_list_of_expr e))
+ let nd = node_from_name id in
+ Fun (node_name nd, List.map translate_expr (expr_list_of_expr e))
| Expr_ite (g,t,e) -> (
(* special treatment depending on the active backend. For horn backend, ite
are preserved in expression. While they are removed for C or Java
backends. *)
match !Options.output with
| "horn" ->
- Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
+ Fun ("ite", [translate_expr g; translate_expr t; translate_expr e])
| "C" | "java" | _ ->
(Format.eprintf "Normalization error for backend %s: %a@."
!Options.output
@@ -114,65 +131,89 @@ let rec translate_expr node ((m, si, j, d, s) as args) expr =
in
mk_val value_desc expr.expr_type
-let translate_guard node args expr =
+let translate_guard vars args expr =
match expr.expr_desc with
- | Expr_ident x -> translate_ident node args x
- | _ -> (Format.eprintf "internal error: translate_guard %s %a@." node.node_id Printers.pp_expr expr;assert false)
+ | Expr_ident x -> translate_ident vars args x
+ | _ -> (Format.eprintf "internal error: translate_guard %a@."
+ Printers.pp_expr expr;
+ assert false)
-let rec translate_act node ((m, si, j, d, s) as args) (y, expr) =
+let rec translate_act vars ((m, si, j, d, s) as args) (y, expr) =
+ let translate_act = translate_act vars args in
+ let translate_guard = translate_guard vars args in
+ let translate_ident = translate_ident vars args in
+ let translate_expr = translate_expr vars args in
let eq = Corelang.mkeq Location.dummy_loc ([y.var_id], expr) in
match expr.expr_desc with
- | Expr_ite (c, t, e) -> let g = translate_guard node args c in
+ | Expr_ite (c, t, e) -> let g = translate_guard c in
mk_conditional ?lustre_eq:(Some eq) g
- [translate_act node args (y, t)]
- [translate_act node args (y, e)]
- | Expr_merge (x, hl) -> mkinstr ?lustre_eq:(Some eq) (MBranch (translate_ident node args x,
- List.map (fun (t, h) -> t, [translate_act node args (y, h)]) hl))
- | _ -> mkinstr ?lustre_eq:(Some eq) (MLocalAssign (y, translate_expr node args expr))
+ [translate_act (y, t)]
+ [translate_act (y, e)]
+ | Expr_merge (x, hl) -> mkinstr ?lustre_eq:(Some eq)
+ (MBranch (translate_ident x,
+ List.map (fun (t, h) ->
+ t, [translate_act (y, h)])
+ hl))
+ | _ -> mkinstr ?lustre_eq:(Some eq)
+ (MLocalAssign (y, translate_expr expr))
-let reset_instance node args i r c =
+let reset_instance vars args i r c =
match r with
| None -> []
- | Some r -> let g = translate_guard node args r in
- [control_on_clock node args c (mk_conditional g [mkinstr (MReset i)] [mkinstr (MNoReset i)])]
+ | Some r -> let g = translate_guard vars args r in
+ [control_on_clock
+ vars
+ args
+ c
+ (mk_conditional
+ g
+ [mkinstr (MReset i)]
+ [mkinstr (MNoReset i)])
+ ]
+
+let translate_eq vars ((m, si, j, d, s) as args) eq =
+ let translate_expr = translate_expr vars args in
+ let translate_act = translate_act vars args in
+ let control_on_clock = control_on_clock vars args in
+ let reset_instance = reset_instance vars args in
-let translate_eq node ((m, si, j, d, s) as args) eq =
- (* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *)
+ (* Format.eprintf "translate_eq %a with clock %a@."
+ Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *)
match eq.eq_lhs, eq.eq_rhs.expr_desc with
| [x], Expr_arrow (e1, e2) ->
- let var_x = get_node_var x node in
- let o = new_instance node Arrow.arrow_top_decl eq.eq_rhs.expr_tag in
- let c1 = translate_expr node args e1 in
- let c2 = translate_expr node args e2 in
+ let var_x = get_var x vars in
+ let o = new_instance Arrow.arrow_top_decl eq.eq_rhs.expr_tag in
+ let c1 = translate_expr e1 in
+ let c2 = translate_expr e2 in
(m,
mkinstr (MReset o) :: si,
Utils.IMap.add o (Arrow.arrow_top_decl, []) j,
d,
- (control_on_clock node args eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStep ([var_x], o, [c1;c2])))) :: s)
- | [x], Expr_pre e1 when VSet.mem (get_node_var x node) d ->
- let var_x = get_node_var x node in
+ (control_on_clock eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStep ([var_x], o, [c1;c2])))) :: s)
+ | [x], Expr_pre e1 when VSet.mem (get_var x vars) d ->
+ let var_x = get_var x vars in
(VSet.add var_x m,
si,
j,
d,
- control_on_clock node args eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr node args e1))) :: s)
- | [x], Expr_fby (e1, e2) when VSet.mem (get_node_var x node) d ->
- let var_x = get_node_var x node in
+ control_on_clock eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr e1))) :: s)
+ | [x], Expr_fby (e1, e2) when VSet.mem (get_var x vars) d ->
+ let var_x = get_var x vars in
(VSet.add var_x m,
- mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr node args e1)) :: si,
+ mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr e1)) :: si,
j,
d,
- control_on_clock node args eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr node args e2))) :: s)
+ control_on_clock eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr e2))) :: s)
| p , Expr_appl (f, arg, r) when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->
- let var_p = List.map (fun v -> get_node_var v node) p in
+ let var_p = List.map (fun v -> get_var v vars) p in
let el = expr_list_of_expr arg in
- let vl = List.map (translate_expr node args) el in
+ let vl = List.map translate_expr el in
let node_f = node_from_name f in
let call_f =
node_f,
NodeDep.filter_static_inputs (node_inputs node_f) el in
- let o = new_instance node node_f eq.eq_rhs.expr_tag in
+ let o = new_instance node_f eq.eq_rhs.expr_tag in
let env_cks = List.fold_right (fun arg cks -> arg.expr_clock :: cks) el [eq.eq_rhs.expr_clock] in
let call_ck = Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks) in
(*Clocks.new_var true in
@@ -184,8 +225,8 @@ let translate_eq node ((m, si, j, d, s) as args) eq =
d,
(if Stateless.check_node node_f
then []
- else reset_instance node args o r call_ck) @
- (control_on_clock node args call_ck (mkinstr ?lustre_eq:(Some eq) (MStep (var_p, o, vl)))) :: s)
+ else reset_instance o r call_ck) @
+ (control_on_clock call_ck (mkinstr ?lustre_eq:(Some eq) (MStep (var_p, o, vl)))) :: s)
(*
(* special treatment depending on the active backend. For horn backend, x = ite (g,t,e)
are preserved. While they are replaced as if g then x = t else x = e in C or Java
@@ -204,13 +245,11 @@ let translate_eq node ((m, si, j, d, s) as args) eq =
*)
| [x], _ -> (
- let var_x = get_node_var x node in
+ let var_x = get_var x vars in
(m, si, j, d,
control_on_clock
- node
- args
eq.eq_rhs.expr_clock
- (translate_act node args (var_x, eq.eq_rhs)) :: s
+ (translate_act (var_x, eq.eq_rhs)) :: s
)
)
| _ ->
@@ -235,15 +274,8 @@ let constant_equations nd =
let translate_eqs node args eqs =
List.fold_right (fun eq args -> translate_eq node args eq) eqs args;;
-let translate_decl nd sch =
- (*Log.report ~level:1 (fun fmt -> Printers.pp_node fmt nd);*)
- let schedule = sch.Scheduling_type.schedule in
- let sorted_eqs = Scheduling.sort_equations_from_schedule nd schedule in
- let constant_eqs = constant_equations nd in
-
- (* In case of non functional backend (eg. C), additional local variables have
- to be declared for each assert *)
- let new_locals, assert_instrs, nd_node_asserts =
+let process_asserts nd =
+
let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in
if Backends.is_functional () then
[], [], exprl
@@ -267,21 +299,41 @@ let translate_decl nd sch =
in
assert_var.var_type <- Type_predef.type_bool (* Types.new_ty (Types.Tbool) *);
let eq = mkeq loc ([var_id], expr) in
- (i+1, assert_var::vars, eq::eqlist, {expr with expr_desc = Expr_ident var_id}::assertlist)
+ (i+1, assert_var::vars, eq::eqlist, {expr with expr_desc = Expr_ident var_id}::assertlist)
) (1, [], [], []) exprl
in
vars, eql, assertl
- in
- let locals_list = nd.node_locals @ new_locals in
+
+let translate_decl nd sch =
+ (*Log.report ~level:1 (fun fmt -> Printers.pp_node fmt nd);*)
+ let schedule = sch.Scheduling_type.schedule in
+ let sorted_eqs = Scheduling.sort_equations_from_schedule nd schedule in
+ let constant_eqs = constant_equations nd in
+ (* In case of non functional backend (eg. C), additional local variables have
+ to be declared for each assert *)
+ let new_locals, assert_instrs, nd_node_asserts = process_asserts nd in
+ let locals_list = nd.node_locals @ new_locals in
let nd = { nd with node_locals = locals_list } in
+ let vars = get_node_vars nd in
+
let init_args = VSet.empty, [], Utils.IMap.empty, List.fold_right (fun l -> VSet.add l) locals_list VSet.empty, [] in
(* memories, init instructions, node calls, local variables (including memories), step instrs *)
- let m0, init0, j0, locals0, s0 = translate_eqs nd init_args constant_eqs in
+
+ let m0, init0, j0, locals0, s0 =
+ translate_eqs vars init_args constant_eqs
+ in
+
assert (VSet.is_empty m0);
assert (init0 = []);
assert (Utils.IMap.is_empty j0);
- let m, init, j, locals, s as context_with_asserts = translate_eqs nd (m0, init0, j0, locals0, []) (assert_instrs@sorted_eqs) in
+
+ let m, init, j, locals, s as context_with_asserts =
+ translate_eqs
+ vars
+ (m0, init0, j0, locals0, [])
+ (assert_instrs@sorted_eqs)
+ in
let mmap = Utils.IMap.fold (fun i n res -> (i, n)::res) j [] in
{
mname = nd;
@@ -295,7 +347,10 @@ let translate_decl nd sch =
step_inputs = nd.node_inputs;
step_outputs = nd.node_outputs;
step_locals = VSet.elements (VSet.diff locals m);
- step_checks = List.map (fun d -> d.Dimension.dim_loc, translate_expr nd init_args (expr_of_dimension d)) nd.node_checks;
+ step_checks = List.map (fun d -> d.Dimension.dim_loc,
+ translate_expr vars init_args
+ (expr_of_dimension d))
+ nd.node_checks;
step_instrs = (
(* special treatment depending on the active backend. For horn backend,
common branches are not merged while they are in C or Java
@@ -308,7 +363,7 @@ let translate_decl nd sch =
else
s
);
- step_asserts = List.map (translate_expr nd context_with_asserts) nd_node_asserts;
+ step_asserts = List.map (translate_expr vars context_with_asserts) nd_node_asserts;
};
mspec = nd.node_spec;
mannot = nd.node_annot;
diff --git a/src/machine_code_common.ml b/src/machine_code_common.ml
index d72cf89d..f784d10f 100644
--- a/src/machine_code_common.ml
+++ b/src/machine_code_common.ml
@@ -216,7 +216,7 @@ let empty_machine =
let new_instance =
let cpt = ref (-1) in
- fun caller callee tag ->
+ fun callee tag ->
begin
let o =
if Stateless.check_node callee then
@@ -225,7 +225,9 @@ let new_instance =
Printf.sprintf "ni_%d" (incr cpt; !cpt) in
let o =
if !Options.ansi && is_generic_node callee
- then Printf.sprintf "%s_inst_%d" o (Utils.position (fun e -> e.expr_tag = tag) caller.node_gencalls)
+ then Printf.sprintf "%s_inst_%d"
+ o
+ (incr cpt; !cpt)
else o in
o
end
diff --git a/src/machine_code_common.mli b/src/machine_code_common.mli
index a5eede3d..ad080b34 100644
--- a/src/machine_code_common.mli
+++ b/src/machine_code_common.mli
@@ -9,7 +9,7 @@ val mk_val: Machine_code_types.value_t_desc -> Types.type_expr -> Machine_code_t
val mk_conditional: ?lustre_eq:Lustre_types.eq -> Machine_code_types.value_t -> Machine_code_types.instr_t list -> Machine_code_types.instr_t list -> Machine_code_types.instr_t
val empty_machine: Machine_code_types.machine_t
val arrow_machine: Machine_code_types.machine_t
-val new_instance: Lustre_types.node_desc -> Lustre_types.top_decl -> Lustre_types.tag -> Lustre_types.ident
+val new_instance: Lustre_types.top_decl -> Lustre_types.tag -> Lustre_types.ident
val value_of_dimension: Machine_code_types.machine_t -> Dimension.dim_expr -> Machine_code_types.value_t
val dimension_of_value:Machine_code_types.value_t -> Dimension.dim_expr
val pp_instr: Machine_code_types.machine_t -> Format.formatter -> Machine_code_types.instr_t -> unit
diff --git a/src/machine_code_types.ml b/src/machine_code_types.ml
index 7a614e29..4d962b66 100644
--- a/src/machine_code_types.ml
+++ b/src/machine_code_types.ml
@@ -41,6 +41,7 @@ and instr_t_desc =
type static_call = top_decl * (Dimension.dim_expr list)
+
type machine_t = {
mname: node_desc;
mmemory: var_decl list;
diff --git a/src/normalization.ml b/src/normalization.ml
index e151836a..ca5cfd76 100644
--- a/src/normalization.ml
+++ b/src/normalization.ml
@@ -170,14 +170,16 @@ let mk_expr_alias_opt opt norm_ctx (defs, vars) expr =
then
let new_aliases =
List.map2
- (mk_fresh_var (norm_ctx.parentid, norm_ctx.vars) expr.expr_loc)
+ (mk_fresh_var (norm_ctx.parentid, (norm_ctx.vars@vars)) expr.expr_loc)
(Types.type_list_of_type expr.expr_type)
(Clocks.clock_list_of_clock expr.expr_clock) in
let new_def =
mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
in
(* Typing and Registering machine type *)
- let _ = if Machine_types.is_active then Machine_types.type_def (norm_ctx.parentid, norm_ctx.vars) new_aliases expr in
+ let _ = if Machine_types.is_active then
+ Machine_types.type_def (norm_ctx.parentid, norm_ctx.vars) new_aliases expr
+ in
(new_def::defs, new_aliases@vars), replace_expr new_aliases expr
else
(defs, vars), expr
@@ -400,46 +402,110 @@ let rec normalize_eq norm_ctx defvars eq =
let normalize_eq_split norm_ctx defvars eq =
try
let defs, vars = normalize_eq norm_ctx defvars eq in
- List.fold_right (fun eq (def, vars) ->
- let eq_defs = Splitting.tuple_split_eq eq in
- if eq_defs = [eq] then
- eq::def, vars
- else
- List.fold_left (normalize_eq norm_ctx) (def, vars) eq_defs
- ) defs ([], vars)
-
- with _ -> (
+ List.fold_right (fun eq (def, vars) ->
+ let eq_defs = Splitting.tuple_split_eq eq in
+ if eq_defs = [eq] then
+ eq::def, vars
+ else
+ List.fold_left (normalize_eq norm_ctx) (def, vars) eq_defs
+ ) defs ([], vars)
+
+ with ex -> (
Format.eprintf "Issue normalizing eq split: %a@." Printers.pp_node_eq eq;
- assert false
+ raise ex
)
-let normalize_eexpr decls norm_ctx vars ee = ee (*
- (* New output variable *)
- let output_id = "spec" ^ string_of_int ee.eexpr_tag in
- let output_var =
- mkvar_decl
- ee.eexpr_loc
- (output_id,
- mktyp ee.eexpr_loc Tydec_any, (*TODO: Make it bool when it is spec *)
- mkclock ee.eexpr_loc Ckdec_any,
- false (* not a constant *),
- None,
- None
- )
+(* Projecting an eexpr to an eexpr associated to a single
+ variable. Returns the updated ee, the bounded variable and the
+ associated statement *)
+let normalize_pred_eexpr decls norm_ctx (def,vars) ee =
+ assert (ee.eexpr_quantifiers = []); (* We do not normalize quantifiers yet. This is for very far future. *)
+ (* don't do anything is eexpr is just a variable *)
+ let skip =
+ match ee.eexpr_qfexpr.expr_desc with
+ | Expr_ident _ | Expr_const _ -> true
+ | _ -> false
in
+ if skip then
+ ee, (def, vars)
+ else (
+ (* New output variable *)
+ let output_id = "spec" ^ string_of_int ee.eexpr_tag in
+ let output_var =
+ mkvar_decl
+ ee.eexpr_loc
+ (output_id,
+ mktyp ee.eexpr_loc Tydec_bool, (* It is a predicate, hence a bool *)
+ mkclock ee.eexpr_loc Ckdec_any,
+ false (* not a constant *),
+ None,
+ None
+ )
+ in
+ let output_expr = expr_of_vdecl output_var in
+ (* Rebuilding an eexpr with a silly expression, just a variable *)
+ let ee' = { ee with eexpr_qfexpr = output_expr } in
+
+ (* Now processing a fresh equation output_id = eexpr_qfexpr. We
+ inline possible calls within, normalize it and type/clock the
+ result. *)
+ let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in
+ (* Inlining any calls *)
+ let nodes = get_nodes decls in
+ let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in
+ let vars, eqs =
+ if calls = [] && not (eq_has_arrows eq) then
+ vars, [eq]
+ else
+ assert false (* TODO *)
+ in
+
+ (* Normalizing expr and eqs *)
+ let defs, vars = List.fold_left (normalize_eq_split norm_ctx) (def, vars) eqs in
+(* let todefine =
+ List.fold_left
+ (fun m x-> if List.exists (fun y-> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m)
+ (ISet.add output_id ISet.empty) vars in
+ *)
+
+ (* Typing / Clocking *)
+ try
+ ignore (Typing.type_var_decl_list vars !Global.type_env vars);
+ (*
+ let env = Typing.type_var_decl [] !Global.type_env xxxx output_var in (* typing the variable *)
+ (* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *)
+ let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in
+ (*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*)
+ let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in
+ (* check that table is empty *)
+ if (not (ISet.is_empty undefined_vars)) then
+ raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars));
+
+ (*Format.eprintf "normalized eqs %a@.@?"
+ (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs; *)
+ *)
+
+ ee', (defs, vars)
+
+ with (Types.Error (loc,err)) as exc ->
+ eprintf "Typing error for eexpr %a: %a%a%a@."
+ Printers.pp_eexpr ee
+ Types.pp_error err
+ (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs
+ Location.pp_loc loc
+
+
+ ;
+ raise exc
+
+ )
+
+ (*
let quant_vars = List.flatten (List.map snd ee.eexpr_quantifiers) in
(* Calls are first inlined *)
- let nodes = get_nodes decls in
- let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in
-(* TODO remettre egalement, i ly a un probleme de decapsulage de nodes
- let calls = List.map
- (fun called_nd -> List.find (fun nd2 -> nd2.node_id = called_nd) nodes) calls
- in
-*)
+
(*Format.eprintf "eexpr %a@.calls: %a@.@?" Printers.pp_eexpr ee (Utils.fprintf_list ~sep:", " (fun fmt nd -> pp_print_string fmt nd.node_id)) calls; *)
- let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in
- let locals = node.node_locals @ (List.fold_left (fun accu (_, q) -> q@accu) [] ee.eexpr_quantifiers) in
let (new_locals, eqs) =
if calls = [] && not (eq_has_arrows eq) then
(locals, [eq])
@@ -485,35 +551,70 @@ let normalize_eexpr decls norm_ctx vars ee = ee (*
raise exc
*)
-
-let normalize_spec decls iovars s = s (*
- (* Each stmt is normalized *)
- let orig_vars = iovars @ s.locals in
+
+(* We use node local vars to make sure we are creating fresh variables *)
+let normalize_spec decls parentid (in_vars, out_vars, l_vars) s =
+ (* Original set of variables actually visible from here: iun/out and
+ spec locals (no node locals) *)
+ let orig_vars = in_vars @ out_vars @ s.locals in
let not_is_orig_var v =
List.for_all ((!=) v) orig_vars in
- let defs, vars =
- let eqs, auts = List.fold_right (fun (el,al) s -> match s with Eq e -> e::el, al | Aut a -> el, a::al) s.stmts ([], []) in
- if auts != [] then assert false; (* Automata should be expanded by now. *)
- List.fold_left (normalize_eq node) ([], orig_vars) eqs
+ let norm_ctx = {
+ parentid = parentid;
+ vars = in_vars @ out_vars @ l_vars;
+ is_output = (fun _ -> false) (* no need to introduce fresh variables for outputs *);
+ }
+ in
+ (* Normalizing existing stmts *)
+ let eqs, auts = List.fold_right (fun s (el,al) -> match s with Eq e -> e::el, al | Aut a -> el, a::al) s.stmts ([], []) in
+ if auts != [] then assert false; (* Automata should be expanded by now. *)
+ let defsvars =
+ List.fold_left (normalize_eq norm_ctx) ([], orig_vars) eqs
+ in
+ (* Iterate through predicates and normalize them on the go, creating
+ fresh variables for any guarantees/assumes/require/ensure *)
+ let process_predicates l defvars =
+ List.fold_right (fun ee (accu, defvars) ->
+ let ee', defvars = normalize_pred_eexpr decls norm_ctx defvars ee in
+ ee'::accu, defvars
+ ) l ([], defvars)
in
- let new_locals = List.filter not_is_orig_var vars in (* removing inouts and initial locals ones *)
- (*
+
+ let assume', defsvars = process_predicates s.assume defsvars in
+ let guarantees', defsvars = process_predicates s.guarantees defsvars in
+ let modes', (defs, vars) =
+ List.fold_right (
+ fun m (accu_m, defsvars) ->
+ let require', defsvars = process_predicates m.require defsvars in
+ let ensure', defsvars = process_predicates m.ensure defsvars in
+ { m with require = require'; ensure = ensure' }:: accu_m, defsvars
+ ) s.modes ([], defsvars)
+ in
+
+ let new_locals = List.filter not_is_orig_var vars in (* removing inouts and initial locals ones *)
+
{s with
locals = s.locals @ new_locals;
stmts = List.map (fun eq -> Eq eq) defs;
- let nee _ = () in
- (*normalize_eexpr decls iovars in *)
- List.iter nee s.assume;
- List.iter nee s.guarantees;
- List.iter (fun m ->
- List.iter nee m.require;
- List.iter nee m.ensure
- ) s.modes;
- *)
- s
- *)
+ assume = assume';
+ guarantees = guarantees';
+ modes = modes'
+ }
+(* let nee _ = () in
+ * (\*normalize_eexpr decls iovars in *\)
+ * List.iter nee s.assume;
+ * List.iter nee s.guarantees;
+ * List.iter (fun m ->
+ * List.iter nee m.require;
+ * List.iter nee m.ensure
+ * ) s.modes; *)
+
+
+
+
+
(* The normalization phase introduces new local variables
- output cannot be memories. If this happen, new local variables acting as
@@ -534,8 +635,7 @@ let normalize_spec decls iovars s = s (*
*)
let normalize_node decls node =
reset_cpt_fresh ();
- let inputs_outputs = node.node_inputs@node.node_outputs in
- let orig_vars = inputs_outputs@node.node_locals in
+ let orig_vars = node.node_inputs@node.node_outputs@node.node_locals in
let not_is_orig_var v =
List.for_all ((!=) v) orig_vars in
let norm_ctx = {
@@ -636,7 +736,7 @@ let normalize_node decls node =
Careful: we do not normalize annotations, since they can have the form
x = (a, b, c) *)
- match node.node_spec with None -> None | Some s -> Some (normalize_spec decls inputs_outputs s)
+ match node.node_spec with None -> None | Some s -> Some (normalize_spec decls node.node_id (node.node_inputs, node.node_outputs, node.node_locals) s)
end
in
@@ -658,8 +758,7 @@ let normalize_inode decls nd =
match nd.nodei_spec with
None -> nd
| Some s ->
- let inputs_outputs = nd.nodei_inputs@nd.nodei_outputs in
- let s = normalize_spec decls inputs_outputs s in
+ let s = normalize_spec decls nd.nodei_id (nd.nodei_inputs, nd.nodei_outputs, []) s in
{ nd with nodei_spec = Some s }
let normalize_decl (decls: program_t) (decl: top_decl) : top_decl =
diff --git a/src/typing.ml b/src/typing.ml
index cf4d79ef..dfee23e2 100644
--- a/src/typing.ml
+++ b/src/typing.ml
@@ -27,7 +27,7 @@ open Corelang
open Format
-(* TODO general remark: expect in the add_vdelc, it seems to me that
+(* TODO general remark: except in the add_vdecl, it seems to me that
all the pairs (env, vd_env) should be replace with just env, since
vd_env is never used and the env element is always extract with a
fst *)
@@ -686,7 +686,16 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
undefined_vars_init
eqs
in
-
+ (* Typing each predicate expr *)
+ let type_pred_ee ee : unit=
+ type_subtyping_arg (env, vd_env) (false (* not in main *)) (false (* not a const *)) ee.eexpr_qfexpr type_bool
+ in
+ List.iter type_pred_ee
+ (
+ spec.assume
+ @ spec.guarantees
+ @ List.flatten (List.map (fun m -> m.ensure @ m.require) spec.modes)
+ );
(*TODO
enrich env locally with locals and consts
type each pre/post as a boolean expr
--
GitLab