diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-19 18:19:24 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-19 18:19:24 +0100 |
| commit | fb6325b46ff522a9120f4a101f095908b1ab38c9 (patch) | |
| tree | d2f32b5d368328d36bc752de66bf1ee9a78d7b26 /riscV/ExpansionOracle.ml | |
| parent | 9c9d516ba5df536d15bc27bed0a84fd8170fcdc0 (diff) | |
| download | compcert-kvx-fb6325b46ff522a9120f4a101f095908b1ab38c9.tar.gz compcert-kvx-fb6325b46ff522a9120f4a101f095908b1ab38c9.zip | |
Branch expansions activated and configured in the checker (but admitted) and bugfix in the expansion liveness modification
Diffstat (limited to 'riscV/ExpansionOracle.ml')
| -rw-r--r-- | riscV/ExpansionOracle.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index 32c8731f..9a3518c0 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -442,7 +442,7 @@ let expanse (sb : superblock) code pm = exp := cbranch_int32u false c a1 a2 info succ1 succ2 []; was_branch := true; was_exp := true - (*| Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) -> + | Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) -> debug "Icond/Ccompimm\n"; exp := expanse_cbranchimm_int32s c a1 imm info succ1 succ2 []; was_branch := true; @@ -451,7 +451,7 @@ let expanse (sb : superblock) code pm = debug "Icond/Ccompuimm\n"; exp := expanse_cbranchimm_int32u c a1 imm info succ1 succ2 []; was_branch := true; - was_exp := true*) + was_exp := true | Icond (Ccompl c, a1 :: a2 :: nil, succ1, succ2, info) -> debug "Icond/Ccompl\n"; exp := cbranch_int64s false c a1 a2 info succ1 succ2 []; @@ -462,7 +462,7 @@ let expanse (sb : superblock) code pm = exp := cbranch_int64u false c a1 a2 info succ1 succ2 []; was_branch := true; was_exp := true - (*| Icond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, info) -> + | Icond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, info) -> debug "Icond/Ccomplimm\n"; exp := expanse_cbranchimm_int64s c a1 imm info succ1 succ2 []; was_branch := true; @@ -492,7 +492,7 @@ let expanse (sb : superblock) code pm = debug "Icond/Cnotcompfs\n"; exp := expanse_cbranch_fp true cond_single c f1 f2 info succ1 succ2 []; was_branch := true; - was_exp := true*) + was_exp := true | _ -> new_order := n :: !new_order); if !was_exp then ( node := !node + 1; @@ -500,7 +500,8 @@ let expanse (sb : superblock) code pm = let lives = PTree.get n !liveins in match lives with | Some lives -> - liveins := PTree.set (n2p ()) lives !liveins; + let new_branch_pc = Camlcoq.P.of_int (!node - ((List.length !exp) - 1)) in + liveins := PTree.set new_branch_pc lives !liveins; liveins := PTree.remove n !liveins | _ -> ()); write_pathmap sb.instructions.(0) (List.length !exp) pm'; |