Appearance
| 1 | namespace Syntax.Process is | |
| 2 | use Logging.Logger | |
| 3 | use Source.LOCATION | |
| 4 | use Semantic.Types.Type | |
| 5 | use Semantic.Types.INTERSECTION | |
| 6 | use Symbol = Semantic.Symbols.Symbol | |
| 7 | use Ghul.Disposable | |
| 8 | ||
| 9 | // Per-IF bookkeeping for the flow pass. pre(IF) pushes a frame; | |
| 10 | // each branch's controlled walk records its body-exit | |
| 11 | // environment and threads the running else-environment to the | |
| 12 | // next branch; visit(IF) joins the branch exits. | |
| 13 | class IF_FLOW_FRAME is | |
| 14 | // Environment for the next not-yet-walked branch — refined | |
| 15 | // by each cond branch's false edge as the chain proceeds. | |
| 16 | running_else: NARROW_ENV public | |
| 17 | // Exit environment of each branch already walked (bottom for | |
| 18 | // a branch whose body diverges). | |
| 19 | branch_exits: Collections.LIST[NARROW_ENV] public | |
| 20 | // True once an unconditional (else) branch has been seen. | |
| 21 | has_else: bool public | |
| 22 | ||
| 23 | init(in_env: NARROW_ENV) is | |
| 24 | running_else = in_env | |
| 25 | branch_exits = Collections.LIST[NARROW_ENV]() | |
| 26 | si | |
| 27 | si | |
| 28 | ||
| 29 | // Per-CASE bookkeeping for the flow pass, mirroring IF_FLOW_FRAME. | |
| 30 | // Case arms are mutually exclusive alternatives rather than a | |
| 31 | // chained if/elif, so every arm's body walks from the same | |
| 32 | // pre-case entry environment (plus whatever narrowing the arm's | |
| 33 | // own pattern/guard adds) instead of a running_else threaded arm | |
| 34 | // to arm — a case has no equivalent of an elif's "previous | |
| 35 | // conditions were false" fact today, since the else-arm complement | |
| 36 | // narrowing this would require isn't implemented (see the | |
| 37 | // `case-when-pattern-scrutinee-narrow` test region). pre(CASE) | |
| 38 | // pushes a frame; each arm's controlled walk resets to `entry`, | |
| 39 | // applies its own narrowing, walks its body, and records the | |
| 40 | // exit; visit(CASE) joins the arm exits, plus `entry` itself when | |
| 41 | // no `else` arm was seen — the no-arm-matched fall-through. | |
| 42 | class CASE_FLOW_FRAME is | |
| 43 | entry: NARROW_ENV public | |
| 44 | branch_exits: Collections.LIST[NARROW_ENV] public | |
| 45 | has_else: bool public | |
| 46 | ||
| 47 | init(entry: NARROW_ENV) is | |
| 48 | self.entry = entry | |
| 49 | branch_exits = Collections.LIST[NARROW_ENV]() | |
| 50 | si | |
| 51 | si | |
| 52 | ||
| 53 | // Per-`try` bookkeeping for the flow pass. pre(TRY) pushes a | |
| 54 | // frame; pre(CATCH) observes the try body's exit, visit(CATCH) | |
| 55 | // each handler's exit, and visit(TRY) the no-catch body exit, so | |
| 56 | // visit(TRY) can tell whether control can fall through the try | |
| 57 | // statement at all (it cannot when the body and every handler | |
| 58 | // diverge). | |
| 59 | class TRY_FLOW_FRAME is | |
| 60 | // The environment in force before the try — its | |
| 61 | // definite-assignment facts survive the statement. | |
| 62 | entry: NARROW_ENV public | |
| 63 | // True once the try body's exit environment has been | |
| 64 | // observed (at the first catch, or — with no catches — at | |
| 65 | // visit(TRY)). | |
| 66 | body_seen: bool public | |
| 67 | // True if the body, or some catch handler, can complete | |
| 68 | // normally and so reach the end of the try statement. | |
| 69 | can_complete: bool public | |
| 70 | // True if the finally body cannot complete normally, in | |
| 71 | // which case control never falls through the try however | |
| 72 | // the body and handlers fared. | |
| 73 | finally_diverges: bool public | |
| 74 | ||
| 75 | init(entry: NARROW_ENV) is | |
| 76 | self.entry = entry | |
| 77 | si | |
| 78 | si | |
| 79 | ||
| 80 | ||
| 81 | // The flow-sensitive narrowing orchestrator. Holds the narrowing | |
| 82 | // environment in force at the current walk point and keeps each | |
| 83 | // narrowed variable's `Symbol.type` reconciled to it, so the | |
| 84 | // rest of COMPILE_EXPRESSIONS — and the per-use-site IR value | |
| 85 | // snapshots the IDE reads — observe the narrowed type. | |
| 86 | // | |
| 87 | // Replaces the scope-stack NARROWING. See | |
| 88 | // `docs/claude/flow-sensitive-narrowing.md`. | |
| 89 | class NARROWING_FLOW is | |
| 90 | // Sink for the analysis-mode narrowing-kill hints. Its | |
| 91 | // `want_hint_for` gate and `hint` are the only members consulted | |
| 92 | // here. | |
| 93 | _logger: Logger | |
| 94 | ||
| 95 | _current_env: NARROW_ENV | |
| 96 | // Declared (pre-narrowing) type of every variable that has | |
| 97 | // been narrowed — the restore target. Captured lazily the | |
| 98 | // first time a variable is narrowed. | |
| 99 | _declared: Collections.MAP[Symbol, Type] | |
| 100 | ||
| 101 | // Deferred-initialization locals (`let x: T;` with no | |
| 102 | // initializer) subject to the definite-assignment read | |
| 103 | // check. Method-global within one body walk — a variable, | |
| 104 | // once declared, stays tracked until the next reset. | |
| 105 | _tracked: Collections.SET[Symbol] | |
| 106 | ||
| 107 | // Assignment-target receivers held exempt from the call transfer | |
| 108 | // while their assignment is in flight. See RECEIVER_SHIELD. | |
| 109 | _shield: RECEIVER_SHIELD | |
| 110 | ||
| 111 | // Bumped by every heap-fact kill (call, heap store, member | |
| 112 | // store). Controlled walks capture it before walking and | |
| 113 | // compare after: branch environments derived from a snapshot | |
| 114 | // taken before a walk that killed cannot keep the snapshot's | |
| 115 | // heap facts. `_current_env` itself always reflects kills | |
| 116 | // directly, so straight-line flow needs no epoch check. | |
| 117 | _heap_epoch: int | |
| 118 | ||
| 119 | // Speculation baselines, mirroring the logger's diagnostics | |
| 120 | // stack. A speculative expression re-walk pushes the pre-walk | |
| 121 | // env, resets to it between retry attempts, and on completion | |
| 122 | // either commits (keeps the final walk's facts) or rolls back | |
| 123 | // (discards them). This keeps the flow env and the coupled | |
| 124 | // in-place `Symbol.type` narrowing from desyncing when a | |
| 125 | // re-walk's diagnostics are scrubbed. | |
| 126 | _speculation: Collections.STACK[NARROW_ENV] | |
| 127 | ||
| 128 | ||
| 129 | // Every call crossing this body walk has noted, in order — | |
| 130 | // the source adopt_crossings_* copies from. Grows for the | |
| 131 | // body's duration and clears at reset(). A rolled-back | |
| 132 | // speculative walk's entries stay in the log; adopting them | |
| 133 | // is conservative (an extra crossing can only add an | |
| 134 | // obligation), and the retry re-walks the same calls anyway. | |
| 135 | _crossing_log: Collections.LIST[CROSSING] | |
| 136 | ||
| 137 | // The crossing-log count at the moment each condition-leaf | |
| 138 | // test expression was first compiled — an `isa`, a `?`, a | |
| 139 | // null-comparison. The condition analyzer reads it back when | |
| 140 | // it forms a leaf's facts, so adoption can skip the calls a | |
| 141 | // condition walked before the leaf's own test ran. First walk | |
| 142 | // wins: a crossing excluded by that stamp ran before the leaf | |
| 143 | // in every walk that reached it, and a speculative walk's | |
| 144 | // re-stamp can only attach more. | |
| 145 | _test_site_marks: Collections.MAP[Trees.Expressions.Expression, int] | |
| 146 | ||
| 147 | init(logger: Logger) is | |
| 148 | _logger = logger | |
| 149 | _crossing_log = Collections.LIST[CROSSING]() | |
| 150 | _test_site_marks = Collections.MAP[Trees.Expressions.Expression, int]() | |
| 151 | _current_env = NARROW_ENV() | |
| 152 | _declared = Collections.MAP[Symbol, Type]() | |
| 153 | _tracked = Collections.SET[Symbol]() | |
| 154 | _shield = RECEIVER_SHIELD() | |
| 155 | _speculation = Collections.STACK[NARROW_ENV]() | |
| 156 | si | |
| 157 | ||
| 158 | // Surface a hint at the point a narrowing is discarded, so the | |
| 159 | // editor can show where and why a narrowed type stops | |
| 160 | // applying. Emitted only in analysis mode, and only for a | |
| 161 | // variable that actually carries a narrow at this point — | |
| 162 | // `reason` names what invalidated it. Must be called before | |
| 163 | // the narrow is dropped, while `_current_env` still holds it. | |
| 164 | _report_kill(v: Symbol, location: LOCATION, reason: string) is | |
| 165 | // Editor-only: never generate a kill hint for a file the client | |
| 166 | // is not viewing — it would be invisible there and only add | |
| 167 | // formatting and transmission cost. | |
| 168 | if !_logger.want_hint_for(location) then | |
| 169 | return | |
| 170 | fi | |
| 171 | ||
| 172 | let narrowed = _current_env.narrowed_type_of(v) | |
| 173 | let declared = declared_type_of(v) | |
| 174 | ||
| 175 | if narrowed? then | |
| 176 | _logger.inlay(location, "narrowing-killed", "◄", "{v.name}\n ◄ {declared}\n\n{reason}") | |
| 177 | elif _current_env.is_non_null(v) then | |
| 178 | // The presence bit is redundant with a non-optional | |
| 179 | // declared type — a non-optional variable is always | |
| 180 | // known to hold a value, so the bit adds nothing over | |
| 181 | // the declaration and the kill hint would confuse the | |
| 182 | // reader by pointing at a narrowing that never carried | |
| 183 | // information. | |
| 184 | if declared? /\ declared.is_optional then | |
| 185 | _logger.inlay(location, "narrowing-killed", "◄", "{v.name}\n ◄ {declared}\n\n{reason}") | |
| 186 | fi | |
| 187 | fi | |
| 188 | si | |
| 189 | ||
| 190 | // Path analogue of `_report_kill`: surface a hint at the point | |
| 191 | // a member-access path's narrow or presence fact is discarded. | |
| 192 | // A path presence fact is only ever recorded for an optional | |
| 193 | // access, so — unlike the symbol case — there is no redundant | |
| 194 | // non-optional branch to guard. Same analysis-mode + open-file | |
| 195 | // gating; must be called while `_current_env` still holds the | |
| 196 | // fact. | |
| 197 | _report_path_kill(path: ACCESS_PATH, location: LOCATION, reason: string) is | |
| 198 | if !_logger.want_hint_for(location) then | |
| 199 | return | |
| 200 | fi | |
| 201 | ||
| 202 | let narrowed = _current_env.narrowed_type_of_path(path) | |
| 203 | ||
| 204 | // A member-access path has no single declared type to name as | |
| 205 | // the revert target, so the code body is just the path; the | |
| 206 | // reason carries what changed. | |
| 207 | if narrowed? then | |
| 208 | _logger.inlay(location, "narrowing-killed", "◄", "{path}\n\n{reason}") | |
| 209 | elif _current_env.is_non_null_path(path) then | |
| 210 | _logger.inlay(location, "narrowing-killed", "◄", "{path}\n\n{reason}") | |
| 211 | fi | |
| 212 | si | |
| 213 | ||
| 214 | current_env: NARROW_ENV => _current_env | |
| 215 | is_unreachable: bool => _current_env.is_bottom | |
| 216 | ||
| 217 | heap_epoch: int => _heap_epoch | |
| 218 | ||
| 219 | // True iff a heap-fact kill has fired since `epoch` was | |
| 220 | // captured. | |
| 221 | heap_killed_since(epoch: int) -> bool => _heap_epoch != epoch | |
| 222 | ||
| 223 | // While a function literal's body compiles, the transfers | |
| 224 | // also record whether it performed any possibly heap-visible | |
| 225 | // operation — the signal behind Function.literal_body_impure. | |
| 226 | // A call only charges the frame when it records a crossing, | |
| 227 | // so a call to a structurally store-free callee — declared | |
| 228 | // pure, whitelisted, a backing read — leaves the literal | |
| 229 | // clean; a call the solve would later prove harmless still | |
| 230 | // charges it, so the pure shape surfaces on fewer literals | |
| 231 | // than the solve proves. That costs display only: the pure | |
| 232 | // slot judge answers from the solved relations, not from the | |
| 233 | // shape. A stack because literals nest; only the innermost | |
| 234 | // literal is charged (an outer literal that never invokes the | |
| 235 | // inner one is unaffected by it). | |
| 236 | _literal_impure_stack: Collections.LIST[bool]? | |
| 237 | ||
| 238 | push_literal_frame() is | |
| 239 | if !_literal_impure_stack? then | |
| 240 | _literal_impure_stack = Collections.LIST[bool]() | |
| 241 | fi | |
| 242 | ||
| 243 | _literal_impure_stack.add(false) | |
| 244 | si | |
| 245 | ||
| 246 | pop_literal_frame() -> bool is | |
| 247 | let stack = _literal_impure_stack | |
| 248 | ||
| 249 | assert stack? | |
| 250 | ||
| 251 | let result = stack[stack.count - 1] | |
| 252 | stack.remove_at(stack.count - 1) | |
| 253 | return result | |
| 254 | si | |
| 255 | ||
| 256 | _mark_literal_impure() is | |
| 257 | if _literal_impure_stack? /\ _literal_impure_stack.count > 0 then | |
| 258 | _literal_impure_stack[_literal_impure_stack.count - 1] = true | |
| 259 | fi | |
| 260 | si | |
| 261 | ||
| 262 | // Narrowing subjects are local variables, fields and | |
| 263 | // properties — all carry a settable type; anything else never | |
| 264 | // enters the environment, but stay defensive. | |
| 265 | _set_symbol_type(v: Symbol, t: Type) is | |
| 266 | if isa Semantic.Types.SettableTyped(v) then | |
| 267 | (cast Semantic.Types.SettableTyped(v)).set_type(t) | |
| 268 | fi | |
| 269 | si | |
| 270 | ||
| 271 | // Restore every currently-narrowed variable to its declared | |
| 272 | // type, empty the environment, and forget declared types. | |
| 273 | // Called at each method-body boundary. | |
| 274 | reset() is | |
| 275 | restore_all() | |
| 276 | _current_env = NARROW_ENV() | |
| 277 | _declared.clear() | |
| 278 | _tracked.clear() | |
| 279 | ||
| 280 | // literal frames are pushed and popped around literal | |
| 281 | // body walks; an aborted walk (analysis-mode exception) | |
| 282 | // can leak one, so drop any leftovers at body boundaries | |
| 283 | if _literal_impure_stack? then | |
| 284 | _literal_impure_stack.clear() | |
| 285 | fi | |
| 286 | ||
| 287 | _crossing_log.clear() | |
| 288 | _test_site_marks.clear() | |
| 289 | ||
| 290 | // Speculation baselines are balanced by the `speculate_then_*` | |
| 291 | // disposables, but an aborted walk can leak one; drop any | |
| 292 | // leftovers at the body boundary (inert env copies — nothing | |
| 293 | // to restore, restore_all already reconciled `Symbol.type`). | |
| 294 | _speculation.clear() | |
| 295 | si | |
| 296 | ||
| 297 | // Restore every currently-narrowed variable's `.type` to its | |
| 298 | // declared type (without emptying the environment). | |
| 299 | restore_all() is | |
| 300 | for v in _current_env.variables do | |
| 301 | let declared: Type mut | |
| 302 | ||
| 303 | if _declared.try_get_value(v, declared ref) then | |
| 304 | _set_symbol_type(v, declared) | |
| 305 | fi | |
| 306 | od | |
| 307 | si | |
| 308 | ||
| 309 | // The declared (pre-narrowing) type of `v` — used for the | |
| 310 | // assignment-LHS typecheck, which must see past any narrow. | |
| 311 | declared_type_of(v: Symbol) -> Type? is | |
| 312 | let declared: Type mut | |
| 313 | ||
| 314 | if _declared.try_get_value(v, declared ref) then | |
| 315 | return declared | |
| 316 | fi | |
| 317 | ||
| 318 | return v.type | |
| 319 | si | |
| 320 | ||
| 321 | // Make `target` the environment in force: restore all | |
| 322 | // current narrows, then apply `target`'s sound narrows, | |
| 323 | // reconciling `Symbol.type` to match. `_current_env` | |
| 324 | // becomes the actually-applied subset of `target`. | |
| 325 | set_env(target: NARROW_ENV) is | |
| 326 | restore_all() | |
| 327 | ||
| 328 | let applied = NARROW_ENV() | |
| 329 | ||
| 330 | if target.is_bottom then | |
| 331 | applied.is_bottom = true | |
| 332 | else | |
| 333 | for v in target.variables do | |
| 334 | if let t = target.narrowed_type_of(v) then | |
| 335 | if _apply_one(v, t) then | |
| 336 | applied.set_narrow(v, t) | |
| 337 | fi | |
| 338 | fi | |
| 339 | od | |
| 340 | ||
| 341 | for v in target.assigned_variables do | |
| 342 | applied.set_assigned(v) | |
| 343 | od | |
| 344 | ||
| 345 | for f in target.called_methods do | |
| 346 | applied.set_called(f) | |
| 347 | od | |
| 348 | ||
| 349 | for v in target.non_null_variables do | |
| 350 | applied.set_non_null(v) | |
| 351 | od | |
| 352 | ||
| 353 | for p in target.non_null_paths do | |
| 354 | applied.set_non_null_path(p) | |
| 355 | od | |
| 356 | ||
| 357 | for p in target.narrowed_paths do | |
| 358 | if let t = target.narrowed_type_of_path(p) then | |
| 359 | applied.set_path_narrow(p, t) | |
| 360 | fi | |
| 361 | od | |
| 362 | fi | |
| 363 | ||
| 364 | // the set_* establishment calls above cleared the records | |
| 365 | // a branch entry must carry forward | |
| 366 | applied.adopt_crossings_from(target) | |
| 367 | applied.adopt_creation_marks_from(target) | |
| 368 | ||
| 369 | _current_env = applied | |
| 370 | si | |
| 371 | ||
| 372 | // Snapshot the current env as a speculation baseline (see | |
| 373 | // `_speculation`). Pairs with `commit` or `roll_back`; usually | |
| 374 | // reached through the `speculate_then_*` disposables. | |
| 375 | speculate() is | |
| 376 | _speculation.push(_current_env.copy()) | |
| 377 | PURE_SLOTS.speculate() | |
| 378 | si | |
| 379 | ||
| 380 | // Reset the current env to the active baseline without dropping | |
| 381 | // it, so a retry re-walk starts from the facts the first walk | |
| 382 | // saw rather than the ones it recorded. A no-op when no | |
| 383 | // speculation is active, so callers that may or may not run | |
| 384 | // inside a speculation can call it unconditionally. | |
| 385 | restore() is | |
| 386 | if _speculation.count > 0 then | |
| 387 | set_env(_speculation.peek()) | |
| 388 | fi | |
| 389 | si | |
| 390 | ||
| 391 | // Drop the active baseline, keeping the current env — the | |
| 392 | // walk's narrowing facts survive into the enclosing expression. | |
| 393 | commit() is | |
| 394 | assert _speculation.count >= 1 else "flow commit with no active speculation" | |
| 395 | ||
| 396 | _speculation.pop() | |
| 397 | PURE_SLOTS.commit() | |
| 398 | si | |
| 399 | ||
| 400 | // Drop the active baseline and restore the current env to it, | |
| 401 | // discarding the speculative walk's narrowing facts. | |
| 402 | roll_back() is | |
| 403 | assert _speculation.count >= 1 else "flow roll_back with no active speculation" | |
| 404 | ||
| 405 | set_env(_speculation.pop()) | |
| 406 | PURE_SLOTS.roll_back() | |
| 407 | si | |
| 408 | ||
| 409 | speculate_then_commit() -> FLOW_SPECULATE_THEN_COMMIT => | |
| 410 | FLOW_SPECULATE_THEN_COMMIT(self) | |
| 411 | ||
| 412 | speculate_then_roll_back() -> FLOW_SPECULATE_THEN_ROLL_BACK => | |
| 413 | FLOW_SPECULATE_THEN_ROLL_BACK(self) | |
| 414 | ||
| 415 | // Mark the current point unreachable (after return / throw / | |
| 416 | // break / continue). | |
| 417 | set_unreachable() is | |
| 418 | set_env(NARROW_ENV.bottom()) | |
| 419 | si | |
| 420 | ||
| 421 | // Assignment transfer plus re-narrow: a write to `v` | |
| 422 | // invalidates any narrow on it and any presence fact, since | |
| 423 | // the new value may not satisfy them; when the assigned | |
| 424 | // value's static type is a strict refinement of the declared | |
| 425 | // type, `v` then re-narrows to it. Returns the narrowed-to | |
| 426 | // view when one was applied, else null. | |
| 427 | // | |
| 428 | // The editor hint reflects which of the two halves fired: a | |
| 429 | // re-narrow to a different view renders both edges in one | |
| 430 | // hint (the killed view and the new one) with the usual | |
| 431 | // reassignment note; a re-narrow to the same view is a plain | |
| 432 | // introduction; a kill with no new narrow keeps the plain | |
| 433 | // kill hint. | |
| 434 | on_assignment(v: Symbol, location: LOCATION, value_type: Type?) -> Type? is | |
| 435 | // The in-force facts, captured before the transfer drops | |
| 436 | // them, so the hint can name the killed view. | |
| 437 | let killed_narrow = _current_env.narrowed_type_of(v) | |
| 438 | let killed_presence = _current_env.is_non_null(v) | |
| 439 | ||
| 440 | _assignment_transfer(v) | |
| 441 | ||
| 442 | let narrowed = narrow_to_assigned_value(v, value_type) | |
| 443 | ||
| 444 | if !_logger.want_hint_for(location) then | |
| 445 | return narrowed | |
| 446 | fi | |
| 447 | ||
| 448 | let reason = "{v.name} is reassigned" | |
| 449 | ||
| 450 | if narrowed? then | |
| 451 | if killed_narrow? /\ !killed_narrow.matches(narrowed) then | |
| 452 | _logger.inlay( | |
| 453 | location, | |
| 454 | "narrowing-assign", | |
| 455 | "◄►", | |
| 456 | "{v.name}\n ◄ {INLAY_TYPE.render(killed_narrow)}\n ► {INLAY_TYPE.render(narrowed)}\n\n{reason}") | |
| 457 | else | |
| 458 | _logger.inlay(location, "narrowing-assign", "►", INLAY_TYPE.render(narrowed)) | |
| 459 | fi | |
| 460 | ||
| 461 | return narrowed | |
| 462 | fi | |
| 463 | ||
| 464 | let declared = declared_type_of(v) | |
| 465 | ||
| 466 | if killed_narrow? then | |
| 467 | _logger.inlay(location, "narrowing-killed", "◄", "{v.name}\n ◄ {declared}\n\n{reason}") | |
| 468 | elif killed_presence then | |
| 469 | // The presence bit is redundant with a non-optional | |
| 470 | // declared type — a non-optional variable is always | |
| 471 | // known to hold a value, so the bit adds nothing over | |
| 472 | // the declaration and the kill hint would confuse the | |
| 473 | // reader by pointing at a narrowing that never carried | |
| 474 | // information. | |
| 475 | if declared? /\ declared.is_optional then | |
| 476 | _logger.inlay(location, "narrowing-killed", "◄", "{v.name}\n ◄ {declared}\n\n{reason}") | |
| 477 | fi | |
| 478 | fi | |
| 479 | ||
| 480 | return null | |
| 481 | si | |
| 482 | ||
| 483 | // The assignment transfer proper: drop every fact the write | |
| 484 | // invalidates and restore the declared view. | |
| 485 | _assignment_transfer(v: Symbol) is | |
| 486 | _mark_literal_impure() | |
| 487 | ||
| 488 | _current_env.drop_non_null(v) | |
| 489 | ||
| 490 | // Reassigning the root redirects every `v.…` path; and a | |
| 491 | // bare field target writes `self.<v>`, so any path reading | |
| 492 | // through that field — on any receiver — is stale too. | |
| 493 | _current_env.drop_paths_rooted_at(v) | |
| 494 | ||
| 495 | if isa Semantic.Symbols.Field(v) then | |
| 496 | _current_env.drop_paths_through(v) | |
| 497 | fi | |
| 498 | ||
| 499 | if !_current_env.contains(v) then | |
| 500 | return | |
| 501 | fi | |
| 502 | ||
| 503 | _current_env.drop_narrow(v) | |
| 504 | ||
| 505 | let declared = declared_type_of(v) | |
| 506 | ||
| 507 | if declared? then | |
| 508 | _set_symbol_type(v, declared) | |
| 509 | fi | |
| 510 | si | |
| 511 | ||
| 512 | // Narrow `v` to the static type of a just-assigned value when | |
| 513 | // that type is more specific than the declared type, so | |
| 514 | // `if isa CAT(pet) then pet = DOG()` leaves `pet` viewed as DOG | |
| 515 | // rather than reverting all the way to the declared Animal. The | |
| 516 | // assigned value always typechecks against the declared type, so | |
| 517 | // this only ever tightens, never relaxes. Runs after the | |
| 518 | // assignment transfer has reset the target to its declared | |
| 519 | // type. Returns the narrowed-to view when a narrow was | |
| 520 | // applied, else null. | |
| 521 | // | |
| 522 | // Locals only (locals and parameters): a field target wants the | |
| 523 | // path-narrow plumbing (`self.field` is an access path, and its | |
| 524 | // facts die at calls), not a symbol narrow. | |
| 525 | // | |
| 526 | // A null RHS contributes no type information — `x = null` is | |
| 527 | // fully described by the presence facts the assignment transfer | |
| 528 | // already maintains. | |
| 529 | // | |
| 530 | // A value-type RHS never narrows: storing a value type into a | |
| 531 | // wider slot boxes it, so the slot holds a box reference and a | |
| 532 | // bare-struct view would misdescribe every subsequent load — | |
| 533 | // plain reads carry no unbox projection. (A value-type slot | |
| 534 | // can't be narrowed anyway: structs have no subtypes.) | |
| 535 | // | |
| 536 | // Skipped on an unreachable edge: a bottom environment ignores | |
| 537 | // `set_narrow`, and applying the symbol-type half without the | |
| 538 | // environment record would leave a stale narrow no later | |
| 539 | // restore point knows about. | |
| 540 | narrow_to_assigned_value(v: Symbol, value_type: Type?) -> Type? is | |
| 541 | if | |
| 542 | !value_type? \/ | |
| 543 | value_type.is_null \/ | |
| 544 | value_type.is_value_type \/ | |
| 545 | !_narrows_on_assignment(v) \/ | |
| 546 | _current_env.is_bottom | |
| 547 | then | |
| 548 | return null | |
| 549 | fi | |
| 550 | ||
| 551 | // Only a strict refinement narrows. A mutually-assignable | |
| 552 | // RHS type is a different spelling of the same slot, not | |
| 553 | // extra information. | |
| 554 | let v_type = v.type | |
| 555 | ||
| 556 | if v_type? /\ value_type.is_assignable_from(v_type) then | |
| 557 | return null | |
| 558 | fi | |
| 559 | ||
| 560 | // Tuple element names sit outside the subtype lattice: an | |
| 561 | // unnamed tuple is assignable where a named-element tuple | |
| 562 | // is expected, at any nesting depth (an unnamed-tuple array | |
| 563 | // refines an Iterable of named tuples), so a view that | |
| 564 | // mentions a tuple can silently lose the declared names and | |
| 565 | // break by-name element access. Keep the declared spelling. | |
| 566 | if _mentions_tuple(value_type, 0) then | |
| 567 | return null | |
| 568 | fi | |
| 569 | ||
| 570 | if _apply_one(v, value_type) then | |
| 571 | _current_env.set_narrow(v, value_type) | |
| 572 | return v.type | |
| 573 | fi | |
| 574 | ||
| 575 | return null | |
| 576 | si | |
| 577 | ||
| 578 | // Whether a write to `v` re-narrows it. | |
| 579 | // | |
| 580 | // A local qualifies, and so does a variable at namespace or | |
| 581 | // file scope - a global, or a top-level `let`. Neither is a | |
| 582 | // member of a type, so the only way to write one is to name | |
| 583 | // it, and the fact is a heap fact like any other: it takes | |
| 584 | // crossings, and a use leaning on it across a call that | |
| 585 | // cannot be discharged is judged. | |
| 586 | // | |
| 587 | // A field or property of a type does not, though the fact | |
| 588 | // would be no less sound. A member's declared type is | |
| 589 | // routinely a trait the constructor assigns a concrete | |
| 590 | // implementation of, and the mutators called on it next - | |
| 591 | // `MAP.add`, and every other member whose body can re-enter | |
| 592 | // user code - cannot be discharged, so narrowing there turns | |
| 593 | // an everyday initialization idiom into an error at the | |
| 594 | // second call. That is the crossing discharge being | |
| 595 | // imprecise rather than the narrow being wrong, so this | |
| 596 | // waits on the discharge improving. | |
| 597 | _narrows_on_assignment(v: Symbol) -> bool => | |
| 598 | v.is_local \/ isa Semantic.Symbols.GLOBAL_VARIABLE(v) | |
| 599 | ||
| 600 | // True when `t` is or mentions a tuple type anywhere in its | |
| 601 | // type arguments. Depth-capped: type arguments cannot cycle, | |
| 602 | // but the cap keeps a malformed recursive shape from spinning. | |
| 603 | _mentions_tuple(t: Type?, depth: int) -> bool is | |
| 604 | if !t? \/ depth > 8 then | |
| 605 | return false | |
| 606 | fi | |
| 607 | ||
| 608 | // Tuple types appear in three shapes: the ghūl-side | |
| 609 | // Types.TUPLE, and the reflected ValueTuple wrappers, | |
| 610 | // which carry `is_value_tuple` / `tuple_element_names` | |
| 611 | // but are not TUPLE subclasses. | |
| 612 | if isa Semantic.Types.TUPLE(t) \/ t.is_value_tuple \/ t.tuple_element_names? then | |
| 613 | return true | |
| 614 | fi | |
| 615 | ||
| 616 | for a in t.arguments do | |
| 617 | if _mentions_tuple(a, depth + 1) then | |
| 618 | return true | |
| 619 | fi | |
| 620 | od | |
| 621 | ||
| 622 | return false | |
| 623 | si | |
| 624 | ||
| 625 | // Call transfer. Narrowing is optimistic: a call drops no | |
| 626 | // heap fact. Instead the call is recorded as a crossing | |
| 627 | // against every heap fact live over it, and each later use of | |
| 628 | // such a fact is judged against its crossings — a crossing | |
| 629 | // whose callee provably left the fact alone is discharged, | |
| 630 | // and relying on a fact with an undischarged crossing is a | |
| 631 | // compile error at the use site. Locals are unreachable to | |
| 632 | // the callee and take no crossings. Fires once a call | |
| 633 | // expression has been compiled — its receiver has already | |
| 634 | // been read, so the call's own narrowed access is unaffected. | |
| 635 | on_call(location: LOCATION) is | |
| 636 | on_call_of(location, null) | |
| 637 | si | |
| 638 | ||
| 639 | // The call transfer, told which function is being called. | |
| 640 | // `callee` is null where the site has no single bounded | |
| 641 | // callee — a closure invocation, an interpolation — which no | |
| 642 | // judgement can discharge. A call does not bump the heap | |
| 643 | // epoch: facts survive it optimistically, carrying the | |
| 644 | // crossing, and the epoch is what direct stores use to make | |
| 645 | // snapshot-derived environments drop. The crossing is also | |
| 646 | // logged so controlled walks can attach it to environments | |
| 647 | // derived from snapshots taken before the call ran. | |
| 648 | on_call_of(location: LOCATION, callee: Semantic.Symbols.Function?) is | |
| 649 | _mark_literal_impure() | |
| 650 | ||
| 651 | let crossing = CROSSING(location, callee) | |
| 652 | ||
| 653 | if KILL_LEDGER.can_kill_in_walk then | |
| 654 | _apply_relations(crossing) | |
| 655 | fi | |
| 656 | ||
| 657 | _current_env.note_crossing(crossing) | |
| 658 | _crossing_log.add(crossing) | |
| 659 | si | |
| 660 | ||
| 661 | // The in-walk kill transfer of the combined-solve prototype: a | |
| 662 | // heap fact the solved relations cannot show the callee left | |
| 663 | // alone dies at this call, the same question the reliance | |
| 664 | // judge would otherwise ask of each later use. Each kill is | |
| 665 | // recorded so a later solve can say whether it still holds. | |
| 666 | // See KILL_LEDGER. | |
| 667 | _apply_relations(crossing: CROSSING) is | |
| 668 | let file_name = crossing.location.file_name | |
| 669 | let details = Collections.LIST[string]() | |
| 670 | ||
| 671 | let doomed_narrows = Collections.LIST[Symbol]() | |
| 672 | ||
| 673 | for v in _current_env.heap_fact_variables do | |
| 674 | if | |
| 675 | _current_env.narrowed_type_of(v)? /\ | |
| 676 | !RELIANCES.crossing_discharged(crossing, v, null, false) | |
| 677 | then | |
| 678 | doomed_narrows.add(v) | |
| 679 | fi | |
| 680 | od | |
| 681 | ||
| 682 | for v in doomed_narrows do | |
| 683 | details.add("{v.name}\n ◄ {declared_type_of(v)}") | |
| 684 | ||
| 685 | let kill = KILL(file_name, crossing, v, null, false, true) | |
| 686 | ||
| 687 | kill.narrowed_type = _current_env.narrowed_type_of(v) | |
| 688 | ||
| 689 | _current_env.drop_narrow(v) | |
| 690 | ||
| 691 | let declared = declared_type_of(v) | |
| 692 | ||
| 693 | if declared? then | |
| 694 | _set_symbol_type(v, declared) | |
| 695 | fi | |
| 696 | ||
| 697 | KILL_LEDGER.record(kill) | |
| 698 | od | |
| 699 | ||
| 700 | let doomed_presence = Collections.LIST[Symbol]() | |
| 701 | ||
| 702 | for v in _current_env.heap_fact_variables do | |
| 703 | if | |
| 704 | _current_env.is_non_null(v) /\ | |
| 705 | !RELIANCES.crossing_discharged(crossing, v, null, true) | |
| 706 | then | |
| 707 | doomed_presence.add(v) | |
| 708 | fi | |
| 709 | od | |
| 710 | ||
| 711 | for v in doomed_presence do | |
| 712 | let declared = declared_type_of(v) | |
| 713 | ||
| 714 | // a presence bit on a non-optional declaration carried | |
| 715 | // nothing over the declaration, so its loss is not shown | |
| 716 | if declared? /\ declared.is_optional /\ !doomed_narrows.contains(v) then | |
| 717 | details.add("{v.name}\n ◄ {declared}") | |
| 718 | fi | |
| 719 | ||
| 720 | _current_env.drop_non_null(v) | |
| 721 | ||
| 722 | KILL_LEDGER.record(KILL(file_name, crossing, v, null, true, true)) | |
| 723 | od | |
| 724 | ||
| 725 | let doomed_paths = Collections.LIST[ACCESS_PATH]() | |
| 726 | ||
| 727 | for p in _current_env.heap_fact_paths do | |
| 728 | let is_presence = !_current_env.narrowed_type_of_path(p)? | |
| 729 | ||
| 730 | if !RELIANCES.crossing_discharged(crossing, null, p, is_presence) then | |
| 731 | doomed_paths.add(p) | |
| 732 | fi | |
| 733 | od | |
| 734 | ||
| 735 | for p in doomed_paths do | |
| 736 | let is_presence = !_current_env.narrowed_type_of_path(p)? | |
| 737 | ||
| 738 | details.add("{p}") | |
| 739 | ||
| 740 | let kill = KILL(file_name, crossing, null, p, is_presence, true) | |
| 741 | ||
| 742 | kill.narrowed_type = _current_env.narrowed_type_of_path(p) | |
| 743 | ||
| 744 | _current_env.drop_path(p) | |
| 745 | ||
| 746 | KILL_LEDGER.record(kill) | |
| 747 | od | |
| 748 | ||
| 749 | _report_kills_at(crossing, details) | |
| 750 | si | |
| 751 | ||
| 752 | // One sigil per call site however many facts die there. | |
| 753 | _report_kills_at(crossing: CROSSING, details: Collections.List[string]) is | |
| 754 | if details.count == 0 \/ !_logger.want_hint_for(crossing.location) then | |
| 755 | return | |
| 756 | fi | |
| 757 | ||
| 758 | let callee = crossing.callee | |
| 759 | let reason = if callee? then "the call to '{callee.name}()' may change it" else "a call here may change it" fi | |
| 760 | ||
| 761 | if details.count == 1 then | |
| 762 | _logger.inlay(crossing.location, "narrowing-killed", "◄", "{details[0]}\n\n{reason}") | |
| 763 | return | |
| 764 | fi | |
| 765 | ||
| 766 | let out = System.Text.StringBuilder(if callee? then "the call to '{callee.name}()' may change:" else "a call here may change:" fi) | |
| 767 | ||
| 768 | for detail in details do | |
| 769 | out.append("\n ") | |
| 770 | out.append(detail) | |
| 771 | od | |
| 772 | ||
| 773 | _logger.inlay(crossing.location, "narrowing-killed", "◄", out.to_string()) | |
| 774 | si | |
| 775 | // fact alone; the report adds the wording, because several | |
| 776 | // facts can share one call site and it renders them together. | |
| 777 | ||
| 778 | // Position marker into the call-crossing log, paired with the | |
| 779 | // adopt_crossings_* methods below: an environment derived | |
| 780 | // from a snapshot never saw the calls walked after the | |
| 781 | // snapshot was taken, so their crossings are attached to its | |
| 782 | // heap facts before it comes into force. This replaces the | |
| 783 | // epoch drop for calls; direct stores still bump the epoch, | |
| 784 | // and snapshot consumers still drop everything on it. | |
| 785 | crossing_mark: int => _crossing_log.count | |
| 786 | ||
| 787 | // Record the log position at which a condition-leaf test | |
| 788 | // expression compiles. Called as the leaf's node is walked; | |
| 789 | // the first stamp wins (see `_test_site_marks`). | |
| 790 | note_test_site(expr: Trees.Expressions.Expression) is | |
| 791 | if !_test_site_marks.contains_key(expr) then | |
| 792 | _test_site_marks[expr] = _crossing_log.count | |
| 793 | fi | |
| 794 | si | |
| 795 | ||
| 796 | // The log position a leaf test was first walked at, or null | |
| 797 | // when no walk stamped it. | |
| 798 | test_site_mark_of(expr: Trees.Expressions.Expression) -> int? is | |
| 799 | let mark mut = 0 | |
| 800 | ||
| 801 | if _test_site_marks.try_get_value(expr, mark ref) then | |
| 802 | return mark | |
| 803 | fi | |
| 804 | ||
| 805 | return null | |
| 806 | si | |
| 807 | ||
| 808 | adopt_crossings_since(env: NARROW_ENV, mark: int) is | |
| 809 | adopt_crossings_between(env, mark, _crossing_log.count) | |
| 810 | si | |
| 811 | ||
| 812 | adopt_crossings_between(env: NARROW_ENV, from_mark: int, to_mark: int) is | |
| 813 | for i in from_mark..to_mark do | |
| 814 | env.note_crossing_at(_crossing_log[i], i) | |
| 815 | od | |
| 816 | si | |
| 817 | ||
| 818 | // Emit a kill hint for each tracked path about to be dropped, | |
| 819 | // deduplicating a path carrying both a narrow and a presence | |
| 820 | // fact. When `getter_only`, restricts to getter-bearing paths — | |
| 821 | // the subset a heap store discards. Gated once on the call | |
| 822 | // location so the set is not built during a normal compile. | |
| 823 | _report_dropped_paths(location: LOCATION, reason: string, getter_only: bool) is | |
| 824 | if !_logger.want_hint_for(location) then | |
| 825 | return | |
| 826 | fi | |
| 827 | ||
| 828 | let doomed = Collections.SET[ACCESS_PATH]() | |
| 829 | ||
| 830 | for p in _current_env.narrowed_paths do | |
| 831 | if !getter_only \/ p.has_getter_hop then | |
| 832 | doomed.add(p) | |
| 833 | fi | |
| 834 | od | |
| 835 | ||
| 836 | for p in _current_env.non_null_paths do | |
| 837 | if !getter_only \/ p.has_getter_hop then | |
| 838 | doomed.add(p) | |
| 839 | fi | |
| 840 | od | |
| 841 | ||
| 842 | for p in doomed do | |
| 843 | _report_path_kill(p, location, reason) | |
| 844 | od | |
| 845 | si | |
| 846 | ||
| 847 | // Heap-store transfer: a direct store — to a field, a | |
| 848 | // property, an index or any member path — can change what any | |
| 849 | // property getter returns, so property facts cannot survive | |
| 850 | // it. Field facts do: a store to one field cannot alter | |
| 851 | // another field, and a store to the narrowed field itself is | |
| 852 | // handled by the assignment transfer. Local facts are | |
| 853 | // unaffected. | |
| 854 | on_heap_store(location: LOCATION) is | |
| 855 | _drop_property_facts(location, "a store here may change it") | |
| 856 | si | |
| 857 | ||
| 858 | // ==== kill ledger records ==== | |
| 859 | // | |
| 860 | // A use that leans on a heap fact — a load compiled at the | |
| 861 | // narrowed type, or an optional read compiled as present — is | |
| 862 | // checked against the fact's crossings. Every crossing must | |
| 863 | // be discharged: the callee provably left the fact alone. | |
| 864 | // Anything less is an error at the use site: the value may | |
| 865 | // have changed since the fact was proven, and the emitted | |
| 866 | // code would trust a stale view. The remedy at the use site is | |
| 867 | // to re-establish — test again, unwrap with `!`, or copy to a | |
| 868 | // local before the call. | |
| 869 | ||
| 870 | // A crossing is discharged when the callee provably left the | |
| 871 | // fact alone: a store-free callee writes nothing at all; a | |
| 872 | // receiver-interior callee writes only its own receiver's | |
| 873 | // BCL-internal state, which no field is, so it leaves field | |
| 874 | // facts alone but can change what a getter reads. | |
| 875 | _crossing_discharged(crossing: CROSSING, reads_through_getter: bool) -> bool is | |
| 876 | let callee = crossing.callee | |
| 877 | ||
| 878 | return | |
| 879 | callee? /\ | |
| 880 | (callee.is_store_free \/ | |
| 881 | (!reads_through_getter /\ callee.writes_only_receiver_interior)) | |
| 882 | si | |
| 883 | ||
| 884 | _first_undischarged( | |
| 885 | crossings: Collections.LIST[CROSSING]?, | |
| 886 | reads_through_getter: bool | |
| 887 | ) -> CROSSING? is | |
| 888 | if !crossings? then | |
| 889 | return null | |
| 890 | fi | |
| 891 | ||
| 892 | for c in crossings do | |
| 893 | if !_crossing_discharged(c, reads_through_getter) then | |
| 894 | return c | |
| 895 | fi | |
| 896 | od | |
| 897 | ||
| 898 | return null | |
| 899 | si | |
| 900 | ||
| 901 | // The crossings the inline filter cannot discharge, snapshot | |
| 902 | // so later mutation of the fact's own list cannot reach a | |
| 903 | // pending event. Null when every crossing is discharged. | |
| 904 | _undischarged_crossings( | |
| 905 | crossings: Collections.LIST[CROSSING]?, | |
| 906 | reads_through_getter: bool | |
| 907 | ) -> Collections.LIST[CROSSING]? is | |
| 908 | if !crossings? then | |
| 909 | return null | |
| 910 | fi | |
| 911 | ||
| 912 | let kept: Collections.LIST[CROSSING]? mut = null | |
| 913 | ||
| 914 | for c in crossings do | |
| 915 | if !_crossing_discharged(c, reads_through_getter) then | |
| 916 | if !kept? then | |
| 917 | kept = Collections.LIST[CROSSING]() | |
| 918 | fi | |
| 919 | ||
| 920 | kept.add(c) | |
| 921 | fi | |
| 922 | od | |
| 923 | ||
| 924 | return kept | |
| 925 | si | |
| 926 | ||
| 927 | // Record a heap-fact load of `v` for the kill ledger. Locals are | |
| 928 | // filtered here - their facts take no crossings - except one a | |
| 929 | // closure body assigns, which lives in a shared heap cell and is | |
| 930 | // recorded exactly as a field is. | |
| 931 | record_load_of_symbol(location: LOCATION, v: Symbol) is | |
| 932 | if !isa Semantic.Symbols.Field(v) /\ !isa Semantic.Symbols.Property(v) /\ !NARROW_ENV.is_closure_assigned(v) then | |
| 933 | return | |
| 934 | fi | |
| 935 | ||
| 936 | let getter = isa Semantic.Symbols.Property(v) | |
| 937 | let narrow_in_force = _current_env.contains(v) | |
| 938 | let presence_in_force = _current_env.is_non_null(v) | |
| 939 | ||
| 940 | if !narrow_in_force /\ !presence_in_force then | |
| 941 | return | |
| 942 | fi | |
| 943 | ||
| 944 | _record_load( | |
| 945 | location, | |
| 946 | v, | |
| 947 | null, | |
| 948 | narrow_in_force, | |
| 949 | presence_in_force, | |
| 950 | if narrow_in_force then _undischarged_crossings(_current_env.narrow_crossings_of(v), getter) else null fi, | |
| 951 | if presence_in_force then _undischarged_crossings(_current_env.non_null_crossings_of(v), getter) else null fi) | |
| 952 | si | |
| 953 | // The same, for a member-access path: a path fact is recorded | |
| 954 | // with the crossings it was kept across and, for each getter | |
| 955 | // hop, the hop's own call. | |
| 956 | ||
| 957 | record_load_of_path(location: LOCATION, path: ACCESS_PATH) is | |
| 958 | let getter = path.has_getter_hop | |
| 959 | let narrow_in_force = _current_env.narrowed_type_of_path(path)? | |
| 960 | let presence_in_force = _current_env.is_non_null_path(path) | |
| 961 | ||
| 962 | if !narrow_in_force /\ !presence_in_force then | |
| 963 | return | |
| 964 | fi | |
| 965 | ||
| 966 | _record_load( | |
| 967 | location, | |
| 968 | null, | |
| 969 | path, | |
| 970 | narrow_in_force, | |
| 971 | presence_in_force, | |
| 972 | if narrow_in_force then _undischarged_crossings(_current_env.path_narrow_crossings_of(path), getter) else null fi, | |
| 973 | if presence_in_force then _undischarged_crossings(_current_env.path_presence_crossings_of(path), getter) else null fi) | |
| 974 | si | |
| 975 | ||
| 976 | ||
| 977 | // The ledger's record of a load through a fact: every crossing | |
| 978 | // the fact was kept across, and the getter's own call for a | |
| 979 | // fact read through a getter the inline tiers cannot prove. | |
| 980 | // Each is the walk's decision to keep the fact, re-asked of | |
| 981 | // the relations after the next solve. See KILL_LEDGER. | |
| 982 | _record_load( | |
| 983 | location: LOCATION, | |
| 984 | target: Symbol?, | |
| 985 | path: ACCESS_PATH?, | |
| 986 | narrow_in_force: bool, | |
| 987 | presence_in_force: bool, | |
| 988 | narrow_crossings: Collections.LIST[CROSSING]?, | |
| 989 | presence_crossings: Collections.LIST[CROSSING]? | |
| 990 | ) is | |
| 991 | ||
| 992 | let file_name = location.file_name | |
| 993 | ||
| 994 | if narrow_crossings? then | |
| 995 | for c in narrow_crossings do | |
| 996 | KILL_LEDGER.record(KILL(file_name, c, target, path, false, false)) | |
| 997 | od | |
| 998 | fi | |
| 999 | ||
| 1000 | if presence_crossings? then | |
| 1001 | for c in presence_crossings do | |
| 1002 | KILL_LEDGER.record(KILL(file_name, c, target, path, true, false)) | |
| 1003 | od | |
| 1004 | fi | |
| 1005 | ||
| 1006 | for is_presence in [presence_in_force, !narrow_in_force] do | |
| 1007 | if is_presence /\ !presence_in_force then | |
| 1008 | continue | |
| 1009 | fi | |
| 1010 | ||
| 1011 | if !is_presence /\ !narrow_in_force then | |
| 1012 | continue | |
| 1013 | fi | |
| 1014 | ||
| 1015 | // Every getter the fact reads through is a crossing of | |
| 1016 | // its own, kept here; the re-ask after a solve decides | |
| 1017 | // whether it backs the fact. | |
| 1018 | for hop in _getter_hops(target, path) do | |
| 1019 | if let read = hop.read_function then | |
| 1020 | KILL_LEDGER.record(KILL(file_name, CROSSING(hop.location, read), target, path, is_presence, false)) | |
| 1021 | fi | |
| 1022 | od | |
| 1023 | od | |
| 1024 | si | |
| 1025 | ||
| 1026 | ||
| 1027 | _getter_hops(target: Symbol?, path: ACCESS_PATH?) -> Collections.LIST[Semantic.Symbols.Property] is | |
| 1028 | let result = Collections.LIST[Semantic.Symbols.Property]() | |
| 1029 | ||
| 1030 | if let property: Semantic.Symbols.Property = target then | |
| 1031 | result.add(property) | |
| 1032 | fi | |
| 1033 | ||
| 1034 | if path? then | |
| 1035 | if let property: Semantic.Symbols.Property = path.root then | |
| 1036 | result.add(property) | |
| 1037 | fi | |
| 1038 | ||
| 1039 | for m in path.members do | |
| 1040 | if let property: Semantic.Symbols.Property = m then | |
| 1041 | result.add(property) | |
| 1042 | fi | |
| 1043 | od | |
| 1044 | fi | |
| 1045 | ||
| 1046 | return result | |
| 1047 | si | |
| 1048 | ||
| 1049 | ||
| 1050 | ||
| 1051 | // Whether the fact-formation tier proves the getter a fact | |
| 1052 | // reads through - the same Property.narrowable_getter rule | |
| 1053 | // the formation gates apply, so with the gates in place this | |
| 1054 | // never fails. It is kept as a safety net: should a fact ever | |
| 1055 | // arrive through a getter the tier no longer proves (a stale | |
| 1056 | // incremental state, a future gate change), the use records | |
| 1057 | // an obligation for the deferred judge instead of silently | |
| 1058 | // leaning on the getter. | |
| 1059 | _getter_proven_inline(m: Symbol) -> bool is | |
| 1060 | if !isa Semantic.Symbols.Property(m) then | |
| 1061 | return true | |
| 1062 | fi | |
| 1063 | ||
| 1064 | return (cast Semantic.Symbols.Property(m)).narrowable_getter | |
| 1065 | si | |
| 1066 | ||
| 1067 | _path_getters_proven_inline(path: ACCESS_PATH) -> bool is | |
| 1068 | if !_getter_proven_inline(path.root) then | |
| 1069 | return false | |
| 1070 | fi | |
| 1071 | ||
| 1072 | for m in path.members do | |
| 1073 | if !_getter_proven_inline(m) then | |
| 1074 | return false | |
| 1075 | fi | |
| 1076 | od | |
| 1077 | ||
| 1078 | return true | |
| 1079 | si | |
| 1080 | ||
| 1081 | ||
| 1082 | ||
| 1083 | ||
| 1084 | ||
| 1085 | ||
| 1086 | ||
| 1087 | ||
| 1088 | // Whether every crossing recorded against `v`'s facts is | |
| 1089 | // discharged. Gates the redundancy warnings: an `!` or a | |
| 1090 | // re-test after an undischarged crossing is load-bearing — | |
| 1091 | // it is the remedy the reliance error asks for — and must not | |
| 1092 | // be reported redundant. | |
| 1093 | symbol_fact_validated(v: Symbol) -> bool is | |
| 1094 | // A plain local's facts take no crossings, so they are | |
| 1095 | // always validated; one a closure body assigns is a heap | |
| 1096 | // fact and owes its crossings like a field does. | |
| 1097 | if | |
| 1098 | !isa Semantic.Symbols.Field(v) /\ | |
| 1099 | !isa Semantic.Symbols.Property(v) /\ | |
| 1100 | !NARROW_ENV.is_closure_assigned(v) | |
| 1101 | then | |
| 1102 | return true | |
| 1103 | fi | |
| 1104 | ||
| 1105 | let getter = isa Semantic.Symbols.Property(v) | |
| 1106 | ||
| 1107 | return | |
| 1108 | _getter_proven_inline(v) /\ | |
| 1109 | !_first_undischarged(_current_env.non_null_crossings_of(v), getter)? /\ | |
| 1110 | !_first_undischarged(_current_env.narrow_crossings_of(v), getter)? | |
| 1111 | si | |
| 1112 | ||
| 1113 | path_fact_validated(path: ACCESS_PATH) -> bool => | |
| 1114 | _path_getters_proven_inline(path) /\ | |
| 1115 | !_first_undischarged(_current_env.path_presence_crossings_of(path), path.has_getter_hop)? /\ | |
| 1116 | !_first_undischarged(_current_env.path_narrow_crossings_of(path), path.has_getter_hop)? | |
| 1117 | ||
| 1118 | _drop_property_facts(location: LOCATION, reason: string) is | |
| 1119 | _heap_epoch = _heap_epoch + 1 | |
| 1120 | _mark_literal_impure() | |
| 1121 | ||
| 1122 | let stale = Collections.SET[Symbol]() | |
| 1123 | ||
| 1124 | for v in _current_env.variables do | |
| 1125 | if isa Semantic.Symbols.Property(v) then | |
| 1126 | stale.add(v) | |
| 1127 | fi | |
| 1128 | od | |
| 1129 | ||
| 1130 | for v in _current_env.non_null_variables do | |
| 1131 | if isa Semantic.Symbols.Property(v) then | |
| 1132 | stale.add(v) | |
| 1133 | fi | |
| 1134 | od | |
| 1135 | ||
| 1136 | for v in stale do | |
| 1137 | _report_kill(v, location, reason) | |
| 1138 | forget(v) | |
| 1139 | od | |
| 1140 | ||
| 1141 | _report_dropped_paths(location, reason, true) | |
| 1142 | _current_env.drop_getter_paths() | |
| 1143 | si | |
| 1144 | ||
| 1145 | // Member-store transfer: a store through `receiver.member` | |
| 1146 | // invalidates the member's own facts and every path reading | |
| 1147 | // through it. Keyed on the member symbol, not the receiver — | |
| 1148 | // the written receiver may alias whatever receiver a fact was | |
| 1149 | // established on, so `other.f = e` must invalidate a fact | |
| 1150 | // proven on `self`'s bare `f` just as `f = e` would. | |
| 1151 | on_member_store(member: Symbol?) is | |
| 1152 | if !member? then | |
| 1153 | return | |
| 1154 | fi | |
| 1155 | ||
| 1156 | _heap_epoch = _heap_epoch + 1 | |
| 1157 | _mark_literal_impure() | |
| 1158 | ||
| 1159 | forget(member) | |
| 1160 | ||
| 1161 | _current_env.drop_paths_rooted_at(member) | |
| 1162 | _current_env.drop_paths_through(member) | |
| 1163 | si | |
| 1164 | ||
| 1165 | // Drop a single field's narrow + presence facts — the call | |
| 1166 | // transfer applied to one variable. | |
| 1167 | forget(v: Symbol) is | |
| 1168 | if _current_env.contains(v) then | |
| 1169 | _current_env.drop_narrow(v) | |
| 1170 | ||
| 1171 | let declared = declared_type_of(v) | |
| 1172 | ||
| 1173 | if declared? then | |
| 1174 | _set_symbol_type(v, declared) | |
| 1175 | fi | |
| 1176 | fi | |
| 1177 | ||
| 1178 | _current_env.drop_non_null(v) | |
| 1179 | si | |
| 1180 | ||
| 1181 | // Exempt `v` from the call transfer until its frame is released. | |
| 1182 | // See RECEIVER_SHIELD.push. | |
| 1183 | push_shield(v: Symbol?) -> SHIELD_FRAME? => _shield.push(v) | |
| 1184 | ||
| 1185 | // Release a frame from `push_shield`, returning whether a call | |
| 1186 | // dropped the receiver. See RECEIVER_SHIELD.release. | |
| 1187 | release_shield(frame: SHIELD_FRAME?) -> bool => _shield.release(frame) | |
| 1188 | ||
| 1189 | // Register `v` as a deferred-init local subject to the | |
| 1190 | // definite-assignment use-before-assignment check. | |
| 1191 | track_deferred(v: Symbol) is | |
| 1192 | _tracked.add(v) | |
| 1193 | si | |
| 1194 | ||
| 1195 | // True iff `v` is a tracked deferred-init local. | |
| 1196 | is_tracked(v: Symbol) -> bool => _tracked.contains(v) | |
| 1197 | ||
| 1198 | // True iff `v` is definitely assigned at the current point. | |
| 1199 | is_assigned(v: Symbol) -> bool => _current_env.is_assigned(v) | |
| 1200 | ||
| 1201 | // Record `v` as definitely assigned at the current point. | |
| 1202 | mark_assigned(v: Symbol) is | |
| 1203 | _current_env.set_assigned(v) | |
| 1204 | si | |
| 1205 | ||
| 1206 | // Record a method of the enclosing type as called on every path | |
| 1207 | // reaching here, and read the set back at the end of a body. | |
| 1208 | mark_called(f: Symbol) is | |
| 1209 | _current_env.set_called(f) | |
| 1210 | si | |
| 1211 | ||
| 1212 | called_methods: Collections.Iterable[Symbol] => _current_env.called_methods | |
| 1213 | ||
| 1214 | // The symbols definitely assigned at the current point. | |
| 1215 | assigned_variables: Collections.Iterable[Symbol] => _current_env.assigned_variables | |
| 1216 | ||
| 1217 | // True iff `v` is known to hold a value at the current point. | |
| 1218 | is_non_null(v: Symbol) -> bool => _current_env.is_non_null(v) | |
| 1219 | ||
| 1220 | // Record `v` as known to hold a value at the current point — | |
| 1221 | // used by the `x!` (unwrap) transfer. | |
| 1222 | mark_non_null(v: Symbol) is | |
| 1223 | _current_env.creation_mark = crossing_mark | |
| 1224 | _current_env.set_non_null(v) | |
| 1225 | si | |
| 1226 | ||
| 1227 | // Editor-only narrowing-introduction hint emitted at a site | |
| 1228 | // outside the condition analyzer (unwrap `x!`, non-optional | |
| 1229 | // initializer / assignment). Same open-files gating as | |
| 1230 | // `_report_kill`; each caller supplies its own slug so the | |
| 1231 | // editor can suppress it independently. `detail` carries only the | |
| 1232 | // narrowed-to type; NARROWING_INLAY_MERGER builds the hover text. | |
| 1233 | report_narrowing_site(location: LOCATION, code: string, label: string, detail: string) is | |
| 1234 | if !_logger.want_hint_for(location) then | |
| 1235 | return | |
| 1236 | fi | |
| 1237 | ||
| 1238 | _logger.inlay(location, code, label, detail) | |
| 1239 | si | |
| 1240 | ||
| 1241 | // True iff the member-access `path` is known to hold a value | |
| 1242 | // at the current point — consulted at member-load sites to | |
| 1243 | // narrow the access optional -> non-optional. | |
| 1244 | is_non_null_path(path: ACCESS_PATH?) -> bool => path? /\ _current_env.is_non_null_path(path) | |
| 1245 | ||
| 1246 | // The type recorded for `path` at the current point, or null | |
| 1247 | // when none — consulted at member-load sites to narrow the | |
| 1248 | // access to its recorded static subtype. | |
| 1249 | narrowed_type_of_path(path: ACCESS_PATH?) -> Type? => | |
| 1250 | if path? then _current_env.narrowed_type_of_path(path) else null fi | |
| 1251 | ||
| 1252 | // Compose a loaded type with the recorded path narrow into a | |
| 1253 | // sound view type, or null when the narrow cannot be applied. | |
| 1254 | // The rules mirror `_apply_one` for symbol narrowing: | |
| 1255 | // - reject error / inferred targets | |
| 1256 | // - strict-subtype narrow -> target | |
| 1257 | // - sibling / class+trait -> INTERSECTION(loaded, target) | |
| 1258 | // - reject supertype broadening | |
| 1259 | // Returns null when the composed view equals the loaded type | |
| 1260 | // itself, so callers can skip the wrap in that case. | |
| 1261 | compose_path_narrow(loaded: Type?, target: Type?) -> Type? is | |
| 1262 | if !loaded? \/ !target? then | |
| 1263 | return null | |
| 1264 | fi | |
| 1265 | ||
| 1266 | if target.is_error \/ target.is_inferred then | |
| 1267 | return null | |
| 1268 | fi | |
| 1269 | ||
| 1270 | let effective_target: Type mut = target | |
| 1271 | ||
| 1272 | if !loaded.is_optional /\ target.is_optional then | |
| 1273 | let stripped = target.as_non_optional() | |
| 1274 | effective_target = stripped | |
| 1275 | fi | |
| 1276 | ||
| 1277 | if loaded.matches(effective_target) then | |
| 1278 | return null | |
| 1279 | fi | |
| 1280 | ||
| 1281 | // A bounded type variable narrows through its bound, the same | |
| 1282 | // way `_apply_one` and member access resolve through it. | |
| 1283 | let loaded_effective = | |
| 1284 | if let bound = loaded.bound_type then bound else loaded fi | |
| 1285 | ||
| 1286 | if loaded_effective.is_assignable_from(effective_target) then | |
| 1287 | return _keep_type_variable(loaded, effective_target) | |
| 1288 | fi | |
| 1289 | ||
| 1290 | let both_reference = !loaded_effective.is_value_type /\ !effective_target.is_value_type | |
| 1291 | let loaded_supertypes_target = effective_target.is_assignable_from(loaded_effective) | |
| 1292 | ||
| 1293 | if !both_reference \/ loaded_supertypes_target then | |
| 1294 | return null | |
| 1295 | fi | |
| 1296 | ||
| 1297 | let composed = INTERSECTION.try_create(loaded_effective, effective_target) | |
| 1298 | ||
| 1299 | if !composed? \/ composed.matches(loaded_effective) then | |
| 1300 | return null | |
| 1301 | fi | |
| 1302 | ||
| 1303 | return composed | |
| 1304 | si | |
| 1305 | ||
| 1306 | // A type variable is peeled to its bound when a narrow is | |
| 1307 | // judged, because that is what the value can be at runtime. | |
| 1308 | // The value is still a `T`, though, so the narrowed view has | |
| 1309 | // to say so: `T & TARGET` keeps it assignable back to `T` and | |
| 1310 | // lets member lookup see both sides. The variable is read off | |
| 1311 | // the current view rather than tested for directly, so a | |
| 1312 | // second narrow of an already-composed view keeps it too. | |
| 1313 | // Composing can fail when the two carry unrelated concrete | |
| 1314 | // identities, which on this edge means the test can never | |
| 1315 | // succeed - fall back to the target alone rather than | |
| 1316 | // declining the narrow. | |
| 1317 | _keep_type_variable(current: Type, target: Type) -> Type static is | |
| 1318 | let variable = current.type_variable_side | |
| 1319 | ||
| 1320 | if !variable? \/ variable.matches(target) then | |
| 1321 | return target | |
| 1322 | fi | |
| 1323 | ||
| 1324 | let composed = INTERSECTION.try_create(variable, target) | |
| 1325 | ||
| 1326 | if !composed? then | |
| 1327 | return target | |
| 1328 | fi | |
| 1329 | ||
| 1330 | return composed | |
| 1331 | si | |
| 1332 | ||
| 1333 | // Apply one narrow if it is sound. Two cases: | |
| 1334 | // | |
| 1335 | // - Strict-subtype narrow: `t` is a static subtype of v's | |
| 1336 | // declared type. Narrow v.type to t directly. | |
| 1337 | // | |
| 1338 | // - Sibling/class+trait narrow: neither t nor declared | |
| 1339 | // subtypes the other, both are reference types. The | |
| 1340 | // runtime `isa` check guarantees the value satisfies | |
| 1341 | // both — narrow v.type to an INTERSECTION of declared | |
| 1342 | // and t so subsequent member lookups can see both | |
| 1343 | // sides. (For pure trait→trait or class→trait | |
| 1344 | // narrowings the user's earlier "drops the declared | |
| 1345 | // side" trade-off becomes a non-issue.) | |
| 1346 | // | |
| 1347 | // Supertype broadening is still rejected — narrowing must | |
| 1348 | // be sound and informative; widening declared → t where t | |
| 1349 | // supertypes declared would lose information. | |
| 1350 | // | |
| 1351 | // Captures the declared type on first narrow. Returns true | |
| 1352 | // when the narrow was applied. | |
| 1353 | _apply_one(v: Symbol, t: Type) -> bool is | |
| 1354 | if !v.type? then | |
| 1355 | return false | |
| 1356 | fi | |
| 1357 | ||
| 1358 | if t.is_error \/ t.is_inferred then | |
| 1359 | return false | |
| 1360 | fi | |
| 1361 | ||
| 1362 | let current = v.type! | |
| 1363 | let declared = declared_type_of(v) | |
| 1364 | ||
| 1365 | // Strict non-nullable-by-default: a non-optional slot | |
| 1366 | // can't be narrowed to an optional type. If `current` | |
| 1367 | // is already non-optional (the if-X? check has fired) | |
| 1368 | // and the narrowing target is optional, strip the | |
| 1369 | // optional layer — the narrow is from a non-null value | |
| 1370 | // to a more specific type, never re-introducing | |
| 1371 | // optionality. | |
| 1372 | let target: Type mut = t | |
| 1373 | if !current.is_optional /\ target.is_optional then | |
| 1374 | let stripped = target.as_non_optional() | |
| 1375 | target = stripped | |
| 1376 | fi | |
| 1377 | ||
| 1378 | if !declared? \/ current.matches(target) then | |
| 1379 | return false | |
| 1380 | fi | |
| 1381 | ||
| 1382 | // A bounded type variable narrows through its bound: a value | |
| 1383 | // of `T: List[E]` can be a `CONS[E]` at runtime even though | |
| 1384 | // `CONS[E]` subtypes the bound, not `T` itself. Evaluate the | |
| 1385 | // narrow against the bound (what `T` is), not the variable. | |
| 1386 | // The narrowed view stays a valid subtype; IL loads it against | |
| 1387 | // the variable's declared `!!N` with a checked cast. | |
| 1388 | let current_effective = | |
| 1389 | if let bound = current.bound_type then bound else current fi | |
| 1390 | ||
| 1391 | let narrowed: Type? mut = null | |
| 1392 | ||
| 1393 | if current_effective.is_assignable_from(target) then | |
| 1394 | // Strict-subtype narrow: target is a static subtype of | |
| 1395 | // the current (possibly already-narrowed) type. When the | |
| 1396 | // narrow was judged against a type variable's bound, the | |
| 1397 | // variable itself is still what the value is, so keep it | |
| 1398 | // alongside the target rather than replacing it. | |
| 1399 | narrowed = _keep_type_variable(current, target) | |
| 1400 | else | |
| 1401 | // Sibling / class+trait relaxation: extend current | |
| 1402 | // with target. Factory drops redundant supertypes and | |
| 1403 | // collapses to a plain type if a single survivor | |
| 1404 | // remains. Composes correctly with an already- | |
| 1405 | // narrowed intersection — adding a second trait | |
| 1406 | // produces a three-element intersection rather | |
| 1407 | // than replacing. | |
| 1408 | let both_reference = !current_effective.is_value_type /\ !target.is_value_type | |
| 1409 | let current_supertypes_t = target.is_assignable_from(current_effective) | |
| 1410 | ||
| 1411 | if !both_reference \/ current_supertypes_t then | |
| 1412 | return false | |
| 1413 | fi | |
| 1414 | ||
| 1415 | narrowed = INTERSECTION.try_create(current_effective, target) | |
| 1416 | ||
| 1417 | if !narrowed? then | |
| 1418 | // Unrelated concrete identities — no value can be | |
| 1419 | // both, so there is no narrowed view to apply. | |
| 1420 | return false | |
| 1421 | fi | |
| 1422 | ||
| 1423 | if narrowed.matches(current) then | |
| 1424 | return false | |
| 1425 | fi | |
| 1426 | fi | |
| 1427 | ||
| 1428 | if !_declared.contains_key(v) then | |
| 1429 | _declared[v] = current | |
| 1430 | fi | |
| 1431 | ||
| 1432 | _set_symbol_type(v, narrowed) | |
| 1433 | ||
| 1434 | return true | |
| 1435 | si | |
| 1436 | si | |
| 1437 | ||
| 1438 | // RAII narrowing-env speculation, mirroring the logger's | |
| 1439 | // LOGGER_SPECULATE_THEN_* disposables. Construct to snapshot the | |
| 1440 | // current env as a baseline; a retry re-walk resets to it through | |
| 1441 | // `_flow.restore()`; on scope exit COMMIT keeps the walked facts, | |
| 1442 | // ROLL_BACK discards them. Pair the flow disposable with the logger | |
| 1443 | // disposable at any site that speculatively re-walks expressions, so | |
| 1444 | // the narrowing facts and the diagnostics roll back together. | |
| 1445 | struct FLOW_SPECULATE_THEN_COMMIT: Disposable is | |
| 1446 | _flow: NARROWING_FLOW? | |
| 1447 | ||
| 1448 | init(flow: NARROWING_FLOW) is | |
| 1449 | _flow = flow | |
| 1450 | flow.speculate() | |
| 1451 | si | |
| 1452 | ||
| 1453 | commit() is | |
| 1454 | _flow!.commit() | |
| 1455 | _flow = null | |
| 1456 | si | |
| 1457 | ||
| 1458 | cancel() is | |
| 1459 | _flow = null | |
| 1460 | si | |
| 1461 | ||
| 1462 | dispose() is | |
| 1463 | if _flow? then | |
| 1464 | _flow.commit() | |
| 1465 | _flow = null | |
| 1466 | fi | |
| 1467 | si | |
| 1468 | si | |
| 1469 | ||
| 1470 | struct FLOW_SPECULATE_THEN_ROLL_BACK: Disposable is | |
| 1471 | _flow: NARROWING_FLOW? | |
| 1472 | ||
| 1473 | init(flow: NARROWING_FLOW) is | |
| 1474 | _flow = flow | |
| 1475 | flow.speculate() | |
| 1476 | si | |
| 1477 | ||
| 1478 | roll_back() is | |
| 1479 | _flow!.roll_back() | |
| 1480 | _flow = null | |
| 1481 | si | |
| 1482 | ||
| 1483 | cancel() is | |
| 1484 | _flow = null | |
| 1485 | si | |
| 1486 | ||
| 1487 | dispose() is | |
| 1488 | if _flow? then | |
| 1489 | _flow.roll_back() | |
| 1490 | _flow = null | |
| 1491 | fi | |
| 1492 | si | |
| 1493 | si | |
| 1494 | si |