Recursive nondet init of pointers to structs [blocks: #3443] #3251

danpoe · 2018-10-31T14:08:17Z

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.
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).
n/a 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.

peterschrammel · 2018-11-01T04:03:07Z

jbmc/src/java_bytecode/java_object_factory_parameters.h

+
+#include <util/object_factory_parameters.h>
+
+struct java_object_factory_parameterst final : public object_factory_parameterst


Why this if they are the same?

This would be a place to add options in the future that are not common to both the C and Java object factory. For C at least we expect some special options (e.g., to indicate which length function argument corresponds to which array function arguments).

peterschrammel · 2018-11-01T04:08:15Z

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -51,6 +30,13 @@ class symbol_factoryt
  const bool assume_non_null;
  namespacet ns;

+  const symbolt &c_new_tmp_symbol(


Why can't this use util/fresh_symbol?

Yes, this should probably be replaced by a call to get_fresh_aux_symbol() since it's called in one place only.

src/cbmc/cbmc_parse_options.cpp

jbmc/src/java_bytecode/java_object_factory_parameters.h

hannes-steffenhagen-diffblue

Can't see anything wrong with this, but I'll need some more time to look over this before I can approve

hannes-steffenhagen-diffblue · 2018-11-01T13:36:57Z

jbmc/src/java_bytecode/java_object_factory_parameters.cpp

+
+\*******************************************************************/
+
+#include "java_object_factory_parameters.h"


Why is this in a commit called "move object factory parameters to util"?

Ok, renamed the commit to "Move object factory parameters to util and add java object factory parameters" (plus a body with some more details).

hannes-steffenhagen-diffblue · 2018-11-01T13:41:06Z

src/cbmc/cbmc_parse_options.cpp

@@ -922,6 +923,8 @@ void cbmc_parse_optionst::help()
    " --round-to-plus-inf          rounding towards plus infinity\n"
    " --round-to-minus-inf         rounding towards minus infinity\n"
    " --round-to-zero              rounding towards zero\n"
+    " --max-nondet-tree-depth N    limit size of nondet (e.g. input) object tree;\n" /* NOLINT(*) */ \


We should have some more detailed description of how this behaves in our docs

I've updated the documentation in object_factory_parameters.h for the max_nondet_tree_depth parameter.

That helps, but it's not user visible, and even for us it's going to take some digging to find out that this parameter does end up there if we ever need to find out

(This is a reply to one of @danpoe 's other comments, but doesn't show up as such in github. Thanks github).

Definitely agree that this could do with some user documentation and not just source code documentation.

src/langapi/language_file.cpp

hannes-steffenhagen-diffblue · 2018-11-01T13:48:39Z

regression/cbmc/pointer-function-parameters-3/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>


Could the tests get better names than "pointer-function-parameters-{3,4,5,6}"?

Ok, renamed.

xbauch · 2018-11-02T11:10:43Z

src/ansi-c/c_nondet_symbol_factory.cpp

+
+      if(
+        recursion_set.find(struct_tag) != recursion_set.end() &&
+        depth >= object_factory_params.max_nondet_tree_depth)


So the depth is the minimal length of dereference-chain before null-pointer initialisation? And every chain longer than depth will have pointers initialised to null but only when they point to a struct that appeared somewhere before on this chain?

Yes, max_nondet_tree_depth gives the depth of a chain such that a pointer to a struct will be initialised to null if the depth of the chain exceeds it and the struct appeared already before somewhere on the chain. If there is no recursion the chains can have any depth.

I see. So it may turn out to be non-terminating but it would have nothing to do with this new code. I was just thinking if there is a more accurate way to describe the input option.

I think if there's no recursion then the chains would always have finite length thus it can never be non-terminating. The current behaviour is similar to that of the java object factory.

danpoe · 2018-11-23T12:09:48Z

@tautschnig @peterschrammel @thk123 This still requires code owner approval if you get a chance.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 9049aff).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/92377593
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.

peterschrammel

This is ready to go. @allredj confirmed that there is a passing bump.

allredj · 2018-11-23T17:28:29Z

(bump is here: https://github.com/diffblue/test-gen/pull/2444)

tautschnig

Some smaller requests remain, otherwise looks good. In future, I would really appreciate if such PRs could 1) be broken into several smaller PRs to make sure reviewing is also possible other than on weekends (where longer consecutive stretches of time may be available) and 2) each commit message has a body.

tautschnig · 2018-11-24T14:57:00Z

src/util/object_factory_parameters.h

+    set(options);
+  }
+
+  virtual ~object_factory_parameterst()


= default;

tautschnig · 2018-11-24T15:03:59Z

src/util/nondet_bool.h

-inline exprt get_nondet_bool(const typet &type)
+inline exprt get_nondet_bool(
+  const typet &type,
+  const source_locationt &source_location = source_locationt())


Let's not make this optional: there is a single call site (and the next commit adds a second one), which could trivially pass in a proper source location.

tautschnig · 2018-11-24T15:07:25Z

src/cbmc/cbmc_parse_options.cpp

@@ -933,6 +934,10 @@ void cbmc_parse_optionst::help()
    " --round-to-plus-inf          rounding towards plus infinity\n"
    " --round-to-minus-inf         rounding towards minus infinity\n"
    " --round-to-zero              rounding towards zero\n"
+    " --max-nondet-tree-depth N    limit size of nondet (e.g. input) object tree;\n" /* NOLINT(*) */ \
+    "                              at level N pointers are set to null\n" /* NOLINT(*) */ \
+    " --min-null-tree-depth N      minimum level at which a pointer can first be\n" /* NOLINT(*) */ \


This option is not added in the header file.

tautschnig · 2018-11-24T15:07:46Z

src/cbmc/cbmc_parse_options.h

@@ -75,6 +77,7 @@ class optionst;
  "(localize-faults)(localize-faults-method):" \
  OPT_GOTO_TRACE \
  OPT_VALIDATE \
+  "(max-nondet-tree-depth):" \


Use OPT... instead of the raw string in here.

tautschnig · 2018-11-24T15:08:06Z

src/cbmc/cbmc_parse_options.cpp

@@ -933,6 +934,10 @@ void cbmc_parse_optionst::help()
    " --round-to-plus-inf          rounding towards plus infinity\n"
    " --round-to-minus-inf         rounding towards minus infinity\n"
    " --round-to-zero              rounding towards zero\n"
+    " --max-nondet-tree-depth N    limit size of nondet (e.g. input) object tree;\n" /* NOLINT(*) */ \


Define a HELP_... macro.

tautschnig · 2018-11-24T15:10:08Z

src/langapi/language.h

@@ -70,8 +70,7 @@ class languaget:public messaget
  /// complete. Functions introduced here are visible to lazy loading and
  /// can influence its decisions (e.g. picking the types of input parameters
  /// and globals), whereas anything introduced during `final` cannot.
-  virtual bool generate_support_functions(
-    symbol_tablet &symbol_table)=0;
+  virtual bool generate_support_functions(symbol_tablet &symbol_table) = 0;


Whitespace change only?

tautschnig · 2018-11-24T15:10:28Z

src/ansi-c/ansi_c_language.h


 class ansi_c_languaget:public languaget
 {
 public:
+  void set_language_options(const optionst &options) override


Added but never invoked?

This would e.g. be called by initialize_goto_model() where languaget & might reference ansi_c_languaget.

tautschnig · 2018-11-24T15:12:43Z

jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp

@@ -46,7 +46,7 @@ SCENARIO(
    symbol_typet java_string_type("java::java.lang.String");
    symbol_exprt expr("arg", java_string_type);

-    object_factory_parameterst object_factory_parameters;
+    java_object_factory_parameterst object_factory_parameters;


Should be merged into the earlier commit introducing java_object_factory_parameterst.

tautschnig · 2018-11-24T15:13:14Z

scripts/delete_failing_smt2_solver_tests

+rm pointer-function-parameters-struct-non-recursive/test.desc
+rm pointer-function-parameters-struct-simple-recursion/test.desc
+rm pointer-function-parameters-struct-simple-recursion-2/test.desc
+rm pointer-function-parameters-struct-simple-recursion-3/test.desc


Please merge into the commit introducing them.

tautschnig · 2018-11-24T15:14:11Z

regression/cbmc/pointer-function-parameters-struct-non-recursive/test.desc

+CORE
+main.c
+--function func --min-null-tree-depth 10
+^SIGNAL=0$


Add ^EXIT=10$

…rameters This moves object_factory_parameterst to util, and creates a new class derived from it called java_object_factory_parameterst in java_bytecode. This is to separate out common object factory options in preparation of adding c object factory parameters.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 0b605ea).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/92589920
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.

danpoe added the do not merge label Oct 31, 2018

danpoe requested review from cesaro, chrisr-diffblue, cristina-david, kroening, NathanJPhillips, peterschrammel, pkesseli, smowton, tautschnig and thk123 as code owners October 31, 2018 14:08

danpoe force-pushed the feature/nondet-init-structs branch 9 times, most recently from 60395ea to 2b31997 Compare October 31, 2018 17:55

peterschrammel reviewed Nov 1, 2018

View reviewed changes

hannes-steffenhagen-diffblue reviewed Nov 1, 2018

View reviewed changes

danpoe force-pushed the feature/nondet-init-structs branch 5 times, most recently from 114a027 to 102199d Compare November 2, 2018 11:06

xbauch reviewed Nov 2, 2018

View reviewed changes

danpoe force-pushed the feature/nondet-init-structs branch 2 times, most recently from 3244d70 to 199bfd9 Compare November 2, 2018 11:54

allredj reviewed Nov 23, 2018

View reviewed changes

peterschrammel approved these changes Nov 23, 2018

View reviewed changes

peterschrammel assigned kroening and tautschnig Nov 23, 2018

peterschrammel added the blocker label Nov 23, 2018

tautschnig changed the title ~~Recursive nondet init of pointers to structs~~ Recursive nondet init of pointers to structs [blocks: #3443] Nov 24, 2018

tautschnig approved these changes Nov 24, 2018

View reviewed changes

tautschnig assigned danpoe and unassigned tautschnig and kroening Nov 24, 2018

danpoe added 2 commits November 26, 2018 17:14

Add source location parameter to get_nondet_bool()

f0a7f1f

danpoe force-pushed the feature/nondet-init-structs branch 2 times, most recently from 3fbc8e2 to be40ff5 Compare November 26, 2018 17:30

danpoe added 8 commits November 26, 2018 17:40

Use get_nondet_bool() in the c nondet symbol factory

d92e817

Remove c_new_tmp_symbol

19effd3

Add c object factory parameters

7f95dd8

Parse c object factory options

d4e14c2

Pass object factory parameters through to object factories

fac59a8

Add regression tests for nondet struct init

8722822

Add recursive nondet struct initialization

a481241

Update documentation of max_nondet_tree_depth object factory parameter

0b605ea

danpoe force-pushed the feature/nondet-init-structs branch from be40ff5 to 0b605ea Compare November 26, 2018 17:41

allredj reviewed Nov 26, 2018

View reviewed changes

danpoe merged commit 28fd58d into diffblue:develop Nov 27, 2018

hannes-steffenhagen-diffblue mentioned this pull request Jan 11, 2019

Feature nondet array initialization [blocks: #3572] #3750

Closed

6 tasks

hannes-steffenhagen-diffblue mentioned this pull request Feb 13, 2019

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

Merged

7 tasks

danpoe deleted the feature/nondet-init-structs branch June 2, 2020 17:13

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Recursive nondet init of pointers to structs [blocks: #3443] #3251

Recursive nondet init of pointers to structs [blocks: #3443] #3251

danpoe commented Oct 31, 2018 •

edited

Loading

peterschrammel Nov 1, 2018

danpoe Nov 2, 2018

peterschrammel Nov 1, 2018

danpoe Nov 2, 2018

hannes-steffenhagen-diffblue left a comment

hannes-steffenhagen-diffblue Nov 1, 2018

danpoe Nov 2, 2018

hannes-steffenhagen-diffblue Nov 1, 2018

danpoe Nov 5, 2018

hannes-steffenhagen-diffblue Nov 7, 2018 •

edited

Loading

chrisr-diffblue Nov 16, 2018

hannes-steffenhagen-diffblue Nov 1, 2018

danpoe Nov 5, 2018

xbauch Nov 2, 2018

danpoe Nov 2, 2018

xbauch Nov 2, 2018

danpoe Nov 2, 2018

danpoe commented Nov 23, 2018

allredj left a comment

peterschrammel left a comment •

edited

Loading

allredj commented Nov 23, 2018

tautschnig left a comment

tautschnig Nov 24, 2018

tautschnig Nov 24, 2018

tautschnig Nov 24, 2018

tautschnig Nov 24, 2018

tautschnig Nov 24, 2018

tautschnig Nov 24, 2018

tautschnig Nov 24, 2018

danpoe Nov 26, 2018

tautschnig Nov 24, 2018

tautschnig Nov 24, 2018

tautschnig Nov 24, 2018

allredj left a comment


		#include <util/object_factory_parameters.h>

		struct java_object_factory_parameterst final : public object_factory_parameterst


		\*******************************************************************/

		#include "java_object_factory_parameters.h"

Recursive nondet init of pointers to structs [blocks: #3443] #3251

Recursive nondet init of pointers to structs [blocks: #3443] #3251

Conversation

danpoe commented Oct 31, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hannes-steffenhagen-diffblue left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hannes-steffenhagen-diffblue Nov 7, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

danpoe commented Nov 23, 2018

allredj left a comment

Choose a reason for hiding this comment

peterschrammel left a comment • edited Loading

Choose a reason for hiding this comment

allredj commented Nov 23, 2018

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

danpoe commented Oct 31, 2018 •

edited

Loading

hannes-steffenhagen-diffblue Nov 7, 2018 •

edited

Loading

peterschrammel left a comment •

edited

Loading