From b8f89fa45d44be7fa6bd5fa848f1de0891468120 Mon Sep 17 00:00:00 2001
From: Martin Blicha <martin.blicha@gmail.com>
Date: Wed, 9 Aug 2023 12:08:29 +0200
Subject: [PATCH] SMTSolverCommand: Use pipe instead of temporary file for the
 query

---
 libsolidity/interface/SMTSolverCommand.cpp | 30 ++++++++++------------
 1 file changed, 14 insertions(+), 16 deletions(-)

diff --git a/libsolidity/interface/SMTSolverCommand.cpp b/libsolidity/interface/SMTSolverCommand.cpp
index 436702c7c..7602bd729 100644
--- a/libsolidity/interface/SMTSolverCommand.cpp
+++ b/libsolidity/interface/SMTSolverCommand.cpp
@@ -22,12 +22,9 @@
 #include <libsolutil/CommonIO.h>
 #include <libsolutil/Exceptions.h>
 #include <libsolutil/Keccak256.h>
-#include <libsolutil/TemporaryDirectory.h>
 
 #include <boost/algorithm/string/join.hpp>
 #include <boost/algorithm/string/predicate.hpp>
-#include <boost/filesystem.hpp>
-#include <boost/filesystem/fstream.hpp>
 #include <boost/process.hpp>
 
 using solidity::langutil::InternalCompilerError;
@@ -47,35 +44,36 @@ ReadCallback::Result SMTSolverCommand::solve(std::string const& _kind, std::stri
 		if (kind != ReadCallback::kindString(ReadCallback::Kind::SMTQuery))
 			solAssert(false, "SMTQuery callback used as callback kind " + kind);
 
-		auto tempDir = solidity::util::TemporaryDirectory("smt");
-		util::h256 queryHash = util::keccak256(_query);
-		auto queryFileName = tempDir.path() / ("query_" + queryHash.hex() + ".smt2");
-
-		auto queryFile = boost::filesystem::ofstream(queryFileName);
-
-		queryFile << _query << std::flush;
-
 		std::vector<std::string> commandArgs;
 		boost::split(commandArgs, solverCommand, boost::is_any_of(" "));
 		solAssert(commandArgs.size() > 0, "SMT command was empty");
-		auto const& solverBinary = commandArgs[0];
+		auto solverBinary = commandArgs[0];
 		auto pathToBinary = boost::process::search_path(solverBinary);
 
 		if (pathToBinary.empty())
 			return ReadCallback::Result{false, solverBinary + " binary not found."};
 
 		commandArgs.erase(commandArgs.begin());
-		commandArgs.push_back(queryFileName.string());
-		boost::process::ipstream pipe;
+
+		if (solverBinary == "z3")
+			commandArgs.insert(commandArgs.begin(), "-in");
+
+		boost::process::opstream in;  // input to subprocess written to by main process
+		boost::process::ipstream out; // output from subprocess read by main process
 		boost::process::child solver(
 			pathToBinary,
 			boost::process::args(commandArgs),
-			boost::process::std_out > pipe
+			boost::process::std_out > out,
+			boost::process::std_in < in
 		);
 
+		in << _query << std::flush;
+		in.pipe().close();
+		in.close();
+
 		std::vector<std::string> data;
 		std::string line;
-		while (solver.running() && std::getline(pipe, line))
+		while (solver.running() && std::getline(out, line))
 			if (!line.empty())
 				data.push_back(line);