XXIIVV

Using program validation in Uxntal.

Type inference in Uxntal is done by checking the stack effect notation of words, against the sum of stack changes predicted to occur based on the items in their bodies.

Words that do not pass the stack-checker are generating a warning, and so essentially this defines a very basic and permissive type system that nevertheless catches some invalid programs and enables compiler optimizations. 

@routine ( a b -: c ) Ok.
	MUL
JMP2r

The simplest case is when a piece of code does not have any branches or recursion, and merely pushes literals and calls words. Pushing a literal has stack effect ( -- x ). The stack effect of most words is always known statically from the declaration.

@add ( a* b* -- c* ) Warning: Imbalance in @add of +2
	DUP2 ADD2
JMP2r

Branch Validation

A word calling a subroutine that would force an exit of the parent routine with an imbalanced stack also triggers an error.

@routine ( a b -: c ) Warning: Imbalance in @routine of +1
	EQUk ?&sub-routine
	POP2 #0a JMP2r
	&sub-routine ( a b -: c* )
		POP2 #000b JMP2r

Return-Stack Passing

The following example shows some extra syntax where stack elements passed through the return stack are separated with a pipe:

@wcpy ( src* des* -: cap* ) Ok.
	STH2
	&w ( src* `des* -: cap* )
		LDAk STH2kr STA
		INC2r INC2 LDAk #20 GTH ?&w
	POP2
	( cap ) #00 STH2kr STA
	INC2r STH2r JMP2r

Each jump label must be defined for a routine's body to validate with the arity checker, but labels can also be used anywhere in a routine to test against a specific arity in time, like you would a breakpoint.

Fall-through Type

The fall-through comment allows to validate a tail-less routine(or, that does not return or break), by including the stack effect of the following routine in memory.

@falling ( a b c -: c ) Ok.
	POP
	( >> )
@next-routine ( a b -: res )
	ADD
JMP2r

More research has to be done in this space, but it would be interesting to check a routine's side-effects by making sure that no ST/LD/DE opcodes can be reached.

Runtime Validation

Lastly, a runtime specific solution to validate the stack state at any one point during the execution of a program, is to read the System/wst port and compare it against a given stack pointer byte value. Note: that the value in the wst and rst ports include the stack pointer byte.

@on-reset ( -> )
	#abcd DUP2 
	.System/wst DEI #05 EQU ?{
		#01 .System/debug DEO
		}
	BRK

incoming uxntal notation uxntal stacks