Fix off-by-one error in stack access check

Signed-off-by: Alan Jowett <[email protected]>

src/assertions.cpp

@@ -168,8 +168,7 @@ class AssertExtractor {
         Imm width{static_cast<uint32_t>(ins.access.width)};
         const int offset = ins.access.offset;
         if (basereg.v == R10_STACK_POINTER) {
-            // We know we are accessing the stack.
-            if (offset < -EBPF_STACK_SIZE || offset + static_cast<int>(width.v) >= 0) {
+            if (offset < -EBPF_STACK_SIZE || offset + static_cast<int>(width.v) > 0) {
                 // This assertion will fail
                 res.emplace_back(
                     ValidAccess{basereg, offset, width, false, ins.is_load ? AccessType::read : AccessType::write});

test-data/uninit.yaml

@@ -495,3 +495,85 @@ post:
 
 messages:
   - "0: Invalid type (r5.type == number)"
+
+# Issue: https://github.com/vbpf/ebpf-verifier/issues/754
+# Should these tests fail?
+---
+test-case: Read uninitialized stack range - aligned
+
+pre:
+  - r10.type=stack
+  - r10.stack_offset=512
+
+code:
+  <start>: |
+    r0 = *(u64 *)(r10 - 16)
+
+post:
+  - "r0.ctx_offset=s[496...503].ctx_offset"
+  - "r0.map_fd=s[496...503].map_fd"
+  - "r0.packet_offset=s[496...503].packet_offset"
+  - "r0.shared_offset=s[496...503].shared_offset"
+  - "r0.shared_region_size=s[496...503].shared_region_size"
+  - "r0.stack_numeric_size=s[496...503].stack_numeric_size"
+  - "r0.stack_offset=s[496...503].stack_offset"
+  - "r0.svalue=s[496...503].svalue"
+  - "r0.type=s[496...503].type"
+  - "r0.uvalue=s[496...503].uvalue"
+  - "r10.stack_offset=512"
+  - "r10.type=stack"
+
+messages: []
+
+---
+test-case: Read uninitialized stack range - aligned
+
+pre:
+  - r10.type=stack
+  - r10.stack_offset=512
+
+code:
+  <start>: |
+    r0 = *(u64 *)(r10 - 8)
+
+post:
+  - "r0.ctx_offset=s[504...511].ctx_offset"
+  - "r0.map_fd=s[504...511].map_fd"
+  - "r0.packet_offset=s[504...511].packet_offset"
+  - "r0.shared_offset=s[504...511].shared_offset"
+  - "r0.shared_region_size=s[504...511].shared_region_size"
+  - "r0.stack_numeric_size=s[504...511].stack_numeric_size"
+  - "r0.stack_offset=s[504...511].stack_offset"
+  - "r0.svalue=s[504...511].svalue"
+  - "r0.type=s[504...511].type"
+  - "r0.uvalue=s[504...511].uvalue"
+  - "r10.stack_offset=512"
+  - "r10.type=stack"
+
+messages: []
+---
+test-case: Read uninitialized stack range - unaligned
+
+pre:
+  - r10.type=stack
+  - r10.stack_offset=512
+
+code:
+  <start>: |
+    r0 = *(u64 *)(r10 - 10)
+
+post:
+  - "r0.ctx_offset=s[502...509].ctx_offset"
+  - "r0.map_fd=s[502...509].map_fd"
+  - "r0.packet_offset=s[502...509].packet_offset"
+  - "r0.shared_offset=s[502...509].shared_offset"
+  - "r0.shared_region_size=s[502...509].shared_region_size"
+  - "r0.stack_numeric_size=s[502...509].stack_numeric_size"
+  - "r0.stack_offset=s[502...509].stack_offset"
+  - "r0.svalue=s[502...509].svalue"
+  - "r0.type=s[502...509].type"
+  - "r0.uvalue=s[502...509].uvalue"
+  - "r10.stack_offset=512"
+  - "r10.type=stack"
+
+messages: []