Updating the output type of alloca in heapster

[jpaykin]

The alloca command was previously given the following heapster return type:

                  ret:ptr((W,0) |-> true, (W,M) |-> true, (W,2*M) |-> true,
                          ..., (w, (i-1)*M, 8*(sz-(i-1)*M)) |-> true)

which indicated a block of size sz broken up into chunks of size M. However, this produced undesired behavior when allocating data structures whose fields were not all the same size, such as structs. This update gives alloca an unstructured return type described as a memblock:

                 ret:memblock(W,0,sz,emptysh)

This branch is work in progress as I ensure all heapster examples pass and that the change can correctly interpret fields.

[jpaykin]

This branch passes all the tests in the saw/script/heapster/saw/examples directory except for arrays.saw:

"heapster_typecheck_fun" (/home/jennifer/work/PICARD/saw-script/heapster-saw/examples/arrays.saw:44:1-44:23):
Inferred type
  sort 1
Not a subtype of expected type
  sort 0
For term
  sort 0

The code referenced is the following call to heapster_typecheck_fun:

heapster_typecheck_fun env "sum_2d"
  "(l1:bv 64,l2:bv 64). arg0:array(W,0,<l1,*8,fieldsh(array(W,0,<l2,*8,fieldsh(int64<>)))), \
                      \ arg1:eq(llvmword(l1)), arg2:eq(llvmword(l2)) -o \
                      \ arg0:array(W,0,<l1,*8,fieldsh(array(W,0,<l2,*8,fieldsh(int64<>)))), \
                      \ arg1:true, arg2:true, ret:int64<>";

[eddywestbrook]

Awesome, this looks great! Though we do have to wait for #1496 to get merged before this one.