From 7186571f6da0bcd2f954b5676d9f83509de0bfb2 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 15 May 2024 15:49:59 +0200 Subject: [PATCH 1/8] Typo --- src/analyses/base.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 4385f1fca8..9f0dae4d9c 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1579,7 +1579,7 @@ struct let set ~(ctx: _ ctx) ?(invariant=false) ?(blob_destructive=false) ?lval_raw ?rval_raw ?t_override (st: store) (lval: AD.t) (lval_type: Cil.typ) (value: value) : store = let update_variable x t y z = if M.tracing then M.tracel "set" ~var:x.vname "update_variable: start '%s' '%a'\nto\n%a" x.vname VD.pretty y CPA.pretty z; - let r = update_variable x t y z in (* refers to defintion that is outside of set *) + let r = update_variable x t y z in (* refers to definition that is outside of set *) if M.tracing then M.tracel "set" ~var:x.vname "update_variable: start '%s' '%a'\nto\n%a\nresults in\n%a" x.vname VD.pretty y CPA.pretty z CPA.pretty r; r in From c1b7284c0718cb110aad37a043dcd0eb18f9aa04 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 15 May 2024 15:53:12 +0200 Subject: [PATCH 2/8] Add `amenable_to_meet` and test for it --- src/cdomain/value/cdomains/addressDomain.ml | 5 ++++ .../value/cdomains/addressDomain_intf.ml | 5 +++- src/domain/disjointDomain.ml | 14 +++++++-- .../89-write-lacking-precision.c | 30 +++++++++++++++++++ 4 files changed, 51 insertions(+), 3 deletions(-) create mode 100644 tests/regression/13-privatized/89-write-lacking-precision.c diff --git a/src/cdomain/value/cdomains/addressDomain.ml b/src/cdomain/value/cdomains/addressDomain.ml index dc1ebfff7d..52e48e5612 100644 --- a/src/cdomain/value/cdomains/addressDomain.ml +++ b/src/cdomain/value/cdomains/addressDomain.ml @@ -110,6 +110,10 @@ struct | StrPtr _, UnknownPtr -> None | _, _ -> Some false + let amenable_to_meet x y = match x,y with + | StrPtr _, StrPtr _ -> true + | _ -> false + let leq x y = match x, y with | StrPtr s1, StrPtr s2 -> SD.leq s1 s2 | Addr x, Addr y -> Mval.leq x y @@ -178,6 +182,7 @@ struct struct include SetDomain.Joined (Addr) let may_be_equal a b = Option.value (Addr.semantic_equal a b) ~default:true + let amenable_to_meet = Addr.amenable_to_meet end module OffsetSplit = DisjointDomain.ProjectiveSetPairwiseMeet (Addr) (J) (Addr.UnitOffsetRepr) diff --git a/src/cdomain/value/cdomains/addressDomain_intf.ml b/src/cdomain/value/cdomains/addressDomain_intf.ml index f65b2977c4..78c65dd98a 100644 --- a/src/cdomain/value/cdomains/addressDomain_intf.ml +++ b/src/cdomain/value/cdomains/addressDomain_intf.ml @@ -80,8 +80,11 @@ sig val semantic_equal: t -> t -> bool option (** Check semantic equality of two addresses. - @return [Some true] if definitely equal, [Some false] if definitely not equal, [None] if unknown. *) + + val amenable_to_meet: t -> t -> bool + (** Whether two addresses are amenable to meet operation, i.e., their lattice meet overapproximates the intersection + of concretizations. If true, meet is used instead of semantic_equal *) end (** Address lattice with sublattice representatives for {!DisjointDomain}. *) diff --git a/src/domain/disjointDomain.ml b/src/domain/disjointDomain.ml index d8e59c4ba7..00f875bb3a 100644 --- a/src/domain/disjointDomain.ml +++ b/src/domain/disjointDomain.ml @@ -182,16 +182,26 @@ module type MayEqualSetDomain = sig include SetDomain.S val may_be_equal: elt -> elt -> bool + val amenable_to_meet: elt -> elt -> bool end -module ProjectiveSetPairwiseMeet (E: Printable.S) (B: MayEqualSetDomain with type elt = E.t) (R: Representative with type elt = E.t): SetDomain.S with type elt = E.t = struct +module ProjectiveSetPairwiseMeet (E: Lattice.S) (B: MayEqualSetDomain with type elt = E.t) (R: Representative with type elt = E.t): SetDomain.S with type elt = E.t = struct include ProjectiveSet (E) (B) (R) let meet m1 m2 = let meet_buckets b1 b2 acc = B.fold (fun e1 acc -> B.fold (fun e2 acc -> - if B.may_be_equal e1 e2 then + if B.amenable_to_meet e1 e2 then + try + let m = E.meet e1 e2 in + if not (E.is_bot m) then + add m acc + else + acc + with Lattice.Uncomparable -> + failwith (GobPretty.sprintf "amenable_to_meet %a %a returned true, but meet throws!" E.pretty e1 E.pretty e2) + else if B.may_be_equal e1 e2 then add e1 (add e2 acc) else acc diff --git a/tests/regression/13-privatized/89-write-lacking-precision.c b/tests/regression/13-privatized/89-write-lacking-precision.c new file mode 100644 index 0000000000..75ee78974d --- /dev/null +++ b/tests/regression/13-privatized/89-write-lacking-precision.c @@ -0,0 +1,30 @@ +// PARAM: --set ana.base.privatization write +#include +struct a { + char* b; +}; + +struct a *c; +struct a h = {""}; +struct a i = {"string"}; + +void* d(void* args) { + struct a r; + if (c->b) { + __goblint_check(strlen(h.b) == 0); // Should also work for write! + } +} + +int main() { + int top; + + if(top) { + c = &h; + } else { + c = &i; + } + + pthread_t t; + pthread_create(&t, 0, d, 0); + return 0; +} From 3eff22f8eb8b6858e5c9753548a02c7f69554381 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 15 May 2024 16:08:53 +0200 Subject: [PATCH 3/8] Make comparison of pointers amenable to `meet` if they only differ in offsets --- src/cdomain/value/cdomains/addressDomain.ml | 1 + .../27-inv_invariants/22-meet-ptrs.c | 24 +++++++++++++++++++ 2 files changed, 25 insertions(+) create mode 100644 tests/regression/27-inv_invariants/22-meet-ptrs.c diff --git a/src/cdomain/value/cdomains/addressDomain.ml b/src/cdomain/value/cdomains/addressDomain.ml index 52e48e5612..1a09aed026 100644 --- a/src/cdomain/value/cdomains/addressDomain.ml +++ b/src/cdomain/value/cdomains/addressDomain.ml @@ -112,6 +112,7 @@ struct let amenable_to_meet x y = match x,y with | StrPtr _, StrPtr _ -> true + | Addr x, Addr y when Mval.equal (Mval.top_indices x) (Mval.top_indices y) -> true | _ -> false let leq x y = match x, y with diff --git a/tests/regression/27-inv_invariants/22-meet-ptrs.c b/tests/regression/27-inv_invariants/22-meet-ptrs.c new file mode 100644 index 0000000000..33adfa879f --- /dev/null +++ b/tests/regression/27-inv_invariants/22-meet-ptrs.c @@ -0,0 +1,24 @@ +//PARAM: --enable ana.int.interval +#include +#include +#include + + +int main() { + int arr[20]; + + int top; + + int i = 2; + if(top) { + i = 8; + } + + int* imprecise = &arr[i]; + + if(imprecise == &arr[2]) { + __goblint_check(imprecise == &arr[2]); + } + + return 0; +} From dc2a9c3f14a9dcbbac57f6708dee493962bc030e Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 20 May 2024 15:06:27 +0200 Subject: [PATCH 4/8] Restore linebreak for odoc --- src/cdomain/value/cdomains/addressDomain_intf.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/cdomain/value/cdomains/addressDomain_intf.ml b/src/cdomain/value/cdomains/addressDomain_intf.ml index 78c65dd98a..b5eb5299f3 100644 --- a/src/cdomain/value/cdomains/addressDomain_intf.ml +++ b/src/cdomain/value/cdomains/addressDomain_intf.ml @@ -80,6 +80,7 @@ sig val semantic_equal: t -> t -> bool option (** Check semantic equality of two addresses. + @return [Some true] if definitely equal, [Some false] if definitely not equal, [None] if unknown. *) val amenable_to_meet: t -> t -> bool From b7265e7d3daa87aa1c62e428f5eeeb6b56b35e28 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 20 May 2024 15:18:03 +0200 Subject: [PATCH 5/8] Add more intricate example (with TODO for refinement of both sides) --- .../27-inv_invariants/22-meet-ptrs.c | 27 +++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/tests/regression/27-inv_invariants/22-meet-ptrs.c b/tests/regression/27-inv_invariants/22-meet-ptrs.c index 33adfa879f..ae089c2c3b 100644 --- a/tests/regression/27-inv_invariants/22-meet-ptrs.c +++ b/tests/regression/27-inv_invariants/22-meet-ptrs.c @@ -3,6 +3,32 @@ #include #include +int more_intricate() { + int arr[20]; + + int top; + + int i = 2; + int j = 8; + if(top) { + i = 8; + j = 9; + } + + int* imprecise1 = &arr[i]; // &arr[2..8] + int* imprecise2 = &arr[j]; // &arr[8..9] + + if(imprecise1 == imprecise2) { + __goblint_check(imprecise1 == &arr[8]); + __goblint_check(imprecise2 == &arr[8]); //TODO (Refinement should happen in both directions!) + } + + if(imprecise1 == &arr[j]) { + __goblint_check(imprecise1 == &arr[8]); + } + +} + int main() { int arr[20]; @@ -20,5 +46,6 @@ int main() { __goblint_check(imprecise == &arr[2]); } + more_intricate(); return 0; } From 8af2e49087633176ffeb23170ad63bae387e538b Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 16 Dec 2024 17:18:27 +0100 Subject: [PATCH 6/8] For elements in the same bucket, perform meet --- src/cdomain/value/cdomains/addressDomain.ml | 6 ------ src/cdomain/value/cdomains/addressDomain_intf.ml | 4 ---- src/domain/disjointDomain.ml | 6 +++--- 3 files changed, 3 insertions(+), 13 deletions(-) diff --git a/src/cdomain/value/cdomains/addressDomain.ml b/src/cdomain/value/cdomains/addressDomain.ml index 8f5bb4db4d..da684cc4f4 100644 --- a/src/cdomain/value/cdomains/addressDomain.ml +++ b/src/cdomain/value/cdomains/addressDomain.ml @@ -110,11 +110,6 @@ struct | StrPtr _, UnknownPtr -> None | _, _ -> Some false - let amenable_to_meet x y = match x,y with - | StrPtr _, StrPtr _ -> true - | Addr x, Addr y when Mval.equal (Mval.top_indices x) (Mval.top_indices y) -> true - | _ -> false - let leq x y = match x, y with | StrPtr s1, StrPtr s2 -> SD.leq s1 s2 | Addr x, Addr y -> Mval.leq x y @@ -183,7 +178,6 @@ struct struct include SetDomain.Joined (Addr) let may_be_equal a b = Option.value (Addr.semantic_equal a b) ~default:true - let amenable_to_meet = Addr.amenable_to_meet end module OffsetSplit = DisjointDomain.ProjectiveSetPairwiseMeet (Addr) (J) (Addr.UnitOffsetRepr) diff --git a/src/cdomain/value/cdomains/addressDomain_intf.ml b/src/cdomain/value/cdomains/addressDomain_intf.ml index b5eb5299f3..f65b2977c4 100644 --- a/src/cdomain/value/cdomains/addressDomain_intf.ml +++ b/src/cdomain/value/cdomains/addressDomain_intf.ml @@ -82,10 +82,6 @@ sig (** Check semantic equality of two addresses. @return [Some true] if definitely equal, [Some false] if definitely not equal, [None] if unknown. *) - - val amenable_to_meet: t -> t -> bool - (** Whether two addresses are amenable to meet operation, i.e., their lattice meet overapproximates the intersection - of concretizations. If true, meet is used instead of semantic_equal *) end (** Address lattice with sublattice representatives for {!DisjointDomain}. *) diff --git a/src/domain/disjointDomain.ml b/src/domain/disjointDomain.ml index 00f875bb3a..f8851155fb 100644 --- a/src/domain/disjointDomain.ml +++ b/src/domain/disjointDomain.ml @@ -182,7 +182,6 @@ module type MayEqualSetDomain = sig include SetDomain.S val may_be_equal: elt -> elt -> bool - val amenable_to_meet: elt -> elt -> bool end module ProjectiveSetPairwiseMeet (E: Lattice.S) (B: MayEqualSetDomain with type elt = E.t) (R: Representative with type elt = E.t): SetDomain.S with type elt = E.t = struct @@ -192,7 +191,8 @@ module ProjectiveSetPairwiseMeet (E: Lattice.S) (B: MayEqualSetDomain with type let meet_buckets b1 b2 acc = B.fold (fun e1 acc -> B.fold (fun e2 acc -> - if B.amenable_to_meet e1 e2 then + (* If they have the same representative, we use the normal meet within this bucket *) + if R.equal (R.of_elt e1) (R.of_elt e2) then try let m = E.meet e1 e2 in if not (E.is_bot m) then @@ -200,7 +200,7 @@ module ProjectiveSetPairwiseMeet (E: Lattice.S) (B: MayEqualSetDomain with type else acc with Lattice.Uncomparable -> - failwith (GobPretty.sprintf "amenable_to_meet %a %a returned true, but meet throws!" E.pretty e1 E.pretty e2) + failwith (GobPretty.sprintf "Elements %a and %a are in same bucket, but meet throws!" E.pretty e1 E.pretty e2) else if B.may_be_equal e1 e2 then add e1 (add e2 acc) else From 004e3ae3e286ee7a76d79996aafa4f26e4e34661 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 17 Jan 2025 13:16:41 +0100 Subject: [PATCH 7/8] Pull out `R.of_elt` --- src/domain/disjointDomain.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/domain/disjointDomain.ml b/src/domain/disjointDomain.ml index f8851155fb..3e02c1d3a0 100644 --- a/src/domain/disjointDomain.ml +++ b/src/domain/disjointDomain.ml @@ -190,9 +190,10 @@ module ProjectiveSetPairwiseMeet (E: Lattice.S) (B: MayEqualSetDomain with type let meet m1 m2 = let meet_buckets b1 b2 acc = B.fold (fun e1 acc -> + let r1 = R.of_elt e1 in B.fold (fun e2 acc -> (* If they have the same representative, we use the normal meet within this bucket *) - if R.equal (R.of_elt e1) (R.of_elt e2) then + if R.equal r1 (R.of_elt e2) then try let m = E.meet e1 e2 in if not (E.is_bot m) then From 7f60099fb775434d58222cc6bc3f58eabc4391d9 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 17 Jan 2025 13:31:26 +0100 Subject: [PATCH 8/8] Explain why if is needed and what is checked --- tests/regression/13-privatized/89-write-lacking-precision.c | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/tests/regression/13-privatized/89-write-lacking-precision.c b/tests/regression/13-privatized/89-write-lacking-precision.c index 75ee78974d..bb35cdf6dc 100644 --- a/tests/regression/13-privatized/89-write-lacking-precision.c +++ b/tests/regression/13-privatized/89-write-lacking-precision.c @@ -9,9 +9,10 @@ struct a h = {""}; struct a i = {"string"}; void* d(void* args) { - struct a r; if (c->b) { - __goblint_check(strlen(h.b) == 0); // Should also work for write! + // Handled by privatization as a write + // Without fix (#1468) causes both h.b and i.b to become unknown string + __goblint_check(strlen(h.b) == 0); // Check h.b is still known } }