cerc-io/solidity
15
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

Move VerificationTarget and add BMCVerificationTarget

Browse Source
This commit is contained in:
Leonardo Alt 2020-02-11 22:09:45 -03:00
parent ba576bc6c3
commit 6451a4d2a0
3 changed files with 29 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
libsolidity/formal/BMC.cpp
View File

@ -575,7 +575,7 @@ void BMC::checkVerificationTargets(smt::Expression const& _constraints)
checkVerificationTarget(target, _constraints);
}
void BMC::checkVerificationTarget(VerificationTarget& _target, smt::Expression const& _constraints)
void BMC::checkVerificationTarget(BMCVerificationTarget& _target, smt::Expression const& _constraints)
{
switch (_target.type)
{
@ -606,7 +606,7 @@ void BMC::checkVerificationTarget(VerificationTarget& _target, smt::Expression c
}
}
void BMC::checkConstantCondition(VerificationTarget& _target)
void BMC::checkConstantCondition(BMCVerificationTarget& _target)
{
checkBooleanNotConstant(
*_target.expression,
@ -617,7 +617,7 @@ void BMC::checkConstantCondition(VerificationTarget& _target)
);
}
void BMC::checkUnderflow(VerificationTarget& _target, smt::Expression const& _constraints)
void BMC::checkUnderflow(BMCVerificationTarget& _target, smt::Expression const& _constraints)
{
solAssert(
_target.type == VerificationTarget::Type::Underflow ||
@ -637,7 +637,7 @@ void BMC::checkUnderflow(VerificationTarget& _target, smt::Expression const& _co
);
}
void BMC::checkOverflow(VerificationTarget& _target, smt::Expression const& _constraints)
void BMC::checkOverflow(BMCVerificationTarget& _target, smt::Expression const& _constraints)
{
solAssert(
_target.type == VerificationTarget::Type::Overflow ||
@ -657,7 +657,7 @@ void BMC::checkOverflow(VerificationTarget& _target, smt::Expression const& _con
);
}
void BMC::checkDivByZero(VerificationTarget& _target)
void BMC::checkDivByZero(BMCVerificationTarget& _target)
{
solAssert(_target.type == VerificationTarget::Type::DivByZero, "");
checkCondition(
@ -671,7 +671,7 @@ void BMC::checkDivByZero(VerificationTarget& _target)
);
}
void BMC::checkBalance(VerificationTarget& _target)
void BMC::checkBalance(BMCVerificationTarget& _target)
{
solAssert(_target.type == VerificationTarget::Type::Balance, "");
checkCondition(
@ -684,7 +684,7 @@ void BMC::checkBalance(VerificationTarget& _target)
);
}
void BMC::checkAssert(VerificationTarget& _target)
void BMC::checkAssert(BMCVerificationTarget& _target)
{
solAssert(_target.type == VerificationTarget::Type::Assert, "");
if (!m_safeAssertions.count(_target.expression))
@ -703,10 +703,12 @@ void BMC::addVerificationTarget(
Expression const* _expression
)
{
VerificationTarget target{
BMCVerificationTarget target{
{
_type,
_value,
currentPathConditions() && m_context.assertions(),
currentPathConditions() && m_context.assertions()
},
_expression,
m_callStack,
modelExpressions()

21
libsolidity/formal/BMC.h
View File

@ -117,24 +117,21 @@ private:
/// Verification targets.
//@{
struct VerificationTarget
struct BMCVerificationTarget: VerificationTarget
{
enum class Type { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert } type;
smt::Expression value;
smt::Expression constraints;
Expression const* expression;
std::vector<CallStackEntry> callStack;
std::pair<std::vector<smt::Expression>, std::vector<std::string>> modelExpressions;
};
void checkVerificationTargets(smt::Expression const& _constraints);
void checkVerificationTarget(VerificationTarget& _target, smt::Expression const& _constraints = smt::Expression(true));
void checkConstantCondition(VerificationTarget& _target);
void checkUnderflow(VerificationTarget& _target, smt::Expression const& _constraints);
void checkOverflow(VerificationTarget& _target, smt::Expression const& _constraints);
void checkDivByZero(VerificationTarget& _target);
void checkBalance(VerificationTarget& _target);
void checkAssert(VerificationTarget& _target);
void checkVerificationTarget(BMCVerificationTarget& _target, smt::Expression const& _constraints = smt::Expression(true));
void checkConstantCondition(BMCVerificationTarget& _target);
void checkUnderflow(BMCVerificationTarget& _target, smt::Expression const& _constraints);
void checkOverflow(BMCVerificationTarget& _target, smt::Expression const& _constraints);
void checkDivByZero(BMCVerificationTarget& _target);
void checkBalance(BMCVerificationTarget& _target);
void checkAssert(BMCVerificationTarget& _target);
void addVerificationTarget(
VerificationTarget::Type _type,
smt::Expression const& _value,
@ -179,7 +176,7 @@ private:
/// ErrorReporter that comes from CompilerStack.
langutil::ErrorReporter& m_outerErrorReporter;
std::vector<VerificationTarget> m_verificationTargets;
std::vector<BMCVerificationTarget> m_verificationTargets;
/// Assertions that are known to be safe.
std::set<Expression const*> m_safeAssertions;

7
libsolidity/formal/SMTEncoder.h
View File

@ -233,6 +233,13 @@ protected:
/// @returns a note to be added to warnings.
std::string extraComment();
struct VerificationTarget
{
enum class Type { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert } type;
smt::Expression value;
smt::Expression constraints;
};
smt::VariableUsage m_variableUsage;
bool m_arrayAssignmentHappened = false;
// True if the "No SMT solver available" warning was already created.