CBMC
analyze_symbol.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbol Analyzer
4 
5 Author: Malte Mues <mail.mues@gmail.com>
6  Daniel Poetzl
7 
8 \*******************************************************************/
9 
10 #include "analyze_symbol.h"
11 
12 #include <util/c_types.h>
13 #include <util/c_types_util.h>
14 #include <util/expr_initializer.h>
15 #include <util/pointer_expr.h>
17 #include <util/string2int.h>
18 #include <util/string_constant.h>
19 #include <util/string_utils.h>
20 
21 #include <climits>
22 #include <cstdlib>
23 
25  const symbol_table_baset &symbol_table,
26  const std::vector<std::string> &args)
27  : gdb_api(args),
28  symbol_table(symbol_table),
29  ns(symbol_table),
30  c_converter(ns, expr2c_configurationt::clean_configuration),
31  allocate_objects(ID_C, source_locationt(), irep_idt{}, this->symbol_table)
32 {
33 }
34 
36  const memory_addresst &begin,
37  const mp_integer &byte_size,
38  const irep_idt &name)
39  : begin_int(safe_string2size_t(begin.address_string, 0)),
40  byte_size(byte_size),
41  name(name)
42 {
43 }
44 
46  const memory_addresst &point) const
47 {
48  return safe_string2size_t(point.address_string, 0);
49 }
50 
52  const memory_addresst &point,
53  mp_integer member_size) const
54 {
55  auto point_int = address2size_t(point);
56  CHECK_RETURN(check_containment(point_int));
57  return (point_int - begin_int) / member_size;
58 }
59 
60 std::vector<gdb_value_extractort::memory_scopet>::iterator
62 {
63  return std::find_if(
64  dynamically_allocated.begin(),
66  [&name](const memory_scopet &scope) { return scope.id() == name; });
67 }
68 
69 std::vector<gdb_value_extractort::memory_scopet>::iterator
71 {
72  return std::find_if(
73  dynamically_allocated.begin(),
75  [&point](const memory_scopet &memory_scope) {
76  return memory_scope.contains(point);
77  });
78 }
79 
81 {
82  const auto scope_it = find_dynamic_allocation(name);
83  if(scope_it == dynamically_allocated.end())
84  return 1;
85  else
86  return scope_it->size();
87 }
88 
89 std::optional<std::string> gdb_value_extractort::get_malloc_pointee(
90  const memory_addresst &point,
91  mp_integer member_size)
92 {
93  const auto scope_it = find_dynamic_allocation(point);
94  if(scope_it == dynamically_allocated.end())
95  return {};
96 
97  const auto pointer_distance = scope_it->distance(point, member_size);
98  return id2string(scope_it->id()) +
99  (pointer_distance > 0 ? "+" + integer2string(pointer_distance) : "");
100 }
101 
103 {
104  const auto maybe_size = pointer_offset_bits(type, ns);
105  CHECK_RETURN(maybe_size.has_value());
106  return *maybe_size / CHAR_BIT;
107 }
108 
110  const std::list<std::string> &symbols)
111 {
112  // record addresses of given symbols
113  for(const auto &id : symbols)
114  {
115  const symbolt &symbol = ns.lookup(id);
116  if(
117  symbol.type.id() != ID_pointer ||
119  {
120  const symbol_exprt &symbol_expr = ns.lookup(id).symbol_expr();
121  const address_of_exprt aoe(symbol_expr);
122 
123  const std::string c_expr = c_converter.convert(aoe);
124  const pointer_valuet &value = gdb_api.get_memory(c_expr);
125  CHECK_RETURN(value.pointee.empty() || (id == value.pointee));
126 
127  memory_map[id] = value;
128  }
129  else
130  {
131  const std::string c_symbol = c_converter.convert(symbol.symbol_expr());
132  const pointer_valuet &symbol_value = gdb_api.get_memory(c_symbol);
133  size_t symbol_size = gdb_api.query_malloc_size(c_symbol);
134 
135  if(symbol_size > 1)
136  dynamically_allocated.emplace_back(
137  symbol_value.address, symbol_size, id);
138  memory_map[id] = symbol_value;
139  }
140  }
141 
142  for(const auto &id : symbols)
143  {
144  analyze_symbol(id);
145  }
146 }
147 
149 {
150  const symbolt &symbol = ns.lookup(symbol_name);
151  const symbol_exprt symbol_expr = symbol.symbol_expr();
152 
153  try
154  {
155  const typet target_type = symbol.type;
156 
157  const auto zero_expr = zero_initializer(target_type, symbol.location, ns);
158  CHECK_RETURN(zero_expr);
159 
160  const exprt target_expr =
161  get_expr_value(symbol_expr, *zero_expr, symbol.location);
162 
163  add_assignment(symbol_expr, target_expr);
164  }
165  catch(const gdb_interaction_exceptiont &e)
166  {
167  throw analysis_exceptiont(e.what());
168  }
169 
171 }
172 
175 {
176  code_blockt generated_code;
177 
179 
180  for(auto const &pair : assignments)
181  {
182  generated_code.add(code_assignt(pair.first, pair.second));
183  }
184 
185  return c_converter.convert(generated_code);
186 }
187 
190 {
191  symbol_tablet snapshot;
192 
193  for(const auto &pair : assignments)
194  {
195  const symbol_exprt &symbol_expr = to_symbol_expr(pair.first);
196  const irep_idt id = symbol_expr.get_identifier();
197 
198  INVARIANT(symbol_table.has_symbol(id), "symbol must exist in symbol table");
199 
200  const symbolt &symbol = symbol_table.lookup_ref(id);
201 
202  symbolt snapshot_symbol(symbol);
203  snapshot_symbol.value = pair.second;
204 
205  snapshot.insert(snapshot_symbol);
206  }
207 
208  // Also add type symbols to the snapshot
209  for(const auto &pair : symbol_table)
210  {
211  const symbolt &symbol = pair.second;
212 
213  if(symbol.is_type)
214  {
215  snapshot.insert(symbol);
216  }
217  }
218 
219  return snapshot;
220 }
221 
222 void gdb_value_extractort::add_assignment(const exprt &lhs, const exprt &value)
223 {
224  if(assignments.count(lhs) == 0)
225  assignments.emplace(std::make_pair(lhs, value));
226 }
227 
229  const exprt &expr,
230  const memory_addresst &memory_location,
231  const source_locationt &location)
232 {
233  PRECONDITION(expr.type().id() == ID_pointer);
235  PRECONDITION(!memory_location.is_null());
236 
237  auto it = values.find(memory_location);
238 
239  if(it == values.end())
240  {
241  std::string c_expr = c_converter.convert(expr);
242  pointer_valuet value = gdb_api.get_memory(c_expr);
243  CHECK_RETURN(value.string);
244 
245  string_constantt init(*value.string);
247 
248  symbol_exprt dummy("tmp", pointer_type(init.type()));
250 
251  const symbol_exprt new_symbol =
253  assignments, dummy, init.type()));
254 
255  add_assignment(new_symbol, init);
256 
257  values.insert(std::make_pair(memory_location, new_symbol));
258 
259  // check that we are returning objects of the right type
260  CHECK_RETURN(
261  to_array_type(new_symbol.type()).element_type() ==
262  to_pointer_type(expr.type()).base_type());
263  return new_symbol;
264  }
265  else
266  {
267  CHECK_RETURN(
268  to_array_type(it->second.type()).element_type() ==
269  to_pointer_type(expr.type()).base_type());
270  return it->second;
271  }
272 }
273 
275  const exprt &expr,
276  const pointer_valuet &pointer_value,
277  const source_locationt &location)
278 {
279  PRECONDITION(expr.type().id() == ID_pointer);
280  const auto &memory_location = pointer_value.address;
281  std::string memory_location_string = memory_location.string();
282  PRECONDITION(memory_location_string != "0x0");
283  PRECONDITION(!pointer_value.pointee.empty());
284 
285  std::string struct_name;
286  size_t member_offset;
287  if(pointer_value.has_known_offset())
288  {
289  std::string member_offset_string;
290  split_string(
291  pointer_value.pointee, '+', struct_name, member_offset_string, true);
292  member_offset = safe_string2size_t(member_offset_string);
293  }
294  else
295  {
296  struct_name = pointer_value.pointee;
297  member_offset = 0;
298  }
299 
300  const symbolt *struct_symbol = symbol_table.lookup(struct_name);
301  DATA_INVARIANT(struct_symbol != nullptr, "unknown struct");
302 
303  if(!has_known_memory_location(struct_name))
304  {
305  memory_map[struct_name] = gdb_api.get_memory(struct_name);
306  analyze_symbol(irep_idt{struct_name});
307  }
308 
309  const auto &struct_symbol_expr = struct_symbol->symbol_expr();
310  if(struct_symbol->type.id() == ID_array)
311  {
312  return index_exprt{
313  struct_symbol_expr,
314  from_integer(
316  c_index_type())};
317  }
318  if(struct_symbol->type.id() == ID_pointer)
319  {
320  return dereference_exprt{
321  plus_exprt{struct_symbol_expr,
323  expr.type()}};
324  }
325 
326  const auto maybe_member_expr = get_subexpression_at_offset(
327  struct_symbol_expr,
329  to_pointer_type(expr.type()).base_type(),
330  ns);
332  maybe_member_expr.has_value(), "structure doesn't have member");
333 
334  // check that we return the right type
335  CHECK_RETURN(
336  maybe_member_expr->type() == to_pointer_type(expr.type()).base_type());
337  return *maybe_member_expr;
338 }
339 
341  const exprt &expr,
342  const pointer_valuet &pointer_value,
343  const source_locationt &location)
344 {
345  PRECONDITION(expr.type().id() == ID_pointer);
346  PRECONDITION(to_pointer_type(expr.type()).base_type().id() == ID_code);
347  PRECONDITION(!pointer_value.address.is_null());
348 
349  const auto &function_name = pointer_value.pointee;
350  CHECK_RETURN(!function_name.empty());
351  const auto function_symbol = symbol_table.lookup(function_name);
352  if(function_symbol == nullptr)
353  {
355  "input source code does not contain function: " + function_name};
356  }
357  CHECK_RETURN(function_symbol->type.id() == ID_code);
358  return function_symbol->symbol_expr();
359 }
360 
362  const exprt &expr,
363  const pointer_valuet &value,
364  const source_locationt &location)
365 {
366  PRECONDITION(expr.type().id() == ID_pointer);
368  const auto &memory_location = value.address;
369  PRECONDITION(!memory_location.is_null());
370 
371  auto it = values.find(memory_location);
372 
373  if(it == values.end())
374  {
375  if(!value.pointee.empty() && value.pointee != c_converter.convert(expr))
376  {
377  analyze_symbol(value.pointee);
378  const auto pointee_symbol = symbol_table.lookup(value.pointee);
379  CHECK_RETURN(pointee_symbol != nullptr);
380  const auto pointee_symbol_expr = pointee_symbol->symbol_expr();
381  return pointee_symbol_expr;
382  }
383 
384  values.insert(std::make_pair(memory_location, nil_exprt()));
385 
386  const typet target_type = to_pointer_type(expr.type()).base_type();
387 
388  symbol_exprt dummy("tmp", expr.type());
390 
391  const auto zero_expr = zero_initializer(target_type, location, ns);
392  CHECK_RETURN(zero_expr);
393 
394  // Check if pointer was dynamically allocated (via malloc). If so we will
395  // replace the pointee with a static array filled with values stored at the
396  // expected positions. Since the allocated size is an over-approximation we
397  // may end up querying past the allocated bounds and building a larger array
398  // with meaningless values.
399  mp_integer allocated_size = get_malloc_size(c_converter.convert(expr));
400  // get the sizeof(target_type) and thus the number of elements
401  const auto number_of_elements = allocated_size / get_type_size(target_type);
402  if(allocated_size != 1 && number_of_elements > 1)
403  {
404  array_exprt::operandst elements;
405  // build the operands by querying for an index expression
406  for(size_t i = 0; i < number_of_elements; i++)
407  {
408  const auto sub_expr_value = get_expr_value(
410  *zero_expr,
411  location);
412  elements.push_back(sub_expr_value);
413  }
414  CHECK_RETURN(elements.size() == number_of_elements);
415 
416  // knowing the number of elements we can build the type
417  const typet target_array_type =
418  array_typet{target_type, from_integer(elements.size(), c_index_type())};
419 
420  array_exprt new_array{elements, to_array_type(target_array_type)};
421 
422  // allocate a new symbol for the temporary static array
423  symbol_exprt array_dummy("tmp", pointer_type(target_array_type));
424  const auto array_symbol =
426  assignments, array_dummy, target_array_type);
427 
428  // add assignment of value to newly created symbol
429  add_assignment(array_symbol, new_array);
430  values[memory_location] = array_symbol;
431  CHECK_RETURN(array_symbol.type().id() == ID_array);
432  return array_symbol;
433  }
434 
435  const symbol_exprt new_symbol =
437  assignments, dummy, target_type));
438 
439  dereference_exprt dereference_expr(expr);
440 
441  const exprt target_expr =
442  get_expr_value(dereference_expr, *zero_expr, location);
443  // add assignment of value to newly created symbol
444  add_assignment(new_symbol, target_expr);
445 
446  values[memory_location] = new_symbol;
447 
448  return new_symbol;
449  }
450  else
451  {
452  const auto &known_value = it->second;
453  const auto &expected_type = to_pointer_type(expr.type()).base_type();
454  if(find_dynamic_allocation(memory_location) != dynamically_allocated.end())
455  return known_value;
456  if(known_value.is_not_nil() && known_value.type() != expected_type)
457  {
458  return symbol_exprt{to_symbol_expr(known_value).get_identifier(),
459  expected_type};
460  }
461  return known_value;
462  }
463 }
464 
466  pointer_valuet &pointer_value,
467  const pointer_typet &expected_type)
468 {
469  if(pointer_value.has_known_offset())
470  return true;
471 
472  if(pointer_value.pointee.empty())
473  {
474  const auto maybe_pointee = get_malloc_pointee(
475  pointer_value.address, get_type_size(expected_type.base_type()));
476  if(maybe_pointee.has_value())
477  pointer_value.pointee = *maybe_pointee;
478  if(pointer_value.pointee.find("+") != std::string::npos)
479  return true;
480  }
481 
482  const symbolt *pointee_symbol = symbol_table.lookup(pointer_value.pointee);
483  if(pointee_symbol == nullptr)
484  return false;
485  const auto &pointee_type = pointee_symbol->type;
486  return pointee_type.id() == ID_struct_tag ||
487  pointee_type.id() == ID_union_tag || pointee_type.id() == ID_array ||
488  pointee_type.id() == ID_struct || pointee_type.id() == ID_union;
489 }
490 
492  const exprt &expr,
493  const exprt &zero_expr,
494  const source_locationt &location)
495 {
496  PRECONDITION(zero_expr.is_constant());
497 
498  PRECONDITION(expr.type().id() == ID_pointer);
499  PRECONDITION(expr.type() == zero_expr.type());
500 
501  std::string c_expr = c_converter.convert(expr);
502  const auto known_pointer = memory_map.find(c_expr);
503 
504  pointer_valuet value = (known_pointer == memory_map.end() ||
505  known_pointer->second.pointee == c_expr)
506  ? gdb_api.get_memory(c_expr)
507  : known_pointer->second;
508  if(!value.valid)
509  return zero_expr;
510 
511  const auto memory_location = value.address;
512 
513  if(!memory_location.is_null())
514  {
515  // pointers-to-char can point to members as well, e.g. char[]
516  if(points_to_member(value, to_pointer_type(expr.type())))
517  {
518  const auto target_expr =
519  get_pointer_to_member_value(expr, value, location);
520  CHECK_RETURN(target_expr.is_not_nil());
521  const address_of_exprt result_expr{target_expr};
522  CHECK_RETURN(result_expr.type() == zero_expr.type());
523  return std::move(result_expr);
524  }
525 
526  // pointer to function
527  if(to_pointer_type(expr.type()).base_type().id() == ID_code)
528  {
529  const auto target_expr =
530  get_pointer_to_function_value(expr, value, location);
531  CHECK_RETURN(target_expr.is_not_nil());
532  const address_of_exprt result_expr{target_expr};
533  CHECK_RETURN(result_expr.type() == zero_expr.type());
534  return std::move(result_expr);
535  }
536 
537  // non-member: split for char/non-char
538  const auto target_expr =
540  ? get_char_pointer_value(expr, memory_location, location)
541  : get_non_char_pointer_value(expr, value, location);
542 
543  // postpone if we cannot resolve now
544  if(target_expr.is_nil())
545  {
546  outstanding_assignments[expr] = memory_location;
547  return zero_expr;
548  }
549 
550  // the pointee was (probably) dynamically allocated (but the allocation
551  // would not be visible in the snapshot) so we pretend it is statically
552  // allocated (we have the value) and return address to the first element
553  // of the array (instead of the array as char*)
554  if(target_expr.type().id() == ID_array)
555  {
556  const auto result_indexed_expr = get_subexpression_at_offset(
557  target_expr, 0, to_pointer_type(zero_expr.type()).base_type(), ns);
558  CHECK_RETURN(result_indexed_expr.has_value());
559  if(result_indexed_expr->type() == zero_expr.type())
560  return *result_indexed_expr;
561  const address_of_exprt result_expr{*result_indexed_expr};
562  CHECK_RETURN(result_expr.type() == zero_expr.type());
563  return std::move(result_expr);
564  }
565 
566  // if the types match return right away
567  if(target_expr.type() == zero_expr.type())
568  return target_expr;
569 
570  // otherwise the address of target should type-match
571  const address_of_exprt result_expr{target_expr};
572  if(result_expr.type() != zero_expr.type())
573  return typecast_exprt{result_expr, zero_expr.type()};
574  return std::move(result_expr);
575  }
576 
577  return zero_expr;
578 }
579 
581  const exprt &expr,
582  const exprt &array,
583  const source_locationt &location)
584 {
585  PRECONDITION(array.id() == ID_array);
586 
587  PRECONDITION(expr.type().id() == ID_array);
588  PRECONDITION(expr.type() == array.type());
589 
590  exprt new_array(array);
591 
592  for(size_t i = 0; i < new_array.operands().size(); ++i)
593  {
594  const index_exprt index_expr(expr, from_integer(i, c_index_type()));
595 
596  exprt &operand = new_array.operands()[i];
597 
598  operand = get_expr_value(index_expr, operand, location);
599  }
600 
601  return new_array;
602 }
603 
605  const exprt &expr,
606  const exprt &zero_expr,
607  const source_locationt &location)
608 {
609  PRECONDITION(expr.type() == zero_expr.type());
610 
611  const typet &type = expr.type();
612  PRECONDITION(type.id() != ID_struct);
613 
614  if(is_c_integral_type(type))
615  {
616  INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
617 
618  std::string c_expr = c_converter.convert(expr);
619  const auto maybe_value = gdb_api.get_value(c_expr);
620  if(!maybe_value.has_value())
621  return zero_expr;
622  const std::string value = *maybe_value;
623 
624  const mp_integer int_rep = string2integer(value);
625 
626  return from_integer(int_rep, type);
627  }
628  else if(is_c_char_type(type))
629  {
630  INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
631 
632  // check the char-value and return as bitvector-type value
633  std::string c_expr = c_converter.convert(expr);
634  const auto maybe_value = gdb_api.get_value(c_expr);
635  if(!maybe_value.has_value() || maybe_value->empty())
636  return zero_expr;
637  const std::string value = *maybe_value;
638 
639  const mp_integer int_rep = value[0];
640  return from_integer(int_rep, type);
641  }
642  else if(type.id() == ID_c_bool)
643  {
644  INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
645 
646  std::string c_expr = c_converter.convert(expr);
647  const auto maybe_value = gdb_api.get_value(c_expr);
648  if(!maybe_value.has_value())
649  return zero_expr;
650  const std::string value = *maybe_value;
651 
652  return from_c_boolean_value(id2boolean(value), type);
653  }
654  else if(type.id() == ID_c_enum)
655  {
656  INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
657 
658  std::string c_expr = c_converter.convert(expr);
659  const auto maybe_value = gdb_api.get_value(c_expr);
660  if(!maybe_value.has_value())
661  return zero_expr;
662  const std::string value = *maybe_value;
663 
665  }
666  else if(type.id() == ID_struct_tag)
667  {
668  return get_struct_value(expr, zero_expr, location);
669  }
670  else if(type.id() == ID_array)
671  {
672  return get_array_value(expr, zero_expr, location);
673  }
674  else if(type.id() == ID_pointer)
675  {
676  INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
677 
678  return get_pointer_value(expr, zero_expr, location);
679  }
680  else if(type.id() == ID_union_tag)
681  {
682  return get_union_value(expr, zero_expr, location);
683  }
684  UNREACHABLE;
685 }
686 
688  const exprt &expr,
689  const exprt &zero_expr,
690  const source_locationt &location)
691 {
692  PRECONDITION(zero_expr.id() == ID_struct);
693 
694  PRECONDITION(expr.type().id() == ID_struct_tag);
695  PRECONDITION(expr.type() == zero_expr.type());
696 
697  exprt new_expr(zero_expr);
698 
699  const struct_tag_typet &struct_tag_type = to_struct_tag_type(expr.type());
700  const struct_typet &struct_type = ns.follow_tag(struct_tag_type);
701 
702  for(size_t i = 0; i < new_expr.operands().size(); ++i)
703  {
704  const struct_typet::componentt &component = struct_type.components()[i];
705 
707  component.type().id() != ID_code,
708  "struct member must not be of code type");
709  if(component.get_is_padding())
710  {
711  continue;
712  }
713 
714  exprt &operand = new_expr.operands()[i];
715  member_exprt member_expr(expr, component);
716 
717  operand = get_expr_value(member_expr, operand, location);
718  }
719 
720  return new_expr;
721 }
722 
724  const exprt &expr,
725  const exprt &zero_expr,
726  const source_locationt &location)
727 {
728  PRECONDITION(zero_expr.id() == ID_union);
729 
730  PRECONDITION(expr.type().id() == ID_union_tag);
731  PRECONDITION(expr.type() == zero_expr.type());
732 
733  exprt new_expr(zero_expr);
734 
735  const union_tag_typet &union_tag_type = to_union_tag_type(expr.type());
736  const union_typet &union_type = ns.follow_tag(union_tag_type);
737 
738  CHECK_RETURN(new_expr.operands().size() == 1);
739  const union_typet::componentt &component = union_type.components()[0];
740  auto &operand = new_expr.operands()[0];
741  operand = get_expr_value(member_exprt{expr, component}, operand, location);
742  return new_expr;
743 }
744 
746 {
747  for(const auto &pair : outstanding_assignments)
748  {
749  const address_of_exprt aoe(values[pair.second]);
750  add_assignment(pair.first, aoe);
751  }
752 }
753 
755 {
756  std::string c_expr = c_converter.convert(expr);
757  const auto maybe_value = gdb_api.get_value(c_expr);
758  CHECK_RETURN(maybe_value.has_value());
759  return *maybe_value;
760 }
High-level interface to gdb.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:235
bitvector_typet c_index_type()
Definition: c_types.cpp:16
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:335
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:224
This file contains functions, that should support test for underlying c types, in cases where this is...
bool is_c_integral_type(const typet &type)
This function checks, whether the type has been some kind of integer type in the c program.
Definition: c_types_util.h:44
bool id2boolean(const std::string &bool_value)
Convert id to a Boolean value.
Definition: c_types_util.h:105
constant_exprt from_c_boolean_value(bool bool_value, const typet &type)
This function creates a constant representing either 0 or 1 as value of type type.
Definition: c_types_util.h:122
constant_exprt convert_member_name_to_enum_value(const irep_idt &member_name, const c_enum_typet &c_enum)
This function creates a constant representing the bitvector encoded integer value of a string in the ...
Definition: c_types_util.h:85
bool is_c_char_type(const typet &type)
This function checks, whether this has been a char type in the c program.
Definition: c_types_util.h:25
Operator to return the address of an object.
Definition: pointer_expr.h:540
exprt allocate_automatic_local_object(code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const irep_idt &basename_prefix="tmp")
Creates a local variable with automatic lifetime.
void declare_created_symbols(code_blockt &init_code)
Adds declarations for all non-static symbols created.
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
Array constructor from list of elements.
Definition: std_expr.h:1621
Arrays with given size.
Definition: std_types.h:807
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:827
bool is_complete() const
Definition: std_types.h:852
A goto_instruction_codet representing an assignment in the program.
A codet representing sequential composition of program statements.
Definition: std_code.h:130
void add(const codet &code)
Definition: std_code.h:168
virtual std::string what() const
A human readable description of what went wrong.
Operator to dereference a pointer.
Definition: pointer_expr.h:834
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
virtual std::string convert(const typet &src)
Definition: expr2c.cpp:213
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
typet & type()
Return the type of the expression.
Definition: expr.h:84
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.h:212
operandst & operands()
Definition: expr.h:94
std::optional< std::string > get_value(const std::string &expr)
Get the memory address pointed to by the given pointer expression.
pointer_valuet get_memory(const std::string &expr)
Get the value of a pointer associated with expr.
size_t query_malloc_size(const std::string &pointer_expr)
Get the exact allocated size for a pointer pointer_expr.
Definition: gdb_api.cpp:56
std::string get_gdb_value(const exprt &expr)
Extract a stringified value from and c-converted expr.
exprt get_pointer_to_member_value(const exprt &expr, const pointer_valuet &pointer_value, const source_locationt &location)
Call get_subexpression_at_offset to get the correct member expression.
allocate_objectst allocate_objects
std::map< irep_idt, pointer_valuet > memory_map
Keep track of the memory location for the analyzed symbols.
std::map< exprt, memory_addresst > outstanding_assignments
Mapping pointer expression for which get_non_char_pointer_value returned nil expression to memory loc...
void analyze_symbol(const irep_idt &symbol_name)
Assign the gdb-extracted value for symbol_name to its symbol expression and then process outstanding ...
bool has_known_memory_location(const irep_idt &id) const
exprt get_char_pointer_value(const exprt &expr, const memory_addresst &memory_location, const source_locationt &location)
If memory_location is found among values then return the symbol expression associated with it.
exprt get_pointer_to_function_value(const exprt &expr, const pointer_valuet &pointer_value, const source_locationt &location)
Extract the function name from pointer_value, check it has a symbol and return the associated symbol ...
void process_outstanding_assignments()
Call add_assignment for each pair in outstanding_assignments.
exprt get_array_value(const exprt &expr, const exprt &array, const source_locationt &location)
Iterate over array and fill its operands with the results of calling get_expr_value on index expressi...
void add_assignment(const exprt &lhs, const exprt &value)
Create assignment lhs := value (see analyze_symbol)
std::vector< memory_scopet > dynamically_allocated
Keep track of the dynamically allocated memory.
std::map< exprt, exprt > assignments
Sequence of assignments collected during analyze_symbols.
std::string get_snapshot_as_c_code()
Get memory snapshot as C code.
std::map< memory_addresst, exprt > values
Storing pairs <address, symbol> such that at address is stored the value of symbol.
gdb_value_extractort(const symbol_table_baset &symbol_table, const std::vector< std::string > &args)
exprt get_expr_value(const exprt &expr, const exprt &zero_expr, const source_locationt &location)
Case analysis on the typet of expr 1) For integers, booleans, and enums: call gdb_apit::get_value dir...
mp_integer get_type_size(const typet &type) const
Wrapper for call get_offset_pointer_bits.
void analyze_symbols(const std::list< std::string > &symbols)
For each input symbol in symbols: map its value address to its symbol_exprt (via the values map) and ...
bool points_to_member(pointer_valuet &pointer_value, const pointer_typet &expected_type)
Analyzes the pointer_value to decide if it point to a struct or a union (or array)
mp_integer get_malloc_size(irep_idt name)
Search for the size of the allocated memory for name.
std::optional< std::string > get_malloc_pointee(const memory_addresst &point, mp_integer member_size)
Build the pointee string for address point assuming it points to a dynamic allocation of ā€˜nā€™ elements...
exprt get_pointer_value(const exprt &expr, const exprt &zero_expr, const source_locationt &location)
Call gdb_apit::get_memory on expr then split based on the points-to type being char type or not.
symbol_tablet symbol_table
External symbol table ā€“ extracted from read_goto_binary We only expect to analyse symbols located the...
exprt get_struct_value(const exprt &expr, const exprt &zero_expr, const source_locationt &location)
For each of the members of the struct: call get_expr_value.
std::vector< memory_scopet >::iterator find_dynamic_allocation(irep_idt name)
Search for a memory scope allocated under name.
exprt get_union_value(const exprt &expr, const exprt &zero_expr, const source_locationt &location)
For each of the members of the struct: call get_expr_value.
symbol_tablet get_snapshot_as_symbol_table()
Get memory snapshot as symbol table Build a new symbol_tablet and for each lhs symbol from collected ...
exprt get_non_char_pointer_value(const exprt &expr, const pointer_valuet &value, const source_locationt &location)
Similar to get_char_pointer_value.
const namespacet ns
Array index operator.
Definition: std_expr.h:1470
Thrown when user-provided input cannot be processed.
const irep_idt & id() const
Definition: irep.h:388
Extract member of struct or union.
Definition: std_expr.h:2854
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:148
The NIL expression.
Definition: std_expr.h:3091
The plus expression Associativity is not specified.
Definition: std_expr.h:1002
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
const array_typet & type() const
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:493
Structure type, corresponds to C style structs.
Definition: std_types.h:231
const componentst & components() const
Definition: std_types.h:147
Expression to hold a symbol (variable)
Definition: std_expr.h:131
const irep_idt & get_identifier() const
Definition: std_expr.h:160
The symbol table base class interface.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
The symbol table.
Definition: symbol_table.h:14
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Symbol table entry.
Definition: symbol.h:28
bool is_type
Definition: symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
exprt value
Initial value of symbol.
Definition: symbol.h:34
Semantic type conversion.
Definition: std_expr.h:2073
The type of an expression, extends irept.
Definition: type.h:29
A union tag type, i.e., union_typet with an identifier.
Definition: c_types.h:199
The union type.
Definition: c_types.h:147
std::optional< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Expression Initialization.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:54
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:103
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:93
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
std::optional< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::optional< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
Pointer Logic.
BigInt mp_integer
Definition: smt_terms.h:17
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:97
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:888
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:518
std::size_t safe_string2size_t(const std::string &str, int base)
Definition: string2int.cpp:23
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Used for configuring the behaviour of expr2c and type2c.
Definition: expr2c.h:21
Memory address imbued with the explicit boolean data indicating if the address is null or not.
Definition: gdb_api.h:37
std::string string() const
Definition: gdb_api.h:56
std::string address_string
Definition: gdb_api.h:39
bool is_null() const
Definition: gdb_api.h:48
Data associated with the value of a pointer, i.e.
Definition: gdb_api.h:77
memory_addresst address
Definition: gdb_api.h:92
std::optional< std::string > string
Definition: gdb_api.h:95
bool has_known_offset() const
Definition: gdb_api.h:97
std::string pointee
Definition: gdb_api.h:93
mp_integer distance(const memory_addresst &point, mp_integer member_size) const
Compute the distance of point from the beginning of this scope.
memory_scopet(const memory_addresst &begin, const mp_integer &byte_size, const irep_idt &name)
size_t address2size_t(const memory_addresst &point) const
Convert base-16 memory address to a natural number.
#define size_type
Definition: unistd.c:347