Assembly-validator: introduction

The aforementioned assembler can be used to translate assembly-language into machine-code. These machine-code programs can then be run on the CPU.

In case the programmer made a mistake when constructing the assembly-language program, the resulting machine-code program may show different behaviour than expected. Such a mistake is often called a bug.

One method of reducing bugs in programs is to run the corresponding machine-code, and try to understand what causes the unexpected behaviour when it actually happens. This is generally called debugging.

Another method is to describe, in terms of its input and output, what a program should do, and then have the computer check whether the program's behaviour matches these expectations.

This section describes an assembly-validator utility that does exactly this.

Like the assembler, this utility is written in the Tcl programming-language. And like the assembler, the behaviour-descriptions used here are in fact Tcl-code.

General concept

Recall from previous sections that an assembly-macro has zero or more formal arguments.

These arguments basically specify what data goes into the macro, and what comes out. (Furthermore, there may be branch-arguments, discussed later.)

When the behaviour of the macro is fully described in terms of these arguments, the computer can simply try all possible combination of input-arguments, each time verifying that the output-arguments' values match the behaviour-description.

Written in pseudo-code, this looks something like this:

assemble macro to be validated

load resulting machine-code

for each possible combination of input-arguments:        \
                                                          |
    fill in the input-arguments                           |
                                                          |
    run the macro                                         | (*)
                                                          |
    read the output-arguments                             |
                                                          |
    verify behaviour-description for this combination     |
                                                         / 

The following text deals with the steps marked by "*", and ignores the assembly- and load-steps.

Describing a macro's behaviour

In the previous section, the "not1"-macro was introduced, with the goal of inverting a bit:

# Invert a bit.

macro  not1  reg {

            ibc1    $reg    done
    : done
} 

This macro has 1 argument: "reg", the bit to be inverted.

The behaviour of a macro can be described using a number of relations between its argument-values from before and after running the macro.

In case of "not1", the only relation is as follows:

'The final value of "reg" is the inverse of its initial value.'

or, as Tcl-statement:

if  { $final::reg == $initial::reg }  { 

    error "register has not been inverted"
} 

The assembly-validator simply tries all possible argument-values, each time verifying correct behaviour using this rule.

This kind of behaviour-desciption works fine for data-arguments, such as "reg" in the above example.

However, for macros taking branch-arguments, the user will have to make a wrapper (a small piece of assembly-code around the actual code to be tested), and use helper-variables to check whether a branch was or was not taken.

(The assembly-validator package in the downloads-section contains real-life examples of such wrappers.)

Macro-arguments revisited

When the assembler was explained in the previous section, macro-arguments were described as being simply symbolic names. However, for the purpose of assembly-validation, it makes sense to add some extra info to each such argument.

Consider the "not1"-macro shown above, with its "reg"-argument as symbolic placeholder for a RAM-address.

This argument can be extended with access- and bitwidth-specifiers, as shown here:

macro  not1  reg:rw1 {

    ...
} 

This states that the "reg"-argument is being read as well as written by the macro ("rw"), and that its size is 1 bit ("1").

Access-specifiers - such as "rw" in this example - specify how the macro treats this argument:

• "r" for read-only (i.e. the macro doesn't alter this argument)
• "w" for write-only (i.e. the macro writes this argument, and ignores its original value)
• "rw" (or "wr") for read-write (i.e. the macro reads, and may then overwrite this argument)

Bitwidth-specifiers - such as the "1" in this example - specify how many bits of RAM, starting at the argument-address, belong to the argument.

The assembler ignores these specifiers, but the validator does not. Bitwidth-specifiers tell the validator how many possible values it has to try for each argument.

Checking read-only argument clobbering

Strictly speaking, only write-only and read-write arguments would have to be checked in order to verify a macro's behaviour.

However, in case a macro erroneously clobbers (overwrites) any read-only arguments, following code would likely fail, if it expected the macro to leave its read-only arguments unaltered.

To avoid this, the validator automatically verifies that no read-only argument is changed by the macro, by comparing each read-only argument's value from before and after running the macro. If there is a mismatch, the validator will throw an error.

Examples of use

For the "not1"-macro, a file containing the aforementioned behaviour-description can be created, say "not1.test":

$ cat not1.test 

if  { $final::reg == $initial::reg }  {

    error "register has not been inverted"
}

$ 

To run the assembly-validator, the assembly-source file containing the macro, the macro-name and the behaviour-file must be given as command-line arguments, in that order:

$ ./trace.tcl  1bit.asm  not1  not1.test
$ 

There are no error-messages, meaning the validation was succesful, and "not1" behaves as it should.

Let's say the macro-definition was changed as follows, introducing a deliberate error:

macro  not1  reg:rw1 {

            ibc1    $reg    done
    : done

            set1    $reg       ;# deliberate mistake!
} 

When running the validator again, the error is spotted:

$ ./trace.tcl  1bit.asm  not1  not1.test 
Fail (id=1): register has not been inverted.
Arguments (before): reg:rw1=1
Arguments (after) : reg:rw1=1
$ 

(The "id=1" can be ignored, and is basically a sequence-number indicating the number of argument-combinations tried so far.)

As can be seen, because of the error introduced, when "1" goes into the macro, "1" comes out - this is not according to the behaviour-description.

As another example, a different kind of error can be introduced into the macro-definition:

macro  not1  reg:r1 {      ;# "reg" is read-only now!

            ibc1    $reg    done
    : done
} 

This example is somewhat contrived, but says that the macro should not alter its "reg"-argument (which is now read-only).

However, the macro-body obviously still inverts it. Therefore, the macro now clobbers a read-only argument.

When running the validator again, the argument-clobbering is noticed:

$ ./trace.tcl  1bit.asm  not1  not1.test 
Fail (id=0): r/o variable 'reg' has been changed.
Arguments (before): reg:r1=0
Arguments (after) : reg:r1=1
Fail (id=1): r/o variable 'reg' has been changed.
Arguments (before): reg:r1=1
Arguments (after) : reg:r1=0
$