Commit 3f37c3c5 authored by phlo's avatar phlo

added CVC4::parse_line

parent 911eb67b
#include "boolector.hh"
#include <iomanip>
#include "parser.hh"
namespace ConcuBinE {
......@@ -43,6 +41,8 @@ Boolector::Symbol Boolector::parse_line (std::istringstream & line)
try { value = stoul(token, nullptr, 2); }
catch (const std::logic_error &)
{
word_t address;
// array element index
try
{
......@@ -63,6 +63,8 @@ Boolector::Symbol Boolector::parse_line (std::istringstream & line)
{
throw std::runtime_error("illegal array value [" + token + "]");
}
heap[address] = value;
}
// parse symbol
......
......@@ -77,41 +77,43 @@ BtorMC::Symbol BtorMC::parse_symbol (std::istringstream & line)
if (name.empty())
throw std::runtime_error("missing symbol");
line.unget();
if (name == Encoder::accu_sym)
{
thread = parse_symbol(line, "thread", '#');
step = parse_symbol(line, "step");
thread = parse_symbol(line, "thread");
step = parse_symbol(line, "step", '#');
return Symbol::accu;
}
else if (name == Encoder::mem_sym)
{
thread = parse_symbol(line, "thread", '#');
step = parse_symbol(line, "step");
thread = parse_symbol(line, "thread");
step = parse_symbol(line, "step", '#');
return Symbol::mem;
}
else if (name == Encoder::sb_adr_sym)
{
thread = parse_symbol(line, "thread", '#');
step = parse_symbol(line, "step");
thread = parse_symbol(line, "thread");
step = parse_symbol(line, "step", '#');
return Symbol::sb_adr;
}
else if (name == Encoder::sb_val_sym)
{
thread = parse_symbol(line, "thread", '#');
step = parse_symbol(line, "step");
thread = parse_symbol(line, "thread");
step = parse_symbol(line, "step", '#');
return Symbol::sb_val;
}
else if (name == Encoder::sb_full_sym)
{
thread = parse_symbol(line, "thread", '#');
step = parse_symbol(line, "step");
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");
pc = parse_symbol(line, "pc");
step = parse_symbol(line, "step", '#');
return Symbol::stmt;
}
else if (name == Encoder::heap_sym)
......@@ -131,14 +133,14 @@ BtorMC::Symbol BtorMC::parse_symbol (std::istringstream & line)
}
else if (name == Encoder::thread_sym)
{
thread = parse_symbol(line, "thread", '@');
step = parse_symbol(line, "step");
thread = parse_symbol(line, "thread");
step = parse_symbol(line, "step", '@');
return Symbol::thread;
}
else if (name == Encoder::flush_sym)
{
thread = parse_symbol(line, "thread", '@');
step = parse_symbol(line, "step");
thread = parse_symbol(line, "thread");
step = parse_symbol(line, "step", '@');
return Symbol::flush;
}
......
......@@ -4,13 +4,27 @@
namespace ConcuBinE {
//==============================================================================
// CVC4
//==============================================================================
//------------------------------------------------------------------------------
// member functions
//------------------------------------------------------------------------------
// CVC4::name ------------------------------------------------------------------
std::string CVC4::name () const { return "cvc4"; }
// CVC4::build_command ---------------------------------------------------------
std::string CVC4::build_command ()
{
return "cvc4 -L smt2 -m --output-lang=cvc4";
}
// CVC4::build_formula ---------------------------------------------------------
std::string CVC4::build_formula (Encoder & formula,
const std::string & constraints)
{
......@@ -20,12 +34,78 @@ std::string CVC4::build_formula (Encoder & formula,
smtlib::get_model();
}
// CVC4::parse_line ------------------------------------------------------------
inline
bool parse_bool (std::istringstream & line, std::string & token)
{
line >> token;
return token == "TRUE;";
}
inline
word_t parse_bv (std::istringstream & line, std::string & token)
{
line.seekg(static_cast<long>(line.tellg()) + 5) >> token;
try { return std::stoul(token, NULL, 2); }
catch (...) { throw std::runtime_error("illegal value [" + token + "]"); }
}
CVC4::Symbol CVC4::parse_line (std::istringstream & line)
{
// TODO
(void) line;
Symbol symbol = parse_symbol(line);
std::string token;
if (!std::getline(line, token, '='))
throw std::runtime_error("missing value");
switch (symbol)
{
case Symbol::accu:
case Symbol::mem:
case Symbol::sb_adr:
case Symbol::sb_val:
case Symbol::exit_code:
value = parse_bv(line, token);
return symbol;
case Symbol::sb_full:
value = parse_bool(line, token);
return symbol;
case Symbol::heap:
while (line && token != "WITH")
line >> token;
while (line && token.back() != ';')
{
// skip "["
line.seekg(static_cast<long>(line.tellg()) + 1);
word_t address = parse_bv(line, token);
// skip " := 0bin"
line.seekg(static_cast<long>(line.tellg()) + 8);
value = parse_bv(line, token);
heap[address] = value;
}
return symbol;
case Symbol::stmt:
case Symbol::exit_flag:
case Symbol::thread:
case Symbol::flush:
if (parse_bool(line, token))
return symbol;
else
return Symbol::ignore;
return {};
default: return symbol;
}
}
} // namespace ConcuBinE
......@@ -5,9 +5,19 @@
namespace ConcuBinE {
class CVC4 : public External
//==============================================================================
// CVC4 class
//
// NOTE: seems like CVC4 always assigns uninitialized array elements with zero
//==============================================================================
struct CVC4 : public External
{
private:
//----------------------------------------------------------------------------
// member functions
//----------------------------------------------------------------------------
virtual std::string name () const;
virtual std::string build_command ();
......@@ -15,10 +25,6 @@ private:
const std::string & constraints);
virtual Symbol parse_line (std::istringstream &);
public:
virtual std::string name () const;
};
} // namespace ConcuBinE
......
......@@ -57,11 +57,8 @@ Trace::ptr External::build_trace (const Program::List::ptr & programs)
{
Trace::ptr trace = std::make_unique<Trace>(programs);
// heap updates found in the model (might contain spurious elements)
std::unordered_map<word_t, word_t> heap;
// instruction at step - 2, leading to the previous step's state update
const Instruction * op = NULL;
const Instruction * op = nullptr;
// current line number
size_t lineno = 2;
......@@ -91,23 +88,23 @@ Trace::ptr External::build_trace (const Program::List::ptr & programs)
// NOTE: heap update visible one step after flush is set
if (trace->flush(k))
{
address = trace->sb_adr(t);
assert(heap.find(address) != heap.end());
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))
{
address = op->indirect() ? heap[op->arg()] : op->arg();
word_t address = op->indirect() ? heap[op->arg()] : op->arg();
trace->push_back_heap(step - 1, address, heap[address]);
}
// TODO: get correct thread, pc and accu for step - 2
// instruction executed at step - 2
op = &(*programs)[t][trace->pc(t)];
// reset heap map for the next step
heap = {};
// NOTE: really necessary?
heap.clear();
}
switch (symbol)
......@@ -132,10 +129,6 @@ Trace::ptr External::build_trace (const Program::List::ptr & programs)
trace->push_back_sb_full(step, thread, value);
break;
case Symbol::heap:
heap[address] = value;
break;
case Symbol::thread:
trace->push_back_thread(step, thread);
break;
......@@ -149,7 +142,8 @@ Trace::ptr External::build_trace (const Program::List::ptr & programs)
trace->push_back_flush(step);
break;
case Symbol::exit_flag: break;
case Symbol::exit_flag:
break;
case Symbol::exit_code:
trace->exit = value;
......@@ -174,16 +168,21 @@ size_t External::parse_symbol (std::istringstream & line,
const std::string & name,
const char delimiter)
{
std::string token;
if (line.peek() != delimiter)
{
std::string token;
line >> token;
throw std::runtime_error("missing delimiter [" + token + "]");
}
if (!getline(line, token, delimiter))
line.get(); // discard delimiter
size_t val;
if (!(line >> val))
throw std::runtime_error("missing " + name);
try { return stoul(token); }
catch (...)
{
throw std::runtime_error("illegal " + name + " [" + token + "]");
}
return val;
}
External::Symbol External::parse_symbol (std::istringstream & line)
......@@ -193,6 +192,8 @@ External::Symbol External::parse_symbol (std::istringstream & line)
if (!getline(line >> std::ws, name, '_'))
throw std::runtime_error("missing symbol");
line.unget(); // restore initial delimiter
if (name == Encoder::accu_sym)
{
step = parse_symbol(line, "step");
......
......@@ -32,15 +32,15 @@ struct Solver
// member functions
//----------------------------------------------------------------------------
// returns the solver's name
//
virtual std::string name () const = 0;
// build formula for the specific solver
//
virtual std::string build_formula (Encoder & encoder,
const std::string & constraints);
// returns the solver's name
//
virtual std::string name () const = 0;
// evaluate arbitrary formula
//
virtual bool sat (const std::string & formula) = 0;
......@@ -95,14 +95,14 @@ struct External : Solver
//
word_t pc;
// current address
//
word_t address;
// current value
//
word_t value;
// current heap state (might contain spurious elements)
//
std::unordered_map<word_t, word_t> heap;
// the solver's stdout
//
std::stringstream std_out;
......
......@@ -60,10 +60,10 @@ GTEST_FILTER = --gtest_filter=
# GTEST_FILTER += Trace.*
# GTEST_FILTER += MMap.*
# GTEST_FILTER += Shell.*
# GTEST_FILTER += Boolector.*
# GTEST_FILTER += BtorMC.*
GTEST_FILTER += Boolector.*
GTEST_FILTER += BtorMC.*
GTEST_FILTER += Z3.*
# GTEST_FILTER += CVC4.*
GTEST_FILTER += CVC4.*
GTEST_FILTER := $(shell echo ${GTEST_FILTER} | sed -e 's/ /:/g')
......
......@@ -21,19 +21,13 @@ struct Boolector : public ::testing::Test
TEST_F(Boolector, sat)
{
std::string formula = "(assert true)(check-sat)";
ASSERT_TRUE(boolector.sat(formula));
ASSERT_TRUE(boolector.sat("(assert true)(check-sat)"));
ASSERT_EQ("sat\n", boolector.std_out.str());
}
TEST_F(Boolector, unsat)
{
std::string formula = "(assert false)(check-sat)";
ASSERT_FALSE(boolector.sat(formula));
ASSERT_FALSE(boolector.sat("(assert false)(check-sat)"));
ASSERT_EQ("unsat\n", boolector.std_out.str());
}
......
......@@ -21,12 +21,10 @@ struct BtorMC : public ::testing::Test
TEST_F(BtorMC, sat)
{
std::string formula =
ASSERT_TRUE(btormc.sat(
"1 sort bitvec 1\n"
"2 state 1 x\n"
"3 bad 2\n";
ASSERT_TRUE(btormc.sat(formula));
"3 bad 2\n"));
ASSERT_EQ(
"sat\n"
"b0 \n"
......@@ -39,11 +37,9 @@ TEST_F(BtorMC, sat)
TEST_F(BtorMC, unsat)
{
std::string formula =
ASSERT_FALSE(btormc.sat(
"1 sort bitvec 1\n"
"2 state 1 x\n";
ASSERT_FALSE(btormc.sat(formula));
"2 state 1 x\n"));
ASSERT_EQ("", btormc.std_out.str());
}
......
......@@ -2,7 +2,7 @@
#include "encoder.hh"
#include "parser.hh"
#include "streamredirecter.hh"
#include "simulator.hh"
#include "publicate.hh"
#include "cvc4.hh"
......@@ -16,38 +16,138 @@ namespace ConcuBinE::test {
struct CVC4 : public ::testing::Test
{
ConcuBinE::CVC4 cvc4;
Encoder::ptr encoder;
Program::List::ptr programs = std::make_shared<Program::List>();
Trace::ptr trace;
};
TEST_F(CVC4, sat)
{
std::string formula = "(set-logic QF_AUFBV)(assert true)(check-sat)";
ASSERT_TRUE(cvc4.sat("(set-logic QF_AUFBV)(assert true)(check-sat)"));
ASSERT_EQ("sat\n", cvc4.std_out.str());
}
TEST_F(CVC4, unsat)
{
ASSERT_FALSE(cvc4.sat("(set-logic QF_AUFBV)(assert false)(check-sat)"));
ASSERT_EQ("unsat\n", cvc4.std_out.str());
}
TEST_F(CVC4, solve_check)
{
// concurrent increment using CHECK
std::string increment_0 = "data/increment.check.thread.0.asm";
std::string increment_n = "data/increment.check.thread.n.asm";
programs->push_back(create_from_file<Program>(increment_0));
programs->push_back(create_from_file<Program>(increment_n));
std::ostringstream ss;
StreamRedirecter redirecter(std::cout, ss);
encoder = std::make_unique<smtlib::Functional>(programs, 16);
redirecter.start();
trace = cvc4.solve(*encoder);
ASSERT_TRUE(cvc4.sat(formula));
std::cout << "time to solve = " << cvc4.time << " ms" << eol;
redirecter.stop();
// std::cout << trace->print();
ASSERT_EQ("sat\n", cvc4.std_out.str());
Simulator simulator (programs);
Trace::ptr replay (simulator.replay(*trace));
// std::cout << replay->print();
ASSERT_EQ(*replay, *trace);
}
TEST_F(CVC4, unsat)
TEST_F(CVC4, solve_cas)
{
std::string formula = "(set-logic QF_AUFBV)(assert false)(check-sat)";
// concurrent increment using CAS
std::string increment = "data/increment.cas.asm";
std::ostringstream ss;
StreamRedirecter redirecter(std::cout, ss);
programs->push_back(create_from_file<Program>(increment));
programs->push_back(create_from_file<Program>(increment));
redirecter.start();
encoder = std::make_unique<smtlib::Functional>(programs, 16);
ASSERT_FALSE(cvc4.sat(formula));
trace = cvc4.solve(*encoder);
redirecter.stop();
std::cout << "time to solve = " << cvc4.time << " ms" << eol;
ASSERT_EQ("unsat\n", cvc4.std_out.str());
// std::cout << trace->print();
Simulator simulator (programs);
Trace::ptr replay (simulator.replay(*trace));
// std::cout << replay->print();
ASSERT_EQ(*replay, *trace);
}
TEST_F(CVC4, DISABLED_solve_multiple_addresses)
{
std::istringstream p0 (
"STORE 0\n"
"ADDI 1\n"
"STORE 0\n"
"HALT\n");
std::istringstream p1 (
"STORE 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, 16);
trace = cvc4.solve(*encoder);
std::cout << "time to solve = " << cvc4.time << " ms" << eol;
std::cout << trace->print();
Simulator simulator (programs);
Trace::ptr replay (simulator.replay(*trace));
std::cout << replay->print();
ASSERT_EQ(*replay, *trace);
}
TEST_F(CVC4, DISABLED_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, 16);
trace = cvc4.solve(*encoder);
std::cout << "time to solve = " << cvc4.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
......@@ -58,16 +158,12 @@ TEST_F(CVC4, print_model_check)
std::string increment_0 = "data/increment.check.thread.0.asm";
std::string increment_n = "data/increment.check.thread.n.asm";
Program::List::ptr programs = std::make_shared<Program::List>();
programs->push_back(create_from_file<Program>(increment_0));
programs->push_back(create_from_file<Program>(increment_n));
Encoder::ptr encoder = std::make_unique<smtlib::Functional>(programs, 12);
encoder = std::make_unique<smtlib::Functional>(programs, 16);
std::string formula = cvc4.build_formula(*encoder, constraints);
bool sat = cvc4.sat(formula);
bool sat = cvc4.sat(cvc4.build_formula(*encoder, constraints));
std::ofstream outfile("/tmp/cvc4.check.out");
outfile << cvc4.std_out.str();
......@@ -81,18 +177,71 @@ TEST_F(CVC4, print_model_cas)
std::string constraints;
std::string increment_cas = "data/increment.cas.asm";
Program::List::ptr programs = std::make_shared<Program::List>();
programs->push_back(create_from_file<Program>(increment_cas));
programs->push_back(create_from_file<Program>(increment_cas));
Encoder::ptr encoder = std::make_unique<smtlib::Functional>(programs, 12);
encoder = std::make_unique<smtlib::Functional>(programs, 16);
bool sat = cvc4.sat(cvc4.build_formula(*encoder, constraints));
std::ofstream outfile("/tmp/cvc4.cas.out");
outfile << cvc4.std_out.str();
ASSERT_TRUE(sat);
}
TEST_F(CVC4, DISABLED_print_multiple_addresses)
{
std::istringstream p0 (
"STORE 0\n"
"ADDI 1\n"
"STORE 0\n"
"HALT\n");
std::istringstream p1 (
"STORE 1\n"
"ADDI 1\n"
"STORE 1\n"
"HALT\n");
programs->push_back(Program(p0, "dummy.asm"));
programs->push_back(Program(p1, "dummy.asm"));
encoder = std::make_unique<smtlib::Functional>(programs, 16);
bool sat = cvc4.sat(cvc4.build_formula(*encoder, ""));
std::ofstream outfile("/tmp/cvc4.multiple-addresses.out");
outfile << cvc4.std_out.str();
ASSERT_TRUE(sat);
}
TEST_F(CVC4, DISABLED_print_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, "dummy.asm"));
programs->push_back(Program(p1, "dummy.asm"));
encoder = std::make_unique<smtlib::Functional>(programs, 16);
std::string formula = cvc4.build_formula(*encoder, constraints);
std::string formula = cvc4.build_formula(*encoder, "");
std::ofstream f("/tmp/cvc4.indirect.uninitialized.smt2");
f << formula;
bool sat = cvc4.sat(formula);
std::ofstream outfile("/tmp/cvc4.cas.out");
std::ofstream outfile("/tmp/cvc4.indirect.uninitialized.out");
outfile << cvc4.std_out.str();
ASSERT_TRUE(sat);
......
......@@ -21,16 +21,12 @@ struct Z3 : public ::testing::Test
TEST_F(Z3, sat)
{
std::string formula = "(assert true)(check-sat)";
ASSERT_TRUE(z3.sat(formula));
ASSERT_TRUE(z3.sat("(assert true)(check-sat)"));
}
TEST_F(Z3, unsat)
{
std::string formula = "(assert false)(check-sat)";
ASSERT_FALSE(z3.sat(formula));
ASSERT_FALSE(z3.sat("(assert false)(check-sat)"));
}
TEST_F(Z3, solve_check)
......
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