Commit 7e78076d authored by phlo's avatar phlo

fixed cutting off traces upon exit

parent 7ceaa039
......@@ -55,10 +55,9 @@ Trace::ptr External::solve (Encoder & formula, const std::string & constraints)
Trace::ptr External::build_trace (const Program::List::ptr & programs)
{
Trace::ptr trace = std::make_unique<Trace>(programs);
// current line number
size_t lineno = 2;
size_t next = 2;
Trace::ptr trace = std::make_unique<Trace>(programs);
for (std::string line_buf; getline(std_out, line_buf); lineno++)
{
......@@ -77,9 +76,9 @@ Trace::ptr External::build_trace (const Program::List::ptr & programs)
// detect an eventual heap update
// reached next step: previous state at step - 1 fully visible
if (step > 1 && step == trace->length)
if (step > 1 && step == next)
{
const size_t k = step - 2;
const size_t k = next++ - 2;
const word_t t = trace->thread(k);
// instruction responsible for state at step - 1
......@@ -116,49 +115,46 @@ Trace::ptr External::build_trace (const Program::List::ptr & programs)
heap.clear();
}
switch (symbol)
if (symbol == Symbol::accu)
{
case Symbol::accu:
trace->push_back_accu(step, thread, value);
break;
case Symbol::mem:
}
else if (symbol == Symbol::mem)
{
trace->push_back_mem(step, thread, value);
break;
case Symbol::sb_adr:
}
else if (symbol == Symbol::sb_adr)
{
trace->push_back_sb_adr(step, thread, value);
break;
case Symbol::sb_val:
}
else if (symbol == Symbol::sb_val)
{
trace->push_back_sb_val(step, thread, value);
break;
case Symbol::sb_full:
}
else if (symbol == Symbol::sb_full)
{
trace->push_back_sb_full(step, thread, value);
break;
case Symbol::thread:
trace->push_back_thread(step, thread);
break;
case Symbol::stmt:
}
else if (symbol == Symbol::stmt)
{
trace->push_back_pc(step, thread, pc);
}
else if (symbol == Symbol::exit_flag)
{
break;
case Symbol::flush:
}
else if (symbol == Symbol::exit_code)
{
trace->exit = value;
}
else if (symbol == Symbol::thread)
{
trace->push_back_thread(step, thread);
}
else if (symbol == Symbol::flush)
{
trace->push_back_thread(step, thread);
trace->push_back_flush(step);
break;
case Symbol::exit_flag:
break;
case Symbol::exit_code:
trace->exit = value;
break;
default: break;
}
}
catch (const std::exception & e)
......
......@@ -102,7 +102,7 @@ TEST_F(Boolector, solve_indirect_uninitialized)
programs->push_back(Program(p0, "load.store.0.asm"));
programs->push_back(Program(p1, "load.store.1.asm"));
encoder = std::make_unique<smtlib::Functional>(programs, 9);
encoder = std::make_unique<smtlib::Functional>(programs, 16);
trace = boolector.solve(*encoder);
......
......@@ -114,7 +114,7 @@ TEST_F(BtorMC, solve_indirect_uninitialized)
programs->push_back(Program(p0, "load.store.0.asm"));
programs->push_back(Program(p1, "load.store.1.asm"));
encoder = std::make_unique<btor2::Encoder>(programs, 9);
encoder = std::make_unique<btor2::Encoder>(programs, 16);
trace = btormc.solve(*encoder);
......
......@@ -133,7 +133,7 @@ TEST_F(CVC4, solve_indirect_uninitialized)
programs->push_back(Program(p0, "load.store.0.asm"));
programs->push_back(Program(p1, "load.store.1.asm"));
encoder = std::make_unique<smtlib::Functional>(programs, 9);
encoder = std::make_unique<smtlib::Functional>(programs, 16);
trace = cvc4.solve(*encoder);
......
......@@ -102,7 +102,7 @@ TEST_F(Z3, solve_indirect_uninitialized)
programs->push_back(Program(p0, "load.store.0.asm"));
programs->push_back(Program(p1, "load.store.1.asm"));
encoder = std::make_unique<smtlib::Functional>(programs, 9);
encoder = std::make_unique<smtlib::Functional>(programs, 16);
trace = z3.solve(*encoder);
......
......@@ -352,28 +352,34 @@ void Trace::init_heap (const word_t address, const word_t value)
// Trace::push_back ------------------------------------------------------------
template <typename T>
void Trace::push_back (Trace::update_map<T> & updates,
template <class T>
bool Trace::push_back (Trace::update_map<T> & updates,
const size_t step,
const T val)
const T value)
{
if (updates.empty())
{
updates.insert({step, val});
updates[step] = value;
return true;
}
else
{
auto end = updates.end();
auto prev = std::prev(end);
auto end = updates.cend();
auto prev = updates.crbegin();
// ensure that no update exists for this step
if (prev->first == step)
throw std::runtime_error("update already exists");
// insert if value doesn't change
if (prev->second != val)
updates.insert(end, {step, val});
if (prev->second != value)
{
updates.emplace_hint(end, step, value);
return true;
}
}
return false;
}
void Trace::push_back (const word_t thread,
......@@ -413,40 +419,32 @@ void Trace::push_back (const word_t thread,
void Trace::push_back_thread (size_t step, const word_t thread)
{
push_back<word_t>(thread_updates, step, thread);
if (++step > length)
length = step;
if (push_back<word_t>(thread_updates, step, thread) && step >= length)
length = ++step;
}
// Trace::push_back_pc ---------------------------------------------------------
void Trace::push_back_pc (size_t step, const word_t thread, const word_t pc)
{
push_back<word_t>(pc_updates.at(thread), step, pc);
if (++step > length)
length = step;
if (push_back<word_t>(pc_updates[thread], step, pc) && step >= length)
length = ++step;
}
// Trace::push_back_accu -------------------------------------------------------
void Trace::push_back_accu (size_t step, const word_t thread, const word_t accu)
{
push_back<word_t>(accu_updates.at(thread), step, accu);
if (++step > length)
length = step;
if (push_back<word_t>(accu_updates[thread], step, accu) && step >= length)
length = ++step;
}
// Trace::push_back_mem --------------------------------------------------------
void Trace::push_back_mem (size_t step, const word_t thread, const word_t mem)
{
push_back<word_t>(mem_updates.at(thread), step, mem);
if (++step > length)
length = step;
if (push_back<word_t>(mem_updates[thread], step, mem) && step >= length)
length = ++step;
}
// Trace::push_back_sb_adr -----------------------------------------------------
......@@ -455,10 +453,8 @@ void Trace::push_back_sb_adr (size_t step,
const word_t thread,
const word_t adr)
{
push_back<word_t>(sb_adr_updates.at(thread), step, adr);
if (++step > length)
length = step;
if (push_back<word_t>(sb_adr_updates[thread], step, adr) && step >= length)
length = ++step;
}
// Trace::push_back_sb_val -----------------------------------------------------
......@@ -467,10 +463,8 @@ void Trace::push_back_sb_val (size_t step,
const word_t thread,
const word_t val)
{
push_back<word_t>(sb_val_updates.at(thread), step, val);
if (++step > length)
length = step;
if (push_back<word_t>(sb_val_updates[thread], step, val) && step >= length)
length = ++step;
}
// Trace::push_back_sb_full ----------------------------------------------------
......@@ -479,10 +473,8 @@ void Trace::push_back_sb_full (size_t step,
const word_t thread,
const bool full)
{
push_back<bool>(sb_full_updates.at(thread), step, full);
if (++step > length)
length = step;
if (push_back<bool>(sb_full_updates[thread], step, full) && step >= length)
length = ++step;
}
// Trace::push_back_heap -------------------------------------------------------
......@@ -492,8 +484,8 @@ void Trace::push_back_heap (size_t step, const word_t adr, const word_t val)
heap_adr_updates.emplace_hint(heap_adr_updates.end(), step, adr);
push_back<word_t>(heap_val_updates[adr], step, val);
if (++step > length)
length = step;
if (step >= length)
length = ++step;
}
// Trace::push_back_flush ------------------------------------------------------
......@@ -502,8 +494,8 @@ void Trace::push_back_flush (size_t step)
{
flushes.insert(step);
if (++step > length)
length = step;
if (step >= length)
length = ++step;
}
// Trace::thread ---------------------------------------------------------------
......
......@@ -259,8 +259,8 @@ struct Trace
// append state update helper
//
template <typename T>
void push_back (update_map<T> & updates, const size_t step, const T val);
template <class T>
bool push_back (update_map<T> & updates, size_t step, T value);
// append state update after executing an instruction
//
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment