Unassume benchmarking fixes #1124

sim642 · 2023-08-02T09:01:03Z

Changes

Disable witness lifter if GraphML witness generation disabled (but SV-COMP is still enabled for BenchExec use).
Special case calloc with count 1 in base (cherry-picked from Missing races from free of calloc, special case calloc with count 1 #978).
Fix var_eq may_change for other argument being constant.
Fix fixpoint issue from Regressions from string literals domain #1126.
Handle all_index in evalbinop_base.
Disable CIL check in unassume because variables of typedef types fail.
Fix two unassume literature witnesses.
Improve some tracing.

src/cdomains/intDomain.ml

michael-schwarz

Other than one small comment, LGTM!

michael-schwarz · 2023-08-31T13:41:36Z

src/cdomains/valueDomain.ml

@@ -115,7 +115,7 @@ struct
    | _ -> false

  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"


Why are we treating pthread_cond_t as a mutex type here? That is confusing.

It's just in the base analysis to ignore the condition variable struct contents.

Still, for consistency, I think we should introduce a is_cond_type here, there are several similar functions already around.

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.

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?

And we do something with condition variables, see #520.

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.

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.

…erging #1124

sim642 added 15 commits August 2, 2023 11:41

Improve solside tracing

027b9cd

Handle all_index in evalbinop_base

152f34e

Improve widen tracing

6d04983

Fix var_eq may_change for other argument being constant

f0a0566

Disable CIL check in unassume because variables of typedef types fail

5372a76

Add solchange tracing to TD3 side effects

10881f0

Exclude more pthread types from base

90f155c

Fix relational witness literature examples to also validate

5e19b23

Add non-terminating hh-ex3

e018cb7

Simplify hh-ex3-term

0715a04

Disable witness lifter if GraphML witness generation disabled

ac8baaa

Enable witness.invariant.other in svcomp-yaml-validate conf

33eb674

Fix ARG enabled without ana.sv-comp.enabled

9127dad

Remove pthread_mutexattr_t from is_mutex_type

d512cb5

Special case calloc with count 1 in base

66204e4

sim642 added sv-comp SV-COMP (analyses, results), witnesses precision benchmarking labels Aug 2, 2023

github-advanced-security bot found potential problems Aug 2, 2023

View reviewed changes

src/cdomains/intDomain.ml Fixed Show fixed Hide fixed

Fix trace-not-in-tracing semgrep rule for conjunctions

22f6061

sim642 mentioned this pull request Aug 2, 2023

Missing races from free of calloc, special case calloc with count 1 #978

Closed

sim642 added 3 commits August 3, 2023 11:20

Fix PartitionDomain.SetSet.pretty_diff crash

870a9b8

Add failing fixpoint test case for #1126

4fcfc71

Fix fixpoint issue from #1126

409cbd1

sim642 mentioned this pull request Aug 3, 2023

Regressions from string literals domain #1126

Open

Move options from unassume bench to yaml confs

ddecc85

michael-schwarz approved these changes Aug 31, 2023

View reviewed changes

sim642 added this to the v2.2.0 milestone Sep 5, 2023

sim642 merged commit b80c7d3 into master Sep 5, 2023
16 checks passed

sim642 deleted the yaml-witness-unassume-bench branch September 5, 2023 10:37

sim642 added a commit that referenced this pull request Sep 7, 2023

Fix YAML witness unassume indentation (PR #1124)

d97504b

sim642 mentioned this pull request Sep 13, 2023

[new release] goblint (2.2.0) ocaml/opam-repository#24420

Closed

karoliineh added a commit that referenced this pull request May 24, 2024

Reverts error handling from #114 that is not covered by tests since m…

f325c59

…erging #1124

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Unassume benchmarking fixes #1124

Unassume benchmarking fixes #1124

sim642 commented Aug 2, 2023 •

edited

Loading

michael-schwarz left a comment

michael-schwarz Aug 31, 2023

sim642 Aug 31, 2023

michael-schwarz Aug 31, 2023

sim642 Sep 3, 2023

michael-schwarz Sep 3, 2023

michael-schwarz Sep 3, 2023

sim642 Sep 5, 2023

michael-schwarz Sep 5, 2023

Unassume benchmarking fixes #1124

Unassume benchmarking fixes #1124

Conversation

sim642 commented Aug 2, 2023 • edited Loading

Changes

michael-schwarz left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

sim642 commented Aug 2, 2023 •

edited

Loading