From 829d32be441b3a677f735e582b9145b168081732 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 17 Dec 2024 15:56:40 +0100 Subject: [PATCH 1/2] PrivPrecCompare: Add `bot_in_blob_leq_bot` so `bot` and `Blob(bot)` compare equal --- src/cdomain/value/cdomains/valueDomain.ml | 8 +++++++- src/common/framework/analysisState.ml | 4 +++- src/privPrecCompare.ml | 1 + 3 files changed, 11 insertions(+), 2 deletions(-) diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml index b126d712bf..af101b933b 100644 --- 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 index 96816b8529..e9cbafa8a4 100644 --- a/src/common/framework/analysisState.ml +++ b/src/common/framework/analysisState.ml @@ -40,4 +40,6 @@ 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. *) \ No newline at end of file + [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/privPrecCompare.ml b/src/privPrecCompare.ml index b4588e25bd..3b2e385383 100644 --- 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 () From 254a21fd879ee61207c74f84e7d856509de3f084 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 17 Dec 2024 15:57:52 +0100 Subject: [PATCH 2/2] Add new line --- src/common/framework/analysisState.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/common/framework/analysisState.ml b/src/common/framework/analysisState.ml index e9cbafa8a4..4dd4744967 100644 --- a/src/common/framework/analysisState.ml +++ b/src/common/framework/analysisState.ml @@ -41,5 +41,6 @@ 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. *) + (* 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