More

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]);
@@ -52,12 +51,7 @@ int main( int argc, char* argv[] )
     {
       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 +69,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 +142,20 @@ int main( int argc, char* argv[] )
       EO_FATAL() << "Error: mulitple files specified, \"" << file << "\" and \"" << arg << "\"";
     }
   }
+  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 +211,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

@@ -80,15 +80,15 @@ 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)
+    if (itri->second.d_time==itrj->second.d_time)
     {
-      return true;
+      return itri->second.d_count>itrj->second.d_count;
     }
-    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)
@@ -102,7 +102,8 @@ 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;
-  for (size_t i=0; i<2; i++)
+  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())
@@ -111,22 +112,29 @@ std::string Stats::toString(State& s, bool compact) const
     }
     if (!compact)
     {
-      ss << "========================================================================" << std::endl;
-      ss << std::right << std::setw(28) << (i==0 ? "Rule  " : "Program  ");
+      ss << "====================================================================================" << std::endl;
+      ss << std::right << std::setw(40) << (i==0 ? "Rule  " : "Program  ");
       ss << std::left << std::setw(7) << "#";
-      if (i==1)
+      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 : 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
@@ -163,7 +171,7 @@ std::string Stats::toString(State& s, bool compact) const
       else
       {
         sss << ": ";
-        ss << std::right << std::setw(28) << sss.str();
+        ss << std::right << std::setw(40) << sss.str();
         if (i==0)
         {
           ss << rs.toString(totalTime) << std::endl;

src/stats.h

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

src/type_checker.cpp

@@ -936,7 +936,11 @@ Expr TypeChecker::evaluateProgramInternal(
     Expr prog = d_state.getProgram(hd);
     if (d_statsEnabled)
     {
-      d_sts.d_pstats[prog.getValue()].d_count++;
+      Trace("type_checker") << "increment stat " << Expr(hd) << std::endl;
+      RuleStat * ps = &d_sts.d_pstats[hd];
+      Trace("type_checker") << "rule " << ps << std::endl;
+      ps->d_count++;
+      Trace("type_checker") << "...finish" << std::endl;
     }
     Assert (!prog.isNull());
     if (!prog.isNull())

user_manual.md

@@ -1942,6 +1942,7 @@ The Ethos command line interface can be invoked by `ethos <option>* <file>` wher
 - `--reference=X`: includes the file specified by `X` as a reference file.
 - `--show-config`: displays the build information for the given binary.
 - `--stats`: enables detailed statistics.
+- `--stats-all`: enables all available statistics, including program invocations.
 - `--stats-compact`: print statistics in a compact format.
 - `-t <tag>`: enables the given trace tag (for debugging).
 - `-v`: verbose mode, enable all standard trace messages.