Enhance detection of buffer overflows by introducing variable for length of array/blob

A possible direction that we could go in to convince people that our analysis of globals is useful would be to target the absence of buffer overflows (our if we want to go for something more sophisticated, the absence of buffer overflows in string manipulation).

A critical ability there would be to relate the length of a buffer with variables used to access things inside the buffer. Currently, this only works for the non-relational case.

int readUntil(char arr[], int len) {
	for(int i=0;i < len;i++) {
		char s  = arr[i];
	}
}

int main() {
	int len;
	int top;

	if(top) {
		len = 5;
	} else {
		len = 10;
	}

	// char* ptr = malloc(sizeof(char)*len);
	char ptr[len];
	readUntil(ptr, len);
}

With --enable ana.arrayoob, we warn at the access in readUntil because we do not know that the length of arr is len here (and also, for some reason, when we call readUntil in main(?)). Also, we currently do not warn at all for access of buffers created by malloc, which is why I used the VLA here.

TODOs:

• Make out of bounds check apply equally for dynamically allocated memory
• Track symbolic relationships between the length of an array and programs variables (just using the relationship between len and the expression used to access the array would not suffice as that could be reassigned later)
  • Ghost variable len$array$ that is set to len on malloc and then automatically tracks the length
• Figure out how (if) this would work for globals (which would be the case we actually care about)

Start with the ana.arrayoob analysis and reproduce the VLA example, checking both the readUntil access and the call in main. Trace how array lengths are represented for VLA and malloc-created buffers, then define and test the symbolic relationship and global-buffer behavior described in the TODOs.