diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-12 17:20:45 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-12 17:20:45 +0100 |
| commit | df8f93225869980a0fff3df6659aca836952b720 (patch) | |
| tree | f96df40e14ee516b6381b934babf1970d4de0948 /aarch64/PostpassSchedulingOracle.ml | |
| parent | b387d68faae6cdc520a1ae4d213402de473f6022 (diff) | |
| download | compcert-kvx-df8f93225869980a0fff3df6659aca836952b720.tar.gz compcert-kvx-df8f93225869980a0fff3df6659aca836952b720.zip | |
Arith inst OK for the verifier
Diffstat (limited to 'aarch64/PostpassSchedulingOracle.ml')
| -rw-r--r-- | aarch64/PostpassSchedulingOracle.ml | 42 |
1 files changed, 36 insertions, 6 deletions
diff --git a/aarch64/PostpassSchedulingOracle.ml b/aarch64/PostpassSchedulingOracle.ml index 831080d5..7c8bd144 100644 --- a/aarch64/PostpassSchedulingOracle.ml +++ b/aarch64/PostpassSchedulingOracle.ml @@ -212,6 +212,14 @@ let reg_of_ireg0 r = let reg_of_freg r = Reg (Asm.DR (Asm.FR r)) +let flags_wlocs = + [ + Reg (Asm.CR Asm.CN); + Reg (Asm.CR Asm.CZ); + Reg (Asm.CR Asm.CC); + Reg (Asm.CR Asm.CV); + ] + let arith_p_rec i rd = { inst = arith_p_real i; @@ -266,7 +274,7 @@ let arith_arrrr0_rec i rd r1 r2 r3 = let arith_comparison_pp_rec i r1 r2 = { inst = arith_comparison_pp_real i; - write_locs = []; + write_locs = flags_wlocs; read_locs = [ r1; r2 ]; is_control = false; } @@ -275,7 +283,7 @@ let arith_comparison_r0r_rec i r1 r2 = let rlocs = if is_XZR r1 then [ r2 ] else [ r1; r2 ] in { inst = arith_comparison_r0r_real i; - write_locs = []; + write_locs = flags_wlocs; read_locs = rlocs; is_control = false; } @@ -283,7 +291,7 @@ let arith_comparison_r0r_rec i r1 r2 = let arith_comparison_p_rec i r1 = { inst = arith_comparison_p_real i; - write_locs = []; + write_locs = flags_wlocs; read_locs = [ r1 ]; is_control = false; } @@ -331,14 +339,36 @@ let cvtuw2x_rec rd r1 = let cvtx2w_rec rd = { inst = cvtx2w_real; write_locs = []; read_locs = []; is_control = false } +let get_testcond_rlocs c = + match c with + | Asm.TCeq -> [ Reg (Asm.CR Asm.CZ) ] + | Asm.TCne -> [ Reg (Asm.CR Asm.CZ) ] + | Asm.TChs -> [ Reg (Asm.CR Asm.CC) ] + | Asm.TClo -> [ Reg (Asm.CR Asm.CC) ] + | Asm.TCmi -> [ Reg (Asm.CR Asm.CN) ] + | Asm.TCpl -> [ Reg (Asm.CR Asm.CN) ] + | Asm.TChi -> [ Reg (Asm.CR Asm.CZ); Reg (Asm.CR Asm.CC) ] + | Asm.TCls -> [ Reg (Asm.CR Asm.CZ); Reg (Asm.CR Asm.CC) ] + | Asm.TCge -> [ Reg (Asm.CR Asm.CN); Reg (Asm.CR Asm.CV) ] + | Asm.TClt -> [ Reg (Asm.CR Asm.CN); Reg (Asm.CR Asm.CV) ] + | Asm.TCgt -> + [ Reg (Asm.CR Asm.CN); Reg (Asm.CR Asm.CZ); Reg (Asm.CR Asm.CV) ] + | Asm.TCle -> + [ Reg (Asm.CR Asm.CN); Reg (Asm.CR Asm.CZ); Reg (Asm.CR Asm.CV) ] + let cset_rec rd c = - { inst = cset_real; write_locs = [ rd ]; read_locs = []; is_control = false } + { + inst = cset_real; + write_locs = [ rd ]; + read_locs = get_testcond_rlocs c; + is_control = false; + } let csel_rec rd r1 r2 c = { inst = csel_real; write_locs = [ rd ]; - read_locs = [ r1; r2 ]; + read_locs = [ r1; r2 ] @ get_testcond_rlocs c; is_control = false; } @@ -891,7 +921,7 @@ let smart_schedule bb = let bblock_schedule bb = let identity_mode = not !Clflags.option_fpostpass in - if (debug && not identity_mode) then ( + if debug && not identity_mode then ( Printf.eprintf "###############################\n"; Printf.eprintf "SCHEDULING\n" ); if identity_mode then pack_result bb else smart_schedule bb |