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

mgudemann · 2018-02-08T12:40:20Z

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 · 2018-02-08T12:45:44Z

src/util/source_location.h

+  {
+    return get_bool(ID_C_java_removed_virtual_call);
+  }
+


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?

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

Maybe you can fix that all in one go?

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 · 2018-02-08T13:53:37Z

unit/java_bytecode/java_virtual_functions/virtual_functions.cpp

+        THEN("instrumentation assertions are inserted")
+        {
+          REQUIRE(
+            !instrument_cover_goals(


What does this check? REQUIRE_FALSE might be clearer here.

nothing much beyond verifying that instrumentation has been done

thk123 · 2018-02-12T10:41:44Z

src/goto-instrument/cover_instrument.h

+      // originating from a java virtual function call removal
+      if(
+        i_it->source_location == source_locationt::nil() ||
+        !i_it->source_location.get_java_removed_virtual_call())


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

thk123 · 2018-02-12T10:45:11Z

src/util/source_location.h

+  {
+    return get_bool(ID_C_java_removed_virtual_call);
+  }
+


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

thk123 · 2018-02-12T10:46:25Z

unit/java_bytecode/java_virtual_functions/virtual_functions.cpp

+          REQUIRE(function != new_goto_functions.function_map.end());
+
+          const goto_programt &goto_program = function->second.body;
+          for(auto it = goto_program.instructions.begin();


Can this not just be a range based for loop?

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.

converted to std::find_if

thk123 · 2018-02-12T10:53:08Z

src/goto-instrument/Makefile

@@ -94,12 +94,12 @@ INCLUDES= -I ..

 LIBS =

-CLEANFILES = goto-instrument$(EXEEXT)
+CLEANFILES = goto-instrument$(EXEEXT) goto-instrument$(LIBEXT)


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

peterschrammel · 2018-02-12T17:32:48Z

src/goto-instrument/cover_instrument.h

-      instrument(goto_program, i_it, basic_blocks);
+      // do not instrument if instruction has a source location but is marked as
+      // originating from a java virtual function call removal
+      if(


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

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

This adds a goal_filter to the instrumentation that skips over instructions marked as originating from a removed virtual call.

thk123 · 2018-02-13T16:34:01Z

unit/java_bytecode/java_virtual_functions/virtual_functions.cpp

+            "call and there is no GOTO ASSERT")
+          {
+            const source_locationt &loc = it->source_location;
+            REQUIRE(


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 · 2018-02-14T09:46:43Z

@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 · 2018-02-14T22:19:56Z

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 · 2021-02-24T10:24:06Z

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.

mgudemann self-assigned this Feb 8, 2018

mgudemann requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel, smowton and tautschnig as code owners February 8, 2018 12:40

tautschnig reviewed Feb 8, 2018

View reviewed changes

mgudemann force-pushed the feature/skip_basic_blocks_from_virtual_call_removal branch 5 times, most recently from 2b16c13 to 9690e9c Compare February 8, 2018 16:07

thk123 mentioned this pull request Feb 12, 2018

Introduce a java_source_locationt to contain Java specific source location information #1824

Closed

thk123 reviewed Feb 12, 2018

View reviewed changes

peterschrammel requested changes Feb 12, 2018

View reviewed changes

mgudemann force-pushed the feature/skip_basic_blocks_from_virtual_call_removal branch 4 times, most recently from 8a15359 to ca7cbbf Compare February 13, 2018 14:56

Matthias Güdemann added 4 commits February 13, 2018 17:19

Add ID_C_java_removed_virtual_call to irep defs

a9e2e51

Add possibility to mark instructions to source_locationt`

83481aa

Mark instructions in remove_virtual_functions

e596be1

Skip instructions from virtual call removal from instrumentation

012985f

This adds a goal_filter to the instrumentation that skips over instructions marked as originating from a removed virtual call.

mgudemann force-pushed the feature/skip_basic_blocks_from_virtual_call_removal branch from ca7cbbf to e7cf6c6 Compare February 13, 2018 16:26

thk123 approved these changes Feb 13, 2018

View reviewed changes

Add unit test for non-instrumentation of Java virtual calls

d0aea6e

mgudemann force-pushed the feature/skip_basic_blocks_from_virtual_call_removal branch from e7cf6c6 to d0aea6e Compare February 13, 2018 16:38

peterschrammel reviewed Feb 13, 2018

View reviewed changes

romainbrenguier mentioned this pull request Feb 14, 2018

[TG-1404] Specific implementation of cover basic block for Java #1830

Merged

NlightNFotis closed this Feb 24, 2021

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

mgudemann commented Feb 8, 2018 •

edited

Loading

tautschnig Feb 8, 2018

mgudemann Feb 8, 2018

tautschnig Feb 8, 2018

thk123 Feb 12, 2018

thk123 left a comment

thk123 Feb 8, 2018

mgudemann Feb 12, 2018

thk123 Feb 12, 2018

thk123 Feb 12, 2018

thk123 Feb 12, 2018

thk123 Feb 12, 2018

mgudemann Feb 13, 2018

thk123 Feb 12, 2018

peterschrammel Feb 12, 2018

mgudemann Feb 13, 2018

thk123 Feb 13, 2018

peterschrammel left a comment

mgudemann commented Feb 14, 2018

peterschrammel commented Feb 14, 2018

NlightNFotis commented Feb 24, 2021

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

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

Conversation

mgudemann commented Feb 8, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thk123 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

peterschrammel left a comment

Choose a reason for hiding this comment

mgudemann commented Feb 14, 2018

peterschrammel commented Feb 14, 2018

NlightNFotis commented Feb 24, 2021

mgudemann commented Feb 8, 2018 •

edited

Loading