cprover
|
Verifier that take a goto program as input, and output formatted counterexamples for counterexample-guided-synthesis. More...
#include <cegis_verifier.h>
Public Member Functions | |
cegis_verifiert (const invariant_mapt &invariant_candidates, const std::map< loop_idt, std::set< exprt > > &assigns_map, goto_modelt &goto_model, const optionst &options, messaget &log) | |
Public Attributes | |
std::unordered_map< goto_programt::const_targett, unsigned, const_target_hash > | original_loop_number_map |
Verify goto_model . | |
std::unordered_set< goto_programt::const_targett, const_target_hash > | loop_havoc_set |
Loop havoc instructions instrumented during applying loop contracts. | |
Verifier that take a goto program as input, and output formatted counterexamples for counterexample-guided-synthesis.
Definition at line 99 of file cegis_verifier.h.
|
inline |
Definition at line 102 of file cegis_verifier.h.
std::unordered_set<goto_programt::const_targett, const_target_hash> cegis_verifiert::loop_havoc_set |
Loop havoc instructions instrumented during applying loop contracts.
Definition at line 190 of file cegis_verifier.h.
std::unordered_map<goto_programt::const_targett, unsigned, const_target_hash> cegis_verifiert::original_loop_number_map |
Verify goto_model
.
Return an empty `optionalt if there is no violation. / Otherwise, return the formatted counterexample. optionalt<cext> verify();
/ Result counterexample. propertiest properties; irep_idt target_violation_id;
protected: Compute the cause loops of violation
. We say a loop is the cause loop if the violated predicate is dependent upon the write set of the loop. std::list<loop_idt> get_cause_loop_id(
const goto_tracet &goto_trace,
const goto_programt::const_targett violation);
Compute the cause loops of a assignable-violation. We say a loop is the cause loop if the assignable check is in the loop. std::list<loop_idt> get_cause_loop_id_for_assigns(const goto_tracet &goto_trace);
Extract the violation type from violation description. cext::violation_typet extract_violation_type(const std::string &description);
Compute the location of the violation. cext::violation_locationt get_violation_location( const loop_idt &loop_id, const goto_functiont &function, unsigned location_number_of_target);
/ Restore transformed functions to original functions. void restore_functions();
Build counterexample from trace, and store it in return_cex
. cext build_cex(
const goto_tracet &goto_trace,
const source_locationt &loop_entry_loc);
/ Decide whether the target instruction is in the body of the transformed / loop specified by loop_id
. bool is_instruction_in_transformed_loop(
const loop_idt &loop_id,
const goto_functiont &function,
unsigned location_number_of_target);
/ Decide whether the target instruction is between the loop-havoc and the / evaluation of the loop guard. bool is_instruction_in_transformed_loop_condition( const loop_idt &loop_id, const goto_functiont &function, unsigned location_number_of_target);
/ Preprocess the goto model to prepare for verification. void preprocess_goto_model();
const invariant_mapt &invariant_candidates; const std::map<loop_idt, std::set<exprt>> &assigns_map; goto_modelt &goto_model; const optionst &options; messaget log; const namespacet ns;
/ Map from function names to original functions. It is used to / restore functions with annotated loops to original functions. std::unordered_map<irep_idt, goto_programt> original_functions;
/ Map from instrumented instructions for loop contracts to their / original loop numbers. Returned by code_contractst
Definition at line 186 of file cegis_verifier.h.