From 26e5faa038d09fe04a3aad7b384d3433324a9380 Mon Sep 17 00:00:00 2001
From: chriseth <c@ethdev.com>
Date: Wed, 13 Jul 2016 11:16:00 +0200
Subject: Handle external effects.
---
libsolidity/formal/Why3Translator.cpp | 200 ++++++++++++++++++++++++++--------
libsolidity/formal/Why3Translator.h | 17 ++-
2 files changed, 169 insertions(+), 48 deletions(-)
diff --git a/libsolidity/formal/Why3Translator.cpp b/libsolidity/formal/Why3Translator.cpp
index c794cb24..bd0a020d 100644
--- a/libsolidity/formal/Why3Translator.cpp
+++ b/libsolidity/formal/Why3Translator.cpp
@@ -67,23 +67,11 @@ void Why3Translator::fatalError(ASTNode const& _node, string const& _description
BOOST_THROW_EXCEPTION(FatalError());
}
-void Why3Translator::appendPreface()
-{
- m_lines.push_back(Line{R"(
-module UInt256
- use import mach.int.Unsigned
- type uint256
- constant max_uint256: int = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
- clone export mach.int.Unsigned with
- type t = uint256,
- constant max = max_uint256
-end
-)", 0});
-}
-
string Why3Translator::toFormalType(Type const& _type) const
{
- if (auto type = dynamic_cast<IntegerType const*>(&_type))
+ if (_type.category() == Type::Category::Bool)
+ return "bool";
+ else if (auto type = dynamic_cast<IntegerType const*>(&_type))
{
if (!type->isAddress() && !type->isSigned() && type->numBits() == 256)
return "uint256";
@@ -129,6 +117,7 @@ bool Why3Translator::visit(ContractDefinition const& _contract)
if (m_seenContract)
error(_contract, "More than one contract not supported.");
m_seenContract = true;
+ m_currentContract.contract = &_contract;
if (_contract.isLibrary())
error(_contract, "Libraries not supported.");
@@ -141,21 +130,41 @@ bool Why3Translator::visit(ContractDefinition const& _contract)
addLine("use import int.ComputerDivision");
addLine("use import mach.int.Unsigned");
addLine("use import UInt256");
- addLine("exception Ret");
+ addLine("exception Revert");
+ addLine("exception Return");
- addLine("type state = {");
- indent();
- m_stateVariables = _contract.stateVariables();
- for (VariableDeclaration const* variable: m_stateVariables)
+ if (_contract.stateVariables().empty())
+ addLine("type state = ()");
+ else
{
- string varType = toFormalType(*variable->annotation().type);
- if (varType.empty())
- fatalError(*variable, "Type not supported.");
- addLine("mutable _" + variable->name() + ": ref " + varType);
+ addLine("type state = {");
+ indent();
+ m_currentContract.stateVariables = _contract.stateVariables();
+ for (VariableDeclaration const* variable: m_currentContract.stateVariables)
+ {
+ string varType = toFormalType(*variable->annotation().type);
+ if (varType.empty())
+ fatalError(*variable, "Type not supported for state variable.");
+ addLine("mutable _" + variable->name() + ": " + varType);
+ }
+ unindent();
+ addLine("}");
}
+
+ addLine("type account = {");
+ indent();
+ addLine("mutable balance: uint256;");
+ addLine("storage: state");
unindent();
addLine("}");
+ addLine("val external_call (this: account): bool");
+ indent();
+ addLine("ensures { result = false -> this = (old this) }");
+ addLine("writes { this }");
+ addSourceFromDocStrings(m_currentContract.contract->annotation());
+ unindent();
+
if (!_contract.baseContracts().empty())
error(*_contract.baseContracts().front(), "Inheritance not supported.");
if (!_contract.definedStructs().empty())
@@ -172,10 +181,9 @@ bool Why3Translator::visit(ContractDefinition const& _contract)
return false;
}
-void Why3Translator::endVisit(ContractDefinition const& _contract)
+void Why3Translator::endVisit(ContractDefinition const&)
{
- m_stateVariables.clear();
- addSourceFromDocStrings(_contract.annotation());
+ m_currentContract.reset();
unindent();
addLine("end");
}
@@ -207,7 +215,7 @@ bool Why3Translator::visit(FunctionDefinition const& _function)
m_localVariables[var->name()] = var;
add("let rec _" + _function.name());
- add(" (state: state)");
+ add(" (this: account)");
for (auto const& param: _function.parameters())
{
string paramType = toFormalType(*param->annotation().type);
@@ -235,9 +243,20 @@ bool Why3Translator::visit(FunctionDefinition const& _function)
unindent();
addSourceFromDocStrings(_function.annotation());
+ if (!m_currentContract.contract)
+ error(_function, "Only functions inside contracts allowed.");
+ addSourceFromDocStrings(m_currentContract.contract->annotation());
+
+ if (_function.isDeclaredConst())
+ addLine("ensures { (old this) = this }");
+ else
+ addLine("writes { this }");
addLine("=");
+ // store the prestate in the case we need to revert
+ addLine("let prestate = {balance = this.balance; storage = " + copyOfStorage() + "} in ");
+
// initialise local variables
for (auto const& variable: _function.parameters())
addLine("let _" + variable->name() + " = ref arg_" + variable->name() + " in");
@@ -259,7 +278,7 @@ bool Why3Translator::visit(FunctionDefinition const& _function)
_function.body().accept(*this);
add(";");
- addLine("raise Ret");
+ addLine("raise Return");
string retVals;
for (auto const& variable: _function.returnParameters())
@@ -268,8 +287,14 @@ bool Why3Translator::visit(FunctionDefinition const& _function)
retVals += ", ";
retVals += "!_" + variable->name();
}
- addLine("with Ret -> (" + retVals + ")");
- newLine();
+ addLine("with Return -> (" + retVals + ") |");
+ string reversion = " Revert -> this.balance <- prestate.balance; ";
+ for (auto const* variable: m_currentContract.stateVariables)
+ reversion += "this.storage._" + variable->name() + " <- prestate.storage._" + variable->name() + "; ";
+ //@TODO in case of reversion the return values are wrong - we need to change the
+ // return type to include a bool to signify if an exception was thrown.
+ reversion += "(" + retVals + ")";
+ addLine(reversion);
unindent();
addLine("end");
addLine("");
@@ -349,10 +374,17 @@ bool Why3Translator::visit(Return const& _node)
}
add("begin _" + params.front()->name() + " := ");
_node.expression()->accept(*this);
- add("; raise Ret end");
+ add("; raise Return end");
}
else
- add("raise Ret");
+ add("raise Return");
+ return false;
+}
+
+bool Why3Translator::visit(Throw const& _node)
+{
+ addSourceFromDocStrings(_node.annotation());
+ add("raise Revert");
return false;
}
@@ -385,7 +417,8 @@ bool Why3Translator::visit(Assignment const& _node)
error(_node, "Compound assignment not supported.");
_node.leftHandSide().accept(*this);
- add(" := ");
+
+ add(m_currentLValueIsRef ? " := " : " <- ");
_node.rightHandSide().accept(*this);
return false;
@@ -402,7 +435,7 @@ bool Why3Translator::visit(TupleExpression const& _node)
bool Why3Translator::visit(UnaryOperation const& _unaryOperation)
{
if (toFormalType(*_unaryOperation.annotation().type).empty())
- error(_unaryOperation, "Type not supported.");
+ error(_unaryOperation, "Type not supported in unary operation.");
switch (_unaryOperation.getOperator())
{
@@ -512,6 +545,42 @@ bool Why3Translator::visit(FunctionCall const& _node)
add(")");
return false;
}
+ case FunctionType::Location::Bare:
+ {
+ if (!_node.arguments().empty())
+ {
+ error(_node, "Function calls with named arguments not supported.");
+ return true;
+ }
+
+ add("(");
+ indent();
+ add("let amount = 0 in ");
+ _node.expression().accept(*this);
+ addLine("if amount <= this.balance then");
+ indent();
+ addLine("let balance_precall = this.balance in");
+ addLine("begin");
+ indent();
+ addLine("this.balance <- this.balance - amount;");
+ addLine("if not (external_call this) then begin this.balance = balance_precall; false end else true");
+ unindent();
+ addLine("end");
+ unindent();
+ addLine("else false");
+
+ unindent();
+ add(")");
+ return false;
+ }
+ case FunctionType::Location::SetValue:
+ {
+ add("let amount = ");
+ solAssert(_node.arguments().size() == 1, "");
+ _node.arguments()[0]->accept(*this);
+ add(" in ");
+ return false;
+ }
default:
error(_node, "Only internal function calls supported.");
return true;
@@ -531,8 +600,17 @@ bool Why3Translator::visit(MemberAccess const& _node)
add(".length");
add(")");
}
+ else if (
+ _node.memberName() == "call" &&
+ *_node.expression().annotation().type == IntegerType(160, IntegerType::Modifier::Address)
+ )
+ {
+ // Do nothing, do not even visit the address because this will be an external call
+ //@TODO ensure that the expression itself does not have side-effects
+ return false;
+ }
else
- error(_node, "Only read-only length access for arrays supported.");
+ error(_node, "Member access: Only call and array length supported.");
return false;
}
@@ -568,13 +646,14 @@ bool Why3Translator::visit(Identifier const& _identifier)
{
bool isStateVar = isStateVariable(variable);
bool lvalue = _identifier.annotation().lValueRequested;
- if (!lvalue)
- add("!(");
if (isStateVar)
- add("state.");
+ add("this.storage.");
+ else if (!lvalue)
+ add("!(");
add("_" + variable->name());
- if (!lvalue)
+ if (!isStateVar && !lvalue)
add(")");
+ m_currentLValueIsRef = !isStateVar;
}
else
error(_identifier, "Not supported.");
@@ -608,12 +687,12 @@ bool Why3Translator::visit(Literal const& _literal)
bool Why3Translator::isStateVariable(VariableDeclaration const* _var) const
{
- return contains(m_stateVariables, _var);
+ return contains(m_currentContract.stateVariables, _var);
}
bool Why3Translator::isStateVariable(string const& _name) const
{
- for (auto const& var: m_stateVariables)
+ for (auto const& var: m_currentContract.stateVariables)
if (var->name() == _name)
return true;
return false;
@@ -632,6 +711,23 @@ bool Why3Translator::isLocalVariable(string const& _name) const
return m_localVariables.count(_name);
}
+string Why3Translator::copyOfStorage() const
+{
+ if (m_currentContract.stateVariables.empty())
+ return "()";
+ string ret = "{";
+ bool first = true;
+ for (auto const* variable: m_currentContract.stateVariables)
+ {
+ if (first)
+ first = false;
+ else
+ ret += "; ";
+ ret += "_" + variable->name() + " = this.storage._" + variable->name();
+ }
+ return ret + "}";
+}
+
void Why3Translator::visitIndentedUnlessBlock(Statement const& _statement)
{
bool isBlock = !!dynamic_cast<Block const*>(&_statement);
@@ -674,11 +770,10 @@ string Why3Translator::transformVariableReferences(string const& _annotation)
});
string varName(hash + 1, hashEnd);
if (isLocalVariable(varName))
- ret += "(to_int !_" + varName + ")";
+ ret += "(!_" + varName + ")";
else if (isStateVariable(varName))
- ret += "(to_int !(state._" + varName + "))";
- else if (varName == "result") //@todo actually use the name of the return parameters
- ret += "(to_int result)";
+ ret += "(this.storage._" + varName + ")";
+ //@todo return variables
else
ret.append(hash, hashEnd);
@@ -687,3 +782,16 @@ string Why3Translator::transformVariableReferences(string const& _annotation)
return ret;
}
+void Why3Translator::appendPreface()
+{
+ m_lines.push_back(Line{R"(
+module UInt256
+ use import mach.int.Unsigned
+ type uint256
+ constant max_uint256: int = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
+ clone export mach.int.Unsigned with
+ type t = uint256,
+ constant max = max_uint256
+end
+ )", 0});
+}
diff --git a/libsolidity/formal/Why3Translator.h b/libsolidity/formal/Why3Translator.h
index 588b6d80..e5b16844 100644
--- a/libsolidity/formal/Why3Translator.h
+++ b/libsolidity/formal/Why3Translator.h
@@ -80,6 +80,7 @@ private:
virtual bool visit(IfStatement const& _node) override;
virtual bool visit(WhileStatement const& _node) override;
virtual bool visit(Return const& _node) override;
+ virtual bool visit(Throw const& _node) override;
virtual bool visit(VariableDeclarationStatement const& _node) override;
virtual bool visit(ExpressionStatement const&) override;
virtual bool visit(Assignment const& _node) override;
@@ -104,6 +105,9 @@ private:
bool isLocalVariable(VariableDeclaration const* _var) const;
bool isLocalVariable(std::string const& _name) const;
+ /// @returns a string representing an expression that is a copy of this.storage
+ std::string copyOfStorage() const;
+
/// Visits the givin statement and indents it unless it is a block
/// (which does its own indentation).
void visitIndentedUnlessBlock(Statement const& _statement);
@@ -117,7 +121,17 @@ private:
bool m_seenContract = false;
bool m_errorOccured = false;
- std::vector<VariableDeclaration const*> m_stateVariables;
+ /// Metadata relating to the current contract
+ struct ContractMetadata
+ {
+ ContractDefinition const* contract = nullptr;
+ std::vector<VariableDeclaration const*> stateVariables;
+
+ void reset() { contract = nullptr; stateVariables.clear(); }
+ };
+
+ ContractMetadata m_currentContract;
+ bool m_currentLValueIsRef = false;
std::map<std::string, VariableDeclaration const*> m_localVariables;
struct Line
@@ -129,6 +143,5 @@ private:
ErrorList& m_errors;
};
-
}
}
--
cgit v1.2.3