Uses goto-symex to symbolically execute each path in the goto model and calls a solver to find property violations. More...

#include <single_path_symex_checker.h>

Inheritance diagram for single_path_symex_checkert:

Collaboration diagram for single_path_symex_checkert:

Public Member Functions
	single_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

virtual	~single_path_symex_checkert ()=default

Public Member Functions inherited from single_path_symex_only_checkert
	single_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...

virtual	~single_path_symex_only_checkert ()=default

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

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

Public Member Functions inherited from witness_providert
virtual	~witness_providert ()=default

Public Member Functions inherited from goto_trace_providert
virtual	~goto_trace_providert ()=default

Protected Member Functions
bool	is_ready_to_decide (const symex_bmct &, const path_storaget::patht &) override
	Returns whether the given `path` produced by `symex` is ready to be checked. More...

virtual std::chrono::duration< double >	prepare_property_decider (propertiest &properties, symex_target_equationt &equation, goto_symex_property_decidert &property_decider)
	Prepare the `property_decider` for solving. More...

virtual void	run_property_decider (incremental_goto_checkert::resultt &result, propertiest &properties, goto_symex_property_decidert &property_decider, 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 single_path_symex_only_checkert
void	equation_output (const symex_bmct &symex, const symex_target_equationt &equation)

virtual void	setup_symex (symex_bmct &symex)

virtual void	initialize_worklist ()
	Adds the initial goto-symex state as a path to the worklist. More...

virtual bool	resume_path (path_storaget::patht &path)
	Continues exploring the given `path` using goto-symex. More...

virtual bool	has_finished_exploration (const propertiest &)
	Returns whether we should stop exploring paths. More...

virtual void	update_properties (propertiest &properties, std::unordered_set< irep_idt > &updated_properties, const symex_target_equationt &equation)
	Updates the `properties` from the `equation` and adds their property IDs to `updated_properties`. More...

virtual void	final_update_properties (propertiest &properties, std::unordered_set< irep_idt > &updated_properties)
	Updates the `properties` after having finished exploration 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	symex_initialized = false

std::unique_ptr< goto_symex_property_decidert >	property_decider

Protected Attributes inherited from single_path_symex_only_checkert
abstract_goto_modelt &	goto_model

symbol_tablet	symex_symbol_table

namespacet	ns

guard_managert	guard_manager

std::unique_ptr< path_storaget >	worklist

std::chrono::duration< double >	symex_runtime

unwindsett	unwindset

Protected Attributes inherited from incremental_goto_checkert
const optionst &	options

ui_message_handlert &	ui_message_handler

messaget	log

Detailed Description

Uses goto-symex to symbolically execute each path in the goto model and calls a solver to find property violations.

Definition at line 24 of file single_path_symex_checker.h.

Constructor & Destructor Documentation

◆ single_path_symex_checkert()

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

Definition at line 20 of file single_path_symex_checker.cpp.

◆ ~single_path_symex_checkert()

virtual single_path_symex_checkert::~single_path_symex_checkert ( )

virtualdefault

Member Function Documentation

◆ build_full_trace()

goto_tracet single_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_single_path_symex_checkert.

Definition at line 128 of file single_path_symex_checker.cpp.

◆ build_shortest_trace()

goto_tracet single_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_single_path_symex_checkert.

Definition at line 141 of file single_path_symex_checker.cpp.

◆ build_trace()

goto_tracet single_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_single_path_symex_checkert.

Definition at line 162 of file single_path_symex_checker.cpp.

◆ get_namespace()

const namespacet & single_path_symex_checkert::get_namespace ( ) const

overridevirtual

Returns the namespace associated with the traces.

Implements goto_trace_providert.

Definition at line 175 of file single_path_symex_checker.cpp.

◆ is_ready_to_decide()

bool single_path_symex_checkert::is_ready_to_decide	(	const symex_bmct &	symex,
		const path_storaget::patht &	path
	)

overrideprotectedvirtual

Returns whether the given path produced by symex is ready to be checked.

Reimplemented from single_path_symex_only_checkert.

Definition at line 94 of file single_path_symex_checker.cpp.

◆ operator()()

incremental_goto_checkert::resultt single_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.

Implements incremental_goto_checkert.

Definition at line 29 of file single_path_symex_checker.cpp.

◆ output_error_witness()

void single_path_symex_checkert::output_error_witness ( const goto_tracet & goto_trace )

overridevirtual

Implements witness_providert.

Definition at line 180 of file single_path_symex_checker.cpp.

◆ output_proof()

void single_path_symex_checkert::output_proof ( )

overridevirtual

Implements witness_providert.

Definition at line 186 of file single_path_symex_checker.cpp.

◆ prepare_property_decider()

std::chrono::duration< double > single_path_symex_checkert::prepare_property_decider	(	propertiest &	properties,
		symex_target_equationt &	equation,
		goto_symex_property_decidert &	property_decider
	)

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 102 of file single_path_symex_checker.cpp.

◆ run_property_decider()

void single_path_symex_checkert::run_property_decider	(	incremental_goto_checkert::resultt &	result,
		propertiest &	properties,
		goto_symex_property_decidert &	property_decider,
		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 113 of file single_path_symex_checker.cpp.

Member Data Documentation

◆ property_decider

std::unique_ptr<goto_symex_property_decidert> single_path_symex_checkert::property_decider

protected

Definition at line 48 of file single_path_symex_checker.h.

◆ symex_initialized

bool single_path_symex_checkert::symex_initialized = false

protected

Definition at line 47 of file single_path_symex_checker.h.

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

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

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ single_path_symex_checkert()

◆ ~single_path_symex_checkert()

Member Function Documentation

◆ build_full_trace()

◆ build_shortest_trace()

◆ build_trace()

◆ get_namespace()

◆ is_ready_to_decide()

◆ operator()()

◆ output_error_witness()

◆ output_proof()

◆ prepare_property_decider()

◆ run_property_decider()

Member Data Documentation

◆ property_decider

◆ symex_initialized