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

Grouping of symbolic variables in the same file and support to FixedBytes

Browse Source
This commit is contained in:
Leonardo Alt 2018-10-22 10:29:03 +02:00
parent 01566c2e1a
commit d8cbf321da
15 changed files with 160 additions and 288 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsolidity/formal/SMTChecker.cpp
View File

@ -19,8 +19,6 @@
#include <libsolidity/formal/SMTPortfolio.h>
#include <libsolidity/formal/SSAVariable.h>
#include <libsolidity/formal/SymbolicIntVariable.h>
#include <libsolidity/formal/VariableUsage.h>
#include <libsolidity/formal/SymbolicTypes.h>

2
libsolidity/formal/SMTChecker.h
View File

@ -19,7 +19,7 @@
#include <libsolidity/formal/SolverInterface.h>
#include <libsolidity/formal/SymbolicVariable.h>
#include <libsolidity/formal/SymbolicVariables.h>
#include <libsolidity/ast/ASTVisitor.h>

40
libsolidity/formal/SymbolicAddressVariable.cpp
View File

@ -1,40 +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/>.
*/
#include <libsolidity/formal/SymbolicAddressVariable.h>
#include <libsolidity/formal/SymbolicTypes.h>
using namespace std;
using namespace dev;
using namespace dev::solidity;
SymbolicAddressVariable::SymbolicAddressVariable(
string const& _uniqueName,
smt::SolverInterface& _interface
):
SymbolicIntVariable(make_shared<IntegerType>(160), _uniqueName, _interface)
{
}
void SymbolicAddressVariable::setUnknownValue()
{
auto intType = dynamic_cast<IntegerType const*>(m_type.get());
solAssert(intType, "");
m_interface.addAssertion(currentValue() >= minValue(*intType));
m_interface.addAssertion(currentValue() <= maxValue(*intType));
}

43
libsolidity/formal/SymbolicAddressVariable.h
View File

@ -1,43 +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/>.
*/
#pragma once
#include <libsolidity/formal/SymbolicIntVariable.h>
namespace dev
{
namespace solidity
{
/**
* Specialization of SymbolicVariable for Address
*/
class SymbolicAddressVariable: public SymbolicIntVariable
{
public:
SymbolicAddressVariable(
std::string const& _uniqueName,
smt::SolverInterface& _interface
);
/// Sets the variable to the full valid value range.
void setUnknownValue();
};
}
}

46
libsolidity/formal/SymbolicBoolVariable.cpp
View File

@ -1,46 +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/>.
*/
#include <libsolidity/formal/SymbolicBoolVariable.h>
using namespace std;
using namespace dev;
using namespace dev::solidity;
SymbolicBoolVariable::SymbolicBoolVariable(
TypePointer _type,
string const& _uniqueName,
smt::SolverInterface&_interface
):
SymbolicVariable(move(_type), _uniqueName, _interface)
{
solAssert(m_type->category() == Type::Category::Bool, "");
}
smt::Expression SymbolicBoolVariable::valueAtIndex(int _index) const
{
return m_interface.newBool(uniqueSymbol(_index));
}
void SymbolicBoolVariable::setZeroValue()
{
m_interface.addAssertion(currentValue() == smt::Expression(false));
}
void SymbolicBoolVariable::setUnknownValue()
{
}

49
libsolidity/formal/SymbolicBoolVariable.h
View File

@ -1,49 +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/>.
*/
#pragma once
#include <libsolidity/formal/SymbolicVariable.h>
namespace dev
{
namespace solidity
{
/**
* Specialization of SymbolicVariable for Bool
*/
class SymbolicBoolVariable: public SymbolicVariable
{
public:
SymbolicBoolVariable(
TypePointer _type,
std::string const& _uniqueName,
smt::SolverInterface& _interface
);
/// Sets the var to false.
void setZeroValue();
/// Does nothing since the SMT solver already knows the valid values for Bool.
void setUnknownValue();
protected:
smt::Expression valueAtIndex(int _index) const;
};
}
}

49
libsolidity/formal/SymbolicIntVariable.h
View File

@ -1,49 +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/>.
*/
#pragma once
#include <libsolidity/formal/SymbolicVariable.h>
namespace dev
{
namespace solidity
{
/**
* Specialization of SymbolicVariable for Integers
*/
class SymbolicIntVariable: public SymbolicVariable
{
public:
SymbolicIntVariable(
TypePointer _type,
std::string const& _uniqueName,
smt::SolverInterface& _interface
);
/// Sets the var to 0.
void setZeroValue();
/// Sets the variable to the full valid value range.
virtual void setUnknownValue();
protected:
smt::Expression valueAtIndex(int _index) const;
};
}
}

16
libsolidity/formal/SymbolicTypes.cpp
View File

@ -17,10 +17,6 @@
#include <libsolidity/formal/SymbolicTypes.h>
#include <libsolidity/formal/SymbolicBoolVariable.h>
#include <libsolidity/formal/SymbolicIntVariable.h>
#include <libsolidity/formal/SymbolicAddressVariable.h>
#include <libsolidity/ast/Types.h>
#include <memory>
@ -55,6 +51,12 @@ pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable(
var = make_shared<SymbolicIntVariable>(make_shared<IntegerType>(256), _uniqueName, _solver);
else if (isInteger(_type.category()))
var = make_shared<SymbolicIntVariable>(type, _uniqueName, _solver);
else if (isFixedBytes(_type.category()))
{
auto fixedBytesType = dynamic_cast<FixedBytesType const*>(type.get());
solAssert(fixedBytesType, "");
var = make_shared<SymbolicFixedBytesVariable>(fixedBytesType->numBytes(), _uniqueName, _solver);
}
else if (isAddress(_type.category()))
var = make_shared<SymbolicAddressVariable>(_uniqueName, _solver);
else if (isRational(_type.category()))
@ -86,6 +88,11 @@ bool dev::solidity::isRational(Type::Category _category)
return _category == Type::Category::RationalNumber;
}
bool dev::solidity::isFixedBytes(Type::Category _category)
{
return _category == Type::Category::FixedBytes;
}
bool dev::solidity::isAddress(Type::Category _category)
{
return _category == Type::Category::Address;
@ -95,6 +102,7 @@ bool dev::solidity::isNumber(Type::Category _category)
{
return isInteger(_category) ||
isRational(_category) ||
isFixedBytes(_category) ||
isAddress(_category);
}

3
libsolidity/formal/SymbolicTypes.h
View File

@ -18,7 +18,7 @@
#pragma once
#include <libsolidity/formal/SolverInterface.h>
#include <libsolidity/formal/SymbolicVariable.h>
#include <libsolidity/formal/SymbolicVariables.h>
#include <libsolidity/ast/AST.h>
#include <libsolidity/ast/Types.h>
@ -35,6 +35,7 @@ bool isSupportedType(Type const& _type);
bool isInteger(Type::Category _category);
bool isRational(Type::Category _category);
bool isFixedBytes(Type::Category _category);
bool isAddress(Type::Category _category);
bool isNumber(Type::Category _category);
bool isBool(Type::Category _category);

43
libsolidity/formal/SymbolicVariable.cpp
View File

@ -1,43 +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/>.
*/
#include <libsolidity/formal/SymbolicVariable.h>
#include <libsolidity/ast/AST.h>
using namespace std;
using namespace dev;
using namespace dev::solidity;
SymbolicVariable::SymbolicVariable(
TypePointer _type,
string const& _uniqueName,
smt::SolverInterface& _interface
):
m_type(move(_type)),
m_uniqueName(_uniqueName),
m_interface(_interface),
m_ssa(make_shared<SSAVariable>())
{
}
string SymbolicVariable::uniqueSymbol(unsigned _index) const
{
return m_uniqueName + "_" + to_string(_index);
}

62
libsolidity/formal/SymbolicIntVariable.cpp → libsolidity/formal/SymbolicVariables.cpp
View File

@ -15,14 +15,57 @@
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
#include <libsolidity/formal/SymbolicIntVariable.h>
#include <libsolidity/formal/SymbolicVariables.h>
#include <libsolidity/formal/SymbolicTypes.h>
#include <libsolidity/ast/AST.h>
using namespace std;
using namespace dev;
using namespace dev::solidity;
SymbolicVariable::SymbolicVariable(
TypePointer _type,
string const& _uniqueName,
smt::SolverInterface& _interface
):
m_type(move(_type)),
m_uniqueName(_uniqueName),
m_interface(_interface),
m_ssa(make_shared<SSAVariable>())
{
}
string SymbolicVariable::uniqueSymbol(unsigned _index) const
{
return m_uniqueName + "_" + to_string(_index);
}
SymbolicBoolVariable::SymbolicBoolVariable(
TypePointer _type,
string const& _uniqueName,
smt::SolverInterface&_interface
):
SymbolicVariable(move(_type), _uniqueName, _interface)
{
solAssert(m_type->category() == Type::Category::Bool, "");
}
smt::Expression SymbolicBoolVariable::valueAtIndex(int _index) const
{
return m_interface.newBool(uniqueSymbol(_index));
}
void SymbolicBoolVariable::setZeroValue()
{
m_interface.addAssertion(currentValue() == smt::Expression(false));
}
void SymbolicBoolVariable::setUnknownValue()
{
}
SymbolicIntVariable::SymbolicIntVariable(
TypePointer _type,
string const& _uniqueName,
@ -50,3 +93,20 @@ void SymbolicIntVariable::setUnknownValue()
m_interface.addAssertion(currentValue() >= minValue(*intType));
m_interface.addAssertion(currentValue() <= maxValue(*intType));
}
SymbolicAddressVariable::SymbolicAddressVariable(
string const& _uniqueName,
smt::SolverInterface& _interface
):
SymbolicIntVariable(make_shared<IntegerType>(160), _uniqueName, _interface)
{
}
SymbolicFixedBytesVariable::SymbolicFixedBytesVariable(
unsigned _numBytes,
string const& _uniqueName,
smt::SolverInterface& _interface
):
SymbolicIntVariable(make_shared<IntegerType>(_numBytes * 8), _uniqueName, _interface)
{
}

69
libsolidity/formal/SymbolicVariable.h → libsolidity/formal/SymbolicVariables.h
View File

@ -33,7 +33,7 @@ namespace solidity
class Type;
/**
* This class represents the symbolic version of a program variable.
* This abstract class represents the symbolic version of a program variable.
*/
class SymbolicVariable
{
@ -78,5 +78,72 @@ protected:
std::shared_ptr<SSAVariable> m_ssa = nullptr;
};
/**
* Specialization of SymbolicVariable for Bool
*/
class SymbolicBoolVariable: public SymbolicVariable
{
public:
SymbolicBoolVariable(
TypePointer _type,
std::string const& _uniqueName,
smt::SolverInterface& _interface
);
/// Sets the var to false.
void setZeroValue();
/// Does nothing since the SMT solver already knows the valid values for Bool.
void setUnknownValue();
protected:
smt::Expression valueAtIndex(int _index) const;
};
/**
* Specialization of SymbolicVariable for Integers
*/
class SymbolicIntVariable: public SymbolicVariable
{
public:
SymbolicIntVariable(
TypePointer _type,
std::string const& _uniqueName,
smt::SolverInterface& _interface
);
/// Sets the var to 0.
void setZeroValue();
/// Sets the variable to the full valid value range.
void setUnknownValue();
protected:
smt::Expression valueAtIndex(int _index) const;
};
/**
* Specialization of SymbolicVariable for Address
*/
class SymbolicAddressVariable: public SymbolicIntVariable
{
public:
SymbolicAddressVariable(
std::string const& _uniqueName,
smt::SolverInterface& _interface
);
};
/**
* Specialization of SymbolicVariable for FixedBytes
*/
class SymbolicFixedBytesVariable: public SymbolicIntVariable
{
public:
SymbolicFixedBytesVariable(
unsigned _numBytes,
std::string const& _uniqueName,
smt::SolverInterface& _interface
);
};
}
}

4
test/libsolidity/smtCheckerTests/special/blockhash.sol
View File

@ -7,8 +7,4 @@ contract C
}
}
// ----
// Warning: (86-98): Assertion checker does not yet support this special variable.
// Warning: (86-98): Assertion checker does not yet implement this type.
// Warning: (86-102): Assertion checker does not yet implement the type bytes32 for comparisons
// Warning: (86-102): Internal error: Expression undefined for SMT solver.
// Warning: (79-103): Assertion violation happens here

4
test/libsolidity/smtCheckerTests/special/msg_sig.sol
View File

@ -7,8 +7,4 @@ contract C
}
}
// ----
// Warning: (86-93): Assertion checker does not yet support this special variable.
// Warning: (86-93): Assertion checker does not yet implement this type.
// Warning: (86-107): Assertion checker does not yet implement the type bytes4 for comparisons
// Warning: (86-107): Internal error: Expression undefined for SMT solver.
// Warning: (79-108): Assertion violation happens here

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

@ -0,0 +1,16 @@
pragma experimental SMTChecker;
contract C
{
bytes32 x;
function f(bytes8 y) public view {
assert(x != y);
assert(x != g());
}
function g() public view returns (bytes32) {
return x;
}
}
// ----
// Warning: (96-110): Assertion violation happens here
// Warning: (114-130): Assertion violation happens here