cprover
custom_bitvector_analysis.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Field-insensitive, location-sensitive bitvector analysis
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <util/expr_util.h>
15 #include <util/pointer_expr.h>
16 #include <util/simplify_expr.h>
17 #include <util/string_constant.h>
18 #include <util/xml_irep.h>
19 
20 #include <langapi/language_util.h>
21 
22 #include <iostream>
23 
25  const irep_idt &identifier,
26  unsigned bit_nr,
27  modet mode)
28 {
29  switch(mode)
30  {
31  case modet::SET_MUST:
32  set_bit(must_bits[identifier], bit_nr);
33  break;
34 
35  case modet::CLEAR_MUST:
36  clear_bit(must_bits[identifier], bit_nr);
37  break;
38 
39  case modet::SET_MAY:
40  set_bit(may_bits[identifier], bit_nr);
41  break;
42 
43  case modet::CLEAR_MAY:
44  clear_bit(may_bits[identifier], bit_nr);
45  break;
46  }
47 }
48 
50  const exprt &lhs,
51  unsigned bit_nr,
52  modet mode)
53 {
54  irep_idt id=object2id(lhs);
55  if(!id.empty())
56  set_bit(id, bit_nr, mode);
57 }
58 
60 {
61  if(src.id()==ID_symbol)
62  {
63  return to_symbol_expr(src).get_identifier();
64  }
65  else if(src.id()==ID_dereference)
66  {
67  const exprt &op=to_dereference_expr(src).pointer();
68 
69  if(op.id()==ID_address_of)
70  {
71  return object2id(to_address_of_expr(op).object());
72  }
73  else if(op.id()==ID_typecast)
74  {
75  irep_idt op_id=object2id(to_typecast_expr(op).op());
76 
77  if(op_id.empty())
78  return irep_idt();
79  else
80  return '*'+id2string(op_id);
81  }
82  else
83  {
84  irep_idt op_id=object2id(op);
85 
86  if(op_id.empty())
87  return irep_idt();
88  else
89  return '*'+id2string(op_id);
90  }
91  }
92  else if(src.id()==ID_member)
93  {
94  const auto &m=to_member_expr(src);
95  const exprt &op=m.compound();
96 
97  irep_idt op_id=object2id(op);
98 
99  if(op_id.empty())
100  return irep_idt();
101  else
102  return id2string(op_id)+'.'+
103  id2string(m.get_component_name());
104  }
105  else if(src.id()==ID_typecast)
106  return object2id(to_typecast_expr(src).op());
107  else
108  return irep_idt();
109 }
110 
112  const exprt &lhs,
113  const vectorst &vectors)
114 {
115  irep_idt id=object2id(lhs);
116  if(!id.empty())
117  assign_lhs(id, vectors);
118 }
119 
121  const irep_idt &identifier,
122  const vectorst &vectors)
123 {
124  // we erase blank ones to avoid noise
125 
126  if(vectors.must_bits==0)
127  must_bits.erase(identifier);
128  else
129  must_bits[identifier]=vectors.must_bits;
130 
131  if(vectors.may_bits==0)
132  may_bits.erase(identifier);
133  else
134  may_bits[identifier]=vectors.may_bits;
135 }
136 
139 {
140  vectorst vectors;
141 
142  bitst::const_iterator may_it=may_bits.find(identifier);
143  if(may_it!=may_bits.end())
144  vectors.may_bits=may_it->second;
145 
146  bitst::const_iterator must_it=must_bits.find(identifier);
147  if(must_it!=must_bits.end())
148  vectors.must_bits=must_it->second;
149 
150  return vectors;
151 }
152 
155 {
156  if(rhs.id()==ID_symbol ||
157  rhs.id()==ID_dereference)
158  {
159  const irep_idt identifier=object2id(rhs);
160  return get_rhs(identifier);
161  }
162  else if(rhs.id()==ID_typecast)
163  {
164  return get_rhs(to_typecast_expr(rhs).op());
165  }
166  else if(rhs.id()==ID_if)
167  {
168  // need to merge both
169  vectorst v_true=get_rhs(to_if_expr(rhs).true_case());
170  vectorst v_false=get_rhs(to_if_expr(rhs).false_case());
171  return merge(v_true, v_false);
172  }
173 
174  return vectorst();
175 }
176 
178  const exprt &string_expr)
179 {
180  if(string_expr.id()==ID_typecast)
181  return get_bit_nr(to_typecast_expr(string_expr).op());
182  else if(string_expr.id()==ID_address_of)
183  return get_bit_nr(to_address_of_expr(string_expr).object());
184  else if(string_expr.id()==ID_index)
185  return get_bit_nr(to_index_expr(string_expr).array());
186  else if(string_expr.id()==ID_string_constant)
187  return bits.number(to_string_constant(string_expr).get_value());
188  else
189  return bits.number("(unknown)");
190 }
191 
193  const exprt &src,
194  locationt loc)
195 {
196  if(src.id()==ID_symbol)
197  {
198  std::set<exprt> result;
199  result.insert(src);
200  return result;
201  }
202  else if(src.id()==ID_dereference)
203  {
204  exprt pointer=to_dereference_expr(src).pointer();
205 
206  const std::set<exprt> alias_set =
207  local_may_alias_factory(loc).get(loc, pointer);
208 
209  std::set<exprt> result;
210 
211  for(const auto &alias : alias_set)
212  if(alias.type().id() == ID_pointer)
213  result.insert(dereference_exprt(alias));
214 
215  result.insert(src);
216 
217  return result;
218  }
219  else if(src.id()==ID_typecast)
220  {
221  return aliases(to_typecast_expr(src).op(), loc);
222  }
223  else
224  return std::set<exprt>();
225 }
226 
228  locationt from,
229  const exprt &lhs,
230  const exprt &rhs,
232  const namespacet &ns)
233 {
234  if(lhs.type().id() == ID_struct || lhs.type().id() == ID_struct_tag)
235  {
236  const struct_typet &struct_type=
237  to_struct_type(ns.follow(lhs.type()));
238 
239  // assign member-by-member
240  for(const auto &c : struct_type.components())
241  {
242  member_exprt lhs_member(lhs, c),
243  rhs_member(rhs, c);
244  assign_struct_rec(from, lhs_member, rhs_member, cba, ns);
245  }
246  }
247  else
248  {
249  // may alias other stuff
250  std::set<exprt> lhs_set=cba.aliases(lhs, from);
251 
252  vectorst rhs_vectors=get_rhs(rhs);
253 
254  for(const auto &lhs_alias : lhs_set)
255  {
256  assign_lhs(lhs_alias, rhs_vectors);
257  }
258 
259  // is it a pointer?
260  if(lhs.type().id()==ID_pointer)
261  {
262  dereference_exprt lhs_deref(lhs);
263  dereference_exprt rhs_deref(rhs);
264  assign_lhs(lhs_deref, get_rhs(rhs_deref));
265  }
266  }
267 }
268 
270  const irep_idt &function_from,
271  trace_ptrt trace_from,
272  const irep_idt &function_to,
273  trace_ptrt trace_to,
274  ai_baset &ai,
275  const namespacet &ns)
276 {
277  locationt from{trace_from->current_location()};
278  locationt to{trace_to->current_location()};
279 
280  // upcast of ai
282  static_cast<custom_bitvector_analysist &>(ai);
283 
284  const goto_programt::instructiont &instruction=*from;
285 
286  switch(instruction.type)
287  {
288  case ASSIGN:
289  {
290  const code_assignt &code_assign=to_code_assign(instruction.code);
291  assign_struct_rec(from, code_assign.lhs(), code_assign.rhs(), cba, ns);
292  }
293  break;
294 
295  case DECL:
296  {
297  const auto &decl_symbol = instruction.decl_symbol();
298  assign_lhs(decl_symbol, vectorst());
299 
300  // is it a pointer?
301  if(decl_symbol.type().id() == ID_pointer)
302  assign_lhs(dereference_exprt(decl_symbol), vectorst());
303  }
304  break;
305 
306  case DEAD:
307  assign_lhs(instruction.dead_symbol(), vectorst());
308 
309  // is it a pointer?
310  if(instruction.dead_symbol().type().id() == ID_pointer)
312  break;
313 
314  case FUNCTION_CALL:
315  {
316  const code_function_callt &code_function_call=
317  to_code_function_call(instruction.code);
318  const exprt &function=code_function_call.function();
319 
320  if(function.id()==ID_symbol)
321  {
322  const irep_idt &identifier=to_symbol_expr(function).get_identifier();
323 
324  if(
325  identifier == CPROVER_PREFIX "set_must" ||
326  identifier == CPROVER_PREFIX "clear_must" ||
327  identifier == CPROVER_PREFIX "set_may" ||
328  identifier == CPROVER_PREFIX "clear_may")
329  {
330  if(code_function_call.arguments().size()==2)
331  {
332  unsigned bit_nr=
333  cba.get_bit_nr(code_function_call.arguments()[1]);
334 
335  // initialize to make Visual Studio happy
336  modet mode = modet::SET_MUST;
337 
338  if(identifier == CPROVER_PREFIX "set_must")
339  mode=modet::SET_MUST;
340  else if(identifier == CPROVER_PREFIX "clear_must")
341  mode=modet::CLEAR_MUST;
342  else if(identifier == CPROVER_PREFIX "set_may")
343  mode=modet::SET_MAY;
344  else if(identifier == CPROVER_PREFIX "clear_may")
345  mode=modet::CLEAR_MAY;
346  else
347  UNREACHABLE;
348 
349  exprt lhs=code_function_call.arguments()[0];
350 
351  if(lhs.type().id()==ID_pointer)
352  {
353  if(lhs.is_constant() &&
354  to_constant_expr(lhs).get_value()==ID_NULL) // NULL means all
355  {
356  if(mode==modet::CLEAR_MAY)
357  {
358  for(auto &bit : may_bits)
359  clear_bit(bit.second, bit_nr);
360 
361  // erase blank ones
363  }
364  else if(mode==modet::CLEAR_MUST)
365  {
366  for(auto &bit : must_bits)
367  clear_bit(bit.second, bit_nr);
368 
369  // erase blank ones
371  }
372  }
373  else
374  {
375  dereference_exprt deref(lhs);
376 
377  // may alias other stuff
378  std::set<exprt> lhs_set=cba.aliases(deref, from);
379 
380  for(const auto &l : lhs_set)
381  {
382  set_bit(l, bit_nr, mode);
383  }
384  }
385  }
386  }
387  }
388  else if(identifier=="memcpy" ||
389  identifier=="memmove")
390  {
391  if(code_function_call.arguments().size()==3)
392  {
393  // we copy all tracked bits from op1 to op0
394  // we do not consider any bits attached to the size op2
395  dereference_exprt lhs_deref(code_function_call.arguments()[0]);
396  dereference_exprt rhs_deref(code_function_call.arguments()[1]);
397 
398  assign_struct_rec(from, lhs_deref, rhs_deref, cba, ns);
399  }
400  }
401  else
402  {
403  // only if there is an actual call, i.e., we have a body
404  if(function_from != function_to)
405  {
406  const code_typet &code_type=
407  to_code_type(ns.lookup(identifier).type);
408 
409  code_function_callt::argumentst::const_iterator arg_it=
410  code_function_call.arguments().begin();
411  for(const auto &param : code_type.parameters())
412  {
413  const irep_idt &p_identifier=param.get_identifier();
414  if(p_identifier.empty())
415  continue;
416 
417  // there may be a mismatch in the number of arguments
418  if(arg_it==code_function_call.arguments().end())
419  break;
420 
421  // assignments arguments -> parameters
422  symbol_exprt p=ns.lookup(p_identifier).symbol_expr();
423  // may alias other stuff
424  std::set<exprt> lhs_set=cba.aliases(p, from);
425 
426  vectorst rhs_vectors=get_rhs(*arg_it);
427 
428  for(const auto &lhs : lhs_set)
429  {
430  assign_lhs(lhs, rhs_vectors);
431  }
432 
433  // is it a pointer?
434  if(p.type().id()==ID_pointer)
435  {
436  dereference_exprt lhs_deref(p);
437  dereference_exprt rhs_deref(*arg_it);
438  assign_lhs(lhs_deref, get_rhs(rhs_deref));
439  }
440 
441  ++arg_it;
442  }
443  }
444  }
445  }
446  }
447  break;
448 
449  case OTHER:
450  {
451  const auto &code = instruction.get_other();
452  const irep_idt &statement = code.get_statement();
453 
454  if(
455  statement == ID_set_may || statement == ID_set_must ||
456  statement == ID_clear_may || statement == ID_clear_must)
457  {
459  code.operands().size() == 2, "set/clear_may/must has two operands");
460 
461  unsigned bit_nr = cba.get_bit_nr(code.op1());
462 
463  // initialize to make Visual Studio happy
464  modet mode = modet::SET_MUST;
465 
466  if(statement == ID_set_must)
467  mode=modet::SET_MUST;
468  else if(statement == ID_clear_must)
469  mode=modet::CLEAR_MUST;
470  else if(statement == ID_set_may)
471  mode=modet::SET_MAY;
472  else if(statement == ID_clear_may)
473  mode=modet::CLEAR_MAY;
474  else
475  UNREACHABLE;
476 
477  exprt lhs = code.op0();
478 
479  if(lhs.type().id()==ID_pointer)
480  {
481  if(lhs.is_constant() &&
482  to_constant_expr(lhs).get_value()==ID_NULL) // NULL means all
483  {
484  if(mode==modet::CLEAR_MAY)
485  {
486  for(bitst::iterator b_it=may_bits.begin();
487  b_it!=may_bits.end();
488  b_it++)
489  clear_bit(b_it->second, bit_nr);
490 
491  // erase blank ones
493  }
494  else if(mode==modet::CLEAR_MUST)
495  {
496  for(bitst::iterator b_it=must_bits.begin();
497  b_it!=must_bits.end();
498  b_it++)
499  clear_bit(b_it->second, bit_nr);
500 
501  // erase blank ones
503  }
504  }
505  else
506  {
507  dereference_exprt deref(lhs);
508 
509  // may alias other stuff
510  std::set<exprt> lhs_set=cba.aliases(deref, from);
511 
512  for(const auto &l : lhs_set)
513  {
514  set_bit(l, bit_nr, mode);
515  }
516  }
517  }
518  }
519  }
520  break;
521 
522  case GOTO:
523  if(has_get_must_or_may(instruction.get_condition()))
524  {
525  exprt guard = instruction.get_condition();
526 
527  // Comparing iterators is safe as the target must be within the same list
528  // of instructions because this is a GOTO.
529  if(to!=from->get_target())
530  guard = boolean_negate(guard);
531 
532  const exprt result2 = simplify_expr(eval(guard, cba), ns);
533 
534  if(result2.is_false())
535  make_bottom();
536  }
537  break;
538 
539  case CATCH:
540  case THROW:
541  DATA_INVARIANT(false, "Exceptions must be removed before analysis");
542  break;
543  case RETURN:
544  DATA_INVARIANT(false, "Returns must be removed before analysis");
545  break;
546  case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
547  case ATOMIC_END: // Ignoring is a valid over-approximation
548  case END_FUNCTION: // No action required
549  case LOCATION: // No action required
550  case START_THREAD: // Require a concurrent analysis at higher level
551  case END_THREAD: // Require a concurrent analysis at higher level
552  case SKIP: // No action required
553  case ASSERT: // No action required
554  case ASSUME: // Ignoring is a valid over-approximation
555  break;
556  case INCOMPLETE_GOTO:
557  case NO_INSTRUCTION_TYPE:
558  DATA_INVARIANT(false, "Only complete instructions can be analyzed");
559  break;
560  }
561 }
562 
564  std::ostream &out,
565  const ai_baset &ai,
566  const namespacet &) const
567 {
568  if(has_values.is_known())
569  {
570  out << has_values.to_string() << '\n';
571  return;
572  }
573 
574  const custom_bitvector_analysist &cba=
575  static_cast<const custom_bitvector_analysist &>(ai);
576 
577  for(const auto &bit : may_bits)
578  {
579  out << bit.first << " MAY:";
580  bit_vectort b=bit.second;
581 
582  for(unsigned i=0; b!=0; i++, b>>=1)
583  if(b&1)
584  {
585  assert(i<cba.bits.size());
586  out << ' '
587  << cba.bits[i];
588  }
589 
590  out << '\n';
591  }
592 
593  for(const auto &bit : must_bits)
594  {
595  out << bit.first << " MUST:";
596  bit_vectort b=bit.second;
597 
598  for(unsigned i=0; b!=0; i++, b>>=1)
599  if(b&1)
600  {
601  assert(i<cba.bits.size());
602  out << ' '
603  << cba.bits[i];
604  }
605 
606  out << '\n';
607  }
608 }
609 
611  const custom_bitvector_domaint &b,
612  locationt,
613  locationt)
614 {
615  bool changed=has_values.is_false();
617 
618  // first do MAY
619  bitst::iterator it=may_bits.begin();
620  for(const auto &bit : b.may_bits)
621  {
622  while(it!=may_bits.end() && it->first<bit.first)
623  ++it;
624  if(it==may_bits.end() || bit.first<it->first)
625  {
626  may_bits.insert(it, bit);
627  changed=true;
628  }
629  else if(it!=may_bits.end())
630  {
631  bit_vectort &a_bits=it->second;
632  bit_vectort old=a_bits;
633  a_bits|=bit.second;
634  if(old!=a_bits)
635  changed=true;
636 
637  ++it;
638  }
639  }
640 
641  // now do MUST
642  it=must_bits.begin();
643  for(auto &bit : b.must_bits)
644  {
645  while(it!=must_bits.end() && it->first<bit.first)
646  {
647  it=must_bits.erase(it);
648  changed=true;
649  }
650  if(it==must_bits.end() || bit.first<it->first)
651  {
652  must_bits.insert(it, bit);
653  changed=true;
654  }
655  else if(it!=must_bits.end())
656  {
657  bit_vectort &a_bits=it->second;
658  bit_vectort old=a_bits;
659  a_bits&=bit.second;
660  if(old!=a_bits)
661  changed=true;
662 
663  ++it;
664  }
665  }
666 
667  // erase blank ones
670 
671  return changed;
672 }
673 
676 {
677  for(bitst::iterator a_it=bits.begin();
678  a_it!=bits.end();
679  ) // no a_it++
680  {
681  if(a_it->second==0)
682  a_it=bits.erase(a_it);
683  else
684  a_it++;
685  }
686 }
687 
689 {
690  if(src.id() == ID_get_must || src.id() == ID_get_may)
691  return true;
692 
693  forall_operands(it, src)
694  if(has_get_must_or_may(*it))
695  return true;
696 
697  return false;
698 }
699 
701  const exprt &src,
702  custom_bitvector_analysist &custom_bitvector_analysis) const
703 {
704  if(src.id() == ID_get_must || src.id() == ID_get_may)
705  {
706  if(src.operands().size()==2)
707  {
708  unsigned bit_nr =
709  custom_bitvector_analysis.get_bit_nr(to_binary_expr(src).op1());
710 
711  exprt pointer = to_binary_expr(src).op0();
712 
713  if(pointer.type().id()!=ID_pointer)
714  return src;
715 
716  if(pointer.is_constant() &&
717  to_constant_expr(pointer).get_value()==ID_NULL) // NULL means all
718  {
719  if(src.id() == ID_get_may)
720  {
721  for(const auto &bit : may_bits)
722  if(get_bit(bit.second, bit_nr))
723  return true_exprt();
724 
725  return false_exprt();
726  }
727  else if(src.id() == ID_get_must)
728  {
729  return false_exprt();
730  }
731  else
732  return src;
733  }
734  else
735  {
737  get_rhs(dereference_exprt(pointer));
738 
739  bool value=false;
740 
741  if(src.id() == ID_get_must)
742  value=get_bit(v.must_bits, bit_nr);
743  else if(src.id() == ID_get_may)
744  value=get_bit(v.may_bits, bit_nr);
745 
746  if(value)
747  return true_exprt();
748  else
749  return false_exprt();
750  }
751  }
752  else
753  return src;
754  }
755  else
756  {
757  exprt tmp=src;
758  Forall_operands(it, tmp)
759  *it=eval(*it, custom_bitvector_analysis);
760 
761  return tmp;
762  }
763 }
764 
766 {
767 }
768 
770  const goto_modelt &goto_model,
771  bool use_xml,
772  std::ostream &out)
773 {
774  unsigned pass=0, fail=0, unknown=0;
775 
776  for(const auto &gf_entry : goto_model.goto_functions.function_map)
777  {
778  if(!gf_entry.second.body.has_assertion())
779  continue;
780 
781  // TODO this is a hard-coded hack
782  if(gf_entry.first == "__actual_thread_spawn")
783  continue;
784 
785  if(!use_xml)
786  out << "******** Function " << gf_entry.first << '\n';
787 
788  forall_goto_program_instructions(i_it, gf_entry.second.body)
789  {
790  exprt result;
791  irep_idt description;
792 
793  if(i_it->is_assert())
794  {
796  i_it->get_condition()))
797  {
798  continue;
799  }
800 
801  if(operator[](i_it).has_values.is_false())
802  continue;
803 
804  exprt tmp = eval(i_it->get_condition(), i_it);
805  const namespacet ns(goto_model.symbol_table);
806  result = simplify_expr(std::move(tmp), ns);
807 
808  description=i_it->source_location.get_comment();
809  }
810  else
811  continue;
812 
813  if(use_xml)
814  {
815  out << "<result status=\"";
816  if(result.is_true())
817  out << "SUCCESS";
818  else if(result.is_false())
819  out << "FAILURE";
820  else
821  out << "UNKNOWN";
822  out << "\">\n";
823  out << xml(i_it->source_location);
824  out << "<description>"
825  << description
826  << "</description>\n";
827  out << "</result>\n\n";
828  }
829  else
830  {
831  out << i_it->source_location;
832  if(!description.empty())
833  out << ", " << description;
834  out << ": ";
835  const namespacet ns(goto_model.symbol_table);
836  out << from_expr(ns, gf_entry.first, result);
837  out << '\n';
838  }
839 
840  if(result.is_true())
841  pass++;
842  else if(result.is_false())
843  fail++;
844  else
845  unknown++;
846  }
847 
848  if(!use_xml)
849  out << '\n';
850  }
851 
852  if(!use_xml)
853  out << "SUMMARY: " << pass << " pass, " << fail << " fail, "
854  << unknown << " unknown\n";
855 }
custom_bitvector_domaint::modet::CLEAR_MAY
@ CLEAR_MAY
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
custom_bitvector_domaint::assign_lhs
void assign_lhs(const exprt &, const vectorst &)
Definition: custom_bitvector_analysis.cpp:111
custom_bitvector_domaint::object2id
static irep_idt object2id(const exprt &)
Definition: custom_bitvector_analysis.cpp:59
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:25
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
custom_bitvector_domaint::vectorst::must_bits
bit_vectort must_bits
Definition: custom_bitvector_analysis.h:85
custom_bitvector_domaint::modet::SET_MAY
@ SET_MAY
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:312
ai_baset::locationt
goto_programt::const_targett locationt
Definition: ai.h:127
custom_bitvector_domaint::assign_struct_rec
void assign_struct_rec(locationt from, const exprt &lhs, const exprt &rhs, custom_bitvector_analysist &, const namespacet &)
Definition: custom_bitvector_analysis.cpp:227
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
custom_bitvector_domaint::erase_blank_vectors
void erase_blank_vectors(bitst &)
erase blank bitvectors
Definition: custom_bitvector_analysis.cpp:675
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2152
custom_bitvector_analysis.h
Field-insensitive, location-sensitive bitvector analysis.
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:256
goto_programt::instructiont::type
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:337
custom_bitvector_domaint::get_rhs
vectorst get_rhs(const exprt &) const
Definition: custom_bitvector_analysis.cpp:154
custom_bitvector_domaint::modet::CLEAR_MUST
@ CLEAR_MUST
custom_bitvector_domaint::must_bits
bitst must_bits
Definition: custom_bitvector_analysis.h:99
to_string_constant
const string_constantt & to_string_constant(const exprt &expr)
Definition: string_constant.h:31
string_constant.h
exprt
Base class for all expressions.
Definition: expr.h:54
xml_irep.h
goto_modelt
Definition: goto_model.h:26
exprt::op0
exprt & op0()
Definition: expr.h:103
custom_bitvector_analysist::eval
exprt eval(const exprt &src, locationt loc)
Definition: custom_bitvector_analysis.h:159
irep_idt
dstringt irep_idt
Definition: irep.h:37
custom_bitvector_domaint::set_bit
void set_bit(const exprt &, unsigned bit_nr, modet)
Definition: custom_bitvector_analysis.cpp:49
custom_bitvector_analysist::instrument
void instrument(goto_functionst &)
Definition: custom_bitvector_analysis.cpp:765
custom_bitvector_analysist::aliases
std::set< exprt > aliases(const exprt &, locationt loc)
Definition: custom_bitvector_analysis.cpp:192
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:47
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
goto_programt::instructiont::decl_symbol
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
Definition: goto_program.h:212
custom_bitvector_domaint::may_bits
bitst may_bits
Definition: custom_bitvector_analysis.h:99
ai_domain_baset::trace_ptrt
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:78
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:56
tvt::is_known
bool is_known() const
Definition: threeval.h:28
goto_programt::instructiont::get_other
const codet & get_other() const
Get the statement for OTHER.
Definition: goto_program.h:320
custom_bitvector_domaint::clear_bit
static void clear_bit(bit_vectort &dest, unsigned bit_nr)
Definition: custom_bitvector_analysis.h:135
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:628
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
THROW
@ THROW
Definition: goto_program.h:51
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
GOTO
@ GOTO
Definition: goto_program.h:35
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:949
custom_bitvector_domaint::output
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
Definition: custom_bitvector_analysis.cpp:563
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
custom_bitvector_domaint::modet
modet
Definition: custom_bitvector_analysis.h:125
custom_bitvector_domaint::modet::SET_MUST
@ SET_MUST
goto_programt::instructiont::dead_symbol
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
Definition: goto_program.h:254
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
xml
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:105
goto_programt::instructiont::code
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:183
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
language_util.h
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:110
dereference_exprt::pointer
exprt & pointer()
Definition: pointer_expr.h:269
boolean_negate
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:128
pointer_expr.h
API to expression classes for Pointers.
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
custom_bitvector_domaint
Definition: custom_bitvector_analysis.h:24
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2529
NO_INSTRUCTION_TYPE
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:34
custom_bitvector_analysist
Definition: custom_bitvector_analysis.h:152
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
code_typet
Base type of functions.
Definition: std_types.h:744
OTHER
@ OTHER
Definition: goto_program.h:38
irept::id
const irep_idt & id() const
Definition: irep.h:407
tvt::unknown
static tvt unknown()
Definition: threeval.h:33
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1326
dstringt::empty
bool empty() const
Definition: dstring.h:88
tvt::to_string
const char * to_string() const
Definition: threeval.cpp:13
false_exprt
The Boolean constant false.
Definition: std_expr.h:2726
END_FUNCTION
@ END_FUNCTION
Definition: goto_program.h:43
SKIP
@ SKIP
Definition: goto_program.h:39
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:860
tvt::is_false
bool is_false() const
Definition: threeval.h:26
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1260
custom_bitvector_domaint::vectorst::may_bits
bit_vectort may_bits
Definition: custom_bitvector_analysis.h:85
simplify_expr.h
RETURN
@ RETURN
Definition: goto_program.h:46
numberingt::size
size_type size() const
Definition: numbering.h:66
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2528
expr_util.h
Deprecated expression utility functions.
ASSIGN
@ ASSIGN
Definition: goto_program.h:47
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
custom_bitvector_domaint::has_get_must_or_may
static bool has_get_must_or_may(const exprt &)
Definition: custom_bitvector_analysis.cpp:688
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition: ai_domain.h:77
local_may_alias_factoryt::get
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
custom_bitvector_domaint::bit_vectort
unsigned long long bit_vectort
Definition: custom_bitvector_analysis.h:79
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
CATCH
@ CATCH
Definition: goto_program.h:52
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
DECL
@ DECL
Definition: goto_program.h:48
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
numberingt::number
number_type number(const key_type &a)
Definition: numbering.h:37
ASSUME
@ ASSUME
Definition: goto_program.h:36
custom_bitvector_domaint::vectorst
Definition: custom_bitvector_analysis.h:84
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1815
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:40
custom_bitvector_analysist::local_may_alias_factory
local_may_alias_factoryt local_may_alias_factory
Definition: custom_bitvector_analysis.h:178
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
custom_bitvector_domaint::eval
exprt eval(const exprt &src, custom_bitvector_analysist &) const
Definition: custom_bitvector_analysis.cpp:700
START_THREAD
@ START_THREAD
Definition: goto_program.h:40
FUNCTION_CALL
@ FUNCTION_CALL
Definition: goto_program.h:50
custom_bitvector_analysist::check
void check(const goto_modelt &, bool xml, std::ostream &)
Definition: custom_bitvector_analysis.cpp:769
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2612
ATOMIC_END
@ ATOMIC_END
Definition: goto_program.h:45
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:237
DEAD
@ DEAD
Definition: goto_program.h:49
exprt::operands
operandst & operands()
Definition: expr.h:96
ATOMIC_BEGIN
@ ATOMIC_BEGIN
Definition: goto_program.h:44
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
true_exprt
The Boolean constant true.
Definition: std_expr.h:2717
goto_programt::instructiont::get_condition
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:350
LOCATION
@ LOCATION
Definition: goto_program.h:42
custom_bitvector_analysist::bits
bitst bits
Definition: custom_bitvector_analysis.h:167
ASSERT
@ ASSERT
Definition: goto_program.h:37
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
custom_bitvector_domaint::transform
void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) final override
how function calls are treated: a) there is an edge from each call site to the function head b) there...
Definition: custom_bitvector_analysis.cpp:269
custom_bitvector_domaint::bitst
std::map< irep_idt, bit_vectort > bitst
Definition: custom_bitvector_analysis.h:81
custom_bitvector_domaint::has_values
tvt has_values
Definition: custom_bitvector_analysis.h:113
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
END_THREAD
@ END_THREAD
Definition: goto_program.h:41
INCOMPLETE_GOTO
@ INCOMPLETE_GOTO
Definition: goto_program.h:53
code_function_callt::function
exprt & function()
Definition: std_code.h:1250
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1167
custom_bitvector_analysist::get_bit_nr
unsigned get_bit_nr(const exprt &)
Definition: custom_bitvector_analysis.cpp:177
binary_exprt::op0
exprt & op0()
Definition: expr.h:103
custom_bitvector_domaint::merge
bool merge(const custom_bitvector_domaint &b, locationt from, locationt to)
Definition: custom_bitvector_analysis.cpp:610
custom_bitvector_domaint::get_bit
static bool get_bit(const bit_vectort src, unsigned bit_nr)
Definition: custom_bitvector_analysis.h:141
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2701
custom_bitvector_domaint::make_bottom
void make_bottom() final override
no states
Definition: custom_bitvector_analysis.h:39