From 6d1693b9a18db56292dc417972f18bb70f1a644f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lelio.brun@isae-supaero.fr>
Date: Mon, 14 Jun 2021 19:06:13 +0200
Subject: [PATCH] work on spec generation almost done
---
include/arrow.c | 8 +
include/arrow.h | 11 +-
include/arrow_spec.c | 25 +
include/arrow_spec.h | 71 +-
src/arrow.ml | 3 +
src/arrow.mli | 1 +
src/backends/Ada/ada_backend_adb.ml | 6 +-
src/backends/Ada/misc_lustre_function.ml | 2 +-
src/backends/C/c_backend_common.ml | 129 ++-
src/backends/C/c_backend_header.ml | 17 +-
src/backends/C/c_backend_main.ml | 2 +-
src/backends/C/c_backend_spec.ml | 1096 +++++++++-----------
src/backends/C/c_backend_src.ml | 170 +--
src/backends/EMF/EMF_backend.ml | 18 +-
src/backends/Horn/horn_backend_printers.ml | 4 +-
src/corelang.ml | 7 +-
src/corelang.mli | 7 +-
src/dune | 1 +
src/lustre_live.ml | 104 ++
src/machine_code.ml | 333 +++---
src/machine_code_common.ml | 290 ++++--
src/machine_code_common.mli | 8 +-
src/machine_code_types.ml | 9 +-
src/optimize_machine.ml | 27 +-
src/plugins/scopes/scopes.ml | 4 +-
src/spec_common.ml | 121 +--
src/spec_types.ml | 59 +-
src/utils/utils.ml | 10 +
28 files changed, 1502 insertions(+), 1041 deletions(-)
create mode 100644 include/arrow_spec.c
create mode 100644 src/lustre_live.ml
diff --git a/include/arrow.c b/include/arrow.c
index 93ae5979..7cfb2e86 100644
--- a/include/arrow.c
+++ b/include/arrow.c
@@ -12,3 +12,11 @@ struct _arrow_mem * _arrow_alloc () {
void _arrow_dealloc (struct _arrow_mem * _alloc) {
free (_alloc);
}
+
+_Bool _arrow_step(struct _arrow_mem *self) {
+ if (self->_reg._first) {
+ self->_reg._first = 0;
+ return 1;
+ }
+ return 0;
+}
diff --git a/include/arrow.h b/include/arrow.h
index d2956d8b..e0799784 100644
--- a/include/arrow.h
+++ b/include/arrow.h
@@ -1,8 +1,9 @@
-
#ifndef _ARROW
#define _ARROW
-struct _arrow_mem {struct _arrow_reg {_Bool _first; } _reg; };
+struct _arrow_mem {
+ struct _arrow_reg {_Bool _first; } _reg;
+};
extern struct _arrow_mem *_arrow_alloc ();
@@ -23,12 +24,8 @@ extern void _arrow_dealloc (struct _arrow_mem *);
#define _arrow_clear(self) {}
-/* #define _arrow_step(x,y,output,self) ((self)->_reg._first?((self)->_reg._first=0,(*output = x)):(*output = y)) */
-
#define _arrow_reset(self) {(self)->_reg._first = 1;}
-/* Step macro for specialized arrows of the form: (true -> false) */
-
-#define _once_step(output,self) { *output = (self)->_reg._first; if ((self)->_reg._first) { (self)->_reg._first=0; }; }
+_Bool _arrow_step(struct _arrow_mem *self);
#endif
diff --git a/include/arrow_spec.c b/include/arrow_spec.c
new file mode 100644
index 00000000..d47e314f
--- /dev/null
+++ b/include/arrow_spec.c
@@ -0,0 +1,25 @@
+#include <stdlib.h>
+#include <assert.h>
+#include "arrow_spec.h"
+
+struct _arrow_mem * _arrow_alloc () {
+ struct _arrow_mem *_alloc;
+ _alloc = (struct _arrow_mem *) malloc(sizeof(struct _arrow_mem *));
+ assert (_alloc);
+ return _alloc;
+}
+
+void _arrow_dealloc (struct _arrow_mem * _alloc) {
+ free (_alloc);
+}
+
+_Bool _arrow_step(struct _arrow_mem *self)
+ /*@ ghost (struct _arrow_mem_ghost \ghost *mem) */
+{
+ if (self->_reg._first) {
+ self->_reg._first = 0;
+ //@ ghost _arrow_step_ghost(*mem);
+ return 1;
+ }
+ return 0;
+}
diff --git a/include/arrow_spec.h b/include/arrow_spec.h
index 7ac02a4b..b1e1b544 100644
--- a/include/arrow_spec.h
+++ b/include/arrow_spec.h
@@ -1,29 +1,64 @@
#ifndef ARROW_SPEC_H_
#define ARROW_SPEC_H_
+struct _arrow_mem {
+ struct _arrow_reg {_Bool _first; } _reg;
+};
+
+extern struct _arrow_mem *_arrow_alloc ();
+
+extern void _arrow_dealloc (struct _arrow_mem *);
+
+#define _arrow_DECLARE(attr, inst)\
+ attr struct _arrow_mem inst;
+
+#define _arrow_LINK(inst) do {\
+ ;\
+} while (0)
+
+#define _arrow_ALLOC(attr, inst)\
+ _arrow_DECLARE(attr, inst);\
+ _arrow_LINK(inst)
+
+#define _arrow_init(self) {}
+
+#define _arrow_clear(self) {}
+
+#define _arrow_reset(self) {(self)->_reg._first = 1;}
+
/* ACSL arrow spec */
//@ ghost struct _arrow_mem_ghost {struct _arrow_reg _reg;};
-/*@
- predicate _arrow_valid(struct _arrow_mem *self) =
- \valid(self);
-*/
-/*@
- predicate _arrow_initialization(struct _arrow_mem_ghost mem_in) =
- mem_in._reg._first == 1;
+
+#define _arrow_reset_ghost(mem) (mem)._reg._first = 1
+#define _arrow_step_ghost(mem) (mem)._reg._first = 0
+
+/*@ predicate _arrow_initialization(struct _arrow_mem_ghost mem_in) =
+ mem_in._reg._first == 1;
+ */
+
+/*@ predicate _arrow_transition(struct _arrow_mem_ghost mem_in,
+ struct _arrow_mem_ghost mem_out,
+ _Bool out) =
+ out == mem_in._reg._first
+ && (mem_in._reg._first ? (mem_out._reg._first == 0)
+ : (mem_out._reg._first == mem_in._reg._first));
*/
-/*@
- predicate _arrow_transition(struct _arrow_mem_ghost mem_in,
- integer x, integer y,
- struct _arrow_mem_ghost mem_out, _Bool out) =
- (mem_in._reg._first ? (mem_out._reg._first == 0
- && out == x)
- : (mem_out._reg._first == mem_in._reg._first
- && out == y));
+
+/*@ predicate _arrow_ghost(struct _arrow_mem_ghost mem,
+ struct _arrow_mem *self) =
+ mem._reg._first == self->_reg._first;
*/
+
/*@
- predicate _arrow_ghost(struct _arrow_mem_ghost mem,
- struct _arrow_mem *self) =
- mem._reg._first == self->_reg._first;
+ requires \separated(mem, self);
+ requires _arrow_ghost(*mem, self);
+ ensures _arrow_ghost(*mem, self);
+ ensures \result == \old(self->_reg._first);
+ ensures self->_reg._first == 0;
+ ensures !\old(mem->_reg._first) ==> *mem == \old(*mem);
+ assigns mem->_reg._first, self->_reg._first;
*/
+_Bool _arrow_step(struct _arrow_mem *self)
+ /*@ ghost (struct _arrow_mem_ghost \ghost *mem) */;
#endif // ARROW_SPEC_H_
diff --git a/src/arrow.ml b/src/arrow.ml
index 610b4792..23a71b1f 100644
--- a/src/arrow.ml
+++ b/src/arrow.ml
@@ -30,3 +30,6 @@ let arrow_top_decl () =
top_decl_itf = false;
top_decl_loc = Location.dummy_loc
}
+
+let td_is_arrow td =
+ Corelang.node_name td = arrow_id
diff --git a/src/arrow.mli b/src/arrow.mli
index ace9a285..31916c58 100644
--- a/src/arrow.mli
+++ b/src/arrow.mli
@@ -1,3 +1,4 @@
val arrow_id: string
val arrow_top_decl: unit -> Lustre_types.top_decl
val arrow_desc: Lustre_types.node_desc
+val td_is_arrow: Lustre_types.top_decl -> bool
diff --git a/src/backends/Ada/ada_backend_adb.ml b/src/backends/Ada/ada_backend_adb.ml
index 9ab15e30..18a0c7dd 100644
--- a/src/backends/Ada/ada_backend_adb.ml
+++ b/src/backends/Ada/ada_backend_adb.ml
@@ -85,8 +85,10 @@ struct
match get_instr_desc instr with
(* no reset *)
| MNoReset _ -> ()
+ (* TODO: handle clear_reset *)
+ | MClearReset -> ()
(* reset *)
- | MReset i when List.mem_assoc i typed_submachines ->
+ | MSetReset i when List.mem_assoc i typed_submachines ->
let (substitution, submachine) = get_instance i typed_submachines in
let pp_package = pp_package_name_with_polymorphic substitution submachine in
let args = if is_machine_statefull submachine then [[pp_state i]] else [] in
@@ -149,7 +151,7 @@ struct
**)
let pp_reset_definition env typed_submachines fmt (m, m_spec_opt) =
let build_assign = function var ->
- mkinstr Spec_types.True (MStateAssign (var, mk_default_value var.var_type))
+ mkinstr (MStateAssign (var, mk_default_value var.var_type))
in
let env, memory = match m_spec_opt with
| None -> env, m.mmemory
diff --git a/src/backends/Ada/misc_lustre_function.ml b/src/backends/Ada/misc_lustre_function.ml
index 35fb018c..45ebcd91 100644
--- a/src/backends/Ada/misc_lustre_function.ml
+++ b/src/backends/Ada/misc_lustre_function.ml
@@ -268,7 +268,7 @@ let rec push_if_in_expr = function
let assign = if state then MStateAssign (ident, value) else MLocalAssign (ident, value) in
{ instr_desc = assign;
lustre_eq = None;
- instr_spec = Spec_types.True
+ instr_spec = []
}
in
let mkval_var id = {
diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml
index 030e8bd9..bcffd9e9 100644
--- a/src/backends/C/c_backend_common.ml
+++ b/src/backends/C/c_backend_common.ml
@@ -37,6 +37,14 @@ let file_to_module_name basename =
let baseNAME = protect_filename baseNAME in
baseNAME
+let pp_ptr fmt =
+ fprintf fmt "*%s"
+
+let reset_label = "Reset"
+
+let pp_label fmt =
+ fprintf fmt "%s:"
+
let var_is name v =
v.var_id = name
@@ -55,6 +63,7 @@ let mk_self = mk_local "self"
let mk_mem = mk_local "mem"
let mk_mem_in = mk_local "mem_in"
let mk_mem_out = mk_local "mem_out"
+let mk_mem_reset = mk_local "mem_reset"
(* Generation of a non-clashing name for the instance variable of static allocation macro *)
let mk_instance m =
@@ -118,13 +127,18 @@ let pp_global_init_name fmt id = fprintf fmt "%s_INIT" id
let pp_global_clear_name fmt id = fprintf fmt "%s_CLEAR" id
let pp_machine_memtype_name ?(ghost=false) fmt id =
fprintf fmt "struct %s_mem%s" id (if ghost then "_ghost" else "")
+let pp_machine_decl ?(ghost=false) pp_var fmt (id, var) =
+ fprintf fmt "%a %a" (pp_machine_memtype_name ~ghost) id pp_var var
+let pp_machine_decl' ?(ghost=false) fmt =
+ pp_machine_decl ~ghost pp_print_string fmt
let pp_machine_regtype_name fmt id = fprintf fmt "struct %s_reg" id
let pp_machine_alloc_name fmt id = fprintf fmt "%s_alloc" id
let pp_machine_dealloc_name fmt id = fprintf fmt "%s_dealloc" id
let pp_machine_static_declare_name fmt id = fprintf fmt "%s_DECLARE" id
let pp_machine_static_link_name fmt id = fprintf fmt "%s_LINK" id
let pp_machine_static_alloc_name fmt id = fprintf fmt "%s_ALLOC" id
-let pp_machine_reset_name fmt id = fprintf fmt "%s_reset" id
+let pp_machine_set_reset_name fmt id = fprintf fmt "%s_set_reset" id
+let pp_machine_clear_reset_name fmt id = fprintf fmt "%s_clear_reset" id
let pp_machine_init_name fmt id = fprintf fmt "%s_init" id
let pp_machine_clear_name fmt id = fprintf fmt "%s_clear" id
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
@@ -583,6 +597,9 @@ let rec pp_value_suffix ?(indirect=true) m self var_type loop_vars pp_var fmt va
then fprintf fmt "%a%a" pp_var v pp_suffix loop_vars
else fprintf fmt "%s%s_reg.%a%a"
self (if indirect then "->" else ".") pp_var v pp_suffix loop_vars
+ else if is_reset_flag v then
+ fprintf fmt "%s%s%a%a"
+ self (if indirect then "->" else ".") pp_var v pp_suffix loop_vars
else
fprintf fmt "%a%a" pp_var v pp_suffix loop_vars
| _, Cst cst ->
@@ -610,7 +627,7 @@ let rec pp_value_suffix ?(indirect=true) m self var_type loop_vars pp_var fmt va
let print_machine_struct ?(ghost=false) fmt m =
if not (fst (Machine_code_common.get_stateless_status m)) then
(* Define struct *)
- fprintf fmt "@[<v 2>%a {%a%a@]@,};"
+ fprintf fmt "@[<v 2>%a {@,_Bool _reset;%a%a@]@,};"
(pp_machine_memtype_name ~ghost) m.mname.node_id
(if ghost then
(fun fmt -> function
@@ -658,46 +675,74 @@ let print_dealloc_prototype fmt name =
pp_machine_dealloc_name name
(pp_machine_memtype_name ~ghost:false) name
-let print_reset_prototype self fmt (name, static) =
- fprintf fmt "void %a (%a%a *%s)"
- pp_machine_reset_name name
- (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
- pp_c_decl_input_var) static
- (pp_machine_memtype_name ~ghost:false) name
- self
-
-let print_init_prototype self fmt (name, static) =
- fprintf fmt "void %a (%a%a *%s)"
- pp_machine_init_name name
- (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
- pp_c_decl_input_var) static
- (pp_machine_memtype_name ~ghost:false) name
- self
-
-let print_clear_prototype self fmt (name, static) =
- fprintf fmt "void %a (%a%a *%s)"
- pp_machine_clear_name name
- (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
- pp_c_decl_input_var) static
- (pp_machine_memtype_name ~ghost:false) name
- self
-
-let print_stateless_prototype fmt (name, inputs, outputs) =
- fprintf fmt "void %a (@[<v>%a%a@])"
- pp_machine_step_name name
- (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
- ~pp_epilogue:pp_print_cut pp_c_decl_input_var) inputs
- (pp_print_list ~pp_sep:pp_print_comma pp_c_decl_output_var) outputs
-
-let print_step_prototype self fmt (name, inputs, outputs) =
- fprintf fmt "void %a (@[<v>%a%a%a *%s@])"
- pp_machine_step_name name
- (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
- ~pp_epilogue:pp_print_cut pp_c_decl_input_var) inputs
- (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
- ~pp_epilogue:pp_print_cut pp_c_decl_output_var) outputs
- (pp_machine_memtype_name ~ghost:false) name
- self
+module type MODIFIERS_GHOST_PROTO = sig
+ val pp_ghost_parameters: formatter -> (string * (formatter -> string -> unit)) list -> unit
+end
+
+module EmptyGhostProto: MODIFIERS_GHOST_PROTO = struct
+ let pp_ghost_parameters _ _ = ()
+end
+
+module Protos (Mod: MODIFIERS_GHOST_PROTO) = struct
+
+ let pp_mem_ghost name fmt mem =
+ pp_machine_decl ~ghost:true
+ (fun fmt mem -> fprintf fmt "\ghost %a" pp_ptr mem) fmt
+ (name, mem)
+
+ let print_clear_reset_prototype self mem fmt (name, static) =
+ fprintf fmt "@[<v>void %a (%a%a *%s)%a@]"
+ pp_machine_clear_reset_name name
+ (pp_comma_list ~pp_eol:pp_print_comma
+ pp_c_decl_input_var) static
+ (pp_machine_memtype_name ~ghost:false) name
+ self
+ Mod.pp_ghost_parameters [mem, pp_mem_ghost name]
+
+ let print_set_reset_prototype self mem fmt (name, static) =
+ fprintf fmt "@[<v>void %a (%a%a *%s)%a@]"
+ pp_machine_set_reset_name name
+ (pp_comma_list ~pp_eol:pp_print_comma
+ pp_c_decl_input_var) static
+ (pp_machine_memtype_name ~ghost:false) name
+ self
+ Mod.pp_ghost_parameters [mem, pp_mem_ghost name]
+
+ let print_step_prototype self mem fmt (name, inputs, outputs) =
+ fprintf fmt "@[<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) inputs
+ (pp_comma_list ~pp_eol:pp_print_comma
+ ~pp_epilogue:pp_print_cut pp_c_decl_output_var) outputs
+ (pp_machine_memtype_name ~ghost:false) name
+ self
+ Mod.pp_ghost_parameters [mem, pp_mem_ghost name]
+
+ let print_init_prototype self fmt (name, static) =
+ fprintf fmt "void %a (%a%a *%s)"
+ pp_machine_init_name name
+ (pp_comma_list ~pp_eol:pp_print_comma
+ pp_c_decl_input_var) static
+ (pp_machine_memtype_name ~ghost:false) name
+ self
+
+ let print_clear_prototype self fmt (name, static) =
+ fprintf fmt "void %a (%a%a *%s)"
+ pp_machine_clear_name name
+ (pp_comma_list ~pp_eol:pp_print_comma
+ pp_c_decl_input_var) static
+ (pp_machine_memtype_name ~ghost:false) name
+ self
+
+ let print_stateless_prototype fmt (name, inputs, outputs) =
+ fprintf fmt "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) inputs
+ (pp_comma_list pp_c_decl_output_var) outputs
+
+end
let print_import_prototype fmt dep =
fprintf fmt "#include \"%s.h\"" dep.name
diff --git a/src/backends/C/c_backend_header.ml b/src/backends/C/c_backend_header.ml
index 3e667072..74b3ff08 100644
--- a/src/backends/C/c_backend_header.ml
+++ b/src/backends/C/c_backend_header.ml
@@ -22,17 +22,21 @@ open C_backend_common
module type MODIFIERS_HDR = sig
+ module GhostProto: MODIFIERS_GHOST_PROTO
val print_machine_decl_prefix: Format.formatter -> machine_t -> unit
val pp_import_standard_spec: formatter -> unit -> unit
end
module EmptyMod = struct
+ module GhostProto = EmptyGhostProto
let print_machine_decl_prefix = fun _ _ -> ()
let pp_import_standard_spec _ _ = ()
end
module Main = functor (Mod: MODIFIERS_HDR) -> struct
+ module Protos = Protos(Mod.GhostProto)
+
let print_import_standard fmt () =
(* if Machine_types.has_machine_type () then *)
fprintf fmt
@@ -231,7 +235,7 @@ module Main = functor (Mod: MODIFIERS_HDR) -> struct
assert false
end
else if inode.nodei_stateless then
- fprintf fmt "extern %a;" print_stateless_prototype prototype
+ fprintf fmt "extern %a;" Protos.print_stateless_prototype prototype
else
let static_inputs = List.filter (fun v -> v.var_dec_const)
inode.nodei_inputs in
@@ -239,16 +243,19 @@ module Main = functor (Mod: MODIFIERS_HDR) -> struct
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;"
- (print_reset_prototype self) static_prototype
- (print_init_prototype self) static_prototype
- (print_clear_prototype self) static_prototype
- (print_step_prototype self) prototype
+ (Protos.print_set_reset_prototype self mem) static_prototype
+ (Protos.print_clear_reset_prototype self mem) static_prototype
+ (Protos.print_init_prototype self) static_prototype
+ (Protos.print_clear_prototype self) static_prototype
+ (Protos.print_step_prototype self mem) prototype
let print_const_top_decl fmt tdecl =
let cdecl = const_of_top tdecl in
diff --git a/src/backends/C/c_backend_main.ml b/src/backends/C/c_backend_main.ml
index 187abec6..b66d794c 100644
--- a/src/backends/C/c_backend_main.ml
+++ b/src/backends/C/c_backend_main.ml
@@ -87,7 +87,7 @@ module Main = functor (Mod: MODIFIERS_MAINSRC) -> struct
fprintf fmt "%a *main_mem = %a();"
(pp_machine_memtype_name ~ghost:false) mname
pp_machine_alloc_name mname) ()
- pp_machine_reset_name mname
+ pp_machine_set_reset_name mname
main_mem
let print_global_initialize fmt basename =
diff --git a/src/backends/C/c_backend_spec.ml b/src/backends/C/c_backend_spec.ml
index 10562936..c87b1f74 100644
--- a/src/backends/C/c_backend_spec.ml
+++ b/src/backends/C/c_backend_spec.ml
@@ -1,3 +1,4 @@
+
(********************************************************************)
(* *)
(* The LustreC compiler toolset / The LustreC Development Team *)
@@ -13,132 +14,20 @@ open Utils.Format
open Lustre_types
open Machine_code_types
open C_backend_common
-open Machine_code_common
open Corelang
+open Spec_types
+open Spec_common
+open Machine_code_common
(**************************************************************************)
(* Printing spec for c *)
(**************************************************************************)
-(* OLD STUFF ???
-
-
-let pp_acsl_type var fmt t =
- let rec aux t pp_suffix =
- match (Types.repr t).Types.tdesc with
- | Types.Tclock t' -> aux t' pp_suffix
- | Types.Tbool -> fprintf fmt "int %s%a" var pp_suffix ()
- | Types.Treal -> fprintf fmt "real %s%a" var pp_suffix ()
- | Types.Tint -> fprintf fmt "int %s%a" var pp_suffix ()
- | Types.Tarray (d, t') ->
- let pp_suffix' fmt () = fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in
- aux t' pp_suffix'
- (* | Types.Tstatic (_, t') -> fprintf fmt "const "; aux t' pp_suffix *)
- (* | Types.Tconst ty -> fprintf fmt "%s %s" ty var *)
- (* | Types.Tarrow (_, _) -> fprintf fmt "void (\*%s)()" var *)
- | _ -> eprintf "internal error: pp_acsl_type %a@." Types.print_ty t; assert false
- in aux t (fun fmt () -> ())
-
-let pp_acsl_var_decl fmt id =
- pp_acsl_type id.var_id fmt id.var_type
-
-
-let rec pp_eexpr is_output fmt eexpr =
- let pp_eexpr = pp_eexpr is_output in
- match eexpr.eexpr_desc with
- | EExpr_const c -> Printers.pp_econst fmt c
- | EExpr_ident id ->
- if is_output id then pp_print_string fmt ("*" ^ id) else pp_print_string fmt id
- | EExpr_tuple el -> Utils.fprintf_list ~sep:"," pp_eexpr fmt el
- | EExpr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_eexpr e1 pp_eexpr e2
- | EExpr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_eexpr e1 pp_eexpr e2
- (* | EExpr_concat (e1, e2) -> fprintf fmt "%a::%a" pp_eexpr e1 pp_eexpr e2 *)
- (* | EExpr_tail e -> fprintf fmt "tail %a" pp_eexpr e *)
- | EExpr_pre e -> fprintf fmt "pre %a" pp_eexpr e
- | EExpr_when (e, id) -> fprintf fmt "%a when %s" pp_eexpr e id
- | EExpr_merge (id, e1, e2) ->
- fprintf fmt "merge (%s, %a, %a)" id pp_eexpr e1 pp_eexpr e2
- | EExpr_appl (id, e, r) -> pp_eapp is_output fmt id e r
- | EExpr_forall (vars, e) -> fprintf fmt "forall %a; %a" Printers.pp_node_args vars pp_eexpr e
- | EExpr_exists (vars, e) -> fprintf fmt "exists %a; %a" Printers.pp_node_args vars pp_eexpr e
-
-
- (* | EExpr_whennot _ *)
- (* | EExpr_uclock _ *)
- (* | EExpr_dclock _ *)
- (* | EExpr_phclock _ -> assert false *)
-and pp_eapp is_output fmt id e r =
- let pp_eexpr = pp_eexpr is_output in
- match r with
- | None ->
- (match id, e.eexpr_desc with
- | "+", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_eexpr e1 pp_eexpr e2
- | "uminus", _ -> fprintf fmt "(- %a)" pp_eexpr e
- | "-", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_eexpr e1 pp_eexpr e2
- | "*", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_eexpr e1 pp_eexpr e2
- | "/", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_eexpr e1 pp_eexpr e2
- | "mod", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_eexpr e1 pp_eexpr e2
- | "&&", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a && %a)" pp_eexpr e1 pp_eexpr e2
- | "||", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a || %a)" pp_eexpr e1 pp_eexpr e2
- | "xor", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ^^ %a)" pp_eexpr e1 pp_eexpr e2
- | "impl", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ==> %a)" pp_eexpr e1 pp_eexpr e2
- | "<", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_eexpr e1 pp_eexpr e2
- | "<=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_eexpr e1 pp_eexpr e2
- | ">", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_eexpr e1 pp_eexpr e2
- | ">=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_eexpr e1 pp_eexpr e2
- | "!=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_eexpr e1 pp_eexpr e2
- | "=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_eexpr e1 pp_eexpr e2
- | "not", _ -> fprintf fmt "(! %a)" pp_eexpr e
- | "ite", EExpr_tuple([e1;e2;e3]) -> fprintf fmt "(if %a then %a else %a)" pp_eexpr e1 pp_eexpr e2 pp_eexpr e3
- | _ -> fprintf fmt "%s (%a)" id pp_eexpr e)
- | Some x -> fprintf fmt "%s (%a) every %s" id pp_eexpr e x
-
-let pp_ensures is_output fmt e =
- match e with
- | EnsuresExpr e -> fprintf fmt "ensures %a;@ " (pp_eexpr is_output) e
- | SpecObserverNode (name, args) -> fprintf fmt "observer %s (%a);@ " name (Utils.fprintf_list ~sep:", " (pp_eexpr is_output)) args
-
-let pp_acsl_spec outputs fmt spec =
- let is_output = fun oid -> List.exists (fun v -> v.var_id = oid) outputs in
- let pp_eexpr = pp_eexpr is_output in
- fprintf fmt "@[<v 2>/*@@ ";
- Utils.fprintf_list ~sep:"" (fun fmt r -> fprintf fmt "requires %a;@ " pp_eexpr r) fmt spec.requires;
- Utils.fprintf_list ~sep:"" (pp_ensures is_output) fmt spec.ensures;
- fprintf fmt "@ ";
- (* fprintf fmt "assigns *self%t%a;@ " *)
- (* (fun fmt -> if List.length outputs > 0 then fprintf fmt ", ") *)
- (* (fprintf_list ~sep:"," (fun fmt v -> fprintf fmt "*%s" v.var_id)) outputs; *)
- Utils.fprintf_list ~sep:"@ " (fun fmt (name, assumes, requires) ->
- fprintf fmt "behavior %s:@[@ %a@ %a@]"
- name
- (Utils.fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes
- (Utils.fprintf_list ~sep:"@ " (pp_ensures is_output)) requires
- ) fmt spec.behaviors;
- fprintf fmt "@]@ */@.";
- ()
-
-
-
-
-let print_machine_decl_prefix fmt m =
- (* Print specification if any *)
- (match m.mspec with
- | None -> ()
- | Some spec ->
- pp_acsl_spec m.mstep.step_outputs fmt spec
- )
-
- *)
-
- (* TODO ACSL
+
+(* TODO ACSL
Return updates machines (eg with local annotations) and acsl preamble *)
let preprocess_acsl machines = machines, []
-(* TODO: This preamble shall be a list of types, axiomatics, predicates, theorems *)
-(* let pp_acsl_preamble fmt _preamble =
- * fprintf fmt "";
- * () *)
-
let pp_acsl_basic_type_desc t_desc =
if Types.is_bool_type t_desc then
(* if !Options.cpp then "bool" else "_Bool" *)
@@ -151,22 +40,14 @@ let pp_acsl_basic_type_desc t_desc =
else
assert false (* Not a basic C type. Do not handle arrays or pointers *)
-module VarDecl = struct
- type t = var_decl
- let compare v1 v2 = compare v1.var_id v2.var_id
-end
-module VDSet = Set.Make(VarDecl)
-
-module Live = Map.Make(Int)
-
-let pp_spec pp fmt =
- fprintf fmt "@[<v>/*%@@[<v>@,%a@]@,*/@]" pp
+let pp_acsl pp fmt =
+ fprintf fmt "@[<v>/*%@ @[<v>%a@]@,*/@]" pp
-let pp_spec_cut pp fmt =
- fprintf fmt "%a@," (pp_spec pp)
+let pp_acsl_cut pp fmt =
+ fprintf fmt "%a@," (pp_acsl pp)
-let pp_spec_line pp fmt =
- fprintf fmt "//%@ %a@," pp
+let pp_acsl_line pp fmt =
+ fprintf fmt "//%@ @[<h>%a@]" pp
let pp_requires pp_req fmt =
fprintf fmt "requires %a;" pp_req
@@ -174,11 +55,13 @@ let pp_requires pp_req fmt =
let pp_ensures pp_ens fmt =
fprintf fmt "ensures %a;" pp_ens
+let pp_assumes pp_asm fmt =
+ fprintf fmt "assumes %a;" pp_asm
+
let pp_assigns pp =
- pp_print_list
+ pp_comma_list
~pp_prologue:(fun fmt () -> pp_print_string fmt "assigns ")
~pp_epilogue:pp_print_semicolon'
- ~pp_sep:pp_print_comma
pp
let pp_ghost pp_gho fmt =
@@ -214,73 +97,46 @@ let pp_reg self fmt field =
let pp_true fmt () =
pp_print_string fmt "\\true"
-(* let memories machines m =
- * let open List in
- * let grow paths i =
- * match paths with
- * | [] -> [[i]]
- * | _ -> map (cons i) paths
- * in
- * let rec aux paths m =
- * map (fun (i, (td, _)) ->
- * let paths = grow paths i in
- * try
- * let m = find (fun m -> m.mname.node_id = node_name td) machines in
- * aux paths m
- * with Not_found -> paths)
- * m.minstances |> flatten
- * in
- * aux [] m |> map rev *)
+let pp_false fmt () =
+ pp_print_string fmt "\\false"
+
+let pp_at pp_v fmt (v, l) =
+ fprintf fmt "\\at(%a, %s)" pp_v v l
let instances machines m =
let open List in
- let grow paths i mems =
+ let grow paths i td mems =
match paths with
- | [] -> [[i, mems]]
- | _ -> map (cons (i, mems)) paths
+ | [] -> [[i, (td, mems)]]
+ | _ -> map (cons (i, (td, mems))) paths
in
let rec aux paths m =
map (fun (i, (td, _)) ->
try
let m = find (fun m -> m.mname.node_id = node_name td) machines in
- aux (grow paths i m.mmemory) m
- with Not_found -> grow paths i [])
+ aux (grow paths i td m.mmemory) m
+ with Not_found -> grow paths i td [])
m.minstances |> flatten
in
aux [] m |> map rev
let memories insts =
List.(map (fun path ->
- let mems = snd (hd (rev path)) in
+ let _, (_, mems) = hd (rev path) in
map (fun mem -> path, mem) mems) insts |> flatten)
-let pp_instance =
+let pp_instance ?(indirect=true) ptr =
pp_print_list
- ~pp_prologue:(fun fmt () -> pp_print_string fmt "self->")
- ~pp_sep:(fun fmt () -> pp_print_string fmt "->")
+ ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
+ ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
(fun fmt (i, _) -> pp_print_string fmt i)
-let pp_memory fmt (path, mem) =
- pp_access (pp_indirect pp_instance pp_print_string) pp_var_decl
+let pp_memory ?(indirect=true) ptr fmt (path, mem) =
+ pp_access
+ ((if indirect then pp_indirect else pp_access)
+ (pp_instance ~indirect ptr) pp_print_string)
+ pp_var_decl
fmt ((path, "_reg"), mem)
- (* let mems = snd List.(hd (rev path)) in
- * pp_print_list
- * ~pp_sep:pp_print_comma
- * (fun fmt mem -> pp_access pp_instance pp_var_decl fmt (path, mem))
- * fmt
- * mems *)
- (* let mems = ref [] in
- * let pp fmt =
- * pp_print_list
- * ~pp_prologue:(fun fmt () -> pp_print_string fmt "self->")
- * ~pp_sep:(fun fmt () -> pp_print_string fmt "->")
- * (fun fmt (i, regs) -> mems := regs; pp_print_string fmt i)
- * fmt
- * in
- * pp_print_list
- * ~pp_sep:pp_print_comma
- * (fun fmt mem -> pp_access pp pp_var_decl fmt (insts, mem))
- * fmt !mems *)
let prefixes l =
let rec pref acc = function
@@ -292,27 +148,28 @@ let prefixes l =
let powerset_instances paths =
List.map prefixes paths |> List.flatten
-let pp_separated self fmt (paths, ptrs) =
- fprintf fmt "\\separated(@[<h>%s%a%a@])"
+let pp_separated self mem fmt (paths, ptrs) =
+ fprintf fmt "\\separated(@[<v>%s, %s@;%a@;%a@])"
self
- (pp_print_list
- ~pp_prologue:pp_print_comma
- ~pp_sep:pp_print_comma
- pp_instance)
+ mem
+ (pp_comma_list
+ ~pp_prologue:pp_print_comma'
+ (pp_instance self))
paths
- (pp_print_list
- ~pp_prologue:pp_print_comma
- ~pp_sep:pp_print_comma
+ (pp_comma_list
+ ~pp_prologue:pp_print_comma'
pp_var_decl)
ptrs
let pp_separated' =
- pp_print_list
+ pp_comma_list
~pp_prologue:(fun fmt () -> pp_print_string fmt "\\separated(")
~pp_epilogue:pp_print_cpar
- ~pp_sep:pp_print_comma
pp_var_decl
+let pp_par pp fmt =
+ fprintf fmt "(%a)" pp
+
let pp_forall pp_l pp_r fmt (l, r) =
fprintf fmt "@[<v 2>\\forall %a;@,%a@]"
pp_l l
@@ -350,12 +207,30 @@ let pp_and_l pp_v fmt =
pp_v
fmt
+let pp_or pp_l pp_r fmt (l, r) =
+ fprintf fmt "@[<v>%a @ || %a@]"
+ pp_l l
+ pp_r r
+
+let pp_or_l pp_v fmt =
+ pp_print_list
+ ~pp_open_box:pp_open_vbox0
+ ~pp_sep:(fun fmt () -> fprintf fmt "@,|| ")
+ pp_v
+ fmt
+
+let pp_not pp fmt =
+ fprintf fmt "!%a" pp
+
let pp_valid pp =
pp_and_l
(* pp_print_list *)
(* ~pp_sep:pp_print_cut *)
(fun fmt x -> fprintf fmt "\\valid(%a)" pp x)
+let pp_old pp fmt =
+ fprintf fmt "\\old(%a)" pp
+
let pp_ite pp_c pp_t pp_f fmt (c, t, f) =
fprintf fmt "(%a @[<hov>? %a@ : %a)@]"
pp_c c
@@ -365,31 +240,18 @@ let pp_ite pp_c pp_t pp_f fmt (c, t, f) =
let pp_paren pp fmt v =
fprintf fmt "(%a)" pp v
-let pp_machine_decl fmt (id, mem_type, var) =
- fprintf fmt "struct %s_%s %s" id mem_type var
-
-let pp_mem_ghost pp_mem pp_self ?i fmt (name, mem, self) =
- fprintf fmt "%s_ghost%a(@[<hov>%a,@ %a@])"
- name
- (pp_print_option pp_print_int) i
- pp_mem mem
- pp_self self
-
-let pp_mem_ghost' = pp_mem_ghost pp_print_string pp_print_string
-
-let pp_mem_init pp_mem fmt (name, mem) =
+let pp_initialization pp_mem fmt (name, mem) =
fprintf fmt "%s_initialization(%a)" name pp_mem mem
-let pp_mem_init' = pp_mem_init pp_print_string
+let pp_initialization' = pp_initialization pp_print_string
-let pp_locals m fmt vs =
- pp_print_list
+let pp_locals m =
+ pp_comma_list
~pp_open_box:pp_open_hbox
- ~pp_sep:pp_print_comma
- (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m) fmt vs
+ (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m)
let pp_ptr_decl fmt v =
- fprintf fmt "*%s" v.var_id
+ pp_ptr fmt v.var_id
let pp_basic_assign_spec pp_l pp_r fmt typ var_name value =
if Types.is_real_type typ && !Options.mpfr
@@ -399,8 +261,8 @@ let pp_basic_assign_spec pp_l pp_r fmt typ var_name value =
else
pp_equal pp_l pp_r fmt (var_name, value)
-let pp_assign_spec
- m self_l pp_var_l self_r pp_var_r fmt (var_type, var_name, value) =
+let pp_assign_spec m self_l pp_var_l indirect_l self_r pp_var_r indirect_r fmt
+ (var_type, var_name, value) =
let depth = expansion_depth value in
let loop_vars = mk_loop_variables m var_type depth in
let reordered_loop_vars = reorder_loop_variables loop_vars in
@@ -408,8 +270,8 @@ let pp_assign_spec
match vars with
| [] ->
pp_basic_assign_spec
- (pp_value_suffix ~indirect:false m self_l var_type loop_vars pp_var_l)
- (pp_value_suffix ~indirect:false m self_r var_type loop_vars pp_var_r)
+ (pp_value_suffix ~indirect:indirect_l m self_l var_type loop_vars pp_var_l)
+ (pp_value_suffix ~indirect:indirect_r m self_r var_type loop_vars pp_var_r)
fmt typ var_name value
| (_d, LVar _i) :: _q ->
assert false
@@ -441,118 +303,210 @@ let pp_c_var_read m fmt id =
else
fprintf fmt "%s" id.var_id
-let rec assigned s instr =
- let open VDSet in
- match instr.instr_desc with
- | MLocalAssign (x, _) ->
- add x s
- | MStep (xs, _, _) ->
- union s (of_list xs)
- | MBranch (_, brs) ->
- List.(fold_left (fun s (_, instrs) -> fold_left assigned s instrs) s brs)
- | _ -> s
-
-let rec occur_val s v =
- let open VDSet in
- match v.value_desc with
- | Var x ->
- add x s
- | Fun (_, vs)
- | Array vs ->
- List.fold_left occur_val s vs
- | Access (v1, v2)
- | Power (v1, v2) ->
- occur_val (occur_val s v1) v2
- | _ -> s
-
-let rec occur s instr =
- let open VDSet in
- match instr.instr_desc with
- | MLocalAssign (_, v)
- | MStateAssign (_, v) ->
- occur_val s v
- | MStep (_, _, vs) ->
- List.fold_left occur_val s vs
- | MBranch (v, brs) ->
- List.(fold_left (fun s (_, instrs) -> fold_left occur s instrs)
- (occur_val s v) brs)
- | _ -> s
-
-let live = Hashtbl.create 32
-
-let set_live_of m =
- let open VDSet in
- let locals = of_list m.mstep.step_locals in
- let outputs = of_list m.mstep.step_outputs in
- let vars = union locals outputs in
- let no_occur_after i =
- let occ, _ = List.fold_left (fun (s, j) instr ->
- if j <= i then (s, j+1) else (occur s instr, j+1))
- (empty, 0) m.mstep.step_instrs in
- diff locals occ
- in
- let l, _, _ = List.fold_left (fun (l, asg, i) instr ->
- let asg = inter (assigned asg instr) vars in
- Live.add (i + 1) (diff asg (no_occur_after i)) l, asg, i + 1)
- (Live.empty, empty, 0) m.mstep.step_instrs in
- Hashtbl.add live m.mname.node_id (Live.add 0 empty l)
+let pp_nothing fmt () =
+ pp_print_string fmt "\\nothing"
-let live_i m i =
- Live.find i (Hashtbl.find live m.mname.node_id)
+let pp_memory_pack_aux ?i pp_mem pp_self fmt (name, mem, self) =
+ fprintf fmt "%s_pack%a(@[<hov>%a,@ %a@])"
+ name
+ (pp_print_option pp_print_int) i
+ pp_mem mem
+ pp_self self
+
+let pp_memory_pack pp_mem pp_self fmt (mp, mem, self) =
+ pp_memory_pack_aux ?i:mp.mpindex pp_mem pp_self fmt
+ (mp.mpname.node_id, mem, self)
+
+let pp_memory_pack_aux' ?i fmt =
+ pp_memory_pack_aux ?i pp_print_string pp_print_string fmt
+let pp_memory_pack' fmt =
+ pp_memory_pack pp_print_string pp_print_string fmt
-let pp_mem_trans_aux ?i stateless pp_mem_in pp_mem_out pp_input pp_output fmt
+let pp_transition_aux ?i m pp_mem_in pp_mem_out pp_input pp_output fmt
(name, inputs, locals, outputs, mem_in, mem_out) =
- fprintf fmt "%s_transition%a(@[<hov>%a%a%a%a%a@])"
+ let stateless = fst (get_stateless_status m) in
+ fprintf fmt "%s_transition%a(@[<hov>%t%a%a%t%a@])"
name
(pp_print_option pp_print_int) i
- (fun fmt () -> if not stateless then fprintf fmt "%a,@ " pp_mem_in mem_in) ()
- (pp_print_list
- (* ~pp_epilogue:pp_print_comma *)
- ~pp_sep:pp_print_comma
- pp_input) inputs
- (pp_print_option
- (fun fmt _ ->
- pp_print_list
- ~pp_prologue:pp_print_comma
- ~pp_sep:pp_print_comma
- pp_input fmt locals))
+ (fun fmt -> if not stateless then fprintf fmt "%a,@ " pp_mem_in mem_in)
+ (pp_comma_list pp_input) inputs
+ (pp_print_option (fun fmt _ ->
+ pp_comma_list ~pp_prologue:pp_print_comma pp_input fmt locals))
i
- (fun fmt () -> if not stateless then fprintf fmt ",@ %a" pp_mem_out mem_out) ()
- (pp_print_list
- ~pp_prologue:pp_print_comma
- ~pp_sep:pp_print_comma
- pp_output) outputs
-
-let pp_mem_trans ?i pp_mem_in pp_mem_out pp_input pp_output fmt
- (m, mem_in, mem_out) =
- let locals, outputs = match i with
- | Some 0 ->
- [], []
- | Some i when i < List.length m.mstep.step_instrs ->
- let li = live_i m i in
- VDSet.(inter (of_list m.mstep.step_locals) li |> elements,
- inter (of_list m.mstep.step_outputs) li |> elements)
- | Some _ ->
- [], m.mstep.step_outputs
- | _ ->
- m.mstep.step_locals, m.mstep.step_outputs
- in
- pp_mem_trans_aux ?i (fst (get_stateless_status m))
- pp_mem_in pp_mem_out pp_input pp_output fmt
- (m.mname.node_id,
- m.mstep.step_inputs,
- locals,
- outputs,
- mem_in,
- mem_out)
-
-let pp_mem_trans' ?i fmt =
- pp_mem_trans ?i pp_print_string pp_print_string pp_var_decl pp_var_decl fmt
-let pp_mem_trans'' ?i fmt =
- pp_mem_trans ?i pp_print_string pp_print_string pp_var_decl pp_ptr_decl fmt
+ (fun fmt -> if not stateless then fprintf fmt ",@ %a" pp_mem_out mem_out)
+ (pp_comma_list ~pp_prologue:pp_print_comma pp_output) outputs
+
+let pp_transition m pp_mem_in pp_mem_out pp_input pp_output fmt
+ (t, mem_in, mem_out) =
+ pp_transition_aux ?i:t.tindex m pp_mem_in pp_mem_out pp_input pp_output fmt
+ (t.tname.node_id, t.tinputs, t.tlocals, t.toutputs, mem_in, mem_out)
+
+let pp_transition_aux' ?i m =
+ pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl pp_var_decl
+let pp_transition_aux'' ?i m =
+ pp_transition_aux ?i m pp_print_string pp_print_string pp_var_decl pp_ptr_decl
+let pp_transition' m =
+ pp_transition m pp_print_string pp_print_string pp_var_decl pp_var_decl
+let pp_transition'' m =
+ pp_transition m pp_print_string pp_print_string pp_var_decl pp_ptr_decl
+
+let pp_reset_cleared pp_mem_in pp_mem_out fmt (name, mem_in, mem_out) =
+ fprintf fmt "%s_reset_cleared(@[<hov>%a,@ %a@])"
+ name
+ pp_mem_in mem_in
+ pp_mem_out mem_out
+
+let pp_reset_cleared' = pp_reset_cleared pp_print_string pp_print_string
+
+module PrintSpec = struct
+
+ let pp_reg pp_mem fmt = function
+ | ResetFlag ->
+ fprintf fmt "%t_reset" pp_mem
+ | StateVar x ->
+ fprintf fmt "%t%a" pp_mem pp_var_decl x
+
+ let pp_expr:
+ type a. machine_t -> (formatter -> unit) -> formatter -> (value_t, a) expression_t -> unit =
+ fun m pp_mem fmt -> function
+ | Val v -> pp_val m fmt v
+ | Tag t -> pp_print_string fmt t
+ | Var v -> pp_var_decl fmt v
+ | Memory r -> pp_reg pp_mem fmt r
+
+ let pp_predicate m mem_in mem_in' mem_out mem_out' fmt p =
+ let pp_expr: type a. formatter -> (value_t, a) expression_t -> unit =
+ fun fmt e -> pp_expr m (fun fmt -> fprintf fmt "%s." mem_out) fmt e
+ in
+ match p with
+ | Transition (f, inst, i, inputs, locals, outputs) ->
+ let pp_mem_in, pp_mem_out = match inst with
+ | None ->
+ pp_print_string, pp_print_string
+ | Some inst ->
+ (fun fmt mem_in -> pp_access' fmt (mem_in, inst)),
+ (fun fmt mem_out -> pp_access' fmt (mem_out, inst))
+ in
+ pp_transition_aux ?i m pp_mem_in pp_mem_out pp_expr pp_expr fmt
+ (f, inputs, locals, outputs, mem_in', mem_out')
+ | MemoryPack (f, inst, i) ->
+ let pp_mem, pp_self = match inst with
+ | None ->
+ pp_print_string, pp_print_string
+ | Some inst ->
+ (fun fmt mem -> pp_access' fmt (mem, inst)),
+ (fun fmt self -> pp_indirect' fmt (self, inst))
+ in
+ pp_memory_pack_aux ?i pp_mem pp_self fmt (f, mem_out, mem_in)
+ | ResetCleared f ->
+ pp_reset_cleared' fmt (f, mem_in, mem_out)
+ (* fprintf fmt "ResetCleared_%a" pp_print_string f *)
+ | Initialization -> ()
+
+ let reset_flag = dummy_var_decl "_reset" Type_predef.type_bool
+
+ let val_of_expr: type a. (value_t, a) expression_t -> value_t = function
+ | Val v -> v
+ | Tag t -> id_to_tag t
+ | Var v -> vdecl_to_val v
+ | Memory (StateVar v) -> vdecl_to_val v
+ | Memory ResetFlag -> vdecl_to_val reset_flag
+
+ type mode =
+ | MemoryPackMode
+ | TransitionMode
+ | ResetIn
+ | ResetOut
+ | InstrMode of ident
+
+ let find_arrow m =
+ try
+ List.find (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances
+ |> fst
+ with Not_found -> eprintf "Internal error: arrow not found"; raise Not_found
+
+ let pp_spec mode m =
+ let rec pp_spec mode fmt f =
+ let mem_in, mem_in', indirect_r, mem_out, mem_out', indirect_l =
+ let self = mk_self m in
+ let mem = mk_mem m in
+ let mem_in = mk_mem_in m in
+ let mem_out = mk_mem_out m in
+ let mem_reset = mk_mem_reset m in
+ match mode with
+ | MemoryPackMode ->
+ self, self, true, mem, mem, false
+ | TransitionMode ->
+ mem_in, mem_in, false, mem_out, mem_out, false
+ | ResetIn ->
+ mem_in, mem_in, false, mem_reset, mem_reset, false
+ | ResetOut ->
+ mem_reset, mem_reset, false, mem_out, mem_out, false
+ | InstrMode self ->
+ let mem = "*" ^ mem in
+ fprintf str_formatter "%a" (pp_at pp_print_string) (mem, reset_label);
+ self, flush_str_formatter (), false,
+ mem, mem, false
+ in
+ let pp_expr: type a. formatter -> (value_t, a) expression_t -> unit =
+ fun fmt e -> pp_expr m (fun fmt -> fprintf fmt "%s." mem_out) fmt e
+ in
+ let pp_spec' = pp_spec mode in
+ match f with
+ | True ->
+ pp_true fmt ()
+ | False ->
+ pp_false fmt ()
+ | Equal (a, b) ->
+ pp_assign_spec m
+ mem_out (pp_c_var_read m) indirect_l
+ mem_in (pp_c_var_read m) indirect_r
+ fmt
+ (type_of_l_value a, val_of_expr a, val_of_expr b)
+ | And fs ->
+ pp_and_l pp_spec' fmt fs
+ | Or fs ->
+ pp_or_l pp_spec' fmt fs
+ | Imply (a, b) ->
+ pp_par (pp_implies pp_spec' pp_spec') fmt (a, b)
+ | Exists (xs, a) ->
+ pp_exists (pp_locals m) pp_spec' fmt (xs, a)
+ | Forall (xs, a) ->
+ pp_forall (pp_locals m) pp_spec' fmt (xs, a)
+ | Ternary (e, a, b) ->
+ pp_ite pp_expr pp_spec' pp_spec' fmt (e, a, b)
+ | Predicate p ->
+ pp_predicate m mem_in mem_in' mem_out mem_out' fmt p
+ | StateVarPack ResetFlag ->
+ let r = vdecl_to_val reset_flag in
+ pp_assign_spec m
+ mem_out (pp_c_var_read m) indirect_l
+ mem_in (pp_c_var_read m) indirect_r
+ fmt
+ (Type_predef.type_bool, r, r)
+ | StateVarPack (StateVar v) ->
+ let v' = vdecl_to_val v in
+ let inst = find_arrow m in
+ pp_par (pp_implies
+ (pp_not (pp_initialization pp_access'))
+ (pp_assign_spec m
+ mem_out (pp_c_var_read m) indirect_l
+ mem_in (pp_c_var_read m) indirect_r))
+ fmt
+ ((Arrow.arrow_id, (mem_out, inst)),
+ (v.var_type, v', v'))
+ | ExistsMem (rc, tr) ->
+ pp_exists
+ (pp_machine_decl' ~ghost:true)
+ (pp_and (pp_spec ResetIn) (pp_spec ResetOut))
+ fmt
+ ((m.mname.node_id, mk_mem_reset m),
+ (rc, tr))
+ (* fprintf fmt "@[<hv 2>∃ MEM,@ %a@]" pp_spec f *)
+ in
+ pp_spec mode
-let pp_nothing fmt () =
- pp_print_string fmt "\\nothing"
+end
let pp_predicate pp_l pp_r fmt (l, r) =
fprintf fmt "@[<v 2>predicate %a =@,%a;@]"
@@ -563,227 +517,175 @@ let print_machine_valid_predicate fmt m =
if not (fst (get_stateless_status m)) then
let name = m.mname.node_id in
let self = mk_self m in
- pp_spec
+ pp_acsl
(pp_predicate
- (pp_mem_valid pp_machine_decl)
+ (pp_mem_valid (pp_machine_decl pp_ptr))
(pp_and
(pp_and_l (fun fmt (_, (td, _) as inst) ->
pp_mem_valid (pp_inst self) fmt (node_name td, inst)))
(pp_valid pp_print_string)))
fmt
- ((name, (name, "mem", "*" ^ self)),
+ ((name, (name, self)),
(m.minstances, [self]))
-let print_machine_ghost_simulation_aux ?i m pp fmt v =
- let name = m.mname.node_id in
+
+let pp_memory_pack_def m fmt mp =
+ let name = mp.mpname.node_id in
let self = mk_self m in
let mem = mk_mem m in
- pp_spec
+ pp_acsl
(pp_predicate
- (pp_mem_ghost pp_machine_decl pp_machine_decl ?i)
- pp)
+ (pp_memory_pack (pp_machine_decl' ~ghost:true) (pp_machine_decl pp_ptr))
+ (PrintSpec.pp_spec MemoryPackMode m))
fmt
- ((name, (name, "mem_ghost", mem), (name, "mem", "*" ^ self)),
- v)
-
-let print_ghost_simulation dependencies m fmt (i, instr) =
- let name = m.mname.node_id in
- let self = mk_self m in
- let mem = mk_mem m in
- let prev_ghost fmt () = pp_mem_ghost' ~i fmt (name, mem, self) in
- let pred pp v = pp_and prev_ghost pp fmt ((), v) in
- let rec aux fmt instr =
- match instr.instr_desc with
- | MStateAssign (m, _) ->
- pp_equal
- (pp_access pp_print_string (pp_access pp_print_string pp_var_decl))
- (pp_indirect pp_print_string (pp_access pp_print_string pp_var_decl))
- fmt
- ((mem, ("_reg", m)), (self, ("_reg", m)))
- | MStep ([i0], i, vl)
- when Basic_library.is_value_internal_fun
- (mk_val (Fun (i, vl)) i0.var_type) ->
- pp_true fmt ()
- | MStep (_, i, _) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
- pp_true fmt ()
- | MStep ([_], i, _) when has_c_prototype i dependencies ->
- pp_true fmt ()
- | MStep (_, i, _)
- | MReset i ->
- begin try
- let n, _ = List.assoc i m.minstances in
- pp_mem_ghost pp_access' pp_indirect' fmt
- (node_name n, (mem, i), (self, i))
- with Not_found -> pp_true fmt ()
- end
- | MBranch (_, brs) ->
- (* TODO: handle branches *)
- pp_and_l aux fmt List.(flatten (map snd brs))
- | _ -> pp_true fmt ()
- in
- pred aux instr
-
-let print_machine_ghost_simulation dependencies m fmt i instr =
- print_machine_ghost_simulation_aux m
- (print_ghost_simulation dependencies m)
- ~i:(i+1)
- fmt (i, instr)
+ ((mp, (name, mem), (name, self)),
+ mp.mpformula)
let print_machine_ghost_struct fmt m =
- pp_spec (pp_ghost (print_machine_struct ~ghost:true)) fmt m
+ pp_acsl (pp_ghost (print_machine_struct ~ghost:true)) fmt m
-let print_machine_ghost_simulations dependencies fmt m =
+let pp_memory_pack_defs fmt m =
if not (fst (get_stateless_status m)) then
- let name = m.mname.node_id in
- let self = mk_self m in
- let mem = mk_mem m in
- fprintf fmt "%a@,%a@,%a%a"
+ fprintf fmt "%a@,%a"
print_machine_ghost_struct m
- (print_machine_ghost_simulation_aux m pp_true ~i:0) ()
- (pp_print_list_i
- ~pp_epilogue:pp_print_cut
- ~pp_open_box:pp_open_vbox0
- (print_machine_ghost_simulation dependencies m))
- m.mstep.step_instrs
- (print_machine_ghost_simulation_aux m
- (pp_mem_ghost' ~i:(List.length m.mstep.step_instrs))) (name, mem, self)
-
-let print_machine_trans_simulation_aux ?i m pp fmt v =
- let name = m.mname.node_id in
+ (pp_print_list
+ ~pp_epilogue:pp_print_cut
+ ~pp_open_box:pp_open_vbox0
+ (pp_memory_pack_def m)) m.mspec.mmemory_packs
+
+let pp_transition_def m fmt t =
+ let name = t.tname.node_id in
let mem_in = mk_mem_in m in
let mem_out = mk_mem_out m in
- pp_spec
+ pp_acsl
(pp_predicate
- (pp_mem_trans pp_machine_decl pp_machine_decl
- (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m)
+ (pp_transition m
+ (pp_machine_decl' ~ghost:true) (pp_machine_decl' ~ghost:true)
(pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m)
- ?i)
- pp)
+ (pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m))
+ (PrintSpec.pp_spec TransitionMode m))
fmt
- ((m, (name, "mem_ghost", mem_in), (name, "mem_ghost", mem_out)),
- v)
-
-let print_trans_simulation dependencies m fmt (i, instr) =
- let mem_in = mk_mem_in m in
- let mem_out = mk_mem_out m in
- let d = VDSet.(diff (union (live_i m i) (assigned empty instr))
- (live_i m (i+1))) in
- (* XXX *)
- (* printf "%d : %a\n%d : %a\nocc: %a\n\n"
- * i
- * (pp_print_parenthesized pp_var_decl) (VDSet.elements (live_i m i))
- * (i+1)
- * (pp_print_parenthesized pp_var_decl) (VDSet.elements (live_i m (i+1)))
- * (pp_print_parenthesized pp_var_decl) VDSet.(elements (assigned empty instr)); *)
- let prev_trans fmt () = pp_mem_trans' ~i fmt (m, mem_in, mem_out) in
- let pred pp v =
- let vars = VDSet.(union (of_list m.mstep.step_locals)
- (of_list m.mstep.step_outputs)) in
- let locals = VDSet.(inter vars d |> elements) in
- if locals = []
- then pp_and prev_trans pp fmt ((), v)
- else pp_exists (pp_locals m) (pp_and prev_trans pp) fmt (locals, ((), v))
- in
- let rec aux fmt instr = match instr.instr_desc with
- | MLocalAssign (x, v)
- | MStateAssign (x, v) ->
- pp_assign_spec m mem_out (pp_c_var_read m) mem_in (pp_c_var_read m) fmt
- (x.var_type, mk_val (Var x) x.var_type, v)
- | MStep ([i0], i, vl)
- when Basic_library.is_value_internal_fun
- (mk_val (Fun (i, vl)) i0.var_type) ->
- pp_true fmt ()
- | MStep (_, i, _) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
- pp_true fmt ()
- | MStep ([_], i, _) when has_c_prototype i dependencies ->
- pp_true fmt ()
- | MStep (xs, i, ys) ->
- begin try
- let n, _ = List.assoc i m.minstances in
- pp_mem_trans_aux
- (fst (get_stateless_status_top_decl n))
- pp_access' pp_access'
- (pp_c_val m mem_in (pp_c_var_read m))
- pp_var_decl
- fmt
- (node_name n, ys, [], xs, (mem_in, i), (mem_out, i))
- with Not_found -> pp_true fmt ()
- end
- | MReset i ->
- begin try
- let n, _ = List.assoc i m.minstances in
- pp_mem_init' fmt (node_name n, mem_out)
- with Not_found -> pp_true fmt ()
- end
- | MBranch (v, brs) ->
- if let t = fst (List.hd brs) in t = tag_true || t = tag_false
- then (* boolean case *)
- pp_ite (pp_c_val m mem_in (pp_c_var_read m))
- (fun fmt () ->
- match List.assoc tag_true brs with
- | _ :: _ as l -> pp_paren (pp_and_l aux) fmt l
- | []
- | exception Not_found -> pp_true fmt ())
- (fun fmt () ->
- match List.assoc tag_false brs with
- | _ :: _ as l -> pp_paren (pp_and_l aux) fmt l
- | []
- | exception Not_found -> pp_true fmt ())
- fmt (v, (), ())
- else (* enum type case *)
- pp_and_l (fun fmt (l, instrs) ->
- let pp_val = pp_c_val m mem_in (pp_c_var_read m) in
- pp_paren (pp_implies
- (pp_equal pp_val pp_c_tag)
- (pp_and_l aux))
- fmt
- ((v, l), instrs))
- fmt brs
- | _ -> pp_true fmt ()
- in
- pred aux instr
-
-let print_machine_trans_simulation dependencies m fmt i instr =
- print_machine_trans_simulation_aux m
- (print_trans_simulation dependencies m)
- ~i:(i+1)
- fmt (i, instr)
-
-let print_machine_trans_annotations dependencies fmt m =
- set_live_of m;
- let i = List.length m.mstep.step_instrs in
- let mem_in = mk_mem_in m in
- let mem_out = mk_mem_out m in
- let last_trans fmt () =
- let locals = VDSet.(inter
- (of_list m.mstep.step_locals)
- (live_i m i)
- |> elements) in
- if locals = []
- then pp_mem_trans' ~i fmt (m, mem_in, mem_out)
- else pp_exists (pp_locals m) (pp_mem_trans' ~i) fmt
- (locals, (m, mem_in, mem_out))
- in
- fprintf fmt "%a@,%a%a"
- (print_machine_trans_simulation_aux m pp_true ~i:0) ()
- (pp_print_list_i
+ ((t, (name, mem_in), (name, mem_out)),
+ t.tformula)
+
+(* let print_trans_simulation dependencies m fmt (i, instr) =
+ * let mem_in = mk_mem_in m in
+ * let mem_out = mk_mem_out m in
+ * let d = VDSet.(diff (union (live_i m i) (assigned empty instr))
+ * (live_i m (i+1))) in
+ * (\* XXX *\)
+ * (\* printf "%d : %a\n%d : %a\nocc: %a\n\n"
+ * * i
+ * * (pp_print_parenthesized pp_var_decl) (VDSet.elements (live_i m i))
+ * * (i+1)
+ * * (pp_print_parenthesized pp_var_decl) (VDSet.elements (live_i m (i+1)))
+ * * (pp_print_parenthesized pp_var_decl) VDSet.(elements (assigned empty instr)); *\)
+ * let prev_trans fmt () = pp_mem_trans' ~i fmt (m, mem_in, mem_out) in
+ * let pred pp v =
+ * let vars = VDSet.(union (of_list m.mstep.step_locals)
+ * (of_list m.mstep.step_outputs)) in
+ * let locals = VDSet.(inter vars d |> elements) in
+ * if locals = []
+ * then pp_and prev_trans pp fmt ((), v)
+ * else pp_exists (pp_locals m) (pp_and prev_trans pp) fmt (locals, ((), v))
+ * in
+ * let rec aux fmt instr = match instr.instr_desc with
+ * | MLocalAssign (x, v)
+ * | MStateAssign (x, v) ->
+ * pp_assign_spec m mem_out (pp_c_var_read m) mem_in (pp_c_var_read m) fmt
+ * (x.var_type, mk_val (Var x) x.var_type, v)
+ * | MStep ([i0], i, vl)
+ * when Basic_library.is_value_internal_fun
+ * (mk_val (Fun (i, vl)) i0.var_type) ->
+ * pp_true fmt ()
+ * | MStep (_, i, _) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
+ * pp_true fmt ()
+ * | MStep ([_], i, _) when has_c_prototype i dependencies ->
+ * pp_true fmt ()
+ * | MStep (xs, i, ys) ->
+ * begin try
+ * let n, _ = List.assoc i m.minstances in
+ * pp_mem_trans_aux
+ * (fst (get_stateless_status_top_decl n))
+ * pp_access' pp_access'
+ * (pp_c_val m mem_in (pp_c_var_read m))
+ * pp_var_decl
+ * fmt
+ * (node_name n, ys, [], xs, (mem_in, i), (mem_out, i))
+ * with Not_found -> pp_true fmt ()
+ * end
+ * | MReset i ->
+ * begin try
+ * let n, _ = List.assoc i m.minstances in
+ * pp_mem_init' fmt (node_name n, mem_out)
+ * with Not_found -> pp_true fmt ()
+ * end
+ * | MBranch (v, brs) ->
+ * if let t = fst (List.hd brs) in t = tag_true || t = tag_false
+ * then (\* boolean case *\)
+ * pp_ite (pp_c_val m mem_in (pp_c_var_read m))
+ * (fun fmt () ->
+ * match List.assoc tag_true brs with
+ * | _ :: _ as l -> pp_paren (pp_and_l aux) fmt l
+ * | []
+ * | exception Not_found -> pp_true fmt ())
+ * (fun fmt () ->
+ * match List.assoc tag_false brs with
+ * | _ :: _ as l -> pp_paren (pp_and_l aux) fmt l
+ * | []
+ * | exception Not_found -> pp_true fmt ())
+ * fmt (v, (), ())
+ * else (\* enum type case *\)
+ * pp_and_l (fun fmt (l, instrs) ->
+ * let pp_val = pp_c_val m mem_in (pp_c_var_read m) in
+ * pp_paren (pp_implies
+ * (pp_equal pp_val pp_c_tag)
+ * (pp_and_l aux))
+ * fmt
+ * ((v, l), instrs))
+ * fmt brs
+ * | _ -> pp_true fmt ()
+ * in
+ * pred aux instr *)
+
+(* let print_machine_trans_simulation dependencies m fmt i instr =
+ * print_machine_trans_simulation_aux m
+ * (print_trans_simulation dependencies m)
+ * ~i:(i+1)
+ * fmt (i, instr) *)
+
+let pp_transition_defs fmt m =
+ (* set_live_of m; *)
+ (* let i = List.length m.mstep.step_instrs in *)
+ (* let mem_in = mk_mem_in m in
+ * let mem_out = mk_mem_out m in *)
+ (* let last_trans fmt () =
+ * let locals = VDSet.(inter
+ * (of_list m.mstep.step_locals)
+ * (live_i m i)
+ * |> elements) in
+ * if locals = []
+ * then pp_mem_trans' ~i fmt (m, mem_in, mem_out)
+ * else pp_exists (pp_locals m) (pp_mem_trans' ~i) fmt
+ * (locals, (m, mem_in, mem_out))
+ * in *)
+ fprintf fmt "%a"
+ (pp_print_list
~pp_epilogue:pp_print_cut
~pp_open_box:pp_open_vbox0
- (print_machine_trans_simulation dependencies m))
- m.mstep.step_instrs
- (print_machine_trans_simulation_aux m last_trans) ()
+ (pp_transition_def m)) m.mspec.mtransitions
let print_machine_init_predicate fmt m =
if not (fst (get_stateless_status m)) then
let name = m.mname.node_id in
let mem_in = mk_mem_in m in
- pp_spec
+ pp_acsl
(pp_predicate
- (pp_mem_init pp_machine_decl)
+ (pp_initialization (pp_machine_decl' ~ghost:true))
(pp_and_l (fun fmt (i, (td, _)) ->
- pp_mem_init pp_access' fmt (node_name td, (mem_in, i)))))
+ pp_initialization pp_access' fmt (node_name td, (mem_in, i)))))
fmt
- ((name, (name, "mem_ghost", mem_in)), m.minstances)
+ ((name, (name, mem_in)), m.minstances)
let pp_at pp_p fmt (p, l) =
fprintf fmt "\\at(%a, %s)" pp_p p l
@@ -793,15 +695,34 @@ let label_pre = "Pre"
let pp_at_pre pp_p fmt p =
pp_at pp_p fmt (p, label_pre)
-let pp_register =
+let pp_register ?(indirect=true) ptr =
pp_print_list
- ~pp_prologue:(fun fmt () -> pp_print_string fmt "self->")
- ~pp_epilogue:(fun fmt () -> pp_print_string fmt "->_reg._first")
- ~pp_sep:(fun fmt () -> pp_print_string fmt "->")
+ ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
+ ~pp_epilogue:(fun fmt () -> fprintf fmt "%s_reg._first"
+ (if indirect then "->" else "."))
+ ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
(fun fmt (i, _) -> pp_print_string fmt i)
+let pp_reset_flag ?(indirect=true) ptr fmt mems =
+ pp_print_list
+ ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
+ ~pp_epilogue:(fun fmt () -> fprintf fmt "%s_reset"
+ (if indirect then "->" else "."))
+ ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
+ (fun fmt (i, _) -> pp_print_string fmt i)
+ fmt mems
+
+module GhostProto: MODIFIERS_GHOST_PROTO = struct
+ let pp_ghost_parameters fmt vs =
+ fprintf fmt "@;%a"
+ (pp_acsl (pp_ghost (pp_print_parenthesized (fun fmt (x, pp) -> pp fmt x))))
+ vs
+end
+
module HdrMod = struct
+ module GhostProto = GhostProto
+
let print_machine_decl_prefix = fun _ _ -> ()
let pp_import_standard_spec fmt () =
@@ -813,7 +734,9 @@ end
module SrcMod = struct
- let pp_predicates dependencies fmt machines =
+ module GhostProto = GhostProto
+
+ let pp_predicates (* dependencies *) fmt machines =
fprintf fmt
"%a%a%a%a"
(pp_print_list
@@ -825,7 +748,7 @@ module SrcMod = struct
~pp_open_box:pp_open_vbox0
~pp_sep:pp_print_cutcut
~pp_prologue:(pp_print_endcut "/* ACSL ghost simulations */")
- (print_machine_ghost_simulations dependencies)
+ pp_memory_pack_defs
~pp_epilogue:pp_print_cutcut) machines
(pp_print_list
~pp_open_box:pp_open_vbox0
@@ -837,97 +760,102 @@ module SrcMod = struct
~pp_open_box:pp_open_vbox0
~pp_sep:pp_print_cutcut
~pp_prologue:(pp_print_endcut "/* ACSL transition annotations */")
- (print_machine_trans_annotations dependencies)
+ pp_transition_defs
~pp_epilogue:pp_print_cutcut) machines
- let pp_reset_spec fmt machines self m =
+ let pp_clear_reset_spec fmt machines self mem m =
let name = m.mname.node_id in
- let mem = mk_mem m in
- let insts = instances machines m in
- pp_spec_cut (fun fmt () ->
+ let arws, narws = List.partition (fun (_, (td, _)) -> Arrow.td_is_arrow td)
+ m.minstances in
+ let mk_insts = List.map (fun x -> [x]) in
+ pp_acsl_cut (fun fmt () ->
fprintf fmt
- "%a@,%a@,%a@,%a"
+ "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,\
+ @[<v 2>behavior reset:@;\
+ %a@,%a@]@,\
+ @[<v 2>behavior no_reset:@;\
+ %a@,%a@]"
(pp_requires pp_mem_valid') (name, self)
- (pp_requires (pp_separated self)) (powerset_instances insts, [])
- (pp_assigns pp_register) insts
- (pp_ensures
- (pp_forall
- pp_machine_decl
- (pp_implies
- pp_mem_ghost'
- pp_mem_init')))
- ((name, "mem_ghost", mem),
- ((name, mem, self), (name, mem))))
+ (pp_requires (pp_separated self mem)) (mk_insts m.minstances, [])
+ (pp_ensures (pp_memory_pack_aux
+ ~i:(List.length m.mspec.mmemory_packs - 2)
+ pp_ptr pp_print_string))
+ (name, mem, self)
+ (pp_assigns pp_indirect') [self, "_reset"]
+ (pp_assigns (pp_register self)) (mk_insts arws)
+ (pp_assigns (pp_reset_flag self)) (mk_insts narws)
+ (pp_assigns pp_indirect') [mem, "_reset"]
+ (pp_assigns (pp_register ~indirect:false mem)) (mk_insts arws)
+ (pp_assigns (pp_reset_flag ~indirect:false mem)) (mk_insts narws)
+ (pp_assumes (pp_equal pp_indirect' pp_print_int)) ((mem, "_reset"), 1)
+ (pp_ensures (pp_initialization pp_ptr)) (name, mem)
+ (pp_assumes (pp_equal pp_indirect' pp_print_int)) ((mem, "_reset"), 0)
+ (pp_ensures (pp_equal pp_ptr (pp_old pp_ptr))) (mem, mem)
+ )
fmt ()
- let pp_step_spec fmt machines self m =
+ let pp_set_reset_spec fmt self mem m =
+ let name = m.mname.node_id in
+ pp_acsl_cut (fun fmt () ->
+ fprintf fmt
+ "%a@,%a@,%a"
+ (pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string)) (name, mem, self)
+ (pp_ensures (pp_equal pp_indirect' pp_print_string)) ((mem, "_reset"), "1")
+ (pp_assigns (fun fmt ptr -> pp_indirect' fmt (ptr, "_reset"))) [self; mem])
+ fmt ()
+
+ let pp_step_spec fmt machines self mem m =
let name = m.mname.node_id in
- let mem_in = mk_mem_in m in
- let mem_out = mk_mem_out m in
let insts = instances machines m in
let insts' = powerset_instances insts in
- pp_spec_cut (fun fmt () ->
+ let insts'' = List.(filter (fun l -> l <> [])
+ (map (filter (fun (_, (td, _)) ->
+ not (Arrow.td_is_arrow td))) insts)) in
+ let inputs = m.mstep.step_inputs in
+ let outputs = m.mstep.step_outputs in
+ pp_acsl_cut (fun fmt () ->
if fst (get_stateless_status m) then
fprintf fmt
"%a@,%a@,%a@,%a"
- (pp_requires (pp_valid pp_var_decl)) m.mstep.step_outputs
- (pp_requires pp_separated') m.mstep.step_outputs
- (pp_assigns pp_ptr_decl) m.mstep.step_outputs
- (pp_ensures pp_mem_trans'') (m, mem_in, mem_out)
+ (pp_requires (pp_valid pp_var_decl)) outputs
+ (pp_requires pp_separated') outputs
+ (pp_assigns pp_ptr_decl) outputs
+ (pp_ensures (pp_transition_aux'' m))
+ (name, inputs, [], outputs, "", "")
else
fprintf fmt
- "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a"
- (pp_requires (pp_valid pp_var_decl)) m.mstep.step_outputs
+ "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a"
+ (pp_requires (pp_valid pp_var_decl)) outputs
(pp_requires pp_mem_valid') (name, self)
- (pp_requires (pp_separated self)) (insts', m.mstep.step_outputs)
- (pp_assigns pp_ptr_decl) m.mstep.step_outputs
+ (pp_requires (pp_separated self mem)) (insts', outputs)
+ (pp_requires (pp_memory_pack_aux pp_ptr pp_print_string))
+ (name, mem, self)
+ (pp_assigns pp_ptr_decl) outputs
(pp_assigns (pp_reg self)) m.mmemory
- (pp_assigns pp_memory) (memories insts')
- (pp_assigns pp_register) insts
- (pp_ensures
- (pp_forall
- pp_machine_decl
- (pp_forall
- pp_machine_decl
- (pp_implies
- (pp_at_pre pp_mem_ghost')
- (pp_implies
- pp_mem_ghost'
- pp_mem_trans'')))))
- ((name, "mem_ghost", mem_in),
- ((name, "mem_ghost", mem_out),
- ((name, mem_in, self),
- ((name, mem_out, self),
- (m, mem_in, mem_out)))))
+ (pp_assigns (pp_memory self)) (memories insts')
+ (pp_assigns (pp_register self)) insts
+ (pp_assigns (pp_reset_flag self)) insts''
+ (pp_assigns (pp_reg mem)) m.mmemory
+ (pp_assigns (pp_memory ~indirect:false mem)) (memories insts')
+ (pp_assigns (pp_register ~indirect:false mem)) insts
+ (pp_assigns (pp_reset_flag ~indirect:false mem)) insts''
+ (pp_ensures (pp_transition_aux m (pp_old pp_ptr)
+ pp_ptr pp_var_decl pp_ptr_decl))
+ (name, inputs, [], outputs, mem, mem)
)
fmt ()
- let pp_step_instr_spec m self fmt (i, _instr) =
- let name = m.mname.node_id in
- let mem_in = mk_mem_in m in
- let mem_out = mk_mem_out m in
- if fst (get_stateless_status m) then
- fprintf fmt "@,%a"
- (pp_spec (pp_assert (pp_mem_trans'' ~i))) (m, mem_in, mem_out)
- else
- fprintf fmt "@,%a"
- (pp_spec
- (pp_assert
- (pp_forall
- pp_machine_decl
- (pp_forall
- pp_machine_decl
- (pp_implies
- (pp_at_pre pp_mem_ghost')
- (pp_implies
- (pp_mem_ghost' ~i)
- (pp_mem_trans'' ~i)))))))
- ((name, "mem_ghost", mem_in),
- ((name, "mem_ghost", mem_out),
- ((name, mem_in, self),
- ((name, mem_out, self),
- (m, mem_in, mem_out)))))
-
+ let pp_step_instr_spec m self fmt instr =
+ fprintf fmt "@,%a"
+ (pp_print_list ~pp_open_box:pp_open_vbox0
+ (pp_acsl (pp_assert (PrintSpec.pp_spec (InstrMode self) m))))
+ instr.instr_spec
+
+ let pp_ghost_set_reset_spec fmt =
+ fprintf fmt "@;%a@;"
+ (pp_acsl_line
+ (pp_ghost
+ (fun fmt mem -> fprintf fmt "%a = 1;" pp_indirect' (mem, "_reset"))))
end
(**************************************************************************)
diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index 1df132a0..002ae1d7 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/src/backends/C/c_backend_src.ml
@@ -17,21 +17,29 @@ open Machine_code_common
open C_backend_common
module type MODIFIERS_SRC = sig
- val pp_predicates: dep_t list -> formatter -> machine_t list -> unit
- val pp_reset_spec: formatter -> machine_t list -> ident -> machine_t -> unit
- val pp_step_spec: formatter -> machine_t list -> ident -> machine_t -> unit
- val pp_step_instr_spec: machine_t -> ident -> formatter -> (int * instr_t) -> unit
+ module GhostProto: MODIFIERS_GHOST_PROTO
+ val pp_predicates: formatter -> machine_t list -> unit
+ val pp_set_reset_spec: formatter -> ident -> ident -> machine_t -> unit
+ val pp_clear_reset_spec: formatter -> machine_t list -> ident -> ident -> machine_t -> unit
+ val pp_step_spec: formatter -> machine_t list -> ident -> ident -> machine_t -> unit
+ val pp_step_instr_spec: machine_t -> ident -> formatter -> instr_t -> unit
+ val pp_ghost_set_reset_spec: formatter -> ident -> unit
end
module EmptyMod = struct
- let pp_predicates _ _ _ = ()
- let pp_reset_spec _ _ _ _ = ()
- let pp_step_spec _ _ _ _ = ()
+ module GhostProto = EmptyGhostProto
+ let pp_predicates _ _ = ()
+ let pp_set_reset_spec _ _ _ _ = ()
+ let pp_clear_reset_spec _ _ _ _ _ = ()
+ let pp_step_spec _ _ _ _ _ = ()
let pp_step_instr_spec _ _ _ _ = ()
+ let pp_ghost_set_reset_spec _ _ = ()
end
module Main = functor (Mod: MODIFIERS_SRC) -> struct
+ module Protos = Protos(Mod.GhostProto)
+
(********************************************************************************************)
(* Instruction Printing functions *)
(********************************************************************************************)
@@ -119,50 +127,70 @@ module Main = functor (Mod: MODIFIERS_SRC) -> struct
(*eprintf "end pp_assign@.";*)
end
- let pp_machine_ pp_machine_name fn_name m self fmt inst =
- let (node, static) = try List.assoc inst m.minstances with Not_found ->
- eprintf "internal error: %s %s %s %s:@." fn_name m.mname.node_id self inst;
- raise Not_found
+ let pp_machine_ pp_machine_name fn_name m fmt ?inst self =
+ let name, static =
+ match inst with
+ | Some inst ->
+ let node, static = try List.assoc inst m.minstances with Not_found ->
+ eprintf "internal error: %s %s %s %s:@."
+ fn_name m.mname.node_id self inst;
+ raise Not_found
+ in
+ node_name node, static
+ | None ->
+ m.mname.node_id, []
in
- fprintf fmt "%a(%a%s->%s);"
- pp_machine_name (node_name node)
- (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
- Dimension.pp_dimension) static
- self inst
+ fprintf fmt "%a(%a%s%a);"
+ pp_machine_name name
+ (pp_comma_list ~pp_eol:pp_print_comma Dimension.pp_dimension) static
+ self
+ (pp_print_option (fun fmt -> fprintf fmt "->%s")) inst
+
+ let pp_machine_set_reset m self fmt inst =
+ pp_machine_ pp_machine_set_reset_name "pp_machine_set_reset" m fmt ~inst self
- let pp_machine_reset =
- pp_machine_ pp_machine_reset_name "pp_machine_reset"
+ let pp_machine_clear_reset m self fmt =
+ pp_machine_ pp_machine_clear_reset_name "pp_machine_clear_reset" m fmt self
- let pp_machine_init =
- pp_machine_ pp_machine_init_name "pp_machine_init"
+ let pp_machine_init m self fmt inst =
+ pp_machine_ pp_machine_init_name "pp_machine_init" m fmt ~inst self
- let pp_machine_clear =
- pp_machine_ pp_machine_clear_name "pp_machine_clear"
+ let pp_machine_clear m self fmt inst =
+ pp_machine_ pp_machine_clear_name "pp_machine_clear" m fmt ~inst self
- let pp_call m self pp_read pp_write fmt i
- (inputs: Machine_code_types.value_t list) (outputs: var_decl list) =
+ let pp_call m self pp_read pp_write fmt i inputs outputs =
try (* stateful node instance *)
let n, _ = List.assoc i m.minstances in
- fprintf fmt "%a (%a%a%s->%s);"
+ fprintf fmt "%a(%a%a%s->%s);"
pp_machine_step_name (node_name n)
- (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
+ (pp_comma_list ~pp_eol:pp_print_comma
(pp_c_val m self pp_read)) inputs
- (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
+ (pp_comma_list ~pp_eol:pp_print_comma
pp_write) outputs
self
i
with Not_found -> (* stateless node instance *)
let n, _ = List.assoc i m.mcalls in
- fprintf fmt "%a (%a%a);"
+ fprintf fmt "%a(%a%a);"
pp_machine_step_name (node_name n)
- (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
+ (pp_comma_list ~pp_eol:pp_print_comma
(pp_c_val m self pp_read)) inputs
- (pp_print_list ~pp_sep:pp_print_comma pp_write) outputs
+ (pp_comma_list pp_write) outputs
let pp_basic_instance_call m self =
pp_call m self (pp_c_var_read m) (pp_c_var_write m)
- let pp_instance_call m self fmt i (inputs: Machine_code_types.value_t list) (outputs: var_decl list) =
+ let pp_arrow_call m self fmt i outputs =
+ match outputs with
+ | [x] ->
+ fprintf fmt "%a = %a(%s->%s);"
+ (pp_c_var_read m) x
+ pp_machine_step_name Arrow.arrow_id
+ self
+ i
+ | _ -> assert false
+
+ let pp_instance_call m self fmt i inputs outputs =
let pp_offset pp_var indices fmt var =
fprintf fmt "%a%a"
pp_var var
@@ -196,8 +224,11 @@ module Main = functor (Mod: MODIFIERS_SRC) -> struct
and pp_machine_instr dependencies (m: machine_t) self fmt instr =
match get_instr_desc instr with
| MNoReset _ -> ()
- | MReset i ->
- pp_machine_reset m self fmt i
+ | MSetReset inst ->
+ pp_machine_set_reset m self fmt inst
+ | MClearReset ->
+ fprintf fmt "%t@,%a"
+ (pp_machine_clear_reset m self) pp_label reset_label
| MLocalAssign (i,v) ->
pp_assign
m self (pp_c_var_read m) fmt
@@ -217,7 +248,11 @@ module Main = functor (Mod: MODIFIERS_SRC) -> struct
i
(pp_print_parenthesized (pp_c_val m self (pp_c_var_read m))) vl
| MStep (il, i, vl) ->
- pp_basic_instance_call m self fmt i vl il
+ let td, _ = List.assoc i m.minstances in
+ if Arrow.td_is_arrow td then
+ pp_arrow_call m self fmt i il
+ else
+ pp_basic_instance_call m self fmt i vl il
| MBranch (_, []) ->
eprintf "internal error: C_backend_src.pp_machine_instr %a@."
(pp_instr m) instr;
@@ -249,15 +284,10 @@ module Main = functor (Mod: MODIFIERS_SRC) -> struct
let pp_machine_nospec_instr dependencies m self fmt _i instr =
pp_machine_instr dependencies m self fmt instr
- let pp_machine_step_instr dependencies m self fmt i instr =
- fprintf fmt "%a%a%a"
- (if i = 0 then
- (fun fmt () -> fprintf fmt "%a@,"
- (Mod.pp_step_instr_spec m self) (i, instr))
- else
- pp_print_nothing) ()
+ let pp_machine_step_instr dependencies m self fmt _i instr =
+ fprintf fmt "%a%a"
(pp_machine_instr dependencies m self) instr
- (Mod.pp_step_instr_spec m self) (i+1, instr)
+ (Mod.pp_step_instr_spec m self) instr
(********************************************************************************************)
(* C file Printing functions *)
@@ -438,8 +468,8 @@ module Main = functor (Mod: MODIFIERS_SRC) -> struct
then
(* C99 code *)
pp_print_function
- ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self m)
- ~pp_prototype:print_stateless_prototype
+ ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self self m)
+ ~pp_prototype:Protos.print_stateless_prototype
~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
~pp_local:(pp_c_decl_local_var m)
~base_locals:m.mstep.step_locals
@@ -459,7 +489,7 @@ module Main = functor (Mod: MODIFIERS_SRC) -> struct
let (id, _, _) = call_of_expr e
in mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in
pp_print_function
- ~pp_prototype:print_stateless_prototype
+ ~pp_prototype:Protos.print_stateless_prototype
~prototype:(m.mname.node_id,
m.mstep.step_inputs @ gen_locals @ gen_calls,
m.mstep.step_outputs)
@@ -474,10 +504,10 @@ module Main = functor (Mod: MODIFIERS_SRC) -> struct
~instrs:m.mstep.step_instrs
fmt
- let print_reset_code machines dependencies self fmt m =
+ let print_clear_reset_code machines dependencies self mem fmt m =
pp_print_function
- ~pp_spec:(fun fmt () -> Mod.pp_reset_spec fmt machines self m)
- ~pp_prototype:(print_reset_prototype self)
+ ~pp_spec:(fun fmt () -> Mod.pp_clear_reset_spec fmt machines self mem m)
+ ~pp_prototype:(Protos.print_clear_reset_prototype self mem)
~prototype:(m.mname.node_id, m.mstatic)
~pp_local:(pp_c_decl_local_var m)
~base_locals:(const_locals m)
@@ -485,11 +515,23 @@ module Main = functor (Mod: MODIFIERS_SRC) -> struct
~instrs:m.minit
fmt
+ let print_set_reset_code self mem fmt m =
+ pp_print_function
+ ~pp_spec:(fun fmt () -> Mod.pp_set_reset_spec fmt self mem m)
+ ~pp_prototype:(Protos.print_set_reset_prototype self mem)
+ ~prototype:(m.mname.node_id, m.mstatic)
+ ~pp_extra:(fun fmt () -> fprintf fmt "self->_reset = 1;%a"
+ Mod.pp_ghost_set_reset_spec mem)
+ fmt
+
let print_init_code self fmt m =
let minit = List.map (fun i ->
- match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
+ match get_instr_desc i with
+ | MSetReset i -> i
+ | _ -> assert false)
+ m.minit in
pp_print_function
- ~pp_prototype:(print_init_prototype self)
+ ~pp_prototype:(Protos.print_init_prototype self)
~prototype:(m.mname.node_id, m.mstatic)
~pp_array_mem:(pp_c_decl_array_mem self)
~array_mems:(array_mems m)
@@ -505,9 +547,11 @@ module Main = functor (Mod: MODIFIERS_SRC) -> struct
let print_clear_code self fmt m =
let minit = List.map (fun i ->
- match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
+ match get_instr_desc i with
+ | MSetReset i -> i
+ | _ -> assert false) m.minit in
pp_print_function
- ~pp_prototype:(print_clear_prototype self)
+ ~pp_prototype:(Protos.print_clear_prototype self)
~prototype:(m.mname.node_id, m.mstatic)
~pp_array_mem:(pp_c_decl_array_mem self)
~array_mems:(array_mems m)
@@ -521,13 +565,13 @@ module Main = functor (Mod: MODIFIERS_SRC) -> struct
fmt minit)
fmt
- let print_step_code machines dependencies self fmt m =
+ let print_step_code machines dependencies self mem fmt m =
if not (!Options.ansi && is_generic_node (node_of_machine m))
then
(* C99 code *)
pp_print_function
- ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self m)
- ~pp_prototype:(print_step_prototype self)
+ ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self mem m)
+ ~pp_prototype:(Protos.print_step_prototype self mem)
~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
~pp_local:(pp_c_decl_local_var m)
~base_locals:m.mstep.step_locals
@@ -549,8 +593,8 @@ module Main = functor (Mod: MODIFIERS_SRC) -> struct
let id, _, _ = call_of_expr e in
mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in
pp_print_function
- ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self m)
- ~pp_prototype:(print_step_prototype self)
+ ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self mem m)
+ ~pp_prototype:(Protos.print_step_prototype self mem)
~prototype:(m.mname.node_id,
m.mstep.step_inputs @ gen_locals @ gen_calls,
m.mstep.step_outputs)
@@ -706,12 +750,14 @@ module Main = functor (Mod: MODIFIERS_SRC) -> struct
print_stateless_code machines dependencies fmt m
else
let self = mk_self m in
- fprintf fmt "@[<v>%a%a@,@,%a%a@]"
+ let mem = mk_mem m in
+ fprintf fmt "@[<v>%a%a@,@,%a@,@,%a%a@]"
print_alloc_function m
- (* Reset function *)
- (print_reset_code machines dependencies self) m
+ (* Reset functions *)
+ (print_clear_reset_code machines dependencies self mem) m
+ (print_set_reset_code self mem) m
(* Step function *)
- (print_step_code machines dependencies self) m
+ (print_step_code machines dependencies self mem) m
(print_mpfr_code self) m
let print_import_standard source_fmt () =
@@ -826,7 +872,7 @@ module Main = functor (Mod: MODIFIERS_SRC) -> struct
~pp_epilogue:pp_print_cutcut) machines
(* Print the spec predicates *)
- (Mod.pp_predicates dependencies) machines
+ Mod.pp_predicates machines
(* Print nodes one by one (in the previous order) *)
(pp_print_list
diff --git a/src/backends/EMF/EMF_backend.ml b/src/backends/EMF/EMF_backend.ml
index c144f5b4..ff89bc40 100644
--- a/src/backends/EMF/EMF_backend.ml
+++ b/src/backends/EMF/EMF_backend.ml
@@ -165,7 +165,9 @@ let branch_cpt = ref 0
let get_instr_id fmt i =
match Corelang.get_instr_desc i with
| MLocalAssign(lhs,_) | MStateAssign (lhs, _) -> pp_var_name fmt lhs
- | MReset i | MNoReset i -> fprintf fmt "%s" (reset_name i)
+ | MSetReset i | MNoReset i -> fprintf fmt "%s" (reset_name i)
+ (* TODO: handle clear_reset *)
+ | MClearReset -> ()
| MBranch _ -> incr branch_cpt; fprintf fmt "branch_%i" !branch_cpt
| MStep (outs, id, _) ->
print_protect fmt
@@ -242,10 +244,12 @@ and branch_instr_vars m i =
all_def_vars, def_vars, VSet.union read_guard read_vars
| MBranch _ -> assert false (* branch instruction should admit at least one case *)
- | MReset ni
- | MNoReset ni ->
- let write = ISet.singleton (reset_name ni) in
- write, write, VSet.empty
+ | MSetReset ni
+ | MNoReset ni ->
+ let write = ISet.singleton (reset_name ni) in
+ write, write, VSet.empty
+ (* TODO: handle clear_reset *)
+ | MClearReset -> ISet.empty, ISet.empty, VSet.empty
| MSpec _ | MComment _ -> assert false (* not available for EMF output *)
(* A kind of super join_guards: all MBranch are postponed and sorted by
@@ -298,7 +302,7 @@ let rec pp_emf_instr m fmt i =
(pp_emf_cst_or_var m) expr
)
- | MReset id
+ | MSetReset id
-> (
fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"true\""
(reset_name id)
@@ -308,6 +312,8 @@ let rec pp_emf_instr m fmt i =
fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"false\""
(reset_name id)
)
+ (* TODO: handle clear_reset *)
+ | MClearReset -> ()
| MBranch (g, hl) -> (
let all_outputs, outputs, inputs = branch_instr_vars m i in
diff --git a/src/backends/Horn/horn_backend_printers.ml b/src/backends/Horn/horn_backend_printers.ml
index 9576a3b9..4fe13f20 100644
--- a/src/backends/Horn/horn_backend_printers.ml
+++ b/src/backends/Horn/horn_backend_printers.ml
@@ -295,10 +295,12 @@ let pp_instance_call machines reset_instances m fmt i inputs outputs =
let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ident list =
match get_instr_desc instr with
| MSpec _ | MComment _ -> reset_instances
+ (* TODO: handle clear_reset *)
+ | MClearReset -> reset_instances
| MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
pp_no_reset machines m fmt i;
i::reset_instances
- | MReset i -> (* we assign middle_mem with reset: reset(mem_m) *)
+ | MSetReset i -> (* we assign middle_mem with reset: reset(mem_m) *)
pp_instance_reset machines m fmt i;
i::reset_instances
| MLocalAssign (i,v) ->
diff --git a/src/corelang.ml b/src/corelang.ml
index 32e57bda..a819930d 100644
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -257,7 +257,7 @@ let update_expr_annot node_id e annot =
e
-let mkinstr ?lustre_eq instr_spec instr_desc = {
+let mkinstr ?lustre_eq ?(instr_spec=[]) instr_desc = {
instr_desc;
(* lustre_expr = lustre_expr; *)
instr_spec;
@@ -662,9 +662,10 @@ let get_nodes prog =
List.fold_left (
fun nodes decl ->
match decl.top_decl_desc with
- | Node _ -> decl::nodes
- | Const _ | ImportedNode _ | Include _ | Open _ | TypeDef _ -> nodes
+ | Node _ -> decl::nodes
+ | Const _ | ImportedNode _ | Include _ | Open _ | TypeDef _ -> nodes
) [] prog
+ |> List.rev
let get_imported_nodes prog =
List.fold_left (
diff --git a/src/corelang.mli b/src/corelang.mli
index 0f099f0d..e4d1053f 100644
--- a/src/corelang.mli
+++ b/src/corelang.mli
@@ -12,6 +12,11 @@
open Lustre_types
+module VDeclModule: sig
+ type t
+ val compare: t -> t -> int
+end with type t = Lustre_types.var_decl
+
module VSet: sig
include Set.S
val pp: Format.formatter -> t -> unit
@@ -45,7 +50,7 @@ val mk_new_node_name: node_desc -> ident -> ident
val mktop: top_decl_desc -> top_decl
(* constructor for machine types *)
-val mkinstr: (* ?lustre_expr:expr -> *)?lustre_eq: eq -> Machine_code_types.value_t Spec_types.formula_t -> Machine_code_types.instr_t_desc -> Machine_code_types.instr_t
+val mkinstr: (* ?lustre_expr:expr -> *)?lustre_eq: eq -> ?instr_spec: Machine_code_types.value_t Spec_types.formula_t list -> Machine_code_types.instr_t_desc -> Machine_code_types.instr_t
val get_instr_desc: Machine_code_types.instr_t -> Machine_code_types.instr_t_desc
val update_instr_desc: Machine_code_types.instr_t -> Machine_code_types.instr_t_desc -> Machine_code_types.instr_t
diff --git a/src/dune b/src/dune
index b189c653..ed1caff8 100644
--- a/src/dune
+++ b/src/dune
@@ -23,6 +23,7 @@
machine_code_types
spec_types
spec_common
+ lustre_live
scheduling_type
log
printers
diff --git a/src/lustre_live.ml b/src/lustre_live.ml
new file mode 100644
index 00000000..69c1ce6d
--- /dev/null
+++ b/src/lustre_live.ml
@@ -0,0 +1,104 @@
+(********************************************************************)
+(* *)
+(* The LustreC compiler toolset / The LustreC Development Team *)
+(* Copyright 2012 - -- ONERA - CNRS - INPT *)
+(* *)
+(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
+(* under the terms of the GNU Lesser General Public License *)
+(* version 2.1. *)
+(* *)
+(********************************************************************)
+
+open Lustre_types
+open Dimension
+open Utils
+open ISet
+module Live = Map.Make(Int)
+
+let pp_live fmt l =
+ Live.bindings
+
+let assigned s eq =
+ union s (of_list eq.eq_lhs)
+
+let rec occur_dim_expr s d =
+ match d.dim_desc with
+ | Dident x ->
+ add x s
+ | Dappl (_, ds) ->
+ List.fold_left occur_dim_expr s ds
+ | Dite (e, t, f) ->
+ occur_dim_expr (occur_dim_expr (occur_dim_expr s e) t) f
+ | Dlink d ->
+ occur_dim_expr s d
+ | _ -> s
+
+let rec occur_expr s e =
+ match e.expr_desc with
+ | Expr_ident x ->
+ add x s
+ | Expr_tuple es
+ | Expr_array es ->
+ List.fold_left occur_expr s es
+ | Expr_ite (e, t, f) ->
+ occur_expr (occur_expr (occur_expr s e) t) f
+ | Expr_arrow (e1, e2)
+ | Expr_fby (e1, e2) ->
+ occur_expr (occur_expr s e1) e2
+ | Expr_access (e, d)
+ | Expr_power (e, d) ->
+ occur_expr (occur_dim_expr s d) e
+ | Expr_pre e ->
+ occur_expr s e
+ | Expr_when (e, x, _) ->
+ occur_expr (add x s) e
+ | Expr_merge (x, les) ->
+ List.fold_left (fun s (_, e) -> occur_expr s e) (add x s) les
+ | Expr_appl (_, e, r) ->
+ occur_expr (match r with Some r -> occur_expr s r | None -> s) e
+ | _ -> s
+
+let occur s eq =
+ occur_expr s eq.eq_rhs
+
+let live: (ident, ISet.t Live.t) Hashtbl.t = Hashtbl.create 32
+
+let of_var_decls =
+ List.fold_left (fun s v -> add v.var_id s) empty
+
+let set_live_of nid outputs locals sorted_eqs =
+ let outputs = of_var_decls outputs in
+ let locals = of_var_decls locals in
+ let vars = union locals outputs in
+ let no_occur_after i =
+ let occ, _ = List.fold_left (fun (s, j) eq ->
+ if j <= i then (s, j + 1) else (occur s eq, j + 1))
+ (empty, 0) sorted_eqs in
+ diff locals occ
+ in
+ let l, _, _ = List.fold_left (fun (l, asg, i) eq ->
+ let asg = inter (assigned asg eq) vars in
+ let noc = no_occur_after i in
+ let liv = diff asg noc in
+ Format.printf "asg %i: %a@." (i+1) pp_iset asg;
+ Format.printf "noc %i: %a@." (i+1) pp_iset noc;
+ Format.printf "liv %i: %a@." (i+1) pp_iset liv;
+ Live.add (i + 1) liv l, asg, i + 1)
+ (Live.add 0 empty Live.empty, empty, 0) sorted_eqs in
+ Format.(printf "@;%a@." (pp_print_list ~pp_open_box:pp_open_vbox0
+ (fun fmt (i, l) -> fprintf fmt "%i : %a" i pp_iset l))
+ (Live.bindings l));
+ Hashtbl.add live nid l
+
+let live_i nid i =
+ Live.find i (Hashtbl.find live nid)
+
+let inter_live_i_with nid i =
+ let li = live_i nid i in
+ List.filter (fun v -> mem v.var_id li)
+
+let existential_vars nid i eq =
+ let li' = live_i nid (i-1) in
+ let li = live_i nid i in
+ let d = diff (union li' (assigned empty eq)) li in
+ List.filter (fun v -> mem v.var_id d)
diff --git a/src/machine_code.ml b/src/machine_code.ml
index abc36a7e..b840e6b7 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -42,11 +42,10 @@ type machine_env = {
}
-let build_env locals non_locals =
- let all = VSet.union locals non_locals in
- {
- is_local = (fun id -> VSet.exists (fun v -> v.var_id = id) locals);
- get_var = (fun id -> try VSet.get id all with Not_found ->
+let build_env inputs locals outputs =
+ let all = List.sort_uniq VDeclModule.compare (locals @ inputs @ outputs) in
+ { is_local = (fun id -> List.exists (fun v -> v.var_id = id) locals);
+ get_var = (fun id -> try List.find (fun v -> v.var_id = id) all with Not_found ->
(* Format.eprintf "Impossible to find variable %s in set %a@.@?"
* id
* VSet.pp all; *)
@@ -64,7 +63,7 @@ let translate_ident env id =
(* id is a var that shall be visible here , ie. in vars *)
try
let var_id = env.get_var id in
- mk_val (Var var_id) var_id.var_type
+ vdecl_to_val var_id
with Not_found ->
(* id is a constant *)
@@ -72,13 +71,12 @@ let translate_ident env id =
let vdecl = (Corelang.var_decl_of_const
(const_of_top (Hashtbl.find Corelang.consts_table id)))
in
- mk_val (Var vdecl) vdecl.var_type
+ vdecl_to_val vdecl
with Not_found ->
(* id is a tag, getting its type in the list of declared enums *)
try
- let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in
- mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)
+ id_to_tag id
with Not_found ->
Format.eprintf "internal error: Machine_code.translate_ident %s@.@?" id;
assert false
@@ -147,28 +145,40 @@ let translate_guard env expr =
let rec translate_act env (y, expr) =
let translate_act = translate_act env in
let translate_guard = translate_guard env in
- let translate_ident = translate_ident env in
+ (* let translate_ident = translate_ident env in *)
let translate_expr = translate_expr env in
let lustre_eq = Corelang.mkeq Location.dummy_loc ([y.var_id], expr) in
match expr.expr_desc with
| Expr_ite (c, t, e) ->
- mk_conditional ~lustre_eq
- (translate_guard c)
- [translate_act (y, t)]
- [translate_act (y, e)]
+ let c = translate_guard c in
+ let t, spec_t = translate_act (y, t) in
+ let e, spec_e = translate_act (y, e) in
+ mk_conditional ~lustre_eq c [t] [e],
+ mk_conditional_tr c spec_t spec_e
| Expr_merge (x, hl) ->
- mk_branch ~lustre_eq
- (translate_ident x)
- (List.map (fun (t, h) -> t, [translate_act (y, h)]) hl)
+ let var_x = env.get_var x in
+ let hl, spec_hl = List.(split (map (fun (t, h) ->
+ let h, spec_h = translate_act (y, h) in
+ (t, [h]), (t, spec_h))
+ hl)) in
+ mk_branch ~lustre_eq var_x hl,
+ mk_branch_tr var_x spec_hl
| _ ->
- mk_assign ~lustre_eq y (translate_expr expr)
+ let e = translate_expr expr in
+ mk_assign ~lustre_eq y e,
+ mk_assign_tr y e
+
+let get_memory env mems eq = match eq.eq_lhs, eq.eq_rhs.expr_desc with
+ | ([x], Expr_pre _ | [x], Expr_fby _) when env.is_local x ->
+ let var_x = env.get_var x in
+ VSet.add var_x mems
+ | _ -> mems
+
+let get_memories env =
+ List.fold_left (get_memory env) VSet.empty
(* Datastructure updated while visiting equations *)
type machine_ctx = {
- (* machine name *)
- id: ident;
- (* Memories *)
- m: VSet.t;
(* Reset instructions *)
si: instr_t list;
(* Instances *)
@@ -177,25 +187,18 @@ type machine_ctx = {
s: instr_t list;
(* Memory pack spec *)
mp: mc_formula_t list;
- (* Clocked spec *)
- c: mc_formula_t IMap.t;
(* Transition spec *)
- t: mc_formula_t list;
+ t: (var_decl list * var_decl list * var_decl list * mc_formula_t) list;
}
-let ctx_init id = {
- id;
- m = VSet.empty;
+let ctx_init = {
si = [];
j = IMap.empty;
s = [];
mp = [];
- c = IMap.empty;
t = []
}
-let ctx_dummy = ctx_init ""
-
(****************************************************************)
(* Main function to translate equations into this machine context we
are building *)
@@ -203,57 +206,74 @@ let ctx_dummy = ctx_init ""
let mk_control v l inst =
mkinstr
- True
- (* (Imply (mk_clocked_on id vs, inst.instr_spec)) *)
- (MBranch (v, [l, [inst]]))
+ (MBranch (vdecl_to_val v, [l, [inst]]))
-let control_on_clock env ctx ck spec inst =
- let rec aux (ck_ids, vs, ctx, spec, inst as acc) ck =
+let control_on_clock env ck inst =
+ let rec aux (fspec, inst as acc) ck =
match (Clocks.repr ck).cdesc with
| Con (ck, cr, l) ->
let id = Clocks.const_of_carrier cr in
- let v = translate_ident env id in
- let ck_ids' = String.concat "_" ck_ids in
- let id' = id ^ "_" ^ ck_ids' in
- let ck_spec = mk_condition v l in
- aux (id :: ck_ids,
- v :: vs,
- { ctx with
- c = IMap.add id ck_spec
- (IMap.add id' (And [ck_spec; mk_clocked_on ck_ids' vs]) ctx.c)
- },
- Imply (mk_clocked_on id' (v :: vs), spec),
- mk_control v l inst) ck
+ let v = env.get_var id in
+ aux ((fun spec -> Imply (Equal (Var v, Tag l), fspec spec)),
+ mk_control v l inst)
+ ck
| _ -> acc
in
- let _, _, ctx, spec, inst = aux ([], [], ctx, spec, inst) ck in
- ctx, spec, inst
+ let fspec, inst = aux ((fun spec -> spec), inst) ck in
+ fspec, inst
let reset_instance env i r c =
match r with
| Some r ->
- let _, _, inst = control_on_clock env ctx_dummy c True
+ let _, inst = control_on_clock env c
(mk_conditional
(translate_guard env r)
- [mkinstr True (MReset i)]
- [mkinstr True (MNoReset i)]) in
+ [mkinstr (MSetReset i)]
+ [mkinstr (MNoReset i)]) in
[ inst ]
| None -> []
-
-let translate_eq env ctx i eq =
+let translate_eq env ctx id inputs locals outputs i eq =
let translate_expr = translate_expr env in
let translate_act = translate_act env in
- let control_on_clock ck spec inst =
- let ctx, _spec, inst = control_on_clock env ctx ck spec inst in
+ let locals_pi = Lustre_live.inter_live_i_with id (i-1) locals in
+ let outputs_pi = Lustre_live.inter_live_i_with id (i-1) outputs in
+ let locals_i = Lustre_live.inter_live_i_with id i locals in
+ let outputs_i = Lustre_live.inter_live_i_with id i outputs in
+ let pred_mp ctx a =
+ And [mk_memory_pack ~i:(i-1) id; a] :: ctx.mp in
+ let pred_t ctx a =
+ (inputs, locals_i, outputs_i,
+ Exists
+ (Lustre_live.existential_vars id i eq (locals @ outputs),
+ And [
+ mk_transition ~i:(i-1) id
+ (vdecls_to_vals inputs)
+ (vdecls_to_vals locals_pi)
+ (vdecls_to_vals outputs_pi);
+ a
+ ]))
+ :: ctx.t in
+ let control_on_clock ck inst spec_mp spec_t =
+ let fspec, inst = control_on_clock env ck inst in
{ ctx with
s = { inst with
- instr_spec = mk_transition ~i ctx.id [] } :: ctx.s }
+ instr_spec = [
+ mk_memory_pack ~i id;
+ mk_transition ~i id
+ (vdecls_to_vals inputs)
+ (vdecls_to_vals locals_i)
+ (vdecls_to_vals outputs_i)
+ ] }
+ :: ctx.s;
+ mp = pred_mp ctx spec_mp;
+ t = pred_t ctx (fspec spec_t);
+ }
in
let reset_instance = reset_instance env in
- let mkinstr' = mkinstr ~lustre_eq:eq True in
- let ctl ?(ck=eq.eq_rhs.expr_clock) spec instr =
- control_on_clock ck spec (mkinstr' instr) in
+ let mkinstr' = mkinstr ~lustre_eq:eq in
+ let ctl ?(ck=eq.eq_rhs.expr_clock) instr spec_mp spec_t =
+ control_on_clock ck (mkinstr' instr) spec_mp spec_t in
(* Format.eprintf "translate_eq %a with clock %a@."
Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *)
@@ -261,33 +281,38 @@ let translate_eq env ctx i eq =
| [x], Expr_arrow (e1, e2) ->
let var_x = env.get_var x in
let td = Arrow.arrow_top_decl () in
- let o = new_instance td eq.eq_rhs.expr_tag in
+ let inst = new_instance td eq.eq_rhs.expr_tag in
let c1 = translate_expr e1 in
let c2 = translate_expr e2 in
+ assert (c1.value_desc = Cst (Const_tag "true"));
+ assert (c2.value_desc = Cst (Const_tag "false"));
let ctx = ctl
- (mk_transition (node_name td) [])
- (MStep ([var_x], o, [c1;c2])) in
+ (MStep ([var_x], inst, [c1; c2]))
+ (mk_memory_pack ~inst (node_name td))
+ (mk_transition ~inst (node_name td) [] [] [vdecl_to_val var_x])
+ in
{ ctx with
- si = mkinstr True (MReset o) :: ctx.si;
- j = IMap.add o (td, []) ctx.j;
+ si = mkinstr (MSetReset inst) :: ctx.si;
+ j = IMap.add inst (td, []) ctx.j;
}
- | [x], Expr_pre e1 when env.is_local x ->
+ | [x], Expr_pre e when env.is_local x ->
let var_x = env.get_var x in
- let ctx = ctl
- True
- (MStateAssign (var_x, translate_expr e1)) in
- { ctx with
- m = VSet.add var_x ctx.m;
- }
+ let e = translate_expr e in
+ ctl
+ (MStateAssign (var_x, e))
+ (mk_state_variable_pack var_x)
+ (mk_state_assign_tr var_x e)
| [x], Expr_fby (e1, e2) when env.is_local x ->
let var_x = env.get_var x in
+ let e2 = translate_expr e2 in
let ctx = ctl
- True
- (MStateAssign (var_x, translate_expr e2)) in
+ (MStateAssign (var_x, e2))
+ (mk_state_variable_pack var_x)
+ (mk_state_assign_tr var_x e2)
+ in
{ ctx with
- m = VSet.add var_x ctx.m;
si = mkinstr' (MStateAssign (var_x, translate_expr e1)) :: ctx.si;
}
@@ -298,31 +323,34 @@ let translate_eq env ctx i eq =
let vl = List.map translate_expr el in
let node_f = node_from_name f in
let call_f = node_f, NodeDep.filter_static_inputs (node_inputs node_f) el in
- let o = new_instance node_f eq.eq_rhs.expr_tag in
+ let inst = new_instance node_f eq.eq_rhs.expr_tag in
let env_cks = List.fold_right (fun arg cks -> arg.expr_clock :: cks)
el [eq.eq_rhs.expr_clock] in
let call_ck = Clock_calculus.compute_root_clock
(Clock_predef.ck_tuple env_cks) in
let ctx = ctl
~ck:call_ck
- True
- (MStep (var_p, o, vl)) in
+ (MStep (var_p, inst, vl))
+ (mk_memory_pack ~inst (node_name node_f))
+ (mk_transition ~inst (node_name node_f) vl [] (vdecls_to_vals var_p))
+ in
(*Clocks.new_var true in
Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc;
Format.eprintf "call %a: %a: %a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple env_cks) Clocks.print_ck call_ck;*)
{ ctx with
si = if Stateless.check_node node_f
- then ctx.si else mkinstr True (MReset o) :: ctx.si;
- j = IMap.add o call_f ctx.j;
+ then ctx.si else mkinstr (MSetReset inst) :: ctx.si;
+ j = IMap.add inst call_f ctx.j;
s = (if Stateless.check_node node_f
then []
- else reset_instance o r call_ck)
- @ ctx.s
+ else reset_instance inst r call_ck)
+ @ ctx.s;
}
| [x], _ ->
let var_x = env.get_var x in
- control_on_clock eq.eq_rhs.expr_clock True (translate_act (var_x, eq.eq_rhs))
+ let instr, spec = translate_act (var_x, eq.eq_rhs) in
+ control_on_clock eq.eq_rhs.expr_clock instr True spec
| _ ->
Format.eprintf "internal error: Machine_code.translate_eq %a@?"
@@ -330,7 +358,7 @@ let translate_eq env ctx i eq =
assert false
let constant_equations locals =
- VSet.fold (fun vdecl eqs ->
+ List.fold_left (fun eqs vdecl ->
if vdecl.var_dec_const
then
{ eq_lhs = [vdecl.var_id];
@@ -338,11 +366,11 @@ let constant_equations locals =
eq_loc = vdecl.var_loc
} :: eqs
else eqs)
- locals []
+ [] locals
-let translate_eqs env ctx eqs =
+let translate_eqs env ctx id inputs locals outputs eqs =
List.fold_right (fun eq (ctx, i) ->
- let ctx = translate_eq env ctx i eq in
+ let ctx = translate_eq env ctx id inputs locals outputs i eq in
ctx, i - 1)
eqs (ctx, List.length eqs)
|> fst
@@ -385,22 +413,60 @@ let process_asserts nd =
in
vars, eql, assertl
-let translate_core nid sorted_eqs locals other_vars =
+let translate_core env nid sorted_eqs inputs locals outputs =
let constant_eqs = constant_equations locals in
- let env = build_env locals other_vars in
-
(* Compute constants' instructions *)
- let ctx0 = translate_eqs env (ctx_init nid) constant_eqs in
- assert (VSet.is_empty ctx0.m);
+ let ctx0 = translate_eqs env ctx_init nid inputs locals outputs constant_eqs in
assert (ctx0.si = []);
assert (IMap.is_empty ctx0.j);
(* Compute ctx for all eqs *)
- let ctx = translate_eqs env (ctx_init nid) sorted_eqs in
+ let ctx = translate_eqs env ctx_init nid inputs locals outputs sorted_eqs in
ctx, ctx0.s
+let zero = mk_val (Cst (Const_int 0)) Type_predef.type_int
+
+let memory_pack_0 nd =
+ {
+ mpname = nd;
+ mpindex = Some 0;
+ mpformula = And [StateVarPack ResetFlag; Equal (Memory ResetFlag, Val zero)]
+ }
+
+let memory_pack_toplevel nd i =
+ {
+ mpname = nd;
+ mpindex = None;
+ mpformula = Ternary (Memory ResetFlag,
+ StateVarPack ResetFlag,
+ mk_memory_pack ~i nd.node_id)
+ }
+
+let transition_0 nd =
+ {
+ tname = nd;
+ tindex = Some 0;
+ tinputs = nd.node_inputs;
+ tlocals = [];
+ toutputs = [];
+ tformula = True;
+ }
+
+let transition_toplevel nd i =
+ {
+ tname = nd;
+ tindex = None;
+ tinputs = nd.node_inputs;
+ tlocals = [];
+ toutputs = nd.node_outputs;
+ tformula = ExistsMem (Predicate (ResetCleared nd.node_id),
+ mk_transition nd.node_id ~i
+ (vdecls_to_vals (nd.node_inputs))
+ []
+ (vdecls_to_vals nd.node_outputs));
+ }
let translate_decl nd sch =
(* Format.eprintf "Translating node %s@." nd.node_id; *)
@@ -413,10 +479,10 @@ let translate_decl nd sch =
let new_locals, assert_instrs, nd_node_asserts = process_asserts nd in
(* Build the env: variables visible in the current scope *)
- let locals_list = nd.node_locals @ new_locals in
- 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
+ let locals = nd.node_locals @ new_locals in
+ (* let locals = VSet.of_list locals_list in *)
+ (* let inout_vars = nd.node_inputs @ nd.node_outputs in *)
+ let env = build_env nd.node_inputs locals nd.node_outputs in
(* Format.eprintf "Node content is %a@." Printers.pp_node nd; *)
@@ -430,20 +496,54 @@ let translate_decl nd sch =
* VSet.pp inout_vars
* ; *)
- let ctx, ctx0_s = translate_core
- nd.node_id (assert_instrs@sorted_eqs) locals inout_vars in
+ let equations = assert_instrs @ sorted_eqs in
+ let mems = get_memories env equations in
+ (* Removing computed memories from locals. We also removed unused variables. *)
+ let locals = List.filter
+ (fun v -> not (VSet.mem v mems) && not (List.mem v.var_id unused)) locals in
+ (* Compute live sets for spec *)
+ Lustre_live.set_live_of nd.node_id nd.node_outputs locals equations;
+
+ (* Translate equations *)
+ let ctx, ctx0_s = translate_core env nd.node_id equations
+ nd.node_inputs locals nd.node_outputs in
(* Format.eprintf "ok4@.@?"; *)
- (* Removing computed memories from locals. We also removed unused variables. *)
- let updated_locals =
- let l = VSet.elements (VSet.diff locals ctx.m) in
- List.fold_left (fun res v -> if List.mem v.var_id unused then res else v::res) [] l
- in
+ (* Build the machine *)
let mmap = IMap.bindings ctx.j in
+ let mmemory_packs =
+ memory_pack_0 nd
+ :: List.mapi (fun i f ->
+ {
+ mpname = nd;
+ mpindex = Some (i + 1);
+ mpformula = red f
+ }) ctx.mp
+ @ [memory_pack_toplevel nd (List.length ctx.mp)]
+ in
+ let mtransitions =
+ transition_0 nd
+ :: List.mapi (fun i (tinputs, tlocals, toutputs, f) ->
+ {
+ tname = nd;
+ tindex = Some (i + 1);
+ tinputs;
+ tlocals;
+ toutputs;
+ tformula = red f;
+ }) ctx.t
+ @ [transition_toplevel nd (List.length ctx.t)]
+ in
+ let clear_reset = mkinstr ~instr_spec:[
+ mk_memory_pack ~i:0 nd.node_id;
+ mk_transition ~i:0 nd.node_id
+ (vdecls_to_vals nd.node_inputs)
+ []
+ []] MClearReset in
{
mname = nd;
- mmemory = VSet.elements ctx.m;
+ mmemory = VSet.elements mems;
mcalls = mmap;
minstances = List.filter (fun (_, (n,_)) -> not (Stateless.check_node n)) mmap;
minit = ctx.si;
@@ -452,20 +552,19 @@ let translate_decl nd sch =
mstep = {
step_inputs = nd.node_inputs;
step_outputs = nd.node_outputs;
- step_locals = updated_locals;
+ step_locals = locals;
step_checks = List.map (fun d -> d.Dimension.dim_loc,
translate_expr env
(expr_of_dimension d))
nd.node_checks;
- step_instrs = (
- (* special treatment depending on the active backend. For horn backend,
- common branches are not merged while they are in C or Java
- backends. *)
- if !Backends.join_guards then
- join_guards_list ctx.s
- else
- ctx.s
- );
+ step_instrs = clear_reset ::
+ (* special treatment depending on the active backend. For horn backend,
+ common branches are not merged while they are in C or Java
+ backends. *)
+ (if !Backends.join_guards then
+ join_guards_list ctx.s
+ else
+ ctx.s);
step_asserts = List.map (translate_expr env) nd_node_asserts;
};
@@ -474,7 +573,7 @@ let translate_decl nd sch =
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 = [] };
+ mspec = { mnode_spec = nd.node_spec; mtransitions; mmemory_packs };
mannot = nd.node_annot;
msch = Some sch;
}
diff --git a/src/machine_code_common.ml b/src/machine_code_common.ml
index 35512053..47fa5d8c 100644
--- a/src/machine_code_common.ml
+++ b/src/machine_code_common.ml
@@ -1,7 +1,6 @@
open Lustre_types
open Machine_code_types
open Spec_types
-open Spec_common
open Corelang
open Utils.Format
@@ -10,63 +9,142 @@ let print_statelocaltag = true
let is_memory m id =
(List.exists (fun o -> o.var_id = id.var_id) m.mmemory)
+let is_reset_flag id =
+ id.var_id = "_reset"
+
+let pp_vdecl fmt v =
+ pp_print_string fmt v.var_id
+
let rec pp_val m fmt v =
let pp_val = pp_val m in
match v.value_desc with
| Cst c -> Printers.pp_const fmt c
| Var v ->
- if is_memory m v then
- if print_statelocaltag then
- fprintf fmt "{%s}" v.var_id
- else
- pp_print_string fmt v.var_id
- else
- if print_statelocaltag then
- fprintf fmt "%s" v.var_id
- else
- pp_print_string fmt v.var_id
- | Array vl -> fprintf fmt "[%a]" (Utils.fprintf_list ~sep:", " pp_val) vl
+ if is_memory m v then
+ if print_statelocaltag then
+ fprintf fmt "{%s}" v.var_id
+ else
+ pp_print_string fmt v.var_id
+ else
+ if print_statelocaltag then
+ fprintf fmt "%s" v.var_id
+ else
+ pp_vdecl fmt v
+ | Array vl -> pp_print_bracketed pp_val fmt vl
| Access (t, i) -> fprintf fmt "%a[%a]" pp_val t pp_val i
| Power (v, n) -> fprintf fmt "(%a^%a)" pp_val v pp_val n
- | Fun (n, vl) -> fprintf fmt "%s (%a)" n (Utils.fprintf_list ~sep:", " pp_val) vl
-
-module PrintSpec = PrintSpec(struct
- type t = value_t
- type ctx = machine_t
- let pp_val = pp_val
- end)
-
-let rec pp_instr m fmt i =
- let pp_val = pp_val m and
- pp_branch = pp_branch m in
- let _ =
- match i.instr_desc with
+ | Fun (n, vl) -> fprintf fmt "%s%a" n (pp_print_parenthesized pp_val) vl
+
+module PrintSpec = struct
+
+ let pp_reg fmt = function
+ | ResetFlag -> pp_print_string fmt "{RESET}"
+ | StateVar v -> fprintf fmt "{OUT:%a}" pp_vdecl v
+
+ let pp_expr: type a. machine_t -> formatter -> (value_t, a) expression_t -> unit =
+ fun m fmt -> function
+ | Val v -> pp_val m fmt v
+ | Tag t -> pp_print_string fmt t
+ | Var v -> pp_vdecl fmt v
+ | Memory r -> pp_reg fmt r
+
+ let pp_predicate m fmt p =
+ let pp_expr: type a. formatter -> (value_t, a) expression_t -> unit =
+ fun fmt e -> pp_expr m fmt e
+ in
+ match p with
+ | Transition (f, inst, i, inputs, locals, outputs) ->
+ fprintf fmt "Transition_%a<%a>%a%a"
+ pp_print_string f
+ (pp_print_option ~none:(fun fmt () -> pp_print_string fmt "SELF")
+ pp_print_string) inst
+ (pp_print_option pp_print_int) i
+ (pp_print_parenthesized pp_expr) (inputs @ locals @ outputs)
+ | MemoryPack (f, inst, i) ->
+ fprintf fmt "MemoryPack_%a<%a>%a"
+ pp_print_string f
+ (pp_print_option ~none:(fun fmt () -> pp_print_string fmt "SELF")
+ pp_print_string) inst
+ (pp_print_option pp_print_int) i
+ | ResetCleared f ->
+ fprintf fmt "ResetCleared_%a" pp_print_string f
+ | Initialization -> ()
+
+ let pp_spec m =
+ let pp_expr: type a. formatter -> (value_t, a) expression_t -> unit =
+ fun fmt e -> pp_expr m fmt e
+ in
+ let rec pp_spec fmt f =
+ match f with
+ | True -> pp_print_string fmt "true"
+ | False -> pp_print_string fmt "false"
+ | Equal (a, b) ->
+ fprintf fmt "%a == %a" pp_expr a pp_expr b
+ | And fs ->
+ pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@ ∧ ")
+ (fun fmt spec -> fprintf fmt "@[%a@]" pp_spec spec) fmt fs
+ | Or fs ->
+ pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@ ∨ ")
+ (fun fmt spec -> fprintf fmt "@[%a@]" pp_spec spec) fmt fs
+ | Imply (a, b) ->
+ fprintf fmt "%a@ -> %a" pp_spec a pp_spec b
+ | Exists (xs, a) ->
+ fprintf fmt "@[<hv 2>∃ @[<h>%a,@]@ %a@]"
+ (pp_comma_list Printers.pp_var) xs pp_spec a
+ | Forall (xs, a) ->
+ fprintf fmt "@[<hv 2>∀ @[<h>%a,@]@ %a@]"
+ (pp_comma_list Printers.pp_var) xs pp_spec a
+ | Ternary (e, a, b) ->
+ fprintf fmt "If %a Then (@[<hov>%a@]) Else (@[<hov>%a@])"
+ pp_expr e pp_spec a pp_spec b
+ | Predicate p ->
+ pp_predicate m fmt p
+ | StateVarPack r ->
+ fprintf fmt "StateVarPack<%a>" pp_reg r
+ | ExistsMem (rc, tr) ->
+ fprintf fmt "@[<hv 2>∃ MEM,@ %a@]" pp_spec (And [rc; tr])
+ in
+ pp_spec
+
+end
+
+let pp_spec m =
+ pp_print_list
+ ~pp_open_box:pp_open_vbox0
+ ~pp_prologue:pp_print_cut
+ (fun fmt -> fprintf fmt "@[<h>--%@ %a@]" (PrintSpec.pp_spec m))
+
+let rec pp_instr m fmt i =
+ let pp_val = pp_val m in
+ let pp_branch = pp_branch m in
+ begin match i.instr_desc with
| MLocalAssign (i,v) -> fprintf fmt "%s := %a" i.var_id pp_val v
| MStateAssign (i,v) -> fprintf fmt "{%s} := %a" i.var_id pp_val v
- | MReset i -> fprintf fmt "reset %s" i
+ | MSetReset i -> fprintf fmt "set_reset %s" i
+ | MClearReset -> fprintf fmt "clear_reset %s" m.mname.node_id
| MNoReset i -> fprintf fmt "noreset %s" i
| MStep (il, i, vl) ->
- fprintf fmt "%a = %s (%a)"
- (Utils.fprintf_list ~sep:", " (fun fmt v -> pp_print_string fmt v.var_id)) il
- i
- (Utils.fprintf_list ~sep:", " pp_val) vl
+ fprintf fmt "%a := %s%a"
+ (pp_comma_list pp_vdecl) il
+ i
+ (pp_print_parenthesized pp_val) vl
| MBranch (g,hl) ->
- fprintf fmt "@[<v 2>case(%a) {@,%a@,}@]"
- pp_val g
- (Utils.fprintf_list ~sep:"@," pp_branch) hl
+ fprintf fmt "@[<v 2>case(%a) {@,%a@]@,}"
+ pp_val g
+ (pp_print_list ~pp_open_box:pp_open_vbox0 pp_branch) hl
| MComment s -> pp_print_string fmt s
| MSpec s -> pp_print_string fmt ("@" ^ s)
-
- in
+
+ end;
(* Annotation *)
(* let _ = *)
(* match i.lustre_expr with None -> () | Some e -> fprintf fmt " -- original expr: %a" Printers.pp_expr e *)
(* in *)
begin match i.lustre_eq with
| None -> ()
- | Some eq -> fprintf fmt " -- original eq: %a" Printers.pp_node_eq eq
+ | Some eq -> fprintf fmt " @[<h>-- original eq: %a@]" Printers.pp_node_eq eq
end;
- fprintf fmt "@ --%@ %a" (PrintSpec.pp_spec m) i.instr_spec
+ pp_spec m fmt i.instr_spec
and pp_branch m fmt (t, h) =
@@ -95,21 +173,56 @@ let get_node_def id m =
let machine_vars m = m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ m.mmemory
let pp_step m fmt s =
- let pp_list = pp_print_list ~pp_sep:pp_print_comma in
- fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ asserts : @[%a@]@]@ "
- (pp_list Printers.pp_var) s.step_inputs
- (pp_list Printers.pp_var) s.step_outputs
- (pp_list Printers.pp_var) s.step_locals
- (pp_list (fun fmt (_, c) -> pp_val m fmt c))
+ fprintf fmt
+ "@[<v>\
+ inputs : %a@ \
+ outputs: %a@ \
+ locals : %a@ \
+ checks : %a@ \
+ instrs : @[%a@]@ \
+ asserts : @[%a@]@]@ "
+ (pp_comma_list Printers.pp_var) s.step_inputs
+ (pp_comma_list Printers.pp_var) s.step_outputs
+ (pp_comma_list Printers.pp_var) s.step_locals
+ (pp_comma_list (fun fmt (_, c) -> pp_val m fmt c))
s.step_checks
(pp_instrs m) s.step_instrs
- (pp_list (pp_val m)) s.step_asserts
-
+ (pp_comma_list (pp_val m)) s.step_asserts
let pp_static_call fmt (node, args) =
- fprintf fmt "%s<%a>"
- (node_name node)
- (Utils.fprintf_list ~sep:", " Dimension.pp_dimension) args
+ fprintf fmt "%s<%a>"
+ (node_name node)
+ (pp_comma_list Dimension.pp_dimension) args
+
+let pp_instance fmt (o1, o2) =
+ fprintf fmt "(%s, %a)"
+ o1
+ pp_static_call o2
+
+let pp_memory_pack m fmt mp =
+ fprintf fmt
+ "@[<v 2>MemoryPack_%a<SELF>%a =@ %a@]"
+ pp_print_string mp.mpname.node_id
+ (pp_print_option pp_print_int) mp.mpindex
+ (PrintSpec.pp_spec m) mp.mpformula
+
+let pp_memory_packs m fmt =
+ fprintf fmt
+ "@[<v 2>memory_packs:@ %a@]"
+ (pp_print_list (pp_memory_pack m))
+
+let pp_transition m fmt t =
+ fprintf fmt
+ "@[<v 2>Transition_%a<SELF>%a%a =@ %a@]"
+ pp_print_string t.tname.node_id
+ (pp_print_option pp_print_int) t.tindex
+ (pp_print_parenthesized pp_vdecl) (t.tinputs @ t.tlocals @ t.toutputs)
+ (PrintSpec.pp_spec m) t.tformula
+
+let pp_transitions m fmt =
+ fprintf fmt
+ "@[<v 2>transitions:@ %a@]"
+ (pp_print_list (pp_transition m))
let pp_machine fmt m =
fprintf fmt
@@ -120,24 +233,25 @@ let pp_machine fmt m =
const : %a@ \
step :@ \
@[<v 2>%a@]@ \
- spec : @[%t@]@ \
+ spec : @[<v>%t@ %a@ @ %a@]@ \
annot : @[%a@]@]@ "
m.mname.node_id
- (Utils.fprintf_list ~sep:", " Printers.pp_var) m.mmemory
- (Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) -> fprintf fmt "(%s, %a)" o1 pp_static_call o2)) m.minstances
- (Utils.fprintf_list ~sep:"@ " (pp_instr m)) m.minit
- (Utils.fprintf_list ~sep:"@ " (pp_instr m)) m.mconst
+ (pp_comma_list Printers.pp_var) m.mmemory
+ (pp_comma_list pp_instance) m.minstances
+ (pp_instrs m) m.minit
+ (pp_instrs m) m.mconst
(pp_step m) m.mstep
(fun fmt -> match m.mspec.mnode_spec with
| None -> ()
| Some (NodeSpec id) -> fprintf fmt "cocospec: %s" id
| Some (Contract spec) -> Printers.pp_spec fmt spec)
- (Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot
+ (pp_memory_packs m) m.mspec.mmemory_packs
+ (pp_transitions m) m.mspec.mtransitions
+ (pp_print_list Printers.pp_expr_annot) m.mannot
-let pp_machines fmt ml =
- fprintf fmt "@[<v 0>%a@]" (Utils.fprintf_list ~sep:"@," pp_machine) ml
+let pp_machines =
+ pp_print_list ~pp_open_box:pp_open_vbox0 pp_machine
-
let rec is_const_value v =
match v.value_desc with
| Cst _ -> true
@@ -169,12 +283,26 @@ let is_output m id =
let get_instr_spec i = i.instr_spec
+let mk_val v t =
+ { value_desc = v;
+ value_type = t;
+ value_annot = None }
+
+let vdecl_to_val vd =
+ mk_val (Var vd) vd.var_type
+
+let vdecls_to_vals =
+ List.map vdecl_to_val
+
+let id_to_tag id =
+ let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in
+ mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)
+
let mk_conditional ?lustre_eq c t e =
mkinstr ?lustre_eq
(* (Ternary (Val c,
* And (List.map get_instr_spec t),
* And (List.map get_instr_spec e))) *)
- True
(MBranch(c, [
(tag_true, t);
(tag_false, e) ]))
@@ -184,20 +312,13 @@ let mk_branch ?lustre_eq c br =
(* (And (List.map (fun (l, instrs) ->
* Imply (Equal (Val c, Tag l), And (List.map get_instr_spec instrs)))
* br)) *)
- True
- (MBranch (c, br))
+ (MBranch (vdecl_to_val c, br))
let mk_assign ?lustre_eq x v =
mkinstr ?lustre_eq
(* (Equal (Var x, Val v)) *)
- True
(MLocalAssign (x, v))
-let mk_val v t =
- { value_desc = v;
- value_type = t;
- value_annot = None }
-
let arrow_machine =
let state = "_first" in
let var_state = dummy_var_decl state Type_predef.type_bool(* (Types.new_ty Types.Tbool) *) in
@@ -212,7 +333,7 @@ let arrow_machine =
mmemory = [var_state];
mcalls = [];
minstances = [];
- minit = [mkinstr True (MStateAssign(var_state, cst true))];
+ minit = [mkinstr (MStateAssign(var_state, cst true))];
mstatic = [];
mconst = [];
mstep = {
@@ -221,14 +342,14 @@ let arrow_machine =
step_locals = [];
step_checks = [];
step_instrs = [mk_conditional (mk_val (Var var_state) Type_predef.type_bool)
- (List.map (mkinstr True)
- [MStateAssign(var_state, cst false);
- MLocalAssign(var_output, mk_val (Var var_input1) t_arg)])
- (List.map (mkinstr True)
- [MLocalAssign(var_output, mk_val (Var var_input2) t_arg)]) ];
+ (List.map mkinstr
+ [MStateAssign(var_state, cst false);
+ MLocalAssign(var_output, mk_val (Var var_input1) t_arg)])
+ (List.map mkinstr
+ [MLocalAssign(var_output, mk_val (Var var_input2) t_arg)]) ];
step_asserts = [];
};
- mspec = { mnode_spec = None; mtransitions = [] };
+ mspec = { mnode_spec = None; mtransitions = []; mmemory_packs = [] };
mannot = [];
msch = None
}
@@ -269,7 +390,7 @@ let empty_machine =
step_instrs = [];
step_asserts = [];
};
- mspec = { mnode_spec = None; mtransitions = [] };
+ mspec = { mnode_spec = None; mtransitions = []; mmemory_packs = [] };
mannot = [];
msch = None
}
@@ -374,7 +495,7 @@ let rec dimension_of_value value =
| _ -> assert false
- let rec join_branches hl1 hl2 =
+let rec join_branches hl1 hl2 =
match hl1, hl2 with
| [] , _ -> hl2
| _ , [] -> hl1
@@ -384,15 +505,16 @@ let rec dimension_of_value value =
else (t1, List.fold_right join_guards h1 h2) :: join_branches q1 q2
and join_guards inst1 insts2 =
- match get_instr_desc inst1, List.map get_instr_desc insts2 with
- | _ , [] ->
- [inst1]
- | MBranch (x1, hl1), MBranch (x2, hl2) :: _ when x1 = x2 ->
- mkinstr True
- (* TODO on pourrait uniquement concatener les lustres de inst1 et hd(inst2) *)
- (MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2)))
- :: (List.tl insts2)
- | _ -> inst1 :: insts2
+ match get_instr_desc inst1, insts2 with
+ | MBranch (x1, hl1),
+ ({ instr_desc = MBranch (x2, hl2); _ } as inst2) :: insts2
+ when x1 = x2 ->
+ mkinstr
+ ~instr_spec:(get_instr_spec inst1 @ get_instr_spec inst2)
+ (* TODO on pourrait uniquement concatener les lustres de inst1 et hd(inst2) *)
+ (MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2)))
+ :: insts2
+ | _ -> inst1 :: insts2
let join_guards_list insts =
List.fold_right join_guards insts []
diff --git a/src/machine_code_common.mli b/src/machine_code_common.mli
index 341d81c4..0655bc63 100644
--- a/src/machine_code_common.mli
+++ b/src/machine_code_common.mli
@@ -1,5 +1,6 @@
val pp_val: Machine_code_types.machine_t -> Format.formatter -> Machine_code_types.value_t -> unit
val is_memory: Machine_code_types.machine_t -> Lustre_types.var_decl -> bool
+val is_reset_flag: Lustre_types.var_decl -> bool
val is_output: Machine_code_types.machine_t -> Lustre_types.var_decl -> bool
val is_const_value: Machine_code_types.value_t -> bool
val get_const_assign: Machine_code_types.machine_t -> Lustre_types.var_decl -> Machine_code_types.value_t
@@ -7,8 +8,11 @@ val get_stateless_status: Machine_code_types.machine_t -> bool * bool
val get_stateless_status_top_decl: Lustre_types.top_decl -> bool * bool
val is_stateless: Machine_code_types.machine_t -> bool
val mk_val: Machine_code_types.value_t_desc -> Types.type_expr -> Machine_code_types.value_t
+val vdecl_to_val: Lustre_types.var_decl -> Machine_code_types.value_t
+val vdecls_to_vals: Lustre_types.var_decl list -> Machine_code_types.value_t list
+val id_to_tag: Lustre_types.ident -> Machine_code_types.value_t
val mk_conditional: ?lustre_eq:Lustre_types.eq -> Machine_code_types.value_t -> Machine_code_types.instr_t list -> Machine_code_types.instr_t list -> Machine_code_types.instr_t
-val mk_branch: ?lustre_eq:Lustre_types.eq -> Machine_code_types.value_t -> (Lustre_types.label * Machine_code_types.instr_t list) list -> Machine_code_types.instr_t
+val mk_branch: ?lustre_eq:Lustre_types.eq -> Lustre_types.var_decl -> (Lustre_types.label * Machine_code_types.instr_t list) list -> Machine_code_types.instr_t
val mk_assign: ?lustre_eq:Lustre_types.eq -> Lustre_types.var_decl -> Machine_code_types.value_t -> Machine_code_types.instr_t
val empty_machine: Machine_code_types.machine_t
val arrow_machine: Machine_code_types.machine_t
@@ -26,3 +30,5 @@ val get_machine: Machine_code_types.machine_t list -> string -> Machine_code_typ
val get_node_def: string -> Machine_code_types.machine_t -> Lustre_types.node_desc
val join_guards_list: Machine_code_types.instr_t list -> Machine_code_types.instr_t list
val machine_vars: Machine_code_types.machine_t -> Lustre_types.var_decl list
+
+module PrintSpec: sig val pp_spec: Machine_code_types.machine_t -> Format.formatter -> Machine_code_types.value_t Spec_types.formula_t -> unit end
diff --git a/src/machine_code_types.ml b/src/machine_code_types.ml
index 9403b67b..7cdfc1fe 100644
--- a/src/machine_code_types.ml
+++ b/src/machine_code_types.ml
@@ -23,12 +23,13 @@ type instr_t =
instr_desc: instr_t_desc; (* main data: the content *)
(* lustre_expr: expr option; (* possible representation as a lustre expression *) *)
lustre_eq: eq option; (* possible representation as a lustre flow equation *)
- instr_spec: mc_formula_t
+ instr_spec: mc_formula_t list
}
and instr_t_desc =
| MLocalAssign of var_decl * value_t
| MStateAssign of var_decl * value_t
- | MReset of ident
+ | MClearReset
+ | MSetReset of ident
| MNoReset of ident
| MStep of var_decl list * ident * value_t list
| MBranch of value_t * (label * instr_t list) list
@@ -47,10 +48,12 @@ type step_t = {
type static_call = top_decl * (Dimension.dim_expr list)
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;
- mtransitions: mc_transition_t list
+ mtransitions: mc_transition_t list;
+ mmemory_packs: mc_memory_pack_t list
}
type machine_t = {
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index ab06ccdf..b79835ab 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -28,11 +28,13 @@ 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
- | 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 _ -> instr
- | MNoReset _ -> instr
+ | MSetReset _
+ | MNoReset _
+ | MClearReset
+ | MSpec _
+ | MComment _ -> instr
| MStep (il, i, vl) -> update_instr_desc instr (MStep(il, i, List.map e_expr vl))
| MBranch (g,hl) ->
update_instr_desc instr (
@@ -115,14 +117,16 @@ let rec simplify_instr_offset m instr =
match get_instr_desc instr with
| MLocalAssign (v, expr) -> update_instr_desc instr (MLocalAssign (v, simplify_expr_offset m expr))
| MStateAssign (v, expr) -> update_instr_desc instr (MStateAssign (v, simplify_expr_offset m expr))
- | MReset _ -> instr
- | MNoReset _ -> instr
+ | MSetReset _
+ | MNoReset _
+ | MClearReset
+ | MSpec _
+ | MComment _ -> instr
| MStep (outputs, id, inputs) -> update_instr_desc instr (MStep (outputs, id, List.map (simplify_expr_offset m) inputs))
| MBranch (cond, brl)
-> update_instr_desc instr (
MBranch(simplify_expr_offset m cond, List.map (fun (l, il) -> l, simplify_instrs_offset m il) brl)
)
- | MSpec _ | MComment _ -> instr
and simplify_instrs_offset m instrs =
List.map (simplify_instr_offset m) instrs
@@ -284,7 +288,6 @@ let instr_of_const top_const =
let lustre_eq = mkeq loc ([const.const_id], mkexpr loc (Expr_const const.const_value)) in
mkinstr
~lustre_eq
- True
(MLocalAssign (vdecl, mk_val (Cst const.const_value) vdecl.var_type))
(* We do not perform this optimization on contract nodes since there
@@ -499,11 +502,13 @@ let rec value_replace_var fvar value =
let rec instr_replace_var fvar instr cont =
match get_instr_desc instr with
- | 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 _ -> instr_cons instr cont
- | MNoReset _ -> instr_cons instr cont
+ | MSetReset _
+ | MNoReset _
+ | MClearReset
+ | MSpec _
+ | MComment _ -> instr_cons instr cont
| MStep (il, i, vl) -> instr_cons (update_instr_desc instr (MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl))) cont
| MBranch (g, hl) -> instr_cons (update_instr_desc instr (MBranch (value_replace_var fvar g, List.map (fun (h, il) -> (h, instrs_replace_var fvar il [])) hl))) cont
@@ -763,7 +768,7 @@ let optimize params prog node_schs machine_code =
in
- prog, List.rev machine_code
+ prog, machine_code
(* Local Variables: *)
diff --git a/src/plugins/scopes/scopes.ml b/src/plugins/scopes/scopes.ml
index 0772b160..45e4e358 100644
--- a/src/plugins/scopes/scopes.ml
+++ b/src/plugins/scopes/scopes.ml
@@ -220,7 +220,7 @@ let pp_scopes fmt scopes =
let update_machine main_node machine scopes =
let stateassign (vdecl_mem, vdecl_orig) =
- mkinstr True
+ mkinstr
(MStateAssign (vdecl_mem, mk_val (Var vdecl_orig) vdecl_orig.var_type))
in
let selection =
@@ -248,7 +248,7 @@ let update_machine main_node machine scopes =
mstep = {
machine.mstep with
step_instrs = machine.mstep.step_instrs
- @ (mkinstr True (MComment "Registering all flows"))::(List.map stateassign new_mems)
+ @ (mkinstr (MComment "Registering all flows"))::(List.map stateassign new_mems)
}
}
diff --git a/src/spec_common.ml b/src/spec_common.ml
index 3eb96c70..44cd7f9b 100644
--- a/src/spec_common.ml
+++ b/src/spec_common.ml
@@ -10,8 +10,15 @@ let is_false = function
| False -> true
| _ -> false
-let rec red = function
- | Equal (a, b) when a = b ->
+let expr_eq: type a b. (a, left_v) expression_t -> (a, b) expression_t -> bool =
+ fun a b ->
+ match a, b with
+ | Var x, Var y -> x = y
+ | Memory r1, Memory r2 -> r1 = r2
+ | _ -> false
+
+let rec red: type a. a formula_t -> a formula_t = function
+ | Equal (a, b) when expr_eq a b ->
True
| And l ->
@@ -45,11 +52,17 @@ let rec red = function
| Exists (x, p) ->
let p' = red p in
- if is_true p' then True else Exists (x, p')
+ if is_true p' then True else begin match x with
+ | [] -> p'
+ | x -> Exists (x, p')
+ end
| Forall (x, p) ->
let p' = red p in
- if is_true p' then True else Forall (x, p')
+ if is_true p' then True else begin match x with
+ | [] -> p'
+ | x -> Forall (x, p')
+ end
| Ternary (x, a, b) ->
let a' = red a in
@@ -59,74 +72,38 @@ let rec red = function
| f -> f
(* smart constructors *)
-let mk_condition x l =
- if l = tag_true then Ternary (Val x, True, False)
- else if l = tag_false then Ternary (Val x, False, True)
- else Equal (Val x, Tag l)
+(* let mk_condition x l =
+ * if l = tag_true then Ternary (Val x, True, False)
+ * else if l = tag_false then Ternary (Val x, False, True)
+ * else Equal (Val x, Tag l) *)
let vals vs = List.map (fun v -> Val v) vs
-let mk_pred_call pred vars =
- Predicate (pred, vals vars)
-
-let mk_clocked_on id =
- mk_pred_call (Clocked_on id)
-
-let mk_transition ?i id =
- mk_pred_call (Transition (id, i))
-
-module type SPECVALUE = sig
- type t
- type ctx
- val pp_val: ctx -> Format.formatter -> t -> unit
-end
-
-module PrintSpec(SV: SPECVALUE) = struct
-
- open Utils.Format
-
- let pp_state fmt = function
- | In -> pp_print_string fmt "IN"
- | Out -> pp_print_string fmt "OUT"
-
- let pp_expr ctx fmt = function
- | Val v -> SV.pp_val ctx fmt v
- | Tag t -> pp_print_string fmt t
- | Var v -> pp_print_string fmt v.var_id
- | Instance (s, i) -> fprintf fmt "%a:%a" pp_state s pp_print_string i
- | Memory (s, i) -> fprintf fmt "%a:%a" pp_state s pp_print_string i
-
- let pp_predicate fmt = function
- | Clocked_on x -> fprintf fmt "On<%a>" pp_print_string x
- | Transition (f, i) ->
- fprintf fmt "Transition<%a>%a"
- pp_print_string f
- (pp_print_option pp_print_int) i
- | Initialization -> ()
-
- let pp_spec ctx =
- let pp_expr = pp_expr ctx in
- let rec pp_spec fmt f =
- match f with
- | True -> pp_print_string fmt "true"
- | False -> pp_print_string fmt "false"
- | Equal (a, b) ->
- fprintf fmt "%a == %a" pp_expr a pp_expr b
- | And fs ->
- pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt "/\\") pp_spec fmt fs
- | Or fs ->
- pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt "\\/") pp_spec fmt fs
- | Imply (a, b) ->
- fprintf fmt "%a -> %a" pp_spec a pp_spec b
- | Exists (xs, a) ->
- fprintf fmt "∃%a, %a" (pp_print_list Printers.pp_var) xs pp_spec a
- | Forall (xs, a) ->
- fprintf fmt "∀%a, %a" (pp_print_list Printers.pp_var) xs pp_spec a
- | Ternary (e, a, b) ->
- fprintf fmt "If %a Then %a Else %a" pp_expr e pp_spec a pp_spec b
- | Predicate (p, es) ->
- fprintf fmt "%a%a" pp_predicate p (pp_print_parenthesized pp_expr) es
- in
- pp_spec
-
-end
+let mk_pred_call pred =
+ Predicate pred
+
+(* let mk_clocked_on id =
+ * mk_pred_call (Clocked_on id) *)
+
+let mk_transition ?i ?inst id inputs locals outputs =
+ mk_pred_call
+ (Transition (id, inst, i, vals inputs, vals locals, vals outputs))
+
+let mk_memory_pack ?i ?inst id =
+ mk_pred_call (MemoryPack (id, inst, i))
+
+let mk_state_variable_pack x =
+ StateVarPack (StateVar x)
+
+let mk_state_assign_tr x v =
+ Equal (Memory (StateVar x), Val v)
+
+let mk_conditional_tr v t f =
+ Ternary (Val v, t, f)
+
+let mk_branch_tr x hl =
+ And (List.map (fun (t, spec) -> Imply (Equal (Var x, Tag t), spec)) hl)
+
+let mk_assign_tr x v =
+ Equal (Var x, Val v)
+
diff --git a/src/spec_types.ml b/src/spec_types.ml
index a96d0a44..32391548 100644
--- a/src/spec_types.ml
+++ b/src/spec_types.ml
@@ -1,33 +1,49 @@
open Lustre_types
-type state_t =
- | In
- | Out
-
-type 'a expression_t =
- | Val of 'a
- | Tag of ident
- | Var of var_decl
- | Instance of state_t * ident
- | Memory of state_t * ident
-
-type predicate_t =
- (* | Memory_pack *)
- | Clocked_on of ident
- | Transition of ident * int option
+type register_t =
+ | ResetFlag
+ | StateVar of var_decl
+
+type left_v
+type right_v
+
+type ('a, _) expression_t =
+ | Val: 'a -> ('a, right_v) expression_t
+ | Tag: ident -> ('a, right_v) expression_t
+ | Var: var_decl -> ('a, left_v) expression_t
+ | Memory: register_t -> ('a, left_v) expression_t
+
+(** TODO: why moving this elsewhere makes the exhaustiveness check fail? *)
+let type_of_l_value: type a. (a, left_v) expression_t -> Types.type_expr =
+ function
+ | Var v -> v.var_type
+ | Memory ResetFlag -> Type_predef.type_bool
+ | Memory (StateVar v) -> v.var_type
+
+type ('a, 'b) expressions_t = ('a, 'b) expression_t list
+
+type 'a predicate_t =
+ | Transition: ident * ident option * int option
+ * ('a, 'b) expressions_t
+ * ('a, 'b) expressions_t
+ * ('a, 'b) expressions_t -> 'a predicate_t
+ | MemoryPack of ident * ident option * int option
| Initialization
+ | ResetCleared of ident
type 'a formula_t =
| True
| False
- | Equal of 'a expression_t * 'a expression_t
+ | Equal: ('a, left_v) expression_t * ('a, 'b) expression_t -> 'a formula_t
| And of 'a formula_t list
| Or of 'a formula_t list
| Imply of 'a formula_t * 'a formula_t
| Exists of var_decl list * 'a formula_t
| Forall of var_decl list * 'a formula_t
- | Ternary of 'a expression_t * 'a formula_t * 'a formula_t
- | Predicate of predicate_t * 'a expression_t list
+ | Ternary: ('a, 'b) expression_t * 'a formula_t * 'a formula_t -> 'a formula_t
+ | Predicate: 'a predicate_t -> 'a formula_t
+ | StateVarPack of register_t
+ | ExistsMem of 'a formula_t * 'a formula_t
(* type 'a simulation_t = {
* sname: node_desc;
@@ -35,9 +51,16 @@ type 'a formula_t =
* sformula: 'a formula_t;
* } *)
+type 'a memory_pack_t = {
+ mpname: node_desc;
+ mpindex: int option;
+ mpformula: 'a formula_t;
+}
+
type 'a transition_t = {
tname: node_desc;
tindex: int option;
+ tinputs: var_decl list;
tlocals: var_decl list;
toutputs: var_decl list;
tformula: 'a formula_t;
diff --git a/src/utils/utils.ml b/src/utils/utils.ml
index a298bd36..df6e0bb8 100644
--- a/src/utils/utils.ml
+++ b/src/utils/utils.ml
@@ -284,6 +284,8 @@ module Format = struct
let pp_print_opar fmt () = pp_print_string fmt "("
let pp_print_cpar fmt () = pp_print_string fmt ")"
+ let pp_print_obracket fmt () = pp_print_string fmt "["
+ let pp_print_cbracket fmt () = pp_print_string fmt "]"
let pp_print_obrace fmt () = pp_print_string fmt "{"
let pp_print_cbrace fmt () = pp_print_string fmt "}"
let pp_print_opar' fmt () = pp_print_string fmt "( "
@@ -315,6 +317,8 @@ module Format = struct
pp_cl ()
(fun fmt l -> if l <> [] then pp_epilogue fmt ()) l
+ let pp_comma_list = pp_print_list ~pp_sep:pp_print_comma
+
let pp_print_list_i
?pp_prologue ?pp_epilogue ?pp_op ?pp_cl ?pp_open_box ?pp_eol ?pp_sep
pp_v =
@@ -343,6 +347,12 @@ module Format = struct
~pp_cl:pp_print_cpar
~pp_sep
+ let pp_print_bracketed ?(pp_sep=pp_print_comma) =
+ pp_print_list
+ ~pp_op:pp_print_obracket
+ ~pp_cl:pp_print_cbracket
+ ~pp_sep
+
let pp_print_braced ?(pp_sep=pp_print_comma) =
pp_print_list
~pp_op:pp_print_obrace
--
GitLab