The Mach intermediate language: abstract syntax.
Mach is the last intermediate language before generation of assembly
code.
.
.
.
.
.
.
.
.
.
.
.
.
.
Like Linear, the Mach language is organized as lists of instructions
operating over machine registers, with default fall-through behaviour
and explicit labels and branch instructions.
The main difference with Linear lies in the instructions used to
access the activation record. Mach has three such instructions:
Mgetstack and Msetstack to read and write within the activation
record for the current function, at a given word offset and with a
given type; and Mgetparam, to read within the activation record of
the caller.
These instructions implement a more concrete view of the activation
record than the the Lgetstack and Lsetstack instructions of
Linear: actual offsets are used instead of abstract stack slots, and the
distinction between the caller's frame and the callee's frame is
made explicit.
The semantics for Mach is close to that of
Linear: they differ only
on the interpretation of stack slot accesses. In Mach, these
accesses are interpreted as memory accesses relative to the
stack pointer. More precisely:
-
Mgetstack ofs ty r is a memory load at offset ofs * 4 relative
to the stack pointer.
-
Msetstack r ofs ty is a memory store at offset ofs * 4 relative
to the stack pointer.
-
Mgetparam ofs ty r is a memory load at offset ofs * 4
relative to the pointer found at offset 0 from the stack pointer.
The semantics maintain a linked structure of activation records,
with the current record containing a pointer to the record of the
caller function at offset 0.
In addition to this linking of activation records, the
semantics also make provisions for storing a back link at offset
f.(fn_link_ofs) from the stack pointer, and a return address at
offset
f.(fn_retaddr_ofs). The latter stack location will be used
by the Asm code generated by
Asmgen to save the return address into
the caller at the beginning of a function, then restore it and jump to
it at the end of a function. The Mach concrete semantics does not
attach any particular meaning to the pointer stored in this reserved
location, but makes sure that it is preserved during execution of a
function. The
return_address_offset parameter is used to guess the
value of the return address that the Asm code generated later will
store in the reserved location.
.
1).
.
Proof.
.
Proof.
.
Proof.
.
Proof.
Extract the values of the arguments to an external call.
Mach execution states.
Mach execution states.
).