diff options
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'; |