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.

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

Read offsets separately in eval_rv_base for pointer dereference #935

Merged
merged 8 commits into from
Dec 2, 2022

Conversation

jerhard
Copy link
Member

@jerhard jerhard commented Dec 1, 2022

This PR changes the treatment of pointer dereference eval_rv_base and the Structs.get method, to avoid producing top in the cases described in #716.

The change affects the case that eval_rv_base evaluates a pointer that is dereferenced and some offset is taken from the resulting value. Previously, all objects that the pointer could point to without the offset. Then, these memory objects were joined, and the offset was taken from the result. This led to additional imprecision in case of the join of e.g. structs of different type.

Now, eval_rv_base will look at all the possible target addresses, and read for each of them the value at the offset. Then, the values at the offsets are joined, to produce the result.
The struct domain is changed such that get yields a top_value of the corresponding type, rather than 'Top. This way, if a field of pointer type is requested, but the abstract value does not contain the field, a top pointer ({?, NULL}) is constructed instead of 'Top. By avoiding to produce the 'Top in this case, addresses are read from structs of the appropriate type are kept in the result of the join.

Closes #716.

@jerhard
Copy link
Member Author

jerhard commented Dec 1, 2022

When the list of malloc-wrappers is provided to Goblint, this also fixes the issue of warnings for no suitable function existing for dynamic function calls dereferencing pointers with some field offset, e.g.:

[Warning][Unsound] Unknown call to function *(inst->handler). (nameserv_async.c:94:4-94:66)
[Warning][Unsound] No suitable function to be called at call site. Continuing with state before call. (nameserv_async.c:94:4-94:66)

There remain four cases of "No suitable function to be called at call site. Continuing with state before call", however, these are cases, where the function pointer is only ever set to Null. So this is not an issue caused by the analysis.

@sim642
Copy link
Member

sim642 commented Dec 2, 2022

Now, eval_rv_base will look at all the possible target addresses, and read for each of them the value at the offset. Then, the values at the offsets are joined, to produce the result.

This replaces one eval_offset with as many as there are elements in the address set, which could have a performance impact.
I suppose the Munich benchmarking server is currently busy with interactive, so I'll do the benchmarks on the Tartu server.

src/analyses/base.ml Outdated Show resolved Hide resolved
@sim642
Copy link
Member

sim642 commented Dec 2, 2022

This replaces one eval_offset with as many as there are elements in the address set, which could have a performance impact.
I suppose the Munich benchmarking server is currently busy with interactive, so I'll do the benchmarks on the Tartu server.

A bit surprisingly there's no effect:
image
(Full table)

I guess eval_offset is cheap enough.

@jerhard
Copy link
Member Author

jerhard commented Dec 2, 2022

Thanks for benchmarking this! Good to know that it does in general not have a negative impact on performance.

@jerhard jerhard merged commit 51f6a40 into master Dec 2, 2022
@jerhard jerhard deleted the issue_716 branch December 2, 2022 15:37
@sim642 sim642 added this to the v2.2.0 milestone Apr 5, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Different field access on imprecise address set
2 participants