Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add support for is_valid_before #825

Open
wants to merge 3 commits into
base: main
Choose a base branch
from
Open

Add support for is_valid_before #825

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
c48889c
Add support for is_valid_before.
Alan-Jowett Jan 16, 2025
b3b36e1
Switch to intersection of the two states
Alan-Jowett Jan 21, 2025
0d2ce9e
Remove unused parameter warning
Alan-Jowett Jan 21, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions src/crab/split_dbm.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -209,8 +209,8 @@ class SplitDBM final {
SplitDBM widen(const SplitDBM& o) const;

[[nodiscard]]
SplitDBM widening_thresholds(const SplitDBM& o, const iterators::thresholds_t& ts) const {
// TODO: use thresholds
SplitDBM widening_thresholds(const SplitDBM& o, const iterators::thresholds_t&) const {
// TODO: use thresholds. For now, make thresholds an anonymous argument to avoid unused parameter warning.
return this->widen(o);
elazarg marked this conversation as resolved.
Show resolved Hide resolved
}

Expand Down
23 changes: 22 additions & 1 deletion src/crab_verifier.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,10 +24,31 @@ thread_local crab::lazy_allocator<program_info> thread_local_program_info;
thread_local ebpf_verifier_options_t thread_local_options;
void ebpf_verifier_clear_before_analysis();

// Note:
// The check is intended to find abstract state values that violate the constraints of the
// pre or post invariant. The check is done by the crab library.
// There are 4 possible outcomes:
// 1. The abstract state contains an invariant that is not present in the pre or post invariant.
// 2. The pre or post invariant contains an invariant that is not present in the abstract state.
// 3. The abstract state contains an invariant that is present in the pre or post invariant and
// the value of the invariant is within the constraints of the pre or post invariant.
// 4. The abstract state contains an invariant that is present in the pre or post invariant, but the
// value of the invariant is not within the constraints of the pre or post invariant.
// The check should return false only for the 4th case where there is a violation of the constraints.
// Usage of <= doesn't work as there are cases where the externally provided state contains constraints
// that the pre and post invariant doesn't have. Examples are the registers where the pre and post invariant
// have 'havoc'ed the constraints, but the externally provided state has constraints on the registers.

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();
}
Comment on lines 42 to +46
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🧹 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.

Suggested change
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();
Comment on lines +48 to +51
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🧹 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.

Suggested change
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();
}

Comment on lines 42 to +51
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 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

}

string_invariant Invariants::invariant_at(const label_t& label) const { return invariants.at(label).post.to_set(); }
Expand Down
1 change: 1 addition & 0 deletions src/crab_verifier.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🧹 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.

Suggested change
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;


string_invariant invariant_at(const label_t& label) const;

Expand Down
Loading