diff options
| -rw-r--r-- | mppa_k1c/SelectOp.vp | 9 | ||||
| -rw-r--r-- | mppa_k1c/SelectOpproof.v | 38 | ||||
| -rw-r--r-- | test/monniaux/ternary_builtin/ternary_builtin.c | 7 |
3 files changed, 54 insertions, 0 deletions
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index d01b7616..13650a2c 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -285,6 +285,15 @@ Nondetfunction or (e1: expr) (e2: expr) := && Int.eq zero1 Int.zero then Eop Oselect (v0:::v1:::y0:::Enil) else Eop Oor (e1:::e2:::Enil) + | (Eop Oand ((Eop Oneg ((Eop (Ocmp (Ccompuimm Ceq zero0)) + (y0:::Enil)):::Enil)):::v0:::Enil)), + (Eop Oand ((Eop Oneg ((Eop (Ocmp (Ccompuimm Cne zero1)) + (y1:::Enil)):::Enil)):::v1:::Enil)) => + if same_expr_pure y0 y1 + && Int.eq zero0 Int.zero + && Int.eq zero1 Int.zero + then Eop Oselect (v0:::v1:::y0:::Enil) + else Eop Oor (e1:::e2:::Enil) | _, _ => Eop Oor (e1:::e2:::Enil) end. diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 8f8e5b67..d35c4b6d 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -600,6 +600,44 @@ Proof. rewrite Int.and_zero. rewrite Int.or_zero. reflexivity. + - (* select unsigned *) + destruct (same_expr_pure y0 y1) eqn:PURE; simpl; try exact DEFAULT. + predSpec Int.eq Int.eq_spec zero0 Int.zero; simpl; try exact DEFAULT. + predSpec Int.eq Int.eq_spec zero1 Int.zero; simpl; try exact DEFAULT. + TrivialExists. + simpl in *. + unfold select. + f_equal. + inv H6. + inv H7. + inv H9. + inv H11. + unfold same_expr_pure in PURE. + destruct y0; try congruence. + destruct y1; try congruence. + destruct (ident_eq i i0); try congruence. + rewrite <- e0 in *. clear e0. clear PURE. + inv H2. inv H5. + replace v8 with v4 in * by congruence. + rename v4 into vselect. + destruct vselect; simpl; trivial. + rewrite (Val.and_commut _ v5). + destruct v5; simpl; trivial. + rewrite (Val.and_commut _ v9). + rewrite Val.or_commut. + destruct v9; simpl; trivial. + rewrite int_eq_commut. + destruct (Int.eq i1 Int.zero); simpl. + + rewrite Int.and_zero. + rewrite Int.or_commut. + rewrite Int.or_zero. + rewrite Int.and_mone. + reflexivity. + + rewrite Int.and_mone. + rewrite Int.neg_zero. + rewrite Int.and_zero. + rewrite Int.or_zero. + reflexivity. - apply DEFAULT. Qed. diff --git a/test/monniaux/ternary_builtin/ternary_builtin.c b/test/monniaux/ternary_builtin/ternary_builtin.c new file mode 100644 index 00000000..0267fea5 --- /dev/null +++ b/test/monniaux/ternary_builtin/ternary_builtin.c @@ -0,0 +1,7 @@ +int ternary_signed(int x, int v0, int v1) { + return ((-(x==0)) & v0) | ((-(x!=0)) & v1); +} + +int ternary_unsigned(unsigned x, int v0, int v1) { + return ((-(x==0)) & v0) | ((-(x!=0)) & v1); +} |