6502
/
SixtyPical
mirror of https://github.com/catseye/SixtyPical.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity
SixtyPical/tests/SixtyPical Storage.md

1991 lines
38 KiB
Markdown
Raw Permalink Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

SixtyPical Analysis - Storage
=============================
<!--
Copyright (c) 2014-2024, Chris Pressey, Cat's Eye Technologies.
This file is distributed under a 2-clause BSD license. See LICENSES/ dir.
SPDX-License-Identifier: LicenseRef-BSD-2-Clause-X-SixtyPical
-->
This is a test suite, written in [Falderal][] format, for the SixtyPical
static analysis rules, with regard to storage (load, store, tables, etc.)
[Falderal]: http://catseye.tc/node/Falderal
-> 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 `reset`s 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 `save`s.
| 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 `save`s.
| 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 `save`d.
| 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
Reference in New Issue View Git Blame Copy Permalink