← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2000/lusk-mccune/lusk-mccune-final/stepproc2.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/2000/lusk-mccune/lusk-mccune-final/stepproc2.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
(include-book "setup")
 
4
 
 
5
(local (in-theory (enable statementp)))
 
6
 
 
7
;; The following are useful when disabling mstatep
 
8
 
 
9
(defthm mstate-pstate-listp
 
10
  (implies (mstatep ms)
 
11
           (pstate-listp (first ms))))
 
12
 
 
13
(defthm mstate-cstate-listp
 
14
  (implies (mstatep ms)
 
15
           (cstate-listp (second ms))))
 
16
 
 
17
(defthm mstate-lstate-listp
 
18
  (implies (mstatep ms)
 
19
           (lstate-listp (third ms))))
 
20
 
 
21
(defthm mstate-program-listp
 
22
  (implies (mstatep ms)
 
23
           (program-listp (fourth ms))))
 
24
 
 
25
;;--------------------------------
 
26
;; exec-setup-listener
 
27
 
 
28
;; [Jared] adding this because the defun below failed when it was added to ACL2.
 
29
(local (in-theory (disable FOLD-CONSTS-IN-+)))
 
30
 
 
31
(defun exec-setup-listener (stmt ps ms)
 
32
  (declare (xargs :guard (and (statementp stmt)
 
33
                              (equal (car stmt) 'setup-listener)
 
34
                              (mstatep ms)
 
35
                              (pstatep ps))
 
36
                  :verify-guards nil))
 
37
 
 
38
  (let ((port (evl2 (second stmt) (memory ps))))
 
39
    (if (portp port)
 
40
        (let* ((x (setup-listener (car ps) port ms))
 
41
               (lfd (first x))
 
42
               (ms1 (second x)))
 
43
    
 
44
          (make-mstate
 
45
           (update-pstate (car ps)
 
46
                          (make-pstate (car ps)
 
47
                                       (code ps)
 
48
                                       (+ 1 (cc ps))
 
49
                                       (xstack ps)
 
50
                                       (asgn (third stmt)
 
51
                                             lfd
 
52
                                             (memory ps)))
 
53
                          (pstates ms1))
 
54
           (cstates ms1)
 
55
           (lstates ms1)
 
56
           (programs ms)))
 
57
 
 
58
      (make-mstate
 
59
       (update-pstate (car ps)
 
60
                      (make-pstate (car ps)
 
61
                                   (code ps)
 
62
                                   0
 
63
                                   (xstack ps)
 
64
                                   (asgn 'error
 
65
                                         ''bad-port-in-setup-listener
 
66
                                         (memory ps)))
 
67
                      (pstates ms))
 
68
       (cstates ms)
 
69
       (lstates ms)
 
70
       (programs ms))
 
71
      )))
 
72
 
 
73
(defthm evaluated-expressionp-car-setup-listener
 
74
  (evaluated-expressionp (car (setup-listener hpid port ms))))
 
75
 
 
76
(verify-guards exec-setup-listener
 
77
               :hints (("Goal"
 
78
                        :in-theory (disable setup-listener)))
 
79
               :otf-flg t)
 
80
 
 
81
(defthm exec-setup-listener-preserves-mstatep
 
82
  (implies (and (statementp stmt)
 
83
                (equal (car stmt) 'setup-listener)
 
84
                (mstatep ms)
 
85
                (pstatep ps))
 
86
           (mstatep (exec-setup-listener stmt ps ms)))
 
87
  :hints (("Goal"
 
88
           :in-theory (disable setup-listener))))
 
89
 
 
90
;;------------------------------------
 
91
 
 
92
(defthm request-listp-is-alistp
 
93
  (implies (request-listp rq)
 
94
           (alistp rq))
 
95
  :hints (("Goal"
 
96
           :in-theory (enable hpid-fdp)))
 
97
  :rule-classes :forward-chaining)
 
98
 
 
99
(defthm find-ls-alistp
 
100
  (implies (and (lstate-listp lss)
 
101
                (consp (find-ls dest-host dest-port lss)))
 
102
           (alistp (caddr (find-ls dest-host dest-port lss)))))
 
103
 
 
104
(defun connection-status (my-hpid dest-host dest-port ms)
 
105
  (declare (xargs :guard (and (hpidp my-hpid)
 
106
                              (hostp dest-host)
 
107
                              (portp dest-port)
 
108
                              (mstatep ms))))
 
109
  (let ((ls (find-ls dest-host dest-port (lstates ms))))
 
110
    (cond ((atom ls) 'not-listening)
 
111
          ((assoc-equal my-hpid (requestq ls)) 'pending)
 
112
          (t 'ready))))
 
113
 
 
114
(defun unkwote (x)
 
115
  (declare (xargs :guard t))
 
116
  (if (and (equal (len x) 2)
 
117
           (equal (first x) 'quote))
 
118
      (second x)
 
119
    x))
 
120
 
 
121
(in-theory (disable unkwote))
 
122
 
 
123
;;------------------------------------------------------------------
 
124
;; exec-connect
 
125
;;
 
126
;; This executes (or continues to execute) a statement like
 
127
;; (FDASGN FD (CONNECT remote-host remote-port)).
 
128
;;
 
129
;; If the remote-host is not listening on the remote-port, we set
 
130
;; the FD to -1 and bump the PC (connection refused).
 
131
;; If we have already issued a connect-request, and the remote host
 
132
;; has not accepted it, we do nothing.
 
133
;; Otherwise, we issue a connect-request.
 
134
;;
 
135
;; Note that the PC is bumped by the accepting process when the connection
 
136
;; is accepted.  Perhaps this bit of implicit handshaking should be rethought.
 
137
 
 
138
(defun exec-connect (stmt ps ms)
 
139
  (declare (xargs :guard (and (statementp stmt)
 
140
                              (equal (car stmt) 'connect)
 
141
                              (mstatep ms)
 
142
                              (pstatep ps))
 
143
                  :verify-guards nil))
 
144
 
 
145
  (let ((my-hpid (car ps))
 
146
        (dest-host (unkwote (evl2 (second stmt) (memory ps))))
 
147
        (dest-port (evl2 (third stmt) (memory ps))))
 
148
    (if (or (not (hostp dest-host))
 
149
            (not (portp dest-port)))
 
150
        (make-mstate
 
151
         (update-pstate (car ps)
 
152
                        (make-pstate (car ps)
 
153
                                     (code ps)
 
154
                                     0
 
155
                                     (xstack ps)
 
156
                                     (asgn 'error
 
157
                                           ''bad-host-or-port-in-connect
 
158
                                           (memory ps)))
 
159
                        (pstates ms))
 
160
         (cstates ms)
 
161
         (lstates ms)
 
162
         (programs ms))
 
163
      
 
164
      (let ((status (connection-status my-hpid dest-host dest-port ms)))
 
165
        (case status
 
166
              (pending ms)  ;; do nothing
 
167
 
 
168
              (not-listening (make-mstate
 
169
                              (update-pstate (car ps)
 
170
                                             (make-pstate (car ps)
 
171
                                                          (code ps)
 
172
                                                          (+ 1 (cc ps))
 
173
                                                          (xstack ps)
 
174
                                                          (asgn (fourth stmt)
 
175
                                                                -1
 
176
                                                                (memory ps)))
 
177
                                             (pstates ms))
 
178
                              (cstates ms)
 
179
                              (lstates ms)
 
180
                              (programs ms)))
 
181
 
 
182
              (ready (let* ((x (connect my-hpid dest-host dest-port ms))
 
183
                            (fd (first x))
 
184
                            (ms1 (second x)))
 
185
    
 
186
                       (make-mstate
 
187
                        (update-pstate (car ps)
 
188
                                       (make-pstate (car ps)
 
189
                                                    (code ps)
 
190
                                                    (cc ps)
 
191
                                                    (xstack ps)
 
192
                                                    (asgn (fourth stmt)
 
193
                                                          fd
 
194
                                                          (memory ps)))
 
195
                                       (pstates ms1))
 
196
                        (cstates ms1)
 
197
                        (lstates ms1)
 
198
                        (programs ms))))
 
199
 
 
200
              (otherwise ms)
 
201
              )))))
 
202
 
 
203
(defthm evaluated-expressionp-car-connect
 
204
  (evaluated-expressionp (car (connect hpid host port ms))))
 
205
 
 
206
(defthm conp-cdr-connect
 
207
  (consp (cdr (connect hpid host port ms))))
 
208
 
 
209
(defthm cdr-connect
 
210
  (cdr (connect hpid host port ms)))
 
211
 
 
212
(verify-guards exec-connect
 
213
               :hints (("Goal"
 
214
                        :in-theory (disable connect mstatep))))
 
215
 
 
216
(defthm exec-connect-preserves-mstatep
 
217
  (implies (and (statementp stmt)
 
218
                (equal (car stmt) 'connect)
 
219
                (mstatep ms)
 
220
                (pstatep ps))
 
221
           (mstatep (exec-connect stmt ps ms)))
 
222
  :hints (("Goal"
 
223
           :in-theory (disable connect))))
 
224
 
 
225
;;------------------------------------
 
226
;; exec-accept
 
227
;;
 
228
;; This executes a statement like (FDASGN FD (ACCEPT LFD)), where
 
229
;; LFD is the listening fd.  When and if we succeed, FD is given
 
230
;; the new fd for the conection.  If there are no requests to accept,
 
231
;; we do nothing (i.e., we wait).
 
232
 
 
233
(defun exec-accept (stmt ps ms)
 
234
  (declare (xargs :guard (and (statementp stmt)
 
235
                              (equal (car stmt) 'accept)
 
236
                              (mstatep ms)
 
237
                              (pstatep ps))
 
238
                  :verify-guards nil))
 
239
 
 
240
  (let ((lfd (evl2 (second stmt) (memory ps))))
 
241
    (if (not (fdp lfd))
 
242
        ;; The fd is bad, so set pc to 0 and set error variable.
 
243
        (make-mstate
 
244
         (update-pstate (car ps)
 
245
                        (make-pstate (car ps)
 
246
                                     (code ps)
 
247
                                     0
 
248
                                     (xstack ps)
 
249
                                     (asgn 'error
 
250
                                           ''bad-fd-in-accept
 
251
                                           (memory ps)))
 
252
                        (pstates ms))
 
253
         (cstates ms)
 
254
         (lstates ms)
 
255
         (programs ms))
 
256
      
 
257
      ;; The listening FD is ok.  Try to accept a connection.
 
258
      (let* ((x (accept (car ps) lfd ms))
 
259
             (fd (first x))
 
260
             (ms1 (second x)))
 
261
 
 
262
        (if (equal fd -1)
 
263
            ;; There is nothing to accept, so just wait.
 
264
            ms
 
265
          ;; All is well, so accept, bump our PC, and assign fd.
 
266
          (make-mstate
 
267
           (update-pstate (car ps)
 
268
                          (make-pstate (car ps)
 
269
                                       (code ps)
 
270
                                       (+ 1 (cc ps))
 
271
                                       (xstack ps)
 
272
                                       (asgn (third stmt)
 
273
                                             fd
 
274
                                             (memory ps)))
 
275
                          (pstates ms1))
 
276
           (cstates ms1)
 
277
           (lstates ms1)
 
278
           (programs ms)))))))
 
279
 
 
280
(defthm evaluated-expressionp-car-accept
 
281
  (evaluated-expressionp (car (accept hpid fd ms))))
 
282
 
 
283
(verify-guards exec-accept
 
284
               :hints (("Goal"
 
285
                        :in-theory (disable accept))))
 
286
 
 
287
(defthm exec-accept-preserves-mstatep
 
288
  (implies (and (statementp stmt)
 
289
                (equal (car stmt) 'accept)
 
290
                (mstatep ms)
 
291
                (pstatep ps))
 
292
           (mstatep (exec-accept stmt ps ms)))
 
293
  :hints (("Goal"
 
294
           :in-theory (disable accept))))