Merge pull request #1005 from diffblue/completeness_threshold

EBMC: completeness threshold engine

Author: tautschnig

regression/smv/expressions/smv_if2.desc

@@ -1,7 +1,7 @@
 CORE
 smv_if2.smv
 
-^\[.*\] X \(b = 2 \| b = 4\): PROVED up to bound 5$
+^\[.*\] X \(b = 2 \| b = 4\): PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/smv/smv/initial1.desc

@@ -1,7 +1,7 @@
 CORE
 initial1.smv
---bound 0
-^\[spec1\] tmp1 = TRUE: PROVED up to bound 0$
+
+^\[spec1\] tmp1 = TRUE: PROVED$
 ^\[spec2\] tmp2 = TRUE: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/verilog/SVA/initial1.desc

@@ -1,11 +1,11 @@
 CORE
 initial1.sv
---module main --bound 1
-^\[main\.p0\] main\.counter == 0: PROVED up to bound 1$
+--module main
+^\[main\.p0\] main\.counter == 0: PROVED$
 ^\[main\.p1\] main\.counter == 100: REFUTED$
-^\[main\.p2\] ##1 main\.counter == 1: PROVED up to bound 1$
+^\[main\.p2\] ##1 main\.counter == 1: PROVED up to bound 5$
 ^\[main\.p3\] ##1 main\.counter == 100: REFUTED$
-^\[main\.p4\] s_nexttime main\.counter == 1: PROVED up to bound 1$
+^\[main\.p4\] s_nexttime main\.counter == 1: PROVED$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/verilog/SVA/initial2.desc

@@ -1,8 +1,8 @@
 CORE
 initial2.sv
---module main --bound 1
-^\[main\.assert\.1\] main\.counter == 1: PROVED up to bound 1
-^\[main\.assert\.2\] main\.counter == 2: PROVED up to bound 1
+--module main
+^\[main\.assert\.1\] main\.counter == 1: PROVED$
+^\[main\.assert\.2\] main\.counter == 2: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/SVA/sequence5.desc

@@ -1,7 +1,7 @@
 CORE
 sequence5.sv
 
-^\[main\.p0\] 1: PROVED up to bound 5$
+^\[main\.p0\] 1: PROVED$
 ^\[main\.p1\] 0: REFUTED$
 ^\[main\.p2\] 1'bx: REFUTED$
 ^\[main\.p3\] 1'bz: REFUTED$

regression/verilog/SVA/sequence_or1.desc

@@ -1,8 +1,8 @@
 CORE
 sequence_or1.sv
 
-^\[main\.p0\] main\.x == 0 or main\.x == 1: PROVED up to bound \d+$
-^\[main\.p1\] strong\(main\.x == 0 or main\.x == 1\): PROVED up to bound \d+$
+^\[main\.p0\] main\.x == 0 or main\.x == 1: PROVED$
+^\[main\.p1\] strong\(main\.x == 0 or main\.x == 1\): PROVED$
 ^\[main\.p2\] main\.x == 0 or \(nexttime main\.x == 1\): PROVED up to bound \d+$
 ^\[main\.p3\] \(nexttime main\.x == 1\) or main\.x == 1: PROVED up to bound \d+$
 ^EXIT=0$

src/ebmc/Makefile

@@ -7,6 +7,7 @@ SRC = \
       cegar/refine.cpp \
       cegar/simulate.cpp \
       cegar/verify.cpp \
+      completeness_threshold.cpp \
       diameter.cpp \
       diatest.cpp \
       dimacs_writer.cpp \

src/ebmc/completeness_threshold.cpp

@@ -0,0 +1,84 @@
+/*******************************************************************\
+
+Module: Completeness Threshold
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#include "completeness_threshold.h"
+
+#include <temporal-logic/ltl.h>
+#include <temporal-logic/temporal_logic.h>
+#include <verilog/sva_expr.h>
+
+#include "bmc.h"
+
+bool has_low_completeness_threshold(const exprt &expr)
+{
+  if(!has_temporal_operator(expr))
+  {
+    return true; // state predicate only
+  }
+  else if(expr.id() == ID_X)
+  {
+    // X p
+    return !has_temporal_operator(to_X_expr(expr).op());
+  }
+  else if(expr.id() == ID_sva_nexttime)
+  {
+    // nexttime p
+    return !has_temporal_operator(to_sva_nexttime_expr(expr).op());
+  }
+  else
+    return false;
+}
+
+bool has_low_completeness_threshold(const ebmc_propertiest::propertyt &property)
+{
+  return has_low_completeness_threshold(property.normalized_expr);
+}
+
+bool have_low_completeness_threshold(const ebmc_propertiest &properties)
+{
+  for(auto &property : properties.properties)
+    if(has_low_completeness_threshold(property))
+      return true;
+  return false;
+}
+
+property_checker_resultt completeness_threshold(
+  const cmdlinet &cmdline,
+  const transition_systemt &transition_system,
+  const ebmc_propertiest &properties,
+  const ebmc_solver_factoryt &solver_factory,
+  message_handlert &message_handler)
+{
+  // Do we have an eligibile property?
+  if(!have_low_completeness_threshold(properties))
+    return property_checker_resultt{properties}; // give up
+
+  // Do BMC with two timeframes
+  auto result = bmc(
+    1,     // bound
+    false, // convert_only
+    cmdline.isset("bmc-with-assumptions"),
+    transition_system,
+    properties,
+    solver_factory,
+    message_handler);
+
+  for(auto &property : result.properties)
+  {
+    if(property.is_proved_with_bound())
+    {
+      // Turn "PROVED up to bound k" into "PROVED" if k>=CT
+      if(has_low_completeness_threshold(property) && property.bound >= 1)
+        property.proved();
+      else
+        property.unknown();
+    }
+  }
+
+  return result;
+}

src/ebmc/completeness_threshold.h

@@ -0,0 +1,27 @@
+/*******************************************************************\
+
+Module: Completeness Threshold
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_EBMC_COMPLETENESS_THRESHOLD_H
+#define CPROVER_EBMC_COMPLETENESS_THRESHOLD_H
+
+#include "ebmc_solver_factory.h"
+#include "property_checker.h"
+
+class cmdlinet;
+class ebmc_propertiest;
+class message_handlert;
+class transition_systemt;
+
+[[nodiscard]] property_checker_resultt completeness_threshold(
+  const cmdlinet &,
+  const transition_systemt &,
+  const ebmc_propertiest &,
+  const ebmc_solver_factoryt &,
+  message_handlert &);
+
+#endif

src/ebmc/k_induction.cpp

@@ -184,11 +184,12 @@ void k_inductiont::operator()()
     }
   }
 
-  // Fail unsupported properties
+  // Fail unsupported properties that are not proved yet
   for(auto &property : properties.properties)
   {
     if(
-      !supported(property) && !property.is_assumed() && !property.is_disabled())
+      !supported(property) && !property.is_assumed() &&
+      !property.is_disabled() && !property.is_proved())
     {
       property.unsupported("unsupported by k-induction");
     }
@@ -264,7 +265,7 @@ void k_inductiont::induction_step()
   {
     if(
       p_it.is_disabled() || p_it.is_failure() || p_it.is_assumed() ||
-      p_it.is_unsupported())
+      p_it.is_unsupported() || p_it.is_proved())
     {
       continue;
     }