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 =
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 =
231 id2string(symbol_lhs->get_identifier()).find(
"tmp::tmp_post") !=
234 tmp_post_map[instruction.assign_lhs()] = instruction.assign_rhs();
240std::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,
309 expr_sett leafexprs(terminal_symbols.begin(), terminal_symbols.end());
315 start_args.push_back(&leaf_g);
323 if(partition.size() <= 1)
325 return partition.front() == 1;
328 start_args.push_back(&plus_g);
334 start_bool_args.push_back(&and_g);
337 start_bool_args.push_back(&equal_g);
340 start_bool_args.push_back(&le_g);
343 start_bool_args.push_back(<_g);
351 size_t size_bound = 0;
359 for(
auto strengthening_candidate : start_bool_ph.
enumerate(size_bound))
364 new_in_clauses[cause_loop_id] =
365 and_exprt(new_in_clauses[cause_loop_id], strengthening_candidate);
367 new_pos_clauses[cause_loop_id] =
368 and_exprt(new_pos_clauses[cause_loop_id], strengthening_candidate);
379 const auto &return_cex = verifier.verify();
381 !return_cex.has_value() ||
382 (verifier.properties.at(violation_id).status !=
384 return_cex->violation_type !=
386 return_cex->violation_type !=
389 return strengthening_candidate;
412 std::set<symbol_exprt> dependent_symbols;
414 std::vector<exprt> terminal_symbols;
417 auto return_cex = verifier.verify();
419 while(return_cex.has_value())
424 switch(return_cex->violation_type)
427 new_invariant_clause =
431 case cext::violation_typet ::cex_null_pointer:
432 new_invariant_clause =
438 return_cex->checked_pointer, return_cex->cause_loop_ids);
444 return_cex->cause_loop_ids.front(),
445 new_invariant_clause,
446 return_cex->live_variables);
451 return_cex->cause_loop_ids.front(),
452 verifier.target_violation_id);
456 INVARIANT(
false,
"unsupported violation type");
464 INVARIANT(!return_cex->cause_loop_ids.empty(),
"No cause loop found!");
467 "failed to synthesized meaningful clause");
473 const auto &cause_loop_id = return_cex->cause_loop_ids.front();
476 cause_loop_id, new_invariant_clause, return_cex->live_variables);
480 return_cex->violation_location ==
515 return_cex = verifier.verify();
521 return combined_invariant;
unsignedbv_typet size_type()
signedbv_typet signed_short_int_type()
Verifier for Counterexample-Guided Synthesis.
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.
Verifier that take a goto program as input, and output formatted counterexamples for counterexample-g...
@ cex_not_hold_upon_entry
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
exprt synthesize_strengthening_clause(const std::vector< exprt > terminal_symbols, const loop_idt &cause_loop_id, const irep_idt &violation_id)
Synthesize strengthening clause for invariant-not-preserved violation.
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_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)
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 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.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
auto expr_dynamic_cast(TExpr &base) -> typename detail::expr_dynamic_cast_return_typet< T, TExpr >::type
Cast a reference to a generic exprt to a specific derived class.
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