On 11/21/23 12:32 PM, Tao Lyu wrote:
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.
The format "if w0 != 0 goto +2;\" should be supported by recent clang compiler.
Which clang version you are using? Maybe try clang 15/16? Could you also
post the C inline assembly code here so we can investigate?
So I can only attach the bytecodes.
Signed-off-by: Tao Lyu <tao.lyu@xxxxxxx>
---
.../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(),
+ },
+},
