Skip to content

Commit

Permalink
move bit-level BMC to property_checker
Browse files Browse the repository at this point in the history 
This moves the bit-level BMC engine invocation from ebmc_baset to
property_checker(...).
  • Loading branch information
@kroening
kroening committed Aug 27, 2024
1 parent 0fc2ab6 commit a59dcd5
Show file tree
Hide file tree
Showing 5 changed files with 278 additions and 287 deletions.
267 changes: 0 additions & 267 deletions src/ebmc/ebmc_base.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,27 +10,14 @@ Author: Daniel Kroening, [email protected]

#include <util/cmdline.h>
#include <util/config.h>
#include <util/expr_util.h>
#include <util/string2int.h>

#include <solvers/prop/literal_expr.h>
#include <solvers/sat/satcheck.h>
#include <trans-netlist/compute_ct.h>
#include <trans-netlist/ldg.h>
#include <trans-netlist/trans_to_netlist.h>
#include <trans-netlist/trans_trace_netlist.h>
#include <trans-netlist/unwind_netlist.h>
#include <trans-word-level/trans_trace_word_level.h>
#include <trans-word-level/unwind.h>

#include "dimacs_writer.h"
#include "ebmc_error.h"
#include "ebmc_solver_factory.h"
#include "ebmc_version.h"
#include "output_file.h"
#include "report_results.h"

#include <chrono>
#include <iostream>

/*******************************************************************\
Expand All @@ -54,260 +41,6 @@ ebmc_baset::ebmc_baset(

/*******************************************************************\
Function: ebmc_baset::finish_bit_level_bmc
Inputs:
Outputs:
Purpose:
\*******************************************************************/

int ebmc_baset::finish_bit_level_bmc(const bmc_mapt &bmc_map, propt &solver)
{
auto sat_start_time = std::chrono::steady_clock::now();

message.status() << "Solving with " << solver.solver_text() << messaget::eom;

for(propertyt &property : properties.properties)
{
if(property.is_disabled())
continue;

if(property.is_failure())
continue;

if(property.is_assumed())
continue;

message.status() << "Checking " << property.name << messaget::eom;

literalt property_literal=!solver.land(property.timeframe_literals);

bvt assumptions;
assumptions.push_back(property_literal);

propt::resultt prop_result = solver.prop_solve(assumptions);

switch(prop_result)
{
case propt::resultt::P_SATISFIABLE:
{
property.refuted();
message.result() << "SAT: counterexample found" << messaget::eom;

namespacet ns(transition_system.symbol_table);

property.witness_trace =
compute_trans_trace(property.timeframe_literals, bmc_map, solver, ns);
}
break;

case propt::resultt::P_UNSATISFIABLE:
message.result() << "UNSAT: No counterexample found within bound"
<< messaget::eom;
property.proved_with_bound(bound);
break;

case propt::resultt::P_ERROR:
message.error() << "Error from decision procedure" << messaget::eom;
return 2;

default:
message.error() << "Unexpected result from decision procedure"
<< messaget::eom;
return 1;
}
}

auto sat_stop_time = std::chrono::steady_clock::now();

message.statistics()
<< "Solver time: "
<< std::chrono::duration<double>(sat_stop_time - sat_start_time).count()
<< messaget::eom;

return properties.exit_code();
}

/*******************************************************************\
Function: ebmc_baset::get_bound
Inputs:
Outputs:
Purpose:
\*******************************************************************/

bool ebmc_baset::get_bound()
{
if(!cmdline.isset("bound"))
{
message.warning() << "using default bound 1" << messaget::eom;
bound=1;
return false;
}

bound=unsafe_string2unsigned(cmdline.get_value("bound"));

return false;
}

/*******************************************************************\
Function: ebmc_baset::do_bit_level_bmc
Inputs:
Outputs:
Purpose:
\*******************************************************************/

int ebmc_baset::do_bit_level_bmc(cnft &solver, bool convert_only)
{
if(get_bound()) return 1;

int result;

try
{
bmc_mapt bmc_map;

if(!convert_only)
if(properties.properties.empty())
throw "no properties";

netlistt netlist;
if(make_netlist(netlist))
throw 0;

message.status() << "Unwinding Netlist" << messaget::eom;

bmc_map.map_timeframes(netlist, bound+1, solver);

::unwind(netlist, bmc_map, message, solver);

const namespacet ns(transition_system.symbol_table);

// convert the properties
for(propertyt &property : properties.properties)
{
if(property.is_disabled())
continue;

if(!netlist_bmc_supports_property(property.normalized_expr))
{
property.failure("property not supported by netlist BMC engine");
continue;
}

// look up the property in the netlist
auto netlist_property = netlist.properties.find(property.identifier);
CHECK_RETURN(netlist_property != netlist.properties.end());

::unwind_property(
netlist_property->second, bmc_map, property.timeframe_literals);

if(property.is_assumed())
{
// force these to be true
for(auto l : property.timeframe_literals)
solver.l_set_to(l, true);
}
else
{
// freeze for incremental usage
for(auto l : property.timeframe_literals)
solver.set_frozen(l);
}
}

if(convert_only)
result=0;
else
{
result = finish_bit_level_bmc(bmc_map, solver);
report_results(cmdline, properties, ns, message.get_message_handler());
}
}

catch(const char *e)
{
message.error() << e << messaget::eom;
return 10;
}

catch(const std::string &e)
{
message.error() << e << messaget::eom;
return 10;
}

catch(int)
{
return 10;
}

return result;
}

/*******************************************************************\
Function: ebmc_baset::do_bit_level_bmc
Inputs:
Outputs:
Purpose:
\*******************************************************************/

int ebmc_baset::do_bit_level_bmc()
{
if(cmdline.isset("dimacs"))
{
if(cmdline.isset("outfile"))
{
auto outfile = output_filet{cmdline.get_value("outfile")};

message.status() << "Writing DIMACS CNF to `" << outfile.name() << "'"
<< messaget::eom;

dimacs_cnf_writert dimacs_cnf_writer{
outfile.stream(), message.get_message_handler()};

return do_bit_level_bmc(dimacs_cnf_writer, true);
}
else
{
dimacs_cnf_writert dimacs_cnf_writer{
std::cout, message.get_message_handler()};

return do_bit_level_bmc(dimacs_cnf_writer, true);
}
}
else
{
if(cmdline.isset("outfile"))
throw ebmc_errort()
<< "Cannot write to outfile without file format option";

satcheckt satcheck{message.get_message_handler()};

message.status() << "Using " << satcheck.solver_text() << messaget::eom;

return do_bit_level_bmc(satcheck, false);
}
}
/*******************************************************************\
Function: ebmc_baset::get_properties
Inputs:
Expand Down
7 changes: 0 additions & 7 deletions src/ebmc/ebmc_base.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,12 +43,6 @@ class ebmc_baset
messaget message;
const cmdlinet &cmdline;

bool get_bound();

// bit-level
int do_bit_level_bmc(cnft &solver, bool convert_only);
int finish_bit_level_bmc(const bmc_mapt &bmc_map, propt &solver);

bool parse_property(const std::string &property);
bool get_model_properties();
void show_properties();
Expand All @@ -63,7 +57,6 @@ class ebmc_baset

public:
int do_compute_ct();
int do_bit_level_bmc();
};

#endif
13 changes: 5 additions & 8 deletions src/ebmc/ebmc_parse_options.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -304,14 +304,11 @@ int ebmc_parse_optionst::doit()
if(cmdline.isset("compute-ct"))
return ebmc_base.do_compute_ct();

if(cmdline.isset("aig") || cmdline.isset("dimacs"))
return ebmc_base.do_bit_level_bmc();
else
return property_checker(
cmdline,
ebmc_base.transition_system,
ebmc_base.properties,
ui_message_handler);
return property_checker(
cmdline,
ebmc_base.transition_system,
ebmc_base.properties,
ui_message_handler);
}
}
catch(const ebmc_errort &ebmc_error)
Expand Down
Loading

0 comments on commit a59dcd5

Please sign in to comment.