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>
15 
17 {
18  if(expr.type().id()!=ID_bool)
19  throw "bv_pointerst::convert_rest got non-boolean operand";
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  if(expr.operands().size()!=2)
116  throw "index takes two operands";
117 
118  const index_exprt &index_expr=to_index_expr(expr);
119  const exprt &array=index_expr.array();
120  const exprt &index=index_expr.index();
121  const typet &array_type=ns.follow(array.type());
122 
123  // recursive call
124  if(array_type.id()==ID_pointer)
125  {
126  // this should be gone
127  bv=convert_pointer_type(array);
128  CHECK_RETURN(bv.size()==bits);
129  }
130  else if(array_type.id()==ID_array ||
131  array_type.id()==ID_incomplete_array ||
132  array_type.id()==ID_string_constant)
133  {
134  if(convert_address_of_rec(array, bv))
135  return true;
136  CHECK_RETURN(bv.size()==bits);
137  }
138  else
139  UNREACHABLE;
140 
141  // get size
142  mp_integer size=
143  pointer_offset_size(array_type.subtype(), ns);
144  DATA_INVARIANT(size>0, "array subtype expected to have non-zero size");
145 
146  offset_arithmetic(bv, size, index);
147  CHECK_RETURN(bv.size()==bits);
148  return false;
149  }
150  else if(expr.id()==ID_byte_extract_little_endian ||
151  expr.id()==ID_byte_extract_big_endian)
152  {
153  const auto &byte_extract_expr=to_byte_extract_expr(expr);
154 
155  // recursive call
156  if(convert_address_of_rec(byte_extract_expr.op(), bv))
157  return true;
158 
159  CHECK_RETURN(bv.size()==bits);
160 
161  offset_arithmetic(bv, 1, byte_extract_expr.offset());
162  CHECK_RETURN(bv.size()==bits);
163  return false;
164  }
165  else if(expr.id()==ID_member)
166  {
167  const member_exprt &member_expr=to_member_expr(expr);
168  const exprt &struct_op=member_expr.op0();
169  const typet &struct_op_type=ns.follow(struct_op.type());
170 
171  // recursive call
172  if(convert_address_of_rec(struct_op, bv))
173  return true;
174 
175  if(struct_op_type.id()==ID_struct)
176  {
177  mp_integer offset=member_offset(
178  to_struct_type(struct_op_type),
179  member_expr.get_component_name(), ns);
180  DATA_INVARIANT(offset>=0, "member offset expected to be positive");
181 
182  // add offset
183  offset_arithmetic(bv, offset);
184  }
185  else if(struct_op_type.id()==ID_union)
186  {
187  // nothing to do, all members have offset 0
188  }
189  else
190  throw "member takes struct or union operand";
191 
192  return false;
193  }
194  else if(expr.id()==ID_constant ||
195  expr.id()==ID_string_constant ||
196  expr.id()==ID_array)
197  { // constant
198  add_addr(expr, bv);
199  return false;
200  }
201  else if(expr.id()==ID_if)
202  {
203  const if_exprt &ifex=to_if_expr(expr);
204 
205  literalt cond=convert(ifex.cond());
206 
207  bvt bv1, bv2;
208 
209  if(convert_address_of_rec(ifex.true_case(), bv1))
210  return true;
211 
212  if(convert_address_of_rec(ifex.false_case(), bv2))
213  return true;
214 
215  bv=bv_utils.select(cond, bv1, bv2);
216 
217  return false;
218  }
219 
220  return true;
221 }
222 
224 {
225  if(expr.type().id()!=ID_pointer)
226  throw "convert_pointer_type got non-pointer type";
227 
228  // make sure the config hasn't been changed
230 
231  if(expr.id()==ID_symbol)
232  {
233  const irep_idt &identifier=to_symbol_expr(expr).get_identifier();
234  const typet &type=expr.type();
235 
236  bvt bv;
237  bv.resize(bits);
238 
239  map.get_literals(identifier, type, bits, bv);
240 
241  return bv;
242  }
243  else if(expr.id()==ID_nondet_symbol)
244  {
245  bvt bv;
246  bv.resize(bits);
247 
248  Forall_literals(it, bv)
249  *it=prop.new_variable();
250 
251  return bv;
252  }
253  else if(expr.id()==ID_typecast)
254  {
255  if(expr.operands().size()!=1)
256  throw "typecast takes one operand";
257 
258  const exprt &op=expr.op0();
259  const typet &op_type=ns.follow(op.type());
260 
261  if(op_type.id()==ID_pointer)
262  return convert_bv(op);
263  else if(op_type.id()==ID_signedbv ||
264  op_type.id()==ID_unsignedbv ||
265  op_type.id()==ID_bool ||
266  op_type.id()==ID_c_enum ||
267  op_type.id()==ID_c_enum_tag)
268  {
269  // Cast from integer to pointer.
270  // We just do a zero extension.
271 
272  const bvt &op_bv=convert_bv(op);
273 
274  return bv_utils.zero_extension(op_bv, bits);
275  }
276  }
277  else if(expr.id()==ID_if)
278  {
279  return SUB::convert_if(to_if_expr(expr));
280  }
281  else if(expr.id()==ID_index)
282  {
283  return SUB::convert_index(to_index_expr(expr));
284  }
285  else if(expr.id()==ID_member)
286  {
287  return SUB::convert_member(to_member_expr(expr));
288  }
289  else if(expr.id()==ID_address_of)
290  {
291  if(expr.operands().size()!=1)
292  throw expr.id_string()+" takes one operand";
293 
294  bvt bv;
295  bv.resize(bits);
296 
297  if(convert_address_of_rec(expr.op0(), bv))
298  {
299  conversion_failed(expr, bv);
300  return bv;
301  }
302 
303  CHECK_RETURN(bv.size()==bits);
304  return bv;
305  }
306  else if(expr.id()==ID_constant)
307  {
308  irep_idt value=to_constant_expr(expr).get_value();
309 
310  bvt bv;
311  bv.resize(bits);
312 
313  if(value==ID_NULL)
315  else
316  {
317  mp_integer i=string2integer(id2string(value), 2);
319  }
320 
321  return bv;
322  }
323  else if(expr.id()==ID_plus)
324  {
325  // this has to be pointer plus integer
326 
327  if(expr.operands().size()<2)
328  throw "operator + takes at least two operands";
329 
330  bvt bv;
331 
332  mp_integer size=0;
333  std::size_t count=0;
334 
335  forall_operands(it, expr)
336  {
337  if(it->type().id()==ID_pointer)
338  {
339  count++;
340  bv=convert_bv(*it);
341  CHECK_RETURN(bv.size()==bits);
342 
343  typet pointer_sub_type=it->type().subtype();
344 
345  if(pointer_sub_type.id()==ID_empty)
346  {
347  // This is a gcc extension.
348  // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
349  size = 1;
350  }
351  else
352  {
353  size = pointer_offset_size(pointer_sub_type, ns);
354  CHECK_RETURN(size > 0);
355  }
356  }
357  }
358 
359  if(count==0)
360  throw "found no pointer in pointer-type sum";
361  else if(count!=1)
362  throw "found more than one pointer in sum";
363 
365 
366  forall_operands(it, expr)
367  {
368  if(it->type().id()==ID_pointer)
369  continue;
370 
371  if(it->type().id()!=ID_unsignedbv &&
372  it->type().id()!=ID_signedbv)
373  {
374  bvt bv;
375  conversion_failed(expr, bv);
376  return bv;
377  }
378 
380  it->type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
382 
383  bvt op=convert_bv(*it);
384 
385  if(op.empty())
386  throw "unexpected pointer arithmetic operand width";
387 
388  // we cut any extra bits off
389 
390  if(op.size()>bits)
391  op.resize(bits);
392  else if(op.size()<bits)
393  op=bv_utils.extension(op, bits, rep);
394 
395  sum=bv_utils.add(sum, op);
396  }
397 
398  offset_arithmetic(bv, size, sum);
399 
400  return bv;
401  }
402  else if(expr.id()==ID_minus)
403  {
404  // this is pointer-integer
405 
406  if(expr.operands().size()!=2)
407  throw "operator "+expr.id_string()+" takes two operands";
408 
409  if(expr.op0().type().id()!=ID_pointer)
410  throw "found no pointer in pointer type in difference";
411 
412  bvt bv;
413 
414  if(expr.op1().type().id()!=ID_unsignedbv &&
415  expr.op1().type().id()!=ID_signedbv)
416  {
417  bvt bv;
418  conversion_failed(expr, bv);
419  return bv;
420  }
421 
422  const unary_minus_exprt neg_op1(expr.op1());
423 
424  bv=convert_bv(expr.op0());
425 
426  typet pointer_sub_type=expr.op0().type().subtype();
427  mp_integer element_size;
428 
429  if(pointer_sub_type.id()==ID_empty)
430  {
431  // This is a gcc extension.
432  // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
433  element_size = 1;
434  }
435  else
436  {
437  element_size = pointer_offset_size(pointer_sub_type, ns);
438  DATA_INVARIANT(element_size > 0, "object size expected to be positive");
439  }
440 
441  offset_arithmetic(bv, element_size, neg_op1);
442 
443  return bv;
444  }
445  else if(expr.id()==ID_lshr ||
446  expr.id()==ID_shl)
447  {
448  return SUB::convert_shift(to_shift_expr(expr));
449  }
450  else if(expr.id()==ID_bitand ||
451  expr.id()==ID_bitor ||
452  expr.id()==ID_bitnot)
453  {
454  return convert_bitwise(expr);
455  }
456  else if(expr.id()==ID_concatenation)
457  {
458  return SUB::convert_concatenation(expr);
459  }
460  else if(expr.id()==ID_byte_extract_little_endian ||
461  expr.id()==ID_byte_extract_big_endian)
462  {
464  }
465  else if(
466  expr.id() == ID_byte_update_little_endian ||
467  expr.id() == ID_byte_update_big_endian)
468  {
469  throw "byte-wise updates of pointers are unsupported";
470  }
471 
472  return conversion_failed(expr);
473 }
474 
476 {
477  if(expr.type().id()==ID_pointer)
478  return convert_pointer_type(expr);
479 
480  if(expr.id()==ID_minus &&
481  expr.operands().size()==2 &&
482  expr.op0().type().id()==ID_pointer &&
483  expr.op1().type().id()==ID_pointer)
484  {
485  // pointer minus pointer
486  bvt op0=convert_bv(expr.op0());
487  bvt op1=convert_bv(expr.op1());
488 
489  std::size_t width=boolbv_width(expr.type());
490 
491  if(width==0)
492  return conversion_failed(expr);
493 
494  // we do a zero extension
495  op0=bv_utils.zero_extension(op0, width);
496  op1=bv_utils.zero_extension(op1, width);
497 
498  bvt bv=bv_utils.sub(op0, op1);
499 
500  typet pointer_sub_type=expr.op0().type().subtype();
501  mp_integer element_size;
502 
503  if(pointer_sub_type.id()==ID_empty)
504  {
505  // This is a gcc extension.
506  // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
507  element_size = 1;
508  }
509  else
510  {
511  element_size = pointer_offset_size(pointer_sub_type, ns);
512  DATA_INVARIANT(element_size > 0, "object size expected to be positive");
513  }
514 
515  if(element_size!=1)
516  {
517  bvt element_size_bv=
518  bv_utils.build_constant(element_size, bv.size());
519  bv=bv_utils.divider(
520  bv, element_size_bv, bv_utilst::representationt::SIGNED);
521  }
522 
523  return bv;
524  }
525  else if(expr.id()==ID_pointer_offset &&
526  expr.operands().size()==1 &&
527  expr.op0().type().id()==ID_pointer)
528  {
529  bvt op0=convert_bv(expr.op0());
530 
531  std::size_t width=boolbv_width(expr.type());
532 
533  if(width==0)
534  return conversion_failed(expr);
535 
536  // we need to strip off the object part
537  op0.resize(offset_bits);
538 
539  // we do a sign extension to permit negative offsets
540  return bv_utils.sign_extension(op0, width);
541  }
542  else if(expr.id()==ID_object_size &&
543  expr.operands().size()==1 &&
544  expr.op0().type().id()==ID_pointer)
545  {
546  // we postpone until we know the objects
547  std::size_t width=boolbv_width(expr.type());
548 
549  bvt bv;
550  bv.resize(width);
551 
552  for(std::size_t i=0; i<width; i++)
553  bv[i]=prop.new_variable();
554 
555  postponed_list.push_back(postponedt());
556 
557  postponed_list.back().op=convert_bv(expr.op0());
558  postponed_list.back().bv=bv;
559  postponed_list.back().expr=expr;
560 
561  return bv;
562  }
563  else if(expr.id()==ID_pointer_object &&
564  expr.operands().size()==1 &&
565  expr.op0().type().id()==ID_pointer)
566  {
567  bvt op0=convert_bv(expr.op0());
568 
569  std::size_t width=boolbv_width(expr.type());
570 
571  if(width==0)
572  return conversion_failed(expr);
573 
574  // erase offset bits
575 
576  op0.erase(op0.begin()+0, op0.begin()+offset_bits);
577 
578  return bv_utils.zero_extension(op0, width);
579  }
580  else if(expr.id()==ID_typecast &&
581  expr.operands().size()==1 &&
582  expr.op0().type().id()==ID_pointer)
583  {
584  // pointer to int
585  bvt op0=convert_pointer_type(expr.op0());
586 
587  // squeeze it in!
588 
589  std::size_t width=boolbv_width(expr.type());
590 
591  if(width==0)
592  return conversion_failed(expr);
593 
594  return bv_utils.zero_extension(op0, width);
595  }
596 
597  return SUB::convert_bitvector(expr);
598 }
599 
601  const bvt &bv,
602  const std::vector<bool> &unknown,
603  std::size_t offset,
604  const typet &type) const
605 {
606  if(type.id()!=ID_pointer)
607  return SUB::bv_get_rec(bv, unknown, offset, type);
608 
609  std::string value_addr, value_offset, value;
610 
611  for(std::size_t i=0; i<bits; i++)
612  {
613  char ch=0;
614  std::size_t bit_nr=i+offset;
615 
616  if(unknown[bit_nr])
617  ch='0';
618  else
619  {
620  switch(prop.l_get(bv[bit_nr]).get_value())
621  {
622  case tvt::tv_enumt::TV_FALSE: ch='0'; break;
623  case tvt::tv_enumt::TV_TRUE: ch='1'; break;
624  case tvt::tv_enumt::TV_UNKNOWN: ch='0'; break;
625  default: UNREACHABLE;
626  }
627  }
628 
629  value=ch+value;
630 
631  if(i<offset_bits)
632  value_offset=ch+value_offset;
633  else
634  value_addr=ch+value_addr;
635  }
636 
637  // we treat these like bit-vector constants, but with
638  // some additional annotation
639 
640  constant_exprt result(type);
641  result.set_value(value);
642 
643  pointer_logict::pointert pointer;
644  pointer.object=integer2size_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 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  if(a==max_objects)
727  throw
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  "use the `--object-bits n` option to increase the maximum number";
731 
732  encode(a, bv);
733 }
734 
736  const postponedt &postponed)
737 {
738  if(postponed.expr.id()==ID_dynamic_object)
739  {
740  const pointer_logict::objectst &objects=
742 
743  std::size_t number=0;
744 
746  it=objects.begin();
747  it!=objects.end();
748  it++, number++)
749  {
750  const exprt &expr=*it;
751 
752  bool is_dynamic=pointer_logic.is_dynamic_object(expr);
753 
754  // only compare object part
755  bvt bv;
756  encode(number, bv);
757 
758  bv.erase(bv.begin(), bv.begin()+offset_bits);
759 
760  bvt saved_bv=postponed.op;
761  saved_bv.erase(saved_bv.begin(), saved_bv.begin()+offset_bits);
762 
763  POSTCONDITION(bv.size()==saved_bv.size());
764  PRECONDITION(postponed.bv.size()==1);
765 
766  literalt l1=bv_utils.equal(bv, saved_bv);
767  literalt l2=postponed.bv.front();
768 
769  if(!is_dynamic)
770  l2=!l2;
771 
772  prop.l_set_to(prop.limplies(l1, l2), true);
773  }
774  }
775  else if(postponed.expr.id()==ID_object_size)
776  {
777  const pointer_logict::objectst &objects=
779 
780  std::size_t number=0;
781 
783  it=objects.begin();
784  it!=objects.end();
785  it++, number++)
786  {
787  const exprt &expr=*it;
788 
790 
791  if(expr.id()==ID_symbol)
792  {
793  // just get the type
794  const typet &type=ns.follow(expr.type());
795 
796  exprt size_expr=size_of_expr(type, ns);
797 
798  if(size_expr.is_nil())
799  continue;
800 
801  if(to_integer(size_expr, object_size))
802  continue;
803  }
804  else
805  continue;
806 
807  // only compare object part
808  bvt bv;
809  encode(number, bv);
810 
811  bv.erase(bv.begin(), bv.begin()+offset_bits);
812 
813  bvt saved_bv=postponed.op;
814  saved_bv.erase(saved_bv.begin(), saved_bv.begin()+offset_bits);
815 
816  POSTCONDITION(bv.size()==saved_bv.size());
817  PRECONDITION(postponed.bv.size()>=1);
818 
819  literalt l1=bv_utils.equal(bv, saved_bv);
820 
821  bvt size_bv=bv_utils.build_constant(object_size, postponed.bv.size());
822  literalt l2=bv_utils.equal(postponed.bv, size_bv);
823 
824  prop.l_set_to(prop.limplies(l1, l2), true);
825  }
826  }
827  else
828  UNREACHABLE;
829 }
830 
832 {
833  // post-processing arrays may yield further objects, do this first
835 
836  for(postponed_listt::const_iterator
837  it=postponed_list.begin();
838  it!=postponed_list.end();
839  it++)
840  do_postponed(*it);
841 
842  // Clear the list to avoid re-doing in case of incremental usage.
843  postponed_list.clear();
844 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3424
The type of an expression.
Definition: type.h:22
exprt size_of_expr(const typet &type, const namespacet &ns)
std::size_t get_null_object() const
Definition: pointer_logic.h:59
virtual bvt convert_concatenation(const exprt &expr)
exprt & true_case()
Definition: std_expr.h:3393
typet void_type()
Definition: c_types.cpp:253
bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
Definition: bv_utils.cpp:109
bv_utilst bv_utils
Definition: boolbv.h:93
BigInt mp_integer
Definition: mp_arith.h:22
bool is_nil() const
Definition: irep.h:172
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:162
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
exprt & op0()
Definition: expr.h:72
virtual bvt convert_shift(const binary_exprt &expr)
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.h:87
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1108
literalt convert_rest(const exprt &expr) override
Definition: bv_pointers.cpp:16
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
boolbv_widtht boolbv_width
Definition: boolbv.h:90
const irep_idt & get_identifier() const
Definition: std_expr.h:128
bvt convert_bitvector(const exprt &expr) override
Converts an expression into its gate-level representation and returns a vector of literals correspond...
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
const irep_idt & get_value() const
Definition: std_expr.h:4439
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
representationt
Definition: bv_utils.h:31
The trinary if-then-else operator.
Definition: std_expr.h:3359
exprt & cond()
Definition: std_expr.h:3383
bvt sub(const bvt &op0, const bvt &op1)
Definition: bv_utils.h:65
typet & type()
Definition: expr.h:56
A constant literal expression.
Definition: std_expr.h:4422
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:266
void post_process() override
Definition: boolbv.h:60
configt config
Definition: config.cpp:23
#define POSTCONDITION(CONDITION)
Definition: invariant.h:254
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
virtual literalt limplies(literalt a, literalt b)=0
Definition: boolbv.h:31
std::size_t get_invalid_object() const
Definition: pointer_logic.h:65
Extract member of struct or union.
Definition: std_expr.h:3869
struct configt::bv_encodingt bv_encoding
virtual literalt land(literalt a, literalt b)=0
exprt object_size(const exprt &pointer)
const irep_idt & id() const
Definition: irep.h:259
virtual literalt new_variable()=0
#define Forall_literals(it, bv)
Definition: literal.h:206
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
virtual void l_set_to(literalt a, bool value)
Definition: prop.h:44
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
Definition: bv_utils.cpp:1281
unsigned offset_bits
Definition: bv_pointers.h:30
iterator begin()
Definition: numbering.h:85
std::size_t object_bits
Definition: config.h:164
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:163
virtual void add_addr(const exprt &expr, bvt &bv)
pointer_logict pointer_logic
Definition: bv_pointers.h:25
exprt & op1()
Definition: expr.h:75
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
unsigned object_bits
Definition: bv_pointers.h:30
TO_BE_DOCUMENTED.
Definition: namespace.h:74
bool is_dynamic_object(const exprt &expr) const
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3953
#define forall_operands(it, expr)
Definition: expr.h:17
const namespacet & ns
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
bvt unsigned_multiplier(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:633
const typet & follow(const typet &) const
Definition: namespace.cpp:55
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
Definition: bv_utils.cpp:96
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
The unary minus expression.
Definition: std_expr.h:444
exprt & false_case()
Definition: std_expr.h:3403
literalt convert_rest(const exprt &expr) override
Definition: boolbv.cpp:434
TO_BE_DOCUMENTED.
Definition: prop.h:24
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:4463
bvt zero_extension(const bvt &bv, std::size_t new_size)
Definition: bv_utils.h:184
bv_pointerst(const namespacet &_ns, propt &_prop)
Definition: bv_pointers.cpp:82
exprt pointer_expr(const pointert &pointer, const pointer_typet &type) const
typename data_typet::const_iterator const_iterator
Definition: numbering.h:35
postponed_listt postponed_list
Definition: bv_pointers.h:64
std::vector< exprt > operandst
Definition: expr.h:45
Pointer Logic.
virtual literalt lequal(literalt a, literalt b)=0
objectst objects
Definition: pointer_logic.h:27
literalt const_literal(bool value)
Definition: literal.h:187
void post_process() override
bvt add(const bvt &op0, const bvt &op1)
Definition: bv_utils.h:64
void encode(std::size_t object, bvt &bv)
const shift_exprt & to_shift_expr(const exprt &expr)
Cast a generic exprt to a shift_exprt.
Definition: std_expr.h:2818
mstreamt & result() const
Definition: message.h:312
exprt & index()
Definition: std_expr.h:1496
exprt bv_get_rec(const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const override
Base class for all expressions.
Definition: expr.h:42
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
void do_postponed(const postponedt &postponed)
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
virtual bvt convert_pointer_type(const exprt &expr)
std::string to_string(const string_constraintt &expr)
Used for debug printing.
irep_idt get_component_name() const
Definition: std_expr.h:3893
virtual tvt l_get(literalt a) const =0
#define UNREACHABLE
Definition: invariant.h:271
virtual bvt convert_member(const member_exprt &expr)
virtual bvt convert_if(const if_exprt &expr)
Definition: boolbv_if.cpp:12
const std::string & id_string() const
Definition: irep.h:262
bool convert_address_of_rec(const exprt &expr, bvt &bv)
Definition: bv_pointers.cpp:94
unsigned bits
Definition: bv_pointers.h:30
tv_enumt get_value() const
Definition: threeval.h:40
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
bvt sign_extension(const bvt &bv, std::size_t new_size)
Definition: bv_utils.h:179
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1459
void get_literals(const irep_idt &identifier, const typet &type, const std::size_t width, bvt &literals)
Definition: boolbv_map.cpp:84
boolbv_mapt map
Definition: boolbv.h:99
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
iterator end()
Definition: numbering.h:98
const typet & subtype() const
Definition: type.h:33
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
operandst & operands()
Definition: expr.h:66
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
std::size_t add_object(const exprt &expr)
exprt & array()
Definition: std_expr.h:1486
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
std::vector< literalt > bvt
Definition: literal.h:200
bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:15
void offset_arithmetic(bvt &bv, const mp_integer &x)
virtual bvt convert_bitwise(const exprt &expr)
array index operator
Definition: std_expr.h:1462