Merge pull request PrincetonUniversity#205 from Bo-Yuan-Huang/i203

Issue 203: missing valid condition check

CMakeLists.txt

@@ -11,7 +11,7 @@ endif()
 # PROJECT
 # name version language
 # ---------------------------------------------------------------------------- #
-project(ilang VERSION     1.1.3
+project(ilang VERSION     1.1.4
               LANGUAGES   CXX
 )
 

README.md

@@ -4,7 +4,6 @@
 [![Build Status](https://travis-ci.com/Bo-Yuan-Huang/ILAng.svg?branch=master)](https://travis-ci.com/Bo-Yuan-Huang/ILAng)
 [![Build Status](https://ilang.semaphoreci.com/badges/ILAng.svg)](https://ilang.semaphoreci.com/projects/ILAng)
 [![Build status](https://ci.appveyor.com/api/projects/status/cwhlq09513art6hw/branch/master?svg=true)](https://ci.appveyor.com/project/Bo-Yuan-Huang/ilang/branch/master)
-[![Coverity Scan Build Status](https://scan.coverity.com/projects/17719/badge.svg)](https://scan.coverity.com/projects/bo-yuan-huang-ilang)
 [![Coverage Status](https://coveralls.io/repos/github/Bo-Yuan-Huang/ILAng/badge.svg?branch=master)](https://coveralls.io/github/Bo-Yuan-Huang/ILAng?branch=master)
 [![Language grade: C/C++](https://img.shields.io/lgtm/grade/cpp/g/Bo-Yuan-Huang/ILAng.svg?logo=lgtm&logoWidth=18)](https://lgtm.com/projects/g/Bo-Yuan-Huang/ILAng/context:cpp)
 [![Codacy Badge](https://api.codacy.com/project/badge/Grade/b120e2527cc04d4aacd1dc11581e2f30)](https://www.codacy.com/app/Bo-Yuan-Huang/ILAng?utm_source=github.com&utm_medium=referral&utm_content=Bo-Yuan-Huang/ILAng&utm_campaign=Badge_Grade)

include/ilang/ila-mngr/u_abs_knob.h

@@ -9,8 +9,8 @@
 /// \namespace ilang
 namespace ilang {
 
-/// \namespace AbsKnob
-namespace AbsKnob {
+/// \namespace absknob
+namespace absknob {
 /****************************************************************************/
 /// Add all dependent vars of the expr to the set.
 void InsertVar(const ExprPtr& e, ExprSet& vars);
@@ -108,7 +108,7 @@ InstrPtr DuplInstr(const InstrCnstPtr instr_src, const InstrLvlAbsPtr& dst,
 /// Duplicate instruction sequence to dst. NOT IMPLEMENTED YET.
 void DuplInstrSeq(const InstrLvlAbsCnstPtr& src, const InstrLvlAbsPtr& dst);
 
-}; // namespace AbsKnob
+}; // namespace absknob
 
 } // namespace ilang
 

include/ilang/target-sc/ilator.h

@@ -77,6 +77,8 @@ class Ilator {
   /// Generation bootstrap, e.g., creating directories.
   bool Bootstrap(const std::string& root, bool opt);
 
+  /// Interpret non-instr basics, e.g., valid.
+  bool GenerateIlaBasics(const std::string& dir);
   /// Interpret instruction semantics (decode and state updates).
   bool GenerateInstrContent(const InstrPtr& instr, const std::string& dir);
   /// Special handle for memory updates.
@@ -143,6 +145,8 @@ class Ilator {
   static std::string GetCxxType(const SortPtr& sort);
   /// Get the variable name in SystemC.
   static std::string GetCxxName(const ExprPtr& expr);
+  /// Get the valid function name of the ILA.
+  static std::string GetValidFuncName(const InstrLvlAbsCnstPtr& m);
   /// Get the decode function name of the instruction.
   static std::string GetDecodeFuncName(const InstrPtr& instr);
   /// Get the state update function name of the instruction.

src/ila-mngr/p_sanity_check_and_fix.cc

@@ -65,7 +65,7 @@ bool SanityCheckAndFix(const InstrLvlAbsPtr& m) {
 
   // check completeness
   auto acc = asthub::BoolConst(false);
-  for (const auto& instr : AbsKnob::GetInstrTree(m)) {
+  for (const auto& instr : absknob::GetInstrTree(m)) {
     auto host = instr->host();
     ILA_NOT_NULL(host);
     auto valid = host->valid() ? host->valid() : asthub::BoolConst(true);
@@ -78,7 +78,7 @@ bool SanityCheckAndFix(const InstrLvlAbsPtr& m) {
   if (!is_complete) {
     ILA_WARN << "Incomplete instruction set - create default instruction";
     auto clean = true;
-    for (const auto& var : AbsKnob::GetVar(acc)) {
+    for (const auto& var : absknob::GetVar(acc)) {
       auto is_top_state = m->find_state(var->name());
       auto is_top_input = m->find_input(var->name());
       clean &= (is_top_state || is_top_input);

src/ila-mngr/u_abs_knob.cc

@@ -8,7 +8,7 @@
 
 namespace ilang {
 
-namespace AbsKnob {
+namespace absknob {
 
 ExprPtr DuplInp(const InstrLvlAbsPtr& m, const ExprPtr& inp) {
   ILA_ASSERT(inp->is_var()) << "Creating input from non-var Expr.";
@@ -392,6 +392,6 @@ void DuplInstrSeq(const InstrLvlAbsCnstPtr& src, const InstrLvlAbsPtr& dst) {
   // TODO
 }
 
-} // namespace AbsKnob
+} // namespace absknob
 
 } // namespace ilang

src/ila-mngr/u_rewrite_ila.cc

@@ -27,9 +27,9 @@ bool FuncObjRewrIla::pre(const InstrLvlAbsCnstPtr& src) {
       << "Rewriting ILA to partially constructed ILA not support.";
 
   // input
-  AbsKnob::DuplInp(src, dst, expr_map_);
+  absknob::DuplInp(src, dst, expr_map_);
   // state
-  AbsKnob::DuplStt(src, dst, expr_map_);
+  absknob::DuplStt(src, dst, expr_map_);
 
   // child
   for (decltype(src->child_num()) i = 0; i != src->child_num(); i++) {
@@ -40,20 +40,20 @@ bool FuncObjRewrIla::pre(const InstrLvlAbsCnstPtr& src) {
   }
 
   // fetch
-  AbsKnob::DuplFetch(src, dst, expr_map_);
+  absknob::DuplFetch(src, dst, expr_map_);
   // valid
-  AbsKnob::DuplValid(src, dst, expr_map_);
+  absknob::DuplValid(src, dst, expr_map_);
   // init
-  AbsKnob::DuplInit(src, dst, expr_map_);
+  absknob::DuplInit(src, dst, expr_map_);
 
   // instruction && child-program
   for (decltype(src->instr_num()) i = 0; i != src->instr_num(); i++) {
     auto i_src = src->instr(i);
-    AbsKnob::DuplInstr(i_src, dst, expr_map_, ila_map_);
+    absknob::DuplInstr(i_src, dst, expr_map_, ila_map_);
   }
 
   // sequence
-  AbsKnob::DuplInstrSeq(src, dst);
+  absknob::DuplInstrSeq(src, dst);
 
   return false;
 }
@@ -84,23 +84,23 @@ bool FuncObjFlatIla::pre(const InstrLvlAbsCnstPtr& src) {
     valid_cond_ = asthub::BoolConst(true);
   }
 #ifdef VALID_STACK
-  valid_cond_ = AbsKnob::Rewrite(valid_cond_, expr_map_);
+  valid_cond_ = absknob::Rewrite(valid_cond_, expr_map_);
   valid_cond_stack_.push(asthub::And(valid_cond_stack_.top(), valid_cond_));
   const auto& hierarchical_valid_cond = valid_cond_stack_.top();
 #endif // VALID_STACK
 
   // instruction && child-program
   for (decltype(src->instr_num()) i = 0; i != src->instr_num(); i++) {
     auto i_src = src->instr(i);
-    auto i_dst = AbsKnob::DuplInstr(i_src, dst, expr_map_, ila_map_);
+    auto i_dst = absknob::DuplInstr(i_src, dst, expr_map_, ila_map_);
 #ifdef VALID_STACK
     auto new_decode = asthub::And(i_dst->decode(), hierarchical_valid_cond);
     i_dst->ForceSetDecode(new_decode);
 #endif // VALID_STACK
   }
 
   // sequence - do we need to do this?
-  // AbsKnob::DuplInstrSeq(src, dst);
+  // absknob::DuplInstrSeq(src, dst);
 
   return false;
 }

src/ila-mngr/u_unroller.cc

@@ -341,7 +341,7 @@ void PathUnroll::DefineDepVar() {
   // collect the set of vars
   auto dep_var = ExprSet();
   for (auto it = seq_.begin(); it != seq_.end(); it++) {
-    AbsKnob::InsertStt(*it, dep_var);
+    absknob::InsertStt(*it, dep_var);
   }
   // update to the global set
   vars_.clear();
@@ -404,7 +404,7 @@ ZExpr MonoUnroll::MonoIncr(const InstrLvlAbsPtr& top, const int& length,
 
 void MonoUnroll::DefineDepVar() {
   vars_.clear();
-  auto dep_var = AbsKnob::GetSttTree(top_);
+  auto dep_var = absknob::GetSttTree(top_);
   // update global
   ILA_ASSERT(!dep_var.empty()) << "No state var found.";
   for (auto it = dep_var.begin(); it != dep_var.end(); it++) {
@@ -423,7 +423,7 @@ void MonoUnroll::Transition(const int& idx) {
   }
 
   // extract the set of insturctions
-  auto instr_set = AbsKnob::GetInstrTree(top_);
+  auto instr_set = absknob::GetInstrTree(top_);
 
   // create the set of selection bits
   std::vector<ExprPtr> sel_bits;

src/ila-mngr/u_unroller_smt.cc

@@ -84,7 +84,7 @@ template class UnrollerSmt<SmtSwitchItf>;
 template <class Generator> void PathUnroller<Generator>::SetDecidingVars() {
   ExprSet unique_vars;
   for (const auto& instr : seq_) {
-    AbsKnob::InsertStt(instr, unique_vars);
+    absknob::InsertStt(instr, unique_vars);
   }
   // move to global order
   this->deciding_vars_.clear();

src/ila-mngr/v_eq_check_crr.cc

@@ -186,8 +186,8 @@ void CommDiag::Init() {
     un.AddGlobPred(ref->flush());
   }
   // state vars of each ILA
-  stts_a_ = AbsKnob::GetSttTree(crr_->refine_a()->ila());
-  stts_b_ = AbsKnob::GetSttTree(crr_->refine_b()->ila());
+  stts_a_ = absknob::GetSttTree(crr_->refine_a()->ila());
+  stts_b_ = absknob::GetSttTree(crr_->refine_b()->ila());
 }
 
 CommDiag::Unroll& CommDiag::GetUnrl(const UID& uid) {
@@ -322,8 +322,8 @@ bool CommDiag::IncEqCheck(const int& min, const int& max, const int& step) {
 
   const auto ma = crr_->refine_a()->coi(); // representative ILA
   const auto mb = crr_->refine_b()->coi();
-  const auto stts_a = AbsKnob::GetSttTree(ma); // used for marking
-  const auto stts_b = AbsKnob::GetSttTree(mb);
+  const auto stts_a = absknob::GetSttTree(ma); // used for marking
+  const auto stts_b = absknob::GetSttTree(mb);
 
   auto s = z3::solver(ctx_); // solver
   { // default basic condition (old/new/apply path & assm & prop)
@@ -528,7 +528,7 @@ bool CommDiag::SanityCheckRefinement(const RefPtr ref) {
   // check: /\s_n, a_n -> (a_n & f_o & eq_o_n)
   s.reset();
   auto appl_z3 = z3::expr_vector(ctx_);
-  auto appl_vars = AbsKnob::GetVar(a);
+  auto appl_vars = absknob::GetVar(a);
   for (auto it = appl_vars.begin(); it != appl_vars.end(); it++) {
     appl_z3.push_back(unroll_appl_.CurrState(*it, 0));
   }
@@ -550,11 +550,11 @@ bool CommDiag::SanityCheckRelation(const RelPtr rel, const InstrLvlAbsPtr& ma,
 
   ILA_NOT_NULL(rel);
   auto rel_expr = rel->get();
-  auto rel_vars = AbsKnob::GetVar(rel_expr);
+  auto rel_vars = absknob::GetVar(rel_expr);
 
   auto ref_vars = ExprSet();
-  AbsKnob::InsertStt(ma, ref_vars);
-  AbsKnob::InsertStt(mb, ref_vars);
+  absknob::InsertStt(ma, ref_vars);
+  absknob::InsertStt(mb, ref_vars);
 
   // check: rel_vars <= ref_vars
   for (auto it = rel_vars.begin(); it != rel_vars.end(); it++) {
@@ -709,7 +709,7 @@ z3::expr CommDiag::GetZ3ApplInstr(const ExprSet& stts, const RefPtr ref) {
 
 z3::expr CommDiag::GenInit(const RefPtr ref) {
   // default equivalence: state variables (not including inputs)
-  auto vars = AbsKnob::GetSttTree(ref->coi());
+  auto vars = absknob::GetSttTree(ref->coi());
   auto eq = ctx_.bool_val(true);
   for (auto it = vars.begin(); it != vars.end(); it++) {
     auto so = unroll_orig_.CurrState(*it, 0);
@@ -833,7 +833,7 @@ z3::expr CommDiag::UnrollFlush(MonoUnroll& unroller, const RefPtr ref,
   // unroll
   auto path = unroller.MonoAssn(ref->coi(), length, base);
 
-  auto vars = AbsKnob::GetStt(ref->coi());
+  auto vars = absknob::GetStt(ref->coi());
   auto mark = ctx_.bool_val(true);
   // mark complete step with representing state
   for (auto i = start; i <= base + length; i++) {

src/ila-mngr/v_refinement.cc

@@ -19,7 +19,7 @@ void RefinementMap::set_tgt(const InstrLvlAbsPtr& tgt) {
 
 void RefinementMap::set_tgt(const InstrPtr& tgt) {
   ILA_ASSERT(tgt && tgt->host());
-  coi_ = AbsKnob::ExtrDeptModl(tgt, tgt->host()->name().str());
+  coi_ = absknob::ExtrDeptModl(tgt, tgt->host()->name().str());
 }
 
 void RefinementMap::set_appl(const ExprPtr& appl) {

src/ilang++.cc

@@ -584,8 +584,8 @@ void InstrRef::ExportToVerilog(std::ostream& fout) const {
 }
 
 void InstrRef::ExportToVerilogWithChild(std::ostream& fout) const {
-  auto dept_ila_ptr = AbsKnob::ExtrDeptModl(ptr_, ptr_->name().str() + "_ila_");
-  AbsKnob::FlattenIla(dept_ila_ptr);
+  auto dept_ila_ptr = absknob::ExtrDeptModl(ptr_, ptr_->name().str() + "_ila_");
+  absknob::FlattenIla(dept_ila_ptr);
 
   VerilogGenerator vgen(VerilogGenerator::VlgGenConfig(
       true)); // overwrite default configuration : memory is external
@@ -693,7 +693,7 @@ void Ila::ExportToVerilog(std::ostream& fout) const {
   vgen.DumpToFile(fout);
 }
 
-void Ila::FlattenHierarchy() { AbsKnob::FlattenIla(ptr_); }
+void Ila::FlattenHierarchy() { absknob::FlattenIla(ptr_); }
 
 bool Ila::ExecutePass(const std::vector<PassID>& passes) const {
   auto status = true;