diff --git a/TODO.org b/TODO.org
index 91c9830663698c12c37b736ac48506a702a5523a..87199e28b41bf3c05d18e75d69918b1b59fe835c 100644
--- a/TODO.org
+++ b/TODO.org
@@ -141,7 +141,9 @@ But also some not-so-nice features (ploc's remarks):
** Development
*** Done
- (ploc) retirer le parser Kind2 et revenir à celui de lustrec
+
*** To be done
+
**** Court terme
- (CG) etendre la syntaxe pour coller à la definition donnée ci-dessus
- lexeur/parseur lustreSpec + document latex de grammaire
diff --git a/src/arrow.ml b/src/arrow.ml
index fc38ad5f3e8377c978452c58098fd2cbdcd49f1d..1ce3b268e1843be36510f033dbe97af8de1980e9 100644
--- a/src/arrow.ml
+++ b/src/arrow.ml
@@ -19,7 +19,9 @@ let arrow_desc =
node_dec_stateless = false;
node_stateless = Some false;
node_spec = None;
- node_annot = []; }
+ node_annot = [];
+ node_iscontract = false;
+}
let arrow_top_decl =
{
diff --git a/src/automata.ml b/src/automata.ml
index d543a1e7034856ec4d8400c88571698b87b46ec8..97686e04b92cc519f6de4d800b48eddb2aa81707 100644
--- a/src/automata.ml
+++ b/src/automata.ml
@@ -162,7 +162,8 @@ let node_of_unless nused used node aut_id aut_state handler =
node_dec_stateless = false;
node_stateless = None;
node_spec = None;
- node_annot = []
+ node_annot = [];
+ node_iscontract = false;
},
mkexpr handler.hand_loc (Expr_appl (node_id, mkexpr handler.hand_loc (Expr_tuple args), reset))
@@ -213,7 +214,8 @@ let node_of_assign_until nused used node aut_id aut_state handler =
node_dec_stateless = false;
node_stateless = None;
node_spec = None;
- node_annot = handler.hand_annots
+ node_annot = handler.hand_annots;
+ node_iscontract = false;
},
mkexpr handler.hand_loc (Expr_appl (node_id, mkexpr handler.hand_loc (Expr_tuple args), reset))
diff --git a/src/backends/EMF/EMF_backend.ml b/src/backends/EMF/EMF_backend.ml
index 4a4913be136b3089baafb99e182058c85d48b294..801815020e6a40575620a8e7ab81f08b07f2f731 100644
--- a/src/backends/EMF/EMF_backend.ml
+++ b/src/backends/EMF/EMF_backend.ml
@@ -393,9 +393,9 @@ let pp_emf_spec_import fmt i =
fprintf fmt "\"contract\": \"%s\",@ "
i.import_nodeid;
fprintf fmt "\"inputs\": [%a],@ "
- pp_emf_exprs i.inputs;
+ pp_emf_expr i.inputs;
fprintf fmt "\"outputs\": [%a],@ "
- pp_emf_exprs i.outputs;
+ pp_emf_expr i.outputs;
fprintf fmt "@]}"
let pp_emf_spec_imports = pp_emf_list pp_emf_spec_import
@@ -421,8 +421,14 @@ let pp_emf_spec fmt spec =
let pp_emf_annots cpt fmt annots = fprintf_list ~sep:",@ " (pp_emf_annot cpt) fmt annots.annots
let pp_emf_annots_list cpt fmt annots_list = fprintf_list ~sep:",@ " (pp_emf_annots cpt) fmt annots_list
+let pp_emf_contract fmt nd =
+ let c = Printers.node_as_contract nd in
+ fprintf fmt "@[v 2>\"%a\": {@ "
+ print_protect (fun fmt -> pp_print_string fmt nd.node_id);
+ fprintf fmt "\"contract\": %a@ "
+ pp_emf_spec c;
+ fprintf fmt "@]@ }"
-
let pp_machine fmt m =
let instrs = (*merge_branches*) m.mstep.step_instrs in
try
@@ -445,7 +451,10 @@ let pp_machine fmt m =
fprintf fmt "\"original_name\": \"%s\",@ " m.mname.node_id;
fprintf fmt "\"instrs\": {@[<v 0> %a@]@ },@ "
(pp_emf_instrs m) instrs;
- (match m.mspec with None -> () | Some spec -> fprintf fmt "\"spec\": %a,@ " pp_emf_spec spec);
+ (match m.mspec with | None -> ()
+ | Some (Contract _) -> assert false
+ | Some (NodeSpec id) -> fprintf fmt "\"coco_contract\": %s" id
+ );
fprintf fmt "\"annots\": {@[<v 0> %a@]@ }" (pp_emf_annots_list (ref 0)) m.mannot;
fprintf fmt "@]@ }"
with Unhandled msg -> (
@@ -455,9 +464,14 @@ let pp_machine fmt m =
eprintf "node skipped - no output generated@ @]@."
)
+let pp_machine fmt m =
+ match m.mspec with
+ | None | Some (NodeSpec _) -> pp_machine fmt m
+ | Some (Contract _) -> pp_emf_contract fmt m.mname
+
let pp_emf_imported_node fmt top =
let ind = Corelang.imported_node_of_top top in
- try
+ try
fprintf fmt "@[<v 2>\"%a\": {@ "
print_protect (fun fmt -> pp_print_string fmt ind.nodei_id);
fprintf fmt "\"imported\": \"true\",@ ";
@@ -466,7 +480,10 @@ let pp_emf_imported_node fmt top =
fprintf fmt "\"outputs\": [%a],@ "
pp_emf_vars_decl ind.nodei_outputs;
fprintf fmt "\"original_name\": \"%s\",@ " ind.nodei_id;
- (match ind.nodei_spec with None -> () | Some spec -> fprintf fmt "\"spec\": %a" pp_emf_spec spec);
+ (match ind.nodei_spec with None -> ()
+ | Some (Contract _) -> assert false (* should have been processed *)
+ | Some (NodeSpec id) -> fprintf fmt "\"coco_contract\": %s" id
+ );
fprintf fmt "@]@ }"
with Unhandled msg -> (
eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ "
diff --git a/src/causality.ml b/src/causality.ml
index a11db4293d282604336104a52e7f5dc84b6a2095..97f65972663a71a2d73bee67e80d47996c535e79 100644
--- a/src/causality.ml
+++ b/src/causality.ml
@@ -148,7 +148,15 @@ module ExprDep = struct
List.fold_left eq_memory_variables ISet.empty (get_node_eqs nd)
let node_input_variables nd =
- List.fold_left (fun inputs v -> ISet.add v.var_id inputs) ISet.empty nd.node_inputs
+ List.fold_left (fun inputs v -> ISet.add v.var_id inputs) ISet.empty
+ (if nd.node_iscontract then
+ nd.node_inputs@nd.node_outputs
+ else
+ nd.node_inputs)
+
+ let node_output_variables nd =
+ List.fold_left (fun outputs v -> ISet.add v.var_id outputs) ISet.empty
+ (if nd.node_iscontract then [] else nd.node_outputs)
let node_local_variables nd =
List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty nd.node_locals
@@ -156,9 +164,6 @@ module ExprDep = struct
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
-
let node_auxiliary_variables nd =
ISet.diff (node_local_variables nd) (node_memory_variables nd)
@@ -170,15 +175,17 @@ module ExprDep = struct
(* computes the equivalence relation relating variables
in the same equation lhs, under the form of a table
of class representatives *)
- let node_eq_equiv nd =
+ let eqs_eq_equiv eqs =
let eq_equiv = Hashtbl.create 23 in
List.iter (fun eq ->
let first = List.hd eq.eq_lhs in
List.iter (fun v -> Hashtbl.add eq_equiv v first) eq.eq_lhs
)
- (get_node_eqs nd);
+ eqs;
eq_equiv
-
+
+ let node_eq_equiv nd = eqs_eq_equiv (get_node_eqs nd)
+
(* Create a tuple of right dimension, according to [expr] type, *)
(* filled with variable [v] *)
let adjust_tuple v expr =
@@ -624,6 +631,9 @@ let add_external_dependency outputs mems g =
ISet.iter (fun m -> IdentDepGraph.add_edge g world m) mems;
end
+(* Takes a node and return a pair (node', graph) where node' is node
+ rebuilt with the equations enriched with new ones introduced to
+ "break cycles" *)
let global_dependency node =
let mems = ExprDep.node_memory_variables node in
let inputs =
diff --git a/src/checks/stateless.ml b/src/checks/stateless.ml
index efceddd46ecdecf1a63738995ff655e55b02c82d..e58bb639d7b5f40fbdaec54b5938ed04cc699348 100644
--- a/src/checks/stateless.ml
+++ b/src/checks/stateless.ml
@@ -76,17 +76,28 @@ let force_prog decls =
List.iter (fun td -> ignore (force_node td)) decls
let check_compat_decl decl =
- match decl.top_decl_desc with
- | ImportedNode nd ->
- let td = Corelang.node_from_name nd.nodei_id in
- (match td.top_decl_desc with
- | Node nd' -> let stateless = check_node td in
- if nd.nodei_stateless && (not stateless)
- then raise (Error (td.top_decl_loc, Stateful_imp nd.nodei_id))
- else nd'.node_dec_stateless <- nd.nodei_stateless
- | _ -> assert false)
- | Node _ -> assert false
- | _ -> ()
+ match decl.top_decl_desc with
+ | ImportedNode nd -> (* A node declared in the header (lusi) shall
+ be locally defined with compatible stateless
+ flag *)
+ begin
+ let td = Corelang.node_from_name nd.nodei_id in
+ (match td.top_decl_desc with
+ | Node nd' -> let stateless = check_node td in
+ if nd.nodei_stateless && (not stateless)
+ then raise (Error (td.top_decl_loc, Stateful_imp nd.nodei_id))
+ else nd'.node_dec_stateless <- nd.nodei_stateless
+ | _ -> assert false)
+ end
+ | Node nd -> (
+ match nd.node_spec with
+ Some (Contract _) -> (* A contract element in a header does not
+ need to be provided in the associed lus
+ file *)
+ ()
+ | _ -> assert false)
+
+ | _ -> ()
let check_compat header =
List.iter check_compat_decl header
diff --git a/src/clock_calculus.ml b/src/clock_calculus.ml
index cee0793345a7647fe9aa5b54456fa54e2201d6b0..520704efc3f2c26bb8d4c3a40f08deebe96d2359 100644
--- a/src/clock_calculus.ml
+++ b/src/clock_calculus.ml
@@ -794,10 +794,17 @@ let uneval_prog_generics prog =
let check_env_compat header declared computed =
uneval_prog_generics header;
- Env.iter declared (fun k decl_clock_k ->
- let computed_c = instantiate (ref []) (ref []) (Env.lookup_value computed k) in
- try_semi_unify decl_clock_k computed_c Location.dummy_loc
- )
+ Env.iter declared (fun k decl_clock_k ->
+ try
+ let computed_c = instantiate (ref []) (ref []) (Env.lookup_value computed k) in
+ try_semi_unify decl_clock_k computed_c Location.dummy_loc
+ with Not_found -> (* If the lookup failed then either an actual
+ required element should have been declared
+ and is missing but typing should have catch
+ it, or it was a contract and does not
+ require this additional check. *)
+ ()
+ )
(* Local Variables: *)
(* compile-command:"make -C .." *)
(* End: *)
diff --git a/src/compiler_common.ml b/src/compiler_common.ml
index 40c2ff2a49f2d474ffb350b8d47582354f800564..2e347c31b9a9f7be06a16a4c6772f63139a93c87 100644
--- a/src/compiler_common.ml
+++ b/src/compiler_common.ml
@@ -187,7 +187,182 @@ let check_compatibility (prog, computed_types_env, computed_clocks_env) (header,
Location.pp_loc loc;
raise exc
+(* Process each node/imported node and introduce the associated contract node *)
+let resolve_contracts prog =
+ (* Bind a fresh node with a new name according to existing nodes and freshly binded contract node. Clean the contract to remove the stmts *)
+ let process_contract new_contracts prog c =
+ (* Resolve first the imports *)
+ let stmts, locals, c =
+ List.fold_left (
+ fun (stmts, locals, c) import ->
+ (* Search for contract in prog.
+ The node have to be processed already. Otherwise raise an error.
+ Each stmts in injected with a fresh name
+ Inputs are renamed and associated to the expression in1
+ Same thing for outputs.
+ Last the contracts elements are replaced with the renamed vars and merged with c contract.
+ *)
+ let name = import.import_nodeid in
+ assert false; (* TODO: we do not handle imports yet. The
+ algorithm is sketched below *)
+ (*
+ try
+ let imp_nd = xxx in (* Get the contract node in prog *)
+ (* checking that it's actually a (processed) contract *)
+ let imp_c =
+ match imp_nd.node_spec with
+ Some (Contract imp_c) ->
+ if imp_c.imports = [] then
+ imp_c
+ else
+ assert false (* should be processed *)
+ | _ -> assert false (* should be a contract *)
+ in
+ (* Preparing vars: renaming them *)
+ let imp_in = rename imp_nd.node_inputs in
+ let imp_out = rename imp_nd.node_outputs in
+ let imp_locals = rename imp_nd.node_locals in
+ let locals = imp_in@imp_out@imp_locals@locals in
+ (* Assinging in and out *)
+ let in_assigns =
+ xxx imp_in = import.inputs
+ in
+ let out_assigns =
+ xxx imp_out = import.outputs
+ in
+ let stmts = stmts @ (rename imp_nd.stmts) in
+ let imp_c = rename imp_c in
+ let c = merge_contracts c imp_c in
+ stmts, locals, c
+ with Not_found -> raise (Error.Unbound_symbol ("contract " ^ name))
+
+ *)
+ ) ([], c.consts@c.locals, c) c.imports
+ in
+ (* Other contract elements will be normalized later *)
+ let c = { c with
+ locals = [];
+ consts = [];
+ stmts = [];
+ imports = []
+ }
+ in
+ stmts, locals, c
+
+ in
+ let process_contract_new_node accu_contracts prog top =
+ let id, spec, inputs, outputs =
+ match top.top_decl_desc with
+ | Node nd -> nd.node_id, nd.node_spec, nd.node_inputs, nd.node_outputs
+ | ImportedNode ind -> ind.nodei_id, ind.nodei_spec, ind.nodei_inputs, ind.nodei_outputs
+ | _ -> assert false
+ in
+ let stmts, locals, c =
+ match spec with
+ | None | Some (NodeSpec _) -> assert false
+ | Some (Contract c) ->
+ process_contract accu_contracts prog c
+ in
+ (* Create a fresh name *)
+ let used v = List.exists (fun top ->
+ match top.top_decl_desc with
+ | Node _
+ | ImportedNode _ ->
+ (node_name top) = v
+ | _ -> false
+ ) (accu_contracts@prog)
+ in
+ let new_nd_id = mk_new_name used (id ^ "_coco") in
+ let new_nd =
+ mktop_decl
+ c.spec_loc
+ top.top_decl_owner
+ top.top_decl_itf
+ (Node {
+ node_id = new_nd_id;
+ node_type = Types.new_var ();
+ node_clock = Clocks.new_var true;
+ node_inputs = inputs;
+ node_outputs = outputs;
+ node_locals = locals;
+ node_gencalls = [];
+ node_checks = [];
+ node_asserts = [];
+ node_stmts = stmts;
+ node_dec_stateless = false;
+ node_stateless = None;
+ node_spec = Some (Contract c);
+ node_annot = [];
+ node_iscontract = true;
+ }) in
+ new_nd
+ in
+ (* Processing nodes in order. Should have been sorted by now
+
+ Each top level contract is processed: stmts pushed in node
+
+ Each regular imported node or node associated with a contract is
+ replaced with a simplidfied contract and its contract is bound to
+ a fresh node.
+
+ *)
+ let new_contracts, prog =
+ List.fold_left
+ (
+ fun (accu_contracts, accu_nodes) top ->
+ match top.top_decl_desc with
+
+ | Node nd when nd.node_iscontract -> (
+ match nd.node_spec with
+ | None | Some (NodeSpec _) -> assert false
+ | Some (Contract c) ->
+ let stmts, locals, c = process_contract accu_contracts prog c in
+ let nd =
+ { nd with
+ node_locals = nd.node_locals @ locals;
+ node_stmts = nd.node_stmts @ stmts;
+ node_spec = Some (Contract c);
+ }
+ in
+ { top with top_decl_desc = Node nd }::accu_contracts,
+ accu_nodes
+
+ )
+ | Node nd -> (
+ match nd.node_spec with
+ | None -> accu_contracts, top::accu_nodes (* A boring node: no contract *)
+ | Some (NodeSpec id) -> (* shall not happen, its too early *)
+ assert false
+ | Some (Contract c) -> (* A contract: processing it *)
+ (* we bind a fresh node *)
+ let new_nd = process_contract_new_node accu_contracts prog top in
+ Format.eprintf "Creating new contract node %s@." (node_name new_nd);
+ let nd = { nd with node_spec = (Some (NodeSpec (node_name new_nd))) } in
+ new_nd::accu_contracts,
+ { top with top_decl_desc = Node nd }::accu_nodes
+
+ )
+
+ | ImportedNode ind -> ( (* Similar treatment for imported nodes *)
+ match ind.nodei_spec with
+ None -> accu_contracts, top::accu_nodes (* A boring node: no contract *)
+ | Some (NodeSpec id) -> (* shall not happen, its too early *)
+ assert false
+ | Some (Contract c) -> (* A contract: processing it *)
+ (* we bind a fresh node *)
+ let new_nd = process_contract_new_node accu_contracts prog top in
+ let ind = { ind with nodei_spec = (Some (NodeSpec (node_name new_nd))) } in
+ new_nd::accu_contracts,
+ { top with top_decl_desc = ImportedNode ind }::accu_nodes
+ )
+ | _ -> accu_contracts, top::accu_nodes
+ ) ([],[]) prog
+ in
+ (List.rev new_contracts) @ (List.rev prog)
+
+
+
let track_exception () =
if !Options.track_exceptions
then (Printexc.print_backtrace stdout; flush stdout)
diff --git a/src/compiler_stages.ml b/src/compiler_stages.ml
index a6ac627223cb5be28bf23d10457f7afd6c74fbb4..bc7923a4561d74e4679d3d6a4b6fda0620482484 100644
--- a/src/compiler_stages.ml
+++ b/src/compiler_stages.ml
@@ -78,6 +78,9 @@ let stage1 params prog dirname basename extension =
(* Sorting nodes *)
let prog = SortProg.sort prog in
+ (* Consolidating contracts *)
+ let prog = resolve_contracts prog in
+
(* Perform inlining before any analysis *)
let orig, prog =
if !Options.global_inline && !Options.main_node <> "" then
diff --git a/src/corelang.ml b/src/corelang.ml
index cd57e20c021f8f9fb07e93d1bc3166e03b412ec5..561c2e9e525998d84cd50656ca8ed7f7b3adb33d 100644
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -324,6 +324,15 @@ let is_imported_node td =
| ImportedNode nd -> true
| _ -> assert false
+let is_contract td =
+ match td.top_decl_desc with
+ | Node nd -> (
+ match nd.node_spec with
+ | Some (Contract _) -> true
+ | _ -> false
+ )
+ | _ -> false
+
(* alias and type definition table *)
@@ -855,6 +864,7 @@ and rename_eexpr f_node f_var ee =
node_stateless = nd.node_stateless;
node_spec = spec;
node_annot = annot;
+ node_iscontract = nd.node_iscontract;
}
@@ -1255,6 +1265,9 @@ let find_eq xl eqs =
in
aux [] eqs
+
+
+
(* Local Variables: *)
(* compile-command:"make -C .." *)
(* End: *)
diff --git a/src/corelang.mli b/src/corelang.mli
index 77ded12a878e37c449d56b1c8a9895433bf06b71..fc099b5006b694a5cbf60cecd76c28464205a394 100644
--- a/src/corelang.mli
+++ b/src/corelang.mli
@@ -58,7 +58,8 @@ val node_from_name: ident -> top_decl
val update_node: ident -> top_decl -> unit
val is_generic_node: top_decl -> bool
val is_imported_node: top_decl -> bool
-
+val is_contract: top_decl -> bool
+
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
@@ -167,7 +168,7 @@ val mk_contract_var: ident -> bool -> type_dec option -> expr -> Location.t -> c
val mk_contract_guarantees: eexpr -> contract_desc
val mk_contract_assume: eexpr -> contract_desc
val mk_contract_mode: ident -> eexpr list -> eexpr list -> Location.t -> contract_desc
-val mk_contract_import: ident -> expr list -> expr list -> Location.t -> contract_desc
+val mk_contract_import: ident -> expr -> expr -> Location.t -> contract_desc
val merge_contracts: contract_desc -> contract_desc -> contract_desc
val extend_eexpr: (quantifier_type * var_decl list) list -> eexpr -> eexpr
val update_expr_annot: ident -> expr -> expr_annot -> expr
diff --git a/src/error.ml b/src/error.ml
index 1ec7b9e6a89250a65d0904262da028b93afee28b..507b9948490a7a5316a886d27dd3b2871b2eec07 100644
--- a/src/error.ml
+++ b/src/error.ml
@@ -24,6 +24,7 @@ let return_code kind =
| AlgebraicLoop -> 9
| LoadError _ -> 10
+
let pp_error_msg fmt = function
| Main_not_found ->
fprintf fmt "Could not find the definition of main node %s.@."
diff --git a/src/inliner.ml b/src/inliner.ml
index 06923735bbf0820193bf39e68e3653f8d719f4de..8e4f2988b854c281638c9df8c8a7bf9caf46a225 100644
--- a/src/inliner.ml
+++ b/src/inliner.ml
@@ -421,9 +421,14 @@ let witness filename main_name orig inlined type_env clock_env =
node_dec_stateless = false;
node_stateless = None;
node_spec = Some
- (mk_contract_guarantees (mkeexpr loc (mkexpr loc (Expr_ident ok_ident))));
- node_annot = [];
- }
+ (Contract
+ (mk_contract_guarantees
+ (mkeexpr loc (mkexpr loc (Expr_ident ok_ident)))
+ )
+ );
+ node_annot = [];
+ node_iscontract = true;
+ }
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
diff --git a/src/lustre_types.ml b/src/lustre_types.ml
index 829a93445698b9ffc355fcac0d42b309a97056b2..b19566444216b1f62d852a3dd13bfdaabb58493e 100644
--- a/src/lustre_types.ml
+++ b/src/lustre_types.ml
@@ -129,7 +129,10 @@ type contract_mode =
{ mode_id: ident; require: eexpr list; ensure: eexpr list; mode_loc: Location.t}
type contract_import =
- { import_nodeid: ident; inputs: expr list; outputs: expr list; import_loc: Location.t }
+ { import_nodeid: ident;
+ inputs: expr;
+ outputs: expr;
+ import_loc: Location.t }
@@ -174,6 +177,9 @@ type contract_desc =
spec_loc: Location.t;
}
+type node_spec_t = Contract of contract_desc
+ | NodeSpec of ident
+
type node_desc =
{node_id: ident;
mutable node_type: Types.type_expr;
@@ -187,8 +193,9 @@ type node_desc =
node_stmts: statement list;
mutable node_dec_stateless: bool;
mutable node_stateless: bool option;
- node_spec: contract_desc option;
+ node_spec: node_spec_t option;
node_annot: expr_annot list;
+ node_iscontract: bool;
}
type imported_node_desc =
@@ -198,7 +205,7 @@ type imported_node_desc =
nodei_inputs: var_decl list;
nodei_outputs: var_decl list;
nodei_stateless: bool;
- nodei_spec: contract_desc option;
+ nodei_spec: node_spec_t option;
(* nodei_annot: expr_annot list; *)
nodei_prototype: string option;
nodei_in_lib: string list;
@@ -213,14 +220,14 @@ type const_desc =
type top_decl_desc =
-| Node of node_desc
-| Const of const_desc
-| ImportedNode of imported_node_desc
-| Open of bool * string (* the boolean set to true denotes a local
+ | Node of node_desc
+ | Const of const_desc
+ | ImportedNode of imported_node_desc
+ | Open of bool * string (* the boolean set to true denotes a local
lusi vs a lusi installed at system level *)
-| Include of string (* the boolean set to true denotes a local
+ | Include of string (* the boolean set to true denotes a local
lus vs a lus installed at system level *)
-| TypeDef of typedef_desc
+ | TypeDef of typedef_desc
type top_decl =
{top_decl_desc: top_decl_desc; (* description of the symbol *)
@@ -237,6 +244,10 @@ type dep_t = {
is_stateful: bool
}
+type spec_types =
+ | LocalContract of contract_desc
+ | TopContract of top_decl list
+
(* Local Variables: *)
diff --git a/src/machine_code.ml b/src/machine_code.ml
index 5b995ae3ea75e719a919a223c98e7e017dd32da9..d789639c631597b611803f202575797a59970d26 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -375,6 +375,7 @@ let translate_core sorted_eqs locals other_vars =
ctx, ctx0.s
+
let translate_decl nd sch =
(* Extracting eqs, variables .. *)
let eqs, auts = get_node_eqs nd in
@@ -395,36 +396,9 @@ let translate_decl nd sch =
let sorted_eqs = Scheduling.sort_equations_from_schedule eqs schedule in
let ctx, ctx0_s = translate_core (assert_instrs@sorted_eqs) locals inout_vars in
-(* CODE QUI MARCHE
- let constant_eqs = constant_equations locals in
- (* Compute constants' instructions *)
- let ctx0 = translate_eqs env ctx_init constant_eqs in
- assert (VSet.is_empty ctx0.m);
- assert (ctx0.si = []);
- assert (Utils.IMap.is_empty ctx0.j);
-
- (* Compute ctx for all eqs *)
- let ctx = translate_eqs env ctx_init (assert_instrs@sorted_eqs) in
- *)
- (*
- (* Processing spec: locals would be actual locals of the spec while
- non locals would be inputs/ouptpus of the node. Locals of the
- node are not visible. *)
- let spec =
- match nd.node_spec with
- | None -> None
- | Some spec -> translate_spec inout_vars spec
- in
-
-
- inout_vars spec =
- let locals = VSet.of_list spec.locals in
- let spec_consts = VSet.of_list spec.consts in
- let other_spec_vars = VSet.union inout_vars spec_consts in
- let spec_env = build_env spec_locals other_spec_vars in
- *)
+
let mmap = Utils.IMap.elements ctx.j in
{
mname = nd;
@@ -454,6 +428,12 @@ let translate_decl nd sch =
);
step_asserts = List.map (translate_expr env) nd_node_asserts;
};
+
+ (* Processing spec: there is no processing performed here. Contract
+ have been processed already. Either one of the other machine is a
+ cocospec node, or the current one is a cocospec node. Contract do
+ not contain any statement or import. *)
+
mspec = nd.node_spec;
mannot = nd.node_annot;
msch = Some sch;
@@ -462,13 +442,15 @@ let translate_decl nd sch =
(** 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
+ let machines =
+ List.map
(fun decl ->
let node = node_of_top decl in
let sch = Utils.IMap.find node.node_id node_schs in
translate_decl node sch
) nodes
-
+ in
+ machines
(* Local Variables: *)
(* compile-command:"make -C .." *)
diff --git a/src/machine_code.mli b/src/machine_code.mli
index aaeab7c2e9f2ba0bf93f6c4463764c8130859306..f646b982850e10b60a1caa0b720b4ed7f6e9ac35 100644
--- a/src/machine_code.mli
+++ b/src/machine_code.mli
@@ -1 +1,4 @@
-val translate_prog: Lustre_types.program_t -> Scheduling_type.schedule_report Utils.IMap.t -> Machine_code_types.machine_t list
+val translate_prog:
+ Lustre_types.program_t ->
+ Scheduling_type.schedule_report Utils.IMap.t ->
+ Machine_code_types.machine_t list
diff --git a/src/machine_code_common.ml b/src/machine_code_common.ml
index f784d10fedac9a85d844a104bac44921b33bc7f0..8612bc62a21b2852a8846099090a2e9573f98f88 100644
--- a/src/machine_code_common.ml
+++ b/src/machine_code_common.ml
@@ -105,7 +105,9 @@ let pp_machine fmt m =
(Utils.fprintf_list ~sep:"@ " (pp_instr m)) m.minit
(Utils.fprintf_list ~sep:"@ " (pp_instr m)) m.mconst
(pp_step m) m.mstep
- (fun fmt -> match m.mspec with | None -> () | Some spec -> Printers.pp_spec fmt spec)
+ (fun fmt -> match m.mspec with | None -> ()
+ | Some (NodeSpec id) -> Format.fprintf fmt "cocospec: %s" id
+ | Some (Contract spec) -> Printers.pp_spec fmt spec)
(Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot
let pp_machines fmt ml =
@@ -190,7 +192,9 @@ let empty_desc =
node_dec_stateless = true;
node_stateless = Some true;
node_spec = None;
- node_annot = []; }
+ node_annot = [];
+ node_iscontract = false;
+}
let empty_machine =
{
diff --git a/src/machine_code_types.ml b/src/machine_code_types.ml
index 4d962b66e284c8c3419905744a3eb610c59abbe4..1283f39658520789b777698ce5bf36a2ce26ed45 100644
--- a/src/machine_code_types.ml
+++ b/src/machine_code_types.ml
@@ -30,18 +30,18 @@ and instr_t_desc =
| MBranch of value_t * (label * instr_t list) list
| MComment of string
- type step_t = {
- step_checks: (Location.t * value_t) list;
- step_inputs: var_decl list;
- step_outputs: var_decl list;
- step_locals: var_decl list;
- step_instrs: instr_t list;
- step_asserts: value_t list;
-}
+type step_t = {
+ step_checks: (Location.t * value_t) list;
+ step_inputs: var_decl list;
+ step_outputs: var_decl list;
+ step_locals: var_decl list;
+ step_instrs: instr_t list;
+ step_asserts: value_t list;
+ }
type static_call = top_decl * (Dimension.dim_expr list)
-
+
type machine_t = {
mname: node_desc;
mmemory: var_decl list;
@@ -51,7 +51,7 @@ type machine_t = {
mstatic: var_decl list; (* static inputs only *)
mconst: instr_t list; (* assignments of node constant locals *)
mstep: step_t;
- mspec: contract_desc option;
+ mspec: node_spec_t option;
mannot: expr_annot list;
msch: Scheduling_type.schedule_report option; (* Equations scheduling *)
}
diff --git a/src/modules.ml b/src/modules.ml
index 7cf8ce46c08434fcf8084a2c1569360c517a4a87..548b0e0591de54cba427f0de5eed5a10a8e1ca7b 100644
--- a/src/modules.ml
+++ b/src/modules.ml
@@ -49,7 +49,7 @@ let add_node name value =
let itf = value.top_decl_itf in
match value'.top_decl_desc, value.top_decl_desc with
| ImportedNode _, Node _ when owner = owner' && itf' && (not itf) -> ()
- | Node _ , Node _ -> raise (Error (value.top_decl_loc, Error.Already_bound_symbol ("node " ^ name)))
+ | Node _ , Node _ -> assert false; raise (Error (value.top_decl_loc, Error.Already_bound_symbol ("node " ^ name)))
| _ -> assert false
with
Not_found -> update_node name value
diff --git a/src/normalization.ml b/src/normalization.ml
index ca5cfd76c3e2905c8aeddc2d86e7fcf8a76a9d50..710262156736193e63ef0cd232f0de9afaf597a5 100644
--- a/src/normalization.ml
+++ b/src/normalization.ml
@@ -554,7 +554,7 @@ let normalize_pred_eexpr decls norm_ctx (def,vars) ee =
(* We use node local vars to make sure we are creating fresh variables *)
let normalize_spec decls parentid (in_vars, out_vars, l_vars) s =
- (* Original set of variables actually visible from here: iun/out and
+ (* Original set of variables actually visible from here: in/out and
spec locals (no node locals) *)
let orig_vars = in_vars @ out_vars @ s.locals in
let not_is_orig_var v =
@@ -593,11 +593,10 @@ let normalize_spec decls parentid (in_vars, out_vars, l_vars) s =
in
let new_locals = List.filter not_is_orig_var vars in (* removing inouts and initial locals ones *)
-
-
+ new_locals, defs,
{s with
locals = s.locals @ new_locals;
- stmts = List.map (fun eq -> Eq eq) defs;
+ stmts = [];
assume = assume';
guarantees = guarantees';
modes = modes'
@@ -644,15 +643,35 @@ let normalize_node decls node =
is_output = (fun vid -> List.exists (fun v -> v.var_id = vid) node.node_outputs);
}
in
-
+
+ let eqs, auts = get_node_eqs node in
+ if auts != [] then assert false; (* Automata should be expanded by now. *)
+ let spec, new_vars, eqs =
+ begin
+ (* Update mutable fields of eexpr to perform normalization of
+ specification.
+
+ Careful: we do not normalize annotations, since they can have the form
+ x = (a, b, c) *)
+ match node.node_spec with
+ | None
+ | Some (NodeSpec _) -> node.node_spec, [], eqs
+ | Some (Contract s) ->
+ let new_locals, new_stmts, s' = normalize_spec
+ decls
+ node.node_id
+ (node.node_inputs, node.node_outputs, node.node_locals)
+ s
+ in
+ Some (Contract s'), new_locals, new_stmts@eqs
+ end
+ in
let defs, vars =
- let eqs, auts = get_node_eqs node in
- if auts != [] then assert false; (* Automata should be expanded by now. *)
- List.fold_left (normalize_eq norm_ctx) ([], orig_vars) eqs in
+ List.fold_left (normalize_eq norm_ctx) ([], new_vars@orig_vars) eqs in
(* Normalize the asserts *)
let vars, assert_defs, asserts =
List.fold_left (
- fun (vars, def_accu, assert_accu) assert_ ->
+ fun (vars, def_accu, assert_accu) assert_ ->
let assert_expr = assert_.assert_expr in
let (defs, vars'), expr =
normalize_expr
@@ -662,9 +681,9 @@ let normalize_node decls node =
([], vars) (* defvar only contains vars *)
assert_expr
in
- (*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*)
+ (*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*)
vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
- ) (vars, [], []) node.node_asserts in
+ ) (vars, [], []) node.node_asserts in
let new_locals = List.filter not_is_orig_var vars in (* we filter out inout
vars and initial locals ones *)
@@ -679,29 +698,29 @@ let normalize_node decls node =
(* Compute traceability info:
- gather newly bound variables
- compute the associated expression without aliases
- *)
+ *)
let new_annots =
if !Options.traces then
begin
let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) all_locals in
let norm_traceability = {
- annots = List.map (fun v ->
- let eq =
- try
- List.find (fun eq -> List.exists (fun v' -> v' = v.var_id ) eq.eq_lhs) (defs@assert_defs)
- with Not_found ->
- (
- Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id;
- assert false
- )
- in
- let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
- let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
- Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"];
- (["traceability"], pair)
- ) diff_vars;
- annot_loc = Location.dummy_loc
- }
+ annots = List.map (fun v ->
+ let eq =
+ try
+ List.find (fun eq -> List.exists (fun v' -> v' = v.var_id ) eq.eq_lhs) (defs@assert_defs)
+ with Not_found ->
+ (
+ Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id;
+ assert false
+ )
+ in
+ let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
+ let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
+ Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"];
+ (["traceability"], pair)
+ ) diff_vars;
+ annot_loc = Location.dummy_loc
+ }
in
norm_traceability::node.node_annot
end
@@ -711,33 +730,23 @@ let normalize_node decls node =
let new_annots =
List.fold_left (fun annots v ->
- if Machine_types.is_active && Machine_types.is_exportable v then
- let typ = Machine_types.get_specified_type v in
- let typ_name = Machine_types.type_name typ in
-
- let loc = v.var_loc in
- let typ_as_string =
- mkexpr
- loc
- (Expr_const
- (Const_string typ_name))
- in
- let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in
- Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword;
- {annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots
- else
- annots
- ) new_annots new_locals
- in
- let spec =
- begin
- (* Update mutable fields of eexpr to perform normalization of
- specification.
-
- Careful: we do not normalize annotations, since they can have the form
- x = (a, b, c) *)
- match node.node_spec with None -> None | Some s -> Some (normalize_spec decls node.node_id (node.node_inputs, node.node_outputs, node.node_locals) s)
- end
+ if Machine_types.is_active && Machine_types.is_exportable v then
+ let typ = Machine_types.get_specified_type v in
+ let typ_name = Machine_types.type_name typ in
+
+ let loc = v.var_loc in
+ let typ_as_string =
+ mkexpr
+ loc
+ (Expr_const
+ (Const_string typ_name))
+ in
+ let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in
+ Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword;
+ {annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots
+ else
+ annots
+ ) new_annots new_locals
in
@@ -750,17 +759,15 @@ let normalize_node decls node =
node_spec = spec;
}
in ((*Printers.pp_node Format.err_formatter node;*)
- node
- )
+ node
+ )
let normalize_inode decls nd =
reset_cpt_fresh ();
match nd.nodei_spec with
- None -> nd
- | Some s ->
- let s = normalize_spec decls nd.nodei_id (nd.nodei_inputs, nd.nodei_outputs, []) s in
- { nd with nodei_spec = Some s }
-
+ None | Some (NodeSpec _) -> nd
+ | Some (Contract _) -> assert false
+
let normalize_decl (decls: program_t) (decl: top_decl) : top_decl =
match decl.top_decl_desc with
| Node nd ->
diff --git a/src/parsers/lexerLustreSpec.mll b/src/parsers/lexerLustreSpec.mll
index dffeedbe38c01e57fa7fa25038ca0dfbf35e4a9a..e4ef79b06ba1aa6090fbb51ff564a8bffb627b02 100644
--- a/src/parsers/lexerLustreSpec.mll
+++ b/src/parsers/lexerLustreSpec.mll
@@ -40,6 +40,7 @@ let keyword_table =
"tel", TEL;
"returns", RETURNS;
"var", VAR;
+ "import", IMPORT;
"imported", IMPORTED;
"int", TINT;
"bool", TBOOL;
diff --git a/src/parsers/lexer_lustre.mll b/src/parsers/lexer_lustre.mll
index f9727e9c434ed5810acd49e4b93619f697359f71..5d81cff71ad64a8df17927305fb07ae66991e046 100644
--- a/src/parsers/lexer_lustre.mll
+++ b/src/parsers/lexer_lustre.mll
@@ -41,6 +41,7 @@ let keyword_table =
"returns", RETURNS;
"var", VAR;
"imported", IMPORTED;
+ "import", IMPORT;
"type", TYPE;
"int", TINT;
"bool", TBOOL;
diff --git a/src/parsers/parserLustreSpec.mly b/src/parsers/parserLustreSpec.mly
index 8fb24bfb0c022494d427b9537f76640c970fc6f6..2be9d71f58706811c17d823636bba9f76fac0446 100644
--- a/src/parsers/parserLustreSpec.mly
+++ b/src/parsers/parserLustreSpec.mly
@@ -95,7 +95,7 @@ contract:
{ Guarantees($2)::$4 }
| MODE ident LPAR mode_content RPAR SCOL contract
{ Mode($2,$4)::$7 }
-| IMPORT ident LPAR tuple_expr RPAR returns LPAR tuple_expr RPAR SCOL contract
+| IMPORT ident LPAR expr RPAR returns LPAR expr RPAR SCOL contract
{ Import($2, $4, $8)::$11 }
diff --git a/src/parsers/parser_lustre.mly b/src/parsers/parser_lustre.mly
index 3befe345abf9280c2858c532e63bdbda5303d7de..31323d7b89c3dc3538f792a5df8bbb35c7740a33 100644
--- a/src/parsers/parser_lustre.mly
+++ b/src/parsers/parser_lustre.mly
@@ -49,7 +49,8 @@ let rec fby expr n init =
mkexpr (Expr_arrow (init, mkexpr (Expr_pre expr)))
else
mkexpr (Expr_arrow (init, mkexpr (Expr_pre (fby expr (n-1) init))))
-
+
+
%}
%token <int> INT
@@ -62,7 +63,7 @@ let rec fby expr n init =
%token <string> UIDENT
%token TRUE FALSE
%token <Lustre_types.expr_annot> ANNOT
-%token <Lustre_types.contract_desc> NODESPEC
+%token <Lustre_types.spec_types> NODESPEC
%token LBRACKET RBRACKET LCUR RCUR LPAR RPAR SCOL COL COMMA COLCOL
%token AMPERAMPER BARBAR NOT POWER
%token IF THEN ELSE
@@ -113,7 +114,7 @@ let rec fby expr n init =
%type <Lustre_types.expr_annot> lustre_annot
%start lustre_spec
-%type <Lustre_types.contract_desc> lustre_spec
+%type <Lustre_types.spec_types> lustre_spec
%start signed_const
%type <Lustre_types.constant> signed_const
@@ -203,32 +204,25 @@ state_annot:
top_decl_header:
| CONST cdecl_list { List.rev ($2 true) }
-| nodespec_list state_annot node_ident LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR prototype_opt in_lib_list SCOL
- {let nd = mktop_decl true (ImportedNode
+| nodespecs state_annot node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR prototype_opt in_lib_list SCOL
+ {
+ let inputs = List.rev $5 in
+ let outputs = List.rev $10 in
+ let nd = mktop_decl true (ImportedNode
{nodei_id = $3;
nodei_type = Types.new_var ();
nodei_clock = Clocks.new_var true;
- nodei_inputs = List.rev $5;
- nodei_outputs = List.rev $10;
+ nodei_inputs = inputs;
+ nodei_outputs = outputs;
nodei_stateless = $2;
nodei_spec = $1;
nodei_prototype = $13;
nodei_in_lib = $14;})
in
- (*add_imported_node $3 nd;*) [nd] }
-| CONTRACT node_ident LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt LET contract TEL
- {let nd = mktop_decl true (ImportedNode
- {nodei_id = $2;
- nodei_type = Types.new_var ();
- nodei_clock = Clocks.new_var true;
- nodei_inputs = List.rev $4;
- nodei_outputs = List.rev $9;
- nodei_stateless = false (* By default we assume contracts as stateful *);
- nodei_spec = Some $14;
- nodei_prototype = None;
- nodei_in_lib = [];})
- in
- (*add_imported_node $3 nd;*) [nd] }
+ pop_node ();
+ [nd] }
+| top_contract { [$1] }
+
prototype_opt:
{ None }
@@ -240,7 +234,7 @@ in_lib_list:
top_decl:
| CONST cdecl_list { List.rev ($2 false) }
-| state_annot node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt nodespec_list locals LET stmt_list TEL
+| state_annot node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt nodespecs locals LET stmt_list TEL
{
let stmts, asserts, annots = $16 in
(* Declaring eqs annots *)
@@ -249,13 +243,15 @@ top_decl:
Annotations.add_node_ann $2 key
) ann.annots
) annots;
- (* Building the node *)
+ (* Building the node *)
+ let inputs = List.rev $4 in
+ let outputs = List.rev $9 in
let nd = mktop_decl false (Node
{node_id = $2;
node_type = Types.new_var ();
node_clock = Clocks.new_var true;
- node_inputs = List.rev $4;
- node_outputs = List.rev $9;
+ node_inputs = inputs;
+ node_outputs = outputs;
node_locals = List.rev $14;
node_gencalls = [];
node_checks = [];
@@ -264,46 +260,36 @@ top_decl:
node_dec_stateless = $1;
node_stateless = None;
node_spec = $13;
- node_annot = annots})
+ node_annot = annots;
+ node_iscontract = false;
+ })
in
pop_node ();
(*add_node $3 nd;*) [nd] }
-| state_annot IMPORTED node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt LET contract TEL
- {let nd = mktop_decl true (ImportedNode
- {nodei_id = $3;
- nodei_type = Types.new_var ();
- nodei_clock = Clocks.new_var true;
- nodei_inputs = List.rev $5;
- nodei_outputs = List.rev $10;
- nodei_stateless = $1;
- nodei_spec = Some $15;
- nodei_prototype = None;
- nodei_in_lib = [];})
- in
- pop_node ();
- (*add_imported_node $3 nd;*) [nd] }
-| state_annot IMPORTED node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL
- {let nd = mktop_decl true (ImportedNode
- {nodei_id = $3;
- nodei_type = Types.new_var ();
- nodei_clock = Clocks.new_var true;
- nodei_inputs = List.rev $5;
- nodei_outputs = List.rev $10;
- nodei_stateless = $1;
- nodei_spec = None;
- nodei_prototype = None;
- nodei_in_lib = [];})
- in
- pop_node ();
- (*add_imported_node $3 nd;*) [nd] }
+
+| NODESPEC
+ { match $1 with
+ | LocalContract c -> assert false
+ | TopContract c -> c
+
+ }
+
+nodespecs:
+nodespec_list {
+ match $1 with
+ | None -> None
+ | Some c -> Some (Contract c)
+}
nodespec_list:
{ None }
-| NODESPEC nodespec_list {
- (function
- | None -> (fun s1 -> Some s1)
- | Some s2 -> (fun s1 -> Some (merge_contracts s1 s2))) $2 $1 }
+ | NODESPEC nodespec_list {
+ let extract x = match x with LocalContract c -> c | _ -> assert false in
+ let s1 = extract $1 in
+ match $2 with
+ | None -> Some s1
+ | Some s2 -> Some (merge_contracts s1 s2) }
typ_def_list:
/* empty */ { (fun itf -> []) }
@@ -382,26 +368,58 @@ eq:
| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev (List.map fst $2), $5)}
lustre_spec:
-| contract EOF { $1 }
+| top_contracts EOF { TopContract $1 }
+| contract_content EOF { LocalContract $1}
+
+top_contracts:
+| top_contract { [$1] }
+| top_contract top_contracts { $1::$2 }
+
+top_contract:
+| CONTRACT node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt LET contract_content TEL
+ {
+ let nd = mktop_decl true (Node
+ {node_id = $2;
+ node_type = Types.new_var ();
+ node_clock = Clocks.new_var true;
+ node_inputs = List.rev $4;
+ node_outputs = List.rev $9;
+ node_locals = []; (* will be filled later *)
+ node_gencalls = [];
+ node_checks = [];
+ node_asserts = [];
+ node_stmts = []; (* will be filled later *)
+ node_dec_stateless = false;
+ (* By default we assume contracts as stateful *)
+ node_stateless = None;
+ node_spec = Some (Contract $14);
+ node_annot = [];
+ node_iscontract = true;
+ }
+ )
+ in
+ pop_node ();
+ (*add_imported_node $3 nd;*)
+ nd }
-contract:
+contract_content:
{ empty_contract }
-| CONTRACT contract { $2 }
-| CONST IDENT EQ expr SCOL contract
+| CONTRACT contract_content { $2 }
+| CONST IDENT EQ expr SCOL contract_content
{ merge_contracts (mk_contract_var $2 true None $4 (get_loc())) $6 }
-| CONST IDENT COL typeconst EQ expr SCOL contract
+| CONST IDENT COL typeconst EQ expr SCOL contract_content
{ merge_contracts (mk_contract_var $2 true (Some(mktyp $4)) $6 (get_loc())) $8 }
-| VAR IDENT COL typeconst EQ expr SCOL contract
+| VAR IDENT COL typeconst EQ expr SCOL contract_content
{ merge_contracts (mk_contract_var $2 false (Some(mktyp $4)) $6 (get_loc())) $8 }
-| ASSUME qexpr SCOL contract
+| ASSUME qexpr SCOL contract_content
{ merge_contracts (mk_contract_assume $2) $4 }
-| GUARANTEES qexpr SCOL contract
+| GUARANTEES qexpr SCOL contract_content
{ merge_contracts (mk_contract_guarantees $2) $4 }
-| MODE IDENT LPAR mode_content RPAR SCOL contract
+| MODE IDENT LPAR mode_content RPAR SCOL contract_content
{ merge_contracts (
let r, e = $4 in
mk_contract_mode $2 r e (get_loc())) $7 }
-| IMPORT IDENT LPAR tuple_expr RPAR RETURNS LPAR tuple_expr RPAR SCOL contract
+| IMPORT IDENT LPAR expr RPAR RETURNS LPAR expr RPAR SCOL contract_content
{ merge_contracts (mk_contract_import $2 $4 $8 (get_loc())) $11 }
mode_content:
diff --git a/src/printers.ml b/src/printers.ml
index a0f7881ebae7b5b2f3e03081d658bf7c00b07c77..51ceca36373f98add0db8ed188de2976a54f96a7 100644
--- a/src/printers.ml
+++ b/src/printers.ml
@@ -323,15 +323,51 @@ let pp_spec fmt spec =
fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt import ->
fprintf fmt "import %s (%a) returns (%a);"
import.import_nodeid
- (fprintf_list ~sep:"@ " pp_expr) import.inputs
- (fprintf_list ~sep:"@ " pp_expr) import.outputs
+ pp_expr import.inputs
+ pp_expr import.outputs
) fmt spec.imports
-let pp_spec_as_comment fmt spec =
- fprintf fmt "@[<hov 2>(*@@ ";
- pp_spec fmt spec;
- fprintf fmt "@]*)@ "
+
+ let node_as_contract nd =
+ match nd.node_spec with
+ | None | Some (NodeSpec _) -> raise (Invalid_argument "Not a contract")
+ | Some (Contract c) -> (
+ assert (c.locals = []);
+ assert (c.stmts = []);
+ { c with
+ locals = nd.node_locals;
+ stmts = nd.node_stmts;
+ }
+ )
+
+let pp_contract fmt nd =
+ let c = node_as_contract nd in
+ let pp_l = fprintf_list ~sep:"," pp_var_name in
+ fprintf fmt "@[<hov 2>(*@@ contract %s(%a) returns (%a);@ "
+ nd.node_id
+ pp_l nd.node_inputs
+ pp_l nd.node_outputs;
+ fprintf fmt "let@ ";
+ pp_spec fmt c;
+ fprintf fmt "tel@ @]*)@ "
+let pp_spec_as_comment fmt (inl, outl, spec) =
+ match spec with
+ | Contract c -> (* should have been processed by now *)
+ fprintf fmt "@[<hov 2>(*@@ ";
+ pp_spec fmt c;
+ fprintf fmt "@]*)@ "
+
+ | NodeSpec name -> (* Pushing stmts in contract. We update the
+ original information with the computed one in
+ nd. *)
+ let pp_l = fprintf_list ~sep:"," pp_var_name in
+ fprintf fmt "@[<hov 2>(*@@ contract import %s(%a) returns (%a)@]*)@ "
+ name
+ pp_l inl
+ pp_l outl
+
+
let pp_node fmt nd =
fprintf fmt "@[<v 0>";
(* Prototype *)
@@ -342,7 +378,7 @@ let pp_node fmt nd =
pp_node_args nd.node_outputs;
(* Contracts *)
fprintf fmt "%a%t"
- (fun fmt s -> match s with Some s -> pp_spec_as_comment fmt s | _ -> ()) nd.node_spec
+ (fun fmt s -> match s with Some s -> pp_spec_as_comment fmt (nd.node_inputs, nd.node_outputs, s) | _ -> ()) nd.node_spec
(fun fmt -> match nd.node_spec with None -> () | Some _ -> fprintf fmt "@ ");
(* Locals *)
fprintf fmt "%a" (fun fmt locals ->
@@ -375,6 +411,15 @@ let pp_node fmt nd =
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", " pp_print_string) (Scheduling.schedule_node nd)*)
+let pp_node fmt nd =
+ match nd.node_spec, nd.node_iscontract with
+ | None, false
+ | Some (NodeSpec _), false
+ -> pp_node fmt nd
+ | Some (Contract _), false -> pp_node fmt nd (* may happen early in the compil process *)
+ | Some (Contract _), true -> pp_contract fmt nd
+ | _ -> assert false
+
let pp_imported_node fmt ind =
fprintf fmt "@[<v 0>";
(* Prototype *)
@@ -385,7 +430,7 @@ let pp_imported_node fmt ind =
pp_node_args ind.nodei_outputs;
(* Contracts *)
fprintf fmt "%a%t"
- (fun fmt s -> match s with Some s -> pp_spec_as_comment fmt s | _ -> ()) ind.nodei_spec
+ (fun fmt s -> match s with Some s -> pp_spec_as_comment fmt (ind.nodei_inputs, ind.nodei_outputs, s) | _ -> ()) ind.nodei_spec
(fun fmt -> match ind.nodei_spec with None -> () | Some _ -> fprintf fmt "@ ");
fprintf fmt "@]@ "
diff --git a/src/scheduling.ml b/src/scheduling.ml
index 8721b72b5f4795f6776c9c3440ea0ea21461f787..983d38bd6c5a58440e0c5605c3406cd5234014fc 100644
--- a/src/scheduling.ml
+++ b/src/scheduling.ml
@@ -113,13 +113,15 @@ let filter_original n vl =
let vdecl = get_node_var v n in
if vdecl.var_orig then v :: res else res) vl []
+let eq_equiv eq_equiv_hash =
+ fun v1 v2 ->
+ try
+ Hashtbl.find eq_equiv_hash v1 = Hashtbl.find eq_equiv_hash v2
+ with Not_found -> false
+
let schedule_node n =
(* let node_vars = get_node_vars n in *)
- let eq_equiv = ExprDep.node_eq_equiv n in
- let eq_equiv v1 v2 =
- try
- Hashtbl.find eq_equiv v1 = Hashtbl.find eq_equiv v2
- with Not_found -> false in
+ let eq_equiv = eq_equiv (ExprDep.node_eq_equiv n) in
let n', g = global_dependency n in
@@ -135,6 +137,9 @@ let schedule_node n =
let fanin = Liveness.compute_fanin n gg in
{ node = n'; schedule = sort; unused_vars = unused; fanin_table = fanin; dep_graph = gg; }
+(* let schedule_eqs eqs =
+ * let eq_equiv = eq_equiv (ExprDep.eqs_eq_equiv eqs) in
+ * assert false (\* TODO: continue to implement scheduling of eqs for spec *\) *)
let compute_node_reuse_table report =
let disjoint = Disjunction.clock_disjoint_map (get_node_vars report.node) in
diff --git a/src/tools/stateflow/semantics/cPS_lustre_generator.ml b/src/tools/stateflow/semantics/cPS_lustre_generator.ml
index 1ca7be39c746e1d55a4a192d2e896dbb0d70a085..6d88a593f3e109481f7e68255850b7e0a95cfb26 100644
--- a/src/tools/stateflow/semantics/cPS_lustre_generator.ml
+++ b/src/tools/stateflow/semantics/cPS_lustre_generator.ml
@@ -345,7 +345,8 @@ struct
node_dec_stateless = false;
node_stateless = None;
node_spec = None;
- node_annot = []}
+ node_annot = [];
+ node_iscontract = false}
)
in
[node]
@@ -400,7 +401,8 @@ Il faut faire les choses suivantes:
node_dec_stateless = false;
node_stateless = None;
node_spec = None;
- node_annot = []}
+ node_annot = [];
+ node_iscontract = false;}
)
in
node_principal
diff --git a/src/typing.ml b/src/typing.ml
index dfee23e23ddf188bf1ac610807b3cfae139d7070..be1ec772940223c1ed5ef1e6ea27059072071a9f 100644
--- a/src/typing.ml
+++ b/src/typing.ml
@@ -669,16 +669,16 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
let check_vd_env vd_env =
ignore (List.fold_left add_vdecl [] vd_env)
- let type_spec env spec =
- let vd_env = spec.consts @ spec.locals in
+ let type_contract env c =
+ let vd_env = c.consts @ c.locals in
check_vd_env vd_env;
let env = type_var_decl_list ((* this argument seems useless to me, cf TODO at top of the file*) vd_env) env vd_env in
(* typing stmts *)
- let eqs = List.map (fun s -> match s with Eq eq -> eq | _ -> assert false) spec.stmts in
+ let eqs = List.map (fun s -> match s with Eq eq -> eq | _ -> assert false) c.stmts in
let undefined_vars_init =
List.fold_left
(fun uvs v -> ISet.add v.var_id uvs)
- ISet.empty spec.locals
+ ISet.empty c.locals
in
let _ =
List.fold_left
@@ -692,9 +692,9 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
in
List.iter type_pred_ee
(
- spec.assume
- @ spec.guarantees
- @ List.flatten (List.map (fun m -> m.ensure @ m.require) spec.modes)
+ c.assume
+ @ c.guarantees
+ @ List.flatten (List.map (fun m -> m.ensure @ m.require) c.modes)
);
(*TODO
enrich env locally with locals and consts
@@ -703,13 +703,19 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
For the moment, returning the provided env
*)
env
-
+
+ let rec type_spec env spec loc =
+ match spec with
+ | Contract c -> type_contract env c
+ | NodeSpec id -> env
+
(** [type_node env nd loc] types node [nd] in environment env. The
location is used for error reports. *)
- let type_node env nd loc =
+ and type_node env nd loc =
let is_main = nd.node_id = !Options.main_node in
- let vd_env_ol = nd.node_outputs@nd.node_locals in
- let vd_env = nd.node_inputs@vd_env_ol in
+ (* In contracts, outputs are considered as input values *)
+ let vd_env_ol = if nd.node_iscontract then nd.node_locals else nd.node_outputs@nd.node_locals in
+ let vd_env = nd.node_inputs@nd.node_outputs@nd.node_locals 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
@@ -720,18 +726,22 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
List.fold_left
(fun uvs v -> ISet.add v.var_id uvs)
ISet.empty vd_env_ol in
+ Format.eprintf "Undef1: %a@ " pp_iset undefined_vars_init;
let undefined_vars =
let eqs, auts = get_node_eqs nd in
(* TODO XXX: il faut typer les handlers de l'automate *)
List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init eqs
in
+ Format.eprintf "Undef2: %a@ " pp_iset undefined_vars;
(* Typing asserts *)
List.iter (fun assert_ ->
let assert_expr = assert_.assert_expr in
type_subtyping_arg (new_env, vd_env) is_main false assert_expr (* Type_predef. *)type_bool
) nd.node_asserts;
(* Typing spec/contracts *)
- (match nd.node_spec with None -> () | Some spec -> ignore (type_spec new_env spec));
+ (match nd.node_spec with
+ | None -> ()
+ | Some spec -> ignore (type_spec new_env spec loc));
(* Typing annots *)
List.iter (fun annot ->
List.iter (fun (_, eexpr) -> ignore (type_eexpr (new_env, vd_env) eexpr)) annot.annots
@@ -739,7 +749,10 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
(* check that table is empty *)
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
+ Format.eprintf "Localconsts: %a@ " pp_iset local_consts;
let undefined_vars = ISet.diff undefined_vars local_consts in
+ Format.eprintf "Undef3: %a@ " pp_iset undefined_vars;
+
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
@@ -757,7 +770,9 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
let delta_env = type_var_decl_list vd_env delta_env nd.nodei_outputs in
let new_env = Env.overwrite env delta_env in
(* Typing spec *)
- (match nd.nodei_spec with None -> () | Some spec -> ignore (type_spec new_env spec));
+ (match nd.nodei_spec with
+ | None -> ()
+ | Some spec -> ignore (type_spec new_env spec loc));
let ty_ins = type_of_vlist nd.nodei_inputs in
let ty_outs = type_of_vlist nd.nodei_outputs in
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
@@ -865,14 +880,27 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
let check_env_compat header declared computed =
uneval_prog_generics header;
Env.iter declared (fun k decl_type_k ->
- let loc = (get_imported_symbol header k).top_decl_loc in
- let computed_t =
- instantiate (ref []) (ref [])
- (try Env.lookup_value computed k
- with Not_found -> raise (Error (loc, Declared_but_undefined k))) in
- (*Types.print_ty Format.std_formatter decl_type_k;
- Types.print_ty Format.std_formatter computed_t;*)
- try_unify ~sub:true ~semi:true decl_type_k computed_t loc
+ let top = get_imported_symbol header k in
+ let loc = top.top_decl_loc in
+ try
+ let computed_t = Env.lookup_value computed k in
+ let computed_t = instantiate (ref []) (ref []) computed_t in
+ (*Types.print_ty Format.std_formatter decl_type_k;
+ Types.print_ty Format.std_formatter computed_t;*)
+ try_unify ~sub:true ~semi:true decl_type_k computed_t loc
+ with Not_found ->
+ begin
+ (* If top is a contract we do not require the lustre
+ file to provide the same definition. *)
+ match top.top_decl_desc with
+ | Node nd -> (
+ match nd.node_spec with
+ | Some (Contract _) -> ()
+ | _ -> raise (Error (loc, Declared_but_undefined k))
+ )
+ | _ ->
+ raise (Error (loc, Declared_but_undefined k))
+ end
)
let check_typedef_top decl =
diff --git a/src/utils/utils.ml b/src/utils/utils.ml
index a2b7a2d8bfe2025ae049ff7af6c9e4e494e97229..89d1be33652004832e86eebf09c1bb0ce9955223 100644
--- a/src/utils/utils.ml
+++ b/src/utils/utils.ml
@@ -427,6 +427,9 @@ let get_date () =
(* in *)
Format.flush_str_formatter ()
-(* Local Variables: *)
-(* compile-command:"make -C .." *)
-(* End: *)
+
+
+ (* Local Variables: *)
+ (* compile-command:"make -C .." *)
+ (* End: *)
+