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_Bool] Fix PR review comments: method renaming and solAssert

Browse Source
This commit is contained in:
Leonardo Alt 2018-03-12 20:15:27 +01:00
parent c2d26eb6a2
commit 9b64dc501d
3 changed files with 17 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
libsolidity/formal/SMTChecker.cpp
View File

@ -205,7 +205,7 @@ void SMTChecker::endVisit(Assignment const& _assignment)
_assignment.location(), _assignment.location(),
"Assertion checker does not yet implement compound assignment." "Assertion checker does not yet implement compound assignment."
); );
else if (!SSAVariable::supportedType(_assignment.annotation().type->category())) else if (!SSAVariable::isSupportedType(_assignment.annotation().type->category()))
m_errorReporter.warning( m_errorReporter.warning(
_assignment.location(), _assignment.location(),
"Assertion checker does not yet implement type " + _assignment.annotation().type->toString() "Assertion checker does not yet implement type " + _assignment.annotation().type->toString()
@ -266,7 +266,7 @@ void SMTChecker::endVisit(UnaryOperation const& _op)
{ {
case Token::Not: // ! case Token::Not: // !
{ {
solAssert(SSAVariable::typeBool(_op.annotation().type->category()), ""); solAssert(SSAVariable::isBool(_op.annotation().type->category()), "");
defineExpr(_op, !expr(_op.subExpression())); defineExpr(_op, !expr(_op.subExpression()));
break; break;
} }
@ -274,7 +274,7 @@ void SMTChecker::endVisit(UnaryOperation const& _op)
case Token::Dec: // -- (pre- or postfix) case Token::Dec: // -- (pre- or postfix)
{ {
solAssert(SSAVariable::typeInteger(_op.annotation().type->category()), ""); solAssert(SSAVariable::isInteger(_op.annotation().type->category()), "");
solAssert(_op.subExpression().annotation().lValueRequested, ""); solAssert(_op.subExpression().annotation().lValueRequested, "");
if (Identifier const* identifier = dynamic_cast<Identifier const*>(&_op.subExpression())) if (Identifier const* identifier = dynamic_cast<Identifier const*>(&_op.subExpression()))
{ {
@ -371,7 +371,7 @@ void SMTChecker::endVisit(Identifier const& _identifier)
{ {
// Will be translated as part of the node that requested the lvalue. // Will be translated as part of the node that requested the lvalue.
} }
else if (SSAVariable::supportedType(_identifier.annotation().type->category())) else if (SSAVariable::isSupportedType(_identifier.annotation().type->category()))
defineExpr(_identifier, currentValue(*decl)); defineExpr(_identifier, currentValue(*decl));
else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get())) else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
{ {
@ -445,13 +445,13 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
void SMTChecker::compareOperation(BinaryOperation const& _op) void SMTChecker::compareOperation(BinaryOperation const& _op)
{ {
solAssert(_op.annotation().commonType, ""); solAssert(_op.annotation().commonType, "");
if (SSAVariable::supportedType(_op.annotation().commonType->category())) if (SSAVariable::isSupportedType(_op.annotation().commonType->category()))
{ {
smt::Expression left(expr(_op.leftExpression())); smt::Expression left(expr(_op.leftExpression()));
smt::Expression right(expr(_op.rightExpression())); smt::Expression right(expr(_op.rightExpression()));
Token::Value op = _op.getOperator(); Token::Value op = _op.getOperator();
shared_ptr<smt::Expression> value; shared_ptr<smt::Expression> value;
if (SSAVariable::typeInteger(_op.annotation().commonType->category())) if (SSAVariable::isInteger(_op.annotation().commonType->category()))
{ {
value = make_shared<smt::Expression>( value = make_shared<smt::Expression>(
op == Token::Equal ? (left == right) : op == Token::Equal ? (left == right) :
@ -464,6 +464,7 @@ void SMTChecker::compareOperation(BinaryOperation const& _op)
} }
else // Bool else // Bool
{ {
solAssert(SSAVariable::isBool(_op.annotation().commonType->category()), "");
value = make_shared<smt::Expression>( value = make_shared<smt::Expression>(
op == Token::Equal ? (left == right) : op == Token::Equal ? (left == right) :
op == Token::NotEqual ? (left != right) : op == Token::NotEqual ? (left != right) :
@ -744,7 +745,7 @@ void SMTChecker::mergeVariables(vector<Declaration const*> const& _variables, sm
bool SMTChecker::createVariable(VariableDeclaration const& _varDecl) bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
{ {
if (SSAVariable::supportedType(_varDecl.type()->category())) if (SSAVariable::isSupportedType(_varDecl.type()->category()))
{ {
solAssert(m_variables.count(&_varDecl) == 0, ""); solAssert(m_variables.count(&_varDecl) == 0, "");
m_variables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface)); m_variables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface));

12
libsolidity/formal/SSAVariable.cpp
View File

@ -33,9 +33,9 @@ SSAVariable::SSAVariable(
{ {
resetIndex(); resetIndex();
if (typeInteger(_decl.type()->category())) if (isInteger(_decl.type()->category()))
m_symbolicVar = make_shared<SymbolicIntVariable>(_decl, _interface); m_symbolicVar = make_shared<SymbolicIntVariable>(_decl, _interface);
else if (typeBool(_decl.type()->category())) else if (isBool(_decl.type()->category()))
m_symbolicVar = make_shared<SymbolicBoolVariable>(_decl, _interface); m_symbolicVar = make_shared<SymbolicBoolVariable>(_decl, _interface);
else else
{ {
@ -43,17 +43,17 @@ SSAVariable::SSAVariable(
} }
} }
bool SSAVariable::supportedType(Type::Category _category) bool SSAVariable::isSupportedType(Type::Category _category)
{ {
return typeInteger(_category) || typeBool(_category); return isInteger(_category) || isBool(_category);
} }
bool SSAVariable::typeInteger(Type::Category _category) bool SSAVariable::isInteger(Type::Category _category)
{ {
return _category == Type::Category::Integer; return _category == Type::Category::Integer;
} }
bool SSAVariable::typeBool(Type::Category _category) bool SSAVariable::isBool(Type::Category _category)
{ {
return _category == Type::Category::Bool; return _category == Type::Category::Bool;
} }

6
libsolidity/formal/SSAVariable.h
View File

@ -69,9 +69,9 @@ public:
void setUnknownValue(); void setUnknownValue();
/// So far Int and Bool are supported. /// So far Int and Bool are supported.
static bool supportedType(Type::Category _category); static bool isSupportedType(Type::Category _category);
static bool typeInteger(Type::Category _category); static bool isInteger(Type::Category _category);
static bool typeBool(Type::Category _category); static bool isBool(Type::Category _category);
private: private:
smt::Expression valueAtSequence(int _seq) const smt::Expression valueAtSequence(int _seq) const