SMTChecker: Parse invariants from SMT-LIB response #15032

blishko · 2024-04-16T12:38:08Z

This PR adds initial support for parsing invariants, computed by CHC solver, in SMT-LIB format.

This is done in a few separate steps (found in individual commits):

Introduction of a basic SMT-LIB parser that parses string representation and creates S-expression representation. This parser was originally developed by @chriseth (for solsmt) and we only updated it slightly to handle malformed SMT-LIB strings.
Instructing Eldarica to produce model (invariants) when this is requested by the user.
Reorganization of where we remember declared SMT-LIB sorts. This is necessary for proper parsing of the solver response and creation of our representation of the invariants.
The actual translation from SMT-LIB S-expressions to our Expression representation of the invariants.

Note: This is only initial support and will require more iterations as we add more tests.

blishko · 2024-04-16T13:11:41Z

libsmtutil/CHCSmtLib2Interface.cpp

+	};
+
+
+#define precondition(CONDITION) if(!(CONDITION)) return {}


Is there a better for to achieve this?
If I don't what to explicitly write 10 if checks like this

if (!<condition>) return {};

Yet, I want to check these conditions, but only bail out on further processing, not throwing an exception.
It feels like there currently isn't a better way than a macro.

nikola-matic

These are (almost) exclusively stylistic - unfortunately I can't seem to help much with the actual SMT stuff :)

nikola-matic · 2024-04-16T20:13:30Z

libsmtutil/CHCSmtLib2Interface.cpp

+		CHCSmtLib2Interface const& m_chcInterface;
+		std::map<std::string, SortPointer> knownVariables;
+
+		bool isNumber(std::string const& _expr)


Is this supposed to handle only positive numbers?

Good question. It turns out yes, because in SMT-LIB, unary minus is an operator, so negative number should be represented as (- <number>).

I'll try invariant with a negative number, to check this case.

libsmtutil/CHCSmtLib2Interface.cpp

nikola-matic · 2024-04-17T12:26:59Z

libsmtutil/CHCSmtLib2Interface.cpp

+						else if (isNumber(_atom))
+							return smtutil::Expression(_atom, {}, SortProvider::sintSort);
+						else if (knownVariables.find(_atom) != knownVariables.end())
+							return smtutil::Expression(_atom, {}, knownVariables.at(_atom));


Suggested change

return smtutil::Expression(_atom, {}, knownVariables.at(_atom));

return smtutil::Expression(_atom, {}, knownVariables[_atom]);

nikola-matic · 2024-04-17T12:28:50Z

libsmtutil/CHCSmtLib2Interface.cpp

+			std::vector<std::pair<std::string, SortPointer>> boundVariables;
+			for (auto const& sortedVar: varList)
+			{
+				solAssert(!isAtom(sortedVar));


Just curious - why do you sometimes use smtAssert(), and other times solAssert()?

I don't know :)
I've changed everything to smtAssert.

libsmtutil/CHCSmtLib2Interface.cpp

nikola-matic · 2024-04-17T12:33:40Z

libsmtutil/SMTLib2Interface.cpp

-	switch (_sort.kind)
+	if (!m_sortNames.count(_sort))
+		m_sortNames[_sort] = toSmtLibSortInternal(_sort);
+	return m_sortNames.at(_sort);


Suggested change

return m_sortNames.at(_sort);

return m_sortNames.at[_sort];

What is it about at that you don't like?

at() throws an exception if the element is not present in the container, but you already check for that in the if above, so it's just unnecessary overhead.

Well, for map operator [] default-initializes a new value and insert the new pair into the map, if the key was not present. So I think it has even more overhead than at.

Sure, but not in this case, because you've already checked for the existence of the element. It's not a big deal regardless, so no need to make this change.

libsmtutil/CHCSmtLib2Interface.cpp

nikola-matic · 2024-04-17T12:40:32Z

The failing tests have been fixed by the way, you just need to rebase.

libsmtutil/CHCSmtLib2Interface.cpp

libsmtutil/SMTLib2Parser.cpp

libsmtutil/SMTLib2Interface.cpp

libsmtutil/SMTLib2Interface.h

libsmtutil/SMTLib2Interface.cpp

libsmtutil/CHCSmtLib2Interface.cpp

blishko · 2024-04-25T08:48:03Z

@nikola-matic , @pgebal , I fixed the code according to your suggestions, or at least commented on your comments :)
So, this should be ready for another round.

pgebal · 2024-04-29T20:38:51Z

@nikola-matic , @pgebal , I fixed the code according to your suggestions, or at least commented on your comments :) So, this should be ready for another round.

@blishko the code looks good to me

libsmtutil/CHCSmtLib2Interface.cpp

nikola-matic · 2024-04-30T11:56:48Z

libsmtutil/CHCSmtLib2Interface.cpp

+								if (typeArgs.size() == 4 && typeArgs[0].toString() == "_")
+								{
+									if (typeArgs[1].toString() == "extract")
+									{
+										return smtutil::Expression(
+											"extract",
+											{toSMTUtilExpression(typeArgs[2]), toSMTUtilExpression(typeArgs[3])},
+											SortProvider::bitVectorSort // TODO: Compute bit size properly?
+										);
+									}
+								}


Suggested change

if (typeArgs.size() == 4 && typeArgs[0].toString() == "_")

{

if (typeArgs[1].toString() == "extract")

{

return smtutil::Expression(

"extract",

{toSMTUtilExpression(typeArgs[2]), toSMTUtilExpression(typeArgs[3])},

SortProvider::bitVectorSort // TODO: Compute bit size properly?

);

}

}

if (typeArgs.size() == 4 && typeArgs[0].toString() == "_" && typeArgs[1].toString() == "extract")

return smtutil::Expression(

"extract",

{toSMTUtilExpression(typeArgs[2]), toSMTUtilExpression(typeArgs[3])},

SortProvider::bitVectorSort // TODO: Compute bit size properly?

);

nikola-matic

Eh, there are a few tiny style issues (mostly around overuse of scoping braces with conditional statements), but it's our fault for not having a sane formatting check, so merge away :)

nikola-matic · 2024-04-30T11:59:05Z

libsmtutil/CHCSmtLib2Interface.cpp

@@ -223,3 +226,282 @@ std::string CHCSmtLib2Interface::createHeaderAndDeclarations() {
 std::string CHCSmtLib2Interface::createQueryAssertion(std::string name) {
 	return "(assert\n(forall " + forall() + "\n" + "(=> " + name + " false)))";
 }
+
+class SMTLibTranslationContext


Uh, everything in the class has an extra indent by the way.

@chriseth

Parser code was originally written by @chriseth for solsmt, an SMT solver developed internally for Solidity

We add support for parsing CHC solver response containing a model, i.e., invariants. We utilise our SMT parser to build S-expression representation which we then interpret using the context we remembered while building the query. We have to rememeber all predicates declared to the solver, and, consequently, all sorts we have declared to the solver.

blishko force-pushed the smt-eld-invariants branch from 921240a to e2fb54d Compare April 16, 2024 12:42

blishko commented Apr 16, 2024

View reviewed changes

blishko force-pushed the smt-eld-invariants branch 2 times, most recently from b7b26b5 to e98f8ed Compare April 16, 2024 13:18

ethereum deleted a comment from stackenbotten Apr 16, 2024

blishko marked this pull request as ready for review April 16, 2024 13:29

nikola-matic reviewed Apr 17, 2024

View reviewed changes

pgebal requested changes Apr 21, 2024

View reviewed changes

blishko force-pushed the smt-eld-invariants branch 2 times, most recently from 4866974 to 5df3915 Compare April 23, 2024 15:34

nikola-matic reviewed Apr 23, 2024

View reviewed changes

libsmtutil/CHCSmtLib2Interface.cpp Outdated Show resolved Hide resolved

libsmtutil/CHCSmtLib2Interface.cpp Outdated Show resolved Hide resolved

pgebal reviewed Apr 24, 2024

View reviewed changes

libsmtutil/CHCSmtLib2Interface.cpp Outdated Show resolved Hide resolved

blishko force-pushed the smt-eld-invariants branch from 5df3915 to 271bb4f Compare April 25, 2024 08:36

cameel added the smt label Apr 26, 2024

pgebal previously approved these changes Apr 29, 2024

View reviewed changes

nikola-matic reviewed Apr 30, 2024

View reviewed changes

libsmtutil/CHCSmtLib2Interface.cpp Outdated Show resolved Hide resolved

nikola-matic reviewed Apr 30, 2024

View reviewed changes

libsmtutil/CHCSmtLib2Interface.cpp Outdated Show resolved Hide resolved

nikola-matic reviewed Apr 30, 2024

View reviewed changes

nikola-matic previously approved these changes Apr 30, 2024

View reviewed changes

nikola-matic reviewed Apr 30, 2024

View reviewed changes

blishko added 5 commits April 30, 2024 15:10

SMTChecker: First version of SMTLIB2 parser

7fb6222

Parser code was originally written by @chriseth for solsmt, an SMT solver developed internally for Solidity

SMTChecker: Instruct Eldarica to produce invariants if requested

eb11819

SMTChecker: Remember sorts already in SMTLibInterface

1fcaec5

SMTChecker: Add command-line test for invariants from Eldarica

048ce0b

blishko dismissed stale reviews from nikola-matic and pgebal via 048ce0b April 30, 2024 13:27

blishko force-pushed the smt-eld-invariants branch from 271bb4f to 048ce0b Compare April 30, 2024 13:27

nikola-matic approved these changes Apr 30, 2024

View reviewed changes

blishko merged commit 5afa25e into develop Apr 30, 2024
72 checks passed

blishko deleted the smt-eld-invariants branch April 30, 2024 14:31

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

SMTChecker: Parse invariants from SMT-LIB response #15032

SMTChecker: Parse invariants from SMT-LIB response #15032

blishko commented Apr 16, 2024

blishko Apr 16, 2024 •

edited

nikola-matic left a comment

nikola-matic Apr 16, 2024

blishko Apr 23, 2024

nikola-matic Apr 17, 2024

nikola-matic Apr 17, 2024

blishko Apr 23, 2024

nikola-matic Apr 17, 2024

blishko Apr 25, 2024

nikola-matic Apr 30, 2024

blishko Apr 30, 2024

nikola-matic Apr 30, 2024

nikola-matic commented Apr 17, 2024

blishko commented Apr 25, 2024

pgebal commented Apr 29, 2024

nikola-matic Apr 30, 2024

nikola-matic left a comment

nikola-matic Apr 30, 2024

		};


		#define precondition(CONDITION) if(!(CONDITION)) return {}

	return smtutil::Expression(_atom, {}, knownVariables.at(_atom));
	return smtutil::Expression(_atom, {}, knownVariables[_atom]);

SMTChecker: Parse invariants from SMT-LIB response #15032

SMTChecker: Parse invariants from SMT-LIB response #15032

Conversation

blishko commented Apr 16, 2024

blishko Apr 16, 2024 • edited

Choose a reason for hiding this comment

nikola-matic left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nikola-matic commented Apr 17, 2024

blishko commented Apr 25, 2024

pgebal commented Apr 29, 2024

Choose a reason for hiding this comment

nikola-matic left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

blishko Apr 16, 2024 •

edited