Do not use side_effect_expr_nondett in recursive_initialization #5409

hannes-steffenhagen-diffblue · 2020-07-03T08:45:17Z

If we use side_effect_expr_nondett then dump_c will generation function calls
to functions with names like nondet_int without declaration.

This is a problem because it’ll lead the C frontend to complain about
undeclared identifiers and such.

To fix this, we changed goto-harness to just not use side_effect_expr_nondett
at all (better long term fix would be to make sure dump_c outputs
declarations too).

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.

thk123

There are a bunch of changes - it'd be good to have a test for each one to ensure the change has worked as expected. Other than that, lgtm

thk123 · 2020-07-03T09:04:20Z

regression/goto-harness/do-not-use-nondet-for-primitives/test.desc

+test.c
+--function test_function --harness-type call-function
+\[test_function\.assertion\.1\] line \d+ assertion test != 42
+^EXIT=10$


⛏️ It'd be good to have a positive regex for what it now contains (e.g. a declaration or whatever) since that documents the behaviour, and makes the test less likely to spuriously pass in the future

thk123 · 2020-07-03T09:05:31Z

regression/goto-harness/do-not-use-nondet-for-primitives/test.desc

+If we use side_effect_expr_nondett then dump_c will generation function calls
+to functions with names like nondet_signed_int without declaration.
+This can cause problems around usability.
+
+To fix this, we changed goto-harness to just not use side_effect_expr_nondett
+at all.
+
+This test tests for the absence the use for these things.


⛏️ This seems like great info for a commit message (since it is talking about why we moved from one solution to another) but in a test, where the reader won't have the context that we used to use side_effect_expr_nondett it is maybe confusing. I'd focus instead on what the test is testing - in this case not using undeclared functions.

I note this info is in the commit too 👍 I still think probably more confusing than helpful in the test, but up to you

thk123 · 2020-07-03T09:06:26Z

src/goto-harness/recursive_initialization.cpp

@@ -169,11 +169,11 @@ void recursive_initializationt::initialize(
            goto_model.symbol_table.lookup_ref(fun_name);
          const auto proper_init_case = code_function_callt{
            fun_symbol.symbol_expr(), {depth, address_of_exprt{lhs}}};
-
+          const auto should_make_equal =


🚫 Looks like this is a separate case and therefore should have a separate test? 🧷

thk123 · 2020-07-03T09:06:49Z

src/goto-harness/recursive_initialization.cpp

@@ -693,9 +693,12 @@ code_blockt recursive_initializationt::build_pointer_constructor(
  code_blockt null_and_return{{assign_null, code_returnt{}}};
  body.add(code_ifthenelset{conjunction(should_not_recurse), null_and_return});

+  const auto should_recurse_nondet =


thk123 · 2020-07-03T09:10:02Z

src/goto-harness/recursive_initialization.cpp

@@ -753,8 +756,10 @@ code_blockt recursive_initializationt::build_array_string_constructor(
  {
    index_exprt index_expr{dereference_exprt{result},
                           from_integer(index, size_type())};
-    body.add(code_assignt{


thk123 · 2020-07-03T09:10:46Z

src/goto-harness/recursive_initialization.cpp

@@ -1029,10 +1035,6 @@ code_blockt recursive_initializationt::build_function_pointer_constructor(
  const auto function_pointer_selector =
    get_fresh_local_symexpr("function_pointer_selector");
  body.add(code_declt{function_pointer_selector});
-  body.add(


Ehem, upon trying to come up with a test for this I actually found that there was a mess up in some earlier refactoring leading to this function never ever getting called (instead implementation of what this used to do has been moved into build_dynamic_array_constructor.

That is a tad unfortunate. I will add a commit that removes this function to show that it doesn’t work right now, and then we can re-refactor it later if we like.

NlightNFotis

Good enough for me, can we have a ticket for the better long term fix?

codecov · 2020-07-03T09:54:42Z

Codecov Report

Merging #5409 into develop will increase coverage by 0.00%.
The diff coverage is 100.00%.

@@           Coverage Diff            @@
##           develop    #5409   +/-   ##
========================================
  Coverage    68.19%   68.19%           
========================================
  Files         1175     1175           
  Lines        97497    97478   -19     
========================================
- Hits         66484    66479    -5     
+ Misses       31013    30999   -14

Flag	Coverage Δ
#cproversmt2	`42.50% <ø> (ø)`
#regression	`65.36% <100.00%> (-0.01%)`	⬇️
#unit	`32.24% <ø> (ø)`

Impacted Files	Coverage Δ
src/goto-harness/recursive_initialization.h	`100.00% <ø> (ø)`
src/goto-harness/recursive_initialization.cpp	`90.68% <100.00%> (+3.53%)`	⬆️
src/goto-instrument/goto_program2code.cpp	`65.75% <0.00%> (-0.52%)`	⬇️

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 823782c...430ab00. Read the comment docs.

martin-cs

Fine modulo @thk123 's comments.

If we use side_effect_expr_nondett then dump_c will generation function calls to functions with names like `nondet_int` without declaration. This is a problem because it’ll lead the C frontend to complain about undeclared identifiers and such. To fix this, we changed goto-harness to just not use side_effect_expr_nondett at all (better long term fix would be to make sure `dump_c` outputs declarations too).

The ::build_array_string_constructor method was originally intended to be used for building C string constructors. Unfortunately as written the condition for calling it was actually impossible to satisfy. This wasn’t noticed so far because similar code is now generated in ::build_dynamic_array_constructor instead. Dead code is a maintenance burden so it’s removed here.

hannes-steffenhagen-diffblue · 2020-07-08T09:34:23Z

Note that there’s a second commit removing a dead (as in, impossible to reach) function now.

hannes-steffenhagen-diffblue requested review from chrisr-diffblue, danpoe, martin-cs and peterschrammel as code owners July 3, 2020 08:45

thk123 reviewed Jul 3, 2020

View reviewed changes

NlightNFotis approved these changes Jul 3, 2020

View reviewed changes

martin-cs approved these changes Jul 7, 2020

View reviewed changes

NlightNFotis mentioned this pull request Jul 7, 2020

Fix static symbols referencing in harness file #5412

Merged

7 tasks

hannes-steffenhagen-diffblue force-pushed the fix/do_not_use_side_effect_expr_nondett_in_goto_harness branch from 07dec16 to 8bc1772 Compare July 7, 2020 18:26

hannes-steffenhagen-diffblue added 2 commits July 8, 2020 10:21

hannes-steffenhagen-diffblue force-pushed the fix/do_not_use_side_effect_expr_nondett_in_goto_harness branch from 8bc1772 to 430ab00 Compare July 8, 2020 09:30

NlightNFotis merged commit 695a360 into diffblue:develop Jul 8, 2020

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Do not use side_effect_expr_nondett in recursive_initialization #5409

Do not use side_effect_expr_nondett in recursive_initialization #5409

Uh oh!

hannes-steffenhagen-diffblue commented Jul 3, 2020

Uh oh!

thk123 left a comment

Uh oh!

thk123 Jul 3, 2020

Uh oh!

thk123 Jul 3, 2020

Uh oh!

thk123 Jul 3, 2020

Uh oh!

thk123 Jul 3, 2020

Uh oh!

thk123 Jul 3, 2020

Uh oh!

thk123 Jul 3, 2020

Uh oh!

thk123 Jul 3, 2020

Uh oh!

hannes-steffenhagen-diffblue Jul 7, 2020

Uh oh!

NlightNFotis left a comment

Uh oh!

codecov bot commented Jul 3, 2020 •

edited

Loading

Uh oh!

martin-cs left a comment

Uh oh!

hannes-steffenhagen-diffblue commented Jul 8, 2020

Uh oh!

Uh oh!

Do not use side_effect_expr_nondett in recursive_initialization #5409

Do not use side_effect_expr_nondett in recursive_initialization #5409

Uh oh!

Conversation

hannes-steffenhagen-diffblue commented Jul 3, 2020

Uh oh!

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

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!

NlightNFotis left a comment

Choose a reason for hiding this comment

Uh oh!

codecov bot commented Jul 3, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue commented Jul 8, 2020

Uh oh!

Uh oh!

codecov bot commented Jul 3, 2020 •

edited

Loading