[TG-2356] skip basic block instrumentation from virtual call removal

[mgudemann]

When a virtual function call is encountered in Java, we replace it by explicit calls to all possible implementing object types.

The coverage instrumentation does not allow for a single bytecode index (the virtual call) to be instrumented several times, which makes sense, as only a single such instrumentation can be placed at the bytecode.

In the current implementation, a coverage property was placed right after the first guarded GOTO, but not on succeeding ones, leading to the situation that coverage was reported differently, depending on the order implementing classes were found. This patch removes instrumentation of GOTO instructions generated via remove_virtual_functions altogether, the function call is considered to be completed and covered if the final target t_final is reached. This is the target for each concrete function call.

[tautschnig]

I'm failing to parse the commit message for this one, and I'm not too happy to have Java-specific APIs enter something as general as a source_locationt? You might play the same game as is done with various other irept-children and introduce a java_source_locationt that has those extra functions?

[mgudemann]

@tautschnig I don't mind, but please note that source_locationt already has get_java_bytecode_index

[tautschnig]

Maybe you can fix that all in one go?

[thk123]

As this is a fairly large refactoring I've raised an issue (#1824) to tackle this separately.

[thk123]

Looks good, but the final commit should be squashed into the unit tests commit (or introduced before it) so that each commit compiles (also confusingly GH shows Add possibility to mark instructions to source_locationt before Skip instructions from virtual call removal from instrumentation but this is just GH being weird.

[thk123]

What does this check? REQUIRE_FALSE might be clearer here.

[mgudemann]

nothing much beyond verifying that instrumentation has been done

[thk123]

I think this commit may be in the wrong order as I don't think this function has been introduced yet.

[thk123]

As this is a fairly large refactoring I've raised an issue (#1824) to tackle this separately.

[thk123]

Can this not just be a range based for loop?

[thk123]

Or since you are actually just looking for a specific find, perhaps:

std::find(
  goto_program.instructions.begin(), 
  goto_program.instructions.end(), 
  [](const instructiont &instruction) {
    return instruction.type==goto_program_instruction_typet::GOTO &&
      instruction.guard.id() == ID_equal;
  });

This has the advantage you can require that you find the relevant instruction and make it clear you're only looking for the first equal guarded goto.

[mgudemann]

converted to std::find_if

[thk123]

Perhaps the intent was already there, but this should be squashed with the commit that introduces the unit tests so that they compile.

[peterschrammel]

This is misplaced - it should be implemented as a goal filter, see e.g. https://github.com/diffblue/cbmc/blob/develop/src/goto-instrument/cover_filter.cpp#L96

[mgudemann]

done, it's now part of bool internal_goals_filtert::operator()(const source_locationt &source_location) const

[thk123]

The printer deals better with simple statements, perhaps:

REQUIRE(loc != source_locationt::nil());
REQUIRE_FALSE(loc.get_java_bytecode_index().empty());

[peterschrammel]

Apart from #1824, this looks ok. The underlying problem that this tries to solve is more generally solved in #1830, though. So, I actually think that this PR is redundant.

[mgudemann]

@peterschrammel I see the point, #1830 seems to be more generic. On the other hand, it might introduce a superfluous coverage property, e.g., for virtual calls the first guarded GOTO will always be reached so this basic block is always covered. Then again, this is likely harmless.

[peterschrammel]

Yes, #1830 is not optimal. We measured on tika that we could decrease the number of coverage goals by 15-20% by making the instrumentation proposed in #1830 more sparse.

[NlightNFotis]

Hello.

I'm closing this PR as it appears stale and no longer in sync with the repository. Feel free to reopen it if you feel it adds enough value and should be merged, but in that case this will need to be rebased on top of branch develop first.