cprover
multi_path_symex_only_checker.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Checker using Multi-Path Symbolic Execution Only
4 
5 Author: Daniel Kroening, Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <util/invariant.h>
15 
18 #include <goto-symex/show_vcc.h>
19 
20 #include "bmc_util.h"
21 
23  const optionst &options,
24  ui_message_handlert &ui_message_handler,
25  abstract_goto_modelt &goto_model)
26  : incremental_goto_checkert(options, ui_message_handler),
27  goto_model(goto_model),
28  ns(goto_model.get_symbol_table(), symex_symbol_table),
29  equation(ui_message_handler),
30  symex(
31  ui_message_handler,
32  goto_model.get_symbol_table(),
33  equation,
34  options,
35  path_storage,
36  guard_manager)
37 {
39 }
40 
42 operator()(propertiest &properties)
43 {
45 
47  options.get_option("symex-coverage-report"),
48  goto_model,
49  symex,
51 
52  if(options.get_bool_option("show-vcc"))
53  {
55  }
56 
57  if(options.get_bool_option("program-only"))
58  {
60  }
61 
62  if(options.get_bool_option("show-byte-ops"))
63  {
65  }
66 
67  resultt result(resultt::progresst::DONE);
68  update_properties(properties, result.updated_properties);
69  return result;
70 }
71 
73 {
77 }
78 
80  propertiest &properties,
81  std::unordered_set<irep_idt> &updated_properties)
82 {
83  if(options.get_bool_option("symex-driven-lazy-loading"))
85 
87  properties, updated_properties, equation);
88  // Since we will not symex any further we can decide the status
89  // of all properties that do not occur in the equation now.
90  // The current behavior is PASS.
91  update_status_of_not_checked_properties(properties, updated_properties);
92 }
propertiest
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:75
show_program
void show_program(const namespacet &ns, const symex_target_equationt &equation)
Print the steps of equation on the standard output.
Definition: show_program.cpp:59
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.
Definition: bmc_util.cpp:321
multi_path_symex_only_checkert::symex_symbol_table
symbol_tablet symex_symbol_table
Definition: multi_path_symex_only_checker.h:31
ui_message_handlert
Definition: ui_message.h:20
incremental_goto_checkert::resultt
Definition: incremental_goto_checker.h:41
optionst
Definition: options.h:23
show_vcc.h
Output of the verification conditions (VCCs)
incremental_goto_checkert::options
const optionst & options
Definition: incremental_goto_checker.h:89
optionst::get_option
const std::string get_option(const std::string &option) const
Definition: options.cpp:67
multi_path_symex_only_checker.h
Goto Checker using Multi-Path Symbolic Execution only (no SAT solving)
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.
Definition: bmc_util.cpp:273
invariant.h
multi_path_symex_only_checkert::multi_path_symex_only_checkert
multi_path_symex_only_checkert(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
Definition: multi_path_symex_only_checker.cpp:22
multi_path_symex_only_checkert::equation
symex_target_equationt equation
Definition: multi_path_symex_only_checker.h:33
update_properties_from_goto_model
void update_properties_from_goto_model(propertiest &properties, const abstract_goto_modelt &goto_model)
Updates properties with the assertions in goto_model.
Definition: properties.cpp:73
multi_path_symex_only_checkert::symex
symex_bmct symex
Definition: multi_path_symex_only_checker.h:36
multi_path_symex_only_checkert::ns
namespacet ns
Definition: multi_path_symex_only_checker.h:32
bmc_util.h
Bounded Model Checking Utilities.
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.
Definition: bmc_util.cpp:237
goto_symext::symex_from_entry_point_of
virtual void symex_from_entry_point_of(const get_goto_functiont &get_goto_function, symbol_tablet &new_symbol_table)
Symbolically execute the entire program starting from entry point.
Definition: symex_main.cpp:470
multi_path_symex_only_checkert::goto_model
abstract_goto_modelt & goto_model
Definition: multi_path_symex_only_checker.h:30
multi_path_symex_only_checkert::update_properties
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.
Definition: multi_path_symex_only_checker.cpp:79
show_vcc
void show_vcc(const optionst &options, ui_message_handlert &ui_message_handler, const symex_target_equationt &equation)
Output equations from equation to a file or to the standard output.
Definition: show_vcc.cpp:169
incremental_goto_checkert
An implementation of incremental_goto_checkert provides functionality for checking a set of propertie...
Definition: incremental_goto_checker.h:34
setup_symex
void setup_symex(symex_bmct &symex, const namespacet &ns, const optionst &options, ui_message_handlert &ui_message_handler)
Definition: bmc_util.cpp:178
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
goto_symext::get_goto_function
static get_goto_functiont get_goto_function(abstract_goto_modelt &goto_model)
Return a function to get/load a goto function from the given goto model Create a default delegate to ...
Definition: symex_main.cpp:493
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.
Definition: bmc_util.cpp:305
incremental_goto_checkert::resultt::updated_properties
std::unordered_set< irep_idt > updated_properties
Changed properties since the last call to incremental_goto_checkert::operator()
Definition: incremental_goto_checker.h:59
show_program.h
Output of the program (SSA) constraints.
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition: abstract_goto_model.h:21
incremental_goto_checkert::ui_message_handler
ui_message_handlert & ui_message_handler
Definition: incremental_goto_checker.h:90
memory_model.h
Memory models for partial order concurrency.
show_byte_ops
void show_byte_ops(const optionst &options, ui_message_handlert &ui_message_handler, const namespacet &ns, const symex_target_equationt &equation)
Count and display all byte extract and byte update operations from equation on standard output or fil...
Definition: show_program.cpp:321
multi_path_symex_only_checkert::operator()
resultt operator()(propertiest &) override
Check whether the given properties with status NOT_CHECKED, UNKNOWN or properties newly discovered by...
Definition: multi_path_symex_only_checker.cpp:42
multi_path_symex_only_checkert::generate_equation
virtual void generate_equation()
Generates the equation by running goto-symex.
Definition: multi_path_symex_only_checker.cpp:72