5.1.6 · Instruction summary

Each instruction has an explicit data, stack, and control contract.

Classify the registers read and written by every controller instruction, then execute a micro-controller that uses every supported instruction.

Guiding question

What must a reader know about one instruction before reasoning about a complete controller?

Summarize register reads and writes for each instruction tag
Distinguish stack effects from register effects
Distinguish next, conditional, direct, indirect, and halt control
Recognize constant, register, label, and operation sources
Execute a controller containing every instruction in the supported subset

instruction-summary treats controller text as data. It recursively extracts register sources from operation expressions, identifies the destination of assign and restore, records push or pop effects, and classifies how the pc changes. A branch reads the flag rather than an ordinary register; a label goto is direct while a register goto reads its target from a register.

The micro-controller then exercises the same reference against execution. It assigns constants and an operation result, saves and restores val, stores a label position in continue, jumps indirectly through that register, tests, takes a branch, performs an observable operation, and halts. The summary is the exact reference for this finite simulator subset.

SICP code2,378 of 1,048,576 UTF-8 bytes

(begin
  (define (tagged-list? value tag)
    (and (pair? value) (eq? (car value) tag)))
  (define (contains? item items)
    (cond ((null? items) #f)
          ((eq? item (car items)) #t)
          (else (contains? item (cdr items)))))
  (define (adjoin item items)
    (if (contains? item items) items (append items (list item))))
  (define (union left right)
    (if (null? right)
        left
        (union (adjoin (car right) left) (cdr right))))
  (define (source-registers source)
    (cond ((tagged-list? source 'reg)
           (list (cadr source)))
          ((tagged-list? source 'op)
           (collect-registers (cddr source)))
          (else '())))
  (define (collect-registers sources)
    (if (null? sources)
        '()
        (union (source-registers (car sources))
               (collect-registers (cdr sources)))))
  (define (instruction-summary instruction)
    (let ((tag (car instruction)))
      (cond
        ((eq? tag 'assign)
         (list 'assign
               (source-registers (caddr instruction))
               (list (cadr instruction))
               'none
               'next))
        ((eq? tag 'test)
         (list 'test
               (source-registers (cadr instruction))
               '()
               'none
               'next))
        ((eq? tag 'branch)
         (list 'branch '() '() 'none 'conditional))
        ((eq? tag 'goto)
         (list 'goto
               (source-registers (cadr instruction))
               '()
               'none
               (if (tagged-list? (cadr instruction) 'reg)
                   'indirect
                   'direct)))
        ((eq? tag 'save)
         (list 'save (list (cadr instruction)) '() 'push 'next))
        ((eq? tag 'restore)
         (list 'restore '() (list (cadr instruction)) 'pop 'next))
        ((eq? tag 'perform)
         (list 'perform
               (source-registers (cadr instruction))
               '()
               'none
               'next))
        ((eq? tag 'halt)
         (list 'halt '() '() 'none 'halt))
        (else
         (list 'unknown '() '() 'none 'unknown)))))
  (map instruction-summary
       '((assign val (op + (reg a) (const 1)))
         (test (op = (reg val) (const 10)))
         (branch done)
         (goto (reg continue))
         (save val)
         (restore val)
         (perform (op record (reg val)))
         (halt))))

(begin
  (define (tagged-list? value tag)
    (and (pair? value) (eq? (car value) tag)))
  (define (contains? item items)
    (cond ((null? items) #f)
          ((eq? item (car items)) #t)
          (else (contains? item (cdr items)))))
  (define (adjoin item items)
    (if (contains? item items) items (append items (list item))))
  (define (union left right)
    (if (null? right)
        left
        (union (adjoin (car right) left) (cdr right))))
  (define (source-registers source)
    (cond ((tagged-list? source 'reg)
           (list (cadr source)))
          ((tagged-list? source 'op)
           (collect-registers (cddr source)))
          (else '())))
  (define (collect-registers sources)
    (if (null? sources)
        '()
        (union (source-registers (car sources))
               (collect-registers (cdr sources)))))
  (define (instruction-summary instruction)
    (let ((tag (car instruction)))
      (cond
        ((eq? tag 'assign)
         (list 'assign
               (source-registers (caddr instruction))
               (list (cadr instruction))
               'none
               'next))
        ((eq? tag 'test)
         (list 'test
               (source-registers (cadr instruction))
               '()
               'none
               'next))
        ((eq? tag 'branch)
         (list 'branch '() '() 'none 'conditional))
        ((eq? tag 'goto)
         (list 'goto
               (source-registers (cadr instruction))
               '()
               'none
               (if (tagged-list? (cadr instruction) 'reg)
                   'indirect
                   'direct)))
        ((eq? tag 'save)
         (list 'save (list (cadr instruction)) '() 'push 'next))
        ((eq? tag 'restore)
         (list 'restore '() (list (cadr instruction)) 'pop 'next))
        ((eq? tag 'perform)
         (list 'perform
               (source-registers (cadr instruction))
               '()
               'none
               'next))
        ((eq? tag 'halt)
         (list 'halt '() '() 'none 'halt))
        (else
         (list 'unknown '() '() 'none 'unknown)))))
  (map instruction-summary
       '((assign val (op + (reg a) (const 1)))
         (test (op = (reg val) (const 10)))
         (branch done)
         (goto (reg continue))
         (save val)
         (restore val)
         (perform (op record (reg val)))
         (halt))))

Examples

Result—

Output: —
Value: —
Diagnostic: —

Execution trace0 / 0 events

Expected result

The summary program returns contracts for assign, test, branch, goto, save, restore, perform, and halt in that order. The micro-controller returns (complete 10 #t 12 (10)).

Trace focus

Compare each static contract with its executed transition. In particular, follow save and restore without a visible final stack value, the label source stored in continue, the indirect goto, the flag-setting test, and the true branch that skips the -1 assignment.

Try it yourself

Change the program and compare the result.

Add a second goto that uses a label source and a perform instruction with two register operands. Update the static summaries before running the controller.

Show hint

A direct label goto reads no ordinary register. A perform instruction reads every register found recursively inside its operation source.

Complete this lesson

0 of 23 lessons complete in this chapter0%