EBMC: tautology checker

regression/ebmc-spot/sva-buechi/sequence5.desc

@@ -1,7 +1,7 @@
 CORE
 ../../verilog/SVA/sequence5.sv
 --buechi
-^\[main\.p0\] 1: PROVED up to bound \d+$
+^\[main\.p0\] 1: PROVED \(tautology\)$
 ^\[main\.p1\] 0: REFUTED$
 ^\[main\.p2\] 1'bx: REFUTED$
 ^\[main\.p3\] 1'bz: REFUTED$

regression/ebmc-spot/sva-buechi/sva_and1.desc

@@ -1,7 +1,7 @@
 CORE
 ../../verilog/SVA/sva_and1.sv
 --buechi
-^\[main\.p0\] always \(1 and 1\): PROVED up to bound \d+$
+^\[main\.p0\] always \(1 and 1\): PROVED \(tautology\)$
 ^\[main\.p1\] always \(1 and 0\): REFUTED$
 ^\[main\.p2\] always \(1 and 32'b0000000000000000000000000000000x\): REFUTED$
 ^EXIT=10$

regression/ebmc-spot/sva-buechi/sva_iff1.desc

@@ -1,7 +1,7 @@
 CORE
 ../../verilog/SVA/sva_iff1.sv
 --buechi
-^\[main\.p0\] always \(1 iff 1\): PROVED up to bound \d+$
+^\[main\.p0\] always \(1 iff 1\): PROVED \(tautology\)$
 ^\[main\.p1\] always \(1 iff 0\): REFUTED$
 ^\[main\.p2\] always \(1 iff 32'b0000000000000000000000000000000x\): REFUTED$
 ^EXIT=10$

regression/ebmc-spot/sva-buechi/sva_implies1.desc

@@ -1,7 +1,7 @@
 CORE
 ../../verilog/SVA/sva_implies1.sv
 --buechi
-^\[main\.p0\] always \(1 implies 1\): PROVED up to bound \d+$
+^\[main\.p0\] always \(1 implies 1\): PROVED \(tautology\)$
 ^\[main\.p1\] always \(1 implies 0\): REFUTED$
 ^\[main\.p2\] always \(1 implies 32'b0000000000000000000000000000000x\): REFUTED$
 ^EXIT=10$

regression/ebmc-spot/sva-buechi/sva_not1.desc

@@ -1,7 +1,7 @@
 CORE
 ../../verilog/SVA/sva_not1.sv
 --buechi
-^\[main\.p0] always not 0: PROVED up to bound \d+$
+^\[main\.p0] always not 0: PROVED \(tautology\)$
 ^\[main\.p1] always not 1: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/ebmc/engine-heuristic/tautology1.desc

@@ -0,0 +1,16 @@
+CORE
+tautology1.smv
+
+^\[.*\] 2 > 1: PROVED \(tautology\)$
+^\[.*\] G 2 > 1: PROVED \(tautology\)$
+^\[.*\] X 2 > 1: PROVED \(tautology\)$
+^\[.*\] F 2 > 1: PROVED \(tautology\)$
+^\[.*\] 2 > 1: PROVED \(tautology\)$
+^\[.*\] AG 2 > 1: PROVED \(tautology\)$
+^\[.*\] AX 2 > 1: PROVED \(tautology\)$
+^\[.*\] AF 2 > 1: PROVED \(tautology\)$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/engine-heuristic/tautology1.smv

@@ -0,0 +1,10 @@
+MODULE main
+
+LTLSPEC 2>1
+LTLSPEC G 2>1
+LTLSPEC X 2>1
+LTLSPEC F 2>1
+CTLSPEC 2>1
+CTLSPEC AG 2>1
+CTLSPEC AX 2>1
+CTLSPEC AF 2>1

src/ebmc/Makefile

@@ -36,6 +36,7 @@ SRC = \
       show_formula_solver.cpp \
       show_properties.cpp \
       show_trans.cpp \
+      tautology_check.cpp \
       transition_system.cpp \
       waveform.cpp \
       #empty line

src/ebmc/instrument_buechi.cpp

@@ -64,15 +64,24 @@ void instrument_buechi(
     transition_system.trans_expr.trans() =
       and_exprt{transition_system.trans_expr.trans(), buechi.trans};
 
-    // Replace the normalized property expression.
-    // Note that we have negated the property,
-    // so this is the negation of the Buechi acceptance condition.
-    property.normalized_expr =
-      F_exprt{G_exprt{not_exprt{buechi.liveness_signal}}};
+    // Replace the normalized property expression
+    // by the Buechi acceptance condition.
+    exprt::operandst property_conjuncts;
+
+    if(!buechi.liveness_signal.is_false())
+    {
+      // Note that we have negated the property,
+      // so this is the negation of the Buechi acceptance condition.
+      property_conjuncts.push_back(
+        F_exprt{G_exprt{not_exprt{buechi.liveness_signal}}});
+    }
 
     if(!buechi.error_signal.is_true())
-      property.normalized_expr = and_exprt{
-        property.normalized_expr, G_exprt{not_exprt{buechi.error_signal}}};
+    {
+      property_conjuncts.push_back(G_exprt{not_exprt{buechi.error_signal}});
+    }
+
+    property.normalized_expr = conjunction(property_conjuncts);
 
     message.debug() << "New property: " << format(property.normalized_expr)
                     << messaget::eom;

src/ebmc/property_checker.cpp

@@ -25,6 +25,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #include "netlist.h"
 #include "output_file.h"
 #include "report_results.h"
+#include "tautology_check.h"
 
 #include <chrono>
 #include <iostream>
@@ -382,7 +383,22 @@ property_checker_resultt engine_heuristic(
   message.status() << "No engine given, attempting heuristic engine selection"
                    << messaget::eom;
 
-  // First check whether we have a low completenes threshold
+  // First check if we can tell that the property is a tautology
+  message.status() << "Tautology check" << messaget::eom;
+
+  auto tautology_check_result =
+    tautology_check(cmdline, properties, solver_factory, message_handler);
+
+  properties.properties = tautology_check_result.properties;
+
+  if(!properties.has_unfinished_property())
+    return tautology_check_result; // done
+
+  properties.reset_failure();
+  properties.reset_inconclusive();
+  properties.reset_unsupported();
+
+  // Check whether we have a low completenes threshold
   message.status() << "Attempting completeness threshold" << messaget::eom;
 
   auto completeness_threshold_result = completeness_threshold(

src/ebmc/tautology_check.cpp

@@ -0,0 +1,84 @@
+/*******************************************************************\
+
+Module: Property Tautology Check
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#include "tautology_check.h"
+
+#include <util/namespace.h>
+
+#include <temporal-logic/ctl.h>
+#include <temporal-logic/ltl.h>
+
+static bool is_tautology(
+  const exprt &expr,
+  const ebmc_solver_factoryt &solver_factory,
+  message_handlert &message_handler)
+{
+  auto is_tautology_p = [&solver_factory, &message_handler](const exprt &expr)
+  {
+    // rec. call
+    return is_tautology(expr, solver_factory, message_handler);
+  };
+
+  if(!has_temporal_operator(expr))
+  {
+    // State predicate. Let's ask the SAT solver.
+    if(expr.is_true())
+      return true;
+
+    symbol_tablet symbol_table;
+    namespacet ns{symbol_table};
+    auto solver = solver_factory(ns, message_handler);
+
+    switch(solver.decision_procedure()(not_exprt{expr}))
+    {
+    case decision_proceduret::resultt::D_UNSATISFIABLE:
+      return true;
+
+    case decision_proceduret::resultt::D_SATISFIABLE:
+    case decision_proceduret::resultt::D_ERROR:
+    default:
+      return false;
+    }
+  }
+  else // has temporal operator
+  {
+    if(expr.id() == ID_G && is_tautology_p(to_G_expr(expr).op()))
+      return true;
+    else if(expr.id() == ID_F && is_tautology_p(to_F_expr(expr).op()))
+      return true;
+    else if(expr.id() == ID_X && is_tautology_p(to_X_expr(expr).op()))
+      return true;
+    else if(expr.id() == ID_AG && is_tautology_p(to_AG_expr(expr).op()))
+      return true;
+    else if(expr.id() == ID_AF && is_tautology_p(to_AF_expr(expr).op()))
+      return true;
+    else if(expr.id() == ID_AX && is_tautology_p(to_AX_expr(expr).op()))
+      return true;
+    else // other temporal operator
+      return false;
+  }
+}
+
+property_checker_resultt tautology_check(
+  const cmdlinet &,
+  const ebmc_propertiest &properties,
+  const ebmc_solver_factoryt &solver_factory,
+  message_handlert &message_handler)
+{
+  property_checker_resultt result{properties};
+
+  for(auto &property : result.properties)
+  {
+    if(is_tautology(property.normalized_expr, solver_factory, message_handler))
+    {
+      property.proved("tautology");
+    }
+  }
+
+  return result;
+}

src/ebmc/tautology_check.h

@@ -0,0 +1,25 @@
+/*******************************************************************\
+
+Module: Property Tautology Check
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_EBMC_TAUTOLOGY_CHECK_H
+#define CPROVER_EBMC_TAUTOLOGY_CHECK_H
+
+#include "ebmc_solver_factory.h"
+#include "property_checker.h"
+
+class cmdlinet;
+class ebmc_propertiest;
+class message_handlert;
+
+[[nodiscard]] property_checker_resultt tautology_check(
+  const cmdlinet &,
+  const ebmc_propertiest &,
+  const ebmc_solver_factoryt &,
+  message_handlert &);
+
+#endif