...
 
Commits (2)
......@@ -43,31 +43,32 @@ Encoder::Encoder (const std::shared_ptr<Program::List> & p,
{
predecessors.reserve(num_threads);
iterate_programs([this] (const Program & program) {
// collect predecessors
predecessors.push_back(program.predecessors());
for (pc = 0; pc < program.size(); pc++)
{
const Instruction & op = program[pc];
// collect statements requiring an empty store buffer
if (op.requires_flush())
flushes[thread].push_back(pc);
// collect checkpoints
if (!op.type())
checkpoints[op.arg()][thread].push_back(pc);
// collect explicit halt statements
if (&op.symbol() == &Instruction::Halt::symbol)
halts[thread].push_back(pc);
// collect exit calls
if (&op.symbol() == &Instruction::Exit::symbol)
exits[thread].push_back(pc);
}
});
iterate_programs([this] (const Program & program)
{
// collect predecessors
predecessors.push_back(program.predecessors());
for (pc = 0; pc < program.size(); pc++)
{
const Instruction & op = program[pc];
// collect statements requiring an empty store buffer
if (op.requires_flush())
flushes[thread].push_back(pc);
// collect checkpoints
if (!op.type())
checkpoints[op.arg()][thread].push_back(pc);
// collect explicit halt statements
if (&op.symbol() == &Instruction::Halt::symbol)
halts[thread].push_back(pc);
// collect exit calls
if (&op.symbol() == &Instruction::Exit::symbol)
exits[thread].push_back(pc);
}
});
// remove single-threaded checkpoints
for (auto it = checkpoints.begin(); it != checkpoints.end();)
......
This diff is collapsed.
......@@ -625,9 +625,10 @@ void Encoder::declare_accu ()
if (verbose)
formula << accu_comment;
iterate_threads([this] {
formula << declare_bv_var(accu_var(), word_size) << eol;
});
iterate_threads([this]
{
formula << declare_bv_var(accu_var(), word_size) << eol;
});
formula << eol;
}
......@@ -639,9 +640,10 @@ void Encoder::declare_mem ()
if (verbose)
formula << mem_comment;
iterate_threads([this] {
formula << declare_bv_var(mem_var(), word_size) << eol;
});
iterate_threads([this]
{
formula << declare_bv_var(mem_var(), word_size) << eol;
});
formula << eol;
}
......@@ -653,9 +655,10 @@ void Encoder::declare_sb_adr ()
if (verbose)
formula << sb_adr_comment;
iterate_threads([this] {
formula << declare_bv_var(sb_adr_var(), word_size) << eol;
});
iterate_threads([this]
{
formula << declare_bv_var(sb_adr_var(), word_size) << eol;
});
formula << eol;
}
......@@ -667,9 +670,10 @@ void Encoder::declare_sb_val ()
if (verbose)
formula << sb_val_comment;
iterate_threads([this] {
formula << declare_bv_var(sb_val_var(), word_size) << eol;
});
iterate_threads([this]
{
formula << declare_bv_var(sb_val_var(), word_size) << eol;
});
formula << eol;
}
......@@ -681,9 +685,10 @@ void Encoder::declare_sb_full ()
if (verbose)
formula << sb_full_comment;
iterate_threads([this] {
formula << declare_bool_var(sb_full_var()) << eol;
});
iterate_threads([this]
{
formula << declare_bool_var(sb_full_var()) << eol;
});
formula << eol;
}
......@@ -695,12 +700,13 @@ void Encoder::declare_stmt ()
if (verbose)
formula << stmt_comment;
iterate_programs([this] (const Program & program) {
for (pc = 0; pc < program.size(); pc++)
formula << declare_bool_var(stmt_var()) << eol;
iterate_programs([this] (const Program & program)
{
for (pc = 0; pc < program.size(); pc++)
formula << declare_bool_var(stmt_var()) << eol;
formula << eol;
});
formula << eol;
});
}
// smtlib::Encoder::declare_block ----------------------------------------------
......@@ -736,8 +742,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;
}
......@@ -807,9 +812,7 @@ void Encoder::declare_thread ()
if (verbose)
formula << thread_comment;
iterate_threads([this] {
formula << declare_bool_var(thread_var()) << eol;
});
iterate_threads([this] { formula << declare_bool_var(thread_var()) << eol; });
formula << eol;
}
......@@ -821,12 +824,13 @@ void Encoder::declare_exec ()
if (verbose)
formula << exec_comment;
iterate_programs([this] (const Program & program) {
for (pc = 0; pc < program.size(); pc++)
formula << declare_bool_var(exec_var()) << eol;
iterate_programs([this] (const Program & program)
{
for (pc = 0; pc < program.size(); pc++)
formula << declare_bool_var(exec_var()) << eol;
formula << eol;
});
formula << eol;
});
}
// smtlib::Encoder::declare_flush ----------------------------------------------
......@@ -836,9 +840,7 @@ void Encoder::declare_flush ()
if (verbose)
formula << flush_comment;
iterate_threads([this] {
formula << declare_bool_var(flush_var()) << eol;
});
iterate_threads([this] { formula << declare_bool_var(flush_var()) << eol; });
formula << eol;
}
......@@ -876,9 +878,10 @@ void Encoder::declare_transitions ()
#define INIT_STATE(_var) \
do { \
iterate_threads([this] { \
formula << assign(_var(step, thread), word2hex(0)) << eol; \
}); \
iterate_threads([this] \
{ \
formula << assign(_var(step, thread), word2hex(0)) << eol; \
}); \
formula << eol; \
} while (0)
......@@ -927,9 +930,7 @@ void Encoder::init_sb_full ()
if (verbose)
formula << sb_full_comment;
iterate_threads([this] {
formula << assertion(lnot(sb_full_var())) << eol;
});
iterate_threads([this] { formula << assertion(lnot(sb_full_var())) << eol; });
formula << eol;
}
......@@ -941,14 +942,15 @@ void Encoder::init_stmt ()
if (verbose)
formula << stmt_comment;
iterate_programs([this] (const Program & program) {
for (pc = 0; pc < program.size(); pc++)
formula
<< assertion(pc ? lnot(stmt_var()) : stmt_var())
<< eol;
iterate_programs([this] (const Program & program)
{
for (pc = 0; pc < program.size(); pc++)
formula
<< assertion(pc ? lnot(stmt_var()) : stmt_var())
<< eol;
formula << eol;
});
formula << eol;
});
}
// smtlib::Encoder::init_block -------------------------------------------------
......@@ -982,8 +984,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;
}
......@@ -1046,14 +1047,15 @@ void Encoder::define_exec ()
if (verbose)
formula << exec_comment;
iterate_programs([this] (const Program & program) {
for (pc = 0; pc < program.size(); pc++)
formula
<< assign(exec_var(), land(stmt_var(), thread_var()))
<< eol;
iterate_programs([this] (const Program & program)
{
for (pc = 0; pc < program.size(); pc++)
formula
<< assign(exec_var(), land(stmt_var(), thread_var()))
<< eol;
formula << eol;
});
formula << eol;
});
}
// smtlib::Encoder::define_check -----------------------------------------------
......@@ -1114,10 +1116,11 @@ void Encoder::define_scheduling_constraints ()
variables.reserve(num_threads * 2 + 1);
iterate_threads([this, &variables] {
variables.push_back(thread_var());
variables.push_back(flush_var());
});
iterate_threads([this, &variables]
{
variables.push_back(thread_var());
variables.push_back(flush_var());
});
if (!halts.empty() || !exits.empty())
variables.push_back(exit_flag_var());
......@@ -1136,39 +1139,39 @@ void Encoder::define_store_buffer_constraints ()
if (verbose)
formula << comment_subsection("store buffer constraints");
iterate_threads([this] {
if (flushes.find(thread) != flushes.end())
{
const auto & pcs = flushes[thread];
std::vector<std::string> stmts;
iterate_threads([this]
{
if (flushes.find(thread) != flushes.end())
{
const auto & pcs = flushes[thread];
stmts.reserve(pcs.size());
std::vector<std::string> stmts;
stmts.reserve(pcs.size());
for (const word_t p : pcs)
stmts.push_back(stmt_var(step, thread, p));
for (const word_t p : pcs)
stmts.push_back(stmt_var(step, thread, p));
formula <<
assertion(
ite(
sb_full_var(),
formula <<
assertion(
ite(
sb_full_var(),
implication(
lor(stmts),
lnot(thread_var())),
lnot(flush_var()))) <<
eol;
}
else
{
// TODO: (or sb-full (not flush)) directly?
formula <<
assertion(
implication(
lor(stmts),
lnot(thread_var())),
lnot(flush_var()))) <<
eol;
}
else
{
// TODO: (or sb-full (not flush)) directly?
formula <<
assertion(
implication(
lnot(sb_full_var()),
lnot(flush_var()))) <<
eol;
}
});
lnot(sb_full_var()),
lnot(flush_var()))) <<
eol;
}
});
formula << eol;
}
......
......@@ -29,17 +29,18 @@ void Functional::encode ()
#define DEFINE_STATE(_update, _type, _var) \
do { \
update = _update; \
iterate_programs([this] (const Program & program) { \
std::string expr = _var(prev, thread); \
pc = program.size() - 1; \
for (auto rit = program.rbegin(); rit != program.rend(); ++rit, pc--) \
{ \
const Instruction & op = *rit; \
if (op.type() & _type) \
expr = ite(exec_var(prev, thread, pc), op.encode(*this), expr); \
} \
formula << assign(_var(step, thread), expr) << eol; \
}); \
iterate_programs([this] (const Program & program) \
{ \
std::string expr = _var(prev, thread); \
pc = program.size() - 1; \
for (auto rit = program.rbegin(); rit != program.rend(); ++rit, pc--) \
{ \
const Instruction & op = *rit; \
if (op.type() & _type) \
expr = ite(exec_var(prev, thread, pc), op.encode(*this), expr); \
} \
formula << assign(_var(step, thread), expr) << eol; \
}); \
formula << eol; \
} while (0)
......@@ -90,25 +91,26 @@ void Functional::define_sb_full ()
if (verbose)
formula << sb_full_comment;
iterate_programs([this] (const Program & program) {
std::vector<std::string> args;
pc = program.size() - 1;
iterate_programs([this] (const Program & program)
{
std::vector<std::string> args;
pc = program.size() - 1;
for (auto rit = program.rbegin(); rit != program.rend(); ++rit, pc--)
if (rit->type() & Instruction::Type::write)
args.push_back(exec_var(prev, thread, pc));
for (auto rit = program.rbegin(); rit != program.rend(); ++rit, pc--)
if (rit->type() & Instruction::Type::write)
args.push_back(exec_var(prev, thread, pc));
args.push_back(sb_full_var(prev, thread));
args.push_back(sb_full_var(prev, thread));
formula <<
assign(
sb_full_var(),
ite(
flush_var(prev, thread),
FALSE,
lor(args))) <<
eol;
});
formula <<
assign(
sb_full_var(),
ite(
flush_var(prev, thread),
FALSE,
lor(args))) <<
eol;
});
formula << eol;
}
......@@ -120,49 +122,50 @@ void Functional::define_stmt ()
if (verbose)
formula << stmt_comment;
iterate_programs([this] (const Program & program) {
for (pc = 0; pc < program.size(); pc++)
{
// statement reactivation
std::string expr =
land(
stmt_var(prev, thread, pc),
lnot(exec_var(prev, thread, pc)));
const auto & pred = predecessors[thread][pc];
for (auto rit = pred.rbegin(); rit != pred.rend(); ++rit)
{
// predecessor's execution variable
std::string val = exec_var(prev, thread, *rit);
// build conjunction of execution variable and jump condition
const Instruction & pre = program[*rit];
if (pre.is_jump())
{
const std::string cond = pre.encode(*this);
// JMP has no condition and returns an empty std::string
if (!cond.empty())
val =
land(
val,
// only activate successor if jump condition failed
*rit == pc - 1 && pre.arg() != pc
? lnot(cond)
: cond);
}
// add predecessor to the activation
expr = ite(stmt_var(prev, thread, *rit), val, expr);
}
formula << assign(stmt_var(), expr) << eol;
}
formula << eol;
});
iterate_programs([this] (const Program & program)
{
for (pc = 0; pc < program.size(); pc++)
{
// statement reactivation
std::string expr =
land(
stmt_var(prev, thread, pc),
lnot(exec_var(prev, thread, pc)));
const auto & pred = predecessors[thread][pc];
for (auto rit = pred.rbegin(); rit != pred.rend(); ++rit)
{
// predecessor's execution variable
std::string val = exec_var(prev, thread, *rit);
// build conjunction of execution variable and jump condition
const Instruction & pre = program[*rit];
if (pre.is_jump())
{
const std::string cond = pre.encode(*this);
// JMP has no condition and returns an empty std::string
if (!cond.empty())
val =
land(
val,
// only activate successor if jump condition failed
*rit == pc - 1 && pre.arg() != pc
? lnot(cond)
: cond);
}
// add predecessor to the activation
expr = ite(stmt_var(prev, thread, *rit), val, expr);
}
formula << assign(stmt_var(), expr) << eol;
}
formula << eol;
});
}
// smtlib::Functional::define_block --------------------------------------------
......@@ -213,18 +216,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;
}
......@@ -241,26 +252,27 @@ void Functional::define_heap ()
const std::string heap_prev = heap_var(prev);
std::string expr = heap_prev;
iterate_programs_reverse([this, &heap_prev, &expr] (const Program & program) {
pc = program.size() - 1;
iterate_programs_reverse([this, &heap_prev, &expr] (const Program & program)
{
pc = program.size() - 1;
for (auto rit = program.rbegin(); rit != program.rend(); ++rit, pc--)
{
const Instruction & op = *rit;
for (auto rit = program.rbegin(); rit != program.rend(); ++rit, pc--)
{
const Instruction & op = *rit;
if (op.type() & Instruction::Type::atomic)
expr = ite(exec_var(prev, thread, pc), op.encode(*this), expr);
}
if (op.type() & Instruction::Type::atomic)
expr = ite(exec_var(prev, thread, pc), op.encode(*this), expr);
}
expr =
ite(
flush_var(prev, thread),
store(
heap_prev,
sb_adr_var(prev, thread),
sb_val_var(prev, thread)),
expr);
});
expr =
ite(
flush_var(prev, thread),
store(
heap_prev,
sb_adr_var(prev, thread),
sb_val_var(prev, thread)),
expr);
});
formula << assign(heap_var(), expr) << eol << eol;
}
......@@ -280,11 +292,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 +315,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>(); }
......
......@@ -138,10 +138,11 @@ TEST(Encoder, iterate_programs)
word_t thread = 0;
encoder.iterate_programs([&] (const Program & p) {
ASSERT_EQ(thread, encoder.thread);
ASSERT_EQ(&(*programs)[thread++], &p);
});
encoder.iterate_programs([&] (const Program & p)
{
ASSERT_EQ(thread, encoder.thread);
ASSERT_EQ(&(*programs)[thread++], &p);
});
}
// Encoder::iterate_programs_reverse ===========================================
......@@ -153,10 +154,11 @@ TEST(Encoder, iterate_programs_reverse)
word_t thread = encoder.num_threads - 1;
encoder.iterate_programs_reverse([&] (const Program & p) {
ASSERT_EQ(thread, encoder.thread);
ASSERT_EQ(&(*programs)[thread--], &p);
});
encoder.iterate_programs_reverse([&] (const Program & p)
{
ASSERT_EQ(thread, encoder.thread);
ASSERT_EQ(&(*programs)[thread--], &p);
});
}
} // namespace ConcuBinE::test
This diff is collapsed.
......@@ -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>(); }
......