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_is_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_is_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  message_handlert &message_handler)
86  : boolbvt(_ns, _prop, message_handler), pointer_logic(_ns)
87 {
89  std::size_t pointer_width = boolbv_width(pointer_type(empty_typet()));
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 = 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_string_constant)
129  {
130  if(convert_address_of_rec(array, bv))
131  return true;
132  CHECK_RETURN(bv.size()==bits);
133  }
134  else
135  UNREACHABLE;
136 
137  // get size
138  auto size = pointer_offset_size(array_type.subtype(), ns);
139  CHECK_RETURN(size.has_value() && *size > 0);
140 
141  offset_arithmetic(bv, *size, index);
142  CHECK_RETURN(bv.size()==bits);
143  return false;
144  }
145  else if(expr.id()==ID_byte_extract_little_endian ||
146  expr.id()==ID_byte_extract_big_endian)
147  {
148  const auto &byte_extract_expr=to_byte_extract_expr(expr);
149 
150  // recursive call
151  if(convert_address_of_rec(byte_extract_expr.op(), bv))
152  return true;
153 
154  CHECK_RETURN(bv.size()==bits);
155 
156  offset_arithmetic(bv, 1, byte_extract_expr.offset());
157  CHECK_RETURN(bv.size()==bits);
158  return false;
159  }
160  else if(expr.id()==ID_member)
161  {
162  const member_exprt &member_expr=to_member_expr(expr);
163  const exprt &struct_op = member_expr.compound();
164  const typet &struct_op_type=ns.follow(struct_op.type());
165 
166  // recursive call
167  if(convert_address_of_rec(struct_op, bv))
168  return true;
169 
170  if(struct_op_type.id()==ID_struct)
171  {
172  auto offset = member_offset(
173  to_struct_type(struct_op_type), member_expr.get_component_name(), ns);
174  CHECK_RETURN(offset.has_value());
175 
176  // add offset
177  offset_arithmetic(bv, *offset);
178  }
179  else
180  {
181  INVARIANT(
182  struct_op_type.id() == ID_union,
183  "member expression should operate on struct or union");
184  // nothing to do, all members have offset 0
185  }
186 
187  return false;
188  }
189  else if(expr.id()==ID_constant ||
190  expr.id()==ID_string_constant ||
191  expr.id()==ID_array)
192  { // constant
193  add_addr(expr, bv);
194  return false;
195  }
196  else if(expr.id()==ID_if)
197  {
198  const if_exprt &ifex=to_if_expr(expr);
199 
200  literalt cond=convert(ifex.cond());
201 
202  bvt bv1, bv2;
203 
204  if(convert_address_of_rec(ifex.true_case(), bv1))
205  return true;
206 
207  if(convert_address_of_rec(ifex.false_case(), bv2))
208  return true;
209 
210  bv=bv_utils.select(cond, bv1, bv2);
211 
212  return false;
213  }
214 
215  return true;
216 }
217 
219 {
220  PRECONDITION(expr.type().id() == ID_pointer);
221 
222  // make sure the config hasn't been changed
224 
225  if(expr.id()==ID_symbol)
226  {
227  const irep_idt &identifier=to_symbol_expr(expr).get_identifier();
228  const typet &type=expr.type();
229 
230  bvt bv;
231  bv.resize(bits);
232 
233  map.get_literals(identifier, type, bits, bv);
234 
235  return bv;
236  }
237  else if(expr.id()==ID_nondet_symbol)
238  {
239  bvt bv;
240  bv.resize(bits);
241 
242  Forall_literals(it, bv)
243  *it=prop.new_variable();
244 
245  return bv;
246  }
247  else if(expr.id()==ID_typecast)
248  {
249  const typecast_exprt &typecast_expr = to_typecast_expr(expr);
250 
251  const exprt &op = typecast_expr.op();
252  const typet &op_type = op.type();
253 
254  if(op_type.id()==ID_pointer)
255  return convert_bv(op);
256  else if(
257  can_cast_type<bitvector_typet>(op_type) || op_type.id() == ID_bool ||
258  op_type.id() == ID_c_enum || op_type.id() == ID_c_enum_tag)
259  {
260  // Cast from a bitvector type to pointer.
261  // We just do a zero extension.
262 
263  const bvt &op_bv=convert_bv(op);
264 
265  return bv_utils.zero_extension(op_bv, bits);
266  }
267  }
268  else if(expr.id()==ID_if)
269  {
270  return SUB::convert_if(to_if_expr(expr));
271  }
272  else if(expr.id()==ID_index)
273  {
274  return SUB::convert_index(to_index_expr(expr));
275  }
276  else if(expr.id()==ID_member)
277  {
278  return SUB::convert_member(to_member_expr(expr));
279  }
280  else if(expr.id()==ID_address_of)
281  {
282  const address_of_exprt &address_of_expr = to_address_of_expr(expr);
283 
284  bvt bv;
285  bv.resize(bits);
286 
287  if(convert_address_of_rec(address_of_expr.op(), bv))
288  {
289  conversion_failed(address_of_expr, bv);
290  return bv;
291  }
292 
293  CHECK_RETURN(bv.size()==bits);
294  return bv;
295  }
296  else if(expr.id()==ID_constant)
297  {
298  irep_idt value=to_constant_expr(expr).get_value();
299 
300  bvt bv;
301  bv.resize(bits);
302 
303  if(value==ID_NULL)
305  else
306  {
307  mp_integer i=string2integer(id2string(value), 2);
309  }
310 
311  return bv;
312  }
313  else if(expr.id()==ID_plus)
314  {
315  // this has to be pointer plus integer
316 
317  const plus_exprt &plus_expr = to_plus_expr(expr);
318 
319  bvt bv;
320 
321  mp_integer size=0;
322  std::size_t count=0;
323 
324  forall_operands(it, plus_expr)
325  {
326  if(it->type().id()==ID_pointer)
327  {
328  count++;
329  bv=convert_bv(*it);
330  CHECK_RETURN(bv.size()==bits);
331 
332  typet pointer_sub_type=it->type().subtype();
333 
334  if(pointer_sub_type.id()==ID_empty)
335  {
336  // This is a gcc extension.
337  // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
338  size = 1;
339  }
340  else
341  {
342  auto size_opt = pointer_offset_size(pointer_sub_type, ns);
343  CHECK_RETURN(size_opt.has_value() && *size_opt > 0);
344  size = *size_opt;
345  }
346  }
347  }
348 
349  INVARIANT(
350  count == 1,
351  "there should be exactly one pointer-type operand in a pointer-type sum");
352 
354 
355  forall_operands(it, plus_expr)
356  {
357  if(it->type().id()==ID_pointer)
358  continue;
359 
360  if(it->type().id()!=ID_unsignedbv &&
361  it->type().id()!=ID_signedbv)
362  {
363  bvt failed_bv;
364  conversion_failed(plus_expr, failed_bv);
365  return failed_bv;
366  }
367 
369  it->type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
371 
372  bvt op=convert_bv(*it);
373  CHECK_RETURN(!op.empty());
374 
375  // we cut any extra bits off
376 
377  if(op.size()>bits)
378  op.resize(bits);
379  else if(op.size()<bits)
380  op=bv_utils.extension(op, bits, rep);
381 
382  sum=bv_utils.add(sum, op);
383  }
384 
385  offset_arithmetic(bv, size, sum);
386 
387  return bv;
388  }
389  else if(expr.id()==ID_minus)
390  {
391  // this is pointer-integer
392 
393  const minus_exprt &minus_expr = to_minus_expr(expr);
394 
395  INVARIANT(
396  minus_expr.lhs().type().id() == ID_pointer,
397  "first operand should be of pointer type");
398 
399  if(
400  minus_expr.rhs().type().id() != ID_unsignedbv &&
401  minus_expr.rhs().type().id() != ID_signedbv)
402  {
403  bvt bv;
404  conversion_failed(minus_expr, bv);
405  return bv;
406  }
407 
408  const unary_minus_exprt neg_op1(minus_expr.rhs());
409 
410  bvt bv = convert_bv(minus_expr.lhs());
411 
412  typet pointer_sub_type = minus_expr.rhs().type().subtype();
413  mp_integer element_size;
414 
415  if(pointer_sub_type.id()==ID_empty)
416  {
417  // This is a gcc extension.
418  // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
419  element_size = 1;
420  }
421  else
422  {
423  auto element_size_opt = pointer_offset_size(pointer_sub_type, ns);
424  CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
425  element_size = *element_size_opt;
426  }
427 
428  offset_arithmetic(bv, element_size, neg_op1);
429 
430  return bv;
431  }
432  else if(expr.id()==ID_lshr ||
433  expr.id()==ID_shl)
434  {
435  return SUB::convert_shift(to_shift_expr(expr));
436  }
437  else if(expr.id()==ID_bitand ||
438  expr.id()==ID_bitor ||
439  expr.id()==ID_bitnot)
440  {
441  return convert_bitwise(expr);
442  }
443  else if(expr.id()==ID_concatenation)
444  {
446  }
447  else if(expr.id()==ID_byte_extract_little_endian ||
448  expr.id()==ID_byte_extract_big_endian)
449  {
451  }
452  else
453  {
455  }
456 
457  return conversion_failed(expr);
458 }
459 
460 static bool is_pointer_subtraction(const exprt &expr)
461 {
462  if(expr.id() != ID_minus)
463  return false;
464 
465  const auto &minus_expr = to_minus_expr(expr);
466 
467  return minus_expr.lhs().type().id() == ID_pointer &&
468  minus_expr.rhs().type().id() == ID_pointer;
469 }
470 
472 {
473  if(expr.type().id()==ID_pointer)
474  return convert_pointer_type(expr);
475 
476  if(is_pointer_subtraction(expr))
477  {
478  // pointer minus pointer
479  const auto &minus_expr = to_minus_expr(expr);
480  bvt lhs = convert_bv(minus_expr.lhs());
481  bvt rhs = convert_bv(minus_expr.rhs());
482 
483  std::size_t width=boolbv_width(expr.type());
484 
485  if(width==0)
486  return conversion_failed(expr);
487 
488  // we do a zero extension
489  lhs = bv_utils.zero_extension(lhs, width);
490  rhs = bv_utils.zero_extension(rhs, width);
491 
492  bvt bv = bv_utils.sub(lhs, rhs);
493 
494  typet pointer_sub_type = minus_expr.lhs().type().subtype();
495  mp_integer element_size;
496 
497  if(pointer_sub_type.id()==ID_empty)
498  {
499  // This is a gcc extension.
500  // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
501  element_size = 1;
502  }
503  else
504  {
505  auto element_size_opt = pointer_offset_size(pointer_sub_type, ns);
506  CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
507  element_size = *element_size_opt;
508  }
509 
510  if(element_size != 1)
511  {
512  bvt element_size_bv = bv_utils.build_constant(element_size, bv.size());
513  bv=bv_utils.divider(
514  bv, element_size_bv, bv_utilst::representationt::SIGNED);
515  }
516 
517  return bv;
518  }
519  else if(
520  expr.id() == ID_pointer_offset &&
521  to_unary_expr(expr).op().type().id() == ID_pointer)
522  {
523  bvt op0 = convert_bv(to_unary_expr(expr).op());
524 
525  std::size_t width=boolbv_width(expr.type());
526 
527  if(width==0)
528  return conversion_failed(expr);
529 
530  // we need to strip off the object part
531  op0.resize(offset_bits);
532 
533  // we do a sign extension to permit negative offsets
534  return bv_utils.sign_extension(op0, width);
535  }
536  else if(
537  expr.id() == ID_object_size &&
538  to_unary_expr(expr).op().type().id() == ID_pointer)
539  {
540  // we postpone until we know the objects
541  std::size_t width=boolbv_width(expr.type());
542 
543  bvt bv;
544  bv.resize(width);
545 
546  for(std::size_t i=0; i<width; i++)
547  bv[i]=prop.new_variable();
548 
549  postponed_list.push_back(postponedt());
550 
551  postponed_list.back().op = convert_bv(to_unary_expr(expr).op());
552  postponed_list.back().bv=bv;
553  postponed_list.back().expr=expr;
554 
555  return bv;
556  }
557  else if(
558  expr.id() == ID_pointer_object &&
559  to_unary_expr(expr).op().type().id() == ID_pointer)
560  {
561  bvt op0 = convert_bv(to_unary_expr(expr).op());
562 
563  std::size_t width=boolbv_width(expr.type());
564 
565  if(width==0)
566  return conversion_failed(expr);
567 
568  // erase offset bits
569 
570  op0.erase(op0.begin()+0, op0.begin()+offset_bits);
571 
572  return bv_utils.zero_extension(op0, width);
573  }
574  else if(
575  expr.id() == ID_typecast &&
576  to_typecast_expr(expr).op().type().id() == ID_pointer)
577  {
578  // pointer to int
579  bvt op0 = convert_pointer_type(to_typecast_expr(expr).op());
580 
581  // squeeze it in!
582 
583  std::size_t width=boolbv_width(expr.type());
584 
585  if(width==0)
586  return conversion_failed(expr);
587 
588  return bv_utils.zero_extension(op0, width);
589  }
590 
591  return SUB::convert_bitvector(expr);
592 }
593 
595  const exprt &expr,
596  const bvt &bv,
597  const std::vector<bool> &unknown,
598  std::size_t offset,
599  const typet &type) const
600 {
601  if(type.id()!=ID_pointer)
602  return SUB::bv_get_rec(expr, bv, unknown, offset, type);
603 
604  std::string value_addr, value_offset, value;
605 
606  for(std::size_t i=0; i<bits; i++)
607  {
608  char ch=0;
609  std::size_t bit_nr=i+offset;
610 
611  if(unknown[bit_nr])
612  ch='0';
613  else
614  {
615  switch(prop.l_get(bv[bit_nr]).get_value())
616  {
617  case tvt::tv_enumt::TV_FALSE: ch='0'; break;
618  case tvt::tv_enumt::TV_TRUE: ch='1'; break;
619  case tvt::tv_enumt::TV_UNKNOWN: ch='0'; break;
620  default: UNREACHABLE;
621  }
622  }
623 
624  value=ch+value;
625 
626  if(i<offset_bits)
627  value_offset=ch+value_offset;
628  else
629  value_addr=ch+value_addr;
630  }
631 
632  // we treat these like bit-vector constants, but with
633  // some additional annotation
634 
635  const irep_idt bvrep = make_bvrep(bits, [&value](std::size_t i) {
636  return value[value.size() - 1 - i] == '1';
637  });
638 
639  constant_exprt result(bvrep, type);
640 
641  pointer_logict::pointert pointer;
642  pointer.object =
643  numeric_cast_v<std::size_t>(binary2integer(value_addr, false));
644  pointer.offset=binary2integer(value_offset, true);
645 
646  // we add the elaborated expression as operand
647  result.copy_to_operands(
648  pointer_logic.pointer_expr(pointer, to_pointer_type(type)));
649 
650  return std::move(result);
651 }
652 
653 void bv_pointerst::encode(std::size_t addr, bvt &bv)
654 {
655  bv.resize(bits);
656 
657  // set offset to zero
658  for(std::size_t i=0; i<offset_bits; i++)
659  bv[i]=const_literal(false);
660 
661  // set variable part
662  for(std::size_t i=0; i<object_bits; i++)
663  bv[offset_bits+i]=const_literal((addr&(std::size_t(1)<<i))!=0);
664 }
665 
667 {
668  bvt bv1=bv;
669  bv1.resize(offset_bits); // strip down
670 
672 
673  bvt tmp=bv_utils.add(bv1, bv2);
674 
675  // copy offset bits
676  for(std::size_t i=0; i<offset_bits; i++)
677  bv[i]=tmp[i];
678 }
679 
681  bvt &bv,
682  const mp_integer &factor,
683  const exprt &index)
684 {
685  bvt bv_index=convert_bv(index);
686 
688  index.type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
690 
691  bv_index=bv_utils.extension(bv_index, offset_bits, rep);
692 
693  offset_arithmetic(bv, factor, bv_index);
694 }
695 
697  bvt &bv,
698  const mp_integer &factor,
699  const bvt &index)
700 {
701  bvt bv_index;
702 
703  if(factor==1)
704  bv_index=index;
705  else
706  {
707  bvt bv_factor=bv_utils.build_constant(factor, index.size());
708  bv_index=bv_utils.unsigned_multiplier(index, bv_factor);
709  }
710 
711  bv_index=bv_utils.zero_extension(bv_index, bv.size());
712 
713  bvt bv_tmp=bv_utils.add(bv, bv_index);
714 
715  // copy lower parts of result
716  for(std::size_t i=0; i<offset_bits; i++)
717  bv[i]=bv_tmp[i];
718 }
719 
720 void bv_pointerst::add_addr(const exprt &expr, bvt &bv)
721 {
722  std::size_t a=pointer_logic.add_object(expr);
723 
724  const std::size_t max_objects=std::size_t(1)<<object_bits;
725 
726  if(a==max_objects)
727  throw analysis_exceptiont(
728  "too many addressed objects: maximum number of objects is set to 2^n=" +
729  std::to_string(max_objects) + " (with n=" + std::to_string(object_bits) +
730  "); " +
731  "use the `--object-bits n` option to increase the maximum number");
732 
733  encode(a, bv);
734 }
735 
737  const postponedt &postponed)
738 {
739  if(postponed.expr.id() == ID_is_dynamic_object)
740  {
741  const auto &objects = pointer_logic.objects;
742  std::size_t number=0;
743 
744  for(auto it = objects.cbegin(); it != objects.cend(); ++it, ++number)
745  {
746  const exprt &expr=*it;
747 
748  bool is_dynamic=pointer_logic.is_dynamic_object(expr);
749 
750  // only compare object part
751  bvt bv;
752  encode(number, bv);
753 
754  bv.erase(bv.begin(), bv.begin()+offset_bits);
755 
756  bvt saved_bv=postponed.op;
757  saved_bv.erase(saved_bv.begin(), saved_bv.begin()+offset_bits);
758 
759  POSTCONDITION(bv.size()==saved_bv.size());
760  PRECONDITION(postponed.bv.size()==1);
761 
762  literalt l1=bv_utils.equal(bv, saved_bv);
763  literalt l2=postponed.bv.front();
764 
765  if(!is_dynamic)
766  l2=!l2;
767 
768  prop.l_set_to_true(prop.limplies(l1, l2));
769  }
770  }
771  else if(postponed.expr.id()==ID_object_size)
772  {
773  const auto &objects = pointer_logic.objects;
774  std::size_t number=0;
775 
776  for(auto it = objects.cbegin(); it != objects.cend(); ++it, ++number)
777  {
778  const exprt &expr=*it;
779 
780  if(expr.id() != ID_symbol && expr.id() != ID_string_constant)
781  continue;
782 
783  const auto size_expr = size_of_expr(expr.type(), ns);
784 
785  if(!size_expr.has_value())
786  continue;
787 
789  size_expr.value(), postponed.expr.type());
790 
791  // only compare object part
792  bvt bv;
793  encode(number, bv);
794 
795  bv.erase(bv.begin(), bv.begin()+offset_bits);
796 
797  bvt saved_bv=postponed.op;
798  saved_bv.erase(saved_bv.begin(), saved_bv.begin()+offset_bits);
799 
800  bvt size_bv = convert_bv(object_size);
801 
802  POSTCONDITION(bv.size()==saved_bv.size());
803  PRECONDITION(postponed.bv.size()>=1);
804  PRECONDITION(size_bv.size() == postponed.bv.size());
805 
806  literalt l1=bv_utils.equal(bv, saved_bv);
807  literalt l2=bv_utils.equal(postponed.bv, size_bv);
808 
809  prop.l_set_to_true(prop.limplies(l1, l2));
810  }
811  }
812  else
813  UNREACHABLE;
814 }
815 
817 {
818  // post-processing arrays may yield further objects, do this first
820 
821  for(postponed_listt::const_iterator
822  it=postponed_list.begin();
823  it!=postponed_list.end();
824  it++)
825  do_postponed(*it);
826 
827  // Clear the list to avoid re-doing in case of incremental usage.
828  postponed_list.clear();
829 }
bv_pointerst::object_bits
unsigned object_bits
Definition: bv_pointers.h:33
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
pointer_logict::get_null_object
std::size_t get_null_object() const
Definition: pointer_logic.h:58
exception_utils.h
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
configt::bv_encodingt::object_bits
std::size_t object_bits
Definition: config.h:176
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2021
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:316
boolbvt::map
boolbv_mapt map
Definition: boolbv.h:104
typet::subtype
const typet & subtype() const
Definition: type.h:47
boolbvt::convert_member
virtual bvt convert_member(const member_exprt &expr)
Definition: boolbv_member.cpp:11
binary_exprt::rhs
exprt & rhs()
Definition: std_expr.h:641
boolbvt::convert_byte_update
virtual bvt convert_byte_update(const byte_update_exprt &expr)
Definition: boolbv_byte_update.cpp:20
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:305
bv_pointerst::postponedt::op
bvt op
Definition: bv_pointers.h:63
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
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:174
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:29
bvt
std::vector< literalt > bvt
Definition: literal.h:201
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:57
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3029
bv_pointerst::postponed_list
postponed_listt postponed_list
Definition: bv_pointers.h:68
bv_pointerst::postponedt::expr
exprt expr
Definition: bv_pointers.h:64
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
bv_pointerst::bv_pointerst
bv_pointerst(const namespacet &_ns, propt &_prop, message_handlert &message_handler)
Definition: bv_pointers.cpp:82
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
boolbvt::bv_get_rec
virtual exprt bv_get_rec(const exprt &expr, const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const
Definition: boolbv_get.cpp:71
string2integer
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
pointer_logict::add_object
std::size_t add_object(const exprt &expr)
Definition: pointer_logic.cpp:43
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:83
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:881
bv_pointerst::do_postponed
void do_postponed(const postponedt &postponed)
Definition: bv_pointers.cpp:736
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:283
exprt
Base class for all expressions.
Definition: expr.h:53
binary_exprt::lhs
exprt & lhs()
Definition: std_expr.h:631
propt::l_set_to_true
void l_set_to_true(literalt a)
Definition: prop.h:52
bv_pointerst::bv_get_rec
exprt bv_get_rec(const exprt &expr, const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const override
Definition: bv_pointers.cpp:594
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
bv_pointerst::convert_pointer_type
virtual bvt convert_pointer_type(const exprt &expr)
Definition: bv_pointers.cpp:218
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:207
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:965
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3001
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:4095
pointer_logict::pointert::object
std::size_t object
Definition: pointer_logic.h:30
to_shift_expr
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
Definition: std_expr.h:2543
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:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
pointer_logict::objects
hash_numbering< exprt, irep_hash > objects
Definition: pointer_logic.h:26
boolbvt::convert_byte_extract
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
Definition: boolbv_byte_extract.cpp:39
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:95
empty_typet
The empty type.
Definition: std_types.h:46
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:113
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:2823
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
member_exprt::compound
const exprt & compound() const
Definition: std_expr.h:3446
bv_utilst::representationt::SIGNED
@ SIGNED
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
to_byte_update_expr
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
Definition: byte_operators.h:127
pointer_logict::pointert::offset
mp_integer offset
Definition: pointer_logic.h:31
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
bv_utilst::representationt
representationt
Definition: bv_utils.h:31
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
arrayst::ns
const namespacet & ns
Definition: arrays.h:51
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:920
const_literal
literalt const_literal(bool value)
Definition: literal.h:188
boolbvt::post_process
void post_process() override
Definition: boolbv.h:67
index_exprt::index
exprt & index()
Definition: std_expr.h:1319
bv_pointerst::pointer_logic
pointer_logict pointer_logic
Definition: bv_pointers.h:28
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
unary_minus_exprt
The unary minus expression.
Definition: std_expr.h:378
index_exprt::array
exprt & array()
Definition: std_expr.h:1309
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
object_size
exprt object_size(const exprt &pointer)
Definition: pointer_predicates.cpp:32
bv_pointerst::bits
unsigned bits
Definition: bv_pointers.h:33
irept::id
const irep_idt & id() const
Definition: irep.h:418
message_handlert
Definition: message.h:28
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
boolbvt::convert_bv
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition: boolbv.cpp:119
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
bv_pointerst::encode
void encode(std::size_t object, bvt &bv)
Definition: bv_pointers.cpp:653
prop_conv_solvert::convert
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
Definition: prop_conv_solver.cpp:168
minus_exprt
Binary minus.
Definition: std_expr.h:940
config
configt config
Definition: config.cpp:24
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
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:1290
POSTCONDITION
#define POSTCONDITION(CONDITION)
Definition: invariant.h:480
bv_pointerst::offset_bits
unsigned offset_bits
Definition: bv_pointers.h:33
propt
TO_BE_DOCUMENTED.
Definition: prop.h:25
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:89
pointer_logict::is_dynamic_object
bool is_dynamic_object(const exprt &expr) const
Definition: pointer_logic.cpp:24
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2991
propt::l_get
virtual tvt l_get(literalt a) const =0
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
bv_pointerst::postponedt
Definition: bv_pointers.h:62
boolbvt::bv_utils
bv_utilst bv_utils
Definition: boolbv.h:98
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2047
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:2981
literalt
Definition: literal.h:26
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:64
boolbvt
Definition: boolbv.h:35
config.h
tvt::tv_enumt::TV_UNKNOWN
@ TV_UNKNOWN
size_of_expr
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:285
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3489
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:3419
exprt::operands
operandst & operands()
Definition: expr.h:95
index_exprt
Array index operator.
Definition: std_expr.h:1293
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2786
bv_utilst::equal
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1113
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
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:666
boolbvt::convert_rest
literalt convert_rest(const exprt &expr) override
Definition: boolbv.cpp:427
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
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:816
is_pointer_subtraction
static bool is_pointer_subtraction(const exprt &expr)
Definition: bv_pointers.cpp:460
tvt::tv_enumt::TV_FALSE
@ TV_FALSE
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:3914
member_offset
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
Definition: pointer_offset_size.cpp:23
c_types.h
bv_pointerst::add_addr
virtual void add_addr(const exprt &expr, bvt &bv)
Definition: bv_pointers.cpp:720
pointer_logict::pointert
Definition: pointer_logic.h:29
can_cast_type< bitvector_typet >
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
Definition: std_types.h:1064
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_solver.h:131
bv_pointerst::postponedt::bv
bvt bv
Definition: bv_pointers.h:63
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
Convert an (object,offset) pair to an expression.
Definition: pointer_logic.cpp:67
analysis_exceptiont
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
Definition: exception_utils.h:157
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939