Defrstobj
Record-like stobjs combine the run-time efficiency of stobjs
with the reasoning efficiency of records. They are designed for modeling,
e.g., the state of a processor or virtual machine.
Defrstobj creates an abstract stobj where the concrete stobj
contains some user-specified scalar fields, fixed-length array fields, and child stobjs, but
the logical interface is that of a multityped record (see def-multityped-record). The executable accessors/updaters expand to calls of
a single multityped record accessor/updater so that only a small number of
theorems are needed for reasoning about reads over writes, and writes over
writes, etc.
This topic pertains only to rstobj2::defrstobj, defined in
centaur/defrstobj2/defrstobj.lisp. A previous version,
rstobj::defrstobj, is defined in centaur/defrstobj/defrstobj.lisp,
and another one before that in projects/legacy-defrstobj/defrstobj.lisp.
The main difference between this version and previous versions is the logical
interface. In previous versions the top-level stobj was an untyped record
containing certain keys (those corresponding to array fields) that were
uniformly typed records. In this version, the entire stobj is a multityped
record and the array contents are not their own subfields.
Invocation and Options
Example invocations:
(defrstobj myst
(u32-scalar :type (unsigned-byte 32) :initially 0 :fix (ec-call (acl2::loghead$inline 32 x)))
(u32-array :type (array (unsigned-byte 32) (16)) :initially 5 :fix (acl2::loghead 32 (ifix x)))
(nat-scalar :type (integer 0 *) :initially 6 :fix (nfix x))
(nat-array :type (array (integer 0 *) (12)) :initially 8 :fix (nfix x)))
(defrstobj parent
(parent-nat-scalar :type (integer 0 *) :initially 0 :fix (nfix x))
;; "Exporting" two fields from the child stobj into this parent stobj
(child-u32-array :type (array (unsigned-byte 32) (16))
:initially 5
:fix (acl2::loghead 32 (ifix x))
:child-stobj child
:child-accessor get-u32-array
:child-updater set-u32-array)
(child-u32-scalar :type (unsigned-byte 32)
:initially 0
:fix (acl2::loghead 32 (ifix x))
:child-stobj child
:child-accessor get-u32-scalar
:child-updater set-u32-scalar)
:enable '(get-u32-array-over-set-u32-array
get-u32-scalar-over-set-u32-scalar
get-u32-array-default-value
get-u32-scalar-default-value))
The first argument to defrstobj is the name of the abstract stobj
to generate; the rest of the arguments are field specifiers and top-level
keyword options, as follows:
- :recname -- name of the multityped record to generate, default <name>rec
- :inline -- inline the concrete stobj accessor/updaters; default T
- :non-memoizable -- declare the concrete stobj non-memoizable; default NIL
- :concrete-stobj -- name of the concrete stobj, default <name>$c
- :pkg-sym -- symbol in whose package all new names will be generated, default name
- :elem-p -- name of the element predicate function to be generated, default <name>-elem-p
- :elem-fix -- name of the element fixing function to be generated, default <name>-elem-fix
- :elem-default -- name of the element default function to be generated, default <name>-elem-default
- :logic-stobj -- variable name to use for the logical analogue of the
stobj in the logic definitions of the accessors and updaters; default
<name>$a
- :recognizer -- name of the stobj recognizer function; default <name>p
- :logic-recognizer -- logic version of the stobj recognizer function; default <logic-stobj>p
- :creator -- name of the stobj creator function; default create-<name>
- :logic-creator -- logic version of the stobj creator function; default create-<logic-stobj>
- :accessor-template -- list of symbols whose names will be concatenated
to generate the name of a field accessor, where acl2::x stands for the name of
a field; default (get- x)
- :updater-template -- list of symbols whose names will be concatenated
to generate the name of a field updater, where acl2::x stands for the name
of a field; default (set- x)
- :accessor -- name of the generic accessor; default is generated from
the accessor template by substituting name for x; therefore the
default for the default accessor template is get-<name>
- :updater -- name of the generic updater; default is generated from the
updater template by substituting name for x; therefore the default
for the default updater template is set-<name>.
Fields consist of a name followed by a keyword/value list where the
acceptable keys are the following:
- :type -- the stobj field type, such as string or
(array (integer 0 *) (12)), defaulting to t.
- :pred -- the element recognizer predicate, as an expression in terms
of x, where the default is generated from :type by applying
translate-declaration-to-guard. May be more specific than the stobj field
type.
- :fix -- the element fixing function, as an expression in terms of
x, defaulting to the identity x, which is only valid for untyped
fields
- :initially -- the initial value of the field or of an element for
array fields; default nil
- :accessor -- the name of the accessor for the field; default is
determined by the :accessor-template top-level argument
- :updater -- the name of the updater for the field; default is
determined by the :updater-template top-level argument
- :logic-accessor -- the logical version of the accessor function,
default <accessor>$a
- :logic-updater -- the logical version of the updater function,
default <updater>$a
- :child-stobj -- the name of a previously-introduced stobj
- :child-accessor -- the name of an accessor function of some
field of the child stobj
- :child-updater -- the name of an updater function of some
field of the child stobj
- :key -- the keyword corresponding to the field, for use as a key in
the typed record.
When a field is based off a child stobj, then defrstobj
requires certain theorems about the child stobj's accessors and
updaters to be made available to it using the top-level keyword option
:enable. Two kinds of theorems are expected:
- Non-interference Theorems -- standard accessor/updater
independence or read-over-write theorems. Also see stobjs::stobj-updater-independence and std/stobjs/nicestobj for
a possible strategy to adopt to prove these kinds of theorems.
- Default-value Theorems -- theorems stating that calling the
accessor on a stobj's creator function returns the default value.
Subtopics
- Def-multityped-record
- Introduce a multi-typed record for use with defrstobj.
