Add the heapster_define_opaque_llvmshape command

[eddywestbrook]

This command will define an opaque named LLVM shape. This is like a "shape axiom", where Heapster does not know or care about the contents of memory of this shape but instead treats that memory as an opaque object, defined only by its length. The user also specifies a SAW core type-level function from (the translations of) the arguments of this new named shape to a SAW core type that is used as the translation of the shape.

The syntax for this command will be:

heapster_define_opaque_llvmshape henv nm w args len tp_fun

where:

• henv is a Heapster environment
• nm is the name of the new shape being defined
• w is the pointer width used for the shape
• args is a context of argument types for the shape
• len is the length in bytes of the shape as an expression of type bv w over the variables in args
• tp_fun is a SAW core expression for a type over the translations of the variables in args