diff options
Diffstat (limited to 'riscV/Op.v')
| -rw-r--r-- | riscV/Op.v | 295 |
1 files changed, 226 insertions, 69 deletions
@@ -49,7 +49,20 @@ Inductive condition : Type := | Ccompf (c: comparison) (**r 64-bit floating-point comparison *) | Cnotcompf (c: comparison) (**r negation of a floating-point comparison *) | Ccompfs (c: comparison) (**r 32-bit floating-point comparison *) - | Cnotcompfs (c: comparison). (**r negation of a floating-point comparison *) + | Cnotcompfs (c: comparison) (**r negation of a floating-point comparison *) + (* Expansed branches *) + | CEbeqw (optR0: option bool) (**r branch-if-equal *) + | CEbnew (optR0: option bool) (**r branch-if-not-equal signed *) + | CEbltw (optR0: option bool) (**r branch-if-less signed *) + | CEbltuw (optR0: option bool) (**r branch-if-less unsigned *) + | CEbgew (optR0: option bool) (**r branch-if-greater-or-equal signed *) + | CEbgeuw (optR0: option bool) (**r branch-if-greater-or-equal unsigned *) + | CEbeql (optR0: option bool) (**r branch-if-equal *) + | CEbnel (optR0: option bool) (**r branch-if-not-equal signed *) + | CEbltl (optR0: option bool) (**r branch-if-less signed *) + | CEbltul (optR0: option bool) (**r branch-if-less unsigned *) + | CEbgel (optR0: option bool) (**r branch-if-greater-or-equal signed *) + | CEbgeul (optR0: option bool). (**r branch-if-greater-or-equal unsigned *) (** Arithmetic and logical operations. In the descriptions, [rd] is the result of the operation and [r1], [r2], etc, are the arguments. *) @@ -153,6 +166,7 @@ Inductive operation : Type := | Osingleoflongu (**r [rd = float32_of_unsigned_int(r1)] *) (*c Boolean tests: *) | Ocmp (cond: condition) (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) + (* Expansed conditions *) | OEseqw (optR0: option bool) (**r [rd <- rs1 == rs2] (pseudo) *) | OEsnew (optR0: option bool) (**r [rd <- rs1 != rs2] (pseudo) *) | OEsltw (optR0: option bool) (**r set-less-than *) @@ -191,9 +205,10 @@ Inductive addressing: Type := Definition eq_condition (x y: condition) : {x=y} + {x<>y}. Proof. - generalize Int.eq_dec Int64.eq_dec; intro. + generalize Int.eq_dec Int64.eq_dec bool_dec; intros. assert (forall (x y: comparison), {x=y}+{x<>y}). decide equality. decide equality. + all: destruct optR0, optR1; decide equality. Defined. Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}. @@ -254,6 +269,19 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool | Cnotcompf c, v1 :: v2 :: nil => option_map negb (Val.cmpf_bool c v1 v2) | Ccompfs c, v1 :: v2 :: nil => Val.cmpfs_bool c v1 v2 | Cnotcompfs c, v1 :: v2 :: nil => option_map negb (Val.cmpfs_bool c v1 v2) + (* Expansed branches *) + | CEbeqw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero32 + | CEbnew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Cne) v1 v2 zero32 + | CEbltw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmp_bool Clt) v1 v2 zero32 + | CEbltuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Clt) v1 v2 zero32 + | CEbgew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmp_bool Cge) v1 v2 zero32 + | CEbgeuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Cge) v1 v2 zero32 + | CEbeql optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero64 + | CEbnel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Cne) v1 v2 zero64 + | CEbltl optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpl_bool Clt) v1 v2 zero64 + | CEbltul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Clt) v1 v2 zero64 + | CEbgel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpl_bool Cge) v1 v2 zero64 + | CEbgeul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Cge) v1 v2 zero64 | _, _ => None end. @@ -354,6 +382,7 @@ Definition eval_operation | Osingleoflong, v1::nil => Some (Val.maketotal (Val.singleoflong v1)) | Osingleoflongu, v1::nil => Some (Val.maketotal (Val.singleoflongu v1)) | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m)) + (* Expansed conditions *) | OEseqw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Ceq) v1 v2 zero32) | OEsnew optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Cne) v1 v2 zero32) | OEsltw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmp Clt) v1 v2 zero32) @@ -438,6 +467,18 @@ Definition type_of_condition (c: condition) : list typ := | Cnotcompf _ => Tfloat :: Tfloat :: nil | Ccompfs _ => Tsingle :: Tsingle :: nil | Cnotcompfs _ => Tsingle :: Tsingle :: nil + | CEbeqw _ => Tint :: Tint :: nil + | CEbnew _ => Tint :: Tint :: nil + | CEbltw _ => Tint :: Tint :: nil + | CEbltuw _ => Tint :: Tint :: nil + | CEbgew _ => Tint :: Tint :: nil + | CEbgeuw _ => Tint :: Tint :: nil + | CEbeql _ => Tlong :: Tlong :: nil + | CEbnel _ => Tlong :: Tlong :: nil + | CEbltl _ => Tlong :: Tlong :: nil + | CEbltul _ => Tlong :: Tlong :: nil + | CEbgel _ => Tlong :: Tlong :: nil + | CEbgeul _ => Tlong :: Tlong :: nil end. Definition type_of_operation (op: operation) : list typ * typ := @@ -766,48 +807,72 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0; cbn; trivial. (* cmp *) - destruct (eval_condition cond vl m)... destruct b... - -- destruct optR0 as [[]|]; simpl; unfold Val.cmpu; - destruct Val.cmpu_bool... all: destruct b... -- destruct optR0 as [[]|]; simpl; unfold Val.cmpu; - destruct Val.cmpu_bool... all: destruct b... -- destruct optR0 as [[]|]; simpl; unfold Val.cmp; - destruct Val.cmp_bool... all: destruct b... -- destruct optR0 as [[]|]; simpl; unfold Val.cmpu; - destruct Val.cmpu_bool... all: destruct b... -- unfold Val.cmp; destruct Val.cmp_bool... - all: destruct b... -- unfold Val.cmpu; destruct Val.cmpu_bool... destruct b... -- destruct v0... -- trivial. -- trivial. -- destruct optR0 as [[]|]; simpl; unfold Val.cmplu; - destruct Val.cmplu_bool... all: destruct b... -- destruct optR0 as [[]|]; simpl; unfold Val.cmplu; - destruct Val.cmplu_bool... all: destruct b... -- destruct optR0 as [[]|]; simpl; unfold Val.cmpl; - destruct Val.cmpl_bool... all: destruct b... -- destruct optR0 as [[]|]; simpl; unfold Val.cmplu; - destruct Val.cmplu_bool... all: destruct b... -- unfold Val.cmpl; destruct Val.cmpl_bool... - all: destruct b... -- unfold Val.cmplu; destruct Val.cmplu_bool... destruct b... -- destruct v0... -- trivial. -- trivial. -- trivial. -- destruct v0; destruct v1; cbn; auto. - destruct Float.cmp; cbn; auto. -- destruct v0; destruct v1; cbn; auto. - destruct Float.cmp; cbn; auto. -- destruct v0; destruct v1; cbn; auto. - destruct Float.cmp; cbn; auto. -- destruct v0; destruct v1; cbn; auto. - destruct Float32.cmp; cbn; auto. -- destruct v0; destruct v1; cbn; auto. - destruct Float32.cmp; cbn; auto. -- destruct v0; destruct v1; cbn; auto. - destruct Float32.cmp; cbn; auto. + (* OEseqw *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmpu; + destruct Val.cmpu_bool... all: destruct b... + (* OEsnew *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmpu; + destruct Val.cmpu_bool... all: destruct b... + (* OEsltw *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmp; + destruct Val.cmp_bool... all: destruct b... + (* OEsltuw *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmpu; + destruct Val.cmpu_bool... all: destruct b... + (* OEsltiw *) + - unfold Val.cmp; destruct Val.cmp_bool... + all: destruct b... + (* OEsltiuw *) + - unfold Val.cmpu; destruct Val.cmpu_bool... destruct b... + (* OExoriw *) + - destruct v0... + (* OEluiw *) + - trivial. + (* OEaddiwr0 *) + - trivial. + (* OEseql *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmplu; + destruct Val.cmplu_bool... all: destruct b... + (* OEsnel *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmplu; + destruct Val.cmplu_bool... all: destruct b... + (* OEsltl *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmpl; + destruct Val.cmpl_bool... all: destruct b... + (* OEsltul *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmplu; + destruct Val.cmplu_bool... all: destruct b... + (* OEsltil *) + - unfold Val.cmpl; destruct Val.cmpl_bool... + all: destruct b... + (* OEsltiul *) + - unfold Val.cmplu; destruct Val.cmplu_bool... destruct b... + (* OExoril *) + - destruct v0... + (* OEluil *) + - trivial. + (* OEaddilr0 *) + - trivial. + (* OEloadli *) + - trivial. + (* OEfeqd *) + - destruct v0; destruct v1; cbn; auto. + destruct Float.cmp; cbn; auto. + (* OEfltd *) + - destruct v0; destruct v1; cbn; auto. + destruct Float.cmp; cbn; auto. + (* OEfled *) + - destruct v0; destruct v1; cbn; auto. + destruct Float.cmp; cbn; auto. + (* OEfeqs *) + - destruct v0; destruct v1; cbn; auto. + destruct Float32.cmp; cbn; auto. + (* OEflts *) + - destruct v0; destruct v1; cbn; auto. + destruct Float32.cmp; cbn; auto. + (* OEfles *) + - destruct v0; destruct v1; cbn; auto. + destruct Float32.cmp; cbn; auto. Qed. (* This should not be simplified to "false" because it breaks proofs elsewhere. *) @@ -877,6 +942,18 @@ Definition negate_condition (cond: condition): condition := | Cnotcompf c => Ccompf c | Ccompfs c => Cnotcompfs c | Cnotcompfs c => Ccompfs c + | CEbeqw optR0 => CEbnew optR0 + | CEbnew optR0 => CEbeqw optR0 + | CEbltw optR0 => CEbgew optR0 + | CEbltuw optR0 => CEbgeuw optR0 + | CEbgew optR0 => CEbltw optR0 + | CEbgeuw optR0 => CEbltuw optR0 + | CEbeql optR0 => CEbnel optR0 + | CEbnel optR0 => CEbeql optR0 + | CEbltl optR0 => CEbgel optR0 + | CEbltul optR0 => CEbgeul optR0 + | CEbgel optR0 => CEbltl optR0 + | CEbgeul optR0 => CEbltul optR0 end. Lemma eval_negate_condition: @@ -896,6 +973,31 @@ Proof. repeat (destruct vl; auto). destruct (Val.cmpf_bool c v v0) as [[]|]; auto. repeat (destruct vl; auto). repeat (destruct vl; auto). destruct (Val.cmpfs_bool c v v0) as [[]|]; auto. + + repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmpu_bool. + repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmpu_bool. + repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmp_bool. + repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmpu_bool. + repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmp_bool. + repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmpu_bool. + repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmplu_bool. + repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmplu_bool. + repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmpl_bool. + repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmplu_bool. + repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmpl_bool. + repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmplu_bool. Qed. (** Shifting stack-relative references. This is used in [Stacking]. *) @@ -992,6 +1094,14 @@ Definition cond_depends_on_memory (cond : condition) : bool := | Ccompuimm _ _ => negb Archi.ptr64 | Ccomplu _ => Archi.ptr64 | Ccompluimm _ _ => Archi.ptr64 + | CEbeqw _ => negb Archi.ptr64 + | CEbnew _ => negb Archi.ptr64 + | CEbltuw _ => negb Archi.ptr64 + | CEbgeuw _ => negb Archi.ptr64 + | CEbeql _ => Archi.ptr64 + | CEbnel _ => Archi.ptr64 + | CEbltul _ => Archi.ptr64 + | CEbgeul _ => Archi.ptr64 | _ => false end. @@ -1043,7 +1153,9 @@ Lemma cond_valid_pointer_eq: Proof. intros until m2. intro MEM. destruct cond eqn:COND; simpl; try congruence. all: repeat (destruct args; simpl; try congruence); - erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. + try destruct optR0 as [[]|]; simpl; + try destruct v, v0; try rewrite !MEM; auto; + try erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. Qed. Lemma op_valid_pointer_eq: @@ -1052,8 +1164,7 @@ Lemma op_valid_pointer_eq: eval_operation ge sp op args m1 = eval_operation ge sp op args m2. Proof. intros until m2. destruct op; simpl; try congruence. - intros MEM; destruct cond; repeat (destruct args; simpl; try congruence); - erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. + intro MEM; erewrite cond_valid_pointer_eq; eauto. all: intros MEM; repeat (destruct args; simpl; try congruence); try destruct optR0 as [[]|]; simpl; try destruct v, v0; try rewrite !MEM; auto; unfold Val.cmpu, Val.cmplu; @@ -1164,27 +1275,6 @@ Ltac InvInject := | _ => idtac end. -Lemma eval_condition_inj: - forall cond vl1 vl2 b, - Val.inject_list f vl1 vl2 -> - eval_condition cond vl1 m1 = Some b -> - eval_condition cond vl2 m2 = Some b. -Proof. - intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto. -- inv H3; inv H2; simpl in H0; inv H0; auto. -- eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. -- inv H3; simpl in H0; inv H0; auto. -- eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. -- inv H3; inv H2; simpl in H0; inv H0; auto. -- eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies. -- inv H3; simpl in H0; inv H0; auto. -- eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies. -- inv H3; inv H2; simpl in H0; inv H0; auto. -- inv H3; inv H2; simpl in H0; inv H0; auto. -- inv H3; inv H2; simpl in H0; inv H0; auto. -- inv H3; inv H2; simpl in H0; inv H0; auto. -Qed. - Lemma eval_cmpu_bool_inj': forall b c v v' v0 v0', Val.inject f v v' -> Val.inject f v0 v0' -> @@ -1267,6 +1357,54 @@ Proof. intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. Qed. +Lemma eval_condition_inj: + forall cond vl1 vl2 b, + Val.inject_list f vl1 vl2 -> + eval_condition cond vl1 m1 = Some b -> + eval_condition cond vl2 m2 = Some b. +Proof. + intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto. + all: assert (HVI32: Val.inject f (Vint Int.zero) (Vint Int.zero)) by apply Val.inject_int; + assert (HVI64: Val.inject f (Vlong Int64.zero) (Vlong Int64.zero)) by apply Val.inject_long; + try unfold zero32, zero64. +- inv H3; inv H2; simpl in H0; inv H0; auto. +- eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. +- inv H3; simpl in H0; inv H0; auto. +- eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. +- inv H3; inv H2; simpl in H0; inv H0; auto. +- eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies. +- inv H3; simpl in H0; inv H0; auto. +- eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies. +- inv H3; inv H2; simpl in H0; inv H0; auto. +- inv H3; inv H2; simpl in H0; inv H0; auto. +- inv H3; inv H2; simpl in H0; inv H0; auto. +- inv H3; inv H2; simpl in H0; inv H0; auto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + eapply eval_cmpu_bool_inj'; eauto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + eapply eval_cmpu_bool_inj'; eauto. +- destruct optR0 as [[]|]; simpl; + inv H3; inv H2; simpl in H0; inv H0; auto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + eapply eval_cmpu_bool_inj'; eauto. +- destruct optR0 as [[]|]; simpl; + inv H3; inv H2; simpl in H0; inv H0; auto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + eapply eval_cmpu_bool_inj'; eauto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + eapply eval_cmplu_bool_inj'; eauto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + eapply eval_cmplu_bool_inj'; eauto. +- destruct optR0 as [[]|]; simpl; + inv H3; inv H2; simpl in H0; inv H0; auto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + eapply eval_cmplu_bool_inj'; eauto. +- destruct optR0 as [[]|]; simpl; + inv H3; inv H2; simpl in H0; inv H0; auto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + eapply eval_cmplu_bool_inj'; eauto. +Qed. + Ltac TrivialExists := match goal with | [ |- exists v2, Some ?v1 = Some v2 /\ Val.inject _ _ v2 ] => @@ -1473,35 +1611,54 @@ Proof. exploit eval_condition_inj; eauto. intros EQ; rewrite EQ. destruct b; simpl; constructor. simpl; constructor. - + (* OEseqw *) - apply eval_cmpu_bool_inj_opt; auto. + (* OEsnew *) - apply eval_cmpu_bool_inj_opt; auto. + (* OEsltw *) - destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmp; inv H4; inv H2; simpl; try destruct (Int.lt _ _); simpl; cbn; auto; try apply Val.inject_int. + (* OEsltuw *) - apply eval_cmpu_bool_inj_opt; auto. + (* OEsltiw *) - inv H4; simpl; cbn; auto; try destruct (Int.lt _ _); apply Val.inject_int. + (* OEsltiuw *) - apply eval_cmpu_bool_inj; auto. + (* OExoriw *) - inv H4; simpl; auto. + (* OEseql *) - apply eval_cmplu_bool_inj_opt; auto. + (* OEsnel *) - apply eval_cmplu_bool_inj_opt; auto. + (* OEsltl *) - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmpl; inv H4; inv H2; simpl; try destruct (Int64.lt _ _); simpl; cbn; auto; try apply Val.inject_int. + (* OEsltul *) - apply eval_cmplu_bool_inj_opt; auto. + (* OEsltil *) - inv H4; simpl; cbn; auto; try destruct (Int64.lt _ _); apply Val.inject_int. + (* OEsltiul *) - apply eval_cmplu_bool_inj; auto. + (* OExoril *) - inv H4; simpl; auto. + (* OEfeqd *) - inv H4; inv H2; cbn; simpl; auto. destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto. + (* OEfltd *) - inv H4; inv H2; cbn; simpl; auto. destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto. + (* OEfled *) - inv H4; inv H2; cbn; simpl; auto. destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto. + (* OEfeqs *) - inv H4; inv H2; cbn; simpl; auto. destruct Float32.cmp; unfold Vtrue, Vfalse; cbn; auto. + (* OEflts *) - inv H4; inv H2; cbn; simpl; auto. destruct Float32.cmp; unfold Vtrue, Vfalse; cbn; auto. + (* OEfles *) - inv H4; inv H2; cbn; simpl; auto. destruct Float32.cmp; unfold Vtrue, Vfalse; cbn; auto. Qed. |