diff options
Diffstat (limited to 'ia32')
-rw-r--r-- | ia32/PrintAsm.ml | 4 | ||||
-rw-r--r-- | ia32/SelectOp.vp | 84 | ||||
-rw-r--r-- | ia32/SelectOpproof.v | 164 |
3 files changed, 133 insertions, 119 deletions
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 9664be86..a36adb17 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -399,8 +399,8 @@ let print_builtin_vstore_common oc chunk addr src tmp = | Mint32, IR src -> fprintf oc " movl %a, %a\n" ireg src addressing addr | Mfloat32, FR src -> - fprintf oc " cvtsd2ss %a, %%xmm7\n" freg src; - fprintf oc " movss %%xmm7, %a\n" addressing addr + fprintf oc " cvtsd2ss %a, %%xmm7\n" freg src; + fprintf oc " movss %%xmm7, %a\n" addressing addr | (Mfloat64 | Mfloat64al32), FR src -> fprintf oc " movsd %a, %a\n" freg src addressing addr | _ -> diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp index 6d44cf50..7bb2bee6 100644 --- a/ia32/SelectOp.vp +++ b/ia32/SelectOp.vp @@ -74,36 +74,6 @@ Definition addrstack (ofs: int) := Definition notint (e: expr) := Eop (Oxorimm Int.mone) (e ::: Enil). -(** ** Boolean value and boolean negation *) - -Fixpoint boolval (e: expr) {struct e} : expr := - let default := Eop (Ocmp (Ccompuimm Cne Int.zero)) (e ::: Enil) in - match e with - | Eop (Ointconst n) Enil => - Eop (Ointconst (if Int.eq n Int.zero then Int.zero else Int.one)) Enil - | Eop (Ocmp cond) args => - Eop (Ocmp cond) args - | Econdition e1 e2 e3 => - Econdition e1 (boolval e2) (boolval e3) - | _ => - default - end. - -(** ** Boolean negation *) - -Fixpoint notbool (e: expr) {struct e} : expr := - let default := Eop (Ocmp (Ccompuimm Ceq Int.zero)) (e ::: Enil) in - match e with - | Eop (Ointconst n) Enil => - Eop (Ointconst (if Int.eq n Int.zero then Int.one else Int.zero)) Enil - | Eop (Ocmp cond) args => - Eop (Ocmp (negate_condition cond)) args - | Econdition e1 e2 e3 => - Econdition e1 (notbool e2) (notbool e3) - | _ => - default - end. - (** ** Integer addition and pointer addition *) Definition offset_addressing (a: addressing) (ofs: int) : addressing := @@ -368,12 +338,46 @@ Definition divf (e1 e2: expr) := Eop Odivf (e1 ::: e2 ::: Enil). (** ** Comparisons *) +Nondetfunction compimm (default: comparison -> int -> condition) + (sem: comparison -> int -> int -> bool) + (c: comparison) (e1: expr) (n2: int) := + match c, e1 with + | c, Eop (Ointconst n1) Enil => + Eop (Ointconst (if sem c n1 n2 then Int.one else Int.zero)) Enil + | Ceq, Eop (Ocmp c) el => + if Int.eq_dec n2 Int.zero then + Eop (Ocmp (negate_condition c)) el + else if Int.eq_dec n2 Int.one then + Eop (Ocmp c) el + else + Eop (Ointconst Int.zero) Enil + | Cne, Eop (Ocmp c) el => + if Int.eq_dec n2 Int.zero then + Eop (Ocmp c) el + else if Int.eq_dec n2 Int.one then + Eop (Ocmp (negate_condition c)) el + else + Eop (Ointconst Int.one) Enil + | Ceq, Eop (Oandimm n1) (t1 ::: Enil) => + if Int.eq_dec n2 Int.zero then + Eop (Ocmp (Cmaskzero n1)) (t1 ::: Enil) + else + Eop (Ocmp (default c n2)) (e1 ::: Enil) + | Cne, Eop (Oandimm n1) (t1 ::: Enil) => + if Int.eq_dec n2 Int.zero then + Eop (Ocmp (Cmasknotzero n1)) (t1 ::: Enil) + else + Eop (Ocmp (default c n2)) (e1 ::: Enil) + | _, _ => + Eop (Ocmp (default c n2)) (e1 ::: Enil) + end. + Nondetfunction comp (c: comparison) (e1: expr) (e2: expr) := match e1, e2 with | Eop (Ointconst n1) Enil, t2 => - Eop (Ocmp (Ccompimm (swap_comparison c) n1)) (t2 ::: Enil) + compimm Ccompimm Int.cmp (swap_comparison c) t2 n1 | t1, Eop (Ointconst n2) Enil => - Eop (Ocmp (Ccompimm c n2)) (t1 ::: Enil) + compimm Ccompimm Int.cmp c t1 n2 | _, _ => Eop (Ocmp (Ccomp c)) (e1 ::: e2 ::: Enil) end. @@ -381,9 +385,9 @@ Nondetfunction comp (c: comparison) (e1: expr) (e2: expr) := Nondetfunction compu (c: comparison) (e1: expr) (e2: expr) := match e1, e2 with | Eop (Ointconst n1) Enil, t2 => - Eop (Ocmp (Ccompuimm (swap_comparison c) n1)) (t2 ::: Enil) + compimm Ccompuimm Int.cmpu (swap_comparison c) t2 n1 | t1, Eop (Ointconst n2) Enil => - Eop (Ocmp (Ccompuimm c n2)) (t1 ::: Enil) + compimm Ccompuimm Int.cmpu c t1 n2 | _, _ => Eop (Ocmp (Ccompu c)) (e1 ::: e2 ::: Enil) end. @@ -420,17 +424,16 @@ Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil). Definition floatofint (e: expr) := Eop Ofloatofint (e ::: Enil). Definition intuoffloat (e: expr) := - let f := Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil in Elet e (Elet (Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil) - (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil)) + (Econdition (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil) (intoffloat (Eletvar 1)) (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat. Definition floatofintu (e: expr) := let f := Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil in Elet e - (Econdition (CEcond (Ccompuimm Clt Float.ox8000_0000) (Eletvar O ::: Enil)) + (Econdition (Ccompuimm Clt Float.ox8000_0000) (Eletvar O ::: Enil) (floatofint (Eletvar O)) (addf (floatofint (addimm (Int.neg Float.ox8000_0000) (Eletvar O))) f)). @@ -442,10 +445,3 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) := | _ => (Aindexed Int.zero, e:::Enil) end. -(** ** Turning an expression into a condition *) - -Nondetfunction cond_of_expr (e: expr) := - match e with - | Eop (Oandimm n) (t1:::Enil) => (Cmasknotzero n, t1:::Enil) - | _ => (Ccompuimm Cne Int.zero, e:::Enil) - end. diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v index 27d85746..f88f9c00 100644 --- a/ia32/SelectOpproof.v +++ b/ia32/SelectOpproof.v @@ -143,53 +143,6 @@ Proof. unfold notint; red; intros. TrivialExists. Qed. -Theorem eval_boolval: unary_constructor_sound boolval Val.boolval. -Proof. - assert (DFL: - forall le a x, - eval_expr ge sp e m le a x -> - exists v, eval_expr ge sp e m le (Eop (Ocmp (Ccompuimm Cne Int.zero)) (a ::: Enil)) v - /\ Val.lessdef (Val.boolval x) v). - intros. TrivialExists. simpl. destruct x; simpl; auto. - - red. induction a; simpl; intros; eauto. destruct o; eauto. -(* intconst *) - destruct e0; eauto. InvEval. TrivialExists. simpl. destruct (Int.eq i Int.zero); auto. -(* cmp *) - inv H. simpl in H5. - destruct (eval_condition c vl m) as []_eqn. - TrivialExists. simpl. inv H5. rewrite Heqo. destruct b; auto. - simpl in H5. inv H5. - exists Vundef; split; auto. EvalOp; simpl. rewrite Heqo; auto. - -(* condition *) - inv H. destruct v1. - exploit IHa1; eauto. intros [v [A B]]. exists v; split; auto. eapply eval_Econdition; eauto. - exploit IHa2; eauto. intros [v [A B]]. exists v; split; auto. eapply eval_Econdition; eauto. -Qed. - -Theorem eval_notbool: unary_constructor_sound notbool Val.notbool. -Proof. - assert (DFL: - forall le a x, - eval_expr ge sp e m le a x -> - exists v, eval_expr ge sp e m le (Eop (Ocmp (Ccompuimm Ceq Int.zero)) (a ::: Enil)) v - /\ Val.lessdef (Val.notbool x) v). - intros. TrivialExists. simpl. destruct x; simpl; auto. - - red. induction a; simpl; intros; eauto. destruct o; eauto. -(* intconst *) - destruct e0; eauto. InvEval. TrivialExists. simpl. destruct (Int.eq i Int.zero); auto. -(* cmp *) - inv H. simpl in H5. inv H5. - TrivialExists. simpl. rewrite eval_negate_condition. - destruct (eval_condition c vl m); auto. destruct b; auto. -(* condition *) - inv H. destruct v1. - exploit IHa1; eauto. intros [v [A B]]. exists v; split; auto. eapply eval_Econdition; eauto. - exploit IHa2; eauto. intros [v [A B]]. exists v; split; auto. eapply eval_Econdition; eauto. -Qed. - Lemma shift_symbol_address: forall id ofs n, symbol_address ge id (Int.add ofs n) = Val.add (symbol_address ge id ofs) (Vint n). Proof. @@ -604,12 +557,94 @@ Proof. red; intros; TrivialExists. Qed. +Section COMP_IMM. + +Variable default: comparison -> int -> condition. +Variable intsem: comparison -> int -> int -> bool. +Variable sem: comparison -> val -> val -> val. + +Hypothesis sem_int: forall c x y, sem c (Vint x) (Vint y) = Val.of_bool (intsem c x y). +Hypothesis sem_undef: forall c v, sem c Vundef v = Vundef. +Hypothesis sem_eq: forall x y, sem Ceq (Vint x) (Vint y) = Val.of_bool (Int.eq x y). +Hypothesis sem_ne: forall x y, sem Cne (Vint x) (Vint y) = Val.of_bool (negb (Int.eq x y)). +Hypothesis sem_default: forall c v n, sem c v (Vint n) = Val.of_optbool (eval_condition (default c n) (v :: nil) m). + +Lemma eval_compimm: + forall le c a n2 x, + eval_expr ge sp e m le a x -> + exists v, eval_expr ge sp e m le (compimm default intsem c a n2) v + /\ Val.lessdef (sem c x (Vint n2)) v. +Proof. + intros until x. + unfold compimm; case (compimm_match c a); intros. +(* constant *) + InvEval. rewrite sem_int. TrivialExists. simpl. destruct (intsem c0 n1 n2); auto. +(* eq cmp *) + InvEval. inv H. simpl in H5. inv H5. + destruct (Int.eq_dec n2 Int.zero). subst n2. TrivialExists. + simpl. rewrite eval_negate_condition. + destruct (eval_condition c0 vl m); simpl. + unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_eq; auto. + rewrite sem_undef; auto. + destruct (Int.eq_dec n2 Int.one). subst n2. TrivialExists. + simpl. destruct (eval_condition c0 vl m); simpl. + unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_eq; auto. + rewrite sem_undef; auto. + exists (Vint Int.zero); split. EvalOp. + destruct (eval_condition c0 vl m); simpl. + unfold Vtrue, Vfalse. destruct b; rewrite sem_eq; rewrite Int.eq_false; auto. + rewrite sem_undef; auto. +(* ne cmp *) + InvEval. inv H. simpl in H5. inv H5. + destruct (Int.eq_dec n2 Int.zero). subst n2. TrivialExists. + simpl. destruct (eval_condition c0 vl m); simpl. + unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_ne; auto. + rewrite sem_undef; auto. + destruct (Int.eq_dec n2 Int.one). subst n2. TrivialExists. + simpl. rewrite eval_negate_condition. destruct (eval_condition c0 vl m); simpl. + unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_ne; auto. + rewrite sem_undef; auto. + exists (Vint Int.one); split. EvalOp. + destruct (eval_condition c0 vl m); simpl. + unfold Vtrue, Vfalse. destruct b; rewrite sem_ne; rewrite Int.eq_false; auto. + rewrite sem_undef; auto. +(* eq andimm *) + destruct (Int.eq_dec n2 Int.zero). InvEval; subst. + econstructor; split. EvalOp. simpl; eauto. + destruct v1; simpl; try (rewrite sem_undef; auto). rewrite sem_eq. + destruct (Int.eq (Int.and i n1) Int.zero); auto. + TrivialExists. simpl. rewrite sem_default. auto. +(* ne andimm *) + destruct (Int.eq_dec n2 Int.zero). InvEval; subst. + econstructor; split. EvalOp. simpl; eauto. + destruct v1; simpl; try (rewrite sem_undef; auto). rewrite sem_ne. + destruct (Int.eq (Int.and i n1) Int.zero); auto. + TrivialExists. simpl. rewrite sem_default. auto. +(* default *) + TrivialExists. simpl. rewrite sem_default. auto. +Qed. + +Hypothesis sem_swap: + forall c x y, sem (swap_comparison c) x y = sem c y x. + +Lemma eval_compimm_swap: + forall le c a n2 x, + eval_expr ge sp e m le a x -> + exists v, eval_expr ge sp e m le (compimm default intsem (swap_comparison c) a n2) v + /\ Val.lessdef (sem c (Vint n2) x) v. +Proof. + intros. rewrite <- sem_swap. eapply eval_compimm; eauto. +Qed. + +End COMP_IMM. + Theorem eval_comp: forall c, binary_constructor_sound (comp c) (Val.cmp c). Proof. intros; red; intros until y. unfold comp; case (comp_match a b); intros; InvEval. - TrivialExists. simpl. rewrite Val.swap_cmp_bool. auto. - TrivialExists. + eapply eval_compimm_swap; eauto. + intros. unfold Val.cmp. rewrite Val.swap_cmp_bool; auto. + eapply eval_compimm; eauto. TrivialExists. Qed. @@ -617,8 +652,9 @@ Theorem eval_compu: forall c, binary_constructor_sound (compu c) (Val.cmpu (Mem.valid_pointer m) c). Proof. intros; red; intros until y. unfold compu; case (compu_match a b); intros; InvEval. - TrivialExists. simpl. rewrite Val.swap_cmpu_bool. auto. - TrivialExists. + eapply eval_compimm_swap; eauto. + intros. unfold Val.cmpu. rewrite Val.swap_cmpu_bool; auto. + eapply eval_compimm; eauto. TrivialExists. Qed. @@ -628,7 +664,6 @@ Proof. intros; red; intros. unfold compf. TrivialExists. Qed. - Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8). Proof. red; intros. unfold cast8signed. TrivialExists. @@ -695,8 +730,8 @@ Proof. constructor. auto. econstructor. eauto. econstructor. instantiate (1 := Vfloat fm). EvalOp. - apply eval_Econdition with (v1 := Float.cmp Clt f fm). - econstructor. eauto with evalexpr. auto. + eapply eval_Econdition with (vb := Float.cmp Clt f fm). + eauto with evalexpr. auto. destruct (Float.cmp Clt f fm) as []_eqn. exploit Float.intuoffloat_intoffloat_1; eauto. intro EQ. EvalOp. simpl. rewrite EQ; auto. @@ -728,8 +763,8 @@ Proof. set (fm := Float.floatofintu Float.ox8000_0000). assert (eval_expr ge sp e m (Vint i :: le) (Eletvar O) (Vint i)). constructor. auto. - apply eval_Econdition with (v1 := Int.ltu i Float.ox8000_0000). - econstructor. constructor. eauto. constructor. + eapply eval_Econdition with (vb := Int.ltu i Float.ox8000_0000). + constructor. eauto. constructor. simpl. auto. destruct (Int.ltu i Float.ox8000_0000) as []_eqn. rewrite Float.floatofintu_floatofint_1; auto. @@ -758,21 +793,4 @@ Proof. exists (v :: nil); split. constructor; auto. constructor. subst; simpl. rewrite Int.add_zero; auto. Qed. -Theorem eval_cond_of_expr: - forall le a v b, - eval_expr ge sp e m le a v -> - Val.bool_of_val v b -> - match cond_of_expr a with (cond, args) => - exists vl, - eval_exprlist ge sp e m le args vl /\ - eval_condition cond vl m = Some b - end. -Proof. - intros until v. unfold cond_of_expr; case (cond_of_expr_match a); intros; InvEval. - subst v. exists (v1 :: nil); split; auto with evalexpr. - simpl. destruct v1; unfold Val.and in H0; inv H0; auto. - exists (v :: nil); split; auto with evalexpr. - simpl. inv H0; auto. -Qed. - End CMCONSTR. |