diff --git a/src/analyses/base.ml b/src/analyses/base.ml index c7ec23a217..b11933b016 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -344,15 +344,18 @@ struct if AD.is_definite x && AD.is_definite y then let ax = AD.choose x in let ay = AD.choose y in - if AD.Addr.equal ax ay then - match AD.Addr.to_var ax with + let handle_address_is_multiple addr = begin match AD.Addr.to_var addr with | Some v when a.f (Q.IsMultiple v) -> None | _ -> Some true - else - (* If they are unequal, it does not matter if the underlying var represents multiple concrete vars or not *) - Some false + end + in + match AD.Addr.semantic_equal ax ay with + | Some true -> + handle_address_is_multiple ax + | Some false -> Some false + | None -> None else None in diff --git a/src/cdomains/addressDomain.ml b/src/cdomains/addressDomain.ml index 7cfffd3dcd..c6905a5cdc 100644 --- a/src/cdomains/addressDomain.ml +++ b/src/cdomains/addressDomain.ml @@ -20,12 +20,19 @@ end module AddressSet (Idx: IntDomain.Z) = struct + module BaseAddr = Lval.BaseAddrRepr (Idx) module Addr = Lval.NormalLatRepr (Idx) - module J = SetDomain.Joined (Addr) + module J = (struct + include SetDomain.Joined (Addr) + let may_be_equal a b = Option.value (Addr.semantic_equal a b) ~default:true + end) + module OffsetSplit = DisjointDomain.ProjectiveSetPairwiseMeet (Addr) (J) (Addr.R) + (* module H = HoareDomain.SetEM (Addr) *) (* Hoare set for bucket doesn't play well with StrPtr limiting: https://github.com/goblint/analyzer/pull/808 *) - include DisjointDomain.ProjectiveSet (Addr) (J) (Addr.R) + module AddressSet : SetDomain.S with type elt = Addr.t = DisjointDomain.ProjectiveSet (BaseAddr) (OffsetSplit) (BaseAddr.R) + include AddressSet (* short-circuit with physical equality, makes a difference at long-scale: https://github.com/goblint/analyzer/pull/809#issuecomment-1206174751 *) diff --git a/src/cdomains/lval.ml b/src/cdomains/lval.ml index f979b60130..ce80b799e3 100644 --- a/src/cdomains/lval.ml +++ b/src/cdomains/lval.ml @@ -18,16 +18,10 @@ sig val to_int: t -> IntOps.BigIntOps.t option end -module type IdxDomain = -sig - include IdxPrintable - include Lattice.S with type t := t -end - -module OffsetPrintable (Idx: IdxPrintable) = +module Offset (Idx: IdxPrintable) = struct type t = (fieldinfo, Idx.t) offs - include Printable.Std + include Printable.StdLeaf let name () = "offset" @@ -113,9 +107,9 @@ struct | `Index(i,o) -> NoOffset (* array domain can not deal with this -> leads to being handeled as access to unknown part *) end -module Offset (Idx: IdxDomain) = +module OffsetLat (Idx: IntDomain.Z) = struct - include OffsetPrintable (Idx) + include Offset (Idx) let rec leq x y = match x, y with @@ -150,6 +144,43 @@ struct | `NoOffset -> `NoOffset end +module OffsetLatWithSemanticEqual (Idx: IntDomain.Z) = +struct + include OffsetLat (Idx) + + let ikind () = Cilfacade.ptrdiff_ikind () + + let offset_to_index_offset typ offs = + let idx_of_int x = + Idx.of_int (ikind ()) (Z.of_int x) + in + let rec offset_to_index_offset ?typ offs = match offs with + | `NoOffset -> idx_of_int 0 + | `Field (field, o) -> + let field_as_offset = Field (field, NoOffset) in + let bits_offset, _size = GoblintCil.bitsOffset (TComp (field.fcomp, [])) field_as_offset in + let bits_offset = idx_of_int bits_offset in + let remaining_offset = offset_to_index_offset ~typ:field.ftype o in + Idx.add bits_offset remaining_offset + | `Index (x, o) -> + match Option.map unrollType typ with + | Some TArray(item_typ, _, _) -> + let item_size_in_bits = bitsSizeOf item_typ in + let item_size_in_bits = idx_of_int item_size_in_bits in + let bits_offset = Idx.mul item_size_in_bits x in + let remaining_offset = offset_to_index_offset ~typ:item_typ o in + Idx.add bits_offset remaining_offset + | _ -> Idx.top () + in + offset_to_index_offset ~typ offs + + let semantic_equal ~xtyp ~xoffs ~ytyp ~yoffs = + let x_index = offset_to_index_offset xtyp xoffs in + let y_index = offset_to_index_offset ytyp yoffs in + Idx.to_bool (Idx.eq x_index y_index) + +end + module type S = sig type field @@ -181,14 +212,11 @@ sig (** Finds the type of the address location. *) end -module Normal (Idx: IdxPrintable) = +module PreNormal (Offset: Printable.S) = struct - type field = fieldinfo - type idx = Idx.t - module Offs = OffsetPrintable (Idx) - + include Printable.StdLeaf type t = - | Addr of CilType.Varinfo.t * Offs.t (** Pointer to offset of a variable. *) + | Addr of CilType.Varinfo.t * Offset.t (** Pointer to offset of a variable. *) | NullPtr (** NULL pointer. *) | UnknownPtr (** Unknown pointer. Could point to globals, heap and escaped variables. *) | StrPtr of string option (** String literal pointer. [StrPtr None] abstracts any string pointer *) @@ -202,7 +230,34 @@ struct hash x | _ -> hash x - include Printable.StdLeaf + let show_addr (x, o) = + if RichVarinfo.BiVarinfoMap.Collection.mem_varinfo x then + let description = RichVarinfo.BiVarinfoMap.Collection.describe_varinfo x in + "(" ^ x.vname ^ ", " ^ description ^ ")" ^ Offset.show o + else x.vname ^ Offset.show o + + let show = function + | Addr (x, o)-> show_addr (x, o) + | StrPtr (Some x) -> "\"" ^ x ^ "\"" + | StrPtr None -> "(unknown string)" + | UnknownPtr -> "?" + | NullPtr -> "NULL" + + include Printable.SimpleShow ( + struct + type nonrec t = t + let show = show + end + ) +end + +module Normal (Idx: IdxPrintable) = +struct + type field = fieldinfo + type idx = Idx.t + module Offs = Offset (Idx) + include PreNormal (Offs) + let name () = "Normal Lvals" type group = Basetype.Variables.group @@ -233,31 +288,6 @@ struct | StrPtr (Some x) -> Some x | _ -> None - let rec short_offs = function - | `NoOffset -> "" - | `Field (fld, o) -> "." ^ fld.fname ^ short_offs o - | `Index (v, o) -> "[" ^ Idx.show v ^ "]" ^ short_offs o - - let short_addr (x, o) = - if RichVarinfo.BiVarinfoMap.Collection.mem_varinfo x then - let description = RichVarinfo.BiVarinfoMap.Collection.describe_varinfo x in - "(" ^ x.vname ^ ", " ^ description ^ ")" ^ short_offs o - else x.vname ^ short_offs o - - let show = function - | Addr (x, o)-> short_addr (x, o) - | StrPtr (Some x) -> "\"" ^ x ^ "\"" - | StrPtr None -> "(unknown string)" - | UnknownPtr -> "?" - | NullPtr -> "NULL" - - include Printable.SimpleShow ( - struct - type nonrec t = t - let show = show - end - ) - (* exception if the offset can't be followed completely *) exception Type_offset of typ * string (* tries to follow o in t *) @@ -273,7 +303,7 @@ struct in type_offset fi.ftype o | TComp _, `Index (_,o) -> type_offset t o (* this happens (hmmer, perlbench). safe? *) | t,o -> - let s = sprint ~width:max_int @@ dprintf "Addr.type_offset: could not follow offset in type. type: %a, offset: %s" d_plaintype t (short_offs o) in + let s = sprint ~width:max_int @@ dprintf "Addr.type_offset: could not follow offset in type. type: %a, offset: %a" d_plaintype t Offs.pretty o in raise (Type_offset (t, s)) let get_type_addr (v,o) = try type_offset v.vtype o with Type_offset (t,_) -> t @@ -326,10 +356,30 @@ end - {!NullPtr} is a singleton sublattice. - {!UnknownPtr} is a singleton sublattice. - If [ana.base.limit-string-addresses] is enabled, then all {!StrPtr} are together in one sublattice with flat ordering. If [ana.base.limit-string-addresses] is disabled, then each {!StrPtr} is a singleton sublattice. *) -module NormalLat (Idx: IdxDomain) = +module NormalLat (Idx: IntDomain.Z) = struct include Normal (Idx) - module Offs = Offset (Idx) + module Offs = OffsetLatWithSemanticEqual (Idx) + + (** Semantic equal. [Some true] if definitely equal, [Some false] if definitely not equal, [None] otherwise *) + let semantic_equal x y = match x, y with + | Addr (x, xoffs), Addr (y, yoffs) -> + if CilType.Varinfo.equal x y then + let xtyp = x.vtype in + let ytyp = y.vtype in + Offs.semantic_equal ~xtyp ~xoffs ~ytyp ~yoffs + else + Some false + | StrPtr None, StrPtr _ + | StrPtr _, StrPtr None -> Some true + | StrPtr (Some a), StrPtr (Some b) -> if a = b then None else Some false + | NullPtr, NullPtr -> Some true + | UnknownPtr, UnknownPtr + | UnknownPtr, Addr _ + | Addr _, UnknownPtr + | UnknownPtr, StrPtr _ + | StrPtr _, UnknownPtr -> None + | _, _ -> Some false let is_definite = function | NullPtr -> true @@ -390,7 +440,30 @@ struct end (** Lvalue lattice with sublattice representatives for {!DisjointDomain}. *) -module NormalLatRepr (Idx: IdxDomain) = +module BaseAddrRepr (Idx: IntDomain.Z) = +struct + include NormalLat (Idx) + + module R: DisjointDomain.Representative with type elt = t = + struct + type elt = t + + module AnyOffset = Printable.UnitConf (struct let name = "" end) + include PreNormal (AnyOffset) + + let name () = "BaseAddrRepr.R" + + let of_elt (x: elt): t = match x with + | Addr (v, o) -> Addr (v, ()) + | StrPtr _ when GobConfig.get_bool "ana.base.limit-string-addresses" -> StrPtr None (* all strings together if limited *) + | StrPtr x -> StrPtr x (* everything else is kept separate, including strings if not limited *) + | NullPtr -> NullPtr + | UnknownPtr -> UnknownPtr + end +end + +(** Lvalue lattice with sublattice representatives for {!DisjointDomain}. *) +module NormalLatRepr (Idx: IntDomain.Z) = struct include NormalLat (Idx) diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml index 288f675bee..035094125b 100644 --- a/src/cdomains/valueDomain.ml +++ b/src/cdomains/valueDomain.ml @@ -3,7 +3,7 @@ open Pretty open PrecisionUtil include PreValueDomain -module Offs = Lval.Offset (IndexDomain) +module Offs = Lval.OffsetLat (IndexDomain) module M = Messages module GU = Goblintutil module Q = Queries diff --git a/src/domains/disjointDomain.ml b/src/domains/disjointDomain.ml index cb7a361384..db055561c4 100644 --- a/src/domains/disjointDomain.ml +++ b/src/domains/disjointDomain.ml @@ -27,7 +27,12 @@ end Common choices for [B] are {!SetDomain.Joined} and {!HoareDomain.SetEM}. Handles {!Lattice.BotValue} from [B]. *) -module ProjectiveSet (E: Printable.S) (B: SetDomain.S with type elt = E.t) (R: Representative with type elt = E.t): SetDomain.S with type elt = E.t = +module ProjectiveSet (E: Printable.S) (B: SetDomain.S with type elt = E.t) (R: Representative with type elt = E.t): +sig + include SetDomain.S with type elt = E.t + val fold_buckets: (R.t -> B.t -> 'a -> 'a) -> t -> 'a -> 'a +end += struct type elt = E.t @@ -174,6 +179,36 @@ struct let min_elt m = SetDomain.unsupported "Projective.min_elt" let max_elt m = SetDomain.unsupported "Projective.max_elt" let disjoint m1 m2 = is_empty (inter m1 m2) (* TODO: optimize? *) + + let fold_buckets = M.fold +end + +module type MayEqualSetDomain = +sig + include SetDomain.S + val may_be_equal: 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 + 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 + add e1 (add e2 acc) + else + acc + ) b2 acc + ) b1 acc + in + fold_buckets (fun _ b1 acc -> + fold_buckets (fun _ b2 acc -> + meet_buckets b1 b2 acc + ) m2 acc + ) m1 (empty ()) + end (** {2 By congruence} *) diff --git a/tests/regression/02-base/91-ad-meet.c b/tests/regression/02-base/91-ad-meet.c index 456234afb1..1503182f2b 100644 --- a/tests/regression/02-base/91-ad-meet.c +++ b/tests/regression/02-base/91-ad-meet.c @@ -1,16 +1,59 @@ -// SKIP -// TODO: be sound and claim that assert may hold instead of must not hold -// assert passes when compiled +//PARAM: --set ana.malloc.unique_address_count 1 #include +#include struct s { int fst; }; +void blob_offsets(){ + int *a = malloc(10 * sizeof(int)); + int *b = a; + + // Relies on malloc uniqueness, but zero offset can be determined to be equal. + __goblint_check(a == b); + + // TODO: Determine bitoffsets for blocks (currently top) + __goblint_check(a + 4 == b + 4); //TODO + __goblint_check(a == b + 1 ); //TODO +} + +void array_offsets(){ + int a[10]; + int *b = a; + int *c = a + 2; + + __goblint_check(a == b); + __goblint_check(a + 2 == c); + __goblint_check(b + 2 == c); + + __goblint_check(a + 1 == b + 1); + __goblint_check(a + 1 + 2 == c + 1 ); + __goblint_check(b + 1 + 2 == c + 1 ); +} + +typedef struct { + int x; + int y; +} tuple; + +void array_with_tuple_offsets(){ + tuple ts[10]; + + __goblint_check(&(ts[3].x) == &(ts[3].x)); + __goblint_check(&(ts[3].x) != &(ts[3].y)); + __goblint_check((void*) &(ts[3]) != (void*) &(ts[3].y)); +} + int main() { struct s a; void *p = &a.fst; void *q = ((int(*)[1]) (&a))[0]; - assert(p == q); + // as an __goblint_check, this passes when compiled + __goblint_check(p == q); //UNKNOWN + + blob_offsets(); + array_offsets(); + array_with_tuple_offsets(); return 0; } diff --git a/tests/regression/02-base/92-ad-union-fields.c b/tests/regression/02-base/92-ad-union-fields.c index 2545d88a54..2da2194595 100644 --- a/tests/regression/02-base/92-ad-union-fields.c +++ b/tests/regression/02-base/92-ad-union-fields.c @@ -1,4 +1,3 @@ -// SKIP // TODO: be sound and claim that assert may hold instead of must not hold // assert passes when compiled #include diff --git a/tests/regression/02-base/93-ad-struct-offset.c b/tests/regression/02-base/93-ad-struct-offset.c index f9ce8f8987..c1ea876700 100644 --- a/tests/regression/02-base/93-ad-struct-offset.c +++ b/tests/regression/02-base/93-ad-struct-offset.c @@ -1,4 +1,3 @@ -// SKIP #include struct str{ int a; @@ -21,8 +20,8 @@ int main(){ z = 2; } - // Aaccording to the C standard (section 6.2.8 in the C11 standard), + // According to the C standard (section 6.2.8 in the C11 standard), // the alignment of fields in structs is implementation defined. // When compiling with GCC, the following check as an assert happens to hold. - __goblint_check(z==1); //UNKNOWN! + __goblint_check(z==1); //UNKNOWN } diff --git a/tests/regression/69-addresses/01-meet.c b/tests/regression/69-addresses/01-meet.c new file mode 100644 index 0000000000..d5ac776249 --- /dev/null +++ b/tests/regression/69-addresses/01-meet.c @@ -0,0 +1,23 @@ +#include +#include + +int main(){ + long long l; + + int* p = malloc(sizeof(int)); + + int i; + int* p2 = (int*) i; // create a top-pointer + + __goblint_check(p == p2); //UNKNOWN! + + if(p == p2){ + __goblint_check(p == p2); //TODO + } + + if(p2 == p){ + __goblint_check(p == p2); //TODO + } + + return 0; +} \ No newline at end of file diff --git a/tests/regression/69-addresses/02-array-cast.c b/tests/regression/69-addresses/02-array-cast.c new file mode 100644 index 0000000000..6a3f123ac7 --- /dev/null +++ b/tests/regression/69-addresses/02-array-cast.c @@ -0,0 +1,26 @@ +// SKIP +#include + +int main() { + int a[10]; + int *b = a; + + __goblint_check(a == b); + __goblint_check(a + 4 == b + 4); + + char *b_char = (char*) a; + __goblint_check((void*) a == (void*) b_char ); + + char* a_intoffset =(char*) (a + 1); + char* b_intoffset = b_char + sizeof(int); + + __goblint_check(a_intoffset == b_intoffset); + __goblint_check((char*) (a + 1) == b_char + sizeof(int)); + + char* a_4intoffset = (char*) (a + 4); + + __goblint_check(a_4intoffset == b_intoffset); // FAIL + __goblint_check((char*) (a + 4) == b_char + sizeof(int)); // FAIL + + return 0; +}