diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-02 18:48:53 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-02 18:48:53 +0100 |
| commit | 801cd27eb78a9ba9dce6f62626288531905fcfed (patch) | |
| tree | 83a5811930ebb3fa659fa2e531fc270f1e145b38 /riscV/ExpansionOracle.ml | |
| parent | 3e953ef41f736ed5b7db699b1adf21d46cb5b8db (diff) | |
| download | compcert-kvx-801cd27eb78a9ba9dce6f62626288531905fcfed.tar.gz compcert-kvx-801cd27eb78a9ba9dce6f62626288531905fcfed.zip | |
[Admitted checker] Oracle expansion for float/float32 constant init
Diffstat (limited to 'riscV/ExpansionOracle.ml')
| -rw-r--r-- | riscV/ExpansionOracle.ml | 25 |
1 files changed, 23 insertions, 2 deletions
diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index 95a300c5..c6710a95 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -379,7 +379,7 @@ let rec write_tree exp current code' new_order = | _ -> failwith "ExpansionOracle.write_tree: inconsistent instruction." let expanse (sb : superblock) code pm = - (*debug_flag := true;*) + debug_flag := true; let new_order = ref [] in let liveins = ref sb.liveins in let exp = ref [] in @@ -393,6 +393,7 @@ let expanse (sb : superblock) code pm = was_exp := false; let inst = get_some @@ PTree.get n code in (match inst with + (* Expansion of conditions - Ocmp *) | Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, succ) -> debug "Iop/Ccomp\n"; exp := cond_int32s false c a1 a2 dest succ []; @@ -441,6 +442,7 @@ let expanse (sb : superblock) code pm = debug "Iop/Cnotcompfs\n"; exp := expanse_cond_fp true cond_single c f1 f2 dest succ []; was_exp := true + (* Expansion of branches - Ccomp *) | Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) -> debug "Icond/Ccomp\n"; exp := cbranch_int32s false c a1 a2 info succ1 succ2 []; @@ -502,6 +504,25 @@ let expanse (sb : superblock) code pm = exp := expanse_cbranch_fp true cond_single c f1 f2 info succ1 succ2 []; was_branch := true; was_exp := true + (* Expansion of fp constants *) + | Iop (Ofloatconst f, nil, dest, succ) -> + debug "Iop/Ofloatconst\n"; + let r = r2pi () in + exp := + [ + Iop (Olongconst (Floats.Float.to_bits f), [], r, n2pi ()); + Iop (Ofloat_of_bits, [ r ], dest, succ); + ]; + was_exp := true + | Iop (Osingleconst f, nil, dest, succ) -> + debug "Iop/Osingleconst\n"; + let r = r2pi () in + exp := + [ + Iop (Ointconst (Floats.Float32.to_bits f), [], r, n2pi ()); + Iop (Osingle_of_bits, [ r ], dest, succ); + ]; + was_exp := true | _ -> new_order := n :: !new_order); if !was_exp then ( node := !node + 1; @@ -521,7 +542,7 @@ let expanse (sb : superblock) code pm = sb.instructions; sb.instructions <- Array.of_list (List.rev !new_order); sb.liveins <- !liveins; - (*debug_flag := false;*) + debug_flag := false; (!code', !pm') let rec find_last_node_reg = function |