CBMC: /home/runner/work/cbmc/cbmc/src/cprover/state_encoding.cpp Source File

CBMC
Loading...
Searching...
No Matches
state_encoding.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: State Encoding
4
5Author: Daniel Kroening, dkr@amazon.com
6
7\*******************************************************************/
8
9#include "state_encoding.h"
10
11#include <util/arith_tools.h>
12#include <util/c_types.h>
13#include <util/mathematical_expr.h>
14#include <util/pointer_expr.h>
15#include <util/prefix.h>
16#include <util/simplify_expr.h>
17#include <util/std_code.h>
18
19#include <goto-programs/goto_model.h>
20
21#include "equality_propagation.h"
22#include "instrument_contracts.h"
23#include "sentinel_dll.h"
24#include "solver.h"
25#include "state.h"
26#include "state_encoding_targets.h"
27#include "variable_encoding.h"
28
29#include <algorithm>
30#include <iostream>
31
33{
34public:
39
40 void operator()(
41 const goto_functionst::function_mapt::const_iterator,
43
44 void encode(
45 const goto_functiont &,
47 const std::string &state_prefix,
48 const std::vector<irep_idt> &call_stack,
49 const std::string &annotation,
51 const exprt &return_lhs,
53
54protected:
57
59 symbol_exprt state_expr_with_suffix(loct, const std::string &suffix) const;
62 std::vector<symbol_exprt> incoming_symbols(loct) const;
63 exprt evaluate_expr(loct, const exprt &, const exprt &) const;
65 loct,
66 const exprt &,
67 const exprt &,
68 const std::unordered_set<symbol_exprt, irep_hash> &) const;
70 loct,
71 const exprt &,
72 std::vector<symbol_exprt> &nondet_symbols) const;
73 exprt evaluate_expr(loct, const exprt &) const;
74 exprt address_rec(loct, const exprt &, exprt) const;
78 void setup_incoming(const goto_functiont &);
81 loct,
82 exprt state,
83 exprt lhs,
84 exprt rhs,
85 std::vector<symbol_exprt> &nondet_symbols) const;
88
90 std::string state_prefix;
91 std::string annotation;
92 std::vector<irep_idt> call_stack;
96 using incomingt =
97 std::map<loct, std::vector<loct>, goto_programt::target_less_than>;
99
100 static symbol_exprt va_args(irep_idt function);
101};
102
107
109 loct loc,
110 const std::string &suffix) const
111{
112 irep_idt identifier =
113 state_prefix + std::to_string(loc->location_number) + suffix;
114 return symbol_exprt(identifier, state_predicate_type());
115}
116
118{
119 return state_expr_with_suffix(loc, taken ? "T" : "");
120}
121
122 std::vector<symbol_exprt> state_encodingt::incoming_symbols(loct loc) const
123{
124 auto incoming_it = incoming.find(loc);
125
126 DATA_INVARIANT(incoming_it != incoming.end(), "incoming is complete");
127
128 std::vector<symbol_exprt> symbols;
129 symbols.reserve(incoming_it->second.size());
130
131 for(auto &loc_in : incoming_it->second)
132 {
133 std::string suffix;
134
135 // conditional jump from loc_in to loc?
136 if(
137 loc_in->is_goto() && loc_in->condition() != true &&
138 loc != std::next(loc_in))
139 {
140 suffix = "T";
141 }
142
143 symbols.push_back(state_expr_with_suffix(loc_in, suffix));
144 }
145
146 return symbols;
147}
148
150{
151 if(loc == first_loc)
152 return entry_state;
153
154 auto incoming_symbols = this->incoming_symbols(loc);
155
156 if(incoming_symbols.size() == 1)
157 return incoming_symbols.front();
158 else
159 return state_expr_with_suffix(loc, "in");
160}
161
163 loct loc,
164 const exprt &state,
165 const exprt &what) const
166{
167 return evaluate_expr_rec(loc, state, what, {});
168}
169
171 loct loc,
172 const exprt &what,
173 std::vector<symbol_exprt> &nondet_symbols) const
174{
175 if(what.id() == ID_side_effect)
176 {
177 auto &side_effect = to_side_effect_expr(what);
178 auto statement = side_effect.get_statement();
179 if(statement == ID_nondet)
180 {
181 irep_idt identifier = "nondet::" + state_prefix +
182 std::to_string(loc->location_number) + "-" +
183 std::to_string(nondet_symbols.size());
184 auto symbol = symbol_exprt(identifier, side_effect.type());
185 nondet_symbols.push_back(symbol);
186 return std::move(symbol);
187 }
188 else if(statement == ID_va_start)
189 {
190 // return address of va_args array
193 what.type());
194 }
195 else
196 return what; // leave it
197 }
198 else
199 {
200 exprt tmp = what;
201 for(auto &op : tmp.operands())
202 op = replace_nondet_rec(loc, op, nondet_symbols);
203 return tmp;
204 }
205}
206
208 loct loc,
209 const exprt &state,
210 const exprt &what,
211 const std::unordered_set<symbol_exprt, irep_hash> &bound_symbols) const
212{
213 PRECONDITION(state.type().id() == ID_state);
214
215 if(what.id() == ID_symbol)
216 {
217 const auto &symbol_expr = to_symbol_expr(what);
218
219 if(symbol_expr.identifier() == CPROVER_PREFIX "return_value")
220 {
221 auto new_symbol = symbol_exprt("return_value", what.type());
222 return evaluate_exprt(
223 state, address_rec(loc, state, new_symbol), what.type());
224 }
225 else if(bound_symbols.find(symbol_expr) == bound_symbols.end())
226 {
227 return evaluate_exprt(state, address_rec(loc, state, what), what.type());
228 }
229 else
230 return what; // leave as is
231 }
232 else if(
233 what.id() == ID_dereference || what.id() == ID_member ||
234 what.id() == ID_index)
235 {
236 return evaluate_exprt(state, address_rec(loc, state, what), what.type());
237 }
238 else if(what.id() == ID_forall || what.id() == ID_exists)
239 {
240 auto new_quantifier_expr = to_quantifier_expr(what); // copy
241 auto new_bound_symbols = bound_symbols; // copy
242
243 for(const auto &v : new_quantifier_expr.variables())
244 new_bound_symbols.insert(v);
245
247 loc, state, new_quantifier_expr.where(), new_bound_symbols);
248
249 return std::move(new_quantifier_expr);
250 }
251 else if(what.id() == ID_address_of)
252 {
253 const auto &object = to_address_of_expr(what).object();
254 return address_rec(loc, state, object);
255 }
256 else if(what.id() == ID_live_object)
257 {
258 const auto &live_object_expr = to_live_object_expr(what);
259 auto pointer =
260 evaluate_expr_rec(loc, state, live_object_expr.pointer(), bound_symbols);
261 return state_live_object_exprt(state, pointer);
262 }
263 else if(what.id() == ID_writeable_object)
264 {
266 auto pointer = evaluate_expr_rec(
267 loc, state, writeable_object_expr.pointer(), bound_symbols);
268 return state_writeable_object_exprt(state, pointer);
269 }
270 else if(what.id() == ID_is_dynamic_object)
271 {
273 auto pointer = evaluate_expr_rec(
274 loc, state, is_dynamic_object_expr.address(), bound_symbols);
275 return state_is_dynamic_object_exprt(state, pointer);
276 }
277 else if(what.id() == ID_object_size)
278 {
279 const auto &object_size_expr = to_object_size_expr(what);
280 auto pointer =
281 evaluate_expr_rec(loc, state, object_size_expr.pointer(), bound_symbols);
282 return state_object_size_exprt(state, pointer, what.type());
283 }
284 else if(what.id() == ID_r_ok || what.id() == ID_w_ok || what.id() == ID_rw_ok)
285 {
286 // we need to add the state
287 const auto &r_or_w_ok_expr = to_r_or_w_ok_expr(what);
288 auto pointer =
289 evaluate_expr_rec(loc, state, r_or_w_ok_expr.pointer(), bound_symbols);
290 auto size =
292 auto new_id = what.id() == ID_r_ok ? ID_state_r_ok
293 : what.id() == ID_w_ok ? ID_state_w_ok
295 return ternary_exprt(new_id, state, pointer, size, what.type());
296 }
297 else if(what.id() == ID_is_cstring)
298 {
299 // we need to add the state
300 const auto &is_cstring_expr = to_unary_expr(what);
301 auto pointer =
303 return binary_predicate_exprt(state, ID_state_is_cstring, pointer);
304 }
305 else if(what.id() == ID_cstrlen)
306 {
307 // we need to add the state
308 const auto &cstrlen_expr = to_cstrlen_expr(what);
309 auto address =
311 return state_cstrlen_exprt(state, address, cstrlen_expr.type());
312 }
313 else if(what.id() == ID_is_sentinel_dll)
314 {
315 // we need to add the state
316 if(what.operands().size() == 2)
317 {
318 const auto &is_sentinel_dll_expr = to_binary_expr(what);
319 auto head = evaluate_expr_rec(
320 loc, state, is_sentinel_dll_expr.op0(), bound_symbols);
321 auto tail = evaluate_expr_rec(
322 loc, state, is_sentinel_dll_expr.op1(), bound_symbols);
323 return state_is_sentinel_dll_exprt(state, head, tail);
324 }
325 else if(what.operands().size() == 3)
326 {
327 const auto &is_sentinel_dll_expr = to_ternary_expr(what);
328 auto head = evaluate_expr_rec(
329 loc, state, is_sentinel_dll_expr.op0(), bound_symbols);
330 auto tail = evaluate_expr_rec(
331 loc, state, is_sentinel_dll_expr.op1(), bound_symbols);
332 auto node = evaluate_expr_rec(
333 loc, state, is_sentinel_dll_expr.op2(), bound_symbols);
334 return state_is_sentinel_dll_exprt(state, head, tail, node);
335 }
336 else
337 DATA_INVARIANT(false, "is_sentinel_dll expressions have 2 or 3 operands");
338 }
339 else if(what.id() == ID_side_effect)
340 {
341 // leave as is
342 return what;
343 }
344 else if(
345 (what.id() == ID_equal || what.id() == ID_notequal) &&
346 to_binary_relation_expr(what).lhs().type().id() == ID_struct_tag)
347 {
348 const auto &lhs = to_binary_relation_expr(what).lhs();
349 const auto &rhs = to_binary_relation_expr(what).rhs();
350
351 const auto &type = to_struct_tag_type(lhs.type());
352 const namespacet ns(goto_model.symbol_table);
353 const auto &struct_type = ns.follow_tag(type);
354
356
357 for(auto &field : struct_type.components())
358 {
359 exprt lhs_member = member_exprt(lhs, field.get_name(), field.type());
360 exprt rhs_member = member_exprt(rhs, field.get_name(), field.type());
361 auto equality = equal_exprt(lhs_member, rhs_member);
362 auto equality_evaluated =
363 evaluate_expr_rec(loc, state, equality, bound_symbols);
364 conjuncts.push_back(std::move(equality_evaluated));
365 }
366
367 if(what.id() == ID_equal)
368 return conjunction(conjuncts);
369 else
371 }
372 else
373 {
374 exprt tmp = what;
375 for(auto &op : tmp.operands())
376 op = evaluate_expr_rec(loc, state, op, bound_symbols);
377 return tmp;
378 }
379}
380
382{
383 return evaluate_expr(loc, in_state_expr(loc), what);
384}
385
387{
388 return lambda_exprt({state_expr()}, std::move(what));
389}
390
392{
393 return forall_exprt(
394 {state_expr()},
397 std::move(what)));
398}
399
401 const
402{
403 return forall_exprt(
404 {state_expr()},
406 and_exprt(
408 std::move(condition)),
409 std::move(what)));
410}
411
413 const
414{
415 if(expr.id() == ID_symbol)
416 {
418 }
419 else if(expr.id() == ID_member)
420 {
421 auto compound = to_member_expr(expr).struct_op();
422 auto compound_address = address_rec(loc, state, std::move(compound));
423 auto component_name = to_member_expr(expr).get_component_name();
424
426
427 if(expr.type().id() == ID_array)
428 {
429 const auto &element_type = to_array_type(expr.type()).element_type();
430 return field_address_exprt(
431 std::move(compound_address),
432 component_name,
433 pointer_type(element_type));
434 }
435 else
436 {
437 return field_address_exprt(
438 std::move(compound_address), component_name, pointer_type(expr.type()));
439 }
440 }
441 else if(expr.id() == ID_index)
442 {
443 auto array = to_index_expr(expr).array();
444 auto index_evaluated =
445 evaluate_expr(loc, state, to_index_expr(expr).index());
446 auto array_address = address_rec(loc, state, std::move(array));
447 // The type of the element pointer may not be the type
448 // of the base pointer, which may be a pointer to an array.
450 std::move(array_address),
451 std::move(index_evaluated),
452 pointer_type(expr.type()));
453 }
454 else if(expr.id() == ID_dereference)
455 return evaluate_expr(loc, state, to_dereference_expr(expr).pointer());
456 else if(expr.id() == ID_string_constant)
457 {
458 // we'll stick to 'address_of' here.
459 return address_of_exprt(
460 expr, pointer_type(to_array_type(expr.type()).element_type()));
461 }
462 else if(expr.id() == ID_array)
463 {
464 // TBD.
466 "can't do array literals", expr.source_location());
467 }
468 else if(expr.id() == ID_struct)
469 {
470 // TBD.
472 "can't do struct literals", expr.source_location());
473 }
474 else if(expr.id() == ID_union)
475 {
476 // TBD.
478 "can't do union literals", expr.source_location());
479 }
480 else if(expr.id() == ID_side_effect)
481 {
482 // Should have been removed elsewhere.
484 "address of side effect " +
485 id2string(to_side_effect_expr(expr).get_statement()),
486 expr.source_location());
487 }
488 else if(expr.id() == ID_typecast)
489 {
490 // TBD.
492 "can't do assignments to typecasts", expr.source_location());
493 }
494 else
495 {
496 // address of something we don't know
498 "address of unknown object " + expr.id_string(), expr.source_location());
499 }
500}
501
503 loct loc,
504 exprt state,
505 exprt lhs,
506 exprt rhs,
507 std::vector<symbol_exprt> &nondet_symbols) const
508{
509 if(lhs.type().id() == ID_struct_tag)
510 {
511 // split up into fields, recursively
512 const namespacet ns(goto_model.symbol_table);
513 const auto &struct_type = ns.follow_tag(to_struct_tag_type(lhs.type()));
514 exprt new_state = state;
515 for(auto &field : struct_type.components())
516 {
517 exprt lhs_member = member_exprt(lhs, field.get_name(), field.type());
518 exprt rhs_member = member_exprt(rhs, field.get_name(), field.type());
519
520 if(rhs.id() == ID_struct)
522 else if(
523 rhs.id() == ID_side_effect &&
524 to_side_effect_expr(rhs).get_statement() == ID_nondet)
525 {
526 rhs_member =
528 }
529
532 }
533
534 return new_state;
535 }
536 else if(lhs.type().id() == ID_array)
537 {
538 // split up into elements, recursively
539 const namespacet ns(goto_model.symbol_table);
540 auto &array_type = to_array_type(lhs.type());
541 if(array_type.size().is_constant())
542 {
543 auto size_int =
545 exprt new_state = state;
546
547 for(mp_integer i = 0; i < size_int; ++i)
548 {
549 auto i_expr = from_integer(i, array_type.index_type());
552
553 if(rhs.id() == ID_array)
555 else if(
556 rhs.id() == ID_side_effect &&
557 to_side_effect_expr(rhs).get_statement() == ID_nondet)
558 {
559 rhs_index =
561 }
562
565 }
566
567 return new_state;
568 }
569 else
570 {
571 // TODO: quantifier?
572 return state;
573 }
574 }
575 else
576 {
577 auto s = state_expr();
578 auto address = address_rec(loc, s, lhs);
579
580 exprt rhs_evaluated = evaluate_expr(loc, s, rhs);
581
583
584 return update_state_exprt(state, address, new_value);
585 }
586}
587
589 const
590{
591 std::vector<symbol_exprt> nondet_symbols;
592
593 auto new_state =
595
597 binding.insert(binding.end(), nondet_symbols.begin(), nondet_symbols.end());
598
599 return forall_exprt(
600 std::move(binding),
604}
605
607{
608 forall_goto_program_instructions(it, goto_function.body)
609 incoming[it];
610
611 forall_goto_program_instructions(it, goto_function.body)
612 {
613 if(it->is_goto())
614 incoming[it->get_target()].push_back(it);
615 }
616
617 forall_goto_program_instructions(it, goto_function.body)
618 {
619 auto next = std::next(it);
620 if(it->is_goto() && it->condition() == true)
621 {
622 }
623 else if(next != goto_function.body.instructions.end())
624 {
625 incoming[next].push_back(it);
626 }
627 }
628}
629
631{
632 if(src.id() == ID_not)
633 return to_not_expr(src).op();
634 else
635 return not_exprt(src);
636}
637
639{
640 return symbol_exprt(
641 "va_args::" + id2string(function),
643}
644
645 std::set<irep_idt> no_body_warnings;
646
649 encoding_targett &dest)
650{
651 const auto &function = to_symbol_expr(loc->call_function());
652 const auto &type = to_code_type(function.type());
653 auto identifier = function.identifier();
654
655 auto new_annotation = annotation + u8 " \u2192 " + id2string(identifier);
657
658 // malloc is special-cased
659 if(identifier == "malloc")
660 {
661 auto state = state_expr();
662 PRECONDITION(loc->call_arguments().size() == 1);
663 auto size_evaluated = evaluate_expr(loc, state, loc->call_arguments()[0]);
664
665 auto lhs_address = address_rec(loc, state, loc->call_lhs());
666 auto lhs_type = to_pointer_type(loc->call_lhs().type());
669 dest << forall_states_expr(
671 return;
672 }
673
674 // malloc is special-cased
675 if(identifier == "posix_memalign")
676 {
677 // int posix_memalign(void **memptr, size_t alignment, size_t size);
678 auto state = state_expr();
679 PRECONDITION(loc->call_arguments().size() == 3);
680 auto memptr_evaluated = evaluate_expr(loc, state, loc->call_arguments()[0]);
681 auto size_evaluated = evaluate_expr(loc, state, loc->call_arguments()[2]);
682 auto lhs_type =
686 dest << forall_states_expr(
688 return;
689 }
690
691 // realloc is special-cased
692 if(identifier == "realloc")
693 {
694 auto state = state_expr();
695 PRECONDITION(loc->call_arguments().size() == 2);
696 auto pointer_evaluated =
697 evaluate_expr(loc, state, loc->call_arguments()[0]);
698 auto size_evaluated = evaluate_expr(loc, state, loc->call_arguments()[1]);
699
700 auto lhs_address = address_rec(loc, state, loc->call_lhs());
701 auto lhs_type = to_pointer_type(loc->call_lhs().type());
703 state,
706 dest << forall_states_expr(
708 return;
709 }
710
711 // free is special-cased
712 if(identifier == "free")
713 {
714 auto state = state_expr();
715 PRECONDITION(loc->call_arguments().size() == 1);
716 auto address_evaluated =
717 evaluate_expr(loc, state, loc->call_arguments()[0]);
718
720 dest << forall_states_expr(
722 return;
723 }
724
725 // Find the function
726 auto f = goto_model.goto_functions.function_map.find(identifier);
727 if(f == goto_model.goto_functions.function_map.end())
728 DATA_INVARIANT(false, "failed find function in function_map");
729
730 // Do we have a function body?
731 if(!f->second.body_available())
732 {
733 // no function body -- do LHS assignment nondeterministically, if any
734 if(loc->call_lhs().is_not_nil())
735 {
736 auto rhs = side_effect_expr_nondett(
737 loc->call_lhs().type(), loc->source_location());
738 dest << assignment_constraint(loc, loc->call_lhs(), std::move(rhs));
739 }
740 else
741 {
742 // This is a SKIP.
743 dest << equal_exprt(out_state_expr(loc), in_state_expr(loc));
744 }
745
746 // issue a warning, but only once
747 if(no_body_warnings.insert(identifier).second)
748 std::cout << "**** WARNING: no body for function " << identifier << '\n';
749 }
750 else
751 {
752 // Yes, we've got a body. Check whether this is recursive.
753 if(
754 std::find(call_stack.begin(), call_stack.end(), identifier) !=
755 call_stack.end())
756 {
757 // ignore
758 dest << equal_exprt(out_state_expr(loc), in_state_expr(loc));
759 return;
760 }
761
762 // Evaluate the arguments of the call in the 'in state'
764 const auto &arguments = loc->call_arguments();
765
766 // regular parameters
767 for(std::size_t i = 0; i < type.parameters().size(); i++)
768 {
769 auto address = object_address_exprt(symbol_exprt(
770 f->second.parameter_identifiers[i], type.parameters()[i].type()));
771 auto value = evaluate_expr(loc, state_expr(), arguments[i]);
773 }
774
775 // extra arguments, i.e., va_arg
776 if(arguments.size() > type.parameters().size())
777 {
778 std::vector<exprt> va_args_elements;
780
781 for(std::size_t i = type.parameters().size(); i < arguments.size(); i++)
782 {
783 auto index = i - type.parameters().size();
784 auto id = "va_arg::" + state_prefix +
785 std::to_string(loc->location_number) +
786 "::" + std::to_string(index);
787 auto address =
788 object_address_exprt(symbol_exprt(id, arguments[i].type()));
789 auto value = evaluate_expr(loc, state_expr(), arguments[i]);
790 va_args_elements.push_back(
793 }
794
795 // assign these to an array
796 auto va_count = va_args_elements.size();
797 auto array_type = array_typet(
799 auto array_identifier =
800 "va_arg_array::" + state_prefix + std::to_string(loc->location_number);
801 auto array_symbol = symbol_exprt(array_identifier, array_type);
802
803 for(std::size_t i = 0; i < va_count; i++)
804 {
805 auto address = element_address_exprt(
806 object_address_exprt(array_symbol),
807 from_integer(i, array_type.index_type()),
809 auto value = va_args_elements[i];
811 }
812
813 // now make va_args point to the beginning of that array
814 auto address = object_address_exprt(va_args(identifier));
815 auto value = element_address_exprt(
816 object_address_exprt(array_symbol),
817 from_integer(0, array_type.index_type()),
820 }
821
822 // Now assign all the arguments to the parameters
823 auto function_entry_state = state_expr_with_suffix(loc, "Entry");
824 dest << forall_states_expr(
826
827 // now do the body, recursively
829 auto new_state_prefix =
830 state_prefix + std::to_string(loc->location_number) + ".";
833 body_state_encoding.encode(
834 f->second,
835 identifier,
840 nil_exprt(),
841 dest);
842
843 // exit state of called function
844 auto exit_loc = std::prev(f->second.body.instructions.end());
846 new_state_prefix + std::to_string(exit_loc->location_number);
847 auto exit_state =
849
850 // done with function, reset source location to call site
851 dest.set_source_location(loc->source_location());
852
853 // now assign the return value, if any
854 if(loc->call_lhs().is_not_nil())
855 {
856 auto rhs = symbol_exprt("return_value", loc->call_lhs().type());
857 auto state = state_expr();
858 auto address = address_rec(exit_loc, state, loc->call_lhs());
859 auto rhs_evaluated = evaluate_expr(exit_loc, state, rhs);
861 dest << forall_exprt(
862 {state_expr()},
866 }
867 else
868 {
869 // link up return state to exit state
870 dest << equal_exprt(out_state_expr(loc), std::move(exit_state));
871 }
872 }
873}
874
877 encoding_targett &dest)
878{
879 // Function pointer?
880 const auto &function = loc->call_function();
881 if(function.id() == ID_dereference)
882 {
883 // TBD.
885 "can't do function pointers", loc->source_location());
886 }
887 else if(function.id() == ID_symbol)
888 {
889 function_call_symbol(loc, dest);
890 }
891 else
892 {
894 false, "got function that's neither a symbol nor a function pointer");
895 }
896}
897
899 goto_functionst::function_mapt::const_iterator f_entry,
900 encoding_targett &dest)
901{
902 const auto &goto_function = f_entry->second;
903
904 if(goto_function.body.instructions.empty())
905 return;
906
907 // initial state
908 auto in_state = symbol_exprt("SInitial", state_predicate_type());
909
910 dest << forall_exprt(
911 {state_expr()},
915
916 auto annotation = id2string(f_entry->first);
917
918 encode(
919 goto_function,
920 f_entry->first,
921 "S",
922 {},
924 in_state,
925 nil_exprt(),
926 dest);
927}
928
930 const goto_functiont &goto_function,
931 const irep_idt function_identifier,
932 const std::string &state_prefix,
933 const std::vector<irep_idt> &call_stack,
934 const std::string &annotation,
935 const symbol_exprt &entry_state,
936 const exprt &return_lhs,
937 encoding_targett &dest)
938{
939 first_loc = goto_function.body.instructions.begin();
940 this->function_identifier = function_identifier;
941 this->state_prefix = state_prefix;
942 this->call_stack = call_stack;
943 this->annotation = annotation;
944 this->entry_state = entry_state;
945 this->return_lhs = return_lhs;
946
947 setup_incoming(goto_function);
948
949 // constraints for each instruction
950 forall_goto_program_instructions(loc, goto_function.body)
951 {
952 // pass on the source code location
953 dest.set_source_location(loc->source_location());
954
955 // constraints on the incoming state
956 {
957 auto incoming_symbols = this->incoming_symbols(loc);
958
959 if(incoming_symbols.size() >= 2)
960 {
961 auto s = state_expr();
963 {
964 dest << forall_exprt(
965 {s},
969 }
970 }
971 }
972
973 if(loc->is_assign())
974 {
975 auto &lhs = loc->assign_lhs();
976 auto &rhs = loc->assign_rhs();
977
978 DATA_INVARIANT(lhs.type() == rhs.type(), "assignment type consistency");
979
980 if(
981 lhs.id() == ID_symbol &&
983 id2string(to_symbol_expr(lhs).identifier()), CPROVER_PREFIX) &&
984 to_symbol_expr(lhs).identifier() != CPROVER_PREFIX "rounding_mode")
985 {
986 // skip for now
987 dest << equal_exprt(out_state_expr(loc), in_state_expr(loc));
988 }
989 else if(
990 lhs.id() == ID_symbol &&
991 to_symbol_expr(lhs).identifier() == "_DefaultRuneLocale")
992 {
993 // /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/runetype.h
994 // skip for now
995 dest << equal_exprt(out_state_expr(loc), in_state_expr(loc));
996 }
997 else
998 dest << assignment_constraint(loc, lhs, rhs);
999 }
1000 else if(loc->is_assume())
1001 {
1002 // we produce ∅ when the assumption is false
1003 auto state = state_expr();
1004 auto condition_evaluated = evaluate_expr(loc, state, loc->condition());
1005
1006 dest << forall_states_expr(
1007 loc,
1010 }
1011 else if(loc->is_goto())
1012 {
1013 // We produce ∅ when the 'other' branch is taken. Get the condition.
1014 const auto &condition = loc->condition();
1015
1016 if(condition == true)
1017 {
1018 dest << equal_exprt(out_state_expr(loc), in_state_expr(loc));
1019 }
1020 else
1021 {
1022 auto state = state_expr();
1023 auto condition_evaluated = evaluate_expr(loc, state, condition);
1024
1025 dest << forall_states_expr(
1026 loc,
1028 function_application_exprt(out_state_expr(loc, true), {state}));
1029
1030 dest << forall_states_expr(
1031 loc,
1033 function_application_exprt(out_state_expr(loc, false), {state}));
1034 }
1035 }
1036 else if(loc->is_assert())
1037 {
1038 // all assertions need to hold
1039 dest << forall_states_expr(
1040 loc, evaluate_expr(loc, state_expr(), loc->condition()));
1041
1042 dest << equal_exprt(out_state_expr(loc), in_state_expr(loc));
1043 }
1044 else if(
1045 loc->is_skip() || loc->is_assert() || loc->is_location() ||
1046 loc->is_end_function())
1047 {
1048 // these do not change the state
1049 dest << equal_exprt(out_state_expr(loc), in_state_expr(loc));
1050 }
1051 else if(loc->is_atomic_begin() || loc->is_atomic_end())
1052 {
1053 // no concurrency yet
1054 dest << equal_exprt(out_state_expr(loc), in_state_expr(loc));
1055 }
1056 else if(loc->is_other())
1057 {
1058 auto &code = loc->code();
1059 auto &statement = code.get_statement();
1060 if(statement == ID_array_set)
1061 {
1063 code.operands().size() == 2, "array_set has two operands");
1064 // op0 must be an array
1065 dest << equal_exprt(out_state_expr(loc), in_state_expr(loc));
1066 }
1067 else
1068 {
1069 // ought to print a warning
1070 dest << equal_exprt(out_state_expr(loc), in_state_expr(loc));
1071 }
1072 }
1073 else if(loc->is_decl())
1074 {
1075 auto s_in = state_expr();
1077 s_in, address_rec(loc, s_in, loc->decl_symbol()));
1078 dest << forall_states_expr(
1080 }
1081 else if(loc->is_dead())
1082 {
1083 auto s = state_expr();
1084 auto s_in = state_expr();
1086 s_in, address_rec(loc, s_in, loc->dead_symbol()));
1087 dest << forall_states_expr(
1089 }
1090 else if(loc->is_function_call())
1091 {
1092 function_call(loc, dest);
1093 }
1094 else if(loc->is_set_return_value())
1095 {
1096 const auto &rhs = loc->return_value();
1097
1098 if(return_lhs.is_nil())
1099 {
1100 // treat these as assignments to a special symbol named 'return_value'
1101 auto lhs = symbol_exprt("return_value", rhs.type());
1102 dest << assignment_constraint(loc, std::move(lhs), std::move(rhs));
1103 }
1104 else
1105 {
1106 }
1107 }
1108 else
1109 {
1110 std::cout << "X: " << loc->type() << '\n';
1111 DATA_INVARIANT(false, "unexpected GOTO instruction");
1112 }
1113 }
1114}
1115
1117 const goto_modelt &goto_model,
1118 bool program_is_inlined,
1119 std::optional<irep_idt> contract,
1120 encoding_targett &dest)
1121{
1123 {
1124 auto f_entry = goto_model.goto_functions.function_map.find(
1126
1127 if(f_entry == goto_model.goto_functions.function_map.end())
1128 throw incorrect_goto_program_exceptiont("The program has no entry point");
1129
1130 dest.annotation("function " + id2string(f_entry->first));
1131
1132 state_encodingt{goto_model}(f_entry, dest);
1133 }
1134 else if(contract.has_value())
1135 {
1136 // check given contract
1137 const namespacet ns(goto_model.symbol_table);
1138 const symbolt *symbol;
1139 if(ns.lookup(*contract, symbol))
1141 "The given function was not found", "contract");
1142
1143 if(!get_contract(*contract, ns).has_value())
1145 "The given function has no contract", "contract");
1146
1147 const auto f = goto_model.goto_functions.function_map.find(symbol->name);
1148 CHECK_RETURN(f != goto_model.goto_functions.function_map.end());
1149
1150 dest.annotation("");
1151 dest.annotation("function " + id2string(symbol->name));
1152 state_encodingt{goto_model}(f, dest);
1153 }
1154 else
1155 {
1156 // sort alphabetically
1157 const auto sorted = goto_model.goto_functions.sorted();
1158 const namespacet ns(goto_model.symbol_table);
1159 bool found = false;
1160 for(auto &f : sorted)
1161 {
1162 if(
1163 f->first == goto_functionst::entry_point() ||
1164 get_contract(f->first, ns).has_value())
1165 {
1166 dest.annotation("");
1167 dest.annotation("function " + id2string(f->first));
1168 state_encodingt{goto_model}(f, dest);
1169 found = true;
1170 }
1171 }
1172
1173 if(!found)
1174 throw incorrect_goto_program_exceptiont("The program has no entry point");
1175 }
1176}
1177
1179 const goto_modelt &goto_model,
1181 bool program_is_inlined,
1182 std::optional<irep_idt> contract,
1183 std::ostream &out)
1184{
1185 switch(state_encoding_format)
1186 {
1188 {
1189 ascii_encoding_targett dest(out);
1190 state_encoding(goto_model, program_is_inlined, contract, dest);
1191 }
1192 break;
1193
1195 {
1196 const namespacet ns(goto_model.symbol_table);
1197 smt2_encoding_targett dest(ns, out);
1198 state_encoding(goto_model, program_is_inlined, contract, dest);
1199 }
1200 break;
1201 }
1202}
1203
1205 const goto_modelt &goto_model,
1207 std::ostream &out)
1208{
1209 const namespacet ns(goto_model.symbol_table);
1210
1212 state_encoding(goto_model, true, {}, container);
1213
1215
1216 variable_encoding(container.constraints);
1217
1218 switch(state_encoding_format)
1219 {
1221 {
1222 ascii_encoding_targett dest(out);
1223 dest << container;
1224 }
1225 break;
1226
1228 {
1229 smt2_encoding_targett dest(ns, out);
1230 dest << container;
1231 }
1232 break;
1233 }
1234}
1235
1237 const goto_modelt &goto_model,
1238 bool program_is_inlined,
1239 std::optional<irep_idt> contract,
1241{
1242 const namespacet ns(goto_model.symbol_table);
1243
1245 state_encoding(goto_model, program_is_inlined, contract, container);
1246
1248
1249#if 0
1250 if(solver_options.verbose)
1251 {
1252 ascii_encoding_targett dest(std::cout);
1253 dest << container;
1254 }
1255#endif
1256
1257 return solver(container.constraints, solver_options, ns);
1258}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
Operator to return the address of an object.
Definition pointer_expr.h:540
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
Definition state.h:218
Boolean AND All operands must be boolean, and the result is always boolean.
Definition std_expr.h:2043
Arrays with given size.
Definition std_types.h:806
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition std_expr.h:737
std::vector< symbol_exprt > variablest
Definition std_expr.h:3172
constraintst constraints
Definition state.h:412
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Operator to return the address of an array element relative to a base address.
Definition pointer_expr.h:748
The empty type.
Definition std_types.h:50
virtual void annotation(const std::string &)
void set_source_location(source_locationt __source_location)
Definition state.h:978
Equality.
Definition std_expr.h:1339
Definition state.h:78
Definition state.h:1061
Base class for all expressions.
Definition expr.h:57
std::vector< exprt > operandst
Definition expr.h:59
typet & type()
Return the type of the expression.
Definition expr.h:85
operandst & operands()
Definition expr.h:95
const source_locationt & source_location() const
Definition expr.h:236
Operator to return the address of a field relative to a base address.
Definition pointer_expr.h:664
A forall expression.
Application of (mathematical) function.
function_mapt function_map
std::vector< function_mapt::const_iterator > sorted() const
returns a vector of the iterators in alphabetical order
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition goto_function.h:24
goto_programt body
Definition goto_function.h:26
Definition goto_model.h:27
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
instructionst instructions
The list of instructions in the goto program.
Definition goto_program.h:621
instructionst::const_iterator const_targett
Definition goto_program.h:614
Boolean implication.
Definition std_expr.h:2154
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
Array index operator.
Definition std_expr.h:1431
Definition state.h:34
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
const std::string & id_string() const
Definition irep.h:391
const irep_idt & id() const
Definition irep.h:388
bool is_nil() const
Definition irep.h:368
A (mathematical) lambda expression.
Extract member of struct or union.
Definition std_expr.h:2866
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:49
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition namespace.cpp:134
The NIL expression.
Definition std_expr.h:3144
Boolean negation.
Definition std_expr.h:2388
Operator to return the address of an object.
Definition pointer_expr.h:596
Definition state.h:313
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
Definition solver.h:28
Definition state.h:634
incomingt incoming
state_encodingt(const goto_modelt &__goto_model)
exprt evaluate_expr_rec(loct, const exprt &, const exprt &, const std::unordered_set< symbol_exprt, irep_hash > &) const
void setup_incoming(const goto_functiont &)
symbol_exprt in_state_expr(loct) const
void function_call(goto_programt::const_targett, encoding_targett &)
const goto_modelt & goto_model
exprt address_rec(loct, const exprt &, exprt) const
goto_programt::const_targett loct
void encode(const goto_functiont &, const irep_idt function_identifier, const std::string &state_prefix, const std::vector< irep_idt > &call_stack, const std::string &annotation, const symbol_exprt &entry_state, const exprt &return_lhs, encoding_targett &)
std::string annotation
symbol_exprt out_state_expr(loct) const
static symbol_exprt va_args(irep_idt function)
exprt assignment_constraint_rec(loct, exprt state, exprt lhs, exprt rhs, std::vector< symbol_exprt > &nondet_symbols) const
std::map< loct, std::vector< loct >, goto_programt::target_less_than > incomingt
loct first_loc
exprt return_lhs
exprt replace_nondet_rec(loct, const exprt &, std::vector< symbol_exprt > &nondet_symbols) const
void function_call_symbol(goto_programt::const_targett, encoding_targett &)
symbol_exprt entry_state
exprt evaluate_expr(loct, const exprt &, const exprt &) const
irep_idt function_identifier
symbol_exprt state_expr_with_suffix(loct, const std::string &suffix) const
std::vector< irep_idt > call_stack
exprt assignment_constraint(loct, exprt lhs, exprt rhs) const
std::string state_prefix
std::vector< symbol_exprt > incoming_symbols(loct) const
void operator()(const goto_functionst::function_mapt::const_iterator, encoding_targett &)
static exprt state_lambda_expr(exprt)
exprt forall_states_expr(loct, exprt) const
Definition state.h:696
Definition sentinel_dll.h:15
Definition state.h:456
Definition state.h:760
Definition state.h:518
Expression to hold a symbol (variable)
Definition std_expr.h:132
Symbol table entry.
Definition symbol.h:28
irep_idt name
The unique identifier.
Definition symbol.h:40
An expression with three operands.
Definition std_expr.h:68
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2003
The type of an expression, extends irept.
Definition type.h:29
Definition state.h:148
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
#define CPROVER_PREFIX
void equality_propagation(std::vector< exprt > &constraints)
Equality Propagation.
Symbol Table + CFG.
#define forall_goto_program_instructions(it, program)
static symbol_exprt state_expr()
static exprt simplifying_not(exprt src)
static mathematical_function_typet state_predicate_type()
std::optional< code_with_contract_typet > get_contract(const irep_idt &function_identifier, const namespacet &ns)
Instrument Given Invariants.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
API to expression classes for 'mathematical' expressions.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
API to expression classes for Pointers.
const live_object_exprt & to_live_object_expr(const exprt &expr)
Cast an exprt to a live_object_exprt.
const r_or_w_ok_exprt & to_r_or_w_ok_expr(const exprt &expr)
Definition pointer_expr.h:949
const cstrlen_exprt & to_cstrlen_expr(const exprt &expr)
Cast an exprt to a cstrlen_exprt.
const writeable_object_exprt & to_writeable_object_expr(const exprt &expr)
Cast an exprt to a writeable_object_exprt.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition pointer_expr.h:577
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition pointer_expr.h:93
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition pointer_expr.h:890
const object_size_exprt & to_object_size_expr(const exprt &expr)
Cast an exprt to a object_size_exprt.
const is_dynamic_object_exprt & to_is_dynamic_object_expr(const exprt &expr)
Definition pointer_expr.h:365
exprt simplify_expr(exprt src, const namespacet &ns)
void solver(std::vector< framet > &frames, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const solver_optionst &solver_options, const namespacet &ns, std::vector< propertyt > &properties, std::size_t property_index)
Definition solver.cpp:44
Equality Propagation.
solver_resultt
Definition solver.h:21
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#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
solver_resultt state_encoding_solver(const goto_modelt &goto_model, bool program_is_inlined, std::optional< irep_idt > contract, const solver_optionst &solver_options)
void state_encoding(const goto_modelt &goto_model, bool program_is_inlined, std::optional< irep_idt > contract, encoding_targett &dest)
void variable_encoding(const goto_modelt &goto_model, state_encoding_formatt state_encoding_format, std::ostream &out)
std::set< irep_idt > no_body_warnings
static exprt simplifying_not(exprt src)
State Encoding.
state_encoding_formatt
@ SMT2
@ ASCII
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition std_code.h:1506
exprt conjunction(exprt a, exprt b)
Conjunction of two expressions.
Definition std_expr.cpp:252
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition std_expr.h:828
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1494
const ternary_exprt & to_ternary_expr(const exprt &expr)
Cast an exprt to a ternary_exprt.
Definition std_expr.h:117
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:721
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:424
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2953
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3078
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2408
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:221
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:787
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:517
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:887
A total order over targett and const_targett.
Definition goto_program.h:391
#define size_type
Definition unistd.c:186
Variable Encoding.
dstringt irep_idt

AltStyle によって変換されたページ (->オリジナル) /