From 3ae2c455dbb6ac95834fd23082688b11784dfcae Mon Sep 17 00:00:00 2001
From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Date: Tue, 19 Oct 2021 20:11:53 -0500
Subject: [PATCH] Avoid escaping `double-quotes` twice. (#7409)

With -o raw-benchmark, The command:

(echo """")
was printed as

(echo """""""")
because we run the quote-escaping procedure twice on it. This PR fixes the issue by ensuring that we only run it once.
---
 src/parser/smt2/Smt2.g            |  2 +-
 src/printer/smt2/smt2_printer.cpp | 21 ++++-----------------
 src/smt/command.cpp               | 17 +++++------------
 src/util/smt2_quote_string.cpp    | 12 ++++++++++++
 src/util/smt2_quote_string.h      |  5 +++++
 5 files changed, 27 insertions(+), 30 deletions(-)

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index bff4f72ab..a75aa36da 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -793,7 +793,7 @@ smt25Command[std::unique_ptr<cvc5::Command>* cmd]
 
     /* echo */
   | ECHO_TOK
-    ( simpleSymbolicExpr[s]
+    ( str[s, true]
       { cmd->reset(new EchoCommand(s)); }
     | { cmd->reset(new EchoCommand()); }
     )
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 32b195be2..1da2a3c7b 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1723,15 +1723,7 @@ void Smt2Printer::toStreamCmdEmpty(std::ostream& out,
 void Smt2Printer::toStreamCmdEcho(std::ostream& out,
                                   const std::string& output) const
 {
-  std::string s = output;
-  // escape all double-quotes
-  size_t pos = 0;
-  while ((pos = s.find('"', pos)) != string::npos)
-  {
-    s.replace(pos, 1, "\"\"");
-    pos += 2;
-  }
-  out << "(echo \"" << s << "\")" << std::endl;
+  out << "(echo " << cvc5::quoteString(output) << ')' << std::endl;
 }
 
 /*
@@ -1930,14 +1922,9 @@ static void toStream(std::ostream& out, const CommandUnsupported* s, Variant v)
 #endif /* CVC5_COMPETITION_MODE */
 }
 
-static void errorToStream(std::ostream& out, std::string message, Variant v) {
-  // escape all double-quotes
-  size_t pos = 0;
-  while((pos = message.find('"', pos)) != string::npos) {
-    message.replace(pos, 1, "\"\"");
-    pos += 2;
-  }
-  out << "(error \"" << message << "\")" << endl;
+static void errorToStream(std::ostream& out, std::string message, Variant v)
+{
+  out << "(error " << cvc5::quoteString(message) << ')' << endl;
 }
 
 static void toStream(std::ostream& out, const CommandFailure* s, Variant v) {
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 311d6713a..e8ee6d59c 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -38,6 +38,7 @@
 #include "proof/unsat_core.h"
 #include "smt/dump.h"
 #include "smt/model.h"
+#include "util/smt2_quote_string.h"
 #include "util/unsafe_interrupt_exception.h"
 #include "util/utility.h"
 
@@ -302,19 +303,10 @@ void EmptyCommand::toStream(std::ostream& out,
 /* class EchoCommand                                                          */
 /* -------------------------------------------------------------------------- */
 
-EchoCommand::EchoCommand(std::string output)
-{
-  // escape all double-quotes
-  size_t pos = 0;
-  while ((pos = output.find('"', pos)) != string::npos)
-  {
-    output.replace(pos, 1, "\"\"");
-    pos += 2;
-  }
-  d_output = '"' + output + '"';
-}
+EchoCommand::EchoCommand(std::string output) : d_output(output) {}
 
 std::string EchoCommand::getOutput() const { return d_output; }
+
 void EchoCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   /* we don't have an output stream here, nothing to do */
@@ -325,7 +317,7 @@ void EchoCommand::invoke(api::Solver* solver,
                          SymbolManager* sm,
                          std::ostream& out)
 {
-  out << d_output << std::endl;
+  out << cvc5::quoteString(d_output) << std::endl;
   Trace("dtview::command") << "* ~COMMAND: echo |" << d_output << "|~"
                            << std::endl;
   d_commandStatus = CommandSuccess::instance();
@@ -335,6 +327,7 @@ void EchoCommand::invoke(api::Solver* solver,
 }
 
 Command* EchoCommand::clone() const { return new EchoCommand(d_output); }
+
 std::string EchoCommand::getCommandName() const { return "echo"; }
 
 void EchoCommand::toStream(std::ostream& out,
diff --git a/src/util/smt2_quote_string.cpp b/src/util/smt2_quote_string.cpp
index 82750c48b..e2ab4a74c 100644
--- a/src/util/smt2_quote_string.cpp
+++ b/src/util/smt2_quote_string.cpp
@@ -42,4 +42,16 @@ std::string quoteSymbol(const std::string& s){
   return s;
 }
 
+std::string quoteString(const std::string& s) {
+  // escape all double-quotes
+  std::string output = s;
+  size_t pos = 0;
+  while ((pos = output.find('"', pos)) != std::string::npos)
+  {
+    output.replace(pos, 1, "\"\"");
+    pos += 2;
+  }
+  return '"' + output + '"';
+}
+
 }  // namespace cvc5
diff --git a/src/util/smt2_quote_string.h b/src/util/smt2_quote_string.h
index 98b2f89dd..f8be53c0c 100644
--- a/src/util/smt2_quote_string.h
+++ b/src/util/smt2_quote_string.h
@@ -27,6 +27,11 @@ namespace cvc5 {
  */
 std::string quoteSymbol(const std::string& s);
 
+/**
+ * SMT-LIB 2 quoting for strings
+ */
+std::string quoteString(const std::string& s);
+
 }  // namespace cvc5
 
 #endif /* CVC5__UTIL__SMT2_QUOTE_STRING_H */
-- 
2.30.2