Adding bounds inference of the form count(i+1)

[Machiry]

This will add a new heuristic, where the bounds of an array will be inferred as index + 1.

For instance, for the following code:

int getX(int *x) { return x[0]; }
int getY(int *x, int i) { return x[i]; }

The bounds will be inferred as follows:

int getX(_Array_ptr<int> x : count(0 + 1)) { return x[0]; }
int getY(_Array_ptr<int> x : count(i + 1), int i) { return x[i]; }

More details: #599

This improves the bounds inference of other benchmarks as well.

For yacr2 of ptrdist:

ulong ExistPathAboveVCG(_Array_ptr<nodeVCGType> VCG : count(below + 1), ulong above, ulong below)
{
    DFSClearVCG(VCG);
    DFSAboveVCG(VCG, above);
    return(VCG[below].netsAboveReached);
}

That further added bounds to other functions:

ulong VCV(_Array_ptr<nodeVCGType> VCG : count(check + 1), ulong check, ulong track, _Array_ptr<ulong> assign)
{
    ulong	net;
    ulong	vcv;
    vcv = 0;
    for (net = 1; net <= channelNets; net++) {
	if (assign[net]) {
	    if (assign[net] < track) {
		/*
		 * Above VCV?
		 */
		if (ExistPathAboveVCG(VCG, net, check)) {
		    vcv++;
		}
	    }
	    else if (assign[net] > track) {
		/*
		 * Below VCV?
		 */
		if (ExistPathAboveVCG(VCG, check, net)) {
		    vcv++;
		}
	    }
	    else {
		/*
		 * Above or Below VCV?
		 */
		if (ExistPathAboveVCG(VCG, net, check) || ExistPathAboveVCG(VCG, check, net)) {
		    vcv++;
		}
	    }
	}
    }
    return(vcv);
}

[mattmccutchen-cci]

I would still like to have a realistic example program on record before adding this much code to 3C, but others can overrule me.

[john-h-kastner]

What's changed here that requires and extra outer loop?

[Machiry]

I changed the organization of the code a little.
OuterLoop (Loop until nothing changes):

• Loop until nothing changes: Propagate Bounds.
• Loop untill nothing changes: Get bounds from likely bounds (e.g., i < n, arr[i], etc).

[john-h-kastner]

Why doesn't realloc generate a bound on z?

[Machiry]

As of now, we do not insert bounds because of realloc (we only handle malloc). Lets make another issue for this.

[john-h-kastner]

The return bound here is incorrect, but maybe this is acceptable since we know bounds inference gets bounds wrong some times.

[Machiry]

Yup. Let's make another issue for this. There are some issues with generating bounds for &(arr[1]) kinda expressions.

[john-h-kastner]

Could q get the same bound as the return?

[Machiry]

The return bounds do not flow to inside variables.

[john-h-kastner]

OK. looks good.

[mattmccutchen-cci]

Just recording my skepticism that this change should be made at all (per the pending discussion in #599) in a more obvious way, though of course I may be overruled, in which case we can dismiss my review here.

[Machiry]

@john-h-kastner I tested on yacr2 of ptrdist. We found many new bounds.
Example:
in vcg.c

ulong ExistPathAboveVCG(_Array_ptr<nodeVCGType> VCG : count(below + 1), ulong above, ulong below)
{
    DFSClearVCG(VCG);
    DFSAboveVCG(VCG, above);
    return(VCG[below].netsAboveReached);
}

ulong VCV(_Array_ptr<nodeVCGType> VCG : count(check + 1), ulong check, ulong track, _Array_ptr<ulong> assign)
{
...
if (ExistPathAboveVCG(VCG, net, check)) {

and there are other examples too.
I think this change is worth it.

(Recording justification)

[mattmccutchen-cci]

With regrets for belaboring the point, this is the same example that you already posted on #599 and that I argued there wasn't convincing to me.

[Machiry]

Merging this for now. Zane will do a clean of the code and make it more streamlined.