From cef17c22a1d4a75e0335dbfce0f450563c2a870f Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Mon, 2 Jul 2018 17:08:02 +0100
Subject: [PATCH] remove some allocs from exceptions

---
 src/cmd_context/basic_cmds.cpp    | 4 ++--
 src/cmd_context/cmd_context.cpp   | 2 +-
 src/muz/fp/horn_tactic.cpp        | 2 +-
 src/parsers/smt2/smt2parser.cpp   | 6 +++---
 src/qe/nlqsat.cpp                 | 3 +--
 src/qe/qsat.cpp                   | 4 ++--
 src/sat/tactic/goal2sat.cpp       | 2 +-
 src/smt/tactic/smt_tactic.cpp     | 6 ++----
 src/solver/parallel_tactic.cpp    | 2 +-
 src/tactic/arith/pb2bv_tactic.cpp | 2 +-
 src/tactic/tactic.cpp             | 6 +++---
 src/tactic/tactic_exception.h     | 2 +-
 src/tactic/tactical.cpp           | 8 ++++----
 src/util/cmd_context_types.h      | 4 ++--
 src/util/gparams.cpp              | 8 ++++----
 src/util/lp/lp_utils.h            | 4 ++--
 src/util/timeout.cpp              | 6 ++++--
 src/util/z3_exception.cpp         | 3 ---
 src/util/z3_exception.h           | 2 +-
 19 files changed, 36 insertions(+), 40 deletions(-)

diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
index 846fb1ded..e65eb1b32 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -59,7 +59,7 @@ public:
         if (c == nullptr) {
             std::string err_msg("unknown command '");
             err_msg = err_msg + s.bare_str() + "'";
-            throw cmd_exception(err_msg);
+            throw cmd_exception(std::move(err_msg));
         }
         m_cmds.push_back(s);
     }
@@ -384,7 +384,7 @@ class set_option_cmd : public set_get_option_cmd {
             std::string msg = "error setting '";
             msg += opt_name.str();
             msg += "', option value cannot be modified after initialization";
-            throw cmd_exception(msg);
+            throw cmd_exception(std::move(msg));
         }
     }
 
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 0b4c5cd3d..585dd0fa6 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -369,7 +369,7 @@ void stream_ref::set(char const * name) {
             std::string msg = "failed to set output stream '";
             msg += name;
             msg += "'";
-            throw cmd_exception(msg);
+            throw cmd_exception(std::move(msg));
         }
         SASSERT(m_stream);
     }
diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp
index eef95915d..65be3e9ae 100644
--- a/src/muz/fp/horn_tactic.cpp
+++ b/src/muz/fp/horn_tactic.cpp
@@ -211,7 +211,7 @@ class horn_tactic : public tactic {
                 default:
                     msg << "formula is not in Horn fragment: " << mk_pp(g->form(i), m) << "\n";
                     TRACE("horn", tout << msg.str(););
-                    throw tactic_exception(msg.str().c_str());
+                    throw tactic_exception(msg.str());
                 }
             }
 
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index 79ad717c0..403ea4c85 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -909,7 +909,7 @@ namespace smt2 {
                     std::string err_msg = "invalid datatype declaration, unknown sort '";
                     err_msg += missing.str();
                     err_msg += "'";
-                    throw parser_exception(err_msg, line, pos);
+                    throw parser_exception(std::move(err_msg), line, pos);
                 }
                 dts->commit(pm());
                 m_ctx.insert_aux_pdecl(dts.get());
@@ -989,7 +989,7 @@ namespace smt2 {
                 std::string err_msg = "invalid datatype declaration, unknown sort '";
                 err_msg += missing.str();
                 err_msg += "'";
-                throw parser_exception(err_msg, line, pos);
+                throw parser_exception(std::move(err_msg), line, pos);
             }
         }
 
@@ -999,7 +999,7 @@ namespace smt2 {
                 std::string err_msg = "invalid datatype declaration, repeated accessor identifier '";
                 err_msg += duplicated.str();
                 err_msg += "'";
-                throw parser_exception(err_msg, line, pos);
+                throw parser_exception(std::move(err_msg), line, pos);
             }
         }
 
diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp
index 1ae9723c9..695bac07d 100644
--- a/src/qe/nlqsat.cpp
+++ b/src/qe/nlqsat.cpp
@@ -844,8 +844,7 @@ namespace qe {
                 break;
             case l_undef:
                 result.push_back(in.get());
-                std::string s = "search failed";
-                throw tactic_exception(s.c_str()); 
+                throw tactic_exception("search failed");
             }        
         }
 
diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index 68fd56cdf..c87b1c2eb 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -1279,7 +1279,7 @@ namespace qe {
                 if (s == "ok" || s == "unknown") {
                     s = m_fa.s().reason_unknown();
                 }
-                throw tactic_exception(s.c_str()); 
+                throw tactic_exception(std::move(s));
             }        
         }
         
@@ -1344,7 +1344,7 @@ namespace qe {
                     s = m_fa.s().reason_unknown();
                 }
 
-                throw tactic_exception(s.c_str()); 
+                throw tactic_exception(std::move(s));
             }        
             return l_true;
         }
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 5f0fbec16..029ddf924 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -92,7 +92,7 @@ struct goal2sat::imp {
 
     void throw_op_not_handled(std::string const& s) {
         std::string s0 = "operator " + s + " not supported, apply simplifier before invoking translator";
-        throw tactic_exception(s0.c_str());
+        throw tactic_exception(std::move(s0));
     }
     
     void mk_clause(sat::literal l) {
diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp
index cc0f0f207..50fe47985 100644
--- a/src/smt/tactic/smt_tactic.cpp
+++ b/src/smt/tactic/smt_tactic.cpp
@@ -39,7 +39,6 @@ class smt_tactic : public tactic {
     smt_params                   m_params;
     params_ref                   m_params_ref;
     statistics                   m_stats;
-    std::string                  m_failure;
     smt::kernel *                m_ctx;
     symbol                       m_logic;
     progress_callback *          m_callback;
@@ -259,7 +258,7 @@ public:
                 if (m_fail_if_inconclusive && !m_candidate_models) {
                     std::stringstream strm;
                     strm << "smt tactic failed to show goal to be sat/unsat " << m_ctx->last_failure_as_string();
-                    throw tactic_exception(strm.str().c_str());
+                    throw tactic_exception(strm.str());
                 }
                 result.push_back(in.get());
                 if (m_candidate_models) {
@@ -281,8 +280,7 @@ public:
                         break;
                     }
                 }
-                m_failure = m_ctx->last_failure_as_string();
-                throw tactic_exception(m_failure.c_str());
+                throw tactic_exception(m_ctx->last_failure_as_string());
             }
         }
         catch (rewriter_exception & ex) {
diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp
index 451a62064..142ba4bb8 100644
--- a/src/solver/parallel_tactic.cpp
+++ b/src/solver/parallel_tactic.cpp
@@ -635,7 +635,7 @@ private:
             t.join();
         m_manager.limit().reset_cancel();
         if (m_exn_code == -1) 
-            throw default_exception(m_exn_msg);
+            throw default_exception(std::move(m_exn_msg));
         if (m_exn_code != 0) 
             throw z3_error(m_exn_code);            
         if (!m_models.empty()) {
diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp
index 836808de1..f36e3a6db 100644
--- a/src/tactic/arith/pb2bv_tactic.cpp
+++ b/src/tactic/arith/pb2bv_tactic.cpp
@@ -968,7 +968,7 @@ private:
         void throw_tactic(expr* e) {
             std::stringstream strm;
             strm << "goal is in a fragment unsupported by pb2bv. Offending expression: " << mk_pp(e, m);
-            throw tactic_exception(strm.str().c_str());
+            throw tactic_exception(strm.str());
         }
     };
 
diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp
index 4fa9ca43f..3b3c2444f 100644
--- a/src/tactic/tactic.cpp
+++ b/src/tactic/tactic.cpp
@@ -206,7 +206,7 @@ void fail_if_proof_generation(char const * tactic_name, goal_ref const & in) {
     if (in->proofs_enabled()) {
         std::string msg = tactic_name;
         msg += " does not support proof production";
-        throw tactic_exception(msg.c_str());
+        throw tactic_exception(std::move(msg));
     }
 }
 
@@ -214,7 +214,7 @@ void fail_if_unsat_core_generation(char const * tactic_name, goal_ref const & in
     if (in->unsat_core_enabled()) {
         std::string msg = tactic_name;
         msg += " does not support unsat core production";
-        throw tactic_exception(msg.c_str());
+        throw tactic_exception(std::move(msg));
     }
 }
 
@@ -222,6 +222,6 @@ void fail_if_model_generation(char const * tactic_name, goal_ref const & in) {
     if (in->models_enabled()) {
         std::string msg = tactic_name;
         msg += " does not generate models";
-        throw tactic_exception(msg.c_str());
+        throw tactic_exception(std::move(msg));
     }
 }
diff --git a/src/tactic/tactic_exception.h b/src/tactic/tactic_exception.h
index bdf2636a9..0af6d66b1 100644
--- a/src/tactic/tactic_exception.h
+++ b/src/tactic/tactic_exception.h
@@ -26,7 +26,7 @@ class tactic_exception : public z3_exception {
 protected:
     std::string m_msg;
 public:
-    tactic_exception(char const * msg):m_msg(msg) {}
+    tactic_exception(std::string && msg) : m_msg(std::move(msg)) {}
     ~tactic_exception() override {}
     char const * msg() const override { return m_msg.c_str(); }
 };
diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp
index bb04a2be7..43087f50f 100644
--- a/src/tactic/tactical.cpp
+++ b/src/tactic/tactical.cpp
@@ -463,9 +463,9 @@ public:
         if (finished_id == UINT_MAX) {
             switch (ex_kind) {
             case ERROR_EX: throw z3_error(error_code);
-            case TACTIC_EX: throw tactic_exception(ex_msg.c_str());
+            case TACTIC_EX: throw tactic_exception(std::move(ex_msg));
             default:
-                throw default_exception(ex_msg.c_str());
+                throw default_exception(std::move(ex_msg));
             }
         }
     }    
@@ -660,9 +660,9 @@ public:
             if (failed) {
                 switch (ex_kind) {
                 case ERROR_EX: throw z3_error(error_code);
-                case TACTIC_EX: throw tactic_exception(ex_msg.c_str());
+                case TACTIC_EX: throw tactic_exception(std::move(ex_msg));
                 default:
-                    throw default_exception(ex_msg.c_str());
+                    throw default_exception(std::move(ex_msg));
                 }
             }
 
diff --git a/src/util/cmd_context_types.h b/src/util/cmd_context_types.h
index e82536704..564ae6325 100644
--- a/src/util/cmd_context_types.h
+++ b/src/util/cmd_context_types.h
@@ -55,8 +55,8 @@ class cmd_exception : public default_exception {
     }
 public:
     cmd_exception(char const * msg):default_exception(msg), m_line(-1), m_pos(-1) {}
-    cmd_exception(std::string const & msg):default_exception(msg), m_line(-1), m_pos(-1) {}
-    cmd_exception(std::string const & msg, int line, int pos):default_exception(msg), m_line(line), m_pos(pos) {}
+    cmd_exception(std::string && msg):default_exception(std::move(msg)), m_line(-1), m_pos(-1) {}
+    cmd_exception(std::string && msg, int line, int pos):default_exception(std::move(msg)), m_line(line), m_pos(pos) {}
     cmd_exception(char const * msg, symbol const & s): 
         default_exception(compose(msg,s)),m_line(-1),m_pos(-1) {}
     cmd_exception(char const * msg, symbol const & s, int line, int pos): 
diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp
index 5ee49ef16..4ba3b3b5c 100644
--- a/src/util/gparams.cpp
+++ b/src/util/gparams.cpp
@@ -356,7 +356,7 @@ public:
             }
         }
         if (error)
-            throw exception(error_msg);
+            throw exception(std::move(error_msg));
     }
 
     std::string get_value(params_ref const & ps, symbol const & p) {
@@ -417,7 +417,7 @@ public:
             }
         }
         if (error)
-            throw exception(error_msg);
+            throw exception(std::move(error_msg));
         return r;
     }
 
@@ -509,7 +509,7 @@ public:
             }
         }
         if (error)
-            throw exception(error_msg);
+            throw exception(std::move(error_msg));
     }
 
     void display_parameter(std::ostream & out, char const * name) {
@@ -550,7 +550,7 @@ public:
             }
         }
         if (error)
-            throw exception(error_msg);
+            throw exception(std::move(error_msg));
     }
 };
 
diff --git a/src/util/lp/lp_utils.h b/src/util/lp/lp_utils.h
index fce9f4d02..3a5dd2a22 100644
--- a/src/util/lp/lp_utils.h
+++ b/src/util/lp/lp_utils.h
@@ -36,8 +36,8 @@ bool contains(const std::unordered_map<A, B> & map, const A& key) {
 }
 
 namespace lp {
-    inline void throw_exception(const std::string & str) {
-        throw default_exception(str);
+    inline void throw_exception(std::string && str) {
+        throw default_exception(std::move(str));
     }
     typedef z3_exception exception;
 
diff --git a/src/util/timeout.cpp b/src/util/timeout.cpp
index 283b4c206..ad02a747d 100644
--- a/src/util/timeout.cpp
+++ b/src/util/timeout.cpp
@@ -27,9 +27,10 @@ Revision History:
 #include "util/event_handler.h"
 #include "util/scoped_timer.h"
 
-scoped_timer * g_timeout = nullptr;
-void (* g_on_timeout)() = nullptr;
+static scoped_timer * g_timeout = nullptr;
+static void (* g_on_timeout)() = nullptr;
 
+namespace {
 class g_timeout_eh : public event_handler {
 public:
     void operator()(event_handler_caller_t caller_id) override {
@@ -46,6 +47,7 @@ public:
         }
     }
 };
+}
 
 void set_timeout(long ms) {
     if (g_timeout) 
diff --git a/src/util/z3_exception.cpp b/src/util/z3_exception.cpp
index d028a688a..585313024 100644
--- a/src/util/z3_exception.cpp
+++ b/src/util/z3_exception.cpp
@@ -67,9 +67,6 @@ default_exception::default_exception(fmt, char const* msg, ...) {
     m_msg = out.str();
 }
 
-default_exception::default_exception(std::string const & msg): m_msg(msg) {
-}
-
 char const * default_exception::msg() const { 
     return m_msg.c_str(); 
 }
diff --git a/src/util/z3_exception.h b/src/util/z3_exception.h
index e3260e89d..b5c1bf55d 100644
--- a/src/util/z3_exception.h
+++ b/src/util/z3_exception.h
@@ -41,7 +41,7 @@ class default_exception : public z3_exception {
     std::string m_msg;
 public:
     struct fmt {};
-    default_exception(std::string const& msg);
+    default_exception(std::string && msg) : m_msg(std::move(msg)) {}
     default_exception(fmt, char const* msg, ...);
     ~default_exception() override {}
     char const * msg() const override;