Fix checking of bad call parameter

Prior to this change, if the caller didn't pass enough registers, the verifier would throw an exception instead of gracefully failing verification. Signed-off-by: Dave Thaler <[email protected]>
vbpf · Jan 2, 2024 · 5a082ec · 5a082ec
1 parent 68951ab
commit 5a082ec
Showing 1 changed file with 6 additions and 1 deletion.
diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp
@@ -2144,7 +2144,12 @@ void ebpf_domain_t::operator()(const Call& call) {
 
         case ArgPair::Kind::PTR_TO_WRITABLE_MEM: {
             bool store_numbers = true;
-            variable_t addr = get_type_offset_variable(param.mem).value();
+            auto variable = get_type_offset_variable(param.mem);
+            if (!variable.has_value()) {
+                require(m_inv, linear_constraint_t::FALSE(), "Argument must be a pointer to writable memory");
+                return;
+            }
+            variable_t addr = variable.value();
             variable_t width = reg_pack(param.size).svalue;
 
             m_inv = type_inv.join_over_types(m_inv, param.mem, [&](NumAbsDomain& inv, type_encoding_t type) {