cprover
Loading...
Searching...
No Matches
utils.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Utility functions for code contracts.
4
5Author: Saswat Padhi, saspadhi@amazon.com
6
7Date: September 2021
8
9\*******************************************************************/
10
11#include "utils.h"
12
13#include <util/c_types.h>
14#include <util/fresh_symbol.h>
15#include <util/graph.h>
17#include <util/message.h>
18#include <util/pointer_expr.h>
21#include <util/prefix.h>
22#include <util/simplify_expr.h>
23#include <util/symbol.h>
24
25#include <goto-programs/cfg.h>
26
28#include <ansi-c/c_expr.h>
30
32 const source_locationt location,
33 const namespacet &ns,
34 const exprt &expr,
35 goto_programt &dest,
36 const std::function<void()> &havoc_code_impl)
37{
38 goto_programt skip_program;
39 const auto skip_target = skip_program.add(goto_programt::make_skip(location));
40
41 // skip havocing only if all pointer derefs in the expression are valid
42 // (to avoid spurious pointer deref errors)
44 skip_target, not_exprt{all_dereferences_are_valid(expr, ns)}, location));
45
46 havoc_code_impl();
47
48 // add the final skip target
49 dest.destructive_append(skip_program);
50}
51
53 const source_locationt location,
54 const exprt &ptr,
55 const exprt &size,
56 goto_programt &dest)
57{
59 location,
60 ns,
61 ptr,
62 dest,
63 // clang-format off
64 [&]() {
65 symbol_exprt function{CPROVER_PREFIX "havoc_slice", empty_typet()};
66 function.add_source_location() = location;
67 // havoc slice is lowered to array operations during goto conversion
68 // so we use goto_convertt directly as provided by clearnert
69 cleaner.do_havoc_slice(function, {ptr, size}, dest, mode);
70 });
71 // clang-format on
72}
73
75 const source_locationt location,
76 const exprt &ptr_to_ptr,
77 goto_programt &dest)
78{
79 append_safe_havoc_code_for_expr(location, ns, ptr_to_ptr, dest, [&]() {
80 auto ptr = dereference_exprt(ptr_to_ptr);
82 ptr, side_effect_expr_nondett(ptr.type(), location), location));
83 });
84}
85
87 const source_locationt location,
88 const exprt &expr,
89 goto_programt &dest) const
90{
91 append_safe_havoc_code_for_expr(location, ns, expr, dest, [&]() {
93 });
94}
95
97 const source_locationt location,
98 const exprt &expr,
99 goto_programt &dest) const
100{
101 append_safe_havoc_code_for_expr(location, ns, expr, dest, [&]() {
103 });
104}
105
107 const source_locationt location,
108 const exprt &expr,
109 goto_programt &dest)
110{
111 if(expr.id() == ID_pointer_object)
112 {
113 // pointer_object is still used internally to support malloc/free
115 location, to_pointer_object_expr(expr).pointer(), dest);
116 return;
117 }
119 {
120 const auto &funcall = to_side_effect_expr_function_call(expr);
121 // type-checking ensures the function expression is necessarily a symbol
122 const auto &ident = to_symbol_expr(funcall.function()).get_identifier();
123 if(ident == CPROVER_PREFIX "object_whole")
124 {
126 location, funcall.arguments().at(0), dest);
127 }
128 else if(ident == CPROVER_PREFIX "object_from")
129 {
130 const auto ptr = typecast_exprt::conditional_cast(
131 funcall.arguments().at(0), pointer_type(char_type()));
132
133 exprt obj_size = object_size(ptr);
134 minus_exprt size{
135 obj_size,
137
138 append_havoc_slice_code(expr.source_location(), ptr, size, dest);
139 }
140 else if(ident == CPROVER_PREFIX "object_upto")
141 {
142 const auto ptr = typecast_exprt::conditional_cast(
143 funcall.arguments().at(0), pointer_type(char_type()));
144 const auto size = typecast_exprt::conditional_cast(
145 funcall.arguments().at(1), size_type());
146 append_havoc_slice_code(expr.source_location(), ptr, size, dest);
147 }
148 else if(ident == CPROVER_PREFIX "assignable")
149 {
150 const auto &ptr = funcall.arguments().at(0);
151 const auto &size = funcall.arguments().at(1);
152 if(funcall.arguments().at(2).is_true())
153 {
155 }
156 else
157 {
158 append_havoc_slice_code(expr.source_location(), ptr, size, dest);
159 }
160 }
161 else
162 {
164 }
165 }
166 else
167 {
168 // we have an lvalue expression, make nondet assignment
169 havoc_utilst::append_havoc_code_for_expr(location, expr, dest);
170 }
171}
172
174{
175 exprt::operandst validity_checks;
176
177 if(auto deref = expr_try_dynamic_cast<dereference_exprt>(expr))
178 {
179 const auto size_of_expr_opt = size_of_expr(expr.type(), ns);
180 CHECK_RETURN(size_of_expr_opt.has_value());
181
182 validity_checks.push_back(r_ok_exprt{deref->pointer(), *size_of_expr_opt});
183 }
184
185 for(const auto &op : expr.operands())
186 validity_checks.push_back(all_dereferences_are_valid(op, ns));
187
188 return conjunction(validity_checks);
189}
190
192 const std::vector<symbol_exprt> &lhs,
193 const std::vector<symbol_exprt> &rhs)
194{
195 PRECONDITION(lhs.size() == rhs.size());
196
197 if(lhs.empty())
198 {
199 return false_exprt();
200 }
201
202 // Store conjunctions of equalities.
203 // For example, suppose that the two input vectors are <s1, s2, s3> and <l1,
204 // l2, l3>.
205 // Then this vector stores <s1 == l1, s1 == l1 && s2 == l2,
206 // s1 == l1 && s2 == l2 && s3 == l3>.
207 // In fact, the last element is unnecessary, so we do not create it.
208 exprt::operandst equality_conjunctions(lhs.size());
209 equality_conjunctions[0] = binary_relation_exprt(lhs[0], ID_equal, rhs[0]);
210 for(size_t i = 1; i < equality_conjunctions.size() - 1; i++)
211 {
212 binary_relation_exprt component_i_equality{lhs[i], ID_equal, rhs[i]};
213 equality_conjunctions[i] =
214 and_exprt(equality_conjunctions[i - 1], component_i_equality);
215 }
216
217 // Store inequalities between the i-th components of the input vectors
218 // (i.e. lhs and rhs).
219 // For example, suppose that the two input vectors are <s1, s2, s3> and <l1,
220 // l2, l3>.
221 // Then this vector stores <s1 < l1, s1 == l1 && s2 < l2, s1 == l1 &&
222 // s2 == l2 && s3 < l3>.
223 exprt::operandst lexicographic_individual_comparisons(lhs.size());
224 lexicographic_individual_comparisons[0] =
225 binary_relation_exprt(lhs[0], ID_lt, rhs[0]);
226 for(size_t i = 1; i < lexicographic_individual_comparisons.size(); i++)
227 {
228 binary_relation_exprt component_i_less_than{lhs[i], ID_lt, rhs[i]};
229 lexicographic_individual_comparisons[i] =
230 and_exprt(equality_conjunctions[i - 1], component_i_less_than);
231 }
232 return disjunction(lexicographic_individual_comparisons);
233}
234
236 goto_programt &destination,
238 goto_programt &payload)
239{
240 const auto offset = payload.instructions.size();
241 destination.insert_before_swap(target, payload);
242 std::advance(target, offset);
243}
244
246 goto_programt &destination,
249{
250 const auto new_target = destination.insert_before(target, i);
251 for(auto it : target->incoming_edges)
252 {
253 if(it->is_goto() && it->get_target() == target)
254 it->set_target(new_target);
255 }
256}
257
259{
260 for(auto &instruction : goto_program.instructions)
261 {
262 if(
263 instruction.is_goto() &&
264 simplify_expr(instruction.condition(), ns).is_false())
265 instruction.turn_into_skip();
266 }
267}
268
270 const goto_programt &goto_program,
271 namespacet &ns,
272 messaget &log)
273{
274 // create cfg from instruction list
276 cfg(goto_program);
277
278 // check that all nodes are there
279 INVARIANT(
280 goto_program.instructions.size() == cfg.size(),
281 "Instruction list vs CFG size mismatch.");
282
283 // compute SCCs
285 std::vector<idxt> node_to_scc(cfg.size(), -1);
286 auto nof_sccs = cfg.SCCs(node_to_scc);
287
288 // compute size of each SCC
289 std::vector<int> scc_size(nof_sccs, 0);
290 for(auto scc : node_to_scc)
291 {
292 INVARIANT(
293 0 <= scc && scc < nof_sccs, "Could not determine SCC for instruction");
294 scc_size[scc]++;
295 }
296
297 // check they are all of size 1
298 for(size_t scc_id = 0; scc_id < nof_sccs; scc_id++)
299 {
300 auto size = scc_size[scc_id];
301 if(size > 1)
302 {
304 log.error(),
305 [&cfg, &node_to_scc, &scc_id, &size](messaget::mstreamt &mstream) {
306 mstream << "Found CFG SCC with size " << size << messaget::eom;
307 for(const auto &node_id : node_to_scc)
308 {
309 if(node_to_scc[node_id] == scc_id)
310 {
311 const auto &pc = cfg[node_id].PC;
312 pc->output(mstream);
313 mstream << messaget::eom;
314 }
315 }
316 });
317 return false;
318 }
319 }
320 return true;
321}
322
325 " (assigned by the contract of ";
326
328 const exprt &target,
329 const irep_idt &function_id,
330 const namespacet &ns)
331{
332 return from_expr(ns, target.id(), target) +
334}
335
341
343 const local_may_aliast &local_may_alias,
344 const loopt &loop,
345 assignst &assigns)
346{
347 // Assign targets should not include cprover symbols.
348 get_assigns(local_may_alias, loop, assigns, [](const exprt &e) {
349 if(e.id() == ID_symbol)
350 {
351 const auto &s = expr_try_dynamic_cast<symbol_exprt>(e);
352 return !has_prefix(id2string(s->get_identifier()), CPROVER_PREFIX);
353 }
354 return true;
355 });
356}
357
358void widen_assigns(assignst &assigns, const namespacet &ns)
359{
360 assignst result;
361
363
364 for(const auto &e : assigns)
365 {
366 if(e.id() == ID_index || e.id() == ID_dereference)
367 {
368 address_of_exprt address_of_expr(e);
369
370 // index or offset is non-constant.
371 if(!is_constant(address_of_expr))
372 {
373 result.emplace(pointer_object(address_of_expr));
374 }
375 else
376 result.emplace(e);
377 }
378 else
379 result.emplace(e);
380 }
381 assigns = result;
382}
383
385 symbol_table_baset &symbol_table,
386 exprt &expression,
387 const irep_idt &mode)
388{
389 auto visitor = [&symbol_table, &mode](exprt &expr) {
390 if(expr.id() != ID_exists && expr.id() != ID_forall)
391 return;
392 // When a quantifier expression is found, create a fresh symbol for each
393 // quantified variable and rewrite the expression to use those fresh
394 // symbols.
395 auto &quantifier_expression = to_quantifier_expr(expr);
396 std::vector<symbol_exprt> fresh_variables;
397 fresh_variables.reserve(quantifier_expression.variables().size());
398 for(const auto &quantified_variable : quantifier_expression.variables())
399 {
400 // 1. create fresh symbol
401 symbolt new_symbol = get_fresh_aux_symbol(
402 quantified_variable.type(),
403 id2string(quantified_variable.source_location().get_function()),
404 "tmp_cc",
405 quantified_variable.source_location(),
406 mode,
407 symbol_table);
408
409 // 2. add created fresh symbol to expression map
410 fresh_variables.push_back(new_symbol.symbol_expr());
411 }
412
413 // use fresh symbols
414 exprt where = quantifier_expression.instantiate(fresh_variables);
415
416 // recursively check for nested quantified formulae
417 add_quantified_variable(symbol_table, where, mode);
418
419 // replace previous variables and body
420 quantifier_expression.variables() = fresh_variables;
421 quantifier_expression.where() = std::move(where);
422 };
423 expression.visit_pre(visitor);
424}
425
427 symbol_table_baset &symbol_table,
428 exprt &expr,
429 std::unordered_map<exprt, symbol_exprt, irep_hash> &parameter2history,
430 const source_locationt &location,
431 const irep_idt &mode,
432 goto_programt &history,
433 const irep_idt &history_id)
434{
435 for(auto &op : expr.operands())
436 {
438 symbol_table, op, parameter2history, location, mode, history, history_id);
439 }
440
441 if(expr.id() != ID_old && expr.id() != ID_loop_entry)
442 return;
443
444 const auto &parameter = to_history_expr(expr, history_id).expression();
445 const auto &id = parameter.id();
447 id == ID_dereference || id == ID_member || id == ID_symbol ||
448 id == ID_ptrmember || id == ID_constant || id == ID_typecast ||
449 id == ID_index,
450 "Tracking history of " + id2string(id) +
451 " expressions is not supported yet.",
452 parameter.pretty());
453
454 // speculatively insert a dummy, which will be replaced below if the insert
455 // actually happened
456 auto entry =
457 parameter2history.insert({parameter, symbol_exprt::typeless(ID_nil)});
458
459 if(entry.second)
460 {
461 // 1. Create a temporary symbol expression that represents the
462 // history variable
463 entry.first->second = get_fresh_aux_symbol(
464 parameter.type(),
465 id2string(location.get_function()),
466 "tmp_cc",
467 location,
468 mode,
469 symbol_table)
470 .symbol_expr();
471
472 // 2. Add the required instructions to the instructions list
473 // 2.1. Declare the newly created temporary variable
474 history.add(goto_programt::make_decl(entry.first->second, location));
475
476 // 2.2. Skip storing the history if the expression is invalid
477 auto goto_instruction = history.add(goto_programt::make_incomplete_goto(
478 not_exprt{
479 all_dereferences_are_valid(parameter, namespacet(symbol_table))},
480 location));
481
482 // 2.3. Add an assignment such that the value pointed to by the new
483 // temporary variable is equal to the value of the corresponding
484 // parameter
485 history.add(
486 goto_programt::make_assignment(entry.first->second, parameter, location));
487
488 // 2.4. Complete conditional jump for invalid-parameter case
489 auto label_instruction = history.add(goto_programt::make_skip(location));
490 goto_instruction->complete_goto(label_instruction);
491 }
492
493 expr = entry.first->second;
494}
495
497 symbol_table_baset &symbol_table,
498 const exprt &expr,
499 const source_locationt &location,
500 const irep_idt &mode)
501{
503 result.expression_after_replacement = expr;
505 symbol_table,
508 location,
509 mode,
511 ID_old);
512 return result;
513}
514
516 symbol_table_baset &symbol_table,
517 const exprt &expr,
518 const source_locationt &location,
519 const irep_idt &mode)
520{
522 result.expression_after_replacement = expr;
524 symbol_table,
527 location,
528 mode,
530 ID_loop_entry);
531 return result;
532}
533
535 symbol_table_baset &symbol_table,
536 exprt &clause,
537 const irep_idt &mode,
538 goto_programt &program)
539{
540 // Find and replace "old" expression in the "expression" variable
541 auto result =
542 replace_history_old(symbol_table, clause, clause.source_location(), mode);
543 clause.swap(result.expression_after_replacement);
544 // Add all the history variable initialization instructions
545 program.destructive_append(result.history_construction);
546}
547
549{
550 // The head of a transformed loop is
551 // ASSIGN entered_loop = false
553 target->assign_rhs() == false_exprt();
554}
555
557{
558 // The end of a transformed loop is
559 // ASSIGN entered_loop = true
561 target->assign_rhs() == true_exprt();
562}
563
565 const goto_programt::const_targett &target,
566 std::string var_name)
567{
568 INVARIANT(
569 var_name == IN_BASE_CASE || var_name == ENTERED_LOOP ||
570 var_name == IN_LOOP_HAVOC_BLOCK,
571 "var_name is not of instrumented variables.");
572
573 if(!target->is_assign())
574 return false;
575
576 if(can_cast_expr<symbol_exprt>(target->assign_lhs()))
577 {
578 const auto &lhs = to_symbol_expr(target->assign_lhs());
579 return id2string(lhs.get_identifier()).find("::" + var_name) !=
580 std::string::npos;
581 }
582
583 return false;
584}
585
586unsigned get_suffix_unsigned(const std::string &str, const std::string &prefix)
587{
588 // first_index is the end of the `prefix`.
589 auto first_index = str.find(prefix);
590 INVARIANT(
591 first_index != std::string::npos, "Prefix not found in the given string");
592 first_index += prefix.length();
593
594 // last_index is the index of not-digit.
595 auto last_index = str.find_first_not_of("0123456789", first_index);
596 std::string result = str.substr(first_index, last_index - first_index);
597 return std::stol(result);
598}
599
601 const goto_programt::const_targett &loop_head,
602 const loop_templatet<
605{
606 goto_programt::const_targett loop_end = loop_head;
607 for(const auto &t : loop)
608 {
609 // an instruction is the loop end if it is a goto instruction
610 // and it jumps backward to the loop head
611 if(
612 t->is_goto() && t->get_target() == loop_head &&
613 t->location_number > loop_end->location_number)
614 loop_end = t;
615 }
616 INVARIANT(
617 loop_head != loop_end,
618 "Could not find end of the loop starting at: " +
619 loop_head->source_location().as_string());
620
621 return loop_end;
622}
623
625 const goto_programt::targett &loop_head,
627 &loop)
628{
629 goto_programt::targett loop_end = loop_head;
630 for(const auto &t : loop)
631 {
632 // an instruction is the loop end if it is a goto instruction
633 // and it jumps backward to the loop head
634 if(
635 t->is_goto() && t->get_target() == loop_head &&
636 t->location_number > loop_end->location_number)
637 loop_end = t;
638 }
639 INVARIANT(
640 loop_head != loop_end,
641 "Could not find end of the loop starting at: " +
642 loop_head->source_location().as_string());
643
644 return loop_end;
645}
646
648 const unsigned int target_loop_number,
649 goto_functiont &function,
650 bool finding_head)
651{
652 natural_loops_mutablet natural_loops(function.body);
653
654 // iterate over all natural loops to find the loop with `target_loop_number`
655 for(const auto &loop_p : natural_loops.loop_map)
656 {
657 const goto_programt::targett loop_head = loop_p.first;
658 goto_programt::targett loop_end =
659 get_loop_end_from_loop_head_and_content_mutable(loop_head, loop_p.second);
660 // check if the current loop is the target loop by comparing loop number
661 if(loop_end->loop_number == target_loop_number)
662 {
663 if(finding_head)
664 return loop_head;
665 else
666 return loop_end;
667 }
668 }
669
671}
672
674get_loop_end(const unsigned int target_loop_number, goto_functiont &function)
675{
676 return get_loop_head_or_end(target_loop_number, function, false);
677}
678
680get_loop_head(const unsigned int target_loop_number, goto_functiont &function)
681{
682 return get_loop_head_or_end(target_loop_number, function, true);
683}
684
686static exprt
688{
689 return static_cast<const exprt &>(
690 loop_end->condition().find(ID_C_spec_loop_invariant));
691}
692
694{
695 return static_cast<const exprt &>(
696 loop_end->condition().find(ID_C_spec_assigns));
697}
698
699static exprt
701{
702 return static_cast<const exprt &>(
703 loop_end->condition().find(ID_C_spec_decreases));
704}
705
707 const goto_programt::const_targett &loop_end,
708 const bool check_side_effect)
709{
710 auto invariant = extract_loop_invariants(loop_end);
711 if(!invariant.is_nil() && check_side_effect)
712 {
713 if(has_subexpr(invariant, ID_side_effect))
714 {
716 "Loop invariant is not side-effect free.",
717 loop_end->condition().find_source_location());
718 }
719 }
720 return invariant;
721}
722
724{
725 return extract_loop_assigns(loop_end);
726}
727
729 const goto_programt::const_targett &loop_end,
730 const bool check_side_effect)
731{
732 auto decreases_clause = extract_loop_decreases(loop_end);
733 if(!decreases_clause.is_nil() && check_side_effect)
734 {
735 if(has_subexpr(decreases_clause, ID_side_effect))
736 {
738 "Decreases clause is not side-effect free.",
739 loop_end->condition().find_source_location());
740 }
741 }
742 return decreases_clause;
743}
744
746 const invariant_mapt &invariant_map,
747 goto_modelt &goto_model)
748{
749 for(const auto &invariant_map_entry : invariant_map)
750 {
751 loop_idt loop_id = invariant_map_entry.first;
752 irep_idt function_id = loop_id.function_id;
753 unsigned int loop_number = loop_id.loop_number;
754
755 // get the last instruction of the target loop
756 auto &function = goto_model.goto_functions.function_map[function_id];
757 goto_programt::targett loop_end = get_loop_end(loop_number, function);
758
759 // annotate the invariant to the condition of `loop_end`
760 loop_end->condition_nonconst().add(ID_C_spec_loop_invariant) =
761 invariant_map_entry.second;
762 }
763}
764
766 const std::map<loop_idt, std::set<exprt>> &assigns_map,
767 goto_modelt &goto_model)
768{
769 for(const auto &assigns_map_entry : assigns_map)
770 {
771 loop_idt loop_id = assigns_map_entry.first;
772 irep_idt function_id = loop_id.function_id;
773 unsigned int loop_number = loop_id.loop_number;
774
775 // get the last instruction of the target loop
776 auto &function = goto_model.goto_functions.function_map[function_id];
777 goto_programt::targett loop_end = get_loop_end(loop_number, function);
778
779 exprt &condition = loop_end->condition_nonconst();
780 auto assigns = exprt(ID_target_list);
781 for(const auto &e : assigns_map_entry.second)
782 assigns.add_to_operands(e);
783 condition.add(ID_C_spec_assigns) = assigns;
784 }
785}
786
788 const std::map<loop_idt, exprt> &assigns_map,
789 goto_modelt &goto_model)
790{
791 for(const auto &assigns_map_entry : assigns_map)
792 {
793 loop_idt loop_id = assigns_map_entry.first;
794 irep_idt function_id = loop_id.function_id;
795 unsigned int loop_number = loop_id.loop_number;
796
797 // get the last instruction of the target loop
798 auto &function = goto_model.goto_functions.function_map[function_id];
799 goto_programt::targett loop_end = get_loop_end(loop_number, function);
800
801 exprt &condition = loop_end->condition_nonconst();
802 condition.add(ID_C_spec_assigns) = assigns_map_entry.second;
803 }
804}
805
807 const std::map<loop_idt, std::vector<exprt>> &decreases_map,
808 goto_modelt &goto_model)
809{
810 for(const auto &decreases_map_entry : decreases_map)
811 {
812 loop_idt loop_id = decreases_map_entry.first;
813 irep_idt function_id = loop_id.function_id;
814 unsigned int loop_number = loop_id.loop_number;
815
816 // get the last instruction of the target loop
817 auto &function = goto_model.goto_functions.function_map[function_id];
818 goto_programt::targett loop_end = get_loop_end(loop_number, function);
819
820 exprt &condition = loop_end->condition_nonconst();
821 auto decreases = exprt(ID_target_list);
822 for(const auto &e : decreases_map_entry.second)
823 decreases.add_to_operands(e);
824 condition.add(ID_C_spec_decreases) = decreases;
825 }
826}
API to expression classes that are internal to the C frontend.
const history_exprt & to_history_expr(const exprt &expr, const irep_idt &id)
Definition c_expr.h:220
unsignedbv_typet size_type()
Definition c_types.cpp:50
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
bitvector_typet char_type()
Definition c_types.cpp:106
Control Flow Graph.
Operator to return the address of an object.
Boolean AND.
Definition std_expr.h:2120
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:762
A multi-procedural control flow graph (CFG) whose nodes store references to instructions in a GOTO pr...
Definition cfg.h:87
void do_havoc_slice(const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
Definition utils.h:54
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
The empty type.
Definition std_types.h:51
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:34
void visit_pre(std::function< void(exprt &)>)
Definition expr.cpp:227
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
const source_locationt & source_location() const
Definition expr.h:231
source_locationt & add_source_location()
Definition expr.h:236
The Boolean constant false.
Definition std_expr.h:3064
function_mapt function_map
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
goto_programt body
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
This class represents an instruction in the GOTO intermediate representation.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
instructionst::iterator targett
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
instructionst::const_iterator const_targett
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
std::size_t node_indext
Definition graph.h:37
std::size_t SCCs(std::vector< node_indext > &subgraph_nr) const
Computes strongly-connected components of a graph and yields a vector expressing a mapping from nodes...
Definition graph.h:832
std::size_t size() const
Definition graph.h:212
void append_havoc_pointer_code(const source_locationt location, const exprt &ptr_to_ptr, goto_programt &dest)
Definition utils.cpp:74
void append_havoc_slice_code(const source_locationt location, const exprt &ptr, const exprt &size, goto_programt &dest)
Definition utils.cpp:52
const irep_idt & mode
Definition utils.h:126
void append_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest)
Append goto instructions to havoc a single expression expr
Definition utils.cpp:106
void append_object_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const override
Append goto instructions to havoc the underlying object of expr
Definition utils.cpp:86
const namespacet & ns
Definition utils.h:86
void append_scalar_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const override
Append goto instructions to havoc the value of expr
Definition utils.cpp:96
A class containing utility functions for havocing expressions.
Definition havoc_utils.h:28
virtual void append_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest)
Append goto instructions to havoc a single expression expr
virtual void append_object_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const
Append goto instructions to havoc the underlying object of expr
virtual void append_scalar_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const
Append goto instructions to havoc the value of expr
const exprt & expression() const
Definition c_expr.h:213
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
void swap(irept &irep)
Definition irep.h:434
const irep_idt & id() const
Definition irep.h:388
irept & add(const irep_idt &name)
Definition irep.cpp:103
loop_mapt loop_map
A loop, specified as a set of instructions.
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
mstreamt & error() const
Definition message.h:391
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
Binary minus.
Definition std_expr.h:1061
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:94
Boolean negation.
Definition std_expr.h:2327
A predicate that indicates that an address range is ok to read.
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
const irep_idt & get_function() const
Expression to hold a symbol (variable)
Definition std_expr.h:131
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition std_expr.h:150
const irep_idt & get_identifier() const
Definition std_expr.h:160
The symbol table base class interface.
Symbol table entry.
Definition symbol.h:28
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
The Boolean constant true.
Definition std_expr.h:3055
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2076
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
#define CPROVER_PREFIX
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition expr_cast.h:81
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
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.
A Template Class for Graphs.
std::set< exprt > assignst
Definition havoc_utils.h:24
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
void get_assigns(const local_may_aliast &local_may_alias, const loopt &loop, assignst &assigns)
natural_loops_mutablet::natural_loopt loopt
Definition loop_utils.h:20
API to expression classes for 'mathematical' expressions.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
Compute natural loops in a goto_function.
API to expression classes for Pointers.
const pointer_object_exprt & to_pointer_object_expr(const exprt &expr)
Cast an exprt to a pointer_object_exprt.
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
Pointer Logic.
exprt pointer_offset(const exprt &pointer)
exprt object_size(const exprt &pointer)
exprt pointer_object(const exprt &p)
Various predicates over pointers in programs.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#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
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition std_code.h:1739
bool can_cast_expr< side_effect_expr_function_callt >(const exprt &base)
Definition std_code.h:1730
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:66
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:54
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition std_expr.h:256
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition std_types.h:29
A total order over targett and const_targett.
Loop id used to identify loops.
Definition loop_ids.h:28
irep_idt function_id
Definition loop_ids.h:36
unsigned int loop_number
Definition loop_ids.h:37
std::unordered_map< exprt, symbol_exprt, irep_hash > parameter_to_history
Definition utils.h:247
goto_programt history_construction
Definition utils.h:248
exprt expression_after_replacement
Definition utils.h:246
Symbol table entry.
replace_history_parametert replace_history_old(symbol_table_baset &symbol_table, const exprt &expr, const source_locationt &location, const irep_idt &mode)
This function recursively identifies the "old" expressions within expr and replaces them with corresp...
Definition utils.cpp:496
void generate_history_variables_initialization(symbol_table_baset &symbol_table, exprt &clause, const irep_idt &mode, goto_programt &program)
This function generates all the instructions required to initialize history variables.
Definition utils.cpp:534
bool is_assignment_to_instrumented_variable(const goto_programt::const_targett &target, std::string var_name)
Return true if target is an assignment to an instrumented variable with name var_name.
Definition utils.cpp:564
irep_idt make_assigns_clause_replacement_tracking_comment(const exprt &target, const irep_idt &function_id, const namespacet &ns)
Returns an irep_idt that essentially says that target was assigned by the contract of function_id.
Definition utils.cpp:327
goto_programt::targett get_loop_end(const unsigned int target_loop_number, goto_functiont &function)
Find and return the last instruction of the natural loop with loop_number in function.
Definition utils.cpp:674
static void append_safe_havoc_code_for_expr(const source_locationt location, const namespacet &ns, const exprt &expr, goto_programt &dest, const std::function< void()> &havoc_code_impl)
Definition utils.cpp:31
goto_programt::const_targett get_loop_end_from_loop_head_and_content(const goto_programt::const_targett &loop_head, const loop_templatet< goto_programt::const_targett, goto_programt::target_less_than > &loop)
Definition utils.cpp:600
void insert_before_and_update_jumps(goto_programt &destination, goto_programt::targett &target, const goto_programt::instructiont &i)
Insert a goto instruction before a target instruction iterator and update targets of all jumps that p...
Definition utils.cpp:245
void add_quantified_variable(symbol_table_baset &symbol_table, exprt &expression, const irep_idt &mode)
This function recursively searches expression to find nested or non-nested quantified expressions.
Definition utils.cpp:384
void infer_loop_assigns(const local_may_aliast &local_may_alias, const loopt &loop, assignst &assigns)
Infer loop assigns using alias analysis result local_may_alias.
Definition utils.cpp:342
bool is_loop_free(const goto_programt &goto_program, namespacet &ns, messaget &log)
Returns true iff the given program is loop-free, i.e.
Definition utils.cpp:269
exprt get_loop_assigns(const goto_programt::const_targett &loop_end)
Definition utils.cpp:723
replace_history_parametert replace_history_loop_entry(symbol_table_baset &symbol_table, const exprt &expr, const source_locationt &location, const irep_idt &mode)
This function recursively identifies the "loop_entry" expressions within expr and replaces them with ...
Definition utils.cpp:515
goto_programt::targett get_loop_head(const unsigned int target_loop_number, goto_functiont &function)
Find and return the first instruction of the natural loop with loop_number in function.
Definition utils.cpp:680
bool is_transformed_loop_head(const goto_programt::const_targett &target)
Return true if target is the head of some transformed loop.
Definition utils.cpp:548
exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns)
Generate a validity check over all dereferences in an expression.
Definition utils.cpp:173
void annotate_decreases(const std::map< loop_idt, std::vector< exprt > > &decreases_map, goto_modelt &goto_model)
Annotate the decreases in decreases_map to their corresponding loops.
Definition utils.cpp:806
bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment)
Returns true if the given comment matches the type of comments created by make_assigns_clause_replace...
Definition utils.cpp:336
void annotate_assigns(const std::map< loop_idt, std::set< exprt > > &assigns_map, goto_modelt &goto_model)
Annotate the assigns in assigns_map to their corresponding loops.
Definition utils.cpp:765
goto_programt::targett get_loop_head_or_end(const unsigned int target_loop_number, goto_functiont &function, bool finding_head)
Return loop head if finding_head is true, Otherwise return loop end.
Definition utils.cpp:647
void insert_before_swap_and_advance(goto_programt &destination, goto_programt::targett &target, goto_programt &payload)
Insert a goto program before a target instruction iterator and advance the iterator.
Definition utils.cpp:235
static exprt extract_loop_assigns(const goto_programt::const_targett &loop_end)
Definition utils.cpp:693
void widen_assigns(assignst &assigns, const namespacet &ns)
Widen expressions in assigns with the following strategy.
Definition utils.cpp:358
exprt get_loop_invariants(const goto_programt::const_targett &loop_end, const bool check_side_effect)
Definition utils.cpp:706
bool is_transformed_loop_end(const goto_programt::const_targett &target)
Return true if target is the end of some transformed loop.
Definition utils.cpp:556
goto_programt::targett get_loop_end_from_loop_head_and_content_mutable(const goto_programt::targett &loop_head, const loop_templatet< goto_programt::targett, goto_programt::target_less_than > &loop)
Find the goto instruction of loop that jumps to loop_head
Definition utils.cpp:624
void annotate_invariants(const invariant_mapt &invariant_map, goto_modelt &goto_model)
Annotate the invariants in invariant_map to their corresponding loops.
Definition utils.cpp:745
static void replace_history_parameter_rec(symbol_table_baset &symbol_table, exprt &expr, std::unordered_map< exprt, symbol_exprt, irep_hash > &parameter2history, const source_locationt &location, const irep_idt &mode, goto_programt &history, const irep_idt &history_id)
Definition utils.cpp:426
void simplify_gotos(goto_programt &goto_program, namespacet &ns)
Turns goto instructions IF cond GOTO label where the condition statically simplifies to false into SK...
Definition utils.cpp:258
static const char ASSIGNS_CLAUSE_REPLACEMENT_TRACKING[]
Prefix for comments added to track assigns clause replacement.
Definition utils.cpp:324
static exprt extract_loop_decreases(const goto_programt::const_targett &loop_end)
Definition utils.cpp:700
exprt get_loop_decreases(const goto_programt::const_targett &loop_end, const bool check_side_effect)
Extract loop invariants from annotated loop end.
Definition utils.cpp:728
unsigned get_suffix_unsigned(const std::string &str, const std::string &prefix)
Convert the suffix digits right after prefix of str into unsigned.
Definition utils.cpp:586
exprt generate_lexicographic_less_than_check(const std::vector< symbol_exprt > &lhs, const std::vector< symbol_exprt > &rhs)
Generate a lexicographic less-than comparison over ordered tuples.
Definition utils.cpp:191
static exprt extract_loop_invariants(const goto_programt::const_targett &loop_end)
Extract loop invariants from loop end without any checks.
Definition utils.cpp:687
#define ENTERED_LOOP
Definition utils.h:26
std::map< loop_idt, exprt > invariant_mapt
Definition utils.h:32
#define IN_BASE_CASE
Definition utils.h:25
#define IN_LOOP_HAVOC_BLOCK
Definition utils.h:27