CBMC
Loading...
Searching...
No Matches
Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
multi_path_symex_checkert Class Reference

Performs a multi-path symbolic execution using goto-symex and calls a SAT/SMT solver to check the status of the properties. More...

#include <multi_path_symex_checker.h>

+ Inheritance diagram for multi_path_symex_checkert:
[フレーム]
[legend]
+ Collaboration diagram for multi_path_symex_checkert:
[フレーム]
[legend]

Public Member Functions

  multi_path_symex_checkert (const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
 
resultt  operator() (propertiest &) override
  Check whether the given properties with status NOT_CHECKED, UNKNOWN or properties newly discovered by incremental_goto_checkert hold.
 
goto_tracet  build_full_trace () const override
  Builds and returns the complete trace.
 
goto_tracet  build_shortest_trace () const override
  Builds and returns the trace up to the first failed property.
 
goto_tracet  build_trace (const irep_idt &) const override
  Builds and returns the trace for the FAILed property with the given property_id.
 
const namespacet &  get_namespace () const override
  Returns the namespace associated with the traces.
 
void  output_error_witness (const goto_tracet &) override
 
void  output_proof () override
 
fault_location_infot  localize_fault (const irep_idt &property_id) const override
  Returns the most likely fault locations for the given FAILed property_id.
 
void  report () override
  Additional reporting that may result from the underlying solver, no-op by default.
 
- Public Member Functions inherited from multi_path_symex_only_checkert
  multi_path_symex_only_checkert (const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
 
resultt  operator() (propertiest &) override
  Check whether the given properties with status NOT_CHECKED, UNKNOWN or properties newly discovered by incremental_goto_checkert hold.
 
- Public Member Functions inherited from incremental_goto_checkert
  incremental_goto_checkert ()=delete
 
  incremental_goto_checkert (const incremental_goto_checkert &)=delete
 
virtual  ~incremental_goto_checkert ()=default
 
- Public Member Functions inherited from goto_trace_providert
virtual  ~goto_trace_providert ()=default
 
- Public Member Functions inherited from witness_providert
virtual  ~witness_providert ()=default
 
- Public Member Functions inherited from fault_localization_providert
virtual  ~fault_localization_providert ()=default
 

Protected Member Functions

virtual std::chrono::duration< double >  prepare_property_decider (propertiest &properties)
  Prepare the property decider for solving.
 
virtual void  run_property_decider (incremental_goto_checkert::resultt &result, propertiest &properties, std::chrono::duration< double > solver_runtime)
  Run the property decider, which calls the SAT solver, and set the status of checked properties accordingly.
 
- Protected Member Functions inherited from multi_path_symex_only_checkert
virtual void  generate_equation ()
  Generates the equation by running goto-symex.
 
virtual void  update_properties (propertiest &properties, std::unordered_set< irep_idt > &updated_properties)
  Updates the properties from the equation and adds their property IDs to updated_properties.
 
- Protected Member Functions inherited from incremental_goto_checkert
  incremental_goto_checkert (const optionst &, ui_message_handlert &)
 

Protected Attributes

bool  equation_generated
 
goto_symex_property_decidert  property_decider
 
- Protected Attributes inherited from multi_path_symex_only_checkert
abstract_goto_modelt &  goto_model
 
symbol_tablet  symex_symbol_table
 
namespacet  ns
 
symex_target_equationt  equation
 
guard_managert  guard_manager
 
path_fifot  path_storage
 
unwindsett  unwindset
 
symex_bmct  symex
 
- Protected Attributes inherited from incremental_goto_checkert
const optionst &  options
 
ui_message_handlert &  ui_message_handler
 
messaget  log
 

Detailed Description

Performs a multi-path symbolic execution using goto-symex and calls a SAT/SMT solver to check the status of the properties.

Definition at line 25 of file multi_path_symex_checker.h.

Constructor & Destructor Documentation

◆  multi_path_symex_checkert()

multi_path_symex_checkert::multi_path_symex_checkert ( const optionst &  options,
ui_message_handlert &  ui_message_handler,
abstract_goto_modelt &  goto_model 
)

Definition at line 26 of file multi_path_symex_checker.cpp.

Member Function Documentation

◆  build_full_trace()

goto_tracet multi_path_symex_checkert::build_full_trace ( ) const
overridevirtual

Builds and returns the complete trace.

Note
If slicing is used then the trace will not be complete. E.g. with simple-slice it will end at the last assertion.

Implements goto_trace_providert.

Definition at line 97 of file multi_path_symex_checker.cpp.

◆  build_shortest_trace()

goto_tracet multi_path_symex_checkert::build_shortest_trace ( ) const
overridevirtual

Builds and returns the trace up to the first failed property.

Implements goto_trace_providert.

Definition at line 110 of file multi_path_symex_checker.cpp.

◆  build_trace()

goto_tracet multi_path_symex_checkert::build_trace ( const irep_idt &  property_id ) const
overridevirtual

Builds and returns the trace for the FAILed property with the given property_id.

Implements goto_trace_providert.

Definition at line 127 of file multi_path_symex_checker.cpp.

◆  get_namespace()

const namespacet & multi_path_symex_checkert::get_namespace ( ) const
overridevirtual

Returns the namespace associated with the traces.

Implements goto_trace_providert.

Definition at line 140 of file multi_path_symex_checker.cpp.

◆  localize_fault()

fault_location_infot multi_path_symex_checkert::localize_fault ( const irep_idt &  property_id ) const
overridevirtual

Returns the most likely fault locations for the given FAILed property_id.

Implements fault_localization_providert.

Definition at line 157 of file multi_path_symex_checker.cpp.

◆  operator()()

incremental_goto_checkert::resultt multi_path_symex_checkert::operator() ( propertiest &  properties )
overridevirtual

Check whether the given properties with status NOT_CHECKED, UNKNOWN or properties newly discovered by incremental_goto_checkert hold.

Parameters
[out] properties Properties updated to whether their status have been determined. Newly discovered properties are added.
Returns
whether the goto checker found a violated property (FOUND_FAIL) or whether it is DONE with the given properties, together with the properties whose status changed since the last call to operator(). After returning DONE, another call to operator() with the same properties will return DONE and leave the properties' status unchanged. If there is a property with status FAIL then its counterexample can be retrieved by calling build_error_trace before any subsequent call to operator(). incremental_goto_checkert derivatives shall be implemented in a way such that repeated calls to operator() shall return when the next FAILed property has been found until eventually it does not find any failing properties any more.

Note: Repeated invocations of this operator with properties P_1, P_2, ... must satisfy the condition 'P_i contains P_i+1'. I.e. after checking properties P_i the caller may decide to check only a subset of properties P_i+1 in the following invocation, but the caller may not add properties to P_i+1 that have not been in P_i. Such additional properties will be ignored.

Implements incremental_goto_checkert.

Definition at line 40 of file multi_path_symex_checker.cpp.

◆  output_error_witness()

void multi_path_symex_checkert::output_error_witness ( const goto_tracet &  error_trace )
overridevirtual

Implements witness_providert.

Definition at line 150 of file multi_path_symex_checker.cpp.

◆  output_proof()

void multi_path_symex_checkert::output_proof ( )
overridevirtual

Implements witness_providert.

Definition at line 145 of file multi_path_symex_checker.cpp.

◆  prepare_property_decider()

std::chrono::duration< double > multi_path_symex_checkert::prepare_property_decider ( propertiest &  properties )
protectedvirtual

Prepare the property decider for solving.

This sets up the data structures for tracking goal literals, sets the status of properties to be checked to UNKNOWN and pushes the equation into the solver.

Returns
the time taken (pushing into the solver is a costly operation)

Definition at line 80 of file multi_path_symex_checker.cpp.

◆  report()

void multi_path_symex_checkert::report ( )
overridevirtual

Additional reporting that may result from the underlying solver, no-op by default.

Reimplemented from incremental_goto_checkert.

Definition at line 168 of file multi_path_symex_checker.cpp.

◆  run_property_decider()

void multi_path_symex_checkert::run_property_decider ( incremental_goto_checkert::resultt &  result,
propertiest &  properties,
std::chrono::duration< double >  solver_runtime 
)
protectedvirtual

Run the property decider, which calls the SAT solver, and set the status of checked properties accordingly.

The property IDs of updated properties are added to the result.updated_properties and the goto checker's progress (DONE, FOUND_FAIL) is set in result. The solver_runtime will be logged.

Definition at line 88 of file multi_path_symex_checker.cpp.

Member Data Documentation

◆  equation_generated

bool multi_path_symex_checkert::equation_generated
protected

Definition at line 60 of file multi_path_symex_checker.h.

◆  property_decider

goto_symex_property_decidert multi_path_symex_checkert::property_decider
protected

Definition at line 61 of file multi_path_symex_checker.h.

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

AltStyle によって変換されたページ (->オリジナル) /