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