1
0
mirror of https://github.com/catseye/SixtyPical.git synced 2024-11-26 14:49:15 +00:00
SixtyPical/tests/SixtyPical Analysis.md
2017-12-12 16:04:59 +00:00

31 KiB
Raw Blame History

SixtyPical Analysis

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

-> 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, and vice-versa.

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

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

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

Reading from a table, you must use an index, and vice-versa.

| 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 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 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

Copying to and from a word table.

| word one
| word table 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 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 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 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

adding 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, adding 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

adding 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

adding 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

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

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