• 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
          • Fty::basetypes
          • Defomap
          • 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
      • 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))