From 1fd3d00272e2289a411c2fafcb158e8643c31114 Mon Sep 17 00:00:00 2001
From: ploc <ploc@garoche.net>
Date: Thu, 21 Mar 2019 09:20:24 -0700
Subject: [PATCH] Cocospec: parsing, normalizing and processing machines for
contracts.
---
src/causality.ml | 7 +-
src/clock_calculus.ml | 1 +
src/clocks.ml | 8 --
src/compiler_common.ml | 108 ++++++++++---------
src/compiler_stages.ml | 9 +-
src/corelang.ml | 141 ++++++++++++++++---------
src/corelang.mli | 9 +-
src/lustre_types.ml | 1 +
src/machine_code.ml | 18 +++-
src/machine_code_common.ml | 6 +-
src/machine_code_types.ml | 1 +
src/normalization.ml | 35 +++---
src/optimize_machine.ml | 27 +++--
src/parsers/lexerLustreSpec.mll | 2 +-
src/parsers/lexer_lustre.mll | 2 +-
src/parsers/parser_lustre.mly | 12 +++
src/plugins/salsa/machine_salsa_opt.ml | 6 +-
src/printers.ml | 60 ++++++-----
src/typing.ml | 7 +-
19 files changed, 285 insertions(+), 175 deletions(-)
diff --git a/src/causality.ml b/src/causality.ml
index 97f65972..78be31e6 100644
--- a/src/causality.ml
+++ b/src/causality.ml
@@ -384,8 +384,13 @@ module NodeDep = struct
)
)
in
+ let deps_spec = match nd.node_spec with
+ | None -> []
+ | Some (NodeSpec id) -> [id]
+ | Some (Contract c) -> []
+ in
(*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *)
- add_edges [nd.node_id] (deps@deps_asserts) accu
+ add_edges [nd.node_id] (deps@deps_asserts@deps_spec) accu
| _ -> assert false (* should not happen *)
) prog g in
diff --git a/src/clock_calculus.ml b/src/clock_calculus.ml
index 520704ef..2324b496 100644
--- a/src/clock_calculus.ml
+++ b/src/clock_calculus.ml
@@ -493,6 +493,7 @@ and clock_appl env f args clock_reset loc =
clock_call env f args clock_reset loc
and clock_call env f args clock_reset loc =
+ (* Format.eprintf "Clocking call %s@." f; *)
let cfun = clock_ident false env f loc in
let cins, couts = split_arrow cfun in
let cins = clock_list_of_clock cins in
diff --git a/src/clocks.ml b/src/clocks.ml
index c148d482..9fc3ecaa 100644
--- a/src/clocks.ml
+++ b/src/clocks.ml
@@ -132,14 +132,6 @@ let rec carrier_repr =
function {carrier_desc = Carry_link cr'} -> carrier_repr cr'
| cr -> cr
-(** Splits [ck] into the [lhs,rhs] of an arrow clock. Expects an arrow clock
- (ensured by language syntax) *)
-let split_arrow ck =
- match (repr ck).cdesc with
- | Carrow (cin,cout) -> cin,cout
- (* Functions are not first order, I don't think the var case
- needs to be considered here *)
- | _ -> failwith "Internal error: not an arrow clock"
let get_carrier_name ck =
match (repr ck).cdesc with
diff --git a/src/compiler_common.ml b/src/compiler_common.ml
index 2e347c31..b145bbad 100644
--- a/src/compiler_common.ml
+++ b/src/compiler_common.ml
@@ -190,7 +190,8 @@ let check_compatibility (prog, computed_types_env, computed_clocks_env) (header,
(* 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 =
+ let process_contract new_contracts c =
+ Format.eprintf "Process contract@.";
(* Resolve first the imports *)
let stmts, locals, c =
List.fold_left (
@@ -204,50 +205,55 @@ let resolve_contracts prog =
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 *)
- (*
+ Format.eprintf "Process contract import %s@." name;
+ let loc = import.import_loc in
try
- let imp_nd = xxx in (* Get the contract node in prog *)
+ let imp_nd = get_node name new_contracts in (* Get the contract node in process contracts *)
(* 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
+ let _ =
+ if not (is_node_contract imp_nd) then
+ assert false (* should be a contract *)
+ else
+ let imp_c = get_node_contract imp_nd in
+ if not (imp_c.imports = [] && imp_c.locals = [] && imp_c.consts = [] && imp_c.stmts = []) then
+ ( Format.eprintf "Invalid processed contract: %i %i %i %i@.@?" (List.length imp_c.imports) (List.length imp_c.locals) (List.length imp_c.consts) (List.length imp_c.stmts);
+ assert false (* should be processed *)
+ )
in
- let out_assigns =
- xxx imp_out = import.outputs
+ let name_prefix x = "__" ^ name ^ "__" ^ x in
+ let imp_nd = rename_node (fun x -> x (* not changing node names *)) name_prefix imp_nd in
+ 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 imp_c = get_node_contract imp_nd in
+ (* Assigning in and out *)
+ let mk_def vars_l e =
+ let lhs = List.map (fun v -> v.var_id) vars_l in
+ Eq (mkeq loc (lhs, e))
in
- let stmts = stmts @ (rename imp_nd.stmts) in
- let imp_c = rename imp_c in
+ let in_assigns = mk_def imp_in import.inputs in
+ let out_assigns = mk_def imp_out import.outputs in
+ let stmts = in_assigns :: out_assigns :: imp_nd.node_stmts @ stmts in
let c = merge_contracts c imp_c in
stmts, locals, c
- with Not_found -> raise (Error.Unbound_symbol ("contract " ^ name))
+ with Not_found -> assert false; raise (Error (loc, (Error.Unbound_symbol ("contract " ^ name))))
- *)
+
) ([], c.consts@c.locals, c) c.imports
in
+ let stmts = stmts @ c.stmts in
(* Other contract elements will be normalized later *)
- let c = { c with
+ let c = { c with (* we erase locals and stmts sinced they are now in the parent node *)
locals = [];
consts = [];
stmts = [];
imports = []
}
in
+
+ (* Format.eprintf "Processed stmts: %a@." Printers.pp_node_stmts stmts;
+ * Format.eprintf "Processed locals: %a@." Printers.pp_vars locals; *)
stmts, locals, c
in
@@ -258,11 +264,14 @@ let resolve_contracts prog =
| ImportedNode ind -> ind.nodei_id, ind.nodei_spec, ind.nodei_inputs, ind.nodei_outputs
| _ -> assert false
in
+ Format.eprintf "Process contract new node for node %s@." id;
+
let stmts, locals, c =
match spec with
| None | Some (NodeSpec _) -> assert false
| Some (Contract c) ->
- process_contract accu_contracts prog c
+ (* Format.eprintf "Processing contract of node %s@." id; *)
+ process_contract accu_contracts c
in
(* Create a fresh name *)
let used v = List.exists (fun top ->
@@ -279,23 +288,23 @@ let resolve_contracts prog =
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
+ (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
@@ -317,7 +326,8 @@ let resolve_contracts prog =
match nd.node_spec with
| None | Some (NodeSpec _) -> assert false
| Some (Contract c) ->
- let stmts, locals, c = process_contract accu_contracts prog c in
+ (* Format.eprintf "Processing top contract %s@." nd.node_id; *)
+ let stmts, locals, c = process_contract accu_contracts c in
let nd =
{ nd with
node_locals = nd.node_locals @ locals;
@@ -337,7 +347,7 @@ let resolve_contracts prog =
| 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);
+ (* 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
diff --git a/src/compiler_stages.ml b/src/compiler_stages.ml
index 3c72b644..397c1494 100644
--- a/src/compiler_stages.ml
+++ b/src/compiler_stages.ml
@@ -77,9 +77,14 @@ let stage1 params prog dirname basename extension =
(* Sorting nodes *)
let prog = SortProg.sort prog in
-
+Format.eprintf "ok1@.";
(* Consolidating contracts *)
let prog = resolve_contracts prog in
+Format.eprintf "ok2@.";
+ let prog = SortProg.sort prog in
+Format.eprintf "ok3@.";
+ Log.report ~level:3 (fun fmt ->
+ Format.fprintf fmt "@[<v 0>Contracts resolved:@ %a@ @]@ " Printers.pp_prog prog);
(* Perform inlining before any analysis *)
let orig, prog =
@@ -322,7 +327,7 @@ let stage3 prog machine_code dependencies basename extension =
| "emf", _ ->
begin
let destname = !Options.dest_dir ^ "/" ^ basename in
- let source_file = destname ^ ".emf" in (* Could be changed *)
+ let source_file = destname ^ ".json" in (* Could be changed *)
let source_out = open_out source_file in
let fmt = formatter_of_out_channel source_out in
EMF_backend.translate fmt basename prog machine_code;
diff --git a/src/corelang.ml b/src/corelang.ml
index 65e429d0..82f45f38 100644
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -194,12 +194,13 @@ let mk_contract_var id is_const type_opt expr loc =
let v = mkvar_decl loc (id, typ, mkclock loc Ckdec_any, is_const, None, None) in
let eq = mkeq loc ([id], expr) in
{ empty_contract with locals = [v]; stmts = [Eq eq]; spec_loc = loc; }
+let eexpr_add_name eexpr name =
+ {eexpr with eexpr_name = match name with "" -> None | _ -> Some name}
+let mk_contract_guarantees ?(name="") eexpr =
+ { empty_contract with guarantees = [eexpr_add_name eexpr name]; spec_loc = eexpr.eexpr_loc }
-let mk_contract_guarantees eexpr =
- { empty_contract with guarantees = [eexpr]; spec_loc = eexpr.eexpr_loc }
-
-let mk_contract_assume eexpr =
- { empty_contract with assume = [eexpr]; spec_loc = eexpr.eexpr_loc }
+let mk_contract_assume ?(name="") eexpr =
+ { empty_contract with assume = [eexpr_add_name eexpr name]; spec_loc = eexpr.eexpr_loc }
let mk_contract_mode id rl el loc =
{ empty_contract with modes = [{ mode_id = id; require = rl; ensure = el; mode_loc = loc; }]; spec_loc = loc }
@@ -223,6 +224,7 @@ let mkeexpr loc expr =
{ eexpr_tag = Utils.new_tag ();
eexpr_qfexpr = expr;
eexpr_quantifiers = [];
+ eexpr_name = None;
eexpr_type = Types.new_var ();
eexpr_clock = Clocks.new_var true;
eexpr_loc = loc }
@@ -324,16 +326,21 @@ let is_imported_node td =
| ImportedNode nd -> true
| _ -> assert false
+let is_node_contract nd =
+ match nd.node_spec with
+ | Some (Contract _) -> true
+ | _ -> false
+
+let get_node_contract nd =
+ match nd.node_spec with
+ | Some (Contract c) -> c
+ | _ -> assert false
+
let is_contract td =
match td.top_decl_desc with
- | Node nd -> (
- match nd.node_spec with
- | Some (Contract _) -> true
- | _ -> false
- )
+ | Node nd -> is_node_contract nd
| _ -> false
-
(* alias and type definition table *)
let mktop = mktop_decl Location.dummy_loc !Options.dest_dir false
@@ -709,8 +716,36 @@ let get_node_interface nd =
}
(************************************************************************)
-(* Renaming *)
+(* Renaming / Copying *)
+
+let copy_var_decl vdecl =
+ mkvar_decl vdecl.var_loc ~orig:vdecl.var_orig (vdecl.var_id, vdecl.var_dec_type, vdecl.var_dec_clock, vdecl.var_dec_const, vdecl.var_dec_value, vdecl.var_parent_nodeid)
+let copy_const cdecl =
+ { cdecl with const_type = Types.new_var () }
+
+let copy_node nd =
+ { nd with
+ node_type = Types.new_var ();
+ node_clock = Clocks.new_var true;
+ node_inputs = List.map copy_var_decl nd.node_inputs;
+ node_outputs = List.map copy_var_decl nd.node_outputs;
+ node_locals = List.map copy_var_decl nd.node_locals;
+ node_gencalls = [];
+ node_checks = [];
+ node_stateless = None;
+ }
+
+let copy_top top =
+ match top.top_decl_desc with
+ | Node nd -> { top with top_decl_desc = Node (copy_node nd) }
+ | Const c -> { top with top_decl_desc = Const (copy_const c) }
+ | _ -> top
+
+let copy_prog top_list =
+ List.map copy_top top_list
+
+
let rec rename_static rename cty =
match cty with
| Tydec_array (d, cty') -> Tydec_array (Dimension.expr_replace_expr rename d, rename_static rename cty')
@@ -768,17 +803,17 @@ let rec rename_carrier rename cck =
| Expr_appl (i, e', i') ->
Expr_appl (f_node i, re e', Utils.option_map re i')
- let rename_dec_type f_node f_var t = assert false (*
+ let rename_dec_type f_node f_var t = t (* TODO : do we really want to rename a declared type ?
Types.rename_dim_type (Dimension.rename f_node f_var) t*)
- let rename_dec_clock f_node f_var c = assert false (*
+ let rename_dec_clock f_node f_var c = c (* TODO : do we really want to rename a declared clock ? assert false
Clocks.rename_clock_expr f_var c*)
let rename_var f_node f_var v = {
- v with
+ (copy_var_decl v) with
var_id = f_var v.var_id;
- var_dec_type = rename_dec_type f_node f_var v.var_type;
- var_dec_clock = rename_dec_clock f_node f_var v.var_clock
+ var_dec_type = rename_dec_type f_node f_var v.var_dec_type;
+ var_dec_clock = rename_dec_clock f_node f_var v.var_dec_clock
}
let rename_vars f_node f_var = List.map (rename_var f_node f_var)
@@ -822,17 +857,38 @@ and rename_eexpr f_node f_var ee =
eexpr_qfexpr = rename_expr f_node f_var ee.eexpr_qfexpr;
eexpr_quantifiers = List.map (fun (typ,vdecls) -> typ, rename_vars f_node f_var vdecls) ee.eexpr_quantifiers;
}
-
-
+and rename_mode f_node f_var m =
+ let rename_ee = rename_eexpr f_node f_var in
+ {
+ m with
+ require = List.map rename_ee m.require;
+ ensure = List.map rename_ee m.ensure
+ }
+ let rename_import f_node f_var imp =
+ let rename_expr = rename_expr f_node f_var in
+ {
+ imp with
+ import_nodeid = f_node imp.import_nodeid;
+ inputs = rename_expr imp.inputs;
+ outputs = rename_expr imp.outputs;
+ }
let rename_node f_node f_var nd =
+ let f_var x = (* checking that this is actually a local variable *)
+ if List.exists (fun v -> v.var_id = x) (get_node_vars nd) then
+ f_var x
+ else
+ x
+ in
let rename_var = rename_var f_node f_var in
+ let rename_vars = List.map rename_var in
let rename_expr = rename_expr f_node f_var in
+ let rename_eexpr = rename_eexpr f_node f_var in
let rename_stmts = rename_stmts f_node f_var in
- let inputs = List.map rename_var nd.node_inputs in
- let outputs = List.map rename_var nd.node_outputs in
- let locals = List.map rename_var nd.node_locals in
+ let inputs = rename_vars nd.node_inputs in
+ let outputs = rename_vars nd.node_outputs in
+ let locals = rename_vars 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 = List.map
@@ -848,7 +904,19 @@ and rename_eexpr f_node f_var ee =
in
let spec =
Utils.option_map
- (fun s -> assert false; (*rename_node_annot f_node f_var s*) ) (* TODO: implement! *)
+ (fun s -> match s with
+ NodeSpec id -> NodeSpec (f_node id)
+ | Contract c -> Contract {
+ c with
+ consts = rename_vars c.consts;
+ locals = rename_vars c.locals;
+ stmts = rename_stmts c.stmts;
+ assume = List.map rename_eexpr c.assume;
+ guarantees = List.map rename_eexpr c.guarantees;
+ modes = List.map (rename_mode f_node f_var) c.modes;
+ imports = List.map (rename_import f_node f_var) c.imports;
+ }
+ )
nd.node_spec
in
let annot = rename_annots f_node f_var nd.node_annot in
@@ -1042,6 +1110,7 @@ let rec substitute_expr vars_to_replace defs e =
{ eexpr_tag = expr.expr_tag;
eexpr_qfexpr = expr;
eexpr_quantifiers = [];
+ eexpr_name = None;
eexpr_type = expr.expr_type;
eexpr_clock = expr.expr_clock;
eexpr_loc = expr.expr_loc;
@@ -1176,32 +1245,6 @@ and node_has_arrows node =
-let copy_var_decl vdecl =
- mkvar_decl vdecl.var_loc ~orig:vdecl.var_orig (vdecl.var_id, vdecl.var_dec_type, vdecl.var_dec_clock, vdecl.var_dec_const, vdecl.var_dec_value, vdecl.var_parent_nodeid)
-
-let copy_const cdecl =
- { cdecl with const_type = Types.new_var () }
-
-let copy_node nd =
- { nd with
- node_type = Types.new_var ();
- node_clock = Clocks.new_var true;
- node_inputs = List.map copy_var_decl nd.node_inputs;
- node_outputs = List.map copy_var_decl nd.node_outputs;
- node_locals = List.map copy_var_decl nd.node_locals;
- node_gencalls = [];
- node_checks = [];
- node_stateless = None;
- }
-
-let copy_top top =
- match top.top_decl_desc with
- | Node nd -> { top with top_decl_desc = Node (copy_node nd) }
- | Const c -> { top with top_decl_desc = Const (copy_const c) }
- | _ -> top
-
-let copy_prog top_list =
- List.map copy_top top_list
let rec expr_contains_expr expr_tag expr =
diff --git a/src/corelang.mli b/src/corelang.mli
index 32a84264..bff17ca2 100644
--- a/src/corelang.mli
+++ b/src/corelang.mli
@@ -59,6 +59,8 @@ 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 is_node_contract: node_desc -> bool
+val get_node_contract: node_desc -> contract_desc
val consts_table: (ident, top_decl) Hashtbl.t
val print_consts_table: Format.formatter -> unit -> unit
@@ -154,8 +156,9 @@ val rename_expr : (ident -> ident) -> (ident -> ident) -> expr -> expr
val rename_eq : (ident -> ident) -> (ident -> ident) -> eq -> eq
(** val rename_aut f_node f_var aut *)
val rename_aut : (ident -> ident) -> (ident -> ident) -> automata_desc -> automata_desc
-(** rename_prog f_node f_var prog *)
+(** rename_prog f_node f_var f_const prog *)
val rename_prog: (ident -> ident) -> (ident -> ident) -> (ident -> ident) -> program_t -> program_t
+val rename_node: (ident -> ident) -> (ident -> ident) -> node_desc -> node_desc
val substitute_expr: var_decl list -> eq list -> expr -> expr
@@ -169,8 +172,8 @@ val copy_prog: top_decl list -> top_decl list
val mkeexpr: Location.t -> expr -> eexpr
val empty_contract: contract_desc
val mk_contract_var: ident -> bool -> type_dec option -> expr -> Location.t -> contract_desc
-val mk_contract_guarantees: eexpr -> contract_desc
-val mk_contract_assume: eexpr -> contract_desc
+val mk_contract_guarantees: ?name:string -> eexpr -> contract_desc
+val mk_contract_assume: ?name:string -> eexpr -> contract_desc
val mk_contract_mode: ident -> eexpr list -> eexpr 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
diff --git a/src/lustre_types.ml b/src/lustre_types.ml
index b1956644..58764678 100644
--- a/src/lustre_types.ml
+++ b/src/lustre_types.ml
@@ -116,6 +116,7 @@ and eexpr =
{eexpr_tag: tag;
eexpr_qfexpr: expr;
eexpr_quantifiers: (quantifier_type * var_decl list) list;
+ eexpr_name: string option;
mutable eexpr_type: Types.type_expr;
mutable eexpr_clock: Clocks.clock_expr;
(* mutable eexpr_normalized: (var_decl * eq list * var_decl list) option; *)
diff --git a/src/machine_code.ml b/src/machine_code.ml
index 318c719d..81a52b78 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -46,9 +46,9 @@ let build_env locals non_locals =
get_var = (fun id -> try
VSet.get id all
with Not_found -> (
- Format.eprintf "Impossible to find variable %s in set %a@.@?"
- id
- VSet.pp all;
+ (* Format.eprintf "Impossible to find variable %s in set %a@.@?"
+ * id
+ * VSet.pp all; *)
raise Not_found
)
)
@@ -377,6 +377,7 @@ let translate_core sorted_eqs locals other_vars =
let translate_decl nd sch =
+ (* Format.eprintf "Translating node %s@." nd.node_id; *)
(* Extracting eqs, variables .. *)
let eqs, auts = get_node_eqs nd in
assert (auts = []); (* Automata should be expanded by now *)
@@ -390,13 +391,22 @@ let translate_decl nd sch =
let locals = VSet.of_list locals_list in
let inout_vars = (VSet.of_list (nd.node_inputs @ nd.node_outputs)) in
let env = build_env locals inout_vars in
+
+ (* Format.eprintf "Node content is %a@." Printers.pp_node nd; *)
(* Computing main content *)
+ (* Format.eprintf "ok1@.@?"; *)
let schedule = sch.Scheduling_type.schedule in
+ (* Format.eprintf "ok2@.@?"; *)
let sorted_eqs = Scheduling.sort_equations_from_schedule eqs schedule in
-
+ (* Format.eprintf "ok3@.locals=%a@.inout:%a@?"
+ * VSet.pp locals
+ * VSet.pp inout_vars
+ * ; *)
+
let ctx, ctx0_s = translate_core (assert_instrs@sorted_eqs) locals inout_vars in
+ (* Format.eprintf "ok4@.@?"; *)
let mmap = Utils.IMap.elements ctx.j in
diff --git a/src/machine_code_common.ml b/src/machine_code_common.ml
index 41f6a374..a58ec1b4 100644
--- a/src/machine_code_common.ml
+++ b/src/machine_code_common.ml
@@ -46,6 +46,7 @@ let rec pp_instr m fmt i =
pp_val g
(Utils.fprintf_list ~sep:"@," pp_branch) hl
| MComment s -> Format.pp_print_string fmt s
+ | MSpec s -> Format.pp_print_string fmt ("@" ^ s)
in
(* Annotation *)
@@ -122,7 +123,10 @@ let rec is_const_value v =
(* Returns the declared stateless status and the computed one. *)
let get_stateless_status m =
- (m.mname.node_dec_stateless, try Utils.desome m.mname.node_stateless with _ -> failwith ("stateless status of machine " ^ m.mname.node_id ^ " not computed"))
+ (m.mname.node_dec_stateless,
+ try
+ Utils.desome m.mname.node_stateless
+ with _ -> failwith ("stateless status of machine " ^ m.mname.node_id ^ " not computed"))
let is_stateless m = m.minstances = [] && m.mmemory = []
diff --git a/src/machine_code_types.ml b/src/machine_code_types.ml
index 1283f396..e5ce4c4b 100644
--- a/src/machine_code_types.ml
+++ b/src/machine_code_types.ml
@@ -29,6 +29,7 @@ and instr_t_desc =
| MStep of var_decl list * ident * value_t list
| MBranch of value_t * (label * instr_t list) list
| MComment of string
+ | MSpec of string
type step_t = {
step_checks: (Location.t * value_t) list;
diff --git a/src/normalization.ml b/src/normalization.ml
index 71026215..079ec722 100644
--- a/src/normalization.ml
+++ b/src/normalization.ml
@@ -450,18 +450,21 @@ let normalize_pred_eexpr decls norm_ctx (def,vars) ee =
inline possible calls within, normalize it and type/clock the
result. *)
let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in
- (* Inlining any calls *)
- let nodes = get_nodes decls in
- let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in
- let vars, eqs =
- if calls = [] && not (eq_has_arrows eq) then
- vars, [eq]
- else
- assert false (* TODO *)
- in
+
+
+ (* (\* Inlining any calls *\)
+ * let nodes = get_nodes decls in
+ * let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in
+ * let vars, eqs =
+ * if calls = [] && not (eq_has_arrows eq) then
+ * vars, [eq]
+ * else
+ * assert false (\* TODO *\)
+ * in *)
(* Normalizing expr and eqs *)
- let defs, vars = List.fold_left (normalize_eq_split norm_ctx) (def, vars) eqs in
+ let defs, vars = List.fold_left (normalize_eq_split norm_ctx) (def, vars) [eq] in
+ let vars = output_var :: vars in
(* let todefine =
List.fold_left
(fun m x-> if List.exists (fun y-> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m)
@@ -557,6 +560,7 @@ let normalize_spec decls parentid (in_vars, out_vars, l_vars) s =
(* 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
+ (* Format.eprintf "NormSpec: init locals: %a@." Printers.pp_vars s.locals; *)
let not_is_orig_var v =
List.for_all ((!=) v) orig_vars in
let norm_ctx = {
@@ -574,10 +578,15 @@ let normalize_spec decls parentid (in_vars, out_vars, l_vars) s =
(* Iterate through predicates and normalize them on the go, creating
fresh variables for any guarantees/assumes/require/ensure *)
let process_predicates l defvars =
- List.fold_right (fun ee (accu, defvars) ->
+ (* Format.eprintf "ProcPred: vars: %a@." Printers.pp_vars (snd defvars); *)
+ let res = List.fold_right (fun ee (accu, defvars) ->
let ee', defvars = normalize_pred_eexpr decls norm_ctx defvars ee in
ee'::accu, defvars
) l ([], defvars)
+ in
+ (* Format.eprintf "ProcStmt: %a@." Printers.pp_node_eqs (fst (snd res));
+ * Format.eprintf "ProcPred: vars: %a@." Printers.pp_vars (snd (snd res)); *)
+ res
in
@@ -595,7 +604,7 @@ let normalize_spec decls parentid (in_vars, out_vars, l_vars) s =
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;
+ (* locals = s.locals @ new_locals; *)
stmts = [];
assume = assume';
guarantees = guarantees';
@@ -663,6 +672,8 @@ let normalize_node decls node =
(node.node_inputs, node.node_outputs, node.node_locals)
s
in
+ (* Format.eprintf "Normalization bounded new locals: %a@." Printers.pp_vars new_locals;
+ * Format.eprintf "Normalization bounded stmts: %a@." Printers.pp_node_eqs new_stmts; *)
Some (Contract s'), new_locals, new_stmts@eqs
end
in
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index df4fea07..61777be3 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -28,7 +28,7 @@ let pp_elim m fmt elim =
let rec eliminate m elim instr =
let e_expr = eliminate_expr m elim in
match get_instr_desc instr with
- | MComment _ -> instr
+ | MSpec _ | MComment _ -> instr
| MLocalAssign (i,v) -> update_instr_desc instr (MLocalAssign (i, e_expr v))
| MStateAssign (i,v) -> update_instr_desc instr (MStateAssign (i, e_expr v))
| MReset i -> instr
@@ -119,7 +119,7 @@ let rec simplify_instr_offset m instr =
-> update_instr_desc instr (
MBranch(simplify_expr_offset m cond, List.map (fun (l, il) -> l, simplify_instrs_offset m il) brl)
)
- | MComment _ -> instr
+ | MSpec _ | MComment _ -> instr
and simplify_instrs_offset m instrs =
List.map (simplify_instr_offset m) instrs
@@ -265,12 +265,19 @@ let instr_of_const top_const =
let vdecl = { vdecl with var_type = const.const_type }
in mkinstr (MLocalAssign (vdecl, mk_val (Cst const.const_value) vdecl.var_type))
+(* We do not perform this optimization on contract nodes since there
+ is not explicit dependence btw variables and their use in
+ contracts. *)
let machines_unfold consts node_schs machines =
List.fold_right (fun m (machines, removed) ->
- let fanin = (IMap.find m.mname.node_id node_schs).Scheduling_type.fanin_table in
- let elim_consts, _ = instrs_unfold m fanin IMap.empty (List.map instr_of_const consts) in
- let (m, removed_m) = machine_unfold fanin elim_consts m in
- (m::machines, IMap.add m.mname.node_id removed_m removed)
+ let is_contract = match m.mspec with Some (Contract _) -> true | _ -> false in
+ if is_contract then
+ m::machines, removed
+ else
+ let fanin = (IMap.find m.mname.node_id node_schs).Scheduling_type.fanin_table in
+ let elim_consts, _ = instrs_unfold m fanin IMap.empty (List.map instr_of_const consts) in
+ let (m, removed_m) = machine_unfold fanin elim_consts m in
+ (m::machines, IMap.add m.mname.node_id removed_m removed)
)
machines
([], IMap.empty)
@@ -468,7 +475,7 @@ let rec value_replace_var fvar value =
let rec instr_replace_var fvar instr cont =
match get_instr_desc instr with
- | MComment _ -> instr_cons instr cont
+ | MSpec _ | MComment _ -> instr_cons instr cont
| MLocalAssign (i, v) -> instr_cons (update_instr_desc instr (MLocalAssign (fvar i, value_replace_var fvar v))) cont
| MStateAssign (i, v) -> instr_cons (update_instr_desc instr (MStateAssign (i, value_replace_var fvar v))) cont
| MReset i -> instr_cons instr cont
@@ -593,7 +600,9 @@ let optimize prog node_schs machine_code =
in
(* Optimize machine code *)
let machine_code, removed_table =
- if !Options.optimization >= 2 && !Options.output <> "emf" (*&& !Options.output <> "horn"*) then
+ if !Options.optimization >= 2
+ && !Options.output <> "emf" (*&& !Options.output <> "horn"*)
+ then
begin
Log.report ~level:1 (fun fmt -> Format.fprintf fmt
".. machines optimization: const. inlining (partial eval. with const)@,");
@@ -620,7 +629,7 @@ let optimize prog node_schs machine_code =
in
- machine_code
+ List.rev machine_code
(* Local Variables: *)
diff --git a/src/parsers/lexerLustreSpec.mll b/src/parsers/lexerLustreSpec.mll
index e4ef79b0..18c911ee 100644
--- a/src/parsers/lexerLustreSpec.mll
+++ b/src/parsers/lexerLustreSpec.mll
@@ -64,7 +64,7 @@ let keyword_table =
"mode", MODE;
"assume", ASSUME;
"contract", CONTRACT;
- "guarantees", GUARANTEES;
+ "guarantee", GUARANTEES;
"exists", EXISTS;
"forall", FORALL;
"c_code", CCODE;
diff --git a/src/parsers/lexer_lustre.mll b/src/parsers/lexer_lustre.mll
index 5d81cff7..ad68e09b 100644
--- a/src/parsers/lexer_lustre.mll
+++ b/src/parsers/lexer_lustre.mll
@@ -69,7 +69,7 @@ let keyword_table =
"mode", MODE;
"assume", ASSUME;
"contract", CONTRACT;
- "guarantees", GUARANTEES;
+ "guarantee", GUARANTEES;
"exists", EXISTS;
"forall", FORALL;
diff --git a/src/parsers/parser_lustre.mly b/src/parsers/parser_lustre.mly
index 31323d7b..8ad04a4b 100644
--- a/src/parsers/parser_lustre.mly
+++ b/src/parsers/parser_lustre.mly
@@ -413,19 +413,31 @@ contract_content:
{ merge_contracts (mk_contract_var $2 false (Some(mktyp $4)) $6 (get_loc())) $8 }
| ASSUME qexpr SCOL contract_content
{ merge_contracts (mk_contract_assume $2) $4 }
+| ASSUME STRING qexpr SCOL contract_content
+ { merge_contracts (mk_contract_assume ~name:$2 $3) $5 }
| GUARANTEES qexpr SCOL contract_content
{ merge_contracts (mk_contract_guarantees $2) $4 }
+| GUARANTEES STRING qexpr SCOL contract_content
+ { merge_contracts (mk_contract_guarantees ~name:$2 $3) $5 }
| 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_content
+ { merge_contracts (mk_contract_import $2 (mkexpr (Expr_tuple (List.rev $4))) (mkexpr (Expr_tuple (List.rev $8))) (get_loc())) $11 }
+| IMPORT IDENT LPAR expr RPAR RETURNS LPAR tuple_expr RPAR SCOL contract_content
+ { merge_contracts (mk_contract_import $2 $4 (mkexpr (Expr_tuple (List.rev $8))) (get_loc())) $11 }
+| IMPORT IDENT LPAR tuple_expr RPAR RETURNS LPAR expr RPAR SCOL contract_content
+ { merge_contracts (mk_contract_import $2 (mkexpr (Expr_tuple (List.rev $4))) $8 (get_loc())) $11 }
| 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:
{ [], [] }
| REQUIRE qexpr SCOL mode_content { let (r,e) = $4 in $2::r, e }
+| REQUIRE STRING qexpr SCOL mode_content { let (r,e) = $5 in {$3 with eexpr_name = Some $2}::r, e }
| ENSURE qexpr SCOL mode_content { let (r,e) = $4 in r, $2::e }
+| ENSURE STRING qexpr SCOL mode_content { let (r,e) = $5 in r, {$3 with eexpr_name = Some $2}::e }
/* WARNING: UNUSED RULES */
tuple_qexpr:
diff --git a/src/plugins/salsa/machine_salsa_opt.ml b/src/plugins/salsa/machine_salsa_opt.ml
index 9cc0babc..e6ce5e28 100644
--- a/src/plugins/salsa/machine_salsa_opt.ml
+++ b/src/plugins/salsa/machine_salsa_opt.ml
@@ -61,7 +61,7 @@ let rec get_read_vars instrs =
)
| MReset _
| MNoReset _
- | MComment _ -> Vars.empty
+ | MSpec _ | MComment _ -> Vars.empty
)
let rec get_written_vars instrs =
@@ -79,7 +79,7 @@ let rec get_written_vars instrs =
)
| MReset _
| MNoReset _
- | MComment _ -> Vars.empty
+ | MSpec _ | MComment _ -> Vars.empty
)
(* let rec iterTransformExpr fresh_id e_salsa abstractEnv old_range = *)
@@ -720,7 +720,7 @@ let rec rewrite_instrs nodename m constEnv vars_env m instrs ranges formalEnv p
new_locals
- | MT.MReset(_) | MT.MNoReset _ | MT.MComment _ ->
+ | MT.MReset(_) | MT.MNoReset _ | MT.MSpec _ | MT.MComment _ ->
(* if !debug then Format.eprintf "Untouched %a (non real)@ " MC.pp_instr hd_instr; *)
(* Untouched instruction *)
diff --git a/src/printers.ml b/src/printers.ml
index 51ceca36..6cb91a36 100644
--- a/src/printers.ml
+++ b/src/printers.ml
@@ -62,10 +62,13 @@ let pp_var fmt id =
id.var_id
pp_var_type id
+let pp_vars fmt vars =
+ fprintf_list ~sep:"; " pp_var fmt vars
+
let pp_quantifiers fmt (q, vars) =
match q with
- | Forall -> fprintf fmt "forall %a" (fprintf_list ~sep:"; " pp_var) vars
- | Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars
+ | Forall -> fprintf fmt "forall %a" pp_vars vars
+ | Exists -> fprintf fmt "exists %a" pp_vars vars
let rec pp_struct_const_field fmt (label, c) =
fprintf fmt "%a = %a;" pp_print_string label pp_const c
@@ -278,17 +281,17 @@ let pp_typedec fmt ty =
-let pp_quantifiers fmt (q, vars) =
- match q with
- | Forall -> fprintf fmt "forall %a" (fprintf_list ~sep:"; " pp_var) vars
- | Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars
+(* let pp_quantifiers fmt (q, vars) =
+ * match q with
+ * | Forall -> fprintf fmt "forall %a" pp_vars vars
+ * | Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars *)
-let pp_eexpr fmt e =
+(*let pp_eexpr fmt e =
fprintf fmt "%a%t %a"
(Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers
(fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
pp_expr e.eexpr_qfexpr
-
+ *)
let pp_spec_eq fmt eq =
fprintf fmt "var %a : %a = %a;"
@@ -306,7 +309,7 @@ let pp_spec fmt spec =
(* const are prefixed with const in pp_var and with nothing for regular
variables. We adapt the call to produce the appropriate output. *)
fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt v ->
- fprintf fmt "const %a = %t;"
+ fprintf fmt "%a = %t;"
pp_var v
(fun fmt -> match v.var_dec_value with None -> assert false | Some e -> pp_expr fmt e)
) fmt spec.consts;
@@ -315,10 +318,10 @@ let pp_spec fmt spec =
fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt r -> fprintf fmt "assume %a;" pp_eexpr r) fmt spec.assume;
fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt r -> fprintf fmt "guarantees %a;" pp_eexpr r) fmt spec.guarantees;
fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt mode ->
- fprintf fmt "mode %s (@[@ %a@ %a@]);"
+ fprintf fmt "mode %s (@[<v 0>%a@ %a@]);"
mode.mode_id
- (fprintf_list ~eol:"@," ~sep:"@ " (fun fmt r -> fprintf fmt "require %a;" pp_eexpr r)) mode.require
- (fprintf_list ~eol:"@," ~sep:"@ " (fun fmt r -> fprintf fmt "ensure %a;" pp_eexpr r)) mode.ensure
+ (fprintf_list ~eol:"" ~sep:"@ " (fun fmt r -> fprintf fmt "require %a;" pp_eexpr r)) mode.require
+ (fprintf_list ~eol:"" ~sep:"@ " (fun fmt r -> fprintf fmt "ensure %a;" pp_eexpr r)) mode.ensure
) fmt spec.modes;
fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt import ->
fprintf fmt "import %s (%a) returns (%a);"
@@ -327,29 +330,32 @@ let pp_spec fmt spec =
pp_expr import.outputs
) fmt spec.imports
-
- let node_as_contract nd =
+(* Project the contract node as a pure contract: local memories are pushed back in the contract definition. Should mainly be used to print it *)
+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 = []);
+ (* While a processed contract shall have no locals, sttms nor
+ consts, an 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 in
{ c with
- locals = nd.node_locals;
- stmts = nd.node_stmts;
+ consts = consts @ c.consts;
+ locals = locals @ c.locals;
+ stmts = nd.node_stmts @ c.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);@ "
+ fprintf fmt "@[<v 2>(*@@ contract %s(%a) returns (%a);@ "
nd.node_id
- pp_l nd.node_inputs
- pp_l nd.node_outputs;
- fprintf fmt "let@ ";
+ pp_node_args nd.node_inputs
+ pp_node_args nd.node_outputs;
+ fprintf fmt "@[<v 2>let@ ";
pp_spec fmt c;
- fprintf fmt "tel@ @]*)@ "
+ fprintf fmt "@]@ tel@ @]*)@ "
let pp_spec_as_comment fmt (inl, outl, spec) =
match spec with
@@ -377,9 +383,9 @@ let pp_node fmt nd =
pp_node_args nd.node_inputs
pp_node_args nd.node_outputs;
(* Contracts *)
- fprintf fmt "%a%t"
+ fprintf fmt "%a"
(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 "@ ");
+ (* (fun fmt -> match nd.node_spec with None -> () | Some _ -> fprintf fmt "@ ") *);
(* Locals *)
fprintf fmt "%a" (fun fmt locals ->
match locals with [] -> () | _ ->
diff --git a/src/typing.ml b/src/typing.ml
index be1ec772..8b84e621 100644
--- a/src/typing.ml
+++ b/src/typing.ml
@@ -712,6 +712,7 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
(** [type_node env nd loc] types node [nd] in environment env. The
location is used for error reports. *)
and type_node env nd loc =
+ (* 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 vd_env_ol = if nd.node_iscontract then nd.node_locals else nd.node_outputs@nd.node_locals in
@@ -726,13 +727,11 @@ 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
@@ -749,10 +748,8 @@ 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
--
GitLab