From c4780a6a66b6da8b4dec76193acca22ccda416f3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lelio.brun@isae-supaero.fr>
Date: Tue, 15 Jun 2021 17:34:57 +0200
Subject: [PATCH] work on new reset functions generation
---
src/backends/C/c_backend_common.ml | 74 ++++-
src/backends/C/c_backend_spec.ml | 110 +++++---
src/backends/C/c_backend_src.ml | 309 ++++++++++-----------
src/backends/EMF/EMF_common.ml | 3 +
src/backends/Horn/horn_backend_printers.ml | 5 +
src/machine_code.ml | 2 +-
src/machine_code_common.ml | 7 +-
src/machine_code_common.mli | 3 +-
src/machine_code_types.ml | 2 +
src/optimize_machine.ml | 18 +-
10 files changed, 321 insertions(+), 212 deletions(-)
diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml
index bcffd9e9..49475226 100644
--- a/src/backends/C/c_backend_common.ml
+++ b/src/backends/C/c_backend_common.ml
@@ -298,7 +298,14 @@ let rec pp_c_const fmt c =
| Const_string _
| Const_modeid _ -> assert false (* string occurs in annotations not in C *)
-
+let reset_flag_name = "_reset"
+let pp_reset_flag ?(indirect=true) fmt self =
+ fprintf fmt "%s%s%s" self (if indirect then "->" else ".") reset_flag_name
+
+let pp_reset_assign self fmt b =
+ fprintf fmt "%a = %i;"
+ (pp_reset_flag ~indirect:true) self (if b then 1 else 0)
+
(* Prints a value expression [v], with internal function calls only.
[pp_var] is a printer for variables (typically [pp_c_var_read]),
but an offset suffix may be added for array variables
@@ -329,6 +336,9 @@ let rec pp_c_val m self pp_var fmt v =
pp_var fmt v
| Fun (n, vl) ->
pp_basic_lib_fun (Types.is_int_type v.value_type) n pp_c_val fmt vl
+ | ResetFlag ->
+ pp_reset_flag fmt self
+
(* Access to the value of a variable:
- if it's not a scalar output, then its name is enough
@@ -472,6 +482,7 @@ let rec expansion_depth v =
| Array vl -> 1 + List.fold_right (fun v -> max (expansion_depth v)) vl 0
| Access (v, _) -> max 0 (expansion_depth v - 1)
| Power _ -> 0 (*1 + expansion_depth v*)
+ | ResetFlag -> 0
and expansion_depth_cst c =
match c with
| Const_array cl ->
@@ -604,6 +615,8 @@ let rec pp_value_suffix ?(indirect=true) m self var_type loop_vars pp_var fmt va
fprintf fmt "%a%a" pp_var v pp_suffix loop_vars
| _, Cst cst ->
pp_c_const_suffix var_type fmt cst
+ | _, ResetFlag ->
+ pp_reset_flag fmt self
| _, _ ->
eprintf "internal error: C_backend_src.pp_value_suffix %a %a %a@."
Types.print_ty var_type (pp_val m) value pp_suffix loop_vars;
@@ -676,18 +689,18 @@ let print_dealloc_prototype fmt name =
(pp_machine_memtype_name ~ghost:false) name
module type MODIFIERS_GHOST_PROTO = sig
- val pp_ghost_parameters: formatter -> (string * (formatter -> string -> unit)) list -> unit
+ val pp_ghost_parameters: ?cut:bool -> formatter -> (string * (formatter -> string -> unit)) list -> unit
end
module EmptyGhostProto: MODIFIERS_GHOST_PROTO = struct
- let pp_ghost_parameters _ _ = ()
+ let pp_ghost_parameters ?cut _ _ = ()
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
+ (fun fmt mem -> fprintf fmt "\\ghost %a" pp_ptr mem) fmt
(name, mem)
let print_clear_reset_prototype self mem fmt (name, static) =
@@ -697,7 +710,7 @@ module Protos (Mod: MODIFIERS_GHOST_PROTO) = struct
pp_c_decl_input_var) static
(pp_machine_memtype_name ~ghost:false) name
self
- Mod.pp_ghost_parameters [mem, pp_mem_ghost name]
+ (Mod.pp_ghost_parameters ~cut:true) [mem, pp_mem_ghost name]
let print_set_reset_prototype self mem fmt (name, static) =
fprintf fmt "@[<v>void %a (%a%a *%s)%a@]"
@@ -706,7 +719,7 @@ module Protos (Mod: MODIFIERS_GHOST_PROTO) = struct
pp_c_decl_input_var) static
(pp_machine_memtype_name ~ghost:false) name
self
- Mod.pp_ghost_parameters [mem, pp_mem_ghost name]
+ (Mod.pp_ghost_parameters ~cut:true) [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@]"
@@ -717,7 +730,7 @@ module Protos (Mod: MODIFIERS_GHOST_PROTO) = struct
~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]
+ (Mod.pp_ghost_parameters ~cut:true) [mem, pp_mem_ghost name]
let print_init_prototype self fmt (name, static) =
fprintf fmt "void %a (%a%a *%s)"
@@ -879,6 +892,53 @@ let pp_file_open fmt inout idx =
inout idx;
"f_" ^ inout ^ string_of_int idx
+let pp_basic_assign pp_var fmt typ var_name value =
+ if Types.is_real_type typ && !Options.mpfr
+ then
+ Mpfr.pp_inject_assign pp_var fmt (var_name, value)
+ else
+ fprintf fmt "%a = %a;"
+ pp_var var_name
+ pp_var value
+
+(* type_directed assignment: array vs. statically sized type
+ - [var_type]: type of variable to be assigned
+ - [var_name]: name of variable to be assigned
+ - [value]: assigned value
+ - [pp_var]: printer for variables
+*)
+let pp_assign m self pp_var fmt (var, value) =
+ let depth = expansion_depth value in
+ let var_type = var.var_type in
+ let var = mk_val (Var var) var_type in
+ (*eprintf "pp_assign %a %a %a %d@." Types.print_ty var_type pp_val var_name pp_val value depth;*)
+ let loop_vars = mk_loop_variables m var_type depth in
+ let reordered_loop_vars = reorder_loop_variables loop_vars in
+ let rec aux typ fmt vars =
+ match vars with
+ | [] ->
+ pp_basic_assign (pp_value_suffix m self var_type loop_vars pp_var)
+ fmt typ var value
+ | (d, LVar i) :: q ->
+ let typ' = Types.array_element_type typ in
+ (*eprintf "pp_aux %a %s@." Dimension.pp_dimension d i;*)
+ fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
+ i i i pp_c_dimension d i
+ (aux typ') q
+ | (d, LInt r) :: q ->
+ (*eprintf "pp_aux %a %d@." Dimension.pp_dimension d (!r);*)
+ let typ' = Types.array_element_type typ in
+ let szl = Utils.enumerate (Dimension.size_const_dimension d) in
+ fprintf fmt "@[<v 2>{@,%a@]@,}"
+ (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl
+ | _ -> assert false
+ in
+ begin
+ reset_loop_counter ();
+ (*reset_addr_counter ();*)
+ aux var_type fmt reordered_loop_vars;
+ (*eprintf "end pp_assign@.";*)
+ end
(* Local Variables: *)
(* compile-command:"make -C ../../.." *)
diff --git a/src/backends/C/c_backend_spec.ml b/src/backends/C/c_backend_spec.ml
index c87b1f74..16fe5e6a 100644
--- a/src/backends/C/c_backend_spec.ml
+++ b/src/backends/C/c_backend_spec.ml
@@ -49,6 +49,12 @@ let pp_acsl_cut pp fmt =
let pp_acsl_line pp fmt =
fprintf fmt "//%@ @[<h>%a@]" pp
+let pp_acsl_line' pp fmt =
+ fprintf fmt "/*%@ @[<h>%a@] */" pp
+
+let pp_acsl_line_cut pp fmt =
+ fprintf fmt "%a@," (pp_acsl_line pp)
+
let pp_requires pp_req fmt =
fprintf fmt "requires %a;" pp_req
@@ -362,7 +368,7 @@ module PrintSpec = struct
let pp_reg pp_mem fmt = function
| ResetFlag ->
- fprintf fmt "%t_reset" pp_mem
+ fprintf fmt "%t%s" pp_mem reset_flag_name
| StateVar x ->
fprintf fmt "%t%a" pp_mem pp_var_decl x
@@ -695,7 +701,7 @@ let label_pre = "Pre"
let pp_at_pre pp_p fmt p =
pp_at pp_p fmt (p, label_pre)
-let pp_register ?(indirect=true) ptr =
+let pp_register_chain ?(indirect=true) ptr =
pp_print_list
~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
~pp_epilogue:(fun fmt () -> fprintf fmt "%s_reg._first"
@@ -703,19 +709,24 @@ let pp_register ?(indirect=true) ptr =
~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 =
+let pp_reset_flag_chain ?(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_epilogue:(fun fmt () -> pp_reset_flag ~indirect fmt "")
~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
(fun fmt (i, _) -> pp_print_string fmt i)
fmt mems
+let pp_arrow_reset_ghost mem fmt inst =
+ fprintf fmt "%s_reset_ghost(%a)" Arrow.arrow_id pp_indirect' (mem, inst)
+
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))))
+ let pp_ghost_parameters ?(cut=true) fmt vs =
+ fprintf fmt "%a%a"
+ (if cut then pp_print_cut else pp_print_nothing) ()
+ (pp_acsl_line'
+ (pp_ghost
+ (pp_print_parenthesized (fun fmt (x, pp) -> pp fmt x))))
vs
end
@@ -763,33 +774,37 @@ module SrcMod = struct
pp_transition_defs
~pp_epilogue:pp_print_cutcut) machines
- let pp_clear_reset_spec fmt machines self mem m =
+ let pp_clear_reset_spec fmt self mem m =
let name = m.mname.node_id in
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@,%a@,%a@,%a@,%a@,%a@,%a@,\
@[<v 2>behavior reset:@;\
%a@,%a@]@,\
@[<v 2>behavior no_reset:@;\
- %a@,%a@]"
+ %a@,%a@]@,\
+ complete behaviors;@,\
+ disjoint behaviors;"
(pp_requires pp_mem_valid') (name, self)
(pp_requires (pp_separated self mem)) (mk_insts m.minstances, [])
+ (pp_requires (pp_memory_pack_aux pp_ptr pp_print_string))
+ (name, mem, self)
(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_assigns pp_reset_flag) [self]
+ (pp_assigns (pp_register_chain self)) (mk_insts arws)
+ (pp_assigns (pp_reset_flag_chain self)) (mk_insts narws)
+ (pp_assigns pp_reset_flag) [mem]
+ (pp_assigns (pp_register_chain ~indirect:false mem)) (mk_insts arws)
+ (pp_assigns (pp_reset_flag_chain ~indirect:false mem)) (mk_insts narws)
+ (pp_assumes (pp_equal pp_reset_flag pp_print_int)) (mem, 1)
(pp_ensures (pp_initialization pp_ptr)) (name, mem)
- (pp_assumes (pp_equal pp_indirect' pp_print_int)) ((mem, "_reset"), 0)
+ (pp_assumes (pp_equal pp_reset_flag pp_print_int)) (mem, 0)
(pp_ensures (pp_equal pp_ptr (pp_old pp_ptr))) (mem, mem)
)
fmt ()
@@ -800,8 +815,8 @@ module SrcMod = struct
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])
+ (pp_ensures (pp_equal pp_reset_flag pp_print_string)) (mem, "1")
+ (pp_assigns pp_reset_flag) [self; mem])
fmt ()
let pp_step_spec fmt machines self mem m =
@@ -833,29 +848,56 @@ module SrcMod = struct
(pp_assigns pp_ptr_decl) outputs
(pp_assigns (pp_reg self)) m.mmemory
(pp_assigns (pp_memory self)) (memories insts')
- (pp_assigns (pp_register self)) insts
- (pp_assigns (pp_reset_flag self)) insts''
+ (pp_assigns (pp_register_chain self)) insts
+ (pp_assigns (pp_reset_flag_chain 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_assigns (pp_register_chain ~indirect:false mem)) insts
+ (pp_assigns (pp_reset_flag_chain ~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 instr =
- fprintf fmt "@,%a"
- (pp_print_list ~pp_open_box:pp_open_vbox0
- (pp_acsl (pp_assert (PrintSpec.pp_spec (InstrMode self) m))))
+ let pp_ghost_instr_code m self fmt instr = match instr.instr_desc with
+ | MStateAssign (x, v) ->
+ fprintf fmt "@,%a"
+ (pp_acsl_line
+ (pp_ghost
+ (pp_assign m self (pp_c_var_read m))))
+ (x, v)
+ | MResetAssign b ->
+ fprintf fmt "@,%a"
+ (pp_acsl_line
+ (pp_ghost
+ (pp_reset_assign self)))
+ b
+ | MSetReset inst ->
+ let td, _ = List.assoc inst m.minstances in
+ if Arrow.td_is_arrow td then
+ fprintf fmt "@,%a"
+ (pp_acsl_line
+ (pp_ghost
+ (pp_arrow_reset_ghost self)))
+ inst
+ | _ -> ()
+
+ let pp_step_instr_spec m self mem fmt instr =
+ fprintf fmt "%a%a"
+ (pp_ghost_instr_code m mem) instr
+ (pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_prologue:pp_print_cut
+ (pp_acsl_line' (pp_assert (PrintSpec.pp_spec (InstrMode self) m))))
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"))))
+ let pp_ghost_parameter mem fmt inst =
+ GhostProto.pp_ghost_parameters ~cut:false fmt
+ (match inst with
+ | Some inst ->
+ [inst, fun fmt inst -> fprintf fmt "&%a" pp_indirect' (mem, inst)]
+ | None ->
+ [mem, pp_print_string])
+
end
(**************************************************************************)
diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index 002ae1d7..e7d245cf 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/src/backends/C/c_backend_src.ml
@@ -20,20 +20,20 @@ module type MODIFIERS_SRC = sig
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_clear_reset_spec: formatter -> 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
+ val pp_step_instr_spec: machine_t -> ident -> ident -> formatter -> instr_t -> unit
+ val pp_ghost_parameter: ident -> formatter -> ident option -> unit
end
module EmptyMod = struct
module GhostProto = EmptyGhostProto
let pp_predicates _ _ = ()
let pp_set_reset_spec _ _ _ _ = ()
- let pp_clear_reset_spec _ _ _ _ _ = ()
+ let pp_clear_reset_spec _ _ _ _ = ()
let pp_step_spec _ _ _ _ _ = ()
- let pp_step_instr_spec _ _ _ _ = ()
- let pp_ghost_set_reset_spec _ _ = ()
+ let pp_step_instr_spec _ _ _ _ _ = ()
+ let pp_ghost_parameter _ _ _ = ()
end
module Main = functor (Mod: MODIFIERS_SRC) -> struct
@@ -55,7 +55,7 @@ module Main = functor (Mod: MODIFIERS_SRC) -> struct
let rec static_loop_profile v =
match v.value_desc with
| Cst cst -> static_loop_profile_cst cst
- | Var _ -> []
+ | Var _ | ResetFlag -> []
| Fun (_, vl) ->
List.fold_right
(fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) vl []
@@ -81,54 +81,8 @@ module Main = functor (Mod: MODIFIERS_SRC) -> struct
let pp_c_val m self pp_var fmt v =
pp_value_suffix m self v.value_type [] pp_var fmt v
- let pp_basic_assign pp_var fmt typ var_name value =
- if Types.is_real_type typ && !Options.mpfr
- then
- Mpfr.pp_inject_assign pp_var fmt (var_name, value)
- else
- fprintf fmt "%a = %a;"
- pp_var var_name
- pp_var value
-
- (* type_directed assignment: array vs. statically sized type
- - [var_type]: type of variable to be assigned
- - [var_name]: name of variable to be assigned
- - [value]: assigned value
- - [pp_var]: printer for variables
- *)
- let pp_assign m self pp_var fmt var_type var_name value =
- let depth = expansion_depth value in
- (*eprintf "pp_assign %a %a %a %d@." Types.print_ty var_type pp_val var_name pp_val value depth;*)
- let loop_vars = mk_loop_variables m var_type depth in
- let reordered_loop_vars = reorder_loop_variables loop_vars in
- let rec aux typ fmt vars =
- match vars with
- | [] ->
- pp_basic_assign (pp_value_suffix m self var_type loop_vars pp_var)
- fmt typ var_name value
- | (d, LVar i) :: q ->
- let typ' = Types.array_element_type typ in
- (*eprintf "pp_aux %a %s@." Dimension.pp_dimension d i;*)
- fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
- i i i pp_c_dimension d i
- (aux typ') q
- | (d, LInt r) :: q ->
- (*eprintf "pp_aux %a %d@." Dimension.pp_dimension d (!r);*)
- let typ' = Types.array_element_type typ in
- let szl = Utils.enumerate (Dimension.size_const_dimension d) in
- fprintf fmt "@[<v 2>{@,%a@]@,}"
- (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl
- | _ -> assert false
- in
- begin
- reset_loop_counter ();
- (*reset_addr_counter ();*)
- aux var_type fmt reordered_loop_vars;
- (*eprintf "end pp_assign@.";*)
- end
-
- let pp_machine_ pp_machine_name fn_name m fmt ?inst self =
- let name, static =
+ let pp_machine_ pp_machine_name fn_name m fmt ?inst self mem =
+ let name, is_arrow, static =
match inst with
| Some inst ->
let node, static = try List.assoc inst m.minstances with Not_found ->
@@ -136,32 +90,40 @@ module Main = functor (Mod: MODIFIERS_SRC) -> struct
fn_name m.mname.node_id self inst;
raise Not_found
in
- node_name node, static
+ node_name node, Arrow.td_is_arrow node, static
| None ->
- m.mname.node_id, []
+ m.mname.node_id, false, []
in
- fprintf fmt "%a(%a%s%a);"
- pp_machine_name name
+ let is_arrow_reset = is_arrow && fn_name = "pp_machine_set_reset" in
+ fprintf fmt "%a(%a%s%a)%a;"
+ (if is_arrow_reset then
+ (fun fmt -> fprintf fmt "%s_reset")
+ else
+ 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
+ (if is_arrow_reset then pp_print_nothing else Mod.pp_ghost_parameter mem)
+ 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_set_reset m self mem fmt inst =
+ pp_machine_ pp_machine_set_reset_name "pp_machine_set_reset" m fmt ~inst
+ self mem
- 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_clear_reset m self mem fmt =
+ pp_machine_ pp_machine_clear_reset_name "pp_machine_clear_reset" m fmt
+ self mem
- let pp_machine_init m self fmt inst =
- pp_machine_ pp_machine_init_name "pp_machine_init" m fmt ~inst self
+ let pp_machine_init m self mem fmt inst =
+ pp_machine_ pp_machine_init_name "pp_machine_init" m fmt ~inst self mem
- let pp_machine_clear m self fmt inst =
- pp_machine_ pp_machine_clear_name "pp_machine_clear" m fmt ~inst self
+ let pp_machine_clear m self mem fmt inst =
+ pp_machine_ pp_machine_clear_name "pp_machine_clear" m fmt ~inst self mem
- let pp_call m self pp_read pp_write fmt i inputs outputs =
+ let pp_call m self mem 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)%a;"
pp_machine_step_name (node_name n)
(pp_comma_list ~pp_eol:pp_print_comma
(pp_c_val m self pp_read)) inputs
@@ -169,6 +131,7 @@ module Main = functor (Mod: MODIFIERS_SRC) -> struct
pp_write) outputs
self
i
+ (Mod.pp_ghost_parameter mem) (Some i)
with Not_found -> (* stateless node instance *)
let n, _ = List.assoc i m.mcalls in
fprintf fmt "%a(%a%a);"
@@ -177,20 +140,21 @@ module Main = functor (Mod: MODIFIERS_SRC) -> struct
(pp_c_val m self pp_read)) inputs
(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_basic_instance_call m self mem =
+ pp_call m self mem (pp_c_var_read m) (pp_c_var_write m)
- let pp_arrow_call m self fmt i outputs =
+ let pp_arrow_call m self mem fmt i outputs =
match outputs with
| [x] ->
- fprintf fmt "%a = %a(%s->%s);"
+ fprintf fmt "%a = %a(%s->%s)%a;"
(pp_c_var_read m) x
pp_machine_step_name Arrow.arrow_id
self
i
+ (Mod.pp_ghost_parameter mem) (Some i)
| _ -> assert false
- let pp_instance_call m self fmt i inputs outputs =
+ let pp_instance_call m self mem fmt i inputs outputs =
let pp_offset pp_var indices fmt var =
fprintf fmt "%a%a"
pp_var var
@@ -208,86 +172,103 @@ module Main = functor (Mod: MODIFIERS_SRC) -> struct
else
let pp_read = pp_offset (pp_c_var_read m) indices in
let pp_write = pp_offset (pp_c_var_write m) indices in
- pp_call m self pp_read pp_write fmt i inputs outputs
+ pp_call m self mem pp_read pp_write fmt i inputs outputs
in
reset_loop_counter ();
aux [] fmt (List.hd inputs).Machine_code_types.value_type
- let rec pp_conditional dependencies (m: machine_t) self fmt c tl el =
- fprintf fmt "@[<v 2>if (%a) {%a@]@,@[<v 2>} else {%a@]@,}"
- (pp_c_val m self (pp_c_var_read m)) c
- (pp_print_list ~pp_prologue:pp_print_cut
- (pp_machine_instr dependencies m self)) tl
- (pp_print_list ~pp_prologue:pp_print_cut
- (pp_machine_instr dependencies m self)) el
-
- and pp_machine_instr dependencies (m: machine_t) self fmt instr =
- match get_instr_desc instr with
- | MNoReset _ -> ()
- | 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
- i.var_type (mk_val (Var i) i.var_type) v
- | MStateAssign (i,v) ->
- pp_assign
- m self (pp_c_var_read m) fmt
- i.var_type (mk_val (Var i) i.var_type) v
- | MStep ([i0], i, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (i, vl)) i0.var_type) ->
- pp_machine_instr dependencies m self fmt
- (update_instr_desc instr (MLocalAssign (i0, mk_val (Fun (i, vl)) i0.var_type)))
- | MStep (il, i, vl) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
- pp_instance_call m self fmt i vl il
- | MStep ([i0], i, vl) when has_c_prototype i dependencies ->
- fprintf fmt "%a = %s%a;"
- (pp_c_val m self (pp_c_var_read m)) (mk_val (Var i0) i0.var_type)
- i
- (pp_print_parenthesized (pp_c_val m self (pp_c_var_read m))) vl
- | MStep (il, i, vl) ->
- 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;
- assert false
- | MBranch (g, hl) ->
- if let t = fst (List.hd hl) in t = tag_true || t = tag_false
- then (* boolean case, needs special treatment in C because truth value is not unique *)
- (* may disappear if we optimize code by replacing last branch test with default *)
- let tl = try List.assoc tag_true hl with Not_found -> [] in
- let el = try List.assoc tag_false hl with Not_found -> [] in
- pp_conditional dependencies m self fmt g tl el
- else (* enum type case *)
- (*let g_typ = Typing.type_const Location.dummy_loc (Const_tag (fst (List.hd hl))) in*)
- fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]"
- (pp_c_val m self (pp_c_var_read m)) g
- (pp_print_list ~pp_open_box:pp_open_vbox0
- (pp_machine_branch dependencies m self)) hl
- | MSpec s ->
- fprintf fmt "@[/*@@ %s */@]@ " s
- | MComment s ->
- fprintf fmt "/*%s*/@ " s
-
- and pp_machine_branch dependencies m self fmt (t, h) =
+ let rec pp_conditional dependencies m self mem fmt c tl el =
+ let pp_machine_instrs =
+ pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_prologue:pp_print_cut
+ (pp_machine_instr dependencies m self mem) in
+ let pp_cond = pp_c_val m self (pp_c_var_read m) in
+ match tl, el with
+ | [], _ :: _ ->
+ fprintf fmt "@[<v 2>if (!%a) {%a@]@,}"
+ pp_cond c
+ pp_machine_instrs el
+ | _, [] ->
+ fprintf fmt "@[<v 2>if (%a) {%a@]@,}"
+ pp_cond c
+ pp_machine_instrs tl
+ | _, _ ->
+ fprintf fmt "@[<v 2>if (%a) {%a@]@,@[<v 2>} else {%a@]@,}"
+ pp_cond c
+ pp_machine_instrs tl
+ pp_machine_instrs el
+
+ and pp_machine_instr dependencies m self mem fmt instr =
+ let pp_instr fmt instr = match get_instr_desc instr with
+ | MNoReset _ -> ()
+ | MSetReset inst ->
+ pp_machine_set_reset m self mem fmt inst
+ | MClearReset ->
+ fprintf fmt "%t@,%a"
+ (pp_machine_clear_reset m self mem) pp_label reset_label
+ | MResetAssign b ->
+ pp_reset_assign self fmt b
+ | MLocalAssign (i, v) ->
+ pp_assign m self (pp_c_var_read m) fmt (i, v)
+ | MStateAssign (i, v) ->
+ pp_assign m self (pp_c_var_read m) fmt (i, v)
+ | MStep ([i0], i, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (i, vl)) i0.var_type) ->
+ pp_machine_instr dependencies m self mem fmt
+ (update_instr_desc instr (MLocalAssign (i0, mk_val (Fun (i, vl)) i0.var_type)))
+ | MStep (il, i, vl) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
+ pp_instance_call m self mem fmt i vl il
+ | MStep ([i0], i, vl) when has_c_prototype i dependencies ->
+ fprintf fmt "%a = %s%a;"
+ (pp_c_val m self (pp_c_var_read m)) (mk_val (Var i0) i0.var_type)
+ i
+ (pp_print_parenthesized (pp_c_val m self (pp_c_var_read m))) vl
+ | MStep (il, i, vl) ->
+ let td, _ = List.assoc i m.minstances in
+ if Arrow.td_is_arrow td then
+ pp_arrow_call m self mem fmt i il
+ else
+ pp_basic_instance_call m self mem fmt i vl il
+ | MBranch (_, []) ->
+ eprintf "internal error: C_backend_src.pp_machine_instr %a@."
+ (pp_instr m) instr;
+ assert false
+ | MBranch (g, hl) ->
+ if let t = fst (List.hd hl) in t = tag_true || t = tag_false
+ then (* boolean case, needs special treatment in C because truth value is not unique *)
+ (* may disappear if we optimize code by replacing last branch test with default *)
+ let tl = try List.assoc tag_true hl with Not_found -> [] in
+ let el = try List.assoc tag_false hl with Not_found -> [] in
+ let no_noreset = List.filter (fun i -> match i.instr_desc with
+ | MNoReset _ -> false
+ | _ -> true)
+ in
+ pp_conditional dependencies m self mem fmt g
+ (no_noreset tl) (no_noreset el)
+ else (* enum type case *)
+ (*let g_typ = Typing.type_const Location.dummy_loc (Const_tag (fst (List.hd hl))) in*)
+ fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]"
+ (pp_c_val m self (pp_c_var_read m)) g
+ (pp_print_list ~pp_open_box:pp_open_vbox0
+ (pp_machine_branch dependencies m self mem)) hl
+ | MSpec s ->
+ fprintf fmt "@[/*@@ %s */@]@ " s
+ | MComment s ->
+ fprintf fmt "/*%s*/@ " s
+ in
+ fprintf fmt "%a%a" pp_instr instr (Mod.pp_step_instr_spec m self mem) instr
+
+ and pp_machine_branch dependencies m self mem fmt (t, h) =
fprintf fmt "@[<v 2>case %a:@,%a@,break;@]"
pp_c_tag t
(pp_print_list ~pp_open_box:pp_open_vbox0
- (pp_machine_instr dependencies m self)) h
+ (pp_machine_instr dependencies m self mem)) h
- 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"
- (pp_machine_instr dependencies m self) instr
- (Mod.pp_step_instr_spec m self) instr
+ (* let pp_machine_nospec_instr dependencies m self fmt instr =
+ * pp_machine_instr dependencies m self fmt instr
+ *
+ * let pp_machine_step_instr dependencies m self mem fmt instr =
+ * fprintf fmt "%a%a"
+ * (pp_machine_instr dependencies m self) instr
+ * (Mod.pp_step_instr_spec m self mem) instr *)
(********************************************************************************************)
(* C file Printing functions *)
@@ -414,7 +395,7 @@ module Main = functor (Mod: MODIFIERS_SRC) -> struct
?(mpfr_locals=[])
?(pp_check=pp_print_nothing) ?(checks=[])
?(pp_extra=pp_print_nothing)
- ?(pp_instr=fun fmt _ _ -> pp_print_nothing fmt ()) ?(instrs=[])
+ ?(pp_instr=fun fmt _ -> pp_print_nothing fmt ()) ?(instrs=[])
fmt =
fprintf fmt
"%a@[<v 2>%a {@,\
@@ -444,7 +425,7 @@ module Main = functor (Mod: MODIFIERS_SRC) -> struct
(* check assertions *)
(pp_print_list pp_check) checks
(* instrs *)
- (pp_print_list_i
+ (pp_print_list
~pp_open_box:pp_open_vbox0
~pp_epilogue:pp_print_cut
pp_instr) instrs
@@ -478,7 +459,7 @@ module Main = functor (Mod: MODIFIERS_SRC) -> struct
~mpfr_locals:m.mstep.step_locals
~pp_check:(pp_c_check m self)
~checks:m.mstep.step_checks
- ~pp_instr:(pp_machine_step_instr dependencies m self)
+ ~pp_instr:(pp_machine_instr dependencies m self self)
~instrs:m.mstep.step_instrs
fmt
else
@@ -500,28 +481,30 @@ module Main = functor (Mod: MODIFIERS_SRC) -> struct
~mpfr_locals:m.mstep.step_locals
~pp_check:(pp_c_check m self)
~checks:m.mstep.step_checks
- ~pp_instr:(pp_machine_step_instr dependencies m self)
+ ~pp_instr:(pp_machine_instr dependencies m self self)
~instrs:m.mstep.step_instrs
fmt
- let print_clear_reset_code machines dependencies self mem fmt m =
+ let print_clear_reset_code dependencies self mem fmt m =
pp_print_function
- ~pp_spec:(fun fmt () -> Mod.pp_clear_reset_spec fmt machines self mem m)
+ ~pp_spec:(fun fmt () -> Mod.pp_clear_reset_spec fmt 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)
- ~pp_instr:(pp_machine_nospec_instr dependencies m self)
- ~instrs:m.minit
+ ~pp_instr:(pp_machine_instr dependencies m self mem)
+ ~instrs:[mk_branch
+ (mk_val ResetFlag Type_predef.type_bool)
+ ["true", mkinstr (MResetAssign false) :: m.minit]]
fmt
- let print_set_reset_code self mem fmt m =
+ let print_set_reset_code dependencies 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)
+ ~pp_instr:(pp_machine_instr dependencies m self mem)
+ ~instrs:[mkinstr (MResetAssign true)]
fmt
let print_init_code self fmt m =
@@ -541,7 +524,7 @@ module Main = functor (Mod: MODIFIERS_SRC) -> struct
pp_print_list
~pp_open_box:pp_open_vbox0
~pp_epilogue:pp_print_cut
- (pp_machine_init m self)
+ (pp_machine_init m self self)
fmt minit)
fmt
@@ -561,7 +544,7 @@ module Main = functor (Mod: MODIFIERS_SRC) -> struct
pp_print_list
~pp_open_box:pp_open_vbox0
~pp_epilogue:pp_print_cut
- (pp_machine_clear m self)
+ (pp_machine_clear m self self)
fmt minit)
fmt
@@ -582,7 +565,7 @@ module Main = functor (Mod: MODIFIERS_SRC) -> struct
~mpfr_locals:m.mstep.step_locals
~pp_check:(pp_c_check m self)
~checks:m.mstep.step_checks
- ~pp_instr:(pp_machine_step_instr dependencies m self)
+ ~pp_instr:(pp_machine_instr dependencies m self mem)
~instrs:m.mstep.step_instrs
fmt
else
@@ -605,7 +588,7 @@ module Main = functor (Mod: MODIFIERS_SRC) -> struct
~mpfr_locals:m.mstep.step_locals
~pp_check:(pp_c_check m self)
~checks:m.mstep.step_checks
- ~pp_instr:(pp_machine_step_instr dependencies m self)
+ ~pp_instr:(pp_machine_instr dependencies m self mem)
~instrs:m.mstep.step_instrs
fmt
@@ -754,8 +737,8 @@ module Main = functor (Mod: MODIFIERS_SRC) -> struct
fprintf fmt "@[<v>%a%a@,@,%a@,@,%a%a@]"
print_alloc_function m
(* Reset functions *)
- (print_clear_reset_code machines dependencies self mem) m
- (print_set_reset_code self mem) m
+ (print_clear_reset_code dependencies self mem) m
+ (print_set_reset_code dependencies self mem) m
(* Step function *)
(print_step_code machines dependencies self mem) m
(print_mpfr_code self) m
diff --git a/src/backends/EMF/EMF_common.ml b/src/backends/EMF/EMF_common.ml
index 38bcb5be..d93bc214 100644
--- a/src/backends/EMF/EMF_common.ml
+++ b/src/backends/EMF/EMF_common.ml
@@ -316,6 +316,9 @@ let rec pp_emf_cst_or_var m fmt v =
fprintf fmt "@]}"
)
| Fun _ -> eprintf "Fun expression should have been normalized: %a@." (pp_val m) v ; assert false (* Invalid argument *)
+ | ResetFlag ->
+ (* TODO: handle reset flag *)
+ assert false
and pp_emf_cst_or_var_list m =
Utils.fprintf_list ~sep:",@ " (pp_emf_cst_or_var m)
diff --git a/src/backends/Horn/horn_backend_printers.ml b/src/backends/Horn/horn_backend_printers.ml
index 4fe13f20..de903a39 100644
--- a/src/backends/Horn/horn_backend_printers.ml
+++ b/src/backends/Horn/horn_backend_printers.ml
@@ -163,6 +163,9 @@ let rec pp_horn_val ?(is_lhs=false) m self pp_var fmt v =
pp_var fmt (rename_machine self v)
| Fun (n, vl) -> fprintf fmt "%a" (pp_basic_lib_fun n (pp_horn_val m self pp_var)) vl
+ | ResetFlag ->
+ (* TODO: handle reset flag *)
+ assert false
(* Prints a [value] indexed by the suffix list [loop_vars] *)
let rec pp_value_suffix m self pp_value fmt value =
@@ -295,6 +298,8 @@ 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 reset flag *)
+ | MResetAssign _ -> reset_instances
(* TODO: handle clear_reset *)
| MClearReset -> reset_instances
| MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
diff --git a/src/machine_code.ml b/src/machine_code.ml
index b840e6b7..3b10b974 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -161,7 +161,7 @@ let rec translate_act env (y, expr) =
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' ~lustre_eq var_x hl,
mk_branch_tr var_x spec_hl
| _ ->
let e = translate_expr expr in
diff --git a/src/machine_code_common.ml b/src/machine_code_common.ml
index 47fa5d8c..30e1a871 100644
--- a/src/machine_code_common.ml
+++ b/src/machine_code_common.ml
@@ -34,6 +34,7 @@ let rec pp_val m fmt v =
| 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 (pp_print_parenthesized pp_val) vl
+ | ResetFlag -> fprintf fmt "RESET"
module PrintSpec = struct
@@ -120,6 +121,7 @@ let rec pp_instr m fmt i =
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
+ | MResetAssign b -> fprintf fmt "RESET := %a" pp_print_bool b
| 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
@@ -312,7 +314,10 @@ 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)) *)
- (MBranch (vdecl_to_val c, br))
+ (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
diff --git a/src/machine_code_common.mli b/src/machine_code_common.mli
index 0655bc63..54466603 100644
--- a/src/machine_code_common.mli
+++ b/src/machine_code_common.mli
@@ -12,7 +12,8 @@ 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 -> Lustre_types.var_decl -> (Lustre_types.label * Machine_code_types.instr_t list) 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
diff --git a/src/machine_code_types.ml b/src/machine_code_types.ml
index 7cdfc1fe..297d25ee 100644
--- a/src/machine_code_types.ml
+++ b/src/machine_code_types.ml
@@ -15,6 +15,7 @@ and value_t_desc =
| Array of value_t list
| Access of value_t * value_t
| Power of value_t * value_t
+ | ResetFlag
type mc_formula_t = value_t formula_t
@@ -28,6 +29,7 @@ type instr_t =
and instr_t_desc =
| MLocalAssign of var_decl * value_t
| MStateAssign of var_decl * value_t
+ | MResetAssign of bool
| MClearReset
| MSetReset of ident
| MNoReset of ident
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index b79835ab..fee43707 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -33,6 +33,7 @@ let rec eliminate m elim instr =
| MSetReset _
| MNoReset _
| MClearReset
+ | MResetAssign _
| MSpec _
| MComment _ -> instr
| MStep (il, i, vl) -> update_instr_desc instr (MStep(il, i, List.map e_expr vl))
@@ -58,7 +59,7 @@ and eliminate_expr m elim expr =
| Array(vl) -> {expr with value_desc = Array(List.map (eliminate_expr elim) vl)}
| Access(v1, v2) -> { expr with value_desc = Access(eliminate_expr elim v1, eliminate_expr elim v2)}
| Power(v1, v2) -> { expr with value_desc = Power(eliminate_expr elim v1, eliminate_expr elim v2)}
- | Cst _ -> expr
+ | Cst _ | ResetFlag -> expr
let eliminate_dim elim dim =
Dimension.expr_replace_expr
@@ -74,9 +75,13 @@ let eliminate_dim elim dim =
let unfold_expr_offset m offset expr =
List.fold_left
- (fun res -> (function | Index i -> mk_val (Access (res, value_of_dimension m i))
- (Types.array_element_type res.value_type)
- | Field _ -> Format.eprintf "internal error: not yet implemented !"; assert false))
+ (fun res -> function
+ | Index i ->
+ mk_val (Access (res, value_of_dimension m i))
+ (Types.array_element_type res.value_type)
+ | Field _ ->
+ Format.eprintf "internal error: not yet implemented !";
+ assert false)
expr offset
let rec simplify_cst_expr m offset typ cst =
@@ -104,6 +109,7 @@ let simplify_expr_offset m expr =
| _ , Var _ -> unfold_expr_offset m offset expr
| _ , Cst cst -> simplify_cst_expr m offset expr.value_type cst
| _ , Access (expr, i) -> simplify (Index (dimension_of_value i) :: offset) expr
+ | _ , ResetFlag -> expr
| [] , _ -> expr
| Index _ :: q, Power (expr, _) -> simplify q expr
| Index i :: q, Array vl when Dimension.is_dimension_const i
@@ -120,6 +126,7 @@ let rec simplify_instr_offset m instr =
| MSetReset _
| MNoReset _
| MClearReset
+ | MResetAssign _
| MSpec _
| MComment _ -> instr
| MStep (outputs, id, inputs) -> update_instr_desc instr (MStep (outputs, id, List.map (simplify_expr_offset m) inputs))
@@ -493,7 +500,7 @@ and instrs_remove_skip instrs cont =
let rec value_replace_var fvar value =
match value.value_desc with
- | Cst _ -> value
+ | Cst _ | ResetFlag -> value
| Var v -> { value with value_desc = Var (fvar v) }
| Fun (id, args) -> { value with value_desc = Fun (id, List.map (value_replace_var fvar) args) }
| Array vl -> { value with value_desc = Array (List.map (value_replace_var fvar) vl)}
@@ -507,6 +514,7 @@ let rec instr_replace_var fvar instr cont =
| MSetReset _
| MNoReset _
| MClearReset
+ | MResetAssign _
| 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
--
GitLab