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