CBMC
shadow_memory_util.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symex Shadow Memory Instrumentation
4 
5 Author: Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #include "shadow_memory_util.h"
13 
14 #include <util/arith_tools.h>
15 #include <util/bitvector_expr.h>
16 #include <util/byte_operators.h>
17 #include <util/c_types.h>
18 #include <util/config.h>
19 #include <util/format_expr.h>
20 #include <util/invariant.h>
21 #include <util/namespace.h>
23 #include <util/ssa_expr.h>
24 #include <util/std_expr.h>
25 #include <util/string_constant.h>
26 
27 #include <langapi/language_util.h> // IWYU pragma: keep
30 
32  const namespacet &ns,
33  const messaget &log,
34  const irep_idt &field_name,
35  const exprt &expr,
36  const exprt &value)
37 {
38 #ifdef DEBUG_SHADOW_MEMORY
39  log.conditional_output(
40  log.debug(), [field_name, ns, expr, value](messaget::mstreamt &mstream) {
41  mstream << "Shadow memory: set_field: " << id2string(field_name)
42  << " for " << format(expr) << " to " << format(value)
43  << messaget::eom;
44  });
45 #endif
46 }
47 
49  const namespacet &ns,
50  const messaget &log,
51  const irep_idt &field_name,
52  const exprt &expr)
53 {
54 #ifdef DEBUG_SHADOW_MEMORY
55  log.conditional_output(
56  log.debug(), [ns, field_name, expr](messaget::mstreamt &mstream) {
57  mstream << "Shadow memory: get_field: " << id2string(field_name)
58  << " for " << format(expr) << messaget::eom;
59  });
60 #endif
61 }
62 
64  const namespacet &ns,
65  const messaget &log,
66  const std::vector<exprt> &value_set)
67 {
68 #ifdef DEBUG_SHADOW_MEMORY
69  log.conditional_output(
70  log.debug(), [ns, value_set](messaget::mstreamt &mstream) {
71  for(const auto &e : value_set)
72  {
73  mstream << "Shadow memory: value_set: " << format(e) << messaget::eom;
74  }
75  });
76 #endif
77 }
78 
80  const namespacet &ns,
81  const messaget &log,
82  const exprt &address,
83  const exprt &expr)
84 {
85  // Leave guards rename to DEBUG_SHADOW_MEMORY
86 #ifdef DEBUG_SHADOW_MEMORY
87  log.conditional_output(
88  log.debug(), [ns, address, expr](messaget::mstreamt &mstream) {
89  mstream << "Shadow memory: value_set_match: " << format(address)
90  << " <-- " << format(expr) << messaget::eom;
91  });
92 #endif
93 }
94 
96  const namespacet &ns,
97  const messaget &log,
98  const char *text,
99  const exprt &expr)
100 {
101 #ifdef DEBUG_SHADOW_MEMORY
102  log.conditional_output(
103  log.debug(), [ns, text, expr](messaget::mstreamt &mstream) {
104  mstream << "Shadow memory: " << text << ": " << format(expr)
105  << messaget::eom;
106  });
107 #endif
108 }
109 
114  const namespacet &ns,
115  const messaget &log,
116  const shadow_memory_statet::shadowed_addresst &shadowed_address,
117  const exprt &matched_base_address,
119  const exprt &expr,
120  const value_set_dereferencet::valuet &shadow_dereference)
121 {
122 #ifdef DEBUG_SHADOW_MEMORY
123  log.conditional_output(
124  log.debug(),
125  [ns,
126  shadowed_address,
127  expr,
128  dereference,
129  matched_base_address,
130  shadow_dereference](messaget::mstreamt &mstream) {
131  mstream << "Shadow memory: value_set_match: " << messaget::eom;
132  mstream << "Shadow memory: base: " << format(shadowed_address.address)
133  << " <-- " << format(matched_base_address) << messaget::eom;
134  mstream << "Shadow memory: cell: " << format(dereference.pointer)
135  << " <-- " << format(expr) << messaget::eom;
136  mstream << "Shadow memory: shadow_ptr: "
137  << format(shadow_dereference.pointer) << messaget::eom;
138  mstream << "Shadow memory: shadow_val: "
139  << format(shadow_dereference.value) << messaget::eom;
140  });
141 #endif
142 }
143 
146  const namespacet &ns,
147  const messaget &log,
148  const shadow_memory_statet::shadowed_addresst &shadowed_address)
149 {
150 #ifdef DEBUG_SHADOW_MEMORY
151  log.conditional_output(
152  log.debug(), [ns, shadowed_address](messaget::mstreamt &mstream) {
153  mstream << "Shadow memory: trying shadowed address: "
154  << format(shadowed_address.address) << messaget::eom;
155  });
156 #endif
157 }
158 
160 static void log_shadow_memory_message(const messaget &log, const char *text)
161 {
162 #ifdef DEBUG_SHADOW_MEMORY
163  log.debug() << text << messaget::eom;
164 #endif
165 }
166 
168  const namespacet &ns,
169  const exprt &expr,
170  const shadow_memory_statet::shadowed_addresst &shadowed_address,
171  const messaget &log)
172 {
173 #ifdef DEBUG_SHADOW_MEMORY
174  log.debug() << "Shadow memory: incompatible types "
175  << from_type(ns, "", expr.type()) << ", "
176  << from_type(ns, "", shadowed_address.address.type())
177  << messaget::eom;
178 #endif
179 }
180 
182  const messaget &log,
183  const namespacet &ns,
184  const exprt &expr,
185  const exprt &null_pointer)
186 {
187 #ifdef DEBUG_SHADOW_MEMORY
188  log.conditional_output(
189  log.debug(), [ns, null_pointer, expr](messaget::mstreamt &mstream) {
190  mstream << "Shadow memory: value set match: " << format(null_pointer)
191  << " <-- " << format(expr) << messaget::eom;
192  mstream << "Shadow memory: ignoring set field on NULL object"
193  << messaget::eom;
194  });
195 #endif
196 }
197 
199  const messaget &log,
200  const namespacet &ns,
201  const exprt &expr,
202  const shadow_memory_statet::shadowed_addresst &shadowed_address)
203 {
204 #ifdef DEBUG_SHADOW_MEMORY
205  log.debug() << "Shadow memory: incompatible types "
206  << from_type(ns, "", expr.type()) << ", "
207  << from_type(ns, "", shadowed_address.address.type())
208  << messaget::eom;
209 #endif
210 }
211 
212 irep_idt extract_field_name(const exprt &string_expr)
213 {
214  if(can_cast_expr<typecast_exprt>(string_expr))
215  return extract_field_name(to_typecast_expr(string_expr).op());
216  else if(can_cast_expr<address_of_exprt>(string_expr))
217  return extract_field_name(to_address_of_expr(string_expr).object());
218  else if(can_cast_expr<index_exprt>(string_expr))
219  return extract_field_name(to_index_expr(string_expr).array());
220  else if(can_cast_expr<string_constantt>(string_expr))
221  {
222  return string_expr.get(ID_value);
223  }
224  else
225  {
226  UNREACHABLE_BECAUSE("Failed to extract shadow memory field name.");
227  }
228 }
229 
233 static void remove_array_type_l2(typet &type)
234 {
235  if(to_array_type(type).size().id() != ID_symbol)
236  return;
237 
238  ssa_exprt &size = to_ssa_expr(to_array_type(type).size());
239  size.remove_level_2();
240 }
241 
242 exprt deref_expr(const exprt &expr)
243 {
245  {
246  return to_address_of_expr(expr).object();
247  }
248 
249  return dereference_exprt(expr);
250 }
251 
253 {
254  if(
257  to_array_type(expr.type()).size().get_bool(ID_C_SSA_symbol))
258  {
259  remove_array_type_l2(expr.type());
260  exprt original_expr = to_ssa_expr(expr).get_original_expr();
261  remove_array_type_l2(original_expr.type());
262  to_ssa_expr(expr).set_expression(original_expr);
263  }
264  if(expr.id() == ID_string_constant)
265  {
266  expr = address_of_exprt(expr);
267  expr.type() = pointer_type(char_type());
268  }
269  else if(can_cast_expr<dereference_exprt>(expr))
270  {
271  expr = to_dereference_expr(expr).pointer();
272  }
273  else
274  {
275  expr = address_of_exprt(expr);
276  }
278 }
279 
281 {
282  if(
283  expr.id() == ID_symbol && expr.type().id() == ID_pointer &&
284  (id2string(to_symbol_expr(expr).get_identifier()).rfind("invalid_object") !=
285  std::string::npos ||
286  id2string(to_symbol_expr(expr).get_identifier()).rfind("$object") !=
287  std::string::npos))
288  {
289  expr = null_pointer_exprt(to_pointer_type(expr.type()));
290  return;
291  }
292  Forall_operands(it, expr)
293  {
295  }
296 }
297 
298 const exprt &
299 get_field_init_expr(const irep_idt &field_name, const goto_symex_statet &state)
300 {
301  auto field_type_it = state.shadow_memory.fields.local_fields.find(field_name);
302  if(field_type_it != state.shadow_memory.fields.local_fields.end())
303  {
304  return field_type_it->second;
305  }
306  field_type_it = state.shadow_memory.fields.global_fields.find(field_name);
307  CHECK_RETURN(field_type_it != state.shadow_memory.fields.global_fields.end());
308  return field_type_it->second;
309 }
310 
311 const typet &
312 get_field_init_type(const irep_idt &field_name, const goto_symex_statet &state)
313 {
314  const exprt &field_init_expr = get_field_init_expr(field_name, state);
315  return field_init_expr.type();
316 }
317 
319  const std::vector<exprt> &value_set,
320  const exprt &address)
321 {
322  if(address.is_constant() && to_constant_expr(address).is_null_pointer())
323  {
324  for(const auto &e : value_set)
325  {
326  if(e.id() != ID_object_descriptor)
327  continue;
328 
329  const exprt &expr = to_object_descriptor_expr(e).object();
330  if(expr.id() == ID_null_object)
331  return true;
332  }
333  return false;
334  }
335 
336  for(const auto &e : value_set)
337  {
338  if(e.id() == ID_unknown || e.id() == ID_object_descriptor)
339  return true;
340  }
341  return false;
342 }
343 
348 {
349  if(value.type().id() != ID_floatbv)
350  {
351  return value;
352  }
353  return make_byte_extract(
354  value,
357 }
358 
367  const exprt &value,
368  const typet &type,
369  const typet &field_type,
370  exprt::operandst &values)
371 {
372  INVARIANT(
374  "Cannot combine with *or* elements of a non-bitvector type.");
375  const size_t size =
377  values.push_back(typecast_exprt::conditional_cast(value, field_type));
378  for(size_t i = 1; i < size; ++i)
379  {
380  values.push_back(typecast_exprt::conditional_cast(
381  lshr_exprt(value, from_integer(8 * i, size_type())), field_type));
382  }
383 }
384 
396  exprt element,
397  const typet &field_type,
398  const namespacet &ns,
399  const messaget &log,
400  const bool is_union,
401  exprt::operandst &values)
402 {
403  element = conditional_cast_floatbv_to_unsignedbv(element);
404  if(element.type().id() == ID_unsignedbv || element.type().id() == ID_signedbv)
405  {
406  exprt value = element;
407  if(is_union)
408  {
409  extract_bytes_of_bv(value, element.type(), field_type, values);
410  }
411  else
412  {
413  values.push_back(typecast_exprt::conditional_cast(value, field_type));
414  }
415  }
416  else
417  {
418  exprt value = compute_or_over_bytes(element, field_type, ns, log, is_union);
419  values.push_back(typecast_exprt::conditional_cast(value, field_type));
420  }
421 }
422 
430 static exprt or_values(const exprt::operandst &values, const typet &field_type)
431 {
432  if(values.size() == 1)
433  {
434  return values[0];
435  }
436  return multi_ary_exprt(ID_bitor, values, field_type);
437 }
438 
440  const exprt &expr,
441  const typet &field_type,
442  const namespacet &ns,
443  const messaget &log,
444  const bool is_union)
445 {
446  INVARIANT(
447  can_cast_type<c_bool_typet>(field_type) ||
448  can_cast_type<bool_typet>(field_type),
449  "Can aggregate bytes with *or* only if the shadow memory type is _Bool.");
450 
451  if(
452  expr.type().id() == ID_struct || expr.type().id() == ID_union ||
453  expr.type().id() == ID_struct_tag || expr.type().id() == ID_union_tag)
454  {
455  const auto &components =
456  (expr.type().id() == ID_struct_tag || expr.type().id() == ID_union_tag)
457  ? ns.follow_tag(to_struct_or_union_tag_type(expr.type())).components()
459  exprt::operandst values;
460  for(const auto &component : components)
461  {
462  if(component.get_is_padding())
463  {
464  continue;
465  }
467  member_exprt(expr, component), field_type, ns, log, is_union, values);
468  }
469  return or_values(values, field_type);
470  }
471  else if(expr.type().id() == ID_array)
472  {
473  const array_typet &array_type = to_array_type(expr.type());
474  if(array_type.size().is_constant())
475  {
476  exprt::operandst values;
477  const mp_integer size =
478  numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
479  for(mp_integer index = 0; index < size; ++index)
480  {
482  index_exprt(expr, from_integer(index, array_type.index_type())),
483  field_type,
484  ns,
485  log,
486  is_union,
487  values);
488  }
489  return or_values(values, field_type);
490  }
491  else
492  {
493  log.warning()
494  << "Shadow memory: cannot compute or over variable-size array "
495  << format(expr) << messaget::eom;
496  }
497  }
498  exprt::operandst values;
499  if(is_union)
500  {
503  expr.type(),
504  field_type,
505  values);
506  }
507  else
508  {
509  values.push_back(typecast_exprt::conditional_cast(
510  conditional_cast_floatbv_to_unsignedbv(expr), field_type));
511  }
512  return or_values(values, field_type);
513 }
514 
523 std::pair<exprt, exprt> compare_to_collection(
524  const std::vector<exprt>::const_iterator &expr_iterator,
525  const std::vector<exprt>::const_iterator &end)
526 {
527  // We need at least an element in the collection
528  INVARIANT(expr_iterator != end, "Cannot compute max of an empty collection");
529  const exprt &current_expr = *expr_iterator;
530 
531  // Iterator for the other elements in the collection in the interval denoted
532  // by `expr_iterator` and `end`.
533  std::vector<exprt>::const_iterator expr_to_compare_to =
534  std::next(expr_iterator);
535  if(expr_to_compare_to == end)
536  {
537  return {nil_exprt{}, current_expr};
538  }
539 
540  std::vector<exprt> comparisons;
541  for(; expr_to_compare_to != end; ++expr_to_compare_to)
542  {
543  // Compare the current element with the n-th following it
544  comparisons.emplace_back(
545  binary_predicate_exprt(current_expr, ID_gt, *expr_to_compare_to));
546  }
547 
548  return {and_exprt(comparisons), current_expr};
549 }
550 
557  const std::vector<std::pair<exprt, exprt>> &conditions_and_values)
558 {
559  // We need at least one element
560  INVARIANT(
561  conditions_and_values.size() > 0,
562  "Cannot compute max of an empty collection");
563 
564  // We use reverse-iterator, so the last element is the one in the last else
565  // case.
566  auto reverse_ite = conditions_and_values.rbegin();
567 
568  // The last element must have `nil_exprt` as condition
569  INVARIANT(
570  reverse_ite->first == nil_exprt{},
571  "Last element of condition-value list must have nil_exprt condition.");
572 
573  exprt res = std::move(reverse_ite->second);
574 
575  for(++reverse_ite; reverse_ite != conditions_and_values.rend(); ++reverse_ite)
576  {
577  res = if_exprt(reverse_ite->first, reverse_ite->second, res);
578  }
579 
580  return res;
581 }
582 
586 static exprt create_max_expr(const std::vector<exprt> &values)
587 {
588  std::vector<std::pair<exprt, exprt>> rows;
589  rows.reserve(values.size());
590  for(auto byte_it = values.begin(); byte_it != values.end(); ++byte_it)
591  {
592  // Create a pair condition-element where the condition is the comparison of
593  // the element with all the ones contained in the rest of the collection.
594  rows.emplace_back(compare_to_collection(byte_it, values.end()));
595  }
596 
598 }
599 
601  const exprt &expr,
602  const typet &field_type,
603  const namespacet &ns)
604 {
605  // Compute the bit-width of the type of `expr`.
606  std::size_t size = boolbv_widtht{ns}(expr.type());
607 
608  // Compute how many bytes are in `expr`
609  std::size_t byte_count = size / config.ansi_c.char_width;
610 
611  // Extract each byte of `expr` by using byte_extract.
612  std::vector<exprt> extracted_bytes;
613  extracted_bytes.reserve(byte_count);
614  for(std::size_t i = 0; i < byte_count; ++i)
615  {
616  extracted_bytes.emplace_back(make_byte_extract(
617  expr, from_integer(i, unsigned_long_int_type()), field_type));
618  }
619 
620  // Compute the max of the bytes extracted from `expr`.
621  exprt max_expr = create_max_expr(extracted_bytes);
622 
623  INVARIANT(
624  max_expr.type() == field_type,
625  "Aggregated max value type must be the same as shadow memory field's "
626  "type.");
627 
628  return max_expr;
629 }
630 
632  const std::vector<std::pair<exprt, exprt>> &conds_values)
633 {
635  !conds_values.empty(), "build_if_else_expr requires non-empty argument");
636  exprt result = nil_exprt();
637  for(const auto &cond_value : conds_values)
638  {
639  if(result.is_nil())
640  {
641  result = cond_value.second;
642  }
643  else
644  {
645  result = if_exprt(cond_value.first, cond_value.second, result);
646  }
647  }
648  return result;
649 }
650 
657 static bool
658 are_types_compatible(const typet &expr_type, const typet &shadow_type)
659 {
660  if(expr_type.id() != ID_pointer || shadow_type.id() != ID_pointer)
661  return true;
662 
663  // We filter out the particularly annoying case of char ** being definitely
664  // incompatible with char[].
665  const typet &expr_subtype = to_pointer_type(expr_type).base_type();
666  const typet &shadow_subtype = to_pointer_type(shadow_type).base_type();
667 
668  if(
669  expr_subtype.id() == ID_pointer &&
670  to_pointer_type(expr_subtype).base_type().id() != ID_pointer &&
671  shadow_subtype.id() == ID_array &&
672  to_array_type(shadow_subtype).element_type().id() != ID_pointer)
673  {
674  return false;
675  }
676  if(
677  shadow_subtype.id() == ID_pointer &&
678  to_pointer_type(shadow_subtype).base_type().id() != ID_pointer &&
679  expr_subtype.id() != ID_pointer)
680  {
681  return false;
682  }
683  return true;
684 }
685 
689 static void clean_string_constant(exprt &expr)
690 {
691  const auto *index_expr = expr_try_dynamic_cast<index_exprt>(expr);
692  if(
693  index_expr && index_expr->index().is_zero() &&
694  can_cast_expr<string_constantt>(index_expr->array()))
695  {
696  expr = index_expr->array();
697  }
698 }
699 
704 static void adjust_array_types(typet &type)
705 {
706  auto *pointer_type = type_try_dynamic_cast<pointer_typet>(type);
707  if(!pointer_type)
708  {
709  return;
710  }
711  if(
712  const auto *array_type =
713  type_try_dynamic_cast<array_typet>(pointer_type->base_type()))
714  {
715  pointer_type->base_type() = array_type->element_type();
716  }
717  if(pointer_type->base_type().id() == ID_string_constant)
718  {
720  }
721 }
722 
730  const exprt &shadowed_address,
731  const exprt &matched_base_address,
732  const namespacet &ns,
733  const messaget &log)
734 {
735  typet shadowed_address_type = shadowed_address.type();
736  adjust_array_types(shadowed_address_type);
737  exprt lhs =
738  typecast_exprt::conditional_cast(shadowed_address, shadowed_address_type);
740  matched_base_address, shadowed_address_type);
741  exprt base_cond = simplify_expr(equal_exprt(lhs, rhs), ns);
742  if(
743  base_cond.id() == ID_equal &&
744  to_equal_expr(base_cond).lhs() == to_equal_expr(base_cond).rhs())
745  {
746  return true_exprt();
747  }
748  if(base_cond.id() == ID_equal)
749  {
750  const equal_exprt &equal_expr = to_equal_expr(base_cond);
751  const bool equality_types_match =
752  equal_expr.lhs().type() == equal_expr.rhs().type();
754  equality_types_match,
755  "types of expressions on each side of equality should match",
756  irep_pretty_diagnosticst{equal_expr.lhs()},
757  irep_pretty_diagnosticst{equal_expr.rhs()});
758  }
759 
760  return base_cond;
761 }
762 
769  const exprt &dereference_pointer,
770  const exprt &expr,
771  const namespacet &ns,
772  const messaget &log)
773 {
774  typet expr_type = expr.type();
775  adjust_array_types(expr_type);
776  exprt expr_cond = simplify_expr(
777  equal_exprt(
778  typecast_exprt::conditional_cast(expr, expr_type),
779  typecast_exprt::conditional_cast(dereference_pointer, expr_type)),
780  ns);
781  if(
782  expr_cond.id() == ID_equal &&
783  to_equal_expr(expr_cond).lhs() == to_equal_expr(expr_cond).rhs())
784  {
785  return true_exprt();
786  }
787  if(expr_cond.id() == ID_equal)
788  {
789  const equal_exprt &equal_expr = to_equal_expr(expr_cond);
790  const bool equality_types_match =
791  equal_expr.lhs().type() == equal_expr.rhs().type();
793  equality_types_match,
794  "types of expressions on each side of equality should match",
795  irep_pretty_diagnosticst{equal_expr.lhs()},
796  irep_pretty_diagnosticst{equal_expr.rhs()});
797  }
798  return expr_cond;
799 }
800 
812  const exprt &shadow,
813  const object_descriptor_exprt &matched_base_descriptor,
814  const exprt &expr,
815  const namespacet &ns,
816  const messaget &log)
817 {
818  object_descriptor_exprt shadowed_object = matched_base_descriptor;
819  shadowed_object.object() = shadow;
820  value_set_dereferencet::valuet shadow_dereference =
821  value_set_dereferencet::build_reference_to(shadowed_object, expr, ns);
822 #ifdef DEBUG_SHADOW_MEMORY
823  log.debug() << "Shadow memory: shadow-deref: "
824  << format(shadow_dereference.value) << messaget::eom;
825 #endif
826  return shadow_dereference;
827 }
828 
829 /* foreach shadowed_address in SM:
830  * if(incompatible(shadow.object, object)) continue; // Type incompatibility
831  * base_match = object == shadow_object; // Do the base obj match the SM obj
832  * if(!base_match) continue;
833  * if(object is null) continue; // Done in the caller
834  * if(type_of(dereference object is void)
835  * // we terminate as we don't know how big is the memory at that location
836  * shadowed_dereference.pointer = deref(shadow.shadowed_object, expr);
837  * aggregate the object depending on the type
838  * expr_match = shadowed_dereference == expr
839  * if(!expr_match)
840  * continue;
841  * shadow_dereference = deref(shadow.object, expr);
842  * if(expr_match)
843  * result = shadow_dereference.value [exact match]
844  * break;
845  * if(base_match) [shadow memory matches]
846  * result += (expr_match, shadow_dereference.value)
847  * break;
848  * result += (base_match & expr_match, shadow_dereference.value)
849 */
850 std::vector<std::pair<exprt, exprt>> get_shadow_dereference_candidates(
851  const namespacet &ns,
852  const messaget &log,
853  const exprt &matched_object,
854  const std::vector<shadow_memory_statet::shadowed_addresst> &addresses,
855  const typet &field_type,
856  const exprt &expr,
857  const typet &lhs_type,
858  bool &exact_match)
859 {
860  std::vector<std::pair<exprt, exprt>> result;
861 
862  for(const auto &shadowed_address : addresses)
863  {
864  log_try_shadow_address(ns, log, shadowed_address);
865  if(!are_types_compatible(expr.type(), shadowed_address.address.type()))
866  {
867  log_are_types_incompatible(ns, expr, shadowed_address, log);
868  continue;
869  }
870  const object_descriptor_exprt &matched_base_descriptor =
871  to_object_descriptor_expr(matched_object);
872  exprt matched_base_address =
873  address_of_exprt(matched_base_descriptor.object());
874  clean_string_constant(to_address_of_expr(matched_base_address).op());
875 
876  // NULL has already been handled in the caller; skip.
877  if(matched_base_descriptor.object().id() == ID_null_object)
878  {
879  continue;
880  }
881 
882  // Used only to check if the pointer is `void`
884  value_set_dereferencet::build_reference_to(matched_object, expr, ns);
885 
886  if(is_void_pointer(dereference.pointer.type()))
887  {
888  std::stringstream s;
889  s << "Shadow memory: cannot get shadow memory via type void* for "
890  << format(expr)
891  << ". Insert a cast to the type that you want to access.";
892  throw invalid_input_exceptiont(s.str());
893  }
894 
895  // Replace original memory with the shadow object (symbolic dereferencing is
896  // performed during symex later on).
897  const value_set_dereferencet::valuet shadow_dereference =
899  shadowed_address.shadow, matched_base_descriptor, expr, ns, log);
901  ns,
902  log,
903  shadowed_address,
904  matched_base_address,
905  dereference,
906  expr,
907  shadow_dereference);
908 
909  const bool is_union = matched_base_descriptor.type().id() == ID_union ||
910  matched_base_descriptor.type().id() == ID_union_tag;
911 
912  exprt value;
913  // Aggregate the value depending on the type
914  if(field_type.id() == ID_c_bool || field_type.id() == ID_bool)
915  {
916  // Value is of bool type, so aggregate with or.
919  shadow_dereference.value, field_type, ns, log, is_union),
920  lhs_type);
921  }
922  else
923  {
924  // Value is of other (bitvector) type, so aggregate with max
925  value = compute_max_over_bytes(shadow_dereference.value, field_type, ns);
926  }
927 
928  const exprt base_cond = get_matched_base_cond(
929  shadowed_address.address, matched_base_address, ns, log);
930  shadow_memory_log_text_and_expr(ns, log, "base_cond", base_cond);
931  if(base_cond.is_false())
932  {
933  continue;
934  }
935 
936  const exprt expr_cond =
937  get_matched_expr_cond(dereference.pointer, expr, ns, log);
938  if(expr_cond.is_false())
939  {
940  continue;
941  }
942 
943  if(base_cond.is_true() && expr_cond.is_true())
944  {
945 #ifdef DEBUG_SHADOW_MEMORY
946  log.debug() << "exact match" << messaget::eom;
947 #endif
948  exact_match = true;
949  result.clear();
950  result.emplace_back(base_cond, value);
951  break;
952  }
953 
954  if(base_cond.is_true())
955  {
956  // No point looking at further shadow addresses
957  // as only one of them can match.
958 #ifdef DEBUG_SHADOW_MEMORY
959  log.debug() << "base match" << messaget::eom;
960 #endif
961  result.clear();
962  result.emplace_back(expr_cond, value);
963  break;
964  }
965  else
966  {
967 #ifdef DEBUG_SHADOW_MEMORY
968  log.debug() << "conditional match" << messaget::eom;
969 #endif
970  result.emplace_back(and_exprt(base_cond, expr_cond), value);
971  }
972  }
973  return result;
974 }
975 
976 // Unfortunately.
979 {
980  if(expr.object().id() == ID_symbol)
981  {
982  return expr;
983  }
984  if(expr.offset().id() == ID_unknown)
985  {
986  return expr;
987  }
988 
989  object_descriptor_exprt result = expr;
990  mp_integer offset =
991  numeric_cast_v<mp_integer>(to_constant_expr(expr.offset()));
992  exprt object = expr.object();
993 
994  while(true)
995  {
996  if(object.id() == ID_index)
997  {
998  const index_exprt &index_expr = to_index_expr(object);
999  mp_integer index =
1000  numeric_cast_v<mp_integer>(to_constant_expr(index_expr.index()));
1001 
1002  offset += *pointer_offset_size(index_expr.type(), ns) * index;
1003  object = index_expr.array();
1004  }
1005  else if(object.id() == ID_member)
1006  {
1007  const member_exprt &member_expr = to_member_expr(object);
1008  const auto &struct_op = member_expr.struct_op();
1009  const struct_typet &struct_type =
1010  struct_op.type().id() == ID_struct_tag
1011  ? ns.follow_tag(to_struct_tag_type(struct_op.type()))
1012  : to_struct_type(struct_op.type());
1013  offset +=
1014  *member_offset(struct_type, member_expr.get_component_name(), ns);
1015  object = struct_op;
1016  }
1017  else
1018  {
1019  break;
1020  }
1021  }
1022  result.object() = object;
1023  result.offset() = from_integer(offset, expr.offset().type());
1024  return result;
1025 }
1026 
1028  const namespacet &ns,
1029  const messaget &log,
1030  const std::vector<exprt> &value_set,
1031  const exprt &expr)
1032 {
1033  INVARIANT(
1035  "Cannot check if value_set contains only NULL as `expr` type is not a "
1036  "pointer.");
1037  const null_pointer_exprt null_pointer(to_pointer_type(expr.type()));
1038  if(value_set.size() == 1 && contains_null_or_invalid(value_set, null_pointer))
1039  {
1040  log_value_set_contains_only_null(log, ns, expr, null_pointer);
1041  return true;
1042  }
1043  return false;
1044 }
1045 
1047 static std::vector<std::pair<exprt, exprt>>
1049  const exprt &expr,
1050  const exprt &matched_object,
1051  const std::vector<shadow_memory_statet::shadowed_addresst> &addresses,
1052  const namespacet &ns,
1053  const messaget &log,
1054  bool &exact_match)
1055 {
1056  std::vector<std::pair<exprt, exprt>> result;
1057  for(const auto &shadowed_address : addresses)
1058  {
1059  log_try_shadow_address(ns, log, shadowed_address);
1060 
1061  if(!are_types_compatible(expr.type(), shadowed_address.address.type()))
1062  {
1063  log_shadow_memory_incompatible_types(log, ns, expr, shadowed_address);
1064  continue;
1065  }
1066 
1067  object_descriptor_exprt matched_base_descriptor =
1068  normalize(to_object_descriptor_expr(matched_object), ns);
1069 
1072  matched_base_descriptor, expr, ns);
1073 
1074  exprt matched_base_address =
1075  address_of_exprt(matched_base_descriptor.object());
1076  clean_string_constant(to_address_of_expr(matched_base_address).op());
1077 
1078  // NULL has already been handled in the caller; skip.
1079  if(matched_base_descriptor.object().id() == ID_null_object)
1080  {
1081  continue;
1082  }
1083  const value_set_dereferencet::valuet shadow_dereference =
1085  shadowed_address.shadow, matched_base_descriptor, expr, ns, log);
1087  ns,
1088  log,
1089  shadowed_address,
1090  matched_base_address,
1091  dereference,
1092  expr,
1093  shadow_dereference);
1094 
1095  const exprt base_cond = get_matched_base_cond(
1096  shadowed_address.address, matched_base_address, ns, log);
1097  shadow_memory_log_text_and_expr(ns, log, "base_cond", base_cond);
1098  if(base_cond.is_false())
1099  {
1100  continue;
1101  }
1102 
1103  const exprt expr_cond =
1104  get_matched_expr_cond(dereference.pointer, expr, ns, log);
1105  if(expr_cond.is_false())
1106  {
1107  continue;
1108  }
1109 
1110  if(base_cond.is_true() && expr_cond.is_true())
1111  {
1112  log_shadow_memory_message(log, "exact match");
1113 
1114  exact_match = true;
1115  result.clear();
1116  result.push_back({base_cond, shadow_dereference.pointer});
1117  break;
1118  }
1119 
1120  if(base_cond.is_true())
1121  {
1122  // No point looking at further shadow addresses
1123  // as only one of them can match.
1124  log_shadow_memory_message(log, "base match");
1125 
1126  result.clear();
1127  result.emplace_back(expr_cond, shadow_dereference.pointer);
1128  break;
1129  }
1130  else
1131  {
1132  log_shadow_memory_message(log, "conditional match");
1133  result.emplace_back(
1134  and_exprt(base_cond, expr_cond), shadow_dereference.pointer);
1135  }
1136  }
1137  return result;
1138 }
1139 
1140 std::optional<exprt> get_shadow_memory(
1141  const exprt &expr,
1142  const std::vector<exprt> &value_set,
1143  const std::vector<shadow_memory_statet::shadowed_addresst> &addresses,
1144  const namespacet &ns,
1145  const messaget &log,
1146  size_t &mux_size)
1147 {
1148  std::vector<std::pair<exprt, exprt>> conds_values;
1149  for(const auto &matched_object : value_set)
1150  {
1151  if(matched_object.id() != ID_object_descriptor)
1152  {
1153  log.warning() << "Shadow memory: value set contains unknown for "
1154  << format(expr) << messaget::eom;
1155  continue;
1156  }
1157  if(
1158  to_object_descriptor_expr(matched_object).root_object().id() ==
1159  ID_integer_address)
1160  {
1161  log.warning() << "Shadow memory: value set contains integer_address for "
1162  << format(expr) << messaget::eom;
1163  continue;
1164  }
1165  if(matched_object.type().get_bool(ID_C_is_failed_symbol))
1166  {
1167  log.warning() << "Shadow memory: value set contains failed symbol for "
1168  << format(expr) << messaget::eom;
1169  continue;
1170  }
1171 
1172  bool exact_match = false;
1173  auto per_value_set_conds_values = get_shadow_memory_for_matched_object(
1174  expr, matched_object, addresses, ns, log, exact_match);
1175 
1176  if(!per_value_set_conds_values.empty())
1177  {
1178  if(exact_match)
1179  {
1180  conds_values.clear();
1181  }
1182  conds_values.insert(
1183  conds_values.begin(),
1184  per_value_set_conds_values.begin(),
1185  per_value_set_conds_values.end());
1186  mux_size += conds_values.size() - 1;
1187  if(exact_match)
1188  {
1189  break;
1190  }
1191  }
1192  }
1193  if(!conds_values.empty())
1194  {
1195  return build_if_else_expr(conds_values);
1196  }
1197  return {};
1198 }
configt config
Definition: config.cpp:25
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
API to expression classes for bitvectors.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
byte_extract_exprt make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
Construct a byte_extract_exprt with endianness and byte width matching the current configuration.
Expression classes for byte-level operators.
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:36
unsignedbv_typet unsigned_long_int_type()
Definition: c_types.cpp:86
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:235
bitvector_typet char_type()
Definition: c_types.cpp:106
bool can_cast_type< c_bool_typet >(const typet &type)
Check whether a reference to a typet is a c_bool_typet.
Definition: c_types.h:115
Operator to return the address of an object.
Definition: pointer_expr.h:540
exprt & object()
Definition: pointer_expr.h:549
Boolean AND.
Definition: std_expr.h:2120
Arrays with given size.
Definition: std_types.h:807
typet index_type() const
The type of the index expressions into any instance of this type.
Definition: std_types.cpp:34
const exprt & size() const
Definition: std_types.h:840
exprt & lhs()
Definition: std_expr.h:668
exprt & rhs()
Definition: std_expr.h:678
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:731
std::size_t get_width() const
Definition: std_types.h:925
struct configt::ansi_ct ansi_c
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
Equality.
Definition: std_expr.h:1361
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:27
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:34
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
Central data structure: state.
shadow_memory_statet shadow_memory
The trinary if-then-else operator.
Definition: std_expr.h:2370
Array index operator.
Definition: std_expr.h:1465
exprt & array()
Definition: std_expr.h:1495
exprt & index()
Definition: std_expr.h:1505
Thrown when user-provided input cannot be processed.
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:57
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
const irep_idt & id() const
Definition: irep.h:388
bool is_nil() const
Definition: irep.h:368
Logical right shift.
Extract member of struct or union.
Definition: std_expr.h:2844
const exprt & struct_op() const
Definition: std_expr.h:2882
irep_idt get_component_name() const
Definition: std_expr.h:2866
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:154
static eomt eom
Definition: message.h:289
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:912
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
The NIL expression.
Definition: std_expr.h:3081
The null pointer constant.
Definition: pointer_expr.h:909
Split an expression into a base object and a (byte) offset.
Definition: pointer_expr.h:181
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
field_definitiont global_fields
Field definitions for global-scope fields.
field_definitiont local_fields
Field definitions for local-scope fields.
shadow_memory_field_definitionst fields
The available shadow memory field definitions.
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
void remove_level_2()
void set_expression(exprt expr)
Replace the underlying, original expression by expr while maintaining SSA indices.
const exprt & get_original_expr() const
Definition: ssa_expr.h:33
Structure type, corresponds to C style structs.
Definition: std_types.h:231
const componentst & components() const
Definition: std_types.h:147
The Boolean constant true.
Definition: std_expr.h:3063
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2076
The type of an expression, extends irept.
Definition: type.h:29
Fixed-width bit-vector with unsigned binary interpretation.
Return value for build_reference_to; see that method for documentation.
static valuet build_reference_to(const exprt &what, const exprt &pointer, const namespacet &ns)
#define Forall_operands(it, expr)
Definition: expr.h:27
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Definition: expr_util.cpp:344
static format_containert< T > format(const T &o)
Definition: format.h:37
void dereference(const irep_idt &function_id, goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets, message_handlert &message_handler)
Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointin...
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
double log(double x)
Definition: math.c:2776
bool is_void_pointer(const typet &type)
This method tests, if the given typet is a pointer of type void.
Definition: pointer_expr.h:110
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
Definition: pointer_expr.h:80
bool can_cast_expr< dereference_exprt >(const exprt &base)
Definition: pointer_expr.h:874
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:890
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:93
bool can_cast_expr< address_of_exprt >(const exprt &base)
Definition: pointer_expr.h:561
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
Definition: pointer_expr.h:252
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:577
std::optional< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
Pointer Logic.
exprt build_if_else_expr(const std::vector< std::pair< exprt, exprt >> &conds_values)
Build an if-then-else chain from a vector containing pairs of expressions.
void replace_invalid_object_by_null(exprt &expr)
Replace an invalid object by a null pointer.
static object_descriptor_exprt normalize(const object_descriptor_exprt &expr, const namespacet &ns)
void shadow_memory_log_value_set_match(const namespacet &ns, const messaget &log, const exprt &address, const exprt &expr)
Logs a successful match between an address and a value within the value set.
static void clean_string_constant(exprt &expr)
Simplify &string_constant[0] to &string_constant to facilitate expression equality for exact matching...
exprt deref_expr(const exprt &expr)
Wraps a given expression into a dereference_exprt unless it is an address_of_exprt in which case it j...
bool contains_null_or_invalid(const std::vector< exprt > &value_set, const exprt &address)
Given a pointer expression check to see if it can be a null pointer or an invalid object within value...
static exprt or_values(const exprt::operandst &values, const typet &field_type)
Translate a list of values into an or expression.
exprt compute_or_over_bytes(const exprt &expr, const typet &field_type, const namespacet &ns, const messaget &log, const bool is_union)
Performs aggregation of the shadow memory field value over multiple bytes for fields whose type is _B...
static bool are_types_compatible(const typet &expr_type, const typet &shadow_type)
Checks given types (object type and shadow memory field type) for equality.
static std::vector< std::pair< exprt, exprt > > get_shadow_memory_for_matched_object(const exprt &expr, const exprt &matched_object, const std::vector< shadow_memory_statet::shadowed_addresst > &addresses, const namespacet &ns, const messaget &log, bool &exact_match)
Used for set_field and shadow memory copy.
static void extract_bytes_of_expr(exprt element, const typet &field_type, const namespacet &ns, const messaget &log, const bool is_union, exprt::operandst &values)
Extract the components from the input expression value and places them into the array values.
static void adjust_array_types(typet &type)
Flattens type of the form pointer_type(array_type(element_type)) to pointer_type(element_type) and po...
bool check_value_set_contains_only_null_ptr(const namespacet &ns, const messaget &log, const std::vector< exprt > &value_set, const exprt &expr)
Checks if value_set contains only a NULL pointer expression of the same type of expr.
static void log_value_set_match(const namespacet &ns, const messaget &log, const shadow_memory_statet::shadowed_addresst &shadowed_address, const exprt &matched_base_address, const value_set_dereferencet::valuet &dereference, const exprt &expr, const value_set_dereferencet::valuet &shadow_dereference)
Log a match between an address and the value set.
void shadow_memory_log_set_field(const namespacet &ns, const messaget &log, const irep_idt &field_name, const exprt &expr, const exprt &value)
Logs setting a value to a given shadow field.
const typet & get_field_init_type(const irep_idt &field_name, const goto_symex_statet &state)
Retrieves the type of the shadow memory by returning the type of the shadow memory initializer value.
const exprt & get_field_init_expr(const irep_idt &field_name, const goto_symex_statet &state)
Retrieve the expression that a field was initialised with within a given symex state.
std::pair< exprt, exprt > compare_to_collection(const std::vector< exprt >::const_iterator &expr_iterator, const std::vector< exprt >::const_iterator &end)
Create an expression comparing the element at expr_iterator with the following elements of the collec...
void clean_pointer_expr(exprt &expr)
Clean the given pointer expression so that it has the right shape for being used for identifying shad...
std::vector< std::pair< exprt, exprt > > get_shadow_dereference_candidates(const namespacet &ns, const messaget &log, const exprt &matched_object, const std::vector< shadow_memory_statet::shadowed_addresst > &addresses, const typet &field_type, const exprt &expr, const typet &lhs_type, bool &exact_match)
Get a list of (condition, value) pairs for a certain pointer from the shadow memory,...
static exprt get_matched_expr_cond(const exprt &dereference_pointer, const exprt &expr, const namespacet &ns, const messaget &log)
Function that compares the two arguments dereference_pointer and expr, simplifies the comparison expr...
static void log_try_shadow_address(const namespacet &ns, const messaget &log, const shadow_memory_statet::shadowed_addresst &shadowed_address)
Log trying out a match between an object and a (target) shadow address.
static void log_value_set_contains_only_null(const messaget &log, const namespacet &ns, const exprt &expr, const exprt &null_pointer)
static void log_are_types_incompatible(const namespacet &ns, const exprt &expr, const shadow_memory_statet::shadowed_addresst &shadowed_address, const messaget &log)
exprt compute_max_over_bytes(const exprt &expr, const typet &field_type, const namespacet &ns)
Performs aggregation of the shadow memory field value over multiple cells for fields whose type is a ...
static void log_shadow_memory_incompatible_types(const messaget &log, const namespacet &ns, const exprt &expr, const shadow_memory_statet::shadowed_addresst &shadowed_address)
static void log_shadow_memory_message(const messaget &log, const char *text)
Generic logging function to log a text if DEBUG_SHADOW_MEMORY is defined.
void shadow_memory_log_get_field(const namespacet &ns, const messaget &log, const irep_idt &field_name, const exprt &expr)
Logs getting a value corresponding to a shadow memory field.
irep_idt extract_field_name(const exprt &string_expr)
Extracts the field name identifier from a string expression, e.g.
static exprt create_max_expr(const std::vector< exprt > &values)
Create an expression encoding the max operation over the collection values
static void remove_array_type_l2(typet &type)
If the given type is an array type, then remove the L2 level renaming from its size.
void shadow_memory_log_value_set(const namespacet &ns, const messaget &log, const std::vector< exprt > &value_set)
Logs the retrieval of the value associated with a given shadow memory field.
void shadow_memory_log_text_and_expr(const namespacet &ns, const messaget &log, const char *text, const exprt &expr)
Generic logging function that will log depending on the configured verbosity.
static exprt combine_condition_and_max_values(const std::vector< std::pair< exprt, exprt >> &conditions_and_values)
Combine each (condition, value) element in the input collection into a if-then-else expression such a...
static value_set_dereferencet::valuet get_shadow_dereference(const exprt &shadow, const object_descriptor_exprt &matched_base_descriptor, const exprt &expr, const namespacet &ns, const messaget &log)
Retrieve the shadow value a pointer expression may point to.
std::optional< exprt > get_shadow_memory(const exprt &expr, const std::vector< exprt > &value_set, const std::vector< shadow_memory_statet::shadowed_addresst > &addresses, const namespacet &ns, const messaget &log, size_t &mux_size)
Get shadow memory values for a given expression within a specified value set.
static exprt conditional_cast_floatbv_to_unsignedbv(const exprt &value)
Casts a given (float) bitvector expression to an unsigned bitvector.
static void extract_bytes_of_bv(const exprt &value, const typet &type, const typet &field_type, exprt::operandst &values)
Extract byte-sized elements from the input bitvector-typed expression value and places them into the ...
static exprt get_matched_base_cond(const exprt &shadowed_address, const exprt &matched_base_address, const namespacet &ns, const messaget &log)
Function that compares the two arguments shadowed_address and matched_base_address,...
Symex Shadow Memory Instrumentation Utilities.
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition: smt_terms.h:17
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#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 INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition: invariant.h:535
#define POSTCONDITION(CONDITION)
Definition: invariant.h:479
#define UNREACHABLE_BECAUSE(REASON)
Definition: invariant.h:526
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:145
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:97
API to expression classes.
bool can_cast_expr< typecast_exprt >(const exprt &base)
Definition: std_expr.h:2086
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3045
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2102
bool can_cast_expr< index_exprt >(const exprt &base)
Definition: std_expr.h:1517
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition: std_expr.h:256
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1402
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2936
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1533
bool can_cast_type< bool_typet >(const typet &base)
Definition: std_types.h:44
bool can_cast_type< array_typet >(const typet &type)
Check whether a reference to a typet is a array_typet.
Definition: std_types.h:875
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:888
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:214
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:518
const struct_or_union_tag_typet & to_struct_or_union_tag_type(const typet &type)
Cast a typet to a struct_or_union_tag_typet.
Definition: std_types.h:478
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
Definition: std_types.h:952
bool can_cast_expr< string_constantt >(const exprt &base)
std::size_t char_width
Definition: config.h:140
#define size_type
Definition: unistd.c:347
Pointer Dereferencing.