From 3613083bc90465e02271bd50e8104718f8ccfde6 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Tue, 22 Nov 2022 13:29:39 +0100 Subject: [PATCH 01/10] Add test case where both branches are erroneously considered dead. --- .../regression/29-svcomp/31-dd-address-meet.c | 21 +++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 tests/regression/29-svcomp/31-dd-address-meet.c diff --git a/tests/regression/29-svcomp/31-dd-address-meet.c b/tests/regression/29-svcomp/31-dd-address-meet.c new file mode 100644 index 0000000000..be7c71f67d --- /dev/null +++ b/tests/regression/29-svcomp/31-dd-address-meet.c @@ -0,0 +1,21 @@ +// PARAM: --enable annotation.int.enabled +#include +struct slotvec { + size_t size ; + char *val ; +}; +static char slot0[256] ; +static struct slotvec slotvec0 = {sizeof(slot0), slot0}; + +static void install_signal_handlers(void) +{ + { if(!(slotvec0.val == & slot0[0LL])) { reach_error(); abort(); } }; +} + +int main(int argc , char **argv ) +{ + // Goblint used to consider both branches in this condition to be dead, because the meet on addresses with different active int domains was broken + { if(!(slotvec0.val == & slot0[0LL])) { reach_error(); abort(); } }; + install_signal_handlers(); + return 0; +} From 88e1d2b3cb969fd0e08d4905b5c0d8f06335826b Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Tue, 22 Nov 2022 14:13:06 +0100 Subject: [PATCH 02/10] Add __goblint_check to test to check reachability. --- tests/regression/29-svcomp/31-dd-address-meet.c | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/tests/regression/29-svcomp/31-dd-address-meet.c b/tests/regression/29-svcomp/31-dd-address-meet.c index be7c71f67d..05f45398e9 100644 --- a/tests/regression/29-svcomp/31-dd-address-meet.c +++ b/tests/regression/29-svcomp/31-dd-address-meet.c @@ -1,5 +1,6 @@ // PARAM: --enable annotation.int.enabled #include +#include struct slotvec { size_t size ; char *val ; @@ -9,7 +10,7 @@ static struct slotvec slotvec0 = {sizeof(slot0), slot0}; static void install_signal_handlers(void) { - { if(!(slotvec0.val == & slot0[0LL])) { reach_error(); abort(); } }; + { if(!(slotvec0.val == & slot0[0LL])) { reach_error(); abort(); } }; } int main(int argc , char **argv ) @@ -17,5 +18,8 @@ int main(int argc , char **argv ) // Goblint used to consider both branches in this condition to be dead, because the meet on addresses with different active int domains was broken { if(!(slotvec0.val == & slot0[0LL])) { reach_error(); abort(); } }; install_signal_handlers(); + + // Should be reachable + __goblint_check(1); return 0; } From d35bc54f50531b0f4c98951df55bbcf04b7be04c Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Tue, 22 Nov 2022 14:16:59 +0100 Subject: [PATCH 03/10] Addressets: Remove index-offset information from representative. The representative should not keep any information about the values of the index offset. Previously, the top() offset led to offsets being kept apart (i.e. the corresponding addresses in different buckets) in the case that different integer domains were active in the index offset. Co-authored-by: Michael Schwarz Co-authored-by: Sarah Tilscher <66023521+stilscher@users.noreply.github.com> --- src/cdomains/lval.ml | 77 ++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 70 insertions(+), 7 deletions(-) diff --git a/src/cdomains/lval.ml b/src/cdomains/lval.ml index b2f4006fdf..887c6b8c43 100644 --- a/src/cdomains/lval.ml +++ b/src/cdomains/lval.ml @@ -385,22 +385,85 @@ end module NormalLatRepr (Idx: IntDomain.Z) = struct include NormalLat (Idx) + module Offset = struct + type t = NoOffset | Field of CilType.Fieldinfo.t * t | Index of unit * t [@@deriving eq, ord, hash] + + let is_first_field x = match x.fcomp.cfields with + | [] -> false + | f :: _ -> CilType.Fieldinfo.equal f x + + let rec cmp_zero_offset : t -> [`MustZero | `MustNonzero | `MayZero] = function + | NoOffset -> `MustZero + | Index (_, o) -> (match cmp_zero_offset o with + | `MustNonzero -> `MustNonzero + | _ -> `MayZero) + | Field (x, o) -> + if is_first_field x then cmp_zero_offset o else `MustNonzero + + let rec equal x y = + match x, y with + | NoOffset , NoOffset -> true + | NoOffset, x + | x, NoOffset -> cmp_zero_offset x = `MustZero (* cannot derive due to this special case, special cases not used for AddressDomain any more due to splitting *) + | Field (f1,o1), Field (f2,o2) when CilType.Fieldinfo.equal f1 f2 -> equal o1 o2 + | Index (_,o1), Index (_,o2) -> equal o1 o2 + | _ -> false + + let rec hash = function (* special cases not used for AddressDomain any more due to splitting *) + | NoOffset -> 1 + | Field (f,o) when not (is_first_field f) -> Hashtbl.hash f.fname * hash o + 13 + | Field (_,o) (* zero offsets need to yield the same hash as `NoOffset! *) + | Index (_,o) -> hash o (* index might become top during fp -> might be zero offset *) + + let rec compare o1 o2 = match o1, o2 with + | NoOffset, NoOffset -> 0 + | NoOffset, x + | x, NoOffset when cmp_zero_offset x = `MustZero -> 0 (* cannot derive due to this special case, special cases not used for AddressDomain any more due to splitting *) + | Field (f1,o1), Field (f2,o2) -> + let c = CilType.Fieldinfo.compare f1 f2 in + if c=0 then compare o1 o2 else c + | Index (_,o1), Index (_,o2) -> + compare o1 o2 + | NoOffset, _ -> -1 + | _, NoOffset -> 1 + | Field _, Index _ -> -1 + | Index _, Field _ -> 1 + end + type elttype = + | MyAddr of CilType.Varinfo.t * Offset.t (** Pointer to offset of a variable. *) + | MyNullPtr (** NULL pointer. *) + | MyUnknownPtr (** Unknown pointer. Could point to globals, heap and escaped variables. *) + | MyStrPtr of string option [@@deriving eq, ord, hash] (** Representatives for lvalue sublattices as defined by {!NormalLat}. *) module R: DisjointDomain.Representative with type elt = t = struct include Normal (Idx) type elt = t + type t = elttype [@@deriving eq, ord, hash] + + let show x = "" + + let pretty _= failwith "" + + let printXml _ = failwith "" - let rec of_elt_offset: Offs.t -> Offs.t = + let to_yojson _ = failwith "" + + let arbitrary _ = failwith "" + + let rec of_elt_offset: Offs.t -> Offset.t = function - | `NoOffset -> `NoOffset - | `Field (f,o) -> `Field (f, of_elt_offset o) - | `Index (_,o) -> `Index (Idx.top (), of_elt_offset o) (* all indices to same bucket *) + | `NoOffset -> NoOffset + | `Field (f,o) -> Field (f, of_elt_offset o) + | `Index (_,o) -> Index ((), of_elt_offset o) (* all indices to same bucket *) let of_elt = function - | Addr (v, o) -> Addr (v, of_elt_offset o) (* addrs grouped by var and part of offset *) - | StrPtr _ when GobConfig.get_bool "ana.base.limit-string-addresses" -> StrPtr None (* all strings together if limited *) - | a -> a (* everything else is kept separate, including strings if not limited *) + | Addr (v, o) -> MyAddr (v, of_elt_offset o) (* addrs grouped by var and part of offset *) + | StrPtr _ when GobConfig.get_bool "ana.base.limit-string-addresses" -> MyStrPtr None (* all strings together if limited *) + | UnknownPtr -> MyUnknownPtr + | StrPtr a -> MyStrPtr a + | NullPtr -> MyNullPtr + end end From 21bd2cd65d8ea0964884f86c75a132fb71d9edb4 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Tue, 22 Nov 2022 14:34:08 +0100 Subject: [PATCH 04/10] Rename type to r --- src/cdomains/lval.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/cdomains/lval.ml b/src/cdomains/lval.ml index 887c6b8c43..3e9f969a1d 100644 --- a/src/cdomains/lval.ml +++ b/src/cdomains/lval.ml @@ -429,7 +429,7 @@ struct | Field _, Index _ -> -1 | Index _, Field _ -> 1 end - type elttype = + type r = | MyAddr of CilType.Varinfo.t * Offset.t (** Pointer to offset of a variable. *) | MyNullPtr (** NULL pointer. *) | MyUnknownPtr (** Unknown pointer. Could point to globals, heap and escaped variables. *) @@ -440,9 +440,9 @@ struct struct include Normal (Idx) type elt = t - type t = elttype [@@deriving eq, ord, hash] + type t = r [@@deriving eq, ord, hash] - let show x = "" + let show x = failwith "" let pretty _= failwith "" From d5bdc968ccb86023c16ae289dda061f1884fbf1a Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Tue, 22 Nov 2022 14:49:57 +0100 Subject: [PATCH 05/10] Lval.R: Implement show and related print functions. --- src/cdomains/lval.ml | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) diff --git a/src/cdomains/lval.ml b/src/cdomains/lval.ml index 3e9f969a1d..b25db076b1 100644 --- a/src/cdomains/lval.ml +++ b/src/cdomains/lval.ml @@ -388,6 +388,11 @@ struct module Offset = struct type t = NoOffset | Field of CilType.Fieldinfo.t * t | Index of unit * t [@@deriving eq, ord, hash] + let rec show = function + | NoOffset -> "" + | Field (f, o) -> "." ^ f.fname ^ show o + | Index ((), o) -> "[?]" ^ show o ^ ")" + let is_first_field x = match x.fcomp.cfields with | [] -> false | f :: _ -> CilType.Fieldinfo.equal f x @@ -442,15 +447,14 @@ struct type elt = t type t = r [@@deriving eq, ord, hash] - let show x = failwith "" - - let pretty _= failwith "" - - let printXml _ = failwith "" - - let to_yojson _ = failwith "" + let show = function + | MyAddr (v, o) -> v.vname ^ (Offset.show o) + | MyNullPtr -> "NULL" + | MyUnknownPtr -> "?" + | MyStrPtr (Some s) -> s + | MyStrPtr None -> "(unknown string)" - let arbitrary _ = failwith "" + include Printable.SimpleShow (struct type nonrec t = t let show = show end) let rec of_elt_offset: Offs.t -> Offset.t = function @@ -464,6 +468,7 @@ struct | StrPtr a -> MyStrPtr a | NullPtr -> MyNullPtr + let arbitrary _ = failwith "arbitrary not implemented for Lval.R" end end From a0f48e6f5e11e7982ddee2f001b73efb189b3127 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Tue, 22 Nov 2022 14:53:12 +0100 Subject: [PATCH 06/10] Imporve Lval.R.show output for strings. --- src/cdomains/lval.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cdomains/lval.ml b/src/cdomains/lval.ml index b25db076b1..c68f939e89 100644 --- a/src/cdomains/lval.ml +++ b/src/cdomains/lval.ml @@ -451,7 +451,7 @@ struct | MyAddr (v, o) -> v.vname ^ (Offset.show o) | MyNullPtr -> "NULL" | MyUnknownPtr -> "?" - | MyStrPtr (Some s) -> s + | MyStrPtr (Some s) -> "\"" ^ s ^ "\"" | MyStrPtr None -> "(unknown string)" include Printable.SimpleShow (struct type nonrec t = t let show = show end) From 18ebb359ef98aa6a840d0c5f0516ee3174474034 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Tue, 22 Nov 2022 15:06:33 +0100 Subject: [PATCH 07/10] Add comment explaining why separate type for offsets without abstract value for index offsets is introduced. --- src/cdomains/lval.ml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/cdomains/lval.ml b/src/cdomains/lval.ml index c68f939e89..8cee69bbab 100644 --- a/src/cdomains/lval.ml +++ b/src/cdomains/lval.ml @@ -386,6 +386,10 @@ module NormalLatRepr (Idx: IntDomain.Z) = struct include NormalLat (Idx) module Offset = struct + + (* Offset type for representative without abstract values for index offsets. + Reason: The offset in the representative (used for buckets) should not depend on the integer domains, + since different integer domains may be active at different program points. *) type t = NoOffset | Field of CilType.Fieldinfo.t * t | Index of unit * t [@@deriving eq, ord, hash] let rec show = function From 0c0249516eea8631d53f96ee6742dee287e4d048 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Tue, 22 Nov 2022 15:17:02 +0100 Subject: [PATCH 08/10] Rename NormalLatRepr variants and inner Offset module Rename the variants in NormalLatRepr, and the NormalLatRepr.Offset module. --- src/cdomains/lval.ml | 32 ++++++++++++++++---------------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/src/cdomains/lval.ml b/src/cdomains/lval.ml index 8cee69bbab..87572d99e3 100644 --- a/src/cdomains/lval.ml +++ b/src/cdomains/lval.ml @@ -385,7 +385,7 @@ end module NormalLatRepr (Idx: IntDomain.Z) = struct include NormalLat (Idx) - module Offset = struct + module ReprOffset = struct (* Offset type for representative without abstract values for index offsets. Reason: The offset in the representative (used for buckets) should not depend on the integer domains, @@ -439,10 +439,10 @@ struct | Index _, Field _ -> 1 end type r = - | MyAddr of CilType.Varinfo.t * Offset.t (** Pointer to offset of a variable. *) - | MyNullPtr (** NULL pointer. *) - | MyUnknownPtr (** Unknown pointer. Could point to globals, heap and escaped variables. *) - | MyStrPtr of string option [@@deriving eq, ord, hash] + | ReprAddr of CilType.Varinfo.t * ReprOffset.t (** Pointer to offset of a variable. *) + | ReprNullPtr (** NULL pointer. *) + | ReprUnknownPtr (** Unknown pointer. Could point to globals, heap and escaped variables. *) + | ReprMyStrPtr of string option [@@deriving eq, ord, hash] (** Representatives for lvalue sublattices as defined by {!NormalLat}. *) module R: DisjointDomain.Representative with type elt = t = @@ -452,25 +452,25 @@ struct type t = r [@@deriving eq, ord, hash] let show = function - | MyAddr (v, o) -> v.vname ^ (Offset.show o) - | MyNullPtr -> "NULL" - | MyUnknownPtr -> "?" - | MyStrPtr (Some s) -> "\"" ^ s ^ "\"" - | MyStrPtr None -> "(unknown string)" + | ReprAddr (v, o) -> v.vname ^ (ReprOffset.show o) + | ReprNullPtr -> "NULL" + | ReprUnknownPtr -> "?" + | ReprMyStrPtr (Some s) -> "\"" ^ s ^ "\"" + | ReprMyStrPtr None -> "(unknown string)" include Printable.SimpleShow (struct type nonrec t = t let show = show end) - let rec of_elt_offset: Offs.t -> Offset.t = + let rec of_elt_offset: Offs.t -> ReprOffset.t = function | `NoOffset -> NoOffset | `Field (f,o) -> Field (f, of_elt_offset o) | `Index (_,o) -> Index ((), of_elt_offset o) (* all indices to same bucket *) let of_elt = function - | Addr (v, o) -> MyAddr (v, of_elt_offset o) (* addrs grouped by var and part of offset *) - | StrPtr _ when GobConfig.get_bool "ana.base.limit-string-addresses" -> MyStrPtr None (* all strings together if limited *) - | UnknownPtr -> MyUnknownPtr - | StrPtr a -> MyStrPtr a - | NullPtr -> MyNullPtr + | Addr (v, o) -> ReprAddr (v, of_elt_offset o) (* addrs grouped by var and part of offset *) + | StrPtr _ when GobConfig.get_bool "ana.base.limit-string-addresses" -> ReprMyStrPtr None (* all strings together if limited *) + | UnknownPtr -> ReprUnknownPtr + | StrPtr a -> ReprMyStrPtr a + | NullPtr -> ReprNullPtr let arbitrary _ = failwith "arbitrary not implemented for Lval.R" end From a754b7d6ee0ff64e27b213605c2eaee1855e1617 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Tue, 22 Nov 2022 15:22:35 +0100 Subject: [PATCH 09/10] Rename ReprMyStrPtr to ReprStrPtr. --- src/cdomains/lval.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/cdomains/lval.ml b/src/cdomains/lval.ml index 87572d99e3..1cf9a02ce9 100644 --- a/src/cdomains/lval.ml +++ b/src/cdomains/lval.ml @@ -442,7 +442,7 @@ struct | ReprAddr of CilType.Varinfo.t * ReprOffset.t (** Pointer to offset of a variable. *) | ReprNullPtr (** NULL pointer. *) | ReprUnknownPtr (** Unknown pointer. Could point to globals, heap and escaped variables. *) - | ReprMyStrPtr of string option [@@deriving eq, ord, hash] + | ReprStrPtr of string option [@@deriving eq, ord, hash] (** Representatives for lvalue sublattices as defined by {!NormalLat}. *) module R: DisjointDomain.Representative with type elt = t = @@ -455,8 +455,8 @@ struct | ReprAddr (v, o) -> v.vname ^ (ReprOffset.show o) | ReprNullPtr -> "NULL" | ReprUnknownPtr -> "?" - | ReprMyStrPtr (Some s) -> "\"" ^ s ^ "\"" - | ReprMyStrPtr None -> "(unknown string)" + | ReprStrPtr (Some s) -> "\"" ^ s ^ "\"" + | ReprStrPtr None -> "(unknown string)" include Printable.SimpleShow (struct type nonrec t = t let show = show end) @@ -467,9 +467,9 @@ struct | `Index (_,o) -> Index ((), of_elt_offset o) (* all indices to same bucket *) let of_elt = function | Addr (v, o) -> ReprAddr (v, of_elt_offset o) (* addrs grouped by var and part of offset *) - | StrPtr _ when GobConfig.get_bool "ana.base.limit-string-addresses" -> ReprMyStrPtr None (* all strings together if limited *) + | StrPtr _ when GobConfig.get_bool "ana.base.limit-string-addresses" -> ReprStrPtr None (* all strings together if limited *) | UnknownPtr -> ReprUnknownPtr - | StrPtr a -> ReprMyStrPtr a + | StrPtr a -> ReprStrPtr a | NullPtr -> ReprNullPtr let arbitrary _ = failwith "arbitrary not implemented for Lval.R" From 3dd39e7abbe813ad63fe0137e6a1e17fcaa506c1 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Tue, 22 Nov 2022 15:49:30 +0100 Subject: [PATCH 10/10] Add comment explaining impact of option in test case Co-authored-by: Michael Schwarz --- tests/regression/29-svcomp/31-dd-address-meet.c | 1 + 1 file changed, 1 insertion(+) diff --git a/tests/regression/29-svcomp/31-dd-address-meet.c b/tests/regression/29-svcomp/31-dd-address-meet.c index 05f45398e9..10e686bcc9 100644 --- a/tests/regression/29-svcomp/31-dd-address-meet.c +++ b/tests/regression/29-svcomp/31-dd-address-meet.c @@ -1,4 +1,5 @@ // PARAM: --enable annotation.int.enabled +// This option enables ALL int domains for globals #include #include struct slotvec {