Make global string_container more resilient to different static init orders #1213

reuk · 2017-08-07T10:15:17Z

At the moment, if we initialise a static object which depends on the global string_container, there's no guarantee which object will be initialised first, which means the string_container may be uninitialised when first used. This problem was spotted by @jasigal recently.

This PR wraps the global object in a function which ensures it is initialised before it is first used.

clang -Wall says: Struct_Initialization1/main.c:16:38: warning: suggest braces around initialization of subobject [-Wmissing-braces] struct _classinfo nullclass1 = { 42, 1, 2, 3, 4 }; ^~~~ { } and then constructs a suitable object. Our implementation now attempts to build an initializer list if a variable-length array is encountered; if this succeeds, the same suitable object is constructed. Variable-length arrays in the middle of a struct are not permitted (neither by GCC nor Clang or our C front-end).

Previously the code would rely on type sizes being constant when building a subtraction; this is unnecessary as the expression is sent to the solver for evaluation anyway.

fgets may (and certainly does when successful) change the contents of the buffer passed in. Building a regression test showed further deficiences in the stdio library model: 1) MacOS uses _fdopen; 2) fclose uses free from stdlib.h.

Licensing: I had contributed these myself to the SV-COMP benchmarks.

Array initialization with a non-array is expected to fail

…apply miniBDD: added a non-recursive variant of APPLY

vectors don't need to be handled, they have been removed via remove_vector.

Unlike CBMC, all output is enabled in debug mode only.

All symex limits use value -1 as marking "not set". Use size_t for counting statistics.

The solver back end cannot necessarily handle unbounded integers. Do not use them unless explicitly requested/supported.

fix for operator< on reverse_keyt in miniBDD, fixing segfault in ebmc

Symex improvements

C library modelling: fgets, getopt, vasprintf

Avoid using integer_typet where unsuitable

Follow-up to 260e03d: instead of using negative numbers to represent "limit not set", use the maximum value as default.

Avoid spurious signed/unsigned comparison warnings

Support out-of-bounds checks on arrays of dynamic size

Enable extractbits over arbitrary types, fix byte extract omission

Stop using C headers

tautschnig · 2017-08-07T10:25:33Z

src/util/string_container.cpp

+/// Get a reference to the global string container.
+string_containert &get_string_container()
+{
+  static string_containert ret{};


Why are those {} required?

They're not, but they make it clear that default-initialisation is intentional.

Could be done if done consistently across the code base. Else please remove them for we don't (yet) do it elsewhere.

tautschnig · 2017-08-07T10:26:56Z

What is the performance difference?

reuk · 2017-08-07T10:37:00Z

I'm not sure how to measure the performance difference. This PR shouldn't affect performance at all, because it only changes the order in which static objects are initialised. The total number of static initialisations is unchanged.

tautschnig · 2017-08-07T10:40:51Z

I'm not sure how to measure the performance difference.

I believe this is a problem that needs to be addressed before this PR can be merged.

This PR shouldn't affect performance at all, because it only changes the order in which static objects are initialised.

How about the non-inlined function calls that will now be necessary each time dstringt or as_string is invoked?

smowton · 2017-08-07T11:12:48Z

Possible alternative: instead of a static irep_idt (if that's what was causing this to begin with), I've been using a static function local, which gets initialised on first call instead of during library init. For example,

const irep_idt &get_some_id() {
  static const irep_idt some_id("some_id");
  return some_id;
}

The cost should be minimal for most sensible implementations per http://en.cppreference.com/w/cpp/language/storage_duration#Static_local_variables

LAJW · 2017-08-07T11:13:07Z

Apart from the cost of function call there's going to be a performance hit similar to reading atomic ("magic static" - C++11 static variable initialisation is thread safe, so likely implemented using atomics). It's not implemented in VC2013 which we're supporting. If irep reference counting is not thread safe either, then that is a problem that can be safely ignored. (VC Support)

Moving get_string_declaration to header file and adding inline might alleviate @tautschnig's concern.

reuk · 2017-08-07T11:15:34Z

If we explicitly inline the function, wouldn't we end up with one copy of the static local variable for each translation unit?

LAJW · 2017-08-07T11:18:09Z

@reuk Apparently not.

A static local variable in an extern inline function always refers to the same object.
7.1.2/4 - C++98/C++14 (n3797)

reuk · 2017-08-07T11:24:03Z

Some of the answers on StackOverflow say you may still end up with one instance per TU but the linker will pick a specific one to be the "canonical" instance, although I guess this may be implementation-dependent and may depend on LTO... I haven't been able to find hard evidence one way or the other.

jasigal

Approving on the basis that my original problem is fixed, but I don't know enough to weigh in on the other topics. Obviously a senior developer needs to approve this anyways.

tautschnig · 2017-08-07T12:11:55Z

Don't get me wrong: I'm all for getting rid of the undefinedness that initialisation of static global objects induces; but this must not be merged until a performance evaluation is performed.

reuk · 2017-08-07T13:15:55Z

@tautschnig How would you propose to benchmark this PR?

tautschnig · 2017-08-07T13:20:11Z

This PR should not be benchmarked differently from any other PR, even though it is slightly easier here. Doing a summary profile across the regression tests might suffice for this PR if specific attention is paid to where in the profile the affected functions (dstringt and dstringt::as_string) show up.

Proper benchmarking would entail analysis of the effect on overall performance across a large set of benchmark inputs.

reuk · 2017-08-07T13:43:16Z

The following are times to run make from the regression directory.

With patch:

make  177.83s user 11.76s system 92% cpu 3:25.03 total

Master:

make  177.36s user 11.84s system 93% cpu 3:21.84 total

tautschnig · 2017-08-07T13:49:34Z

That experiment won't provide more than the most basic sanity check. The bare minimum is actual profiling so that you can get information on what fraction of the total time is spent on the mentioned functions.

martin-cs · 2017-08-09T15:17:43Z

If it would help, I should be int he office tomorrow and have done quite a bit of profiling of CBMC and we could chat about it.

Also at one point @Degiorgio had an interest in this code...

reuk · 2017-08-22T14:30:28Z

Closing as duplicate of #1218 seeing as both are targeting develop now.

tautschnig and others added 30 commits July 19, 2017 10:19

added a non-recursive variant of APPLY

564f64c

disable linter for assertions

a71ca41

Support out-of-bounds checks on arrays of dynamic size

d078dd8

Previously the code would rely on type sizes being constant when building a subtraction; this is unnecessary as the expression is sent to the solver for evaluation anyway.

More complete modelling of fgets

6eef691

fgets may (and certainly does when successful) change the contents of the buffer passed in. Building a regression test showed further deficiences in the stdio library model: 1) MacOS uses _fdopen; 2) fclose uses free from stdlib.h.

Import getopt{,_long} and vasprintf models from SV-COMP/busybox

f691135

Licensing: I had contributed these myself to the SV-COMP benchmarks.

Merge pull request diffblue#131 from tautschnig/struct-init-error

151efbc

Array initialization with a non-array is expected to fail

increased version number in preparation for release 5.8

eb96b70

Merge pull request diffblue#1144 from diffblue/miniBDD-non-recursive-…

8e70eaa

…apply miniBDD: added a non-recursive variant of APPLY

fix for operator< on reverse_keyt in miniBDD, fixing segfault in ebmc

439ef97

invariant_violated does not return

393256f

test for miniBDD

ff945b3

Symex support for lhs-typecasts and side effects

879a47b

Extract elements of array, struct directly instead of simplifying

08f1a9e

vectors don't need to be handled, they have been removed via remove_vector.

Removed redundant get_pc() (there is pc())

f281f88

Fix symex thread statistics

52db9e4

Extended symex progres statistics

c69a21b

Symex: output instruction processing and loop unwinding like CBMC

acdc797

Unlike CBMC, all output is enabled in debug mode only.

symex --max-search-time limit and cleanup

260e03d

All symex limits use value -1 as marking "not set". Use size_t for counting statistics.

Perform function-pointer removal in symex

73adfb0

Avoid using integer_typet where unsuitable

e2ed0df

The solver back end cannot necessarily handle unbounded integers. Do not use them unless explicitly requested/supported.

Merge pull request diffblue#1062 from diffblue/fix_for_miniBDD

0cad6f4

fix for operator< on reverse_keyt in miniBDD, fixing segfault in ebmc

Merge pull request diffblue#151 from tautschnig/symex-improvements

ea476f7

Symex improvements

Merge pull request diffblue#1167 from tautschnig/c-library-ext

df81a9c

C library modelling: fgets, getopt, vasprintf

Merge pull request diffblue#1035 from tautschnig/no_integer_typet

bb9cef3

Avoid using integer_typet where unsuitable

Avoid spurious signed/unsigned comparison warnings

a3578c0

Follow-up to 260e03d: instead of using negative numbers to represent "limit not set", use the maximum value as default.

Merge pull request diffblue#1205 from tautschnig/sign-compare-fix

652ea09

Avoid spurious signed/unsigned comparison warnings

Merge pull request diffblue#1158 from tautschnig/array-bounds

76ae912

Support out-of-bounds checks on arrays of dynamic size

fix vacuous conjuncts

de40333

Stop using C headers

548aeba

Daniel Kroening added 2 commits August 4, 2017 22:29

Merge pull request diffblue#1211 from tautschnig/fix-1209

9d3a99e

Enable extractbits over arbitrary types, fix byte extract omission

Merge pull request diffblue#1210 from reuk/stop-using-c-headers

4dd5405

Stop using C headers

reuk force-pushed the reuk/static-string-container branch from fe41573 to ee8ea7d Compare August 7, 2017 10:16

tautschnig reviewed Aug 7, 2017

View reviewed changes

Make string_container static init more resilient

8314aab

reuk force-pushed the reuk/static-string-container branch from ee8ea7d to e6dcaa7 Compare August 7, 2017 10:37

Fix up uses of string_container

eb89bc0

reuk force-pushed the reuk/static-string-container branch from e6dcaa7 to eb89bc0 Compare August 7, 2017 11:06

Fix circular initialisation

39b8cc6

jasigal approved these changes Aug 7, 2017

View reviewed changes

jasigal mentioned this pull request Aug 8, 2017

Unit tests for solvers/refinement/string_constraint_instantiation.cpp:instantiate_not_contains #1215

Merged

reuk mentioned this pull request Aug 8, 2017

Make string_container static init more resilient #1218

Merged

tautschnig changed the base branch from master to develop August 22, 2017 12:16

reuk closed this Aug 22, 2017

reuk deleted the reuk/static-string-container branch September 14, 2017 17:05

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Make global string_container more resilient to different static init orders #1213

Make global string_container more resilient to different static init orders #1213

reuk commented Aug 7, 2017

tautschnig Aug 7, 2017

reuk Aug 7, 2017

tautschnig Aug 7, 2017

tautschnig commented Aug 7, 2017

reuk commented Aug 7, 2017

tautschnig commented Aug 7, 2017

smowton commented Aug 7, 2017

LAJW commented Aug 7, 2017 •

edited

Loading

reuk commented Aug 7, 2017

LAJW commented Aug 7, 2017

reuk commented Aug 7, 2017 •

edited

Loading

jasigal left a comment

tautschnig commented Aug 7, 2017

reuk commented Aug 7, 2017

tautschnig commented Aug 7, 2017

reuk commented Aug 7, 2017

tautschnig commented Aug 7, 2017

martin-cs commented Aug 9, 2017

reuk commented Aug 22, 2017

Make global string_container more resilient to different static init orders #1213

Make global string_container more resilient to different static init orders #1213

Conversation

reuk commented Aug 7, 2017

tautschnig Aug 7, 2017

Choose a reason for hiding this comment

reuk Aug 7, 2017

Choose a reason for hiding this comment

tautschnig Aug 7, 2017

Choose a reason for hiding this comment

tautschnig commented Aug 7, 2017

reuk commented Aug 7, 2017

tautschnig commented Aug 7, 2017

smowton commented Aug 7, 2017

LAJW commented Aug 7, 2017 • edited Loading

reuk commented Aug 7, 2017

LAJW commented Aug 7, 2017

reuk commented Aug 7, 2017 • edited Loading

jasigal left a comment

Choose a reason for hiding this comment

tautschnig commented Aug 7, 2017

reuk commented Aug 7, 2017

tautschnig commented Aug 7, 2017

reuk commented Aug 7, 2017

tautschnig commented Aug 7, 2017

martin-cs commented Aug 9, 2017

reuk commented Aug 22, 2017

LAJW commented Aug 7, 2017 •

edited

Loading

reuk commented Aug 7, 2017 •

edited

Loading