diff options
Diffstat (limited to 'ia32/CBuiltins.ml')
-rw-r--r-- | ia32/CBuiltins.ml | 94 |
1 files changed, 0 insertions, 94 deletions
diff --git a/ia32/CBuiltins.ml b/ia32/CBuiltins.ml deleted file mode 100644 index 09303223..00000000 --- a/ia32/CBuiltins.ml +++ /dev/null @@ -1,94 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(* Processor-dependent builtin C functions *) - -open C - -let (va_list_type, va_list_scalar, size_va_list) = - if Archi.ptr64 then - (* Actually a struct passed by reference; equivalent to 3 64-bit words *) - (TArray(TInt(IULong, []), Some 3L, []), false, 3*8) - else - (* Just a pointer *) - (TPtr(TVoid [], []), true, 4) - -let builtins = { - Builtins.typedefs = [ - "__builtin_va_list", va_list_type; - ]; - Builtins.functions = [ - (* Integer arithmetic *) - "__builtin_bswap", - (TInt(IUInt, []), [TInt(IUInt, [])], false); - "__builtin_bswap64", - (TInt(IULongLong, []), [TInt(IULongLong, [])], false); - "__builtin_bswap32", - (TInt(IUInt, []), [TInt(IUInt, [])], false); - "__builtin_bswap16", - (TInt(IUShort, []), [TInt(IUShort, [])], false); - "__builtin_clz", - (TInt(IInt, []), [TInt(IUInt, [])], false); - "__builtin_clzl", - (TInt(IInt, []), [TInt(IULong, [])], false); - "__builtin_clzll", - (TInt(IInt, []), [TInt(IULongLong, [])], false); - "__builtin_ctz", - (TInt(IInt, []), [TInt(IUInt, [])], false); - "__builtin_ctzl", - (TInt(IInt, []), [TInt(IULong, [])], false); - "__builtin_ctzll", - (TInt(IInt, []), [TInt(IULongLong, [])], false); - (* Float arithmetic *) - "__builtin_fsqrt", - (TFloat(FDouble, []), [TFloat(FDouble, [])], false); - "__builtin_fmax", - (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false); - "__builtin_fmin", - (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false); - "__builtin_fmadd", - (TFloat(FDouble, []), - [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])], - false); - "__builtin_fmsub", - (TFloat(FDouble, []), - [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])], - false); - "__builtin_fnmadd", - (TFloat(FDouble, []), - [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])], - false); - "__builtin_fnmsub", - (TFloat(FDouble, []), - [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])], - false); - (* Memory accesses *) - "__builtin_read16_reversed", - (TInt(IUShort, []), [TPtr(TInt(IUShort, [AConst]), [])], false); - "__builtin_read32_reversed", - (TInt(IUInt, []), [TPtr(TInt(IUInt, [AConst]), [])], false); - "__builtin_write16_reversed", - (TVoid [], [TPtr(TInt(IUShort, []), []); TInt(IUShort, [])], false); - "__builtin_write32_reversed", - (TVoid [], [TPtr(TInt(IUInt, []), []); TInt(IUInt, [])], false); - (* no operation *) - "__builtin_nop", - (TVoid [], [], false); - ] -} - -(* Expand memory references inside extended asm statements. Used in C2C. *) - -let asm_mem_argument arg = Printf.sprintf "0(%s)" arg |