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

Implement missing overrides and relax smtAsserts

Browse Source
This commit is contained in:
Matheus Aguiar 2023-05-03 21:55:49 -03:00
parent 347c966f08
commit c1720e62aa
2 changed files with 31 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
libsmtutil/SolverInterface.h
View File

@ -123,7 +123,7 @@ public:
explicit Expression(std::shared_ptr<SortSort> _sort, std::string _name = ""): Expression(std::move(_name), {}, _sort) {} explicit Expression(std::shared_ptr<SortSort> _sort, std::string _name = ""): Expression(std::move(_name), {}, _sort) {}
explicit Expression(std::string _name, std::vector<Expression> _arguments, SortPointer _sort): explicit Expression(std::string _name, std::vector<Expression> _arguments, SortPointer _sort):
name(std::move(_name)), arguments(std::move(_arguments)), sort(std::move(_sort)) {} name(std::move(_name)), arguments(std::move(_arguments)), sort(std::move(_sort)) {}
Expression(size_t _number): Expression(std::to_string(_number), {}, SortProvider::sintSort) {} Expression(size_t _number): Expression(std::to_string(_number), {}, SortProvider::uintSort) {}
Expression(u256 const& _number): Expression(_number.str(), {}, SortProvider::sintSort) {} Expression(u256 const& _number): Expression(_number.str(), {}, SortProvider::sintSort) {}
Expression(s256 const& _number): Expression( Expression(s256 const& _number): Expression(
_number >= 0 ? _number.str() : "-", _number >= 0 ? _number.str() : "-",
@ -189,7 +189,10 @@ public:
static Expression ite(Expression _condition, Expression _trueValue, Expression _falseValue) static Expression ite(Expression _condition, Expression _trueValue, Expression _falseValue)
{ {
smtAssert(*_trueValue.sort == *_falseValue.sort, ""); if (_trueValue.sort->kind == Kind::Int)
smtAssert(_trueValue.sort->kind == _falseValue.sort->kind, "");
else
smtAssert(*_trueValue.sort == *_falseValue.sort, "");
SortPointer sort = _trueValue.sort; SortPointer sort = _trueValue.sort;
return Expression("ite", std::vector<Expression>{ return Expression("ite", std::vector<Expression>{
std::move(_condition), std::move(_trueValue), std::move(_falseValue) std::move(_condition), std::move(_trueValue), std::move(_falseValue)
@ -213,7 +216,10 @@ public:
std::shared_ptr<ArraySort> arraySort = std::dynamic_pointer_cast<ArraySort>(_array.sort); std::shared_ptr<ArraySort> arraySort = std::dynamic_pointer_cast<ArraySort>(_array.sort);
smtAssert(arraySort, ""); smtAssert(arraySort, "");
smtAssert(_index.sort, ""); smtAssert(_index.sort, "");
smtAssert(*arraySort->domain == *_index.sort, ""); if (arraySort->domain->kind == Kind::Int)
smtAssert(arraySort->domain->kind == _index.sort->kind, "");
else
smtAssert(*arraySort->domain == *_index.sort, "");
return Expression( return Expression(
"select", "select",
std::vector<Expression>{std::move(_array), std::move(_index)}, std::vector<Expression>{std::move(_array), std::move(_index)},
@ -230,7 +236,10 @@ public:
smtAssert(_index.sort, ""); smtAssert(_index.sort, "");
smtAssert(_element.sort, ""); smtAssert(_element.sort, "");
smtAssert(*arraySort->domain == *_index.sort, ""); smtAssert(*arraySort->domain == *_index.sort, "");
smtAssert(*arraySort->range == *_element.sort, ""); if (arraySort->domain->kind == Kind::Int)
smtAssert(arraySort->range->kind == _element.sort->kind, "");
else
smtAssert(*arraySort->range == *_element.sort, "");
return Expression( return Expression(
"store", "store",
std::vector<Expression>{std::move(_array), std::move(_index), std::move(_element)}, std::vector<Expression>{std::move(_array), std::move(_index), std::move(_element)},
@ -245,7 +254,10 @@ public:
auto arraySort = std::dynamic_pointer_cast<ArraySort>(sortSort->inner); auto arraySort = std::dynamic_pointer_cast<ArraySort>(sortSort->inner);
smtAssert(sortSort && arraySort, ""); smtAssert(sortSort && arraySort, "");
smtAssert(_value.sort, ""); smtAssert(_value.sort, "");
smtAssert(*arraySort->range == *_value.sort, ""); if (arraySort->domain->kind == Kind::Int)
smtAssert(arraySort->range->kind == _value.sort->kind, "");
else
smtAssert(*arraySort->range == *_value.sort, "");
return Expression( return Expression(
"const_array", "const_array",
std::vector<Expression>{std::move(_sort), std::move(_value)}, std::vector<Expression>{std::move(_sort), std::move(_value)},

18
libsmtutil/Sorts.h
View File

@ -57,9 +57,14 @@ struct IntSort: public Sort
isSigned(_signed) isSigned(_signed)
{} {}
bool operator==(IntSort const& _other) const bool operator==(Sort const& _other) const override
{ {
return Sort::operator==(_other) && isSigned == _other.isSigned; if (!Sort::operator==(_other))
return false;
auto otherIntSort = dynamic_cast<IntSort const*>(&_other);
smtAssert(otherIntSort);
return isSigned == otherIntSort->isSigned;
} }
bool isSigned; bool isSigned;
@ -72,9 +77,14 @@ struct BitVectorSort: public Sort
size(_size) size(_size)
{} {}
bool operator==(BitVectorSort const& _other) const bool operator==(Sort const& _other) const override
{ {
return Sort::operator==(_other) && size == _other.size; if (!Sort::operator==(_other))
return false;
auto otherBitVectorSort = dynamic_cast<BitVectorSort const*>(&_other);
smtAssert(otherBitVectorSort);
return size == otherBitVectorSort->size;
} }
unsigned size; unsigned size;