Symex-dereference: simplify after deref [blocks: #2574, #4056]

[tautschnig]

This is generally useful because it turns member-of-if into if-of-member, which
avoids repeatedly quoting large complex if expressions in a with_exprt, but it
is especially good for field sensitivity as it puts member expressions directly
on top of symbol expressions, which field sensitivity knows how to deal with.

Performance evaluation is required , but also this change shows that some tests newly fail with this change, which is unexpected. See #3724 for the first one of them.

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

[tautschnig]

This requires the byte_update fixes from #2068 to make the SMT solver happy (adding the simplify step changes a nested byte_extract into a byte_update).

[allredj]

I'm curious to see what the impact on performance this change has.

[tautschnig]

I will benchmark (and I hope @romainbrenguier can do his benchmarking as well) once the dependencies #2068 and #3770 are merged so that we have a precise analysis.

[romainbrenguier]

This could maybe be made faster with a simplify method which would focus on the conversions that are mentioned above.

[tautschnig]

That is certainly one option - are there particular patterns that affect Java? (@smowton maybe?)

[kroening]

Update: this appears to be causing performance degradation; we may need to look into a specialised simplifier to achieve this.

[allredj]

This seems quite heavy to run on each call to dereference. Do we yet have a way to avoid evaluating invariants (and other assertions) in deployed binaries of CBMC?

[tautschnig]

Good point, I have now wrapped it in if(symex_config.run_validation_checks).

[allredj]

This line seems redundant

[tautschnig]

Comment cleaned up.

[allredj]

Thanks for running those benchmarks. Is there any evidence that this helps for Java?

[smowton]

Summary here: this isn't expected to cause a performance increase by itself (and indeed will definitely cost a little more). It is primarily a pre-requisite for field-sensitive symex, because of the member-of-if -> if-of-member transformation mentioned in the comments added by this PR.

I don't see a clear way to restrict simplify's activities except to keep track of expressions which are already maximally simplified and suppress repeated simplification. I've seen a couple of drafts by @tautschnig which attempt this, either by the simplifier tracking ireps it has seen and simplified, or by attaching comments to simplified ireps, or by adding an extra boolean to irept to track is-simplified state.

[romainbrenguier]

Summary here: this isn't expected to cause a performance increase by itself (and indeed will definitely cost a little more). It is primarily a pre-requisite for field-sensitive symex, because of the member-of-if -> if-of-member transformation mentioned in the comments added by this PR.

I guess that's fine, but in that case it could have been better for it to be part of the field-sensitive PR.

[tautschnig]

I've seen a couple of drafts by @tautschnig which attempt this, either by the simplifier tracking ireps it has seen and simplified, or by attaching comments to simplified ireps, or by adding an extra boolean to irept to track is-simplified state.

FWIW, tautschnig@ef00e0a is the most serious of those. It does seem to work well, but @kroening rightfully remarked that it opens the door to everyone asking for their little pet flag. But we'll get there when the other performance-optimising PRs have been reviewed/merged so that I can start posting those changes as PRs. Yet, as @smowton said, it's one more reason I'm not at all worried about performance cost here.

I have no issue merging this as part of #2574 as @romainbrenguier suggested, but I think it was important to debug and evaluate it separately as this has lead to a lot of type-related bug fixes.

[allredj]

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

[allredj]

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: f1ce452).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103024631
Status will be re-evaluated on next push.
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 compatibility was already broken by an earlier merge.

[tautschnig]

@smowton will add some benchmarking data to confirm that this is necessary for #4314 to go ahead.

[allredj]

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 427df5c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103062461
Status will be re-evaluated on next push.
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 compatibility was already broken by an earlier merge.

[smowton]

I benchmarked 133 Tika methods and found total runtime = 4818s with this PR + #4314, 4860s with just #4314, 5974s with just develop. Most of that reduction comes from 3 tests that were previously timeouts (timeout = 300s) that now complete in 30 seconds; the rest comes from 10-15s reductions in many tests that previously took 10-20s to analyse.

I expected to find a major penalty for not including this PR alongside #4314, because #4314 causes value_set_dereferencet to more rigorously use byte_extract operations when generic types differ, but no such effect was observed. This may be because constant-propagation was rarely succeeding in these cases and without it the byte-extract op is not actually that expensive, or it may be because the associated cost is only exposed when field-sensitivity is enabled, which by failing to promote member-of-symbol to an atomic SSA identifier forces a more-expensive composite struct operation.

[smowton]

4314 + this + develop vs. develop:

[smowton]

Successfully reproduced a micro-benchmark exposing the kind of problem I was expecting:

Test program:

public class Test {

  public static void main() {

    Generic<Integer> g = new GenericSub<Integer>();

    int x = 0;
    for(int i = 0; i < 3000; ++i)
      x += g.get();

    assert x == 0;

  }

}

class Generic<T> {

  T key; // Only here to make sure the compiler doesn't throw <T> away
  int x;

  public int get() { return 0; }

  public Generic() {
    key = null;
    x = 5;
  }

}

class GenericSub<S> extends Generic<S> {

  public int get() { return x; }

}

Times for --show-vcc:

Develop: 1.3s
#4314: 9.4s
#4314 + #3725: 1.5s

[smowton]

Excerpt from --show-vcc illustrating the problem:

-{-14} symex_dynamic::dynamic_object1#3 = { { { "java::GenericSub" }, NULL, 0 } }
-{-15} symex_dynamic::dynamic_object1#4 = { { { "java::GenericSub" }, NULL, 5 } }
+{-14} symex_dynamic::dynamic_object1#3 = byte_extract_little_endian(with(byte_extract_little_endian({ { "java::GenericSub" }, NULL, 0 }, 0, struct java::Generic), member_name component_name="key", NULL), 0, struct java::GenericSub)
+{-15} symex_dynamic::dynamic_object1#4 = byte_extract_little_endian(with(byte_extract_little_endian(symex_dynamic::dynamic_object1#3.@Generic, 0, struct java::Generic), member_name component_name="x", 5), 0, struct java::GenericSub)

[smowton]

VCCs for develop and #4314 + #3725 are identical; those for #4314 alone are ~25000 lines longer due to constant prop failure

[tautschnig]

Thanks a lot @smowton for the detailed analysis! I have added the test that you provided as a second commit.

[allredj]

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