Implement a per-allocation-site memory-safety checking

[shaobo-he]

Motivation

Currently, we only have one bookkeeping variable $Alloc for the entire program. We can split it into multiple bookkeep variables such that one variable roughly corresponds to one allocation site (i.e., a call to malloc or an alloca instruction). Having multiple bookkeeping variables reduces the solver's burden to reason about arrays.

Implementation Plan

The key idea to implement this feature is to id allocation sites and find out which allocate sites a pointer is associated with.

However, an implication of having multiple bookkeeping variables is that we have to change the signature of $alloca, malloc, or __SMACK_check_memory_safety procedures since they check/constrain/update different variables.