Deprecate old instructiont API #4177

kroening · 2019-02-13T12:36:10Z

No change to code, documentation only.

Each commit message has a non-empty body, explaining why the change was made.
n/a 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/
n/a 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).
n/a 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.

tautschnig · 2019-02-13T12:55:47Z

jbmc/src/java_bytecode/remove_instanceof.cpp

@@ -211,7 +211,7 @@ bool remove_instanceoft::lower_instanceof(
    // GOTO programs before the target instruction without inserting into the
    // wrong basic block.
    goto_program.insert_before_swap(target);
-    target->make_skip();
+    *target = goto_programt::make_skip();


Why not turn_into_skip?

It's actually a new instruction; now passing directly to insert_before_swap.

tautschnig · 2019-02-13T12:57:45Z

src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp

@@ -915,7 +914,7 @@ void disjunctive_polynomial_accelerationt::build_fixed()
    if(loop.find(t)==loop.end())
    {
      // This instruction isn't part of the loop...  Just remove it.
-      fixedt->make_skip();
+      *fixedt = goto_programt::make_skip(fixedt->source_location);


turn_into_skip

tautschnig · 2019-02-13T12:58:08Z

src/goto-instrument/accelerate/sat_path_enumerator.cpp

@@ -269,7 +269,7 @@ void sat_path_enumeratort::build_fixed()
    if(loop.find(t)==loop.end())
    {
      // This instruction isn't part of the loop...  Just remove it.
-      fixedt->make_skip();
+      *fixedt = goto_programt::make_skip(fixedt->source_location);


turn_into_skip

tautschnig · 2019-02-13T13:01:01Z

src/goto-instrument/generate_function_bodies.cpp

-    auto add_instruction = [&]() {
-      auto instruction = function.body.add_instruction();
+    auto add_instruction = [&](goto_programt::instructiont &&i) {
+      auto instruction = function.body.add(std::move(i));
      instruction->source_location = function_symbol.location;
      return instruction;
    };


Does this lambda still have any value left in it? The make_* calls would now also take a source location.

tautschnig · 2019-02-13T13:03:47Z

src/goto-instrument/generate_function_bodies.cpp

-    auto add_instruction = [&]() {
-      auto instruction = function.body.add_instruction();
+    auto add_instruction = [&](goto_programt::instructiont &&i) {
+      auto instruction = function.body.add(std::move(i));
      instruction->source_location = function_symbol.location;
      instruction->source_location.set_function(function_name);
      return instruction;
    };


As above: I'm not sure this Lambda adds value. Though there also is #2149...

tautschnig · 2019-02-13T13:11:28Z

unit/goto-programs/goto_program_dead.cpp

-    code_deadt removal(var_a);
-    instructions.back().make_dead();
-    instructions.back().code = removal;
+    instructions.emplace_back(goto_programt::make_dead(var_a));


Could we use add instead so as to avoid use of an implementation detail?

tautschnig · 2019-02-13T13:11:40Z

unit/goto-programs/goto_program_declaration.cpp

-    instructions.emplace_back(goto_program_instruction_typet::DECL);
-    code_declt declaration(var_a);
-    instructions.back().make_decl(declaration);
+    instructions.emplace_back(goto_programt::make_decl(var_a));


As above: use add

tautschnig · 2019-02-13T13:11:59Z

unit/goto-programs/goto_program_goto_target.cpp

@@ -33,11 +33,10 @@ SCENARIO(

    goto_functiont goto_function;
    auto &instructions = goto_function.body.instructions;
-    instructions.emplace_back(goto_program_instruction_typet::ASSERT);
-    instructions.back().make_assertion(x_le_10);
+    instructions.emplace_back(goto_programt::make_assertion(x_le_10));


tautschnig · 2019-02-13T13:12:08Z

unit/goto-programs/goto_program_symbol_type_table_consistency.cpp

@@ -34,8 +34,7 @@ SCENARIO(

    goto_functiont goto_function;
    auto &instructions = goto_function.body.instructions;
-    instructions.emplace_back(goto_program_instruction_typet::ASSERT);
-    instructions.back().make_assertion(x_le_10);
+    instructions.emplace_back(goto_programt::make_assertion(x_le_10));


tautschnig · 2019-02-13T13:12:15Z

unit/goto-programs/goto_program_table_consistency.cpp

@@ -33,8 +33,7 @@ SCENARIO(

    goto_functiont goto_function;
    auto &instructions = goto_function.body.instructions;
-    instructions.emplace_back(goto_program_instruction_typet::ASSERT);
-    instructions.back().make_assertion(x_le_10);
+    instructions.emplace_back(goto_programt::make_assertion(x_le_10));


allredj

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

We now avoid construction followed by overwriting, and construct the final object directly.

kroening · 2019-02-13T16:11:15Z

@tautschnig The lambdas can definitively go away once we're agreed that .function isn't abused any more.

kroening · 2019-02-13T17:48:04Z

(Moving the actual code changes recommended here into a new PR).

allredj

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

kroening added the documentation label Feb 13, 2019

kroening requested review from cesaro, chrisr-diffblue, cristina-david, danpoe, hannes-steffenhagen-diffblue, martin-cs, NathanJPhillips, peterschrammel, pkesseli, smowton, tautschnig and thk123 as code owners February 13, 2019 12:36

tautschnig approved these changes Feb 13, 2019

View reviewed changes

allredj reviewed Feb 13, 2019

View reviewed changes

deprecate old instructiont API

09fde0d

We now avoid construction followed by overwriting, and construct the final object directly.

kroening force-pushed the deprecate_old_instructiont_API branch from 02f68bb to 7d64d7e Compare February 13, 2019 16:02

kroening mentioned this pull request Feb 13, 2019

use make_X API follow-up #4182

Merged

3 tasks

kroening force-pushed the deprecate_old_instructiont_API branch from d449057 to 09fde0d Compare February 13, 2019 17:49

allredj reviewed Feb 13, 2019

View reviewed changes

kroening merged commit c033898 into develop Feb 14, 2019

kroening deleted the deprecate_old_instructiont_API branch February 14, 2019 08:07

Deprecate old instructiont API #4177

Deprecate old instructiont API #4177

Uh oh!

Conversation

kroening commented Feb 13, 2019

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!

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!

kroening commented Feb 13, 2019

Uh oh!

kroening commented Feb 13, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!