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/string_constant.h>
24 #include <util/symbol_table.h>
25 
29 
30 predicate_exprt is_zero_string(const exprt &what, bool write)
31 {
32  predicate_exprt result("is_zero_string");
33  result.copy_to_operands(what);
34  result.set("lhs", write);
35  return result;
36 }
37 
39  const exprt &what,
40  bool write)
41 {
42  exprt result("zero_string_length", size_type());
43  result.copy_to_operands(what);
44  result.set("lhs", write);
45  return result;
46 }
47 
48 exprt buffer_size(const exprt &what)
49 {
50  exprt result("buffer_size", size_type());
51  result.copy_to_operands(what);
52  return result;
53 }
54 
56 {
57 public:
59  symbol_tablet &_symbol_table,
60  message_handlert &_message_handler):
61  messaget(_message_handler),
62  symbol_table(_symbol_table),
63  ns(_symbol_table)
64  {
65  }
66 
67  void operator()(goto_programt &dest);
68  void operator()(goto_functionst &dest);
69 
70 protected:
73 
74  void make_type(exprt &dest, const typet &type)
75  {
76  if(ns.follow(dest.type())!=ns.follow(type))
77  dest = typecast_exprt(dest, type);
78  }
79 
82 
83  // strings
84  void do_sprintf(
85  goto_programt &dest,
87  const code_function_callt &);
88  void do_snprintf(
89  goto_programt &dest,
91  const code_function_callt &);
92  void do_strcat(
93  goto_programt &dest,
95  const code_function_callt &);
96  void do_strncmp(
97  goto_programt &dest,
99  const code_function_callt &);
100  void do_strchr(
101  goto_programt &dest,
102  goto_programt::targett target,
103  const code_function_callt &);
104  void do_strrchr(
105  goto_programt &dest,
106  goto_programt::targett target,
107  const code_function_callt &);
108  void do_strstr(
109  goto_programt &dest,
110  goto_programt::targett target,
111  const code_function_callt &);
112  void do_strtok(
113  goto_programt &dest,
114  goto_programt::targett target,
115  const code_function_callt &);
116  void do_strerror(
117  goto_programt &dest,
119  const code_function_callt &);
120  void do_fscanf(
121  goto_programt &dest,
122  goto_programt::targett target,
123  const code_function_callt &);
124 
126  goto_programt &dest,
128  const code_function_callt::argumentst &arguments,
129  std::size_t format_string_inx,
130  std::size_t argument_start_inx,
131  const std::string &function_name);
132 
134  goto_programt &dest,
136  const code_function_callt::argumentst &arguments,
137  std::size_t format_string_inx,
138  std::size_t argument_start_inx,
139  const std::string &function_name);
140 
141  bool is_string_type(const typet &t) const
142  {
143  return
144  (t.id()==ID_pointer || t.id()==ID_array) &&
145  (t.subtype().id()==ID_signedbv || t.subtype().id()==ID_unsignedbv) &&
147  }
148 
149  void invalidate_buffer(
150  goto_programt &dest,
152  const exprt &buffer,
153  const typet &buf_type,
154  const mp_integer &limit);
155 };
156 
158  symbol_tablet &symbol_table,
159  message_handlert &message_handler,
160  goto_programt &dest)
161 {
162  string_instrumentationt string_instrumentation(symbol_table, message_handler);
164 }
165 
167  symbol_tablet &symbol_table,
168  message_handlert &message_handler,
169  goto_functionst &dest)
170 {
171  string_instrumentationt string_instrumentation(symbol_table, message_handler);
173 }
174 
176  goto_modelt &goto_model,
177  message_handlert &message_handler)
178 {
180  goto_model.symbol_table,
181  message_handler,
182  goto_model.goto_functions);
183 }
184 
186 {
187  for(goto_functionst::function_mapt::iterator
188  it=dest.function_map.begin();
189  it!=dest.function_map.end();
190  it++)
191  {
192  (*this)(it->second.body);
193  }
194 }
195 
197 {
199  instrument(dest, it);
200 }
201 
203  goto_programt &dest,
205 {
206  if(it->is_function_call())
207  do_function_call(dest, it);
208 }
209 
211  goto_programt &dest,
212  goto_programt::targett target)
213 {
214  const code_function_callt &call = target->get_function_call();
215  const 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  remove_skip(dest);
258  }
259 }
260 
262  goto_programt &dest,
263  goto_programt::targett target,
264  const code_function_callt &call)
265 {
266  const code_function_callt::argumentst &arguments=call.arguments();
267 
268  if(arguments.size()<2)
269  {
271  "sprintf expected to have two or more arguments",
272  target->source_location);
273  }
274 
275  goto_programt tmp;
276 
277  // in the abstract model, we have to report a
278  // (possibly false) positive here
279  goto_programt::targett assertion = tmp.add(
281  assertion->source_location.set_property_class("string");
282  assertion->source_location.set_comment("sprintf buffer overflow");
283 
284  do_format_string_read(tmp, target, arguments, 1, 2, "sprintf");
285 
286  if(call.lhs().is_not_nil())
287  {
288  exprt rhs =
290 
291  tmp.add(
292  goto_programt::make_assignment(call.lhs(), rhs, target->source_location));
293  }
294 
295  target->turn_into_skip();
296  dest.insert_before_swap(target, tmp);
297 }
298 
300  goto_programt &dest,
301  goto_programt::targett target,
302  const code_function_callt &call)
303 {
304  const code_function_callt::argumentst &arguments=call.arguments();
305 
306  if(arguments.size()<3)
307  {
309  "snprintf expected to have three or more arguments",
310  target->source_location);
311  }
312 
313  goto_programt tmp;
314 
315  exprt bufsize = buffer_size(arguments[0]);
316 
318  binary_relation_exprt(bufsize, ID_ge, arguments[1]),
319  target->source_location));
320  assertion->source_location.set_property_class("string");
321  assertion->source_location.set_comment("snprintf buffer overflow");
322 
323  do_format_string_read(tmp, target, arguments, 2, 3, "snprintf");
324 
325  if(call.lhs().is_not_nil())
326  {
327  exprt rhs =
329 
330  tmp.add(
331  goto_programt::make_assignment(call.lhs(), rhs, target->source_location));
332  }
333 
334  target->turn_into_skip();
335  dest.insert_before_swap(target, tmp);
336 }
337 
339  goto_programt &dest,
340  goto_programt::targett target,
341  const code_function_callt &call)
342 {
343  const code_function_callt::argumentst &arguments=call.arguments();
344 
345  if(arguments.size()<2)
346  {
348  "fscanf expected to have two or more arguments", target->source_location);
349  }
350 
351  goto_programt tmp;
352 
353  do_format_string_write(tmp, target, arguments, 1, 2, "fscanf");
354 
355  if(call.lhs().is_not_nil())
356  {
357  exprt rhs =
359 
360  tmp.add(
361  goto_programt::make_assignment(call.lhs(), rhs, target->source_location));
362  }
363 
364  target->turn_into_skip();
365  dest.insert_before_swap(target, tmp);
366 }
367 
369  goto_programt &dest,
371  const code_function_callt::argumentst &arguments,
372  std::size_t format_string_inx,
373  std::size_t argument_start_inx,
374  const std::string &function_name)
375 {
376  const exprt &format_arg=arguments[format_string_inx];
377 
378  if(
379  format_arg.id() == ID_address_of &&
380  to_address_of_expr(format_arg).object().id() == ID_index &&
381  to_index_expr(to_address_of_expr(format_arg).object()).array().id() ==
382  ID_string_constant)
383  {
386  to_index_expr(to_address_of_expr(format_arg).object()).array())
387  .get_value()));
388 
389  std::size_t args=0;
390 
391  for(const auto &token : token_list)
392  {
393  if(token.type==format_tokent::token_typet::STRING)
394  {
395  const exprt &arg=arguments[argument_start_inx+args];
396 
397  if(arg.id()!=ID_string_constant) // we don't need to check constants
398  {
399  exprt temp(arg);
400 
401  if(arg.type().id() != ID_pointer)
402  {
403  index_exprt index(temp, from_integer(0, index_type()));
404  temp=address_of_exprt(index);
405  }
406 
407  goto_programt::targett assertion =
409  is_zero_string(temp), target->source_location));
410  assertion->source_location.set_property_class("string");
411  std::string comment("zero-termination of string argument of ");
412  comment += function_name;
413  assertion->source_location.set_comment(comment);
414  }
415  }
416 
417  if(token.type!=format_tokent::token_typet::TEXT &&
418  token.type!=format_tokent::token_typet::UNKNOWN) args++;
419 
420  if(find(
421  token.flags.begin(),
422  token.flags.end(),
424  token.flags.end())
425  args++; // just eat the additional argument
426  }
427  }
428  else // non-const format string
429  {
431  is_zero_string(arguments[1]), target->source_location));
432  format_ass->source_location.set_property_class("string");
433  format_ass->source_location.set_comment(
434  "zero-termination of format string of " + function_name);
435 
436  for(std::size_t i=2; i<arguments.size(); i++)
437  {
438  const exprt &arg=arguments[i];
439 
440  if(arguments[i].id() != ID_string_constant && is_string_type(arg.type()))
441  {
442  exprt temp(arg);
443 
444  if(arg.type().id() != ID_pointer)
445  {
446  index_exprt index(temp, from_integer(0, index_type()));
447  temp=address_of_exprt(index);
448  }
449 
450  goto_programt::targett assertion =
452  is_zero_string(temp), target->source_location));
453  assertion->source_location.set_property_class("string");
454  assertion->source_location.set_comment(
455  "zero-termination of string argument of " + function_name);
456  }
457  }
458  }
459 }
460 
462  goto_programt &dest,
464  const code_function_callt::argumentst &arguments,
465  std::size_t format_string_inx,
466  std::size_t argument_start_inx,
467  const std::string &function_name)
468 {
469  const exprt &format_arg=arguments[format_string_inx];
470 
471  if(
472  format_arg.id() == ID_address_of &&
473  to_address_of_expr(format_arg).object().id() == ID_index &&
474  to_index_expr(to_address_of_expr(format_arg).object()).array().id() ==
475  ID_string_constant) // constant format
476  {
479  to_index_expr(to_address_of_expr(format_arg).object()).array())
480  .get_value()));
481 
482  std::size_t args=0;
483 
484  for(const auto &token : token_list)
485  {
486  if(find(
487  token.flags.begin(),
488  token.flags.end(),
490  token.flags.end())
491  continue; // asterisk means `ignore this'
492 
493  switch(token.type)
494  {
496  {
497  const exprt &argument=arguments[argument_start_inx+args];
498  const typet &arg_type = argument.type();
499 
500  exprt condition;
501 
502  if(token.field_width!=0)
503  {
504  exprt fwidth=from_integer(token.field_width, unsigned_int_type());
506  const plus_exprt fw_1(fwidth, one); // +1 for 0-char
507 
508  exprt fw_lt_bs;
509 
510  if(arg_type.id()==ID_pointer)
511  fw_lt_bs=
512  binary_relation_exprt(fw_1, ID_le, buffer_size(argument));
513  else
514  {
515  const index_exprt index(
516  argument, from_integer(0, unsigned_int_type()));
517  address_of_exprt aof(index);
518  fw_lt_bs=binary_relation_exprt(fw_1, ID_le, buffer_size(aof));
519  }
520 
521  condition = fw_lt_bs;
522  }
523  else
524  {
525  // this is a possible overflow.
526  condition = false_exprt();
527  }
528 
529  goto_programt::targett assertion = dest.add(
530  goto_programt::make_assertion(condition, target->source_location));
531  assertion->source_location.set_property_class("string");
532  std::string comment("format string buffer overflow in ");
533  comment += function_name;
534  assertion->source_location.set_comment(comment);
535 
536  // now kill the contents
538  dest, target, argument, arg_type, token.field_width);
539 
540  args++;
541  break;
542  }
545  {
546  // nothing
547  break;
548  }
553  {
554  const exprt &argument=arguments[argument_start_inx+args];
555  const dereference_exprt lhs{argument};
556 
557  side_effect_expr_nondett rhs(lhs.type(), target->source_location);
558 
559  dest.add(
561 
562  args++;
563  break;
564  }
565  }
566  }
567  }
568  else // non-const format string
569  {
570  for(std::size_t i=argument_start_inx; i<arguments.size(); i++)
571  {
572  const typet &arg_type = arguments[i].type();
573 
574  // Note: is_string_type() is a `good guess' here. Actually
575  // any of the pointers could point into an array. But it
576  // would suck if we had to invalidate all variables.
577  // Luckily this case isn't needed too often.
578  if(is_string_type(arg_type))
579  {
580  // as we don't know any field width for the %s that
581  // should be here during runtime, we just report a
582  // possibly false positive
583  goto_programt::targett assertion =
585  false_exprt(), target->source_location));
586  assertion->source_location.set_property_class("string");
587  std::string comment("format string buffer overflow in ");
588  comment += function_name;
589  assertion->source_location.set_comment(comment);
590 
591  invalidate_buffer(dest, target, arguments[i], arg_type, 0);
592  }
593  else
594  {
595  dereference_exprt lhs{arguments[i]};
596 
597  side_effect_expr_nondett rhs(lhs.type(), target->source_location);
598 
599  dest.add(
601  }
602  }
603  }
604 }
605 
607  goto_programt &,
609  const code_function_callt &)
610 {
611 }
612 
614  goto_programt &dest,
615  goto_programt::targett target,
616  const code_function_callt &call)
617 {
618  const code_function_callt::argumentst &arguments=call.arguments();
619 
620  if(arguments.size()!=2)
621  {
623  "strchr expected to have two arguments", target->source_location);
624  }
625 
626  goto_programt tmp;
627 
629  is_zero_string(arguments[0]), target->source_location));
630  assertion->source_location.set_property_class("string");
631  assertion->source_location.set_comment(
632  "zero-termination of string argument of strchr");
633 
634  target->turn_into_skip();
635  dest.insert_before_swap(target, tmp);
636 }
637 
639  goto_programt &dest,
640  goto_programt::targett target,
641  const code_function_callt &call)
642 {
643  const code_function_callt::argumentst &arguments=call.arguments();
644 
645  if(arguments.size()!=2)
646  {
648  "strrchr expected to have two arguments", target->source_location);
649  }
650 
651  goto_programt tmp;
652 
654  is_zero_string(arguments[0]), target->source_location));
655  assertion->source_location.set_property_class("string");
656  assertion->source_location.set_comment(
657  "zero-termination of string argument of strrchr");
658 
659  target->turn_into_skip();
660  dest.insert_before_swap(target, tmp);
661 }
662 
664  goto_programt &dest,
665  goto_programt::targett target,
666  const code_function_callt &call)
667 {
668  const code_function_callt::argumentst &arguments=call.arguments();
669 
670  if(arguments.size()!=2)
671  {
673  "strstr expected to have two arguments", target->source_location);
674  }
675 
676  goto_programt tmp;
677 
679  is_zero_string(arguments[0]), target->source_location));
680  assertion0->source_location.set_property_class("string");
681  assertion0->source_location.set_comment(
682  "zero-termination of 1st string argument of strstr");
683 
685  is_zero_string(arguments[1]), target->source_location));
686  assertion1->source_location.set_property_class("string");
687  assertion1->source_location.set_comment(
688  "zero-termination of 2nd string argument of strstr");
689 
690  target->turn_into_skip();
691  dest.insert_before_swap(target, tmp);
692 }
693 
695  goto_programt &dest,
696  goto_programt::targett target,
697  const code_function_callt &call)
698 {
699  const code_function_callt::argumentst &arguments=call.arguments();
700 
701  if(arguments.size()!=2)
702  {
704  "strtok expected to have two arguments", target->source_location);
705  }
706 
707  goto_programt tmp;
708 
710  is_zero_string(arguments[0]), 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 strtok");
714 
716  is_zero_string(arguments[1]), target->source_location));
717  assertion1->source_location.set_property_class("string");
718  assertion1->source_location.set_comment(
719  "zero-termination of 2nd string argument of strtok");
720 
721  target->turn_into_skip();
722  dest.insert_before_swap(target, tmp);
723 }
724 
726  goto_programt &dest,
728  const code_function_callt &call)
729 {
730  if(call.lhs().is_nil())
731  {
732  it->turn_into_skip();
733  return;
734  }
735 
736  irep_idt identifier_buf="__strerror_buffer";
737  irep_idt identifier_size="__strerror_buffer_size";
738 
739  if(symbol_table.symbols.find(identifier_buf)==symbol_table.symbols.end())
740  {
741  symbolt new_symbol_size;
742  new_symbol_size.base_name="__strerror_buffer_size";
743  new_symbol_size.pretty_name=new_symbol_size.base_name;
744  new_symbol_size.name=identifier_size;
745  new_symbol_size.mode=ID_C;
746  new_symbol_size.type=size_type();
747  new_symbol_size.is_state_var=true;
748  new_symbol_size.is_lvalue=true;
749  new_symbol_size.is_static_lifetime=true;
750 
751  array_typet type(char_type(), new_symbol_size.symbol_expr());
752  symbolt new_symbol_buf;
753  new_symbol_buf.mode=ID_C;
754  new_symbol_buf.type=type;
755  new_symbol_buf.is_state_var=true;
756  new_symbol_buf.is_lvalue=true;
757  new_symbol_buf.is_static_lifetime=true;
758  new_symbol_buf.base_name="__strerror_buffer";
759  new_symbol_buf.pretty_name=new_symbol_buf.base_name;
760  new_symbol_buf.name=new_symbol_buf.base_name;
761 
762  symbol_table.insert(std::move(new_symbol_buf));
763  symbol_table.insert(std::move(new_symbol_size));
764  }
765 
766  const symbolt &symbol_size=ns.lookup(identifier_size);
767  const symbolt &symbol_buf=ns.lookup(identifier_buf);
768 
769  goto_programt tmp;
770 
771  {
772  exprt nondet_size =
775  code_assignt(symbol_size.symbol_expr(), nondet_size),
776  it->source_location));
777 
780  symbol_size.symbol_expr(),
781  ID_notequal,
782  from_integer(0, symbol_size.type)),
783  it->source_location));
784  }
785 
786  // return a pointer to some magic buffer
787  index_exprt index(
788  symbol_buf.symbol_expr(),
789  from_integer(0, index_type()),
790  char_type());
791 
792  address_of_exprt ptr(index);
793 
794  // make that zero-terminated
796  is_zero_string(ptr, true), true_exprt(), it->source_location));
797 
798  // assign address
799  {
800  exprt rhs=ptr;
801  make_type(rhs, call.lhs().type());
803  code_assignt(call.lhs(), rhs), it->source_location));
804  }
805 
806  it->turn_into_skip();
807  dest.insert_before_swap(it, tmp);
808 }
809 
811  goto_programt &dest,
813  const exprt &buffer,
814  const typet &buf_type,
815  const mp_integer &limit)
816 {
817  irep_idt cntr_id="string_instrumentation::$counter";
818 
819  if(symbol_table.symbols.find(cntr_id)==symbol_table.symbols.end())
820  {
821  symbolt new_symbol;
822  new_symbol.base_name="$counter";
823  new_symbol.pretty_name=new_symbol.base_name;
824  new_symbol.name=cntr_id;
825  new_symbol.mode=ID_C;
826  new_symbol.type=size_type();
827  new_symbol.is_state_var=true;
828  new_symbol.is_lvalue=true;
829  new_symbol.is_static_lifetime=true;
830 
831  symbol_table.insert(std::move(new_symbol));
832  }
833 
834  const symbolt &cntr_sym=ns.lookup(cntr_id);
835 
836  // create a loop that runs over the buffer
837  // and invalidates every element
838 
840  cntr_sym.symbol_expr(),
841  from_integer(0, cntr_sym.type),
842  target->source_location));
843 
844  exprt bufp;
845 
846  if(buf_type.id()==ID_pointer)
847  bufp=buffer;
848  else
849  {
850  index_exprt index(
851  buffer, from_integer(0, index_type()), buf_type.subtype());
852  bufp=address_of_exprt(index);
853  }
854 
855  exprt condition;
856 
857  if(limit==0)
858  condition =
859  binary_relation_exprt(cntr_sym.symbol_expr(), ID_ge, buffer_size(bufp));
860  else
861  condition = binary_relation_exprt(
862  cntr_sym.symbol_expr(), ID_gt, from_integer(limit, unsigned_int_type()));
863 
864  goto_programt::targett check = dest.add(
866 
868  static_cast<const codet &>(get_nil_irep()),
869  target->source_location,
870  ASSIGN,
871  nil_exprt(),
872  {}));
873 
874  const plus_exprt plus(
875  cntr_sym.symbol_expr(), from_integer(1, unsigned_int_type()));
876 
878  cntr_sym.symbol_expr(), plus, target->source_location));
879 
880  dest.add(
882 
884  dest.add(goto_programt::make_skip(target->source_location));
885 
886  check->complete_goto(exit);
887 
888  const plus_exprt b_plus_i(bufp, cntr_sym.symbol_expr());
889  const dereference_exprt deref(b_plus_i, buf_type.subtype());
890 
891  const side_effect_expr_nondett nondet(
892  buf_type.subtype(), target->source_location);
893 
894  invalidate->code=code_assignt(deref, nondet);
895 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1201
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:150
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
string_instrumentationt::do_strcat
void do_strcat(goto_programt &dest, goto_programt::targett it, const code_function_callt &)
symbolt::is_state_var
bool is_state_var
Definition: symbol.h:62
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
typet::subtype
const typet & subtype() const
Definition: type.h:47
string_instrumentationt::do_fscanf
void do_fscanf(goto_programt &dest, goto_programt::targett target, const code_function_callt &)
Definition: string_instrumentation.cpp:338
string_instrumentationt::ns
namespacet ns
Definition: string_instrumentation.cpp:72
parse_format_string
format_token_listt parse_format_string(const std::string &arg_string)
Definition: format_strings.cpp:187
string_instrumentationt
Definition: string_instrumentation.cpp:56
arith_tools.h
string_instrumentationt::operator()
void operator()(goto_programt &dest)
Definition: string_instrumentation.cpp:196
format_tokent::token_typet::STRING
@ STRING
string_instrumentationt::string_instrumentationt
string_instrumentationt(symbol_tablet &_symbol_table, message_handlert &_message_handler)
Definition: string_instrumentation.cpp:58
typet
The type of an expression, extends irept.
Definition: type.h:29
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
string_instrumentationt::do_format_string_write
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)
Definition: string_instrumentation.cpp:461
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
remove_skip
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:85
is_zero_string
predicate_exprt is_zero_string(const exprt &what, bool write)
Definition: string_instrumentation.cpp:30
string_instrumentationt::do_snprintf
void do_snprintf(goto_programt &dest, goto_programt::targett target, const code_function_callt &)
Definition: string_instrumentation.cpp:299
string_instrumentationt::instrument
void instrument(goto_programt &dest, goto_programt::targett it)
Definition: string_instrumentation.cpp:202
invariant.h
to_string_constant
const string_constantt & to_string_constant(const exprt &expr)
Definition: string_constant.h:31
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:686
goto_model.h
Symbol Table + CFG.
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:881
format_strings.h
Format String Parser.
string_constant.h
string_instrumentationt::symbol_table
symbol_tablet & symbol_table
Definition: string_instrumentation.cpp:71
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
string_instrumentationt::do_strstr
void do_strstr(goto_programt &dest, goto_programt::targett target, const code_function_callt &)
Definition: string_instrumentation.cpp:663
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
string_instrumentationt::do_format_string_read
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)
Definition: string_instrumentation.cpp:368
configt::ansi_c
struct configt::ansi_ct ansi_c
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
string_instrumentation.h
String Abstraction.
string_instrumentationt::do_sprintf
void do_sprintf(goto_programt &dest, goto_programt::targett target, const code_function_callt &)
Definition: string_instrumentation.cpp:261
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1208
goto_programt::make_assignment
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:1024
goto_programt::make_goto
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:998
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
format_tokent::token_typet::POINTER
@ POINTER
configt::ansi_ct::char_width
std::size_t char_width
Definition: config.h:34
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
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
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
format_token_listt
std::list< format_tokent > format_token_listt
Definition: format_strings.h:87
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:893
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
string_instrumentation
void string_instrumentation(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
Definition: string_instrumentation.cpp:157
string_instrumentationt::do_strncmp
void do_strncmp(goto_programt &dest, goto_programt::targett it, const code_function_callt &)
Definition: string_instrumentation.cpp:606
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
format_tokent::token_typet::INT
@ INT
predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed.
Definition: std_expr.h:535
goto_programt::make_skip
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:851
string_instrumentationt::do_strtok
void do_strtok(goto_programt &dest, goto_programt::targett target, const code_function_callt &)
Definition: string_instrumentation.cpp:694
zero_string_length
exprt zero_string_length(const exprt &what, bool write)
Definition: string_instrumentation.cpp:38
typet::source_location
const source_locationt & source_location() const
Definition: type.h:71
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
nil_exprt
The NIL expression.
Definition: std_expr.h:3973
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
symbol_tablet::insert
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Definition: symbol_table.cpp:19
string_instrumentationt::do_strrchr
void do_strrchr(goto_programt &dest, goto_programt::targett target, const code_function_callt &)
Definition: string_instrumentation.cpp:638
unsigned_int_type
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:44
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
message_handlert
Definition: message.h:28
code_function_callt::argumentst
exprt::operandst argumentst
Definition: std_code.h:1192
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
std_code.h
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1228
config
configt config
Definition: config.cpp:24
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1041
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1945
string_instrumentationt::invalidate_buffer
void invalidate_buffer(goto_programt &dest, goto_programt::const_targett target, const exprt &buffer, const typet &buf_type, const mp_integer &limit)
Definition: string_instrumentation.cpp:810
ASSIGN
@ ASSIGN
Definition: goto_program.h:46
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
string_instrumentationt::do_strchr
void do_strchr(goto_programt &dest, goto_programt::targett target, const code_function_callt &)
Definition: string_instrumentation.cpp:613
format_tokent::token_typet::CHAR
@ CHAR
array_typet
Arrays with given size.
Definition: std_types.h:965
format_tokent::token_typet::UNKNOWN
@ UNKNOWN
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:725
string_instrumentationt::is_string_type
bool is_string_type(const typet &t) const
Definition: string_instrumentation.cpp:141
string_instrumentationt::do_function_call
void do_function_call(goto_programt &dest, goto_programt::targett target)
Definition: string_instrumentation.cpp:210
incorrect_source_program_exceptiont
Definition: string_instrumentation.h:23
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
string_instrumentationt::do_strerror
void do_strerror(goto_programt &dest, goto_programt::targett it, const code_function_callt &)
Definition: string_instrumentation.cpp:725
config.h
buffer_size
exprt buffer_size(const exprt &what)
Definition: string_instrumentation.cpp:48
format_tokent::token_typet::FLOAT
@ FLOAT
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:26
goto_programt::make_assumption
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:905
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
index_exprt
Array index operator.
Definition: std_expr.h:1293
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2786
format_tokent::token_typet::TEXT
@ TEXT
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:606
symbol_table.h
Author: Diffblue Ltd.
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
remove_skip.h
Program Transformation.
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
message.h
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
comment
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179
std_expr.h
API to expression classes.
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
c_types.h
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
code_function_callt::function
exprt & function()
Definition: std_code.h:1218
goto_programt::make_incomplete_goto
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:967
format_tokent::flag_typet::ASTERISK
@ ASTERISK
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1089
string_instrumentationt::make_type
void make_type(exprt &dest, const typet &type)
Definition: string_instrumentation.cpp:74
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35