Only set type to pointer if the width is correct

src/asm_parse.cpp

@@ -52,7 +52,7 @@ using crab::linear_expression_t;
 #define ARRAY_RANGE R"_(\s*\[([-+]?\d+)\.\.\.\s*([-+]?\d+)\]?\s*)_"
 
 #define DOT "[.]"
-#define TYPE R"_(\s*(shared|number|packet|stack|ctx|map_fd|map_fd_program)\s*)_"
+#define TYPE R"_(\s*(shared|number|packet|stack|ctx|map_fd|map_fd_programs)\s*)_"
 
 static const std::map<std::string, Bin::Op> str_to_binop = {
     {"", Bin::Op::MOV},   {"+", Bin::Op::ADD},  {"-", Bin::Op::SUB},    {"*", Bin::Op::MUL},

src/crab/ebpf_domain.cpp

@@ -64,6 +64,13 @@ static linear_constraint_t neq(variable_t a, variable_t b) {
 }
 
 constexpr int MAX_PACKET_SIZE = 0xffff;
+
+// Pointers in the BPF VM are defined to be 64 bits.  Some contexts, like
+// data, data_end, and meta in Linux's struct xdp_md are only 32 bit offsets
+// from a base address not exposed to the program, but when a program is loaded,
+// the offsets get replaced with 64-bit address pointers.  However, we currently
+// need to do pointer arithmetic on 64-bit numbers so for now we cap the interval
+// to 32 bits.
 constexpr int64_t PTR_MAX = std::numeric_limits<int32_t>::max() - MAX_PACKET_SIZE;
 
 /** Linear constraint for a pointer comparison.
@@ -1906,22 +1913,32 @@ void ebpf_domain_t::do_load_ctx(NumAbsDomain& inv, const Reg& target_reg, const
 
     number_t addr = *maybe_addr;
 
+    // We use offsets for packet data, data_end, and meta during verification,
+    // but at runtime they will be 64-bit pointers.  We can use the offset values
+    // for verification like we use map_fd's as a proxy for maps which
+    // at runtime are actually 64-bit memory pointers.
+    int offset_width = desc->end - desc->data;
     if (addr == desc->data) {
-        inv.assign(target.packet_offset, 0);
+        if (width == offset_width)
+            inv.assign(target.packet_offset, 0);
     } else if (addr == desc->end) {
-        inv.assign(target.packet_offset, variable_t::packet_size());
+        if (width == offset_width)
+            inv.assign(target.packet_offset, variable_t::packet_size());
     } else if (addr == desc->meta) {
-        inv.assign(target.packet_offset, variable_t::meta_offset());
+        if (width == offset_width)
+            inv.assign(target.packet_offset, variable_t::meta_offset());
     } else {
         if (may_touch_ptr)
             type_inv.havoc_type(inv, target_reg);
         else
             type_inv.assign_type(inv, target_reg, T_NUM);
         return;
     }
-    type_inv.assign_type(inv, target_reg, T_PACKET);
-    inv += 4098 <= target.svalue;
-    inv += target.svalue <= PTR_MAX;
+    if (width == offset_width) {
+        type_inv.assign_type(inv, target_reg, T_PACKET);
+        inv += 4098 <= target.svalue;
+        inv += target.svalue <= PTR_MAX;
+    }
 }
 
 void ebpf_domain_t::do_load_packet_or_shared(NumAbsDomain& inv, const Reg& target_reg, const linear_expression_t& addr,
@@ -2733,30 +2750,52 @@ void ebpf_domain_t::operator()(const Bin& bin) {
             assign(dst.uvalue, src.uvalue);
             havoc_offsets(bin.dst);
             m_inv = type_inv.join_over_types(m_inv, src_reg, [&](NumAbsDomain& inv, type_encoding_t type) {
-                inv.assign(dst.type, type);
-
                 switch (type) {
-                case T_CTX: inv.assign(dst.ctx_offset, src.ctx_offset); break;
+                case T_CTX:
+                    if (bin.is64) {
+                        inv.assign(dst.type, type);
+                        inv.assign(dst.ctx_offset, src.ctx_offset);
+                    }
+                    break;
                 case T_MAP:
-                case T_MAP_PROGRAMS: inv.assign(dst.map_fd, src.map_fd); break;
-                case T_PACKET: inv.assign(dst.packet_offset, src.packet_offset); break;
+                case T_MAP_PROGRAMS:
+                    if (bin.is64) {
+                        inv.assign(dst.type, type);
+                        inv.assign(dst.map_fd, src.map_fd);
+                    }
+                    break;
+                case T_PACKET:
+                    if (bin.is64) {
+                        inv.assign(dst.type, type);
+                        inv.assign(dst.packet_offset, src.packet_offset);
+                    }
+                    break;
                 case T_SHARED:
-                    inv.assign(dst.shared_region_size, src.shared_region_size);
-                    inv.assign(dst.shared_offset, src.shared_offset);
+                    if (bin.is64) {
+                        inv.assign(dst.type, type);
+                        inv.assign(dst.shared_region_size, src.shared_region_size);
+                        inv.assign(dst.shared_offset, src.shared_offset);
+                    }
                     break;
                 case T_STACK:
-                    inv.assign(dst.stack_offset, src.stack_offset);
-                    inv.assign(dst.stack_numeric_size, src.stack_numeric_size);
+                    if (bin.is64) {
+                        inv.assign(dst.type, type);
+                        inv.assign(dst.stack_offset, src.stack_offset);
+                        inv.assign(dst.stack_numeric_size, src.stack_numeric_size);
+                    }
                     break;
-                default: break;
+                default: inv.assign(dst.type, type); break;
                 }
             });
-            if ((bin.dst.v != std::get<Reg>(bin.v).v) || (type_inv.get_type(m_inv, dst.type) == T_UNINIT)) {
-                // Only forget the destination type if we're copying from a different register,
-                // or from the same uninitialized register.
-                havoc(dst.type);
+            if (bin.is64) {
+                // Add dst.type=src.type invariant.
+                if ((bin.dst.v != std::get<Reg>(bin.v).v) || (type_inv.get_type(m_inv, dst.type) == T_UNINIT)) {
+                    // Only forget the destination type if we're copying from a different register,
+                    // or from the same uninitialized register.
+                    havoc(dst.type);
+                }
+                type_inv.assign_type(m_inv, bin.dst, std::get<Reg>(bin.v));
             }
-            type_inv.assign_type(m_inv, bin.dst, std::get<Reg>(bin.v));
             break;
         }
     }

src/crab/split_dbm.cpp

@@ -1052,7 +1052,7 @@ static std::string to_string(variable_t vd, variable_t vs, const SplitDBM::Param
 }
 
 static const std::vector<std::string> type_string = {
-    "shared", "stack", "packet", "ctx", "number", "map_fd", "map_fd_program", "uninitialized"
+    "shared", "stack", "packet", "ctx", "number", "map_fd", "map_fd_programs", "uninitialized"
 };
 
 string_invariant SplitDBM::to_set() const {

test-data/assign.yaml

@@ -172,6 +172,21 @@ post:
   - r1.uvalue=r2.uvalue
   - r1.stack_numeric_size=r2.stack_numeric_size
 ---
+test-case: 32-bit assign register stack value
+
+pre: ["r10.type=stack", "r10.stack_offset=512"]
+
+code:
+  <start>: |
+    w2 = r10
+
+post:
+  - r2.svalue=[0, 4294967295]
+  - r2.svalue=r2.uvalue
+  - r2.uvalue=[0, 4294967295]
+  - r10.type=stack
+  - r10.stack_offset=512
+---
 test-case: assign register shared value
 
 pre: ["r1.type=shared", "r1.shared_offset=0", "r1.shared_region_size=16"]
@@ -190,6 +205,22 @@ post:
   - r1.svalue=r2.svalue
   - r1.uvalue=r2.uvalue
 ---
+test-case: 32-bit assign register shared value
+
+pre: ["r1.type=shared", "r1.shared_offset=0", "r1.shared_region_size=16"]
+
+code:
+  <start>: |
+    w2 = r1
+
+post:
+  - r1.type=shared
+  - r1.shared_offset=0
+  - r1.shared_region_size=16
+  - r2.svalue=[0, 4294967295]
+  - r2.uvalue=[0, 4294967295]
+  - r2.svalue=r2.uvalue
+---
 test-case: assign register combination value
 
 pre: ["r1.type=[-1,0]", "r1.shared_offset=0", "r1.shared_region_size=16", "r1.stack_offset=500", "r1.stack_numeric_size=16"]
@@ -229,3 +260,165 @@ post:
   - r1.uvalue=[1, 2147418112]
   - r2.type=packet
   - r2.svalue=[4098, 2147418112]
+---
+test-case: 16-bit indirect assignment from context
+
+pre: ["r1.ctx_offset=0", "r1.type=ctx", "r1.svalue=[1, 2147418112]", "r1.uvalue=[1, 2147418112]"]
+
+code:
+  <start>: |
+    r2 = *(u16 *)(r1 + 4)
+
+post:
+  - r1.ctx_offset=0
+  - r1.type=ctx
+  - r1.svalue=[1, 2147418112]
+  - r1.uvalue=[1, 2147418112]
+---
+test-case: 64-bit indirect assignment from context
+
+pre: ["r1.ctx_offset=0", "r1.type=ctx", "r1.svalue=[1, 2147418112]", "r1.uvalue=[1, 2147418112]"]
+
+code:
+  <start>: |
+    r2 = *(u64 *)(r1 + 4)
+
+post:
+  - r1.ctx_offset=0
+  - r1.type=ctx
+  - r1.svalue=[1, 2147418112]
+  - r1.uvalue=[1, 2147418112]
+---
+test-case: assign register packet value
+
+pre: ["packet_size=r2.packet_offset", "r2.type=packet", "r2.svalue=[4098, 2147418112]"]
+
+code:
+  <start>: |
+    r1 = r2
+
+post:
+  - packet_size=r1.packet_offset
+  - r1.type=packet
+  - r1.svalue=[4098, 2147418112]
+  - packet_size=r2.packet_offset
+  - r2.type=packet
+  - r2.svalue=[4098, 2147418112]
+  - r1.packet_offset=r2.packet_offset
+  - r1.svalue=r2.svalue
+  - r1.uvalue=r2.uvalue
+---
+test-case: 32-bit assign register packet value
+
+pre: ["packet_size=r2.packet_offset", "r2.type=packet", "r2.svalue=[4098, 2147418112]"]
+
+code:
+  <start>: |
+    w1 = r2
+
+post:
+  - r1.svalue=[0, 4294967295]
+  - r1.uvalue=[0, 4294967295]
+  - r1.svalue=r1.uvalue
+  - packet_size=r2.packet_offset
+  - r2.type=packet
+  - r2.svalue=[4098, 2147418112]
+---
+test-case: assign register context value
+
+pre: ["r1.ctx_offset=0", "r1.type=ctx", "r1.svalue=[1, 2147418112]", "r1.uvalue=[1, 2147418112]"]
+
+code:
+  <start>: |
+    r2 = r1
+
+post:
+  - r1.ctx_offset=0
+  - r1.type=ctx
+  - r1.svalue=[1, 2147418112]
+  - r1.uvalue=[1, 2147418112]
+  - r2.ctx_offset=0
+  - r2.type=ctx
+  - r2.svalue=[1, 2147418112]
+  - r2.uvalue=[1, 2147418112]
+  - r1.svalue=r2.svalue
+  - r1.uvalue=r2.uvalue
+---
+test-case: 32-bit assign register context value
+
+pre: ["r1.ctx_offset=0", "r1.type=ctx", "r1.svalue=[1, 2147418112]", "r1.uvalue=[1, 2147418112]"]
+
+code:
+  <start>: |
+    w2 = r1
+
+post:
+  - r1.ctx_offset=0
+  - r1.type=ctx
+  - r1.svalue=[1, 2147418112]
+  - r1.uvalue=[1, 2147418112]
+  - r2.svalue=[1, 2147418112]
+  - r2.uvalue=[1, 2147418112]
+  - r2.svalue=r2.uvalue
+---
+test-case: assign register map value
+
+pre: ["r1.type=map_fd", "r1.map_fd=1"]
+
+code:
+  <start>: |
+    r2 = r1
+
+post:
+  - r1.map_fd=1
+  - r1.type=map_fd
+  - r2.map_fd=1
+  - r2.type=map_fd
+  - r1.svalue=r2.svalue
+  - r1.uvalue=r2.uvalue
+---
+test-case: 32-bit assign register map value
+
+pre: ["r1.type=map_fd", "r1.map_fd=1"]
+
+code:
+  <start>: |
+    w2 = r1
+
+post:
+  - r1.map_fd=1
+  - r1.type=map_fd
+  - r2.svalue=[0, 4294967295]
+  - r2.uvalue=[0, 4294967295]
+  - r2.svalue=r2.uvalue
+---
+test-case: assign register map programs value
+
+pre: ["r1.type=map_fd_programs", "r1.map_fd=1"]
+
+code:
+  <start>: |
+    r2 = r1
+
+post:
+  - r1.map_fd=1
+  - r1.type=map_fd_programs
+  - r2.map_fd=1
+  - r2.type=map_fd_programs
+  - r1.svalue=r2.svalue
+  - r1.uvalue=r2.uvalue
+---
+test-case: 32-bit assign register map programs value
+
+pre: ["r1.type=map_fd_programs", "r1.map_fd=1"]
+
+code:
+  <start>: |
+    w2 = r1
+
+post:
+  - r1.map_fd=1
+  - r1.type=map_fd_programs
+  - r2.svalue=[0, 4294967295]
+  - r2.uvalue=[0, 4294967295]
+  - r2.svalue=r2.uvalue