Clean-up and document symex_function_call [DOC-150] #4080

romainbrenguier · 2019-02-05T13:52:43Z

Make a couple of functions static and add documentation where missing.

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.

tautschnig

Could "Move and make static symex_end_of_function" please be skipped? If we go this route, we will eventually have a single file containing all source code.

romainbrenguier · 2019-02-05T14:47:19Z

@tautschnig

If we go this route, we will eventually have a single file containing all source code.

That would be better because more efficient.
More seriously, I think the better way to avoid having all the code in one file would be to split goto_symex in several smaller meaningful classes with their own header. I find having several cpp file for the same header confusing, and I'm not sure of the advantage.

allredj

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

tautschnig · 2019-02-05T15:02:53Z

More seriously, I think the better way to avoid having all the code in one file would be to split goto_symex in several smaller meaningful classes with their own header. I find having several cpp file for the same header confusing, and I'm not sure of the advantage.

Fully agreed, just the other day I had to make some changes in src/solvers/strings/... But then at least the existing cpp files are a starting point and really just the classes should be added in.

romainbrenguier · 2019-02-05T15:13:40Z

@tautschnig

But then at least the existing cpp files are a starting point and really just the classes should be added in.

Yes, so I don't see the problem with that particular commit, since it's reducing the dependencies between different cpp files, it will make it a little bit easier.

tautschnig · 2019-02-05T15:21:51Z

I don't see the problem with that particular commit

It's moving code that is entirely specific to dealing with function calls to symex_main from symex_function_call.

romainbrenguier · 2019-02-05T15:47:16Z

It's moving code that is entirely specific to dealing with function calls to symex_main from symex_function_call.

OK, I see the point and will drop it. I still think grouping function_call and end_function is artificial since they don't depend on each other, but refactoring goto_symext can wait a bit.

tautschnig · 2019-02-05T15:55:23Z

I still think grouping function_call and end_function is artificial since they don't depend on each other, [...]

This may be true as far as compiling code is concerned, but at a more abstract level end_function needs to be consistent with what function_call does, e.g., in terms of setting up frames. It's actually bad that there is no dependency, because it means it's all down to humans checking consistency.

tautschnig · 2019-02-05T15:56:33Z

src/goto-symex/goto_symex.h

@@ -271,25 +271,41 @@ class goto_symext

  virtual void loop_bound_exceeded(statet &, const exprt &guard);

-  // function calls
+  /// Assuming \p state is currently pointing on a return instruction, assign


The state doesn't point, maybe the program counter inside it?

tautschnig · 2019-02-05T15:57:28Z

src/goto-symex/goto_symex.h

@@ -271,25 +271,41 @@ class goto_symext

  virtual void loop_bound_exceeded(statet &, const exprt &guard);

-  // function calls
+  /// Assuming \p state is currently pointing on a return instruction, assign
+  /// the value in that return to the top frame's \p return_value field.
  void return_assignment(statet &);


Is this actually dead code? return-value removal should render it such.

Indeed it looks like it, I've added a commit to replace the call to this by an UNREACHABLE

tautschnig · 2019-02-05T15:59:37Z

src/goto-symex/goto_symex.h

@@ -300,6 +316,12 @@ class goto_symext
    unsigned thread_nr,
    unsigned unwind);

+  /// Iterates over \p arguments and assign them to the parameters, which are


tautschnig · 2019-02-05T15:59:52Z

src/goto-symex/goto_symex.h

@@ -300,6 +316,12 @@ class goto_symext
    unsigned thread_nr,
    unsigned unwind);

+  /// Iterates over \p arguments and assign them to the parameters, which are
+  /// symbols whose name and type are deduce from the type of \p goto_function.


allredj

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

allredj

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

romainbrenguier · 2019-02-06T09:59:34Z

@peterschrammel this is ready for review

peterschrammel · 2019-02-07T15:27:33Z

src/goto-symex/goto_symex.h

  virtual void no_body(const irep_idt &)
  {
  }

+  /// Symbolic execution of a function call.
+  /// Only functions that are symbols are supported, see
+  /// \link goto_symext::symex_function_call_symbol \endlink


\ref doesn't work here?

This function is only used within the same cpp file. Making it static simplifies the global interface and is potentially more efficient.

locality is only used in symex_function_call.cpp, it can be made static. This simplifies the symex interface and is potentially more efficient.

This documents (mostly in goto_symex.h) functions that are defined in symex_function_call.cpp.

The return instructions should have been removed by return-value removal, so they should not reach symex. We replace this case by an unreachable statement and remove the method that is now unused.

allredj

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

romainbrenguier requested review from kroening, peterschrammel and tautschnig as code owners February 5, 2019 13:52

tautschnig requested changes Feb 5, 2019

View reviewed changes

allredj reviewed Feb 5, 2019

View reviewed changes

tautschnig assigned romainbrenguier Feb 5, 2019

romainbrenguier force-pushed the doc/symex-function-call branch from 13ce1de to f7d8891 Compare February 5, 2019 15:42

tautschnig approved these changes Feb 5, 2019

View reviewed changes

peterschrammel added the documentation label Feb 5, 2019

allredj reviewed Feb 5, 2019

View reviewed changes

romainbrenguier force-pushed the doc/symex-function-call branch 2 times, most recently from 6dcf197 to 16c8165 Compare February 6, 2019 07:58

allredj reviewed Feb 6, 2019

View reviewed changes

tautschnig assigned peterschrammel and unassigned romainbrenguier Feb 6, 2019

peterschrammel approved these changes Feb 7, 2019

View reviewed changes

peterschrammel added the cleanup label Feb 7, 2019

romainbrenguier added 4 commits February 7, 2019 15:50

Make pop_frame static

b5986a7

This function is only used within the same cpp file. Making it static simplifies the global interface and is potentially more efficient.

Make locality a static function

1f6ca60

locality is only used in symex_function_call.cpp, it can be made static. This simplifies the symex interface and is potentially more efficient.

Document symex_function_call functions

afc4663

This documents (mostly in goto_symex.h) functions that are defined in symex_function_call.cpp.

Remove unused case of return assignment in symex

7dc47a4

The return instructions should have been removed by return-value removal, so they should not reach symex. We replace this case by an unreachable statement and remove the method that is now unused.

romainbrenguier force-pushed the doc/symex-function-call branch from 16c8165 to 7dc47a4 Compare February 7, 2019 15:50

allredj reviewed Feb 7, 2019

View reviewed changes

peterschrammel assigned romainbrenguier and unassigned peterschrammel Feb 7, 2019

romainbrenguier merged commit 58b5de0 into diffblue:develop Feb 7, 2019

romainbrenguier deleted the doc/symex-function-call branch February 7, 2019 18:17

Clean-up and document symex_function_call [DOC-150] #4080

Clean-up and document symex_function_call [DOC-150] #4080

Uh oh!

Conversation

romainbrenguier commented Feb 5, 2019

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

romainbrenguier commented Feb 5, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Feb 5, 2019

Uh oh!

romainbrenguier commented Feb 5, 2019

Uh oh!

tautschnig commented Feb 5, 2019

Uh oh!

romainbrenguier commented Feb 5, 2019

Uh oh!

tautschnig commented Feb 5, 2019

Uh oh!

tautschnig Feb 5, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Feb 5, 2019

Choose a reason for hiding this comment

Uh oh!

romainbrenguier Feb 6, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Feb 5, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Feb 5, 2019

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!

romainbrenguier commented Feb 6, 2019

Uh oh!

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