Replace all uses of deprecated symbol_exprt constructors [blocks: #3768] #3766

tautschnig · 2019-01-11T17:14:31Z

This helps type safety has it avoids constructing symbol_exprts that never get
a proper type (or identifier).

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/
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.

allredj

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

kroening · 2019-01-12T09:06:29Z

jbmc/src/java_bytecode/simple_method_stubbing.cpp

@@ -170,7 +170,8 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol)
      symbol_table);
    const symbol_exprt &init_symbol_expression = init_symbol.symbol_expr();
    code_assignt get_argument(
-      init_symbol_expression, symbol_exprt(this_argument.get_identifier()));
+      init_symbol_expression,
+      symbol_exprt(this_argument.get_identifier(), this_argument.type()));
    get_argument.add_source_location() = synthesized_source_location;


This one does appear to be a bugfix!

Yes, but it should actually get merged via #3747, I'll then rebase this PR on top of it.

kroening · 2019-01-12T09:07:21Z

jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp

@@ -215,7 +215,7 @@ SCENARIO("instantiate_not_contains",
        simplify(sc.premise, empty_ns);
        simplify(sc.s0, empty_ns);
        simplify(sc.s1, empty_ns);
-        witnesses[sc] = generator.fresh_symbol("w", t.witness_type());
+        witnesses.emplace(sc, generator.fresh_symbol("w", t.witness_type()));
        nc_axioms.push_back(sc);


Not sure that the .emplace adds a lot here (exprt is very cheap to construct).

The .emplace is necessary, because a symbol_exprt cannot be default constructed.

kroening · 2019-01-12T09:09:35Z

src/analyses/locals.cpp

-      symbol_exprt(param.get_identifier(), param.type());
+    locals_map.emplace(
+      param.get_identifier(),
+      symbol_exprt(param.get_identifier(), param.type()));
 }


kroening · 2019-01-12T09:32:42Z

src/goto-instrument/concurrency.cpp

@@ -58,14 +58,14 @@ class concurrency_instrumentationt
  {
  public:
    typet type;
-    symbol_exprt array_symbol, w_index_symbol;
+    exprt array_symbol, w_index_symbol;
  };


Can these ever be something that's not a symbol_exprt?
If initialisation is delayed, then perhaps optionalt<symbol_exprt> is the right way to say that.

Well, the code is not particularly complete. These are actually never set at the moment.

kroening · 2019-01-12T09:36:11Z

src/goto-symex/symex_function_call.cpp

@@ -409,7 +409,7 @@ void goto_symext::locality(

    if(c_it != state.level1.current_names.end())
    {
-      frame.old_level1[l0_name]=c_it->second;
+      frame.old_level1.emplace(l0_name, c_it->second);
      c_it->second = std::make_pair(ssa, frame_nr);


kroening · 2019-01-12T09:41:59Z

src/util/ssa_expr.h

  /// Constructor
  /// \param expr: Expression to be converted to SSA symbol
-  explicit ssa_exprt(const exprt &expr):
-    symbol_exprt(expr.type())
+  explicit ssa_exprt(const exprt &expr) : symbol_exprt(ID_nil, expr.type())
  {


This is the first time you've used the nil ID -- before it has been the empty one.
If you are concerned about any time taken to convert "" into an irep_idt, then use irep_idt().

Now using irep_idt() here.

Use optionalt<symbol_exprt> when it isn't always set [blocks: #3766]

…ation Use consistent types with function_application_exprt [blocks: #3766]

tautschnig · 2019-01-22T08:09:26Z

This PR now only has a single commit left, (re-)reviews would be appreciated.

allredj

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

allredj

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

martin-cs

The bits that touch my areas of responsibility seem fine.

martin-cs · 2019-01-28T15:33:23Z

src/solvers/smt2/smt2_parser.h

+      : term(_term), name(_name)
+    {
+    }
+


+1 this is not clear.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: d16fbeb).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98896786
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

This helps type safety has it avoids constructing symbol_exprts that never get a proper type (or identifier).

allredj

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

tautschnig added the cleanup label Jan 11, 2019

tautschnig self-assigned this Jan 11, 2019

tautschnig requested review from allredj, cesaro, chrisr-diffblue, cristina-david, kroening, martin-cs, NathanJPhillips, peterschrammel, pkesseli, romainbrenguier, smowton and thk123 as code owners January 11, 2019 17:14

tautschnig force-pushed the remove-deprecated-symbol-exprt-constructors branch from 538612f to 4269207 Compare January 11, 2019 17:27

tautschnig removed their assignment Jan 11, 2019

tautschnig force-pushed the remove-deprecated-symbol-exprt-constructors branch from 4269207 to 115efb3 Compare January 11, 2019 19:40

allredj reviewed Jan 11, 2019

View reviewed changes

kroening reviewed Jan 12, 2019

View reviewed changes

kroening approved these changes Jan 12, 2019

View reviewed changes

tautschnig force-pushed the remove-deprecated-symbol-exprt-constructors branch from 115efb3 to 2a5c14a Compare January 14, 2019 17:07

tautschnig changed the title ~~Replace all uses of deprecated symbol_exprt constructors~~ Replace all uses of deprecated symbol_exprt constructors [depends-on: #3474] Jan 14, 2019

tautschnig added the dependent - do not merge label Jan 14, 2019

tautschnig self-assigned this Jan 14, 2019

tautschnig changed the title ~~Replace all uses of deprecated symbol_exprt constructors [depends-on: #3474]~~ Replace all uses of deprecated symbol_exprt constructors [depends-on: #3747] Jan 14, 2019

tautschnig added a commit that referenced this pull request Jan 22, 2019

Merge pull request #3874 from tautschnig/symbol_exprt-optional

7c844fb

Use optionalt<symbol_exprt> when it isn't always set [blocks: #3766]

tautschnig added a commit that referenced this pull request Jan 22, 2019

Merge pull request #3872 from tautschnig/symbol_exprt-function_applic…

adb3d7b

…ation Use consistent types with function_application_exprt [blocks: #3766]

tautschnig force-pushed the remove-deprecated-symbol-exprt-constructors branch from 272b62c to 7c9aaff Compare January 22, 2019 08:08

tautschnig removed the dependent - do not merge label Jan 22, 2019

tautschnig removed their assignment Jan 22, 2019

tautschnig changed the title ~~Replace all uses of deprecated symbol_exprt constructors [depends-on: #3870, blocks: #3768]~~ Replace all uses of deprecated symbol_exprt constructors [blocks: #3768] Jan 22, 2019

smowton approved these changes Jan 22, 2019

View reviewed changes

tautschnig force-pushed the remove-deprecated-symbol-exprt-constructors branch from 7c9aaff to 697a744 Compare January 22, 2019 13:00

tautschnig assigned peterschrammel, martin-cs and chrisr-diffblue Jan 22, 2019

tautschnig force-pushed the remove-deprecated-symbol-exprt-constructors branch from 697a744 to c539028 Compare January 23, 2019 14:01

allredj reviewed Jan 23, 2019

View reviewed changes

tautschnig force-pushed the remove-deprecated-symbol-exprt-constructors branch from c539028 to 45c74ce Compare January 26, 2019 13:17

allredj reviewed Jan 26, 2019

View reviewed changes

martin-cs approved these changes Jan 28, 2019

View reviewed changes

src/solvers/smt2/smt2_parser.h

: term(_term), name(_name)

{

}

Copy link

Collaborator

martin-cs Jan 28, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

+1 this is not clear.

tautschnig force-pushed the remove-deprecated-symbol-exprt-constructors branch from 45c74ce to 8bea959 Compare January 28, 2019 16:31

peterschrammel approved these changes Jan 28, 2019

View reviewed changes

peterschrammel assigned tautschnig and unassigned peterschrammel Jan 28, 2019

tautschnig force-pushed the remove-deprecated-symbol-exprt-constructors branch from 8bea959 to d16fbeb Compare January 28, 2019 23:12

allredj reviewed Jan 29, 2019

View reviewed changes

tautschnig unassigned martin-cs and chrisr-diffblue Jan 29, 2019

Replace all uses of deprecated symbol_exprt constructors

267094c

This helps type safety has it avoids constructing symbol_exprts that never get a proper type (or identifier).

tautschnig force-pushed the remove-deprecated-symbol-exprt-constructors branch from d16fbeb to 267094c Compare January 29, 2019 18:23

allredj reviewed Jan 30, 2019

View reviewed changes

tautschnig merged commit c2e3503 into diffblue:develop Jan 30, 2019

tautschnig deleted the remove-deprecated-symbol-exprt-constructors branch January 30, 2019 08:28

Replace all uses of deprecated symbol_exprt constructors [blocks: #3768] #3766

Replace all uses of deprecated symbol_exprt constructors [blocks: #3768] #3766

Uh oh!

Conversation

tautschnig commented Jan 11, 2019

Uh oh!

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

tautschnig commented Jan 22, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!