Feature nondet string initialization [depends-on: #3750] #3572

hannes-steffenhagen-diffblue · 2018-12-14T19:50:00Z

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.

tautschnig · 2018-12-17T15:43:52Z

src/ansi-c/ansi_c_language.h


 #define HELP_ANSI_C_LANGUAGE \
  " --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" \
  " --min-null-tree-depth N      minimum level at which a pointer can first be\n" /* NOLINT(*) */\
-  "                              NULL in a recursively nondet initialized struct\n" /* NOLINT(*) */
+  "                              NULL in a recursively nondet initialized struct\n" /* NOLINT(*) */\
+  " --pointers-to-treat-as-array <identifier,...>  Comma separated list of\n" \


Nit pick: we seem to start help messages with a lowercase letter.

tautschnig · 2018-12-17T15:44:31Z

src/ansi-c/ansi_c_language.h

+  "                               identifiers that should be initialized as arrays\n" /* NOLINT(*) */ \
+  " --associated-array-sizes <identifier:identifier...>\n" \
+  "                               comma separated list of colon separated pairs\n" /* NOLINT(*) */ \
+  "                               of identifiers; The first should be the name\n" /* NOLINT(*) */ \


"The first" ... what?

tautschnig · 2018-12-17T15:45:20Z

src/ansi-c/c_nondet_symbol_factory.cpp

 #include <util/std_expr.h>
 #include <util/std_types.h>
 #include <util/string_constant.h>

 #include <goto-programs/goto_functions.h>
+#include <util/array_name.h>
+#include <util/optional_utils.h>
+#include <util/pointer_offset_size.h>


Place alongside the other includes from util

tautschnig · 2018-12-17T15:51:11Z

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -39,12 +45,14 @@ class symbol_factoryt
    std::vector<const symbolt *> &_symbols_created,
    symbol_tablet &_symbol_table,
    const source_locationt &loc,
-    const c_object_factory_parameterst &object_factory_params)
+    const c_object_factory_parameterst &object_factory_params,
+    std::map<irep_idt, irep_idt> &deferred_array_sizes)


Where is this passed in as a non-empty map?

This is kept as state between calls to c_nondet_symbol_factory here: 25be369#diff-ffd0a317958e24d1f65f21ed40f67c99L39

tautschnig · 2018-12-17T15:52:26Z

src/ansi-c/ansi_c_language.h

@@ -26,6 +26,7 @@ Author: Daniel Kroening, [email protected]
  "(pointers-to-treat-as-array):" \
  "(associated-array-sizes):" \
  "(max-dynamic-array-size):" \
+  "(pointers-to-treat-as-string):"


Missing help

hannes-steffenhagen-diffblue · 2018-12-18T17:55:09Z

src/ansi-c/c_nondet_symbol_factory.cpp

+
+  /// Return the name of a variable holding an array size if one is associated
+  /// with the given symbol name
+  optionalt<dstringt> get_deferred_size(irep_idt symbol_name) const;


should be an irep_idt, damn you clion

tautschnig · 2018-12-18T18:04:49Z

As a note while this is still "work in progress": I found it quite difficult to review. If there is any way to break things up into smaller commits, or maybe just into smaller hunks by refactoring functions that would be much appreciated.

danpoe · 2018-12-20T14:11:52Z

src/ansi-c/ansi_c_language.h

@@ -22,13 +22,30 @@ Author: Daniel Kroening, [email protected]
 // clang-format off
 #define OPT_ANSI_C_LANGUAGE \
  "(max-nondet-tree-depth):" \
-  "(min-null-tree-depth):"
+  "(min-null-tree-depth):" \
+  "(pointers-to-treat-as-array):" \


pointers-to-treat-as-array -> pointers-to-treat-as-arrays (and throughout the PR)

danpoe · 2018-12-20T14:12:32Z

src/ansi-c/ansi_c_language.h

+  "(pointers-to-treat-as-array):" \
+  "(associated-array-sizes):" \
+  "(max-dynamic-array-size):" \
+  "(pointers-to-treat-as-string):"


pointers-to-treat-as-string -> pointers-to-treat-as-strings (and throughout the PR)

danpoe · 2018-12-20T14:13:44Z

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -13,16 +13,21 @@ Author: Diffblue Ltd.

 #include <ansi-c/c_object_factory_parameters.h>

+#include <functional>


Separate from the rest of the includes

danpoe · 2018-12-20T14:14:20Z

src/ansi-c/c_nondet_symbol_factory.cpp

+  /// \param prefix: This forms the first part of the parameter,
+  ///   for debugging purposes must be a valid identifier prefix
+  /// \return A reference to the newly created symbol table entry
+  symbolt &new_tmp_symbol(const typet &type, const std::string &prefix);


This can now be replaced by allocate_objectst::allocate_automatic_local_object()

danpoe · 2018-12-20T14:17:03Z

src/ansi-c/c_nondet_symbol_factory.cpp

+  /// variable yet (i.e. it is not yet in the symbol table and doesn't have
+  /// initialisation code generated for it yet). If that's the case we remember
+  /// that we have to set it to the right size later with this method.
+  /// \param associated_size_name: The of variable that should be set to


The of variable... -> The name of the variable...

danpoe · 2018-12-20T14:17:45Z

src/ansi-c/c_nondet_symbol_factory.cpp

+    array_member_init_body,
+    dereference_exprt{
+      plus_exprt{array, array_index_symbol.symbol_expr(), array.type()}},
+    depth,


I think we need to pass in depth + 1 here since we dereference the expression (since we pass in a dereference_exprt).

danpoe · 2018-12-20T14:29:54Z

src/ansi-c/c_nondet_symbol_factory.cpp

+      if(associated_array_size.has_value())
+      {
+        assign.rhs() = typecast_exprt{
+          symbol_table.lookup_ref(associated_array_size.value()).symbol_expr(),


Hm, does this work? I thought lookup_ref() requires the full name of a symbol whereas associated_array_size is the base name I think.

Ah, this does work but is confusingly worded. The associated_array_size here is actually the deferred array size symbol which we dynamically created earlier, and we do have the full name for that. I'll see if I can make this clearer

hannes-steffenhagen-diffblue · 2019-01-08T10:26:07Z

@tautschnig I'll see if I can restructure the commits to make the changes clearer. Meanwhile the first and second commit do implement related but separate features so it probably makes sense to keep them as separate PRs, which would also help a bit I hope

tautschnig · 2019-01-08T11:30:27Z

@hannes-steffenhagen-diffblue Anything that can be done to make this a bit smaller would really help reviewing. If it's not possible we'll have to bite the bullet, so please just send a ping when this is in the best possible state for a review.

hannes-steffenhagen-diffblue · 2019-01-10T16:46:36Z

@tautschnig I've extracted the larger part (that which is not string specific) into a separate PR at #3750. In there I've also split up that feature into a couple of mostly independent commits, which should make it a bit easier to review (although it is still not a small amount of code).

If that goes through I'll rebase the string specific bits and put them here.

hannes-steffenhagen-diffblue · 2019-01-27T21:19:25Z

Closed as we decided to do this another way

tautschnig · 2019-01-28T09:34:59Z

@hannes-steffenhagen-diffblue I'm a bit confused, as #3750 appears to have been closed as well?

hannes-steffenhagen-diffblue added the work in progress label Dec 14, 2018

hannes-steffenhagen-diffblue requested review from kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners December 14, 2018 19:50

hannes-steffenhagen-diffblue force-pushed the feature-nondet-string-initialization branch 4 times, most recently from 8b51090 to a986d5e Compare December 17, 2018 14:54

hannes-steffenhagen-diffblue added 2 commits December 17, 2018 15:38

Add support for dynamic pointer to array initialisation

25be369

Add support for nondet initialisation of dynamic C strings

ff47643

hannes-steffenhagen-diffblue force-pushed the feature-nondet-string-initialization branch from a986d5e to ff47643 Compare December 17, 2018 15:38

tautschnig reviewed Dec 17, 2018

View reviewed changes

tautschnig assigned hannes-steffenhagen-diffblue Dec 17, 2018

hannes-steffenhagen-diffblue commented Dec 18, 2018

View reviewed changes

danpoe reviewed Dec 20, 2018

View reviewed changes

hannes-steffenhagen-diffblue changed the title ~~Feature nondet string initialization~~ Feature nondet string initialization [depends-on: #3572] Jan 10, 2019

hannes-steffenhagen-diffblue changed the title ~~Feature nondet string initialization [depends-on: #3572]~~ Feature nondet string initialization [depends-on: #3750] Jan 10, 2019

hannes-steffenhagen-diffblue closed this Jan 27, 2019

		@@ -13,16 +13,21 @@ Author: Diffblue Ltd.

		#include <ansi-c/c_object_factory_parameters.h>

		#include <functional>

Feature nondet string initialization [depends-on: #3750] #3572

Feature nondet string initialization [depends-on: #3750] #3572

Uh oh!

Conversation

hannes-steffenhagen-diffblue commented Dec 14, 2018

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!

tautschnig commented Dec 18, 2018

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 commented Jan 8, 2019

Uh oh!

tautschnig commented Jan 8, 2019

Uh oh!

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

Uh oh!

Uh oh!

hannes-steffenhagen-diffblue commented Jan 27, 2019

Uh oh!

tautschnig commented Jan 28, 2019

Uh oh!

Uh oh!

hannes-steffenhagen-diffblue commented Jan 10, 2019 •

edited

Loading