• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
        • Syntax-for-tools
        • Atc
        • Language
        • Representation
        • Transformation-tools
          • Simpadd0
          • Deftrans
          • Splitgso
          • Constant-propagation
          • Split-fn
          • Copy-fn
          • Specialize
            • Param-declon-list-remove-param-by-ident
            • Specialize-fundef
            • Specialize-extdecl
            • Specialize-filepath-transunit-map
            • Specialize-transunit-ensemble
            • Specialize-extdecl-list
            • Param-declon-to-decl
            • Specialize-transunit
            • Ident-from-param-declon
          • Split-all-gso
          • Rename
          • Utilities
        • Insertion-sort
        • Pack
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Bitcoin
      • Riscv
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Bigmems
      • Builtins
      • Execloader
      • Aleo
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Transformation-tools

Specialize

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

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.

For a concrete example, consider the following C code:

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

Specializing parameter y with the constant 1 yields 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.

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.

Subtopics

Param-declon-list-remove-param-by-ident
Remove a parameter from a list of parameter declarations.
Specialize-fundef
Transform a function definition.
Specialize-extdecl
Transform an external declaration.
Specialize-filepath-transunit-map
Transform a filepath.
Specialize-transunit-ensemble
Transform a translation unit ensemble.
Specialize-extdecl-list
Transform a list of external declarations.
Param-declon-to-decl
Convert a parameter declaration to a regular declaration.
Specialize-transunit
Transform a translation unit.
Ident-from-param-declon
Get the identifier from a parameter declaration.