Unassume benchmarking fixes #1124
Conversation
sim642
added
sv-comp
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
michael-schwarz
left a comment
michael-schwarz
left a comment
There was a problem hiding this comment.
Other than one small comment, LGTM!
|
|
||
| let is_mutex_type (t: typ): bool = match t with | ||
| | TNamed (info, attr) -> info.tname = "pthread_mutex_t" || info.tname = "spinlock_t" || info.tname = "pthread_spinlock_t" | ||
| | TNamed (info, attr) -> info.tname = "pthread_mutex_t" || info.tname = "spinlock_t" || info.tname = "pthread_spinlock_t" || info.tname = "pthread_cond_t" |
There was a problem hiding this comment.
Why are we treating pthread_cond_t as a mutex type here? That is confusing.
There was a problem hiding this comment.
It's just in the base analysis to ignore the condition variable struct contents.
There was a problem hiding this comment.
Still, for consistency, I think we should introduce a is_cond_type here, there are several similar functions already around.
There was a problem hiding this comment.
It wouldn't be more consistent though because it still uses Mutex for ValueDomain. I don't think it's worth it to introduce Cond into ValueDomain just for this. Mutex analyses treat condition variables via unlock-lock anyway.
There was a problem hiding this comment.
Mutex analyses treat condition variables via unlock-lock anyway.
What do you mean by this? If there is an analysis that does this, it is wrong. (Or are you talking about the second argument of pthread_cond_wait? That seems to be unrelated, no?
There was a problem hiding this comment.
And we do something with condition variables, see #520.
There was a problem hiding this comment.
Well yes, but we don't care about the implementation detail struct of a condition variable in base, just like we don't care about it for mutexes. All this does is make the contents opaque instead of tracking a struct whose contents our special functions don't update and thus those contents are outright wrong.
There was a problem hiding this comment.
I get that. I still think it is cleaner to have a dedicated function for this case, rather than confusing things. Maybe one should replace Mutex in base with OpaquePThreadType or something like this?
However, my happiness isn't tied up in this, so if you prefer we can merge as-is.
CHANGES: * Add `setjmp`/`longjmp` analysis (goblint/analyzer#887, goblint/analyzer#970, goblint/analyzer#1015, goblint/analyzer#1019). * Refactor race analysis to lazy distribution (goblint/analyzer#1084, goblint/analyzer#1089, goblint/analyzer#1136, goblint/analyzer#1016). * Add thread-unsafe library function call analysis (goblint/analyzer#723, goblint/analyzer#1082). * Add mutex type analysis and mutex API analysis (goblint/analyzer#800, goblint/analyzer#839, goblint/analyzer#1073). * Add interval set domain and string literals domain (goblint/analyzer#901, goblint/analyzer#966, goblint/analyzer#994, goblint/analyzer#1048). * Add affine equalities analysis (goblint/analyzer#592). * Add use-after-free analysis (goblint/analyzer#1050, goblint/analyzer#1114). * Add dead code elimination transformation (goblint/analyzer#850, goblint/analyzer#979). * Add taint analysis for partial contexts (goblint/analyzer#553, goblint/analyzer#952). * Add YAML witness validation via unassume (goblint/analyzer#796, goblint/analyzer#977, goblint/analyzer#1044, goblint/analyzer#1045, goblint/analyzer#1124). * Add incremental analysis rename detection (goblint/analyzer#774, goblint/analyzer#777). * Fix address sets unsoundness (goblint/analyzer#822, goblint/analyzer#967, goblint/analyzer#564, goblint/analyzer#1032, goblint/analyzer#998, goblint/analyzer#1031). * Fix thread escape analysis unsoundness (goblint/analyzer#939, goblint/analyzer#984, goblint/analyzer#1074, goblint/analyzer#1078). * Fix many incremental analysis issues (goblint/analyzer#627, goblint/analyzer#836, goblint/analyzer#835, goblint/analyzer#841, goblint/analyzer#932, goblint/analyzer#678, goblint/analyzer#942, goblint/analyzer#949, goblint/analyzer#950, goblint/analyzer#957, goblint/analyzer#955, goblint/analyzer#954, goblint/analyzer#960, goblint/analyzer#959, goblint/analyzer#1004, goblint/analyzer#558, goblint/analyzer#1010, goblint/analyzer#1091). * Fix server mode for abstract debugging (goblint/analyzer#983, goblint/analyzer#990, goblint/analyzer#997, goblint/analyzer#1000, goblint/analyzer#1001, goblint/analyzer#1013, goblint/analyzer#1018, goblint/analyzer#1017, goblint/analyzer#1026, goblint/analyzer#1027). * Add documentation for configuration JSON schema and OCaml API (goblint/analyzer#999, goblint/analyzer#1054, goblint/analyzer#1055, goblint/analyzer#1053). * Add many library function specifications (goblint/analyzer#962, goblint/analyzer#996, goblint/analyzer#1028, goblint/analyzer#1079, goblint/analyzer#1121, goblint/analyzer#1135, goblint/analyzer#1138). * Add OCaml 5.0 support (goblint/analyzer#1003, goblint/analyzer#945, goblint/analyzer#1162).
Changes
callocwith count 1 in base (cherry-picked from Missing races fromfreeofcalloc, special casecallocwith count 1 #978).may_changefor other argument being constant.all_indexinevalbinop_base.