Commit e9eca300 authored by phlo's avatar phlo

clarified Trace member names

parent 75db0f48
......@@ -2,7 +2,7 @@
#include "encoder.hh"
BtorMC::BtorMC(bound_t b) : bound(b) {}
BtorMC::BtorMC(size_t b) : bound(b) {}
std::string BtorMC::name () const { return "btormc"; }
......
......@@ -5,9 +5,9 @@
struct BtorMC : public Boolector
{
BtorMC (bound_t);
BtorMC (size_t);
const bound_t bound;
const size_t bound;
virtual std::string build_command ();
......
......@@ -13,10 +13,6 @@
using word_t = uint16_t;
using sword_t = int16_t; // signed
// model checking step
//
using bound_t = uint64_t;
//==============================================================================
// global variables
//==============================================================================
......
......@@ -48,7 +48,7 @@ const std::string Encoder::check_comment = "checkpoint variables";
// constructors
//------------------------------------------------------------------------------
Encoder::Encoder (const Program::List::ptr & p, bound_t b) :
Encoder::Encoder (const Program::List::ptr & p, size_t b) :
programs(p),
num_threads(p->size()),
bound(b),
......
......@@ -97,7 +97,7 @@ struct Encoder
// bound
//
const bound_t bound;
const size_t bound;
// use Sinz's cardinality constraint (num_threads > 4)
//
......@@ -147,7 +147,7 @@ struct Encoder
// constructors
//----------------------------------------------------------------------------
Encoder (const Program::List::ptr & programs, bound_t bound);
Encoder (const Program::List::ptr & programs, size_t bound);
//----------------------------------------------------------------------------
// private member functions
......@@ -283,17 +283,17 @@ struct Encoder : public ::Encoder
// current step
//
bound_t step;
size_t step;
// previous step (reduce subtractions)
//
bound_t prev;
size_t prev;
//----------------------------------------------------------------------------
// constructors
//----------------------------------------------------------------------------
Encoder (const Program::List::ptr & programs, bound_t bound);
Encoder (const Program::List::ptr & programs, size_t bound);
//----------------------------------------------------------------------------
// private member functions
......@@ -450,7 +450,7 @@ struct Functional : public Encoder
//----------------------------------------------------------------------------
Functional (const Program::List::ptr & programs,
bound_t bound,
size_t bound,
bool encode = true);
//----------------------------------------------------------------------------
......@@ -524,7 +524,7 @@ struct Relational : public Encoder
//----------------------------------------------------------------------------
Relational (const Program::List::ptr & programs,
bound_t bound,
size_t bound,
bool encode = true);
//----------------------------------------------------------------------------
......@@ -806,7 +806,7 @@ struct Encoder : public ::Encoder
//----------------------------------------------------------------------------
Encoder (const Program::List::ptr & programs,
bound_t bound,
size_t bound,
bool encode = true);
//----------------------------------------------------------------------------
......
......@@ -103,7 +103,7 @@ const std::string Encoder::msb = std::to_string(word_size - 1);
// constructors
//------------------------------------------------------------------------------
Encoder::Encoder (const Program::List::ptr & p, const bound_t b, const bool e) :
Encoder::Encoder (const Program::List::ptr & p, const size_t b, const bool e) :
::Encoder(p, b),
node(1)
{
......
......@@ -86,7 +86,7 @@ const std::string Encoder::check_comment =
// constructors
//------------------------------------------------------------------------------
Encoder::Encoder (const Program::List::ptr & p, const bound_t b) :
Encoder::Encoder (const Program::List::ptr & p, const size_t b) :
::Encoder(p, b),
step(0)
{}
......@@ -938,7 +938,7 @@ void Encoder::encode ()
{
formula << set_logic() << eol << eol;
for (step = 0, prev = static_cast<bound_t>(-1); step <= bound; step++, prev++)
for (step = 0, prev = static_cast<size_t>(-1); step <= bound; step++, prev++)
{
if (verbose)
formula << comment_section("step " + std::to_string(step));
......
......@@ -15,7 +15,7 @@ namespace smtlib {
//------------------------------------------------------------------------------
Functional::Functional (const Program::List::ptr & p,
const bound_t b,
const size_t b,
const bool e) :
Encoder(p, b)
{
......@@ -303,7 +303,7 @@ void Functional::define_exit_code ()
std::string expr = word2hex(0);
if (!exit_pcs.empty())
for (bound_t k = step = bound; k > 0; k--)
for (size_t k = step = bound; k > 0; k--)
iterate_programs_reverse([this, &expr, k] (const Program & program) {
for (const word_t & exit_pc : exit_pcs[thread])
expr =
......
......@@ -77,7 +77,7 @@ Relational::State::operator std::string () const
//------------------------------------------------------------------------------
Relational::Relational (const Program::List::ptr & p,
const bound_t b,
const size_t b,
const bool e) :
Encoder(p, b)
{
......
......@@ -129,7 +129,7 @@ int help (const char * name, const int argc, const char **argv)
int simulate (const char * name, const int argc, const char ** argv)
{
bound_t bound = 0;
size_t bound = 0;
uint64_t seed = static_cast<uint64_t>(time(NULL));
Program::List::ptr programs = std::make_shared<Program::List>();
......@@ -213,7 +213,7 @@ int simulate (const char * name, const int argc, const char ** argv)
int replay (const char * name, const int argc, const char ** argv)
{
bound_t bound = 0;
size_t bound = 0;
std::string trace_path;
for (int i = 0; i < argc; i++)
......@@ -373,7 +373,7 @@ int solve (const char * name, const int argc, const char ** argv)
}
// parse bound
bound_t bound = 0;
size_t bound = 0;
try
{
bound = std::stoul(argv[i++], nullptr, 0);
......
......@@ -25,7 +25,7 @@ inline void erase (C & container, T & val)
//------------------------------------------------------------------------------
Simulator::Simulator (const Program::List::ptr & p,
const bound_t b,
const size_t b,
const uint64_t s) :
programs(p),
trace(std::make_unique<Trace>(p)),
......@@ -172,8 +172,8 @@ Trace::ptr Simulator::run (std::function<Thread *()> scheduler)
// Simulator::simulate ---------------------------------------------------------
Trace::ptr Simulator::simulate (const Program::List::ptr & programs,
const bound_t bound,
const bound_t seed)
const size_t bound,
const size_t seed)
{
Simulator simulator {programs, bound, seed};
......@@ -197,7 +197,7 @@ Trace::ptr Simulator::simulate (const Program::List::ptr & programs,
// Simulator::replay -----------------------------------------------------------
Trace::ptr Simulator::replay (const Trace & trace, const bound_t bound)
Trace::ptr Simulator::replay (const Trace & trace, const size_t bound)
{
Simulator simulator {
trace.programs,
......@@ -456,7 +456,7 @@ void Thread::execute (const Instruction::Mem & m)
void Thread::execute (const Instruction::Cas & c)
{
std::optional<Trace::Heap> heap;
std::optional<Trace::cell_t> heap;
if (mem == load(c.arg, c.indirect))
{
......
......@@ -34,7 +34,7 @@ struct Simulator
// bound
//
bound_t bound;
size_t bound;
// seed used for random thread scheduling
//
......@@ -73,7 +73,7 @@ struct Simulator
//----------------------------------------------------------------------------
Simulator (const Program::List::ptr & programs,
bound_t bound = 0,
size_t bound = 0,
uint64_t seed = 0);
//----------------------------------------------------------------------------
......@@ -99,12 +99,12 @@ struct Simulator
// runs the simulator using a random trace
//
static Trace::ptr simulate (const Program::List::ptr & programs,
bound_t bound = 0,
size_t bound = 0,
uint64_t seed = 0);
// replay the given trace (trace must match simulator configuration)
//
static Trace::ptr replay (const Trace & trace, bound_t bound = 0);
static Trace::ptr replay (const Trace & trace, size_t bound = 0);
};
//==============================================================================
......
......@@ -10,9 +10,9 @@
// Solver::parse_attribute -----------------------------------------------------
bound_t Solver::parse_attribute (std::istringstream & line,
const std::string & name,
const char delimiter)
size_t Solver::parse_attribute (std::istringstream & line,
const std::string & name,
const char delimiter)
{
std::string token;
......
......@@ -22,9 +22,9 @@ struct Solver
// member functions
//----------------------------------------------------------------------------
bound_t parse_attribute (std::istringstream & line,
const std::string & name,
char delimiter = '_');
size_t parse_attribute (std::istringstream & line,
const std::string & name,
char delimiter = '_');
// build formula for the specific solver
//
......@@ -70,12 +70,12 @@ struct External : public Solver
EXIT_CODE
};
Type type;
bound_t step;
word_t thread;
word_t pc;
word_t adr;
word_t val;
Type type;
size_t step;
word_t thread;
word_t pc;
word_t adr;
word_t val;
};
//----------------------------------------------------------------------------
......
......@@ -119,10 +119,10 @@ TEST_F(Boolector, DISABLED_solve_check)
Trace::ptr parsed =
std::make_unique<Trace>(create_from_file<Trace>("/tmp/test.trace"));
std::vector<std::vector<std::pair<bound_t, word_t>>> pc_diff;
std::vector<std::vector<std::pair<size_t, word_t>>> pc_diff;
for (size_t t = 0; t < trace->pc_updates.size(); t++)
{
std::vector<std::pair<bound_t, word_t>> diff;
std::vector<std::pair<size_t, word_t>> diff;
std::set_symmetric_difference(
trace->pc_updates[t].begin(), trace->pc_updates[t].end(),
......
......@@ -131,10 +131,10 @@ TEST_F(BtorMC, DISABLED_solve_check)
Trace::ptr parsed =
std::make_unique<Trace>(create_from_file<Trace>("/tmp/test.trace"));
std::vector<std::vector<std::pair<bound_t, word_t>>> pc_diff;
std::vector<std::vector<std::pair<size_t, word_t>>> pc_diff;
for (size_t t = 0; t < trace->pc_updates.size(); t++)
{
std::vector<std::pair<bound_t, word_t>> diff;
std::vector<std::pair<size_t, word_t>> diff;
std::set_symmetric_difference(
trace->pc_updates[t].begin(), trace->pc_updates[t].end(),
......
......@@ -18,7 +18,7 @@ struct Encoder: public ::testing::Test
return e;
}
std::unique_ptr<E> create_encoder (const bound_t bound = 1)
std::unique_ptr<E> create_encoder (const size_t bound = 1)
{
return
init_encoder(
......@@ -35,7 +35,7 @@ struct Encoder: public ::testing::Test
return Program(inbuf, path);
}
void reset_encoder (const bound_t bound = 1)
void reset_encoder (const size_t bound = 1)
{
encoder = create_encoder(bound);
}
......@@ -79,7 +79,7 @@ struct Encoder: public ::testing::Test
void encode (const std::initializer_list<std::string> _programs,
const std::string file,
const bound_t bound,
const size_t bound,
const char * dir = "data/")
{
for (const auto & p : _programs)
......
......@@ -73,7 +73,7 @@ TEST_F(Simulator, run_simple)
ASSERT_TRUE(simulator->threads_per_checkpoint.empty());
ASSERT_TRUE(simulator->waiting_for_checkpoint.empty());
bound_t step = 0;
size_t step = 0;
// NOTE: EXPECT_* required by lambda std::function
std::function<Thread *()> scheduler = [&] () -> Thread *
......@@ -125,30 +125,30 @@ TEST_F(Simulator, run_simple)
ASSERT_EQ(0, trace->exit);
ASSERT_EQ(
Trace::Thread_Updates<word_t>({{{1, 0}}, {{2, 0}}}),
Trace::thread_states<word_t>({{{1, 0}}, {{2, 0}}}),
trace->pc_updates);
ASSERT_EQ(
Trace::Thread_Updates<word_t>({{{1, 1}}, {{2, 1}}}),
Trace::thread_states<word_t>({{{1, 1}}, {{2, 1}}}),
trace->accu_updates);
ASSERT_EQ(
Trace::Thread_Updates<word_t>({{{1, 0}}, {{2, 0}}}),
Trace::thread_states<word_t>({{{1, 0}}, {{2, 0}}}),
trace->mem_updates);
ASSERT_EQ(
Trace::Thread_Updates<word_t>({{{1, 0}}, {{2, 0}}}),
Trace::thread_states<word_t>({{{1, 0}}, {{2, 0}}}),
trace->sb_adr_updates);
ASSERT_EQ(
Trace::Thread_Updates<word_t>({{{1, 0}}, {{2, 0}}}),
Trace::thread_states<word_t>({{{1, 0}}, {{2, 0}}}),
trace->sb_val_updates);
ASSERT_EQ(
Trace::Thread_Updates<bool>({{{1, false}}, {{2, false}}}),
Trace::thread_states<bool>({{{1, false}}, {{2, false}}}),
trace->sb_full_updates);
ASSERT_EQ(Trace::Flushes(), trace->flushes);
ASSERT_EQ(std::unordered_set<size_t>(), trace->flushes);
ASSERT_TRUE(trace->heap_updates.empty());
}
......@@ -166,7 +166,7 @@ TEST_F(Simulator, run_add_check_exit)
ASSERT_EQ(2, simulator->threads_per_checkpoint[1].size());
ASSERT_EQ(0, simulator->waiting_for_checkpoint[1]);
bound_t step = 0;
size_t step = 0;
std::function<Thread *()> scheduler = [&] () -> Thread *
{
......@@ -244,32 +244,32 @@ TEST_F(Simulator, run_add_check_exit)
ASSERT_EQ(1, trace->exit);
ASSERT_EQ(
Trace::Thread_Updates<word_t>({
Trace::thread_states<word_t>({
{{1, 0}, {3, 1}, {5, 2}},
{{2, 0}, {4, 1}}}),
trace->pc_updates);
ASSERT_EQ(
Trace::Thread_Updates<word_t>({{{1, 1}}, {{2, 1}}}),
Trace::thread_states<word_t>({{{1, 1}}, {{2, 1}}}),
trace->accu_updates);
ASSERT_EQ(
Trace::Thread_Updates<word_t>({{{1, 0}}, {{2, 0}}}),
Trace::thread_states<word_t>({{{1, 0}}, {{2, 0}}}),
trace->mem_updates);
ASSERT_EQ(
Trace::Thread_Updates<word_t>({{{1, 0}}, {{2, 0}}}),
Trace::thread_states<word_t>({{{1, 0}}, {{2, 0}}}),
trace->sb_adr_updates);
ASSERT_EQ(
Trace::Thread_Updates<word_t>({{{1, 0}}, {{2, 0}}}),
Trace::thread_states<word_t>({{{1, 0}}, {{2, 0}}}),
trace->sb_val_updates);
ASSERT_EQ(
Trace::Thread_Updates<bool>({{{1, false}}, {{2, false}}}),
Trace::thread_states<bool>({{{1, false}}, {{2, false}}}),
trace->sb_full_updates);
ASSERT_EQ(Trace::Flushes(), trace->flushes);
ASSERT_EQ(std::unordered_set<size_t>(), trace->flushes);
ASSERT_TRUE(trace->heap_updates.empty());
}
......@@ -297,7 +297,7 @@ TEST_F(Simulator, run_race_condition)
ASSERT_EQ(3, simulator->threads_per_checkpoint[1].size());
ASSERT_EQ(0, simulator->waiting_for_checkpoint[1]);
bound_t step = 0;
size_t step = 0;
std::function<Thread *()> scheduler = [&] () -> Thread *
{
......@@ -545,48 +545,48 @@ TEST_F(Simulator, run_race_condition)
ASSERT_EQ(1, trace->exit);
ASSERT_EQ(
Trace::Thread_Updates<word_t>({
Trace::thread_states<word_t>({
{{1, 0}, {12, 1}, {13, 2}, {14, 3}, {15, 4}},
{{2, 0}, {4, 1}, {6, 2}, {10, 3}},
{{3, 0}, {5, 1}, {7, 2}, {11, 3}}}),
trace->pc_updates);
ASSERT_EQ(
Trace::Thread_Updates<word_t>({
Trace::thread_states<word_t>({
{{1, 0}, {12, 1}, {13, 65535}},
{{2, 0}, {4, 1}},
{{3, 0}, {5, 1}}}),
trace->accu_updates);
ASSERT_EQ(
Trace::Thread_Updates<word_t>({{{1, 0}}, {{2, 0}}, {{3, 0}}}),
Trace::thread_states<word_t>({{{1, 0}}, {{2, 0}}, {{3, 0}}}),
trace->mem_updates);
ASSERT_EQ(
Trace::Thread_Updates<word_t>({
Trace::thread_states<word_t>({
{{1, 0}},
{{2, 0}, {6, 1}},
{{3, 0}, {7, 1}}}),
trace->sb_adr_updates);
ASSERT_EQ(
Trace::Thread_Updates<word_t>({
Trace::thread_states<word_t>({
{{1, 0}},
{{2, 0}, {6, 1}},
{{3, 0}, {7, 1}}}),
trace->sb_val_updates);
ASSERT_EQ(
Trace::Thread_Updates<bool>({
Trace::thread_states<bool>({
{{1, false}},
{{2, false}, {6, true}, {8, false}},
{{3, false}, {7, true}, {9, false}}}),
trace->sb_full_updates);
ASSERT_EQ(Trace::Flushes({8, 9}), trace->flushes);
ASSERT_EQ(std::unordered_set<size_t>({8, 9}), trace->flushes);
ASSERT_EQ(
Trace::Heap_Updates({{1, {{8, 1}}}}),
Trace::heap_states({{1, {{8, 1}}}}),
trace->heap_updates);
}
......@@ -596,7 +596,7 @@ TEST_F(Simulator, run_zero_bound)
create_simulator({program});
bound_t step = 0;
size_t step = 0;
std::function<Thread *()> scheduler = [&] () -> Thread *
{
......@@ -640,30 +640,30 @@ TEST_F(Simulator, run_zero_bound)
ASSERT_EQ(0, trace->exit);
ASSERT_EQ(
Trace::Thread_Updates<word_t>({{{1, 0}}}),
Trace::thread_states<word_t>({{{1, 0}}}),
trace->pc_updates);
ASSERT_EQ(
Trace::Thread_Updates<word_t>({{{1, 0}}}),
Trace::thread_states<word_t>({{{1, 0}}}),
trace->accu_updates);
ASSERT_EQ(
Trace::Thread_Updates<word_t>({{{1, 0}}}),
Trace::thread_states<word_t>({{{1, 0}}}),
trace->mem_updates);
ASSERT_EQ(
Trace::Thread_Updates<word_t>({{{1, 0}}}),
Trace::thread_states<word_t>({{{1, 0}}}),
trace->sb_adr_updates);
ASSERT_EQ(
Trace::Thread_Updates<word_t>({{{1, 0}}}),
Trace::thread_states<word_t>({{{1, 0}}}),
trace->sb_val_updates);
ASSERT_EQ(
Trace::Thread_Updates<bool>({{{1, false}}}),
Trace::thread_states<bool>({{{1, false}}}),
trace->sb_full_updates);
ASSERT_EQ(Trace::Flushes(), trace->flushes);
ASSERT_EQ(std::unordered_set<size_t>(), trace->flushes);
ASSERT_TRUE(trace->heap_updates.empty());
}
......
......@@ -48,7 +48,7 @@ TEST_F(Trace, parse_check)
ASSERT_EQ(check_program_paths[1], trace->programs->at(1).path);
ASSERT_EQ(
::Trace::Updates<word_t>({
::Trace::update_map<word_t>({
{1, 0},
{2, 1},
{3, 0},
......@@ -58,7 +58,7 @@ TEST_F(Trace, parse_check)
trace->thread_updates);
ASSERT_EQ(
::Trace::Updates<word_t>({
::Trace::update_map<word_t>({
{1, 0},
{4, 1},
{5, 2},
......@@ -69,7 +69,7 @@ TEST_F(Trace, parse_check)
{12, 1}}),
trace->pc_updates[0]);
ASSERT_EQ(
::Trace::Updates<word_t>({
::Trace::update_map<word_t>({
{2, 0},
{6, 1},
{13, 2},
......@@ -78,48 +78,48 @@ TEST_F(Trace, parse_check)
trace->pc_updates[1]);
ASSERT_EQ(
::Trace::Updates<word_t>({
::Trace::update_map<word_t>({
{1, 0},
{7, 1}}),
trace->accu_updates[0]);
ASSERT_EQ(
::Trace::Updates<word_t>({
::Trace::update_map<word_t>({
{2, 0},
{13, 1},
{14, 2}}),
trace->accu_updates[1]);
ASSERT_EQ(
::Trace::Updates<word_t>({
::Trace::update_map<word_t>({
{1, 0}}),
trace->mem_updates[0]);
ASSERT_EQ(
::Trace::Updates<word_t>({
::Trace::update_map<word_t>({
{2, 0}}),
trace->mem_updates[1]);
ASSERT_EQ(
::Trace::Thread_Updates<word_t>({
::Trace::thread_states<word_t>({
{{1, 0}},
{{2, 0}}}),
trace->sb_adr_updates);
ASSERT_EQ(
::Trace::Thread_Updates<word_t>({
::Trace::thread_states<word_t>({
{{1, 0}, {8, 1}},
{{2, 0}, {15, 2}}}),
trace->sb_val_updates);
ASSERT_EQ(
::Trace::Thread_Updates<bool>({
::Trace::thread_states<bool>({
{{1, true}, {3, false}, {8, true}, {9, false}},
{{2, false}, {15, true}, {16, false}}}),
trace->sb_full_updates);
ASSERT_EQ(::Trace::Flushes({3, 9, 16}), trace->flushes);
ASSERT_EQ(std::unordered_set<size_t>({3, 9, 16}), trace->flushes);
ASSERT_EQ(
::Trace::Heap_Updates({{0, {{3, 0}, {9, 1}, {16, 2}}}}),
::Trace::heap_states({{0, {{3, 0}, {9, 1}, {16, 2}}}}),
trace->heap_updates);
}
......@@ -134,7 +134,7 @@ TEST_F(Trace, parse_cas)
ASSERT_EQ(cas_program_path, trace->programs->at(1).path);
ASSERT_EQ(
::Trace::Updates<word_t>({
::Trace::update_map<word_t>({
{1, 0},
{2, 1},
{4, 0},
......@@ -146,7 +146,7 @@ TEST_F(Trace, parse_cas)
trace->thread_updates);
ASSERT_EQ(
::Trace::Updates<word_t>({
::Trace::update_map<word_t>({
{1, 0},
{6, 1},
{7, 2},
......@@ -156,7 +156,7 @@ TEST_F(Trace, parse_cas)
{13, 2}}),
trace->pc_updates[0]);
ASSERT_EQ(
::Trace::Updates<word_t>({
::Trace::update_map<word_t>({
{2, 0},
{5, 1},
{8, 2},
......@@ -167,12 +167,12 @@ TEST_F(Trace, parse_cas)
trace->pc_updates[1]);
ASSERT_EQ(
::Trace::Updates<word_t>({
::Trace::update_map<word_t>({
{1, 0},
{10, 1}}),
trace->accu_updates[0]);
ASSERT_EQ(
::Trace::Updates<word_t>({
::Trace::update_map<word_t>({
{2, 0},
{9, 1},
{14, 0},
......@@ -180,38 +180,38 @@ TEST_F(Trace, parse_cas)
trace->accu_updates[1]);
ASSERT_EQ(
::Trace::Updates<word_t>({
::Trace::update_map<word_t>({
{1, 0},
{13, 1}}),
trace->mem_updates[0]);
ASSERT_EQ(
::Trace::Updates<word_t>({
::Trace::update_map<word_t>({
{2, 0},
{16, 1}}),
trace->mem_updates[1]);
ASSERT_EQ(
::Trace::Thread_Updates<word_t>({
::Trace::thread_states<word_t>({
{{1, 0}},
{{2, 0}}}),
trace->sb_adr_updates);
ASSERT_EQ(
::Trace::Thread_Updates<word_t>({
::Trace::thread_states<word_t>({
{{1, 0}},
{{2, 0}}}),
trace->sb_val_updates);
ASSERT_EQ(
::Trace::Thread_Updates<bool>({
::Trace::thread_states<bool>({
{{1, true}, {4, false}},
{{2, true}, {3, false}}}),
trace->sb_full_updates);
ASSERT_EQ(::Trace::Flushes({3, 4}), trace->flushes);
ASSERT_EQ(std::unordered_set<size_t>({3, 4}), trace->flushes);
ASSERT_EQ(
::Trace::Heap_Updates({{0, {{3, 0}, {11, 1}}}}),
::Trace::heap_states({{0, {{3, 0}, {11, 1}}}}),
trace->heap_updates);
}