Commit 083c70d5 authored by phlo's avatar phlo

fixed final state update

parent 5cf89af2
......@@ -6,14 +6,23 @@
namespace ConcuBinE {
std::string Boolector::name () const { return "boolector"; }
//==============================================================================
// Boolector
//==============================================================================
//------------------------------------------------------------------------------
// member functions
//------------------------------------------------------------------------------
// Boolector::build_command ----------------------------------------------------
std::string Boolector::build_command ()
{
// return "boolector --model-gen --output-number-format=dec";
return "boolector --model-gen";
return "boolector --model-gen"; // --output-number-format=dec
}
// Boolector::parse_line -------------------------------------------------------
Boolector::Symbol Boolector::parse_line (std::istringstream & line)
{
std::string token;
......@@ -75,4 +84,8 @@ Boolector::Symbol Boolector::parse_line (std::istringstream & line)
return Symbol::ignore;
}
// Boolector::name -------------------------------------------------------------
std::string Boolector::name () const { return "boolector"; }
} // namespace ConcuBinE
......@@ -5,15 +5,21 @@
namespace ConcuBinE {
//==============================================================================
// Boolector class
//==============================================================================
class Boolector : public External
{
private: //---------------------------------------------------------------------
virtual std::string build_command ();
protected:
protected: //-------------------------------------------------------------------
virtual Symbol parse_line (std::istringstream & line);
public:
public: //----------------------------------------------------------------------
virtual std::string name () const;
};
......
......@@ -4,21 +4,41 @@
namespace ConcuBinE {
//==============================================================================
// BtorMC
//==============================================================================
//------------------------------------------------------------------------------
// constructors
//------------------------------------------------------------------------------
BtorMC::BtorMC(size_t b) : bound(b) {}
//------------------------------------------------------------------------------
// member functions
//------------------------------------------------------------------------------
// BtorMC::name ----------------------------------------------------------------
std::string BtorMC::name () const { return "btormc"; }
// BtorMC::build_command -------------------------------------------------------
std::string BtorMC::build_command ()
{
return "btormc --trace-gen-full -kmax " + std::to_string(bound);
}
// BtorMC::build_formula -------------------------------------------------------
std::string BtorMC::build_formula (Encoder & formula,
const std::string & constraints)
{
return formula.str() + (constraints.empty() ? "" : constraints + eol);
}
// BtorMC::parse_line ----------------------------------------------------------
BtorMC::Symbol BtorMC::parse_line (std::istringstream & line)
{
switch (line.peek())
......@@ -34,17 +54,19 @@ BtorMC::Symbol BtorMC::parse_line (std::istringstream & line)
}
}
BtorMC::Symbol BtorMC::parse_symbol (std::istringstream & line)
{
std::ostringstream os;
// BtorMC::parse_symbol --------------------------------------------------------
// cout << line.str() << eol;
// if (!getline(line >> ws, name, '_'))
// runtime_error("missing symbol");
inline
bool starts_with (const std::string & str, const std::string & prefix)
{
return str.find(prefix) != std::string::npos;
}
BtorMC::Symbol BtorMC::parse_symbol (std::istringstream & line)
{
line >> std::ws;
std::ostringstream os;
for (char c = line.get();
c != '@' && c != '#' && c != '_' && c != EOF;
c = line.get())
......@@ -52,32 +74,45 @@ BtorMC::Symbol BtorMC::parse_symbol (std::istringstream & line)
std::string name = os.str();
// cout << "BtorMC::parse_variable name = '" << name << '\'' << eol;
if (name.empty())
throw std::runtime_error("missing symbol");
if (name == Encoder::thread_sym)
if (name == Encoder::accu_sym)
{
thread = parse_symbol(line, "thread", '@');
step = parse_symbol(line, "step") + 1;
return Symbol::thread;
thread = parse_symbol(line, "thread", '#');
step = parse_symbol(line, "step");
return Symbol::accu;
}
else if (name == Encoder::stmt_sym)
else if (name == Encoder::mem_sym)
{
thread = parse_symbol(line, "thread");
pc = parse_symbol(line, "pc", '#');
step = parse_symbol(line, "step") + 1;
return Symbol::stmt;
thread = parse_symbol(line, "thread", '#');
step = parse_symbol(line, "step");
return Symbol::mem;
}
else if (name == Encoder::accu_sym)
else if (name == Encoder::sb_adr_sym)
{
thread = parse_symbol(line, "thread", '#');
step = parse_symbol(line, "step");
return Symbol::accu;
return Symbol::sb_adr;
}
else if (name == Encoder::mem_sym)
else if (name == Encoder::sb_val_sym)
{
thread = parse_symbol(line, "thread", '#');
step = parse_symbol(line, "step");
return Symbol::mem;
return Symbol::sb_val;
}
else if (name == Encoder::sb_full_sym)
{
thread = parse_symbol(line, "thread", '#');
step = parse_symbol(line, "step");
return Symbol::sb_full;
}
else if (name == Encoder::stmt_sym)
{
thread = parse_symbol(line, "thread");
pc = parse_symbol(line, "pc", '#');
step = parse_symbol(line, "step");
return Symbol::stmt;
}
else if (name == Encoder::heap_sym)
{
......@@ -94,22 +129,18 @@ BtorMC::Symbol BtorMC::parse_symbol (std::istringstream & line)
step = parse_symbol(line, "step", '#');
return Symbol::exit_code;
}
/*
cout << "symbol: ";
switch (symbol->type)
else if (name == Encoder::thread_sym)
{
thread = parse_symbol(line, "thread", '@');
step = parse_symbol(line, "step");
return Symbol::thread;
}
else if (name == Encoder::flush_sym)
{
case Symbol::Type::THREAD: cout << "THREAD"; break;
case Symbol::Type::EXEC: cout << "EXEC"; break;
case Symbol::Type::ACCU: cout << "ACCU"; break;
case Symbol::Type::MEM: cout << "MEM"; break;
case Symbol::Type::HEAP: cout << "HEAP"; break;
case Symbol::Type::EXIT: cout << "EXIT"; break;
case Symbol::Type::EXIT_CODE: cout << "EXIT_CODE"; break;
default: ;
thread = parse_symbol(line, "thread", '@');
step = parse_symbol(line, "step");
return Symbol::flush;
}
cout << " step = " << symbol->step << eol;
*/
return Symbol::ignore;
}
......
......@@ -5,23 +5,35 @@
namespace ConcuBinE {
struct BtorMC : Boolector
struct BtorMC : public Boolector
{
BtorMC (size_t);
//----------------------------------------------------------------------------
// members
//----------------------------------------------------------------------------
const size_t bound;
virtual std::string build_command ();
//----------------------------------------------------------------------------
// constructors
//----------------------------------------------------------------------------
BtorMC (size_t);
//----------------------------------------------------------------------------
// member functions
//----------------------------------------------------------------------------
virtual std::string name () const;
virtual std::string build_formula (Encoder &, const std::string &);
virtual Symbol parse_line (std::istringstream &);
virtual std::string build_command ();
using Boolector::parse_symbol;
virtual Symbol parse_symbol (std::istringstream &);
virtual std::string name () const;
virtual Symbol parse_line (std::istringstream &);
};
} // namespace ConcuBinE
......
......@@ -771,7 +771,7 @@ struct Encoder : public ConcuBinE::Encoder
//
// checkpoint id -> nid
//
nid_map nids_check;
std::map<word_t, std::string> nids_check;
// array read nodes
//
......
......@@ -192,16 +192,25 @@ void Simulator::flush ()
assert(sb_full());
assert(state[thread] == State::flushing);
sb_full(false);
state[thread] = State::running;
trace->push_back_flush(step - 1);
trace->push_back_heap(step, sb_adr(), sb_val());
// skip state updates during final step
if (step <= bound)
{
sb_full(false);
trace->push_back_heap(step, sb_adr(), sb_val());
}
}
// Simulator::execute ----------------------------------------------------------
void Simulator::execute ()
{
// skip state updates during final step
if (step > bound)
return;
const Program & program = (*programs)[thread];
const Instruction & op = program[pc()];
......@@ -401,11 +410,11 @@ Trace::ptr Simulator::run (std::function<void()> scheduler)
{
bool done = active.empty();
while (!done && ++step <= bound)
while (!done && step <= bound)
{
scheduler();
trace->push_back_thread(step - 1, thread);
trace->push_back_thread(step++, thread);
// flush store buffer or execute instruction
if (state[thread] == State::flushing)
......
......@@ -29,8 +29,11 @@ std::string Solver::build_formula (Encoder & formula,
bool External::sat (const std::string & input)
{
Shell shell;
std_out = shell.run(build_command(), input);
std::string sat;
return (std_out >> sat) && sat == "sat";
}
......@@ -38,7 +41,10 @@ bool External::sat (const std::string & input)
Trace::ptr External::solve (Encoder & formula, const std::string & constraints)
{
sat(build_formula(formula, constraints));
std::string input = build_formula(formula, constraints);
sat(input);
return build_trace(formula.programs);
}
......@@ -73,24 +79,29 @@ 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 && step == trace->length)
if (step > 1 && step == trace->length)
{
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(step - 2))
if (trace->flush(k))
{
address = trace->sb_adr(trace->thread());
address = trace->sb_adr(t);
assert(heap.find(address) != heap.end());
trace->push_back_heap(step - 1, address, heap[address]);
}
// atomic operation has been executed
// CAS has been executed
else if (op && op->type() & Instruction::Type::atomic)
{
address = op->indirect() ? heap[op->arg()] : op->arg();
trace->push_back_heap(step - 1, address, heap[address]);
}
if (trace->accu(k, t))
{
address = op->indirect() ? heap[op->arg()] : op->arg();
trace->push_back_heap(step - 1, address, heap[address]);
}
op = &(*programs)[thread][trace->pc(thread)];
// TODO: get correct thread, pc and accu for step - 2
op = &(*programs)[t][trace->pc(t)];
// reset heap map for the next step
heap = {};
......@@ -209,17 +220,26 @@ External::Symbol External::parse_symbol (std::istringstream & line)
thread = parse_symbol(line, "thread");
return Symbol::sb_full;
}
else if (name == Encoder::stmt_sym)
{
step = parse_symbol(line, "step");
thread = parse_symbol(line, "thread");
pc = parse_symbol(line, "pc");
return Symbol::stmt;
}
else if (name == Encoder::heap_sym)
{
step = parse_symbol(line, "step");
return Symbol::heap;
}
else if (name == Encoder::stmt_sym)
else if (name == Encoder::exit_flag_sym)
{
step = parse_symbol(line, "step");
thread = parse_symbol(line, "thread");
pc = parse_symbol(line, "pc");
return Symbol::stmt;
return Symbol::exit_flag; // TODO
}
else if (name == Encoder::exit_code_sym)
{
return Symbol::exit_code;
}
else if (name == Encoder::thread_sym)
{
......@@ -233,15 +253,6 @@ External::Symbol External::parse_symbol (std::istringstream & line)
thread = parse_symbol(line, "thread");
return Symbol::flush;
}
else if (name == Encoder::exit_flag_sym)
{
step = parse_symbol(line, "step");
return Symbol::exit_flag; // TODO
}
else if (name == Encoder::exit_code_sym)
{
return Symbol::exit_code;
}
return Symbol::ignore;
}
......
......@@ -52,16 +52,16 @@ GTEST_FILTER = --gtest_filter=
# GTEST_FILTER += smtlib_Relational.*
# GTEST_FILTER += btor2.*
# GTEST_FILTER += btor2_Encoder.*
# GTEST_FILTER += Simulator.*
GTEST_FILTER += Simulator.*
# GTEST_FILTER += Main.*
# GTEST_FILTER += Experimental.*
# GTEST_FILTER += Instruction.*
# GTEST_FILTER += Program.*
# GTEST_FILTER += Trace.*
GTEST_FILTER += Trace.*
# GTEST_FILTER += MMap.*
# GTEST_FILTER += Shell.*
GTEST_FILTER += Boolector.*
# GTEST_FILTER += BtorMC.*
GTEST_FILTER += BtorMC.*
# GTEST_FILTER += Z3.*
# GTEST_FILTER += CVC4.*
......
......@@ -18,4 +18,4 @@ data/increment.check.thread.n.asm
0 7 FLUSH - 1 0 0 1 1 {} # 13
0 7 JNZ 1 1 0 0 1 0 {(0,1)} # 14
0 1 FENCE - 1 0 0 1 0 {} # 15
0 2 CHECK 0 1 0 0 1 0 {} # 16
1 5 FLUSH - 1 0 0 1 1 {} # 16
......@@ -89,19 +89,6 @@ TEST_F(Boolector, solve_cas)
ASSERT_EQ(*replay, *trace);
}
TEST_F(Boolector, DISABLED_encode_deadlock)
{
// deadlock after 3 steps -> unsat
programs->push_back(create_from_file<Program>("data/deadlock.thread.0.asm"));
programs->push_back(create_from_file<Program>("data/deadlock.thread.1.asm"));
encoder = std::make_unique<smtlib::Functional>(programs, 3);
std::string formula = encoder->str();
ASSERT_FALSE(boolector.sat(formula));
}
// TODO: remove
TEST_F(Boolector, print_model_check)
{
......
......@@ -47,7 +47,7 @@ TEST_F(BtorMC, unsat)
ASSERT_EQ("", btormc.std_out.str());
}
TEST_F(BtorMC, DISABLED_solve_check)
TEST_F(BtorMC, solve_check)
{
// concurrent increment using CHECK
std::string constraints;
......@@ -63,109 +63,18 @@ TEST_F(BtorMC, DISABLED_solve_check)
trace = btormc.solve(*encoder, constraints);
/*
std::cout << "scheduled threads" << eol;
for (const auto & [step, thread] : trace->thread_updates)
{
std::cout << "\t{" << step << ", " << thread << "}" << eol;
}
std::cout << "pc updates" << eol;
unsigned long thread = 0;
for (const auto & updates : trace->pc_updates)
{
for (const auto & [step, val] : updates)
{
std::cout << "\t" << thread << ": {" << step << ", " << val << "}" << eol;
}
thread++;
}
std::cout << "accu updates" << eol;
thread = 0;
for (const auto & updates : trace->accu_updates)
{
for (const auto & [step, val] : updates)
{
std::cout << "\t" << thread << ": {" << step << ", " << val << "}" << eol;
}
thread++;
}
std::cout << "heap updates" << eol;
for (const auto & updates : trace->heap_updates)
for (const auto & [idx, val] : updates.second)
{
std::cout << "\t{" << idx << ", " << val << "}" << eol;
}
*/
ASSERT_EQ(
"data/increment.check.thread.0.asm\n"
"data/increment.check.thread.n.asm\n"
".\n"
"# tid pc cmd arg accu mem heap\n"
"0 0 STORE 0 0 0 {(0,0)}\n"
"1 0 CHECK 0 0 0 {}\n"
"0 2 LOAD 0 0 0 {}\n"
"0 3 ADDI 1 1 0 {}\n"
"0 4 STORE 0 1 0 {(0,1)}\n"
"1 1 CHECK 1 0 0 {}\n"
"1 2 LOAD 0 1 0 {}\n"
"1 3 ADDI 1 2 0 {}\n"
"0 6 JNZ 1 1 0 {}\n"
"1 4 STORE 0 2 0 {(0,2)}\n"
"1 5 JNZ 0 2 0 {}\n"
"1 0 CHECK 0 2 0 {}\n"
"0 2 LOAD 0 2 0 {}\n"
"0 3 ADDI 1 3 0 {}\n"
"0 4 STORE 0 3 0 {(0,3)}\n"
"1 1 CHECK 1 2 0 {}\n"
"1 2 LOAD 0 2 0 {}\n",
trace->print());
std::ofstream file {"/tmp/test.trace"};
file << trace->print();
file.close();
Trace::ptr parsed =
std::make_unique<Trace>(create_from_file<Trace>("/tmp/test.trace"));
std::vector<std::vector<std::pair<size_t, word_t>>> pc_diff;
for (size_t t = 0; t < trace->pc_updates.size(); t++)
{
std::vector<std::pair<size_t, word_t>> diff;
std::set_symmetric_difference(
trace->pc_updates[t].begin(), trace->pc_updates[t].end(),
parsed->pc_updates[t].begin(), parsed->pc_updates[t].end(),
std::back_inserter(diff));
pc_diff.push_back(diff);
}
std::cout << "pc diff" << eol;
word_t thread = 0;
for (const auto & updates : pc_diff)
{
for (const auto & [step, val] : updates)
std::cout
<< "\t" << thread << ": {" << step << ", " << val << "}"
<< eol;
thread++;
}
ASSERT_EQ(*parsed, *trace);
// std::cout << trace->print();
Simulator simulator {programs};
Trace::ptr simulated {simulator.replay(*parsed)};
Trace::ptr replay {simulator.replay(*trace)};
// std::cout << replay->print();
ASSERT_EQ(*simulated, *trace);
ASSERT_EQ(*replay, *trace);
}
TEST_F(BtorMC, DISABLED_solve_cas)
TEST_F(BtorMC, solve_cas)
{
// concurrent increment using CAS
std::string constraints;
......@@ -180,29 +89,15 @@ TEST_F(BtorMC, DISABLED_solve_cas)
trace = btormc.solve(*encoder, constraints);
ASSERT_EQ(
"",
// "data/increment.cas.asm\n"
// "data/increment.cas.asm\n"
// ".\n"
// "# tid pc cmd arg accu mem heap\n"
// "0 0 STORE 0 0 0 {(0,0)}\n"
// "1 0 STORE 0 0 0 {}\n"
// "1 1 CHECK 0 0 0 {}\n"
// "0 LOOP MEM 0 0 0 {}\n"
// "1 LOOP MEM 0 0 0 {}\n"
// "0 3 ADDI 1 1 0 {}\n"
// "0 4 CAS 0 1 0 {(0,1)}\n"
// "1 3 ADDI 1 1 0 {}\n"
// "1 4 CAS 0 0 0 {}\n"
// "0 5 JMP LOOP 1 0 {}\n"
// "1 5 JMP LOOP 0 0 {}\n"
// "0 LOOP MEM 0 1 1 {}\n"
// "0 3 ADDI 1 2 1 {}\n"
// "0 4 CAS 0 1 1 {(0,2)}\n"
// "1 LOOP MEM 0 2 2 {}\n"
// "1 3 ADDI 1 3 2 {}\n",
trace->print());
// std::cout << trace->print();
Simulator simulator {programs};
Trace::ptr replay {simulator.replay(*trace)};
// std::cout << replay->print();
ASSERT_EQ(*replay, *trace);
}
// TODO: remove
......@@ -217,14 +112,14 @@ TEST_F(BtorMC, print_model_check)
programs->push_back(create_from_file<Program>(increment_0));
programs->push_back(create_from_file<Program>(increment_n));
encoder = std::make_unique<btor2::Encoder>(programs, 12);
encoder = std::make_unique<btor2::Encoder>(programs, 16);
std::string formula = btormc.build_formula(*encoder, "");
bool sat = btormc.sat(formula);
std::ofstream outfile("/tmp/btormc.check.out");
outfile << btormc.std_out.str();
std::ofstream trace_file("/tmp/btormc.check.out");
trace_file << btormc.std_out.str();
ASSERT_TRUE(sat);
}
......@@ -239,14 +134,14 @@ TEST_F(BtorMC, print_model_cas)
programs->push_back(create_from_file<Program>(increment_cas));
programs->push_back(create_from_file<Program>(increment_cas));
encoder = std::make_unique<btor2::Encoder>(programs, 12);
encoder = std::make_unique<btor2::Encoder>(programs, 16);
std::string formula = btormc.build_formula(*encoder, "");
bool sat = btormc.sat(formula);
std::ofstream outfile("/tmp/btormc.cas.out");
outfile << btormc.std_out.str();
std::ofstream trace_file("/tmp/btormc.cas.out");
trace_file << btormc.std_out.str();
ASSERT_TRUE(sat);
}
......
This diff is collapsed.
......@@ -62,7 +62,8 @@ TEST_F(Trace, parse_check)
{6, 1},
{7, 0},
{10, 1},
{13, 0}}),
{13, 0},
{16, 1}}),
trace->thread_updates);
ASSERT_EQ(
......@@ -75,8 +76,7 @@ TEST_F(Trace, parse_check)
{8, 5},
{9, 6},
{13, 7},
{15, 1},
{16, 2}}),
{15, 1}}),
trace->pc_updates[0]);
ASSERT_EQ(
update_map<word_t>({
......@@ -84,7 +84,8 @@ TEST_F(Trace, parse_check)
{6, 1},
{10, 2},
{11, 3},
{12, 4}}),
{12, 4},
{16, 5}}),
trace->pc_updates[1]);
ASSERT_EQ(
......@@ -110,16 +111,16 @@ TEST_F(Trace, parse_check)
ASSERT_EQ(
thread_map<word_t>({
{{0, 0}, {9, 1}},
{{1, 0}}}),
{{1, 0}, {16, 1}}}),
trace->sb_val_updates);
ASSERT_EQ(
thread_map<bool>({
{{0, false}, {2, true}, {3, false}, {9, true}, {14, false}},
{{1, false}}}),
{{1, false}, {16, true}}}),
trace->sb_full_updates);
ASSERT_EQ(std::unordered_set<size_t>({2, 13}), trace->flushes);
ASSERT_EQ(std::unordered_set<size_t>({2, 13, 16}), trace->flushes);
ASSERT_EQ(
update_map<word_t>({
......@@ -1035,6 +1036,17 @@ TEST_F(Trace, thread)
}
}
TEST_F(Trace, thread_k)
{
create_dummy_trace(2);
for (const auto & [step, thread, _, __] : data)
trace->push_back_thread(step, thread);
for (const auto & [step, thread, _, __] : data)
ASSERT_EQ(thread, trace->thread(step));
}
// Trace::pc ===================================================================
TEST_F(Trace, pc)
......@@ -1048,6 +1060,17 @@ TEST_F(Trace, pc)
}
}
TEST_F(Trace, pc_k)
{
create_dummy_trace(2);
for (const auto & [step, thread, pc, _] : data)
trace->push_back_pc(step, thread, pc);
for (const auto & [step, thread, pc, _] : data)
ASSERT_EQ(pc, trace->pc(step, thread));
}
// Trace::accu =================================================================
TEST_F(Trace, accu)
......@@ -1061,6 +1084,17 @@ TEST_F(Trace, accu)
}