From 089f94be1a2e20008f617d37955205920f1793b5 Mon Sep 17 00:00:00 2001
From: ploc <ploc@garoche.net>
Date: Fri, 30 Mar 2018 22:43:08 +0200
Subject: [PATCH] MLI for normalization and machine_code. Structs defining
machines are now in machine_code_types
---
src/backends/C/c_backend_common.ml | 24 +++++++--------
src/backends/C/c_backend_header.ml | 12 ++++----
src/backends/C/c_backend_mauve.ml | 1 +
src/backends/EMF/EMF_backend.ml | 2 +-
src/backends/EMF/EMF_common.ml | 2 +-
src/backends/EMF/EMF_library_calls.ml | 2 +-
src/backends/Horn/horn_backend.ml | 2 +-
.../Horn/horn_backend_collecting_sem.ml | 2 +-
src/backends/Horn/horn_backend_common.ml | 2 +-
src/backends/Horn/horn_backend_traces.ml | 2 +-
src/corelang.ml | 2 +-
src/corelang.mli | 2 +-
src/machine_code.ml | 27 -----------------
src/machine_code.mli | 20 +++++++++++++
src/machine_code_types.ml | 24 +++++++++++++++
src/mpfr.ml | 5 ++--
src/normalization.mli | 2 ++
src/pluginType.ml | 2 +-
src/plugins/salsa/machine_salsa_opt.ml | 30 +++++++++----------
src/plugins/salsa/salsaDatatypes.ml | 4 +--
src/plugins/scopes/scopes.ml | 1 +
21 files changed, 96 insertions(+), 74 deletions(-)
create mode 100644 src/machine_code.mli
create mode 100644 src/normalization.mli
diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml
index 946cca32..ad4fbceb 100644
--- a/src/backends/C/c_backend_common.ml
+++ b/src/backends/C/c_backend_common.ml
@@ -12,7 +12,7 @@
open Format
open Lustre_types
open Corelang
-open Machine_code
+open Machine_code_types
let print_version fmt =
@@ -199,7 +199,7 @@ let rec pp_c_val self pp_var fmt v =
| Cst c -> pp_c_const fmt c
| Array vl -> fprintf fmt "{%a}" (Utils.fprintf_list ~sep:", " (pp_c_val self pp_var)) vl
| Access (t, i) -> fprintf fmt "%a[%a]" (pp_c_val self pp_var) t (pp_c_val self pp_var) i
- | Power (v, n) -> (Format.eprintf "internal error: C_backend_common.pp_c_val %a@." pp_val v; assert false)
+ | Power (v, n) -> (Format.eprintf "internal error: C_backend_common.pp_c_val %a@." Machine_code.pp_val v; assert false)
| LocalVar v -> pp_var fmt v
| StateVar v ->
(* array memory vars are represented by an indirection to a local var with the right type,
@@ -219,11 +219,11 @@ let pp_c_var_read m fmt id =
(* mpfr_t is a static array, not treated as general arrays *)
if Types.is_address_type id.var_type
then
- if is_memory m id && not (Types.is_real_type id.var_type && !Options.mpfr)
+ if Machine_code.is_memory m id && not (Types.is_real_type id.var_type && !Options.mpfr)
then fprintf fmt "(*%s)" id.var_id
else fprintf fmt "%s" id.var_id
else
- if is_output m id
+ if Machine_code.is_output m id
then fprintf fmt "*%s" id.var_id
else fprintf fmt "%s" id.var_id
@@ -237,7 +237,7 @@ let pp_c_var_write m fmt id =
then
fprintf fmt "%s" id.var_id
else
- if is_output m id
+ if Machine_code.is_output m id
then
fprintf fmt "%s" id.var_id
else
@@ -274,7 +274,7 @@ let pp_c_decl_local_var m fmt id =
then
Format.fprintf fmt "%a = %a"
(pp_c_type ~var_opt:(Some id) id.var_id) id.var_type
- (pp_c_val "" (pp_c_var_read m)) (get_const_assign m id)
+ (pp_c_val "" (pp_c_var_read m)) (Machine_code.get_const_assign m id)
else
Format.fprintf fmt "%a"
(pp_c_type ~var_opt:(Some id) id.var_id) id.var_type
@@ -322,7 +322,7 @@ let pp_registers_struct fmt m =
()
let print_machine_struct fmt m =
- if fst (get_stateless_status m) then
+ if fst (Machine_code.get_stateless_status m) then
begin
end
else
@@ -464,7 +464,7 @@ let pp_c_main_var_output fmt id =
fprintf fmt "&%s" id.var_id
let pp_main_call mname self fmt m (inputs: Machine_code_types.value_t list) (outputs: var_decl list) =
- if fst (get_stateless_status m)
+ if fst (Machine_code.get_stateless_status m)
then
fprintf fmt "%a (%a%t%a);"
pp_machine_step_name mname
@@ -482,11 +482,11 @@ let pp_main_call mname self fmt m (inputs: Machine_code_types.value_t list) (out
let pp_c_var m self pp_var fmt var =
let open Machine_code_types in
- if is_memory m var
+ if Machine_code.is_memory m var
then
- pp_c_val self pp_var fmt (mk_val (StateVar var) var.var_type)
+ pp_c_val self pp_var fmt (Machine_code.mk_val (StateVar var) var.var_type)
else
- pp_c_val self pp_var fmt (mk_val (LocalVar var) var.var_type)
+ pp_c_val self pp_var fmt (Machine_code.mk_val (LocalVar var) var.var_type)
let pp_array_suffix fmt loop_vars =
@@ -519,7 +519,7 @@ let pp_initialize m self pp_var fmt var =
let pp_const_initialize pp_var fmt const =
let open Machine_code_types in
- let var = mk_val (LocalVar (Corelang.var_decl_of_const const)) const.const_type in
+ let var = Machine_code.mk_val (LocalVar (Corelang.var_decl_of_const const)) const.const_type in
let rec aux indices value fmt typ =
if Types.is_array_type typ
then
diff --git a/src/backends/C/c_backend_header.ml b/src/backends/C/c_backend_header.ml
index acadeebe..07d08268 100644
--- a/src/backends/C/c_backend_header.ml
+++ b/src/backends/C/c_backend_header.ml
@@ -12,7 +12,7 @@
open Format
open Lustre_types
open Corelang
-open Machine_code
+open Machine_code_types
open C_backend_common
(********************************************************************************************)
@@ -22,7 +22,7 @@ open C_backend_common
module type MODIFIERS_HDR =
sig
- val print_machine_decl_prefix: Format.formatter -> Machine_code.machine_t -> unit
+ val print_machine_decl_prefix: Format.formatter -> Machine_code_types.machine_t -> unit
end
module EmptyMod =
@@ -44,9 +44,9 @@ let print_import_standard fmt =
fprintf fmt "#include <mpfr.h>@."
end;
if !Options.cpp then
- fprintf fmt "#include \"%s/arrow.hpp\"@.@." arrow_top_decl.top_decl_owner
+ fprintf fmt "#include \"%s/arrow.hpp\"@.@." Machine_code.arrow_top_decl.top_decl_owner
else
- fprintf fmt "#include \"%s/arrow.h\"@.@." arrow_top_decl.top_decl_owner
+ fprintf fmt "#include \"%s/arrow.h\"@.@." Machine_code.arrow_top_decl.top_decl_owner
end
@@ -162,7 +162,7 @@ let print_static_alloc_macro fmt (m, attr, inst) =
let print_machine_decl fmt m =
begin
Mod.print_machine_decl_prefix fmt m;
- if fst (get_stateless_status m) then
+ if fst (Machine_code.get_stateless_status m) then
begin
fprintf fmt "extern %a;@.@."
print_stateless_prototype
@@ -211,7 +211,7 @@ let print_machine_decl fmt m =
let print_machine_alloc_decl fmt m =
Mod.print_machine_decl_prefix fmt m;
- if fst (get_stateless_status m) then
+ if fst (Machine_code.get_stateless_status m) then
begin
end
else
diff --git a/src/backends/C/c_backend_mauve.ml b/src/backends/C/c_backend_mauve.ml
index 2bc69fef..86f9d4f6 100644
--- a/src/backends/C/c_backend_mauve.ml
+++ b/src/backends/C/c_backend_mauve.ml
@@ -1,4 +1,5 @@
open Lustre_types
+open Machine_code_types
open Corelang
open Machine_code
open Format
diff --git a/src/backends/EMF/EMF_backend.ml b/src/backends/EMF/EMF_backend.ml
index 5098a643..636f596a 100644
--- a/src/backends/EMF/EMF_backend.ml
+++ b/src/backends/EMF/EMF_backend.ml
@@ -245,7 +245,7 @@ let merge_branches instrs =
| _ -> assert false
in
let sorted_branches = List.sort sorting_branches branches in
- instrs @ (join_guards_list sorted_branches)
+ instrs @ (Machine_code.join_guards_list sorted_branches)
let rec pp_emf_instr m fmt i =
let pp_content fmt i =
diff --git a/src/backends/EMF/EMF_common.ml b/src/backends/EMF/EMF_common.ml
index 8f97824f..31de7761 100644
--- a/src/backends/EMF/EMF_common.ml
+++ b/src/backends/EMF/EMF_common.ml
@@ -1,6 +1,6 @@
open Lustre_types
open Machine_code_types
-
+module VSet = Corelang.VSet
open Format
open Machine_code
diff --git a/src/backends/EMF/EMF_library_calls.ml b/src/backends/EMF/EMF_library_calls.ml
index ece2efa7..353dbf59 100644
--- a/src/backends/EMF/EMF_library_calls.ml
+++ b/src/backends/EMF/EMF_library_calls.ml
@@ -4,7 +4,7 @@
considered. *)
open Lustre_types
-open Machine_code
+open Machine_code_types
open Format
open EMF_common
diff --git a/src/backends/Horn/horn_backend.ml b/src/backends/Horn/horn_backend.ml
index 0fb582ab..bdb3c6af 100644
--- a/src/backends/Horn/horn_backend.ml
+++ b/src/backends/Horn/horn_backend.ml
@@ -18,7 +18,7 @@
open Format
open Lustre_types
open Corelang
-open Machine_code
+open Machine_code_types
open Horn_backend_common
open Horn_backend_printers
diff --git a/src/backends/Horn/horn_backend_collecting_sem.ml b/src/backends/Horn/horn_backend_collecting_sem.ml
index 4111eaf0..9c28a488 100644
--- a/src/backends/Horn/horn_backend_collecting_sem.ml
+++ b/src/backends/Horn/horn_backend_collecting_sem.ml
@@ -18,7 +18,7 @@
open Format
open Lustre_types
open Corelang
-open Machine_code
+open Machine_code_types
open Horn_backend_common
open Horn_backend_printers
diff --git a/src/backends/Horn/horn_backend_common.ml b/src/backends/Horn/horn_backend_common.ml
index ce756a4a..a8e677e4 100644
--- a/src/backends/Horn/horn_backend_common.ml
+++ b/src/backends/Horn/horn_backend_common.ml
@@ -11,8 +11,8 @@
open Format
open Lustre_types
+open Machine_code_types
open Corelang
-open Machine_code
let pp_machine_reset_name fmt id = fprintf fmt "%s_reset" id
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
diff --git a/src/backends/Horn/horn_backend_traces.ml b/src/backends/Horn/horn_backend_traces.ml
index 6f4060c8..3e67a632 100644
--- a/src/backends/Horn/horn_backend_traces.ml
+++ b/src/backends/Horn/horn_backend_traces.ml
@@ -18,7 +18,7 @@
open Format
open Lustre_types
open Corelang
-open Machine_code
+open Machine_code_types
open Horn_backend_common
open Horn_backend_printers
diff --git a/src/corelang.ml b/src/corelang.ml
index 6aaf1331..7893f5fe 100755
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -25,7 +25,7 @@ end
module VMap = Map.Make(VDeclModule)
-module VSet = Set.Make(VDeclModule)
+module VSet : Set.S with type elt = var_decl = Set.Make(VDeclModule)
let dummy_type_dec = {ty_dec_desc=Tydec_any; ty_dec_loc=Location.dummy_loc}
diff --git a/src/corelang.mli b/src/corelang.mli
index 4c08dfcf..9cf9dac0 100755
--- a/src/corelang.mli
+++ b/src/corelang.mli
@@ -13,7 +13,7 @@
open Lustre_types
exception Error of Location.t * Error.error_kind
-module VSet: Set.S
+module VSet: Set.S with type elt = Lustre_types.var_decl
val dummy_type_dec: type_dec
val dummy_clock_dec: clock_dec
diff --git a/src/machine_code.ml b/src/machine_code.ml
index 7010d811..45981f63 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -19,10 +19,6 @@ let print_statelocaltag = true
exception NormalizationError
-module OrdVarDecl:Map.OrderedType with type t=var_decl =
- struct type t = var_decl;; let compare = compare end
-
-module VSet = Set.Make(OrdVarDecl)
let rec pp_val fmt v =
match v.value_desc with
@@ -77,29 +73,6 @@ and pp_branch fmt (t, h) =
and pp_instrs fmt il =
Format.fprintf fmt "@[<v 2>%a@]" (Utils.fprintf_list ~sep:"@," pp_instr) il
-type step_t = {
- step_checks: (Location.t * value_t) list;
- step_inputs: var_decl list;
- step_outputs: var_decl list;
- step_locals: var_decl list;
- step_instrs: instr_t list;
- step_asserts: value_t list;
-}
-
-type static_call = top_decl * (Dimension.dim_expr list)
-
-type machine_t = {
- mname: node_desc;
- mmemory: var_decl list;
- mcalls: (ident * static_call) list; (* map from stateful/stateless instance to node, no internals *)
- minstances: (ident * static_call) list; (* sub-map of mcalls, from stateful instance to node *)
- minit: instr_t list;
- mstatic: var_decl list; (* static inputs only *)
- mconst: instr_t list; (* assignments of node constant locals *)
- mstep: step_t;
- mspec: node_annot option;
- mannot: expr_annot list;
-}
(* merge log: get_node_def was in c0f8 *)
(* Returns the node/machine associated to id in m calls *)
diff --git a/src/machine_code.mli b/src/machine_code.mli
new file mode 100644
index 00000000..0458fc5a
--- /dev/null
+++ b/src/machine_code.mli
@@ -0,0 +1,20 @@
+val pp_val: Format.formatter -> Machine_code_types.value_t -> unit
+val is_memory: Machine_code_types.machine_t -> Lustre_types.var_decl -> bool
+val is_output: Machine_code_types.machine_t -> Lustre_types.var_decl -> bool
+val is_const_value: Machine_code_types.value_t -> bool
+val get_const_assign: Machine_code_types.machine_t -> Lustre_types.var_decl -> Machine_code_types.value_t
+val get_stateless_status: Machine_code_types.machine_t -> bool * bool
+val mk_val: Machine_code_types.value_t_desc -> Types.type_expr -> Machine_code_types.value_t
+val empty_machine: Machine_code_types.machine_t
+val arrow_machine: Machine_code_types.machine_t
+val arrow_id: string
+val arrow_top_decl: Lustre_types.top_decl
+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: Format.formatter -> Machine_code_types.instr_t -> unit
+val pp_instrs: Format.formatter -> Machine_code_types.instr_t list -> unit
+val pp_machines: Format.formatter -> Machine_code_types.machine_t list -> unit
+val get_machine_opt: string -> Machine_code_types.machine_t list -> Machine_code_types.machine_t option
+val get_node_def: string -> Machine_code_types.machine_t -> Lustre_types.node_desc
+val join_guards_list: Machine_code_types.instr_t list -> Machine_code_types.instr_t list
+val translate_prog: Lustre_types.program -> Scheduling.schedule_report Utils.IMap.t -> Machine_code_types.machine_t list
diff --git a/src/machine_code_types.ml b/src/machine_code_types.ml
index c82754c2..692684ab 100644
--- a/src/machine_code_types.ml
+++ b/src/machine_code_types.ml
@@ -30,3 +30,27 @@ and instr_t_desc =
| MStep of var_decl list * ident * value_t list
| MBranch of value_t * (label * instr_t list) list
| MComment of string
+
+ type step_t = {
+ step_checks: (Location.t * value_t) list;
+ step_inputs: var_decl list;
+ step_outputs: var_decl list;
+ step_locals: var_decl list;
+ step_instrs: instr_t list;
+ step_asserts: value_t list;
+}
+
+type static_call = top_decl * (Dimension.dim_expr list)
+
+type machine_t = {
+ mname: node_desc;
+ mmemory: var_decl list;
+ mcalls: (ident * static_call) list; (* map from stateful/stateless instance to node, no internals *)
+ minstances: (ident * static_call) list; (* sub-map of mcalls, from stateful instance to node *)
+ minit: instr_t list;
+ mstatic: var_decl list; (* static inputs only *)
+ mconst: instr_t list; (* assignments of node constant locals *)
+ mstep: step_t;
+ mspec: node_annot option;
+ mannot: expr_annot list;
+}
diff --git a/src/mpfr.ml b/src/mpfr.ml
index 363f3d08..8cd62208 100755
--- a/src/mpfr.ml
+++ b/src/mpfr.ml
@@ -17,7 +17,8 @@ open Normalization
open Machine_code
let mpfr_module = mktop (Open(false, "mpfr_lustre"))
-
+let cpt_fresh = ref 0
+
let mpfr_rnd () = "MPFR_RNDN"
let mpfr_prec () = !Options.mpfr_prec
@@ -140,7 +141,7 @@ let rec inject_list alias node inject_element defvars elist =
) elist (defvars, [])
let rec inject_expr ?(alias=true) node defvars expr =
-let res=
+let res =
match expr.expr_desc with
| Expr_const (Const_real _) -> mk_expr_alias_opt alias node defvars expr
| Expr_const (Const_array _) -> inject_expr ~alias:alias node defvars (expr_of_const_array expr)
diff --git a/src/normalization.mli b/src/normalization.mli
new file mode 100644
index 00000000..a24a9452
--- /dev/null
+++ b/src/normalization.mli
@@ -0,0 +1,2 @@
+val mk_expr_alias_opt: bool -> Lustre_types.node_desc -> (Lustre_types.eq list * Lustre_types.var_decl list)-> Lustre_types.expr -> (Lustre_types.eq list * Lustre_types.var_decl list) * Lustre_types.expr
+val normalize_prog: ?backend:string -> Lustre_types.program -> Lustre_types.program
diff --git a/src/pluginType.ml b/src/pluginType.ml
index 8850e3af..3af5b490 100644
--- a/src/pluginType.ml
+++ b/src/pluginType.ml
@@ -5,7 +5,7 @@ sig
val options: (string * Arg.spec * string) list
val check_force_stateful : unit -> bool
val refine_machine_code: Lustre_types.top_decl list ->
- Machine_code.machine_t list -> Machine_code.machine_t list
+ Machine_code_types.machine_t list -> Machine_code_types.machine_t list
val c_backend_main_loop_body_prefix : string -> string -> Format.formatter -> unit -> unit
val c_backend_main_loop_body_suffix : Format.formatter -> unit -> unit
end
diff --git a/src/plugins/salsa/machine_salsa_opt.ml b/src/plugins/salsa/machine_salsa_opt.ml
index 999456ea..283d3d0f 100644
--- a/src/plugins/salsa/machine_salsa_opt.ml
+++ b/src/plugins/salsa/machine_salsa_opt.ml
@@ -22,7 +22,7 @@ let fun_types node =
let called_node_id m id =
let td, _ =
try
- List.assoc id m.MC.mcalls (* TODO Xavier: mcalls or minstances ? *)
+ List.assoc id m.MT.mcalls (* TODO Xavier: mcalls or minstances ? *)
with Not_found -> assert false
in
td
@@ -350,7 +350,7 @@ let rec rewrite_instrs nodename m constEnv vars_env m instrs ranges formalEnv p
produced
variables *)
Format.eprintf "Requited vars: %a@." Vars.pp required_vars;
- let required_vars = Vars.diff required_vars (Vars.of_list m.MC.mmemory) in
+ let required_vars = Vars.diff required_vars (Vars.of_list m.MT.mmemory) in
let prefix_instr, ranges =
assign_vars printed_vars ranges formalEnv required_vars in
@@ -532,7 +532,7 @@ let salsaStep constEnv m s =
| ["salsa"; "ranges"; var] -> (var, range)::accu
| _ -> accu
) accu annl.LT.annots
- ) [] m.MC.mannot
+ ) [] m.MT.mannot
in
let ranges =
List.fold_left (fun ranges (v, value) ->
@@ -565,8 +565,8 @@ let salsaStep constEnv m s =
Vars.real_vars
(
Vars.union
- (Vars.of_list m.MC.mmemory)
- (Vars.of_list s.MC.step_outputs)
+ (Vars.of_list m.MT.mmemory)
+ (Vars.of_list s.MT.step_outputs)
)
in
(* TODO: should be at least step output + may be memories *)
@@ -575,39 +575,39 @@ let salsaStep constEnv m s =
if !debug then Format.eprintf "@[<v 2>Registering node equations@ ";
let new_instrs, _, _, printed_vars, _ =
rewrite_instrs
- m.MC.mname.LT.node_id
+ m.MT.mname.LT.node_id
m
constEnv
vars_env
m
- s.MC.step_instrs
+ s.MT.step_instrs
ranges
formal_env
- (Vars.real_vars (Vars.of_list s.MC.step_inputs (* printed_vars : real
+ (Vars.real_vars (Vars.of_list s.MT.step_inputs (* printed_vars : real
inputs are considered as
already printed *)))
vars_to_print
in
- let all_local_vars = Vars.real_vars (Vars.of_list s.MC.step_locals) in
+ let all_local_vars = Vars.real_vars (Vars.of_list s.MT.step_locals) in
let unused = (Vars.diff all_local_vars printed_vars) in
let locals =
if not (Vars.is_empty unused) then (
Format.eprintf "Unused local vars: [%a]. Removing them.@.@?"
Vars.pp unused;
- List.filter (fun v -> not (Vars.mem v unused)) s.MC.step_locals
+ List.filter (fun v -> not (Vars.mem v unused)) s.MT.step_locals
)
else
- s.MC.step_locals
+ s.MT.step_locals
in
- { s with MC.step_instrs = new_instrs; MC.step_locals = locals } (* we have also to modify local variables to declare new vars *)
+ { s with MT.step_instrs = new_instrs; MT.step_locals = locals } (* we have also to modify local variables to declare new vars *)
let machine_t2machine_t_optimized_by_salsa constEnv mt =
try
- if !debug then Format.eprintf "@[<v 8>[salsa] Optimizing machine %s@ " mt.MC.mname.LT.node_id;
- let new_step = salsaStep constEnv mt mt.MC.mstep in
+ if !debug then Format.eprintf "@[<v 8>[salsa] Optimizing machine %s@ " mt.MT.mname.LT.node_id;
+ let new_step = salsaStep constEnv mt mt.MT.mstep in
if !debug then Format.eprintf "@]@ ";
- { mt with MC.mstep = new_step }
+ { mt with MT.mstep = new_step }
with FormalEnv.NoDefinition v as exp ->
diff --git a/src/plugins/salsa/salsaDatatypes.ml b/src/plugins/salsa/salsaDatatypes.ml
index b0f8d25d..379acf39 100644
--- a/src/plugins/salsa/salsaDatatypes.ml
+++ b/src/plugins/salsa/salsaDatatypes.ml
@@ -212,14 +212,14 @@ let compute_vars_env m =
List.fold_left
(fun accu v -> VarEnv.add v.LT.var_id {vdecl = v; is_local = false; } accu)
env
- m.MC.mmemory
+ m.MT.mmemory
in
let env =
List.fold_left (
fun accu v -> VarEnv.add v.LT.var_id {vdecl = v; is_local = true; } accu
)
env
- MC.(m.mstep.step_inputs@m.mstep.step_outputs@m.mstep.step_locals)
+ MC.(m.MT.mstep.MT.step_inputs@m.MT.mstep.MT.step_outputs@m.MT.mstep.MT.step_locals)
in
env
diff --git a/src/plugins/scopes/scopes.ml b/src/plugins/scopes/scopes.ml
index 24f9456d..79625091 100644
--- a/src/plugins/scopes/scopes.ml
+++ b/src/plugins/scopes/scopes.ml
@@ -1,5 +1,6 @@
open Lustre_types
open Corelang
+open Machine_code_types
open Machine_code
(* (variable, node name, node instance) *)
--
GitLab