protect instructiont::code #5908

kroening · 2021-03-10T15:34:16Z

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.
n/a 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).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

codecov · 2021-03-10T17:32:45Z

Codecov Report

Merging #5908 (99afbae) into develop (76ad937) will increase coverage by 0.00%.
The diff coverage is 70.64%.

@@           Coverage Diff            @@
##           develop    #5908   +/-   ##
========================================
  Coverage    73.54%   73.55%           
========================================
  Files         1431     1431           
  Lines       155229   155245   +16     
========================================
+ Hits        114163   114188   +25     
+ Misses       41066    41057    -9

Impacted Files	Coverage Δ
src/analyses/cfg_dominators.h	`100.00% <ø> (ø)`
src/analyses/global_may_alias.cpp	`0.00% <0.00%> (ø)`
src/goto-cc/linker_script_merge.cpp	`0.00% <0.00%> (ø)`
.../goto-instrument/accelerate/acceleration_utils.cpp	`2.27% <0.00%> (ø)`
...o-instrument/accelerate/polynomial_accelerator.cpp	`0.00% <0.00%> (ø)`
src/goto-instrument/concurrency.cpp	`0.00% <0.00%> (ø)`
src/goto-instrument/dot.cpp	`0.00% <0.00%> (ø)`
src/goto-instrument/function_modifies.cpp	`0.00% <0.00%> (ø)`
src/goto-instrument/rw_set.cpp	`0.00% <0.00%> (ø)`
src/goto-instrument/thread_instrumentation.cpp	`0.00% <0.00%> (ø)`
... and 82 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 e0a6f44...99afbae. Read the comment docs.

tautschnig

I am aware that quite a few of my comments amount to shooting-the-messenger, but I really think we need to use this opportunity to fix the code.

tautschnig · 2021-03-14T21:58:36Z

jbmc/src/java_bytecode/remove_exceptions.cpp

  instr_it->type=ASSIGN;
-  instr_it->code=assignment;
+  instr_it->code_nonconst() = assignment;


Couldn't we instead replace the entire instruction here?

tautschnig · 2021-03-14T22:01:02Z

jbmc/src/java_bytecode/convert_java_nondet.cpp

@@ -93,7 +93,7 @@ static std::pair<goto_programt::targett, bool> insert_nondet_init_code(
  // We only expect to find nondets in the rhs of an assignments, and in return
  // statements if remove_returns has not been run, but we do a more general
  // check on all operands in case this changes
-  for(exprt &op : target->code.operands())
+  for(exprt &op : target->code_nonconst().operands())


I believe this should be replaced by a call to instructiont::transform.

tautschnig · 2021-03-14T22:01:52Z

jbmc/src/java_bytecode/remove_instanceof.cpp

+  if(
+    target->is_target() && (contains_instanceof(target->get_code()) ||
+                            contains_instanceof(target->guard)))


I believe this should be handled via instructiont::transform.

tautschnig · 2021-03-14T22:03:36Z

jbmc/src/java_bytecode/replace_java_nondet.cpp

+    target_instruction->code_nonconst() = code_returnt(inserted_expr);
+    target_instruction->code_nonconst().add_source_location() =
      target_instruction->source_location;


Why did we ever need to replace the entire code - wouldn't the return_value() suffice?

tautschnig · 2021-03-14T22:04:23Z

jbmc/src/java_bytecode/replace_java_nondet.cpp

+    target_instruction->code_nonconst() =
+      code_assignt(nondet_var, inserted_expr);
+    target_instruction->code_nonconst().add_source_location() =
      target_instruction->source_location;


Just like the above: it's an ASSIGN instruction already, don't we just need to replace lhs/rhs here?

tautschnig · 2021-03-14T22:26:52Z

src/goto-programs/label_function_pointer_call_sites.cpp

@@ -61,7 +61,7 @@ void label_function_pointer_call_sites(goto_modelt &goto_model)

        goto_function.second.body.insert_before_swap(it, assign_instruction);
        const auto next = std::next(it);
-        to_code_function_call(next->code).function() =
+        to_code_function_call(next->code_nonconst()).function() =


Use set_function_call

tautschnig · 2021-03-14T22:27:05Z

src/goto-programs/link_goto_model.cpp

@@ -36,7 +36,7 @@ static void rename_symbols_in_function(

  for(auto &instruction : function.body.instructions)
  {
-    rename_symbol(instruction.code);
+    rename_symbol(instruction.code_nonconst());


Use instructiont::transform

tautschnig · 2021-03-14T22:27:58Z

src/goto-programs/string_abstraction.cpp

  }

  {
    goto_programt::targett assignment = tmp.add(goto_programt::make_assignment(
      member(lhs, whatt::SIZE),
      member(rhs, whatt::SIZE),
      target->source_location));
-    assignment->code.add_source_location()=target->source_location;
+    assignment->code_nonconst().add_source_location() = target->source_location;


This line should not be necessary.

tautschnig · 2021-03-14T22:28:03Z

src/goto-programs/string_abstraction.cpp

  }

  {
    goto_programt::targett assignment = tmp.add(goto_programt::make_assignment(
      member(lhs, whatt::LENGTH),
      member(rhs, whatt::LENGTH),
      target->source_location));
-    assignment->code.add_source_location()=target->source_location;
+    assignment->code_nonconst().add_source_location() = target->source_location;


This line should not be necessary.

tautschnig · 2021-03-14T22:29:29Z

src/goto-programs/string_instrumentation.cpp

@@ -882,5 +882,5 @@ void string_instrumentationt::invalidate_buffer(
  const side_effect_expr_nondett nondet(
    buf_type.subtype(), target->source_location);

-  invalidate->code=code_assignt(deref, nondet);
+  invalidate->code_nonconst() = code_assignt(deref, nondet);


Use set_assign

kroening · 2021-03-15T08:03:51Z

The suggested changes are all agreed -- but should come as a separate PR, to keep this reviewable.

tautschnig

Approving under the assumption that the follow-up PR will be created that cleans up most (all?) uses of code_nonconst() as suggested in my earlier comments.

This replaces direct access to instructiont::code to the provided API for the case of assignment and function call instructions.

This PR is a step towards removing direct access to instructiont::code, with the long-term goal of removing the use of codet expressions in goto programs.

kroening added the cleanup label Mar 10, 2021

kroening force-pushed the code_nonconst branch from 6a5524f to 6ed9406 Compare March 10, 2021 16:13

kroening marked this pull request as ready for review March 14, 2021 21:42

kroening requested review from chrisr-diffblue, hannes-steffenhagen-diffblue, martin-cs, peterschrammel, romainbrenguier, smowton and tautschnig as code owners March 14, 2021 21:42

tautschnig reviewed Mar 14, 2021

View reviewed changes

tautschnig assigned kroening Mar 14, 2021

tautschnig approved these changes Mar 15, 2021

View reviewed changes

use instructiont::get_function_call() and get_assign()

03eecc2

This replaces direct access to instructiont::code to the provided API for the case of assignment and function call instructions.

peterschrammel approved these changes Mar 15, 2021

View reviewed changes

protect instructiont::code

99afbae

This PR is a step towards removing direct access to instructiont::code, with the long-term goal of removing the use of codet expressions in goto programs.

kroening force-pushed the code_nonconst branch from 6ed9406 to 99afbae Compare March 15, 2021 10:10

kroening merged commit 1ea6f18 into develop Mar 15, 2021

kroening deleted the code_nonconst branch March 15, 2021 11:48

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

protect instructiont::code #5908

protect instructiont::code #5908

Uh oh!

kroening commented Mar 10, 2021

Uh oh!

codecov bot commented Mar 10, 2021 •

edited

Loading

Uh oh!

tautschnig left a comment

Uh oh!

tautschnig Mar 14, 2021

Uh oh!

tautschnig Mar 14, 2021

Uh oh!

tautschnig Mar 14, 2021

Uh oh!

tautschnig Mar 14, 2021

Uh oh!

tautschnig Mar 14, 2021

Uh oh!

tautschnig Mar 14, 2021

Uh oh!

tautschnig Mar 14, 2021

Uh oh!

tautschnig Mar 14, 2021

Uh oh!

tautschnig Mar 14, 2021

Uh oh!

tautschnig Mar 14, 2021

Uh oh!

kroening commented Mar 15, 2021

Uh oh!

tautschnig left a comment

Uh oh!

Uh oh!

protect instructiont::code #5908

protect instructiont::code #5908

Uh oh!

Conversation

kroening commented Mar 10, 2021

Uh oh!

codecov bot commented Mar 10, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

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

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

kroening commented Mar 15, 2021

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

codecov bot commented Mar 10, 2021 •

edited

Loading