|
|
|---|
|
|
|
|---|
Define a shallowly embedded external object.
A more colloquial term for this is `global variable', i.e. a variable declared at the top level of a file, as opposed to a local variable, which is declared in a block. In more technical terms, a C translation unit consists of a sequence of external declarations [C:6.9], where an external declaration is either a function definition [C:6.9.1] or a declaration [C:6.7], where the latter may define an object [C:6.9.2]. Thus, a global variable is introduced as an external object definition.
This macro defines an external C object shallowly embedded in ACL2. The macro specifies the name, type, and optional initializer. The macro stores this information in a table, and generates a recognizer for the possible values of the object. A shallowly embedded C function that accesses the object is represented by an ACL2 function with a parameter that has the same name as the object and whose guard says that the parameter satisfies the generated recognizer. While the parameter has to be explicit in purely functional ACL2, the C function has no corresponding parameter, and instead accesses the object directly by name, since the object is in scope. The macro also generates a nullary function that returns the initial value of the object.
Currently this macro only supports objects of integer array types, but we plan to extend support to more types.
(defobject name :type ... :init ... )
Name of the externally defined object.
It must be a symbol whose symbol-name is a portable ASCII identifier as defined in atc, that is distinct from the symbol-names of objects introduced by previous successful calls of
defobject .
Type of the externally defined object.
It must be one of
schar uchar sshort ushort sint uint slong ulong sllong ullong (schar <size>) (uchar <size>) (sshort <size>) (ushort <size>) (sint <size>) (uint <size>) (slong <size>) (ulong <size>) (sllong <size>) (ullong <size>) where
<size> is a positive integer not exceeding ullong-max. Each of these represents either an integer type or an integer array type with the specified size, where the limit on the size is so that it can be represented by a C integer constant.
Initializer of the externally defined object.
It must be either of of the following (where the notion of constant expression term returning
T is defined later below):
nil , which is the default.- A constant expression terms returning
T , whereT is the integer type specified in the:type input, if the:type input specifies an integer type.- A list
(... ... ...) of constant expression terms returningT , whereT is the element type of the integer array type specified in the:type input, when the:type input specifies an integer array type.If this input is not
nil , it represents an initializer [C:6.7.9]. If this input isnil , the object declaration does not have an initializer.If this input is not
nil , its term or terms must be guard-verifiable. This requirement is checked implicitly by generating theobject-<name>-init function (see the `Generated Events' section below) via an event that requires its guard verification.
This is a restricted version of the notion of
pure expression terms defined in atc.
A pure expression term is an ACL2 term that represent
a C pure expression that may involve variables.
A constant expression term is an ACL2 term that represents
a C constant expression [C:6.6],
which does not involve variables.
Since there are no variables involved,
the notion of constant expression term is defined
without reference to any ACL2 function
A constant expression term returning
Recognizer of the possible values of the externally defined object.
This is defined as
;; if the object has integer type: (defun object-<name>-p (x) (<type>p x)) ;; if the object has integer array type: (defun object-<name>-p (x) (and (<type>-arrayp x) (equal (<type>-array-length x) <size>)))where
<name> is the name of the object specified in thename input and<type> is the integer fixtype name specified in the:type input. The recognizerobject-<name>-p is in the same package as thename input. The function is in logic mode and guard-verified; its guard verification is always expected to succeed.
Nullary function that returns the initializing value of the externally defined object.
This is defined as
;; if the object has integer type: (defun object-<name>-init () <term>) ;; if the object has integer array type: (defun object-<name>-init () (<type>-array-of (list <term1> <term2> ...)))where
<name> is the name of the object specified in thename input,<type> is the integer fixtype name specified in the:type input (either the integer type of the object, or the element type of the array type of the object),<term> is the term in the:init input (if the object has integer type and that input is notnil ), and<term1> ,<term2> , etc. are the terms in the list in the:init input (if the object has integer array type and that input is notnil ); if the:init input isnil , each term is(<type>-from-integer 0) , where<type> is the type or element type of the object, and where, in the case of the array, the term is repeated<size> times. These default initializers reflect the default initialization of external objects: an integer external object is initialized with 0 of the type, and an integer array external object is initialized with 0 values of the element type.The nullary function
object-<name>-init is in the same package as thename input. The function is in logic mode and guard-verified: its guard verification checks some of the requirements on the:init input mentioned in the `Inputs' section above, when that input is notnil .