Optimize remove_level_2 #3559

romainbrenguier · 2018-12-11T10:43:25Z

Instead of rebuilding the identifier from scratch when we remove the level 2 of the ssa_exprt, we can just strip the suffix, which is more efficient. On benchmarks I ran locally (70 methods from tika) this has improved the execution time of symex by about 8% (from 77.2 sec to 70.8).

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.
[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).
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

No, this would break any work towards field sensitivity, which build_ssa_identifier_rec takes care of.

romainbrenguier · 2018-12-11T12:43:01Z

@tautschnig

No, this would break any work towards field sensitivity, which build_ssa_identifier_rec takes care of.

What is field sensitivity?

tautschnig · 2018-12-11T12:50:28Z

What is field sensitivity?

Cf. #2574: we would treat individual members of structs or arrays as separate entities in the SSA encoding for the purpose of field-level constant propagation and smaller SAT encodings. Especially for Java it should be highly beneficial. @smowton has poked me about it several times...

romainbrenguier · 2018-12-11T12:58:14Z

@tautschnig

Cf. #2574: we would treat individual members of structs or arrays as separate entities in the SSA encoding for the purpose of field-level constant propagation and smaller SAT encodings. Especially for Java it should be highly beneficial. @smowton has poked me about it several times...

It sounds interesting but I'm not sure this would be affected by this PR. I will investigate another way to improve how ssa_exprt's are used in symex.

tautschnig · 2018-12-11T13:02:05Z

It sounds interesting but I'm not sure this would be affected by this PR.

The code in build_ssa_identifier_rec (which update_identifier invokes) would build identifiers like a!0@1#2.some_member for a struct member expression a.some_member. The change that this PR introduces would turn such an expression into a!0@1 upon a call to remove_level_2, when the correct result is [email protected]_member.

allredj

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

romainbrenguier · 2018-12-12T11:27:50Z

@tautschnig I've changed my approach to optimize the function, this version should be cleaner. I've also added a couple of commits to make the interface of these classes clearer.

smowton · 2018-12-12T11:52:13Z

src/util/ssa_expr.cpp

@@ -82,7 +82,7 @@ bool ssa_exprt::can_build_identifier(const exprt &expr)
    return false;


Commit message typo: "and probably shouldn't." -> "and probably shouldn't be part of it."

smowton · 2018-12-12T11:56:01Z

Unless I'm misreading this changes very little? Previously inline functions aren't anymore, a couple of functions are static rather than members, and a single "if-is-ssa-expr" test is eliminated? Not objecting, just checking if something has been missed out in shuffling the commits; it currently looks like a cleanup with perhaps 1% performance impact rather than an optimisation.

romainbrenguier · 2018-12-12T12:48:51Z

@smowton

Unless I'm misreading this changes very little? Previously inline functions aren't anymore, a couple of functions are static rather than members, and a single "if-is-ssa-expr" test is eliminated? Not objecting, just checking if something has been missed out in shuffling the commits; it currently looks like a cleanup with perhaps 1% performance impact rather than an optimisation.

This is mostly true. The essential change is the remove_level_2 simplification. I would expect more than 1% improvement; I will run some benchmarks to confirm that.

romainbrenguier · 2018-12-12T12:56:02Z

I would expect more than 1% improvement; I will run some benchmarks to confirm that.

Yes, a get more than 5% improvement on my benchmarks.

smowton · 2018-12-12T13:25:21Z

Just from removing that check? Impressive!

allredj

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

romainbrenguier · 2018-12-13T08:07:55Z

@smowton

Just from removing that check? Impressive!

It's more than a check because update_identifier is rebuilding the identifier strings from scratch, and it's called very frequently during symex.

romainbrenguier · 2018-12-13T08:08:32Z

@tautschnig are you happy with the changes?

tautschnig

Ok, looks good to me except there may be further room for improvement by dropping one change as noted below.

tautschnig · 2018-12-13T08:24:09Z

src/util/ssa_expr.cpp

@@ -114,5 +114,5 @@ void ssa_exprt::update_identifier()
 void ssa_exprt::remove_level_2()
 {
  remove(ID_L2);
-  update_identifier();
+  set_identifier(get_l1_object_identifier());


With this change: shouldn't you move it back to the header file as now everything can be inlined?

To lighten the header.

This is not used outside of the ssa_exprt class and shouldn't be part of the public interface.

This is only used in one function.

For ssa_exprt's this always remove_level_2

To reset the identifier we can just used the l1_object_identifier which is a cached version of the level1 identifier.

romainbrenguier · 2018-12-13T13:53:44Z

The CI failure is caused by doxygen not being able to be downloaded and installed

allredj

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

romainbrenguier requested review from kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners December 11, 2018 10:43

tautschnig requested changes Dec 11, 2018

View reviewed changes

romainbrenguier force-pushed the optimize/get_l1_name branch from 6e86875 to 4935a90 Compare December 11, 2018 12:45

allredj reviewed Dec 11, 2018

View reviewed changes

romainbrenguier added the do not merge label Dec 11, 2018

romainbrenguier force-pushed the optimize/get_l1_name branch from 4935a90 to bf87ff3 Compare December 12, 2018 11:25

romainbrenguier removed the do not merge label Dec 12, 2018

smowton reviewed Dec 12, 2018

View reviewed changes

romainbrenguier force-pushed the optimize/get_l1_name branch from bf87ff3 to dfd511e Compare December 12, 2018 12:49

smowton approved these changes Dec 12, 2018

View reviewed changes

allredj reviewed Dec 12, 2018

View reviewed changes

allredj approved these changes Dec 12, 2018

View reviewed changes

romainbrenguier force-pushed the optimize/get_l1_name branch from dfd511e to 3f4677f Compare December 13, 2018 08:06

romainbrenguier assigned tautschnig Dec 13, 2018

tautschnig approved these changes Dec 13, 2018

View reviewed changes

romainbrenguier added 6 commits December 13, 2018 11:25

Move update_identifier definition to cpp file

9157f0f

To lighten the header.

Remove build_identifier from the public_interface

5f9fd35

This is not used outside of the ssa_exprt class and shouldn't be part of the public interface.

Document build_ssa_identifier_rec

8bd5402

Hide get_l1_name from interface

75f7c77

This is only used in one function.

Inline get_l1_name

7efc7b8

For ssa_exprt's this always remove_level_2

Optimize remove_level_2

7114c57

To reset the identifier we can just used the l1_object_identifier which is a cached version of the level1 identifier.

romainbrenguier force-pushed the optimize/get_l1_name branch from 3f4677f to 7114c57 Compare December 13, 2018 11:29

romainbrenguier merged commit 58d440a into diffblue:develop Dec 14, 2018

allredj reviewed Dec 14, 2018

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Optimize remove_level_2 #3559

Optimize remove_level_2 #3559

romainbrenguier commented Dec 11, 2018

tautschnig left a comment

romainbrenguier commented Dec 11, 2018

tautschnig commented Dec 11, 2018

romainbrenguier commented Dec 11, 2018

tautschnig commented Dec 11, 2018

allredj left a comment

romainbrenguier commented Dec 12, 2018

smowton Dec 12, 2018

smowton commented Dec 12, 2018

romainbrenguier commented Dec 12, 2018

romainbrenguier commented Dec 12, 2018

smowton commented Dec 12, 2018

allredj left a comment

romainbrenguier commented Dec 13, 2018

romainbrenguier commented Dec 13, 2018

tautschnig left a comment

tautschnig Dec 13, 2018

romainbrenguier commented Dec 13, 2018

allredj left a comment

		@@ -82,7 +82,7 @@ bool ssa_exprt::can_build_identifier(const exprt &expr)
		return false;

Optimize remove_level_2 #3559

Optimize remove_level_2 #3559

Conversation

romainbrenguier commented Dec 11, 2018

tautschnig left a comment

Choose a reason for hiding this comment

romainbrenguier commented Dec 11, 2018

tautschnig commented Dec 11, 2018

romainbrenguier commented Dec 11, 2018

tautschnig commented Dec 11, 2018

allredj left a comment

Choose a reason for hiding this comment

romainbrenguier commented Dec 12, 2018

smowton Dec 12, 2018

Choose a reason for hiding this comment

smowton commented Dec 12, 2018

romainbrenguier commented Dec 12, 2018

romainbrenguier commented Dec 12, 2018

smowton commented Dec 12, 2018

allredj left a comment

Choose a reason for hiding this comment

romainbrenguier commented Dec 13, 2018

romainbrenguier commented Dec 13, 2018

tautschnig left a comment

Choose a reason for hiding this comment

tautschnig Dec 13, 2018

Choose a reason for hiding this comment

romainbrenguier commented Dec 13, 2018

allredj left a comment

Choose a reason for hiding this comment