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