From 7cb3f0a804754ca4ba381a4f9d58cfc47963f924 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Mon, 6 Jan 2025 18:14:28 +0000
Subject: [PATCH] Engine heuristic: fix for assumptions unsupported by
 k-induction

The k-induction engine now correctly reports unsupported assumptions, and is
then skipped by the engine selection heuristic.

Fixes #921.
---
 regression/ebmc/engine-heuristic/basic1.desc  | 10 +++
 regression/ebmc/engine-heuristic/basic1.sv    |  8 ++
 regression/ebmc/engine-heuristic/basic2.desc  | 11 +++
 regression/ebmc/engine-heuristic/basic2.sv    | 15 ++++
 .../k-induction/k-induction-unsupported2.desc |  2 +-
 regression/ebmc/k-induction/k-induction6.desc |  7 +-
 regression/ebmc/k-induction/k-induction7.desc | 11 +++
 regression/ebmc/k-induction/k-induction7.sv   | 15 ++++
 src/ebmc/bdd_engine.cpp                       |  2 +-
 src/ebmc/ebmc_properties.cpp                  | 17 +++--
 src/ebmc/ebmc_properties.h                    | 73 ++++++++++++++++++-
 src/ebmc/k_induction.cpp                      | 36 ++++++++-
 src/ebmc/property_checker.cpp                 | 17 +++--
 src/ebmc/property_checker.h                   |  8 +-
 src/ebmc/report_results.cpp                   |  1 +
 src/trans-word-level/property.cpp             |  1 +
 16 files changed, 208 insertions(+), 26 deletions(-)
 create mode 100644 regression/ebmc/engine-heuristic/basic1.desc
 create mode 100644 regression/ebmc/engine-heuristic/basic1.sv
 create mode 100644 regression/ebmc/engine-heuristic/basic2.desc
 create mode 100644 regression/ebmc/engine-heuristic/basic2.sv
 create mode 100644 regression/ebmc/k-induction/k-induction7.desc
 create mode 100644 regression/ebmc/k-induction/k-induction7.sv

diff --git a/regression/ebmc/engine-heuristic/basic1.desc b/regression/ebmc/engine-heuristic/basic1.desc
new file mode 100644
index 000000000..6ca1327a4
--- /dev/null
+++ b/regression/ebmc/engine-heuristic/basic1.desc
@@ -0,0 +1,10 @@
+CORE
+basic1.sv
+
+^\[main\.a0\] always not s_eventually !main\.x: ASSUMED$
+^\[main\.p0\] always main\.x: PROVED up to bound 5$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc/engine-heuristic/basic1.sv b/regression/ebmc/engine-heuristic/basic1.sv
new file mode 100644
index 000000000..4c7ada49c
--- /dev/null
+++ b/regression/ebmc/engine-heuristic/basic1.sv
@@ -0,0 +1,8 @@
+module main(input clk, input x);
+
+  // not supported by k-induction
+  a0: assume property (not s_eventually !x);
+
+  p0: assert property (x);
+
+endmodule
diff --git a/regression/ebmc/engine-heuristic/basic2.desc b/regression/ebmc/engine-heuristic/basic2.desc
new file mode 100644
index 000000000..e8adb78c1
--- /dev/null
+++ b/regression/ebmc/engine-heuristic/basic2.desc
@@ -0,0 +1,11 @@
+CORE
+basic2.sv
+
+^\[main\.a0\] always not s_eventually !main\.y: UNSUPPORTED: unsupported by k-induction$
+^\[main\.a1\] always !main\.x: ASSUMED$
+^\[main\.p0\] always !main\.z: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc/engine-heuristic/basic2.sv b/regression/ebmc/engine-heuristic/basic2.sv
new file mode 100644
index 000000000..c48fbb156
--- /dev/null
+++ b/regression/ebmc/engine-heuristic/basic2.sv
@@ -0,0 +1,15 @@
+module main(input clk, input x, input y);
+
+  reg z = 0;
+  always_ff @(posedge clk) z <= z || x;
+
+  // unsupported assumption
+  a0: assume property (not s_eventually !y);
+
+  // supported assumption
+  a1: assume property (!x);
+
+  // inductive property
+  p0: assert property (!z);
+
+endmodule
diff --git a/regression/ebmc/k-induction/k-induction-unsupported2.desc b/regression/ebmc/k-induction/k-induction-unsupported2.desc
index 6f0045012..da7ac0bf6 100644
--- a/regression/ebmc/k-induction/k-induction-unsupported2.desc
+++ b/regression/ebmc/k-induction/k-induction-unsupported2.desc
@@ -3,7 +3,7 @@ k-induction-unsupported2.sv
 --module main --k-induction
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.p0\] always s_eventually main\.x == 10: FAILURE: property unsupported by k-induction$
+^\[main\.p0\] always s_eventually main\.x == 10: UNSUPPORTED: unsupported by k-induction$
 ^\[main\.p1\] always main\.x <= 10: PROVED$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/k-induction/k-induction6.desc b/regression/ebmc/k-induction/k-induction6.desc
index 7b106e616..76f743edd 100644
--- a/regression/ebmc/k-induction/k-induction6.desc
+++ b/regression/ebmc/k-induction/k-induction6.desc
@@ -1,9 +1,10 @@
-KNOWNBUG
+CORE
 k-induction6.sv
-
+--k-induction
+^\[main\.a0\] always not s_eventually !main\.x: UNSUPPORTED: unsupported by k-induction$
+^\[main\.p0\] always main\.x: INCONCLUSIVE$
 ^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-The property should hold, but is reported as refuted.
diff --git a/regression/ebmc/k-induction/k-induction7.desc b/regression/ebmc/k-induction/k-induction7.desc
new file mode 100644
index 000000000..b12da4946
--- /dev/null
+++ b/regression/ebmc/k-induction/k-induction7.desc
@@ -0,0 +1,11 @@
+CORE
+k-induction7.sv
+--k-induction
+^\[main\.a0\] always not s_eventually !main\.y: UNSUPPORTED: unsupported by k-induction$
+^\[main\.a1\] always !main\.x: ASSUMED$
+^\[main\.p0\] always !main\.z: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc/k-induction/k-induction7.sv b/regression/ebmc/k-induction/k-induction7.sv
new file mode 100644
index 000000000..c48fbb156
--- /dev/null
+++ b/regression/ebmc/k-induction/k-induction7.sv
@@ -0,0 +1,15 @@
+module main(input clk, input x, input y);
+
+  reg z = 0;
+  always_ff @(posedge clk) z <= z || x;
+
+  // unsupported assumption
+  a0: assume property (not s_eventually !y);
+
+  // supported assumption
+  a1: assume property (!x);
+
+  // inductive property
+  p0: assert property (!z);
+
+endmodule
diff --git a/src/ebmc/bdd_engine.cpp b/src/ebmc/bdd_engine.cpp
index b1c35d48e..bb51b4788 100644
--- a/src/ebmc/bdd_engine.cpp
+++ b/src/ebmc/bdd_engine.cpp
@@ -180,7 +180,7 @@ property_checker_resultt bdd_enginet::operator()()
   try
   {
     // any properties left?
-    if(!properties.has_unknown_property())
+    if(!properties.has_unfinished_property())
       return property_checker_resultt{properties};
 
     // possibly apply liveness-to-safety
diff --git a/src/ebmc/ebmc_properties.cpp b/src/ebmc/ebmc_properties.cpp
index daa0d07c8..e20983a78 100644
--- a/src/ebmc/ebmc_properties.cpp
+++ b/src/ebmc/ebmc_properties.cpp
@@ -18,6 +18,8 @@ Author: Daniel Kroening, dkr@amazon.com
 
 std::string ebmc_propertiest::propertyt::status_as_string() const
 {
+  auto suffix = failure_reason.has_value() ? ": " + failure_reason.value() : "";
+
   switch(status)
   {
   case statust::ASSUMED:
@@ -31,14 +33,15 @@ std::string ebmc_propertiest::propertyt::status_as_string() const
   case statust::REFUTED_WITH_BOUND:
     return "REFUTED up to bound " + std::to_string(bound);
   case statust::UNKNOWN:
-    return "UNKNOWN";
+    return "UNKNOWN" + suffix;
+  case statust::UNSUPPORTED:
+    return "UNSUPPORTED" + suffix;
   case statust::INCONCLUSIVE:
-    return "INCONCLUSIVE";
+    return "INCONCLUSIVE" + suffix;
   case statust::FAILURE:
-    return failure_reason.has_value() ? "FAILURE: " + failure_reason.value()
-                                      : "FAILURE";
+    return "FAILURE" + suffix;
   case statust::DROPPED:
-    return "DROPPED";
+    return "DROPPED" + suffix;
   case statust::DISABLED:
   default:
     UNREACHABLE;
@@ -78,9 +81,9 @@ ebmc_propertiest ebmc_propertiest::from_transition_system(
         id2string(symbol.location.get_comment());
 
       // Don't try to prove assumption properties.
-      if(symbol.value.id() == ID_sva_assume)
+      if(properties.properties.back().is_assumption())
       {
-        properties.properties.back().status = propertyt::statust::ASSUMED;
+        properties.properties.back().assumed();
         properties.properties.back().normalized_expr =
           normalize_property(to_sva_assume_expr(symbol.value).op());
       }
diff --git a/src/ebmc/ebmc_properties.h b/src/ebmc/ebmc_properties.h
index 8ebd1c861..4f777dd30 100644
--- a/src/ebmc/ebmc_properties.h
+++ b/src/ebmc/ebmc_properties.h
@@ -40,6 +40,7 @@ class ebmc_propertiest
       UNKNOWN,            // no work done yet
       DISABLED,           // turned off by user
       ASSUMED,            // property is assumed to be true, unbounded
+      UNSUPPORTED,        // property is unsupported
       PROVED,             // property is true, unbounded
       PROVED_WITH_BOUND,  // property is true, with bound
       REFUTED,            // property is false, possibly counterexample
@@ -98,24 +99,38 @@ class ebmc_propertiest
       return status == statust::FAILURE;
     }
 
+    bool is_unsupported() const
+    {
+      return status == statust::UNSUPPORTED;
+    }
+
     bool is_inconclusive() const
     {
       return status == statust::INCONCLUSIVE;
     }
 
+    void assumed()
+    {
+      status = statust::ASSUMED;
+      failure_reason = {};
+    }
+
     void unknown()
     {
       status = statust::UNKNOWN;
+      failure_reason = {};
     }
 
     void disable()
     {
       status = statust::DISABLED;
+      failure_reason = {};
     }
 
     void proved()
     {
       status = statust::PROVED;
+      failure_reason = {};
     }
 
     void proved_with_bound(std::size_t _bound)
@@ -127,17 +142,20 @@ class ebmc_propertiest
     void refuted()
     {
       status = statust::REFUTED;
+      failure_reason = {};
     }
 
     void refuted_with_bound(std::size_t _bound)
     {
       status = statust::REFUTED_WITH_BOUND;
       bound = _bound;
+      failure_reason = {};
     }
 
     void drop()
     {
       status = statust::DROPPED;
+      failure_reason = {};
     }
 
     void failure(const std::optional<std::string> &reason = {})
@@ -146,9 +164,16 @@ class ebmc_propertiest
       failure_reason = reason;
     }
 
+    void unsupported(const std::optional<std::string> &reason = {})
+    {
+      status = statust::UNSUPPORTED;
+      failure_reason = reason;
+    }
+
     void inconclusive()
     {
       status = statust::INCONCLUSIVE;
+      failure_reason = {};
     }
 
     std::string status_as_string() const;
@@ -164,16 +189,30 @@ class ebmc_propertiest
     {
       return ::is_exists_path(original_expr);
     }
+
+    bool is_assumption() const
+    {
+      return original_expr.id() == ID_sva_assume;
+    }
   };
 
   typedef std::list<propertyt> propertiest;
   propertiest properties;
 
-  bool has_unknown_property() const
+  bool has_unfinished_property() const
   {
     for(const auto &p : properties)
-      if(p.is_unknown())
+    {
+      if(p.is_assumption())
+      {
+      }
+      else if(
+        p.is_unknown() || p.is_unsupported() || p.is_failure() ||
+        p.is_inconclusive())
+      {
         return true;
+      }
+    }
 
     return false;
   }
@@ -209,12 +248,40 @@ class ebmc_propertiest
     return result;
   }
 
-  void reset_failure_to_unknown()
+  /// Resets properties/assumptions in FAILURE state to
+  /// ASSUMED/UNKNOWN respectively.
+  void reset_failure()
   {
     for(auto &p : properties)
       if(p.is_failure())
+      {
+        if(p.is_assumption())
+          p.assumed();
+        else
+          p.unknown();
+      }
+  }
+
+  /// Resets properties in INCONCLUSIVE state to UNKNOWN.
+  void reset_inconclusive()
+  {
+    for(auto &p : properties)
+      if(p.is_inconclusive())
         p.unknown();
   }
+
+  /// Resets properties in UNSUPPORTED state to UNKNOWN/ASSUMED.
+  void reset_unsupported()
+  {
+    for(auto &p : properties)
+      if(p.is_unsupported())
+      {
+        if(p.is_assumption())
+          p.assumed();
+        else
+          p.unknown();
+      }
+  }
 };
 
 #endif // CPROVER_EBMC_PROPERTIES_H
diff --git a/src/ebmc/k_induction.cpp b/src/ebmc/k_induction.cpp
index 9123617d4..123a6f818 100644
--- a/src/ebmc/k_induction.cpp
+++ b/src/ebmc/k_induction.cpp
@@ -170,16 +170,42 @@ Function: k_inductiont::operator()
 
 void k_inductiont::operator()()
 {
+  // Unsupported assumption? Mark as such.
+  bool assumption_unsupported = false;
+  for(auto &property : properties.properties)
+  {
+    if(!supported(property) && property.is_assumed())
+    {
+      assumption_unsupported = true;
+      property.unsupported("unsupported by k-induction");
+    }
+  }
+
   // Fail unsupported properties
   for(auto &property : properties.properties)
   {
-    if(!supported(property))
-      property.failure("property unsupported by k-induction");
+    if(
+      !supported(property) && !property.is_assumed() && !property.is_disabled())
+    {
+      property.unsupported("unsupported by k-induction");
+    }
   }
 
   // do induction base
   induction_base();
 
+  // Any refuted properties are really inconclusive if there are
+  // unsupported assumptions, as the assumption might have
+  // proven the property.
+  if(assumption_unsupported)
+  {
+    for(auto &property : properties.properties)
+    {
+      if(property.is_refuted())
+        property.unknown();
+    }
+  }
+
   // do induction step
   induction_step();
 }
@@ -231,8 +257,12 @@ void k_inductiont::induction_step()
 
   for(auto &p_it : properties.properties)
   {
-    if(p_it.is_disabled() || p_it.is_failure() || p_it.is_assumed())
+    if(
+      p_it.is_disabled() || p_it.is_failure() || p_it.is_assumed() ||
+      p_it.is_unsupported())
+    {
       continue;
+    }
 
     // If it's not failed, then it's supported.
     DATA_INVARIANT(supported(p_it), "property must be supported");
diff --git a/src/ebmc/property_checker.cpp b/src/ebmc/property_checker.cpp
index 39b5ee9cd..833392ad1 100644
--- a/src/ebmc/property_checker.cpp
+++ b/src/ebmc/property_checker.cpp
@@ -372,7 +372,7 @@ property_checker_resultt engine_heuristic(
 
   auto solver_factory = ebmc_solver_factory(cmdline);
 
-  if(!properties.has_unknown_property())
+  if(!properties.has_unfinished_property())
     return property_checker_resultt{properties}; // done
 
   message.status() << "No engine given, attempting heuristic engine selection"
@@ -384,12 +384,15 @@ property_checker_resultt engine_heuristic(
   k_induction(
     1, transition_system, properties, solver_factory, message_handler);
 
-  properties.reset_failure_to_unknown();
-
-  if(!properties.has_unknown_property())
+  if(!properties.has_unfinished_property())
     return property_checker_resultt{properties}; // done
 
+  properties.reset_failure();
+  properties.reset_inconclusive();
+  properties.reset_unsupported();
+
   // Now try BMC with bound 5, word-level
+  message.status() << "Attempting BMC with bound 5" << messaget::eom;
 
   bmc(
     5,     // bound
@@ -400,11 +403,11 @@ property_checker_resultt engine_heuristic(
     solver_factory,
     message_handler);
 
-  properties.reset_failure_to_unknown();
-
-  if(!properties.has_unknown_property())
+  if(!properties.has_unfinished_property())
     return property_checker_resultt{properties}; // done
 
+  properties.reset_failure();
+
   // Give up
   return property_checker_resultt{properties}; // done
 }
diff --git a/src/ebmc/property_checker.h b/src/ebmc/property_checker.h
index d1fe7f008..bd59e6b88 100644
--- a/src/ebmc/property_checker.h
+++ b/src/ebmc/property_checker.h
@@ -50,12 +50,18 @@ class property_checker_resultt
   bool all_properties_proved() const
   {
     for(const auto &p : properties)
-      if(
+    {
+      if(p.is_assumption())
+      {
+        // ignore
+      }
+      else if(
         !p.is_proved() && !p.is_proved_with_bound() && !p.is_disabled() &&
         !p.is_assumed())
       {
         return false;
       }
+    }
 
     return true;
   }
diff --git a/src/ebmc/report_results.cpp b/src/ebmc/report_results.cpp
index 88523d15a..6469c0d9a 100644
--- a/src/ebmc/report_results.cpp
+++ b/src/ebmc/report_results.cpp
@@ -111,6 +111,7 @@ void report_results(
       case statust::DROPPED: message.status() << messaget::red; break;
       case statust::FAILURE: message.status() << messaget::red; break;
       case statust::UNKNOWN: message.status() << messaget::yellow; break;
+      case statust::UNSUPPORTED: message.status() << messaget::yellow; break;
       case statust::DISABLED: break;
       case statust::INCONCLUSIVE: message.status() << messaget::yellow; break;
       }
diff --git a/src/trans-word-level/property.cpp b/src/trans-word-level/property.cpp
index 1a44dca7c..70acd2fb2 100644
--- a/src/trans-word-level/property.cpp
+++ b/src/trans-word-level/property.cpp
@@ -696,6 +696,7 @@ void property(
   auto obligations = property_obligations(property_expr, no_timeframes);
 
   // Map obligations onto timeframes.
+  prop_handles.clear();
   prop_handles.resize(no_timeframes, true_exprt());
   for(auto &obligation_it : obligations.map)
   {