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:

Collaboration diagram for multi_path_symex_checkert:

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. More...

goto_tracet	build_full_trace () const override
	Builds and returns the complete trace. More...

goto_tracet	build_shortest_trace () const override
	Builds and returns the trace up to the first failed property. More...

goto_tracet	build_trace (const irep_idt &) const override
	Builds and returns the trace for the FAILed property with the given `property_id`. More...

const namespacet &	get_namespace () const override
	Returns the namespace associated with the traces. More...

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`. More...

void	report () override
	Additional reporting that may result from the underlying solver, no-op by default. More...

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. More...

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. More...

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. More...

Protected Member Functions inherited from multi_path_symex_only_checkert
virtual void	generate_equation ()
	Generates the equation by running goto-symex. More...

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`. More...

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.

Reimplemented in java_multi_path_symex_checkert.

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.

Reimplemented in java_multi_path_symex_checkert.

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.

Reimplemented in java_multi_path_symex_checkert.

Definition at line 128 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 141 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 158 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 151 of file multi_path_symex_checker.cpp.

◆ output_proof()

void multi_path_symex_checkert::output_proof ( )

overridevirtual

Implements witness_providert.

Definition at line 146 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 169 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:

/home/runner/work/cbmc/cbmc/src/goto-checker/multi_path_symex_checker.h
/home/runner/work/cbmc/cbmc/src/goto-checker/multi_path_symex_checker.cpp

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ multi_path_symex_checkert()

Member Function Documentation

◆ build_full_trace()

◆ build_shortest_trace()

◆ build_trace()

◆ get_namespace()

◆ localize_fault()

◆ operator()()

◆ output_error_witness()

◆ output_proof()

◆ prepare_property_decider()

◆ report()

◆ run_property_decider()

Member Data Documentation

◆ equation_generated

◆ property_decider