Merge pull request #311 from goblint/arm64

support Apple M1 (`arm64`), cpp kernel as `x86_64`
goblint · Oct 14, 2021 · 9d1d189 · 9d1d189
2 parents e168a4e + e2c4388
commit 9d1d189
Show file tree

Hide file tree

Showing 5 changed files with 8 additions and 5 deletions.
diff --git a/goblint.opam.locked b/goblint.opam.locked
@@ -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"]

diff --git a/goblint.opam.template b/goblint.opam.template
@@ -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"]

diff --git a/scripts/set_version.sh b/scripts/set_version.sh
@@ -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
 

diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml
@@ -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
@@ -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

diff --git a/src/maingoblint.ml b/src/maingoblint.ml
@@ -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
@@ -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" [