diff options
Diffstat (limited to 'backend/CSE.v')
| -rw-r--r-- | backend/CSE.v | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/backend/CSE.v b/backend/CSE.v index ecfa1f9e..838d96a6 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -459,8 +459,10 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb before | Iop op args res s => add_op before res op args - | Iload chunk addr args dst s => - add_load before dst chunk addr args + | Iload TRAP chunk addr args dst s => + add_load before dst chunk addr args + | Iload NOTRAP _ _ _ dst _ => + set_unknown before dst | Istore chunk addr args src s => let app := approx!!pc in let n := kill_loads_after_store app before chunk addr args in @@ -491,10 +493,10 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb | _ => empty_numbering end - | EF_vload _ | EF_annot _ _ _ | EF_annot_val _ _ _ | EF_debug _ _ _ => + | EF_vload _ | EF_annot _ _ _ | EF_annot_val _ _ _ | EF_debug _ _ _ | EF_profiling _ _ => set_res_unknown before res end - | Icond cond args ifso ifnot => + | Icond cond args ifso ifnot _ => before | Ijumptable arg tbl => before @@ -534,23 +536,23 @@ Definition transf_instr (n: numbering) (instr: instruction) := let (op', args') := reduce _ combine_op n1 op args vl in Iop op' args' res s end - | Iload chunk addr args dst s => + | Iload TRAP chunk addr args dst s => let (n1, vl) := valnum_regs n args in match find_rhs n1 (Load chunk addr vl) with | Some r => Iop Omove (r :: nil) dst s | None => let (addr', args') := reduce _ combine_addr n1 addr args vl in - Iload chunk addr' args' dst s + Iload TRAP chunk addr' args' dst s end | Istore chunk addr args src s => let (n1, vl) := valnum_regs n args in let (addr', args') := reduce _ combine_addr n1 addr args vl in Istore chunk addr' args' src s - | Icond cond args s1 s2 => + | Icond cond args s1 s2 i => let (n1, vl) := valnum_regs n args in let (cond', args') := reduce _ combine_cond n1 cond args vl in - Icond cond' args' s1 s2 + Icond cond' args' s1 s2 i | _ => instr end. |