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/Asmgen.v | 14 ---- riscV/Asmgenproof.v | 2 - riscV/Asmgenproof1.v | 5 +- riscV/ExpansionOracle.ml | 30 -------- riscV/NeedOp.v | 1 - riscV/Op.v | 171 +++++++++++++++------------------------------ riscV/PrintOp.ml | 2 - riscV/RTLpathSE_simplify.v | 35 ---------- riscV/ValueAOp.v | 98 +++++++++++++------------- 9 files changed, 104 insertions(+), 254 deletions(-) (limited to 'riscV') diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index ff5d1a6e..3e84e950 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -212,12 +212,10 @@ Definition apply_bin_oreg_ireg0 (optR: option oreg) (r1 r2: ireg0): (ireg0 * ire | None => (r1, r2) | Some X0_L => (X0, r1) | Some X0_R => (r1, X0) - | Some SP_S => (X SP, r1) end. Definition get_oreg (optR: option oreg) (r: ireg0) := match optR with - | Some SP_S => X SP | Some X0_L | Some X0_R => X0 | _ => r end. @@ -846,12 +844,6 @@ Definition transl_op do rd <- ireg_of res; let rs := get_oreg optR X0 in OK (Paddiw rd rs n :: k) - | OEaddiw (Some SP_S) n, a1 :: nil => - do rd <- ireg_of res; - do rs <- ireg_of a1; - if Int.eq n Int.zero then - OK (Paddw rd SP rs :: k) - else Error (msg "Asmgen.transl_op") | OEaddiw optR n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; @@ -920,12 +912,6 @@ Definition transl_op do rd <- ireg_of res; let rs := get_oreg optR X0 in OK (Paddil rd rs n :: k) - | OEaddil (Some SP_S) n, a1 :: nil => - do rd <- ireg_of res; - do rs <- ireg_of a1; - if Int64.eq n Int64.zero then - OK (Paddl rd SP rs :: k) - else Error (msg "Asmgen.transl_op") | OEaddil optR n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index bf9ede7f..509eac94 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -320,8 +320,6 @@ Opaque Int.eq. - destruct optR as [[]|]; simpl in *; TailNoLabel. - destruct optR as [[]|]; simpl in *; TailNoLabel. - destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. Qed. Remark indexed_memory_access_label: diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index cbe68577..2293e001 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -1274,7 +1274,7 @@ Opaque Int.eq. { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). exists rs'; split. eexact A. eauto with asmgen. } (* Expanded instructions from RTL *) - 8,9,17,18: + 9,10,19,20: econstructor; split; try apply exec_straight_one; simpl; eauto; split; intros; Simpl; try destruct (rs x0); try rewrite Int64.add_commut; @@ -1283,9 +1283,8 @@ Opaque Int.eq. try rewrite Int.and_commut; auto; try rewrite Int64.or_commut; try rewrite Int.or_commut; auto. - 1-14: + 1-16: destruct optR as [[]|]; try discriminate; - try (ArgsInv; simpl in EV; SimplEval EV; try TranslOpSimpl); unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; try inv EQ3; try inv EQ2; try destruct (Int.eq _ _) eqn:A; try inv H0; try destruct (Int64.eq _ _) eqn:A; try inv H1; diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index b54bd5e1..092bf0d1 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -606,31 +606,6 @@ let expanse_cbranch_fp vn cnot fn_cond cmp f1 f2 info succ1 succ2 = Sfinalcond (CEbnew (Some X0_R), [ r'; r' ], succ1, succ2, info) :: l else Sfinalcond (CEbeqw (Some X0_R), [ r'; r' ], succ1, succ2, info) :: l -let addptrofs vn n dest = - if Ptrofs.eq_dec n Ptrofs.zero then [ addinst vn OEmoveSP [] dest ] - else if Archi.ptr64 then - match make_immed64 (Ptrofs.to_int64 n) with - | Imm64_single imm -> [ addinst vn (OEaddil (Some SP_S, imm)) [] dest ] - | Imm64_pair (hi, lo) -> - let r = r2pi () in - let l = load_hilo64 vn r hi lo in - let r', l' = extract_arg l in - addinst vn (OEaddil (Some SP_S, Int64.zero)) [ r' ] dest :: l' - | Imm64_large imm -> - let r = r2pi () in - let op1 = OEloadli imm in - let i1 = addinst vn op1 [] r in - let r', l = extract_arg [ i1 ] in - addinst vn (OEaddil (Some SP_S, Int64.zero)) [ r' ] dest :: l - else - match make_immed32 (Ptrofs.to_int n) with - | Imm32_single imm -> [ addinst vn (OEaddiw (Some SP_S, imm)) [] dest ] - | Imm32_pair (hi, lo) -> - let r = r2pi () in - let l = load_hilo32 vn r hi lo in - let r', l' = extract_arg l in - addinst vn (OEaddiw (Some SP_S, Int.zero)) [ r' ] dest :: l' - (** Form a list containing both sources and destination regs of an instruction *) let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ] @@ -1033,11 +1008,6 @@ let expanse (sb : superblock) code pm = exp := addinst vn (OEmayundef (MUshrxl n)) [ r4; r4 ] dest :: l4); exp := extract_final vn !exp dest succ; was_exp := true - (*| Iop (Oaddrstack n, nil, dest, succ) ->*) - (*if exp_debug then eprintf "Iop/Oaddrstack\n";*) - (*exp := addptrofs vn n dest;*) - (*exp := extract_final vn !exp dest succ;*) - (*was_exp := true*) | _ -> ()); (* Update the CSE numbering *) (if not !was_exp then diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v index d0ca5bb2..7d66cbb8 100644 --- a/riscV/NeedOp.v +++ b/riscV/NeedOp.v @@ -87,7 +87,6 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Ointofsingle | Ointuofsingle | Osingleofint | Osingleofintu => op1 (default nv) | Olongofsingle | Olonguofsingle | Osingleoflong | Osingleoflongu => op1 (default nv) | Ocmp c => needs_of_condition c - | OEmoveSP => nil | OEseqw _ => op2 (default nv) | OEsnew _ => op2 (default nv) | OEsequw _ => op2 (default nv) 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 *) diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml index 53730a1b..0d47192a 100644 --- a/riscV/PrintOp.ml +++ b/riscV/PrintOp.ml @@ -40,12 +40,10 @@ let get_optR_s c reg pp r1 r2 = function | None -> fprintf pp "(%a %s %a)" reg r1 (comparison_name c) reg r2 | Some X0_L -> fprintf pp "(X0 %s %a)" (comparison_name c) reg r1 | Some X0_R -> fprintf pp "(%a %s X0)" reg r1 (comparison_name c) - | Some SP_S -> failwith "PrintOp: SP_S in get_optR_s instruction (problem with RTL expansions?)" let get_optR_a pp = function | None -> failwith "PrintOp: None in get_optR_a instruction (problem with RTL expansions?)" | Some X0_L | Some X0_R -> fprintf pp "X0" - | Some SP_S -> fprintf pp "SP" let print_condition reg pp = function | (Ccomp c, [r1;r2]) -> diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v index c453dfb8..d55d94ad 100644 --- a/riscV/RTLpathSE_simplify.v +++ b/riscV/RTLpathSE_simplify.v @@ -309,36 +309,6 @@ Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) : (con let hl := make_lhsv_cmp false hvs hvs in if normal' then ((CEbnew (Some X0_R)), hl) else ((CEbeqw (Some X0_R)), hl). -(** ** Add pointer expansion *) - -Definition addptrofs (n: ptrofs) := - if Ptrofs.eq_dec n Ptrofs.zero then - fSop OEmoveSP fSnil - else - if Archi.ptr64 - then ( - match make_immed64 (Ptrofs.to_int64 n) with - | Imm64_single imm => - fSop (OEaddil (Some SP_S) imm) fSnil - | Imm64_pair hi lo => - let hvs := load_hilo64 hi lo in - let hl := make_lhsv_single hvs in - fSop (OEaddil (Some SP_S) Int64.zero) hl - | Imm64_large imm => - let hvs := fSop (OEloadli imm) fSnil in - let hl := make_lhsv_single hvs in - fSop (OEaddil (Some SP_S) Int64.zero) hl - end) - else ( - match make_immed32 (Ptrofs.to_int n) with - | Imm32_single imm => - fSop (OEaddiw (Some SP_S) imm) fSnil - | Imm32_pair hi lo => - let hvs := load_hilo32 hi lo in - let hl := make_lhsv_single hvs in - fSop (OEaddiw (Some SP_S) Int.zero) hl - end). - (** * Target simplifications using "fake" values *) Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval := @@ -507,8 +477,6 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca let srail_s' := fSop (Oshrlimm n) addl_l in let srail_l' := make_lhsv_cmp false srail_s' srail_s' in Some (fSop (OEmayundef (MUshrxl n)) srail_l') - (* TODO gourdinl | Oaddrstack n, nil =>*) - (*Some (addptrofs n)*) | _, _ => None end. @@ -1943,8 +1911,6 @@ Proof. eapply simplify_longconst_correct; eauto. eapply simplify_floatconst_correct; eauto. eapply simplify_singleconst_correct; eauto. - (* TODO gourdinl*) - (*admit.*) eapply simplify_cast8signed_correct; eauto. eapply simplify_cast16signed_correct; eauto. eapply simplify_addimm_correct; eauto. @@ -1975,7 +1941,6 @@ Proof. - eapply simplify_ccompfs_correct; eauto. - eapply simplify_cnotcompfs_correct; eauto. Qed. -(*Admitted.*) Lemma target_cbranch_expanse_correct hst c l ge sp rs0 m0 st c' l': forall (TARGET: target_cbranch_expanse hst c l = Some (c', l')) diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index 3ba2732d..d29180e4 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -22,12 +22,11 @@ Definition zero64 := (L Int64.zero). (** Functions to select a special register (see Op.v) *) -Definition apply_bin_oreg {B} (optR: option oreg) (sem: aval -> aval -> B) (v1 v2 vz sp: aval): B := +Definition apply_bin_oreg {B} (optR: option oreg) (sem: aval -> aval -> B) (v1 v2 vz: aval): 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. Definition eval_may_undef (mu: mayundef) (v1 v2: aval): aval := @@ -68,22 +67,22 @@ Definition eval_static_condition (cond: condition) (vl: list aval): abool := | Cnotcompf c, v1 :: v2 :: nil => cnot (cmpf_bool c v1 v2) | Ccompfs c, v1 :: v2 :: nil => cmpfs_bool c v1 v2 | Cnotcompfs c, v1 :: v2 :: nil => cnot (cmpfs_bool c v1 v2) - | CEbeqw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32 (Ifptr Ptop) - | CEbnew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32 (Ifptr Ptop) - | CEbequw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32 (Ifptr Ptop) - | CEbneuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32 (Ifptr Ptop) - | CEbltw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32 (Ifptr Ptop) - | CEbltuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32 (Ifptr Ptop) - | CEbgew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cge) v1 v2 zero32 (Ifptr Ptop) - | CEbgeuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cge) v1 v2 zero32 (Ifptr Ptop) - | CEbeql optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64 (Ifptr Ptop) - | CEbnel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64 (Ifptr Ptop) - | CEbequl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64 (Ifptr Ptop) - | CEbneul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64 (Ifptr Ptop) - | CEbltl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64 (Ifptr Ptop) - | CEbltul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64 (Ifptr Ptop) - | CEbgel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cge) v1 v2 zero64 (Ifptr Ptop) - | CEbgeul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cge) v1 v2 zero64 (Ifptr Ptop) + | CEbeqw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32 + | CEbnew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32 + | CEbequw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32 + | CEbneuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32 + | CEbltw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32 + | CEbltuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32 + | CEbgew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cge) v1 v2 zero32 + | CEbgeuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cge) v1 v2 zero32 + | CEbeql optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64 + | CEbnel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64 + | CEbequl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64 + | CEbneul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64 + | CEbltl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64 + | CEbltul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64 + | CEbgel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cge) v1 v2 zero64 + | CEbgeul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cge) v1 v2 zero64 | _, _ => Bnone end. @@ -223,35 +222,34 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Osingleoflong, v1::nil => singleoflong v1 | Osingleoflongu, v1::nil => singleoflongu v1 | Ocmp c, _ => of_optbool (eval_static_condition c vl) - | OEmoveSP, nil => Ptr Stack - | OEseqw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32 (Ifptr Ptop)) - | OEsnew optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32 (Ifptr Ptop)) - | OEsequw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32 (Ifptr Ptop)) - | OEsneuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32 (Ifptr Ptop)) - | OEsltw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32 (Ifptr Ptop)) - | OEsltuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32 (Ifptr Ptop)) + | OEseqw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32) + | OEsnew optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32) + | OEsequw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32) + | OEsneuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32) + | OEsltw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32) + | OEsltuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32) | OEsltiw n, v1::nil => of_optbool (cmp_bool Clt v1 (I n)) | OEsltiuw n, v1::nil => of_optbool (cmpu_bool Clt v1 (I n)) | OExoriw n, v1::nil => xor v1 (I n) | OEluiw n, nil => shl (I n) (I (Int.repr 12)) - | OEaddiw optR n, nil => apply_bin_oreg optR add (I n) (Ifptr Ptop) zero32 (Ifptr Ptop) - | OEaddiw optR n, v1::nil => apply_bin_oreg optR add v1 (Ifptr Ptop) (Ifptr Ptop) (Ptr Stack) + | OEaddiw optR n, nil => apply_bin_oreg optR add (I n) (Ifptr Ptop) zero32 + | OEaddiw optR n, v1::nil => apply_bin_oreg optR add v1 (I n) (Ifptr Ptop) | OEandiw n, v1::nil => and (I n) v1 | OEoriw n, v1::nil => or (I n) v1 - | OEseql optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64 (Ifptr Ptop)) - | OEsnel optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64 (Ifptr Ptop)) - | OEsequl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64 (Ifptr Ptop)) - | OEsneul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64 (Ifptr Ptop)) - | OEsltl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64 (Ifptr Ptop)) - | OEsltul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64 (Ifptr Ptop)) + | OEseql optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64) + | OEsnel optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64) + | OEsequl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64) + | OEsneul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64) + | OEsltl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64) + | OEsltul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64) | OEsltil n, v1::nil => of_optbool (cmpl_bool Clt v1 (L n)) | OEsltiul n, v1::nil => of_optbool (cmplu_bool Clt v1 (L n)) | OEandil n, v1::nil => andl (L n) v1 | OEoril n, v1::nil => orl (L n) v1 | OExoril n, v1::nil => xorl v1 (L n) | OEluil n, nil => sign_ext 32 (shll (L n) (L (Int64.repr 12))) - | OEaddil optR n, nil => apply_bin_oreg optR addl (L n) (Ifptr Ptop) zero64 (Ifptr Ptop) - | OEaddil optR n, v1::nil => apply_bin_oreg optR addl v1 (Ifptr Ptop) (Ifptr Ptop) (Ptr Stack) + | OEaddil optR n, nil => apply_bin_oreg optR addl (L n) (Ifptr Ptop) zero64 + | OEaddil optR n, v1::nil => apply_bin_oreg optR addl v1 (L n) (Ifptr Ptop) | OEloadli n, nil => L (n) | OEmayundef mu, v1 :: v2 :: nil => eval_may_undef mu v1 v2 | OEfeqd, v1::v2::nil => of_optbool (cmpf_bool Ceq v1 v2) @@ -418,8 +416,8 @@ Lemma eval_cmpu_sound c: forall a1 b1 a0 b0 optR m, c = Ceq \/ c = Cne \/ c = Clt-> vmatch bc a1 b1 -> vmatch bc a0 b0 -> - vmatch bc (Op.apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) c) a1 a0 Op.zero32 Vundef) - (of_optbool (apply_bin_oreg optR (cmpu_bool c) b1 b0 zero32 (Ifptr Ptop))). + vmatch bc (Op.apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) c) a1 a0 Op.zero32) + (of_optbool (apply_bin_oreg optR (cmpu_bool c) b1 b0 zero32)). Proof. intros. destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; @@ -433,8 +431,8 @@ Lemma eval_cmplu_sound c: forall a1 b1 a0 b0 optR m, vmatch bc (Val.maketotal (Op.apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) c) a1 a0 - Op.zero64 Vundef)) - (of_optbool (apply_bin_oreg optR (cmplu_bool c) b1 b0 zero64 (Ifptr Ptop))). + Op.zero64)) + (of_optbool (apply_bin_oreg optR (cmplu_bool c) b1 b0 zero64)). Proof. intros. destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; @@ -444,8 +442,8 @@ Qed. Lemma eval_cmp_sound: forall a1 b1 a0 b0 optR cmp, vmatch bc a1 b1 -> vmatch bc a0 b0 -> - vmatch bc (Op.apply_bin_oreg optR (Val.cmp cmp) a1 a0 Op.zero32 Vundef) - (of_optbool (apply_bin_oreg optR (cmp_bool cmp) b1 b0 zero32 (Ifptr Ptop))). + vmatch bc (Op.apply_bin_oreg optR (Val.cmp cmp) a1 a0 Op.zero32) + (of_optbool (apply_bin_oreg optR (cmp_bool cmp) b1 b0 zero32)). Proof. intros. destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; @@ -456,8 +454,8 @@ Lemma eval_cmpl_sound: forall a1 b1 a0 b0 optR cmp, vmatch bc a1 b1 -> vmatch bc a0 b0 -> vmatch bc - (Val.maketotal (Op.apply_bin_oreg optR (Val.cmpl cmp) a1 a0 Op.zero64 Vundef)) - (of_optbool (apply_bin_oreg optR (cmpl_bool cmp) b1 b0 zero64 (Ifptr Ptop))). + (Val.maketotal (Op.apply_bin_oreg optR (Val.cmpl cmp) a1 a0 Op.zero64)) + (of_optbool (apply_bin_oreg optR (cmpl_bool cmp) b1 b0 zero64)). Proof. intros. destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; @@ -482,18 +480,16 @@ Proof. unfold Val.cmp; apply of_optbool_sound; eauto with va. unfold Val.cmpu; apply of_optbool_sound; eauto with va. - { destruct optR as [[]|]; simpl; eauto with va; - InvHyps; eauto with va; - destruct Archi.ptr64 eqn:A; simpl; - inv H1; simpl; try rewrite A; simpl; eauto with va. } + { destruct optR as [[]|]; simpl; eauto with va. } + { destruct optR as [[]|]; + unfold apply_bin_oreg, Op.apply_bin_oreg; eauto with va. } { fold (Val.and (Vint n) a1); eauto with va. } { fold (Val.or (Vint n) a1); eauto with va. } { simpl; try destruct (Int.ltu _ _); eauto with va; unfold ntop1; try apply vmatch_ifptr_undef. } - 9: { destruct optR as [[]|]; simpl; eauto with va; - InvHyps; eauto with va; - destruct Archi.ptr64 eqn:A; simpl; - inv H1; simpl; try rewrite A; simpl; eauto with va. } + 9: { destruct optR as [[]|]; simpl; eauto with va. } + 9: { destruct optR as [[]|]; + unfold apply_bin_oreg, Op.apply_bin_oreg; eauto with va. } 9: { fold (Val.andl (Vlong n) a1); eauto with va. } 9: { fold (Val.orl (Vlong n) a1); eauto with va. } 9: { simpl; unfold ntop1, sign_ext, Int64.sign_ext, sgn; simpl; -- cgit