Commit c886a154 authored by phlo's avatar phlo

fixed copying mmap in Simulator::replay

parent a795531b
......@@ -477,6 +477,10 @@ Trace::ptr Simulator::replay (const Trace & trace, const size_t bound)
{},
bound && bound < trace.length ? bound : trace.length - 1);
// copy memory map
if (trace.mmap)
s.trace->mmap = trace.mmap;
// replay scheduler
Trace::iterator it = trace.begin();
......
......@@ -46,7 +46,7 @@ TEST_F(Boolector, solve_check)
trace = boolector.solve(*encoder);
std::cout << "time to solve = " << boolector.time << " ms" << eol;
// std::cout << "time to solve = " << boolector.time << " ms" << eol;
// std::cout << trace->print();
......@@ -73,7 +73,7 @@ TEST_F(Boolector, solve_cas)
trace = boolector.solve(*encoder);
std::cout << "time to solve = " << boolector.time << " ms" << eol;
// std::cout << "time to solve = " << boolector.time << " ms" << eol;
// std::cout << trace->print();
......@@ -106,15 +106,15 @@ TEST_F(Boolector, solve_indirect_uninitialized)
trace = boolector.solve(*encoder);
std::cout << "time to solve = " << boolector.time << " ms" << eol;
// std::cout << "time to solve = " << boolector.time << " ms" << eol;
std::cout << trace->print();
// std::cout << trace->print();
Simulator simulator (programs);
Trace::ptr replay (simulator.replay(*trace));
std::cout << replay->print();
// std::cout << replay->print();
ASSERT_EQ(*replay, *trace);
}
......
......@@ -58,7 +58,7 @@ TEST_F(BtorMC, solve_check)
trace = btormc.solve(*encoder);
std::cout << "time to solve = " << btormc.time << " ms" << eol;
// std::cout << "time to solve = " << btormc.time << " ms" << eol;
// std::cout << trace->print();
......@@ -85,7 +85,7 @@ TEST_F(BtorMC, solve_cas)
trace = btormc.solve(*encoder);
std::cout << "time to solve = " << btormc.time << " ms" << eol;
// std::cout << "time to solve = " << btormc.time << " ms" << eol;
// std::cout << trace->print();
......@@ -118,15 +118,15 @@ TEST_F(BtorMC, solve_indirect_uninitialized)
trace = btormc.solve(*encoder);
std::cout << "time to solve = " << btormc.time << " ms" << eol;
// std::cout << "time to solve = " << btormc.time << " ms" << eol;
std::cout << trace->print();
// std::cout << trace->print();
Simulator simulator (programs);
Trace::ptr replay (simulator.replay(*trace));
std::cout << replay->print();
// std::cout << replay->print();
ASSERT_EQ(*replay, *trace);
}
......
......@@ -46,7 +46,7 @@ TEST_F(CVC4, solve_check)
trace = cvc4.solve(*encoder);
std::cout << "time to solve = " << cvc4.time << " ms" << eol;
// std::cout << "time to solve = " << cvc4.time << " ms" << eol;
// std::cout << trace->print();
......@@ -71,7 +71,7 @@ TEST_F(CVC4, solve_cas)
trace = cvc4.solve(*encoder);
std::cout << "time to solve = " << cvc4.time << " ms" << eol;
// std::cout << "time to solve = " << cvc4.time << " ms" << eol;
// std::cout << trace->print();
......@@ -84,39 +84,6 @@ TEST_F(CVC4, solve_cas)
ASSERT_EQ(*replay, *trace);
}
TEST_F(CVC4, DISABLED_solve_multiple_addresses)
{
std::istringstream p0 (
"STORE 0\n"
"ADDI 1\n"
"STORE 0\n"
"HALT\n");
std::istringstream p1 (
"STORE 1\n"
"ADDI 1\n"
"STORE 1\n"
"HALT\n");
programs->push_back(Program(p0, "load.store.0.asm"));
programs->push_back(Program(p1, "load.store.1.asm"));
encoder = std::make_unique<smtlib::Functional>(programs, 16);
trace = cvc4.solve(*encoder);
std::cout << "time to solve = " << cvc4.time << " ms" << eol;
std::cout << trace->print();
Simulator simulator (programs);
Trace::ptr replay (simulator.replay(*trace));
std::cout << replay->print();
ASSERT_EQ(*replay, *trace);
}
TEST_F(CVC4, solve_indirect_uninitialized)
{
std::istringstream p0 (
......@@ -137,15 +104,15 @@ TEST_F(CVC4, solve_indirect_uninitialized)
trace = cvc4.solve(*encoder);
std::cout << "time to solve = " << cvc4.time << " ms" << eol;
// std::cout << "time to solve = " << cvc4.time << " ms" << eol;
std::cout << trace->print();
// std::cout << trace->print();
Simulator simulator (programs);
Trace::ptr replay (simulator.replay(*trace));
std::cout << replay->print();
// std::cout << replay->print();
ASSERT_EQ(*replay, *trace);
}
......@@ -190,61 +157,4 @@ TEST_F(CVC4, print_model_cas)
ASSERT_TRUE(sat);
}
TEST_F(CVC4, DISABLED_print_multiple_addresses)
{
std::istringstream p0 (
"STORE 0\n"
"ADDI 1\n"
"STORE 0\n"
"HALT\n");
std::istringstream p1 (
"STORE 1\n"
"ADDI 1\n"
"STORE 1\n"
"HALT\n");
programs->push_back(Program(p0, "dummy.asm"));
programs->push_back(Program(p1, "dummy.asm"));
encoder = std::make_unique<smtlib::Functional>(programs, 16);
bool sat = cvc4.sat(cvc4.build_formula(*encoder, ""));
std::ofstream outfile("/tmp/cvc4.multiple-addresses.out");
outfile << cvc4.std_out.str();
ASSERT_TRUE(sat);
}
TEST_F(CVC4, DISABLED_print_indirect_uninitialized)
{
std::istringstream p0 (
"LOAD [0]\n"
"ADDI 1\n"
"STORE [0]\n"
"HALT\n");
std::istringstream p1 (
"LOAD [1]\n"
"ADDI 1\n"
"STORE [1]\n"
"HALT\n");
programs->push_back(Program(p0, "dummy.asm"));
programs->push_back(Program(p1, "dummy.asm"));
encoder = std::make_unique<smtlib::Functional>(programs, 16);
std::string formula = cvc4.build_formula(*encoder, "");
std::ofstream f("/tmp/cvc4.indirect.uninitialized.smt2");
f << formula;
bool sat = cvc4.sat(formula);
std::ofstream outfile("/tmp/cvc4.indirect.uninitialized.out");
outfile << cvc4.std_out.str();
ASSERT_TRUE(sat);
}
} // namespace ConcuBinE::test
......@@ -45,7 +45,7 @@ TEST_F(Z3, solve_check)
trace = z3.solve(*encoder, constraints);
std::cout << "time to solve = " << z3.time << " ms" << eol;
// std::cout << "time to solve = " << z3.time << " ms" << eol;
// std::cout << trace->print();
......@@ -73,7 +73,7 @@ TEST_F(Z3, solve_cas)
trace = z3.solve(*encoder, constraints);
std::cout << "time to solve = " << z3.time << " ms" << eol;
// std::cout << "time to solve = " << z3.time << " ms" << eol;
// std::cout << trace->print();
......@@ -106,15 +106,15 @@ TEST_F(Z3, solve_indirect_uninitialized)
trace = z3.solve(*encoder);
std::cout << "time to solve = " << z3.time << " ms" << eol;
// std::cout << "time to solve = " << z3.time << " ms" << eol;
std::cout << trace->print();
// std::cout << trace->print();
Simulator simulator (programs);
Trace::ptr replay (simulator.replay(*trace));
std::cout << replay->print();
// std::cout << replay->print();
ASSERT_EQ(*replay, *trace);
}
......
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