cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Enable resource limit for Z3

Browse Source
This commit is contained in:
Martin Blicha 2023-06-27 11:49:20 +02:00
parent c6f274892e
commit d9dc8f475e
3 changed files with 9 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsmtutil/CHCSmtLib2Interface.cpp
View File

@ -189,7 +189,7 @@ std::string CHCSmtLib2Interface::querySolver(std::string const& _input)
if (m_enabledSolvers.eld) if (m_enabledSolvers.eld)
return "eld"; return "eld";
if (m_enabledSolvers.z3) if (m_enabledSolvers.z3)
return "z3"; return "z3 rlimit=1000000";
return ""; return "";
}(); }();
auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery) + " " + solverBinary, _input); auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery) + " " + solverBinary, _input);

2
libsmtutil/SMTLib2Interface.cpp
View File

@ -163,7 +163,7 @@ std::pair<CheckResult, std::vector<std::string>> SMTLib2Interface::check(std::ve
std::vector<std::string> solverCommands; std::vector<std::string> solverCommands;
if (m_enabledSolvers.z3) if (m_enabledSolvers.z3)
solverCommands.emplace_back("z3"); solverCommands.emplace_back("z3 rlimit=1000000");
if (m_enabledSolvers.cvc4) if (m_enabledSolvers.cvc4)
solverCommands.emplace_back("cvc4"); solverCommands.emplace_back("cvc4");

9
libsolidity/interface/SMTSolverCommand.cpp
View File

@ -55,16 +55,21 @@ ReadCallback::Result SMTSolverCommand::solve(std::string const& _kind, std::stri
queryFile << _query; queryFile << _query;
std::string solverBinary = solverCommand.substr(0, solverCommand.find(' ')); 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 pathToBinary = boost::process::search_path(solverBinary); auto pathToBinary = boost::process::search_path(solverBinary);
if (pathToBinary.empty()) if (pathToBinary.empty())
return ReadCallback::Result{false, solverBinary + " binary not found."}; return ReadCallback::Result{false, solverBinary + " binary not found."};
commandArgs.erase(commandArgs.begin());
commandArgs.push_back(queryFileName.string());
boost::process::ipstream pipe; boost::process::ipstream pipe;
boost::process::child solver( boost::process::child solver(
pathToBinary, pathToBinary,
queryFileName, boost::process::args(commandArgs),
boost::process::std_out > pipe boost::process::std_out > pipe
); );