38 KiB
SixtyPical Analysis - Storage
This is a test suite, written in Falderal format, for the SixtyPical static analysis rules, with regard to storage (load, store, tables, etc.)
-> Tests for functionality "Analyze SixtyPical program"
Rudiments
Routines must declare their inputs, outputs, and memory locations they trash.
| define up routine
| inputs a
| outputs a
| trashes c, z, v, n
| {
| st off, c
| add a, 1
| }
= ok
Routines may not declare a memory location to be both an output and trashed.
| define main routine
| outputs a
| trashes a
| {
| ld a, 0
| }
? InconsistentConstraintsError: a
If a routine declares it outputs a location, that location should be initialized.
| define main routine
| outputs a, x, z, n
| {
| ld x, 0
| }
? UnmeaningfulOutputError: a
| define main routine
| inputs a
| outputs a
| {
| }
= ok
If a routine declares it outputs a location, that location may or may not have been initialized. Trashing is mainly a signal to the caller.
| define main routine
| trashes x, z, n
| {
| ld x, 0
| }
= ok
| define main routine
| trashes x, z, n
| {
| }
= ok
If a routine modifies a location, it needs to either output it or trash it.
| define main routine
| {
| ld x, 0
| }
? ForbiddenWriteError: x
| define main routine
| outputs x, z, n
| {
| ld x, 0
| }
= ok
| define main routine
| trashes x, z, n
| {
| ld x, 0
| }
= ok
This is true regardless of whether it's an input or not.
| define main routine
| inputs x
| {
| ld x, 0
| }
? ForbiddenWriteError: x
| define main routine
| inputs x
| outputs x, z, n
| {
| ld x, 0
| }
= ok
| define main routine
| inputs x
| trashes x, z, n
| {
| ld x, 0
| }
= ok
If a routine trashes a location, this must be declared.
| define foo routine
| trashes x
| {
| trash x
| }
= ok
| define foo routine
| {
| trash x
| }
? ForbiddenWriteError: x
| define foo routine
| outputs x
| {
| trash x
| }
? UnmeaningfulOutputError: x
If a routine causes a location to be trashed, this must be declared in the caller.
| define trash_x routine
| trashes x, z, n
| {
| ld x, 0
| }
|
| define foo routine
| trashes x, z, n
| {
| call trash_x
| }
= ok
| define trash_x routine
| trashes x, z, n
| {
| ld x, 0
| }
|
| define foo routine
| trashes z, n
| {
| call trash_x
| }
? ForbiddenWriteError: x
| define trash_x routine
| trashes x, z, n
| {
| ld x, 0
| }
|
| define foo routine
| outputs x
| trashes z, n
| {
| call trash_x
| }
? UnmeaningfulOutputError: x (in foo, line 12)
If a routine reads or writes a user-define memory location, it needs to declare that too.
| byte b1 @ 60000
| byte b2 : 3
| word w1 @ 60001
| word w2 : 2000
|
| define main routine
| inputs b1, w1
| outputs b2, w2
| trashes a, z, n
| {
| ld a, b1
| st a, b2
| copy w1, w2
| }
= ok
ld
Can't ld from a memory location that isn't initialized.
| define main routine
| inputs a, x
| trashes a, z, n
| {
| ld a, x
| }
= ok
| define main routine
| inputs a
| trashes a
| {
| ld a, x
| }
? UnmeaningfulReadError: x
Can't ld to a memory location that doesn't appear in (outputs ∪ trashes).
| define main routine
| trashes a, z, n
| {
| ld a, 0
| }
= ok
| define main routine
| outputs a
| trashes z, n
| {
| ld a, 0
| }
= ok
| define main routine
| outputs z, n
| trashes a
| {
| ld a, 0
| }
= ok
| define main routine
| trashes z, n
| {
| ld a, 0
| }
? ForbiddenWriteError: a
| define main routine
| trashes a, n
| {
| ld a, 0
| }
? ForbiddenWriteError: z
Can't ld a word type.
| word foo
|
| define main routine
| inputs foo
| trashes a, n, z
| {
| ld a, foo
| }
? TypeMismatchError: foo and a
st
Can't st from a memory location that isn't initialized.
| byte lives
| define main routine
| inputs x
| trashes lives
| {
| st x, lives
| }
= ok
| byte lives
| define main routine
| trashes x, lives
| {
| st x, lives
| }
? UnmeaningfulReadError: x
Can't st to a memory location that doesn't appear in (outputs ∪ trashes).
| byte lives
| define main routine
| trashes lives
| {
| st 0, lives
| }
= ok
| byte lives
| define main routine
| outputs lives
| {
| st 0, lives
| }
= ok
| byte lives
| define main routine
| inputs lives
| {
| st 0, lives
| }
? ForbiddenWriteError: lives
Can't st a word type.
| word foo
|
| define main routine
| outputs foo
| trashes a, n, z
| {
| ld a, 0
| st a, foo
| }
? TypeMismatchError
tables
Storing to a table, you must use an index.
| byte one
| byte table[256] many
|
| define main routine
| outputs one
| trashes a, x, n, z
| {
| ld x, 0
| ld a, 0
| st a, one
| }
= ok
| byte one
| byte table[256] many
|
| define main routine
| outputs many
| trashes a, x, n, z
| {
| ld x, 0
| ld a, 0
| st a, many
| }
? TypeMismatchError
| byte one
| byte table[256] many
|
| define main routine
| outputs one
| trashes a, x, n, z
| {
| ld x, 0
| ld a, 0
| st a, one + x
| }
? TypeMismatchError
| byte one
| byte table[256] many
|
| define main routine
| outputs many
| trashes a, x, n, z
| {
| ld x, 0
| ld a, 0
| st a, many + x
| }
= ok
The index must be initialized.
| byte one
| byte table[256] many
|
| define main routine
| outputs many
| trashes a, x, n, z
| {
| ld a, 0
| st a, many + x
| }
? UnmeaningfulReadError: x
Reading from a table, you must use an index.
| byte one
|
| define main routine
| outputs one
| trashes a, x, n, z
| {
| ld x, 0
| st x, one
| ld a, one
| }
= ok
| byte one
|
| define main routine
| outputs one
| trashes a, x, n, z
| {
| ld x, 0
| st x, one
| ld a, one + x
| }
? TypeMismatchError
| byte table[256] many
|
| define main routine
| outputs many
| trashes a, x, n, z
| {
| ld x, 0
| ld a, 0
| st a, many + x
| ld a, many
| }
? TypeMismatchError
| byte table[256] many
|
| define main routine
| outputs many
| trashes a, x, n, z
| {
| ld x, 0
| ld a, 0
| st a, many + x
| ld a, many + x
| }
= ok
| byte table[256] many
|
| define main routine
| inputs many
| outputs many
| trashes a, x, n, z
| {
| ld x, 0
| ld a, many + x
| }
= ok
The index must be initialized.
| byte table[256] many
|
| define main routine
| inputs many
| outputs many
| trashes a, x, n, z
| {
| ld a, many + x
| }
? UnmeaningfulReadError: x
Storing to a table, you may also include a constant offset.
| byte one
| byte table[256] many
|
| define main routine
| outputs many
| trashes a, x, n, z
| {
| ld x, 0
| ld a, 0
| st a, many + 100 + x
| }
= ok
Reading from a table, you may also include a constant offset.
| byte table[256] many
|
| define main routine
| inputs many
| outputs many
| trashes a, x, n, z
| {
| ld x, 0
| ld a, many + 100 + x
| }
= ok
Using a constant offset, you can read and write entries in the table beyond the 256th.
| byte one
| byte table[1024] many
|
| define main routine
| inputs many
| outputs many
| trashes a, x, n, z
| {
| ld x, 0
| ld a, many + 999 + x
| st a, many + 1000 + x
| }
= ok
There are other operations you can do on tables. (1/3)
| byte table[256] many
|
| define main routine
| inputs many
| outputs many
| trashes a, x, c, n, z, v
| {
| ld x, 0
| ld a, 0
| st off, c
| add a, many + x
| sub a, many + x
| cmp a, many + x
| }
= ok
There are other operations you can do on tables. (2/3)
| byte table[256] many
|
| define main routine
| inputs many
| outputs many
| trashes a, x, c, n, z
| {
| ld x, 0
| ld a, 0
| and a, many + x
| or a, many + x
| xor a, many + x
| }
= ok
There are other operations you can do on tables. (3/3)
| byte table[256] many
|
| define main routine
| inputs many
| outputs many
| trashes a, x, c, n, z
| {
| ld x, 0
| ld a, 0
| st off, c
| shl many + x
| shr many + x
| inc many + x
| dec many + x
| }
= ok
Copying to and from a word table.
| word one
| word table[256] many
|
| define main routine
| inputs one, many
| outputs one, many
| trashes a, x, n, z
| {
| ld x, 0
| copy one, many + x
| copy many + x, one
| }
= ok
| word one
| word table[256] many
|
| define main routine
| inputs one, many
| outputs one, many
| trashes a, x, n, z
| {
| ld x, 0
| copy one, many
| }
? TypeMismatchError
| word one
| word table[256] many
|
| define main routine
| inputs one, many
| outputs one, many
| trashes a, x, n, z
| {
| ld x, 0
| copy one + x, many
| }
? TypeMismatchError
You can also copy a literal word to a word table. (Even if the table has fewer than 256 entries.)
| word table[32] many
|
| define main routine
| inputs many
| outputs many
| trashes a, x, n, z
| {
| ld x, 0
| copy 9999, many + x
| }
= ok
Copying to and from a word table with a constant offset.
| word one
| word table[256] many
|
| define main routine
| inputs one, many
| outputs one, many
| trashes a, x, n, z
| {
| ld x, 0
| copy one, many + 100 + x
| copy many + 100 + x, one
| copy 9999, many + 1 + x
| }
= ok
tables: range checking
It is a static analysis error if it cannot be proven that a read or write to a table falls within the defined size of that table.
If a table has 256 entries, then there is never a problem (so long as no constant offset is supplied), because a byte cannot index any entry outside of 0..255.
But if the table has fewer than 256 entries, or if a constant offset is supplied, there is the possibility that the index will refer to an entry in the table which does not exist.
A SixtyPical implementation must be able to prove that the index is inside the range of the table in various ways. The simplest is to show that a constant value falls inside or outside the range of the table.
| byte table[32] many
|
| define main routine
| inputs many
| outputs many
| trashes a, x, n, z
| {
| ld x, 31
| ld a, many + x
| st a, many + x
| }
= ok
| byte table[32] many
|
| define main routine
| inputs many
| outputs many
| trashes a, x, n, z
| {
| ld x, 32
| ld a, many + x
| }
? RangeExceededError
| byte table[32] many
|
| define main routine
| inputs many
| outputs many
| trashes a, x, n, z
| {
| ld x, 32
| ld a, 0
| st a, many + x
| }
? RangeExceededError
Any constant offset is taken into account in this check.
| byte table[32] many
|
| define main routine
| inputs many
| outputs many
| trashes a, x, n, z
| {
| ld x, 31
| ld a, many + 1 + x
| }
? RangeExceededError
| byte table[32] many
|
| define main routine
| inputs many
| outputs many
| trashes a, x, n, z
| {
| ld x, 31
| ld a, 0
| st a, many + 1 + x
| }
? RangeExceededError
This applies to copy as well.
| word one: 77
| word table[32] many
|
| define main routine
| inputs many, one
| outputs many, one
| trashes a, x, n, z
| {
| ld x, 31
| copy one, many + x
| copy many + x, one
| }
= ok
| word one: 77
| word table[32] many
|
| define main routine
| inputs many, one
| outputs many, one
| trashes a, x, n, z
| {
| ld x, 32
| copy many + x, one
| }
? RangeExceededError
| word one: 77
| word table[32] many
|
| define main routine
| inputs many, one
| outputs many, one
| trashes a, x, n, z
| {
| ld x, 32
| copy one, many + x
| }
? RangeExceededError
Any constant offset is taken into account in this check.
| word one: 77
| word table[32] many
|
| define main routine
| inputs many, one
| outputs many, one
| trashes a, x, n, z
| {
| ld x, 31
| copy many + 1 + x, one
| }
? RangeExceededError
| word one: 77
| word table[32] many
|
| define main routine
| inputs many, one
| outputs many, one
| trashes a, x, n, z
| {
| ld x, 31
| copy one, many + 1 + x
| }
? RangeExceededError
AND'ing a register with a value ensures the range of the
register will not exceed the range of the value. This can
be used to "clip" the range of an index so that it fits in
a table.
| word one: 77
| word table[32] many
|
| define main routine
| inputs a, many, one
| outputs many, one
| trashes a, x, n, z
| {
| and a, 31
| ld x, a
| copy one, many + x
| copy many + x, one
| }
= ok
Tests for "clipping", but not enough.
| word one: 77
| word table[32] many
|
| define main routine
| inputs a, many, one
| outputs many, one
| trashes a, x, n, z
| {
| and a, 63
| ld x, a
| copy one, many + x
| copy many + x, one
| }
? RangeExceededError
| word one: 77
| word table[32] many
|
| define main routine
| inputs a, many, one
| outputs many, one
| trashes a, x, n, z
| {
| and a, 31
| ld x, a
| copy one, many + 1 + x
| copy many + 1 + x, one
| }
? RangeExceededError
If you alter the value after "clipping" it, the range can no longer be guaranteed.
| word one: 77
| word table[32] many
|
| define main routine
| inputs a, many, one
| outputs many, one
| trashes a, x, n, z
| {
| and a, 31
| ld x, a
| inc x
| copy one, many + x
| copy many + x, one
| }
? RangeExceededError
When the range of a location is known, incrementing or decrementing that location's value will shift the known range. It will not invalidate it unless the known range is at the limits of the possible ranges for the type.
| vector routine
| trashes a, z, n
| print
|
| vector (routine
| trashes a, z, n)
| table[32] vectors
|
| define main routine
| inputs vectors, print
| outputs vectors
| trashes print, a, x, z, n, c
| {
| ld x, 0
| inc x
| copy print, vectors + x
| }
= ok
| vector routine
| trashes a, z, n
| print
|
| vector (routine
| trashes a, z, n)
| table[32] vectors
|
| define main routine
| inputs vectors, print
| outputs vectors
| trashes print, a, x, z, n, c
| {
| ld x, 32
| dec x
| copy print, vectors + x
| }
= ok
trash
Trash does nothing except indicate that we do not care about the value anymore.
| define foo routine
| inputs a
| outputs x
| trashes a, z, n
| {
| st a, x
| ld a, 0
| trash a
| }
= ok
| define foo routine
| inputs a
| outputs a, x
| trashes z, n
| {
| st a, x
| ld a, 0
| trash a
| }
? UnmeaningfulOutputError: a
| define foo routine
| inputs a
| outputs x
| trashes a, z, n
| {
| st a, x
| trash a
| st a, x
| }
? UnmeaningfulReadError: a
copy
Can't copy from a memory location that isn't initialized.
| byte lives
| define main routine
| inputs x
| outputs lives
| trashes a, z, n
| {
| copy x, lives
| }
= ok
| byte lives
| define main routine
| outputs lives
| trashes x, a, z, n
| {
| copy x, lives
| }
? UnmeaningfulReadError: x
Can't copy to a memory location that doesn't appear in (outputs ∪ trashes).
| byte lives
| define main routine
| trashes lives, a, z, n
| {
| copy 0, lives
| }
= ok
| byte lives
| define main routine
| outputs lives
| trashes a, z, n
| {
| copy 0, lives
| }
= ok
| byte lives
| define main routine
| inputs lives
| trashes a, z, n
| {
| copy 0, lives
| }
? ForbiddenWriteError: lives
a, z, and n are trashed, and must be declared as such.
(Note, both n and z are forbidden writes in this test.)
| byte lives
| define main routine
| outputs lives
| {
| copy 0, lives
| }
? ForbiddenWriteError
a, z, and n are trashed, and must not be declared as outputs.
(Note, both n and a are unmeaningful outputs in this test.)
| byte lives
| define main routine
| outputs lives, a, z, n
| {
| copy 0, lives
| }
? UnmeaningfulOutputError
Unless of course you subsequently initialize them.
| byte lives
| define main routine
| outputs lives, a, z, n
| {
| copy 0, lives
| ld a, 0
| }
= ok
Can copy from a byte to a byte.
| byte source : 0
| byte dest
|
| define main routine
| inputs source
| outputs dest
| trashes a, z, n
| {
| copy source, dest
| }
= ok
The understanding is that, because copy trashes a, a cannot be used
as the destination of a copy.
| byte source : 0
| byte dest
|
| define main routine
| inputs source
| outputs dest
| trashes a, z, n
| {
| copy source, a
| }
? ForbiddenWriteError
Can copy from a word to a word.
| word source : 0
| word dest
|
| define main routine
| inputs source
| outputs dest
| trashes a, z, n
| {
| copy source, dest
| }
= ok
Can't copy from a byte to a word.
| byte source : 0
| word dest
|
| define main routine
| inputs source
| outputs dest
| trashes a, z, n
| {
| copy source, dest
| }
? TypeMismatchError
Can't copy from a word to a byte.
| word source : 0
| byte dest
|
| define main routine
| inputs source
| outputs dest
| trashes a, z, n
| {
| copy source, dest
| }
? TypeMismatchError
point ... into blocks
Pointer must be a pointer type.
| byte table[256] tab
| word ptr
|
| define main routine
| inputs tab
| outputs y, tab
| trashes a, z, n, ptr
| {
| ld y, 0
| point ptr into tab {
| reset ptr 0
| copy 123, [ptr] + y
| }
| }
? TypeMismatchError
Cannot write through pointer outside a point ... into block.
| byte table[256] tab
| pointer ptr
|
| define main routine
| inputs tab, ptr
| outputs y, tab
| trashes a, z, n, ptr
| {
| ld y, 0
| copy 123, [ptr] + y
| }
? ForbiddenWriteError
After a point ... into block, the pointer is no longer meaningful.
| byte table[256] tab
| pointer ptr
|
| define main routine
| inputs tab
| outputs y, tab
| trashes a, z, n, ptr
| {
| ld y, 0
| point ptr into tab {
| reset ptr 0
| copy 123, [ptr] + y
| }
| copy 123, [ptr] + y
| }
? UnmeaningfulReadError: ptr
Write literal through a pointer into a table.
| byte table[256] tab
| pointer ptr
|
| define main routine
| inputs tab
| outputs y, tab
| trashes a, z, n, ptr
| {
| ld y, 0
| point ptr into tab {
| reset ptr 0
| copy 123, [ptr] + y
| }
| }
= ok
Writing into a table via a pointer does use y.
| byte table[256] tab
| pointer ptr
|
| define main routine
| inputs tab
| outputs tab
| trashes a, z, n, ptr
| {
| point ptr into tab {
| reset ptr 0
| copy 123, [ptr] + y
| }
| }
? UnmeaningfulReadError
Write stored value through a pointer into a table.
| byte table[256] tab
| pointer ptr
| byte foo
|
| define main routine
| inputs foo, tab
| outputs y, tab
| trashes a, z, n, ptr
| {
| ld y, 0
| point ptr into tab {
| reset ptr 0
| copy foo, [ptr] + y
| }
| }
= ok
Read a table entry via a pointer.
| byte table[256] tab
| pointer ptr
| byte foo
|
| define main routine
| inputs tab
| outputs foo
| trashes a, y, z, n, ptr
| {
| ld y, 0
| point ptr into tab {
| reset ptr 0
| copy [ptr] + y, foo
| }
| }
= ok
Read and write through two pointers into a table.
| byte table[256] tab
| pointer ptra
| pointer ptrb
|
| define main routine
| inputs tab
| outputs tab
| trashes a, y, z, n, ptra, ptrb
| {
| ld y, 0
| point ptra into tab {
| reset ptra 0
| point ptrb into tab {
| reset ptrb 0
| copy [ptra] + y, [ptrb] + y
| }
| }
| }
= ok
Read through a pointer into a table, to the a register. Note that this is done with ld,
not copy.
| byte table[256] tab
| pointer ptr
| byte foo
|
| define main routine
| inputs tab
| outputs a
| trashes y, z, n, ptr
| {
| ld y, 0
| point ptr into tab {
| reset ptr 0
| ld a, [ptr] + y
| }
| }
= ok
Write the a register through a pointer into a table. Note that this is done with st,
not copy.
| byte table[256] tab
| pointer ptr
| byte foo
|
| define main routine
| inputs tab
| outputs tab
| trashes a, y, z, n, ptr
| {
| ld y, 0
| point ptr into tab {
| reset ptr 0
| ld a, 255
| st a, [ptr] + y
| }
| }
= ok
Cannot get a pointer into a non-byte (for instance, word) table.
| word table[256] tab
| pointer ptr
| byte foo
|
| define main routine
| inputs tab
| outputs foo
| trashes a, y, z, n, ptr
| {
| ld y, 0
| point ptr into tab {
| reset ptr 0
| copy [ptr] + y, foo
| }
| }
? TypeMismatchError
Cannot get a pointer into a non-byte (for instance, vector) table.
| vector (routine trashes a, z, n) table[256] tab
| pointer ptr
| vector (routine trashes a, z, n) foo
|
| define main routine
| inputs tab
| outputs foo
| trashes a, y, z, n, ptr
| {
| ld y, 0
| point ptr into tab {
| reset ptr 0
| copy [ptr] + y, foo
| }
| }
? TypeMismatchError
point into by itself only requires ptr to be writeable. By itself,
it does not require tab to be readable or writeable.
| byte table[256] tab
| pointer ptr
|
| define main routine
| trashes a, z, n, ptr
| {
| point ptr into tab {
| ld a, 0
| }
| }
= ok
| byte table[256] tab
| pointer ptr
|
| define main routine
| trashes a, z, n
| {
| point ptr into tab {
| ld a, 0
| }
| }
= ok
It does need to be accessible by the routine if you're going to reset the pointer to it though.
| byte table[256] tab
| pointer ptr
|
| define main routine
| trashes a, z, n
| {
| point ptr into tab {
| reset ptr 0
| ld a, 0
| }
| }
? UnmeaningfulReadError: tab
And the pointer needs to be writeable if it's going to be reset as well.
| byte table[256] tab
| pointer ptr
|
| define main routine
| inputs tab
| trashes a, z, n
| {
| point ptr into tab {
| reset ptr 0
| ld a, 0
| }
| }
? ForbiddenWriteError
After a point into block, the pointer is no longer meaningful and cannot
be considered an output of the routine.
| byte table[256] tab
| pointer ptr
|
| define main routine
| inputs tab
| outputs y, tab, ptr
| trashes a, z, n
| {
| ld y, 0
| point ptr into tab {
| reset ptr 0
| copy 123, [ptr] + y
| }
| }
? UnmeaningfulOutputError
If code in a routine reads from a table through a pointer, the table must be in
the inputs of that routine.
| byte table[256] tab
| pointer ptr
| byte foo
|
| define main routine
| outputs foo
| trashes a, y, z, n, ptr
| {
| ld y, 0
| point ptr into tab {
| reset ptr 0
| copy [ptr] + y, foo
| }
| }
? UnmeaningfulReadError
Likewise, if code in a routine writes into a table via a pointer, the table must
be in the outputs of that routine.
| byte table[256] tab
| pointer ptr
|
| define main routine
| inputs tab
| trashes a, y, z, n, ptr
| {
| ld y, 0
| point ptr into tab {
| reset ptr 0
| copy 123, [ptr] + y
| }
| }
? ForbiddenWriteError
If code in a routine reads from a table through a pointer, the pointer should remain inside the range of the table. This is currently not checked.
| byte table[32] tab
| pointer ptr
| byte foo
|
| define main routine
| inputs tab
| outputs foo
| trashes a, y, c, z, n, v, ptr
| {
| ld y, 0
| point ptr into tab {
| reset ptr 0
| st off, c
| add ptr, word 100
| copy [ptr] + y, foo
| }
| }
= ok
Likewise, if code in a routine writes into a table through a pointer, the pointer should remain inside the range of the table. This is currently not checked.
| byte table[32] tab
| pointer ptr
|
| define main routine
| inputs tab
| outputs tab
| trashes a, y, c, z, n, v, ptr
| {
| ld y, 0
| point ptr into tab {
| reset ptr 0
| st off, c
| add ptr, word 100
| copy 123, [ptr] + y
| }
| }
= ok
reset
Can't have a reset outside a point ... into block.
| byte table[32] tab
| pointer ptr
|
| define main routine
| inputs tab
| outputs tab
| trashes a, y, c, z, n, v, ptr
| {
| ld y, 0
| reset ptr 0
| point ptr into tab {
| st off, c
| add ptr, word 10
| copy 123, [ptr] + y
| }
| }
? ForbiddenWriteError: ptr
Can't write into a table if the pointer hasn't been reset; the
pointer is not meaningful until it's reset.
| byte table[32] tab
| pointer ptr
|
| define main routine
| inputs tab
| outputs tab
| trashes a, y, c, z, n, v, ptr
| {
| ld y, 0
| point ptr into tab {
| st off, c
| copy 123, [ptr] + y
| }
| }
? UnmeaningfulReadError: ptr
Can't read from a table if the pointer hasn't been reset.
| byte table[32] tab
| pointer ptr
| byte ou
|
| define main routine
| inputs tab
| outputs tab, ou
| trashes a, y, c, z, n, v, ptr
| {
| ld y, 0
| point ptr into tab {
| st off, c
| copy [ptr] + y, ou
| }
| }
? UnmeaningfulReadError: ptr
Multiple resets may occur inside the same block.
| byte table[32] tab
| pointer ptr
|
| define main routine
| inputs tab
| outputs tab
| trashes a, y, c, z, n, v, ptr
| {
| ld y, 0
| point ptr into tab {
| reset ptr 10
| copy 123, [ptr] + y
| reset ptr 20
| copy 35, [ptr] + y
| }
| }
= ok
The offset in reset may not exceed the table's size.
| byte table[32] tab
| pointer ptr
|
| define main routine
| inputs tab
| outputs tab
| trashes a, y, c, z, n, v, ptr
| {
| ld y, 0
| point ptr into tab {
| reset ptr 32
| copy 123, [ptr] + y
| }
| }
? RangeExceededError
dynamic recurrence of point ... into blocks
You cannot call a routine which trashes the pointer from inside a
point ... into block. Remember that point ... into by
itself doesn't change anything, so doesn't trash anything.
| byte table[256] tab
| byte table[256] other
| pointer ptr
|
| define sub routine
| inputs other
| outputs other
| {
| point ptr into other {
| }
| }
|
| define main routine
| inputs tab, other
| outputs tab, other
| trashes a, y, c, z, n, v, ptr
| {
| ld y, 0
| point ptr into tab {
| reset ptr 0
| copy 123, [ptr] + y
| call sub
| copy 123, [ptr] + y
| }
| }
= ok
| byte table[256] tab
| byte table[256] other
| pointer ptr
|
| define sub routine
| inputs other
| outputs other
| trashes ptr
| {
| point ptr into other {
| reset ptr 0
| }
| }
|
| define main routine
| inputs tab, other
| outputs tab, other
| trashes a, y, c, z, n, v, ptr
| {
| ld y, 0
| point ptr into tab {
| reset ptr 0
| copy 123, [ptr] + y
| call sub
| copy 123, [ptr] + y
| }
| }
? UnmeaningfulReadError
locals
When memory locations are defined static to a routine, they cannot be directly input, nor directly output; and since they are always initialized, they cannot be trashed. Thus, they really don't participate in the analysis.
| define foo routine
| inputs x
| outputs x
| trashes z, n
| static byte t : 0
| {
| st x, t
| inc t
| ld x, t
| }
|
| define main routine
| trashes a, x, z, n
| static byte t : 0
| {
| ld x, t
| call foo
| }
= ok
When memory locations are defined local to a routine, but not static, they cannot be directly input, nor directly output; but they are considered uninitialized from the time the routine is called to until a value is stored in them.
| define main routine
| inputs x
| outputs x
| trashes z, n
| local byte t
| {
| st x, t
| inc t
| ld x, t
| }
= ok
| define main routine
| outputs x
| trashes z, n
| local byte t
| {
| inc t
| ld x, t
| }
? UnmeaningfulReadError: t
Local non-statics can be meaningully given an explicit address.
| define main routine
| inputs x
| outputs x
| trashes z, n
| local byte t @ 1024
| {
| st x, t
| inc t
| ld x, t
| }
= ok
| define main routine
| outputs x
| trashes z, n
| local byte t @ 1024
| {
| inc t
| ld x, t
| }
? UnmeaningfulReadError: t
save
Basic neutral test, where the save makes no difference.
| define main routine
| inputs a, x
| outputs a, x
| trashes z, n
| {
| ld a, 1
| save x {
| ld a, 2
| }
| ld a, 3
| }
= ok
Saving any location (other than a) will trash a.
| define main routine
| inputs a, x
| outputs a, x
| trashes z, n
| {
| ld a, 1
| save x {
| ld a, 2
| }
| }
? UnmeaningfulOutputError
Saving a does not trash anything.
| define main routine
| inputs a, x
| outputs a, x
| trashes z, n
| {
| ld x, 1
| save a {
| ld x, 2
| }
| ld x, 3
| }
= ok
A defined value that has been saved can be trashed inside the block. It will continue to be defined outside the block.
| define main routine
| outputs x, y
| trashes a, z, n
| {
| ld x, 0
| save x {
| ld y, 0
| trash x
| }
| }
= ok
A trashed value that has been saved can be used inside the block. It will continue to be trashed outside the block.
(Note, both x and a are unmeaningful in this test.)
| define main routine
| inputs a
| outputs a, x
| trashes z, n
| {
| ld x, 0
| trash x
| save x {
| ld a, 0
| ld x, 1
| }
| }
? UnmeaningfulOutputError
The known range of a value will be preserved outside the block as well.
| word one: 77
| word table[32] many
|
| define main routine
| inputs a, many, one
| outputs many, one
| trashes a, x, n, z
| {
| and a, 31
| ld x, a
| save x {
| ld x, 255
| }
| copy one, many + x
| copy many + x, one
| }
= ok
| word one: 77
| word table[32] many
|
| define main routine
| inputs a, many, one
| outputs many, one
| trashes a, x, n, z
| {
| and a, 63
| ld x, a
| save x {
| ld x, 1
| }
| copy one, many + x
| copy many + x, one
| }
? RangeExceededError
The known properties of a value are preserved inside the block, too.
| word one: 77
| word table[32] many
|
| define main routine
| inputs a, many, one
| outputs many, one
| trashes a, x, n, z
| {
| and a, 31
| ld x, a
| save x {
| copy one, many + x
| copy many + x, one
| }
| copy one, many + x
| copy many + x, one
| }
= ok
A value which is not output from the routine, is preserved by the
routine; and can appear in a save exactly because a save preserves it.
| define main routine
| outputs y
| trashes a, z, n
| {
| save x {
| ld y, 0
| ld x, 1
| }
| }
= ok
Because saving anything except a trashes a, a common idiom is to save a
first in a nested series of saves.
| define main routine
| inputs a
| outputs a
| trashes z, n
| {
| save a {
| save x {
| ld a, 0
| ld x, 1
| }
| }
| }
= ok
There is a shortcut syntax for a nested series of saves.
| define main routine
| inputs a
| outputs a
| trashes z, n
| {
| save a, x {
| ld a, 0
| ld x, 1
| }
| }
= ok
a is only preserved if it is the outermost thing saved.
| define main routine
| inputs a
| outputs a
| trashes z, n
| {
| save x, a {
| ld a, 0
| ld x, 1
| }
| }
? UnmeaningfulOutputError: a
Not just registers, but also user-defined locations can be saved.
| byte foo
|
| define main routine
| trashes a, z, n
| {
| save foo {
| st 5, foo
| }
| }
= ok
But only if they are bytes.
| word foo
|
| define main routine
| trashes a, z, n
| {
| save foo {
| copy 555, foo
| }
| }
? TypeMismatchError
| byte table[16] tab
|
| define main routine
| trashes a, y, z, n
| {
| save tab {
| ld y, 0
| st 5, tab + y
| }
| }
? TypeMismatchError
A goto cannot appear within a save block.
| define other routine
| trashes a, z, n
| {
| ld a, 0
| }
|
| define main routine
| trashes a, z, n
| {
| ld a, 1
| save x {
| ld x, 2
| goto other
| }
| }
? IllegalJumpError