Cleanup interval bound handling #692
Conversation
Signed-off-by: Elazar Gershuni <[email protected]>
WalkthroughThe changes primarily involve refactoring and enhancing the code in multiple files related to the Changes
Possibly related PRs
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
📜 Review details
Configuration used: CodeRabbit UI
Review profile: ASSERTIVE
📒 Files selected for processing (7)
- src/crab/ebpf_domain.cpp (19 hunks)
- src/crab/ebpf_domain.hpp (2 hunks)
- src/crab/interval.hpp (2 hunks)
- src/crab/split_dbm.cpp (1 hunks)
- src/crab_utils/debug.hpp (1 hunks)
- src/crab_utils/num_big.hpp (2 hunks)
- src/string_constraints.hpp (1 hunks)
🧰 Additional context used
📓 Learnings (1)
src/crab_utils/num_big.hpp (1)
Learnt from: elazarg PR: vbpf/ebpf-verifier#689 File: src/crab_utils/num_big.hpp:30-30 Timestamp: 2024-09-26T00:56:36.307Z Learning: Casting enums to `int64_t` in the `number_t` constructor is intentional and should not be flagged.
🔇 Additional comments (7)
src/string_constraints.hpp (1)
35-35: LGTM! Formatting improvement.The formatting change in the
string_invariantconstructor improves consistency with the coding style used in the rest of the file. It's a good practice to maintain consistent formatting throughout the codebase.src/crab_utils/num_big.hpp (2)
30-30: Improved type safety for enum constructorThe updated constructor now uses
std::underlying_type_t<decltype(n)>instead ofint64_tfor casting enum values. This change enhances type safety and provides better compatibility with different enum types, as it uses the actual underlying type of the enum.While a previous learning suggested that casting to
int64_twas intentional, this change appears to be an improvement in line with modern C++ practices.
Line range hint
30-44: Summary: Improved enum handling innumber_tclassThe changes in this file enhance the
number_tclass's handling of enumeration types:
- The constructor for enum types now uses
std::underlying_type_tfor more precise type conversion.- A new
cast_to()method allows for type-safe conversion fromnumber_tback to enum types.These improvements contribute to better type safety and more consistent handling of enum types throughout the codebase. The changes align well with the PR objective of cleaning up interval bound handling.
src/crab/ebpf_domain.hpp (3)
Line range hint
1-262: Summary of changesThe changes in this file improve code clarity and potentially performance:
- Renaming
shared_region_sizetopacket_sizein thecheck_access_packetmethod enhances readability and consistency.- Changing the parameter type to
NumAbsDomain&&inselectively_join_based_on_typemethod allows for move semantics, potentially improving performance.Both changes are approved, but please ensure to run the provided verification scripts to check for any potential issues in the wider codebase.
252-252: Approve parameter type change for potential performance improvement.The change from
NumAbsDomain&toNumAbsDomain&&for thesrcparameter in theselectively_join_based_on_typemethod allows for rvalue references. This can potentially improve performance by enabling move semantics, suggesting that thesrcobject is likely to be moved from rather than copied.To ensure this change is implemented correctly and doesn't introduce any issues, please run the following script to check the method's implementation and its usage across the codebase:
#!/bin/bash # Check the implementation of selectively_join_based_on_type echo "Checking implementation:" rg --type cpp -A 10 "void selectively_join_based_on_type\(NumAbsDomain& dst, NumAbsDomain&& src\)" echo "\nChecking usage:" # Check for calls to selectively_join_based_on_type rg --type cpp "selectively_join_based_on_type\s*\("Also, please ensure that:
- The method implementation takes advantage of move semantics where appropriate.
- All call sites are updated to pass rvalue references (e.g., using
std::move) when necessary.
179-179: Approve parameter rename for improved clarity.The rename from
shared_region_sizetopacket_sizein thecheck_access_packetmethod improves code clarity and consistency. It better reflects the method's purpose of checking packet access.To ensure this change doesn't introduce any issues, please run the following script to check for any remaining occurrences of
shared_region_sizein relation to packet access:✅ Verification successful
Verified: No remaining occurrences of
shared_region_sizefound outsidesrc/crab/ebpf_domain.hpp.The parameter rename from
shared_region_sizetopacket_sizein thecheck_access_packetmethod has been successfully applied throughout the codebase without any lingering references.🏁 Scripts executed
The following scripts were executed for the analysis:
Script:
#!/bin/bash # Search for any remaining occurrences of 'shared_region_size' related to packet access rg --type cpp "shared_region_size.*packet" -g '!src/crab/ebpf_domain.hpp'Length of output: 1530
src/crab/split_dbm.cpp (1)
300-300: Use oftrim_intervalinadd_univar_disequationenhances interval adjustmentIntegrating
trim_intervalintoadd_univar_disequationsimplifies the handling of intervals when adding univariate disequations. This change improves code clarity and ensures consistent interval adjustments.
Signed-off-by: Elazar Gershuni <[email protected]>
Signed-off-by: Elazar Gershuni <[email protected]>
There was a problem hiding this comment.
Actionable comments posted: 2
🧹 Outside diff range comments (1)
src/crab/ebpf_domain.cpp (1)
Line range hint
348-360: Possible Uninitialized VariablelpubUsedIn the blocks starting at lines 348 and 359, the variable
lpubis declared but may not be initialized before use if certain conditions are not met.Ensure that
lpubis properly initialized before it is used in any expressions to avoid undefined behavior.
📜 Review details
Configuration used: CodeRabbit UI
Review profile: ASSERTIVE
📒 Files selected for processing (2)
- src/crab/ebpf_domain.cpp (19 hunks)
- src/crab/interval.hpp (2 hunks)
🧰 Additional context used
📓 Learnings (2)
src/crab/ebpf_domain.cpp (3)
Learnt from: elazarg PR: vbpf/ebpf-verifier#692 File: src/crab/ebpf_domain.cpp:1366-1367 Timestamp: 2024-09-27T00:34:47.474Z Learning: The project is compiled with C++20.Learnt from: elazarg PR: vbpf/ebpf-verifier#692 File: src/crab/ebpf_domain.cpp:641-642 Timestamp: 2024-09-27T00:33:26.772Z Learning: The project uses the C++20 standard and supports C++20 features.Learnt from: elazarg PR: vbpf/ebpf-verifier#692 File: src/crab/ebpf_domain.cpp:884-893 Timestamp: 2024-09-27T00:36:08.058Z Learning: When analyzing the `operator|=(ebpf_domain_t&& other)` method in `src/crab/ebpf_domain.cpp`, ensure to carefully read the control flow and verify whether the moved-from object `other` is actually used after `std::move`.src/crab/interval.hpp (1)
Learnt from: elazarg PR: vbpf/ebpf-verifier#692 File: src/crab/interval.hpp:89-94 Timestamp: 2024-09-27T00:32:54.738Z Learning: In the `bound(T lb, T ub)` method within `interval_t`, safety when dereferencing optional values of `_lb.number()` and `_ub.number()` is ensured by the meet operation in the first line. Therefore, it's acceptable to dereference without checking for infinite bounds in this context.
🔇 Additional comments (7)
src/crab/interval.hpp (1)
99-104:⚠️ Potential issuePotential undefined behavior when casting to enum types
In the
bound(T elb, T eub) constmethod, you are casting integral values back to the enum typeTusingstatic_cast<T>(lb)andstatic_cast<T>(ub). If the valueslbandubdo not correspond to valid enumerators ofT, this can lead to undefined behavior.Consider adding a validation step to ensure that the casted values are valid enumerators of the enum
Tbefore returning them. Alternatively, you might return the underlying integral values or use a safer casting method that handles invalid values appropriately.⛔ Skipped due to learnings
Learnt from: elazarg PR: vbpf/ebpf-verifier#692 File: src/crab/interval.hpp:89-94 Timestamp: 2024-09-27T00:32:54.738Z Learning: In the `bound(T lb, T ub)` method within `interval_t`, safety when dereferencing optional values of `_lb.number()` and `_ub.number()` is ensured by the meet operation in the first line. Therefore, it's acceptable to dereference without checking for infinite bounds in this context.src/crab/ebpf_domain.cpp (6)
641-642: LGTM!The use of structured bindings here is appropriate and enhances code readability. No issues identified.
884-884: Potential Use of Moved-From Object Afterstd::moveIn the
operator|=(ebpf_domain_t&& other)method, after movingotherinto*thisat line 884:*this = std::move(other);There are further uses of
otherat lines 891 and 893:type_inv.selectively_join_based_on_type(m_inv, std::move(other.m_inv)); stack |= std::move(other.stack);Since
otherhas been moved, accessing its members may lead to undefined behavior. However, upon closer examination, the move occurs within a conditional block:if (is_bottom()) { *this = std::move(other); return; }This means that if
is_bottom()istrue, we moveotherinto*thisand return immediately. In the subsequent code whereotheris used, it is guaranteed thatis_bottom()isfalse, and thusotherhas not been moved yet. Therefore, the usage is safe.Also applies to: 891-891, 893-893
1346-1346: LGTM!The function
has_typecorrectly returns whether the interval contains the specified type. No issues found.
1366-1367: LGTM!The use of structured bindings and the for-loop to iterate over type encodings enhances code clarity. No issues identified.
Also applies to: 1370-1370
1454-1454: LGTM!The addition of
shared_region_sizeas a parameter and its use in therequirefunction improves the function's correctness in checking bounds. No issues found.Also applies to: 1457-1457
147-148:⚠️ Potential issuePotential Null Pointer Dereference in Interval Bounds Access
In the lines where
left_svalue_interval.lb().number()->cast_to<int64_t>()andleft_svalue_interval.ub().number()->cast_to<int64_t>()are called, there is a risk of dereferencing a null pointer ifleft_svalue_interval.lb().number()orleft_svalue_interval.ub().number()returnsnullptr. This can occur if the interval is unbounded or represents an empty interval.To ensure safety, please add checks to verify that
left_svalue_interval.lb().number()andleft_svalue_interval.ub().number()are notnullptrbefore dereferencing.Apply this diff to add null pointer checks:
if (auto size = left_svalue_interval.finite_size()) { - int64_t lb = left_svalue_interval.lb().number()->cast_to<int64_t>(); + auto lb_number = left_svalue_interval.lb().number(); + if (!lb_number) { + // Handle the case where lb_number is null + // Possibly return or continue safely + } + int64_t lb = lb_number->cast_to<int64_t>(); // ... - const int64_t ub = left_svalue_interval.ub().number()->cast_to<int64_t>(); + auto ub_number = left_svalue_interval.ub().number(); + if (!ub_number) { + // Handle the case where ub_number is null + // Possibly return or continue safely + } + int64_t ub = ub_number->cast_to<int64_t>();Also applies to: 152-152, 166-166
⛔ Skipped due to learnings
Learnt from: elazarg PR: vbpf/ebpf-verifier#689 File: src/crab/ebpf_domain.cpp:210-212 Timestamp: 2024-09-25T23:02:10.338Z Learning: Always truncating intervals without checking if they are already within the desired range is acceptable and simplifies the code.
|
This PR introduces some 25% performance speedup to the CI. |
Summary by CodeRabbit
Release Notes
New Features
interval_tclass for enhanced functionality, including a method to return interval bounds as a tuple.Improvements
check_access_packetmethod with a parameter name change for improved clarity.join_over_typesfor better readability.trim_intervalto near its use.Bug Fixes