Commit 7ceaa039 authored by phlo's avatar phlo

added detection of uninitialized reads to solvers

parent 3f37c3c5
......@@ -57,9 +57,6 @@ Trace::ptr External::build_trace (const Program::List::ptr & programs)
{
Trace::ptr trace = std::make_unique<Trace>(programs);
// instruction at step - 2, leading to the previous step's state update
const Instruction * op = nullptr;
// current line number
size_t lineno = 2;
......@@ -75,82 +72,93 @@ Trace::ptr External::build_trace (const Program::List::ptr & programs)
std::istringstream line(line_buf);
Symbol symbol = parse_line(line);
if (symbol != Symbol::ignore)
if (symbol == Symbol::ignore)
continue;
// detect an eventual heap update
// reached next step: previous state at step - 1 fully visible
if (step > 1 && step == trace->length)
{
// detect an eventual heap update
// reached next step: previous state at step - 1 fully visible
if (step > 1 && step == trace->length)
const size_t k = step - 2;
const word_t t = trace->thread(k);
// instruction responsible for state at step - 1
const Instruction & op = (*programs)[t][trace->pc(k, t)];
// store buffer has been flushed
// NOTE: heap update visible one step after flush is set
if (trace->flush(k))
{
const size_t k = step - 2;
const word_t t = trace->thread(k);
// store buffer has been flushed
// NOTE: heap update visible one step after flush is set
if (trace->flush(k))
{
word_t address = trace->sb_adr(t);
trace->push_back_heap(step - 1, address, heap[address]);
}
// CAS has been executed
else if (op && op->type() & Instruction::Type::atomic)
if (trace->accu(k, t))
{
word_t address = op->indirect() ? heap[op->arg()] : op->arg();
trace->push_back_heap(step - 1, address, heap[address]);
}
// instruction executed at step - 2
op = &(*programs)[t][trace->pc(t)];
// reset heap map for the next step
// NOTE: really necessary?
heap.clear();
const word_t adr = trace->sb_adr(t);
trace->push_back_heap(step - 1, adr, heap[adr]);
}
// CAS has been executed
else if (op.type() & Instruction::Type::atomic && trace->accu(t))
{
const word_t adr = op.indirect() ? heap[op.arg()] : op.arg();
trace->push_back_heap(step - 1, adr, heap[adr]);
}
switch (symbol)
// detect uninitialized reads
if (op.type() & Instruction::Type::read)
{
case Symbol::accu:
trace->push_back_accu(step, thread, value);
break;
word_t adr = op.arg();
if (!trace->heap(adr))
trace->init_heap(adr, heap[adr]);
case Symbol::mem:
trace->push_back_mem(step, thread, value);
break;
if (op.indirect() && !trace->heap(adr = heap[adr]))
trace->init_heap(adr, heap[adr]);
}
case Symbol::sb_adr:
trace->push_back_sb_adr(step, thread, value);
break;
// reset heap map for the next step
// NOTE: really necessary?
heap.clear();
}
case Symbol::sb_val:
trace->push_back_sb_val(step, thread, value);
break;
switch (symbol)
{
case Symbol::accu:
trace->push_back_accu(step, thread, value);
break;
case Symbol::sb_full:
trace->push_back_sb_full(step, thread, value);
break;
case Symbol::mem:
trace->push_back_mem(step, thread, value);
break;
case Symbol::thread:
trace->push_back_thread(step, thread);
break;
case Symbol::sb_adr:
trace->push_back_sb_adr(step, thread, value);
break;
case Symbol::stmt:
trace->push_back_pc(step, thread, pc);
break;
case Symbol::sb_val:
trace->push_back_sb_val(step, thread, value);
break;
case Symbol::flush:
trace->push_back_thread(step, thread);
trace->push_back_flush(step);
break;
case Symbol::sb_full:
trace->push_back_sb_full(step, thread, value);
break;
case Symbol::exit_flag:
break;
case Symbol::thread:
trace->push_back_thread(step, thread);
break;
case Symbol::exit_code:
trace->exit = value;
break;
case Symbol::stmt:
trace->push_back_pc(step, thread, pc);
break;
default: break;
}
case 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)
......
......@@ -86,6 +86,39 @@ TEST_F(Boolector, solve_cas)
ASSERT_EQ(*replay, *trace);
}
TEST_F(Boolector, solve_indirect_uninitialized)
{
std::istringstream p0 (
"LOAD [0]\n"
"ADDI 1\n"
"STORE [0]\n"
"HALT\n");
std::istringstream p1 (
"LOAD [1]\n"
"ADDI 1\n"
"STORE [1]\n"
"HALT\n");
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);
trace = boolector.solve(*encoder);
std::cout << "time to solve = " << boolector.time << " ms" << eol;
std::cout << trace->print();
Simulator simulator (programs);
Trace::ptr replay (simulator.replay(*trace));
std::cout << replay->print();
ASSERT_EQ(*replay, *trace);
}
// TODO: remove
TEST_F(Boolector, print_model_check)
{
......
......@@ -98,6 +98,39 @@ TEST_F(BtorMC, solve_cas)
ASSERT_EQ(*replay, *trace);
}
TEST_F(BtorMC, solve_indirect_uninitialized)
{
std::istringstream p0 (
"LOAD [0]\n"
"ADDI 1\n"
"STORE [0]\n"
"HALT\n");
std::istringstream p1 (
"LOAD [1]\n"
"ADDI 1\n"
"STORE [1]\n"
"HALT\n");
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);
trace = btormc.solve(*encoder);
std::cout << "time to solve = " << btormc.time << " ms" << eol;
std::cout << trace->print();
Simulator simulator (programs);
Trace::ptr replay (simulator.replay(*trace));
std::cout << replay->print();
ASSERT_EQ(*replay, *trace);
}
// TODO: remove
TEST_F(BtorMC, print_model_check)
{
......
......@@ -117,7 +117,7 @@ TEST_F(CVC4, DISABLED_solve_multiple_addresses)
ASSERT_EQ(*replay, *trace);
}
TEST_F(CVC4, DISABLED_solve_indirect_uninitialized)
TEST_F(CVC4, solve_indirect_uninitialized)
{
std::istringstream p0 (
"LOAD [0]\n"
......@@ -133,7 +133,7 @@ TEST_F(CVC4, DISABLED_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, 16);
encoder = std::make_unique<smtlib::Functional>(programs, 9);
trace = cvc4.solve(*encoder);
......
......@@ -86,4 +86,37 @@ TEST_F(Z3, solve_cas)
ASSERT_EQ(*replay, *trace);
}
TEST_F(Z3, solve_indirect_uninitialized)
{
std::istringstream p0 (
"LOAD [0]\n"
"ADDI 1\n"
"STORE [0]\n"
"HALT\n");
std::istringstream p1 (
"LOAD [1]\n"
"ADDI 1\n"
"STORE [1]\n"
"HALT\n");
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);
trace = z3.solve(*encoder);
std::cout << "time to solve = " << z3.time << " ms" << eol;
std::cout << trace->print();
Simulator simulator (programs);
Trace::ptr replay (simulator.replay(*trace));
std::cout << replay->print();
ASSERT_EQ(*replay, *trace);
}
} // namespace ConcuBinE::test
......@@ -89,14 +89,18 @@ Trace::ptr Z3::solve (Encoder & encoder, const std::string & constraints)
time = duration_cast<milliseconds>(high_resolution_clock::now() - t).count();
Trace::ptr trace = std::make_unique<Trace>(encoder.programs);
const Program::List::ptr & programs = encoder.programs;
Trace::ptr trace = std::make_unique<Trace>(programs);
for (size_t step = 0; step <= encoder.bound; step++)
{
// heap state
if (step)
{
word_t thread = trace->thread();
const word_t thread = trace->thread();
const Instruction & op = (*programs)[thread][trace->pc(thread)];
const std::string heap = smtlib::Encoder::heap_var(step);
if (trace->flush(step - 1))
{
......@@ -105,30 +109,34 @@ Trace::ptr Z3::solve (Encoder & encoder, const std::string & constraints)
trace->sb_adr(thread),
trace->sb_val(thread));
}
else
else if (op.type() & Instruction::Type::atomic && trace->accu(thread))
{
const Instruction & op =
(*encoder.programs)[thread][trace->pc(thread)];
if (op.type() & Instruction::Type::atomic && trace->accu(thread))
{
std::string sym = smtlib::Encoder::heap_var(step);
word_t address =
op.indirect()
? eval_array(c, m, sym, op.arg())
: op.arg();
trace->push_back_heap(
step,
address,
eval_array(c, m, sym, address));
}
const word_t adr =
op.indirect()
? eval_array(c, m, heap, op.arg())
: op.arg();
trace->push_back_heap(
step,
adr,
eval_array(c, m, heap, adr));
}
if (op.type() & Instruction::Type::read)
{
word_t adr = op.arg();
if (!trace->heap(adr))
trace->init_heap(adr, eval_array(c, m, heap, adr));
if (op.indirect())
if (!trace->heap(adr = eval_array(c, m, heap, adr)))
trace->init_heap(adr, eval_array(c, m, heap, adr));
}
}
// thread states
for (word_t thread = 0; thread < encoder.programs->size(); thread++)
for (word_t thread = 0; thread < programs->size(); thread++)
{
if (eval_bool(c, m, smtlib::Encoder::thread_var(step, thread)))
{
......@@ -161,7 +169,7 @@ Trace::ptr Z3::solve (Encoder & encoder, const std::string & constraints)
thread,
eval_bool(c, m, smtlib::Encoder::sb_full_var(step, thread)));
const Program & program = (*encoder.programs)[thread];
const Program & program = (*programs)[thread];
for (word_t pc = 0; pc < program.size(); pc++)
if (eval_bool(c, m, smtlib::Encoder::stmt_var(step, thread, pc)))
......
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