35 const std::unordered_map<exprt, exprt, irep_hash> &tmp_post_map)
38 for(
const auto &tmp_post_entry : tmp_post_map)
42 "tmp_post variables must be symbol expression.");
43 const auto &tmp_post_symbol =
44 expr_dynamic_cast<symbol_exprt>(tmp_post_entry.first);
45 r.insert(tmp_post_symbol, tmp_post_entry.second);
58 std::vector<exprt> result;
59 for(
const auto &e : symbols)
61 if(e.type().id() == ID_unsignedbv)
70 if((e.type().id() == ID_signedbv))
73 result.push_back(
unary_exprt(ID_loop_entry, e, e.type()));
75 if((e.type().id() == ID_pointer))
96 natural_loops(function_p.second.body);
102 for(
const auto &loop_head_and_content : natural_loops.
loop_map)
105 if(loop_head_and_content.second.size() <= 1)
110 loop_head_and_content.first, loop_head_and_content.second);
112 loop_idt new_id(function_p.first, loop_end->loop_number);
113 loop_cfg_infot cfg_info(function_p.second, loop_head_and_content.second);
115 log.
progress() <<
"Initialize candidates for the loop at "
130 loop_end->is_goto() &&
133 loop_end->turn_into_skip();
138 if(loop_end->condition().find(ID_C_spec_loop_invariant).is_nil())
142 loop_end->loop_number,
145 if(loop_head->has_condition())
153 if(loop_end->condition().find(ID_C_spec_assigns).is_nil())
159 local_may_alias, loop_head_and_content.second,
assigns_map[new_id]);
175 const exprt &checked_pointer,
176 const std::list<loop_idt> cause_loop_ids)
178 auto new_assign = checked_pointer;
182 for(
const auto &loop_id : cause_loop_ids)
185 if(new_assign.id() == ID_index || new_assign.id() == ID_dereference)
195 const auto &source_location =
207 new_assign.add_source_location() = source_location;
213 INVARIANT(
false,
"Failed to synthesize a new assigns target.");
220 for(
const auto &instruction : goto_function.second.body.instructions)
223 if(!instruction.is_assign() || instruction.assign_lhs().id() != ID_symbol)
226 const auto symbol_lhs =
227 expr_try_dynamic_cast<symbol_exprt>(instruction.assign_lhs());
231 id2string(symbol_lhs->get_identifier()).find(
"tmp::tmp_post") !=
234 tmp_post_map[instruction.assign_lhs()] = instruction.assign_rhs();
240 std::set<symbol_exprt>
243 const exprt &new_clause,
244 const std::set<exprt> &live_vars)
249 std::set<symbol_exprt> result;
250 for(
const auto &e : live_vars)
255 for(
auto it = result.begin(); it != result.end();)
259 it = result.erase(it);
269 const exprt &violated_predicate)
275 return violated_predicate;
279 const exprt &checked_pointer)
286 checked_pointer,
unary_exprt(ID_loop_entry, checked_pointer));
290 const std::vector<exprt> terminal_symbols,
293 const std::vector<cext> &cexs)
310 expr_sett leafexprs(terminal_symbols.begin(), terminal_symbols.end());
316 start_args.push_back(&leaf_g);
324 if(partition.size() <= 1)
326 return partition.front() == 1;
329 start_args.push_back(&plus_g);
335 start_bool_args.push_back(&and_g);
338 start_bool_args.push_back(&equal_g);
341 start_bool_args.push_back(&le_g);
344 start_bool_args.push_back(<_g);
352 size_t size_bound = 0;
355 size_t count_all = 0;
356 size_t count_filtered = 0;
364 for(
auto strengthening_candidate : start_bool_ph.
enumerate(size_bound))
369 new_in_clauses[cause_loop_id] =
370 and_exprt(new_in_clauses[cause_loop_id], strengthening_candidate);
372 new_pos_clauses[cause_loop_id] =
373 and_exprt(new_pos_clauses[cause_loop_id], strengthening_candidate);
394 const auto &return_cex = verifier.
verify();
396 !return_cex.has_value() ||
397 (verifier.
properties.at(violation_id).status !=
399 return_cex->violation_type !=
401 return_cex->violation_type !=
404 log.
progress() <<
"Quick filter: " << count_filtered <<
" out of "
405 << count_all <<
" candidates were filtered out.\n";
406 return strengthening_candidate;
429 std::set<symbol_exprt> dependent_symbols;
431 std::vector<exprt> terminal_symbols;
434 auto return_cex = verifier.
verify();
437 std::vector<cext> cexs;
439 while(return_cex.has_value())
441 cexs.push_back(return_cex.value());
445 switch(return_cex->violation_type)
448 new_invariant_clause =
453 new_invariant_clause =
459 return_cex->checked_pointer, return_cex->cause_loop_ids);
465 return_cex->cause_loop_ids.front(),
466 new_invariant_clause,
467 return_cex->live_variables);
472 return_cex->cause_loop_ids.front(),
478 INVARIANT(
false,
"unsupported violation type");
486 INVARIANT(!return_cex->cause_loop_ids.empty(),
"No cause loop found!");
489 "failed to synthesized meaningful clause");
495 const auto &cause_loop_id = return_cex->cause_loop_ids.front();
498 cause_loop_id, new_invariant_clause, return_cex->live_variables);
502 return_cex->violation_location ==
537 return_cex = verifier.
verify();
543 return combined_invariant;
signedbv_typet signed_short_int_type()
Evaluate if an expression is consistent with examples.
Classes providing CFG-based information about symbols to guide simplifications in function and loop a...
Operator to return the address of an object.
Enumerator that enumerates binary functional expressions.
Evaluator for checking if an expression is consistent with a given set of test cases (positive exampl...
Verifier that take a goto program as input, and output formatted counterexamples for counterexample-g...
std::optional< cext > verify()
Verify goto_model.
irep_idt target_violation_id
propertiest properties
Result counterexample.
@ cex_not_hold_upon_entry
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
std::map< loop_idt, std::set< exprt > > assigns_map
Synthesized assigns clauses.
invariant_mapt synthesize_all() override
This synthesizer guarantees that, with the synthesized loop contracts, all checks in the annotated GO...
exprt synthesize(loop_idt loop_id) override
Synthesize loop invariant for a specified loop in the goto_model.
exprt synthesize_range_predicate(const exprt &violated_predicate)
Synthesize range predicate for OOB violation with violated_predicate.
const symbol_tablet original_symbol_table
Symbol table of the input goto model.
std::set< symbol_exprt > compute_dependent_symbols(const loop_idt &cause_loop_id, const exprt &new_clause, const std::set< exprt > &live_vars)
Compute the dependent symbols for a loop with invariant-not-preserved violation which happen after ne...
invariant_mapt in_invariant_clause_map
Synthesize invariant of form (in_inv || !guard) && (!guard -> pos_inv)
void build_tmp_post_map()
Scan all ASSIGN instructions to build the map from tmp_post variables to their original variables.
std::unordered_map< exprt, exprt, irep_hash > tmp_post_map
Map from tmp_post variables to their original variables.
void init_candidates()
Initialize invariants as true for all unannotated loops.
invariant_mapt pos_invariant_clause_map
invariant_mapt neg_guards
void synthesize_assigns(const exprt &checked_pointer, const std::list< loop_idt > cause_loop_ids)
Synthesize assigns target and update assigns_map.
exprt synthesize_strengthening_clause(const std::vector< exprt > terminal_symbols, const loop_idt &cause_loop_id, const irep_idt &violation_id, const std::vector< cext > &cexs)
Synthesize strengthening clause for invariant-not-preserved violation.
exprt synthesize_same_object_predicate(const exprt &checked_pointer)
Synthesize same object predicate for null-pointer violation for checked_pointer.
Factory for enumerator that can be used to represent a tree grammar.
void attach_productions(const std::string &id, const enumeratorst &enumerators)
Attach enumerators to the placeholder with id.
Base class for all expressions.
The Boolean constant false.
function_mapt function_map
goto_functionst goto_functions
GOTO functions.
instructionst::iterator targett
A class containing utility functions for havocing expressions.
Enumerator that enumerates leaf expressions from a given list.
void erase_locals(std::set< exprt > &exprs)
source_locationt source_location
static const commandt reset
return to default formatting, as defined by the terminal
static const commandt green
render text with green foreground color
mstreamt & progress() const
mstreamt & result() const
The offset (in bytes) of a pointer relative to the object.
Placeholders for actual enumerators, which represent nonterminals.
expr_sett enumerate(const std::size_t size) const override
Replace a symbol expression by a given expression.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The Boolean constant true.
Semantic type conversion.
Generic base class for unary expressions.
std::unordered_set< exprt, irep_hash > expr_sett
static exprt evaluator(const std::unordered_map< exprt, exprt, irep_hash > &memory, const decision_proceduret &solver, exprt src, const namespacet &ns)
static const exprt::operandst & get_assigns(const goto_programt::const_targett &latch_target)
Extracts the assigns clause expression from the latch condition.
std::vector< exprt > construct_terminals(const std::set< symbol_exprt > &symbols)
void replace_tmp_post(exprt &dest, const std::unordered_map< exprt, exprt, irep_hash > &tmp_post_map)
Enumerative Loop Contracts Synthesizer.
std::list< const enumerator_baset * > enumeratorst
std::list< std::size_t > partitiont
static bool find_symbols(symbol_kindt, const typet &, std::function< bool(const symbol_exprt &)>, std::unordered_set< irep_idt > &bindings)
Utilities for building havoc code for expressions.
const std::string & id2string(const irep_idt &d)
Field-insensitive, location-sensitive may-alias analysis.
Helper functions for k-induction and loop invariants.
Compute natural loops in a goto_function.
exprt same_object(const exprt &p1, const exprt &p2)
exprt pointer_object(const exprt &p)
Various predicates over pointers in programs.
@ FAIL
The property was violated.
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
bool can_cast_expr< symbol_exprt >(const exprt &base)
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Loop id used to identify loops.
invariant_mapt combine_in_and_post_invariant_clauses(const invariant_mapt &in_clauses, const invariant_mapt &post_clauses, const invariant_mapt &neg_guards)
Combine invariant of form (in_inv || !guard) && (!guard -> pos_inv)
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.
void widen_assigns(assignst &assigns, const namespacet &ns)
Widen expressions in assigns with the following strategy.
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
std::map< loop_idt, exprt > invariant_mapt