Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1 | // Copyright 2013 the V8 project authors. All rights reserved. |
| 2 | // Use of this source code is governed by a BSD-style license that can be |
| 3 | // found in the LICENSE file. |
| 4 | |
| 5 | #include <vector> |
| 6 | |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 7 | #include "src/crankshaft/hydrogen-types.h" |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 8 | #include "src/types.h" |
| 9 | #include "test/cctest/cctest.h" |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 10 | #include "test/cctest/types-fuzz.h" |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 11 | |
| 12 | using namespace v8::internal; |
| 13 | |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 14 | |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 15 | // Testing auxiliaries (breaking the Type abstraction). |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 16 | |
| 17 | |
| 18 | static bool IsInteger(double x) { |
| 19 | return nearbyint(x) == x && !i::IsMinusZero(x); // Allows for infinities. |
| 20 | } |
| 21 | |
| 22 | |
| 23 | static bool IsInteger(i::Object* x) { |
| 24 | return x->IsNumber() && IsInteger(x->Number()); |
| 25 | } |
| 26 | |
| 27 | |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 28 | typedef uint32_t bitset; |
| 29 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 30 | struct Tests { |
| 31 | typedef Types::TypeVector::iterator TypeIterator; |
| 32 | typedef Types::MapVector::iterator MapIterator; |
| 33 | typedef Types::ValueVector::iterator ValueIterator; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 34 | |
| 35 | Isolate* isolate; |
| 36 | HandleScope scope; |
| 37 | Zone zone; |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 38 | Types T; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 39 | |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 40 | Tests() |
| 41 | : isolate(CcTest::InitIsolateOnce()), |
| 42 | scope(isolate), |
Ben Murdoch | da12d29 | 2016-06-02 14:46:10 +0100 | [diff] [blame] | 43 | zone(isolate->allocator()), |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 44 | T(&zone, isolate, isolate->random_number_generator()) {} |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 45 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 46 | bool IsBitset(Type* type) { return type->IsBitsetForTesting(); } |
| 47 | bool IsUnion(Type* type) { return type->IsUnionForTesting(); } |
| 48 | BitsetType::bitset AsBitset(Type* type) { return type->AsBitsetForTesting(); } |
| 49 | UnionType* AsUnion(Type* type) { return type->AsUnionForTesting(); } |
| 50 | |
| 51 | bool Equal(Type* type1, Type* type2) { |
| 52 | return type1->Equals(type2) && |
| 53 | this->IsBitset(type1) == this->IsBitset(type2) && |
| 54 | this->IsUnion(type1) == this->IsUnion(type2) && |
| 55 | type1->NumClasses() == type2->NumClasses() && |
| 56 | type1->NumConstants() == type2->NumConstants() && |
| 57 | (!this->IsBitset(type1) || |
| 58 | this->AsBitset(type1) == this->AsBitset(type2)) && |
| 59 | (!this->IsUnion(type1) || |
| 60 | this->AsUnion(type1)->LengthForTesting() == |
| 61 | this->AsUnion(type2)->LengthForTesting()); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 62 | } |
| 63 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 64 | void CheckEqual(Type* type1, Type* type2) { CHECK(Equal(type1, type2)); } |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 65 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 66 | void CheckSub(Type* type1, Type* type2) { |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 67 | CHECK(type1->Is(type2)); |
| 68 | CHECK(!type2->Is(type1)); |
| 69 | if (this->IsBitset(type1) && this->IsBitset(type2)) { |
| 70 | CHECK(this->AsBitset(type1) != this->AsBitset(type2)); |
| 71 | } |
| 72 | } |
| 73 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 74 | void CheckSubOrEqual(Type* type1, Type* type2) { |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 75 | CHECK(type1->Is(type2)); |
| 76 | if (this->IsBitset(type1) && this->IsBitset(type2)) { |
| 77 | CHECK((this->AsBitset(type1) | this->AsBitset(type2)) |
| 78 | == this->AsBitset(type2)); |
| 79 | } |
| 80 | } |
| 81 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 82 | void CheckUnordered(Type* type1, Type* type2) { |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 83 | CHECK(!type1->Is(type2)); |
| 84 | CHECK(!type2->Is(type1)); |
| 85 | if (this->IsBitset(type1) && this->IsBitset(type2)) { |
| 86 | CHECK(this->AsBitset(type1) != this->AsBitset(type2)); |
| 87 | } |
| 88 | } |
| 89 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 90 | void CheckOverlap(Type* type1, Type* type2) { |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 91 | CHECK(type1->Maybe(type2)); |
| 92 | CHECK(type2->Maybe(type1)); |
| 93 | } |
| 94 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 95 | void CheckDisjoint(Type* type1, Type* type2) { |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 96 | CHECK(!type1->Is(type2)); |
| 97 | CHECK(!type2->Is(type1)); |
| 98 | CHECK(!type1->Maybe(type2)); |
| 99 | CHECK(!type2->Maybe(type1)); |
| 100 | } |
| 101 | |
| 102 | void IsSomeType() { |
| 103 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 104 | Type* t = *it; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 105 | CHECK(1 == |
| 106 | this->IsBitset(t) + t->IsClass() + t->IsConstant() + t->IsRange() + |
| 107 | this->IsUnion(t) + t->IsArray() + t->IsFunction() + t->IsContext()); |
| 108 | } |
| 109 | } |
| 110 | |
| 111 | void Bitset() { |
| 112 | // None and Any are bitsets. |
| 113 | CHECK(this->IsBitset(T.None)); |
| 114 | CHECK(this->IsBitset(T.Any)); |
| 115 | |
| 116 | CHECK(bitset(0) == this->AsBitset(T.None)); |
| 117 | CHECK(bitset(0xfffffffeu) == this->AsBitset(T.Any)); |
| 118 | |
| 119 | // Union(T1, T2) is bitset for bitsets T1,T2 |
| 120 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 121 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 122 | Type* type1 = *it1; |
| 123 | Type* type2 = *it2; |
| 124 | Type* union12 = T.Union(type1, type2); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 125 | CHECK(!(this->IsBitset(type1) && this->IsBitset(type2)) || |
| 126 | this->IsBitset(union12)); |
| 127 | } |
| 128 | } |
| 129 | |
| 130 | // Intersect(T1, T2) is bitset for bitsets T1,T2 |
| 131 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 132 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 133 | Type* type1 = *it1; |
| 134 | Type* type2 = *it2; |
| 135 | Type* intersect12 = T.Intersect(type1, type2); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 136 | CHECK(!(this->IsBitset(type1) && this->IsBitset(type2)) || |
| 137 | this->IsBitset(intersect12)); |
| 138 | } |
| 139 | } |
| 140 | |
| 141 | // Union(T1, T2) is bitset if T2 is bitset and T1->Is(T2) |
| 142 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 143 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 144 | Type* type1 = *it1; |
| 145 | Type* type2 = *it2; |
| 146 | Type* union12 = T.Union(type1, type2); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 147 | CHECK(!(this->IsBitset(type2) && type1->Is(type2)) || |
| 148 | this->IsBitset(union12)); |
| 149 | } |
| 150 | } |
| 151 | |
| 152 | // Union(T1, T2) is bitwise disjunction for bitsets T1,T2 |
| 153 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 154 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 155 | Type* type1 = *it1; |
| 156 | Type* type2 = *it2; |
| 157 | Type* union12 = T.Union(type1, type2); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 158 | if (this->IsBitset(type1) && this->IsBitset(type2)) { |
| 159 | CHECK( |
| 160 | (this->AsBitset(type1) | this->AsBitset(type2)) == |
| 161 | this->AsBitset(union12)); |
| 162 | } |
| 163 | } |
| 164 | } |
| 165 | |
| 166 | // Intersect(T1, T2) is bitwise conjunction for bitsets T1,T2 (modulo None) |
| 167 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 168 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 169 | Type* type1 = *it1; |
| 170 | Type* type2 = *it2; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 171 | if (this->IsBitset(type1) && this->IsBitset(type2)) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 172 | Type* intersect12 = T.Intersect(type1, type2); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 173 | bitset bits = this->AsBitset(type1) & this->AsBitset(type2); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 174 | CHECK(bits == this->AsBitset(intersect12)); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 175 | } |
| 176 | } |
| 177 | } |
| 178 | } |
| 179 | |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 180 | void PointwiseRepresentation() { |
| 181 | // Check we can decompose type into semantics and representation and |
| 182 | // then compose it back to get an equivalent type. |
| 183 | int counter = 0; |
| 184 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 185 | counter++; |
| 186 | printf("Counter: %i\n", counter); |
| 187 | fflush(stdout); |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 188 | Type* type1 = *it1; |
| 189 | Type* representation = T.Representation(type1); |
| 190 | Type* semantic = T.Semantic(type1); |
| 191 | Type* composed = T.Union(representation, semantic); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 192 | CHECK(type1->Equals(composed)); |
| 193 | } |
| 194 | |
| 195 | // Pointwiseness of Union. |
| 196 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 197 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 198 | Type* type1 = *it1; |
| 199 | Type* type2 = *it2; |
| 200 | Type* representation1 = T.Representation(type1); |
| 201 | Type* semantic1 = T.Semantic(type1); |
| 202 | Type* representation2 = T.Representation(type2); |
| 203 | Type* semantic2 = T.Semantic(type2); |
| 204 | Type* direct_union = T.Union(type1, type2); |
| 205 | Type* representation_union = T.Union(representation1, representation2); |
| 206 | Type* semantic_union = T.Union(semantic1, semantic2); |
| 207 | Type* composed_union = T.Union(representation_union, semantic_union); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 208 | CHECK(direct_union->Equals(composed_union)); |
| 209 | } |
| 210 | } |
| 211 | |
| 212 | // Pointwiseness of Intersect. |
| 213 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 214 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 215 | Type* type1 = *it1; |
| 216 | Type* type2 = *it2; |
| 217 | Type* representation1 = T.Representation(type1); |
| 218 | Type* semantic1 = T.Semantic(type1); |
| 219 | Type* representation2 = T.Representation(type2); |
| 220 | Type* semantic2 = T.Semantic(type2); |
| 221 | Type* direct_intersection = T.Intersect(type1, type2); |
| 222 | Type* representation_intersection = |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 223 | T.Intersect(representation1, representation2); |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 224 | Type* semantic_intersection = T.Intersect(semantic1, semantic2); |
| 225 | Type* composed_intersection = |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 226 | T.Union(representation_intersection, semantic_intersection); |
| 227 | CHECK(direct_intersection->Equals(composed_intersection)); |
| 228 | } |
| 229 | } |
| 230 | |
| 231 | // Pointwiseness of Is. |
| 232 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 233 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 234 | Type* type1 = *it1; |
| 235 | Type* type2 = *it2; |
| 236 | Type* representation1 = T.Representation(type1); |
| 237 | Type* semantic1 = T.Semantic(type1); |
| 238 | Type* representation2 = T.Representation(type2); |
| 239 | Type* semantic2 = T.Semantic(type2); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 240 | bool representation_is = representation1->Is(representation2); |
| 241 | bool semantic_is = semantic1->Is(semantic2); |
| 242 | bool direct_is = type1->Is(type2); |
| 243 | CHECK(direct_is == (semantic_is && representation_is)); |
| 244 | } |
| 245 | } |
| 246 | } |
| 247 | |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 248 | void Class() { |
| 249 | // Constructor |
| 250 | for (MapIterator mt = T.maps.begin(); mt != T.maps.end(); ++mt) { |
| 251 | Handle<i::Map> map = *mt; |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 252 | Type* type = T.Class(map); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 253 | CHECK(type->IsClass()); |
| 254 | } |
| 255 | |
| 256 | // Map attribute |
| 257 | for (MapIterator mt = T.maps.begin(); mt != T.maps.end(); ++mt) { |
| 258 | Handle<i::Map> map = *mt; |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 259 | Type* type = T.Class(map); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 260 | CHECK(*map == *type->AsClass()->Map()); |
| 261 | } |
| 262 | |
| 263 | // Functionality & Injectivity: Class(M1) = Class(M2) iff M1 = M2 |
| 264 | for (MapIterator mt1 = T.maps.begin(); mt1 != T.maps.end(); ++mt1) { |
| 265 | for (MapIterator mt2 = T.maps.begin(); mt2 != T.maps.end(); ++mt2) { |
| 266 | Handle<i::Map> map1 = *mt1; |
| 267 | Handle<i::Map> map2 = *mt2; |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 268 | Type* type1 = T.Class(map1); |
| 269 | Type* type2 = T.Class(map2); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 270 | CHECK(Equal(type1, type2) == (*map1 == *map2)); |
| 271 | } |
| 272 | } |
| 273 | } |
| 274 | |
| 275 | void Constant() { |
| 276 | // Constructor |
| 277 | for (ValueIterator vt = T.values.begin(); vt != T.values.end(); ++vt) { |
| 278 | Handle<i::Object> value = *vt; |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 279 | Type* type = T.Constant(value); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 280 | CHECK(type->IsConstant()); |
| 281 | } |
| 282 | |
| 283 | // Value attribute |
| 284 | for (ValueIterator vt = T.values.begin(); vt != T.values.end(); ++vt) { |
| 285 | Handle<i::Object> value = *vt; |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 286 | Type* type = T.Constant(value); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 287 | CHECK(*value == *type->AsConstant()->Value()); |
| 288 | } |
| 289 | |
| 290 | // Functionality & Injectivity: Constant(V1) = Constant(V2) iff V1 = V2 |
| 291 | for (ValueIterator vt1 = T.values.begin(); vt1 != T.values.end(); ++vt1) { |
| 292 | for (ValueIterator vt2 = T.values.begin(); vt2 != T.values.end(); ++vt2) { |
| 293 | Handle<i::Object> value1 = *vt1; |
| 294 | Handle<i::Object> value2 = *vt2; |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 295 | Type* type1 = T.Constant(value1); |
| 296 | Type* type2 = T.Constant(value2); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 297 | CHECK(Equal(type1, type2) == (*value1 == *value2)); |
| 298 | } |
| 299 | } |
| 300 | |
| 301 | // Typing of numbers |
| 302 | Factory* fac = isolate->factory(); |
| 303 | CHECK(T.Constant(fac->NewNumber(0))->Is(T.UnsignedSmall)); |
| 304 | CHECK(T.Constant(fac->NewNumber(1))->Is(T.UnsignedSmall)); |
| 305 | CHECK(T.Constant(fac->NewNumber(0x3fffffff))->Is(T.UnsignedSmall)); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 306 | CHECK(T.Constant(fac->NewNumber(-1))->Is(T.Negative31)); |
| 307 | CHECK(T.Constant(fac->NewNumber(-0x3fffffff))->Is(T.Negative31)); |
| 308 | CHECK(T.Constant(fac->NewNumber(-0x40000000))->Is(T.Negative31)); |
| 309 | CHECK(T.Constant(fac->NewNumber(0x40000000))->Is(T.Unsigned31)); |
| 310 | CHECK(!T.Constant(fac->NewNumber(0x40000000))->Is(T.Unsigned30)); |
| 311 | CHECK(T.Constant(fac->NewNumber(0x7fffffff))->Is(T.Unsigned31)); |
| 312 | CHECK(!T.Constant(fac->NewNumber(0x7fffffff))->Is(T.Unsigned30)); |
| 313 | CHECK(T.Constant(fac->NewNumber(-0x40000001))->Is(T.Negative32)); |
| 314 | CHECK(!T.Constant(fac->NewNumber(-0x40000001))->Is(T.Negative31)); |
| 315 | CHECK(T.Constant(fac->NewNumber(-0x7fffffff))->Is(T.Negative32)); |
| 316 | CHECK(!T.Constant(fac->NewNumber(-0x7fffffff - 1))->Is(T.Negative31)); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 317 | if (SmiValuesAre31Bits()) { |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 318 | CHECK(!T.Constant(fac->NewNumber(0x40000000))->Is(T.UnsignedSmall)); |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 319 | CHECK(!T.Constant(fac->NewNumber(0x7fffffff))->Is(T.UnsignedSmall)); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 320 | CHECK(!T.Constant(fac->NewNumber(-0x40000001))->Is(T.SignedSmall)); |
| 321 | CHECK(!T.Constant(fac->NewNumber(-0x7fffffff - 1))->Is(T.SignedSmall)); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 322 | } else { |
| 323 | CHECK(SmiValuesAre32Bits()); |
| 324 | CHECK(T.Constant(fac->NewNumber(0x40000000))->Is(T.UnsignedSmall)); |
| 325 | CHECK(T.Constant(fac->NewNumber(0x7fffffff))->Is(T.UnsignedSmall)); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 326 | CHECK(T.Constant(fac->NewNumber(-0x40000001))->Is(T.SignedSmall)); |
| 327 | CHECK(T.Constant(fac->NewNumber(-0x7fffffff - 1))->Is(T.SignedSmall)); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 328 | } |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 329 | CHECK(T.Constant(fac->NewNumber(0x80000000u))->Is(T.Unsigned32)); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 330 | CHECK(!T.Constant(fac->NewNumber(0x80000000u))->Is(T.Unsigned31)); |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 331 | CHECK(T.Constant(fac->NewNumber(0xffffffffu))->Is(T.Unsigned32)); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 332 | CHECK(!T.Constant(fac->NewNumber(0xffffffffu))->Is(T.Unsigned31)); |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 333 | CHECK(T.Constant(fac->NewNumber(0xffffffffu + 1.0))->Is(T.PlainNumber)); |
| 334 | CHECK(!T.Constant(fac->NewNumber(0xffffffffu + 1.0))->Is(T.Integral32)); |
| 335 | CHECK(T.Constant(fac->NewNumber(-0x7fffffff - 2.0))->Is(T.PlainNumber)); |
| 336 | CHECK(!T.Constant(fac->NewNumber(-0x7fffffff - 2.0))->Is(T.Integral32)); |
| 337 | CHECK(T.Constant(fac->NewNumber(0.1))->Is(T.PlainNumber)); |
| 338 | CHECK(!T.Constant(fac->NewNumber(0.1))->Is(T.Integral32)); |
| 339 | CHECK(T.Constant(fac->NewNumber(-10.1))->Is(T.PlainNumber)); |
| 340 | CHECK(!T.Constant(fac->NewNumber(-10.1))->Is(T.Integral32)); |
| 341 | CHECK(T.Constant(fac->NewNumber(10e60))->Is(T.PlainNumber)); |
| 342 | CHECK(!T.Constant(fac->NewNumber(10e60))->Is(T.Integral32)); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 343 | CHECK(T.Constant(fac->NewNumber(-1.0*0.0))->Is(T.MinusZero)); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 344 | CHECK(T.Constant(fac->NewNumber(std::numeric_limits<double>::quiet_NaN())) |
| 345 | ->Is(T.NaN)); |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 346 | CHECK(T.Constant(fac->NewNumber(V8_INFINITY))->Is(T.PlainNumber)); |
| 347 | CHECK(!T.Constant(fac->NewNumber(V8_INFINITY))->Is(T.Integral32)); |
| 348 | CHECK(T.Constant(fac->NewNumber(-V8_INFINITY))->Is(T.PlainNumber)); |
| 349 | CHECK(!T.Constant(fac->NewNumber(-V8_INFINITY))->Is(T.Integral32)); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 350 | } |
| 351 | |
| 352 | void Range() { |
| 353 | // Constructor |
| 354 | for (ValueIterator i = T.integers.begin(); i != T.integers.end(); ++i) { |
| 355 | for (ValueIterator j = T.integers.begin(); j != T.integers.end(); ++j) { |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 356 | double min = (*i)->Number(); |
| 357 | double max = (*j)->Number(); |
| 358 | if (min > max) std::swap(min, max); |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 359 | Type* type = T.Range(min, max); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 360 | CHECK(type->IsRange()); |
| 361 | } |
| 362 | } |
| 363 | |
| 364 | // Range attributes |
| 365 | for (ValueIterator i = T.integers.begin(); i != T.integers.end(); ++i) { |
| 366 | for (ValueIterator j = T.integers.begin(); j != T.integers.end(); ++j) { |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 367 | double min = (*i)->Number(); |
| 368 | double max = (*j)->Number(); |
| 369 | if (min > max) std::swap(min, max); |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 370 | Type* type = T.Range(min, max); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 371 | CHECK(min == type->AsRange()->Min()); |
| 372 | CHECK(max == type->AsRange()->Max()); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 373 | } |
| 374 | } |
| 375 | |
| 376 | // Functionality & Injectivity: |
| 377 | // Range(min1, max1) = Range(min2, max2) <=> min1 = min2 /\ max1 = max2 |
| 378 | for (ValueIterator i1 = T.integers.begin(); |
| 379 | i1 != T.integers.end(); ++i1) { |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 380 | for (ValueIterator j1 = i1; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 381 | j1 != T.integers.end(); ++j1) { |
| 382 | for (ValueIterator i2 = T.integers.begin(); |
| 383 | i2 != T.integers.end(); ++i2) { |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 384 | for (ValueIterator j2 = i2; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 385 | j2 != T.integers.end(); ++j2) { |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 386 | double min1 = (*i1)->Number(); |
| 387 | double max1 = (*j1)->Number(); |
| 388 | double min2 = (*i2)->Number(); |
| 389 | double max2 = (*j2)->Number(); |
| 390 | if (min1 > max1) std::swap(min1, max1); |
| 391 | if (min2 > max2) std::swap(min2, max2); |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 392 | Type* type1 = T.Range(min1, max1); |
| 393 | Type* type2 = T.Range(min2, max2); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 394 | CHECK(Equal(type1, type2) == (min1 == min2 && max1 == max2)); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 395 | } |
| 396 | } |
| 397 | } |
| 398 | } |
| 399 | } |
| 400 | |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 401 | void Context() { |
| 402 | // Constructor |
| 403 | for (int i = 0; i < 20; ++i) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 404 | Type* type = T.Random(); |
| 405 | Type* context = T.Context(type); |
| 406 | CHECK(context->IsContext()); |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 407 | } |
| 408 | |
| 409 | // Attributes |
| 410 | for (int i = 0; i < 20; ++i) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 411 | Type* type = T.Random(); |
| 412 | Type* context = T.Context(type); |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 413 | CheckEqual(type, context->AsContext()->Outer()); |
| 414 | } |
| 415 | |
| 416 | // Functionality & Injectivity: Context(T1) = Context(T2) iff T1 = T2 |
| 417 | for (int i = 0; i < 20; ++i) { |
| 418 | for (int j = 0; j < 20; ++j) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 419 | Type* type1 = T.Random(); |
| 420 | Type* type2 = T.Random(); |
| 421 | Type* context1 = T.Context(type1); |
| 422 | Type* context2 = T.Context(type2); |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 423 | CHECK(Equal(context1, context2) == Equal(type1, type2)); |
| 424 | } |
| 425 | } |
| 426 | } |
| 427 | |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 428 | void Array() { |
| 429 | // Constructor |
| 430 | for (int i = 0; i < 20; ++i) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 431 | Type* type = T.Random(); |
| 432 | Type* array = T.Array1(type); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 433 | CHECK(array->IsArray()); |
| 434 | } |
| 435 | |
| 436 | // Attributes |
| 437 | for (int i = 0; i < 20; ++i) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 438 | Type* type = T.Random(); |
| 439 | Type* array = T.Array1(type); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 440 | CheckEqual(type, array->AsArray()->Element()); |
| 441 | } |
| 442 | |
| 443 | // Functionality & Injectivity: Array(T1) = Array(T2) iff T1 = T2 |
| 444 | for (int i = 0; i < 20; ++i) { |
| 445 | for (int j = 0; j < 20; ++j) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 446 | Type* type1 = T.Random(); |
| 447 | Type* type2 = T.Random(); |
| 448 | Type* array1 = T.Array1(type1); |
| 449 | Type* array2 = T.Array1(type2); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 450 | CHECK(Equal(array1, array2) == Equal(type1, type2)); |
| 451 | } |
| 452 | } |
| 453 | } |
| 454 | |
| 455 | void Function() { |
| 456 | // Constructors |
| 457 | for (int i = 0; i < 20; ++i) { |
| 458 | for (int j = 0; j < 20; ++j) { |
| 459 | for (int k = 0; k < 20; ++k) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 460 | Type* type1 = T.Random(); |
| 461 | Type* type2 = T.Random(); |
| 462 | Type* type3 = T.Random(); |
| 463 | Type* function0 = T.Function0(type1, type2); |
| 464 | Type* function1 = T.Function1(type1, type2, type3); |
| 465 | Type* function2 = T.Function2(type1, type2, type3); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 466 | CHECK(function0->IsFunction()); |
| 467 | CHECK(function1->IsFunction()); |
| 468 | CHECK(function2->IsFunction()); |
| 469 | } |
| 470 | } |
| 471 | } |
| 472 | |
| 473 | // Attributes |
| 474 | for (int i = 0; i < 20; ++i) { |
| 475 | for (int j = 0; j < 20; ++j) { |
| 476 | for (int k = 0; k < 20; ++k) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 477 | Type* type1 = T.Random(); |
| 478 | Type* type2 = T.Random(); |
| 479 | Type* type3 = T.Random(); |
| 480 | Type* function0 = T.Function0(type1, type2); |
| 481 | Type* function1 = T.Function1(type1, type2, type3); |
| 482 | Type* function2 = T.Function2(type1, type2, type3); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 483 | CHECK_EQ(0, function0->AsFunction()->Arity()); |
| 484 | CHECK_EQ(1, function1->AsFunction()->Arity()); |
| 485 | CHECK_EQ(2, function2->AsFunction()->Arity()); |
| 486 | CheckEqual(type1, function0->AsFunction()->Result()); |
| 487 | CheckEqual(type1, function1->AsFunction()->Result()); |
| 488 | CheckEqual(type1, function2->AsFunction()->Result()); |
| 489 | CheckEqual(type2, function0->AsFunction()->Receiver()); |
| 490 | CheckEqual(type2, function1->AsFunction()->Receiver()); |
| 491 | CheckEqual(T.Any, function2->AsFunction()->Receiver()); |
| 492 | CheckEqual(type3, function1->AsFunction()->Parameter(0)); |
| 493 | CheckEqual(type2, function2->AsFunction()->Parameter(0)); |
| 494 | CheckEqual(type3, function2->AsFunction()->Parameter(1)); |
| 495 | } |
| 496 | } |
| 497 | } |
| 498 | |
| 499 | // Functionality & Injectivity: Function(Ts1) = Function(Ts2) iff Ts1 = Ts2 |
| 500 | for (int i = 0; i < 20; ++i) { |
| 501 | for (int j = 0; j < 20; ++j) { |
| 502 | for (int k = 0; k < 20; ++k) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 503 | Type* type1 = T.Random(); |
| 504 | Type* type2 = T.Random(); |
| 505 | Type* type3 = T.Random(); |
| 506 | Type* function01 = T.Function0(type1, type2); |
| 507 | Type* function02 = T.Function0(type1, type3); |
| 508 | Type* function03 = T.Function0(type3, type2); |
| 509 | Type* function11 = T.Function1(type1, type2, type2); |
| 510 | Type* function12 = T.Function1(type1, type2, type3); |
| 511 | Type* function21 = T.Function2(type1, type2, type2); |
| 512 | Type* function22 = T.Function2(type1, type2, type3); |
| 513 | Type* function23 = T.Function2(type1, type3, type2); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 514 | CHECK(Equal(function01, function02) == Equal(type2, type3)); |
| 515 | CHECK(Equal(function01, function03) == Equal(type1, type3)); |
| 516 | CHECK(Equal(function11, function12) == Equal(type2, type3)); |
| 517 | CHECK(Equal(function21, function22) == Equal(type2, type3)); |
| 518 | CHECK(Equal(function21, function23) == Equal(type2, type3)); |
| 519 | } |
| 520 | } |
| 521 | } |
| 522 | } |
| 523 | |
| 524 | void Of() { |
| 525 | // Constant(V)->Is(Of(V)) |
| 526 | for (ValueIterator vt = T.values.begin(); vt != T.values.end(); ++vt) { |
| 527 | Handle<i::Object> value = *vt; |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 528 | Type* const_type = T.Constant(value); |
| 529 | Type* of_type = T.Of(value); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 530 | CHECK(const_type->Is(of_type)); |
| 531 | } |
| 532 | |
| 533 | // If Of(V)->Is(T), then Constant(V)->Is(T) |
| 534 | for (ValueIterator vt = T.values.begin(); vt != T.values.end(); ++vt) { |
| 535 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
| 536 | Handle<i::Object> value = *vt; |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 537 | Type* type = *it; |
| 538 | Type* const_type = T.Constant(value); |
| 539 | Type* of_type = T.Of(value); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 540 | CHECK(!of_type->Is(type) || const_type->Is(type)); |
| 541 | } |
| 542 | } |
| 543 | |
| 544 | // If Constant(V)->Is(T), then Of(V)->Is(T) or T->Maybe(Constant(V)) |
| 545 | for (ValueIterator vt = T.values.begin(); vt != T.values.end(); ++vt) { |
| 546 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
| 547 | Handle<i::Object> value = *vt; |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 548 | Type* type = *it; |
| 549 | Type* const_type = T.Constant(value); |
| 550 | Type* of_type = T.Of(value); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 551 | CHECK(!const_type->Is(type) || |
| 552 | of_type->Is(type) || type->Maybe(const_type)); |
| 553 | } |
| 554 | } |
| 555 | } |
| 556 | |
| 557 | void NowOf() { |
| 558 | // Constant(V)->NowIs(NowOf(V)) |
| 559 | for (ValueIterator vt = T.values.begin(); vt != T.values.end(); ++vt) { |
| 560 | Handle<i::Object> value = *vt; |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 561 | Type* const_type = T.Constant(value); |
| 562 | Type* nowof_type = T.NowOf(value); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 563 | CHECK(const_type->NowIs(nowof_type)); |
| 564 | } |
| 565 | |
| 566 | // NowOf(V)->Is(Of(V)) |
| 567 | for (ValueIterator vt = T.values.begin(); vt != T.values.end(); ++vt) { |
| 568 | Handle<i::Object> value = *vt; |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 569 | Type* nowof_type = T.NowOf(value); |
| 570 | Type* of_type = T.Of(value); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 571 | CHECK(nowof_type->Is(of_type)); |
| 572 | } |
| 573 | |
| 574 | // If NowOf(V)->NowIs(T), then Constant(V)->NowIs(T) |
| 575 | for (ValueIterator vt = T.values.begin(); vt != T.values.end(); ++vt) { |
| 576 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
| 577 | Handle<i::Object> value = *vt; |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 578 | Type* type = *it; |
| 579 | Type* const_type = T.Constant(value); |
| 580 | Type* nowof_type = T.NowOf(value); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 581 | CHECK(!nowof_type->NowIs(type) || const_type->NowIs(type)); |
| 582 | } |
| 583 | } |
| 584 | |
| 585 | // If Constant(V)->NowIs(T), |
| 586 | // then NowOf(V)->NowIs(T) or T->Maybe(Constant(V)) |
| 587 | for (ValueIterator vt = T.values.begin(); vt != T.values.end(); ++vt) { |
| 588 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
| 589 | Handle<i::Object> value = *vt; |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 590 | Type* type = *it; |
| 591 | Type* const_type = T.Constant(value); |
| 592 | Type* nowof_type = T.NowOf(value); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 593 | CHECK(!const_type->NowIs(type) || |
| 594 | nowof_type->NowIs(type) || type->Maybe(const_type)); |
| 595 | } |
| 596 | } |
| 597 | |
| 598 | // If Constant(V)->Is(T), |
| 599 | // then NowOf(V)->Is(T) or T->Maybe(Constant(V)) |
| 600 | for (ValueIterator vt = T.values.begin(); vt != T.values.end(); ++vt) { |
| 601 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
| 602 | Handle<i::Object> value = *vt; |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 603 | Type* type = *it; |
| 604 | Type* const_type = T.Constant(value); |
| 605 | Type* nowof_type = T.NowOf(value); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 606 | CHECK(!const_type->Is(type) || |
| 607 | nowof_type->Is(type) || type->Maybe(const_type)); |
| 608 | } |
| 609 | } |
| 610 | } |
| 611 | |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 612 | void MinMax() { |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 613 | // If b is regular numeric bitset, then Range(b->Min(), b->Max())->Is(b). |
| 614 | // TODO(neis): Need to ignore representation for this to be true. |
| 615 | /* |
| 616 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 617 | Type* type = *it; |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 618 | if (this->IsBitset(type) && type->Is(T.Number) && |
| 619 | !type->Is(T.None) && !type->Is(T.NaN)) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 620 | Type* range = T.Range( |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 621 | isolate->factory()->NewNumber(type->Min()), |
| 622 | isolate->factory()->NewNumber(type->Max())); |
| 623 | CHECK(range->Is(type)); |
| 624 | } |
| 625 | } |
| 626 | */ |
| 627 | |
| 628 | // If b is regular numeric bitset, then b->Min() and b->Max() are integers. |
| 629 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 630 | Type* type = *it; |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 631 | if (this->IsBitset(type) && type->Is(T.Number) && !type->Is(T.NaN)) { |
| 632 | CHECK(IsInteger(type->Min()) && IsInteger(type->Max())); |
| 633 | } |
| 634 | } |
| 635 | |
| 636 | // If b1 and b2 are regular numeric bitsets with b1->Is(b2), then |
| 637 | // b1->Min() >= b2->Min() and b1->Max() <= b2->Max(). |
| 638 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 639 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 640 | Type* type1 = *it1; |
| 641 | Type* type2 = *it2; |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 642 | if (this->IsBitset(type1) && type1->Is(type2) && type2->Is(T.Number) && |
| 643 | !type1->Is(T.NaN) && !type2->Is(T.NaN)) { |
| 644 | CHECK(type1->Min() >= type2->Min()); |
| 645 | CHECK(type1->Max() <= type2->Max()); |
| 646 | } |
| 647 | } |
| 648 | } |
| 649 | |
| 650 | // Lub(Range(x,y))->Min() <= x and y <= Lub(Range(x,y))->Max() |
| 651 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 652 | Type* type = *it; |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 653 | if (type->IsRange()) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 654 | Type* lub = BitsetType::NewForTesting(BitsetType::Lub(type)); |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 655 | CHECK(lub->Min() <= type->Min() && type->Max() <= lub->Max()); |
| 656 | } |
| 657 | } |
| 658 | |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 659 | // Rangification: If T->Is(Range(-inf,+inf)) and T is inhabited, then |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 660 | // T->Is(Range(T->Min(), T->Max())). |
| 661 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 662 | Type* type = *it; |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 663 | CHECK(!type->Is(T.Integer) || !type->IsInhabited() || |
| 664 | type->Is(T.Range(type->Min(), type->Max()))); |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 665 | } |
| 666 | } |
| 667 | |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 668 | void BitsetGlb() { |
| 669 | // Lower: (T->BitsetGlb())->Is(T) |
| 670 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 671 | Type* type = *it; |
| 672 | Type* glb = BitsetType::NewForTesting(BitsetType::Glb(type)); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 673 | CHECK(glb->Is(type)); |
| 674 | } |
| 675 | |
| 676 | // Greatest: If T1->IsBitset() and T1->Is(T2), then T1->Is(T2->BitsetGlb()) |
| 677 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 678 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 679 | Type* type1 = *it1; |
| 680 | Type* type2 = *it2; |
| 681 | Type* glb2 = BitsetType::NewForTesting(BitsetType::Glb(type2)); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 682 | CHECK(!this->IsBitset(type1) || !type1->Is(type2) || type1->Is(glb2)); |
| 683 | } |
| 684 | } |
| 685 | |
| 686 | // Monotonicity: T1->Is(T2) implies (T1->BitsetGlb())->Is(T2->BitsetGlb()) |
| 687 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 688 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 689 | Type* type1 = *it1; |
| 690 | Type* type2 = *it2; |
| 691 | Type* glb1 = BitsetType::NewForTesting(BitsetType::Glb(type1)); |
| 692 | Type* glb2 = BitsetType::NewForTesting(BitsetType::Glb(type2)); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 693 | CHECK(!type1->Is(type2) || glb1->Is(glb2)); |
| 694 | } |
| 695 | } |
| 696 | } |
| 697 | |
| 698 | void BitsetLub() { |
| 699 | // Upper: T->Is(T->BitsetLub()) |
| 700 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 701 | Type* type = *it; |
| 702 | Type* lub = BitsetType::NewForTesting(BitsetType::Lub(type)); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 703 | CHECK(type->Is(lub)); |
| 704 | } |
| 705 | |
| 706 | // Least: If T2->IsBitset() and T1->Is(T2), then (T1->BitsetLub())->Is(T2) |
| 707 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 708 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 709 | Type* type1 = *it1; |
| 710 | Type* type2 = *it2; |
| 711 | Type* lub1 = BitsetType::NewForTesting(BitsetType::Lub(type1)); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 712 | CHECK(!this->IsBitset(type2) || !type1->Is(type2) || lub1->Is(type2)); |
| 713 | } |
| 714 | } |
| 715 | |
| 716 | // Monotonicity: T1->Is(T2) implies (T1->BitsetLub())->Is(T2->BitsetLub()) |
| 717 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 718 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 719 | Type* type1 = *it1; |
| 720 | Type* type2 = *it2; |
| 721 | Type* lub1 = BitsetType::NewForTesting(BitsetType::Lub(type1)); |
| 722 | Type* lub2 = BitsetType::NewForTesting(BitsetType::Lub(type2)); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 723 | CHECK(!type1->Is(type2) || lub1->Is(lub2)); |
| 724 | } |
| 725 | } |
| 726 | } |
| 727 | |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 728 | void Is1() { |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 729 | // Least Element (Bottom): None->Is(T) |
| 730 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 731 | Type* type = *it; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 732 | CHECK(T.None->Is(type)); |
| 733 | } |
| 734 | |
| 735 | // Greatest Element (Top): T->Is(Any) |
| 736 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 737 | Type* type = *it; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 738 | CHECK(type->Is(T.Any)); |
| 739 | } |
| 740 | |
| 741 | // Bottom Uniqueness: T->Is(None) implies T = None |
| 742 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 743 | Type* type = *it; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 744 | if (type->Is(T.None)) CheckEqual(type, T.None); |
| 745 | } |
| 746 | |
| 747 | // Top Uniqueness: Any->Is(T) implies T = Any |
| 748 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 749 | Type* type = *it; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 750 | if (T.Any->Is(type)) CheckEqual(type, T.Any); |
| 751 | } |
| 752 | |
| 753 | // Reflexivity: T->Is(T) |
| 754 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 755 | Type* type = *it; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 756 | CHECK(type->Is(type)); |
| 757 | } |
| 758 | |
| 759 | // Transitivity: T1->Is(T2) and T2->Is(T3) implies T1->Is(T3) |
| 760 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 761 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
| 762 | for (TypeIterator it3 = T.types.begin(); it3 != T.types.end(); ++it3) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 763 | Type* type1 = *it1; |
| 764 | Type* type2 = *it2; |
| 765 | Type* type3 = *it3; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 766 | CHECK(!(type1->Is(type2) && type2->Is(type3)) || type1->Is(type3)); |
| 767 | } |
| 768 | } |
| 769 | } |
| 770 | |
| 771 | // Antisymmetry: T1->Is(T2) and T2->Is(T1) iff T1 = T2 |
| 772 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 773 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 774 | Type* type1 = *it1; |
| 775 | Type* type2 = *it2; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 776 | CHECK((type1->Is(type2) && type2->Is(type1)) == Equal(type1, type2)); |
| 777 | } |
| 778 | } |
| 779 | |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 780 | // (In-)Compatibilities. |
| 781 | for (TypeIterator i = T.types.begin(); i != T.types.end(); ++i) { |
| 782 | for (TypeIterator j = T.types.begin(); j != T.types.end(); ++j) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 783 | Type* type1 = *i; |
| 784 | Type* type2 = *j; |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 785 | CHECK(!type1->Is(type2) || this->IsBitset(type2) || |
| 786 | this->IsUnion(type2) || this->IsUnion(type1) || |
| 787 | (type1->IsClass() && type2->IsClass()) || |
| 788 | (type1->IsConstant() && type2->IsConstant()) || |
| 789 | (type1->IsConstant() && type2->IsRange()) || |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 790 | (this->IsBitset(type1) && type2->IsRange()) || |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 791 | (type1->IsRange() && type2->IsRange()) || |
| 792 | (type1->IsContext() && type2->IsContext()) || |
| 793 | (type1->IsArray() && type2->IsArray()) || |
| 794 | (type1->IsFunction() && type2->IsFunction()) || |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 795 | !type1->IsInhabited()); |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 796 | } |
| 797 | } |
| 798 | } |
| 799 | |
| 800 | void Is2() { |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 801 | // Class(M1)->Is(Class(M2)) iff M1 = M2 |
| 802 | for (MapIterator mt1 = T.maps.begin(); mt1 != T.maps.end(); ++mt1) { |
| 803 | for (MapIterator mt2 = T.maps.begin(); mt2 != T.maps.end(); ++mt2) { |
| 804 | Handle<i::Map> map1 = *mt1; |
| 805 | Handle<i::Map> map2 = *mt2; |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 806 | Type* class_type1 = T.Class(map1); |
| 807 | Type* class_type2 = T.Class(map2); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 808 | CHECK(class_type1->Is(class_type2) == (*map1 == *map2)); |
| 809 | } |
| 810 | } |
| 811 | |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 812 | // Range(X1, Y1)->Is(Range(X2, Y2)) iff X1 >= X2 /\ Y1 <= Y2 |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 813 | for (ValueIterator i1 = T.integers.begin(); |
| 814 | i1 != T.integers.end(); ++i1) { |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 815 | for (ValueIterator j1 = i1; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 816 | j1 != T.integers.end(); ++j1) { |
| 817 | for (ValueIterator i2 = T.integers.begin(); |
| 818 | i2 != T.integers.end(); ++i2) { |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 819 | for (ValueIterator j2 = i2; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 820 | j2 != T.integers.end(); ++j2) { |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 821 | double min1 = (*i1)->Number(); |
| 822 | double max1 = (*j1)->Number(); |
| 823 | double min2 = (*i2)->Number(); |
| 824 | double max2 = (*j2)->Number(); |
| 825 | if (min1 > max1) std::swap(min1, max1); |
| 826 | if (min2 > max2) std::swap(min2, max2); |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 827 | Type* type1 = T.Range(min1, max1); |
| 828 | Type* type2 = T.Range(min2, max2); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 829 | CHECK(type1->Is(type2) == (min1 >= min2 && max1 <= max2)); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 830 | } |
| 831 | } |
| 832 | } |
| 833 | } |
| 834 | |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 835 | // Constant(V1)->Is(Constant(V2)) iff V1 = V2 |
| 836 | for (ValueIterator vt1 = T.values.begin(); vt1 != T.values.end(); ++vt1) { |
| 837 | for (ValueIterator vt2 = T.values.begin(); vt2 != T.values.end(); ++vt2) { |
| 838 | Handle<i::Object> value1 = *vt1; |
| 839 | Handle<i::Object> value2 = *vt2; |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 840 | Type* const_type1 = T.Constant(value1); |
| 841 | Type* const_type2 = T.Constant(value2); |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 842 | CHECK(const_type1->Is(const_type2) == (*value1 == *value2)); |
| 843 | } |
| 844 | } |
| 845 | |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 846 | // Context(T1)->Is(Context(T2)) iff T1 = T2 |
| 847 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 848 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 849 | Type* outer1 = *it1; |
| 850 | Type* outer2 = *it2; |
| 851 | Type* type1 = T.Context(outer1); |
| 852 | Type* type2 = T.Context(outer2); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 853 | CHECK(type1->Is(type2) == outer1->Equals(outer2)); |
| 854 | } |
| 855 | } |
| 856 | |
| 857 | // Array(T1)->Is(Array(T2)) iff T1 = T2 |
| 858 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 859 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 860 | Type* element1 = *it1; |
| 861 | Type* element2 = *it2; |
| 862 | Type* type1 = T.Array1(element1); |
| 863 | Type* type2 = T.Array1(element2); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 864 | CHECK(type1->Is(type2) == element1->Equals(element2)); |
| 865 | } |
| 866 | } |
| 867 | |
| 868 | // Function0(S1, T1)->Is(Function0(S2, T2)) iff S1 = S2 and T1 = T2 |
| 869 | for (TypeIterator i = T.types.begin(); i != T.types.end(); ++i) { |
| 870 | for (TypeIterator j = T.types.begin(); j != T.types.end(); ++j) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 871 | Type* result1 = *i; |
| 872 | Type* receiver1 = *j; |
| 873 | Type* type1 = T.Function0(result1, receiver1); |
| 874 | Type* result2 = T.Random(); |
| 875 | Type* receiver2 = T.Random(); |
| 876 | Type* type2 = T.Function0(result2, receiver2); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 877 | CHECK(type1->Is(type2) == |
| 878 | (result1->Equals(result2) && receiver1->Equals(receiver2))); |
| 879 | } |
| 880 | } |
| 881 | |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 882 | |
| 883 | // Range-specific subtyping |
| 884 | |
| 885 | // If IsInteger(v) then Constant(v)->Is(Range(v, v)). |
| 886 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 887 | Type* type = *it; |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 888 | if (type->IsConstant() && IsInteger(*type->AsConstant()->Value())) { |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 889 | CHECK(type->Is(T.Range(type->AsConstant()->Value()->Number(), |
| 890 | type->AsConstant()->Value()->Number()))); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 891 | } |
| 892 | } |
| 893 | |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 894 | // If Constant(x)->Is(Range(min,max)) then IsInteger(v) and min <= x <= max. |
| 895 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 896 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 897 | Type* type1 = *it1; |
| 898 | Type* type2 = *it2; |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 899 | if (type1->IsConstant() && type2->IsRange() && type1->Is(type2)) { |
| 900 | double x = type1->AsConstant()->Value()->Number(); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 901 | double min = type2->AsRange()->Min(); |
| 902 | double max = type2->AsRange()->Max(); |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 903 | CHECK(IsInteger(x) && min <= x && x <= max); |
| 904 | } |
| 905 | } |
| 906 | } |
| 907 | |
| 908 | // Lub(Range(x,y))->Is(T.Union(T.Integral32, T.OtherNumber)) |
| 909 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 910 | Type* type = *it; |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 911 | if (type->IsRange()) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 912 | Type* lub = BitsetType::NewForTesting(BitsetType::Lub(type)); |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 913 | CHECK(lub->Is(T.PlainNumber)); |
| 914 | } |
| 915 | } |
| 916 | |
| 917 | |
| 918 | // Subtyping between concrete basic types |
| 919 | |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 920 | CheckUnordered(T.Boolean, T.Null); |
| 921 | CheckUnordered(T.Undefined, T.Null); |
| 922 | CheckUnordered(T.Boolean, T.Undefined); |
| 923 | |
| 924 | CheckSub(T.SignedSmall, T.Number); |
| 925 | CheckSub(T.Signed32, T.Number); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 926 | CheckSubOrEqual(T.SignedSmall, T.Signed32); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 927 | CheckUnordered(T.SignedSmall, T.MinusZero); |
| 928 | CheckUnordered(T.Signed32, T.Unsigned32); |
| 929 | |
| 930 | CheckSub(T.UniqueName, T.Name); |
| 931 | CheckSub(T.String, T.Name); |
| 932 | CheckSub(T.InternalizedString, T.String); |
| 933 | CheckSub(T.InternalizedString, T.UniqueName); |
| 934 | CheckSub(T.InternalizedString, T.Name); |
| 935 | CheckSub(T.Symbol, T.UniqueName); |
| 936 | CheckSub(T.Symbol, T.Name); |
| 937 | CheckUnordered(T.String, T.UniqueName); |
| 938 | CheckUnordered(T.String, T.Symbol); |
| 939 | CheckUnordered(T.InternalizedString, T.Symbol); |
| 940 | |
| 941 | CheckSub(T.Object, T.Receiver); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 942 | CheckSub(T.Proxy, T.Receiver); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 943 | CheckSub(T.OtherObject, T.Object); |
Ben Murdoch | da12d29 | 2016-06-02 14:46:10 +0100 | [diff] [blame] | 944 | CheckSub(T.OtherUndetectable, T.Object); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 945 | CheckSub(T.OtherObject, T.Object); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 946 | |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 947 | CheckUnordered(T.Object, T.Proxy); |
| 948 | CheckUnordered(T.OtherObject, T.Undetectable); |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 949 | |
| 950 | // Subtyping between concrete structural types |
| 951 | |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 952 | CheckSub(T.ObjectClass, T.Object); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 953 | CheckSub(T.ArrayClass, T.OtherObject); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 954 | CheckSub(T.UninitializedClass, T.Internal); |
| 955 | CheckUnordered(T.ObjectClass, T.ArrayClass); |
| 956 | CheckUnordered(T.UninitializedClass, T.Null); |
| 957 | CheckUnordered(T.UninitializedClass, T.Undefined); |
| 958 | |
| 959 | CheckSub(T.SmiConstant, T.SignedSmall); |
| 960 | CheckSub(T.SmiConstant, T.Signed32); |
| 961 | CheckSub(T.SmiConstant, T.Number); |
| 962 | CheckSub(T.ObjectConstant1, T.Object); |
| 963 | CheckSub(T.ObjectConstant2, T.Object); |
| 964 | CheckSub(T.ArrayConstant, T.Object); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 965 | CheckSub(T.ArrayConstant, T.OtherObject); |
| 966 | CheckSub(T.ArrayConstant, T.Receiver); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 967 | CheckSub(T.UninitializedConstant, T.Internal); |
| 968 | CheckUnordered(T.ObjectConstant1, T.ObjectConstant2); |
| 969 | CheckUnordered(T.ObjectConstant1, T.ArrayConstant); |
| 970 | CheckUnordered(T.UninitializedConstant, T.Null); |
| 971 | CheckUnordered(T.UninitializedConstant, T.Undefined); |
| 972 | |
| 973 | CheckUnordered(T.ObjectConstant1, T.ObjectClass); |
| 974 | CheckUnordered(T.ObjectConstant2, T.ObjectClass); |
| 975 | CheckUnordered(T.ObjectConstant1, T.ArrayClass); |
| 976 | CheckUnordered(T.ObjectConstant2, T.ArrayClass); |
| 977 | CheckUnordered(T.ArrayConstant, T.ObjectClass); |
| 978 | |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 979 | CheckSub(T.NumberArray, T.OtherObject); |
| 980 | CheckSub(T.NumberArray, T.Receiver); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 981 | CheckSub(T.NumberArray, T.Object); |
| 982 | CheckUnordered(T.StringArray, T.AnyArray); |
| 983 | |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 984 | CheckSub(T.MethodFunction, T.Object); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 985 | CheckSub(T.NumberFunction1, T.Object); |
| 986 | CheckUnordered(T.SignedFunction1, T.NumberFunction1); |
| 987 | CheckUnordered(T.NumberFunction1, T.NumberFunction2); |
| 988 | } |
| 989 | |
| 990 | void NowIs() { |
| 991 | // Least Element (Bottom): None->NowIs(T) |
| 992 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 993 | Type* type = *it; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 994 | CHECK(T.None->NowIs(type)); |
| 995 | } |
| 996 | |
| 997 | // Greatest Element (Top): T->NowIs(Any) |
| 998 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 999 | Type* type = *it; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1000 | CHECK(type->NowIs(T.Any)); |
| 1001 | } |
| 1002 | |
| 1003 | // Bottom Uniqueness: T->NowIs(None) implies T = None |
| 1004 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1005 | Type* type = *it; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1006 | if (type->NowIs(T.None)) CheckEqual(type, T.None); |
| 1007 | } |
| 1008 | |
| 1009 | // Top Uniqueness: Any->NowIs(T) implies T = Any |
| 1010 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1011 | Type* type = *it; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1012 | if (T.Any->NowIs(type)) CheckEqual(type, T.Any); |
| 1013 | } |
| 1014 | |
| 1015 | // Reflexivity: T->NowIs(T) |
| 1016 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1017 | Type* type = *it; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1018 | CHECK(type->NowIs(type)); |
| 1019 | } |
| 1020 | |
| 1021 | // Transitivity: T1->NowIs(T2) and T2->NowIs(T3) implies T1->NowIs(T3) |
| 1022 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 1023 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
| 1024 | for (TypeIterator it3 = T.types.begin(); it3 != T.types.end(); ++it3) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1025 | Type* type1 = *it1; |
| 1026 | Type* type2 = *it2; |
| 1027 | Type* type3 = *it3; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1028 | CHECK(!(type1->NowIs(type2) && type2->NowIs(type3)) || |
| 1029 | type1->NowIs(type3)); |
| 1030 | } |
| 1031 | } |
| 1032 | } |
| 1033 | |
| 1034 | // Antisymmetry: T1->NowIs(T2) and T2->NowIs(T1) iff T1 = T2 |
| 1035 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 1036 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1037 | Type* type1 = *it1; |
| 1038 | Type* type2 = *it2; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1039 | CHECK((type1->NowIs(type2) && type2->NowIs(type1)) == |
| 1040 | Equal(type1, type2)); |
| 1041 | } |
| 1042 | } |
| 1043 | |
| 1044 | // T1->Is(T2) implies T1->NowIs(T2) |
| 1045 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 1046 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1047 | Type* type1 = *it1; |
| 1048 | Type* type2 = *it2; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1049 | CHECK(!type1->Is(type2) || type1->NowIs(type2)); |
| 1050 | } |
| 1051 | } |
| 1052 | |
| 1053 | // Constant(V1)->NowIs(Constant(V2)) iff V1 = V2 |
| 1054 | for (ValueIterator vt1 = T.values.begin(); vt1 != T.values.end(); ++vt1) { |
| 1055 | for (ValueIterator vt2 = T.values.begin(); vt2 != T.values.end(); ++vt2) { |
| 1056 | Handle<i::Object> value1 = *vt1; |
| 1057 | Handle<i::Object> value2 = *vt2; |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1058 | Type* const_type1 = T.Constant(value1); |
| 1059 | Type* const_type2 = T.Constant(value2); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1060 | CHECK(const_type1->NowIs(const_type2) == (*value1 == *value2)); |
| 1061 | } |
| 1062 | } |
| 1063 | |
| 1064 | // Class(M1)->NowIs(Class(M2)) iff M1 = M2 |
| 1065 | for (MapIterator mt1 = T.maps.begin(); mt1 != T.maps.end(); ++mt1) { |
| 1066 | for (MapIterator mt2 = T.maps.begin(); mt2 != T.maps.end(); ++mt2) { |
| 1067 | Handle<i::Map> map1 = *mt1; |
| 1068 | Handle<i::Map> map2 = *mt2; |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1069 | Type* class_type1 = T.Class(map1); |
| 1070 | Type* class_type2 = T.Class(map2); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1071 | CHECK(class_type1->NowIs(class_type2) == (*map1 == *map2)); |
| 1072 | } |
| 1073 | } |
| 1074 | |
| 1075 | // Constant(V)->NowIs(Class(M)) iff V has map M |
| 1076 | for (MapIterator mt = T.maps.begin(); mt != T.maps.end(); ++mt) { |
| 1077 | for (ValueIterator vt = T.values.begin(); vt != T.values.end(); ++vt) { |
| 1078 | Handle<i::Map> map = *mt; |
| 1079 | Handle<i::Object> value = *vt; |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1080 | Type* const_type = T.Constant(value); |
| 1081 | Type* class_type = T.Class(map); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1082 | CHECK((value->IsHeapObject() && |
| 1083 | i::HeapObject::cast(*value)->map() == *map) |
| 1084 | == const_type->NowIs(class_type)); |
| 1085 | } |
| 1086 | } |
| 1087 | |
| 1088 | // Class(M)->NowIs(Constant(V)) never |
| 1089 | for (MapIterator mt = T.maps.begin(); mt != T.maps.end(); ++mt) { |
| 1090 | for (ValueIterator vt = T.values.begin(); vt != T.values.end(); ++vt) { |
| 1091 | Handle<i::Map> map = *mt; |
| 1092 | Handle<i::Object> value = *vt; |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1093 | Type* const_type = T.Constant(value); |
| 1094 | Type* class_type = T.Class(map); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1095 | CHECK(!class_type->NowIs(const_type)); |
| 1096 | } |
| 1097 | } |
| 1098 | } |
| 1099 | |
| 1100 | void Contains() { |
| 1101 | // T->Contains(V) iff Constant(V)->Is(T) |
| 1102 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
| 1103 | for (ValueIterator vt = T.values.begin(); vt != T.values.end(); ++vt) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1104 | Type* type = *it; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1105 | Handle<i::Object> value = *vt; |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1106 | Type* const_type = T.Constant(value); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1107 | CHECK(type->Contains(value) == const_type->Is(type)); |
| 1108 | } |
| 1109 | } |
| 1110 | } |
| 1111 | |
| 1112 | void NowContains() { |
| 1113 | // T->NowContains(V) iff Constant(V)->NowIs(T) |
| 1114 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
| 1115 | for (ValueIterator vt = T.values.begin(); vt != T.values.end(); ++vt) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1116 | Type* type = *it; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1117 | Handle<i::Object> value = *vt; |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1118 | Type* const_type = T.Constant(value); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1119 | CHECK(type->NowContains(value) == const_type->NowIs(type)); |
| 1120 | } |
| 1121 | } |
| 1122 | |
| 1123 | // T->Contains(V) implies T->NowContains(V) |
| 1124 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
| 1125 | for (ValueIterator vt = T.values.begin(); vt != T.values.end(); ++vt) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1126 | Type* type = *it; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1127 | Handle<i::Object> value = *vt; |
| 1128 | CHECK(!type->Contains(value) || type->NowContains(value)); |
| 1129 | } |
| 1130 | } |
| 1131 | |
| 1132 | // NowOf(V)->Is(T) implies T->NowContains(V) |
| 1133 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
| 1134 | for (ValueIterator vt = T.values.begin(); vt != T.values.end(); ++vt) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1135 | Type* type = *it; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1136 | Handle<i::Object> value = *vt; |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1137 | Type* nowof_type = T.Of(value); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1138 | CHECK(!nowof_type->NowIs(type) || type->NowContains(value)); |
| 1139 | } |
| 1140 | } |
| 1141 | } |
| 1142 | |
| 1143 | void Maybe() { |
| 1144 | // T->Maybe(Any) iff T inhabited |
| 1145 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1146 | Type* type = *it; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1147 | CHECK(type->Maybe(T.Any) == type->IsInhabited()); |
| 1148 | } |
| 1149 | |
| 1150 | // T->Maybe(None) never |
| 1151 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1152 | Type* type = *it; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1153 | CHECK(!type->Maybe(T.None)); |
| 1154 | } |
| 1155 | |
| 1156 | // Reflexivity upto Inhabitation: T->Maybe(T) iff T inhabited |
| 1157 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1158 | Type* type = *it; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1159 | CHECK(type->Maybe(type) == type->IsInhabited()); |
| 1160 | } |
| 1161 | |
| 1162 | // Symmetry: T1->Maybe(T2) iff T2->Maybe(T1) |
| 1163 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 1164 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1165 | Type* type1 = *it1; |
| 1166 | Type* type2 = *it2; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1167 | CHECK(type1->Maybe(type2) == type2->Maybe(type1)); |
| 1168 | } |
| 1169 | } |
| 1170 | |
| 1171 | // T1->Maybe(T2) implies T1, T2 inhabited |
| 1172 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 1173 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1174 | Type* type1 = *it1; |
| 1175 | Type* type2 = *it2; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1176 | CHECK(!type1->Maybe(type2) || |
| 1177 | (type1->IsInhabited() && type2->IsInhabited())); |
| 1178 | } |
| 1179 | } |
| 1180 | |
| 1181 | // T1->Maybe(T2) implies Intersect(T1, T2) inhabited |
| 1182 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 1183 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1184 | Type* type1 = *it1; |
| 1185 | Type* type2 = *it2; |
| 1186 | Type* intersect12 = T.Intersect(type1, type2); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1187 | CHECK(!type1->Maybe(type2) || intersect12->IsInhabited()); |
| 1188 | } |
| 1189 | } |
| 1190 | |
| 1191 | // T1->Is(T2) and T1 inhabited implies T1->Maybe(T2) |
| 1192 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 1193 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1194 | Type* type1 = *it1; |
| 1195 | Type* type2 = *it2; |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1196 | CHECK(!(type1->Is(type2) && type1->IsInhabited()) || |
| 1197 | type1->Maybe(type2)); |
| 1198 | } |
| 1199 | } |
| 1200 | |
| 1201 | // Constant(V1)->Maybe(Constant(V2)) iff V1 = V2 |
| 1202 | for (ValueIterator vt1 = T.values.begin(); vt1 != T.values.end(); ++vt1) { |
| 1203 | for (ValueIterator vt2 = T.values.begin(); vt2 != T.values.end(); ++vt2) { |
| 1204 | Handle<i::Object> value1 = *vt1; |
| 1205 | Handle<i::Object> value2 = *vt2; |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1206 | Type* const_type1 = T.Constant(value1); |
| 1207 | Type* const_type2 = T.Constant(value2); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1208 | CHECK(const_type1->Maybe(const_type2) == (*value1 == *value2)); |
| 1209 | } |
| 1210 | } |
| 1211 | |
| 1212 | // Class(M1)->Maybe(Class(M2)) iff M1 = M2 |
| 1213 | for (MapIterator mt1 = T.maps.begin(); mt1 != T.maps.end(); ++mt1) { |
| 1214 | for (MapIterator mt2 = T.maps.begin(); mt2 != T.maps.end(); ++mt2) { |
| 1215 | Handle<i::Map> map1 = *mt1; |
| 1216 | Handle<i::Map> map2 = *mt2; |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1217 | Type* class_type1 = T.Class(map1); |
| 1218 | Type* class_type2 = T.Class(map2); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1219 | CHECK(class_type1->Maybe(class_type2) == (*map1 == *map2)); |
| 1220 | } |
| 1221 | } |
| 1222 | |
| 1223 | // Constant(V)->Maybe(Class(M)) never |
| 1224 | // This does NOT hold! |
| 1225 | /* |
| 1226 | for (MapIterator mt = T.maps.begin(); mt != T.maps.end(); ++mt) { |
| 1227 | for (ValueIterator vt = T.values.begin(); vt != T.values.end(); ++vt) { |
| 1228 | Handle<i::Map> map = *mt; |
| 1229 | Handle<i::Object> value = *vt; |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1230 | Type* const_type = T.Constant(value); |
| 1231 | Type* class_type = T.Class(map); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1232 | CHECK(!const_type->Maybe(class_type)); |
| 1233 | } |
| 1234 | } |
| 1235 | */ |
| 1236 | |
| 1237 | // Class(M)->Maybe(Constant(V)) never |
| 1238 | // This does NOT hold! |
| 1239 | /* |
| 1240 | for (MapIterator mt = T.maps.begin(); mt != T.maps.end(); ++mt) { |
| 1241 | for (ValueIterator vt = T.values.begin(); vt != T.values.end(); ++vt) { |
| 1242 | Handle<i::Map> map = *mt; |
| 1243 | Handle<i::Object> value = *vt; |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1244 | Type* const_type = T.Constant(value); |
| 1245 | Type* class_type = T.Class(map); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1246 | CHECK(!class_type->Maybe(const_type)); |
| 1247 | } |
| 1248 | } |
| 1249 | */ |
| 1250 | |
| 1251 | // Basic types |
| 1252 | CheckDisjoint(T.Boolean, T.Null); |
| 1253 | CheckDisjoint(T.Undefined, T.Null); |
| 1254 | CheckDisjoint(T.Boolean, T.Undefined); |
| 1255 | CheckOverlap(T.SignedSmall, T.Number); |
| 1256 | CheckOverlap(T.NaN, T.Number); |
| 1257 | CheckDisjoint(T.Signed32, T.NaN); |
| 1258 | CheckOverlap(T.UniqueName, T.Name); |
| 1259 | CheckOverlap(T.String, T.Name); |
| 1260 | CheckOverlap(T.InternalizedString, T.String); |
| 1261 | CheckOverlap(T.InternalizedString, T.UniqueName); |
| 1262 | CheckOverlap(T.InternalizedString, T.Name); |
| 1263 | CheckOverlap(T.Symbol, T.UniqueName); |
| 1264 | CheckOverlap(T.Symbol, T.Name); |
| 1265 | CheckOverlap(T.String, T.UniqueName); |
| 1266 | CheckDisjoint(T.String, T.Symbol); |
| 1267 | CheckDisjoint(T.InternalizedString, T.Symbol); |
| 1268 | CheckOverlap(T.Object, T.Receiver); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 1269 | CheckOverlap(T.OtherObject, T.Object); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1270 | CheckOverlap(T.Proxy, T.Receiver); |
| 1271 | CheckDisjoint(T.Object, T.Proxy); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1272 | |
| 1273 | // Structural types |
| 1274 | CheckOverlap(T.ObjectClass, T.Object); |
| 1275 | CheckOverlap(T.ArrayClass, T.Object); |
| 1276 | CheckOverlap(T.ObjectClass, T.ObjectClass); |
| 1277 | CheckOverlap(T.ArrayClass, T.ArrayClass); |
| 1278 | CheckDisjoint(T.ObjectClass, T.ArrayClass); |
| 1279 | CheckOverlap(T.SmiConstant, T.SignedSmall); |
| 1280 | CheckOverlap(T.SmiConstant, T.Signed32); |
| 1281 | CheckOverlap(T.SmiConstant, T.Number); |
| 1282 | CheckOverlap(T.ObjectConstant1, T.Object); |
| 1283 | CheckOverlap(T.ObjectConstant2, T.Object); |
| 1284 | CheckOverlap(T.ArrayConstant, T.Object); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 1285 | CheckOverlap(T.ArrayConstant, T.Receiver); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1286 | CheckOverlap(T.ObjectConstant1, T.ObjectConstant1); |
| 1287 | CheckDisjoint(T.ObjectConstant1, T.ObjectConstant2); |
| 1288 | CheckDisjoint(T.ObjectConstant1, T.ArrayConstant); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 1289 | CheckOverlap(T.ObjectConstant1, T.ArrayClass); |
| 1290 | CheckOverlap(T.ObjectConstant2, T.ArrayClass); |
| 1291 | CheckOverlap(T.ArrayConstant, T.ObjectClass); |
| 1292 | CheckOverlap(T.NumberArray, T.Receiver); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1293 | CheckDisjoint(T.NumberArray, T.AnyArray); |
| 1294 | CheckDisjoint(T.NumberArray, T.StringArray); |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 1295 | CheckOverlap(T.MethodFunction, T.Object); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1296 | CheckDisjoint(T.SignedFunction1, T.NumberFunction1); |
| 1297 | CheckDisjoint(T.SignedFunction1, T.NumberFunction2); |
| 1298 | CheckDisjoint(T.NumberFunction1, T.NumberFunction2); |
| 1299 | CheckDisjoint(T.SignedFunction1, T.MethodFunction); |
| 1300 | CheckOverlap(T.ObjectConstant1, T.ObjectClass); // !!! |
| 1301 | CheckOverlap(T.ObjectConstant2, T.ObjectClass); // !!! |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 1302 | CheckOverlap(T.NumberClass, T.Intersect(T.Number, T.Tagged)); // !!! |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1303 | } |
| 1304 | |
| 1305 | void Union1() { |
| 1306 | // Identity: Union(T, None) = T |
| 1307 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1308 | Type* type = *it; |
| 1309 | Type* union_type = T.Union(type, T.None); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1310 | CheckEqual(union_type, type); |
| 1311 | } |
| 1312 | |
| 1313 | // Domination: Union(T, Any) = Any |
| 1314 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1315 | Type* type = *it; |
| 1316 | Type* union_type = T.Union(type, T.Any); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1317 | CheckEqual(union_type, T.Any); |
| 1318 | } |
| 1319 | |
| 1320 | // Idempotence: Union(T, T) = T |
| 1321 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1322 | Type* type = *it; |
| 1323 | Type* union_type = T.Union(type, type); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1324 | CheckEqual(union_type, type); |
| 1325 | } |
| 1326 | |
| 1327 | // Commutativity: Union(T1, T2) = Union(T2, T1) |
| 1328 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 1329 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1330 | Type* type1 = *it1; |
| 1331 | Type* type2 = *it2; |
| 1332 | Type* union12 = T.Union(type1, type2); |
| 1333 | Type* union21 = T.Union(type2, type1); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1334 | CheckEqual(union12, union21); |
| 1335 | } |
| 1336 | } |
| 1337 | |
| 1338 | // Associativity: Union(T1, Union(T2, T3)) = Union(Union(T1, T2), T3) |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 1339 | // This does NOT hold! For example: |
| 1340 | // (Unsigned32 \/ Range(0,5)) \/ Range(-5,0) = Unsigned32 \/ Range(-5,0) |
| 1341 | // Unsigned32 \/ (Range(0,5) \/ Range(-5,0)) = Unsigned32 \/ Range(-5,5) |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1342 | /* |
| 1343 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 1344 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
| 1345 | for (TypeIterator it3 = T.types.begin(); it3 != T.types.end(); ++it3) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1346 | Type* type1 = *it1; |
| 1347 | Type* type2 = *it2; |
| 1348 | Type* type3 = *it3; |
| 1349 | Type* union12 = T.Union(type1, type2); |
| 1350 | Type* union23 = T.Union(type2, type3); |
| 1351 | Type* union1_23 = T.Union(type1, union23); |
| 1352 | Type* union12_3 = T.Union(union12, type3); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1353 | CheckEqual(union1_23, union12_3); |
| 1354 | } |
| 1355 | } |
| 1356 | } |
| 1357 | */ |
| 1358 | |
| 1359 | // Meet: T1->Is(Union(T1, T2)) and T2->Is(Union(T1, T2)) |
| 1360 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 1361 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1362 | Type* type1 = *it1; |
| 1363 | Type* type2 = *it2; |
| 1364 | Type* union12 = T.Union(type1, type2); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1365 | CHECK(type1->Is(union12)); |
| 1366 | CHECK(type2->Is(union12)); |
| 1367 | } |
| 1368 | } |
| 1369 | |
| 1370 | // Upper Boundedness: T1->Is(T2) implies Union(T1, T2) = T2 |
| 1371 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 1372 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1373 | Type* type1 = *it1; |
| 1374 | Type* type2 = *it2; |
| 1375 | Type* union12 = T.Union(type1, type2); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1376 | if (type1->Is(type2)) CheckEqual(union12, type2); |
| 1377 | } |
| 1378 | } |
| 1379 | |
| 1380 | // Monotonicity: T1->Is(T2) implies Union(T1, T3)->Is(Union(T2, T3)) |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 1381 | // This does NOT hold. For example: |
| 1382 | // Range(-5,-1) <= Signed32 |
| 1383 | // Range(-5,-1) \/ Range(1,5) = Range(-5,5) </= Signed32 \/ Range(1,5) |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1384 | /* |
| 1385 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 1386 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
| 1387 | for (TypeIterator it3 = T.types.begin(); it3 != T.types.end(); ++it3) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1388 | Type* type1 = *it1; |
| 1389 | Type* type2 = *it2; |
| 1390 | Type* type3 = *it3; |
| 1391 | Type* union13 = T.Union(type1, type3); |
| 1392 | Type* union23 = T.Union(type2, type3); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1393 | CHECK(!type1->Is(type2) || union13->Is(union23)); |
| 1394 | } |
| 1395 | } |
| 1396 | } |
| 1397 | */ |
| 1398 | } |
| 1399 | |
| 1400 | void Union2() { |
| 1401 | // Monotonicity: T1->Is(T3) and T2->Is(T3) implies Union(T1, T2)->Is(T3) |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 1402 | // This does NOT hold. For example: |
| 1403 | // Range(-2^33, -2^33) <= OtherNumber |
| 1404 | // Range(2^33, 2^33) <= OtherNumber |
| 1405 | // Range(-2^33, 2^33) </= OtherNumber |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1406 | /* |
| 1407 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 1408 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
| 1409 | for (TypeIterator it3 = T.types.begin(); it3 != T.types.end(); ++it3) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1410 | Type* type1 = *it1; |
| 1411 | Type* type2 = *it2; |
| 1412 | Type* type3 = *it3; |
| 1413 | Type* union12 = T.Union(type1, type2); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1414 | CHECK(!(type1->Is(type3) && type2->Is(type3)) || union12->Is(type3)); |
| 1415 | } |
| 1416 | } |
| 1417 | } |
| 1418 | */ |
| 1419 | } |
| 1420 | |
| 1421 | void Union3() { |
| 1422 | // Monotonicity: T1->Is(T2) or T1->Is(T3) implies T1->Is(Union(T2, T3)) |
| 1423 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 1424 | HandleScope scope(isolate); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1425 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 1426 | for (TypeIterator it3 = it2; it3 != T.types.end(); ++it3) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1427 | Type* type1 = *it1; |
| 1428 | Type* type2 = *it2; |
| 1429 | Type* type3 = *it3; |
| 1430 | Type* union23 = T.Union(type2, type3); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1431 | CHECK(!(type1->Is(type2) || type1->Is(type3)) || type1->Is(union23)); |
| 1432 | } |
| 1433 | } |
| 1434 | } |
| 1435 | } |
| 1436 | |
| 1437 | void Union4() { |
| 1438 | // Class-class |
| 1439 | CheckSub(T.Union(T.ObjectClass, T.ArrayClass), T.Object); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 1440 | CheckOverlap(T.Union(T.ObjectClass, T.ArrayClass), T.OtherObject); |
| 1441 | CheckOverlap(T.Union(T.ObjectClass, T.ArrayClass), T.Receiver); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1442 | CheckDisjoint(T.Union(T.ObjectClass, T.ArrayClass), T.Number); |
| 1443 | |
| 1444 | // Constant-constant |
| 1445 | CheckSub(T.Union(T.ObjectConstant1, T.ObjectConstant2), T.Object); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 1446 | CheckOverlap(T.Union(T.ObjectConstant1, T.ArrayConstant), T.OtherObject); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1447 | CheckUnordered( |
| 1448 | T.Union(T.ObjectConstant1, T.ObjectConstant2), T.ObjectClass); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 1449 | CheckOverlap(T.Union(T.ObjectConstant1, T.ArrayConstant), T.OtherObject); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1450 | CheckDisjoint( |
| 1451 | T.Union(T.ObjectConstant1, T.ArrayConstant), T.Number); |
| 1452 | CheckOverlap( |
| 1453 | T.Union(T.ObjectConstant1, T.ArrayConstant), T.ObjectClass); // !!! |
| 1454 | |
| 1455 | // Bitset-array |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 1456 | CHECK(this->IsBitset(T.Union(T.AnyArray, T.Receiver))); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1457 | CHECK(this->IsUnion(T.Union(T.NumberArray, T.Number))); |
| 1458 | |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 1459 | CheckEqual(T.Union(T.AnyArray, T.Receiver), T.Receiver); |
| 1460 | CheckEqual(T.Union(T.AnyArray, T.OtherObject), T.OtherObject); |
| 1461 | CheckUnordered(T.Union(T.AnyArray, T.String), T.Receiver); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1462 | CheckOverlap(T.Union(T.NumberArray, T.String), T.Object); |
| 1463 | CheckDisjoint(T.Union(T.NumberArray, T.String), T.Number); |
| 1464 | |
| 1465 | // Bitset-function |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 1466 | CHECK(this->IsBitset(T.Union(T.MethodFunction, T.Object))); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1467 | CHECK(this->IsUnion(T.Union(T.NumberFunction1, T.Number))); |
| 1468 | |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 1469 | CheckEqual(T.Union(T.MethodFunction, T.Object), T.Object); |
| 1470 | CheckUnordered(T.Union(T.NumberFunction1, T.String), T.Object); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1471 | CheckOverlap(T.Union(T.NumberFunction2, T.String), T.Object); |
| 1472 | CheckDisjoint(T.Union(T.NumberFunction1, T.String), T.Number); |
| 1473 | |
| 1474 | // Bitset-class |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 1475 | CheckSub(T.Union(T.ObjectClass, T.SignedSmall), |
| 1476 | T.Union(T.Object, T.Number)); |
| 1477 | CheckSub(T.Union(T.ObjectClass, T.OtherObject), T.Object); |
| 1478 | CheckUnordered(T.Union(T.ObjectClass, T.String), T.OtherObject); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1479 | CheckOverlap(T.Union(T.ObjectClass, T.String), T.Object); |
| 1480 | CheckDisjoint(T.Union(T.ObjectClass, T.String), T.Number); |
| 1481 | |
| 1482 | // Bitset-constant |
| 1483 | CheckSub( |
| 1484 | T.Union(T.ObjectConstant1, T.Signed32), T.Union(T.Object, T.Number)); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 1485 | CheckSub(T.Union(T.ObjectConstant1, T.OtherObject), T.Object); |
| 1486 | CheckUnordered(T.Union(T.ObjectConstant1, T.String), T.OtherObject); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1487 | CheckOverlap(T.Union(T.ObjectConstant1, T.String), T.Object); |
| 1488 | CheckDisjoint(T.Union(T.ObjectConstant1, T.String), T.Number); |
| 1489 | |
| 1490 | // Class-constant |
| 1491 | CheckSub(T.Union(T.ObjectConstant1, T.ArrayClass), T.Object); |
| 1492 | CheckUnordered(T.ObjectClass, T.Union(T.ObjectConstant1, T.ArrayClass)); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 1493 | CheckSub(T.Union(T.ObjectConstant1, T.ArrayClass), |
| 1494 | T.Union(T.Receiver, T.Object)); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1495 | CheckUnordered(T.Union(T.ObjectConstant1, T.ArrayClass), T.ArrayConstant); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 1496 | CheckOverlap(T.Union(T.ObjectConstant1, T.ArrayClass), T.ObjectConstant2); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1497 | CheckOverlap( |
| 1498 | T.Union(T.ObjectConstant1, T.ArrayClass), T.ObjectClass); // !!! |
| 1499 | |
| 1500 | // Bitset-union |
| 1501 | CheckSub( |
| 1502 | T.NaN, |
| 1503 | T.Union(T.Union(T.ArrayClass, T.ObjectConstant1), T.Number)); |
| 1504 | CheckSub( |
| 1505 | T.Union(T.Union(T.ArrayClass, T.ObjectConstant1), T.Signed32), |
| 1506 | T.Union(T.ObjectConstant1, T.Union(T.Number, T.ArrayClass))); |
| 1507 | |
| 1508 | // Class-union |
| 1509 | CheckSub( |
| 1510 | T.Union(T.ObjectClass, T.Union(T.ObjectConstant1, T.ObjectClass)), |
| 1511 | T.Object); |
| 1512 | CheckEqual( |
| 1513 | T.Union(T.Union(T.ArrayClass, T.ObjectConstant2), T.ArrayClass), |
| 1514 | T.Union(T.ArrayClass, T.ObjectConstant2)); |
| 1515 | |
| 1516 | // Constant-union |
| 1517 | CheckEqual( |
| 1518 | T.Union( |
| 1519 | T.ObjectConstant1, T.Union(T.ObjectConstant1, T.ObjectConstant2)), |
| 1520 | T.Union(T.ObjectConstant2, T.ObjectConstant1)); |
| 1521 | CheckEqual( |
| 1522 | T.Union( |
| 1523 | T.Union(T.ArrayConstant, T.ObjectConstant2), T.ObjectConstant1), |
| 1524 | T.Union( |
| 1525 | T.ObjectConstant2, T.Union(T.ArrayConstant, T.ObjectConstant1))); |
| 1526 | |
| 1527 | // Array-union |
| 1528 | CheckEqual( |
| 1529 | T.Union(T.AnyArray, T.Union(T.NumberArray, T.AnyArray)), |
| 1530 | T.Union(T.AnyArray, T.NumberArray)); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 1531 | CheckSub(T.Union(T.AnyArray, T.NumberArray), T.OtherObject); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1532 | |
| 1533 | // Function-union |
| 1534 | CheckEqual( |
| 1535 | T.Union(T.NumberFunction1, T.NumberFunction2), |
| 1536 | T.Union(T.NumberFunction2, T.NumberFunction1)); |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 1537 | CheckSub(T.Union(T.SignedFunction1, T.MethodFunction), T.Object); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1538 | |
| 1539 | // Union-union |
| 1540 | CheckEqual( |
| 1541 | T.Union( |
| 1542 | T.Union(T.ObjectConstant2, T.ObjectConstant1), |
| 1543 | T.Union(T.ObjectConstant1, T.ObjectConstant2)), |
| 1544 | T.Union(T.ObjectConstant2, T.ObjectConstant1)); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 1545 | CheckEqual(T.Union(T.Union(T.Number, T.ArrayClass), |
| 1546 | T.Union(T.SignedSmall, T.Receiver)), |
| 1547 | T.Union(T.Number, T.Receiver)); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1548 | } |
| 1549 | |
| 1550 | void Intersect() { |
| 1551 | // Identity: Intersect(T, Any) = T |
| 1552 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1553 | Type* type = *it; |
| 1554 | Type* intersect_type = T.Intersect(type, T.Any); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1555 | CheckEqual(intersect_type, type); |
| 1556 | } |
| 1557 | |
| 1558 | // Domination: Intersect(T, None) = None |
| 1559 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1560 | Type* type = *it; |
| 1561 | Type* intersect_type = T.Intersect(type, T.None); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1562 | CheckEqual(intersect_type, T.None); |
| 1563 | } |
| 1564 | |
| 1565 | // Idempotence: Intersect(T, T) = T |
| 1566 | for (TypeIterator it = T.types.begin(); it != T.types.end(); ++it) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1567 | Type* type = *it; |
| 1568 | Type* intersect_type = T.Intersect(type, type); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1569 | CheckEqual(intersect_type, type); |
| 1570 | } |
| 1571 | |
| 1572 | // Commutativity: Intersect(T1, T2) = Intersect(T2, T1) |
| 1573 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 1574 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1575 | Type* type1 = *it1; |
| 1576 | Type* type2 = *it2; |
| 1577 | Type* intersect12 = T.Intersect(type1, type2); |
| 1578 | Type* intersect21 = T.Intersect(type2, type1); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1579 | CheckEqual(intersect12, intersect21); |
| 1580 | } |
| 1581 | } |
| 1582 | |
| 1583 | // Associativity: |
| 1584 | // Intersect(T1, Intersect(T2, T3)) = Intersect(Intersect(T1, T2), T3) |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 1585 | // This does NOT hold. For example: |
| 1586 | // (Class(..stringy1..) /\ Class(..stringy2..)) /\ Constant(..string..) = |
| 1587 | // None |
| 1588 | // Class(..stringy1..) /\ (Class(..stringy2..) /\ Constant(..string..)) = |
| 1589 | // Constant(..string..) |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1590 | /* |
| 1591 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 1592 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
| 1593 | for (TypeIterator it3 = T.types.begin(); it3 != T.types.end(); ++it3) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1594 | Type* type1 = *it1; |
| 1595 | Type* type2 = *it2; |
| 1596 | Type* type3 = *it3; |
| 1597 | Type* intersect12 = T.Intersect(type1, type2); |
| 1598 | Type* intersect23 = T.Intersect(type2, type3); |
| 1599 | Type* intersect1_23 = T.Intersect(type1, intersect23); |
| 1600 | Type* intersect12_3 = T.Intersect(intersect12, type3); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1601 | CheckEqual(intersect1_23, intersect12_3); |
| 1602 | } |
| 1603 | } |
| 1604 | } |
| 1605 | */ |
| 1606 | |
| 1607 | // Join: Intersect(T1, T2)->Is(T1) and Intersect(T1, T2)->Is(T2) |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 1608 | // This does NOT hold. For example: |
| 1609 | // Class(..stringy..) /\ Constant(..string..) = Constant(..string..) |
| 1610 | // Currently, not even the disjunction holds: |
| 1611 | // Class(Internal/TaggedPtr) /\ (Any/Untagged \/ Context(..)) = |
| 1612 | // Class(Internal/TaggedPtr) \/ Context(..) |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1613 | /* |
| 1614 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 1615 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1616 | Type* type1 = *it1; |
| 1617 | Type* type2 = *it2; |
| 1618 | Type* intersect12 = T.Intersect(type1, type2); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1619 | CHECK(intersect12->Is(type1)); |
| 1620 | CHECK(intersect12->Is(type2)); |
| 1621 | } |
| 1622 | } |
| 1623 | */ |
| 1624 | |
| 1625 | // Lower Boundedness: T1->Is(T2) implies Intersect(T1, T2) = T1 |
| 1626 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 1627 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1628 | Type* type1 = *it1; |
| 1629 | Type* type2 = *it2; |
| 1630 | Type* intersect12 = T.Intersect(type1, type2); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1631 | if (type1->Is(type2)) CheckEqual(intersect12, type1); |
| 1632 | } |
| 1633 | } |
| 1634 | |
| 1635 | // Monotonicity: T1->Is(T2) implies Intersect(T1, T3)->Is(Intersect(T2, T3)) |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 1636 | // This does NOT hold. For example: |
| 1637 | // Class(OtherObject/TaggedPtr) <= Any/TaggedPtr |
| 1638 | // Class(OtherObject/TaggedPtr) /\ Any/UntaggedInt1 = Class(..) |
| 1639 | // Any/TaggedPtr /\ Any/UntaggedInt1 = None |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1640 | /* |
| 1641 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 1642 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
| 1643 | for (TypeIterator it3 = T.types.begin(); it3 != T.types.end(); ++it3) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1644 | Type* type1 = *it1; |
| 1645 | Type* type2 = *it2; |
| 1646 | Type* type3 = *it3; |
| 1647 | Type* intersect13 = T.Intersect(type1, type3); |
| 1648 | Type* intersect23 = T.Intersect(type2, type3); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1649 | CHECK(!type1->Is(type2) || intersect13->Is(intersect23)); |
| 1650 | } |
| 1651 | } |
| 1652 | } |
| 1653 | */ |
| 1654 | |
| 1655 | // Monotonicity: T1->Is(T3) or T2->Is(T3) implies Intersect(T1, T2)->Is(T3) |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 1656 | // This does NOT hold. For example: |
| 1657 | // Class(..stringy..) <= Class(..stringy..) |
| 1658 | // Class(..stringy..) /\ Constant(..string..) = Constant(..string..) |
| 1659 | // Constant(..string..) </= Class(..stringy..) |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1660 | /* |
| 1661 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 1662 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
| 1663 | for (TypeIterator it3 = T.types.begin(); it3 != T.types.end(); ++it3) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1664 | Type* type1 = *it1; |
| 1665 | Type* type2 = *it2; |
| 1666 | Type* type3 = *it3; |
| 1667 | Type* intersect12 = T.Intersect(type1, type2); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1668 | CHECK(!(type1->Is(type3) || type2->Is(type3)) || |
| 1669 | intersect12->Is(type3)); |
| 1670 | } |
| 1671 | } |
| 1672 | } |
| 1673 | */ |
| 1674 | |
| 1675 | // Monotonicity: T1->Is(T2) and T1->Is(T3) implies T1->Is(Intersect(T2, T3)) |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1676 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 1677 | HandleScope scope(isolate); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1678 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
| 1679 | for (TypeIterator it3 = T.types.begin(); it3 != T.types.end(); ++it3) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1680 | Type* type1 = *it1; |
| 1681 | Type* type2 = *it2; |
| 1682 | Type* type3 = *it3; |
| 1683 | Type* intersect23 = T.Intersect(type2, type3); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1684 | CHECK(!(type1->Is(type2) && type1->Is(type3)) || |
| 1685 | type1->Is(intersect23)); |
| 1686 | } |
| 1687 | } |
| 1688 | } |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1689 | |
| 1690 | // Bitset-class |
| 1691 | CheckEqual(T.Intersect(T.ObjectClass, T.Object), T.ObjectClass); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 1692 | CheckEqual(T.Semantic(T.Intersect(T.ObjectClass, T.Number)), T.None); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1693 | |
| 1694 | // Bitset-array |
| 1695 | CheckEqual(T.Intersect(T.NumberArray, T.Object), T.NumberArray); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 1696 | CheckEqual(T.Semantic(T.Intersect(T.AnyArray, T.Proxy)), T.None); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1697 | |
| 1698 | // Bitset-function |
| 1699 | CheckEqual(T.Intersect(T.MethodFunction, T.Object), T.MethodFunction); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 1700 | CheckEqual(T.Semantic(T.Intersect(T.NumberFunction1, T.Proxy)), T.None); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1701 | |
| 1702 | // Bitset-union |
| 1703 | CheckEqual( |
| 1704 | T.Intersect(T.Object, T.Union(T.ObjectConstant1, T.ObjectClass)), |
| 1705 | T.Union(T.ObjectConstant1, T.ObjectClass)); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 1706 | CheckEqual(T.Semantic(T.Intersect(T.Union(T.ArrayClass, T.ObjectConstant1), |
| 1707 | T.Number)), |
| 1708 | T.None); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1709 | |
| 1710 | // Class-constant |
| 1711 | CHECK(T.Intersect(T.ObjectConstant1, T.ObjectClass)->IsInhabited()); // !!! |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 1712 | CHECK(T.Intersect(T.ArrayClass, T.ObjectConstant2)->IsInhabited()); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1713 | |
| 1714 | // Array-union |
| 1715 | CheckEqual( |
| 1716 | T.Intersect(T.NumberArray, T.Union(T.NumberArray, T.ArrayClass)), |
| 1717 | T.NumberArray); |
| 1718 | CheckEqual( |
| 1719 | T.Intersect(T.AnyArray, T.Union(T.Object, T.SmiConstant)), |
| 1720 | T.AnyArray); |
| 1721 | CHECK( |
| 1722 | !T.Intersect(T.Union(T.AnyArray, T.ArrayConstant), T.NumberArray) |
| 1723 | ->IsInhabited()); |
| 1724 | |
| 1725 | // Function-union |
| 1726 | CheckEqual( |
| 1727 | T.Intersect(T.MethodFunction, T.Union(T.String, T.MethodFunction)), |
| 1728 | T.MethodFunction); |
| 1729 | CheckEqual( |
| 1730 | T.Intersect(T.NumberFunction1, T.Union(T.Object, T.SmiConstant)), |
| 1731 | T.NumberFunction1); |
| 1732 | CHECK( |
| 1733 | !T.Intersect(T.Union(T.MethodFunction, T.Name), T.NumberFunction2) |
| 1734 | ->IsInhabited()); |
| 1735 | |
| 1736 | // Class-union |
| 1737 | CheckEqual( |
| 1738 | T.Intersect(T.ArrayClass, T.Union(T.ObjectConstant2, T.ArrayClass)), |
| 1739 | T.ArrayClass); |
| 1740 | CheckEqual( |
| 1741 | T.Intersect(T.ArrayClass, T.Union(T.Object, T.SmiConstant)), |
| 1742 | T.ArrayClass); |
| 1743 | CHECK( |
| 1744 | T.Intersect(T.Union(T.ObjectClass, T.ArrayConstant), T.ArrayClass) |
| 1745 | ->IsInhabited()); // !!! |
| 1746 | |
| 1747 | // Constant-union |
| 1748 | CheckEqual( |
| 1749 | T.Intersect( |
| 1750 | T.ObjectConstant1, T.Union(T.ObjectConstant1, T.ObjectConstant2)), |
| 1751 | T.ObjectConstant1); |
| 1752 | CheckEqual( |
| 1753 | T.Intersect(T.SmiConstant, T.Union(T.Number, T.ObjectConstant2)), |
| 1754 | T.SmiConstant); |
| 1755 | CHECK( |
| 1756 | T.Intersect( |
| 1757 | T.Union(T.ArrayConstant, T.ObjectClass), T.ObjectConstant1) |
| 1758 | ->IsInhabited()); // !!! |
| 1759 | |
| 1760 | // Union-union |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 1761 | CheckEqual(T.Intersect(T.Union(T.Number, T.ArrayClass), |
| 1762 | T.Union(T.SignedSmall, T.Receiver)), |
| 1763 | T.Union(T.SignedSmall, T.ArrayClass)); |
| 1764 | CheckEqual(T.Intersect(T.Union(T.Number, T.ObjectClass), |
| 1765 | T.Union(T.Signed32, T.OtherObject)), |
| 1766 | T.Union(T.Signed32, T.ObjectClass)); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1767 | CheckEqual( |
| 1768 | T.Intersect( |
| 1769 | T.Union(T.ObjectConstant2, T.ObjectConstant1), |
| 1770 | T.Union(T.ObjectConstant1, T.ObjectConstant2)), |
| 1771 | T.Union(T.ObjectConstant2, T.ObjectConstant1)); |
| 1772 | CheckEqual( |
| 1773 | T.Intersect( |
| 1774 | T.Union( |
| 1775 | T.ArrayClass, |
| 1776 | T.Union(T.ObjectConstant2, T.ObjectConstant1)), |
| 1777 | T.Union( |
| 1778 | T.ObjectConstant1, |
| 1779 | T.Union(T.ArrayConstant, T.ObjectConstant2))), |
| 1780 | T.Union( |
| 1781 | T.ArrayConstant, |
| 1782 | T.Union(T.ObjectConstant2, T.ObjectConstant1))); // !!! |
| 1783 | } |
| 1784 | |
| 1785 | void Distributivity() { |
| 1786 | // Union(T1, Intersect(T2, T3)) = Intersect(Union(T1, T2), Union(T1, T3)) |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 1787 | // This does NOT hold. For example: |
| 1788 | // Untagged \/ (Untagged /\ Class(../Tagged)) = Untagged \/ Class(../Tagged) |
| 1789 | // (Untagged \/ Untagged) /\ (Untagged \/ Class(../Tagged)) = |
| 1790 | // Untagged /\ (Untagged \/ Class(../Tagged)) = Untagged |
| 1791 | // because Untagged <= Untagged \/ Class(../Tagged) |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1792 | /* |
| 1793 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 1794 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
| 1795 | for (TypeIterator it3 = T.types.begin(); it3 != T.types.end(); ++it3) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1796 | Type* type1 = *it1; |
| 1797 | Type* type2 = *it2; |
| 1798 | Type* type3 = *it3; |
| 1799 | Type* union12 = T.Union(type1, type2); |
| 1800 | Type* union13 = T.Union(type1, type3); |
| 1801 | Type* intersect23 = T.Intersect(type2, type3); |
| 1802 | Type* union1_23 = T.Union(type1, intersect23); |
| 1803 | Type* intersect12_13 = T.Intersect(union12, union13); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1804 | CHECK(Equal(union1_23, intersect12_13)); |
| 1805 | } |
| 1806 | } |
| 1807 | } |
| 1808 | */ |
| 1809 | |
| 1810 | // Intersect(T1, Union(T2, T3)) = Union(Intersect(T1, T2), Intersect(T1,T3)) |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 1811 | // This does NOT hold. For example: |
| 1812 | // Untagged /\ (Untagged \/ Class(../Tagged)) = Untagged |
| 1813 | // (Untagged /\ Untagged) \/ (Untagged /\ Class(../Tagged)) = |
| 1814 | // Untagged \/ Class(../Tagged) |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1815 | /* |
| 1816 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 1817 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
| 1818 | for (TypeIterator it3 = T.types.begin(); it3 != T.types.end(); ++it3) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1819 | Type* type1 = *it1; |
| 1820 | Type* type2 = *it2; |
| 1821 | Type* type3 = *it3; |
| 1822 | Type* intersect12 = T.Intersect(type1, type2); |
| 1823 | Type* intersect13 = T.Intersect(type1, type3); |
| 1824 | Type* union23 = T.Union(type2, type3); |
| 1825 | Type* intersect1_23 = T.Intersect(type1, union23); |
| 1826 | Type* union12_13 = T.Union(intersect12, intersect13); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1827 | CHECK(Equal(intersect1_23, union12_13)); |
| 1828 | } |
| 1829 | } |
| 1830 | } |
| 1831 | */ |
| 1832 | } |
| 1833 | |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 1834 | void GetRange() { |
| 1835 | // GetRange(Range(a, b)) = Range(a, b). |
| 1836 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1837 | Type* type1 = *it1; |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 1838 | if (type1->IsRange()) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1839 | RangeType* range = type1->GetRange()->AsRange(); |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 1840 | CHECK(type1->Min() == range->Min()); |
| 1841 | CHECK(type1->Max() == range->Max()); |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 1842 | } |
| 1843 | } |
| 1844 | |
| 1845 | // GetRange(Union(Constant(x), Range(min,max))) == Range(min, max). |
| 1846 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 1847 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1848 | Type* type1 = *it1; |
| 1849 | Type* type2 = *it2; |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 1850 | if (type1->IsConstant() && type2->IsRange()) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1851 | Type* u = T.Union(type1, type2); |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 1852 | |
Ben Murdoch | 4a90d5f | 2016-03-22 12:00:34 +0000 | [diff] [blame] | 1853 | CHECK(type2->Min() == u->GetRange()->Min()); |
| 1854 | CHECK(type2->Max() == u->GetRange()->Max()); |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 1855 | } |
| 1856 | } |
| 1857 | } |
| 1858 | } |
| 1859 | |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1860 | void HTypeFromType() { |
| 1861 | for (TypeIterator it1 = T.types.begin(); it1 != T.types.end(); ++it1) { |
| 1862 | for (TypeIterator it2 = T.types.begin(); it2 != T.types.end(); ++it2) { |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1863 | Type* type1 = *it1; |
| 1864 | Type* type2 = *it2; |
| 1865 | HType htype1 = HType::FromType(type1); |
| 1866 | HType htype2 = HType::FromType(type2); |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1867 | CHECK(!type1->Is(type2) || htype1.IsSubtypeOf(htype2)); |
| 1868 | } |
| 1869 | } |
| 1870 | } |
| 1871 | }; |
| 1872 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1873 | TEST(IsSomeType_zone) { Tests().IsSomeType(); } |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1874 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1875 | TEST(PointwiseRepresentation_zone) { Tests().PointwiseRepresentation(); } |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1876 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1877 | TEST(BitsetType_zone) { Tests().Bitset(); } |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1878 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1879 | TEST(ClassType_zone) { Tests().Class(); } |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1880 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1881 | TEST(ConstantType_zone) { Tests().Constant(); } |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1882 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1883 | TEST(RangeType_zone) { Tests().Range(); } |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1884 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1885 | TEST(ArrayType_zone) { Tests().Array(); } |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1886 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1887 | TEST(FunctionType_zone) { Tests().Function(); } |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1888 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1889 | TEST(Of_zone) { Tests().Of(); } |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1890 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1891 | TEST(NowOf_zone) { Tests().NowOf(); } |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1892 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1893 | TEST(MinMax_zone) { Tests().MinMax(); } |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1894 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1895 | TEST(BitsetGlb_zone) { Tests().BitsetGlb(); } |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1896 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1897 | TEST(BitsetLub_zone) { Tests().BitsetLub(); } |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1898 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1899 | TEST(Is1_zone) { Tests().Is1(); } |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1900 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1901 | TEST(Is2_zone) { Tests().Is2(); } |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1902 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1903 | TEST(NowIs_zone) { Tests().NowIs(); } |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1904 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1905 | TEST(Contains_zone) { Tests().Contains(); } |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1906 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1907 | TEST(NowContains_zone) { Tests().NowContains(); } |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1908 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1909 | TEST(Maybe_zone) { Tests().Maybe(); } |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1910 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1911 | TEST(Union1_zone) { Tests().Union1(); } |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1912 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1913 | TEST(Union2_zone) { Tests().Union2(); } |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 1914 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1915 | TEST(Union3_zone) { Tests().Union3(); } |
Emily Bernier | d0a1eb7 | 2015-03-24 16:35:39 -0400 | [diff] [blame] | 1916 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1917 | TEST(Union4_zone) { Tests().Union4(); } |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1918 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1919 | TEST(Intersect_zone) { Tests().Intersect(); } |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1920 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1921 | TEST(Distributivity_zone) { Tests().Distributivity(); } |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1922 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1923 | TEST(GetRange_zone) { Tests().GetRange(); } |
Ben Murdoch | b8a8cc1 | 2014-11-26 15:28:44 +0000 | [diff] [blame] | 1924 | |
Ben Murdoch | 097c5b2 | 2016-05-18 11:27:45 +0100 | [diff] [blame] | 1925 | TEST(HTypeFromType_zone) { Tests().HTypeFromType(); } |