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/pointer_expr.h>
20 #include <util/std_code.h>
21 #include <util/string_constant.h>
22 #include <util/symbol_table.h>
23 
27 
28 exprt is_zero_string(const exprt &what, bool write)
29 {
30  unary_exprt result{"is_zero_string", what, c_bool_type()};
31  result.copy_to_operands(what);
32  result.set("lhs", write);
33  return notequal_exprt{result, from_integer(0, c_bool_type())};
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:
56  explicit string_instrumentationt(symbol_tablet &_symbol_table)
57  : symbol_table(_symbol_table), ns(_symbol_table)
58  {
59  }
60 
61  void operator()(goto_programt &dest);
62  void operator()(goto_functionst &dest);
63 
64 protected:
67 
68  void make_type(exprt &dest, const typet &type)
69  {
70  if(ns.follow(dest.type())!=ns.follow(type))
71  dest = typecast_exprt(dest, type);
72  }
73 
76 
77  // strings
78  void do_sprintf(
79  goto_programt &dest,
81  const exprt &lhs,
82  const exprt::operandst &arguments);
83  void do_snprintf(
84  goto_programt &dest,
86  const exprt &lhs,
87  const exprt::operandst &arguments);
88  void do_strcat(
89  goto_programt &dest,
91  const exprt &lhs,
92  const exprt::operandst &arguments);
93  void do_strncmp(
94  goto_programt &dest,
96  const exprt &lhs,
97  const exprt::operandst &arguments);
98  void do_strchr(
99  goto_programt &dest,
100  goto_programt::targett target,
101  const exprt &lhs,
102  const exprt::operandst &arguments);
103  void do_strrchr(
104  goto_programt &dest,
105  goto_programt::targett target,
106  const exprt &lhs,
107  const exprt::operandst &arguments);
108  void do_strstr(
109  goto_programt &dest,
110  goto_programt::targett target,
111  const exprt &lhs,
112  const exprt::operandst &arguments);
113  void do_strtok(
114  goto_programt &dest,
115  goto_programt::targett target,
116  const exprt &lhs,
117  const exprt::operandst &arguments);
118  void do_strerror(
119  goto_programt &dest,
121  const exprt &lhs,
122  const exprt::operandst &arguments);
123  void do_fscanf(
124  goto_programt &dest,
125  goto_programt::targett target,
126  const exprt &lhs,
127  const exprt::operandst &arguments);
128 
130  goto_programt &dest,
132  const code_function_callt::argumentst &arguments,
133  std::size_t format_string_inx,
134  std::size_t argument_start_inx,
135  const std::string &function_name);
136 
138  goto_programt &dest,
140  const code_function_callt::argumentst &arguments,
141  std::size_t format_string_inx,
142  std::size_t argument_start_inx,
143  const std::string &function_name);
144 
145  bool is_string_type(const typet &t) const
146  {
147  return
148  (t.id()==ID_pointer || t.id()==ID_array) &&
149  (t.subtype().id()==ID_signedbv || t.subtype().id()==ID_unsignedbv) &&
151  }
152 
153  void invalidate_buffer(
154  goto_programt &dest,
156  const exprt &buffer,
157  const typet &buf_type,
158  const mp_integer &limit);
159 };
160 
162  symbol_tablet &symbol_table,
163  goto_programt &dest)
164 {
167 }
168 
170  symbol_tablet &symbol_table,
171  goto_functionst &dest)
172 {
175 }
176 
178 {
180  goto_model.symbol_table,
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  if(it->is_function_call())
206  do_function_call(dest, it);
207 }
208 
210  goto_programt &dest,
211  goto_programt::targett target)
212 {
213  const exprt &lhs = as_const(*target).call_lhs();
214  const exprt &function = as_const(*target).call_function();
215  const auto &arguments = as_const(*target).call_arguments();
216 
217  if(function.id()==ID_symbol)
218  {
219  const irep_idt &identifier=
220  to_symbol_expr(function).get_identifier();
221 
222  if(identifier=="strcoll")
223  {
224  }
225  else if(identifier=="strncmp")
226  do_strncmp(dest, target, lhs, arguments);
227  else if(identifier=="strxfrm")
228  {
229  }
230  else if(identifier=="strchr")
231  do_strchr(dest, target, lhs, arguments);
232  else if(identifier=="strcspn")
233  {
234  }
235  else if(identifier=="strpbrk")
236  {
237  }
238  else if(identifier=="strrchr")
239  do_strrchr(dest, target, lhs, arguments);
240  else if(identifier=="strspn")
241  {
242  }
243  else if(identifier=="strerror")
244  do_strerror(dest, target, lhs, arguments);
245  else if(identifier=="strstr")
246  do_strstr(dest, target, lhs, arguments);
247  else if(identifier=="strtok")
248  do_strtok(dest, target, lhs, arguments);
249  else if(identifier=="sprintf")
250  do_sprintf(dest, target, lhs, arguments);
251  else if(identifier=="snprintf")
252  do_snprintf(dest, target, lhs, arguments);
253  else if(identifier=="fscanf")
254  do_fscanf(dest, target, lhs, arguments);
255 
256  remove_skip(dest);
257  }
258 }
259 
261  goto_programt &dest,
262  goto_programt::targett target,
263  const exprt &lhs,
264  const exprt::operandst &arguments)
265 {
266  if(arguments.size()<2)
267  {
269  "sprintf expected to have two or more arguments",
270  target->source_location);
271  }
272 
273  goto_programt tmp;
274 
275  // in the abstract model, we have to report a
276  // (possibly false) positive here
277  goto_programt::targett assertion = tmp.add(
279  assertion->source_location.set_property_class("string");
280  assertion->source_location.set_comment("sprintf buffer overflow");
281 
282  do_format_string_read(tmp, target, arguments, 1, 2, "sprintf");
283 
284  if(lhs.is_not_nil())
285  {
286  exprt rhs = side_effect_expr_nondett(lhs.type(), target->source_location);
287 
288  tmp.add(goto_programt::make_assignment(lhs, rhs, target->source_location));
289  }
290 
291  target->turn_into_skip();
292  dest.insert_before_swap(target, tmp);
293 }
294 
296  goto_programt &dest,
297  goto_programt::targett target,
298  const exprt &lhs,
299  const exprt::operandst &arguments)
300 {
301  if(arguments.size()<3)
302  {
304  "snprintf expected to have three or more arguments",
305  target->source_location);
306  }
307 
308  goto_programt tmp;
309 
310  exprt bufsize = buffer_size(arguments[0]);
311 
313  binary_relation_exprt(bufsize, ID_ge, arguments[1]),
314  target->source_location));
315  assertion->source_location.set_property_class("string");
316  assertion->source_location.set_comment("snprintf buffer overflow");
317 
318  do_format_string_read(tmp, target, arguments, 2, 3, "snprintf");
319 
320  if(lhs.is_not_nil())
321  {
322  exprt rhs = side_effect_expr_nondett(lhs.type(), target->source_location);
323 
324  tmp.add(goto_programt::make_assignment(lhs, rhs, target->source_location));
325  }
326 
327  target->turn_into_skip();
328  dest.insert_before_swap(target, tmp);
329 }
330 
332  goto_programt &dest,
333  goto_programt::targett target,
334  const exprt &lhs,
335  const exprt::operandst &arguments)
336 {
337  if(arguments.size()<2)
338  {
340  "fscanf expected to have two or more arguments", target->source_location);
341  }
342 
343  goto_programt tmp;
344 
345  do_format_string_write(tmp, target, arguments, 1, 2, "fscanf");
346 
347  if(lhs.is_not_nil())
348  {
349  exprt rhs = side_effect_expr_nondett(lhs.type(), target->source_location);
350 
351  tmp.add(goto_programt::make_assignment(lhs, rhs, target->source_location));
352  }
353 
354  target->turn_into_skip();
355  dest.insert_before_swap(target, tmp);
356 }
357 
359  goto_programt &dest,
361  const code_function_callt::argumentst &arguments,
362  std::size_t format_string_inx,
363  std::size_t argument_start_inx,
364  const std::string &function_name)
365 {
366  const exprt &format_arg=arguments[format_string_inx];
367 
368  if(
369  format_arg.id() == ID_address_of &&
370  to_address_of_expr(format_arg).object().id() == ID_index &&
371  to_index_expr(to_address_of_expr(format_arg).object()).array().id() ==
372  ID_string_constant)
373  {
376  to_index_expr(to_address_of_expr(format_arg).object()).array())
377  .get_value()));
378 
379  std::size_t args=0;
380 
381  for(const auto &token : token_list)
382  {
383  if(token.type==format_tokent::token_typet::STRING)
384  {
385  const exprt &arg=arguments[argument_start_inx+args];
386 
387  if(arg.id()!=ID_string_constant) // we don't need to check constants
388  {
389  exprt temp(arg);
390 
391  if(arg.type().id() != ID_pointer)
392  {
393  index_exprt index(temp, from_integer(0, index_type()));
394  temp=address_of_exprt(index);
395  }
396 
397  goto_programt::targett assertion =
399  is_zero_string(temp), target->source_location));
400  assertion->source_location.set_property_class("string");
401  std::string comment("zero-termination of string argument of ");
402  comment += function_name;
403  assertion->source_location.set_comment(comment);
404  }
405  }
406 
407  if(token.type!=format_tokent::token_typet::TEXT &&
408  token.type!=format_tokent::token_typet::UNKNOWN) args++;
409 
410  if(find(
411  token.flags.begin(),
412  token.flags.end(),
414  token.flags.end())
415  args++; // just eat the additional argument
416  }
417  }
418  else // non-const format string
419  {
421  is_zero_string(arguments[1]), target->source_location));
422  format_ass->source_location.set_property_class("string");
423  format_ass->source_location.set_comment(
424  "zero-termination of format string of " + function_name);
425 
426  for(std::size_t i=2; i<arguments.size(); i++)
427  {
428  const exprt &arg=arguments[i];
429 
430  if(arguments[i].id() != ID_string_constant && is_string_type(arg.type()))
431  {
432  exprt temp(arg);
433 
434  if(arg.type().id() != ID_pointer)
435  {
436  index_exprt index(temp, from_integer(0, index_type()));
437  temp=address_of_exprt(index);
438  }
439 
440  goto_programt::targett assertion =
442  is_zero_string(temp), target->source_location));
443  assertion->source_location.set_property_class("string");
444  assertion->source_location.set_comment(
445  "zero-termination of string argument of " + function_name);
446  }
447  }
448  }
449 }
450 
452  goto_programt &dest,
454  const code_function_callt::argumentst &arguments,
455  std::size_t format_string_inx,
456  std::size_t argument_start_inx,
457  const std::string &function_name)
458 {
459  const exprt &format_arg=arguments[format_string_inx];
460 
461  if(
462  format_arg.id() == ID_address_of &&
463  to_address_of_expr(format_arg).object().id() == ID_index &&
464  to_index_expr(to_address_of_expr(format_arg).object()).array().id() ==
465  ID_string_constant) // constant format
466  {
469  to_index_expr(to_address_of_expr(format_arg).object()).array())
470  .get_value()));
471 
472  std::size_t args=0;
473 
474  for(const auto &token : token_list)
475  {
476  if(find(
477  token.flags.begin(),
478  token.flags.end(),
480  token.flags.end())
481  continue; // asterisk means `ignore this'
482 
483  switch(token.type)
484  {
486  {
487  const exprt &argument=arguments[argument_start_inx+args];
488  const typet &arg_type = argument.type();
489 
490  exprt condition;
491 
492  if(token.field_width!=0)
493  {
494  exprt fwidth=from_integer(token.field_width, unsigned_int_type());
496  const plus_exprt fw_1(fwidth, one); // +1 for 0-char
497 
498  exprt fw_lt_bs;
499 
500  if(arg_type.id()==ID_pointer)
501  fw_lt_bs=
502  binary_relation_exprt(fw_1, ID_le, buffer_size(argument));
503  else
504  {
505  const index_exprt index(
506  argument, from_integer(0, unsigned_int_type()));
507  address_of_exprt aof(index);
508  fw_lt_bs=binary_relation_exprt(fw_1, ID_le, buffer_size(aof));
509  }
510 
511  condition = fw_lt_bs;
512  }
513  else
514  {
515  // this is a possible overflow.
516  condition = false_exprt();
517  }
518 
519  goto_programt::targett assertion = dest.add(
520  goto_programt::make_assertion(condition, target->source_location));
521  assertion->source_location.set_property_class("string");
522  std::string comment("format string buffer overflow in ");
523  comment += function_name;
524  assertion->source_location.set_comment(comment);
525 
526  // now kill the contents
528  dest, target, argument, arg_type, token.field_width);
529 
530  args++;
531  break;
532  }
535  {
536  // nothing
537  break;
538  }
543  {
544  const exprt &argument=arguments[argument_start_inx+args];
545  const dereference_exprt lhs{argument};
546 
547  side_effect_expr_nondett rhs(lhs.type(), target->source_location);
548 
549  dest.add(
551 
552  args++;
553  break;
554  }
555  }
556  }
557  }
558  else // non-const format string
559  {
560  for(std::size_t i=argument_start_inx; i<arguments.size(); i++)
561  {
562  const typet &arg_type = arguments[i].type();
563 
564  // Note: is_string_type() is a `good guess' here. Actually
565  // any of the pointers could point into an array. But it
566  // would suck if we had to invalidate all variables.
567  // Luckily this case isn't needed too often.
568  if(is_string_type(arg_type))
569  {
570  // as we don't know any field width for the %s that
571  // should be here during runtime, we just report a
572  // possibly false positive
573  goto_programt::targett assertion =
575  false_exprt(), target->source_location));
576  assertion->source_location.set_property_class("string");
577  std::string comment("format string buffer overflow in ");
578  comment += function_name;
579  assertion->source_location.set_comment(comment);
580 
581  invalidate_buffer(dest, target, arguments[i], arg_type, 0);
582  }
583  else
584  {
585  dereference_exprt lhs{arguments[i]};
586 
587  side_effect_expr_nondett rhs(lhs.type(), target->source_location);
588 
589  dest.add(
591  }
592  }
593  }
594 }
595 
597  goto_programt &,
599  const exprt &,
600  const exprt::operandst &)
601 {
602 }
603 
605  goto_programt &dest,
606  goto_programt::targett target,
607  const exprt &lhs,
608  const exprt::operandst &arguments)
609 {
610  if(arguments.size()!=2)
611  {
613  "strchr expected to have two arguments", target->source_location);
614  }
615 
616  goto_programt tmp;
617 
619  is_zero_string(arguments[0]), target->source_location));
620  assertion->source_location.set_property_class("string");
621  assertion->source_location.set_comment(
622  "zero-termination of string argument of strchr");
623 
624  target->turn_into_skip();
625  dest.insert_before_swap(target, tmp);
626 }
627 
629  goto_programt &dest,
630  goto_programt::targett target,
631  const exprt &lhs,
632  const exprt::operandst &arguments)
633 {
634  if(arguments.size()!=2)
635  {
637  "strrchr expected to have two arguments", target->source_location);
638  }
639 
640  goto_programt tmp;
641 
643  is_zero_string(arguments[0]), target->source_location));
644  assertion->source_location.set_property_class("string");
645  assertion->source_location.set_comment(
646  "zero-termination of string argument of strrchr");
647 
648  target->turn_into_skip();
649  dest.insert_before_swap(target, tmp);
650 }
651 
653  goto_programt &dest,
654  goto_programt::targett target,
655  const exprt &lhs,
656  const exprt::operandst &arguments)
657 {
658  if(arguments.size()!=2)
659  {
661  "strstr expected to have two arguments", target->source_location);
662  }
663 
664  goto_programt tmp;
665 
667  is_zero_string(arguments[0]), target->source_location));
668  assertion0->source_location.set_property_class("string");
669  assertion0->source_location.set_comment(
670  "zero-termination of 1st string argument of strstr");
671 
673  is_zero_string(arguments[1]), target->source_location));
674  assertion1->source_location.set_property_class("string");
675  assertion1->source_location.set_comment(
676  "zero-termination of 2nd string argument of strstr");
677 
678  target->turn_into_skip();
679  dest.insert_before_swap(target, tmp);
680 }
681 
683  goto_programt &dest,
684  goto_programt::targett target,
685  const exprt &lhs,
686  const exprt::operandst &arguments)
687 {
688  if(arguments.size()!=2)
689  {
691  "strtok expected to have two arguments", target->source_location);
692  }
693 
694  goto_programt tmp;
695 
697  is_zero_string(arguments[0]), target->source_location));
698  assertion0->source_location.set_property_class("string");
699  assertion0->source_location.set_comment(
700  "zero-termination of 1st string argument of strtok");
701 
703  is_zero_string(arguments[1]), target->source_location));
704  assertion1->source_location.set_property_class("string");
705  assertion1->source_location.set_comment(
706  "zero-termination of 2nd string argument of strtok");
707 
708  target->turn_into_skip();
709  dest.insert_before_swap(target, tmp);
710 }
711 
713  goto_programt &dest,
715  const exprt &lhs,
716  const exprt::operandst &arguments)
717 {
718  if(lhs.is_nil())
719  {
720  it->turn_into_skip();
721  return;
722  }
723 
724  irep_idt identifier_buf="__strerror_buffer";
725  irep_idt identifier_size="__strerror_buffer_size";
726 
727  if(symbol_table.symbols.find(identifier_buf)==symbol_table.symbols.end())
728  {
729  symbolt new_symbol_size;
730  new_symbol_size.base_name="__strerror_buffer_size";
731  new_symbol_size.pretty_name=new_symbol_size.base_name;
732  new_symbol_size.name=identifier_size;
733  new_symbol_size.mode=ID_C;
734  new_symbol_size.type=size_type();
735  new_symbol_size.is_state_var=true;
736  new_symbol_size.is_lvalue=true;
737  new_symbol_size.is_static_lifetime=true;
738 
739  array_typet type(char_type(), new_symbol_size.symbol_expr());
740  symbolt new_symbol_buf;
741  new_symbol_buf.mode=ID_C;
742  new_symbol_buf.type=type;
743  new_symbol_buf.is_state_var=true;
744  new_symbol_buf.is_lvalue=true;
745  new_symbol_buf.is_static_lifetime=true;
746  new_symbol_buf.base_name="__strerror_buffer";
747  new_symbol_buf.pretty_name=new_symbol_buf.base_name;
748  new_symbol_buf.name=new_symbol_buf.base_name;
749 
750  symbol_table.insert(std::move(new_symbol_buf));
751  symbol_table.insert(std::move(new_symbol_size));
752  }
753 
754  const symbolt &symbol_size=ns.lookup(identifier_size);
755  const symbolt &symbol_buf=ns.lookup(identifier_buf);
756 
757  goto_programt tmp;
758 
759  {
760  exprt nondet_size =
763  code_assignt(symbol_size.symbol_expr(), nondet_size),
764  it->source_location));
765 
768  symbol_size.symbol_expr(),
769  ID_notequal,
770  from_integer(0, symbol_size.type)),
771  it->source_location));
772  }
773 
774  // return a pointer to some magic buffer
775  index_exprt index(
776  symbol_buf.symbol_expr(),
777  from_integer(0, index_type()),
778  char_type());
779 
780  address_of_exprt ptr(index);
781 
782  // make that zero-terminated
784  unary_exprt{"is_zero_string", ptr, c_bool_type()},
786  it->source_location));
787 
788  // assign address
789  {
790  exprt rhs=ptr;
791  make_type(rhs, lhs.type());
793  code_assignt(lhs, rhs), it->source_location));
794  }
795 
796  it->turn_into_skip();
797  dest.insert_before_swap(it, tmp);
798 }
799 
801  goto_programt &dest,
803  const exprt &buffer,
804  const typet &buf_type,
805  const mp_integer &limit)
806 {
807  irep_idt cntr_id="string_instrumentation::$counter";
808 
809  if(symbol_table.symbols.find(cntr_id)==symbol_table.symbols.end())
810  {
811  symbolt new_symbol;
812  new_symbol.base_name="$counter";
813  new_symbol.pretty_name=new_symbol.base_name;
814  new_symbol.name=cntr_id;
815  new_symbol.mode=ID_C;
816  new_symbol.type=size_type();
817  new_symbol.is_state_var=true;
818  new_symbol.is_lvalue=true;
819  new_symbol.is_static_lifetime=true;
820 
821  symbol_table.insert(std::move(new_symbol));
822  }
823 
824  const symbolt &cntr_sym=ns.lookup(cntr_id);
825 
826  // create a loop that runs over the buffer
827  // and invalidates every element
828 
830  cntr_sym.symbol_expr(),
831  from_integer(0, cntr_sym.type),
832  target->source_location));
833 
834  exprt bufp;
835 
836  if(buf_type.id()==ID_pointer)
837  bufp=buffer;
838  else
839  {
840  index_exprt index(
841  buffer, from_integer(0, index_type()), buf_type.subtype());
842  bufp=address_of_exprt(index);
843  }
844 
845  exprt condition;
846 
847  if(limit==0)
848  condition =
849  binary_relation_exprt(cntr_sym.symbol_expr(), ID_ge, buffer_size(bufp));
850  else
851  condition = binary_relation_exprt(
852  cntr_sym.symbol_expr(), ID_gt, from_integer(limit, unsigned_int_type()));
853 
854  goto_programt::targett check = dest.add(
856 
858  static_cast<const codet &>(get_nil_irep()),
859  target->source_location,
860  ASSIGN,
861  nil_exprt(),
862  {}));
863 
864  const plus_exprt plus(
865  cntr_sym.symbol_expr(), from_integer(1, unsigned_int_type()));
866 
868  cntr_sym.symbol_expr(), plus, target->source_location));
869 
870  dest.add(
872 
874  dest.add(goto_programt::make_skip(target->source_location));
875 
876  check->complete_goto(exit);
877 
878  const plus_exprt b_plus_i(bufp, cntr_sym.symbol_expr());
879  const dereference_exprt deref(b_plus_i, buf_type.subtype());
880 
881  const side_effect_expr_nondett nondet(
882  buf_type.subtype(), target->source_location);
883 
884  invalidate->code_nonconst() = code_assignt(deref, nondet);
885 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1260
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:129
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_snprintf
void do_snprintf(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
Definition: string_instrumentation.cpp:295
string_instrumentationt::do_strtok
void do_strtok(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
Definition: string_instrumentation.cpp:682
symbolt::is_state_var
bool is_state_var
Definition: symbol.h:62
symbol_tablet
The symbol table.
Definition: symbol_table.h:14
typet::subtype
const typet & subtype() const
Definition: type.h:47
mp_integer
BigInt mp_integer
Definition: smt_terms.h:12
string_instrumentationt::ns
namespacet ns
Definition: string_instrumentation.cpp:66
parse_format_string
format_token_listt parse_format_string(const std::string &arg_string)
Definition: format_strings.cpp:186
string_instrumentationt
Definition: string_instrumentation.cpp:54
arith_tools.h
string_instrumentationt::operator()
void operator()(goto_programt &dest)
Definition: string_instrumentation.cpp:195
format_tokent::token_typet::STRING
@ STRING
typet
The type of an expression, extends irept.
Definition: type.h:28
string_instrumentationt::do_strchr
void do_strchr(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
Definition: string_instrumentation.cpp:604
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
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:451
is_zero_string
exprt is_zero_string(const exprt &what, bool write)
Definition: string_instrumentation.cpp:28
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:628
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:86
string_instrumentationt::instrument
void instrument(goto_programt &dest, goto_programt::targett it)
Definition: string_instrumentation.cpp:201
c_bool_type
typet c_bool_type()
Definition: c_types.cpp:108
to_string_constant
const string_constantt & to_string_constant(const exprt &expr)
Definition: string_constant.h:41
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:753
goto_model.h
Symbol Table + CFG.
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:914
format_strings.h
Format String Parser.
string_constant.h
string_instrumentationt::symbol_table
symbol_tablet & symbol_table
Definition: string_instrumentation.cpp:65
exprt
Base class for all expressions.
Definition: expr.h:54
goto_modelt
Definition: goto_model.h:26
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:281
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
string_instrumentationt::do_strncmp
void do_strncmp(goto_programt &dest, goto_programt::targett it, const exprt &lhs, const exprt::operandst &arguments)
Definition: string_instrumentation.cpp:596
string_instrumentationt::do_strstr
void do_strstr(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
Definition: string_instrumentation.cpp:652
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:358
configt::ansi_c
struct configt::ansi_ct ansi_c
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: bitvector_types.h:32
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:29
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
string_instrumentation.h
String Abstraction.
string_instrumentationt::string_instrumentationt
string_instrumentationt(symbol_tablet &_symbol_table)
Definition: string_instrumentation.cpp:56
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:1082
goto_programt::make_goto
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:1056
notequal_exprt
Disequality.
Definition: std_expr.h:1283
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:113
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
string_instrumentationt::do_strerror
void do_strerror(goto_programt &dest, goto_programt::targett it, const exprt &lhs, const exprt::operandst &arguments)
Definition: string_instrumentation.cpp:712
format_token_listt
std::list< format_tokent > format_token_listt
Definition: format_strings.h:90
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:951
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
as_const
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
string_instrumentation
void string_instrumentation(symbol_tablet &symbol_table, goto_programt &dest)
Definition: string_instrumentation.cpp:161
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
format_tokent::token_typet::INT
@ INT
goto_programt::make_skip
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:909
zero_string_length
exprt zero_string_length(const exprt &what, bool write)
Definition: string_instrumentation.cpp:36
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:109
nil_exprt
The NIL expression.
Definition: std_expr.h:2820
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
pointer_expr.h
API to expression classes for Pointers.
symbol_tablet::insert
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Definition: symbol_table.cpp:17
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:189
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
code_function_callt::argumentst
exprt::operandst argumentst
Definition: std_code.h:1222
string_instrumentationt::do_sprintf
void do_sprintf(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
Definition: string_instrumentation.cpp:260
false_exprt
The Boolean constant false.
Definition: std_expr.h:2811
std_code.h
config
configt config
Definition: config.cpp:25
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:843
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1966
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:800
ASSIGN
@ ASSIGN
Definition: goto_program.h:44
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:25
format_tokent::token_typet::CHAR
@ CHAR
array_typet
Arrays with given size.
Definition: std_types.h:763
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:49
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
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:674
string_instrumentationt::is_string_type
bool is_string_type(const typet &t) const
Definition: string_instrumentation.cpp:145
string_instrumentationt::do_function_call
void do_function_call(goto_programt &dest, goto_programt::targett target)
Definition: string_instrumentation.cpp:209
incorrect_source_program_exceptiont
Definition: string_instrumentation.h:24
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:71
config.h
buffer_size
exprt buffer_size(const exprt &what)
Definition: string_instrumentation.cpp:46
format_tokent::token_typet::FLOAT
@ FLOAT
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:647
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:20
goto_programt::make_assumption
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:963
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:378
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
index_exprt
Array index operator.
Definition: std_expr.h:1328
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:341
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:673
symbol_table.h
Author: Diffblue Ltd.
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1866
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
remove_skip.h
Program Transformation.
string_instrumentationt::do_strrchr
void do_strrchr(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
Definition: string_instrumentation.cpp:628
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:293
true_exprt
The Boolean constant true.
Definition: std_expr.h:2802
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:178
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:230
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:646
string_instrumentationt::do_strcat
void do_strcat(goto_programt &dest, goto_programt::targett it, const exprt &lhs, const exprt::operandst &arguments)
goto_programt::make_incomplete_goto
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:1025
format_tokent::flag_typet::ASTERISK
@ ASTERISK
string_instrumentationt::make_type
void make_type(exprt &dest, const typet &type)
Definition: string_instrumentation.cpp:68
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33
string_instrumentationt::do_fscanf
void do_fscanf(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
Definition: string_instrumentation.cpp:331