Project

General

Profile

« Previous | Next » 

Revision c4780a6a

Added by LĂ©lio Brun 7 months ago

work on new reset functions generation

View differences:

src/backends/C/c_backend_common.ml
298 298
  | Const_string _
299 299
  | Const_modeid _ -> assert false (* string occurs in annotations not in C *)
300 300

  
301
                  
301
let reset_flag_name = "_reset"
302
let pp_reset_flag ?(indirect=true) fmt self =
303
  fprintf fmt "%s%s%s" self (if indirect then "->" else ".") reset_flag_name
304

  
305
let pp_reset_assign self fmt b =
306
  fprintf fmt "%a = %i;"
307
    (pp_reset_flag ~indirect:true) self (if b then 1 else 0)
308

  
302 309
(* Prints a value expression [v], with internal function calls only.
303 310
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
304 311
   but an offset suffix may be added for array variables
......
329 336
       pp_var fmt v
330 337
  | Fun (n, vl) ->
331 338
    pp_basic_lib_fun (Types.is_int_type v.value_type) n pp_c_val fmt vl
339
  | ResetFlag ->
340
    pp_reset_flag fmt self
341

  
332 342

  
333 343
(* Access to the value of a variable:
334 344
   - if it's not a scalar output, then its name is enough
......
472 482
  | Array vl    -> 1 + List.fold_right (fun v -> max (expansion_depth v)) vl 0
473 483
  | Access (v, _) -> max 0 (expansion_depth v - 1)
474 484
  | Power _  -> 0 (*1 + expansion_depth v*)
485
  | ResetFlag -> 0
475 486
and expansion_depth_cst c =
476 487
  match c with
477 488
  | Const_array cl ->
......
604 615
      fprintf fmt "%a%a" pp_var v pp_suffix loop_vars
605 616
  | _, Cst cst ->
606 617
    pp_c_const_suffix var_type fmt cst
618
  | _, ResetFlag ->
619
    pp_reset_flag fmt self
607 620
  | _, _ ->
608 621
    eprintf "internal error: C_backend_src.pp_value_suffix %a %a %a@."
609 622
      Types.print_ty var_type (pp_val m) value pp_suffix loop_vars;
......
676 689
    (pp_machine_memtype_name ~ghost:false) name
677 690

  
678 691
module type MODIFIERS_GHOST_PROTO = sig
679
  val pp_ghost_parameters: formatter -> (string * (formatter -> string -> unit)) list -> unit
692
  val pp_ghost_parameters: ?cut:bool -> formatter -> (string * (formatter -> string -> unit)) list -> unit
680 693
end
681 694

  
682 695
module EmptyGhostProto: MODIFIERS_GHOST_PROTO = struct
683
  let pp_ghost_parameters _ _ = ()
696
  let pp_ghost_parameters ?cut _ _ = ()
684 697
end
685 698

  
686 699
module Protos (Mod: MODIFIERS_GHOST_PROTO) = struct
687 700

  
688 701
  let pp_mem_ghost name fmt mem =
689 702
    pp_machine_decl ~ghost:true
690
      (fun fmt mem -> fprintf fmt "\ghost %a" pp_ptr mem) fmt
703
      (fun fmt mem -> fprintf fmt "\\ghost %a" pp_ptr mem) fmt
691 704
      (name, mem)
692 705

  
693 706
  let print_clear_reset_prototype self mem fmt (name, static) =
......
697 710
         pp_c_decl_input_var) static
698 711
      (pp_machine_memtype_name ~ghost:false) name
699 712
      self
700
      Mod.pp_ghost_parameters [mem, pp_mem_ghost name]
713
      (Mod.pp_ghost_parameters ~cut:true) [mem, pp_mem_ghost name]
701 714

  
702 715
  let print_set_reset_prototype self mem fmt (name, static) =
703 716
    fprintf fmt "@[<v>void %a (%a%a *%s)%a@]"
......
706 719
         pp_c_decl_input_var) static
707 720
      (pp_machine_memtype_name ~ghost:false) name
708 721
      self
709
      Mod.pp_ghost_parameters [mem, pp_mem_ghost name]
722
      (Mod.pp_ghost_parameters ~cut:true) [mem, pp_mem_ghost name]
710 723

  
711 724
  let print_step_prototype self mem fmt (name, inputs, outputs) =
712 725
    fprintf fmt "@[<v>void %a (@[<v>%a%a%a *%s@])%a@]"
......
717 730
         ~pp_epilogue:pp_print_cut pp_c_decl_output_var) outputs
718 731
      (pp_machine_memtype_name ~ghost:false) name
719 732
      self
720
      Mod.pp_ghost_parameters [mem, pp_mem_ghost name]
733
      (Mod.pp_ghost_parameters ~cut:true) [mem, pp_mem_ghost name]
721 734

  
722 735
  let print_init_prototype self fmt (name, static) =
723 736
    fprintf fmt "void %a (%a%a *%s)"
......
879 892
    inout idx;
880 893
  "f_" ^ inout ^ string_of_int idx
881 894

  
895
let pp_basic_assign pp_var fmt typ var_name value =
896
  if Types.is_real_type typ && !Options.mpfr
897
  then
898
    Mpfr.pp_inject_assign pp_var fmt (var_name, value)
899
  else
900
    fprintf fmt "%a = %a;"
901
      pp_var var_name
902
      pp_var value
903

  
904
(* type_directed assignment: array vs. statically sized type
905
   - [var_type]: type of variable to be assigned
906
   - [var_name]: name of variable to be assigned
907
   - [value]: assigned value
908
   - [pp_var]: printer for variables
909
*)
910
let pp_assign m self pp_var fmt (var, value) =
911
  let depth = expansion_depth value in
912
  let var_type = var.var_type in
913
  let var = mk_val (Var var) var_type in
914
  (*eprintf "pp_assign %a %a %a %d@." Types.print_ty var_type pp_val var_name pp_val value depth;*)
915
  let loop_vars = mk_loop_variables m var_type depth in
916
  let reordered_loop_vars = reorder_loop_variables loop_vars in
917
  let rec aux typ fmt vars =
918
    match vars with
919
    | [] ->
920
      pp_basic_assign (pp_value_suffix m self var_type loop_vars pp_var)
921
        fmt typ var value
922
    | (d, LVar i) :: q ->
923
      let typ' = Types.array_element_type typ in
924
      (*eprintf "pp_aux %a %s@." Dimension.pp_dimension d i;*)
925
      fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
926
        i i i pp_c_dimension d i
927
        (aux typ') q
928
    | (d, LInt r) :: q ->
929
      (*eprintf "pp_aux %a %d@." Dimension.pp_dimension d (!r);*)
930
      let typ' = Types.array_element_type typ in
931
      let szl = Utils.enumerate (Dimension.size_const_dimension d) in
932
      fprintf fmt "@[<v 2>{@,%a@]@,}"
933
        (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl
934
    | _ -> assert false
935
  in
936
  begin
937
    reset_loop_counter ();
938
    (*reset_addr_counter ();*)
939
    aux var_type fmt reordered_loop_vars;
940
    (*eprintf "end pp_assign@.";*)
941
  end
882 942

  
883 943
(* Local Variables: *)
884 944
(* compile-command:"make -C ../../.." *)
src/backends/C/c_backend_spec.ml
49 49
let pp_acsl_line pp fmt =
50 50
  fprintf fmt "//%@ @[<h>%a@]" pp
51 51

  
52
let pp_acsl_line' pp fmt =
53
  fprintf fmt "/*%@ @[<h>%a@] */" pp
54

  
55
let pp_acsl_line_cut pp fmt =
56
  fprintf fmt "%a@," (pp_acsl_line pp)
57

  
52 58
let pp_requires pp_req fmt =
53 59
  fprintf fmt "requires %a;" pp_req
54 60

  
......
362 368

  
363 369
  let pp_reg pp_mem fmt = function
364 370
    | ResetFlag ->
365
      fprintf fmt "%t_reset" pp_mem
371
      fprintf fmt "%t%s" pp_mem reset_flag_name
366 372
    | StateVar x ->
367 373
      fprintf fmt "%t%a" pp_mem pp_var_decl x
368 374

  
......
695 701
let pp_at_pre pp_p fmt p =
696 702
  pp_at pp_p fmt (p, label_pre)
697 703

  
698
let pp_register ?(indirect=true) ptr =
704
let pp_register_chain ?(indirect=true) ptr =
699 705
  pp_print_list
700 706
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
701 707
    ~pp_epilogue:(fun fmt () -> fprintf fmt "%s_reg._first"
......
703 709
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
704 710
    (fun fmt (i, _) -> pp_print_string fmt i)
705 711

  
706
let pp_reset_flag ?(indirect=true) ptr fmt mems =
712
let pp_reset_flag_chain ?(indirect=true) ptr fmt mems =
707 713
  pp_print_list
708 714
    ~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
709
    ~pp_epilogue:(fun fmt () -> fprintf fmt "%s_reset"
710
                     (if indirect then "->" else "."))
715
    ~pp_epilogue:(fun fmt () -> pp_reset_flag ~indirect fmt "")
711 716
    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))
712 717
    (fun fmt (i, _) -> pp_print_string fmt i)
713 718
    fmt mems
714 719

  
720
let pp_arrow_reset_ghost mem fmt inst =
721
  fprintf fmt "%s_reset_ghost(%a)" Arrow.arrow_id pp_indirect' (mem, inst)
722

  
715 723
module GhostProto: MODIFIERS_GHOST_PROTO = struct
716
  let pp_ghost_parameters fmt vs =
717
    fprintf fmt "@;%a"
718
      (pp_acsl (pp_ghost (pp_print_parenthesized (fun fmt (x, pp) -> pp fmt x))))
724
  let pp_ghost_parameters ?(cut=true) fmt vs =
725
    fprintf fmt "%a%a"
726
      (if cut then pp_print_cut else pp_print_nothing) ()
727
      (pp_acsl_line'
728
         (pp_ghost
729
            (pp_print_parenthesized (fun fmt (x, pp) -> pp fmt x))))
719 730
      vs
720 731
end
721 732

  
......
763 774
         pp_transition_defs
764 775
         ~pp_epilogue:pp_print_cutcut) machines
765 776

  
766
  let pp_clear_reset_spec fmt machines self mem m =
777
  let pp_clear_reset_spec fmt self mem m =
767 778
    let name = m.mname.node_id in
768 779
    let arws, narws = List.partition (fun (_, (td, _)) -> Arrow.td_is_arrow td)
769 780
        m.minstances in
770 781
    let mk_insts = List.map (fun x -> [x]) in
771 782
    pp_acsl_cut (fun fmt () ->
772 783
        fprintf fmt
773
          "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,\
784
          "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,\
774 785
          @[<v 2>behavior reset:@;\
775 786
          %a@,%a@]@,\
776 787
          @[<v 2>behavior no_reset:@;\
777
          %a@,%a@]"
788
          %a@,%a@]@,\
789
          complete behaviors;@,\
790
          disjoint behaviors;"
778 791
          (pp_requires pp_mem_valid') (name, self)
779 792
          (pp_requires (pp_separated self mem)) (mk_insts m.minstances, [])
793
          (pp_requires (pp_memory_pack_aux pp_ptr pp_print_string))
794
          (name, mem, self)
780 795
          (pp_ensures (pp_memory_pack_aux
781 796
                         ~i:(List.length m.mspec.mmemory_packs - 2)
782 797
                         pp_ptr pp_print_string))
783 798
          (name, mem, self)
784
          (pp_assigns pp_indirect') [self, "_reset"]
785
          (pp_assigns (pp_register self)) (mk_insts arws)
786
          (pp_assigns (pp_reset_flag self)) (mk_insts narws)
787
          (pp_assigns pp_indirect') [mem, "_reset"]
788
          (pp_assigns (pp_register ~indirect:false mem)) (mk_insts arws)
789
          (pp_assigns (pp_reset_flag ~indirect:false mem)) (mk_insts narws)
790
          (pp_assumes (pp_equal pp_indirect' pp_print_int)) ((mem, "_reset"), 1)
799
          (pp_assigns pp_reset_flag) [self]
800
          (pp_assigns (pp_register_chain self)) (mk_insts arws)
801
          (pp_assigns (pp_reset_flag_chain self)) (mk_insts narws)
802
          (pp_assigns pp_reset_flag) [mem]
803
          (pp_assigns (pp_register_chain ~indirect:false mem)) (mk_insts arws)
804
          (pp_assigns (pp_reset_flag_chain ~indirect:false mem)) (mk_insts narws)
805
          (pp_assumes (pp_equal pp_reset_flag pp_print_int)) (mem, 1)
791 806
          (pp_ensures (pp_initialization pp_ptr)) (name, mem)
792
          (pp_assumes (pp_equal pp_indirect' pp_print_int)) ((mem, "_reset"), 0)
807
          (pp_assumes (pp_equal pp_reset_flag pp_print_int)) (mem, 0)
793 808
          (pp_ensures (pp_equal pp_ptr (pp_old pp_ptr))) (mem, mem)
794 809
      )
795 810
      fmt ()
......
800 815
        fprintf fmt
801 816
          "%a@,%a@,%a"
802 817
          (pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string)) (name, mem, self)
803
          (pp_ensures (pp_equal pp_indirect' pp_print_string)) ((mem, "_reset"), "1")
804
          (pp_assigns (fun fmt ptr -> pp_indirect' fmt (ptr, "_reset"))) [self; mem])
818
          (pp_ensures (pp_equal pp_reset_flag pp_print_string)) (mem, "1")
819
          (pp_assigns pp_reset_flag) [self; mem])
805 820
      fmt ()
806 821

  
807 822
  let pp_step_spec fmt machines self mem m =
......
833 848
            (pp_assigns pp_ptr_decl) outputs
834 849
            (pp_assigns (pp_reg self)) m.mmemory
835 850
            (pp_assigns (pp_memory self)) (memories insts')
836
            (pp_assigns (pp_register self)) insts
837
            (pp_assigns (pp_reset_flag self)) insts''
851
            (pp_assigns (pp_register_chain self)) insts
852
            (pp_assigns (pp_reset_flag_chain self)) insts''
838 853
            (pp_assigns (pp_reg mem)) m.mmemory
839 854
            (pp_assigns (pp_memory ~indirect:false mem)) (memories insts')
840
            (pp_assigns (pp_register ~indirect:false mem)) insts
841
            (pp_assigns (pp_reset_flag ~indirect:false mem)) insts''
855
            (pp_assigns (pp_register_chain ~indirect:false mem)) insts
856
            (pp_assigns (pp_reset_flag_chain ~indirect:false mem)) insts''
842 857
            (pp_ensures (pp_transition_aux m (pp_old pp_ptr)
843 858
                           pp_ptr pp_var_decl pp_ptr_decl))
844 859
            (name, inputs, [], outputs, mem, mem)
845 860
      )
846 861
      fmt ()
847 862

  
848
  let pp_step_instr_spec m self fmt instr =
849
    fprintf fmt "@,%a"
850
      (pp_print_list ~pp_open_box:pp_open_vbox0
851
         (pp_acsl (pp_assert (PrintSpec.pp_spec (InstrMode self) m))))
863
  let pp_ghost_instr_code m self fmt instr = match instr.instr_desc with
864
    | MStateAssign (x, v) ->
865
      fprintf fmt "@,%a"
866
        (pp_acsl_line
867
           (pp_ghost
868
              (pp_assign m self (pp_c_var_read m))))
869
        (x, v)
870
    | MResetAssign b ->
871
      fprintf fmt "@,%a"
872
        (pp_acsl_line
873
           (pp_ghost
874
              (pp_reset_assign self)))
875
        b
876
    | MSetReset inst ->
877
      let td, _ = List.assoc inst m.minstances in
878
      if Arrow.td_is_arrow td then
879
         fprintf fmt "@,%a"
880
           (pp_acsl_line
881
              (pp_ghost
882
                 (pp_arrow_reset_ghost self)))
883
           inst
884
    | _ -> ()
885

  
886
  let pp_step_instr_spec m self mem fmt instr =
887
    fprintf fmt "%a%a"
888
      (pp_ghost_instr_code m mem) instr
889
      (pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_prologue:pp_print_cut
890
         (pp_acsl_line' (pp_assert (PrintSpec.pp_spec (InstrMode self) m))))
852 891
      instr.instr_spec
853 892

  
854
  let pp_ghost_set_reset_spec fmt =
855
    fprintf fmt "@;%a@;"
856
      (pp_acsl_line
857
         (pp_ghost
858
            (fun fmt mem -> fprintf fmt "%a = 1;" pp_indirect' (mem, "_reset"))))
893
  let pp_ghost_parameter mem fmt inst =
894
    GhostProto.pp_ghost_parameters ~cut:false fmt
895
      (match inst with
896
       | Some inst ->
897
         [inst, fun fmt inst -> fprintf fmt "&%a" pp_indirect' (mem, inst)]
898
       | None ->
899
         [mem, pp_print_string])
900

  
859 901
end
860 902

  
861 903
(**************************************************************************)
src/backends/C/c_backend_src.ml
20 20
  module GhostProto: MODIFIERS_GHOST_PROTO
21 21
  val pp_predicates: formatter -> machine_t list -> unit
22 22
  val pp_set_reset_spec: formatter -> ident -> ident -> machine_t -> unit
23
  val pp_clear_reset_spec: formatter -> machine_t list -> ident -> ident -> machine_t -> unit
23
  val pp_clear_reset_spec: formatter -> ident -> ident -> machine_t -> unit
24 24
  val pp_step_spec: formatter -> machine_t list -> ident -> ident -> machine_t -> unit
25
  val pp_step_instr_spec: machine_t -> ident -> formatter -> instr_t -> unit
26
  val pp_ghost_set_reset_spec: formatter -> ident -> unit
25
  val pp_step_instr_spec: machine_t -> ident -> ident -> formatter -> instr_t -> unit
26
  val pp_ghost_parameter: ident -> formatter -> ident option -> unit
27 27
end
28 28

  
29 29
module EmptyMod = struct
30 30
  module GhostProto = EmptyGhostProto
31 31
  let pp_predicates _ _ = ()
32 32
  let pp_set_reset_spec _ _ _ _ = ()
33
  let pp_clear_reset_spec _ _ _ _ _ = ()
33
  let pp_clear_reset_spec _ _ _ _ = ()
34 34
  let pp_step_spec _ _ _ _ _ = ()
35
  let pp_step_instr_spec _ _ _ _ = ()
36
  let pp_ghost_set_reset_spec _ _ = ()
35
  let pp_step_instr_spec _ _ _ _ _ = ()
36
  let pp_ghost_parameter _ _ _ = ()
37 37
end
38 38

  
39 39
module Main = functor (Mod: MODIFIERS_SRC) -> struct
......
55 55
  let rec static_loop_profile v =
56 56
    match v.value_desc with
57 57
    | Cst cst  -> static_loop_profile_cst cst
58
    | Var _  -> []
58
    | Var _  | ResetFlag -> []
59 59
    | Fun (_, vl) ->
60 60
      List.fold_right
61 61
        (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) vl []
......
81 81
  let pp_c_val m self pp_var fmt v =
82 82
    pp_value_suffix m self v.value_type [] pp_var fmt v
83 83

  
84
  let pp_basic_assign pp_var fmt typ var_name value =
85
    if Types.is_real_type typ && !Options.mpfr
86
    then
87
      Mpfr.pp_inject_assign pp_var fmt (var_name, value)
88
    else
89
      fprintf fmt "%a = %a;"
90
        pp_var var_name
91
        pp_var value
92

  
93
  (* type_directed assignment: array vs. statically sized type
94
     - [var_type]: type of variable to be assigned
95
     - [var_name]: name of variable to be assigned
96
     - [value]: assigned value
97
     - [pp_var]: printer for variables
98
  *)
99
  let pp_assign m self pp_var fmt var_type var_name value =
100
    let depth = expansion_depth value in
101
    (*eprintf "pp_assign %a %a %a %d@." Types.print_ty var_type pp_val var_name pp_val value depth;*)
102
    let loop_vars = mk_loop_variables m var_type depth in
103
    let reordered_loop_vars = reorder_loop_variables loop_vars in
104
    let rec aux typ fmt vars =
105
      match vars with
106
      | [] ->
107
        pp_basic_assign (pp_value_suffix m self var_type loop_vars pp_var)
108
          fmt typ var_name value
109
      | (d, LVar i) :: q ->
110
        let typ' = Types.array_element_type typ in
111
        (*eprintf "pp_aux %a %s@." Dimension.pp_dimension d i;*)
112
        fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
113
          i i i pp_c_dimension d i
114
          (aux typ') q
115
      | (d, LInt r) :: q ->
116
        (*eprintf "pp_aux %a %d@." Dimension.pp_dimension d (!r);*)
117
        let typ' = Types.array_element_type typ in
118
        let szl = Utils.enumerate (Dimension.size_const_dimension d) in
119
        fprintf fmt "@[<v 2>{@,%a@]@,}"
120
          (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl
121
      | _ -> assert false
122
    in
123
    begin
124
      reset_loop_counter ();
125
      (*reset_addr_counter ();*)
126
      aux var_type fmt reordered_loop_vars;
127
      (*eprintf "end pp_assign@.";*)
128
    end
129

  
130
  let pp_machine_ pp_machine_name fn_name m fmt ?inst self =
131
    let name, static =
84
  let pp_machine_ pp_machine_name fn_name m fmt ?inst self mem =
85
    let name, is_arrow, static =
132 86
      match inst with
133 87
      | Some inst ->
134 88
        let node, static = try List.assoc inst m.minstances with Not_found ->
......
136 90
            fn_name m.mname.node_id self inst;
137 91
          raise Not_found
138 92
        in
139
        node_name node, static
93
        node_name node, Arrow.td_is_arrow node, static
140 94
      | None ->
141
        m.mname.node_id, []
95
        m.mname.node_id, false, []
142 96
    in
143
    fprintf fmt "%a(%a%s%a);"
144
      pp_machine_name name
97
    let is_arrow_reset = is_arrow && fn_name = "pp_machine_set_reset" in
98
    fprintf fmt "%a(%a%s%a)%a;"
99
      (if is_arrow_reset then
100
         (fun fmt -> fprintf fmt "%s_reset")
101
       else
102
         pp_machine_name) name
145 103
      (pp_comma_list ~pp_eol:pp_print_comma Dimension.pp_dimension) static
146 104
      self
147 105
      (pp_print_option (fun fmt -> fprintf fmt "->%s")) inst
106
      (if is_arrow_reset then pp_print_nothing else Mod.pp_ghost_parameter mem)
107
      inst
148 108

  
149
  let pp_machine_set_reset m self fmt inst =
150
    pp_machine_ pp_machine_set_reset_name "pp_machine_set_reset" m fmt ~inst self
109
  let pp_machine_set_reset m self mem fmt inst =
110
    pp_machine_ pp_machine_set_reset_name "pp_machine_set_reset" m fmt ~inst
111
      self mem
151 112

  
152
  let pp_machine_clear_reset m self fmt =
153
    pp_machine_ pp_machine_clear_reset_name "pp_machine_clear_reset" m fmt self
113
  let pp_machine_clear_reset m self mem fmt =
114
    pp_machine_ pp_machine_clear_reset_name "pp_machine_clear_reset" m fmt
115
      self mem
154 116

  
155
  let pp_machine_init m self fmt inst =
156
    pp_machine_ pp_machine_init_name "pp_machine_init" m fmt ~inst self
117
  let pp_machine_init m self mem fmt inst =
118
    pp_machine_ pp_machine_init_name "pp_machine_init" m fmt ~inst self mem
157 119

  
158
  let pp_machine_clear m self fmt inst =
159
    pp_machine_ pp_machine_clear_name "pp_machine_clear" m fmt ~inst self
120
  let pp_machine_clear m self mem fmt inst =
121
    pp_machine_ pp_machine_clear_name "pp_machine_clear" m fmt ~inst self mem
160 122

  
161
  let pp_call m self pp_read pp_write fmt i inputs outputs =
123
  let pp_call m self mem pp_read pp_write fmt i inputs outputs =
162 124
    try (* stateful node instance *)
163 125
      let n, _ = List.assoc i m.minstances in
164
      fprintf fmt "%a(%a%a%s->%s);"
126
      fprintf fmt "%a(%a%a%s->%s)%a;"
165 127
        pp_machine_step_name (node_name n)
166 128
        (pp_comma_list ~pp_eol:pp_print_comma
167 129
           (pp_c_val m self pp_read)) inputs
......
169 131
           pp_write) outputs
170 132
        self
171 133
        i
134
        (Mod.pp_ghost_parameter mem) (Some i)
172 135
    with Not_found -> (* stateless node instance *)
173 136
      let n, _ = List.assoc i m.mcalls in
174 137
      fprintf fmt "%a(%a%a);"
......
177 140
           (pp_c_val m self pp_read)) inputs
178 141
        (pp_comma_list pp_write) outputs
179 142

  
180
  let pp_basic_instance_call m self =
181
    pp_call m self (pp_c_var_read m) (pp_c_var_write m)
143
  let pp_basic_instance_call m self mem =
144
    pp_call m self mem (pp_c_var_read m) (pp_c_var_write m)
182 145

  
183
  let pp_arrow_call m self fmt i outputs =
146
  let pp_arrow_call m self mem fmt i outputs =
184 147
    match outputs with
185 148
    | [x] ->
186
      fprintf fmt "%a = %a(%s->%s);"
149
      fprintf fmt "%a = %a(%s->%s)%a;"
187 150
        (pp_c_var_read m) x
188 151
        pp_machine_step_name Arrow.arrow_id
189 152
        self
190 153
        i
154
        (Mod.pp_ghost_parameter mem) (Some i)
191 155
    | _ -> assert false
192 156

  
193
  let pp_instance_call m self fmt i inputs outputs =
157
  let pp_instance_call m self mem fmt i inputs outputs =
194 158
    let pp_offset pp_var indices fmt var =
195 159
      fprintf fmt "%a%a"
196 160
        pp_var var
......
208 172
      else
209 173
        let pp_read  = pp_offset (pp_c_var_read  m) indices in
210 174
        let pp_write = pp_offset (pp_c_var_write m) indices in
211
        pp_call m self pp_read pp_write fmt i inputs outputs
175
        pp_call m self mem pp_read pp_write fmt i inputs outputs
212 176
    in
213 177
    reset_loop_counter ();
214 178
    aux [] fmt (List.hd inputs).Machine_code_types.value_type
215 179

  
216
  let rec pp_conditional dependencies (m: machine_t) self fmt c tl el =
217
    fprintf fmt "@[<v 2>if (%a) {%a@]@,@[<v 2>} else {%a@]@,}"
218
      (pp_c_val m self (pp_c_var_read m)) c
219
      (pp_print_list ~pp_prologue:pp_print_cut
220
         (pp_machine_instr dependencies m self)) tl
221
      (pp_print_list ~pp_prologue:pp_print_cut
222
         (pp_machine_instr dependencies m self)) el
223

  
224
  and pp_machine_instr dependencies (m: machine_t) self fmt instr =
225
    match get_instr_desc instr with
226
    | MNoReset _ -> ()
227
    | MSetReset inst ->
228
      pp_machine_set_reset m self fmt inst
229
    | MClearReset ->
230
      fprintf fmt "%t@,%a"
231
        (pp_machine_clear_reset m self) pp_label reset_label
232
    | MLocalAssign (i,v) ->
233
      pp_assign
234
        m self (pp_c_var_read m) fmt
235
        i.var_type (mk_val (Var i) i.var_type) v
236
    | MStateAssign (i,v) ->
237
      pp_assign
238
        m self (pp_c_var_read m) fmt
239
        i.var_type (mk_val (Var i) i.var_type) v
240
    | MStep ([i0], i, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (i, vl)) i0.var_type)  ->
241
      pp_machine_instr dependencies m self fmt
242
        (update_instr_desc instr (MLocalAssign (i0, mk_val (Fun (i, vl)) i0.var_type)))
243
    | MStep (il, i, vl) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
244
      pp_instance_call m self fmt i vl il
245
    | MStep ([i0], i, vl) when has_c_prototype i dependencies ->
246
      fprintf fmt "%a = %s%a;"
247
        (pp_c_val m self (pp_c_var_read m)) (mk_val (Var i0) i0.var_type)
248
        i
249
        (pp_print_parenthesized (pp_c_val m self (pp_c_var_read m))) vl
250
    | MStep (il, i, vl) ->
251
      let td, _ = List.assoc i m.minstances in
252
      if Arrow.td_is_arrow td then
253
        pp_arrow_call m self fmt i il
254
      else
255
        pp_basic_instance_call m self fmt i vl il
256
    | MBranch (_, []) ->
257
      eprintf "internal error: C_backend_src.pp_machine_instr %a@."
258
        (pp_instr m) instr;
259
      assert false
260
    | MBranch (g, hl) ->
261
      if let t = fst (List.hd hl) in t = tag_true || t = tag_false
262
      then (* boolean case, needs special treatment in C because truth value is not unique *)
263
        (* may disappear if we optimize code by replacing last branch test with default *)
264
        let tl = try List.assoc tag_true  hl with Not_found -> [] in
265
        let el = try List.assoc tag_false hl with Not_found -> [] in
266
        pp_conditional dependencies m self fmt g tl el
267
      else (* enum type case *)
268
        (*let g_typ = Typing.type_const Location.dummy_loc (Const_tag (fst (List.hd hl))) in*)
269
        fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]"
270
          (pp_c_val m self (pp_c_var_read m)) g
271
          (pp_print_list ~pp_open_box:pp_open_vbox0
272
             (pp_machine_branch dependencies m self)) hl
273
    | MSpec s ->
274
      fprintf fmt "@[/*@@ %s */@]@ " s
275
    | MComment s  ->
276
      fprintf fmt "/*%s*/@ " s
277

  
278
  and pp_machine_branch dependencies m self fmt (t, h) =
180
  let rec pp_conditional dependencies m self mem fmt c tl el =
181
    let pp_machine_instrs =
182
      pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_prologue:pp_print_cut
183
        (pp_machine_instr dependencies m self mem) in
184
    let pp_cond = pp_c_val m self (pp_c_var_read m) in
185
    match tl, el with
186
    | [], _ :: _ ->
187
      fprintf fmt "@[<v 2>if (!%a) {%a@]@,}"
188
        pp_cond c
189
        pp_machine_instrs el
190
    | _, [] ->
191
      fprintf fmt "@[<v 2>if (%a) {%a@]@,}"
192
        pp_cond c
193
        pp_machine_instrs tl
194
    | _, _ ->
195
      fprintf fmt "@[<v 2>if (%a) {%a@]@,@[<v 2>} else {%a@]@,}"
196
        pp_cond c
197
        pp_machine_instrs tl
198
        pp_machine_instrs el
199

  
200
  and pp_machine_instr dependencies m self mem fmt instr =
201
    let pp_instr fmt instr = match get_instr_desc instr with
202
      | MNoReset _ -> ()
203
      | MSetReset inst ->
204
        pp_machine_set_reset m self mem fmt inst
205
      | MClearReset ->
206
        fprintf fmt "%t@,%a"
207
          (pp_machine_clear_reset m self mem) pp_label reset_label
208
      | MResetAssign b ->
209
        pp_reset_assign self fmt b
210
      | MLocalAssign (i, v) ->
211
        pp_assign m self (pp_c_var_read m) fmt (i, v)
212
      | MStateAssign (i, v) ->
213
        pp_assign m self (pp_c_var_read m) fmt (i, v)
214
      | MStep ([i0], i, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (i, vl)) i0.var_type)  ->
215
        pp_machine_instr dependencies m self mem fmt
216
          (update_instr_desc instr (MLocalAssign (i0, mk_val (Fun (i, vl)) i0.var_type)))
217
      | MStep (il, i, vl) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
218
        pp_instance_call m self mem fmt i vl il
219
      | MStep ([i0], i, vl) when has_c_prototype i dependencies ->
220
        fprintf fmt "%a = %s%a;"
221
          (pp_c_val m self (pp_c_var_read m)) (mk_val (Var i0) i0.var_type)
222
          i
223
          (pp_print_parenthesized (pp_c_val m self (pp_c_var_read m))) vl
224
      | MStep (il, i, vl) ->
225
        let td, _ = List.assoc i m.minstances in
226
        if Arrow.td_is_arrow td then
227
          pp_arrow_call m self mem fmt i il
228
        else
229
          pp_basic_instance_call m self mem fmt i vl il
230
      | MBranch (_, []) ->
231
        eprintf "internal error: C_backend_src.pp_machine_instr %a@."
232
          (pp_instr m) instr;
233
        assert false
234
      | MBranch (g, hl) ->
235
        if let t = fst (List.hd hl) in t = tag_true || t = tag_false
236
        then (* boolean case, needs special treatment in C because truth value is not unique *)
237
          (* may disappear if we optimize code by replacing last branch test with default *)
238
          let tl = try List.assoc tag_true  hl with Not_found -> [] in
239
          let el = try List.assoc tag_false hl with Not_found -> [] in
240
          let no_noreset = List.filter (fun i -> match i.instr_desc with
241
              | MNoReset _ -> false
242
              | _ -> true)
243
          in
244
          pp_conditional dependencies m self mem fmt g
245
            (no_noreset tl) (no_noreset el)
246
        else (* enum type case *)
247
          (*let g_typ = Typing.type_const Location.dummy_loc (Const_tag (fst (List.hd hl))) in*)
248
          fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]"
249
            (pp_c_val m self (pp_c_var_read m)) g
250
            (pp_print_list ~pp_open_box:pp_open_vbox0
251
               (pp_machine_branch dependencies m self mem)) hl
252
      | MSpec s ->
253
        fprintf fmt "@[/*@@ %s */@]@ " s
254
      | MComment s  ->
255
        fprintf fmt "/*%s*/@ " s
256
    in
257
    fprintf fmt "%a%a" pp_instr instr (Mod.pp_step_instr_spec m self mem) instr
258

  
259
  and pp_machine_branch dependencies m self mem fmt (t, h) =
279 260
    fprintf fmt "@[<v 2>case %a:@,%a@,break;@]"
280 261
      pp_c_tag t
281 262
      (pp_print_list ~pp_open_box:pp_open_vbox0
282
         (pp_machine_instr dependencies m self)) h
263
         (pp_machine_instr dependencies m self mem)) h
283 264

  
284
  let pp_machine_nospec_instr dependencies m self fmt _i instr =
285
    pp_machine_instr dependencies m self fmt instr
286

  
287
  let pp_machine_step_instr dependencies m self fmt _i instr =
288
    fprintf fmt "%a%a"
289
      (pp_machine_instr dependencies m self) instr
290
      (Mod.pp_step_instr_spec m self) instr
265
  (* let pp_machine_nospec_instr dependencies m self fmt instr =
266
   *   pp_machine_instr dependencies m self fmt instr
267
   *
268
   * let pp_machine_step_instr dependencies m self mem fmt instr =
269
   *   fprintf fmt "%a%a"
270
   *     (pp_machine_instr dependencies m self) instr
271
   *     (Mod.pp_step_instr_spec m self mem) instr *)
291 272

  
292 273
  (********************************************************************************************)
293 274
  (*                         C file Printing functions                                        *)
......
414 395
      ?(mpfr_locals=[])
415 396
      ?(pp_check=pp_print_nothing) ?(checks=[])
416 397
      ?(pp_extra=pp_print_nothing)
417
      ?(pp_instr=fun fmt _ _ -> pp_print_nothing fmt ()) ?(instrs=[])
398
      ?(pp_instr=fun fmt _ -> pp_print_nothing fmt ()) ?(instrs=[])
418 399
      fmt =
419 400
    fprintf fmt
420 401
      "%a@[<v 2>%a {@,\
......
444 425
      (* check assertions *)
445 426
      (pp_print_list pp_check) checks
446 427
      (* instrs *)
447
      (pp_print_list_i
428
      (pp_print_list
448 429
         ~pp_open_box:pp_open_vbox0
449 430
         ~pp_epilogue:pp_print_cut
450 431
         pp_instr) instrs
......
478 459
        ~mpfr_locals:m.mstep.step_locals
479 460
        ~pp_check:(pp_c_check m self)
480 461
        ~checks:m.mstep.step_checks
481
        ~pp_instr:(pp_machine_step_instr dependencies m self)
462
        ~pp_instr:(pp_machine_instr dependencies m self self)
482 463
        ~instrs:m.mstep.step_instrs
483 464
        fmt
484 465
    else
......
500 481
        ~mpfr_locals:m.mstep.step_locals
501 482
        ~pp_check:(pp_c_check m self)
502 483
        ~checks:m.mstep.step_checks
503
        ~pp_instr:(pp_machine_step_instr dependencies m self)
484
        ~pp_instr:(pp_machine_instr dependencies m self self)
504 485
        ~instrs:m.mstep.step_instrs
505 486
        fmt
506 487

  
507
  let print_clear_reset_code machines dependencies self mem fmt m =
488
  let print_clear_reset_code dependencies self mem fmt m =
508 489
    pp_print_function
509
      ~pp_spec:(fun fmt () -> Mod.pp_clear_reset_spec fmt machines self mem m)
490
      ~pp_spec:(fun fmt () -> Mod.pp_clear_reset_spec fmt self mem m)
510 491
      ~pp_prototype:(Protos.print_clear_reset_prototype self mem)
511 492
      ~prototype:(m.mname.node_id, m.mstatic)
512 493
      ~pp_local:(pp_c_decl_local_var m)
513 494
      ~base_locals:(const_locals m)
514
      ~pp_instr:(pp_machine_nospec_instr dependencies m self)
515
      ~instrs:m.minit
495
      ~pp_instr:(pp_machine_instr dependencies m self mem)
496
      ~instrs:[mk_branch
497
                 (mk_val ResetFlag Type_predef.type_bool)
498
                 ["true", mkinstr (MResetAssign false) :: m.minit]]
516 499
      fmt
517 500

  
518
  let print_set_reset_code self mem fmt m =
501
  let print_set_reset_code dependencies self mem fmt m =
519 502
    pp_print_function
520 503
      ~pp_spec:(fun fmt () -> Mod.pp_set_reset_spec fmt self mem m)
521 504
      ~pp_prototype:(Protos.print_set_reset_prototype self mem)
522 505
      ~prototype:(m.mname.node_id, m.mstatic)
523
      ~pp_extra:(fun fmt () -> fprintf fmt "self->_reset = 1;%a"
524
                    Mod.pp_ghost_set_reset_spec mem)
506
      ~pp_instr:(pp_machine_instr dependencies m self mem)
507
      ~instrs:[mkinstr (MResetAssign true)]
525 508
      fmt
526 509

  
527 510
  let print_init_code self fmt m =
......
541 524
          pp_print_list
542 525
            ~pp_open_box:pp_open_vbox0
543 526
            ~pp_epilogue:pp_print_cut
544
            (pp_machine_init m self)
527
            (pp_machine_init m self self)
545 528
            fmt minit)
546 529
      fmt
547 530

  
......
561 544
          pp_print_list
562 545
            ~pp_open_box:pp_open_vbox0
563 546
            ~pp_epilogue:pp_print_cut
564
            (pp_machine_clear m self)
547
            (pp_machine_clear m self self)
565 548
            fmt minit)
566 549
      fmt
567 550

  
......
582 565
        ~mpfr_locals:m.mstep.step_locals
583 566
        ~pp_check:(pp_c_check m self)
584 567
        ~checks:m.mstep.step_checks
585
        ~pp_instr:(pp_machine_step_instr dependencies m self)
568
        ~pp_instr:(pp_machine_instr dependencies m self mem)
586 569
        ~instrs:m.mstep.step_instrs
587 570
        fmt
588 571
    else
......
605 588
        ~mpfr_locals:m.mstep.step_locals
606 589
        ~pp_check:(pp_c_check m self)
607 590
        ~checks:m.mstep.step_checks
608
        ~pp_instr:(pp_machine_step_instr dependencies m self)
591
        ~pp_instr:(pp_machine_instr dependencies m self mem)
609 592
        ~instrs:m.mstep.step_instrs
610 593
        fmt
611 594

  
......
754 737
      fprintf fmt "@[<v>%a%a@,@,%a@,@,%a%a@]"
755 738
        print_alloc_function m
756 739
        (* Reset functions *)
757
        (print_clear_reset_code machines dependencies self mem) m
758
        (print_set_reset_code self mem) m
740
        (print_clear_reset_code dependencies self mem) m
741
        (print_set_reset_code dependencies self mem) m
759 742
        (* Step function *)
760 743
        (print_step_code machines dependencies self mem) m
761 744
        (print_mpfr_code self) m
src/backends/EMF/EMF_common.ml
316 316
     fprintf fmt "@]}"
317 317
  )
318 318
  | Fun _ -> eprintf "Fun expression should have been normalized: %a@." (pp_val m) v ; assert false (* Invalid argument *)
319
  | ResetFlag ->
320
    (* TODO: handle reset flag *)
321
    assert false
319 322

  
320 323
and pp_emf_cst_or_var_list m =
321 324
  Utils.fprintf_list ~sep:",@ " (pp_emf_cst_or_var m)
src/backends/Horn/horn_backend_printers.ml
163 163
       pp_var fmt (rename_machine self v)
164 164
    
165 165
  | Fun (n, vl)   -> fprintf fmt "%a" (pp_basic_lib_fun n (pp_horn_val m self pp_var)) vl
166
  | ResetFlag ->
167
    (* TODO: handle reset flag *)
168
    assert false
166 169

  
167 170
(* Prints a [value] indexed by the suffix list [loop_vars] *)
168 171
let rec pp_value_suffix m self pp_value fmt value =
......
295 298
let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ident list =
296 299
  match get_instr_desc instr with
297 300
  | MSpec _ | MComment _ -> reset_instances
301
  (* TODO: handle reset flag *)
302
  | MResetAssign _ -> reset_instances
298 303
  (* TODO: handle clear_reset *)
299 304
  | MClearReset -> reset_instances
300 305
  | MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
src/machine_code.ml
161 161
        let h, spec_h = translate_act (y, h) in
162 162
        (t, [h]), (t, spec_h))
163 163
        hl)) in
164
    mk_branch ~lustre_eq var_x hl,
164
    mk_branch' ~lustre_eq var_x hl,
165 165
    mk_branch_tr var_x spec_hl
166 166
  | _ ->
167 167
    let e = translate_expr expr in
src/machine_code_common.ml
34 34
  | Access (t, i) -> fprintf fmt "%a[%a]" pp_val t pp_val i
35 35
  | Power (v, n)  -> fprintf fmt "(%a^%a)" pp_val v pp_val n
36 36
  | Fun (n, vl)   -> fprintf fmt "%s%a" n (pp_print_parenthesized pp_val) vl
37
  | ResetFlag     -> fprintf fmt "RESET"
37 38

  
38 39
module PrintSpec = struct
39 40

  
......
120 121
  begin match i.instr_desc with
121 122
    | MLocalAssign (i,v) -> fprintf fmt "%s := %a" i.var_id pp_val v
122 123
    | MStateAssign (i,v) -> fprintf fmt "{%s} := %a" i.var_id pp_val v
124
    | MResetAssign b     -> fprintf fmt "RESET := %a" pp_print_bool b
123 125
    | MSetReset i        -> fprintf fmt "set_reset %s" i
124 126
    | MClearReset        -> fprintf fmt "clear_reset %s" m.mname.node_id
125 127
    | MNoReset i         -> fprintf fmt "noreset %s" i
......
312 314
    (* (And (List.map (fun (l, instrs) ->
313 315
     *      Imply (Equal (Val c, Tag l), And (List.map get_instr_spec instrs)))
314 316
     *      br)) *)
315
    (MBranch (vdecl_to_val c, br))
317
    (MBranch (c, br))
318

  
319
let mk_branch' ?lustre_eq v =
320
  mk_branch ?lustre_eq (vdecl_to_val v)
316 321

  
317 322
let mk_assign ?lustre_eq x v =
318 323
  mkinstr ?lustre_eq
src/machine_code_common.mli
12 12
val vdecls_to_vals: Lustre_types.var_decl list -> Machine_code_types.value_t list
13 13
val id_to_tag: Lustre_types.ident -> Machine_code_types.value_t
14 14
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
15
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
15
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
16
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
16 17
val mk_assign: ?lustre_eq:Lustre_types.eq -> Lustre_types.var_decl -> Machine_code_types.value_t -> Machine_code_types.instr_t
17 18
val empty_machine: Machine_code_types.machine_t
18 19
val arrow_machine: Machine_code_types.machine_t
src/machine_code_types.ml
15 15
  | Array of value_t list
16 16
  | Access of value_t * value_t
17 17
  | Power of value_t * value_t
18
  | ResetFlag
18 19

  
19 20
type mc_formula_t = value_t formula_t
20 21

  
......
28 29
and instr_t_desc =
29 30
  | MLocalAssign of var_decl * value_t
30 31
  | MStateAssign of var_decl * value_t
32
  | MResetAssign of bool
31 33
  | MClearReset
32 34
  | MSetReset of ident
33 35
  | MNoReset of ident
src/optimize_machine.ml
33 33
  | MSetReset _
34 34
  | MNoReset _
35 35
  | MClearReset
36
  | MResetAssign _
36 37
  | MSpec _
37 38
  | MComment _         -> instr
38 39
  | MStep (il, i, vl)  -> update_instr_desc instr (MStep(il, i, List.map e_expr vl))
......
58 59
  | Array(vl) -> {expr with value_desc = Array(List.map (eliminate_expr elim) vl)}
59 60
  | Access(v1, v2) -> { expr with value_desc = Access(eliminate_expr elim v1, eliminate_expr elim v2)}
60 61
  | Power(v1, v2) -> { expr with value_desc = Power(eliminate_expr elim v1, eliminate_expr elim v2)}
61
  | Cst _ -> expr
62
  | Cst _ | ResetFlag -> expr
62 63

  
63 64
let eliminate_dim elim dim =
64 65
  Dimension.expr_replace_expr 
......
74 75

  
75 76
let unfold_expr_offset m offset expr =
76 77
  List.fold_left
77
    (fun res -> (function | Index i -> mk_val (Access (res, value_of_dimension m i))
78
					      (Types.array_element_type res.value_type)
79
                          | Field _ -> Format.eprintf "internal error: not yet implemented !"; assert false))
78
    (fun res -> function
79
       | Index i ->
80
         mk_val (Access (res, value_of_dimension m i))
81
           (Types.array_element_type res.value_type)
82
       | Field _ ->
83
         Format.eprintf "internal error: not yet implemented !";
84
         assert false)
80 85
    expr offset
81 86

  
82 87
let rec simplify_cst_expr m offset typ cst =
......
104 109
    | _           , Var _            -> unfold_expr_offset m offset expr
105 110
    | _           , Cst cst          -> simplify_cst_expr m offset expr.value_type cst
106 111
    | _           , Access (expr, i) -> simplify (Index (dimension_of_value i) :: offset) expr
112
    | _           , ResetFlag        -> expr
107 113
    | []          , _                -> expr
108 114
    | Index _ :: q, Power (expr, _)  -> simplify q expr
109 115
    | Index i :: q, Array vl when Dimension.is_dimension_const i
......
120 126
  | MSetReset _
121 127
  | MNoReset _
122 128
  | MClearReset
129
  | MResetAssign _
123 130
  | MSpec _
124 131
  | MComment _             -> instr
125 132
  | MStep (outputs, id, inputs) -> update_instr_desc instr (MStep (outputs, id, List.map (simplify_expr_offset m) inputs))
......
493 500

  
494 501
let rec value_replace_var fvar value =
495 502
  match value.value_desc with
496
  | Cst _ -> value
503
  | Cst _ | ResetFlag -> value
497 504
  | Var v -> { value with value_desc = Var (fvar v) }
498 505
  | Fun (id, args) -> { value with value_desc = Fun (id, List.map (value_replace_var fvar) args) }
499 506
  | Array vl -> { value with value_desc = Array (List.map (value_replace_var fvar) vl)}
......
507 514
  | MSetReset _
508 515
  | MNoReset _
509 516
  | MClearReset
517
  | MResetAssign _
510 518
  | MSpec _
511 519
  | MComment _          -> instr_cons instr cont
512 520
  | MStep (il, i, vl)   -> instr_cons (update_instr_desc instr (MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl))) cont

Also available in: Unified diff