[DRAFT] [pulse] keep caller arithmetic facts when applying callee comparisons

[VladimirMakaev]

Applying a callee's path condition could lose arithmetic facts, so comparisons made in callees led
Pulse down infeasible paths, e.g. spurious leaks of RAII file descriptors checked with fd < 0.

int less_than(int a, int b) { return a < b; }

void f() {
  int x = random();
  if (x <= 0) {
    return;
  }
  if (less_than(x, 0)) {
    return;
  }
  if (x == 0) {
    int* p = NULL;
    *p = 42; // false positive: null dereference reported here
  }
}

The fix has three parts:

• callee intervals go on the caller's representatives, and caller intervals follow the new
  equalities (needed by not_zero_or_one_*);
• a restricted (non-negative) variable equal to a necessarily negative term is Unsat
  (assume_in_callee_*);
• intervals of restricted variables are intersected with [0,+∞) (negative_*).

Either of the first two fixes the example and owned_fd, where the restricted variables are
tableau slacks (x <= 0 gives x = 1 + w, w >= 0). The last two only use the non-negativity the
tableau already assumes, adding no trust in models.

Test plan

New tests in c/pulse/arithmetic.c (one FP_ for a remaining gap), cpp/pulse/owned_fd.cpp and
PulseFormulaTest.ml; reverting any part fails some of them. The C, C++, Java, Kotlin and SIL
codetoanalyze tests and the Pulse OCaml unit tests pass.