aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity
diff options
context:
space:
mode:
Diffstat (limited to 'libsolidity')
-rw-r--r--libsolidity/analysis/TypeChecker.cpp73
-rw-r--r--libsolidity/analysis/TypeChecker.h3
-rw-r--r--libsolidity/ast/AST.cpp2
-rw-r--r--libsolidity/ast/Types.cpp10
-rw-r--r--libsolidity/ast/Types.h9
-rw-r--r--libsolidity/codegen/CompilerContext.cpp16
-rw-r--r--libsolidity/codegen/CompilerContext.h10
-rw-r--r--libsolidity/codegen/CompilerUtils.cpp60
-rw-r--r--libsolidity/codegen/CompilerUtils.h12
-rw-r--r--libsolidity/codegen/ContractCompiler.cpp13
-rw-r--r--libsolidity/codegen/ExpressionCompiler.cpp17
-rw-r--r--libsolidity/formal/Why3Translator.cpp898
-rw-r--r--libsolidity/formal/Why3Translator.h147
-rw-r--r--libsolidity/inlineasm/AsmCodeGen.cpp5
-rw-r--r--libsolidity/interface/CompilerStack.cpp15
-rw-r--r--libsolidity/interface/CompilerStack.h7
-rw-r--r--libsolidity/parsing/ParserBase.cpp20
-rw-r--r--libsolidity/parsing/ParserBase.h9
18 files changed, 197 insertions, 1129 deletions
diff --git a/libsolidity/analysis/TypeChecker.cpp b/libsolidity/analysis/TypeChecker.cpp
index 4194e1c2..ef8a9345 100644
--- a/libsolidity/analysis/TypeChecker.cpp
+++ b/libsolidity/analysis/TypeChecker.cpp
@@ -22,6 +22,7 @@
#include <libsolidity/analysis/TypeChecker.h>
#include <memory>
+#include <boost/algorithm/string/predicate.hpp>
#include <boost/range/adaptor/reversed.hpp>
#include <libsolidity/ast/AST.h>
#include <libsolidity/inlineasm/AsmAnalysis.h>
@@ -363,6 +364,35 @@ void TypeChecker::checkLibraryRequirements(ContractDefinition const& _contract)
m_errorReporter.typeError(var->location(), "Library cannot have non-constant state variables");
}
+void TypeChecker::checkDoubleStorageAssignment(Assignment const& _assignment)
+{
+ TupleType const& lhs = dynamic_cast<TupleType const&>(*type(_assignment.leftHandSide()));
+ TupleType const& rhs = dynamic_cast<TupleType const&>(*type(_assignment.rightHandSide()));
+
+ bool fillRight = !lhs.components().empty() && (!lhs.components().back() || lhs.components().front());
+ size_t storageToStorageCopies = 0;
+ size_t toStorageCopies = 0;
+ for (size_t i = 0; i < lhs.components().size(); ++i)
+ {
+ ReferenceType const* ref = dynamic_cast<ReferenceType const*>(lhs.components()[i].get());
+ if (!ref || !ref->dataStoredIn(DataLocation::Storage) || ref->isPointer())
+ continue;
+ size_t rhsPos = fillRight ? i : rhs.components().size() - (lhs.components().size() - i);
+ solAssert(rhsPos < rhs.components().size(), "");
+ toStorageCopies++;
+ if (rhs.components()[rhsPos]->dataStoredIn(DataLocation::Storage))
+ storageToStorageCopies++;
+ }
+ if (storageToStorageCopies >= 1 && toStorageCopies >= 2)
+ m_errorReporter.warning(
+ _assignment.location(),
+ "This assignment performs two copies to storage. Since storage copies do not first "
+ "copy to a temporary location, one of them might be overwritten before the second "
+ "is executed and thus may have unexpected effects. It is safer to perform the copies "
+ "separately or assign to storage pointers first."
+ );
+}
+
void TypeChecker::endVisit(InheritanceSpecifier const& _inheritance)
{
auto base = dynamic_cast<ContractDefinition const*>(&dereference(_inheritance.name()));
@@ -466,13 +496,26 @@ bool TypeChecker::visit(FunctionDefinition const& _function)
var->accept(*this);
}
+ set<Declaration const*> modifiers;
for (ASTPointer<ModifierInvocation> const& modifier: _function.modifiers())
+ {
visitManually(
*modifier,
_function.isConstructor() ?
dynamic_cast<ContractDefinition const&>(*_function.scope()).annotation().linearizedBaseContracts :
vector<ContractDefinition const*>()
);
+ Declaration const* decl = &dereference(*modifier->name());
+ if (modifiers.count(decl))
+ {
+ if (dynamic_cast<ContractDefinition const*>(decl))
+ m_errorReporter.declarationError(modifier->location(), "Base constructor already provided.");
+ else
+ m_errorReporter.declarationError(modifier->location(), "Modifier already used for this function.");
+ }
+ else
+ modifiers.insert(decl);
+ }
if (m_scope->contractKind() == ContractDefinition::ContractKind::Interface)
{
if (_function.isImplemented())
@@ -1033,6 +1076,8 @@ bool TypeChecker::visit(Assignment const& _assignment)
// Sequenced assignments of tuples is not valid, make the result a "void" type.
_assignment.annotation().type = make_shared<TupleType>();
expectType(_assignment.rightHandSide(), *tupleType);
+
+ checkDoubleStorageAssignment(_assignment);
}
else if (t->category() == Type::Category::Mapping)
{
@@ -1726,10 +1771,7 @@ void TypeChecker::endVisit(Literal const& _literal)
if (_literal.looksLikeAddress())
{
if (_literal.passesAddressChecksum())
- {
_literal.annotation().type = make_shared<IntegerType>(0, IntegerType::Modifier::Address);
- return;
- }
else
m_errorReporter.warning(
_literal.location(),
@@ -1737,10 +1779,13 @@ void TypeChecker::endVisit(Literal const& _literal)
"If this is not used as an address, please prepend '00'."
);
}
- _literal.annotation().type = Type::forLiteral(_literal);
- _literal.annotation().isPure = true;
+ if (!_literal.annotation().type)
+ _literal.annotation().type = Type::forLiteral(_literal);
+
if (!_literal.annotation().type)
m_errorReporter.fatalTypeError(_literal.location(), "Invalid literal value.");
+
+ _literal.annotation().isPure = true;
}
bool TypeChecker::contractDependenciesAreCyclic(
@@ -1800,7 +1845,23 @@ void TypeChecker::expectType(Expression const& _expression, Type const& _expecte
_expectedType.toString() +
"."
);
- }
+ }
+
+ if (
+ type(_expression)->category() == Type::Category::RationalNumber &&
+ _expectedType.category() == Type::Category::FixedBytes
+ )
+ {
+ auto literal = dynamic_cast<Literal const*>(&_expression);
+
+ if (literal && !boost::starts_with(literal->value(), "0x"))
+ m_errorReporter.warning(
+ _expression.location(),
+ "Decimal literal assigned to bytesXX variable will be left-aligned. "
+ "Use an explicit conversion to silence this warning."
+ );
+ }
+
}
void TypeChecker::requireLValue(Expression const& _expression)
diff --git a/libsolidity/analysis/TypeChecker.h b/libsolidity/analysis/TypeChecker.h
index 2fa66f97..ee43d13a 100644
--- a/libsolidity/analysis/TypeChecker.h
+++ b/libsolidity/analysis/TypeChecker.h
@@ -69,6 +69,9 @@ private:
void checkContractExternalTypeClashes(ContractDefinition const& _contract);
/// Checks that all requirements for a library are fulfilled if this is a library.
void checkLibraryRequirements(ContractDefinition const& _contract);
+ /// Checks (and warns) if a tuple assignment might cause unexpected overwrites in storage.
+ /// Should only be called if the left hand side is tuple-typed.
+ void checkDoubleStorageAssignment(Assignment const& _assignment);
virtual void endVisit(InheritanceSpecifier const& _inheritance) override;
virtual void endVisit(UsingForDirective const& _usingFor) override;
diff --git a/libsolidity/ast/AST.cpp b/libsolidity/ast/AST.cpp
index 40dfa348..b929b6fe 100644
--- a/libsolidity/ast/AST.cpp
+++ b/libsolidity/ast/AST.cpp
@@ -534,6 +534,8 @@ bool Literal::looksLikeAddress() const
{
if (subDenomination() != SubDenomination::None)
return false;
+ if (token() != Token::Number)
+ return false;
string lit = value();
return lit.substr(0, 2) == "0x" && abs(int(lit.length()) - 42) <= 1;
diff --git a/libsolidity/ast/Types.cpp b/libsolidity/ast/Types.cpp
index bd3346f9..7dc6c4a6 100644
--- a/libsolidity/ast/Types.cpp
+++ b/libsolidity/ast/Types.cpp
@@ -2248,6 +2248,16 @@ TypePointer FunctionType::unaryOperatorResult(Token::Value _operator) const
return TypePointer();
}
+TypePointer FunctionType::binaryOperatorResult(Token::Value _operator, TypePointer const& _other) const
+{
+ if (_other->category() != category() || !(_operator == Token::Equal || _operator == Token::NotEqual))
+ return TypePointer();
+ FunctionType const& other = dynamic_cast<FunctionType const&>(*_other);
+ if (kind() == Kind::Internal && other.kind() == Kind::Internal && sizeOnStack() == 1 && other.sizeOnStack() == 1)
+ return commonType(shared_from_this(), _other);
+ return TypePointer();
+}
+
string FunctionType::canonicalName(bool) const
{
solAssert(m_kind == Kind::External, "");
diff --git a/libsolidity/ast/Types.h b/libsolidity/ast/Types.h
index c4ffc44c..f7a73ab5 100644
--- a/libsolidity/ast/Types.h
+++ b/libsolidity/ast/Types.h
@@ -933,6 +933,7 @@ public:
virtual bool operator==(Type const& _other) const override;
virtual bool isExplicitlyConvertibleTo(Type const& _convertTo) const override;
virtual TypePointer unaryOperatorResult(Token::Value _operator) const override;
+ virtual TypePointer binaryOperatorResult(Token::Value, TypePointer const&) const override;
virtual std::string canonicalName(bool /*_addDataLocation*/) const override;
virtual std::string toString(bool _short) const override;
virtual unsigned calldataEncodedSize(bool _padded) const override;
@@ -1038,6 +1039,7 @@ public:
virtual std::string toString(bool _short) const override;
virtual std::string canonicalName(bool _addDataLocation) const override;
virtual bool canLiveOutsideStorage() const override { return false; }
+ virtual TypePointer binaryOperatorResult(Token::Value, TypePointer const&) const override { return TypePointer(); }
virtual TypePointer encodingType() const override
{
return std::make_shared<IntegerType>(256);
@@ -1116,11 +1118,7 @@ public:
explicit ModuleType(SourceUnit const& _source): m_sourceUnit(_source) {}
- virtual TypePointer binaryOperatorResult(Token::Value, TypePointer const&) const override
- {
- return TypePointer();
- }
-
+ virtual TypePointer binaryOperatorResult(Token::Value, TypePointer const&) const override { return TypePointer(); }
virtual std::string identifier() const override;
virtual bool operator==(Type const& _other) const override;
virtual bool canBeStored() const override { return false; }
@@ -1178,6 +1176,7 @@ public:
virtual std::string identifier() const override { return "t_inaccessible"; }
virtual bool isImplicitlyConvertibleTo(Type const&) const override { return false; }
virtual bool isExplicitlyConvertibleTo(Type const&) const override { return false; }
+ virtual TypePointer binaryOperatorResult(Token::Value, TypePointer const&) const override { return TypePointer(); }
virtual unsigned calldataEncodedSize(bool _padded) const override { (void)_padded; return 32; }
virtual bool canBeStored() const override { return false; }
virtual bool canLiveOutsideStorage() const override { return false; }
diff --git a/libsolidity/codegen/CompilerContext.cpp b/libsolidity/codegen/CompilerContext.cpp
index d98efcad..6875bda1 100644
--- a/libsolidity/codegen/CompilerContext.cpp
+++ b/libsolidity/codegen/CompilerContext.cpp
@@ -26,6 +26,7 @@
#include <libsolidity/codegen/Compiler.h>
#include <libsolidity/interface/Version.h>
#include <libsolidity/interface/ErrorReporter.h>
+#include <libsolidity/parsing/Scanner.h>
#include <libsolidity/inlineasm/AsmParser.h>
#include <libsolidity/inlineasm/AsmCodeGen.h>
#include <libsolidity/inlineasm/AsmAnalysis.h>
@@ -123,6 +124,7 @@ void CompilerContext::addVariable(VariableDeclaration const& _declaration,
unsigned _offsetToCurrent)
{
solAssert(m_asm->deposit() >= 0 && unsigned(m_asm->deposit()) >= _offsetToCurrent, "");
+ solAssert(m_localVariables.count(&_declaration) == 0, "Variable already present");
m_localVariables[&_declaration] = unsigned(m_asm->deposit()) - _offsetToCurrent;
}
@@ -243,6 +245,20 @@ CompilerContext& CompilerContext::appendConditionalInvalid()
return *this;
}
+CompilerContext& CompilerContext::appendRevert()
+{
+ return *this << u256(0) << u256(0) << Instruction::REVERT;
+}
+
+CompilerContext& CompilerContext::appendConditionalRevert()
+{
+ *this << Instruction::ISZERO;
+ eth::AssemblyItem afterTag = appendConditionalJump();
+ appendRevert();
+ *this << afterTag;
+ return *this;
+}
+
void CompilerContext::resetVisitedNodes(ASTNode const* _node)
{
stack<ASTNode const*> newStack;
diff --git a/libsolidity/codegen/CompilerContext.h b/libsolidity/codegen/CompilerContext.h
index 030b35a6..1968c1e1 100644
--- a/libsolidity/codegen/CompilerContext.h
+++ b/libsolidity/codegen/CompilerContext.h
@@ -136,11 +136,15 @@ public:
/// Appends a JUMP to a new tag and @returns the tag
eth::AssemblyItem appendJumpToNew() { return m_asm->appendJump().tag(); }
/// Appends a JUMP to a tag already on the stack
- CompilerContext& appendJump(eth::AssemblyItem::JumpType _jumpType = eth::AssemblyItem::JumpType::Ordinary);
+ CompilerContext& appendJump(eth::AssemblyItem::JumpType _jumpType = eth::AssemblyItem::JumpType::Ordinary);
/// Appends an INVALID instruction
- CompilerContext& appendInvalid();
+ CompilerContext& appendInvalid();
/// Appends a conditional INVALID instruction
- CompilerContext& appendConditionalInvalid();
+ CompilerContext& appendConditionalInvalid();
+ /// Appends a REVERT(0, 0) call
+ CompilerContext& appendRevert();
+ /// Appends a conditional REVERT(0, 0) call
+ CompilerContext& appendConditionalRevert();
/// Appends a JUMP to a specific tag
CompilerContext& appendJumpTo(eth::AssemblyItem const& _tag) { m_asm->appendJump(_tag); return *this; }
/// Appends pushing of a new tag and @returns the new tag.
diff --git a/libsolidity/codegen/CompilerUtils.cpp b/libsolidity/codegen/CompilerUtils.cpp
index 3baaaddf..4edec155 100644
--- a/libsolidity/codegen/CompilerUtils.cpp
+++ b/libsolidity/codegen/CompilerUtils.cpp
@@ -128,7 +128,7 @@ void CompilerUtils::storeInMemoryDynamic(Type const& _type, bool _padToWordBound
m_context << Instruction::DUP1;
storeStringData(bytesConstRef(str->value()));
if (_padToWordBoundaries)
- m_context << u256(((str->value().size() + 31) / 32) * 32);
+ m_context << u256(max<size_t>(32, ((str->value().size() + 31) / 32) * 32));
else
m_context << u256(str->value().size());
m_context << Instruction::ADD;
@@ -305,15 +305,9 @@ void CompilerUtils::memoryCopy32()
m_context.appendInlineAssembly(R"(
{
- jumpi(end, eq(len, 0))
- start:
- mstore(dst, mload(src))
- jumpi(end, iszero(gt(len, 32)))
- dst := add(dst, 32)
- src := add(src, 32)
- len := sub(len, 32)
- jump(start)
- end:
+ for { let i := 0 } lt(i, len) { i := add(i, 32) } {
+ mstore(add(dst, i), mload(add(src, i)))
+ }
}
)",
{ "len", "dst", "src" }
@@ -327,21 +321,22 @@ void CompilerUtils::memoryCopy()
m_context.appendInlineAssembly(R"(
{
- // copy 32 bytes at once
- start32:
- jumpi(end32, lt(len, 32))
- mstore(dst, mload(src))
- dst := add(dst, 32)
- src := add(src, 32)
- len := sub(len, 32)
- jump(start32)
- end32:
-
- // copy the remainder (0 < len < 32)
- let mask := sub(exp(256, sub(32, len)), 1)
- let srcpart := and(mload(src), not(mask))
- let dstpart := and(mload(dst), mask)
- mstore(dst, or(srcpart, dstpart))
+ // copy 32 bytes at once
+ for
+ {}
+ iszero(lt(len, 32))
+ {
+ dst := add(dst, 32)
+ src := add(src, 32)
+ len := sub(len, 32)
+ }
+ { mstore(dst, mload(src)) }
+
+ // copy the remainder (0 < len < 32)
+ let mask := sub(exp(256, sub(32, len)), 1)
+ let srcpart := and(mload(src), not(mask))
+ let dstpart := and(mload(dst), mask)
+ mstore(dst, or(srcpart, dstpart))
}
)",
{ "len", "dst", "src" }
@@ -392,7 +387,13 @@ void CompilerUtils::pushCombinedFunctionEntryLabel(Declaration const& _function)
Instruction::OR;
}
-void CompilerUtils::convertType(Type const& _typeOnStack, Type const& _targetType, bool _cleanupNeeded, bool _chopSignBits)
+void CompilerUtils::convertType(
+ Type const& _typeOnStack,
+ Type const& _targetType,
+ bool _cleanupNeeded,
+ bool _chopSignBits,
+ bool _asPartOfArgumentDecoding
+)
{
// For a type extension, we need to remove all higher-order bits that we might have ignored in
// previous operations.
@@ -450,7 +451,10 @@ void CompilerUtils::convertType(Type const& _typeOnStack, Type const& _targetTyp
EnumType const& enumType = dynamic_cast<decltype(enumType)>(_typeOnStack);
solAssert(enumType.numberOfMembers() > 0, "empty enum should have caused a parser error.");
m_context << u256(enumType.numberOfMembers() - 1) << Instruction::DUP2 << Instruction::GT;
- m_context.appendConditionalInvalid();
+ if (_asPartOfArgumentDecoding)
+ m_context.appendConditionalRevert();
+ else
+ m_context.appendConditionalInvalid();
enumOverflowCheckPending = false;
}
break;
@@ -985,7 +989,7 @@ unsigned CompilerUtils::loadFromMemoryHelper(Type const& _type, bool _fromCallda
m_context << shiftFactor << Instruction::MUL;
}
if (_fromCalldata)
- convertType(_type, _type, true);
+ convertType(_type, _type, true, false, true);
return numBytes;
}
diff --git a/libsolidity/codegen/CompilerUtils.h b/libsolidity/codegen/CompilerUtils.h
index a88951bc..0ee053a9 100644
--- a/libsolidity/codegen/CompilerUtils.h
+++ b/libsolidity/codegen/CompilerUtils.h
@@ -110,10 +110,12 @@ public:
void zeroInitialiseMemoryArray(ArrayType const& _type);
/// Copies full 32 byte words in memory (regions cannot overlap), i.e. may copy more than length.
+ /// Length can be zero, in this case, it copies nothing.
/// Stack pre: <size> <target> <source>
/// Stack post:
void memoryCopy32();
/// Copies data in memory (regions cannot overlap).
+ /// Length can be zero, in this case, it copies nothing.
/// Stack pre: <size> <target> <source>
/// Stack post:
void memoryCopy();
@@ -135,7 +137,15 @@ public:
/// If @a _cleanupNeeded, high order bits cleanup is also done if no type conversion would be
/// necessary.
/// If @a _chopSignBits, the function resets the signed bits out of the width of the signed integer.
- void convertType(Type const& _typeOnStack, Type const& _targetType, bool _cleanupNeeded = false, bool _chopSignBits = false);
+ /// If @a _asPartOfArgumentDecoding is true, failed conversions are flagged via REVERT,
+ /// otherwise they are flagged with INVALID.
+ void convertType(
+ Type const& _typeOnStack,
+ Type const& _targetType,
+ bool _cleanupNeeded = false,
+ bool _chopSignBits = false,
+ bool _asPartOfArgumentDecoding = false
+ );
/// Creates a zero-value for the given type and puts it onto the stack. This might allocate
/// memory for memory references.
diff --git a/libsolidity/codegen/ContractCompiler.cpp b/libsolidity/codegen/ContractCompiler.cpp
index dc090634..977a2c7c 100644
--- a/libsolidity/codegen/ContractCompiler.cpp
+++ b/libsolidity/codegen/ContractCompiler.cpp
@@ -111,7 +111,7 @@ void ContractCompiler::appendCallValueCheck()
{
// Throw if function is not payable but call contained ether.
m_context << Instruction::CALLVALUE;
- m_context.appendConditionalInvalid();
+ m_context.appendConditionalRevert();
}
void ContractCompiler::appendInitAndConstructorCode(ContractDefinition const& _contract)
@@ -276,7 +276,7 @@ void ContractCompiler::appendFunctionSelector(ContractDefinition const& _contrac
appendReturnValuePacker(FunctionType(*fallback).returnParameterTypes(), _contract.isLibrary());
}
else
- m_context.appendInvalid();
+ m_context.appendRevert();
for (auto const& it: interfaceFunctions)
{
@@ -368,7 +368,7 @@ void ContractCompiler::appendCalldataUnpacker(TypePointers const& _typeParameter
// copy to memory
// move calldata type up again
CompilerUtils(m_context).moveIntoStack(calldataType->sizeOnStack());
- CompilerUtils(m_context).convertType(*calldataType, arrayType);
+ CompilerUtils(m_context).convertType(*calldataType, arrayType, false, false, true);
// fetch next pointer again
CompilerUtils(m_context).moveToStackTop(arrayType.sizeOnStack());
}
@@ -805,8 +805,7 @@ bool ContractCompiler::visit(Throw const& _throw)
{
CompilerContext::LocationSetter locationSetter(m_context, _throw);
// Do not send back an error detail.
- m_context << u256(0) << u256(0);
- m_context << Instruction::REVERT;
+ m_context.appendRevert();
return false;
}
@@ -879,6 +878,7 @@ void ContractCompiler::appendModifierOrFunctionCode()
solAssert(m_currentFunction, "");
unsigned stackSurplus = 0;
Block const* codeBlock = nullptr;
+ vector<VariableDeclaration const*> addedVariables;
m_modifierDepth++;
@@ -902,6 +902,7 @@ void ContractCompiler::appendModifierOrFunctionCode()
for (unsigned i = 0; i < modifier.parameters().size(); ++i)
{
m_context.addVariable(*modifier.parameters()[i]);
+ addedVariables.push_back(modifier.parameters()[i].get());
compileExpression(
*modifierInvocation->arguments()[i],
modifier.parameters()[i]->annotation().type
@@ -928,6 +929,8 @@ void ContractCompiler::appendModifierOrFunctionCode()
m_returnTags.pop_back();
CompilerUtils(m_context).popStackSlots(stackSurplus);
+ for (auto var: addedVariables)
+ m_context.removeVariable(*var);
}
m_modifierDepth--;
}
diff --git a/libsolidity/codegen/ExpressionCompiler.cpp b/libsolidity/codegen/ExpressionCompiler.cpp
index 03bba80c..a65549fd 100644
--- a/libsolidity/codegen/ExpressionCompiler.cpp
+++ b/libsolidity/codegen/ExpressionCompiler.cpp
@@ -587,7 +587,7 @@ bool ExpressionCompiler::visit(FunctionCall const& _functionCall)
m_context << Instruction::CREATE;
// Check if zero (out of stack or not enough balance).
m_context << Instruction::DUP1 << Instruction::ISZERO;
- m_context.appendConditionalInvalid();
+ m_context.appendConditionalRevert();
if (function.valueSet())
m_context << swapInstruction(1) << Instruction::POP;
break;
@@ -651,7 +651,7 @@ bool ExpressionCompiler::visit(FunctionCall const& _functionCall)
{
// Check if zero (out of stack or not enough balance).
m_context << Instruction::ISZERO;
- m_context.appendConditionalInvalid();
+ m_context.appendConditionalRevert();
}
break;
case FunctionType::Kind::Selfdestruct:
@@ -660,9 +660,7 @@ bool ExpressionCompiler::visit(FunctionCall const& _functionCall)
m_context << Instruction::SELFDESTRUCT;
break;
case FunctionType::Kind::Revert:
- // memory offset returned - zero length
- m_context << u256(0) << u256(0);
- m_context << Instruction::REVERT;
+ m_context.appendRevert();
break;
case FunctionType::Kind::SHA3:
{
@@ -888,9 +886,9 @@ bool ExpressionCompiler::visit(FunctionCall const& _functionCall)
auto success = m_context.appendConditionalJump();
if (function.kind() == FunctionType::Kind::Assert)
// condition was not met, flag an error
- m_context << Instruction::INVALID;
+ m_context.appendInvalid();
else
- m_context << u256(0) << u256(0) << Instruction::REVERT;
+ m_context.appendRevert();
// the success branch
m_context << success;
break;
@@ -1368,6 +1366,7 @@ void ExpressionCompiler::appendAndOrOperatorCode(BinaryOperation const& _binaryO
void ExpressionCompiler::appendCompareOperatorCode(Token::Value _operator, Type const& _type)
{
+ solAssert(_type.sizeOnStack() == 1, "Comparison of multi-slot types.");
if (_operator == Token::Equal || _operator == Token::NotEqual)
{
if (FunctionType const* funType = dynamic_cast<decltype(funType)>(&_type))
@@ -1695,7 +1694,7 @@ void ExpressionCompiler::appendExternalFunctionCall(
if (funKind == FunctionType::Kind::External || funKind == FunctionType::Kind::CallCode || funKind == FunctionType::Kind::DelegateCall)
{
m_context << Instruction::DUP1 << Instruction::EXTCODESIZE << Instruction::ISZERO;
- m_context.appendConditionalInvalid();
+ m_context.appendConditionalRevert();
existenceChecked = true;
}
@@ -1731,7 +1730,7 @@ void ExpressionCompiler::appendExternalFunctionCall(
{
//Propagate error condition (if CALL pushes 0 on stack).
m_context << Instruction::ISZERO;
- m_context.appendConditionalInvalid();
+ m_context.appendConditionalRevert();
}
utils().popStackSlots(remainsSize);
diff --git a/libsolidity/formal/Why3Translator.cpp b/libsolidity/formal/Why3Translator.cpp
deleted file mode 100644
index fecab2de..00000000
--- a/libsolidity/formal/Why3Translator.cpp
+++ /dev/null
@@ -1,898 +0,0 @@
-/*
- This file is part of solidity.
-
- solidity is free software: you can redistribute it and/or modify
- it under the terms of the GNU General Public License as published by
- the Free Software Foundation, either version 3 of the License, or
- (at your option) any later version.
-
- solidity is distributed in the hope that it will be useful,
- but WITHOUT ANY WARRANTY; without even the implied warranty of
- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- GNU General Public License for more details.
-
- You should have received a copy of the GNU General Public License
- along with solidity. If not, see <http://www.gnu.org/licenses/>.
-*/
-/**
- * @author Christian <c@ethdev.com>
- * @date 2015
- * Component that translates Solidity code into the why3 programming language.
- */
-
-#include <libsolidity/formal/Why3Translator.h>
-#include <boost/algorithm/string/predicate.hpp>
-
-using namespace std;
-using namespace dev;
-using namespace dev::solidity;
-
-bool Why3Translator::process(SourceUnit const& _source)
-{
- try
- {
- if (m_lines.size() != 1 || !m_lines.back().contents.empty())
- fatalError(_source, string("Multiple source units not yet supported"));
- appendPreface();
- _source.accept(*this);
- }
- catch (NoFormalType&)
- {
- solAssert(false, "There is a call to toFormalType() that does not catch NoFormalType exceptions.");
- }
- catch (FatalError& /*_e*/)
- {
- solAssert(m_errorOccured, "");
- }
- return !m_errorOccured;
-}
-
-string Why3Translator::translation() const
-{
- string result;
- for (auto const& line: m_lines)
- result += string(line.indentation, '\t') + line.contents + "\n";
- return result;
-}
-
-string Why3Translator::toFormalType(Type const& _type) const
-{
- 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";
- }
- else if (auto type = dynamic_cast<ArrayType const*>(&_type))
- {
- if (!type->isByteArray() && type->isDynamicallySized() && type->dataStoredIn(DataLocation::Memory))
- {
- // Not catching NoFormalType exception. Let the caller deal with it.
- string base = toFormalType(*type->baseType());
- return "array " + base;
- }
- }
- else if (auto mappingType = dynamic_cast<MappingType const*>(&_type))
- {
- solAssert(mappingType->keyType(), "A mappingType misses a keyType.");
- if (dynamic_cast<IntegerType const*>(&*mappingType->keyType()))
- {
- //@TODO Use the information from the key type and specify the length of the array as an invariant.
- // Also the constructor need to specify the length of the array.
- solAssert(mappingType->valueType(), "A mappingType misses a valueType.");
- // Not catching NoFormalType exception. Let the caller deal with it.
- string valueTypeFormal = toFormalType(*mappingType->valueType());
- return "array " + valueTypeFormal;
- }
- }
-
- BOOST_THROW_EXCEPTION(NoFormalType()
- << errinfo_noFormalTypeFrom(_type.toString(true)));
-}
-
-void Why3Translator::addLine(string const& _line)
-{
- newLine();
- add(_line);
- newLine();
-}
-
-void Why3Translator::add(string const& _str)
-{
- m_lines.back().contents += _str;
-}
-
-void Why3Translator::newLine()
-{
- if (!m_lines.back().contents.empty())
- m_lines.push_back({"", m_lines.back().indentation});
-}
-
-void Why3Translator::unindent()
-{
- newLine();
- solAssert(m_lines.back().indentation > 0, "");
- m_lines.back().indentation--;
-}
-
-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.");
-
- 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 Revert");
- addLine("exception Return");
-
- if (_contract.stateVariables().empty())
- addLine("type state = ()");
- else
- {
- addLine("type state = {");
- indent();
- m_currentContract.stateVariables = _contract.stateVariables();
- for (VariableDeclaration const* variable: m_currentContract.stateVariables)
- {
- string varType;
- try
- {
- varType = toFormalType(*variable->annotation().type);
- }
- catch (NoFormalType &err)
- {
- string const* typeNamePtr = boost::get_error_info<errinfo_noFormalTypeFrom>(err);
- string typeName = typeNamePtr ? " \"" + *typeNamePtr + "\"" : "";
- fatalError(*variable, "Type" + typeName + " 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())
- 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&)
-{
- m_currentContract.reset();
- unindent();
- addLine("end");
-}
-
-bool Why3Translator::visit(FunctionDefinition const& _function)
-{
- if (!_function.isImplemented())
- {
- error(_function, "Unimplemented functions not supported.");
- return false;
- }
- if (_function.name().empty())
- {
- error(_function, "Fallback functions not supported.");
- return false;
- }
- if (!_function.modifiers().empty())
- {
- error(_function, "Modifiers not supported.");
- 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(" (this: account)");
- for (auto const& param: _function.parameters())
- {
- string paramType;
- try
- {
- paramType = toFormalType(*param->annotation().type);
- }
- catch (NoFormalType &err)
- {
- string const* typeName = boost::get_error_info<errinfo_noFormalTypeFrom>(err);
- error(*param, "Parameter type \"" + (typeName ? *typeName : "") + "\" not supported.");
- }
- if (param->name().empty())
- error(*param, "Anonymous function parameters not supported.");
- add(" (arg_" + param->name() + ": " + paramType + ")");
- }
- add(":");
-
- indent();
- indent();
- string retString = "(";
- for (auto const& retParam: _function.returnParameters())
- {
- string paramType;
- try
- {
- paramType = toFormalType(*retParam->annotation().type);
- }
- catch (NoFormalType &err)
- {
- string const* typeName = boost::get_error_info<errinfo_noFormalTypeFrom>(err);
- error(*retParam, "Parameter type " + (typeName ? *typeName : "") + " not supported.");
- }
- if (retString.size() != 1)
- retString += ", ";
- retString += paramType;
- }
- add(retString + ")");
- 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");
- for (auto const& variable: _function.returnParameters())
- {
- if (variable->name().empty())
- error(*variable, "Unnamed return variables not yet supported.");
- string varType;
- try
- {
- varType = toFormalType(*variable->annotation().type);
- }
- catch (NoFormalType &err)
- {
- string const* typeNamePtr = boost::get_error_info<errinfo_noFormalTypeFrom>(err);
- error(*variable, "Type " + (typeNamePtr ? *typeNamePtr : "") + "in return parameter not yet supported.");
- }
- addLine("let _" + variable->name() + ": ref " + varType + " = ref (of_int 0) in");
- }
- for (VariableDeclaration const* variable: _function.localVariables())
- {
- if (variable->name().empty())
- error(*variable, "Unnamed variables not yet supported.");
- string varType;
- try
- {
- varType = toFormalType(*variable->annotation().type);
- }
- catch (NoFormalType &err)
- {
- string const* typeNamePtr = boost::get_error_info<errinfo_noFormalTypeFrom>(err);
- error(*variable, "Type " + (typeNamePtr ? *typeNamePtr : "") + "in variable declaration not yet supported.");
- }
- addLine("let _" + variable->name() + ": ref " + varType + " = ref (of_int 0) in");
- }
- addLine("try");
-
- _function.body().accept(*this);
- add(";");
- addLine("raise Return");
-
- string retVals;
- for (auto const& variable: _function.returnParameters())
- {
- if (!retVals.empty())
- retVals += ", ";
- retVals += "!_" + variable->name();
- }
- 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("");
- return false;
-}
-
-void Why3Translator::endVisit(FunctionDefinition const&)
-{
- m_localVariables.clear();
-}
-
-bool Why3Translator::visit(Block const& _node)
-{
- addSourceFromDocStrings(_node.annotation());
- add("begin");
- indent();
- for (size_t i = 0; i < _node.statements().size(); ++i)
- {
- _node.statements()[i]->accept(*this);
- if (i != _node.statements().size() - 1)
- {
- auto it = m_lines.end() - 1;
- while (it != m_lines.begin() && it->contents.empty())
- --it;
- if (!boost::algorithm::ends_with(it->contents, "begin"))
- it->contents += ";";
- }
- newLine();
- }
- unindent();
- add("end");
- return false;
-}
-
-bool Why3Translator::visit(IfStatement const& _node)
-{
- addSourceFromDocStrings(_node.annotation());
-
- add("if ");
- _node.condition().accept(*this);
- add(" then");
- visitIndentedUnlessBlock(_node.trueStatement());
- if (_node.falseStatement())
- {
- newLine();
- add("else");
- visitIndentedUnlessBlock(*_node.falseStatement());
- }
- return false;
-}
-
-bool Why3Translator::visit(WhileStatement const& _node)
-{
- addSourceFromDocStrings(_node.annotation());
-
- // Why3 does not appear to support do-while loops,
- // so we will simulate them by performing a while
- // loop with the body prepended once.
-
- if (_node.isDoWhile())
- {
- visitIndentedUnlessBlock(_node.body());
- newLine();
- }
-
- add("while ");
- _node.condition().accept(*this);
- newLine();
- add("do");
- visitIndentedUnlessBlock(_node.body());
- add("done");
- return false;
-}
-
-bool Why3Translator::visit(Return const& _node)
-{
- addSourceFromDocStrings(_node.annotation());
-
- if (_node.expression())
- {
- solAssert(!!_node.annotation().functionReturnParameters, "");
- auto const& params = _node.annotation().functionReturnParameters->parameters();
- if (params.size() != 1)
- {
- error(_node, "Directly returning tuples not supported. Rather assign to return variable.");
- return false;
- }
- add("begin _" + params.front()->name() + " := ");
- _node.expression()->accept(*this);
- add("; raise Return end");
- }
- else
- add("raise Return");
- return false;
-}
-
-bool Why3Translator::visit(Throw const& _node)
-{
- addSourceFromDocStrings(_node.annotation());
- add("raise Revert");
- return false;
-}
-
-bool Why3Translator::visit(VariableDeclarationStatement const& _node)
-{
- addSourceFromDocStrings(_node.annotation());
-
- if (_node.declarations().size() != 1)
- {
- error(_node, "Multiple variables not supported.");
- return false;
- }
- if (_node.initialValue())
- {
- add("_" + _node.declarations().front()->name() + " := ");
- _node.initialValue()->accept(*this);
- }
- return false;
-}
-
-bool Why3Translator::visit(ExpressionStatement const& _node)
-{
- addSourceFromDocStrings(_node.annotation());
- return true;
-}
-
-bool Why3Translator::visit(Assignment const& _node)
-{
- if (_node.assignmentOperator() != Token::Assign)
- error(_node, "Compound assignment not supported.");
-
- _node.leftHandSide().accept(*this);
-
- add(m_currentLValueIsRef ? " := " : " <- ");
- _node.rightHandSide().accept(*this);
-
- return false;
-}
-
-bool Why3Translator::visit(TupleExpression const& _node)
-{
- if (_node.components().size() != 1)
- error(_node, "Only tuples with exactly one component supported.");
- add("(");
- return true;
-}
-
-bool Why3Translator::visit(UnaryOperation const& _unaryOperation)
-{
- try
- {
- toFormalType(*_unaryOperation.annotation().type);
- }
- catch (NoFormalType &err)
- {
- string const* typeNamePtr = boost::get_error_info<errinfo_noFormalTypeFrom>(err);
- error(_unaryOperation, "Type \"" + (typeNamePtr ? *typeNamePtr : "") + "\" supported in unary operation.");
- }
-
- switch (_unaryOperation.getOperator())
- {
- case Token::Not: // !
- add("(not ");
- break;
- default:
- error(_unaryOperation, "Operator not supported.");
- break;
- }
-
- _unaryOperation.subExpression().accept(*this);
- add(")");
-
- return false;
-}
-
-bool Why3Translator::visit(BinaryOperation const& _binaryOperation)
-{
- Expression const& leftExpression = _binaryOperation.leftExpression();
- Expression const& rightExpression = _binaryOperation.rightExpression();
- solAssert(!!_binaryOperation.annotation().commonType, "");
- Type const& commonType = *_binaryOperation.annotation().commonType;
- Token::Value const c_op = _binaryOperation.getOperator();
-
- if (commonType.category() == Type::Category::RationalNumber)
- {
- auto const& constantNumber = dynamic_cast<RationalNumberType const&>(commonType);
- if (constantNumber.isFractional())
- error(_binaryOperation, "Fractional numbers not supported.");
- else
- add("(of_int " + toString(commonType.literalValue(nullptr)) + ")");
- return false;
- }
- static const map<Token::Value, char const*> optrans({
- {Token::And, " && "},
- {Token::Or, " || "},
- {Token::BitOr, " lor "},
- {Token::BitXor, " lxor "},
- {Token::BitAnd, " land "},
- {Token::Add, " + "},
- {Token::Sub, " - "},
- {Token::Mul, " * "},
- {Token::Div, " / "},
- {Token::Mod, " mod "},
- {Token::Equal, " = "},
- {Token::NotEqual, " <> "},
- {Token::LessThan, " < "},
- {Token::GreaterThan, " > "},
- {Token::LessThanOrEqual, " <= "},
- {Token::GreaterThanOrEqual, " >= "}
- });
- if (!optrans.count(c_op))
- {
- error(_binaryOperation, "Operator not supported.");
- return true;
- }
-
- add("(");
- leftExpression.accept(*this);
- add(optrans.at(c_op));
- rightExpression.accept(*this);
- add(")");
-
- return false;
-}
-
-bool Why3Translator::visit(FunctionCall const& _node)
-{
- if (_node.annotation().kind == FunctionCallKind::TypeConversion || _node.annotation().kind == FunctionCallKind::StructConstructorCall)
- {
- error(_node, "Only ordinary function calls supported.");
- return true;
- }
- FunctionType const& function = dynamic_cast<FunctionType const&>(*_node.expression().annotation().type);
- switch (function.kind())
- {
- case FunctionType::Kind::AddMod:
- case FunctionType::Kind::MulMod:
- {
- //@todo require that third parameter is not zero
- add("(of_int (mod (Int.(");
- add(function.kind() == FunctionType::Kind::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::Kind::Internal:
- {
- if (!_node.names().empty())
- {
- error(_node, "Function calls with named arguments not supported.");
- return true;
- }
-
- //@TODO check type conversions
-
- add("(");
- _node.expression().accept(*this);
- add(" state");
- for (auto const& arg: _node.arguments())
- {
- add(" ");
- arg->accept(*this);
- }
- add(")");
- return false;
- }
- case FunctionType::Kind::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::Kind::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;
- }
-}
-
-bool Why3Translator::visit(MemberAccess const& _node)
-{
- if (
- _node.expression().annotation().type->category() == Type::Category::Array &&
- _node.memberName() == "length" &&
- !_node.annotation().lValueRequested
- )
- {
- add("(of_int ");
- _node.expression().accept(*this);
- 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, "Member access: Only call and array length supported.");
- return false;
-}
-
-bool Why3Translator::visit(IndexAccess const& _node)
-{
- auto baseType = dynamic_cast<ArrayType const*>(_node.baseExpression().annotation().type.get());
- if (!baseType)
- {
- error(_node, "Index access only supported for arrays.");
- return true;
- }
- if (_node.annotation().lValueRequested)
- {
- error(_node, "Assignment to array elements not supported.");
- return true;
- }
- add("(");
- _node.baseExpression().accept(*this);
- add("[to_int ");
- _node.indexExpression()->accept(*this);
- add("]");
- add(")");
-
- return false;
-}
-
-bool Why3Translator::visit(Identifier const& _identifier)
-{
- Declaration const* declaration = _identifier.annotation().referencedDeclaration;
- if (FunctionDefinition const* functionDef = dynamic_cast<FunctionDefinition const*>(declaration))
- add("_" + functionDef->name());
- else if (auto variable = dynamic_cast<VariableDeclaration const*>(declaration))
- {
- bool isStateVar = isStateVariable(variable);
- bool lvalue = _identifier.annotation().lValueRequested;
- if (isStateVar)
- add("this.storage.");
- else if (!lvalue)
- add("!(");
- add("_" + variable->name());
- if (!isStateVar && !lvalue)
- add(")");
- m_currentLValueIsRef = !isStateVar;
- }
- else
- error(_identifier, "Not supported.");
- return false;
-}
-
-bool Why3Translator::visit(Literal const& _literal)
-{
- TypePointer type = _literal.annotation().type;
- switch (type->category())
- {
- case Type::Category::Bool:
- if (type->literalValue(&_literal) == 0)
- add("false");
- else
- add("true");
- break;
- case Type::Category::RationalNumber:
- {
- auto const& constantNumber = dynamic_cast<RationalNumberType const&>(*type);
- if (constantNumber.isFractional())
- error(_literal, "Fractional numbers not supported.");
- else
- add("(of_int " + toString(type->literalValue(&_literal)) + ")");
- break;
- }
- default:
- error(_literal, "Not supported.");
- }
- return false;
-}
-
-bool Why3Translator::visit(PragmaDirective const& _pragma)
-{
- if (_pragma.tokens().empty())
- error(_pragma, "Not supported");
- else if (_pragma.literals().empty())
- error(_pragma, "Not supported");
- else if (_pragma.literals()[0] != "solidity")
- error(_pragma, "Not supported");
- else if (_pragma.tokens()[0] != Token::Identifier)
- error(_pragma, "A literal 'solidity' is not an identifier. Strange");
-
- return false;
-}
-
-bool Why3Translator::isStateVariable(VariableDeclaration const* _var) const
-{
- return contains(m_currentContract.stateVariables, _var);
-}
-
-bool Why3Translator::isStateVariable(string const& _name) const
-{
- for (auto const& var: m_currentContract.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);
-}
-
-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);
- if (isBlock)
- newLine();
- else
- indent();
- _statement.accept(*this);
- if (isBlock)
- newLine();
- else
- unindent();
-}
-
-void Why3Translator::addSourceFromDocStrings(DocumentedAnnotation const& _annotation)
-{
- auto why3Range = _annotation.docTags.equal_range("why3");
- for (auto i = why3Range.first; i != why3Range.second; ++i)
- 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 += "(!_" + varName + ")";
- else if (isStateVariable(varName))
- ret += "(this.storage._" + varName + ")";
- //@todo return variables
- else
- ret.append(hash, hashEnd);
-
- pos = hashEnd;
- }
- 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
-
-module Address
- use import mach.int.Unsigned
- type address
- constant max_address: int = 0xffffffffffffffffffffffffffffffffffffffff (* 160 bit = 40 f's *)
- clone export mach.int.Unsigned with
- type t = address,
- constant max = max_address
-end
- )", 0});
-}
-
-void Why3Translator::error(ASTNode const& _source, std::string const& _description)
-{
- m_errorOccured = true;
- m_errorReporter.why3TranslatorError(_source, _description);
-}
-void Why3Translator::fatalError(ASTNode const& _source, std::string const& _description)
-{
- m_errorOccured = true;
- m_errorReporter.fatalWhy3TranslatorError(_source, _description);
-}
-
diff --git a/libsolidity/formal/Why3Translator.h b/libsolidity/formal/Why3Translator.h
deleted file mode 100644
index b48317be..00000000
--- a/libsolidity/formal/Why3Translator.h
+++ /dev/null
@@ -1,147 +0,0 @@
-/*
- This file is part of solidity.
-
- solidity is free software: you can redistribute it and/or modify
- it under the terms of the GNU General Public License as published by
- the Free Software Foundation, either version 3 of the License, or
- (at your option) any later version.
-
- solidity is distributed in the hope that it will be useful,
- but WITHOUT ANY WARRANTY; without even the implied warranty of
- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- GNU General Public License for more details.
-
- You should have received a copy of the GNU General Public License
- along with solidity. If not, see <http://www.gnu.org/licenses/>.
-*/
-/**
- * @author Christian <c@ethdev.com>
- * @date 2015
- * Component that translates Solidity code into the why3 programming language.
- */
-
-#pragma once
-
-#include <libsolidity/ast/ASTVisitor.h>
-#include <libsolidity/interface/ErrorReporter.h>
-#include <string>
-
-namespace dev
-{
-namespace solidity
-{
-
-class SourceUnit;
-
-/**
- * Simple translator from Solidity to Why3.
- *
- * @todo detect side effects in sub-expressions and limit them to one per statement. #1043
- * @todo `x = y = z`
- * @todo implicit and explicit type conversion
- */
-class Why3Translator: private ASTConstVisitor
-{
-public:
- Why3Translator(ErrorReporter& _errorReporter): m_lines(std::vector<Line>{{std::string(), 0}}), m_errorReporter(_errorReporter) {}
-
- /// Appends formalisation of the given source unit to the output.
- /// @returns false on error.
- bool process(SourceUnit const& _source);
-
- std::string translation() const;
-
-private:
- /// Appends imports and constants use throughout the formal code.
- void appendPreface();
-
- /// @returns a string representation of the corresponding formal type or throws NoFormalType exception.
- std::string toFormalType(Type const& _type) const;
- using errinfo_noFormalTypeFrom = boost::error_info<struct tag_noFormalTypeFrom, std::string /* name of the type that cannot be translated */ >;
- struct NoFormalType: virtual Exception {};
-
- void error(ASTNode const& _source, std::string const& _description);
- void fatalError(ASTNode const& _source, std::string const& _description);
-
- void indent() { newLine(); m_lines.back().indentation++; }
- void unindent();
- void addLine(std::string const& _line);
- void add(std::string const& _str);
- void newLine();
- void appendSemicolon();
-
- 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 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;
- 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;
- virtual bool visit(TupleExpression const& _node) override;
- virtual void endVisit(TupleExpression const&) override { add(")"); }
- virtual bool visit(UnaryOperation const& _node) override;
- virtual bool visit(BinaryOperation const& _node) override;
- virtual bool visit(FunctionCall const& _node) override;
- virtual bool visit(MemberAccess const& _node) override;
- virtual bool visit(IndexAccess const& _node) override;
- virtual bool visit(Identifier const& _node) override;
- virtual bool visit(Literal const& _node) override;
- virtual bool visit(PragmaDirective const& _node) override;
-
- virtual bool visitNode(ASTNode const& _node) override
- {
- m_errorReporter.why3TranslatorError(_node, "Code not supported for formal verification.");
- return false;
- }
-
- 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;
-
- /// @returns a string representing an expression that is a copy of this.storage
- std::string copyOfStorage() const;
-
- /// Visits the given 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);
-
- /// True if we have already seen a contract. For now, only a single contract
- /// is supported.
- bool m_seenContract = false;
- bool m_errorOccured = false;
-
- /// 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
- {
- std::string contents;
- unsigned indentation;
- };
- std::vector<Line> m_lines;
- ErrorReporter& m_errorReporter;
-};
-
-}
-}
diff --git a/libsolidity/inlineasm/AsmCodeGen.cpp b/libsolidity/inlineasm/AsmCodeGen.cpp
index 3c7c62c6..2bbd1b70 100644
--- a/libsolidity/inlineasm/AsmCodeGen.cpp
+++ b/libsolidity/inlineasm/AsmCodeGen.cpp
@@ -121,6 +121,11 @@ public:
solAssert(false, "RETURNSUB not implemented for EVM 1.0");
}
+ virtual void appendAssemblySize() override
+ {
+ m_assembly.appendProgramSize();
+ }
+
private:
LabelID assemblyTagToIdentifier(eth::AssemblyItem const& _tag) const
{
diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp
index 8be2c8dd..e2507821 100644
--- a/libsolidity/interface/CompilerStack.cpp
+++ b/libsolidity/interface/CompilerStack.cpp
@@ -40,7 +40,6 @@
#include <libsolidity/interface/ABI.h>
#include <libsolidity/interface/Natspec.h>
#include <libsolidity/interface/GasEstimator.h>
-#include <libsolidity/formal/Why3Translator.h>
#include <libevmasm/Exceptions.h>
@@ -316,20 +315,6 @@ void CompilerStack::link()
}
}
-bool CompilerStack::prepareFormalAnalysis(ErrorReporter* _errorReporter)
-{
- if (!_errorReporter)
- _errorReporter = &m_errorReporter;
- Why3Translator translator(*_errorReporter);
- for (Source const* source: m_sourceOrder)
- if (!translator.process(*source->ast))
- return false;
-
- m_formalTranslation = translator.translation();
-
- return true;
-}
-
eth::AssemblyItems const* CompilerStack::assemblyItems(string const& _contractName) const
{
Contract const& currentContract = contract(_contractName);
diff --git a/libsolidity/interface/CompilerStack.h b/libsolidity/interface/CompilerStack.h
index f7435f0e..c51ae9c9 100644
--- a/libsolidity/interface/CompilerStack.h
+++ b/libsolidity/interface/CompilerStack.h
@@ -129,12 +129,6 @@ public:
/// @returns false on error.
bool compile(std::string const& _sourceCode, bool _optimize = false, unsigned _runs = 200);
- /// Tries to translate all source files into a language suitable for formal analysis.
- /// @param _errors list to store errors - defaults to the internal error list.
- /// @returns false on error.
- bool prepareFormalAnalysis(ErrorReporter* _errorReporter = nullptr);
- std::string const& formalTranslation() const { return m_formalTranslation; }
-
/// @returns the assembled object for a contract.
eth::LinkerObject const& object(std::string const& _contractName = "") const;
/// @returns the runtime object for the contract.
@@ -290,7 +284,6 @@ private:
std::map<ASTNode const*, std::shared_ptr<DeclarationContainer>> m_scopes;
std::vector<Source const*> m_sourceOrder;
std::map<std::string const, Contract> m_contracts;
- std::string m_formalTranslation;
ErrorList m_errorList;
ErrorReporter m_errorReporter;
bool m_metadataLiteralSources = false;
diff --git a/libsolidity/parsing/ParserBase.cpp b/libsolidity/parsing/ParserBase.cpp
index 9987b82c..5657c2c0 100644
--- a/libsolidity/parsing/ParserBase.cpp
+++ b/libsolidity/parsing/ParserBase.cpp
@@ -43,6 +43,26 @@ int ParserBase::endPosition() const
return m_scanner->currentLocation().end;
}
+Token::Value ParserBase::currentToken() const
+{
+ return m_scanner->currentToken();
+}
+
+Token::Value ParserBase::peekNextToken() const
+{
+ return m_scanner->peekNextToken();
+}
+
+std::string ParserBase::currentLiteral() const
+{
+ return m_scanner->currentLiteral();
+}
+
+Token::Value ParserBase::advance()
+{
+ return m_scanner->next();
+}
+
void ParserBase::expectToken(Token::Value _value)
{
Token::Value tok = m_scanner->currentToken();
diff --git a/libsolidity/parsing/ParserBase.h b/libsolidity/parsing/ParserBase.h
index ae56cead..5b03ab5e 100644
--- a/libsolidity/parsing/ParserBase.h
+++ b/libsolidity/parsing/ParserBase.h
@@ -23,7 +23,6 @@
#pragma once
#include <memory>
-#include <libsolidity/parsing/Scanner.h>
#include <libsolidity/parsing/Token.h>
namespace dev
@@ -51,10 +50,10 @@ protected:
///@name Helper functions
/// If current token value is not _value, throw exception otherwise advance token.
void expectToken(Token::Value _value);
- Token::Value currentToken() const { return m_scanner->currentToken(); }
- Token::Value peekNextToken() const { return m_scanner->peekNextToken(); }
- std::string currentLiteral() const { return m_scanner->currentLiteral(); }
- Token::Value advance() { return m_scanner->next(); }
+ Token::Value currentToken() const;
+ Token::Value peekNextToken() const;
+ std::string currentLiteral() const;
+ Token::Value advance();
///@}
/// Creates a @ref ParserError and annotates it with the current position and the
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 05:49:57 +0800