cprover
Loading...
Searching...
No Matches
memory_snapshot_harness_generator.h
Go to the documentation of this file.
1/******************************************************************\
2
3Module: Harness to initialise memory from memory snapshot
4
5Author: Daniel Poetzl
6
7\******************************************************************/
8
9#ifndef CPROVER_GOTO_HARNESS_MEMORY_SNAPSHOT_HARNESS_GENERATOR_H
10#define CPROVER_GOTO_HARNESS_MEMORY_SNAPSHOT_HARNESS_GENERATOR_H
11
12#include <list>
13#include <string>
14
17
19
20#include <util/message.h>
21#include <util/optional.h>
22
28{
29public:
34
46 void generate(goto_modelt &goto_model, const irep_idt &harness_function_name)
47 override;
48
49protected:
77
82 entry_goto_locationt parse_goto_location(const std::string &cmdl_option);
83
87 {
89 unsigned line_number;
90
96
102 std::pair<goto_programt::const_targett, size_t>
104 const goto_programt::instructionst &instructions) const;
105 };
106
111 entry_source_locationt parse_source_location(const std::string &cmdl_option);
112
128
157
164 entry_locationt initialize_entry_via_goto(
165 const entry_goto_locationt &entry_goto_location,
166 const goto_functionst &goto_functions);
167
174 entry_locationt initialize_entry_via_source(
175 const entry_source_locationt &entry_source_location,
176 const goto_functionst &goto_functions);
177
181 void handle_option(
182 const std::string &option,
183 const std::list<std::string> &values) override;
184
191 void validate_options(const goto_modelt &goto_model) override;
192
196 void
197 get_memory_snapshot(const std::string &file, symbol_tablet &snapshot) const;
198
229 void add_init_section(
231 goto_modelt &goto_model) const;
232
240 symbol_tablet &symbol_table) const;
241
254 const symbol_tablet &snapshot,
255 goto_modelt &goto_model) const;
256
263 code_blockt &code) const;
264
270 goto_modelt &goto_model,
271 const symbolt &function) const;
272
276 size_t pointer_depth(const typet &t) const;
277
278 template <typename Adder>
279 void collect_references(const exprt &expr, Adder &&add_reference) const
280 {
281 if(expr.id() == ID_symbol)
282 add_reference(to_symbol_expr(expr).get_identifier());
283 for(const auto &operand : expr.operands())
284 {
285 collect_references(operand, add_reference);
286 }
287 }
288
291 template <typename Key>
293 {
294 public:
295 using relationt = std::multimap<Key, Key>;
296 using keyst = std::set<Key>;
297
302
303 template <typename T>
304 void sort(
305 const std::vector<std::pair<Key, T>> &input,
306 std::vector<std::pair<Key, T>> &output)
307 {
308 std::unordered_map<Key, T> searchable_input;
309 using valuet = std::pair<Key, T>;
310
311 for(const auto &item : input)
312 {
313 searchable_input[item.first] = item.second;
314 }
317 if(searchable_input.count(key) != 0)
318 return valuet(key, searchable_input[key]);
319 else
320 return {};
321 };
322 auto push_to_output = [&output](const valuet &value) {
323 output.push_back(value);
324 };
325 for(const auto &item : input)
326 {
328 }
329 }
330
331 private:
333
336
337 template <typename Value, typename Map, typename Handler>
338 void dfs(Value &&node, Map &&key_to_t, Handler &&handle)
339 {
340 PRECONDITION(seen.empty() && inserted.empty());
341 dfs_inner(node, key_to_t, handle);
342 seen.clear();
343 inserted.clear();
344 }
345
346 template <typename Value, typename Map, typename Handler>
347 void dfs_inner(Value &&node, Map &&key_to_t, Handler &&handle)
348 {
349 const Key &key = node.first;
350 if(seen.count(key) == 0)
351 {
352 seen.insert(key);
353 auto key_range = preorder_relation.equal_range(key);
354 for(auto it = key_range.first; it != key_range.second; ++it)
355 {
356 auto maybe_value = key_to_t(it->second);
357 if(maybe_value.has_value())
358 dfs_inner(*maybe_value, key_to_t, handle);
359 }
360 }
361 if(inserted.count(key) != 0)
362 return;
363 handle(node);
364 inserted.insert(key);
365 }
366 };
367
372 std::unordered_set<irep_idt> variables_to_havoc;
373
376
378
380};
381
382#endif // CPROVER_GOTO_HARNESS_MEMORY_SNAPSHOT_HARNESS_GENERATOR_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
A codet representing sequential composition of program statements.
Definition std_code.h:130
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:54
operandst & operands()
Definition expr.h:92
A collection of goto functions.
instructionst::const_iterator const_targett
std::list< instructiont > instructionst
const irep_idt & id() const
Definition irep.h:396
Generates a harness which first assigns global variables with values from a given memory snapshot and...
void add_init_section(const symbol_exprt &func_init_done_var, goto_modelt &goto_model) const
Modify the entry-point function to start from the user-specified initial location.
entry_locationt entry_location
data to initialize the entry function
void insert_harness_function_into_goto_model(goto_modelt &goto_model, const symbolt &function) const
Insert the function into the symbol table (and the goto functions map) of the goto_model.
entry_locationt initialize_entry_via_goto(const entry_goto_locationt &entry_goto_location, const goto_functionst &goto_functions)
Find and return the entry instruction (requested by the user as goto location: function name + locati...
entry_source_locationt parse_source_location(const std::string &cmdl_option)
Parse a command line option to extract the user specified entry source location.
entry_locationt initialize_entry_via_source(const entry_source_locationt &entry_source_location, const goto_functionst &goto_functions)
Find and return the entry instruction (requested by the user as source location: file name + line num...
memory_snapshot_harness_generatort(message_handlert &message_handler)
void handle_option(const std::string &option, const std::list< std::string > &values) override
Collect the memory-snapshot specific cmdline options (one at a time)
void get_memory_snapshot(const std::string &file, symbol_tablet &snapshot) const
Parse the snapshot JSON file and initialise the symbol table.
entry_goto_locationt parse_goto_location(const std::string &cmdl_option)
Parse a command line option to extract the user specified entry goto location.
void collect_references(const exprt &expr, Adder &&add_reference) const
void generate(goto_modelt &goto_model, const irep_idt &harness_function_name) override
The main function of this harness, consists of the following:
void add_call_with_nondet_arguments(const symbolt &called_function_symbol, code_blockt &code) const
Create as many non-deterministic arguments as there are arguments of the called_function_symbol and a...
recursive_initialization_configt recursive_initialization_config
void validate_options(const goto_modelt &goto_model) override
Check that user options make sense: On their own, e.g.
const symbolt & fresh_symbol_copy(const symbolt &snapshot_symbol, symbol_tablet &symbol_table) const
Introduce a new symbol into symbol_table with the same name and type as snapshot_symbol.
std::string memory_snapshot_file
data to store the command-line options
code_blockt add_assignments_to_globals(const symbol_tablet &snapshot, goto_modelt &goto_model) const
For each global symbol in the snapshot symbol table either: 1) add code_assignt assigning a value fro...
size_t pointer_depth(const typet &t) const
Recursively compute the pointer depth.
Expression to hold a symbol (variable)
Definition std_expr.h:80
The symbol table.
Symbol table entry.
Definition symbol.h:28
The type of an expression, extends irept.
Definition type.h:29
Symbol Table + CFG.
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define PRECONDITION(CONDITION)
Definition invariant.h:463
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
Definition kdev_t.h:19
User provided goto location: function name and (maybe) location number; the structure wraps this opti...
goto_programt::const_targett find_first_corresponding_instruction(const goto_programt::instructionst &instructions) const
Returns the first goto_programt::instructiont represented by this goto location, i....
entry_goto_locationt(irep_idt function_name, unsigned location_number)
Wraps the information needed to identify the entry point.
entry_locationt(irep_idt function_name, goto_programt::const_targett start_instruction)
User provided source location: file name and line number; the structure wraps this option with a pars...
std::pair< goto_programt::const_targett, size_t > find_first_corresponding_instruction(const goto_programt::instructionst &instructions) const
Returns the first goto_programt::instructiont represented by this source location,...
void sort(const std::vector< std::pair< Key, T > > &input, std::vector< std::pair< Key, T > > &output)
void dfs(Value &&node, Map &&key_to_t, Handler &&handle)
void dfs_inner(Value &&node, Map &&key_to_t, Handler &&handle)
Wraps the information for source location match candidates.
void match_up(const size_t &candidate_distance, const irep_idt &candidate_function_name, const goto_programt::const_targett &candidate_instruction)