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-nameis a portable ASCII identifier as defined inatc, that is distinct from thesymbol-names of objects introduced by previous successful calls ofdefobject .

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 exceedingullong-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 `atc`.

A *constant expression term returning*

- A call of a function
<type>-<base>-const on a quoted integer, when<type> is amongsint uint slong ulong sllong ullong

<base> is amongdec oct hex

T is the C type corresponding to<type> and the quoted integer is non-negative and in the range ofT . This represents a C integer constant of the C type indicated by the name of the function, expressed in decimal, octal, or hexadecimal base. - A call of a function
<op>-<type> on a constant expression term returningU , when<op> is amongplus minus bitnot lognot

<type> is amongschar uchar sshort ushort sint uint slong ulong sllong ullong

T is the C type corresponding to the return type of<op>-<type> andU is the C type corresponding to<type> . This represents the C operator indicated by the name of the function applied to a value of the type indicated by the name of the function. The guard verification requirement ensures that the operator yields a well-defined result. These functions cover all the C unary operators (using the nomenclature in [C]). - A call of a function
<op>-<type1>-<type2> on constant expression terms returningU andV , when<op> is amongadd sub mul div rem shl shr lt gt le ge eq ne bitand bitxor bitior

<type1> and<type2> are amongschar uchar sshort ushort sint uint slong ulong sllong ullong

T is the C type corresponding to the return type of<op>-<type1>-<type2> ,U is the C type corresponding to<type1> , andV is the C type corresponding to<type2> . This represents the C operator indicated by the name of the function applied to values of the types indicated by the name of the function. The guard verification requirement ensures that the operator yields a well-defined result. These functions cover all the C strict pure binary operators; the non-strict operators&& and|| , and the non-pure operators= ,+= , etc., are represented differently. - A call of a function
<type1>-from-<type2> on a constant expression term returningU , when<type1> and<type2> are amongschar uchar sshort ushort sint uint slong ulong sllong ullong

T is the C type corresponding to<type1> andU is the C type corresponding to<type2> . This represents a cast to the type indicated by the first part of the function name. The guard verification requirement ensures that the conversion yields a well-defined result. Even though conversions happen automatically in certain circumstances in C, these functions always represent explicit casts; implict conversions are represented implicitly, e.g. via the function for a unary operator that promotes the operand.

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 .

- Defobject-implementation
- Implementation of
`defobject`.