Removing addptrofs draft, next will be merging

9 files changed, 104 insertions, 254 deletions

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;