max<min after jset

[Tao Lyu <tao.lyu@epfl.ch>]

Hi,

The eBPF program shown below leads to an reversed min and max
after insn 6 "if w0 & 0x894b6a55 goto +2",
whic means max < min.

Here is the introduction how it happens.

Before insn 6,
the range of r0 expressed by the min and max field is
min1 = 884670597, max1 = 900354100
And the range expressed by the var_off=(0x34000000; 0x1ff5fbf))
is min2=872415232, max2=905928639.

---min2-----------------------min1-----max1-----max2---

Here we can see that the range expressed by var_off is wider than that of min and max.

When verifying insn6,
it first uses the var_off and immediate "0x894b6a55" to
calculate the new var_off=(0x34b00000; 0x415aa).
The range expressed by the new var_off is:
min3=883949568, max3=884217258

---min2-----min3-----max3-----min1-----max1-----max2---

And then it will calculate the new min and max by:
(1) new-min = MAX(min3, min1) = min1
(2) new-max = MIN(max3, max1) = max3

---min2-----min3-----max3-----min1-----max1-----max2---
         "new-max"          "new-min" 

Now, the new-max becomes less than the new min.

Notably, [min1, max1] can never make "w0 & 0x894b6a55 == 0"
and thus cannot goes the fall-through branch.
In other words, actually the fall-trough branch is a dead path.

BTW, I cannot successfully compile this instruciton "if w0 != 0 goto +2;\"
in the c inline assembly code.
So I can only attach the bytecodes.

Signed-off-by: Tao Lyu <tao.lyu@epfl.ch>
---
 .../selftests/bpf/verifier/jset_reversed_range.c  | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 tools/testing/selftests/bpf/verifier/jset_reversed_range.c

diff --git a/tools/testing/selftests/bpf/verifier/jset_reversed_range.c b/tools/testing/selftests/bpf/verifier/jset_reversed_range.c
new file mode 100644
index 000000000000..734f492a2a96
--- /dev/null
+++ b/tools/testing/selftests/bpf/verifier/jset_reversed_range.c
@@ -0,0 +1,15 @@
+{
+    "BPF_JSET: incorrect scalar range",
+    .insns = {
+    BPF_MOV64_IMM(BPF_REG_5, 100),
+    BPF_ALU64_IMM(BPF_DIV, BPF_REG_5, 3),
+    BPF_ALU32_IMM(BPF_RSH, BPF_REG_5, 7),
+    BPF_ALU64_IMM(BPF_AND, BPF_REG_5, -386969681),
+    BPF_ALU64_IMM(BPF_SUB, BPF_REG_5, -884670597),
+    BPF_MOV32_REG(BPF_REG_0, BPF_REG_5),
+    BPF_JMP32_IMM(BPF_JSET, BPF_REG_0, 0x894b6a55, 1),
+    BPF_MOV64_IMM(BPF_REG_0, 1),
+    BPF_MOV64_IMM(BPF_REG_0, 0),
+    BPF_EXIT_INSN(),
+    },
+},
-- 
2.25.1