diff options
| -rw-r--r-- | ia32/CombineOp.v | 15 | ||||
| -rw-r--r-- | ia32/CombineOpproof.v | 9 |
2 files changed, 0 insertions, 24 deletions
diff --git a/ia32/CombineOp.v b/ia32/CombineOp.v index 61f26e7..1391f55 100644 --- a/ia32/CombineOp.v +++ b/ia32/CombineOp.v @@ -68,21 +68,6 @@ Function combine_addr (addr: addressing) (args: list valnum) : option(addressing Function combine_op (op: operation) (args: list valnum) : option(operation * list valnum) := match op, args with - | Oandimm n, x :: nil => - match get x with - | Some(Op (Oandimm m) ys) => Some(Oandimm (Int.and m n), ys) - | _ => None - end - | Oorimm n, x :: nil => - match get x with - | Some(Op (Oorimm m) ys) => Some(Oorimm (Int.or m n), ys) - | _ => None - end - | Oxorimm n, x :: nil => - match get x with - | Some(Op (Oxorimm m) ys) => Some(Oxorimm (Int.xor m n), ys) - | _ => None - end | Olea addr, _ => match combine_addr addr args with | Some(addr', args') => Some(Olea addr', args') diff --git a/ia32/CombineOpproof.v b/ia32/CombineOpproof.v index c6d2509..2f1fe7b 100644 --- a/ia32/CombineOpproof.v +++ b/ia32/CombineOpproof.v @@ -112,15 +112,6 @@ Theorem combine_op_sound: eval_operation ge sp op' (map valu args') m = eval_operation ge sp op (map valu args) m. Proof. intros. functional inversion H; subst. -(* andimm *) - exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. - rewrite <- H1. rewrite Val.and_assoc. auto. -(* orimm *) - exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. - rewrite <- H1. rewrite Val.or_assoc. auto. -(* xorimm *) - exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. - rewrite <- H1. rewrite Val.xor_assoc. auto. (* lea *) simpl. eapply combine_addr_sound; eauto. (* cmp *) |