From ed76761f1bc5c3c028a368e495c2c60423b5c4ea Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Luk=C3=A1=C5=A1=20Koren=C4=8Dik?= <xkorenc1@fi.muni.cz>
Date: Thu, 30 Jan 2020 13:50:38 +0000
Subject: [PATCH] ra: Add indent in namespace and remove comment at the end.
---
divine/ra/base.hpp | 105 +++++++++++-----------
divine/ra/llvmrefine.cpp | 100 ++++++++++-----------
divine/ra/llvmrefine.hpp | 184 +++++++++++++++++++--------------------
divine/ra/test.hpp | 1 +
divine/ra/util.hpp | 27 +++---
5 files changed, 209 insertions(+), 208 deletions(-)
diff --git a/divine/ra/base.hpp b/divine/ra/base.hpp
index eb67466bc..3e2e180c7 100644
--- a/divine/ra/base.hpp
+++ b/divine/ra/base.hpp
@@ -34,58 +34,57 @@ DIVINE_UNRELAX_WARNINGS
namespace divine::ra {
-// Preset minimal attributes needed to be passed to divine::mc::make_job
-struct _BitCode : divine::mc::BitCode
-{
- _BitCode( std::unique_ptr< llvm::Module > m,
- std::shared_ptr< llvm::LLVMContext > ctx,
- const divine::mc::BCOptions &opts)
- : BitCode( std::move( m ), ctx )
+ // Preset minimal attributes needed to be passed to divine::mc::make_job
+ struct _BitCode : divine::mc::BitCode
{
- this->set_options( opts );
- this->init();
- }
-};
-
-struct refinement_t
-{
- using BCOptions = divine::mc::BCOptions;
-
- BCOptions _bc_opts;
-
- // Order is important because of dtors
- std::shared_ptr< llvm::LLVMContext > _ctx = std::make_shared< llvm::LLVMContext >();
- std::unique_ptr< llvm::Module > _m;
-
- refinement_t( std::shared_ptr< llvm::LLVMContext > ctx,
- std::unique_ptr< llvm::Module > m,
- const BCOptions &bc_opts )
- : _ctx( std::move( ctx ) ),
- _m ( std::move( m ) ),
- _bc_opts( bc_opts )
- {}
-
- refinement_t( const BCOptions &bc_opts ) : _bc_opts( bc_opts )
+ _BitCode( std::unique_ptr< llvm::Module > m,
+ std::shared_ptr< llvm::LLVMContext > ctx,
+ const divine::mc::BCOptions &opts)
+ : BitCode( std::move( m ), ctx )
+ {
+ this->set_options( opts );
+ this->init();
+ }
+ };
+
+ struct refinement_t
{
- if ( _bc_opts.input_file.name.empty() )
- UNREACHABLE( "Invalid options passed to refinement_t input_file is missing" );
- _m = util::load_bc( _bc_opts.input_file.name, &*_ctx );
- }
-
- auto make_bc() {
- return std::make_shared< _BitCode >( llvm::CloneModule( *_m ), _ctx, _bc_opts );
- }
-
- template< template<typename, typename> class job_t = divine::mc::Safety >
- auto run() {
- auto bc = make_bc();
- auto safe = mc::make_job< job_t >( bc, ss::passive_listen() );
- // FIXME: thread_count
- safe->start( 1 );
- safe->wait();
- return std::pair( std::move( safe ), std::move( bc ) );
- }
-
-};
-
-} // namespace divine::ra
+ using BCOptions = divine::mc::BCOptions;
+
+ BCOptions _bc_opts;
+
+ // Order is important because of dtors
+ std::shared_ptr< llvm::LLVMContext > _ctx = std::make_shared< llvm::LLVMContext >();
+ std::unique_ptr< llvm::Module > _m;
+
+ refinement_t( std::shared_ptr< llvm::LLVMContext > ctx,
+ std::unique_ptr< llvm::Module > m,
+ const BCOptions &bc_opts )
+ : _ctx( std::move( ctx ) ),
+ _m ( std::move( m ) ),
+ _bc_opts( bc_opts )
+ {}
+
+ refinement_t( const BCOptions &bc_opts ) : _bc_opts( bc_opts )
+ {
+ if ( _bc_opts.input_file.name.empty() )
+ UNREACHABLE( "Invalid options passed to refinement_t input_file is missing" );
+ _m = util::load_bc( _bc_opts.input_file.name, &*_ctx );
+ }
+
+ auto make_bc() {
+ return std::make_shared< _BitCode >( llvm::CloneModule( *_m ), _ctx, _bc_opts );
+ }
+
+ template< template<typename, typename> class job_t = divine::mc::Safety >
+ auto run() {
+ auto bc = make_bc();
+ auto safe = mc::make_job< job_t >( bc, ss::passive_listen() );
+ // FIXME: thread_count
+ safe->start( 1 );
+ safe->wait();
+ return std::pair( std::move( safe ), std::move( bc ) );
+ }
+
+ };
+}
diff --git a/divine/ra/llvmrefine.cpp b/divine/ra/llvmrefine.cpp
index 4919b9107..bf9a7d7a2 100644
--- a/divine/ra/llvmrefine.cpp
+++ b/divine/ra/llvmrefine.cpp
@@ -17,66 +17,66 @@
namespace divine::ra {
-void ce_t::_create_ctx( dbg_ctx_t &dbg_ctx, mc::Job &job )
-{
- auto trace = job.ce_trace();
+ void ce_t::_create_ctx( dbg_ctx_t &dbg_ctx, mc::Job &job )
+ {
+ auto trace = job.ce_trace();
- if ( job.result() == mc::Result::BootError )
- UNREACHABLE( "Refinement encountered an unexpected boot error." );
+ if ( job.result() == mc::Result::BootError )
+ UNREACHABLE( "Refinement encountered an unexpected boot error." );
- job.dbg_fill( dbg_ctx );
- dbg_ctx.load( trace.final );
+ job.dbg_fill( dbg_ctx );
+ dbg_ctx.load( trace.final );
- dbg_ctx._lock = trace.steps.back();
- dbg_ctx._lock_mode = dbg_ctx_t::LockBoth;
- vm::setup::scheduler( dbg_ctx );
- using Stepper = dbg::Stepper< dbg_ctx_t >;
- Stepper step;
- step._stop_on_error = true;
- step._stop_on_accept = true;
- step._ff_components = dbg::component::kernel;
- step.run( dbg_ctx, Stepper::Quiet );
-}
+ dbg_ctx._lock = trace.steps.back();
+ dbg_ctx._lock_mode = dbg_ctx_t::LockBoth;
+ vm::setup::scheduler( dbg_ctx );
+ using Stepper = dbg::Stepper< dbg_ctx_t >;
+ Stepper step;
+ step._stop_on_error = true;
+ step._stop_on_accept = true;
+ step._ff_components = dbg::component::kernel;
+ step.run( dbg_ctx, Stepper::Quiet );
+ }
-auto ce_t::stack_trace() -> stack_trace_t
-{
- stack_trace_t out;
- auto gather = [ & ]( auto frame, auto &heap, auto &info ) {
- vm::PointerV current_pc;
- heap.read_shift( frame, current_pc );
- auto [ inst, pc ] = info.find( nullptr, current_pc.cooked() );
- out.push_back( inst );
- };
- stack_trace( gather );
- return out;
-}
+ auto ce_t::stack_trace() -> stack_trace_t
+ {
+ stack_trace_t out;
+ auto gather = [ & ]( auto frame, auto &heap, auto &info ) {
+ vm::PointerV current_pc;
+ heap.read_shift( frame, current_pc );
+ auto [ inst, pc ] = info.find( nullptr, current_pc.cooked() );
+ out.push_back( inst );
+ };
+ stack_trace( gather );
+ return out;
+ }
-void remove_indirect_calls::enhance( ce_t &counter_example )
-{
- std::optional< std::pair< llvm::Function *, llvm::Function * > > target;
- auto gather = [ & ]( auto frame, auto &heap, auto &info )
+ void remove_indirect_calls::enhance( ce_t &counter_example )
{
- if ( target ) return;
+ std::optional< std::pair< llvm::Function *, llvm::Function * > > target;
+ auto gather = [ & ]( auto frame, auto &heap, auto &info )
+ {
+ if ( target ) return;
- vm::PointerV current_pc;
- heap.read_shift( frame, current_pc );
- auto where = info.function( current_pc.cooked() );
+ vm::PointerV current_pc;
+ heap.read_shift( frame, current_pc );
+ auto where = info.function( current_pc.cooked() );
- if ( !llvm_pass.is_wrapper( where ) ) return;
+ if ( !llvm_pass.is_wrapper( where ) ) return;
- vm::PointerV first_arg;
+ vm::PointerV first_arg;
- // Get rid of the parent frame first
- heap.read_shift( frame, first_arg );
- heap.read_shift( frame, first_arg );
- target = { where, info.function( first_arg.cooked() ) };
- };
+ // Get rid of the parent frame first
+ heap.read_shift( frame, first_arg );
+ heap.read_shift( frame, first_arg );
+ target = { where, info.function( first_arg.cooked() ) };
+ };
- counter_example.stack_trace( gather );
- ASSERT( target );
+ counter_example.stack_trace( gather );
+ ASSERT( target );
- auto [ where, callee ] = *target;
- llvm_pass.enhance( where, callee );
-}
+ auto [ where, callee ] = *target;
+ llvm_pass.enhance( where, callee );
+ }
-} // namespace divine::ra
+}
diff --git a/divine/ra/llvmrefine.hpp b/divine/ra/llvmrefine.hpp
index 7c64becea..0b3d39020 100644
--- a/divine/ra/llvmrefine.hpp
+++ b/divine/ra/llvmrefine.hpp
@@ -38,113 +38,113 @@ DIVINE_UNRELAX_WARNINGS
namespace divine::ra {
-struct ce_t
-{
- using stack_trace_t = std::vector< llvm::Instruction * >;
- using dbg_ctx_t = dbg::Context< vm::CowHeap >;
+ struct ce_t
+ {
+ using stack_trace_t = std::vector< llvm::Instruction * >;
+ using dbg_ctx_t = dbg::Context< vm::CowHeap >;
- dbg::Info info;
- dbg_ctx_t dbg_ctx;
+ dbg::Info info;
+ dbg_ctx_t dbg_ctx;
- ce_t( mc::Job &job, mc::BitCode *bc )
- : info( *bc->_program, *bc->_module ),
- dbg_ctx( bc->program(), bc->debug() )
- {
- _create_ctx( dbg_ctx, job );
- }
+ ce_t( mc::Job &job, mc::BitCode *bc )
+ : info( *bc->_program, *bc->_module ),
+ dbg_ctx( bc->program(), bc->debug() )
+ {
+ _create_ctx( dbg_ctx, job );
+ }
- void _create_ctx( dbg_ctx_t &dbg_ctx, mc::Job &job );
+ void _create_ctx( dbg_ctx_t &dbg_ctx, mc::Job &job );
- stack_trace_t stack_trace();
+ stack_trace_t stack_trace();
- template< typename Yield >
- void stack_trace( Yield &&yield )
- {
- auto &heap = dbg_ctx.heap();
+ template< typename Yield >
+ void stack_trace( Yield &&yield )
+ {
+ auto &heap = dbg_ctx.heap();
- vm::PointerV iter_frame( dbg_ctx.frame() );
- vm::PointerV parent;
+ vm::PointerV iter_frame( dbg_ctx.frame() );
+ vm::PointerV parent;
- while ( !iter_frame.cooked().null() )
+ while ( !iter_frame.cooked().null() )
+ {
+ yield( iter_frame, heap, info );
+ // First entry of frame is program counter
+ heap.read_shift( iter_frame, parent );
+ heap.read_shift( iter_frame, parent );
+ iter_frame = parent;
+ }
+ }
+
+ template< typename Stream >
+ static Stream &trace( Stream &os, const stack_trace_t& stack_trace )
{
- yield( iter_frame, heap, info );
- // First entry of frame is program counter
- heap.read_shift( iter_frame, parent );
- heap.read_shift( iter_frame, parent );
- iter_frame = parent;
+ os << "Stack trace:" << std::endl;
+ for ( auto frame : stack_trace )
+ os << "\t"
+ << ( frame ? frame->getFunction()->getName().str() : "nullptr" )
+ << std::endl;
+ return os;
}
- }
+ };
- template< typename Stream >
- static Stream &trace( Stream &os, const stack_trace_t& stack_trace )
- {
- os << "Stack trace:" << std::endl;
- for ( auto frame : stack_trace )
- os << "\t" << ( frame ? frame->getFunction()->getName().str() : "nullptr" )
- << std::endl;
- return os;
- }
-};
-
-// TODO: Maybe let refiner_t be mixin?
-template< typename refiner_t >
-struct llvm_refinement : refinement_t
-{
- using BCOptions = refinement_t::BCOptions;
-
- refiner_t _refiner;
-
- llvm_refinement( std::shared_ptr< llvm::LLVMContext > ctx,
- std::unique_ptr< llvm::Module > m,
- const BCOptions &bc_opts )
- : refinement_t( std::move( ctx ), std::move( m ), bc_opts ),
- _refiner( *_m )
- {}
-
- llvm_refinement( const BCOptions &bc_opts )
- : refinement_t( bc_opts ), _refiner( *_m )
- {}
-
- bool iterate( uint64_t n )
+ // TODO: Maybe let refiner_t be mixin?
+ template< typename refiner_t >
+ struct llvm_refinement : refinement_t
{
- if ( n == 0 ) return false;
- if ( n == 1 ) return iterate();
- iterate();
- return iterate( n - 1 );
- }
+ using BCOptions = refinement_t::BCOptions;
- void finish()
- {
- while ( !iterate() ) {}
- }
-
- bool iterate() {
- auto [ result, bc ] = this->run();
- if ( result->result() == mc::Result::Valid )
- return true;
- ce_t ce( *result, bc.get() );
- _refiner.enhance( ce );
- return false;
- }
-
- std::string report() { _refiner.report(); }
-};
-
-struct remove_indirect_calls
-{
- lart::divine::rewire_calls_t llvm_pass;
-
- remove_indirect_calls( llvm::Module &m ) : llvm_pass( m )
+ refiner_t _refiner;
+
+ llvm_refinement( std::shared_ptr< llvm::LLVMContext > ctx,
+ std::unique_ptr< llvm::Module > m,
+ const BCOptions &bc_opts )
+ : refinement_t( std::move( ctx ), std::move( m ), bc_opts ),
+ _refiner( *_m )
+ {}
+
+ llvm_refinement( const BCOptions &bc_opts )
+ : refinement_t( bc_opts ), _refiner( *_m )
+ {}
+
+ bool iterate( uint64_t n )
+ {
+ if ( n == 0 ) return false;
+ if ( n == 1 ) return iterate();
+ iterate();
+ return iterate( n - 1 );
+ }
+
+ void finish()
+ {
+ while ( !iterate() ) {}
+ }
+
+ bool iterate() {
+ auto [ result, bc ] = this->run();
+ if ( result->result() == mc::Result::Valid )
+ return true;
+ ce_t ce( *result, bc.get() );
+ _refiner.enhance( ce );
+ return false;
+ }
+
+ std::string report() { _refiner.report(); }
+ };
+
+ struct remove_indirect_calls
{
- llvm_pass.init();
- }
+ lart::divine::rewire_calls_t llvm_pass;
- void enhance( ce_t &counter_example );
+ remove_indirect_calls( llvm::Module &m ) : llvm_pass( m )
+ {
+ llvm_pass.init();
+ }
- std::string report() { return llvm_pass.report(); }
-};
+ void enhance( ce_t &counter_example );
-using indirect_calls_refinement_t = llvm_refinement< remove_indirect_calls >;
+ std::string report() { return llvm_pass.report(); }
+ };
-} // namespace divine::ra
+ using indirect_calls_refinement_t = llvm_refinement< remove_indirect_calls >;
+}
diff --git a/divine/ra/test.hpp b/divine/ra/test.hpp
index a7dac4bc3..82a6aa9d2 100644
--- a/divine/ra/test.hpp
+++ b/divine/ra/test.hpp
@@ -38,6 +38,7 @@ DIVINE_UNRELAX_WARNINGS
#include <divine/ra/llvmrefine.hpp>
namespace divine::t_ra {
+
struct base {
static const bool dont_link = false;
static const bool verbose = false;
diff --git a/divine/ra/util.hpp b/divine/ra/util.hpp
index a06f7e731..502362b88 100644
--- a/divine/ra/util.hpp
+++ b/divine/ra/util.hpp
@@ -28,22 +28,23 @@ DIVINE_UNRELAX_WARNINGS
namespace divine::ra::util {
-std::unique_ptr< llvm::Module > load_bc( const std::string &str, llvm::LLVMContext *ctx )
-{
- using namespace llvm::object;
+ std::unique_ptr< llvm::Module > load_bc( const std::string &str,
+ llvm::LLVMContext *ctx )
+ {
+ using namespace llvm::object;
- std::unique_ptr< llvm::MemoryBuffer > input =
- std::move( llvm::MemoryBuffer::getFile( str ).get() );
- auto bc_input = IRObjectFile::findBitcodeInMemBuffer( input->getMemBufferRef() );
+ std::unique_ptr< llvm::MemoryBuffer > input =
+ std::move( llvm::MemoryBuffer::getFile( str ).get() );
+ auto bc_input = IRObjectFile::findBitcodeInMemBuffer( input->getMemBufferRef() );
- if ( !bc_input )
- UNREACHABLE( "Could not load bitcode file" );
- auto module = llvm::parseBitcodeFile( bc_input.get(), *ctx );
+ if ( !bc_input )
+ UNREACHABLE( "Could not load bitcode file" );
+ auto module = llvm::parseBitcodeFile( bc_input.get(), *ctx );
- if ( !module )
- UNREACHABLE( "Error parsing input model; probably not a valid bc file." );
+ if ( !module )
+ UNREACHABLE( "Error parsing input model; probably not a valid bc file." );
- return std::move( module.get() );
-}
+ return std::move( module.get() );
+ }
} // namespace divine::ra::util
--
GitLab