Add support for is_valid_before.

Signed-off-by: Alan Jowett <[email protected]>
vbpf · Jan 16, 2025 · c861682 · c861682
1 parent c752a2e
commit c861682
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 0 deletions.
diff --git a/src/crab_verifier.cpp b/src/crab_verifier.cpp
@@ -30,6 +30,12 @@ bool Invariants::is_valid_after(const label_t& label, const string_invariant& st
     return abstract_state <= invariants.at(label).post;
 }
 
+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;
+}
+
 string_invariant Invariants::invariant_at(const label_t& label) const { return invariants.at(label).post.to_set(); }
 
 crab::interval_t Invariants::exit_value() const { return invariants.at(label_t::exit).post.get_r0(); }

diff --git a/src/crab_verifier.hpp b/src/crab_verifier.hpp
@@ -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;
 
     string_invariant invariant_at(const label_t& label) const;