aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--libsolidity/formal/SMTChecker.cpp70
-rw-r--r--libsolidity/formal/SMTChecker.h3
-rw-r--r--libsolidity/formal/SymbolicTypes.cpp54
-rw-r--r--libsolidity/formal/SymbolicTypes.h14
4 files changed, 62 insertions, 79 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 671c2049..e5648eb3 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -458,6 +458,12 @@ void SMTChecker::endVisit(Identifier const& _identifier)
{
// Will be translated as part of the node that requested the lvalue.
}
+ else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
+ {
+ if (fun->kind() == FunctionType::Kind::Assert || fun->kind() == FunctionType::Kind::Require)
+ return;
+ createExpr(_identifier);
+ }
else if (isSupportedType(_identifier.annotation().type->category()))
{
if (VariableDeclaration const* decl = dynamic_cast<VariableDeclaration const*>(_identifier.annotation().referencedDeclaration))
@@ -469,25 +475,15 @@ void SMTChecker::endVisit(Identifier const& _identifier)
"Assertion checker does not yet support the type of this variable."
);
}
- else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
- {
- if (fun->kind() == FunctionType::Kind::Assert || fun->kind() == FunctionType::Kind::Require)
- return;
- createExpr(_identifier);
- }
}
void SMTChecker::endVisit(Literal const& _literal)
{
Type const& type = *_literal.annotation().type;
- if (type.category() == Type::Category::Integer || type.category() == Type::Category::Address || type.category() == Type::Category::RationalNumber)
- {
- if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(&type))
- solAssert(!rational->isFractional(), "");
+ if (isNumber(type.category()))
defineExpr(_literal, smt::Expression(type.literalValue(&_literal)));
- }
- else if (type.category() == Type::Category::Bool)
+ else if (isBool(type.category()))
defineExpr(_literal, smt::Expression(_literal.token() == Token::TrueLiteral ? true : false));
else
m_errorReporter.warning(
@@ -917,13 +913,10 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
if (hasVariable(_varDecl))
return true;
auto const& type = _varDecl.type();
- if (isSupportedType(type->category()))
- {
- solAssert(m_variables.count(&_varDecl) == 0, "");
- m_variables.emplace(&_varDecl, newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()), *m_interface));
- return true;
- }
- else
+ solAssert(m_variables.count(&_varDecl) == 0, "");
+ auto result = newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()), *m_interface);
+ m_variables.emplace(&_varDecl, result.second);
+ if (result.first)
{
m_errorReporter.warning(
_varDecl.location(),
@@ -931,6 +924,7 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
);
return false;
}
+ return true;
}
string SMTChecker::uniqueSymbol(Expression const& _expr)
@@ -980,7 +974,7 @@ smt::Expression SMTChecker::expr(Expression const& _e)
m_errorReporter.warning(_e.location(), "Internal error: Expression undefined for SMT solver." );
createExpr(_e);
}
- return prev(m_expressions.upper_bound(&_e))->second;
+ return m_expressions.at(&_e)->currentValue();
}
bool SMTChecker::hasExpr(Expression const& _e) const
@@ -996,33 +990,17 @@ bool SMTChecker::hasVariable(VariableDeclaration const& _var) const
void SMTChecker::createExpr(Expression const& _e)
{
solAssert(_e.annotation().type, "");
- string exprSymbol = uniqueSymbol(_e) + "_" + to_string(m_expressions.count(&_e));
- switch (_e.annotation().type->category())
- {
- case Type::Category::RationalNumber:
+ if (hasExpr(_e))
+ m_expressions.at(&_e)->increaseIndex();
+ else
{
- if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(_e.annotation().type.get()))
- solAssert(!rational->isFractional(), "");
- m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol));
- break;
- }
- case Type::Category::Address:
- case Type::Category::Integer:
- m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol));
- break;
- case Type::Category::Bool:
- m_expressions.emplace(&_e, m_interface->newBool(exprSymbol));
- break;
- case Type::Category::Function:
- // This should be replaced by a `non-deterministic` type in the future.
- m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol));
- break;
- default:
- m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol));
- m_errorReporter.warning(
- _e.location(),
- "Assertion checker does not yet implement this type."
- );
+ auto result = newSymbolicVariable(*_e.annotation().type, "expr_" + to_string(_e.id()), *m_interface);
+ m_expressions.emplace(&_e, result.second);
+ if (result.first)
+ m_errorReporter.warning(
+ _e.location(),
+ "Assertion checker does not yet implement this type."
+ );
}
}
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index 0b078556..f66693d2 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -25,7 +25,6 @@
#include <libsolidity/interface/ReadFile.h>
-#include <map>
#include <unordered_map>
#include <string>
#include <vector>
@@ -186,7 +185,7 @@ private:
bool m_loopExecutionHappened = false;
/// An Expression may have multiple smt::Expression due to
/// repeated calls to the same function.
- std::multimap<Expression const*, smt::Expression> m_expressions;
+ std::unordered_map<Expression const*, std::shared_ptr<SymbolicVariable>> m_expressions;
std::unordered_map<VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables;
std::vector<smt::Expression> m_pathConditions;
ErrorReporter& m_errorReporter;
diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp
index 2d993865..d47869db 100644
--- a/libsolidity/formal/SymbolicTypes.cpp
+++ b/libsolidity/formal/SymbolicTypes.cpp
@@ -30,27 +30,44 @@ using namespace dev::solidity;
bool dev::solidity::isSupportedType(Type::Category _category)
{
- return isInteger(_category) ||
- isAddress(_category) ||
- isBool(_category);
+ return isNumber(_category) ||
+ isBool(_category) ||
+ isFunction(_category);
}
-shared_ptr<SymbolicVariable> dev::solidity::newSymbolicVariable(
+pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable(
Type const& _type,
std::string const& _uniqueName,
smt::SolverInterface& _solver
)
{
+ bool abstract = false;
+ shared_ptr<SymbolicVariable> var;
if (!isSupportedType(_type))
- return nullptr;
- if (isBool(_type.category()))
- return make_shared<SymbolicBoolVariable>(_type, _uniqueName, _solver);
+ {
+ abstract = true;
+ var = make_shared<SymbolicIntVariable>(IntegerType{256}, _uniqueName, _solver);
+ }
+ else if (isBool(_type.category()))
+ var = make_shared<SymbolicBoolVariable>(_type, _uniqueName, _solver);
+ else if (isFunction(_type.category()))
+ var = make_shared<SymbolicIntVariable>(IntegerType{256}, _uniqueName, _solver);
else if (isInteger(_type.category()))
- return make_shared<SymbolicIntVariable>(_type, _uniqueName, _solver);
+ var = make_shared<SymbolicIntVariable>(_type, _uniqueName, _solver);
else if (isAddress(_type.category()))
- return make_shared<SymbolicAddressVariable>(_type, _uniqueName, _solver);
+ var = make_shared<SymbolicAddressVariable>(_type, _uniqueName, _solver);
+ else if (isRational(_type.category()))
+ {
+ auto rational = dynamic_cast<RationalNumberType const*>(&_type);
+ solAssert(rational, "");
+ if (rational->isFractional())
+ var = make_shared<SymbolicIntVariable>(IntegerType{256}, _uniqueName, _solver);
+ else
+ var = make_shared<SymbolicIntVariable>(_type, _uniqueName, _solver);
+ }
else
solAssert(false, "");
+ return make_pair(abstract, var);
}
bool dev::solidity::isSupportedType(Type const& _type)
@@ -63,9 +80,9 @@ bool dev::solidity::isInteger(Type::Category _category)
return _category == Type::Category::Integer;
}
-bool dev::solidity::isInteger(Type const& _type)
+bool dev::solidity::isRational(Type::Category _category)
{
- return isInteger(_type.category());
+ return _category == Type::Category::RationalNumber;
}
bool dev::solidity::isAddress(Type::Category _category)
@@ -73,30 +90,21 @@ bool dev::solidity::isAddress(Type::Category _category)
return _category == Type::Category::Address;
}
-bool dev::solidity::isAddress(Type const& _type)
-{
- return isAddress(_type.category());
-}
-
bool dev::solidity::isNumber(Type::Category _category)
{
return isInteger(_category) ||
+ isRational(_category) ||
isAddress(_category);
}
-bool dev::solidity::isNumber(Type const& _type)
-{
- return isNumber(_type.category());
-}
-
bool dev::solidity::isBool(Type::Category _category)
{
return _category == Type::Category::Bool;
}
-bool dev::solidity::isBool(Type const& _type)
+bool dev::solidity::isFunction(Type::Category _category)
{
- return isBool(_type.category());
+ return _category == Type::Category::Function;
}
smt::Expression dev::solidity::minValue(IntegerType const& _type)
diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h
index 77822fed..0887fa41 100644
--- a/libsolidity/formal/SymbolicTypes.h
+++ b/libsolidity/formal/SymbolicTypes.h
@@ -34,18 +34,16 @@ bool isSupportedType(Type::Category _category);
bool isSupportedType(Type const& _type);
bool isInteger(Type::Category _category);
-bool isInteger(Type const& _type);
-
+bool isRational(Type::Category _category);
bool isAddress(Type::Category _category);
-bool isAddress(Type const& _type);
-
bool isNumber(Type::Category _category);
-bool isNumber(Type const& _type);
-
bool isBool(Type::Category _category);
-bool isBool(Type const& _type);
+bool isFunction(Type::Category _category);
-std::shared_ptr<SymbolicVariable> newSymbolicVariable(Type const& _type, std::string const& _uniqueName, smt::SolverInterface& _solver);
+/// Returns a new symbolic variable, according to _type.
+/// Also returns whether the type is abstract or not,
+/// which is true for unsupported types.
+std::pair<bool, std::shared_ptr<SymbolicVariable>> newSymbolicVariable(Type const& _type, std::string const& _uniqueName, smt::SolverInterface& _solver);
smt::Expression minValue(IntegerType const& _type);
smt::Expression maxValue(IntegerType const& _type);
generated by cgit (git 2.34.1) at 2024-11-18 11:58:54 +0800