This pull request introduces changes in the src/assertions.cpp, src/crab/ebpf_domain.cpp, test-data/call.yaml, and test-data/callx.yaml files. The changes mainly focus on modifying the handling of memory types in the codebase and updating the test cases accordingly.
Changes to memory handling:
src/assertions.cpp: Modified the AssertExtractor class to change the type constraint of arg.reg from TypeGroup::stack_or_packet to TypeGroup::mem for PTR_TO_MAP_KEY and PTR_TO_MAP_VALUE cases.
src/crab/ebpf_domain.cpp: Updated the ebpf_domain_t::operator() method to handle T_SHARED access register type. It now checks the access to shared memory and requires that the shared value is greater than 0.
Updates to test cases:
test-data/call.yaml: Added new test cases for the bpf_map_update_elem function with different conditions for shared values. Also, updated the error messages in existing test cases to include shared as a valid type. [1][2]
test-data/callx.yaml: Updated the error message in a test case to include shared as a valid type.
coverage: 90.358% (-0.02%) from 90.375%
when pulling 959fc177edd0b5c619b3c0cb80d508b2f9ea23a4 on Alan-Jowett:issue620
into edf88e2bed6d281657a032dc38fa6e4983ab0478 on vbpf:main.
Resolves: #620
This pull request introduces changes in the
src/assertions.cpp
,src/crab/ebpf_domain.cpp
,test-data/call.yaml
, andtest-data/callx.yaml
files. The changes mainly focus on modifying the handling of memory types in the codebase and updating the test cases accordingly.Changes to memory handling:
src/assertions.cpp
: Modified theAssertExtractor
class to change the type constraint ofarg.reg
fromTypeGroup::stack_or_packet
toTypeGroup::mem
forPTR_TO_MAP_KEY
andPTR_TO_MAP_VALUE
cases.src/crab/ebpf_domain.cpp
: Updated theebpf_domain_t::operator()
method to handleT_SHARED
access register type. It now checks the access to shared memory and requires that the shared value is greater than 0.Updates to test cases:
test-data/call.yaml
: Added new test cases for thebpf_map_update_elem
function with different conditions for shared values. Also, updated the error messages in existing test cases to includeshared
as a valid type. [1] [2]test-data/callx.yaml
: Updated the error message in a test case to includeshared
as a valid type.