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

Do not use side_effect_expr_nondett in recursive_initialization #5409

Do not use side_effect_expr_nondett in recursive_initialization #5409

hannes-steffenhagen-diffblue commented Jul 3, 2020

thk123 left a comment

thk123 Jul 3, 2020

thk123 Jul 3, 2020

thk123 Jul 3, 2020

thk123 Jul 3, 2020

thk123 Jul 3, 2020

thk123 Jul 3, 2020

thk123 Jul 3, 2020

hannes-steffenhagen-diffblue Jul 7, 2020

NlightNFotis left a comment

codecov bot commented Jul 3, 2020 •

edited

Loading

martin-cs left a comment

hannes-steffenhagen-diffblue commented Jul 8, 2020

Do not use side_effect_expr_nondett in recursive_initialization #5409

Do not use side_effect_expr_nondett in recursive_initialization #5409

Conversation

hannes-steffenhagen-diffblue commented Jul 3, 2020

thk123 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

NlightNFotis left a comment

Choose a reason for hiding this comment

codecov bot commented Jul 3, 2020 • edited Loading

Codecov Report

martin-cs left a comment

Choose a reason for hiding this comment

hannes-steffenhagen-diffblue commented Jul 8, 2020

codecov bot commented Jul 3, 2020 •

edited

Loading