Appearance
| 1 | namespace Syntax.Process is | |
| 2 | use Function = Semantic.Symbols.Function | |
| 3 | use Symbol = Semantic.Symbols.Symbol | |
| 4 | use Semantic.Symbols.STORE_FREE_IMPORTS | |
| 5 | ||
| 6 | // One solve's worth of whole-program effect facts: per function, | |
| 7 | // the members it may write, the members it may assign a | |
| 8 | // possibly-absent value, and the members its getter closure reads, | |
| 9 | // each folded over everything the function can dispatch to or | |
| 10 | // invoke. Keyed by symbol id on both axes - a specialized function | |
| 11 | // or member queries as its root - so facts recorded against one | |
| 12 | // instantiation answer for all of them, and so the relations | |
| 13 | // outlive the symbol objects: a symbol re-created by an | |
| 14 | // incremental edit or a rebuild adopts its predecessor's id and | |
| 15 | // is answered for as before. | |
| 16 | // | |
| 17 | // `complete` says the solve covered every body of the program with | |
| 18 | // the types compile-expressions resolved. An analysis-mode rebuild | |
| 19 | // with files closed solves over declared types for those files and | |
| 20 | // is not complete: its dispatch is coarser, so its relations are | |
| 21 | // more pessimistic than the program warrants. | |
| 22 | class EFFECT_RELATIONS is | |
| 23 | write_sets: Collections.MAP[int, Collections.SET[int]] | |
| 24 | write_unbounded: Collections.SET[int] | |
| 25 | null_sets: Collections.MAP[int, Collections.SET[int]] | |
| 26 | null_unbounded: Collections.SET[int] | |
| 27 | store_free: Collections.SET[int] | |
| 28 | constructs_store_free: Collections.SET[int] | |
| 29 | read_sets: Collections.MAP[int, Collections.SET[int]] | |
| 30 | read_unbounded: Collections.SET[int] | |
| 31 | reads_elements: Collections.SET[int] | |
| 32 | writes_elements: Collections.SET[int] | |
| 33 | complete: bool | |
| 34 | ||
| 35 | init( | |
| 36 | write_sets: Collections.MutableMap[Function, Collections.SET[Symbol]], | |
| 37 | write_unbounded: Collections.SET[Function], | |
| 38 | null_sets: Collections.MutableMap[Function, Collections.SET[Symbol]], | |
| 39 | null_unbounded: Collections.SET[Function], | |
| 40 | store_free: Collections.SET[Function], | |
| 41 | constructs_store_free: Collections.SET[Function], | |
| 42 | read_sets: Collections.MutableMap[Function, Collections.SET[Symbol]], | |
| 43 | read_unbounded: Collections.SET[Function], | |
| 44 | reads_elements: Collections.SET[Function], | |
| 45 | writes_elements: Collections.SET[Function], | |
| 46 | complete: bool | |
| 47 | ) is | |
| 48 | self.write_sets = _ids_of(write_sets) | |
| 49 | self.write_unbounded = _ids_of(write_unbounded) | |
| 50 | self.null_sets = _ids_of(null_sets) | |
| 51 | self.null_unbounded = _ids_of(null_unbounded) | |
| 52 | self.store_free = _ids_of(store_free) | |
| 53 | self.constructs_store_free = _ids_of(constructs_store_free) | |
| 54 | self.read_sets = _ids_of(read_sets) | |
| 55 | self.read_unbounded = _ids_of(read_unbounded) | |
| 56 | self.reads_elements = _ids_of(reads_elements) | |
| 57 | self.writes_elements = _ids_of(writes_elements) | |
| 58 | self.complete = complete | |
| 59 | si | |
| 60 | ||
| 61 | _ids_of(map: Collections.MutableMap[Function, Collections.SET[Symbol]]) -> Collections.MAP[int, Collections.SET[int]] static is | |
| 62 | let result = Collections.MAP[int, Collections.SET[int]]() | |
| 63 | ||
| 64 | for entry in map do | |
| 65 | let members = Collections.SET[int]() | |
| 66 | ||
| 67 | for member in entry.value do | |
| 68 | members.add(member.id) | |
| 69 | od | |
| 70 | ||
| 71 | result[entry.key.id] = members | |
| 72 | od | |
| 73 | ||
| 74 | return result | |
| 75 | si | |
| 76 | ||
| 77 | _ids_of(functions: Collections.SET[Function]) -> Collections.SET[int] static is | |
| 78 | let result = Collections.SET[int]() | |
| 79 | ||
| 80 | for function in functions do | |
| 81 | result.add(function.id) | |
| 82 | od | |
| 83 | ||
| 84 | return result | |
| 85 | si | |
| 86 | si | |
| 87 | ||
| 88 | // The solved effect relations the narrowing walk and the kill | |
| 89 | // ledger read. Every query answers conservatively until a solve is | |
| 90 | // installed, and again after clear(). | |
| 91 | // | |
| 92 | // Why a walk only ever kills from a complete solve, and why a | |
| 93 | // source function the solve did not see answers as harmless: the | |
| 94 | // walk and the solve feed each other. A fact killed at a call | |
| 95 | // widens the view the rest of the body reads, a wider receiver | |
| 96 | // dispatches more coarsely, a coarser dispatch bounds fewer | |
| 97 | // callees, and the next solve then justifies the kill with the | |
| 98 | // relations the kill itself made worse. Started from every fact | |
| 99 | // kept, the descent only kills what the relations of the program | |
| 100 | // as it is cannot back, and settles at the most precise answer; | |
| 101 | // started from a pessimistic guess, it can settle short of it. So | |
| 102 | // an incomplete solve never displaces a complete one, and a source | |
| 103 | // function unknown to the relations in use - declared since the | |
| 104 | // last complete solve - is taken to leave every fact alone until a | |
| 105 | // complete solve says otherwise. Every such decision is on the | |
| 106 | // ledger and re-asked. | |
| 107 | class EFFECTS is | |
| 108 | _relations: EFFECT_RELATIONS? static | |
| 109 | ||
| 110 | is_solved: bool static => _relations? | |
| 111 | ||
| 112 | // Whether the relations in use came from a complete solve. | |
| 113 | is_complete: bool static => | |
| 114 | if let relations = _relations then relations.complete else false fi | |
| 115 | ||
| 116 | install( | |
| 117 | write_sets: Collections.MutableMap[Function, Collections.SET[Symbol]], | |
| 118 | write_unbounded: Collections.SET[Function], | |
| 119 | null_sets: Collections.MutableMap[Function, Collections.SET[Symbol]], | |
| 120 | null_unbounded: Collections.SET[Function], | |
| 121 | store_free: Collections.SET[Function], | |
| 122 | constructs_store_free: Collections.SET[Function], | |
| 123 | read_sets: Collections.MutableMap[Function, Collections.SET[Symbol]], | |
| 124 | read_unbounded: Collections.SET[Function], | |
| 125 | reads_elements: Collections.SET[Function], | |
| 126 | writes_elements: Collections.SET[Function], | |
| 127 | complete: bool | |
| 128 | ) static is | |
| 129 | if !complete /\ is_complete then | |
| 130 | if System.Environment.get_environment_variable("GHUL_EFFECTS_TIMING")? then | |
| 131 | IO.Std.error.write_line("effects: incomplete solve not installed over the complete one") | |
| 132 | fi | |
| 133 | ||
| 134 | return | |
| 135 | fi | |
| 136 | ||
| 137 | _relations = EFFECT_RELATIONS( | |
| 138 | write_sets, write_unbounded, | |
| 139 | null_sets, null_unbounded, | |
| 140 | store_free, constructs_store_free, | |
| 141 | read_sets, read_unbounded, reads_elements, writes_elements, | |
| 142 | complete) | |
| 143 | si | |
| 144 | ||
| 145 | clear() static is | |
| 146 | _relations = null | |
| 147 | si | |
| 148 | ||
| 149 | _root_of(callee: Function?) -> Function? static => | |
| 150 | if let c = callee then cast Function?(c.root_specialized_from) else null fi | |
| 151 | ||
| 152 | // Whether the relations in use saw this function's body. | |
| 153 | knows(callee: Function?) -> bool static is | |
| 154 | if let relations = _relations, root = _root_of(callee) then | |
| 155 | return relations.write_sets.contains_key(root.id) | |
| 156 | fi | |
| 157 | ||
| 158 | return false | |
| 159 | si | |
| 160 | ||
| 161 | // A source function the relations did not see is taken to be | |
| 162 | // harmless; see the class comment. An import was never going | |
| 163 | // to be walked and keeps the conservative default. | |
| 164 | _unknown_source(root: Function) -> bool static => | |
| 165 | !root.location.is_reflected /\ !root.location.is_internal | |
| 166 | ||
| 167 | // May calling `callee` - or anything it can reach - store to | |
| 168 | // `member` through any receiver? Conservatively yes when | |
| 169 | // nothing is solved, when the callee's write set could not be | |
| 170 | // bounded, or when the callee is an import that is neither | |
| 171 | // declared pure nor on the curated store-free whitelist. | |
| 172 | may_write(callee: Function?, member: Symbol?) -> bool static => | |
| 173 | if let m = member then may_write(callee, m.root_specialized_from.id) else true fi | |
| 174 | ||
| 175 | may_write(callee: Function?, member_id: int) -> bool static => | |
| 176 | _may_touch(callee, member_id, true) | |
| 177 | ||
| 178 | // May calling `callee` - or anything it can reach - assign a | |
| 179 | // possibly-absent value to `member`? Same defaults as may_write. | |
| 180 | may_null(callee: Function?, member: Symbol?) -> bool static => | |
| 181 | if let m = member then _may_touch(callee, m.root_specialized_from.id, false) else true fi | |
| 182 | ||
| 183 | _may_touch(callee: Function?, member_id: int, writes: bool) -> bool static is | |
| 184 | let relations = _relations | |
| 185 | let root = _root_of(callee) | |
| 186 | ||
| 187 | if !relations? \/ !root? then | |
| 188 | return true | |
| 189 | fi | |
| 190 | ||
| 191 | let sets = if writes then relations.write_sets else relations.null_sets fi | |
| 192 | let unbounded = if writes then relations.write_unbounded else relations.null_unbounded fi | |
| 193 | ||
| 194 | if !sets.contains_key(root.id) then | |
| 195 | if _unknown_source(root) then | |
| 196 | return false | |
| 197 | fi | |
| 198 | ||
| 199 | // an import: a store-free or receiver-interior one | |
| 200 | // writes no ghul member; anything else could | |
| 201 | return !_trusted_leaf(root) /\ !root.writes_only_receiver_interior | |
| 202 | fi | |
| 203 | ||
| 204 | if unbounded.contains(root.id) then | |
| 205 | return true | |
| 206 | fi | |
| 207 | ||
| 208 | return sets[root.id].contains(member_id) | |
| 209 | si | |
| 210 | ||
| 211 | // Does `callee` provably store nothing at all - member writes, | |
| 212 | // element writes, and everything reachable included? The | |
| 213 | // strong answer property facts need, since a getter can read | |
| 214 | // any of it. | |
| 215 | is_store_free(callee: Function?) -> bool static is | |
| 216 | let root = _root_of(callee) | |
| 217 | ||
| 218 | if !root? then | |
| 219 | return false | |
| 220 | fi | |
| 221 | ||
| 222 | // The declared, whitelisted and already-proven answers | |
| 223 | // are sound however this run's solve went, so take the | |
| 224 | // union with the solved set rather than replacing it. | |
| 225 | if root.is_store_free then | |
| 226 | return true | |
| 227 | fi | |
| 228 | ||
| 229 | if let relations = _relations then | |
| 230 | if relations.store_free.contains(root.id) then | |
| 231 | return true | |
| 232 | fi | |
| 233 | ||
| 234 | return !relations.write_sets.contains_key(root.id) /\ _unknown_source(root) | |
| 235 | fi | |
| 236 | ||
| 237 | return false | |
| 238 | si | |
| 239 | ||
| 240 | // Does calling `callee` as a constructor on a fresh receiver | |
| 241 | // provably leave every pre-existing heap slot alone? Weaker | |
| 242 | // than store-free - the body may write its own receiver's | |
| 243 | // state - but just as harmless to any fact established before | |
| 244 | // the construction, since nothing pre-existing can reach the | |
| 245 | // fresh object. | |
| 246 | constructs_store_free(callee: Function?) -> bool static is | |
| 247 | if is_store_free(callee) then | |
| 248 | return true | |
| 249 | fi | |
| 250 | ||
| 251 | if let relations = _relations, root = _root_of(callee) then | |
| 252 | return relations.constructs_store_free.contains(root.id) | |
| 253 | fi | |
| 254 | ||
| 255 | return false | |
| 256 | si | |
| 257 | ||
| 258 | // The solved write set of `function`, or null when it is unbounded | |
| 259 | // or unknown. Measurement only. | |
| 260 | write_set_of(function: Function) -> Collections.SET[int]? static is | |
| 261 | if let relations = _relations, root = _root_of(function) then | |
| 262 | if relations.write_unbounded.contains(root.id) \/ !relations.write_sets.contains_key(root.id) then | |
| 263 | return null | |
| 264 | fi | |
| 265 | ||
| 266 | return relations.write_sets[root.id] | |
| 267 | fi | |
| 268 | ||
| 269 | return null | |
| 270 | si | |
| 271 | ||
| 272 | _trusted_leaf(root: Function) -> bool static => | |
| 273 | root.is_store_free \/ STORE_FREE_IMPORTS.is_store_free(root) | |
| 274 | ||
| 275 | // The ids of the members in `getter`'s read closure, or null | |
| 276 | // when it cannot be bounded (unsolved, an unwalked import, or | |
| 277 | // the closure reaches something unboundable). An unknown | |
| 278 | // source getter reads nothing the relations know of. | |
| 279 | getter_read_closure(getter: Function?) -> Collections.SET[int]? static is | |
| 280 | let relations = _relations | |
| 281 | let root = _root_of(getter) | |
| 282 | ||
| 283 | if !relations? \/ !root? then | |
| 284 | return null | |
| 285 | fi | |
| 286 | ||
| 287 | if !relations.read_sets.contains_key(root.id) then | |
| 288 | return if _unknown_source(root) then Collections.SET[int]() else null fi | |
| 289 | fi | |
| 290 | ||
| 291 | if relations.read_unbounded.contains(root.id) then | |
| 292 | return null | |
| 293 | fi | |
| 294 | ||
| 295 | return relations.read_sets[root.id] | |
| 296 | si | |
| 297 | ||
| 298 | // Whether the getter's closure may read collection or array | |
| 299 | // elements. Conservatively yes when nothing is solved. | |
| 300 | getter_reads_elements(getter: Function?) -> bool static is | |
| 301 | let relations = _relations | |
| 302 | let root = _root_of(getter) | |
| 303 | ||
| 304 | if !relations? \/ !root? then | |
| 305 | return true | |
| 306 | fi | |
| 307 | ||
| 308 | if !relations.read_sets.contains_key(root.id) /\ _unknown_source(root) then | |
| 309 | return false | |
| 310 | fi | |
| 311 | ||
| 312 | return relations.reads_elements.contains(root.id) | |
| 313 | si | |
| 314 | ||
| 315 | // May calling `callee` write a collection or array element? | |
| 316 | // Conservatively yes; the trusted store-free tiers write | |
| 317 | // nothing at all, while a receiver-interior mutator writes | |
| 318 | // exactly this. | |
| 319 | may_write_elements(callee: Function?) -> bool static is | |
| 320 | let relations = _relations | |
| 321 | let root = _root_of(callee) | |
| 322 | ||
| 323 | if !relations? \/ !root? then | |
| 324 | return true | |
| 325 | fi | |
| 326 | ||
| 327 | if relations.write_sets.contains_key(root.id) then | |
| 328 | return relations.writes_elements.contains(root.id) | |
| 329 | fi | |
| 330 | ||
| 331 | if _unknown_source(root) \/ _trusted_leaf(root) then | |
| 332 | return false | |
| 333 | fi | |
| 334 | ||
| 335 | return true | |
| 336 | si | |
| 337 | si | |
| 338 | si |