Go to the documentation of this file.
34 const std::string &option,
35 const std::list<std::string> &values)
46 values.begin(), values.end());
50 for(
auto const &array_size_pair : values)
68 "can not have two associated array sizes for one array",
75 "'" + array_size_pair +
76 "' is in an invalid format for array size pair",
78 "array_name:size_name, where both are the names of global "
93 std::vector<std::string> havoc_candidates =
95 for(
const auto &candidate : havoc_candidates)
107 "unrecognized option for memory snapshot harness generator",
118 "option --memory_snapshot is required",
119 "--harness-type initialise-from-memory-snapshot");
125 "choose either source or goto location to specify the entry point",
126 "--initial-source/goto-location");
144 const symbolt *called_function_symbol =
147 if(called_function_symbol ==
nullptr)
151 "` not found in the symbol table",
152 "--initial-location");
173 ins_it1->guard = func_init_done_var;
188 const symbolt &snapshot_symbol,
192 snapshot_symbol.
type,
196 snapshot_symbol.
mode,
206 if(t.
id() != ID_pointer)
219 std::vector<std::pair<irep_idt, symbolt>> ordered_snapshot_symbols;
224 std::vector<std::pair<irep_idt, symbolt>> selected_snapshot_symbols;
226 relationt reference_relation;
228 for(
const auto &snapshot_pair : snapshot)
230 const auto name =
id2string(snapshot_pair.first);
234 snapshot_pair.second.value,
235 [&reference_relation, &snapshot_pair](
const irep_idt &
id) {
236 reference_relation.insert(std::make_pair(snapshot_pair.first, id));
238 selected_snapshot_symbols.push_back(snapshot_pair);
242 reference_order.
sort(selected_snapshot_symbols, ordered_snapshot_symbols);
250 const auto &global_symbol = pair.second;
253 auto symeexr = global_symbol.symbol_expr();
254 if(symeexr.type() == global_symbol.value.type())
259 for(
const auto &pair : ordered_snapshot_symbols)
261 const symbolt &snapshot_symbol = pair.second;
264 auto should_get_fresh = [&symbol_table](
const symbolt &symbol) {
265 return symbol_table.
lookup(symbol.base_name) ==
nullptr &&
268 const symbolt &fresh_or_snapshot_symbol =
269 should_get_fresh(snapshot_symbol)
274 fresh_or_snapshot_symbol))
280 fresh_or_snapshot_symbol.
value});
284 recursive_initialization.initialize(
294 const symbolt &called_function_symbol,
308 std::move(arguments)});
324 goto_functiont &harness_function = function_iterator_pair.first->second;
333 const std::string &
file,
350 for(
auto const &arr_element : jarr)
352 if(!arr_element.is_object())
355 const auto it = json_obj.find(
"symbolTable");
356 if(it != json_obj.end())
363 "JSON memory snapshot does not contain symbol table");
376 const irep_idt &harness_function_name)
384 const symbolt *called_function_symbol =
395 called_function_symbol->
mode,
397 func_init_done_symbol.is_static_lifetime =
true;
399 symbol_exprt func_init_done_var = func_init_done_symbol.symbol_expr();
409 *called_function_symbol, harness_function_body);
413 symbolt harness_function_symbol;
414 harness_function_symbol.
name = harness_function_name;
415 harness_function_symbol.
base_name = harness_function_name;
416 harness_function_symbol.
pretty_name = harness_function_name;
418 harness_function_symbol.
is_lvalue =
true;
419 harness_function_symbol.
mode = called_function_symbol->
mode;
421 harness_function_symbol.
value = harness_function_body;
431 const std::string &cmdl_option)
433 std::vector<std::string> start =
split_string(cmdl_option,
':',
true);
436 start.empty() || start.front().empty() ||
437 (start.size() == 2 && start.back().empty()) || start.size() > 2)
440 "invalid initial location specification",
"--initial-location");
443 if(start.size() == 2)
457 const std::string &cmdl_option)
459 std::string initial_file_string;
460 std::string initial_line_string;
462 cmdl_option,
':', initial_file_string, initial_line_string,
true);
464 if(initial_file_string.empty() || initial_line_string.empty())
467 "invalid initial location specification",
"--initial-file-line");
485 const auto &goto_function =
489 goto_function->second.body_available())
491 const auto &goto_program = goto_function->second.body;
493 const auto corresponding_instruction =
495 goto_program.instructions);
497 if(corresponding_instruction != goto_program.instructions.end())
501 "could not find the specified entry point",
"--initial-goto-location");
515 const auto &goto_function = entry.second;
517 const auto &goto_program = goto_function.body;
519 const auto candidate_instruction =
521 goto_program.instructions);
523 if(candidate_instruction.first != goto_program.instructions.end())
526 candidate_instruction.second, entry.first, candidate_instruction.first);
534 "could not find the specified entry point",
"--initial-source-location");
541 if(!location_number.has_value())
542 return instructions.begin();
545 instructions.begin(),
548 return *location_number == instruction.location_number;
552 std::pair<goto_programt::const_targett, size_t>
557 auto it = std::find_if(
558 instructions.begin(),
561 return instruction.source_location.get_file() == file_name &&
562 safe_string2unsigned(id2string(
563 instruction.source_location.get_line())) >= line_number;
566 if(it == instructions.end())
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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...
A codet representing sequential composition of program statements.
void match_up(const size_t &candidate_distance, const irep_idt &candidate_function_name, const goto_programt::const_targett &candidate_instruction)
entry_goto_locationt parse_goto_location(const std::string &cmdl_option)
Parse a command line option to extract the user specified entry goto location.
const typet & subtype() const
std::multimap< Key, Key > relationt
#define MEMORY_SNAPSHOT_HARNESS_HAVOC_VARIABLES_OPT
#define CHECK_RETURN(CONDITION)
The type of an expression, extends irept.
Fresh auxiliary symbol creation.
typet type
Type of symbol.
Class for generating initialisation code for compound structures.
std::list< instructiont > instructionst
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
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)
static const source_locationt & nil()
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,...
Wraps the information for source location match candidates.
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
std::map< irep_idt, irep_idt > array_name_to_associated_array_size_variable
std::string memory_snapshot_file
data to store the command-line options
irep_idt base_name
Base (non-scoped) name.
void validate_options(const goto_modelt &goto_model) override
Check that user options make sense: On their own, e.g.
entry_source_locationt parse_source_location(const std::string &cmdl_option)
Parse a command line option to extract the user specified entry source location.
recursive_initialization_configt recursive_initialization_config
std::string require_exactly_one_value(const std::string &option, const std::list< std::string > &values)
Returns the only value of a single element list, throws an exception if not passed a single element l...
function_mapt function_map
json_arrayt & to_json_array(jsont &json)
Expression to hold a symbol (variable)
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
message_handlert & message_handler
irep_idt pretty_name
Language-specific display name.
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
std::set< irep_idt > pointers_to_treat_as_arrays
typet & type()
Return the type of the expression.
#define MEMORY_SNAPSHOT_HARNESS_INITIAL_SOURCE_LOC_OPT
codet representation of a function call statement.
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
User provided goto location: function name and (maybe) location number; the structure wraps this opti...
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...
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
optionalt< unsigned > string2optional_unsigned(const std::string &str, int base)
Convert string to unsigned similar to the stoul or stoull functions, return nullopt when the conversi...
irep_idt mode
Language mode.
const std::string & id2string(const irep_idt &d)
#define MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT
Wraps the information needed to identify the entry point.
#define PRECONDITION(CONDITION)
goto_programt::const_targett start_instruction
void compute_location_numbers(unsigned &nr)
Compute location numbers.
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
#define MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
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.
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.
const irep_idt & id() const
A goto function, consisting of function type (see type), function body (see body),...
exprt::operandst argumentst
goto_programt::const_targett instruction
void add(const codet &code)
The Boolean constant false.
std::unordered_set< irep_idt > variables_to_havoc
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...
const parameterst & parameters() const
std::string initial_source_location_line
bool handle_option(const std::string &option, const std::list< std::string > &values)
Parse the options specific for recursive initialisation.
unsigned safe_string2unsigned(const std::string &str, int base)
void get_memory_snapshot(const std::string &file, symbol_tablet &snapshot) const
Parse the snapshot JSON file and initialise the symbol table.
#define MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT
A side_effect_exprt that returns a non-deterministically chosen value.
User provided source location: file name and line number; the structure wraps this option with a pars...
instructionst instructions
The list of instructions in the goto program.
std::string initial_goto_location_line
A collection of goto functions.
exprt value
Initial value of symbol.
goto_functionst goto_functions
GOTO functions.
void generate(goto_modelt &goto_model, const irep_idt &harness_function_name) override
The main function of this harness, consists of the following:
json_objectt & to_json_object(jsont &json)
source_locationt location
Source code location of definition of symbol.
targett const_cast_target(const_targett t)
Convert a const_targett to a targett - use with care and avoid whenever possible.
entry_locationt entry_location
data to initialize the entry function
void collect_references(const exprt &expr, Adder &&add_reference) const
#define MEMORY_SNAPSHOT_HARNESS_INITIAL_GOTO_LOC_OPT
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....
size_t pointer_depth(const typet &t) const
Recursively compute the pointer depth.
A generic container class for the GOTO intermediate representation of one function.
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
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...
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
instructionst::const_iterator const_targett
code_typet type
The type of the function, indicating the return type and parameter types.
void sort(const std::vector< std::pair< Key, T >> &input, std::vector< std::pair< Key, T >> &output)
Goto Programs with Functions.
unsignedbv_typet size_type()
A codet representing an assignment in the program.
The Boolean constant true.
static bool is_initialization_allowed(const symbolt &symbol)
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
bool parse_json(std::istream &in, const std::string &filename, message_handlert &message_handler, jsont &dest)
This class represents an instruction in the GOTO intermediate representation.
Simple structure for linearising posets.
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.
symbol_tablet symbol_table
Symbol table.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
irep_idt name
The unique identifier.
void symbol_table_from_json(const jsont &in, symbol_tablet &symbol_table)