1 /** 2 * Copyright (c) 2021-2022 Huawei Device Co., Ltd. 3 * Licensed under the Apache License, Version 2.0 (the "License"); 4 * you may not use this file except in compliance with the License. 5 * You may obtain a copy of the License at 6 * 7 * http://www.apache.org/licenses/LICENSE-2.0 8 * 9 * Unless required by applicable law or agreed to in writing, software 10 * distributed under the License is distributed on an "AS IS" BASIS, 11 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. 12 * See the License for the specific language governing permissions and 13 * limitations under the License. 14 */ 15 16 #ifndef _PANDA_TYPE_SYSTEM_RELATION_HPP 17 #define _PANDA_TYPE_SYSTEM_RELATION_HPP 18 19 #include "lazy.h" 20 #include "index.h" 21 22 #include "runtime/include/mem/panda_containers.h" 23 #include "int_set.h" 24 25 #include "macros.h" 26 27 #include <limits> 28 #include <initializer_list> 29 #include <type_traits> 30 31 namespace panda::verifier { 32 33 class Relation { 34 public: 35 using RelIndex = size_t; 36 using MapIndexFromTo = PandaVector<IntSet<size_t>>; 37 Relate(RelIndex from,RelIndex to)38 void Relate(RelIndex from, RelIndex to) 39 { 40 ASSERT(from < Direct_.size()); 41 ASSERT(to < Inverse_.size()); 42 Inverse_[to].Insert(from); 43 Inverse_[to] |= Inverse_[from]; 44 Direct_[from].Insert(to); 45 Direct_[from] |= Direct_[to]; 46 // flatten relation 47 Direct_[to].ForAll([&](RelIndex dst) { 48 Inverse_[dst].Insert(from); 49 Inverse_[dst] |= Inverse_[from]; 50 return true; 51 }); 52 Inverse_[from].ForAll([&](RelIndex src) { 53 Direct_[src].Insert(to); 54 Direct_[src] |= Direct_[to]; 55 return true; 56 }); 57 } 58 SymmRelate(RelIndex lhs,RelIndex rhs)59 void SymmRelate(RelIndex lhs, RelIndex rhs) 60 { 61 Relate(lhs, rhs); 62 Relate(rhs, lhs); 63 } 64 65 Relation &operator+=(const std::pair<RelIndex, RelIndex> &pair) 66 { 67 Relate(pair.first, pair.second); 68 return *this; 69 } 70 71 Relation &operator+=(std::initializer_list<std::pair<RelIndex, RelIndex>> pairs) 72 { 73 for (const auto &p : pairs) { 74 *this += p; 75 } 76 return *this; 77 } 78 EnsureMinSize(size_t idx)79 void EnsureMinSize(size_t idx) 80 { 81 if (idx >= Direct_.size()) { 82 size_t i = idx + 1; 83 Direct_.resize(i); 84 Inverse_.resize(i); 85 } 86 } 87 88 template <typename Handler> ForAllFrom(RelIndex from,Handler && handler)89 void ForAllFrom(RelIndex from, Handler &&handler) const 90 { 91 ASSERT(from < Direct_.size()); 92 Direct_[from].ForAll(handler); 93 } 94 95 template <typename Handler> ForAllTo(RelIndex to,Handler && handler)96 void ForAllTo(RelIndex to, Handler &&handler) const 97 { 98 ASSERT(to < Inverse_.size()); 99 Inverse_[to].ForAll(handler); 100 } 101 102 template <typename Handler> ForAllBetween(RelIndex from,RelIndex to,Handler && handler)103 void ForAllBetween(RelIndex from, RelIndex to, Handler &&handler) const 104 { 105 if (IsInInverseRelation(from, to)) { 106 auto tmp = to; 107 to = from; 108 from = tmp; 109 } 110 auto stream = Direct_[from].LazyIntersect(Inverse_[to]); 111 auto value = stream(); 112 while (value.IsValid()) { 113 if (!handler(value)) { 114 return; 115 } 116 value = stream(); 117 } 118 } 119 IsInDirectRelation(RelIndex from,RelIndex to)120 bool IsInDirectRelation(RelIndex from, RelIndex to) const 121 { 122 return from < Direct_.size() && Direct_[from].Contains(to); 123 } 124 IsInInverseRelation(RelIndex from,RelIndex to)125 bool IsInInverseRelation(RelIndex from, RelIndex to) const 126 { 127 return from < Inverse_.size() && Inverse_[from].Contains(to); 128 } 129 IsInAnyRelation(RelIndex from,RelIndex to)130 bool IsInAnyRelation(RelIndex from, RelIndex to) const 131 { 132 return IsInDirectRelation(from, to) || IsInInverseRelation(from, to); 133 } 134 IsInIsoRelation(RelIndex from,RelIndex to)135 bool IsInIsoRelation(RelIndex from, RelIndex to) const 136 { 137 return IsInDirectRelation(from, to) && IsInInverseRelation(from, to); 138 } 139 GetDirectlyRelated(RelIndex from)140 const IntSet<RelIndex> &GetDirectlyRelated(RelIndex from) const 141 { 142 return Direct_[from]; 143 } 144 GetInverselyRelated(RelIndex to)145 const IntSet<RelIndex> &GetInverselyRelated(RelIndex to) const 146 { 147 return Inverse_[to]; 148 } 149 150 private: 151 MapIndexFromTo Direct_, Inverse_; 152 }; 153 } // namespace panda::verifier 154 155 #endif // !_PANDA_TYPE_SYSTEM_RELATION_HPP 156