Commit 4cfb144b authored by phlo's avatar phlo

fixed iterate_* indentation

parent 06d83aa9
......@@ -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 ----------------------------------------------
......@@ -806,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;
}
......@@ -820,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 ----------------------------------------------
......@@ -835,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;
}
......@@ -875,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)
......@@ -926,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;
}
......@@ -940,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 -------------------------------------------------
......@@ -1044,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 -----------------------------------------------
......@@ -1112,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());
......@@ -1134,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;
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));
formula <<
assign(
sb_full_var(),
ite(
flush_var(prev, thread),
FALSE,
lor(args))) <<
eol;
});
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));
args.push_back(sb_full_var(prev, thread));
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 --------------------------------------------
......@@ -249,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;
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);
}
expr =
ite(
flush_var(prev, thread),
store(
heap_prev,
sb_adr_var(prev, thread),
sb_val_var(prev, thread)),
expr);
});
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;
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);
});
formula << assign(heap_var(), expr) << eol << eol;
}
......
......@@ -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.
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