Support user-defined operators in SMTChecker #14534

pgebal · 2023-09-05T09:21:41Z

User-defined operators are handled like function calls.

pgebal · 2023-09-11T09:58:34Z

.../libsolidity/smtCheckerTests/operators/userDefined/user_defined_division_same_as_builtin.sol

 }

 contract C {
    function f(U x, U y) public pure returns (U) {
-        return x / y; // FIXME: should detect div by zero
+        return x / y; // FIXME: are we ok that div by zero not reported here?


There is a potential problem that errors are not reported where the operator is used, but in the implementation.
In this example division by zero is reported in line 5 but not here.
I could live with that, but maybe we want the error to be reported here as well?

Oh, it makes perfect sense to report it in the implementation. I guess that's consistent with what would happen for a div(x, y) function that does division. So I think this is fine and probably even expected.

I agree. The implementation of the user-defined operator can be arbitrary code, so it makes sense to pinpoint the exact problem in the operator implementation.

pgebal · 2023-09-11T10:00:22Z

...heckerTests/operators/userDefined/user_defined_operator_matches_equivalent_function_call.sol

    }

    function testArithmetic(I16 x, I16 y) public pure {
-        assert(x + y == add(x, y)); // FIXME: should hold
+        assert(x + y == add(x, y)); // should hold


CHC reports Assertion violation *might* happen here.
I don't know why. Maybe it's because there are possible overlows/underflows/division by zero in implementation?

It affects only integer arithmetic operators. Bitwise and boolean are ok.

When I don't use operators and just apply appropriate function calls on both sides of the relation I also get those warnings.

edit:
On current develop branch, if I turn the assert statement into for example:
assert(eq(add(x, y), add(x, y))) it also yields Assertion violation *might* happen here. warnings.

@blishko Do you know what this^ might happen?

*might* happen just means that the solver was not able to solve the query within the given timeout/resource limit.
At least I think it is only in this case. This does not mean that there is necessarily something wrong here, just that the solver is not able to deal with the query efficiently. We can try to solve it with increased timeout, see if that helps.

blishko

Looks pretty good! I agree that treating the user-defined operators as function calls is the right approach. I just have a few questions.

libsolidity/formal/SMTEncoder.h

libsolidity/formal/CHC.cpp

libsolidity/formal/CHC.h

libsolidity/formal/CHC.cpp

blishko

Left some more comments based on my recent reflections.

blishko · 2023-10-04T07:18:19Z

libsolidity/formal/BMC.cpp

+void BMC::inlineFunctionCall(
+	FunctionDefinition const* _funDef,
+	Expression const& _callStackExpr,
+	Expression const* _calledExpr,


It looks to me like we are not consistent about what _calledExpr represents.
In case of Operations, you pass the pointer to the whole operation expression, e.g. a + b.
But in case of a function call, e.g., f(a,b), this is only the pointer to the expression representing the name of the function, i.e, f.

Yea there is a mix up here:

pushCallStack and defineExpr inside createReturnedExpression should be called on the FunctionCall object for the normal function call case, and indeed for the expression in case if user-defined operator call (e.g. a + b).

_funType->hasBoundFirstArgument() can only be true for normal function calls (I assume, we should check in solidity-dev), so in symbolicArguments we do need the FunctionCall::expression() object (of type Expression) for the function call case, but not for the user-defined case

Please correct me if I'm wrong, but I think now the arguments provided to BMC::inlineFuncitonCall are correct.

blishko · 2023-10-04T07:19:43Z

libsolidity/formal/BMC.cpp

+	Expression const* calledExpr = &_funCall.expression();
+	auto funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
+	std::vector<ASTPointer<Expression const>> arguments = _funCall.sortedArguments();
+
+	inlineFunctionCall(funDef, _funCall, calledExpr, funType, arguments);


Here we extract only the name of the function to calledExpr from the whole function call expression, see my comment above about difference in what calledExpr represents.

yes I agree, the callstack object needs to be the one of type FunctionCall* in case of an actual function call

@leonardoalt, to make sure, the current code is ok in that regard?
Maybe I should leave a clarifying comment in the code?

@leonardoalt , I am still confused about "callstack object". This should be the expression that represents the function call in the caller?

For me the confusing bit here is the calledExpr. In the case of an actual function call, this will be the expression representing the name of the function (because it is FunctionCall::expression).
Why would we refer to the expressions of the function name as calledExpr? It is not the expression that represents the function call, only the name of the function.

blishko · 2023-10-04T07:38:38Z

libsolidity/formal/SMTEncoder.cpp

+	if (_funType->hasBoundFirstArgument())
 	{
-		calledExpr = innermostTuple(*calledExpr);
-		auto const& attachedFunction = dynamic_cast<MemberAccess const*>(calledExpr);
+		_calledExpr = innermostTuple(*_calledExpr);
+		auto const& attachedFunction = dynamic_cast<MemberAccess const*>(_calledExpr);
 		solAssert(attachedFunction, "");
 		args.push_back(expr(attachedFunction->expression(), functionParams.front()->type()));
 		firstParam = 1;
 	}


The more I am looking at this, the more I would like to refactor this method somehow to split the treatment of the extra argument in the special case of MemberAccess and the conversion of actual arguments to SMT expressions.

One way that comes to my mind is to check for this optional extra argument beforehand and pass here just std::optional<smtutil::Expression>. Then instead of _funDef, _calledExpr, _funType, this method would only need the formal parameters (what we now get from _funDef->parameters()).

libsolidity/ast/AST.h

...solidity/smtCheckerTests/operators/userDefined/user_defined_operations_on_constants_fail.sol

leonardoalt · 2023-10-05T09:05:06Z

libsolidity/formal/BMC.cpp

+	Expression const* calledExpr = &_funCall.expression();
+	auto funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
+	std::vector<ASTPointer<Expression const>> arguments = _funCall.sortedArguments();
+
+	inlineFunctionCall(funDef, _funCall, calledExpr, funType, arguments);


yes I agree, the callstack object needs to be the one of type FunctionCall* in case of an actual function call

leonardoalt · 2023-10-05T09:11:43Z

libsolidity/formal/BMC.cpp

+void BMC::inlineFunctionCall(
+	FunctionDefinition const* _funDef,
+	Expression const& _callStackExpr,
+	Expression const* _calledExpr,


Yea there is a mix up here:

pushCallStack and defineExpr inside createReturnedExpression should be called on the FunctionCall object for the normal function call case, and indeed for the expression in case if user-defined operator call (e.g. a + b).

_funType->hasBoundFirstArgument() can only be true for normal function calls (I assume, we should check in solidity-dev), so in symbolicArguments we do need the FunctionCall::expression() object (of type Expression) for the function call case, but not for the user-defined case

blishko

This looks good from my side!

leonardoalt · 2023-10-18T10:05:02Z

libsolidity/formal/SMTEncoder.cpp

 	unsigned firstParam = 0;
-	if (funType->hasBoundFirstArgument())
+	if (_calledExpr)


This looks a bit misleading. It must run only for bound calls, but it's called _calledExpr. Are we sure it only runs in such case? Looking into the caller code I think this is the case, but we should confirm. In any case, I think this variable should be renamed to show more explicitly that it's about bound function calls.

Right. I corrected that by renaming it to boundArgumentCall.
I've checked it in the code, that this is an optional with value only for functions in which funType->hasBoundFirstArgument() is true.

leonardoalt · 2023-10-18T10:06:49Z

libsolidity/formal/CHC.cpp

+			m_callGraph[m_currentContract].insert(funDef);
+	}
+
+	Expression const* calledExpr = &_funCall.expression();


The calledExpr here has the meaning that I imagined at first during the previous review, but in BMC it means bound functions. We should clarify this

leonardoalt · 2023-10-18T10:07:34Z

libsolidity/formal/CHC.cpp

-	if (!usesStaticCall(_funCall))
+
+	std::optional<Expression const*> calledExpr =
+		_funType->hasBoundFirstArgument() ? std::make_optional(_calledExpr) : std::nullopt;


here it has the same behavior as BMC

leonardoalt

lgtm, please squash

blishko

LGTM!

pgebal marked this pull request as draft September 5, 2023 09:22

pgebal force-pushed the pgebal/operators branch 3 times, most recently from 3a5a4df to bb37a3e Compare September 8, 2023 08:39

pgebal changed the title ~~Pgebal/operators~~ Support user-defined operators in SMT checker Sep 8, 2023

pgebal changed the title ~~Support user-defined operators in SMT checker~~ Support user-defined operators in SMTChecker Sep 8, 2023

pgebal force-pushed the pgebal/operators branch from bb37a3e to 23a346e Compare September 11, 2023 08:50

pgebal commented Sep 11, 2023

View reviewed changes

pgebal force-pushed the pgebal/operators branch from 23a346e to 27969b4 Compare September 11, 2023 10:02

ethereum deleted a comment Sep 21, 2023

pgebal force-pushed the pgebal/operators branch 2 times, most recently from 439c4e1 to 3a8b65c Compare September 26, 2023 09:00

pgebal marked this pull request as ready for review September 26, 2023 09:00

pgebal requested a review from leonardoalt September 28, 2023 17:13

pgebal force-pushed the pgebal/operators branch 3 times, most recently from 772ecc0 to b68f8f8 Compare September 29, 2023 16:14

blishko reviewed Sep 30, 2023

View reviewed changes

pgebal force-pushed the pgebal/operators branch from 51d0dc6 to 6a9a0a4 Compare October 3, 2023 10:15

blishko reviewed Oct 4, 2023

View reviewed changes

leonardoalt reviewed Oct 5, 2023

View reviewed changes

pgebal force-pushed the pgebal/operators branch 3 times, most recently from b7e11f2 to 71eb81f Compare October 12, 2023 08:36

pgebal requested review from blishko and leonardoalt October 12, 2023 08:37

blishko previously approved these changes Oct 12, 2023

View reviewed changes

pgebal force-pushed the pgebal/operators branch from 71eb81f to 00bf98e Compare October 13, 2023 15:32

leonardoalt reviewed Oct 18, 2023

View reviewed changes

pgebal dismissed blishko’s stale review via 5e9c27a October 19, 2023 14:26

pgebal force-pushed the pgebal/operators branch from 5e9c27a to ba88e25 Compare October 19, 2023 14:42

leonardoalt reviewed Oct 19, 2023

View reviewed changes

pgebal force-pushed the pgebal/operators branch from 67956f8 to 5fe9d5d Compare October 20, 2023 15:44

pgebal added 4 commits October 20, 2023 17:45

Support user defined operators in SMT

78eb37d

apply CR changes

13c2d62

refactor: rename calledExpr to boundArgumentCall

353dbdd

fix test error

da7c00e

pgebal force-pushed the pgebal/operators branch from 5fe9d5d to da7c00e Compare October 20, 2023 15:45

pgebal requested review from leonardoalt and blishko October 20, 2023 16:17

leonardoalt approved these changes Oct 21, 2023

View reviewed changes

blishko approved these changes Oct 21, 2023

View reviewed changes

leonardoalt merged commit b187d06 into ethereum:develop Oct 22, 2023
1 check passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Support user-defined operators in SMTChecker #14534

Support user-defined operators in SMTChecker #14534

pgebal commented Sep 5, 2023 •

edited

Loading

pgebal Sep 11, 2023

cameel Sep 28, 2023

blishko Sep 28, 2023

pgebal Sep 11, 2023 •

edited

Loading

pgebal Sep 18, 2023 •

edited

Loading

blishko Sep 18, 2023

blishko left a comment

blishko left a comment

blishko Oct 4, 2023

leonardoalt Oct 5, 2023

pgebal Oct 12, 2023

blishko Oct 4, 2023

leonardoalt Oct 5, 2023

pgebal Oct 5, 2023 •

edited

Loading

blishko Oct 5, 2023

blishko Oct 4, 2023

pgebal Oct 12, 2023

leonardoalt Oct 5, 2023

leonardoalt Oct 5, 2023

blishko left a comment

leonardoalt Oct 18, 2023

pgebal Oct 19, 2023

leonardoalt Oct 18, 2023

leonardoalt Oct 18, 2023

leonardoalt left a comment

blishko left a comment

Support user-defined operators in SMTChecker #14534

Support user-defined operators in SMTChecker #14534

Conversation

pgebal commented Sep 5, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

pgebal Sep 11, 2023 • edited Loading

Choose a reason for hiding this comment

pgebal Sep 18, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

blishko left a comment

Choose a reason for hiding this comment

blishko 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

pgebal Oct 5, 2023 • edited Loading

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

blishko 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

leonardoalt left a comment

Choose a reason for hiding this comment

blishko left a comment

Choose a reason for hiding this comment

pgebal commented Sep 5, 2023 •

edited

Loading

pgebal Sep 11, 2023 •

edited

Loading

pgebal Sep 18, 2023 •

edited

Loading

pgebal Oct 5, 2023 •

edited

Loading