Lazy methods: allow driver program to provide stubs

[smowton]

This adds a mechanism for asking languaget instances to produce functions they have not advertised.
DeepTest currently uses it to supply stub function bodies (jbmc replaces the calls, but this results
in a less-useful trace, as it lacks FUNCTION_CALL steps for stubbed functions).

[tautschnig]

Please check with #1272. Apparently there are N ways of marking something as do-not-display. Let's please not add approach N+1. The concept of "fallback functions" muddles the semantics of goto programs for the benefit of the user interface. At least that's my understanding of this matter...

[smowton]

This isn't about hiding symbols or GOTO functions, it's about providing bodies for functions that we don't have source code for.

Example:

class A {
  public int afield;

  static void f() {
    A a = Opaque.getA();
  }
}

If we don't have Opaque.class available, then jbmc currently replaces the callsite (using convert_nondet), so we get a program like:

f:
  A a;
  a = ALLOCATE(sizeof(A));
  a->afield = NONDET(int);

DeepTest on the other hand retains the call, but uses a custom derivative of java_bytecode_languaget that provides a body for the callee, so instead we get:

f:
  A a;
  a = Opaque.getA();

Opaque.getA():
  A ret = ALLOCATE(sizeof(A));
  ret->afield = NONDET(int);
  return ret;

That's more useful than JBMC's approach (I think JBMC should switch to using this method), as it (a) clarifies where the nondet init sequence came from (a call to stub Opaque.getA()), and (b) results in a trace containing FUNCTION_CALL and FUNCTION_RETURN steps for Opaque.getA(), which helps identify stub calls.

In order to do this, lazy_goto_modelt needs to know which languaget to ask to provide the body for Opaque.getA. The usual method of asking each languaget what methods it can provide doesn't work, as we actually don't have bytecode for Opaque.getA, but nontheless we can provide a definition if no other languaget is offering one. Hence we need some way to ask for the method body, even though it isn't a "claimed" method.

[tautschnig]

Thanks a lot for the elaboration, but can we please have a comprehensive and agreed solution to address #1948, #1949, #2070, #1317, #1585, #1566 (and there might be more)? And of course right now, thanks to @hannes-steffenhagen-diffblue's work, we already have --generate-function-body in the public code base.

Maybe this PR is part of a bigger plan, but if so it would really help to sketch this out to make sure there isn't further fragmentation.

[smowton]

Hmmm, okay, to cooperate better with these goto-instrument-oriented function generators / replacers we could instead ask the driver program what to do in this circumstance -- i.e., none of the language frontends could furnish a body for this front-end, so does the driver program want to have a go at providing a GOTO program somehow? Then it would use one of @hannes-steffenhagen-diffblue's passes, or for Java we'd do the nondet-object-graph thing. I can have a go at this solution next week.

[smowton]

@tautschnig pushed an alternative implementation. I think this should satisfy everyone's needs (when using the lazy loading framework): it gives the driver program a chance to provide a body before language_filest (e.g. to replace bodies we could provide, as in @polgreen's block-function patch), but it can also opt to only provide missing functions (the stub use-case).

I'm checking with @peterschrammel whether we can open-source DeepTest's stub generation code; if so I plan to submit a followup PR to get jbmc using this mechanism to provide stubs.

[tautschnig]

I think this proposal is good, because it keeps the lazy behaviour contained rather than spreading it across multiple classes and APIs.

Yet I struggle to fully evaluate it (thus sticking with "Comment" rather than "Approve") as there are no regression tests (there may be tests exercising the new code paths already present in the test suite, but no test has observably different behaviour).

[tautschnig]

Unintended change?

[smowton]

If I get an ok to open a file of deeptest's code I will make jbmc a user of this code, then hopefully its existing tests will suffice to show this is working as intended.

[tautschnig]

I, for one, am ok for the moment if you tell me that there are tests elsewhere that show this makes a difference and works as intended. Not great, but if you put that note in the commit message then you're committing to it ;-)

Elsewhere it was said that there are current issues in tests elsewhere, so you might, however, have to hold off on this anyway.

[smowton]

This should be tested with Deeptest once it can build with mainline cbmc again.

[smowton]

@tautschnig @thk123 I've obtained permission from @peterschrammel to open a simple version of Deeptest's stub generator and added a commit to use it in jbmc.

The new stub generator, java_bytecode/simple_method_stubbing.h/cpp, has much reduced features compared to Deeptest's version, but is comparable to convert_nondet, which used to provide similar behaviour for jbmc.

If this works this will serve as a template for how Deeptest can integrate its own stub generator with lazy_goto_modelt.

[smowton]

Test-gen bump: https://github.com/diffblue/test-gen/pull/1794

@tautschnig @peterschrammel @thk123 @mgudemann this is ready for review.

[tautschnig]

Various, mostly stylistic notes.

[tautschnig]

Forward declarations would suffice.

[tautschnig]

Is that actually used in this method?

[tautschnig]

Nit pick: lexicographic sorting.

[tautschnig]

Is this needed/used?

[tautschnig]

Seems unused.

[tautschnig]

Seems unnecessary?!

[tautschnig]

Seems unnecessary?!

[tautschnig]

Nit pick: the use of && would make this code more concise and would express what is the condition instead of saying when not to do this. Like this:
if(!sym.is_type && sym.value.id() == ID_nil && sym.type.id() == ID_code) create_method_stub(...); (while moving the two sym.name to the top to clearly mark the exceptional case.

[tautschnig]

This is a newly added file, so should be made clang-format correct.

[smowton]

@tautschnig all changes applied.

[tautschnig]

Some compilers insist that this should be a struct and thus make the Travis build fail.

[tautschnig]

clang-format has a lot to criticise - I'd suggest to make newly added code clang-format-clean.

[smowton]

Fixed the compile bug. My local clang-format (LLVM 6.0) appears to disagree with the version running on Travis (LLVM 3.7), so I'm inclined to ignore them both.