Skip to content

Patch set for SV-COMP'19 [depends-on: #2000, #3462] #3486

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
Closed
wants to merge 33 commits into from
Closed

Patch set for SV-COMP'19 [depends-on: #2000, #3462] #3486

wants to merge 33 commits into from

Conversation

tautschnig
Copy link
Collaborator

@tautschnig tautschnig commented Dec 1, 2018 •
edited
Loading

This is just to provide a to-do list of PRs to be created or existing PRs to be merged to put in place the fixes applied for CBMC's SV-COMP'19 submission. No review needed or expected.

tautschnig and others added 30 commits November 28, 2018 09:15
@tautschnig
expr2ct hack for SV-COMP: no struct type body output
1f0e11f 
A proper fix would be done via #354
@tautschnig
Use clean-C configuration for graphml counterexample
84d6008
@tautschnig
Do not output "NULL"
98463e1
@peterschrammel @tautschnig
No outgoing edges from violation nodes
a171575
@marek-trtik @tautschnig
Using cache to speed up generation of grapml file.
65da097
@peterschrammel @tautschnig
Hack to make CPAchecker parse graphml concurrency witnesses
52e25c7
@peterschrammel @tautschnig
Make sure SSA suffixes are stripped off graphml output
9782c4b
@peterschrammel @tautschnig
Remove obsolete graphml frontierNode, nodeType and add new cyclehead
b527893
@peterschrammel @tautschnig
Remove obsolete sourcecode element in graphml
587b5c7
@peterschrammel @tautschnig
Split array-list into assignments and hide dynamic objects
a4ceecc
@peterschrammel @tautschnig
Remove obsolete sourcecode element from graphml
bb159ae
@marek-trtik @tautschnig
graphml: More precise detection of when to use '\result' variable.
154bdad
@marek-trtik @tautschnig
graphml: Special (hacky) structure of concurrency witness.
c38b2dd
@tautschnig
Update expected graphml output, to be merged
c3022b0
@lucasccordeiro @tautschnig
Add violation node for the memory safety benchmarks
6803218
@tautschnig
Ensure that local declarations do not introduce spurious dead warnings
d1bf5ea
@tautschnig
invalid_object(pointer) is true for all non-existent objects
479dd14 
Check whether the object part of a pointer is greater or equal the total
number of objects, or equals a dynamic object that has not actually been
allocated on a given trace.
@tautschnig
fixup! Do not output "NULL"
52de440
@tautschnig
Add a definition of alloca
a80f756 
Benchmarks not including headers files fail as we only provided a definition of
__builtin_alloca, which alloca expands to in standard libary headers, but none
for alloca directly.
@tautschnig
Do not perform SSA sanity checks
53352cd 
Iterating over all expression tress has considerable performance cost,
seemingly accounting for up to 10% of runtime (on SV-COMP benchmarks,
with profiling enabled).
@tautschnig
irept: Use singly-linked lists with SUB_IS_LIST
04f9c35 
This reduces the memory footprint by two pointers for both named_sub and
comments. The cost is that computing the size of lists and add/remove require
additional iterator increments.
@tautschnig
Avoid repeated hash computation, reduce irept::dt size
28255e4 
On SV-COMP benchmarks, hashing accounts for >22% of CPU time (with
profiling enabled).
@tautschnig
C library: model pthread_key_create, pthread_{get,set}specific
7d439f4 
This is used by pthread-divine/tls_basic_true-unreach-call in SV-COMP.
@peterschrammel @tautschnig
Factor out memory leak instrumentation into separate function
53e4f60
@peterschrammel @tautschnig
Add memory leak instrumentation to abort and exit
1672dbc
@peterschrammel @tautschnig
Fix memory leak check for __VERIFIER_error
7e3b18a
@tautschnig
Needs more profiling: Do not sort operands as part of simplification
4d6d81f
@tautschnig
Detect use of free() with alloca-allocated objects
ca9673f 
As we internally use dynamic allocation, we previously did not distinguish
alloca-allocated from malloc/calloc-allocated ones.
@tautschnig
pthread_cond_wait may return spuriously
bc2c2be
@tautschnig
Don't implement pthread_keyt destructors
443dfdb 
They are too expensive due to extensive shared-variable use.
@tautschnig
Non-deterministic initialisation of argc/argv/envp
f2139d3
@tautschnig
clang-format cleanup
95f1859
@tautschnig
Skip phi assignment if one of the merged states has an uninitialised …
ce20fbe 
…object

With level-2 counters incremented on declaration and non-deterministic
initialisation upon allocation, the only remaining sources are pointer
dereferencing, where uninitialised objects necessarily refer to invalid objects.

This is a cleaner implementation of 369f077. Removing only the code
introduced in 369f077 would yield a wrong result for
regression/cbmc/Local_out_of_scope3.
@tautschnig tautschnig self-assigned this Dec 17, 2018
tautschnig added a commit that referenced this pull request Dec 19, 2018
@tautschnig
Merge pull request #2220 from tautschnig/phi-cleanup
a94389d 
Skip phi assignment if one of the merged states has an uninitialised object [blocks: #35, #2574, #3486]
@owen-mc-diffblue
Copy link
Contributor

@tautschnig #2220 has been merged, so you can tick it off

@tautschnig tautschnig changed the title Patch set for SV-COMP'19 Patch set for SV-COMP'19 [depends-on: #1992, #1996, #1997, #2000, #2001, #3462, #4269..#4272] Feb 25, 2019
@tautschnig tautschnig changed the title Patch set for SV-COMP'19 [depends-on: #1992, #1996, #1997, #2000, #2001, #3462, #4269..#4272] Patch set for SV-COMP'19 [depends-on: #1992, #1996, #1997, #2000, #2001, #3462, #4272] Feb 28, 2019
@tautschnig tautschnig mentioned this pull request Mar 22, 2019
Closed
@tautschnig tautschnig changed the title Patch set for SV-COMP'19 [depends-on: #1992, #1996, #1997, #2000, #2001, #3462, #4272] Patch set for SV-COMP'19 [depends-on: #1992, #1996, #1997, #2000, #2001, #3462, #4272, #4458] Mar 29, 2019
tautschnig added a commit that referenced this pull request May 8, 2019
@tautschnig
Merge pull request #1992 from tautschnig/irep-speedup
fd79fe0 
Enable HASH_CODE by default to avoid repeated hash computation [blocks: #3486]
@tautschnig tautschnig changed the title Patch set for SV-COMP'19 [depends-on: #1992, #1996, #1997, #2000, #2001, #3462, #4272, #4458] Patch set for SV-COMP'19 [depends-on: #1997, #2000, #3462, #4458] May 16, 2019
tautschnig added a commit that referenced this pull request May 28, 2019
@tautschnig
Merge pull request #4458 from tautschnig/forward-list
c4ffbee 
Use std::forward_list instead of std::map in irept by default [blocks: #3486]
@tautschnig tautschnig changed the title Patch set for SV-COMP'19 [depends-on: #1997, #2000, #3462, #4458] Patch set for SV-COMP'19 [depends-on: #1997, #2000, #3462] May 28, 2019
tautschnig added a commit that referenced this pull request Jan 28, 2021
@tautschnig
Merge pull request #1997 from tautschnig/no-sort-operands
cf40d22 
Do not sort operands as part of simplification [blocks: #3486]
@tautschnig tautschnig changed the title Patch set for SV-COMP'19 [depends-on: #1997, #2000, #3462] Patch set for SV-COMP'19 [depends-on: #2000, #3462] Jan 28, 2021
@tautschnig
Copy link
Collaborator Author

Closing as the remaining patches of PRs of their own.

@tautschnig tautschnig closed this May 1, 2021
tautschnig added a commit that referenced this pull request May 19, 2021
@tautschnig
Merge pull request #1998 from tautschnig/no-sort-guards
60abd1e 
Do not unnecessarily sort guard conjuncts [blocks: #3486]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@chrisr-diffblue chrisr-diffblue Awaiting requested review from chrisr-diffblue

@kroening kroening Awaiting requested review from kroening kroening is a code owner

@martin-cs martin-cs Awaiting requested review from martin-cs martin-cs is a code owner

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

@pkesseli pkesseli Awaiting requested review from pkesseli

@smowton smowton Awaiting requested review from smowton

@thk123 thk123 Awaiting requested review from thk123

Assignees

@tautschnig tautschnig

Labels
dependent - do not merge do not review
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@tautschnig @owen-mc-diffblue @peterschrammel @marek-trtik @lucasccordeiro