diff options
Diffstat (limited to 'riscV/Op.v')
| -rw-r--r-- | riscV/Op.v | 536 |
1 files changed, 529 insertions, 7 deletions
@@ -50,7 +50,24 @@ 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 signed *) + | CEbnew (optR0: option bool) (**r branch-if-not-equal signed *) + | CEbequw (optR0: option bool) (**r branch-if-equal unsigned *) + | CEbneuw (optR0: option bool) (**r branch-if-not-equal unsigned *) + | 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 signed *) + | CEbnel (optR0: option bool) (**r branch-if-not-equal signed *) + | CEbequl (optR0: option bool) (**r branch-if-equal unsigned *) + | CEbneul (optR0: option bool) (**r branch-if-not-equal unsigned *) + | 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 +170,37 @@ Inductive operation : Type := | Osingleoflong (**r [rd = float32_of_signed_long(r1)] *) | 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] signed *) + | OEsnew (optR0: option bool) (**r [rd <- rs1 != rs2] signed *) + | OEsequw (optR0: option bool) (**r [rd <- rs1 == rs2] unsigned *) + | OEsneuw (optR0: option bool) (**r [rd <- rs1 != rs2] unsigned *) + | OEsltw (optR0: option bool) (**r set-less-than *) + | OEsltuw (optR0: option bool) (**r set-less-than unsigned *) + | OEsltiw (n: int) (**r set-less-than immediate *) + | OEsltiuw (n: int) (**r set-less-than unsigned immediate *) + | OExoriw (n: int) (**r xor immediate *) + | OEluiw (n: int) (is_long: bool) (**r load upper-immediate *) + | OEaddiwr0 (n: int) (is_long: bool) (**r add immediate *) + | OEseql (optR0: option bool) (**r [rd <- rs1 == rs2] signed *) + | OEsnel (optR0: option bool) (**r [rd <- rs1 != rs2] signed *) + | OEsequl (optR0: option bool) (**r [rd <- rs1 == rs2] unsigned *) + | OEsneul (optR0: option bool) (**r [rd <- rs1 != rs2] unsigned *) + | OEsltl (optR0: option bool) (**r set-less-than *) + | OEsltul (optR0: option bool) (**r set-less-than unsigned *) + | OEsltil (n: int64) (**r set-less-than immediate *) + | OEsltiul (n: int64) (**r set-less-than unsigned immediate *) + | OExoril (n: int64) (**r xor immediate *) + | OEluil (n: int64) (**r load upper-immediate *) + | OEaddilr0 (n: int64) (**r add immediate *) + | OEloadli (n: int64) (**r load an immediate int64 *) + | OEfeqd (**r compare equal *) + | OEfltd (**r compare less-than *) + | OEfled (**r compare less-than/equal *) + | OEfeqs (**r compare equal *) + | OEflts (**r compare less-than *) + | OEfles. (**r compare less-than/equal *) | Ocmp (cond: condition) (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) | Obits_of_single | Obits_of_float @@ -172,9 +220,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}. @@ -185,8 +234,9 @@ Defined. Definition eq_operation: forall (x y: operation), {x=y} + {x<>y}. Proof. - generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition; intros. + generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition bool_dec; intros. decide equality. + all: destruct optR0, optR1; decide equality. Defined. (* Alternate definition: @@ -209,6 +259,34 @@ Global Opaque eq_condition eq_addressing eq_operation. to lists of values. Return [None] when the computation can trigger an error, e.g. integer division by zero. [eval_condition] returns a boolean, [eval_operation] and [eval_addressing] return a value. *) + +Definition zero32 := (Vint Int.zero). +Definition zero64 := (Vlong Int64.zero). + +Definition apply_bin_r0 {B} (optR0: option bool) (sem: val -> val -> B) (v1 v2 vz: val): B := + match optR0 with + | None => sem v1 v2 + | Some true => sem vz v1 + | Some false => sem v1 vz + end. + +Definition may_undef_int (is_long: bool) (sem: val -> val -> val) (v1 vimm vz: val): val := + if negb is_long then + match v1 with + | Vint _ => sem vimm vz + | _ => Vundef + end + else + match v1 with + | Vlong _ => sem vimm vz + | _ => Vundef + end. + +Definition may_undef_luil (v1: val) (n: int64): val := + match v1 with + | Vlong _ => Vlong (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12))) + | _ => Vundef + end. Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool := match cond, vl with @@ -224,6 +302,23 @@ 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.cmp_bool Ceq) v1 v2 zero32 + | CEbnew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmp_bool Cne) v1 v2 zero32 + | CEbequw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero32 + | CEbneuw 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.cmpl_bool Ceq) v1 v2 zero64 + | CEbnel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpl_bool Cne) v1 v2 zero64 + | CEbequl optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero64 + | CEbneul 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. @@ -328,6 +423,36 @@ Definition eval_operation | Osingle_of_bits, v1::nil => Some (ExtValues.single_of_bits v1) | Ofloat_of_bits, v1::nil => Some (ExtValues.float_of_bits 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.cmp Ceq) v1 v2 zero32) + | OEsnew optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmp Cne) v1 v2 zero32) + | OEsequw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Ceq) v1 v2 zero32) + | OEsneuw 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) + | OEsltuw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Clt) v1 v2 zero32) + | OEsltiw n, v1::nil => Some (Val.cmp Clt v1 (Vint n)) + | OEsltiuw n, v1::nil => Some (Val.cmpu (Mem.valid_pointer m) Clt v1 (Vint n)) + | OExoriw n, v1::nil => Some (Val.xor v1 (Vint n)) + | OEluiw n is_long, v1::nil => Some (may_undef_int is_long Val.shl v1 (Vint n) (Vint (Int.repr 12))) + | OEaddiwr0 n is_long, v1::nil => Some (may_undef_int is_long Val.add v1 (Vint n) zero32) + | OEseql optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Ceq) v1 v2 zero64)) + | OEsnel optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Cne) v1 v2 zero64)) + | OEsequl optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Ceq) v1 v2 zero64)) + | OEsneul optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Cne) v1 v2 zero64)) + | OEsltl optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Clt) v1 v2 zero64)) + | OEsltul optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Clt) v1 v2 zero64)) + | OEsltil n, v1::nil => Some (Val.maketotal (Val.cmpl Clt v1 (Vlong n))) + | OEsltiul n, v1::nil => Some (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt v1 (Vlong n))) + | OExoril n, v1::nil => Some (Val.xorl v1 (Vlong n)) + | OEluil n, v1::nil => Some (may_undef_luil v1 n) + | OEaddilr0 n, v1::nil => Some (may_undef_int true Val.addl v1 (Vlong n) zero64) + | OEloadli n, nil => Some (Vlong n) + | OEfeqd, v1::v2::nil => Some (Val.cmpf Ceq v1 v2) + | OEfltd, v1::v2::nil => Some (Val.cmpf Clt v1 v2) + | OEfled, v1::v2::nil => Some (Val.cmpf Cle v1 v2) + | OEfeqs, v1::v2::nil => Some (Val.cmpfs Ceq v1 v2) + | OEflts, v1::v2::nil => Some (Val.cmpfs Clt v1 v2) + | OEfles, v1::v2::nil => Some (Val.cmpfs Cle v1 v2) | Oselectl, vb::vt::vf::nil => Some (Val.normalize (ExtValues.select01_long vb vt vf) Tlong) | _, _ => None end. @@ -388,6 +513,22 @@ 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 + | CEbequw _ => Tint :: Tint :: nil + | CEbneuw _ => 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 + | CEbequl _ => Tlong :: Tlong :: nil + | CEbneul _ => 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 := @@ -485,6 +626,35 @@ Definition type_of_operation (op: operation) : list typ * typ := | Osingleoflong => (Tlong :: nil, Tsingle) | Osingleoflongu => (Tlong :: nil, Tsingle) | Ocmp c => (type_of_condition c, Tint) + | OEseqw _ => (Tint :: Tint :: nil, Tint) + | OEsnew _ => (Tint :: Tint :: nil, Tint) + | OEsequw _ => (Tint :: Tint :: nil, Tint) + | OEsneuw _ => (Tint :: Tint :: nil, Tint) + | OEsltw _ => (Tint :: Tint :: nil, Tint) + | OEsltuw _ => (Tint :: Tint :: nil, Tint) + | OEsltiw _ => (Tint :: nil, Tint) + | OEsltiuw _ => (Tint :: nil, Tint) + | OExoriw _ => (Tint :: nil, Tint) + | OEluiw _ _ => (Tint :: nil, Tint) + | OEaddiwr0 _ _ => (Tint :: nil, Tint) + | OEseql _ => (Tlong :: Tlong :: nil, Tint) + | OEsnel _ => (Tlong :: Tlong :: nil, Tint) + | OEsequl _ => (Tlong :: Tlong :: nil, Tint) + | OEsneul _ => (Tlong :: Tlong :: nil, Tint) + | OEsltl _ => (Tlong :: Tlong :: nil, Tint) + | OEsltul _ => (Tlong :: Tlong :: nil, Tint) + | OEsltil _ => (Tlong :: nil, Tint) + | OEsltiul _ => (Tlong :: nil, Tint) + | OExoril _ => (Tlong :: nil, Tlong) + | OEluil _ => (Tlong :: nil, Tlong) + | OEaddilr0 _ => (Tlong :: nil, Tlong) + | OEloadli _ => (nil, Tlong) + | OEfeqd => (Tfloat :: Tfloat :: nil, Tint) + | OEfltd => (Tfloat :: Tfloat :: nil, Tint) + | OEfled => (Tfloat :: Tfloat :: nil, Tint) + | OEfeqs => (Tsingle :: Tsingle :: nil, Tint) + | OEflts => (Tsingle :: Tsingle :: nil, Tint) + | OEfles => (Tsingle :: Tsingle :: nil, Tint) | Obits_of_single => (Tsingle :: nil, Tint) | Obits_of_float => (Tfloat :: nil, Tlong) | Osingle_of_bits => (Tint :: nil, Tsingle) @@ -696,6 +866,86 @@ 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... + (* OEseqw *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmp; + destruct Val.cmp_bool... all: destruct b... + (* OEsnew *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmp; + destruct Val.cmp_bool... all: destruct b... + (* OEsequw *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmpu; + destruct Val.cmpu_bool... all: destruct b... + (* OEsneuw *) + - 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 *) + - unfold may_undef_int; + destruct v0, is_long; simpl; trivial; + destruct (Int.ltu _ _); cbn; trivial. + (* OEaddiwr0 *) + - destruct v0, is_long; simpl; trivial. + (* OEseql *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmpl; + destruct Val.cmpl_bool... all: destruct b... + (* OEsnel *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmpl; + destruct Val.cmpl_bool... all: destruct b... + (* OEsequl *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmplu; + destruct Val.cmplu_bool... all: destruct b... + (* OEsneul *) + - 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 *) + - destruct v0; simpl; trivial. + (* OEaddilr0 *) + - destruct v0; simpl; 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. (* Bits_of_single, float *) - destruct v0; cbn; trivial. - destruct v0; cbn; trivial. @@ -777,6 +1027,22 @@ 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 + | CEbequw optR0 => CEbneuw optR0 + | CEbneuw optR0 => CEbequw 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 + | CEbequl optR0 => CEbneul optR0 + | CEbneul optR0 => CEbequl optR0 + | CEbltl optR0 => CEbgel optR0 + | CEbltul optR0 => CEbgeul optR0 + | CEbgel optR0 => CEbltl optR0 + | CEbgeul optR0 => CEbltul optR0 end. Lemma eval_negate_condition: @@ -796,6 +1062,39 @@ 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_cmp_bool. + repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmp_bool. + 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_cmpl_bool. + repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmpl_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]. *) @@ -892,12 +1191,28 @@ Definition cond_depends_on_memory (cond : condition) : bool := | Ccompuimm _ _ => negb Archi.ptr64 | Ccomplu _ => Archi.ptr64 | Ccompluimm _ _ => Archi.ptr64 + | CEbequw _ => negb Archi.ptr64 + | CEbneuw _ => negb Archi.ptr64 + | CEbltuw _ => negb Archi.ptr64 + | CEbgeuw _ => negb Archi.ptr64 + | CEbequl _ => Archi.ptr64 + | CEbneul _ => Archi.ptr64 + | CEbltul _ => Archi.ptr64 + | CEbgeul _ => Archi.ptr64 | _ => false end. Definition op_depends_on_memory (op: operation) : bool := match op with | Ocmp cmp => cond_depends_on_memory cmp + | OEsequw _ => negb Archi.ptr64 + | OEsneuw _ => negb Archi.ptr64 + | OEsltiuw _ => negb Archi.ptr64 + | OEsltuw _ => negb Archi.ptr64 + | OEsequl _ => Archi.ptr64 + | OEsneul _ => Archi.ptr64 + | OEsltul _ => Archi.ptr64 + | OEsltiul _ => Archi.ptr64 | _ => false end. @@ -921,6 +1236,11 @@ Proof. intros until m2. destruct op; simpl; try congruence. intro DEPEND. f_equal. f_equal. apply cond_depends_on_memory_correct; trivial. + all: intros; repeat (destruct args; auto); + unfold Val.cmpu, Val.cmpu_bool, Val.cmplu, Val.cmplu_bool; + try destruct optR0 as [[]|]; simpl; + destruct v; try destruct v0; simpl; auto; + try apply negb_false_iff in H; try rewrite H; auto. Qed. Lemma cond_valid_pointer_eq: @@ -930,7 +1250,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: @@ -939,8 +1261,11 @@ 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; + erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. Qed. (** Global variables mentioned in an operation or addressing mode *) @@ -1047,6 +1372,88 @@ Ltac InvInject := | _ => idtac end. +Lemma eval_cmpu_bool_inj': forall b c v v' v0 v0', + Val.inject f v v' -> + Val.inject f v0 v0' -> + Val.cmpu_bool (Mem.valid_pointer m1) c v v0 = Some b -> + Val.cmpu_bool (Mem.valid_pointer m2) c v' v0' = Some b. +Proof. + intros. + eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. +Qed. + +Lemma eval_cmpu_bool_inj: forall c v v' v0 v'0, + Val.inject f v v' -> + Val.inject f v0 v'0 -> + Val.inject f (Val.cmpu (Mem.valid_pointer m1) c v v0) + (Val.cmpu (Mem.valid_pointer m2) c v' v'0). +Proof. + intros until v'0. intros HV1 HV2. + unfold Val.cmpu; + destruct (Val.cmpu_bool (Mem.valid_pointer m1) c _ _) eqn:?; eauto. + exploit eval_cmpu_bool_inj'. eapply HV1. eapply HV2. eapply Heqo. + intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. +Qed. + +Lemma eval_cmpu_bool_inj_opt: forall c v v' v0 v'0 optR0, + Val.inject f v v' -> + Val.inject f v0 v'0 -> + Val.inject f (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m1) c) v v0 zero32) + (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m2) c) v' v'0 zero32). +Proof. + intros until optR0. intros HV1 HV2. + destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmpu; + destruct (Val.cmpu_bool (Mem.valid_pointer m1) c _ _) eqn:?; eauto; + assert (HVI: Val.inject f (Vint Int.zero) (Vint Int.zero)) by apply Val.inject_int. + + exploit eval_cmpu_bool_inj'. eapply HVI. eapply HV1. eapply Heqo. + intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. + + exploit eval_cmpu_bool_inj'. eapply HV1. eapply HVI. eapply Heqo. + intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. + + exploit eval_cmpu_bool_inj'. eapply HV1. eapply HV2. eapply Heqo. + intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. +Qed. + +Lemma eval_cmplu_bool_inj': forall b c v v' v0 v0', + Val.inject f v v' -> + Val.inject f v0 v0' -> + Val.cmplu_bool (Mem.valid_pointer m1) c v v0 = Some b -> + Val.cmplu_bool (Mem.valid_pointer m2) c v' v0' = Some b. +Proof. + intros. + eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies. +Qed. + +Lemma eval_cmplu_bool_inj: forall c v v' v0 v'0, + Val.inject f v v' -> + Val.inject f v0 v'0 -> + Val.inject f (Val.maketotal (Val.cmplu (Mem.valid_pointer m1) c v v0)) + (Val.maketotal (Val.cmplu (Mem.valid_pointer m2) c v' v'0)). +Proof. + intros until v'0. intros HV1 HV2. + unfold Val.cmplu; + destruct (Val.cmplu_bool (Mem.valid_pointer m1) c _ _) eqn:?; eauto. + exploit eval_cmplu_bool_inj'. eapply HV1. eapply HV2. eapply Heqo. + intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. +Qed. + +Lemma eval_cmplu_bool_inj_opt: forall c v v' v0 v'0 optR0, + Val.inject f v v' -> + Val.inject f v0 v'0 -> + Val.inject f (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m1) c) v v0 zero64)) + (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m2) c) v' v'0 zero64)). +Proof. + intros until optR0. intros HV1 HV2. + destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmplu; + destruct (Val.cmplu_bool (Mem.valid_pointer m1) c _ _) eqn:?; eauto; + assert (HVI: Val.inject f (Vlong Int64.zero) (Vlong Int64.zero)) by apply Val.inject_long. + + exploit eval_cmplu_bool_inj'. eapply HVI. eapply HV1. eapply Heqo. + intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. + + exploit eval_cmplu_bool_inj'. eapply HV1. eapply HVI. eapply Heqo. + intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. + + exploit eval_cmplu_bool_inj'. eapply HV1. eapply HV2. eapply Heqo. + 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 -> @@ -1054,6 +1461,9 @@ Lemma eval_condition_inj: 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. @@ -1066,6 +1476,38 @@ Proof. - 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 *; + inv H3; inv H2; simpl in H0; inv H0; auto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + 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 *; + inv H3; inv H2; simpl in H0; inv H0; auto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + 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 [[]|]; 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 := @@ -1274,6 +1716,86 @@ Proof. exploit eval_condition_inj; eauto. intros EQ; rewrite EQ. destruct b; simpl; constructor. simpl; constructor. + (* OEseqw *) + - destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmp; + inv H4; inv H2; simpl; try destruct (Int.eq _ _); simpl; cbn; auto; + try apply Val.inject_int. + (* OEsnew *) + - destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmp; + inv H4; inv H2; simpl; try destruct (Int.eq _ _); simpl; cbn; auto; + try apply Val.inject_int. + (* OEsequw *) + - apply eval_cmpu_bool_inj_opt; auto. + (* OEsneuw *) + - 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. + (* OEluiw *) + - unfold may_undef_int; + destruct is_long; + inv H4; simpl; auto; + destruct (Int.ltu _ _); auto. + (* OEaddiwr0 *) + - unfold may_undef_int; + destruct is_long; + inv H4; simpl; auto. + (* OEseql *) + - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmpl; + inv H4; inv H2; simpl; try destruct (Int64.eq _ _); simpl; cbn; auto; + try apply Val.inject_int. + (* OEsnel *) + - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmpl; + inv H4; inv H2; simpl; try destruct (Int64.eq _ _); simpl; cbn; auto; + try apply Val.inject_int. + (* OEsequl *) + - apply eval_cmplu_bool_inj_opt; auto. + (* OEsneul *) + - 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. + (* OEluil *) + - inv H4; simpl; auto. + (* OEaddilr0 *) + - unfold may_undef_int; + 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. (* Bits_of_single, double *) - inv H4; simpl; auto. - inv H4; simpl; auto. @@ -1542,4 +2064,4 @@ Definition builtin_arg_ok match ba with | (BA _ | BA_splitlong (BA _) (BA _)) => true | _ => builtin_arg_ok_1 ba c - end. + end. |