Commit 2e184c74 authored by Henrich Lauko's avatar Henrich Lauko

lart: Generate abstract operations for branches instead of placeholders.

parent 7d2f83bb
......@@ -14,7 +14,7 @@ DIVINE_RELAX_WARNINGS
DIVINE_UNRELAX_WARNINGS
#include <brick-assert>
#include <lart/abstract/placeholder.h>
#include <lart/abstract/operation.h>
#include <lart/abstract/assume.h>
#include <lart/abstract/util.h>
#include <lart/analysis/edge.h>
......@@ -61,10 +61,13 @@ namespace {
llvm::IRBuilder<> irb( &*edgebb->getFirstInsertionPt() );
APlaceholderBuilder builder;
OperationBuilder builder;
auto ph = builder.construct< Placeholder::Type::Assume >( cond, irb );
meta::abstract::inherit( ph.inst, cond );
auto op = builder.construct< Operation::Type::Assume >( cond, irb );
auto abs = cond->getModule()->getFunction( "lart.abstract.assume" );
auto tag = meta::tag::operation::index;
op.inst->setMetadata( tag, abs->getMetadata( tag ) );
// Correct phis after edge splitting
replace_phis_incoming_bbs( to, from, edgebb );
......@@ -82,7 +85,7 @@ namespace {
}
void AddAssumes::run( Module & m ) {
for ( const auto & ph : placeholders< Placeholder::Type::ToBool >( m ) )
for ( const auto & ph : operations< Operation::Type::ToBool >( m ) )
for ( auto * u : ph.inst->users() )
if ( auto * br = llvm::dyn_cast< llvm::BranchInst >( u ) )
process( br );
......
......@@ -2,29 +2,34 @@
#include <lart/abstract/branching.h>
#include <lart/support/util.h>
#include <lart/abstract/placeholder.h>
#include <lart/abstract/operation.h>
namespace lart::abstract {
void LowerToBool::run( llvm::Module & m ) {
auto conditional = [] ( llvm::Value * val ) {
return query::query( val->users() ).any( [] ( auto * u ) {
return llvm::isa< llvm::BranchInst >( u );
} );
};
APlaceholderBuilder builder;
for ( const auto & ph : placeholders( m ) ) {
auto op = ph.inst->getOperand( 0 );
if ( conditional( op ) ) {
auto cond = builder.construct< Placeholder::Type::ToBool >( ph.inst );
for ( auto * u : op->users() )
if ( auto br = llvm::dyn_cast< llvm::BranchInst >( u ) )
br->setCondition( cond.inst );
}
void LowerToBool::run( llvm::Module & m )
{
auto brs = query::query( m ).flatten().flatten()
.map( query::llvmdyncast< llvm::BranchInst > )
.filter( query::notnull )
.filter( [] ( auto br ) {
if ( br->isConditional() )
return meta::abstract::has( br->getCondition() );
return false;
} ).freeze();
auto tag = meta::tag::operation::index;
auto index = m.getFunction( "lart.abstract.to_tristate" )->getMetadata( tag );
OperationBuilder builder;
for ( auto * br : brs ) {
auto abs = llvm::cast< llvm::Instruction >( meta::get_dual( br->getCondition() ) );
auto cond = builder.construct< Operation::Type::ToBool >( abs );
cond.inst->setMetadata( tag, index );
br->setCondition( cond.inst );
};
}
}
} // namespace lart::abstract
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment