cprover
string_instrumentation.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: String Abstraction
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "string_instrumentation.h"
13 
14 #include <algorithm>
15 
16 #include <util/std_expr.h>
17 #include <util/std_code.h>
18 #include <util/message.h>
19 #include <util/arith_tools.h>
20 #include <util/config.h>
21 #include <util/symbol_table.h>
22 
24 #include <util/c_types.h>
25 
27  const exprt &what,
28  bool write)
29 {
30  exprt result=predicate_exprt("is_zero_string");
31  result.copy_to_operands(what);
32  result.set("lhs", write);
33  return result;
34 }
35 
37  const exprt &what,
38  bool write)
39 {
40  exprt result("zero_string_length", size_type());
41  result.copy_to_operands(what);
42  result.set("lhs", write);
43  return result;
44 }
45 
46 exprt buffer_size(const exprt &what)
47 {
48  exprt result("buffer_size", size_type());
49  result.copy_to_operands(what);
50  return result;
51 }
52 
54 {
55 public:
57  symbol_tablet &_symbol_table,
58  message_handlert &_message_handler):
59  messaget(_message_handler),
60  symbol_table(_symbol_table),
61  ns(_symbol_table)
62  {
63  }
64 
65  void operator()(goto_programt &dest);
66  void operator()(goto_functionst &dest);
67 
68 protected:
71 
72  void make_type(exprt &dest, const typet &type)
73  {
74  if(ns.follow(dest.type())!=ns.follow(type))
75  dest.make_typecast(type);
76  }
77 
80 
81  // strings
82  void do_sprintf(
83  goto_programt &dest,
85  code_function_callt &call);
86  void do_snprintf(
87  goto_programt &dest,
89  code_function_callt &call);
90  void do_strcat(
91  goto_programt &dest,
93  code_function_callt &call);
94  void do_strncmp(
95  goto_programt &dest,
97  code_function_callt &call);
98  void do_strchr(
99  goto_programt &dest,
101  code_function_callt &call);
102  void do_strrchr(
103  goto_programt &dest,
105  code_function_callt &call);
106  void do_strstr(
107  goto_programt &dest,
109  code_function_callt &call);
110  void do_strtok(
111  goto_programt &dest,
113  code_function_callt &call);
114  void do_strerror(
115  goto_programt &dest,
117  code_function_callt &call);
118  void do_fscanf(
119  goto_programt &dest,
121  code_function_callt &call);
122 
124  goto_programt &dest,
126  const code_function_callt::argumentst &arguments,
127  unsigned format_string_inx,
128  unsigned argument_start_inx,
129  const std::string &function_name);
130 
132  goto_programt &dest,
134  const code_function_callt::argumentst &arguments,
135  unsigned format_string_inx,
136  unsigned argument_start_inx,
137  const std::string &function_name);
138 
139  bool is_string_type(const typet &t) const
140  {
141  return
142  (t.id()==ID_pointer || t.id()==ID_array) &&
143  (t.subtype().id()==ID_signedbv || t.subtype().id()==ID_unsignedbv) &&
144  (to_bitvector_type(t.subtype()).get_width()==config.ansi_c.char_width);
145  }
146 
147  void invalidate_buffer(
148  goto_programt &dest,
150  const exprt &buffer,
151  const typet &buf_type,
152  const mp_integer &limit);
153 };
154 
156  symbol_tablet &symbol_table,
157  message_handlert &message_handler,
158  goto_programt &dest)
159 {
160  string_instrumentationt string_instrumentation(symbol_table, message_handler);
162 }
163 
165  symbol_tablet &symbol_table,
166  message_handlert &message_handler,
167  goto_functionst &dest)
168 {
169  string_instrumentationt string_instrumentation(symbol_table, message_handler);
171 }
172 
174 {
175  for(goto_functionst::function_mapt::iterator
176  it=dest.function_map.begin();
177  it!=dest.function_map.end();
178  it++)
179  {
180  (*this)(it->second.body);
181  }
182 }
183 
185 {
187  instrument(dest, it);
188 }
189 
191  goto_programt &dest,
193 {
194  switch(it->type)
195  {
196  case ASSIGN:
197  break;
198 
199  case FUNCTION_CALL:
200  do_function_call(dest, it);
201  break;
202 
203  default:
204  {
205  }
206  }
207 }
208 
210  goto_programt &dest,
211  goto_programt::targett target)
212 {
213  code_function_callt &call=
214  to_code_function_call(target->code);
215  exprt &function=call.function();
216  // const exprt &lhs=call.lhs();
217 
218  if(function.id()==ID_symbol)
219  {
220  const irep_idt &identifier=
221  to_symbol_expr(function).get_identifier();
222 
223  if(identifier=="strcoll")
224  {
225  }
226  else if(identifier=="strncmp")
227  do_strncmp(dest, target, call);
228  else if(identifier=="strxfrm")
229  {
230  }
231  else if(identifier=="strchr")
232  do_strchr(dest, target, call);
233  else if(identifier=="strcspn")
234  {
235  }
236  else if(identifier=="strpbrk")
237  {
238  }
239  else if(identifier=="strrchr")
240  do_strrchr(dest, target, call);
241  else if(identifier=="strspn")
242  {
243  }
244  else if(identifier=="strerror")
245  do_strerror(dest, target, call);
246  else if(identifier=="strstr")
247  do_strstr(dest, target, call);
248  else if(identifier=="strtok")
249  do_strtok(dest, target, call);
250  else if(identifier=="sprintf")
251  do_sprintf(dest, target, call);
252  else if(identifier=="snprintf")
253  do_snprintf(dest, target, call);
254  else if(identifier=="fscanf")
255  do_fscanf(dest, target, call);
256 
257  dest.update();
258  }
259 }
260 
262  goto_programt &dest,
263  goto_programt::targett target,
264  code_function_callt &call)
265 {
266  const code_function_callt::argumentst &arguments=call.arguments();
267 
268  if(arguments.size()<2)
269  {
270  error().source_location=target->source_location;
271  error() << "sprintf expected to have two or more arguments" << eom;
272  throw 0;
273  }
274 
275  goto_programt tmp;
276 
277  goto_programt::targett assertion=tmp.add_instruction();
278  assertion->source_location=target->source_location;
279  assertion->source_location.set_property_class("string");
280  assertion->source_location.set_comment("sprintf buffer overflow");
281 
282  // in the abstract model, we have to report a
283  // (possibly false) positive here
284  assertion->make_assertion(false_exprt());
285 
286  do_format_string_read(tmp, target, arguments, 1, 2, "sprintf");
287 
288  if(call.lhs().is_not_nil())
289  {
290  goto_programt::targett return_assignment=tmp.add_instruction(ASSIGN);
291  return_assignment->source_location=target->source_location;
292 
293  exprt rhs=side_effect_expr_nondett(call.lhs().type());
294  rhs.add_source_location()=target->source_location;
295 
296  return_assignment->code=code_assignt(call.lhs(), rhs);
297  }
298 
299  target->make_skip();
300  dest.insert_before_swap(target, tmp);
301 }
302 
304  goto_programt &dest,
305  goto_programt::targett target,
306  code_function_callt &call)
307 {
308  const code_function_callt::argumentst &arguments=call.arguments();
309 
310  if(arguments.size()<3)
311  {
312  error().source_location=target->source_location;
313  error() << "snprintf expected to have three or more arguments"
314  << eom;
315  throw 0;
316  }
317 
318  goto_programt tmp;
319 
320  goto_programt::targett assertion=tmp.add_instruction();
321  assertion->source_location=target->source_location;
322  assertion->source_location.set_property_class("string");
323  assertion->source_location.set_comment("snprintf buffer overflow");
324 
325  exprt bufsize=buffer_size(arguments[0]);
326  assertion->make_assertion(
327  binary_relation_exprt(bufsize, ID_ge, arguments[1]));
328 
329  do_format_string_read(tmp, target, arguments, 2, 3, "snprintf");
330 
331  if(call.lhs().is_not_nil())
332  {
333  goto_programt::targett return_assignment=tmp.add_instruction(ASSIGN);
334  return_assignment->source_location=target->source_location;
335 
336  exprt rhs=side_effect_expr_nondett(call.lhs().type());
337  rhs.add_source_location()=target->source_location;
338 
339  return_assignment->code=code_assignt(call.lhs(), rhs);
340  }
341 
342  target->make_skip();
343  dest.insert_before_swap(target, tmp);
344 }
345 
347  goto_programt &dest,
348  goto_programt::targett target,
349  code_function_callt &call)
350 {
351  const code_function_callt::argumentst &arguments=call.arguments();
352 
353  if(arguments.size()<2)
354  {
355  error().source_location=target->source_location;
356  error() << "fscanf expected to have two or more arguments" << eom;
357  throw 0;
358  }
359 
360  goto_programt tmp;
361 
362  do_format_string_write(tmp, target, arguments, 1, 2, "fscanf");
363 
364  if(call.lhs().is_not_nil())
365  {
366  goto_programt::targett return_assignment=tmp.add_instruction(ASSIGN);
367  return_assignment->source_location=target->source_location;
368 
369  exprt rhs=side_effect_expr_nondett(call.lhs().type());
370  rhs.add_source_location()=target->source_location;
371 
372  return_assignment->code=code_assignt(call.lhs(), rhs);
373  }
374 
375  target->make_skip();
376  dest.insert_before_swap(target, tmp);
377 }
378 
380  goto_programt &dest,
382  const code_function_callt::argumentst &arguments,
383  unsigned format_string_inx,
384  unsigned argument_start_inx,
385  const std::string &function_name)
386 {
387  const exprt &format_arg=arguments[format_string_inx];
388 
389  if(format_arg.id()==ID_address_of &&
390  format_arg.op0().id()==ID_index &&
391  format_arg.op0().op0().id()==ID_string_constant)
392  {
393  format_token_listt token_list=
394  parse_format_string(format_arg.op0().op0().get_string(ID_value));
395 
396  unsigned args=0;
397 
398  for(const auto &token : token_list)
399  {
400  if(token.type==format_tokent::token_typet::STRING)
401  {
402  const exprt &arg=arguments[argument_start_inx+args];
403  const typet &arg_type=ns.follow(arg.type());
404 
405  if(arg.id()!=ID_string_constant) // we don't need to check constants
406  {
407  goto_programt::targett assertion=dest.add_instruction();
408  assertion->source_location=target->source_location;
409  assertion->source_location.set_property_class("string");
410  std::string comment("zero-termination of string argument of ");
411  comment += function_name;
412  assertion->source_location.set_comment(comment);
413 
414  exprt temp(arg);
415 
416  if(arg_type.id()!=ID_pointer)
417  {
418  index_exprt index;
419  index.array()=temp;
420  index.index()=from_integer(0, index_type());
421  index.type()=arg_type.subtype();
422  temp=address_of_exprt(index);
423  }
424 
425  assertion->make_assertion(is_zero_string(temp));
426  }
427  }
428 
429  if(token.type!=format_tokent::token_typet::TEXT &&
430  token.type!=format_tokent::token_typet::UNKNOWN) args++;
431 
432  if(find(
433  token.flags.begin(),
434  token.flags.end(),
436  token.flags.end())
437  args++; // just eat the additional argument
438  }
439  }
440  else // non-const format string
441  {
442  goto_programt::targett format_ass=dest.add_instruction();
443  format_ass->make_assertion(is_zero_string(arguments[1]));
444  format_ass->source_location=target->source_location;
445  format_ass->source_location.set_property_class("string");
446  std::string comment("zero-termination of format string of ");
447  comment += function_name;
448  format_ass->source_location.set_comment(comment);
449 
450  for(unsigned i=2; i<arguments.size(); i++)
451  {
452  const exprt &arg=arguments[i];
453  const typet &arg_type=ns.follow(arguments[i].type());
454 
455  if(arguments[i].id()!=ID_string_constant &&
456  is_string_type(arg_type))
457  {
458  goto_programt::targett assertion=dest.add_instruction();
459  assertion->source_location=target->source_location;
460  assertion->source_location.set_property_class("string");
461  std::string comment("zero-termination of string argument of ");
462  comment += function_name;
463  assertion->source_location.set_comment(comment);
464 
465  exprt temp(arg);
466 
467  if(arg_type.id()!=ID_pointer)
468  {
469  index_exprt index;
470  index.array()=temp;
471  index.index()=from_integer(0, index_type());
472  index.type()=arg_type.subtype();
473  temp=address_of_exprt(index);
474  }
475 
476  assertion->make_assertion(is_zero_string(temp));
477  }
478  }
479  }
480 }
481 
483  goto_programt &dest,
485  const code_function_callt::argumentst &arguments,
486  unsigned format_string_inx,
487  unsigned argument_start_inx,
488  const std::string &function_name)
489 {
490  const exprt &format_arg=arguments[format_string_inx];
491 
492  if(format_arg.id()==ID_address_of &&
493  format_arg.op0().id()==ID_index &&
494  format_arg.op0().op0().id()==ID_string_constant) // constant format
495  {
496  format_token_listt token_list=
497  parse_format_string(format_arg.op0().op0().get_string(ID_value));
498 
499  unsigned args=0;
500 
501  for(const auto &token : token_list)
502  {
503  if(find(
504  token.flags.begin(),
505  token.flags.end(),
507  token.flags.end())
508  continue; // asterisk means `ignore this'
509 
510  switch(token.type)
511  {
513  {
514  const exprt &argument=arguments[argument_start_inx+args];
515  const typet &arg_type=ns.follow(argument.type());
516 
517  goto_programt::targett assertion=dest.add_instruction();
518  assertion->source_location=target->source_location;
519  assertion->source_location.set_property_class("string");
520  std::string comment("format string buffer overflow in ");
521  comment += function_name;
522  assertion->source_location.set_comment(comment);
523 
524  if(token.field_width!=0)
525  {
526  exprt fwidth=from_integer(token.field_width, unsigned_int_type());
527  exprt fw_1(ID_plus, unsigned_int_type());
529  fw_1.move_to_operands(fwidth);
530  fw_1.move_to_operands(one); // +1 for 0-char
531 
532  exprt fw_lt_bs;
533 
534  if(arg_type.id()==ID_pointer)
535  fw_lt_bs=
536  binary_relation_exprt(fw_1, ID_le, buffer_size(argument));
537  else
538  {
539  index_exprt index;
540  index.array()=argument;
541  index.index()=from_integer(0, unsigned_int_type());
542  address_of_exprt aof(index);
543  fw_lt_bs=binary_relation_exprt(fw_1, ID_le, buffer_size(aof));
544  }
545 
546  assertion->make_assertion(fw_lt_bs);
547  }
548  else
549  {
550  // this is a possible overflow.
551  assertion->make_assertion(false_exprt());
552  }
553 
554  // now kill the contents
556  dest, target, argument, arg_type, token.field_width);
557 
558  args++;
559  break;
560  }
563  {
564  // nothing
565  break;
566  }
567  default: // everything else
568  {
569  const exprt &argument=arguments[argument_start_inx+args];
570  const typet &arg_type=ns.follow(argument.type());
571 
573  assignment->source_location=target->source_location;
574 
575  exprt lhs(ID_dereference, arg_type.subtype());
576  lhs.copy_to_operands(argument);
577 
578  exprt rhs=side_effect_expr_nondett(lhs.type());
579  rhs.add_source_location()=target->source_location;
580 
581  assignment->code=code_assignt(lhs, rhs);
582 
583  args++;
584  break;
585  }
586  }
587  }
588  }
589  else // non-const format string
590  {
591  for(unsigned i=argument_start_inx; i<arguments.size(); i++)
592  {
593  const typet &arg_type=ns.follow(arguments[i].type());
594 
595  // Note: is_string_type() is a `good guess' here. Actually
596  // any of the pointers could point into an array. But it
597  // would suck if we had to invalidate all variables.
598  // Luckily this case isn't needed too often.
599  if(is_string_type(arg_type))
600  {
601  goto_programt::targett assertion=dest.add_instruction();
602  assertion->source_location=target->source_location;
603  assertion->source_location.set_property_class("string");
604  std::string comment("format string buffer overflow in ");
605  comment += function_name;
606  assertion->source_location.set_comment(comment);
607 
608  // as we don't know any field width for the %s that
609  // should be here during runtime, we just report a
610  // possibly false positive
611  assertion->make_assertion(false_exprt());
612 
613  invalidate_buffer(dest, target, arguments[i], arg_type, 0);
614  }
615  else
616  {
618  assignment->source_location=target->source_location;
619 
620  exprt lhs(ID_dereference, arg_type.subtype());
621  lhs.copy_to_operands(arguments[i]);
622 
623  exprt rhs=side_effect_expr_nondett(lhs.type());
624  rhs.add_source_location()=target->source_location;
625 
626  assignment->code=code_assignt(lhs, rhs);
627  }
628  }
629  }
630 }
631 
633  goto_programt &dest,
634  goto_programt::targett target,
635  code_function_callt &call)
636 {
637 }
638 
640  goto_programt &dest,
641  goto_programt::targett target,
642  code_function_callt &call)
643 {
644  const code_function_callt::argumentst &arguments=call.arguments();
645 
646  if(arguments.size()!=2)
647  {
648  error().source_location=target->source_location;
649  error() << "strchr expected to have two arguments" << eom;
650  throw 0;
651  }
652 
653  goto_programt tmp;
654 
655  goto_programt::targett assertion=tmp.add_instruction();
656  assertion->make_assertion(is_zero_string(arguments[0]));
657  assertion->source_location=target->source_location;
658  assertion->source_location.set_property_class("string");
659  assertion->source_location.set_comment(
660  "zero-termination of string argument of strchr");
661 
662  target->make_skip();
663  dest.insert_before_swap(target, tmp);
664 }
665 
667  goto_programt &dest,
668  goto_programt::targett target,
669  code_function_callt &call)
670 {
671  const code_function_callt::argumentst &arguments=call.arguments();
672 
673  if(arguments.size()!=2)
674  {
675  error().source_location=target->source_location;
676  error() << "strrchr expected to have two arguments" << eom;
677  throw 0;
678  }
679 
680  goto_programt tmp;
681 
682  goto_programt::targett assertion=tmp.add_instruction();
683  assertion->make_assertion(is_zero_string(arguments[0]));
684  assertion->source_location=target->source_location;
685  assertion->source_location.set_property_class("string");
686  assertion->source_location.set_comment(
687  "zero-termination of string argument of strrchr");
688 
689  target->make_skip();
690  dest.insert_before_swap(target, tmp);
691 }
692 
694  goto_programt &dest,
695  goto_programt::targett target,
696  code_function_callt &call)
697 {
698  const code_function_callt::argumentst &arguments=call.arguments();
699 
700  if(arguments.size()!=2)
701  {
702  error().source_location=target->source_location;
703  error() << "strstr expected to have two arguments" << eom;
704  throw 0;
705  }
706 
707  goto_programt tmp;
708 
709  goto_programt::targett assertion0=tmp.add_instruction();
710  assertion0->make_assertion(is_zero_string(arguments[0]));
711  assertion0->source_location=target->source_location;
712  assertion0->source_location.set_property_class("string");
713  assertion0->source_location.set_comment(
714  "zero-termination of 1st string argument of strstr");
715 
716  goto_programt::targett assertion1=tmp.add_instruction();
717  assertion1->make_assertion(is_zero_string(arguments[1]));
718  assertion1->source_location=target->source_location;
719  assertion1->source_location.set_property_class("string");
720  assertion1->source_location.set_comment(
721  "zero-termination of 2nd string argument of strstr");
722 
723  target->make_skip();
724  dest.insert_before_swap(target, tmp);
725 }
726 
728  goto_programt &dest,
729  goto_programt::targett target,
730  code_function_callt &call)
731 {
732  const code_function_callt::argumentst &arguments=call.arguments();
733 
734  if(arguments.size()!=2)
735  {
736  error().source_location=target->source_location;
737  error() << "strtok expected to have two arguments" << eom;
738  throw 0;
739  }
740 
741  goto_programt tmp;
742 
743  goto_programt::targett assertion0=tmp.add_instruction();
744  assertion0->make_assertion(is_zero_string(arguments[0]));
745  assertion0->source_location=target->source_location;
746  assertion0->source_location.set_property_class("string");
747  assertion0->source_location.set_comment(
748  "zero-termination of 1st string argument of strtok");
749 
750  goto_programt::targett assertion1=tmp.add_instruction();
751  assertion1->make_assertion(is_zero_string(arguments[1]));
752  assertion1->source_location=target->source_location;
753  assertion1->source_location.set_property_class("string");
754  assertion1->source_location.set_comment(
755  "zero-termination of 2nd string argument of strtok");
756 
757  target->make_skip();
758  dest.insert_before_swap(target, tmp);
759 }
760 
762  goto_programt &dest,
764  code_function_callt &call)
765 {
766  if(call.lhs().is_nil())
767  {
768  it->make_skip();
769  return;
770  }
771 
772  irep_idt identifier_buf="__strerror_buffer";
773  irep_idt identifier_size="__strerror_buffer_size";
774 
775  if(symbol_table.symbols.find(identifier_buf)==symbol_table.symbols.end())
776  {
777  symbolt new_symbol_size;
778  new_symbol_size.base_name="__strerror_buffer_size";
779  new_symbol_size.pretty_name=new_symbol_size.base_name;
780  new_symbol_size.name=identifier_size;
781  new_symbol_size.mode=ID_C;
782  new_symbol_size.type=size_type();
783  new_symbol_size.is_state_var=true;
784  new_symbol_size.is_lvalue=true;
785  new_symbol_size.is_static_lifetime=true;
786 
787  array_typet type;
788  type.subtype()=char_type();
789  type.size()=new_symbol_size.symbol_expr();
790  symbolt new_symbol_buf;
791  new_symbol_buf.mode=ID_C;
792  new_symbol_buf.type=type;
793  new_symbol_buf.is_state_var=true;
794  new_symbol_buf.is_lvalue=true;
795  new_symbol_buf.is_static_lifetime=true;
796  new_symbol_buf.base_name="__strerror_buffer";
797  new_symbol_buf.pretty_name=new_symbol_buf.base_name;
798  new_symbol_buf.name=new_symbol_buf.base_name;
799 
800  symbol_table.move(new_symbol_buf);
801  symbol_table.move(new_symbol_size);
802  }
803 
804  const symbolt &symbol_size=ns.lookup(identifier_size);
805  const symbolt &symbol_buf=ns.lookup(identifier_buf);
806 
807  goto_programt tmp;
808 
809  {
812 
813  assignment1->code=code_assignt(symbol_size.symbol_expr(), nondet_size);
814  assignment1->source_location=it->source_location;
815 
816  goto_programt::targett assumption1=tmp.add_instruction();
817 
818  assumption1->make_assumption(
820  symbol_size.symbol_expr(),
821  ID_notequal,
822  from_integer(0, symbol_size.type)));
823 
824  assumption1->source_location=it->source_location;
825  }
826 
827  // return a pointer to some magic buffer
828  index_exprt index(
829  symbol_buf.symbol_expr(),
830  from_integer(0, index_type()),
831  char_type());
832 
833  address_of_exprt ptr(index);
834 
835  // make that zero-terminated
836  {
838  assignment2->code=code_assignt(is_zero_string(ptr, true), true_exprt());
839  assignment2->source_location=it->source_location;
840  }
841 
842  // assign address
843  {
845  exprt rhs=ptr;
846  make_type(rhs, call.lhs().type());
847  assignment3->code=code_assignt(call.lhs(), rhs);
848  assignment3->source_location=it->source_location;
849  }
850 
851  it->make_skip();
852  dest.insert_before_swap(it, tmp);
853 }
854 
856  goto_programt &dest,
858  const exprt &buffer,
859  const typet &buf_type,
860  const mp_integer &limit)
861 {
862  irep_idt cntr_id="string_instrumentation::$counter";
863 
864  if(symbol_table.symbols.find(cntr_id)==symbol_table.symbols.end())
865  {
866  symbolt new_symbol;
867  new_symbol.base_name="$counter";
868  new_symbol.pretty_name=new_symbol.base_name;
869  new_symbol.name=cntr_id;
870  new_symbol.mode=ID_C;
871  new_symbol.type=size_type();
872  new_symbol.is_state_var=true;
873  new_symbol.is_lvalue=true;
874  new_symbol.is_static_lifetime=true;
875 
876  symbol_table.move(new_symbol);
877  }
878 
879  const symbolt &cntr_sym=ns.lookup(cntr_id);
880 
881  // create a loop that runs over the buffer
882  // and invalidates every element
883 
885  init->source_location=target->source_location;
886  init->code=
887  code_assignt(cntr_sym.symbol_expr(), from_integer(0, cntr_sym.type));
888 
890  check->source_location=target->source_location;
891 
893  invalidate->source_location=target->source_location;
894 
896  increment->source_location=target->source_location;
897 
898  exprt plus(ID_plus, unsigned_int_type());
899  plus.copy_to_operands(cntr_sym.symbol_expr());
901 
902  increment->code=code_assignt(cntr_sym.symbol_expr(), plus);
903 
905  back->source_location=target->source_location;
906  back->make_goto(check);
907  back->guard=true_exprt();
908 
910  exit->source_location=target->source_location;
911  exit->make_skip();
912 
913  exprt cnt_bs, bufp;
914 
915  if(buf_type.id()==ID_pointer)
916  bufp=buffer;
917  else
918  {
919  index_exprt index;
920  index.array()=buffer;
921  index.index()=from_integer(0, index_type());
922  index.type()=buf_type.subtype();
923  bufp=address_of_exprt(index);
924  }
925 
926  exprt deref(ID_dereference, buf_type.subtype());
927  exprt b_plus_i(ID_plus, bufp.type());
928  b_plus_i.copy_to_operands(bufp);
929  b_plus_i.copy_to_operands(cntr_sym.symbol_expr());
930  deref.copy_to_operands(b_plus_i);
931 
932  check->make_goto(exit);
933 
934  if(limit==0)
935  check->guard=
937  cntr_sym.symbol_expr(),
938  ID_ge,
939  buffer_size(bufp));
940  else
941  check->guard=
943  cntr_sym.symbol_expr(),
944  ID_gt,
945  from_integer(limit, unsigned_int_type()));
946 
947  exprt nondet=side_effect_expr_nondett(buf_type.subtype());
948  invalidate->code=code_assignt(deref, nondet);
949 }
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
void do_strchr(goto_programt &dest, goto_programt::targett it, code_function_callt &call)
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
struct configt::ansi_ct ansi_c
void update()
Update all indices.
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
BigInt mp_integer
Definition: mp_arith.h:19
string_instrumentationt(symbol_tablet &_symbol_table, message_handlert &_message_handler)
void invalidate_buffer(goto_programt &dest, goto_programt::const_targett target, const exprt &buffer, const typet &buf_type, const mp_integer &limit)
targett add_instruction()
Adds an instruction at the end.
bool is_nil() const
Definition: irep.h:103
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:568
bool is_not_nil() const
Definition: irep.h:104
format_token_listt parse_format_string(const std::string &arg_string)
exprt & op0()
Definition: expr.h:84
irep_idt mode
Language mode.
Definition: symbol.h:55
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:115
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:43
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
const irep_idt & get_identifier() const
Definition: std_expr.h:120
bool is_string_type(const typet &t) const
void do_strrchr(goto_programt &dest, goto_programt::targett it, code_function_callt &call)
void do_strtok(goto_programt &dest, goto_programt::targett it, code_function_callt &call)
void do_strerror(goto_programt &dest, goto_programt::targett it, code_function_callt &call)
void move_to_operands(exprt &expr)
Definition: expr.cpp:28
Format String Parser.
void do_strncmp(goto_programt &dest, goto_programt::targett it, code_function_callt &call)
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:58
typet & type()
Definition: expr.h:60
exprt::operandst argumentst
Definition: std_code.h:687
unsignedbv_typet size_type()
Definition: c_types.cpp:57
unsigned char_width
Definition: config.h:33
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
String Abstraction.
configt config
Definition: config.cpp:21
exprt is_zero_string(const exprt &what, bool write)
bool is_static_lifetime
Definition: symbol.h:70
const irep_idt & id() const
Definition: irep.h:189
void string_instrumentation(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
instructionst::const_iterator const_targett
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:191
void do_strcat(goto_programt &dest, goto_programt::targett it, code_function_callt &call)
The boolean constant true.
Definition: std_expr.h:3742
argumentst & arguments()
Definition: std_code.h:689
symbolst symbols
Definition: symbol_table.h:57
void do_format_string_write(goto_programt &dest, goto_programt::const_targett target, const code_function_callt::argumentst &arguments, unsigned format_string_inx, unsigned argument_start_inx, const std::string &function_name)
source_locationt source_location
Definition: message.h:175
API to expression classes.
The symbol table.
Definition: symbol_table.h:52
void operator()(goto_programt &dest)
TO_BE_DOCUMENTED.
Definition: namespace.h:62
void instrument(goto_programt &dest, goto_programt::targett it)
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1037
const exprt & size() const
Definition: std_types.h:915
A function call.
Definition: std_code.h:657
exprt zero_string_length(const exprt &what, bool write)
bitvector_typet index_type()
Definition: c_types.cpp:15
Symbol table.
void do_fscanf(goto_programt &dest, goto_programt::targett it, code_function_callt &call)
Operator to return the address of an object.
Definition: std_expr.h:2593
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
void do_snprintf(goto_programt &dest, goto_programt::targett it, code_function_callt &call)
The boolean constant false.
Definition: std_expr.h:3753
void do_sprintf(goto_programt &dest, goto_programt::targett it, code_function_callt &call)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
typet type
Type of symbol.
Definition: symbol.h:37
exprt & index()
Definition: std_expr.h:1208
void make_type(exprt &dest, const typet &type)
exprt & function()
Definition: std_code.h:677
Base class for all expressions.
Definition: expr.h:46
bool is_state_var
Definition: symbol.h:66
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
const source_locationt & source_location() const
Definition: expr.h:142
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
mstreamt & error()
Definition: message.h:223
source_locationt & add_source_location()
Definition: expr.h:147
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
arrays with given size
Definition: std_types.h:901
void do_function_call(goto_programt &dest, goto_programt::targett it)
const typet & subtype() const
Definition: type.h:31
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
exprt & array()
Definition: std_expr.h:1198
void make_typecast(const typet &_type)
Definition: expr.cpp:90
void do_format_string_read(goto_programt &dest, goto_programt::const_targett target, const code_function_callt::argumentst &arguments, unsigned format_string_inx, unsigned argument_start_inx, const std::string &function_name)
bitvector_typet char_type()
Definition: c_types.cpp:113
void do_strstr(goto_programt &dest, goto_programt::targett it, code_function_callt &call)
Assignment.
Definition: std_code.h:144
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
exprt buffer_size(const exprt &what)
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700
A generic base class for expressions that are predicates, i.e., boolean-typed.
Definition: std_expr.h:400
bool is_lvalue
Definition: symbol.h:71
array index operator
Definition: std_expr.h:1170
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
Definition: std_types.h:1051