1 files changed, 0 insertions, 35 deletions
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'))