Commit 0c5d1b99 authored by phlo's avatar phlo

added halt conditions to SMT encoders

parent 167b9651
......@@ -96,7 +96,7 @@ flags:
@echo $(CXXFLAGS)
# export compiler flags for sub-make
export CXX CXXFLAGS OBJ
export CXX CXXFLAGS LDFLAGS OBJ
# auto-dependency generation
include dependencies.mk
......
......@@ -15,6 +15,7 @@ const std::string Encoder::sb_val_sym = "sb-val";
const std::string Encoder::sb_full_sym = "sb-full";
const std::string Encoder::stmt_sym = "stmt";
const std::string Encoder::block_sym = "block";
const std::string Encoder::halt_sym = "halt";
const std::string Encoder::heap_sym = "heap";
const std::string Encoder::exit_flag_sym = "exit";
......@@ -32,6 +33,7 @@ const std::string Encoder::sb_val_comment = "store buffer value variables";
const std::string Encoder::sb_full_comment = "store buffer full variables";
const std::string Encoder::stmt_comment = "statement activation variables";
const std::string Encoder::block_comment = "blocking variables";
const std::string Encoder::halt_comment = "halt variables";
const std::string Encoder::heap_comment = "heap variable";
const std::string Encoder::exit_flag_comment = "exit flag variable";
......@@ -61,6 +63,10 @@ Encoder::Encoder (const Program::List::ptr & p, bound_t b) :
if (op.requires_flush())
flush_pcs[thread].push_back(pc);
// collect explicit halt statements
if (&op.symbol() == &Instruction::Halt::symbol)
halt_pcs[thread].push_back(pc);
// collect exit calls
if (&op.symbol() == &Instruction::Exit::symbol)
exit_pcs[thread].push_back(pc);
......@@ -74,6 +80,10 @@ Encoder::Encoder (const Program::List::ptr & p, bound_t b) :
lst.reserve(lst.size() + pcs.size());
lst.insert(lst.end(), pcs.begin(), pcs.end());
}
// collect final halt statement (excluding control operations)
if (!(program.back().type() & Instruction::Type::control))
halt_pcs[thread].push_back(pc - 1);
});
}
......
......@@ -46,6 +46,7 @@ struct Encoder
static const std::string sb_full_sym;
static const std::string stmt_sym;
static const std::string block_sym;
static const std::string halt_sym;
// machine state symbols
//
......@@ -69,6 +70,7 @@ struct Encoder
static const std::string sb_full_comment;
static const std::string stmt_comment;
static const std::string block_comment;
static const std::string halt_comment;
static const std::string exit_flag_comment;
static const std::string exit_code_comment;
......@@ -129,6 +131,12 @@ struct Encoder
//
std::map<word_t, std::map<word_t, std::vector<word_t>>> check_pcs; // checkpoints
// pcs of halt statements
//
// thread -> list of program counters
//
std::map<word_t, std::vector<word_t>> halt_pcs; // halts
// pcs of exit calls
//
// thread -> list of program counters
......@@ -258,6 +266,7 @@ struct Encoder : public ::Encoder
static const std::string sb_full_comment;
static const std::string stmt_comment;
static const std::string block_comment;
static const std::string halt_comment;
static const std::string exit_flag_comment;
static const std::string exit_code_comment;
......@@ -304,8 +313,9 @@ struct Encoder : public ::Encoder
std::string sb_full_var () const;
static std::string stmt_var (word_t step, word_t thread, word_t pc);
std::string stmt_var () const;
static std::string block_var (word_t step, word_t thread, word_t id);
static std::string halt_var (word_t step, word_t thread);
std::string halt_var () const;
// machine state variable name generators
//
......@@ -342,6 +352,7 @@ struct Encoder : public ::Encoder
void declare_sb_full ();
void declare_stmt ();
void declare_block ();
void declare_halt ();
void declare_heap ();
void declare_exit_flag ();
......@@ -367,6 +378,7 @@ struct Encoder : public ::Encoder
void init_sb_full ();
void init_stmt ();
void init_block ();
void init_halt ();
void init_exit_flag ();
......@@ -387,7 +399,8 @@ struct Encoder : public ::Encoder
//
void define_scheduling_constraints ();
void define_store_buffer_constraints ();
void define_checkpoint_contraints ();
void define_checkpoint_constraints ();
void define_halt_constraints ();
void define_constraints (); // all of the above
......@@ -453,6 +466,7 @@ struct Functional : public Encoder
void define_sb_full ();
void define_stmt ();
void define_block ();
void define_halt ();
void define_heap ();
void define_exit_flag ();
......@@ -486,6 +500,7 @@ struct Relational : public Encoder
std::shared_ptr<std::string> sb_full;
std::shared_ptr<std::string> stmt;
std::shared_ptr<std::string> block;
std::shared_ptr<std::string> halt;
std::shared_ptr<std::string> heap;
std::shared_ptr<std::string> exit_flag;
std::shared_ptr<std::string> exit_code;
......@@ -553,6 +568,9 @@ struct Relational : public Encoder
std::string reset_block (word_t id) const;
std::shared_ptr<std::string> restore_block () const;
std::shared_ptr<std::string> set_halt () const;
std::shared_ptr<std::string> restore_halt () const;
template <class T>
std::shared_ptr<std::string> set_heap (const T & op);
std::shared_ptr<std::string> restore_heap () const;
......@@ -647,6 +665,7 @@ struct Encoder : public ::Encoder
static const std::string sb_full_comment;
static const std::string stmt_comment;
static const std::string block_comment;
static const std::string halt_comment;
static const std::string exit_flag_comment;
static const std::string exit_code_comment;
......@@ -709,6 +728,18 @@ struct Encoder : public ::Encoder
//
std::map<word_t, std::map<word_t, std::string>> nids_block;
// halt state nodes
//
// thread -> nid
//
std::map<word_t, std::string> nids_halt;
// halt state definition nodes (as used in next)
//
// required in exit_flag definition: exit_flag and last halt set in same step
//
std::map<word_t, std::string> nids_halt_next;
// machine state nodes
//
std::string nid_heap;
......@@ -794,10 +825,11 @@ struct Encoder : public ::Encoder
std::string sb_val_var () const;
static std::string sb_full_var (word_t thread);
std::string sb_full_var () const;
static std::string stmt_var (word_t thread, word_t pc);
std::string stmt_var () const;
static std::string block_var (word_t thread, word_t id);
static std::string halt_var (word_t thread);
std::string halt_var () const;
// transition symbol generators
//
......@@ -838,6 +870,7 @@ struct Encoder : public ::Encoder
void declare_sb_full ();
void declare_stmt ();
void declare_block ();
void declare_halt ();
void declare_heap ();
void declare_exit_flag ();
......@@ -872,6 +905,7 @@ struct Encoder : public ::Encoder
void define_sb_full ();
void define_stmt ();
void define_block ();
void define_halt ();
void define_heap ();
void define_exit_flag ();
......@@ -884,6 +918,7 @@ struct Encoder : public ::Encoder
void define_scheduling_constraints ();
void define_store_buffer_constraints ();
void define_checkpoint_constraints ();
void define_halt_constraints ();
void define_constraints (); // all of the above
......
This diff is collapsed.
......@@ -51,6 +51,10 @@ const std::string Encoder::block_comment =
comment(
::Encoder::block_comment + " - " + block_sym + "_<step>_<id>_<thread>" + eol);
const std::string Encoder::halt_comment =
comment(
::Encoder::halt_comment + " - " + halt_sym + "_<step>_<thread>" + eol);
const std::string Encoder::heap_comment =
comment(
::Encoder::heap_comment + " - " + heap_sym + "_<step>" + eol);
......@@ -180,6 +184,18 @@ std::string Encoder::block_var (const word_t k,
std::to_string(tid);
}
// smtlib::Encoder::halt_var ---------------------------------------------------
std::string Encoder::halt_var (const word_t k, const word_t t)
{
return halt_sym + '_' + std::to_string(k) + '_' + std::to_string(t);
}
std::string Encoder::halt_var () const
{
return halt_var(step, thread);
}
// smtlib::Encoder::heap_var ---------------------------------------------------
std::string Encoder::heap_var (const word_t k)
......@@ -431,6 +447,22 @@ void Encoder::declare_block ()
formula << eol;
}
// smtlib::Encoder::declare_halt -----------------------------------------------
void Encoder::declare_halt ()
{
if (halt_pcs.empty())
return;
if (verbose)
formula << halt_comment;
for (const auto & it : halt_pcs)
formula << declare_bool_var(halt_var(step, it.first)) << eol;
formula << eol;
}
// smtlib::Encoder::declare_heap -----------------------------------------------
void Encoder::declare_heap ()
......@@ -447,7 +479,7 @@ void Encoder::declare_heap ()
void Encoder::declare_exit_flag ()
{
if (exit_pcs.empty())
if (halt_pcs.empty() && exit_pcs.empty())
return;
if (verbose)
......@@ -480,6 +512,7 @@ void Encoder::declare_states ()
declare_sb_full();
declare_stmt();
declare_block();
declare_halt();
declare_heap();
declare_exit_flag();
......@@ -656,11 +689,28 @@ void Encoder::init_block ()
formula << eol;
}
// smtlib::Encoder::init_halt --------------------------------------------------
void Encoder::init_halt ()
{
if (halt_pcs.empty())
return;
if (verbose)
formula << halt_comment;
iterate_threads([this] {
formula << assertion(lnot(halt_var())) << eol;
});
formula << eol;
}
// smtlib::Encoder::init_exit_flag ---------------------------------------------
void Encoder::init_exit_flag ()
{
if (exit_pcs.empty())
if (halt_pcs.empty() && exit_pcs.empty())
return;
if (verbose)
......@@ -685,6 +735,7 @@ void Encoder::init_states ()
init_sb_full();
init_stmt();
init_block();
init_halt();
init_exit_flag();
}
......@@ -766,7 +817,7 @@ void Encoder::define_scheduling_constraints ()
variables.push_back(flush_var());
});
if (!exit_pcs.empty())
if (!halt_pcs.empty() || !exit_pcs.empty())
variables.push_back(exit_flag_var());
formula
......@@ -780,9 +831,6 @@ void Encoder::define_scheduling_constraints ()
void Encoder::define_store_buffer_constraints ()
{
if (flush_pcs.empty())
return;
if (verbose)
formula << comment_subsection("store buffer constraints");
......@@ -823,9 +871,9 @@ void Encoder::define_store_buffer_constraints ()
formula << eol;
}
// smtlib::Encoder::define_checkpoint_contraints -------------------------------
// smtlib::Encoder::define_checkpoint_constraints ------------------------------
void Encoder::define_checkpoint_contraints ()
void Encoder::define_checkpoint_constraints ()
{
if (check_pcs.empty())
return;
......@@ -853,13 +901,35 @@ void Encoder::define_checkpoint_contraints ()
formula << eol;
}
// smtlib::Encoder::define_halt_constraints ------------------------------------
void Encoder::define_halt_constraints ()
{
if (halt_pcs.empty())
return;
if (verbose)
formula << comment_subsection("halt constraints");
for (const auto & it : halt_pcs)
formula <<
assertion(
implication(
halt_var(step, it.first),
lnot(thread_var(step, it.first)))) <<
eol;
formula << eol;
}
// smtlib::Encoder::define_constraints -----------------------------------------
void Encoder::define_constraints ()
{
define_scheduling_constraints();
define_store_buffer_constraints();
define_checkpoint_contraints();
define_checkpoint_constraints();
define_halt_constraints();
}
// smtlib::Encoder::encode -----------------------------------------------------
......
......@@ -178,14 +178,14 @@ void Functional::define_block ()
for (const auto & [c, threads] : check_pcs)
for (const auto & [t, pcs] : threads)
{
std::vector<std::string> block_args;
std::vector<std::string> args;
block_args.reserve(pcs.size() + 1);
args.reserve(pcs.size() + 1);
for (const word_t p : pcs)
block_args.push_back(exec_var(prev, t, p));
args.push_back(exec_var(prev, t, p));
block_args.push_back(block_var(prev, c, t));
args.push_back(block_var(prev, c, t));
formula <<
assign(
......@@ -193,13 +193,39 @@ void Functional::define_block ()
ite(
check_var(prev, c),
FALSE,
lor(block_args))) <<
lor(args))) <<
eol;
}
formula << eol;
}
// smtlib::Functional::define_halt ---------------------------------------------
void Functional::define_halt ()
{
if (halt_pcs.empty())
return;
if (verbose)
formula << halt_comment;
for (const auto & [t, pcs] : halt_pcs)
{
std::vector<std::string> args;
args.reserve(pcs.size() + 1);
for (const word_t p : pcs)
args.push_back(exec_var(prev, t, p));
args.push_back(halt_var(prev, t));
formula << assign(halt_var(step, t), lor(args)) << eol;
}
formula << eol;
}
// smtlib::Functional::define_heap ---------------------------------------------
void Functional::define_heap ()
......@@ -236,11 +262,11 @@ void Functional::define_heap ()
formula << assign(heap_var(), expr) << eol << eol;
}
// smtlib::Functional::define_exit_code ----------------------------------------
// smtlib::Functional::define_exit_flag ----------------------------------------
void Functional::define_exit_flag ()
{
if (exit_pcs.empty())
if (halt_pcs.empty() && exit_pcs.empty())
return;
if (verbose)
......@@ -248,15 +274,26 @@ void Functional::define_exit_flag ()
std::vector<std::string> args {exit_flag_var(prev)};
iterate_threads([this, &args] {
for (const word_t & exit_pc : exit_pcs[thread])
args.push_back(exec_var(prev, thread, exit_pc));
});
if (!halt_pcs.empty())
{
std::vector<std::string> halt;
halt.reserve(halt_pcs.size());
for (const auto & it : halt_pcs)
halt.push_back(halt_var(step, it.first));
args.push_back(land(halt));
}
if (!exit_pcs.empty())
for (const auto & [t, pcs] : exit_pcs)
for (const word_t p : pcs)
args.push_back(exec_var(prev, t, p));
formula << assign(exit_flag_var(), lor(args)) << eol << eol;
}
// smtlib::Functional::define_exit_flag ----------------------------------------
// smtlib::Functional::define_exit_code ----------------------------------------
void Functional::define_exit_code ()
{
......@@ -295,6 +332,7 @@ void Functional::define_states ()
define_sb_full();
define_stmt();
define_block();
define_halt();
define_heap();
define_exit_flag();
......
......@@ -21,6 +21,7 @@ Relational::State::State (Relational & e) :
sb_val(e.restore_sb_val()),
sb_full(e.restore_sb_full()),
block(e.restore_block()),
halt(e.restore_halt()),
heap(e.restore_heap()),
exit_flag(e.unset_exit_flag())
{
......@@ -52,6 +53,9 @@ Relational::State::operator std::string () const
if (block)
args.push_back(*block);
if (halt)
args.push_back(*halt);
if (heap)
args.push_back(*heap);
......@@ -338,6 +342,40 @@ std::shared_ptr<std::string> Relational::restore_block () const
return std::make_shared<std::string>(land(block_vars));
}
// smtlib::Relational::set_halt ------------------------------------------------
std::shared_ptr<std::string> Relational::set_halt () const
{
if (halt_pcs.empty())
return {};
std::vector<std::string> args;
args.reserve(halt_pcs.size());
for (const auto & it : halt_pcs)
args.push_back(halt_var(step, it.first));
return
std::make_shared<std::string>(
land({
halt_var(),
implication(
land(args),
exit_flag_var())}));
}
// smtlib::Relational::restore_halt --------------------------------------------
std::shared_ptr<std::string> Relational::restore_halt () const
{
if (halt_pcs.empty())
return {};
return
std::make_shared<std::string>(
equality({halt_var(), halt_var(prev, thread)}));
}
// smtlib::Relational::set_heap ------------------------------------------------
template <class T>
......@@ -361,7 +399,7 @@ std::shared_ptr<std::string> Relational::restore_heap () const
std::shared_ptr<std::string> Relational::set_exit_flag () const
{
if (exit_pcs.empty())
if (halt_pcs.empty() && exit_pcs.empty())
return {};
return std::make_shared<std::string>(exit_flag_var());
......@@ -371,7 +409,7 @@ std::shared_ptr<std::string> Relational::set_exit_flag () const
std::shared_ptr<std::string> Relational::unset_exit_flag () const
{
if (exit_pcs.empty())
if (halt_pcs.empty() && exit_pcs.empty())
return {};
return std::make_shared<std::string>(lnot(exit_flag_var()));
......@@ -389,7 +427,7 @@ std::shared_ptr<std::string> Relational::set_exit_code (const word_t e) const
// thread t executed an instruction (exec_k_t_pc):
// * update thread state accordingly
// * restore heap (or update iff the instruction was a successful CAS)
// * unset exit flag
// * unset exit flag iff the instruction was neither an EXIT, nor a HALT
// * set exit code iff the instruction was an EXIT
void Relational::imply_thread_executed ()
......@@ -398,9 +436,18 @@ void Relational::imply_thread_executed ()
const State tmp = state = *this;
for (pc = 0; pc < program.size(); pc++, state = tmp)
formula
<< imply(exec_var(prev, thread, pc), program[pc].encode(*this))
<< eol;
{
// halts (final statement)
if (halt_pcs.find(thread) != halt_pcs.end() && pc == halt_pcs[thread].back())
{
state.halt = set_halt();
state.exit_flag = {};
}
formula
<< imply(exec_var(prev, thread, pc), program[pc].encode(*this))
<< eol;
}
}
// smtlib::Relational::imply_thread_not_executed -------------------------------
......@@ -451,7 +498,7 @@ void Relational::imply_thread_flushed ()
void Relational::imply_machine_exited ()
{
if (exit_pcs.empty())
if (halt_pcs.empty() && exit_pcs.empty())
return;
if (verbose)
......@@ -649,10 +696,12 @@ std::string Relational::encode (const Instruction::Check & c)
return state;
}
// TODO
std::string Relational::encode (const Instruction::Halt & h [[maybe_unused]])
{
throw std::runtime_error("not implemented");
state.halt = set_halt();
state.exit_flag = {};
return state;
}
std::string Relational::encode (const Instruction::Exit & e)
......
......@@ -153,9 +153,9 @@ struct Instruction
DECLARE_MEMORY (Mem, Load, "MEM", accu | mem | read)
DECLARE_MEMORY (Cas, Store, "CAS", accu | read | atomic | barrier)
DECLARE_UNARY (Check, Unary, "CHECK", control)
DECLARE_UNARY (Check, Unary, "CHECK", none)
DECLARE_NULLARY (Halt, Nullary, "HALT", control)
DECLARE_NULLARY (Halt, Nullary, "HALT", barrier | control)
DECLARE_UNARY (Exit, Unary, "EXIT", control)
// abstract interface (types erasure concept) --------------------------------
......
......@@ -3,6 +3,13 @@
# - CXXFLAGS
# - OBJ
# link std::filesystem
ifeq ($(CXX),g++)
LDFLAGS += -lstdc++fs
else
LDFLAGS += -lc++fs
endif
# googletest root
GTEST_DIR = lib/googletest/googletest
......@@ -43,7 +50,7 @@ GTEST_FILTER += smtlib_Functional.*
GTEST_FILTER += smtlib_Relational.*
GTEST_FILTER += btor2.*
GTEST_FILTER += btor2_Encoder.*
# GTEST_FILTER += Thread.*
GTEST_FILTER += Thread.*
# GTEST_FILTER += Simulator.*
# GTEST_FILTER += Main.*
# GTEST_FILTER += Experimental.*
......@@ -93,7 +100,7 @@ experimental: $(EXPERIMENTS) $(GTEST_LIB)
# build executable containing all test cases
$(TEST_RUN): $(GTEST_LIB) $(OBJ) $(TEST_OBJ)
$(CXX) $(CXXFLAGS) $^ $(TEST_MAIN) -o $@
$(CXX) $(CXXFLAGS) $^ $(TEST_MAIN) $(LDFLAGS) -o $@
# build googletest library
$(GTEST_DIR):
......
This diff is collapsed.
......@@ -343,11 +343,11 @@
233 or 1 24 232
234 implies 1 233 -42
235 ite 1 17 234 -44
236 constraint 235
236 constraint 235 flush_0
237 implies 1 32 -43
238 ite 1 18 237 -45
239 constraint 238
239 constraint 238 flush_1
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; checkpoint constraints
......
......@@ -34,6 +34,8 @@ TEST_F(Encoder, constructor)
id == 1 ? std::vector<word_t>({3}) : std::vector<word_t>({5}),
std::get<1>(pcs));
ASSERT_TRUE(encoder->halt_pcs.empty());
for (const auto & [thread, pcs] : encoder->exit_pcs)
{
ASSERT_TRUE(!thread || thread < 3);
......@@ -78,6 +80,26 @@ TEST_F(Encoder, constructor_check_pcs)
}
}
TEST_F(Encoder, constructor_halt_pcs)
{
for (size_t i = 0; i < 2; i++)
{
if (i)
programs.push_back(create_program("ADDI 1\n"));
else
programs.push_back(create_program(
"JZ 2\n"
"HALT\n"
"ADDI 1\n"
));
}
reset_encoder();
ASSERT_EQ(std::vector<word_t>({1, 2}), encoder->halt_pcs[0]);
ASSERT_EQ(std::vector<word_t>({0}), encoder->halt_pcs[1]);
}
TEST_F(Encoder, constructor_exit_pcs)
{
for (size_t i = 0; i < 3; i++)
......
......@@ -79,19 +79,18 @@ struct Encoder: public ::testing::Test
void encode (const std::initializer_list<std::string> _programs,
const std::string file,
const bound_t bound)
const bound_t bound,
const char * dir = "data/")
{
const char * data = "data/";
for (const auto & p : _programs)
programs.push_back(create_from_file<Program>(data + p));
programs.push_back(create_from_file<Program>(dir + p));
encoder =
std::make_unique<Impl>(
std::make_shared<Program::List>(programs),
bound);
std::ifstream ifs(data + file);
std::ifstream ifs(dir + file);
std::string expected;
expected.assign(std::istreambuf_iterator<char>(ifs),
......
#include "test_encoder.hh"
#include <filesystem>
#include <functional>
#include "btor2.hh"
......@@ -682,6 +683,53 @@ TEST_F(btor2_Encoder, declare_block_empty)
ASSERT_EQ("", encoder->str());
}
// btor2::Encoder::declare_halt ================================================
TEST_F(btor2_Encoder, declare_halt)
{
add_dummy_programs(3);
reset_encoder();
init_declarations();