bmc_util.cpp File Reference

Bounded Model Checking Utilities. More...

#include "bmc_util.h"
#include <iostream>
#include <goto-programs/graphml_witness.h>
#include <goto-programs/json_goto_trace.h>
#include <goto-programs/xml_goto_trace.h>
#include <goto-symex/build_goto_trace.h>
#include <goto-symex/memory_model_pso.h>
#include <goto-symex/slice.h>
#include <goto-symex/symex_target_equation.h>
#include <linking/static_lifetime_init.h>
#include <solvers/decision_procedure.h>
#include <util/json_stream.h>
#include <util/ui_message.h>
#include "goto_symex_property_decider.h"
#include "symex_bmc.h"

Include dependency graph for bmc_util.cpp:

Go to the source code of this file.

Functions
void	message_building_error_trace (messaget &log)
	Outputs a message that an error trace is being built. More...
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)
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. More...
void	output_error_trace (const goto_tracet &goto_trace, const namespacet &ns, const trace_optionst &trace_options, ui_message_handlert &ui_message_handler)
void	output_graphml (const goto_tracet &goto_trace, const namespacet &ns, const optionst &options)
	outputs an error witness in graphml format More...
void	output_graphml (const symex_target_equationt &symex_target_equation, const namespacet &ns, const optionst &options)
	outputs a proof in graphml format More...
void	convert_symex_target_equation (symex_target_equationt &equation, decision_proceduret &decision_procedure, message_handlert &message_handler)
std::unique_ptr< memory_model_baset >	get_memory_model (const optionst &options, const namespacet &ns)
void	setup_symex (symex_bmct &symex, const namespacet &ns, const optionst &options, ui_message_handlert &ui_message_handler)
void	slice (symex_bmct &symex, symex_target_equationt &symex_target_equation, const namespacet &ns, const optionst &options, ui_message_handlert &ui_message_handler)
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. More...
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. More...
void	update_status_of_unknown_properties (propertiest &properties, std::unordered_set< irep_idt > &updated_properties)
	Sets the property status of UNKNOWN properties to PASS. More...
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. More...
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. More...
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. More...
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)
	Runs the property decider to solve the equation. More...

Detailed Description

Bounded Model Checking Utilities.

Definition in file bmc_util.cpp.

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.