diff options
Diffstat (limited to 'backend/CSE.v')
-rw-r--r-- | backend/CSE.v | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/backend/CSE.v b/backend/CSE.v index ecfa1f9e..2827161d 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 @@ -534,14 +536,14 @@ 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 |