diff options
Diffstat (limited to 'backend/Constprop.v')
| -rw-r--r-- | backend/Constprop.v | 23 |
1 files changed, 10 insertions, 13 deletions
diff --git a/backend/Constprop.v b/backend/Constprop.v index cccce9a..e1ab2e9 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -121,26 +121,14 @@ Definition transfer (f: function) (pc: node) (before: D.t) := | None => before | Some i => match i with - | Inop s => - before | Iop op args res s => let a := eval_static_operation op (approx_regs before args) in D.set res a before | Iload chunk addr args dst s => D.set dst Unknown before - | Istore chunk addr args src s => - before | Icall sig ros args res s => D.set res Unknown before - | Itailcall sig ros args => - before -(* - | Ialloc arg res s => - D.set res Unknown before -*) - | Icond cond args ifso ifnot => - before - | Ireturn optarg => + | _ => before end end. @@ -212,6 +200,15 @@ Definition transf_instr (app: D.t) (instr: instruction) := let (cond', args') := cond_strength_reduction (approx_reg app) cond args in Icond cond' args' s1 s2 end + | Ijumptable arg tbl => + match intval (approx_reg app) arg with + | Some n => + match list_nth_z tbl (Int.signed n) with + | Some s => Inop s + | None => instr + end + | None => instr + end | _ => instr end. |