aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity
diff options
context:
space:
mode:
authorchriseth <c@ethdev.com>2015-11-24 18:33:35 +0800
committerchriseth <c@ethdev.com>2015-11-24 18:33:35 +0800
commite59b9b445aead10dfd83a9e33a4f97853094de74 (patch)
tree7233392d86510352f1952a00be2dd5cac55277ea /libsolidity
parent2554d6104a491e586ecad9cf7fe31949dc46e968 (diff)
parent10fe0a2434519e9be0b556c3566d8a7b17700750 (diff)
downloaddexon-solidity-e59b9b445aead10dfd83a9e33a4f97853094de74.tar.gz
dexon-solidity-e59b9b445aead10dfd83a9e33a4f97853094de74.tar.zst
dexon-solidity-e59b9b445aead10dfd83a9e33a4f97853094de74.zip
Merge pull request #241 from chriseth/why3VariablesInConditions
Why3 variables in conditions
Diffstat (limited to 'libsolidity')
-rw-r--r--libsolidity/formal/Why3Translator.cpp125
-rw-r--r--libsolidity/formal/Why3Translator.h7
2 files changed, 114 insertions, 18 deletions
diff --git a/libsolidity/formal/Why3Translator.cpp b/libsolidity/formal/Why3Translator.cpp
index 4c187a56..356a336c 100644
--- a/libsolidity/formal/Why3Translator.cpp
+++ b/libsolidity/formal/Why3Translator.cpp
@@ -198,6 +198,14 @@ bool Why3Translator::visit(FunctionDefinition const& _function)
return false;
}
+ m_localVariables.clear();
+ for (auto const& var: _function.parameters())
+ m_localVariables[var->name()] = var.get();
+ for (auto const& var: _function.returnParameters())
+ m_localVariables[var->name()] = var.get();
+ for (auto const& var: _function.localVariables())
+ m_localVariables[var->name()] = var;
+
add("let rec _" + _function.name());
add(" (state: state)");
for (auto const& param: _function.parameters())
@@ -268,6 +276,11 @@ bool Why3Translator::visit(FunctionDefinition const& _function)
return false;
}
+void Why3Translator::endVisit(FunctionDefinition const&)
+{
+ m_localVariables.clear();
+}
+
bool Why3Translator::visit(Block const& _node)
{
addSourceFromDocStrings(_node.annotation());
@@ -452,29 +465,48 @@ bool Why3Translator::visit(FunctionCall const& _node)
return true;
}
FunctionType const& function = dynamic_cast<FunctionType const&>(*_node.expression().annotation().type);
- if (function.location() != FunctionType::Location::Internal)
+ switch (function.location())
{
- error(_node, "Only internal function calls supported.");
- return true;
- }
- if (!_node.names().empty())
+ case FunctionType::Location::AddMod:
+ case FunctionType::Location::MulMod:
{
- error(_node, "Function calls with named arguments not supported.");
- return true;
+ //@todo require that third parameter is not zero
+ add("(of_int (mod (Int.(");
+ add(function.location() == FunctionType::Location::AddMod ? "+" : "*");
+ add(") (to_int ");
+ _node.arguments().at(0)->accept(*this);
+ add(") (to_int ");
+ _node.arguments().at(1)->accept(*this);
+ add(")) (to_int ");
+ _node.arguments().at(2)->accept(*this);
+ add(")))");
+ return false;
}
+ case FunctionType::Location::Internal:
+ {
+ if (!_node.names().empty())
+ {
+ error(_node, "Function calls with named arguments not supported.");
+ return true;
+ }
- //@TODO check type conversions
+ //@TODO check type conversions
- add("(");
- _node.expression().accept(*this);
- add(" state");
- for (auto const& arg: _node.arguments())
- {
- add(" ");
- arg->accept(*this);
+ add("(");
+ _node.expression().accept(*this);
+ add(" state");
+ for (auto const& arg: _node.arguments())
+ {
+ add(" ");
+ arg->accept(*this);
+ }
+ add(")");
+ return false;
+ }
+ default:
+ error(_node, "Only internal function calls supported.");
+ return true;
}
- add(")");
- return false;
}
bool Why3Translator::visit(MemberAccess const& _node)
@@ -569,6 +601,28 @@ bool Why3Translator::isStateVariable(VariableDeclaration const* _var) const
return false;
}
+bool Why3Translator::isStateVariable(string const& _name) const
+{
+ solAssert(!!m_stateVariables, "");
+ for (auto const& var: *m_stateVariables)
+ if (var->name() == _name)
+ return true;
+ return false;
+}
+
+bool Why3Translator::isLocalVariable(VariableDeclaration const* _var) const
+{
+ for (auto const& var: m_localVariables)
+ if (var.second == _var)
+ return true;
+ return false;
+}
+
+bool Why3Translator::isLocalVariable(string const& _name) const
+{
+ return m_localVariables.count(_name);
+}
+
void Why3Translator::visitIndentedUnlessBlock(Statement const& _statement)
{
bool isBlock = !!dynamic_cast<Block const*>(&_statement);
@@ -587,5 +641,40 @@ void Why3Translator::addSourceFromDocStrings(DocumentedAnnotation const& _annota
{
auto why3Range = _annotation.docTags.equal_range("why3");
for (auto i = why3Range.first; i != why3Range.second; ++i)
- addLine(i->second.content);
+ addLine(transformVariableReferences(i->second.content));
+}
+
+string Why3Translator::transformVariableReferences(string const& _annotation)
+{
+ string ret;
+ auto pos = _annotation.begin();
+ while (true)
+ {
+ auto hash = find(pos, _annotation.end(), '#');
+ ret.append(pos, hash);
+ if (hash == _annotation.end())
+ break;
+
+ auto hashEnd = find_if(hash + 1, _annotation.end(), [](char _c)
+ {
+ return
+ (_c != '_' && _c != '$') &&
+ !('a' <= _c && _c <= 'z') &&
+ !('A' <= _c && _c <= 'Z') &&
+ !('0' <= _c && _c <= '9');
+ });
+ string varName(hash + 1, hashEnd);
+ if (isLocalVariable(varName))
+ ret += "(to_int !_" + 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)";
+ else
+ ret.append(hash, hashEnd);
+
+ pos = hashEnd;
+ }
+ return ret;
}
+
diff --git a/libsolidity/formal/Why3Translator.h b/libsolidity/formal/Why3Translator.h
index 989047e8..21dafa3c 100644
--- a/libsolidity/formal/Why3Translator.h
+++ b/libsolidity/formal/Why3Translator.h
@@ -74,6 +74,7 @@ private:
virtual bool visit(ContractDefinition const& _contract) override;
virtual void endVisit(ContractDefinition const& _contract) override;
virtual bool visit(FunctionDefinition const& _function) override;
+ virtual void endVisit(FunctionDefinition const& _function) override;
virtual bool visit(Block const&) override;
virtual bool visit(IfStatement const& _node) override;
virtual bool visit(WhileStatement const& _node) override;
@@ -98,12 +99,17 @@ private:
}
bool isStateVariable(VariableDeclaration const* _var) const;
+ bool isStateVariable(std::string const& _name) const;
+ bool isLocalVariable(VariableDeclaration const* _var) const;
+ bool isLocalVariable(std::string const& _name) const;
/// Visits the givin statement and indents it unless it is a block
/// (which does its own indentation).
void visitIndentedUnlessBlock(Statement const& _statement);
void addSourceFromDocStrings(DocumentedAnnotation const& _annotation);
+ /// Transforms substring like `#varName` and `#stateVarName` to code that evaluates to their value.
+ std::string transformVariableReferences(std::string const& _annotation);
size_t m_indentationAtLineStart = 0;
size_t m_indentation = 0;
@@ -114,6 +120,7 @@ private:
bool m_errorOccured = false;
std::vector<ASTPointer<VariableDeclaration>> const* m_stateVariables = nullptr;
+ std::map<std::string, VariableDeclaration const*> m_localVariables;
std::string m_result;
ErrorList& m_errors;