mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
63 lines
2.1 KiB
C
63 lines
2.1 KiB
C
|
/*
|
||
|
|
This file is part of solidity.
|
||
|
|
|
||
|
|
solidity is free software: you can redistribute it and/or modify
|
||
|
|
it under the terms of the GNU General Public License as published by
|
||
|
|
the Free Software Foundation, either version 3 of the License, or
|
||
|
|
(at your option) any later version.
|
||
|
|
|
||
|
|
solidity is distributed in the hope that it will be useful,
|
||
|
|
but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||
|
|
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||
|
|
GNU General Public License for more details.
|
||
|
|
|
||
|
|
You should have received a copy of the GNU General Public License
|
||
|
|
along with solidity. If not, see <http://www.gnu.org/licenses/>.
|
||
|
|
*/
|
||
|
|
// SPDX-License-Identifier: GPL-3.0
|
||
|
|
|
||
|
|
#include <libsolidity/formal/EncodingContext.h>
|
||
|
|
#include <libsolidity/formal/Predicate.h>
|
||
|
|
#include <libsolidity/formal/SymbolicVariables.h>
|
||
|
|
|
||
|
|
#include <libsmtutil/Sorts.h>
|
||
|
|
|
||
|
|
#include <vector>
|
||
|
|
|
||
|
|
namespace solidity::frontend
|
||
|
|
{
|
||
|
|
|
||
|
|
/**
|
||
|
|
* Contains the set of rules to compute an array slice.
|
||
|
|
* Rules:
|
||
|
|
* 1. end > start => ArraySliceHeader(a, b, start, end, 0)
|
||
|
|
* 2. ArraySliceHeader(a, b, start, end, i) && i >= (end - start) => ArraySlice(a, b, start, end)
|
||
|
|
* 3. ArraySliceHeader(a, b, start, end, i) && i >= 0 && i < (end - start) => ArraySliceLoop(a, b, start, end, i)
|
||
|
|
* 4. ArraySliceLoop(a, b, start, end, i) && b[i] = a[start + i] => ArraySliceHeader(a, b, start, end, i + 1)
|
||
|
|
*
|
||
|
|
* The rule to be used by CHC is ArraySlice(a, b, start, end).
|
||
|
|
*/
|
||
|
|
|
||
|
|
struct ArraySlicePredicate
|
||
|
|
{
|
||
|
|
/// Contains the predicates and rules created to compute
|
||
|
|
/// array slices for a given sort.
|
||
|
|
struct SliceData
|
||
|
|
{
|
||
|
|
std::vector<Predicate const*> predicates;
|
||
|
|
std::vector<smtutil::Expression> rules;
|
||
|
|
};
|
||
|
|
|
||
|
|
/// @returns a flag representing whether the array slice predicates had already been created before for this sort,
|
||
|
|
/// and the corresponding slice data.
|
||
|
|
static std::pair<bool, SliceData const&> create(smtutil::SortPointer _sort, smt::EncodingContext& _context);
|
||
|
|
|
||
|
|
static void reset() { m_slicePredicates.clear(); }
|
||
|
|
|
||
|
|
private:
|
||
|
|
/// Maps a unique sort name to its slice data.
|
||
|
|
static std::map<std::string, SliceData> m_slicePredicates;
|
||
|
|
};
|
||
|
|
|
||
|
|
}
|