From b918f121ef93b61346583be7a1b896fca1bbdd0f Mon Sep 17 00:00:00 2001
From: Luca Bruno <lucab@debian.org>
Date: Tue, 23 Mar 2021 18:25:59 +0000
Subject: [PATCH] zstring: fix encode rountrip for '\' as printable ASCII
 (#5120)

This fixes encode roundtripping for all printable ASCII characters.
In particular, this now leaves a plain '\' untouched by the
encoding logic, instead of converting it to escaped hex-digits.
It also adds unit testing covering this specific zstring encoding
property, in order to avoid future regressions.
---
 src/test/CMakeLists.txt |  1 +
 src/test/main.cpp       |  1 +
 src/test/zstring.cpp    | 25 +++++++++++++++++++++++++
 src/util/zstring.cpp    |  2 +-
 4 files changed, 28 insertions(+), 1 deletion(-)
 create mode 100644 src/test/zstring.cpp

diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt
index 816d1a848..eb0e94173 100644
--- a/src/test/CMakeLists.txt
+++ b/src/test/CMakeLists.txt
@@ -129,6 +129,7 @@ add_executable(test-z3
   vector.cpp
   lp/lp.cpp
   lp/nla_solver_test.cpp
+  zstring.cpp
   ${z3_test_extra_object_files}
 )
 z3_add_install_tactic_rule(${z3_test_deps})
diff --git a/src/test/main.cpp b/src/test/main.cpp
index cf7ae8acc..3e3f1d575 100644
--- a/src/test/main.cpp
+++ b/src/test/main.cpp
@@ -215,6 +215,7 @@ int main(int argc, char ** argv) {
     TST(prime_generator);
     TST(permutation);
     TST(nlsat);
+    TST(zstring);
     if (test_all) return 0;
     TST(ext_numeral);
     TST(interval);
diff --git a/src/test/zstring.cpp b/src/test/zstring.cpp
new file mode 100644
index 000000000..ffeda7fce
--- /dev/null
+++ b/src/test/zstring.cpp
@@ -0,0 +1,25 @@
+#include "util/debug.h"
+#include "util/trace.h"
+#include "util/zstring.h"
+
+// Encode and check for roundtrip all printable ASCII characters.
+static void tst_ascii_roundtrip() {
+    unsigned ascii_min = 0x20; // ' '
+    unsigned ascii_max = 0x7E; // '~'
+
+    for (unsigned i = ascii_min; i <= ascii_max; i++) {
+        zstring input(i);
+        std::string expected(1, i);
+        bool roundtrip_ok = input.encode() == expected;
+
+        if (!roundtrip_ok) {
+            std::cout << "Failed to roundtrip printable ASCII char: " << expected
+                      << "\n" << std::flush;
+            ENSURE(roundtrip_ok);
+        }
+    }
+}
+
+void tst_zstring() {
+    tst_ascii_roundtrip();
+}
diff --git a/src/util/zstring.cpp b/src/util/zstring.cpp
index af0400de0..8508b9790 100644
--- a/src/util/zstring.cpp
+++ b/src/util/zstring.cpp
@@ -146,7 +146,7 @@ std::string zstring::encode() const {
 #define _flush() if (offset > 0) { buffer[offset] = 0; strm << buffer; offset = 0; }
     for (unsigned i = 0; i < m_buffer.size(); ++i) {
         unsigned ch = m_buffer[i];
-        if (ch < 32 || ch >= 128 || ch == '\\') {
+        if (ch < 32 || ch >= 128) {
             _flush();
             strm << "\\u{" << std::hex << ch << std::dec << "}";
         }