diff options
| -rw-r--r-- | mppa_k1c/SelectLong.vp | 5 | ||||
| -rw-r--r-- | mppa_k1c/SelectLongproof.v | 5 |
2 files changed, 10 insertions, 0 deletions
diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp index dbd14b99..07ebf1a2 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -238,6 +238,7 @@ Nondetfunction andlimm (n1: int64) (e2: expr) := longconst (Int64.and n1 n2) | Eop (Oandlimm n2) (t2:::Enil) => Eop (Oandlimm (Int64.and n1 n2)) (t2:::Enil) + | Eop Onotl (t2:::Enil) => Eop (Oandnlimm n1) (t2:::Enil) | _ => Eop (Oandlimm n1) (e2:::Enil) end. @@ -247,6 +248,8 @@ Nondetfunction andl (e1: expr) (e2: expr) := match e1, e2 with | Eop (Olongconst n1) Enil, t2 => andlimm n1 t2 | t1, Eop (Olongconst n2) Enil => andlimm n2 t1 + | (Eop Onotl (t1:::Enil)), t2 => Eop Oandnl (t1:::t2:::Enil) + | t1, (Eop Onotl (t2:::Enil)) => Eop Oandnl (t2:::t1:::Enil) | _, _ => Eop Oandl (e1:::e2:::Enil) end. @@ -264,6 +267,8 @@ Nondetfunction orl (e1: expr) (e2: expr) := match e1, e2 with | Eop (Olongconst n1) Enil, t2 => orlimm n1 t2 | t1, Eop (Olongconst n2) Enil => orlimm n2 t1 + | (Eop Onotl (t1:::Enil)), t2 => Eop Oornl (t1:::t2:::Enil) + | t1, (Eop Onotl (t2:::Enil)) => Eop Oornl (t2:::t1:::Enil) | _, _ => Eop Oorl (e1:::e2:::Enil) end. diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v index 27052edc..27681875 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -382,6 +382,7 @@ Proof. - econstructor; split. apply eval_longconst. simpl. rewrite Int64.and_commut; auto. - TrivialExists. simpl. rewrite Val.andl_assoc. rewrite Int64.and_commut; auto. - TrivialExists. +- TrivialExists. Qed. Theorem eval_andl: binary_constructor_sound andl Val.andl. @@ -390,6 +391,8 @@ Proof. red; intros. destruct (andl_match a b). - InvEval. rewrite Val.andl_commut. apply eval_andlimm; auto. - InvEval. apply eval_andlimm; auto. +- (*andn*) InvEval. TrivialExists. simpl. congruence. +- (*andn reverse*) InvEval. rewrite Val.andl_commut. TrivialExists; simpl. congruence. - TrivialExists. Qed. @@ -413,6 +416,8 @@ Proof. destruct (orl_match a b). - InvEval. rewrite Val.orl_commut. apply eval_orlimm; auto. - InvEval. apply eval_orlimm; auto. +- (*orn*) InvEval. TrivialExists; simpl; congruence. +- (*orn reversed*) InvEval. rewrite Val.orl_commut. TrivialExists; simpl; congruence. - TrivialExists. Qed. |