cprover
Loading...
Searching...
No Matches
cegis_verifiert Class Reference

Verifier that take a goto program as input, and output formatted counterexamples for counterexample-guided-synthesis. More...

#include <cegis_verifier.h>

+ Collaboration diagram for cegis_verifiert:

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_hashoriginal_loop_number_map
 Verify goto_model.
 
std::unordered_set< goto_programt::const_targett, const_target_hashloop_havoc_set
 Loop havoc instructions instrumented during applying loop contracts.
 

Detailed Description

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.

Constructor & Destructor Documentation

◆ cegis_verifiert()

cegis_verifiert::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 )
inline

Definition at line 102 of file cegis_verifier.h.

Member Data Documentation

◆ loop_havoc_set

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.

◆ original_loop_number_map

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.


The documentation for this class was generated from the following file: