From d200d8441444d4008592cc1c7fc3ee0c20c0e8bb Mon Sep 17 00:00:00 2001
From: Petr Rockai <me@mornfall.net>
Date: Tue, 30 Jul 2019 13:35:12 +0000
Subject: [PATCH] MC: Re-implement 'divine exec' in terms of mc::machine.
---
divine/mc/exec.cpp | 49 +++++++++++++++++++++++++---------------------
1 file changed, 27 insertions(+), 22 deletions(-)
diff --git a/divine/mc/exec.cpp b/divine/mc/exec.cpp
index 19acba9e7..608f39239 100644
--- a/divine/mc/exec.cpp
+++ b/divine/mc/exec.cpp
@@ -16,44 +16,49 @@
* OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
*/
+#include <divine/mc/ctx-assume.hpp>
#include <divine/mc/exec.hpp>
+#include <divine/mc/search.hpp>
#include <divine/mc/bitcode.hpp>
+#include <divine/mc/machine.hpp>
+#include <divine/mc/weaver.hpp>
+
#include <divine/vm/eval.hpp>
#include <divine/vm/setup.hpp>
#include <divine/vm/eval.tpp>
-#include <divine/vm/ctx-debug.tpp>
#include <divine/dbg/stepper.tpp>
#include <divine/dbg/print.tpp>
namespace divine::mc
{
-
- void Exec::run()
+ template< typename next >
+ struct print_trace : next
{
- using Eval = vm::Eval< ExecContext >;
- auto &program = _bc->program();
- ExecContext _ctx;
- _ctx.program( program );
- Eval eval( _ctx );
+ using next::trace;
+ void trace( std::string s ) { std::cout << s << std::endl; }
+ };
- vm::setup::boot( _ctx );
- _ctx.enable_debug();
- eval.run();
- if ( !_ctx.flags_any( _VM_CF_Cancel | _VM_CF_Error ) )
- ASSERT( !_ctx.state_ptr().null() );
+ namespace ctx = vm::ctx;
+ struct ctx_exec : brq::compose_stack< ctx_assume, ctx_choice, brq::module< print_trace >,
+ ctx::with_debug, ctx::with_tracking,
+ ctx::common< vm::Program, vm::CowHeap > > {};
- while ( !_ctx.flags_any( _VM_CF_Cancel | _VM_CF_Error ) )
- {
- vm::setup::scheduler( _ctx );
- eval.run();
- }
+ struct mach_exec : brq::compose_stack< machine::graph_dispatch,
+ machine::compute,
+ machine::tree_search,
+ machine::choose_random, machine::choose,
+ machine::with_context< ctx_exec >,
+ machine::base< smt::NoSolver > > {};
- if ( _ctx.flags_any( _VM_CF_Cancel ) )
- std::cerr << "encountered an infeasible path (execution cancelled)" << std::endl;
+ struct search : mc::Search< mc::State, mc::Label > {};
- if ( _ctx.flags_any( _VM_CF_Error ) )
- std::cerr << "execution stopped due to a program error" << std::endl;
+ void Exec::run()
+ {
+ mach_exec m;
+ m.bc( _bc );
+ m.context().enable_debug();
+ weave( m ).extend( search() ).start();
}
void Exec::trace()
--
GitLab