Improve multi-threaded UAF analysis and add SVComp result generation #1123
Conversation
Currently only considering UAF
This aims to improve precision
tests/regression/74-use_after_free/13-multi-threaded-uaf-with-joined-thread.c
Show resolved
Hide resolved
| else if Str.string_match regexp s 0 then | ||
| let global = Str.matched_group 1 s in | ||
| if global = "valid-free" then | ||
| ValidFree | ||
| else if global = "valid-deref" then | ||
| ValidDeref | ||
| else if global = "valid-memtrack" then | ||
| ValidMemtrack | ||
| else | ||
| failwith "Svcomp.Specification.of_string: unknown global expression" |
There was a problem hiding this comment.
The problem with this is that the property file in SV-COMP doesn't contain just one, but all three at once: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/3d65c76d8521ef5bc79077a31e7b7e41dd077309/c/properties/valid-memsafety.prp.
But we can leave it for now if the idea is to at least test one of them specifically. I can do larger refactoring of the SV-COMP stuff to allow for multi-property.
It just means that as-is, this isn't ready for valid-memsafety.prp from SV-COMP.
There was a problem hiding this comment.
I'd suggest that we discuss and implement support for supporting all three properties, so that we can try and let all relevant analyses for memory safety run together in order to be able to evaluate how we are actually performing in SV-COMP for memory safety.
There was a problem hiding this comment.
This stuff was run on SV-COMP but that was done per-specification or? because there's no handling of all three simultaneously here still.
There was a problem hiding this comment.
We added a workaround by having an internal "memory-safety" property which unites all three. This way we were able to let all three run and be tested simultaneously for the benchmarks
There was a problem hiding this comment.
To clarify, this will be fixed in a follow-up PR, which will contain commits from the https://github.com/goblint/analyzer/tree/staging_memsafety branch, we just don't want to include them here yet to avoid polluting the history.
|
@sim642 If you still want to review this, it would be nice to do it soon, we hope to merge most of Stanimir's things before he defends his thesis in two weeks. |
| else if Str.string_match regexp s 0 then | ||
| let global = Str.matched_group 1 s in | ||
| if global = "valid-free" then | ||
| ValidFree | ||
| else if global = "valid-deref" then | ||
| ValidDeref | ||
| else if global = "valid-memtrack" then | ||
| ValidMemtrack | ||
| else | ||
| failwith "Svcomp.Specification.of_string: unknown global expression" |
There was a problem hiding this comment.
This stuff was run on SV-COMP but that was done per-specification or? because there's no handling of all three simultaneously here still.
|
@mrstanb can you resolve the merge conflict with master? Then we should be good to go! |
Sure, right away. |
This PR:
(tid, {must-joined threads}), wheretiddenotes the tid of a thread which has freed the memory being tracked for UAF