MC: Refactor machine::{Tree,Graph} into component stacks.

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 )

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; };