diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-04-30 10:00:32 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-04-30 10:00:32 +0000 |
| commit | b2ec46d86034261ed42be26b42ecee6f454ee344 (patch) | |
| tree | 477604ac7ec68e6297051534262446e3153c4f0b /checklink | |
| parent | c2df6044b7560b2a4c1f3ca32571baa83de0f15a (diff) | |
Add bswap16
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2223 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'checklink')
| -rw-r--r-- | checklink/Check.ml | 24 |
1 files changed, 23 insertions, 1 deletions
diff --git a/checklink/Check.ml b/checklink/Check.ml index 412d3ab..4097267 100644 --- a/checklink/Check.ml +++ b/checklink/Check.ml @@ -1191,7 +1191,7 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end - | "__builtin_bswap", [IR a1], [IR res] -> + | ("__builtin_bswap"|"__builtin_bswap32"), [IR a1], [IR res] -> begin match ecode with | STWU (rS0, rA0, d0) :: LWBRX(rD1, rA1, rB1) :: @@ -1209,6 +1209,28 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= compare_code cs es (Int32.add 12l pc) | _ -> error end + | "__builtin_bswap16", [IR a1], [IR res] -> + begin match ecode with + | RLWINMx(rS1, rA1, sh1, mb1, me1, rc1) :: + RLWINMx(rS2, rA2, sh2, mb2, me2, rc2) :: + ORx(rS3, rA3, rB3, rc3) :: es -> + OK(fw) + >>= match_iregs GPR0 rS1 + >>= match_iregs a1 rA1 + >>= check_eq "bswap16-1" sh1 8 + >>= check_eq "bswap16-2" mb1 16 + >>= check_eq "bswap16-3" me1 23 + >>= match_iregs res rS2 + >>= match_iregs a1 rA2 + >>= check_eq "bswap16-4" sh2 24 + >>= check_eq "bswap16-5" mb2 24 + >>= check_eq "bswap16-6" me2 31 + >>= match_iregs res rS3 + >>= match_iregs GPR0 rA3 + >>= match_iregs res rB3 + >>= compare_code cs es (Int32.add 12l pc) + | _ -> error + end | "__builtin_fmadd", [FR a1; FR a2; FR a3], [FR res] -> begin match ecode with | FMADDx(frD, frA, frB, frC, rc) :: es -> |