Loading...

Searching...

No Matches

bmc_util.cpp File Reference

Bounded Model Checking Utilities. More...

#include "bmc_util.h"
#include <util/json_stream.h>
#include <util/ui_message.h>
#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 <solvers/decision_procedure.h>
#include "goto_symex_property_decider.h"
#include "symex_bmc.h"
#include <iostream>

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

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.

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

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

outputs a proof in graphml format

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

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.

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

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)

Runs the property decider to solve the equation.

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 37 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 148 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 160 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 32 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 284 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 62 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 105 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 127 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 300 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 336 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 372 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 176 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 51 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 216 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 252 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 268 of file bmc_util.cpp.