Merge pull request #5879 from tautschnig/clz-expression

New expression: count_leading_zeros_exprt

Author: tautschnig

regression/ansi-c/__builtin_clz-02/main.c

@@ -0,0 +1,10 @@
+int main()
+{
+#ifdef __GNUC__
+  _Static_assert(
+    __builtin_clz(0xffU) == 8 * sizeof(unsigned) - 8,
+    "GCC/Clang compile-time constant");
+#endif
+
+  return 0;
+}

regression/cbmc-library/__builtin_clz-02/test.desc renamed to regression/ansi-c/__builtin_clz-02/test.desc

@@ -56,5 +56,9 @@ int main()
   __CPROVER_assume(u != 0);
   assert(nlz2a(u) == __builtin_clz(u));
 
+#undef __builtin_clz
+  // a failing assertion should be generated as __builtin_clz is undefined for 0
+  __builtin_clz(0U);
+
   return 0;
 }

regression/cbmc-library/__builtin_clz-02/main.c

@@ -0,0 +1,10 @@
+CORE
+main.c
+--bounds-check
+^\[main.bit_count.\d+\] line 61 count leading zeros argument in __builtin_clz\(0u\): FAILURE$
+^\*\* 1 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc-library/__builtin_clz-01/main.c renamed to regression/cbmc/__builtin_clz-01/main.c

@@ -21,19 +21,19 @@
 warning: Include graph for 'goto_instrument_parse_options.cpp' not generated, too many nodes (97), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'goto_functions.h' not generated, too many nodes (66), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'goto_model.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'arith_tools.h' not generated, too many nodes (182), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'arith_tools.h' not generated, too many nodes (181), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'c_types.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'config.h' not generated, too many nodes (87), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'exception_utils.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'expr.h' not generated, too many nodes (87), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'expr_util.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'invariant.h' not generated, too many nodes (187), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'invariant.h' not generated, too many nodes (186), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'irep.h' not generated, too many nodes (62), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'message.h' not generated, too many nodes (117), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'namespace.h' not generated, too many nodes (109), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (117), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'prefix.h' not generated, too many nodes (85), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (77), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (79), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_code.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_expr.h' not generated, too many nodes (241), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_types.h' not generated, too many nodes (102), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

regression/cbmc/__builtin_clz-01/test.desc

@@ -172,7 +172,9 @@ class goto_checkt
 
   using conditionst = std::list<conditiont>;
 
-  void bounds_check(const index_exprt &, const guardt &);
+  void bounds_check(const exprt &, const guardt &);
+  void bounds_check_index(const index_exprt &, const guardt &);
+  void bounds_check_clz(const count_leading_zeros_exprt &, const guardt &);
   void div_by_zero_check(const div_exprt &, const guardt &);
   void mod_by_zero_check(const mod_exprt &, const guardt &);
   void mod_overflow_check(const mod_exprt &, const guardt &);
@@ -1321,17 +1323,28 @@ std::string goto_checkt::array_name(const exprt &expr)
   return ::array_name(ns, expr);
 }
 
-void goto_checkt::bounds_check(
-  const index_exprt &expr,
-  const guardt &guard)
+void goto_checkt::bounds_check(const exprt &expr, const guardt &guard)
 {
   if(!enable_bounds_check)
     return;
 
-  if(expr.find("bounds_check").is_not_nil() &&
-     !expr.get_bool("bounds_check"))
+  if(
+    expr.find(ID_C_bounds_check).is_not_nil() &&
+    !expr.get_bool(ID_C_bounds_check))
+  {
     return;
+  }
 
+  if(expr.id() == ID_index)
+    bounds_check_index(to_index_expr(expr), guard);
+  else if(expr.id() == ID_count_leading_zeros)
+    bounds_check_clz(to_count_leading_zeros_expr(expr), guard);
+}
+
+void goto_checkt::bounds_check_index(
+  const index_exprt &expr,
+  const guardt &guard)
+{
   typet array_type = expr.array().type();
 
   if(array_type.id()==ID_pointer)
@@ -1507,6 +1520,19 @@ void goto_checkt::bounds_check(
   }
 }
 
+void goto_checkt::bounds_check_clz(
+  const count_leading_zeros_exprt &expr,
+  const guardt &guard)
+{
+  add_guarded_property(
+    notequal_exprt{expr.op(), from_integer(0, expr.op().type())},
+    "count leading zeros argument",
+    "bit count",
+    expr.find_source_location(),
+    expr,
+    guard);
+}
+
 void goto_checkt::add_guarded_property(
   const exprt &asserted_expr,
   const std::string &comment,
@@ -1726,7 +1752,7 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard)
 
   if(expr.id()==ID_index)
   {
-    bounds_check(to_index_expr(expr), guard);
+    bounds_check(expr, guard);
   }
   else if(expr.id()==ID_div)
   {
@@ -1763,6 +1789,10 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard)
   {
     pointer_primitive_check(expr, guard);
   }
+  else if(expr.id() == ID_count_leading_zeros)
+  {
+    bounds_check(expr, guard);
+  }
 }
 
 void goto_checkt::check(const exprt &expr)

scripts/expected_doxygen_warnings.txt

@@ -407,7 +407,7 @@ bool generate_ansi_c_start_function(
           argv_symbol.symbol_expr(), argc_symbol.symbol_expr());
 
         // disable bounds check on that one
-        index_expr.set("bounds_check", false);
+        index_expr.set(ID_C_bounds_check, false);
 
         init_code.add(code_assignt(index_expr, null));
       }
@@ -423,7 +423,7 @@ bool generate_ansi_c_start_function(
         index_exprt index_expr(
           envp_symbol.symbol_expr(), envp_size_symbol.symbol_expr());
         // disable bounds check on that one
-        index_expr.set("bounds_check", false);
+        index_expr.set(ID_C_bounds_check, false);
 
         equal_exprt is_null(std::move(index_expr), std::move(null));
 
@@ -449,7 +449,7 @@ bool generate_ansi_c_start_function(
             argv_symbol.symbol_expr(), from_integer(0, index_type()));
 
           // disable bounds check on that one
-          index_expr.set("bounds_check", false);
+          index_expr.set(ID_C_bounds_check, false);
 
           const pointer_typet &pointer_type =
             to_pointer_type(parameters[1].type());

src/analyses/goto_check.cpp

@@ -2689,27 +2689,14 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
-    side_effect_expr_function_callt try_constant{expr};
-    typecheck_function_call_arguments(try_constant);
-    exprt argument = try_constant.arguments().front();
-    simplify(argument, *this);
-    const auto int_constant = numeric_cast<mp_integer>(argument);
-
-    if(
-      !int_constant.has_value() || *int_constant == 0 ||
-      argument.type().id() != ID_unsignedbv)
-    {
-      return nil_exprt{};
-    }
+    typecheck_function_call_arguments(expr);
 
-    const std::string binary_value = integer2binary(
-      *int_constant, to_unsignedbv_type(argument.type()).get_width());
-    std::size_t n_leading_zeros = binary_value.find('1');
-    CHECK_RETURN(n_leading_zeros != std::string::npos);
+    count_leading_zeros_exprt clz{expr.arguments().front(),
+                                  has_prefix(id2string(identifier), "__lzcnt"),
+                                  expr.type()};
+    clz.add_source_location() = source_location;
 
-    return from_integer(
-      n_leading_zeros,
-      to_code_type(try_constant.function().type()).return_type());
+    return std::move(clz);
   }
   else if(identifier==CPROVER_PREFIX "equal")
   {

src/ansi-c/ansi_c_entry_point.cpp

@@ -3896,6 +3896,9 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()==ID_type)
     return convert(src.type());
 
+  else if(src.id() == ID_count_leading_zeros)
+    return convert_function(src, "__builtin_clz");
+
   // no C language expression for internal representation
   return convert_norep(src, precedence);
 }

src/ansi-c/c_typecheck_expr.cpp

@@ -33,64 +33,6 @@ inline void __sync_synchronize(void)
   #endif
 }
 
-/* FUNCTION: __builtin_clz */
-
-int __builtin_popcount(unsigned int);
-
-inline int __builtin_clz(unsigned int x)
-{
-  __CPROVER_precondition(x != 0, "__builtin_clz(0) is undefined");
-
-  x = x | (x >> 1);
-  x = x | (x >> 2);
-  x = x | (x >> 4);
-  x = x | (x >> 8);
-  if(sizeof(x) >= 4)
-    x = x | (x >> 16);
-
-  return __builtin_popcount(~x);
-}
-
-/* FUNCTION: __builtin_clzl */
-
-int __builtin_popcountl(unsigned long int);
-
-inline int __builtin_clzl(unsigned long int x)
-{
-  __CPROVER_precondition(x != 0, "__builtin_clzl(0) is undefined");
-
-  x = x | (x >> 1);
-  x = x | (x >> 2);
-  x = x | (x >> 4);
-  x = x | (x >> 8);
-  if(sizeof(x) >= 4)
-    x = x | (x >> 16);
-  if(sizeof(x) >= 8)
-    x = x | (x >> 32);
-
-  return __builtin_popcountl(~x);
-}
-
-/* FUNCTION: __builtin_clzll */
-
-int __builtin_popcountll(unsigned long long int);
-
-inline int __builtin_clzll(unsigned long long int x)
-{
-  __CPROVER_precondition(x != 0, "__builtin_clzll(0) is undefined");
-
-  x = x | (x >> 1);
-  x = x | (x >> 2);
-  x = x | (x >> 4);
-  x = x | (x >> 8);
-  if(sizeof(x) >= 4)
-    x = x | (x >> 16);
-  if(sizeof(x) >= 8)
-    x = x | (x >> 32);
-
-  return __builtin_popcountll(~x);
-}
-
 /* FUNCTION: __builtin_ffs */
 
 int __builtin_clz(unsigned int x);

src/ansi-c/expr2c.cpp

@@ -51,46 +51,3 @@ inline HANDLE CreateThread(
   return handle;
 }
 #endif
-
-/* FUNCTION: __lzcnt16 */
-
-#ifdef _MSC_VER
-int __builtin_clz(unsigned int x);
-
-unsigned short __lzcnt16(unsigned short value)
-{
-  if(value == 0)
-    return 16;
-
-  return __builtin_clz(value) -
-         (sizeof(unsigned int) - sizeof(unsigned short)) * 8;
-}
-#endif
-
-/* FUNCTION: __lzcnt */
-
-#ifdef _MSC_VER
-int __builtin_clz(unsigned int x);
-
-unsigned int __lzcnt(unsigned int value)
-{
-  if(value == 0)
-    return 32;
-
-  return __builtin_clz(value);
-}
-#endif
-
-/* FUNCTION: __lzcnt64 */
-
-#ifdef _MSC_VER
-int __builtin_clzll(unsigned long long x);
-
-unsigned __int64 __lzcnt64(unsigned __int64 value)
-{
-  if(value == 0)
-    return 64;
-
-  return __builtin_clzll(value);
-}
-#endif

src/ansi-c/library/gcc.c

@@ -570,7 +570,7 @@ void string_abstractiont::abstract_function_call(
 
       index_exprt idx(str_args.back(), from_integer(0, index_type()));
       // disable bounds check on that one
-      idx.set("bounds_check", false);
+      idx.set(ID_C_bounds_check, false);
 
       str_args.back()=address_of_exprt(idx);
     }

src/ansi-c/library/windows.c

@@ -141,7 +141,6 @@ SRC = $(BOOLEFORCE_SRC) \
       floatbv/float_approximation.cpp \
       lowering/byte_operators.cpp \
       lowering/functions.cpp \
-      lowering/popcount.cpp \
       bdd/miniBDD/miniBDD.cpp \
       prop/bdd_expr.cpp \
       prop/cover_goals.cpp \

src/goto-programs/string_abstraction.cpp

@@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/magic.h>
 #include <util/mp_arith.h>
 #include <util/replace_expr.h>
+#include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
 #include <util/string2int.h>
@@ -227,7 +228,12 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
   else if(expr.id()==ID_power)
      return convert_power(to_binary_expr(expr));
   else if(expr.id() == ID_popcount)
-    return convert_bv(lower_popcount(to_popcount_expr(expr), ns));
+    return convert_bv(simplify_expr(to_popcount_expr(expr).lower(), ns));
+  else if(expr.id() == ID_count_leading_zeros)
+  {
+    return convert_bv(
+      simplify_expr(to_count_leading_zeros_expr(expr).lower(), ns));
+  }
 
   return conversion_failed(expr);
 }

src/solvers/Makefile

@@ -14,7 +14,6 @@ Author: Michael Tautschnig
 class byte_extract_exprt;
 class byte_update_exprt;
 class namespacet;
-class popcount_exprt;
 
 /// Rewrite a byte extract expression to more fundamental operations.
 /// \param src: Byte extract expression
@@ -44,10 +43,4 @@ exprt lower_byte_operators(const exprt &src, const namespacet &ns);
 
 bool has_byte_operator(const exprt &src);
 
-/// Lower a popcount_exprt to arithmetic and logic expressions
-/// \param expr: Input expression to be translated
-/// \param ns: Namespace for type lookups
-/// \return Semantically equivalent expression
-exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns);
-
 #endif /* CPROVER_SOLVERS_LOWERING_EXPR_LOWERING_H */