← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2014/puri-ray-hao-xie/support/semantics.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/2014/puri-ray-hao-xie/support/semantics.lisp
 
1
#||
 
2
 
 
3
semantics.lisp
 
4
~~~~~~~~~~~~~~
 
5
Author: Disha Puri
 
6
Last Updated: 12th April 2014 
 
7
 
 
8
This file provides the semantics of CCDFG. It specifies what it 
 
9
means to execute a CCDFG. This can be viewed as providing an 
 
10
interpreter semantics to a parse tree.   
 
11
 
 
12
The syntax and semantics together provide a way to write a program in
 
13
terms of a graph and allow classical logic to manipulate and reason
 
14
about that graph-based program.
 
15
 
 
16
||#
 
17
 
 
18
(in-package "ACL2")
 
19
(include-book "functions")
 
20
 
 
21
 
 
22
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
23
;; Section 1: Execute a statement in a CCDFG
 
24
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
25
 
 
26
;; execute-store statement
 
27
(defun append-pos (val pos heap)
 
28
  (if (or (not (integerp val))
 
29
          (< val 0)  
 
30
          (not (integerp pos))
 
31
          (< pos 0)) heap 
 
32
    (if (equal pos 0) (append (list val) (cdr heap))
 
33
      (append (list (car heap)) 
 
34
              (append-pos val (1- pos) (cdr heap))))))
 
35
  
 
36
;; stmt is  store value address v
 
37
(defun execute-store (stmt init-state)
 
38
  (let* ((val (evaluate-val (second stmt) (car init-state)))
 
39
         (addr (evaluate-val (third stmt) (car init-state)))
 
40
         (heap (evaluate-val (fourth stmt) (third init-state))))
 
41
    (if (or (not (integerp addr))
 
42
            (< addr 0)
 
43
            (not (integerp val))
 
44
            (< val 0)) 
 
45
      init-state
 
46
      (list (car init-state) (second init-state) 
 
47
            (replace-var (fourth stmt) 
 
48
                         (append-pos val addr heap)
 
49
                         (third init-state))))))
 
50
 
 
51
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
52
;; Now execution of assignment statement.
 
53
;; This really is in two parts.  First we will need to evaluate the
 
54
;; expression and then we will do an assignment of the appropriate
 
55
;; variable to extend the mapping.
 
56
 
 
57
(defun evaluate-load (expr mem bindings)
 
58
  (let* ((addr (evaluate-val (second expr) bindings)))
 
59
         (if (or (not (integerp addr))
 
60
                 (< addr 0)
 
61
                 (>= addr (- (len mem) 2))) nil
 
62
        (nth addr (cdr mem)))))
 
63
 
 
64
(defun evaluate-load2 (expr mem bindings)
 
65
  (let* ((addr (evaluate-val (second expr) bindings)))
 
66
         (if (or (not (integerp addr))
 
67
                 (< addr 0)
 
68
                 (>= addr (- (len mem) 2))) nil
 
69
       (nth addr (cdr mem)))))
 
70
 
 
71
(defun evaluate-add (expr bindings)
 
72
  (let ((op1 (evaluate-val (second expr) bindings))
 
73
        (op2 (evaluate-val (third expr) bindings)))
 
74
    (if (and (acl2-numberp op1)
 
75
             (acl2-numberp op2))
 
76
        (+ op1 op2)
 
77
      nil)))
 
78
 
 
79
(defun evaluate-xor (expr bindings)
 
80
  (let* ((op1 (evaluate-val (second expr) bindings))
 
81
         (op2 (evaluate-val (third expr) bindings)))
 
82
      (let ((res (xor (if (equal op1 0) nil  t) 
 
83
                      (if (equal op2 0) nil t))))
 
84
        (if (equal (or op1 op2) nil) nil
 
85
          (if res 1 0)))))
 
86
 
 
87
(defun evaluate-lshr (expr bindings)
 
88
  (let ((op1 (evaluate-val (second expr) bindings))
 
89
        (op2 (evaluate-val (third expr) bindings)))
 
90
        (if (and (integerp op1)
 
91
                 (integerp op2))
 
92
            (ash op1 op2)
 
93
          nil)))
 
94
 
 
95
(defun evaluate-shl (expr bindings)
 
96
  (let* ((op1 (evaluate-val (second expr) bindings))
 
97
        (op2 (evaluate-val (third expr) bindings)))
 
98
                (if (and (integerp op1)
 
99
                 (integerp op2))
 
100
            (ash op1 (- 0 op2))
 
101
          nil)))
 
102
 
 
103
(defun evaluate-symbol (expr bindings)
 
104
  (let ((op (evaluate-val (first expr) bindings)))
 
105
    op))
 
106
 
 
107
(defun evaluate-eq (expr bindings)
 
108
  (let ((op1 (evaluate-val (second expr) bindings))
 
109
        (op2 (evaluate-val (third expr) bindings)))
 
110
    (if (equal op1 op2) 1
 
111
      0)))
 
112
 
 
113
(defun evaluate-ptr (expr ptrs)
 
114
  (let ((op (nth 0 (evaluate-val (second expr) ptrs))))
 
115
    op))
 
116
 
 
117
(defun execute-assignment (stmt init-state)
 
118
  (let* 
 
119
      ((expr (second stmt))
 
120
       (var (first stmt))
 
121
       (val 
 
122
        (cond 
 
123
         ((load-expression-p expr) (evaluate-load expr (second init-state) (car init-state)))
 
124
         ((load2-expression-p expr) (evaluate-load2 expr (second init-state) (car init-state)))
 
125
         ((add-expression-p expr) (evaluate-add expr (car init-state)))
 
126
         ((xor-expression-p expr) (evaluate-xor expr (car init-state)))
 
127
         ((shl-expression-p expr) (evaluate-shl expr (car init-state)))
 
128
         ((lshr-expression-p expr) (evaluate-lshr expr (car init-state)))
 
129
         ((eq-expression-p expr) (evaluate-eq expr (car init-state)))
 
130
         ((getelementptr-expression-p expr) (evaluate-ptr expr (third init-state)))
 
131
         ((symbol-expression-p expr) (evaluate-symbol expr (car init-state)))
 
132
         (t (er hard 'evaluate-assignment "wrong expression ~p0~%" expr)))))
 
133
    (list (replace-var var val (car init-state)) (second init-state) (third init-state))))
 
134
 
 
135
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
136
 
 
137
;; phi-construct
 
138
 
 
139
(defun choose (choices prev-bb)
 
140
  (if (or (equal (nth 1 (first choices)) prev-bb)
 
141
          (equal (symbol-name (nth 1 (first choices))) prev-bb))
 
142
      (nth 0 (first choices))
 
143
    (nth 0 (second choices))))
 
144
 
 
145
;;one stmt is (|%v0_1| (phi  (|%v0_2| bb) (|%v0| entry)))
 
146
(defun execute-phi (stmt init-state prev-bb)
 
147
  (let* 
 
148
      ((expr (cdr stmt))
 
149
       (var (first stmt))
 
150
       (val 
 
151
        (cond 
 
152
         ((phi-expression-p expr) (evaluate-val (choose (cdr (car expr)) prev-bb) (car init-state)))
 
153
         (t (er hard 'evaluate-phi "wrong expression ~p0~%" expr)))))
 
154
    (list (replace-var var val (car init-state)) (second init-state) (third init-state))))         
 
155
 
 
156
(defun execute-phi-s (stmts init-state prev-bb)
 
157
  (if (or (endp stmts)
 
158
          (not (consp stmts))) init-state
 
159
    (execute-phi-s (cdr stmts) 
 
160
                   (execute-phi (car stmts) 
 
161
                                init-state 
 
162
                                prev-bb)
 
163
                   prev-bb)))
 
164
 
 
165
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
166
 
 
167
;; while executing a CCDFG, we give special treatement to phi and branch statements,
 
168
;; for others we do execute-statement
 
169
;; so we have branch, assignment and store
 
170
;; we keep phi separate as it is not used once phi-construct is removed
 
171
;; we keep branch separate as it changes the control flow
 
172
(defun execute-statement (stmt init-state)
 
173
  (cond ((branch-statement-p stmt) init-state)
 
174
        ((store-statement-p stmt) (execute-store (car stmt) init-state))
 
175
        ((assignment-statement-p stmt) (execute-assignment (car stmt) init-state))
 
176
        (t init-state))) 
 
177
 
 
178
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
179
 
 
180
;; br bb1 [from entry]
 
181
(defun get-next-block-uncond (stmt init-state)
 
182
  (declare (ignore init-state))
 
183
  (second stmt))
 
184
 
 
185
;; A conditional branch statement has a condition label and two
 
186
;; targets (based on the value of the source).
 
187
;; condition is either true or false
 
188
(defun get-next-block-cond (stmt init-state)
 
189
  (let* ((condition (evaluate-val (second stmt) (car init-state)))
 
190
         (tgt (third stmt))
 
191
         (ft (fourth stmt)))
 
192
    (if (equal condition 1) 
 
193
      tgt
 
194
      ft)))
 
195
  
 
196
;; gives the name of the next basic block by evaluating the branch statement
 
197
(defun get-next-bb (stmt init-state)
 
198
  (if (unconditional-branch-statement-p stmt)
 
199
    (get-next-block-uncond stmt init-state)
 
200
    (get-next-block-cond stmt init-state)))
 
201
 
 
202
;; finds the next steps in same list of msteps from where to start executing if encounter a branch
 
203
(defun next-to-execute (msteps bb)
 
204
  (if (endp msteps) nil
 
205
    (if (equal (prefix (car msteps))
 
206
               (prefix bb))
 
207
      msteps
 
208
      (next-to-execute (cdr msteps) bb))))
 
209
       
 
210
;; if there is no branch statement in the block, next block is the one in order
 
211
;; if there is a branch which has been used within the block, then too
 
212
;; else next block is found by get-next-bb
 
213
(defun get-next-lists (l init-state)
 
214
  (if (endp l) nil
 
215
    (if (not (branch-statement-p (cdr (car l))))
 
216
      (get-next-lists (cdr l) init-state)
 
217
      (if (equal (next-to-execute (cdr l) (get-next-bb (cadr (car l)) init-state)) nil)
 
218
        (get-next-bb (cadr (car l)) init-state)
 
219
        nil))))
 
220
 
 
221
(defun get-next-block (block init-state)
 
222
  (if (endp block) nil
 
223
    (if (equal (get-next-block (cdr block) (get-next-lists (car block) init-state)) nil)
 
224
        (get-next-lists (car block) init-state)
 
225
        nil)))
 
226
        
 
227
;; if branch-statement, go to next stmt with the next bb if in the same block
 
228
;; for everything else, execute-statement and go to next one
 
229
;; when you run a block, we go in order unless there is a branch 
 
230
;; a block is a list of msteps
 
231
 
 
232
;; b = (x y z)
 
233
(defun run-lists (msteps init-state next prev)
 
234
  (if (endp msteps) init-state
 
235
    (if (or (equal next nil)
 
236
            (equal next (prefix (car msteps))))
 
237
      (if (branch-statement-p (cdr (car msteps)))
 
238
        (run-lists (next-to-execute (cdr msteps) (get-next-bb (cadr (car msteps)) init-state)) 
 
239
                   init-state
 
240
                   nil
 
241
                   prev)
 
242
        (if (phi-statements-p (cdar msteps))
 
243
          (run-lists (cdr msteps) (execute-phi-s (cdar msteps) init-state prev) nil prev)
 
244
          (run-lists (cdr msteps) (execute-statement (cdar msteps) init-state) nil prev)))
 
245
      (run-lists (cdr msteps) init-state next prev))))
 
246
  
 
247
;; b = (()()())
 
248
(defun run-block (b init-state next prev)
 
249
  (if (endp b) init-state
 
250
    (run-block (cdr b) (run-lists (car b) init-state next
 
251
                                  prev)
 
252
               (get-next-block b init-state)
 
253
               prev)))
 
254
 
 
255
;; run a set of blocks, c here is equivalent to a list of basic blocks
 
256
;; (cadar c) = ((a) (b) (c))
 
257
;; first statement is (caar (cadar c))
 
258
;; if next is nil or next is equal to prefix of first statement, then execute the first statement 
 
259
(defun run-block-set (c init-state next-bb prev)
 
260
  (if (endp c) init-state
 
261
      (run-block-set (cdr c) (run-block (cadar c) init-state next-bb prev) 
 
262
                     (get-next-block (cadar c) init-state) 
 
263
                     prev)))
 
264
 
 
265
;; run the entire loop block set for certian number of iterations
 
266
;; c = ((name1 ((a)(b)(c))) (name2 (()()())))
 
267
(defun run-blocks-iters (c init-state iter prev)
 
268
  (if (zp iter) init-state
 
269
    (run-blocks-iters c (run-block-set c init-state nil prev) (- iter 1) prev)))
 
270
 
 
271
;; Because we want loop to be iterated a certain number of types,
 
272
;; I have divided run a ccdfg into run-pre, run-loop and run-post
 
273
;; run-ccdfg-k means run-pre, then run-loop for k iterations
 
274
(defun run-ccdfg-k (pre loop iterations init-state prev)
 
275
  (let* ((state1 (run-block-set pre init-state nil prev))
 
276
         (state2 (run-blocks-iters loop state1 iterations 
 
277
                                   (prefix (car (last (cadar (last loop))))))))
 
278
  state2))
 
279
 
 
280
;; run-pre, then run-loop for k iterations, then run-post
 
281
(defun run-ccdfg (pre loop post iterations init-state prev)
 
282
  (let* ((state1 (run-block-set pre init-state nil prev))
 
283
         (state2 (run-blocks-iters loop state1 iterations 
 
284
                                   (prefix (car (last (cadar (last loop)))))))
 
285
         (state3 (run-block-set post state2 nil
 
286
                                  (prefix (car (last (cadar (last post))))))))
 
287
    state3))
 
288