WIP: Heapster/source hints

[abakst]

Adds a mechanism to specify Heapster block-entry hints in LLVM IR. The hints are automatically extracted by the heapster_typecheck_fun SAW command and added to the perm env.

A basic block should include a call to void (...) @heapster.require like so:

@.ghosts = private unnamed_addr constant [42 x i8] c"frm:llvmframe 64,a:llvmptr 64,b:llvmptr 64", align 1
@.spec = private unnamed_addr constant [90 x i8] c"arg0:eq(top1),arg1:eq(top0),top1:true,top0:ptr((R,0) |-> eq(arg0)),frm:llvmframe [b:8,a:8]", align 1

...

  call void (...) @heapster.require(
    i8* getelementptr inbounds ([42 x i8], [42 x i8]* @.ghosts, i64 0, i64 0),
    i8* getelementptr inbounds ([90 x i8], [90 x i8]* @.spec, i64 0, i64 0),
    i64 %1,
    i64* %0
  )

• The first argument is a ghost context. The names here can be arbitrary
• The second argument is a list of value permissions. The names bound should be arg0 ... argN. Permissions can also be assigned to ghosts defined in the ghost context, or toplevels via the names top0...topM
• The remaining arguments are the llvm instructions to substitute for each argi, i.e. the in the above, use %1 for arg0, %2 for arg1.

[eddywestbrook]

LGTM!