From 465a4b285c903a3237cbab9837e70e0f9d723195 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Basile=20Cl=C3=A9ment?=
 <129742207+bclement-ocp@users.noreply.github.com>
Date: Fri, 7 Feb 2025 10:08:04 +0100
Subject: [PATCH] Escape quotes when printing SMT-LIB error messages (#1289)

* Escape quotes when printing SMT-LIB error messages
---
 src/bin/common/solving_loop.ml                |  6 +++---
 src/lib/util/printer.ml                       | 19 ++++++++++++++++++-
 src/lib/util/printer.mli                      |  3 +++
 .../testfile-get-assignment1.err.expected     |  2 +-
 .../testfile-get-assignment2.err.expected     |  2 +-
 tests/smtlib/testfile-get-info2.err.expected  |  2 +-
 6 files changed, 27 insertions(+), 7 deletions(-)

diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml
index 0cbe38b99..bb752d681 100644
--- a/src/bin/common/solving_loop.ml
+++ b/src/bin/common/solving_loop.ml
@@ -832,11 +832,11 @@ let process_source ?selector_inst ~print_status src =
       | {contents = `Exit; _} -> raise Exit
 
       | {contents = `Echo str; _} ->
-        let new_str = String.concat "\"\"" (String.split_on_char '"' str) in
         Fmt.pf
           (Options.Output.get_fmt_regular ())
-          "\"%s\"@."
-          new_str;
+          "%a@."
+          Printer.pp_smtlib_string
+          str;
         st
 
       | {contents = `Get_info kind; _ } ->
diff --git a/src/lib/util/printer.ml b/src/lib/util/printer.ml
index f56edd190..54930b777 100644
--- a/src/lib/util/printer.ml
+++ b/src/lib/util/printer.ml
@@ -375,6 +375,23 @@ let print_status_timeout ?(validity_mode=true) loc
     ("Timeout","unknown","fg_orange") loc
     time steps goal
 
+(* Version of [kfprintf] that escapes its input. *)
+let ekfprintf k ppf fmt =
+  let buf = Buffer.create 1024 in
+  let buf_ppf = Format.formatter_of_buffer buf in
+  Format.kfprintf (fun buf_ppf ->
+      Format.pp_print_flush buf_ppf ();
+      let s =
+        String.concat "\"\"" (String.split_on_char '"' (Buffer.contents buf))
+      in
+      Format.pp_print_string ppf s;
+      k ppf
+    ) buf_ppf fmt
+
+let pp_smtlib_string ppf s =
+  Format.fprintf ppf "\"";
+  ekfprintf (fun ppf -> Format.fprintf ppf "\"") ppf "%s" s
+
 let print_smtlib_err ?(flushed=true) s =
   (* The smtlib error messages are printed on the regular output. *)
   pp_std_smt ();
@@ -386,7 +403,7 @@ let print_smtlib_err ?(flushed=true) s =
       Format.fprintf fmt "\")"
   in
   Format.fprintf fmt "(error \"";
-  Format.kfprintf k fmt s
+  ekfprintf k fmt s
 
 let pp_source ppf src =
   let name = Logs.Src.doc src in
diff --git a/src/lib/util/printer.mli b/src/lib/util/printer.mli
index f1b9e625a..08460be51 100644
--- a/src/lib/util/printer.mli
+++ b/src/lib/util/printer.mli
@@ -161,6 +161,9 @@ val print_status_inconsistent :
   int option ->
   string option -> unit
 
+(** Print an SMT-LIB string with quotes and escaping. *)
+val pp_smtlib_string : Format.formatter -> string -> unit
+
 (** Print smtlib error message on the regular formatter, accessible with
     {!val:Options.get_fmt_regular} and set by default to stdout.
     The regular formatter is flushed after the print if flushed is set. *)
diff --git a/tests/smtlib/testfile-get-assignment1.err.expected b/tests/smtlib/testfile-get-assignment1.err.expected
index 40cd8b144..9b6e62fc4 100644
--- a/tests/smtlib/testfile-get-assignment1.err.expected
+++ b/tests/smtlib/testfile-get-assignment1.err.expected
@@ -1,2 +1,2 @@
 (error "../tests/smtlib/testfile-get-assignment1.err.smt2:3.0:
-        No model produced, cannot execute get-assignment.")
+No model produced, cannot execute get-assignment.")
diff --git a/tests/smtlib/testfile-get-assignment2.err.expected b/tests/smtlib/testfile-get-assignment2.err.expected
index c4623ee7a..3e89f97f0 100644
--- a/tests/smtlib/testfile-get-assignment2.err.expected
+++ b/tests/smtlib/testfile-get-assignment2.err.expected
@@ -4,4 +4,4 @@ unknown
   (define-fun x () Int 0)
 )
 (error "../tests/smtlib/testfile-get-assignment2.err.smt2:8.0:
-        Produce assignments disabled; add (set-option :produce-assignments true)")
+Produce assignments disabled; add (set-option :produce-assignments true)")
diff --git a/tests/smtlib/testfile-get-info2.err.expected b/tests/smtlib/testfile-get-info2.err.expected
index 5f43e2dca..ebc7d5c20 100644
--- a/tests/smtlib/testfile-get-info2.err.expected
+++ b/tests/smtlib/testfile-get-info2.err.expected
@@ -1,2 +1,2 @@
 (error "../tests/smtlib/testfile-get-info2.err.smt2:7.0:
-        Invalid (get-info :reason-unknown)")
+Invalid (get-info :reason-unknown)")