diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-08-28 22:39:41 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-08-28 22:39:41 +0200 |
| commit | 23a129e18ae930de5f40df59307c48c68d62d8d7 (patch) | |
| tree | 403387a98ea9da32d70ac5b5607d5be30fa0ee42 /x86 | |
| parent | 780ad9d001af651a49d7470e963ed9a49ee11a4c (diff) | |
| parent | 192bd462233d0284fa3d5f8e8994a514b549713e (diff) | |
| download | compcert-kvx-23a129e18ae930de5f40df59307c48c68d62d8d7.tar.gz compcert-kvx-23a129e18ae930de5f40df59307c48c68d62d8d7.zip | |
Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-upstream-merge
Diffstat (limited to 'x86')
| -rw-r--r-- | x86/CBuiltins.ml | 2 | ||||
| -rw-r--r-- | x86/TargetPrinter.ml | 32 |
2 files changed, 19 insertions, 15 deletions
diff --git a/x86/CBuiltins.ml b/x86/CBuiltins.ml index 6fb8b697..f4f40a31 100644 --- a/x86/CBuiltins.ml +++ b/x86/CBuiltins.ml @@ -31,8 +31,6 @@ let builtins = { ]; builtin_functions = [ (* Integer arithmetic *) - "__builtin_bswap64", - (TInt(IULongLong, []), [TInt(IULongLong, [])], false); "__builtin_clz", (TInt(IInt, []), [TInt(IUInt, [])], false); "__builtin_clzl", diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml index cd54e08b..6159437e 100644 --- a/x86/TargetPrinter.ml +++ b/x86/TargetPrinter.ml @@ -399,7 +399,13 @@ module Target(System: SYSTEM):TARGET = (* Printing of instructions *) -(* Reminder on AT&T syntax: op source, dest *) +(* Reminder on X86 assembly syntaxes: + AT&T syntax Intel syntax + (used by GNU as) (used in reference manuals) + dst <- op(src) op src, dst op dst, src + dst <- op(dst, src2) op src2, dst op dst, src2 + dst <- op(dst, src2, src3) op src3, src2, dst op dst, src2, src3 +*) let print_instruction oc = function (* Moves *) @@ -752,29 +758,29 @@ module Target(System: SYSTEM):TARGET = | Pcfi_adjust sz -> cfi_adjust oc (camlint_of_coqint sz) | Pfmadd132 (res,a1,a2) -> - fprintf oc " vfmadd132sd %a, %a, %a\n" freg a1 freg a2 freg res + fprintf oc " vfmadd132sd %a, %a, %a\n" freg a2 freg a1 freg res | Pfmadd213 (res,a1,a2) -> - fprintf oc " vfmadd213sd %a, %a, %a\n" freg a1 freg a2 freg res + fprintf oc " vfmadd213sd %a, %a, %a\n" freg a2 freg a1 freg res | Pfmadd231 (res,a1,a2) -> - fprintf oc " vfmadd231sd %a, %a, %a\n" freg a1 freg a2 freg res + fprintf oc " vfmadd231sd %a, %a, %a\n" freg a2 freg a1 freg res | Pfmsub132 (res,a1,a2) -> - fprintf oc " vfmsub132sd %a, %a, %a\n" freg a1 freg a2 freg res + fprintf oc " vfmsub132sd %a, %a, %a\n" freg a2 freg a1 freg res | Pfmsub213 (res,a1,a2) -> - fprintf oc " vfmsub213sd %a, %a, %a\n" freg a1 freg a2 freg res + fprintf oc " vfmsub213sd %a, %a, %a\n" freg a2 freg a1 freg res | Pfmsub231 (res,a1,a2) -> - fprintf oc " vfmsub231sd %a, %a, %a\n" freg a1 freg a2 freg res + fprintf oc " vfmsub231sd %a, %a, %a\n" freg a2 freg a1 freg res | Pfnmadd132 (res,a1,a2) -> - fprintf oc " vfnmadd132sd %a, %a, %a\n" freg a1 freg a2 freg res + fprintf oc " vfnmadd132sd %a, %a, %a\n" freg a2 freg a1 freg res | Pfnmadd213 (res,a1,a2) -> - fprintf oc " vfnmadd213sd %a, %a, %a\n" freg a1 freg a2 freg res + fprintf oc " vfnmadd213sd %a, %a, %a\n" freg a2 freg a1 freg res | Pfnmadd231 (res,a1,a2) -> - fprintf oc " vfnmadd231sd %a, %a, %a\n" freg a1 freg a2 freg res + fprintf oc " vfnmadd231sd %a, %a, %a\n" freg a2 freg a1 freg res | Pfnmsub132 (res,a1,a2) -> - fprintf oc " vfnmsub132sd %a, %a, %a\n" freg a1 freg a2 freg res + fprintf oc " vfnmsub132sd %a, %a, %a\n" freg a2 freg a1 freg res | Pfnmsub213 (res,a1,a2) -> - fprintf oc " vfnmsub213sd %a, %a, %a\n" freg a1 freg a2 freg res + fprintf oc " vfnmsub213sd %a, %a, %a\n" freg a2 freg a1 freg res | Pfnmsub231 (res,a1,a2) -> - fprintf oc " vfnmsub231sd %a, %a, %a\n" freg a1 freg a2 freg res + fprintf oc " vfnmsub231sd %a, %a, %a\n" freg a2 freg a1 freg res | Pmaxsd (res,a1) -> fprintf oc " maxsd %a, %a\n" freg a1 freg res | Pminsd (res,a1) -> |