SixtyPical/tests/SixtyPical Analysis.md

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

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

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

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

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

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

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

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

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

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