Implement ebpf_check_constraints_at_label #729
Conversation
WalkthroughThe changes introduce several new functionalities and modifications across multiple files. A new function Changes
Assessment against linked issues
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: 11
📜 Review details
Configuration used: CodeRabbit UI
Review profile: ASSERTIVE
📒 Files selected for processing (8)
- src/asm_parse.hpp (1 hunks)
- src/asm_syntax.hpp (1 hunks)
- src/config.hpp (1 hunks)
- src/crab_verifier.cpp (5 hunks)
- src/crab_verifier.hpp (1 hunks)
- src/ebpf_yaml.cpp (6 hunks)
- src/ebpf_yaml.hpp (1 hunks)
- test-data/add.yaml (1 hunks)
🧰 Additional context used
📓 Learnings (1)
src/ebpf_yaml.cpp (1)
Learnt from: dthaler PR: vbpf/ebpf-verifier#721 File: src/ebpf_yaml.cpp:327-329 Timestamp: 2024-10-11T20:51:53.396Z Learning: In `src/ebpf_yaml.cpp`, avoid suggesting changes to error handling code in the `run_conformance_test_case` function if the code is not modified in the current PR.
🪛 GitHub Check: validate-yaml
test-data/add.yaml
[warning] 196-196:
196:6 [comments] too few spaces before comment
[warning] 200-200:
200:6 [comments] too few spaces before comment
[warning] 204-204:
204:7 [comments] too few spaces before comment
[warning] 196-196:
196:6 [comments] too few spaces before comment
[warning] 200-200:
200:6 [comments] too few spaces before comment
[warning] 204-204:
204:7 [comments] too few spaces before comment
🔇 Additional comments (9)
src/asm_parse.hpp (1)
6-6: LGTM: New header inclusions are appropriate.The added headers (, "crab/interval.hpp", and "crab/linear_constraint.hpp") are necessary for the new function declaration and align with the PR objectives of implementing constraint checking functionality.
Also applies to: 9-10
src/config.hpp (1)
24-24: Verify integration of the new optionWhile the addition of
store_pre_invariantsis correct, we should ensure its proper integration:
- Verify that
ebpf_verifier_default_options(declared at the end of this file) is updated to include a default value forstore_pre_invariants.- Check that
thread_local_optionsis properly initialized with this new option where relevant in the codebase.To verify the integration, run the following script:
This script will help ensure that the new option is properly integrated into the codebase.
src/crab_verifier.hpp (1)
29-42: LGTM! Function declaration aligns well with PR objectives.The new function
ebpf_check_constraints_at_labelis well-declared and documented. It accurately implements the PR objective of allowing users to compare a set of constraints against a model at a specific label. The function signature and documentation provide clear information about its purpose, parameters, and return value.test-data/add.yaml (3)
182-182: LGTM: Pre-conditions are well-defined.The pre-conditions for registers r0, r1, and r2 are clearly specified and consistent, initializing them as numbers with a value of 0. This sets up a good starting point for the test case.
184-190: LGTM: Code section is concise and relevant.The code section contains a series of simple arithmetic operations and register assignments. This is well-suited for testing the eBPF verifier's ability to track concrete register states, which aligns with the PR objectives.
179-219: Overall, the new test case is well-designed and aligns with PR objectives.The "check concrete state" test case is a valuable addition to the test suite. It effectively demonstrates the ability to check constraints at specific labels and verify concrete state invariants, which aligns perfectly with the PR objectives.
The test case is well-structured with clear pre-conditions, a concise code section, comprehensive invariants-to-check, and thorough post-conditions. The minor formatting and duplication issues mentioned earlier can be easily addressed to further improve the quality of the test case.
Great job on implementing this test case to validate the new
ebpf_check_constraints_at_labelfunctionality!🧰 Tools
🪛 GitHub Check: validate-yaml
[warning] 196-196:
196:6 [comments] too few spaces before comment
[warning] 200-200:
200:6 [comments] too few spaces before comment
[warning] 204-204:
204:7 [comments] too few spaces before comment
[warning] 196-196:
196:6 [comments] too few spaces before comment
[warning] 200-200:
200:6 [comments] too few spaces before comment
[warning] 204-204:
204:7 [comments] too few spaces before commentsrc/crab_verifier.cpp (2)
287-287: Validate label string before constructinglabel_tThe construction of
label_t label(label_string);assumes thatlabel_stringis a valid label. Consider adding validation to ensure thatlabel_stringcorresponds to a valid label in the program, and handle any exceptions that may be thrown if the label is invalid.You can verify whether the label exists by checking against the available labels in the
save_pre_invariants. If the label is invalid, provide a clear error message to the user.
305-309: Handle bottom abstract invariant appropriatelyIf the
from_inv(abstract invariant) is bottom, it means the program state at that label is unreachable.Ensure that this situation is expected in your use case. If reaching a bottom invariant is unexpected, you might need to investigate why the invariant is bottom at this label.
src/ebpf_yaml.cpp (1)
262-262: Verify the necessity of setting 'store_pre_invariants' to trueSetting
test_case.options.store_pre_invariantstotrueunconditionally may have unintended side effects or performance implications. Ensure that this option needs to be enabled for all test cases, or consider making it configurable per test case.
There was a problem hiding this comment.
Actionable comments posted: 7
📜 Review details
Configuration used: CodeRabbit UI
Review profile: ASSERTIVE
📒 Files selected for processing (8)
- src/asm_parse.hpp (1 hunks)
- src/asm_syntax.hpp (1 hunks)
- src/config.hpp (1 hunks)
- src/crab_verifier.cpp (5 hunks)
- src/crab_verifier.hpp (1 hunks)
- src/ebpf_yaml.cpp (6 hunks)
- src/ebpf_yaml.hpp (1 hunks)
- test-data/add.yaml (1 hunks)
🧰 Additional context used
🔇 Additional comments (11)
src/asm_parse.hpp (3)
6-6: LGTM: New header inclusions are appropriate.The added headers (, "crab/interval.hpp", "crab/linear_constraint.hpp") are necessary for the new function declaration and align with the PR objectives.
Also applies to: 9-10
14-21: Excellent addition of function documentation.The detailed comment above the
parse_linear_constraintsfunction provides clear information about its purpose, parameters, and return value. This addition addresses the suggestion from the previous review and enhances code readability and maintainability.
22-23: LGTM: New function declaration is well-structured and aligns with PR objectives.The
parse_linear_constraintsfunction declaration is appropriately designed with efficient parameter passing (const and reference) and a clear return type. The function signature matches the description in the comment and supports the new functionality for constraint checking.src/config.hpp (1)
24-25: LGTM: New option for storing pre-invariants added with clear documentationThe addition of
bool store_pre_invariants;to theebpf_verifier_options_tstructure is appropriate and aligns with the PR objectives. The comment explaining its purpose is clear and concise, which improves code readability and maintainability.src/ebpf_yaml.hpp (1)
17-17: LGTM! Documentation suggestion addressed.The new member variable
invariants_to_checkis well-defined and appropriately documented. The inline comment clearly explains its purpose, addressing the suggestion from the previous review.This addition aligns with the PR objectives, enabling the checking of constraints at specific labels. The use of
std::map<std::string, std::set<std::string>>is a good choice for efficient lookup and prevention of duplicate invariants.test-data/add.yaml (1)
178-261: Excellent addition of comprehensive test cases.The two new test cases, "check concrete state" and "check concrete state - negative", are excellent additions to the test suite. They provide thorough coverage of the new functionality for checking constraints at specific labels, including both positive and negative scenarios. These test cases align perfectly with the PR objectives and significantly enhance the overall quality of the test suite.
Great job on improving the test coverage and ensuring the robustness of the new feature!
src/ebpf_yaml.cpp (5)
102-102: LGTMThe addition of the
invariants_to_checkmember toRawTestCaseis appropriate and integrates well with the existing code. This allows for the storage of invariants to check from the YAML test cases.
130-142: Function 'parse_invariants_to_check' is correctly implementedThe function properly checks for the existence of
'invariants-to-check'before accessing it, preventing potential exceptions. It correctly parses the invariants and constructs the required map for further processing.
151-151: Assignment of 'invariants_to_check' in 'parse_case'The field
invariants_to_checkinRawTestCaseis correctly initialized using theparse_invariants_to_check(case_node)function. This ensures that the invariants are properly loaded from the YAML configuration.
223-225: Proper propagation of 'invariants_to_check' in 'read_case'The
invariants_to_checkmember is correctly assigned fromraw_caseto the newTestCase, ensuring that the invariants are available for verification during test execution.
266-267: Setting 'store_pre_invariants' to 'true'Setting
test_case.options.store_pre_invariantstotrueensures that pre-invariants are stored. This is necessary for checking invariants at specific labels during the test case execution.
Alan-Jowett
force-pushed
the
issue728
branch
3 times, most recently
from
8a8a8fd
to
73a9473
Compare
|
The PR was rebased. @coderabbitai full review |
|
@Alan-Jowett: Understood, I will perform a full review of the updated PR. ✅ Actions performedFull review triggered. |
There was a problem hiding this comment.
Actionable comments posted: 10
📜 Review details
Configuration used: CodeRabbit UI
Review profile: ASSERTIVE
📒 Files selected for processing (9)
- src/asm_parse.hpp (1 hunks)
- src/asm_syntax.hpp (1 hunks)
- src/config.cpp (1 hunks)
- src/config.hpp (1 hunks)
- src/crab_verifier.cpp (5 hunks)
- src/crab_verifier.hpp (1 hunks)
- src/ebpf_yaml.cpp (6 hunks)
- src/ebpf_yaml.hpp (1 hunks)
- test-data/add.yaml (1 hunks)
🧰 Additional context used
📓 Learnings (2)
src/ebpf_yaml.cpp (1)
Learnt from: dthaler PR: vbpf/ebpf-verifier#721 File: src/ebpf_yaml.cpp:327-329 Timestamp: 2024-10-11T20:51:53.396Z Learning: In `src/ebpf_yaml.cpp`, avoid suggesting changes to error handling code in the `run_conformance_test_case` function if the code is not modified in the current PR.test-data/add.yaml (1)
Learnt from: Alan-Jowett PR: vbpf/ebpf-verifier#729 File: test-data/add.yaml:220-261 Timestamp: 2024-10-14T21:52:47.957Z Learning: In `test-data/add.yaml`, error messages in test cases should match the style used by the verifier by including the label number at the beginning of the message, e.g., `"3: message"`.
🔇 Additional comments (8)
src/asm_parse.hpp (2)
6-6: LGTM: New includes are appropriate and well-organized.The added includes for
<vector>,"crab/interval.hpp", and"crab/linear_constraint.hpp"are necessary for the new function declaration. The ordering of includes follows good practices, with standard library headers preceding project-specific ones.Also applies to: 9-10
14-23: LGTM: Well-documented function declaration aligns with PR objectives.The new
parse_linear_constraintsfunction declaration is well-structured and consistent with the existing code style. The added documentation provides a clear description of the function's purpose, parameters, and return value, which addresses the previous review comments and enhances code readability and maintainability.src/config.hpp (1)
24-25: LGTM: New option for storing pre-invariants added with clear documentationThe addition of
bool store_pre_invariants;to theebpf_verifier_options_tstructure is appropriate and aligns with the PR objectives. The inline comment clearly explains the purpose of this new option, which enhances code readability and maintainability.src/ebpf_yaml.hpp (1)
17-17: LGTM! Documentation added as suggested.The new member variable
invariants_to_checkhas been added to theTestCasestruct with appropriate documentation. This addition aligns well with the PR objectives, allowing for the storage and checking of invariants at specific labels. The implementation uses suitable data structures (std::mapandstd::set) for efficient lookup and prevention of duplicate invariants.The inline comment provides a clear explanation of the member's purpose, addressing the suggestion from the previous review.
test-data/add.yaml (1)
180-261: Overall: Excellent addition of test cases for constraint checking.The two new test cases, "check concrete state" and "check concrete state - negative", are valuable additions to the test suite. They effectively cover the functionality of checking constraints at specific labels, which aligns perfectly with the PR objectives. The positive and negative test scenarios provide comprehensive coverage for the new
ebpf_check_constraints_at_labelAPI function.These test cases will help ensure the reliability and correctness of the constraint checking feature, contributing to the overall robustness of the eBPF verifier.
src/asm_syntax.hpp (1)
26-47: Well-implemented constructor and appropriate exception handlingThe new
label_tconstructor correctly parses the inputstd::string_viewto initializefrom,to, andstack_frame_prefix. Exception handling forstd::invalid_argumentandstd::out_of_rangeis properly implemented, ensuring robustness against invalid inputs.src/crab_verifier.cpp (1)
165-166: Confirm thread-local storage usage forsave_pre_invariantsThe introduction of
static thread_local std::optional<crab::invariant_table_t> save_pre_invariantsensures that pre-invariants are stored per thread. If the verifier operates in a multi-threaded environment, this approach is appropriate. However, please verify that all accesses tosave_pre_invariantsare thread-safe and that its use aligns with the intended concurrency model.src/ebpf_yaml.cpp (1)
130-142: Functionparse_invariants_to_checkhandles YAML parsing correctlyThe
parse_invariants_to_checkfunction effectively parses the "invariants-to-check" node from the YAML file and appropriately handles the case when the node is not defined, ensuring robustness against missing data.
Signed-off-by: Alan Jowett <[email protected]>
There was a problem hiding this comment.
Actionable comments posted: 7
📜 Review details
Configuration used: CodeRabbit UI
Review profile: ASSERTIVE
📒 Files selected for processing (9)
- src/asm_parse.hpp (1 hunks)
- src/asm_syntax.hpp (1 hunks)
- src/config.cpp (1 hunks)
- src/config.hpp (1 hunks)
- src/crab_verifier.cpp (5 hunks)
- src/crab_verifier.hpp (1 hunks)
- src/ebpf_yaml.cpp (6 hunks)
- src/ebpf_yaml.hpp (1 hunks)
- test-data/add.yaml (1 hunks)
🧰 Additional context used
📓 Learnings (2)
src/ebpf_yaml.cpp (1)
Learnt from: dthaler PR: vbpf/ebpf-verifier#721 File: src/ebpf_yaml.cpp:327-329 Timestamp: 2024-10-11T20:51:53.396Z Learning: In `src/ebpf_yaml.cpp`, avoid suggesting changes to error handling code in the `run_conformance_test_case` function if the code is not modified in the current PR.test-data/add.yaml (1)
Learnt from: Alan-Jowett PR: vbpf/ebpf-verifier#729 File: test-data/add.yaml:220-261 Timestamp: 2024-10-14T21:52:47.957Z Learning: In `test-data/add.yaml`, error messages in test cases should match the style used by the verifier by including the label number at the beginning of the message, e.g., `"3: message"`.
🔇 Additional comments (17)
src/config.cpp (1)
17-17: LGTM! Consider adding documentation for the new option.The addition of
.store_pre_invariants = falseis consistent with the PR objectives and provides a sensible default value. This new option enhances the configurability of the verifier, allowing users to opt-in to storing pre-invariants when needed.As previously suggested, consider adding a comment above this line or in the header file to briefly explain the purpose and usage of this new option. This would improve the maintainability of the code and help future developers understand its significance.
src/asm_parse.hpp (2)
6-6: LGTM: New includes are appropriate and well-ordered.The addition of these headers is necessary for the new
parse_linear_constraintsfunction. The ordering follows the convention of placing standard library headers before project-specific ones.Also applies to: 9-10
14-23: LGTM: Well-documented and properly declared new function.The
parse_linear_constraintsfunction declaration is well-structured and consistent with the existing code style. The added comment provides a clear description of the function's purpose, parameters, and return value, which enhances code readability and maintainability.src/config.hpp (1)
24-25: LGTM: Well-documented addition ofstore_pre_invariantsoptionThe new
store_pre_invariantsboolean member has been added to theebpf_verifier_options_tstructure with a clear and informative comment. This addition aligns well with the PR objectives and supports the new functionality for storing pre-invariants.The comment above the new member effectively explains its purpose, addressing the suggestion from the previous review. The naming is consistent with other boolean options in the structure, maintaining good code readability.
src/ebpf_yaml.hpp (1)
17-17: LGTM. Documentation added as suggested.The new member variable
invariants_to_checkhas been added to theTestCasestruct with appropriate documentation. This addition aligns well with the PR objectives and the requirements from the linked issue #728.The use of
std::map<std::string, std::set<std::string>>is a good choice for efficient lookup of invariants by label and prevention of duplicate invariants for each label.src/crab_verifier.hpp (1)
30-43: LGTM! Documentation enhancement implemented.The function declaration and documentation for
ebpf_check_constraints_at_labelare well-defined and align with the PR objectives. The previous suggestion to explain "abstract verifier constraints" has been implemented, improving the clarity of the documentation.src/crab_verifier.cpp (7)
20-20: Appropriate inclusion of 'asm_parse.hpp' headerThe inclusion of
#include "asm_parse.hpp"is necessary to expose the function for parsing linear constraints. This ensures that the parsing functionality is accessible within this source file.
165-166: Declaration of thread-local variable 'save_pre_invariants'The addition of the thread-local variable
save_pre_invariantscorrectly initializes it tostd::nullopt. This variable is used to store pre-invariants when thestore_pre_invariantsoption is enabled.
178-180: Conditional storage of pre-invariants in 'get_ebpf_report'The code appropriately checks if
store_pre_invariantsis enabled before storingpre_invariantsinsave_pre_invariants. This ensures that pre-invariants are only stored when required.
230-232: Conditional storage of pre-invariants in 'ebpf_analyze_program_for_test'Similarly, the function
ebpf_analyze_program_for_testnow storespre_invariantsinsave_pre_invariantswhenstore_pre_invariantsis enabled. This maintains consistency across functions that perform analysis.
279-280: Clearing thread-local state in 'ebpf_verifier_clear_thread_local_state'Resetting
save_pre_invariantstostd::nulloptensures that the thread-local state is properly cleared when the verifier's state is reset. This prevents any potential leakage of pre-invariants between verifications.
282-326: Implementation of 'ebpf_check_constraints_at_label' functionThe new
ebpf_check_constraints_at_labelfunction provides the ability to compare a set of constraints against the stored pre-invariants at a specific label. The function includes detailed error messages to aid in debugging when discrepancies are found.
328-337: Implementation of 'ebpf_get_invariants_at_label' functionThe addition of
ebpf_get_invariants_at_labelallows retrieval of the stored invariants at a given label. The function checks if pre-invariants are available and returns them appropriately.src/ebpf_yaml.cpp (4)
102-102: Addition of 'invariants_to_check' to 'RawTestCase' StructureThe new member
invariants_to_checkis appropriately added to theRawTestCasestruct to store invariants for testing purposes.
151-151: Initializing 'invariants_to_check' in 'parse_case' FunctionThe
parse_casefunction correctly initializes theinvariants_to_checkmember by invokingparse_invariants_to_check(case_node).
223-225: Transferring 'invariants_to_check' to 'TestCase'The
read_casefunction appropriately transfers theinvariants_to_checkmember fromRawTestCasetoTestCase, ensuring that the invariants are available for test execution.
266-269: Setting 'store_pre_invariants' Based on Invariants to CheckThe logic correctly sets
test_case.options.store_pre_invariantstotruewhentest_case.invariants_to_checkis not empty, enabling the storage of pre-invariants necessary for invariant checks.
Signed-off-by: Alan Jowett <[email protected]>
There was a problem hiding this comment.
Actionable comments posted: 3
📜 Review details
Configuration used: CodeRabbit UI
Review profile: ASSERTIVE
📒 Files selected for processing (5)
- src/config.cpp (1 hunks)
- src/crab_verifier.cpp (5 hunks)
- src/crab_verifier.hpp (1 hunks)
- src/ebpf_yaml.cpp (6 hunks)
- test-data/add.yaml (1 hunks)
🧰 Additional context used
📓 Learnings (3)
src/crab_verifier.cpp (1)
Learnt from: Alan-Jowett PR: vbpf/ebpf-verifier#729 File: src/crab_verifier.cpp:323-326 Timestamp: 2024-10-16T04:59:11.616Z Learning: In `src/crab_verifier.cpp`, all exceptions thrown in the function `ebpf_check_constraints_at_label` derive from `std::exception`, making a catch-all handler unnecessary.src/crab_verifier.hpp (1)
Learnt from: Alan-Jowett PR: vbpf/ebpf-verifier#729 File: src/crab_verifier.hpp:44-51 Timestamp: 2024-10-16T05:00:24.900Z Learning: In `src/crab_verifier.hpp`, adding usage examples to the documentation of `ebpf_get_invariants_at_label` is not necessary.src/ebpf_yaml.cpp (1)
Learnt from: Alan-Jowett PR: vbpf/ebpf-verifier#729 File: src/ebpf_yaml.hpp:17-17 Timestamp: 2024-10-16T04:59:56.598Z Learning: Remember that the `invariants_to_check` member in `TestCase` is properly populated and used in the YAML parsing logic in `src/ebpf_yaml.cpp`.
🪛 GitHub Check: validate-yaml
test-data/add.yaml
[warning] 192-192:
192:6 [comments] too few spaces before comment
[warning] 196-196:
196:6 [comments] too few spaces before comment
[warning] 200-200:
200:6 [comments] too few spaces before comment
[warning] 204-204:
204:7 [comments] too few spaces before comment
[warning] 232-232:
232:6 [comments] too few spaces before comment
[warning] 236-236:
236:6 [comments] too few spaces before comment
[warning] 240-240:
240:6 [comments] too few spaces before comment
[warning] 244-244:
244:7 [comments] too few spaces before comment
[warning] 192-192:
192:6 [comments] too few spaces before comment
[warning] 196-196:
196:6 [comments] too few spaces before comment
🔇 Additional comments (13)
src/config.cpp (1)
17-17: LGTM! The new option is well-implemented and documented.The addition of
.store_pre_invariants = falsewith an explanatory comment is consistent with the PR objectives. It provides a sensible default value and clear guidance on its usage, enhancing the configurability of the verifier while maintaining backward compatibility.src/crab_verifier.hpp (3)
30-45: LGTM! Function aligns well with PR objectives.The
ebpf_check_constraints_at_labelfunction declaration and its documentation are well-defined and directly address the PR objectives. The function provides a way to compare concrete constraints against abstract verifier constraints at a specific label, which is a key requirement outlined in the linked issue #728.The documentation is comprehensive and includes a clear explanation of abstract constraints, which enhances usability. The function signature accurately reflects its purpose and the described behavior.
46-53: LGTM! Function complements the PR objectives well.The
ebpf_get_invariants_at_labelfunction declaration and its documentation are well-defined and support the PR objectives. This function provides a mechanism to retrieve invariants at a specific label, which is crucial for comparing abstract and concrete states as outlined in the linked issue #728.The documentation clearly states the function's purpose and requirements, and the exception handling is properly documented. The function signature accurately reflects its intended behavior.
29-53: Overall, excellent additions to the codebase.The new functions
ebpf_check_constraints_at_labelandebpf_get_invariants_at_labelare well-implemented and documented. They directly address the requirements outlined in the linked issue #728 and align perfectly with the PR objectives. These additions will significantly enhance the ability to compare abstract and concrete states in the BPF verification process.The code is clean, well-structured, and maintains the existing coding style of the file. Great job on these implementations!
test-data/add.yaml (2)
180-219: LGTM: Well-structured test case for concrete state checking.The "check concrete state" test case is well-designed and aligns perfectly with the PR objective of checking constraints at specific labels. The pre-conditions, code execution, invariants-to-check, and post-conditions are all correctly defined and provide a thorough validation of the register states throughout the execution.
🧰 Tools
🪛 GitHub Check: validate-yaml
[warning] 192-192:
192:6 [comments] too few spaces before comment
[warning] 196-196:
196:6 [comments] too few spaces before comment
[warning] 200-200:
200:6 [comments] too few spaces before comment
[warning] 204-204:
204:7 [comments] too few spaces before comment
[warning] 192-192:
192:6 [comments] too few spaces before comment
[warning] 196-196:
196:6 [comments] too few spaces before comment
220-261: LGTM: Well-designed negative test case for constraint checking.The "check concrete state - negative" test case is well-structured and serves as an excellent negative test for the constraint checking functionality. It intentionally includes an incorrect invariant to trigger a mismatch between concrete and abstract invariants, which aligns with the PR objectives.
The error message format correctly includes the label number at the beginning, which is consistent with the verifier's error reporting style.
🧰 Tools
🪛 GitHub Check: validate-yaml
[warning] 232-232:
232:6 [comments] too few spaces before comment
[warning] 236-236:
236:6 [comments] too few spaces before comment
[warning] 240-240:
240:6 [comments] too few spaces before comment
[warning] 244-244:
244:7 [comments] too few spaces before commentsrc/crab_verifier.cpp (6)
165-172: Modularize invariant saving logic for maintainabilityThe addition of
save_invariants_if_neededimproves code maintainability by encapsulating the logic for saving pre-invariants. This adheres to the DRY principle and makes future changes easier.
184-184: Ensure pre-invariants are saved consistentlyBy calling
save_invariants_if_needed(pre_invariants);, the function ensures that pre-invariants are stored when necessary. This is crucial for functions that rely on these invariants later in the verification process.
234-234: Consistent use of invariant saving functionThe invocation of
save_invariants_if_needed(pre_invariants);here ensures that pre-invariants are consistently saved across different analysis functions, promoting code consistency.
281-282: Properly clear thread-local stateResetting
saved_pre_invariantstostd::nulloptinebpf_verifier_clear_thread_local_stateensures that the thread-local state is clean for subsequent analyses. This prevents potential issues from residual data.
284-328: Robust exception handling during constraint checkingThe
ebpf_check_constraints_at_labelfunction is wrapped in atry-catchblock to handle exceptions derived fromstd::exception. This ensures that any errors during constraint checking are caught and reported gracefully.
330-341: Intentional exception propagation for label parsingIn
ebpf_get_invariants_at_label, constructinglabel_t l = label_t(label);may throw an exception if the label is invalid. The comment indicates that this is intentional so that the caller can handle malformed labels appropriately.src/ebpf_yaml.cpp (1)
266-269: Ensure side effects of setting 'store_pre_invariants' are intendedSetting
test_case.options.store_pre_invariantstotruewheninvariants_to_checkis not empty allows pre-invariants to be stored for later checks. Verify that enabling this option does not unintentionally affect other parts of the verifier or introduce performance overhead.To assess any potential side effects, consider reviewing where
store_pre_invariantsis used in the codebase:✅ Verification successful
Side Effects of Setting
store_pre_invariantsConfirmedAfter reviewing all usages of
store_pre_invariants, enabling this option is intentional and does not introduce unintended side effects or significant performance overhead. The flag is used in a controlled manner within the verifier, ensuring that activating it supports necessary functionalities without negatively impacting other parts of the system.🏁 Scripts executed
The following scripts were executed for the analysis:
Script:
#!/bin/bash # Description: Find all usages of 'store_pre_invariants' in the codebase. # Expected Result: Identify code that relies on 'store_pre_invariants' to ensure enabling it is safe. rg --type cpp 'store_pre_invariants'Length of output: 832
|
@elazarg is this the best option for allowing the caller to check the current concrete state of the vm against the abstract state the verifier has? I had considered just passing in the register values, but that doesn't really work well as there is additional context that the VM has that can be used to filter the assertions (things like if the register value is pointing to context, packet, shared, or stack memory) that the verifier would otherwise not know. This becomes an issue as the concrete values for pointers tend to be > 2GB which trips some assertions in the verifier. |
Resolves: #728
This pull request exposes a new API "ebpf_check_constraints_at_label" which permits the caller to compare a set of constraints against the model at a specific label. If the model and the constraints differ it will return the two sets of constraints.
Enhancements and New Features:
src/asm_parse.hpp: Exposed existing function to parse linear constraints.src/asm_syntax.hpp: Extended thelabel_tstruct to support initialization from a string label.src/config.hpp: Added a new option to store pre-invariants in the verifier options.src/crab_verifier.cpp: Implemented functions to store pre-invariants and check constraints at specific labels. [1] [2] [3] [4]src/crab_verifier.hpp: Declared the new function for checking constraints at a label.Test Case Updates:
src/ebpf_yaml.cpp: Updated YAML parsing to include invariants to check and modified test case execution to validate these invariants. [1] [2] [3] [4] [5]src/ebpf_yaml.hpp: Added a new field to theTestCasestruct for invariants to check.test-data/add.yaml: Added a new test case to check concrete state invariants.Summary by CodeRabbit
Summary by CodeRabbit
New Features
RawTestCasestructure to include invariants to check.TestCasestruct.Bug Fixes
Documentation
Chores