Commit 75db0f48 authored by phlo's avatar phlo

renamed Trace::insert_* to Trace::push_back_*

parent 1147797a
# compiler flags
CXX = g++
#CXX = clang++
CFLAGS = -std=c++17 -g -ggdb #-O2
CFLAGS = -std=c++17 \
-g \
-ggdb \
#-O3
CXXFLAGS = $(CFLAGS) $(WFLAGS)
WFLAGS = -pedantic \
-Wall \
......
......@@ -105,34 +105,34 @@ Trace::ptr External::build_trace (const Program::List::ptr & programs)
switch (variable->type)
{
case Variable::Type::THREAD:
trace->insert_thread(
trace->push_back_thread(
variable->step,
variable->thread);
break;
case Variable::Type::EXEC:
trace->insert_pc(
trace->push_back_pc(
variable->step,
variable->thread,
variable->pc);
break;
case Variable::Type::ACCU:
trace->insert_accu(
trace->push_back_accu(
variable->step,
variable->thread,
variable->val);
break;
case Variable::Type::MEM:
trace->insert_mem(
trace->push_back_mem(
variable->step,
variable->thread,
variable->val);
break;
case Variable::Type::HEAP:
trace->insert_heap(
trace->push_back_heap(
variable->step,
{variable->adr, variable->val});
break;
......
......@@ -3,13 +3,6 @@
# - CXXFLAGS
# - OBJ
# link std::filesystem
ifeq ($(CXX),g++)
LDFLAGS += -lstdc++fs
else
LDFLAGS += -lc++fs
endif
# googletest root
GTEST_DIR = lib/googletest/googletest
......@@ -18,11 +11,20 @@ GTEST_LIB = $(GTEST_DIR)/make/gtest-all.o
# compiler flags (exported from parent makefile)
CXXFLAGS += -isystem $(GTEST_DIR)/include \
-I../ \
-pthread \
-lboolector \
-lz3 \
-D__TEST__
-I../ \
-pthread \
-D__TEST__
# linker flags (exported from parent makefile)
LDFLAGS += -lboolector
ifeq ($(CXX),g++)
# std::filesystem
LDFLAGS += -lstdc++fs
else
# std::filesystem
LDFLAGS += -lc++fs
endif
# object files of code to test (exported)
OBJ := $(addprefix ../,$(OBJ))
......@@ -43,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 += Thread.*
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 += Thread.*
# GTEST_FILTER += Simulator.*
# GTEST_FILTER += Main.*
# GTEST_FILTER += Experimental.*
GTEST_FILTER += Instruction.*
GTEST_FILTER += Program.*
# GTEST_FILTER += Instruction.*
# GTEST_FILTER += Program.*
GTEST_FILTER += Trace.*
# GTEST_FILTER += Shell.*
# GTEST_FILTER += Boolector.*
......
......@@ -38,7 +38,7 @@ TEST_F(Boolector, unsat)
ASSERT_EQ("unsat\n", boolector.std_out.str());
}
TEST_F(Boolector, solve_check)
TEST_F(Boolector, DISABLED_solve_check)
{
// concurrent increment using CHECK
std::string increment_0 = "data/increment.check.thread.0.asm";
......@@ -115,7 +115,6 @@ TEST_F(Boolector, solve_check)
std::ofstream file {"/tmp/test.trace"};
file << trace->print();
file.close();
Trace::ptr parsed =
std::make_unique<Trace>(create_from_file<Trace>("/tmp/test.trace"));
......@@ -192,7 +191,7 @@ TEST_F(Boolector, DISABLED_solve_cas)
trace->print());
}
TEST_F(Boolector, encode_deadlock)
TEST_F(Boolector, DISABLED_encode_deadlock)
{
// deadlock after 3 steps -> unsat
programs->push_back(create_from_file<Program>("data/deadlock.thread.0.asm"));
......@@ -205,4 +204,50 @@ TEST_F(Boolector, encode_deadlock)
ASSERT_FALSE(boolector.sat(formula));
}
// TODO: remove
TEST_F(Boolector, print_model_check)
{
// concurrent increment using CHECK
std::string increment_0 = "data/increment.check.thread.0.asm";
std::string increment_n = "data/increment.check.thread.n.asm";
programs = std::make_shared<Program::List>();
programs->push_back(create_from_file<Program>(increment_0));
programs->push_back(create_from_file<Program>(increment_n));
encoder = std::make_unique<smtlib::Functional>(programs, 12);
std::string formula = boolector.build_formula(*encoder, constraints);
bool sat = boolector.sat(formula);
std::ofstream outfile("/tmp/boolector.check.out");
outfile << boolector.std_out.str();
ASSERT_TRUE(sat);
}
TEST_F(Boolector, print_model_cas)
{
// concurrent increment using CAS
std::string increment_cas = "data/increment.cas.asm";
programs = std::make_shared<Program::List>();
programs->push_back(create_from_file<Program>(increment_cas));
programs->push_back(create_from_file<Program>(increment_cas));
encoder = std::make_unique<smtlib::Functional>(programs, 12);
std::string formula = boolector.build_formula(*encoder, constraints);
bool sat = boolector.sat(formula);
std::ofstream outfile("/tmp/boolector.cas.out");
outfile << boolector.std_out.str();
ASSERT_TRUE(sat);
}
} // namespace test
......@@ -47,7 +47,7 @@ TEST_F(BtorMC, unsat)
ASSERT_EQ("", btormc.std_out.str());
}
TEST_F(BtorMC, solve_check)
TEST_F(BtorMC, DISABLED_solve_check)
{
// concurrent increment using CHECK
std::string constraints;
......@@ -205,4 +205,50 @@ TEST_F(BtorMC, DISABLED_solve_cas)
trace->print());
}
// TODO: remove
TEST_F(BtorMC, print_model_check)
{
// concurrent increment using CHECK
std::string increment_0 = "data/increment.check.thread.0.asm";
std::string increment_n = "data/increment.check.thread.n.asm";
programs = std::make_shared<Program::List>();
programs->push_back(create_from_file<Program>(increment_0));
programs->push_back(create_from_file<Program>(increment_n));
encoder = std::make_unique<btor2::Encoder>(programs, 12);
std::string formula = btormc.build_formula(*encoder, "");
bool sat = btormc.sat(formula);
std::ofstream outfile("/tmp/btormc.check.out");
outfile << btormc.std_out.str();
ASSERT_TRUE(sat);
}
TEST_F(BtorMC, print_model_cas)
{
// concurrent increment using CAS
std::string increment_cas = "data/increment.cas.asm";
programs = std::make_shared<Program::List>();
programs->push_back(create_from_file<Program>(increment_cas));
programs->push_back(create_from_file<Program>(increment_cas));
encoder = std::make_unique<btor2::Encoder>(programs, 12);
std::string formula = btormc.build_formula(*encoder, "");
bool sat = btormc.sat(formula);
std::ofstream outfile("/tmp/btormc.cas.out");
outfile << btormc.std_out.str();
ASSERT_TRUE(sat);
}
} // namespace test
......@@ -51,7 +51,7 @@ TEST_F(CVC4, unsat)
}
// TODO: remove
TEST_F(CVC4, print_model)
TEST_F(CVC4, print_model_check)
{
// concurrent increment using CHECK
std::string constraints;
......@@ -69,7 +69,31 @@ TEST_F(CVC4, print_model)
bool sat = cvc4.sat(formula);
std::cout << cvc4.std_out.str();
std::ofstream outfile("/tmp/cvc4.check.out");
outfile << cvc4.std_out.str();
ASSERT_TRUE(sat);
}
TEST_F(CVC4, print_model_cas)
{
// concurrent increment using CAS
std::string constraints;
std::string increment_cas = "data/increment.cas.asm";
Program::List::ptr programs = std::make_shared<Program::List>();
programs->push_back(create_from_file<Program>(increment_cas));
programs->push_back(create_from_file<Program>(increment_cas));
Encoder::ptr encoder = std::make_unique<smtlib::Functional>(programs, 12);
std::string formula = cvc4.build_formula(*encoder, constraints);
bool sat = cvc4.sat(formula);
std::ofstream outfile("/tmp/cvc4.cas.out");
outfile << cvc4.std_out.str();
ASSERT_TRUE(sat);
}
......
......@@ -781,9 +781,7 @@ TEST_F(Trace, parse_missing_heap)
// Trace::push_back ============================================================
using Insert_Data = std::tuple<bound_t, word_t, word_t, word_t>;
const std::vector<Insert_Data> insert_data {
const std::vector<std::tuple<bound_t, word_t, word_t, word_t>> data {
{1, 0, 0, 0},
{2, 1, 0, 0},
{3, 0, 0, 0},
......@@ -802,16 +800,16 @@ const std::vector<Insert_Data> insert_data {
{16, 1, 1, 1},
};
// Trace::insert_thread ========================================================
// Trace::push_back_thread =====================================================
TEST_F(Trace, insert_thread)
TEST_F(Trace, push_back_thread)
{
create_dummy_trace(2);
for (const auto & [step, thread, _, __] : insert_data)
trace->insert_thread(step, thread);
for (const auto & [step, thread, _, __] : data)
trace->push_back_thread(step, thread);
ASSERT_EQ(insert_data.size(), trace->bound);
ASSERT_EQ(data.size(), trace->bound);
ASSERT_EQ(
::Trace::Updates<word_t> ({
{1, 0},
......@@ -834,104 +832,104 @@ TEST_F(Trace, insert_thread)
trace->thread_updates);
}
// Trace::insert_pc ============================================================
// Trace::push_back_pc =========================================================
const std::vector<::Trace::Updates<word_t>> insert_expected {
const std::vector<::Trace::Updates<word_t>> push_back_expected {
{{1, 0}, {5, 1}, {9, 0}, {13, 1}},
{{2, 0}, {6, 1}, {10, 0}, {14, 1}}
};
TEST_F(Trace, insert_pc)
TEST_F(Trace, push_back_pc)
{
create_dummy_trace(2);
for (const auto & [step, thread, pc, _] : insert_data)
trace->insert_pc(step, thread, pc);
for (const auto & [step, thread, pc, _] : data)
trace->push_back_pc(step, thread, pc);
ASSERT_EQ(insert_data.size(), trace->bound);
ASSERT_EQ(insert_expected, trace->pc_updates);
ASSERT_EQ(data.size(), trace->bound);
ASSERT_EQ(push_back_expected, trace->pc_updates);
}
// Trace::insert_accu ==========================================================
// Trace::push_back_accu =======================================================
TEST_F(Trace, insert_accu)
TEST_F(Trace, push_back_accu)
{
create_dummy_trace(2);
for (const auto & [step, thread, accu, _] : insert_data)
trace->insert_accu(step, thread, accu);
for (const auto & [step, thread, accu, _] : data)
trace->push_back_accu(step, thread, accu);
ASSERT_EQ(insert_data.size(), trace->bound);
ASSERT_EQ(insert_expected, trace->accu_updates);
ASSERT_EQ(data.size(), trace->bound);
ASSERT_EQ(push_back_expected, trace->accu_updates);
}
// Trace::insert_mem ===========================================================
// Trace::push_back_mem ========================================================
TEST_F(Trace, insert_mem)
TEST_F(Trace, push_back_mem)
{
create_dummy_trace(2);
for (const auto & [step, thread, mem, _] : insert_data)
trace->insert_mem(step, thread, mem);
for (const auto & [step, thread, mem, _] : data)
trace->push_back_mem(step, thread, mem);
ASSERT_EQ(insert_data.size(), trace->bound);
ASSERT_EQ(insert_expected, trace->mem_updates);
ASSERT_EQ(data.size(), trace->bound);
ASSERT_EQ(push_back_expected, trace->mem_updates);
}
// Trace::insert_sb_adr ========================================================
// Trace::push_back_sb_adr =====================================================
TEST_F(Trace, insert_sb_adr)
TEST_F(Trace, push_back_sb_adr)
{
create_dummy_trace(2);
for (const auto & [step, thread, adr, _] : insert_data)
trace->insert_sb_adr(step, thread, adr);
for (const auto & [step, thread, adr, _] : data)
trace->push_back_sb_adr(step, thread, adr);
ASSERT_EQ(insert_data.size(), trace->bound);
ASSERT_EQ(insert_expected, trace->sb_adr_updates);
ASSERT_EQ(data.size(), trace->bound);
ASSERT_EQ(push_back_expected, trace->sb_adr_updates);
}
// Trace::insert_sb_val ========================================================
// Trace::push_back_sb_val =====================================================
TEST_F(Trace, insert_sb_val)
TEST_F(Trace, push_back_sb_val)
{
create_dummy_trace(2);
for (const auto & [step, thread, adr, _] : insert_data)
trace->insert_sb_val(step, thread, adr);
for (const auto & [step, thread, adr, _] : data)
trace->push_back_sb_val(step, thread, adr);
ASSERT_EQ(insert_data.size(), trace->bound);
ASSERT_EQ(insert_expected, trace->sb_val_updates);
ASSERT_EQ(data.size(), trace->bound);
ASSERT_EQ(push_back_expected, trace->sb_val_updates);
}
// Trace::insert_sb_full =======================================================
// Trace::push_back_sb_full ====================================================
TEST_F(Trace, insert_sb_full)
TEST_F(Trace, push_back_sb_full)
{
create_dummy_trace(2);
for (const auto & [step, thread, full, _] : insert_data)
trace->insert_sb_full(step, thread, full);
for (const auto & [step, thread, full, _] : data)
trace->push_back_sb_full(step, thread, full);
const std::vector<::Trace::Updates<bool>> expected {
{{1, 0}, {5, 1}, {9, 0}, {13, 1}},
{{2, 0}, {6, 1}, {10, 0}, {14, 1}}
};
ASSERT_EQ(insert_data.size(), trace->bound);
ASSERT_EQ(data.size(), trace->bound);
ASSERT_EQ(expected, trace->sb_full_updates);
}
// Trace::insert_heap ==========================================================
// Trace::push_back_heap =======================================================
TEST_F(Trace, insert_heap)
TEST_F(Trace, push_back_heap)
{
create_dummy_trace(2);
for (const auto & [step, thread, idx, val] : insert_data)
trace->insert_heap(step, {idx, val});
for (const auto & [step, thread, idx, val] : data)
trace->push_back_heap(step, {idx, val});
ASSERT_EQ(insert_data.size(), trace->bound);
ASSERT_EQ(data.size(), trace->bound);
ASSERT_EQ(
::Trace::Heap_Updates ({
{0, {{1, 0}, {9, 1}}},
......
......@@ -413,9 +413,9 @@ void Trace::push_back (const word_t thread, const Heap & heap)
push_back<word_t>(heap_updates[heap.adr], bound, heap.val);
}
// Trace::insert_thread --------------------------------------------------------
// Trace::push_back_thread -----------------------------------------------------
void Trace::insert_thread (const bound_t step, const word_t thread)
void Trace::push_back_thread (const bound_t step, const word_t thread)
{
push_back<word_t>(thread_updates, step, thread);
......@@ -423,9 +423,11 @@ void Trace::insert_thread (const bound_t step, const word_t thread)
bound = step;
}
// Trace::insert_pc ------------------------------------------------------------
// Trace::push_back_pc ---------------------------------------------------------
void Trace::insert_pc (const bound_t step, const word_t thread, const word_t pc)
void Trace::push_back_pc (const bound_t step,
const word_t thread,
const word_t pc)
{
push_back<word_t>(pc_updates.at(thread), step, pc);
......@@ -433,11 +435,11 @@ void Trace::insert_pc (const bound_t step, const word_t thread, const word_t pc)
bound = step;
}
// Trace::insert_accu ----------------------------------------------------------
// Trace::push_back_accu -------------------------------------------------------
void Trace::insert_accu (const bound_t step,
const word_t thread,
const word_t accu)
void Trace::push_back_accu (const bound_t step,
const word_t thread,
const word_t accu)
{
push_back<word_t>(accu_updates.at(thread), step, accu);
......@@ -445,11 +447,11 @@ void Trace::insert_accu (const bound_t step,
bound = step;
}
// Trace::insert_mem -----------------------------------------------------------
// Trace::push_back_mem --------------------------------------------------------
void Trace::insert_mem (const bound_t step,
const word_t thread,
const word_t mem)
void Trace::push_back_mem (const bound_t step,
const word_t thread,
const word_t mem)
{
push_back<word_t>(mem_updates.at(thread), step, mem);
......@@ -457,11 +459,11 @@ void Trace::insert_mem (const bound_t step,
bound = step;
}
// Trace::insert_sb_adr --------------------------------------------------------
// Trace::push_back_sb_adr -----------------------------------------------------
void Trace::insert_sb_adr (const bound_t step,
const word_t thread,
const word_t adr)
void Trace::push_back_sb_adr (const bound_t step,
const word_t thread,
const word_t adr)
{
push_back<word_t>(sb_adr_updates.at(thread), step, adr);
......@@ -469,11 +471,11 @@ void Trace::insert_sb_adr (const bound_t step,
bound = step;
}
// Trace::insert_sb_val --------------------------------------------------------
// Trace::push_back_sb_val -----------------------------------------------------
void Trace::insert_sb_val (const bound_t step,
const word_t thread,
const word_t val)
void Trace::push_back_sb_val (const bound_t step,
const word_t thread,
const word_t val)
{
push_back<word_t>(sb_val_updates.at(thread), step, val);
......@@ -481,11 +483,11 @@ void Trace::insert_sb_val (const bound_t step,
bound = step;
}
// Trace::insert_sb_full -------------------------------------------------------
// Trace::push_back_sb_full ----------------------------------------------------
void Trace::insert_sb_full (const bound_t step,
const word_t thread,
const bool full)
void Trace::push_back_sb_full (const bound_t step,
const word_t thread,
const bool full)
{
push_back<bool>(sb_full_updates.at(thread), step, full);
......@@ -493,9 +495,9 @@ void Trace::insert_sb_full (const bound_t step,
bound = step;
}
// Trace::insert_heap ----------------------------------------------------------
// Trace::push_back_heap -------------------------------------------------------
void Trace::insert_heap (const bound_t step, const Heap & heap)
void Trace::push_back_heap (const bound_t step, const Heap & heap)
{
push_back<word_t>(heap_updates[heap.adr], step, heap.val);
......@@ -503,9 +505,9 @@ void Trace::insert_heap (const bound_t step, const Heap & heap)
bound = step;
}
// Trace::insert_flush ---------------------------------------------------------
// Trace::push_back_flush ---------------------------------------------------------
void Trace::insert_flush (const bound_t step)
void Trace::push_back_flush (const bound_t step)
{
flushes.insert(step);
......
......@@ -219,19 +219,17 @@ struct Trace
//
void push_back (word_t thread, const Heap & heap);
// insert individual state updates
// append individual state updates
//
// NOTE: expects step to increase monotonically
//
void insert_thread (bound_t step, word_t thread);
void insert_pc (bound_t step, word_t thread, word_t pc);
void insert_accu (bound_t step, word_t thread, word_t accu);
void insert_mem (bound_t step, word_t thread, word_t mem);
void insert_sb_adr (bound_t step, word_t thread, word_t adr);
void insert_sb_val (bound_t step, word_t thread, word_t val);
void insert_sb_full (bound_t step, word_t thread, bool full);
void insert_heap (bound_t step, const Heap & heap);
void insert_flush (const bound_t step);
void push_back_thread (bound_t step, word_t thread);
void push_back_pc (bound_t step, word_t thread, word_t pc);
void push_back_accu (bound_t step, word_t thread, word_t accu);
void push_back_mem (bound_t step, word_t thread, word_t mem);
void push_back_sb_adr (bound_t step, word_t thread, word_t adr);
void push_back_sb_val (bound_t step, word_t thread, word_t val);
void push_back_sb_full (bound_t step, word_t thread, bool full);
void push_back_heap (bound_t step, const Heap & heap);
void push_back_flush (const bound_t step);
// return trace size (bound)
//
......
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