• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
      • B*
      • Defunc
      • Fty
        • Deftagsum
        • Defprod
        • Defflexsum
        • Defbitstruct
          • Deflist
          • Defalist
          • Defbyte
          • Deffixequiv
          • Defresult
          • Deffixtype
          • Defoption
          • Fty-discipline
          • Fold
          • Fty-extensions
          • Defsubtype
          • Defset
          • Deftypes
          • Specific-types
          • 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
      • 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
                • Defset
                • Deftypes
                • Specific-types
                • 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
          • Interfacing-tools
        • 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))