		Search-engine friendly clone of the ACL2 documentation.

Transformation-tools

Splitgso

A transformation to split a global struct object.

Introduction

This transformation targets a global struct object, i.e. a file-scope object, that has a struct type. The transformation splits it into two objects, of two new struct types, each with a subset of the original struct members, which are divided between the two new struct types (and objects). Member access expressions are replaced with new access expressions with the original object replaced with one of the new objects. The transformation will fail if the original object appears in any other sorts of expressions.

We only aim to preserve functional equivalence (up to the obvious isomorphism of data representation between the original and split struct objects) between the original and transformed programs. No consideration is given to performance, which may be affected by padding, locality, etc.

General Form

(splitgso const-old
          const-new
          :object-name       ...
          :split-members     ...
          :object-filepath   ... ; optional
          :new-object1       ... ; optional
          :new-object2       ... ; optional
          :new-type1         ... ; optional
          :new-type2         ... ; optional
  )

Inputs

const-old

Specifies the code to be transformed.
This must be a symbol that names an existing ACL2 constant that contains a validated translation unit ensemble, i.e. a value of type transunit-ensemble resulting from validation, and in particular containing validation information. This constant could result from c$::input-files, or from some other transformation.

const-new

Specifies the name of the constant for the transformed code.
This must be a symbol that is valid name for a new ACL2 constant.

:object-name — no default

A string denoting the identifier of the global struct object to split.

:split-members — no default

A string list denoting the identifiers representing the fields of the original struct type which should be "split" out into a new struct.

:object-filepath — optional

A string denoting the filepath of a translation unit. This is required when the target struct object has internal linkage in order to disambiguate the :object-name argument.

:new-object1 — optional

A string denoting the name of the first new struct object to be created. This object will possess the fields which are not split out (i.e. not listed in the :split-members argument).
If this argument is omitted, a fresh name will be inferred.

:new-object2 — optional

A string denoting the name of the second new struct object to be created. This object will possess the fields which are split out (i.e. listed in the :split-members argument).
If this argument is omitted, a fresh name will be inferred.

:new-type1 — optional

A string denoting the tag of the first new struct type to be created. This struct type will possess the fields which are not split out (i.e. not listed in the :split-members argument).
This represents the type of :new-object1.
If this argument is omitted, a fresh name will be inferred.

:new-type2 — optional

A string denoting the tag of the second new struct type to be created. This struct type will possess the fields which are split out (i.e. listed in the :split-members argument).
This represents the type of :new-object2.
If this argument is omitted, a fresh name will be inferred.

Constraints on the Input Code

The global struct object cannot occur in certain expressions we deem "illegal". These are expressions which might threaten the soundness of the transformation if they were permitted. Any expression which includes a reference to the global struct object which is not a member access is considered illegal.
A member access of the global struct object cannot occur in certain contexts. In particular, you cannot take the address of the member access expression or the sizeof the member access; such expressions are illegal.

Current Limitations

The following are temporary limitations which will hopefully be removed in the future with improvements to the implementation.

Fields in a struct type declaration must not share a type specification (e.g., int x, y; is currently unsupported, where int x; int y; is supported)
Similarly, struct object declarations must not share a type specification (e.g. struct myStruct foo, bar; is currently unsupported, while struct myStruct foo; struct myStuct bar; is allowed.)
The names of the new struct objects and their types are not yet checked for uniqueness/shadowing.

Subtopics

Splitgso-implementation: Implementation of splitgso.