Merge branch 'master' into assert-ptr

sim642 · sim642 · commit 3694620edbe2 · 2025-02-19T10:51:20.000+02:00
diff --git a/conf/svcomp-ghost.json b/conf/svcomp-ghost.json
@@ -81,7 +81,7 @@
     "autotune": {
       "enabled": true,
       "activated": [
-        "singleThreaded",
+        "reduceAnalyses",
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",
diff --git a/conf/svcomp-validate.json b/conf/svcomp-validate.json
@@ -59,7 +59,7 @@
     "autotune": {
       "enabled": true,
       "activated": [
-        "singleThreaded",
+        "reduceAnalyses",
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",
diff --git a/conf/svcomp.json b/conf/svcomp.json
@@ -58,7 +58,7 @@
     "autotune": {
       "enabled": true,
       "activated": [
-        "singleThreaded",
+        "reduceAnalyses",
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",
diff --git a/conf/svcomp23.json b/conf/svcomp23.json
@@ -63,7 +63,7 @@
     "autotune": {
       "enabled": true,
       "activated": [
-        "singleThreaded",
+        "reduceAnalyses",
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",
diff --git a/conf/svcomp24-validate.json b/conf/svcomp24-validate.json
@@ -79,7 +79,7 @@
     "autotune": {
       "enabled": true,
       "activated": [
-        "singleThreaded",
+        "reduceAnalyses",
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",
diff --git a/conf/svcomp24.json b/conf/svcomp24.json
@@ -78,7 +78,7 @@
     "autotune": {
       "enabled": true,
       "activated": [
-        "singleThreaded",
+        "reduceAnalyses",
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",
diff --git a/conf/svcomp25-validate.json b/conf/svcomp25-validate.json
@@ -59,7 +59,7 @@
     "autotune": {
       "enabled": true,
       "activated": [
-        "singleThreaded",
+        "reduceAnalyses",
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",
diff --git a/conf/svcomp25.json b/conf/svcomp25.json
@@ -58,7 +58,7 @@
     "autotune": {
       "enabled": true,
       "activated": [
-        "singleThreaded",
+        "reduceAnalyses",
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",
diff --git a/conf/svcomp2var.json b/conf/svcomp2var.json
@@ -78,7 +78,7 @@
     "autotune": {
       "enabled": true,
       "activated": [
-        "singleThreaded",
+        "reduceAnalyses",
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",
diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
@@ -395,13 +395,13 @@ struct
             | Le, Some false -> meet_bin (ID.starting ikind (Z.succ l2)) (ID.ending ikind (Z.pred u1))
             | _, _ -> a, b)
          | _ -> a, b)
-      | BOr ->      
-        (* Be careful: inv_exp performs a meet on both arguments of the BOr / BXor. *)        
+      | BOr ->
+        (* Be careful: inv_exp performs a meet on both arguments of the BOr / BXor. *)
         if PrecisionUtil.get_bitfield () then
           (* refinement based on the following idea: bit set to one in c and set to zero in b must be one in a and bit set to zero in c must be zero in a too (analogously for b) *)
-          let ((az, ao), (bz, bo)) = BitfieldDomain.Bitfield.refine_bor (ID.to_bitfield ikind a) (ID.to_bitfield ikind b) (ID.to_bitfield ikind c) in 
+          let ((az, ao), (bz, bo)) = BitfieldDomain.Bitfield.refine_bor (ID.to_bitfield ikind a) (ID.to_bitfield ikind b) (ID.to_bitfield ikind c) in
           ID.meet a (ID.of_bitfield ikind (az, ao)), ID.meet b (ID.of_bitfield ikind (bz, bo))
-        else 
+        else
           (if M.tracing then M.tracel "inv" "Unhandled operator %a" d_binop op;
            (* Be careful: inv_exp performs a meet on both arguments of the BOr / BXor. *)
            (a, b)
@@ -416,7 +416,7 @@ struct
           a, b
       | BAnd ->
         (* we only attempt to refine a here *)
-        let b_int = ID.to_int b in 
+        let b_int = ID.to_int b in
         let a =
           match b_int with
           | Some x when Z.equal x Z.one ->
@@ -426,11 +426,11 @@ struct
              | None -> a)
           | _ -> a
         in
-        if PrecisionUtil.get_bitfield () then 
+        if PrecisionUtil.get_bitfield () then
           (* refinement based on the following idea: bit set to zero in c and set to one in b must be zero in a and bit set to one in c must be one in a too (analogously for b) *)
-          let ((az, ao), (bz, bo)) = BitfieldDomain.Bitfield.refine_band (ID.to_bitfield ikind a) (ID.to_bitfield ikind b) (ID.to_bitfield ikind c) in 
+          let ((az, ao), (bz, bo)) = BitfieldDomain.Bitfield.refine_band (ID.to_bitfield ikind a) (ID.to_bitfield ikind b) (ID.to_bitfield ikind c) in
           ID.meet a (ID.of_bitfield ikind (az, ao)), ID.meet b (ID.of_bitfield ikind (bz, bo))
-        else if b_int = None then 
+        else if b_int = None then
           (if M.tracing then M.tracel "inv" "Unhandled operator %a" d_binop op;
            (a, b)
           )
diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml
@@ -227,7 +227,7 @@ struct
       (* Upon a call to the "Abort" special function in the multi-threaded case, we give up and conservatively warn *)
       warn_for_multi_threaded_due_to_abort man;
       state
-    | Assert { exp; _ } ->
+    | Assert { exp; refine = true; _ } ->
       begin match man.ask (Queries.EvalInt exp) with (* TODO: Queries.eval_bool? *)
         | a when Queries.ID.is_bot a -> M.warn ~category:Assert "assert expression %a is bottom" d_exp exp
         | a ->
diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml
@@ -174,7 +174,7 @@ struct
         `Index (ID.top (), convert_offset ofs)
       | Index (exp, ofs) ->
         let i = match man.ask (Queries.EvalInt exp) with
-          | `Lifted x -> x
+          | `Lifted x -> ID.cast_to (Cilfacade.ptrdiff_ikind ()) x
           | _ -> ID.top_of @@ Cilfacade.ptrdiff_ikind ()
         in
         `Index (i, convert_offset ofs)
diff --git a/src/autoTune.ml b/src/autoTune.ml
@@ -206,29 +206,31 @@ let hasFunction pred =
   calls.calledBy |> FunctionCallMap.exists (fun var _ -> relevant_static var) ||
   calls.dynamicallyCalled |> FunctionSet.exists relevant_dynamic
 
-let disableAnalyses anas =
-  List.iter (GobConfig.set_auto "ana.activated[-]") anas
+let disableAnalyses reason analyses =
+  Logs.info "%s -> disabling analyses: \"%s\"" reason (String.concat ", " analyses);
+  List.iter (GobConfig.set_auto "ana.activated[-]") analyses
 
-let enableAnalyses anas =
-  List.iter (GobConfig.set_auto "ana.activated[+]") anas
+let enableAnalyses reason description analyses =
+  Logs.info "%s -> enabling %s: \"%s\"" reason description (String.concat ", " analyses);
+  List.iter (GobConfig.set_auto "ana.activated[+]") analyses
 
 (*If only one thread is used in the program, we can disable most thread analyses*)
 (*The exceptions are analyses that are depended on by others: base -> mutex -> mutexEvents, access; termination -> threadflag *)
 (*escape is also still enabled, because otherwise we get a warning*)
 (*does not consider dynamic calls!*)
+let notNeccessaryRaceAnalyses = ["race"; "symb_locks"; "region"]
+let notNeccessaryThreadAnalyses = notNeccessaryRaceAnalyses @ ["deadlock"; "maylocks"; "thread"; "threadid"; "threadJoins"; "threadreturn"; "mhp"; "pthreadMutexType"]
 
-let notNeccessaryThreadAnalyses = ["race"; "deadlock"; "maylocks"; "symb_locks"; "thread"; "threadid"; "threadJoins"; "threadreturn"; "mhp"; "region"; "pthreadMutexType"]
-let reduceThreadAnalyses () =
+let hasSpec spec = List.mem spec (Svcomp.Specification.of_option ())
+
+let reduceAnalyses () =
   let isThreadCreate (desc: LibraryDesc.t) args =
     match desc.special args with
     | LibraryDesc.ThreadCreate _ -> true
     | _ -> LibraryDesc.Accesses.find_kind desc.accs Spawn args <> []
   in
   let hasThreadCreate = hasFunction isThreadCreate in
-  if not @@ hasThreadCreate then (
-    Logs.info "no thread creation -> disabling thread analyses \"%s\"" (String.concat ", " notNeccessaryThreadAnalyses);
-    disableAnalyses notNeccessaryThreadAnalyses;
-  )
+  if not hasThreadCreate then disableAnalyses "no thread creation" notNeccessaryThreadAnalyses
 
 let focusOnMemSafetySpecification (spec: Svcomp.Specification.t) =
   match spec with
@@ -247,8 +249,7 @@ let focusOnTermination (spec: Svcomp.Specification.t) =
   match spec with
   | Termination ->
     let terminationAnas = ["threadflag"; "apron"] in
-    Logs.info "Specification: Termination -> enabling termination analyses \"%s\"" (String.concat ", " terminationAnas);
-    enableAnalyses terminationAnas;
+    enableAnalyses "Specification: Termination" "termination analyses" terminationAnas;
     set_string "sem.int.signed_overflow" "assume_none";
     set_bool "ana.int.interval" true;
     set_string "ana.apron.domain" "polyhedra"; (* TODO: Needed? *)
@@ -258,16 +259,16 @@ let focusOnTermination (spec: Svcomp.Specification.t) =
 let focusOnTermination () =
   List.iter focusOnTermination (Svcomp.Specification.of_option ())
 
-let concurrencySafety (spec: Svcomp.Specification.t) =
-  match spec with
-  | NoDataRace -> (*enable all thread analyses*)
-    Logs.info "Specification: NoDataRace -> enabling thread analyses \"%s\"" (String.concat ", " notNeccessaryThreadAnalyses);
-    enableAnalyses notNeccessaryThreadAnalyses;
-  | _ -> ()
+let focusOnConcurrencySafety () =
+  if hasSpec SvcompSpec.NoDataRace then
+    (*enable all thread analyses*)
+    (* TODO: what's the exact relation between thread analyses enabled in conf, the ones we disable in reduceAnalyses and the ones we enable here? *)
+    enableAnalyses "Specification: NoDataRace" "thread analyses" notNeccessaryThreadAnalyses
+  else
+    disableAnalyses "NoDataRace property is not in spec" notNeccessaryRaceAnalyses
 
-let noOverflows (spec: Svcomp.Specification.t) =
-  match spec with
-  | NoOverflow ->
+let focusOnNoOverflows () =
+  if hasSpec SvcompSpec.NoOverflow then (
     (*We focus on integer analysis*)
     set_bool "ana.int.def_exc" true;
     begin
@@ -276,10 +277,7 @@ let noOverflows (spec: Svcomp.Specification.t) =
         set_int "ana.malloc.unique_address_count" 1
       with Found -> set_int "ana.malloc.unique_address_count" 0;
     end
-  | _ -> ()
-
-let focusOn (f : SvcompSpec.t -> unit) =
-  List.iter f (Svcomp.Specification.of_option ())
+  )
 
 (*Detect enumerations and enable the "ana.int.enums" option*)
 exception EnumFound
@@ -492,8 +490,7 @@ let activateTmpSpecialAnalysis () =
   in
   let hasMathFunctions = hasFunction isMathFun in
   if hasMathFunctions then (
-    Logs.info "math function -> enabling tmpSpecial analysis and floating-point domain";
-    enableAnalyses ["tmpSpecial"];
+    enableAnalyses "Math function" "tmpSpecial analysis and floating-point domain" ["tmpSpecial"];
     set_bool "ana.float.interval" true;
   )
 
@@ -546,15 +543,17 @@ let chooseConfig file =
   if isActivated "mallocWrappers" then
     findMallocWrappers ();
 
-  if isActivated "concurrencySafetySpecification" then focusOn concurrencySafety;
+  if isActivated "concurrencySafetySpecification" then
+    focusOnConcurrencySafety ();
 
-  if isActivated "noOverflows" then focusOn noOverflows;
+  if isActivated "noOverflows" then
+    focusOnNoOverflows ();
 
   if isActivated "enums" && hasEnums file then
     set_bool "ana.int.enums" true;
 
-  if isActivated "singleThreaded" then
-    reduceThreadAnalyses ();
+  if isActivated "reduceAnalyses" then
+    reduceAnalyses ();
 
   if isActivated "arrayDomain" then
     selectArrayDomains file;
diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml
@@ -561,7 +561,13 @@ struct
     | (_, Top) -> true
     | (Top, _) -> false
     | (Bot, _) -> true
-    | (_, Bot) -> false
+    | (x, Bot) ->
+      if !AnalysisState.bot_in_blob_leq_bot then
+        match x with
+        | Blob (x,s,o) -> leq x Bot
+        | _ -> false
+      else
+        false
     | (Int x, Int y) -> ID.leq x y
     | (Float x, Float y) -> FD.leq x y
     | (Int x, Address y) when ID.to_int x = Some Z.zero && not (AD.is_not_null y) -> true
diff --git a/src/common/framework/analysisState.ml b/src/common/framework/analysisState.ml
@@ -40,4 +40,7 @@ let verified : bool option ref = ref None
 let unsound_both_branches_dead: bool option ref = ref None
 (** [Some true] if unsound both branches dead occurs in analysis results.
     [Some false] if it doesn't occur.
-    [None] if [ana.dead-code.branches] option is disabled and this isn't checked. *)
+    [None] if [ana.dead-code.branches] option is disabled and this isn't checked. *)
+
+(* Comparison mode where blobs with bot content that are not zero-initalized are considered equivalent to top-level bot *)
+let bot_in_blob_leq_bot = ref false
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
@@ -541,7 +541,7 @@
                 "type": "string",
                 "enum": [
                   "congruence",
-                  "singleThreaded",
+                  "reduceAnalyses",
                   "mallocWrappers",
                   "noRecursiveIntervals",
                   "enums",
@@ -559,7 +559,7 @@
               },
               "default": [
                 "congruence",
-                "singleThreaded",
+                "reduceAnalyses",
                 "mallocWrappers",
                 "noRecursiveIntervals",
                 "enums",
diff --git a/src/privPrecCompare.ml b/src/privPrecCompare.ml
@@ -4,4 +4,5 @@ open Goblint_lib
 module A = PrecCompare.MakeDump (PrivPrecCompareUtil)
 
 let () =
+  AnalysisState.bot_in_blob_leq_bot := true;
   A.main ()
diff --git a/src/util/autoSoundConfig.ml b/src/util/autoSoundConfig.ml
@@ -9,8 +9,7 @@ open GobConfig
 open AutoTune
 
 let enableSpecAnalyses spec analyses =
-  Logs.info "Specification: %s -> enabling soundness analyses \"%s\"" (Svcomp.Specification.to_string [spec]) (String.concat ", " analyses);
-  enableAnalyses analyses
+  enableAnalyses ("Specification: " ^ (Svcomp.Specification.to_string [spec])) "soundness analyses" analyses
 
 let enableOptions options =
   let enableOpt option =
@@ -65,7 +64,5 @@ let activateLongjmpAnalysesWhenRequired () =
     | LibraryDesc.Longjmp _ -> true
     | _ -> false
   in
-  if hasFunction isLongjmp  then (
-    Logs.info "longjmp -> enabling longjmp analyses \"%s\"" (String.concat ", " longjmpAnalyses);
-    enableAnalyses longjmpAnalyses;
-  )
+  if hasFunction isLongjmp then
+    enableAnalyses "Longjmp" "longjmp analyses" longjmpAnalyses;
diff --git a/tests/regression/13-privatized/63-access-threadspawn-lval.t b/tests/regression/13-privatized/63-access-threadspawn-lval.t
@@ -1,24 +1,24 @@
 Should have (safe) write accesses to id1 and id2:
 
-  $ goblint --enable allglobs 63-access-threadspawn-lval.c
-  [Error][Imprecise][Unsound] Function definition missing for magic2 (63-access-threadspawn-lval.c:21:3-21:12)
-  [Info][Imprecise] INVALIDATING ALL GLOBALS! (63-access-threadspawn-lval.c:21:3-21:12)
-  [Info][Imprecise] Invalidating expressions: & A, & id2, & id1, & e (63-access-threadspawn-lval.c:21:3-21:12)
-  [Error][Imprecise][Unsound] Function definition missing for magic1 (63-access-threadspawn-lval.c:13:3-13:11)
-  [Info][Imprecise] INVALIDATING ALL GLOBALS! (63-access-threadspawn-lval.c:13:3-13:11)
-  [Info][Imprecise] Invalidating expressions: & A, & id2, & id1 (63-access-threadspawn-lval.c:13:3-13:11)
-  [Info][Deadcode] Logical lines of code (LLoC) summary:
-    live: 13
-    dead: 0
-    total lines: 13
-  [Success][Race] Memory location id1 (safe): (63-access-threadspawn-lval.c:4:11-4:14)
-    write with [multi:false, thread:[main]] (conf. 110)  (exp: & *((pthread_t * __restrict  )(& id1))) (63-access-threadspawn-lval.c:27:3-27:37)
-  [Success][Race] Memory location id2 (safe): (63-access-threadspawn-lval.c:5:11-5:14)
-    write with [mhp:{created={[main, f@63-access-threadspawn-lval.c:27:3-27:37]}}, thread:[main]] (conf. 110)  (exp: (pthread_t * __restrict  )(& id2)) (63-access-threadspawn-lval.c:28:3-28:37)
-    write with [mhp:{created={[main, f@63-access-threadspawn-lval.c:27:3-27:37]}}, thread:[main]] (conf. 110)  (exp: & *((pthread_t * __restrict  )(& id2))) (63-access-threadspawn-lval.c:28:3-28:37)
+  $ goblint --enable warn.deterministic --enable allglobs 63-access-threadspawn-lval.c
   [Info][Race] Memory locations race summary:
     safe: 2
     vulnerable: 0
     unsafe: 0
     total memory locations: 2
+  [Success][Race] Memory location id1 (safe): (63-access-threadspawn-lval.c:4:11-4:14)
+    write with [multi:false, thread:[main]] (conf. 110)  (exp: & *((pthread_t * __restrict  )(& id1))) (63-access-threadspawn-lval.c:27:3-27:37)
+  [Success][Race] Memory location id2 (safe): (63-access-threadspawn-lval.c:5:11-5:14)
+    write with [mhp:{created={[main, f@63-access-threadspawn-lval.c:27:3-27:37]}}, thread:[main]] (conf. 110)  (exp: (pthread_t * __restrict  )(& id2)) (63-access-threadspawn-lval.c:28:3-28:37)
+    write with [mhp:{created={[main, f@63-access-threadspawn-lval.c:27:3-27:37]}}, thread:[main]] (conf. 110)  (exp: & *((pthread_t * __restrict  )(& id2))) (63-access-threadspawn-lval.c:28:3-28:37)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 13
+    dead: 0
+    total lines: 13
+  [Info][Imprecise] INVALIDATING ALL GLOBALS! (63-access-threadspawn-lval.c:13:3-13:11)
+  [Info][Imprecise] Invalidating expressions: & A, & id2, & id1 (63-access-threadspawn-lval.c:13:3-13:11)
+  [Info][Imprecise] INVALIDATING ALL GLOBALS! (63-access-threadspawn-lval.c:21:3-21:12)
+  [Info][Imprecise] Invalidating expressions: & A, & id2, & id1, & e (63-access-threadspawn-lval.c:21:3-21:12)
+  [Error][Imprecise][Unsound] Function definition missing for magic1 (63-access-threadspawn-lval.c:13:3-13:11)
+  [Error][Imprecise][Unsound] Function definition missing for magic2 (63-access-threadspawn-lval.c:21:3-21:12)
   [Error][Imprecise][Unsound] Function definition missing
diff --git a/tests/regression/36-apron/12-traces-min-rpb1.t b/tests/regression/36-apron/12-traces-min-rpb1.t
diff --git a/tests/regression/46-apron2/97-std-globals.c b/tests/regression/46-apron2/97-std-globals.c
diff --git a/tests/regression/74-invalid_deref/33-enum-in-index.c b/tests/regression/74-invalid_deref/33-enum-in-index.c
diff --git a/tests/regression/76-memleak/32-no-mem-leak-goblint-check.c b/tests/regression/76-memleak/32-no-mem-leak-goblint-check.c
diff --git a/tests/regression/76-memleak/32-no-mem-leak-goblint-check.t b/tests/regression/76-memleak/32-no-mem-leak-goblint-check.t
diff --git a/tests/regression/76-memleak/dune b/tests/regression/76-memleak/dune
