Add test cases for metadata region access (#863)

* add metadata test cases
* add false negative

Signed-off-by: Laksh Kotian <[email protected]>

Author: LakshK98

test-data/packet.yaml

@@ -195,3 +195,83 @@ code:
 post: ["r0.type=number",
        "r6.type=ctx", "r6.ctx_offset=0",
        "r7.type=number", "r7.svalue=23", "r7.uvalue=23"]
+---
+test-case: meta_offset lower bound access
+
+pre: ["meta_offset=-8", "packet_size=0",
+      "r1.type=packet", "r1.packet_offset=0", "r1.svalue=[4098, 2147418112]", "r1.uvalue=[4098, 2147418112]"]
+
+code:
+  <start>: |
+    r2 = *(u64 *)(r1 - 8)
+
+post: ["meta_offset=-8", "packet_size=0",
+       "r1.type=packet", "r1.packet_offset=0", "r1.svalue=[4098, 2147418112]", "r1.uvalue=[4098, 2147418112]",
+       "r2.type=number"]
+messages: []
+---
+test-case: meta_offset lower bound incorrect access
+
+pre: ["meta_offset=0", "packet_size=8",
+      "r1.type=packet", "r1.packet_offset=0", "r1.svalue=[4098, 2147418112]", "r1.uvalue=[4098, 2147418112]"]
+
+code:
+  <start>: |
+    r2 = *(u64 *)(r1 - 8)
+
+post: ["meta_offset=0", "packet_size=8",
+       "r1.type=packet", "r1.packet_offset=0", "r1.svalue=[4098, 2147418112]", "r1.uvalue=[4098, 2147418112]",
+       "r2.type=number"]
+messages:
+  - "0: Lower bound must be at least meta_offset (valid_access(r1.offset-8, width=8) for read)"
+---
+test-case: meta_offset upper bound incorrect access
+
+pre: ["meta_offset=-8", "packet_size=0",
+      "r1.type=packet", "r1.packet_offset=-8", "r1.svalue=[4098, 2147418112]", "r1.uvalue=[4098, 2147418112]"]
+
+code:
+  <start>: |
+    r2 = *(u64 *)(r1 + 8)
+
+post: ["meta_offset=-8", "packet_size=0",
+       "r1.type=packet", "r1.packet_offset=-8", "r1.svalue=[4098, 2147418112]", "r1.uvalue=[4098, 2147418112]",
+       "r2.type=number"]
+messages:
+  - "0: Upper bound must be at most packet_size (valid_access(r1.offset+8, width=8) for read)"
+---
+test-case: meta_offset upper bound access
+
+pre: ["meta_offset=-8", "packet_size=0",
+      "r1.type=packet", "r1.packet_offset=-8", "r1.svalue=[4098, 2147418112]", "r1.uvalue=[4098, 2147418112]"]
+
+code:
+  <start>: |
+    r2 = *(u64 *)(r1 + 0)
+
+post: ["meta_offset=-8", "packet_size=0",
+       "r1.type=packet", "r1.packet_offset=-8", "r1.svalue=[4098, 2147418112]", "r1.uvalue=[4098, 2147418112]",
+       "r2.type=number"]
+---
+#  This test case demonstrates a false negative generated by the verifier where data_meta + offset < data is known
+#  but packet access at that offset is not allowed.
+
+test-case: meta access with data bound check
+pre: ["meta_offset=[-4098, 0]", "meta_offset=r2.packet_offset",
+      "r2.packet_offset=[-4098, 0]", "r2.svalue=[4098, 2147418112]", "r2.type=packet",
+      "r1.packet_offset=0", "r1.svalue=[4098, 2147418112]", "r1.type=packet"]
+
+code:
+  <start>: |
+    r1 -= r2
+    r3 = 101
+    assume r3 s<= r1;
+    r0 = *(u8 *)(r2 + 100);
+
+post: ["meta_offset=[-4098, 0]",
+       "r0.svalue=[0, 255]", "r0.type=number", "r0.uvalue=[0, 255]",
+       "r1.svalue=[101, 4098]", "r1.type=number", "r1.uvalue=r1.svalue",
+       "r2.packet_offset=meta_offset", "r2.svalue=[4098, 2147418112]", "r2.type=packet",
+       "r3.svalue=101", "r3.type=number", "r3.uvalue=101"]
+messages:
+  - "3: Upper bound must be at most packet_size (valid_access(r2.offset+100, width=1) for read)"