• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • 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
        • Make-event
        • Defmacro
        • Untranslate-patterns
        • Tc
        • Trans*
        • Macro-aliases-table
        • Macro-args
        • Defabbrev
        • User-defined-functions-table
        • Trans
        • Untranslate-for-execution
        • Add-macro-fn
        • Check-vars-not-free
        • Safe-mode
        • Macro-libraries
          • B*
          • Defunc
          • Fty
            • Deftagsum
            • Defprod
            • Defflexsum
            • Defbitstruct
              • Deflist
              • Defalist
              • Defbyte
              • Deffixequiv
              • Defresult
              • Deffixtype
              • Defoption
              • Fty-discipline
              • Fold
              • Fty-extensions
              • Defsubtype
              • Deftypes
              • Specific-types
              • Defset
              • Defflatsum
              • Deflist-of-len
              • Defbytelist
              • Defomap
              • Fty::basetypes
              • Defvisitors
              • Deffixtype-alias
              • Deffixequiv-sk
              • Defunit
              • Multicase
              • Deffixequiv-mutual
              • Fty::baselists
              • Def-enumcase
              • Defmap
            • Apt
            • Std/util
            • Defdata
            • Defrstobj
            • Seq
            • Match-tree
            • Defrstobj
            • With-supporters
            • Def-partial-measure
            • Template-subst
            • Soft
            • Defthm-domain
            • Event-macros
            • Def-universal-equiv
            • Def-saved-obligs
            • With-supporters-after
            • Definec
            • Sig
            • Outer-local
            • Data-structures
          • Trans1
          • Defmacro-untouchable
          • Set-duplicate-keys-action
          • Add-macro-alias
          • Magic-macroexpand
          • Defmacroq
          • Trans!
          • Remove-macro-fn
          • Remove-macro-alias
          • Add-binop
          • Untrans-table
          • Trans*-
          • Remove-binop
          • Tcp
          • Tca
        • Mailing-lists
        • Interfacing-tools
      • Macro-libraries
        • B*
        • Defunc
        • Fty
          • Deftagsum
          • Defprod
          • Defflexsum
          • Defbitstruct
            • Deflist
            • Defalist
            • Defbyte
            • Deffixequiv
            • Defresult
            • Deffixtype
            • Defoption
            • Fty-discipline
            • Fold
            • Fty-extensions
            • Defsubtype
            • Deftypes
            • Specific-types
            • Defset
            • Defflatsum
            • Deflist-of-len
            • Defbytelist
            • Defomap
            • Fty::basetypes
            • Defvisitors
            • Deffixtype-alias
            • Deffixequiv-sk
            • Defunit
            • Multicase
            • Deffixequiv-mutual
            • Fty::baselists
            • Def-enumcase
            • Defmap
          • Apt
          • Std/util
          • Defdata
          • Defrstobj
          • Seq
          • Match-tree
          • Defrstobj
          • With-supporters
          • Def-partial-measure
          • Template-subst
          • Soft
          • Defthm-domain
          • Event-macros
          • Def-universal-equiv
          • Def-saved-obligs
          • With-supporters-after
          • Definec
          • Sig
          • Outer-local
          • Data-structures
        • Interfacing-tools
        • Hardware-verification
        • Software-verification
        • Math
        • Testing-utilities
      • Fty

      Defbitstruct

      Define a bitvector type with accessors for its fields.

      This macro defines a bitstruct type. A bitstruct can either be a base type, which is a single fixed-width integer, or a product type containing fields that are bits, Booleans, or other bitstructs. Such a product is represented as a single integer produced by concatenating all the fields together, where the first field is least significant.

      Examples:

      A bitstruct can be made up of single bits and Booleans. (The difference is only in the return type of the accessors and the input type of the updaters; the representation is the same.) The fields are ordered LSB first, so a is bit 0 of the representation and c is bit 2. This defines a predicate, fixing function, accessors, and a constructor similar to defprod, but also updaters such as !foo->a.

      (defbitstruct foo
        ((a bitp)
         (b booleanp)
         (c bitp)))

      A bitstruct can also contain fields that are other bitstructs. Here, the first field is a foo, which is three bits wide, so the b and c fields are bits 3 and 4, respectively. Also, since :signedp t was specified, the representation is signed: the product is represented as a 5-bit signed integer rather than a 5-bit natural.

      (defbitstruct bar
        ((myfoo foo-p)
         (b booleanp)
         (c bitp))
        :signedp t)

      A bitstruct can also be defined without any fields, giving only a width. These are mainly useful as fields of other bitstructs. This makes sense when the individual bits aren't meaningful, and their combined value is what's important. This defines a rounding-control as a 2-bit unsigned value.

      (defbitstruct rounding-control 2)

      Sometimes we may want to nest one bitstruct inside another, but also directly access the fields of the internal struct. Providing the :subfields keyword causes defbitstruct to produce direct accessors and updaters for the subfields of the nested struct. The following definition of mxcsr produces the usual accessors and updaters including mxcsr->flags and mxcsr->masks, but also mxcsr->ie and mxcsr->im, etc.

      (defbitstruct fp-flags
        ((ie bitp)
         (de bitp)
         (ze bitp)
         (oe bitp)
         (ue bitp)
         (pe bitp)))
      
      (defbitstruct mxcsr
        ((flags fp-flags :subfields (ie de ze oe ue pe))
         (daz bitp)
         (masks fp-flags :subfields (im dm zm om um pm))
         (rc  rounding-control)
         (ftz bitp)))
      Syntax

      A defbitstruct form is one of:

      (defbitstruct typename fields [ options ] )

      or

      (defbitstruct typename width [ options ] ).

      The syntax of fields is described below.

      Top-level options
      • :pred, :fix, :equiv -- override the default names (foo-p, foo-fix, and foo-equiv) for the predicate, fixing function, and equivalence relation.
      • :parents, :short, :long -- provide xdoc for the bitstruct
      • :signedp -- when true, represents the structure as a signed integer rather than an unsigned one. (Signed and unsigned fields can be used inside unsigned and signed bitstructs -- they are simply sign- or zero-extended as necessary when accessed.)
      • :msb-first -- when non-NIL, reverses the order of the top-level fields, it does not reverse :subfield accessors/updaters.
      • :extra-binder-args -- a list of symbols that, in addition to the fields, will be accessible through the generated B* binder once corresponding accessor functions are defined. For example if we define a bitstruct foo with :extra-binder-args (bar), then once the function foo->bar is defined, the B* binder (b* (((foo x))) ...) will allow access to (foo->bar x) via variable x.bar.
      Field Syntax

      A field has the following form:

      (fieldname type [ docstring ] [ options ... ] )

      The type can be either a predicate or type name, i.e., bit or bitp, and must refer to either a single-bit type (bit or boolean) or a previously-defined bitstruct type. The docstring is a string which may contain xdoc syntax.

      Field Options
      • :accessor, :updater -- override the default names struct->field, !struct->field for the accessor and updater functions.
      • :default -- change the default value for the field in the make-foo macro. The default default is NIL for Boolean fields and 0 for everything else.
      • :rule-classes -- override the rule classes of the accessor function's return type theorem. The default is :rewrite; it may be appealing to use :type-prescription, but typically the type prescription for the accessor should be determined automatically anyway.
      • :subfields -- Indicates that accessors and updaters should be created for subfields of this field, and gives their subfield names. See the section on subfields below.
      Subfields

      The :subfields field option may only be used on a field whose type is itself a bitstruct type containing fields. The value of the :subfields argument should be a list of subfield_entries, according to the following syntax:

      subfield_entry ::= name | ( name ( subfield_entry ... ) )

      Each top-level entry corresponds to a subfield of the field type. If the entry uses the second syntax, which itself has a list of entries, those entries correspond to sub-subfields of the subfield type. For example:

      (defbitstruct innermost
        ((aa bitp)
         (bb bitp)))
      
      (defbitstruct midlevel
        ((ii innermost :subfields (iaa ibb))
         (qq bitp)
         (jj innermost :subfields (jaa jbb))))
      
      (defbitstruct toplevel
        ((ss innermost :subfields (saa sbb))
         (tt midlevel  :subfields ((tii (tiaa tibb))
                                   tqq
                                   tjj))))

      For the toplevel bitstruct, this generates the following subfield accessors, in addition to the direct accessors toplevel->ss and toplevel->tt:

      (toplevel->saa x)    == (innermost->aa (toplevel->ss x))
      (toplevel->sbb x)    == (innermost->bb (toplevel->ss x))
      (toplevel->tii x)    == (midlevel->ii (toplevel->tt x))
      (toplevel->tiaa x)   == (innermost->aa (midlevel->ii (toplevel->tt x)))
      (toplevel->tibb x)   == (innermost->bb (midlevel->ii (toplevel->tt x)))
      (toplevel->tqq x)    == (midlevel->qq (toplevel->tt x))
      (toplevel->tjj x)    == (midlevel->jj (toplevel->tt x))