Verifier fails to detect infinite loops on conditional jumps

[Alan-Jowett]

All these tests should fail, but currently pass:

---
test-case: simple infinite loop, less than
options: ["termination"]

pre: []

code:
  <start>: |
    r0 = 0
    if r0 < 1 goto <start>
    exit

post: []

messages:
  - "1:2: Code is unreachable after 1:2"
# Message that should be generated by the verifier, but isn't:
#  - "Could not prove termination."
---
test-case: simple infinite loop, less than or equal
options: ["termination"]

pre: []

code:
  <start>: |
    r0 = 0
    if r0 <= 1 goto <start>
    exit

post: []

messages:
  - "1:2: Code is unreachable after 1:2"
# Message that should be generated by the verifier, but isn't:
#  - "Could not prove termination."

---
test-case: simple infinite loop, equal
options: ["termination"]

pre: []

code:
  <start>: |
    r0 = 0
    if r0 == 0 goto <start>
    exit

post: []

messages:
  - "1:2: Code is unreachable after 1:2"
# Message that should be generated by the verifier, but isn't:
#  - "Could not prove termination."

---
test-case: simple infinite loop, greater than
options: ["termination"]

pre: []

code:
  <start>: |
    r0 = 1
    if r0 > 0 goto <start>
    exit

post: []

messages:
  - "1:2: Code is unreachable after 1:2"
# Message that should be generated by the verifier, but isn't:
#  - "Could not prove termination."

---
test-case: simple infinite loop, greater than or equal
options: ["termination"]

pre: []

code:
  <start>: |
    r0 = 1
    if r0 >= 0 goto <start>
    exit

post: []

messages:
  - "1:2: Code is unreachable after 1:2"
# Message that should be generated by the verifier, but isn't:
#  - "Could not prove termination."

[Alan-Jowett]

I think the bug is here:
https://github.com/vbpf/ebpf-verifier/blob/9f25cee94f74108c19fa1cc88bc32c01d7ad758a/src/crab_verifier.cpp#L97C1-L100C6

The exit instruction is unreachable, and hence has a loop count of 0.

[Alan-Jowett]

Resolved by #745