C++: Allocate more FunctionInput and FunctionOutputs

[MathiasVP]

The modelling language we use for specifying C/C++ models allows us to express stuff like "there's flow from the second indirection of a parameter to the second indirection of the return value" using a model like:

override predicate hasTaintFlow(FunctionInput input, FunctionOutput output) {
  input.isParameterDeref(2) and output.isReturnValueDeref(2)
}

if we add this model to a function foo this should ensure that we get flow in an example such as:

int** foo(int**);

void test(int** buffer) {
  **buffer = source();
  char** buffer2 = foo(buffer);
  sink(**buffer2);
}

However, while the modelling interface allowed us to do this, the modelling implementation was hardcoded to only allow input.isParameterDeref(1) and output.isReturnValueDeref(1) 😱.

So this PR bumps those bounds up to 2. In reality we can probably bump it up arbitrarily large (although we do have to provide some bound to make sure it's all finite), but I didn't want to do that in this PR since I want to get this in quickly to unblock @jketema's work on #14561.

Commit-by-commit review recommended.

[jketema]

One small comment.

Regarding the DCA results: are these actually new results, or are they just duplicating existing results?

[MathiasVP]

Regarding the DCA results: are these actually new results, or are they just duplicating existing results?

On Samate this looks like new results 🎉. I'm still checking the other DBs.

Edit: The other ones are also new results 🎉. I have yet to find out exactly why we didn't find these results before, but I'm very happy that we now do find them 😂

[MathiasVP]

@jketema in 31c2a3b I've reverted the redefinitions of the single-parameter predicates. I've tested that we preserve the test results even if I keep the old definition of of hasRemoteFlowSource in the recv class (and likewise if I keep the old definition of hasRemoteFlowSink in the Send class). However, I think the more explicit models we have now are better, so I think we should keep them as they are in this PR.

[jketema]

Probably want to re-run DCA, other than that LGTM.

[MathiasVP]

Probably want to re-run DCA, other than that LGTM.

Agreed. DCA running now 👍

[MathiasVP]

DCA looks fine. The new real-world results are gone, but we still find all the new Samate results. So I'll merge this and we can always investigate why we lost the real-world results again at a later time.