From 9d779097bd97468f3f0d995489db4415bf7900b9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lelio.brun@isae-supaero.fr>
Date: Thu, 3 Feb 2022 15:18:08 +0100
Subject: [PATCH] ast modifs and additional arrow_taint phase to retrieve which
arrow "protects" / "taints" which variable
---
offline_tests/test.ml | 3 +-
src/automata.ml | 6 +-
src/backends/Ada/ada_backend_adb.ml | 5 +-
src/backends/Ada/ada_backend_ads.ml | 4 +-
src/backends/Ada/misc_lustre_function.ml | 2 +-
src/backends/C/c_backend_common.ml | 16 +--
src/backends/C/c_backend_spec.ml | 110 +++++++++---------
src/backends/C/c_backend_src.ml | 7 +-
src/backends/EMF/EMF_backend.ml | 2 +-
src/backends/Horn/horn_backend_common.ml | 18 +--
src/backends/Horn/horn_backend_traces.ml | 2 +-
src/causality.ml | 14 +--
src/causality.mli | 2 +-
src/clock_calculus.ml | 4 +-
src/clocks.ml | 35 ++++--
src/clocks.mli | 2 +
src/compiler_common.ml | 7 +-
src/compiler_stages.ml | 4 +
src/corelang.ml | 34 +++++-
src/corelang.mli | 2 +
src/dune | 1 +
src/features/machine_types/machine_types.ml | 2 +-
src/inliner.ml | 6 +-
src/lustre_types.ml | 4 +-
src/lustre_types.mli | 2 +-
src/machine_code.ml | 32 +++--
src/machine_code_common.ml | 15 ++-
src/machine_code_common.mli | 2 +
src/machine_code_dep.ml | 2 +-
src/machine_code_types.mli | 2 +-
src/normalization.ml | 10 +-
src/optimize_machine.ml | 6 +-
src/parsers/parser_lustre.mly | 25 ++--
src/pathConditions.ml | 2 +-
src/plugins/mpfr/lustrec_mpfr.ml | 4 +-
src/plugins/scopes/scopes.ml | 13 ++-
src/printers.ml | 2 +-
.../semantics/cPS_lustre_generator.ml | 2 +-
src/typing.ml | 11 +-
src/utils/dimension.ml | 12 ++
src/utils/dimension.mli | 2 +
41 files changed, 271 insertions(+), 165 deletions(-)
diff --git a/offline_tests/test.ml b/offline_tests/test.ml
index 77d435cc..629eefbb 100644
--- a/offline_tests/test.ml
+++ b/offline_tests/test.ml
@@ -223,7 +223,7 @@ let read_whole_file f =
let has_warning log =
let open Re.Str in
- let reg = "Warning: Generating stateful spec for uninitialized state variables." in
+ let reg = "Warning: Generating stateful spec for uninitialized state variable" in
try
search_forward (regexp reg) log 0 |> ignore;
true
@@ -274,6 +274,7 @@ let compile report lustrec fs =
fail report log
in
print_result p f fmt_str check;
+ write_report report;
report, ok, ko, ninits, i')
(report, 0, 0, 0, 0) fs
in
diff --git a/src/automata.ml b/src/automata.ml
index 715af1eb..506b2d7d 100644
--- a/src/automata.ml
+++ b/src/automata.ml
@@ -378,7 +378,7 @@ let node_of_assign_until nused used node aut_id aut_state handler =
List.map
copy_var_decl
(aut_state.incoming_r :: aut_state.incoming_s :: new_var_outputs);
- node_locals = List.map copy_var_decl (new_var_locals @ handler.hand_locals);
+ node_locals = List.map (fun v -> copy_var_decl v, None) (new_var_locals @ handler.hand_locals);
node_gencalls = [];
node_checks = [];
node_asserts = handler.hand_asserts;
@@ -520,7 +520,7 @@ let expand_node_stmts nused used loc owner node =
node.node_stmts
in
let node' =
- { node with node_locals = locals' @ node.node_locals; node_stmts = eqs' }
+ { node with node_locals = List.map (fun v -> v, None) locals' @ node.node_locals; node_stmts = eqs' }
in
let top_node = mktop_decl loc owner false (Node node') in
top_types', top_node, top_nodes'
@@ -535,7 +535,7 @@ let rec expand_decls_rec nused top_decls =
let used name =
List.exists (fun v -> v.var_id = name) nd.node_inputs
|| List.exists (fun v -> v.var_id = name) nd.node_outputs
- || List.exists (fun v -> v.var_id = name) nd.node_locals
+ || List.exists (fun (v, _) -> v.var_id = name) nd.node_locals
in
let top_types', top_decl', top_nodes' =
expand_node_stmts
diff --git a/src/backends/Ada/ada_backend_adb.ml b/src/backends/Ada/ada_backend_adb.ml
index cf61062c..2b35098b 100644
--- a/src/backends/Ada/ada_backend_adb.ml
+++ b/src/backends/Ada/ada_backend_adb.ml
@@ -172,8 +172,7 @@ let pp_step_definition env typed_submachines fmt (m, m_spec_opt, guarantees) =
@param typed_submachines list of all typed machine instances of this machine
@param fmt the formater to print on @param machine the machine **)
let pp_reset_definition env typed_submachines fmt (m, m_spec_opt) =
- let build_assign = function
- | var ->
+ let build_assign (var, _) =
mkinstr (MStateAssign (var, mk_default_value var.var_type))
in
let env, memory =
@@ -198,7 +197,7 @@ let pp_reset_definition env typed_submachines fmt (m, m_spec_opt) =
on @param typed_submachines list of all typed machine instances of this
machine @param m the machine **)
let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees), machine)) =
- let env = List.map (fun x -> x.var_id, pp_state_name) machine.mmemory in
+ let env = List.map (fun (x, _) -> x.var_id, pp_state_name) machine.mmemory in
let pp_reset fmt =
if is_machine_statefull machine then
fprintf
diff --git a/src/backends/Ada/ada_backend_ads.ml b/src/backends/Ada/ada_backend_ads.ml
index dd69ab5a..6ecf0e1c 100644
--- a/src/backends/Ada/ada_backend_ads.ml
+++ b/src/backends/Ada/ada_backend_ads.ml
@@ -119,7 +119,7 @@ let pp_file fmt (typed_submachines, ((m_spec_opt, guarantees), m)) =
[]
| Some m ->
List.map
- (fun x ->
+ (fun (x, _) ->
pp_var_decl
(build_pp_var_decl AdaNoMode (Some (true, false, [], [])) x))
m.mmemory
@@ -129,7 +129,7 @@ let pp_file fmt (typed_submachines, ((m_spec_opt, guarantees), m)) =
match m_spec_opt with | None -> [] | Some m_spec -> List.map
(build_pp_var_decl AdaNoMode (Some (true, false, [], []))) (m_spec.mmemory)
in *)
- let vars = List.map (build_pp_var_decl AdaNoMode None) m.mmemory in
+ let vars = List.map (fun (x, _) -> build_pp_var_decl AdaNoMode None x) m.mmemory in
let states =
List.map
(build_pp_state_decl_from_subinstance AdaNoMode None)
diff --git a/src/backends/Ada/misc_lustre_function.ml b/src/backends/Ada/misc_lustre_function.ml
index b14c8535..b2686b21 100644
--- a/src/backends/Ada/misc_lustre_function.ml
+++ b/src/backends/Ada/misc_lustre_function.ml
@@ -25,7 +25,7 @@ let get_machine machines instance =
(** Extract all the inputs and outputs. @param machine the machine @return a
list of all the var_decl of a macine **)
let get_all_vars_machine m =
- m.mmemory @ m.mstep.step_inputs @ m.mstep.step_outputs @ m.mstatic
+ List.map fst m.mmemory @ m.mstep.step_inputs @ m.mstep.step_outputs @ m.mstatic
(** Check if a type is polymorphic. @param typ the type @return true if its
polymorphic **)
diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml
index 8f462db5..4707881d 100644
--- a/src/backends/C/c_backend_common.ml
+++ b/src/backends/C/c_backend_common.ml
@@ -48,7 +48,7 @@ let mk_local n m =
exists (var_is name) m.mstep.step_inputs
|| exists (var_is name) m.mstep.step_outputs
|| exists (var_is name) m.mstep.step_locals
- || exists (var_is name) m.mmemory
+ || exists (fun (x, _) -> var_is name x) m.mmemory
in
mk_new_name used n
@@ -75,7 +75,7 @@ let mk_mem_reset = mk_local "mem_reset"
let mk_instance m =
let used name =
let open List in
- exists (var_is name) m.mstep.step_inputs || exists (var_is name) m.mmemory
+ exists (var_is name) m.mstep.step_inputs || exists (fun (x, _) -> var_is name x) m.mmemory
in
mk_new_name used "inst"
@@ -84,7 +84,7 @@ let mk_instance m =
let mk_attribute m =
let used name =
let open List in
- exists (var_is name) m.mstep.step_inputs || exists (var_is name) m.mmemory
+ exists (var_is name) m.mstep.step_inputs || exists (fun (x, _) -> var_is name x) m.mmemory
in
mk_new_name used "attr"
@@ -110,7 +110,7 @@ let reset_loop_counter () = loop_cpt := -1
let mk_loop_var m () =
let vars =
- m.mstep.step_inputs @ m.mstep.step_outputs @ m.mstep.step_locals @ m.mmemory
+ m.mstep.step_inputs @ m.mstep.step_outputs @ m.mstep.step_locals @ List.map fst m.mmemory
in
let rec aux () =
incr loop_cpt;
@@ -800,7 +800,7 @@ let pp_machine_struct ?(ghost = false) fmt m =
~pp_sep:pp_print_semicolon
~pp_eol:pp_print_semicolon'
~pp_epilogue:(fun fmt () -> fprintf fmt "}@] _reg;")
- pp_c_decl_struct_var)
+ (fun fmt (x, _) -> pp_c_decl_struct_var fmt x))
m.mmemory
(pp_print_list
~pp_open_box:pp_open_vbox0
@@ -1255,7 +1255,8 @@ let pp_static_declare_macro ?(ghost = false) fmt ((m, attr, inst) as macro) =
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
+ List.filter_map (fun (v, _) -> if Types.is_array_type v.var_type then Some v else None)
+ m.mmemory
in
fprintf
fmt
@@ -1298,7 +1299,8 @@ let pp_static_link_instance ?(ghost = false) fmt (i, (m, _)) =
it to a pointer (see pp_registers_struct) *)
let pp_static_link_macro ?(ghost = false) fmt (m, _, inst) =
let array_mem =
- List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory
+ List.filter_map (fun (v, _) -> if Types.is_array_type v.var_type then Some v else None)
+ m.mmemory
in
fprintf
fmt
diff --git a/src/backends/C/c_backend_spec.ml b/src/backends/C/c_backend_spec.ml
index e8b8352f..a17f9b8c 100644
--- a/src/backends/C/c_backend_spec.ml
+++ b/src/backends/C/c_backend_spec.ml
@@ -476,32 +476,41 @@ module PrintSpec = struct
| Memory ResetFlag ->
vdecl_to_val reset_flag
- let find_arrow loc m =
- match
- List.find_opt (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances
- with
- | Some (f, _) ->
- Some f
- | None ->
- Error.pp_warning loc (fun fmt ->
- pp_print_string
- fmt
- "Generating stateful spec for uninitialized state variables.");
- None
-
- let rec has_memory_val m v =
- let has_mem = has_memory_val m in
- match v.value_desc with
- | Var v ->
- is_memory m v
- | Array vl | Fun (_, vl) ->
- List.exists has_mem vl
- | Access (t, i) | Power (t, i) ->
- has_mem t || has_mem i
- | _ ->
- false
+ let find_arrow_val =
+ let bad_inits = Hashtbl.create 32 in
+ let rec find_arrow_val loc m v =
+ let find = find_arrow_val loc m in
+ match v.value_desc with
+ | Var v ->
+ begin match find_tainter_arrow m v with
+ | Some (Some a) ->
+ Some a
+ | Some None ->
+ if not (Hashtbl.mem bad_inits v) then begin
+ Hashtbl.add bad_inits v ();
+ Error.pp_warning loc (fun fmt ->
+ fprintf fmt
+ "Generating stateful spec for uninitialized state variable %s."
+ v.var_id);
+ end;
+ None
+ | None -> None
+ end
+ | Array vl | Fun (_, vl) ->
+ List.find_map find vl
+ | Access (t, i) | Power (t, i) ->
+ begin match find t with
+ | None -> find i
+ | a -> a
+ end
+ | _ ->
+ None
+ in
+ find_arrow_val
- let has_memory_expr m = function Val v -> has_memory_val m v | _ -> false
+ let find_arrow loc m = function
+ | Val v -> find_arrow_val loc m v
+ | _ -> None
let pp_spec mode m fmt f =
let rec pp_spec mode fmt f =
@@ -546,18 +555,16 @@ module PrintSpec = struct
fmt
(Spec_common.type_of_value a, val_of_expr a, val_of_expr b)
in
- if has_memory_expr m b then
- let inst = find_arrow Location.dummy m in
- pp_print_option
- ~none:pp_eq
- (fun fmt inst ->
- pp_paren
- (pp_implies (pp_not (pp_initialization pp_access')) pp_eq)
- fmt
- ((Arrow.arrow_id, (mem_in, inst)), ()))
- fmt
- inst
- else pp_eq fmt ()
+ let inst = find_arrow Location.dummy m b in
+ pp_print_option
+ ~none:pp_eq
+ (fun fmt inst ->
+ pp_paren
+ (pp_implies (pp_not (pp_initialization pp_access')) pp_eq)
+ fmt
+ ((Arrow.arrow_id, (mem_in, inst)), ()))
+ fmt
+ inst
| GEqual (a, b) ->
pp_assign_spec
~pp_op:pp_gequal
@@ -584,18 +591,16 @@ module PrintSpec = struct
pp_forall (pp_locals m) pp_spec' fmt (xs, a)
| Ternary (e, a, b) ->
let pp_ite fmt () = pp_ite pp_expr pp_spec' pp_spec' fmt (e, a, b) in
- if has_memory_expr m e then
- let inst = find_arrow Location.dummy m in
- pp_print_option
- ~none:pp_ite
- (fun fmt inst ->
- pp_paren
- (pp_implies (pp_not (pp_initialization pp_access')) pp_ite)
- fmt
- ((Arrow.arrow_id, (mem_in, inst)), ()))
- fmt
- inst
- else pp_ite fmt ()
+ let inst = find_arrow Location.dummy m e in
+ pp_print_option
+ ~none:pp_ite
+ (fun fmt inst ->
+ pp_paren
+ (pp_implies (pp_not (pp_initialization pp_access')) pp_ite)
+ fmt
+ ((Arrow.arrow_id, (mem_in, inst)), ()))
+ fmt
+ inst
| Predicate p ->
pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p
| StateVarPack ResetFlag ->
@@ -624,7 +629,7 @@ module PrintSpec = struct
fmt
(v.var_type, v', v')
in
- let inst = find_arrow Location.dummy m in
+ let inst = find_arrow Location.dummy m (Val v') in
pp_print_option
~none:pp_eq
(fun fmt inst ->
@@ -745,7 +750,7 @@ let pp_transition_footprint_lemma m fmt t =
let stateless = fst (get_stateless_status m) in
let mems =
ISet.(
- diff (of_list (List.map (fun v -> v.var_id) m.mmemory)) t.tmem_footprint)
+ diff (of_list (List.map (fun (v, _) -> v.var_id) m.mmemory)) t.tmem_footprint)
in
let insts =
IMap.(
@@ -756,7 +761,8 @@ let pp_transition_footprint_lemma m fmt t =
let memories =
List.map
(fun v -> { v with var_type = { v.var_type with tid = -1 } })
- (List.filter (fun v -> ISet.mem v.var_id mems) m.mmemory)
+ (List.filter_map (fun (v, _) -> if ISet.mem v.var_id mems then Some v else None)
+ m.mmemory)
in
let mems_empty = ISet.is_empty mems in
let insts_empty = IMap.is_empty insts in
diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index df21ed74..13713085 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/src/backends/C/c_backend_src.ml
@@ -489,7 +489,8 @@ module Main (Mod : MODIFIERS_SRC) = struct
fprintf fmt "free (_alloc->_reg.%s);" vdecl.var_id
let array_mems m =
- List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory
+ List.filter_map (fun (v, _) -> if Types.is_array_type v.var_type then Some v else None)
+ m.mmemory
let pp_alloc_code fmt m =
fprintf
@@ -722,7 +723,7 @@ module Main (Mod : MODIFIERS_SRC) = struct
~pp_array_mem:(pp_c_decl_array_mem self)
~array_mems:(array_mems m)
~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
- ~mpfr_locals:m.mmemory
+ ~mpfr_locals:(List.map fst m.mmemory)
~pp_extra:(fun fmt () ->
pp_print_list
~pp_open_box:pp_open_vbox0
@@ -745,7 +746,7 @@ module Main (Mod : MODIFIERS_SRC) = struct
~pp_array_mem:(pp_c_decl_array_mem self)
~array_mems:(array_mems m)
~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
- ~mpfr_locals:m.mmemory
+ ~mpfr_locals:(List.map fst m.mmemory)
~pp_extra:(fun fmt () ->
pp_print_list
~pp_open_box:pp_open_vbox0
diff --git a/src/backends/EMF/EMF_backend.ml b/src/backends/EMF/EMF_backend.ml
index a605cd13..3aea2cb7 100644
--- a/src/backends/EMF/EMF_backend.ml
+++ b/src/backends/EMF/EMF_backend.ml
@@ -480,7 +480,7 @@ let pp_machine fmt m =
fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl m.mstep.step_inputs;
fprintf fmt "\"outputs\": [%a],@ " pp_emf_vars_decl m.mstep.step_outputs;
fprintf fmt "\"locals\": [%a],@ " pp_emf_vars_decl m.mstep.step_locals;
- fprintf fmt "\"mems\": [%a],@ " pp_emf_vars_decl m.mmemory;
+ fprintf fmt "\"mems\": [%a],@ " pp_emf_vars_decl (List.map fst m.mmemory);
fprintf fmt "\"original_name\": \"%s\",@ " m.mname.node_id;
fprintf fmt "\"instrs\": {@[<v 0> %a@]@ },@ " (pp_emf_instrs m) instrs;
(match m.mspec.mnode_spec with
diff --git a/src/backends/Horn/horn_backend_common.ml b/src/backends/Horn/horn_backend_common.ml
index f2107000..e85a160d 100644
--- a/src/backends/Horn/horn_backend_common.ml
+++ b/src/backends/Horn/horn_backend_common.ml
@@ -98,12 +98,12 @@ let rename_next = rename (fun n -> n ^ "_x")
let rename_next_list = List.map rename_next
let local_memory_vars machine =
- rename_machine_list machine.mname.node_id machine.mmemory
+ rename_machine_list machine.mname.node_id (List.map fst machine.mmemory)
let instances_memory_vars ?(without_arrow = false) machines machine =
- let rec aux fst prefix m =
- (if not fst then
- rename_machine_list (concat prefix m.mname.node_id) m.mmemory
+ let rec aux first prefix m =
+ (if not first then
+ rename_machine_list (concat prefix m.mname.node_id) (List.map fst m.mmemory)
else [])
@ List.fold_left
(fun accu (id, (n, _)) ->
@@ -113,7 +113,7 @@ let instances_memory_vars ?(without_arrow = false) machines machine =
let machine_n = get_machine machines name in
aux
false
- (concat prefix (if fst then id else concat m.mname.node_id id))
+ (concat prefix (if first then id else concat m.mname.node_id id))
machine_n
@ accu)
[]
@@ -123,7 +123,7 @@ let instances_memory_vars ?(without_arrow = false) machines machine =
(* Extract the arrows of a given node/machine *)
let arrow_vars machines machine : Lustre_types.var_decl list =
- let rec aux fst prefix m =
+ let rec aux first prefix m =
List.fold_left
(fun accu (id, (n, _)) ->
let name = node_name n in
@@ -132,14 +132,14 @@ let arrow_vars machines machine : Lustre_types.var_decl list =
rename_machine_list
(concat
prefix
- (concat (if fst then id else concat m.mname.node_id id) "_arrow"))
- arrow_machine.mmemory
+ (concat (if first then id else concat m.mname.node_id id) "_arrow"))
+ (List.map fst arrow_machine.mmemory)
@ accu
else
let machine_n = get_machine machines name in
aux
false
- (concat prefix (if fst then id else concat m.mname.node_id id))
+ (concat prefix (if first then id else concat m.mname.node_id id))
machine_n
@ accu)
[]
diff --git a/src/backends/Horn/horn_backend_traces.ml b/src/backends/Horn/horn_backend_traces.ml
index afbba341..42b89726 100644
--- a/src/backends/Horn/horn_backend_traces.ml
+++ b/src/backends/Horn/horn_backend_traces.ml
@@ -29,7 +29,7 @@ open Horn_backend_printers
(* Compute memories associated to each machine *)
let compute_mems machines m =
let rec aux prefix m =
- List.map (fun mem -> prefix, mem) m.mmemory
+ List.map (fun (mem, _) -> prefix, mem) m.mmemory
@ List.fold_left
(fun accu (id, (n, _)) ->
let name = node_name n in
diff --git a/src/causality.ml b/src/causality.ml
index d02e2cb0..1a4b2701 100644
--- a/src/causality.ml
+++ b/src/causality.ml
@@ -151,13 +151,13 @@ module ExprDep = struct
let node_local_variables nd =
List.fold_left
- (fun locals v -> ISet.add v.var_id locals)
+ (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 ->
+ (fun locals (v, _) ->
if v.var_dec_const then ISet.add v.var_id locals else locals)
ISet.empty
nd.node_locals
@@ -175,7 +175,7 @@ module ExprDep = struct
nd.node_outputs
in
List.fold_left
- (fun vars v -> ISet.add v.var_id vars)
+ (fun vars (v, _) -> ISet.add v.var_id vars)
inoutputs
nd.node_locals
@@ -522,7 +522,7 @@ module CycleDetection = struct
let mk_copy_var n id =
let used name =
- List.exists (fun v -> v.var_id = name) n.node_locals
+ List.exists (fun (v, _) -> v.var_id = name) n.node_locals
|| List.exists (fun v -> v.var_id = name) n.node_inputs
|| List.exists (fun v -> v.var_id = name) n.node_outputs
in
@@ -784,7 +784,7 @@ let global_dependency node =
( {
node with
node_stmts = List.map (fun eq -> Eq eq) eqs';
- node_locals = vdecls' @ node.node_locals;
+ node_locals = List.map (fun v -> v, None) vdecls' @ node.node_locals;
},
g_non_mems )
with Error (DataCycle _ as exc) -> raise (Error exc)
@@ -805,7 +805,7 @@ module VarClockDep = struct
let g = new_graph () in
let g =
List.fold_left
- (fun g var_decl ->
+ (fun g (var_decl, _) ->
let deps = get_clock_dep var_decl.var_clock in
add_edges [ var_decl.var_id ] deps g)
g
@@ -814,7 +814,7 @@ module VarClockDep = struct
let sorted, no_deps =
TopologicalDepGraph.fold
(fun vid (accu, remaining) ->
- let select v = v.var_id = vid in
+ let select (v, _) = v.var_id = vid in
let selected, not_selected = List.partition select remaining in
selected @ accu, not_selected)
g
diff --git a/src/causality.mli b/src/causality.mli
index 6b72661f..72bbc518 100644
--- a/src/causality.mli
+++ b/src/causality.mli
@@ -32,7 +32,7 @@ end
(* A module to sort dependencies among local variables when relying on clocked
declarations *)
module VarClockDep : sig
- val sort : var_decl list -> var_decl list
+ val sort : (var_decl * 'a) list -> (var_decl * 'a) list
end
module ExprDep : sig
diff --git a/src/clock_calculus.ml b/src/clock_calculus.ml
index 1f2bf34f..ab5bfcea 100644
--- a/src/clock_calculus.ml
+++ b/src/clock_calculus.ml
@@ -684,7 +684,7 @@ let clock_node env loc nd =
(* let is_main = nd.node_id = !Options.main_node in *)
let new_env = clock_var_decl_list env false nd.node_inputs in
let new_env = clock_var_decl_list new_env true nd.node_outputs in
- let new_env = clock_var_decl_list new_env true nd.node_locals in
+ let new_env = clock_var_decl_list new_env true (List.map fst nd.node_locals) in
let eqs, _ = get_node_eqs nd in
(* TODO XXX: perform the clocking on auts. For the moment, it is ignored *)
List.iter (clock_eq new_env) eqs;
@@ -803,7 +803,7 @@ let uneval_top_generics decl =
| Node nd ->
(* A node could contain first-order carrier variable in local vars. This is
not the case for types. *)
- uneval_node_generics (nd.node_inputs @ nd.node_locals @ nd.node_outputs)
+ uneval_node_generics (nd.node_inputs @ List.map fst nd.node_locals @ nd.node_outputs)
| ImportedNode nd ->
uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
| Const _ | Include _ | Open _ | TypeDef _ ->
diff --git a/src/clocks.ml b/src/clocks.ml
index d0d4abf4..f7585213 100644
--- a/src/clocks.ml
+++ b/src/clocks.ml
@@ -291,13 +291,34 @@ let constrained_vars_of_clock ck =
aux [] ck
let eq_carrier cr1 cr2 =
- match (carrier_repr cr1).carrier_desc, (carrier_repr cr2).carrier_desc with
- | Carry_const id1, Carry_const id2 ->
- id1 = id2
- | _ ->
- cr1.carrier_id = cr2.carrier_id
-
-let equal ck1 ck2 = (repr ck1).cid = (repr ck2).cid
+ let cr1' = carrier_repr cr1 in
+ let cr2' = carrier_repr cr2 in
+ cr1.carrier_id = cr2.carrier_id
+ || cr1'.carrier_id = cr2'.carrier_id
+ || cr1'.carrier_desc = cr2'.carrier_desc
+
+let rec eq_clock ck1 ck2 =
+ let ck1' = repr ck1 in
+ let ck2' = repr ck2 in
+ ck1.cid = ck2.cid
+ || ck1'.cid = ck2'.cid
+ || match ck1'.cdesc, ck2'.cdesc with
+ | Carrow (ck11, ck12), Carrow (ck21, ck22) ->
+ eq_clock ck11 ck21 && eq_clock ck12 ck22
+ | Ctuple cks1, Ctuple cks2 ->
+ begin try List.for_all2 eq_clock cks1 cks2 with Invalid_argument _ -> false end
+ | Con (ck1, cr1, x1), Con (ck2, cr2, x2) ->
+ eq_clock ck1 ck2 && eq_carrier cr1 cr2 && x1 = x2
+ | Ccarrying (cr1, ck1), Ccarrying (cr2, ck2) ->
+ eq_carrier cr1 cr2 && eq_clock ck1 ck2
+ | Cunivar, _ | _, Cunivar -> true
+ | _ -> false
+
+let equal ck1 ck2 =
+ (* let ck1 = repr ck1 in *)
+ (* let ck2 = repr ck2 in *)
+ (* ck1.cid = ck2.cid *)
+ eq_clock ck1 ck2
(* Returns the clock root of a clock *)
let rec root ck =
diff --git a/src/clocks.mli b/src/clocks.mli
index 2272fbe6..69502461 100644
--- a/src/clocks.mli
+++ b/src/clocks.mli
@@ -46,6 +46,8 @@ type error =
complexity. *)
val pp : Format.formatter -> t -> unit
+val print_ck_long : Format.formatter -> t -> unit
+
val pp_suffix : Format.formatter -> t -> unit
val new_var : bool -> t
diff --git a/src/compiler_common.ml b/src/compiler_common.ml
index 19d91e06..ba31aefd 100644
--- a/src/compiler_common.ml
+++ b/src/compiler_common.ml
@@ -241,7 +241,7 @@ let resolve_contracts prog =
let imp_in = imp_nd.node_inputs in
let imp_out = imp_nd.node_outputs in
let imp_locals = imp_nd.node_locals in
- let locals = imp_in @ imp_out @ imp_locals @ locals in
+ let locals = imp_in @ imp_out @ List.map fst imp_locals @ locals in
let imp_c = get_node_contract imp_nd in
(* Assigning in and out *)
let mk_def vars_l e =
@@ -310,6 +310,7 @@ let resolve_contracts prog =
false)
(accu_contracts @ prog)
in
+ let node_locals = List.map (fun v -> v, None) node_locals in
let nd =
{
node_id = mk_new_name used (id ^ "_contract");
@@ -356,7 +357,7 @@ let resolve_contracts prog =
let nd =
{
nd with
- node_locals = nd.node_locals @ locals;
+ node_locals = nd.node_locals @ List.map (fun v -> v, None) locals;
node_stmts = nd.node_stmts @ stmts;
node_spec = Some (Contract c);
}
@@ -418,7 +419,7 @@ let update_vdecl_parents_prog prog =
| Node nd ->
List.iter
(update_vdecl_parents nd.node_id)
- (nd.node_inputs @ nd.node_outputs @ nd.node_locals)
+ (nd.node_inputs @ nd.node_outputs @ List.map fst nd.node_locals)
| ImportedNode ind ->
List.iter
(update_vdecl_parents ind.nodei_id)
diff --git a/src/compiler_stages.ml b/src/compiler_stages.ml
index 01ae12b1..a86c7440 100644
--- a/src/compiler_stages.ml
+++ b/src/compiler_stages.ml
@@ -190,6 +190,10 @@ let stage1 params prog dirname basename extension =
Log.report ~level:3 (fun fmt ->
fprintf fmt "@[<v 2>@ %a@]@ " Printers.pp_prog prog);
+ (* Initialization check phase *)
+ Log.report ~level:1 (fun fmt -> fprintf fmt "@ .. initialization check@ ");
+ let prog = Arrow_taint.arrow_taint_prog prog in
+
(* Compatibility with Lusi *)
(* If compiling a lusi, generate the lusic. If this is a lus file, Check the
existence of a lusi (Lustre Interface file) *)
diff --git a/src/corelang.ml b/src/corelang.ml
index 62b47a30..8f49132f 100644
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -56,6 +56,34 @@ let dummy_clock_dec = { ck_dec_desc = Ckdec_any; ck_dec_loc = Location.dummy }
(************************************************************)
(* *)
+let fv_expr e =
+ let open ISet in
+ let rec fv s e = match e.expr_desc with
+ | Expr_ident x ->
+ add x s
+ | Expr_tuple es
+ | Expr_array es ->
+ List.fold_left fv s es
+ | Expr_ite (e1, e2, e3) ->
+ fv (fv (fv s e1) e2) e3
+ | Expr_arrow (e1, e2)
+ | Expr_fby (e1, e2) ->
+ fv (fv s e1) e2
+ | Expr_access (e1, d)
+ | Expr_power (e1, d) ->
+ union (fv s e1) (Dimension.fv d)
+ | Expr_pre e ->
+ fv s e
+ | Expr_when (e, x, _) ->
+ fv (add x s) e
+ | Expr_merge (x, br) ->
+ List.fold_left (fun s (_, e) -> fv s e) (add x s) br
+ | Expr_appl (x, e, r) ->
+ fv (add x (Option.fold ~none:s ~some:(fv s) r)) e
+ | Expr_const _ -> s
+ in
+ fv ISet.empty e
+
let mktyp loc d = { ty_dec_desc = d; ty_dec_loc = loc }
let mkclock loc d = { ck_dec_desc = d; ck_dec_loc = loc }
@@ -754,7 +782,7 @@ let rec is_eq_expr e1 e2 =
| _ ->
false
-let get_node_vars nd = nd.node_inputs @ nd.node_locals @ nd.node_outputs
+let get_node_vars nd = nd.node_inputs @ List.map fst nd.node_locals @ nd.node_outputs
let mk_new_node_name nd id =
let used_vars = get_node_vars nd in
@@ -894,7 +922,7 @@ let copy_node nd =
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_locals = List.map (fun (v, i) -> copy_var_decl v, i) nd.node_locals;
node_gencalls = [];
node_checks = [];
node_stateless = None;
@@ -1105,7 +1133,7 @@ let rename_node f_node f_var nd =
let rename_stmts = rename_stmts f_node f_var in
let inputs = rename_vars nd.node_inputs in
let outputs = rename_vars nd.node_outputs in
- let locals = rename_vars nd.node_locals in
+ let locals = List.map (fun (v, i) -> rename_var v, Option.map f_var i) nd.node_locals in
let gen_calls = List.map rename_expr nd.node_gencalls in
let node_checks = List.map (Dimension.rename f_node f_var) nd.node_checks in
let node_asserts =
diff --git a/src/corelang.mli b/src/corelang.mli
index b6612ad9..1b6f9c80 100644
--- a/src/corelang.mli
+++ b/src/corelang.mli
@@ -39,6 +39,8 @@ module VSet : sig
end
with type elt = var_decl
+val fv_expr : expr -> ISet.t
+
val dummy_type_dec : type_dec
val dummy_clock_dec : clock_dec
diff --git a/src/dune b/src/dune
index 2d02e713..02546538 100644
--- a/src/dune
+++ b/src/dune
@@ -46,6 +46,7 @@
backends
lustrec_mpfr
normalization
+ arrow_taint
machine_types
splitting
compiler_common
diff --git a/src/features/machine_types/machine_types.ml b/src/features/machine_types/machine_types.ml
index 57745ad0..50765873 100644
--- a/src/features/machine_types/machine_types.ml
+++ b/src/features/machine_types/machine_types.ml
@@ -459,7 +459,7 @@ let load prog =
match top.top_decl_desc with
| Node nd ->
(* Format.eprintf "Registeing node %s@." nd.node_id; *)
- let vars = nd.node_inputs @ nd.node_outputs @ nd.node_locals in
+ let vars = nd.node_inputs @ nd.node_outputs @ List.map fst nd.node_locals in
let constrained_vars = register_node vars nd.node_annot in
check_node nd constrained_vars;
diff --git a/src/inliner.ml b/src/inliner.ml
index 8a15a094..e1b15397 100644
--- a/src/inliner.ml
+++ b/src/inliner.ml
@@ -180,7 +180,7 @@ let inline_call node loc uid args reset locals caller =
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
+ @ List.map ( fun (v, _) -> rename_var v) node.node_locals
in
(* checking we are at the appropriate (early) step: node_checks and
node_gencalls should be empty (not yet assigned) *)
@@ -359,13 +359,13 @@ and inline_node ?(selection_on_annotation = false) node nodes =
(Eq { eq with eq_rhs = eq_rhs' } :: new_stmts') @ stmts,
asserts' @ asserts,
annots' @ annots ))
- (node.node_locals, [], node.node_asserts, node.node_annot)
+ (List.map fst node.node_locals, [], node.node_asserts, node.node_annot)
eqs
in
let inlined =
{
node with
- node_locals = new_locals;
+ node_locals = List.map (fun v -> v, None) new_locals;
node_stmts = stmts;
node_asserts = asserts;
node_annot = annots;
diff --git a/src/lustre_types.ml b/src/lustre_types.ml
index cc5d978b..79b38408 100644
--- a/src/lustre_types.ml
+++ b/src/lustre_types.ml
@@ -173,7 +173,7 @@ type node_desc = {
mutable node_clock : Clocks.t;
node_inputs : var_decl list;
node_outputs : var_decl list;
- node_locals : var_decl list;
+ node_locals : (var_decl * ident option) list;
mutable node_gencalls : expr list;
mutable node_checks : Dimension.t list;
node_asserts : assert_t list;
@@ -257,7 +257,7 @@ let node_as_contract nd =
unprocessed one could. So we conservatively merge elements, to enable
printing unprocessed contracts *)
let consts, locals =
- List.partition (fun v -> v.var_dec_const) nd.node_locals
+ List.partition (fun v -> v.var_dec_const) (List.map fst nd.node_locals)
in
{
c with
diff --git a/src/lustre_types.mli b/src/lustre_types.mli
index 160e2572..d533bbfe 100644
--- a/src/lustre_types.mli
+++ b/src/lustre_types.mli
@@ -162,7 +162,7 @@ type node_desc = {
mutable node_clock : Clocks.t;
node_inputs : var_decl list;
node_outputs : var_decl list;
- node_locals : var_decl list;
+ node_locals : (var_decl * ident option) list;
mutable node_gencalls : expr list;
mutable node_checks : Dimension.t list;
node_asserts : assert_t list;
diff --git a/src/machine_code.ml b/src/machine_code.ml
index 1d149421..02cd4fbf 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -147,17 +147,15 @@ let rec translate_act env (y, expr) =
let c = translate_guard c in
let t, spec_t = translate_act (y, t) in
let e, spec_e = translate_act (y, e) in
- mk_conditional ~lustre_eq c [ t ] [ e ], mk_conditional_tr c spec_t spec_e
+ mk_conditional ~lustre_eq c [ t ] [ e ],
+ mk_conditional_tr c spec_t spec_e
| Expr_merge (x, hl) ->
let var_x = env.get_var x in
let hl, spec_hl =
- List.(
- split
- (map
- (fun (t, h) ->
- let h, spec_h = translate_act (y, h) in
- (t, [ h ]), (t, spec_h))
- hl))
+ List.fold_right (fun (t, h) (hl, spec_hl) ->
+ let h, spec_h = translate_act (y, h) in
+ (t, [ h ]) :: hl, (t, spec_h) :: spec_hl)
+ hl ([], [])
in
mk_branch' ~lustre_eq var_x hl, mk_branch_tr var_x spec_hl
| _ ->
@@ -178,6 +176,8 @@ let get_memories env = List.fold_left (get_memory env) VSet.empty
type machine_ctx = {
(* memories *)
m : ISet.t;
+ (* arrows *)
+ a: ident IMap.t;
(* Reset instructions *)
si : instr_t list;
(* Instances *)
@@ -199,7 +199,7 @@ type machine_ctx = {
}
let ctx_init =
- { m = ISet.empty; si = []; j = IMap.empty; s = []; mp = []; t = [] }
+ { m = ISet.empty; a = IMap.empty; si = []; j = IMap.empty; s = []; mp = []; t = [] }
(****************************************************************)
(* Main function to translate equations into this machine context we are
@@ -320,7 +320,10 @@ let translate_eq env ctx nd inputs locals outputs i eq =
(mk_transition ~inst false (node_name td) [ vdecl_to_val var_x ])
{ ctx with j = IMap.add inst (td, []) ctx.j }
in
- { ctx with si = mkinstr (MSetReset inst) :: ctx.si }
+ { ctx with
+ si = mkinstr (MSetReset inst) :: ctx.si;
+ a = IMap.add x inst ctx.a
+ }
| [ x ], Expr_pre e when env.is_local x ->
let var_x = env.get_var x in
let e = translate_expr e in
@@ -576,7 +579,7 @@ let translate_decl nd sch =
let new_locals, assert_instrs, nd_node_asserts = process_asserts nd in
(* Build the env: variables visible in the current scope *)
- let locals = nd.node_locals @ new_locals in
+ let locals = List.map fst nd.node_locals @ new_locals in
(* let locals = VSet.of_list locals_list in *)
(* let inout_vars = nd.node_inputs @ nd.node_outputs in *)
let env = build_env nd.node_inputs locals nd.node_outputs in
@@ -655,10 +658,15 @@ let translate_decl nd sch =
])
MClearReset
in
+ let find_arrow v =
+ match List.assoc_opt v nd.node_locals with
+ | Some (Some x) -> IMap.find_opt x ctx.a
+ | _ -> None
+ in
let mnode_spec = Utils.option_map (translate_spec env) nd.node_spec in
{
mname = nd;
- mmemory = VSet.elements mems;
+ mmemory = VSet.fold (fun x xs -> (x, find_arrow x) :: xs) mems [];
mcalls = mmap;
minstances =
List.filter (fun (_, (n, _)) -> not (Stateless.check_node n)) mmap;
diff --git a/src/machine_code_common.ml b/src/machine_code_common.ml
index f3d1a1c3..9ceeb9d6 100644
--- a/src/machine_code_common.ml
+++ b/src/machine_code_common.ml
@@ -7,7 +7,12 @@ open Format
let print_statelocaltag = true
-let is_memory m id = List.exists (fun o -> o.var_id = id.var_id) m.mmemory
+let find_tainter_arrow m id =
+ List.find_opt (fun (x, _) -> x.var_id = id.var_id) m.mmemory
+ |> Option.map snd
+
+let is_memory m id =
+ Option.is_some (find_tainter_arrow m id)
let is_reset_flag id = id.var_id = "_reset"
@@ -248,7 +253,7 @@ let get_node_def id m =
(* merge log: machine_vars was in 44686 *)
let machine_vars m =
- m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ m.mmemory
+ m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ List.map fst m.mmemory
let pp_step m fmt s =
fprintf
@@ -327,7 +332,7 @@ let pp_machine fmt m =
: %a@ step :@ @[<v 2>%a@]@ spec : @[<v>%t@ %a@ @ %a@]@ annot \
: @[%a@]@]@ "
m.mname.node_id
- (pp_comma_list Printers.pp_var)
+ (pp_comma_list (fun fmt (x, _) -> Printers.pp_var fmt x))
m.mmemory
(pp_comma_list pp_instance)
m.minstances
@@ -423,7 +428,7 @@ let arrow_machine =
reprendre le type des variables non ? *)
{
mname = Arrow.arrow_desc;
- mmemory = [ var_state ];
+ mmemory = [ var_state, None ];
mcalls = [];
minstances = [];
minit = [ mkinstr (MStateAssign (var_state, cst true)) ];
@@ -565,7 +570,7 @@ let get_const_assign m id =
let value_of_ident loc m id =
(* is is a state var *)
try
- let v = List.find (fun v -> v.var_id = id) m.mmemory in
+ let v, _ = List.find (fun (v, _) -> v.var_id = id) m.mmemory in
mk_val (Var v) v.var_type
with Not_found -> (
try
diff --git a/src/machine_code_common.mli b/src/machine_code_common.mli
index b920f694..e6e07d35 100644
--- a/src/machine_code_common.mli
+++ b/src/machine_code_common.mli
@@ -4,6 +4,8 @@ open Machine_code_types
val pp_val : machine_t -> Format.formatter -> value_t -> unit
+val find_tainter_arrow : machine_t -> var_decl -> ident option option
+
val is_memory : machine_t -> var_decl -> bool
val is_reset_flag : var_decl -> bool
diff --git a/src/machine_code_dep.ml b/src/machine_code_dep.ml
index 36d94768..b93760fb 100644
--- a/src/machine_code_dep.ml
+++ b/src/machine_code_dep.ml
@@ -69,4 +69,4 @@ let compute_unused_variables m =
(* Format.printf "unused: %a@;coi of %s: %a@." ISet.pp unused x.var_id ISet.pp coi; *)
ISet.diff unused coi)
(List.fold_left (fun s v -> ISet.add v.var_id s) ISet.empty m.mstep.step_locals)
- (m.mstep.step_outputs @ m.mmemory)
+ (m.mstep.step_outputs @ List.map fst m.mmemory)
diff --git a/src/machine_code_types.mli b/src/machine_code_types.mli
index 45736d90..d96d6fc8 100644
--- a/src/machine_code_types.mli
+++ b/src/machine_code_types.mli
@@ -71,7 +71,7 @@ type machine_spec = {
type machine_t = {
mname : node_desc;
- mmemory : var_decl list;
+ mmemory : (var_decl * ident option) list;
mcalls : (ident * static_call) list;
(* map from stateful/stateless instance to node, no internals *)
minstances : (ident * static_call) list;
diff --git a/src/normalization.ml b/src/normalization.ml
index e039d11f..a8ef1a02 100644
--- a/src/normalization.ml
+++ b/src/normalization.ml
@@ -732,7 +732,7 @@ let normalize_spec parentid (in_vars, out_vars, l_vars) s =
*)
let normalize_node ?(first=true) node =
reset_cpt_fresh ();
- let orig_vars = node.node_inputs @ node.node_outputs @ node.node_locals in
+ let orig_vars = node.node_inputs @ node.node_outputs @ List.map fst node.node_locals in
let not_is_orig_var v = List.for_all (( != ) v) orig_vars in
let norm_ctx =
{
@@ -758,7 +758,7 @@ let normalize_node ?(first=true) node =
| Some (Contract s) ->
let new_locals, new_outs, new_stmts, s' =
normalize_spec node.node_id
- (node.node_inputs, node.node_outputs, node.node_locals)
+ (node.node_inputs, node.node_outputs, List.map fst node.node_locals)
s
in
(* Format.eprintf "Normalization bounded new locals: %a@." Printers.pp_vars new_locals;
@@ -792,7 +792,7 @@ let normalize_node ?(first=true) node =
(* we filter out inout
vars and initial locals ones *)
- let node_locals = node.node_locals @ new_locals in
+ let node_locals = node.node_locals @ List.map (fun v -> v, None) new_locals in
(* we add again, at the
beginning of the list the
@@ -808,7 +808,9 @@ let normalize_node ?(first=true) node =
let new_annots =
if !Options.traces then
let diff_vars =
- List.filter (fun v -> not (List.mem v node.node_locals)) node_locals
+ let node_locals' = List.map fst node_locals in
+ let node_node_locals' = List.map fst node.node_locals in
+ List.filter (fun v -> not (List.mem v node_node_locals')) node_locals'
in
let norm_traceability =
{
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index da5a941f..9171eb51 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -738,7 +738,7 @@ let machine_cse subst machine =
let assigned = assigns_instrs instrs VSet.empty in
{
machine with
- mmemory = List.filter (fun vdecl -> VSet.mem vdecl assigned) machine.mmemory;
+ mmemory = List.filter (fun (v, _) -> VSet.mem v assigned) machine.mmemory;
mstep =
{
machine.mstep with
@@ -1185,7 +1185,7 @@ let elim_prog_variables prog removed_table =
(fun v (_, eq) (accu_locals, accu_defs) ->
let locals =
try
- List.find (fun v' -> v'.var_id = v) nd.node_locals
+ List.find (fun v' -> v'.var_id = v) (List.map fst nd.node_locals)
:: accu_locals
with Not_found -> accu_locals
(* Variable v shall be a global constant, we do no need to
@@ -1212,7 +1212,7 @@ let elim_prog_variables prog removed_table =
when List.exists (fun v -> v.var_id = lhs) vars_to_replace
->
(* We remove the def *)
- List.filter (fun v -> v.var_id <> lhs) locals, res_stmts
+ List.filter (fun (v, _) -> v.var_id <> lhs) locals, res_stmts
| _ ->
(* When more than one lhs we just keep the equation and do
not delete it *)
diff --git a/src/parsers/parser_lustre.mly b/src/parsers/parser_lustre.mly
index 5038be55..588f4f19 100644
--- a/src/parsers/parser_lustre.mly
+++ b/src/parsers/parser_lustre.mly
@@ -28,13 +28,18 @@ let mkdim_appl_u loc f x = mkdim_appl loc f [x]
let mkarraytype = List.fold_left (fun t d -> Tydec_array (d, t))
+let mkvdecl const typ clock expr (id, loc) =
+ mkvar_decl loc
+ (id,
+ mktyp loc (match typ with Some t -> t | None -> Tydec_any),
+ (match clock with Some ck -> ck | None -> mkclock loc Ckdec_any),
+ const, expr, None)
+
let mkvdecls const typ clock expr =
- List.map (fun (id, loc) ->
- mkvar_decl loc
- (id,
- mktyp loc (match typ with Some t -> t | None -> Tydec_any),
- (match clock with Some ck -> ck | None -> mkclock loc Ckdec_any),
- const, expr, None))
+ List.map (mkvdecl const typ clock expr)
+
+let mkvdecls_locals const typ clock expr =
+ List.map (fun id_loc -> mkvdecl const typ clock expr id_loc, None)
(* let mkannots annots = { annots = annots; annot_loc = get_loc () } *)
@@ -318,7 +323,7 @@ automaton:
handler:
| STATE x=UIDENT COL ul=unless* l=locals LET ss=stmt_list TEL ut=until*
- { Automata.mkhandler $sloc x ul ut l ss }
+ { Automata.mkhandler $sloc x ul ut (List.map fst l) ss }
unless:
| UNLESS e=expr RESTART s=UIDENT { $sloc, e, true, s }
@@ -577,12 +582,12 @@ vdecl:
local_vdecl:
| xs=ident_list /* Useless no ?*/
- { mkvdecls false None None None xs }
+ { mkvdecls_locals false None None None xs }
| xs=ident_list COL t=typeconst c=clock?
- { mkvdecls false (Some t) c None xs }
+ { mkvdecls_locals false (Some t) c None xs }
| CONST x=vdecl_ident t=preceded(COL, typeconst)? EQ e=expr
/* static parameters don't have clocks */
- { mkvdecls true t None (Some e) [x] }
+ { mkvdecls_locals true t None (Some e) [x] }
cdecl:
| x=const_ident EQ c=signed_const
diff --git a/src/pathConditions.ml b/src/pathConditions.ml
index 68d6de05..9720da97 100644
--- a/src/pathConditions.ml
+++ b/src/pathConditions.ml
@@ -370,7 +370,7 @@ let mcdc_top_decl td =
Node
{
nd with
- node_locals = nd.node_locals @ fresh_vars;
+ node_locals = nd.node_locals @ List.map (fun v -> v, None) fresh_vars;
node_stmts = nd.node_stmts @ fresh_eqs;
node_annot = nd.node_annot @ fresh_annots;
};
diff --git a/src/plugins/mpfr/lustrec_mpfr.ml b/src/plugins/mpfr/lustrec_mpfr.ml
index 334886c5..ccb2c6d0 100644
--- a/src/plugins/mpfr/lustrec_mpfr.ml
+++ b/src/plugins/mpfr/lustrec_mpfr.ml
@@ -333,7 +333,7 @@ let inject_node node =
let inputs_outputs = node.node_inputs @ node.node_outputs in
let norm_ctx = node.node_id, get_node_vars node in
let is_local v = List.for_all (( != ) v) inputs_outputs in
- let orig_vars = inputs_outputs @ node.node_locals in
+ let orig_vars = inputs_outputs @ List.map fst node.node_locals in
let defs, vars =
let eqs, auts = get_node_eqs node in
if auts != [] then assert false;
@@ -359,7 +359,7 @@ let inject_node node =
(vars, [], [])
node.node_asserts
in
- let new_locals = List.filter is_local vars in
+ let new_locals = List.filter_map (fun v -> if is_local v then Some (v, None) else None) vars in
(* Compute traceability info: - gather newly bound variables - compute the
associated expression without aliases *)
(* let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals))
diff --git a/src/plugins/scopes/scopes.ml b/src/plugins/scopes/scopes.ml
index 85693b13..be6743f8 100644
--- a/src/plugins/scopes/scopes.ml
+++ b/src/plugins/scopes/scopes.ml
@@ -19,9 +19,10 @@ let rec compute_scopes ?(first = true) prog root_node : scope_t list =
(* Format.eprintf "Compute scope of %s@." main_node; *)
try
let node = get_node root_node prog in
- let all_vars = node.node_inputs @ node.node_locals @ node.node_outputs in
+ let locals = List.map fst node.node_locals in
+ let all_vars = node.node_inputs @ locals @ node.node_outputs in
let local_vars =
- if first then node.node_locals else node.node_inputs @ node.node_locals
+ if first then locals else node.node_inputs @ locals
in
let local_scopes = List.map (fun x -> [], x) local_vars in
let sub_scopes =
@@ -84,7 +85,7 @@ let get_node_vdecl_of_name name node =
try
List.find
(fun v -> v.var_id = name)
- (node.node_inputs @ node.node_outputs @ node.node_locals)
+ (node.node_inputs @ node.node_outputs @ List.map fst node.node_locals)
with Not_found ->
Format.eprintf "Cannot find variable %s in node %s@." name node.node_id;
assert false
@@ -239,7 +240,7 @@ let update_machine main_node machine scopes =
(if machine.mname.node_id = main_node then []
else machine.mstep.step_inputs)
(* @ machine.mstep.step_outputs *)
- @ machine.mmemory
+ @ List.map fst machine.mmemory
@ machine.mstep.step_locals
in
let selection =
@@ -258,7 +259,7 @@ let update_machine main_node machine scopes =
in
{
machine with
- mmemory = machine.mmemory @ List.map fst new_mems;
+ mmemory = machine.mmemory @ List.map (fun (v, _) -> v, None) new_mems;
mstep =
{
machine.mstep with
@@ -279,7 +280,7 @@ let rec is_valid_path path nodename prog machines =
let res =
List.exists
(fun v -> v.var_id = vid)
- (m.mmemory @ m.mstep.step_inputs @ m.mstep.step_locals)
+ (List.map fst m.mmemory @ m.mstep.step_inputs @ m.mstep.step_locals)
in
(* if not res then *)
(* Format.eprintf "Variable %s cannot be found in machine %s@.Local vars are
diff --git a/src/printers.ml b/src/printers.ml
index 24df7295..73ba93b3 100644
--- a/src/printers.ml
+++ b/src/printers.ml
@@ -612,7 +612,7 @@ let pp_node fmt nd =
fprintf
fmt
"@[<v 4>var %a@]@ "
- (pp_print_list (fun fmt v -> fprintf fmt "%a;" pp_node_var v))
+ (pp_print_list (fun fmt (v, _) -> fprintf fmt "%a;" pp_node_var v))
locals)
nd.node_locals;
(* Checks *)
diff --git a/src/tools/stateflow/semantics/cPS_lustre_generator.ml b/src/tools/stateflow/semantics/cPS_lustre_generator.ml
index b5b9f5ec..e228aae7 100644
--- a/src/tools/stateflow/semantics/cPS_lustre_generator.ml
+++ b/src/tools/stateflow/semantics/cPS_lustre_generator.ml
@@ -397,7 +397,7 @@ end) : TransformerType = struct
node_clock = Clocks.new_var true;
node_inputs = inputs;
node_outputs = outputs;
- node_locals = mk_locals vars';
+ node_locals = List.map (fun v -> v, None) (mk_locals vars');
(* TODO: add global vars *)
node_gencalls = [];
node_checks = [];
diff --git a/src/typing.ml b/src/typing.ml
index 71dc0883..96605223 100644
--- a/src/typing.ml
+++ b/src/typing.ml
@@ -916,16 +916,17 @@ struct
(* Format.eprintf "Typing node %s@." nd.node_id; *)
let is_main = nd.node_id = !Options.main_node in
(* In contracts, outputs are considered as input values *)
+ let locals_vars = List.map fst nd.node_locals in
let vd_env_ol =
- if nd.node_iscontract then nd.node_locals
- else nd.node_outputs @ nd.node_locals
+ if nd.node_iscontract then locals_vars
+ else nd.node_outputs @ locals_vars
in
- let vd_env = nd.node_inputs @ nd.node_outputs @ nd.node_locals in
+ let vd_env = nd.node_inputs @ nd.node_outputs @ locals_vars in
check_vd_env vd_env;
let init_env = env in
let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in
let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in
- let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in
+ let delta_env = type_var_decl_list vd_env delta_env locals_vars in
let new_env = Env.overwrite env delta_env in
let undefined_vars_init =
List.fold_left (fun uvs v -> ISet.add v.var_id uvs) ISet.empty vd_env_ol
@@ -964,7 +965,7 @@ struct
(* check that table is empty *)
let local_consts =
List.fold_left
- (fun res vdecl ->
+ (fun res (vdecl, _) ->
if vdecl.var_dec_const then ISet.add vdecl.var_id res else res)
ISet.empty
nd.node_locals
diff --git a/src/utils/dimension.ml b/src/utils/dimension.ml
index 36e23a55..32b0f423 100644
--- a/src/utils/dimension.ml
+++ b/src/utils/dimension.ml
@@ -10,6 +10,7 @@
(********************************************************************)
open Format
+open Utils
type t = { mutable dim_desc : dim_desc; dim_loc : Location.t; dim_id : int }
@@ -27,6 +28,17 @@ exception Unify of t * t
exception InvalidDimension
+let fv d =
+ let open ISet in
+ let rec fv s d = match d.dim_desc with
+ | Dident x -> add x s
+ | Dappl (_, ds) -> List.fold_left fv s ds
+ | Dite (d1, d2, d3) -> fv (fv (fv s d1) d2) d3
+ | Dlink d -> fv s d
+ | _ -> s
+ in
+ fv ISet.empty d
+
let new_id = ref (-1)
let mkdim loc dim =
diff --git a/src/utils/dimension.mli b/src/utils/dimension.mli
index 3b66b13d..a8419e14 100644
--- a/src/utils/dimension.mli
+++ b/src/utils/dimension.mli
@@ -16,6 +16,8 @@ exception Unify of t * t
exception InvalidDimension
+val fv : t -> ISet.t
+
val mkdim : Location.t -> dim_desc -> t
val mkdim_ident : Location.t -> ident -> t
--
GitLab