From 5b98398a7783a5702467d5fd8e2c5f6c2ef66aa2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lelio.brun@isae-supaero.fr>
Date: Thu, 29 Jul 2021 16:02:24 +0200
Subject: [PATCH] first version working with stateless contracts
---
src/backends/Ada/ada_backend.ml | 12 ++--
src/backends/C/c_backend_common.ml | 24 ++++----
src/backends/C/c_backend_common.mli | 1 +
src/backends/C/c_backend_header.ml | 69 ++++++++++-----------
src/backends/C/c_backend_spec.ml | 81 +++++++++++++++++++++----
src/backends/C/c_backend_src.ml | 18 +++++-
src/backends/C/c_backend_src.mli | 2 +
src/backends/EMF/EMF_backend.ml | 14 +++--
src/clocks.ml | 5 +-
src/compiler_common.ml | 55 ++++++++---------
src/corelang.ml | 8 ++-
src/corelang.mli | 1 +
src/lustre_types.ml | 8 ++-
src/lustre_types.mli | 8 ++-
src/machine_code.ml | 21 ++++++-
src/machine_code_common.ml | 11 +++-
src/machine_code_types.mli | 3 +-
src/normalization.ml | 94 +++++++++++++++++------------
src/normalization.mli | 2 +-
src/optimize_machine.ml | 2 +-
src/parsers/parser_lustre.mly | 3 +-
src/printers.ml | 92 ++++++++++++++--------------
src/sortProg.ml | 2 +-
src/spec_types.ml | 1 +
src/spec_types.mli | 1 +
src/types.ml | 5 +-
src/typing.ml | 5 +-
27 files changed, 343 insertions(+), 205 deletions(-)
diff --git a/src/backends/Ada/ada_backend.ml b/src/backends/Ada/ada_backend.ml
index 065ffa71..a94b1b12 100644
--- a/src/backends/Ada/ada_backend.ml
+++ b/src/backends/Ada/ada_backend.ml
@@ -91,11 +91,13 @@ let extract_contract machines m =
let guarantees =
match machine_spec.mspec.mnode_spec with
| Some (Contract contract) ->
- assert (contract.consts = []);
- assert (contract.locals = []);
- assert (contract.stmts = []);
- assert (contract.assume = []);
- List.map extract_ident contract.guarantees
+ (* assert (contract.consts = []);
+ * assert (contract.locals = []);
+ * assert (contract.stmts = []);
+ * assert (contract.assume = []);
+ * List.map extract_ident contract.guarantees *)
+ (* TODO *)
+ assert false
| _ ->
assert false
in
diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml
index ea86dbbb..b3d00c13 100644
--- a/src/backends/C/c_backend_common.ml
+++ b/src/backends/C/c_backend_common.ml
@@ -98,6 +98,7 @@ let mk_call_var_decl loc id =
var_type = Type_predef.type_arrow (Types.new_var ()) (Types.new_var ());
var_clock = Clocks.new_var true;
var_loc = loc;
+ var_is_contract = false;
}
(* counter for loop variable creation *)
@@ -269,14 +270,15 @@ let pp_basic_c_type ?(pp_c_basic_type_desc = pp_c_basic_type_desc) ?var_opt fmt
| _ ->
fprintf fmt "%s" (pp_c_basic_type_desc t)
-let pp_c_type ?pp_c_basic_type_desc ?var_opt var_id fmt t =
+let pp_c_type ?(var_is_contract=false) ?pp_c_basic_type_desc ?var_opt var_id fmt t =
let rec aux t pp_suffix =
if is_basic_c_type t then
fprintf
fmt
- "%a %s%a"
+ "%a %s%s%a"
(pp_basic_c_type ?pp_c_basic_type_desc ?var_opt)
t
+ (if var_is_contract then "\\ghost " else "")
var_id
pp_suffix
()
@@ -431,9 +433,10 @@ let pp_c_decl_input_var fmt id =
the case for generics *)
let pp_c_decl_output_var fmt id =
if (not !Options.ansi) && Types.is_address_type id.var_type then
- pp_c_type ~var_opt:id id.var_id fmt id.var_type
+ pp_c_type ~var_is_contract:id.var_is_contract ~var_opt:id id.var_id fmt id.var_type
else
pp_c_type
+ ~var_is_contract:id.var_is_contract
~var_opt:id
(sprintf "(*%s)" id.var_id)
fmt
@@ -882,12 +885,10 @@ module Protos (Mod : MODIFIERS_GHOST_PROTO) = struct
"@[<v>void %a (@[<v>%a%a%a *%s@])%a@]"
pp_machine_step_name
name
- (pp_comma_list
- ~pp_eol:pp_print_comma
- ~pp_epilogue:pp_print_cut
- pp_c_decl_input_var)
+ (pp_comma_list pp_c_decl_input_var)
inputs
(pp_comma_list
+ ~pp_prologue:pp_print_comma
~pp_eol:pp_print_comma
~pp_epilogue:pp_print_cut
pp_c_decl_output_var)
@@ -928,12 +929,11 @@ module Protos (Mod : MODIFIERS_GHOST_PROTO) = struct
"void %a (@[<v>%a%a@])"
pp_machine_step_name
name
- (pp_comma_list
- ~pp_eol:pp_print_comma
- ~pp_epilogue:pp_print_cut
- pp_c_decl_input_var)
+ (pp_comma_list pp_c_decl_input_var)
inputs
- (pp_comma_list pp_c_decl_output_var)
+ (pp_comma_list
+ ~pp_prologue:pp_print_comma
+ pp_c_decl_output_var)
outputs
end
diff --git a/src/backends/C/c_backend_common.mli b/src/backends/C/c_backend_common.mli
index a5a934ed..6243b45d 100644
--- a/src/backends/C/c_backend_common.mli
+++ b/src/backends/C/c_backend_common.mli
@@ -77,6 +77,7 @@ val pp_assign :
unit
val pp_c_type :
+ ?var_is_contract:bool ->
?pp_c_basic_type_desc:(Types.t -> string) ->
?var_opt:var_decl ->
ident ->
diff --git a/src/backends/C/c_backend_header.ml b/src/backends/C/c_backend_header.ml
index f926e84d..e6b9363f 100644
--- a/src/backends/C/c_backend_header.ml
+++ b/src/backends/C/c_backend_header.ml
@@ -119,40 +119,41 @@ functor
let inode = imported_node_of_top tdecl in
(*Mod.print_machine_decl_prefix fmt m;*)
let prototype = inode.nodei_id, inode.nodei_inputs, inode.nodei_outputs in
- if inode.nodei_prototype = Some "C" then
- if inode.nodei_stateless then
- fprintf fmt "extern %a;" pp_stateless_C_prototype prototype
- else (
- (* TODO: raise proper error *)
- Format.eprintf "internal error: pp_machine_decl_top_decl_from_header";
- assert false)
- else if inode.nodei_stateless then
- fprintf fmt "extern %a;" Protos.pp_stateless_prototype prototype
- else
- let static_inputs =
- List.filter (fun v -> v.var_dec_const) inode.nodei_inputs
- in
- let used name =
- List.exists
- (fun v -> v.var_id = name)
- (inode.nodei_inputs @ inode.nodei_outputs)
- in
- let self = mk_new_name used "self" in
- let mem = mk_new_name used "mem" in
- let static_prototype = inode.nodei_id, static_inputs in
- fprintf
- fmt
- "extern %a;@,extern %a;@,extern %a;@,extern %a;@,extern %a;"
- (Protos.pp_set_reset_prototype self mem)
- static_prototype
- (Protos.pp_clear_reset_prototype self mem)
- static_prototype
- (Protos.pp_init_prototype self)
- static_prototype
- (Protos.pp_clear_prototype self)
- static_prototype
- (Protos.pp_step_prototype self mem)
- prototype
+ if not inode.nodei_iscontract then
+ if inode.nodei_prototype = Some "C" then
+ if inode.nodei_stateless then
+ fprintf fmt "extern %a;" pp_stateless_C_prototype prototype
+ else (
+ (* TODO: raise proper error *)
+ Format.eprintf "internal error: pp_machine_decl_top_decl_from_header";
+ assert false)
+ else if inode.nodei_stateless then
+ fprintf fmt "extern %a;" Protos.pp_stateless_prototype prototype
+ else
+ let static_inputs =
+ List.filter (fun v -> v.var_dec_const) inode.nodei_inputs
+ in
+ let used name =
+ List.exists
+ (fun v -> v.var_id = name)
+ (inode.nodei_inputs @ inode.nodei_outputs)
+ in
+ let self = mk_new_name used "self" in
+ let mem = mk_new_name used "mem" in
+ let static_prototype = inode.nodei_id, static_inputs in
+ fprintf
+ fmt
+ "extern %a;@,extern %a;@,extern %a;@,extern %a;@,extern %a;"
+ (Protos.pp_set_reset_prototype self mem)
+ static_prototype
+ (Protos.pp_clear_reset_prototype self mem)
+ static_prototype
+ (Protos.pp_init_prototype self)
+ static_prototype
+ (Protos.pp_clear_prototype self)
+ static_prototype
+ (Protos.pp_step_prototype self mem)
+ prototype
let pp_const_top_decl fmt tdecl =
let cdecl = const_of_top tdecl in
diff --git a/src/backends/C/c_backend_spec.ml b/src/backends/C/c_backend_spec.ml
index ace5f218..bc226541 100644
--- a/src/backends/C/c_backend_spec.ml
+++ b/src/backends/C/c_backend_spec.ml
@@ -35,13 +35,19 @@ let pp_acsl_basic_type_desc t_desc =
else assert false
(* Not a basic C type. Do not handle arrays or pointers *)
-let pp_acsl pp fmt = fprintf fmt "@[<v>/*%@ @[<v>%a@]@,*/@]" pp
+let pp_acsl ?(ghost=false) pp fmt x =
+ let op = if ghost then "" else "*" in
+ let cl = if ghost then "@" else "*" in
+ fprintf fmt "@[<v>/%s%@ @[<v>%a@]@,%s/@]" op pp x cl
-let pp_acsl_cut pp fmt = fprintf fmt "%a@," (pp_acsl pp)
+let pp_acsl_cut ?ghost pp fmt = fprintf fmt "%a@," (pp_acsl ?ghost pp)
let pp_acsl_line pp fmt = fprintf fmt "//%@ @[<h>%a@]" pp
-let pp_acsl_line' pp fmt = fprintf fmt "/*%@ @[<h>%a@] */" pp
+let pp_acsl_line' ?(ghost=false) pp fmt x =
+ let op = if ghost then "" else "*" in
+ let cl = if ghost then "@" else "*" in
+ fprintf fmt "/%s%@ @[<h>%a@] %s/" op pp x cl
let pp_acsl_line'_cut pp fmt = fprintf fmt "%a@," (pp_acsl_line' pp)
@@ -101,6 +107,9 @@ let pp_stdout fmt () = pp_print_string fmt "stdout"
let pp_at pp_v fmt (v, l) = fprintf fmt "\\at(%a, %s)" pp_v v l
+let find_machine f =
+ List.find (fun m -> m.mname.node_id = f)
+
let instances machines m =
let open List in
let grow paths i td mems =
@@ -114,7 +123,7 @@ let instances machines m =
map
(fun (i, (td, _)) ->
try
- let m = find (fun m -> m.mname.node_id = node_name td) machines in
+ let m = find_machine (node_name td) machines in
aux (grow paths i td m.mmemory) m
with Not_found -> grow paths i td [])
m.minstances
@@ -161,14 +170,14 @@ let powerset_instances paths =
let pp_separated pp_self pp_mem pp_ptr fmt (self, mem, paths, ptrs) =
fprintf
fmt
- "\\separated(@[<v>%a, %a@;%a@;%a@])"
+ "\\separated(@[<v>%a, %a%a%a@])"
pp_self
self
pp_mem
mem
- (pp_comma_list ~pp_prologue:pp_print_comma' (pp_instance pp_self self))
+ (pp_comma_list ~pp_prologue:pp_print_comma (pp_instance pp_self self))
paths
- (pp_comma_list ~pp_prologue:pp_print_comma' pp_ptr)
+ (pp_comma_list ~pp_prologue:pp_print_comma pp_ptr)
ptrs
let pp_separated' self mem fmt (paths, ptrs) =
@@ -575,6 +584,9 @@ module PrintSpec = struct
(pp_and (pp_spec ResetOut) (pp_spec ResetIn))
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
+
in
pp_spec mode
end
@@ -948,6 +960,12 @@ module SrcMod = struct
fmt
()
+ let pp_node_spec m fmt = function
+ | Contract c ->
+ PrintSpec.pp_spec PrintSpec.TransitionMode m fmt c
+ | NodeSpec f ->
+ pp_print_string fmt f
+
let pp_step_spec fmt machines self mem m =
let name = m.mname.node_id in
let insts = instances machines m in
@@ -960,25 +978,37 @@ module SrcMod = struct
in
let inputs = m.mstep.step_inputs in
let outputs = m.mstep.step_outputs in
+ 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
pp_acsl_cut
+ ~ghost:m.mis_contract
(fun fmt () ->
if fst (get_stateless_status m) then
fprintf
fmt
- "%a@,%a@,%a@,%a"
- (pp_requires (pp_valid pp_var_decl))
+ "%a@,%a@,%a@,%a@,%a"
+ (pp_if_outputs (pp_requires (pp_valid pp_var_decl)))
outputs
- (pp_requires pp_separated'')
+ (pp_if_outputs (pp_requires pp_separated''))
outputs
(pp_assigns pp_ptr_decl)
outputs
(pp_ensures (pp_transition_aux' m))
(name, inputs @ outputs, "", "")
+ (pp_print_option (pp_ensures (pp_node_spec m)))
+ spec
else
fprintf
fmt
- "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a"
- (pp_requires (pp_valid pp_var_decl))
+ "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a"
+ (pp_if_outputs (pp_requires (pp_valid pp_var_decl)))
outputs
(pp_requires pp_mem_valid')
(name, self)
@@ -992,6 +1022,8 @@ 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)))
+ spec
(pp_assigns pp_ptr_decl)
outputs
(pp_assigns (pp_reg self))
@@ -1039,6 +1071,7 @@ module SrcMod = struct
()
let pp_step_instr_spec m self mem fmt instr =
+ let ghost = m.mis_contract in
fprintf
fmt
"%a%a"
@@ -1047,7 +1080,7 @@ module SrcMod = struct
(pp_print_list
~pp_open_box:pp_open_vbox0
~pp_prologue:pp_print_cut
- (pp_acsl_line' (pp_assert (PrintSpec.pp_spec (InstrMode self) m))))
+ (pp_acsl_line' ~ghost (pp_assert (PrintSpec.pp_spec (InstrMode self) m))))
instr.instr_spec
let pp_ghost_parameter mem fmt inst =
@@ -1059,6 +1092,28 @@ module SrcMod = struct
[ (inst, fun fmt inst -> pp_ref pp_indirect' fmt (mem, inst)) ]
| None ->
[ mem, pp_print_string ])
+
+ let pp_contract fmt machines _self m =
+ match m.mspec.mnode_spec with
+ | Some (NodeSpec f) ->
+ let m_f = find_machine f machines in
+ pp_acsl_cut
+ (pp_ghost
+ (fun fmt () ->
+ fprintf
+ fmt
+ "@;<0 2>@[<v>%a%a(%a%a);@]"
+ (pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_semicolon ~pp_eol:pp_print_semicolon (pp_c_decl_local_var m))
+ m_f.mstep.step_outputs
+ pp_machine_step_name
+ m_f.mname.node_id
+ (pp_comma_list ~pp_eol:pp_print_comma (pp_c_var_read m))
+ m_f.mstep.step_inputs
+ (pp_comma_list (pp_c_var_write m))
+ m_f.mstep.step_outputs))
+ fmt ()
+ | _ -> ()
+
end
module MainMod = struct
diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index b1428331..f3dbce18 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/src/backends/C/c_backend_src.ml
@@ -34,6 +34,8 @@ module type MODIFIERS_SRC = sig
machine_t -> ident -> ident -> formatter -> instr_t -> unit
val pp_ghost_parameter : ident -> formatter -> ident option -> unit
+
+ val pp_contract : formatter -> machine_t list -> ident -> machine_t -> unit
end
module EmptyMod = struct
@@ -50,6 +52,8 @@ module EmptyMod = struct
let pp_step_instr_spec _ _ _ _ _ = ()
let pp_ghost_parameter _ _ _ = ()
+
+ let pp_contract _ _ _ _ = ()
end
module Main (Mod : MODIFIERS_SRC) = struct
@@ -537,7 +541,8 @@ module Main (Mod : MODIFIERS_SRC) = struct
(pp_c_val m self (pp_c_var_read m))
check
- let pp_print_function ~pp_prototype ~prototype ?(pp_spec = pp_print_nothing)
+ let pp_print_function ~pp_prototype ~prototype ?(is_contract = false)
+ ?(pp_spec = pp_print_nothing)
?(pp_local = pp_print_nothing) ?(base_locals = [])
?(pp_array_mem = pp_print_nothing) ?(array_mems = [])
?(pp_init_mpfr_local = pp_print_nothing)
@@ -547,7 +552,8 @@ module Main (Mod : MODIFIERS_SRC) = struct
?(pp_instr = fun fmt _ -> pp_print_nothing fmt ()) ?(instrs = []) fmt =
fprintf
fmt
- "%a@[<v 2>%a {@,%a%a%a%a%a%a%areturn;@]@,}"
+ "%t%a@[<v 2>%a {@,%a%a%a%a%a%a%areturn;@]@,}%t"
+ (fun fmt -> if is_contract then fprintf fmt "@[<v 2>/*%@ ghost@;")
pp_spec
()
pp_prototype
@@ -583,6 +589,7 @@ module Main (Mod : MODIFIERS_SRC) = struct
(mpfr_vars mpfr_locals) (* extra *)
pp_extra
()
+ (fun fmt -> if is_contract then fprintf fmt "@]@;*/")
let node_of_machine m =
{
@@ -594,9 +601,11 @@ module Main (Mod : MODIFIERS_SRC) = struct
let pp_stateless_code machines dependencies fmt m =
let self = "__ERROR__" in
+ let is_contract = m.mis_contract in
if not (!Options.ansi && is_generic_node (node_of_machine m)) then
(* C99 code *)
pp_print_function
+ ~is_contract
~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self self m)
~pp_prototype:Protos.pp_stateless_prototype
~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
@@ -609,6 +618,7 @@ module Main (Mod : MODIFIERS_SRC) = struct
~checks:m.mstep.step_checks
~pp_instr:(pp_machine_instr dependencies m self self)
~instrs:m.mstep.step_instrs
+ ~pp_extra:(fun fmt () -> Mod.pp_contract fmt machines self m)
fmt
else
(* C90 code *)
@@ -625,6 +635,7 @@ module Main (Mod : MODIFIERS_SRC) = struct
m.mname.node_gencalls
in
pp_print_function
+ ~is_contract
~pp_prototype:Protos.pp_stateless_prototype
~prototype:
( m.mname.node_id,
@@ -639,6 +650,7 @@ module Main (Mod : MODIFIERS_SRC) = struct
~checks:m.mstep.step_checks
~pp_instr:(pp_machine_instr dependencies m self self)
~instrs:m.mstep.step_instrs
+ ~pp_extra:(fun fmt () -> Mod.pp_contract fmt machines self m)
fmt
let pp_clear_reset_code dependencies self mem fmt m =
@@ -730,6 +742,7 @@ module Main (Mod : MODIFIERS_SRC) = struct
~checks:m.mstep.step_checks
~pp_instr:(pp_machine_instr dependencies m self mem)
~instrs:m.mstep.step_instrs
+ ~pp_extra:(fun fmt () -> Mod.pp_contract fmt machines self m)
fmt
else
(* C90 code *)
@@ -761,6 +774,7 @@ module Main (Mod : MODIFIERS_SRC) = struct
~checks:m.mstep.step_checks
~pp_instr:(pp_machine_instr dependencies m self mem)
~instrs:m.mstep.step_instrs
+ ~pp_extra:(fun fmt () -> Mod.pp_contract fmt machines self m)
fmt
(********************************************************************************************)
diff --git a/src/backends/C/c_backend_src.mli b/src/backends/C/c_backend_src.mli
index a51a0beb..2eb4add1 100644
--- a/src/backends/C/c_backend_src.mli
+++ b/src/backends/C/c_backend_src.mli
@@ -20,6 +20,8 @@ module type MODIFIERS_SRC = sig
machine_t -> ident -> ident -> formatter -> instr_t -> unit
val pp_ghost_parameter : ident -> formatter -> ident option -> unit
+
+ val pp_contract : formatter -> machine_t list -> ident -> machine_t -> unit
end
module EmptyMod : MODIFIERS_SRC
diff --git a/src/backends/EMF/EMF_backend.ml b/src/backends/EMF/EMF_backend.ml
index db2a361d..a605cd13 100644
--- a/src/backends/EMF/EMF_backend.ml
+++ b/src/backends/EMF/EMF_backend.ml
@@ -438,10 +438,13 @@ let pp_emf_spec fmt spec =
* pp_emf_vars_decl spec.locals;
* fprintf fmt "\"stmts\": [%a],@ "
* pp_emf_stmts spec.stmts; *)
- fprintf fmt "\"assume\": [%a],@ " pp_emf_eexprs spec.assume;
- fprintf fmt "\"guarantees\": [%a],@ " pp_emf_eexprs spec.guarantees;
- fprintf fmt "\"modes\": [%a]@ " pp_emf_spec_modes spec.modes;
- (* fprintf fmt "\"imports\": [%a]@ "
+
+ (* TODO *)
+ (* fprintf fmt "\"assume\": [%a],@ " pp_emf_eexprs spec.assume;
+ * fprintf fmt "\"guarantees\": [%a],@ " pp_emf_eexprs spec.guarantees;
+ * fprintf fmt "\"modes\": [%a]@ " pp_emf_spec_modes spec.modes; *)
+
+ (* fprintf fmt "\"imports\": [%a]@ "
* pp_emf_spec_imports spec.imports; *)
fprintf fmt "@] }"
@@ -483,7 +486,8 @@ let pp_machine fmt m =
(match m.mspec.mnode_spec with
| None -> ()
| Some (Contract c) ->
- assert (c.locals = [] && c.consts = [] && c.stmts = [] && c.imports = []);
+ (* 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);
fprintf fmt "\"annots\": {@[<v 0> %a@]@ }"
diff --git a/src/clocks.ml b/src/clocks.ml
index 6a04ed1d..d90a8492 100644
--- a/src/clocks.ml
+++ b/src/clocks.ml
@@ -204,8 +204,9 @@ let split_arrow ck =
failwith "Internal error: not an arrow clock"
(** Returns the clock corresponding to a clock list. *)
-let clock_of_clock_list ckl =
- if List.length ckl > 1 then new_ck (Ctuple ckl) true else List.hd ckl
+let clock_of_clock_list = function
+ | [ck] -> ck
+ | ckl -> new_ck (Ctuple ckl) true
let clock_list_of_clock ck =
match (repr ck).cdesc with Ctuple cl -> cl | _ -> [ ck ]
diff --git a/src/compiler_common.ml b/src/compiler_common.ml
index 89a68947..2c087aef 100644
--- a/src/compiler_common.ml
+++ b/src/compiler_common.ml
@@ -289,7 +289,7 @@ let resolve_contracts prog =
in
(* Format.eprintf "Process contract new node for node %s@." id; *)
- let stmts, locals, c =
+ let node_stmts, node_locals, c =
match spec with
| None | Some (NodeSpec _) ->
assert false
@@ -308,32 +308,33 @@ let resolve_contracts prog =
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
+ let nd = {
+ node_id = mk_new_name used (id ^ "_contract");
+ node_type = Types.new_var ();
+ node_clock = Clocks.new_var true;
+ node_inputs = inputs @ outputs;
+ node_outputs = [];
+ node_locals;
+ node_gencalls = [];
+ node_checks = [];
+ node_asserts = [];
+ node_stmts;
+ node_dec_stateless = false;
+ node_stateless = None;
+ node_spec = Some (Contract c);
+ node_annot = [];
+ node_iscontract = true;
+ } in
+ (* let stateless = Stateless.compute_node nd in *)
+ mktop_decl
+ c.spec_loc
+ top.top_decl_owner
+ top.top_decl_itf
+ (Node nd)
+ (* { nd with
+ * node_dec_stateless = stateless;
+ * node_stateless = Some stateless;
+ * }) *)
in
(* Processing nodes in order. Should have been sorted by now
diff --git a/src/corelang.ml b/src/corelang.ml
index b20dd867..2c546608 100644
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -53,7 +53,7 @@ let mktyp loc d = { ty_dec_desc = d; ty_dec_loc = loc }
let mkclock loc d = { ck_dec_desc = d; ck_dec_loc = loc }
-let mkvar_decl loc ?(orig = false)
+let mkvar_decl loc ?(var_is_contract=false) ?(orig = false)
(id, ty_dec, ck_dec, is_const, value, parentid) =
assert (value = None || is_const);
{
@@ -67,6 +67,7 @@ let mkvar_decl loc ?(orig = false)
var_type = Types.new_var ();
var_clock = Clocks.new_var true;
var_loc = loc;
+ var_is_contract
}
let dummy_var_decl name typ =
@@ -81,6 +82,7 @@ let dummy_var_decl name typ =
var_type = typ;
var_clock = Clocks.new_ck Clocks.Cvar true;
var_loc = Location.dummy;
+ var_is_contract = false;
}
let mkexpr loc d =
@@ -106,6 +108,7 @@ let var_decl_of_const ?(parentid = None) c =
var_type = c.const_type;
var_clock = Clocks.new_var false;
var_loc = c.const_loc;
+ var_is_contract = false;
}
let mk_new_name used id =
@@ -845,6 +848,7 @@ let get_node_interface nd =
(* nodei_annot = nd.node_annot; *)
nodei_prototype = None;
nodei_in_lib = [];
+ nodei_iscontract = nd.node_iscontract;
}
(************************************************************************)
@@ -1267,6 +1271,7 @@ let mk_internal_node id =
(* nodei_annot = []; *)
nodei_prototype = None;
nodei_in_lib = [];
+ nodei_iscontract = false;
})
let add_internal_funs () =
@@ -1540,6 +1545,7 @@ let mk_fresh_var (parentid, ctx_env) loc ty ck =
var_type = ty;
var_clock = ck;
var_loc = loc;
+ var_is_contract = false;
}
in
aux ()
diff --git a/src/corelang.mli b/src/corelang.mli
index 2bd3923a..8fa4fedf 100644
--- a/src/corelang.mli
+++ b/src/corelang.mli
@@ -37,6 +37,7 @@ val mkclock : Location.t -> clock_dec_desc -> clock_dec
val mkvar_decl :
Location.t ->
+ ?var_is_contract:bool ->
?orig:bool ->
ident
* type_dec
diff --git a/src/lustre_types.ml b/src/lustre_types.ml
index 824193cc..3f8b8371 100644
--- a/src/lustre_types.ml
+++ b/src/lustre_types.ml
@@ -59,6 +59,7 @@ type var_decl = {
mutable var_type : Types.t;
mutable var_clock : Clocks.t;
var_loc : Location.t;
+ var_is_contract: bool;
}
(* The tag of an expression is a unique identifier used to distinguish different
instances of the same node *)
@@ -161,7 +162,7 @@ type contract_desc = {
spec_loc : Location.t;
}
-type node_spec_t = Contract of contract_desc | NodeSpec of ident
+type 'a node_spec_t = Contract of 'a | NodeSpec of ident
type node_desc = {
node_id : ident;
@@ -176,7 +177,7 @@ type node_desc = {
node_stmts : statement list;
mutable node_dec_stateless : bool;
mutable node_stateless : bool option;
- node_spec : node_spec_t option;
+ node_spec : contract_desc node_spec_t option;
node_annot : expr_annot list;
node_iscontract : bool;
}
@@ -188,10 +189,11 @@ type imported_node_desc = {
nodei_inputs : var_decl list;
nodei_outputs : var_decl list;
nodei_stateless : bool;
- nodei_spec : node_spec_t option;
+ nodei_spec : contract_desc node_spec_t option;
(* nodei_annot: expr_annot list; *)
nodei_prototype : string option;
nodei_in_lib : string list;
+ nodei_iscontract : bool;
}
type const_desc = {
diff --git a/src/lustre_types.mli b/src/lustre_types.mli
index 07b760b4..1ad1a88f 100644
--- a/src/lustre_types.mli
+++ b/src/lustre_types.mli
@@ -48,6 +48,7 @@ type var_decl = {
mutable var_type : Types.t;
mutable var_clock : Clocks.t;
var_loc : Location.t;
+ var_is_contract: bool;
}
(* The tag of an expression is a unique identifier used to distinguish different
instances of the same node *)
@@ -150,7 +151,7 @@ type contract_desc = {
spec_loc : Location.t;
}
-type node_spec_t = Contract of contract_desc | NodeSpec of ident
+type 'a node_spec_t = Contract of 'a | NodeSpec of ident
type node_desc = {
node_id : ident;
@@ -165,7 +166,7 @@ type node_desc = {
node_stmts : statement list;
mutable node_dec_stateless : bool;
mutable node_stateless : bool option;
- node_spec : node_spec_t option;
+ node_spec : contract_desc node_spec_t option;
node_annot : expr_annot list;
node_iscontract : bool;
}
@@ -177,10 +178,11 @@ type imported_node_desc = {
nodei_inputs : var_decl list;
nodei_outputs : var_decl list;
nodei_stateless : bool;
- nodei_spec : node_spec_t option;
+ nodei_spec : contract_desc node_spec_t option;
(* nodei_annot: expr_annot list; *)
nodei_prototype : string option;
nodei_in_lib : string list;
+ nodei_iscontract : bool;
}
type const_desc = {
diff --git a/src/machine_code.ml b/src/machine_code.ml
index b7c4ac4f..77f52136 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -507,6 +507,23 @@ let transition_toplevel nd i =
tinst_footprint = IMap.empty;
}
+let translate_eexpr env e =
+ List.fold_right (fun (qt, xs) f -> match qt with
+ | Lustre_types.Exists -> Exists (xs, f)
+ | Lustre_types.Forall -> Forall (xs, f))
+ 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_spec env = function
+ | Contract c ->
+ Contract (translate_contract env c)
+ | NodeSpec s ->
+ NodeSpec s
+
let translate_decl nd sch =
(* Format.eprintf "Translating node %s@." nd.node_id; *)
(* Extracting eqs, variables .. *)
@@ -591,6 +608,7 @@ let translate_decl nd sch =
@ [ mk_transition ~i:0 nd.node_id (vdecls_to_vals nd.node_inputs) ])
MClearReset
in
+ let mnode_spec = Utils.option_map (translate_spec env) nd.node_spec in
{
mname = nd;
mmemory = VSet.elements mems;
@@ -624,9 +642,10 @@ let translate_decl nd sch =
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 = { mnode_spec = nd.node_spec; mtransitions; mmemory_packs };
+ mspec = { mnode_spec; mtransitions; mmemory_packs };
mannot = nd.node_annot;
msch = Some sch;
+ mis_contract = nd.node_iscontract
}
(** takes the global declarations and the scheduling associated to each node *)
diff --git a/src/machine_code_common.ml b/src/machine_code_common.ml
index 420c04f9..3f0d6f7d 100644
--- a/src/machine_code_common.ml
+++ b/src/machine_code_common.ml
@@ -158,6 +158,9 @@ module PrintSpec = struct
fprintf fmt "StateVarPack<%a>" pp_reg r
| ExistsMem (_f, a, b) ->
fprintf fmt "@[<hv 2>∃ MEM,@ %a@]" pp_spec (And [ a; b ])
+ | Value v ->
+ pp_val m fmt v
+
in
pp_spec
end
@@ -310,6 +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_machine fmt m =
fprintf
fmt
@@ -334,7 +341,7 @@ let pp_machine fmt m =
| Some (NodeSpec id) ->
fprintf fmt "cocospec: %s" id
| Some (Contract spec) ->
- Printers.pp_spec fmt spec)
+ pp_mspec m fmt spec)
(pp_memory_packs m)
m.mspec.mmemory_packs
(pp_transitions m)
@@ -444,6 +451,7 @@ let arrow_machine =
mspec = { mnode_spec = None; mtransitions = []; mmemory_packs = [] };
mannot = [];
msch = None;
+ mis_contract = false
}
let empty_desc =
@@ -486,6 +494,7 @@ let empty_machine =
mspec = { mnode_spec = None; mtransitions = []; mmemory_packs = [] };
mannot = [];
msch = None;
+ mis_contract = false
}
let new_instance =
diff --git a/src/machine_code_types.mli b/src/machine_code_types.mli
index 7f2ecfaa..25d8e732 100644
--- a/src/machine_code_types.mli
+++ b/src/machine_code_types.mli
@@ -58,7 +58,7 @@ type mc_transition_t = value_t transition_t
type mc_memory_pack_t = value_t memory_pack_t
type machine_spec = {
- mnode_spec : node_spec_t option;
+ mnode_spec : mc_formula_t node_spec_t option;
mtransitions : mc_transition_t list;
mmemory_packs : mc_memory_pack_t list;
}
@@ -79,4 +79,5 @@ type machine_t = {
mspec : machine_spec;
mannot : expr_annot list;
msch : Scheduling_type.schedule_report option; (* Equations scheduling *)
+ mis_contract: bool
}
diff --git a/src/normalization.ml b/src/normalization.ml
index 2226e942..7e2b3aff 100644
--- a/src/normalization.ml
+++ b/src/normalization.ml
@@ -507,18 +507,18 @@ let normalize_eq_split norm_ctx defvars eq =
let normalize_pred_eexpr norm_ctx (def, vars) ee =
assert (ee.eexpr_quantifiers = []);
(* We do not normalize quantifiers yet. This is for very far future. *)
- (* don't do anything is eexpr is just a variable *)
- let skip =
- match ee.eexpr_qfexpr.expr_desc with
- | Expr_ident _ | Expr_const _ -> true
- | _ -> false
- in
- if skip then ee, (def, vars)
- else
+ (* (\* don't do anything if eexpr is just a variable *\)
+ * let skip =
+ * match ee.eexpr_qfexpr.expr_desc with
+ * | Expr_ident _ | Expr_const _ -> true
+ * | _ -> false
+ * in
+ * if skip then None, ee, (def, vars)
+ * else *)
(* New output variable *)
let output_id = "spec" ^ string_of_int ee.eexpr_tag in
let output_var =
- mkvar_decl ee.eexpr_loc
+ mkvar_decl ~var_is_contract:true ee.eexpr_loc
( output_id,
mktyp ee.eexpr_loc Tydec_bool,
(* It is a predicate, hence a bool *)
@@ -527,6 +527,8 @@ let normalize_pred_eexpr norm_ctx (def, vars) ee =
None,
None )
in
+ (* It is a predicate, hence a bool *)
+ output_var.var_type <- Type_predef.type_bool;
let output_expr = expr_of_vdecl output_var in
(* Rebuilding an eexpr with a silly expression, just a variable *)
let ee' = { ee with eexpr_qfexpr = output_expr } in
@@ -550,7 +552,7 @@ let normalize_pred_eexpr norm_ctx (def, vars) ee =
let defs, vars =
List.fold_left (normalize_eq_split norm_ctx) (def, vars) [ eq ]
in
- let vars = output_var :: vars in
+ (* let vars = output_var :: vars in *)
(* let todefine =
List.fold_left
@@ -575,7 +577,7 @@ let normalize_pred_eexpr norm_ctx (def, vars) ee =
(*Format.eprintf "normalized eqs %a@.@?"
(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs; *)
*)
- ee', (defs, vars)
+ output_var, ee', (defs, vars)
with Types.Error (loc, err) as exc ->
eprintf "Typing error for eexpr %a: %a%a%a@." Printers.pp_eexpr ee
Types.pp_error err
@@ -666,30 +668,33 @@ let normalize_spec parentid (in_vars, out_vars, l_vars) s =
(* 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 norm_ctx defvars ee in
- ee' :: accu, defvars)
- l ([], defvars)
+ (fun ee (outputs, accu, defvars) ->
+ let x, ee', defvars = normalize_pred_eexpr norm_ctx defvars ee in
+ x :: outputs, 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
- let assume', defsvars = process_predicates s.assume defsvars in
- let guarantees', defsvars = process_predicates s.guarantees defsvars in
- let modes', (defs, vars) =
+ let outs_asm, assume', defsvars = process_predicates s.assume defsvars in
+ let outs_grt, guarantees', defsvars = process_predicates s.guarantees defsvars in
+ let outs, modes', (defs, vars) =
List.fold_right
- (fun m (accu_m, defsvars) ->
- let require', defsvars = process_predicates m.require defsvars in
- let ensure', defsvars = process_predicates m.ensure defsvars in
- { m with require = require'; ensure = ensure' } :: accu_m, defsvars)
- s.modes ([], defsvars)
+ (fun m (outs, accu_m, defsvars) ->
+ let outs_req, require', defsvars = process_predicates m.require defsvars in
+ let outs_ens, ensure', defsvars = process_predicates m.ensure defsvars in
+ outs_req @ outs_ens @ outs,
+ { m with require = require'; ensure = ensure' } :: accu_m,
+ defsvars)
+ s.modes (outs_asm @ outs_grt, [], defsvars)
in
let new_locals = List.filter not_is_orig_var vars in
(* removing inouts and initial locals ones *)
( new_locals,
+ outs,
defs,
{
s with
@@ -725,7 +730,7 @@ let normalize_spec parentid (in_vars, out_vars, l_vars) s =
- new equations
-
*)
-let normalize_node node =
+let normalize_node ?(first=true) node =
reset_cpt_fresh ();
let orig_vars = node.node_inputs @ node.node_outputs @ node.node_locals in
let not_is_orig_var v = List.for_all (( != ) v) orig_vars in
@@ -741,29 +746,29 @@ let normalize_node node =
let eqs, auts = get_node_eqs node in
if auts != [] then assert false;
(* Automata should be expanded by now. *)
- let spec, new_vars, eqs =
+ let node_spec, new_vars, new_outs, eqs =
(* 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
+ | None | Some (NodeSpec _) -> node.node_spec, [], [], eqs
| Some (Contract s) ->
- let new_locals, new_stmts, s' =
+ let new_locals, new_outs, new_stmts, s' =
normalize_spec node.node_id
(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
+ Some (Contract s'), new_locals, new_outs, new_stmts @ eqs
in
let defs, vars =
List.fold_left (normalize_eq norm_ctx) ([], new_vars @ orig_vars) eqs
in
(* Normalize the asserts *)
- let vars, assert_defs, asserts =
+ let vars, assert_defs, node_asserts =
List.fold_left
(fun (vars, def_accu, assert_accu) assert_ ->
let assert_expr = assert_.assert_expr in
@@ -786,7 +791,7 @@ let normalize_node node =
(* we filter out inout
vars and initial locals ones *)
- let all_locals = node.node_locals @ new_locals in
+ let node_locals = node.node_locals @ new_locals in
(* we add again, at the
beginning of the list the
@@ -802,7 +807,7 @@ let normalize_node node =
let new_annots =
if !Options.traces then
let diff_vars =
- List.filter (fun v -> not (List.mem v node.node_locals)) all_locals
+ List.filter (fun v -> not (List.mem v node.node_locals)) node_locals
in
let norm_traceability =
{
@@ -841,7 +846,7 @@ let normalize_node node =
else node.node_annot
in
- let new_annots =
+ let node_annot =
List.fold_left
(fun annots v ->
if Machine_types.is_active && Machine_types.is_exportable v then (
@@ -862,14 +867,23 @@ let normalize_node node =
new_annots new_locals
in
+ let node_inputs, node_outputs =
+ if node.node_iscontract && first then
+ node.node_inputs @ node.node_outputs, new_outs
+ else
+ node.node_inputs, node.node_outputs
+ in
+
let node =
{
node with
- node_locals = all_locals;
+ node_inputs;
+ node_outputs;
+ node_locals;
node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
- node_asserts = asserts;
- node_annot = new_annots;
- node_spec = spec;
+ node_asserts;
+ node_annot;
+ node_spec
}
in
(*Printers.pp_node Format.err_formatter node;*)
@@ -881,10 +895,10 @@ let normalize_inode nd =
| None | Some (NodeSpec _) -> nd
| Some (Contract _) -> assert false
-let normalize_decl (decl : top_decl) : top_decl =
+let normalize_decl ?first (decl : top_decl) : top_decl =
match decl.top_decl_desc with
| Node nd ->
- let decl' = { decl with top_decl_desc = Node (normalize_node nd) } in
+ let decl' = { decl with top_decl_desc = Node (normalize_node ?first nd) } in
update_node nd.node_id decl';
decl'
| ImportedNode nd ->
@@ -895,12 +909,12 @@ let normalize_decl (decl : top_decl) : top_decl =
decl'
| Include _ | Open _ | Const _ | TypeDef _ -> decl
-let normalize_prog p decls =
+let normalize_prog ?first p decls =
(* Backend specific configurations for normalization *)
params := p;
(* Main algorithm: iterates over nodes *)
- List.map normalize_decl decls
+ List.map (normalize_decl ?first) decls
(* Fake interface for outside uses *)
let mk_expr_alias_opt opt (parentid, ctx_vars) (defs, vars) expr =
diff --git a/src/normalization.mli b/src/normalization.mli
index 80503773..43a75c90 100644
--- a/src/normalization.mli
+++ b/src/normalization.mli
@@ -14,4 +14,4 @@ val mk_expr_alias_opt :
expr ->
(eq list * var_decl list) * expr
-val normalize_prog : param_t -> program_t -> program_t
+val normalize_prog : ?first:bool -> param_t -> program_t -> program_t
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index 7fe096b6..f9d32b40 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -952,7 +952,7 @@ let optimize params prog node_schs machine_code =
else
let prog = elim_prog_variables prog removed_table in
(* Mini stage1 *)
- let prog = Normalization.normalize_prog params prog in
+ let prog = Normalization.normalize_prog ~first:false params prog in
let prog = SortProg.sort_nodes_locals prog in
(* Mini stage2: note that we do not protect against alg. loop since
this should have been handled before *)
diff --git a/src/parsers/parser_lustre.mly b/src/parsers/parser_lustre.mly
index 0964ee6e..8c86a0f3 100644
--- a/src/parsers/parser_lustre.mly
+++ b/src/parsers/parser_lustre.mly
@@ -191,7 +191,8 @@ top_decl_header:
nodei_stateless;
nodei_spec;
nodei_prototype;
- nodei_in_lib
+ nodei_in_lib;
+ nodei_iscontract = false;
})
in
pop_node ();
diff --git a/src/printers.ml b/src/printers.ml
index 597c4231..15bae926 100644
--- a/src/printers.ml
+++ b/src/printers.ml
@@ -495,49 +495,47 @@ let pp_spec_stmt fmt stmt =
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. *)
- pp_print_list
- (fun fmt v ->
- 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;
+ fprintf fmt "@[<v>%a%a%a%a%a%a@]"
+ (pp_print_list
+ (fun fmt v ->
+ fprintf fmt "%a = %t;" pp_var v (fun fmt ->
+ match v.var_dec_value with
+ | None ->
+ assert false
+ | Some e ->
+ pp_expr fmt e)))
+ spec.consts
- pp_print_list (fun fmt s -> pp_spec_stmt fmt s) fmt spec.stmts;
- pp_print_list
- (fun fmt r -> fprintf fmt "assume %a;" pp_eexpr r)
- fmt
- spec.assume;
- pp_print_list
- (fun fmt r -> fprintf fmt "guarantee %a;" pp_eexpr r)
- fmt
- spec.guarantees;
- pp_print_list
- (fun fmt mode ->
- fprintf
- fmt
- "mode %s (@[<v 0>%a@ %a@]);"
- mode.mode_id
- (pp_print_list (fun fmt r -> fprintf fmt "require %a;" pp_eexpr r))
- mode.require
- (pp_print_list (fun fmt r -> fprintf fmt "ensure %a;" pp_eexpr r))
- mode.ensure)
- fmt
- spec.modes;
- pp_print_list
- (fun fmt import ->
- fprintf
- fmt
- "import %s (%a) returns (%a);"
- import.import_nodeid
- pp_expr
- import.inputs
- pp_expr
- import.outputs)
- fmt
+ (pp_print_list ~pp_prologue:pp_print_cut pp_spec_stmt) spec.stmts
+
+ (pp_print_list ~pp_prologue:pp_print_cut (fun fmt -> fprintf fmt "assume %a;" pp_eexpr))
+ spec.assume
+
+ (pp_print_list ~pp_prologue:pp_print_cut (fun fmt -> fprintf fmt "guarantee %a;" pp_eexpr))
+ spec.guarantees
+
+ (pp_print_list ~pp_prologue:pp_print_cut
+ (fun fmt mode ->
+ fprintf
+ fmt
+ "mode %s (@[<v 0>%a@ %a@]);"
+ mode.mode_id
+ (pp_print_list (fun fmt r -> fprintf fmt "require %a;" pp_eexpr r))
+ mode.require
+ (pp_print_list (fun fmt r -> fprintf fmt "ensure %a;" pp_eexpr r))
+ mode.ensure))
+ spec.modes
+
+ (pp_print_list ~pp_prologue:pp_print_cut
+ (fun fmt import ->
+ fprintf
+ fmt
+ "import %s (%a) returns (%a);"
+ import.import_nodeid
+ pp_expr
+ import.inputs
+ pp_expr
+ import.outputs))
spec.imports
(* Project the contract node as a pure contract: local memories are pushed back
@@ -754,18 +752,18 @@ let pp_prog pp_decl fmt prog =
let pp_short_decl fmt decl =
match decl.top_decl_desc with
| Node nd ->
- fprintf fmt "%a %s@ " pp_node_vs_function nd nd.node_id
+ fprintf fmt "%a %s" pp_node_vs_function nd nd.node_id
| ImportedNode ind ->
fprintf fmt "imported node %s" ind.nodei_id
| Const c ->
- fprintf fmt "const %a@ " pp_const_decl c
+ fprintf fmt "const %a" pp_const_decl c
| Include s ->
fprintf fmt "include \"%s\"" s
| Open (local, s) ->
- if local then fprintf fmt "#open \"%s\"@ " s
- else fprintf fmt "#open <%s>@ " s
+ if local then fprintf fmt "#open \"%s\"" s
+ else fprintf fmt "#open <%s>" s
| TypeDef tdef ->
- fprintf fmt "type %s;@ " tdef.tydef_id
+ fprintf fmt "type %s" tdef.tydef_id
let pp_prog_short = pp_prog pp_short_decl
diff --git a/src/sortProg.ml b/src/sortProg.ml
index 2a386c6a..9c41dca1 100644
--- a/src/sortProg.ml
+++ b/src/sortProg.ml
@@ -53,7 +53,7 @@ let sort prog =
Format.fprintf
fmt
"@ @[<v 2>.. ordered list of declarations:@ %a@]@ "
- (Format.pp_print_list Printers.pp_short_decl)
+ Format.(pp_print_list ~pp_open_box:pp_open_vbox0 Printers.pp_short_decl)
sorted);
not_nodes @ sorted
diff --git a/src/spec_types.ml b/src/spec_types.ml
index e39974cf..8eb61540 100644
--- a/src/spec_types.ml
+++ b/src/spec_types.ml
@@ -56,6 +56,7 @@ type 'a formula_t =
| Predicate : 'a predicate_t -> 'a formula_t
| StateVarPack of register_t
| ExistsMem of ident * 'a formula_t * 'a formula_t
+ | Value of 'a
(* type 'a simulation_t = {
* sname: node_desc;
diff --git a/src/spec_types.mli b/src/spec_types.mli
index c557a720..5edb4568 100644
--- a/src/spec_types.mli
+++ b/src/spec_types.mli
@@ -49,6 +49,7 @@ type 'a formula_t =
| Predicate : 'a predicate_t -> 'a formula_t
| StateVarPack of register_t
| ExistsMem of ident * 'a formula_t * 'a formula_t
+ | Value of 'a
type 'a transition_t = {
tname : node_desc;
diff --git a/src/types.ml b/src/types.ml
index de500870..6cfb6b19 100644
--- a/src/types.ml
+++ b/src/types.ml
@@ -589,8 +589,9 @@ module Make (BasicT : BASIC_TYPES) = struct
assert false
(** Returns the type corresponding to a type list. *)
- let type_of_type_list tyl =
- if List.length tyl > 1 then new_ty (Ttuple tyl) else List.hd tyl
+ let type_of_type_list = function
+ | [t] -> t
+ | tyl -> new_ty (Ttuple tyl)
let rec type_list_of_type ty =
match (repr ty).tdesc with
diff --git a/src/typing.ml b/src/typing.ml
index 74003319..ba7c0877 100644
--- a/src/typing.ml
+++ b/src/typing.ml
@@ -1047,8 +1047,9 @@ struct
* assert false *)
let type_prog env decls =
- try List.fold_left type_top_decl env decls
- with Failure _ as exc -> raise exc
+ (* try *)
+ List.fold_left type_top_decl env decls
+ (* with Failure _ as exc -> raise exc *)
(* Once the Lustre program is fully typed, we must get back to the original
description of dimensions, with constant parameters, instead of unifiable
--
GitLab