Bytecode index aware block selection in coverage instrumentation [TG-1404] #3
Conversation
This is more explicit that using goto_program.instructions.end to denote the empty case.
This does not need to be exposed in the interface of the class, and is only working on the block_info member.
We pull this function out of the cover_basic_blockst constructor, as the constructor is rather long, and having a function for this part makes this part of the code clearer.
Put type definition at the beggining. Remove typedef that are used only once (they hide what the type actually is). Use private membres instead of protected.
This will allow to have two implementations for this functor.
romainbrenguier
changed the title
| #include <goto-programs/goto_model.h> | ||
| #include "cover_basic_blocks.h" | ||
|
|
||
| class cover_location_blockst : public cover_blocks_baset |
There was a problem hiding this comment.
I suggest to rename to 'cover_basic_blocks_javat'
There was a problem hiding this comment.
You can even move this into the same cover_basic_blocks.h/cpp file. It's not huge.
| message_handlert &message_handler){}; | ||
| }; | ||
|
|
||
| class cover_basic_blockst : public cover_blocks_baset |
There was a problem hiding this comment.
You could make the language-independent instrumentation be done by the base class, i.e. there is then only a cover_basic_blockst and a derived cover_basic_blocks_javat.
Provide a virtual method for constructing the blocks instead of doing it in the constructor.
| /// the java bytecode indices for each basic block is unique | ||
| /// \param goto_program The goto program | ||
| /// \param message_handler The message handler | ||
| virtual void select_unique_java_bytecode_indices( |
| @@ -38,31 +38,15 @@ struct cover_configt | |||
| { | |||
| bool keep_assertions; | |||
| bool traces_must_terminate; | |||
| bool java_bytecode; | |||
There was a problem hiding this comment.
The cover_instrumenter should already know about that.
| function_filterst function_filters; | ||
| goal_filterst goal_filters; | ||
| cover_instrumenterst cover_instrumenters; | ||
| }; | ||
|
|
||
| void instrument_cover_goals( |
There was a problem hiding this comment.
Do not remove these methods. They are kept for legacy reasons.
|
|
||
| // Hackish way of finding whether we should instrument as bytecode | ||
| config->java_bytecode = | ||
| symbol_table.lookup(CPROVER_PREFIX "initialize")->mode == ID_java; |
| function.body, | ||
| config.cover_instrumenters, | ||
| message_handler, | ||
| config.java_bytecode); |
There was a problem hiding this comment.
get the mode of the function symbol from the symbol table
| @@ -18,7 +18,46 @@ Author: Daniel Kroening | |||
|
|
|||
| class message_handlert; | |||
|
|
|||
| class cover_basic_blockst | |||
| class cover_blocks_baset | |||
There was a problem hiding this comment.
No need to rename this. The base class should provide the language-independent (=goto) case.
| forall_goto_program_instructions(it, _goto_program) | ||
| { | ||
| const auto &bytecode_index = it->source_location.get_java_bytecode_index(); | ||
| if(!index_to_block.count(bytecode_index)) |
There was a problem hiding this comment.
Covering each bytecode is too much. Restrict to function entry, function exit, gotos and function calls.
| class cover_location_blockst : public cover_blocks_baset | ||
| { | ||
| public: | ||
| struct block_infot |
There was a problem hiding this comment.
Not sure why the data structure from the cover_basic_blockst is insufficient. The bytecode index is part of the source location.
romainbrenguier
force-pushed
the
refactor/coverage-instrumentation
branch
from
3ef6759 to
3454ef1
Compare
|
replaced by #4 |
romainbrenguier
force-pushed
the
refactor/coverage-instrumentation
branch
5 times, most recently
from
eb6463f to
6492b3a
Compare
|
Actual PR on CBMC: diffblue#1830 |
No description provided.