C++: Sign analysis library

[rdmarsh2]

This is the first part of a port of the Java range analysis library using the IR. It's based off #197, but I wanted to get it out for a round of review now. deeeb25 is the first commit that isn't part of #197.

I'm expecting the main review to come from @jbj, but I'd also like a look from @dave-bartolomeo for the IR changes and from @aschackmull since he wrote the Java library.

[aschackmull]

Have you tried some tests for completeness on some complex snapshots? I.e. testing that every integral-typed expression has sign information. I seem to remember needing to close some holes in various corner cases when doing the java version.

[aschackmull]

The Java guards library includes a set of "implies" predicates to handle
short-circuiting conditionals. C++ handles those in IR generation, so
dominance on the IR produces correct results for controlling blocks.

This is not entirely correct. The java CFG also handles short-circuiting conditionals, so dominance does "the right thing". The reason why these are also included in the implies family of predicates is to support when such conditions occur in non-boolean contexts. E.g.:

boolean b = cond1 && cond2;
if (b) {
  foo();
}

In this case we'd like both cond1 and cond2 to act as guards for foo(), which isn't directly given from dominance.

[jbj]

I think there are some fundamental questions here we should answer about the relationship between Instruction, ValueNumber and a possible Operand type. This doesn't have to hold back this PR, but I think it should hold back further work on porting range analysis. Let's discuss over Hangouts when @dave-bartolomeo is back next week.

[jbj]

You have to change all three copies of Instruction.qll. Check with buildutils-internal/scripts/pr-checks/sync-identical-files.py if it worked.

[jbj]

There are now two cached predicates in this file. Please group them in a cached module like we've done elsewhere to make sure the engine will put them in the same stage both now and in the future. Otherwise we risk evaluating most of the range analysis twice.

[jbj]

The QLDoc for both the unary and binary versions of these predicates needs updating. It mentions e, but there's only i and pos.

[jbj]

use hasGuard here?

I'm having trouble answering that question too. Maybe that's because this port sometimes uses Instruction in place of Java's Expr (like in this predicate) and sometimes uses Instruction i, Instruction pos. We can get away with using Instruction for Expr in cases like addition and such because the IR does not apply common subexpression elimination and therefore guarantees that each such Instruction is consumed only once, but that's not the case for instructions like LoadInstruction or PhiInstruction.

To expose this problem in its full generality, one option would be to replace our use of Instruction with ValueNumber. Then this library can see that x - 2 is positive under if (x - 2 > 0), but we'll have to be consistent in using ValueNumber val, Instruction pos. Or we could create a SsaReadPosition class like in Java to use for pos.

[jbj]

Thanks, @rdmarsh2. What do you say to @aschackmull's comments? Are they best addressed now or in a follow-up PR?

[jbj]

The test is failing due to a semantic merge conflict with #254.

[rdmarsh2]

I'll fix the test failures and run on some real snapshots this afternoon. I'll try and get the implies predicates done tomorrow.

[jbj]

Double backtick

[jbj]

To port this library to Operand, I thought you'd just change pairs of (Instruction instr, Instruction pos) into Operand op, but this commit also changes occurrences like Instruction lowerbound to have type Operand without calling its .getInstruction(). That will increase the size of each predicate like this by effectively joining with all the places where lowerbound is used. Is there a good reason to do that?

[rdmarsh2]

This allows us to be more precise when lowerbound has a lower bound, as in the following (contrived) example:

int f(int x, int y) {
  if (x < 0) {
    return x;
  }
  iif (x < y) {
   return y; // y is strictly positive because of the bound on x above
  }
  return 0;
}

[jbj]

Nice.

[rdmarsh2]

I've added a test demonstrating this for lower bounds

[rdmarsh2]

Oh ,there actually is a cartesian product there - I'll see if I can add it in directly or if I need to do a rewrite of IRGuards.qll to make it work

[jbj]

This code assumes that overflow can't occur, but we often get FP reports for the existing range analysis library because overflow is relied on in practice. See, for example, https://discuss.lgtm.com/t/false-positive-c-comparison-result-is-always-the-same/1428.

I expect that we'll need to model overflow for unsigned integers, but we can continue to ignore it for signed integers because it's undefined there. For a case like inc, this means adding that this = TPos() and result = TZero() in the unsigned case.

[aschackmull]

For the corresponding query in java, FPs for overflow checks are instead excluded in the query. This works because overflow checks are pretty idiomatic and easy to recognise, and thus allows the rangeanalysis to stay (mostly) oblivious to such overflows.

[jbj]

Okay, let's go with the Java approach for now and evaluate whether to change it later, when we have queries and results to look at.

[jbj]

I'm willing to merge this when the tests pass if you can vouch for the performance of the modified IRGuards.qll. I wonder if IRGuardCondition should extend Operand instead of Instruction, but we can discuss that outside this PR.

[rdmarsh2]

From testing on LuaJit, it doesn't look like there's a significant impact on IRGuards performance; both runs spent approximately 17 seconds evaluating the IRGuards stages.

[rdmarsh2]

I wonder if IRGuardCondition should extend Operand instead of Instruction, but we can discuss that outside this PR.

That's an interesting point... It might allow us to infer some additional bounds when a variable is compared to multiple other variables in a short-circuiting conditional. I agree we should leave it for another PR.