1/* 2 * Copyright (c) 2021-2024 Huawei Device Co., Ltd. 3 * Licensed under the Apache License, Version 2.0 (the "License"); 4 * you may not use this file except in compliance with the License. 5 * You may obtain a copy of the License at 6 * 7 * http://www.apache.org/licenses/LICENSE-2.0 8 * 9 * Unless required by applicable law or agreed to in writing, software 10 * distributed under the License is distributed on an "AS IS" BASIS, 11 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. 12 * See the License for the specific language governing permissions and 13 * limitations under the License. 14 */ 15 16module check_set_intersection_as_lub 17open java_typing 18 19fact Validity {all r: Register | r.Valid } 20let supertypes[t] = { t.^~subtypes } 21 22fun SuperTypesIntersection[regs: set Register] : set Type 23{{t : Type | all r : regs | t in r.type + r.type.supertypes}} 24 25-- Correct subtyping definition: 26-- exists some type in set of types, 27-- which is a subtype of register type 28pred CorrectSubtyping[r: Register, types: set Type] 29{ some t : types | t in (r.type + r.type.^subtypes) & ProperType } 30 31-- check that one reg type may be used as substitutuion for the other 32pred MayBeSubstitutedFor[subst, r:Register] 33{ subst.type in (r.type + r.type.subtypes) } 34 35-- r1,r2,r3 - reg values accured during context calculation 36-- arg - is some type to be checked for compatibility with context 37-- like some argument type in call instruction, etc 38-- compatibility means that either of r1,r2,r3 may be used for arg 39pred Show { 40 Register.holds in Instance 41 some Class 42 some Interface 43 some Register.type & Interface 44 some disj r1, r2, r3, arg : Register { 45 let comp_types = SuperTypesIntersection[r1+r2+r3] { 46 some comp_types - Top and arg.CorrectSubtyping[comp_types] and { 47 r1.MayBeSubstitutedFor[arg] 48 r2.MayBeSubstitutedFor[arg] 49 r3.MayBeSubstitutedFor[arg] 50 } 51 } 52 } 53} 54 55example: run Show for 7 but exactly 4 Register, exactly 5 Class, exactly 5 Interface, exactly 3 Instance 56 57assert SupertypesIntersectionAsLUB { 58 { 59 #Register >=4 60 #Class >= 1 61 #Instance >= 1 62 } implies 63 some r1, r2, r3, arg : Register { 64 -- select some regs (suppose it is the same reg from different contexts) 65 -- select target arg, that will be checked against merged context 66 let comp_types = SuperTypesIntersection[r1+r2+r3] { 67 -- calculate supertypes intersection on contexts merge 68 { 69 some comp_types - Top -- we have some proper types after contexts merge 70 arg.CorrectSubtyping[comp_types] -- and arg is checked against this new context 71 } implies { 72 -- so verify, that all reg instances from all contexts can be used for arg 73 r1.MayBeSubstitutedFor[arg] 74 r2.MayBeSubstitutedFor[arg] 75 r3.MayBeSubstitutedFor[arg] 76 } 77 } 78 } 79} 80 81verify: check SupertypesIntersectionAsLUB for 8 82 83-- results: 84-- 85-- Executing "Check verify for 8" 86-- Sig java_typing/Top scope <= 1 87-- Sig java_typing/Bot scope <= 1 88-- Sig java_typing/Object scope <= 1 89-- Sig java_typing/NullType scope <= 1 90-- Sig java_typing/Null scope <= 1 91-- Sig java_typing/Type scope <= 8 92-- Sig java_typing/Value scope <= 8 93-- Sig java_typing/Register scope <= 8 94-- Sig java_typing/Instance scope <= 7 95-- Sig java_typing/Class scope <= 8 96-- Sig java_typing/Interface scope <= 8 97-- Sig java_typing/Type in [[java_typing/Top$0], [java_typing/Bot$0], [java_typing/Object$0], [java_typing/NullType$0], [java_typing/Type$0], [java_typing/Type$1], [java_typing/Type$2], [java_typing/Type$3]] 98-- Sig java_typing/Top == [[java_typing/Top$0]] 99-- Sig java_typing/Bot == [[java_typing/Bot$0]] 100-- Sig java_typing/Class in [[java_typing/Type$0], [java_typing/Type$1], [java_typing/Type$2], [java_typing/Type$3]] 101-- Sig java_typing/Interface in [[java_typing/Type$0], [java_typing/Type$1], [java_typing/Type$2], [java_typing/Type$3]] 102-- Sig java_typing/Object == [[java_typing/Object$0]] 103-- Sig java_typing/NullType == [[java_typing/NullType$0]] 104-- Sig java_typing/Value in [[java_typing/Null$0], [java_typing/Value$0], [java_typing/Value$1], [java_typing/Value$2], [java_typing/Value$3], [java_typing/Value$4], [java_typing/Value$5], [java_typing/Value$6]] 105-- Sig java_typing/Instance in [[java_typing/Value$0], [java_typing/Value$1], [java_typing/Value$2], [java_typing/Value$3], [java_typing/Value$4], [java_typing/Value$5], [java_typing/Value$6]] 106-- Sig java_typing/Null == [[java_typing/Null$0]] 107-- Sig java_typing/Register in [[java_typing/Register$0], [java_typing/Register$1], [java_typing/Register$2], [java_typing/Register$3], [java_typing/Register$4], [java_typing/Register$5], [java_typing/Register$6], [java_typing/Register$7]] 108-- Generating facts... 109-- Simplifying the bounds... 110-- Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=4 Symmetry=20 111-- Generating CNF... 112-- Generating the solution... 113-- 502376 vars. 33023 primary vars. 881131 clauses. 3609ms. 114-- No counterexample found. Assertion may be valid. 127ms. 115