[SMTChecker] Support to integer and Bool storage vars #3947

leonardoalt · 2018-04-19T12:44:06Z

The encoding isn't very different from local variables. In the beginning of every function the state vars are reset, meaning that their SSA index is increased and the new var is set to unknown.

Maybe we need more tests, not sure.

Added Changelog entry under 23 for now, will rebase later on.

leonardoalt · 2018-04-19T12:46:57Z

libsolidity/formal/SMTChecker.cpp

 	m_interface->reset();
 	m_variables.clear();
+	m_variables.insert(m_stateVariables.begin(), m_stateVariables.end());


m_variables is mostly used in a way that works for both local and state vars, that's why I decided to have only one map (instead of this one and another m_stateVariables) and add the state vars to m_variables in the beginning of a function visit

I think this can still be refactored a little better, for example having only a single map where the entries know when they have to be reset and how, but we can merge it like that for now.

leonardoalt · 2018-04-19T12:54:29Z

libsolidity/formal/SMTChecker.cpp

@@ -607,7 +615,8 @@ void SMTChecker::checkCondition(
 			message << " for:\n";
 			solAssert(values.size() == expressionNames.size(), "");
 			for (size_t i = 0; i < values.size(); ++i)
-				message << "  " << expressionNames.at(i) << " = " << values.at(i) << "\n";
+				if (expressionsToEvaluate.at(i).name != values.at(i))
+					message << "  " << expressionNames.at(i) << " = " << values.at(i) << "\n";


This if had to be added so that state variables that are not touched by a function don't appear in a counterexample, since they don't have a model. In that case, the solver returns the name of the SMT variable itself as the model. Right now this happens only for Bool. The reason is that when we set a Bool var to unknown, no constraint is added to the solver, therefore if the function doesn't do anything with this state var, it's just not there. Since integers have constraints for the unknown case, integer state variables will have a model even if they're not used.

So, we should choose one out of the following 3 cases for how counterexamples are shown:

As it is in this PR: unused state integer vars get a model, Bools don't.

Unused Bool state vars should have a model too. This case is probably simple to create, we just have to add the trivial constraint (or var (not var)) in the unknown case.

No unused state vars should have models. This is more complicated and would require changes in the class VariableUsage or something similar

I think it's fine this way.

chriseth · 2018-04-30T13:33:58Z

libsolidity/formal/SMTChecker.cpp

@@ -62,6 +62,8 @@ void SMTChecker::endVisit(VariableDeclaration const& _varDecl)
 {
 	if (_varDecl.isLocalVariable() && _varDecl.type()->isValueType() &&_varDecl.value())
 		assignment(_varDecl, *_varDecl.value(), _varDecl.location());
+	else if (_varDecl.isStateVariable() && _varDecl.type()->isValueType())


This probably fails if variables are declared below functions. I think we have to manually register them.

True.. I read somewhere that state vars were visited before functions, but you're right.

chriseth · 2018-04-30T13:34:38Z

libsolidity/formal/SMTChecker.cpp

@@ -62,6 +62,8 @@ void SMTChecker::endVisit(VariableDeclaration const& _varDecl)
 {
 	if (_varDecl.isLocalVariable() && _varDecl.type()->isValueType() &&_varDecl.value())


Hm, I think this was always wrong with variables like var (a, b) = f().

chriseth · 2018-04-30T13:35:43Z

libsolidity/formal/SMTChecker.cpp

 	m_pathConditions.clear();
 	m_conditionalExecutionHappened = false;
 	initializeLocalVariables(_function);
+	resetStateVariables();


Above, we call m_interface->reset(), so is this really necessary?

It's necessary to re-add the range constraints coming from types

chriseth · 2018-04-30T13:39:29Z

libsolidity/formal/SMTChecker.cpp

+		else
+		{
+			solAssert(_varDecl.isStateVariable(), "");
+			m_stateVariables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface));


Why do we have this distinction in the first place? If we do not add the state variables to m_variables, they are not taken into account when unifying branches.

The distinction is because state vars are visited before functions, so we keep a single copy while visiting all the functions, and add them to m_variables in the beginning of each function

So, the thing about state vars being visited before functions: has to be done manually

chriseth

m_variables do not include m_stateVariables. Because of that, a test for if(b) { a = 200; } assert(a == 200); should be incorrect if a is a state variable and b is an input.

leonardoalt · 2018-04-30T13:53:23Z

m_stateVariables is included in m_variables when a function is visited, with the resets:
m_variables.insert(m_stateVariables.begin(), m_stateVariables.end());

chriseth · 2018-05-15T12:16:40Z

libsolidity/formal/VariableUsage.cpp

@@ -33,7 +33,6 @@ VariableUsage::VariableUsage(ASTNode const& _node)
 			solAssert(declaration, "");
 			if (VariableDeclaration const* varDecl = dynamic_cast<VariableDeclaration const*>(declaration))
 				if (
-					varDecl->isLocalVariable() &&
 					identifier->annotation().lValueRequested &&


This might not work correctly for tuple assignments, I created an issue for that: #4141

True, I wanted to check that after a similar comment from you

chriseth · 2018-05-15T12:18:29Z

libsolidity/formal/SMTChecker.cpp

@@ -58,6 +58,19 @@ void SMTChecker::analyze(SourceUnit const& _source)
 		_source.accept(*this);
 }

+bool SMTChecker::visit(ContractDefinition const& _contract)
+{
+	for (auto _var : _contract.stateVariables())


This does not include inherited state variables, so we have to be careful once we add inheritance.

chriseth · 2018-05-15T12:28:19Z

Rebased and adjusted changelog entry.

leonardoalt commented Apr 19, 2018

View reviewed changes

chriseth reviewed Apr 30, 2018

View reviewed changes

chriseth suggested changes Apr 30, 2018

View reviewed changes

leonardoalt force-pushed the smt_storage branch from ea3625d to 60b9083 Compare April 30, 2018 14:33

leonardoalt changed the title ~~[SMTChecker] Support to integer and Bool storage vars~~ [DO NOT MERGE][SMTChecker] Support to integer and Bool storage vars May 2, 2018

leonardoalt force-pushed the smt_storage branch from 60b9083 to f185322 Compare May 2, 2018 13:53

leonardoalt changed the title ~~[DO NOT MERGE][SMTChecker] Support to integer and Bool storage vars~~ [SMTChecker] Support to integer and Bool storage vars May 2, 2018

chriseth reviewed May 15, 2018

View reviewed changes

[SMTChecker] Support to integer and Bool storage vars

2dbb35d

chriseth previously approved these changes May 15, 2018

View reviewed changes

chriseth dismissed their stale review via 3cd5d56 May 15, 2018 12:25

chriseth force-pushed the smt_storage branch from f185322 to 3cd5d56 Compare May 15, 2018 12:25

chriseth previously approved these changes May 15, 2018

View reviewed changes

Leonardo Alt added 2 commits May 15, 2018 14:28

[SMTChecker] Declaring all state vars before any function is visited

4117e85

Testing state vars that are declared after functions that use them

a0b4210

chriseth dismissed their stale review via a0b4210 May 15, 2018 12:28

chriseth force-pushed the smt_storage branch from 3cd5d56 to a0b4210 Compare May 15, 2018 12:28

chriseth approved these changes May 15, 2018

View reviewed changes

chriseth merged commit 63861aa into develop May 15, 2018

axic deleted the smt_storage branch June 11, 2018 11:05

		@@ -62,6 +62,8 @@ void SMTChecker::endVisit(VariableDeclaration const& _varDecl)
		{
		if (_varDecl.isLocalVariable() && _varDecl.type()->isValueType() &&_varDecl.value())

[SMTChecker] Support to integer and Bool storage vars #3947

[SMTChecker] Support to integer and Bool storage vars #3947

Uh oh!

Conversation

leonardoalt commented Apr 19, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

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!

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!

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!

chriseth left a comment

Choose a reason for hiding this comment

Uh oh!

leonardoalt commented Apr 30, 2018

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!

chriseth commented May 15, 2018

Uh oh!

Uh oh!

leonardoalt commented Apr 19, 2018 •

edited

Loading