diff --git a/TODO.org b/TODO.org
index a70e2762d78fcd75fda1c6be03506846d5a1fff7..c5d3efe6325d9aa380607c53c371890efb356f31 100644
--- a/TODO.org
+++ b/TODO.org
@@ -131,6 +131,13 @@ But also some not-so-nice features (ploc's remarks):
- in lustre file: contract attached to lustre node before the locals/let
- in lusi file: contract attached to lustre node before the node foo ...
+- Dev. choices
+ - contracts rely look like imported node: a signature and a contract content attached
+ - in lusi one could have an alias for contract / imported node
+ - in lus similarly a top level contract could be parsed as an imported node
+ - contract import would amount to concatenate contract elements
+ from provided nodes or imported nodes.
+
** Development
*** Done
- (ploc) retirer le parser Kind2 et revenir à celui de lustrec
@@ -150,6 +157,12 @@ But also some not-so-nice features (ploc's remarks):
- EMF
- LustreV
+* Slicing
+ - reprendre le slicing inlined de seal pour
+ - when provided with a main node and a selection of outputs or memories
+ - slice the local node
+ - for each node called try to slice to the selected vars
+ - could be used to analyze counterexamples
* TODO refactoring + doc
- separate lustre types from machine types in different files
- split basic libs into backend specific files
diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml
index f61e1ba69560cf938b59d7d647d74337254882ff..ae3c5cb9f8eed9b39578300a745f54da06a5da72 100644
--- a/src/backends/C/c_backend_common.ml
+++ b/src/backends/C/c_backend_common.ml
@@ -231,7 +231,7 @@ let rec pp_c_const fmt c =
| 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 *)
+ | Const_string _ | Const_modeid _ -> assert false (* string occurs in annotations not in C *)
(* Prints a value expression [v], with internal function calls only.
diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index 3666dd58f300d89f292a47eae78bb5c9ceea49e8..29506130dc18bc05ac90f25fe1be61cecf0798ce 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/src/backends/C/c_backend_src.ml
@@ -137,7 +137,8 @@ let rec pp_c_const_suffix var_type fmt c =
| Const_array ca -> let var_type = Types.array_element_type var_type in
fprintf fmt "(%a[]){%a }" (pp_c_type "") var_type (Utils.fprintf_list ~sep:", " (pp_c_const_suffix var_type)) ca
| Const_struct fl -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " (fun fmt (f, c) -> (pp_c_const_suffix (Types.struct_field_type var_type f)) fmt c)) fl
- | Const_string _ -> assert false (* string occurs in annotations not in C *)
+ | Const_string _
+ | Const_modeid _ -> assert false (* string occurs in annotations not in C *)
(* Prints a [value] of type [var_type] indexed by the suffix list [loop_vars] *)
diff --git a/src/backends/Horn/horn_backend_traces.ml b/src/backends/Horn/horn_backend_traces.ml
index 0d3913404b8948f709da73af9eb1771a883b6c46..99811029d26d52e08ff7d6769e7f12aefc6c3eb8 100644
--- a/src/backends/Horn/horn_backend_traces.ml
+++ b/src/backends/Horn/horn_backend_traces.ml
@@ -112,7 +112,8 @@ let memories_next machines m = (* We remove the topest pre in each expression *
(fun def ->
match def with
| Eq eq -> (match eq.eq_lhs with
- | [v] -> v = var_id
+ | [v] -> v = var_id
+ | _ -> assert false
)
| _ -> false)
m.mname.node_stmts
diff --git a/src/checks/algebraicLoop.ml b/src/checks/algebraicLoop.ml
index 557a192d6b9a4d09793ff3e0f237abb243c10c1c..bd1303a5a52cafce78655cfa4ae89a7fb944be35 100644
--- a/src/checks/algebraicLoop.ml
+++ b/src/checks/algebraicLoop.ml
@@ -143,8 +143,8 @@ let fast_stages_processing prog =
Options.verbose_level := !Options.verbose_level - 2;
(* Mini stage 1 *)
- (* Extracting dependencies *)
- let dependencies = Compiler_common.import_dependencies prog in
+ (* Extracting dependencies: fill some table with typing info *)
+ ignore (Compiler_common.import_dependencies prog);
(* Local inlining *)
let prog = Inliner.local_inline prog (* type_env clock_env *) in
(* Checking stateless/stateful status *)
diff --git a/src/clock_calculus.ml b/src/clock_calculus.ml
index c6e7544311379b0cf729fa1642097db2b767680f..78d01a03ad4e4e84d3960d47682522d40bf6be76 100644
--- a/src/clock_calculus.ml
+++ b/src/clock_calculus.ml
@@ -734,6 +734,9 @@ let clock_imported_node env loc nd =
nd.nodei_clock <- ck_node;
Env.add_value env nd.nodei_id ck_node
+
+let new_env = clock_var_decl_list
+
let clock_top_const env cdecl=
let ck = new_var false in
try_generalize ck cdecl.const_loc;
diff --git a/src/lustre_types.ml b/src/lustre_types.ml
index aa5c8c6612c51966d343fabd9fb6ab0369397725..2d7ed6b6eb323fb20771439f5fac3178dbc6e847 100644
--- a/src/lustre_types.ml
+++ b/src/lustre_types.ml
@@ -148,6 +148,7 @@ type contract_desc =
spec_loc: Location.t;
}
+
type offset =
| Index of Dimension.dim_expr
| Field of label
@@ -214,6 +215,7 @@ type const_desc =
mutable const_type: Types.type_expr;
}
+
type top_decl_desc =
| Node of node_desc
| Const of const_desc
@@ -221,7 +223,6 @@ type top_decl_desc =
| Open of bool * string (* the boolean set to true denotes a local
lusi vs a lusi installed at system level *)
| TypeDef of typedef_desc
-| Contract of contract_desc
type top_decl =
{top_decl_desc: top_decl_desc; (* description of the symbol *)
diff --git a/src/mpfr.ml b/src/mpfr.ml
index f7ec336ceed54e88211a216d7437bfbda4756801..1e4c6ecc0069ca1d5cc247dd0b77cc1fc7ea74e9 100644
--- a/src/mpfr.ml
+++ b/src/mpfr.ml
@@ -211,6 +211,21 @@ let rec inject_eq node defvars eq =
let norm_eq = { eq with eq_rhs = norm_rhs } in
norm_eq::defs', vars'
+(* let inject_eexpr ee =
+ * { ee with eexpr_qfexpr = inject_expr ee.eexpr_qfexpr }
+ *
+ * let inject_spec s =
+ * { s with
+ * assume = List.map inject_eexpr s.assume;
+ * guarantees = List.map inject_eexpr s.guarantees;
+ * modes = List.map (fun m ->
+ * { m with
+ * require = List.map inject_eexpr m.require;
+ * ensure = List.map inject_eexpr m.ensure
+ * }
+ * ) s.modes
+ * } *)
+
(** normalize_node node returns a normalized node,
ie.
- updated locals
@@ -247,10 +262,25 @@ let inject_node node =
- compute the associated expression without aliases
*)
(* let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals)) new_locals in *)
+ (* See comment below
+ * let spec = match node.node_spec with
+ * | None -> None
+ * | Some spec -> Some (inject_spec spec)
+ * in *)
let node =
{ node with
node_locals = new_locals;
node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
+ (* Incomplete work: TODO. Do we have to inject MPFR code here?
+ Does it make sense for annotations? For me, only if we produce
+ C code for annotations. Otherwise the various verification
+ backend should have their own understanding, but would not
+ necessarily require this additional normalization. *)
+ (*
+ node_spec = spec;
+ node_annot = List.map (fun ann -> {ann with
+ annots = List.map (fun (ids, ee) -> ids, inject_eexpr ee) ann.annots}
+ ) node.node_annot *)
}
in ((*Printers.pp_node Format.err_formatter node;*) node)
diff --git a/src/mutation.ml b/src/mutation.ml
index c94495255cd7d42303e9d71ef518f361e5f7da18..b98d2cb8276890fc6d1d2c771933619309d82114 100644
--- a/src/mutation.ml
+++ b/src/mutation.ml
@@ -223,6 +223,7 @@ let rdm_mutate_const_value c =
| Const_real (n, i, s) -> let (n', i', s') = rdm_mutate_real (n, i, s) in Const_real (n', i', s')
| Const_array _
| Const_string _
+ | Const_modeid _
| Const_struct _
| Const_tag _ -> c
diff --git a/src/normalization.ml b/src/normalization.ml
index 3cdba2b9adda78c3ca14e427696c12f16c3310a0..f47fbff5e0ec44adaf5a09e7bbf4f0c08a09d050 100644
--- a/src/normalization.ml
+++ b/src/normalization.ml
@@ -488,8 +488,6 @@ let normalize_spec decls node vars s =
let normalize_node decls node =
reset_cpt_fresh ();
let inputs_outputs = node.node_inputs@node.node_outputs in
- let is_local v =
- List.for_all ((<>) v) inputs_outputs in
let orig_vars = inputs_outputs@node.node_locals in
let not_is_orig_var v =
List.for_all ((!=) v) orig_vars in
@@ -595,7 +593,6 @@ let normalize_node decls node =
end;
- let new_locals = List.filter is_local vars in (* TODO a quoi ca sert ? *)
let node =
{ node with
node_locals = all_locals;
diff --git a/src/printers.ml b/src/printers.ml
index bb48165d279359567239d9ecbb0c82d7766cbd3a..cd37a71dd876420786648f9cb1bb8131cfd86b1e 100644
--- a/src/printers.ml
+++ b/src/printers.ml
@@ -367,7 +367,6 @@ let pp_decl fmt decl =
| Const c -> fprintf fmt "const %a" pp_const_decl c
| Open (local, s) -> if local then fprintf fmt "#open \"%s\"" s else fprintf fmt "#open <%s>" s
| TypeDef tdef -> fprintf fmt "%a" pp_typedef tdef
- | Contract c -> pp_spec fmt c (* TODO: may be we need to produce it outside of comments.To be discussed *)
let pp_prog fmt prog =
(* we first print types: the function SortProg.sort could do the job but ut
@@ -385,8 +384,7 @@ let pp_short_decl fmt decl =
| Const c -> fprintf fmt "const %a@ " pp_const_decl c
| Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
| TypeDef tdef -> fprintf fmt "type %s;@ " tdef.tydef_id
- | Contract c -> fprintf fmt "(*@ contract *)@ "
-
+
let pp_lusi fmt decl =
match decl.top_decl_desc with
| ImportedNode ind -> fprintf fmt "%a;@ " pp_imported_node ind
@@ -394,7 +392,6 @@ let pp_lusi fmt decl =
| Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
| TypeDef tdef -> fprintf fmt "%a@ " pp_typedef tdef
| Node _ -> assert false
- | Contract c -> pp_spec fmt c (* TODO idem pp_node: how to print contract in lusi, within/without comments brackets ? *)
let pp_lusi_header fmt basename prog =
fprintf fmt "@[<v 0>";
diff --git a/src/typing.ml b/src/typing.ml
index 6751be896549a22dfb9d034722d7be099e3a7edf..105df8be8ff01e7faf2bf4655889b8da8d4587ec 100644
--- a/src/typing.ml
+++ b/src/typing.ml
@@ -767,8 +767,7 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
type_top_const env c
| TypeDef _ -> List.fold_left type_top_decl env (consts_of_enum_type decl)
| Open _ -> env
- | Contract c -> type_spec env c
-
+
let get_type_of_call decl =
match decl.top_decl_desc with
| Node nd ->
@@ -812,7 +811,6 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
uneval_node_generics (nd.node_inputs @ nd.node_outputs)
| ImportedNode nd ->
uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
- | Contract c -> uneval_spec_generics c
| Const _
| TypeDef _
| Open _