Download Assertion Language manual - Bound

instruction to perform some other kind of transfer of control. For example, a jump to a
dynamically computed address can be performed by pushing the address value on the stack
and executing a "return".
To analyze such multi-role instructions Bound-T must decide which role the instruction
performs, because Bound-T uses different data structures and different analysis methods for
different roles. The automatic algorithms built into Bound-T can sometimes choose the wrong
role, which may make the analysis fail. In such cases you can tell Bound-T which role to use for
that instruction.
An instruction that performs a tail call
For a concrete example, consider the way some compilers implement calls via function
pointers on the Intel-8051 processor. This processor has a stack that is normally used to hold
return addresses. The ret instruction pops a 16-bit address off the stack and into the Program
Counter PC. Assume now that the 16-bit DPTR register holds the dynamically computed
address of a subprogram (a function pointer, in C language terms). One way to call the
subprogram at this address is to call an intermediate subprogram that we name ICall which
contains instructions that push the DPTR on the stack, followed by a ret. In 8051 assembly
language:
ICall: push DPL
push DPH
ret
Note that although the ret instruction occurs in its usual place at the end of a subprogram
(ICall), its role is not just to return from this subprogram. What it does is to transfer control to
the address in DPTR, the entry point of the subprogram we want to call. However, the return
address for ICall is still on the stack, so when the subprogram at DPTR eventually returns, it
returns to that address (the instruction following the call of ICall). This kind of "trampoline"
call is often termed a tail call, and here is how you can assert to the Intel-8051 version of
Bound-T that this ret instruction performs a tail call, not an ordinary return:
subprogram "ICall"
instruction at offset "4"
performs a "tail call";
end instruction;
end "ICall";
Note that the name of the instruction role is written in quotes as "tail call". This is because the
instruction roles are target-specific and are not standard keywords of the assertion language.
To find out which offset to use to identify an instruction you can disassemble the subprogram
(for example with the Bound-T option -trace decode) and compute the difference of the
instruction address and the subprogram entry point address. In the example, the offset is 4
octets because each of the push instructions is 2 octets long.
The roles that instructions can perform
The instructions and their roles are of course target-specific. Moreover, most instructions have
fixed roles that cannot be changed with role assertions. For example, an instruction that just
adds two data registers and puts the sum in a third data register can hardly be required to
perform a call. The role-instruction combinations for a given target processor are listed in the
Bound-T Application Note for that target. If you assert a role for an instruction that Bound-T is
not willing to model for that instruction, the result will be an error message to this effect, or a
warning message saying that the assertion was not used at all.
Bound-T Assertion Language
Writing Assertions
43