bmc_util.h File Reference

Bounded Model Checking Utilities. More...

#include <goto-instrument/unwindset.h>
#include <goto-symex/build_goto_trace.h>
#include "incremental_goto_checker.h"
#include "properties.h"
#include <chrono>
#include <memory>

Include dependency graph for bmc_util.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Macros
#define	OPT_BMC
#define	HELP_BMC

Functions
void	convert_symex_target_equation (symex_target_equationt &equation, decision_proceduret &decision_procedure, message_handlert &message_handler)
ssa_step_predicatet	ssa_step_matches_failing_property (const irep_idt &property_id)
	Returns a function that checks whether an SSA step is an assertion with property_id.
void	message_building_error_trace (messaget &)
	Outputs a message that an error trace is being built.
void	build_error_trace (goto_tracet &, const namespacet &, const symex_target_equationt &, const decision_proceduret &, ui_message_handlert &)
void	output_error_trace (const goto_tracet &, const namespacet &, const trace_optionst &, ui_message_handlert &)
void	output_graphml (const goto_tracet &, const namespacet &, const optionst &)
	outputs an error witness in graphml format
void	output_graphml (const symex_target_equationt &, const namespacet &, const optionst &)
	outputs a proof in graphml format
std::unique_ptr< memory_model_baset >	get_memory_model (const optionst &options, const namespacet &)
void	setup_symex (symex_bmct &, const namespacet &, const optionst &, ui_message_handlert &)
void	slice (symex_bmct &, symex_target_equationt &symex_target_equation, const namespacet &, const optionst &, ui_message_handlert &)
void	postprocess_equation (symex_bmct &symex, symex_target_equationt &equation, const optionst &options, const namespacet &ns, ui_message_handlert &ui_message_handler)
	Post process the equation.
void	output_coverage_report (const std::string &cov_out, const abstract_goto_modelt &goto_model, const symex_bmct &symex, ui_message_handlert &ui_message_handler)
	Output a coverage report as generated by symex_coveraget if cov_out is non-empty.
void	update_properties_status_from_symex_target_equation (propertiest &properties, std::unordered_set< irep_idt > &updated_properties, const symex_target_equationt &equation)
	Sets property status to PASS for properties whose conditions are constant true in the equation.
void	update_status_of_not_checked_properties (propertiest &properties, std::unordered_set< irep_idt > &updated_properties)
	Sets the property status of NOT_CHECKED properties to PASS.
void	update_status_of_unknown_properties (propertiest &properties, std::unordered_set< irep_idt > &updated_properties)
	Sets the property status of UNKNOWN properties to PASS.
std::chrono::duration< double >	prepare_property_decider (propertiest &properties, symex_target_equationt &equation, goto_symex_property_decidert &property_decider, ui_message_handlert &ui_message_handler)
	Converts the equation and sets up the property decider, but does not call solve.
void	run_property_decider (incremental_goto_checkert::resultt &result, propertiest &properties, goto_symex_property_decidert &property_decider, ui_message_handlert &ui_message_handler, std::chrono::duration< double > solver_runtime, bool set_pass=true)
	Runs the property decider to solve the equation.

Detailed Description

Bounded Model Checking Utilities.

Definition in file bmc_util.h.

Macro Definition Documentation

HELP_BMC

#define HELP_BMC

Definition at line 197 of file bmc_util.h.

OPT_BMC

#define OPT_BMC

Value:

  "(program-only)"                                                             \
  "(show-byte-ops)"                                                            \
  "(show-vcc)"                                                                 \
  "(show-goto-symex-steps)"                                                    \
  "(show-points-to-sets)"                                                      \
  "(slice-formula)"                                                            \
  "(unwinding-assertions)"                                                     \
  "(no-unwinding-assertions)"                                                  \
  "(no-self-loops-to-assumptions)"                                             \
  "(partial-loops)"                                                            \
  "(paths):"                                                                   \
  "(show-symex-strategies)"                                                    \
  "(depth):"                                                                   \
  "(max-field-sensitivity-array-size):"                                        \
  "(no-array-field-sensitivity)"                                               \
  "(graphml-witness):"                                                         \
  "(symex-complexity-limit):"                                                  \
  "(symex-complexity-failed-child-loops-limit):"                               \
  "(incremental-loop):"                                                        \
  "(unwind-min):"                                                              \
  "(unwind-max):"                                                              \
  "(ignore-properties-before-unwind-min)"                                      \
  "(symex-cache-dereferences)" OPT_UNWINDSET

Definition at line 172 of file bmc_util.h.

Function Documentation

build_error_trace()

void build_error_trace	(	goto_tracet &	goto_trace,
		const namespacet &	ns,
		const symex_target_equationt &	symex_target_equation,
		const decision_proceduret &	decision_procedure,
		ui_message_handlert &	ui_message_handler
	)

Definition at line 40 of file bmc_util.cpp.

convert_symex_target_equation()

void convert_symex_target_equation	(	symex_target_equationt &	equation,
		decision_proceduret &	decision_procedure,
		message_handlert &	message_handler
	)

Definition at line 150 of file bmc_util.cpp.

get_memory_model()

std::unique_ptr< memory_model_baset > get_memory_model	(	const optionst &	options,
		const namespacet &	ns
	)

Definition at line 162 of file bmc_util.cpp.

message_building_error_trace()

void message_building_error_trace

(

messaget &

log

)

Outputs a message that an error trace is being built.

Definition at line 35 of file bmc_util.cpp.

output_coverage_report()

void output_coverage_report	(	const std::string &	cov_out,
		const abstract_goto_modelt &	goto_model,
		const symex_bmct &	symex,
		ui_message_handlert &	ui_message_handler
	)

Output a coverage report as generated by symex_coveraget if cov_out is non-empty.

Parameters

cov_out	file to write the report to; no report is generated if this is empty
goto_model	goto model to build the coverage report for
symex	symbolic execution run to report coverage for
ui_message_handler	status/warning message handler

Definition at line 306 of file bmc_util.cpp.

output_error_trace()

void output_error_trace	(	const goto_tracet &	goto_trace,
		const namespacet &	ns,
		const trace_optionst &	trace_options,
		ui_message_handlert &	ui_message_handler
	)

Definition at line 64 of file bmc_util.cpp.

output_graphml() [1/2]

void output_graphml	(	const goto_tracet &	goto_trace,
		const namespacet &	ns,
		const optionst &	options
	)

outputs an error witness in graphml format

Definition at line 107 of file bmc_util.cpp.

output_graphml() [2/2]

void output_graphml	(	const symex_target_equationt &	symex_target_equation,
		const namespacet &	ns,
		const optionst &	options
	)

outputs a proof in graphml format

Definition at line 129 of file bmc_util.cpp.

postprocess_equation()

void postprocess_equation	(	symex_bmct &	symex,
		symex_target_equationt &	equation,
		const optionst &	options,
		const namespacet &	ns,
		ui_message_handlert &	ui_message_handler
	)

Post process the equation.

• add partial order constraints
• slice
• perform validation

Definition at line 322 of file bmc_util.cpp.

prepare_property_decider()

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

Converts the equation and sets up the property decider, but does not call solve.

Parameters

[in,out]	properties	Sets the status of properties to be checked to UNKNOWN
[in,out]	equation	The equation that will be converted
[in,out]	property_decider	The property decider that we are going to set up
[in,out]	ui_message_handler	For logging

Returns

The runtime for converting the equation

Definition at line 358 of file bmc_util.cpp.

run_property_decider()

void run_property_decider	(	incremental_goto_checkert::resultt &	result,
		propertiest &	properties,
		goto_symex_property_decidert &	property_decider,
		ui_message_handlert &	ui_message_handler,
		std::chrono::duration< double >	solver_runtime,
		bool	set_pass = true
	)

Runs the property decider to solve the equation.

Parameters

[in,out]	result	For recording the progress and the updated properties
[in,out]	properties	The status will be updated
[in,out]	property_decider	The property decider that will solve the equation
[in,out]	ui_message_handler	For logging
	solver_runtime	The solver runtime will be added and output
	set_pass	If true then update UNKNOWN properties to PASS if the solver returns UNSATISFIABLE

Definition at line 382 of file bmc_util.cpp.

setup_symex()

void setup_symex	(	symex_bmct &	symex,
		const namespacet &	ns,
		const optionst &	options,
		ui_message_handlert &	ui_message_handler
	)

Definition at line 178 of file bmc_util.cpp.

slice()

void slice	(	symex_bmct &	symex,
		symex_target_equationt &	symex_target_equation,
		const namespacet &	ns,
		const optionst &	options,
		ui_message_handlert &	ui_message_handler
	)

Definition at line 198 of file bmc_util.cpp.

ssa_step_matches_failing_property()

ssa_step_predicatet ssa_step_matches_failing_property

(

const irep_idt &

property_id

)

Returns a function that checks whether an SSA step is an assertion with property_id.

Usually used for build_goto_trace.

Definition at line 54 of file bmc_util.cpp.

update_properties_status_from_symex_target_equation()

void update_properties_status_from_symex_target_equation	(	propertiest &	properties,
		std::unordered_set< irep_idt > &	updated_properties,
		const symex_target_equationt &	equation
	)

Sets property status to PASS for properties whose conditions are constant true in the equation.

Parameters

[in,out]	properties	The status is updated in this data structure
[in,out]	updated_properties	The set of property IDs of updated properties
	equation	A equation generated by goto-symex

Definition at line 238 of file bmc_util.cpp.

update_status_of_not_checked_properties()

void update_status_of_not_checked_properties	(	propertiest &	properties,
		std::unordered_set< irep_idt > &	updated_properties
	)

Sets the property status of NOT_CHECKED properties to PASS.

Parameters

[in,out]	properties	The status is updated in this data structure
[in,out]	updated_properties	The IDs of updated properties are added here Note: this should inspect the equation, but the equation doesn't have any useful information at the moment.

Definition at line 274 of file bmc_util.cpp.

update_status_of_unknown_properties()

void update_status_of_unknown_properties	(	propertiest &	properties,
		std::unordered_set< irep_idt > &	updated_properties
	)

Sets the property status of UNKNOWN properties to PASS.

Parameters

[in,out]	properties	The status is updated in this data structure
[in,out]	updated_properties	The set of property IDs of updated properties Note: we currently declare everything PASS that is UNKNOWN at the end of the model checking algorithm.

Definition at line 290 of file bmc_util.cpp.