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

[SMTChecker] Support to mapping

Browse Source
This commit is contained in:
Leonardo Alt 2018-11-09 17:06:30 +01:00
parent 8d3617b7c5
commit 6a2809a582
23 changed files with 358 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

92
libsolidity/formal/SMTChecker.cpp
View File

@ -60,8 +60,7 @@ void SMTChecker::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _
bool SMTChecker::visit(ContractDefinition const& _contract)
{
for (auto _var : _contract.stateVariables())
if (_var->type()->isValueType())
createVariable(*_var);
createVariable(*_var);
return true;
}
@ -271,6 +270,11 @@ void SMTChecker::endVisit(Assignment const& _assignment)
assignment(decl, _assignment.rightHandSide(), _assignment.location());
defineExpr(_assignment, expr(_assignment.rightHandSide()));
}
else if (dynamic_cast<IndexAccess const*>(&_assignment.leftHandSide()))
{
arrayAssignment(_assignment);
defineExpr(_assignment, expr(_assignment.rightHandSide()));
}
else
m_errorReporter.warning(
_assignment.location(),
@ -532,7 +536,7 @@ void SMTChecker::abstractFunctionCall(FunctionCall const& _funCall)
for (auto const& arg: _funCall.arguments())
smtArguments.push_back(expr(*arg));
defineExpr(_funCall, (*m_expressions.at(&_funCall.expression()))(smtArguments));
m_uninterpretedTerms.push_back(&_funCall);
m_uninterpretedTerms.insert(&_funCall);
setSymbolicUnknownValue(expr(_funCall), _funCall.annotation().type, *m_interface);
}
@ -638,6 +642,68 @@ bool SMTChecker::visit(MemberAccess const& _memberAccess)
return true;
}
void SMTChecker::endVisit(IndexAccess const& _indexAccess)
{
shared_ptr<SymbolicVariable> array;
if (auto const& id = dynamic_cast<Identifier const*>(&_indexAccess.baseExpression()))
{
auto const& varDecl = dynamic_cast<VariableDeclaration const&>(*id->annotation().referencedDeclaration);
solAssert(knownVariable(varDecl), "");
array = m_variables[&varDecl];
}
else if (auto const& innerAccess = dynamic_cast<IndexAccess const*>(&_indexAccess.baseExpression()))
{
solAssert(knownExpr(*innerAccess), "");
array = m_expressions[innerAccess];
}
else
{
m_errorReporter.warning(
_indexAccess.location(),
"Assertion checker does not yet implement this expression."
);
return;
}
solAssert(array, "");
defineExpr(_indexAccess, smt::Expression::select(
array->currentValue(),
expr(*_indexAccess.indexExpression())
));
setSymbolicUnknownValue(
expr(_indexAccess),
_indexAccess.annotation().type,
*m_interface
);
m_uninterpretedTerms.insert(&_indexAccess);
}
void SMTChecker::arrayAssignment(Assignment const& _assignment)
{
auto const& indexAccess = dynamic_cast<IndexAccess const&>(_assignment.leftHandSide());
if (auto const& id = dynamic_cast<Identifier const*>(&indexAccess.baseExpression()))
{
auto const& varDecl = dynamic_cast<VariableDeclaration const&>(*id->annotation().referencedDeclaration);
solAssert(knownVariable(varDecl), "");
smt::Expression store = smt::Expression::store(
m_variables[&varDecl]->currentValue(),
expr(*indexAccess.indexExpression()),
expr(_assignment.rightHandSide())
);
m_interface->addAssertion(newValue(varDecl) == store);
}
else if (dynamic_cast<IndexAccess const*>(&indexAccess.baseExpression()))
m_errorReporter.warning(
indexAccess.location(),
"Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays."
);
else
m_errorReporter.warning(
_assignment.location(),
"Assertion checker does not yet implement this expression."
);
}
void SMTChecker::defineGlobalVariable(string const& _name, Expression const& _expr, bool _increaseIndex)
{
if (!knownGlobalSymbol(_name))
@ -847,12 +913,19 @@ void SMTChecker::checkCondition(
}
for (auto const& var: m_variables)
{
expressionsToEvaluate.emplace_back(currentValue(*var.first));
expressionNames.push_back(var.first->name());
if (var.first->type()->isValueType())
{
expressionsToEvaluate.emplace_back(currentValue(*var.first));
expressionNames.push_back(var.first->name());
}
}
for (auto const& var: m_globalContext)
{
if (smtKind(var.second->type()->category()) != smt::Kind::Function)
auto const& type = var.second->type();
if (
type->isValueType() &&
smtKind(type->category()) != smt::Kind::Function
)
{
expressionsToEvaluate.emplace_back(var.second->currentValue());
expressionNames.push_back(var.first);
@ -860,8 +933,11 @@ void SMTChecker::checkCondition(
}
for (auto const& uf: m_uninterpretedTerms)
{
expressionsToEvaluate.emplace_back(expr(*uf));
expressionNames.push_back(m_scanner->sourceAt(uf->location()));
if (uf->annotation().type->isValueType())
{
expressionsToEvaluate.emplace_back(expr(*uf));
expressionNames.push_back(m_scanner->sourceAt(uf->location()));
}
}
}
smt::CheckResult result;

5
libsolidity/formal/SMTChecker.h
View File

@ -79,6 +79,7 @@ private:
void endVisit(Literal const& _node) override;
void endVisit(Return const& _node) override;
bool visit(MemberAccess const& _node) override;
void endVisit(IndexAccess const& _node) override;
void arithmeticOperation(BinaryOperation const& _op);
void compareOperation(BinaryOperation const& _op);
@ -96,6 +97,7 @@ private:
void defineGlobalVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false);
void defineGlobalFunction(std::string const& _name, Expression const& _expr);
void arrayAssignment(Assignment const& _assignment);
/// Division expression in the given type. Requires special treatment because
/// of rounding for signed division.
@ -209,8 +211,9 @@ private:
std::unordered_map<VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables;
std::unordered_map<std::string, std::shared_ptr<SymbolicVariable>> m_globalContext;
/// Stores the instances of an Uninterpreted Function applied to arguments.
/// These may be direct application of UFs or Array index access.
/// Used to retrieve models.
std::vector<Expression const*> m_uninterpretedTerms;
std::set<Expression const*> m_uninterpretedTerms;
std::vector<smt::Expression> m_pathConditions;
langutil::ErrorReporter& m_errorReporter;
std::shared_ptr<langutil::Scanner> m_scanner;

15
libsolidity/formal/SolverInterface.h
View File

@ -80,6 +80,8 @@ struct FunctionSort: public Sort
[&](SortPointer _a, SortPointer _b) { return *_a == *_b; }
))
return false;
solAssert(codomain, "");
solAssert(_otherFunction->codomain, "");
return *codomain == *_otherFunction->codomain;
}
@ -99,6 +101,10 @@ struct ArraySort: public Sort
return false;
auto _otherArray = dynamic_cast<ArraySort const*>(&_other);
solAssert(_otherArray, "");
solAssert(_otherArray->domain, "");
solAssert(_otherArray->range, "");
solAssert(domain, "");
solAssert(range, "");
return *domain == *_otherArray->domain && *range == *_otherArray->range;
}
@ -161,8 +167,9 @@ public:
static Expression select(Expression _array, Expression _index)
{
solAssert(_array.sort->kind == Kind::Array, "");
auto const& arraySort = dynamic_cast<ArraySort const*>(_array.sort.get());
std::shared_ptr<ArraySort> arraySort = std::dynamic_pointer_cast<ArraySort>(_array.sort);
solAssert(arraySort, "");
solAssert(_index.sort, "");
solAssert(*arraySort->domain == *_index.sort, "");
return Expression(
"select",
@ -176,14 +183,16 @@ public:
static Expression store(Expression _array, Expression _index, Expression _element)
{
solAssert(_array.sort->kind == Kind::Array, "");
auto const& arraySort = dynamic_cast<ArraySort const*>(_array.sort.get());
std::shared_ptr<ArraySort> arraySort = std::dynamic_pointer_cast<ArraySort>(_array.sort);
solAssert(arraySort, "");
solAssert(_index.sort, "");
solAssert(_element.sort, "");
solAssert(*arraySort->domain == *_index.sort, "");
solAssert(*arraySort->range == *_element.sort, "");
return Expression(
"store",
std::vector<Expression>{std::move(_array), std::move(_index), std::move(_element)},
_array.sort
arraySort
);
}

22
libsolidity/formal/SymbolicTypes.cpp
View File

@ -52,13 +52,19 @@ smt::SortPointer dev::solidity::smtSort(Type const& _type)
}
case smt::Kind::Array:
{
solUnimplementedAssert(false, "Invalid type");
if (isMapping(_type.category()))
{
auto mapType = dynamic_cast<MappingType const*>(&_type);
solAssert(mapType, "");
return make_shared<smt::ArraySort>(smtSort(*mapType->keyType()), smtSort(*mapType->valueType()));
}
// TODO Solidity array
return make_shared<smt::Sort>(smt::Kind::Int);
}
default:
// Abstract case.
return make_shared<smt::Sort>(smt::Kind::Int);
}
solAssert(false, "Invalid type");
}
vector<smt::SortPointer> dev::solidity::smtSort(vector<TypePointer> const& _types)
@ -77,6 +83,8 @@ smt::Kind dev::solidity::smtKind(Type::Category _category)
return smt::Kind::Bool;
else if (isFunction(_category))
return smt::Kind::Function;
else if (isMapping(_category))
return smt::Kind::Array;
// Abstract case.
return smt::Kind::Int;
}
@ -84,7 +92,8 @@ smt::Kind dev::solidity::smtKind(Type::Category _category)
bool dev::solidity::isSupportedType(Type::Category _category)
{
return isNumber(_category) ||
isBool(_category);
isBool(_category) ||
isMapping(_category);
}
bool dev::solidity::isSupportedTypeDeclaration(Type::Category _category)
@ -130,6 +139,8 @@ pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable(
else
var = make_shared<SymbolicIntVariable>(type, _uniqueName, _solver);
}
else if (isMapping(_type.category()))
var = make_shared<SymbolicMappingVariable>(type, _uniqueName, _solver);
else
solAssert(false, "");
return make_pair(abstract, var);
@ -183,6 +194,11 @@ bool dev::solidity::isFunction(Type::Category _category)
return _category == Type::Category::Function;
}
bool dev::solidity::isMapping(Type::Category _category)
{
return _category == Type::Category::Mapping;
}
smt::Expression dev::solidity::minValue(IntegerType const& _type)
{
return smt::Expression(_type.minValue());

1
libsolidity/formal/SymbolicTypes.h
View File

@ -48,6 +48,7 @@ bool isAddress(Type::Category _category);
bool isNumber(Type::Category _category);
bool isBool(Type::Category _category);
bool isFunction(Type::Category _category);
bool isMapping(Type::Category _category);
/// Returns a new symbolic variable, according to _type.
/// Also returns whether the type is abstract or not,

10
libsolidity/formal/SymbolicVariables.cpp
View File

@ -127,3 +127,13 @@ smt::Expression SymbolicFunctionVariable::operator()(vector<smt::Expression> _ar
{
return m_declaration(_arguments);
}
SymbolicMappingVariable::SymbolicMappingVariable(
TypePointer _type,
string const& _uniqueName,
smt::SolverInterface& _interface
):
SymbolicVariable(move(_type), _uniqueName, _interface)
{
solAssert(isMapping(m_type->category()), "");
}

13
libsolidity/formal/SymbolicVariables.h
View File

@ -143,5 +143,18 @@ private:
smt::Expression m_declaration;
};
/**
* Specialization of SymbolicVariable for Mapping
*/
class SymbolicMappingVariable: public SymbolicVariable
{
public:
SymbolicMappingVariable(
TypePointer _type,
std::string const& _uniqueName,
smt::SolverInterface& _interface
);
};
}
}

10
test/libsolidity/smtCheckerTests/types/mapping_1.sol Normal file
View File

@ -0,0 +1,10 @@
pragma experimental SMTChecker;
contract C
{
mapping (uint => uint) map;
function f(uint x) public {
map[2] = x;
assert(x == map[2]);
}
}

13
test/libsolidity/smtCheckerTests/types/mapping_1_fail.sol Normal file
View File

@ -0,0 +1,13 @@
pragma experimental SMTChecker;
contract C
{
mapping (uint => uint) map;
function f(uint x) public {
map[2] = x;
map[2] = 3;
assert(x != map[2]);
}
}
// ----
// Warning: (134-153): Assertion violation happens here

11
test/libsolidity/smtCheckerTests/types/mapping_2.sol Normal file
View File

@ -0,0 +1,11 @@
pragma experimental SMTChecker;
contract C
{
mapping (uint => bool) map;
function f(bool x) public view {
assert(x != map[2]);
}
}
// ----
// Warning: (111-130): Assertion violation happens here

14
test/libsolidity/smtCheckerTests/types/mapping_2d_1.sol Normal file
View File

@ -0,0 +1,14 @@
pragma experimental SMTChecker;
contract C
{
mapping (uint => mapping (uint => uint)) map;
function f(uint x) public {
x = 42;
map[13][14] = 42;
assert(x == map[13][14]);
}
}
// ----
// Warning: (134-145): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
// Warning: (154-178): Assertion violation happens here

14
test/libsolidity/smtCheckerTests/types/mapping_2d_1_fail.sol Normal file
View File

@ -0,0 +1,14 @@
pragma experimental SMTChecker;
contract C
{
mapping (uint => mapping (uint => uint)) map;
function f(uint x) public {
x = 41;
map[13][14] = 42;
assert(x == map[13][14]);
}
}
// ----
// Warning: (134-145): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
// Warning: (154-178): Assertion violation happens here

12
test/libsolidity/smtCheckerTests/types/mapping_3.sol Normal file
View File

@ -0,0 +1,12 @@
pragma experimental SMTChecker;
contract C
{
mapping (uint => uint) map;
function f() public {
map[1] = 111;
uint x = map[2];
map[1] = 112;
assert(map[2] == x);
}
}

14
test/libsolidity/smtCheckerTests/types/mapping_3d_1.sol Normal file
View File

@ -0,0 +1,14 @@
pragma experimental SMTChecker;
contract C
{
mapping (uint => mapping (uint => mapping (uint => uint))) map;
function f(uint x) public {
x = 42;
map[13][14][15] = 42;
assert(x == map[13][14][15]);
}
}
// ----
// Warning: (152-167): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
// Warning: (176-204): Assertion violation happens here

14
test/libsolidity/smtCheckerTests/types/mapping_3d_1_fail.sol Normal file
View File

@ -0,0 +1,14 @@
pragma experimental SMTChecker;
contract C
{
mapping (uint => mapping (uint => mapping (uint => uint))) map;
function f(uint x) public {
x = 41;
map[13][14][15] = 42;
assert(x == map[13][14][15]);
}
}
// ----
// Warning: (152-167): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
// Warning: (176-204): Assertion violation happens here

12
test/libsolidity/smtCheckerTests/types/mapping_4.sol Normal file
View File

@ -0,0 +1,12 @@
pragma experimental SMTChecker;
contract C
{
mapping (bool => bool) map;
function f(bool x) public view {
require(x);
assert(x != map[x]);
}
}
// ----
// Warning: (125-144): Assertion violation happens here

11
test/libsolidity/smtCheckerTests/types/mapping_5.sol Normal file
View File

@ -0,0 +1,11 @@
pragma experimental SMTChecker;
contract C
{
mapping (address => uint) map;
function f(address a, uint x) public view {
assert(x != map[a]);
}
}
// ----
// Warning: (125-144): Assertion violation happens here

15
test/libsolidity/smtCheckerTests/types/mapping_aliasing_1.sol Normal file
View File

@ -0,0 +1,15 @@
pragma experimental SMTChecker;
contract C
{
mapping (uint => uint) a;
mapping (uint => uint) b;
function f() public {
require(a[1] == b[1]);
mapping (uint => uint) storage c = a;
c[1] = 2;
// False negative! Needs aliasing.
assert(a[1] == b[1]);
}
}

21
test/libsolidity/smtCheckerTests/types/mapping_as_local_var_1.sol Normal file
View File

@ -0,0 +1,21 @@
pragma experimental SMTChecker;
contract c {
mapping(uint => uint) x;
mapping(uint => uint) y;
function f(bool cond) public {
mapping(uint => uint) storage a = cond ? x : y;
x[2] = 1;
y[2] = 2;
a[2] = 3;
// False positive since aliasing is not yet supported.
if (cond)
assert(a[2] == x[2] && a[2] != y[2]);
else
assert(a[2] == y[2] && a[2] != x[2]);
}
}
// ----
// Warning: (166-178): Internal error: Expression undefined for SMT solver.
// Warning: (288-324): Assertion violation happens here
// Warning: (336-372): Assertion violation happens here

15
test/libsolidity/smtCheckerTests/types/mapping_as_parameter_1.sol Normal file
View File

@ -0,0 +1,15 @@
pragma experimental SMTChecker;
contract c {
mapping(uint => uint) x;
function f(mapping(uint => uint) storage map, uint index, uint value) internal {
map[index] = value;
}
function g(uint a, uint b) public {
f(x, a, b);
// False positive since aliasing is not yet supported.
assert(x[a] == b);
}
}
// ----
// Warning: (289-306): Assertion violation happens here

10
test/libsolidity/smtCheckerTests/types/mapping_equal_keys_1.sol Normal file
View File

@ -0,0 +1,10 @@
pragma experimental SMTChecker;
contract C
{
mapping (uint => uint) map;
function f(uint x, uint y) public view {
require(x == y);
assert(map[x] == map[y]);
}
}

12
test/libsolidity/smtCheckerTests/types/mapping_equal_keys_2.sol Normal file
View File

@ -0,0 +1,12 @@
pragma experimental SMTChecker;
contract C
{
mapping (uint => uint) map;
function f(uint x, uint y) public view {
assert(x == y);
assert(map[x] == map[y]);
}
}
// ----
// Warning: (119-133): Assertion violation happens here

17
test/libsolidity/smtCheckerTests/types/mapping_unsupported_key_type_1.sol Normal file
View File

@ -0,0 +1,17 @@
pragma experimental SMTChecker;
contract C
{
mapping (string => uint) map;
function f(string memory s, uint x) public {
map[s] = x;
assert(x == map[s]);
}
}
// ----
// Warning: (89-104): Assertion checker does not yet support the type of this variable.
// Warning: (129-130): Internal error: Expression undefined for SMT solver.
// Warning: (129-130): Assertion checker does not yet implement this type.
// Warning: (155-156): Internal error: Expression undefined for SMT solver.
// Warning: (155-156): Assertion checker does not yet implement this type.
// Warning: (139-158): Assertion violation happens here