diff options
-rw-r--r-- | Changelog | 40 | ||||
-rw-r--r-- | VERSION | 2 | ||||
-rw-r--r-- | cfrontend/C2C.ml | 4 | ||||
-rw-r--r-- | common/Sections.ml | 29 | ||||
-rw-r--r-- | common/Sections.mli | 4 | ||||
-rw-r--r-- | doc/index.html | 4 | ||||
-rw-r--r-- | runtime/arm/i64_stof.S | 9 | ||||
-rw-r--r-- | runtime/powerpc/i64_stof.s | 17 | ||||
-rw-r--r-- | runtime/powerpc/i64_utof.s | 10 | ||||
-rw-r--r-- | runtime/powerpc64/i64_utof.s | 10 | ||||
-rw-r--r-- | test/regression/Results/int64 | 874 | ||||
-rw-r--r-- | test/regression/int64.c | 3 |
12 files changed, 926 insertions, 80 deletions
@@ -1,7 +1,41 @@ -Coq development: -- Compatibility with Coq version 8.11.0 (#316) +Release 3.7, 2020-03-31 +======================= + +ISO C conformance: +- Functions declared `extern` then implemented `inline` remain `extern` +- The type of a wide char constant is `wchar_t`, not `int` +- Support vertical tabs and treat them as whitespace +- Define the semantics of `free(NULL)` + +Bug fixing: +- Take sign into account for conversions from 32-bit integers to 64-bit pointers +- PowerPC: more precise determination of small data accesses +- AArch64: when addressing global variables, check for correct alignment +- PowerPC, ARM: double rounding error in int64->float32 conversions + +ABI conformance: +- x86, AArch64: re-normalize values of small integer types returned by + function calls +- PowerPC: `float` arguments passed on stack are passed in 64-bit format +- RISC-V: use the new ELF psABI instead of the old ABI from ISA 2.1 + +Usability and diagnostics: +- Unknown builtin functions trigger a specific error message +- Improved error messages + +Coq formalization: +- Revised modeling of the PowerPC/EREF `isel` instruction +- Weaker `ec_readonly` condition over external calls + (permissions can be dropped on read-only locations) + +Coq and OCaml development: +- Compatibility with Coq version 8.10.1, 8.10.2, 8.11.0 +- Compatibility with OCaml 4.10 and up +- Compatibility with Menhir 20200123 and up +- Coq versions prior to 8.8.0 are no longer supported +- OCaml versions prior to 4.05.0 are no longer supported + - Release 3.6, 2019-09-17 ======================= @@ -1,3 +1,3 @@ -version=3.6 +version=3.7 buildnr= tag= diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index ec5fb4dc..bc5173ca 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -1258,7 +1258,7 @@ let convertFundef loc env fd = { a_storage = fd.fd_storage; a_alignment = None; a_size = None; - a_sections = Sections.for_function env id' fd.fd_attrib; + a_sections = Sections.for_function env loc id' fd.fd_attrib; a_access = Sections.Access_default; a_inline = inline; a_loc = loc }; @@ -1343,7 +1343,7 @@ let convertGlobvar loc env (sto, id, ty, optinit) = | Some i -> convertInitializer env ty i in let (section, access) = - Sections.for_variable env id' ty (optinit <> None) in + Sections.for_variable env loc id' ty (optinit <> None) in if Z.gt sz (Z.of_uint64 0xFFFF_FFFFL) then error "'%s' is too big (%s bytes)" id.name (Z.to_string sz); diff --git a/common/Sections.ml b/common/Sections.ml index 30be9e69..839128a5 100644 --- a/common/Sections.ml +++ b/common/Sections.ml @@ -160,9 +160,22 @@ let gcc_section name readonly exec = sec_writable = not readonly; sec_executable = exec; sec_access = Access_default } +(* Check and extract whether a section was given as attribute *) + +let get_attr_section loc attr = + match Cutil.find_custom_attributes ["section"; "__section__"] attr with + | [] -> None + | [[C.AString name]] -> Some name + | [[_]] -> + Diagnostics.error loc "'section' attribute requires a string"; + None + | _ -> + Diagnostics.error loc "ambiguous 'section' attribute"; + None + (* Determine section for a variable definition *) -let for_variable env id ty init = +let for_variable env loc id ty init = let attr = Cutil.attributes_of_type env ty in let readonly = List.mem C.AConst attr && not(List.mem C.AVolatile attr) in let si = @@ -170,11 +183,11 @@ let for_variable env id ty init = (* 1- Section explicitly associated with #use_section *) Hashtbl.find use_section_table id with Not_found -> - match Cutil.find_custom_attributes ["section"; "__section__"] attr with - | [[C.AString name]] -> + match get_attr_section loc attr with + | Some name -> (* 2- Section given as an attribute, gcc-style *) gcc_section name readonly false - | _ -> + | None -> (* 3- Default section appropriate for size and const-ness *) let size = match Cutil.sizeof env ty with Some sz -> sz | None -> max_int in @@ -190,17 +203,17 @@ let for_variable env id ty init = (* Determine sections for a function definition *) -let for_function env id attr = +let for_function env loc id attr = let si_code = try (* 1- Section explicitly associated with #use_section *) Hashtbl.find use_section_table id with Not_found -> - match Cutil.find_custom_attributes ["section"; "__section__"] attr with - | [[C.AString name]] -> + match get_attr_section loc attr with + | Some name -> (* 2- Section given as an attribute, gcc-style *) gcc_section name true true - | _ -> + | None -> (* 3- Default section *) try Hashtbl.find current_section_table "CODE" diff --git a/common/Sections.mli b/common/Sections.mli index bc97814d..d9fd9239 100644 --- a/common/Sections.mli +++ b/common/Sections.mli @@ -46,7 +46,7 @@ val define_section: -> ?writable:bool -> ?executable:bool -> ?access:access_mode -> unit -> unit val use_section_for: AST.ident -> string -> bool -val for_variable: Env.t -> AST.ident -> C.typ -> bool -> +val for_variable: Env.t -> C.location -> AST.ident -> C.typ -> bool -> section_name * access_mode -val for_function: Env.t -> AST.ident -> C.attributes -> section_name list +val for_function: Env.t -> C.location -> AST.ident -> C.attributes -> section_name list val for_stringlit: unit -> section_name diff --git a/doc/index.html b/doc/index.html index 3a4cf6ba..631c5d99 100644 --- a/doc/index.html +++ b/doc/index.html @@ -24,7 +24,7 @@ a:active {color : Red; text-decoration : underline; } <H1 align="center">The CompCert verified compiler</H1> <H2 align="center">Commented Coq development</H2> -<H3 align="center">Version 3.6, 2019-09-17</H3> +<H3 align="center">Version 3.7, 2020-03-31</H3> <H2>Introduction</H2> @@ -101,6 +101,8 @@ See also: <A HREF="html/compcert.common.Memdata.html">Memdata</A> (in-memory rep <LI> <A HREF="html/compcert.common.Determinism.html">Determinism</A>: determinism properties of small-step semantics. <LI> <A HREF="html/compcert.powerpc.Op.html"><I>Op</I></A>: operators, addressing modes and their semantics. +<LI> <A HREF="html/compcert.common.Builtins.html">Builtins</A>: semantics of built-in functions. <BR> +See also: <A HREF="html/compcert.common.Builtins0.html">Builtins0</A> (target-independent part), <A HREF="html/compcert.powerpc.Builtins1.html"><I>Builtins1</I></A> (target-dependent part). <LI> <A HREF="html/compcert.common.Unityping.html">Unityping</A>: a solver for atomic unification constraints. </UL> diff --git a/runtime/arm/i64_stof.S b/runtime/arm/i64_stof.S index bcfa471c..11e00a2a 100644 --- a/runtime/arm/i64_stof.S +++ b/runtime/arm/i64_stof.S @@ -39,12 +39,11 @@ @@@ Conversion from signed 64-bit integer to single float FUNCTION(__compcert_i64_stof) - @ Check whether -2^53 <= X < 2^53 - ASR r2, Reg0HI, #21 - ASR r3, Reg0HI, #31 @ (r2,r3) = X >> 53 + @ Check whether -2^53 <= X < 2^53 + ASR r2, Reg0HI, #21 @ r2 = high 32 bits of X >> 53 + @ -2^53 <= X < 2^53 iff r2 is -1 or 0, that is, iff r2 + 1 is 0 or 1 adds r2, r2, #1 - adc r3, r3, #0 @ (r2,r3) = X >> 53 + 1 - cmp r3, #2 + cmp r2, #2 blo 1f @ X is large enough that double rounding can occur. @ Avoid it by nudging X away from the points where double rounding diff --git a/runtime/powerpc/i64_stof.s b/runtime/powerpc/i64_stof.s index 97fa6bb8..ea23a1c8 100644 --- a/runtime/powerpc/i64_stof.s +++ b/runtime/powerpc/i64_stof.s @@ -43,20 +43,19 @@ __compcert_i64_stof: mflr r9 # Check whether -2^53 <= X < 2^53 - srawi r5, r3, 31 - srawi r6, r3, 21 # (r5,r6) = X >> 53 - addic r6, r6, 1 - addze r5, r5 # (r5,r6) = (X >> 53) + 1 + srawi r5, r3, 21 # r5 = high 32 bits of X >> 53 + # -2^53 <= X < 2^53 iff r5 is -1 or 0, that is, iff r5 + 1 is 0 or 1 + addi r5, r5, 1 cmplwi r5, 2 blt 1f # X is large enough that double rounding can occur. # Avoid it by nudging X away from the points where double rounding # occurs (the "round to odd" technique) - rlwinm r0, r4, 0, 21, 31 # extract bits 0 to 11 of X - addi r0, r0, 0x7FF # r0 = (X & 0x7FF) + 0x7FF - # bit 12 of r0 is 0 if all low 12 bits of X are 0, 1 otherwise - # bits 13-31 of r0 are 0 - or r4, r4, r0 # correct bit number 12 of X + rlwinm r5, r4, 0, 21, 31 # extract bits 0 to 11 of X + addi r5, r5, 0x7FF # r5 = (X & 0x7FF) + 0x7FF + # bit 12 of r5 is 0 if all low 12 bits of X are 0, 1 otherwise + # bits 13-31 of r5 are 0 + or r4, r4, r5 # correct bit number 12 of X rlwinm r4, r4, 0, 0, 20 # set to 0 bits 0 to 11 of X # Convert to double, then round to single 1: bl __compcert_i64_stod diff --git a/runtime/powerpc/i64_utof.s b/runtime/powerpc/i64_utof.s index cdb2f867..4a2a172b 100644 --- a/runtime/powerpc/i64_utof.s +++ b/runtime/powerpc/i64_utof.s @@ -48,11 +48,11 @@ __compcert_i64_utof: # X is large enough that double rounding can occur. # Avoid it by nudging X away from the points where double rounding # occurs (the "round to odd" technique) - rlwinm r0, r4, 0, 21, 31 # extract bits 0 to 11 of X - addi r0, r0, 0x7FF # r0 = (X & 0x7FF) + 0x7FF - # bit 12 of r0 is 0 if all low 12 bits of X are 0, 1 otherwise - # bits 13-31 of r0 are 0 - or r4, r4, r0 # correct bit number 12 of X + rlwinm r5, r4, 0, 21, 31 # extract bits 0 to 11 of X + addi r5, r5, 0x7FF # r5 = (X & 0x7FF) + 0x7FF + # bit 12 of r5 is 0 if all low 12 bits of X are 0, 1 otherwise + # bits 13-31 of r5 are 0 + or r4, r4, r5 # correct bit number 12 of X rlwinm r4, r4, 0, 0, 20 # set to 0 bits 0 to 11 of X # Convert to double, then round to single 1: bl __compcert_i64_utod diff --git a/runtime/powerpc64/i64_utof.s b/runtime/powerpc64/i64_utof.s index cdb2f867..4a2a172b 100644 --- a/runtime/powerpc64/i64_utof.s +++ b/runtime/powerpc64/i64_utof.s @@ -48,11 +48,11 @@ __compcert_i64_utof: # X is large enough that double rounding can occur. # Avoid it by nudging X away from the points where double rounding # occurs (the "round to odd" technique) - rlwinm r0, r4, 0, 21, 31 # extract bits 0 to 11 of X - addi r0, r0, 0x7FF # r0 = (X & 0x7FF) + 0x7FF - # bit 12 of r0 is 0 if all low 12 bits of X are 0, 1 otherwise - # bits 13-31 of r0 are 0 - or r4, r4, r0 # correct bit number 12 of X + rlwinm r5, r4, 0, 21, 31 # extract bits 0 to 11 of X + addi r5, r5, 0x7FF # r5 = (X & 0x7FF) + 0x7FF + # bit 12 of r5 is 0 if all low 12 bits of X are 0, 1 otherwise + # bits 13-31 of r5 are 0 + or r4, r4, r5 # correct bit number 12 of X rlwinm r4, r4, 0, 0, 20 # set to 0 bits 0 to 11 of X # Convert to double, then round to single 1: bl __compcert_i64_utod diff --git a/test/regression/Results/int64 b/test/regression/Results/int64 index af444cf6..ae8a3cc1 100644 --- a/test/regression/Results/int64 +++ b/test/regression/Results/int64 @@ -335,6 +335,48 @@ utof x = 0 stof x = 0 x = 0 +y = 52ce6b4000000063 +-x = 0 +x + y = 52ce6b4000000063 +x - y = ad3194bfffffff9d +x * y = 0 +x /u y = 0 +x %u y = 0 +x /s y = 0 +x %s y = 0 +x /u y2 = 0 +x %u y2 = 0 +x /s y3 = 0 +x %s y3 = 0 +x /u 3 = 0 +x %u 3 = 0 +x /s 3 = 0 +x %s 3 = 0 +x /u 5 = 0 +x %u 5 = 0 +x /s 5 = 0 +x %s 5 = 0 +x /u 11 = 0 +x %u 11 = 0 +x /s 11 = 0 +x %s 11 = 0 +~x = ffffffffffffffff +x & y = 0 +x | y = 52ce6b4000000063 +x ^ y = 52ce6b4000000063 +x << i = 0 +x >>u i = 0 +x >>s i = 0 +x cmpu y = lt +x cmps y = lt +utod x = 0 +dtou f = 0 +stod x = 0 +dtos f = 0 +utof x = 0 +stof x = 0 + +x = 0 y = 14057b7ef767814f -x = 0 x + y = 14057b7ef767814f @@ -755,6 +797,48 @@ utof x = 3f800000 stof x = 3f800000 x = 1 +y = 52ce6b4000000063 +-x = ffffffffffffffff +x + y = 52ce6b4000000064 +x - y = ad3194bfffffff9e +x * y = 52ce6b4000000063 +x /u y = 0 +x %u y = 1 +x /s y = 0 +x %s y = 1 +x /u y2 = 0 +x %u y2 = 1 +x /s y3 = 0 +x %s y3 = 1 +x /u 3 = 0 +x %u 3 = 1 +x /s 3 = 0 +x %s 3 = 1 +x /u 5 = 0 +x %u 5 = 1 +x /s 5 = 0 +x %s 5 = 1 +x /u 11 = 0 +x %u 11 = 1 +x /s 11 = 0 +x %s 11 = 1 +~x = fffffffffffffffe +x & y = 1 +x | y = 52ce6b4000000063 +x ^ y = 52ce6b4000000062 +x << i = 800000000 +x >>u i = 0 +x >>s i = 0 +x cmpu y = lt +x cmps y = lt +utod x = 3ff0000000000000 +dtou f = 0 +stod x = 3ff0000000000000 +dtos f = 0 +utof x = 3f800000 +stof x = 3f800000 + +x = 1 y = 9af678222e728119 -x = ffffffffffffffff x + y = 9af678222e72811a @@ -1175,6 +1259,48 @@ utof x = 5f800000 stof x = bf800000 x = ffffffffffffffff +y = 52ce6b4000000063 +-x = 1 +x + y = 52ce6b4000000062 +x - y = ad3194bfffffff9c +x * y = ad3194bfffffff9d +x /u y = 3 +x %u y = 794be3ffffffed6 +x /s y = 0 +x %s y = ffffffffffffffff +x /u y2 = 3176fe836 +x %u y2 = 3683607f +x /s y3 = 0 +x %s y3 = ffffffffffffffff +x /u 3 = 5555555555555555 +x %u 3 = 0 +x /s 3 = 0 +x %s 3 = ffffffffffffffff +x /u 5 = 3333333333333333 +x %u 5 = 0 +x /s 5 = 0 +x %s 5 = ffffffffffffffff +x /u 11 = 1745d1745d1745d1 +x %u 11 = 4 +x /s 11 = 0 +x %s 11 = ffffffffffffffff +~x = 0 +x & y = 52ce6b4000000063 +x | y = ffffffffffffffff +x ^ y = ad3194bfffffff9c +x << i = fffffff800000000 +x >>u i = 1fffffff +x >>s i = ffffffffffffffff +x cmpu y = gt +x cmps y = lt +utod x = 43f0000000000000 +dtou f = 68db8bac710cb +stod x = bff0000000000000 +dtos f = 0 +utof x = 5f800000 +stof x = bf800000 + +x = ffffffffffffffff y = 62354cda6226d1f3 -x = 1 x + y = 62354cda6226d1f2 @@ -1595,6 +1721,48 @@ utof x = 4f000000 stof x = 4f000000 x = 7fffffff +y = 52ce6b4000000063 +-x = ffffffff80000001 +x + y = 52ce6b4080000062 +x - y = ad3194c07fffff9c +x * y = ad3194f17fffff9d +x /u y = 0 +x %u y = 7fffffff +x /s y = 0 +x %s y = 7fffffff +x /u y2 = 1 +x %u y2 = 2d3194bf +x /s y3 = 1 +x %s y3 = 2d3194bf +x /u 3 = 2aaaaaaa +x %u 3 = 1 +x /s 3 = 2aaaaaaa +x %s 3 = 1 +x /u 5 = 19999999 +x %u 5 = 2 +x /s 5 = 19999999 +x %s 5 = 2 +x /u 11 = ba2e8ba +x %u 11 = 1 +x /s 11 = ba2e8ba +x %s 11 = 1 +~x = ffffffff80000000 +x & y = 63 +x | y = 52ce6b407fffffff +x ^ y = 52ce6b407fffff9c +x << i = fffffff800000000 +x >>u i = 0 +x >>s i = 0 +x cmpu y = lt +x cmps y = lt +utod x = 41dfffffffc00000 +dtou f = 346dc +stod x = 41dfffffffc00000 +dtos f = 346dc +utof x = 4f000000 +stof x = 4f000000 + +x = 7fffffff y = 144093704fadba5d -x = ffffffff80000001 x + y = 14409370cfadba5c @@ -2015,6 +2183,48 @@ utof x = 4f000000 stof x = 4f000000 x = 80000000 +y = 52ce6b4000000063 +-x = ffffffff80000000 +x + y = 52ce6b4080000063 +x - y = ad3194c07fffff9d +x * y = 3180000000 +x /u y = 0 +x %u y = 80000000 +x /s y = 0 +x %s y = 80000000 +x /u y2 = 1 +x %u y2 = 2d3194c0 +x /s y3 = 1 +x %s y3 = 2d3194c0 +x /u 3 = 2aaaaaaa +x %u 3 = 2 +x /s 3 = 2aaaaaaa +x %s 3 = 2 +x /u 5 = 19999999 +x %u 5 = 3 +x /s 5 = 19999999 +x %s 5 = 3 +x /u 11 = ba2e8ba +x %u 11 = 2 +x /s 11 = ba2e8ba +x %s 11 = 2 +~x = ffffffff7fffffff +x & y = 0 +x | y = 52ce6b4080000063 +x ^ y = 52ce6b4080000063 +x << i = 0 +x >>u i = 0 +x >>s i = 0 +x cmpu y = lt +x cmps y = lt +utod x = 41e0000000000000 +dtou f = 346dc +stod x = 41e0000000000000 +dtos f = 346dc +utof x = 4f000000 +stof x = 4f000000 + +x = 80000000 y = 7b985bc1e7bce4d7 -x = ffffffff80000000 x + y = 7b985bc267bce4d7 @@ -2435,6 +2645,48 @@ utof x = 5f000000 stof x = 5f000000 x = 7fffffffffffffff +y = 52ce6b4000000063 +-x = 8000000000000001 +x + y = d2ce6b4000000062 +x - y = 2d3194bfffffff9c +x * y = 2d3194bfffffff9d +x /u y = 1 +x %u y = 2d3194bfffffff9c +x /s y = 1 +x %s y = 2d3194bfffffff9c +x /u y2 = 18bb7f41b +x %u y2 = 1b41b03f +x /s y3 = 18bb7f41b +x %s y3 = 1b41b03f +x /u 3 = 2aaaaaaaaaaaaaaa +x %u 3 = 1 +x /s 3 = 2aaaaaaaaaaaaaaa +x %s 3 = 1 +x /u 5 = 1999999999999999 +x %u 5 = 2 +x /s 5 = 1999999999999999 +x %s 5 = 2 +x /u 11 = ba2e8ba2e8ba2e8 +x %u 11 = 7 +x /s 11 = ba2e8ba2e8ba2e8 +x %s 11 = 7 +~x = 8000000000000000 +x & y = 52ce6b4000000063 +x | y = 7fffffffffffffff +x ^ y = 2d3194bfffffff9c +x << i = fffffff800000000 +x >>u i = fffffff +x >>s i = fffffff +x cmpu y = gt +x cmps y = gt +utod x = 43e0000000000000 +dtou f = 346dc5d638865 +stod x = 43e0000000000000 +dtos f = 346dc5d638865 +utof x = 5f000000 +stof x = 5f000000 + +x = 7fffffffffffffff y = a220229ec164ffe1 -x = 8000000000000001 x + y = 2220229ec164ffe0 @@ -2855,6 +3107,48 @@ utof x = 5f000000 stof x = df000000 x = 8000000000000000 +y = 52ce6b4000000063 +-x = 8000000000000000 +x + y = d2ce6b4000000063 +x - y = 2d3194bfffffff9d +x * y = 8000000000000000 +x /u y = 1 +x %u y = 2d3194bfffffff9d +x /s y = ffffffffffffffff +x %s y = d2ce6b4000000063 +x /u y2 = 18bb7f41b +x %u y2 = 1b41b040 +x /s y3 = fffffffe74480be5 +x %s y3 = ffffffffe4be4fc0 +x /u 3 = 2aaaaaaaaaaaaaaa +x %u 3 = 2 +x /s 3 = d555555555555556 +x %s 3 = fffffffffffffffe +x /u 5 = 1999999999999999 +x %u 5 = 3 +x /s 5 = e666666666666667 +x %s 5 = fffffffffffffffd +x /u 11 = ba2e8ba2e8ba2e8 +x %u 11 = 8 +x /s 11 = f45d1745d1745d18 +x %s 11 = fffffffffffffff8 +~x = 7fffffffffffffff +x & y = 0 +x | y = d2ce6b4000000063 +x ^ y = d2ce6b4000000063 +x << i = 0 +x >>u i = 10000000 +x >>s i = fffffffff0000000 +x cmpu y = gt +x cmps y = lt +utod x = 43e0000000000000 +dtou f = 346dc5d638865 +stod x = c3e0000000000000 +dtos f = fffcb923a29c779b +utof x = 5f000000 +stof x = df000000 + +x = 8000000000000000 y = c73aa0d9a415dfb -x = 8000000000000000 x + y = 8c73aa0d9a415dfb @@ -3275,6 +3569,48 @@ utof x = 4f800000 stof x = 4f800000 x = 100000003 +y = 52ce6b4000000063 +-x = fffffffefffffffd +x + y = 52ce6b4100000066 +x - y = ad3194c0ffffffa0 +x * y = f86b422300000129 +x /u y = 0 +x %u y = 100000003 +x /s y = 0 +x %s y = 100000003 +x /u y2 = 3 +x %u y2 = 794be43 +x /s y3 = 3 +x %s y3 = 794be43 +x /u 3 = 55555556 +x %u 3 = 1 +x /s 3 = 55555556 +x %s 3 = 1 +x /u 5 = 33333333 +x %u 5 = 4 +x /s 5 = 33333333 +x %s 5 = 4 +x /u 11 = 1745d174 +x %u 11 = 7 +x /s 11 = 1745d174 +x %s 11 = 7 +~x = fffffffefffffffc +x & y = 3 +x | y = 52ce6b4100000063 +x ^ y = 52ce6b4100000060 +x << i = 1800000000 +x >>u i = 0 +x >>s i = 0 +x cmpu y = lt +x cmps y = lt +utod x = 41f0000000300000 +dtou f = 68db8 +stod x = 41f0000000300000 +dtos f = 68db8 +utof x = 4f800000 +stof x = 4f800000 + +x = 100000003 y = e9bcd26890f095a5 -x = fffffffefffffffd x + y = e9bcd26990f095a8 @@ -3358,47 +3694,467 @@ dtos f = 14bb101261e18 utof x = 5e4a72c9 stof x = 5e4a72c9 -x = 8362aa9340fe215f -y = f986342416ec8002 --x = 7c9d556cbf01dea1 -x + y = 7ce8deb757eaa161 -x - y = 89dc766f2a11a15d -x * y = e4a2b426803fc2be +x = 52ce6b4000000063 +y = 0 +-x = ad3194bfffffff9d +x + y = 52ce6b4000000063 +x - y = 52ce6b4000000063 +x * y = 0 x /u y = 0 -x %u y = 8362aa9340fe215f -x /s y = 13 -x %s y = fe6ccbe58d70a139 -x /u y2 = 86cb918b -x %u y2 = 910b6dd3 -x /s y3 = 133e437097 -x %s y3 = fffffffffe99a023 -x /u 3 = 2bcb8e3115aa0b1f -x %u 3 = 2 -x /s 3 = d67638dbc054b5cb -x %s 3 = fffffffffffffffe -x /u 5 = 1a46eeea4032d379 -x %u 5 = 2 -x /s 5 = e713bbb70cffa047 -x %s 5 = fffffffffffffffc -x /u 11 = bf1b26a7a45a5f1 -x %u 11 = 4 -x /s 11 = f4abe0f61d2e6020 -x %s 11 = ffffffffffffffff -~x = 7c9d556cbf01dea0 -x & y = 8102200000ec0002 -x | y = fbe6beb756fea15f -x ^ y = 7ae49eb75612a15d -x << i = d8aaa4d03f8857c -x >>u i = 20d8aaa4d03f8857 -x >>s i = e0d8aaa4d03f8857 +x %u y = 0 +x /s y = 0 +x %s y = 0 +x /u y2 = 0 +x %u y2 = 0 +x /s y3 = 0 +x %s y3 = 0 +x /u 3 = 1b9a23c000000021 +x %u 3 = 0 +x /s 3 = 1b9a23c000000021 +x %s 3 = 0 +x /u 5 = 108faf0ccccccce0 +x %u 5 = 3 +x /s 5 = 108faf0ccccccce0 +x %s 5 = 3 +x /u 11 = 7872105d1745d20 +x %u 11 = 3 +x /s 11 = 7872105d1745d20 +x %s 11 = 3 +~x = ad3194bfffffff9c +x & y = 0 +x | y = 52ce6b4000000063 +x ^ y = 52ce6b4000000063 +x << i = 52ce6b4000000063 +x >>u i = 52ce6b4000000063 +x >>s i = 52ce6b4000000063 +x cmpu y = gt +x cmps y = gt +utod x = 43d4b39ad0000000 +dtou f = 21eadf559b3d0 +stod x = 43d4b39ad0000000 +dtos f = 21eadf559b3d0 +utof x = 5ea59cd7 +stof x = 5ea59cd7 + +x = 52ce6b4000000063 +y = 1 +-x = ad3194bfffffff9d +x + y = 52ce6b4000000064 +x - y = 52ce6b4000000062 +x * y = 52ce6b4000000063 +x /u y = 52ce6b4000000063 +x %u y = 0 +x /s y = 52ce6b4000000063 +x %s y = 0 +x /u y2 = 0 +x %u y2 = 0 +x /s y3 = 0 +x %s y3 = 0 +x /u 3 = 1b9a23c000000021 +x %u 3 = 0 +x /s 3 = 1b9a23c000000021 +x %s 3 = 0 +x /u 5 = 108faf0ccccccce0 +x %u 5 = 3 +x /s 5 = 108faf0ccccccce0 +x %s 5 = 3 +x /u 11 = 7872105d1745d20 +x %u 11 = 3 +x /s 11 = 7872105d1745d20 +x %s 11 = 3 +~x = ad3194bfffffff9c +x & y = 1 +x | y = 52ce6b4000000063 +x ^ y = 52ce6b4000000062 +x << i = a59cd680000000c6 +x >>u i = 296735a000000031 +x >>s i = 296735a000000031 +x cmpu y = gt +x cmps y = gt +utod x = 43d4b39ad0000000 +dtou f = 21eadf559b3d0 +stod x = 43d4b39ad0000000 +dtos f = 21eadf559b3d0 +utof x = 5ea59cd7 +stof x = 5ea59cd7 + +x = 52ce6b4000000063 +y = ffffffffffffffff +-x = ad3194bfffffff9d +x + y = 52ce6b4000000062 +x - y = 52ce6b4000000064 +x * y = ad3194bfffffff9d +x /u y = 0 +x %u y = 52ce6b4000000063 +x /s y = ad3194bfffffff9d +x %s y = 0 +x /u y2 = 52ce6b40 +x %u y2 = 52ce6ba3 +x /s y3 = ad3194bfffffff9d +x %s y3 = 0 +x /u 3 = 1b9a23c000000021 +x %u 3 = 0 +x /s 3 = 1b9a23c000000021 +x %s 3 = 0 +x /u 5 = 108faf0ccccccce0 +x %u 5 = 3 +x /s 5 = 108faf0ccccccce0 +x %s 5 = 3 +x /u 11 = 7872105d1745d20 +x %u 11 = 3 +x /s 11 = 7872105d1745d20 +x %s 11 = 3 +~x = ad3194bfffffff9c +x & y = 52ce6b4000000063 +x | y = ffffffffffffffff +x ^ y = ad3194bfffffff9c +x << i = 8000000000000000 +x >>u i = 0 +x >>s i = 0 +x cmpu y = lt +x cmps y = gt +utod x = 43d4b39ad0000000 +dtou f = 21eadf559b3d0 +stod x = 43d4b39ad0000000 +dtos f = 21eadf559b3d0 +utof x = 5ea59cd7 +stof x = 5ea59cd7 + +x = 52ce6b4000000063 +y = 7fffffff +-x = ad3194bfffffff9d +x + y = 52ce6b4080000062 +x - y = 52ce6b3f80000064 +x * y = ad3194f17fffff9d +x /u y = a59cd681 +x %u y = 259cd6e4 +x /s y = a59cd681 +x %s y = 259cd6e4 +x /u y2 = 0 +x %u y2 = 0 +x /s y3 = 0 +x %s y3 = 0 +x /u 3 = 1b9a23c000000021 +x %u 3 = 0 +x /s 3 = 1b9a23c000000021 +x %s 3 = 0 +x /u 5 = 108faf0ccccccce0 +x %u 5 = 3 +x /s 5 = 108faf0ccccccce0 +x %s 5 = 3 +x /u 11 = 7872105d1745d20 +x %u 11 = 3 +x /s 11 = 7872105d1745d20 +x %s 11 = 3 +~x = ad3194bfffffff9c +x & y = 63 +x | y = 52ce6b407fffffff +x ^ y = 52ce6b407fffff9c +x << i = 8000000000000000 +x >>u i = 0 +x >>s i = 0 +x cmpu y = gt +x cmps y = gt +utod x = 43d4b39ad0000000 +dtou f = 21eadf559b3d0 +stod x = 43d4b39ad0000000 +dtos f = 21eadf559b3d0 +utof x = 5ea59cd7 +stof x = 5ea59cd7 + +x = 52ce6b4000000063 +y = 80000000 +-x = ad3194bfffffff9d +x + y = 52ce6b4080000063 +x - y = 52ce6b3f80000063 +x * y = 3180000000 +x /u y = a59cd680 +x %u y = 63 +x /s y = a59cd680 +x %s y = 63 +x /u y2 = 0 +x %u y2 = 0 +x /s y3 = 0 +x %s y3 = 0 +x /u 3 = 1b9a23c000000021 +x %u 3 = 0 +x /s 3 = 1b9a23c000000021 +x %s 3 = 0 +x /u 5 = 108faf0ccccccce0 +x %u 5 = 3 +x /s 5 = 108faf0ccccccce0 +x %s 5 = 3 +x /u 11 = 7872105d1745d20 +x %u 11 = 3 +x /s 11 = 7872105d1745d20 +x %s 11 = 3 +~x = ad3194bfffffff9c +x & y = 0 +x | y = 52ce6b4080000063 +x ^ y = 52ce6b4080000063 +x << i = 52ce6b4000000063 +x >>u i = 52ce6b4000000063 +x >>s i = 52ce6b4000000063 +x cmpu y = gt +x cmps y = gt +utod x = 43d4b39ad0000000 +dtou f = 21eadf559b3d0 +stod x = 43d4b39ad0000000 +dtos f = 21eadf559b3d0 +utof x = 5ea59cd7 +stof x = 5ea59cd7 + +x = 52ce6b4000000063 +y = 7fffffffffffffff +-x = ad3194bfffffff9d +x + y = d2ce6b4000000062 +x - y = d2ce6b4000000064 +x * y = 2d3194bfffffff9d +x /u y = 0 +x %u y = 52ce6b4000000063 +x /s y = 0 +x %s y = 52ce6b4000000063 +x /u y2 = a59cd681 +x %u y2 = 259cd6e4 +x /s y3 = a59cd681 +x %s y3 = 259cd6e4 +x /u 3 = 1b9a23c000000021 +x %u 3 = 0 +x /s 3 = 1b9a23c000000021 +x %s 3 = 0 +x /u 5 = 108faf0ccccccce0 +x %u 5 = 3 +x /s 5 = 108faf0ccccccce0 +x %s 5 = 3 +x /u 11 = 7872105d1745d20 +x %u 11 = 3 +x /s 11 = 7872105d1745d20 +x %s 11 = 3 +~x = ad3194bfffffff9c +x & y = 52ce6b4000000063 +x | y = 7fffffffffffffff +x ^ y = 2d3194bfffffff9c +x << i = 8000000000000000 +x >>u i = 0 +x >>s i = 0 x cmpu y = lt x cmps y = lt -utod x = 43e06c5552681fc4 -dtou f = 35d0c262d14d7 -stod x = c3df27555b2fc078 -dtos f = fffccf536b66040d -utof x = 5f0362ab -stof x = def93aab +utod x = 43d4b39ad0000000 +dtou f = 21eadf559b3d0 +stod x = 43d4b39ad0000000 +dtos f = 21eadf559b3d0 +utof x = 5ea59cd7 +stof x = 5ea59cd7 + +x = 52ce6b4000000063 +y = 8000000000000000 +-x = ad3194bfffffff9d +x + y = d2ce6b4000000063 +x - y = d2ce6b4000000063 +x * y = 8000000000000000 +x /u y = 0 +x %u y = 52ce6b4000000063 +x /s y = 0 +x %s y = 52ce6b4000000063 +x /u y2 = a59cd680 +x %u y2 = 63 +x /s y3 = ffffffff5a632980 +x %s y3 = 63 +x /u 3 = 1b9a23c000000021 +x %u 3 = 0 +x /s 3 = 1b9a23c000000021 +x %s 3 = 0 +x /u 5 = 108faf0ccccccce0 +x %u 5 = 3 +x /s 5 = 108faf0ccccccce0 +x %s 5 = 3 +x /u 11 = 7872105d1745d20 +x %u 11 = 3 +x /s 11 = 7872105d1745d20 +x %s 11 = 3 +~x = ad3194bfffffff9c +x & y = 0 +x | y = d2ce6b4000000063 +x ^ y = d2ce6b4000000063 +x << i = 52ce6b4000000063 +x >>u i = 52ce6b4000000063 +x >>s i = 52ce6b4000000063 +x cmpu y = lt +x cmps y = gt +utod x = 43d4b39ad0000000 +dtou f = 21eadf559b3d0 +stod x = 43d4b39ad0000000 +dtos f = 21eadf559b3d0 +utof x = 5ea59cd7 +stof x = 5ea59cd7 + +x = 52ce6b4000000063 +y = 100000003 +-x = ad3194bfffffff9d +x + y = 52ce6b4100000066 +x - y = 52ce6b3f00000060 +x * y = f86b422300000129 +x /u y = 52ce6b3f +x %u y = 794bea6 +x /s y = 52ce6b3f +x %s y = 794bea6 +x /u y2 = 52ce6b4000000063 +x %u y2 = 0 +x /s y3 = 52ce6b4000000063 +x %s y3 = 0 +x /u 3 = 1b9a23c000000021 +x %u 3 = 0 +x /s 3 = 1b9a23c000000021 +x %s 3 = 0 +x /u 5 = 108faf0ccccccce0 +x %u 5 = 3 +x /s 5 = 108faf0ccccccce0 +x %s 5 = 3 +x /u 11 = 7872105d1745d20 +x %u 11 = 3 +x /s 11 = 7872105d1745d20 +x %s 11 = 3 +~x = ad3194bfffffff9c +x & y = 3 +x | y = 52ce6b4100000063 +x ^ y = 52ce6b4100000060 +x << i = 96735a0000000318 +x >>u i = a59cd680000000c +x >>s i = a59cd680000000c +x cmpu y = gt +x cmps y = gt +utod x = 43d4b39ad0000000 +dtou f = 21eadf559b3d0 +stod x = 43d4b39ad0000000 +dtos f = 21eadf559b3d0 +utof x = 5ea59cd7 +stof x = 5ea59cd7 + +x = 52ce6b4000000063 +y = 52ce6b4000000063 +-x = ad3194bfffffff9d +x + y = a59cd680000000c6 +x - y = 0 +x * y = ba6f38000002649 +x /u y = 1 +x %u y = 0 +x /s y = 1 +x %s y = 0 +x /u y2 = 100000000 +x %u y2 = 63 +x /s y3 = 100000000 +x %s y3 = 63 +x /u 3 = 1b9a23c000000021 +x %u 3 = 0 +x /s 3 = 1b9a23c000000021 +x %s 3 = 0 +x /u 5 = 108faf0ccccccce0 +x %u 5 = 3 +x /s 5 = 108faf0ccccccce0 +x %s 5 = 3 +x /u 11 = 7872105d1745d20 +x %u 11 = 3 +x /s 11 = 7872105d1745d20 +x %s 11 = 3 +~x = ad3194bfffffff9c +x & y = 52ce6b4000000063 +x | y = 52ce6b4000000063 +x ^ y = 0 +x << i = 31800000000 +x >>u i = a59cd68 +x >>s i = a59cd68 +x cmpu y = eq +x cmps y = eq +utod x = 43d4b39ad0000000 +dtou f = 21eadf559b3d0 +stod x = 43d4b39ad0000000 +dtos f = 21eadf559b3d0 +utof x = 5ea59cd7 +stof x = 5ea59cd7 + +x = 52ce6b4000000063 +y = 8362aa9340fe215f +-x = ad3194bfffffff9d +x + y = d63115d340fe21c2 +x - y = cf6bc0acbf01df04 +x * y = 8f1503b22246e7bd +x /u y = 0 +x %u y = 52ce6b4000000063 +x /s y = 0 +x %s y = 52ce6b4000000063 +x /u y2 = a158656f +x %u y2 = 5640ba6 +x /s y3 = ffffffff55e35d11 +x %s y3 = 5f2245a0 +x /u 3 = 1b9a23c000000021 +x %u 3 = 0 +x /s 3 = 1b9a23c000000021 +x %s 3 = 0 +x /u 5 = 108faf0ccccccce0 +x %u 5 = 3 +x /s 5 = 108faf0ccccccce0 +x %s 5 = 3 +x /u 11 = 7872105d1745d20 +x %u 11 = 3 +x /s 11 = 7872105d1745d20 +x %s 11 = 3 +~x = ad3194bfffffff9c +x & y = 2422a0000000043 +x | y = d3eeebd340fe217f +x ^ y = d1acc1d340fe213c +x << i = 3180000000 +x >>u i = a59cd680 +x >>s i = a59cd680 +x cmpu y = lt +x cmps y = gt +utod x = 43d4b39ad0000000 +dtou f = 21eadf559b3d0 +stod x = 43d4b39ad0000000 +dtos f = 21eadf559b3d0 +utof x = 5ea59cd7 +stof x = 5ea59cd7 + +x = f986342416ec8002 +y = 52ce6b4000000063 +-x = 679cbdbe9137ffe +x + y = 4c549f6416ec8065 +x - y = a6b7c8e416ec7f9f +x * y = b9230074dd7580c6 +x /u y = 3 +x %u y = 11af26416ec7ed9 +x /s y = 0 +x %s y = f986342416ec8002 +x /u y2 = 3036abea3 +x %u y2 = 164b642 +x /s y3 = ffffffffebfad66d +x %s y3 = ffffffffcae155c2 +x /u 3 = 532cbc0c07a42aab +x %u 3 = 1 +x /s 3 = fdd766b6b24ed556 +x %s 3 = 0 +x /u 5 = 31e7a40737c8e666 +x %u 5 = 4 +x /s 5 = feb470d40495b334 +x %s 5 = fffffffffffffffe +x /u 11 = 16af1c0347e6f45d +x %u 11 = 3 +x /s 11 = ff694a8eeacfae8c +x %s 11 = fffffffffffffffe +~x = 679cbdbe9137ffd +x & y = 5086200000000002 +x | y = fbce7f6416ec8063 +x ^ y = ab485f6416ec8061 +x << i = b764001000000000 +x >>u i = 1f30c684 +x >>s i = ffffffffff30c684 +x cmpu y = gt +x cmps y = lt +utod x = 43ef30c68482dd90 +dtou f = 6634832136daf +stod x = c399e72f6fa44e00 +dtos f = ffffd58f774c5ce4 +utof x = 5f798634 +stof x = dccf397b x = 368083376ba4ffa9 y = 6912b247b79a4904 @@ -7558,3 +8314,45 @@ dtos f = b3fdf698d581 utof x = 5ddbb784 stof x = 5ddbb784 +x = ca9a47c1649d27a7 +y = d56d650045e652aa +-x = 3565b83e9b62d859 +x + y = a007acc1aa837a51 +x - y = f52ce2c11eb6d4fd +x * y = 630e3c88ca19d2e6 +x /u y = 0 +x %u y = ca9a47c1649d27a7 +x /s y = 1 +x %s y = f52ce2c11eb6d4fd +x /u y2 = f3042098 +x %u y2 = 6b092fa7 +x /s y3 = 141176486 +x %s y3 = ffffffffdee649a7 +x /u 3 = 4388c295cc34628d +x %u 3 = 0 +x /s 3 = ee336d4076df0d38 +x %s 3 = ffffffffffffffff +x /u 5 = 2885418d141f6e54 +x %u 5 = 3 +x /s 5 = f5520e59e0ec3b22 +x %s 5 = fffffffffffffffd +x /u 11 = 126b1dcbc3541ae0 +x %u 11 = 7 +x /s 11 = fb254c57663cd510 +x %s 11 = fffffffffffffff7 +~x = 3565b83e9b62d858 +x & y = c0084500448402a2 +x | y = dfff67c165ff77af +x ^ y = 1ff722c1217b750d +x << i = 749e9c0000000000 +x >>u i = 32a691 +x >>s i = fffffffffff2a691 +x cmpu y = lt +x cmps y = lt +utod x = 43e95348f82c93a5 +dtou f = 52fc6dac31674 +stod x = c3cab2dc1f4db16c +dtos f = fffea20e1ffc05aa +utof x = 5f4a9a48 +stof x = de5596e1 + diff --git a/test/regression/int64.c b/test/regression/int64.c index d9785e95..0da9602d 100644 --- a/test/regression/int64.c +++ b/test/regression/int64.c @@ -103,7 +103,8 @@ u64 special_values[] = { 0x80000000LLU, 0x7FFFFFFFFFFFFFFFLLU, 0x8000000000000000LLU, - 0x100000003LLU + 0x100000003LLU, + 0x52ce6b4000000063LLU }; #define NUM_SPECIAL_VALUES (sizeof(special_values) / sizeof(u64)) |