Commit 4e7fd88b authored by phlo's avatar phlo

introduced namespace ConcuBinE

parent b5a95a50
......@@ -4,6 +4,8 @@
#include "parser.hh"
namespace ConcuBinE {
std::string Boolector::name () const { return "boolector"; }
std::string Boolector::build_command ()
......@@ -119,3 +121,5 @@ Boolector::parse_line (std::istringstream & line)
return {};
}
} // namespace ConcuBinE
......@@ -3,6 +3,8 @@
#include "solver.hh"
namespace ConcuBinE {
class Boolector : public External
{
virtual std::string build_command ();
......@@ -16,4 +18,6 @@ public:
virtual std::string name () const;
};
} // namespace ConcuBinE
#endif
......@@ -8,7 +8,7 @@
#include <string>
#include <vector>
namespace btor2 {
namespace ConcuBinE::btor2 {
//==============================================================================
// BTOR2 std::string generators for commonly used expressions
......@@ -827,6 +827,6 @@ inline std::string card_constraint_sinz (nid_t & nid,
return os.str();
}
} // namespace btor2
} // namespace ConcuBinE::btor2
#endif
......@@ -2,6 +2,8 @@
#include "encoder.hh"
namespace ConcuBinE {
BtorMC::BtorMC(size_t b) : bound(b) {}
std::string BtorMC::name () const { return "btormc"; }
......@@ -115,3 +117,5 @@ std::optional<BtorMC::Variable> BtorMC::parse_variable (std::istringstream & lin
return variable;
}
} // namespace ConcuBinE
......@@ -3,6 +3,8 @@
#include "boolector.hh"
namespace ConcuBinE {
struct BtorMC : public Boolector
{
BtorMC (size_t);
......@@ -20,4 +22,6 @@ struct BtorMC : public Boolector
virtual std::string name () const;
};
} // namespace ConcuBinE
#endif
......@@ -3,6 +3,9 @@
#include <cstdint>
#include <limits>
#include <random>
namespace ConcuBinE {
//==============================================================================
// types
......@@ -14,23 +17,29 @@ using word_t = uint16_t;
using sword_t = int16_t; // signed
//==============================================================================
// global variables
// constants
//==============================================================================
// word attributes
// register type attributes
//
const word_t word_size = std::numeric_limits<word_t>::digits;
const word_t word_max = std::numeric_limits<word_t>::max();
constexpr word_t word_size = std::numeric_limits<word_t>::digits;
constexpr word_t word_max = std::numeric_limits<word_t>::max();
constexpr sword_t sword_min = std::numeric_limits<sword_t>::min();
constexpr sword_t sword_max = std::numeric_limits<sword_t>::max();
const sword_t sword_min = std::numeric_limits<sword_t>::min();
const sword_t sword_max = std::numeric_limits<sword_t>::max();
// end of line character
//
constexpr char eol = '\n';
//==============================================================================
// global variables
//==============================================================================
// verbose output
//
extern bool verbose;
// end of line character
//
const char eol = '\n';
} // namespace ConcuBinE
#endif
......@@ -2,6 +2,8 @@
#include "smtlib.hh"
namespace ConcuBinE {
std::string CVC4::name () const { return "cvc4"; }
std::string CVC4::build_command ()
......@@ -25,3 +27,5 @@ std::optional<CVC4::Variable> CVC4::parse_line (std::istringstream & line)
return {};
}
} // namespace ConcuBinE
......@@ -3,6 +3,8 @@
#include "solver.hh"
namespace ConcuBinE {
class CVC4 : public External
{
private:
......@@ -19,4 +21,6 @@ public:
virtual std::string name () const;
};
} // namespace ConcuBinE
#endif
#include "encoder.hh"
namespace ConcuBinE {
//==============================================================================
// Encoder
//==============================================================================
......@@ -148,3 +150,5 @@ std::string Encoder::exit_pcs_to_string ()
return ss.str();
}
} // namespace ConcuBinE
......@@ -8,6 +8,8 @@
#include "instruction.hh"
#include "program.hh"
namespace ConcuBinE {
//==============================================================================
// Encoder base class
//
......@@ -243,7 +245,7 @@ namespace smtlib {
// SMT-Lib v2.5 Encoder base class
//==============================================================================
struct Encoder : public ::Encoder
struct Encoder : public ConcuBinE::Encoder
{
//----------------------------------------------------------------------------
// static members
......@@ -630,7 +632,7 @@ namespace btor2 {
// BTOR2 Encoder class
//==============================================================================
struct Encoder : public ::Encoder
struct Encoder : public ConcuBinE::Encoder
{
//----------------------------------------------------------------------------
// member types
......@@ -962,5 +964,6 @@ struct Encoder : public ::Encoder
};
} // namespace btor2
} // namespace ConcuBinE
#endif
......@@ -5,7 +5,7 @@
#include "btor2.hh"
namespace btor2 {
namespace ConcuBinE::btor2 {
//==============================================================================
// helpers
......@@ -51,49 +51,109 @@ const std::string & Encoder::exit_code_var = exit_code_sym;
// variable comments -----------------------------------------------------------
const std::string Encoder::accu_comment =
comment(::Encoder::accu_comment + " - " + accu_sym + "_<thread>" + eol);
comment(
ConcuBinE::Encoder::accu_comment
+ " - "
+ accu_sym
+ "_<thread>"
+ eol);
const std::string Encoder::mem_comment =
comment(::Encoder::mem_comment + " - " + mem_sym + "_<thread>" + eol);
comment(
ConcuBinE::Encoder::mem_comment
+ " - "
+ mem_sym
+ "_<thread>"
+ eol);
const std::string Encoder::sb_adr_comment =
comment(::Encoder::sb_adr_comment + " - " + sb_adr_sym + "_<thread>" + eol);
comment(
ConcuBinE::Encoder::sb_adr_comment
+ " - "
+ sb_adr_sym
+ "_<thread>"
+ eol);
const std::string Encoder::sb_val_comment =
comment(::Encoder::sb_val_comment + " - " + sb_val_sym + "_<thread>" + eol);
comment(
ConcuBinE::Encoder::sb_val_comment
+ " - "
+ sb_val_sym
+ "_<thread>"
+ eol);
const std::string Encoder::sb_full_comment =
comment(::Encoder::sb_full_comment + " - " + sb_full_sym + "_<thread>" + eol);
comment(
ConcuBinE::Encoder::sb_full_comment
+ " - "
+ sb_full_sym
+ "_<thread>"
+ eol);
const std::string Encoder::stmt_comment =
comment(::Encoder::stmt_comment + " - " + stmt_sym + "_<thread>_<pc>" + eol);
comment(
ConcuBinE::Encoder::stmt_comment
+ " - "
+ stmt_sym
+ "_<thread>_<pc>"
+ eol);
const std::string Encoder::block_comment =
comment(::Encoder::block_comment + " - " + block_sym + "_<id>_<thread>" + eol);
comment(
ConcuBinE::Encoder::block_comment
+ " - "
+ block_sym
+ "_<id>_<thread>"
+ eol);
const std::string Encoder::halt_comment =
comment(::Encoder::halt_comment + " - " + halt_sym + "_<thread>" + eol);
comment(
ConcuBinE::Encoder::halt_comment
+ " - "
+ halt_sym
+ "_<thread>"
+ eol);
const std::string Encoder::heap_comment =
comment(::Encoder::heap_comment + eol);
comment(ConcuBinE::Encoder::heap_comment + eol);
const std::string Encoder::exit_flag_comment =
comment(::Encoder::exit_flag_comment + eol);
comment(ConcuBinE::Encoder::exit_flag_comment + eol);
const std::string Encoder::exit_code_comment =
comment(::Encoder::exit_code_comment + eol);
comment(ConcuBinE::Encoder::exit_code_comment + eol);
const std::string Encoder::thread_comment =
comment(::Encoder::thread_comment + " - " + thread_sym + "_<thread>" + eol);
comment(
ConcuBinE::Encoder::thread_comment
+ " - "
+ thread_sym
+ "_<thread>"
+ eol);
const std::string Encoder::exec_comment =
comment(::Encoder::exec_comment + " - " + exec_sym + "_<thread>_<pc>" + eol);
comment(
ConcuBinE::Encoder::exec_comment
+ " - "
+ exec_sym
+ "_<thread>_<pc>"
+ eol);
const std::string Encoder::flush_comment =
comment(::Encoder::flush_comment + " - " + flush_sym + "_<thread>" + eol);
comment(
ConcuBinE::Encoder::flush_comment
+ " - "
+ flush_sym
+ "_<thread>"
+ eol);
const std::string Encoder::check_comment =
comment(::Encoder::check_comment + " - " + check_sym + "_<id>" + eol);
comment(
ConcuBinE::Encoder::check_comment
+ " - "
+ check_sym
+ "_<id>"
+ eol);
// most significant bit's bitvector constant -----------------------------------
......@@ -104,7 +164,7 @@ const std::string Encoder::msb = std::to_string(word_size - 1);
//------------------------------------------------------------------------------
Encoder::Encoder (const Program::List::ptr & p, const size_t b, const bool e) :
::Encoder(p, b),
ConcuBinE::Encoder(p, b),
node(1)
{
// collect constants
......@@ -1729,4 +1789,4 @@ std::string Encoder::encode (const Instruction::Exit & e [[maybe_unused]])
return nids_const[e.arg];
}
} // namespace btor2
} // namespace ConcuBinE::btor2
......@@ -4,7 +4,7 @@
#include "smtlib.hh"
namespace smtlib {
namespace ConcuBinE::smtlib {
//==============================================================================
// smtlib::Encoder
......@@ -26,68 +26,125 @@ const std::string & Encoder::exit_code_var = exit_code_sym;
const std::string Encoder::accu_comment =
comment(
::Encoder::accu_comment + " - " + accu_sym + "_<step>_<thread>" + eol);
ConcuBinE::Encoder::accu_comment
+ " - "
+ accu_sym
+ "_<step>_<thread>"
+ eol);
const std::string Encoder::mem_comment =
comment(::Encoder::mem_comment + " - " + mem_sym + "_<step>_<thread>" + eol);
comment(
ConcuBinE::Encoder::mem_comment
+ " - "
+ mem_sym
+ "_<step>_<thread>"
+ eol);
const std::string Encoder::sb_adr_comment =
comment(
::Encoder::sb_adr_comment + " - " + sb_adr_sym + "_<step>_<thread>" + eol);
ConcuBinE::Encoder::sb_adr_comment
+ " - "
+ sb_adr_sym
+ "_<step>_<thread>"
+ eol);
const std::string Encoder::sb_val_comment =
comment(
::Encoder::sb_val_comment + " - " + sb_val_sym + "_<step>_<thread>" + eol);
ConcuBinE::Encoder::sb_val_comment
+ " - "
+ sb_val_sym
+ "_<step>_<thread>"
+ eol);
const std::string Encoder::sb_full_comment =
comment(
::Encoder::sb_full_comment + " - " + sb_full_sym + "_<step>_<thread>" + eol);
ConcuBinE::Encoder::sb_full_comment
+ " - "
+ sb_full_sym
+ "_<step>_<thread>"
+ eol);
const std::string Encoder::stmt_comment =
comment(
::Encoder::stmt_comment + " - " + stmt_sym + "_<step>_<thread>_<pc>" + eol);
ConcuBinE::Encoder::stmt_comment
+ " - "
+ stmt_sym
+ "_<step>_<thread>_<pc>"
+ eol);
const std::string Encoder::block_comment =
comment(
::Encoder::block_comment + " - " + block_sym + "_<step>_<id>_<thread>" + eol);
ConcuBinE::Encoder::block_comment
+ " - "
+ block_sym
+ "_<step>_<id>_<thread>"
+ eol);
const std::string Encoder::halt_comment =
comment(
::Encoder::halt_comment + " - " + halt_sym + "_<step>_<thread>" + eol);
ConcuBinE::Encoder::halt_comment
+ " - "
+ halt_sym
+ "_<step>_<thread>"
+ eol);
const std::string Encoder::heap_comment =
comment(
::Encoder::heap_comment + " - " + heap_sym + "_<step>" + eol);
ConcuBinE::Encoder::heap_comment
+ " - "
+ heap_sym
+ "_<step>"
+ eol);
const std::string Encoder::exit_flag_comment =
comment(
::Encoder::exit_flag_comment + " - " + exit_flag_sym + "_<step>" + eol);
ConcuBinE::Encoder::exit_flag_comment
+ " - "
+ exit_flag_sym
+ "_<step>"
+ eol);
const std::string Encoder::exit_code_comment =
comment(::Encoder::exit_code_comment + eol);
comment(ConcuBinE::Encoder::exit_code_comment + eol);
const std::string Encoder::thread_comment =
comment(
::Encoder::thread_comment + " - " + thread_sym + "_<step>_<thread>" + eol);
ConcuBinE::Encoder::thread_comment
+ " - "
+ thread_sym
+ "_<step>_<thread>"
+ eol);
const std::string Encoder::exec_comment =
comment(
::Encoder::exec_comment + " - " + exec_sym + "_<step>_<thread>_<pc>" + eol);
ConcuBinE::Encoder::exec_comment
+ " - "
+ exec_sym
+ "_<step>_<thread>_<pc>"
+ eol);
const std::string Encoder::flush_comment =
comment(
::Encoder::flush_comment + " - " + flush_sym + "_<step>_<thread>" + eol);
ConcuBinE::Encoder::flush_comment
+ " - "
+ flush_sym
+ "_<step>_<thread>"
+ eol);
const std::string Encoder::check_comment =
comment(
::Encoder::check_comment + " - " + check_sym + "_<step>_<id>" + eol);
ConcuBinE::Encoder::check_comment
+ " - "
+ check_sym
+ "_<step>_<id>"
+ eol);
//------------------------------------------------------------------------------
// constructors
//------------------------------------------------------------------------------
Encoder::Encoder (const Program::List::ptr & p, const size_t b) :
::Encoder(p, b),
ConcuBinE::Encoder(p, b),
step(0)
{}
......@@ -1126,4 +1183,4 @@ std::string Encoder::encode (const Instruction::Exit & e)
return word2hex(e.arg);
}
} // namespace smtlib
} // namespace ConcuBinE::smtlib
......@@ -4,7 +4,7 @@
#include "smtlib.hh"
namespace smtlib {
namespace ConcuBinE::smtlib {
//==============================================================================
// smtlib::Functional
......@@ -347,4 +347,4 @@ void Functional::encode ()
define_exit_code();
}
} // namespace smtlib
} // namespace ConcuBinE::smtlib
......@@ -4,7 +4,7 @@
#include "smtlib.hh"
namespace smtlib {
namespace ConcuBinE::smtlib {
//==============================================================================
// smtlib::Relational::State
......@@ -713,4 +713,4 @@ std::string Relational::encode (const Instruction::Exit & e)
return state;
}
} // namespace smtlib
} // namespace ConcuBinE::smtlib
......@@ -5,6 +5,8 @@
#include "encoder.hh"
#include "simulator.hh"
namespace ConcuBinE {
//==============================================================================
// Model<POD>
//
......@@ -38,10 +40,10 @@ struct Model : Instruction::Concept
return std::make_unique<Model<POD>>(pod);
}
bool is_nullary () const { return ::is_nullary<POD>; }
bool is_unary () const { return ::is_unary<POD>; }
bool is_memory () const { return ::is_memory<POD>; }
bool is_jump () const { return ::is_jump<POD>; }
bool is_nullary () const { return ConcuBinE::is_nullary<POD>; }
bool is_unary () const { return ConcuBinE::is_unary<POD>; }
bool is_memory () const { return ConcuBinE::is_memory<POD>; }
bool is_jump () const { return ConcuBinE::is_jump<POD>; }
bool requires_flush () const
{
......@@ -55,7 +57,7 @@ struct Model : Instruction::Concept
word_t arg () const
{
if constexpr(::is_unary<POD>)
if constexpr(ConcuBinE::is_unary<POD>)
return pod.arg;
else
{ assert(false); return 0; }
......@@ -63,7 +65,7 @@ struct Model : Instruction::Concept
void arg (const word_t a [[maybe_unused]])
{
if constexpr(::is_unary<POD>)
if constexpr(ConcuBinE::is_unary<POD>)
pod.arg = a;
else
assert(false);
......@@ -71,7 +73,7 @@ struct Model : Instruction::Concept
bool indirect () const
{
if constexpr(::is_memory<POD>)
if constexpr(ConcuBinE::is_memory<POD>)
return pod.indirect;
else
{ assert(false); return false; }
......@@ -79,7 +81,7 @@ struct Model : Instruction::Concept
void indirect (const bool i [[maybe_unused]])
{
if constexpr(::is_memory<POD>)
if constexpr(ConcuBinE::is_memory<POD>)
pod.indirect = i;
else
assert(false);
......@@ -288,3 +290,5 @@ bool operator != (const Instruction & a, const Instruction & b)
{
return !(a == b);
}
} // namespace ConcuBinE
......@@ -8,6 +8,8 @@
#include "common.hh"
namespace ConcuBinE {
//==============================================================================
// macros
//==============================================================================
......@@ -270,4 +272,6 @@ struct Instruction
bool operator == (const Instruction &, const Instruction &);
bool operator != (const Instruction &, const Instruction &);
} // namespace ConcuBinE
#endif
......@@ -10,6 +10,8 @@
#include "z3.hh"
#include "cvc4.hh"
namespace ConcuBinE {
//==============================================================================
// global flags
//==============================================================================
......@@ -442,6 +444,8 @@ int solve (const char * name, const int argc, const char ** argv)
return 0;
}
} // namespace ConcuBinE
//==============================================================================
// main
//==============================================================================
......@@ -453,23 +457,23 @@ int main (const int argc, const char ** argv)
// forward to given command's main
if (!strcmp(argv[1], "help"))
{
return help(argv[0], argc - 2, argv + 2);
return ConcuBinE::help(argv[0], argc - 2, argv + 2);
}
else if (!strcmp(argv[1], "simulate"))
{
return simulate(argv[0], argc - 2, argv + 2);
return ConcuBinE::simulate(argv[0], argc - 2, argv + 2);
}
else if (!strcmp(argv[1], "replay"))
{
return replay(argv[0], argc - 2, argv + 2);
return ConcuBinE::replay(argv[0], argc - 2, argv + 2);
}
else if (!strcmp(argv[1], "solve"))
{
return solve(argv[0], argc - 2, argv + 2);
return ConcuBinE::solve(argv[0], argc - 2, argv + 2);
}
}
// found no command
print_usage_main(argv[0]);
ConcuBinE::print_usage_main(argv[0]);
return -1;
}
......@@ -3,6 +3,8 @@
#include <fstream>
namespace ConcuBinE {
// error reporting helper
//
inline void parser_error (const std::string & file,
......@@ -25,4 +27,6 @@ inline T create_from_file (const std::string & path)
throw std::runtime_error(path + " not found");
}
} // namespace ConcuBinE
#endif
......@@ -5,6 +5,8 @@
#include "instruction.hh"
#include "parser.hh"
namespace ConcuBinE {
//==============================================================================
// macros
//==============================================================================
......@@ -318,3 +320,5 @@ bool operator != (const Program & a, const Program & b)
{
return !(a == b);
}
} // namespace ConcuBinE
......@@ -10,6 +10,8 @@
#include "common.hh"
namespace ConcuBinE {
//==============================================================================
// forward declarations
//==============================================================================
......@@ -113,4 +115,6 @@ struct Program : public std::vector<Instruction>
bool operator == (const Program &, const Program &);
bool operator != (const Program &, const Program &);
} // namespace ConcuBinE
#endif
......@@ -4,6 +4,8 @@
#include <unistd.h>
#include <sys/wait.h>
namespace ConcuBinE {
//==============================================================================
// constants
//==============================================================================
......@@ -146,3 +148,5 @@ std::stringstream Shell::run (const std::string & cmd,
return output;
}
} // namespace ConcuBinE
......@@ -3,6 +3,8 @@
#include <sstream>
namespace ConcuBinE {
//==============================================================================
// Shell
//==============================================================================
......@@ -36,4 +38,6 @@ public:
std::stringstream run (const std::string & cmd, const std::string & input);
};
} // namespace ConcuBinE
#endif
......@@ -4,6 +4,8 @@
#include <random>
#include <sstream>
namespace ConcuBinE {
//==============================================================================
// functions
//==============================================================================
......@@ -55,136 +57,6 @@ Simulator::Simulator (const Program::List::ptr & p,
// member functions
//------------------------------------------------------------------------------
// Simulator::check_and_resume -------------------------------------------------
void Simulator::check_and_resume (word_t id)
{