← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2004/matthews-vroon/support/tiny-fib-example/fib-def.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2004/matthews-vroon/support/tiny-fib-example/fib-def.lisp
 
1
(in-package "ACL2")
 
2
;; A proof that an implementation of the Fibonacci function
 
3
;; on Tiny, a small stack-machine, is correct.
 
4
 
 
5
(include-book "tiny")
 
6
;(include-book "tiny-rewrites")
 
7
;(include-book "stream-fib")
 
8
 
 
9
(set-verify-guards-eagerness 0)
 
10
 
 
11
(defun tiny-loaded () t)
 
12
 
 
13
;; Addresses of fib's temporary variables
 
14
(defconst *fib-adr* 20)
 
15
(defconst *fib-1-adr* (1+ *fib-adr*))
 
16
 
 
17
;; The start-of-program address
 
18
(defconst *prog-start-address* 100)
 
19
 
 
20
;; Replaces label placeholders in a program fragment with
 
21
;; their final computed values. Label placeholders should
 
22
;; be negative integers, to prevent conflicts with opcodes
 
23
;; and address references in the program being patched.
 
24
(defun patch-prog-labels (prog label-map)
 
25
  (cond ((endp prog)
 
26
         prog)
 
27
        ((assoc-equal (car prog) label-map)
 
28
         (cons (cdr (assoc-equal (car prog) label-map))
 
29
               (patch-prog-labels (cdr prog) label-map)))
 
30
        (t
 
31
         (cons (car prog)
 
32
               (patch-prog-labels (cdr prog) label-map)))))
 
33
 
 
34
#|
 
35
NOTE: I am using Hoare triples to document the pre- and post-conditions
 
36
      of basic blocks. To describe the contents of the stack I am overloading
 
37
      the predicate symbol (<=) to compare stacks. Given stacks xs and ys,
 
38
      xs <= ys holds when xs is a prefix of ys. I write the contents of
 
39
      a stack using Haskell notation, so that [1,2,3] represents a three
 
40
      element stack with 1 as the top element. I use the special constant
 
41
      'stack' to represent tiny's current value stack.
 
42
 
 
43
      I also define an operator on memory that takes a stack of addresses
 
44
      and returns a stack of values consisting of the current contents of
 
45
      memory at those addresses. So if the contents of memory at address
 
46
      1 is 3 and the contents of memory at address 5 is 12, then
 
47
      mem[1,3] = [5,12].
 
48
|#
 
49
 
 
50
;; {[N] <= stack}
 
51
;; *init-block*
 
52
;; {[N-1] <= stack /\ mem[*fib-adr*,*fib-adr-1*] = [1,1]}
 
53
(defconst *init-block*
 
54
  (assemble `(pushsi 1
 
55
              dup
 
56
              dup
 
57
              pop ,*fib-adr*
 
58
              pop ,*fib-1-adr*
 
59
              sub)))
 
60
 
 
61
 
 
62
;; {[N] <= stack /\ mem[*fib-adr*,*fib-adr-1*] = [M,K]}
 
63
;; *loop-block*
 
64
;; {   (N=0 /\ [0] <= stack /\ mem[*fib-adr*] = M)
 
65
;;  \/ ([N-1] <= stack /\ mem[*fib-adr*,*fib-adr-1*] = [M+K,M])}
 
66
(defconst *loop-label-hole* -2)
 
67
(defconst *done-label-hole* -3)
 
68
(defconst *unpatched-loop-block*
 
69
  (assemble `(; loop-label-hole:
 
70
              dup
 
71
              jumpz ,*done-label-hole*
 
72
              pushs ,*fib-adr*
 
73
              dup
 
74
              pushs ,*fib-1-adr*
 
75
              add
 
76
              pop ,*fib-adr*
 
77
              pop ,*fib-1-adr*
 
78
              pushsi 1
 
79
              sub
 
80
              jump ,*loop-label-hole*
 
81
              ; done-label-hole:
 
82
              )))
 
83
 
 
84
; Calculate the actual program labels to patch
 
85
(defconst *loop-label*        (+ *prog-start-address*
 
86
                                 (len *init-block*)))
 
87
(defconst *done-label*        (+ *loop-label*
 
88
                                 (len *unpatched-loop-block*)))
 
89
 
 
90
(defconst *label-patches*
 
91
     `((,*loop-label-hole* . ,*loop-label*)
 
92
       (,*done-label-hole* . ,*done-label*)))
 
93
 
 
94
(defconst *loop-block*
 
95
  (patch-prog-labels *unpatched-loop-block* *label-patches*))
 
96
 
 
97
;; {[0] <= stack /\ mem[*fib-adr*] = M)
 
98
;; *done-block*
 
99
;; {[M] <= stack}
 
100
(defconst *done-block*
 
101
  (assemble `(pushs ,*fib-adr*
 
102
              add
 
103
              halt)))
 
104
 
 
105
(defconst *prog-halt-address* (+ *done-label*
 
106
                                 (1- (len *done-block*))))
 
107
 
 
108
;; The Fibonacci program
 
109
(defconst *fib-prog*
 
110
  (append *init-block*
 
111
          *loop-block*
 
112
          *done-block*))
 
113
 
 
114
 
 
115
;;; ;;========== Test harness for evaluating *fib-prog* on tiny =============
 
116
 
 
117
;; ;; Initialize the state of the tiny interpreter so
 
118
;; ;; that it will calculate the n'th Fibonacci number.
 
119
;; ;; The variable 'tiny-state' is a stobj defined in tiny.lisp.
 
120
;; (defun init-tiny-fib (tiny-state n)
 
121
;;   (declare (xargs :stobjs (tiny-state)))
 
122
;;   (load-tiny *prog-start-address*
 
123
;;           `((,*prog-start-address* . ,*fib-prog*) ; Load program into memory
 
124
;;             (901 . (,n)))                         ; Initialize TOS with n
 
125
;;           tiny-state))
 
126
 
 
127
;; ;; Initialize the current tiny machine state
 
128
;; (defconst *fib-input* 4)
 
129
;; (init-tiny-fib tiny-state *fib-input*)
 
130
 
 
131
;; ;;Execute exactly enough TINY steps to have the
 
132
;; ;; fib program halt.
 
133
;; (tiny tiny-state (+ (len *init-block*)
 
134
;;                  (* (1- *fib-input*) (len *loop-block*))
 
135
;;                  (len *done-block*)))
 
136
 
 
137
;; ; Examine the returned Fibonacci number
 
138
;; (dtos-val tiny-state 0)
 
139
 
 
140
;; ; Check that the returned number matches
 
141
;; ;  the Fibonacci specification.
 
142
;; (equal (dtos-val tiny-state 0) (fib-spec *fib-input*))
 
143
 
 
144
;; ; Check that the program has halted.
 
145
;; (equal (memi (progc tiny-state) tiny-state) (encode 'halt))
 
146
 
 
147
;; ;;Execute these commands in ACL2's repl-loop to probe
 
148
;; ;; the contents of the TINY machine state.
 
149
;; *prog-start-address*
 
150
;; (memi *prog-start-address* tiny-state)
 
151
;; (dtos-val tiny-state 0)  ; data TOS
 
152
;; (progc tiny-state)       ; program counter
 
153
;; (ctos tiny-state)        ; return value TOS
 
154
 
 
155
(defconst *fib-cutpoints*
 
156
  `(,*prog-start-address*
 
157
    ,*loop-label*
 
158
    ,*done-label*
 
159
    ,*prog-halt-address*))
 
160
 
 
161
;;The initial top-of-stack address. Note that the stack already
 
162
;; contains a single input value, namely the parameter to fib.
 
163
(defconst *init-dtos* 899)