Function pointer non-det initialisation in goto-harness [depends-on: #5171] #5176

NlightNFotis · 2019-11-07T16:59:16Z

This is extending the work done in #5171 of which the first commit of this PR belongs to.

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.

src/goto-harness/recursive_initialization.cpp

xbauch

Looks good.

codecov-io · 2019-11-08T11:57:20Z

Codecov Report

Merging #5176 into develop will decrease coverage by 0.06%.
The diff coverage is 86.95%.

@@             Coverage Diff             @@
##           develop    #5176      +/-   ##
===========================================
- Coverage     67.4%   67.33%   -0.07%     
===========================================
  Files         1157     1155       -2     
  Lines        95166    94736     -430     
===========================================
- Hits         64144    63794     -350     
+ Misses       31022    30942      -80

Flag	Coverage Δ
#cproversmt2	`42.64% <ø> (-0.03%)`	⬇️
#regression	`63.82% <86.95%> (-0.1%)`	⬇️
#unit	`31.96% <ø> (ø)`	⬆️

Impacted Files	Coverage Δ
src/goto-harness/recursive_initialization.h	`100% <100%> (ø)`	⬆️
src/goto-harness/recursive_initialization.cpp	`85.56% <100%> (+0.24%)`	⬆️
...c/goto-harness/function_call_harness_generator.cpp	`82.55% <65.38%> (-4.41%)`	⬇️
src/analyses/ai_domain.h	`12.5% <0%> (-55.69%)`	⬇️
src/goto-analyzer/static_verifier.cpp	`45.16% <0%> (-12.24%)`	⬇️
...c/goto-harness/memory_snapshot_harness_generator.h	`88.88% <0%> (-8.48%)`	⬇️
src/analyses/ai.cpp	`66.9% <0%> (-6.71%)`	⬇️
src/goto-checker/report_util.cpp	`38.27% <0%> (-4.7%)`	⬇️
src/goto-instrument/unwindset.cpp	`82.75% <0%> (-2.54%)`	⬇️
jbmc/src/janalyzer/janalyzer_parse_options.cpp	`45.7% <0%> (-2.5%)`	⬇️
... and 87 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 2400d10...6b684f7. Read the comment docs.

allredj

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

allredj

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

allredj

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

allredj

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

xbauch · 2019-11-13T08:34:54Z

src/goto-harness/function_call_harness_generator.cpp

@@ -12,6 +12,7 @@ Author: Diffblue Ltd.
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/exception_utils.h>
+#include <util/prefix.h>


do you still need this? (edit: you do, but somewhere in the 4th commit; no need to reorder because of this.)

I think it's worth fixing that.

xbauch · 2019-11-13T08:37:38Z

src/goto-harness/recursive_initialization.cpp


  goto_model.goto_functions.function_map[function_symbol.name].type =
    to_code_type(function_symbol.type);
-  return type_constructor_names[type];
+  return type_constructor_names.at(key);


Is there a reason why this access is checked but the above are not?

Not really, tbh we'd considered refactoring this entire section to avoid multiple lookup of the same key. We only added the .at because at some point we were hitting a case where keys were missing from the map.

xbauch · 2019-11-13T08:39:00Z

src/goto-harness/recursive_initialization.cpp

  if(expr.id() == ID_symbol)
  {
    expr_name = to_symbol_expr(expr).get_identifier();
+    is_nullable = initialization_config.potential_null_function_pointers.count(
+      expr_name.value());


Maybe it's idiomatic, but I would prefer count(..) != 0

I agree that'd be easier to read.

xbauch · 2019-11-13T08:46:17Z

src/goto-harness/function_call_harness_generator.cpp

+    }
+
+    const auto &function_pointer_type =
+      ns.follow(function_pointer_symbol_pointer->type);


Why do we need to follow the type?

Symbol types aren't resolved at this point (i.e. in the symbol table). They can't be, otherwise we couldn't correctly print typedefs etc in dump-c.

src/goto-harness/common_harness_generator_options.h

src/goto-harness/recursive_initialization.cpp

allredj

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

hannes-steffenhagen-diffblue · 2020-01-24T10:40:51Z

src/goto-harness/function_call_harness_generator.cpp

@@ -72,10 +72,10 @@ struct function_call_harness_generatort::implt
  void ensure_harness_does_not_already_exist();
  /// Update the goto-model with the new harness function.
  void add_harness_function_to_goto_model(code_blockt function_body);
-  /// declare local variables for each of the parameters of the entry function
+  /// Declare local variables for each of the parameters of the entry function


44509e4 are good changes, but might be better off in a separate PR (although it’d be annoying to separate out this late I know)

hannes-steffenhagen-diffblue · 2020-01-24T10:46:59Z

src/goto-harness/recursive_initialization.cpp

+
+  for(const auto &sym : goto_model.get_symbol_table())
+  {
+    if(sym.second.type == function_type)


We should probably make this work with the function pointer restriction table stuff we have some time.

hannes-steffenhagen-diffblue · 2020-01-24T10:50:32Z

src/goto-harness/recursive_initialization.h

+    typet constructor_type;
+    bool is_nullable;
+    bool has_size_parameter;
+    bool operator<(const constructor_keyt &other) const


With C++20 we could just default these ;)

hannes-steffenhagen-diffblue · 2020-01-24T11:30:14Z

src/goto-harness/recursive_initialization.h

+  /// \return the body of the constructor
+  code_blockt build_function_pointer_constructor(
+    const symbol_exprt &result,
+    bool is_nullable);


I’m not extremely excited about having to pass this is_nullable argument down all the time, but I can’t think of anything super great either.

hannes-steffenhagen-diffblue · 2020-01-24T13:11:02Z

src/goto-harness/function_call_harness_generator.cpp

+  /// this specification from that for a global variable of the same name,
+  /// we prepend the name of the function to the parameter name. However,
+  /// what is actually being initialised in the implementation is not the
+  /// parameter itself, but a correspond function argument (local variable


correspond(ing)

Add error checking (check that the entry function is in the symbol table before the code generation, and make sure that it's present correctly) make sure that doc comments are capitalised, change the signatures of functions to make them stricter in the arguments they accept.

Also add support for having multiple constructors for the same type with different behaviours and different signatures. We are doing this because we need some types to be sometimes nullable and sometimes not, and for example, for arrays we sometimes need to pass a size parameter and sometimes not.

Add mapping from function pointer argument names to local variable names of the harness so users can specify properties of arguments in terms of the names of the arguments rather than having to rely on internal implementation details of the function harness.

Add a test to make sure that we can distinguish between a parameter and a global function pointer variable with the same name and a test to make sure that we get different type constructors for the same type but with extra attributes.

Move it to recursive_initialization_configt because it's a common option.

NlightNFotis self-assigned this Nov 7, 2019

xbauch reviewed Nov 8, 2019

View reviewed changes

src/goto-harness/recursive_initialization.cpp Outdated Show resolved Hide resolved

xbauch approved these changes Nov 8, 2019

View reviewed changes

NlightNFotis force-pushed the feature/function-pointer-nondet-harness branch from 67edbb6 to 825029a Compare November 8, 2019 10:48

allredj reviewed Nov 8, 2019

View reviewed changes

NlightNFotis force-pushed the feature/function-pointer-nondet-harness branch 6 times, most recently from ea06a2f to 60398e7 Compare November 12, 2019 11:59

allredj reviewed Nov 12, 2019

View reviewed changes

NlightNFotis marked this pull request as ready for review November 12, 2019 16:37

NlightNFotis requested review from chrisr-diffblue, danpoe, hannes-steffenhagen-diffblue, martin-cs and peterschrammel as code owners November 12, 2019 16:37

allredj reviewed Nov 12, 2019

View reviewed changes

xbauch reviewed Nov 13, 2019

View reviewed changes

xbauch changed the title ~~Function pointer non-det initialisation in goto-harness~~ Function pointer non-det initialisation in goto-harness [depends-on: #5171] Nov 13, 2019

xbauch added the dependent - do not merge label Nov 13, 2019

xbauch pushed a commit to xbauch/cbmc that referenced this pull request Nov 13, 2019

Prerequisite PR diffblue#5176 -- do not review

831fa1a

xbauch mentioned this pull request Nov 13, 2019

Goto-harness support to selectively havoc struct members #5183

Merged

7 tasks

xbauch reviewed Nov 13, 2019

View reviewed changes

src/goto-harness/common_harness_generator_options.h Show resolved Hide resolved

xbauch reviewed Nov 13, 2019

View reviewed changes

src/goto-harness/recursive_initialization.cpp Show resolved Hide resolved

NlightNFotis force-pushed the feature/function-pointer-nondet-harness branch 2 times, most recently from 3922445 to 272477c Compare November 14, 2019 14:34

allredj reviewed Nov 14, 2019

View reviewed changes

hannes-steffenhagen-diffblue reviewed Jan 24, 2020

View reviewed changes

hannes-steffenhagen-diffblue approved these changes Jan 24, 2020

View reviewed changes

NlightNFotis force-pushed the feature/function-pointer-nondet-harness branch from 272477c to 14aeac2 Compare January 27, 2020 14:49

NlightNFotis added 4 commits January 27, 2020 14:59

Add more tests.

6eb5990

Add a test to make sure that we can distinguish between a parameter and a global function pointer variable with the same name and a test to make sure that we get different type constructors for the same type but with extra attributes.

Move function-pointer-can-be-null option handling.

6b684f7

Move it to recursive_initialization_configt because it's a common option.

NlightNFotis force-pushed the feature/function-pointer-nondet-harness branch from 14aeac2 to 6b684f7 Compare January 27, 2020 15:31

hannes-steffenhagen-diffblue removed the dependent - do not merge label Jan 27, 2020

NlightNFotis merged commit 0002950 into diffblue:develop Jan 28, 2020

NlightNFotis deleted the feature/function-pointer-nondet-harness branch January 28, 2020 10:33

Function pointer non-det initialisation in goto-harness [depends-on: #5171] #5176

Function pointer non-det initialisation in goto-harness [depends-on: #5171] #5176

Uh oh!

Conversation

NlightNFotis commented Nov 7, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

xbauch left a comment

Choose a reason for hiding this comment

Uh oh!

codecov-io commented Nov 8, 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!

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!

xbauch Nov 13, 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!

Uh oh!

Uh oh!

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

Uh oh!

NlightNFotis commented Nov 7, 2019 •

edited

Loading

codecov-io commented Nov 8, 2019 •

edited

Loading

xbauch Nov 13, 2019 •

edited

Loading