C++: Fix barriers in invalid pointer deref

[MathiasVP]

This PR fixes both the barriers in cpp/invalid-pointer-deref. That is, the first commit fixes the barrier InvalidPointerToDereference.qll, and the fifth commit fixes the barrier in AllocationToInvalidPointer.qll.

Both barriers should now come with (very informal) correctness proofs.

[geoffw0]

QL changes seem reasonable (though I won't pretend to have a deep understanding of all of them). Test results speak for themselves.

On DCA we lose 6 results, which appear to be false positives as well (as best I can tell).

[MathiasVP]

DCA looks good. We lose the same 6 results as we did on the very first DCA run (which both Geoffrey and I confirmed to be FPs) 🎉

[MathiasVP]

@jketema ce9b018 moves the check out of the predicate as we discussed offline. I hope that makes things more clear. It certainly makes the comments easier to write (since we now have more names for things 😂).

[jketema]

I believe I understand the barrier changes to AllocationToInvalidPointer.qll, and they make sense to me.

[jketema]

Did we do a DCA run after we fixed the off-by-one issue?

[MathiasVP]

Did we do a DCA run after we fixed the off-by-one issue?

I haven't done one yet, but I suppose I might as well start one now, yeah 👍

[jketema]

LGTM provided DCA comes back ok.

[MathiasVP]

The DCA results are in: We still lose the 6 FPs as before, but we now gain a couple of new results that I'm investigating. So far (will update as I go along):

Wireshark

One new result related to a complex loop that depends on the input being a multiple of 4 that looks like:

for (i=ICQ5_CL_SESSIONID; i < size; i+=4 ) {
    k = key+table_v5[i&0xff];
    if ( i != 0x16 ) {
        bfr[i] ^= (guchar)(k & 0xff);
        bfr[i+1] ^= (guchar)((k & 0xff00)>>8); // <--- We now raise an alert here
    }
    if ( i != 0x12 ) {
        bfr[i+2] ^= (guchar)((k & 0xff0000)>>16);
        bfr[i+3] ^= (guchar)((k & 0xff000000)>>24);
    }
}

Vim

A very strange loop that changes the number of iterations, and does different things depending on the current value that's incremented 😭:

for (pos.col = 0; pos.col < len; pos.col += width) {
		if (vterm_screen_get_cell(screen, pos, &cell) == 0) {
			width = 1;
			CLEAR_POINTER(p + pos.col);
			if (ga_grow(&ga, 1) == OK)
					ga.ga_len += utf_char2bytes(' ',
								(char_u *)ga.ga_data + ga.ga_len);
		}
		else width = cell.width;

	cell2cellattr(&cell, &p[pos.col]);
	if (width == 2)
			// second cell of double-width character has the
			// same attributes.
			p[pos.col + 1] = p[pos.col]; // <--- We now raise an alert here
	/* ... */
}

Nelson

This alert LGTM, but it may be a FP because allocateArrayOf may allocate nbElements + 1 number of elements (in which case the code is fine). I haven't verified this yet, though. In any case, I'm happy with this result as it does look like something the current query is expected to find (i.e., while there's a barrier that's making k a safe index, the same thing cannot be said about k + 1). So I'm happy with this result.

double* ptrComplex = (double*)ArrayOf::allocateArrayOf(NLS_DCOMPLEX, nbElements, stringVector(), false);
auto* strElements = (ArrayOf*)A.getDataPointer();
indexType q = 0;
for (indexType k = 0; k < nbElements; k = k + 1) {
    ArrayOf element = strElements[k];
    if (element.getDataClass() == NLS_CHAR) {
        std::wstring str = element.getContentAsWideString();
        bool wasConverted = false;
        doublecomplex asComplex = stringToDoubleComplex(str, wasConverted);
        if (wasConverted) {
            ptrComplex[q] = asComplex.real();
            ptrComplex[q + 1] = asComplex.imag();
        } else {
            ptrComplex[q] = std::nan("NaN");
            ptrComplex[q + 1] = 0;
        }
    } else {
        ptrComplex[k] = std::nan("NaN");
        ptrComplex[k + 1] = 0; // <--- We now raise an alert here
    }
}