diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-10 10:34:38 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-10 10:34:38 +0100 |
| commit | 84cb4939653e5355c2039ed62a140aa392e21162 (patch) | |
| tree | 156a6a78208983cf7fca540899313144f36687e0 /riscV/ExpansionOracle.ml | |
| parent | 3104e551bf87abeab9a257c955cf9b180769dc64 (diff) | |
| download | compcert-kvx-84cb4939653e5355c2039ed62a140aa392e21162.tar.gz compcert-kvx-84cb4939653e5355c2039ed62a140aa392e21162.zip | |
[Admitted checker] Checker expansion for reg Ocmp (without scratch)
Diffstat (limited to 'riscV/ExpansionOracle.ml')
| -rw-r--r-- | riscV/ExpansionOracle.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index e267fd5a..b3a440a4 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -284,7 +284,7 @@ let expanse_condimm_int32u cmp a1 n dest succ k = (cond_int32u false cmp a1 (r2p ()) dest succ k) let expanse_condimm_int64s cmp a1 n dest succ k = - if Int.eq n Int.zero then cond_int64s true cmp a1 a1 dest succ k + if Int64.eq n Int64.zero then cond_int64s true cmp a1 a1 dest succ k else match cmp with | Ceq | Cne -> @@ -391,14 +391,14 @@ let expanse (sb : superblock) code pm = debug "Iop/Ccompu\n"; exp := cond_int32u false c a1 a2 dest succ []; was_exp := true - | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) -> + (*| Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) -> debug "Iop/Ccompimm\n"; exp := expanse_condimm_int32s c a1 imm dest succ []; was_exp := true | Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) -> debug "Iop/Ccompuimm\n"; exp := expanse_condimm_int32u c a1 imm dest succ []; - was_exp := true + was_exp := true*) | Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) -> debug "Iop/Ccompl\n"; exp := cond_int64s false c a1 a2 dest succ []; @@ -407,14 +407,14 @@ let expanse (sb : superblock) code pm = debug "Iop/Ccomplu\n"; exp := cond_int64u false c a1 a2 dest succ []; was_exp := true - | Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) -> + (*| Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) -> debug "Iop/Ccomplimm\n"; exp := expanse_condimm_int64s c a1 imm dest succ []; was_exp := true | Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) -> debug "Iop/Ccompluimm\n"; exp := expanse_condimm_int64u c a1 imm dest succ []; - was_exp := true + was_exp := true*) | Iop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, succ) -> debug "Iop/Ccompf\n"; exp := expanse_cond_fp false cond_float c f1 f2 dest succ []; @@ -431,7 +431,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 - | Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) -> + (*| Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) -> debug "Icond/Ccomp\n"; exp := cbranch_int32s false c a1 a2 info succ1 succ2 []; was_branch := true; @@ -491,7 +491,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; |