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/simplify_expr.h>
22#include <util/symbol.h>
23
24#include <goto-programs/cfg.h>
25
27#include <ansi-c/c_expr.h>
29
31 const source_locationt location,
32 const namespacet &ns,
33 const exprt &expr,
34 goto_programt &dest,
35 const std::function<void()> &havoc_code_impl)
36{
37 goto_programt skip_program;
38 const auto skip_target = skip_program.add(goto_programt::make_skip(location));
39
40 // skip havocing only if all pointer derefs in the expression are valid
41 // (to avoid spurious pointer deref errors)
43 skip_target, not_exprt{all_dereferences_are_valid(expr, ns)}, location));
44
45 havoc_code_impl();
46
47 // add the final skip target
48 dest.destructive_append(skip_program);
49}
50
52 const source_locationt location,
53 const exprt &ptr,
54 const exprt &size,
55 goto_programt &dest)
56{
58 location,
59 ns,
60 ptr,
61 dest,
62 // clang-format off
63 [&]() {
64 symbol_exprt function{CPROVER_PREFIX "havoc_slice", empty_typet()};
65 function.add_source_location() = location;
66 // havoc slice is lowered to array operations during goto conversion
67 // so we use goto_convertt directly as provided by clearnert
68 cleaner.do_havoc_slice(function, {ptr, size}, dest, mode);
69 });
70 // clang-format on
71}
72
74 const source_locationt location,
75 const exprt &ptr_to_ptr,
76 goto_programt &dest)
77{
78 append_safe_havoc_code_for_expr(location, ns, ptr_to_ptr, dest, [&]() {
79 auto ptr = dereference_exprt(ptr_to_ptr);
81 ptr, side_effect_expr_nondett(ptr.type(), location), location));
82 });
83}
84
86 const source_locationt location,
87 const exprt &expr,
88 goto_programt &dest) const
89{
90 append_safe_havoc_code_for_expr(location, ns, expr, dest, [&]() {
92 });
93}
94
96 const source_locationt location,
97 const exprt &expr,
98 goto_programt &dest) const
99{
100 append_safe_havoc_code_for_expr(location, ns, expr, dest, [&]() {
102 });
103}
104
106 const source_locationt location,
107 const exprt &expr,
108 goto_programt &dest)
109{
110 if(expr.id() == ID_pointer_object)
111 {
112 // pointer_object is still used internally to support malloc/free
114 location, to_pointer_object_expr(expr).pointer(), dest);
115 return;
116 }
118 {
119 const auto &funcall = to_side_effect_expr_function_call(expr);
120 // type-checking ensures the function expression is necessarily a symbol
121 const auto &ident = to_symbol_expr(funcall.function()).get_identifier();
122 if(ident == CPROVER_PREFIX "object_whole")
123 {
125 location, funcall.arguments().at(0), dest);
126 }
127 else if(ident == CPROVER_PREFIX "object_from")
128 {
129 const auto ptr = typecast_exprt::conditional_cast(
130 funcall.arguments().at(0), pointer_type(char_type()));
131
132 exprt obj_size = object_size(ptr);
133 minus_exprt size{
134 obj_size,
136
137 append_havoc_slice_code(expr.source_location(), ptr, size, dest);
138 }
139 else if(ident == CPROVER_PREFIX "object_upto")
140 {
141 const auto ptr = typecast_exprt::conditional_cast(
142 funcall.arguments().at(0), pointer_type(char_type()));
143 const auto size = typecast_exprt::conditional_cast(
144 funcall.arguments().at(1), size_type());
145 append_havoc_slice_code(expr.source_location(), ptr, size, dest);
146 }
147 else if(ident == CPROVER_PREFIX "assignable")
148 {
149 const auto &ptr = funcall.arguments().at(0);
150 const auto &size = funcall.arguments().at(1);
151 if(funcall.arguments().at(2).is_true())
152 {
154 }
155 else
156 {
157 append_havoc_slice_code(expr.source_location(), ptr, size, dest);
158 }
159 }
160 else
161 {
163 }
164 }
165 else
166 {
167 // we have an lvalue expression, make nondet assignment
168 havoc_utilst::append_havoc_code_for_expr(location, expr, dest);
169 }
170}
171
173{
174 exprt::operandst validity_checks;
175
176 if(auto deref = expr_try_dynamic_cast<dereference_exprt>(expr))
177 {
178 const auto size_of_expr_opt = size_of_expr(expr.type(), ns);
179 CHECK_RETURN(size_of_expr_opt.has_value());
180
181 validity_checks.push_back(r_ok_exprt{deref->pointer(), *size_of_expr_opt});
182 }
183
184 for(const auto &op : expr.operands())
185 validity_checks.push_back(all_dereferences_are_valid(op, ns));
186
187 return conjunction(validity_checks);
188}
189
191 const std::vector<symbol_exprt> &lhs,
192 const std::vector<symbol_exprt> &rhs)
193{
194 PRECONDITION(lhs.size() == rhs.size());
195
196 if(lhs.empty())
197 {
198 return false_exprt();
199 }
200
201 // Store conjunctions of equalities.
202 // For example, suppose that the two input vectors are <s1, s2, s3> and <l1,
203 // l2, l3>.
204 // Then this vector stores <s1 == l1, s1 == l1 && s2 == l2,
205 // s1 == l1 && s2 == l2 && s3 == l3>.
206 // In fact, the last element is unnecessary, so we do not create it.
207 exprt::operandst equality_conjunctions(lhs.size());
208 equality_conjunctions[0] = binary_relation_exprt(lhs[0], ID_equal, rhs[0]);
209 for(size_t i = 1; i < equality_conjunctions.size() - 1; i++)
210 {
211 binary_relation_exprt component_i_equality{lhs[i], ID_equal, rhs[i]};
212 equality_conjunctions[i] =
213 and_exprt(equality_conjunctions[i - 1], component_i_equality);
214 }
215
216 // Store inequalities between the i-th components of the input vectors
217 // (i.e. lhs and rhs).
218 // For example, suppose that the two input vectors are <s1, s2, s3> and <l1,
219 // l2, l3>.
220 // Then this vector stores <s1 < l1, s1 == l1 && s2 < l2, s1 == l1 &&
221 // s2 == l2 && s3 < l3>.
222 exprt::operandst lexicographic_individual_comparisons(lhs.size());
223 lexicographic_individual_comparisons[0] =
224 binary_relation_exprt(lhs[0], ID_lt, rhs[0]);
225 for(size_t i = 1; i < lexicographic_individual_comparisons.size(); i++)
226 {
227 binary_relation_exprt component_i_less_than{lhs[i], ID_lt, rhs[i]};
228 lexicographic_individual_comparisons[i] =
229 and_exprt(equality_conjunctions[i - 1], component_i_less_than);
230 }
231 return disjunction(lexicographic_individual_comparisons);
232}
233
235 goto_programt &destination,
237 goto_programt &payload)
238{
239 const auto offset = payload.instructions.size();
240 destination.insert_before_swap(target, payload);
241 std::advance(target, offset);
242}
243
245 goto_programt &destination,
248{
249 const auto new_target = destination.insert_before(target, i);
250 for(auto it : target->incoming_edges)
251 {
252 if(it->is_goto())
253 it->set_target(new_target);
254 }
255}
256
258{
259 for(auto &instruction : goto_program.instructions)
260 {
261 if(
262 instruction.is_goto() &&
263 simplify_expr(instruction.condition(), ns).is_false())
264 instruction.turn_into_skip();
265 }
266}
267
269 const goto_programt &goto_program,
270 namespacet &ns,
271 messaget &log)
272{
273 // create cfg from instruction list
275 cfg(goto_program);
276
277 // check that all nodes are there
278 INVARIANT(
279 goto_program.instructions.size() == cfg.size(),
280 "Instruction list vs CFG size mismatch.");
281
282 // compute SCCs
284 std::vector<idxt> node_to_scc(cfg.size(), -1);
285 auto nof_sccs = cfg.SCCs(node_to_scc);
286
287 // compute size of each SCC
288 std::vector<int> scc_size(nof_sccs, 0);
289 for(auto scc : node_to_scc)
290 {
291 INVARIANT(
292 0 <= scc && scc < nof_sccs, "Could not determine SCC for instruction");
293 scc_size[scc]++;
294 }
295
296 // check they are all of size 1
297 for(size_t scc_id = 0; scc_id < nof_sccs; scc_id++)
298 {
299 auto size = scc_size[scc_id];
300 if(size > 1)
301 {
303 log.error(),
304 [&cfg, &node_to_scc, &scc_id, &size](messaget::mstreamt &mstream) {
305 mstream << "Found CFG SCC with size " << size << messaget::eom;
306 for(const auto &node_id : node_to_scc)
307 {
308 if(node_to_scc[node_id] == scc_id)
309 {
310 const auto &pc = cfg[node_id].PC;
311 pc->output(mstream);
312 mstream << messaget::eom;
313 }
314 }
315 });
316 return false;
317 }
318 }
319 return true;
320}
321
324 " (assigned by the contract of ";
325
327 const exprt &target,
328 const irep_idt &function_id,
329 const namespacet &ns)
330{
331 return from_expr(ns, target.id(), target) +
333}
334
340
341void widen_assigns(assignst &assigns, const namespacet &ns)
342{
343 assignst result;
344
346
347 for(const auto &e : assigns)
348 {
349 if(e.id() == ID_index || e.id() == ID_dereference)
350 {
351 address_of_exprt address_of_expr(e);
352
353 // index or offset is non-constant.
354 if(!is_constant(address_of_expr))
355 {
356 result.emplace(pointer_object(address_of_expr));
357 }
358 else
359 result.emplace(e);
360 }
361 else
362 result.emplace(e);
363 }
364 assigns = result;
365}
366
368 symbol_table_baset &symbol_table,
369 exprt &expression,
370 const irep_idt &mode)
371{
372 if(expression.id() == ID_not || expression.id() == ID_typecast)
373 {
374 // For unary connectives, recursively check for
375 // nested quantified formulae in the term
376 auto &unary_expression = to_unary_expr(expression);
377 add_quantified_variable(symbol_table, unary_expression.op(), mode);
378 }
379 if(expression.id() == ID_notequal || expression.id() == ID_implies)
380 {
381 // For binary connectives, recursively check for
382 // nested quantified formulae in the left and right terms
383 auto &binary_expression = to_binary_expr(expression);
384 add_quantified_variable(symbol_table, binary_expression.lhs(), mode);
385 add_quantified_variable(symbol_table, binary_expression.rhs(), mode);
386 }
387 if(expression.id() == ID_if)
388 {
389 // For ternary connectives, recursively check for
390 // nested quantified formulae in all three terms
391 auto &if_expression = to_if_expr(expression);
392 add_quantified_variable(symbol_table, if_expression.cond(), mode);
393 add_quantified_variable(symbol_table, if_expression.true_case(), mode);
394 add_quantified_variable(symbol_table, if_expression.false_case(), mode);
395 }
396 if(expression.id() == ID_and || expression.id() == ID_or)
397 {
398 // For multi-ary connectives, recursively check for
399 // nested quantified formulae in all terms
400 auto &multi_ary_expression = to_multi_ary_expr(expression);
401 for(auto &operand : multi_ary_expression.operands())
402 {
403 add_quantified_variable(symbol_table, operand, mode);
404 }
405 }
406 else if(expression.id() == ID_exists || expression.id() == ID_forall)
407 {
408 // When a quantifier expression is found, create a fresh symbol for each
409 // quantified variable and rewrite the expression to use those fresh
410 // symbols.
411 auto &quantifier_expression = to_quantifier_expr(expression);
412 std::vector<symbol_exprt> fresh_variables;
413 fresh_variables.reserve(quantifier_expression.variables().size());
414 for(const auto &quantified_variable : quantifier_expression.variables())
415 {
416 // 1. create fresh symbol
417 symbolt new_symbol = get_fresh_aux_symbol(
418 quantified_variable.type(),
419 id2string(quantified_variable.source_location().get_function()),
420 "tmp_cc",
421 quantified_variable.source_location(),
422 mode,
423 symbol_table);
424
425 // 2. add created fresh symbol to expression map
426 fresh_variables.push_back(new_symbol.symbol_expr());
427 }
428
429 // use fresh symbols
430 exprt where = quantifier_expression.instantiate(fresh_variables);
431
432 // recursively check for nested quantified formulae
433 add_quantified_variable(symbol_table, where, mode);
434
435 // replace previous variables and body
436 quantifier_expression.variables() = fresh_variables;
437 quantifier_expression.where() = std::move(where);
438 }
439}
440
442 symbol_table_baset &symbol_table,
443 exprt &expr,
444 std::unordered_map<exprt, symbol_exprt, irep_hash> &parameter2history,
445 const source_locationt &location,
446 const irep_idt &mode,
447 goto_programt &history,
448 const irep_idt &history_id)
449{
450 for(auto &op : expr.operands())
451 {
453 symbol_table, op, parameter2history, location, mode, history, history_id);
454 }
455
456 if(expr.id() != ID_old && expr.id() != ID_loop_entry)
457 return;
458
459 const auto &parameter = to_history_expr(expr, history_id).expression();
460 const auto &id = parameter.id();
462 id == ID_dereference || id == ID_member || id == ID_symbol ||
463 id == ID_ptrmember || id == ID_constant || id == ID_typecast ||
464 id == ID_index,
465 "Tracking history of " + id2string(id) +
466 " expressions is not supported yet.",
467 parameter.pretty());
468
469 // speculatively insert a dummy, which will be replaced below if the insert
470 // actually happened
471 auto entry =
472 parameter2history.insert({parameter, symbol_exprt::typeless(ID_nil)});
473
474 if(entry.second)
475 {
476 // 1. Create a temporary symbol expression that represents the
477 // history variable
478 entry.first->second = get_fresh_aux_symbol(
479 parameter.type(),
480 id2string(location.get_function()),
481 "tmp_cc",
482 location,
483 mode,
484 symbol_table)
485 .symbol_expr();
486
487 // 2. Add the required instructions to the instructions list
488 // 2.1. Declare the newly created temporary variable
489 history.add(goto_programt::make_decl(entry.first->second, location));
490
491 // 2.2. Skip storing the history if the expression is invalid
492 auto goto_instruction = history.add(goto_programt::make_incomplete_goto(
493 not_exprt{
494 all_dereferences_are_valid(parameter, namespacet(symbol_table))},
495 location));
496
497 // 2.3. Add an assignment such that the value pointed to by the new
498 // temporary variable is equal to the value of the corresponding
499 // parameter
500 history.add(
501 goto_programt::make_assignment(entry.first->second, parameter, location));
502
503 // 2.4. Complete conditional jump for invalid-parameter case
504 auto label_instruction = history.add(goto_programt::make_skip(location));
505 goto_instruction->complete_goto(label_instruction);
506 }
507
508 expr = entry.first->second;
509}
510
512 symbol_table_baset &symbol_table,
513 const exprt &expr,
514 const source_locationt &location,
515 const irep_idt &mode)
516{
518 result.expression_after_replacement = expr;
520 symbol_table,
523 location,
524 mode,
526 ID_old);
527 return result;
528}
529
531 symbol_table_baset &symbol_table,
532 const exprt &expr,
533 const source_locationt &location,
534 const irep_idt &mode)
535{
537 result.expression_after_replacement = expr;
539 symbol_table,
542 location,
543 mode,
545 ID_loop_entry);
546 return result;
547}
548
550 symbol_table_baset &symbol_table,
551 exprt &clause,
552 const irep_idt &mode,
553 goto_programt &program)
554{
555 // Find and replace "old" expression in the "expression" variable
556 auto result =
557 replace_history_old(symbol_table, clause, clause.source_location(), mode);
558 clause.swap(result.expression_after_replacement);
559 // Add all the history variable initialization instructions
560 program.destructive_append(result.history_construction);
561}
562
564{
565 // The head of a transformed loop is
566 // ASSIGN entered_loop = false
568 target->assign_rhs() == false_exprt();
569}
570
572{
573 // The end of a transformed loop is
574 // ASSIGN entered_loop = true
576 target->assign_rhs() == true_exprt();
577}
578
580 const goto_programt::const_targett &target,
581 std::string var_name)
582{
583 INVARIANT(
584 var_name == IN_BASE_CASE || var_name == ENTERED_LOOP ||
585 var_name == IN_LOOP_HAVOC_BLOCK,
586 "var_name is not of instrumented variables.");
587
588 if(!target->is_assign())
589 return false;
590
591 if(can_cast_expr<symbol_exprt>(target->assign_lhs()))
592 {
593 const auto &lhs = to_symbol_expr(target->assign_lhs());
594 return id2string(lhs.get_identifier()).find("::" + var_name) !=
595 std::string::npos;
596 }
597
598 return false;
599}
600
601unsigned get_suffix_unsigned(const std::string &str, const std::string &prefix)
602{
603 // first_index is the end of the `prefix`.
604 auto first_index = str.find(prefix);
605 INVARIANT(
606 first_index != std::string::npos, "Prefix not found in the given string");
607 first_index += prefix.length();
608
609 // last_index is the index of not-digit.
610 auto last_index = str.find_first_not_of("0123456789", first_index);
611 std::string result = str.substr(first_index, last_index - first_index);
612 return std::stol(result);
613}
614
616 const goto_programt::const_targett &loop_head,
617 const loop_templatet<
620{
621 goto_programt::const_targett loop_end = loop_head;
622 for(const auto &t : loop)
623 {
624 // an instruction is the loop end if it is a goto instruction
625 // and it jumps backward to the loop head
626 if(
627 t->is_goto() && t->get_target() == loop_head &&
628 t->location_number > loop_end->location_number)
629 loop_end = t;
630 }
631 INVARIANT(
632 loop_head != loop_end,
633 "Could not find end of the loop starting at: " +
634 loop_head->source_location().as_string());
635
636 return loop_end;
637}
638
640 const goto_programt::targett &loop_head,
642 &loop)
643{
644 goto_programt::targett loop_end = loop_head;
645 for(const auto &t : loop)
646 {
647 // an instruction is the loop end if it is a goto instruction
648 // and it jumps backward to the loop head
649 if(
650 t->is_goto() && t->get_target() == loop_head &&
651 t->location_number > loop_end->location_number)
652 loop_end = t;
653 }
654 INVARIANT(
655 loop_head != loop_end,
656 "Could not find end of the loop starting at: " +
657 loop_head->source_location().as_string());
658
659 return loop_end;
660}
661
663 const unsigned int target_loop_number,
664 goto_functiont &function,
665 bool finding_head)
666{
667 natural_loops_mutablet natural_loops(function.body);
668
669 // iterate over all natural loops to find the loop with `target_loop_number`
670 for(const auto &loop_p : natural_loops.loop_map)
671 {
672 const goto_programt::targett loop_head = loop_p.first;
673 goto_programt::targett loop_end =
674 get_loop_end_from_loop_head_and_content_mutable(loop_head, loop_p.second);
675 // check if the current loop is the target loop by comparing loop number
676 if(loop_end->loop_number == target_loop_number)
677 {
678 if(finding_head)
679 return loop_head;
680 else
681 return loop_end;
682 }
683 }
684
686}
687
689get_loop_end(const unsigned int target_loop_number, goto_functiont &function)
690{
691 return get_loop_head_or_end(target_loop_number, function, false);
692}
693
695get_loop_head(const unsigned int target_loop_number, goto_functiont &function)
696{
697 return get_loop_head_or_end(target_loop_number, function, true);
698}
699
701 const invariant_mapt &invariant_map,
702 goto_modelt &goto_model)
703{
704 for(const auto &invariant_map_entry : invariant_map)
705 {
706 loop_idt loop_id = invariant_map_entry.first;
707 irep_idt function_id = loop_id.function_id;
708 unsigned int loop_number = loop_id.loop_number;
709
710 // get the last instruction of the target loop
711 auto &function = goto_model.goto_functions.function_map[function_id];
712 goto_programt::targett loop_end = get_loop_end(loop_number, function);
713
714 // annotate the invariant to the condition of `loop_end`
715 loop_end->condition_nonconst().add(ID_C_spec_loop_invariant) =
716 invariant_map_entry.second;
717 }
718}
719
721 const std::map<loop_idt, std::set<exprt>> &assigns_map,
722 goto_modelt &goto_model)
723{
724 for(const auto &assigns_map_entry : assigns_map)
725 {
726 loop_idt loop_id = assigns_map_entry.first;
727 irep_idt function_id = loop_id.function_id;
728 unsigned int loop_number = loop_id.loop_number;
729
730 // get the last instruction of the target loop
731 auto &function = goto_model.goto_functions.function_map[function_id];
732 goto_programt::targett loop_end = get_loop_end(loop_number, function);
733
734 exprt &condition = loop_end->condition_nonconst();
735 auto assigns = exprt(ID_target_list);
736 for(const auto &e : assigns_map_entry.second)
737 assigns.add_to_operands(e);
738 condition.add(ID_C_spec_assigns) = assigns;
739 }
740}
741
743 const std::map<loop_idt, exprt> &assigns_map,
744 goto_modelt &goto_model)
745{
746 for(const auto &assigns_map_entry : assigns_map)
747 {
748 loop_idt loop_id = assigns_map_entry.first;
749 irep_idt function_id = loop_id.function_id;
750 unsigned int loop_number = loop_id.loop_number;
751
752 // get the last instruction of the target loop
753 auto &function = goto_model.goto_functions.function_map[function_id];
754 goto_programt::targett loop_end = get_loop_end(loop_number, function);
755
756 exprt &condition = loop_end->condition_nonconst();
757 condition.add(ID_C_spec_assigns) = assigns_map_entry.second;
758 }
759}
760
762 const std::map<loop_idt, std::vector<exprt>> &decreases_map,
763 goto_modelt &goto_model)
764{
765 for(const auto &decreases_map_entry : decreases_map)
766 {
767 loop_idt loop_id = decreases_map_entry.first;
768 irep_idt function_id = loop_id.function_id;
769 unsigned int loop_number = loop_id.loop_number;
770
771 // get the last instruction of the target loop
772 auto &function = goto_model.goto_functions.function_map[function_id];
773 goto_programt::targett loop_end = get_loop_end(loop_number, function);
774
775 exprt &condition = loop_end->condition_nonconst();
776 auto decreases = exprt(ID_target_list);
777 for(const auto &e : decreases_map_entry.second)
778 decreases.add_to_operands(e);
779 condition.add(ID_C_spec_decreases) = decreases;
780 }
781}
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:219
unsignedbv_typet size_type()
Definition c_types.cpp:55
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:240
bitvector_typet char_type()
Definition c_types.cpp:111
Control Flow Graph.
Operator to return the address of an object.
Boolean AND.
Definition std_expr.h:2071
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:707
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:49
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:39
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
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:223
The Boolean constant false.
Definition std_expr.h:3017
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".
instructionst::iterator targett
instructionst::const_iterator const_targett
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.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
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:73
void append_havoc_slice_code(const source_locationt location, const exprt &ptr, const exprt &size, goto_programt &dest)
Definition utils.cpp:51
const irep_idt & mode
Definition utils.h:121
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:105
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:85
const namespacet & ns
Definition utils.h:81
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:95
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:212
void swap(irept &irep)
Definition irep.h:442
const irep_idt & id() const
Definition irep.h:396
irept & add(const irep_idt &name)
Definition irep.cpp:111
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:155
mstreamt & error() const
Definition message.h:399
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:1006
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Boolean negation.
Definition std_expr.h:2278
A predicate that indicates that an address range is ok to read.
const exprt & pointer() const
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:113
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition std_expr.h:132
const irep_idt & get_identifier() const
Definition std_expr.h:142
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:3008
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
source_locationt & add_source_location()
Definition type.h:77
#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
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:47
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
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.
optionalt< 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:63
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:51
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:660
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:361
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition std_expr.h:932
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2403
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition std_expr.h:206
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
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:236
goto_programt history_construction
Definition utils.h:237
exprt expression_after_replacement
Definition utils.h:235
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:511
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:549
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:579
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:326
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:689
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:30
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:615
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:244
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:367
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:268
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:530
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:695
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:563
exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns)
Generate a validity check over all dereferences in an expression.
Definition utils.cpp:172
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:761
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:335
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:720
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:662
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:234
void widen_assigns(assignst &assigns, const namespacet &ns)
Widen expressions in assigns with the following strategy.
Definition utils.cpp:341
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:571
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:639
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:700
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:441
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:257
static const char ASSIGNS_CLAUSE_REPLACEMENT_TRACKING[]
Prefix for comments added to track assigns clause replacement.
Definition utils.cpp:323
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:601
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:190
#define ENTERED_LOOP
Definition utils.h:24
std::map< loop_idt, exprt > invariant_mapt
Definition utils.h:30
#define IN_BASE_CASE
Definition utils.h:23
#define IN_LOOP_HAVOC_BLOCK
Definition utils.h:25