From 2603f8004379bb9f1b0e70789c05860011cf5517 Mon Sep 17 00:00:00 2001 From: Ralf Vogler Date: Tue, 3 Aug 2021 14:51:57 +0200 Subject: [PATCH 1/5] include arm64.h on arm64 to define missing __uint128_t on macOS https://github.com/goblint/cil/issues/41 --- includes/arm64.h | 9 +++++++++ scripts/set_version.sh | 1 + src/maingoblint.ml | 3 +++ 3 files changed, 13 insertions(+) create mode 100644 includes/arm64.h diff --git a/includes/arm64.h b/includes/arm64.h new file mode 100644 index 0000000000..8dea000e0f --- /dev/null +++ b/includes/arm64.h @@ -0,0 +1,9 @@ +// see https://github.com/goblint/cil/issues/41 +// If goblint pre-processes a file including stdlib.h on an Apple M1 machine, +// it will include /Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/mach/arm/_structs.h +// which uses __uint128_t which is somehow not defined before. + +#if defined(__arm64__) + // typedef unsigned __int128 uint128_t; // https://stackoverflow.com/a/34588884 TODO __int128 exists in CIL but fails; see https://github.com/goblint/cil/issues/41 + typedef unsigned long long __uint128_t; // TODO wrong! use the above once fixed. This the definition for __uint64_t +#endif diff --git a/scripts/set_version.sh b/scripts/set_version.sh index 95cea151fb..8dd76b53fc 100755 --- a/scripts/set_version.sh +++ b/scripts/set_version.sh @@ -15,6 +15,7 @@ if [ ! -f src/config.ml ]; then echo "let tracking = false" echo "let experimental = false" echo "let cpp = \"cpp\"" + echo "let mach = \"$(uname -m)\"" } >> src/config.ml fi diff --git a/src/maingoblint.ml b/src/maingoblint.ml index a688472dbd..bb9c96fa60 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -175,6 +175,9 @@ let preprocess_files () = (* Preprocessor flags *) let cppflags = ref (get_string "cppflags") in + if Config.mach = "arm64" then + cppflags := !cppflags ^ "-include " ^ Filename.concat exe_dir "includes/arm64.h"; + (* the base include directory *) let include_dir = let incl1 = Filename.concat exe_dir "includes" in From 4e6858d98c1c167f6c8512db5c2eb59ed296fd68 Mon Sep 17 00:00:00 2001 From: Ralf Vogler Date: Thu, 5 Aug 2021 10:25:44 +0200 Subject: [PATCH 2/5] link in comment that long long is just 64 bit --- includes/arm64.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/includes/arm64.h b/includes/arm64.h index 8dea000e0f..e418597392 100644 --- a/includes/arm64.h +++ b/includes/arm64.h @@ -4,6 +4,6 @@ // which uses __uint128_t which is somehow not defined before. #if defined(__arm64__) - // typedef unsigned __int128 uint128_t; // https://stackoverflow.com/a/34588884 TODO __int128 exists in CIL but fails; see https://github.com/goblint/cil/issues/41 - typedef unsigned long long __uint128_t; // TODO wrong! use the above once fixed. This the definition for __uint64_t + // typedef unsigned __int128 uint128_t; // https://stackoverflow.com/a/34588884 __int128 exists in gcc and in CIL but fails there; see https://github.com/goblint/cil/issues/41 + typedef unsigned long long __uint128_t; // TODO Use the above once fixed! This is wrong since long long is just 64 bit. See https://github.com/goblint/cil/issues/41#issuecomment-893266843 #endif From 028432b5c3f612614e25001a6b060628d3d97125 Mon Sep 17 00:00:00 2001 From: Ralf Vogler Date: Thu, 14 Oct 2021 02:13:52 +0200 Subject: [PATCH 3/5] only x86 linux-headers -> always preprocess kernel as x86_64 --- src/maingoblint.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index bb9c96fa60..b56dcc3c20 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -170,7 +170,7 @@ let preprocess_files () = (* Handy (almost) constants. *) let kernel_root = Filename.concat exe_dir "linux-headers" in let kernel_dir = kernel_root ^ "/include" in - let arch_dir = kernel_root ^ "/arch/x86/include" in + let arch_dir = kernel_root ^ "/arch/x86/include" in (* TODO add arm64: https://github.com/goblint/analyzer/issues/312 *) (* Preprocessor flags *) let cppflags = ref (get_string "cppflags") in @@ -239,7 +239,7 @@ let preprocess_files () = if get_bool "kernel" then ( let preconf = Filename.concat include_dir "linux/goblint_preconf.h" in let autoconf = Filename.concat kernel_dir "linux/kconfig.h" in - cppflags := "-D__KERNEL__ -U__i386__ -include " ^ preconf ^ " -include " ^ autoconf ^ " " ^ !cppflags; + cppflags := "-D__KERNEL__ -U__i386__ -D__x86_64__ -include " ^ preconf ^ " -include " ^ autoconf ^ " " ^ !cppflags; (* These are not just random permutations of directories, but based on USERINCLUDE from the * Linux kernel Makefile (in the root directory of the kernel distribution). *) includes := !includes ^ " -I" ^ String.concat " -I" [ From 519405d7baa71a15fb18e5e97b272cdc56379526 Mon Sep 17 00:00:00 2001 From: Ralf Vogler Date: Thu, 14 Oct 2021 02:16:06 +0200 Subject: [PATCH 4/5] rm includes/arm64.h; use cil which supports 128bit ints https://github.com/goblint/cil/pull/49 --- goblint.opam.template | 2 +- includes/arm64.h | 9 --------- src/cdomains/intDomain.ml | 4 +++- src/maingoblint.ml | 3 --- 4 files changed, 4 insertions(+), 14 deletions(-) delete mode 100644 includes/arm64.h diff --git a/goblint.opam.template b/goblint.opam.template index e42816dba3..4da0f54027 100644 --- a/goblint.opam.template +++ b/goblint.opam.template @@ -1,3 +1,3 @@ pin-depends: [ - [ "goblint-cil.1.8.1" "git+https://github.com/goblint/cil.git#208d2a2f9e51a42ee0a036f4587624ac7ac23ccb" ] + [ "goblint-cil.1.8.1" "git+https://github.com/goblint/cil.git#c16dddf74f6053a8b3fac07ca2feff18d4d56964" ] ] diff --git a/includes/arm64.h b/includes/arm64.h deleted file mode 100644 index e418597392..0000000000 --- a/includes/arm64.h +++ /dev/null @@ -1,9 +0,0 @@ -// see https://github.com/goblint/cil/issues/41 -// If goblint pre-processes a file including stdlib.h on an Apple M1 machine, -// it will include /Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/mach/arm/_structs.h -// which uses __uint128_t which is somehow not defined before. - -#if defined(__arm64__) - // typedef unsigned __int128 uint128_t; // https://stackoverflow.com/a/34588884 __int128 exists in gcc and in CIL but fails there; see https://github.com/goblint/cil/issues/41 - typedef unsigned long long __uint128_t; // TODO Use the above once fixed! This is wrong since long long is just 64 bit. See https://github.com/goblint/cil/issues/41#issuecomment-893266843 -#endif diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml index 9e9b82f332..74e888111c 100644 --- a/src/cdomains/intDomain.ml +++ b/src/cdomains/intDomain.ml @@ -286,7 +286,7 @@ struct let equal x y = if x.ikind <> y.ikind then false else I.equal x.v y.v let hash x = - let ikind_to_int (ikind: ikind) = match ikind with + let ikind_to_int (ikind: ikind) = match ikind with (* TODO replace with `int_of_string % Batteries.dump` or derive *) | IChar -> 0 | ISChar -> 1 | IUChar -> 2 @@ -299,6 +299,8 @@ struct | IULong -> 9 | ILongLong -> 10 | IULongLong -> 11 + | IInt128 -> 12 + | IUInt128 -> 13 in 3 * (I.hash x.v) + 5 * (ikind_to_int x.ikind) let compare x y = let ik_c = compare x.ikind y.ikind in diff --git a/src/maingoblint.ml b/src/maingoblint.ml index b56dcc3c20..e7164807c2 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -175,9 +175,6 @@ let preprocess_files () = (* Preprocessor flags *) let cppflags = ref (get_string "cppflags") in - if Config.mach = "arm64" then - cppflags := !cppflags ^ "-include " ^ Filename.concat exe_dir "includes/arm64.h"; - (* the base include directory *) let include_dir = let incl1 = Filename.concat exe_dir "includes" in From 62302615419a47839307d8a3a24c710a3cee1afa Mon Sep 17 00:00:00 2001 From: Ralf Vogler Date: Thu, 14 Oct 2021 09:05:56 +0200 Subject: [PATCH 5/5] also update goblint-cil in goblint.opam.locked --- goblint.opam.locked | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/goblint.opam.locked b/goblint.opam.locked index 97ea3ceef1..466582b59c 100644 --- a/goblint.opam.locked +++ b/goblint.opam.locked @@ -67,7 +67,7 @@ build: [ ] dev-repo: "git+https://github.com/goblint/analyzer.git" pin-depends: [ - [ "goblint-cil.1.8.1" "git+https://github.com/goblint/cil.git#208d2a2f9e51a42ee0a036f4587624ac7ac23ccb" ] + [ "goblint-cil.1.8.1" "git+https://github.com/goblint/cil.git#c16dddf74f6053a8b3fac07ca2feff18d4d56964" ] ] name: "goblint" version: "dev"