cprover
Loading...
Searching...
No Matches
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 {
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 {
75 }
76 else if(statement == ID_allocate)
78 else if(statement == ID_va_start)
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
119 symex_assign.assign_rec(
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 {
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 =
176 to_symbol_expr(f_l1.function()).get_identifier();
177
179 {
181 }
183 {
184 // constant propagating the empty string always succeeds as it does
185 // not depend on potentially non-constant inputs
187 return true;
188 }
190 {
192 }
193 else if(
196 {
198 }
200 {
202 }
204 {
206 }
208 {
210 }
212 {
214 }
216 {
218 }
220 {
221 return constant_propagate_case_change(state, symex_assign, f_l1, false);
222 }
224 {
226 }
228 {
230 }
231 }
232 }
233
234 return false;
235}
236
238 statet &state,
239 symex_assignt &symex_assign,
240 const ssa_exprt &length,
242 const ssa_exprt &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 =
258
259 const symbolt &aux_symbol =
264
265 INVARIANT(
266 aux_symbol.value == new_char_array,
267 "symbol shall have value derived from char array content");
268
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
275 {
278 }
279}
280
282 statet &state,
283 symex_assignt &symex_assign,
284 const std::string &aux_symbol_name,
285 const ssa_exprt &char_array,
287{
290
293 "",
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
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
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
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
383}
384
386 statet &state,
387 symex_assignt &symex_assign,
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
397
399 f_l1.arguments().size() >= 2,
400 "empty string primitive requires two output arguments");
401
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,
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
442 from_integer(new_size, length_type);
443
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)),
457 to_ssa_expr(f_l1.arguments().at(1)),
459
460 return true;
461}
462
464 statet &state,
465 symex_assignt &symex_assign,
467{
468 const std::size_t num_operands = f_l1.arguments().size();
469
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
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
493 {
494 return false;
495 }
496
497 end_index =
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
514 {
515 return false;
516 }
517
518 const mp_integer start_index =
520
522 {
523 return false;
524 }
525
527 from_integer(end_index - start_index, length_type);
528
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)),
544 to_ssa_expr(f_l1.arguments().at(1)),
546
547 return true;
548}
549
551 statet &state,
552 symex_assignt &symex_assign,
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
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
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
587 {
588 return false;
589 }
590
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
604 from_integer(s.length(), length_type);
605
607
608 exprt::operandst operands;
609
610 std::transform(
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)),
623 to_ssa_expr(f_l1.arguments().at(1)),
625
626 return true;
627}
628
630 statet &state,
631 symex_assignt &symex_assign,
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
670 from_integer(s_data.operands().size() - 1, length_type);
671
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)),
696 to_ssa_expr(f_l1.arguments().at(1)),
698
699 return true;
700}
701
703 statet &state,
704 symex_assignt &symex_assign,
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
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
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
766 from_integer(new_size, length_type);
767
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)),
790 to_ssa_expr(f_l1.arguments().at(1)),
792
793 return true;
794}
795
797 statet &state,
798 symex_assignt &symex_assign,
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 =
822
823 if(new_length < 0)
824 {
825 return false;
826 }
827
829
831 from_integer(new_size, length_type);
832
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)),
871 to_ssa_expr(f_l1.arguments().at(1)),
873
874 return true;
875}
876
878 statet &state,
879 symex_assignt &symex_assign,
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
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
927 from_integer(s_data.operands().size(), length_type);
928
930
931 s_data.operands()[numeric_cast_v<std::size_t>(index)] = new_char_opt->get();
932
934 std::move(s_data.operands()), new_char_array_type);
935
937 state,
939 to_ssa_expr(f_l1.arguments().at(0)),
941 to_ssa_expr(f_l1.arguments().at(1)),
943
944 return true;
945}
946
948 statet &state,
949 symex_assignt &symex_assign,
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
964
965 auto &operands = string_data.operands();
966 for(auto &operand : operands)
967 {
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))
981 from_integer(toupper(character), constant_value.type());
982 }
983 else
984 {
985 if(isupper(character))
987 from_integer(tolower(character), constant_value.type());
988 }
989 }
990 }
991
993 from_integer(operands.size(), length_type);
994
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)),
1003 to_ssa_expr(f_l1.arguments().at(1)),
1005
1006 return true;
1007}
1008
1010 statet &state,
1011 symex_assignt &symex_assign,
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
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;
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
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 {
1050
1051 const auto new_char_array_opt =
1053
1054 const auto old_char_array_opt =
1056
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.
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.
1079
1080 // Erase them.
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(
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(
1094 existing_data.operands().end(),
1095 characters_to_find.begin(),
1096 characters_to_find.end());
1097 }
1098
1100 from_integer(existing_data.operands().size(), length_type);
1101
1104 std::move(existing_data.operands()), new_char_array_type);
1105
1107 state,
1109 to_ssa_expr(f_l1.arguments().at(0)),
1111 to_ssa_expr(f_l1.arguments().at(1)),
1113
1114 return true;
1115}
1116
1118 statet &state,
1119 symex_assignt &symex_assign,
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.
1148 if(start_iter != operands.end())
1150
1152 from_integer(new_operands.size(), length_type);
1153
1156 std::move(new_operands), new_char_array_type);
1157
1159 state,
1161 to_ssa_expr(f_l1.arguments().at(0)),
1163 to_ssa_expr(f_l1.arguments().at(1)),
1165
1166 return true;
1167}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const integer_bitvector_typet & to_integer_bitvector_type(const typet &type)
Cast a typet to an integer_bitvector_typet.
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Array constructor from list of elements.
Definition std_expr.h:1476
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.
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
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.
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.
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.
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.
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)
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.
void constant_propagate_empty_string(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Create an empty string constant.
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.
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.
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)
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.
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...
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.
virtual void do_simplify(exprt &expr)
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.
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.
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.
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.
optionalt< std::reference_wrapper< const array_exprt > > try_evaluate_constant_string(const statet &state, const exprt &content)
Array index operator.
Definition std_expr.h:1328
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().
const typet & base_type() const
The type of the data what we point to.
const exprt & content() const
An expression containing a side effect.
Definition std_code.h:1450
Expression providing an SSA-renamed symbol of expressions.
Definition ssa_expr.h:17
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
Functor for symex assignment.
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...
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
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
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)
#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)
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
Symbolic Execution of assignments.