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, null_bv;
35 
36  bvt equal_invalid_bv, equal_null_bv;
37  equal_invalid_bv.resize(object_bits);
38  equal_null_bv.resize(object_bits);
39 
40  for(std::size_t i=0; i<object_bits; i++)
41  {
42  equal_invalid_bv[i]=prop.lequal(bv[offset_bits+i],
43  invalid_bv[offset_bits+i]);
44  equal_null_bv[i] =prop.lequal(bv[offset_bits+i],
45  null_bv[offset_bits+i]);
46  }
47 
48  literalt equal_invalid=prop.land(equal_invalid_bv);
49  literalt equal_null=prop.land(equal_null_bv);
50 
51  return prop.lor(equal_invalid, equal_null);
52  }
53  }
54  }
55  else if(expr.id()==ID_dynamic_object)
56  {
57  if(operands.size()==1 &&
58  operands[0].type().id()==ID_pointer)
59  {
60  // we postpone
62 
63  postponed_list.push_back(postponedt());
64  postponed_list.back().op=convert_bv(operands[0]);
65  postponed_list.back().bv.push_back(l);
66  postponed_list.back().expr=expr;
67 
68  return l;
69  }
70  }
71  else if(expr.id()==ID_lt || expr.id()==ID_le ||
72  expr.id()==ID_gt || expr.id()==ID_ge)
73  {
74  if(operands.size()==2 &&
75  operands[0].type().id()==ID_pointer &&
76  operands[1].type().id()==ID_pointer)
77  {
78  const bvt &bv0=convert_bv(operands[0]);
79  const bvt &bv1=convert_bv(operands[1]);
80 
81  return bv_utils.rel(
82  bv0, expr.id(), bv1, bv_utilst::representationt::UNSIGNED);
83  }
84  }
85 
86  return SUB::convert_rest(expr);
87 }
88 
90  const namespacet &_ns,
91  propt &_prop):
92  boolbvt(_ns, _prop),
93  pointer_logic(_ns)
94 {
96  std::size_t pointer_width=boolbv_width(pointer_type(void_type()));
97  offset_bits=pointer_width-object_bits;
98  bits=pointer_width;
99 }
100 
102  const exprt &expr,
103  bvt &bv)
104 {
105  if(expr.id()==ID_symbol)
106  {
107  add_addr(expr, bv);
108  return false;
109  }
110  else if(expr.id()==ID_label)
111  {
112  add_addr(expr, bv);
113  return false;
114  }
115  else if(expr.id() == ID_null_object)
116  {
118  return false;
119  }
120  else if(expr.id()==ID_index)
121  {
122  if(expr.operands().size()!=2)
123  throw "index takes two operands";
124 
125  const index_exprt &index_expr=to_index_expr(expr);
126  const exprt &array=index_expr.array();
127  const exprt &index=index_expr.index();
128  const typet &array_type=ns.follow(array.type());
129 
130  // recursive call
131  if(array_type.id()==ID_pointer)
132  {
133  // this should be gone
134  bv=convert_pointer_type(array);
135  CHECK_RETURN(bv.size()==bits);
136  }
137  else if(array_type.id()==ID_array ||
138  array_type.id()==ID_incomplete_array ||
139  array_type.id()==ID_string_constant)
140  {
141  if(convert_address_of_rec(array, bv))
142  return true;
143  CHECK_RETURN(bv.size()==bits);
144  }
145  else
146  UNREACHABLE;
147 
148  // get size
149  mp_integer size=
150  pointer_offset_size(array_type.subtype(), ns);
151  DATA_INVARIANT(size>0, "array subtype expected to have non-zero size");
152 
153  offset_arithmetic(bv, size, index);
154  CHECK_RETURN(bv.size()==bits);
155  return false;
156  }
157  else if(expr.id()==ID_byte_extract_little_endian ||
158  expr.id()==ID_byte_extract_big_endian)
159  {
160  const auto &byte_extract_expr=to_byte_extract_expr(expr);
161 
162  // recursive call
163  if(convert_address_of_rec(byte_extract_expr.op(), bv))
164  return true;
165 
166  CHECK_RETURN(bv.size()==bits);
167 
168  offset_arithmetic(bv, 1, byte_extract_expr.offset());
169  CHECK_RETURN(bv.size()==bits);
170  return false;
171  }
172  else if(expr.id()==ID_member)
173  {
174  const member_exprt &member_expr=to_member_expr(expr);
175  const exprt &struct_op=member_expr.op0();
176  const typet &struct_op_type=ns.follow(struct_op.type());
177 
178  // recursive call
179  if(convert_address_of_rec(struct_op, bv))
180  return true;
181 
182  if(struct_op_type.id()==ID_struct)
183  {
184  mp_integer offset=member_offset(
185  to_struct_type(struct_op_type),
186  member_expr.get_component_name(), ns);
187  DATA_INVARIANT(offset>=0, "member offset expected to be positive");
188 
189  // add offset
190  offset_arithmetic(bv, offset);
191  }
192  else if(struct_op_type.id()==ID_union)
193  {
194  // nothing to do, all members have offset 0
195  }
196  else
197  throw "member takes struct or union operand";
198 
199  return false;
200  }
201  else if(expr.id()==ID_constant ||
202  expr.id()==ID_string_constant ||
203  expr.id()==ID_array)
204  { // constant
205  add_addr(expr, bv);
206  return false;
207  }
208  else if(expr.id()==ID_if)
209  {
210  const if_exprt &ifex=to_if_expr(expr);
211 
212  literalt cond=convert(ifex.cond());
213 
214  bvt bv1, bv2;
215 
216  if(convert_address_of_rec(ifex.true_case(), bv1))
217  return true;
218 
219  if(convert_address_of_rec(ifex.false_case(), bv2))
220  return true;
221 
222  bv=bv_utils.select(cond, bv1, bv2);
223 
224  return false;
225  }
226 
227  return true;
228 }
229 
231 {
232  if(expr.type().id()!=ID_pointer)
233  throw "convert_pointer_type got non-pointer type";
234 
235  // make sure the config hasn't been changed
237 
238  if(expr.id()==ID_symbol)
239  {
240  const irep_idt &identifier=to_symbol_expr(expr).get_identifier();
241  const typet &type=expr.type();
242 
243  bvt bv;
244  bv.resize(bits);
245 
246  map.get_literals(identifier, type, bits, bv);
247 
248  return bv;
249  }
250  else if(expr.id()==ID_nondet_symbol)
251  {
252  bvt bv;
253  bv.resize(bits);
254 
255  Forall_literals(it, bv)
256  *it=prop.new_variable();
257 
258  return bv;
259  }
260  else if(expr.id()==ID_typecast)
261  {
262  if(expr.operands().size()!=1)
263  throw "typecast takes one operand";
264 
265  const exprt &op=expr.op0();
266  const typet &op_type=ns.follow(op.type());
267 
268  if(op_type.id()==ID_pointer)
269  return convert_bv(op);
270  else if(op_type.id()==ID_signedbv ||
271  op_type.id()==ID_unsignedbv ||
272  op_type.id()==ID_bool ||
273  op_type.id()==ID_c_enum ||
274  op_type.id()==ID_c_enum_tag)
275  {
276  // Cast from integer to pointer.
277  // We just do a zero extension.
278 
279  const bvt &op_bv=convert_bv(op);
280 
281  return bv_utils.zero_extension(op_bv, bits);
282  }
283  }
284  else if(expr.id()==ID_if)
285  {
286  return SUB::convert_if(to_if_expr(expr));
287  }
288  else if(expr.id()==ID_index)
289  {
290  return SUB::convert_index(to_index_expr(expr));
291  }
292  else if(expr.id()==ID_member)
293  {
294  return SUB::convert_member(to_member_expr(expr));
295  }
296  else if(expr.id()==ID_address_of)
297  {
298  if(expr.operands().size()!=1)
299  throw expr.id_string()+" takes one operand";
300 
301  bvt bv;
302  bv.resize(bits);
303 
304  if(convert_address_of_rec(expr.op0(), bv))
305  {
306  conversion_failed(expr, bv);
307  return bv;
308  }
309 
310  CHECK_RETURN(bv.size()==bits);
311  return bv;
312  }
313  else if(expr.id()==ID_constant)
314  {
315  irep_idt value=to_constant_expr(expr).get_value();
316 
317  bvt bv;
318  bv.resize(bits);
319 
320  if(value==ID_NULL)
322  else
323  {
324  mp_integer i=string2integer(id2string(value), 2);
326  }
327 
328  return bv;
329  }
330  else if(expr.id()==ID_plus)
331  {
332  // this has to be pointer plus integer
333 
334  if(expr.operands().size()<2)
335  throw "operator + takes at least two operands";
336 
337  bvt bv;
338 
339  mp_integer size=0;
340  std::size_t count=0;
341 
342  forall_operands(it, expr)
343  {
344  if(it->type().id()==ID_pointer)
345  {
346  count++;
347  bv=convert_bv(*it);
348  CHECK_RETURN(bv.size()==bits);
349 
350  typet pointer_sub_type=it->type().subtype();
351 
352  if(pointer_sub_type.id()==ID_empty)
353  {
354  // This is a gcc extension.
355  // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
356  size = 1;
357  }
358  else
359  {
360  size = pointer_offset_size(pointer_sub_type, ns);
361  CHECK_RETURN(size > 0);
362  }
363  }
364  }
365 
366  if(count==0)
367  throw "found no pointer in pointer-type sum";
368  else if(count!=1)
369  throw "found more than one pointer in sum";
370 
372 
373  forall_operands(it, expr)
374  {
375  if(it->type().id()==ID_pointer)
376  continue;
377 
378  if(it->type().id()!=ID_unsignedbv &&
379  it->type().id()!=ID_signedbv)
380  {
381  bvt bv;
382  conversion_failed(expr, bv);
383  return bv;
384  }
385 
387  it->type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
389 
390  bvt op=convert_bv(*it);
391 
392  if(op.empty())
393  throw "unexpected pointer arithmetic operand width";
394 
395  // we cut any extra bits off
396 
397  if(op.size()>bits)
398  op.resize(bits);
399  else if(op.size()<bits)
400  op=bv_utils.extension(op, bits, rep);
401 
402  sum=bv_utils.add(sum, op);
403  }
404 
405  offset_arithmetic(bv, size, sum);
406 
407  return bv;
408  }
409  else if(expr.id()==ID_minus)
410  {
411  // this is pointer-integer
412 
413  if(expr.operands().size()!=2)
414  throw "operator "+expr.id_string()+" takes two operands";
415 
416  if(expr.op0().type().id()!=ID_pointer)
417  throw "found no pointer in pointer type in difference";
418 
419  bvt bv;
420 
421  if(expr.op1().type().id()!=ID_unsignedbv &&
422  expr.op1().type().id()!=ID_signedbv)
423  {
424  bvt bv;
425  conversion_failed(expr, bv);
426  return bv;
427  }
428 
429  const unary_minus_exprt neg_op1(expr.op1());
430 
431  bv=convert_bv(expr.op0());
432 
433  typet pointer_sub_type=expr.op0().type().subtype();
434  mp_integer element_size;
435 
436  if(pointer_sub_type.id()==ID_empty)
437  {
438  // This is a gcc extension.
439  // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
440  element_size = 1;
441  }
442  else
443  {
444  element_size = pointer_offset_size(pointer_sub_type, ns);
445  DATA_INVARIANT(element_size > 0, "object size expected to be positive");
446  }
447 
448  offset_arithmetic(bv, element_size, neg_op1);
449 
450  return bv;
451  }
452  else if(expr.id()==ID_lshr ||
453  expr.id()==ID_shl)
454  {
455  return SUB::convert_shift(to_shift_expr(expr));
456  }
457  else if(expr.id()==ID_bitand ||
458  expr.id()==ID_bitor ||
459  expr.id()==ID_bitnot)
460  {
461  return convert_bitwise(expr);
462  }
463  else if(expr.id()==ID_concatenation)
464  {
465  return SUB::convert_concatenation(expr);
466  }
467  else if(expr.id()==ID_byte_extract_little_endian ||
468  expr.id()==ID_byte_extract_big_endian)
469  {
471  }
472  else if(
473  expr.id() == ID_byte_update_little_endian ||
474  expr.id() == ID_byte_update_big_endian)
475  {
476  throw "byte-wise updates of pointers are unsupported";
477  }
478 
479  return conversion_failed(expr);
480 }
481 
483 {
484  if(expr.type().id()==ID_pointer)
485  return convert_pointer_type(expr);
486 
487  if(expr.id()==ID_minus &&
488  expr.operands().size()==2 &&
489  expr.op0().type().id()==ID_pointer &&
490  expr.op1().type().id()==ID_pointer)
491  {
492  // pointer minus pointer
493  bvt op0=convert_bv(expr.op0());
494  bvt op1=convert_bv(expr.op1());
495 
496  std::size_t width=boolbv_width(expr.type());
497 
498  if(width==0)
499  return conversion_failed(expr);
500 
501  // we do a zero extension
502  op0=bv_utils.zero_extension(op0, width);
503  op1=bv_utils.zero_extension(op1, width);
504 
505  bvt bv=bv_utils.sub(op0, op1);
506 
507  typet pointer_sub_type=expr.op0().type().subtype();
508  mp_integer element_size;
509 
510  if(pointer_sub_type.id()==ID_empty)
511  {
512  // This is a gcc extension.
513  // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
514  element_size = 1;
515  }
516  else
517  {
518  element_size = pointer_offset_size(pointer_sub_type, ns);
519  DATA_INVARIANT(element_size > 0, "object size expected to be positive");
520  }
521 
522  if(element_size!=1)
523  {
524  bvt element_size_bv=
525  bv_utils.build_constant(element_size, bv.size());
526  bv=bv_utils.divider(
527  bv, element_size_bv, bv_utilst::representationt::SIGNED);
528  }
529 
530  return bv;
531  }
532  else if(expr.id()==ID_pointer_offset &&
533  expr.operands().size()==1 &&
534  expr.op0().type().id()==ID_pointer)
535  {
536  bvt op0=convert_bv(expr.op0());
537 
538  std::size_t width=boolbv_width(expr.type());
539 
540  if(width==0)
541  return conversion_failed(expr);
542 
543  // we need to strip off the object part
544  op0.resize(offset_bits);
545 
546  // we do a sign extension to permit negative offsets
547  return bv_utils.sign_extension(op0, width);
548  }
549  else if(expr.id()==ID_object_size &&
550  expr.operands().size()==1 &&
551  expr.op0().type().id()==ID_pointer)
552  {
553  // we postpone until we know the objects
554  std::size_t width=boolbv_width(expr.type());
555 
556  bvt bv;
557  bv.resize(width);
558 
559  for(std::size_t i=0; i<width; i++)
560  bv[i]=prop.new_variable();
561 
562  postponed_list.push_back(postponedt());
563 
564  postponed_list.back().op=convert_bv(expr.op0());
565  postponed_list.back().bv=bv;
566  postponed_list.back().expr=expr;
567 
568  return bv;
569  }
570  else if(expr.id()==ID_pointer_object &&
571  expr.operands().size()==1 &&
572  expr.op0().type().id()==ID_pointer)
573  {
574  bvt op0=convert_bv(expr.op0());
575 
576  std::size_t width=boolbv_width(expr.type());
577 
578  if(width==0)
579  return conversion_failed(expr);
580 
581  // erase offset bits
582 
583  op0.erase(op0.begin()+0, op0.begin()+offset_bits);
584 
585  return bv_utils.zero_extension(op0, width);
586  }
587  else if(expr.id()==ID_typecast &&
588  expr.operands().size()==1 &&
589  expr.op0().type().id()==ID_pointer)
590  {
591  // pointer to int
592  bvt op0=convert_pointer_type(expr.op0());
593 
594  // squeeze it in!
595 
596  std::size_t width=boolbv_width(expr.type());
597 
598  if(width==0)
599  return conversion_failed(expr);
600 
601  return bv_utils.zero_extension(op0, width);
602  }
603 
604  return SUB::convert_bitvector(expr);
605 }
606 
608  const bvt &bv,
609  const std::vector<bool> &unknown,
610  std::size_t offset,
611  const typet &type) const
612 {
613  if(type.id()!=ID_pointer)
614  return SUB::bv_get_rec(bv, unknown, offset, type);
615 
616  std::string value_addr, value_offset, value;
617 
618  for(std::size_t i=0; i<bits; i++)
619  {
620  char ch=0;
621  std::size_t bit_nr=i+offset;
622 
623  if(unknown[bit_nr])
624  ch='0';
625  else
626  {
627  switch(prop.l_get(bv[bit_nr]).get_value())
628  {
629  case tvt::tv_enumt::TV_FALSE: ch='0'; break;
630  case tvt::tv_enumt::TV_TRUE: ch='1'; break;
631  case tvt::tv_enumt::TV_UNKNOWN: ch='0'; break;
632  default: UNREACHABLE;
633  }
634  }
635 
636  value=ch+value;
637 
638  if(i<offset_bits)
639  value_offset=ch+value_offset;
640  else
641  value_addr=ch+value_addr;
642  }
643 
644  // we treat these like bit-vector constants, but with
645  // some additional annotation
646 
647  constant_exprt result(type);
648  result.set_value(value);
649 
650  pointer_logict::pointert pointer;
651  pointer.object=integer2size_t(binary2integer(value_addr, false));
652  pointer.offset=binary2integer(value_offset, true);
653 
654  // we add the elaborated expression as operand
655  result.copy_to_operands(
656  pointer_logic.pointer_expr(pointer, to_pointer_type(type)));
657 
658  return result;
659 }
660 
661 void bv_pointerst::encode(std::size_t addr, bvt &bv)
662 {
663  bv.resize(bits);
664 
665  // set offset to zero
666  for(std::size_t i=0; i<offset_bits; i++)
667  bv[i]=const_literal(false);
668 
669  // set variable part
670  for(std::size_t i=0; i<object_bits; i++)
671  bv[offset_bits+i]=const_literal((addr&(std::size_t(1)<<i))!=0);
672 }
673 
675 {
676  bvt bv1=bv;
677  bv1.resize(offset_bits); // strip down
678 
680 
681  bvt tmp=bv_utils.add(bv1, bv2);
682 
683  // copy offset bits
684  for(std::size_t i=0; i<offset_bits; i++)
685  bv[i]=tmp[i];
686 }
687 
689  bvt &bv,
690  const mp_integer &factor,
691  const exprt &index)
692 {
693  bvt bv_index=convert_bv(index);
694 
696  index.type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
698 
699  bv_index=bv_utils.extension(bv_index, offset_bits, rep);
700 
701  offset_arithmetic(bv, factor, bv_index);
702 }
703 
705  bvt &bv,
706  const mp_integer &factor,
707  const bvt &index)
708 {
709  bvt bv_index;
710 
711  if(factor==1)
712  bv_index=index;
713  else
714  {
715  bvt bv_factor=bv_utils.build_constant(factor, index.size());
716  bv_index=bv_utils.unsigned_multiplier(index, bv_factor);
717  }
718 
719  bv_index=bv_utils.zero_extension(bv_index, bv.size());
720 
721  bvt bv_tmp=bv_utils.add(bv, bv_index);
722 
723  // copy lower parts of result
724  for(std::size_t i=0; i<offset_bits; i++)
725  bv[i]=bv_tmp[i];
726 }
727 
728 void bv_pointerst::add_addr(const exprt &expr, bvt &bv)
729 {
730  std::size_t a=pointer_logic.add_object(expr);
731 
732  const std::size_t max_objects=std::size_t(1)<<object_bits;
733  if(a==max_objects)
734  throw
735  "too many addressed objects: maximum number of objects is set to 2^n="+
736  std::to_string(max_objects)+" (with n="+std::to_string(object_bits)+"); "+
737  "use the `--object-bits n` option to increase the maximum number";
738 
739  encode(a, bv);
740 }
741 
743  const postponedt &postponed)
744 {
745  if(postponed.expr.id()==ID_dynamic_object)
746  {
747  const pointer_logict::objectst &objects=
749 
750  std::size_t number=0;
751 
753  it=objects.begin();
754  it!=objects.end();
755  it++, number++)
756  {
757  const exprt &expr=*it;
758 
759  bool is_dynamic=pointer_logic.is_dynamic_object(expr);
760 
761  // only compare object part
762  bvt bv;
763  encode(number, bv);
764 
765  bv.erase(bv.begin(), bv.begin()+offset_bits);
766 
767  bvt saved_bv=postponed.op;
768  saved_bv.erase(saved_bv.begin(), saved_bv.begin()+offset_bits);
769 
770  POSTCONDITION(bv.size()==saved_bv.size());
771  PRECONDITION(postponed.bv.size()==1);
772 
773  literalt l1=bv_utils.equal(bv, saved_bv);
774  literalt l2=postponed.bv.front();
775 
776  if(!is_dynamic)
777  l2=!l2;
778 
779  prop.l_set_to(prop.limplies(l1, l2), true);
780  }
781  }
782  else if(postponed.expr.id()==ID_object_size)
783  {
784  const pointer_logict::objectst &objects=
786 
787  std::size_t number=0;
788 
790  it=objects.begin();
791  it!=objects.end();
792  it++, number++)
793  {
794  const exprt &expr=*it;
795 
797 
798  if(expr.id()==ID_symbol)
799  {
800  // just get the type
801  const typet &type=ns.follow(expr.type());
802 
803  exprt size_expr=size_of_expr(type, ns);
804 
805  if(size_expr.is_nil())
806  continue;
807 
808  if(to_integer(size_expr, object_size))
809  continue;
810  }
811  else
812  continue;
813 
814  // only compare object part
815  bvt bv;
816  encode(number, bv);
817 
818  bv.erase(bv.begin(), bv.begin()+offset_bits);
819 
820  bvt saved_bv=postponed.op;
821  saved_bv.erase(saved_bv.begin(), saved_bv.begin()+offset_bits);
822 
823  POSTCONDITION(bv.size()==saved_bv.size());
824  PRECONDITION(postponed.bv.size()>=1);
825 
826  literalt l1=bv_utils.equal(bv, saved_bv);
827 
828  bvt size_bv=bv_utils.build_constant(object_size, postponed.bv.size());
829  literalt l2=bv_utils.equal(postponed.bv, size_bv);
830 
831  prop.l_set_to(prop.limplies(l1, l2), true);
832  }
833  }
834  else
835  UNREACHABLE;
836 }
837 
839 {
840  // post-processing arrays may yield further objects, do this first
842 
843  for(postponed_listt::const_iterator
844  it=postponed_list.begin();
845  it!=postponed_list.end();
846  it++)
847  do_postponed(*it);
848 
849  // Clear the list to avoid re-doing in case of incremental usage.
850  postponed_list.clear();
851 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3426
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:3395
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:102
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
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:4441
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
virtual literalt lor(literalt a, literalt b)=0
representationt
Definition: bv_utils.h:31
The trinary if-then-else operator.
Definition: std_expr.h:3361
exprt & cond()
Definition: std_expr.h:3385
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:4424
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:245
void post_process() override
Definition: boolbv.h:60
configt config
Definition: config.cpp:23
#define POSTCONDITION(CONDITION)
Definition: invariant.h:237
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:3871
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:189
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:156
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:230
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3955
#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
The unary minus expression.
Definition: std_expr.h:444
exprt & false_case()
Definition: std_expr.h:3405
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:4465
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:89
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:3895
virtual tvt l_get(literalt a) const =0
#define UNREACHABLE
Definition: invariant.h:250
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:192
bool convert_address_of_rec(const exprt &expr, bvt &bv)
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:1450
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:257
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