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