cprover
memory_snapshot_harness_generator.cpp
Go to the documentation of this file.
1 /******************************************************************\
2 
3 Module: Harness to initialise memory from memory snapshot
4 
5 Author: Daniel Poetzl
6 
7 \******************************************************************/
8 
9 #include <algorithm>
10 
13 
15 
16 #include <json/json_parser.h>
17 
19 
20 #include <util/arith_tools.h>
21 #include <util/c_types.h>
22 #include <util/exception_utils.h>
23 #include <util/fresh_symbol.h>
24 #include <util/message.h>
25 #include <util/string2int.h>
26 #include <util/string_utils.h>
27 #include <util/symbol_table.h>
28 
30 
32 
34  const std::string &option,
35  const std::list<std::string> &values)
36 {
40  {
41  // the option belongs to recursive initialization
42  }
44  {
46  values.begin(), values.end());
47  }
49  {
50  for(auto const &array_size_pair : values)
51  {
52  try
53  {
54  std::string array;
55  std::string size;
56  split_string(array_size_pair, ':', array, size);
57  // --associated-array-size implies --treat-pointer-as-array
58  // but it is not an error to specify both, so we don't check
59  // for duplicates here
61  array);
62  auto const inserted =
65  if(!inserted.second)
66  {
68  "can not have two associated array sizes for one array",
70  }
71  }
72  catch(const deserialization_exceptiont &)
73  {
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 "
79  "variables"};
80  }
81  }
82  }
83  else if(option == MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT)
84  {
86  }
88  {
90  }
92  {
93  std::vector<std::string> havoc_candidates =
94  split_string(values.front(), ',', true);
95  for(const auto &candidate : havoc_candidates)
96  {
97  variables_to_havoc.insert(candidate);
98  }
99  }
101  {
103  }
104  else
105  {
107  "unrecognized option for memory snapshot harness generator",
108  "--" + option);
109  }
110 }
111 
113  const goto_modelt &goto_model)
114 {
115  if(memory_snapshot_file.empty())
116  {
118  "option --memory_snapshot is required",
119  "--harness-type initialise-from-memory-snapshot");
120  }
121 
123  {
125  "choose either source or goto location to specify the entry point",
126  "--initial-source/goto-location");
127  }
128 
129  if(!initial_source_location_line.empty())
130  {
133  goto_model.goto_functions);
134  }
135  else
136  {
139  goto_model.goto_functions);
140  }
141 
142  const symbol_tablet &symbol_table = goto_model.symbol_table;
143 
144  const symbolt *called_function_symbol =
145  symbol_table.lookup(entry_location.function_name);
146 
147  if(called_function_symbol == nullptr)
148  {
150  "function `" + id2string(entry_location.function_name) +
151  "` not found in the symbol table",
152  "--initial-location");
153  }
154 }
155 
157  const symbol_exprt &func_init_done_var,
158  goto_modelt &goto_model) const
159 {
160  goto_functionst &goto_functions = goto_model.goto_functions;
161 
162  goto_functiont &goto_function =
163  goto_functions.function_map[entry_location.function_name];
164 
165  goto_programt &goto_program = goto_function.body;
166 
167  const goto_programt::const_targett start_it =
168  goto_program.instructions.begin();
169 
170  auto ins_it1 = goto_program.insert_before(
171  start_it,
172  goto_programt::make_goto(goto_program.const_cast_target(start_it)));
173  ins_it1->guard = func_init_done_var;
174 
175  auto ins_it2 = goto_program.insert_after(
176  ins_it1,
178  code_assignt(func_init_done_var, true_exprt())));
179 
180  goto_program.compute_location_numbers();
181  goto_program.insert_after(
182  ins_it2,
185 }
186 
188  const symbolt &snapshot_symbol,
189  symbol_tablet &symbol_table) const
190 {
191  symbolt &tmp_symbol = get_fresh_aux_symbol(
192  snapshot_symbol.type,
193  "", // no prefix name
194  id2string(snapshot_symbol.base_name),
195  snapshot_symbol.location,
196  snapshot_symbol.mode,
197  symbol_table);
198  tmp_symbol.is_static_lifetime = true;
199  tmp_symbol.value = snapshot_symbol.value;
200 
201  return tmp_symbol;
202 }
203 
205 {
206  if(t.id() != ID_pointer)
207  return 0;
208  else
209  return pointer_depth(t.subtype()) + 1;
210 }
211 
213  const symbol_tablet &snapshot,
214  goto_modelt &goto_model) const
215 {
216  recursive_initializationt recursive_initialization{
217  recursive_initialization_config, goto_model};
218 
219  std::vector<std::pair<irep_idt, symbolt>> ordered_snapshot_symbols;
220  // sort the snapshot symbols so that the non-pointer symbols are first, then
221  // pointers, then pointers-to-pointers, etc. so that we don't assign
222  // uninitialized values
223  {
224  std::vector<std::pair<irep_idt, symbolt>> selected_snapshot_symbols;
225  using relationt = typename preordert<irep_idt>::relationt;
226  relationt reference_relation;
227 
228  for(const auto &snapshot_pair : snapshot)
229  {
230  const auto name = id2string(snapshot_pair.first);
231  if(name.find(CPROVER_PREFIX) != 0)
232  {
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));
237  });
238  selected_snapshot_symbols.push_back(snapshot_pair);
239  }
240  }
241  preordert<irep_idt> reference_order{reference_relation};
242  reference_order.sort(selected_snapshot_symbols, ordered_snapshot_symbols);
243  }
244 
245  code_blockt code{};
246 
247  // add initialization for existing globals
248  for(const auto &pair : goto_model.symbol_table)
249  {
250  const auto &global_symbol = pair.second;
252  {
253  auto symeexr = global_symbol.symbol_expr();
254  if(symeexr.type() == global_symbol.value.type())
255  code.add(code_assignt{symeexr, global_symbol.value});
256  }
257  }
258 
259  for(const auto &pair : ordered_snapshot_symbols)
260  {
261  const symbolt &snapshot_symbol = pair.second;
262  symbol_tablet &symbol_table = goto_model.symbol_table;
263 
264  auto should_get_fresh = [&symbol_table](const symbolt &symbol) {
265  return symbol_table.lookup(symbol.base_name) == nullptr &&
266  !symbol.is_type;
267  };
268  const symbolt &fresh_or_snapshot_symbol =
269  should_get_fresh(snapshot_symbol)
270  ? fresh_symbol_copy(snapshot_symbol, symbol_table)
271  : snapshot_symbol;
272 
274  fresh_or_snapshot_symbol))
275  continue;
276 
277  if(variables_to_havoc.count(fresh_or_snapshot_symbol.base_name) == 0)
278  {
279  code.add(code_assignt{fresh_or_snapshot_symbol.symbol_expr(),
280  fresh_or_snapshot_symbol.value});
281  }
282  else
283  {
284  recursive_initialization.initialize(
285  fresh_or_snapshot_symbol.symbol_expr(),
286  from_integer(0, size_type()),
287  code);
288  }
289  }
290  return code;
291 }
292 
294  const symbolt &called_function_symbol,
295  code_blockt &code) const
296 {
297  const code_typet &code_type = to_code_type(called_function_symbol.type);
298 
300 
301  for(const code_typet::parametert &parameter : code_type.parameters())
302  {
303  arguments.push_back(side_effect_expr_nondett{
304  parameter.type(), called_function_symbol.location});
305  }
306 
307  code.add(code_function_callt{called_function_symbol.symbol_expr(),
308  std::move(arguments)});
309 }
310 
313  goto_modelt &goto_model,
314  const symbolt &function) const
315 {
316  const auto r = goto_model.symbol_table.insert(function);
317  CHECK_RETURN(r.second);
318 
319  auto function_iterator_pair = goto_model.goto_functions.function_map.emplace(
320  function.name, goto_functiont{});
321 
322  CHECK_RETURN(function_iterator_pair.second);
323 
324  goto_functiont &harness_function = function_iterator_pair.first->second;
325  harness_function.type = to_code_type(function.type);
326 
327  goto_convert(
328  goto_model.symbol_table, goto_model.goto_functions, message_handler);
329  harness_function.body.add(goto_programt::make_end_function());
330 }
331 
333  const std::string &file,
334  symbol_tablet &snapshot) const
335 {
336  jsont json;
337 
339 
340  if(r)
341  {
342  throw deserialization_exceptiont("failed to read JSON memory snapshot");
343  }
344 
345  if(json.is_array())
346  {
347  // since memory-analyzer produces an array JSON we need to search it
348  // to find the first JSON object that is a symbol table
349  const auto &jarr = to_json_array(json);
350  for(auto const &arr_element : jarr)
351  {
352  if(!arr_element.is_object())
353  continue;
354  const auto &json_obj = to_json_object(arr_element);
355  const auto it = json_obj.find("symbolTable");
356  if(it != json_obj.end())
357  {
358  symbol_table_from_json(json_obj, snapshot);
359  return;
360  }
361  }
363  "JSON memory snapshot does not contain symbol table");
364  }
365  else
366  {
367  // throws a deserialization_exceptiont or an
368  // incorrect_goto_program_exceptiont
369  // on failure to read JSON symbol table
370  symbol_table_from_json(json, snapshot);
371  }
372 }
373 
375  goto_modelt &goto_model,
376  const irep_idt &harness_function_name)
377 {
378  symbol_tablet snapshot;
380 
381  symbol_tablet &symbol_table = goto_model.symbol_table;
382  goto_functionst &goto_functions = goto_model.goto_functions;
383 
384  const symbolt *called_function_symbol =
385  symbol_table.lookup(entry_location.function_name);
386  recursive_initialization_config.mode = called_function_symbol->mode;
387 
388  // introduce a symbol for a Boolean variable to indicate the point at which
389  // the function initialisation is completed
390  auto &func_init_done_symbol = get_fresh_aux_symbol(
391  bool_typet(),
393  "func_init_done",
395  called_function_symbol->mode,
396  symbol_table);
397  func_init_done_symbol.is_static_lifetime = true;
398  func_init_done_symbol.value = false_exprt();
399  symbol_exprt func_init_done_var = func_init_done_symbol.symbol_expr();
400 
401  add_init_section(func_init_done_var, goto_model);
402 
403  code_blockt harness_function_body =
404  add_assignments_to_globals(snapshot, goto_model);
405 
406  harness_function_body.add(code_assignt{func_init_done_var, false_exprt{}});
407 
409  *called_function_symbol, harness_function_body);
410 
411  // Create harness function symbol
412 
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;
417 
418  harness_function_symbol.is_lvalue = true;
419  harness_function_symbol.mode = called_function_symbol->mode;
420  harness_function_symbol.type = code_typet({}, empty_typet());
421  harness_function_symbol.value = harness_function_body;
422 
423  // Add harness function to goto model and symbol table
424  insert_harness_function_into_goto_model(goto_model, harness_function_symbol);
425 
426  goto_functions.update();
427 }
428 
431  const std::string &cmdl_option)
432 {
433  std::vector<std::string> start = split_string(cmdl_option, ':', true);
434 
435  if(
436  start.empty() || start.front().empty() ||
437  (start.size() == 2 && start.back().empty()) || start.size() > 2)
438  {
440  "invalid initial location specification", "--initial-location");
441  }
442 
443  if(start.size() == 2)
444  {
445  const auto location_number = string2optional_unsigned(start.back());
446  CHECK_RETURN(location_number.has_value());
447  return entry_goto_locationt{start.front(), *location_number};
448  }
449  else
450  {
451  return entry_goto_locationt{start.front()};
452  }
453 }
454 
457  const std::string &cmdl_option)
458 {
459  std::string initial_file_string;
460  std::string initial_line_string;
461  split_string(
462  cmdl_option, ':', initial_file_string, initial_line_string, true);
463 
464  if(initial_file_string.empty() || initial_line_string.empty())
465  {
467  "invalid initial location specification", "--initial-file-line");
468  }
469 
470  const auto line_number = string2optional_unsigned(initial_line_string);
471  CHECK_RETURN(line_number.has_value());
472  return entry_source_locationt{initial_file_string, *line_number};
473 }
474 
477  const entry_goto_locationt &entry_goto_location,
478  const goto_functionst &goto_functions)
479 {
480  PRECONDITION(!entry_goto_location.function_name.empty());
481  const irep_idt &function_name = entry_goto_location.function_name;
482 
483  // by function(+location): search for the function then jump to n-th
484  // location, then check the number
485  const auto &goto_function =
486  goto_functions.function_map.find(entry_goto_location.function_name);
487  if(
488  goto_function != goto_functions.function_map.end() &&
489  goto_function->second.body_available())
490  {
491  const auto &goto_program = goto_function->second.body;
492 
493  const auto corresponding_instruction =
494  entry_goto_location.find_first_corresponding_instruction(
495  goto_program.instructions);
496 
497  if(corresponding_instruction != goto_program.instructions.end())
498  return entry_locationt{function_name, corresponding_instruction};
499  }
501  "could not find the specified entry point", "--initial-goto-location");
502 }
503 
506  const entry_source_locationt &entry_source_location,
507  const goto_functionst &goto_functions)
508 {
509  PRECONDITION(!entry_source_location.file_name.empty());
510 
511  source_location_matcht best_match;
512  // by line: iterate over all instructions until source location match
513  for(const auto &entry : goto_functions.function_map)
514  {
515  const auto &goto_function = entry.second;
516  // if !body_available() then body.instruction.empty() and that's fine
517  const auto &goto_program = goto_function.body;
518 
519  const auto candidate_instruction =
520  entry_source_location.find_first_corresponding_instruction(
521  goto_program.instructions);
522 
523  if(candidate_instruction.first != goto_program.instructions.end())
524  {
525  best_match.match_up(
526  candidate_instruction.second, entry.first, candidate_instruction.first);
527  }
528  }
529 
530  if(best_match.match_found)
531  return entry_locationt{best_match.function_name, best_match.instruction};
532  else
534  "could not find the specified entry point", "--initial-source-location");
535 }
536 
539  const goto_programt::instructionst &instructions) const
540 {
541  if(!location_number.has_value())
542  return instructions.begin();
543 
544  return std::find_if(
545  instructions.begin(),
546  instructions.end(),
547  [this](const goto_programt::instructiont &instruction) {
548  return *location_number == instruction.location_number;
549  });
550 }
551 
552 std::pair<goto_programt::const_targett, size_t>
555  const goto_programt::instructionst &instructions) const
556 {
557  auto it = std::find_if(
558  instructions.begin(),
559  instructions.end(),
560  [this](const goto_programt::instructiont &instruction) {
561  return instruction.source_location.get_file() == file_name &&
562  safe_string2unsigned(id2string(
563  instruction.source_location.get_line())) >= line_number;
564  });
565 
566  if(it == instructions.end())
567  return {it, 0};
568  else
569  return {it,
570  safe_string2unsigned(id2string(it->source_location.get_line())) -
571  line_number};
572 }
exception_utils.h
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
goto_functiont::body
goto_programt body
Definition: goto_function.h:30
memory_snapshot_harness_generatort::initialize_entry_via_goto
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...
Definition: memory_snapshot_harness_generator.cpp:476
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
memory_snapshot_harness_generatort::source_location_matcht::match_up
void match_up(const size_t &candidate_distance, const irep_idt &candidate_function_name, const goto_programt::const_targett &candidate_instruction)
Definition: memory_snapshot_harness_generator.h:143
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
memory_snapshot_harness_generatort::parse_goto_location
entry_goto_locationt parse_goto_location(const std::string &cmdl_option)
Parse a command line option to extract the user specified entry goto location.
Definition: memory_snapshot_harness_generator.cpp:430
typet::subtype
const typet & subtype() const
Definition: type.h:47
memory_snapshot_harness_generatort::preordert::relationt
std::multimap< Key, Key > relationt
Definition: memory_snapshot_harness_generator.h:295
MEMORY_SNAPSHOT_HARNESS_HAVOC_VARIABLES_OPT
#define MEMORY_SNAPSHOT_HARNESS_HAVOC_VARIABLES_OPT
Definition: memory_snapshot_harness_generator_options.h:17
arith_tools.h
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
string_utils.h
typet
The type of an expression, extends irept.
Definition: type.h:29
fresh_symbol.h
Fresh auxiliary symbol creation.
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
recursive_initializationt
Class for generating initialisation code for compound structures.
Definition: recursive_initialization.h:63
goto_programt::instructionst
std::list< instructiont > instructionst
Definition: goto_program.h:577
deserialization_exceptiont
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
Definition: exception_utils.h:73
memory_snapshot_harness_generatort::handle_option
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)
Definition: memory_snapshot_harness_generator.cpp:33
source_locationt::nil
static const source_locationt & nil()
Definition: source_location.h:188
memory_snapshot_harness_generatort::entry_source_locationt::find_first_corresponding_instruction
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,...
Definition: memory_snapshot_harness_generator.cpp:554
goto_harness_generator_factory.h
file
Definition: kdev_t.h:19
memory_snapshot_harness_generatort::source_location_matcht
Wraps the information for source location match candidates.
Definition: memory_snapshot_harness_generator.h:133
goto_programt::make_end_function
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:957
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:686
recursive_initialization_configt::array_name_to_associated_array_size_variable
std::map< irep_idt, irep_idt > array_name_to_associated_array_size_variable
Definition: recursive_initialization.h:39
memory_snapshot_harness_generatort::memory_snapshot_file
std::string memory_snapshot_file
data to store the command-line options
Definition: memory_snapshot_harness_generator.h:369
goto_modelt
Definition: goto_model.h:26
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
memory_snapshot_harness_generatort::validate_options
void validate_options(const goto_modelt &goto_model) override
Check that user options make sense: On their own, e.g.
Definition: memory_snapshot_harness_generator.cpp:112
memory_snapshot_harness_generatort::parse_source_location
entry_source_locationt parse_source_location(const std::string &cmdl_option)
Parse a command line option to extract the user specified entry source location.
Definition: memory_snapshot_harness_generator.cpp:456
memory_snapshot_harness_generatort::recursive_initialization_config
recursive_initialization_configt recursive_initialization_config
Definition: memory_snapshot_harness_generator.h:379
memory_snapshot_harness_generator_options.h
bool_typet
The Boolean type.
Definition: std_types.h:37
harness_options_parser::require_exactly_one_value
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...
Definition: goto_harness_generator.cpp:21
recursive_initialization_configt::mode
irep_idt mode
Definition: recursive_initialization.h:30
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
to_json_array
json_arrayt & to_json_array(jsont &json)
Definition: json.h:426
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
jsont
Definition: json.h:27
goto_programt::make_assignment
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:1024
goto_programt::make_goto
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:998
memory_snapshot_harness_generatort::entry_locationt::function_name
irep_idt function_name
Definition: memory_snapshot_harness_generator.h:117
memory_snapshot_harness_generatort::message_handler
message_handlert & message_handler
Definition: memory_snapshot_harness_generator.h:377
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
json_parser.h
goto_convert
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Definition: goto_convert.cpp:1846
recursive_initialization_configt::pointers_to_treat_as_arrays
std::set< irep_idt > pointers_to_treat_as_arrays
Definition: recursive_initialization.h:37
string2int.h
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
MEMORY_SNAPSHOT_HARNESS_INITIAL_SOURCE_LOC_OPT
#define MEMORY_SNAPSHOT_HARNESS_INITIAL_SOURCE_LOC_OPT
Definition: memory_snapshot_harness_generator_options.h:16
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
split_string
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Definition: string_utils.cpp:40
memory_snapshot_harness_generatort::entry_goto_locationt
User provided goto location: function name and (maybe) location number; the structure wraps this opti...
Definition: memory_snapshot_harness_generator.h:53
memory_snapshot_harness_generatort::add_assignments_to_globals
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...
Definition: memory_snapshot_harness_generator.cpp:212
goto_programt::insert_before
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:639
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
string2optional_unsigned
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...
Definition: string2int.cpp:67
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
memory_snapshot_harness_generatort::entry_source_locationt::file_name
irep_idt file_name
Definition: memory_snapshot_harness_generator.h:88
empty_typet
The empty type.
Definition: std_types.h:46
memory_snapshot_harness_generatort::source_location_matcht::function_name
irep_idt function_name
Definition: memory_snapshot_harness_generator.h:135
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT
#define MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT
Definition: memory_snapshot_harness_generator_options.h:18
memory_snapshot_harness_generatort::entry_locationt
Wraps the information needed to identify the entry point.
Definition: memory_snapshot_harness_generator.h:116
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
memory_snapshot_harness_generatort::entry_locationt::start_instruction
goto_programt::const_targett start_instruction
Definition: memory_snapshot_harness_generator.h:118
goto_programt::compute_location_numbers
void compute_location_numbers(unsigned &nr)
Compute location numbers.
Definition: goto_program.h:729
json
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:114
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT
#define MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT
Definition: memory_snapshot_harness_generator_options.h:19
symbol_tablet::insert
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Definition: symbol_table.cpp:19
memory_snapshot_harness_generatort::fresh_symbol_copy
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.
Definition: memory_snapshot_harness_generator.cpp:187
code_typet
Base type of functions.
Definition: std_types.h:736
memory_snapshot_harness_generatort::add_init_section
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.
Definition: memory_snapshot_harness_generator.cpp:156
irept::id
const irep_idt & id() const
Definition: irep.h:418
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:28
code_function_callt::argumentst
exprt::operandst argumentst
Definition: std_code.h:1192
dstringt::empty
bool empty() const
Definition: dstring.h:88
memory_snapshot_harness_generatort::source_location_matcht::instruction
goto_programt::const_targett instruction
Definition: memory_snapshot_harness_generator.h:136
code_blockt::add
void add(const codet &code)
Definition: std_code.h:208
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
memory_snapshot_harness_generatort::variables_to_havoc
std::unordered_set< irep_idt > variables_to_havoc
Definition: memory_snapshot_harness_generator.h:372
memory_snapshot_harness_generatort::add_call_with_nondet_arguments
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...
Definition: memory_snapshot_harness_generator.cpp:293
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
memory_snapshot_harness_generatort::initial_source_location_line
std::string initial_source_location_line
Definition: memory_snapshot_harness_generator.h:371
recursive_initialization_configt::handle_option
bool handle_option(const std::string &option, const std::list< std::string > &values)
Parse the options specific for recursive initialisation.
Definition: recursive_initialization.cpp:28
safe_string2unsigned
unsigned safe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:19
memory_snapshot_harness_generatort::get_memory_snapshot
void get_memory_snapshot(const std::string &file, symbol_tablet &snapshot) const
Parse the snapshot JSON file and initialise the symbol table.
Definition: memory_snapshot_harness_generator.cpp:332
memory_snapshot_harness_generator.h
MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT
#define MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT
Definition: memory_snapshot_harness_generator_options.h:14
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1945
memory_snapshot_harness_generatort::entry_source_locationt
User provided source location: file name and line number; the structure wraps this option with a pars...
Definition: memory_snapshot_harness_generator.h:87
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
memory_snapshot_harness_generatort::initial_goto_location_line
std::string initial_goto_location_line
Definition: memory_snapshot_harness_generator.h:370
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
memory_snapshot_harness_generatort::entry_source_locationt::line_number
unsigned line_number
Definition: memory_snapshot_harness_generator.h:89
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
memory_snapshot_harness_generatort::generate
void generate(goto_modelt &goto_model, const irep_idt &harness_function_name) override
The main function of this harness, consists of the following:
Definition: memory_snapshot_harness_generator.cpp:374
memory_snapshot_harness_generatort::entry_goto_locationt::function_name
irep_idt function_name
Definition: memory_snapshot_harness_generator.h:54
to_json_object
json_objectt & to_json_object(jsont &json)
Definition: json.h:444
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
goto_programt::const_cast_target
targett const_cast_target(const_targett t)
Convert a const_targett to a targett - use with care and avoid whenever possible.
Definition: goto_program.h:589
symbolt
Symbol table entry.
Definition: symbol.h:28
memory_snapshot_harness_generatort::entry_location
entry_locationt entry_location
data to initialize the entry function
Definition: memory_snapshot_harness_generator.h:375
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
memory_snapshot_harness_generatort::collect_references
void collect_references(const exprt &expr, Adder &&add_reference) const
Definition: memory_snapshot_harness_generator.h:279
MEMORY_SNAPSHOT_HARNESS_INITIAL_GOTO_LOC_OPT
#define MEMORY_SNAPSHOT_HARNESS_INITIAL_GOTO_LOC_OPT
Definition: memory_snapshot_harness_generator_options.h:15
symbolt::is_type
bool is_type
Definition: symbol.h:61
memory_snapshot_harness_generatort::entry_goto_locationt::find_first_corresponding_instruction
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....
Definition: memory_snapshot_harness_generator.cpp:538
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
goto_functionst::update
void update()
Definition: goto_functions.h:81
code_typet::parametert
Definition: std_types.h:753
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
memory_snapshot_harness_generatort::pointer_depth
size_t pointer_depth(const typet &t) const
Recursively compute the pointer depth.
Definition: memory_snapshot_harness_generator.cpp:204
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
goto_programt::insert_after
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:655
memory_snapshot_harness_generatort::initialize_entry_via_source
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...
Definition: memory_snapshot_harness_generator.cpp:505
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:95
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
r
static int8_t r
Definition: irep_hash.h:59
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
goto_functiont::type
code_typet type
The type of the function, indicating the return type and parameter types.
Definition: goto_function.h:34
memory_snapshot_harness_generatort::preordert::sort
void sort(const std::vector< std::pair< Key, T >> &input, std::vector< std::pair< Key, T >> &output)
Definition: memory_snapshot_harness_generator.h:304
goto_convert_functions.h
Goto Programs with Functions.
static_lifetime_init.h
symbol_table.h
Author: Diffblue Ltd.
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
message.h
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
recursive_initializationt::is_initialization_allowed
static bool is_initialization_allowed(const symbolt &symbol)
Definition: recursive_initialization.h:106
invalid_command_line_argument_exceptiont
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition: exception_utils.h:38
parse_json
bool parse_json(std::istream &in, const std::string &filename, message_handlert &message_handler, jsont &dest)
Definition: json_parser.cpp:16
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179
memory_snapshot_harness_generatort::source_location_matcht::match_found
bool match_found
Definition: memory_snapshot_harness_generator.h:137
memory_snapshot_harness_generatort::preordert
Simple structure for linearising posets.
Definition: memory_snapshot_harness_generator.h:293
memory_snapshot_harness_generatort::insert_harness_function_into_goto_model
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.
Definition: memory_snapshot_harness_generator.cpp:312
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
c_types.h
get_fresh_aux_symbol
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 ...
Definition: fresh_symbol.cpp:32
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
json_symbol_table.h
symbol_table_from_json
void symbol_table_from_json(const jsont &in, symbol_tablet &symbol_table)
Definition: json_symbol_table.cpp:16