introduce goto_programt::instructiont::type() and _nonconst() #6412

kroening · 2021-10-22T14:08:48Z

This introduces two methods to read and write the type of a GOTO program
instruction, and replaces various direct accesses.

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-10-22T15:31:58Z

Codecov Report

Merging #6412 (13c2919) into develop (093a216) will increase coverage by 0.00%.
The diff coverage is 84.67%.

@@           Coverage Diff            @@
##           develop    #6412   +/-   ##
========================================
  Coverage    75.98%   75.98%           
========================================
  Files         1524     1524           
  Lines       164242   164241    -1     
========================================
  Hits        124801   124801           
+ Misses       39441    39440    -1

Impacted Files	Coverage Δ
src/analyses/global_may_alias.cpp	`0.00% <0.00%> (ø)`
src/goto-instrument/points_to.cpp	`0.00% <0.00%> (ø)`
src/goto-instrument/uninitialized.cpp	`0.00% <0.00%> (ø)`
src/goto-programs/remove_unused_functions.cpp	`0.00% <0.00%> (ø)`
src/goto-symex/symex_main.cpp	`85.93% <40.00%> (ø)`
src/goto-programs/interpreter.cpp	`51.64% <50.00%> (ø)`
src/goto-programs/goto_program.cpp	`69.74% <75.00%> (ø)`
jbmc/src/java_bytecode/remove_exceptions.cpp	`95.52% <100.00%> (-0.03%)`	⬇️
...rams/remove_virtual_functions_without_fallback.cpp	`98.70% <100.00%> (ø)`
...a_bytecode_instrument/virtual_call_null_checks.cpp	`97.82% <100.00%> (ø)`
... and 37 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 e7eff1e...13c2919. Read the comment docs.

peterschrammel

💡 I think by introducing turn_into_assume (we've already got turn_into_skip), we can do without type_nonconst().

peterschrammel · 2021-10-22T20:23:31Z

src/goto-instrument/uninitialized.cpp

        i1->source_location_nonconst() = instruction.source_location();
        i1->code_nonconst() = code_declt(symbol_expr);

-        i2->type=ASSIGN;
+        i2->type_nonconst() = ASSIGN;


use the 2-param variant of insert_after?

peterschrammel · 2021-10-22T20:23:34Z

src/goto-instrument/uninitialized.cpp

@@ -120,11 +120,11 @@ void uninitializedt::add_assertions(
          id2string(identifier)+"#initialized";

        symbol_exprt symbol_expr(new_identifier, bool_typet());
-        i1->type=DECL;
+        i1->type_nonconst() = DECL;


use the 2-param variant of insert_after?

peterschrammel · 2021-10-22T20:27:18Z

jbmc/src/java_bytecode/remove_exceptions.cpp

@@ -421,7 +421,7 @@ bool remove_exceptionst::instrument_throw(
    exc_thrown,
    typecast_exprt(exc_expr, exc_thrown.type()));
  // now turn the `throw' into `assignment'
-  instr_it->type=ASSIGN;
+  instr_it->type_nonconst() = ASSIGN;


peterschrammel · 2021-10-22T20:27:45Z

src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp

@@ -846,7 +846,7 @@ void disjunctive_polynomial_accelerationt::build_fixed()
  {
    if(instruction.is_assert())
    {
-      instruction.type = ASSUME;
+      instruction.type_nonconst() = ASSUME;


turn_into_assume?

This method turns a GOTO or an ASSERT instruction into an ASSUME with the same condition. This is a common pattern in the code base, and introducing the method enables doing so in a way that is guaranteed to preserve the class invariants.

martin-cs

Seems reasonable.

martin-cs · 2021-10-23T15:57:50Z

src/goto-programs/goto_program.h

+    /// Set the kind of the instruction.
+    /// This method is best avoided to prevent mal-formed instructions.
+    /// Consider using the goto_programt::make_X methods instead.
+    goto_program_instruction_typet &type_nonconst()


As this only has 7 users, would it be better to just refactor those and not have this functionality at all? Alternatively, could this be marked as deprecated?

Aren't we even down to 2 users, one of which can easily be fixed and the other being read_bin_goto_object? I think the latter could be handled by some low-level constructor that likely wants to be private with access only permitted via a friend declaration.

kroening · 2021-10-24T08:38:39Z

I've added turn_into_assume, which removes some usage of type_nonconst().

This introduces two methods to read and write the type of a GOTO program instruction, and replaces various direct accesses.

tautschnig

It would be great to figure out a story for the nonconst case right away.

tautschnig · 2021-10-25T13:52:52Z

unit/goto-programs/structured_trace_util.cpp

  const auto back_edge = add_instruction(back_edge_location, instructions);
-  back_edge->type = GOTO;
+  back_edge->type_nonconst() = GOTO;


Can't we use make_goto for this one?

add_instruction() in that unit test should be replaced altogether, but this goes beyond this PR.

tautschnig · 2021-10-25T13:55:53Z

src/goto-programs/goto_program.h

+    /// Set the kind of the instruction.
+    /// This method is best avoided to prevent mal-formed instructions.
+    /// Consider using the goto_programt::make_X methods instead.
+    goto_program_instruction_typet &type_nonconst()


Aren't we even down to 2 users, one of which can easily be fixed and the other being read_bin_goto_object? I think the latter could be handled by some low-level constructor that likely wants to be private with access only permitted via a friend declaration.

kroening · 2021-10-26T17:31:44Z

Changing read_bin_goto_object is a major rejfactoring of that piece of code; much more involved than the initial scope of the PR. I'd do this separately.

kroening added the cleanup label Oct 22, 2021

kroening force-pushed the instructiont_type branch from 6e560e2 to a116534 Compare October 22, 2021 14:16

kroening marked this pull request as ready for review October 22, 2021 18:59

kroening requested review from chrisr-diffblue, feliperodri, martin-cs, peterschrammel, romainbrenguier, SaswatPadhi and tautschnig as code owners October 22, 2021 18:59

peterschrammel reviewed Oct 22, 2021

View reviewed changes

introduce instructiont::turn_into_assume

f2abcec

This method turns a GOTO or an ASSERT instruction into an ASSUME with the same condition. This is a common pattern in the code base, and introducing the method enables doing so in a way that is guaranteed to preserve the class invariants.

kroening force-pushed the instructiont_type branch from a116534 to 3e5b976 Compare October 23, 2021 14:46

martin-cs approved these changes Oct 23, 2021

View reviewed changes

kroening force-pushed the instructiont_type branch from 3e5b976 to a6255d4 Compare October 24, 2021 08:51

introduce goto_programt::instructiont::type() and _nonconst()

13c2919

This introduces two methods to read and write the type of a GOTO program instruction, and replaces various direct accesses.

kroening force-pushed the instructiont_type branch from a6255d4 to 13c2919 Compare October 24, 2021 16:35

tautschnig reviewed Oct 25, 2021

View reviewed changes

tautschnig assigned tautschnig and kroening Oct 25, 2021

tautschnig approved these changes Oct 26, 2021

View reviewed changes

tautschnig assigned peterschrammel and unassigned tautschnig and kroening Oct 26, 2021

peterschrammel approved these changes Oct 26, 2021

View reviewed changes

peterschrammel assigned kroening and unassigned peterschrammel Oct 26, 2021

kroening merged commit 6351d3a into develop Oct 26, 2021

kroening deleted the instructiont_type branch October 26, 2021 20:21

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

introduce goto_programt::instructiont::type() and _nonconst() #6412

introduce goto_programt::instructiont::type() and _nonconst() #6412

Uh oh!

kroening commented Oct 22, 2021

Uh oh!

codecov bot commented Oct 22, 2021 •

edited

Loading

Uh oh!

peterschrammel left a comment

Uh oh!

peterschrammel Oct 22, 2021

Uh oh!

peterschrammel Oct 22, 2021

Uh oh!

peterschrammel Oct 22, 2021

Uh oh!

peterschrammel Oct 22, 2021

Uh oh!

martin-cs left a comment

Uh oh!

martin-cs Oct 23, 2021

Uh oh!

tautschnig Oct 25, 2021

Uh oh!

kroening commented Oct 24, 2021

Uh oh!

tautschnig left a comment

Uh oh!

tautschnig Oct 25, 2021

Uh oh!

kroening Oct 26, 2021

Uh oh!

tautschnig Oct 25, 2021

Uh oh!

kroening commented Oct 26, 2021

Uh oh!

Uh oh!

introduce goto_programt::instructiont::type() and _nonconst() #6412

introduce goto_programt::instructiont::type() and _nonconst() #6412

Uh oh!

Conversation

kroening commented Oct 22, 2021

Uh oh!

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

Uh oh!

Codecov Report

Uh oh!

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

martin-cs 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!

kroening commented Oct 24, 2021

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!

kroening commented Oct 26, 2021

Uh oh!

Uh oh!

codecov bot commented Oct 22, 2021 •

edited

Loading