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/c_types.h>
12 #include <util/config.h>
13 #include <util/arith_tools.h>
14 #include <util/prefix.h>
15 #include <util/std_expr.h>
17 #include <util/threeval.h>
18 
20 {
21  if(expr.type().id()!=ID_bool)
22  throw "bv_pointerst::convert_rest got non-boolean operand";
23 
24  const exprt::operandst &operands=expr.operands();
25 
26  if(expr.id()==ID_invalid_pointer)
27  {
28  if(operands.size()==1 &&
29  is_ptr(operands[0].type()))
30  {
31  const bvt &bv=convert_bv(operands[0]);
32 
33  if(!bv.empty())
34  {
35  bvt invalid_bv, null_bv;
38 
39  bvt equal_invalid_bv, equal_null_bv;
40  equal_invalid_bv.resize(object_bits);
41  equal_null_bv.resize(object_bits);
42 
43  for(std::size_t i=0; i<object_bits; i++)
44  {
45  equal_invalid_bv[i]=prop.lequal(bv[offset_bits+i],
46  invalid_bv[offset_bits+i]);
47  equal_null_bv[i] =prop.lequal(bv[offset_bits+i],
48  null_bv[offset_bits+i]);
49  }
50 
51  literalt equal_invalid=prop.land(equal_invalid_bv);
52  literalt equal_null=prop.land(equal_null_bv);
53 
54  return prop.lor(equal_invalid, equal_null);
55  }
56  }
57  }
58  else if(expr.id()==ID_dynamic_object)
59  {
60  if(operands.size()==1 &&
61  is_ptr(operands[0].type()))
62  {
63  // we postpone
65 
66  postponed_list.push_back(postponedt());
67  postponed_list.back().op=convert_bv(operands[0]);
68  postponed_list.back().bv.push_back(l);
69  postponed_list.back().expr=expr;
70 
71  return l;
72  }
73  }
74  else if(expr.id()==ID_lt || expr.id()==ID_le ||
75  expr.id()==ID_gt || expr.id()==ID_ge)
76  {
77  if(operands.size()==2 &&
78  is_ptr(operands[0].type()) &&
79  is_ptr(operands[1].type()))
80  {
81  const bvt &bv0=convert_bv(operands[0]);
82  const bvt &bv1=convert_bv(operands[1]);
83 
84  return bv_utils.rel(
85  bv0, expr.id(), bv1, bv_utilst::representationt::UNSIGNED);
86  }
87  }
88 
89  return SUB::convert_rest(expr);
90 }
91 
93  const namespacet &_ns,
94  propt &_prop):
95  boolbvt(_ns, _prop),
96  pointer_logic(_ns)
97 {
101 }
102 
104  const exprt &expr,
105  bvt &bv)
106 {
107  if(expr.id()==ID_symbol)
108  {
109  add_addr(expr, bv);
110  return false;
111  }
112  else if(expr.id()==ID_label)
113  {
114  add_addr(expr, bv);
115  return false;
116  }
117  else if(expr.id()=="NULL-object")
118  {
120  return false;
121  }
122  else if(expr.id()==ID_index)
123  {
124  if(expr.operands().size()!=2)
125  throw "index takes two operands";
126 
127  const index_exprt &index_expr=to_index_expr(expr);
128  const exprt &array=index_expr.array();
129  const exprt &index=index_expr.index();
130  const typet &array_type=ns.follow(array.type());
131 
132  // recursive call
133  if(array_type.id()==ID_pointer)
134  {
135  // this should be gone
136  bv=convert_pointer_type(array);
137  assert(bv.size()==bits);
138  }
139  else if(array_type.id()==ID_array ||
140  array_type.id()==ID_incomplete_array ||
141  array_type.id()==ID_string_constant)
142  {
143  if(convert_address_of_rec(array, bv))
144  return true;
145  assert(bv.size()==bits);
146  }
147  else
148  assert(false);
149 
150  // get size
151  mp_integer size=
152  pointer_offset_size(array_type.subtype(), ns);
153  assert(size>0);
154 
155  offset_arithmetic(bv, size, index);
156  assert(bv.size()==bits);
157  return false;
158  }
159  else if(expr.id()==ID_member)
160  {
161  const member_exprt &member_expr=to_member_expr(expr);
162  const exprt &struct_op=member_expr.op0();
163  const typet &struct_op_type=ns.follow(struct_op.type());
164 
165  // recursive call
166  if(convert_address_of_rec(struct_op, bv))
167  return true;
168 
169  if(struct_op_type.id()==ID_struct)
170  {
171  mp_integer offset=member_offset(
172  to_struct_type(struct_op_type),
173  member_expr.get_component_name(), ns);
174  assert(offset>=0);
175 
176  // add offset
177  offset_arithmetic(bv, offset);
178  }
179  else if(struct_op_type.id()==ID_union)
180  {
181  // nothing to do, all members have offset 0
182  }
183  else
184  throw "member takes struct or union operand";
185 
186  return false;
187  }
188  else if(expr.id()==ID_constant ||
189  expr.id()==ID_string_constant ||
190  expr.id()==ID_array)
191  { // constant
192  add_addr(expr, bv);
193  return false;
194  }
195  else if(expr.id()==ID_if)
196  {
197  const if_exprt &ifex=to_if_expr(expr);
198 
199  literalt cond=convert(ifex.cond());
200 
201  bvt bv1, bv2;
202 
203  if(convert_address_of_rec(ifex.true_case(), bv1))
204  return true;
205 
206  if(convert_address_of_rec(ifex.false_case(), bv2))
207  return true;
208 
209  bv=bv_utils.select(cond, bv1, bv2);
210 
211  return false;
212  }
213 
214  return true;
215 }
216 
218 {
219  if(!is_ptr(expr.type()))
220  throw "convert_pointer_type got non-pointer type";
221 
222  // make sure the config hasn't been changed
223  assert(bits==config.ansi_c.pointer_width);
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  if(expr.operands().size()!=1)
250  throw "typecast takes one operand";
251 
252  const exprt &op=expr.op0();
253  const typet &op_type=ns.follow(op.type());
254 
255  if(op_type.id()==ID_pointer)
256  return convert_bv(op);
257  else if(op_type.id()==ID_signedbv ||
258  op_type.id()==ID_unsignedbv ||
259  op_type.id()==ID_bool ||
260  op_type.id()==ID_c_enum ||
261  op_type.id()==ID_c_enum_tag)
262  {
263  // Cast from integer to pointer.
264  // We just do a zero extension.
265 
266  const bvt &op_bv=convert_bv(op);
267 
268  return bv_utils.zero_extension(op_bv, bits);
269  }
270  }
271  else if(expr.id()==ID_if)
272  {
273  return SUB::convert_if(to_if_expr(expr));
274  }
275  else if(expr.id()==ID_index)
276  {
277  return SUB::convert_index(to_index_expr(expr));
278  }
279  else if(expr.id()==ID_member)
280  {
281  return SUB::convert_member(to_member_expr(expr));
282  }
283  else if(expr.id()==ID_address_of)
284  {
285  if(expr.operands().size()!=1)
286  throw expr.id_string()+" takes one operand";
287 
288  bvt bv;
289  bv.resize(bits);
290 
291  if(convert_address_of_rec(expr.op0(), bv))
292  {
293  conversion_failed(expr, bv);
294  return bv;
295  }
296 
297  assert(bv.size()==bits);
298  return bv;
299  }
300  else if(expr.id()==ID_constant)
301  {
302  irep_idt value=to_constant_expr(expr).get_value();
303 
304  bvt bv;
305  bv.resize(bits);
306 
307  if(value==ID_NULL)
309  else
310  {
311  mp_integer i=string2integer(id2string(value), 2);
313  }
314 
315  return bv;
316  }
317  else if(expr.id()==ID_plus)
318  {
319  // this has to be pointer plus integer
320 
321  if(expr.operands().size()<2)
322  throw "operator + takes at least two operands";
323 
324  bvt bv;
325 
326  mp_integer size=0;
327  std::size_t count=0;
328 
329  forall_operands(it, expr)
330  {
331  if(it->type().id()==ID_pointer)
332  {
333  count++;
334  bv=convert_bv(*it);
335  assert(bv.size()==bits);
336 
337  typet pointer_sub_type=it->type().subtype();
338  if(pointer_sub_type.id()==ID_empty)
339  pointer_sub_type=char_type();
340  size=pointer_offset_size(pointer_sub_type, ns);
341  assert(size>0);
342  }
343  }
344 
345  if(count==0)
346  throw "found no pointer in pointer-type sum";
347  else if(count!=1)
348  throw "found more than one pointer in sum";
349 
351 
352  forall_operands(it, expr)
353  {
354  if(it->type().id()==ID_pointer)
355  continue;
356 
357  if(it->type().id()!=ID_unsignedbv &&
358  it->type().id()!=ID_signedbv)
359  {
360  bvt bv;
361  conversion_failed(expr, bv);
362  return bv;
363  }
364 
366  it->type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
368 
369  bvt op=convert_bv(*it);
370 
371  if(op.empty())
372  throw "unexpected pointer arithmetic operand width";
373 
374  // we cut any extra bits off
375 
376  if(op.size()>bits)
377  op.resize(bits);
378  else if(op.size()<bits)
379  op=bv_utils.extension(op, bits, rep);
380 
381  sum=bv_utils.add(sum, op);
382  }
383 
384  offset_arithmetic(bv, size, sum);
385 
386  return bv;
387  }
388  else if(expr.id()==ID_minus)
389  {
390  // this is pointer-integer
391 
392  if(expr.operands().size()!=2)
393  throw "operator "+expr.id_string()+" takes two operands";
394 
395  if(expr.op0().type().id()!=ID_pointer)
396  throw "found no pointer in pointer type in difference";
397 
398  bvt bv;
399 
400  if(expr.op1().type().id()!=ID_unsignedbv &&
401  expr.op1().type().id()!=ID_signedbv)
402  {
403  bvt bv;
404  conversion_failed(expr, bv);
405  return bv;
406  }
407 
408  exprt neg_op1=unary_exprt(
409  ID_unary_minus, expr.op1(), expr.op1().type());
410 
411  bv=convert_bv(expr.op0());
412 
413  mp_integer element_size=
414  pointer_offset_size(expr.op0().type().subtype(), ns);
415  assert(element_size>0);
416 
417  offset_arithmetic(bv, element_size, neg_op1);
418 
419  return bv;
420  }
421  else if(expr.id()==ID_lshr ||
422  expr.id()==ID_shl)
423  {
424  return SUB::convert_shift(to_shift_expr(expr));
425  }
426  else if(expr.id()==ID_bitand ||
427  expr.id()==ID_bitor ||
428  expr.id()==ID_bitnot)
429  {
430  return convert_bitwise(expr);
431  }
432  else if(expr.id()==ID_concatenation)
433  {
434  return SUB::convert_concatenation(expr);
435  }
436  else if(expr.id()==ID_byte_extract_little_endian ||
437  expr.id()==ID_byte_extract_big_endian)
438  {
440  }
441 
442  return conversion_failed(expr);
443 }
444 
446 {
447  if(is_ptr(expr.type()))
448  return convert_pointer_type(expr);
449 
450  if(expr.id()==ID_minus &&
451  expr.operands().size()==2 &&
452  expr.op0().type().id()==ID_pointer &&
453  expr.op1().type().id()==ID_pointer)
454  {
455  // pointer minus pointer
456  bvt op0=convert_bv(expr.op0());
457  bvt op1=convert_bv(expr.op1());
458 
459  std::size_t width=boolbv_width(expr.type());
460 
461  if(width==0)
462  return conversion_failed(expr);
463 
464  // we do a zero extension
465  op0=bv_utils.zero_extension(op0, width);
466  op1=bv_utils.zero_extension(op1, width);
467 
468  bvt bv=bv_utils.sub(op0, op1);
469 
470  mp_integer element_size=
471  pointer_offset_size(expr.op0().type().subtype(), ns);
472  assert(element_size>0);
473 
474  if(element_size!=1)
475  {
476  bvt element_size_bv=
477  bv_utils.build_constant(element_size, bv.size());
478  bv=bv_utils.divider(
479  bv, element_size_bv, bv_utilst::representationt::SIGNED);
480  }
481 
482  return bv;
483  }
484  else if(expr.id()==ID_pointer_offset &&
485  expr.operands().size()==1 &&
486  is_ptr(expr.op0().type()))
487  {
488  bvt op0=convert_bv(expr.op0());
489 
490  std::size_t width=boolbv_width(expr.type());
491 
492  if(width==0)
493  return conversion_failed(expr);
494 
495  // we need to strip off the object part
496  op0.resize(offset_bits);
497 
498  // we do a sign extension to permit negative offsets
499  return bv_utils.sign_extension(op0, width);
500  }
501  else if(expr.id()==ID_object_size &&
502  expr.operands().size()==1 &&
503  is_ptr(expr.op0().type()))
504  {
505  // we postpone until we know the objects
506  std::size_t width=boolbv_width(expr.type());
507 
508  bvt bv;
509  bv.resize(width);
510 
511  for(std::size_t i=0; i<width; i++)
512  bv[i]=prop.new_variable();
513 
514  postponed_list.push_back(postponedt());
515 
516  postponed_list.back().op=convert_bv(expr.op0());
517  postponed_list.back().bv=bv;
518  postponed_list.back().expr=expr;
519 
520  return bv;
521  }
522  else if(expr.id()==ID_pointer_object &&
523  expr.operands().size()==1 &&
524  is_ptr(expr.op0().type()))
525  {
526  bvt op0=convert_bv(expr.op0());
527 
528  std::size_t width=boolbv_width(expr.type());
529 
530  if(width==0)
531  return conversion_failed(expr);
532 
533  // erase offset bits
534 
535  op0.erase(op0.begin()+0, op0.begin()+offset_bits);
536 
537  return bv_utils.zero_extension(op0, width);
538  }
539  else if(expr.id()==ID_typecast &&
540  expr.operands().size()==1 &&
541  expr.op0().type().id()==ID_pointer)
542  {
543  // pointer to int
544  bvt op0=convert_pointer_type(expr.op0());
545 
546  // squeeze it in!
547 
548  std::size_t width=boolbv_width(expr.type());
549 
550  if(width==0)
551  return conversion_failed(expr);
552 
553  return bv_utils.zero_extension(op0, width);
554  }
555 
556  return SUB::convert_bitvector(expr);
557 }
558 
560  const bvt &bv,
561  const std::vector<bool> &unknown,
562  std::size_t offset,
563  const typet &type) const
564 {
565  if(!is_ptr(type))
566  return SUB::bv_get_rec(bv, unknown, offset, type);
567 
568  std::string value_addr, value_offset, value;
569 
570  for(std::size_t i=0; i<bits; i++)
571  {
572  char ch;
573  std::size_t bit_nr=i+offset;
574 
575  if(unknown[bit_nr])
576  ch='0';
577  else
578  {
579  switch(prop.l_get(bv[bit_nr]).get_value())
580  {
581  case tvt::tv_enumt::TV_FALSE: ch='0'; break;
582  case tvt::tv_enumt::TV_TRUE: ch='1'; break;
583  case tvt::tv_enumt::TV_UNKNOWN: ch='0'; break;
584  default: assert(false);
585  }
586  }
587 
588  value=ch+value;
589 
590  if(i<offset_bits)
591  value_offset=ch+value_offset;
592  else
593  value_addr=ch+value_addr;
594  }
595 
596  // we treat these like bit-vector constants, but with
597  // some additional annotation
598 
599  constant_exprt result(type);
600  result.set_value(value);
601 
602  pointer_logict::pointert pointer;
603  pointer.object=integer2unsigned(binary2integer(value_addr, false));
604  pointer.offset=binary2integer(value_offset, true);
605 
606  // we add the elaborated expression as operand
607  result.copy_to_operands(
608  pointer_logic.pointer_expr(pointer, type));
609 
610  return result;
611 }
612 
613 void bv_pointerst::encode(std::size_t addr, bvt &bv)
614 {
615  bv.resize(bits);
616 
617  // set offset to zero
618  for(std::size_t i=0; i<offset_bits; i++)
619  bv[i]=const_literal(false);
620 
621  // set variable part
622  for(std::size_t i=0; i<object_bits; i++)
623  bv[offset_bits+i]=const_literal((addr&(std::size_t(1)<<i))!=0);
624 }
625 
627 {
628  bvt bv1=bv;
629  bv1.resize(offset_bits); // strip down
630 
632 
633  bvt tmp=bv_utils.add(bv1, bv2);
634 
635  // copy offset bits
636  for(std::size_t i=0; i<offset_bits; i++)
637  bv[i]=tmp[i];
638 }
639 
641  bvt &bv,
642  const mp_integer &factor,
643  const exprt &index)
644 {
645  bvt bv_index=convert_bv(index);
646 
648  index.type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
650 
651  bv_index=bv_utils.extension(bv_index, offset_bits, rep);
652 
653  offset_arithmetic(bv, factor, bv_index);
654 }
655 
657  bvt &bv,
658  const mp_integer &factor,
659  const bvt &index)
660 {
661  bvt bv_index;
662 
663  if(factor==1)
664  bv_index=index;
665  else
666  {
667  bvt bv_factor=bv_utils.build_constant(factor, index.size());
668  bv_index=bv_utils.unsigned_multiplier(index, bv_factor);
669  }
670 
671  bv_index=bv_utils.zero_extension(bv_index, bv.size());
672 
673  bvt bv_tmp=bv_utils.add(bv, bv_index);
674 
675  // copy lower parts of result
676  for(std::size_t i=0; i<offset_bits; i++)
677  bv[i]=bv_tmp[i];
678 }
679 
680 void bv_pointerst::add_addr(const exprt &expr, bvt &bv)
681 {
682  std::size_t a=pointer_logic.add_object(expr);
683 
684  if(a==(std::size_t(1)<<object_bits))
685  throw "too many variables";
686 
687  encode(a, bv);
688 }
689 
691  const postponedt &postponed)
692 {
693  if(postponed.expr.id()==ID_dynamic_object)
694  {
695  const pointer_logict::objectst &objects=
697 
698  std::size_t number=0;
699 
700  for(pointer_logict::objectst::const_iterator
701  it=objects.begin();
702  it!=objects.end();
703  it++, number++)
704  {
705  const exprt &expr=*it;
706 
707  bool is_dynamic=pointer_logic.is_dynamic_object(expr);
708 
709  // only compare object part
710  bvt bv;
711  encode(number, bv);
712 
713  bv.erase(bv.begin(), bv.begin()+offset_bits);
714 
715  bvt saved_bv=postponed.op;
716  saved_bv.erase(saved_bv.begin(), saved_bv.begin()+offset_bits);
717 
718  assert(bv.size()==saved_bv.size());
719  assert(postponed.bv.size()==1);
720 
721  literalt l1=bv_utils.equal(bv, saved_bv);
722  literalt l2=postponed.bv.front();
723 
724  if(!is_dynamic)
725  l2=!l2;
726 
727  prop.l_set_to(prop.limplies(l1, l2), true);
728  }
729  }
730  else if(postponed.expr.id()==ID_object_size)
731  {
732  const pointer_logict::objectst &objects=
734 
735  std::size_t number=0;
736 
737  for(pointer_logict::objectst::const_iterator
738  it=objects.begin();
739  it!=objects.end();
740  it++, number++)
741  {
742  const exprt &expr=*it;
743 
745 
746  if(expr.id()==ID_symbol)
747  {
748  // just get the type
749  const typet &type=ns.follow(expr.type());
750 
751  exprt size_expr=size_of_expr(type, ns);
752 
753  if(size_expr.is_nil())
754  continue;
755 
756  if(to_integer(size_expr, object_size))
757  continue;
758  }
759  else
760  continue;
761 
762  // only compare object part
763  bvt bv;
764  encode(number, bv);
765 
766  bv.erase(bv.begin(), bv.begin()+offset_bits);
767 
768  bvt saved_bv=postponed.op;
769  saved_bv.erase(saved_bv.begin(), saved_bv.begin()+offset_bits);
770 
771  assert(bv.size()==saved_bv.size());
772  assert(postponed.bv.size()>=1);
773 
774  literalt l1=bv_utils.equal(bv, saved_bv);
775 
776  bvt size_bv=bv_utils.build_constant(object_size, postponed.bv.size());
777  literalt l2=bv_utils.equal(postponed.bv, size_bv);
778 
779  prop.l_set_to(prop.limplies(l1, l2), true);
780  }
781  }
782  else
783  assert(false);
784 }
785 
787 {
788  // post-processing arrays may yield further objects, do this first
790 
791  for(postponed_listt::const_iterator
792  it=postponed_list.begin();
793  it!=postponed_list.end();
794  it++)
795  do_postponed(*it);
796 
797  // Clear the list to avoid re-doing in case of incremental usage.
798  postponed_list.clear();
799 }
The type of an expression.
Definition: type.h:20
exprt size_of_expr(const typet &type, const namespacet &ns)
std::size_t get_null_object() const
Definition: pointer_logic.h:60
mstreamt & result()
Definition: message.h:233
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
struct configt::ansi_ct ansi_c
virtual bvt convert_concatenation(const exprt &expr)
exprt & true_case()
Definition: std_expr.h:2805
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:19
bool is_nil() const
Definition: irep.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
virtual literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:175
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:53
exprt & op0()
Definition: expr.h:84
virtual bvt convert_shift(const binary_exprt &expr)
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.h:83
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1089
literalt convert_rest(const exprt &expr) override
Definition: bv_pointers.cpp:19
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
boolbv_widtht boolbv_width
Definition: boolbv.h:90
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
const irep_idt & get_identifier() const
Definition: std_expr.h:120
bvt convert_bitvector(const exprt &expr) override
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3302
const shift_exprt & to_shift_expr(const exprt &expr)
Cast a generic exprt to a shift_exprt.
Definition: std_expr.h:2280
const irep_idt & get_value() const
Definition: std_expr.h:3702
static bool is_ptr(const typet &type)
Definition: bv_pointers.h:68
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:2771
exprt & cond()
Definition: std_expr.h:2795
bvt sub(const bvt &op0, const bvt &op1)
Definition: bv_utils.h:65
typet & type()
Definition: expr.h:60
A constant literal expression.
Definition: std_expr.h:3685
void post_process() override
Definition: boolbv.h:60
configt config
Definition: config.cpp:21
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
virtual literalt limplies(literalt a, literalt b)=0
Definition: boolbv.h:31
std::size_t get_invalid_object() const
Definition: pointer_logic.h:66
Extract member of struct or union.
Definition: std_expr.h:3214
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1229
virtual literalt land(literalt a, literalt b)=0
exprt object_size(const exprt &pointer)
const irep_idt & id() const
Definition: irep.h:189
void set_value(const irep_idt &value)
Definition: std_expr.h:3707
virtual literalt new_variable()=0
#define Forall_literals(it, bv)
Definition: literal.h:203
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:115
virtual void l_set_to(literalt a, bool value)
Definition: prop.h:42
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:2836
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
Definition: bv_utils.cpp:1262
unsigned offset_bits
Definition: bv_pointers.h:30
virtual bvt convert_bitvector(const exprt &expr)
Definition: boolbv.cpp:154
API to expression classes.
virtual void add_addr(const exprt &expr, bvt &bv)
pointer_logict pointer_logic
Definition: bv_pointers.h:25
exprt & op1()
Definition: expr.h:87
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
unsigned object_bits
Definition: bv_pointers.h:30
Generic base class for unary expressions.
Definition: std_expr.h:221
TO_BE_DOCUMENTED.
Definition: namespace.h:62
bool is_dynamic_object(const exprt &expr) const
#define forall_operands(it, expr)
Definition: expr.h:17
const namespacet & ns
bvt unsigned_multiplier(const bvt &op0, const bvt &op1)
Definition: bv_utils.cpp:614
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
Definition: bv_utils.cpp:96
exprt & false_case()
Definition: std_expr.h:2815
virtual literalt convert_rest(const exprt &expr) override
Definition: boolbv.cpp:424
TO_BE_DOCUMENTED.
Definition: prop.h:22
bvt zero_extension(const bvt &bv, std::size_t new_size)
Definition: bv_utils.h:180
bv_pointerst(const namespacet &_ns, propt &_prop)
Definition: bv_pointers.cpp:92
exprt pointer_expr(const pointert &pointer, const typet &type) const
postponed_listt postponed_list
Definition: bv_pointers.h:64
std::vector< exprt > operandst
Definition: expr.h:49
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
Pointer Logic.
virtual literalt lequal(literalt a, literalt b)=0
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:203
objectst objects
Definition: pointer_logic.h:28
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)
exprt & index()
Definition: std_expr.h:1208
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:46
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
void do_postponed(const postponedt &postponed)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
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)
irep_idt get_component_name() const
Definition: std_expr.h:3249
virtual tvt l_get(literalt a) const =0
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:18
bvt sign_extension(const bvt &bv, std::size_t new_size)
Definition: bv_utils.h:175
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
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:3725
const typet & subtype() const
Definition: type.h:31
unsigned pointer_width
Definition: config.h:36
operandst & operands()
Definition: expr.h:70
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:1198
bitvector_typet char_type()
Definition: c_types.cpp:113
std::vector< literalt > bvt
Definition: literal.h:197
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)
#define BV_ADDR_BITS
Definition: pointer_logic.h:19
array index operator
Definition: std_expr.h:1170