Use-after-free Analysis: Fix warning generation for lvalues #1862
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…analysis. This test case was minimized from a larger example by Michael Schwarz. Co-authored-by: Michael Schwarz <[email protected]>
Given, e.g., a statement lval = rval; There may be two types of use-after-free errors that can occur for the lval: 1. The memory location to which lval evaluates has been freed already. 2. The memory location(s) inside rval that are dereferenced to evaluate rval have been freed already. Previously, the check implemented for lvals did not consistently check for both types of errors. In case a dereference was at the top-level of the lval, only the second type of error was checked, but not recursively for sub-lvals. This is changed with this PR. The 1. check is now performed, whether the lhost is a variable or a memory dereference. The second check is performed using a recursive call of the mutually recursive function `warn_exp_might_contain_freed`.
|
I started an svcomp run a minute ago, I will test svcomp25 and branchset-pathsensitive |
sim642
reviewed
Nov 5, 2025
There was a problem hiding this comment.
One of the spurious warnings on sv-benchmarks this causes is
[Warning][Behavior > Undefined > UseAfterFree][CWE-416] lval ((alloc@sid:145@tid:[main](#0))) in "assign" points to a maybe freed memory region (../sv-benchmarks/c/Juliet_Test/CWE415_Double_Free---s01---CWE415_Double_Free__malloc_free_char_32_good.i:695:10-695:29)
which is
char *data_1 = *dataPtr2;which actually is the initialization assignment
data_1 = *dataPtr2;It seems to me that here there are also extra warnings from the right-hand side now. Here *dataPtr2 is a points-to set which contains a free-d pointer, but that's irrelevant. It would only be a problem if it was **dataPtr2.
Maybe this is now overly aggressive at checking dereferences recursively?
| let undefined_behavior = if is_free then Undefined DoubleFree else Undefined UseAfterFree in | ||
| let cwe_number = if is_free then 415 else 416 in | ||
|
|
||
| let check_adress adresses = |
There was a problem hiding this comment.
Suggested change
| let check_adress adresses = | |
| let check_address addresses = |
Also usages of both below.
Comment on lines
+121
to
+126
| match addr with | ||
| | Queries.AD.Addr.Addr (v,_) when man.ask (Queries.IsAllocVar v) -> v :: vars | ||
| | _ -> vars | ||
| ) adresses [] | ||
| in | ||
| if not (Queries.AD.is_top adresses) then begin |
There was a problem hiding this comment.
The pointed_to_heap_vars above could be moved into this if, right?
2 tasks
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This fixes the handling of lvals in the warning generation of the use-after-free analysis in
warn_lval_might_contain_freed.Background
Given, e.g., a statement
There may be two types of use-after-free errors that can occur for the lval:
Previously, the check implemented for lvals did not consistently check for both types of errors.
In case a dereference was at the top-level of the lval, only the second type of error was checked; also this was not check recursively for sub-lvals.
Changes
This is changed with this PR.
The check for (1.) is now performed whether the lhost is a variable or a memory dereference.
The check for (2.) is performed, in case that the lhost is a dereference, and uses a recursive call of the function
warn_exp_might_contain_freedthat is mutually recursive withwarn_lval_might_contain_freed.Fixes #1861