From 43e2036b6f10efdb7e63613067da16fa7fa4b421 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 12 Apr 2019 12:56:12 +0200 Subject: some more simplification --- mppa_k1c/SelectOp.vp | 2 ++ mppa_k1c/SelectOpproof.v | 14 ++++++++++++++ 2 files changed, 16 insertions(+) diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index da0049fe..d5e3ee4a 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -365,7 +365,9 @@ Nondetfunction notint (e: expr) := | Eop Onxor (e1:::e2:::Enil) => Eop Oxor (e1:::e2:::Enil) | Eop (Onxorimm n) (e1:::Enil) => Eop (Oxorimm n) (e1:::Enil) | Eop Oandn (e1:::e2:::Enil) => Eop Oorn (e2:::e1:::Enil) + | Eop (Oandnimm n) (e1:::Enil) => Eop (Oorimm (Int.not n)) (e1:::Enil) | Eop Oorn (e1:::e2:::Enil) => Eop Oandn (e2:::e1:::Enil) + | Eop (Oornimm n) (e1:::Enil) => Eop (Oandimm (Int.not n)) (e1:::Enil) | Eop Onot (e1:::Enil) => e1 | Eop (Ointconst k) Enil => Eop (Ointconst (Int.not k)) Enil | _ => Eop Onot (e:::Enil) diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 49980c51..fe2ff816 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -698,18 +698,32 @@ Proof. - subst x. exists (Val.xor v1 (Vint n)); split; trivial. econstructor. constructor. eassumption. constructor. simpl. reflexivity. + (* andn *) - subst x. TrivialExists. simpl. destruct v0; destruct v1; simpl; trivial. f_equal. f_equal. rewrite Int.not_and_or_not. rewrite Int.not_involutive. apply Int.or_commut. + - subst x. TrivialExists. simpl. + destruct v1; simpl; trivial. + f_equal. f_equal. + rewrite Int.not_and_or_not. + rewrite Int.not_involutive. + reflexivity. + (* orn *) - subst x. TrivialExists. simpl. destruct v0; destruct v1; simpl; trivial. f_equal. f_equal. rewrite Int.not_or_and_not. rewrite Int.not_involutive. apply Int.and_commut. + - subst x. TrivialExists. simpl. + destruct v1; simpl; trivial. + f_equal. f_equal. + rewrite Int.not_or_and_not. + rewrite Int.not_involutive. + reflexivity. - subst x. exists v1; split; trivial. - TrivialExists. - TrivialExists. -- cgit