Commit b44bed29 authored by phlo's avatar phlo

added memory map support to encoders

parent c89ed040
......@@ -50,9 +50,12 @@ const std::string Encoder::check_comment = "checkpoint variables";
// constructors
//------------------------------------------------------------------------------
Encoder::Encoder (const Program::List::ptr & p, size_t b) :
Encoder::Encoder (const Program::List::ptr & p,
const std::shared_ptr<MMap> & m,
size_t b) :
programs(p),
num_threads(p->size()),
mmap(m),
bound(b),
use_sinz_constraint(num_threads > 4)
{
......
......@@ -10,6 +10,12 @@
namespace ConcuBinE {
//==============================================================================
// forward declarations
//==============================================================================
class MMap;
//==============================================================================
// Encoder base class
//
......@@ -97,6 +103,10 @@ struct Encoder
//
const size_t num_threads;
// reference to initial memory layout
//
std::shared_ptr<MMap> mmap;
// bound
//
const size_t bound;
......@@ -149,7 +159,9 @@ struct Encoder
// constructors
//----------------------------------------------------------------------------
Encoder (const Program::List::ptr & programs, size_t bound);
Encoder (const Program::List::ptr & programs,
const std::shared_ptr<MMap> & mmap,
size_t bound);
//----------------------------------------------------------------------------
// private member functions
......@@ -295,7 +307,9 @@ struct Encoder : public ConcuBinE::Encoder
// constructors
//----------------------------------------------------------------------------
Encoder (const Program::List::ptr & programs, size_t bound);
Encoder (const Program::List::ptr & programs,
const std::shared_ptr<MMap> & mmap,
size_t bound);
//----------------------------------------------------------------------------
// private member functions
......@@ -382,6 +396,7 @@ struct Encoder : public ConcuBinE::Encoder
void init_block ();
void init_halt ();
void init_heap ();
void init_exit_flag ();
void init_states (); // all of the above
......@@ -803,7 +818,9 @@ struct Encoder : public ConcuBinE::Encoder
// constructors
//----------------------------------------------------------------------------
Encoder (const Program::List::ptr & programs, size_t bound);
Encoder (const Program::List::ptr & programs,
const std::shared_ptr<MMap> & mmap,
size_t bound);
//----------------------------------------------------------------------------
// private member functions
......
......@@ -4,6 +4,7 @@
#include <cassert>
#include "btor2.hh"
#include "mmap.hh"
namespace ConcuBinE::btor2 {
......@@ -163,8 +164,10 @@ const std::string Encoder::msb = std::to_string(word_size - 1);
// constructors
//------------------------------------------------------------------------------
Encoder::Encoder (const Program::List::ptr & p, const size_t b) :
ConcuBinE::Encoder(p, b),
Encoder::Encoder (const Program::List::ptr & p,
const std::shared_ptr<MMap> & m,
const size_t b) :
ConcuBinE::Encoder(p, m, b),
node(1)
{
// collect constants
......@@ -176,6 +179,10 @@ Encoder::Encoder (const Program::List::ptr & p, const size_t b) :
if (program[pc].is_unary())
nids_const[program[pc].arg()];
});
if (mmap && !mmap->empty())
for (const auto & [adr, val] : *mmap)
nids_const[adr] = nids_const[val];
}
//------------------------------------------------------------------------------
......@@ -1242,6 +1249,26 @@ void Encoder::define_heap ()
if (verbose)
formula << heap_comment;
// init
if (mmap && !mmap->empty())
{
std::string nid_init = nid();
formula << state(nid_init, sid_heap, "mmap");
for (const auto & [adr, val] : *mmap)
formula <<
write(
nid_init = nid(),
sid_heap,
nid_init,
nids_const[adr],
nids_const[val]);
formula << init(nid(), sid_heap, nid_heap, nid_init);
}
// next
update = State::heap;
std::string nid_next = nid_heap;
......
......@@ -2,6 +2,7 @@
#include <cassert>
#include "mmap.hh"
#include "smtlib.hh"
namespace ConcuBinE::smtlib {
......@@ -143,8 +144,10 @@ const std::string Encoder::check_comment =
// constructors
//------------------------------------------------------------------------------
Encoder::Encoder (const Program::List::ptr & p, const size_t b) :
ConcuBinE::Encoder(p, b),
Encoder::Encoder (const Program::List::ptr & p,
const std::shared_ptr<MMap> & m,
const size_t b) :
ConcuBinE::Encoder(p, m, b),
step(0)
{}
......@@ -763,6 +766,22 @@ void Encoder::init_halt ()
formula << eol;
}
// smtlib::Encoder::init_heap --------------------------------------------------
void Encoder::init_heap ()
{
if (!mmap || mmap->empty())
return;
if (verbose)
formula << heap_comment;
for (const auto & [adr, val] : *mmap)
formula << assign(select(heap_var(), word2hex(adr)), word2hex(val)) << eol;
formula << eol;
}
// smtlib::Encoder::init_exit_flag ---------------------------------------------
void Encoder::init_exit_flag ()
......@@ -793,6 +812,8 @@ void Encoder::init_states ()
init_stmt();
init_block();
init_halt();
init_heap();
init_exit_flag();
}
......
......@@ -396,15 +396,18 @@ int solve (const char * name, const int argc, const char ** argv)
while (i < argc)
programs->push_back(create_from_file<Program>(argv[i++]));
// memory map
std::shared_ptr<MMap> mmap;
// encode program
std::unique_ptr<Encoder> encoder;
if (encoder_name == "smtlib-functional")
encoder = std::make_unique<smtlib::Functional>(programs, bound);
encoder = std::make_unique<smtlib::Functional>(programs, mmap, bound);
else if (encoder_name == "smtlib-relational")
encoder = std::make_unique<smtlib::Relational>(programs, bound);
encoder = std::make_unique<smtlib::Relational>(programs, mmap, bound);
else if (encoder_name == "btor2")
encoder = std::make_unique<btor2::Encoder>(programs, bound);
encoder = std::make_unique<btor2::Encoder>(programs, mmap, bound);
else
{
print_error("unknown encoder [" + encoder_name + "]");
......
......@@ -45,25 +45,25 @@ TEST_RUN := run_all_tests
GTEST_FILTER = --gtest_filter=
# GTEST_FILTER += "*"
GTEST_FILTER += Encoder.*
GTEST_FILTER += smtlib.*
# GTEST_FILTER += Encoder.*
# GTEST_FILTER += smtlib.*
GTEST_FILTER += smtlib_Encoder.*
GTEST_FILTER += smtlib_Functional.*
GTEST_FILTER += smtlib_Relational.*
GTEST_FILTER += btor2.*
# GTEST_FILTER += smtlib_Functional.*
# 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 += Shell.*
GTEST_FILTER += Boolector.*
GTEST_FILTER += BtorMC.*
GTEST_FILTER += Z3.*
GTEST_FILTER += CVC4.*
# GTEST_FILTER += Instruction.*
# GTEST_FILTER += Program.*
# GTEST_FILTER += Trace.*
# GTEST_FILTER += MMap.*
# GTEST_FILTER += Shell.*
# GTEST_FILTER += Boolector.*
# GTEST_FILTER += BtorMC.*
# GTEST_FILTER += Z3.*
# GTEST_FILTER += CVC4.*
GTEST_FILTER := $(shell echo ${GTEST_FILTER} | sed -e 's/ /:/g')
......
......@@ -42,7 +42,7 @@ TEST_F(Boolector, solve_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, 16);
encoder = std::make_unique<smtlib::Functional>(programs, nullptr, 16);
trace = boolector.solve(*encoder);
......@@ -67,7 +67,7 @@ TEST_F(Boolector, solve_cas)
programs->push_back(create_from_file<Program>(increment));
programs->push_back(create_from_file<Program>(increment));
encoder = std::make_unique<smtlib::Functional>(programs, 16);
encoder = std::make_unique<smtlib::Functional>(programs, nullptr, 16);
trace = boolector.solve(*encoder);
......@@ -98,7 +98,7 @@ TEST_F(Boolector, solve_indirect_uninitialized)
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);
encoder = std::make_unique<smtlib::Functional>(programs, nullptr, 16);
trace = boolector.solve(*encoder);
......@@ -125,7 +125,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, 16);
encoder = std::make_unique<smtlib::Functional>(programs, nullptr, 16);
std::string formula = boolector.build_formula(*encoder, "");
......@@ -147,7 +147,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, 16);
encoder = std::make_unique<smtlib::Functional>(programs, nullptr, 16);
std::string formula = boolector.build_formula(*encoder, "");
......
......@@ -54,7 +54,7 @@ TEST_F(BtorMC, solve_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, 16);
encoder = std::make_unique<btor2::Encoder>(programs, nullptr, 16);
trace = btormc.solve(*encoder);
......@@ -79,7 +79,7 @@ TEST_F(BtorMC, solve_cas)
programs->push_back(create_from_file<Program>(increment));
programs->push_back(create_from_file<Program>(increment));
encoder = std::make_unique<btor2::Encoder>(programs, 16);
encoder = std::make_unique<btor2::Encoder>(programs, nullptr, 16);
trace = btormc.solve(*encoder);
......@@ -110,7 +110,7 @@ TEST_F(BtorMC, solve_indirect_uninitialized)
programs->push_back(Program(p0, "load.store.0.asm"));
programs->push_back(Program(p1, "load.store.1.asm"));
encoder = std::make_unique<btor2::Encoder>(programs, 16);
encoder = std::make_unique<btor2::Encoder>(programs, nullptr, 16);
trace = btormc.solve(*encoder);
......@@ -137,7 +137,7 @@ 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, 16);
encoder = std::make_unique<btor2::Encoder>(programs, nullptr, 16);
std::string formula = btormc.build_formula(*encoder, "");
......@@ -159,7 +159,7 @@ 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, 16);
encoder = std::make_unique<btor2::Encoder>(programs, nullptr, 16);
std::string formula = btormc.build_formula(*encoder, "");
......
......@@ -42,7 +42,7 @@ TEST_F(CVC4, solve_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, 16);
encoder = std::make_unique<smtlib::Functional>(programs, nullptr, 16);
trace = cvc4.solve(*encoder);
......@@ -65,7 +65,7 @@ TEST_F(CVC4, solve_cas)
programs->push_back(create_from_file<Program>(increment));
programs->push_back(create_from_file<Program>(increment));
encoder = std::make_unique<smtlib::Functional>(programs, 16);
encoder = std::make_unique<smtlib::Functional>(programs, nullptr, 16);
trace = cvc4.solve(*encoder);
......@@ -96,7 +96,7 @@ TEST_F(CVC4, solve_indirect_uninitialized)
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);
encoder = std::make_unique<smtlib::Functional>(programs, nullptr, 16);
trace = cvc4.solve(*encoder);
......@@ -122,7 +122,7 @@ TEST_F(CVC4, 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, 16);
encoder = std::make_unique<smtlib::Functional>(programs, nullptr, 16);
bool sat = cvc4.sat(cvc4.build_formula(*encoder, constraints));
......@@ -141,7 +141,7 @@ TEST_F(CVC4, 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, 16);
encoder = std::make_unique<smtlib::Functional>(programs, nullptr, 16);
bool sat = cvc4.sat(cvc4.build_formula(*encoder, constraints));
......
#include <gtest/gtest.h>
#include "encoder.hh"
#include "mmap.hh"
#include "parser.hh"
namespace ConcuBinE::test::encoder {
......@@ -12,6 +13,7 @@ struct Encoder: public ::testing::Test
using Type = Instruction::Type;
Program::List programs;
MMap mmap;
std::unique_ptr<E> encoder = create_encoder();
virtual std::unique_ptr<E> init_encoder (std::unique_ptr<E> e)
......@@ -25,6 +27,7 @@ struct Encoder: public ::testing::Test
init_encoder(
std::make_unique<Impl>(
std::make_shared<Program::List>(programs),
std::make_shared<MMap>(mmap),
bound));
}
......@@ -87,6 +90,7 @@ struct Encoder: public ::testing::Test
encoder =
std::make_unique<Impl>(
std::make_shared<Program::List>(programs),
std::make_shared<MMap>(mmap),
bound);
std::ifstream ifs(dir + file);
......
......@@ -2771,6 +2771,97 @@ TEST_F(btor2_Encoder, define_heap)
verbose = true;
}
TEST_F(btor2_Encoder, define_heap_mmap)
{
mmap[0] = mmap[1];
reset_encoder();
init_state_definitions();
btor2::nid_t nid = encoder->node;
encoder->define_heap();
expected = [this, &nid] {
std::ostringstream s;
if (verbose)
s << encoder->heap_comment;
std::string nid_init = std::to_string(nid++);
s << btor2::state(nid_init, encoder->sid_heap, "mmap");
for (const auto & [adr, val] : *encoder->mmap)
s <<
btor2::write(
nid_init = std::to_string(nid++),
encoder->sid_heap,
nid_init,
encoder->nids_const[adr],
encoder->nids_const[val]);
s <<
btor2::init(
std::to_string(nid++),
encoder->sid_heap,
encoder->nid_heap,
nid_init);
s <<
btor2::next(
std::to_string(nid++),
encoder->sid_heap,
encoder->nid_heap,
encoder->nid_heap,
encoder->heap_sym);
s << eol;
return s.str();
};
ASSERT_EQ(expected(), encoder->str());
// verbosity
reset_encoder();
init_state_definitions();
verbose = false;
nid = encoder->node;
encoder->define_heap();
ASSERT_EQ(expected(), encoder->str());
verbose = true;
}
TEST_F(btor2_Encoder, define_heap_mmap_empty)
{
expected = [this] {
std::ostringstream s;
if (verbose)
s << encoder->heap_comment;
s <<
btor2::next(
std::to_string(encoder->node - 1),
encoder->sid_heap,
encoder->nid_heap,
encoder->nid_heap,
encoder->heap_sym) <<
eol;
return s.str();
};
init_state_definitions();
encoder->define_heap();
ASSERT_EQ(expected(), encoder->str());
reset_encoder();
init_state_definitions();
encoder->mmap.reset();
encoder->define_heap();
ASSERT_EQ(expected(), encoder->str());
}
// btor2::Encoder::define_exit_flag ============================================
TEST_F(btor2_Encoder, define_exit_flag)
......
......@@ -1196,6 +1196,46 @@ TEST_F(smtlib_Encoder, init_halt_empty)
ASSERT_EQ("", encoder->formula.str());
}
// smtlib::Encoder::init_heap ==================================================
TEST_F(smtlib_Encoder, init_heap)
{
mmap[0] = mmap[1] = 1;
reset_encoder(0);
encoder->init_heap();
ASSERT_EQ(
"; heap variable - heap_<step>\n"
"(assert (= (select heap_0 #x0000) #x0001))\n"
"(assert (= (select heap_0 #x0001) #x0001))\n"
"\n",
encoder->str());
// verbosity
reset_encoder(0);
verbose = false;
encoder->init_heap();
verbose = true;
ASSERT_EQ(
"(assert (= (select heap_0 #x0000) #x0001))\n"
"(assert (= (select heap_0 #x0001) #x0001))\n"
"\n",
encoder->str());
}
TEST_F(smtlib_Encoder, init_heap_empty)
{
encoder->init_heap();
ASSERT_EQ("", encoder->formula.str());
encoder->mmap.reset();
encoder->init_heap();
ASSERT_EQ("", encoder->formula.str());
}
// smtlib::Encoder::init_exit_flag =============================================
TEST_F(smtlib_Encoder, init_exit_flag)
......
......@@ -41,7 +41,7 @@ TEST_F(Z3, solve_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, 16);
encoder = std::make_unique<smtlib::Functional>(programs, nullptr, 16);
trace = z3.solve(*encoder, constraints);
......@@ -67,7 +67,7 @@ TEST_F(Z3, solve_cas)
programs->push_back(create_from_file<Program>(increment));
programs->push_back(create_from_file<Program>(increment));
encoder = std::make_unique<smtlib::Functional>(programs, 16);
encoder = std::make_unique<smtlib::Functional>(programs, nullptr, 16);
trace = z3.solve(*encoder, constraints);
......@@ -98,7 +98,7 @@ TEST_F(Z3, solve_indirect_uninitialized)
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);
encoder = std::make_unique<smtlib::Functional>(programs, nullptr, 16);
trace = z3.solve(*encoder);
......
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