Merge pull request #1225 from diffblue/tautology-checker

EBMC: tautology checker

Author: kroening

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(