• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
      • Operational-semantics
      • Real
      • Start-here
      • Debugging
      • Miscellaneous
      • Output-controls
      • Macros
      • Interfacing-tools
        • Io
          • Fmt
          • Msg
          • Cw
          • Set-evisc-tuple
          • Set-iprint
          • Print-control
          • Read-file-into-string
          • Std/io
            • Open-channel-lemmas
            • Std/io/read-char$
            • Std/io/read-object
            • Std/io/open-output-channel
            • Unsound-read
            • Read-string
            • Read-bytes$
              • Read-64ule
              • Read-64ube
              • Read-64sle
              • Read-64sbe
              • Read-32ule
              • Read-32sle
              • Read-32sbe
              • Read-32ube
              • Read-16sle
              • Read-16sbe
              • Read-16ule
              • Read-16ube
              • Read-8s
              • Combine-functions
            • File-measure
            • Read-bytes$-n
            • Std/io/read-byte$
            • Std/io/open-input-channel
            • Read-file-lines-no-newlines
            • Print-compressed
            • Nthcdr-bytes
            • Read-file-lines
            • Std/io/close-output-channel
            • Read-file-characters
            • Read-file-bytes
            • Print-legibly
            • Std/io/close-input-channel
            • Read-file-objects
            • Logical-story-of-io
            • Take-bytes
            • Std/io/peek-char$
            • Read-file-characters-rev
            • Read-file-as-string
            • Std/io/write-byte$
            • Std/io/set-serialize-character
            • Std/io/print-object$
            • Std/io/princ$
            • Std/io/read-file-into-string
            • *file-types*
          • Msgp
          • Printing-to-strings
          • Evisc-tuple
          • Output-controls
          • Observation
          • *standard-co*
          • Ppr-special-syms
          • Standard-oi
          • Standard-co
          • Without-evisc
          • Serialize
          • Output-to-file
          • Fmt-to-comment-window
          • Princ$
          • Character-encoding
          • Open-output-channel!
          • Cw-print-base-radix
          • Set-print-case
          • Set-print-base
          • Print-object$
          • Extend-pathname
          • Print-object$+
          • Fmx-cw
          • Set-print-radix
          • Set-fmt-hard-right-margin
          • File-write-date$
          • Proofs-co
          • Set-print-base-radix
          • Print-base-p
          • *standard-oi*
          • Wof
          • File-length$
          • Fms!-lst
          • Delete-file$
          • *standard-ci*
          • Write-list
          • Trace-co
          • Fmt!
          • Fms
          • Cw!
          • Fmt-to-comment-window!
          • Fms!
          • Eviscerate-hide-terms
          • Fmt1!
          • Fmt-to-comment-window!+
          • Read-file-into-byte-array-stobj
          • Fmt1
          • Fmt-to-comment-window+
          • Cw-print-base-radix!
          • Read-file-into-character-array-stobj
          • Fmx
          • Cw!+
          • Read-objects-from-book
          • Newline
          • Cw+
          • Probe-file
          • Write-objects-to-file!
          • Write-objects-to-file
          • Read-objects-from-file
          • Read-object-from-file
          • Read-file-into-byte-list
          • Set-fmt-soft-right-margin
          • Read-file-into-character-list
          • Io-utilities
        • Defttag
        • Sys-call
        • Save-exec
        • Quicklisp
        • Std/io
          • Open-channel-lemmas
          • Std/io/read-char$
          • Std/io/read-object
          • Std/io/open-output-channel
          • Unsound-read
          • Read-string
          • Read-bytes$
            • Read-64ule
            • Read-64ube
            • Read-64sle
            • Read-64sbe
            • Read-32ule
            • Read-32sle
            • Read-32sbe
            • Read-32ube
            • Read-16sle
            • Read-16sbe
            • Read-16ule
            • Read-16ube
            • Read-8s
            • Combine-functions
          • File-measure
          • Read-bytes$-n
          • Std/io/read-byte$
          • Std/io/open-input-channel
          • Read-file-lines-no-newlines
          • Print-compressed
          • Nthcdr-bytes
          • Read-file-lines
          • Std/io/close-output-channel
          • Read-file-characters
          • Read-file-bytes
          • Print-legibly
          • Std/io/close-input-channel
          • Read-file-objects
          • Logical-story-of-io
          • Take-bytes
          • Std/io/peek-char$
          • Read-file-characters-rev
          • Read-file-as-string
          • Std/io/write-byte$
          • Std/io/set-serialize-character
          • Std/io/print-object$
          • Std/io/princ$
          • Std/io/read-file-into-string
          • *file-types*
        • Oslib
        • Bridge
        • Clex
        • Tshell
        • Unsound-eval
        • Hacker
        • ACL2s-interface
        • Startup-banner
        • Command-line
    • Interfacing-tools
      • Io
        • Fmt
        • Msg
        • Cw
        • Set-evisc-tuple
        • Set-iprint
        • Print-control
        • Read-file-into-string
        • Std/io
          • Open-channel-lemmas
          • Std/io/read-char$
          • Std/io/read-object
          • Std/io/open-output-channel
          • Unsound-read
          • Read-string
          • Read-bytes$
            • Read-64ule
            • Read-64ube
            • Read-64sle
            • Read-64sbe
            • Read-32ule
            • Read-32sle
            • Read-32sbe
            • Read-32ube
            • Read-16sle
            • Read-16sbe
            • Read-16ule
            • Read-16ube
            • Read-8s
            • Combine-functions
          • File-measure
          • Read-bytes$-n
          • Std/io/read-byte$
          • Std/io/open-input-channel
          • Read-file-lines-no-newlines
          • Print-compressed
          • Nthcdr-bytes
          • Read-file-lines
          • Std/io/close-output-channel
          • Read-file-characters
          • Read-file-bytes
          • Print-legibly
          • Std/io/close-input-channel
          • Read-file-objects
          • Logical-story-of-io
          • Take-bytes
          • Std/io/peek-char$
          • Read-file-characters-rev
          • Read-file-as-string
          • Std/io/write-byte$
          • Std/io/set-serialize-character
          • Std/io/print-object$
          • Std/io/princ$
          • Std/io/read-file-into-string
          • *file-types*
        • Msgp
        • Printing-to-strings
        • Evisc-tuple
        • Output-controls
        • Observation
        • *standard-co*
        • Ppr-special-syms
        • Standard-oi
        • Standard-co
        • Without-evisc
        • Serialize
        • Output-to-file
        • Fmt-to-comment-window
        • Princ$
        • Character-encoding
        • Open-output-channel!
        • Cw-print-base-radix
        • Set-print-case
        • Set-print-base
        • Print-object$
        • Extend-pathname
        • Print-object$+
        • Fmx-cw
        • Set-print-radix
        • Set-fmt-hard-right-margin
        • File-write-date$
        • Proofs-co
        • Set-print-base-radix
        • Print-base-p
        • *standard-oi*
        • Wof
        • File-length$
        • Fms!-lst
        • Delete-file$
        • *standard-ci*
        • Write-list
        • Trace-co
        • Fmt!
        • Fms
        • Cw!
        • Fmt-to-comment-window!
        • Fms!
        • Eviscerate-hide-terms
        • Fmt1!
        • Fmt-to-comment-window!+
        • Read-file-into-byte-array-stobj
        • Fmt1
        • Fmt-to-comment-window+
        • Cw-print-base-radix!
        • Read-file-into-character-array-stobj
        • Fmx
        • Cw!+
        • Read-objects-from-book
        • Newline
        • Cw+
        • Probe-file
        • Write-objects-to-file!
        • Write-objects-to-file
        • Read-objects-from-file
        • Read-object-from-file
        • Read-file-into-byte-list
        • Set-fmt-soft-right-margin
        • Read-file-into-character-list
        • Io-utilities
      • Defttag
      • Sys-call
      • Save-exec
      • Quicklisp
      • Std/io
        • Open-channel-lemmas
        • Std/io/read-char$
        • Std/io/read-object
        • Std/io/open-output-channel
        • Unsound-read
        • Read-string
        • Read-bytes$
          • Read-64ule
          • Read-64ube
          • Read-64sle
          • Read-64sbe
          • Read-32ule
          • Read-32sle
          • Read-32sbe
          • Read-32ube
          • Read-16sle
          • Read-16sbe
          • Read-16ule
          • Read-16ube
          • Read-8s
          • Combine-functions
        • File-measure
        • Read-bytes$-n
        • Std/io/read-byte$
        • Std/io/open-input-channel
        • Read-file-lines-no-newlines
        • Print-compressed
        • Nthcdr-bytes
        • Read-file-lines
        • Std/io/close-output-channel
        • Read-file-characters
        • Read-file-bytes
        • Print-legibly
        • Std/io/close-input-channel
        • Read-file-objects
        • Logical-story-of-io
        • Take-bytes
        • Std/io/peek-char$
        • Read-file-characters-rev
        • Read-file-as-string
        • Std/io/write-byte$
        • Std/io/set-serialize-character
        • Std/io/print-object$
        • Std/io/princ$
        • Std/io/read-file-into-string
        • *file-types*
      • Oslib
      • Bridge
      • Clex
      • Tshell
      • Unsound-eval
      • Hacker
      • ACL2s-interface
      • Startup-banner
      • Command-line
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Std/io

Read-bytes$

Flexible macro for reading and combining 1, 2, 4, or 8 bytes from an open :byte input stream into a single value.

General form:

(read-bytes$ channel
             [:bytes bytes]    ;; default: 1
             [:signed signed]  ;; default: nil
             [:end end]        ;; default: :big
             )
  -->
(mv value state)
  • If you provide bytes, it must be explicitly 1, 2, 4, or 8.
  • If you provide signed, it must be either t or nil.
  • If you provide end, it must be either :big or :little. (For the 1-byte readers, end does not matter.)

Read-byte$ is a macro that expands into the appropriate function from the table below.

  Name         Bytes Read    Value Range        Endian-ness
---------------------------------------------------------------
  read-byte$   1             [0, 2^8-1]         N/A
  read-8s      1             [-2^7, 2^7-1]      N/A

  read-16ube   2             [0, 2^16-1]        Big Endian
  read-16ule   2             [0, 2^16-1]        Little Endian
  read-16sbe   2             [-2^15, 2^15-1]    Big Endian
  read-16sle   2             [-2^15, 2^15-1]    Little Endian

  read-32ube   4             [0, 2^32-1]        Big Endian
  read-32ule   4             [0, 2^32-1]        Little Endian
  read-32sbe   4             [-2^31, 2^31-1]    Big Endian
  read-32sle   4             [-2^31, 2^31-1]    Little Endian

  read-64ube   8             [0, 2^64-1]        Big Endian
  read-64ule   8             [0, 2^64-1]        Little Endian
  read-64sbe   8             [-2^63, 2^63-1]    Big Endian
  read-64sle   8             [-2^63, 2^63-1]    Little Endian
---------------------------------------------------------------

Subtopics

Read-64ule
(read-64ule channel state) reads a 64-bit, unsigned, little-endian value from the input channel.
Read-64ube
(read-64ube channel state) reads a 64-bit, unsigned, big-endian value from the input channel.
Read-64sle
(read-64sle channel state) reads a 64-bit, signed, big-endian value from the input channel.
Read-64sbe
(read-64sbe channel state) reads a 64-bit, signed, big-endian value from the input channel.
Read-32ule
(read-32ule channel state) reads a 32-bit, unsigned, little-endian value from the input channel.
Read-32sle
(read-32sle channel state) reads a 32-bit, signed, little-endian value from the input channel.
Read-32sbe
(read-32sbe channel state) reads a 32-bit, signed, big-endian value from the input channel.
Read-32ube
(read-32ube channel state) reads a 32-bit, unsigned, big-endian value from the input channel.
Read-16sle
(read-16sle channel state) reads a 16-bit, signed, little-endian value from the input channel.
Read-16sbe
(read-16sbe channel state) reads a 16-bit, signed, big-endian value from the input channel.
Read-16ule
(read-16ule channel state) reads a 16-bit, unsigned, little-endian value from the input channel.
Read-16ube
(read-16ube channel state) reads a 16-bit, unsigned, big-endian value from the input channel.
Read-8s
(read-8s channel state) reads a signed byte from the input channel.
Combine-functions
Optimized byte-combining functions.