Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Meet of string pointers in address domain imprecise #1467

Open
michael-schwarz opened this issue May 15, 2024 · 1 comment · May be fixed by #1468
Open

Meet of string pointers in address domain imprecise #1467

michael-schwarz opened this issue May 15, 2024 · 1 comment · May be fixed by #1468
Assignees
@michael-schwarz
Labels
bug precision

Comments

@michael-schwarz
Copy link
Member

Currently the meet of an unknown string pointer and a known string pointer is the unknown string pointer.

{"string"} \sqcap {(unknown string)} = {(unknown string)}

The problem seems to be in the address domain, as the actual meet in the string domain which is defined to return the known pointer

analyzer/src/cdomain/value/cdomains/stringDomain.ml

Lines 99 to 108 in bffc5e3

let meet x y =
match x, y with
| None, a
| a, None -> a
| Some a, Some b when a = b -> Some a
| Some a, Some b (* when a <> b *) ->
if get_string_domain () = Disjoint then
raise Lattice.Uncomparable
else
raise Lattice.BotValue

is never actually called.
@michael-schwarz michael-schwarz self-assigned this May 15, 2024
@michael-schwarz
Copy link
Member Author

The call propagates until ProjectiveSetPairwiseMeet

analyzer/src/domain/disjointDomain.ml

Lines 190 to 205 in bffc5e3

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 ())

where B.may_be_equal delegates to

analyzer/src/cdomain/value/cdomains/addressDomain.ml

Line 180 in bffc5e3

let may_be_equal a b = Option.value (Addr.semantic_equal a b) ~default:true

Addr.semantic_equal given by

analyzer/src/cdomain/value/cdomains/addressDomain.ml

Lines 102 to 111 in bffc5e3

let semantic_equal x y = match x, y with
| Addr x, Addr y -> Mval.semantic_equal x y
| StrPtr s1, StrPtr s2 -> SD.semantic_equal s1 s2
| NullPtr, NullPtr -> Some true
| UnknownPtr, UnknownPtr
| UnknownPtr, Addr _
| Addr _, UnknownPtr
| UnknownPtr, StrPtr _
| StrPtr _, UnknownPtr -> None
| _, _ -> Some false

which calls SD.sematic_equal

analyzer/src/cdomain/value/cdomains/stringDomain.ml

Lines 77 to 81 in bffc5e3

let semantic_equal x y =
match x, y with
| None, _
| _, None -> Some true
| Some a, Some b -> if a = b then None else Some false

@michael-schwarz michael-schwarz linked a pull request May 15, 2024 that will close this issue
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@michael-schwarz michael-schwarz

Labels
bug precision
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Make meet in AddressDomain more precise goblint/analyzer
1 participant
@michael-schwarz