From 71915398498a1a2bc824e161548a357ca95bc42a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Luk=C3=A1=C5=A1=20Koren=C4=8Dik?= <xkorenc1@fi.muni.cz>
Date: Mon, 20 Jan 2020 21:34:59 +0000
Subject: [PATCH] ra: Add method that returns stack trace of counter-example.
---
divine/ra/llvmrefine.hpp | 43 ++++++++++++++++++++++++++++++++++++++++
1 file changed, 43 insertions(+)
diff --git a/divine/ra/llvmrefine.hpp b/divine/ra/llvmrefine.hpp
index 8762d3828..320a7f5a3 100644
--- a/divine/ra/llvmrefine.hpp
+++ b/divine/ra/llvmrefine.hpp
@@ -40,6 +40,8 @@ namespace divine::ra {
struct get_ce_t_
{
+ using stack_trace_t = std::vector< llvm::Instruction * >;
+
template< typename Ctx >
void static create_ctx( Ctx &dbg_ctx, mc::Job &job)
{
@@ -66,6 +68,47 @@ struct get_ce_t_
return std::move( dbg_ctx );
}
+
+ static stack_trace_t stack_trace( mc::Job &job, mc::BitCode *bc )
+ {
+ dbg::Info info( *bc->_program, *bc->_module );
+ dbg::Context< vm::CowHeap > dbg_ctx( bc->program(), bc->debug() );
+ create_ctx( dbg_ctx, job );
+ return stack_trace( dbg_ctx, info );
+ }
+
+
+ template< typename dbg_ctx_t >
+ static stack_trace_t stack_trace( dbg_ctx_t &dbg_ctx, dbg::Info &info )
+ {
+ stack_trace_t out;
+ auto &heap = dbg_ctx.heap();
+
+ vm::PointerV current_pc;
+ vm::PointerV current_parent;
+
+ vm::PointerV iter_frame( dbg_ctx.frame() );
+
+ while ( !iter_frame.cooked().null() )
+ {
+ heap.read_shift( iter_frame, current_pc );
+ auto [ inst, pc ] = info.find( nullptr, current_pc.cooked() );
+ out.push_back( inst );
+ heap.read_shift( iter_frame, current_parent );
+ iter_frame = current_parent;
+ }
+ return out;
+ }
+
+ 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;
+ }
};
template< typename refiner_t >
--
GitLab