aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal
diff options
context:
space:
mode:
authorchriseth <c@ethdev.com>2015-11-17 03:35:54 +0800
committerchriseth <c@ethdev.com>2015-11-19 09:04:33 +0800
commit12f19fa46b0f6bafab5206f5f4cdb035630757c3 (patch)
tree084e936eaf10b89922881f6fd4c11fe3ff37a31b /libsolidity/formal
parentb4e666ccf4fe39b0a1fc909b61daf6dc39e77fc4 (diff)
downloaddexon-solidity-12f19fa46b0f6bafab5206f5f4cdb035630757c3.tar.gz
dexon-solidity-12f19fa46b0f6bafab5206f5f4cdb035630757c3.tar.zst
dexon-solidity-12f19fa46b0f6bafab5206f5f4cdb035630757c3.zip
Formal Verification: State variables.
Diffstat (limited to 'libsolidity/formal')
-rw-r--r--libsolidity/formal/Why3Translator.cpp84
-rw-r--r--libsolidity/formal/Why3Translator.h6
2 files changed, 70 insertions, 20 deletions
diff --git a/libsolidity/formal/Why3Translator.cpp b/libsolidity/formal/Why3Translator.cpp
index 14b324e0..4c187a56 100644
--- a/libsolidity/formal/Why3Translator.cpp
+++ b/libsolidity/formal/Why3Translator.cpp
@@ -35,7 +35,6 @@ bool Why3Translator::process(SourceUnit const& _source)
fatalError(_source, "Multiple source units not yet supported");
appendPreface();
_source.accept(*this);
- addLine("end");
}
catch (FatalError& _e)
{
@@ -71,18 +70,6 @@ module UInt256
type t = uint256,
constant max = max_uint256
end
-
-module Solidity
-use import int.Int
-use import ref.Ref
-use import map.Map
-use import array.Array
-use import int.ComputerDivision
-use import mach.int.Unsigned
-use import UInt256
-
-exception Ret
-type state = StateUnused
)";
}
@@ -145,9 +132,52 @@ bool Why3Translator::visit(ContractDefinition const& _contract)
if (_contract.isLibrary())
error(_contract, "Libraries not supported.");
- addSourceFromDocStrings(_contract.annotation());
+ addLine("module Contract_" + _contract.name());
+ indent();
+ addLine("use import int.Int");
+ addLine("use import ref.Ref");
+ addLine("use import map.Map");
+ addLine("use import array.Array");
+ addLine("use import int.ComputerDivision");
+ addLine("use import mach.int.Unsigned");
+ addLine("use import UInt256");
+ addLine("exception Ret");
+
+ addLine("type state = {");
+ indent();
+ m_stateVariables = &_contract.stateVariables();
+ for (auto const& variable: _contract.stateVariables())
+ {
+ string varType = toFormalType(*variable->annotation().type);
+ if (varType.empty())
+ fatalError(*variable, "Type not supported.");
+ addLine("mutable _" + variable->name() + ": ref " + varType);
+ }
+ unindent();
+ addLine("}");
- return true;
+ if (!_contract.baseContracts().empty())
+ error(*_contract.baseContracts().front(), "Inheritance not supported.");
+ if (!_contract.definedStructs().empty())
+ error(*_contract.definedStructs().front(), "User-defined types not supported.");
+ if (!_contract.definedEnums().empty())
+ error(*_contract.definedEnums().front(), "User-defined types not supported.");
+ if (!_contract.events().empty())
+ error(*_contract.events().front(), "Events not supported.");
+ if (!_contract.functionModifiers().empty())
+ error(*_contract.functionModifiers().front(), "Modifiers not supported.");
+
+ ASTNode::listAccept(_contract.definedFunctions(), *this);
+
+ return false;
+}
+
+void Why3Translator::endVisit(ContractDefinition const& _contract)
+{
+ m_stateVariables = nullptr;
+ addSourceFromDocStrings(_contract.annotation());
+ unindent();
+ addLine("end");
}
bool Why3Translator::visit(FunctionDefinition const& _function)
@@ -437,7 +467,7 @@ bool Why3Translator::visit(FunctionCall const& _node)
add("(");
_node.expression().accept(*this);
- add(" StateUnused");
+ add(" state");
for (auto const& arg: _node.arguments())
{
add(" ");
@@ -495,10 +525,15 @@ bool Why3Translator::visit(Identifier const& _identifier)
add("_" + functionDef->name());
else if (auto variable = dynamic_cast<VariableDeclaration const*>(declaration))
{
- if (_identifier.annotation().lValueRequested)
- add("_" + variable->name());
- else
- add("!_" + variable->name());
+ bool isStateVar = isStateVariable(variable);
+ bool lvalue = _identifier.annotation().lValueRequested;
+ if (!lvalue)
+ add("!(");
+ if (isStateVar)
+ add("state.");
+ add("_" + variable->name());
+ if (!lvalue)
+ add(")");
}
else
error(_identifier, "Not supported.");
@@ -525,6 +560,15 @@ bool Why3Translator::visit(Literal const& _literal)
return false;
}
+bool Why3Translator::isStateVariable(VariableDeclaration const* _var) const
+{
+ solAssert(!!m_stateVariables, "");
+ for (auto const& var: *m_stateVariables)
+ if (var.get() == _var)
+ return true;
+ return false;
+}
+
void Why3Translator::visitIndentedUnlessBlock(Statement const& _statement)
{
bool isBlock = !!dynamic_cast<Block const*>(&_statement);
diff --git a/libsolidity/formal/Why3Translator.h b/libsolidity/formal/Why3Translator.h
index 1aa46424..989047e8 100644
--- a/libsolidity/formal/Why3Translator.h
+++ b/libsolidity/formal/Why3Translator.h
@@ -72,6 +72,7 @@ private:
virtual bool visit(SourceUnit const&) override { return true; }
virtual bool visit(ContractDefinition const& _contract) override;
+ virtual void endVisit(ContractDefinition const& _contract) override;
virtual bool visit(FunctionDefinition const& _function) override;
virtual bool visit(Block const&) override;
virtual bool visit(IfStatement const& _node) override;
@@ -96,6 +97,8 @@ private:
return false;
}
+ bool isStateVariable(VariableDeclaration const* _var) const;
+
/// Visits the givin statement and indents it unless it is a block
/// (which does its own indentation).
void visitIndentedUnlessBlock(Statement const& _statement);
@@ -109,6 +112,9 @@ private:
/// is supported.
bool m_seenContract = false;
bool m_errorOccured = false;
+
+ std::vector<ASTPointer<VariableDeclaration>> const* m_stateVariables = nullptr;
+
std::string m_result;
ErrorList& m_errors;
};