Non-deterministic initialisation of structs, pointers and globals in function call harness #4181

NlightNFotis · 2019-02-13T16:23:34Z

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

hannes-steffenhagen-diffblue · 2019-02-13T16:26:08Z

Basically, this PR is intended to re-implement (and ultimately replace) the changes made in #3251, except in an external tool rather than within CBMC

EDIT: The diff of the refactoring PR is kind of hopeless, mostly what's going on there is that we break up the generate function into multiple utility functions

hannes-steffenhagen-diffblue · 2019-02-13T16:32:15Z

src/goto-harness/function_call_harness_generator.cpp

+    {
+      const auto &symbol = symbol_table_entry.second;
+      if(
+        symbol.is_static_lifetime && symbol.is_lvalue &&


We think this means "global", but we weren't entirely sure. This is basically reverse engineered from a --show-symbol-table.

Looks good to me.

xbauch · 2019-02-14T10:01:18Z

src/goto-harness/recursive_initialization.h

+  /// exist already.
+  symbol_exprt get_malloc_function();
+
+  void get_struct_tag_initializer(


Why are these called get_* if they don't return?

Good point, we'll change it

xbauch · 2019-02-14T10:19:56Z

src/goto-harness/recursive_initialization.cpp

+  exprt choice;
+  if(
+    depth > initialization_config.min_null_tree_depth &&
+    depth < initialization_config.max_nondet_tree_depth)


What about wrapping these conditions in something a bit more descriptive?, e.g.: should_null_initialize(depth), where
bool should_null_initialize(size_t depth) { return depth >= initialization_config.min_null_tree_depth; }

We'll consider it, I think a function might be a bit overkill though. A local variable might be an improvement here though!

xbauch · 2019-02-14T11:27:34Z

src/goto-harness/function_call_harness_generator.cpp

+  {
+    auto const value = require_exactly_one_value(option, values);
+    p_impl->recursive_initialization_config.min_null_tree_depth =
+      std::stoul(value);


Don't we have some facility to extract numbers from string safely via std::optional?

We probably do, we'll see how we can improve these

So, I still think this would be a good idea but we can’t find it. There are the safe_ conversion functions, but those just assert that the conversion succeeds rather than returning an optionalt. Writing new converters on the other hand seems a bit out of scope for this

Well stoul is safe: throwing exceptions on failure. May want to catch those.

I'd use safe_string2size_t here, unless you actually want to throw an exception.

@tautschnig Considering this is user input I think throwing an exception here would be appropriate. I don't think asserting that user input is always correct is appropriate.

@xbauch @tautschnig I added #4192, which adds a more convenient way to convert strings to integers and handling failures locally.

That's great, indeed we should not be failing an assertion when reporting invalid user input.

xbauch · 2019-02-14T11:39:08Z

src/goto-harness/function_call_harness_generator.cpp

+  recursive_initialization->initialize(lhs, 0, block);
+}
+
+void function_call_harness_generatort::validate_options()


Is this one called anywhere?

This is called by the harness generator factory

xbauch · 2019-02-14T11:41:45Z

src/goto-harness/function_call_harness_generator.cpp

+void function_call_harness_generatort::implt::
+  add_harness_function_to_goto_model(code_blockt function_body)
+{
+  const auto &function_to_call = symbol_table->lookup_ref(function);


Why not use lookup_function_to_call?

xbauch

Looks good.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: cac8026).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100932721
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 365a914).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100935342

tautschnig

Can we actually get rid of goto-instrument/nondet_static.cpp with this code? I think that code might be a bit cleaner when it comes to choosing what (not) to initialise, but isn't very useful when it comes to objects with pointers and such.

tautschnig · 2019-02-14T15:54:09Z

src/goto-harness/function_call_harness_generator.cpp

+    {
+      const auto &symbol = symbol_table_entry.second;
+      if(
+        symbol.is_static_lifetime && symbol.is_lvalue &&


Looks good to me.

chrisr-diffblue

LGTM, though you may want to check Michael's comment about using safe_string2size_t

danpoe · 2019-02-15T12:21:46Z

src/goto-harness/recursive_initialization.cpp

+    allocate_objects.allocate_automatic_local_object(type.subtype(), "pointee");
+  allocate_objects.declare_created_symbols(body);
+  body.add(code_assignt{lhs, null_pointer_exprt{type}});
+  if(depth < initialization_config.max_nondet_tree_depth)


This changes the behavior compared to the existing c_nondet_symbol_factory(). Previously we would only stop initializing when a recursion on a struct was reached (i.e., on a pointer chain the same struct appeared a second time) and the depth was greater or equal to max_nondet_tree_depth. This was done via recording the struct tags in the object recursion_set. All pointer dereferences would increase the depth but only when we see a recursion we would stop initializing. Would it be possible to replicate this behavior here? The intention was to be consistent with how the initialization is done in the Java object factory (to facilitate future refactorings and code sharing between the two).

Ah right, I figured there was something we forgot! Good point, we will implement this.

danpoe · 2019-02-15T12:26:23Z

src/goto-harness/function_call_harness_generator.cpp


-  code_function_callt::operandst arguments{};
-  arguments.reserve(parameters.size());
+void function_call_harness_generatort::implt::generate_nondet_globals(


There's also --nondet-static (using nondet_static()) in cbmc and goto-instrument. I'm not sure how exactly it compares to this functionality but maybe the two could be merged at some point.

Important refactoring to make implementation of later features easier. Co-authored-by: Fotis Koutoulakis <[email protected]> Co-authored-by: Hannes Steffenhagen <[email protected]>

Add ability to non-deterministically initialise globals in the function call harness generator. Co-authored-by: Fotis Koutoulakis <[email protected]> Co-authored-by: Hannes Steffenhagen <[email protected]>

Recursively initialise non-deterministically struct components and pointers. Co-authored-by: Fotis Koutoulakis <[email protected]> Co-authored-by: Hannes Steffenhagen <[email protected]>

Now the depth limit only applies to structs if we have seen this struct before (i.e. the initialisation chain is recursive)

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 550e6ab).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/101132607

NlightNFotis self-assigned this Feb 13, 2019

NlightNFotis requested a review from hannes-steffenhagen-diffblue February 13, 2019 16:23

NlightNFotis requested review from chrisr-diffblue, danpoe, martin-cs and peterschrammel as code owners February 13, 2019 16:23

hannes-steffenhagen-diffblue reviewed Feb 13, 2019

View reviewed changes

NlightNFotis force-pushed the non-det-struct-new branch 2 times, most recently from 0159b21 to 7eff3f5 Compare February 13, 2019 17:00

xbauch reviewed Feb 14, 2019

View reviewed changes

xbauch approved these changes Feb 14, 2019

View reviewed changes

NlightNFotis force-pushed the non-det-struct-new branch 2 times, most recently from cac8026 to 365a914 Compare February 14, 2019 12:05

allredj reviewed Feb 14, 2019

View reviewed changes

hannes-steffenhagen-diffblue assigned hannes-steffenhagen-diffblue and NlightNFotis and unassigned NlightNFotis Feb 14, 2019

tautschnig approved these changes Feb 14, 2019

View reviewed changes

chrisr-diffblue approved these changes Feb 14, 2019

View reviewed changes

danpoe reviewed Feb 15, 2019

View reviewed changes

NlightNFotis and others added 4 commits February 15, 2019 14:36

Refactor function call harness generator

94636b4

Important refactoring to make implementation of later features easier. Co-authored-by: Fotis Koutoulakis <[email protected]> Co-authored-by: Hannes Steffenhagen <[email protected]>

Add option to non-det globals to goto-harness

d343daa

Add ability to non-deterministically initialise globals in the function call harness generator. Co-authored-by: Fotis Koutoulakis <[email protected]> Co-authored-by: Hannes Steffenhagen <[email protected]>

Add recursive initialisation of structs

5ce492c

Recursively initialise non-deterministically struct components and pointers. Co-authored-by: Fotis Koutoulakis <[email protected]> Co-authored-by: Hannes Steffenhagen <[email protected]>

Only apply tree limit to recursive struct

550e6ab

Now the depth limit only applies to structs if we have seen this struct before (i.e. the initialisation chain is recursive)

NlightNFotis force-pushed the non-det-struct-new branch from 365a914 to 550e6ab Compare February 15, 2019 16:09

allredj reviewed Feb 15, 2019

View reviewed changes

NlightNFotis merged commit 79ea945 into diffblue:develop Feb 18, 2019

NlightNFotis deleted the non-det-struct-new branch February 18, 2019 10:46

Non-deterministic initialisation of structs, pointers and globals in function call harness #4181

Non-deterministic initialisation of structs, pointers and globals in function call harness #4181

Uh oh!

Conversation

NlightNFotis commented Feb 13, 2019

Uh oh!

hannes-steffenhagen-diffblue commented Feb 13, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue Feb 14, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

xbauch left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

chrisr-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

hannes-steffenhagen-diffblue commented Feb 13, 2019 •

edited

Loading

hannes-steffenhagen-diffblue Feb 14, 2019 •

edited

Loading