From b7720bc5973e9890e7c320bb34b784e2e2b2da69 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Fri, 9 Apr 2021 11:02:52 +0200
Subject: Removing addptrofs draft, next will be merging

---
 riscV/ExpansionOracle.ml | 30 ------------------------------
 1 file changed, 30 deletions(-)

(limited to 'riscV/ExpansionOracle.ml')

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
-- 
cgit