Use type equality, not base_type_eq in local safe pointers #4164

tautschnig · 2019-02-12T08:25:27Z

We no longer need to resort to tag/symbol type resolution. This enables partial
revert of 959c7a5 (Bugfix: Maintain safe_pointers per-path) as we no
longer need to maintain a namespacet in local_safe_pointerst. On SV-COMP's
ReachSafety-ECA, copying safe_pointers accounted for 14% of the time spent in
goto_symext::symex_goto (715 of 5119 seconds).

~~Requires #3966 to be merged for Java tests to pass.~~

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

smowton

When tests pass, of course. Thanks for removing the pointless copying of local_safe_pointers, I'd been meaning to fix that!

thk123

Don't see anything blocking in this PR - though seems like quite a lot tangled up into one commit which made this a little difficult to review.

thk123 · 2019-02-12T11:07:07Z

src/goto-symex/symex_function_call.cpp

@@ -240,7 +240,7 @@ void goto_symext::symex_function_call_code(
  state.dirty.populate_dirty_for_function(identifier, goto_function);

  auto emplace_safe_pointers_result =
-    state.safe_pointers.emplace(identifier, local_safe_pointerst{ns});
+    path_storage.safe_pointers.emplace(identifier, local_safe_pointerst{});


⛏️ AFAICT this variable renaming should be done in a seperate commit, ideally with an explanation of why this name is more accurate (I don't know this code well enough to comment on whether this is a good renaming or not). 🕊️

Ah, no, this isn't variable renaming, it's an ownership change. safe_pointers used to belong to goto_symex_statet, but is now moved to path_storaget.

thk123 · 2019-02-12T11:07:21Z

src/goto-symex/symex_main.cpp

@@ -178,7 +178,7 @@ void goto_symext::initialize_entry_point(
  state.top().hidden_function = entry_point_function.is_hidden();

  auto emplace_safe_pointers_result =
-    state.safe_pointers.emplace(function_id, local_safe_pointerst{ns});
+    path_storage.safe_pointers.emplace(function_id, local_safe_pointerst{});


⛏️ 🕊️

thk123 · 2019-02-12T11:08:30Z

src/goto-symex/path_storage.h

@@ -90,6 +92,8 @@ class path_storaget
  /// Counter for nondet objects, which require unique names
  symex_nondet_generatort build_symex_nondet;

+  std::unordered_map<irep_idt, local_safe_pointerst> safe_pointers;


⛏️ You might choose to doxygen this variable, safe_pointers doesn't mean mich to me, but perhaps just a reference to a definition of a "safe pointer" would be a good addition here.

Documentation added.

thk123 · 2019-02-12T11:08:48Z

src/goto-symex/symex_dereference.cpp

-        expr_is_not_null =
-          state.safe_pointers.at(expr_function).is_safe_dereference(
-            to_check, state.source.pc);
+        expr_is_not_null = path_storage.safe_pointers.at(expr_function)


thk123 · 2019-02-12T11:13:43Z

src/analyses/local_safe_pointers.h

-  /// their subexpressions, are identical except that one may use a symbol_typet
-  /// while the other uses that type's expanded (namespacet::follow'd) form.
-  class base_type_comparet
+  class type_comparet


❓ Does this class even need to exist? Except the ordering is on the exprs, unless the types match - this is somewhat surprising. Out of scope of this PR, but I wonder if this is really what's needed here...

It now still is a class, but with a near-trivial inline implementation of the comparison. What approach other than a class would you have thought of?

thk123 · 2019-02-12T11:14:50Z

src/goto-symex/goto_symex_state.h

@@ -317,7 +315,6 @@ inline goto_statet::goto_statet(const class goto_symex_statet &s)
    source(s.source),
    propagation(s.propagation),
    atomic_section_id(s.atomic_section_id),
-    safe_pointers(s.safe_pointers),


⛏️ Ideally this removal would have gone in a different commit with an explanation of why not required.

This PR is now composed of three commits:

Removing the base_type_eq comparison from local_safe_pointerst.

Small bits of cleanup in local_safe_pointerst.

Moving the storage from goto_symex_statet to path_storaget.

…ming Reinstate limited symex renaming [blocks: #4164]

allredj

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

We no longer need to resort to tag/symbol type resolution.

1) Inline (now trivial) comparision function. 2) Use skip_typecast.

As local_safe_pointerst no longer needs a namespace we can do a partial revert of 959c7a5 (Bugfix: Maintain safe_pointers per-path). On SV-COMP's ReachSafety-ECA, copying safe_pointers accounted for 14% of the time spent in goto_symext::symex_goto (715 of 5119 seconds).

allredj

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

tautschnig added Performance Optimisations dependent - do not merge labels Feb 12, 2019

tautschnig requested review from chrisr-diffblue, danpoe, hannes-steffenhagen-diffblue, kroening, martin-cs, peterschrammel, smowton and thk123 as code owners February 12, 2019 08:25

smowton approved these changes Feb 12, 2019

View reviewed changes

thk123 approved these changes Feb 12, 2019

View reviewed changes

tautschnig self-assigned this Feb 12, 2019

smowton added a commit that referenced this pull request Feb 12, 2019

Merge pull request #3966 from tautschnig/reinstate-limited-symex-rena…

b43753a

…ming Reinstate limited symex renaming [blocks: #4164]

tautschnig force-pushed the opt-local-safe-pointers branch from e9755ae to 393da45 Compare February 12, 2019 16:04

tautschnig assigned peterschrammel, danpoe, chrisr-diffblue and hannes-steffenhagen-diffblue and unassigned tautschnig Feb 12, 2019

tautschnig added cleanup and removed dependent - do not merge labels Feb 12, 2019

tautschnig changed the title ~~Use type equality, not base_type_eq in local safe pointers [depends-on: #3966]~~ Use type equality, not base_type_eq in local safe pointers Feb 12, 2019

allredj reviewed Feb 12, 2019

View reviewed changes

tautschnig added 3 commits February 13, 2019 15:49

Use type equality, not base_type_eq in local safe pointers

d9cd00f

We no longer need to resort to tag/symbol type resolution.

Code cleanup in local_safe_pointers

d16c097

1) Inline (now trivial) comparision function. 2) Use skip_typecast.

tautschnig force-pushed the opt-local-safe-pointers branch from 393da45 to e1bfc15 Compare February 13, 2019 15:50

allredj reviewed Feb 13, 2019

View reviewed changes

chrisr-diffblue approved these changes Feb 28, 2019

View reviewed changes

chrisr-diffblue assigned kroening and unassigned chrisr-diffblue Feb 28, 2019

tautschnig unassigned danpoe and hannes-steffenhagen-diffblue Feb 28, 2019

peterschrammel approved these changes Feb 28, 2019

View reviewed changes

kroening merged commit fe75b71 into diffblue:develop Feb 28, 2019

tautschnig deleted the opt-local-safe-pointers branch March 1, 2019 08:05

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Use type equality, not base_type_eq in local safe pointers #4164

Use type equality, not base_type_eq in local safe pointers #4164

Uh oh!

tautschnig commented Feb 12, 2019 •

edited

Loading

Uh oh!

smowton left a comment

Uh oh!

thk123 left a comment

Uh oh!

thk123 Feb 12, 2019

Uh oh!

tautschnig Feb 12, 2019

Uh oh!

thk123 Feb 12, 2019

Uh oh!

thk123 Feb 12, 2019

Uh oh!

tautschnig Feb 12, 2019

Uh oh!

thk123 Feb 12, 2019

Uh oh!

thk123 Feb 12, 2019

Uh oh!

tautschnig Feb 12, 2019

Uh oh!

thk123 Feb 12, 2019

Uh oh!

tautschnig Feb 12, 2019

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

Uh oh!

Use type equality, not base_type_eq in local safe pointers #4164

Use type equality, not base_type_eq in local safe pointers #4164

Uh oh!

Conversation

tautschnig commented Feb 12, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

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

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!

tautschnig commented Feb 12, 2019 •

edited

Loading