Improve harness generated code readability #5087

xbauch · 2019-09-04T16:06:00Z

Previously all recursive initialisation took place in a single function. Now each type has it's own constructor function, which are called recursively. The results (variables to be initialised) are passed by pointer.

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.

codecov-io · 2019-09-05T08:51:55Z

Codecov Report

Merging #5087 into develop will decrease coverage by 0.09%.
The diff coverage is 92.88%.

@@            Coverage Diff             @@
##           develop    #5087     +/-   ##
==========================================
- Coverage    69.66%   69.56%   -0.1%     
==========================================
  Files         1319     1315      -4     
  Lines       109239   109122    -117     
==========================================
- Hits         76098    75916    -182     
- Misses       33141    33206     +65

Impacted Files	Coverage Δ
src/goto-harness/recursive_initialization.h	`100% <ø> (ø)`	⬆️
...c/goto-harness/function_call_harness_generator.cpp	`89.81% <100%> (+0.29%)`	⬆️
src/pointer-analysis/value_set.cpp	`76.02% <100%> (-0.78%)`	⬇️
...goto-harness/memory_snapshot_harness_generator.cpp	`90.32% <100%> (+0.32%)`	⬆️
src/goto-harness/recursive_initialization.cpp	`83.59% <92.33%> (+8.59%)`	⬆️
src/analyses/natural_loops.cpp	`0% <0%> (-100%)`	⬇️
src/analyses/natural_loops.h	`76.31% <0%> (-23.69%)`	⬇️
src/util/invariant.cpp	`60.52% <0%> (-13.16%)`	⬇️
src/goto-symex/build_goto_trace.cpp	`84.82% <0%> (-2.76%)`	⬇️
src/analyses/local_may_alias.cpp	`56.25% <0%> (-2.28%)`	⬇️
... and 72 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update eaf8cb3...8cb2f6e. Read the comment docs.

allredj

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

allredj

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

hannes-steffenhagen-diffblue

Mostly looks fine to me, but I think the decision of what things to initialise or not should be made outside of recursive_initialisation

hannes-steffenhagen-diffblue · 2019-09-05T08:14:24Z

src/goto-harness/function_call_harness_generator.cpp

@@ -195,6 +197,9 @@ void function_call_harness_generatort::implt::generate(

  generate_nondet_globals(function_body);
  call_function(arguments, function_body);
+  for(const auto &global_pointer : global_pointers)


⛏️ braces please

hannes-steffenhagen-diffblue · 2019-09-05T08:15:05Z

src/goto-harness/function_call_harness_generator.cpp

@@ -195,6 +197,9 @@ void function_call_harness_generatort::implt::generate(

  generate_nondet_globals(function_body);
  call_function(arguments, function_body);
+  for(const auto &global_pointer : global_pointers)
+    function_body.add(code_function_callt{


Hm, I thought you'd have to pass more than one parameter here sometimes?

hannes-steffenhagen-diffblue · 2019-09-05T08:44:37Z

src/goto-harness/memory_snapshot_harness_generator.cpp

+  code_blockt code{};
+
+  // add initialization for existing globals
+  for(auto pair : goto_model.symbol_table)


hannes-steffenhagen-diffblue · 2019-09-05T09:34:20Z

src/goto-harness/memory_snapshot_harness_generator.cpp

+  {
+    if(
+      id2string(pair.first).find(CPROVER_PREFIX) != 0 &&
+      pair.second.is_static_lifetime)


See the function call harness, you'll also want

&& symbol.is_lvalue && symbol.type.id() != ID_code && !has_prefix(id2string(symbol.name), CPROVER_PREFIX)

because we don't want to initialise function symbols, non-lvalues or cprover internal variables (we should probably factor out this filtering stuff into a separate utility)

Extracted and moved to recursive_initializationt.

hannes-steffenhagen-diffblue · 2019-09-05T09:39:20Z

src/goto-harness/recursive_initialization.cpp

+      "min_depth",
+      from_integer(
+        initialization_config.min_null_tree_depth,
+        signed_int_type())))


it's kind of irrelevant but I'd have expected these to be size_t

The only reason I went for int is that it looks better in the dumped code.

hannes-steffenhagen-diffblue · 2019-09-05T09:47:10Z

src/goto-harness/recursive_initialization.cpp

-    initialize_struct_tag(lhs, depth, known_tags, body);
-  }
-  else if(type.id() == ID_pointer)
+  const irep_idt &fun_name = build_constructor(lhs);


Surely build_constructor only needs lhs.type()?

We also need the name of the symbol (if lhs is a symbol) to get the associated_size_variable etc.

hannes-steffenhagen-diffblue · 2019-09-05T09:49:14Z

src/goto-harness/recursive_initialization.cpp

-    if(lhs.id() == ID_symbol)
+    const irep_idt &lhs_name = to_symbol_expr(lhs).get_identifier();
+    // skip initialisation of max/min depth globals
+    if(lhs_name == max_depth_var_name || lhs_name == min_depth_var_name)


I think it'd be cleaner to remove these from the global set in the first place - IIRC at least the function-harness automatically strips all variables with a __CPROVER_ prefix from the list of variables to nondet (all harnesses should do this, may be worth extracting into separate functionality). All our global (maybe even local, given that cbmc doesn't really care all that much about scope) variables should have the __CPROVER_ prefix attached to them anyway (that way we can avoid accidentally overriding variables that we add in here without having to remember to block each of them individually here)

hannes-steffenhagen-diffblue · 2019-09-05T09:51:02Z

src/goto-harness/recursive_initialization.cpp

+          goto_model.symbol_table.lookup_ref(size_var.value()).symbol_expr();
+        body.add(code_function_callt{
+          fun_symbol.symbol_expr(),
+          {depth, address_of_exprt{lhs}, address_of_exprt{size_symbol}}});


That's one way to do it, but I don't like having the replicated logic between the constructor and the call; I'd prefer if the dynamic array constructor just always took a size pointer and just set it to null if it's not needed (kind of mirroring similar functions in the real world)

hannes-steffenhagen-diffblue · 2019-09-23T10:29:31Z

src/goto-harness/recursive_initialization.cpp

+{
+  symbolt &fresh_symbol = get_fresh_aux_symbol(
+    signed_int_type(),
+    "__goto_harness",


Probably makes more sense to use CPROVER_PREFIX, same in following

hannes-steffenhagen-diffblue · 2019-09-23T10:31:29Z

src/goto-harness/recursive_initialization.cpp

+
+symbol_exprt recursive_initializationt::get_free_function()
+{
+  auto free_sym = goto_model.symbol_table.lookup("free");


FYI we had some talk at some point about using CBMCs internal allocate/deallocate instructions for this, but I didn't have much luck for them (no need for changes, just a remark)

allredj

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

NlightNFotis

Looks good to me overall, just some minor comments.

NlightNFotis · 2019-09-27T08:43:01Z

src/goto-harness/recursive_initialization.cpp

@@ -428,6 +428,9 @@ std::string recursive_initialization_configt::to_string() const

 recursive_initializationt::array_convertert
 recursive_initializationt::default_array_member_initialization()
+irep_idt recursive_initializationt::get_fresh_global_name(
+  const std::string &symbol_name,


get_fresh_global_name and get_fresh_global_symexpr look very similar. Are we sure the bulk of the work performed in one function, and then have the helpers call into it?

NlightNFotis · 2019-09-27T08:45:57Z

src/goto-harness/recursive_initialization.cpp

+  symbolt *mutable_symbol = symbol_table.get_writeable(function_symbol.name);
+
+  // the body is specific for each type of expression
+  mutable_symbol->value = build_constructor_body(


slightly weird that build_constructor_body is being referenced here but added in the next commit and there's a prototype added for it as well in recursive_initialization.h

I wasn't sure how to break the PR into individual commits so I sometimes formed a commit around a body of a function but only declared the functions called inside that body.

NlightNFotis · 2019-09-27T08:49:21Z

src/goto-harness/recursive_initialization.cpp

+  {
+    if(lhs_name.has_value())
+    {
+      if(should_be_treated_as_cstring(*lhs_name) && type == char_type())


Just a question, since I'm not sure why it's happening:

Why in other places we compare the type.id(), like for instance in line 137 type.id() == ID_pointer and here we compare the type itself with the constructor result? Are we sure equality is working as it should? If yes, should all of these be harmonised?

That's just my being lazy and not finding out what type-id char should have.

because we also want to convert the function that will be added during initialisation.

also add mode to memory-snapshot.

and storing the in the symbol table (and one for `free`).

Previously all recursive initialisation took place in a single function. Now each type has it's own constructor function, which are called recursively. The results (variables to be initialised) are passed by pointer.

allredj

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

allredj reviewed Sep 5, 2019

View reviewed changes

hannes-steffenhagen-diffblue approved these changes Sep 23, 2019

View reviewed changes

xbauch force-pushed the feature/better-harness branch 2 times, most recently from b5aec2e to 099cf12 Compare September 24, 2019 10:32

allredj reviewed Sep 24, 2019

View reviewed changes

NlightNFotis reviewed Sep 27, 2019

View reviewed changes

petr-bauch added 4 commits October 3, 2019 15:21

Convert the whole model rather than a single function

32cde1b

because we also want to convert the function that will be added during initialisation.

Clean-up harnesses in testing symbol init-ability

3674dcc

also add mode to memory-snapshot.

Helper functions to simplify manipulating symbols

d0212b9

and storing the in the symbol table (and one for `free`).

Rewrite the recursive constructors

9ca0824

Previously all recursive initialisation took place in a single function. Now each type has it's own constructor function, which are called recursively. The results (variables to be initialised) are passed by pointer.

xbauch force-pushed the feature/better-harness branch from 099cf12 to 9ca0824 Compare October 3, 2019 14:27

xbauch marked this pull request as ready for review October 3, 2019 15:04

xbauch requested review from chrisr-diffblue, danpoe, martin-cs and peterschrammel as code owners October 3, 2019 15:04

allredj reviewed Oct 3, 2019

View reviewed changes

hannes-steffenhagen-diffblue merged commit cb20917 into diffblue:develop Nov 1, 2019

Improve harness generated code readability #5087

Improve harness generated code readability #5087

Uh oh!

Conversation

xbauch commented Sep 4, 2019

Uh oh!

codecov-io commented Sep 5, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

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!

hannes-steffenhagen-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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue Sep 5, 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!

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!

NlightNFotis 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!

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!

codecov-io commented Sep 5, 2019 •

edited

Loading

hannes-steffenhagen-diffblue Sep 5, 2019 •

edited

Loading