cprover
bv_pointers.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "bv_pointers.h"
10 
11 #include <util/arith_tools.h>
12 #include <util/c_types.h>
13 #include <util/config.h>
14 #include <util/exception_utils.h>
16 
18 {
19  PRECONDITION(expr.type().id() == ID_bool);
20 
21  const exprt::operandst &operands=expr.operands();
22 
23  if(expr.id()==ID_invalid_pointer)
24  {
25  if(operands.size()==1 &&
26  operands[0].type().id()==ID_pointer)
27  {
28  const bvt &bv=convert_bv(operands[0]);
29 
30  if(!bv.empty())
31  {
32  bvt invalid_bv;
34 
35  bvt equal_invalid_bv;
36  equal_invalid_bv.resize(object_bits);
37 
38  for(std::size_t i=0; i<object_bits; i++)
39  {
40  equal_invalid_bv[i]=prop.lequal(bv[offset_bits+i],
41  invalid_bv[offset_bits+i]);
42  }
43 
44  return prop.land(equal_invalid_bv);
45  }
46  }
47  }
48  else if(expr.id()==ID_dynamic_object)
49  {
50  if(operands.size()==1 &&
51  operands[0].type().id()==ID_pointer)
52  {
53  // we postpone
55 
56  postponed_list.push_back(postponedt());
57  postponed_list.back().op=convert_bv(operands[0]);
58  postponed_list.back().bv.push_back(l);
59  postponed_list.back().expr=expr;
60 
61  return l;
62  }
63  }
64  else if(expr.id()==ID_lt || expr.id()==ID_le ||
65  expr.id()==ID_gt || expr.id()==ID_ge)
66  {
67  if(operands.size()==2 &&
68  operands[0].type().id()==ID_pointer &&
69  operands[1].type().id()==ID_pointer)
70  {
71  const bvt &bv0=convert_bv(operands[0]);
72  const bvt &bv1=convert_bv(operands[1]);
73 
74  return bv_utils.rel(
75  bv0, expr.id(), bv1, bv_utilst::representationt::UNSIGNED);
76  }
77  }
78 
79  return SUB::convert_rest(expr);
80 }
81 
83  const namespacet &_ns,
84  propt &_prop):
85  boolbvt(_ns, _prop),
86  pointer_logic(_ns)
87 {
89  std::size_t pointer_width=boolbv_width(pointer_type(void_type()));
90  offset_bits=pointer_width-object_bits;
91  bits=pointer_width;
92 }
93 
95  const exprt &expr,
96  bvt &bv)
97 {
98  if(expr.id()==ID_symbol)
99  {
100  add_addr(expr, bv);
101  return false;
102  }
103  else if(expr.id()==ID_label)
104  {
105  add_addr(expr, bv);
106  return false;
107  }
108  else if(expr.id() == ID_null_object)
109  {
111  return false;
112  }
113  else if(expr.id()==ID_index)
114  {
115  const index_exprt &index_expr=to_index_expr(expr);
116  const exprt &array=index_expr.array();
117  const exprt &index=index_expr.index();
118  const typet &array_type=ns.follow(array.type());
119 
120  // recursive call
121  if(array_type.id()==ID_pointer)
122  {
123  // this should be gone
124  bv=convert_pointer_type(array);
125  CHECK_RETURN(bv.size()==bits);
126  }
127  else if(array_type.id()==ID_array ||
128  array_type.id()==ID_incomplete_array ||
129  array_type.id()==ID_string_constant)
130  {
131  if(convert_address_of_rec(array, bv))
132  return true;
133  CHECK_RETURN(bv.size()==bits);
134  }
135  else
136  UNREACHABLE;
137 
138  // get size
139  auto size = pointer_offset_size(array_type.subtype(), ns);
140  CHECK_RETURN(size.has_value() && *size > 0);
141 
142  offset_arithmetic(bv, *size, index);
143  CHECK_RETURN(bv.size()==bits);
144  return false;
145  }
146  else if(expr.id()==ID_byte_extract_little_endian ||
147  expr.id()==ID_byte_extract_big_endian)
148  {
149  const auto &byte_extract_expr=to_byte_extract_expr(expr);
150 
151  // recursive call
152  if(convert_address_of_rec(byte_extract_expr.op(), bv))
153  return true;
154 
155  CHECK_RETURN(bv.size()==bits);
156 
157  offset_arithmetic(bv, 1, byte_extract_expr.offset());
158  CHECK_RETURN(bv.size()==bits);
159  return false;
160  }
161  else if(expr.id()==ID_member)
162  {
163  const member_exprt &member_expr=to_member_expr(expr);
164  const exprt &struct_op=member_expr.op0();
165  const typet &struct_op_type=ns.follow(struct_op.type());
166 
167  // recursive call
168  if(convert_address_of_rec(struct_op, bv))
169  return true;
170 
171  if(struct_op_type.id()==ID_struct)
172  {
173  auto offset = member_offset(
174  to_struct_type(struct_op_type), member_expr.get_component_name(), ns);
175  CHECK_RETURN(offset.has_value());
176 
177  // add offset
178  offset_arithmetic(bv, *offset);
179  }
180  else
181  {
182  INVARIANT(
183  struct_op_type.id() == ID_union,
184  "member expression should operate on struct or union");
185  // nothing to do, all members have offset 0
186  }
187 
188  return false;
189  }
190  else if(expr.id()==ID_constant ||
191  expr.id()==ID_string_constant ||
192  expr.id()==ID_array)
193  { // constant
194  add_addr(expr, bv);
195  return false;
196  }
197  else if(expr.id()==ID_if)
198  {
199  const if_exprt &ifex=to_if_expr(expr);
200 
201  literalt cond=convert(ifex.cond());
202 
203  bvt bv1, bv2;
204 
205  if(convert_address_of_rec(ifex.true_case(), bv1))
206  return true;
207 
208  if(convert_address_of_rec(ifex.false_case(), bv2))
209  return true;
210 
211  bv=bv_utils.select(cond, bv1, bv2);
212 
213  return false;
214  }
215 
216  return true;
217 }
218 
220 {
221  PRECONDITION(expr.type().id() == ID_pointer);
222 
223  // make sure the config hasn't been changed
225 
226  if(expr.id()==ID_symbol)
227  {
228  const irep_idt &identifier=to_symbol_expr(expr).get_identifier();
229  const typet &type=expr.type();
230 
231  bvt bv;
232  bv.resize(bits);
233 
234  map.get_literals(identifier, type, bits, bv);
235 
236  return bv;
237  }
238  else if(expr.id()==ID_nondet_symbol)
239  {
240  bvt bv;
241  bv.resize(bits);
242 
243  Forall_literals(it, bv)
244  *it=prop.new_variable();
245 
246  return bv;
247  }
248  else if(expr.id()==ID_typecast)
249  {
250  const typecast_exprt &typecast_expr = to_typecast_expr(expr);
251 
252  const exprt &op = typecast_expr.op();
253  const typet &op_type=ns.follow(op.type());
254 
255  if(op_type.id()==ID_pointer)
256  return convert_bv(op);
257  else if(op_type.id()==ID_signedbv ||
258  op_type.id()==ID_unsignedbv ||
259  op_type.id()==ID_bool ||
260  op_type.id()==ID_c_enum ||
261  op_type.id()==ID_c_enum_tag)
262  {
263  // Cast from integer to pointer.
264  // We just do a zero extension.
265 
266  const bvt &op_bv=convert_bv(op);
267 
268  return bv_utils.zero_extension(op_bv, bits);
269  }
270  }
271  else if(expr.id()==ID_if)
272  {
273  return SUB::convert_if(to_if_expr(expr));
274  }
275  else if(expr.id()==ID_index)
276  {
277  return SUB::convert_index(to_index_expr(expr));
278  }
279  else if(expr.id()==ID_member)
280  {
281  return SUB::convert_member(to_member_expr(expr));
282  }
283  else if(expr.id()==ID_address_of)
284  {
285  const address_of_exprt &address_of_expr = to_address_of_expr(expr);
286 
287  bvt bv;
288  bv.resize(bits);
289 
290  if(convert_address_of_rec(address_of_expr.op(), bv))
291  {
292  conversion_failed(address_of_expr, bv);
293  return bv;
294  }
295 
296  CHECK_RETURN(bv.size()==bits);
297  return bv;
298  }
299  else if(expr.id()==ID_constant)
300  {
301  irep_idt value=to_constant_expr(expr).get_value();
302 
303  bvt bv;
304  bv.resize(bits);
305 
306  if(value==ID_NULL)
308  else
309  {
310  mp_integer i=string2integer(id2string(value), 2);
312  }
313 
314  return bv;
315  }
316  else if(expr.id()==ID_plus)
317  {
318  // this has to be pointer plus integer
319 
320  const plus_exprt &plus_expr = to_plus_expr(expr);
321 
322  bvt bv;
323 
324  mp_integer size=0;
325  std::size_t count=0;
326 
327  forall_operands(it, plus_expr)
328  {
329  if(it->type().id()==ID_pointer)
330  {
331  count++;
332  bv=convert_bv(*it);
333  CHECK_RETURN(bv.size()==bits);
334 
335  typet pointer_sub_type=it->type().subtype();
336 
337  if(pointer_sub_type.id()==ID_empty)
338  {
339  // This is a gcc extension.
340  // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
341  size = 1;
342  }
343  else
344  {
345  auto size_opt = pointer_offset_size(pointer_sub_type, ns);
346  CHECK_RETURN(size_opt.has_value() && *size_opt > 0);
347  size = *size_opt;
348  }
349  }
350  }
351 
352  INVARIANT(
353  count == 1,
354  "there should be exactly one pointer-type operand in a pointer-type sum");
355 
357 
358  forall_operands(it, plus_expr)
359  {
360  if(it->type().id()==ID_pointer)
361  continue;
362 
363  if(it->type().id()!=ID_unsignedbv &&
364  it->type().id()!=ID_signedbv)
365  {
366  bvt bv;
367  conversion_failed(plus_expr, bv);
368  return bv;
369  }
370 
372  it->type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
374 
375  bvt op=convert_bv(*it);
376  CHECK_RETURN(!op.empty());
377 
378  // we cut any extra bits off
379 
380  if(op.size()>bits)
381  op.resize(bits);
382  else if(op.size()<bits)
383  op=bv_utils.extension(op, bits, rep);
384 
385  sum=bv_utils.add(sum, op);
386  }
387 
388  offset_arithmetic(bv, size, sum);
389 
390  return bv;
391  }
392  else if(expr.id()==ID_minus)
393  {
394  // this is pointer-integer
395 
396  const minus_exprt &minus_expr = to_minus_expr(expr);
397 
398  INVARIANT(
399  minus_expr.op0().type().id() == ID_pointer,
400  "first operand should be of pointer type");
401 
402  bvt bv;
403 
404  if(
405  minus_expr.op1().type().id() != ID_unsignedbv &&
406  minus_expr.op1().type().id() != ID_signedbv)
407  {
408  bvt bv;
409  conversion_failed(minus_expr, bv);
410  return bv;
411  }
412 
413  const unary_minus_exprt neg_op1(minus_expr.op1());
414 
415  bv = convert_bv(minus_expr.op0());
416 
417  typet pointer_sub_type = minus_expr.op0().type().subtype();
418  mp_integer element_size;
419 
420  if(pointer_sub_type.id()==ID_empty)
421  {
422  // This is a gcc extension.
423  // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
424  element_size = 1;
425  }
426  else
427  {
428  auto element_size_opt = pointer_offset_size(pointer_sub_type, ns);
429  CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
430  element_size = *element_size_opt;
431  }
432 
433  offset_arithmetic(bv, element_size, neg_op1);
434 
435  return bv;
436  }
437  else if(expr.id()==ID_lshr ||
438  expr.id()==ID_shl)
439  {
440  return SUB::convert_shift(to_shift_expr(expr));
441  }
442  else if(expr.id()==ID_bitand ||
443  expr.id()==ID_bitor ||
444  expr.id()==ID_bitnot)
445  {
446  return convert_bitwise(expr);
447  }
448  else if(expr.id()==ID_concatenation)
449  {
451  }
452  else if(expr.id()==ID_byte_extract_little_endian ||
453  expr.id()==ID_byte_extract_big_endian)
454  {
456  }
457  else
458  {
459  INVARIANT(
460  expr.id() != ID_byte_update_little_endian,
461  "byte-wise pointer updates are unsupported");
462 
463  INVARIANT(
464  expr.id() != ID_byte_update_big_endian,
465  "byte-wise pointer updates are unsupported");
466  }
467 
468  return conversion_failed(expr);
469 }
470 
472 {
473  if(expr.type().id()==ID_pointer)
474  return convert_pointer_type(expr);
475 
476  if(expr.id()==ID_minus &&
477  expr.operands().size()==2 &&
478  expr.op0().type().id()==ID_pointer &&
479  expr.op1().type().id()==ID_pointer)
480  {
481  // pointer minus pointer
482  bvt op0=convert_bv(expr.op0());
483  bvt op1=convert_bv(expr.op1());
484 
485  std::size_t width=boolbv_width(expr.type());
486 
487  if(width==0)
488  return conversion_failed(expr);
489 
490  // we do a zero extension
491  op0=bv_utils.zero_extension(op0, width);
492  op1=bv_utils.zero_extension(op1, width);
493 
494  bvt bv=bv_utils.sub(op0, op1);
495 
496  typet pointer_sub_type=expr.op0().type().subtype();
497  mp_integer element_size;
498 
499  if(pointer_sub_type.id()==ID_empty)
500  {
501  // This is a gcc extension.
502  // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
503  element_size = 1;
504  }
505  else
506  {
507  auto element_size_opt = pointer_offset_size(pointer_sub_type, ns);
508  CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
509  element_size = *element_size_opt;
510  }
511 
512  if(element_size != 1)
513  {
514  bvt element_size_bv = bv_utils.build_constant(element_size, bv.size());
515  bv=bv_utils.divider(
516  bv, element_size_bv, bv_utilst::representationt::SIGNED);
517  }
518 
519  return bv;
520  }
521  else if(expr.id()==ID_pointer_offset &&
522  expr.operands().size()==1 &&
523  expr.op0().type().id()==ID_pointer)
524  {
525  bvt op0=convert_bv(expr.op0());
526 
527  std::size_t width=boolbv_width(expr.type());
528 
529  if(width==0)
530  return conversion_failed(expr);
531 
532  // we need to strip off the object part
533  op0.resize(offset_bits);
534 
535  // we do a sign extension to permit negative offsets
536  return bv_utils.sign_extension(op0, width);
537  }
538  else if(expr.id()==ID_object_size &&
539  expr.operands().size()==1 &&
540  expr.op0().type().id()==ID_pointer)
541  {
542  // we postpone until we know the objects
543  std::size_t width=boolbv_width(expr.type());
544 
545  bvt bv;
546  bv.resize(width);
547 
548  for(std::size_t i=0; i<width; i++)
549  bv[i]=prop.new_variable();
550 
551  postponed_list.push_back(postponedt());
552 
553  postponed_list.back().op=convert_bv(expr.op0());
554  postponed_list.back().bv=bv;
555  postponed_list.back().expr=expr;
556 
557  return bv;
558  }
559  else if(expr.id()==ID_pointer_object &&
560  expr.operands().size()==1 &&
561  expr.op0().type().id()==ID_pointer)
562  {
563  bvt op0=convert_bv(expr.op0());
564 
565  std::size_t width=boolbv_width(expr.type());
566 
567  if(width==0)
568  return conversion_failed(expr);
569 
570  // erase offset bits
571 
572  op0.erase(op0.begin()+0, op0.begin()+offset_bits);
573 
574  return bv_utils.zero_extension(op0, width);
575  }
576  else if(expr.id()==ID_typecast &&
577  expr.operands().size()==1 &&
578  expr.op0().type().id()==ID_pointer)
579  {
580  // pointer to int
581  bvt op0=convert_pointer_type(expr.op0());
582 
583  // squeeze it in!
584 
585  std::size_t width=boolbv_width(expr.type());
586 
587  if(width==0)
588  return conversion_failed(expr);
589 
590  return bv_utils.zero_extension(op0, width);
591  }
592 
593  return SUB::convert_bitvector(expr);
594 }
595 
597  const bvt &bv,
598  const std::vector<bool> &unknown,
599  std::size_t offset,
600  const typet &type) const
601 {
602  if(type.id()!=ID_pointer)
603  return SUB::bv_get_rec(bv, unknown, offset, type);
604 
605  std::string value_addr, value_offset, value;
606 
607  for(std::size_t i=0; i<bits; i++)
608  {
609  char ch=0;
610  std::size_t bit_nr=i+offset;
611 
612  if(unknown[bit_nr])
613  ch='0';
614  else
615  {
616  switch(prop.l_get(bv[bit_nr]).get_value())
617  {
618  case tvt::tv_enumt::TV_FALSE: ch='0'; break;
619  case tvt::tv_enumt::TV_TRUE: ch='1'; break;
620  case tvt::tv_enumt::TV_UNKNOWN: ch='0'; break;
621  default: UNREACHABLE;
622  }
623  }
624 
625  value=ch+value;
626 
627  if(i<offset_bits)
628  value_offset=ch+value_offset;
629  else
630  value_addr=ch+value_addr;
631  }
632 
633  // we treat these like bit-vector constants, but with
634  // some additional annotation
635 
636  const irep_idt bvrep = make_bvrep(bits, [&value](std::size_t i) {
637  return value[value.size() - 1 - i] == '1';
638  });
639 
640  constant_exprt result(bvrep, type);
641 
642  pointer_logict::pointert pointer;
643  pointer.object =
644  numeric_cast_v<std::size_t>(binary2integer(value_addr, false));
645  pointer.offset=binary2integer(value_offset, true);
646 
647  // we add the elaborated expression as operand
648  result.copy_to_operands(
649  pointer_logic.pointer_expr(pointer, to_pointer_type(type)));
650 
651  return std::move(result);
652 }
653 
654 void bv_pointerst::encode(std::size_t addr, bvt &bv)
655 {
656  bv.resize(bits);
657 
658  // set offset to zero
659  for(std::size_t i=0; i<offset_bits; i++)
660  bv[i]=const_literal(false);
661 
662  // set variable part
663  for(std::size_t i=0; i<object_bits; i++)
664  bv[offset_bits+i]=const_literal((addr&(std::size_t(1)<<i))!=0);
665 }
666 
668 {
669  bvt bv1=bv;
670  bv1.resize(offset_bits); // strip down
671 
673 
674  bvt tmp=bv_utils.add(bv1, bv2);
675 
676  // copy offset bits
677  for(std::size_t i=0; i<offset_bits; i++)
678  bv[i]=tmp[i];
679 }
680 
682  bvt &bv,
683  const mp_integer &factor,
684  const exprt &index)
685 {
686  bvt bv_index=convert_bv(index);
687 
689  index.type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
691 
692  bv_index=bv_utils.extension(bv_index, offset_bits, rep);
693 
694  offset_arithmetic(bv, factor, bv_index);
695 }
696 
698  bvt &bv,
699  const mp_integer &factor,
700  const bvt &index)
701 {
702  bvt bv_index;
703 
704  if(factor==1)
705  bv_index=index;
706  else
707  {
708  bvt bv_factor=bv_utils.build_constant(factor, index.size());
709  bv_index=bv_utils.unsigned_multiplier(index, bv_factor);
710  }
711 
712  bv_index=bv_utils.zero_extension(bv_index, bv.size());
713 
714  bvt bv_tmp=bv_utils.add(bv, bv_index);
715 
716  // copy lower parts of result
717  for(std::size_t i=0; i<offset_bits; i++)
718  bv[i]=bv_tmp[i];
719 }
720 
721 void bv_pointerst::add_addr(const exprt &expr, bvt &bv)
722 {
723  std::size_t a=pointer_logic.add_object(expr);
724 
725  const std::size_t max_objects=std::size_t(1)<<object_bits;
726 
727  if(a==max_objects)
728  throw analysis_exceptiont(
729  "too many addressed objects: maximum number of objects is set to 2^n=" +
730  std::to_string(max_objects) + " (with n=" + std::to_string(object_bits) +
731  "); " +
732  "use the `--object-bits n` option to increase the maximum number");
733 
734  encode(a, bv);
735 }
736 
738  const postponedt &postponed)
739 {
740  if(postponed.expr.id()==ID_dynamic_object)
741  {
742  const pointer_logict::objectst &objects=
744 
745  std::size_t number=0;
746 
748  it=objects.begin();
749  it!=objects.end();
750  it++, number++)
751  {
752  const exprt &expr=*it;
753 
754  bool is_dynamic=pointer_logic.is_dynamic_object(expr);
755 
756  // only compare object part
757  bvt bv;
758  encode(number, bv);
759 
760  bv.erase(bv.begin(), bv.begin()+offset_bits);
761 
762  bvt saved_bv=postponed.op;
763  saved_bv.erase(saved_bv.begin(), saved_bv.begin()+offset_bits);
764 
765  POSTCONDITION(bv.size()==saved_bv.size());
766  PRECONDITION(postponed.bv.size()==1);
767 
768  literalt l1=bv_utils.equal(bv, saved_bv);
769  literalt l2=postponed.bv.front();
770 
771  if(!is_dynamic)
772  l2=!l2;
773 
774  prop.l_set_to(prop.limplies(l1, l2), true);
775  }
776  }
777  else if(postponed.expr.id()==ID_object_size)
778  {
779  const pointer_logict::objectst &objects=
781 
782  std::size_t number=0;
783 
785  it=objects.begin();
786  it!=objects.end();
787  it++, number++)
788  {
789  const exprt &expr=*it;
790 
791  if(expr.id() != ID_symbol)
792  continue;
793 
794  const exprt size_expr = size_of_expr(expr.type(), ns);
795 
796  if(size_expr.is_nil())
797  continue;
798 
799  const exprt object_size =
800  typecast_exprt::conditional_cast(size_expr, postponed.expr.type());
801 
802  // only compare object part
803  bvt bv;
804  encode(number, bv);
805 
806  bv.erase(bv.begin(), bv.begin()+offset_bits);
807 
808  bvt saved_bv=postponed.op;
809  saved_bv.erase(saved_bv.begin(), saved_bv.begin()+offset_bits);
810 
811  bvt size_bv = convert_bv(object_size);
812 
813  POSTCONDITION(bv.size()==saved_bv.size());
814  PRECONDITION(postponed.bv.size()>=1);
815  PRECONDITION(size_bv.size() == postponed.bv.size());
816 
817  literalt l1=bv_utils.equal(bv, saved_bv);
818  literalt l2=bv_utils.equal(postponed.bv, size_bv);
819 
820  prop.l_set_to(prop.limplies(l1, l2), true);
821  }
822  }
823  else
824  UNREACHABLE;
825 }
826 
828 {
829  // post-processing arrays may yield further objects, do this first
831 
832  for(postponed_listt::const_iterator
833  it=postponed_list.begin();
834  it!=postponed_list.end();
835  it++)
836  do_postponed(*it);
837 
838  // Clear the list to avoid re-doing in case of incremental usage.
839  postponed_list.clear();
840 }
bv_pointerst::object_bits
unsigned object_bits
Definition: bv_pointers.h:30
pointer_logict::get_null_object
std::size_t get_null_object() const
Definition: pointer_logic.h:59
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:35
pointer_offset_size.h
template_numberingt::begin
iterator begin()
Definition: numbering.h:85
configt::bv_encodingt::object_bits
std::size_t object_bits
Definition: config.h:165
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2291
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
boolbvt::map
boolbv_mapt map
Definition: boolbv.h:101
typet::subtype
const typet & subtype() const
Definition: type.h:38
boolbvt::convert_member
virtual bvt convert_member(const member_exprt &expr)
Definition: boolbv_member.cpp:16
configt::bv_encoding
struct configt::bv_encodingt bv_encoding
arith_tools.h
bv_pointerst::convert_address_of_rec
bool convert_address_of_rec(const exprt &expr, bvt &bv)
Definition: bv_pointers.cpp:94
make_bvrep
irep_idt make_bvrep(const std::size_t width, const std::function< bool(std::size_t)> f)
construct a bit-vector representation from a functor
Definition: arith_tools.cpp:329
bv_pointerst::postponedt::op
bvt op
Definition: bv_pointers.h:59
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
boolbvt::convert_bitvector
virtual bvt convert_bitvector(const exprt &expr)
Converts an expression into its gate-level representation and returns a vector of literals correspond...
Definition: boolbv.cpp:168
typet
The type of an expression, extends irept.
Definition: type.h:27
bvt
std::vector< literalt > bvt
Definition: literal.h:200
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:53
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
bv_pointerst::postponed_list
postponed_listt postponed_list
Definition: bv_pointers.h:64
bv_pointerst::postponedt::expr
exprt expr
Definition: bv_pointers.h:60
mp_integer
BigInt mp_integer
Definition: mp_arith.h:22
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:3427
string2integer
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
template_numberingt
Definition: numbering.h:21
pointer_logict::add_object
std::size_t add_object(const exprt &expr)
Definition: pointer_logic.cpp:49
bv_utilst::representationt::UNSIGNED
@ UNSIGNED
boolbv_mapt::get_literals
void get_literals(const irep_idt &identifier, const typet &type, const std::size_t width, bvt &literals)
Definition: boolbv_map.cpp:86
bv_pointerst::bv_get_rec
exprt bv_get_rec(const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const override
Definition: bv_pointers.cpp:596
bv_utilst::sign_extension
bvt sign_extension(const bvt &bv, std::size_t new_size)
Definition: bv_utils.h:179
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
bv_pointerst::do_postponed
void do_postponed(const postponedt &postponed)
Definition: bv_pointers.cpp:737
propt::new_variable
virtual literalt new_variable()=0
boolbvt::convert_index
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
Definition: boolbv_index.cpp:275
exprt
Base class for all expressions.
Definition: expr.h:54
exprt::op0
exprt & op0()
Definition: expr.h:84
propt::l_set_to
virtual void l_set_to(literalt a, bool value)
Definition: prop.h:44
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:53
bv_pointerst::convert_pointer_type
virtual bvt convert_pointer_type(const exprt &expr)
Definition: bv_pointers.cpp:219
bv_utilst::unsigned_multiplier
bvt unsigned_multiplier(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:635
propt::land
virtual literalt land(literalt a, literalt b)=0
Forall_literals
#define Forall_literals(it, bv)
Definition: literal.h:206
bv_utilst::select
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
Definition: bv_utils.cpp:96
to_minus_expr
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:1128
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3465
boolbvt::convert_concatenation
virtual bvt convert_concatenation(const concatenation_exprt &expr)
Definition: boolbv_concatenation.cpp:13
bv_pointers.h
to_concatenation_expr
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
Definition: std_expr.h:4589
pointer_logict::pointert::object
std::size_t object
Definition: pointer_logic.h:31
to_shift_expr
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
Definition: std_expr.h:2917
boolbvt::convert_shift
virtual bvt convert_shift(const binary_exprt &expr)
Definition: boolbv_shift.cpp:15
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
boolbvt::convert_byte_extract
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
Definition: boolbv_byte_extract.cpp:41
tvt::tv_enumt::TV_TRUE
@ TV_TRUE
bv_utilst::add
bvt add(const bvt &op0, const bvt &op1)
Definition: bv_utils.h:64
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition: boolbv.h:92
messaget::result
mstreamt & result() const
Definition: message.h:396
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:110
pointer_logict::objects
objectst objects
Definition: pointer_logic.h:27
size_of_expr
exprt size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:292
propt::limplies
virtual literalt limplies(literalt a, literalt b)=0
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:3282
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bv_pointerst::convert_bitvector
bvt convert_bitvector(const exprt &expr) override
Converts an expression into its gate-level representation and returns a vector of literals correspond...
Definition: bv_pointers.cpp:471
bv_utilst::representationt::SIGNED
@ SIGNED
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:20
pointer_logict::pointert::offset
mp_integer offset
Definition: pointer_logic.h:32
bv_utilst::representationt
representationt
Definition: bv_utils.h:31
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
boolbvt::convert_if
virtual bvt convert_if(const if_exprt &expr)
Definition: boolbv_if.cpp:12
to_plus_expr
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:1076
exprt::op1
exprt & op1()
Definition: expr.h:87
const_literal
literalt const_literal(bool value)
Definition: literal.h:187
POSTCONDITION
#define POSTCONDITION(CONDITION)
Definition: invariant.h:454
boolbvt::post_process
void post_process() override
Definition: boolbv.h:64
index_exprt::index
exprt & index()
Definition: std_expr.h:1631
bv_pointerst::pointer_logic
pointer_logict pointer_logic
Definition: bv_pointers.h:25
decision_proceduret::ns
const namespacet & ns
Definition: decision_procedure.h:61
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
template_numberingt::end
iterator end()
Definition: numbering.h:98
unary_minus_exprt
The unary minus expression.
Definition: std_expr.h:469
index_exprt::array
exprt & array()
Definition: std_expr.h:1621
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
object_size
exprt object_size(const exprt &pointer)
Definition: pointer_predicates.cpp:32
bv_pointerst::bits
unsigned bits
Definition: bv_pointers.h:30
irept::is_nil
bool is_nil() const
Definition: irep.h:172
irept::id
const irep_idt & id() const
Definition: irep.h:259
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:371
boolbvt::convert_bv
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Definition: boolbv.cpp:112
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
bv_pointerst::encode
void encode(std::size_t object, bvt &bv)
Definition: bv_pointers.cpp:654
prop_conv_solvert::convert
literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:157
minus_exprt
Binary minus.
Definition: std_expr.h:1106
config
configt config
Definition: config.cpp:24
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3890
boolbvt::convert_bitwise
virtual bvt convert_bitwise(const exprt &expr)
Definition: boolbv_bitwise.cpp:12
bv_utilst::build_constant
bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:15
propt::lequal
virtual literalt lequal(literalt a, literalt b)=0
bv_utilst::rel
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
Definition: bv_utils.cpp:1293
bv_pointerst::offset_bits
unsigned offset_bits
Definition: bv_pointers.h:30
propt
TO_BE_DOCUMENTED.
Definition: prop.h:24
pointer_offset_size
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
Definition: pointer_offset_size.cpp:90
pointer_logict::is_dynamic_object
bool is_dynamic_object(const exprt &expr) const
Definition: pointer_logic.cpp:23
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:3455
propt::l_get
virtual tvt l_get(literalt a) const =0
void_type
typet void_type()
Definition: c_types.cpp:253
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
bv_pointerst::postponedt
Definition: bv_pointers.h:57
boolbvt::bv_utils
bv_utilst bv_utils
Definition: boolbv.h:95
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2306
bv_utilst::extension
bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
Definition: bv_utils.cpp:109
binary2integer
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
if_exprt::cond
exprt & cond()
Definition: std_expr.h:3445
literalt
Definition: literal.h:24
bv_utilst::divider
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.h:87
pointer_logict::get_invalid_object
std::size_t get_invalid_object() const
Definition: pointer_logic.h:65
boolbvt::bv_get_rec
virtual exprt bv_get_rec(const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const
Definition: boolbv_get.cpp:68
boolbvt
Definition: boolbv.h:32
config.h
tvt::tv_enumt::TV_UNKNOWN
@ TV_UNKNOWN
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:3915
bv_pointerst::bv_pointerst
bv_pointerst(const namespacet &_ns, propt &_prop)
Definition: bv_pointers.cpp:82
exprt::operands
operandst & operands()
Definition: expr.h:78
index_exprt
Array index operator.
Definition: std_expr.h:1595
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:3255
bv_utilst::equal
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1116
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2277
tvt::get_value
tv_enumt get_value() const
Definition: threeval.h:40
bv_pointerst::offset_arithmetic
void offset_arithmetic(bvt &bv, const mp_integer &x)
Definition: bv_pointers.cpp:667
boolbvt::convert_rest
literalt convert_rest(const exprt &expr) override
Definition: boolbv.cpp:426
constant_exprt
A constant literal expression.
Definition: std_expr.h:4384
bv_pointerst::convert_rest
literalt convert_rest(const exprt &expr) override
Definition: bv_pointers.cpp:17
bv_pointerst::post_process
void post_process() override
Definition: bv_pointers.cpp:827
tvt::tv_enumt::TV_FALSE
@ TV_FALSE
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:4403
member_offset
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
Definition: pointer_offset_size.cpp:24
template_numberingt::const_iterator
typename data_typet::const_iterator const_iterator
Definition: numbering.h:35
c_types.h
bv_pointerst::add_addr
virtual void add_addr(const exprt &expr, bvt &bv)
Definition: bv_pointers.cpp:721
pointer_logict::pointert
Definition: pointer_logic.h:29
validation_modet::INVARIANT
@ INVARIANT
bv_utilst::zero_extension
bvt zero_extension(const bvt &bv, std::size_t new_size)
Definition: bv_utils.h:184
prop_conv_solvert::prop
propt & prop
Definition: prop_conv.h:152
bv_pointerst::postponedt::bv
bvt bv
Definition: bv_pointers.h:59
bv_utilst::sub
bvt sub(const bvt &op0, const bvt &op1)
Definition: bv_utils.h:65
pointer_logict::pointer_expr
exprt pointer_expr(const pointert &pointer, const pointer_typet &type) const
Definition: pointer_logic.cpp:73
analysis_exceptiont
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
Definition: exception_utils.h:156
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4423
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470