Exclude state variables without update functions in simple path check (…

…stanford-centaur#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

@@ -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

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<std::string, smt::Term> & 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

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);

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));

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)

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);