Appearance
| 1 | namespace Syntax.Process is | |
| 2 | use Function = Semantic.Symbols.Function | |
| 3 | use Semantic.Symbols.STORE_FREE_IMPORTS | |
| 4 | ||
| 5 | // Solves the per-function facts gathered by INFER_STORE_FREE's | |
| 6 | // body walk into the set of functions that cannot be shown | |
| 7 | // store-free. | |
| 8 | // | |
| 9 | // A function is unsafe if its body disqualified it, if a call | |
| 10 | // bound to it could dispatch to an override outside the | |
| 11 | // compilation, or if any bounded callee or any override of it is | |
| 12 | // unsafe; unsafety propagates to a fixpoint and everything never | |
| 13 | // reached is store-free. Mutual recursion between clean bodies is | |
| 14 | // never seeded, so it correctly ends up store-free. | |
| 15 | class STORE_FREE_FIXPOINT is | |
| 16 | init() is si | |
| 17 | ||
| 18 | solve( | |
| 19 | facts: Collections.MutableMap[Function, STORE_FREE_FACTS] | |
| 20 | ) -> (unsafe: Collections.SET[Function], construction_unsafe: Collections.SET[Function]) => | |
| 21 | solve(facts, EFFECT_DEPENDANTS(facts, EFFECT_SOLVERS(facts).param_invokers)) | |
| 22 | ||
| 23 | solve( | |
| 24 | facts: Collections.MutableMap[Function, STORE_FREE_FACTS], | |
| 25 | dependants: EFFECT_DEPENDANTS | |
| 26 | ) -> (unsafe: Collections.SET[Function], construction_unsafe: Collections.SET[Function]) => | |
| 27 | solve(facts, dependants, null, null) | |
| 28 | ||
| 29 | // With `previous` and `affected`, only the affected functions | |
| 30 | // are judged; every other function keeps the bits `previous` | |
| 31 | // gave it, its inputs being unchanged. | |
| 32 | solve( | |
| 33 | facts: Collections.MutableMap[Function, STORE_FREE_FACTS], | |
| 34 | dependants: EFFECT_DEPENDANTS, | |
| 35 | previous: EFFECT_SOLUTION?, | |
| 36 | affected: Collections.SET[Function]? | |
| 37 | ) -> (unsafe: Collections.SET[Function], construction_unsafe: Collections.SET[Function]) is | |
| 38 | let unsafe = Collections.SET[Function]() | |
| 39 | ||
| 40 | // The same relation over the construction bit: a function | |
| 41 | // is construction-unsafe when it writes something other | |
| 42 | // than the state of the object it is called on. The two | |
| 43 | // are solved together because they are mutually recursive | |
| 44 | // - a construction edge makes a strictly store-free caller | |
| 45 | // depend on its callee's construction bit. | |
| 46 | let construction_unsafe = Collections.SET[Function]() | |
| 47 | ||
| 48 | let judged = Collections.LIST[Function]() | |
| 49 | ||
| 50 | for function in facts.keys do | |
| 51 | if previous? /\ affected? /\ !affected.contains(function) then | |
| 52 | if !previous.store_free.contains(function) then | |
| 53 | unsafe.add(function) | |
| 54 | fi | |
| 55 | ||
| 56 | if !previous.constructs_store_free.contains(function) then | |
| 57 | construction_unsafe.add(function) | |
| 58 | fi | |
| 59 | ||
| 60 | continue | |
| 61 | fi | |
| 62 | ||
| 63 | judged.add(function) | |
| 64 | ||
| 65 | let shadowed = is_openly_dispatchable(function) | |
| 66 | ||
| 67 | if facts[function].is_disqualified \/ shadowed then | |
| 68 | unsafe.add(function) | |
| 69 | fi | |
| 70 | ||
| 71 | if facts[function].is_construction_disqualified \/ shadowed then | |
| 72 | construction_unsafe.add(function) | |
| 73 | fi | |
| 74 | od | |
| 75 | ||
| 76 | // Every function is judged once; a function is judged | |
| 77 | // again only when something it depends on became unsafe. | |
| 78 | let dirty mut = Collections.SET[Function]() | |
| 79 | ||
| 80 | for function in judged do | |
| 81 | if _demote(function, facts, unsafe, construction_unsafe) then | |
| 82 | dirty.add(function) | |
| 83 | fi | |
| 84 | od | |
| 85 | ||
| 86 | while dirty.count > 0 do | |
| 87 | let next = Collections.SET[Function]() | |
| 88 | ||
| 89 | for target in dirty do | |
| 90 | for functions in [dependants.dependants_of(target), dependants.dependants_through_unwalked(target)] do | |
| 91 | if !functions? then | |
| 92 | continue | |
| 93 | fi | |
| 94 | ||
| 95 | for function in functions do | |
| 96 | if _demote(function, facts, unsafe, construction_unsafe) then | |
| 97 | next.add(function) | |
| 98 | fi | |
| 99 | od | |
| 100 | od | |
| 101 | od | |
| 102 | ||
| 103 | dirty = next | |
| 104 | od | |
| 105 | ||
| 106 | return (unsafe = unsafe, construction_unsafe = construction_unsafe) | |
| 107 | si | |
| 108 | ||
| 109 | // Judge both bits of one function against the current sets; | |
| 110 | // returns whether either was newly set. | |
| 111 | _demote( | |
| 112 | function: Function, | |
| 113 | facts: Collections.MutableMap[Function, STORE_FREE_FACTS], | |
| 114 | unsafe: Collections.SET[Function], | |
| 115 | construction_unsafe: Collections.SET[Function] | |
| 116 | ) -> bool is | |
| 117 | let demoted mut = false | |
| 118 | ||
| 119 | if | |
| 120 | !unsafe.contains(function) /\ | |
| 121 | !_all_dependencies_safe(function, facts, unsafe, construction_unsafe, false) | |
| 122 | then | |
| 123 | unsafe.add(function) | |
| 124 | demoted = true | |
| 125 | fi | |
| 126 | ||
| 127 | if | |
| 128 | !construction_unsafe.contains(function) /\ | |
| 129 | !_all_dependencies_safe(function, facts, unsafe, construction_unsafe, true) | |
| 130 | then | |
| 131 | construction_unsafe.add(function) | |
| 132 | demoted = true | |
| 133 | fi | |
| 134 | ||
| 135 | return demoted | |
| 136 | si | |
| 137 | ||
| 138 | // Whether every dependency of `function` is safe under the bit | |
| 139 | // being solved. Both bits share the dependency set and differ | |
| 140 | // only in which one each dependency is read against: the | |
| 141 | // dispatch shadow is checked against the bit under solution, | |
| 142 | // because an override reached in place of this function has to | |
| 143 | // meet the same promise this function is making. | |
| 144 | _all_dependencies_safe( | |
| 145 | function: Function, | |
| 146 | facts: Collections.MutableMap[Function, STORE_FREE_FACTS], | |
| 147 | unsafe: Collections.SET[Function], | |
| 148 | construction_unsafe: Collections.SET[Function], | |
| 149 | for_construction: bool | |
| 150 | ) -> bool is | |
| 151 | for callee in facts[function].callees do | |
| 152 | if !_target_is_safe(callee, facts, unsafe) then | |
| 153 | return false | |
| 154 | fi | |
| 155 | od | |
| 156 | ||
| 157 | for callee in facts[function].construction_callees do | |
| 158 | if !_construction_target_is_safe(callee, facts, unsafe, construction_unsafe) then | |
| 159 | return false | |
| 160 | fi | |
| 161 | od | |
| 162 | ||
| 163 | // Effect-polymorphic over invoked function-typed | |
| 164 | // parameters, exactly as the write-set solver's absorption | |
| 165 | // is: a body that invokes one is bounded by the values | |
| 166 | // recorded flowing in at its call sites, and a value | |
| 167 | // nothing could name makes the invocation unboundable. | |
| 168 | // Without this, a wrapper that only invokes its parameter | |
| 169 | // solves store-free however much the value it was handed | |
| 170 | // stores. | |
| 171 | let record = EFFECT_FACTS.record_for(function) | |
| 172 | ||
| 173 | if record? /\ record.invokes_function_param then | |
| 174 | if EFFECT_FACTS.passed_opaque.contains(function) then | |
| 175 | return false | |
| 176 | fi | |
| 177 | ||
| 178 | let passed = EFFECT_FACTS.passed_functions_for(function) | |
| 179 | ||
| 180 | if passed? then | |
| 181 | for value in passed do | |
| 182 | if !_target_is_safe(value, facts, unsafe) then | |
| 183 | return false | |
| 184 | fi | |
| 185 | od | |
| 186 | fi | |
| 187 | fi | |
| 188 | ||
| 189 | // a call bound to this function may dispatch to any | |
| 190 | // override of it | |
| 191 | let overriders = function.overriders | |
| 192 | ||
| 193 | if overriders? then | |
| 194 | for overrider in overriders do | |
| 195 | if !isa Function(overrider) then | |
| 196 | return false | |
| 197 | fi | |
| 198 | ||
| 199 | let overrider_function = cast Function(overrider) | |
| 200 | ||
| 201 | if !facts.contains_key(overrider_function) then | |
| 202 | return false | |
| 203 | fi | |
| 204 | ||
| 205 | if for_construction then | |
| 206 | if construction_unsafe.contains(overrider_function) then | |
| 207 | return false | |
| 208 | fi | |
| 209 | elif unsafe.contains(overrider_function) then | |
| 210 | return false | |
| 211 | fi | |
| 212 | od | |
| 213 | fi | |
| 214 | ||
| 215 | return true | |
| 216 | si | |
| 217 | ||
| 218 | // A target reached on a fresh receiver is safe when it writes | |
| 219 | // nothing beyond that receiver's own state. Only functions this | |
| 220 | // compilation walked carry that classification; anything else | |
| 221 | // has to clear the strict bar instead. | |
| 222 | _construction_target_is_safe( | |
| 223 | target: Function, | |
| 224 | facts: Collections.MutableMap[Function, STORE_FREE_FACTS], | |
| 225 | unsafe: Collections.SET[Function], | |
| 226 | construction_unsafe: Collections.SET[Function] | |
| 227 | ) -> bool is | |
| 228 | if target.is_declared_pure then | |
| 229 | return true | |
| 230 | fi | |
| 231 | ||
| 232 | if facts.contains_key(target) then | |
| 233 | return !construction_unsafe.contains(target) | |
| 234 | fi | |
| 235 | ||
| 236 | return _target_is_safe(target, facts, unsafe) | |
| 237 | si | |
| 238 | ||
| 239 | // A call target is safe when it was walked and has not been | |
| 240 | // demoted, or when it is a trusted store-free import. A | |
| 241 | // trusted import can still be virtual (object.to_string), so | |
| 242 | // its in-assembly overriders — which have facts entries and | |
| 243 | // their own fixpoint rows — are part of the dispatch shadow | |
| 244 | // and must be safe too. | |
| 245 | _target_is_safe( | |
| 246 | target: Function, | |
| 247 | facts: Collections.MutableMap[Function, STORE_FREE_FACTS], | |
| 248 | unsafe: Collections.SET[Function] | |
| 249 | ) -> bool is | |
| 250 | // Declared `pure` is a trust declaration — it holds even | |
| 251 | // when the body is unprovable, and the pure-override | |
| 252 | // contract separately diagnoses any overrider that | |
| 253 | // breaks it, so the dispatch shadow needs no re-check | |
| 254 | // here. | |
| 255 | if target.is_declared_pure then | |
| 256 | return true | |
| 257 | fi | |
| 258 | ||
| 259 | // The other structural tiers — a whitelisted import, a | |
| 260 | // synthesized backing read — carry their own dispatch | |
| 261 | // guard, so a true answer needs no overrider re-check. | |
| 262 | if target.is_store_free then | |
| 263 | return true | |
| 264 | fi | |
| 265 | ||
| 266 | if facts.contains_key(target) then | |
| 267 | return !unsafe.contains(target) | |
| 268 | fi | |
| 269 | ||
| 270 | if !STORE_FREE_IMPORTS.is_store_free(target) then | |
| 271 | return false | |
| 272 | fi | |
| 273 | ||
| 274 | let target_overriders = target.overriders | |
| 275 | ||
| 276 | if target_overriders? then | |
| 277 | for overrider in target_overriders do | |
| 278 | if !isa Function(overrider) then | |
| 279 | return false | |
| 280 | fi | |
| 281 | ||
| 282 | let overrider_function = cast Function(overrider) | |
| 283 | ||
| 284 | if !facts.contains_key(overrider_function) \/ unsafe.contains(overrider_function) then | |
| 285 | return false | |
| 286 | fi | |
| 287 | od | |
| 288 | fi | |
| 289 | ||
| 290 | return true | |
| 291 | si | |
| 292 | ||
| 293 | // A call bound to this function may dispatch to an override | |
| 294 | // this compilation cannot see when the owner hierarchy is | |
| 295 | // open to other assemblies. Struct methods are final, and | |
| 296 | // constructors and static/global functions do not dispatch. | |
| 297 | is_openly_dispatchable(function: Function) -> bool is | |
| 298 | if isa Semantic.Symbols.STRUCT_METHOD(function) then | |
| 299 | return false | |
| 300 | fi | |
| 301 | ||
| 302 | if !isa Semantic.Symbols.INSTANCE_METHOD(function) then | |
| 303 | return false | |
| 304 | fi | |
| 305 | ||
| 306 | if function.name =~ "init" then | |
| 307 | return false | |
| 308 | fi | |
| 309 | ||
| 310 | let owner = function.owner | |
| 311 | ||
| 312 | if !owner? \/ !isa Semantic.Symbols.Classy(owner) then | |
| 313 | return true | |
| 314 | fi | |
| 315 | ||
| 316 | let owner_classy = cast Semantic.Symbols.Classy(owner) | |
| 317 | ||
| 318 | // A closed owner's dispatch is bounded by the recorded | |
| 319 | // override and implementation edges, for traits and | |
| 320 | // unions as much as classes: closed-to-assembly means | |
| 321 | // nothing outside the compilation can add an overrider, | |
| 322 | // and resolve-overrides links every in-assembly one. | |
| 323 | return owner_classy.is_open | |
| 324 | si | |
| 325 | si | |
| 326 | si |