Commit 911eb67b authored by phlo's avatar phlo

updated Z3::solve

parent ac6912ac
......@@ -52,17 +52,17 @@ 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 += Z3.*
# GTEST_FILTER += Boolector.*
# GTEST_FILTER += BtorMC.*
GTEST_FILTER += Z3.*
# GTEST_FILTER += CVC4.*
GTEST_FILTER := $(shell echo ${GTEST_FILTER} | sed -e 's/ /:/g')
......
......@@ -52,7 +52,7 @@ TEST_F(Boolector, solve_check)
trace = boolector.solve(*encoder);
std::cout << "time to solve = " << boolector.time << "ms" << eol;
std::cout << "time to solve = " << boolector.time << " ms" << eol;
// std::cout << trace->print();
......@@ -79,7 +79,7 @@ TEST_F(Boolector, solve_cas)
trace = boolector.solve(*encoder);
std::cout << "time to solve = " << boolector.time << "ms" << eol;
std::cout << "time to solve = " << boolector.time << " ms" << eol;
// std::cout << trace->print();
......
......@@ -62,7 +62,7 @@ TEST_F(BtorMC, solve_check)
trace = btormc.solve(*encoder);
std::cout << "time to solve = " << btormc.time << "ms" << eol;
std::cout << "time to solve = " << btormc.time << " ms" << eol;
// std::cout << trace->print();
......@@ -89,7 +89,7 @@ TEST_F(BtorMC, solve_cas)
trace = btormc.solve(*encoder);
std::cout << "time to solve = " << btormc.time << "ms" << eol;
std::cout << "time to solve = " << btormc.time << " ms" << eol;
// std::cout << trace->print();
......
......@@ -2,6 +2,7 @@
#include "encoder.hh"
#include "parser.hh"
#include "simulator.hh"
#include "z3.hh"
namespace ConcuBinE::test {
......@@ -48,28 +49,17 @@ TEST_F(Z3, solve_check)
trace = z3.solve(*encoder, constraints);
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"
"0 5 CHECK 1 1 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"
"1 5 JNZ 0 2 0 {}\n"
"0 6 JNZ 1 1 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"
"0 5 CHECK 1 3 0 {}\n",
trace->print());
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);
}
TEST_F(Z3, solve_cas)
......@@ -87,28 +77,17 @@ TEST_F(Z3, solve_cas)
trace = z3.solve(*encoder, constraints);
ASSERT_EQ(
"data/increment.cas.asm\n"
"data/increment.cas.asm\n"
".\n"
"# tid pc cmd arg accu mem heap\n"
"1 0 STORE 0 0 0 {(0,0)}\n"
"0 0 STORE 0 0 0 {}\n"
"1 1 CHECK 0 0 0 {}\n"
"1 LOOP MEM 0 0 0 {}\n"
"1 3 ADDI 1 1 0 {}\n"
"1 4 CAS 0 1 0 {(0,1)}\n"
"1 5 JMP LOOP 1 0 {}\n"
"1 LOOP MEM 0 1 1 {}\n"
"1 3 ADDI 1 2 1 {}\n"
"1 4 CAS 0 1 1 {(0,2)}\n"
"1 5 JMP LOOP 1 1 {}\n"
"1 LOOP MEM 0 2 2 {}\n"
"1 3 ADDI 1 3 2 {}\n"
"1 4 CAS 0 1 2 {(0,3)}\n"
"1 5 JMP LOOP 1 2 {}\n"
"1 LOOP MEM 0 3 3 {}\n",
trace->print());
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
......@@ -970,6 +970,9 @@ bool operator == (const Trace & a, const Trace & b)
a.pc_updates == b.pc_updates &&
a.accu_updates == b.accu_updates &&
a.mem_updates == b.mem_updates &&
a.sb_adr_updates == b.sb_adr_updates &&
a.sb_val_updates == b.sb_val_updates &&
a.sb_full_updates == b.sb_full_updates &&
a.heap_adr_updates == b.heap_adr_updates &&
a.heap_val_updates == b.heap_val_updates;
}
......
#include "z3.hh"
#include <chrono>
#include <z3++.h>
#include "encoder.hh"
namespace ConcuBinE {
//==============================================================================
// Z3
//==============================================================================
//------------------------------------------------------------------------------
// member functions
//------------------------------------------------------------------------------
// Z3::name --------------------------------------------------------------------
std::string Z3::name () const { return "z3"; }
// Z3::sat ---------------------------------------------------------------------
bool Z3::sat (const std::string & formula)
{
using namespace std::chrono;
z3::context c;
z3::solver s = c;
s.from_string(formula.c_str());
return s.check() == z3::sat;
}
high_resolution_clock::time_point t = high_resolution_clock::now();
// TODO: replace with SMTLibEncoder variable name generators
inline
std::string symbol (std::string type, std::initializer_list<size_t> attributes)
{
std::ostringstream os;
s.from_string(formula.c_str());
os << type;
bool sat = s.check() == z3::sat;
for (const size_t a : attributes)
os << '_' << a;
time = duration_cast<milliseconds>(high_resolution_clock::now() - t).count();
return os.str();
return sat;
}
// Z3::solve -------------------------------------------------------------------
inline
bool eval_bool (z3::context & c, const z3::model & m, const std::string sym)
bool eval_bool (z3::context & c, const z3::model & m, const std::string & sym)
{
return m.eval(c.bool_const(sym.c_str())).is_true();
}
inline
word_t eval_bv (z3::context & c, const z3::model & m, const std::string sym)
word_t eval_bv (z3::context & c, const z3::model & m, const std::string & sym)
{
return m.eval(c.bv_const(sym.c_str(), word_size)).get_numeral_uint();
}
......@@ -47,7 +56,7 @@ word_t eval_bv (z3::context & c, const z3::model & m, const std::string sym)
inline
word_t eval_array (z3::context & c,
const z3::model & m,
const std::string sym,
const std::string & sym,
const word_t idx)
{
return
......@@ -64,9 +73,13 @@ word_t eval_array (z3::context & c,
Trace::ptr Z3::solve (Encoder & encoder, const std::string & constraints)
{
using namespace std::chrono;
z3::context c;
z3::solver s = c;
high_resolution_clock::time_point t = high_resolution_clock::now();
s.from_string(build_formula(encoder, constraints).c_str());
if (s.check() != z3::sat)
......@@ -74,52 +87,96 @@ Trace::ptr Z3::solve (Encoder & encoder, const std::string & constraints)
z3::model m = s.get_model();
Trace::ptr trace = std::make_unique<Trace>(std::move(encoder.programs));
time = duration_cast<milliseconds>(high_resolution_clock::now() - t).count();
Trace::ptr trace = std::make_unique<Trace>(encoder.programs);
for (size_t step = 1; step <= encoder.bound; ++step)
for (word_t thread = 0; thread < encoder.programs->size(); ++thread)
if (eval_bool(c, m, symbol(Encoder::thread_sym, {step, thread})))
for (size_t step = 0; step <= encoder.bound; step++)
{
// heap state
if (step)
{
word_t thread = trace->thread();
if (trace->flush(step - 1))
{
trace->push_back_heap(
step,
trace->sb_adr(thread),
trace->sb_val(thread));
}
else
{
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));
}
}
}
// thread states
for (word_t thread = 0; thread < encoder.programs->size(); thread++)
{
if (eval_bool(c, m, smtlib::Encoder::thread_var(step, thread)))
{
trace->push_back_thread(step, thread);
}
else if (eval_bool(c, m, smtlib::Encoder::flush_var(step, thread)))
{
trace->push_back_thread(step, thread);
trace->push_back_flush(step);
}
trace->push_back_accu(
step,
thread,
eval_bv(c, m, smtlib::Encoder::accu_var(step, thread)));
trace->push_back_mem(
step,
thread,
eval_bv(c, m, smtlib::Encoder::mem_var(step, thread)));
trace->push_back_sb_adr(
step,
thread,
eval_bv(c, m, smtlib::Encoder::sb_adr_var(step, thread)));
trace->push_back_sb_val(
step,
thread,
eval_bv(c, m, smtlib::Encoder::sb_val_var(step, thread)));
trace->push_back_sb_full(
step,
thread,
eval_bool(c, m, smtlib::Encoder::sb_full_var(step, thread)));
const Program & program = (*encoder.programs)[thread];
for (word_t pc = 0; pc < program.size(); ++pc)
if (eval_bool(c, m, symbol(Encoder::exec_sym, {step, thread, pc})))
for (word_t pc = 0; pc < program.size(); pc++)
if (eval_bool(c, m, smtlib::Encoder::stmt_var(step, thread, pc)))
{
word_t accu =
eval_bv(c, m, symbol(Encoder::accu_sym, {step, thread}));
word_t mem =
eval_bv(c, m, symbol(Encoder::mem_sym, {step, thread}));
std::optional<std::pair<word_t, word_t>> heap;
const Instruction & op = program[pc];
// get eventual heap update (ignore failed CAS)
// TODO flush!
if (op.is_memory() && op.type() & Instruction::atomic && accu)
{
word_t idx = op.arg();
if (op.indirect())
idx =
eval_array(
c,
m,
symbol(Encoder::heap_sym, {step - 1}),
idx);
heap = {
idx,
eval_array(c, m, symbol(Encoder::heap_sym, {step}), idx)
};
}
// TODO: store buffer
trace->push_back(thread, pc, accu, mem, 0, 0, false, heap);
trace->push_back_pc(step, thread, pc);
break;
}
}
trace->exit = eval_bv(c, m, symbol(Encoder::exit_code_sym, {}));
// exited
if (eval_bool(c, m, smtlib::Encoder::exit_flag_var(step)))
break;
}
trace->exit = eval_bv(c, m, smtlib::Encoder::exit_code_var);
return trace;
}
......
......@@ -7,13 +7,22 @@
namespace ConcuBinE {
//==============================================================================
// Z3 class
//==============================================================================
struct Z3 : public Solver
{
//----------------------------------------------------------------------------
// member functions
//----------------------------------------------------------------------------
virtual std::string name () const;
virtual bool sat (const std::string & formula);
virtual Trace::ptr solve (Encoder & encoder, const std::string & constraints);
virtual Trace::ptr solve (Encoder & encoder,
const std::string & constraints = "");
};
} // namespace ConcuBinE
......
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