diff --git a/divine/mc/machine.hpp b/divine/mc/machine.hpp
index d0ed8448b3ef6b9461409c3f2b035d4a3cd3da08..e66ddf3cca7632868fd640638d8d37b7f26913b7 100644
--- a/divine/mc/machine.hpp
+++ b/divine/mc/machine.hpp
@@ -29,14 +29,16 @@
#include <divine/vm/setup.hpp>
#include <divine/vm/eval.tpp> // FIXME
+#include <brick-compose>
+
#include <set>
#include <memory>
#include <random>
namespace divine::mc
{
-
using namespace std::literals;
+ namespace ctx = vm::ctx;
using BC = std::shared_ptr< BitCode >;
using HT = brq::concurrent_hash_set< Snapshot >;
@@ -124,179 +126,224 @@ namespace divine::mc
namespace divine::mc::machine
{
- template< typename Solver, bool randomize = false >
- struct Tree : TQ::Skel
+ struct with_pools
{
- using Hasher = mc::Hasher< Solver >;
- using PointerV = vm::value::Pointer;
- using Context = MContext;
- using Eval = vm::Eval< Context >;
- using Env = std::vector< std::string >;
using Pool = vm::CowHeap::Pool;
- auto &program() { return _bc->program(); }
- auto &debug() { return _bc->debug(); }
- auto &heap() { return context().heap(); }
- Context &context() { return _ctx; }
-
- Solver _solver;
- BC _bc;
- Context _ctx;
- std::mt19937 rand;
-
Pool _snap_pool, _state_pool;
brick::mem::RefPool< Pool, uint8_t > _snap_refcnt;
- std::shared_ptr< std::atomic< int64_t > > _total_instructions;
+ with_pools() : _snap_refcnt( _snap_pool ) {}
- void update_instructions()
+ void queue_choices( TQ &tq, Snapshot snap, Origin origin, vm::State state, int take, int total )
{
- *_total_instructions += context().instruction_count();
- context().instruction_count( 0 );
+ for ( int i = 0; i < total; ++i )
+ if ( i != take )
+ {
+ _snap_refcnt.get( snap );
+ tq.add< Task::Choose >( snap, origin, state, i, total );
+ }
}
- Tree( BC bc )
- : Tree( bc, Context() )
+ int select_choice( TQ &tq, Snapshot snap, Origin origin, vm::State state, int count )
{
- _ctx.program( bc->program() );
+ queue_choices( tq, snap, origin, state, 0, count );
+ return 0;
}
+ };
- Tree( BC bc, const Context &ctx )
- : _bc( bc ), _ctx( ctx ), _snap_refcnt( _snap_pool ),
- _total_instructions( new std::atomic< int64_t >( 0 ) )
+ struct with_counters
+ {
+ std::shared_ptr< std::atomic< int64_t > > _total_instructions;
+
+ with_counters()
+ : _total_instructions( new std::atomic< int64_t >( 0 ) )
{}
+ };
- ~Tree()
- {
- ASSERT_EQ( _snap_pool.stats().total.count.used, 0 );
- update_instructions();
- }
+ struct with_bc
+ {
+ using Env = std::vector< std::string >;
+ BC _bc;
- void choose( TQ &tq, Origin origin )
- {
- auto snap = context().snapshot( _snap_pool );
- auto state = context()._state;
+ void bc( BC bc ) { _bc = bc; }
+ auto &program() { return _bc->program(); }
+ auto &debug() { return _bc->debug(); }
+ };
- _snap_refcnt.get( snap );
+ template< typename solver_ >
+ struct with_solver
+ {
+ using solver_t = solver_;
+ solver_t _solver;
+ solver_t &solver();
+ };
- Eval eval( context() );
- context()._choice_take = context()._choice_count = 0;
- eval.refresh();
- eval.dispatch();
+ template< typename solver, typename next >
+ struct base_ : TQ::Skel, with_pools, with_counters, with_bc, with_solver< solver >, next
+ {
+ void boot( TQ & ) {}
+ };
+
+ template< typename next >
+ struct select_random_ : next
+ {
+ std::mt19937 rand;
+ int select_choice( TQ &tq, Snapshot snap, Origin origin, vm::State state, int count )
+ {
using dist = std::uniform_int_distribution< int >;
- if constexpr ( randomize )
- context()._choice_take = dist( 0, context()._choice_count - 1 )( rand );
+ int c = dist( 0, count - 1 )( rand );
+ this->queue_choices( tq, snap, origin, state, c, count );
+ }
+ };
- /* queue up all choices other than the selected */
- for ( int i = 0; i < context()._choice_count; ++i )
- if ( i != context()._choice_take )
- {
- _snap_refcnt.get( snap );
- tq.add< Task::Choose >( snap, origin, state, i, context()._choice_count );
- }
+ template< typename ctx, typename next >
+ struct with_context_ : next
+ {
+ using context_t = ctx;
+ ctx _ctx;
+ ctx &context() { return _ctx; }
+ auto &heap() { return context().heap(); }
- compute( tq, origin, snap );
+ void update_instructions()
+ {
+ *this->_total_instructions += context().instruction_count();
+ context().instruction_count( 0 );
}
- virtual std::pair< State, bool > store()
+ ~with_context_()
{
- return { State( context().snapshot( _state_pool ) ), true };
+ update_instructions();
}
+ };
- virtual bool loop_closed( Origin & )
+ template< typename next >
+ struct compute_ : next
+ {
+ using Eval = vm::Eval< typename next::context_t >;
+
+ void eval_choice( TQ &tq, Origin origin )
{
- return false;
+ auto snap = this->context().snapshot( this->_snap_pool );
+ auto state = this->context()._state;
+
+ this->_snap_refcnt.get( snap );
+
+ Eval eval( this->context() );
+ this->context()._choice_take = this->context()._choice_count = 0;
+ eval.refresh();
+ eval.dispatch();
+
+ this->context()._choice_take =
+ this->select_choice( tq, snap, origin, state, this->context()._choice_count );
+ compute( tq, origin, snap );
}
- void schedule( TQ &tq, Origin origin, Snapshot cont_from )
+ void eval_interrupt( TQ &tq, Origin origin, Snapshot cont_from )
{
- if ( context().frame().null() )
+ if ( this->context().frame().null() )
{
Label lbl;
- lbl.accepting = context().flags_any( _VM_CF_Accepting );
- lbl.error = context().flags_any( _VM_CF_Error );
- auto [ state, isnew ] = store();
+ lbl.accepting = this->context().flags_any( _VM_CF_Accepting );
+ lbl.error = this->context().flags_any( _VM_CF_Error );
+ auto [ state, isnew ] = this->store();
tq.add< StateTQ::Skel::Edge >( State( origin.snap ), state, lbl, isnew );
}
- else if ( !loop_closed( origin ) )
+ else if ( this->loop_closed( origin ) )
+ {
+ /* TODO: check for error/accepting flags */
+ }
+ else
return compute( tq, origin, cont_from );
}
bool feasible()
{
- if ( context().flags_any( _VM_CF_Cancel ) )
+ if ( this->context().flags_any( _VM_CF_Cancel ) )
return false;
- if ( context()._assume.null() )
+ if ( this->context()._assume.null() )
return true;
- // TODO validate the path condition
- return _solver.feasible( context().heap(), context()._assume );
+ return this->_solver.feasible( this->context().heap(), this->context()._assume );
}
void compute( TQ &tq, Origin origin, Snapshot cont_from = Snapshot() )
{
- auto destroy = [&]( auto p ) { heap().snap_put( _snap_pool, p, false ); };
-
+ auto destroy = [&]( auto p ) { this->heap().snap_put( this->_snap_pool, p, false ); };
auto cleanup = [&]
{
if ( cont_from )
- _snap_refcnt.put( cont_from, destroy );
+ this->_snap_refcnt.put( cont_from, destroy );
};
brick::types::Defer _( cleanup );
- Eval eval( context() );
+ Eval eval( this->context() );
bool choice = eval.run_seq( !!cont_from );
if ( !feasible() )
return;
if ( choice )
- choose( tq, origin );
+ eval_choice( tq, origin );
else
- schedule( tq, origin, cont_from );
-
+ eval_interrupt( tq, origin, cont_from );
}
- virtual void boot( TQ &tq )
+ bool boot( TQ &tq )
{
- Eval eval( context() );
- vm::setup::boot( context() );
+ this->context().program( this->program() );
+ Eval eval( this->context() );
+ vm::setup::boot( this->context() );
eval.run();
- }
+ next::boot( tq );
- using TQ::Skel::run;
+ if ( vm::setup::postboot_check( this->context() ) )
+ return tq.add< Task::Schedule >( this->store().first ), true;
+ else
+ return false;
+ }
- void run( TQ &tq, Task::Boot )
+ void schedule( TQ &tq, Task::Schedule e )
{
- boot( tq );
+ TRACE( "task (schedule)", e );
+ this->context().load( this->_state_pool, e.from.snap );
+ vm::setup::scheduler( this->context() );
+ compute( tq, Origin( e.from.snap ) );
+ }
- if ( vm::setup::postboot_check( context() ) )
- tq.add< Task::Schedule >( store().first );
+ void choose( TQ &tq, Task::Choose c )
+ {
+ TRACE( "task (choose)", c );
+ if ( !c.total )
+ return;
+ this->context().load( this->_snap_pool, c.snap );
+ this->context()._state = c.state;
+ this->context()._choice_take = c.choice;
+ this->context()._choice_count = c.total;
+ this->context().flush_ptr2i();
+ this->context().load_pc();
+ compute( tq, c.origin, c.snap );
}
+ };
- void run( TQ &tq, Task::Schedule e )
+ template< typename next >
+ struct tree_store_ : next
+ {
+ virtual std::pair< State, bool > store()
{
- context().load( _state_pool, e.from.snap );
- vm::setup::scheduler( context() );
- compute( tq, Origin( e.from.snap ) );
+ return { State( this->context().snapshot( this->_state_pool ) ), true };
}
- void run( TQ &tq, Task::Choose c )
+ virtual bool loop_closed( Origin & )
{
- context().load( _snap_pool, c.snap );
- context()._state = c.state;
- context()._choice_take = c.choice;
- context()._choice_count = c.total;
- context().flush_ptr2i();
- context().load_pc();
- compute( tq, c.origin, c.snap );
+ return false;
}
auto make_hasher()
{
- Hasher h( _state_pool, context().heap(), this->_solver );
- h._root = context().state_ptr();
+ Hasher h( this->_state_pool, this->context().heap(), this->_solver );
+ h._root = this->context().state_ptr();
ASSERT( !h._root.null() );
return h;
}
@@ -305,69 +352,100 @@ namespace divine::mc::machine
{
return make_hasher().equal_symbolic( a, b );
}
+
+ ~tree_store_()
+ {
+ ASSERT_EQ( this->_snap_pool.stats().total.count.used, 0 );
+ }
+
};
- template< typename Solver >
- struct Graph : Tree< Solver >
+ template< typename next >
+ struct graph_store_ : next
{
- using Hasher = mc::Hasher< Solver >;
- using Tree< Solver >::context;
+ using Hasher = mc::Hasher< typename next::solver_t >;
Hasher _hasher;
- struct Ext
- {
- HT ht_sched;
- bool overwrite = false;
- } _ext;
-
- Graph( BC bc ) : Tree< Solver >( bc ),
- _hasher( this->_state_pool, context().heap(), this->_solver )
- {}
+ HT _ht_sched;
auto &hasher() { return _hasher; }
- void enable_overwrite() { _ext.hasher.overwrite = true; }
bool equal( Snapshot a, Snapshot b ) { return hasher().equal_symbolic( a, b ); }
+ graph_store_() : _hasher( this->_state_pool, this->heap(), this->_solver ) {}
std::pair< State, bool > store( HT &table )
{
- auto snap = context().snapshot( this->_state_pool );
+ auto snap = this->context().snapshot( this->_state_pool );
auto r = table.insert( snap, hasher() );
if ( r->load() != snap )
{
ASSERT( !_hasher.overwrite );
ASSERT( !r.isnew() );
- context().heap().snap_put( this->_state_pool, snap );
+ this->heap().snap_put( this->_state_pool, snap );
}
return { State( *r ), r.isnew() };
}
- std::pair< State, bool > store() override
+ std::pair< State, bool > store()
{
- return store( _ext.ht_sched );
+ return store( _ht_sched );
}
- bool loop_closed( Origin &origin ) override
+ bool loop_closed( Origin &origin )
{
auto [ state, isnew ] = store( origin.ht_loop );
if ( isnew )
- context().flush_ptr2i();
+ this->context().flush_ptr2i();
else
- context().load( this->_state_pool, state.snap );
+ {
+ this->context().load( this->_state_pool, state.snap );
+ TRACE( "loop closed at", state.snap );
+ }
+
return !isnew;
}
- virtual void boot( TQ &tq ) override
+ void boot( TQ &tq )
{
- Tree< Solver >::boot( tq );
- hasher()._root = context().state_ptr();
+ next::boot( tq );
+ hasher()._root = this->context().state_ptr();
}
};
+
+ template< typename next >
+ struct dispatch_ : next
+ {
+ using next::run;
+
+ void run( TQ &tq, Task::Boot ) { next::boot( tq ); }
+ void run( TQ &tq, Task::Schedule e ) { next::schedule( tq, e ); }
+ void run( TQ &tq, Task::Choose c ) { next::choose( tq, c ); }
+ };
+
+ template< typename solver >
+ using base = brq::module< base_, solver >;
+
+ template< typename ctx >
+ using with_context = brq::module< with_context_, ctx >;
+
+ using compute = brq::module< compute_ >;
+ using select_random = brq::module< select_random_ >;
+ using tree_store = brq::module< tree_store_ >;
+ using graph_store = brq::module< graph_store_ >;
+ using dispatch = brq::module< dispatch_ >;
+
+ template< typename solver >
+ using tree = brq::compose_stack< dispatch, compute, tree_store,
+ with_context< MContext >, base< solver > >;
+
+ template< typename solver >
+ using graph = brq::compose_stack< dispatch, compute, graph_store, with_context< MContext >,
+ base< solver > >;
}
namespace divine::mc
{
- using TMachine = machine::Tree< smt::NoSolver >;
- using GMachine = machine::Graph< smt::NoSolver >;
+ using TMachine = machine::tree< smt::NoSolver >;
+ using GMachine = machine::graph< smt::NoSolver >;
template< typename M >
auto weave( M &machine )
diff --git a/divine/mc/t-machine.hpp b/divine/mc/t-machine.hpp
index fb0a876719b9860184a41f30a24d52f693328883..d7e455f21abd76a5ae463875030d790ac9137665 100644
--- a/divine/mc/t-machine.hpp
+++ b/divine/mc/t-machine.hpp
@@ -85,18 +85,22 @@ namespace divine::t_mc
TEST( instance )
{
auto bc = prog( "void __boot( void *e ) { __vm_ctl_flag( 0, 0b10000 ); }" );
- mc::TMachine m( bc );
+ mc::TMachine m;
+ m.bc( bc );
}
using Search = mc::Search< mc::TQ >;
using Expand = mc::TQ::Tasks::Expand;
using Edge = mc::TQ::Tasks::Edge;
+ auto tmachine( mc::BC bc ) { mc::TMachine tm; tm.bc( bc ); return tm; }
+ auto gmachine( mc::BC bc ) { mc::GMachine tm; tm.bc( bc ); return tm; }
+
TEST( simple )
{
bool found = false;
auto state = [&]( Expand ) { found = true; };
- auto machine = mc::TMachine( prog_int( 4, "x - 1" ) );
+ auto machine = tmachine( prog_int( 4, "x - 1" ) );
mc::weave( machine ).observe( state ).start();
ASSERT( found );
}
@@ -104,7 +108,7 @@ namespace divine::t_mc
TEST( hasher )
{
bool ran = false;
- auto machine = mc::GMachine( prog_int( 4, "x - 1" ) );
+ auto machine = gmachine( prog_int( 4, "x - 1" ) );
auto check = [&]( Expand s )
{
ASSERT( machine.hasher()._pool.size( s.from.snap ) );
@@ -117,7 +121,7 @@ namespace divine::t_mc
TEST( start_twice )
{
- auto machine = mc::TMachine( prog_int( 4, "x - 1" ) );
+ auto machine = tmachine( prog_int( 4, "x - 1" ) );
mc::State i1, i2;
mc::weave( machine ).observe( [&]( Expand e ) { i1 = e.from; } ).start();
@@ -130,7 +134,7 @@ namespace divine::t_mc
{
mc::State i1, i2;
- auto m1 = mc::TMachine( prog_int( 4, "x - 1" ) ), m2 = m1;
+ auto m1 = tmachine( prog_int( 4, "x - 1" ) ), m2 = m1;
mc::weave( m1 ).observe( [&]( Expand e ) { i1 = e.from; } ).start();
mc::weave( m2 ).observe( [&]( Expand e ) { i2 = e.from; } ).start();
@@ -141,7 +145,7 @@ namespace divine::t_mc
TEST( unfold )
{
std::vector< mc::Snapshot > snaps;
- auto machine = mc::TMachine( prog_int( 4, "x - 1" ) );
+ auto machine = tmachine( prog_int( 4, "x - 1" ) );
auto state = [&]( Expand e )
{
@@ -157,7 +161,8 @@ namespace divine::t_mc
template< typename M >
void _search( std::shared_ptr< mc::BitCode > bc, int sc, int ec )
{
- M machine( bc );
+ M machine;
+ machine.bc( bc );
int edgecount = 0, statecount = 0;
auto edge = [&]( Edge ) { ++edgecount; };
auto state = [&]( Expand ) { ++statecount; };