Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Digital systems, linear algebra, introduction to formal proof resit / 1 / a / Solution 2026-10-25
View more
Use r0 for the argument and result. With 32-bit integers and pointers, the three fields have byte offsets 0, 4 and 8. Assume an acyclic finite binary tree, no concurrent mutation, a valid aligned call stack, and no signed integer overflow in any evaluated sum. These are representation and arithmetic assumptions, rather than properties of arbitrary C programming language implementations.
.syntax unified
.cpu cortex-m0
.thumb
.global sum_rec
.thumb_func
sum_rec:
    cmp  r0, #0
    beq  .Lempty
    push {r4, r5, r6, lr}    @ 16-byte frame; r6 is alignment padding
    movs r4, r0              @ retain this invocation's node
    ldr  r5, [r4, #0]        @ running value begins with its label
    ldr  r0, [r4, #4]
    bl   sum_rec             @ r0 = left subtree sum
    adds r5, r5, r0
    ldr  r0, [r4, #8]
    bl   sum_rec             @ r0 = right subtree sum
    adds r0, r0, r5
    pop  {r4, r5, r6, pc}    @ restore caller state and return
.Lempty:
    movs r0, #0
    bx   lr
The node and partial sum are held in callee-saved registers r4,r5. Each recursive invocation saves its caller's values before replacing them, so a child returns with the parent's values intact. Saving lr preserves the return address across the two bl instructions. Caller-saved registers may be overwritten by a child; no parent value is left live only in them. Pushing four words maintains eight-byte stack alignment at recursive calls.[ref]
Correctness follows by structural induction. An empty subtree returns zero. For a nonempty subtree, assume both recursive calls return their respective label sums. The final addition then combines the node's label with exactly those two sums, so r0 returns the sum of all labels. The instruction forms and field offsets fit the short load and arithmetic encodings.[ref]
Read the full article
Stack alignment 2026-10-24
View more
Stack alignment constrains the stack pointer to a multiple of a specified byte boundary. AAPCS32 requires word alignment generally and eight-byte alignment at public interfaces. Saving four 32-bit words preserves eight-byte alignment; saving three would change it by four bytes and may require padding before another call. Frame size and the alignment of local objects must be considered together.[ref]
Read the full article