Handle tricky case of abs.interp.'ing a `repeat` loop.
Cat's Eye Technologies
8 years ago
86 | 86 |
|
87 | 87 |
Abstract interpretation extends to `if` blocks. The two incoming contexts are
|
88 | 88 |
merged, and any storage locations poisoned in either context are considered
|
89 | |
poisoned in the result context.
|
90 | |
|
91 | |
(Same should apply for `repeat` and `with` and, really, many other cases
|
92 | |
which there just aren't enough test cases for yet.)
|
|
89 |
poisoned in the result context. (A similar case applies to `repeat` and
|
|
90 |
`with`, but these are different too as there is only one block and it is always
|
|
91 |
executed at least once.)
|
93 | 92 |
|
94 | 93 |
Declarations can have block scope. Such declarations may only be used within
|
95 | 94 |
the block in which they are declared. `reserve`d storage inside a block is not,
|
131 | 131 |
= A: UpdatedWith (Immediate 8)
|
132 | 132 |
|
133 | 133 |
If a location is poisoned in either branch of an `if`, it is poisoned
|
134 | |
after the `if`.
|
|
134 |
after the `if`. Note there are several tests for this.
|
135 | 135 |
|
136 | 136 |
| reserve byte score
|
137 | 137 |
| routine update_score
|
|
222 | 222 |
= update_score ([])
|
223 | 223 |
= X: UpdatedWith (Immediate 4)
|
224 | 224 |
= NamedLocation Nothing "score": UpdatedWith X
|
225 | |
|
226 | |
Poisoning a high byte or low byte of a word poisons the whole word.
|
227 | |
|
228 | |
| reserve word score
|
229 | |
| reserve byte temp
|
230 | |
| routine update_score
|
231 | |
| {
|
232 | |
| ldx #4
|
233 | |
| stx <score
|
234 | |
| }
|
235 | |
| routine main {
|
236 | |
| jsr update_score
|
237 | |
| lda >score
|
238 | |
| sta temp
|
239 | |
| }
|
240 | |
? routine 'main' does not preserve 'NamedLocation Nothing "score"'
|
241 | |
|
242 | |
Some more tests...
|
243 | 225 |
|
244 | 226 |
| assign word position $fb
|
245 | 227 |
| reserve byte value
|
|
317 | 299 |
| }
|
318 | 300 |
| }
|
319 | 301 |
? routine 'main' does not preserve 'A'
|
|
302 |
|
|
303 |
A storage location poisoned in a `repeat` continues to be poisoned
|
|
304 |
after the `repeat`.
|
|
305 |
|
|
306 |
| reserve byte value
|
|
307 |
|
|
|
308 |
| routine blah {
|
|
309 |
| lda #123
|
|
310 |
| }
|
|
311 |
| routine main {
|
|
312 |
| lda #33
|
|
313 |
| ldy #255
|
|
314 |
| repeat bne {
|
|
315 |
| jsr blah
|
|
316 |
| dey
|
|
317 |
| }
|
|
318 |
| sta value
|
|
319 |
| }
|
|
320 |
? routine 'main' does not preserve 'A'
|
|
321 |
|
|
322 |
Oh, here's a tricky one. The accumulator isn't poisoned on the first run
|
|
323 |
through the `repeat`, but it **is** on the second run through. We handle
|
|
324 |
this simply by abstractly interpreting the `repeat`'s block twice — the
|
|
325 |
second time in the context of having already interpreted it once.
|
|
326 |
|
|
327 |
| reserve byte value
|
|
328 |
|
|
|
329 |
| routine blah {
|
|
330 |
| lda #123
|
|
331 |
| }
|
|
332 |
| routine main {
|
|
333 |
| lda #33
|
|
334 |
| ldy #255
|
|
335 |
| repeat bne {
|
|
336 |
| sta value
|
|
337 |
| jsr blah
|
|
338 |
| dey
|
|
339 |
| }
|
|
340 |
| }
|
|
341 |
? routine 'main' does not preserve 'A'
|
|
342 |
|
|
343 |
Poisoning a high byte or low byte of a word poisons the whole word.
|
|
344 |
|
|
345 |
| reserve word score
|
|
346 |
| reserve byte temp
|
|
347 |
| routine update_score
|
|
348 |
| {
|
|
349 |
| ldx #4
|
|
350 |
| stx <score
|
|
351 |
| }
|
|
352 |
| routine main {
|
|
353 |
| jsr update_score
|
|
354 |
| lda >score
|
|
355 |
| sta temp
|
|
356 |
| }
|
|
357 |
? routine 'main' does not preserve 'NamedLocation Nothing "score"'
|
|
358 |
|
|
359 |
| reserve word score
|
|
360 |
| reserve byte temp
|
|
361 |
| routine update_score
|
|
362 |
| {
|
|
363 |
| ldx #4
|
|
364 |
| stx >score
|
|
365 |
| }
|
|
366 |
| routine main {
|
|
367 |
| jsr update_score
|
|
368 |
| lda <score
|
|
369 |
| sta temp
|
|
370 |
| }
|
|
371 |
? routine 'main' does not preserve 'NamedLocation Nothing "score"'
|
70 | 70 |
in
|
71 | 71 |
mergeAlternateRoutCtxs nm routCtx1 routCtx2
|
72 | 72 |
checkInstr nm (REPEAT _ branch blk) progCtx routCtx =
|
73 | |
-- TODO: oooh, this one's gonna be fun too
|
74 | |
--checkBlock blk progCtx routCtx
|
75 | |
routCtx
|
|
73 |
-- we analyze the block twice, to simulate it being
|
|
74 |
-- repeated. (see tests for a test case on this.
|
|
75 |
let
|
|
76 |
routCtx' = checkBlock nm blk progCtx routCtx
|
|
77 |
routCtx'' = checkBlock nm blk progCtx routCtx'
|
|
78 |
in
|
|
79 |
routCtx''
|
76 | 80 |
|
77 | 81 |
-- TODO -- THESE ARE WEAK --
|
78 | 82 |
checkInstr nm (WITH _ blk) progCtx routCtx =
|