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