Split ebpf_domain_t into domain, transformer, checker #787
Conversation
Signed-off-by: Elazar Gershuni <[email protected]>
Signed-off-by: Elazar Gershuni <[email protected]>
WalkthroughThis pull request includes several updates, primarily focusing on restructuring the Changes
Possibly related PRs
Suggested reviewers
Thank you for using CodeRabbit. We offer it for free to the OSS community and would appreciate your support in helping us grow. If you find it useful, would you consider giving us a shout-out on your favorite social media? 🪧 TipsChatThere are 3 ways to chat with CodeRabbit:
Note: Be mindful of the bot's finite context window. It's strongly recommended to break down tasks such as reading entire modules into smaller chunks. For a focused discussion, use review comments to chat about specific files and their changes, instead of using the PR comments. CodeRabbit Commands (Invoked using PR comments)
Other keywords and placeholders
CodeRabbit Configuration File (
|
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 12
🧹 Outside diff range comments (4)
test-data/jump.yaml (1)
Line range hint
763-1359: Architecture suggestion: Consider test case consolidation.The test cases follow a highly repetitive pattern with similar structures. Consider:
- Using a test case generator to reduce duplication
- Creating shared fixtures for common pre-conditions and post-conditions
- Implementing parameterized tests for different operators
src/crab/ebpf_domain.cpp (3)
Line range hint
952-964: Fix use of undeclared variable 'dom' inforget_packet_pointersThe variable
domused ininitialize_packet(dom);is not declared within the scope of theforget_packet_pointersfunction. This will cause a compilation error due to the use of an undeclared identifier.Apply this diff to correct the issue:
void ebpf_transformer::forget_packet_pointers() { using namespace crab::dsl_syntax; for (const variable_t type_variable : variable_t::get_type_variables()) { if (type_inv.has_type(m_inv, type_variable, T_PACKET)) { havoc(variable_t::kind_var(data_kind_t::types, type_variable)); havoc(variable_t::kind_var(data_kind_t::packet_offsets, type_variable)); havoc(variable_t::kind_var(data_kind_t::svalues, type_variable)); havoc(variable_t::kind_var(data_kind_t::uvalues, type_variable)); } } - initialize_packet(dom); + initialize_packet(m_inv); }
Line range hint
2519-2527: Handle unsupported operation inoperator()forBin::Op::MOVSX8,MOVSX16, andMOVSX32In the
operator()method forBinoperations, the case forBin::Op::MOVSX8,MOVSX16, andMOVSX32results inCRAB_ERROR("Unsupported operation");, which could terminate the program unexpectedly.Modify the code to handle these cases appropriately or provide a clear error message without terminating the program:
case Bin::Op::MOVSX8: case Bin::Op::MOVSX16: case Bin::Op::MOVSX32: - CRAB_ERROR("Unsupported operation"); + // Handle sign-extension operations + sign_extend(bin.dst, imm, finite_width, bin.op); + break;
Line range hint
2895-2908: Correct invocation ofinitialize_packetinsetup_entryIn the
setup_entrymethod,initialize_packetis called without an instance, which may lead to incorrect behavior ifinitialize_packetis not a static method.Apply this diff to ensure correct invocation:
initialize_packet(inv); return inv; } -void ebpf_transformer::initialize_packet(ebpf_domain_t& inv) { +void ebpf_domain_t::initialize_packet(ebpf_domain_t& inv) { using namespace crab::dsl_syntax; inv -= variable_t::packet_size(); inv -= variable_t::meta_offset();
📜 Review details
Configuration used: CodeRabbit UI
Review profile: ASSERTIVE
📒 Files selected for processing (9)
ebpf-samples(1 hunks)external/bpf_conformance(1 hunks)external/libbtf(1 hunks)src/crab/ebpf_domain.cpp(54 hunks)src/crab/ebpf_domain.hpp(3 hunks)src/crab/fwd_analyzer.cpp(2 hunks)src/crab_verifier.cpp(3 hunks)src/main/check.cpp(1 hunks)test-data/jump.yaml(21 hunks)
🧰 Additional context used
🪛 cppcheck
src/crab/ebpf_domain.cpp
[style] 1286-1286: The function 'truncate' is never used.
(unusedFunction)
🔇 Additional comments (19)
ebpf-samples (1)
1-1: Verify submodule compatibility with new architecture.
The submodule update appears intentional, but given the significant architectural changes in the main project (splitting ebpf_domain_t), please ensure this specific version of ebpf-samples is compatible with the new domain/transformer/checker structure.
Let's verify the submodule changes:
✅ Verification successful
Let me try a different approach to verify the submodule changes.
Let me try one final verification to check if the submodule is properly initialized and to examine its contents.
Submodule update appears safe and properly structured
The submodule has been successfully initialized and checked out to the new commit 325cce1. The repository structure shows a well-organized collection of eBPF samples across different categories (linux, cilium, falco, etc.) with no obvious breaking changes. Since this is a test samples repository, the update is unlikely to affect the main project's architectural changes, as these samples serve as test cases rather than dependent code.
🏁 Scripts executed
The following scripts were executed for the analysis:
Script:
#!/bin/bash
# Description: Analyze the submodule changes between the old and new commits
# to ensure compatibility with the new architecture.
# Test 1: Check commit message and changes
echo "Analyzing commit changes in ebpf-samples submodule..."
git -C ebpf-samples log --oneline --patch 33f01fafa414520ad56ab219db343422bb655b32..325cce1bc528a8b70e02ea914d407b4e4f89731d
# Test 2: Look for any related configuration or interface files that might need updates
echo "Checking for potential interface files..."
cd ebpf-samples && fd -e yaml -e h -e hpp
Length of output: 551
Script:
#!/bin/bash
# Check the current state of the submodule
echo "Current submodule status:"
git submodule status
# Try to get information about the submodule URL and branch
echo -e "\nSubmodule configuration:"
git config --file .gitmodules --get-regexp '^submodule\..*\.(path|url)$'
# List files in the submodule directory
echo -e "\nFiles in ebpf-samples directory:"
ls -la ebpf-samples/
# Check if there's a jump.yaml file mentioned in the PR context
echo -e "\nSearching for jump.yaml:"
find ebpf-samples -name "jump.yaml" -type f
Length of output: 1300
Script:
#!/bin/bash
# Initialize and update the submodule
echo "Initializing and updating submodule:"
git submodule update --init ebpf-samples
echo -e "\nListing contents after initialization:"
ls -la ebpf-samples/
echo -e "\nChecking git status of submodule:"
cd ebpf-samples && git status
Length of output: 1908
external/bpf_conformance (1)
1-1: Verify compatibility with main PR changes.
The subproject commit reference update appears to be part of a coordinated effort to synchronize dependencies. However, since this PR involves significant restructuring of ebpf_domain_t, please ensure this specific version of bpf_conformance is compatible with the new domain/transformer/checker separation.
Let's verify the commit message and changes in the referenced commit:
external/libbtf (1)
1-1: Verify compatibility with the new libbtf version.
The subproject update looks good. However, since this is a dependency update, please ensure that:
- The new version is compatible with the refactored
ebpf_domain_tstructure - All existing functionality depending on libbtf continues to work as expected
Let's check for any major changes in the libbtf subproject:
src/main/check.cpp (1)
41-41: LGTM: Performance optimization for string parameter.
The change from std::string to const std::string& is a good optimization that avoids unnecessary string copies when looking up conformance groups.
test-data/jump.yaml (7)
763-766: LGTM: Consistent post-conditions for pointer comparison tests.
The post-conditions for JNE, JSET, and JNSET tests with pointers are consistent, correctly verifying:
- The context offset remains unchanged
- The value range is preserved
- The type remains ctx
Also applies to: 788-791, 812-815
885-885: LGTM: Consistent error handling for greater-than comparisons.
The error messages for JGT, JGE, JSGT, and JSGE tests correctly handle:
- Unreachable code detection
- Invalid type checking for pointer comparisons
- Proper sequencing of error messages
Also applies to: 897-899, 911-911, 923-925, 993-993, 1006-1008, 1020-1020, 1033-1035
942-948: LGTM: Consistent post-conditions for signed comparisons.
The post-conditions for JSLT, JSLE, and JSGT tests properly verify:
- Register value preservation
- Type checking
- Value range constraints
Also applies to: 952-952, 970-976, 981-981, 998-1001, 1006-1008
1052-1058: LGTM: Consistent 32-bit comparison handling.
The post-conditions and error messages for JEQ32, JNE32, and JSET32 tests correctly:
- Maintain type consistency
- Preserve value ranges
- Handle unreachable code cases
Also applies to: 1063-1063, 1080-1083, 1088-1090, 1107-1110, 1115-1116
1133-1136: LGTM: Consistent error handling for 32-bit bitwise operations.
The error messages for JNSET32, JLT32, and JLE32 tests properly handle:
- Invalid type checks
- Unreachable code detection
- Proper error sequencing
Also applies to: 1141-1142, 1159-1165, 1170-1170, 1187-1190, 1195-1196
1208-1208: LGTM: Consistent 32-bit greater-than comparison handling.
The post-conditions and error messages for JGT32 and JGE32 tests correctly:
- Maintain type consistency
- Handle unreachable code
- Verify invalid type cases
Also applies to: 1213-1216, 1221-1222, 1234-1234, 1239-1242, 1247-1249
1266-1272: LGTM: Consistent 32-bit signed comparison handling.
The post-conditions and error messages for JSLT32, JSLE32, JSGT32, and JSGE32 tests properly:
- Verify register states
- Handle type checking
- Manage unreachable code cases
Also applies to: 1277-1277, 1294-1300, 1305-1305, 1317-1317, 1322-1325, 1330-1332, 1344-1344, 1349-1352, 1357-1359
src/crab/fwd_analyzer.cpp (2)
73-75: Transformation now processes each instruction individually
The code change correctly updates the transform_to_post method to apply the ebpf_transformer to each GuardedInstruction within the basic block. This enhances granularity in how transformations are applied.
135-136: Loop counter initialization encapsulated in ebpf_transformer
The modification to use ebpf_transformer{entry_inv}.initialize_loop_counter(label); appropriately encapsulates loop counter initialization within the transformer class, improving modularity and code organization.
src/crab_verifier.cpp (4)
65-67: Initialization and Setup of pre_bot and checker Are Correct
The introduction of pre_bot and the initialization of crab::ebpf_checker with from_inv correctly reflect the separation of concerns after refactoring. This aligns with the PR objective to split ebpf_domain_t into domain, transformer, and checker.
90-95: Proper Handling of Assertions and Instructions
The nested loops efficiently process each GuardedInstruction and its associated Assertions. The use of checker(assertion); ensures that all preconditions are appropriately checked before applying the transformer. The refactored code enhances readability and maintainability.
95-95: 🧹 Nitpick (assertive)
Remove Unnecessary Semicolon After Closing Brace
There is an unnecessary semicolon after the closing brace of the for-loop at line 95. Removing it will improve code clarity and adhere to standard coding practices.
Apply this diff to remove the unnecessary semicolon:
- };
+ }Likely invalid or redundant comment.
180-180: Ensure All References to setup_entry Are Updated
With the change from ebpf_domain_t::setup_entry to crab::ebpf_transformer::setup_entry, please verify that all references to setup_entry throughout the codebase have been updated accordingly to prevent any inconsistencies or runtime errors.
Run the following script to check for any remaining outdated references:
✅ Verification successful
Based on the search results, I can now provide a conclusive response:
No Action Required - Change is Consistent
The change from ebpf_domain_t::setup_entry to crab::ebpf_transformer::setup_entry is correct and consistent with the codebase. The search results show that:
setup_entryis correctly defined in theebpf_transformerclass insrc/crab/ebpf_domain.hpp- All usages of
setup_entryin the codebase are already using the correctebpf_transformer::setup_entryform:- In
src/crab_verifier.cpp:crab::ebpf_transformer::setup_entry(true) - In
src/crab/ebpf_domain.cpp:ebpf_transformer::setup_entry(false)
- In
🏁 Scripts executed
The following scripts were executed for the analysis:
Script:
#!/bin/bash
# Description: Verify there are no remaining references to `ebpf_domain_t::setup_entry`
# Test: Search for old references. Expect: No matches found.
rg 'ebpf_domain_t::setup_entry'
Length of output: 31
Script:
#!/bin/bash
# Let's search for any usage of setup_entry to understand the context better
rg "setup_entry" -A 2
# Also search for ebpf_domain_t to understand its usage
rg "ebpf_domain_t" -A 2
# Look for transformer class definition
ast-grep --pattern 'class ebpf_transformer {
$$$
}'
Length of output: 17068
src/crab/ebpf_domain.hpp (2)
49-49: New method calculate_constant_limits is appropriately introduced
The static method calculate_constant_limits enhances ebpf_domain_t by providing functionality to compute constant limits, which is beneficial for the domain's operations.
60-69: Accessor methods correctly utilize [[nodiscard]] and return types
The new accessor methods for map properties are well-defined, with proper use of [[nodiscard]] to prevent ignored return values and appropriate return types (std::optional<uint32_t> and interval_t).
| post: | ||
| - r1.ctx_offset=0 | ||
| - r1.svalue=[1, 2147418112] | ||
| - r1.type=ctx |
There was a problem hiding this comment.
This seems correct to me, but I'm not 100% sure, and I don't know why this was not already the case. This PR is supposed to only be a refactoring, so I may have introduced a bug.
@Alan-Jowett what do you think?
There was a problem hiding this comment.
I'm merging the PR despite this question. If needed it will be fixed later on.
There was a problem hiding this comment.
Turns out I broke assume-assert. Will fix soon.
Signed-off-by: Elazar Gershuni <[email protected]>
The checks and transforms occur on different places and have different dependencies. They may also be moved in the future to different cpp files.
There were mistakes on jump.yaml, but I'm not sure what's the reason for the different results.
Summary by CodeRabbit
Release Notes
New Features
ebpf_checkerandebpf_transformerfor enhanced handling of eBPF operations.Improvements
Bug Fixes
Refactor
ebpf_domain_tclass to improve organization and functionality.