33 : goto_model(goto_model),
36 spec_functions(spec_functions),
37 contract_clauses_codegen(contract_clauses_codegen),
38 ns(goto_model.symbol_table)
43 const std::size_t loop_id,
47 const std::set<symbol_exprt> &local_statics,
48 std::set<irep_idt> &function_pointer_contracts)
54 auto head_location(head->source_location());
81 std::vector<symbol_exprt> old_decreases_vars, new_decreases_vars;
82 for(
const auto &clause : decreases_clauses)
86 symbol_table, clause.type(), function_id,
"tmp_cc", head_location);
87 old_decreases_vars.push_back(old_decreases_var);
90 symbol_table, clause.type(), function_id,
"tmp_cc", head_location);
91 new_decreases_vars.push_back(new_decreases_var);
98 for(
auto &local_static : local_statics)
100 assigns.push_back(local_static);
103 auto nof_targets = assigns.size();
114 language_mode, assigns, write_set_populate_instrs);
122 write_set_populate_instrs,
129 write_set_populate_instrs,
142 write_set_populate_instrs,
202 std::unordered_map<exprt, symbol_exprt, irep_hash>
204 const std::size_t loop_id,
219 auto loop_head_location(loop_head->source_location());
240 symbol_table, invariant, loop_head_location, language_mode);
241 invariant.
swap(replace_history_result.expression_after_replacement);
243 replace_history_result.history_construction;
247 pre_loop_head_instrs.
add(
257 pre_loop_head_instrs.
add(
264 initial_invariant, invariant, loop_head_location};
267 initial_invariant_assignment, pre_loop_head_instrs, language_mode);
274 pre_loop_head_instrs.
add(
277 in_base_case,
true_exprt{}, loop_head_location));
289 pre_loop_head_instrs.
add(
291 pre_loop_head_instrs.
add(
294 addr_of_loop_write_set,
296 loop_head_location));
299 addr_of_loop_write_set,
302 pre_loop_head_instrs.
add(
309 pre_loop_head_instrs.
add(
312 goto_function.body.destructive_insert(loop_head, pre_loop_head_instrs);
313 return replace_history_result.parameter_to_history;
318 const std::size_t loop_id,
319 const std::size_t cbmc_loop_id,
329 const exprt &outer_write_set,
332 const std::vector<symbol_exprt> &old_decreases_vars)
334 auto loop_head_location(loop_head->source_location());
364 "Check invariant before entry for loop " +
378 loop_head_location));
384 "__check_assigns_clause_incl_loop_" +
std::to_string(cbmc_loop_id),
390 check_var, outer_write_set, addr_of_loop_write_set, loop_head_location),
391 loop_head_location));
396 "Check assigns clause inclusion for loop " +
402 auto label_instruction =
404 goto_instruction->complete_goto(label_instruction);
418 in_loop_havoc_block,
true_exprt{}, loop_head_location));
421 in_loop_havoc_block,
false_exprt{}, loop_head_location));
431 if(invariant.
id() == ID_and)
433 for(
const auto &op : invariant.
operands())
437 converter.
goto_convert(assumption, step_instrs, language_mode);
444 converter.
goto_convert(assumption, step_instrs, language_mode);
451 for(
size_t i = 0; i < old_decreases_vars.size(); i++)
454 old_decreases_vars[i], decreases_clauses[i], loop_head_location};
456 old_decreases_assignment, step_instrs, language_mode);
460 goto_function.body.destructive_insert(loop_head, step_instrs);
462 return step_case_target;
466 const std::size_t loop_id,
467 const std::size_t cbmc_loop_id,
476 const std::vector<symbol_exprt> &old_decreases_vars,
477 const std::vector<symbol_exprt> &new_decreases_vars,
481 auto loop_head_location(loop_head->source_location());
502 entered_loop,
true_exprt{}, loop_head_location));
509 step_case_target, in_base_case, loop_head_location));
520 "Check invariant after step for loop " +
526 if(invariant.
id() == ID_and)
528 for(
const auto &op : invariant.
operands())
532 converter.
goto_convert(assertion, pre_loop_latch_instrs, language_mode);
539 converter.
goto_convert(assertion, pre_loop_latch_instrs, language_mode);
546 if(!decreases_clauses.empty())
548 for(
size_t i = 0; i < new_decreases_vars.size(); i++)
551 new_decreases_vars[i], decreases_clauses[i], loop_head_location};
553 new_decreases_assignment, pre_loop_latch_instrs, language_mode);
561 "Check variant decreases after step for loop " +
566 new_decreases_vars, old_decreases_vars),
570 for(
size_t i = 0; i < old_decreases_vars.size(); i++)
572 pre_loop_latch_instrs.
add(
574 pre_loop_latch_instrs.
add(
581 goto_function.body, loop_latch, pre_loop_latch_instrs);
585 loop_latch->turn_into_assume();
586 loop_latch->condition_nonconst() =
boolean_negate(loop_latch->condition());
591 const std::size_t loop_id,
592 const std::size_t cbmc_loop_id,
597 const std::unordered_map<exprt, symbol_exprt, irep_hash> &history_var_map,
601 const std::vector<symbol_exprt> &old_decreases_vars,
602 const std::vector<symbol_exprt> &new_decreases_vars)
605 std::set<goto_programt::targett, goto_programt::target_less_than>
609 goto_function.body.instructions.begin();
610 target != goto_function.body.instructions.end();
615 INVARIANT(target->is_goto(),
"Exiting instructions must be GOTOs");
616 auto exit_target = target->get_target();
619 exit_loop_id_opt.has_value() && exit_loop_id_opt.value() != loop_id,
620 "Exiting instructions must jump out of the loop");
621 exit_targets.insert(exit_target);
636 for(
auto exit_target : exit_targets)
645 "Check step was unwound for loop " +
654 loop_exit_program.
add(
656 loop_exit_program.
add(
658 loop_exit_program.
add(
667 loop_exit_program.
add(
673 for(
const auto &v : history_var_map)
677 for(
size_t i = 0; i < old_decreases_vars.size(); i++)
679 loop_exit_program.
add(
681 loop_exit_program.
add(
687 goto_function.body, exit_target, loop_exit_program);
Operator to return the address of an object.
A non-fatal assertion, which checks a condition then permits execution to continue.
An assumption, which must hold in subsequent code.
A codet representing an assignment in the program.
goto_instruction_codet representation of a function call statement.
Computes natural loops, enforces normal form conditions, computes the nesting graph,...
const dfcc_loop_infot & get_loop_info(const std::size_t loop_id) const
Returns the loop info for that loop_id.
const exprt & get_outer_write_set(std::size_t loop_id) const
Returns the write set of the outer loop of that loop or the top level write set if that loop has no o...
Translates assigns and frees clauses of a function contract or loop contract into GOTO programs that ...
void gen_spec_assigns_instructions(const irep_idt &language_mode, const exprt::operandst &assigns_clause, goto_programt &dest)
Generates instructions encoding the assigns_clause targets and adds them to dest.
void add_exit_instructions(const std::size_t loop_id, const std::size_t cbmc_loop_id, goto_functionst::goto_functiont &goto_function, goto_programt::targett loop_head, const symbol_exprt &loop_write_set, const symbol_exprt &addr_of_loop_write_set, const std::unordered_map< exprt, symbol_exprt, irep_hash > &history_var_map, const symbol_exprt &entered_loop, const symbol_exprt &initial_invariant, const symbol_exprt &in_base_case, const std::vector< symbol_exprt > &old_decreases_vars, const std::vector< symbol_exprt > &new_decreases_vars)
Adds instructions of the exit block.
dfcc_spec_functionst & spec_functions
dfcc_instrument_loopt(goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library, dfcc_spec_functionst &spec_functions, dfcc_contract_clauses_codegent &contract_clauses_codegen)
Constructor for the loop contract instrumentation class.
void add_body_instructions(const std::size_t loop_id, const std::size_t cbmc_loop_id, goto_functionst::goto_functiont &goto_function, symbol_table_baset &symbol_table, goto_programt::targett loop_head, goto_programt::targett loop_latch, exprt &invariant, const exprt::operandst &decreases_clauses, const symbol_exprt &entered_loop, const symbol_exprt &in_base_case, const std::vector< symbol_exprt > &old_decreases_vars, const std::vector< symbol_exprt > &new_decreases_vars, const goto_programt::instructiont::targett &step_case_target, const irep_idt &symbol_mode)
Adds instructions of the body block.
std::size_t max_assigns_clause_size
std::unordered_map< exprt, symbol_exprt, irep_hash > add_prehead_instructions(const std::size_t loop_id, goto_functionst::goto_functiont &goto_function, symbol_table_baset &symbol_table, goto_programt::targett loop_head, goto_programt::targett loop_latch, goto_programt &assigns_instrs, exprt &invariant, const exprt::operandst &assigns, const symbol_exprt &loop_write_set, const symbol_exprt &addr_of_loop_write_set, const symbol_exprt &entered_loop, const symbol_exprt &initial_invariant, const symbol_exprt &in_base_case, const irep_idt &symbol_mode)
Adds instructions of prehead block, and return history variables.
void operator()(const std::size_t loop_id, const irep_idt &function_id, goto_functiont &goto_function, dfcc_cfg_infot &cfg_info, const std::set< symbol_exprt > &local_statics, std::set< irep_idt > &function_pointer_contracts)
Replaces a loop by a base + step abstraction generated from its contract.
goto_programt::instructiont::targett add_step_instructions(const std::size_t loop_id, const std::size_t cbmc_loop_id, const irep_idt &function_id, goto_functionst::goto_functiont &goto_function, symbol_table_baset &symbol_table, goto_programt::targett loop_head, goto_programt::targett loop_latch, goto_programt &havoc_instrs, exprt &invariant, const exprt::operandst &decreases_clauses, const symbol_exprt &loop_write_set, const exprt &outer_write_set, const symbol_exprt &initial_invariant, const symbol_exprt &in_base_case, const std::vector< symbol_exprt > &old_decreases_vars)
Adds instructions of the step block, and returns the STEP jump target so that it can be used to jump ...
dfcc_contract_clauses_codegent & contract_clauses_codegen
Class interface to library types and functions defined in cprover_contracts.c.
const code_function_callt write_set_release_call(const exprt &write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_release.
const code_function_callt write_set_check_assigns_clause_inclusion_call(const exprt &check_var, const exprt &reference_write_set_ptr, const exprt &candidate_write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_assigns_clause_inclusion.
const code_function_callt write_set_create_call(const exprt &write_set_ptr, const exprt &contract_assigns_size, const exprt &contract_frees_size, const exprt &assume_requires_ctx, const exprt &assert_requires_ctx, const exprt &assume_ensures_ctx, const exprt &assert_ensures_ctx, const exprt &allow_allocate, const exprt &allow_deallocate, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_create.
Describes a single loop for the purpose of DFCC loop contract instrumentation.
const symbol_exprt addr_of_write_set_var
Symbol representing pointer to the stack allocated write set object for this loop.
const exprt::operandst decreases
Decreases clause expression.
const std::set< exprt > assigns
Set of targets assigned by the loop, either user-provided or inferred.
const std::size_t cbmc_loop_id
Loop identifier assigned to this loop by traditional CBMC loop numbering.
std::optional< goto_programt::targett > find_latch(goto_programt &goto_program) const
const exprt invariant
Loop invariant expression.
std::optional< goto_programt::targett > find_head(goto_programt &goto_program) const
Finds the first instruction tagged as loop head and having the same loop identifier as this struct in...
const symbol_exprt write_set_var
Symbol representing the stack-allocated write set object for this loop.
This class rewrites GOTO functions that use the built-ins:
void generate_havoc_instructions(const irep_idt &function_id, const goto_programt &original_program, const exprt &write_set_to_havoc, goto_programt &havoc_program, std::size_t &nof_targets)
Translates original_program that specifies assignable targets into a program that havocs the targets.
void to_spec_assigns_instructions(const exprt &write_set_to_fill, const irep_idt &language_mode, goto_programt &program, std::size_t &nof_targets)
Rewrites in place program expressed in terms of built-ins specifying assignable targets declaratively...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
source_locationt & add_source_location()
typet & type()
Return the type of the expression.
The Boolean constant false.
void goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode)
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
symbol_tablet symbol_table
Symbol table.
std::list< instructiont >::iterator targett
The target for gotos and for start_thread nodes.
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
void update()
Update all indices.
instructionst::iterator 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())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
const irep_idt & id() const
message_handlert & get_message_handler()
The null pointer constant.
const irep_idt & get_function() const
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
Expression to hold a symbol (variable)
The symbol table base class interface.
irep_idt mode
Language mode.
The Boolean constant true.
Class that computes CFG information about the loop structure of a GOTO function for the purpose of dy...
Translates assigns and frees clauses of a function contract or loop contract into goto programs that ...
Add instrumentation to a goto program to perform frame condition checks.
This class applies the loop contract transformation to a loop in a goto function.
Translate functions that specify assignable and freeable targets declaratively into active functions ...
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Fresh auxiliary symbol creation.
const std::string & id2string(const irep_idt &d)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
static symbolt & get_function_symbol(symbol_table_baset &, const irep_idt &function_id)
Returns the symbolt for function_id.
static symbol_exprt create_symbol(symbol_table_baset &, const typet &type, const irep_idt &function_id, const std::string &base_name, const source_locationt &source_location)
Adds a new symbol named function_id::base_name of type type with given attributes in the symbol table...
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 ...
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.
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.
#define IN_LOOP_HAVOC_BLOCK