[SMTChecker] Report contract invariants #11451

leonardoalt · 2021-05-28T17:44:35Z

Spacer already gives invariants for every predicate when the result of a query is unsat, that's the interpretation of each predicate.
If we take those expressions for our interface_* and nondet_interface_* predicates, we have respectively, contract invariants (over a state) and reentrancy properties (over a transition).
So what we do here is

collect the z3::expr that represents the invariants (a big conjunction)
translate that into smtutil::Expression
collect the contract invariants above
format them in an almost-Solidity way

Open questions:

How do we report the found invariants? Imo it doesn't make sense to report them as warnings. For the JSON output, we can have a new object, but what about CLI?
Should we report only contract invariants or the reentrancy invariants too? The latter has not obvious semantics, so maybe requires a different output, separated from the contract invariants.

TODO:

Docs
CLI tests
Organize the code a bit better
Format ABI functions better [SMTChecker] Contract invariants - format abi functions better #11463
Handle exists inside forall properly, with a stack of substitution maps and shadowing (this is just a note to self) [SMTChecker] Contract invariants - support nested quantifiers #11462

Future:
The expressions can of course be simplified to transform things like a * (- 1) into -a among others, but that should go into a different PR.

test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2.sol

mijovic · 2021-06-09T09:01:42Z

I checked most of the tests and they are looking good.
Open question is how to report invariants in CLI interface. Do we have any open issue about additional way of reporting things from compiler? I think I saw discussion about having notice instead of warning, but can't find it now...

I am reviewing implementation now

leonardoalt · 2021-06-09T09:04:19Z

We only briefly talked in the chat, should talk about that in the design call today.

mijovic

Only first small comments.
I am doing another turn now

libsolidity/formal/Invariants.cpp

libsmtutil/CHCSolverInterface.h

leonardoalt · 2021-09-28T22:15:58Z

Test blockchain_state/balance_receive_calls.sol has (:var 1) terms which should be taken care of.

leonardoalt · 2021-10-05T14:04:58Z

This is now ready for review

test/cmdlineTests/model_checker_invariants_reentrancy/input.sol

libsmtutil/SolverInterface.h

libsmtutil/CHCSmtLib2Interface.cpp

libsmtutil/CHCSmtLib2Interface.h

libsmtutil/SolverInterface.h

test/libsolidity/smtCheckerTests/array_members/length_1d_copy_2d_storage_to_memory.sol

test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_1.sol

test/libsolidity/smtCheckerTests/array_members/length_function_call.sol

hrkrshnn · 2021-10-07T09:17:54Z

test/cmdlineTests/model_checker_invariants_contract_reentrancy/err

+(x <= 0)
+Reentrancy property(ies) for model_checker_invariants_contract_reentrancy/input.sol:test:
+(!(x <= 0) || (x' <= 0))
+((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))


What's errorCode?

Yea maybe we need to either change that or explain it a bit more. Every verification target (assertion, out of bounds, etc) gets a unique non-zero errorCode starting at one. So if errorCode = 0, all good. If errorCode > 0, something failed, but we're not saying here exactly what failed. Do you have a suggestion for how to handle it?

Actually what does !(errorCode >= 3) mean here? The failure is one of the three {assertion, out of bounds, ...}.

Maybe it would be nice to print a table of error codes. It would be even better if we can change !(<errorCode> >= 3) to just a list of possibilities.

No, the number is not per target type, it's per query, basically.

I think it would be better to leave it is as for the moment, and try to explain what it means, and adjust it later. I don't have a clear answer about what's best for this now, so I'd prefer not to stall this PR and do it after.

Hmm maybe listing all targets if errorCode is present is not too hard to do

Or this @hrkrshnn

docs/smtchecker.rst

libsmtutil/Z3Interface.cpp

libsolidity/formal/CHC.cpp

hrkrshnn · 2021-10-13T09:40:11Z

libsolidity/formal/ExpressionFormatter.cpp

+		return type;
+
+	return _args.at(0) + "." + type;
+}


I'm going to assume this function is correct :)

I can argue for its correctness in a call if you want, but yea, I think it's also not too bad if it's buggy, since this is non essential extra information.

libsolidity/formal/ExpressionFormatter.cpp

solc/CommandLineParser.cpp

hrkrshnn · 2021-10-13T09:59:59Z

test/cmdlineTests/model_checker_invariants_contract_reentrancy/err

+(x <= 0)
+Reentrancy property(ies) for model_checker_invariants_contract_reentrancy/input.sol:test:
+(!(x <= 0) || (x' <= 0))
+((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))


Actually what does !(errorCode >= 3) mean here? The failure is one of the three {assertion, out of bounds, ...}.

Maybe it would be nice to print a table of error codes. It would be even better if we can change !(<errorCode> >= 3) to just a list of possibilities.

hrkrshnn · 2021-10-13T10:01:31Z

test/libsolidity/SMTCheckerTest.cpp

+
+	if (m_ignoreInv)
+		ranges::actions::remove_if(m_errorList, [](auto&& _error) {
+			return _error.errorId && _error.errorId->error != 1180;


Isn't it possible to avoid creating this in the first place?

Yea, probably better.

test/cmdlineTests/model_checker_invariants_all/err

leonardoalt · 2021-10-13T17:37:46Z

@hrkrshnn I fixed the latest comments in new commits, will fixup those in the proper original commits when the PR is approved.

cameel

I haven't reviewed all of it yet but so far I haven't found anything important. Just minor stuff.

libsmtutil/SolverInterface.h

libsmtutil/Z3Interface.cpp

cameel · 2021-10-18T12:51:29Z

libsmtutil/Z3Interface.cpp

 	else if (kind == Z3_OP_INT2BV)
-		smtAssert(false, "");
+		return Expression::int2bv(arguments[0], _expr.get_sort().bv_size());
 	else if (kind == Z3_OP_BV2INT)
-		smtAssert(false, "");
+		// TODO manually wrap the result with a check whether the number
+		// is positive or negative somehow.
+		return Expression::bv2int(arguments[0]);
+	else if (kind == Z3_OP_EXTRACT)
+		return Expression("extract", {arguments[0]. arguments[1]}, arguments[0].sort);


What about the number of arguments here? Can there be more than 1 or 2? I think we need asserts against that.

And for Z3_OP_EXTRACT, do sorts have to be the same?

Good point. Extract is actually quite complex since it creates a new function for bitvectors of different sizes, so I'm just gonna do the same as dt_accessor and use all arguments with that operator's name. We can give it some interpretation if we ever handle it properly on the way from z3 to our representation.

ok. What about Z3_OP_BV2INT and Z3_OP_INT2BV though?

libsmtutil/Z3Interface.cpp

test/cmdlineTests/standard_model_checker_invariants_wrong_type_2/input.json

hrkrshnn

Looks good. We agreed that this can be more or less merged and the additional changes can be done in follow up PR. Probably missing fixups.

leonardoalt · 2021-10-19T19:50:22Z

Fixed @cameel 's comments and fixedup the fixup commits into the original ones.

Agreed on a call with @hrkrshnn to report locations the same as warnings in a different PR.

cameel · 2021-10-19T20:21:38Z

Unfortunately I did not manage to finish the review today but so far I did not find anything that would look like an actual problem so if @hrkrshnn approves then I guess it should be fine to merge it.

…a Solidity-like expression string

…the given predicates

leonardoalt · 2021-10-26T09:30:46Z

@hrkrshnn merge merge?

axic reviewed May 28, 2021

View reviewed changes

test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2.sol Outdated Show resolved Hide resolved

leonardoalt force-pushed the smt_report_invariants branch 2 times, most recently from a0c8df3 to 360d86a Compare May 31, 2021 18:28

This was referenced May 31, 2021

[SMTChecker] Contract invariants - support nested quantifiers #11462

Open

[SMTChecker] Contract invariants - format abi functions better #11463

Open

[SMTChecker] Contract invariants - simplify expressions #11464

Open

mijovic reviewed Jun 9, 2021

View reviewed changes

leonardoalt force-pushed the smt_report_invariants branch from 360d86a to 2b0f519 Compare July 15, 2021 11:20

leonardoalt mentioned this pull request Sep 6, 2021

Add notice severity to "error messages" #11508

Closed

leonardoalt force-pushed the smt_report_invariants branch from 2b0f519 to 7570c3c Compare September 27, 2021 18:33

leonardoalt force-pushed the smt_report_invariants branch 2 times, most recently from e67ed7a to 8f1645b Compare October 4, 2021 18:22

leonardoalt marked this pull request as ready for review October 5, 2021 13:48

leonardoalt force-pushed the smt_report_invariants branch from 8f1645b to e2588a5 Compare October 5, 2021 13:48

leonardoalt force-pushed the smt_report_invariants branch 2 times, most recently from 4a653bf to 41838a7 Compare October 6, 2021 12:07

hrkrshnn reviewed Oct 7, 2021

View reviewed changes

leonardoalt force-pushed the smt_report_invariants branch from 41838a7 to e55b71d Compare October 7, 2021 11:37

hrkrshnn reviewed Oct 13, 2021

View reviewed changes

leonardoalt force-pushed the smt_report_invariants branch 2 times, most recently from 4399bcb to b72aabf Compare October 13, 2021 14:51

leonardoalt commented Oct 13, 2021

View reviewed changes

test/cmdlineTests/model_checker_invariants_all/err Outdated Show resolved Hide resolved

leonardoalt force-pushed the smt_report_invariants branch from 830576f to 428bab6 Compare October 13, 2021 17:37

cameel reviewed Oct 18, 2021

View reviewed changes

hrkrshnn previously approved these changes Oct 19, 2021

View reviewed changes

leonardoalt dismissed hrkrshnn’s stale review via f193e76 October 19, 2021 19:49

leonardoalt force-pushed the smt_report_invariants branch from 428bab6 to f193e76 Compare October 19, 2021 19:49

leonardoalt force-pushed the smt_report_invariants branch from f193e76 to ac8bf8c Compare October 21, 2021 19:00

Leo Alt added 17 commits October 26, 2021 11:30

Add new info functions

fa48abf

Add invariant to the solver results

9a87680

Adjust Z3Interface::fromZ3 for the extra cases

1d65977

Add ExpressionFormatter which translates an smtutil::Expression into …

ce72d7c

…a Solidity-like expression string

Add expression substitution to Predicate

9bcd2c1

Add Invariants which traverses the proof and collects invariants for …

d554824

…the given predicates

Add invariants to ModelCheckerSettings

bc90533

Use invariants in CHC

49e7627

Add errorCode list to invariants report

d419c30

Add invariants option to CLI and JSON

3118fb3

Add SMTCheckerTest isoltest option to ignore invariants

37215ff

Adjust errors script to also look for infos

a104443

Adjust ModelCheckerSettings in tools tests

2cbd496

SMTChecker tests

38b0cf7

CLI and JSON tests

4f823c6

Docs

d04ad57

Changelog

902a2e2

leonardoalt force-pushed the smt_report_invariants branch from ac8bf8c to 902a2e2 Compare October 26, 2021 09:31

hrkrshnn approved these changes Oct 26, 2021

View reviewed changes

hrkrshnn merged commit 401dd43 into develop Oct 26, 2021

hrkrshnn deleted the smt_report_invariants branch October 26, 2021 10:41

[SMTChecker] Report contract invariants #11451

[SMTChecker] Report contract invariants #11451

Uh oh!

Conversation

leonardoalt commented May 28, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

mijovic commented Jun 9, 2021

Uh oh!

leonardoalt commented Jun 9, 2021

Uh oh!

mijovic left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

leonardoalt commented Sep 28, 2021

Uh oh!

leonardoalt commented Oct 5, 2021

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

leonardoalt Oct 7, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

leonardoalt commented Oct 13, 2021

Uh oh!

cameel left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

leonardoalt commented May 28, 2021 •

edited

Loading

leonardoalt Oct 7, 2021 •

edited

Loading

hrkrshnn left a comment •

edited

Loading

cameel commented Oct 19, 2021 •

edited

Loading