Skip to content

support Apple M1 (arm64), cpp kernel as x86_64 #311

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
vogler merged 6 commits into from
Oct 14, 2021
Merged

support Apple M1 (arm64), cpp kernel as x86_64 #311

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
2603f80
include arm64.h on arm64 to define missing __uint128_t on macOS
vogler Aug 3, 2021
4e6858d
link in comment that long long is just 64 bit
vogler Aug 5, 2021
028432b
only x86 linux-headers -> always preprocess kernel as x86_64
vogler Oct 14, 2021
519405d
rm includes/arm64.h; use cil which supports 128bit ints
vogler Oct 14, 2021
6230261
also update goblint-cil in goblint.opam.locked
vogler Oct 14, 2021
e2c4388
Merge branch 'master' into arm64
vogler Oct 14, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion goblint.opam.locked
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,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" ]
[ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
[ "zarith.1.12-gob0" "git+https://github.com/goblint/Zarith.git#goblint-release-1.12" ]
[ "apron.v0.9.13" "git+https://github.com/antoinemine/apron.git#c852ebcc89e5cf4a5a3318e7c13c73e1756abb11"]
Expand Down
2 changes: 1 addition & 1 deletion goblint.opam.template
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
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" ]
[ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
[ "zarith.1.12-gob0" "git+https://github.com/goblint/Zarith.git#goblint-release-1.12" ]
[ "apron.v0.9.13" "git+https://github.com/antoinemine/apron.git#c852ebcc89e5cf4a5a3318e7c13c73e1756abb11"]
Expand Down
1 change: 1 addition & 0 deletions scripts/set_version.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ if [ ! -f src/config.ml ]; then
{
echo "let tracing = false"
echo "let cpp = \"cpp\""
echo "let mach = \"$(uname -m)\""
} >> src/config.ml
fi

Expand Down
4 changes: 3 additions & 1 deletion src/cdomains/intDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -293,7 +293,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
Expand All @@ -306,6 +306,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
Expand Down
4 changes: 2 additions & 2 deletions src/maingoblint.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -168,7 +168,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
Expand Down Expand Up @@ -234,7 +234,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" [
Expand Down