Add --stats-all

src/expr_parser.cpp

@@ -596,7 +596,7 @@ Expr ExprParser::parseExpr()
               // make the program variable, whose type is abstract
               Expr ftype = d_state.mkFunctionType(fargTypes, atype, false);
               std::stringstream pvname;
-              pvname << "_match_" << hd;
+              pvname << "eo::match_" << hd;
               Expr pv = d_state.mkSymbol(Kind::PROGRAM_CONST, pvname.str(), ftype);
               // process the cases
               std::vector<Expr> cases;

src/main.cpp

@@ -21,14 +21,13 @@ using namespace ethos;
 int main( int argc, char* argv[] )
 {
   Options opts;
-  Stats stats;
-  State s(opts, stats);
-  Plugin* plugin = nullptr;
   // read the options
   size_t i = 1;
   std::string file;
   bool readFile = false;
   size_t nargs = static_cast<size_t>(argc);
+  // the list of includes and whether they were an include or reference
+  std::vector<std::pair<std::string, bool>> includes;
   while (i<nargs)
   {
     std::string arg(argv[i]);
@@ -50,14 +49,10 @@ int main( int argc, char* argv[] )
     bool isInclude = (arg.compare(0, 10, "--include=") == 0);
     if (isInclude || arg.compare(0, 12, "--reference=") == 0)
     {
+      // defer the inclusion until the options are finalized
       size_t first = arg.find_first_of("=");
       std::string file = arg.substr(first + 1);
-      // cannot provide reference
-      Expr refNf;
-      if (!s.includeFile(file, isInclude, !isInclude, refNf))
-      {
-        EO_FATAL() << "Error: cannot include file " << file;
-      }
+      includes.emplace_back(file, isInclude);
       continue;
     }
     if (arg == "--help")
@@ -75,6 +70,7 @@ int main( int argc, char* argv[] )
       out << "      --reference=X: includes the file specified by X as a reference file." << std::endl;
       out << "      --show-config: displays the build information for this binary." << std::endl;
       out << "            --stats: enables detailed statistics." << std::endl;
+      out << "        --stats-all: enables all available statistics." << std::endl;
       out << "    --stats-compact: print statistics in a compact format." << std::endl;
       out << "           -t <tag>: enables the given trace tag (requires debug build)." << std::endl;
       out << "                 -v: verbose mode, enable all standard trace messages (requires debug build)." << std::endl;
@@ -147,6 +143,21 @@ int main( int argc, char* argv[] )
       EO_FATAL() << "Error: mulitple files specified, \"" << file << "\" and \"" << arg << "\"";
     }
   }
+  // options are finalized, now initialize the state and run the includes
+  Stats stats;
+  State s(opts, stats);
+  Plugin* plugin = nullptr;
+  for (size_t i=0, nincludes=includes.size(); i<nincludes; i++)
+  {
+    std::string file = includes[i].first;
+    bool isInclude = includes[i].second;
+    // cannot provide reference
+    Expr refNf;
+    if (!s.includeFile(file, isInclude, !isInclude, refNf))
+    {
+      EO_FATAL() << "Error: cannot include file " << file;
+    }
+  }
   // NOTE: initialization of plugin goes here
   if (plugin!=nullptr)
   {
@@ -202,7 +213,7 @@ int main( int argc, char* argv[] )
   }
   if (opts.d_stats)
   {
-    std::cout << stats.toString(s, opts.d_statsCompact);
+    std::cout << stats.toString(s, opts.d_statsCompact, opts.d_statsAll);
   }
   // exit immediately, which avoids deleting all expressions which can take time
   exit(0);

src/state.cpp

@@ -22,6 +22,7 @@ Options::Options()
   d_parseLet = true;
   d_printLet = false;
   d_stats = false;
+  d_statsAll = false;
   d_statsCompact = false;
   d_ruleSymTable = true;
   d_normalizeDecimal = true;
@@ -48,13 +49,16 @@ bool Options::setOption(const std::string& key, bool val)
   {
     d_stats = val;
   }
+  else if (key == "stats-all")
+  {
+    // also implies stats are enabled.
+    d_stats = val ? true : d_stats;
+    d_statsAll = val;
+  }
   else if (key == "stats-compact")
   {
-    if (val)
-    {
-      // also implies stats are enabled.
-      d_stats = val;
-    }
+    // also implies stats are enabled.
+    d_stats = val ? true : d_stats;
     d_statsCompact = val;
   }
   else if (key == "rule-sym-table")
@@ -86,9 +90,9 @@ State::State(Options& opts, Stats& stats)
     : d_hashCounter(0),
       d_hasReference(false),
       d_inGarbageCollection(false),
-      d_tc(*this, opts),
       d_opts(opts),
       d_stats(stats),
+      d_tc(*this, opts),
       d_plugin(nullptr)
 {
   ExprValue::d_state = this;

src/state.h

@@ -38,6 +38,7 @@ class Options
   /** 'let' is lexed as the SMT-LIB syntax for a dag term specified by a let */
   bool d_parseLet;
   bool d_stats;
+  bool d_statsAll;
   bool d_statsCompact;
   bool d_ruleSymTable;
   bool d_normalizeDecimal;
@@ -332,12 +333,12 @@ class State
   /** Are we in garbage collection? */
   bool d_inGarbageCollection;
   //--------------------- utilities
-  /** Type checker */
-  TypeChecker d_tc;
   /** Options */
   Options& d_opts;
   /** Stats */
   Stats& d_stats;
+  /** Type checker */
+  TypeChecker d_tc;
   /** Plugin, if using one */
   Plugin* d_plugin;
 };

src/stats.cpp

@@ -43,12 +43,10 @@ std::string RuleStat::toString(std::time_t totalTime) const
 {
   std::stringstream ss;
   std::stringstream st;
+  ss << std::left << std::setw(7) << d_count;
   double pct = static_cast<double>(100*d_time)/static_cast<double>(totalTime);
   st << d_time << " (" << std::fixed << std::setprecision(1) << pct << "%)";
   ss << std::left << std::setw(17) << st.str();
-  std::stringstream sc;
-  sc << d_count;
-  ss << std::left << std::setw(7) << sc.str();
   // time per rule
   double timePerRule = static_cast<double>(d_time)/static_cast<double>(d_count);
   std::stringstream sp;
@@ -65,6 +63,9 @@ Stats::Stats() : d_mkExprCount(0), d_exprCount(0), d_deleteExprCount(0), d_symCo
   d_startTime = getCurrentTime();
 }
 
+/**
+ * Either sorts by time or by counts
+ */
 struct SortRuleTime
 {
   SortRuleTime(const std::map<const ExprValue*, RuleStat>& rs) : d_rstats(rs)
@@ -79,16 +80,20 @@ struct SortRuleTime
     std::map<const ExprValue*, RuleStat>::const_iterator itrj;
     itrj = d_rstats.find(j);
     Assert (itrj!=d_rstats.end());
+    if (itri->second.d_time==itrj->second.d_time)
+    {
+      return itri->second.d_count>itrj->second.d_count;
+    }
     return itri->second.d_time>itrj->second.d_time;
   }
 };
 
-std::string Stats::toString(State& s, bool compact) const
+std::string Stats::toString(State& s, bool compact, bool all) const
 {
   std::stringstream ss;
   if (!compact)
   {
-    ss << "========================================================================" << std::endl;
+    ss << "====================================================================================" << std::endl;
   }
   ss << "mkExprCount = " << d_mkExprCount << std::endl;
   ss << "newExprCount = " << d_exprCount << std::endl;
@@ -97,40 +102,56 @@ std::string Stats::toString(State& s, bool compact) const
   ss << "litCount = " << d_litCount << std::endl;
   std::time_t totalTime = (getCurrentTime()-d_startTime);
   ss << "time = " << totalTime << std::endl;
-  if (!d_rstats.empty())
+  size_t imax = all ? 2 : 1;
+  for (size_t i=0; i<imax; i++)
   {
+    const std::map<const ExprValue*, RuleStat>& rs = i==0 ? d_rstats : d_pstats;
+    if (rs.empty())
+    {
+      continue;
+    }
     if (!compact)
     {
-      ss << "========================================================================" << std::endl;
-      ss << std::right << std::setw(28) << "Rule  ";
-      ss << std::left << std::setw(17) << "t";
+      ss << "====================================================================================" << std::endl;
+      ss << std::right << std::setw(40) << (i==0 ? "Rule  " : "Program  ");
       ss << std::left << std::setw(7) << "#";
-      ss << std::left << std::setw(10) << "t/#";
-      ss << std::left << std::setw(10) << "#mkExpr";
+      if (i==0)
+      {
+        ss << std::left << std::setw(17) << "t";
+        ss << std::left << std::setw(10) << "t/#";
+        ss << std::left << std::setw(10) << "#mkExpr";
+      }
       ss << std::endl;
-      ss << "========================================================================" << std::endl;
+      ss << "====================================================================================" << std::endl;
     }
     // display stats for each rule
     std::vector<const ExprValue*> sortedStats;
-    for (const std::pair<const ExprValue* const, RuleStat>& r : d_rstats)
+    for (const std::pair<const ExprValue* const, RuleStat>& r : rs)
     {
+      // might be an internal match program, in which case, skip
+      Expr sym(r.first);
+      std::string symbol = sym.getSymbol();
+      if (symbol.compare(0, 4, "eo::")==0)
+      {
+        continue;
+      }
       sortedStats.push_back(r.first);
     }
     // sort based on time
-    SortRuleTime srt(d_rstats);
+    SortRuleTime srt(rs);
     std::sort(sortedStats.begin(), sortedStats.end(), srt);    
     std::map<const ExprValue*, RuleStat>::const_iterator itr;
+    std::stringstream ssCount;
     std::stringstream ssCheck;
     std::stringstream ssMkExpr;
     bool firstTime = true;
     for (const ExprValue* e : sortedStats)
     {
-      itr = d_rstats.find(e);
-      Assert (itr!=d_rstats.end());
+      itr = rs.find(e);
+      Assert (itr!=rs.end());
       const RuleStat& rs = itr->second;
-      Assert (e->getKind()==Kind::PROOF_RULE);
-      std::stringstream sss;
-      sss << Expr(e);
+      std::stringstream ssExpr;
+      ssExpr << Expr(e);
       if (compact)
       {
         if (firstTime)
@@ -139,22 +160,36 @@ std::string Stats::toString(State& s, bool compact) const
         }
         else
         {
+          ssCount << ", ";
           ssCheck << ", ";
           ssMkExpr << ", ";
         }
-        ssCheck << sss.str() << ": " << rs.d_time;
-        ssMkExpr << sss.str() << ": " << rs.d_mkExprCount;
+        ssCount << ssExpr.str() << ": " << rs.d_count;
+        ssCheck << ssExpr.str() << ": " << rs.d_time;
+        ssMkExpr << ssExpr.str() << ": " << rs.d_mkExprCount;
       }
       else
       {
-        sss << ": ";
-        ss << std::right << std::setw(28) << sss.str() << rs.toString(totalTime) << std::endl;
+        ssExpr << ": ";
+        ss << std::right << std::setw(40) << ssExpr.str();
+        if (i==0)
+        {
+          ss << rs.toString(totalTime) << std::endl;
+        }
+        else
+        {
+          ss << rs.d_count << std::endl;
+        }
       }
     }
     if (compact)
     {
-      ss << "checkTime = { " << ssCheck.str() << " }" << std::endl;
-      ss << "mkExpr = { " << ssMkExpr.str() << " }" << std::endl;
+      ss << (i==0 ? "rule" : "prog") << "Count = { " << ssCount.str() << " }" << std::endl;
+      if (i==0)
+      {
+        ss << "checkTime = { " << ssCheck.str() << " }" << std::endl;
+        ss << "mkExpr = { " << ssMkExpr.str() << " }" << std::endl;
+      }
     }
   }
   return ss.str();

src/stats.h

@@ -46,7 +46,8 @@ class Stats
   size_t d_litCount;
   std::time_t d_startTime;
   std::map<const ExprValue*, RuleStat> d_rstats;
-  std::string toString(State& s, bool compact) const;
+  std::map<const ExprValue*, RuleStat> d_pstats;
+  std::string toString(State& s, bool compact, bool all) const;
 
   static std::time_t getCurrentTime();
 };