← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/centaur/vl/transforms/always/stmtrewrite.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/always/stmtrewrite.lisp
29
29
; Original author: Jared Davis <jared@centtech.com>
30
30
 
31
31
(in-package "VL")
32
 
(include-book "../xf-resolve-ranges")
 
32
(include-book "../../mlib/consteval")
33
33
(include-book "../../mlib/stmt-tools")
 
34
(include-book "../../mlib/blocks")
34
35
(local (include-book "../../util/arithmetic"))
35
36
 
36
37
(defxdoc stmtrewrite
173
174
})
174
175
 
175
176
<p>We only try to unroll when @('n') is easily resolved to a constant that is
176
 
less than the @('unroll-limit').  In particular, we use @(see
177
 
vl-constexpr-reduce) to try to evaluate the condition.  This lets us handle
178
 
things like @('repeat(width-1) body') after @(see unparameterization) has
179
 
occurred.</p>"
 
177
less than the @('unroll-limit').  In particular, we use @(see vl-consteval) to
 
178
try to evaluate the condition.  This lets us handle things like
 
179
@('repeat(width-1) body') after @(see unparameterization) has occurred.</p>"
180
180
 
181
 
  (b* ((count (vl-constexpr-reduce condition))
 
181
  (b* (((mv ok count-expr) (vl-consteval condition nil))
 
182
       (count (and ok (vl-resolved->val count-expr)))
182
183
       ((when (and count (<= count unroll-limit)))
183
184
        (mv warnings
184
185
            ;; This works even when N is 0 or 1.  We expect our later block
257
258
 
258
259
 
259
260
(define vl-caselist-all-null-p ((x vl-caselist-p))
260
 
  (if (atom x)
261
 
      t
262
 
    (and (vl-nullstmt-p (cdar x))
263
 
         (vl-caselist-all-null-p (cdr x)))))
264
 
 
265
 
 
266
 
(define vl-casestmt-rewrite ((casetype vl-casetype-p)
267
 
                             (test    vl-expr-p)
268
 
                             (cases   vl-caselist-p)
269
 
                             (default vl-stmt-p)
270
 
                             (atts    vl-atts-p))
 
261
  (b* (((when (atom x))
 
262
        t)
 
263
       ((cons ?exprs stmt1) (first x)))
 
264
    (and (vl-nullstmt-p stmt1)
 
265
         (vl-caselist-all-null-p (rest x)))))
 
266
 
 
267
(define vl-casestmt-rewrite ((check    vl-casecheck-p)
 
268
                             (casetype vl-casetype-p)
 
269
                             (test     vl-expr-p)
 
270
                             (caselist vl-caselist-p)
 
271
                             (default  vl-stmt-p)
 
272
                             (atts     vl-atts-p))
271
273
  :returns (stmt vl-stmt-p :hyp :fguard)
272
274
  :short "Eliminate pure-null case statements."
273
275
  :long "<p>This is a pretty silly rewrite:</p>
274
276
@({
275
 
   case/casex/casez(expr):    -->   [null stmt]
 
277
   [priority/unique/unique0/nil] [case/casex/casez](expr):    -->   [null stmt]
276
278
     expr1 : [null stmt];
277
279
     expr2 : [null stmt];
278
280
     ...
287
289
anymore.</p>"
288
290
 
289
291
  (if (and (vl-nullstmt-p default)
290
 
           (vl-caselist-all-null-p cases))
 
292
           (vl-caselist-all-null-p caselist))
291
293
      ;; All statements are null, just turn into null.
292
294
      (make-vl-nullstmt)
293
295
    ;; Otherwise don't change it.  Eventually convert all case statements
294
296
    ;; into if statements?
295
 
    (make-vl-casestmt :casetype casetype
 
297
    (make-vl-casestmt :check check
 
298
                      :casetype casetype
296
299
                      :test test
297
 
                      :cases cases
 
300
                      :caselist caselist
298
301
                      :default default
299
302
                      :atts atts)))
300
303
 
580
583
 
581
584
            ((vl-casestmt-p x)
582
585
             (b* (((vl-casestmt x) x)
583
 
                  ((mv warnings cases)   (vl-caselist-rewrite x.cases unroll-limit warnings))
584
 
                  ((mv warnings default) (vl-stmt-rewrite x.default unroll-limit warnings))
585
 
                  (x-prime               (vl-casestmt-rewrite x.casetype x.test cases default x.atts)))
 
586
                  ((mv warnings caselist) (vl-caselist-rewrite x.caselist unroll-limit warnings))
 
587
                  ((mv warnings default)  (vl-stmt-rewrite x.default unroll-limit warnings))
 
588
                  (x-prime                (vl-casestmt-rewrite x.check x.casetype x.test caselist default x.atts)))
586
589
               (mv warnings x-prime)))
587
590
 
588
591
            ((vl-forstmt-p x)
726
729
            cdr-prime
727
730
          (cons car-prime cdr-prime)))))
728
731
 
 
732
(def-genblob-transform vl-genblob-stmtrewrite ((unroll-limit natp)
 
733
                                               (warnings vl-warninglist-p))
 
734
  :returns ((warnings vl-warninglist-p))
 
735
  ;; :verify-guards nil
 
736
  (b* (((vl-genblob x) x)
 
737
 
 
738
       (unroll-limit (lnfix unroll-limit))
 
739
       (warnings (vl-warninglist-fix warnings))
 
740
       ((mv warnings alwayses)
 
741
        (vl-alwayslist-stmtrewrite x.alwayses unroll-limit warnings))
 
742
       ((mv warnings initials)
 
743
        (vl-initiallist-stmtrewrite x.initials unroll-limit warnings))
 
744
 
 
745
       ((mv warnings generates)  (vl-generates-stmtrewrite x.generates unroll-limit warnings)))
 
746
 
 
747
    (mv warnings
 
748
        (change-vl-genblob
 
749
         x
 
750
         :alwayses alwayses
 
751
         :initials initials
 
752
         :generates generates)))
 
753
  :apply-to-generates vl-generates-stmtrewrite)
 
754
 
729
755
(define vl-module-stmtrewrite ((x            vl-module-p)
730
756
                               (unroll-limit natp))
731
757
  :returns (new-x vl-module-p :hyp :fguard)
732
758
  (b* (((vl-module x) x)
733
759
       ((when (vl-module->hands-offp x))
734
760
        x)
735
 
 
736
 
       ((unless (or x.alwayses x.initials))
737
 
       ;; Optimization: bail early on modules with no blocks.
738
 
        x)
739
 
 
740
 
       (warnings x.warnings)
741
 
       ((mv warnings alwayses)
742
 
        (vl-alwayslist-stmtrewrite x.alwayses unroll-limit warnings))
743
 
       ((mv warnings initials)
744
 
        (vl-initiallist-stmtrewrite x.initials unroll-limit warnings)))
745
 
    (change-vl-module x
746
 
                      :warnings warnings
747
 
                      :alwayses alwayses
748
 
                      :initials initials)))
 
761
       (genblob (vl-module->genblob x))
 
762
       ((mv warnings new-genblob) (vl-genblob-stmtrewrite genblob unroll-limit x.warnings))
 
763
       (x-warn (change-vl-module x :warnings warnings)))
 
764
    (vl-genblob->module new-genblob x-warn)))
749
765
 
750
766
(defprojection vl-modulelist-stmtrewrite (x unroll-limit)
751
767
  (vl-module-stmtrewrite x unroll-limit)