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/xml_expr.h>
15 #include <util/simplify_expr.h>
16 
17 #include <iostream>
18 
20  const irep_idt &identifier,
21  unsigned bit_nr,
22  modet mode)
23 {
24  switch(mode)
25  {
26  case modet::SET_MUST:
27  set_bit(must_bits[identifier], bit_nr);
28  break;
29 
30  case modet::CLEAR_MUST:
31  clear_bit(must_bits[identifier], bit_nr);
32  break;
33 
34  case modet::SET_MAY:
35  set_bit(may_bits[identifier], bit_nr);
36  break;
37 
38  case modet::CLEAR_MAY:
39  clear_bit(may_bits[identifier], bit_nr);
40  break;
41  }
42 }
43 
45  const exprt &lhs,
46  unsigned bit_nr,
47  modet mode)
48 {
49  irep_idt id=object2id(lhs);
50  if(!id.empty())
51  set_bit(id, bit_nr, mode);
52 }
53 
55 {
56  if(src.id()==ID_symbol)
57  {
58  return to_symbol_expr(src).get_identifier();
59  }
60  else if(src.id()==ID_dereference)
61  {
62  const exprt &op=to_dereference_expr(src).pointer();
63 
64  if(op.id()==ID_address_of)
65  {
66  return object2id(to_address_of_expr(op).object());
67  }
68  else if(op.id()==ID_typecast)
69  {
71  }
72  else
73  {
74  irep_idt op_id=object2id(op);
75  if(op_id.empty())
76  return irep_idt();
77  else
78  return '*'+id2string(op_id);
79  }
80  }
81  else if(src.id()==ID_typecast)
82  return object2id(to_typecast_expr(src).op());
83  else
84  return irep_idt();
85 }
86 
88  const exprt &lhs,
89  const vectorst &vectors)
90 {
91  irep_idt id=object2id(lhs);
92  if(!id.empty())
93  assign_lhs(id, vectors);
94 }
95 
97  const irep_idt &identifier,
98  const vectorst &vectors)
99 {
100  // we erase blank ones to avoid noise
101 
102  if(vectors.must_bits==0)
103  must_bits.erase(identifier);
104  else
105  must_bits[identifier]=vectors.must_bits;
106 
107  if(vectors.may_bits==0)
108  may_bits.erase(identifier);
109  else
110  may_bits[identifier]=vectors.may_bits;
111 }
112 
115 {
116  vectorst vectors;
117 
118  bitst::const_iterator may_it=may_bits.find(identifier);
119  if(may_it!=may_bits.end())
120  vectors.may_bits=may_it->second;
121 
122  bitst::const_iterator must_it=must_bits.find(identifier);
123  if(must_it!=must_bits.end())
124  vectors.must_bits=must_it->second;
125 
126  return vectors;
127 }
128 
131 {
132  if(rhs.id()==ID_symbol ||
133  rhs.id()==ID_dereference)
134  {
135  const irep_idt identifier=object2id(rhs);
136  return get_rhs(identifier);
137  }
138  else if(rhs.id()==ID_typecast)
139  {
140  return get_rhs(to_typecast_expr(rhs).op());
141  }
142  else if(rhs.id()==ID_if)
143  {
144  // need to merge both
145  vectorst v_true=get_rhs(to_if_expr(rhs).true_case());
146  vectorst v_false=get_rhs(to_if_expr(rhs).false_case());
147  return merge(v_true, v_false);
148  }
149 
150  return vectorst();
151 }
152 
154  const exprt &string_expr)
155 {
156  if(string_expr.id()==ID_typecast)
157  return get_bit_nr(to_typecast_expr(string_expr).op());
158  else if(string_expr.id()==ID_address_of)
159  return get_bit_nr(to_address_of_expr(string_expr).object());
160  else if(string_expr.id()==ID_index)
161  return get_bit_nr(to_index_expr(string_expr).array());
162  else if(string_expr.id()==ID_string_constant)
163  {
164  irep_idt value=string_expr.get(ID_value);
165  return bits(value);
166  }
167  else
168  return bits("(unknown)");
169 }
170 
172  const exprt &src,
173  locationt loc)
174 {
175  if(src.id()==ID_symbol)
176  {
177  std::set<exprt> result;
178  result.insert(src);
179  return result;
180  }
181  else if(src.id()==ID_dereference)
182  {
183  exprt pointer=to_dereference_expr(src).pointer();
184 
185  std::set<exprt> pointer_set=
186  local_may_alias_factory(loc).get(loc, pointer);
187 
188  std::set<exprt> result;
189 
190  for(const auto &pointer : pointer_set)
191  {
192  result.insert(dereference_exprt(pointer));
193  }
194 
195  result.insert(src);
196 
197  return result;
198  }
199  else if(src.id()==ID_typecast)
200  {
201  return aliases(to_typecast_expr(src).op(), loc);
202  }
203  else
204  return std::set<exprt>();
205 }
206 
208  locationt from,
209  locationt to,
210  ai_baset &ai,
211  const namespacet &ns)
212 {
213  // upcast of ai
215  static_cast<custom_bitvector_analysist &>(ai);
216 
217  const goto_programt::instructiont &instruction=*from;
218 
219  switch(instruction.type)
220  {
221  case ASSIGN:
222  {
223  const code_assignt &code_assign=to_code_assign(instruction.code);
224 
225  // may alias other stuff
226  std::set<exprt> lhs_set=cba.aliases(code_assign.lhs(), from);
227 
228  vectorst rhs_vectors=get_rhs(code_assign.rhs());
229 
230  for(const auto &lhs : lhs_set)
231  {
232  assign_lhs(lhs, rhs_vectors);
233  }
234 
235  // is it a pointer?
236  if(code_assign.lhs().type().id()==ID_pointer)
237  {
238  dereference_exprt lhs_deref(code_assign.lhs());
239  dereference_exprt rhs_deref(code_assign.rhs());
240  vectorst rhs_vectors=get_rhs(rhs_deref);
241  assign_lhs(lhs_deref, rhs_vectors);
242  }
243  }
244  break;
245 
246  case DECL:
247  {
248  const code_declt &code_decl=to_code_decl(instruction.code);
249  assign_lhs(code_decl.symbol(), vectorst());
250 
251  // is it a pointer?
252  if(code_decl.symbol().type().id()==ID_pointer)
253  assign_lhs(dereference_exprt(code_decl.symbol()), vectorst());
254  }
255  break;
256 
257  case DEAD:
258  {
259  const code_deadt &code_dead=to_code_dead(instruction.code);
260  assign_lhs(code_dead.symbol(), vectorst());
261 
262  // is it a pointer?
263  if(code_dead.symbol().type().id()==ID_pointer)
264  assign_lhs(dereference_exprt(code_dead.symbol()), vectorst());
265  }
266  break;
267 
268  case FUNCTION_CALL:
269  {
270  const code_function_callt &code_function_call=
271  to_code_function_call(instruction.code);
272  const exprt &function=code_function_call.function();
273 
274  if(function.id()==ID_symbol)
275  {
276  const irep_idt &identifier=to_symbol_expr(function).get_identifier();
277 
278  if(identifier=="__CPROVER_set_must" ||
279  identifier=="__CPROVER_clear_must" ||
280  identifier=="__CPROVER_set_may" ||
281  identifier=="__CPROVER_clear_may")
282  {
283  if(code_function_call.arguments().size()==2)
284  {
285  unsigned bit_nr=
286  cba.get_bit_nr(code_function_call.arguments()[1]);
287 
288  modet mode;
289 
290  if(identifier=="__CPROVER_set_must")
291  mode=modet::SET_MUST;
292  else if(identifier=="__CPROVER_clear_must")
293  mode=modet::CLEAR_MUST;
294  else if(identifier=="__CPROVER_set_may")
295  mode=modet::SET_MAY;
296  else if(identifier=="__CPROVER_clear_may")
297  mode=modet::CLEAR_MAY;
298  else
299  assert(false);
300 
301  exprt lhs=code_function_call.arguments()[0];
302 
303  if(lhs.is_constant() &&
304  to_constant_expr(lhs).get_value()==ID_NULL) // NULL means all
305  {
306  if(mode==modet::CLEAR_MAY)
307  {
308  for(auto &bit : may_bits)
309  clear_bit(bit.second, bit_nr);
310 
311  // erase blank ones
313  }
314  else if(mode==modet::CLEAR_MUST)
315  {
316  for(auto &bit : must_bits)
317  clear_bit(bit.second, bit_nr);
318 
319  // erase blank ones
321  }
322  }
323  else
324  {
325  dereference_exprt deref(lhs);
326 
327  // may alias other stuff
328  std::set<exprt> lhs_set=cba.aliases(deref, from);
329 
330  for(const auto &lhs : lhs_set)
331  {
332  set_bit(lhs, bit_nr, mode);
333  }
334  }
335  }
336  }
337  else
338  {
340  ++next;
341 
342  // only if there is an actual call, i.e., we have a body
343  if(next!=to)
344  {
345  const code_typet &code_type=
346  to_code_type(ns.lookup(identifier).type);
347 
348  code_function_callt::argumentst::const_iterator arg_it=
349  code_function_call.arguments().begin();
350  for(const auto &param : code_type.parameters())
351  {
352  const irep_idt &p_identifier=param.get_identifier();
353  if(p_identifier.empty())
354  continue;
355 
356  // there may be a mismatch in the number of arguments
357  if(arg_it==code_function_call.arguments().end())
358  break;
359 
360  // assignments arguments -> parameters
361  symbol_exprt p=ns.lookup(p_identifier).symbol_expr();
362  // may alias other stuff
363  std::set<exprt> lhs_set=cba.aliases(p, from);
364 
365  vectorst rhs_vectors=get_rhs(*arg_it);
366 
367  for(const auto &lhs : lhs_set)
368  {
369  assign_lhs(lhs, rhs_vectors);
370  }
371 
372  // is it a pointer?
373  if(p.type().id()==ID_pointer)
374  {
375  dereference_exprt lhs_deref(p);
376  dereference_exprt rhs_deref(*arg_it);
377  vectorst rhs_vectors=get_rhs(rhs_deref);
378  assign_lhs(lhs_deref, rhs_vectors);
379  }
380 
381  ++arg_it;
382  }
383  }
384  }
385  }
386  }
387  break;
388 
389  case OTHER:
390  {
391  const irep_idt &statement=instruction.code.get_statement();
392 
393  if(statement=="set_may" ||
394  statement=="set_must" ||
395  statement=="clear_may" ||
396  statement=="clear_must")
397  {
398  assert(instruction.code.operands().size()==2);
399 
400  unsigned bit_nr=
401  cba.get_bit_nr(instruction.code.op1());
402 
403  modet mode;
404 
405  if(statement=="set_must")
406  mode=modet::SET_MUST;
407  else if(statement=="clear_must")
408  mode=modet::CLEAR_MUST;
409  else if(statement=="set_may")
410  mode=modet::SET_MAY;
411  else if(statement=="clear_may")
412  mode=modet::CLEAR_MAY;
413  else
414  assert(false);
415 
416  exprt lhs=instruction.code.op0();
417 
418  if(lhs.is_constant() &&
419  to_constant_expr(lhs).get_value()==ID_NULL) // NULL means all
420  {
421  if(mode==modet::CLEAR_MAY)
422  {
423  for(bitst::iterator b_it=may_bits.begin();
424  b_it!=may_bits.end();
425  b_it++)
426  clear_bit(b_it->second, bit_nr);
427 
428  // erase blank ones
430  }
431  else if(mode==modet::CLEAR_MUST)
432  {
433  for(bitst::iterator b_it=must_bits.begin();
434  b_it!=must_bits.end();
435  b_it++)
436  clear_bit(b_it->second, bit_nr);
437 
438  // erase blank ones
440  }
441  }
442  else
443  {
444  dereference_exprt deref(lhs);
445 
446  // may alias other stuff
447  std::set<exprt> lhs_set=cba.aliases(deref, from);
448 
449  for(const auto &lhs : lhs_set)
450  {
451  set_bit(lhs, bit_nr, mode);
452  }
453  }
454  }
455  }
456  break;
457 
458  case GOTO:
459  if(has_get_must_or_may(instruction.guard))
460  {
461  exprt guard=instruction.guard;
462 
463  if(to!=from->get_target())
464  guard.make_not();
465 
466  exprt result=eval(guard, cba);
467  exprt result2=simplify_expr(result, ns);
468 
469  if(result2.is_false())
470  make_bottom();
471  }
472  break;
473 
474  default:
475  {
476  }
477  }
478 }
479 
481  std::ostream &out,
482  const ai_baset &ai,
483  const namespacet &ns) const
484 {
485  if(has_values.is_known())
486  {
487  out << has_values.to_string() << '\n';
488  return;
489  }
490 
491  const custom_bitvector_analysist &cba=
492  static_cast<const custom_bitvector_analysist &>(ai);
493 
494  for(const auto &bit : may_bits)
495  {
496  out << bit.first << " MAY:";
497  bit_vectort b=bit.second;
498 
499  for(unsigned i=0; b!=0; i++, b>>=1)
500  if(b&1)
501  {
502  assert(i<cba.bits.size());
503  out << ' '
504  << cba.bits[i];
505  }
506 
507  out << '\n';
508  }
509 
510  for(const auto &bit : must_bits)
511  {
512  out << bit.first << " MUST:";
513  bit_vectort b=bit.second;
514 
515  for(unsigned i=0; b!=0; i++, b>>=1)
516  if(b&1)
517  {
518  assert(i<cba.bits.size());
519  out << ' '
520  << cba.bits[i];
521  }
522 
523  out << '\n';
524  }
525 }
526 
528  const custom_bitvector_domaint &b,
529  locationt from,
530  locationt to)
531 {
532  bool changed=has_values.is_false();
534 
535  // first do MAY
536  bitst::iterator it=may_bits.begin();
537  for(const auto &bit : b.may_bits)
538  {
539  while(it!=may_bits.end() && it->first<bit.first)
540  ++it;
541  if(it==may_bits.end() || bit.first<it->first)
542  {
543  may_bits.insert(it, bit);
544  changed=true;
545  }
546  else if(it!=may_bits.end())
547  {
548  bit_vectort &a_bits=it->second;
549  bit_vectort old=a_bits;
550  a_bits|=bit.second;
551  if(old!=a_bits)
552  changed=true;
553 
554  ++it;
555  }
556  }
557 
558  // now do MUST
559  it=must_bits.begin();
560  for(auto &bit : b.must_bits)
561  {
562  while(it!=must_bits.end() && it->first<bit.first)
563  {
564  it=must_bits.erase(it);
565  changed=true;
566  }
567  if(it==must_bits.end() || bit.first<it->first)
568  {
569  must_bits.insert(it, bit);
570  changed=true;
571  }
572  else if(it!=must_bits.end())
573  {
574  bit_vectort &a_bits=it->second;
575  bit_vectort old=a_bits;
576  a_bits&=bit.second;
577  if(old!=a_bits)
578  changed=true;
579 
580  ++it;
581  }
582  }
583 
584  // erase blank ones
587 
588  return changed;
589 }
590 
593 {
594  for(bitst::iterator a_it=bits.begin();
595  a_it!=bits.end();
596  ) // no a_it++
597  {
598  if(a_it->second==0)
599  a_it=bits.erase(a_it);
600  else
601  a_it++;
602  }
603 }
604 
606 {
607  if(src.id()=="get_must" ||
608  src.id()=="get_may")
609  return true;
610 
611  forall_operands(it, src)
612  if(has_get_must_or_may(*it))
613  return true;
614 
615  return false;
616 }
617 
619  const exprt &src,
620  custom_bitvector_analysist &custom_bitvector_analysis) const
621 {
622  if(src.id()=="get_must" || src.id()=="get_may")
623  {
624  if(src.operands().size()==2)
625  {
626  unsigned bit_nr=
627  custom_bitvector_analysis.get_bit_nr(src.op1());
628 
629  exprt pointer=src.op0();
630 
631  if(pointer.is_constant() &&
632  to_constant_expr(pointer).get_value()==ID_NULL) // NULL means all
633  {
634  if(src.id()=="get_may")
635  {
636  for(const auto &bit : may_bits)
637  if(get_bit(bit.second, bit_nr))
638  return true_exprt();
639 
640  return false_exprt();
641  }
642  else if(src.id()=="get_must")
643  {
644  return false_exprt();
645  }
646  else
647  return src;
648  }
649  else
650  {
652  get_rhs(dereference_exprt(pointer));
653 
654  bool value=false;
655 
656  if(src.id()=="get_must")
657  value=get_bit(v.must_bits, bit_nr);
658  else if(src.id()=="get_may")
659  value=get_bit(v.may_bits, bit_nr);
660 
661  if(value)
662  return true_exprt();
663  else
664  return false_exprt();
665  }
666  }
667  else
668  return src;
669  }
670  else
671  {
672  exprt tmp=src;
673  Forall_operands(it, tmp)
674  *it=eval(*it, custom_bitvector_analysis);
675 
676  return tmp;
677  }
678 }
679 
681 {
682 }
683 
685  const namespacet &ns,
686  const goto_functionst &goto_functions,
687  bool use_xml,
688  std::ostream &out)
689 {
690  unsigned pass=0, fail=0, unknown=0;
691 
692  forall_goto_functions(f_it, goto_functions)
693  {
694  if(!f_it->second.body.has_assertion())
695  continue;
696 
697  // TODO this is a hard-coded hack
698  if(f_it->first=="__actual_thread_spawn")
699  continue;
700 
701  if(!use_xml)
702  out << "******** Function " << f_it->first << '\n';
703 
704  forall_goto_program_instructions(i_it, f_it->second.body)
705  {
706  exprt result;
707  irep_idt description;
708 
709  if(i_it->is_assert())
710  {
712  continue;
713 
714  if(operator[](i_it).has_values.is_false())
715  continue;
716 
717  exprt tmp=eval(i_it->guard, i_it);
718  result=simplify_expr(tmp, ns);
719 
720  description=i_it->source_location.get_comment();
721  }
722  else
723  continue;
724 
725  if(use_xml)
726  {
727  out << "<result status=\"";
728  if(result.is_true())
729  out << "SUCCESS";
730  else if(result.is_false())
731  out << "FAILURE";
732  else
733  out << "UNKNOWN";
734  out << "\">\n";
735  out << xml(i_it->source_location);
736  out << "<description>"
737  << description
738  << "</description>\n";
739  out << "</result>\n\n";
740  }
741  else
742  {
743  out << i_it->source_location;
744  if(!description.empty())
745  out << ", " << description;
746  out << ": ";
747  out << from_expr(ns, f_it->first, result);
748  out << '\n';
749  }
750 
751  if(result.is_true())
752  pass++;
753  else if(result.is_false())
754  fail++;
755  else
756  unknown++;
757  }
758 
759  if(!use_xml)
760  out << '\n';
761  }
762 
763  if(!use_xml)
764  out << "SUMMARY: " << pass << " pass, " << fail << " fail, "
765  << unknown << " unknown\n";
766 }
#define loc()
bool is_false() const
Definition: threeval.h:26
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:1760
void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) final
Field-insensitive, location-sensitive bitvector analysis.
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:218
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
Base type of functions.
Definition: std_types.h:734
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
exprt & object()
Definition: std_expr.h:2608
goto_programt::const_targett locationt
Definition: ai.h:112
std::map< irep_idt, bit_vectort > bitst
exprt & op0()
Definition: expr.h:84
exprt simplify_expr(const exprt &src, const namespacet &ns)
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:260
exprt & symbol()
Definition: std_code.h:205
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
const irep_idt & get_identifier() const
Definition: std_expr.h:120
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
static tvt unknown()
Definition: threeval.h:33
bool is_false() const
Definition: expr.cpp:140
const irep_idt & get_value() const
Definition: std_expr.h:3702
local_may_alias_factoryt local_may_alias_factory
bool is_true() const
Definition: expr.cpp:133
typet & type()
Definition: expr.h:60
static irep_idt object2id(const exprt &)
exprt & op()
Definition: std_expr.h:1739
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:25
static bool get_bit(const bit_vectort src, unsigned bit_nr)
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
Definition: std_expr.h:2748
void assign_lhs(const exprt &, const vectorst &)
const char * to_string() const
Definition: threeval.cpp:13
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1229
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:178
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:157
instructionst::const_iterator const_targett
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Definition: std_expr.h:2629
The boolean constant true.
Definition: std_expr.h:3742
argumentst & arguments()
Definition: std_code.h:689
A declaration of a local variable.
Definition: std_code.h:192
void check(const namespacet &, const goto_functionst &, bool xml, std::ostream &)
static void clear_bit(bit_vectort &dest, unsigned bit_nr)
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:2836
bool is_known() const
Definition: threeval.h:28
exprt & rhs()
Definition: std_code.h:162
void set_bit(const exprt &, unsigned bit_nr, modet)
Operator to dereference a pointer.
Definition: std_expr.h:2701
void erase_blank_vectors(bitst &)
erase blank bitvectors
static bool has_get_must_or_may(const exprt &)
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
exprt eval(const exprt &src, custom_bitvector_analysist &) const
vectorst get_rhs(const exprt &) const
TO_BE_DOCUMENTED.
Definition: namespace.h:62
A function call.
Definition: std_code.h:657
#define forall_operands(it, expr)
Definition: expr.h:17
exprt & symbol()
Definition: std_code.h:247
The boolean constant false.
Definition: std_expr.h:3753
bool is_constant() const
Definition: expr.cpp:128
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
void make_not()
Definition: expr.cpp:100
exprt & function()
Definition: std_code.h:677
Definition: ai.h:108
Base class for all expressions.
Definition: expr.h:46
exprt & pointer()
Definition: std_expr.h:2727
const parameterst & parameters() const
Definition: std_types.h:841
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
exprt eval(const exprt &src, locationt loc)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
bool merge(const custom_bitvector_domaint &b, locationt from, locationt to)
A removal of a local variable.
Definition: std_code.h:234
#define Forall_operands(it, expr)
Definition: expr.h:23
std::set< exprt > aliases(const exprt &, locationt loc)
goto_programt::const_targett locationt
Definition: ai.h:42
Expression to hold a symbol (variable)
Definition: std_expr.h:82
dstringt irep_idt
Definition: irep.h:32
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:3725
#define forall_goto_functions(it, functions)
operandst & operands()
Definition: expr.h:70
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
bool empty() const
Definition: dstring.h:61
exprt & array()
Definition: std_expr.h:1198
Assignment.
Definition: std_code.h:144
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700