Commit 06d83aa9 authored by phlo's avatar phlo

fixed halting mechanism

parent b5ae6c9d
......@@ -786,12 +786,14 @@ void Encoder::declare_halt ()
if (verbose)
formula << halt_comment;
for (const auto & it : halts)
formula <<
state(
nids_halt.emplace_hint(nids_halt.end(), it.first, nid())->second,
sid_bool,
halt_var(it.first));
iterate_threads([this]
{
formula <<
state(
nids_halt.emplace_hint(nids_halt.end(), thread, nid())->second,
sid_bool,
halt_var(thread));
});
formula << eol;
}
......@@ -1223,27 +1225,46 @@ void Encoder::define_halt ()
if (verbose)
formula << halt_comment;
for (const auto & [t, pcs] : halts)
iterate_threads([this]
{
std::vector<std::string> args;
args.reserve(pcs.size() + 1);
const auto & nid_halt = nids_halt[thread];
for (const word_t p : pcs)
args.push_back(nids_exec[t][p]);
formula << init(nid(), sid_bool, nid_halt, nid_false);
std::string nid_next;
if (halts.find(thread) != halts.end())
{
const auto & pcs = halts[thread];
std::vector<std::string> args;
args.reserve(pcs.size() + 1);
for (const word_t p : pcs)
args.push_back(nids_exec[thread][p]);
args.push_back(nid_halt);
formula << lor(node, sid_bool, args);
args.push_back(nids_halt[t]);
nid_next = nid(-1);
}
else
{
nid_next = nid_halt;
}
formula <<
init(nid(), sid_bool, nids_halt[t], nid_false) <<
lor(node, sid_bool, args) <<
next(
nid(),
sid_bool,
nids_halt[t],
nids_halt_next.emplace_hint(nids_halt_next.end(), t, nid(-1))->second,
halt_var(t)) <<
nid_halt,
nids_halt_next.emplace_hint(
nids_halt_next.end(),
thread,
nid_next)->second,
halt_var(thread)) <<
eol;
}
});
}
// btor2::Encoder::define_heap -------------------------------------------------
......
......@@ -736,8 +736,7 @@ void Encoder::declare_halt ()
if (verbose)
formula << halt_comment;
for (const auto & it : halts)
formula << declare_bool_var(halt_var(step, it.first)) << eol;
iterate_threads([this] { formula << declare_bool_var(halt_var()) << eol; });
formula << eol;
}
......@@ -982,8 +981,7 @@ void Encoder::init_halt ()
if (verbose)
formula << halt_comment;
for (const auto & it : halts)
formula << assertion(lnot(halt_var(step, it.first))) << eol;
iterate_threads([this] { formula << assertion(lnot(halt_var())) << eol; });
formula << eol;
}
......
......@@ -213,18 +213,26 @@ void Functional::define_halt ()
if (verbose)
formula << halt_comment;
for (const auto & [t, pcs] : halts)
iterate_threads([this]
{
std::vector<std::string> args;
args.reserve(pcs.size() + 1);
if (halts.find(thread) != halts.end())
{
const auto & pcs = halts[thread];
std::vector<std::string> args;
args.reserve(pcs.size() + 1);
for (const word_t p : pcs)
args.push_back(exec_var(prev, t, p));
for (const word_t p : pcs)
args.push_back(exec_var(prev, thread, p));
args.push_back(halt_var(prev, t));
args.push_back(halt_var(prev, thread));
formula << assign(halt_var(step, t), lor(args)) << eol;
}
formula << assign(halt_var(), lor(args)) << eol;
}
else
{
formula << assign(halt_var(), FALSE) << eol;
}
});
formula << eol;
}
......@@ -280,11 +288,8 @@ void Functional::define_exit_flag ()
if (!halts.empty())
{
std::vector<std::string> halt;
halt.reserve(halts.size());
for (const auto & it : halts)
halt.push_back(halt_var(step, it.first));
halt.reserve(num_threads);
iterate_threads([this, &halt] { halt.push_back(halt_var()); });
args.push_back(land(halt));
}
......@@ -306,15 +311,16 @@ void Functional::define_exit_code ()
std::string expr = word2hex(0);
if (!exits.empty())
for (size_t k = step = bound; k > 0; k--)
iterate_programs_reverse([this, &expr, k] (const Program & program) {
for (const word_t & exit_pc : exits[thread])
expr =
ite(
exec_var(k, thread, exit_pc),
program[exit_pc].encode(*this),
expr);
});
for (size_t k = 0; k <= bound; k++)
iterate_programs_reverse([this, &expr, k] (const Program & program)
{
for (const word_t & exit_pc : exits[thread])
expr =
ite(
exec_var(k, thread, exit_pc),
program[exit_pc].encode(*this),
expr);
});
formula << assign(exit_code_var, expr) << eol << eol;
}
......
......@@ -281,9 +281,11 @@ std::shared_ptr<std::string> Relational::set_halt () const
args.reserve(halts.size());
for (const auto & it : halts)
if (thread != it.first)
args.push_back(halt_var(step, it.first));
if (!halts.empty())
// do not alter thread variable
for (word_t t = 0; t < num_threads; t++)
if (t != thread)
args.push_back(halt_var(step, t));
return
std::make_shared<std::string>(
......@@ -311,7 +313,7 @@ std::shared_ptr<std::string> Relational::set_halt () const
std::shared_ptr<std::string> Relational::restore_halt () const
{
if (halts.find(thread) != halts.end())
if (!halts.empty())
return
std::make_shared<std::string>(
equality(halt_var(), halt_var(prev, thread)));
......
This diff is collapsed.
This diff is collapsed.
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -1544,5 +1544,5 @@
; exit code
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(assert (= exit-code (ite exec_1_0_2 #x0001 (ite exec_1_1_2 #x0001 (ite exec_2_0_2 #x0001 (ite exec_2_1_2 #x0001 (ite exec_3_0_2 #x0001 (ite exec_3_1_2 #x0001 (ite exec_4_0_2 #x0001 (ite exec_4_1_2 #x0001 (ite exec_5_0_2 #x0001 (ite exec_5_1_2 #x0001 (ite exec_6_0_2 #x0001 (ite exec_6_1_2 #x0001 (ite exec_7_0_2 #x0001 (ite exec_7_1_2 #x0001 (ite exec_8_0_2 #x0001 (ite exec_8_1_2 #x0001 (ite exec_9_0_2 #x0001 (ite exec_9_1_2 #x0001 (ite exec_10_0_2 #x0001 (ite exec_10_1_2 #x0001 #x0000))))))))))))))))))))))
(assert (= exit-code (ite exec_10_0_2 #x0001 (ite exec_10_1_2 #x0001 (ite exec_9_0_2 #x0001 (ite exec_9_1_2 #x0001 (ite exec_8_0_2 #x0001 (ite exec_8_1_2 #x0001 (ite exec_7_0_2 #x0001 (ite exec_7_1_2 #x0001 (ite exec_6_0_2 #x0001 (ite exec_6_1_2 #x0001 (ite exec_5_0_2 #x0001 (ite exec_5_1_2 #x0001 (ite exec_4_0_2 #x0001 (ite exec_4_1_2 #x0001 (ite exec_3_0_2 #x0001 (ite exec_3_1_2 #x0001 (ite exec_2_0_2 #x0001 (ite exec_2_1_2 #x0001 (ite exec_1_0_2 #x0001 (ite exec_1_1_2 #x0001 (ite exec_0_0_2 #x0001 (ite exec_0_1_2 #x0001 #x0000))))))))))))))))))))))))
......@@ -3353,5 +3353,5 @@
; exit code
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(assert (= exit-code (ite exec_1_0_8 #x0001 (ite exec_1_1_6 #x0001 (ite exec_2_0_8 #x0001 (ite exec_2_1_6 #x0001 (ite exec_3_0_8 #x0001 (ite exec_3_1_6 #x0001 (ite exec_4_0_8 #x0001 (ite exec_4_1_6 #x0001 (ite exec_5_0_8 #x0001 (ite exec_5_1_6 #x0001 (ite exec_6_0_8 #x0001 (ite exec_6_1_6 #x0001 (ite exec_7_0_8 #x0001 (ite exec_7_1_6 #x0001 (ite exec_8_0_8 #x0001 (ite exec_8_1_6 #x0001 (ite exec_9_0_8 #x0001 (ite exec_9_1_6 #x0001 (ite exec_10_0_8 #x0001 (ite exec_10_1_6 #x0001 (ite exec_11_0_8 #x0001 (ite exec_11_1_6 #x0001 (ite exec_12_0_8 #x0001 (ite exec_12_1_6 #x0001 (ite exec_13_0_8 #x0001 (ite exec_13_1_6 #x0001 (ite exec_14_0_8 #x0001 (ite exec_14_1_6 #x0001 (ite exec_15_0_8 #x0001 (ite exec_15_1_6 #x0001 (ite exec_16_0_8 #x0001 (ite exec_16_1_6 #x0001 #x0000))))))))))))))))))))))))))))))))))
(assert (= exit-code (ite exec_16_0_8 #x0001 (ite exec_16_1_6 #x0001 (ite exec_15_0_8 #x0001 (ite exec_15_1_6 #x0001 (ite exec_14_0_8 #x0001 (ite exec_14_1_6 #x0001 (ite exec_13_0_8 #x0001 (ite exec_13_1_6 #x0001 (ite exec_12_0_8 #x0001 (ite exec_12_1_6 #x0001 (ite exec_11_0_8 #x0001 (ite exec_11_1_6 #x0001 (ite exec_10_0_8 #x0001 (ite exec_10_1_6 #x0001 (ite exec_9_0_8 #x0001 (ite exec_9_1_6 #x0001 (ite exec_8_0_8 #x0001 (ite exec_8_1_6 #x0001 (ite exec_7_0_8 #x0001 (ite exec_7_1_6 #x0001 (ite exec_6_0_8 #x0001 (ite exec_6_1_6 #x0001 (ite exec_5_0_8 #x0001 (ite exec_5_1_6 #x0001 (ite exec_4_0_8 #x0001 (ite exec_4_1_6 #x0001 (ite exec_3_0_8 #x0001 (ite exec_3_1_6 #x0001 (ite exec_2_0_8 #x0001 (ite exec_2_1_6 #x0001 (ite exec_1_0_8 #x0001 (ite exec_1_1_6 #x0001 (ite exec_0_0_8 #x0001 (ite exec_0_1_6 #x0001 #x0000))))))))))))))))))))))))))))))))))))
......@@ -48,7 +48,11 @@ TEST_F(Boolector, simulate_halt_relational) { simulate_halt<R>(); }
TEST_F(Boolector, verify_indirect_functional) { verify_indirect<F>(); }
TEST_F(Boolector, verify_indirect_relational) { verify_indirect<R>(); }
TEST_F(Boolector, verify_halt_functional) { verify_halt<F>(); }
TEST_F(Boolector, verify_halt_relational) { verify_halt<R>(); }
// demo example tests
//
TEST_F(Boolector, demo_functional) { demo<F>(); }
TEST_F(Boolector, demo_relational) { demo<R>(); }
......
......@@ -51,7 +51,10 @@ TEST_F(BtorMC, simulate_halt) { simulate_halt<E>(); }
//
TEST_F(BtorMC, verify_indirect) { verify_indirect<E>(); }
TEST_F(BtorMC, verify_halt) { verify_halt<E>(); }
// demo example test
//
TEST_F(BtorMC, demo) { demo<E>(); }
// litmus tests
......
......@@ -48,7 +48,11 @@ TEST_F(CVC4, simulate_halt_relational) { simulate_halt<R>(); }
TEST_F(CVC4, verify_indirect_functional) { verify_indirect<F>(); }
TEST_F(CVC4, verify_indirect_relational) { verify_indirect<R>(); }
TEST_F(CVC4, verify_halt_functional) { verify_halt<F>(); }
TEST_F(CVC4, verify_halt_relational) { verify_halt<R>(); }
// demo example tests
//
TEST_F(CVC4, DISABLED_demo_functional) { demo<F>(); }
TEST_F(CVC4, DISABLED_demo_relational) { demo<R>(); }
......
......@@ -904,7 +904,13 @@ TEST(smtlib_Functional, define_exit_code)
"#x0001 "
"(ite exec_1_2_0 "
"#x0002 "
"#x0000)))))\n"
"(ite exec_0_0_0 "
"#x0000 "
"(ite exec_0_1_0 "
"#x0001 "
"(ite exec_0_2_0 "
"#x0002 "
"#x0000))))))))\n"
"\n",
encoder.formula.str());
......@@ -923,7 +929,13 @@ TEST(smtlib_Functional, define_exit_code)
"#x0001 "
"(ite exec_1_2_0 "
"#x0002 "
"#x0000)))))\n"
"(ite exec_0_0_0 "
"#x0000 "
"(ite exec_0_1_0 "
"#x0001 "
"(ite exec_0_2_0 "
"#x0002 "
"#x0000))))))))\n"
"\n",
encoder.formula.str());
}
......
......@@ -163,6 +163,8 @@ struct Solver : public ::testing::Test
const std::shared_ptr<MMap> & mmap,
const size_t bound)
{
using namespace fs;
Encoder encoder(programs, mmap, bound);
encoder.encode();
......@@ -170,6 +172,10 @@ struct Solver : public ::testing::Test
if constexpr(std::is_base_of<btor2::Encoder, Encoder>::value)
encoder.define_bound();
write(
mktmp(stem, ext<Encoder>(programs->size(), bound)),
encoder.formula.str());
const auto trace = solver.solve(encoder);
ASSERT_FALSE(trace->empty());
......@@ -178,9 +184,6 @@ struct Solver : public ::testing::Test
const auto replay = Simulator().replay(*trace);
const auto sext = '.' + solver.name();
using namespace fs;
write(mktmp(stem, ext<Encoder>(programs->size(), bound)), formula);
write(mktmp(stem, ext<Encoder>(sext + ".trace")), trace->print());
write(mktmp(stem, ext<Encoder>(sext + ".replay.trace")), replay->print());
......@@ -295,6 +298,45 @@ struct Solver : public ::testing::Test
ASSERT_FALSE(solver.sat(solver.formula(encoder)));
}
// verify halting mechanism
//
template <class Encoder>
void verify_halt ()
{
Encoder encoder(
std::make_shared<Program::List>(
Program({Instruction::create("HALT")}),
Program({Instruction::create("HALT")}),
Program({Instruction::create("EXIT", 1)})),
nullptr,
3);
encoder.encode();
if constexpr(std::is_base_of<smtlib::Encoder, Encoder>::value)
encoder.formula <<
smtlib::assertion(
smtlib::equality(
smtlib::Encoder::exit_code_sym,
smtlib::word2hex(0))) <<
eol;
else
encoder.formula <<
btor2::eq(
encoder.nid(),
encoder.sid_bool,
encoder.nids_const[0],
encoder.nid_exit_code) <<
btor2::land(
encoder.nid(),
encoder.sid_bool,
encoder.nid_exit_flag,
std::to_string(encoder.node - 1)) <<
btor2::bad(encoder.node);
ASSERT_FALSE(solver.sat(solver.formula(encoder)));
}
//----------------------------------------------------------------------------
// demo example tests
//----------------------------------------------------------------------------
......
......@@ -46,7 +46,11 @@ TEST_F(Z3, simulate_halt_relational) { simulate_halt<R>(); }
TEST_F(Z3, verify_indirect_functional) { verify_indirect<F>(); }
TEST_F(Z3, verify_indirect_relational) { verify_indirect<R>(); }
TEST_F(Z3, verify_halt_functional) { verify_halt<F>(); }
TEST_F(Z3, verify_halt_relational) { verify_halt<R>(); }
// demo example tests
//
TEST_F(Z3, demo_functional) { demo<F>(); }
TEST_F(Z3, demo_relational) { demo<R>(); }
......
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