1 /* 2 * Copyright (c) 2021 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_VERIFICATION_UTIL_RELATION_H_ 17 #define PANDA_VERIFICATION_UTIL_RELATION_H_ 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 for (RelIndex dst : Direct_[to]) { 48 Inverse_[dst].Insert(from); 49 Inverse_[dst] |= Inverse_[from]; 50 } 51 for (RelIndex src : Inverse_[from]) { 52 Direct_[src].Insert(to); 53 Direct_[src] |= Direct_[to]; 54 } 55 } 56 SymmRelate(RelIndex lhs,RelIndex rhs)57 void SymmRelate(RelIndex lhs, RelIndex rhs) 58 { 59 Relate(lhs, rhs); 60 Relate(rhs, lhs); 61 } 62 63 Relation &operator+=(const std::pair<RelIndex, RelIndex> &pair) 64 { 65 Relate(pair.first, pair.second); 66 return *this; 67 } 68 69 Relation &operator+=(std::initializer_list<std::pair<RelIndex, RelIndex>> pairs) 70 { 71 for (const auto &p : pairs) { 72 *this += p; 73 } 74 return *this; 75 } 76 EnsureMinSize(size_t idx)77 void EnsureMinSize(size_t idx) 78 { 79 if (idx >= Direct_.size()) { 80 size_t i = idx + 1; 81 Direct_.resize(i); 82 Inverse_.resize(i); 83 } 84 } 85 86 template <typename Handler> ForAllFrom(RelIndex from,Handler && handler)87 void ForAllFrom(RelIndex from, Handler &&handler) const 88 { 89 ASSERT(from < Direct_.size()); 90 Direct_[from].ForAll(handler); 91 } 92 93 template <typename Handler> ForAllTo(RelIndex to,Handler && handler)94 void ForAllTo(RelIndex to, Handler &&handler) const 95 { 96 ASSERT(to < Inverse_.size()); 97 Inverse_[to].ForAll(handler); 98 } 99 100 template <typename Handler> ForAllBetween(RelIndex from,RelIndex to,Handler && handler)101 void ForAllBetween(RelIndex from, RelIndex to, Handler &&handler) const 102 { 103 if (IsInInverseRelation(from, to)) { 104 auto tmp = to; 105 to = from; 106 from = tmp; 107 } 108 auto stream = Direct_[from].LazyIntersect(Inverse_[to]); 109 auto value = stream(); 110 while (value.IsValid()) { 111 if (!handler(value)) { 112 return; 113 } 114 value = stream(); 115 } 116 } 117 IsInDirectRelation(RelIndex from,RelIndex to)118 bool IsInDirectRelation(RelIndex from, RelIndex to) const 119 { 120 return from < Direct_.size() && Direct_[from].Contains(to); 121 } 122 IsInInverseRelation(RelIndex from,RelIndex to)123 bool IsInInverseRelation(RelIndex from, RelIndex to) const 124 { 125 return from < Inverse_.size() && Inverse_[from].Contains(to); 126 } 127 IsInAnyRelation(RelIndex from,RelIndex to)128 bool IsInAnyRelation(RelIndex from, RelIndex to) const 129 { 130 return IsInDirectRelation(from, to) || IsInInverseRelation(from, to); 131 } 132 IsInIsoRelation(RelIndex from,RelIndex to)133 bool IsInIsoRelation(RelIndex from, RelIndex to) const 134 { 135 return IsInDirectRelation(from, to) && IsInInverseRelation(from, to); 136 } 137 GetDirectlyRelated(RelIndex from)138 const IntSet<RelIndex> &GetDirectlyRelated(RelIndex from) const 139 { 140 return Direct_[from]; 141 } 142 GetInverselyRelated(RelIndex to)143 const IntSet<RelIndex> &GetInverselyRelated(RelIndex to) const 144 { 145 return Inverse_[to]; 146 } 147 148 private: 149 MapIndexFromTo Direct_, Inverse_; 150 }; 151 } // namespace panda::verifier 152 153 #endif // PANDA_VERIFICATION_UTIL_RELATION_H_ 154