Byte extract and extract bits can be constant

When all operands are constants and the extract is fully within bounds
of the source object then the result is constant. This permits
constant-propagating byte-extract operations from pointers that are
address-of.

Author: tautschnig

regression/cbmc-library/memcpy-01/constant-propagation.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--show-vcc
+main::1::m!0@1#1 = .*byte_extract_(big|little)_endian\(cast\(44, signedbv\[\d+\]\*\), 0, signedbv\[\d+\]\).*
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

src/analyses/constant_propagator.cpp

@@ -101,7 +101,7 @@ void constant_propagator_domaint::assign_rec(
     exprt tmp = rhs;
     partial_evaluate(dest_values, tmp, ns);
 
-    if(dest_values.is_constant(tmp))
+    if(dest_values.is_constant(tmp, ns))
     {
       DATA_INVARIANT(
         ns.lookup(s).type == tmp.type(),
@@ -394,7 +394,7 @@ bool constant_propagator_domaint::two_way_propagate_rec(
     // two-way propagation
     valuest copy_values=values;
     assign_rec(copy_values, lhs, rhs, ns, cp, false);
-    if(!values.is_constant(rhs) || values.is_constant(lhs))
+    if(!values.is_constant(rhs, ns) || values.is_constant(lhs, ns))
       assign_rec(values, rhs, lhs, ns, cp, false);
     change = values.meet(copy_values, ns);
   }
@@ -420,9 +420,10 @@ bool constant_propagator_domaint::ai_simplify(
 class constant_propagator_is_constantt : public is_constantt
 {
 public:
-  explicit constant_propagator_is_constantt(
-    const replace_symbolt &replace_const)
-    : replace_const(replace_const)
+  constant_propagator_is_constantt(
+    const replace_symbolt &replace_const,
+    const namespacet &ns)
+    : is_constantt(ns), replace_const(replace_const)
   {
   }
 
@@ -443,14 +444,18 @@ class constant_propagator_is_constantt : public is_constantt
   const replace_symbolt &replace_const;
 };
 
-bool constant_propagator_domaint::valuest::is_constant(const exprt &expr) const
+bool constant_propagator_domaint::valuest::is_constant(
+  const exprt &expr,
+  const namespacet &ns) const
 {
-  return constant_propagator_is_constantt(replace_const)(expr);
+  return constant_propagator_is_constantt(replace_const, ns)(expr);
 }
 
-bool constant_propagator_domaint::valuest::is_constant(const irep_idt &id) const
+bool constant_propagator_domaint::valuest::is_constant(
+  const irep_idt &id,
+  const namespacet &ns) const
 {
-  return constant_propagator_is_constantt(replace_const).is_constant(id);
+  return constant_propagator_is_constantt(replace_const, ns).is_constant(id);
 }
 
 /// Do not call this when iterating over replace_const.expr_map!
@@ -658,7 +663,7 @@ bool constant_propagator_domaint::partial_evaluate(
   // if the current rounding mode is top we can
   // still get a non-top result by trying all rounding
   // modes and checking if the results are all the same
-  if(!known_values.is_constant(rounding_mode_identifier()))
+  if(!known_values.is_constant(rounding_mode_identifier(), ns))
     return partial_evaluate_with_all_rounding_modes(known_values, expr, ns);
 
   return replace_constants_and_simplify(known_values, expr, ns);

src/analyses/constant_propagator.h

@@ -123,9 +123,9 @@ class constant_propagator_domaint:public ai_domain_baset
 
     void set_dirty_to_top(const dirtyt &dirty, const namespacet &ns);
 
-    bool is_constant(const exprt &expr) const;
+    bool is_constant(const exprt &expr, const namespacet &ns) const;
 
-    bool is_constant(const irep_idt &id) const;
+    bool is_constant(const irep_idt &id, const namespacet &ns) const;
 
     bool is_empty() const
     {

src/ansi-c/c_typecheck_expr.cpp

@@ -4394,13 +4394,11 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
 class is_compile_time_constantt : public is_constantt
 {
 public:
-  explicit is_compile_time_constantt(const namespacet &ns) : ns(ns)
+  explicit is_compile_time_constantt(const namespacet &ns) : is_constantt(ns)
   {
   }
 
 protected:
-  const namespacet &ns;
-
   bool is_constant(const exprt &e) const override
   {
     if(e.id() == ID_infinity)

src/goto-instrument/contracts/contracts.cpp

@@ -217,7 +217,7 @@ void code_contractst::check_apply_loop_contracts(
 
       // If the set contains pairs (i, a[i]),
       // we widen them to (i, __CPROVER_POINTER_OBJECT(a))
-      widen_assigns(to_havoc);
+      widen_assigns(to_havoc, ns);
 
       log.debug() << "No loop assigns clause provided. Inferred targets: {";
       // Add inferred targets to the loop assigns clause.

src/goto-instrument/contracts/utils.cpp

@@ -246,11 +246,11 @@ bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment)
          std::string::npos;
 }
 
-void widen_assigns(assignst &assigns)
+void widen_assigns(assignst &assigns, const namespacet &ns)
 {
   assignst result;
 
-  havoc_utils_is_constantt is_constant(assigns);
+  havoc_utils_is_constantt is_constant(assigns, ns);
 
   for(const auto &e : assigns)
   {

src/goto-instrument/contracts/utils.h

@@ -34,7 +34,7 @@ class havoc_if_validt : public havoc_utilst
 {
 public:
   havoc_if_validt(const assignst &mod, const namespacet &ns)
-    : havoc_utilst(mod), ns(ns)
+    : havoc_utilst(mod, ns), ns(ns)
   {
   }
 
@@ -185,7 +185,7 @@ bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment);
 /// with a non-constant offset, e.g. a[i] or *(b+i) with a non-constant `i`,
 /// then replace it by the entire underlying object. Otherwise, e.g. for a[i] or
 /// *(b+i) when `i` is a known constant, keep the expression in the result.
-void widen_assigns(assignst &assigns);
+void widen_assigns(assignst &assigns, const namespacet &ns);
 
 /// This function recursively searches \p expression to find nested or
 /// non-nested quantified expressions. When a quantified expression is found,

src/goto-instrument/havoc_loops.cpp

@@ -27,11 +27,13 @@ class havoc_loopst
 
   havoc_loopst(
     function_assignst &_function_assigns,
-    goto_functiont &_goto_function)
+    goto_functiont &_goto_function,
+    const namespacet &ns)
     : goto_function(_goto_function),
       local_may_alias(_goto_function),
       function_assigns(_function_assigns),
-      natural_loops(_goto_function.body)
+      natural_loops(_goto_function.body),
+      ns(ns)
   {
     havoc_loops();
   }
@@ -41,6 +43,7 @@ class havoc_loopst
   local_may_aliast local_may_alias;
   function_assignst &function_assigns;
   natural_loops_mutablet natural_loops;
+  const namespacet &ns;
 
   typedef std::set<exprt> assignst;
   typedef const natural_loops_mutablet::natural_loopt loopt;
@@ -66,7 +69,7 @@ void havoc_loopst::havoc_loop(
 
   // build the havocking code
   goto_programt havoc_code;
-  havoc_utilst havoc_gen(assigns);
+  havoc_utilst havoc_gen(assigns, ns);
   havoc_gen.append_full_havoc_code(loop_head->source_location(), havoc_code);
 
   // Now havoc at the loop head. Use insert_swap to
@@ -118,5 +121,8 @@ void havoc_loops(goto_modelt &goto_model)
   function_assignst function_assigns(goto_model.goto_functions);
 
   for(auto &gf_entry : goto_model.goto_functions.function_map)
-    havoc_loopst(function_assigns, gf_entry.second);
+  {
+    havoc_loopst(
+      function_assigns, gf_entry.second, namespacet{goto_model.symbol_table});
+  }
 }

src/goto-instrument/havoc_utils.h

@@ -26,7 +26,8 @@ typedef std::set<exprt> assignst;
 class havoc_utils_is_constantt : public is_constantt
 {
 public:
-  explicit havoc_utils_is_constantt(const assignst &mod) : assigns(mod)
+  explicit havoc_utils_is_constantt(const assignst &mod, const namespacet &ns)
+    : is_constantt(ns), assigns(mod)
   {
   }
 
@@ -47,7 +48,8 @@ class havoc_utils_is_constantt : public is_constantt
 class havoc_utilst
 {
 public:
-  explicit havoc_utilst(const assignst &mod) : assigns(mod), is_constant(mod)
+  explicit havoc_utilst(const assignst &mod, const namespacet &ns)
+    : assigns(mod), is_constant(mod, ns)
   {
   }
 

src/goto-instrument/k_induction.cpp

@@ -28,14 +28,16 @@ class k_inductiont
     goto_functiont &_goto_function,
     bool _base_case,
     bool _step_case,
-    unsigned _k)
+    unsigned _k,
+    const namespacet &ns)
     : function_id(_function_id),
       goto_function(_goto_function),
       local_may_alias(_goto_function),
       natural_loops(_goto_function.body),
       base_case(_base_case),
       step_case(_step_case),
-      k(_k)
+      k(_k),
+      ns(ns)
   {
     k_induction();
   }
@@ -49,6 +51,8 @@ class k_inductiont
   const bool base_case, step_case;
   const unsigned k;
 
+  const namespacet &ns;
+
   void k_induction();
 
   void process_loop(
@@ -97,7 +101,7 @@ void k_inductiont::process_loop(
 
     // build the havocking code
     goto_programt havoc_code;
-    havoc_utilst havoc_gen(assigns);
+    havoc_utilst havoc_gen(assigns, ns);
     havoc_gen.append_full_havoc_code(loop_head->source_location(), havoc_code);
 
     // unwind to get k+1 copies
@@ -165,5 +169,13 @@ void k_induction(
   unsigned k)
 {
   for(auto &gf_entry : goto_model.goto_functions.function_map)
-    k_inductiont(gf_entry.first, gf_entry.second, base_case, step_case, k);
+  {
+    k_inductiont(
+      gf_entry.first,
+      gf_entry.second,
+      base_case,
+      step_case,
+      k,
+      namespacet{goto_model.symbol_table});
+  }
 }

src/goto-symex/goto_state.cpp

@@ -91,7 +91,7 @@ void goto_statet::apply_condition(
     if(is_ssa_expr(rhs))
       std::swap(lhs, rhs);
 
-    if(is_ssa_expr(lhs) && goto_symex_is_constantt()(rhs))
+    if(is_ssa_expr(lhs) && goto_symex_is_constantt(ns)(rhs))
     {
       const ssa_exprt &ssa_lhs = to_ssa_expr(lhs);
       INVARIANT(
@@ -141,7 +141,7 @@ void goto_statet::apply_condition(
     if(is_ssa_expr(rhs))
       std::swap(lhs, rhs);
 
-    if(!is_ssa_expr(lhs) || !goto_symex_is_constantt()(rhs))
+    if(!is_ssa_expr(lhs) || !goto_symex_is_constantt(ns)(rhs))
       return;
 
     if(rhs.is_true())

src/goto-symex/goto_symex_is_constant.h

@@ -17,6 +17,11 @@ Author: Michael Tautschig, [email protected]
 
 class goto_symex_is_constantt : public is_constantt
 {
+public:
+  explicit goto_symex_is_constantt(const namespacet &ns) : is_constantt(ns)
+  {
+  }
+
 protected:
   bool is_constant(const exprt &expr) const override
   {

src/goto-symex/goto_symex_state.cpp

@@ -110,7 +110,7 @@ renamedt<ssa_exprt, L2> goto_symex_statet::assignment(
       "pointer handling for concurrency is unsound");
 
   // Update constant propagation map -- the RHS is L2
-  if(!is_shared && record_value && goto_symex_is_constantt()(rhs))
+  if(!is_shared && record_value && goto_symex_is_constantt(ns)(rhs))
   {
     const auto propagation_entry = propagation.find(l1_identifier);
     if(!propagation_entry.has_value())

src/goto-symex/symex_goto.cpp

@@ -204,7 +204,7 @@ static optionalt<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
   if(!symbol_expr_lhs)
     return {};
 
-  if(!goto_symex_is_constantt()(rhs))
+  if(!goto_symex_is_constantt(ns)(rhs))
     return {};
 
   return try_evaluate_pointer_comparison(

src/util/expr_util.cpp

@@ -9,12 +9,14 @@ Author: Daniel Kroening, [email protected]
 #include "expr_util.h"
 
 #include "arith_tools.h"
+#include "bitvector_expr.h"
+#include "byte_operators.h"
 #include "c_types.h"
 #include "config.h"
 #include "expr_iterator.h"
 #include "namespace.h"
 #include "pointer_expr.h"
-#include "std_expr.h"
+#include "pointer_offset_size.h"
 
 #include <algorithm>
 #include <unordered_set>
@@ -238,7 +240,6 @@ bool is_constantt::is_constant(const exprt &expr) const
     expr.id() == ID_plus || expr.id() == ID_mult || expr.id() == ID_array ||
     expr.id() == ID_with || expr.id() == ID_struct || expr.id() == ID_union ||
     expr.id() == ID_empty_union ||
-    // byte_update works, byte_extract may be out-of-bounds
     expr.id() == ID_byte_update_big_endian ||
     expr.id() == ID_byte_update_little_endian)
   {
@@ -247,6 +248,46 @@ bool is_constantt::is_constant(const exprt &expr) const
         return is_constant(e);
       });
   }
+  else if(auto be = expr_try_dynamic_cast<byte_extract_exprt>(expr))
+  {
+    if(!is_constant(be->op()) || !be->offset().is_constant())
+      return false;
+
+    const auto op_bits = pointer_offset_bits(be->op().type(), ns);
+    if(!op_bits.has_value())
+      return false;
+
+    const auto extract_bits = pointer_offset_bits(be->type(), ns);
+    if(!extract_bits.has_value())
+      return false;
+
+    const mp_integer offset_bits =
+      numeric_cast_v<mp_integer>(to_constant_expr(be->offset())) *
+      be->get_bits_per_byte();
+
+    return offset_bits + *extract_bits <= *op_bits;
+  }
+  else if(auto eb = expr_try_dynamic_cast<extractbits_exprt>(expr))
+  {
+    if(
+      !is_constant(eb->src()) || !eb->lower().is_constant() ||
+      !eb->upper().is_constant())
+    {
+      return false;
+    }
+
+    const auto src_bits = pointer_offset_bits(eb->src().type(), ns);
+    if(!src_bits.has_value())
+      return false;
+
+    const mp_integer lower_bound =
+      numeric_cast_v<mp_integer>(to_constant_expr(eb->lower()));
+    const mp_integer upper_bound =
+      numeric_cast_v<mp_integer>(to_constant_expr(eb->upper()));
+
+    return lower_bound >= 0 && lower_bound <= upper_bound &&
+           upper_bound < src_bits;
+  }
 
   return false;
 }

src/util/expr_util.h

@@ -88,13 +88,19 @@ const exprt &skip_typecast(const exprt &expr);
 class is_constantt
 {
 public:
+  explicit is_constantt(const namespacet &ns) : ns(ns)
+  {
+  }
+
   /// returns true iff the expression can be considered constant
   bool operator()(const exprt &e) const
   {
     return is_constant(e);
   }
 
 protected:
+  const namespacet &ns;
+
   virtual bool is_constant(const exprt &) const;
   virtual bool is_constant_address_of(const exprt &) const;
 };