Skip to content

move bit-level BMC to property_checker #647

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Aug 29, 2024
Merged

move bit-level BMC to property_checker #647

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
267 changes: 0 additions & 267 deletions src/ebmc/ebmc_base.cpp
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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