Commit 2bbd1e4b authored by phlo's avatar phlo

updated Program class

parent fcf01eef
......@@ -59,7 +59,12 @@ Encoder::Encoder (const std::shared_ptr<Program::List> & p,
bound(b),
use_sinz_constraint(num_threads > 4)
{
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];
......@@ -68,6 +73,10 @@ Encoder::Encoder (const std::shared_ptr<Program::List> & p,
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);
......@@ -76,10 +85,6 @@ Encoder::Encoder (const std::shared_ptr<Program::List> & p,
if (&op.symbol() == &Instruction::Exit::symbol)
exits[thread].push_back(pc);
}
// collect checkpoints
for (const auto & [c, pcs] : program.checkpoints)
checkpoints[c][thread] = &pcs;
});
// remove single-threaded checkpoints
......@@ -110,7 +115,7 @@ std::string Encoder::predecessors_to_string ()
std::ostringstream ss;
for (word_t tid = 0; tid < programs->size(); tid++)
for (const auto & [_pc, _predecessors] : (*programs)[tid].predecessors)
for (const auto & [_pc, _predecessors] : predecessors[tid])
{
ss << "thread " << tid << " @ " << _pc << " :";
for (const auto & prev : _predecessors)
......@@ -131,7 +136,7 @@ std::string Encoder::checkpoints_to_string ()
for (const auto & [_thread, pcs] : threads)
{
ss << " " << _thread << ":";
for (const auto & _pc : *pcs)
for (const auto & _pc : pcs)
ss << " " << _pc;
ss << eol;
}
......
......@@ -131,6 +131,12 @@ struct Encoder
//
State update;
// list of predecessors for each thread
//
// thread -> pc -> set of predecessors
//
std::vector<std::unordered_map<word_t, std::set<word_t>>> predecessors;
// pcs of statements requiring an empty store buffer
//
// thread -> list of program counters
......@@ -139,9 +145,9 @@ struct Encoder
// pcs of checkpoint statements
//
// checkpoint id -> thread -> pointer to list of program counters
// checkpoint id -> thread -> list of program counters
//
std::map<word_t, std::map<word_t, const std::vector<word_t> *>> checkpoints;
std::map<word_t, std::map<word_t, std::vector<word_t>>> checkpoints;
// pcs of halt statements
//
......
......@@ -1081,7 +1081,7 @@ void Encoder::define_stmt ()
verbose ? debug_symbol(thread, pc) : "");
// add activation by predecessor's execution
for (word_t prev : program.predecessors.at(pc))
for (word_t prev : predecessors[thread][pc])
{
nid_exec = nids_exec[thread][prev];
......@@ -1146,9 +1146,9 @@ void Encoder::define_block ()
std::string & nid_block = nid_block_it++->second;
std::vector<std::string> args;
args.reserve(pcs->size() + 1);
args.reserve(pcs.size() + 1);
for (const auto & p : *pcs)
for (const auto & p : pcs)
args.push_back(nids_exec[t][p]);
args.push_back(nid_block);
......
......@@ -117,19 +117,19 @@ void Functional::define_stmt ()
stmt_var(prev, thread, pc),
lnot(exec_var(prev, thread, pc))});
const auto & preds = program.predecessors.at(pc);
const auto & pred = predecessors[thread][pc];
for (auto rit = preds.rbegin(); rit != preds.rend(); ++rit)
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 & pred = program[*rit];
const Instruction & pre = program[*rit];
if (pred.is_jump())
if (pre.is_jump())
{
std::string cond = pred.encode(*this);
const std::string cond = pre.encode(*this);
// JMP has no condition and returns an empty std::string
if (!cond.empty())
......@@ -137,7 +137,7 @@ void Functional::define_stmt ()
land({
val,
// only activate successor if jump condition failed
*rit == pc - 1 && pred.arg() != pc
*rit == pc - 1 && pre.arg() != pc
? lnot(cond)
: cond});
}
......@@ -171,9 +171,9 @@ void Functional::define_block ()
{
std::vector<std::string> args;
args.reserve(pcs->size() + 1);
args.reserve(pcs.size() + 1);
for (const word_t p : *pcs)
for (const word_t p : pcs)
args.push_back(exec_var(prev, t, p));
args.push_back(block_var(prev, c, t));
......
......@@ -74,7 +74,7 @@ public: //======================================================================
// public member types
//----------------------------------------------------------------------------
// operational types ---------------------------------------------------------
// operational types
//
enum Type : uint8_t
{
......@@ -89,7 +89,7 @@ public: //======================================================================
control = 1 << 6 // control flow
};
// instruction PODs ----------------------------------------------------------
// instruction PODs
//
struct Nullary { uint8_t type = Type::none; };
struct Unary : public Nullary { word_t arg = 0; };
......@@ -123,7 +123,7 @@ public: //======================================================================
DECLARE_NULLARY (Halt, Nullary, "HALT", barrier | control)
DECLARE_UNARY (Exit, Unary, "EXIT", control)
// abstract interface (types erasure concept) --------------------------------
// abstract interface (types erasure concept)
//
struct Concept
{
......
This diff is collapsed.
......@@ -2,10 +2,8 @@
#define PROGRAM_HH_
#include <istream>
#include <memory>
#include <set>
#include <unordered_map>
#include <unordered_set>
#include <vector>
#include "common.hh"
......@@ -16,27 +14,27 @@ namespace ConcuBinE {
// forward declarations
//==============================================================================
struct Instruction;
class Instruction;
//==============================================================================
// Program class
//==============================================================================
struct Program : public std::vector<Instruction>
class Program : public std::vector<Instruction>
{
public: //======================================================================
//----------------------------------------------------------------------------
// member types
// public member types
//----------------------------------------------------------------------------
// program list --------------------------------------------------------------
//
struct List : public std::vector<Program>
{
//------------------------------------------------------------------------
// constructors
// public constructors
//------------------------------------------------------------------------
// inherit constructors from std::vector
// expose constructors from std::vector
//
using std::vector<Program>::vector;
......@@ -71,83 +69,72 @@ struct Program : public std::vector<Instruction>
};
//----------------------------------------------------------------------------
// members
// public constructors
//----------------------------------------------------------------------------
// path to program file
// expose constructors from std::vector
//
std::string path;
using std::vector<Instruction>::vector;
// pc of predecessors for each statement
// parse input stream
//
std::unordered_map<word_t, std::set<word_t>> predecessors;
Program (std::istream & stream, const std::string & path);
// maps checkpoint ids to the corresponding program counters
//----------------------------------------------------------------------------
// public member functions
//----------------------------------------------------------------------------
// get map of program counters to set of predecessors
//
// checkpoint id -> thread -> pc
// pc -> set of predecessors
//
std::unordered_map<word_t, std::vector<word_t>> checkpoints;
// * checks for unreachable instructions
//
std::unordered_map<word_t, std::set<word_t>> predecessors () const;
// maps program counters to the label referencing it
// get program counter corresponding to a given label
//
// pc -> label
word_t pc (const std::string & label) const;
// get label corresponding to a given program counter
//
std::unordered_map<word_t, std::string> pc_to_label;
std::string label (word_t pc) const;
// maps labels to the corresponding program counter
// print whole program
//
// label -> pc
std::string print () const;
// print instruction at a given program counter
//
std::unordered_map<std::string, word_t> label_to_pc;
std::string print (word_t pc) const;
//----------------------------------------------------------------------------
// constructors
// public data members
//----------------------------------------------------------------------------
// inherit base constructors
// path to program file
//
using std::vector<Instruction>::vector;
std::string path;
// construct from file
//
Program (std::istream & file, const std::string & path);
private: //=====================================================================
//----------------------------------------------------------------------------
// member functions
// private data members
//----------------------------------------------------------------------------
// appends instruction to the program
//
void push_back (Instruction && op);
// get pc corresponding to the given label
// maps program counters to the label referencing it
//
word_t get_pc (std::string label) const;
// get label corresponding to the given pc
// pc -> label
//
std::string get_label (word_t pc) const;
std::unordered_map<word_t, std::string> pc_to_label;
// print whole program
// maps labels to the corresponding program counter
//
std::string print (bool include_pc = false) const;
// print instruction at pc
// label -> pc
//
std::string print (bool include_pc, word_t pc) const;
std::unordered_map<std::string, word_t> label_to_pc;
};
//==============================================================================
// non-member operators
//==============================================================================
// equality
//
// TODO: really needed - rely on base class?
//
bool operator == (const Program &, const Program &);
bool operator != (const Program &, const Program &);
} // namespace ConcuBinE
#endif
......@@ -63,8 +63,9 @@ void Simulator::init (const std::shared_ptr<Program::List> & p,
sb_full(false);
// collect checkpoints
for (const auto & [c, pcs] : (*programs)[thread].checkpoints)
threads_per_checkpoint[c].insert(thread);
for (const auto & op : (*programs)[thread])
if (!op.type())
threads_per_checkpoint[op.arg()].insert(thread);
}
// reset waiting map
......
......@@ -30,7 +30,7 @@ TEST(Encoder, constructor)
for (const auto & pcs : threads)
ASSERT_EQ(
id == 1 ? std::vector<word_t>({3}) : std::vector<word_t>({5}),
*std::get<1>(pcs));
std::get<1>(pcs));
ASSERT_TRUE(encoder.halts.empty());
......@@ -71,7 +71,7 @@ TEST(Encoder, constructor_checkpoints)
for (const auto & pcs : threads)
{
word_t thread = id - 1;
ASSERT_EQ(std::vector<word_t>({thread}), *pcs.second);
ASSERT_EQ(std::vector<word_t>({thread}), pcs.second);
}
}
......
......@@ -38,7 +38,7 @@ const std::string instruction_set =
// utility functions
// =============================================================================
// create program from source
// create dummy program from source
//
inline Program prog (const std::string & code,
const std::string & path = "dummy.asm")
......@@ -48,6 +48,7 @@ inline Program prog (const std::string & code,
}
// create program list pointer from arbitrary number of programs
//
template <class ... P>
inline std::shared_ptr<Program::List> lst (P && ... programs)
{
......
......@@ -320,13 +320,7 @@ TEST(btor2_Encoder, declare_sorts)
TEST(btor2_Encoder, declare_constants)
{
auto programs = lst(3);
for (size_t tid = 0; tid < 3; tid++)
for (size_t pc = 0; pc < 3; pc++)
(*programs)[tid].push_back(Instruction::create("ADDI", tid + pc + 1));
auto encoder = create<E>(programs);
auto encoder = create<E>(lst(prog("ADD 0"), prog("ADD 1"), prog("ADD 2")));
encoder.declare_sorts();
encoder.formula.str("");
......@@ -345,9 +339,6 @@ TEST(btor2_Encoder, declare_constants)
<< encoder.nids_const[0] << " zero 2\n"
<< encoder.nids_const[1] << " one 2\n"
<< encoder.nids_const[2] << " constd 2 2\n"
<< encoder.nids_const[3] << " constd 2 3\n"
<< encoder.nids_const[4] << " constd 2 4\n"
<< encoder.nids_const[5] << " constd 2 5\n"
<< eol;
return s.str();
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -1427,11 +1427,11 @@ TEST_F(Trace, operator_equals)
ASSERT_TRUE(s1 == s2);
// list of programs differ
p2->push_back(Program());
p2->push_back({});
ASSERT_TRUE(s1 != s2);
p1->push_back(Program());
p1->push_back({});
ASSERT_TRUE(s1 == s2);
......
......@@ -117,7 +117,7 @@ Trace::Trace(std::istream & file, const std::string & path) :
if (!(line >> token))
parser_error(path, line_num, "missing program counter");
try { pc = program.get_pc(token); }
try { pc = program.pc(token); }
catch (...)
{
parser_error(path, line_num, "unknown label [" + token + "]");
......@@ -193,7 +193,7 @@ Trace::Trace(std::istream & file, const std::string & path) :
// arg is a label
else if (op.is_jump())
{
try { arg = program.get_pc(token); }
try { arg = program.pc(token); }
catch (...)
{
parser_error(path, line_num, "unknown label [" + token + "]");
......@@ -697,14 +697,8 @@ std::string Trace::print (const Step & step) const
const Instruction & op = program[step.pc];
// program counter
try
{
ss << program.get_label(step.pc) << sep;
}
catch (...)
{
ss << step.pc << sep;
}
try { ss << program.label(step.pc) << sep; }
catch (...) { ss << step.pc << sep; }
// instruction symbol / argument
if (step.flush)
......@@ -727,7 +721,7 @@ std::string Trace::print (const Step & step) const
arg = '[' + arg + ']';
}
else if (op.is_jump())
try { arg = program.get_label(op.arg()); } catch (...) {}
try { arg = program.label(op.arg()); } catch (...) {}
}
ss << arg << sep;
......
......@@ -2,7 +2,9 @@
#define TRACE_HH_
#include <map>
#include <memory>
#include <unordered_map>
#include <unordered_set>
#include <vector>
#include "program.hh"
......
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