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.

Sign up for GitHub

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

Jump to bottom

Thread-modular witnesses benchmarking fixes #977

Merged
merged 24 commits into from
Mar 21, 2023
Merged

Thread-modular witnesses benchmarking fixes #977

merged 24 commits into from
Mar 21, 2023

Conversation

sim642
Copy link
Member

@sim642 sim642 commented Jan 31, 2023 •
edited
Loading

Changes

  1. Improve pretty printing of global constraint variable names for tracing.
  2. Remove Deadcode exceptions from unassume.
  3. Add general LOr handling to base invariant algorithm.
  4. Unify witness invariant locators for unassume and validate.
  5. Add option pre.transform-paths to avoid filename mismatches when consuming YAML witnesses.
  6. Handle exp.no-narrow in TD3.
  7. Look up confs relative to executable directory as well.

TODO

  • Rewrite history to remove all BenchExec stuff, which should go to bench repository.
  • Remove all YAML BenchExec stuff from before.

@sim642 sim642 self-assigned this Jan 31, 2023
sim642 added 20 commits February 2, 2023 12:54
@sim642
Update bench-yaml confs
0b3ef82
@sim642
Merge branch 'master' into yaml-witness-unassume-bench
dfe4445
@sim642
Add SV-COMP programs to YAML privatization benchmarks
bc2fca9
@sim642
Handle exp.no-narrow in TD3
fe41197
@sim642
Make command_line optional in YAML witness
4709fd6
@sim642
Re-add unassume invariant messages for easier debugging
a1ac32e
@sim642
Add option pre.transform-paths
06c025e
@sim642
Disable pre.transform-paths in svcomp-yaml confs for CPAchecker compa…
d259a27 
…tibility
@sim642
Add generic LOr case to BaseInvariant
0ddddbe
@sim642
Add contra hook to BaseInvariant
b2670d0 
Unassume needs to ignore contradiction in LAnd.
@sim642
Fix equality base unassume with id_meet_down
d6b7313
@sim642
Merge branch 'master' into yaml-witness-unassume-bench
6f51ffa
@sim642
Merge branch 'master' into yaml-witness-unassume-bench
361b80c
@sim642
Unify locator logic between unassume and validate
d22e683
@sim642
Merge remote-tracking branches 'origin/base-lor-interval' and 'origin…
654d7bf 
…/base-cmp-def_exc' into yaml-witness-unassume-bench
@sim642
Merge remote-tracking branch 'origin/master' into yaml-witness-unassu…
de0cd51 
…me-bench
@sim642
Merge remote-tracking branch 'origin/master' into yaml-witness-unassu…
1a9b492 
…me-bench
@sim642
Also look up confs relative to dev directory
e79f47f
@sim642
Trace increasing side effects in TD3
361a349
@sim642
Improve printing of global constraint variable names
d697cec
@sim642 sim642 force-pushed the yaml-witness-unassume-bench branch from 952c63f to d697cec Compare February 2, 2023 10:55
@sim642 sim642 added debugging Abstract debugging preprocessing C preprocessing labels Feb 2, 2023
@sim642 sim642 marked this pull request as ready for review February 2, 2023 11:23
@michael-schwarz michael-schwarz self-requested a review March 12, 2023 06:04
@sim642 sim642 merged commit 45cb427 into master Mar 21, 2023
@sim642 sim642 deleted the yaml-witness-unassume-bench branch March 21, 2023 13:55
@sim642 sim642 added this to the v2.2.0 milestone Apr 5, 2023
@sim642 sim642 mentioned this pull request Sep 13, 2023
Closed
sim642 added a commit to sim642/opam-repository that referenced this pull request Sep 13, 2023
@sim642
[new release] goblint (2.2.0)
eb80bce 
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).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@michael-schwarz michael-schwarz michael-schwarz approved these changes

Assignees

@sim642 sim642

Labels
benchmarking debugging Abstract debugging precision preprocessing C preprocessing
Projects
None yet
Milestone
v2.2.0
Development

Successfully merging this pull request may close these issues.
2 participants
@sim642 @michael-schwarz