Appearance
| 1 | namespace Syntax.Process is | |
| 2 | use Logging | |
| 3 | ||
| 4 | use Source.LOCATION | |
| 5 | use Function = Semantic.Symbols.Function | |
| 6 | ||
| 7 | // One value that reached a pure function-typed slot, held until | |
| 8 | // the effect relations can say whether it is store-free. | |
| 9 | // `slot_index` is the argument's position for a call record and | |
| 10 | // -1 for a store: several arguments of one call can fall back to | |
| 11 | // the same reported location, and the index is what keeps their | |
| 12 | // records distinct. | |
| 13 | // | |
| 14 | // The two carry different slugs because they are worth different | |
| 15 | // things. A store is what makes the slot's claim true, and is | |
| 16 | // trusted wherever the slot is read; an argument's own call is | |
| 17 | // judged on its callee regardless, so the report there is advice | |
| 18 | // rather than the thing soundness rests on. | |
| 19 | class PURE_SLOT_RECORD( | |
| 20 | location: LOCATION, | |
| 21 | slot_index: int, | |
| 22 | value: IR.Values.Value?, | |
| 23 | slug: string, | |
| 24 | message: string | |
| 25 | ) | |
| 26 | ||
| 27 | // Values that reached a pure function-typed slot, recorded while | |
| 28 | // expressions compile and judged once the effect relations are | |
| 29 | // solved. | |
| 30 | // | |
| 31 | // Deferred because a body's own store-freedom is not known until | |
| 32 | // then: the answer available before expressions are compiled | |
| 33 | // cannot see the types most receivers are reached through, so it | |
| 34 | // gives up on bodies that write nothing. | |
| 35 | // | |
| 36 | // Held per file and dropped exactly where a file's other | |
| 37 | // expression-level output is, so an analysis-mode recompile of one | |
| 38 | // file re-records rather than reporting twice. Speculative walks | |
| 39 | // are mirrored from the flow: a rolled-back walk's records are | |
| 40 | // truncated, so an attempt that was scrubbed from the diagnostics | |
| 41 | // does not report. | |
| 42 | class PURE_SLOTS is | |
| 43 | _records: Collections.MAP[string, Collections.LIST[PURE_SLOT_RECORD]] static | |
| 44 | _marks: Collections.LIST[Collections.MAP[string, int]] static | |
| 45 | ||
| 46 | init() static is | |
| 47 | _records = Collections.MAP[string, Collections.LIST[PURE_SLOT_RECORD]]() | |
| 48 | _marks = Collections.LIST[Collections.MAP[string, int]]() | |
| 49 | si | |
| 50 | ||
| 51 | note(record: PURE_SLOT_RECORD) static is | |
| 52 | let path = record.location.file_name | |
| 53 | ||
| 54 | if !_records.contains_key(path) then | |
| 55 | _records[path] = Collections.LIST[PURE_SLOT_RECORD]() | |
| 56 | fi | |
| 57 | ||
| 58 | _records[path].add(record) | |
| 59 | si | |
| 60 | ||
| 61 | clear_for(path: string) static is | |
| 62 | _records.remove(path) | |
| 63 | si | |
| 64 | ||
| 65 | clear_within(path: string, span: LOCATION) static is | |
| 66 | let entries: Collections.LIST[PURE_SLOT_RECORD] mut | |
| 67 | ||
| 68 | if _records.try_get_value(path, entries ref) then | |
| 69 | let kept = Collections.LIST[PURE_SLOT_RECORD]() | |
| 70 | ||
| 71 | for c in entries do | |
| 72 | if !span.contains(c.location) then | |
| 73 | kept.add(c) | |
| 74 | fi | |
| 75 | od | |
| 76 | ||
| 77 | _records[path] = kept | |
| 78 | fi | |
| 79 | si | |
| 80 | ||
| 81 | clear() static is | |
| 82 | _records.clear() | |
| 83 | _marks.clear() | |
| 84 | si | |
| 85 | ||
| 86 | // Speculation, mirrored from NARROWING_FLOW: a record made | |
| 87 | // inside a walk that is rolled back would otherwise survive the | |
| 88 | // scrubbing of that walk's diagnostics. The mark snapshots each | |
| 89 | // file list's length, so a rollback trims every list back to | |
| 90 | // exactly its own length at the mark and touches nothing | |
| 91 | // recorded before it. | |
| 92 | speculate() static is | |
| 93 | let snapshot = Collections.MAP[string, int]() | |
| 94 | ||
| 95 | for entry in _records do | |
| 96 | snapshot[entry.key] = entry.value.count | |
| 97 | od | |
| 98 | ||
| 99 | _marks.add(snapshot) | |
| 100 | si | |
| 101 | ||
| 102 | commit() static is | |
| 103 | if _marks.count > 0 then | |
| 104 | _marks.remove_at(_marks.count - 1) | |
| 105 | fi | |
| 106 | si | |
| 107 | ||
| 108 | roll_back() static is | |
| 109 | if _marks.count == 0 then | |
| 110 | return | |
| 111 | fi | |
| 112 | ||
| 113 | let snapshot = _marks[_marks.count - 1] | |
| 114 | ||
| 115 | _marks.remove_at(_marks.count - 1) | |
| 116 | ||
| 117 | for entry in _records do | |
| 118 | let list = entry.value | |
| 119 | ||
| 120 | let keep = | |
| 121 | if snapshot.contains_key(entry.key) then | |
| 122 | snapshot[entry.key] | |
| 123 | else | |
| 124 | 0 | |
| 125 | fi | |
| 126 | ||
| 127 | while list.count > keep do | |
| 128 | list.remove_at(list.count - 1) | |
| 129 | od | |
| 130 | od | |
| 131 | si | |
| 132 | ||
| 133 | // Hand over what has been recorded and start fresh: the caller | |
| 134 | // reports against the relations just solved. One record per | |
| 135 | // location: a body re-walked to convergence (overload retry, | |
| 136 | // delegate conversion) records the same slot once per walk, | |
| 137 | // and the last walk is the one whose compilation stands. | |
| 138 | take() -> Collections.List[PURE_SLOT_RECORD] static is | |
| 139 | let by_slot = Collections.MAP[(LOCATION, int), PURE_SLOT_RECORD]() | |
| 140 | ||
| 141 | for entry in _records do | |
| 142 | for record in entry.value do | |
| 143 | by_slot[(record.location, record.slot_index)] = record | |
| 144 | od | |
| 145 | od | |
| 146 | ||
| 147 | _records.clear() | |
| 148 | _marks.clear() | |
| 149 | ||
| 150 | let taken = Collections.LIST[PURE_SLOT_RECORD]() | |
| 151 | ||
| 152 | for pair in by_slot do | |
| 153 | taken.add(pair.value) | |
| 154 | od | |
| 155 | ||
| 156 | return taken | |
| 157 | si | |
| 158 | si | |
| 159 | ||
| 160 | // Records values reaching pure function-typed slots as expressions | |
| 161 | // compile. The judgement itself is PURE_SLOT_JUDGE, after the | |
| 162 | // effect relations are solved. | |
| 163 | class PURE_SLOT_CHECK is | |
| 164 | _build_flags: Compiler.GLOBAL_BUILD_FLAGS | |
| 165 | _flow: NARROWING_FLOW | |
| 166 | ||
| 167 | // Resolves argument values to the functions their shapes name. | |
| 168 | // A fresh resolver rather than the effects walk's: at this | |
| 169 | // point in the build its local-variable record does not exist | |
| 170 | // yet, and the structural shapes — literals, delegates, named | |
| 171 | // functions — are all a crossing's callee needs. | |
| 172 | _functions: FUNCTION_VALUES | |
| 173 | ||
| 174 | init(flow: NARROWING_FLOW, build_flags: Compiler.GLOBAL_BUILD_FLAGS) is | |
| 175 | super.init() | |
| 176 | ||
| 177 | _flow = flow | |
| 178 | _build_flags = build_flags | |
| 179 | _functions = FUNCTION_VALUES() | |
| 180 | si | |
| 181 | ||
| 182 | // Every argument of a fully-built call that lands in a pure | |
| 183 | // formal. Applies to any call-shaped value: an ordinary call, | |
| 184 | // a user-defined operator or indexer, a construction. | |
| 185 | // | |
| 186 | // `syntax_arguments` are the written argument expressions, used | |
| 187 | // to report against the offending argument rather than the whole | |
| 188 | // call. They are only trusted when their count matches the | |
| 189 | // built call's, so a lowering that inserts or drops an argument | |
| 190 | // falls back to the call's own location rather than blaming the | |
| 191 | // wrong one. | |
| 192 | check_call( | |
| 193 | location: LOCATION, | |
| 194 | value: IR.Values.Value?, | |
| 195 | syntax_arguments: Trees.Expressions.LIST? | |
| 196 | ) is | |
| 197 | let function: Function? mut = null | |
| 198 | let arguments: Collections.List[IR.Values.Value]? mut = null | |
| 199 | ||
| 200 | if let call: IR.Values.Call.INSTANCE = value then | |
| 201 | function = call.function | |
| 202 | arguments = call.arguments | |
| 203 | elif let call: IR.Values.Call.GLOBAL = value then | |
| 204 | function = call.function | |
| 205 | arguments = call.arguments | |
| 206 | elif let call: IR.Values.Call.STATIC = value then | |
| 207 | function = call.function | |
| 208 | arguments = call.arguments | |
| 209 | elif let call: IR.Values.Call.STRUCT = value then | |
| 210 | function = call.function | |
| 211 | arguments = call.arguments | |
| 212 | else | |
| 213 | return | |
| 214 | fi | |
| 215 | ||
| 216 | let formals = function.arguments | |
| 217 | ||
| 218 | for i in 0..formals.count do | |
| 219 | if i >= arguments.count then | |
| 220 | return | |
| 221 | fi | |
| 222 | ||
| 223 | if formals[i].is_pure_function then | |
| 224 | // suppressing the warning must not change what is | |
| 225 | // compiled, so only the record is gated: the | |
| 226 | // crossing below registers either way | |
| 227 | if !_build_flags.no_warn_impure_function_argument then | |
| 228 | PURE_SLOTS.note( | |
| 229 | PURE_SLOT_RECORD( | |
| 230 | _argument_location(syntax_arguments, i, arguments.count, location), | |
| 231 | i, | |
| 232 | arguments[i], | |
| 233 | "impure-function-argument", | |
| 234 | "argument must be a pure function")) | |
| 235 | fi | |
| 236 | ||
| 237 | _note_untrusted_argument(location, arguments[i]) | |
| 238 | fi | |
| 239 | od | |
| 240 | si | |
| 241 | ||
| 242 | // The callee is trusted on its own store-freedom, and that | |
| 243 | // trust assumes its pure function-typed parameters hold | |
| 244 | // store-free values. An argument that is not structurally | |
| 245 | // trustworthy is a hole in that assumption, so the call is | |
| 246 | // recorded as a crossing against the function the argument | |
| 247 | // names — dischargeable once the solve proves it — or as an | |
| 248 | // unbounded crossing when the value names none. | |
| 249 | _note_untrusted_argument(location: LOCATION, argument: IR.Values.Value?) is | |
| 250 | if argument? /\ argument.type? /\ argument.type.is_pure_function then | |
| 251 | return | |
| 252 | fi | |
| 253 | ||
| 254 | if let function = _functions.function_value_of(argument) then | |
| 255 | if !function.is_store_free then | |
| 256 | _flow.on_call_of(location, function) | |
| 257 | fi | |
| 258 | ||
| 259 | return | |
| 260 | fi | |
| 261 | ||
| 262 | _flow.on_call(location) | |
| 263 | si | |
| 264 | ||
| 265 | _argument_location( | |
| 266 | syntax_arguments: Trees.Expressions.LIST?, | |
| 267 | index: int, | |
| 268 | count: int, | |
| 269 | fallback: LOCATION | |
| 270 | ) -> LOCATION is | |
| 271 | let syntax_index = _syntax_index(syntax_arguments, index, count) | |
| 272 | ||
| 273 | if syntax_index >= 0 then | |
| 274 | return syntax_arguments!.expressions[syntax_index].location | |
| 275 | fi | |
| 276 | ||
| 277 | return fallback | |
| 278 | si | |
| 279 | ||
| 280 | // The written argument standing behind built argument | |
| 281 | // `index`, or -1 when the two lists cannot be aligned. Equal | |
| 282 | // counts align directly; one extra built argument is the | |
| 283 | // thread-first `\|>` shape, where the threaded value is the | |
| 284 | // built call's first argument and the written list supplies | |
| 285 | // the rest. Anything else is a lowering this cannot see | |
| 286 | // through, and the caller falls back to the built value and | |
| 287 | // the call's own location. | |
| 288 | _syntax_index( | |
| 289 | syntax_arguments: Trees.Expressions.LIST?, | |
| 290 | index: int, | |
| 291 | count: int | |
| 292 | ) -> int is | |
| 293 | if !syntax_arguments? then | |
| 294 | return -1 | |
| 295 | fi | |
| 296 | ||
| 297 | let offset = count - syntax_arguments.count | |
| 298 | ||
| 299 | if offset != 0 /\ offset != 1 then | |
| 300 | return -1 | |
| 301 | fi | |
| 302 | ||
| 303 | let syntax_index = index - offset | |
| 304 | ||
| 305 | if syntax_index < 0 then | |
| 306 | return -1 | |
| 307 | fi | |
| 308 | ||
| 309 | return syntax_index | |
| 310 | si | |
| 311 | ||
| 312 | // A value stored into a slot whose type is a pure function | |
| 313 | // type. The slot's type is a claim that it holds store-free | |
| 314 | // values, and is trusted wherever the slot is read, so the | |
| 315 | // store is where the value has to be shown store-free. | |
| 316 | check_store(location: LOCATION, target_type: Semantic.Types.Type?, value: IR.Values.Value?) is | |
| 317 | // A slot whose type is still settling is not a claim about | |
| 318 | // anything: the walk that produced it is superseded by a | |
| 319 | // later one, and the purity of a placeholder shape says | |
| 320 | // only what inference happened to be holding at the time. | |
| 321 | // Recording it leaves a judgement standing against a | |
| 322 | // contract that no longer exists once the type settles. | |
| 323 | if | |
| 324 | target_type? /\ target_type.is_pure_function /\ | |
| 325 | !target_type.contains_inferred /\ | |
| 326 | !_build_flags.no_warn_impure_function_value | |
| 327 | then | |
| 328 | PURE_SLOTS.note( | |
| 329 | PURE_SLOT_RECORD( | |
| 330 | location, | |
| 331 | -1, | |
| 332 | value, | |
| 333 | "impure-function-value", | |
| 334 | "value must be a pure function")) | |
| 335 | fi | |
| 336 | si | |
| 337 | si | |
| 338 | ||
| 339 | // Judges what reached a pure function-typed slot, once the effect | |
| 340 | // relations can answer whether each value is store-free. | |
| 341 | // | |
| 342 | // The test is "cannot prove store-free", not "is known to store", | |
| 343 | // so it is conservative and reports a warning. | |
| 344 | class PURE_SLOT_JUDGE is | |
| 345 | _logger: Logger | |
| 346 | ||
| 347 | // Resolves a compiled value to the function it denotes, | |
| 348 | // including a lambda literal's closure and an immutable local | |
| 349 | // holding one. Owned by INFER_STORE_FREE, whose resolved walk | |
| 350 | // populates the local-value map this consults. | |
| 351 | _functions: FUNCTION_VALUES | |
| 352 | ||
| 353 | init(logger: Logger, functions: FUNCTION_VALUES) is | |
| 354 | super.init() | |
| 355 | ||
| 356 | _logger = logger | |
| 357 | _functions = functions | |
| 358 | si | |
| 359 | ||
| 360 | judge() is | |
| 361 | let trace = System.Environment.get_environment_variable("GHUL_PURE_SLOT_TRACE")? | |
| 362 | ||
| 363 | for record in PURE_SLOTS.take() do | |
| 364 | if !is_satisfied(record.value) then | |
| 365 | if trace then | |
| 366 | let function = _functions.function_value_of(record.value) | |
| 367 | ||
| 368 | IO.Std.error.write_line( | |
| 369 | "pure-slot miss at {record.location}: value kind {record.value?.get_type()} resolved {function} effects {EFFECTS.is_store_free(function)} type {record.value?.type}") | |
| 370 | fi | |
| 371 | ||
| 372 | _logger.warn(record.location, record.slug, record.message) | |
| 373 | fi | |
| 374 | od | |
| 375 | si | |
| 376 | ||
| 377 | is_satisfied(argument: IR.Values.Value?) -> bool is | |
| 378 | if !argument? then | |
| 379 | return true | |
| 380 | fi | |
| 381 | ||
| 382 | // A read of a slot already typed pure — a local, field or | |
| 383 | // parameter — is trusted on the type: the store into that | |
| 384 | // slot is where this same check made the value show | |
| 385 | // itself, and re-reporting every later read of a slot | |
| 386 | // whose one offending store was already reported would be | |
| 387 | // noise. | |
| 388 | if _is_pure_typed_slot_read(argument) then | |
| 389 | return true | |
| 390 | fi | |
| 391 | ||
| 392 | // A lambda literal, a named function, or an immutable | |
| 393 | // local holding one: the function's own store-free answer | |
| 394 | // decides, whether declared, whitelisted or solved. | |
| 395 | if let function = _functions.function_value_of(argument) then | |
| 396 | return EFFECTS.is_store_free(function) | |
| 397 | fi | |
| 398 | ||
| 399 | // Otherwise only the value's own type can say: a slot | |
| 400 | // already declared pure holds store-free values by the | |
| 401 | // same contract this check enforces at its stores. | |
| 402 | return argument.type? /\ argument.type.is_pure_function | |
| 403 | si | |
| 404 | ||
| 405 | _is_pure_typed_slot_read(argument: IR.Values.Value) -> bool is | |
| 406 | if !argument.type? \/ !argument.type.is_pure_function then | |
| 407 | return false | |
| 408 | fi | |
| 409 | ||
| 410 | return | |
| 411 | isa IR.Values.Load.LOCAL_VARIABLE(argument) \/ | |
| 412 | isa IR.Values.Load.LOCAL_ARGUMENT(argument) \/ | |
| 413 | isa IR.Values.Load.ARGUMENT_SLOT(argument) \/ | |
| 414 | isa IR.Values.Load.INSTANCE_FIELD(argument) \/ | |
| 415 | isa IR.Values.Load.STATIC_FIELD(argument) \/ | |
| 416 | isa IR.Values.Load.GLOBAL_FIELD(argument) | |
| 417 | si | |
| 418 | si | |
| 419 | si |