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

Throw when trying to read past the end of SMTLib stream

Browse Source
This commit is contained in:
Martin Blicha 2023-08-12 19:12:33 +02:00
parent d3bbc51ee9
commit 8e0e2cb1ae
3 changed files with 26 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
libsmtutil/CHCSmtLib2Interface.cpp
View File

@ -675,10 +675,19 @@ CHCSolverInterface::CexGraph CHCSmtLib2Interface::graphFromZ3Proof(std::string c
if (parser.isEOF()) // No proof from Z3 if (parser.isEOF()) // No proof from Z3
return {}; return {};
// For some reason Z3 outputs everything as a single s-expression // For some reason Z3 outputs everything as a single s-expression
auto all = parser.parseExpression(); SMTLib2Expression parsedOutput;
try
{
parsedOutput = parser.parseExpression();
}
catch (SMTLib2Parser::ParsingException&)
{
// TODO: What should we do in this case?
smtAssert(false, "SMTLIb2Parser: Error parsing input");
}
solAssert(parser.isEOF()); solAssert(parser.isEOF());
solAssert(!isAtom(all)); solAssert(!isAtom(parsedOutput));
auto& commands = std::get<SMTLib2Expression::args_t>(all.data); auto& commands = asSubExpressions(parsedOutput);
SMTLibTranslationContext context(*m_smtlib2); SMTLibTranslationContext context(*m_smtlib2);
for (auto& command: commands) for (auto& command: commands)
{ {
@ -720,10 +729,17 @@ smtutil::Expression CHCSmtLib2Interface::invariantsFromSMTLib(std::string const&
if (parser.isEOF()) // No model if (parser.isEOF()) // No model
return Expression(true); return Expression(true);
// For some reason Z3 outputs everything as a single s-expression // For some reason Z3 outputs everything as a single s-expression
auto all = parser.parseExpression(); SMTLib2Expression parsedOutput;
try {
parsedOutput = parser.parseExpression();
} catch(SMTLib2Parser::ParsingException&)
{
// TODO: What should we do in this case?
smtAssert(false, "SMTLIb2Parser: Error parsing input");
}
solAssert(parser.isEOF()); solAssert(parser.isEOF());
solAssert(!isAtom(all)); solAssert(!isAtom(parsedOutput));
auto& commands = std::get<SMTLib2Expression::args_t>(all.data); auto& commands = asSubExpressions(parsedOutput);
std::vector<Expression> definitions; std::vector<Expression> definitions;
for (auto& command: commands) for (auto& command: commands)
{ {

2
libsmtutil/SMTLibParser.cpp
View File

@ -65,6 +65,8 @@ std::string SMTLib2Parser::parseToken() {
} }
void SMTLib2Parser::advance() { void SMTLib2Parser::advance() {
if (!m_input.good())
throw ParsingException{};
m_token = static_cast<char>(m_input.get()); m_token = static_cast<char>(m_input.get());
if (token() == ';') if (token() == ';')
while (token() != '\n' && token() != 0) while (token() != '\n' && token() != 0)

2
libsmtutil/SMTLibParser.h
View File

@ -60,6 +60,8 @@ inline auto& asSubExpressions(SMTLib2Expression& expr)
class SMTLib2Parser { class SMTLib2Parser {
public: public:
class ParsingException {};
SMTLib2Parser(std::istream& _input) : SMTLib2Parser(std::istream& _input) :
m_input(_input), m_input(_input),
m_token(static_cast<char>(m_input.get())) {} m_token(static_cast<char>(m_input.get())) {}