Commit 371755e0 authored by phlo's avatar phlo

updated Encoder class visibility

parent 66d15160
......@@ -7,56 +7,38 @@ namespace ConcuBinE {
//==============================================================================
//------------------------------------------------------------------------------
// static members
// public constants
//------------------------------------------------------------------------------
const std::string Encoder::accu_sym = "accu";
const std::string Encoder::mem_sym = "mem";
const std::string Encoder::sb_adr_sym = "sb-adr";
const std::string Encoder::sb_val_sym = "sb-val";
const std::string Encoder::sb_full_sym = "sb-full";
const std::string Encoder::stmt_sym = "stmt";
const std::string Encoder::block_sym = "block";
const std::string Encoder::halt_sym = "halt";
const std::string Encoder::accu_sym = "accu";
const std::string Encoder::mem_sym = "mem";
const std::string Encoder::sb_adr_sym = "sb-adr";
const std::string Encoder::sb_val_sym = "sb-val";
const std::string Encoder::sb_full_sym = "sb-full";
const std::string Encoder::stmt_sym = "stmt";
const std::string Encoder::block_sym = "block";
const std::string Encoder::halt_sym = "halt";
const std::string Encoder::heap_sym = "heap";
const std::string Encoder::exit_flag_sym = "exit";
const std::string Encoder::exit_code_sym = "exit-code";
const std::string Encoder::heap_sym = "heap";
const std::string Encoder::exit_flag_sym = "exit";
const std::string Encoder::exit_code_sym = "exit-code";
const std::string Encoder::thread_sym = "thread";
const std::string Encoder::exec_sym = "exec";
const std::string Encoder::flush_sym = "flush";
const std::string Encoder::check_sym = "check";
const std::string Encoder::accu_comment = "accu variables";
const std::string Encoder::mem_comment = "mem variables";
const std::string Encoder::sb_adr_comment = "store buffer address variables";
const std::string Encoder::sb_val_comment = "store buffer value variables";
const std::string Encoder::sb_full_comment = "store buffer full variables";
const std::string Encoder::stmt_comment = "statement activation variables";
const std::string Encoder::block_comment = "blocking variables";
const std::string Encoder::halt_comment = "halt variables";
const std::string Encoder::heap_comment = "heap variable";
const std::string Encoder::exit_flag_comment = "exit flag variable";
const std::string Encoder::exit_code_comment = "exit code variable";
const std::string Encoder::thread_comment = "thread activation variables";
const std::string Encoder::exec_comment = "statement execution variables";
const std::string Encoder::flush_comment = "store buffer flush variables";
const std::string Encoder::check_comment = "checkpoint variables";
const std::string Encoder::thread_sym = "thread";
const std::string Encoder::exec_sym = "exec";
const std::string Encoder::flush_sym = "flush";
const std::string Encoder::check_sym = "check";
//------------------------------------------------------------------------------
// constructors
// public constructors
//------------------------------------------------------------------------------
Encoder::Encoder (const std::shared_ptr<Program::List> & p,
const std::shared_ptr<MMap> & m,
size_t b) :
programs(p),
num_threads(p->size()),
mmap(m),
bound(b),
num_threads(p->size()),
use_sinz_constraint(num_threads > 4)
{
predecessors.reserve(num_threads);
......@@ -96,68 +78,25 @@ Encoder::Encoder (const std::shared_ptr<Program::List> & p,
}
//------------------------------------------------------------------------------
// public member functions
//------------------------------------------------------------------------------
// Encode::str -----------------------------------------------------------------
std::string Encoder::str ()
{
return formula.str();
}
//------------------------------------------------------------------------------
// DEBUG
// protected constants
//------------------------------------------------------------------------------
std::string Encoder::predecessors_to_string ()
{
std::ostringstream ss;
for (word_t tid = 0; tid < programs->size(); tid++)
for (const auto & [_pc, _predecessors] : predecessors[tid])
{
ss << "thread " << tid << " @ " << _pc << " :";
for (const auto & prev : _predecessors)
ss << " " << prev;
ss << eol;
}
return ss.str();
}
std::string Encoder::checkpoints_to_string ()
{
std::ostringstream ss;
for (const auto & [id, threads] : checkpoints)
{
ss << "check " << id << ": " << eol;
for (const auto & [_thread, pcs] : threads)
{
ss << " " << _thread << ":";
for (const auto & _pc : pcs)
ss << " " << _pc;
ss << eol;
}
}
return ss.str();
}
std::string Encoder::exits_to_string ()
{
std::ostringstream ss;
const std::string Encoder::accu_comment = "accu variables";
const std::string Encoder::mem_comment = "mem variables";
const std::string Encoder::sb_adr_comment = "store buffer address variables";
const std::string Encoder::sb_val_comment = "store buffer value variables";
const std::string Encoder::sb_full_comment = "store buffer full variables";
const std::string Encoder::stmt_comment = "statement activation variables";
const std::string Encoder::block_comment = "blocking variables";
const std::string Encoder::halt_comment = "halt variables";
for (const auto & [_thread, pcs] : exits)
{
ss << "thread " << _thread << ":";
for (const auto & _pc : pcs)
ss << ' ' << _pc;
ss << eol;
}
const std::string Encoder::heap_comment = "heap variable";
const std::string Encoder::exit_flag_comment = "exit flag variable";
const std::string Encoder::exit_code_comment = "exit code variable";
return ss.str();
}
const std::string Encoder::thread_comment = "thread activation variables";
const std::string Encoder::exec_comment = "statement execution variables";
const std::string Encoder::flush_comment = "store buffer flush variables";
const std::string Encoder::check_comment = "checkpoint variables";
} // namespace ConcuBinE
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
#ifndef ENCODER_SMTLIB_HH_
#define ENCODER_SMTLIB_HH_
#include "encoder.hh"
namespace ConcuBinE::smtlib {
//==============================================================================
// SMT-Lib v2.5 Encoder
//==============================================================================
class Encoder : public ConcuBinE::Encoder
{
public: //======================================================================
//----------------------------------------------------------------------------
// public constants
//----------------------------------------------------------------------------
// exit code variable
//
static const std::string & exit_code_var;
//----------------------------------------------------------------------------
// public constructors
//----------------------------------------------------------------------------
Encoder (const std::shared_ptr<Program::List> & programs,
const std::shared_ptr<MMap> & mmap,
size_t bound);
//----------------------------------------------------------------------------
// public member functions
//----------------------------------------------------------------------------
// thread state variable name generators
//
static std::string accu_var (word_t step, word_t thread);
static std::string mem_var (word_t step, word_t thread);
static std::string sb_adr_var (word_t step, word_t thread);
static std::string sb_val_var (word_t step, word_t thread);
static std::string sb_full_var (word_t step, word_t thread);
static std::string stmt_var (word_t step, word_t thread, word_t pc);
static std::string block_var (word_t step, word_t thread, word_t id);
static std::string halt_var (word_t step, word_t thread);
// machine state variable name generators
//
static std::string heap_var (word_t step);
static std::string exit_flag_var (word_t step);
// transition variable name generators
//
static std::string thread_var (word_t step, word_t thread);
static std::string exec_var (word_t step, word_t thread, word_t pc);
static std::string flush_var (word_t step, word_t thread);
static std::string check_var (word_t step, word_t id);
//----------------------------------------------------------------------------
// public member functions inherited from ConcuBinE::Encoder
//----------------------------------------------------------------------------
// main encoding function
//
virtual void encode ();
// add exit code assertion
//
virtual void assert_exit ();
protected: //===================================================================
//----------------------------------------------------------------------------
// protected constants
//----------------------------------------------------------------------------
// bitvector sort declaration
//
static const std::string bv_sort;
// variable comments
//
static const std::string accu_comment;
static const std::string mem_comment;
static const std::string sb_adr_comment;
static const std::string sb_val_comment;
static const std::string sb_full_comment;
static const std::string stmt_comment;
static const std::string block_comment;
static const std::string halt_comment;
static const std::string exit_flag_comment;
static const std::string exit_code_comment;
static const std::string heap_comment;
static const std::string thread_comment;
static const std::string exec_comment;
static const std::string flush_comment;
static const std::string check_comment;
//----------------------------------------------------------------------------
// protected member functions
//----------------------------------------------------------------------------
// thread state variable name generators
//
std::string accu_var () const;
std::string mem_var () const;
std::string sb_adr_var () const;
std::string sb_val_var () const;
std::string sb_full_var () const;
std::string stmt_var () const;
std::string halt_var () const;
// machine state variable name generators
//
std::string heap_var () const;
std::string exit_flag_var () const;
// transition variable name generators
//
std::string thread_var () const;
std::string exec_var () const;
std::string flush_var () const;
// assignment expression generator
//
std::string assign (const std::string & variable,
const std::string & expression) const;
//----------------------------------------------------------------------------
// protected member functions inherited from ConcuBinE::Encoder
//----------------------------------------------------------------------------
// state variable definitions
//
virtual void define_states () = 0;
// double-dispatched instruction encoding functions
//
virtual std::string encode (const Instruction::Load &);
virtual std::string encode (const Instruction::Store &);
virtual std::string encode (const Instruction::Fence &);
virtual std::string encode (const Instruction::Add &);
virtual std::string encode (const Instruction::Addi &);
virtual std::string encode (const Instruction::Sub &);
virtual std::string encode (const Instruction::Subi &);
virtual std::string encode (const Instruction::Mul &);
virtual std::string encode (const Instruction::Muli &);
virtual std::string encode (const Instruction::Cmp &);
virtual std::string encode (const Instruction::Jmp &);
virtual std::string encode (const Instruction::Jz &);
virtual std::string encode (const Instruction::Jnz &);
virtual std::string encode (const Instruction::Js &);
virtual std::string encode (const Instruction::Jns &);
virtual std::string encode (const Instruction::Jnzns &);
virtual std::string encode (const Instruction::Mem &);
virtual std::string encode (const Instruction::Cas &);
virtual std::string encode (const Instruction::Check &);
virtual std::string encode (const Instruction::Halt &);
virtual std::string encode (const Instruction::Exit &);
//----------------------------------------------------------------------------
// protected data members
//----------------------------------------------------------------------------
// current step
//
size_t step;
// previous step (reduce subtractions)
//
size_t prev;
private: //=====================================================================
//----------------------------------------------------------------------------
// private member functions
//----------------------------------------------------------------------------
// load expression generator
//
std::string load (word_t address, bool indirect = false);
// state variable declarations
//
void declare_accu ();
void declare_mem ();
void declare_sb_adr ();
void declare_sb_val ();
void declare_sb_full ();
void declare_stmt ();
void declare_block ();
void declare_halt ();
void declare_heap ();
void declare_exit_flag ();
void declare_exit_code ();
void declare_states (); // all of the above
// transition variable declarations
//
void declare_thread ();
void declare_exec ();
void declare_flush ();
void declare_check ();
void declare_transitions (); // all of the above
// state variable initializers
//
void init_accu ();
void init_mem ();
void init_sb_adr ();
void init_sb_val ();
void init_sb_full ();
void init_stmt ();
void init_block ();
void init_halt ();
void init_heap ();
void init_exit_flag ();
void init_states (); // all of the above
// transition variable definitions
//
void define_exec ();
void define_check ();
void define_transitions (); // all of the above
// constraint definitions
//
void define_scheduling_constraints ();
void define_store_buffer_constraints ();
void define_checkpoint_constraints ();
void define_halt_constraints ();
void define_constraints (); // all of the above
};
} // namespace ConcuBinE::smtlib
#endif
#include "encoder.hh"
#include "encoder_smtlib_functional.hh"
#include <cassert>
......@@ -11,10 +11,20 @@ namespace ConcuBinE::smtlib {
//==============================================================================
//------------------------------------------------------------------------------
// functions
// public member functions inherited from ConcuBinE::smtlib::Encoder
//------------------------------------------------------------------------------
// smtlib::Functional::define_accu ---------------------------------------------
// smtlib::Functional::encode --------------------------------------------------
void Functional::encode ()
{
Encoder::encode();
define_exit_code();
}
//------------------------------------------------------------------------------
// private member functions
//------------------------------------------------------------------------------
#define DEFINE_STATE(_update, _type, _var) \
do { \
......@@ -33,12 +43,14 @@ namespace ConcuBinE::smtlib {
formula << eol; \
} while (0)
// smtlib::Functional::define_accu ---------------------------------------------
void Functional::define_accu ()
{
if (verbose)
formula << accu_comment;
DEFINE_STATE(State::accu, Instruction::Type::accu, accu_var);
DEFINE_STATE(Update::accu, Instruction::Type::accu, accu_var);
}
// smtlib::Functional::define_mem ----------------------------------------------
......@@ -48,7 +60,7 @@ void Functional::define_mem ()
if (verbose)
formula << mem_comment;
DEFINE_STATE(State::mem, Instruction::Type::mem, mem_var);
DEFINE_STATE(Update::mem, Instruction::Type::mem, mem_var);
}
// smtlib::Functional::define_sb_adr -------------------------------------------
......@@ -58,7 +70,7 @@ void Functional::define_sb_adr ()
if (verbose)
formula << sb_adr_comment;
DEFINE_STATE(State::sb_adr, Instruction::Type::write, sb_adr_var);
DEFINE_STATE(Update::sb_adr, Instruction::Type::write, sb_adr_var);
}
// smtlib::Functional::define_sb_val -------------------------------------------
......@@ -68,7 +80,7 @@ void Functional::define_sb_val ()
if (verbose)
formula << sb_val_comment;
DEFINE_STATE(State::sb_val, Instruction::Type::write, sb_val_var);
DEFINE_STATE(Update::sb_val, Instruction::Type::write, sb_val_var);
}
// smtlib::Functional::define_sb_full ------------------------------------------
......@@ -170,7 +182,6 @@ void Functional::define_block ()
for (const auto & [t, pcs] : threads)
{
std::vector<std::string> args;
args.reserve(pcs.size() + 1);
for (const word_t p : pcs)
......@@ -205,7 +216,6 @@ void Functional::define_halt ()
for (const auto & [t, pcs] : halts)
{
std::vector<std::string> args;
args.reserve(pcs.size() + 1);
for (const word_t p : pcs)
......@@ -226,7 +236,7 @@ void Functional::define_heap ()
if (verbose)
formula << heap_comment;
update = State::heap;
update = Update::heap;
const std::string heap_prev = heap_var(prev);
std::string expr = heap_prev;
......@@ -270,7 +280,6 @@ void Functional::define_exit_flag ()
if (!halts.empty())
{
std::vector<std::string> halt;
halt.reserve(halts.size());
for (const auto & it : halts)
......@@ -310,6 +319,10 @@ void Functional::define_exit_code ()
formula << assign(exit_code_var, expr) << eol << eol;
}
//------------------------------------------------------------------------------
// private member functions inherited from ConcuBinE::smtlib::Encoder
//------------------------------------------------------------------------------
// smtlib::Functional::define_states -------------------------------------------
void Functional::define_states ()
......@@ -332,13 +345,4 @@ void Functional::define_states ()
define_exit_flag();
}
// smtlib::Functional::encode --------------------------------------------------
void Functional::encode ()
{
Encoder::encode();
define_exit_code();
}
} // namespace ConcuBinE::smtlib
#ifndef ENCODER_SMTLIB_FUNCTIONAL_HH_
#define ENCODER_SMTLIB_FUNCTIONAL_HH_
#include "encoder_smtlib.hh"
namespace ConcuBinE::smtlib {
//==============================================================================
// SMT-Lib v2.5 Functional Encoder
//==============================================================================
class Functional : public Encoder
{
public: //======================================================================
//----------------------------------------------------------------------------
// public constructors
//----------------------------------------------------------------------------
// expose constructors from ConcuBinE::smtlib::Encoder
//
using Encoder::Encoder;
//----------------------------------------------------------------------------
// public member functions inherited from ConcuBinE::smtlib::Encoder
//----------------------------------------------------------------------------
// main encoding function
//
virtual void encode ();
private: //=====================================================================
//----------------------------------------------------------------------------
// private member functions
//----------------------------------------------------------------------------
// state variable definitions
//
void define_accu ();
void define_mem ();
void define_sb_adr ();
void define_sb_val ();
void define_sb_full ();
void define_stmt ();
void define_block ();
void define_halt ();
void define_heap ();
void define_exit_flag ();
void define_exit_code ();
//----------------------------------------------------------------------------
// private member functions inherited from ConcuBinE::smtlib::Encoder
//----------------------------------------------------------------------------
// state variable definitions
//
virtual void define_states ();
// double-dispatched instruction encoding functions
//
using Encoder::encode;
};
} // namespace ConcuBinE::smtlib
#endif
#include "encoder.hh"
#include "encoder_smtlib_relational.hh"
#include <cassert>
......@@ -6,74 +6,12 @@
namespace ConcuBinE::smtlib {
//==============================================================================
// smtlib::Relational::State
//==============================================================================
//------------------------------------------------------------------------------
// constructors
//------------------------------------------------------------------------------
Relational::State::State (Relational & e) :
accu(e.restore_accu()),
mem(e.restore_mem()),
sb_adr(e.restore_sb_adr()),
sb_val(e.restore_sb_val()),
sb_full(e.restore_sb_full()),
block(e.restore_block()),
halt(e.restore_halt()),
heap(e.restore_heap()),
exit_flag(e.unset_exit_flag())
{
assert(!stmt);
assert(!exit_code);
}
//------------------------------------------------------------------------------
// member operators
//------------------------------------------------------------------------------
// conversion ------------------------------------------------------------------
Relational::State::operator std::string () const
{
std::vector<std::string> args;
args.reserve(10);
args.push_back(*accu);
args.push_back(*mem);
args.push_back(*sb_adr);
args.push_back(*sb_val);
args.push_back(*sb_full);
if (stmt)
args.push_back(*stmt);
if (block)
args.push_back(*block);
if (halt)
args.push_back(*halt);
if (heap)
args.push_back(*heap);
if (exit_flag)
args.push_back(*exit_flag);
if (exit_code)
args.push_back(*exit_code);
return land(args);
}
//==============================================================================
// smtlib::Relational
//==============================================================================
//------------------------------------------------------------------------------
// member functions
// private member functions
//------------------------------------------------------------------------------
// smtlib::Relational::imply ---------------------------------------------------
......@@ -89,7 +27,7 @@ std::string Relational::imply (const std::string & ante,
template <class T>
std::shared_ptr<std::string> Relational::set_accu (const T & op)
{