Project

General

Profile

« Previous | Next » 

Revision 6d1693b9

Added by LĂ©lio Brun 7 months ago

work on spec generation almost done

View differences:

src/optimize_machine.ml
28 28
let rec eliminate m elim instr =
29 29
  let e_expr = eliminate_expr m elim in
30 30
  match get_instr_desc instr with
31
  | MSpec _ | MComment _         -> instr
32 31
  | MLocalAssign (i,v) -> update_instr_desc instr (MLocalAssign (i, e_expr v))
33 32
  | MStateAssign (i,v) -> update_instr_desc instr (MStateAssign (i, e_expr v))
34
  | MReset _           -> instr
35
  | MNoReset _         -> instr
33
  | MSetReset _
34
  | MNoReset _
35
  | MClearReset
36
  | MSpec _
37
  | MComment _         -> instr
36 38
  | MStep (il, i, vl)  -> update_instr_desc instr (MStep(il, i, List.map e_expr vl))
37 39
  | MBranch (g,hl)     -> 
38 40
     update_instr_desc instr (
......
115 117
  match get_instr_desc instr with
116 118
  | MLocalAssign (v, expr) -> update_instr_desc instr (MLocalAssign (v, simplify_expr_offset m expr))
117 119
  | MStateAssign (v, expr) -> update_instr_desc instr (MStateAssign (v, simplify_expr_offset m expr))
118
  | MReset _               -> instr
119
  | MNoReset _             -> instr
120
  | MSetReset _
121
  | MNoReset _
122
  | MClearReset
123
  | MSpec _
124
  | MComment _             -> instr
120 125
  | MStep (outputs, id, inputs) -> update_instr_desc instr (MStep (outputs, id, List.map (simplify_expr_offset m) inputs))
121 126
  | MBranch (cond, brl)
122 127
    -> update_instr_desc instr (
123 128
      MBranch(simplify_expr_offset m cond, List.map (fun (l, il) -> l, simplify_instrs_offset m il) brl)
124 129
    )
125
  | MSpec _ | MComment _             -> instr
126 130

  
127 131
and simplify_instrs_offset m instrs =
128 132
  List.map (simplify_instr_offset m) instrs
......
284 288
  let lustre_eq = mkeq loc ([const.const_id], mkexpr loc (Expr_const const.const_value)) in
285 289
  mkinstr
286 290
    ~lustre_eq
287
    True
288 291
    (MLocalAssign (vdecl, mk_val (Cst const.const_value) vdecl.var_type))
289 292

  
290 293
(* We do not perform this optimization on contract nodes since there
......
499 502

  
500 503
let rec instr_replace_var fvar instr cont =
501 504
  match get_instr_desc instr with
502
  | MSpec _ | MComment _          -> instr_cons instr cont
503 505
  | MLocalAssign (i, v) -> instr_cons (update_instr_desc instr (MLocalAssign (fvar i, value_replace_var fvar v))) cont
504 506
  | MStateAssign (i, v) -> instr_cons (update_instr_desc instr (MStateAssign (i, value_replace_var fvar v))) cont
505
  | MReset _            -> instr_cons instr cont
506
  | MNoReset _          -> instr_cons instr cont
507
  | MSetReset _
508
  | MNoReset _
509
  | MClearReset
510
  | MSpec _
511
  | MComment _          -> instr_cons instr cont
507 512
  | MStep (il, i, vl)   -> instr_cons (update_instr_desc instr (MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl))) cont
508 513
  | MBranch (g, hl)     -> instr_cons (update_instr_desc instr (MBranch (value_replace_var fvar g, List.map (fun (h, il) -> (h, instrs_replace_var fvar il [])) hl))) cont
509 514

  
......
763 768
  in
764 769

  
765 770

  
766
  prog, List.rev machine_code  
771
  prog, machine_code
767 772

  
768 773
          
769 774
                 (* Local Variables: *)

Also available in: Unified diff