diff --git a/src/automata.ml b/src/automata.ml
index 42f547fb65180e178dfab7903f242ba001387125..d079e442d1ad2b6050dbc3003223d64cac90f0da 100755
--- a/src/automata.ml
+++ b/src/automata.ml
@@ -24,6 +24,9 @@ type aut_state =
actual_s : var_decl
}
+let cpvar_decl var_decl =
+ mkvar_decl var_decl.var_loc ~orig:var_decl.var_orig (var_decl.var_id, var_decl.var_dec_type, var_decl.var_dec_clock, var_decl.var_dec_const, var_decl.var_dec_value)
+
let as_clock var_decl =
let tydec = var_decl.var_dec_type in
{ var_decl with var_dec_type = { ty_dec_desc = Tydec_clock tydec.ty_dec_desc; ty_dec_loc = tydec.ty_dec_loc } }
@@ -99,12 +102,12 @@ let mkautomata_state used typedef loc id =
let actual_r = mk_new_name used (id ^ "__restart_act") in
let actual_s = mk_new_name used (id ^ "__state_act") in
{
- incoming_r' = mkvar_decl loc (incoming_r', tydec_bool, ckdec_any, false);
- incoming_s' = mkvar_decl loc (incoming_s', tydec_state typedef.tydef_id, ckdec_any, false);
- incoming_r = mkvar_decl loc (incoming_r, tydec_bool, ckdec_any, false);
- incoming_s = mkvar_decl loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false);
- actual_r = mkvar_decl loc (actual_r , tydec_bool, ckdec_any, false);
- actual_s = mkvar_decl loc (actual_s , tydec_state typedef.tydef_id, ckdec_any, false)
+ incoming_r' = mkvar_decl loc (incoming_r', tydec_bool, ckdec_any, false, None);
+ incoming_s' = mkvar_decl loc (incoming_s', tydec_state typedef.tydef_id, ckdec_any, false, None);
+ incoming_r = mkvar_decl loc (incoming_r, tydec_bool, ckdec_any, false, None);
+ incoming_s = mkvar_decl loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false, None);
+ actual_r = mkvar_decl loc (actual_r , tydec_bool, ckdec_any, false, None);
+ actual_s = mkvar_decl loc (actual_s , tydec_state typedef.tydef_id, ckdec_any, false, None)
}
let vars_of_aut_state aut_state =
@@ -123,8 +126,8 @@ let node_of_unless nused used node aut_id aut_state handler =
node_id = node_id;
node_type = Types.new_var ();
node_clock = Clocks.new_var true;
- node_inputs = var_inputs;
- node_outputs = var_outputs;
+ node_inputs = List.map cpvar_decl var_inputs;
+ node_outputs = List.map cpvar_decl var_outputs;
node_locals = [];
node_gencalls = [];
node_checks = [];
@@ -173,9 +176,9 @@ let node_of_assign_until nused used node aut_id aut_state handler =
node_id = node_id;
node_type = Types.new_var ();
node_clock = Clocks.new_var true;
- node_inputs = var_inputs;
- node_outputs = aut_state.incoming_r :: aut_state.incoming_s :: new_var_outputs;
- node_locals = new_var_locals @ handler.hand_locals;
+ node_inputs = List.map cpvar_decl var_inputs;
+ node_outputs = List.map cpvar_decl (aut_state.incoming_r :: aut_state.incoming_s :: new_var_outputs);
+ node_locals = List.map cpvar_decl (new_var_locals @ handler.hand_locals);
node_gencalls = [];
node_checks = [];
node_asserts = handler.hand_asserts;
diff --git a/src/backends/C/c_backend.ml b/src/backends/C/c_backend.ml
index be30cc996819c4e491cf346dd16a90d0dff6a454..a6d1d711bb632c67e58a10406033b45cc095cb2a 100644
--- a/src/backends/C/c_backend.ml
+++ b/src/backends/C/c_backend.ml
@@ -26,18 +26,19 @@ let makefile_opt print basename dependencies makefile_fmt machines =
*)
let gen_files funs basename prog machines dependencies header_file source_lib_file source_main_file makefile_file machines =
+
let header_out = open_out header_file in
let header_fmt = formatter_of_out_channel header_out in
let source_lib_out = open_out source_lib_file in
let source_lib_fmt = formatter_of_out_channel source_lib_out in
-
+
let print_header, print_lib_c, print_main_c, print_makefile = funs in
(* Generating H file *)
print_header header_fmt basename prog machines dependencies;
-
+
(* Generating Lib C file *)
print_lib_c source_lib_fmt basename prog machines dependencies;
-
+
close_out header_out;
close_out source_lib_out;
@@ -64,8 +65,7 @@ let gen_files funs basename prog machines dependencies header_file source_lib_fi
end
)
-let translate_to_c header source_lib source_main makefile basename prog machines dependencies =
-
+let translate_to_c header source_lib source_main makefile basename prog machines dependencies =
match !Options.spec with
| "no" -> begin
let module HeaderMod = C_backend_header.EmptyMod in
@@ -77,7 +77,7 @@ let translate_to_c header source_lib source_main makefile basename prog machines
let module Source = C_backend_src.Main (SourceMod) in
let module SourceMain = C_backend_main.Main (SourceMainMod) in
let module Makefile = C_backend_makefile.Main (MakefileMod) in
-
+
let funs =
Header.print_alloc_header,
Source.print_lib_c,
@@ -100,7 +100,7 @@ let translate_to_c header source_lib source_main makefile basename prog machines
let module Source = C_backend_src.Main (SourceMod) in
let module SourceMain = C_backend_main.Main (SourceMainMod) in
let module Makefile = C_backend_makefile.Main (MakefileMod) in
-
+
let funs =
Header.print_alloc_header,
Source.print_lib_c,
diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml
index 3ac37bc712e908ff55be9fa9a9da64ac6299ebae..82241ae23412fb9262a2711dbf81967f6029a5d6 100644
--- a/src/backends/C/c_backend_common.ml
+++ b/src/backends/C/c_backend_common.ml
@@ -51,6 +51,7 @@ let mk_call_var_decl loc id =
var_dec_type = mktyp Location.dummy_loc Tydec_any;
var_dec_clock = mkclock Location.dummy_loc Ckdec_any;
var_dec_const = false;
+ var_dec_value = None;
var_type = Type_predef.type_arrow (Types.new_var ()) (Types.new_var ());
var_clock = Clocks.new_var true;
var_loc = loc }
@@ -133,6 +134,73 @@ let rec pp_c_initialize fmt t =
(Utils.duplicate 0 (Dimension.size_const_dimension d))
| _ -> assert false
+
+let pp_c_tag fmt t =
+ pp_print_string fmt (if t = tag_true then "1" else if t = tag_false then "0" else t)
+
+(* Prints a constant value *)
+let rec pp_c_const fmt c =
+ match c with
+ | Const_int i -> pp_print_int fmt i
+ | Const_real r -> pp_print_string fmt r
+ | Const_float r -> pp_print_float fmt r
+ | Const_tag t -> pp_c_tag fmt t
+ | Const_array ca -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " pp_c_const) ca
+ | Const_struct fl -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " (fun fmt (f, c) -> pp_c_const fmt c)) fl
+ | Const_string _ -> assert false (* string occurs in annotations not in C *)
+
+(* Prints a value expression [v], with internal function calls only.
+ [pp_var] is a printer for variables (typically [pp_c_var_read]),
+ but an offset suffix may be added for array variables
+*)
+let rec pp_c_val self pp_var fmt v =
+ match v with
+ | 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) -> 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,
+ in order to avoid casting everywhere. *)
+ if Types.is_array_type v.var_type
+ then fprintf fmt "%a" pp_var v
+ else fprintf fmt "%s->_reg.%a" self pp_var v
+ | Fun (n, vl) -> Basic_library.pp_c n (pp_c_val self pp_var) fmt vl
+
+(* Access to the value of a variable:
+ - if it's not a scalar output, then its name is enough
+ - otherwise, dereference it (it has been declared as a pointer,
+ despite its scalar Lustre type)
+ - moreover, dereference memory array variables.
+*)
+let pp_c_var_read m fmt id =
+ if Types.is_address_type id.var_type
+ then
+ if is_memory m id
+ then fprintf fmt "(*%s)" id.var_id
+ else fprintf fmt "%s" id.var_id
+ else
+ if is_output m id
+ then fprintf fmt "*%s" id.var_id
+ else fprintf fmt "%s" id.var_id
+
+(* Addressable value of a variable, the one that is passed around in calls:
+ - if it's not a scalar non-output, then its name is enough
+ - otherwise, reference it (it must be passed as a pointer,
+ despite its scalar Lustre type)
+*)
+let pp_c_var_write m fmt id =
+ if Types.is_address_type id.var_type
+ then
+ fprintf fmt "%s" id.var_id
+ else
+ if is_output m id
+ then
+ fprintf fmt "%s" id.var_id
+ else
+ fprintf fmt "&%s" id.var_id
+
(* Declaration of an input variable:
- if its type is array/matrix/etc, then declare it as a mere pointer,
in order to cope with unknown/parametric array dimensions,
@@ -159,8 +227,15 @@ let pp_c_decl_output_var fmt id =
known in order to statically allocate memory,
so we print the full type
*)
-let pp_c_decl_local_var fmt id =
- pp_c_type id.var_id fmt id.var_type
+let pp_c_decl_local_var m fmt id =
+ if id.var_dec_const
+ then
+ Format.fprintf fmt "%a = %a"
+ (pp_c_type id.var_id) id.var_type
+ (pp_c_val "" (pp_c_var_read m)) (get_const_assign m id)
+ else
+ Format.fprintf fmt "%a"
+ (pp_c_type id.var_id) id.var_type
let pp_c_decl_array_mem self fmt id =
fprintf fmt "%a = (%a) (%s->_reg.%s)"
@@ -177,75 +252,9 @@ let pp_c_decl_struct_var fmt id =
then pp_c_type (sprintf "(*%s)" id.var_id) fmt (Types.array_base_type id.var_type)
else pp_c_type id.var_id fmt id.var_type
-(* Access to the value of a variable:
- - if it's not a scalar output, then its name is enough
- - otherwise, dereference it (it has been declared as a pointer,
- despite its scalar Lustre type)
- - moreover, dereference memory array variables.
-*)
-let pp_c_var_read m fmt id =
- if Types.is_address_type id.var_type
- then
- if is_memory m id
- then fprintf fmt "(*%s)" id.var_id
- else fprintf fmt "%s" id.var_id
- else
- if is_output m id
- then fprintf fmt "*%s" id.var_id
- else fprintf fmt "%s" id.var_id
-
-(* Addressable value of a variable, the one that is passed around in calls:
- - if it's not a scalar non-output, then its name is enough
- - otherwise, reference it (it must be passed as a pointer,
- despite its scalar Lustre type)
-*)
-let pp_c_var_write m fmt id =
- if Types.is_address_type id.var_type
- then
- fprintf fmt "%s" id.var_id
- else
- if is_output m id
- then
- fprintf fmt "%s" id.var_id
- else
- fprintf fmt "&%s" id.var_id
-
let pp_c_decl_instance_var fmt (name, (node, static)) =
fprintf fmt "%a *%s" pp_machine_memtype_name (node_name node) name
-let pp_c_tag fmt t =
- pp_print_string fmt (if t = tag_true then "1" else if t = tag_false then "0" else t)
-
-(* Prints a constant value *)
-let rec pp_c_const fmt c =
- match c with
- | Const_int i -> pp_print_int fmt i
- | Const_real r -> pp_print_string fmt r
- | Const_float r -> pp_print_float fmt r
- | Const_tag t -> pp_c_tag fmt t
- | Const_array ca -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " pp_c_const) ca
- | Const_struct fl -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " (fun fmt (f, c) -> pp_c_const fmt c)) fl
- | Const_string _ -> assert false (* string occurs in annotations not in C *)
-
-(* Prints a value expression [v], with internal function calls only.
- [pp_var] is a printer for variables (typically [pp_c_var_read]),
- but an offset suffix may be added for array variables
-*)
-let rec pp_c_val self pp_var fmt v =
- match v with
- | 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) -> 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,
- in order to avoid casting everywhere. *)
- if Types.is_array_type v.var_type
- then fprintf fmt "%a" pp_var v
- else fprintf fmt "%s->_reg.%a" self pp_var v
- | Fun (n, vl) -> Basic_library.pp_c n (pp_c_val self pp_var) fmt vl
-
let pp_c_checks self fmt m =
Utils.fprintf_list ~sep:""
(fun fmt (loc, check) ->
diff --git a/src/backends/C/c_backend_header.ml b/src/backends/C/c_backend_header.ml
index 83d01f8ce72f7f0bbf7026743b35c4e68d1a74a3..50e156b80e079e760a77db772832262e9f301878 100644
--- a/src/backends/C/c_backend_header.ml
+++ b/src/backends/C/c_backend_header.ml
@@ -36,34 +36,65 @@ struct
let print_import_standard fmt =
fprintf fmt "#include \"%s/arrow.h\"@.@." Version.include_path
-let print_static_declare_instance attr fmt (i, (m, static)) =
+let rec print_static_val pp_var fmt v =
+ match v with
+ | Cst c -> pp_c_const fmt c
+ | LocalVar v -> pp_var fmt v
+ | Fun (n, vl) -> Basic_library.pp_c n (print_static_val pp_var) fmt vl
+ | _ -> (Format.eprintf "Internal error: C_backend_header.print_static_val"; assert false)
+
+let print_constant m pp_var fmt v =
+ Format.fprintf fmt "inst ## %s = %a"
+ v.var_id
+ (print_static_val pp_var) (Machine_code.get_const_assign m v)
+
+let print_static_constant (m, attr, inst) fmt const_locals =
+ let pp_var fmt v =
+ if List.mem v const_locals
+ then
+ Format.fprintf fmt "%s ## %s" inst v.var_id
+ else
+ Format.fprintf fmt "%s" v.var_id in
+ Format.fprintf fmt "%a%t"
+ (Utils.fprintf_list ~sep:";\\@," (print_constant m pp_var)) const_locals
+ (Utils.pp_final_char_if_non_empty ";\\@," const_locals)
+
+let print_static_declare_instance (m, attr, inst) const_locals fmt (i, (n, static)) =
+ let pp_var fmt v =
+ if List.mem v const_locals
+ then
+ Format.fprintf fmt "%s ## %s" inst v.var_id
+ else
+ Format.fprintf fmt "%s" v.var_id in
+ let values = List.map (Machine_code.value_of_dimension m) static in
fprintf fmt "%a(%s, %a%t%s)"
- pp_machine_static_declare_name (node_name m)
+ pp_machine_static_declare_name (node_name n)
attr
- (Utils.fprintf_list ~sep:", " Dimension.pp_dimension) static
+ (Utils.fprintf_list ~sep:", " (print_static_val pp_var)) values
(Utils.pp_final_char_if_non_empty ", " static)
i
-let print_static_declare_macro fmt m =
+let print_static_declare_macro fmt (m, attr, inst) =
+ let const_locals = List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals in
let array_mem = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
- let inst = mk_instance m in
- let attr = mk_attribute m in
- fprintf fmt "@[<v 2>#define %a(%s, %a%t%s)\\@,%s %a %s;\\@,%a%t%a;@,@]"
+ fprintf fmt "@[<v 2>#define %a(%s, %a%t%s)\\@,%a%s %a %s;\\@,%a%t%a;@,@]"
pp_machine_static_declare_name m.mname.node_id
attr
(Utils.fprintf_list ~sep:", " (pp_c_var_read m)) m.mstatic
(Utils.pp_final_char_if_non_empty ", " m.mstatic)
inst
+ (* constants *)
+ (print_static_constant (m, attr, inst)) const_locals
attr
pp_machine_memtype_name m.mname.node_id
inst
- (Utils.fprintf_list ~sep:";\\@," pp_c_decl_local_var) array_mem
+ (Utils.fprintf_list ~sep:";\\@," (pp_c_decl_local_var m)) array_mem
(Utils.pp_final_char_if_non_empty ";\\@," array_mem)
(Utils.fprintf_list ~sep:";\\@,"
(fun fmt (i',m') ->
- let path = sprintf "inst ## _%s" i' in
+ let path = sprintf "%s ## _%s" inst i' in
fprintf fmt "%a"
- (print_static_declare_instance attr) (path,m')
+ (print_static_declare_instance (m, attr, inst) const_locals) (path, m')
)) m.minstances
@@ -73,13 +104,15 @@ let print_static_link_instance fmt (i, (m, _)) =
(* Allocation of a node struct:
- if node memory is an array/matrix/etc, we cast it to a pointer (see pp_registers_struct)
*)
-let print_static_link_macro fmt m =
+let print_static_link_macro fmt (m, attr, inst) =
let array_mem = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
- fprintf fmt "@[<v>@[<v 2>#define %a(inst) do {\\@,%a%t%a;\\@]@,} while (0)@.@]"
+ fprintf fmt "@[<v>@[<v 2>#define %a(%s) do {\\@,%a%t%a;\\@]@,} while (0)@.@]"
pp_machine_static_link_name m.mname.node_id
+ inst
(Utils.fprintf_list ~sep:";\\@,"
(fun fmt v ->
- fprintf fmt "inst._reg.%s = (%a*) &%s"
+ fprintf fmt "%s._reg.%s = (%a*) &%s"
+ inst
v.var_id
(fun fmt v -> pp_c_type "" fmt (Types.array_base_type v.var_type)) v
v.var_id
@@ -87,24 +120,29 @@ let print_static_link_macro fmt m =
(Utils.pp_final_char_if_non_empty ";\\@," array_mem)
(Utils.fprintf_list ~sep:";\\@,"
(fun fmt (i',m') ->
- let path = sprintf "inst ## _%s" i' in
- fprintf fmt "%a;\\@,inst.%s = &%s"
+ let path = sprintf "%s ## _%s" inst i' in
+ fprintf fmt "%a;\\@,%s.%s = &%s"
print_static_link_instance (path,m')
+ inst
i'
path
)) m.minstances
-
-let print_static_alloc_macro fmt m =
- fprintf fmt "@[<v>@[<v 2>#define %a(attr,%a%tinst)\\@,%a(attr,%a%tinst);\\@,%a(inst);@]@,@]@."
+
+let print_static_alloc_macro fmt (m, attr, inst) =
+ fprintf fmt "@[<v>@[<v 2>#define %a(%s, %a%t%s)\\@,%a(%s, %a%t%s);\\@,%a(%s);@]@,@]@."
pp_machine_static_alloc_name m.mname.node_id
+ attr
(Utils.fprintf_list ~sep:", " (pp_c_var_read m)) m.mstatic
(Utils.pp_final_char_if_non_empty ", " m.mstatic)
+ inst
pp_machine_static_declare_name m.mname.node_id
+ attr
(Utils.fprintf_list ~sep:", " (pp_c_var_read m)) m.mstatic
(Utils.pp_final_char_if_non_empty ", " m.mstatic)
+ inst
pp_machine_static_link_name m.mname.node_id
+ inst
-
let print_machine_decl fmt m =
Mod.print_machine_decl_prefix fmt m;
if fst (get_stateless_status m) then
@@ -117,17 +155,21 @@ let print_machine_decl fmt m =
begin
(* Static allocation *)
if !Options.static_mem
- then (
- fprintf fmt "%a@.%a@.%a@."
- print_static_declare_macro m
- print_static_link_macro m
- print_static_alloc_macro m
- )
- else (
+ then
+ begin
+ let inst = mk_instance m in
+ let attr = mk_attribute m in
+ fprintf fmt "%a@.%a@.%a@."
+ print_static_declare_macro (m, attr, inst)
+ print_static_link_macro (m, attr, inst)
+ print_static_alloc_macro (m, attr, inst)
+ end
+ else
+ begin
(* Dynamic allocation *)
- fprintf fmt "extern %a;@.@."
- print_alloc_prototype (m.mname.node_id, m.mstatic)
- );
+ fprintf fmt "extern %a;@.@."
+ print_alloc_prototype (m.mname.node_id, m.mstatic)
+ end;
let self = mk_self m in
fprintf fmt "extern %a;@.@."
(print_reset_prototype self) (m.mname.node_id, m.mstatic);
@@ -148,10 +190,12 @@ let print_machine_alloc_decl fmt m =
then
begin
(* Static allocation *)
+ let inst = mk_instance m in
+ let attr = mk_attribute m in
fprintf fmt "%a@.%a@.%a@."
- print_static_declare_macro m
- print_static_link_macro m
- print_static_alloc_macro m
+ print_static_declare_macro (m, attr, inst)
+ print_static_link_macro (m, attr, inst)
+ print_static_alloc_macro (m, attr, inst)
end
else
begin
diff --git a/src/backends/C/c_backend_main.ml b/src/backends/C/c_backend_main.ml
index e767723fe8ca32b1ed678474206583b1b654720d..578c6a3e4e936fba9bce0280c176566db3c4d7d5 100644
--- a/src/backends/C/c_backend_main.ml
+++ b/src/backends/C/c_backend_main.ml
@@ -31,7 +31,7 @@ struct
(********************************************************************************************)
let print_get_input fmt v =
- match v.var_type.Types.tdesc with
+ match (Types.repr v.var_type).Types.tdesc with
| Types.Tint -> fprintf fmt "_get_int(\"%s\")" v.var_id
| Types.Tbool -> fprintf fmt "_get_bool(\"%s\")" v.var_id
| Types.Treal -> fprintf fmt "_get_double(\"%s\")" v.var_id
@@ -39,7 +39,7 @@ let print_get_input fmt v =
let print_put_outputs fmt ol =
let po fmt o =
- match o.var_type.Types.tdesc with
+ match (Types.repr o.var_type).Types.tdesc with
| Types.Tint -> fprintf fmt "_put_int(\"%s\", %s)" o.var_id o.var_id
| Types.Tbool -> fprintf fmt "_put_bool(\"%s\", %s)" o.var_id o.var_id
| Types.Treal -> fprintf fmt "_put_double(\"%s\", %s)" o.var_id o.var_id
diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index 230339752f1e9943badcf3a7ab0e4233ad43fc13..ba897830184f13741ef9edc443d6d6313c26e44a 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/src/backends/C/c_backend_src.ml
@@ -293,6 +293,12 @@ let print_alloc_instance fmt (i, (m, static)) =
pp_machine_alloc_name (node_name m)
(Utils.fprintf_list ~sep:", " Dimension.pp_dimension) static
+let print_alloc_const fmt m =
+ let const_locals = List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals in
+ fprintf fmt "%a%t"
+ (Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) const_locals
+ (Utils.pp_final_char_if_non_empty ";@," const_locals)
+
let print_alloc_array fmt vdecl =
let base_type = Types.array_base_type vdecl.var_type in
let size_types = Types.array_type_multi_dimension vdecl.var_type in
@@ -321,7 +327,7 @@ let print_stateless_code dependencies fmt m =
fprintf fmt "@[<v 2>%a {@,%a%t@,%a%a%t%t@]@,}@.@."
print_stateless_prototype (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
(* locals *)
- (Utils.fprintf_list ~sep:";@," pp_c_decl_local_var) m.mstep.step_locals
+ (Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) m.mstep.step_locals
(Utils.pp_final_char_if_non_empty ";@," m.mstep.step_locals)
(* check assertions *)
(pp_c_checks self) m
@@ -336,7 +342,7 @@ let print_stateless_code dependencies fmt m =
fprintf fmt "@[<v 2>%a {@,%a%t@,%a%a%t%t@]@,}@.@."
print_stateless_prototype (m.mname.node_id, (m.mstep.step_inputs@gen_locals@gen_calls), m.mstep.step_outputs)
(* locals *)
- (Utils.fprintf_list ~sep:";@," pp_c_decl_local_var) base_locals
+ (Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) base_locals
(Utils.pp_final_char_if_non_empty ";" base_locals)
(* check assertions *)
(pp_c_checks self) m
@@ -346,8 +352,13 @@ let print_stateless_code dependencies fmt m =
(fun fmt -> fprintf fmt "return;")
let print_reset_code dependencies fmt m self =
- fprintf fmt "@[<v 2>%a {@,%a%treturn;@]@,}@.@."
+ let const_locals = List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals in
+ fprintf fmt "@[<v 2>%a {@,%a%t@,%a%treturn;@]@,}@.@."
(print_reset_prototype self) (m.mname.node_id, m.mstatic)
+ (* constant locals decl *)
+ (Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) const_locals
+ (Utils.pp_final_char_if_non_empty ";" const_locals)
+ (* instrs *)
(Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) m.minit
(Utils.pp_newline_if_non_empty m.minit)
@@ -359,7 +370,7 @@ let print_step_code dependencies fmt m self =
fprintf fmt "@[<v 2>%a {@,%a%t%a%t@,%a%a%t%t@]@,}@.@."
(print_step_prototype self) (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
(* locals *)
- (Utils.fprintf_list ~sep:";@," pp_c_decl_local_var) m.mstep.step_locals
+ (Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) m.mstep.step_locals
(Utils.pp_final_char_if_non_empty ";@," m.mstep.step_locals)
(* array mems *)
(Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
@@ -377,7 +388,7 @@ let print_step_code dependencies fmt m self =
fprintf fmt "@[<v 2>%a {@,%a%t@,%a%a%t%t@]@,}@.@."
(print_step_prototype self) (m.mname.node_id, (m.mstep.step_inputs@gen_locals@gen_calls), m.mstep.step_outputs)
(* locals *)
- (Utils.fprintf_list ~sep:";@," pp_c_decl_local_var) base_locals
+ (Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) base_locals
(Utils.pp_final_char_if_non_empty ";" base_locals)
(* check assertions *)
(pp_c_checks self) m
@@ -402,8 +413,9 @@ let print_machine dependencies fmt m =
(* Alloc function, only if non static mode *)
if (not !Options.static_mem) then
begin
- fprintf fmt "@[<v 2>%a {@,%a@]@,}@.@."
+ fprintf fmt "@[<v 2>%a {@,%a%a@]@,}@.@."
print_alloc_prototype (m.mname.node_id, m.mstatic)
+ print_alloc_const m
print_alloc_code m;
end;
let self = mk_self m in
@@ -435,6 +447,7 @@ let print_lib_c source_fmt basename prog machines dependencies =
fprintf source_fmt "@[<v>";
List.iter (fun c -> print_const_def source_fmt (const_of_top c)) (get_consts prog);
fprintf source_fmt "@]@.";
+
if not !Options.static_mem then
begin
fprintf source_fmt "/* External allocation function prototypes */@.";
@@ -446,6 +459,7 @@ let print_lib_c source_fmt basename prog machines dependencies =
List.iter (fun m -> fprintf source_fmt "%a;@." print_alloc_prototype (m.mname.node_id, m.mstatic)) machines;
fprintf source_fmt "@]@.";
end;
+
(* Print the struct definitions of all machines. *)
fprintf source_fmt "/* Struct definitions */@.";
fprintf source_fmt "@[<v>";
diff --git a/src/causality.ml b/src/causality.ml
index 37b2184c21949caa46d507bc40b611b3c305879c..19c429e1bc1974f530fa90b740976505f45cf971 100644
--- a/src/causality.ml
+++ b/src/causality.ml
@@ -28,7 +28,7 @@ module IdentDepGraph = Graph.Imperative.Digraph.ConcreteBidirectional (IdentModu
by duplication of some mem vars into local node vars.
Thus, cylic dependency errors may only arise between no-mem vars.
non-mem variables are:
- - inputs: not needed for causality/scheduling, needed only for detecting useless vars
+ - constants/inputs: not needed for causality/scheduling, needed only for detecting useless vars
- read mems (fake vars): same remark as above.
- outputs: decoupled from mems, if necessary
- locals
@@ -133,6 +133,9 @@ let node_input_variables nd =
let node_local_variables nd =
List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty nd.node_locals
+let node_constant_variables nd =
+ List.fold_left (fun locals v -> if v.var_dec_const then ISet.add v.var_id locals else locals) ISet.empty nd.node_locals
+
let node_output_variables nd =
List.fold_left (fun outputs v -> ISet.add v.var_id outputs) ISet.empty nd.node_outputs
@@ -533,7 +536,10 @@ let add_external_dependency outputs mems g =
let global_dependency node =
let mems = ExprDep.node_memory_variables node in
- let inputs = ExprDep.node_input_variables node in
+ let inputs =
+ ISet.union
+ (ExprDep.node_input_variables node)
+ (ExprDep.node_constant_variables node) in
let outputs = ExprDep.node_output_variables node in
let node_vars = ExprDep.node_variables node in
let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs node_vars node in
diff --git a/src/clock_calculus.ml b/src/clock_calculus.ml
index 6f64ee073b95fecc77e5ee47fdf6b3b28f2cefa8..ee201a880f60b37691cf4e0f8e6ec1566000628b 100755
--- a/src/clock_calculus.ml
+++ b/src/clock_calculus.ml
@@ -779,7 +779,15 @@ let clock_var_decl scoped env vdecl =
if Types.get_clock_base_type vdecl.var_type <> None
then new_ck (Ccarrying ((new_carrier Carry_name scoped),ck)) scoped
else ck in
- vdecl.var_clock <- ck;
+ (if vdecl.var_dec_const
+ then match vdecl.var_dec_value with
+ | None -> ()
+ | Some v ->
+ begin
+ let ck_static = clock_expr env v in
+ try_unify ck ck_static v.expr_loc
+ end);
+ try_unify ck vdecl.var_clock vdecl.var_loc;
Env.add_value env vdecl.var_id ck
(* Clocks a variable declaration list *)
diff --git a/src/clock_predef.ml b/src/clock_predef.ml
index 24669fd2f2f653b5e059d9a1c629aaa424136c55..a2cd3fedaadcb5333e3cb8f885b3b2e7b1853ce6 100644
--- a/src/clock_predef.ml
+++ b/src/clock_predef.ml
@@ -42,6 +42,8 @@ let ck_clock_to_bool =
let cuniv = new_carrier Carry_var false in
new_ck (Carrow (new_ck (Ccarrying (cuniv, univ)) false, univ))
+let ck_carrier id ck =
+ new_ck (Ccarrying (new_carrier (Carry_const id) true, ck)) true
(* Local Variables: *)
(* compile-command:"make -C .." *)
(* End: *)
diff --git a/src/compiler_common.ml b/src/compiler_common.ml
index e00a0c0ba4bf588240262c203b977b10437593e7..f375d06a707913c8bf92272e6a9b2aaf7a7d9922 100644
--- a/src/compiler_common.ml
+++ b/src/compiler_common.ml
@@ -73,7 +73,7 @@ let parse_source source_name =
Parse.report_error err;
raise exc
| Corelang.Error (loc, err) as exc ->
- eprintf "Parsing error %a%a@."
+ eprintf "Parsing error: %a%a@."
Corelang.pp_error err
Location.pp_loc loc;
raise exc
@@ -83,7 +83,7 @@ let check_stateless_decls decls =
try
Stateless.check_prog decls
with (Stateless.Error (loc, err)) as exc ->
- eprintf "Stateless status error %a%a@."
+ eprintf "Stateless status error: %a%a@."
Stateless.pp_error err
Location.pp_loc loc;
raise exc
@@ -95,7 +95,7 @@ let type_decls env decls =
try
Typing.type_prog env decls
with (Types.Error (loc,err)) as exc ->
- eprintf "Typing error %a%a@."
+ eprintf "Typing error: %a%a@."
Types.pp_error err
Location.pp_loc loc;
raise exc
@@ -112,7 +112,7 @@ let clock_decls env decls =
try
Clock_calculus.clock_prog env decls
with (Clocks.Error (loc,err)) as exc ->
- eprintf "Clock calculus error %a%a@." Clocks.pp_error err Location.pp_loc loc;
+ eprintf "Clock calculus error: %a%a@." Clocks.pp_error err Location.pp_loc loc;
raise exc
end
in
diff --git a/src/corelang.ml b/src/corelang.ml
index 973f44decd5728b7bde260434d8c38e6ad8d55e5..9e39aac391d66dc5154820cc33aa252b1ffd3878 100755
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -41,12 +41,14 @@ let mktyp loc d =
let mkclock loc d =
{ ck_dec_desc = d; ck_dec_loc = loc }
-let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const) =
+let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const, value) =
+ assert (value = None || is_const);
{ var_id = id;
var_orig = orig;
var_dec_type = ty_dec;
var_dec_clock = ck_dec;
var_dec_const = is_const;
+ var_dec_value = value;
var_type = Types.new_var ();
var_clock = Clocks.new_var true;
var_loc = loc }
@@ -66,6 +68,7 @@ let var_decl_of_const c =
var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any };
var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any };
var_dec_const = true;
+ var_dec_value = None;
var_type = c.const_type;
var_clock = Clocks.new_var false;
var_loc = c.const_loc }
@@ -93,6 +96,10 @@ let mktop_decl loc own itf d =
let mkpredef_call loc funname args =
mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None))
+let is_clock_dec_type cty =
+ match cty with
+ | Tydec_clock _ -> true
+ | _ -> false
let const_of_top top_decl =
match top_decl.top_decl_desc with
@@ -578,6 +585,983 @@ let get_node_interface nd =
(************************************************************************)
(* Renaming *)
+let rec rename_static rename cty =
+ match cty with
+ | Tydec_array (d, cty') -> Tydec_array (Dimension.expr_replace_expr rename d, rename_static rename cty')
+ | Tydec_clock cty -> Tydec_clock (rename_static rename cty)
+ | Tydec_struct fl -> Tydec_struct (List.map (fun (f, cty) -> f, rename_static rename cty) fl)
+ | _ -> cty
+
+let rec rename_carrier rename cck =
+ match cck with
+ | Ckdec_bool cl -> Ckdec_bool (List.map (fun (c, l) -> rename c, l) cl)
+ | _ -> cck
+
+(*Format.eprintf "Types.rename_static %a = %a@." print_ty ty print_ty res; res*)
+
+(* applies the renaming function [fvar] to all variables of expression [expr] *)
+ let rec expr_replace_var fvar expr =
+ { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc }
+
+ and expr_desc_replace_var fvar expr_desc =
+ match expr_desc with
+ | Expr_const _ -> expr_desc
+ | Expr_ident i -> Expr_ident (fvar i)
+ | Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el)
+ | Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d)
+ | Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d)
+ | Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el)
+ | Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e)
+ | Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2)
+ | Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2)
+ | Expr_pre e' -> Expr_pre (expr_replace_var fvar e')
+ | Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l)
+ | Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl)
+ | Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (expr_replace_var fvar) i')
+
+(* Applies the renaming function [fvar] to every rhs
+ only when the corresponding lhs satisfies predicate [pvar] *)
+ let eq_replace_rhs_var pvar fvar eq =
+ let pvar l = List.exists pvar l in
+ let rec replace lhs rhs =
+ { rhs with expr_desc = replace_desc lhs rhs.expr_desc }
+ and replace_desc lhs rhs_desc =
+ match lhs with
+ | [] -> assert false
+ | [_] -> if pvar lhs then expr_desc_replace_var fvar rhs_desc else rhs_desc
+ | _ ->
+ (match rhs_desc with
+ | Expr_tuple tl ->
+ Expr_tuple (List.map2 (fun v e -> replace [v] e) lhs tl)
+ | Expr_appl (f, arg, None) when Basic_library.is_internal_fun f ->
+ let args = expr_list_of_expr arg in
+ Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None)
+ | Expr_array _
+ | Expr_access _
+ | Expr_power _
+ | Expr_const _
+ | Expr_ident _
+ | Expr_appl _ ->
+ if pvar lhs
+ then expr_desc_replace_var fvar rhs_desc
+ else rhs_desc
+ | Expr_ite (c, t, e) -> Expr_ite (replace lhs c, replace lhs t, replace lhs e)
+ | Expr_arrow (e1, e2) -> Expr_arrow (replace lhs e1, replace lhs e2)
+ | Expr_fby (e1, e2) -> Expr_fby (replace lhs e1, replace lhs e2)
+ | Expr_pre e' -> Expr_pre (replace lhs e')
+ | Expr_when (e', i, l) -> let i' = if pvar lhs then fvar i else i
+ in Expr_when (replace lhs e', i', l)
+ | Expr_merge (i, hl) -> let i' = if pvar lhs then fvar i else i
+ in Expr_merge (i', List.map (fun (t, h) -> (t, replace lhs h)) hl)
+ )
+ in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs }
+
+
+ let rec rename_expr f_node f_var f_const expr =
+ { expr with expr_desc = rename_expr_desc f_node f_var f_const expr.expr_desc }
+ and rename_expr_desc f_node f_var f_const expr_desc =
+ let re = rename_expr f_node f_var f_const in
+ match expr_desc with
+ | Expr_const _ -> expr_desc
+ | Expr_ident i -> Expr_ident (f_var i)
+ | Expr_array el -> Expr_array (List.map re el)
+ | Expr_access (e1, d) -> Expr_access (re e1, d)
+ | Expr_power (e1, d) -> Expr_power (re e1, d)
+ | Expr_tuple el -> Expr_tuple (List.map re el)
+ | Expr_ite (c, t, e) -> Expr_ite (re c, re t, re e)
+ | Expr_arrow (e1, e2)-> Expr_arrow (re e1, re e2)
+ | Expr_fby (e1, e2) -> Expr_fby (re e1, re e2)
+ | Expr_pre e' -> Expr_pre (re e')
+ | Expr_when (e', i, l)-> Expr_when (re e', f_var i, l)
+ | Expr_merge (i, hl) ->
+ Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl)
+ | Expr_appl (i, e', i') ->
+ Expr_appl (f_node i, re e', Utils.option_map re i')
+
+ let rename_node_annot f_node f_var f_const expr =
+ expr
+ (* TODO assert false *)
+
+ let rename_expr_annot f_node f_var f_const annot =
+ annot
+ (* TODO assert false *)
+
+let rename_node f_node f_var f_const nd =
+ let rename_var v = { v with var_id = f_var v.var_id } in
+ let rename_eq eq = { eq with
+ eq_lhs = List.map f_var eq.eq_lhs;
+ eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs
+ }
+ in
+ let inputs = List.map rename_var nd.node_inputs in
+ let outputs = List.map rename_var nd.node_outputs in
+ let locals = List.map rename_var nd.node_locals in
+ let gen_calls = List.map (rename_expr f_node f_var f_const) nd.node_gencalls in
+ let node_checks = List.map (Dimension.expr_replace_var f_var) nd.node_checks in
+ let node_asserts = List.map
+ (fun a ->
+ {a with assert_expr =
+ let expr = a.assert_expr in
+ rename_expr f_node f_var f_const expr})
+ nd.node_asserts
+ in
+ let node_stmts = List.map (fun eq -> Eq (rename_eq eq)) (get_node_eqs nd) in
+ let spec =
+ Utils.option_map
+ (fun s -> rename_node_annot f_node f_var f_const s)
+ nd.node_spec
+ in
+ let annot =
+ List.map
+ (fun s -> rename_expr_annot f_node f_var f_const s)
+ nd.node_annot
+ in
+ {
+ node_id = f_node nd.node_id;
+ node_type = nd.node_type;
+ node_clock = nd.node_clock;
+ node_inputs = inputs;
+ node_outputs = outputs;
+ node_locals = locals;
+ node_gencalls = gen_calls;
+ node_checks = node_checks;
+ node_asserts = node_asserts;
+ node_stmts = node_stmts;
+ node_dec_stateless = nd.node_dec_stateless;
+ node_stateless = nd.node_stateless;
+ node_spec = spec;
+ node_annot = annot;
+ }
+
+
+let rename_const f_const c =
+ { c with const_id = f_const c.const_id }
+
+let rename_typedef f_var t =
+ match t.tydef_desc with
+ | Tydec_enum tags -> { t with tydef_desc = Tydec_enum (List.map f_var tags) }
+ | _ -> t
+
+let rename_prog f_node f_var f_const prog =
+ List.rev (
+ List.fold_left (fun accu top ->
+ (match top.top_decl_desc with
+ | Node nd ->
+ { top with top_decl_desc = Node (rename_node f_node f_var f_const nd) }
+ | Const c ->
+ { top with top_decl_desc = Const (rename_const f_const c) }
+ | TypeDef tdef ->
+ { top with top_decl_desc = TypeDef (rename_typedef f_var tdef) }
+ | ImportedNode _
+ | Open _ -> top)
+ ::accu
+) [] prog
+ )
+
+(**********************************************************************)
+(* Pretty printers *)
+
+let pp_decl_type fmt tdecl =
+ match tdecl.top_decl_desc with
+ | Node nd ->
+ fprintf fmt "%s: " nd.node_id;
+ Utils.reset_names ();
+ fprintf fmt "%a@ " Types.print_ty nd.node_type
+ | ImportedNode ind ->
+ fprintf fmt "%s: " ind.nodei_id;
+ Utils.reset_names ();
+ fprintf fmt "%a@ " Types.print_ty ind.nodei_type
+ | Const _ | Open _ | TypeDef _ -> ()
+
+let pp_prog_type fmt tdecl_list =
+ Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list
+
+let pp_decl_clock fmt cdecl =
+ match cdecl.top_decl_desc with
+ | Node nd ->
+ fprintf fmt "%s: " nd.node_id;
+ Utils.reset_names ();
+ fprintf fmt "%a@ " Clocks.print_ck nd.node_clock
+ | ImportedNode ind ->
+ fprintf fmt "%s: " ind.nodei_id;
+ Utils.reset_names ();
+ fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock
+ | Const _ | Open _ | TypeDef _ -> ()
+
+let pp_prog_clock fmt prog =
+ Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog
+
+let pp_error fmt = function
+ Main_not_found ->
+ fprintf fmt "Cannot compile node %s: could not find the node definition.@."
+ !Options.main_node
+ | Main_wrong_kind ->
+ fprintf fmt
+ "Name %s does not correspond to a (non-imported) node definition.@."
+ !Options.main_node
+ | No_main_specified ->
+ fprintf fmt "No main node specified@."
+ | Unbound_symbol sym ->
+ fprintf fmt
+ "%s is undefined.@."
+ sym
+ | Already_bound_symbol sym ->
+ fprintf fmt
+ "%s is already defined.@."
+ sym
+ | Unknown_library sym ->
+ fprintf fmt
+ "impossible to load library %s.lusic@.Please compile the corresponding interface or source file.@."
+ sym
+ | Wrong_number sym ->
+ fprintf fmt
+ "library %s.lusic has a different version number and may crash compiler@.Please recompile the corresponding interface or source file.@."
+ sym
+
+(* filling node table with internal functions *)
+let vdecls_of_typ_ck cpt ty =
+ let loc = Location.dummy_loc in
+ List.map
+ (fun _ -> incr cpt;
+ let name = sprintf "_var_%d" !cpt in
+ mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false, None))
+ (Types.type_list_of_type ty)
+
+let mk_internal_node id =
+ let spec = None in
+ let ty = Env.lookup_value Basic_library.type_env id in
+ let ck = Env.lookup_value Basic_library.clock_env id in
+ let (tin, tout) = Types.split_arrow ty in
+ (*eprintf "internal fun %s: %d -> %d@." id (List.length (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*)
+ let cpt = ref (-1) in
+ mktop
+ (ImportedNode
+ {nodei_id = id;
+ nodei_type = ty;
+ nodei_clock = ck;
+ nodei_inputs = vdecls_of_typ_ck cpt tin;
+ nodei_outputs = vdecls_of_typ_ck cpt tout;
+ nodei_stateless = Types.get_static_value ty <> None;
+ nodei_spec = spec;
+ nodei_prototype = None;
+ nodei_in_lib = None;
+ })
+
+let add_internal_funs () =
+ List.iter
+ (fun id -> let nd = mk_internal_node id in Hashtbl.add node_table id nd)
+ Basic_library.internal_funs
+
+
+
+(* Replace any occurence of a var in vars_to_replace by its associated
+ expression in defs until e does not contain any such variables *)
+let rec substitute_expr vars_to_replace defs e =
+ let se = substitute_expr vars_to_replace defs in
+ { e with expr_desc =
+ let ed = e.expr_desc in
+ match ed with
+ | Expr_const _ -> ed
+ | Expr_array el -> Expr_array (List.map se el)
+ | Expr_access (e1, d) -> Expr_access (se e1, d)
+ | Expr_power (e1, d) -> Expr_power (se e1, d)
+ | Expr_tuple el -> Expr_tuple (List.map se el)
+ | Expr_ite (c, t, e) -> Expr_ite (se c, se t, se e)
+ | Expr_arrow (e1, e2)-> Expr_arrow (se e1, se e2)
+ | Expr_fby (e1, e2) -> Expr_fby (se e1, se e2)
+ | Expr_pre e' -> Expr_pre (se e')
+ | Expr_when (e', i, l)-> Expr_when (se e', i, l)
+ | Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, se h)) hl)
+ | Expr_appl (i, e', i') -> Expr_appl (i, se e', i')
+ | Expr_ident i ->
+ if List.exists (fun v -> v.var_id = i) vars_to_replace then (
+ let eq_i eq = eq.eq_lhs = [i] in
+ if List.exists eq_i defs then
+ let sub = List.find eq_i defs in
+ let sub' = se sub.eq_rhs in
+ sub'.expr_desc
+ else
+ assert false
+ )
+ else
+ ed
+
+ }
+(* FAUT IL RETIRER ?
+
+ let rec expr_to_eexpr expr =
+ { eexpr_tag = expr.expr_tag;
+ eexpr_desc = expr_desc_to_eexpr_desc expr.expr_desc;
+ eexpr_type = expr.expr_type;
+ eexpr_clock = expr.expr_clock;
+ eexpr_loc = expr.expr_loc
+ }
+ and expr_desc_to_eexpr_desc expr_desc =
+ let conv = expr_to_eexpr in
+ match expr_desc with
+ | Expr_const c -> EExpr_const (match c with
+ | Const_int x -> EConst_int x
+ | Const_real x -> EConst_real x
+ | Const_float x -> EConst_float x
+ | Const_tag x -> EConst_tag x
+ | _ -> assert false
+
+ )
+ | Expr_ident i -> EExpr_ident i
+ | Expr_tuple el -> EExpr_tuple (List.map conv el)
+
+ | Expr_arrow (e1, e2)-> EExpr_arrow (conv e1, conv e2)
+ | Expr_fby (e1, e2) -> EExpr_fby (conv e1, conv e2)
+ | Expr_pre e' -> EExpr_pre (conv e')
+ | Expr_appl (i, e', i') ->
+ EExpr_appl
+ (i, conv e', match i' with None -> None | Some(id, _) -> Some id)
+
+ | Expr_when _
+ | Expr_merge _ -> assert false
+ | Expr_array _
+ | Expr_access _
+ | Expr_power _ -> assert false
+ | Expr_ite (c, t, e) -> assert false
+ | _ -> assert false
+
+ *)
+let rec get_expr_calls nodes e =
+ get_calls_expr_desc nodes e.expr_desc
+and get_calls_expr_desc nodes expr_desc =
+ let get_calls = get_expr_calls nodes in
+ match expr_desc with
+ | Expr_const _
+ | Expr_ident _ -> Utils.ISet.empty
+ | Expr_tuple el
+ | Expr_array el -> List.fold_left (fun accu e -> Utils.ISet.union accu (get_calls e)) Utils.ISet.empty el
+ | Expr_pre e1
+ | Expr_when (e1, _, _)
+ | Expr_access (e1, _)
+ | Expr_power (e1, _) -> get_calls e1
+ | Expr_ite (c, t, e) -> Utils.ISet.union (Utils.ISet.union (get_calls c) (get_calls t)) (get_calls e)
+ | Expr_arrow (e1, e2)
+ | Expr_fby (e1, e2) -> Utils.ISet.union (get_calls e1) (get_calls e2)
+ | Expr_merge (_, hl) -> List.fold_left (fun accu (_, h) -> Utils.ISet.union accu (get_calls h)) Utils.ISet.empty hl
+ | Expr_appl (i, e', i') ->
+ if Basic_library.is_internal_fun i then
+ (get_calls e')
+ else
+ let calls = Utils.ISet.add i (get_calls e') in
+ let test = (fun n -> match n.top_decl_desc with Node nd -> nd.node_id = i | _ -> false) in
+ if List.exists test nodes then
+ match (List.find test nodes).top_decl_desc with
+ | Node nd -> Utils.ISet.union (get_node_calls nodes nd) calls
+ | _ -> assert false
+ else
+ calls
+
+and get_eq_calls nodes eq =
+ get_expr_calls nodes eq.eq_rhs
+and get_node_calls nodes node =
+ List.fold_left (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu) Utils.ISet.empty (get_node_eqs node)
+
+let rec get_expr_vars vars e =
+ get_expr_desc_vars vars e.expr_desc
+and get_expr_desc_vars vars expr_desc =
+ match expr_desc with
+ | Expr_const _ -> vars
+ | Expr_ident x -> Utils.ISet.add x vars
+ | Expr_tuple el
+ | Expr_array el -> List.fold_left get_expr_vars vars el
+ | Expr_pre e1 -> get_expr_vars vars e1
+ | Expr_when (e1, c, _) -> get_expr_vars (Utils.ISet.add c vars) e1
+ | Expr_access (e1, d)
+ | Expr_power (e1, d) -> List.fold_left get_expr_vars vars [e1; expr_of_dimension d]
+ | Expr_ite (c, t, e) -> List.fold_left get_expr_vars vars [c; t; e]
+ | Expr_arrow (e1, e2)
+ | Expr_fby (e1, e2) -> List.fold_left get_expr_vars vars [e1; e2]
+ | Expr_merge (c, hl) -> List.fold_left (fun vars (_, h) -> get_expr_vars vars h) (Utils.ISet.add c vars) hl
+ | Expr_appl (_, arg, None) -> get_expr_vars vars arg
+ | Expr_appl (_, arg, Some r) -> List.fold_left get_expr_vars vars [arg; r]
+
+
+let rec expr_has_arrows e =
+ expr_desc_has_arrows e.expr_desc
+and expr_desc_has_arrows expr_desc =
+ match expr_desc with
+ | Expr_const _
+ | Expr_ident _ -> false
+ | Expr_tuple el
+ | Expr_array el -> List.exists expr_has_arrows el
+ | Expr_pre e1
+ | Expr_when (e1, _, _)
+ | Expr_access (e1, _)
+ | Expr_power (e1, _) -> expr_has_arrows e1
+ | Expr_ite (c, t, e) -> List.exists expr_has_arrows [c; t; e]
+ | Expr_arrow (e1, e2)
+ | Expr_fby (e1, e2) -> true
+ | Expr_merge (_, hl) -> List.exists (fun (_, h) -> expr_has_arrows h) hl
+ | Expr_appl (i, e', i') -> expr_has_arrows e'
+
+and eq_has_arrows eq =
+ expr_has_arrows eq.eq_rhs
+and node_has_arrows node =
+ List.exists (fun eq -> eq_has_arrows eq) (get_node_eqs node)
+
+let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const, value) =
+ assert (value = None || is_const);
+ { var_id = id;
+ var_orig = orig;
+ var_dec_type = ty_dec;
+ var_dec_clock = ck_dec;
+ var_dec_const = is_const;
+ var_dec_value = value;
+ var_type = Types.new_var ();
+ var_clock = Clocks.new_var true;
+ var_loc = loc }
+
+let mkexpr loc d =
+ { expr_tag = Utils.new_tag ();
+ expr_desc = d;
+ expr_type = Types.new_var ();
+ expr_clock = Clocks.new_var true;
+ expr_delay = Delay.new_var ();
+ expr_annot = None;
+ expr_loc = loc }
+
+let var_decl_of_const c =
+ { var_id = c.const_id;
+ var_orig = true;
+ var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any };
+ var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any };
+ var_dec_const = true;
+ var_dec_value = None;
+ var_type = c.const_type;
+ var_clock = Clocks.new_var false;
+ var_loc = c.const_loc }
+
+let mk_new_name used id =
+ let rec new_name name cpt =
+ if used name
+ then new_name (sprintf "_%s_%i" id cpt) (cpt+1)
+ else name
+ in new_name id 1
+
+let mkeq loc (lhs, rhs) =
+ { eq_lhs = lhs;
+ eq_rhs = rhs;
+ eq_loc = loc }
+
+let mkassert loc expr =
+ { assert_loc = loc;
+ assert_expr = expr
+ }
+
+let mktop_decl loc own itf d =
+ { top_decl_desc = d; top_decl_loc = loc; top_decl_owner = own; top_decl_itf = itf }
+
+let mkpredef_call loc funname args =
+ mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None))
+
+let is_clock_dec_type cty =
+ match cty with
+ | Tydec_clock _ -> true
+ | _ -> false
+
+let const_of_top top_decl =
+ match top_decl.top_decl_desc with
+ | Const c -> c
+ | _ -> assert false
+
+let node_of_top top_decl =
+ match top_decl.top_decl_desc with
+ | Node nd -> nd
+ | _ -> assert false
+
+let imported_node_of_top top_decl =
+ match top_decl.top_decl_desc with
+ | ImportedNode ind -> ind
+ | _ -> assert false
+
+let typedef_of_top top_decl =
+ match top_decl.top_decl_desc with
+ | TypeDef tdef -> tdef
+ | _ -> assert false
+
+let dependency_of_top top_decl =
+ match top_decl.top_decl_desc with
+ | Open (local, dep) -> (local, dep)
+ | _ -> assert false
+
+let consts_of_enum_type top_decl =
+ match top_decl.top_decl_desc with
+ | TypeDef tdef ->
+ (match tdef.tydef_desc with
+ | Tydec_enum tags -> List.map (fun tag -> let cdecl = { const_id = tag; const_loc = top_decl.top_decl_loc; const_value = Const_tag tag; const_type = Type_predef.type_const tdef.tydef_id } in { top_decl with top_decl_desc = Const cdecl }) tags
+ | _ -> [])
+ | _ -> assert false
+
+(************************************************************)
+(* Eexpr functions *)
+(************************************************************)
+
+let merge_node_annot ann1 ann2 =
+ { requires = ann1.requires @ ann2.requires;
+ ensures = ann1.ensures @ ann2.ensures;
+ behaviors = ann1.behaviors @ ann2.behaviors;
+ spec_loc = ann1.spec_loc
+ }
+
+let mkeexpr loc expr =
+ { eexpr_tag = Utils.new_tag ();
+ eexpr_qfexpr = 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 }
+
+(*
+let mkepredef_call loc funname args =
+ mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None))
+
+let mkepredef_unary_call loc funname arg =
+ mkeexpr loc (EExpr_appl (funname, arg, None))
+*)
+
+let merge_expr_annot ann1 ann2 =
+ match ann1, ann2 with
+ | None, None -> assert false
+ | Some _, None -> ann1
+ | None, Some _ -> ann2
+ | Some ann1, Some ann2 -> Some {
+ annots = ann1.annots @ ann2.annots;
+ annot_loc = ann1.annot_loc
+ }
+
+let update_expr_annot node_id e annot =
+ List.iter (fun (key, _) ->
+ Annotations.add_expr_ann node_id e.expr_tag key
+ ) annot.annots;
+ { e with expr_annot = merge_expr_annot e.expr_annot (Some annot) }
+
+
+(***********************************************************)
+(* Fast access to nodes, by name *)
+let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30
+let consts_table = Hashtbl.create 30
+
+let print_node_table fmt () =
+ begin
+ Format.fprintf fmt "{ /* node table */@.";
+ Hashtbl.iter (fun id nd ->
+ Format.fprintf fmt "%s |-> %a"
+ id
+ Printers.pp_short_decl nd
+ ) node_table;
+ Format.fprintf fmt "}@."
+ end
+
+let print_consts_table fmt () =
+ begin
+ Format.fprintf fmt "{ /* consts table */@.";
+ Hashtbl.iter (fun id const ->
+ Format.fprintf fmt "%s |-> %a"
+ id
+ Printers.pp_const_decl (const_of_top const)
+ ) consts_table;
+ Format.fprintf fmt "}@."
+ end
+
+let node_name td =
+ match td.top_decl_desc with
+ | Node nd -> nd.node_id
+ | ImportedNode nd -> nd.nodei_id
+ | _ -> assert false
+
+let is_generic_node td =
+ match td.top_decl_desc with
+ | Node nd -> List.exists (fun v -> v.var_dec_const) nd.node_inputs
+ | ImportedNode nd -> List.exists (fun v -> v.var_dec_const) nd.nodei_inputs
+ | _ -> assert false
+
+let node_inputs td =
+ match td.top_decl_desc with
+ | Node nd -> nd.node_inputs
+ | ImportedNode nd -> nd.nodei_inputs
+ | _ -> assert false
+
+let node_from_name id =
+ try
+ Hashtbl.find node_table id
+ with Not_found -> (Format.eprintf "Unable to find any node named %s@ @?" id;
+ assert false)
+
+let is_imported_node td =
+ match td.top_decl_desc with
+ | Node nd -> false
+ | ImportedNode nd -> true
+ | _ -> assert false
+
+
+(* alias and type definition table *)
+
+let mktop = mktop_decl Location.dummy_loc Version.include_path false
+
+let top_int_type = mktop (TypeDef {tydef_id = "int"; tydef_desc = Tydec_int})
+let top_bool_type = mktop (TypeDef {tydef_id = "bool"; tydef_desc = Tydec_bool})
+let top_float_type = mktop (TypeDef {tydef_id = "float"; tydef_desc = Tydec_float})
+let top_real_type = mktop (TypeDef {tydef_id = "real"; tydef_desc = Tydec_real})
+
+let type_table =
+ Utils.create_hashtable 20 [
+ Tydec_int , top_int_type;
+ Tydec_bool , top_bool_type;
+ Tydec_float, top_float_type;
+ Tydec_real , top_real_type
+ ]
+
+let print_type_table fmt () =
+ begin
+ Format.fprintf fmt "{ /* type table */@.";
+ Hashtbl.iter (fun tydec tdef ->
+ Format.fprintf fmt "%a |-> %a"
+ Printers.pp_var_type_dec_desc tydec
+ Printers.pp_typedef (typedef_of_top tdef)
+ ) type_table;
+ Format.fprintf fmt "}@."
+ end
+
+let rec is_user_type typ =
+ match typ with
+ | Tydec_int | Tydec_bool | Tydec_real
+ | Tydec_float | Tydec_any | Tydec_const _ -> false
+ | Tydec_clock typ' -> is_user_type typ'
+ | _ -> true
+
+let get_repr_type typ =
+ let typ_def = (typedef_of_top (Hashtbl.find type_table typ)).tydef_desc in
+ if is_user_type typ_def then typ else typ_def
+
+let rec coretype_equal ty1 ty2 =
+ let res =
+ match ty1, ty2 with
+ | Tydec_any , _
+ | _ , Tydec_any -> assert false
+ | Tydec_const _ , Tydec_const _ -> get_repr_type ty1 = get_repr_type ty2
+ | Tydec_const _ , _ -> let ty1' = (typedef_of_top (Hashtbl.find type_table ty1)).tydef_desc
+ in (not (is_user_type ty1')) && coretype_equal ty1' ty2
+ | _ , Tydec_const _ -> coretype_equal ty2 ty1
+ | Tydec_int , Tydec_int
+ | Tydec_real , Tydec_real
+ | Tydec_float , Tydec_float
+ | Tydec_bool , Tydec_bool -> true
+ | Tydec_clock ty1 , Tydec_clock ty2 -> coretype_equal ty1 ty2
+ | Tydec_array (d1,ty1), Tydec_array (d2, ty2) -> Dimension.is_eq_dimension d1 d2 && coretype_equal ty1 ty2
+ | Tydec_enum tl1 , Tydec_enum tl2 -> List.sort compare tl1 = List.sort compare tl2
+ | Tydec_struct fl1 , Tydec_struct fl2 ->
+ List.length fl1 = List.length fl2
+ && List.for_all2 (fun (f1, t1) (f2, t2) -> f1 = f2 && coretype_equal t1 t2)
+ (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl1)
+ (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl2)
+ | _ -> false
+ in ((*Format.eprintf "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc ty1 Printers.pp_var_type_dec_desc ty2 res;*) res)
+
+let tag_true = "true"
+let tag_false = "false"
+let tag_default = "default"
+
+let const_is_bool c =
+ match c with
+ | Const_tag t -> t = tag_true || t = tag_false
+ | _ -> false
+
+(* Computes the negation of a boolean constant *)
+let const_negation c =
+ assert (const_is_bool c);
+ match c with
+ | Const_tag t when t = tag_true -> Const_tag tag_false
+ | _ -> Const_tag tag_true
+
+let const_or c1 c2 =
+ assert (const_is_bool c1 && const_is_bool c2);
+ match c1, c2 with
+ | Const_tag t1, _ when t1 = tag_true -> c1
+ | _ , Const_tag t2 when t2 = tag_true -> c2
+ | _ -> Const_tag tag_false
+
+let const_and c1 c2 =
+ assert (const_is_bool c1 && const_is_bool c2);
+ match c1, c2 with
+ | Const_tag t1, _ when t1 = tag_false -> c1
+ | _ , Const_tag t2 when t2 = tag_false -> c2
+ | _ -> Const_tag tag_true
+
+let const_xor c1 c2 =
+ assert (const_is_bool c1 && const_is_bool c2);
+ match c1, c2 with
+ | Const_tag t1, Const_tag t2 when t1 <> t2 -> Const_tag tag_true
+ | _ -> Const_tag tag_false
+
+let const_impl c1 c2 =
+ assert (const_is_bool c1 && const_is_bool c2);
+ match c1, c2 with
+ | Const_tag t1, _ when t1 = tag_false -> Const_tag tag_true
+ | _ , Const_tag t2 when t2 = tag_true -> Const_tag tag_true
+ | _ -> Const_tag tag_false
+
+(* To guarantee uniqueness of tags in enum types *)
+let tag_table =
+ Utils.create_hashtable 20 [
+ tag_true, top_bool_type;
+ tag_false, top_bool_type
+ ]
+
+(* To guarantee uniqueness of fields in struct types *)
+let field_table =
+ Utils.create_hashtable 20 [
+ ]
+
+let get_enum_type_tags cty =
+(*Format.eprintf "get_enum_type_tags %a@." Printers.pp_var_type_dec_desc cty;*)
+ match cty with
+ | Tydec_bool -> [tag_true; tag_false]
+ | Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with
+ | Tydec_enum tl -> tl
+ | _ -> assert false)
+ | _ -> assert false
+
+let get_struct_type_fields cty =
+ match cty with
+ | Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with
+ | Tydec_struct fl -> fl
+ | _ -> assert false)
+ | _ -> assert false
+
+let const_of_bool b =
+ Const_tag (if b then tag_true else tag_false)
+
+(* let get_const c = snd (Hashtbl.find consts_table c) *)
+
+let ident_of_expr expr =
+ match expr.expr_desc with
+ | Expr_ident id -> id
+ | _ -> assert false
+
+(* Generate a new ident expression from a declared variable *)
+let expr_of_vdecl v =
+ { expr_tag = Utils.new_tag ();
+ expr_desc = Expr_ident v.var_id;
+ expr_type = v.var_type;
+ expr_clock = v.var_clock;
+ expr_delay = Delay.new_var ();
+ expr_annot = None;
+ expr_loc = v.var_loc }
+
+(* Caution, returns an untyped and unclocked expression *)
+let expr_of_ident id loc =
+ {expr_tag = Utils.new_tag ();
+ expr_desc = Expr_ident id;
+ expr_type = Types.new_var ();
+ expr_clock = Clocks.new_var true;
+ expr_delay = Delay.new_var ();
+ expr_loc = loc;
+ expr_annot = None}
+
+let is_tuple_expr expr =
+ match expr.expr_desc with
+ | Expr_tuple _ -> true
+ | _ -> false
+
+let expr_list_of_expr expr =
+ match expr.expr_desc with
+ | Expr_tuple elist -> elist
+ | _ -> [expr]
+
+let expr_of_expr_list loc elist =
+ match elist with
+ | [t] -> { t with expr_loc = loc }
+ | t::_ ->
+ let tlist = List.map (fun e -> e.expr_type) elist in
+ let clist = List.map (fun e -> e.expr_clock) elist in
+ { t with expr_desc = Expr_tuple elist;
+ expr_type = Type_predef.type_tuple tlist;
+ expr_clock = Clock_predef.ck_tuple clist;
+ expr_tag = Utils.new_tag ();
+ expr_loc = loc }
+ | _ -> assert false
+
+let call_of_expr expr =
+ match expr.expr_desc with
+ | Expr_appl (f, args, r) -> (f, expr_list_of_expr args, r)
+ | _ -> assert false
+
+(* Conversion from dimension expr to standard expr, for the purpose of printing, typing, etc... *)
+let rec expr_of_dimension dim =
+ match dim.dim_desc with
+ | Dbool b ->
+ mkexpr dim.dim_loc (Expr_const (const_of_bool b))
+ | Dint i ->
+ mkexpr dim.dim_loc (Expr_const (Const_int i))
+ | Dident id ->
+ mkexpr dim.dim_loc (Expr_ident id)
+ | Dite (c, t, e) ->
+ mkexpr dim.dim_loc (Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e))
+ | Dappl (id, args) ->
+ mkexpr dim.dim_loc (Expr_appl (id, expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args), None))
+ | Dlink dim' -> expr_of_dimension dim'
+ | Dvar
+ | Dunivar -> (Format.eprintf "internal error: Corelang.expr_of_dimension %a@." Dimension.pp_dimension dim;
+ assert false)
+
+let dimension_of_const loc const =
+ match const with
+ | Const_int i -> mkdim_int loc i
+ | Const_tag t when t = tag_true || t = tag_false -> mkdim_bool loc (t = tag_true)
+ | _ -> raise InvalidDimension
+
+(* Conversion from standard expr to dimension expr, for the purpose of injecting static call arguments
+ into dimension expressions *)
+let rec dimension_of_expr expr =
+ match expr.expr_desc with
+ | Expr_const c -> dimension_of_const expr.expr_loc c
+ | Expr_ident id -> mkdim_ident expr.expr_loc id
+ | Expr_appl (f, args, None) when Basic_library.is_internal_fun f ->
+ let k = Types.get_static_value (Env.lookup_value Basic_library.type_env f) in
+ if k = None then raise InvalidDimension;
+ mkdim_appl expr.expr_loc f (List.map dimension_of_expr (expr_list_of_expr args))
+ | Expr_ite (i, t, e) ->
+ mkdim_ite expr.expr_loc (dimension_of_expr i) (dimension_of_expr t) (dimension_of_expr e)
+ | _ -> raise InvalidDimension (* not a simple dimension expression *)
+
+
+let sort_handlers hl =
+ List.sort (fun (t, _) (t', _) -> compare t t') hl
+
+let rec is_eq_expr e1 e2 = match e1.expr_desc, e2.expr_desc with
+ | Expr_const c1, Expr_const c2 -> c1 = c2
+ | Expr_ident i1, Expr_ident i2 -> i1 = i2
+ | Expr_array el1, Expr_array el2
+ | Expr_tuple el1, Expr_tuple el2 ->
+ List.length el1 = List.length el2 && List.for_all2 is_eq_expr el1 el2
+ | Expr_arrow (e1, e2), Expr_arrow (e1', e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
+ | Expr_fby (e1,e2), Expr_fby (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
+ | Expr_ite (i1, t1, e1), Expr_ite (i2, t2, e2) -> is_eq_expr i1 i2 && is_eq_expr t1 t2 && is_eq_expr e1 e2
+ (* | Expr_concat (e1,e2), Expr_concat (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' *)
+ (* | Expr_tail e, Expr_tail e' -> is_eq_expr e e' *)
+ | Expr_pre e, Expr_pre e' -> is_eq_expr e e'
+ | Expr_when (e, i, l), Expr_when (e', i', l') -> l=l' && i=i' && is_eq_expr e e'
+ | Expr_merge(i, hl), Expr_merge(i', hl') -> i=i' && List.for_all2 (fun (t, h) (t', h') -> t=t' && is_eq_expr h h') (sort_handlers hl) (sort_handlers hl')
+ | Expr_appl (i, e, r), Expr_appl (i', e', r') -> i=i' && r=r' && is_eq_expr e e'
+ | Expr_power (e1, i1), Expr_power (e2, i2)
+ | Expr_access (e1, i1), Expr_access (e2, i2) -> is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2)
+ | _ -> false
+
+let get_node_vars nd =
+ nd.node_inputs @ nd.node_locals @ nd.node_outputs
+
+let mk_new_node_name nd id =
+ let used_vars = get_node_vars nd in
+ let used v = List.exists (fun vdecl -> vdecl.var_id = v) used_vars in
+ mk_new_name used id
+
+let get_var id var_list =
+ List.find (fun v -> v.var_id = id) var_list
+
+let get_node_var id node =
+ get_var id (get_node_vars node)
+
+let get_node_eqs =
+ let get_eqs stmts =
+ List.fold_right
+ (fun stmt res ->
+ match stmt with
+ | Eq eq -> eq :: res
+ | Aut _ -> assert false)
+ stmts
+ [] in
+ let table_eqs = Hashtbl.create 23 in
+ (fun nd ->
+ try
+ let (old, res) = Hashtbl.find table_eqs nd.node_id
+ in if old == nd.node_stmts then res else raise Not_found
+ with Not_found ->
+ let res = get_eqs nd.node_stmts in
+ begin
+ Hashtbl.replace table_eqs nd.node_id (nd.node_stmts, res);
+ res
+ end)
+
+let get_node_eq id node =
+ List.find (fun eq -> List.mem id eq.eq_lhs) (get_node_eqs node)
+
+let get_nodes prog =
+ List.fold_left (
+ fun nodes decl ->
+ match decl.top_decl_desc with
+ | Node _ -> decl::nodes
+ | Const _ | ImportedNode _ | Open _ | TypeDef _ -> nodes
+ ) [] prog
+
+let get_imported_nodes prog =
+ List.fold_left (
+ fun nodes decl ->
+ match decl.top_decl_desc with
+ | ImportedNode _ -> decl::nodes
+ | Const _ | Node _ | Open _ | TypeDef _-> nodes
+ ) [] prog
+
+let get_consts prog =
+ List.fold_right (
+ fun decl consts ->
+ match decl.top_decl_desc with
+ | Const _ -> decl::consts
+ | Node _ | ImportedNode _ | Open _ | TypeDef _ -> consts
+ ) prog []
+
+let get_typedefs prog =
+ List.fold_right (
+ fun decl types ->
+ match decl.top_decl_desc with
+ | TypeDef _ -> decl::types
+ | Node _ | ImportedNode _ | Open _ | Const _ -> types
+ ) prog []
+
+let get_dependencies prog =
+ List.fold_right (
+ fun decl deps ->
+ match decl.top_decl_desc with
+ | Open _ -> decl::deps
+ | Node _ | ImportedNode _ | TypeDef _ | Const _ -> deps
+ ) prog []
+
+let get_node_interface nd =
+ {nodei_id = nd.node_id;
+ nodei_type = nd.node_type;
+ nodei_clock = nd.node_clock;
+ nodei_inputs = nd.node_inputs;
+ nodei_outputs = nd.node_outputs;
+ nodei_stateless = nd.node_dec_stateless;
+ nodei_spec = nd.node_spec;
+ nodei_prototype = None;
+ nodei_in_lib = None;
+ }
+
+(************************************************************************)
+(* Renaming *)
+
+let rec rename_static rename cty =
+ match cty with
+ | Tydec_array (d, cty') -> Tydec_array (Dimension.expr_replace_expr rename d, rename_static rename cty')
+ | Tydec_clock cty -> Tydec_clock (rename_static rename cty)
+ | Tydec_struct fl -> Tydec_struct (List.map (fun (f, cty) -> f, rename_static rename cty) fl)
+ | _ -> cty
+
+let rec rename_carrier rename cck =
+ match cck with
+ | Ckdec_bool cl -> Ckdec_bool (List.map (fun (c, l) -> rename c, l) cl)
+ | _ -> cck
+
+(*Format.eprintf "Types.rename_static %a = %a@." print_ty ty print_ty res; res*)
+
(* applies the renaming function [fvar] to all variables of expression [expr] *)
let rec expr_replace_var fvar expr =
{ expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc }
@@ -799,7 +1783,7 @@ let vdecls_of_typ_ck cpt ty =
List.map
(fun _ -> incr cpt;
let name = sprintf "_var_%d" !cpt in
- mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false))
+ mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false, None))
(Types.type_list_of_type ty)
let mk_internal_node id =
@@ -979,6 +1963,33 @@ and eq_has_arrows eq =
and node_has_arrows node =
List.exists (fun eq -> eq_has_arrows eq) (get_node_eqs node)
+let copy_var_decl vdecl =
+ mkvar_decl vdecl.var_loc ~orig:vdecl.var_orig (vdecl.var_id, vdecl.var_dec_type, vdecl.var_dec_clock, vdecl.var_dec_const, vdecl.var_dec_value)
+
+let copy_const cdecl =
+ { cdecl with const_type = Types.new_var () }
+
+let copy_node nd =
+ { nd with
+ node_type = Types.new_var ();
+ node_clock = Clocks.new_var true;
+ node_inputs = List.map copy_var_decl nd.node_inputs;
+ node_outputs = List.map copy_var_decl nd.node_outputs;
+ node_locals = List.map copy_var_decl nd.node_locals;
+ node_gencalls = [];
+ node_checks = [];
+ node_stateless = None;
+ }
+
+let copy_top top =
+ match top.top_decl_desc with
+ | Node nd -> { top with top_decl_desc = Node (copy_node nd) }
+ | Const c -> { top with top_decl_desc = Const (copy_const c) }
+ | _ -> top
+
+let copy_prog top_list =
+ List.map copy_top top_list
+
(* Local Variables: *)
(* compile-command:"make -C .." *)
(* End: *)
diff --git a/src/corelang.mli b/src/corelang.mli
index a0eaa6cf253498016d8ad39d2c6c9861cb7850c8..d4a1d5689f2c337a4698c3f420e02f7970acd843 100755
--- a/src/corelang.mli
+++ b/src/corelang.mli
@@ -19,7 +19,8 @@ val dummy_clock_dec: clock_dec
val mktyp: Location.t -> type_dec_desc -> type_dec
val mkclock: Location.t -> clock_dec_desc -> clock_dec
-val mkvar_decl: Location.t -> ?orig:bool -> ident * type_dec * clock_dec * bool (* is const *) -> var_decl
+val mkvar_decl: Location.t -> ?orig:bool -> ident * type_dec * clock_dec * bool (* is const *) * expr option (* value *) -> var_decl
+
val var_decl_of_const: const_desc -> var_decl
val mkexpr: Location.t -> expr_desc -> expr
val mkeq: Location.t -> ident list * expr -> eq
@@ -41,6 +42,7 @@ val consts_table: (ident, top_decl) Hashtbl.t
val print_consts_table: Format.formatter -> unit -> unit
val type_table: (type_dec_desc, top_decl) Hashtbl.t
val print_type_table: Format.formatter -> unit -> unit
+val is_clock_dec_type: type_dec_desc -> bool
val get_repr_type: type_dec_desc -> type_dec_desc
val is_user_type: type_dec_desc -> bool
val coretype_equal: type_dec_desc -> type_dec_desc -> bool
@@ -111,16 +113,23 @@ val get_typedefs: program -> top_decl list
val get_dependencies : program -> top_decl list
(* val prog_unfold_consts: program -> program *)
+val rename_static: (ident -> Dimension.dim_expr) -> type_dec_desc -> type_dec_desc
+val rename_carrier: (ident -> ident) -> clock_dec_desc -> clock_dec_desc
+
val get_expr_vars: Utils.ISet.t -> expr -> Utils.ISet.t
val expr_replace_var: (ident -> ident) -> expr -> expr
val eq_replace_rhs_var: (ident -> bool) -> (ident -> ident) -> eq -> eq
(** rename_prog f_node f_var f_const prog *)
val rename_prog: (ident -> ident) -> (ident -> ident) -> (ident -> ident) -> program -> program
-
-
val substitute_expr: var_decl list -> eq list -> expr -> expr
+val copy_var_decl: var_decl -> var_decl
+val copy_const: const_desc -> const_desc
+val copy_node: node_desc -> node_desc
+val copy_top: top_decl -> top_decl
+val copy_prog: top_decl list -> top_decl list
+
(** Annotation expression related functions *)
val mkeexpr: Location.t -> expr -> eexpr
val merge_node_annot: node_annot -> node_annot -> node_annot
diff --git a/src/dimension.ml b/src/dimension.ml
index e703905ac52fce6ca6e88e5b5208e817936236f5..79d6f1f03ee904c1f07a1267f79b4053de34e3ab 100644
--- a/src/dimension.ml
+++ b/src/dimension.ml
@@ -220,7 +220,7 @@ let rec eval eval_op eval_const dim =
| Dident id ->
(match eval_const id with
| Some val_dim -> dim.dim_desc <- Dlink val_dim
- | None -> raise InvalidDimension)
+ | None -> (Format.eprintf "invalid %a@." pp_dimension dim; raise InvalidDimension))
| Dite (c, t, e) ->
begin
eval eval_op eval_const c;
@@ -243,7 +243,14 @@ let rec eval eval_op eval_const dim =
end
| Dvar -> ()
| Dunivar -> assert false
-
+(*
+in
+begin
+ Format.eprintf "Dimension.eval %a = " pp_dimension dim;
+ eval eval_op eval_const dim;
+ Format.eprintf "%a@." pp_dimension dim
+end
+*)
let uneval const univar =
let univar = repr univar in
match univar.dim_desc with
diff --git a/src/inliner.ml b/src/inliner.ml
index 29b008baef787c49cd3e3bff0c9171aa318cc37f..1a2dd1034d7042c705fcf0392db24650e23cca93 100644
--- a/src/inliner.ml
+++ b/src/inliner.ml
@@ -27,20 +27,6 @@ let check_node_name id = (fun t ->
| Node nd -> nd.node_id = id
| _ -> false)
-let get_static_inputs node args =
- List.fold_right2 (fun vdecl arg static ->
- if vdecl.var_dec_const then (vdecl.var_id, Corelang.dimension_of_expr arg) :: static else static)
- node.node_inputs
- (Corelang.expr_list_of_expr args)
- []
-
-let get_carrier_inputs node args =
- List.fold_right2 (fun vdecl arg carrier ->
- if Types.get_clock_base_type vdecl.var_type <> None then (vdecl.var_id, ident_of_expr arg) :: carrier else carrier)
- node.node_inputs
- (Corelang.expr_list_of_expr args)
- []
-
let is_node_var node v =
try
ignore (Corelang.get_node_var v node); true
@@ -53,7 +39,21 @@ let rename_eq rename eq =
eq_lhs = List.map rename eq.eq_lhs;
eq_rhs = rename_expr rename eq.eq_rhs
}
-
+(*
+let get_static_inputs input_arg_list =
+ List.fold_right (fun (vdecl, arg) res ->
+ if vdecl.var_dec_const
+ then (vdecl.var_id, Corelang.dimension_of_expr arg) :: res
+ else res)
+ input_arg_list []
+
+let get_carrier_inputs input_arg_list =
+ List.fold_right (fun (vdecl, arg) res ->
+ if Corelang.is_clock_dec_type vdecl.var_dec_type.ty_dec_desc
+ then (vdecl.var_id, ident_of_expr arg) :: res
+ else res)
+ input_arg_list []
+*)
(*
expr, locals', eqs = inline_call id args' reset locals node nodes
@@ -73,30 +73,49 @@ let inline_call node orig_expr args reset locals caller =
if v = tag_true || v = tag_false || not (is_node_var node v) then v else
Corelang.mk_new_node_name caller (Format.sprintf "%s_%i_%s" node.node_id uid v)
in
- let eqs' = List.map (rename_eq rename) (get_node_eqs node)
- in
- let static_inputs = get_static_inputs node args in
- let carrier_inputs = get_carrier_inputs node args in
+ let eqs' = List.map (rename_eq rename) (get_node_eqs node) in
+ let input_arg_list = List.combine node.node_inputs (Corelang.expr_list_of_expr args) in
+ let static_inputs, dynamic_inputs = List.partition (fun (vdecl, arg) -> vdecl.var_dec_const) input_arg_list in
+ let static_inputs = List.map (fun (vdecl, arg) -> vdecl, Corelang.dimension_of_expr arg) static_inputs in
+ let carrier_inputs, other_inputs = List.partition (fun (vdecl, arg) -> Corelang.is_clock_dec_type vdecl.var_dec_type.ty_dec_desc) dynamic_inputs in
+ let carrier_inputs = List.map (fun (vdecl, arg) -> vdecl, Corelang.ident_of_expr arg) carrier_inputs in
let rename_static v =
try
- List.assoc v static_inputs
- with Not_found -> Dimension.mkdim_ident loc v
- (*Format.eprintf "Inliner.rename_static %s = %a@." v Dimension.pp_dimension res; res*)
- in
+ snd (List.find (fun (vdecl, _) -> v = vdecl.var_id) static_inputs)
+ with Not_found -> Dimension.mkdim_ident loc v in
let rename_carrier v =
try
- List.assoc v carrier_inputs
+ snd (List.find (fun (vdecl, _) -> v = vdecl.var_id) carrier_inputs)
with Not_found -> v in
let rename_var v =
- (*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*)
- { v with
- var_id = rename v.var_id;
- var_type = Types.rename_static rename_static v.var_type;
- var_clock = Clocks.rename_static rename_carrier v.var_clock;
- } in
- let inputs' = List.map rename_var node.node_inputs in
+ let vdecl =
+ Corelang.mkvar_decl v.var_loc
+ (rename v.var_id,
+ { v.var_dec_type with ty_dec_desc = Corelang.rename_static rename_static v.var_dec_type.ty_dec_desc },
+ { v.var_dec_clock with ck_dec_desc = Corelang.rename_carrier rename_carrier v.var_dec_clock.ck_dec_desc },
+ v.var_dec_const,
+ Utils.option_map (rename_expr rename) v.var_dec_value) in
+ begin
+(*
+ (try
+ Format.eprintf "Inliner.inline_call unify %a %a@." Types.print_ty vdecl.var_type Dimension.pp_dimension (List.assoc v.var_id static_inputs);
+ Typing.unify vdecl.var_type (Type_predef.type_static (List.assoc v.var_id static_inputs) (Types.new_var ()))
+ with Not_found -> ());
+ (try
+Clock_calculus.unify vdecl.var_clock (Clock_predef.ck_carrier (List.assoc v.var_id carrier_inputs) (Clocks.new_var true))
+ with Not_found -> ());
+(*Format.eprintf "Inliner.inline_call res=%a@." Printers.pp_var vdecl;*)
+*)
+ vdecl
+ end
+ (*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*)
+ in
+ let inputs' = List.map (fun (vdecl, _) -> rename_var vdecl) dynamic_inputs in
let outputs' = List.map rename_var node.node_outputs in
- let locals' = List.map rename_var node.node_locals in
+ let locals' =
+ (List.map (fun (vdecl, arg) -> let vdecl' = rename_var vdecl in { vdecl' with var_dec_value = Some (Corelang.expr_of_dimension arg) }) static_inputs)
+ @ (List.map rename_var node.node_locals)
+in
(* checking we are at the appropriate (early) step: node_checks and
node_gencalls should be empty (not yet assigned) *)
assert (node.node_checks = []);
@@ -105,7 +124,7 @@ let inline_call node orig_expr args reset locals caller =
(* Bug included: todo deal with reset *)
assert (reset = None);
- let assign_inputs = mkeq loc (List.map (fun v -> v.var_id) inputs', args) in
+ let assign_inputs = mkeq loc (List.map (fun v -> v.var_id) inputs', expr_of_expr_list args.expr_loc (List.map snd dynamic_inputs)) in
let expr = expr_of_expr_list loc (List.map expr_of_vdecl outputs')
in
let asserts' = (* We rename variables in assert expressions *)
@@ -215,7 +234,7 @@ let rec inline_expr ?(selection_on_annotation=false) expr locals node nodes =
{ expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts'
and inline_node ?(selection_on_annotation=false) node nodes =
- try Hashtbl.find inline_table node.node_id
+ try copy_node (Hashtbl.find inline_table node.node_id)
with Not_found ->
let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
let new_locals, eqs, asserts =
@@ -269,24 +288,26 @@ let witness filename main_name orig inlined type_env clock_env =
(* One ok_i boolean variable per output var *)
let nb_outputs = List.length main_orig_node.node_outputs in
+ let ok_ident = "OK" in
let ok_i = List.map (fun id ->
mkvar_decl
loc
- ("OK" ^ string_of_int id,
+ (Format.sprintf "%s_%i" ok_ident id,
{ty_dec_desc=Tydec_bool; ty_dec_loc=loc},
{ck_dec_desc=Ckdec_any; ck_dec_loc=loc},
- false)
+ false,
+ None)
) (Utils.enumerate nb_outputs)
in
(* OK = ok_1 and ok_2 and ... ok_n-1 *)
- let ok_ident = "OK" in
let ok_output = mkvar_decl
loc
(ok_ident,
{ty_dec_desc=Tydec_bool; ty_dec_loc=loc},
{ck_dec_desc=Ckdec_any; ck_dec_loc=loc},
- false)
+ false,
+ None)
in
let main_ok_expr =
let mkv x = mkexpr loc (Expr_ident x) in
@@ -342,42 +363,35 @@ let witness filename main_name orig inlined type_env clock_env =
in
let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc; top_decl_owner = filename; top_decl_itf = false }] in
let new_prog = others@nodes_origs@nodes_inlined@main in
-
- let _ = Typing.type_prog type_env new_prog in
- let _ = Clock_calculus.clock_prog clock_env new_prog in
-
-
let witness_file = (Options.get_witness_dir filename) ^ "/" ^ "inliner_witness.lus" in
let witness_out = open_out witness_file in
let witness_fmt = Format.formatter_of_out_channel witness_out in
- Format.fprintf witness_fmt
- "(* Generated lustre file to check validity of inlining process *)@.";
- Printers.pp_prog witness_fmt new_prog;
- Format.fprintf witness_fmt "@.";
- () (* xx *)
+ begin
+ List.iter (fun vdecl -> Typing.try_unify Type_predef.type_bool vdecl.var_type vdecl.var_loc) (ok_output::ok_i);
+ Format.fprintf witness_fmt
+ "(* Generated lustre file to check validity of inlining process *)@.";
+ Printers.pp_prog witness_fmt new_prog;
+ Format.fprintf witness_fmt "@.";
+ ()
+ end (* xx *)
let global_inline basename prog type_env clock_env =
(* We select the main node desc *)
let main_node, other_nodes, other_tops =
- List.fold_left
- (fun (main_opt, nodes, others) top ->
+ List.fold_right
+ (fun top (main_opt, nodes, others) ->
match top.top_decl_desc with
| Node nd when nd.node_id = !Options.main_node ->
Some top, nodes, others
| Node _ -> main_opt, top::nodes, others
| _ -> main_opt, nodes, top::others)
- (None, [], []) prog
+ prog (None, [], [])
in
+
(* Recursively each call of a node in the top node is replaced *)
let main_node = Utils.desome main_node in
let main_node' = inline_all_calls main_node other_nodes in
- let res = main_node'::other_tops in
- if !Options.witnesses then (
- witness
- basename
- (match main_node.top_decl_desc with Node nd -> nd.node_id | _ -> assert false)
- prog res type_env clock_env
- );
+ let res = List.map (fun top -> if check_node_name !Options.main_node top then main_node' else top) prog in
res
let local_inline basename prog type_env clock_env =
diff --git a/src/location.ml b/src/location.ml
index 31f25234eff0dff31a9706f36cff1b004a90ef79..3b99fde85aaad526085523e45b2fb4142846bfa0 100755
--- a/src/location.ml
+++ b/src/location.ml
@@ -67,6 +67,7 @@ let print loc =
let pp_loc fmt loc =
+ if loc == dummy_loc then () else
let filename = loc.loc_start.Lexing.pos_fname in
let line = loc.loc_start.Lexing.pos_lnum in
let start_char =
diff --git a/src/lusic.ml b/src/lusic.ml
index 089cac0effd97dd2cd341ce52b6a14deb6f96c30..188990b7badb42936687b2ad6f7d697f4c91dd80 100644
--- a/src/lusic.ml
+++ b/src/lusic.ml
@@ -19,7 +19,9 @@ open Corelang
(********************************************************************************************)
type lusic =
-{ from_lusi : bool;
+{
+ obsolete : bool;
+ from_lusi : bool;
contents : top_decl list;
}
@@ -41,12 +43,27 @@ let extract_header dirname basename prog =
| Open _ -> decl :: header)
prog []
+let check_obsolete lusic basename =
+ if lusic.obsolete then raise (Error (Location.dummy_loc, Wrong_number basename))
+
+let check_lusic lusic basename =
+ try
+ check_obsolete lusic basename
+ with
+ | Corelang.Error (loc, err) as exc -> (
+ eprintf "Library error: %a%a@."
+ Corelang.pp_error err
+ Location.pp_loc loc;
+ raise exc
+ )
+
(* encode and write a header in a file *)
let write_lusic lusi (header : top_decl list) basename extension =
let target_name = basename ^ extension in
let outchan = open_out_bin target_name in
begin
- Marshal.to_channel outchan {from_lusi = lusi; contents = header} [];
+ Marshal.to_channel outchan (Version.number, lusi : string * bool) [];
+ Marshal.to_channel outchan (header : top_decl list) [];
close_out outchan
end
@@ -54,11 +71,27 @@ let write_lusic lusi (header : top_decl list) basename extension =
let read_lusic basename extension =
let source_name = basename ^ extension in
let inchan = open_in_bin source_name in
- let lusic = (Marshal.from_channel inchan : lusic) in
- begin
- close_in inchan;
- lusic
- end
+ let number, from_lusi = (Marshal.from_channel inchan : string * bool) in
+ if number <> Version.number
+ then
+ begin
+ close_in inchan;
+ {
+ obsolete = true;
+ from_lusi = from_lusi;
+ contents = [];
+ }
+ end
+ else
+ begin
+ let lusic = (Marshal.from_channel inchan : top_decl list) in
+ close_in inchan;
+ {
+ obsolete = false;
+ from_lusi = from_lusi;
+ contents = lusic;
+ }
+ end
let print_lusic_to_h basename extension =
let lusic = read_lusic basename extension in
@@ -66,6 +99,7 @@ let print_lusic_to_h basename extension =
let h_out = open_out header_name in
let h_fmt = formatter_of_out_channel h_out in
begin
+ check_lusic lusic basename;
Typing.uneval_prog_generics lusic.contents;
Clock_calculus.uneval_prog_generics lusic.contents;
Header.print_header_from_header h_fmt (Filename.basename basename) lusic.contents;
diff --git a/src/lustreSpec.ml b/src/lustreSpec.ml
index 876ccbaa3803cab71986435b6269c4a1c72adfaa..79c9f5d4b1f9fdd2c31204b2b9f8eac8540ce1de 100644
--- a/src/lustreSpec.ml
+++ b/src/lustreSpec.ml
@@ -48,12 +48,24 @@ and clock_dec_desc =
| Ckdec_bool of (ident * ident) list
| Ckdec_pclock of int * rat
+type constant =
+ | Const_int of int
+ | Const_real of string
+ | Const_float of float
+ | Const_array of constant list
+ | Const_tag of label
+ | Const_string of string (* used only for annotations *)
+ | Const_struct of (label * constant) list
+
+type quantifier_type = Exists | Forall
+
type var_decl =
{var_id: ident;
var_orig:bool;
var_dec_type: type_dec;
var_dec_clock: clock_dec;
var_dec_const: bool;
+ var_dec_value: expr option;
mutable var_type: Types.type_expr;
mutable var_clock: Clocks.clock_expr;
var_loc: Location.t}
@@ -64,20 +76,10 @@ type var_decl =
duplicate ast structures (e.g. ast, typed_ast, clocked_ast). *)
-type constant =
- | Const_int of int
- | Const_real of string
- | Const_float of float
- | Const_array of constant list
- | Const_tag of label
- | Const_string of string (* used only for annotations *)
- | Const_struct of (label * constant) list
-
-type quantifier_type = Exists | Forall
(* The tag of an expression is a unique identifier used to distinguish
different instances of the same node *)
-type expr =
+and expr =
{expr_tag: tag;
expr_desc: expr_desc;
mutable expr_type: Types.type_expr;
@@ -220,6 +222,7 @@ type error =
| Unbound_symbol of ident
| Already_bound_symbol of ident
| Unknown_library of ident
+ | Wrong_number of ident
(* Local Variables: *)
(* compile-command:"make -C .." *)
diff --git a/src/machine_code.ml b/src/machine_code.ml
index 8df2baa6f49eedab125f06c5cf3cdd462087cbdc..491e94f63e29c1897322fe7c5504dcca3628930c 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -83,6 +83,7 @@ type machine_t = {
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;
@@ -105,11 +106,12 @@ let pp_static_call fmt (node, args) =
let pp_machine fmt m =
Format.fprintf fmt
- "@[<v 2>machine %s@ mem : %a@ instances: %a@ init : %a@ step :@ @[<v 2>%a@]@ @ spec : @[%t@]@ annot : @[%a@]@]@ "
+ "@[<v 2>machine %s@ mem : %a@ instances: %a@ init : %a@ const : %a@ step :@ @[<v 2>%a@]@ @ spec : @[%t@]@ annot : @[%a@]@]@ "
m.mname.node_id
(Utils.fprintf_list ~sep:", " Printers.pp_var) m.mmemory
(Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) -> Format.fprintf fmt "(%s, %a)" o1 pp_static_call o2)) m.minstances
(Utils.fprintf_list ~sep:"@ " pp_instr) m.minit
+ (Utils.fprintf_list ~sep:"@ " pp_instr) m.mconst
pp_step m.mstep
(fun fmt -> match m.mspec with | None -> () | Some spec -> Printers.pp_spec fmt spec)
(Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot
@@ -137,6 +139,7 @@ let dummy_var_decl name typ =
var_dec_type = dummy_type_dec;
var_dec_clock = dummy_clock_dec;
var_dec_const = false;
+ var_dec_value = None;
var_type = typ;
var_clock = Clocks.new_ck (Clocks.Cvar Clocks.CSet_all) true;
var_loc = Location.dummy_loc
@@ -183,6 +186,7 @@ let arrow_machine =
mcalls = [];
minstances = [];
minit = [MStateAssign(var_state, Cst (const_of_bool true))];
+ mconst = [];
mstatic = [];
mstep = {
step_inputs = arrow_desc.node_inputs;
@@ -215,6 +219,7 @@ let new_instance =
o
end
+
(* translate_<foo> : node -> context -> <foo> -> machine code/expression *)
(* the context contains m : state aka memory variables *)
(* si : initialization instructions *)
@@ -284,7 +289,7 @@ 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 ?(ite=false) node ((m, si, j, d, s) as args) expr =
let expr = specialize_op expr in
match expr.expr_desc with
| Expr_const v -> Cst v
@@ -305,9 +310,11 @@ let rec translate_expr node ((m, si, j, d, s) as args) expr =
(* 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" ->
+ match !Options.output with
+ | "horn"
+ | ("C" | "java") when ite ->
Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
- | "C" | "java" | _ ->
+ | _ ->
(Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
)
| _ -> raise NormalizationError
@@ -433,7 +440,7 @@ let find_eq xl eqs =
to the computed schedule [sch]
*)
let sort_equations_from_schedule nd sch =
-(* Format.eprintf "%s schedule: %a@."
+(*Format.eprintf "%s schedule: %a@."
nd.node_id
(Utils.fprintf_list ~sep:" ; " Scheduling.pp_eq_schedule) sch;*)
let split_eqs = Splitting.tuple_split_eq_list (get_node_eqs nd) in
@@ -459,6 +466,17 @@ let sort_equations_from_schedule nd sch =
List.rev eqs_rev
end
+let constant_equations nd =
+ List.fold_right (fun vdecl eqs ->
+ if vdecl.var_dec_const
+ then
+ { eq_lhs = [vdecl.var_id];
+ eq_rhs = Utils.desome vdecl.var_dec_value;
+ eq_loc = vdecl.var_loc
+ } :: eqs
+ else eqs)
+ nd.node_locals []
+
let translate_eqs node args eqs =
List.fold_right (fun eq args -> translate_eq node args eq) eqs args;;
@@ -466,10 +484,15 @@ let translate_decl nd sch =
(*Log.report ~level:1 (fun fmt -> Printers.pp_node fmt nd);*)
let sorted_eqs = sort_equations_from_schedule nd sch in
-
+ let constant_eqs = constant_equations nd in
+
let init_args = ISet.empty, [], Utils.IMap.empty, List.fold_right (fun l -> ISet.add l) nd.node_locals ISet.empty, [] in
(* memories, init instructions, node calls, local variables (including memories), step instrs *)
- let m, init, j, locals, s = translate_eqs nd init_args sorted_eqs in
+ let m0, init0, j0, locals0, s0 = translate_eqs nd init_args constant_eqs in
+ assert (ISet.is_empty m0);
+ assert (init0 = []);
+ assert (Utils.IMap.is_empty j0);
+ let m, init, j, locals, s = translate_eqs nd (m0, init0, j0, locals0, s0) sorted_eqs in
let mmap = Utils.IMap.fold (fun i n res -> (i, n)::res) j [] in
{
mname = nd;
@@ -477,6 +500,7 @@ let translate_decl nd sch =
mcalls = mmap;
minstances = List.filter (fun (_, (n,_)) -> not (Stateless.check_node n)) mmap;
minit = init;
+ mconst = s0;
mstatic = List.filter (fun v -> v.var_dec_const) nd.node_inputs;
mstep = {
step_inputs = nd.node_inputs;
@@ -500,7 +524,7 @@ let translate_decl nd sch =
mannot = nd.node_annot;
}
-(** takes the global delcarations and the scheduling associated to each node *)
+(** takes the global declarations and the scheduling associated to each node *)
let translate_prog decls node_schs =
let nodes = get_nodes decls in
List.map
@@ -518,6 +542,46 @@ let get_machine_opt name machines =
| None -> if m.mname.node_id = name then Some m else None)
None machines
+let get_const_assign m id =
+ try
+ match (List.find (fun instr -> match instr with MLocalAssign (v, _) -> v == id | _ -> false) m.mconst) with
+ | MLocalAssign (_, e) -> e
+ | _ -> assert false
+ with Not_found -> assert false
+
+
+let value_of_ident m id =
+ (* is is a state var *)
+ try
+ StateVar (List.find (fun v -> v.var_id = id) m.mmemory)
+ with Not_found ->
+ try (* id is a node var *)
+ LocalVar (get_node_var id m.mname)
+ with Not_found ->
+ try (* id is a constant *)
+ LocalVar (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id)))
+ with Not_found ->
+ (* id is a tag *)
+ Cst (Const_tag id)
+
+let rec value_of_dimension m dim =
+ match dim.Dimension.dim_desc with
+ | Dimension.Dbool b -> Cst (Const_tag (if b then Corelang.tag_true else Corelang.tag_false))
+ | Dimension.Dint i -> Cst (Const_int i)
+ | Dimension.Dident v -> value_of_ident m v
+ | Dimension.Dappl (f, args) -> Fun (f, List.map (value_of_dimension m) args)
+ | Dimension.Dite (i, t, e) -> Fun ("ite", List.map (value_of_dimension m) [i; t; e])
+ | Dimension.Dlink dim' -> value_of_dimension m dim'
+ | _ -> assert false
+
+let rec dimension_of_value value =
+ match value with
+ | Cst (Const_tag t) when t = Corelang.tag_true -> Dimension.mkdim_bool Location.dummy_loc true
+ | Cst (Const_tag t) when t = Corelang.tag_false -> Dimension.mkdim_bool Location.dummy_loc false
+ | Cst (Const_int i) -> Dimension.mkdim_int Location.dummy_loc i
+ | LocalVar v -> Dimension.mkdim_ident Location.dummy_loc v.var_id
+ | Fun (f, args) -> Dimension.mkdim_appl Location.dummy_loc f (List.map dimension_of_value args)
+ | _ -> assert false
(* Local Variables: *)
(* compile-command:"make -C .." *)
diff --git a/src/main_lustre_compiler.ml b/src/main_lustre_compiler.ml
index 0ce60512414cf2533e9adcc331038f445e57cf03..d0b43086d2861a10e302de531e60dc39094229b9 100644
--- a/src/main_lustre_compiler.ml
+++ b/src/main_lustre_compiler.ml
@@ -76,6 +76,7 @@ let compile_source_to_header prog computed_types_env computed_clocks_env dirname
else
begin
Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name);
+ Lusic.check_lusic lusic destname;
let header = lusic.Lusic.contents in
let (declared_types_env, declared_clocks_env) = get_envs_from_top_decls header in
check_compatibility
@@ -104,15 +105,25 @@ let rec compile_source dirname basename extension =
(* Sorting nodes *)
let prog = SortProg.sort prog in
+ (* Perform inlining before any analysis *)
+ let orig, prog =
+ if !Options.global_inline && !Options.main_node <> "" then
+ (if !Options.witnesses then prog else []),
+ Inliner.global_inline basename prog type_env clock_env
+ else (* if !Option.has_local_inline *)
+ [],
+ Inliner.local_inline basename prog type_env clock_env
+ in
+
+ (* Checking stateless/stateful status *)
+ check_stateless_decls prog;
+
(* Typing *)
let computed_types_env = type_decls type_env prog in
(* Clock calculus *)
let computed_clocks_env = clock_decls clock_env prog in
- (* Checking stateless/stateful status *)
- check_stateless_decls prog;
-
(* Generating a .lusi header file only *)
if !Options.lusi then
begin
@@ -150,14 +161,22 @@ let rec compile_source dirname basename extension =
Typing.uneval_prog_generics prog;
Clock_calculus.uneval_prog_generics prog;
- (* Perform global inlining *)
- let prog =
- if !Options.global_inline &&
- (match !Options.main_node with | "" -> false | _ -> true) then
- Inliner.global_inline basename prog type_env clock_env
- else (* if !Option.has_local_inline *)
- Inliner.local_inline basename prog type_env clock_env
- in
+ if !Options.global_inline && !Options.main_node <> "" && !Options.witnesses then
+ begin
+ let orig = Corelang.copy_prog orig in
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating witness file !@,");
+ check_stateless_decls orig;
+ let _ = Typing.type_prog type_env orig in
+ let _ = Clock_calculus.clock_prog clock_env orig in
+ Typing.uneval_prog_generics orig;
+ Clock_calculus.uneval_prog_generics orig;
+ Inliner.witness
+ basename
+ !Options.main_node
+ orig prog type_env clock_env;
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@,");
+ end;
+
(*Format.eprintf "Inliner.global_inline<<@.%a@.>>@." Printers.pp_prog prog;*)
(* Computes and stores generic calls for each node,
only useful for ANSI C90 compliant generic node compilation *)
@@ -194,7 +213,10 @@ let rec compile_source dirname basename extension =
*)
let prog =
if !Options.optimization >= 4 then
- Optimize_prog.prog_unfold_consts prog
+ begin
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. constants elimination@,");
+ Optimize_prog.prog_unfold_consts prog
+ end
else
prog
in
@@ -221,7 +243,7 @@ let rec compile_source dirname basename extension =
end
else
machine_code
- in
+ in
Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,"
(Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
machine_code);
@@ -230,8 +252,8 @@ let rec compile_source dirname basename extension =
let basename = Filename.basename basename in
let destname = !Options.dest_dir ^ "/" ^ basename in
let _ = match !Options.output with
- "C" ->
- begin
+ | "C" ->
+ begin
let alloc_header_file = destname ^ "_alloc.h" in (* Could be changed *)
let source_lib_file = destname ^ ".c" in (* Could be changed *)
let source_main_file = destname ^ "_main.c" in (* Could be changed *)
diff --git a/src/modules.ml b/src/modules.ml
index e01300b3dd776c63a6301ba20b51ed08c88848aa..6e35682203d0eb16d4e3164aa0709e54d3a3af4f 100644
--- a/src/modules.ml
+++ b/src/modules.ml
@@ -117,15 +117,25 @@ let name_dependency (local, dep) =
((if local then !Options.dest_dir else Version.include_path) ^ "/") ^ dep
let import_dependency loc (local, dep) =
- let basename = name_dependency (local, dep) in
- let extension = ".lusic" in
try
- Lusic.read_lusic basename extension
- with Sys_error msg ->
- begin
+ let basename = name_dependency (local, dep) in
+ let extension = ".lusic" in
+ try
+ let lusic = Lusic.read_lusic basename extension in
+ Lusic.check_obsolete lusic basename;
+ lusic
+ with Sys_error msg ->
+ begin
(*Format.eprintf "Error: %s@." msg;*)
- raise (Error (loc, Unknown_library basename))
- end
+ raise (Error (loc, Unknown_library basename))
+ end
+ with
+ | Corelang.Error (loc, err) as exc -> (
+ Format.eprintf "Library error: %a%a@."
+ Corelang.pp_error err
+ Location.pp_loc loc;
+ raise exc
+ )
let rec load_header_rec imported header =
List.fold_left (fun imp decl ->
diff --git a/src/normalization.ml b/src/normalization.ml
index cd4be955b66233131e784855aa33b74cc66a0883..d38ab4ea44e6822a4c1db68b23efc5005ed444bb 100644
--- a/src/normalization.ml
+++ b/src/normalization.ml
@@ -69,6 +69,7 @@ let mk_fresh_var node loc ty ck =
var_dec_type = dummy_type_dec;
var_dec_clock = dummy_clock_dec;
var_dec_const = false;
+ var_dec_value = None;
var_type = ty;
var_clock = ck;
var_loc = loc
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index 06d9161f6e4a314892c6bb6111fd087cec6e5ee1..7fbd651d150a34d85bc788f5cc198ba3a139be6a 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -14,6 +14,7 @@ open LustreSpec
open Corelang
open Causality
open Machine_code
+open Dimension
let pp_elim fmt elim =
begin
@@ -47,6 +48,9 @@ and eliminate_expr elim expr =
| Power(v1, v2) -> Power(eliminate_expr elim v1, eliminate_expr elim v2)
| Cst _ | StateVar _ -> expr
+let eliminate_dim elim dim =
+ Dimension.expr_replace_expr (fun v -> try dimension_of_value (IMap.find v elim) with Not_found -> mkdim_ident dim.dim_loc v) dim
+
let is_scalar_const c =
match c with
| Const_int _
@@ -116,27 +120,40 @@ and instr_unfold fanin instrs elim instr =
2. local assigns then rewrite occurrences of the lhs in the computed accumulator
*)
+let static_call_unfold elim (inst, (n, args)) =
+ let replace v =
+ try
+ Machine_code.dimension_of_value (IMap.find v elim)
+ with Not_found -> Dimension.mkdim_ident Location.dummy_loc v
+ in (inst, (n, List.map (Dimension.expr_replace_expr replace) args))
+
(** Perform optimization on machine code:
- iterate through step instructions and remove simple local assigns
*)
let machine_unfold fanin elim machine =
(*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "machine_unfold %a@." pp_elim elim);*)
- let eliminated_vars, new_instrs = instrs_unfold fanin elim machine.mstep.step_instrs in
- let new_locals = List.filter (fun v -> not (IMap.mem v.var_id eliminated_vars)) machine.mstep.step_locals
+ let elim_consts, mconst = instrs_unfold fanin elim machine.mconst in
+ let elim_vars, instrs = instrs_unfold fanin elim_consts machine.mstep.step_instrs in
+ let locals = List.filter (fun v -> not (IMap.mem v.var_id elim_vars)) machine.mstep.step_locals in
+ let minstances = List.map (static_call_unfold elim_consts) machine.minstances in
+ let mcalls = List.map (static_call_unfold elim_consts) machine.mcalls
in
{
machine with
mstep = {
machine.mstep with
- step_locals = new_locals;
- step_instrs = new_instrs
- }
+ step_locals = locals;
+ step_instrs = instrs
+ };
+ mconst = mconst;
+ minstances = minstances;
+ mcalls = mcalls;
}
let instr_of_const top_const =
let const = const_of_top top_const in
- let vdecl = mkvar_decl Location.dummy_loc (const.const_id, mktyp Location.dummy_loc Tydec_any, mkclock Location.dummy_loc Ckdec_any, true) in
+ let vdecl = mkvar_decl Location.dummy_loc (const.const_id, mktyp Location.dummy_loc Tydec_any, mkclock Location.dummy_loc Ckdec_any, true, None) in
let vdecl = { vdecl with var_type = const.const_type }
in MLocalAssign (vdecl, Cst const.const_value)
diff --git a/src/options.ml b/src/options.ml
index 9afd6f4c62cd575fad0ecd6aa412a05e3986b17e..5674d2bc4305eec896ad876433e70ad2774b3d78 100755
--- a/src/options.ml
+++ b/src/options.ml
@@ -67,6 +67,7 @@ let options =
"-verbose", Arg.Set_int verbose_level, " changes verbose level <default: 1>";
"-version", Arg.Unit print_version, " displays the version";]
+
let get_witness_dir filename =
(* Make sure the directory exists *)
let dir = !dest_dir ^ "/" ^ (Filename.basename filename) ^ "_witnesses" in
diff --git a/src/parser_lustre.mly b/src/parser_lustre.mly
index 453609055461704ab913c33c464b07320c429c08..952de6cc1128fb9e45b3dbaea70eb70a35f381ad 100755
--- a/src/parser_lustre.mly
+++ b/src/parser_lustre.mly
@@ -78,6 +78,7 @@ let get_current_node () = try List.hd !node_stack with _ -> assert false
%nonassoc prec_exists prec_forall
%nonassoc COMMA
+%nonassoc EVERY
%left MERGE IF
%nonassoc ELSE
%right ARROW FBY
@@ -533,20 +534,33 @@ dim:
locals:
{[]}
-| VAR vdecl_list SCOL {$2}
+| VAR local_vdecl_list SCOL {$2}
vdecl_list:
- vdecl {$1}
+ vdecl {$1}
| vdecl_list SCOL vdecl {$3 @ $1}
vdecl:
-/* Useless no ?*/ ident_list
- { List.map (fun id -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, false)) $1 }
+ ident_list COL typeconst clock
+ { List.map (fun id -> mkvar_decl (id, mktyp $3, $4, false, None)) $1 }
+| CONST ident_list /* static parameters don't have clocks */
+ { List.map (fun id -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, None)) $2 }
+| CONST ident_list COL typeconst /* static parameters don't have clocks */
+ { List.map (fun id -> mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, None)) $2 }
+
+local_vdecl_list:
+ local_vdecl {$1}
+| local_vdecl_list SCOL local_vdecl {$3 @ $1}
+local_vdecl:
+/* Useless no ?*/ ident_list
+ { List.map (fun id -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, false, None)) $1 }
| ident_list COL typeconst clock
- { List.map (fun id -> mkvar_decl (id, mktyp $3, $4, false)) $1 }
-| CONST ident_list COL typeconst /* static parameters don't have clocks */
- { List.map (fun id -> mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true)) $2 }
+ { List.map (fun id -> mkvar_decl (id, mktyp $3, $4, false, None)) $1 }
+| CONST vdecl_ident EQ expr /* static parameters don't have clocks */
+ { [ mkvar_decl ($2, mktyp Tydec_any, mkclock Ckdec_any, true, Some $4) ] }
+| CONST vdecl_ident COL typeconst EQ expr /* static parameters don't have clocks */
+ { [ mkvar_decl ($2, mktyp $4, mkclock Ckdec_any, true, Some $6) ] }
cdecl_list:
cdecl SCOL { (fun itf -> [$1 itf]) }
diff --git a/src/printers.ml b/src/printers.ml
index 0a873310f205e89d78590399abc14d5748e37872..92ea74489687b3ecad93b2337611ee24d0344b87 100644
--- a/src/printers.ml
+++ b/src/printers.ml
@@ -24,6 +24,22 @@ let pp_as_c_macro pp_fun fmt v =
pp_set_all_formatter_output_functions fmt out flush newline spaces;
end
+let rec print_dec_struct_ty_field fmt (label, cty) =
+ fprintf fmt "%a : %a" pp_print_string label print_dec_ty cty
+and print_dec_ty fmt cty =
+ match (*get_repr_type*) cty with
+ | Tydec_any -> fprintf fmt "Any"
+ | Tydec_int -> fprintf fmt "int"
+ | Tydec_real
+ | Tydec_float -> fprintf fmt "real"
+ | Tydec_bool -> fprintf fmt "bool"
+ | Tydec_clock cty' -> fprintf fmt "%a clock" print_dec_ty cty'
+ | Tydec_const c -> fprintf fmt "%s" c
+ | Tydec_enum taglist -> fprintf fmt "enum {%a }"
+ (Utils.fprintf_list ~sep:", " pp_print_string) taglist
+ | Tydec_struct fieldlist -> fprintf fmt "struct {%a }"
+ (Utils.fprintf_list ~sep:"; " print_dec_struct_ty_field) fieldlist
+ | Tydec_array (d, cty') -> fprintf fmt "%a^%a" print_dec_ty cty' Dimension.pp_dimension d
let pp_var_name fmt id = fprintf fmt "%s" id.var_id
@@ -31,10 +47,6 @@ let pp_eq_lhs = fprintf_list ~sep:", " pp_print_string
let pp_var fmt id = fprintf fmt "%s%s: %a" (if id.var_dec_const then "const " else "") id.var_id Types.print_ty id.var_type
-let pp_node_var fmt id = fprintf fmt "%s%s: %a%a" (if id.var_dec_const then "const " else "") id.var_id Types.print_node_ty id.var_type Clocks.print_ck_suffix id.var_clock
-
-let pp_node_args = fprintf_list ~sep:"; " pp_node_var
-
let pp_quantifiers fmt (q, vars) =
match q with
| Forall -> fprintf fmt "forall %a" (fprintf_list ~sep:"; " pp_var) vars
@@ -125,7 +137,19 @@ and pp_expr_annot fmt expr_ann =
in
fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots
-
+(*
+let pp_node_var fmt id = fprintf fmt "%s%s: %a(%a)%a" (if id.var_dec_const then "const " else "") id.var_id print_dec_ty id.var_dec_type.ty_dec_desc Types.print_ty id.var_type Clocks.print_ck_suffix id.var_clock
+*)
+let pp_node_var fmt id =
+ begin
+ fprintf fmt "%s%s: %a%a" (if id.var_dec_const then "const " else "") id.var_id Types.print_node_ty id.var_type Clocks.print_ck_suffix id.var_clock;
+ match id.var_dec_value with
+ | None -> ()
+ | Some v -> fprintf fmt " = %a" pp_expr v
+ end
+
+let pp_node_args = fprintf_list ~sep:"; " pp_node_var
+
let pp_node_eq fmt eq =
fprintf fmt "%a = %a;"
pp_eq_lhs eq.eq_lhs
diff --git a/src/scheduling.ml b/src/scheduling.ml
index 8272bebea8aaff5b6187c0d8e17553cee278b339..8238aa7c8e69fbca13cc7a478ea27dfbf6b39ccf 100644
--- a/src/scheduling.ml
+++ b/src/scheduling.ml
@@ -152,7 +152,7 @@ let schedule_node n =
let sort = topological_sort eq_equiv g in
let unused = Liveness.compute_unused_variables n gg in
let fanin = Liveness.compute_fanin n gg in
-
+
let (disjoint, reuse) =
if !Options.optimization >= 3
then
diff --git a/src/types.ml b/src/types.ml
index 7b13fa4ed5918f3ef93abb782961c5c60536e371..77d017afcef3b092665e3e593ed9efc92ad3ef48 100755
--- a/src/types.ml
+++ b/src/types.ml
@@ -41,7 +41,7 @@ type error =
Unbound_value of ident
| Already_bound of ident
| Already_defined of ident
- | Undefined_var of (unit IMap.t)
+ | Undefined_var of ISet.t
| Declared_but_undefined of ident
| Unbound_type of ident
| Not_a_dimension
@@ -158,10 +158,10 @@ let pp_error fmt = function
fprintf fmt "Expecting %d argument(s) for homomorphic extension, found %d@." ar1 ar2
| Type_mismatch id ->
fprintf fmt "Definition and declaration of type %s don't agree@." id
- | Undefined_var vmap ->
+ | Undefined_var vset ->
fprintf fmt "No definition provided for variable(s): %a@."
(Utils.fprintf_list ~sep:"," pp_print_string)
- (fst (Utils.list_of_imap vmap))
+ (ISet.elements vset)
| Declared_but_undefined id ->
fprintf fmt "%s is declared but not defined@." id
| Type_clash (ty1,ty2) ->
@@ -193,13 +193,6 @@ let get_static_value ty =
| Tstatic (d, _) -> Some d
| _ -> None
-let rec rename_static rename ty =
- match (repr ty).tdesc with
- | Tstatic (d, ty') -> { ty with tdesc = Tstatic (Dimension.expr_replace_expr rename d, rename_static rename ty') }
- | Tarray (d, ty') -> { ty with tdesc = Tarray (Dimension.expr_replace_expr rename d, rename_static rename ty') }
- | _ -> ty
-(*Format.eprintf "Types.rename_static %a = %a@." print_ty ty print_ty res; res*)
-
let get_field_type ty label =
match (repr ty).tdesc with
| Tstruct fl -> (try Some (List.assoc label fl) with Not_found -> None)
diff --git a/src/typing.ml b/src/typing.ml
index 5545ddc7fe7815618cd205d437057394639b5529..45d81bd9b8f1bf7852c1e8c2ec86797edffad516 100755
--- a/src/typing.ml
+++ b/src/typing.ml
@@ -111,6 +111,7 @@ let rec type_coretype type_dim cty =
| Tydec_struct fl -> Type_predef.type_struct (List.map (fun (f, ty) -> (f, type_coretype type_dim ty)) fl)
| Tydec_array (d, ty) ->
begin
+ let d = Dimension.copy (ref []) d in
type_dim d;
Type_predef.type_array d (type_coretype type_dim ty)
end
@@ -311,6 +312,7 @@ let check_constant loc const_expected const_real =
then raise (Error (loc, Not_a_constant))
let rec type_add_const env const arg targ =
+(*Format.eprintf "Typing.type_add_const %a %a@." Printers.pp_expr arg Types.print_ty targ;*)
if const
then let d =
if is_dimension_type targ
@@ -357,6 +359,7 @@ and type_appl env in_main loc const f args =
(* type a call with possible dependent types. [targs] is here a list of (argument, type) pairs. *)
and type_dependent_call env in_main loc const f targs =
+(*Format.eprintf "Typing.type_dependent_call %s@." f;*)
let tins, touts = new_var (), new_var () in
let tfun = Type_predef.type_arrow tins touts in
type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
@@ -367,8 +370,10 @@ and type_dependent_call env in_main loc const f targs =
begin
List.iter2 (fun (a,t) ti ->
let t' = type_add_const env (const || Types.get_static_value ti <> None) a t
- in try_unify ~sub:true ti t' a.expr_loc) targs tins;
- touts
+ in try_unify ~sub:true ti t' a.expr_loc;
+ ) targs tins;
+(*Format.eprintf "Typing.type_dependent_call END@.";*)
+ touts;
end
(* type a simple call without dependent types
@@ -506,16 +511,15 @@ and type_branches env in_main loc const hl =
(** [type_eq env eq] types equation [eq] in environment [env] *)
let type_eq env in_main undefined_vars eq =
+(*Format.eprintf "Typing.type_eq %a@." Printers.pp_node_eq eq;*)
(* Check undefined variables, type lhs *)
let expr_lhs = expr_of_expr_list eq.eq_loc (List.map (fun v -> expr_of_ident v eq.eq_loc) eq.eq_lhs) in
let ty_lhs = type_expr env in_main false expr_lhs in
(* Check multiple variable definitions *)
let define_var id uvars =
- try
- ignore(IMap.find id uvars);
- IMap.remove id uvars
- with Not_found ->
- raise (Error (eq.eq_loc, Already_defined id))
+ if ISet.mem id uvars
+ then ISet.remove id uvars
+ else raise (Error (eq.eq_loc, Already_defined id))
in
(* check assignment of declared constant, assignment of clock *)
let ty_lhs =
@@ -566,23 +570,28 @@ let rec check_type_declaration loc cty =
| _ -> ()
let type_var_decl vd_env env vdecl =
-(*Format.eprintf "Typing.type_var_decl START %a@." Printers.pp_var vdecl;*)
+(*Format.eprintf "Typing.type_var_decl START %a:%a@." Printers.pp_var vdecl Printers.print_dec_ty vdecl.var_dec_type.ty_dec_desc;*)
check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;
let eval_const id = Types.get_static_value (Env.lookup_value env id) in
let type_dim d =
begin
type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) Type_predef.type_int;
+
Dimension.eval Basic_library.eval_env eval_const d;
end in
let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in
- let ty_status =
+
+ let ty_static =
if vdecl.var_dec_const
- then Type_predef.type_static (Dimension.mkdim_var ()) ty
+ then Type_predef.type_static (Dimension.mkdim_var ()) ty
else ty in
- let new_env = Env.add_value env vdecl.var_id ty_status in
+ (match vdecl.var_dec_value with
+ | None -> ()
+ | Some v -> type_subtyping_arg (env, vd_env) false ~sub:false true v ty_static);
+ try_unify ty_static vdecl.var_type vdecl.var_loc;
+ let new_env = Env.add_value env vdecl.var_id ty_static in
type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc;
- vdecl.var_type <- ty_status;
-(*Format.eprintf "END@.";*)
+(*Format.eprintf "END %a@." Types.print_ty ty_static;*)
new_env
let type_var_decl_list vd_env env l =
@@ -614,8 +623,8 @@ let type_node env nd loc =
let new_env = Env.overwrite env delta_env in
let undefined_vars_init =
List.fold_left
- (fun uvs v -> IMap.add v.var_id () uvs)
- IMap.empty vd_env_ol in
+ (fun uvs v -> ISet.add v.var_id uvs)
+ ISet.empty vd_env_ol in
let undefined_vars =
List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init (get_node_eqs nd)
in
@@ -626,7 +635,9 @@ let type_node env nd loc =
) nd.node_asserts;
(* check that table is empty *)
- if (not (IMap.is_empty undefined_vars)) then
+ let local_consts = List.fold_left (fun res vdecl -> if vdecl.var_dec_const then ISet.add vdecl.var_id res else res) ISet.empty nd.node_locals in
+ let undefined_vars = ISet.diff undefined_vars local_consts in
+ if (not (ISet.is_empty undefined_vars)) then
raise (Error (loc, Undefined_var undefined_vars));
let ty_ins = type_of_vlist nd.node_inputs in
let ty_outs = type_of_vlist nd.node_outputs in
@@ -673,10 +684,10 @@ let rec type_top_decl env decl =
try
type_node env nd decl.top_decl_loc
with Error (loc, err) as exc -> (
- if !Options.global_inline then
+ (*if !Options.global_inline then
Format.eprintf "Type error: failing node@.%a@.@?"
Printers.pp_node nd
- ;
+ ;*)
raise exc)
)
| ImportedNode nd ->
diff --git a/test/tests_ok.list b/test/tests_ok.list
index b8264891ddf957cf81be39542f0570bc64b59a15..0d2a2b8c26f43ad97ab063e7e150d278799b7d5f 100644
--- a/test/tests_ok.list
+++ b/test/tests_ok.list
@@ -904,6 +904,7 @@
./tests/arrays_arnaud/generic1.lusi
./tests/arrays_arnaud/generic1.lus
./tests/arrays_arnaud/generic2.lus
+./tests/arrays_arnaud/generic3.lus,top,-dynamic -check-access
./tests/clocks/clocks1.lus,,-lusi
./tests/clocks/clocks1.lusi
./tests/clocks/clocks1.lus