Commit 10a02ba5 authored by phlo's avatar phlo

added implicit HALT

if final program statement is not a control operation
parent c5ab05ac
......@@ -82,10 +82,6 @@ Encoder::Encoder (const Program::List::ptr & p, size_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);
});
}
......
......@@ -164,9 +164,13 @@ Program::Program(std::istream & f, const std::string & p) : path(p)
parser_error(path, pc, "unknown label [" + *label + "]");
}
// insert final HALT (if missing)
if (!(back().type() & Instruction::Type::control))
push_back(Instruction::create("HALT"));
// collect predecessors
predecessors[0]; // explicitly add initial instruction
for (word_t pc = 0, last = size() - 1; pc <= last; pc++)
for (word_t pc = 0, final = size() - 1; pc <= final; pc++)
{
const Instruction & op = (*this)[pc];
......@@ -183,7 +187,7 @@ Program::Program(std::istream & f, const std::string & p) : path(p)
predecessors[target].insert(pc);
}
else if (pc < last)
else if (pc < final)
{
using Halt = Instruction::Halt;
using Exit = Instruction::Exit;
......
......@@ -45,19 +45,19 @@ TEST_RUN := run_all_tests
GTEST_FILTER = --gtest_filter=
# GTEST_FILTER += "*"
# GTEST_FILTER += Encoder.*
# GTEST_FILTER += smtlib.*
# GTEST_FILTER += smtlib_Encoder.*
# GTEST_FILTER += smtlib_Functional.*
# GTEST_FILTER += smtlib_Relational.*
# GTEST_FILTER += btor2.*
# GTEST_FILTER += btor2_Encoder.*
# GTEST_FILTER += Simulator.*
GTEST_FILTER += Encoder.*
GTEST_FILTER += smtlib.*
GTEST_FILTER += smtlib_Encoder.*
GTEST_FILTER += smtlib_Functional.*
GTEST_FILTER += smtlib_Relational.*
GTEST_FILTER += btor2.*
GTEST_FILTER += btor2_Encoder.*
GTEST_FILTER += Simulator.*
# GTEST_FILTER += Main.*
# GTEST_FILTER += Experimental.*
# GTEST_FILTER += Instruction.*
# GTEST_FILTER += Program.*
# GTEST_FILTER += Trace.*
GTEST_FILTER += Program.*
GTEST_FILTER += Trace.*
GTEST_FILTER += MMap.*
# GTEST_FILTER += Shell.*
# GTEST_FILTER += Boolector.*
......
......@@ -50,15 +50,15 @@ TEST_F(Encoder, constructor_flush_pcs)
"STORE 1\n"
"FENCE\n"
"CAS 1\n"
));
"HALT\n"));
reset_encoder();
for (const auto & p : *encoder->programs)
ASSERT_EQ(3, p.size());
ASSERT_EQ(4, p.size());
for (const auto & pcs : encoder->flush_pcs)
ASSERT_EQ(std::vector<word_t>({0, 1, 2}), pcs.second);
ASSERT_EQ(std::vector<word_t>({0, 1, 2, 3}), pcs.second);
}
TEST_F(Encoder, constructor_check_pcs)
......@@ -67,8 +67,7 @@ TEST_F(Encoder, constructor_check_pcs)
programs.push_back(create_program(
"CHECK 1\n"
"CHECK 2\n"
"CHECK 3\n"
));
"CHECK 3\n"));
reset_encoder();
......@@ -90,14 +89,13 @@ TEST_F(Encoder, constructor_halt_pcs)
programs.push_back(create_program(
"JZ 2\n"
"HALT\n"
"ADDI 1\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]);
ASSERT_EQ(std::vector<word_t>({1, 3}), encoder->halt_pcs[0]);
ASSERT_EQ(std::vector<word_t>({1}), encoder->halt_pcs[1]);
}
TEST_F(Encoder, constructor_exit_pcs)
......@@ -108,8 +106,7 @@ TEST_F(Encoder, constructor_exit_pcs)
"EXIT 1\n"
"JNZ 4\n"
"EXIT 2\n"
"EXIT 3\n"
));
"EXIT 3\n"));
reset_encoder(0);
......
......@@ -31,9 +31,8 @@ struct Encoder: public ::testing::Test
Program create_program (const std::string code)
{
std::string path = "dummy.asm";
std::istringstream inbuf {code};
return Program(inbuf, path);
return Program(inbuf, "dummy.asm");
}
void reset_encoder (const size_t bound = 1)
......
......@@ -1466,7 +1466,7 @@ TEST_F(btor2_Encoder, define_sb_full)
TEST_F(btor2_Encoder, define_stmt)
{
add_dummy_programs(3, 3);
add_dummy_programs(3, 2);
reset_encoder();
init_state_definitions();
......@@ -1549,7 +1549,7 @@ TEST_F(btor2_Encoder, define_stmt)
s << eol;
// ADDI 1
// HALT
pc++;
s <<
......@@ -2561,7 +2561,8 @@ TEST_F(btor2_Encoder, define_halt)
"JNZ 3\n"
"HALT\n"
"SUBI 1\n"
));
"HALT\n"));
reset_encoder();
init_state_definitions();
......@@ -2590,7 +2591,7 @@ TEST_F(btor2_Encoder, define_halt)
std::to_string(nid),
encoder->sid_bool,
encoder->nids_exec[thread][2],
encoder->nids_exec[thread][3]);
encoder->nids_exec[thread][4]);
nid++;
s <<
btor2::lor(
......@@ -3113,13 +3114,13 @@ TEST_F(btor2_Encoder, define_scheduling_constraints_single_thread)
TEST_F(btor2_Encoder, define_store_buffer_constraints)
{
// add_instruction_set(3);
for (size_t i = 0; i < 3; i++)
programs.push_back(create_program(
"STORE 1\n"
"FENCE\n"
"CAS 1\n"
));
"HALT\n"));
reset_encoder();
init_state_definitions();
......@@ -3173,7 +3174,9 @@ TEST_F(btor2_Encoder, define_store_buffer_constraints)
TEST_F(btor2_Encoder, define_store_buffer_constraints_no_barrier)
{
add_dummy_programs(3);
for (size_t i = 0; i < 3; i++)
programs.push_back(create_program("JMP 0\n"));
reset_encoder();
init_state_definitions();
......
......@@ -519,7 +519,7 @@ TEST_F(smtlib_Encoder, declare_sb_full)
TEST_F(smtlib_Encoder, declare_stmt)
{
add_dummy_programs(3, 3);
add_dummy_programs(3, 2);
reset_encoder();
encoder->declare_stmt();
......@@ -571,8 +571,7 @@ TEST_F(smtlib_Encoder, declare_block)
programs.push_back(
create_program(
"CHECK 0\n"
"CHECK 1\n"
));
"CHECK 1\n"));
reset_encoder();
......@@ -760,7 +759,7 @@ TEST_F(smtlib_Encoder, declare_thread)
TEST_F(smtlib_Encoder, declare_exec)
{
add_dummy_programs(3, 3);
add_dummy_programs(3, 2);
reset_encoder();
encoder->declare_exec();
......@@ -846,7 +845,7 @@ TEST_F(smtlib_Encoder, declare_check)
// 3 different checkpoint ids
for (auto & p : programs)
p = create_program(p.print() + "CHECK " + std::to_string(check_id++) + eol);
p = create_program("CHECK " + std::to_string(check_id++) + eol + p.print());
reset_encoder();
......@@ -862,7 +861,7 @@ TEST_F(smtlib_Encoder, declare_check)
// same checkpoint ids
for (auto & p : programs)
p = create_program(p.print() + "CHECK " + std::to_string(check_id) + eol);
p = create_program("CHECK " + std::to_string(check_id) + eol + p.print());
reset_encoder();
......@@ -1064,7 +1063,7 @@ TEST_F(smtlib_Encoder, init_sb_full)
TEST_F(smtlib_Encoder, init_stmt)
{
add_dummy_programs(3, 3);
add_dummy_programs(3, 2);
reset_encoder(0);
encoder->init_stmt();
......@@ -1116,8 +1115,7 @@ TEST_F(smtlib_Encoder, init_block)
programs.push_back(
create_program(
"CHECK 0\n"
"CHECK 1\n"
));
"CHECK 1\n"));
reset_encoder(0);
......@@ -1290,8 +1288,7 @@ TEST_F(smtlib_Encoder, init_states_check_exit)
programs.push_back(
create_program(
"CHECK 0\n"
"EXIT 1\n"
));
"EXIT 1\n"));
reset_encoder(0);
......@@ -1332,7 +1329,7 @@ TEST_F(smtlib_Encoder, init_states_check_exit)
TEST_F(smtlib_Encoder, define_exec)
{
add_dummy_programs(3, 3);
add_dummy_programs(3, 2);
reset_encoder();
encoder->define_exec();
......@@ -1552,7 +1549,7 @@ TEST_F(smtlib_Encoder, define_store_buffer_constraints)
"STORE 1\n"
"FENCE\n"
"CAS 1\n"
));
"HALT\n"));
reset_encoder();
......@@ -1563,15 +1560,15 @@ TEST_F(smtlib_Encoder, define_store_buffer_constraints)
"\n"
"(assert "
"(ite sb-full_1_0 "
"(=> (or stmt_1_0_0 stmt_1_0_1 stmt_1_0_2) (not thread_1_0)) "
"(=> (or stmt_1_0_0 stmt_1_0_1 stmt_1_0_2 stmt_1_0_3) (not thread_1_0)) "
"(not flush_1_0)))\n"
"(assert "
"(ite sb-full_1_1 "
"(=> (or stmt_1_1_0 stmt_1_1_1 stmt_1_1_2) (not thread_1_1)) "
"(=> (or stmt_1_1_0 stmt_1_1_1 stmt_1_1_2 stmt_1_1_3) (not thread_1_1)) "
"(not flush_1_1)))\n"
"(assert "
"(ite sb-full_1_2 "
"(=> (or stmt_1_2_0 stmt_1_2_1 stmt_1_2_2) (not thread_1_2)) "
"(=> (or stmt_1_2_0 stmt_1_2_1 stmt_1_2_2 stmt_1_2_3) (not thread_1_2)) "
"(not flush_1_2)))\n"
"\n",
encoder->str());
......@@ -1586,15 +1583,15 @@ TEST_F(smtlib_Encoder, define_store_buffer_constraints)
ASSERT_EQ(
"(assert "
"(ite sb-full_1_0 "
"(=> (or stmt_1_0_0 stmt_1_0_1 stmt_1_0_2) (not thread_1_0)) "
"(=> (or stmt_1_0_0 stmt_1_0_1 stmt_1_0_2 stmt_1_0_3) (not thread_1_0)) "
"(not flush_1_0)))\n"
"(assert "
"(ite sb-full_1_1 "
"(=> (or stmt_1_1_0 stmt_1_1_1 stmt_1_1_2) (not thread_1_1)) "
"(=> (or stmt_1_1_0 stmt_1_1_1 stmt_1_1_2 stmt_1_1_3) (not thread_1_1)) "
"(not flush_1_1)))\n"
"(assert "
"(ite sb-full_1_2 "
"(=> (or stmt_1_2_0 stmt_1_2_1 stmt_1_2_2) (not thread_1_2)) "
"(=> (or stmt_1_2_0 stmt_1_2_1 stmt_1_2_2 stmt_1_2_3) (not thread_1_2)) "
"(not flush_1_2)))\n"
"\n",
encoder->str());
......@@ -1622,7 +1619,7 @@ TEST_F(smtlib_Encoder, define_checkpoint_constraints)
// two different checkpoints
for (auto & p : programs)
p = create_program(p.print() + "CHECK 2\n");
p = create_program("CHECK 2\n" + p.print());
reset_encoder();
......@@ -1642,7 +1639,7 @@ TEST_F(smtlib_Encoder, define_checkpoint_constraints)
// two identical checkpoints
for (auto & p : programs)
p = create_program(p.print() + "CHECK 1\n");
p = create_program("CHECK 1\n" + p.print());
reset_encoder();
......
......@@ -311,7 +311,7 @@ TEST_F(smtlib_Functional, define_stmt)
programs.push_back(create_program(
"ADDI 1\n"
"STORE 1\n"
));
"HALT\n"));
reset_encoder();
......@@ -324,18 +324,30 @@ TEST_F(smtlib_Functional, define_stmt)
"(ite stmt_0_0_0 "
"exec_0_0_0 "
"(and stmt_0_0_1 (not exec_0_0_1)))))\n"
"(assert (= stmt_1_0_2 "
"(ite stmt_0_0_1 "
"exec_0_0_1 "
"(and stmt_0_0_2 (not exec_0_0_2)))))\n"
"\n"
"(assert (= stmt_1_1_0 (and stmt_0_1_0 (not exec_0_1_0))))\n"
"(assert (= stmt_1_1_1 "
"(ite stmt_0_1_0 "
"exec_0_1_0 "
"(and stmt_0_1_1 (not exec_0_1_1)))))\n"
"(assert (= stmt_1_1_2 "
"(ite stmt_0_1_1 "
"exec_0_1_1 "
"(and stmt_0_1_2 (not exec_0_1_2)))))\n"
"\n"
"(assert (= stmt_1_2_0 (and stmt_0_2_0 (not exec_0_2_0))))\n"
"(assert (= stmt_1_2_1 "
"(ite stmt_0_2_0 "
"exec_0_2_0 "
"(and stmt_0_2_1 (not exec_0_2_1)))))\n"
"(assert (= stmt_1_2_2 "
"(ite stmt_0_2_1 "
"exec_0_2_1 "
"(and stmt_0_2_2 (not exec_0_2_2)))))\n"
"\n",
encoder->str());
......@@ -352,18 +364,30 @@ TEST_F(smtlib_Functional, define_stmt)
"(ite stmt_0_0_0 "
"exec_0_0_0 "
"(and stmt_0_0_1 (not exec_0_0_1)))))\n"
"(assert (= stmt_1_0_2 "
"(ite stmt_0_0_1 "
"exec_0_0_1 "
"(and stmt_0_0_2 (not exec_0_0_2)))))\n"
"\n"
"(assert (= stmt_1_1_0 (and stmt_0_1_0 (not exec_0_1_0))))\n"
"(assert (= stmt_1_1_1 "
"(ite stmt_0_1_0 "
"exec_0_1_0 "
"(and stmt_0_1_1 (not exec_0_1_1)))))\n"
"(assert (= stmt_1_1_2 "
"(ite stmt_0_1_1 "
"exec_0_1_1 "
"(and stmt_0_1_2 (not exec_0_1_2)))))\n"
"\n"
"(assert (= stmt_1_2_0 (and stmt_0_2_0 (not exec_0_2_0))))\n"
"(assert (= stmt_1_2_1 "
"(ite stmt_0_2_0 "
"exec_0_2_0 "
"(and stmt_0_2_1 (not exec_0_2_1)))))\n"
"(assert (= stmt_1_2_2 "
"(ite stmt_0_2_1 "
"exec_0_2_1 "
"(and stmt_0_2_2 (not exec_0_2_2)))))\n"
"\n",
encoder->str());
}
......@@ -374,8 +398,7 @@ TEST_F(smtlib_Functional, define_stmt_jmp)
programs.push_back(create_program(
"ADDI 1\n"
"STORE 1\n"
"JMP 1\n"
));
"JMP 1\n"));
reset_encoder();
......@@ -429,8 +452,7 @@ TEST_F(smtlib_Functional, define_stmt_jmp_conditional)
"ADDI 1\n"
"STORE 1\n"
"JNZ 1\n"
"EXIT 1\n"
));
"EXIT 1\n"));
reset_encoder();
......@@ -496,8 +518,7 @@ TEST_F(smtlib_Functional, define_stmt_jmp_start)
"ADDI 1\n"
"STORE 1\n"
"JNZ 0\n"
"EXIT 1\n"
));
"EXIT 1\n"));
reset_encoder();
......@@ -567,8 +588,7 @@ TEST_F(smtlib_Functional, define_stmt_jmp_twice)
"STORE 1\n"
"JZ 1\n"
"JNZ 1\n"
"EXIT 1\n"
));
"EXIT 1\n"));
reset_encoder();
......@@ -694,16 +714,17 @@ TEST_F(smtlib_Functional, define_halt)
"JNZ 3\n"
"HALT\n"
"SUBI 1\n"
));
"HALT\n"));
reset_encoder();
encoder->define_halt();
ASSERT_EQ(
"; halt variables - halt_<step>_<thread>\n"
"(assert (= halt_1_0 (or exec_0_0_2 exec_0_0_3 halt_0_0)))\n"
"(assert (= halt_1_1 (or exec_0_1_2 exec_0_1_3 halt_0_1)))\n"
"(assert (= halt_1_2 (or exec_0_2_2 exec_0_2_3 halt_0_2)))\n"
"(assert (= halt_1_0 (or exec_0_0_2 exec_0_0_4 halt_0_0)))\n"
"(assert (= halt_1_1 (or exec_0_1_2 exec_0_1_4 halt_0_1)))\n"
"(assert (= halt_1_2 (or exec_0_2_2 exec_0_2_4 halt_0_2)))\n"
"\n",
encoder->str());
......@@ -715,9 +736,9 @@ TEST_F(smtlib_Functional, define_halt)
verbose = true;
ASSERT_EQ(
"(assert (= halt_1_0 (or exec_0_0_2 exec_0_0_3 halt_0_0)))\n"
"(assert (= halt_1_1 (or exec_0_1_2 exec_0_1_3 halt_0_1)))\n"
"(assert (= halt_1_2 (or exec_0_2_2 exec_0_2_3 halt_0_2)))\n"
"(assert (= halt_1_0 (or exec_0_0_2 exec_0_0_4 halt_0_0)))\n"
"(assert (= halt_1_1 (or exec_0_1_2 exec_0_1_4 halt_0_1)))\n"
"(assert (= halt_1_2 (or exec_0_2_2 exec_0_2_4 halt_0_2)))\n"
"\n",
encoder->str());
}
......@@ -803,8 +824,7 @@ TEST_F(smtlib_Functional, define_exit_flag)
programs.push_back(create_program(
"JNZ 2\n"
"HALT\n"
"EXIT 1\n"
));
"EXIT 1\n"));
reset_encoder();
......@@ -968,8 +988,7 @@ TEST_F(smtlib_Functional, define_states_check_exit)
programs.push_back(
create_program(
"CHECK 0\n"
"EXIT 1\n"
));
"EXIT 1\n"));
reset_encoder();
......
......@@ -99,28 +99,33 @@ TEST_F(Program, parse)
ASSERT_EQ(1, program.label_to_pc.size());
ASSERT_EQ(3, program.label_to_pc[program.pc_to_label[3]]);
ASSERT_EQ("0 STORE 0", program.print(true, 0));
ASSERT_EQ("1 FENCE", program.print(true, 1));
ASSERT_EQ("2 CHECK 0", program.print(true, 2));
ASSERT_EQ("3 LOOP: MEM 0", program.print(true, 3));
ASSERT_EQ("4 ADDI 1", program.print(true, 4));
ASSERT_EQ("5 CAS 0", program.print(true, 5));
ASSERT_EQ("6 JMP LOOP", program.print(true, 6));
ASSERT_EQ(
"0 STORE 0\n"
"1 FENCE\n"
"2 CHECK 0\n"
"3 LOOP: MEM 0\n"
"4 ADDI 1\n"
"5 CAS 0\n"
"6 JMP LOOP\n",
program.print(true));
// indirect addressing
program =
create_from_file<ConcuBinE::Program>("data/indirect.addressing.asm");
ASSERT_EQ(6, program.size());
ASSERT_EQ(7, program.size());
ASSERT_EQ(0, program.checkpoints.size());
ASSERT_EQ(0, program.labels.size());
ASSERT_EQ("0 STORE 1", program.print(true, 0));
ASSERT_EQ("1 ADDI 1", program.print(true, 1));
ASSERT_EQ("2 STORE [1]", program.print(true, 2));
ASSERT_EQ("3 LOAD [0]", program.print(true, 3));
ASSERT_EQ("4 ADD [1]", program.print(true, 4));
ASSERT_EQ("5 CMP [1]", program.print(true, 5));
ASSERT_EQ(
"0 STORE 1\n"
"1 ADDI 1\n"
"2 STORE [1]\n"
"3 LOAD [0]\n"
"4 ADD [1]\n"
"5 CMP [1]\n"
"6 HALT\n",
program.print(true));
}
TEST_F(Program, parse_empty_line)
......
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