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

romainbrenguier · 2018-02-12T09:26:23Z

The current implementation of cover_basic_blockt does a first pass on the goto-program without using the bytecode index information, and then later select instruction for bytecode indices.
The process is a bit complicated and sometimes instruments instruction that are after an IF of the same bytecode indices, leading to wrong information about bytecode coverage.
This PR intruduce an alternative cover_basice_block_javat, which for Java use the bytecode information to determine what are the blocks of the program, and selects the first instruction with that bytecode index as a representative.
This strategy is simple and ensures each goal corresponds to a bytecode index coverage.

LAJW

LGTM

LAJW · 2018-02-12T09:57:20Z

src/goto-instrument/cover_basic_blocks.h

@@ -117,4 +101,33 @@ class cover_basic_blockst : public cover_blocks_baset
  std::vector<block_infot> block_infos;
 };

+class cover_basic_blocks_javat : public cover_blocks_baset


I'd add mark cover_basic_blocks_javat as final.

LAJW · 2018-02-12T09:59:12Z

src/goto-instrument/cover.cpp

@@ -28,21 +28,26 @@ Date: May 2016
 void instrument_cover_goals(


Since this function has so many arguments, could they be packed into an instrument_cover_goals_infot struct?

LAJW · 2018-02-12T10:01:04Z

src/goto-instrument/cover_basic_blocks.cpp

+    {
+      block_infos.push_back(it);
+      index_to_block.insert(
+        std::make_pair(bytecode_index, block_infos.size() - 1));


You write it as insert({ bytecode_index, block_infos.size() - 1}) or emplace(bytecode_index, block_infos.size() - 1) to avoid std::make_pair.

LAJW · 2018-02-12T10:02:36Z

src/goto-instrument/cover_basic_blocks.h

+    message_handlert &message_handler){};
+};
+
+class cover_basic_blockst : public cover_blocks_baset


I'd mark cover_basic_blockst as final.

The operator() functions in goto_symext now have explicit names. Previous commits have overloaded these functions with several combinations of arguments; the renaming is in preparation for a future commit that would necessitate even more overloadings, with the same parameter types. Several of goto_symext's functions have been made protected rather than public, as they are only called from the top-level goto_symext functions. The two_argument operator() function is removed completely, as it was only called from a single place and was only two lines long. Its implementation is moved to the caller.

…ge-instrumentation Refactoring in coverage instrumentation

…ogram This was supplying synthetic --unwind parameters for each loop found in the GOTO program, but that required early access to the GOTO code, which will not be available under symex- driven lazy loading. Therefore we replace that pass with a handler mechanism that allows the driver program to provide its own callback to make unwinding decisions, and use it in JBMC to ensure that enumeration type static initialisers are unwound sufficiently.

This used to be necessary to account for stub globals and stub class fields that were discovered during method elaboration; however, now that they are all discovered up front there is no need.

[path explore 1/8] Tidy up symext top-level funs

… class

This sets the string refinement iteration limit to zero, i.e. unlimited. The mechanism for providing a limit is left in place, for use probably driven by a command-line argument by the first user to need that facility.

…recreate-initialize Remove __CPROVER_initialize recreation

…-clinit-unwinder Reimplement remove-static-init-loops to avoid need to inspect GOTO program

The unused capture breaks the build when compiling with clang++ >= 5.0.1.

Symex class cleanup

…-capture Remove unused lambda capture

…ng-solver-iteration-limit Remove string solver iteration limit

Normally this situation (a reference to static field A.x, when neither A nor any of its ancestors either define a field x or are opaque stubs) would be an error, probably indicating a class version mismatch, but at present some of our library models intentionally exploit this behaviour to obtain a nondet- initialised field. Therefore for the time being we tolerate the situation, initialising such fields in __CPROVER_initialize, as we cannot attach a synthetic clinit method to a non-stub type.

No functional changes.

Previously clinit wrappers that had been generated but never actually called would remain in the GOTO program as empty, uncalled functions. Now they are cleaned up in the same way as unused user functions.

These check that direct and indirect clinit wrappers, as well as stub class synthetic static initialisers, are removed if they are generated but not subsequently called.

These cover various permutations of static fields defined on parents, on interfaces, and those parents and/or interfaces being opaque (stubs). They check both that jbmc doesn't outright crash, and in some cases that jbmc correctly determines that two static fields must be the same one, and therefore cannot differ.

Library preconditions

Emit timestamps on each line of output

…ted-static-fields Add support for inheritence of Java static fields. Fixes TG-2457

…sed-clinits Java frontend: clean up unused clinit symbols

The block numbers in cover_basic_blockst are obtained from `block_info.size() - 1`, they should have type std::size_t rather than unsigned. Also mark const a couple of arguments that are constant.

This will allow to have two implementations for this functor.

This is a specific implementation of cover block for Java. It uses the bytecode index to determine blocks and replace the use of select_unique_java_bytecode_indices.

The index is checked against the size before end so there is no need to use at there.

JBMC use to group together several lines within the same block. This is no longer the case for the Java specific block instrumentation. Each line is part of a different goal.

This checks that coverage instrumentation assertions are added at the first instruction with given bytecode index. And that there is no such assertion in the middle of instructions with same bytecode index.

romainbrenguier · 2018-02-15T10:04:02Z

actual PR on cbmc diffblue#1830

This global name map will be used to check what generation is currently available for each level1 name, and shared across all states. This will only be used when a particular state tries to find out what the next free generation is. The main draw of this is that all branches will now assign unique generations that won't clash with assignments done across other branches. One minor downside is that in VCC's the generation number might jump sporadically (say from #4 to diffblue#40).

romainbrenguier requested a review from LAJW February 12, 2018 09:44

LAJW approved these changes Feb 12, 2018

View reviewed changes

romainbrenguier force-pushed the feature/cover-basic-block-java#TG-1404 branch from 56faac0 to 0c5925a Compare February 12, 2018 13:25

romainbrenguier force-pushed the refactor/coverage-instrumentation branch from 3ef6759 to 3454ef1 Compare February 12, 2018 13:36

romainbrenguier mentioned this pull request Feb 12, 2018

Bytecode index aware block selection in coverage instrumentation [TG-1404] #3

Closed

romainbrenguier force-pushed the refactor/coverage-instrumentation branch 4 times, most recently from efddc26 to eb6463f Compare February 13, 2018 08:58

romainbrenguier force-pushed the refactor/coverage-instrumentation branch from eb6463f to 6492b3a Compare February 13, 2018 11:29

romainbrenguier and others added 3 commits February 13, 2018 16:29

Merge pull request diffblue#1819 from romainbrenguier/refactor/covera…

2bb98d9

…ge-instrumentation Refactoring in coverage instrumentation

Remove __CPROVER_initialize recreation

968d97e

This used to be necessary to account for stub globals and stub class fields that were discovered during method elaboration; however, now that they are all discovered up front there is no need.

romainbrenguier force-pushed the feature/cover-basic-block-java#TG-1404 branch from 0c5925a to f8a159d Compare February 13, 2018 16:44

tautschnig and others added 4 commits February 13, 2018 18:59

Merge pull request diffblue#1827 from karkhaz/kk-symex-operator-tidy

932a38f

[path explore 1/8] Tidy up symext top-level funs

clean up symex_assign vs. symex_assign_rec

bb64ea6

cleanup of some noise (mostly obvious declarators) in the goto_symext…

9ba7fe2

… class

preconditions for delete and delete[]

c94548c

romainbrenguier force-pushed the feature/cover-basic-block-java#TG-1404 branch from f8a159d to 20f8bb2 Compare February 14, 2018 07:58

smowton and others added 8 commits February 14, 2018 08:07

Remove string refinement iteration limit

1ac9abe

This sets the string refinement iteration limit to zero, i.e. unlimited. The mechanism for providing a limit is left in place, for use probably driven by a command-line argument by the first user to need that facility.

Merge pull request diffblue#1828 from smowton/smowton/cleanup/remove-…

9b59631

…recreate-initialize Remove __CPROVER_initialize recreation

Merge pull request diffblue#1815 from smowton/smowton/feature/replace…

9620802

…-clinit-unwinder Reimplement remove-static-init-loops to avoid need to inspect GOTO program

Remove unused lambda capture

fbd54df

The unused capture breaks the build when compiling with clang++ >= 5.0.1.

pre-conditions for strings

9ea0cc6

turn some assertions in the stdlib.h models into preconditions

f6f45fc

Merge pull request diffblue#1833 from diffblue/symex_class_cleanup

e8105bd

Symex class cleanup

Merge pull request diffblue#1836 from karkhaz/kk-remove-unused-lambda…

0f20482

…-capture Remove unused lambda capture

romainbrenguier force-pushed the feature/cover-basic-block-java#TG-1404 branch from 1083f74 to f540273 Compare February 14, 2018 12:05

Merge pull request diffblue#1820 from smowton/smowton/fix/remove-stri…

ef08ae2

…ng-solver-iteration-limit Remove string solver iteration limit

smowton and others added 22 commits February 14, 2018 14:06

US spelling of initialize

afa443c

No functional changes.

Exclude j.l.O from possible static field hosts.

f15c312

Java frontend: clean up unused clinit symbols

adc9fd4

Previously clinit wrappers that had been generated but never actually called would remain in the GOTO program as empty, uncalled functions. Now they are cleaned up in the same way as unused user functions.

Add tests to verify that synthetic method removal is performed

19d622b

These check that direct and indirect clinit wrappers, as well as stub class synthetic static initialisers, are removed if they are generated but not subsequently called.

Merge pull request diffblue#1834 from diffblue/library-preconditions

7b5dd17

Library preconditions

Merge pull request diffblue#1713 from karkhaz/kk-debug-timestamps

a2ebb33

Emit timestamps on each line of output

Merge pull request diffblue#1826 from smowton/smowton/fix/java-inheri…

278e4e6

…ted-static-fields Add support for inheritence of Java static fields. Fixes TG-2457

Merge pull request diffblue#1813 from smowton/smowton/fix/cleanup-unu…

38e6e4a

…sed-clinits Java frontend: clean up unused clinit symbols

Correct types from unsigned to std::size_t

e0eeeb5

The block numbers in cover_basic_blockst are obtained from `block_info.size() - 1`, they should have type std::size_t rather than unsigned. Also mark const a couple of arguments that are constant.

Put interface to cover_blocks in virtual class

379c1e2

This will allow to have two implementations for this functor.

Refer to interface rather than cover_basic_blockst

2c92a17

cover_block implementation using bytecode location

cff56a9

This is a specific implementation of cover block for Java. It uses the bytecode index to determine blocks and replace the use of select_unique_java_bytecode_indices.

fixup! cover_block implementation using bytecode location

cdeeb66

Use [] instead of at on vector

7cecd99

The index is checked against the size before end so there is no need to use at there.

fixup! cover_block implementation using bytecode location

463fb40

fixup! cover_block implementation using bytecode location

c743740

fixup! cover_block implementation using bytecode location

b996ae9

fixup! cover_block implementation using bytecode location

ea385e4

Adapt coverage test for new instrumentation

69ea97b

JBMC use to group together several lines within the same block. This is no longer the case for the Java specific block instrumentation. Each line is part of a different goal.

fixup! cover_block implementation using bytecode location

82079d8

romainbrenguier force-pushed the feature/cover-basic-block-java#TG-1404 branch 3 times, most recently from 750cbfc to 788ba62 Compare February 15, 2018 09:30

Add unit tests for java block instrumentation

2ef935e

This checks that coverage instrumentation assertions are added at the first instruction with given bytecode index. And that there is no such assertion in the middle of instructions with same bytecode index.

romainbrenguier force-pushed the feature/cover-basic-block-java#TG-1404 branch from 788ba62 to 2ef935e Compare February 15, 2018 10:01

romainbrenguier closed this Feb 15, 2018

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

romainbrenguier commented Feb 12, 2018 •

edited

Loading

LAJW left a comment

LAJW Feb 12, 2018

LAJW Feb 12, 2018

LAJW Feb 12, 2018

LAJW Feb 12, 2018

romainbrenguier commented Feb 15, 2018

		@@ -28,21 +28,26 @@ Date: May 2016
		void instrument_cover_goals(

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

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

Conversation

romainbrenguier commented Feb 12, 2018 • edited Loading

LAJW left a comment

Choose a reason for hiding this comment

LAJW Feb 12, 2018

Choose a reason for hiding this comment

LAJW Feb 12, 2018

Choose a reason for hiding this comment

LAJW Feb 12, 2018

Choose a reason for hiding this comment

LAJW Feb 12, 2018

Choose a reason for hiding this comment

romainbrenguier commented Feb 15, 2018

romainbrenguier commented Feb 12, 2018 •

edited

Loading