← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/centaur/vl/transforms/xf-unparam-check.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/centaur/vl/transforms/xf-unparam-check.lisp
 
1
; VL Verilog Toolkit
 
2
; Copyright (C) 2008-2014 Centaur Technology
 
3
;
 
4
; Contact:
 
5
;   Centaur Technology Formal Verification Group
 
6
;   7600-C N. Capital of Texas Highway, Suite 300, Austin, TX 78731, USA.
 
7
;   http://www.centtech.com/
 
8
;
 
9
; License: (An MIT/X11-style license)
 
10
;
 
11
;   Permission is hereby granted, free of charge, to any person obtaining a
 
12
;   copy of this software and associated documentation files (the "Software"),
 
13
;   to deal in the Software without restriction, including without limitation
 
14
;   the rights to use, copy, modify, merge, publish, distribute, sublicense,
 
15
;   and/or sell copies of the Software, and to permit persons to whom the
 
16
;   Software is furnished to do so, subject to the following conditions:
 
17
;
 
18
;   The above copyright notice and this permission notice shall be included in
 
19
;   all copies or substantial portions of the Software.
 
20
;
 
21
;   THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 
22
;   IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 
23
;   FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 
24
;   AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 
25
;   LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
 
26
;   FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
 
27
;   DEALINGS IN THE SOFTWARE.
 
28
;
 
29
; Original author: Jared Davis <jared@centtech.com>
 
30
 
 
31
(in-package "VL")
 
32
(include-book "../mlib/modnamespace")
 
33
(local (include-book "../util/arithmetic"))
 
34
(local (include-book "../util/osets"))
 
35
(local (std::add-default-post-define-hook :fix))
 
36
 
 
37
(defxdoc unparam-check
 
38
  :parents (transforms)
 
39
  :short "Sanity check for ensuring that parameters aren't shadowed by local
 
40
declarations within functions, tasks, or other statements."
 
41
 
 
42
  :long "<p>To keep @(see unparameterization) simple, we don't try to support
 
43
modules where parameter names are shadowed by local names within functions,
 
44
tasks, and other named statements within, e.g., always or initial blocks.</p>
 
45
 
 
46
<p>This is a simple transformation that looks for modules that have any such
 
47
name clashes, and adds fatal warnings to them.</p>")
 
48
 
 
49
(local (xdoc::set-default-parents unparam-check))
 
50
 
 
51
(defprojection vl-blockitemlist->names ((x vl-blockitemlist-p))
 
52
  :returns (names string-listp)
 
53
  (vl-blockitem->name x))
 
54
 
 
55
(defines vl-stmt-localnames-nrev
 
56
  :flag-local nil
 
57
 
 
58
  (define vl-stmt-localnames-nrev ((x vl-stmt-p) nrev)
 
59
    :measure (vl-stmt-count x)
 
60
    :flag :stmt
 
61
    (b* (((when (vl-atomicstmt-p x))
 
62
          (nrev-fix nrev))
 
63
         (nrev (vl-blockitemlist->names-nrev (vl-compoundstmt->decls x) nrev))
 
64
         (nrev (vl-stmtlist-localnames-nrev (vl-compoundstmt->stmts x) nrev)))
 
65
      nrev))
 
66
 
 
67
  (define vl-stmtlist-localnames-nrev ((x vl-stmtlist-p) nrev)
 
68
    :measure (vl-stmtlist-count x)
 
69
    :flag :list
 
70
    (b* (((when (atom x))
 
71
          (nrev-fix nrev))
 
72
         (nrev (vl-stmt-localnames-nrev (car x) nrev))
 
73
         (nrev (vl-stmtlist-localnames-nrev (cdr x) nrev)))
 
74
      nrev)))
 
75
 
 
76
(defines vl-stmt-localnames
 
77
 
 
78
  (define vl-stmt-localnames
 
79
    ((x vl-stmt-p))
 
80
    :returns (names string-listp)
 
81
    :measure (vl-stmt-count x)
 
82
    :verify-guards nil
 
83
    (mbe :logic
 
84
         (if (vl-atomicstmt-p x)
 
85
             nil
 
86
           (append (vl-blockitemlist->names (vl-compoundstmt->decls x))
 
87
                   (vl-stmtlist-localnames (vl-compoundstmt->stmts x))))
 
88
         :exec
 
89
         (with-local-nrev (vl-stmt-localnames-nrev x nrev))))
 
90
 
 
91
  (define vl-stmtlist-localnames
 
92
    ((x vl-stmtlist-p))
 
93
    :returns (names string-listp)
 
94
    :measure (vl-stmtlist-count x)
 
95
    (mbe :logic (if (atom x)
 
96
                    nil
 
97
                  (append (vl-stmt-localnames (car x))
 
98
                          (vl-stmtlist-localnames (cdr x))))
 
99
         :exec
 
100
         (with-local-nrev (vl-stmtlist-localnames-nrev x nrev))))
 
101
  ///
 
102
  (defthm-vl-stmt-localnames-nrev-flag
 
103
    (defthm vl-stmt-localnames-nrev-removal
 
104
      (equal (vl-stmt-localnames-nrev x nrev)
 
105
             (append nrev (vl-stmt-localnames x)))
 
106
      :flag :stmt)
 
107
    (defthm vl-stmtlist-localnames-nrev-removal
 
108
      (equal (vl-stmtlist-localnames-nrev x nrev)
 
109
             (append nrev (vl-stmtlist-localnames x)))
 
110
      :flag :list)
 
111
    :hints(("Goal"
 
112
            :expand ((vl-stmt-localnames x)
 
113
                     (vl-stmtlist-localnames x)
 
114
                     (vl-stmt-localnames-nrev x nrev)
 
115
                     (vl-stmtlist-localnames-nrev x nrev)))))
 
116
 
 
117
  (verify-guards vl-stmtlist-localnames)
 
118
  (deffixequiv-mutual vl-stmt-localnames))
 
119
 
 
120
(define vl-fundecl-localnames-nrev ((x vl-fundecl-p) nrev)
 
121
  (b* (((vl-fundecl x) x)
 
122
       (nrev (vl-portdecllist->names-nrev x.portdecls nrev))
 
123
       (nrev (vl-blockitemlist->names-nrev x.decls nrev))
 
124
       (nrev (vl-stmt-localnames-nrev x.body nrev)))
 
125
    nrev))
 
126
 
 
127
(define vl-fundecl-localnames ((x vl-fundecl-p))
 
128
  :returns (names string-listp)
 
129
  :verify-guards nil
 
130
  (mbe :logic
 
131
       (b* (((vl-fundecl x) x))
 
132
         (append (vl-portdecllist->names x.portdecls)
 
133
                 (vl-blockitemlist->names x.decls)
 
134
                 (vl-stmt-localnames x.body)))
 
135
       :exec
 
136
       (with-local-nrev
 
137
         (vl-fundecl-localnames-nrev x nrev)))
 
138
  ///
 
139
  (defthm vl-fundecl-localnames-nrev-removal
 
140
    (equal (vl-fundecl-localnames-nrev x nrev)
 
141
           (append nrev (vl-fundecl-localnames x)))
 
142
    :hints(("Goal" :in-theory (enable vl-fundecl-localnames-nrev))))
 
143
 
 
144
  (verify-guards vl-fundecl-localnames))
 
145
 
 
146
(defmapappend vl-fundecllist-localnames (x)
 
147
  (vl-fundecl-localnames x)
 
148
  :guard (vl-fundecllist-p x)
 
149
  :rest
 
150
  ((defthm string-listp-of-vl-fundecllist-localnames
 
151
     (string-listp (vl-fundecllist-localnames x)))))
 
152
 
 
153
(define vl-taskdecl-localnames-nrev ((x vl-taskdecl-p) nrev)
 
154
  (b* (((vl-taskdecl x) x)
 
155
       (nrev (vl-portdecllist->names-nrev x.portdecls nrev))
 
156
       (nrev (vl-blockitemlist->names-nrev x.decls nrev))
 
157
       (nrev (vl-stmt-localnames-nrev x.body nrev)))
 
158
    nrev))
 
159
 
 
160
(define vl-taskdecl-localnames ((x vl-taskdecl-p))
 
161
  :returns (names string-listp)
 
162
  :verify-guards nil
 
163
  (mbe :logic
 
164
       (b* (((vl-taskdecl x) x))
 
165
         (append (vl-portdecllist->names x.portdecls)
 
166
                 (vl-blockitemlist->names x.decls)
 
167
                 (vl-stmt-localnames x.body)))
 
168
       :exec
 
169
       (with-local-nrev
 
170
         (vl-taskdecl-localnames-nrev x nrev)))
 
171
  ///
 
172
  (defthm vl-taskdecl-localnames-nrev-removal
 
173
    (equal (vl-taskdecl-localnames-nrev x nrev)
 
174
           (append nrev (vl-taskdecl-localnames x)))
 
175
    :hints(("Goal" :in-theory (enable vl-taskdecl-localnames-nrev))))
 
176
 
 
177
  (verify-guards vl-taskdecl-localnames))
 
178
 
 
179
(defmapappend vl-taskdecllist-localnames (x)
 
180
  (vl-taskdecl-localnames x)
 
181
  :guard (vl-taskdecllist-p x)
 
182
  :rest
 
183
  ((defthm string-listp-of-vl-taskdecllist-localnames
 
184
     (string-listp (vl-taskdecllist-localnames x)))))
 
185
 
 
186
(define vl-always-localnames-nrev ((x vl-always-p) nrev)
 
187
  (b* (((vl-always x) x))
 
188
    (vl-stmt-localnames-nrev x.stmt nrev)))
 
189
 
 
190
(define vl-always-localnames ((x vl-always-p))
 
191
  :returns (names string-listp)
 
192
  :verify-guards nil
 
193
  (mbe :logic
 
194
       (b* (((vl-always x) x))
 
195
         (vl-stmt-localnames x.stmt))
 
196
       :exec
 
197
       (with-local-nrev
 
198
         (vl-always-localnames-nrev x nrev)))
 
199
  ///
 
200
  (defthm vl-always-localnames-nrev-removal
 
201
    (equal (vl-always-localnames-nrev x nrev)
 
202
           (append nrev (vl-always-localnames x)))
 
203
    :hints(("Goal" :in-theory (enable vl-always-localnames-nrev))))
 
204
 
 
205
  (verify-guards vl-always-localnames))
 
206
 
 
207
(defmapappend vl-alwayslist-localnames (x)
 
208
  (vl-always-localnames x)
 
209
  :guard (vl-alwayslist-p x)
 
210
  :rest
 
211
  ((defthm string-listp-of-vl-alwayslist-localnames
 
212
     (string-listp (vl-alwayslist-localnames x)))))
 
213
 
 
214
 
 
215
(define vl-initial-localnames-nrev ((x vl-initial-p) nrev)
 
216
  (b* (((vl-initial x) x))
 
217
    (vl-stmt-localnames-nrev x.stmt nrev)))
 
218
 
 
219
(define vl-initial-localnames ((x vl-initial-p))
 
220
  :returns (names string-listp)
 
221
  :verify-guards nil
 
222
  (mbe :logic
 
223
       (b* (((vl-initial x) x))
 
224
         (vl-stmt-localnames x.stmt))
 
225
       :exec
 
226
       (with-local-nrev
 
227
         (vl-initial-localnames-nrev x nrev)))
 
228
  ///
 
229
  (defthm vl-initial-localnames-nrev-removal
 
230
    (equal (vl-initial-localnames-nrev x nrev)
 
231
           (append nrev (vl-initial-localnames x)))
 
232
    :hints(("Goal" :in-theory (enable vl-initial-localnames-nrev))))
 
233
 
 
234
  (verify-guards vl-initial-localnames))
 
235
 
 
236
(defmapappend vl-initiallist-localnames (x)
 
237
  (vl-initial-localnames x)
 
238
  :guard (vl-initiallist-p x)
 
239
  :rest
 
240
  ((defthm string-listp-of-vl-initiallist-localnames
 
241
     (string-listp (vl-initiallist-localnames x)))))
 
242
 
 
243
(define vl-module-localnames
 
244
  :short "Collect up names that are used as local names within functions,
 
245
          tasks, and other statements."
 
246
  ((x vl-module-p))
 
247
  :returns (localnames string-listp)
 
248
  (b* (((vl-module x) x))
 
249
    (append (vl-taskdecllist-localnames x.taskdecls)
 
250
            (vl-fundecllist-localnames x.fundecls)
 
251
            (vl-alwayslist-localnames x.alwayses)
 
252
            (vl-initiallist-localnames x.initials))))
 
253
 
 
254
(define vl-module-unparam-check ((x vl-module-p))
 
255
  :returns (new-x vl-module-p)
 
256
  (b* (((vl-module x) (vl-module-fix x))
 
257
       ((when (vl-module->hands-offp x))
 
258
        x)
 
259
       ((unless (consp x.paramdecls))
 
260
        ;; Optimization: nothing to check, no need to gather local names.
 
261
        x)
 
262
 
 
263
       (localnames (mergesort (vl-module-localnames x)))
 
264
       (paramnames (mergesort (vl-paramdecllist->names x.paramdecls)))
 
265
       (overlap    (intersect localnames paramnames))
 
266
 
 
267
       ((unless overlap)
 
268
        ;; Fine, no overlap, no worries.
 
269
        x)
 
270
 
 
271
       (warnings (fatal :type :vl-unparam-fail
 
272
                        :msg "Cowardly refusing to attempt unparameterization ~
 
273
                              because some parameter names are shadowed ~
 
274
                              within functions, tasks, or other local blocks, ~
 
275
                              and this just seems error-prone: ~&0."
 
276
                        :args (list overlap)
 
277
                        :acc x.warnings)))
 
278
    (change-vl-module x :warnings warnings)))
 
279
 
 
280
(defprojection vl-modulelist-unparam-check ((x vl-modulelist-p))
 
281
  :returns (new-x vl-modulelist-p)
 
282
  (vl-module-unparam-check x))
 
283
 
 
284
(define vl-design-unparam-check ((x vl-design-p))
 
285
  :returns (new-x vl-design-p)
 
286
  (b* (((vl-design x) x))
 
287
    (change-vl-design x :mods (vl-modulelist-unparam-check x.mods))))
 
288