diff options
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/Machregs.v | 2 | ||||
| -rw-r--r-- | mppa_k1c/SelectLong.vp | 8 | ||||
| -rw-r--r-- | mppa_k1c/SelectLongproof.v | 4 |
3 files changed, 13 insertions, 1 deletions
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index 9f0f6a4d..25048809 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -210,7 +210,7 @@ Global Opaque Definition two_address_op (op: operation) : bool := match op with - | Ocast32unsigned | Omadd | Omaddimm _ => true + | Ocast32unsigned | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ => true | _ => false end. diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp index 07ebf1a2..3a17ab17 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -88,6 +88,14 @@ Nondetfunction addl (e1: expr) (e2: expr) := addlimm n1 (Eop Oaddl (t1:::t2:::Enil)) | t1, Eop (Oaddlimm n2) (t2:::Enil) => addlimm n2 (Eop Oaddl (t1:::t2:::Enil)) + | t1, (Eop Omull (t2:::t3:::Enil)) => + Eop Omaddl (t1:::t2:::t3:::Enil) + | (Eop Omull (t2:::t3:::Enil)), t1 => + Eop Omaddl (t1:::t2:::t3:::Enil) + | t1, (Eop (Omullimm n) (t2:::Enil)) => + Eop (Omaddlimm n) (t1:::t2:::Enil) + | (Eop (Omullimm n) (t2:::Enil)), t1 => + Eop (Omaddlimm n) (t1:::t2:::Enil) | _, _ => Eop Oaddl (e1:::e2:::Enil) end. diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v index 27681875..4723278a 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -185,6 +185,10 @@ Proof. with (Val.addl (Val.addl x v1) (Vlong n2)). apply eval_addlimm. EvalOp. repeat rewrite Val.addl_assoc. reflexivity. + - subst. TrivialExists. + - subst. rewrite Val.addl_commut. TrivialExists. + - subst. TrivialExists. + - subst. rewrite Val.addl_commut. TrivialExists. - TrivialExists. Qed. |