cprover
goto_symex.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_symex.h"
13 
14 #include "expr_skeleton.h"
15 #include "symex_assign.h"
16 
17 #include <util/arith_tools.h>
18 #include <util/c_types.h>
19 #include <util/format_expr.h>
20 #include <util/fresh_symbol.h>
21 #include <util/mathematical_expr.h>
24 #include <util/simplify_expr.h>
25 #include <util/string_expr.h>
26 #include <util/string_utils.h>
27 
28 #include <climits>
29 
31 
33 {
35  simplify(expr, ns);
36 }
37 
39 {
40  exprt lhs = clean_expr(code.lhs(), state, true);
41  exprt rhs = clean_expr(code.rhs(), state, false);
42 
44  lhs.type() == rhs.type(), "assignments must be type consistent");
45 
47  log.debug(), [this, &lhs](messaget::mstreamt &mstream) {
48  mstream << "Assignment to " << format(lhs) << " ["
49  << pointer_offset_bits(lhs.type(), ns).value_or(0) << " bits]"
50  << messaget::eom;
51  });
52 
53  // rvalues present within the lhs (for example, "some_array[this_rvalue]" or
54  // "byte_extract <type> from an_lvalue offset this_rvalue") can affect whether
55  // we use field-sensitive symbols or not, so L2-rename them up front:
56  lhs = state.l2_rename_rvalues(lhs, ns);
57  do_simplify(lhs);
58  lhs = state.field_sensitivity.apply(ns, state, std::move(lhs), true);
59 
60  if(rhs.id() == ID_side_effect)
61  {
62  const side_effect_exprt &side_effect_expr = to_side_effect_expr(rhs);
63  const irep_idt &statement = side_effect_expr.get_statement();
64 
65  if(
66  statement == ID_cpp_new || statement == ID_cpp_new_array ||
67  statement == ID_java_new_array_data)
68  {
69  symex_cpp_new(state, lhs, side_effect_expr);
70  }
71  else if(statement == ID_allocate)
72  symex_allocate(state, lhs, side_effect_expr);
73  else if(statement == ID_va_start)
74  symex_va_start(state, lhs, side_effect_expr);
75  else
77  }
78  else
79  {
81 
82  // Let's hide return value assignments.
83  if(
84  lhs.id() == ID_symbol &&
85  id2string(to_symbol_expr(lhs).get_identifier()).find("#return_value!") !=
86  std::string::npos)
87  {
89  }
90 
91  // We hide if we are in a hidden function.
92  if(state.call_stack().top().hidden_function)
94 
95  // We hide if we are executing a hidden instruction.
96  if(state.source.pc->source_location.get_hide())
98 
100  state, assignment_type, ns, symex_config, target};
101 
102  // Try to constant propagate potential side effects of the assignment, when
103  // simplification is turned on and there is one thread only. Constant
104  // propagation is only sound for sequential code as here we do not take into
105  // account potential writes from other threads when propagating the values.
106  if(symex_config.simplify_opt && state.threads.size() <= 1)
107  {
109  state, symex_assign, lhs, rhs))
110  return;
111  }
112 
113  exprt::operandst lhs_if_then_else_conditions;
114  symex_assign.assign_rec(
115  lhs, expr_skeletont{}, rhs, lhs_if_then_else_conditions);
116  }
117 }
118 
126 static std::string get_alnum_string(const array_exprt &char_array)
127 {
128  const auto &ibv_type =
130 
131  const std::size_t n_bits = ibv_type.get_width();
132  CHECK_RETURN(n_bits % 8 == 0);
133 
134  static_assert(CHAR_BIT == 8, "bitwidth of char assumed to be 8");
135 
136  const std::size_t n_chars = n_bits / 8;
137 
138  INVARIANT(
139  sizeof(std::size_t) >= n_chars,
140  "size_t shall be large enough to represent a character");
141 
142  std::string result;
143 
144  for(const auto &c : char_array.operands())
145  {
146  const std::size_t c_val = numeric_cast_v<std::size_t>(to_constant_expr(c));
147 
148  for(std::size_t i = 0; i < n_chars; i++)
149  {
150  const char c_chunk = static_cast<char>((c_val >> (i * 8)) & 0xff);
151  result.push_back(c_chunk);
152  }
153  }
154 
155  return escape_non_alnum(result);
156 }
157 
159  statet &state,
160  symex_assignt &symex_assign,
161  const exprt &lhs,
162  const exprt &rhs)
163 {
164  if(rhs.id() == ID_function_application)
165  {
167 
168  if(f_l1.function().id() == ID_symbol)
169  {
170  const irep_idt &func_id =
172 
173  if(func_id == ID_cprover_string_concat_func)
174  {
175  return constant_propagate_string_concat(state, symex_assign, f_l1);
176  }
177  else if(func_id == ID_cprover_string_empty_string_func)
178  {
179  // constant propagating the empty string always succeeds as it does
180  // not depend on potentially non-constant inputs
182  return true;
183  }
184  else if(func_id == ID_cprover_string_substring_func)
185  {
187  }
188  else if(
189  func_id == ID_cprover_string_of_int_func ||
190  func_id == ID_cprover_string_of_long_func)
191  {
193  }
194  else if(func_id == ID_cprover_string_delete_char_at_func)
195  {
196  return constant_propagate_delete_char_at(state, symex_assign, f_l1);
197  }
198  else if(func_id == ID_cprover_string_delete_func)
199  {
200  return constant_propagate_delete(state, symex_assign, f_l1);
201  }
202  else if(func_id == ID_cprover_string_set_length_func)
203  {
204  return constant_propagate_set_length(state, symex_assign, f_l1);
205  }
206  else if(func_id == ID_cprover_string_char_set_func)
207  {
208  return constant_propagate_set_char_at(state, symex_assign, f_l1);
209  }
210  else if(func_id == ID_cprover_string_trim_func)
211  {
212  return constant_propagate_trim(state, symex_assign, f_l1);
213  }
214  else if(func_id == ID_cprover_string_to_lower_case_func)
215  {
216  return constant_propagate_case_change(state, symex_assign, f_l1, false);
217  }
218  else if(func_id == ID_cprover_string_to_upper_case_func)
219  {
220  return constant_propagate_case_change(state, symex_assign, f_l1, true);
221  }
222  else if(func_id == ID_cprover_string_replace_func)
223  {
224  return constant_propagate_replace(state, symex_assign, f_l1);
225  }
226  }
227  }
228 
229  return false;
230 }
231 
233  statet &state,
234  symex_assignt &symex_assign,
235  const ssa_exprt &length,
236  const constant_exprt &new_length,
237  const ssa_exprt &char_array,
238  const array_exprt &new_char_array)
239 {
240  // We need to make sure that the length of the previous array isn't
241  // unconstrained, otherwise it could be arbitrarily large which causes
242  // invalid traces
243  symex_assume(state, equal_exprt{length, from_integer(0, length.type())});
244 
245  // assign length of string
246  symex_assign.assign_symbol(length, expr_skeletont{}, new_length, {});
247 
248  const std::string aux_symbol_name =
249  get_alnum_string(new_char_array) + "_constant_char_array";
250 
251  const bool string_constant_exists =
252  state.symbol_table.has_symbol(aux_symbol_name);
253 
254  const symbolt &aux_symbol =
255  string_constant_exists
256  ? state.symbol_table.lookup_ref(aux_symbol_name)
258  state, symex_assign, aux_symbol_name, char_array, new_char_array);
259 
260  INVARIANT(
261  aux_symbol.value == new_char_array,
262  "symbol shall have value derived from char array content");
263 
264  const address_of_exprt string_data(
265  index_exprt(aux_symbol.symbol_expr(), from_integer(0, index_type())));
266 
267  symex_assign.assign_symbol(char_array, expr_skeletont{}, string_data, {});
268 
269  if(!string_constant_exists)
270  {
272  state, symex_assign, new_char_array, string_data);
273  }
274 }
275 
277  statet &state,
278  symex_assignt &symex_assign,
279  const std::string &aux_symbol_name,
280  const ssa_exprt &char_array,
281  const array_exprt &new_char_array)
282 {
283  array_typet new_char_array_type = new_char_array.type();
284  new_char_array_type.set(ID_C_constant, true);
285 
286  symbolt &new_aux_symbol = get_fresh_aux_symbol(
287  new_char_array_type,
288  "",
289  aux_symbol_name,
291  ns.lookup(to_symbol_expr(char_array.get_original_expr())).mode,
292  ns,
293  state.symbol_table);
294 
295  CHECK_RETURN(new_aux_symbol.is_state_var);
296  CHECK_RETURN(new_aux_symbol.is_lvalue);
297 
298  new_aux_symbol.is_static_lifetime = true;
299  new_aux_symbol.is_file_local = false;
300  new_aux_symbol.is_thread_local = false;
301 
302  new_aux_symbol.value = new_char_array;
303 
304  const exprt arr = state.rename(new_aux_symbol.symbol_expr(), ns).get();
305 
306  symex_assign.assign_symbol(
307  to_ssa_expr(arr).get_l1_object(), expr_skeletont{}, new_char_array, {});
308 
309  return new_aux_symbol;
310 }
311 
313  statet &state,
314  symex_assignt &symex_assign,
315  const array_exprt &new_char_array,
316  const address_of_exprt &string_data)
317 {
318  const symbolt &function_symbol =
319  ns.lookup(ID_cprover_associate_array_to_pointer_func);
320 
321  const function_application_exprt array_to_pointer_app{
322  function_symbol.symbol_expr(), {new_char_array, string_data}};
323 
324  const symbolt &return_symbol = get_fresh_aux_symbol(
325  to_mathematical_function_type(function_symbol.type).codomain(),
326  "",
327  "return_value",
329  function_symbol.mode,
330  ns,
331  state.symbol_table);
332 
333  const ssa_exprt ssa_expr(return_symbol.symbol_expr());
334 
335  symex_assign.assign_symbol(
336  ssa_expr, expr_skeletont{}, array_to_pointer_app, {});
337 }
338 
341  const statet &state,
342  const exprt &content)
343 {
344  if(content.id() != ID_symbol)
345  {
346  return {};
347  }
348 
349  const auto s_pointer_opt =
350  state.propagation.find(to_symbol_expr(content).get_identifier());
351 
352  if(!s_pointer_opt)
353  {
354  return {};
355  }
356 
357  return try_get_string_data_array(s_pointer_opt->get(), ns);
358 }
359 
362 {
363  if(expr.id() != ID_symbol)
364  {
365  return {};
366  }
367 
368  const auto constant_expr_opt =
369  state.propagation.find(to_symbol_expr(expr).get_identifier());
370 
371  if(!constant_expr_opt || constant_expr_opt->get().id() != ID_constant)
372  {
373  return {};
374  }
375 
377  to_constant_expr(constant_expr_opt->get()));
378 }
379 
381  statet &state,
382  symex_assignt &symex_assign,
383  const function_application_exprt &f_l1)
384 {
385  const auto &f_type = to_mathematical_function_type(f_l1.function().type());
386  const auto &length_type = f_type.domain().at(0);
387  const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
388 
389  const constant_exprt length = from_integer(0, length_type);
390 
391  const array_typet char_array_type(char_type, length);
392 
394  f_l1.arguments().size() >= 2,
395  "empty string primitive requires two output arguments");
396 
397  const array_exprt char_array({}, char_array_type);
398 
400  state,
401  symex_assign,
402  to_ssa_expr(f_l1.arguments().at(0)),
403  length,
404  to_ssa_expr(f_l1.arguments().at(1)),
405  char_array);
406 }
407 
409  statet &state,
410  symex_assignt &symex_assign,
411  const function_application_exprt &f_l1)
412 {
413  const auto &f_type = to_mathematical_function_type(f_l1.function().type());
414  const auto &length_type = f_type.domain().at(0);
415  const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
416 
417  const refined_string_exprt &s1 = to_string_expr(f_l1.arguments().at(2));
418  const auto s1_data_opt = try_evaluate_constant_string(state, s1.content());
419 
420  if(!s1_data_opt)
421  return false;
422 
423  const array_exprt &s1_data = s1_data_opt->get();
424 
425  const refined_string_exprt &s2 = to_string_expr(f_l1.arguments().at(3));
426  const auto s2_data_opt = try_evaluate_constant_string(state, s2.content());
427 
428  if(!s2_data_opt)
429  return false;
430 
431  const array_exprt &s2_data = s2_data_opt->get();
432 
433  const std::size_t new_size =
434  s1_data.operands().size() + s2_data.operands().size();
435 
436  const constant_exprt new_char_array_length =
437  from_integer(new_size, length_type);
438 
439  const array_typet new_char_array_type(char_type, new_char_array_length);
440 
441  exprt::operandst operands(s1_data.operands());
442  operands.insert(
443  operands.end(), s2_data.operands().begin(), s2_data.operands().end());
444 
445  const array_exprt new_char_array(std::move(operands), new_char_array_type);
446 
448  state,
449  symex_assign,
450  to_ssa_expr(f_l1.arguments().at(0)),
451  new_char_array_length,
452  to_ssa_expr(f_l1.arguments().at(1)),
453  new_char_array);
454 
455  return true;
456 }
457 
459  statet &state,
460  symex_assignt &symex_assign,
461  const function_application_exprt &f_l1)
462 {
463  const std::size_t num_operands = f_l1.arguments().size();
464 
465  PRECONDITION(num_operands >= 4);
466  PRECONDITION(num_operands <= 5);
467 
468  const auto &f_type = to_mathematical_function_type(f_l1.function().type());
469  const auto &length_type = f_type.domain().at(0);
470  const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
471 
472  const refined_string_exprt &s = to_string_expr(f_l1.arguments().at(2));
473  const auto s_data_opt = try_evaluate_constant_string(state, s.content());
474 
475  if(!s_data_opt)
476  return false;
477 
478  const array_exprt &s_data = s_data_opt->get();
479 
480  mp_integer end_index;
481 
482  if(num_operands == 5)
483  {
484  const auto end_index_expr_opt =
485  try_evaluate_constant(state, f_l1.arguments().at(4));
486 
487  if(!end_index_expr_opt)
488  {
489  return false;
490  }
491 
492  end_index =
493  numeric_cast_v<mp_integer>(to_constant_expr(*end_index_expr_opt));
494 
495  if(end_index < 0 || end_index > s_data.operands().size())
496  {
497  return false;
498  }
499  }
500  else
501  {
502  end_index = s_data.operands().size();
503  }
504 
505  const auto start_index_expr_opt =
506  try_evaluate_constant(state, f_l1.arguments().at(3));
507 
508  if(!start_index_expr_opt)
509  {
510  return false;
511  }
512 
513  const mp_integer start_index =
514  numeric_cast_v<mp_integer>(to_constant_expr(*start_index_expr_opt));
515 
516  if(start_index < 0 || start_index > end_index)
517  {
518  return false;
519  }
520 
521  const constant_exprt new_char_array_length =
522  from_integer(end_index - start_index, length_type);
523 
524  const array_typet new_char_array_type(char_type, new_char_array_length);
525 
526  exprt::operandst operands(
527  std::next(
528  s_data.operands().begin(), numeric_cast_v<std::size_t>(start_index)),
529  std::next(
530  s_data.operands().begin(), numeric_cast_v<std::size_t>(end_index)));
531 
532  const array_exprt new_char_array(std::move(operands), new_char_array_type);
533 
535  state,
536  symex_assign,
537  to_ssa_expr(f_l1.arguments().at(0)),
538  new_char_array_length,
539  to_ssa_expr(f_l1.arguments().at(1)),
540  new_char_array);
541 
542  return true;
543 }
544 
546  statet &state,
547  symex_assignt &symex_assign,
548  const function_application_exprt &f_l1)
549 {
550  // The function application expression f_l1 takes the following arguments:
551  // - result string length (output parameter)
552  // - result string data array (output parameter)
553  // - integer to convert to a string
554  // - radix (optional, default 10)
555  const std::size_t num_operands = f_l1.arguments().size();
556 
557  PRECONDITION(num_operands >= 3);
558  PRECONDITION(num_operands <= 4);
559 
560  const auto &f_type = to_mathematical_function_type(f_l1.function().type());
561  const auto &length_type = f_type.domain().at(0);
562  const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
563 
564  const auto &integer_opt =
565  try_evaluate_constant(state, f_l1.arguments().at(2));
566 
567  if(!integer_opt)
568  {
569  return false;
570  }
571 
572  const mp_integer integer = numeric_cast_v<mp_integer>(integer_opt->get());
573 
574  unsigned base = 10;
575 
576  if(num_operands == 4)
577  {
578  const auto &base_constant_opt =
579  try_evaluate_constant(state, f_l1.arguments().at(3));
580 
581  if(!base_constant_opt)
582  {
583  return false;
584  }
585 
586  const auto base_opt = numeric_cast<unsigned>(base_constant_opt->get());
587 
588  if(!base_opt)
589  {
590  return false;
591  }
592 
593  base = *base_opt;
594  }
595 
596  std::string s = integer2string(integer, base);
597 
598  const constant_exprt new_char_array_length =
599  from_integer(s.length(), length_type);
600 
601  const array_typet new_char_array_type(char_type, new_char_array_length);
602 
603  exprt::operandst operands;
604 
605  std::transform(
606  s.begin(),
607  s.end(),
608  std::back_inserter(operands),
609  [&char_type](const char c) { return from_integer(tolower(c), char_type); });
610 
611  const array_exprt new_char_array(std::move(operands), new_char_array_type);
612 
614  state,
615  symex_assign,
616  to_ssa_expr(f_l1.arguments().at(0)),
617  new_char_array_length,
618  to_ssa_expr(f_l1.arguments().at(1)),
619  new_char_array);
620 
621  return true;
622 }
623 
625  statet &state,
626  symex_assignt &symex_assign,
627  const function_application_exprt &f_l1)
628 {
629  // The function application expression f_l1 takes the following arguments:
630  // - result string length (output parameter)
631  // - result string data array (output parameter)
632  // - string to delete char from
633  // - index of char to delete
634  PRECONDITION(f_l1.arguments().size() == 4);
635 
636  const auto &f_type = to_mathematical_function_type(f_l1.function().type());
637  const auto &length_type = f_type.domain().at(0);
638  const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
639 
640  const refined_string_exprt &s = to_string_expr(f_l1.arguments().at(2));
641  const auto s_data_opt = try_evaluate_constant_string(state, s.content());
642 
643  if(!s_data_opt)
644  {
645  return false;
646  }
647 
648  const array_exprt &s_data = s_data_opt->get();
649 
650  const auto &index_opt = try_evaluate_constant(state, f_l1.arguments().at(3));
651 
652  if(!index_opt)
653  {
654  return false;
655  }
656 
657  const mp_integer index = numeric_cast_v<mp_integer>(index_opt->get());
658 
659  if(index < 0 || index >= s_data.operands().size())
660  {
661  return false;
662  }
663 
664  const constant_exprt new_char_array_length =
665  from_integer(s_data.operands().size() - 1, length_type);
666 
667  const array_typet new_char_array_type(char_type, new_char_array_length);
668 
669  exprt::operandst operands;
670  operands.reserve(s_data.operands().size() - 1);
671 
672  const std::size_t i = numeric_cast_v<std::size_t>(index);
673 
674  operands.insert(
675  operands.end(),
676  s_data.operands().begin(),
677  std::next(s_data.operands().begin(), i));
678 
679  operands.insert(
680  operands.end(),
681  std::next(s_data.operands().begin(), i + 1),
682  s_data.operands().end());
683 
684  const array_exprt new_char_array(std::move(operands), new_char_array_type);
685 
687  state,
688  symex_assign,
689  to_ssa_expr(f_l1.arguments().at(0)),
690  new_char_array_length,
691  to_ssa_expr(f_l1.arguments().at(1)),
692  new_char_array);
693 
694  return true;
695 }
696 
698  statet &state,
699  symex_assignt &symex_assign,
700  const function_application_exprt &f_l1)
701 {
702  // The function application expression f_l1 takes the following arguments:
703  // - result string length (output parameter)
704  // - result string data array (output parameter)
705  // - string to delete substring from
706  // - index of start of substring to delete (inclusive)
707  // - index of end of substring to delete (exclusive)
708  PRECONDITION(f_l1.arguments().size() == 5);
709 
710  const auto &f_type = to_mathematical_function_type(f_l1.function().type());
711  const auto &length_type = f_type.domain().at(0);
712  const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
713 
714  const refined_string_exprt &s = to_string_expr(f_l1.arguments().at(2));
715  const auto s_data_opt = try_evaluate_constant_string(state, s.content());
716 
717  if(!s_data_opt)
718  {
719  return false;
720  }
721 
722  const array_exprt &s_data = s_data_opt->get();
723 
724  const auto &start_opt = try_evaluate_constant(state, f_l1.arguments().at(3));
725 
726  if(!start_opt)
727  {
728  return false;
729  }
730 
731  const mp_integer start = numeric_cast_v<mp_integer>(start_opt->get());
732 
733  if(start < 0 || start > s_data.operands().size())
734  {
735  return false;
736  }
737 
738  const auto &end_opt = try_evaluate_constant(state, f_l1.arguments().at(4));
739 
740  if(!end_opt)
741  {
742  return false;
743  }
744 
745  const mp_integer end = numeric_cast_v<mp_integer>(end_opt->get());
746 
747  if(start > end)
748  {
749  return false;
750  }
751 
752  const std::size_t start_index = numeric_cast_v<std::size_t>(start);
753 
754  const std::size_t end_index =
755  std::min(numeric_cast_v<std::size_t>(end), s_data.operands().size());
756 
757  const std::size_t new_size =
758  s_data.operands().size() - end_index + start_index;
759 
760  const constant_exprt new_char_array_length =
761  from_integer(new_size, length_type);
762 
763  const array_typet new_char_array_type(char_type, new_char_array_length);
764 
765  exprt::operandst operands;
766  operands.reserve(new_size);
767 
768  operands.insert(
769  operands.end(),
770  s_data.operands().begin(),
771  std::next(s_data.operands().begin(), start_index));
772 
773  operands.insert(
774  operands.end(),
775  std::next(s_data.operands().begin(), end_index),
776  s_data.operands().end());
777 
778  const array_exprt new_char_array(std::move(operands), new_char_array_type);
779 
781  state,
782  symex_assign,
783  to_ssa_expr(f_l1.arguments().at(0)),
784  new_char_array_length,
785  to_ssa_expr(f_l1.arguments().at(1)),
786  new_char_array);
787 
788  return true;
789 }
790 
792  statet &state,
793  symex_assignt &symex_assign,
794  const function_application_exprt &f_l1)
795 {
796  // The function application expression f_l1 takes the following arguments:
797  // - result string length (output parameter)
798  // - result string data array (output parameter)
799  // - current string
800  // - new length of the string
801  PRECONDITION(f_l1.arguments().size() == 4);
802 
803  const auto &f_type = to_mathematical_function_type(f_l1.function().type());
804  const auto &length_type = f_type.domain().at(0);
805  const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
806 
807  const auto &new_length_opt =
808  try_evaluate_constant(state, f_l1.arguments().at(3));
809 
810  if(!new_length_opt)
811  {
812  return false;
813  }
814 
815  const mp_integer new_length =
816  numeric_cast_v<mp_integer>(new_length_opt->get());
817 
818  if(new_length < 0)
819  {
820  return false;
821  }
822 
823  const std::size_t new_size = numeric_cast_v<std::size_t>(new_length);
824 
825  const constant_exprt new_char_array_length =
826  from_integer(new_size, length_type);
827 
828  const array_typet new_char_array_type(char_type, new_char_array_length);
829 
830  exprt::operandst operands;
831 
832  if(new_size != 0)
833  {
834  operands.reserve(new_size);
835 
836  const refined_string_exprt &s = to_string_expr(f_l1.arguments().at(2));
837  const auto s_data_opt = try_evaluate_constant_string(state, s.content());
838 
839  if(!s_data_opt)
840  {
841  return false;
842  }
843 
844  const array_exprt &s_data = s_data_opt->get();
845 
846  operands.insert(
847  operands.end(),
848  s_data.operands().begin(),
849  std::next(
850  s_data.operands().begin(),
851  std::min(new_size, s_data.operands().size())));
852 
853  operands.insert(
854  operands.end(),
855  new_size - std::min(new_size, s_data.operands().size()),
856  from_integer(0, char_type));
857  }
858 
859  const array_exprt new_char_array(std::move(operands), new_char_array_type);
860 
862  state,
863  symex_assign,
864  to_ssa_expr(f_l1.arguments().at(0)),
865  new_char_array_length,
866  to_ssa_expr(f_l1.arguments().at(1)),
867  new_char_array);
868 
869  return true;
870 }
871 
873  statet &state,
874  symex_assignt &symex_assign,
875  const function_application_exprt &f_l1)
876 {
877  // The function application expression f_l1 takes the following arguments:
878  // - result string length (output parameter)
879  // - result string data array (output parameter)
880  // - current string
881  // - index of char to set
882  // - new char
883  PRECONDITION(f_l1.arguments().size() == 5);
884 
885  const auto &f_type = to_mathematical_function_type(f_l1.function().type());
886  const auto &length_type = f_type.domain().at(0);
887  const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
888 
889  const refined_string_exprt &s = to_string_expr(f_l1.arguments().at(2));
890  const auto s_data_opt = try_evaluate_constant_string(state, s.content());
891 
892  if(!s_data_opt)
893  {
894  return false;
895  }
896 
897  array_exprt s_data = s_data_opt->get();
898 
899  const auto &index_opt = try_evaluate_constant(state, f_l1.arguments().at(3));
900 
901  if(!index_opt)
902  {
903  return false;
904  }
905 
906  const mp_integer index = numeric_cast_v<mp_integer>(index_opt->get());
907 
908  if(index < 0 || index >= s_data.operands().size())
909  {
910  return false;
911  }
912 
913  const auto &new_char_opt =
914  try_evaluate_constant(state, f_l1.arguments().at(4));
915 
916  if(!new_char_opt)
917  {
918  return false;
919  }
920 
921  const constant_exprt new_char_array_length =
922  from_integer(s_data.operands().size(), length_type);
923 
924  const array_typet new_char_array_type(char_type, new_char_array_length);
925 
926  s_data.operands()[numeric_cast_v<std::size_t>(index)] = new_char_opt->get();
927 
928  const array_exprt new_char_array(
929  std::move(s_data.operands()), new_char_array_type);
930 
932  state,
933  symex_assign,
934  to_ssa_expr(f_l1.arguments().at(0)),
935  new_char_array_length,
936  to_ssa_expr(f_l1.arguments().at(1)),
937  new_char_array);
938 
939  return true;
940 }
941 
943  statet &state,
944  symex_assignt &symex_assign,
945  const function_application_exprt &f_l1,
946  bool to_upper)
947 {
948  const auto &f_type = to_mathematical_function_type(f_l1.function().type());
949  const auto &length_type = f_type.domain().at(0);
950  const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
951 
952  const refined_string_exprt &s = to_string_expr(f_l1.arguments().at(2));
953  const auto s_data_opt = try_evaluate_constant_string(state, s.content());
954 
955  if(!s_data_opt)
956  return false;
957 
958  array_exprt string_data = s_data_opt->get();
959 
960  auto &operands = string_data.operands();
961  for(auto &operand : operands)
962  {
963  auto &constant_value = to_constant_expr(operand);
964  auto character = numeric_cast_v<unsigned int>(constant_value);
965 
966  // Can't guarantee matches against non-ASCII characters.
967  if(character >= 128)
968  return false;
969 
970  if(isalpha(character))
971  {
972  if(to_upper)
973  {
974  if(islower(character))
975  constant_value =
976  from_integer(toupper(character), constant_value.type());
977  }
978  else
979  {
980  if(isupper(character))
981  constant_value =
982  from_integer(tolower(character), constant_value.type());
983  }
984  }
985  }
986 
987  const constant_exprt new_char_array_length =
988  from_integer(operands.size(), length_type);
989 
990  const array_typet new_char_array_type(char_type, new_char_array_length);
991  const array_exprt new_char_array(std::move(operands), new_char_array_type);
992 
994  state,
995  symex_assign,
996  to_ssa_expr(f_l1.arguments().at(0)),
997  new_char_array_length,
998  to_ssa_expr(f_l1.arguments().at(1)),
999  new_char_array);
1000 
1001  return true;
1002 }
1003 
1005  statet &state,
1006  symex_assignt &symex_assign,
1007  const function_application_exprt &f_l1)
1008 {
1009  const auto &f_type = to_mathematical_function_type(f_l1.function().type());
1010  const auto &length_type = f_type.domain().at(0);
1011  const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
1012 
1013  const refined_string_exprt &s = to_string_expr(f_l1.arguments().at(2));
1014  const auto s_data_opt = try_evaluate_constant_string(state, s.content());
1015 
1016  if(!s_data_opt)
1017  return false;
1018 
1019  auto &new_data = f_l1.arguments().at(4);
1020  auto &old_data = f_l1.arguments().at(3);
1021 
1022  array_exprt::operandst characters_to_find;
1023  array_exprt::operandst characters_to_replace;
1024 
1025  // Two main ways to perform a replace: characters or strings.
1026  bool is_single_character = new_data.type().id() == ID_unsignedbv &&
1027  old_data.type().id() == ID_unsignedbv;
1028  if(is_single_character)
1029  {
1030  const auto new_char_pointer = try_evaluate_constant(state, new_data);
1031  const auto old_char_pointer = try_evaluate_constant(state, old_data);
1032 
1033  if(!new_char_pointer || !old_char_pointer)
1034  {
1035  return {};
1036  }
1037 
1038  characters_to_find.emplace_back(old_char_pointer->get());
1039  characters_to_replace.emplace_back(new_char_pointer->get());
1040  }
1041  else
1042  {
1043  auto &new_char_array = to_string_expr(new_data);
1044  auto &old_char_array = to_string_expr(old_data);
1045 
1046  const auto new_char_array_opt =
1047  try_evaluate_constant_string(state, new_char_array.content());
1048 
1049  const auto old_char_array_opt =
1050  try_evaluate_constant_string(state, old_char_array.content());
1051 
1052  if(!new_char_array_opt || !old_char_array_opt)
1053  {
1054  return {};
1055  }
1056 
1057  characters_to_find = old_char_array_opt->get().operands();
1058  characters_to_replace = new_char_array_opt->get().operands();
1059  }
1060 
1061  // Copy data, then do initial search for a replace sequence.
1062  array_exprt existing_data = s_data_opt->get();
1063  auto found_pattern = std::search(
1064  existing_data.operands().begin(),
1065  existing_data.operands().end(),
1066  characters_to_find.begin(),
1067  characters_to_find.end());
1068 
1069  // If we've found a match, proceed to perform a replace on all instances.
1070  while(found_pattern != existing_data.operands().end())
1071  {
1072  // Find the difference between our first/last match iterator.
1073  auto match_end = found_pattern + characters_to_find.size();
1074 
1075  // Erase them.
1076  found_pattern = existing_data.operands().erase(found_pattern, match_end);
1077 
1078  // Insert our replacement characters, then move the iterator to the end of
1079  // our new sequence.
1080  found_pattern = existing_data.operands().insert(
1081  found_pattern,
1082  characters_to_replace.begin(),
1083  characters_to_replace.end()) +
1084  characters_to_replace.size();
1085 
1086  // Then search from there for any additional matches.
1087  found_pattern = std::search(
1088  found_pattern,
1089  existing_data.operands().end(),
1090  characters_to_find.begin(),
1091  characters_to_find.end());
1092  }
1093 
1094  const constant_exprt new_char_array_length =
1095  from_integer(existing_data.operands().size(), length_type);
1096 
1097  const array_typet new_char_array_type(char_type, new_char_array_length);
1098  const array_exprt new_char_array(
1099  std::move(existing_data.operands()), new_char_array_type);
1100 
1102  state,
1103  symex_assign,
1104  to_ssa_expr(f_l1.arguments().at(0)),
1105  new_char_array_length,
1106  to_ssa_expr(f_l1.arguments().at(1)),
1107  new_char_array);
1108 
1109  return true;
1110 }
1111 
1113  statet &state,
1114  symex_assignt &symex_assign,
1115  const function_application_exprt &f_l1)
1116 {
1117  const auto &f_type = to_mathematical_function_type(f_l1.function().type());
1118  const auto &length_type = f_type.domain().at(0);
1119  const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
1120 
1121  const refined_string_exprt &s = to_string_expr(f_l1.arguments().at(2));
1122  const auto s_data_opt = try_evaluate_constant_string(state, s.content());
1123 
1124  if(!s_data_opt)
1125  return false;
1126 
1127  auto is_not_whitespace = [](const exprt &expr) {
1128  auto character = numeric_cast_v<unsigned int>(to_constant_expr(expr));
1129  return character > ' ';
1130  };
1131 
1132  // Note the points where a trim would trim too.
1133  auto &operands = s_data_opt->get().operands();
1134  auto end_iter =
1135  std::find_if(operands.rbegin(), operands.rend(), is_not_whitespace);
1136  auto start_iter =
1137  std::find_if(operands.begin(), operands.end(), is_not_whitespace);
1138 
1139  // Then copy in the string with leading/trailing whitespace removed.
1140  // Note: if start_iter == operands.end it means the entire string is
1141  // whitespace, so we'll trim it to be empty anyway.
1142  exprt::operandst new_operands;
1143  if(start_iter != operands.end())
1144  new_operands = exprt::operandst{start_iter, end_iter.base()};
1145 
1146  const constant_exprt new_char_array_length =
1147  from_integer(new_operands.size(), length_type);
1148 
1149  const array_typet new_char_array_type(char_type, new_char_array_length);
1150  const array_exprt new_char_array(
1151  std::move(new_operands), new_char_array_type);
1152 
1154  state,
1155  symex_assign,
1156  to_ssa_expr(f_l1.arguments().at(0)),
1157  new_char_array_length,
1158  to_ssa_expr(f_l1.arguments().at(1)),
1159  new_char_array);
1160 
1161  return true;
1162 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
goto_symext::clean_expr
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
Definition: symex_clean_expr.cpp:229
symbol_table_baset::has_symbol
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Definition: symbol_table_base.h:87
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
function_application_exprt::arguments
argumentst & arguments()
Definition: mathematical_expr.h:221
symex_targett::assignment_typet
assignment_typet
Definition: symex_target.h:70
symbolt::is_state_var
bool is_state_var
Definition: symbol.h:62
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
typet::subtype
const typet & subtype() const
Definition: type.h:47
symex_assign.h
Symbolic Execution of assignments.
arith_tools.h
goto_symext::dynamic_counter
static unsigned dynamic_counter
A monotonically increasing index for each created dynamic object.
Definition: goto_symex.h:788
goto_symext::try_evaluate_constant_string
optionalt< std::reference_wrapper< const array_exprt > > try_evaluate_constant_string(const statet &state, const exprt &content)
Definition: goto_symex.cpp:340
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
escape_non_alnum
std::string escape_non_alnum(const std::string &to_escape)
Replace non-alphanumeric characters with _xx escapes, where xx are hex digits.
Definition: string_utils.cpp:154
string_utils.h
to_string_expr
refined_string_exprt & to_string_expr(exprt &expr)
Definition: string_expr.h:150
goto_symex_statet::l2_rename_rvalues
NODISCARD exprt l2_rename_rvalues(exprt lvalue, const namespacet &ns)
Definition: goto_symex_state.cpp:285
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
fresh_symbol.h
Fresh auxiliary symbol creation.
symex_targett::sourcet::pc
goto_programt::const_targett pc
Definition: symex_target.h:43
expr_skeleton.h
Expression skeleton.
goto_symext::constant_propagate_case_change
bool constant_propagate_case_change(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1, bool to_upper)
Attempt to constant propagate case changes, both upper and lower.
Definition: goto_symex.cpp:942
goto_symext::constant_propagate_delete
bool constant_propagate_delete(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate deleting a substring from a string.
Definition: goto_symex.cpp:697
goto_symext::target
symex_target_equationt & target
The equation that this execution is building up.
Definition: goto_symex.h:264
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
goto_symex_statet
Central data structure: state.
Definition: goto_symex_state.h:46
goto_symext::constant_propagate_trim
bool constant_propagate_trim(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate trim operations.
Definition: goto_symex.cpp:1112
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
goto_symext::constant_propagate_set_char_at
bool constant_propagate_set_char_at(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate setting the char at the given index.
Definition: goto_symex.cpp:872
goto_symext::symex_cpp_new
virtual void symex_cpp_new(statet &state, const exprt &lhs, const side_effect_exprt &code)
Symbolically execute an assignment instruction that has a CPP new or new array or a Java new array on...
Definition: symex_builtin_functions.cpp:477
s1
int8_t s1
Definition: bytecode_info.h:59
goto_symext::get_new_string_data_symbol
const symbolt & get_new_string_data_symbol(statet &state, symex_assignt &symex_assign, const std::string &aux_symbol_name, const ssa_exprt &char_array, const array_exprt &new_char_array)
Installs a new symbol in the symbol table to represent the given character array, and assigns the cha...
Definition: goto_symex.cpp:276
to_mathematical_function_type
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
Definition: mathematical_types.h:119
exprt
Base class for all expressions.
Definition: expr.h:53
goto_symex_statet::source
symex_targett::sourcet source
Definition: goto_symex_state.h:64
goto_symext::constant_propagate_delete_char_at
bool constant_propagate_delete_char_at(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate deleting a character from a string.
Definition: goto_symex.cpp:624
symex_assignt
Functor for symex assignment.
Definition: symex_assign.h:26
to_side_effect_expr
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1931
field_sensitivityt::apply
exprt apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write) const
Turn an expression expr into a field-sensitive SSA expression.
Definition: field_sensitivity.cpp:21
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
equal_exprt
Equality.
Definition: std_expr.h:1190
ssa_exprt::get_original_expr
const exprt & get_original_expr() const
Definition: ssa_expr.h:33
framet::hidden_function
bool hidden_function
Definition: frame.h:34
goto_symext::symex_assign
void symex_assign(statet &state, const code_assignt &code)
Symbolically execute an ASSIGN instruction or simulate such an execution for a synthetic assignment.
Definition: goto_symex.cpp:38
goto_symext::assign_string_constant
void assign_string_constant(statet &state, symex_assignt &symex_assign, const ssa_exprt &length, const constant_exprt &new_length, const ssa_exprt &char_array, const array_exprt &new_char_array)
Assign constant string length and string data given by a char array to given ssa variables.
Definition: goto_symex.cpp:232
refined_string_exprt
Definition: string_expr.h:109
symex_targett::assignment_typet::STATE
@ STATE
goto_statet::propagation
sharing_mapt< irep_idt, exprt > propagation
Definition: goto_state.h:63
goto_symext::log
messaget log
The messaget to write log messages to.
Definition: goto_symex.h:276
mathematical_types.h
Mathematical types.
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
symbolt::is_thread_local
bool is_thread_local
Definition: symbol.h:65
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
array_exprt::type
const array_typet & type() const
Definition: std_expr.h:1439
goto_symex_statet::threads
std::vector< threadt > threads
Definition: goto_symex_state.h:198
goto_symext::associate_array_to_pointer
void associate_array_to_pointer(statet &state, symex_assignt &symex_assign, const array_exprt &new_char_array, const address_of_exprt &string_data)
Generate array to pointer association primitive.
Definition: goto_symex.cpp:312
goto_symext::constant_propagate_string_concat
bool constant_propagate_string_concat(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate string concatenation.
Definition: goto_symex.cpp:408
goto_symex_statet::call_stack
call_stackt & call_stack()
Definition: goto_symex_state.h:147
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
goto_symext::constant_propagate_integer_to_string
bool constant_propagate_integer_to_string(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate converting an integer to a string.
Definition: goto_symex.cpp:545
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
call_stackt::top
framet & top()
Definition: call_stack.h:17
to_ssa_expr
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:148
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
goto_symex_statet::symbol_table
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
Definition: goto_symex_state.h:69
goto_symext::constant_propagate_empty_string
void constant_propagate_empty_string(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Create an empty string constant.
Definition: goto_symex.cpp:380
goto_symext::constant_propagate_string_substring
bool constant_propagate_string_substring(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate getting a substring of a string.
Definition: goto_symex.cpp:458
goto_symext::constant_propagate_set_length
bool constant_propagate_set_length(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate setting the length of a string.
Definition: goto_symex.cpp:791
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
goto_symext::symex_allocate
virtual void symex_allocate(statet &state, const exprt &lhs, const side_effect_exprt &code)
Symbolically execute an assignment instruction that has an allocate on the right hand side.
Definition: symex_builtin_functions.cpp:49
mathematical_function_typet::codomain
typet & codomain()
Return the codomain, i.e., the set of values that the function maps to (the "target").
Definition: mathematical_types.h:89
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
goto_symext::symex_va_start
virtual void symex_va_start(statet &, const exprt &lhs, const side_effect_exprt &)
Definition: symex_builtin_functions.cpp:252
goto_symex.h
Symbolic Execution.
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
symex_configt::simplify_opt
bool simplify_opt
Definition: symex_config.h:31
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2693
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:191
to_integer_bitvector_type
const integer_bitvector_typet & to_integer_bitvector_type(const typet &type)
Cast a typet to an integer_bitvector_typet.
Definition: std_types.h:1199
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::id
const irep_idt & id() const
Definition: irep.h:418
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
goto_symext::do_simplify
virtual void do_simplify(exprt &expr)
Definition: goto_symex.cpp:32
goto_symex_statet::field_sensitivity
field_sensitivityt field_sensitivity
Definition: goto_symex_state.h:124
side_effect_exprt::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:1897
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
source_locationt
Definition: source_location.h:20
simplify_expr.h
goto_symext::ns
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:256
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
refined_string_exprt::content
const exprt & content() const
Definition: string_expr.h:138
format_expr.h
array_typet
Arrays with given size.
Definition: std_types.h:965
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
function_application_exprt::function
exprt & function()
Definition: mathematical_expr.h:211
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
try_get_string_data_array
optionalt< std::reference_wrapper< const array_exprt > > try_get_string_data_array(const exprt &content, const namespacet &ns)
Get char sequence from content field of a refined string expression.
Definition: simplify_expr.cpp:1837
goto_symext::symex_assume
virtual void symex_assume(statet &state, const exprt &cond)
Symbolically execute an ASSUME instruction or simulate such an execution for a synthetic assumption.
Definition: symex_main.cpp:201
messaget::conditional_output
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to message_stream using output_generator if the configured verbosity is at least as h...
Definition: message.cpp:138
goto_symext::symex_config
const symex_configt symex_config
The configuration to use for this symbolic execution.
Definition: goto_symex.h:183
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
goto_symext::constant_propagate_assignment_with_side_effects
bool constant_propagate_assignment_with_side_effects(statet &state, symex_assignt &symex_assign, const exprt &lhs, const exprt &rhs)
Attempt to constant propagate side effects of the assignment (if any)
Definition: goto_symex.cpp:158
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
messaget::mstreamt
Definition: message.h:224
goto_symex_statet::rename
NODISCARD renamedt< exprt, level > rename(exprt expr, const namespacet &ns)
Rewrites symbol expressions in exprt, applying a suffix to each symbol reflecting its most recent ver...
goto_symext::try_evaluate_constant
static optionalt< std::reference_wrapper< const constant_exprt > > try_evaluate_constant(const statet &state, const exprt &expr)
Definition: goto_symex.cpp:361
get_alnum_string
static std::string get_alnum_string(const array_exprt &char_array)
Maps the given array expression containing constant characters to a string containing only alphanumer...
Definition: goto_symex.cpp:126
symbolt::is_file_local
bool is_file_local
Definition: symbol.h:66
exprt::operands
operandst & operands()
Definition: expr.h:95
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
messaget::debug
mstreamt & debug() const
Definition: message.h:429
symex_targett::assignment_typet::HIDDEN
@ HIDDEN
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
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
s2
int16_t s2
Definition: bytecode_info.h:60
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
goto_symext::constant_propagate_replace
bool constant_propagate_replace(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant proagate character replacement.
Definition: goto_symex.cpp:1004
string_expr.h
String expressions for the string solver.
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1432
c_types.h
to_function_application_expr
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
Definition: mathematical_expr.h:250
get_fresh_aux_symbol
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Definition: fresh_symbol.cpp:32
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1866
expr_skeletont
Expression in which some part is missing and can be substituted for another expression.
Definition: expr_skeleton.h:26
validation_modet::INVARIANT
@ INVARIANT
mathematical_expr.h
API to expression classes for 'mathematical' expressions.
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106