From 903fc3ad3e70fa1f681deeebebc04188ba7fed0d Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 4 Apr 2024 11:01:20 +0200 Subject: [PATCH 1/3] NullBytes: Do not print if deactivated --- src/cdomain/value/cdomains/arrayDomain.ml | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/cdomain/value/cdomains/arrayDomain.ml b/src/cdomain/value/cdomains/arrayDomain.ml index 8958ee2303..44d144686a 100644 --- a/src/cdomain/value/cdomains/arrayDomain.ml +++ b/src/cdomain/value/cdomains/arrayDomain.ml @@ -1815,6 +1815,17 @@ struct else f_get + let delegate_if_no_nullbytes (a, n) ffull fa = + if get_bool "ana.base.arrays.nullbytes" then + ffull (a,n) + else + fa a + + let show x = delegate_if_no_nullbytes x show A.show + let printXml f x = delegate_if_no_nullbytes x (printXml f) (A.printXml f) + let to_yojson x = delegate_if_no_nullbytes x to_yojson A.to_yojson + let pretty () x = delegate_if_no_nullbytes x (pretty ()) (A.pretty ()) + let construct a n = if get_bool "ana.base.arrays.nullbytes" then (a, n ()) From 4ed91029b051879a4fba613c934bb0426cd300ca Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 4 Apr 2024 11:02:01 +0200 Subject: [PATCH 2/3] Space --- src/cdomain/value/cdomains/arrayDomain.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cdomain/value/cdomains/arrayDomain.ml b/src/cdomain/value/cdomains/arrayDomain.ml index 44d144686a..9a0cc58f1b 100644 --- a/src/cdomain/value/cdomains/arrayDomain.ml +++ b/src/cdomain/value/cdomains/arrayDomain.ml @@ -1817,7 +1817,7 @@ struct let delegate_if_no_nullbytes (a, n) ffull fa = if get_bool "ana.base.arrays.nullbytes" then - ffull (a,n) + ffull (a, n) else fa a From 82e11db8fad1347f06a0f666791b391fb4ce5fbf Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 4 Apr 2024 11:09:59 +0200 Subject: [PATCH 3/3] NullByte: Give useful names to components --- src/cdomain/value/cdomains/arrayDomain.ml | 4 ++-- src/cdomain/value/cdomains/nullByteSet.ml | 4 ++++ 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/src/cdomain/value/cdomains/arrayDomain.ml b/src/cdomain/value/cdomains/arrayDomain.ml index 9a0cc58f1b..e1cfb96425 100644 --- a/src/cdomain/value/cdomains/arrayDomain.ml +++ b/src/cdomain/value/cdomains/arrayDomain.ml @@ -1012,9 +1012,9 @@ struct let (+.) = Z.add (* (Must Null Set, May Null Set, Array Size) *) - include Lattice.Prod (Nulls) (Idx) + include Lattice.Prod (Nulls) (struct include Idx let name () = "length" end) - let name () = "arrays containing null bytes" + let name () = "ArrayNullBytes" type idx = Idx.t type value = Val.t diff --git a/src/cdomain/value/cdomains/nullByteSet.ml b/src/cdomain/value/cdomains/nullByteSet.ml index ae382b6118..87dcac7f2d 100644 --- a/src/cdomain/value/cdomains/nullByteSet.ml +++ b/src/cdomain/value/cdomains/nullByteSet.ml @@ -4,6 +4,8 @@ module MustSet = struct module M = SetDomain.Reverse (SetDomain.ToppedSet (IntOps.BigIntOps) (struct let topname = "All Null" end)) include M + let name () = "MustNullBytes" + let compute_set len = List.init (Z.to_int len) Z.of_int |> of_list @@ -48,6 +50,8 @@ module MaySet = struct module M = SetDomain.ToppedSet (IntOps.BigIntOps) (struct let topname = "All Null" end) include M + let name () = "MayNullBytes" + let elements ?max_size may_nulls_set = if M.is_top may_nulls_set then match max_size with