• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
        • Vl-lint
        • Vl-server
        • Vl-gather
        • Vl-zip
          • Vl-zip-opts-p
          • Vl-zipfile
            • Vl-zipfile-fix
            • Vl-read-zip-header
            • Vl-maybe-zipfile
            • Vl-read-zip
            • Make-vl-zipfile
            • Vl-zipfile-equiv
            • Vl-zipfile-p
            • Change-vl-zipfile
            • Vl-zipfile->filemap
            • Vl-zipfile->defines
            • Vl-zipfile->syntax
            • Vl-zipfile->name
            • Vl-zipfile->ltime
            • Vl-zipfile->design
            • Vl-zipfile->date
            • Vl-write-zip
          • *vl-zip-help*
          • Vl-zip-top
          • Vl-zip-main
        • Vl-main
        • Split-plusargs
        • Vl-shell
        • Vl-json
      • Mlib
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Vl-zipfile

Vl-read-zip

Read a whole vlzip file.

Signature

(vl-read-zip filename &key (state 'state)) 
  → 
(mv errmsg zip new-state)

Arguments

filename — Guard (stringp filename).

Returns

errmsg — NIL on failure or a msg on any error.

zip — Type (iff (vl-zipfile-p zip) (not errmsg)).

new-state — Type (state-p1 new-state), given (state-p1 state).

Definitions and Theorems

Function: vl-read-zip-fn

(defun
 vl-read-zip-fn (filename state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (stringp filename)))
 (let
  ((__function__ 'vl-read-zip))
  (declare (ignorable __function__))
  (b*
   ((filename (string-fix filename))
    ((mv channel state)
     (open-input-channel filename
                         :object state))
    ((unless channel)
     (mv (msg "Can't load ~x0: error opening file."
              filename)
         nil state))
    ((mv alist state)
     (vl-read-zip-aux channel nil state))
    (state (close-input-channel channel state)))
   (cwtime
    (b*
     (((assocs (name :name)
               (syntax :syntax)
               (date :date)
               (ltime :ltime)
               (design :design)
               (filemap :filemap)
               (defines :defines))
       alist)
      ((unless (stringp name))
       (mv (msg "Can't load ~x0: missing or invalid :name~%"
                filename)
           nil state))
      ((unless (stringp syntax))
       (mv (msg "Can't load ~x0: missing or invalid :syntax~%"
                filename)
           nil state))
      ((unless (equal syntax *vl-current-syntax-version*))
       (mv
        (msg
         "Can't load ~x0: incompatible vl syntax version.~%   ~
                      - The file uses syntax version   ~s1~%   ~
                      - Current VL syntax version      ~s2~%"
         filename
         syntax *vl-current-syntax-version*)
        nil state))
      ((unless (stringp date))
       (mv (msg "Can't load ~x0: missing or invalid :date~%"
                filename)
           nil state))
      ((unless (natp ltime))
       (mv (msg "Can't load ~x0: missing or invalid :ltime~%"
                filename)
           nil state))
      ((unless (vl-design-p design))
       (mv (msg "Can't load ~x0: missing or invalid :design~%"
                filename)
           nil state))
      ((unless (vl-filemap-p filemap))
       (mv (msg "Can't load ~x0: invalid :filemap~%"
                filename)
           nil state))
      ((unless (vl-defines-p defines))
       (mv (msg "Can't load ~x0: invalid :defines~%"
                filename)
           nil state))
      (zip (make-vl-zipfile :name name
                            :syntax syntax
                            :date date
                            :ltime ltime
                            :design design
                            :filemap filemap
                            :defines defines)))
     (mv nil zip state))
    :mintime 1))))

Theorem: return-type-of-vl-read-zip.zip

(defthm return-type-of-vl-read-zip.zip
        (b* (((mv ?errmsg acl2::?zip ?new-state)
              (vl-read-zip-fn filename state)))
            (iff (vl-zipfile-p zip) (not errmsg)))
        :rule-classes :rewrite)

Theorem: state-p1-of-vl-read-zip.new-state

(defthm state-p1-of-vl-read-zip.new-state
        (implies (state-p1 state)
                 (b* (((mv ?errmsg acl2::?zip ?new-state)
                       (vl-read-zip-fn filename state)))
                     (state-p1 new-state)))
        :rule-classes :rewrite)