From b7720bc5973e9890e7c320bb34b784e2e2b2da69 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 9 Apr 2021 11:02:52 +0200 Subject: Removing addptrofs draft, next will be merging --- riscV/Op.v | 171 ++++++++++++++++++++----------------------------------------- 1 file changed, 55 insertions(+), 116 deletions(-) (limited to 'riscV/Op.v') diff --git a/riscV/Op.v b/riscV/Op.v index 9d1826ac..9f94828f 100644 --- a/riscV/Op.v +++ b/riscV/Op.v @@ -42,8 +42,7 @@ Set Implicit Arguments. Inductive oreg: Type := | X0_L: oreg - | X0_R: oreg - | SP_S: oreg. + | X0_R: oreg. Inductive condition : Type := | Ccomp (c: comparison) (**r signed integer comparison *) @@ -187,7 +186,6 @@ Inductive operation : Type := (*c Boolean tests: *) | Ocmp (cond: condition) (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) (* Expansed conditions *) - | OEmoveSP | OEseqw (optR: option oreg) (**r [rd <- rs1 == rs2] signed *) | OEsnew (optR: option oreg) (**r [rd <- rs1 != rs2] signed *) | OEsequw (optR: option oreg) (**r [rd <- rs1 == rs2] unsigned *) @@ -281,12 +279,11 @@ Global Opaque eq_condition eq_addressing eq_operation. Definition zero32 := (Vint Int.zero). Definition zero64 := (Vlong Int64.zero). -Definition apply_bin_oreg {B} (optR: option oreg) (sem: val -> val -> B) (v1 v2 vz sp: val): B := +Definition apply_bin_oreg {B} (optR: option oreg) (sem: val -> val -> B) (v1 v2 vz: val): B := match optR with | None => sem v1 v2 | Some X0_L => sem vz v1 | Some X0_R => sem v1 vz - | Some SP_S => sem v1 sp end. (** Mayundef evaluation according to the above defined type *) @@ -337,22 +334,22 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool | 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 optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Ceq) v1 v2 zero32 Vundef - | CEbnew optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Cne) v1 v2 zero32 Vundef - | CEbequw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero32 Vundef - | CEbneuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Cne) v1 v2 zero32 Vundef - | CEbltw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Clt) v1 v2 zero32 Vundef - | CEbltuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Clt) v1 v2 zero32 Vundef - | CEbgew optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Cge) v1 v2 zero32 Vundef - | CEbgeuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Cge) v1 v2 zero32 Vundef - | CEbeql optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Ceq) v1 v2 zero64 Vundef - | CEbnel optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Cne) v1 v2 zero64 Vundef - | CEbequl optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero64 Vundef - | CEbneul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Cne) v1 v2 zero64 Vundef - | CEbltl optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Clt) v1 v2 zero64 Vundef - | CEbltul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Clt) v1 v2 zero64 Vundef - | CEbgel optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Cge) v1 v2 zero64 Vundef - | CEbgeul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Cge) v1 v2 zero64 Vundef + | CEbeqw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Ceq) v1 v2 zero32 + | CEbnew optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Cne) v1 v2 zero32 + | CEbequw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero32 + | CEbneuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Cne) v1 v2 zero32 + | CEbltw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Clt) v1 v2 zero32 + | CEbltuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Clt) v1 v2 zero32 + | CEbgew optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Cge) v1 v2 zero32 + | CEbgeuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Cge) v1 v2 zero32 + | CEbeql optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Ceq) v1 v2 zero64 + | CEbnel optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Cne) v1 v2 zero64 + | CEbequl optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero64 + | CEbneul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Cne) v1 v2 zero64 + | CEbltl optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Clt) v1 v2 zero64 + | CEbltul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Clt) v1 v2 zero64 + | CEbgel optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Cge) v1 v2 zero64 + | CEbgeul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Cge) v1 v2 zero64 | _, _ => None end. @@ -466,41 +463,32 @@ Definition eval_operation | Ofloat_of_bits, v1::nil => Some (ExtValues.float_of_bits v1) | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m)) (* Expansed conditions *) - | OEmoveSP, nil => Some (get_sp sp) - | OEseqw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Ceq) v1 v2 zero32 Vundef) - | OEsnew optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Cne) v1 v2 zero32 Vundef) - | OEsequw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Ceq) v1 v2 zero32 Vundef) - | OEsneuw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Cne) v1 v2 zero32 Vundef) - | OEsltw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Clt) v1 v2 zero32 Vundef) - | OEsltuw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Clt) v1 v2 zero32 Vundef) + | OEseqw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Ceq) v1 v2 zero32) + | OEsnew optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Cne) v1 v2 zero32) + | OEsequw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Ceq) v1 v2 zero32) + | OEsneuw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Cne) v1 v2 zero32) + | OEsltw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Clt) v1 v2 zero32) + | OEsltuw optR, v1::v2::nil => Some (apply_bin_oreg optR (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, nil => Some (Val.shl (Vint n) (Vint (Int.repr 12))) - | OEaddiw optR n, nil => Some (apply_bin_oreg optR Val.add (Vint n) Vundef zero32 Vundef) - | OEaddiw ((Some SP_S) as optR) n, v1::nil => - let sp' := Val.add (Vint n) (get_sp sp) in - Some (apply_bin_oreg optR Val.add v1 Vundef Vundef sp') - | OEaddiw optR n, v1::nil => - Some (apply_bin_oreg optR Val.add v1 (Vint n) Vundef (get_sp sp)) + | OEaddiw optR n, nil => Some (apply_bin_oreg optR Val.add (Vint n) Vundef zero32) + | OEaddiw optR n, v1::nil => Some (apply_bin_oreg optR Val.add v1 (Vint n) Vundef) | OEandiw n, v1::nil => Some (Val.and (Vint n) v1) | OEoriw n, v1::nil => Some (Val.or (Vint n) v1) - | OEseql optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Ceq) v1 v2 zero64 Vundef)) - | OEsnel optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Cne) v1 v2 zero64 Vundef)) - | OEsequl optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Ceq) v1 v2 zero64 Vundef)) - | OEsneul optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Cne) v1 v2 zero64 Vundef)) - | OEsltl optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Clt) v1 v2 zero64 Vundef)) - | OEsltul optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Clt) v1 v2 zero64 Vundef)) + | OEseql optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Ceq) v1 v2 zero64)) + | OEsnel optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Cne) v1 v2 zero64)) + | OEsequl optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Ceq) v1 v2 zero64)) + | OEsneul optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Cne) v1 v2 zero64)) + | OEsltl optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Clt) v1 v2 zero64)) + | OEsltul optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (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, nil => Some (Vlong (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12)))) - | OEaddil optR n, nil => Some (apply_bin_oreg optR Val.addl (Vlong n) Vundef zero64 Vundef) - | OEaddil ((Some SP_S) as optR) n, v1::nil => - let sp' := Val.addl (Vlong n) (get_sp sp) in - Some (apply_bin_oreg optR Val.addl v1 Vundef Vundef sp') - | OEaddil optR n, v1::nil => - Some (apply_bin_oreg optR Val.addl v1 (Vlong n) Vundef (get_sp sp)) + | OEaddil optR n, nil => Some (apply_bin_oreg optR Val.addl (Vlong n) Vundef zero64) + | OEaddil optR n, v1::nil => Some (apply_bin_oreg optR Val.addl v1 (Vlong n) Vundef) | OEandil n, v1::nil => Some (Val.andl (Vlong n) v1) | OEoril n, v1::nil => Some (Val.orl (Vlong n) v1) | OEloadli n, nil => Some (Vlong n) @@ -598,14 +586,6 @@ Definition type_of_mayundef mu := | MUshrxl _ => (Tlong :: Tlong :: nil, Tlong) end. -Definition type_addsp (is_long: bool): list typ * typ := - if Archi.ptr64 then ( - if is_long then (Tlong :: nil, Tptr) - else (nil, Tint)) - else ( - if is_long then (nil, Tlong) - else (Tint :: nil, Tptr)). - Definition type_of_operation (op: operation) : list typ * typ := match op with | Omove => (nil, Tint) (* treated specially *) @@ -701,7 +681,6 @@ Definition type_of_operation (op: operation) : list typ * typ := | Osingleoflong => (Tlong :: nil, Tsingle) | Osingleoflongu => (Tlong :: nil, Tsingle) | Ocmp c => (type_of_condition c, Tint) - | OEmoveSP => (nil, Tptr) | OEseqw _ => (Tint :: Tint :: nil, Tint) | OEsnew _ => (Tint :: Tint :: nil, Tint) | OEsequw _ => (Tint :: Tint :: nil, Tint) @@ -713,7 +692,6 @@ Definition type_of_operation (op: operation) : list typ * typ := | OExoriw _ => (Tint :: nil, Tint) | OEluiw _ => (nil, Tint) | OEaddiw None _ => (Tint :: nil, Tint) - | OEaddiw (Some SP_S) _ => type_addsp false | OEaddiw (Some _) _ => (nil, Tint) | OEandiw _ => (Tint :: nil, Tint) | OEoriw _ => (Tint :: nil, Tint) @@ -730,7 +708,6 @@ Definition type_of_operation (op: operation) : list typ * typ := | OExoril _ => (Tlong :: nil, Tlong) | OEluil _ => (nil, Tlong) | OEaddil None _ => (Tlong :: nil, Tlong) - | OEaddil (Some SP_S) _ => type_addsp true | OEaddil (Some _) _ => (nil, Tlong) | OEloadli _ => (nil, Tlong) | OEmayundef mu => type_of_mayundef mu @@ -959,9 +936,6 @@ 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... - (* OEmoveSP *) - - destruct sp; unfold Tptr; destruct Archi.ptr64 eqn:?; - simpl; trivial. (* OEseqw *) - destruct optR as [[]|]; simpl; unfold Val.cmp; destruct Val.cmp_bool... all: destruct b... @@ -986,12 +960,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* OEsltiuw *) - unfold Val.cmpu; destruct Val.cmpu_bool... destruct b... (* OEaddiw *) + - destruct optR as [[]|]; simpl in *; trivial. - destruct optR as [[]|]; simpl in *; trivial; - destruct vl; inv H0; simpl; trivial; - destruct vl; inv H2; simpl; trivial; - destruct v0; simpl; trivial; - destruct (get_sp sp); destruct Archi.ptr64 eqn:HA; simpl; trivial; - unfold type_addsp, Tptr; try rewrite HA; simpl; trivial. + apply type_add. (* OEandiw *) - destruct v0... (* OEoriw *) @@ -1024,12 +995,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* OEsltiul *) - unfold Val.cmplu; destruct Val.cmplu_bool... destruct b... (* OEaddil *) + - destruct optR as [[]|]; simpl in *; trivial. - destruct optR as [[]|]; simpl in *; trivial; - destruct vl; inv H0; simpl; trivial; - destruct vl; inv H2; simpl; trivial; - destruct v0; simpl; trivial; - destruct (get_sp sp); destruct Archi.ptr64 eqn:HA; simpl; trivial; - unfold type_addsp, Tptr; try rewrite HA; simpl; trivial. + apply type_addl. (* OEandil *) - destruct v0... (* OEoril *) @@ -1099,7 +1067,6 @@ Proof. all: try (destruct vl2 as [ | vh3 vl3]; try discriminate). all: try (destruct vl3 as [ | vh4 vl4]; try discriminate). all: try destruct optR as [[]|]; simpl in H0; try discriminate. - all: unfold type_addsp in *; simpl in *. all: try destruct Archi.ptr64; simpl in *; try discriminate. all: try destruct mu; simpl in *; try discriminate. Qed. @@ -1226,9 +1193,6 @@ Definition shift_stack_addressing (delta: Z) (addr: addressing) := Definition shift_stack_operation (delta: Z) (op: operation) := match op with | Oaddrstack ofs => Oaddrstack (Ptrofs.add ofs (Ptrofs.repr delta)) - | OEmoveSP => Oaddrstack (Ptrofs.add Ptrofs.zero (Ptrofs.repr delta)) - | OEaddiw (Some SP_S) n => OEaddiw (Some SP_S) (Ptrofs.to_int (Ptrofs.add (Ptrofs.of_int n) (Ptrofs.repr delta))) - | OEaddil (Some SP_S) n => OEaddil (Some SP_S) (Ptrofs.to_int64 (Ptrofs.add (Ptrofs.of_int64 n) (Ptrofs.repr delta))) | _ => op end. @@ -1260,20 +1224,7 @@ Lemma eval_shift_stack_operation: eval_operation ge (Vptr sp (Ptrofs.repr delta)) op vl m. Proof. intros. destruct op eqn:E; simpl; auto; destruct vl; auto. - - rewrite Ptrofs.add_zero_l, Ptrofs.add_commut; auto. - - rewrite !Ptrofs.add_zero_l; auto. - - destruct optR as [[]|]; simpl; auto. - - destruct vl, optR as [[]|]; auto; unfold apply_bin_oreg; simpl; auto. - destruct v, Archi.ptr64 eqn:EA; simpl; try rewrite EA; simpl; auto. - rewrite Ptrofs.add_zero_l; auto. - rewrite Ptrofs.of_int_to_int; auto. - rewrite (Ptrofs.add_commut (Ptrofs.of_int n) (Ptrofs.repr delta)); reflexivity. - - destruct optR as [[]|]; simpl; auto. - - destruct vl, optR as [[]|]; auto; unfold apply_bin_oreg; simpl; auto. - destruct Archi.ptr64 eqn:EA; auto. - rewrite Ptrofs.add_zero_l; auto. - rewrite Ptrofs.of_int64_to_int64; auto. - rewrite (Ptrofs.add_commut (Ptrofs.of_int64 n) (Ptrofs.repr delta)); reflexivity. + rewrite Ptrofs.add_zero_l, Ptrofs.add_commut; auto. Qed. (** Offset an addressing mode [addr] by a quantity [delta], so that @@ -1533,8 +1484,8 @@ Qed. Lemma eval_cmpu_bool_inj_opt: forall c v v' v0 v'0 optR, Val.inject f v v' -> Val.inject f v0 v'0 -> - Val.inject f (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m1) c) v v0 zero32 Vundef) - (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m2) c) v' v'0 zero32 Vundef). + Val.inject f (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m1) c) v v0 zero32) + (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m2) c) v' v'0 zero32). Proof. intros until optR. intros HV1 HV2. destruct optR as [[]|]; simpl; unfold zero32, Val.cmpu; @@ -1544,11 +1495,9 @@ Proof. 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. do 2 instantiate (1:=Vundef). + + exploit eval_cmpu_bool_inj'. eapply HV1. instantiate (1:=v'0). eauto. 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', @@ -1577,8 +1526,8 @@ Qed. Lemma eval_cmplu_bool_inj_opt: forall c v v' v0 v'0 optR, Val.inject f v v' -> Val.inject f v0 v'0 -> - Val.inject f (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m1) c) v v0 zero64 Vundef)) - (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m2) c) v' v'0 zero64 Vundef)). + Val.inject f (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m1) c) v v0 zero64)) + (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m2) c) v' v'0 zero64)). Proof. intros until optR. intros HV1 HV2. destruct optR as [[]|]; simpl; unfold zero64, Val.cmplu; @@ -1588,11 +1537,9 @@ Proof. 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. do 2 instantiate (1:=Vundef). + + exploit eval_cmplu_bool_inj'. eapply HV1. instantiate (1:=v'0). eauto. 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: @@ -1857,9 +1804,6 @@ Proof. exploit eval_condition_inj; eauto. intros EQ; rewrite EQ. destruct b; simpl; constructor. simpl; constructor. - (* moveSP *) - - unfold get_sp; inv H; auto. - econstructor; eauto. (* OEseqw *) - destruct optR as [[]|]; simpl; unfold zero32, Val.cmp; inv H4; inv H2; simpl; try destruct (Int.eq _ _); simpl; cbn; auto; @@ -1883,14 +1827,11 @@ Proof. (* OEsltiuw *) - apply eval_cmpu_bool_inj; auto. (* OEaddiw *) - - destruct optR as [[]|]; auto; simpl; FuncInv; InvInject; TrivialExists; - try fold (Val.add (Vint n) (get_sp sp1)); - try fold (Val.add (Vint n) (get_sp sp2)); - (*try destruct (get_sp sp1), (get_sp sp2);*) - apply Val.add_inject; auto. - apply Val.add_inject; auto. - destruct sp1, sp2; simpl; auto; - inv H. + - destruct optR as [[]|]; auto; simpl. + rewrite Int.add_zero_l; auto. + rewrite Int.add_commut, Int.add_zero_l; auto. + - destruct optR as [[]|]; auto; simpl; + eapply Val.add_inject; auto. (* OEandiw *) - inv H4; cbn; auto. (* OEoriw *) @@ -1922,13 +1863,11 @@ Proof. (* OEsltiul *) - apply eval_cmplu_bool_inj; auto. (* OEaddil *) - - destruct optR as [[]|]; auto; simpl; FuncInv; InvInject; TrivialExists; - try fold (Val.addl (Vlong n) (get_sp sp1)); - try fold (Val.addl (Vlong n) (get_sp sp2)); - apply Val.addl_inject; auto. - apply Val.addl_inject; auto. - destruct sp1, sp2; simpl; auto; - inv H. + - destruct optR as [[]|]; auto; simpl. + rewrite Int64.add_zero_l; auto. + rewrite Int64.add_commut, Int64.add_zero_l; auto. + - destruct optR as [[]|]; auto; simpl; + eapply Val.addl_inject; auto. (* OEandil *) - inv H4; cbn; auto. (* OEoril *) -- cgit