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) | |
| std::optional< cext > | verify () |
Verify goto_model. More... | |
Public Attributes | |
| propertiest | properties |
| Result counterexample. More... | |
| irep_idt | target_violation_id |
Protected Member Functions | |
| std::list< loop_idt > | get_cause_loop_id (const goto_tracet &goto_trace, const goto_programt::const_targett violation) |
| std::list< loop_idt > | get_cause_loop_id_for_assigns (const goto_tracet &goto_trace) |
| cext::violation_typet | extract_violation_type (const std::string &description) |
| cext::violation_locationt | get_violation_location (const loop_idt &loop_id, const goto_functiont &function, unsigned location_number_of_target) |
| void | restore_functions () |
| Restore transformed functions to original functions. More... | |
| cext | build_cex (const goto_tracet &goto_trace, const source_locationt &loop_entry_loc) |
| 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 in the body of the transformed loop specified by loop_id. More... | |
| bool | is_instruction_in_transformed_loop_condition (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. More... | |
| void | preprocess_goto_model () |
| Preprocess the goto model to prepare for verification. More... | |
Protected Attributes | |
| 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 |
| std::unordered_map< irep_idt, goto_programt > | original_functions |
| Map from function names to original functions. More... | |
| std::unordered_map< goto_programt::const_targett, unsigned, const_target_hash > | original_loop_number_map |
| Map from instrumented instructions for loop contracts to their original loop numbers. More... | |
| std::unordered_set< goto_programt::const_targett, const_target_hash > | loop_havoc_set |
| Loop havoc instructions instrumented during applying loop contracts. More... | |
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()
|
inline |
Definition at line 102 of file cegis_verifier.h.
Member Function Documentation
◆ build_cex()
|
protected |
Definition at line 363 of file cegis_verifier.cpp.
◆ extract_violation_type()
|
protected |
Definition at line 109 of file cegis_verifier.cpp.
◆ get_cause_loop_id()
|
protected |
Definition at line 182 of file cegis_verifier.cpp.
◆ get_cause_loop_id_for_assigns()
|
protected |
Definition at line 147 of file cegis_verifier.cpp.
◆ get_violation_location()
|
protected |
Definition at line 262 of file cegis_verifier.cpp.
◆ is_instruction_in_transformed_loop()
|
protected |
Decide whether the target instruction is in the body of the transformed loop specified by loop_id.
Definition at line 318 of file cegis_verifier.cpp.
◆ is_instruction_in_transformed_loop_condition()
|
protected |
Decide whether the target instruction is between the loop-havoc and the evaluation of the loop guard.
Definition at line 282 of file cegis_verifier.cpp.
◆ preprocess_goto_model()
|
protected |
Preprocess the goto model to prepare for verification.
Definition at line 83 of file cegis_verifier.cpp.
◆ restore_functions()
|
protected |
Restore transformed functions to original functions.
Definition at line 547 of file cegis_verifier.cpp.
◆ verify()
| std::optional< cext > cegis_verifiert::verify | ( | ) |
Verify goto_model.
Return an empty std::optional if there is no violation. Otherwise, return the formatted counterexample.
Definition at line 553 of file cegis_verifier.cpp.
Member Data Documentation
◆ assigns_map
Definition at line 173 of file cegis_verifier.h.
◆ goto_model
|
protected |
Definition at line 174 of file cegis_verifier.h.
◆ invariant_candidates
|
protected |
Definition at line 172 of file cegis_verifier.h.
◆ log
|
protected |
Definition at line 176 of file cegis_verifier.h.
◆ loop_havoc_set
|
protected |
Loop havoc instructions instrumented during applying loop contracts.
Definition at line 190 of file cegis_verifier.h.
◆ ns
|
protected |
Definition at line 177 of file cegis_verifier.h.
◆ options
|
protected |
Definition at line 175 of file cegis_verifier.h.
◆ original_functions
|
protected |
Map from function names to original functions.
It is used to restore functions with annotated loops to original functions.
Definition at line 181 of file cegis_verifier.h.
◆ original_loop_number_map
|
protected |
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.
◆ properties
| propertiest cegis_verifiert::properties |
Result counterexample.
Definition at line 122 of file cegis_verifier.h.
◆ target_violation_id
| irep_idt cegis_verifiert::target_violation_id |
Definition at line 123 of file cegis_verifier.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/goto-synthesizer/cegis_verifier.h
- /home/runner/work/cbmc/cbmc/src/goto-synthesizer/cegis_verifier.cpp
