From 14f89bf9c397a4268d2b47418de234992b008d6c Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Sun, 29 Mar 2020 11:35:58 +0200 Subject: Explicit error messages for ill-formed section attributes (#232) Introduce an error message for section attributes with non string arguments,and another for multiple, ambiguous section attributes. This is more consistent with the handling of other attributes, like packed, than the old behavior of silently ignoring them. --- cfrontend/C2C.ml | 4 ++-- common/Sections.ml | 29 +++++++++++++++++++++-------- common/Sections.mli | 4 ++-- 3 files changed, 25 insertions(+), 12 deletions(-) diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 293e79f0..7f796fe3 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -1234,7 +1234,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 }; @@ -1311,7 +1311,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 -- cgit From f2de2518509f198c5ce958ec06c18e78e896f814 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 30 Mar 2020 12:59:24 +0200 Subject: Add a test for int64 -> float32 conversion This is a special value that causes double rounding with the naive conversion schema int64 -> float64 -> float32. --- test/regression/Results/int64 | 874 ++++++++++++++++++++++++++++++++++++++++-- test/regression/int64.c | 3 +- 2 files changed, 838 insertions(+), 39 deletions(-) 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 @@ -334,6 +334,48 @@ dtos f = 0 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 @@ -754,6 +796,48 @@ dtos f = 0 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 @@ -1174,6 +1258,48 @@ dtos f = 0 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 @@ -1594,6 +1720,48 @@ dtos f = 346dc 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 @@ -2014,6 +2182,48 @@ dtos f = 346dc 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 @@ -2434,6 +2644,48 @@ dtos f = 346dc5d638865 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 @@ -2854,6 +3106,48 @@ dtos f = fffcb923a29c779b 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 @@ -3274,6 +3568,48 @@ dtos f = 68db8 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 @@ -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)) -- cgit From f1abe04e503f1c54c5a50f7b3f3906beca15a760 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 29 Mar 2020 11:20:01 +0200 Subject: Double rounding error in int64->float32 conversions on PowerPC and ARM The "stof" and "utof" runtime functions contain a round-to-odd step that avoids double rounding. However, this step was incorrectly coded on PowerPC (stof and utof), PowerPC64 (utof), and ARM (stof), making round-to-odd ineffective and causing double rounding. Closes: #343 --- runtime/arm/i64_stof.S | 9 ++++----- runtime/powerpc/i64_stof.s | 17 ++++++++--------- runtime/powerpc/i64_utof.s | 10 +++++----- runtime/powerpc64/i64_utof.s | 10 +++++----- 4 files changed, 22 insertions(+), 24 deletions(-) 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 -- cgit From 144f466e3baa41e67d1fa908836a74536d52c201 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 31 Mar 2020 11:06:51 +0200 Subject: Update Changelog --- Changelog | 37 ++++++++++++++++++++++++++++++++++--- 1 file changed, 34 insertions(+), 3 deletions(-) diff --git a/Changelog b/Changelog index 08586da5..9dc858ca 100644 --- a/Changelog +++ b/Changelog @@ -1,7 +1,38 @@ -Coq development: -- Compatibility with Coq version 8.11.0 (#316) +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 ======================= -- cgit From 6dace9be5f4760882f879d3026c168cc9112e150 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 31 Mar 2020 17:48:34 +0200 Subject: Updates for release 3.7 --- Changelog | 3 +++ doc/index.html | 4 +++- 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/Changelog b/Changelog index 9dc858ca..8cf4e548 100644 --- a/Changelog +++ b/Changelog @@ -1,3 +1,6 @@ +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` 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; }

The CompCert verified compiler

Commented Coq development

-

Version 3.6, 2019-09-17

+

Version 3.7, 2020-03-31

Introduction

@@ -101,6 +101,8 @@ See also: Memdata (in-memory rep
  • Determinism: determinism properties of small-step semantics.
  • Op: operators, addressing modes and their semantics. +
  • Builtins: semantics of built-in functions.
    +See also: Builtins0 (target-independent part), Builtins1 (target-dependent part).
  • Unityping: a solver for atomic unification constraints. -- cgit From 76a4ff8f5b37429a614a2a97f628d9d862c93f46 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 31 Mar 2020 18:24:12 +0200 Subject: Updates for release 3.7 --- VERSION | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/VERSION b/VERSION index 92686b06..b60e8d9b 100644 --- a/VERSION +++ b/VERSION @@ -1,3 +1,3 @@ -version=3.6 +version=3.7 buildnr= tag= -- cgit