Appearance
| 1 | namespace Syntax.Process is | |
| 2 | use Logging.Logger | |
| 3 | use LOCATION = Source.LOCATION | |
| 4 | use Symbol = Semantic.Symbols.Symbol | |
| 5 | use Function = Semantic.Symbols.Function | |
| 6 | ||
| 7 | // The discharge rules the effect solve asks of every call a | |
| 8 | // narrowing fact was kept across - the write sets, getter read | |
| 9 | // closures and self-stability tiers behind crossing_discharged | |
| 10 | // and first_unproven_getter. Stateful only for the crossing | |
| 11 | // trace. | |
| 12 | class RELIANCES is | |
| 13 | ||
| 14 | // The getter's own call over a presence fact it backs: a | |
| 15 | // monotone memoiser's answer can only move from absent to | |
| 16 | // present, so the presence fact survives the re-read its own | |
| 17 | // getter performs. Type facts stay on the ordinary route - a | |
| 18 | // rewrite while absent can change the runtime type a wider | |
| 19 | // member holds. | |
| 20 | _is_presence_monotone_self_call( | |
| 21 | callee: Function, | |
| 22 | target: Symbol?, | |
| 23 | path: ACCESS_PATH? | |
| 24 | ) -> bool static is | |
| 25 | let property: Semantic.Symbols.Property? mut = null | |
| 26 | ||
| 27 | if target? /\ isa Semantic.Symbols.Property(target) then | |
| 28 | property = cast Semantic.Symbols.Property?(target) | |
| 29 | elif path? /\ path.members.count > 0 then | |
| 30 | let last = path.members[path.members.count - 1] | |
| 31 | ||
| 32 | if isa Semantic.Symbols.Property(last) then | |
| 33 | property = cast Semantic.Symbols.Property?(last) | |
| 34 | fi | |
| 35 | fi | |
| 36 | ||
| 37 | if !property? then | |
| 38 | return false | |
| 39 | fi | |
| 40 | ||
| 41 | let getter = property.read_function | |
| 42 | ||
| 43 | if !getter? then | |
| 44 | return false | |
| 45 | fi | |
| 46 | ||
| 47 | return | |
| 48 | getter.root_specialized_from == callee.root_specialized_from /\ | |
| 49 | MONOTONE_MEMOISER.is_presence_monotone(property) | |
| 50 | si | |
| 51 | ||
| 52 | // The getter's own call over a fact about the property it | |
| 53 | // reads: adjacent reads of a declared-stable property agree | |
| 54 | // on presence and runtime type alike, so the re-read is | |
| 55 | // harmless to both fact kinds. For a path, only the last hop | |
| 56 | // counts — the hop the fact is about. A stable prefix merely | |
| 57 | // returns the same object; its getter may still write through | |
| 58 | // that object on the way, so its call is no guarantee for a | |
| 59 | // fact about a deeper member. | |
| 60 | _is_stable_self_call( | |
| 61 | callee: Function, | |
| 62 | target: Symbol?, | |
| 63 | path: ACCESS_PATH? | |
| 64 | ) -> bool static is | |
| 65 | let property: Semantic.Symbols.Property? mut = null | |
| 66 | ||
| 67 | if target? /\ isa Semantic.Symbols.Property(target) then | |
| 68 | property = cast Semantic.Symbols.Property?(target) | |
| 69 | elif path? /\ path.members.count > 0 then | |
| 70 | let last = path.members[path.members.count - 1] | |
| 71 | ||
| 72 | if isa Semantic.Symbols.Property(last) then | |
| 73 | property = cast Semantic.Symbols.Property?(last) | |
| 74 | fi | |
| 75 | fi | |
| 76 | ||
| 77 | if !property? then | |
| 78 | return false | |
| 79 | fi | |
| 80 | ||
| 81 | return _stable_hop_call(property, callee) | |
| 82 | si | |
| 83 | ||
| 84 | _stable_hop_call(property: Semantic.Symbols.Property, callee: Function) -> bool static is | |
| 85 | let getter = property.read_function | |
| 86 | ||
| 87 | if !getter? then | |
| 88 | return false | |
| 89 | fi | |
| 90 | ||
| 91 | return | |
| 92 | getter.root_specialized_from == callee.root_specialized_from /\ | |
| 93 | property.is_declared_stable | |
| 94 | si | |
| 95 | ||
| 96 | ||
| 97 | // The first property a provenance's fact reads through whose | |
| 98 | // getter is self-unstable for the fact — its own call, | |
| 99 | // treated as an ordinary crossing over the fact, is not | |
| 100 | // discharged by the solved effect relations — or null when | |
| 101 | // every getter backs the fact. No special case: this is the | |
| 102 | // same question asked of any call crossed over a property | |
| 103 | // fact, so a store-free, passthrough or write-only getter | |
| 104 | // backs both kinds, a monotone memoiser backs presence only, | |
| 105 | // and a getter that writes what its closure reads backs | |
| 106 | // neither. | |
| 107 | first_unproven_getter(target: Symbol?, path: ACCESS_PATH?, for_presence: bool) -> Symbol? static is | |
| 108 | if target? then | |
| 109 | if _self_unstable_getter(target, target, null, for_presence) then | |
| 110 | return target | |
| 111 | fi | |
| 112 | ||
| 113 | return null | |
| 114 | fi | |
| 115 | ||
| 116 | if path? then | |
| 117 | if _self_unstable_getter(path.root, null, path, for_presence) then | |
| 118 | return path.root | |
| 119 | fi | |
| 120 | ||
| 121 | for m in path.members do | |
| 122 | if _self_unstable_getter(m, null, path, for_presence) then | |
| 123 | return m | |
| 124 | fi | |
| 125 | od | |
| 126 | fi | |
| 127 | ||
| 128 | return null | |
| 129 | si | |
| 130 | ||
| 131 | // Whether `m` is a property whose getter does not back a | |
| 132 | // fact read through it: the getter's own call, asked of the | |
| 133 | // fact as any crossing is. Non-property hops back every fact. | |
| 134 | _self_unstable_getter(m: Symbol, target: Symbol?, path: ACCESS_PATH?, for_presence: bool) -> bool static is | |
| 135 | if !isa Semantic.Symbols.Property(m) then | |
| 136 | return false | |
| 137 | fi | |
| 138 | ||
| 139 | let property = cast Semantic.Symbols.Property(m) | |
| 140 | ||
| 141 | // A declared-stable getter is trusted to re-read to the | |
| 142 | // same answer — presence and runtime type alike — so its | |
| 143 | // own call backs both fact kinds without proof. Other | |
| 144 | // calls' crossings over the fact are judged as usual. | |
| 145 | if property.is_declared_stable then | |
| 146 | return false | |
| 147 | fi | |
| 148 | ||
| 149 | let getter = property.read_function | |
| 150 | ||
| 151 | if !getter? then | |
| 152 | return false | |
| 153 | fi | |
| 154 | ||
| 155 | return !crossing_discharged(CROSSING(m.location, getter), target, path, for_presence) | |
| 156 | si | |
| 157 | ||
| 158 | // The unbacked-at-formation classification: some getter the | |
| 159 | ||
| 160 | // A fact read through a getter survives a crossing when the | |
| 161 | // callee provably writes nothing the getters read: the | |
| 162 | // callee's write set is disjoint from the union of the fact's | |
| 163 | // hop symbols and every getter hop's read closure, elements | |
| 164 | // included. Anything unboundable on either side declines. | |
| 165 | _trace_this: bool static | |
| 166 | ||
| 167 | _getter_fact_discharged(callee: Function, target: Symbol?, path: ACCESS_PATH?) -> bool static is | |
| 168 | let reads = Collections.SET[int]() | |
| 169 | let reads_elements mut = false | |
| 170 | ||
| 171 | if target? then | |
| 172 | if !_collect_hop_reads(target, reads) then | |
| 173 | return false | |
| 174 | fi | |
| 175 | ||
| 176 | reads_elements = _hop_reads_elements(target) | |
| 177 | fi | |
| 178 | ||
| 179 | if path? then | |
| 180 | if !_collect_hop_reads(path.root, reads) then | |
| 181 | return false | |
| 182 | fi | |
| 183 | ||
| 184 | reads_elements = reads_elements \/ _hop_reads_elements(path.root) | |
| 185 | ||
| 186 | for m in path.members do | |
| 187 | if !_collect_hop_reads(m, reads) then | |
| 188 | return false | |
| 189 | fi | |
| 190 | ||
| 191 | reads_elements = reads_elements \/ _hop_reads_elements(m) | |
| 192 | od | |
| 193 | fi | |
| 194 | ||
| 195 | if _trace_this then | |
| 196 | let ws = EFFECTS.write_set_of(callee) | |
| 197 | ||
| 198 | IO.Std.error.write_line(" gfd: reads {reads.count} elements {reads_elements} callee-writes {if ws? then "{ws.count}" else "unbounded" fi} callee-writes-elements {EFFECTS.may_write_elements(callee)}") | |
| 199 | ||
| 200 | for m in reads do | |
| 201 | IO.Std.error.write_line(" gfd: read id {m} may_write {EFFECTS.may_write(callee, m)}") | |
| 202 | od | |
| 203 | fi | |
| 204 | ||
| 205 | if reads_elements /\ EFFECTS.may_write_elements(callee) then | |
| 206 | return false | |
| 207 | fi | |
| 208 | ||
| 209 | for m in reads do | |
| 210 | if EFFECTS.may_write(callee, m) then | |
| 211 | return false | |
| 212 | fi | |
| 213 | od | |
| 214 | ||
| 215 | return true | |
| 216 | si | |
| 217 | ||
| 218 | // Add the hop symbol itself, and - when it is a property - | |
| 219 | // its getter's read closure. False when the closure cannot be | |
| 220 | // bounded. | |
| 221 | _collect_hop_reads(m: Symbol, reads: Collections.SET[int]) -> bool static is | |
| 222 | reads.add(m.root_specialized_from.id) | |
| 223 | ||
| 224 | if !isa Semantic.Symbols.Property(m) then | |
| 225 | return true | |
| 226 | fi | |
| 227 | ||
| 228 | let getter = (cast Semantic.Symbols.Property(m)).read_function | |
| 229 | ||
| 230 | if !getter? then | |
| 231 | return false | |
| 232 | fi | |
| 233 | ||
| 234 | let closure = EFFECTS.getter_read_closure(getter) | |
| 235 | ||
| 236 | if _trace_this then | |
| 237 | IO.Std.error.write_line(" gfd: hop {m.qualified_name} getter known {EFFECTS.knows(getter)} closure {if closure? then "{closure.count}" else "unbounded" fi} elements {EFFECTS.getter_reads_elements(getter)}") | |
| 238 | fi | |
| 239 | ||
| 240 | if !closure? then | |
| 241 | return false | |
| 242 | fi | |
| 243 | ||
| 244 | for r in closure do | |
| 245 | reads.add(r) | |
| 246 | od | |
| 247 | ||
| 248 | return true | |
| 249 | si | |
| 250 | ||
| 251 | _hop_reads_elements(m: Symbol) -> bool static is | |
| 252 | if !isa Semantic.Symbols.Property(m) then | |
| 253 | return false | |
| 254 | fi | |
| 255 | ||
| 256 | return EFFECTS.getter_reads_elements((cast Semantic.Symbols.Property(m)).read_function) | |
| 257 | si | |
| 258 | ||
| 259 | // Whether `crossing`'s callee provably left the fact alone. | |
| 260 | // A fact read through a getter — a property target, or a path | |
| 261 | // with a getter hop — needs a callee that stores nothing at | |
| 262 | // all, since a getter can read anything a store changed. A | |
| 263 | // fields-only fact needs less: a presence fact survives any | |
| 264 | // callee that cannot assign a possibly-absent value to its | |
| 265 | // member, and a type narrow survives any callee that cannot | |
| 266 | // store to it; for a path, every hop below the last is held | |
| 267 | // to may-write, since rewriting a prefix redirects the path | |
| 268 | // to a different object entirely. | |
| 269 | ||
| 270 | // Whether the crossing's callee provably left the identified | |
| 271 | // fact alone: the question the walk asks at every call a heap | |
| 272 | // fact is live across, and the ledger re-asks after each solve. | |
| 273 | crossing_discharged(crossing: CROSSING, target: Symbol?, path: ACCESS_PATH?, is_presence: bool) -> bool static is | |
| 274 | let callee = crossing.callee | |
| 275 | ||
| 276 | if !callee? then | |
| 277 | return false | |
| 278 | fi | |
| 279 | ||
| 280 | _trace_this = false | |
| 281 | ||
| 282 | if let want = System.Environment.get_environment_variable("GHUL_CROSSING_TRACE") then | |
| 283 | if "{crossing.location}".contains(want) then | |
| 284 | _trace_this = true | |
| 285 | IO.Std.error.write_line("crossing {crossing.location} callee {callee.qualified_name} bit {callee.is_store_free} solved {EFFECTS.is_store_free(callee)} known {EFFECTS.knows(callee)} ctor {callee.is_constructor} stable {_is_stable_self_call(callee, target, path)} mono {_is_presence_monotone_self_call(callee, target, path)} gfd {_getter_fact_discharged(callee, target, path)} rcv {callee.writes_only_receiver_interior}") | |
| 286 | fi | |
| 287 | fi | |
| 288 | ||
| 289 | let getter = | |
| 290 | (target? /\ isa Semantic.Symbols.Property(target)) \/ | |
| 291 | (path? /\ path.has_getter_hop) | |
| 292 | ||
| 293 | if callee.is_store_free \/ EFFECTS.is_store_free(callee) then | |
| 294 | return true | |
| 295 | fi | |
| 296 | ||
| 297 | // A constructor that writes only its own fresh receiver's | |
| 298 | // state is harmless to every fact established before the | |
| 299 | // construction — including one read through a getter, | |
| 300 | // since nothing pre-existing can reach the fresh object. | |
| 301 | if callee.is_constructor /\ EFFECTS.constructs_store_free(callee) then | |
| 302 | return true | |
| 303 | fi | |
| 304 | ||
| 305 | if getter then | |
| 306 | if _is_stable_self_call(callee, target, path) then | |
| 307 | return true | |
| 308 | fi | |
| 309 | ||
| 310 | if is_presence /\ _is_presence_monotone_self_call(callee, target, path) then | |
| 311 | return true | |
| 312 | fi | |
| 313 | ||
| 314 | return _getter_fact_discharged(callee, target, path) | |
| 315 | fi | |
| 316 | ||
| 317 | if callee.writes_only_receiver_interior then | |
| 318 | return true | |
| 319 | fi | |
| 320 | ||
| 321 | if target? then | |
| 322 | if is_presence then | |
| 323 | return !EFFECTS.may_null(callee, target) | |
| 324 | fi | |
| 325 | ||
| 326 | return !EFFECTS.may_write(callee, target) | |
| 327 | fi | |
| 328 | ||
| 329 | if path? then | |
| 330 | // A field root can be redirected by a callee's store; | |
| 331 | // so can a local root a closure body assigns, whose | |
| 332 | // heap cell the write set names like any member. | |
| 333 | if | |
| 334 | (isa Semantic.Symbols.Field(path.root) \/ NARROW_ENV.is_closure_assigned(path.root)) /\ | |
| 335 | EFFECTS.may_write(callee, path.root) | |
| 336 | then | |
| 337 | return false | |
| 338 | fi | |
| 339 | ||
| 340 | let members = path.members | |
| 341 | ||
| 342 | for i in 0..members.count do | |
| 343 | let hop = members[i] | |
| 344 | ||
| 345 | if i < members.count - 1 then | |
| 346 | if EFFECTS.may_write(callee, hop) then | |
| 347 | return false | |
| 348 | fi | |
| 349 | elif is_presence then | |
| 350 | return !EFFECTS.may_null(callee, hop) | |
| 351 | else | |
| 352 | return !EFFECTS.may_write(callee, hop) | |
| 353 | fi | |
| 354 | od | |
| 355 | ||
| 356 | return true | |
| 357 | fi | |
| 358 | ||
| 359 | return false | |
| 360 | si | |
| 361 | si | |
| 362 | si |