SixtyPical/tests/SixtyPical Analysis.md

SixtyPical Analysis
===================

This is a test suite, written in [Falderal][] format, for the SixtyPical
static analysis rules.

[Falderal]:     http://catseye.tc/node/Falderal

    -> Functionality "Analyze SixtyPical program" is implemented by
    -> shell command "bin/sixtypical --analyze --traceback %(test-body-file) && echo ok"

    -> Tests for functionality "Analyze SixtyPical program"

### Rudiments ###

Routines must declare their inputs, outputs, and memory locations they trash.

    | routine up
    |   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.

    | routine main
    |   outputs a
    |   trashes a
    | {
    |     ld a, 0
    | }
    ? InconsistentConstraintsError: a

If a routine declares it outputs a location, that location should be initialized.

    | routine main
    |   outputs a, x, z, n
    | {
    |     ld x, 0
    | }
    ? UnmeaningfulOutputError: a in main

    | routine main
    |   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.

    | routine main
    |   trashes x, z, n
    | {
    |     ld x, 0
    | }
    = ok

    | routine main
    |   trashes x, z, n
    | {
    | }
    = ok

If a routine modifies a location, it needs to either output it or trash it.

    | routine main
    | {
    |     ld x, 0
    | }
    ? ForbiddenWriteError: x in main

    | routine main
    |   outputs x, z, n
    | {
    |     ld x, 0
    | }
    = ok

    | routine main
    |   trashes x, z, n
    | {
    |     ld x, 0
    | }
    = ok

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
    | 
    | routine main
    |   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.

    | routine main
    |   inputs a, x
    |   trashes a, z, n
    | {
    |     ld a, x
    | }
    = ok

    | routine main
    |   inputs a
    |   trashes a
    | {
    |     ld a, x
    | }
    ? UnmeaningfulReadError: x in main

Can't `ld` to a memory location that doesn't appear in (outputs ∪ trashes).

    | routine main
    |   trashes a, z, n
    | {
    |     ld a, 0
    | }
    = ok

    | routine main
    |   outputs a
    |   trashes z, n
    | {
    |     ld a, 0
    | }
    = ok

    | routine main
    |   outputs z, n
    |   trashes a
    | {
    |     ld a, 0
    | }
    = ok

    | routine main
    |   trashes z, n
    | {
    |     ld a, 0
    | }
    ? ForbiddenWriteError: a in main

    | routine main
    |   trashes a, n
    | {
    |     ld a, 0
    | }
    ? ForbiddenWriteError: z in main

Can't `ld` a `word` type.

    | word foo
    | 
    | routine main
    |   inputs foo
    |   trashes a, n, z
    | {
    |     ld a, foo
    | }
    ? TypeMismatchError: foo and a in main

### st ###

Can't `st` from a memory location that isn't initialized.

    | byte lives
    | routine main
    |   inputs x
    |   trashes lives
    | {
    |     st x, lives
    | }
    = ok

    | byte lives
    | routine main
    |   trashes x, lives
    | {
    |     st x, lives
    | }
    ? UnmeaningfulReadError: x in main

Can't `st` to a memory location that doesn't appear in (outputs ∪ trashes).

    | byte lives
    | routine main
    |   trashes lives
    | {
    |     st 0, lives
    | }
    = ok

    | byte lives
    | routine main
    |   outputs lives
    | {
    |     st 0, lives
    | }
    = ok

    | byte lives
    | routine main
    |   inputs lives
    | {
    |     st 0, lives
    | }
    ? ForbiddenWriteError: lives in main

Can't `st` a `word` type.

    | word foo
    | 
    | routine main
    |   outputs foo
    |   trashes a, n, z
    | {
    |     ld a, 0
    |     st a, foo
    | }
    ? TypeMismatchError: a and foo in main

### tables ###

Storing to a table, you must use an index.

    | byte one
    | byte table[256] many
    | 
    | routine main
    |   outputs one
    |   trashes a, x, n, z
    | {
    |     ld x, 0
    |     ld a, 0
    |     st a, one
    | }
    = ok

    | byte one
    | byte table[256] many
    | 
    | routine main
    |   outputs many
    |   trashes a, x, n, z
    | {
    |     ld x, 0
    |     ld a, 0
    |     st a, many
    | }
    ? TypeMismatchError

    | byte one
    | byte table[256] many
    | 
    | routine main
    |   outputs one
    |   trashes a, x, n, z
    | {
    |     ld x, 0
    |     ld a, 0
    |     st a, one + x
    | }
    ? TypeMismatchError

    | byte one
    | byte table[256] many
    | 
    | routine main
    |   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
    | 
    | routine main
    |   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
    | 
    | routine main
    |   outputs one
    |   trashes a, x, n, z
    | {
    |     ld x, 0
    |     st x, one
    |     ld a, one
    | }
    = ok

    | byte one
    | 
    | routine main
    |   outputs one
    |   trashes a, x, n, z
    | {
    |     ld x, 0
    |     st x, one
    |     ld a, one + x
    | }
    ? TypeMismatchError

    | byte table[256] many
    | 
    | routine main
    |   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
    | 
    | routine main
    |   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
    | 
    | routine main
    |   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
    | 
    | routine main
    |   inputs many
    |   outputs many
    |   trashes a, x, n, z
    | {
    |     ld a, many + x
    | }
    ? UnmeaningfulReadError: x

Copying to and from a word table.

    | word one
    | word table[256] many
    | 
    | routine main
    |   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
    | 
    | routine main
    |   inputs one, many
    |   outputs one, many
    |   trashes a, x, n, z
    | {
    |     ld x, 0
    |     copy one, many
    | }
    ? TypeMismatchError

    | word one
    | word table[256] many
    | 
    | routine main
    |   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.

    | word table[256] many
    | 
    | routine main
    |   inputs many
    |   outputs many
    |   trashes a, x, n, z
    | {
    |     ld x, 0
    |     copy 9999, many + x
    | }
    = ok

### add ###

Can't `add` from or to a memory location that isn't initialized.

    | routine main
    |   inputs a
    |   outputs a
    |   trashes c, z, v, n
    | {
    |     st off, c
    |     add a, 0
    | }
    = ok

    | byte lives
    | routine main
    |   inputs a
    |   outputs a
    |   trashes c, z, v, n
    | {
    |     st off, c
    |     add a, lives
    | }
    ? UnmeaningfulReadError: lives in main

    | byte lives
    | routine main
    |   inputs lives
    |   outputs a
    |   trashes c, z, v, n
    | {
    |     st off, c
    |     add a, lives
    | }
    ? UnmeaningfulReadError: a in main

Can't `add` to a memory location that isn't writeable.

    | routine main
    |   inputs a
    |   trashes c
    | {
    |     st off, c
    |     add a, 0
    | }
    ? ForbiddenWriteError: a in main

You can `add` a word constant to a word memory location.

    | word score
    | routine main
    |   inputs a, score
    |   outputs score
    |   trashes a, c, z, v, n
    | {
    |     st off, c
    |     add score, 1999
    | }
    = ok

`add`ing a word constant to a word memory location trashes `a`.

    | word score
    | routine main
    |   inputs a, score
    |   outputs score, a
    |   trashes c, z, v, n
    | {
    |     st off, c
    |     add score, 1999
    | }
    ? UnmeaningfulOutputError: a in main

To be sure, `add`ing a word constant to a word memory location trashes `a`.

    | word score
    | routine main
    |   inputs score
    |   outputs score
    |   trashes c, z, v, n
    | {
    |     st off, c
    |     add score, 1999
    | }
    ? ForbiddenWriteError: a in main

You can `add` a word memory location to another word memory location.

    | word score
    | word delta
    | routine main
    |   inputs score, delta
    |   outputs score
    |   trashes a, c, z, v, n
    | {
    |     st off, c
    |     add score, delta
    | }
    = ok

`add`ing a word memory location to a word memory location trashes `a`.

    | word score
    | word delta
    | routine main
    |   inputs score, delta
    |   outputs score
    |   trashes c, z, v, n
    | {
    |     st off, c
    |     add score, delta
    | }
    ? ForbiddenWriteError: a in main

You can `add` a word memory location, or a constant, to a pointer.

    | pointer ptr
    | word delta
    | routine main
    |   inputs ptr, delta
    |   outputs ptr
    |   trashes a, c, z, v, n
    | {
    |     st off, c
    |     add ptr, delta
    |     add ptr, word 1
    | }
    = ok

`add`ing a word memory location, or a constant, to a pointer, trashes `a`.

    | pointer ptr
    | word delta
    | routine main
    |   inputs ptr, delta
    |   outputs ptr
    |   trashes c, z, v, n
    | {
    |     st off, c
    |     add ptr, delta
    |     add ptr, word 1
    | }
    ? ForbiddenWriteError: a in main

### sub ###

Can't `sub` from or to a memory location that isn't initialized.

    | routine main
    |   inputs a
    |   outputs a
    |   trashes c, z, v, n
    | {
    |     st off, c
    |     sub a, 0
    | }
    = ok

    | byte lives
    | routine main
    |   inputs a
    |   outputs a
    |   trashes c, z, v, n
    | {
    |     st off, c
    |     sub a, lives
    | }
    ? UnmeaningfulReadError: lives in main

    | byte lives
    | routine main
    |   inputs lives
    |   outputs a
    |   trashes c, z, v, n
    | {
    |     st off, c
    |     sub a, lives
    | }
    ? UnmeaningfulReadError: a in main

Can't `sub` to a memory location that isn't writeable.

    | routine main
    |   inputs a
    |   trashes c
    | {
    |     st off, c
    |     sub a, 0
    | }
    ? ForbiddenWriteError: a in main

You can `sub` a word constant from a word memory location.

    | word score
    | routine main
    |   inputs a, score
    |   outputs score
    |   trashes a, c, z, v, n
    | {
    |     st on, c
    |     sub score, 1999
    | }
    = ok

`sub`ing a word constant from a word memory location trashes `a`.

    | word score
    | routine main
    |   inputs a, score
    |   outputs score, a
    |   trashes c, z, v, n
    | {
    |     st on, c
    |     sub score, 1999
    | }
    ? UnmeaningfulOutputError: a in main

You can `sub` a word memory location from another word memory location.

    | word score
    | word delta
    | routine main
    |   inputs score, delta
    |   outputs score
    |   trashes a, c, z, v, n
    | {
    |     st off, c
    |     sub score, delta
    | }
    = ok

`sub`ing a word memory location from a word memory location trashes `a`.

    | word score
    | word delta
    | routine main
    |   inputs score, delta
    |   outputs score
    |   trashes c, z, v, n
    | {
    |     st off, c
    |     sub score, delta
    | }
    ? ForbiddenWriteError: a in main

### inc ###

Location must be initialized and writeable.

    | routine main
    |   outputs x
    |   trashes z, n
    | {
    |     inc x
    | }
    ? UnmeaningfulReadError: x in main

    | routine main
    |   inputs x
    |   trashes z, n
    | {
    |     inc x
    | }
    ? ForbiddenWriteError: x in main

    | routine main
    |   inputs x
    |   outputs x
    |   trashes z, n
    | {
    |     inc x
    | }
    = ok

Can't `inc` a `word` type.

    | word foo
    | 
    | routine main
    |   inputs foo
    |   outputs foo
    |   trashes z, n
    | {
    |     inc foo
    | }
    ? TypeMismatchError: foo in main

### dec ###

Location must be initialized and writeable.

    | routine main
    |   outputs x
    |   trashes z, n
    | {
    |     dec x
    | }
    ? UnmeaningfulReadError: x in main

    | routine main
    |   inputs x
    |   trashes z, n
    | {
    |     dec x
    | }
    ? ForbiddenWriteError: x in main

    | routine main
    |   inputs x
    |   outputs x
    |   trashes z, n
    | {
    |     dec x
    | }
    = ok

Can't `dec` a `word` type.

    | word foo
    | 
    | routine main
    |   inputs foo
    |   outputs foo
    |   trashes z, n
    | {
    |     dec foo
    | }
    ? TypeMismatchError: foo in main

### cmp ###

Some rudimentary tests for cmp.

    | routine main
    |   inputs a
    |   trashes z, c, n
    | {
    |     cmp a, 4
    | }
    = ok

    | routine main
    |   inputs a
    |   trashes z, n
    | {
    |     cmp a, 4
    | }
    ? ForbiddenWriteError: c in main

    | routine main
    |   trashes z, c, n
    | {
    |     cmp a, 4
    | }
    ? UnmeaningfulReadError: a in main

### and ###

Some rudimentary tests for and.

    | routine main
    |   inputs a
    |   outputs a, z, n
    | {
    |     and a, 4
    | }
    = ok

    | routine main
    |   inputs a
    |   trashes z, n
    | {
    |     and a, 4
    | }
    ? ForbiddenWriteError: a in main

    | routine main
    |   trashes z, n
    | {
    |     and a, 4
    | }
    ? UnmeaningfulReadError: a in main

### or ###

Writing unit tests on a train.  Wow.

    | routine main
    |   inputs a
    |   outputs a, z, n
    | {
    |     or a, 4
    | }
    = ok

    | routine main
    |   inputs a
    |   trashes z, n
    | {
    |     or a, 4
    | }
    ? ForbiddenWriteError: a in main

    | routine main
    |   trashes z, n
    | {
    |     or a, 4
    | }
    ? UnmeaningfulReadError: a in main

### xor ###

Writing unit tests on a train.  Wow.

    | routine main
    |   inputs a
    |   outputs a, z, n
    | {
    |     xor a, 4
    | }
    = ok

    | routine main
    |   inputs a
    |   trashes z, n
    | {
    |     xor a, 4
    | }
    ? ForbiddenWriteError: a in main

    | routine main
    |   trashes z, n
    | {
    |     xor a, 4
    | }
    ? UnmeaningfulReadError: a in main

### shl ###

Some rudimentary tests for shl.

    | routine main
    |   inputs a, c
    |   outputs a, c, z, n
    | {
    |     shl a
    | }
    = ok

    | routine main
    |   inputs a, c
    |   outputs c, z, n
    | {
    |     shl a
    | }
    ? ForbiddenWriteError: a in main

    | routine main
    |   inputs a
    |   outputs a, c, z, n
    | {
    |     shl a
    | }
    ? UnmeaningfulReadError: c in main

### shr ###

Some rudimentary tests for shr.

    | routine main
    |   inputs a, c
    |   outputs a, c, z, n
    | {
    |     shr a
    | }
    = ok

    | routine main
    |   inputs a, c
    |   outputs c, z, n
    | {
    |     shr a
    | }
    ? ForbiddenWriteError: a in main

    | routine main
    |   inputs a
    |   outputs a, c, z, n
    | {
    |     shr a
    | }
    ? UnmeaningfulReadError: c in main

### call ###

When calling a routine, all of the locations it lists as inputs must be
initialized.

    | byte lives
    | 
    | routine foo
    |   inputs x
    |   trashes lives
    | {
    |     st x, lives
    | }
    | 
    | routine main
    | {
    |     call foo
    | }
    ? UnmeaningfulReadError: x in main

Note that if you call a routine that trashes a location, you also trash it.

    | byte lives
    | 
    | routine foo
    |   inputs x
    |   trashes lives
    | {
    |     st x, lives
    | }
    | 
    | routine main
    |   outputs x, z, n
    | {
    |     ld x, 0
    |     call foo
    | }
    ? ForbiddenWriteError: lives in main

    | byte lives
    | 
    | routine foo
    |   inputs x
    |   trashes lives
    | {
    |     st x, lives
    | }
    | 
    | routine main
    |   outputs x, z, n
    |   trashes lives
    | {
    |     ld x, 0
    |     call foo
    | }
    = ok

You can't output a value that the thing you called trashed.

    | byte lives
    | 
    | routine foo
    |   inputs x
    |   trashes lives
    | {
    |     st x, lives
    | }
    | 
    | routine main
    |   outputs x, z, n, lives
    | {
    |     ld x, 0
    |     call foo
    | }
    ? UnmeaningfulOutputError: lives in main

...unless you write to it yourself afterwards.

    | byte lives
    | 
    | routine foo
    |   inputs x
    |   trashes lives
    | {
    |     st x, lives
    | }
    | 
    | routine main
    |   outputs x, z, n, lives
    | {
    |     ld x, 0
    |     call foo
    |     st x, lives
    | }
    = ok

If a routine declares outputs, they are initialized in the caller after
calling it.

    | routine foo
    |   outputs x, z, n
    | {
    |     ld x, 0
    | }
    | 
    | routine main
    |   outputs a
    |   trashes x, z, n
    | {
    |     call foo
    |     ld a, x
    | }
    = ok

    | routine foo
    | {
    | }
    | 
    | routine main
    |   outputs a
    |   trashes x
    | {
    |     call foo
    |     ld a, x
    | }
    ? UnmeaningfulReadError: x in main

If a routine trashes locations, they are uninitialized in the caller after
calling it.

    | routine foo
    |   trashes x, z, n
    | {
    |     ld x, 0
    | }
    = ok

    | routine foo
    |   trashes x, z, n
    | {
    |     ld x, 0
    | }
    | 
    | routine main
    |   outputs a
    |   trashes x, z, n
    | {
    |     call foo
    |     ld a, x
    | }
    ? UnmeaningfulReadError: x in main

Calling an extern is just the same as calling a defined routine with the
same constraints.

    | routine chrout
    |   inputs a
    |   trashes a
    |   @ 65490
    | 
    | routine main
    |   trashes a, z, n
    | {
    |     ld a, 65
    |     call chrout
    | }
    = ok

    | routine chrout
    |   inputs a
    |   trashes a
    |   @ 65490
    | 
    | routine main
    |   trashes a, z, n
    | {
    |     call chrout
    | }
    ? UnmeaningfulReadError: a in main

    | routine chrout
    |   inputs a
    |   trashes a
    |   @ 65490
    | 
    | routine main
    |   trashes a, x, z, n
    | {
    |     ld a, 65
    |     call chrout
    |     ld x, a
    | }
    ? UnmeaningfulReadError: a in main

### trash ###

Trash does nothing except indicate that we do not care about the value anymore.

    | routine foo
    |   inputs a
    |   outputs x
    |   trashes a, z, n
    | {
    |     st a, x
    |     ld a, 0
    |     trash a
    | }
    = ok

    | routine foo
    |   inputs a
    |   outputs a, x
    |   trashes z, n
    | {
    |     st a, x
    |     ld a, 0
    |     trash a
    | }
    ? UnmeaningfulOutputError: a in foo

    | routine foo
    |   inputs a
    |   outputs x
    |   trashes a, z, n
    | {
    |     st a, x
    |     trash a
    |     st a, x
    | }
    ? UnmeaningfulReadError: a in foo

### if ###

Both blocks of an `if` are analyzed.

    | routine foo
    |   inputs a
    |   outputs x
    |   trashes a, z, n, c
    | {
    |     cmp a, 42
    |     if z {
    |         ld x, 7
    |     } else {
    |         ld x, 23
    |     }
    | }
    = ok

If a location is initialized in one block, is must be initialized in the other as well.

    | routine foo
    |   inputs a
    |   outputs x
    |   trashes a, z, n, c
    | {
    |     cmp a, 42
    |     if z {
    |         ld x, 7
    |     } else {
    |         ld a, 23
    |     }
    | }
    ? InconsistentInitializationError: x

    | routine foo
    |   inputs a
    |   outputs x
    |   trashes a, z, n, c
    | {
    |     cmp a, 42
    |     if z {
    |         ld a, 6
    |     } else {
    |         ld x, 7
    |     }
    | }
    ? InconsistentInitializationError: x

    | routine foo
    |   inputs a
    |   outputs x
    |   trashes a, z, n, c
    | {
    |     cmp a, 42
    |     if not z {
    |         ld a, 6
    |     } else {
    |         ld x, 7
    |     }
    | }
    ? InconsistentInitializationError: x

However, this only pertains to initialization.  If a value is already
initialized, either because it was set previous to the `if`, or is an
input to the routine, and it is initialized in one branch, it need not
be initialized in the other.

    | routine foo
    |   inputs x
    |   outputs x
    |   trashes a, z, n, c
    | {
    |     ld a, 0
    |     cmp a, 42
    |     if z {
    |         ld x, 7
    |     } else {
    |         ld a, 23
    |     }
    | }
    = ok

An `if` with a single block is analyzed as if it had an empty `else` block.

    | routine foo
    |   inputs a
    |   outputs x
    |   trashes a, z, n, c
    | {
    |     cmp a, 42
    |     if z {
    |         ld x, 7
    |     }
    | }
    ? InconsistentInitializationError: x

    | routine foo
    |   inputs a
    |   outputs x
    |   trashes a, z, n, c
    | {
    |     ld x, 0
    |     cmp a, 42
    |     if z {
    |         ld x, 7
    |     }
    | }
    = ok

    | routine foo
    |   inputs a
    |   outputs x
    |   trashes a, z, n, c
    | {
    |     ld x, 0
    |     cmp a, 42
    |     if not z {
    |         ld x, 7
    |     }
    | }
    = ok

### repeat ###

Repeat loop.

    | routine main
    |   outputs x, y, n, z, c
    | {
    |     ld x, 0
    |     ld y, 15
    |     repeat {
    |         inc x
    |         inc y
    |         cmp x, 10
    |     } until z
    | }
    = ok

You can initialize something inside the loop that was uninitialized outside.

    | routine main
    |   outputs x, y, n, z, c
    | {
    |     ld x, 0
    |     repeat {
    |         ld y, 15
    |         inc x
    |         cmp x, 10
    |     } until z
    | }
    = ok

But you can't UNinitialize something at the end of the loop that you need
initialized at the start.

    | routine foo
    |   trashes y
    | {
    | }
    | 
    | routine main
    |   outputs x, y, n, z, c
    | {
    |     ld x, 0
    |     ld y, 15
    |     repeat {
    |         inc x
    |         inc y
    |         call foo
    |         cmp x, 10
    |     } until z
    | }
    ? UnmeaningfulReadError: y in main

And if you trash the test expression (i.e. `z` in the below) inside the loop,
this is an error too.

    | word one : 0
    | word two : 0
    | 
    | routine main
    |   inputs one, two
    |   outputs two
    |   trashes a, z, n
    | {
    |     repeat {
    |         copy one, two
    |     } until z
    | }
    ? UnmeaningfulReadError: z in main

The body of `repeat forever` can be empty.

    | routine main
    | {
    |     repeat {
    |     } forever
    | }
    = ok

### copy ###

Can't `copy` from a memory location that isn't initialized.

    | byte lives
    | routine main
    |   inputs x
    |   outputs lives
    |   trashes a, z, n
    | {
    |     copy x, lives
    | }
    = ok

    | byte lives
    | routine main
    |   outputs lives
    |   trashes x, a, z, n
    | {
    |     copy x, lives
    | }
    ? UnmeaningfulReadError: x in main

Can't `copy` to a memory location that doesn't appear in (outputs ∪ trashes).

    | byte lives
    | routine main
    |   trashes lives, a, z, n
    | {
    |     copy 0, lives
    | }
    = ok

    | byte lives
    | routine main
    |   outputs lives
    |   trashes a, z, n
    | {
    |     copy 0, lives
    | }
    = ok

    | byte lives
    | routine main
    |   inputs lives
    |   trashes a, z, n
    | {
    |     copy 0, lives
    | }
    ? ForbiddenWriteError: lives in main

a, z, and n are trashed, and must be declared as such

    | byte lives
    | routine main
    |   outputs lives
    | {
    |     copy 0, lives
    | }
    ? ForbiddenWriteError: n in main

a, z, and n are trashed, and must not be declared as outputs.

    | byte lives
    | routine main
    |   outputs lives, a, z, n
    | {
    |     copy 0, lives
    | }
    ? UnmeaningfulOutputError: n in main

Unless of course you subsequently initialize them.

    | byte lives
    | routine main
    |   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
    | 
    | routine main
    |   inputs source
    |   outputs dest
    |   trashes a, z, n
    | {
    |     copy source, dest
    | }
    = ok

Can `copy` from a `word` to a `word`.

    | word source : 0
    | word dest
    | 
    | routine main
    |   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
    | 
    | routine main
    |   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
    | 
    | routine main
    |   inputs source
    |   outputs dest
    |   trashes a, z, n
    | {
    |     copy source, dest
    | }
    ? TypeMismatchError

### copy[] ###

Buffers and pointers.

Note that `^buf` is a constant value, so it by itself does not require `buf` to be
listed in any input/output sets.

However, if the code reads from it through a pointer, it *should* be in `inputs`.

Likewise, if the code writes to it through a pointer, it *should* be in `outputs`.

Of course, unless you write to *all* the bytes in a buffer, some of those bytes
might not be meaningful.  So how meaningful is this check?

This is an open problem.

For now, convention says: if it is being read, list it in `inputs`, and if it is
being modified, list it in both `inputs` and `outputs`.

Write literal through a pointer.

    | buffer[2048] buf
    | pointer ptr
    | 
    | routine main
    |   inputs buf
    |   outputs y, buf
    |   trashes a, z, n, ptr
    | {
    |     ld y, 0
    |     copy ^buf, ptr
    |     copy 123, [ptr] + y
    | }
    = ok

It does use `y`.

    | buffer[2048] buf
    | pointer ptr
    | 
    | routine main
    |   inputs buf
    |   outputs buf
    |   trashes a, z, n, ptr
    | {
    |     copy ^buf, ptr
    |     copy 123, [ptr] + y
    | }
    ? UnmeaningfulReadError

Write stored value through a pointer.

    | buffer[2048] buf
    | pointer ptr
    | byte foo
    | 
    | routine main
    |   inputs foo, buf
    |   outputs y, buf
    |   trashes a, z, n, ptr
    | {
    |     ld y, 0
    |     copy ^buf, ptr
    |     copy foo, [ptr] + y
    | }
    = ok

Read through a pointer.

    | buffer[2048] buf
    | pointer ptr
    | byte foo
    | 
    | routine main
    |   inputs buf
    |   outputs foo
    |   trashes a, y, z, n, ptr
    | {
    |     ld y, 0
    |     copy ^buf, ptr
    |     copy [ptr] + y, foo
    | }
    = ok

### routines ###

Routines are constants.  You need not, and in fact cannot, specify a constant
as an input to, an output of, or as a trashed value of a routine.

    | vector vec
    |   inputs x
    |   outputs x
    |   trashes z, n
    | 
    | routine foo
    |   inputs x
    |   outputs x
    |   trashes z, n
    | {
    |   inc x
    | }
    | 
    | routine main
    |   inputs foo
    |   outputs vec
    |   trashes a, z, n
    | {
    |     copy foo, vec
    | }
    ? ConstantConstraintError: foo in main

    | vector vec
    |   inputs x
    |   outputs x
    |   trashes z, n
    | 
    | routine foo
    |   inputs x
    |   outputs x
    |   trashes z, n
    | {
    |   inc x
    | }
    | 
    | routine main
    |   outputs vec, foo
    |   trashes a, z, n
    | {
    |     copy foo, vec
    | }
    ? ConstantConstraintError: foo in main

    | vector vec
    |   inputs x
    |   outputs x
    |   trashes z, n
    | 
    | routine foo
    |   inputs x
    |   outputs x
    |   trashes z, n
    | {
    |   inc x
    | }
    | 
    | routine main
    |   outputs vec
    |   trashes a, z, n, foo
    | {
    |     copy foo, vec
    | }
    ? ConstantConstraintError: foo in main

You can copy the address of a routine into a vector, if that vector is
declared appropriately.

    | vector vec
    |   inputs x
    |   outputs x
    |   trashes z, n
    | 
    | routine foo
    |   inputs x
    |   outputs x
    |   trashes z, n
    | {
    |   inc x
    | }
    | 
    | routine main
    |   outputs vec
    |   trashes a, z, n
    | {
    |     copy foo, vec
    | }
    = ok

But not if the vector is declared inappropriately.

    | vector vec
    |   inputs y
    |   outputs y
    |   trashes z, n
    | 
    | routine foo
    |   inputs x
    |   outputs x
    |   trashes z, n
    | {
    |   inc x
    | }
    | 
    | routine main
    |   outputs vec
    |   trashes a, z, n
    | {
    |     copy foo, vec
    | }
    ? IncompatibleConstraintsError

"Appropriately" means, if the routine affects no more than what is named
in the input/output sets of the vector.

    | vector vec
    |   inputs a, x
    |   outputs x
    |   trashes a, z, n
    | 
    | routine foo
    |   inputs x
    |   outputs x
    |   trashes z, n
    | {
    |   inc x
    | }
    | 
    | routine main
    |   outputs vec
    |   trashes a, z, n
    | {
    |     copy foo, vec
    | }
    = ok

Routines are read-only.

    | vector vec
    |   inputs x
    |   outputs x
    |   trashes z, n
    | 
    | routine foo
    |   inputs x
    |   outputs x
    |   trashes z, n
    | {
    |   inc x
    | }
    | 
    | routine main
    |   outputs vec
    |   trashes a, z, n
    | {
    |     copy vec, foo
    | }
    ? TypeMismatchError

Indirect call.

    | vector foo outputs x trashes z, n
    | 
    | routine bar outputs x trashes z, n {
    |     ld x, 200
    | }
    | 
    | routine main outputs x, foo trashes a, z, n {
    |     copy bar, foo
    |     call foo
    | }
    = ok

Calling the vector does indeed trash the things the vector says it does.

    | vector foo trashes x, z, n
    | 
    | routine bar trashes x, z, n {
    |     ld x, 200
    | }
    | 
    | routine main outputs x, foo trashes z, n {
    |     ld x, 0
    |     copy bar, foo
    |     call foo
    | }
    ? UnmeaningfulOutputError: x in main

`goto`, if present, must be in tail position (the final instruction in a routine.)

    | routine bar trashes x, z, n {
    |     ld x, 200
    | }
    | 
    | routine main trashes x, z, n {
    |     ld x, 0
    |     goto bar
    | }
    = ok

    | routine bar trashes x, z, n {
    |     ld x, 200
    | }
    | 
    | routine main trashes x, z, n {
    |     goto bar
    |     ld x, 0
    | }
    ? IllegalJumpError

    | routine bar trashes x, z, n {
    |     ld x, 200
    | }
    | 
    | routine main trashes x, z, n {
    |     ld x, 0
    |     if z {
    |         ld x, 1
    |         goto bar
    |     }
    | }
    = ok

    | routine bar trashes x, z, n {
    |     ld x, 200
    | }
    | 
    | routine main trashes x, z, n {
    |     ld x, 0
    |     if z {
    |         ld x, 1
    |         goto bar
    |     }
    |     ld x, 0
    | }
    ? IllegalJumpError

Can't `goto` a routine that outputs or trashes more than the current routine.

    | routine bar trashes x, y, z, n {
    |     ld x, 200
    |     ld y, 200
    | }
    | 
    | routine main trashes x, z, n {
    |     ld x, 0
    |     goto bar
    | }
    ? IncompatibleConstraintsError

    | routine bar outputs y trashes z, n {
    |     ld y, 200
    | }
    | 
    | routine main trashes x, z, n {
    |     ld x, 0
    |     goto bar
    | }
    ? IncompatibleConstraintsError

Can `goto` a routine that outputs or trashes less than the current routine.

    | routine bar trashes x, z, n {
    |     ld x, 1
    | }
    | 
    | routine main trashes a, x, z, n {
    |     ld a, 0
    |     ld x, 0
    |     goto bar
    | }
    = ok

Indirect goto.

    | vector foo outputs x trashes a, z, n
    | 
    | routine bar outputs x trashes a, z, n {
    |     ld x, 200
    | }
    | 
    | routine main outputs x trashes foo, a, z, n {
    |     copy bar, foo
    |     goto foo
    | }
    = ok

Jumping through the vector does indeed trash, or output, the things the
vector says it does.

    | vector foo
    |   trashes a, x, z, n
    | 
    | routine bar
    |   trashes a, x, z, n {
    |     ld x, 200
    | }
    | 
    | routine sub
    |   trashes foo, a, x, z, n {
    |     ld x, 0
    |     copy bar, foo
    |     goto foo
    | }
    | 
    | routine main
    |   outputs a
    |   trashes foo, x, z, n {
    |     call sub
    |     ld a, x
    | }
    ? UnmeaningfulReadError: x in main

    | vector foo
    |   outputs x
    |   trashes a, z, n
    | 
    | routine bar
    |   outputs x
    |   trashes a, z, n {
    |     ld x, 200
    | }
    | 
    | routine sub
    |   outputs x
    |   trashes foo, a, z, n {
    |     ld x, 0
    |     copy bar, foo
    |     goto foo
    | }
    | 
    | routine main
    |   outputs a
    |   trashes foo, x, z, n {
    |     call sub
    |     ld a, x
    | }
    = ok

### Vector tables ###

A vector can be copied into a vector table.

    | vector one
    |   outputs x
    |   trashes a, z, n
    | vector table[256] many
    |   outputs x
    |   trashes a, z, n
    | 
    | routine bar outputs x trashes a, z, n {
    |     ld x, 200
    | }
    | 
    | routine main
    |   inputs one, many
    |   outputs one, many
    |   trashes a, x, n, z
    | {
    |     ld x, 0
    |     copy bar, one
    |     copy one, many + x
    | }
    = ok

A vector can be copied out of a vector table.

    | vector one
    |   outputs x
    |   trashes a, z, n
    | vector table[256] many
    |   outputs x
    |   trashes a, z, n
    | 
    | routine bar outputs x trashes a, z, n {
    |     ld x, 200
    | }
    | 
    | routine main
    |   inputs one, many
    |   outputs one, many
    |   trashes a, x, n, z
    | {
    |     ld x, 0
    |     copy many + x, one
    |     call one
    | }
    = ok

A routine can be copied into a vector table.

    | vector table[256] many
    |   outputs x
    |   trashes a, z, n
    | 
    | routine bar outputs x trashes a, z, n {
    |     ld x, 200
    | }
    | 
    | routine main
    |   inputs many
    |   outputs many
    |   trashes a, x, n, z
    | {
    |     ld x, 0
    |     copy bar, many + x
    | }
    = ok

A vector in a vector table cannot be directly called.

    | vector table[256] many
    |   outputs x
    |   trashes a, z, n
    | 
    | routine bar outputs x trashes a, z, n {
    |     ld x, 200
    | }
    | 
    | routine main
    |   inputs many
    |   outputs many
    |   trashes a, x, n, z
    | {
    |     ld x, 0
    |     copy bar, many + x
    |     call many + x
    | }
    ? ValueError