From f4583dbeee24f6e1ef63e466a053d8f6b2b34b1e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C3=81ron=20Ricardo=20Perez-Lopez?= Date: Wed, 21 Aug 2024 18:10:09 -0400 Subject: [PATCH] Exclude state variables without update functions in simple path check (#341) If there are state variables that are, e.g., used in the property, but do not have an update function, the simple path check in k-induction and BMC will never succeed. This is because we can always pick an arbitrary (new) value for this variable and thus construct a "new" state, even if, in reality, we are in a loop. Such variables should in reality be inputs. However, such a transformation is not completely straightforward, as they could still have an initial value. For now, as a simple solution, we simply exclude them from the simple path checks. * Add method to get set of states without update functions * Exclude states without update functions from simple path checking * Construct set of non-updated statevars on the fly * Update transition system test * Update engine tests * Update Btor2 TS copy test --- core/ts.cpp | 13 +++++++++++++ core/ts.h | 9 +++++++++ engines/kinduction.cpp | 6 ++++++ tests/encoders/test_btor2_ts_copy_equal.cpp | 8 ++++++++ tests/test_engines.cpp | 8 ++++---- tests/test_ts.cpp | 7 +++++++ 6 files changed, 47 insertions(+), 4 deletions(-) diff --git a/core/ts.cpp b/core/ts.cpp index 040337cac..ca5ef33c4 100644 --- a/core/ts.cpp +++ b/core/ts.cpp @@ -38,6 +38,7 @@ void swap(TransitionSystem & ts1, TransitionSystem & ts2) std::swap(ts1.named_terms_, ts2.named_terms_); std::swap(ts1.term_to_name_, ts2.term_to_name_); std::swap(ts1.state_updates_, ts2.state_updates_); + std::swap(ts1.no_state_updates_, ts2.no_state_updates_); std::swap(ts1.next_map_, ts2.next_map_); std::swap(ts1.curr_map_, ts2.curr_map_); std::swap(ts1.functional_, ts2.functional_); @@ -88,6 +89,10 @@ TransitionSystem::TransitionSystem(const TransitionSystem & other_ts, next_statevars_.insert(transfer(v)); } + for (const auto & v : other_ts.no_state_updates_) { + no_state_updates_.insert(transfer(v)); + } + for (const auto & elem : other_ts.named_terms_) { named_terms_[elem.first] = transfer(elem.second); } @@ -138,6 +143,7 @@ bool TransitionSystem::operator==(const TransitionSystem & other) const named_terms_ == other.named_terms_ && term_to_name_ == other.term_to_name_ && state_updates_ == other.state_updates_ && + no_state_updates_ == other.no_state_updates_ && next_map_ == other.next_map_ && curr_map_ == other.curr_map_ && functional_ == other.functional_ && @@ -190,6 +196,8 @@ void TransitionSystem::assign_next(const Term & state, const Term & val) } state_updates_[state] = val; + auto erased = no_state_updates_.erase(state); + assert(erased); trans_ = solver_->make_term( And, trans_, solver_->make_term(Equal, next_map_.at(state), val)); @@ -372,6 +380,7 @@ void TransitionSystem::add_statevar(const Term & cv, const Term & nv) } statevars_.insert(cv); + no_state_updates_.insert(cv); next_statevars_.insert(nv); next_map_[cv] = nv; curr_map_[nv] = cv; @@ -528,11 +537,14 @@ void TransitionSystem::rebuild_trans_based_on_coi( } smt::UnorderedTermMap reduced_state_updates; + no_state_updates_.clear(); for (const auto & var : state_vars_in_coi) { const auto & elem = state_updates_.find(var); if (elem != state_updates_.end()) { Term next_func = elem->second; reduced_state_updates[var] = next_func; + } else { + no_state_updates_.insert(var); } } state_updates_ = reduced_state_updates; @@ -635,6 +647,7 @@ void TransitionSystem::drop_state_updates(const TermVec & svs) throw PonoException("Got non-state var in drop_state_updates"); } state_updates_.erase(sv); + no_state_updates_.insert(sv); } // now rebuild trans diff --git a/core/ts.h b/core/ts.h index b34a26b9f..d37131bd1 100644 --- a/core/ts.h +++ b/core/ts.h @@ -252,6 +252,12 @@ class TransitionSystem return state_updates_; }; + /* Returns the set of state variables with no update function. */ + const smt::UnorderedTermSet & statevars_with_no_update() const + { + return no_state_updates_; + }; + /* @return the named terms mapping */ const std::unordered_map & named_terms() const { @@ -506,6 +512,9 @@ class TransitionSystem // next state update function smt::UnorderedTermMap state_updates_; + // states with no next state update function + smt::UnorderedTermSet no_state_updates_; + // maps states and inputs variables to next versions // note: the next state variables are only used // on the left hand side of equalities in diff --git a/engines/kinduction.cpp b/engines/kinduction.cpp index e401e46f3..8e73a7753 100644 --- a/engines/kinduction.cpp +++ b/engines/kinduction.cpp @@ -265,7 +265,13 @@ Term KInduction::simple_path_constraint(int i, int j) assert(ts_.statevars().size()); Term disj = false_; + const auto no_next_states = ts_.statevars_with_no_update(); for (const auto &v : ts_.statevars()) { + // Skip states without updates, because those cause spurious transitions. + // k=0 is excluded as they could still have initial values. + if (i > 0 && j > 0 && no_next_states.find(v) != no_next_states.end()) { + continue; + } Term vi = unroller_.at_time(v, i); Term vj = unroller_.at_time(v, j); Term eq = solver_->make_term(PrimOp::Equal, vi, vj); diff --git a/tests/encoders/test_btor2_ts_copy_equal.cpp b/tests/encoders/test_btor2_ts_copy_equal.cpp index f9a0b1c45..1a6c8a305 100644 --- a/tests/encoders/test_btor2_ts_copy_equal.cpp +++ b/tests/encoders/test_btor2_ts_copy_equal.cpp @@ -46,6 +46,8 @@ TEST_P(CopyUnitTests, CopyFromDefault) FunctionalTransitionSystem fts_copy(fts, tt); EXPECT_EQ(fts.statevars().size(), fts_copy.statevars().size()); + EXPECT_EQ(fts.statevars_with_no_update().size(), + fts_copy.statevars_with_no_update().size()); EXPECT_EQ(fts.inputvars().size(), fts_copy.inputvars().size()); EXPECT_EQ(fts.named_terms().size(), fts_copy.named_terms().size()); EXPECT_EQ(fts.state_updates().size(), fts_copy.state_updates().size()); @@ -124,6 +126,8 @@ TEST_P(CopyUnitTests, CopyToDefault) fts_copy = FunctionalTransitionSystem(fts, tt); EXPECT_EQ(fts.statevars().size(), fts_copy.statevars().size()); + EXPECT_EQ(fts.statevars_with_no_update().size(), + fts_copy.statevars_with_no_update().size()); EXPECT_EQ(fts.inputvars().size(), fts_copy.inputvars().size()); EXPECT_EQ(fts.named_terms().size(), fts_copy.named_terms().size()); EXPECT_EQ(fts.state_updates().size(), fts_copy.state_updates().size()); @@ -150,6 +154,10 @@ TEST_P(CopyUnitTests, CopyToDefault) for (auto v : fts.inputvars()) { EXPECT_TRUE(fts_2.inputvars().find(v) != fts_2.inputvars().end()); } + for (auto v : fts.statevars_with_no_update()) { + EXPECT_TRUE(fts_2.statevars_with_no_update().find(v) + != fts_2.statevars_with_no_update().end()); + } for (auto v : fts.statevars()) { EXPECT_TRUE(fts_2.statevars().find(v) != fts_2.statevars().end()); EXPECT_TRUE(fts.next(v) == fts_2.next(v)); diff --git a/tests/test_engines.cpp b/tests/test_engines.cpp index b9709ad9e..70a53e6e0 100644 --- a/tests/test_engines.cpp +++ b/tests/test_engines.cpp @@ -221,18 +221,18 @@ TEST_P(InterpWinTests, BmcFail) ASSERT_EQ(r, ProverResult::UNKNOWN); } -TEST_P(InterpWinTests, BmcSimplePathFail) +TEST_P(InterpWinTests, BmcSimplePathWin) { BmcSimplePath bsp(*true_p, *ts, s); ProverResult r = bsp.check_until(10); - ASSERT_EQ(r, ProverResult::UNKNOWN); + ASSERT_EQ(r, ProverResult::TRUE); } -TEST_P(InterpWinTests, KInductionFail) +TEST_P(InterpWinTests, KInductionWin) { KInduction kind(*true_p, *ts, s); ProverResult r = kind.check_until(10); - ASSERT_EQ(r, ProverResult::UNKNOWN); + ASSERT_EQ(r, ProverResult::TRUE); } TEST_P(InterpWinTests, InterpWin) diff --git a/tests/test_ts.cpp b/tests/test_ts.cpp index 0909c8143..e7762c062 100644 --- a/tests/test_ts.cpp +++ b/tests/test_ts.cpp @@ -38,10 +38,12 @@ TEST_P(TSUnitTests, FTS_IsFunc) Term x = fts.make_statevar("x", bvsort); EXPECT_FALSE(fts.is_deterministic()); EXPECT_TRUE(fts.is_functional()); + EXPECT_EQ(fts.statevars_with_no_update(), UnorderedTermSet({x})); fts.assign_next(x, s->make_term(BVAdd, x, s->make_term(1, bvsort))); EXPECT_TRUE(fts.is_functional()); EXPECT_TRUE(fts.is_deterministic()); + EXPECT_EQ(fts.statevars_with_no_update().size(), 0); fts.add_constraint(fts.make_term(BVUge, x, s->make_term(2, bvsort))); // any kind of constrains makes the system non-deterministic @@ -53,10 +55,15 @@ TEST_P(TSUnitTests, FTS_IsFunc) EXPECT_TRUE(fts.is_functional()); // still can't be deterministic because of the constraint EXPECT_FALSE(fts.is_deterministic()); + EXPECT_EQ(fts.statevars_with_no_update().size(), 0); + + Term z = fts.make_statevar("z", bvsort); + EXPECT_EQ(fts.statevars_with_no_update(), UnorderedTermSet({z})); TransitionSystem ts_copy = fts; EXPECT_EQ(fts.is_functional(), ts_copy.is_functional()); EXPECT_EQ(fts.is_deterministic(), ts_copy.is_deterministic()); + EXPECT_EQ(fts.statevars_with_no_update(), ts_copy.statevars_with_no_update()); EXPECT_EQ(ts_copy, fts); ts_copy.set_init(ts_copy.make_term(Equal, x, ts_copy.make_term(1, bvsort))); EXPECT_NE(ts_copy, fts);