From 6a940f0a99e941c48e5deb695e89ac52784c4f3c Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Sun, 21 Jan 2018 13:58:56 +0100 Subject: [SMTChecker] Support to Bool variables --- libsolidity/formal/SMTChecker.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'libsolidity/formal/SMTChecker.cpp') diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 1da5b291..83784ead 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -444,7 +444,7 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op) void SMTChecker::compareOperation(BinaryOperation const& _op) { solAssert(_op.annotation().commonType, ""); - if (_op.annotation().commonType->category() == Type::Category::Integer) + if (SSAVariable::supportedType(_op.annotation().commonType.get())) { smt::Expression left(expr(_op.leftExpression())); smt::Expression right(expr(_op.rightExpression())); -- cgit v1.2.3 From c2d26eb6a20a21f5fe4b5d78a39f8c23f7f3f5cb Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Fri, 9 Mar 2018 16:19:03 +0100 Subject: [SMTChecker_Bool] Fix PR comments; Add support to gt, ge, lt, le. and tests. --- libsolidity/formal/SMTChecker.cpp | 48 ++++++++++++++++++++++++++------------- 1 file changed, 32 insertions(+), 16 deletions(-) (limited to 'libsolidity/formal/SMTChecker.cpp') diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 83784ead..d4f94f16 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -205,7 +205,7 @@ void SMTChecker::endVisit(Assignment const& _assignment) _assignment.location(), "Assertion checker does not yet implement compound assignment." ); - else if (_assignment.annotation().type->category() != Type::Category::Integer) + else if (!SSAVariable::supportedType(_assignment.annotation().type->category())) m_errorReporter.warning( _assignment.location(), "Assertion checker does not yet implement type " + _assignment.annotation().type->toString() @@ -266,14 +266,15 @@ void SMTChecker::endVisit(UnaryOperation const& _op) { case Token::Not: // ! { - solAssert(_op.annotation().type->category() == Type::Category::Bool, ""); + solAssert(SSAVariable::typeBool(_op.annotation().type->category()), ""); defineExpr(_op, !expr(_op.subExpression())); break; } case Token::Inc: // ++ (pre- or postfix) case Token::Dec: // -- (pre- or postfix) { - solAssert(_op.annotation().type->category() == Type::Category::Integer, ""); + + solAssert(SSAVariable::typeInteger(_op.annotation().type->category()), ""); solAssert(_op.subExpression().annotation().lValueRequested, ""); if (Identifier const* identifier = dynamic_cast(&_op.subExpression())) { @@ -370,7 +371,7 @@ void SMTChecker::endVisit(Identifier const& _identifier) { // Will be translated as part of the node that requested the lvalue. } - else if (SSAVariable::supportedType(_identifier.annotation().type.get())) + else if (SSAVariable::supportedType(_identifier.annotation().type->category())) defineExpr(_identifier, currentValue(*decl)); else if (FunctionType const* fun = dynamic_cast(_identifier.annotation().type.get())) { @@ -444,21 +445,36 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op) void SMTChecker::compareOperation(BinaryOperation const& _op) { solAssert(_op.annotation().commonType, ""); - if (SSAVariable::supportedType(_op.annotation().commonType.get())) + if (SSAVariable::supportedType(_op.annotation().commonType->category())) { smt::Expression left(expr(_op.leftExpression())); smt::Expression right(expr(_op.rightExpression())); Token::Value op = _op.getOperator(); - smt::Expression value = ( - op == Token::Equal ? (left == right) : - op == Token::NotEqual ? (left != right) : - op == Token::LessThan ? (left < right) : - op == Token::LessThanOrEqual ? (left <= right) : - op == Token::GreaterThan ? (left > right) : - /*op == Token::GreaterThanOrEqual*/ (left >= right) - ); + shared_ptr value; + if (SSAVariable::typeInteger(_op.annotation().commonType->category())) + { + value = make_shared( + op == Token::Equal ? (left == right) : + op == Token::NotEqual ? (left != right) : + op == Token::LessThan ? (left < right) : + op == Token::LessThanOrEqual ? (left <= right) : + op == Token::GreaterThan ? (left > right) : + /*op == Token::GreaterThanOrEqual*/ (left >= right) + ); + } + else // Bool + { + value = make_shared( + op == Token::Equal ? (left == right) : + op == Token::NotEqual ? (left != right) : + op == Token::LessThan ? (!left && right) : + op == Token::LessThanOrEqual ? (!left || right) : + op == Token::GreaterThan ? (left && !right) : + /*op == Token::GreaterThanOrEqual*/ (left || !right) + ); + } // TODO: check that other values for op are not possible. - defineExpr(_op, value); + defineExpr(_op, *value); } else m_errorReporter.warning( @@ -728,10 +744,10 @@ void SMTChecker::mergeVariables(vector const& _variables, sm bool SMTChecker::createVariable(VariableDeclaration const& _varDecl) { - if (SSAVariable::supportedType(_varDecl.type().get())) + if (SSAVariable::supportedType(_varDecl.type()->category())) { solAssert(m_variables.count(&_varDecl) == 0, ""); - m_variables.emplace(&_varDecl, SSAVariable(&_varDecl, *m_interface)); + m_variables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface)); return true; } else -- cgit v1.2.3 From 9b64dc501da5c743b948e4dca844a6cd67766be1 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 12 Mar 2018 20:15:27 +0100 Subject: [SMTChecker_Bool] Fix PR review comments: method renaming and solAssert --- libsolidity/formal/SMTChecker.cpp | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) (limited to 'libsolidity/formal/SMTChecker.cpp') diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index d4f94f16..8f4abdc2 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -205,7 +205,7 @@ void SMTChecker::endVisit(Assignment const& _assignment) _assignment.location(), "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( _assignment.location(), "Assertion checker does not yet implement type " + _assignment.annotation().type->toString() @@ -266,7 +266,7 @@ void SMTChecker::endVisit(UnaryOperation const& _op) { case Token::Not: // ! { - solAssert(SSAVariable::typeBool(_op.annotation().type->category()), ""); + solAssert(SSAVariable::isBool(_op.annotation().type->category()), ""); defineExpr(_op, !expr(_op.subExpression())); break; } @@ -274,7 +274,7 @@ void SMTChecker::endVisit(UnaryOperation const& _op) 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, ""); if (Identifier const* identifier = dynamic_cast(&_op.subExpression())) { @@ -371,7 +371,7 @@ void SMTChecker::endVisit(Identifier const& _identifier) { // 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)); else if (FunctionType const* fun = dynamic_cast(_identifier.annotation().type.get())) { @@ -445,13 +445,13 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op) void SMTChecker::compareOperation(BinaryOperation const& _op) { 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 right(expr(_op.rightExpression())); Token::Value op = _op.getOperator(); shared_ptr value; - if (SSAVariable::typeInteger(_op.annotation().commonType->category())) + if (SSAVariable::isInteger(_op.annotation().commonType->category())) { value = make_shared( op == Token::Equal ? (left == right) : @@ -464,6 +464,7 @@ void SMTChecker::compareOperation(BinaryOperation const& _op) } else // Bool { + solAssert(SSAVariable::isBool(_op.annotation().commonType->category()), ""); value = make_shared( op == Token::Equal ? (left == right) : op == Token::NotEqual ? (left != right) : @@ -744,7 +745,7 @@ void SMTChecker::mergeVariables(vector const& _variables, sm bool SMTChecker::createVariable(VariableDeclaration const& _varDecl) { - if (SSAVariable::supportedType(_varDecl.type()->category())) + if (SSAVariable::isSupportedType(_varDecl.type()->category())) { solAssert(m_variables.count(&_varDecl) == 0, ""); m_variables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface)); -- cgit v1.2.3