Symex: ignore null dereferences when targeting Java

[smowton]

In Java (and other safe languages) we know that any path that led to dereferencing
a null pointer would have thrown or asserted beforehand (i.e. all pointer dereferences
are checked). Therefore when dereferencing a pointer with value-set {NULL, someobj}
there is no need to generate (for example)
ptr == &someobj ? someobj.somefield : invalid_object.somefield, but rather we can simply
produce someobj.somefield.

In principle this could also be extended to C programs that have --pointer-check enabled,
to other safe languages, and to specific pointer accesses that are analysed never-null at a
particular program point.

[tautschnig]

So why do we have null in the set of objects in the first place?

[smowton]

Flow insensitivity.

A a = null;
if(some_param)
  a = new A(5);

// VS for a = { dynamic_object1, NULL }

int val = a.value;

Here propagating 5 to val is safe because the field a.value can only be accessed if a is non-null. The code is short-hand for:

A a = null;
if(some_param)
  a = new A(5);

if(a == null)
  throw new NullPointerException();
int val = a.value;

The result is a needlessly complex val#1 == a == &dynamic_object1 ? 5 : a$invalid_object.value expression, when we could just have val#1 == 5 and also constant propagation.

Generally symex could figure this out by using the guard at int val = ... (a != null) to filter the value-set. However in a safe language it seems simpler to observe that all pointer accesses are checked.

[smowton]

Similar to the other PR, if you don't want to see ID_java in goto-symex, how about attaching an attribute ID_C_is_checked to dereference_exprt, which indicates a check has already been made to ensure we cannot dereference a null pointer, whether an assert, assume, exception or ordinary branch?

[smowton]

Discussed in person with @kroening: agreed solution is for the driver program to pass a parameter to bmct -> goto_symext indicating whether it can guarantee checked dereferences-- for jbmc this will always be true, and for cbmc it will be true if pointer-checks is set.

[smowton]

@tautschnig @peterschrammel @kroening @mgudemann this has been updated with a first shot at the design described above and is ready for review.

[tautschnig]

I believe we first need to converge on the discussion in #2031. No need to get the code in that PR merged, but the semantics of ASSERT need to be clarified. The code currently generated is

        // 24 file test.java line 14 function java::test.main:(Z)V bytecode-index 10
        // Labels: pc20$
        maybe_t = (struct test *)$stack_tmp1;
        // 25 file test.java line 20 function java::test.main:(Z)V bytecode-index 13
        ASSERT !(maybe_t == null) // Throw null
        // 26 file test.java line 20 function java::test.main:(Z)V bytecode-index 13
        field_value = maybe_t->field;

and the proposal in this PR would only apply if the semantics of ASSERT is "you can't get past 'assert(false)'" (to quote @smowton).

Edit: if the front-end directly tells the back-end what the semantics of the intermediate representation is then we're violating established compiler design principles. Maybe there are good reasons for doing so, but I'd rather see those reasons first. So let's please sort out the semantics of the above snippet first.

[smowton]

Interesting. In that case jbmc should only pass this flag (at present) when running in --cover mode (when assertions-to-assumptions means we really can't pass the assertion).

Reason for the ugly design: because the general problem "can this pointer possibly be null at this program point?" is quite hard to answer -- in principle the state guard tells us the answer, but extracting it might be difficult when e.g. trying to check whether x->y->z is known to be not null, which might manifest as a great big explosion of ternary conditionals over possible referees of x and y. When running against a safe language however we know this is all wasted effort, as the front-end undertakes to always check pointer derefs.

[smowton]

@tautschnig commented at #2031; perhaps we can make assert sane rather than having to restrict the applicability of this patch.

[martin-cs]

I guess after all of the ranting it's clear what my opinion / suggestion / preferred solution for this is...

[smowton]

@tautschnig now the fatal-pointer-checks patch is in, are you happy for this to move forwards?

[tautschnig]

This must not be merged as is, for two reasons:

1. It is unsound: a concurrent update setting a reference to null would be missed.
2. The clarified semantics of assert/assume now enable tweaking either symex or (preferred) the value-set analysis to take into account non-nullness constraints. (Most likely it will be a combination of both: symex should update the value-set analysis upon processing an assume.) This can be done soundly, even in presence of concurrency.

[smowton]

1. Would it be sufficient for the front-end to determine if it's submitting a concurrent program? I have no idea how the Java frontend would actually generate one, but presumably one of the former Java concurrency team knows. This is really a shortcoming of the frontend, as there is no atomic check-not-nulll-and-dereference operation -- any data race over a pointer can produce results that are in fact impossible on the JVM.
2. assume(x != null) filters the value-set sounds tempting, but is very low-powered, as e.g. assume(x->y->z != null); x->y->z->w = 5 will hardly ever eliminate the null pointer, as get_reference_set(x->y->z) is probably not singular. Really you want a peephole alias analysis that checks that x->y->z must alias the x->y->z used some number of ASSUME instructions ago (not strictly the preceding instruction, due to ASSUME(x != null); ASSUME(x->y != null); ASSUME(x->y->z != null); // access x->y->z).

We could get reasonable power by adding a new data structure to symex to track expressions that are currently known not null (blanked on any assignment or control flow, added to by assume-not-null statements), but perhaps this is overpowered for the desired result?

[tautschnig]

any data race over a pointer can produce results that are in fact impossible on the JVM.

If that's the case, then the assert+assume+access should be placed in an atomic section.

I think there is a fair amount of C code that does if(p != NULL) *p = 42; and symex should be able to handle this nicely - not just in the Java case. As much as I can, I will keep pushing back against front-end <-> symex communication. We do symbolic execution on goto programs, and if there are code patterns that cause unnecessary slow-down we should develop an analysis to detect those, and not use some front-end hints. We already do pass the state.guard to the value-set analysis, but I don't think it makes as much use of it. I think we should be able to make at least the simple example described in this PR resolve via this route. This requires studying what information state.guard actually has, and what the value-set analysis does about it.

[smowton]

Benchmark: I generated a synthetic benchmark using this script:

#!/usr/bin/env python

import random
import sys

if len(sys.argv) != 2 or sys.argv[1] not in ("good", "bad"):
    print >>sys.stderr, "Usage: gen.py (good | bad)"
    sys.exit(1)

spoil_assumption = sys.argv[1] == "bad"

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

for i in range(100):
    print "  int local%d = %d;" % (i, i)

vars = ["&local%d" % i for i in range(100)]

choices = 0
def tchoice(l):
    n = len(l)
    global choices
    out = ""
    while len(l) > 1:
        out += "(argc == %d ? %s : " % (choices, l[-1])
        choices += 1
        l.pop()
    if len(l) == 1:
        out += "(%s" % l[0]
    out += ")" * n
    return out

print "  "

for i in range(10000):
    naliases = random.randint(1, 5)
    aliases = random.sample(vars, naliases) + ["0"]
    print "  int *ptr%d = %s;" % (i, tchoice(aliases))
    print "  __CPROVER_assume(ptr%d != 0);" % i
    if spoil_assumption:
        print "  int incidental%d = 0;" % i
    print "  int deref%d = *ptr%d;" % (i, i)

print "  "
print "  assert(0);"

print "}"

In the "good" case it generates something of the form

int local1 = 1, local2 = 2, ...;
int *ptr1 = nondet-choice-of(&local1, &local2, ...., null);
__CPROVER_assume(ptr1 != 0);
int deref1 = *ptr1;

and in the bad case it adds an extra int incidental1 = 0; right before the deref, to confound the analysis and cause it to make no improvement.

Results (Old and New are cbmc before and after this patch; Good and Bad are the scenarios above where the optimisation works and doesn't work respectively):
Time (s):

	Old	New
Good	64	62
Bad	76	81

Size of VCCs (printed, million characters):

	Old	New
Good	3.7	3.2
Bad	4.1	4.1

In all cases I used the debug build (for conveinence) and --show-vcc because the solver didn't terminate in a reasonable timescale. It seems reasonable to suppose that with 3.2M rather than 3.7M chars of VCCs in the Good case it would have recouped some time. However even within the symex-and-print-vccs process we can see a small (6.5%) time cost in the bad case, where we gather lots of information about possible safe pointers but never get to use that information profitably, and a small benefit (3%) in the good case where our information always makes us more certain about a pointer, and so we emit a smaller formula. That benefit would become larger if the result of the deref was subsequently used in expressions that could be constant-propagated away.

[tautschnig]

@smowton Thanks a lot for the detailed benchmarking report! So it seems that in case of C it doesn't make a whole lot of a difference (some improvement, some cost). Hence I'm now curious about results on the benchmarks/problems you had originally looked at that actually lead to you starting this PR?

[smowton]

To give a simple example, I added a new "best" case to the script, which always uses alias sets of size 1 + null, and includes some junk code only executed when we're uncertain -- for example, if(deref1 != local30) { for(int j = 0; j < 10; ++j) { } }

So the situation looks like

int x = 0;
int *ptr = nondet(int) ? &x : null);
assume(ptr != null);
int x2 = *ptr;
if(x != x2) { // something expensive }

I had to lower the number of ops to 1000 (from 10000) for this version to complete in a reasonable timeframe.

Predictably this takes the old CBMC 42s / 1.4Mc of VCCs, and the new one 6s / 0.16Mc of VCCs.

So very large gains are possible when improved constant prop results in certainty about a control-flow choice. The most common form of this in Java is a virtual function call (e.g. A a = nondet(int) ? null : new A(); a.f();). That code can only call the f() method implemented or inherited by A, but in the case where symex thinks there may be a null pointer deref it includes a$object.@class_identifier as a possible key used to dispatch the call, and being uncertain about that value also considers B.f(), C.f(), ... as possible callees. It then generates VCCs for those in-fact-unreachable callees, resulting in potentially enormous cost, depending on how nasty B.f, C.f et al are.

By itself I suspect this won't deliver a massive improvement on practical Java software, as without #2122 we become uncertain about @class_identifier because it is a field of a structure rendered non-constant for other reasons. However, combined with other improvements like that we can increase our chance of resolving a virtual function target (or perhaps a function pointer target?) at symex time, and therefore exclude great gluts of code from the target formula.

[tautschnig]

Ok, thanks, so what is your preferred way to proceed? Should this wait until we have all the bits together to demonstrate big gains, or should we try to merge this soon/now? (I'd actually prefer to hold off on such a change until after 5.9 is released, which should be happening really soon -> @kroening). My suggestion: discussion (offline) between @smowton and @kroening.

[smowton]

Personally I'd like to get this merged as big merges are very difficult. Re: #2122 we need to decide-- is your field-sensitive constant prop stuff going to get in any time soon, and will it be good enough to always resolve a clsid test? If it's too difficult and too performance sensitive to get it in, can we special-case it in a way that's less ugly than the rejected #2122 (which used magic knowledge that @class_identifier is just another word for dynamic type)? Can we stop using a field to store the RTTI at all, and instead introduce a primitive RTTI operator that symex can cleanly interpret?

[smowton]

Discussed with @kroening just now: he is to confer with @tautschnig re: when this goes in; I will follow up with a separate PR to re-use the guard already passed down the symex_dereference recursion to exclude null pointers from expressions like ptr ? *ptr : 0, rather than producing silly expressions like ptr ? (ptr == &local ? 1 : ptr$object) : 0

[allredj]

Passed Diffblue compatibility checks (cbmc commit: aa1b249).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/76979426

[peterschrammel]

LGTM, some nitpicks

[peterschrammel]

weird indentation (several occurrences)

[peterschrammel]

use optional here as well?

[smowton]

Michael argued for a pointer earlier, so I'm going to stick with that rather than go back and forth :)

[peterschrammel]

Alright

[peterschrammel]

aliasing

[peterschrammel]

Is this sizeable method intentionally defined in the header file?

[peterschrammel]

Nitpick: I guess JBMC should report FAILED (not the 'test should fail').

[allredj]

@smowton do you plan on doing a test-gen PR for that?

[smowton]

ok

[smowton]

https://github.com/diffblue/test-gen/pull/1973

[smowton]

Applied all of Peter's comments apart from one response

[allredj]

Passed Diffblue compatibility checks (cbmc commit: ab42137).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77037324

[allredj]

Bump is failing some regression tests.

[allredj]

Passed Diffblue compatibility checks (cbmc commit: 9fd3434).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77151625