mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
Merge pull request #229 from chriseth/fv_storage_types
Formal Verification: State variables.
This commit is contained in:
commit
284d8f8b13
@ -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");
|
||||
|
||||
return true;
|
||||
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("}");
|
||||
|
||||
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);
|
||||
|
@ -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;
|
||||
};
|
||||
|
Loading…
Reference in New Issue
Block a user