Merge pull request #1645 from goblint/bot_in_blob_leq_bot

PrivPrecCompare: Add `bot_in_blob_leq_bot` so `bot` and `Blob(bot)` are considered equal

Author: michael-schwarz

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

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

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 ()