From 70710795384a4c8dffa4dd07cbb952fed406fed1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lelio.brun@isae-supaero.fr>
Date: Wed, 25 Aug 2021 12:00:21 +0200
Subject: [PATCH] first draft with translated cocospec
---
dune-project | 2 +-
lustrec.opam | 5 +++-
src/backends/Ada/ada_backend.ml | 2 +-
src/backends/C/c_backend_spec.ml | 30 ++++++++++++---------
src/backends/EMF/EMF_backend.ml | 4 +--
src/causality.ml | 2 +-
src/compiler_common.ml | 11 ++++----
src/corelang.ml | 45 ++++++++++++++++++--------------
src/lustre_types.ml | 2 +-
src/lustre_types.mli | 2 +-
src/machine_code.ml | 11 ++++----
src/machine_code_common.ml | 12 +++++----
src/machine_code_types.mli | 7 ++++-
src/printers.ml | 2 +-
14 files changed, 79 insertions(+), 58 deletions(-)
diff --git a/dune-project b/dune-project
index cc7c384e..30fd9b40 100644
--- a/dune-project
+++ b/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.8)
+(lang dune 2.9)
(name lustrec)
(version 1.7)
diff --git a/lustrec.opam b/lustrec.opam
index cc55f8a6..de638737 100644
--- a/lustrec.opam
+++ b/lustrec.opam
@@ -25,7 +25,7 @@ depends: [
]
depopts: ["z3"]
build: [
- ["dune" "subst"] {dev}
+ ["dune" "subst" "--root" "."] {dev}
[
"dune"
"build"
@@ -33,9 +33,12 @@ build: [
name
"-j"
jobs
+ "--promote-install-files"
+ "false"
"@install"
"@runtest" {with-test}
"@doc" {with-doc}
]
+ ["dune" "install" "-p" name "--create-install-files" name]
]
dev-repo: "git+https://cavale.enseeiht.fr/git/lustrec#unstable"
diff --git a/src/backends/Ada/ada_backend.ml b/src/backends/Ada/ada_backend.ml
index a94b1b12..fde6f784 100644
--- a/src/backends/Ada/ada_backend.ml
+++ b/src/backends/Ada/ada_backend.ml
@@ -86,7 +86,7 @@ let extract_contract machines m =
l) -> assert false | Expr_appl call -> assert false *)
in
match m.mspec.mnode_spec with
- | Some (NodeSpec ident) ->
+ | Some (NodeSpec (ident, _)) ->
let machine_spec = find_submachine_from_ident ident machines in
let guarantees =
match machine_spec.mspec.mnode_spec with
diff --git a/src/backends/C/c_backend_spec.ml b/src/backends/C/c_backend_spec.ml
index bc226541..ceddd0f9 100644
--- a/src/backends/C/c_backend_spec.ml
+++ b/src/backends/C/c_backend_spec.ml
@@ -585,7 +585,7 @@ module PrintSpec = struct
fmt
((f, mk_mem_reset m), (rc, tr))
| Value v ->
- pp_c_val m mem_in (pp_c_var_read ~test_output:false m) fmt v
+ pp_c_val m mem_in (pp_c_var_read ~test_output:true m) fmt v
in
pp_spec mode
@@ -961,9 +961,10 @@ module SrcMod = struct
()
let pp_node_spec m fmt = function
- | Contract c ->
- PrintSpec.pp_spec PrintSpec.TransitionMode m fmt c
- | NodeSpec f ->
+ | Contract c
+ | NodeSpec (_, Some c) ->
+ PrintSpec.pp_spec PrintSpec.TransitionMode m fmt (Imply (c.mc_pre, c.mc_post))
+ | NodeSpec (f, None) ->
pp_print_string fmt f
let pp_step_spec fmt machines self mem m =
@@ -981,12 +982,15 @@ module SrcMod = struct
let pp_if_outputs pp =
if outputs = [] then pp_print_nothing else pp
in
- (* prevent printing an ensures clause with contract name *)
- let spec =
- match m.mspec.mnode_spec with
- | Some (NodeSpec _) -> None
- | s -> s
- in
+ let spec = m.mspec.mnode_spec in
+ (* (\* prevent printing an ensures clause with contract name *\)
+ * let spec =
+ * match m.mspec.mnode_spec with
+ * | Some (NodeSpec _) -> None
+ * | s -> s
+ * in *)
+ let pp_spec = pp_print_option
+ (if m.mis_contract then pp_print_nothing else pp_ensures (pp_node_spec m)) in
pp_acsl_cut
~ghost:m.mis_contract
(fun fmt () ->
@@ -1002,7 +1006,7 @@ module SrcMod = struct
outputs
(pp_ensures (pp_transition_aux' m))
(name, inputs @ outputs, "", "")
- (pp_print_option (pp_ensures (pp_node_spec m)))
+ pp_spec
spec
else
fprintf
@@ -1022,7 +1026,7 @@ module SrcMod = struct
(pp_transition_aux m (pp_old pp_ptr) pp_ptr (fun fmt v ->
(if is_output m v then pp_ptr_decl else pp_var_decl) fmt v)))
(name, inputs @ outputs, mem, mem)
- (pp_print_option (pp_ensures (pp_node_spec m)))
+ pp_spec
spec
(pp_assigns pp_ptr_decl)
outputs
@@ -1095,7 +1099,7 @@ module SrcMod = struct
let pp_contract fmt machines _self m =
match m.mspec.mnode_spec with
- | Some (NodeSpec f) ->
+ | Some (NodeSpec (f, _)) ->
let m_f = find_machine f machines in
pp_acsl_cut
(pp_ghost
diff --git a/src/backends/EMF/EMF_backend.ml b/src/backends/EMF/EMF_backend.ml
index a605cd13..d2353f05 100644
--- a/src/backends/EMF/EMF_backend.ml
+++ b/src/backends/EMF/EMF_backend.ml
@@ -489,7 +489,7 @@ let pp_machine fmt m =
(* TODO *)
(* assert (c.locals = [] && c.consts = [] && c.stmts = [] && c.imports = []); *)
fprintf fmt "\"spec\": %a,@ " pp_emf_spec c
- | Some (NodeSpec id) -> fprintf fmt "\"contract\": \"%s\",@ " id);
+ | Some (NodeSpec (id, _)) -> fprintf fmt "\"contract\": \"%s\",@ " id);
fprintf fmt "\"annots\": {@[<v 0> %a@]@ }"
(pp_emf_annots_list (ref 0))
m.mannot;
@@ -519,7 +519,7 @@ let pp_emf_imported_node fmt top =
(match ind.nodei_spec with
| None -> fprintf fmt "@ "
| Some (Contract _) -> assert false (* should have been processed *)
- | Some (NodeSpec id) -> fprintf fmt ",@ \"coco_contract\": %s" id);
+ | Some (NodeSpec (id, _)) -> fprintf fmt ",@ \"coco_contract\": %s" id);
fprintf fmt "@]@ }"
(* XXX: UNUSED *)
(* with Unhandled msg ->
diff --git a/src/causality.ml b/src/causality.ml
index 243447ff..3116b1ce 100644
--- a/src/causality.ml
+++ b/src/causality.ml
@@ -475,7 +475,7 @@ module NodeDep = struct
match nd.node_spec with
| None ->
[]
- | Some (NodeSpec id) ->
+ | Some (NodeSpec (id, _)) ->
[ id ]
| Some (Contract c) ->
get_contract_calls (fun _ -> true) c
diff --git a/src/compiler_common.ml b/src/compiler_common.ml
index 2c087aef..0754aa04 100644
--- a/src/compiler_common.ml
+++ b/src/compiler_common.ml
@@ -330,7 +330,8 @@ let resolve_contracts prog =
c.spec_loc
top.top_decl_owner
top.top_decl_itf
- (Node nd)
+ (Node nd),
+ c
(* { nd with
* node_dec_stateless = stateless;
* node_stateless = Some stateless;
@@ -372,11 +373,11 @@ let resolve_contracts prog =
| Some (Contract _) ->
(* A contract: processing it *)
(* we bind a fresh node *)
- let new_nd = process_contract_new_node accu_contracts prog top in
+ let new_nd, new_c = 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)) }
+ { nd with node_spec = Some (NodeSpec (node_name new_nd, Some new_c)) }
in
( new_nd :: accu_contracts,
{ top with top_decl_desc = Node nd } :: accu_nodes ))
@@ -391,9 +392,9 @@ let resolve_contracts prog =
| Some (Contract _) ->
(* A contract: processing it *)
(* we bind a fresh node *)
- let new_nd = process_contract_new_node accu_contracts prog top in
+ let new_nd, new_c = process_contract_new_node accu_contracts prog top in
let ind =
- { ind with nodei_spec = Some (NodeSpec (node_name new_nd)) }
+ { ind with nodei_spec = Some (NodeSpec (node_name new_nd, Some new_c)) }
in
( new_nd :: accu_contracts,
{ top with top_decl_desc = ImportedNode ind } :: accu_nodes ))
diff --git a/src/corelang.ml b/src/corelang.ml
index 2c546608..e25a50ea 100644
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -121,12 +121,12 @@ let mkeq loc (lhs, rhs) = { eq_lhs = lhs; eq_rhs = rhs; eq_loc = loc }
let mkassert loc expr = { assert_loc = loc; assert_expr = expr }
-let mktop_decl loc own itf d =
+let mktop_decl top_decl_loc top_decl_owner top_decl_itf top_decl_desc =
{
- top_decl_desc = d;
- top_decl_loc = loc;
- top_decl_owner = own;
- top_decl_itf = itf;
+ top_decl_desc;
+ top_decl_loc;
+ top_decl_owner;
+ top_decl_itf;
}
let mkpredef_call loc funname args =
@@ -1057,6 +1057,22 @@ let rename_import f_node f_var imp =
outputs = rename_expr imp.outputs;
}
+let rename_contract f_var f_node c =
+ let rename_var = rename_var f_var in
+ let rename_vars = List.map rename_var in
+ let rename_eexpr = rename_eexpr f_node f_var in
+ let rename_stmts = rename_stmts f_node f_var in
+ {
+ 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;
+ }
+
let rename_node f_node f_var nd =
let f_var x =
(* checking that this is actually a local variable *)
@@ -1066,7 +1082,6 @@ let rename_node f_node f_var nd =
let rename_var = rename_var 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 = rename_vars nd.node_inputs in
let outputs = rename_vars nd.node_outputs in
@@ -1087,23 +1102,13 @@ let rename_node f_node f_var nd =
let node_stmts = rename_stmts nd.node_stmts in
let spec =
- Utils.option_map
+ option_map
(fun s ->
match s with
- | NodeSpec id ->
- NodeSpec (f_node id)
+ | NodeSpec (id, oc) ->
+ NodeSpec (f_node id, option_map (rename_contract f_var f_node) oc)
| 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;
- })
+ Contract (rename_contract f_var f_node c))
nd.node_spec
in
let annot = rename_annots f_node f_var nd.node_annot in
diff --git a/src/lustre_types.ml b/src/lustre_types.ml
index 3f8b8371..a408e00e 100644
--- a/src/lustre_types.ml
+++ b/src/lustre_types.ml
@@ -162,7 +162,7 @@ type contract_desc = {
spec_loc : Location.t;
}
-type 'a node_spec_t = Contract of 'a | NodeSpec of ident
+type 'a node_spec_t = Contract of 'a | NodeSpec of ident * 'a option
type node_desc = {
node_id : ident;
diff --git a/src/lustre_types.mli b/src/lustre_types.mli
index 1ad1a88f..563efec0 100644
--- a/src/lustre_types.mli
+++ b/src/lustre_types.mli
@@ -151,7 +151,7 @@ type contract_desc = {
spec_loc : Location.t;
}
-type 'a node_spec_t = Contract of 'a | NodeSpec of ident
+type 'a node_spec_t = Contract of 'a | NodeSpec of ident * 'a option
type node_desc = {
node_id : ident;
diff --git a/src/machine_code.ml b/src/machine_code.ml
index 77f52136..48e8600f 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -514,15 +514,16 @@ let translate_eexpr env e =
e.eexpr_quantifiers
(Value (translate_expr env e.eexpr_qfexpr))
-let translate_contract env c =
- Imply (And (List.map (translate_eexpr env) c.Lustre_types.assume),
- And (List.map (translate_eexpr env) c.Lustre_types.guarantees))
+let translate_contract env c = {
+ mc_pre = And (List.map (translate_eexpr env) c.Lustre_types.assume);
+ mc_post = And (List.map (translate_eexpr env) c.Lustre_types.guarantees)
+}
let translate_spec env = function
| Contract c ->
Contract (translate_contract env c)
- | NodeSpec s ->
- NodeSpec s
+ | NodeSpec (s, c) ->
+ NodeSpec (s, option_map (translate_contract env) c)
let translate_decl nd sch =
(* Format.eprintf "Translating node %s@." nd.node_id; *)
diff --git a/src/machine_code_common.ml b/src/machine_code_common.ml
index 3f0d6f7d..306be7b4 100644
--- a/src/machine_code_common.ml
+++ b/src/machine_code_common.ml
@@ -313,9 +313,10 @@ let pp_transitions m fmt =
| _ ->
fprintf fmt "@[<v 2>transitions:@ %a@]" (pp_print_list (pp_transition m))
-let pp_mspec m fmt spec =
- fprintf fmt "@[<v>contract %a;]"
- (PrintSpec.pp_spec m) spec
+let pp_mspec m fmt c =
+ fprintf fmt "@[<v>contract: G (H (%a) => %a);]"
+ (PrintSpec.pp_spec m) c.mc_pre
+ (PrintSpec.pp_spec m) c.mc_post
let pp_machine fmt m =
fprintf
@@ -338,8 +339,9 @@ let pp_machine fmt m =
match m.mspec.mnode_spec with
| None ->
()
- | Some (NodeSpec id) ->
- fprintf fmt "cocospec: %s" id
+ | Some (NodeSpec (id, c)) ->
+ fprintf fmt "cocospec: %s@;%a" id
+ (pp_print_option (pp_mspec m)) c
| Some (Contract spec) ->
pp_mspec m fmt spec)
(pp_memory_packs m)
diff --git a/src/machine_code_types.mli b/src/machine_code_types.mli
index 25d8e732..f9bd1744 100644
--- a/src/machine_code_types.mli
+++ b/src/machine_code_types.mli
@@ -57,8 +57,13 @@ type mc_transition_t = value_t transition_t
type mc_memory_pack_t = value_t memory_pack_t
+type mc_contract_t = {
+ mc_pre: mc_formula_t;
+ mc_post: mc_formula_t;
+}
+
type machine_spec = {
- mnode_spec : mc_formula_t node_spec_t option;
+ mnode_spec : mc_contract_t node_spec_t option;
mtransitions : mc_transition_t list;
mmemory_packs : mc_memory_pack_t list;
}
diff --git a/src/printers.ml b/src/printers.ml
index 15bae926..4b6e89c4 100644
--- a/src/printers.ml
+++ b/src/printers.ml
@@ -581,7 +581,7 @@ let pp_spec_as_comment fmt (inl, outl, spec) =
fprintf fmt "@[<hov 2>(*@contract@ ";
pp_spec fmt c;
fprintf fmt "@]*)@ "
- | NodeSpec name ->
+ | NodeSpec (name, _) ->
(* Pushing stmts in contract. We update the original information with the
computed one in nd. *)
let pp_l = pp_comma_list pp_var_name in
--
GitLab