Add support for is_valid_before #825
Conversation
WalkthroughThis pull request updates the Changes
✨ Finishing Touches
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 (
|
|
@Alan-Jowett any idea why the code coverage failed? |
|
Converting this to draft for now. Fuzzer integration is failing for reasons I don't understand yet. |
Alan-Jowett
force-pushed
the
verifier_fuzzing_support
branch
from
7cbf769 to
c861682
Compare
It looks like it's failing for all PRs. |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 2
📜 Review details
Configuration used: CodeRabbit UI
Review profile: ASSERTIVE
Plan: Pro
📒 Files selected for processing (2)
src/crab_verifier.cpp(1 hunks)src/crab_verifier.hpp(1 hunks)
⏰ Context from checks skipped due to timeout of 90000ms (9)
- GitHub Check: build_ubuntu (Release, tests)
- GitHub Check: build_windows (Release, library)
- GitHub Check: build_windows (Release, tests)
- GitHub Check: build_windows (Debug, library)
- GitHub Check: build_windows (Debug, tests)
- GitHub Check: build_ubuntu (Debug, tests)
- GitHub Check: build_ubuntu (Release)
- GitHub Check: build_ubuntu (Debug)
- GitHub Check: Analyze (cpp)
🔇 Additional comments (2)
src/crab_verifier.cpp (2)
27-41: LGTM! Clear explanation of validation logic.The comment block effectively explains the validation outcomes and justifies the implementation change.
42-46: Verify the impact of changing the validation logic.The implementation has changed from using <= comparison to using intersection check.
Run this script to find all callers of is_valid_after:
✅ Verification successful
The validation logic change is safe and localized.
The method is internal to the Invariants class with no external callers. The new intersection-based implementation provides more precise state validation for abstract interpretation.
🏁 Scripts executed
The following scripts were executed for the analysis:
Script:
#!/bin/bash # Find all callers of is_valid_after to assess impact rg -l "is_valid_after" | xargs -I {} rg -A 2 "is_valid_after" {}Length of output: 466
Script:
#!/bin/bash # Case-insensitive search for is_valid_after rg -i "is_valid_after" -A 2 # Find usage of Invariants class rg "class Invariants" -A 5 # Find files containing Invariants:: to see all method calls rg "Invariants::" -A 2Length of output: 2928
| @@ -58,6 +58,7 @@ class Invariants final { | |||
| Invariants(const Invariants& invariants) = default; | |||
|
|
|||
| bool is_valid_after(const label_t& label, const string_invariant& state) const; | |||
| bool is_valid_before(const label_t& label, const string_invariant& state) const; | |||
There was a problem hiding this comment.
🧹 Nitpick (assertive)
Add documentation for is_valid_before method.
Document the method's purpose, parameters, return value, and relationship to is_valid_after. This is essential given the complex validation logic explained in the implementation file.
+ /// Checks if the given state is valid before the specified label by comparing
+ /// against the pre-invariant.
+ /// @param label The program point to check
+ /// @param state The state to validate
+ /// @return true if state is valid, false if it violates constraints
bool is_valid_before(const label_t& label, const string_invariant& state) const;📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
| bool is_valid_before(const label_t& label, const string_invariant& state) const; | |
| /// Checks if the given state is valid before the specified label by comparing | |
| /// against the pre-invariant. | |
| /// @param label The program point to check | |
| /// @param state The state to validate | |
| /// @return true if state is valid, false if it violates constraints | |
| bool is_valid_before(const label_t& label, const string_invariant& state) const; |
|
@elazarg This PR contains a change on how is_valid_after and is_valid_before operate. The specific issue is that the usage of the <= operator doesn't work for the uBPF use cases. Specifically, the uBPF doesn't know when the verifier havocs a register. If the abstract state from the uBPF concrete state contains constraints based on valid register state that verifier has havoced then the <= fails. Let me know if I am not understanding this correctly. |
Alan-Jowett
force-pushed
the
verifier_fuzzing_support
branch
from
45016a2 to
b3b36e1
Compare
Note, I understand you are busy, so no rush in responding to this. This was just notes for why I made the change for when you get a chance to review it. |
There was a problem hiding this comment.
Actionable comments posted: 3
📜 Review details
Configuration used: CodeRabbit UI
Review profile: ASSERTIVE
Plan: Pro
📒 Files selected for processing (2)
src/crab_verifier.cpp(1 hunks)src/crab_verifier.hpp(1 hunks)
⏰ Context from checks skipped due to timeout of 90000ms (9)
- GitHub Check: build_windows (Release, library)
- GitHub Check: build_windows (Release, tests)
- GitHub Check: build_windows (Debug, library)
- GitHub Check: build_ubuntu (Release, tests)
- GitHub Check: build_windows (Debug, tests)
- GitHub Check: build_ubuntu (Debug, tests)
- GitHub Check: build_ubuntu (Release)
- GitHub Check: build_ubuntu (Debug)
- GitHub Check: Analyze (cpp)
🔇 Additional comments (2)
src/crab_verifier.hpp (1)
61-61: Add documentation for is_valid_before method.Document the method's purpose, parameters, return value, and relationship to is_valid_after.
+ /// Checks if the given state is valid before the specified label by comparing + /// against the pre-invariant. + /// @param label The program point to check + /// @param state The state to validate + /// @return true if state is valid, false if it violates constraints bool is_valid_before(const label_t& label, const string_invariant& state) const;src/crab_verifier.cpp (1)
27-41: LGTM! Clear explanation of check outcomes.The comment block effectively explains the rationale behind the implementation change from <= to intersection checks.
| bool Invariants::is_valid_after(const label_t& label, const string_invariant& state) const { | ||
| const ebpf_domain_t abstract_state = | ||
| ebpf_domain_t::from_constraints(state.value(), thread_local_options.setup_constraints); | ||
| return abstract_state <= invariants.at(label).post; | ||
| return !(abstract_state & invariants.at(label).post).is_bottom(); | ||
| } |
There was a problem hiding this comment.
🧹 Nitpick (assertive)
Add inline comment explaining the intersection check.
Add a brief comment explaining why we're checking if the intersection is not bottom.
bool Invariants::is_valid_after(const label_t& label, const string_invariant& state) const {
const ebpf_domain_t abstract_state =
ebpf_domain_t::from_constraints(state.value(), thread_local_options.setup_constraints);
+ // Return false only if abstract_state violates post-invariant constraints
return !(abstract_state & invariants.at(label).post).is_bottom();
}📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
| bool Invariants::is_valid_after(const label_t& label, const string_invariant& state) const { | |
| const ebpf_domain_t abstract_state = | |
| ebpf_domain_t::from_constraints(state.value(), thread_local_options.setup_constraints); | |
| return abstract_state <= invariants.at(label).post; | |
| return !(abstract_state & invariants.at(label).post).is_bottom(); | |
| } | |
| bool Invariants::is_valid_after(const label_t& label, const string_invariant& state) const { | |
| const ebpf_domain_t abstract_state = | |
| ebpf_domain_t::from_constraints(state.value(), thread_local_options.setup_constraints); | |
| // Return false only if abstract_state violates post-invariant constraints | |
| return !(abstract_state & invariants.at(label).post).is_bottom(); | |
| } |
| bool Invariants::is_valid_after(const label_t& label, const string_invariant& state) const { | ||
| const ebpf_domain_t abstract_state = | ||
| ebpf_domain_t::from_constraints(state.value(), thread_local_options.setup_constraints); | ||
| return abstract_state <= invariants.at(label).post; | ||
| return !(abstract_state & invariants.at(label).post).is_bottom(); | ||
| } | ||
|
|
||
| bool Invariants::is_valid_before(const label_t& label, const string_invariant& state) const { | ||
| const ebpf_domain_t abstract_state = | ||
| ebpf_domain_t::from_constraints(state.value(), thread_local_options.setup_constraints); | ||
| return !(abstract_state & invariants.at(label).pre).is_bottom(); |
There was a problem hiding this comment.
💡 Codebase verification
Add unit tests for is_valid_before and is_valid_after methods
- Add test cases in src/test/test_verify.cpp covering:
- Valid pre-conditions
- Invalid pre-conditions
- Valid post-conditions
- Invalid post-conditions
- Current coverage is only through integration tests in ebpf_yaml.cpp
🔗 Analysis chain
Verify test coverage for both methods.
Both is_valid_before and is_valid_after need test coverage to ensure they handle all four cases described in the comments.
🏁 Scripts executed
The following scripts were executed for the analysis:
Script:
#!/bin/bash
# Description: Check test coverage for both methods
# Search for test files containing is_valid_before
echo "Searching for is_valid_before tests..."
rg "is_valid_before" "test/"
# Search for test files containing is_valid_after
echo "Searching for is_valid_after tests..."
rg "is_valid_after" "test/"
# Look for test files that might contain relevant test cases
echo "Searching for potential test files..."
fd -t f "test_.*\.(cpp|hpp)" "test/"
Length of output: 531
Script:
#!/bin/bash
# First, find any test-related files or directories
echo "Looking for test files and directories..."
fd -t d "test"
fd -t f "test"
# Search for files containing test in their name
echo -e "\nSearching for test-related files..."
fd -t f "(test|spec|check)"
# Search for files mentioning the class name
echo -e "\nSearching for files mentioning Invariants..."
rg -l "class.*Invariants"
Length of output: 954
Script:
#!/bin/bash
# Check test_verify.cpp content
echo "Checking test_verify.cpp content..."
rg -A 5 -B 5 "is_valid_(before|after)|Invariants::" "src/test/test_verify.cpp"
# Search for Invariants usage in all test files
echo -e "\nSearching for Invariants usage in tests..."
rg -A 3 -B 3 "Invariants" "src/test/"
# Look for related test patterns
echo -e "\nSearching for related verification tests..."
rg -l "TEST.*verify|verify.*test" "src/test/"
Length of output: 1642
There was a problem hiding this comment.
Actionable comments posted: 1
📜 Review details
Configuration used: CodeRabbit UI
Review profile: ASSERTIVE
Plan: Pro
📒 Files selected for processing (1)
src/crab/split_dbm.hpp(1 hunks)
⏰ Context from checks skipped due to timeout of 90000ms (4)
- GitHub Check: build_windows (Debug, tests)
- GitHub Check: build_ubuntu (Debug, tests)
- GitHub Check: build_ubuntu (Release)
- GitHub Check: build_ubuntu (Debug)
I think we're not using the same terminology, and maybe I chose overly generic names. I'll try to write what I understand in my own words.
The last sentence is exactly the test C# <= V#. Another way to write the same test is (C# /\ V#) = C#. Your proposed solution tests whether C# and V# have any common states. These questions differ only when C# represents more concrete states than C. If your fix is correct, then the lifting from C to C# is wrong. It might be due to missing constraints, or due to an overapproxination/bug. In general using the meet operator The invariants found by the verifier are intentionally overapproxinations. Havocing should not be a problem by itself since it only yields larger abstract states, and smaller abstract states are never guaranteed by the verifier. Do you know what is the source of overapproximation? (I really hope I'm not writing nonsense here. If I am, we can return to the discussion when I'm back. Alternatively we may want to consult with @caballa). |
|
To make things easier to reason about, I will re-introduce my changes to ebpf-yaml.cpp to make it easier to check via yaml test definitions. |
|
It might be easier with a C++ unit test |
|
A better approach might be to pass a set of simple constraints. |
|
I guess I simply don't understand what the <= operator does. Domain 1 only has the register values, while domain 2 has register values + type. Previously I was using & to test for the case where values in domain 1 are outside of the expected values in domain 3. Consider the following one register example: TEST_CASE("domain_operations", "[verify]") {
std::set<std::string> invariant1({
"r0.uvalue=0",
"r0.svalue=0",
});
std::set<std::string> invariant2({
"r0.type=number",
"r0.uvalue=0",
"r0.svalue=0",
});
std::set<std::string> invariant3({
"r0.type=number",
"r0.uvalue=[1,10]",
"r0.svalue=[1,10]",
});
const auto domain1 = crab::ebpf_domain_t::from_constraints(invariant1, false);
const auto domain2 = crab::ebpf_domain_t::from_constraints(invariant2, false);
const auto domain3 = crab::ebpf_domain_t::from_constraints(invariant3, false);
std::cerr << "domain 1 " << domain1 << std::endl;
std::cerr << "domain 2 " << domain2 << std::endl;
std::cerr << "domain 3 " << domain3 << std::endl;
std::cerr << "(domain1 <= domain2) " << (domain1 <= domain2) << std::endl;
std::cerr << "(domain2 <= domain1) " << (domain2 <= domain1) << std::endl;
std::cerr << "(domain1 & domain2) " << (domain1 & domain2) << std::endl;
std::cerr << "(domain1 <= domain3) " << (domain1 <= domain3) << std::endl;
std::cerr << "(domain3 <= domain1) " << (domain3 <= domain1) << std::endl;
std::cerr << "(domain1 & domain3) " << (domain1 & domain3) << std::endl;
}This outputs: Use case I am shooting for: Interpreter builds a set of invariants based on the register state and any knowledge it has about context, stack and shared pointers. |
|
It's about the meaning of missing values. In the input you mean "don't care", but the abstract state means "don't know". The operator <= says “left is more specific than right". What you are looking for is to ask "assuming the types are correct, are the values also correct". The meet operator & almost does that, except there's no way to limit it to types only. Another failed attempt might be to set all the types (and "don't care" values) to bottom. This would fail since bottom propagates in the normalization step. You can set explicitly all the types to be the same as the invariant, which is the assumption part. Alternatively you can havoc all the type values in the invariant. I think it's better since it's a single-state immutable operation: give me a new invariant, with only runtime values. Another solution, which from testing point of view is better, would be to add "taint tracking" to ubpf. Of course this will be a lot of work, would complicate the implementation and slow down the execution time. I still think it worth considering since it will significantly increase the confidence in the system. |
Alan-Jowett
force-pushed
the
verifier_fuzzing_support
branch
from
0d2ce9e to
a254702
Compare
There was a problem hiding this comment.
Actionable comments posted: 1
📜 Review details
Configuration used: CodeRabbit UI
Review profile: ASSERTIVE
Plan: Pro
📒 Files selected for processing (3)
src/crab/split_dbm.hpp(1 hunks)src/crab_verifier.cpp(1 hunks)src/crab_verifier.hpp(1 hunks)
⏰ Context from checks skipped due to timeout of 90000ms (9)
- GitHub Check: build_windows (Release, library)
- GitHub Check: build_windows (Release, tests)
- GitHub Check: build_ubuntu (Release, tests)
- GitHub Check: build_windows (Debug, library)
- GitHub Check: build_windows (Debug, tests)
- GitHub Check: build_ubuntu (Debug, tests)
- GitHub Check: build_ubuntu (Release)
- GitHub Check: build_ubuntu (Debug)
- GitHub Check: Analyze (cpp)
🔇 Additional comments (4)
src/crab_verifier.hpp (1)
61-61: Add documentation for is_valid_before method.Document the method's purpose, parameters, return value, and relationship to is_valid_after.
src/crab_verifier.cpp (2)
27-41: LGTM! Clear and comprehensive documentation.The comments effectively explain the validation logic and rationale for using intersection checks.
42-46: Verify the impact of switching from <= to intersection check.The change from <= to intersection check is logically sound based on the documentation.
✅ Verification successful
No other instances of similar validation patterns found
The change from <= to intersection check (&) is isolated to the
is_valid_aftermethod and doesn't require similar updates elsewhere in the codebase.🏁 Scripts executed
The following scripts were executed for the analysis:
Script:
#!/bin/bash # Description: Check for any existing uses of <= operator with invariants # that might need similar updates rg -A 2 "<=.*invariants"Length of output: 26
Script:
#!/bin/bash # Search for operator usage with invariants and related tests echo "=== Searching for invariants with operators ===" rg -l "invariants.*[<>=&|]" echo -e "\n=== Searching for test files related to invariants ===" fd -e cpp -e h "test.*invariant" echo -e "\n=== Checking for documentation ===" fd -e md -e txt | xargs rg -l "invariant"Length of output: 530
Script:
#!/bin/bash # Examine the actual operator usage with invariants echo "=== Checking operator usage context ===" rg -A 3 -B 3 "invariants.*[<>=&|]" echo -e "\n=== Checking README documentation ===" rg -A 3 -B 3 "invariant" README.mdLength of output: 7031
src/crab/split_dbm.hpp (1)
213-213: LGTM! Clear comment update.The comment clarifies why the parameter is anonymous.
| bool Invariants::is_valid_before(const label_t& label, const string_invariant& state) const { | ||
| const ebpf_domain_t abstract_state = | ||
| ebpf_domain_t::from_constraints(state.value(), thread_local_options.setup_constraints); | ||
| return !(abstract_state & invariants.at(label).pre).is_bottom(); |
There was a problem hiding this comment.
💡 Codebase verification
Add unit tests for is_valid_before method in src/test/test_verify.cpp
The method has no test coverage in the codebase. Add tests that verify:
- Valid states before a label
- Invalid states before a label
- Edge cases with bottom states
🔗 Analysis chain
Add unit tests for the new is_valid_before method.
The implementation is correct but needs test coverage.
🏁 Scripts executed
The following scripts were executed for the analysis:
Script:
#!/bin/bash
# Description: Check test coverage for is_valid_before
# Search for existing tests
rg "is_valid_before.*test" "test/"
# Look for test files that might contain relevant test cases
fd -t f "test_.*\.(cpp|hpp)" "test/"
Length of output: 210
Script:
#!/bin/bash
# Find all test-related files in the repository
fd -t f "test.*\.(cpp|hpp)$"
# Search for files containing "Invariants" and "test"
rg -l "class.*Invariants"
# Search for is_valid_before in all files
rg "is_valid_before"
Length of output: 474
Signed-off-by: Alan Jowett <alanjo@microsoft.com>
Alan-Jowett
force-pushed
the
verifier_fuzzing_support
branch
from
a5e702b to
647e9f8
Compare
There was a problem hiding this comment.
Actionable comments posted: 1
♻️ Duplicate comments (1)
src/crab_verifier.hpp (1)
61-61: 🧹 Nitpick (assertive)Add documentation for is_valid_before method.
Document what this method does, its parameters, return value, and how it relates to is_valid_after. Essential for understanding the validation logic.
+ /// Checks if the given state is valid before the specified label by comparing + /// against the pre-invariant. + /// @param label The program point to check + /// @param state The state to validate + /// @return true if state is valid, false if it violates constraints bool is_valid_before(const label_t& label, const string_invariant& state) const;
📜 Review details
Configuration used: CodeRabbit UI
Review profile: ASSERTIVE
Plan: Pro
📒 Files selected for processing (2)
src/crab_verifier.cpp(1 hunks)src/crab_verifier.hpp(1 hunks)
⏰ Context from checks skipped due to timeout of 90000ms (10)
- GitHub Check: build_ubuntu (Release, library)
- GitHub Check: build_windows (Release, tests)
- GitHub Check: build_windows (Debug, library)
- GitHub Check: build_ubuntu (Debug, tests)
- GitHub Check: build_ubuntu (Release, tests)
- GitHub Check: build_windows (Release, library)
- GitHub Check: build_windows (Debug, tests)
- GitHub Check: build_ubuntu (Release)
- GitHub Check: build_ubuntu (Debug)
- GitHub Check: Analyze (cpp)
🔇 Additional comments (2)
src/crab_verifier.cpp (2)
27-41: Comprehensive explanation of check outcomes.The detailed explanation clearly outlines the four possible outcomes and why the intersection-based approach is better than using
<=. This helps maintainers understand the constraints handling.
42-46:❓ Verification inconclusive
Method implementation looks sound.
The implementation correctly checks for constraint violations by testing whether the intersection with post-invariant is bottom.
I recommend adding a few unit tests to verify this change works as expected:
🏁 Script executed:
#!/bin/bash # Verify if there are any tests for is_valid_after with the new implementation rg -A 5 -B 5 "is_valid_(after)" "src/test/"Length of output: 43
Action required: Verify and add missing unit tests for
is_valid_after.
- The implementation in
src/crab_verifier.cpplooks correct as it properly checks for constraint violations via the post-invariant intersection.- However, the search in the
src/test/directory did not find any tests covering theis_valid_afterfunction.- Please add unit tests to exercise different constraint scenarios (e.g., when the intersection is bottom versus non-bottom) to ensure the invariant check behaves as expected.
| bool Invariants::is_valid_before(const label_t& label, const string_invariant& state) const { | ||
| const ebpf_domain_t abstract_state = | ||
| ebpf_domain_t::from_constraints(state.value(), thread_local_options.setup_constraints); | ||
| return !(abstract_state & invariants.at(label).pre).is_bottom(); | ||
| } |
There was a problem hiding this comment.
💡 Verification agent
🧩 Analysis chain
Good implementation of is_valid_before.
Implementation follows the same pattern as is_valid_after but correctly uses pre-invariants.
Add unit tests for this new method:
🏁 Script executed:
#!/bin/bash
# Check for existing tests for the new method
rg "is_valid_before" "src/test/"
# Find suitable test files where unit tests could be added
fd -t f "test_.*\.cpp" "src/test/"Length of output: 215
Action Required: Add Unit Tests for is_valid_before
- The implementation in
src/crab_verifier.cpp(lines 48-52) is correctly following the pattern fromis_valid_after, appropriately using pre-invariants. - Our search in the test suite confirmed there are no existing unit tests for
is_valid_before. - Please add unit tests for this method. Consider using one of the candidate test files (for example,
src/test/test_verify.cpp) to validate its behavior.
The uBPF fuzzer needs a version of the API that checks against the pre-conditions at the label instead of the post conditions.
Summary by CodeRabbit
New Features
Refactor