From c8616822b80bfd909f3ac4917ad6c690f0ba80e1 Mon Sep 17 00:00:00 2001 From: Alan Jowett Date: Thu, 16 Jan 2025 08:50:06 -0800 Subject: [PATCH] Add support for is_valid_before. Signed-off-by: Alan Jowett --- src/crab_verifier.cpp | 6 ++++++ src/crab_verifier.hpp | 1 + 2 files changed, 7 insertions(+) diff --git a/src/crab_verifier.cpp b/src/crab_verifier.cpp index b6b76964..87ca8ee3 100644 --- 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 index 06788d23..b949ec3e 100644 --- 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;