Merge pull request #430 from diffblue/property-normalizer

kroening · web-flow · commit 5612fe0092d5 · 2024-04-14T21:08:22.000-04:00
ebmc: normalize properties
diff --git a/src/ebmc/bdd_engine.cpp b/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?
diff --git a/src/ebmc/bmc.cpp b/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,
diff --git a/src/ebmc/ebmc_base.cpp b/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,
diff --git a/src/ebmc/ebmc_properties.cpp b/src/ebmc/ebmc_properties.cpp
@@ -11,6 +11,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #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();
diff --git a/src/ebmc/ebmc_properties.h b/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);
     }
   };
 
diff --git a/src/ebmc/k_induction.cpp b/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
diff --git a/src/ebmc/liveness_to_safety.cpp b/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(
diff --git a/src/ebmc/neural_liveness.cpp b/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());
diff --git a/src/ebmc/ranking_function.cpp b/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);
diff --git a/src/ic3/r1ead_input.cc b/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) {
diff --git a/src/temporal-logic/Makefile b/src/temporal-logic/Makefile
@@ -1,4 +1,5 @@
 SRC = negate_property.cpp \
+      normalize_property.cpp \
       temporal_logic.cpp \
       #empty line
 
diff --git a/src/temporal-logic/normalize_property.cpp b/src/temporal-logic/normalize_property.cpp
@@ -0,0 +1,65 @@
+/*******************************************************************\
+
+Module: Property Normalization
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#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;
+}
diff --git a/src/temporal-logic/normalize_property.h b/src/temporal-logic/normalize_property.h
@@ -0,0 +1,21 @@
+/*******************************************************************\
+
+Module: Property Normalization
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#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
diff --git a/src/verilog/verilog_synthesis.cpp b/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);
   }

Original file line number	Diff line number	Diff line change
`@@ -71,7 +71,7 @@ class k_inductiont`
`71`	`71`
`72`	`72`	`static bool supported(const ebmc_propertiest::propertyt &p)`
`73`	`73`	`{`
`74`		`- auto &expr = p.expr;`
	`74`	`+ auto &expr = p.normalized_expr;`
`75`	`75`	`if(expr.id() == ID_sva_always \|\| expr.id() == ID_AG \|\| expr.id() == ID_G)`
`76`	`76`	`{`
`77`	`77`	`// Must be AG p or equivalent.`
`@@ -264,7 +264,7 @@ void k_inductiont::induction_step()`
`264`	`264`	`ns,`
`265`	`265`	`false);`
`266`	`266`
`267`		`- const exprt property(p_it.expr);`
	`267`	`+ const exprt property(p_it.normalized_expr);`
`268`	`268`	`const exprt &p = to_unary_expr(property).op();`
`269`	`269`
`270`	`270`	`// assumption: time frames 0,...,k-1`
Original file line number	Diff line number	Diff line change
`@@ -248,9 +248,11 @@ void liveness_to_safetyt::operator()()`
`248`	`248`	`{`
`249`	`249`	`// We want GFp.`
`250`	`250`	`if(`
`251`		`- property.expr.id() == ID_sva_always &&`
`252`		`- (to_sva_always_expr(property.expr).op().id() == ID_sva_eventually \|\|`
`253`		`- to_sva_always_expr(property.expr).op().id() == ID_sva_s_eventually))`
	`251`	`+ property.normalized_expr.id() == ID_sva_always &&`
	`252`	`+ (to_sva_always_expr(property.normalized_expr).op().id() ==`
	`253`	`+ ID_sva_eventually \|\|`
	`254`	`+ to_sva_always_expr(property.normalized_expr).op().id() ==`
	`255`	`+ ID_sva_s_eventually))`
`254`	`256`	`{`
`255`	`257`	`translate_GFp(property);`
`256`	`258`	`}`
`@@ -265,7 +267,7 @@ void liveness_to_safetyt::operator()()`
`265`	`267`
`266`	`268`	`void liveness_to_safetyt::translate_GFp(propertyt &property)`
`267`	`269`	`{`
`268`		`- auto &p = to_unary_expr(to_unary_expr(property.expr).op()).op();`
	`270`	`+ auto &p = to_unary_expr(to_unary_expr(property.normalized_expr).op()).op();`
`269`	`271`
`270`	`272`	`// create the 'live' symbol, one for each liveness property`
`271`	`273`	`{`
`@@ -299,7 +301,8 @@ void liveness_to_safetyt::translate_GFp(propertyt &property)`
`299`	`301`	`conjunction({transition_system.trans_expr.trans(), std::move(live_trans)});`
`300`	`302`
`301`	`303`	`// replace the liveness property`
`302`		`- property.expr = safety_replacement(property.name, property.expr);`
	`304`	`+ property.normalized_expr =`
	`305`	`+ safety_replacement(property.name, property.normalized_expr);`
`303`	`306`	`}`
`304`	`307`
`305`	`308`	`void liveness_to_safety(`
Original file line number	Diff line number	Diff line change
`@@ -162,13 +162,14 @@ void neural_livenesst::validate_properties()`
`162`	`162`	`{`
`163`	`163`	`// ignore`
`164`	`164`	`}`
`165`		`- else if(property.expr.id() == ID_AF)`
	`165`	`+ else if(property.normalized_expr.id() == ID_AF)`
`166`	`166`	`{`
`167`	`167`	`// ok`
`168`	`168`	`}`
`169`	`169`	`else if(`
`170`		`- property.expr.id() == ID_sva_always &&`
`171`		`- to_sva_always_expr(property.expr).op().id() == ID_sva_s_eventually)`
	`170`	`+ property.normalized_expr.id() == ID_sva_always &&`
	`171`	`+ to_sva_always_expr(property.normalized_expr).op().id() ==`
	`172`	`+ ID_sva_s_eventually)`
`172`	`173`	`{`
`173`	`174`	`// ok`
`174`	`175`	`}`
`@@ -188,7 +189,7 @@ void neural_livenesst::set_live_signal(`
`188`	`189`	`auto main_symbol_writeable = transition_system.symbol_table.get_writeable(`
`189`	`190`	`transition_system.main_symbol->name);`
`190`	`191`	`main_symbol_writeable->value = original_trans_expr; // copy`
`191`		`- ::set_live_signal(transition_system, property.expr);`
	`192`	`+ ::set_live_signal(transition_system, property.normalized_expr);`
`192`	`193`	`}`
`193`	`194`
`194`	`195`	`std::function<void(trans_tracet)>`
`@@ -301,7 +302,7 @@ tvt neural_livenesst::verify(`
`301`	`302`
`302`	`303`	`auto result = is_ranking_function(`
`303`	`304`	`transition_system,`
`304`		`- property.expr,`
	`305`	`+ property.normalized_expr,`
`305`	`306`	`candidate,`
`306`	`307`	`solver_factory,`
`307`	`308`	`message.get_message_handler());`