Use let-expression for dereferenced pointers #4576

smowton · 2019-04-26T17:17:41Z

~~Depends on #4574 and #4575.~~ Since #4555 didn't really work out, here's my second stab at avoiding producing comically large expressions during nested dereferencing.

In brief, if we have **p where p is the root of a binary tree with nodes L, R, LL, LR, RL, RR, then instead of *p -> p == &L ? L : R and then **p -> (p == &L ? L : R) == LL ? LL : (p == &L ? L : R) == LR ? LR : ... instead we get let derefd = (p == &L ? L : R) in derefd == LL ? LL : derefd = LR ? LR : .... When we have a large alias set this avoids creating many duplicates of the inner dereference result.

Anecdotally this speeds up a nested deref due to a two-dimensional array from "practically forever" to "around a second".

~~Putting up now for early review, but known TODOs:~~

~~Data~~
~~Check whether the assignments associated with a let expression's temporary variable ought to be STATE or HIDDEN assignments.~~ (gone for HIDDEN, given that #return_value assignments use the same scheme)
~~Forgo a let in more cases when the existing pointer expression is small / simple (e.g. if pointer is (T*)p there's not really any point in creating a temporary for it)~~ (allowed expressions only involving one symbol_exprt to be used directly, such as (type *)p and p[some_constant])
~~Kill the temporaries created for let bound variables when they go out of scope, to avoid pointlessly carrying them around in value_sett, the constant propagator, etc for the rest of time~~ ~~(added an owning object returned by clean_expr that kills the binders after the instruction is done executing)~~ (added a tracking vector of instruction-local bound variables, which are killed at the end of symex_step)

smowton · 2019-04-29T16:44:06Z

@tautschnig @kroening @peterschrammel TODOs done -- only data-gathering remains.

smowton · 2019-04-30T09:57:54Z

Here's a poster-child example:

#include <assert.h>
#include <stdlib.h>

int main(int argc, char **argv) {

  int **pptrs[50];

  // Set up a straightforward vector of double-derefs that lead to
  // seperate integer allocations, but do so in a complicated-enough
  // way to avoid constant propagation solving the whole thing (in a
  // real example some user-controlled control-flow writing to one or
  // other of the arrays would provide the corresponding breakage):
  for(int i = 0; i < 50; ++i) {
    int **new_ptrs = malloc(2 * sizeof(int*));
    new_ptrs[argc % 2] = (int*)malloc(sizeof(int) * 2);
    new_ptrs[argc % 2][0] = 1;
    new_ptrs[argc % 2][1] = 2;    
    new_ptrs[1 - (argc % 2)] = (int*)malloc(sizeof(int) * 2);
    new_ptrs[1 - (argc % 2)][0] = 3;
    new_ptrs[1 - (argc % 2)][1] = 4;    

    pptrs[i % argc] = new_ptrs;
  }

  // Now just try to read from the pointers -- this will generate a
  // pretty big formula as the nested deref could point to any of 50
  // objects, and then the outer deref must condition on its result to
  // determine where the inner pointer leads.

  assert(pptrs[argc % 50][argc % 2][argc % 2] == 5);
}

Interestingly the multiple levels of arrays are necessary -- if straightforward derefs are used instead of array indices then this code (https://github.com/diffblue/cbmc/blob/develop/src/pointer-analysis/value_set_dereference.cpp#L40) recurses into the nested if_exprt and thus avoids the quadratic case. However it's pretty brittle -- an intervening pointer addition, as we get from an index operator, is enough to break it. It could be sufficient to improve that code, though I think this would boil down to rewriting value_sett::get_value_set_rec to special-case if_exprt wherever it occurs in the syntax tree.

Result:
With develop, 4.7MB of VCCs (printed with --show-vcc), 8 seconds to run symex
With this patch, 337KB of VCCs, 0.3 seconds to run symex

Interestingly for this case the solver takes longer with the patch than without (26 seconds vs. 10), despite having very similar clause / variable counts after the simplifier / merge-ireps has got at them. This might be luck or might be systematic; if it is then I'd expect the main win here to come when the assertion violation we end up diagnosing doesn't directly depend on the big deref, or when there are a lot of pointer references meaning symex would be unlikely to finish without this patch.

smowton · 2019-04-30T10:06:20Z

To elaborate on the remark about nested if_exprts: the special case in value_set_dereference can handle directly nested dereferences, so if the first deref makes *(pp == &o1 ? o1 : o2) then we effectively push the deref in to make (pp == &o1 ? *o1 : *o2), producing much smaller value-sets for each sub-deref. However if the if_exprt is not the topmost node in the syntax tree (e.g. from an array access, represented as *(p + offset)) then we use get_value_set_rec's understanding of if_exprt, which simply sums the cases.

So, possibilities:

Use this patch
Push deref inside if_exprt more aggressively, especially inside the patterns generated by array accesses

Advantage of 1: flexible -- the kind of expression is irrelevant, all pointer expressions use let binders
Advantage of 2: less churn, and lower risk of unintentional performance effects

smowton · 2019-05-01T21:10:31Z

Ran benchmarks on Romain's suite -- overall symex runtimes got worse by about 3-4%, though there were a couple of cases that got significantly faster. Will benchmark including the solver on Friday. I suspect the specific deref-of-deref hack is performing better than a let-bound temporary when it works correctly, so I should probably revise this to continue using that workaround when possible, and only resort to let-binding when the situation is more complicated.

smowton · 2019-05-03T14:47:15Z

In fact it seems all the variation observed on that particular benchmark was due to the vagaries of Google's cloud, not any actual difference, as none of them reproduced on further inspection. Given this sort of thing only manifests in Java for multi-dimensional arrays it wouldn't be too surprising if the selection of Tika methods never uses the changed code.

tautschnig · 2019-05-05T10:04:12Z

src/goto-symex/symex_clean_expr.cpp

+{
+  exprt let_value = let_expr.value();
+  clean_expr(let_value, state, false);
+  let_value = state.rename(std::move(let_value), ns).get();


Just as a note: some time ago @kroening proposed to make let expressions be a scope of their own. Thus care would need to be taken as the let expression could have symbols of local scope even when the name overlaps with something occurring elsewhere. Not the case right now, but needs care moving forward.

tautschnig · 2019-05-05T10:08:12Z

src/pointer-analysis/value_set_dereference.cpp

+/// Particularly we want to make sure to insist on a local definition of \p expr
+/// is a large if-expression, such as `p == &o1 ? o1 : p == &o2 ? o2 : ...`, as
+/// can result from dereferencing a subexpression.
+static bool should_use_local_definition_for(const exprt &expr)


At least the implementation could just be replaced by using has_subexpr(ID_symbol), but maybe you want to remove the function altogether.

No, this looks for multiple symbol expressions, looking to permit x, (int*)x etc but not x[y] or *(x + (y ? z : w)) or similar

tautschnig · 2019-05-05T10:09:36Z

src/util/nodiscard.h

+\*******************************************************************/
+
+/// \file
+/// No-discard-result macro


Seems independent and might warrant a PR of its own?

tautschnig · 2019-05-05T10:14:50Z

src/goto-symex/symex_function_call.cpp

@@ -200,13 +200,14 @@ void goto_symext::symex_function_call_symbol(
 {
  code_function_callt code = original_code;

+  symex_live_let_variablest live_let_variables(*this, state);


Hmm, when exactly do we (not) need a new such context? Can we possibly reuse frames for this purpose? It's another bit of state to track and the interplay with branching I'm not entirely sure of.

smowton · 2019-05-07T17:04:48Z

@tautschnig please re-review, have replaced the owning object with a goto_symext-owned vector instruction_local_symbols

smowton · 2019-05-08T15:00:31Z

@tautschnig I added tests that check let-exprs are / are not introduced in several particular circumstances. I then noticed that one of the particular cases that's currently handled badly, *(int*)*p, is easy to fix by analogy with the existing special case for **p, so I added an extra small commit fixing that.

I also have a fix for the x->y->z case that executes that neatly in one expression without a let-binder or expression size blowup, but it's more controversial as it will require moving simplify calls around, so I'll post that as a followup.

peterschrammel · 2019-04-30T13:21:07Z

src/goto-symex/symex_dead.cpp

-  ssa_exprt ssa = state.rename_ssa<L1>(ssa_exprt{code.symbol()}, ns).get();
+void goto_symext::symex_dead(statet &state, const symbol_exprt &symbol_expr)
+{
+  ssa_exprt ssa = state


ugly clang-format

peterschrammel · 2019-05-08T17:05:54Z

src/pointer-analysis/value_set_dereference.cpp

+  {
+    symbolt fresh_binder = get_fresh_aux_symbol(
+      pointer.type(),
+      "derefd_pointer",


Should use the function_id here

I think not, the temporary should not be in the same namespace as the function's locals. Could just be "symex" though, like the namespace occupied by invalid-object symbols

This is needed to handle nested dereferences when symex_dereference uses let expressions. It depends on a cheap-to-copy value_sett so that we can easily record and then later discard the local definition.

There are a couple of key patterns involving members that we can understand, such as member-of-typecast and member-of-byte-extract, neither of which work properly if we have an intervening let expression.

This executes let expressions like ordinary assignments, avoiding the need for all other components of cbmc to understand the little-used local definition expression. It also means that symex's usual constant propagator, value-set and other analyses are brought to bear on the definition just as if the front-end had used an instruction to make the definition.

For the time being symex always lifts these immediately, to avoid having to teach all elements of cbmc about the let expression.

We'll use the symex_dead overload that takes a symbol expression rather than an instruction to kill let-bound local definitions

For example, we're willing to directly quote `p`, `(type *)p`, `p[some_constant]` and other simple expressions directly when comparing a pointer against its possible aliases-- the case we really must prevent is a large if-expression like `q == &o1 ? o1 : q == &o2 ? o2 : ...` that can result from a nested dereference -- in this case we must use a let-bound temporary to avoid producing a very large expression that can founder subsequent algorithms such as simplification, renaming and irep-merging.

Taking inspiration from #return_value variables, which are always marked as hidden, since all let-bound variables encountered by symex are synthetic we mark those hidden too.

This is in preparation for adding post-step cleanup

This avoids both wasted storage due to let-bound variables staying in the L2 renaming map, propagator and/or value-set, and avoids generating pointless PHI-node instructions for them.

This results from expressions such as *(int*)*p, and is very nearly as easy to handle as the already-special-cased deref-of-if case. In essence we transform *(type*)(x ? y : z) into x ? *(type*)y : *(type*)z, which should yield a more compact expression due to not conflating the alias sets that can be derived from the two arms of the conditional.

martin-cs · 2019-05-10T13:48:28Z

Seems to be the right way of going about solving this; will review in detail when I have time.

tautschnig

Looks good to me. @smowton Could you please post some performance evaluation results? You did post some earlier, but there have been significant changes to this PR since. Feel free to merge once you've provided that additional data.

smowton · 2019-05-13T10:43:31Z

Total process-seconds to run the cbmc CORE tests: 700s (-20)
Time to run my large Webgoat example: neither example terminates, but with this patch we get much further in the same time

smowton · 2019-05-13T10:53:18Z

Heh, I actually have another benchmark in progess... will post it here when it finishes anyhow

smowton · 2019-05-13T11:08:09Z

Good news! It was also a neutral finding.

smowton requested review from chrisr-diffblue, kroening, martin-cs, owen-mc-diffblue, peterschrammel, pkesseli and tautschnig as code owners April 26, 2019 17:17

smowton force-pushed the smowton/feature/let-expr-for-derefd-pointers branch from 5fc1cba to 70b510c Compare April 29, 2019 16:42

smowton assigned tautschnig, kroening and peterschrammel Apr 29, 2019

smowton force-pushed the smowton/feature/let-expr-for-derefd-pointers branch 2 times, most recently from 03aecf6 to 62cb205 Compare April 29, 2019 17:23

smowton force-pushed the smowton/feature/let-expr-for-derefd-pointers branch from 62cb205 to 6f05022 Compare April 30, 2019 10:10

tautschnig reviewed May 5, 2019

View reviewed changes

smowton force-pushed the smowton/feature/let-expr-for-derefd-pointers branch from 6f05022 to 65996f1 Compare May 7, 2019 17:03

smowton force-pushed the smowton/feature/let-expr-for-derefd-pointers branch 3 times, most recently from 5ad56b8 to 5b19b26 Compare May 8, 2019 14:57

smowton force-pushed the smowton/feature/let-expr-for-derefd-pointers branch 3 times, most recently from f85ac5a to 4ed2c1c Compare May 8, 2019 15:13

smowton force-pushed the smowton/feature/let-expr-for-derefd-pointers branch from 4ed2c1c to b733ab2 Compare May 8, 2019 15:18

peterschrammel approved these changes May 8, 2019

View reviewed changes

smowton added 12 commits May 9, 2019 15:31

Value-set: handle get_value_set_rec over let expressions

fb1b3a4

This is needed to handle nested dereferences when symex_dereference uses let expressions. It depends on a cheap-to-copy value_sett so that we can easily record and then later discard the local definition.

Simplifier: push member expressions inside a let

86eae91

There are a couple of key patterns involving members that we can understand, such as member-of-typecast and member-of-byte-extract, neither of which work properly if we have an intervening let expression.

Value-set-dereference: generate let expressions for complex pointers

7e7e757

For the time being symex always lifts these immediately, to avoid having to teach all elements of cbmc about the let expression.

Factor goto_symext::symex_dead

440a76d

We'll use the symex_dead overload that takes a symbol expression rather than an instruction to kill let-bound local definitions

Lift-lets: always emit hidden assignments

d3ebf4a

Taking inspiration from #return_value variables, which are always marked as hidden, since all let-bound variables encountered by symex are synthetic we mark those hidden too.

Goto-symex: add documentation to let-lifting and related functions

cbc495d

Split symex_step and execute_next_instruction

dc10d51

This is in preparation for adding post-step cleanup

Kill let-bound variables after the current instruction completes

61507bd

This avoids both wasted storage due to let-bound variables staying in the L2 renaming map, propagator and/or value-set, and avoids generating pointless PHI-node instructions for them.

Add tests for let-expression introduction on double-deref

7552bad

smowton force-pushed the smowton/feature/let-expr-for-derefd-pointers branch from b733ab2 to 87bcf4a Compare May 9, 2019 14:32

smowton mentioned this pull request May 10, 2019

Symex: resolve pointer comparisons using the value-set #4444

Merged

7 tasks

tautschnig approved these changes May 12, 2019

View reviewed changes

tautschnig assigned smowton and unassigned tautschnig and peterschrammel May 12, 2019

tautschnig merged commit 517c783 into diffblue:develop May 13, 2019

tautschnig mentioned this pull request May 13, 2019

Value-set dereference: use cond_exprt to avoid quadratic guards #4555

Closed

Use let-expression for dereferenced pointers #4576

Use let-expression for dereferenced pointers #4576

Uh oh!

Conversation

smowton commented Apr 26, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

smowton commented Apr 29, 2019

Uh oh!

smowton commented Apr 30, 2019

Uh oh!

smowton commented Apr 30, 2019

Uh oh!

smowton commented May 1, 2019

Uh oh!

smowton commented May 3, 2019

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!

smowton commented May 7, 2019

Uh oh!

smowton commented May 8, 2019

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!

martin-cs commented May 10, 2019

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

smowton commented May 13, 2019

Uh oh!

smowton commented May 13, 2019

Uh oh!

smowton commented May 13, 2019

Uh oh!

Uh oh!

smowton commented Apr 26, 2019 •

edited

Loading