diff options
Diffstat (limited to 'riscV/ExpansionOracle.ml')
| -rw-r--r-- | riscV/ExpansionOracle.ml | 30 |
1 files changed, 0 insertions, 30 deletions
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 |