Implement SVA cover in BMC

kroening · kroening · commit 4c3a4dbfbf47 · 2024-04-14T18:08:34.000-07:00
This adds support for SVA cover properties to the BMC engine.
diff --git a/regression/verilog/SVA/cover1.desc b/regression/verilog/SVA/cover1.desc
@@ -1,8 +1,10 @@
 KNOWNBUG
 cover1.sv
---bound 10
-^\[main\.property\.p0\] cover main\.counter == 1: REFUTED$
-^\[main\.property\.p1\] cover main\.counter == 100: REFUTED$
+--bound 10 --numbered-trace
+^\[main\.property\.p0\] cover main\.counter == 1: PROVED$
+^main\.counter@0 = 0$
+^main\.counter@1 = 1$
+^\[main\.property\.p1\] cover main\.counter == 100: REFUTED up to bound 20$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/src/ebmc/bdd_engine.cpp b/src/ebmc/bdd_engine.cpp
@@ -402,7 +402,7 @@ void bdd_enginet::compute_counterexample(
     throw "unexpected result from SAT solver";
   }
 
-  property.counterexample =
+  property.witness_trace =
     compute_trans_trace(property.timeframe_literals, bmc_map, solver, ns);
 }
 
diff --git a/src/ebmc/bmc.cpp b/src/ebmc/bmc.cpp
@@ -98,38 +98,77 @@ void bmc(
 
       message.status() << "Checking " << property.name << messaget::eom;
 
-      auto assumption = not_exprt(conjunction(property.timeframe_handles));
-
-      decision_proceduret::resultt dec_result = solver(assumption);
-
-      switch(dec_result)
+      if(property.is_exists_path())
+      {
+        auto assumption = disjunction(property.timeframe_handles);
+
+        decision_proceduret::resultt dec_result = solver(assumption);
+
+        switch(dec_result)
+        {
+        case decision_proceduret::resultt::D_SATISFIABLE:
+          property.proved();
+          message.result() << "SAT: path found" << messaget::eom;
+
+          property.witness_trace = compute_trans_trace(
+            property.timeframe_handles,
+            solver,
+            bound + 1,
+            ns,
+            transition_system.main_symbol->name);
+          break;
+
+        case decision_proceduret::resultt::D_UNSATISFIABLE:
+          message.result() << "UNSAT: No path found within bound"
+                           << messaget::eom;
+          property.refuted_with_bound(bound);
+          break;
+
+        case decision_proceduret::resultt::D_ERROR:
+          message.error() << "Error from decision procedure" << messaget::eom;
+          property.failure();
+          break;
+
+        default:
+          property.failure();
+          throw ebmc_errort() << "Unexpected result from decision procedure";
+        }
+      }
+      else // universal path property
       {
-      case decision_proceduret::resultt::D_SATISFIABLE:
-        property.refuted();
-        message.result() << "SAT: counterexample found" << messaget::eom;
-
-        property.counterexample = compute_trans_trace(
-          property.timeframe_handles,
-          solver,
-          bound + 1,
-          ns,
-          transition_system.main_symbol->name);
-        break;
-
-      case decision_proceduret::resultt::D_UNSATISFIABLE:
-        message.result() << "UNSAT: No counterexample found within bound"
-                         << messaget::eom;
-        property.proved_with_bound(bound);
-        break;
-
-      case decision_proceduret::resultt::D_ERROR:
-        message.error() << "Error from decision procedure" << messaget::eom;
-        property.failure();
-        break;
-
-      default:
-        property.failure();
-        throw ebmc_errort() << "Unexpected result from decision procedure";
+        auto assumption = not_exprt{conjunction(property.timeframe_handles)};
+
+        decision_proceduret::resultt dec_result = solver(assumption);
+
+        switch(dec_result)
+        {
+        case decision_proceduret::resultt::D_SATISFIABLE:
+          property.refuted();
+          message.result() << "SAT: counterexample found" << messaget::eom;
+
+          property.witness_trace = compute_trans_trace(
+            property.timeframe_handles,
+            solver,
+            bound + 1,
+            ns,
+            transition_system.main_symbol->name);
+          break;
+
+        case decision_proceduret::resultt::D_UNSATISFIABLE:
+          message.result() << "UNSAT: No counterexample found within bound"
+                           << messaget::eom;
+          property.proved_with_bound(bound);
+          break;
+
+        case decision_proceduret::resultt::D_ERROR:
+          message.error() << "Error from decision procedure" << messaget::eom;
+          property.failure();
+          break;
+
+        default:
+          property.failure();
+          throw ebmc_errort() << "Unexpected result from decision procedure";
+        }
       }
     }
 
diff --git a/src/ebmc/ebmc_base.cpp b/src/ebmc/ebmc_base.cpp
@@ -95,7 +95,7 @@ int ebmc_baset::finish_bit_level_bmc(const bmc_mapt &bmc_map, propt &solver)
 
         namespacet ns(transition_system.symbol_table);
 
-        property.counterexample =
+        property.witness_trace =
           compute_trans_trace(property.timeframe_literals, bmc_map, solver, ns);
       }
       break;
diff --git a/src/ebmc/ebmc_properties.cpp b/src/ebmc/ebmc_properties.cpp
@@ -26,6 +26,8 @@ std::string ebmc_propertiest::propertyt::status_as_string() const
     return "PROVED up to bound " + std::to_string(bound);
   case statust::REFUTED:
     return "REFUTED";
+  case statust::REFUTED_WITH_BOUND:
+    return "REFUTED up to bound " + std::to_string(bound);
   case statust::UNKNOWN:
     return "UNKNOWN";
   case statust::INCONCLUSIVE:
diff --git a/src/ebmc/ebmc_properties.h b/src/ebmc/ebmc_properties.h
@@ -15,6 +15,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <solvers/prop/literal.h>
 #include <trans-netlist/trans_trace.h>
 #include <trans-word-level/property.h>
+#include <temporal-logic/temporal_logic.h>
 
 #include "transition_system.h"
 
@@ -42,18 +43,19 @@ class ebmc_propertiest
       PROVED,            // property is true, unbounded
       PROVED_WITH_BOUND, // property is true, with bound
       REFUTED,           // property is false, possibly counterexample
+      REFUTED_WITH_BOUND,// property is false, with bound
       DROPPED,           // given up
       FAILURE,           // error during anaysis
       INCONCLUSIVE       // analysis can't determine truth
     } status = statust::UNKNOWN;
 
     std::size_t bound = 0;
-    std::optional<trans_tracet> counterexample;
+    std::optional<trans_tracet> witness_trace;
     std::optional<std::string> failure_reason;
 
-    bool has_counterexample() const
+    bool has_witness_trace() const
     {
-      return counterexample.has_value();
+      return witness_trace.has_value();
     }
 
     bool is_unknown() const
@@ -122,6 +124,12 @@ class ebmc_propertiest
       status = statust::REFUTED;
     }
 
+    void refuted_with_bound(std::size_t _bound)
+    {
+      status = statust::REFUTED_WITH_BOUND;
+      bound = _bound;
+    }
+
     void drop()
     {
       status = statust::DROPPED;
@@ -146,6 +154,11 @@ class ebmc_propertiest
     {
       return ::requires_lasso_constraints(normalized_expr);
     }
+
+    bool is_exists_path() const
+    {
+      return ::is_exists_path(original_expr);
+    }
   };
 
   typedef std::list<propertyt> propertiest;
diff --git a/src/ebmc/report_results.cpp b/src/ebmc/report_results.cpp
@@ -58,9 +58,9 @@ void report_results(
       json_property["identifier"] = json_stringt(id2string(property.name));
       json_property["status"] = json_stringt(property.status_as_string());
 
-      if(property.has_counterexample())
-        json_property["counterexample"] =
-          json(property.counterexample.value(), ns);
+      if(property.has_witness_trace())
+        json_property["trace"] =
+          json(property.witness_trace.value(), ns);
 
       json_properties.push_back(std::move(json_property));
     }
@@ -81,8 +81,8 @@ void report_results(
       xml_result.set_attribute("property", id2string(property.name));
       xml_result.set_attribute("status", property.status_as_string());
 
-      if(property.has_counterexample())
-        xml_result.new_element() = xml(property.counterexample.value(), ns);
+      if(property.has_witness_trace())
+        xml_result.new_element() = xml(property.witness_trace.value(), ns);
 
       std::cout << xml_result << '\n' << std::flush;
     }
@@ -109,6 +109,7 @@ void report_results(
       case statust::PROVED: message.status() << messaget::green; break;
       case statust::PROVED_WITH_BOUND: message.status() << messaget::green; break;
       case statust::REFUTED: message.status() << messaget::bright_red; break;
+      case statust::REFUTED_WITH_BOUND: message.status() << messaget::bright_red; break;
       case statust::DROPPED: message.status() << messaget::red; break;
       case statust::FAILURE: message.status() << messaget::red; break;
       case statust::UNKNOWN: message.status() << messaget::yellow; break;
@@ -121,24 +122,28 @@ void report_results(
 
       message.status() << messaget::reset << messaget::eom;
 
-      if(property.has_counterexample())
+      if(property.has_witness_trace())
       {
+        auto term = [&property]() {
+          return property.is_exists_path() ? "Trace" : "Counterexample";
+        };
+
         if(cmdline.isset("trace"))
         {
-          message.status() << "Counterexample:\n" << messaget::eom;
+          message.status() << term() << ":\n" << messaget::eom;
           show_trans_trace(
-            property.counterexample.value(), message, ns, std::cout);
+            property.witness_trace.value(), message, ns, std::cout);
         }
         else if(cmdline.isset("numbered-trace"))
         {
-          message.status() << "Counterexample:\n" << messaget::eom;
+          message.status() << term() << ":" << messaget::eom;
           show_trans_trace_numbered(
-            property.counterexample.value(), message, ns, std::cout);
+            property.witness_trace.value(), message, ns, std::cout);
         }
         else if(cmdline.isset("waveform"))
         {
-          message.status() << "Counterexample:" << messaget::eom;
-          show_waveform(property.counterexample.value(), ns);
+          message.status() << term() << ":" << messaget::eom;
+          show_waveform(property.witness_trace.value(), ns);
         }
       }
     }
@@ -148,13 +153,13 @@ void report_results(
   {
     for(const auto &property : properties.properties)
     {
-      if(property.has_counterexample())
+      if(property.has_witness_trace())
       {
         std::string vcdfile = cmdline.get_value("vcd");
         std::ofstream vcd(widen_if_needed(vcdfile));
 
         messaget message(message_handler);
-        show_trans_trace_vcd(property.counterexample.value(), message, ns, vcd);
+        show_trans_trace_vcd(property.witness_trace.value(), message, ns, vcd);
 
         break;
       }
diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp
@@ -36,3 +36,8 @@ bool has_temporal_operator(const exprt &expr)
 
   return false;
 }
+
+bool is_exists_path(const exprt &expr)
+{
+  return expr.id() == ID_sva_cover;
+}
diff --git a/src/temporal-logic/temporal_logic.h b/src/temporal-logic/temporal_logic.h
@@ -18,4 +18,8 @@ bool has_temporal_operator(const exprt &);
 /// as its root
 bool is_temporal_operator(const exprt &);
 
+/// Returns true iff the given expression is an existential path
+/// property.
+bool is_exists_path(const exprt &);
+
 #endif

Original file line number	Diff line number	Diff line change
`@@ -402,7 +402,7 @@ void bdd_enginet::compute_counterexample(`
`402`	`402`	`throw "unexpected result from SAT solver";`
`403`	`403`	`}`
`404`	`404`
`405`		`- property.counterexample =`
	`405`	`+ property.witness_trace =`
`406`	`406`	`compute_trans_trace(property.timeframe_literals, bmc_map, solver, ns);`
`407`	`407`	`}`
`408`	`408`
Original file line number	Diff line number	Diff line change
`@@ -95,7 +95,7 @@ int ebmc_baset::finish_bit_level_bmc(const bmc_mapt &bmc_map, propt &solver)`
`95`	`95`
`96`	`96`	`namespacet ns(transition_system.symbol_table);`
`97`	`97`
`98`		`- property.counterexample =`
	`98`	`+ property.witness_trace =`
`99`	`99`	`compute_trans_trace(property.timeframe_literals, bmc_map, solver, ns);`
`100`	`100`	`}`
`101`	`101`	`break;`
Original file line number	Diff line number	Diff line change
`@@ -58,9 +58,9 @@ void report_results(`
`58`	`58`	`json_property["identifier"] = json_stringt(id2string(property.name));`
`59`	`59`	`json_property["status"] = json_stringt(property.status_as_string());`
`60`	`60`
`61`		`- if(property.has_counterexample())`
`62`		`- json_property["counterexample"] =`
`63`		`- json(property.counterexample.value(), ns);`
	`61`	`+ if(property.has_witness_trace())`
	`62`	`+ json_property["trace"] =`
	`63`	`+ json(property.witness_trace.value(), ns);`
`64`	`64`
`65`	`65`	`json_properties.push_back(std::move(json_property));`
`66`	`66`	`}`
`@@ -81,8 +81,8 @@ void report_results(`
`81`	`81`	`xml_result.set_attribute("property", id2string(property.name));`
`82`	`82`	`xml_result.set_attribute("status", property.status_as_string());`
`83`	`83`
`84`		`- if(property.has_counterexample())`
`85`		`- xml_result.new_element() = xml(property.counterexample.value(), ns);`
	`84`	`+ if(property.has_witness_trace())`
	`85`	`+ xml_result.new_element() = xml(property.witness_trace.value(), ns);`
`86`	`86`
`87`	`87`	`std::cout << xml_result << '\n' << std::flush;`
`88`	`88`	`}`
`@@ -109,6 +109,7 @@ void report_results(`
`109`	`109`	`case statust::PROVED: message.status() << messaget::green; break;`
`110`	`110`	`case statust::PROVED_WITH_BOUND: message.status() << messaget::green; break;`
`111`	`111`	`case statust::REFUTED: message.status() << messaget::bright_red; break;`
	`112`	`+ case statust::REFUTED_WITH_BOUND: message.status() << messaget::bright_red; break;`
`112`	`113`	`case statust::DROPPED: message.status() << messaget::red; break;`
`113`	`114`	`case statust::FAILURE: message.status() << messaget::red; break;`
`114`	`115`	`case statust::UNKNOWN: message.status() << messaget::yellow; break;`
`@@ -121,24 +122,28 @@ void report_results(`
`121`	`122`
`122`	`123`	`message.status() << messaget::reset << messaget::eom;`
`123`	`124`
`124`		`- if(property.has_counterexample())`
	`125`	`+ if(property.has_witness_trace())`
`125`	`126`	`{`
	`127`	`+ auto term = [&property]() {`
	`128`	`+ return property.is_exists_path() ? "Trace" : "Counterexample";`
	`129`	`+ };`
	`130`	`+`
`126`	`131`	`if(cmdline.isset("trace"))`
`127`	`132`	`{`
`128`		`- message.status() << "Counterexample:\n" << messaget::eom;`
	`133`	`+ message.status() << term() << ":\n" << messaget::eom;`
`129`	`134`	`show_trans_trace(`
`130`		`- property.counterexample.value(), message, ns, std::cout);`
	`135`	`+ property.witness_trace.value(), message, ns, std::cout);`
`131`	`136`	`}`
`132`	`137`	`else if(cmdline.isset("numbered-trace"))`
`133`	`138`	`{`
`134`		`- message.status() << "Counterexample:\n" << messaget::eom;`
	`139`	`+ message.status() << term() << ":" << messaget::eom;`
`135`	`140`	`show_trans_trace_numbered(`
`136`		`- property.counterexample.value(), message, ns, std::cout);`
	`141`	`+ property.witness_trace.value(), message, ns, std::cout);`
`137`	`142`	`}`
`138`	`143`	`else if(cmdline.isset("waveform"))`
`139`	`144`	`{`
`140`		`- message.status() << "Counterexample:" << messaget::eom;`
`141`		`- show_waveform(property.counterexample.value(), ns);`
	`145`	`+ message.status() << term() << ":" << messaget::eom;`
	`146`	`+ show_waveform(property.witness_trace.value(), ns);`
`142`	`147`	`}`
`143`	`148`	`}`
`144`	`149`	`}`
`@@ -148,13 +153,13 @@ void report_results(`
`148`	`153`	`{`
`149`	`154`	`for(const auto &property : properties.properties)`
`150`	`155`	`{`
`151`		`- if(property.has_counterexample())`
	`156`	`+ if(property.has_witness_trace())`
`152`	`157`	`{`
`153`	`158`	`std::string vcdfile = cmdline.get_value("vcd");`
`154`	`159`	`std::ofstream vcd(widen_if_needed(vcdfile));`
`155`	`160`
`156`	`161`	`messaget message(message_handler);`
`157`		`- show_trans_trace_vcd(property.counterexample.value(), message, ns, vcd);`
	`162`	`+ show_trans_trace_vcd(property.witness_trace.value(), message, ns, vcd);`
`158`	`163`
`159`	`164`	`break;`
`160`	`165`	`}`
Original file line number	Diff line number	Diff line change
`@@ -36,3 +36,8 @@ bool has_temporal_operator(const exprt &expr)`
`36`	`36`
`37`	`37`	`return false;`
`38`	`38`	`}`
	`39`	`+`
	`40`	`+bool is_exists_path(const exprt &expr)`
	`41`	`+{`
	`42`	`+ return expr.id() == ID_sva_cover;`
	`43`	`+}`