Merge pull request #1574 from goblint/machdep-arch

Change `Machdep` based on SV-COMP architecture

Author: sim642

goblint.opam

@@ -97,7 +97,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # also remember to generate/adjust goblint.opam.locked!
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
-  [ "goblint-cil.2.0.4" "git+https://github.com/goblint/cil.git#04b8a45a7d20425c7b6c8abe1ad094abc063922b" ]
+  [ "goblint-cil.2.0.4" "git+https://github.com/goblint/cil.git#9f4fac450c02bc61a13717784515056b185794cd" ]
 ]
 depexts: [
   ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}

goblint.opam.locked

@@ -140,7 +140,7 @@ post-messages: [
 pin-depends: [
   [
     "goblint-cil.2.0.4"
-    "git+https://github.com/goblint/cil.git#04b8a45a7d20425c7b6c8abe1ad094abc063922b"
+    "git+https://github.com/goblint/cil.git#9f4fac450c02bc61a13717784515056b185794cd"
   ]
 ]
 depexts: ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}

goblint.opam.template

@@ -2,7 +2,7 @@
 # also remember to generate/adjust goblint.opam.locked!
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
-  [ "goblint-cil.2.0.4" "git+https://github.com/goblint/cil.git#04b8a45a7d20425c7b6c8abe1ad094abc063922b" ]
+  [ "goblint-cil.2.0.4" "git+https://github.com/goblint/cil.git#9f4fac450c02bc61a13717784515056b185794cd" ]
 ]
 depexts: [
   ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}

src/analyses/base.ml

@@ -171,7 +171,7 @@ struct
    * Abstract evaluation functions
    **************************************************************************)
 
-  let iDtoIdx = ID.cast_to (Cilfacade.ptrdiff_ikind ())
+  let iDtoIdx x = ID.cast_to (Cilfacade.ptrdiff_ikind ()) x
 
   let unop_ID = function
     | Neg  -> ID.neg

src/cdomain/value/cdomains/arrayDomain.ml

@@ -834,7 +834,7 @@ end
 let array_oob_check ( type a ) (module Idx: IntDomain.Z with type t = a) (x, l) (e, v) =
   if GobConfig.get_bool "ana.arrayoob" then (* The purpose of the following 2 lines is to give the user extra info about the array oob *)
     let idx_before_end = Idx.to_bool (Idx.lt v l) (* check whether index is before the end of the array *)
-    and idx_after_start = Idx.to_bool (Idx.ge v (Idx.of_int Cil.ILong Z.zero)) in (* check whether the index is non-negative *)
+    and idx_after_start = Idx.to_bool (Idx.ge v (Idx.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero)) in (* check whether the index is non-negative *)
     (* For an explanation of the warning types check the Pull Request #255 *)
     match(idx_after_start, idx_before_end) with
     | Some true, Some true -> (* Certainly in bounds on both sides.*)

src/common/util/cilfacade.ml

@@ -47,7 +47,20 @@ let init_options () =
   Mergecil.merge_inlines := get_bool "cil.merge.inlines";
   Cil.cstd := Cil.cstd_of_string (get_string "cil.cstd");
   Cil.gnu89inline := get_bool "cil.gnu89inline";
-  Cabs2cil.addNestedScopeAttr := get_bool "cil.addNestedScopeAttr"
+  Cabs2cil.addNestedScopeAttr := get_bool "cil.addNestedScopeAttr";
+
+  if get_bool "ana.sv-comp.enabled" then (
+    let machine = match get_string "exp.architecture" with
+      | "32bit" -> Machdep.gcc32
+      | "64bit" -> Machdep.gcc64
+      | _ -> assert false
+    in
+    match machine with
+    | Some _ -> Cil.envMachine := machine
+    | None ->
+      GobRef.wrap AnalysisState.should_warn true (fun () -> Messages.msg_final Error ~category:Unsound "Machine definition not available for selected architecture");
+      Logs.error "Machine definition not available for selected architecture, defaulting to host"
+  )
 
 let init () =
   initCIL ();

src/goblint.ml

@@ -5,8 +5,8 @@ open Maingoblint
 (** the main function *)
 let main () =
   try
-    Cilfacade.init ();
     Maingoblint.parse_arguments ();
+    Cilfacade.init ();
 
     (* Timing. *)
     Maingoblint.reset_stats ();

tests/regression/29-svcomp/36-svcomp-arch.c

@@ -0,0 +1,8 @@
+// CRAM
+#include <limits.h>
+
+int main() {
+  long k = INT_MAX;
+  long n = k * k;
+  return 0;
+}

tests/regression/29-svcomp/36-svcomp-arch.t

@@ -0,0 +1,22 @@
+There should be overflow on ILP32:
+
+  $ goblint --enable ana.sv-comp.enabled --set ana.specification "CHECK( init(main()), LTL(G ! overflow) )" --set exp.architecture 32bit 36-svcomp-arch.c
+  [Info] Setting "ana.int.interval" to true
+  [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow (36-svcomp-arch.c:6:8-6:17)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 4
+    dead: 0
+    total lines: 4
+  SV-COMP result: unknown
+
+There shouldn't be an overflow on LP64:
+
+  $ goblint --enable ana.sv-comp.enabled --set ana.specification "CHECK( init(main()), LTL(G ! overflow) )" --set exp.architecture 64bit 36-svcomp-arch.c
+  [Info] Setting "ana.int.interval" to true
+  [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 4
+    dead: 0
+    total lines: 4
+  SV-COMP result: true

tests/regression/29-svcomp/dune

@@ -14,3 +14,7 @@
 
 (cram
  (deps (glob_files *.c)))
+
+(cram
+ (applies_to 36-svcomp-arch)
+ (enabled_if (<> %{system} macosx))) ; https://dune.readthedocs.io/en/stable/reference/boolean-language.html