cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #5454 from ethereum/smt_math_functions

Browse Source 
[SMTChecker] Abstract math functions
This commit is contained in:
chriseth 2018-12-11 18:35:10 +01:00 committed by GitHub
commit 9f86ede32d
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
11 changed files with 172 additions and 106 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -7,6 +7,7 @@ Compiler Features:
* Inline Assembly: Improve error messages around invalid function argument count.
* Code Generator: Use codecopy for string constants more aggressively.
* Code Generator: Use binary search for dispatch function if more efficient. The size/speed tradeoff can be tuned using ``--optimize-runs``.
* SMTChecker: Support mathematical and cryptographic functions in an uninterpreted way.
* Type Checker: Add an additional reason to be displayed when type conversion fails.

157
libsolidity/formal/SMTChecker.cpp
View File

@ -90,8 +90,7 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
m_interface->reset();
m_pathConditions.clear();
m_expressions.clear();
m_specialVariables.clear();
m_uninterpretedFunctions.clear();
m_globalContext.clear();
m_uninterpretedTerms.clear();
resetStateVariables();
initializeLocalVariables(_function);
@ -268,16 +267,9 @@ void SMTChecker::endVisit(Assignment const& _assignment)
else if (Identifier const* identifier = dynamic_cast<Identifier const*>(&_assignment.leftHandSide()))
{
VariableDeclaration const& decl = dynamic_cast<VariableDeclaration const&>(*identifier->annotation().referencedDeclaration);
if (knownVariable(decl))
{
assignment(decl, _assignment.rightHandSide(), _assignment.location());
defineExpr(_assignment, expr(_assignment.rightHandSide()));
}
else
m_errorReporter.warning(
_assignment.location(),
"Assertion checker does not yet implement such assignments."
);
solAssert(knownVariable(decl), "");
assignment(decl, _assignment.rightHandSide(), _assignment.location());
defineExpr(_assignment, expr(_assignment.rightHandSide()));
}
else
m_errorReporter.warning(
@ -288,7 +280,11 @@ void SMTChecker::endVisit(Assignment const& _assignment)
void SMTChecker::endVisit(TupleExpression const& _tuple)
{
if (_tuple.isInlineArray() || _tuple.components().size() != 1)
if (
_tuple.isInlineArray() ||
_tuple.components().size() != 1 ||
!isSupportedType(_tuple.components()[0]->annotation().type->category())
)
m_errorReporter.warning(
_tuple.location(),
"Assertion checker does not yet implement tuples and inline arrays."
@ -399,18 +395,30 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
std::vector<ASTPointer<Expression const>> const args = _funCall.arguments();
if (funType.kind() == FunctionType::Kind::Assert)
visitAssert(_funCall);
else if (funType.kind() == FunctionType::Kind::Require)
visitRequire(_funCall);
else if (funType.kind() == FunctionType::Kind::GasLeft)
visitGasLeft(_funCall);
else if (funType.kind() == FunctionType::Kind::BlockHash)
visitBlockHash(_funCall);
else if (funType.kind() == FunctionType::Kind::Internal)
inlineFunctionCall(_funCall);
else
switch (funType.kind())
{
case FunctionType::Kind::Assert:
visitAssert(_funCall);
break;
case FunctionType::Kind::Require:
visitRequire(_funCall);
break;
case FunctionType::Kind::GasLeft:
visitGasLeft(_funCall);
break;
case FunctionType::Kind::Internal:
inlineFunctionCall(_funCall);
break;
case FunctionType::Kind::KECCAK256:
case FunctionType::Kind::ECRecover:
case FunctionType::Kind::SHA256:
case FunctionType::Kind::RIPEMD160:
case FunctionType::Kind::BlockHash:
case FunctionType::Kind::AddMod:
case FunctionType::Kind::MulMod:
abstractFunctionCall(_funCall);
break;
default:
m_errorReporter.warning(
_funCall.location(),
"Assertion checker does not yet implement this type of function call."
@ -442,8 +450,8 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
string gasLeft = "gasleft()";
// We increase the variable index since gasleft changes
// inside a tx.
defineSpecialVariable(gasLeft, _funCall, true);
auto const& symbolicVar = m_specialVariables.at(gasLeft);
defineGlobalVariable(gasLeft, _funCall, true);
auto const& symbolicVar = m_globalContext.at(gasLeft);
unsigned index = symbolicVar->index();
// We set the current value to unknown anyway to add type constraints.
setUnknownValue(*symbolicVar);
@ -451,21 +459,6 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
m_interface->addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1));
}
void SMTChecker::visitBlockHash(FunctionCall const& _funCall)
{
string blockHash = "blockhash";
auto const& arguments = _funCall.arguments();
solAssert(arguments.size() == 1, "");
smt::SortPointer paramSort = smtSort(*arguments.at(0)->annotation().type);
smt::SortPointer returnSort = smtSort(*_funCall.annotation().type);
defineUninterpretedFunction(
blockHash,
make_shared<smt::FunctionSort>(vector<smt::SortPointer>{paramSort}, returnSort)
);
defineExpr(_funCall, m_uninterpretedFunctions.at(blockHash)({expr(*arguments.at(0))}));
m_uninterpretedTerms.push_back(&_funCall);
}
void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
{
FunctionDefinition const* _funDef = nullptr;
@ -533,29 +526,32 @@ void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
}
}
void SMTChecker::abstractFunctionCall(FunctionCall const& _funCall)
{
vector<smt::Expression> smtArguments;
for (auto const& arg: _funCall.arguments())
smtArguments.push_back(expr(*arg));
defineExpr(_funCall, (*m_expressions.at(&_funCall.expression()))(smtArguments));
m_uninterpretedTerms.push_back(&_funCall);
setSymbolicUnknownValue(expr(_funCall), _funCall.annotation().type, *m_interface);
}
void SMTChecker::endVisit(Identifier const& _identifier)
{
if (_identifier.annotation().lValueRequested)
{
// Will be translated as part of the node that requested the lvalue.
}
else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
else if (dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
{
if (
fun->kind() == FunctionType::Kind::Assert ||
fun->kind() == FunctionType::Kind::Require ||
fun->kind() == FunctionType::Kind::GasLeft ||
fun->kind() == FunctionType::Kind::BlockHash
)
return;
createExpr(_identifier);
visitFunctionIdentifier(_identifier);
}
else if (isSupportedType(_identifier.annotation().type->category()))
{
if (VariableDeclaration const* decl = dynamic_cast<VariableDeclaration const*>(_identifier.annotation().referencedDeclaration))
defineExpr(_identifier, currentValue(*decl));
else if (_identifier.name() == "now")
defineSpecialVariable(_identifier.name(), _identifier);
defineGlobalVariable(_identifier.name(), _identifier);
else
// TODO: handle MagicVariableDeclaration here
m_errorReporter.warning(
@ -565,6 +561,20 @@ void SMTChecker::endVisit(Identifier const& _identifier)
}
}
void SMTChecker::visitFunctionIdentifier(Identifier const& _identifier)
{
auto const& fType = dynamic_cast<FunctionType const&>(*_identifier.annotation().type);
if (fType.returnParameterTypes().size() > 1)
{
m_errorReporter.warning(
_identifier.location(),
"Assertion checker does not yet support functions with more than one return parameter."
);
}
defineGlobalFunction(fType.richIdentifier(), _identifier);
m_expressions.emplace(&_identifier, m_globalContext.at(fType.richIdentifier()));
}
void SMTChecker::endVisit(Literal const& _literal)
{
Type const& type = *_literal.annotation().type;
@ -616,7 +626,7 @@ bool SMTChecker::visit(MemberAccess const& _memberAccess)
_memberAccess.location(),
"Assertion checker does not yet support this expression."
);
defineSpecialVariable(accessedName + "." + _memberAccess.memberName(), _memberAccess);
defineGlobalVariable(accessedName + "." + _memberAccess.memberName(), _memberAccess);
return false;
}
else
@ -628,30 +638,39 @@ bool SMTChecker::visit(MemberAccess const& _memberAccess)
return true;
}
void SMTChecker::defineSpecialVariable(string const& _name, Expression const& _expr, bool _increaseIndex)
void SMTChecker::defineGlobalVariable(string const& _name, Expression const& _expr, bool _increaseIndex)
{
if (!knownSpecialVariable(_name))
if (!knownGlobalSymbol(_name))
{
auto result = newSymbolicVariable(*_expr.annotation().type, _name, *m_interface);
m_specialVariables.emplace(_name, result.second);
m_globalContext.emplace(_name, result.second);
setUnknownValue(*result.second);
if (result.first)
m_errorReporter.warning(
_expr.location(),
"Assertion checker does not yet support this special variable."
"Assertion checker does not yet support this global variable."
);
}
else if (_increaseIndex)
m_specialVariables.at(_name)->increaseIndex();
m_globalContext.at(_name)->increaseIndex();
// The default behavior is not to increase the index since
// most of the special values stay the same throughout a tx.
defineExpr(_expr, m_specialVariables.at(_name)->currentValue());
// most of the global values stay the same throughout a tx.
if (isSupportedType(_expr.annotation().type->category()))
defineExpr(_expr, m_globalContext.at(_name)->currentValue());
}
void SMTChecker::defineUninterpretedFunction(string const& _name, smt::SortPointer _sort)
void SMTChecker::defineGlobalFunction(string const& _name, Expression const& _expr)
{
if (!m_uninterpretedFunctions.count(_name))
m_uninterpretedFunctions.emplace(_name, m_interface->newVariable(_name, _sort));
if (!knownGlobalSymbol(_name))
{
auto result = newSymbolicVariable(*_expr.annotation().type, _name, *m_interface);
m_globalContext.emplace(_name, result.second);
if (result.first)
m_errorReporter.warning(
_expr.location(),
"Assertion checker does not yet support the type of this function."
);
}
}
void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
@ -831,10 +850,13 @@ void SMTChecker::checkCondition(
expressionsToEvaluate.emplace_back(currentValue(*var.first));
expressionNames.push_back(var.first->name());
}
for (auto const& var: m_specialVariables)
for (auto const& var: m_globalContext)
{
expressionsToEvaluate.emplace_back(var.second->currentValue());
expressionNames.push_back(var.first);
if (smtKind(var.second->type()->category()) != smt::Kind::Function)
{
expressionsToEvaluate.emplace_back(var.second->currentValue());
expressionNames.push_back(var.first);
}
}
for (auto const& uf: m_uninterpretedTerms)
{
@ -1147,9 +1169,9 @@ bool SMTChecker::knownExpr(Expression const& _e) const
return m_expressions.count(&_e);
}
bool SMTChecker::knownSpecialVariable(string const& _var) const
bool SMTChecker::knownGlobalSymbol(string const& _var) const
{
return m_specialVariables.count(_var);
return m_globalContext.count(_var);
}
void SMTChecker::createExpr(Expression const& _e)
@ -1172,6 +1194,7 @@ void SMTChecker::createExpr(Expression const& _e)
void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value)
{
createExpr(_e);
solAssert(isSupportedType(*_e.annotation().type), "Equality operator applied to type that is not fully supported");
m_interface->addAssertion(expr(_e) == _value);
}

24
libsolidity/formal/SMTChecker.h
View File

@ -84,16 +84,18 @@ private:
void compareOperation(BinaryOperation const& _op);
void booleanOperation(BinaryOperation const& _op);
void visitAssert(FunctionCall const&);
void visitRequire(FunctionCall const&);
void visitGasLeft(FunctionCall const&);
void visitBlockHash(FunctionCall const&);
void visitAssert(FunctionCall const& _funCall);
void visitRequire(FunctionCall const& _funCall);
void visitGasLeft(FunctionCall const& _funCall);
/// Visits the FunctionDefinition of the called function
/// if available and inlines the return value.
void inlineFunctionCall(FunctionCall const&);
void inlineFunctionCall(FunctionCall const& _funCall);
/// Creates an uninterpreted function call.
void abstractFunctionCall(FunctionCall const& _funCall);
void visitFunctionIdentifier(Identifier const& _identifier);
void defineSpecialVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false);
void defineUninterpretedFunction(std::string const& _name, smt::SortPointer _sort);
void defineGlobalVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false);
void defineGlobalFunction(std::string const& _name, Expression const& _expr);
/// Division expression in the given type. Requires special treatment because
/// of rounding for signed division.
@ -176,8 +178,8 @@ private:
/// Creates the expression and sets its value.
void defineExpr(Expression const& _e, smt::Expression _value);
/// Checks if special variable was seen.
bool knownSpecialVariable(std::string const& _var) const;
/// Checks if special variable or function was seen.
bool knownGlobalSymbol(std::string const& _var) const;
/// Adds a new path condition
void pushPathCondition(smt::Expression const& _e);
@ -205,9 +207,7 @@ private:
/// repeated calls to the same function.
std::unordered_map<Expression const*, std::shared_ptr<SymbolicVariable>> m_expressions;
std::unordered_map<VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables;
std::unordered_map<std::string, std::shared_ptr<SymbolicVariable>> m_specialVariables;
/// Stores the declaration of an Uninterpreted Function.
std::unordered_map<std::string, smt::Expression> m_uninterpretedFunctions;
std::unordered_map<std::string, std::shared_ptr<SymbolicVariable>> m_globalContext;
/// Stores the instances of an Uninterpreted Function applied to arguments.
/// Used to retrieve models.
std::vector<Expression const*> m_uninterpretedTerms;

37
libsolidity/formal/SymbolicTypes.cpp
View File

@ -38,15 +38,25 @@ smt::SortPointer dev::solidity::smtSort(Type const& _type)
solAssert(fType, "");
vector<smt::SortPointer> parameterSorts = smtSort(fType->parameterTypes());
auto returnTypes = fType->returnParameterTypes();
// TODO remove this when we support tuples.
solAssert(returnTypes.size() == 1, "");
smt::SortPointer returnSort = smtSort(*returnTypes.at(0));
smt::SortPointer returnSort;
// TODO change this when we support tuples.
if (returnTypes.size() == 0)
// We cannot declare functions without a return sort, so we use the smallest.
returnSort = make_shared<smt::Sort>(smt::Kind::Bool);
else if (returnTypes.size() > 1)
// Abstract sort.
returnSort = make_shared<smt::Sort>(smt::Kind::Int);
else
returnSort = smtSort(*returnTypes.at(0));
return make_shared<smt::FunctionSort>(parameterSorts, returnSort);
}
case smt::Kind::Array:
{
solUnimplementedAssert(false, "Invalid type");
}
default:
// Abstract case.
return make_shared<smt::Sort>(smt::Kind::Int);
}
solAssert(false, "Invalid type");
}
@ -65,13 +75,21 @@ smt::Kind dev::solidity::smtKind(Type::Category _category)
return smt::Kind::Int;
else if (isBool(_category))
return smt::Kind::Bool;
solAssert(false, "Invalid type");
else if (isFunction(_category))
return smt::Kind::Function;
// Abstract case.
return smt::Kind::Int;
}
bool dev::solidity::isSupportedType(Type::Category _category)
{
return isNumber(_category) ||
isBool(_category) ||
isBool(_category);
}
bool dev::solidity::isSupportedTypeDeclaration(Type::Category _category)
{
return isSupportedType(_category) ||
isFunction(_category);
}
@ -84,7 +102,7 @@ pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable(
bool abstract = false;
shared_ptr<SymbolicVariable> var;
TypePointer type = _type.shared_from_this();
if (!isSupportedType(_type))
if (!isSupportedTypeDeclaration(_type))
{
abstract = true;
var = make_shared<SymbolicIntVariable>(make_shared<IntegerType>(256), _uniqueName, _solver);
@ -92,7 +110,7 @@ pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable(
else if (isBool(_type.category()))
var = make_shared<SymbolicBoolVariable>(type, _uniqueName, _solver);
else if (isFunction(_type.category()))
var = make_shared<SymbolicIntVariable>(make_shared<IntegerType>(256), _uniqueName, _solver);
var = make_shared<SymbolicFunctionVariable>(type, _uniqueName, _solver);
else if (isInteger(_type.category()))
var = make_shared<SymbolicIntVariable>(type, _uniqueName, _solver);
else if (isFixedBytes(_type.category()))
@ -122,6 +140,11 @@ bool dev::solidity::isSupportedType(Type const& _type)
return isSupportedType(_type.category());
}
bool dev::solidity::isSupportedTypeDeclaration(Type const& _type)
{
return isSupportedTypeDeclaration(_type.category());
}
bool dev::solidity::isInteger(Type::Category _category)
{
return _category == Type::Category::Integer;

6
libsolidity/formal/SymbolicTypes.h
View File

@ -34,10 +34,12 @@ std::vector<smt::SortPointer> smtSort(std::vector<TypePointer> const& _types);
/// Returns the SMT kind that models the Solidity type type category _category.
smt::Kind smtKind(Type::Category _category);
/// So far int, bool and address are supported.
/// Returns true if type is supported.
/// Returns true if type is fully supported (declaration and operations).
bool isSupportedType(Type::Category _category);
bool isSupportedType(Type const& _type);
/// Returns true if type is partially supported (declaration).
bool isSupportedTypeDeclaration(Type::Category _category);
bool isSupportedTypeDeclaration(Type const& _type);
bool isInteger(Type::Category _category);
bool isRational(Type::Category _category);

1
test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple.sol
View File

@ -12,3 +12,4 @@ contract C
}
// ----
// Warning: (153-156): Assertion checker does not yet implement tuples and inline arrays.

1
test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol
View File

@ -12,4 +12,5 @@ contract C
}
// ----
// Warning: (153-156): Assertion checker does not yet implement tuples and inline arrays.
// Warning: (163-176): Assertion violation happens here

3
test/libsolidity/smtCheckerTests/special/msg_data.sol
View File

@ -8,7 +8,6 @@ contract C
}
// ----
// Warning: (86-101): Assertion checker does not yet support this expression.
// Warning: (86-94): Assertion checker does not yet support this special variable.
// Warning: (86-94): Assertion checker does not yet implement this type.
// Warning: (86-94): Assertion checker does not yet support this global variable.
// Warning: (86-101): Internal error: Expression undefined for SMT solver.
// Warning: (79-106): Assertion violation happens here

16
test/libsolidity/smtCheckerTests/types/bytes_1.sol Normal file
View File

@ -0,0 +1,16 @@
pragma experimental SMTChecker;
contract C
{
function f(bytes memory b) public pure returns (bytes memory) {
bytes memory c = b;
return b;
}
}
// ----
// Warning: (113-127): Unused local variable.
// Warning: (113-127): Assertion checker does not yet support the type of this variable.
// Warning: (58-72): Assertion checker does not yet support the type of this variable.
// Warning: (95-107): Assertion checker does not yet support the type of this variable.
// Warning: (130-131): Internal error: Expression undefined for SMT solver.
// Warning: (130-131): Assertion checker does not yet implement this type.

18
test/libsolidity/smtCheckerTestsJSON/multi.json
View File

@ -1,11 +1,11 @@
{
"auxiliaryInput":
{
"smtlib2responses":
{
"0x0426cd198d1e7123a28ffac2b759a666b86508ad046babf5166500dd6d8ed308": "unsat\n(error \"line 31 column 26: model is not available\")",
"0xa51ca41ae407f5a727f27101cbc079834743cc8955f9f585582034ca634953f6": "sat\n((|EVALEXPR_0| 1))",
"0xe9477f683ff20aa57fcb08682150f86c5917e1d4c0686b278ab9b73446d0682c": "sat\n((|EVALEXPR_0| 0))"
}
}
"auxiliaryInput":
{
"smtlib2responses":
{
"0x47826ec8b83cfec30171b34f944aed6c33ecd12f02b9ad522ca45317c9bd5f45": "sat\n((|EVALEXPR_0| 1))",
"0x734c058efe9d6ec224de3cf2bdfa6c936a1c9c159c040c128d631145b2fed195": "unsat\n",
"0xa0c072acdbe5181dd56cbad8960cb5bb0b9e97fd598cfd895467bd73bbcca028": "sat\n((|EVALEXPR_0| 0))"
}
}
}

14
test/libsolidity/smtCheckerTestsJSON/simple.json
View File

@ -1,9 +1,9 @@
{
"auxiliaryInput":
{
"smtlib2responses":
{
"0xe9477f683ff20aa57fcb08682150f86c5917e1d4c0686b278ab9b73446d0682c": "sat\n((|EVALEXPR_0| 0))"
}
}
"auxiliaryInput":
{
"smtlib2responses":
{
"0xa0c072acdbe5181dd56cbad8960cb5bb0b9e97fd598cfd895467bd73bbcca028": "sat\n((|EVALEXPR_0| 0))\n"
}
}
}