42 const std::vector<symbol_exprt> &lhs,
43 const std::vector<symbol_exprt> &rhs)
60 for(
size_t i = 1; i < equality_conjunctions.size() - 1; i++)
63 equality_conjunctions[i] =
64 and_exprt(equality_conjunctions[i - 1], component_i_equality);
74 lexicographic_individual_comparisons[0] =
76 for(
size_t i = 1; i < lexicographic_individual_comparisons.size(); i++)
79 lexicographic_individual_comparisons[i] =
80 and_exprt(equality_conjunctions[i - 1], component_i_less_than);
82 return disjunction(lexicographic_individual_comparisons);
92 std::advance(target, offset);
106 for(
const auto &t : loop)
108 t->is_goto() && t->get_target() == loop_head &&
109 t->location_number > loop_end->location_number)
113 auto invariant =
static_cast<const exprt &
>(
114 loop_end->get_condition().find(ID_C_spec_loop_invariant));
115 auto decreases_clause =
static_cast<const exprt &
>(
116 loop_end->get_condition().find(ID_C_spec_decreases));
118 if(invariant.is_nil())
120 if(decreases_clause.is_nil())
127 <<
" does not have a loop invariant, but has a decreases clause. "
128 <<
"Hence, a default loop invariant ('true') is being used."
139 const auto &decreases_clause_exprs = decreases_clause.operands();
143 std::vector<symbol_exprt> old_decreases_vars;
144 std::vector<symbol_exprt> new_decreases_vars;
172 const auto &invariant_expr = [&]() {
173 auto invariant_copy = invariant;
177 return invariant_copy;
182 std::map<exprt, exprt> parameter2history;
186 loop_head->source_location,
201 havoc_code.
instructions.back().source_location.set_comment(
202 "Check loop invariant before entry");
219 for(
const auto &clause : decreases_clause.operands())
221 const auto old_decreases_var =
226 old_decreases_vars.push_back(old_decreases_var);
228 const auto new_decreases_var =
233 new_decreases_vars.push_back(new_decreases_var);
237 if(!loop_head->is_goto())
250 if(!decreases_clause.is_nil())
252 for(
size_t i = 0; i < old_decreases_vars.size(); i++)
254 code_assignt old_decreases_assignment{old_decreases_vars[i],
255 decreases_clause_exprs[i]};
256 old_decreases_assignment.add_source_location() =
257 loop_head->source_location;
261 goto_function.body.destructive_insert(std::next(loop_head), havoc_code);
271 havoc_code.
instructions.back().source_location.set_comment(
272 "Check that loop invariant is preserved");
277 if(!decreases_clause.is_nil())
279 for(
size_t i = 0; i < new_decreases_vars.size(); i++)
281 code_assignt new_decreases_assignment{new_decreases_vars[i],
282 decreases_clause_exprs[i]};
283 new_decreases_assignment.add_source_location() =
284 loop_head->source_location;
294 loop_head->source_location;
296 havoc_code.
instructions.back().source_location.set_comment(
297 "Check decreases clause on loop iteration");
300 for(
size_t i = 0; i < old_decreases_vars.size(); i++)
303 old_decreases_vars[i], loop_head->source_location));
305 new_decreases_vars[i], loop_head->source_location));
312 loop_end->targets.clear();
314 if(loop_head->is_goto())
317 loop_end->set_condition(
boolean_negate(loop_end->get_condition()));
324 return type.has_contract();
328 const exprt &expression,
332 if(expression.
id() == ID_not || expression.
id() == ID_typecast)
339 if(expression.
id() == ID_notequal || expression.
id() == ID_implies)
347 if(expression.
id() == ID_if)
351 const auto &if_expression =
to_if_expr(expression);
356 if(expression.
id() == ID_and || expression.
id() == ID_or)
361 for(
const auto &operand : multi_ary_expression.operands())
366 else if(expression.
id() == ID_exists || expression.
id() == ID_forall)
371 for(
const auto &quantified_variable : quantifier_expression.variables())
373 const auto &quantified_symbol =
to_symbol_expr(quantified_variable);
377 quantified_symbol.type(),
378 id2string(quantified_symbol.get_identifier()),
380 quantified_symbol.source_location(),
386 quantified_symbol.get_identifier(), quantified_symbol.type());
397 std::map<exprt, exprt> ¶meter2history,
406 op, parameter2history, location, mode, history,
id);
409 if(expr.
id() == ID_old || expr.
id() == ID_loop_entry)
414 parameter.id() == ID_dereference || parameter.id() == ID_member ||
415 parameter.id() == ID_symbol || parameter.id() == ID_ptrmember)
417 auto it = parameter2history.find(parameter);
419 if(it == parameter2history.end())
428 parameter2history[parameter] = tmp_symbol;
441 expr = parameter2history[parameter];
445 log.
error() <<
"Tracking history of " << parameter.id()
452 std::pair<goto_programt, goto_programt>
458 std::map<exprt, exprt> parameter2history;
463 expression, parameter2history, location, mode, history, ID_old);
472 return std::make_pair(std::move(ensures_program), std::move(history));
491 auto assigns = type.assigns();
502 if(
as_const(*target).call_lhs().is_not_nil())
525 "ignored_return_value",
526 target->source_location,
537 const auto &arguments = target->call_arguments();
538 auto a_it = arguments.begin();
539 for(
auto p_it = type.parameters().begin();
540 p_it != type.parameters().end() && a_it != arguments.end();
543 if(!p_it->get_identifier().empty())
546 common_replace.
insert(p, *a_it);
552 common_replace(assigns);
560 if(!requires.is_true())
571 assertion.
instructions.back().source_location = requires.source_location();
572 assertion.
instructions.back().source_location.set_comment(
573 "Check requires clause");
574 assertion.
instructions.back().source_location.set_property_class(
582 std::pair<goto_programt, goto_programt> ensures_pair;
583 if(!ensures.is_false())
592 ensures.source_location(),
602 if(assigns.is_not_nil())
613 if(!ensures.is_false())
634 for(
const auto &loop : natural_loops.
loop_map)
671 std::vector<exprt> &aliasable_references)
674 operands.reserve(aliasable_references.size());
675 for(
auto aliasable : aliasable_references)
683 goto_programt::instructionst::iterator &instruction_iterator,
686 std::set<irep_idt> &freely_assignable_symbols,
690 instruction_iterator->is_assign(),
691 "The first instruction of instrument_assign_statement should always be"
694 const exprt &lhs = instruction_iterator->assign_lhs();
697 freely_assignable_symbols.find(lhs.
get(ID_identifier)) ==
698 freely_assignable_symbols.end())
704 alias_assertion.
instructions.back().source_location.set_comment(
705 "Check that " +
from_expr(
ns, lhs.
id(), lhs) +
" is assignable");
707 program, instruction_iterator, alias_assertion);
712 goto_programt::instructionst::iterator &instruction_iterator,
715 std::set<irep_idt> &freely_assignable_symbols,
719 instruction_iterator->is_function_call(),
720 "The first argument of instrument_call_statement should always be "
724 if(instruction_iterator->call_function().id() == ID_dereference)
737 if(called_name ==
"malloc")
742 instruction_iterator++;
743 if(instruction_iterator->is_assign())
745 const exprt &rhs = instruction_iterator->assign_rhs();
747 rhs.
id() == ID_typecast,
748 "malloc is called but the result is not cast. Excluding result from "
749 "the assignable memory frame.");
757 program, instruction_iterator, pointer_capture);
763 instruction_iterator->call_lhs().is_not_nil() &&
764 instruction_iterator->call_lhs().id() == ID_symbol &&
765 freely_assignable_symbols.find(
767 freely_assignable_symbols.end())
775 alias_assertion.
instructions.back().source_location.set_comment(
779 ++instruction_iterator;
784 const typet &called_symbol_type = (called_symbol.
type.
id() == ID_pointer)
786 : called_symbol.
type;
787 exprt called_assigns =
794 const auto &arguments = instruction_iterator->call_arguments();
795 auto a_it = arguments.begin();
796 for(
auto p_it = called_type.
parameters().begin();
797 p_it != called_type.
parameters().end() && a_it != arguments.end();
800 if(!p_it->get_identifier().empty())
803 replace_formal_params.
insert(p, *a_it);
806 replace_formal_params(called_assigns);
810 called_assigns, *
this, called_name,
log);
816 alias_assertion.
instructions.back().source_location.set_comment(
817 "Check compatibility of assigns clause with the called function");
819 ++instruction_iterator;
826 std::vector<goto_programt::instructiont> back_gotos;
827 std::vector<goto_programt::instructiont> malloc_calls;
834 back_gotos.push_back(instruction);
852 if(called_name ==
"malloc")
854 malloc_calls.push_back(instruction);
861 for(
auto goto_entry : back_gotos)
863 for(
const auto &target : goto_entry.targets)
865 for(
auto malloc_entry : malloc_calls)
868 malloc_entry.location_number >= target->location_number &&
869 malloc_entry.location_number < goto_entry.location_number)
871 log.
error() <<
"Call to malloc at location "
872 << malloc_entry.location_number <<
" falls between goto "
873 <<
"source location " << goto_entry.location_number
874 <<
" and it's destination at location "
875 << target->location_number <<
". "
876 <<
"Unable to complete instrumentation, as this malloc "
892 log.
error() <<
"Could not find function '" <<
function
893 <<
"' in goto-program; not enforcing contracts."
919 exprt assigns_expr = type.assigns();
924 std::set<irep_idt> freely_assignable_symbols;
936 for(; instruction_it != program.
instructions.end(); ++instruction_it)
938 if(instruction_it->is_decl())
941 freely_assignable_symbols.insert(
942 instruction_it->get_decl().symbol().get_identifier());
945 assigns.
add_target(instruction_it->get_decl().symbol());
954 else if(instruction_it->is_assign())
960 freely_assignable_symbols,
963 else if(instruction_it->is_function_call())
969 freely_assignable_symbols,
975 while(!instruction_it->is_end_function())
991 std::stringstream ss;
999 log.
error() <<
"Could not find function '" <<
function
1000 <<
"' in goto-program; not enforcing contracts."
1010 sl.
set_file(
"instrumented for code contracts");
1014 mangled_sym = *original_sym;
1015 mangled_sym.
name = mangled;
1020 mangled_found.second,
1021 "There should be no existing function called " + ss.str() +
1022 " in the symbol table because that name is a mangled name");
1028 "There should be no function called " +
id2string(
function) +
1029 " in the function map because that function should have had its"
1035 "There should be a function called " + ss.str() +
1036 " in the function map because we inserted a fresh goto-program"
1037 " with that mangled name");
1057 exprt assigns = code_type.assigns();
1091 code_type.return_type(),
1092 skip->source_location,
1093 function_symbol.
mode)
1101 common_replace.
insert(ret_val,
r);
1105 goto_functionst::function_mapt::iterator f_it =
1110 for(
const auto ¶meter : gf.parameter_identifiers)
1115 parameter_symbol.
type,
1117 parameter_symbol.
mode)
1149 std::pair<goto_programt, goto_programt> ensures_pair;
1166 ensures_pair.first.instructions.back().source_location.set_comment(
1167 "Check ensures clause");
1168 ensures_pair.first.instructions.back().source_location.set_property_class(
1198 for(
const auto &
function : functions)
1202 log.
error() <<
"Function '" <<
function
1203 <<
"' does not have a contract; "
1204 "not replacing calls with contract."
1216 if(ins->is_function_call())
1218 if(ins->call_function().id() != ID_symbol)
1223 auto found = std::find(
1224 functions.begin(), functions.end(),
id2string(called_function));
1225 if(found == functions.end())
1252 std::set<std::string> functions;
1256 functions.insert(
id2string(goto_function.first));
1263 std::set<std::string> functions;
1267 functions.insert(
id2string(goto_function.first));
1275 for(
const auto &
function : functions)
1281 log.
error() <<
"Could not find function '" <<
function
1282 <<
"' in goto-program; not enforcing contracts."
1290 log.
error() <<
"Could not find any contracts within function '"