Typed x86: An Example

fact: "r.{eax:int,esp:(t::r)} where t = {eax:int,esp:r}

; arg in eax, return address on top of stack, rest of stack is abstract

cmp eax,0 ; is arg > 0?

jg L1 ; if so, goto L1

mov eax,1 ; otherwise, return 1 as result

ret ; pop return address and jump to it

L1: push eax ; save arg, stack has type int::t::r

dec eax ; arg := arg - 1

call fact[int::t::r]

; instantiate r with current stack’s type, push return address on stack,

; and jump to fact. Upon return, eax should contain the result and

; the stack will still have type int::t::r.

pop ecx ; ecx := arg

imul ecx ; eax := arg * fact(arg-1)

ret ; pops return address and jumps to it

Previous slide

Next slide

Back to first slide

View graphic version