Commit 8c6ebe14 authored by phlo's avatar phlo

optimized SMTLib expression generators

parent 8fed41d6
......@@ -179,9 +179,9 @@ void Encoder::assert_exit ()
formula <<
smtlib::assertion(
smtlib::lnot(
smtlib::equality({
smtlib::equality(
smtlib::Encoder::exit_code_var,
smtlib::word2hex(0)})));
smtlib::word2hex(0))));
}
//------------------------------------------------------------------------------
......@@ -366,7 +366,7 @@ std::string Encoder::flush_var () const { return flush_var(step, thread); }
std::string Encoder::assign (const std::string & var,
const std::string & expr) const
{
return assertion(equality({var, expr}));
return assertion(equality(var, expr));
}
//------------------------------------------------------------------------------
......@@ -401,37 +401,37 @@ std::string Encoder::encode (const Instruction::Fence & f [[maybe_unused]])
std::string Encoder::encode (const Instruction::Add & a)
{
return bvadd({accu_var(prev, thread), load(a.arg, a.indirect)});
return bvadd(accu_var(prev, thread), load(a.arg, a.indirect));
}
std::string Encoder::encode (const Instruction::Addi & a)
{
return bvadd({accu_var(prev, thread), word2hex(a.arg)});
return bvadd(accu_var(prev, thread), word2hex(a.arg));
}
std::string Encoder::encode (const Instruction::Sub & s)
{
return bvsub({accu_var(prev, thread), load(s.arg, s.indirect)});
return bvsub(accu_var(prev, thread), load(s.arg, s.indirect));
}
std::string Encoder::encode (const Instruction::Subi & s)
{
return bvsub({accu_var(prev, thread), word2hex(s.arg)});
return bvsub(accu_var(prev, thread), word2hex(s.arg));
}
std::string Encoder::encode (const Instruction::Mul & m)
{
return bvmul({accu_var(prev, thread), load(m.arg, m.indirect)});
return bvmul(accu_var(prev, thread), load(m.arg, m.indirect));
}
std::string Encoder::encode (const Instruction::Muli & m)
{
return bvmul({accu_var(prev, thread), word2hex(m.arg)});
return bvmul(accu_var(prev, thread), word2hex(m.arg));
}
std::string Encoder::encode (const Instruction::Cmp & c)
{
return bvsub({accu_var(prev, thread), load(c.arg, c.indirect)});
return bvsub(accu_var(prev, thread), load(c.arg, c.indirect));
}
std::string Encoder::encode (const Instruction::Jmp & j [[maybe_unused]])
......@@ -441,16 +441,16 @@ std::string Encoder::encode (const Instruction::Jmp & j [[maybe_unused]])
std::string Encoder::encode (const Instruction::Jz & j [[maybe_unused]])
{
return equality({accu_var(prev, thread), word2hex(0)});
return equality(accu_var(prev, thread), word2hex(0));
}
std::string Encoder::encode (const Instruction::Jnz & j [[maybe_unused]])
{
return
lnot(
equality({
equality(
accu_var(prev, thread),
word2hex(0)}));
word2hex(0)));
}
std::string Encoder::encode (const Instruction::Js & j [[maybe_unused]])
......@@ -458,9 +458,9 @@ std::string Encoder::encode (const Instruction::Js & j [[maybe_unused]])
static const std::string bw = std::to_string(word_size - 1);
return
equality({
equality(
"#b1",
extract(bw, bw, accu_var(prev, thread))});
extract(bw, bw, accu_var(prev, thread)));
}
std::string Encoder::encode (const Instruction::Jns & j [[maybe_unused]])
......@@ -468,9 +468,9 @@ std::string Encoder::encode (const Instruction::Jns & j [[maybe_unused]])
static const std::string bw = std::to_string(word_size - 1);
return
equality({
equality(
"#b0",
extract(bw, bw, accu_var(prev, thread))});
extract(bw, bw, accu_var(prev, thread)));
}
std::string Encoder::encode (const Instruction::Jnzns & j [[maybe_unused]])
......@@ -478,14 +478,14 @@ std::string Encoder::encode (const Instruction::Jnzns & j [[maybe_unused]])
static const std::string bw = std::to_string(word_size - 1);
return
land({
land(
lnot(
equality({
equality(
accu_var(prev, thread),
word2hex(0)})),
equality({
word2hex(0))),
equality(
"#b0",
extract(bw, bw, accu_var(prev, thread))})});
extract(bw, bw, accu_var(prev, thread))));
}
std::string Encoder::encode (const Instruction::Mem & m)
......@@ -502,9 +502,9 @@ std::string Encoder::encode (const Instruction::Cas & c)
: word2hex(c.arg);
std::string condition =
equality({
equality(
mem_var(prev, thread),
select(heap, address)});
select(heap, address));
switch (update)
{
......@@ -601,20 +601,20 @@ std::string Encoder::load (const word_t adr, const bool indirect)
ite(
sb_full,
ite(
equality({sb_adr, address}),
equality(sb_adr, address),
ite(
equality({sb_val, address}),
equality(sb_val, address),
sb_val,
select(heap, sb_val)),
ite(
equality({sb_adr, load}),
equality(sb_adr, load),
sb_val,
load_indirect)),
load_indirect);
}
else
{
return ite(land({sb_full, equality({sb_adr, address})}), sb_val, load);
return ite(land(sb_full, equality(sb_adr, address)), sb_val, load);
}
}
......@@ -1049,7 +1049,7 @@ void Encoder::define_exec ()
iterate_programs([this] (const Program & program) {
for (pc = 0; pc < program.size(); pc++)
formula
<< assign(exec_var(), land({stmt_var(), thread_var()}))
<< assign(exec_var(), land(stmt_var(), thread_var()))
<< eol;
formula << eol;
......@@ -1192,9 +1192,9 @@ void Encoder::define_checkpoint_constraints ()
formula <<
assertion(
implication(
land({
land(
block_var(step, c, t),
lnot(check_var(step, c))}),
lnot(check_var(step, c))),
lnot(thread_var(step, t))));
if (verbose)
......
......@@ -125,9 +125,9 @@ void Functional::define_stmt ()
{
// statement reactivation
std::string expr =
land({
land(
stmt_var(prev, thread, pc),
lnot(exec_var(prev, thread, pc))});
lnot(exec_var(prev, thread, pc)));
const auto & pred = predecessors[thread][pc];
......@@ -146,12 +146,12 @@ void Functional::define_stmt ()
// JMP has no condition and returns an empty std::string
if (!cond.empty())
val =
land({
land(
val,
// only activate successor if jump condition failed
*rit == pc - 1 && pre.arg() != pc
? lnot(cond)
: cond});
: cond);
}
// add predecessor to the activation
......
......@@ -31,7 +31,7 @@ std::shared_ptr<std::string> Relational::set_accu (const T & op)
return
std::make_shared<std::string>(
equality({accu_var(), Encoder::encode(op)}));
equality(accu_var(), Encoder::encode(op)));
}
// smtlib::Relational::restore_accu --------------------------------------------
......@@ -40,7 +40,7 @@ std::shared_ptr<std::string> Relational::restore_accu () const
{
return
std::make_shared<std::string>(
equality({accu_var(), accu_var(prev, thread)}));
equality(accu_var(), accu_var(prev, thread)));
}
// smtlib::Relational::set_mem -------------------------------------------------
......@@ -52,7 +52,7 @@ std::shared_ptr<std::string> Relational::set_mem (const T & op)
return
std::make_shared<std::string>(
equality({mem_var(), Encoder::encode(op)}));
equality(mem_var(), Encoder::encode(op)));
}
// smtlib::Relational::restore_mem ---------------------------------------------
......@@ -61,7 +61,7 @@ std::shared_ptr<std::string> Relational::restore_mem () const
{
return
std::make_shared<std::string>(
equality({mem_var(), mem_var(prev, thread)}));
equality(mem_var(), mem_var(prev, thread)));
}
// smtlib::Relational::set_sb_adr ----------------------------------------------
......@@ -73,7 +73,7 @@ std::shared_ptr<std::string> Relational::set_sb_adr (const T & op)
return
std::make_shared<std::string>(
equality({sb_adr_var(), Encoder::encode(op)}));
equality(sb_adr_var(), Encoder::encode(op)));
}
// smtlib::Relational::restore_sb_adr ------------------------------------------
......@@ -82,7 +82,7 @@ std::shared_ptr<std::string> Relational::restore_sb_adr () const
{
return
std::make_shared<std::string>(
equality({sb_adr_var(), sb_adr_var(prev, thread)}));
equality(sb_adr_var(), sb_adr_var(prev, thread)));
}
// smtlib::Relational::set_sb_val ----------------------------------------------
......@@ -94,7 +94,7 @@ std::shared_ptr<std::string> Relational::set_sb_val (const T & op)
return
std::make_shared<std::string>(
equality({sb_val_var(), Encoder::encode(op)}));
equality(sb_val_var(), Encoder::encode(op)));
}
// smtlib::Relational::restore_sb_val ------------------------------------------
......@@ -103,7 +103,7 @@ std::shared_ptr<std::string> Relational::restore_sb_val () const
{
return
std::make_shared<std::string>(
equality({sb_val_var(), sb_val_var(prev, thread)}));
equality(sb_val_var(), sb_val_var(prev, thread)));
}
// smtlib::Relational::set_sb_full ---------------------------------------------
......@@ -119,12 +119,12 @@ std::shared_ptr<std::string> Relational::reset_sb_full () const
{
return
std::make_shared<std::string>(
equality({
equality(
sb_full_var(),
ite(
flush_var(prev, thread),
FALSE,
sb_full_var(prev, thread))}));
sb_full_var(prev, thread))));
}
// smtlib::Relational::restor_sb_full ------------------------------------------
......@@ -133,7 +133,7 @@ std::shared_ptr<std::string> Relational::restore_sb_full () const
{
return
std::make_shared<std::string>(
equality({sb_full_var(), sb_full_var(prev, thread)}));
equality(sb_full_var(), sb_full_var(prev, thread)));
}
// smtlib::Relational::set_stmt ------------------------------------------------
......@@ -210,9 +210,9 @@ std::shared_ptr<std::string> Relational::restore_stmt ()
for (pc = 0; pc < program.size(); pc++)
stmts.push_back(
equality({
equality(
stmt_var(step, thread, pc),
stmt_var(prev, thread, pc)}));
stmt_var(prev, thread, pc)));
pc = cur;
......@@ -244,12 +244,12 @@ std::shared_ptr<std::string> Relational::set_block (const T & op) const
std::string Relational::reset_block (const word_t id) const
{
return
equality({
equality(
block_var(step, id, thread),
ite(
check_var(prev, id),
FALSE,
block_var(prev, id, thread))});
block_var(prev, id, thread)));
}
// smtlib::Relational::restore_block -------------------------------------------
......@@ -287,23 +287,23 @@ std::shared_ptr<std::string> Relational::set_halt () const
return
std::make_shared<std::string>(
land({
land(
halt_var(),
ite(
land(args),
land({
land(
exit_flag_var(),
equality({exit_code_var, word2hex(0)})}),
lnot(exit_flag_var()))}));
equality(exit_code_var, word2hex(0))),
lnot(exit_flag_var()))));
}
else
{
return
std::make_shared<std::string>(
land({
land(
halt_var(),
exit_flag_var(),
equality({exit_code_var, word2hex(0)})}));
equality(exit_code_var, word2hex(0))));
}
}
......@@ -316,7 +316,7 @@ std::shared_ptr<std::string> Relational::restore_halt () const
return
std::make_shared<std::string>(
equality({halt_var(), halt_var(prev, thread)}));
equality(halt_var(), halt_var(prev, thread)));
}
// smtlib::Relational::set_heap ------------------------------------------------
......@@ -328,14 +328,14 @@ std::shared_ptr<std::string> Relational::set_heap (const T & op)
return
std::make_shared<std::string>(
equality({heap_var(), Encoder::encode(op)}));
equality(heap_var(), Encoder::encode(op)));
}
// smtlib::Relational::restore_heap --------------------------------------------
std::shared_ptr<std::string> Relational::restore_heap () const
{
return std::make_shared<std::string>(equality({heap_var(), heap_var(prev)}));
return std::make_shared<std::string>(equality(heap_var(), heap_var(prev)));
}
// smtlib::Relational::set_exit_flag -------------------------------------------
......@@ -362,7 +362,7 @@ std::shared_ptr<std::string> Relational::unset_exit_flag () const
std::shared_ptr<std::string> Relational::set_exit_code (const word_t e) const
{
return std::make_shared<std::string>(equality({exit_code_var, word2hex(e)}));
return std::make_shared<std::string>(equality(exit_code_var, word2hex(e)));
}
// smtlib::Relational::imply_thread_executed -----------------------------------
......@@ -410,12 +410,12 @@ void Relational::imply_thread_flushed ()
{
std::vector<std::string> args({
lnot(sb_full_var()),
equality({
equality(
heap_var(),
store(
heap_var(prev),
sb_adr_var(prev, thread),
sb_val_var(prev, thread))})});
sb_val_var(prev, thread)))});
if (!halts.empty() || !exits.empty())
args.push_back(lnot(exit_flag_var()));
......@@ -452,11 +452,11 @@ void Relational::imply_machine_exited ()
formula <<
imply(
exit_flag_var(prev),
land({
equality({
land(
equality(
heap_var(),
heap_var(prev)}),
exit_flag_var()})) <<
heap_var(prev)),
exit_flag_var())) <<
eol;
// set exit if machine didn't exit within bound
......@@ -464,9 +464,9 @@ void Relational::imply_machine_exited ()
formula <<
imply(
lnot(exit_flag_var()),
equality({
equality(
exit_code_var,
word2hex(0)})) <<
word2hex(0))) <<
eol;
}
......
This diff is collapsed.
......@@ -11,7 +11,7 @@ namespace ConcuBinE::test {
// word2hex ====================================================================
TEST(smtlib, word2hex)
TEST(smtlib, word2hex)
{
ASSERT_EQ("#x0000", smtlib::word2hex(0));
ASSERT_EQ("#x0001", smtlib::word2hex(1));
......@@ -24,7 +24,7 @@ namespace ConcuBinE::test {
TEST(smtlib, expr)
{
ASSERT_EQ("(op x1 x2 x3)", smtlib::expr("op", {"x1", "x2", "x3"}));
ASSERT_EQ("(op x1 x2 x3)", smtlib::expr("op", "x1", "x2", "x3"));
}
// comment =====================================================================
......@@ -75,33 +75,24 @@ TEST(smtlib, lnot)
TEST(smtlib, land)
{
ASSERT_THROW(smtlib::land({}), std::runtime_error);
ASSERT_EQ("x1", smtlib::land({"x1"}));
ASSERT_EQ("(and x1 x2 x3)", smtlib::land({"x1", "x2", "x3"}));
ASSERT_EQ("x1", smtlib::land("x1"));
ASSERT_EQ("(and x1 x2 x3)", smtlib::land("x1", "x2", "x3"));
}
// lor =========================================================================
TEST(smtlib, lor)
{
ASSERT_THROW(smtlib::lor({}), std::runtime_error);
ASSERT_EQ("x1", smtlib::lor({"x1"}));
ASSERT_EQ("(or x1 x2 x3)", smtlib::lor({"x1", "x2", "x3"}));
ASSERT_EQ("x1", smtlib::lor("x1"));
ASSERT_EQ("(or x1 x2 x3)", smtlib::lor("x1", "x2", "x3"));
}
// lxor ========================================================================
TEST(smtlib, lxor)
{
ASSERT_THROW(smtlib::lxor({}), std::runtime_error);
ASSERT_EQ("x1", smtlib::lxor({"x1"}));
ASSERT_EQ("(xor x1 x2 x3)", smtlib::lxor({"x1", "x2", "x3"}));
ASSERT_EQ("x1", smtlib::lxor("x1"));
ASSERT_EQ("(xor x1 x2 x3)", smtlib::lxor("x1", "x2", "x3"));
}
// implication =================================================================
......@@ -115,11 +106,7 @@ TEST(smtlib, implication)
TEST(smtlib, equality)
{
ASSERT_THROW(smtlib::equality({}), std::runtime_error);
ASSERT_THROW(smtlib::equality({"x1"}), std::runtime_error);
ASSERT_EQ("(= x1 x2 x3)", smtlib::equality({"x1", "x2", "x3"}));
ASSERT_EQ("(= x1 x2 x3)", smtlib::equality("x1", "x2", "x3"));
}
// ite =========================================================================
......@@ -133,33 +120,21 @@ TEST(smtlib, ite)
TEST(smtlib, bvadd)
{
ASSERT_THROW(smtlib::bvadd({}), std::runtime_error);
ASSERT_THROW(smtlib::bvadd({"x1"}), std::runtime_error);
ASSERT_EQ("(bvadd x1 x2 x3)", smtlib::bvadd({"x1", "x2", "x3"}));
ASSERT_EQ("(bvadd x1 x2 x3)", smtlib::bvadd("x1", "x2", "x3"));
}
// bvsub =======================================================================
TEST(smtlib, bvsub)
{
ASSERT_THROW(smtlib::bvsub({}), std::runtime_error);
ASSERT_THROW(smtlib::bvsub({"x1"}), std::runtime_error);
ASSERT_EQ("(bvsub x1 x2 x3)", smtlib::bvsub({"x1", "x2", "x3"}));
ASSERT_EQ("(bvsub x1 x2 x3)", smtlib::bvsub("x1", "x2", "x3"));
}
// bvmul =======================================================================
TEST(smtlib, bvmul)
{
ASSERT_THROW(smtlib::bvmul({}), std::runtime_error);
ASSERT_THROW(smtlib::bvmul({"x1"}), std::runtime_error);
ASSERT_EQ("(bvmul x1 x2 x3)", smtlib::bvmul({"x1", "x2", "x3"}));
ASSERT_EQ("(bvmul x1 x2 x3)", smtlib::bvmul("x1", "x2", "x3"));
}
// select ======================================================================
......@@ -239,8 +214,6 @@ TEST(smtlib, declare_array_var)
TEST(smtlib, cardinality_exactly_one_naive)
{
ASSERT_THROW(smtlib::card_constraint_naive({}), std::runtime_error);
ASSERT_EQ("(assert x1)\n", smtlib::card_constraint_naive({"x1"}));
ASSERT_EQ(
......@@ -298,7 +271,7 @@ TEST(smtlib, cardinality_exactly_one_naive_verify)
for (size_t i = 0; i < vars.size() - 1; i++)
for (size_t j = i + 1; j < vars.size(); j++)
spec += smtlib::assertion(smtlib::land({vars[i], vars[j]})) + eol;
spec += smtlib::assertion(smtlib::land(vars[i], vars[j])) + eol;
spec += smtlib::check_sat() + eol;
......@@ -309,8 +282,6 @@ TEST(smtlib, cardinality_exactly_one_naive_verify)
TEST(smtlib, cardinality_exactly_one_sinz)
{
ASSERT_THROW(smtlib::card_constraint_sinz({}), std::runtime_error);
ASSERT_EQ("(assert x1)\n", smtlib::card_constraint_sinz({"x1"}));
ASSERT_EQ(
......@@ -384,7 +355,7 @@ TEST(smtlib, cardinality_exactly_one_sinz_verify)
for (size_t i = 0; i < vars.size() - 1; i++)
for (size_t j = i + 1; j < vars.size(); j++)
spec += smtlib::assertion(smtlib::land({vars[i], vars[j]})) + eol;
spec += smtlib::assertion(smtlib::land(vars[i], vars[j])) + eol;
spec += smtlib::check_sat() + eol;
......
This diff is collapsed.
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