Clean_up related to symex_assign_symbol #4793

romainbrenguier · 2019-06-14T07:28:02Z

There is no functional changes, this is just aimed at making the code a bit simpler

Each commit message has a non-empty body, explaining why the change was made.
[na] Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
[na] 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).
[na] My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
[na] White-space or formatting changes outside the feature-related changed lines are in commits of their own.

allredj

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

codecov-io · 2019-06-14T10:30:51Z

Codecov Report

❗ No coverage uploaded for pull request base (develop@3da291c). Click here to learn what that means.
The diff coverage is 100%.

@@            Coverage Diff             @@
##             develop    #4793   +/-   ##
==========================================
  Coverage           ?   68.65%           
==========================================
  Files              ?     1281           
  Lines              ?   105583           
  Branches           ?        0           
==========================================
  Hits               ?    72492           
  Misses             ?    33091           
  Partials           ?        0

Impacted Files	Coverage Δ
src/goto-symex/goto_symex_state.h	`100% <ø> (ø)`
src/goto-symex/goto_symex_state.cpp	`93.75% <ø> (ø)`
src/goto-symex/ssa_step.h	`92.85% <ø> (ø)`
src/goto-symex/renamed.h	`100% <ø> (ø)`
src/goto-symex/renaming_level.h	`50% <ø> (ø)`
src/util/ssa_expr.h	`100% <ø> (ø)`
src/goto-symex/symex_target_equation.cpp	`95.16% <100%> (ø)`
src/goto-symex/renaming_level.cpp	`91.8% <100%> (ø)`
src/goto-symex/symex_assign.cpp	`85.2% <100%> (ø)`
src/util/ssa_expr.cpp	`87.5% <100%> (ø)`
... and 2 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 3da291c...71caf32. Read the comment docs.

tautschnig · 2019-06-14T14:33:22Z

src/goto-symex/symex_assign.cpp

-    }
-    return state.rename(std::move(guarded_rhs), ns).get();
-  }();
+    guard.empty() ? rhs : (exprt)if_exprt{conjunction(guard), rhs, lhs}, ns)


I'd prefer static_cast<exprt> as the C-style cast is just very easy to overlook.

tautschnig · 2019-06-14T14:35:51Z

src/goto-symex/ssa_step.cpp

@@ -231,7 +230,7 @@ SSA_assignment_stept::SSA_assignment_stept(
  original_full_lhs = std::move(_original_full_lhs);
  ssa_rhs = std::move(_ssa_rhs);
  assignment_type = _assignment_type;
-  cond_expr = std::move(_cond_expr);
+  cond_expr = equal_exprt(ssa_lhs, ssa_rhs);


Nit pick: use curly braces

tautschnig · 2019-06-14T14:37:11Z

src/goto-symex/symex_assign.cpp

-  const exprt assignment_guard =
-    make_and(state.guard.as_expr(), conjunction(guard));
-
-  const exprt original_lhs = get_original_name(l2_full_lhs);
  target.assignment(


Random place: typo in the commit message: "this values" -> "these values", and also it should be "Inline variables" (plural)

tautschnig · 2019-06-14T14:38:23Z

src/goto-symex/goto_state.cpp

  {
-    level2.current_names.insert(l1_identifier, std::make_pair(lhs, n));
+    std::pair<ssa_exprt, unsigned> copy = r_opt->get();
+    copy.second = narrow<unsigned>(n);


Ack, but we should really stop using unsigned, the renaming index ought to be std::size_t.

@tautschnig I added that change in a new commit

tautschnig · 2019-06-14T14:38:56Z

src/goto-symex/goto_symex_state.h

@@ -217,7 +217,7 @@ class goto_symex_statet final : public goto_statet
  unsigned remaining_vccs = 0;

  /// Allocates a fresh L2 name for the given L1 identifier, and makes it the
-  //  latest generation on this path.
+  /// latest generation on this path.


Note on the commit message: that's a "slash", not a "backslash"

This intermediary variable doesn't help understanding and slows down reading the code.

Makes it clearer why it is declared.

ns.lookup doesn't do the assignment

The definition of this reference is not useful.

We can deduce it from the assignment type rather than having to give it to the constructor.

This can be deduced fro lhs and rhs without having to give it to the constructor.

Declaring variables for these values doesn't add clarity and makes the function longer.

Add missing const, necessary narrow and insert if and else to make r_opt scoped to only the if branch.

No functional changes. Necessary for doxygen comment

This is necessary for CI

This avoids some conversions, in particular when assigning from the return value of fresh_l2_name_provider.

allredj

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

romainbrenguier requested review from kroening, peterschrammel, smowton and tautschnig as code owners June 14, 2019 07:28

romainbrenguier force-pushed the clean-up/symex-assign-symbol branch from e856514 to 9f408f3 Compare June 14, 2019 08:24

allredj reviewed Jun 14, 2019

View reviewed changes

owen-mc-diffblue approved these changes Jun 14, 2019

View reviewed changes

peterschrammel approved these changes Jun 14, 2019

View reviewed changes

tautschnig approved these changes Jun 14, 2019

View reviewed changes

tautschnig assigned romainbrenguier Jun 14, 2019

romainbrenguier force-pushed the clean-up/symex-assign-symbol branch 2 times, most recently from 980910b to 5e22d89 Compare June 17, 2019 07:47

romainbrenguier requested a review from pkesseli as a code owner June 17, 2019 07:47

romainbrenguier added 14 commits June 17, 2019 12:02

Inline variable used only once

3d3bbdf

This intermediary variable doesn't help understanding and slows down reading the code.

Simplify assignment of l2_rhs

389df45

Declare variable closer to where it is used

0c068ca

Makes it clearer why it is declared.

Inline variable that is immediately moved

2c5ef55

Remove misleading comment

98e7146

ns.lookup doesn't do the assignment

Inline reference used only once

360eb4a

The definition of this reference is not useful.

Infer hidden field in SSA_assignment_stept

a8af4d3

We can deduce it from the assignment type rather than having to give it to the constructor.

Infer cond_expr in SSA_assignment_step

093ee52

This can be deduced fro lhs and rhs without having to give it to the constructor.

Inline variables used immediatly after

56d7bba

Declaring variables for these values doesn't add clarity and makes the function longer.

Clean-up increase_generation

a97d61e

Add missing const, necessary narrow and insert if and else to make r_opt scoped to only the if branch.

Add missing slash

a577ed2

No functional changes. Necessary for doxygen comment

Document l2_thread_write_encoding

7a8f8c7

Formatting changes suggested by clang-format

3e9c60f

This is necessary for CI

Make index in renamings be of std::size_t type

71caf32

This avoids some conversions, in particular when assigning from the return value of fresh_l2_name_provider.

romainbrenguier force-pushed the clean-up/symex-assign-symbol branch from 5e22d89 to 71caf32 Compare June 17, 2019 11:03

romainbrenguier merged commit 5bd95a7 into diffblue:develop Jun 17, 2019

romainbrenguier deleted the clean-up/symex-assign-symbol branch June 17, 2019 12:45

allredj reviewed Jun 17, 2019

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Clean_up related to symex_assign_symbol #4793

Clean_up related to symex_assign_symbol #4793

Uh oh!

romainbrenguier commented Jun 14, 2019

Uh oh!

allredj left a comment

Uh oh!

codecov-io commented Jun 14, 2019 •

edited

Loading

Uh oh!

tautschnig Jun 14, 2019

Uh oh!

tautschnig Jun 14, 2019

Uh oh!

tautschnig Jun 14, 2019

Uh oh!

tautschnig Jun 14, 2019

Uh oh!

romainbrenguier Jun 17, 2019

Uh oh!

tautschnig Jun 17, 2019

Uh oh!

tautschnig Jun 14, 2019

Uh oh!

allredj left a comment

Uh oh!

Uh oh!

Clean_up related to symex_assign_symbol #4793

Clean_up related to symex_assign_symbol #4793

Uh oh!

Conversation

romainbrenguier commented Jun 14, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

codecov-io commented Jun 14, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

tautschnig Jun 14, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Jun 14, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Jun 14, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Jun 14, 2019

Choose a reason for hiding this comment

Uh oh!

romainbrenguier Jun 17, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Jun 17, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Jun 14, 2019

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

codecov-io commented Jun 14, 2019 •

edited

Loading