diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-10 12:19:17 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-10 12:19:17 +0100 |
| commit | c40646559461154e5190a4c887f9992f35eedb9f (patch) | |
| tree | 649dd8137c768fa456f98b961174ddd3ea630c01 /riscV | |
| parent | 84cb4939653e5355c2039ed62a140aa392e21162 (diff) | |
| download | compcert-kvx-c40646559461154e5190a4c887f9992f35eedb9f.tar.gz compcert-kvx-c40646559461154e5190a4c887f9992f35eedb9f.zip | |
[Admitted checker] Adding cbranch expansions (without scratch) to the checker
Diffstat (limited to 'riscV')
| -rw-r--r-- | riscV/Asmgen.v | 2 | ||||
| -rw-r--r-- | riscV/ExpansionOracle.ml | 10 |
2 files changed, 7 insertions, 5 deletions
diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index 7f63bfee..d826f139 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -222,7 +222,7 @@ Definition apply_bin_r0_r0r0 (optR0: option bool) (sem: ireg0 -> ireg0 -> instru Definition transl_cbranch (cond: condition) (args: list mreg) (lbl: label) (k: code) := match cond, args with -| Ccomp c, a1 :: a2 :: nil => + | Ccomp c, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (transl_cbranch_int32s c r1 r2 lbl :: k) | Ccompu c, a1 :: a2 :: nil => diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index b3a440a4..dc7f4b82 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -370,6 +370,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;*) let new_order = ref [] in let liveins = ref sb.liveins in let exp = ref [] in @@ -431,7 +432,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; @@ -441,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; @@ -450,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 []; @@ -461,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; @@ -508,6 +509,7 @@ let expanse (sb : superblock) code pm = sb.instructions; sb.instructions <- Array.of_list (List.rev !new_order); sb.liveins <- !liveins; + (*debug_flag := false;*) (!code', !pm') let rec find_last_node_reg = function |