ebmc: normalize properties

This introduces a pass during which the given property is 'normalized',
using heuristic rewrites, with the goal to reduce the burden of a large
number of redundant case-splits in each backend.

src/ebmc/bdd_engine.cpp

@@ -165,7 +165,7 @@ int bdd_enginet::operator()()
       cmdline, transition_system, message.get_message_handler());
 
     for(const propertyt &p : properties.properties)
-      get_atomic_propositions(p.expr);
+      get_atomic_propositions(p.normalized_expr);
 
     message.status() << "Building BDD for netlist" << messaget::eom;
 
@@ -376,7 +376,7 @@ void bdd_enginet::compute_counterexample(
 
   ::unwind(netlist, bmc_map, message, solver);
   ::unwind_property(
-    property.expr,
+    property.normalized_expr,
     property.timeframe_literals,
     message.get_message_handler(),
     solver,
@@ -450,17 +450,18 @@ void bdd_enginet::check_property(propertyt &property)
            !has_temporal_operator(to_F_expr(to_G_expr(expr).op()).op());
   };
 
-  if(is_AGp(property.expr))
+  if(is_AGp(property.normalized_expr))
   {
     AGp(property);
   }
   else if(
-    is_AG_AFp(property.expr) || is_always_eventually(property.expr) ||
-    is_GFp(property.expr))
+    is_AG_AFp(property.normalized_expr) ||
+    is_always_eventually(property.normalized_expr) ||
+    is_GFp(property.normalized_expr))
   {
     AGAFp(property);
   }
-  else if(!has_temporal_operator(property.expr))
+  else if(!has_temporal_operator(property.normalized_expr))
   {
     just_p(property);
   }
@@ -482,7 +483,7 @@ Function: bdd_enginet::AGp
 
 void bdd_enginet::AGp(propertyt &property)
 {
-  const exprt &sub_expr = to_unary_expr(property.expr).op();
+  const exprt &sub_expr = to_unary_expr(property.normalized_expr).op();
   BDD p = property2BDD(sub_expr);
 
   // Start with !p, and go backwards until saturation or we hit an
@@ -563,7 +564,8 @@ Function: bdd_enginet::AGAFp
 
 void bdd_enginet::AGAFp(propertyt &property)
 {
-  const exprt &sub_expr = to_unary_expr(to_unary_expr(property.expr).op()).op();
+  const exprt &sub_expr =
+    to_unary_expr(to_unary_expr(property.normalized_expr).op()).op();
   BDD p = property2BDD(sub_expr);
 
   // Start with p, and go backwards until saturation.
@@ -648,7 +650,7 @@ void bdd_enginet::just_p(propertyt &property)
 {
   // We check whether the BDD for the negation of the property
   // contains an initial state.
-  exprt negation = negate_property(property.expr);
+  exprt negation = negate_property(property.normalized_expr);
   BDD states = property2BDD(negation);
 
   // do we have an initial state?

src/ebmc/bmc.cpp

@@ -47,14 +47,14 @@ void bmc(
       continue;
 
     // Is it supported by the BMC engine?
-    if(!bmc_supports_property(property.expr))
+    if(!bmc_supports_property(property.normalized_expr))
     {
       property.failure("property not supported by BMC engine");
       continue;
     }
 
     ::property(
-      property.expr,
+      property.normalized_expr,
       property.timeframe_handles,
       message_handler,
       solver,

src/ebmc/ebmc_base.cpp

@@ -200,7 +200,7 @@ int ebmc_baset::do_bit_level_bmc(cnft &solver, bool convert_only)
         continue;
 
       ::unwind_property(
-        property.expr,
+        property.normalized_expr,
         property.timeframe_literals,
         message.get_message_handler(),
         solver,

src/ebmc/ebmc_properties.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #include <langapi/language.h>
 #include <langapi/language_util.h>
 #include <langapi/mode.h>
+#include <temporal-logic/normalize_property.h>
 #include <verilog/sva_expr.h>
 
 #include "ebmc_error.h"
@@ -70,7 +71,9 @@ ebmc_propertiest ebmc_propertiest::from_transition_system(
       else
         properties.properties.back().name = symbol.pretty_name;
 
-      properties.properties.back().expr = symbol.value;
+      properties.properties.back().original_expr = symbol.value;
+      properties.properties.back().normalized_expr =
+        normalize_property(symbol.value);
       properties.properties.back().location = symbol.location;
       properties.properties.back().expr_string = value_as_string;
       properties.properties.back().mode = symbol.mode;
@@ -156,7 +159,8 @@ ebmc_propertiest ebmc_propertiest::from_command_line(
     ebmc_propertiest properties;
     properties.properties.push_back(propertyt());
     auto &p = properties.properties.back();
-    p.expr = expr;
+    p.original_expr = expr;
+    p.normalized_expr = normalize_property(expr);
     p.expr_string = expr_as_string;
     p.mode = transition_system.main_symbol->mode;
     p.location.make_nil();

src/ebmc/ebmc_properties.h

@@ -29,7 +29,8 @@ class ebmc_propertiest
     source_locationt location;
     std::string expr_string;
     irep_idt mode;
-    exprt expr;
+    exprt original_expr;
+    exprt normalized_expr;
     bvt timeframe_literals;             // bit level
     exprt::operandst timeframe_handles; // word level
     std::string description;
@@ -143,7 +144,7 @@ class ebmc_propertiest
 
     bool requires_lasso_constraints() const
     {
-      return ::requires_lasso_constraints(expr);
+      return ::requires_lasso_constraints(normalized_expr);
     }
   };
 

src/ebmc/k_induction.cpp

@@ -71,7 +71,7 @@ class k_inductiont
 
   static bool supported(const ebmc_propertiest::propertyt &p)
   {
-    auto &expr = p.expr;
+    auto &expr = p.normalized_expr;
     if(expr.id() == ID_sva_always || expr.id() == ID_AG || expr.id() == ID_G)
     {
       // Must be AG p or equivalent.
@@ -264,7 +264,7 @@ void k_inductiont::induction_step()
       ns,
       false);
 
-    const exprt property(p_it.expr);
+    const exprt property(p_it.normalized_expr);
     const exprt &p = to_unary_expr(property).op();
 
     // assumption: time frames 0,...,k-1

src/ebmc/liveness_to_safety.cpp

@@ -248,9 +248,11 @@ void liveness_to_safetyt::operator()()
     {
       // We want GFp.
       if(
-        property.expr.id() == ID_sva_always &&
-        (to_sva_always_expr(property.expr).op().id() == ID_sva_eventually ||
-         to_sva_always_expr(property.expr).op().id() == ID_sva_s_eventually))
+        property.normalized_expr.id() == ID_sva_always &&
+        (to_sva_always_expr(property.normalized_expr).op().id() ==
+           ID_sva_eventually ||
+         to_sva_always_expr(property.normalized_expr).op().id() ==
+           ID_sva_s_eventually))
       {
         translate_GFp(property);
       }
@@ -265,7 +267,7 @@ void liveness_to_safetyt::operator()()
 
 void liveness_to_safetyt::translate_GFp(propertyt &property)
 {
-  auto &p = to_unary_expr(to_unary_expr(property.expr).op()).op();
+  auto &p = to_unary_expr(to_unary_expr(property.normalized_expr).op()).op();
 
   // create the 'live' symbol, one for each liveness property
   {
@@ -299,7 +301,8 @@ void liveness_to_safetyt::translate_GFp(propertyt &property)
     conjunction({transition_system.trans_expr.trans(), std::move(live_trans)});
 
   // replace the liveness property
-  property.expr = safety_replacement(property.name, property.expr);
+  property.normalized_expr =
+    safety_replacement(property.name, property.normalized_expr);
 }
 
 void liveness_to_safety(

src/ebmc/neural_liveness.cpp

@@ -162,13 +162,14 @@ void neural_livenesst::validate_properties()
     {
       // ignore
     }
-    else if(property.expr.id() == ID_AF)
+    else if(property.normalized_expr.id() == ID_AF)
     {
       // ok
     }
     else if(
-      property.expr.id() == ID_sva_always &&
-      to_sva_always_expr(property.expr).op().id() == ID_sva_s_eventually)
+      property.normalized_expr.id() == ID_sva_always &&
+      to_sva_always_expr(property.normalized_expr).op().id() ==
+        ID_sva_s_eventually)
     {
       // ok
     }
@@ -188,7 +189,7 @@ void neural_livenesst::set_live_signal(
   auto main_symbol_writeable = transition_system.symbol_table.get_writeable(
     transition_system.main_symbol->name);
   main_symbol_writeable->value = original_trans_expr; // copy
-  ::set_live_signal(transition_system, property.expr);
+  ::set_live_signal(transition_system, property.normalized_expr);
 }
 
 std::function<void(trans_tracet)>
@@ -301,7 +302,7 @@ tvt neural_livenesst::verify(
 
   auto result = is_ranking_function(
     transition_system,
-    property.expr,
+    property.normalized_expr,
     candidate,
     solver_factory,
     message.get_message_handler());

src/ebmc/ranking_function.cpp

@@ -109,7 +109,7 @@ int do_ranking_function(
 
   auto result = is_ranking_function(
     transition_system,
-    property.expr,
+    property.normalized_expr,
     ranking_function,
     solver_factory,
     message_handler);

src/ic3/r1ead_input.cc

@@ -36,9 +36,9 @@ void ic3_enginet::find_prop_lit()
   bool found = find_prop(Prop);
 
   assert(found);
-  assert(Prop.expr.id() == ID_sva_always);
+  assert(Prop.normalized_expr.id() == ID_sva_always);
 
-  exprt Oper = to_unary_expr(Prop.expr).op();
+  exprt Oper = to_unary_expr(Prop.normalized_expr).op();
 
   found = banned_expr(Oper);
   if (found) {

src/temporal-logic/Makefile

@@ -1,4 +1,5 @@
 SRC = negate_property.cpp \
+      normalize_property.cpp \
       temporal_logic.cpp \
       #empty line
 

src/temporal-logic/normalize_property.cpp

@@ -0,0 +1,65 @@
+/*******************************************************************\
+
+Module: Property Normalization
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "normalize_property.h"
+
+#include <util/std_expr.h>
+
+#include <verilog/sva_expr.h>
+
+#include "temporal_expr.h"
+
+exprt normalize_pre_not(not_exprt expr)
+{
+  const auto &op = expr.op();
+
+  if(op.id() == ID_and)
+  {
+    auto operands = op.operands();
+    for(auto &op : operands)
+      op = not_exprt{op};
+    return or_exprt{std::move(operands)};
+  }
+  else if(op.id() == ID_or)
+  {
+    auto operands = op.operands();
+    for(auto &op : operands)
+      op = not_exprt{op};
+    return and_exprt{std::move(operands)};
+  }
+  else if(op.id() == ID_not)
+  {
+    return to_not_expr(op).op();
+  }
+
+  return std::move(expr);
+}
+
+exprt normalize_pre_implies(implies_exprt expr)
+{
+  return or_exprt{not_exprt{expr.lhs()}, expr.rhs()};
+}
+
+exprt normalize_property(exprt expr)
+{
+  // pre-traversal
+  if(expr.id() == ID_not)
+    expr = normalize_pre_not(to_not_expr(expr));
+  else if(expr.id() == ID_implies)
+    expr = normalize_pre_implies(to_implies_expr(expr));
+  else if(expr.id() == ID_sva_cover)
+    expr = G_exprt{not_exprt{to_sva_cover_expr(expr).op()}};
+
+  // normalize the operands
+  for(auto &op : expr.operands())
+    op = normalize_property(op);
+
+  // post-traversal
+
+  return expr;
+}

src/temporal-logic/normalize_property.h

@@ -0,0 +1,21 @@
+/*******************************************************************\
+
+Module: Property Normalization
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_TEMPORAL_LOGIC_NORMALIZE_PROPERTY_H
+#define CPROVER_TEMPORAL_LOGIC_NORMALIZE_PROPERTY_H
+
+#include <util/expr.h>
+
+/// This applies the following rewrites:
+/// cover(φ) --> G¬φ
+/// ¬(a ∨ b) --> ¬a ∧ ¬b
+/// ¬(a ∧ b) --> ¬a ∨ ¬b
+/// ¬¬φ --> φ
+exprt normalize_property(exprt);
+
+#endif

src/verilog/verilog_synthesis.cpp

@@ -1850,7 +1850,8 @@ void verilog_synthesist::synth_assert_cover(
 
   if(module_item.id() == ID_verilog_assert_property)
   {
-    // Concurrent assertions come with an implicit 'always'.
+    // Concurrent assertions come with an implicit 'always'
+    // (1800-2017 Sec 16.12.11).
     if(cond.id() != ID_sva_always)
       cond = sva_always_exprt(cond);
   }