diff --git a/.ocamlformat b/.ocamlformat
index b1bc4470bd72ad17da3b022db1369d0f7afa8e80..fe6b478e4b92fc68351704f501802748f670a884 100644
--- a/.ocamlformat
+++ b/.ocamlformat
@@ -3,3 +3,4 @@ parens-tuple=multi-line-only
wrap-comments=true
cases-exp-indent=2
break-cases=nested
+break-fun-decl=wrap
diff --git a/src/backends/C/c_backend_spec.ml b/src/backends/C/c_backend_spec.ml
index 505a58b881c45b54d37f9dba53f6b7b3258de2a8..fe72e4c3752bb4b87a414ed39239c9ab972ae89a 100644
--- a/src/backends/C/c_backend_spec.ml
+++ b/src/backends/C/c_backend_spec.ml
@@ -8,8 +8,8 @@
(* version 2.1. *)
(* *)
(********************************************************************)
-
-open Utils.Format
+open Utils
+open Format
open Lustre_types
open Machine_code_types
open C_backend_common
@@ -299,23 +299,18 @@ let pp_reset_cleared pp_mem_in pp_mem_out fmt (name, mem_in, mem_out) =
let pp_reset_cleared' = pp_reset_cleared pp_print_string pp_print_string
-let pp_functional_update mems fmt mem =
- let rec aux fmt mems =
- match mems with
+let pp_functional_update mems insts fmt mem =
+ let rec aux fmt = function
| [] ->
pp_print_string fmt mem
- | x :: mems ->
- fprintf fmt "{ @[<hov>%a@ \\with ._reg.%s = %s@] }" aux mems x x
+ | (x, is_mem) :: fields ->
+ fprintf fmt "{ @[<hov>%a@ \\with .%s%s = %s@] }" aux fields
+ (if is_mem then "_reg." else "")
+ x x
in
aux fmt
- (* if Utils.ISet.is_empty mems then
- * pp_print_string fmt mem
- * else
- * fprintf fmt "{ %s @[<hov>\\with %a@] }"
- * mem
- * (pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@;<1 -6>\\with ")
- * (fun fmt x -> fprintf fmt "._reg.%s = %s" x x)) *)
- (Utils.ISet.elements mems)
+ (List.map (fun (x, _) -> x, false) (Utils.IMap.bindings insts)
+ @ List.map (fun x -> x, true) (Utils.ISet.elements mems))
module PrintSpec = struct
type mode =
@@ -365,12 +360,13 @@ module PrintSpec = struct
fun ?output fmt e -> pp_expr ?output m mem_out fmt e
in
match p with
- | Transition (f, inst, i, inputs, locals, outputs, r, mems) ->
+ | Transition (f, inst, i, inputs, locals, outputs, r, mems, insts) ->
let pp_mem_in, pp_mem_out =
match inst with
| None ->
( pp_print_string,
- if mem_update then pp_functional_update mems else pp_print_string )
+ if mem_update then pp_functional_update mems insts
+ else pp_print_string )
| Some inst ->
( (fun fmt mem_in ->
if r then pp_print_string fmt mem_in
@@ -422,7 +418,7 @@ module PrintSpec = struct
eprintf "Internal error: arrow not found";
raise Not_found
- let pp_spec mode m fmt f =
+ 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
@@ -504,16 +500,7 @@ module PrintSpec = struct
fmt
((f, mk_mem_reset m), (rc, tr))
in
- match mode with
- | TransitionFootprintMode ->
- let mem_in = mk_mem_in m in
- let mem_out = mk_mem_out m in
- pp_forall
- (pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
- (pp_spec mode) fmt
- ((m.mname.node_id, [ mem_in; mem_out ]), f)
- | _ ->
- pp_spec mode fmt f
+ pp_spec mode
end
let pp_predicate pp_l pp_r fmt (l, r) =
@@ -583,31 +570,50 @@ let pp_transition_footprint fmt t =
t.tindex
let pp_transition_footprint_lemma m fmt t =
- let open Utils.ISet in
let name = t.tname.node_id in
+ let mem_in = mk_mem_in m in
+ let mem_out = mk_mem_out m in
let mems =
- diff (of_list (List.map (fun v -> v.var_id) m.mmemory)) t.tfootprint
+ ISet.(
+ diff (of_list (List.map (fun v -> v.var_id) m.mmemory)) t.tmem_footprint)
+ in
+ let insts =
+ IMap.(
+ diff
+ (of_list (List.map (fun (x, (td, _)) -> x, node_name td) m.minstances))
+ t.tinst_footprint)
in
let memories =
List.map
(fun v -> { v with var_type = { v.var_type with tid = -1 } })
- (List.filter (fun v -> not (mem v.var_id t.tfootprint)) m.mmemory)
+ (List.filter (fun v -> ISet.mem v.var_id mems) m.mmemory)
+ in
+ let mems_empty = ISet.is_empty mems in
+ let insts_empty = IMap.is_empty insts in
+ let instances = List.map (fun (i, f) -> f, i) (IMap.bindings insts) in
+ let tr ?mems ?insts () =
+ Spec_common.mk_transition ?mems ?insts ?i:t.tindex name
+ (vdecls_to_vals t.tinputs) (vdecls_to_vals t.tlocals)
+ (vdecls_to_vals t.toutputs)
in
- if not (is_empty mems) then
+ if not (mems_empty && insts_empty) then
pp_acsl
(pp_lemma pp_transition_footprint
- (PrintSpec.pp_spec TransitionFootprintMode m))
+ (pp_forall
+ (pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
+ ((if insts_empty then fun pp fmt (_, x) -> pp fmt x
+ else pp_forall (pp_comma_list (pp_machine_decl' ~ghost:true)))
+ ((if mems_empty then fun pp fmt (_, x) -> pp fmt x
+ else pp_forall (pp_locals m))
+ (PrintSpec.pp_spec TransitionFootprintMode m)))))
fmt
( t,
- Forall
- ( memories @ t.tinputs @ t.tlocals @ t.toutputs,
- Imply
- ( Spec_common.mk_transition ?i:t.tindex name
- (vdecls_to_vals t.tinputs) (vdecls_to_vals t.tlocals)
- (vdecls_to_vals t.toutputs),
- Spec_common.mk_transition ~mems ?i:t.tindex name
- (vdecls_to_vals t.tinputs) (vdecls_to_vals t.tlocals)
- (vdecls_to_vals t.toutputs) ) ) )
+ ( (m.mname.node_id, [ mem_in; mem_out ]),
+ ( instances,
+ ( memories,
+ Forall
+ ( t.tinputs @ t.tlocals @ t.toutputs,
+ Imply (tr (), tr ~mems ~insts ()) ) ) ) ) )
let pp_transition_footprint_lemmas fmt m =
pp_print_list ~pp_epilogue:pp_print_cut ~pp_open_box:pp_open_vbox0
diff --git a/src/machine_code.ml b/src/machine_code.ml
index 44645a32bed90dfb7f8aa439dc76660be18e4ec6..cf324c94324ed58f21966f27b0a5411cd07b0400 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -137,7 +137,6 @@ 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_expr = translate_expr env in
let lustre_eq = Corelang.mkeq Location.dummy_loc ([ y.var_id ], expr) in
match expr.expr_desc with
@@ -193,6 +192,8 @@ type machine_ctx = {
* var_decl list
(* outputs *)
* ISet.t (* memory footprint *)
+ * ident IMap.t
+ (* memory instances footprint *)
* mc_formula_t)
(* formula *)
list;
@@ -250,6 +251,7 @@ let translate_eq env ctx nd inputs locals outputs i eq =
locals_i,
outputs_i,
ctx.m,
+ IMap.map (fun (td, _) -> node_name td) ctx.j,
Exists
( Lustre_live.existential_vars id i eq (locals @ outputs),
And
@@ -303,13 +305,9 @@ let translate_eq env ctx nd inputs locals outputs i eq =
(MStep ([ var_x ], inst, [ c1; c2 ]))
(mk_memory_pack ~inst (node_name td))
(mk_transition ~inst (node_name td) [] [] [ vdecl_to_val var_x ])
- ctx
+ { ctx with j = IMap.add inst (td, []) ctx.j }
in
- {
- ctx with
- si = mkinstr (MSetReset inst) :: ctx.si;
- j = IMap.add inst (td, []) ctx.j;
- }
+ { ctx with si = mkinstr (MSetReset inst) :: ctx.si }
| [ x ], Expr_pre e when env.is_local x ->
let var_x = env.get_var x in
let e = translate_expr e in
@@ -354,7 +352,11 @@ let translate_eq env ctx nd inputs locals outputs i eq =
(MStep (var_p, inst, vl))
(mk_memory_pack ~inst (node_name node_f))
(mk_transition ?r ~inst (node_name node_f) vl [] (vdecls_to_vals var_p))
- ctx
+ {
+ ctx with
+ j = IMap.add inst call_f ctx.j;
+ s = (if Stateless.check_node node_f then [] else reset_inst) @ ctx.s;
+ }
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:
@@ -365,8 +367,6 @@ let translate_eq env ctx nd inputs locals outputs i eq =
si =
(if Stateless.check_node node_f 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_inst) @ ctx.s;
}
| [ x ], _ ->
let var_x = env.get_var x in
@@ -476,7 +476,8 @@ let transition_0 nd =
tlocals = [];
toutputs = [];
tformula = True;
- tfootprint = ISet.empty;
+ tmem_footprint = ISet.empty;
+ tinst_footprint = IMap.empty;
}
let transition_toplevel nd i =
@@ -495,7 +496,8 @@ let transition_toplevel nd i =
tformula =
(if fst (get_stateless_status_node nd) then tr
else ExistsMem (nd.node_id, Predicate (ResetCleared nd.node_id), tr));
- tfootprint = ISet.empty;
+ tmem_footprint = ISet.empty;
+ tinst_footprint = IMap.empty;
}
let translate_decl nd sch =
@@ -562,7 +564,7 @@ let translate_decl nd sch =
transition_0 nd
::
List.mapi
- (fun i (tinputs, tlocals, toutputs, tfootprint, f) ->
+ (fun i (tinputs, tlocals, toutputs, tmem_footprint, tinst_footprint, f) ->
{
tname = nd;
tindex = Some (i + 1);
@@ -570,7 +572,8 @@ let translate_decl nd sch =
tlocals;
toutputs;
tformula = red f;
- tfootprint;
+ tmem_footprint;
+ tinst_footprint;
})
(List.rev ctx.t)
@ [ transition_toplevel nd (List.length ctx.t) ]
diff --git a/src/machine_code_common.ml b/src/machine_code_common.ml
index 3248efb87811035e6162a86ff9193b142508a398..af44a8ec969ca118fe20bc97a9a8a3b95678c72c 100644
--- a/src/machine_code_common.ml
+++ b/src/machine_code_common.ml
@@ -58,7 +58,7 @@ module PrintSpec = struct
fun fmt e -> pp_expr m fmt e
in
match p with
- | Transition (f, inst, i, inputs, locals, outputs, _r, _mems) ->
+ | Transition (f, inst, i, inputs, locals, outputs, _r, _mems, _insts) ->
fprintf fmt "Transition_%a<%a>%a%a" pp_print_string f
(pp_print_option
~none:(fun fmt () -> pp_print_string fmt "SELF")
@@ -321,30 +321,17 @@ let id_to_tag id =
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))) *)
- (MBranch (c, [ tag_true, t; tag_false, e ]))
-
-let mk_branch ?lustre_eq c br =
- mkinstr ?lustre_eq
- (* (And (List.map (fun (l, instrs) ->
- * Imply (Equal (Val c, Tag l), And (List.map get_instr_spec instrs)))
- * br)) *)
- (MBranch (c, br))
+ mkinstr ?lustre_eq (MBranch (c, [ tag_true, t; tag_false, e ]))
+
+let mk_branch ?lustre_eq c br = mkinstr ?lustre_eq (MBranch (c, br))
let mk_branch' ?lustre_eq v = mk_branch ?lustre_eq (vdecl_to_val v)
-let mk_assign ?lustre_eq x v =
- mkinstr ?lustre_eq (* (Equal (Var x, Val v)) *) (MLocalAssign (x, v))
+let mk_assign ?lustre_eq x v = mkinstr ?lustre_eq (MLocalAssign (x, v))
let arrow_machine =
let state = "_first" in
- let var_state =
- dummy_var_decl state Type_predef.type_bool
- (* (Types.new_ty Types.Tbool) *)
- in
+ let var_state = dummy_var_decl state Type_predef.type_bool in
let var_input1 = List.nth Arrow.arrow_desc.node_inputs 0 in
let var_input2 = List.nth Arrow.arrow_desc.node_inputs 1 in
let var_output = List.nth Arrow.arrow_desc.node_outputs 0 in
diff --git a/src/spec_common.ml b/src/spec_common.ml
index 399cb31b71dfe88004b5a8803ba32c555dc97b25..6f3c9373bb641f05fedaea2dcbfd9298bbc3e6da 100644
--- a/src/spec_common.ml
+++ b/src/spec_common.ml
@@ -1,4 +1,5 @@
open Spec_types
+open Utils
(* a small reduction engine *)
let is_true = function True -> true | _ -> false
@@ -73,20 +74,13 @@ let rec red : type a. a formula_t -> a formula_t = function
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 vals vs = List.map (fun v -> Val v) vs
let mk_pred_call pred = Predicate pred
-(* let mk_clocked_on id =
- * mk_pred_call (Clocked_on id) *)
-
-let mk_transition ?(mems = Utils.ISet.empty) ?r ?i ?inst id inputs locals
- outputs =
+let mk_transition ?(mems = ISet.empty) ?(insts = IMap.empty) ?r ?i ?inst id
+ inputs locals outputs =
let tr =
mk_pred_call
(Transition
@@ -97,7 +91,8 @@ let mk_transition ?(mems = Utils.ISet.empty) ?r ?i ?inst id inputs locals
vals locals,
vals outputs,
(match r with Some _ -> true | None -> false),
- mems ))
+ mems,
+ insts ))
in
match r, inst with
| Some r, Some inst ->
@@ -113,7 +108,14 @@ 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_branch_tr x =
+ let open Lustre_types in
+ function
+ | [ (h1, spec1); (h2, spec2) ] when h1 = tag_true && h2 = tag_false ->
+ Ternary (Var x, spec1, spec2)
+ | [ (h1, spec1); (h2, spec2) ] when h1 = tag_false && h2 = tag_true ->
+ Ternary (Var x, spec2, spec1)
+ | 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 e8ed01ad6ce243b4c013a3d392dce4840621bf11..c1201c3a138b98171a008ae892c320d86ebddac8 100644
--- a/src/spec_types.ml
+++ b/src/spec_types.ml
@@ -39,6 +39,8 @@ type 'a predicate_t =
(* outputs *)
* bool (* reset *)
* Utils.ISet.t (* memory footprint *)
+ * ident Utils.IMap.t
+ (* memory instances footprint *)
-> 'a predicate_t
| Reset of ident * ident * 'a
| MemoryPack of ident * ident option * int option
@@ -80,5 +82,6 @@ type 'a transition_t = {
tlocals : var_decl list;
toutputs : var_decl list;
tformula : 'a formula_t;
- tfootprint : Utils.ISet.t;
+ tmem_footprint : Utils.ISet.t;
+ tinst_footprint : ident Utils.IMap.t;
}
diff --git a/src/utils/env.ml b/src/utils/env.ml
index d4e03231350f39e3ecd65a780dc4e94d73a68bec..8a6c7bcae80dbea64cf0606e86d10e7c333f35af 100644
--- a/src/utils/env.ml
+++ b/src/utils/env.ml
@@ -35,8 +35,7 @@ let overwrite x y =
x y
let pp_env pp_fun fmt env =
- let lid, lty = list_of_imap env in
- let l' = List.combine lid lty in
+ let l' = IMap.bindings env in
let pp_fun fmt (id, value) = Format.fprintf fmt "%s |-> %a" id pp_fun value in
Format.fprintf fmt "{ @[<v 2>%a@] }" (fprintf_list ~sep:"@," pp_fun) l'
diff --git a/src/utils/utils.ml b/src/utils/utils.ml
index ef930561f58d3945ec615a61cc27ef2cdbfa51a9..5283e7aa05db1c5e15aadc156a45fcf9146a6150 100644
--- a/src/utils/utils.ml
+++ b/src/utils/utils.ml
@@ -41,17 +41,17 @@ end
module IMap = struct
include Map.Make (IdentModule)
- let union_l m1 m2 =
+ let diff m1 m2 =
merge
(fun _ o1 o2 ->
match o1, o2 with
- | None, None ->
- None
- | Some _, _ ->
- o1
- | _, Some _ ->
- o2)
+ | Some v1, Some v2 ->
+ if v1 = v2 then None else o1
+ | _ ->
+ o1)
m1 m2
+
+ let of_list l = List.fold_left (fun m (x, v) -> add x v m) empty l
end
module ISet = Set.Make (IdentModule)
@@ -123,10 +123,6 @@ let rec filter_upto p n l =
| t :: q ->
if p t then t :: filter_upto p (n - 1) q else filter_upto p n q
-(* Warning: bad complexity *)
-let list_of_imap imap =
- IMap.fold (fun i v (il, vl) -> i :: il, v :: vl) imap ([], [])
-
(** [gcd a b] returns the greatest common divisor of [a] and [b]. *)
let rec gcd a b = if b = 0 then a else gcd b (a mod b)