Commit 5cf89af2 authored by phlo's avatar phlo

updated generating traces from solver output

parent 31bcd97b
......@@ -14,16 +14,13 @@ std::string Boolector::build_command ()
return "boolector --model-gen";
}
std::optional<Boolector::Variable>
Boolector::parse_line (std::istringstream & line)
Boolector::Symbol Boolector::parse_line (std::istringstream & line)
{
std::string token;
// parse node id
uint64_t nid;
word_t adr = 0, val = 0;
// parse node id
if (!(line >> nid))
{
line >> token;
......@@ -34,17 +31,14 @@ Boolector::parse_line (std::istringstream & line)
if (!(line >> token))
throw std::runtime_error("missing value");
try
{
val = stoul(token, nullptr, 2);
}
try { value = stoul(token, nullptr, 2); }
catch (const std::logic_error &)
{
// array element index
try
{
token = token.substr(1, token.size() - 2);
adr = stoul(token, nullptr, 2);
address = stoul(token, nullptr, 2);
}
catch (const std::logic_error &)
{
......@@ -55,71 +49,30 @@ Boolector::parse_line (std::istringstream & line)
if (!(line >> token))
throw std::runtime_error("missing array value");
try
{
val = stoul(token, nullptr, 2);
}
try { value = stoul(token, nullptr, 2); }
catch (const std::logic_error &)
{
throw std::runtime_error("illegal array value [" + token + "]");
}
}
// parse variable
std::optional<Variable> variable = parse_variable(line);
// parse symbol
Symbol symbol = parse_symbol(line);
/*
if (variable && variable->type == Variable::Type::EXEC && val)
switch (symbol)
{
cout
<< "exec step = " << variable->step
<< " thread = " << variable->thread
<< " pc = " << variable->pc << eol;
case Symbol::stmt:
case Symbol::exit_flag:
case Symbol::thread:
case Symbol::flush:
if (value)
return symbol;
break;
default: return symbol;
}
if (variable && variable->step)
{
cout << "\tvariable: ";
switch (variable->type)
{
case Variable::Type::THREAD: cout << "THREAD"; break;
case Variable::Type::EXEC: cout << "EXEC"; break;
case Variable::Type::ACCU: cout << "ACCU"; break;
case Variable::Type::MEM: cout << "MEM"; break;
case Variable::Type::HEAP: cout << "HEAP"; break;
case Variable::Type::EXIT: cout << "EXIT"; break;
case Variable::Type::EXIT_CODE: cout << "EXIT_CODE"; break;
default: ;
}
cout << " step = " << variable->step << eol;
}
*/
if (variable && variable->step)
switch (variable->type)
{
case Variable::Type::THREAD:
case Variable::Type::EXEC:
case Variable::Type::EXIT:
if (val)
return variable;
break;
case Variable::Type::ACCU:
case Variable::Type::MEM:
case Variable::Type::EXIT_CODE:
variable->val = val;
return variable;
case Variable::Type::HEAP:
variable->adr = adr;
variable->val = val;
return variable;
default: {}
}
return {};
return Symbol::ignore;
}
} // namespace ConcuBinE
......@@ -11,7 +11,7 @@ class Boolector : public External
protected:
virtual std::optional<Variable> parse_line (std::istringstream & line);
virtual Symbol parse_line (std::istringstream & line);
public:
......
......@@ -19,7 +19,7 @@ std::string BtorMC::build_formula (Encoder & formula,
return formula.str() + (constraints.empty() ? "" : constraints + eol);
}
std::optional<BtorMC::Variable> BtorMC::parse_line (std::istringstream & line)
BtorMC::Symbol BtorMC::parse_line (std::istringstream & line)
{
switch (line.peek())
{
......@@ -34,16 +34,14 @@ std::optional<BtorMC::Variable> BtorMC::parse_line (std::istringstream & line)
}
}
std::optional<BtorMC::Variable> BtorMC::parse_variable (std::istringstream & line)
BtorMC::Symbol BtorMC::parse_symbol (std::istringstream & line)
{
std::optional<Variable> variable {Variable()};
std::ostringstream os;
// cout << line.str() << eol;
// if (!getline(line >> ws, name, '_'))
// runtime_error("missing variable");
// runtime_error("missing symbol");
line >> std::ws;
......@@ -58,64 +56,62 @@ std::optional<BtorMC::Variable> BtorMC::parse_variable (std::istringstream & lin
if (name == Encoder::thread_sym)
{
variable->type = Variable::Type::THREAD;
variable->thread = parse_attribute(line, "thread", '@');
variable->step = parse_attribute(line, "step") + 1;
thread = parse_symbol(line, "thread", '@');
step = parse_symbol(line, "step") + 1;
return Symbol::thread;
}
else if (name == Encoder::stmt_sym)
{
variable->type = Variable::Type::EXEC;
variable->thread = parse_attribute(line, "thread");
variable->pc = parse_attribute(line, "pc", '#');
variable->step = parse_attribute(line, "step") + 1;
thread = parse_symbol(line, "thread");
pc = parse_symbol(line, "pc", '#');
step = parse_symbol(line, "step") + 1;
return Symbol::stmt;
}
else if (name == Encoder::accu_sym)
{
variable->type = Variable::Type::ACCU;
variable->thread = parse_attribute(line, "thread", '#');
variable->step = parse_attribute(line, "step");
thread = parse_symbol(line, "thread", '#');
step = parse_symbol(line, "step");
return Symbol::accu;
}
else if (name == Encoder::mem_sym)
{
variable->type = Variable::Type::MEM;
variable->thread = parse_attribute(line, "thread", '#');
variable->step = parse_attribute(line, "step");
thread = parse_symbol(line, "thread", '#');
step = parse_symbol(line, "step");
return Symbol::mem;
}
else if (name == Encoder::heap_sym)
{
variable->type = Variable::Type::HEAP;
variable->step = parse_attribute(line, "step", '@');
step = parse_symbol(line, "step", '@');
return Symbol::heap;
}
else if (name == Encoder::exit_flag_sym)
{
variable->type = Variable::Type::EXIT;
variable->step = parse_attribute(line, "step", '#');
step = parse_symbol(line, "step", '#');
return Symbol::exit_flag;
}
else if (name == Encoder::exit_code_sym)
{
variable->type = Variable::Type::EXIT_CODE;
variable->step = parse_attribute(line, "step", '#');
step = parse_symbol(line, "step", '#');
return Symbol::exit_code;
}
else
return {};
/*
cout << "variable: ";
switch (variable->type)
cout << "symbol: ";
switch (symbol->type)
{
case Variable::Type::THREAD: cout << "THREAD"; break;
case Variable::Type::EXEC: cout << "EXEC"; break;
case Variable::Type::ACCU: cout << "ACCU"; break;
case Variable::Type::MEM: cout << "MEM"; break;
case Variable::Type::HEAP: cout << "HEAP"; break;
case Variable::Type::EXIT: cout << "EXIT"; break;
case Variable::Type::EXIT_CODE: cout << "EXIT_CODE"; break;
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: ;
}
cout << " step = " << variable->step << eol;
cout << " step = " << symbol->step << eol;
*/
return variable;
return Symbol::ignore;
}
} // namespace ConcuBinE
......@@ -5,7 +5,7 @@
namespace ConcuBinE {
struct BtorMC : public Boolector
struct BtorMC : Boolector
{
BtorMC (size_t);
......@@ -15,9 +15,11 @@ struct BtorMC : public Boolector
virtual std::string build_formula (Encoder &, const std::string &);
virtual std::optional<Variable> parse_line (std::istringstream &);
virtual Symbol parse_line (std::istringstream &);
virtual std::optional<Variable> parse_variable (std::istringstream &);
using Boolector::parse_symbol;
virtual Symbol parse_symbol (std::istringstream &);
virtual std::string name () const;
};
......
......@@ -20,7 +20,7 @@ std::string CVC4::build_formula (Encoder & formula,
smtlib::get_model();
}
std::optional<CVC4::Variable> CVC4::parse_line (std::istringstream & line)
CVC4::Symbol CVC4::parse_line (std::istringstream & line)
{
// TODO
(void) line;
......
......@@ -14,7 +14,7 @@ private:
virtual std::string build_formula (Encoder & encoder,
const std::string & constraints);
virtual std::optional<Variable> parse_line (std::istringstream &);
virtual Symbol parse_line (std::istringstream &);
public:
......
This diff is collapsed.
......@@ -24,10 +24,6 @@ struct Solver
// member functions
//----------------------------------------------------------------------------
size_t parse_attribute (std::istringstream & line,
const std::string & name,
char delimiter = '_');
// build formula for the specific solver
//
virtual std::string build_formula (Encoder & encoder,
......@@ -53,37 +49,52 @@ struct Solver
// Base class for solvers running in a forked process.
//==============================================================================
struct External : public Solver
struct External : Solver
{
//----------------------------------------------------------------------------
// member types
//----------------------------------------------------------------------------
struct Variable
enum class Symbol
{
enum class Type
{
THREAD,
EXEC,
ACCU,
MEM,
HEAP,
EXIT,
EXIT_CODE
};
Type type;
size_t step;
word_t thread;
word_t pc;
word_t adr;
word_t val;
ignore,
accu,
mem,
sb_adr,
sb_val,
sb_full,
heap,
stmt,
thread,
flush,
exit_flag,
exit_code
};
//----------------------------------------------------------------------------
// members
//----------------------------------------------------------------------------
// current step
//
size_t step;
// current thread
//
word_t thread;
// current pc
//
word_t pc;
// current address
//
word_t address;
// current value
//
word_t value;
// the solver's stdout
//
std::stringstream std_out;
......@@ -92,6 +103,10 @@ struct External : public Solver
// member functions
//----------------------------------------------------------------------------
virtual bool sat (const std::string & formula);
virtual Trace::ptr solve (Encoder & encoder, const std::string & constraints);
// build command line for the specific solver
//
virtual std::string build_command () = 0;
......@@ -100,13 +115,19 @@ struct External : public Solver
//
Trace::ptr build_trace (const Program::List::ptr & programs);
virtual std::optional<Variable> parse_variable (std::istringstream & line);
virtual std::optional<Variable> parse_line (std::istringstream & line) = 0;
// parse integer attribute of current symbol
//
size_t parse_symbol (std::istringstream & line,
const std::string & name,
char delimiter = '_');
virtual bool sat (const std::string & formula);
// parse current variable's symbol
//
virtual Symbol parse_symbol (std::istringstream & line);
virtual Trace::ptr solve (Encoder & encoder, const std::string & constraints);
// parse variable
//
virtual Symbol parse_line (std::istringstream & line) = 0;
};
} // namespace ConcuBinE
......
......@@ -52,15 +52,15 @@ 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 += MMap.*
# GTEST_FILTER += Trace.*
# GTEST_FILTER += MMap.*
# GTEST_FILTER += Shell.*
# GTEST_FILTER += Boolector.*
GTEST_FILTER += Boolector.*
# GTEST_FILTER += BtorMC.*
# GTEST_FILTER += Z3.*
# GTEST_FILTER += CVC4.*
......@@ -93,9 +93,7 @@ valgrind: $(TEST_RUN)
experiments: experimental
./$<
EXPERIMENTS = experiments.cc \
../instruction.hh ../instruction.cc \
../program.hh ../program.cc
EXPERIMENTS = experiments.cc
experimental: $(EXPERIMENTS) $(GTEST_LIB)
$(CXX) $(CXXFLAGS) $^ $(TEST_MAIN) -o $@
......
This diff is collapsed.
......@@ -38,7 +38,7 @@ TEST_F(Boolector, unsat)
ASSERT_EQ("unsat\n", boolector.std_out.str());
}
TEST_F(Boolector, DISABLED_solve_check)
TEST_F(Boolector, solve_check)
{
// concurrent increment using CHECK
std::string increment_0 = "data/increment.check.thread.0.asm";
......@@ -53,107 +53,18 @@ TEST_F(Boolector, DISABLED_solve_check)
trace = boolector.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"
"1 4 STORE 0 2 0 {(0,2)}\n"
"0 6 JNZ 1 1 0 {}\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",
trace->print());
std::ofstream file {"/tmp/test.trace"};
file << trace->print();
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));
ASSERT_EQ(*simulated, *trace);
// std::cout << replay->print();
ASSERT_EQ(*replay, *trace);
}
TEST_F(Boolector, DISABLED_solve_cas)
TEST_F(Boolector, solve_cas)
{
// concurrent increment using CAS
std::string increment = "data/increment.cas.asm";
......@@ -167,28 +78,15 @@ TEST_F(Boolector, DISABLED_solve_cas)
trace = boolector.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);
}
TEST_F(Boolector, DISABLED_encode_deadlock)
......@@ -216,7 +114,7 @@ TEST_F(Boolector, 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<smtlib::Functional>(programs, 12);
encoder = std::make_unique<smtlib::Functional>(programs, 16);
std::string formula = boolector.build_formula(*encoder, constraints);
......@@ -238,7 +136,7 @@ TEST_F(Boolector, 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<smtlib::Functional>(programs, 12);
encoder = std::make_unique<smtlib::Functional>(programs, 16);
std::string formula = boolector.build_formula(*encoder, constraints);
......
......@@ -1188,13 +1188,13 @@ TEST_F(Trace, iterator_check)
if (i == 3)
{
ASSERT_EQ(0, it->heap->adr);
ASSERT_EQ(0, it->heap->val);
ASSERT_EQ(0, it->heap->first);
ASSERT_EQ(0, it->heap->second);
}
else if (i == 14)
{
ASSERT_EQ(0, it->heap->adr);
ASSERT_EQ(1, it->heap->val);
ASSERT_EQ(0, it->heap->first);
ASSERT_EQ(1, it->heap->second);
}
else
ASSERT_FALSE(it->heap);
......@@ -1234,13 +1234,13 @@ TEST_F(Trace, iterator_cas)
if (i == 3 || i == 4)
{
ASSERT_EQ(0, it->heap->adr);
ASSERT_EQ(0, it->heap->val);
ASSERT_EQ(0, it->heap->first);
ASSERT_EQ(0, it->heap->second);
}
else if (i == 12)
{
ASSERT_EQ(0, it->heap->adr);
ASSERT_EQ(1, it->heap->val);
ASSERT_EQ(0, it->heap->first);
ASSERT_EQ(1, it->heap->second);
}
else
ASSERT_FALSE(it->heap);
......@@ -1282,7 +1282,7 @@ TEST_F(Trace, operator_equals)
ASSERT_TRUE(s1 == s2);
// non-empty trace
std::optional<ConcuBinE::Trace::cell_t> heap;
std::optional<std::pair<word_t, word_t>> heap;
s1.push_back(0, 0, 0, 0, 0, 0, false, heap = {1, 0});
s1.push_back(1, 0, 0, 0, 0, 0, false, heap);
s1.push_back(0, 1, 1, 0, 0, 0, false, heap);
......
......@@ -295,7 +295,7 @@ Trace::Trace(std::istream & file, const std::string & path) :
}
// parse heap cell
std::optional<cell_t> heap;
std::optional<std::pair<word_t, word_t>> heap;
if (!(line >> token))
parser_error(path, line_num, "missing heap update");
......@@ -392,7 +392,7 @@ void Trace::push_back (const word_t thread,
const word_t buffer_adr,
const word_t buffer_val,
const word_t buffer_full,
std::optional<cell_t> & heap,
std::optional<std::pair<word_t, word_t>> & heap,
const bool flush)
{
push_back<word_t>(thread_updates, length, thread);
......@@ -405,8 +405,11 @@ void Trace::push_back (const word_t thread,
if (heap)
{
heap_adr_updates.emplace_hint(heap_adr_updates.end(), length, heap->adr);
push_back(heap_val_updates[heap->adr], length, heap->val);
heap_adr_updates.emplace_hint(
heap_adr_updates.end(),
length,
heap->first);
push_back(heap_val_updates[heap->second], length, heap->first);
heap.reset();
}
......@@ -604,9 +607,9 @@ Trace::iterator Trace::end () const
std::string Trace::print (const Step & step) const
{
std::ostringstream ss;
constexpr char sep = '\t';
const char sep = '\t';
std::ostringstream ss;
// thread id
ss << step.thread << sep;
......@@ -664,13 +667,13 @@ std::string Trace::print (const Step & step) const
ss << '{';
if (step.heap)
ss << '(' << step.heap->adr << ',' << step.heap->val << ')';
ss << '(' << step.heap->first << ',' << step.heap->second << ')';
ss << '}';
// step number
if (verbose)
ss << sep << "# " << std::to_string(step.step);
ss << sep << "# " << std::to_string(step);
ss << eol;
......@@ -710,7 +713,7 @@ std::string Trace::print () const
// constructors
//------------------------------------------------------------------------------
Trace::Step::Step (size_t s) : step(s) {}
Trace::Step::Step (size_t k) : number(k) {}
//------------------------------------------------------------------------------