Skip to content

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

Closed
tautschnig wants to merge 33 commits into
developfrom
sv-comp19
Closed

Patch set for SV-COMP'19 [depends-on: #2000, #3462]#3486
tautschnig wants to merge 33 commits into
developfrom
sv-comp19

Conversation

@tautschnig

@tautschnigtautschnig commented Dec 1, 2018•
edited
Loading

Copy link
Copy Markdown
Collaborator

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.

tautschnigand 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.
@tautschnigtautschnig self-assigned this Dec 17, 2018
tautschnig added a commit that referenced this pull request Dec 19, 2018
@tautschnig
Merge pull request#2220from tautschnig/phi-cleanup
a94389d
Skip phi assignment if one of the merged states has an uninitialised object [blocks: #35, #2574, #3486]
@owen-mc-diffblue

owen-mc-diffblue commented Jan 7, 2019

Copy link
Copy Markdown
Contributor

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

@tautschnigtautschnig changed the title Patch set for SV-COMP'19Patch set for SV-COMP'19 [depends-on: #1992, #1996, #1997, #2000, #2001, #3462, #4269..#4272]Feb 25, 2019
@tautschnigtautschnig 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
@tautschnigtautschnig mentioned this pull request Mar 22, 2019
Closed
@tautschnigtautschnig 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#1992from tautschnig/irep-speedup
fd79fe0
Enable HASH_CODE by default to avoid repeated hash computation [blocks: #3486]
@tautschnigtautschnig 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#4458from tautschnig/forward-list
c4ffbee
Use std::forward_list instead of std::map in irept by default [blocks: #3486]
@tautschnigtautschnig 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#1997from tautschnig/no-sort-operands
cf40d22
Do not sort operands as part of simplification [blocks: #3486]
@tautschnigtautschnig 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

tautschnig commented May 1, 2021

Copy link
Copy Markdown
CollaboratorAuthor

Closing as the remaining patches of PRs of their own.

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

Reviewers

@chrisr-diffbluechrisr-diffblueAwaiting requested review from chrisr-diffblue
@kroeningkroeningAwaiting requested review from kroeningkroening is a code owner
@martin-csmartin-csAwaiting requested review from martin-csmartin-cs is a code owner
@peterschrammelpeterschrammelAwaiting requested review from peterschrammelpeterschrammel is a code owner
@pkesselipkesseliAwaiting requested review from pkesseli
@smowtonsmowtonAwaiting requested review from smowton
@thk123thk123Awaiting requested review from thk123

Assignees

@tautschnigtautschnig

Labels

dependent - do not mergedo 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