cprover
Loading...
Searching...
No Matches
contracts.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Verify and use annotated loop and function contracts
4
5Author: Michael Tautschnig
6
7Date: February 2016
8
9\*******************************************************************/
10
13
14#include "contracts.h"
15
16#include <algorithm>
17#include <map>
18
21
22#include <ansi-c/c_expr.h>
23
25
29
31
32#include <util/c_types.h>
33#include <util/expr_util.h>
34#include <util/find_symbols.h>
35#include <util/format_expr.h>
36#include <util/fresh_symbol.h>
37#include <util/graph.h>
40#include <util/message.h>
43#include <util/replace_symbol.h>
44#include <util/std_code.h>
45
48#include "memory_predicates.h"
49#include "utils.h"
50
60{
61private:
64
65 void parse_message(const std::string &message)
66 {
67 if(message.find("recursion is ignored on call") != std::string::npos)
69 }
70
71public:
75
80
81 void print(unsigned level, const std::string &message) override
82 {
83 parse_message(message);
84 wrapped.print(level, message);
85 }
86
87 void print(unsigned level, const xmlt &xml) override
88 {
90 }
91
92 void print(unsigned level, const jsont &json) override
93 {
95 }
96
97 void print(unsigned level, const structured_datat &data) override
98 {
100 }
101
102 void print(
103 unsigned level,
104 const std::string &message,
105 const source_locationt &location) override
106 {
107 parse_message(message);
108 wrapped.print(level, message, location);
109 return;
110 }
111
112 void flush(unsigned i) override
113 {
114 return wrapped.flush(i);
115 }
116
118 {
120 }
121
122 unsigned get_verbosity() const
123 {
124 return wrapped.get_verbosity();
125 }
126
127 std::size_t get_message_count(unsigned level) const
128 {
130 }
131
132 std::string command(unsigned i) const override
133 {
134 return wrapped.command(i);
135 }
136};
137
139 const irep_idt &function_name,
140 goto_functionst::goto_functiont &goto_function,
141 const local_may_aliast &local_may_alias,
143 const loopt &loop,
144 const irep_idt &mode)
145{
146 PRECONDITION(!loop.empty());
147
148 // find the last back edge
150 for(const auto &t : loop)
151 if(
152 t->is_goto() && t->get_target() == loop_head &&
153 t->location_number > loop_end->location_number)
154 loop_end = t;
155
156 // check for assigns, invariant, and decreases clauses
157 auto assigns_clause = static_cast<const exprt &>(
158 loop_end->get_condition().find(ID_C_spec_assigns));
159 auto invariant = static_cast<const exprt &>(
160 loop_end->get_condition().find(ID_C_spec_loop_invariant));
161 auto decreases_clause = static_cast<const exprt &>(
162 loop_end->get_condition().find(ID_C_spec_decreases));
163
164 if(invariant.is_nil())
165 {
166 if(decreases_clause.is_nil() && assigns_clause.is_nil())
167 return;
168 else
169 {
170 invariant = true_exprt();
171 log.warning()
172 << "The loop at " << loop_head->source_location().as_string()
173 << " does not have an invariant, but has other clauses"
174 << " specified in its contract.\n"
175 << "Hence, a default invariant ('true') is being used to prove those."
176 << messaget::eom;
177 }
178 }
179 else
180 {
181 // form the conjunction
182 invariant = conjunction(invariant.operands());
183 }
184
185 // Vector representing a (possibly multidimensional) decreases clause
186 const auto &decreases_clause_exprs = decreases_clause.operands();
187
188 // Temporary variables for storing the multidimensional decreases clause
189 // at the start of and end of a loop body
190 std::vector<symbol_exprt> old_decreases_vars;
191 std::vector<symbol_exprt> new_decreases_vars;
192
193 // change
194 // H: loop;
195 // E: ...
196 // to
197 // initialize loop_entry variables;
198 // H: assert(invariant);
199 // snapshot(write_set);
200 // havoc;
201 // assume(invariant);
202 // if(guard) goto E:
203 // old_decreases_value = decreases_clause_expr;
204 // loop with optional write_set inclusion checks;
205 // new_decreases_value = decreases_clause_expr;
206 // assert(invariant);
207 // assert(new_decreases_value < old_decreases_value);
208 // assume(false);
209 // E: ...
210
211 // an intermediate goto_program to store generated instructions
213
214 // process quantified variables correctly (introduce a fresh temporary)
215 // and return a copy of the invariant
216 const auto &invariant_expr = [&]() {
217 auto invariant_copy = invariant;
221 return invariant_copy;
222 };
223
224 // Process "loop_entry" history variables
225 // Find and replace "loop_entry" expression in the "invariant" expression.
226 std::map<exprt, exprt> parameter2history;
228 invariant,
230 loop_head->source_location(),
231 mode,
234
235 // Generate: assert(invariant) just before the loop
236 // We use a block scope to create a temporary assertion,
237 // and immediately convert it to goto instructions.
238 {
239 code_assertt assertion{invariant_expr()};
240 assertion.add_source_location() = loop_head->source_location();
241 converter.goto_convert(assertion, generated_code, mode);
242 generated_code.instructions.back().source_location_nonconst().set_comment(
243 "Check loop invariant before entry");
244 }
245
246 // Add 'loop_entry' history variables and base case assertion.
247 // These variables are local and thus
248 // need not be checked against the enclosing scope's write set.
250 goto_function.body,
251 loop_head,
253
256
257 // assigns clause snapshots
259
261
262 // ^^^ FIXME ^^^ we should only allow assignments to static locals
263 // declared in functions that are called in the loop body, not from the whole
264 // function...
265
266 // set of targets to havoc
268
269 if(assigns_clause.is_nil())
270 {
271 // No assigns clause was specified for this loop.
272 // Infer memory locations assigned by the loop from the loop instructions
273 // and the inferred aliasing relation.
274 try
275 {
276 get_assigns(local_may_alias, loop, to_havoc);
277 // TODO: if the set contains pairs (i, a[i]),
278 // we must at least widen them to (i, pointer_object(a))
279 log.debug() << "No loop assigns clause provided. Inferred targets {";
280 // Add inferred targets to the loop assigns clause.
281 bool ran_once = false;
282 for(const auto &target : to_havoc)
283 {
284 if(ran_once)
285 log.debug() << ", ";
286 ran_once = true;
287 log.debug() << format(target);
288 instrument_spec_assigns.track_spec_target(
289 target, snapshot_instructions);
290 }
291 log.debug()
292 << "}. Please specify an assigns clause if verification fails."
293 << messaget::eom;
294 }
295 catch(const analysis_exceptiont &exc)
296 {
297 log.error() << "Failed to infer variables being modified by the loop at "
298 << loop_head->source_location()
299 << ".\nPlease specify an assigns clause.\nReason:"
300 << messaget::eom;
301 throw exc;
302 }
303 }
304 else
305 {
306 // An assigns clause was specified for this loop.
307 // Add the targets to the set of expressions to havoc.
308 for(const auto &target : assigns_clause.operands())
309 {
310 to_havoc.insert(target);
311 instrument_spec_assigns.track_spec_target(target, snapshot_instructions);
312 }
313 }
314
315 // Insert instrumentation
316 // This must be done before havocing the write set.
317 // ^^^ FIXME this is not true ^^^
319 goto_function.body, loop_head, snapshot_instructions);
320
322
323 // Perform write set instrumentation on the entire loop.
325 function_name,
326 goto_function.body,
327 loop_head,
328 loop_end,
330 // do not skip checks on function parameter assignments
332 // do not use CFG info for now
334
335 // insert havocing code
337 havoc_gen.append_full_havoc_code(
338 loop_head->source_location(), generated_code);
339
340 // Add the havocing code, but only check against the enclosing scope's
341 // write set if it was manually specified.
342 if(assigns_clause.is_nil())
344 goto_function.body,
345 loop_head,
347 else
349 goto_function.body, loop_head, generated_code);
350
351 // ^^^ FIXME ^^^
352 // comment by delmasrd: I did not reactivate this behaviour
353 // because I think we always want to check the loop assignments against
354 // the surrounding clause
355
357
358 // Generate: assume(invariant) just after havocing
359 // We use a block scope to create a temporary assumption,
360 // and immediately convert it to goto instructions.
361 {
362 code_assumet assumption{invariant_expr()};
363 assumption.add_source_location() = loop_head->source_location();
364 converter.goto_convert(assumption, generated_code, mode);
365 }
366
367 // Create fresh temporary variables that store the multidimensional
368 // decreases clause's value before and after the loop
369 for(const auto &clause : decreases_clause.operands())
370 {
371 const auto old_decreases_var =
373 clause.type(), loop_head->source_location(), mode, symbol_table)
374 .symbol_expr();
376 old_decreases_var, loop_head->source_location()));
378
379 const auto new_decreases_var =
381 clause.type(), loop_head->source_location(), mode, symbol_table)
382 .symbol_expr();
384 new_decreases_var, loop_head->source_location()));
386 }
387
388 // TODO: Fix loop contract handling for do/while loops.
389 if(loop_end->is_goto() && !loop_end->get_condition().is_true())
390 {
391 log.error() << "Loop contracts are unsupported on do/while loops: "
392 << loop_head->source_location() << messaget::eom;
393 throw 0;
394
395 // non-deterministically skip the loop if it is a do-while loop.
397 loop_end,
398 side_effect_expr_nondett(bool_typet(), loop_head->source_location())));
399 }
400
401 // Assume invariant & decl the variant temporaries (just before loop guard).
402 // Use insert_before_swap to preserve jumps to loop head.
404 goto_function.body,
405 loop_head,
407
408 // Forward the loop_head iterator until the start of the body.
409 // This is necessary because complex C loop_head conditions could be
410 // converted to multiple GOTO instructions (e.g. temporaries are introduced).
411 // If the loop_head location shifts to a different function,
412 // assume that it's an inlined function and keep skipping.
413 // FIXME: This simple approach wouldn't work when
414 // the loop guard in the source file is split across multiple lines.
415 const auto head_loc = loop_head->source_location();
416 while(loop_head->source_location() == head_loc ||
417 loop_head->source_location().get_function() != head_loc.get_function())
418 loop_head++;
419
420 // At this point, we are just past the loop head,
421 // so at the beginning of the loop body.
422 auto loop_body = loop_head;
423 loop_head--;
424
425 // Generate: assignments to store the multidimensional decreases clause's
426 // value just before the loop body (but just after the loop guard)
427 if(!decreases_clause.is_nil())
428 {
429 for(size_t i = 0; i < old_decreases_vars.size(); i++)
430 {
433 old_decreases_assignment.add_source_location() =
434 loop_head->source_location();
436 }
437
438 goto_function.body.destructive_insert(
440 }
441
442 // Generate: assert(invariant) just after the loop exits
443 // We use a block scope to create a temporary assertion,
444 // and immediately convert it to goto instructions.
445 {
446 code_assertt assertion{invariant_expr()};
447 assertion.add_source_location() = loop_end->source_location();
448 converter.goto_convert(assertion, generated_code, mode);
449 generated_code.instructions.back().source_location_nonconst().set_comment(
450 "Check that loop invariant is preserved");
451 }
452
453 // Generate: assignments to store the multidimensional decreases clause's
454 // value after one iteration of the loop
455 if(!decreases_clause.is_nil())
456 {
457 for(size_t i = 0; i < new_decreases_vars.size(); i++)
458 {
461 new_decreases_assignment.add_source_location() =
462 loop_head->source_location();
464 }
465
466 // Generate: assertion that the multidimensional decreases clause's value
467 // after the loop is smaller than the value before the loop.
468 // Here, we use the lexicographic order.
472 monotonic_decreasing_assertion.add_source_location() =
473 loop_head->source_location();
476 generated_code.instructions.back().source_location_nonconst().set_comment(
477 "Check decreases clause on loop iteration");
478
479 // Discard the temporary variables that store decreases clause's value
480 for(size_t i = 0; i < old_decreases_vars.size(); i++)
481 {
483 old_decreases_vars[i], loop_head->source_location()));
485 new_decreases_vars[i], loop_head->source_location()));
486 }
487 }
488
490 goto_function.body,
491 loop_end,
493
494 // change the back edge into assume(false) or assume(guard)
495 loop_end->turn_into_assume();
496 loop_end->set_condition(boolean_negate(loop_end->get_condition()));
497}
498
500 const exprt &expression,
502 const irep_idt &mode)
503{
504 if(expression.id() == ID_not || expression.id() == ID_typecast)
505 {
506 // For unary connectives, recursively check for
507 // nested quantified formulae in the term
508 const auto &unary_expression = to_unary_expr(expression);
510 }
511 if(expression.id() == ID_notequal || expression.id() == ID_implies)
512 {
513 // For binary connectives, recursively check for
514 // nested quantified formulae in the left and right terms
515 const auto &binary_expression = to_binary_expr(expression);
518 }
519 if(expression.id() == ID_if)
520 {
521 // For ternary connectives, recursively check for
522 // nested quantified formulae in all three terms
523 const auto &if_expression = to_if_expr(expression);
526 add_quantified_variable(if_expression.false_case(), replace, mode);
527 }
528 if(expression.id() == ID_and || expression.id() == ID_or)
529 {
530 // For multi-ary connectives, recursively check for
531 // nested quantified formulae in all terms
532 const auto &multi_ary_expression = to_multi_ary_expr(expression);
533 for(const auto &operand : multi_ary_expression.operands())
534 {
536 }
537 }
538 else if(expression.id() == ID_exists || expression.id() == ID_forall)
539 {
540 // When a quantifier expression is found,
541 // for each quantified variable ...
542 const auto &quantifier_expression = to_quantifier_expr(expression);
543 for(const auto &quantified_variable : quantifier_expression.variables())
544 {
546
547 // 1. create fresh symbol
548 symbolt new_symbol = new_tmp_symbol(
549 quantified_symbol.type(),
550 quantified_symbol.source_location(),
551 mode,
553
554 // 2. add created fresh symbol to expression map
556 quantified_symbol.get_identifier(), quantified_symbol.type());
557 replace.insert(q, new_symbol.symbol_expr());
558
559 // 3. recursively check for nested quantified formulae
560 add_quantified_variable(quantifier_expression.where(), replace, mode);
561 }
562 }
563}
564
566 exprt &expr,
567 std::map<exprt, exprt> &parameter2history,
568 source_locationt location,
569 const irep_idt &mode,
571 const irep_idt &id)
572{
573 for(auto &op : expr.operands())
574 {
576 op, parameter2history, location, mode, history, id);
577 }
578
579 if(expr.id() == ID_old || expr.id() == ID_loop_entry)
580 {
581 const auto &parameter = to_history_expr(expr, id).expression();
582
583 const auto &id = parameter.id();
584 if(
585 id == ID_dereference || id == ID_member || id == ID_symbol ||
586 id == ID_ptrmember || id == ID_constant || id == ID_typecast)
587 {
588 auto it = parameter2history.find(parameter);
589
590 if(it == parameter2history.end())
591 {
592 // 0. Create a skip target to jump to, if the parameter is invalid
594 const auto skip_target =
596
597 // 1. Create a temporary symbol expression that represents the
598 // history variable
600 new_tmp_symbol(parameter.type(), location, mode, symbol_table)
601 .symbol_expr();
602
603 // 2. Associate the above temporary variable to it's corresponding
604 // expression
606
607 // 3. Add the required instructions to the instructions list
608 // 3.1. Declare the newly created temporary variable
610
611 // 3.2. Skip storing the history if the expression is invalid
615 location));
616
617 // 3.3. Add an assignment such that the value pointed to by the new
618 // temporary variable is equal to the value of the corresponding
619 // parameter
620 history.add(
622
623 // 3.4. Add a skip target
624 history.destructive_append(skip_program);
625 }
626
628 }
629 else
630 {
631 log.error() << "Tracking history of " << parameter.id()
632 << " expressions is not supported yet." << messaget::eom;
633 throw 0;
634 }
635 }
636}
637
638std::pair<goto_programt, goto_programt>
640 codet &expression,
641 source_locationt location,
642 const irep_idt &mode)
643{
644 std::map<exprt, exprt> parameter2history;
646
647 // Find and replace "old" expression in the "expression" variable
649 expression, parameter2history, location, mode, history, ID_old);
650
651 // Create instructions corresponding to the ensures clause
653 converter.goto_convert(expression, ensures_program, mode);
654
655 // return a pair containing:
656 // 1. instructions corresponding to the ensures clause
657 // 2. instructions related to initializing the history variables
658 return std::make_pair(std::move(ensures_program), std::move(history));
659}
660
662 const irep_idt &function,
663 const source_locationt &location,
666{
667 const auto &const_target =
668 static_cast<const goto_programt::targett &>(target);
669 // Return if the function is not named in the call; currently we don't handle
670 // function pointers.
671 PRECONDITION(const_target->call_function().id() == ID_symbol);
672
673 // Retrieve the function type, which is needed to extract the contract
674 // components.
675 const irep_idt &target_function =
676 to_symbol_expr(const_target->call_function()).get_identifier();
677 const symbolt &function_symbol = ns.lookup(target_function);
678 const auto &type = to_code_with_contract_type(function_symbol.type);
679
680 // Isolate each component of the contract.
681 auto assigns_clause = type.assigns();
682 auto requires = conjunction(type.requires());
683 auto ensures = conjunction(type.ensures());
684
685 // Create a replace_symbolt object, for replacing expressions in the callee
686 // with expressions from the call site (e.g. the return value).
687 // This object tracks replacements that are common to ENSURES and REQUIRES.
689
690 // keep track of the call's return expression to make it nondet later
692
693 // if true, the call return variable variable was created during replacement
694 bool call_ret_is_fresh_var = false;
695
696 if(type.return_type() != empty_typet())
697 {
698 // Check whether the function's return value is not disregarded.
699 if(target->call_lhs().is_not_nil())
700 {
701 // If so, have it replaced appropriately.
702 // For example, if foo() ensures that its return value is > 5, then
703 // rewrite calls to foo as follows:
704 // x = foo() -> assume(__CPROVER_return_value > 5) -> assume(x > 5)
705 auto &lhs_expr = const_target->call_lhs();
707 symbol_exprt ret_val(CPROVER_PREFIX "return_value", lhs_expr.type());
709 }
710 else
711 {
712 // If the function does return a value, but the return value is
713 // disregarded, check if the postcondition includes the return value.
715 ensures.visit(v);
716 if(v.found_return_value())
717 {
718 // The postcondition does mention __CPROVER_return_value, so mint a
719 // fresh variable to replace __CPROVER_return_value with.
722 type.return_type(),
723 id2string(target_function),
724 "ignored_return_value",
725 const_target->source_location(),
726 symbol_table.lookup_ref(target_function).mode,
727 ns,
729 symbol_exprt ret_val(CPROVER_PREFIX "return_value", type.return_type());
730 auto fresh_sym_expr = fresh.symbol_expr();
733 }
734 }
735 }
736
737 // Replace formal parameters
738 const auto &arguments = const_target->call_arguments();
739 auto a_it = arguments.begin();
740 for(auto p_it = type.parameters().begin();
741 p_it != type.parameters().end() && a_it != arguments.end();
742 ++p_it, ++a_it)
743 {
744 if(!p_it->get_identifier().empty())
745 {
746 symbol_exprt p(p_it->get_identifier(), p_it->type());
747 common_replace.insert(p, *a_it);
748 }
749 }
750
751 const auto &mode = symbol_table.lookup_ref(target_function).mode;
752
753 is_fresh_replacet is_fresh(*this, log, target_function);
754 is_fresh.create_declarations();
755
756 // Insert assertion of the precondition immediately before the call site.
757 if(!requires.is_true())
758 {
761 replace(requires);
762
763 goto_programt assertion;
765 code_assertt(requires),
766 assertion,
767 symbol_table.lookup_ref(target_function).mode);
768 assertion.instructions.back().source_location_nonconst() =
769 requires.source_location();
770 assertion.instructions.back().source_location_nonconst().set_comment(
771 "Check requires clause");
772 assertion.instructions.back().source_location_nonconst().set_property_class(
774 is_fresh.update_requires(assertion);
776 }
777
778 // Gather all the instructions required to handle history variables
779 // as well as the ensures clause
780 std::pair<goto_programt, goto_programt> ensures_pair;
781 if(!ensures.is_false())
782 {
785 replace(ensures);
786
787 auto assumption = code_assumet(ensures);
789 assumption,
790 ensures.source_location(),
791 symbol_table.lookup_ref(target_function).mode);
792
793 // add all the history variable initialization instructions
794 // to the goto program
796 }
797
798 // ASSIGNS clause should not refer to any quantified variables,
799 // and only refer to the common symbols to be replaced.
800 exprt targets;
801 for(auto &target : assigns_clause)
802 targets.add_to_operands(std::move(target));
803 common_replace(targets);
804
805 // Create a sequence of non-deterministic assignments...
807
808 // ...for assigns clause targets
809 if(!assigns_clause.empty())
810 {
811 // Havoc all targets in the assigns clause
812 // TODO: handle local statics possibly touched by this function
814 target_function,
815 targets.operands(),
817 location,
820 havocker.get_instructions(havoc_instructions);
821 }
822
823 // ...for the return value
824 if(call_ret_opt.has_value())
825 {
826 auto &call_ret = call_ret_opt.value();
827 auto &loc = call_ret.source_location();
828 auto &type = call_ret.type();
829
830 // Declare if fresh
834
835 side_effect_expr_nondett expr(type, location);
836 auto target = havoc_instructions.add(
838 target->code_nonconst().add_source_location() = loc;
839 }
840
841 // Insert havoc instructions immediately before the call site.
843
844 // To remove the function call, insert statements related to the assumption.
845 // Then, replace the function call with a SKIP statement.
846 if(!ensures.is_false())
847 {
848 is_fresh.update_ensures(ensures_pair.first);
850 }
851
852 // Kill return value variable if fresh
854 {
855 function_body.output_instruction(ns, "", log.warning(), *target);
856 auto dead_inst =
858 function_body.insert_before_swap(target, dead_inst);
859 ++target;
860 }
861
862 // Erase original function call
863 *target = goto_programt::make_skip();
864
865 // Add this function to the set of replaced functions.
866 summarized.insert(target_function);
867 return false;
868}
869
871 const irep_idt &function_name,
872 goto_functionst::goto_functiont &goto_function)
873{
874 const bool may_have_loops = std::any_of(
875 goto_function.body.instructions.begin(),
876 goto_function.body.instructions.end(),
877 [](const goto_programt::instructiont &instruction) {
878 return instruction.is_backwards_goto();
879 });
880
881 if(!may_have_loops)
882 return;
883
886 goto_functions, function_name, ns, log.get_message_handler());
887
888 INVARIANT(
889 decorated.get_recursive_function_warnings_count() == 0,
890 "Recursive functions found during inlining");
891
892 // restore internal invariants
894
895 local_may_aliast local_may_alias(goto_function);
896 natural_loops_mutablet natural_loops(goto_function.body);
897
898 // A graph node type that stores information about a loop.
899 // We create a DAG representing nesting of various loops in goto_function,
900 // sort them topologically, and instrument them in the top-sorted order.
901 //
902 // The goal here is not avoid explicit "subset checks" on nested write sets.
903 // When instrumenting in a top-sorted order,
904 // the outer loop would no longer observe the inner loop's write set,
905 // but only corresponding `havoc` statements,
906 // which can be instrumented in the usual way to achieve a "subset check".
907
908 struct loop_graph_nodet : public graph_nodet<empty_edget>
909 {
910 typedef const goto_programt::targett &targett;
911 typedef const typename natural_loops_mutablet::loopt &loopt;
912
913 targett target;
914 loopt loop;
915
916 loop_graph_nodet(targett t, loopt l) : target(t), loop(l)
917 {
918 }
919 };
921
922 for(const auto &loop : natural_loops.loop_map)
923 loop_nesting_graph.add_node(loop.first, loop.second);
924
925 for(size_t outer = 0; outer < loop_nesting_graph.size(); ++outer)
926 {
927 for(size_t inner = 0; inner < loop_nesting_graph.size(); ++inner)
928 {
929 if(inner == outer)
930 continue;
931
932 if(loop_nesting_graph[outer].loop.contains(
933 loop_nesting_graph[inner].target))
934 loop_nesting_graph.add_edge(outer, inner);
935 }
936 }
937
938 // Iterate over the (natural) loops in the function, in topo-sorted order,
939 // and apply any loop contracts that we find.
940 for(const auto &idx : loop_nesting_graph.topsort())
941 {
942 const auto &loop_node = loop_nesting_graph[idx];
944 function_name,
945 goto_function,
946 local_may_alias,
947 loop_node.target,
948 loop_node.loop,
949 symbol_table.lookup_ref(function_name).mode);
950 }
951}
952
957
962
965 goto_programt &program,
968{
969 auto lhs = instruction_it->assign_lhs();
970 lhs.add_source_location() = instruction_it->source_location();
972 instrument_spec_assigns.check_inclusion_assignment(
973 lhs, cfg_info_opt, payload);
975}
976
979 const irep_idt &function,
980 goto_programt &body,
983{
984 INVARIANT(
985 instruction_it->is_function_call(),
986 "The first argument of instrument_call_statement should always be "
987 "a function call");
988
989 const auto &callee_name =
990 to_symbol_expr(instruction_it->call_function()).get_identifier();
991
992 if(callee_name == "malloc")
993 {
994 const auto &function_call =
996 if(function_call.lhs().is_not_nil())
997 {
998 // grab the returned pointer from malloc
999 auto object = pointer_object(function_call.lhs());
1000 object.add_source_location() = function_call.source_location();
1001 // move past the call and then insert the CAR
1004 instrument_spec_assigns.track_heap_allocated(object, payload);
1006 // since CAR was inserted *after* the malloc call,
1007 // move the instruction pointer backward,
1008 // because the caller increments it in a `for` loop
1010 }
1011 }
1012 else if(callee_name == "free")
1013 {
1014 const auto &ptr = instruction_it->call_arguments().front();
1015 auto object = pointer_object(ptr);
1016 object.add_source_location() = instruction_it->source_location();
1019 .check_inclusion_heap_allocated_and_invalidate_aliases(
1020 object, cfg_info_opt, payload);
1022 }
1023}
1024
1026{
1027 // Collect all GOTOs and mallocs
1028 std::vector<goto_programt::instructiont> back_gotos;
1029 std::vector<goto_programt::instructiont> malloc_calls;
1030
1031 int index = 0;
1032 for(goto_programt::instructiont instruction : program.instructions)
1033 {
1034 if(instruction.is_backwards_goto())
1035 {
1036 back_gotos.push_back(instruction);
1037 }
1038 if(instruction.is_function_call())
1039 {
1041 if(instruction.call_function().id() == ID_dereference)
1042 {
1043 called_name =
1045 to_dereference_expr(instruction.call_function()).pointer())
1046 .get_identifier();
1047 }
1048 else
1049 {
1050 called_name =
1051 to_symbol_expr(instruction.call_function()).get_identifier();
1052 }
1053
1054 if(called_name == "malloc")
1055 {
1056 malloc_calls.push_back(instruction);
1057 }
1058 }
1059 index++;
1060 }
1061 // Make sure there are no gotos that go back such that a malloc
1062 // is between the goto and its destination (possible loop).
1063 for(auto goto_entry : back_gotos)
1064 {
1065 for(const auto &target : goto_entry.targets)
1066 {
1067 for(auto malloc_entry : malloc_calls)
1068 {
1069 if(
1070 malloc_entry.location_number >= target->location_number &&
1071 malloc_entry.location_number < goto_entry.location_number)
1072 {
1073 log.error() << "Call to malloc at location "
1074 << malloc_entry.location_number << " falls between goto "
1075 << "source location " << goto_entry.location_number
1076 << " and it's destination at location "
1077 << target->location_number << ". "
1078 << "Unable to complete instrumentation, as this malloc "
1079 << "may be in a loop." << messaget::eom;
1080 throw 0;
1081 }
1082 }
1083 }
1084 }
1085 return false;
1086}
1087
1089{
1090 // Get the function object before instrumentation.
1091 auto function_obj = goto_functions.function_map.find(function);
1093 {
1094 log.error() << "Could not find function '" << function
1095 << "' in goto-program; not enforcing contracts."
1096 << messaget::eom;
1097 return true;
1098 }
1099
1100 const auto &goto_function = function_obj->second;
1101 auto &function_body = function_obj->second.body;
1102
1103 // Get assigns clause for function
1104 const symbolt &function_sybmol = ns.lookup(function);
1105 const auto &function_with_contract =
1107
1110
1111 // Detect and track static local variables before inlining
1114
1115 // Full inlining of the function body
1116 // Inlining is performed so that function calls to a same function
1117 // occurring under different write sets get instrumented specifically
1118 // for each write set
1121
1122 INVARIANT(
1123 decorated.get_recursive_function_warnings_count() == 0,
1124 "Recursive functions found during inlining");
1125
1126 // Clean up possible fake loops that are due to `IF 0!=0 GOTO i` instructions
1128
1129 // Restore internal coherence in the programs
1131
1132 INVARIANT(
1134 "Loops remain in function '" + id2string(function) +
1135 "', assigns clause checking instrumentation cannot be applied.");
1136
1137 // Create a deep copy of the inlined body before any instrumentation is added
1138 // and compute static control flow graph information
1140 goto_function_orig.copy_from(goto_function);
1143
1144 // Start instrumentation
1145 auto instruction_it = function_body.instructions.begin();
1146
1147 // Inject local static snapshots
1150
1151 // Track targets mentionned in the specification
1152 for(auto &target : function_with_contract.assigns())
1153 {
1155 instrument_spec_assigns.track_spec_target(target, payload);
1157 }
1158
1159 // Track formal parameters
1161 for(const auto &param : to_code_type(function_sybmol.type).parameters())
1162 {
1164 instrument_spec_assigns.track_stack_allocated(
1165 ns.lookup(param.get_identifier()).symbol_expr(), payload);
1167 }
1168
1169 // Restore internal coherence in the programs
1171
1172 // Insert write set inclusion checks.
1174 function,
1177 function_body.instructions.end(),
1179 // skip checks on function parameter assignments
1181 cfg_info_opt);
1182
1183 return false;
1184}
1185
1189 const goto_programt::const_targett &target)
1190{
1191 const auto &pragmas = target->source_location().get_pragmas();
1193}
1194
1197 const goto_programt::const_targett &target,
1199 const namespacet ns,
1201{
1202 if(
1203 const auto &symbol_expr =
1204 expr_try_dynamic_cast<symbol_exprt>(target->assign_lhs()))
1205 {
1206 if(
1208 ns.lookup(symbol_expr->get_identifier()).is_parameter)
1209 return true;
1210
1211 if(cfg_info_opt.has_value())
1212 return !cfg_info_opt.value().is_local(symbol_expr->get_identifier());
1213 }
1214
1215 return true;
1216}
1217
1228 const goto_programt::const_targett &target,
1230{
1231 if(cfg_info_opt.has_value())
1232 return cfg_info_opt.value().is_not_local_or_dirty_local(
1233 target->decl_symbol().get_identifier());
1234
1235 // Unless proved non-dirty by the CFG analysis we assume it is dirty.
1236 return true;
1237}
1238
1242 const goto_programt::const_targett &target,
1244{
1245 // Unless proved non-dirty by the CFG analysis we assume it is dirty.
1246 if(!cfg_info_opt.has_value())
1247 return true;
1248
1249 return cfg_info_opt.value().is_not_local_or_dirty_local(
1250 target->dead_symbol().get_identifier());
1251}
1252
1254 const irep_idt &function,
1255 goto_programt &body,
1261{
1263 {
1264 // Skip instructions marked as disabled for assigns clause checking
1266 {
1268 if(cfg_info_opt.has_value())
1269 cfg_info_opt.value().step();
1270 continue;
1271 }
1272
1273 // Do not instrument this instruction again in the future,
1274 // since we are going to instrument it now below.
1276
1277 if(
1278 instruction_it->is_decl() &&
1280 {
1281 // grab the declared symbol
1282 const auto &decl_symbol = instruction_it->decl_symbol();
1283 // move past the call and then insert the CAR
1286 instrument_spec_assigns.track_stack_allocated(decl_symbol, payload);
1288 // since CAR was inserted *after* the DECL instruction,
1289 // move the instruction pointer backward,
1290 // because the loop step takes care of the increment
1292 }
1293 else if(
1294 instruction_it->is_assign() &&
1297 {
1300 }
1301 else if(instruction_it->is_function_call())
1302 {
1305 }
1306 else if(
1307 instruction_it->is_dead() &&
1309 {
1310 const auto &symbol = instruction_it->dead_symbol();
1311 if(instrument_spec_assigns.stack_allocated_is_tracked(symbol))
1312 {
1314 instrument_spec_assigns.invalidate_stack_allocated(symbol, payload);
1316 }
1317 else
1318 {
1319 // For loops, the loop_head appears after the DECL of counters,
1320 // and any other temporaries introduced during "initialization".
1321 // However, they go `DEAD` (possible conditionally) inside the loop,
1322 // in presence of return statements.
1323 // Notice that for them those variables be writable,
1324 // they must appear as assigns targets anyway,
1325 // but their DECL statements are outside of the loop.
1326 log.warning() << "Found a `DEAD` variable " << symbol.get_identifier()
1327 << " without corresponding `DECL`, at: "
1328 << instruction_it->source_location() << messaget::eom;
1329 }
1330 }
1331 else if(
1332 instruction_it->is_other() &&
1333 instruction_it->get_other().get_statement() == ID_havoc_object)
1334 {
1335 auto havoc_argument = instruction_it->get_other().operands().front();
1337 havoc_object.add_source_location() = instruction_it->source_location();
1339 instrument_spec_assigns.check_inclusion_assignment(
1342 }
1343
1344 // Move to the next instruction
1346 if(cfg_info_opt.has_value())
1347 cfg_info_opt.value().step();
1348 }
1349}
1350
1352{
1353 // Add statements to the source function
1354 // to ensure assigns clause is respected.
1356
1357 // Rename source function
1358 std::stringstream ss;
1359 ss << CPROVER_PREFIX << "contracts_original_" << function;
1360 const irep_idt mangled(ss.str());
1361 const irep_idt original(function);
1362
1365 {
1366 log.error() << "Could not find function '" << function
1367 << "' in goto-program; not enforcing contracts."
1368 << messaget::eom;
1369 return true;
1370 }
1371
1372 std::swap(goto_functions.function_map[mangled], old_function->second);
1374
1375 // Place a new symbol with the mangled name into the symbol table
1377 sl.set_file("instrumented for code contracts");
1378 sl.set_line("0");
1382 mangled_sym.name = mangled;
1383 mangled_sym.base_name = mangled;
1384 mangled_sym.location = sl;
1385 const auto mangled_found = symbol_table.insert(std::move(mangled_sym));
1386 INVARIANT(
1387 mangled_found.second,
1388 "There should be no existing function called " + ss.str() +
1389 " in the symbol table because that name is a mangled name");
1390
1391 // Insert wrapper function into goto_functions
1393 INVARIANT(
1395 "There should be no function called " + id2string(function) +
1396 " in the function map because that function should have had its"
1397 " name mangled");
1398
1400 INVARIANT(
1402 "There should be a function called " + ss.str() +
1403 " in the function map because we inserted a fresh goto-program"
1404 " with that mangled name");
1405
1407 wrapper.parameter_identifiers = mangled_fun->second.parameter_identifiers;
1410
1411 return false;
1412}
1413
1418{
1419 PRECONDITION(!dest.instructions.empty());
1420
1423
1424 auto assigns = code_type.assigns();
1425 auto requires = conjunction(code_type.requires());
1426 auto ensures = conjunction(code_type.ensures());
1427
1428 // build:
1429 // if(nondet)
1430 // decl ret
1431 // decl parameter1 ...
1432 // decl history_parameter1 ... [optional]
1433 // assume(requires) [optional]
1434 // ret=function(parameter1, ...)
1435 // assert(ensures)
1436 // skip: ...
1437
1438 // build skip so that if(nondet) can refer to it
1441 tmp_skip.add(goto_programt::make_skip(ensures.source_location()));
1442
1443 goto_programt check;
1444
1445 // prepare function call including all declarations
1447
1448 // Create a replace_symbolt object, for replacing expressions in the callee
1449 // with expressions from the call site (e.g. the return value).
1450 // This object tracks replacements that are common to ENSURES and REQUIRES.
1452
1453 // decl ret
1455 if(code_type.return_type() != empty_typet())
1456 {
1458 code_type.return_type(),
1459 skip->source_location(),
1460 function_symbol.mode,
1462 .symbol_expr();
1463 check.add(goto_programt::make_decl(r, skip->source_location()));
1464
1465 call.lhs() = r;
1467
1468 symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type());
1469 common_replace.insert(ret_val, r);
1470 }
1471
1472 // decl parameter1 ...
1473 goto_functionst::function_mapt::iterator f_it =
1476
1477 const goto_functionst::goto_functiont &gf = f_it->second;
1478 for(const auto &parameter : gf.parameter_identifiers)
1479 {
1480 PRECONDITION(!parameter.empty());
1483 parameter_symbol.type,
1484 skip->source_location(),
1485 parameter_symbol.mode,
1487 .symbol_expr();
1488 check.add(goto_programt::make_decl(p, skip->source_location()));
1490 p, parameter_symbol.symbol_expr(), skip->source_location()));
1491
1492 call.arguments().push_back(p);
1493
1494 common_replace.insert(parameter_symbol.symbol_expr(), p);
1495 }
1496
1498 visitor.create_declarations();
1499
1500 // Generate: assume(requires)
1501 if(!requires.is_false())
1502 {
1503 // extend common_replace with quantified variables in REQUIRES,
1504 // and then do the replacement
1507 requires, replace, function_symbol.mode);
1508 replace(requires);
1509
1510 goto_programt assumption;
1512 code_assumet(requires), assumption, function_symbol.mode);
1513 visitor.update_requires(assumption);
1514 check.destructive_append(assumption);
1515 }
1516
1517 // Prepare the history variables handling
1518 std::pair<goto_programt, goto_programt> ensures_pair;
1519
1520 // Generate: copies for history variables
1521 if(!ensures.is_true())
1522 {
1523 // extend common_replace with quantified variables in ENSURES,
1524 // and then do the replacement
1527 ensures, replace, function_symbol.mode);
1528 replace(ensures);
1529
1530 // get all the relevant instructions related to history variables
1531 auto assertion = code_assertt(ensures);
1532 assertion.add_source_location() = ensures.source_location();
1534 assertion, ensures.source_location(), function_symbol.mode);
1535 ensures_pair.first.instructions.back()
1536 .source_location_nonconst()
1537 .set_comment("Check ensures clause");
1538 ensures_pair.first.instructions.back()
1539 .source_location_nonconst()
1540 .set_property_class(ID_postcondition);
1541
1542 // add all the history variable initializations
1543 visitor.update_ensures(ensures_pair.first);
1544 check.destructive_append(ensures_pair.second);
1545 }
1546
1547 // ret=mangled_function(parameter1, ...)
1548 check.add(goto_programt::make_function_call(call, skip->source_location()));
1549
1550 // Generate: assert(ensures)
1551 if(ensures.is_not_nil())
1552 {
1553 check.destructive_append(ensures_pair.first);
1554 }
1555
1556 if(code_type.return_type() != empty_typet())
1557 {
1559 return_stmt.value().return_value(), skip->source_location()));
1560 }
1561
1562 // prepend the new code to dest
1564 dest.destructive_insert(dest.instructions.begin(), check);
1565}
1566
1567bool code_contractst::replace_calls(const std::set<std::string> &to_replace)
1568{
1569 if(to_replace.empty())
1570 return false;
1571
1572 bool fail = false;
1573
1574 for(auto &goto_function : goto_functions.function_map)
1575 {
1576 Forall_goto_program_instructions(ins, goto_function.second.body)
1577 {
1578 if(ins->is_function_call())
1579 {
1580 if(ins->call_function().id() != ID_symbol)
1581 continue;
1582
1583 const irep_idt &called_function =
1584 to_symbol_expr(ins->call_function()).get_identifier();
1585 auto found = std::find(
1586 to_replace.begin(), to_replace.end(), id2string(called_function));
1587 if(found == to_replace.end())
1588 continue;
1589
1591 goto_function.first,
1592 ins->source_location(),
1593 goto_function.second.body,
1594 ins);
1595 }
1596 }
1597 }
1598
1599 if(fail)
1600 return true;
1601
1602 for(auto &goto_function : goto_functions.function_map)
1603 remove_skip(goto_function.second.body);
1604
1606
1607 return false;
1608}
1609
1611{
1612 for(auto &goto_function : goto_functions.function_map)
1613 apply_loop_contract(goto_function.first, goto_function.second);
1614}
1615
1616bool code_contractst::enforce_contracts(const std::set<std::string> &to_enforce)
1617{
1618 if(to_enforce.empty())
1619 return false;
1620
1621 bool fail = false;
1622
1623 for(const auto &function : to_enforce)
1624 {
1625 auto goto_function = goto_functions.function_map.find(function);
1626 if(goto_function == goto_functions.function_map.end())
1627 {
1628 fail = true;
1629 log.error() << "Could not find function '" << function
1630 << "' in goto-program; not enforcing contracts."
1631 << messaget::eom;
1632 continue;
1633 }
1634
1635 if(!fail)
1636 fail = enforce_contract(function);
1637 }
1638 return fail;
1639}
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
const code_with_contract_typet & to_code_with_contract_type(const typet &type)
Cast a typet to a code_with_contract_typet.
Definition c_types.h:418
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
The Boolean type.
Definition std_types.h:36
Stores information about a goto function computed from its CFG, together with a target iterator into ...
Definition utils.h:190
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition std_code.h:270
A codet representing an assignment in the program.
An assumption, which must hold in subsequent code.
Definition std_code.h:217
namespacet ns
Definition contracts.h:112
std::pair< goto_programt, goto_programt > create_ensures_instruction(codet &expression, source_locationt location, const irep_idt &mode)
This function creates and returns an instruction that corresponds to the ensures clause.
void replace_history_parameter(exprt &expr, std::map< exprt, exprt > &parameter2history, source_locationt location, const irep_idt &mode, goto_programt &history, const irep_idt &id)
This function recursively identifies the "old" expressions within expr and replaces them with corresp...
bool replace_calls(const std::set< std::string > &)
Replace all calls to each function in the list with that function's contract.
bool apply_function_contract(const irep_idt &function, const source_locationt &location, goto_programt &function_body, goto_programt::targett &target)
Replaces function calls with assertions based on requires clauses, non-deterministic assignments for ...
void apply_loop_contract(const irep_idt &function, goto_functionst::goto_functiont &goto_function)
Apply loop contracts, whenever available, to all loops in function.
messaget & log
Definition contracts.h:125
goto_functionst & get_goto_functions()
void apply_loop_contracts()
symbol_tablet & symbol_table
Definition contracts.h:122
void instrument_call_statement(goto_programt::targett &instruction_it, const irep_idt &function, goto_programt &body, instrument_spec_assignst &instrument_spec_assigns, optionalt< cfg_infot > &cfg_info_opt)
Inserts an assertion into program immediately before the function call at instruction_it,...
void add_quantified_variable(const exprt &expression, replace_symbolt &replace, const irep_idt &mode)
This function recursively searches the expression to find nested or non-nested quantified expressions...
bool check_frame_conditions_function(const irep_idt &function)
Instrument functions to check frame conditions.
bool enforce_contract(const irep_idt &function)
Enforce contract of a single function.
std::unordered_set< irep_idt > summarized
Definition contracts.h:128
void check_frame_conditions(const irep_idt &function, goto_programt &body, goto_programt::targett instruction_it, const goto_programt::targett &instruction_end, instrument_spec_assignst &instrument_spec_assigns, skipt skip_parameter_assigns, optionalt< cfg_infot > &cfg_info_opt)
Insert assertion statements into the goto program to ensure that assigned memory is within the assign...
bool check_for_looped_mallocs(const goto_programt &program)
Check if there are any malloc statements which may be repeated because of a goto statement that jumps...
goto_convertt converter
Definition contracts.h:126
void instrument_assign_statement(goto_programt::targett &instruction_it, goto_programt &program, instrument_spec_assignst &instrument_spec_assigns, optionalt< cfg_infot > &cfg_info_opt)
Inserts an assertion into program immediately before the assignment instruction_it,...
void check_apply_loop_contracts(const irep_idt &function_name, goto_functionst::goto_functiont &goto_function, const local_may_aliast &local_may_alias, goto_programt::targett loop_head, const loopt &loop, const irep_idt &mode)
goto_functionst & goto_functions
Definition contracts.h:123
skipt
Tells wether to skip or not skip an action.
Definition contracts.h:116
bool enforce_contracts(const std::set< std::string > &functions)
Turn requires & ensures into assumptions and assertions for each of the named functions.
void add_contract_check(const irep_idt &wrapper_function, const irep_idt &mangled_function, goto_programt &dest)
Instruments wrapper_function adding assumptions based on requires clauses and assertions based on ens...
symbol_tablet & get_symbol_table()
codet representation of a function call statement.
codet representation of a "return from a function" statement.
const parameterst & parameters() const
Definition std_types.h:655
Data structure for representing an arbitrary statement in a program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
The empty type.
Definition std_types.h:51
Base class for all expressions.
Definition expr.h:54
operandst & operands()
Definition expr.h:92
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:136
void goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode)
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
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.
static instructiont make_set_return_value(exprt return_value, const source_locationt &l=source_locationt::nil())
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
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())
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
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())
This class represents a node in a directed graph.
Definition graph.h:35
Class to generate havocking instructions for target expressions of a function contract's assign claus...
A class that further overrides the "safe" havoc utilities, and adds support for havocing pointer_obje...
Definition utils.h:57
const exprt & expression() const
Definition c_expr.h:212
Decorator for message_handlert that keeps track of warnings occuring when inlining a function.
Definition contracts.cpp:60
void print(unsigned level, const std::string &message) override
Definition contracts.cpp:81
unsigned get_verbosity() const
void print(unsigned level, const jsont &json) override
Definition contracts.cpp:92
void set_verbosity(unsigned _verbosity)
void print(unsigned level, const std::string &message, const source_locationt &location) override
void flush(unsigned i) override
void print(unsigned level, const xmlt &xml) override
Definition contracts.cpp:87
inlining_decoratort(message_handlert &_wrapped)
Definition contracts.cpp:72
unsigned int get_recursive_function_warnings_count()
Definition contracts.cpp:76
message_handlert & wrapped
Definition contracts.cpp:62
void print(unsigned level, const structured_datat &data) override
Definition contracts.cpp:97
std::string command(unsigned i) const override
Create an ECMA-48 SGR (Select Graphic Rendition) command.
std::size_t get_message_count(unsigned level) const
unsigned int recursive_function_warnings_count
Definition contracts.cpp:63
void parse_message(const std::string &message)
Definition contracts.cpp:65
A class that generates instrumentation for assigns clause checking.
const irep_idt & id() const
Definition irep.h:396
Definition json.h:27
loop_mapt loop_map
void set_verbosity(unsigned _verbosity)
Definition message.h:53
virtual void print(unsigned level, const std::string &message)=0
Definition message.cpp:60
std::size_t get_message_count(unsigned level) const
Definition message.h:56
unsigned get_verbosity() const
Definition message.h:54
virtual std::string command(unsigned) const
Create an ECMA-48 SGR (Select Graphic Rendition) command.
Definition message.h:66
virtual void flush(unsigned)=0
mstreamt & error() const
Definition message.h:399
mstreamt & debug() const
Definition message.h:429
message_handlert & get_message_handler()
Definition message.h:184
mstreamt & warning() const
Definition message.h:404
static eomt eom
Definition message.h:297
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().
Boolean negation.
Definition std_expr.h:2181
Replace expression or type symbols by an expression or type, respectively.
Predicate to be used with the exprt::visit() function.
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
A way of representing nested key/value data.
Expression to hold a symbol (variable)
Definition std_expr.h:80
const irep_idt & get_identifier() const
Definition std_expr.h:109
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The symbol table.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Symbol table entry.
Definition symbol.h:28
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
irep_idt mode
Language mode.
Definition symbol.h:49
The Boolean constant true.
Definition std_expr.h:2856
Definition xml.h:21
bool has_disable_assigns_check_pragma(const goto_programt::const_targett &target)
Returns true iff the target instruction is tagged with a 'CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK' prag...
bool must_track_dead(const goto_programt::const_targett &target, const optionalt< cfg_infot > &cfg_info_opt)
Returns true iff a DEAD x must be processed to upate the local write set.
bool must_check_assign(const goto_programt::const_targett &target, code_contractst::skipt skip_parameter_assigns, const namespacet ns, const optionalt< cfg_infot > cfg_info_opt)
Returns true iff an ASSIGN lhs := rhs instruction must be instrumented.
bool must_track_decl(const goto_programt::const_targett &target, const optionalt< cfg_infot > &cfg_info_opt)
Returns true iff a DECL x must be added to the local write set.
Verify and use annotated invariants and pre/post-conditions.
#define CPROVER_PREFIX
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Deprecated expression utility functions.
static format_containert< T > format(const T &o)
Definition format.h:37
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.
void goto_function_inline(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
Transitively inline all function calls made from a particular function.
Function Inlining This gives a number of different interfaces to the function inlining functionality ...
const code_function_callt & to_code_function_call(const codet &code)
Concrete Goto Program.
#define Forall_goto_program_instructions(it, program)
A Template Class for Graphs.
Havoc function assigns clauses.
Utilities for building havoc code for expressions.
std::set< exprt > assignst
Definition havoc_utils.h:23
Specify write set in function contracts.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
static int8_t r
Definition irep_hash.h:60
bool is_false(const literalt &l)
Definition literal.h:197
bool is_true(const literalt &l)
Definition literal.h:198
Field-insensitive, location-sensitive bitvector analysis.
Field-insensitive, location-sensitive may-alias analysis.
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.
Mathematical types.
Predicates to specify memory footprint in function contracts.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Pointer Logic.
exprt pointer_object(const exprt &p)
Various predicates over pointers in programs.
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Program Transformation.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
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:34
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:627
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:328
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition std_expr.h:899
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2291
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
Definition kdev_t.h:24
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &location, const irep_idt &mode, symbol_table_baset &symtab, std::string suffix, bool is_auxiliary)
Adds a fresh and uniquely named symbol to the symbol table.
Definition utils.cpp:190
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:215
exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns)
Generate a validity check over all dereferences in an expression.
Definition utils.cpp:122
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:180
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:204
void add_pragma_disable_assigns_check(source_locationt &location)
Adds a pragma on a source_locationt to disable inclusion checking.
Definition utils.cpp:103
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:136
#define CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK
Definition utils.h:27