		Search-engine friendly clone of the ACL2 documentation.

Transformation-tools

Specialize

A C-to-C transformation to specialize a function.

Introduction

This transformation specializes a function by moving one of its parameters to a declaration at the top of the function body, initialized to some constant.

Note that this modifies the target function; it does not make a copy of the function. If you want to specialize a copy of a function, first employ the copy-fn transformation.

It is often desirable to propagate constants and eliminate dead code after specializing. The specialize transformation does not implement such behavior. Eventually, we will want to implement separate constant propagation and dead code elimination transformations.

General Form

(specialize const-old
            const-new
            :target ... ; required
            :param  ... ; required
            :const  ... ; required
  )

Inputs

const-old

Specifies the code to be transformed.
This must be a symbol that names an existing ACL2 constant that contains a translation unit ensemble, i.e. a value of type transunit-ensemble. 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.

:target

A string denoting the identifier of the function which should be specialize.
Note: There is currently no way to specify the translation unit to allow for disambiguation of functions of the same name with internal linkage. Eventually, a :target-filepath keyword argument will be introduced to accommodate this case. Until then, the transformation will apply to all functions of the specified name.

:param

A string denoting the identifier of the function parameter which is to be specialized.

:const

An exprp which denotes the value that the :param will be specialized to.
Note: This value should be a constant, but this condition is not currently checked.

Example

For a concrete example, consider the following C code:

int foo(int y, int z) {
  int x = 5;
  return x + y - z;
}

Assuming this function exists in a translation unit ensemble stored in the constant foo, we can specialize the argument y with the constant 1 with the following use of specialize.

(specialize *old*
            *new*
            :target "foo"
            :param  "y"
            :const  (c$::expr-const
                      (c$::const-int
                        (c$::make-iconst
                          :core (c$::dec/oct/hex-const-dec 1)))))

This will produce the following:

int foo(int z) {
  int y = 1;
  int x = 5;
  return x + y - z;
}

Clearly a call of foo(z), where z is arbitrary and foo is the specialized function, is equal to foo(1, z) for the old function foo.

Subtopics

Specialize-implementation: Implementation of specialize.