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 <util/optional.h>
13
15
18
19#include <list>
20#include <string>
21
22class goto_functionst;
25
31{
32public:
37
49 void generate(goto_modelt &goto_model, const irep_idt &harness_function_name)
50 override;
51
52protected:
80
85 entry_goto_locationt parse_goto_location(const std::string &cmdl_option);
86
90 {
92 unsigned line_number;
93
99
105 std::pair<goto_programt::const_targett, size_t>
107 const goto_programt::instructionst &instructions) const;
108 };
109
114 entry_source_locationt parse_source_location(const std::string &cmdl_option);
115
131
136 {
137 size_t distance;
141
143 {
144 }
145
147 const size_t &candidate_distance,
148 const irep_idt &candidate_function_name,
149 const goto_programt::const_targett &candidate_instruction)
150 {
151 if(match_found && distance <= candidate_distance)
152 return;
153
154 match_found = true;
155 distance = candidate_distance;
156 function_name = candidate_function_name;
157 instruction = candidate_instruction;
158 }
159 };
160
167 entry_locationt initialize_entry_via_goto(
168 const entry_goto_locationt &entry_goto_location,
169 const goto_functionst &goto_functions);
170
177 entry_locationt initialize_entry_via_source(
178 const entry_source_locationt &entry_source_location,
179 const goto_functionst &goto_functions);
180
184 void handle_option(
185 const std::string &option,
186 const std::list<std::string> &values) override;
187
194 void validate_options(const goto_modelt &goto_model) override;
195
200 const std::string &file,
201 symbol_table_baset &snapshot) const;
202
233 void add_init_section(
234 const symbol_exprt &func_init_done_var,
235 goto_modelt &goto_model) const;
236
243 const symbolt &snapshot_symbol,
244 symbol_table_baset &symbol_table) const;
245
258 const symbol_table_baset &snapshot,
259 goto_modelt &goto_model) const;
260
266 const symbolt &called_function_symbol,
267 code_blockt &code) const;
268
274 goto_modelt &goto_model,
275 const symbolt &function) const;
276
280 size_t pointer_depth(const typet &t) const;
281
282 template <typename Adder>
283 void collect_references(const exprt &expr, Adder &&add_reference) const
284 {
285 if(expr.id() == ID_symbol)
286 add_reference(to_symbol_expr(expr).get_identifier());
287 for(const auto &operand : expr.operands())
288 {
289 collect_references(operand, add_reference);
290 }
291 }
292
295 template <typename Key>
297 {
298 public:
299 using relationt = std::multimap<Key, Key>;
300 using keyst = std::set<Key>;
301
306
307 template <typename T>
308 void sort(
309 const std::vector<std::pair<Key, T>> &input,
310 std::vector<std::pair<Key, T>> &output)
311 {
312 std::unordered_map<Key, T> searchable_input;
313 using valuet = std::pair<Key, T>;
314
315 for(const auto &item : input)
316 {
317 searchable_input[item.first] = item.second;
318 }
319 auto associate_key_with_t =
320 [&searchable_input](const Key &key) -> optionalt<valuet> {
321 if(searchable_input.count(key) != 0)
322 return valuet(key, searchable_input[key]);
323 else
324 return {};
325 };
326 auto push_to_output = [&output](const valuet &value) {
327 output.push_back(value);
328 };
329 for(const auto &item : input)
330 {
331 dfs(item, associate_key_with_t, push_to_output);
332 }
333 }
334
335 private:
337
340
341 template <typename Value, typename Map, typename Handler>
342 void dfs(Value &&node, Map &&key_to_t, Handler &&handle)
343 {
344 PRECONDITION(seen.empty() && inserted.empty());
345 dfs_inner(node, key_to_t, handle);
346 seen.clear();
347 inserted.clear();
348 }
349
350 template <typename Value, typename Map, typename Handler>
351 void dfs_inner(Value &&node, Map &&key_to_t, Handler &&handle)
352 {
353 const Key &key = node.first;
354 if(seen.count(key) == 0)
355 {
356 seen.insert(key);
357 auto key_range = preorder_relation.equal_range(key);
358 for(auto it = key_range.first; it != key_range.second; ++it)
359 {
360 auto maybe_value = key_to_t(it->second);
361 if(maybe_value.has_value())
362 dfs_inner(*maybe_value, key_to_t, handle);
363 }
364 }
365 if(inserted.count(key) != 0)
366 return;
367 handle(node);
368 inserted.insert(key);
369 }
370 };
371
376 std::unordered_set<irep_idt> variables_to_havoc;
377
380
382
384};
385
386#endif // CPROVER_GOTO_HARNESS_MEMORY_SNAPSHOT_HARNESS_GENERATOR_H
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:39
Base class for all expressions.
Definition expr.h:56
operandst & operands()
Definition expr.h:94
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.
const symbolt & fresh_symbol_copy(const symbolt &snapshot_symbol, symbol_table_baset &symbol_table) const
Introduce a new symbol into symbol_table with the same name and type as snapshot_symbol.
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...
code_blockt add_assignments_to_globals(const symbol_table_baset &snapshot, goto_modelt &goto_model) const
For each global symbol in the snapshot symbol table either: 1) add code_assignt assigning a value fro...
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)
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 get_memory_snapshot(const std::string &file, symbol_table_baset &snapshot) const
Parse the snapshot JSON file and initialise the symbol table.
void validate_options(const goto_modelt &goto_model) override
Check that user options make sense: On their own, e.g.
std::string memory_snapshot_file
data to store the command-line options
size_t pointer_depth(const typet &t) const
Recursively compute the pointer depth.
Expression to hold a symbol (variable)
Definition std_expr.h:113
The symbol table base class interface.
Symbol table entry.
Definition symbol.h:28
The type of an expression, extends irept.
Definition type.h:29
Concrete Goto Program.
nonstd::optional< T > optionalt
Definition optional.h:35
#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:222
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)