solidity/libsolidity/formal/ArraySlicePredicate.h
2020-10-01 11:52:02 +02:00

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;
};
}