Add support for is_valid_before #825
Conversation
WalkthroughThe pull request introduces a new method 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. |
Signed-off-by: Alan Jowett <[email protected]>
Signed-off-by: Alan Jowett <[email protected]>
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_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.
🧹 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_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 false only if abstract_state violates pre-invariant constraints
return !(abstract_state & invariants.at(label).pre).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_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(); | |
| 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 false only if abstract_state violates pre-invariant constraints | |
| return !(abstract_state & invariants.at(label).pre).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
Signed-off-by: Alan Jowett <[email protected]>
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. |
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