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

SV-COMP 2024 development #1257

Merged
merged 87 commits into from
Nov 24, 2023
Merged

SV-COMP 2024 development #1257

merged 87 commits into from
Nov 24, 2023

Conversation

sim642
Copy link
Member

@sim642 sim642 commented Nov 20, 2023 •
edited
Loading

This branch contains development and integration for SV-COMP 2024. This branch is used for creating verifier archives for preruns.

PRs

It includes some not-yet merged PRs:

  1. Improve SV-COMP conf for no-data-race #1207
  2. Fix YAML witness invariants for unrolled loops #1248
  3. Account for allocated heap memory which is unreachable from globals #1241
  4. Improve multi-threaded valid-memcleanup #1246

Changes

Additionally, it contains:

  1. Add svcomp24 and svcomp24-validate confs:
    1. Make threadflag path sensitive.
    2. Add ldv_kzalloc as malloc wrapper.
    3. Disable races from free and standard library calls.
    4. YAML witness generation: invariant_set with loop_invariant-s.
    5. YAML witness validation with unassume.
  2. Update SV-COMP releasing documentation.
  3. Deactivate mhp and region in single-threaded programs.
  4. Fix relation analysis crash due to untracked variables.
  5. Add option ana.race.call for thread-unsafe standard library call race reporting.
  6. Add strict YAML witness validation (with option witness.yaml.strict).
  7. Use exp.architecture option for preprocessing to avoid incompatible type warnings from CIL merging.
  8. Implement YAML witness generation with exponentially increasing buffer size.
  9. Fix YAML invariant_set format.

sim642 and others added 30 commits October 4, 2023 11:49
@sim642
Add ldv_kzalloc to svcomp malloc wrappers
80b3b72
@sim642
Disable free races in svcomp
35f6d00 
They should be considered MemSafety issues instead.
@sim642
Make threadid path sensitive in svcomp
b6dfb14 
This is required for some ldv-races/ no-data-race tasks.
@sim642
Use exp.architecture for SV-COMP preprocessing
11164fd 
Avoids a large number or CIL warnings about mismatching types.
@sim642
Add option ana.race.call
94307d0
@sim642
Use threadflag path-sensitivity instead of threadid in svcomp conf
35f9323 
This is enough for ldv-races/race-2_1-container_of, etc, but cheaper.
@sim642
Merge branch 'master' into svcomp24-conf
ebc8cf8
@sim642
Merge branch 'sv-comp-yaml' into svcomp24-dev
b80ba98
@sim642
Merge branch 'sv-comp-multiproperty' into svcomp24-dev
4910a51
@sim642
Copy svcomp conf to svcomp24
f4b3710
@sim642
Add YAML witness generation to svcomp confs
529a415
@sim642
Copy svcomp24 conf to svcomp24-validate
ab9eacc
@sim642
Add YAML witness validation to svcomp24-validate conf
95ee32e
@sim642
Update sv-comp/archive.sh for 2024
ce917e6
@sim642
Fix Apron license for unpinned package for SV-COMP
6bad00c
@mrstanb
Warn whenever there's allocated heap memory that's unreachable from g…
421abcd 
…lobals at program exit
@mrstanb
Add test cases for unreachable heap memory from globals
9f7224e
@mrstanb
Remove //TODO comment from 76/09
c056b32
@mrstanb @michael-schwarz
Don't set InvalidMemTrack flag a second time
175b003 
Co-authored-by: Michael Schwarz <michael.schwarz93@gmail.com>
@mrstanb @michael-schwarz
Don't set InvalidMemTrack flag a second time
05e4892 
Co-authored-by: Michael Schwarz <michael.schwarz93@gmail.com>
@mrstanb
Add 3 regr. tests for trying out global struct variables
f343d74
@sim642
Merge branch 'master' into svcomp24-conf
afdf566
@sim642
Merge branch 'master' into svcomp24-conf
6aed24f
@sim642
Merge branch 'svcomp24-conf' into svcomp24-dev
c88a1fa
@sim642
Merge branch 'yaml-witness-2.0' into svcomp24-dev
0698aad
@sim642
Fix relation read_globals_to_locals reading untracked variables
7fc8343
@sim642
Remove default Apron polyhedra in svcomp24-validate conf
fbc66e3
@sim642
Merge branch 'yaml-witness-2.0' into svcomp24-dev
39b9834
@michael-schwarz
Merge branch 'master' into improve-valid-memtrack-for-single-threaded…
24fd4e8 
…-programs
@mrstanb
Improve the detection of reachable memory through global struct vars
6decbdd
@sim642 sim642 self-assigned this Nov 20, 2023
sim642 and others added 23 commits November 21, 2023 11:21
@sim642
Fix invariant_set elements schema in YAML witnesses
8b79948
@michael-schwarz
Add example where better privatization helps
ca61360
@sim642
Merge branch 'master' into svcomp24-dev
f75a5ac
@jerhard
Check at end of main thread that the program is certainly single-thre…
2cc915f 
…aded.

If other threads are not joined, they may be killed by the main thread returning.
This will possibly leak memory.
@jerhard
Add test case for memory leaking from a thead that is not joined, add…
45ec8a6 
… thread_joins to other test cases.
@jerhard
Add test case with pthread_exit called in main, remove threadid analy…
56c4d62 
…sis from params as it is not needed.
@jerhard
Add testcases for thread return and pthread_exit in thread different …
2fef812 
…from main.
@jerhard
ThreadAnalysis: Handle pthread_exit like return from thread.
645b03c
@mrstanb
Use AD.fold instead of List.fold_left
9153eb3
@jerhard @sim642
Update tests/regression/76-memleak/16-no-mem-leak-thread-exit-main.c
c6cb63e 
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
@jerhard
Remove call to free.
f12a392
@jerhard
Add annotation of nowarn next to pthread_exit.
be9171b
@jerhard
Check in TheadAnalysis.return whether the return is actually a thread…
585a65d 
…return before side-effecting.
@jerhard
Add test case that checking that analysis distinguishes between threa…
bc7694b 
…d returns and normal returns of a thread.
@michael-schwarz
MemLeak: Do not consider unions
666795f
@sim642
Add initial CHANGELOG for SV-COMP 2024
dd45d19
@sim642
Add initial CHANGELOG for v2.3.0
bf754c0
@sim642
Add CHANGELOG for v2.3.0
9c65057
@sim642
Merge branch 'master' into svcomp24-dev
af1ddef
@sim642
Merge remote-tracking branch 'mrstanb/improve-valid-memtrack-for-sing…
765a64e 
…le-threaded-programs' into svcomp24-dev
@sim642
Merge remote-tracking branch 'mrstanb/improve-multi-threaded-valid-me…
d629d14 
…mcleanup' into svcomp24-dev
@sim642
Merge branch 'master' into svcomp24-dev
e0a0692
@sim642
Merge branch 'master' into svcomp24-dev
c2e9465
@sim642 sim642 mentioned this pull request Nov 24, 2023
Merged
@sim642 sim642 marked this pull request as ready for review November 24, 2023 14:06
@sim642 sim642 merged commit cd2428a into master Nov 24, 2023
25 of 27 checks passed
@sim642 sim642 deleted the svcomp24-dev branch November 24, 2023 14:06
@sim642 sim642 removed in progress pr-dependency Depends or builds on another PR, which should be merged before labels Nov 24, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees

@sim642 sim642

Labels
sv-comp SV-COMP (analyses, results), witnesses
Projects
None yet
Milestone
SV-COMP 2024
Development

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