[mehrdadn]

Oh! I thought bounded loops meant every loop has to have a bound (hence while (true) wouldn't work). If it can handle more complicated situations then that answers my question. The second example is identical to a do-while loop though, so it's not clear to me if it can actually handle more complicated situations that don't directly map to for/while/do-while loops.

For example, can it handle something like the following, where there's no bound, but the loop necessarily always terminates? (I assumed this loop would be called "unbounded", but maybe I'm confused by the terminology?)

  int test(unsigned i, unsigned j) {
    while (true) {
      i ^= j; j ^= i; i ^= j;
      if (i <= j) { return 0; }
      i ^= j; j ^= i; i ^= j;
      if (j <= i) { return 1; }
      i ^= j; j ^= i; i ^= j;
    }
    return 2;
  }

[kleendr13]

Very interesting question, I just gave that a run with i and j being unknown and seems it's getting rejected by the verifier as it still probes the else path. Note that LLVM will convert the xor patterns to moves:

  ; __u64 i = PT_REGS_FP(ctx), j = PT_REGS_RC(ctx);
  0: (79) r2 = *(u64 *)(r1 +32)
  ; __u64 i = PT_REGS_FP(ctx), j = PT_REGS_RC(ctx);
  1: (79) r1 = *(u64 *)(r1 +80)
  ; 
  2: (bf) r3 = r1
  3: (bf) r1 = r2
  4: (bf) r2 = r3
  ; if (i <= j) { return 0; }
  5: (2d) if r3 > r1 goto pc-4
  from 5 to 2: R1=inv(id=2) R2=inv(id=1) R3=inv(id=1) R10=fp0
  ; 
  2: (bf) r3 = r1
  3: (bf) r1 = r2
  4: (bf) r2 = r3
  ; if (i <= j) { return 0; }
  5: (2d) if r3 > r1 goto pc-4
  from 5 to 2: R1_w=inv(id=1) R2_w=inv(id=2) R3_w=inv(id=2) R10=fp0
  ;
  2: (bf) r3 = r1
  3: (bf) r1 = r2
  4: (bf) r2 = r3
  ; if (i <= j) { return 0; }
  5: (2d) if r3 > r1 goto pc-4
  ;
  infinite loop detected at insn 2

[mehrdadn]

Ah I see, thanks for running it! Yeah so it's not this particular loop that's interesting (there's probably always going to be some simple-looking loop a solver can't prove—and I'm sure we could come up with simpler examples), but rather, the interesting question is whether it can figure out anything that doesn't map directly to bounded for/while/do-while loops. It's interesting because:

1. If the answer is no, then what is the precise reason? Is there a legitimate reason for it? After all, a bounded loop that loops for too long is just as bad as one that never terminates, so clearly they need a way to upper-bound the instruction count for any loop—at which point, why is the bound even relevant? The only reason I can think of is that they do simplistic analysis (e.g. multiplying the bounds on nested loops to naively approximate an overall bound), but your examples suggest they have more sophisticated (SMT/BMC?) solvers, and it's not obvious to me why a modern solver would fail on all unbounded loops.

2. If the answer is yes, then it would seem they actually do allow unbounded loops after all?

The other possibility is they're using the word "bounded" differently (e.g. maybe as a synonym for "terminating"), in which case it would be true that they would need bounded loops by definition.

[tptacek]

The verifier is extremely fussy. Different forms of the exact same loop (as far as the programmer is concerned) will get different results, and my experience is that I spend time rewriting the same loop in different ways just to get programs to pass. A bona-fide non-unrolled loop in a BPF program right now is a special thing that takes extra time to implement, and you're probably not going to use them casually.

The answer to whether BPF effectively allows unbounded loops is "no". The verifier essentially emulates the instructions in your loop, iteration by iteration, and gives itself a fixed budget to do so. If it can't prove the loop invariably exits in that budget, it rejects the program. Allowing an unbounded loop would be an important security vulnerability, and is kind of the whole original point of the verifier.

Probably, this is just a terminology issue; what the verifier in fact cares about is indeed whether the program terminates.

[mehrdadn]

Thanks! Yeah that makes sense; it sounds like it's just the terminology then.