Merge pull request #7331 from tautschnig/feature/extract-constant

kroening · web-flow · commit ec854159a91e · 2022-11-28T18:58:00.000Z
Byte extract and extract bits can be constant
diff --git a/regression/cbmc-library/memcpy-01/constant-propagation.desc b/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
diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp
@@ -100,7 +100,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(),
@@ -393,7 +393,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);
   }
@@ -419,9 +419,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)
   {
   }
 
@@ -442,14 +443,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!
@@ -657,7 +662,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);
diff --git a/src/analyses/constant_propagator.h b/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
     {
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
@@ -4467,13 +4467,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)
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
@@ -213,7 +213,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.
diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp
@@ -247,11 +247,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)
   {
diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h
@@ -24,7 +24,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)
   {
   }
 
@@ -175,7 +175,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,
diff --git a/src/goto-instrument/havoc_loops.cpp b/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});
+  }
 }
diff --git a/src/goto-instrument/havoc_utils.h b/src/goto-instrument/havoc_utils.h
@@ -27,7 +27,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)
   {
   }
 
@@ -48,7 +49,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)
   {
   }
 
diff --git a/src/goto-instrument/k_induction.cpp b/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});
+  }
 }
diff --git a/src/goto-symex/goto_state.cpp b/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())
diff --git a/src/goto-symex/goto_symex_is_constant.h b/src/goto-symex/goto_symex_is_constant.h
@@ -17,6 +17,11 @@ Author: Michael Tautschig, tautschn@amazon.com
 
 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
   {
diff --git a/src/goto-symex/goto_symex_state.cpp b/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())
diff --git a/src/goto-symex/symex_goto.cpp b/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(
diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp
@@ -9,12 +9,14 @@ Author: Daniel Kroening, kroening@kroening.com
 #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;
 }
diff --git a/src/util/expr_util.h b/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;
 };
diff --git a/unit/analyses/constant_propagator.cpp b/unit/analyses/constant_propagator.cpp
diff --git a/unit/goto-symex/is_constant.cpp b/unit/goto-symex/is_constant.cpp

Original file line number	Diff line number	Diff line change
`@@ -123,9 +123,9 @@ class constant_propagator_domaint:public ai_domain_baset`
`123`	`123`
`124`	`124`	`void set_dirty_to_top(const dirtyt &dirty, const namespacet &ns);`
`125`	`125`
`126`		`- bool is_constant(const exprt &expr) const;`
	`126`	`+ bool is_constant(const exprt &expr, const namespacet &ns) const;`
`127`	`127`
`128`		`- bool is_constant(const irep_idt &id) const;`
	`128`	`+ bool is_constant(const irep_idt &id, const namespacet &ns) const;`
`129`	`129`
`130`	`130`	`bool is_empty() const`
`131`	`131`	`{`
Original file line number	Diff line number	Diff line change
`@@ -4467,13 +4467,11 @@ void c_typecheck_baset::typecheck_side_effect_assignment(`
`4467`	`4467`	`class is_compile_time_constantt : public is_constantt`
`4468`	`4468`	`{`
`4469`	`4469`	`public:`
`4470`		`- explicit is_compile_time_constantt(const namespacet &ns) : ns(ns)`
	`4470`	`+ explicit is_compile_time_constantt(const namespacet &ns) : is_constantt(ns)`
`4471`	`4471`	`{`
`4472`	`4472`	`}`
`4473`	`4473`
`4474`	`4474`	`protected:`
`4475`		`- const namespacet &ns;`
`4476`		`-`
`4477`	`4475`	`bool is_constant(const exprt &e) const override`
`4478`	`4476`	`{`
`4479`	`4477`	`if(e.id() == ID_infinity)`
Original file line number	Diff line number	Diff line change
`@@ -247,11 +247,11 @@ bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment)`
`247`	`247`	`std::string::npos;`
`248`	`248`	`}`
`249`	`249`
`250`		`-void widen_assigns(assignst &assigns)`
	`250`	`+void widen_assigns(assignst &assigns, const namespacet &ns)`
`251`	`251`	`{`
`252`	`252`	`assignst result;`
`253`	`253`
`254`		`- havoc_utils_is_constantt is_constant(assigns);`
	`254`	`+ havoc_utils_is_constantt is_constant(assigns, ns);`
`255`	`255`
`256`	`256`	`for(const auto &e : assigns)`
`257`	`257`	`{`
Original file line number	Diff line number	Diff line change
`@@ -24,7 +24,7 @@ class havoc_if_validt : public havoc_utilst`
`24`	`24`	`{`
`25`	`25`	`public:`
`26`	`26`	`havoc_if_validt(const assignst &mod, const namespacet &ns)`
`27`		`- : havoc_utilst(mod), ns(ns)`
	`27`	`+ : havoc_utilst(mod, ns), ns(ns)`
`28`	`28`	`{`
`29`	`29`	`}`
`30`	`30`
`@@ -175,7 +175,7 @@ bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment);`
`175`	`175`	/// with a non-constant offset, e.g. a[i] or *(b+i) with a non-constant `i`,
`176`	`176`	`/// then replace it by the entire underlying object. Otherwise, e.g. for a[i] or`
`177`	`177`	/// *(b+i) when `i` is a known constant, keep the expression in the result.
`178`		`-void widen_assigns(assignst &assigns);`
	`178`	`+void widen_assigns(assignst &assigns, const namespacet &ns);`
`179`	`179`
`180`	`180`	`/// This function recursively searches \p expression to find nested or`
`181`	`181`	`/// non-nested quantified expressions. When a quantified expression is found,`
Original file line number	Diff line number	Diff line change
`@@ -27,7 +27,8 @@ typedef std::set<exprt> assignst;`
`27`	`27`	`class havoc_utils_is_constantt : public is_constantt`
`28`	`28`	`{`
`29`	`29`	`public:`
`30`		`- explicit havoc_utils_is_constantt(const assignst &mod) : assigns(mod)`
	`30`	`+ explicit havoc_utils_is_constantt(const assignst &mod, const namespacet &ns)`
	`31`	`+ : is_constantt(ns), assigns(mod)`
`31`	`32`	`{`
`32`	`33`	`}`
`33`	`34`
`@@ -48,7 +49,8 @@ class havoc_utils_is_constantt : public is_constantt`
`48`	`49`	`class havoc_utilst`
`49`	`50`	`{`
`50`	`51`	`public:`
`51`		`- explicit havoc_utilst(const assignst &mod) : assigns(mod), is_constant(mod)`
	`52`	`+ explicit havoc_utilst(const assignst &mod, const namespacet &ns)`
	`53`	`+ : assigns(mod), is_constant(mod, ns)`
`52`	`54`	`{`
`53`	`55`	`}`
`54`	`56`