Merge pull request #7717 from tautschnig/feature/constant-pointer-ops

Change is_constantt logic to enumerate not-constant expressions

Author: tautschnig

regression/cbmc/Array_UF22/main.c

@@ -1,6 +1,7 @@
 int main()
 {
-  int a[2] = {0};
-  int b[2] = {0};
+  int x;
+  int a[2] = {x};
+  int b[2] = {x};
   __CPROVER_assert(__CPROVER_array_equal(a, b), "equal");
 }

src/analyses/constant_propagator.cpp

@@ -416,13 +416,13 @@ bool constant_propagator_domaint::ai_simplify(
   return partial_evaluate(values, condition, ns);
 }
 
-class constant_propagator_is_constantt : public is_constantt
+class constant_propagator_can_forward_propagatet : public can_forward_propagatet
 {
 public:
-  constant_propagator_is_constantt(
+  constant_propagator_can_forward_propagatet(
     const replace_symbolt &replace_const,
     const namespacet &ns)
-    : is_constantt(ns), replace_const(replace_const)
+    : can_forward_propagatet(ns), replace_const(replace_const)
   {
   }
 
@@ -437,7 +437,7 @@ class constant_propagator_is_constantt : public is_constantt
     if(expr.id() == ID_symbol)
       return is_constant(to_symbol_expr(expr).get_identifier());
 
-    return is_constantt::is_constant(expr);
+    return can_forward_propagatet::is_constant(expr);
   }
 
   const replace_symbolt &replace_const;
@@ -447,14 +447,15 @@ bool constant_propagator_domaint::valuest::is_constant(
   const exprt &expr,
   const namespacet &ns) const
 {
-  return constant_propagator_is_constantt(replace_const, ns)(expr);
+  return constant_propagator_can_forward_propagatet(replace_const, ns)(expr);
 }
 
 bool constant_propagator_domaint::valuest::is_constant(
   const irep_idt &id,
   const namespacet &ns) const
 {
-  return constant_propagator_is_constantt(replace_const, ns).is_constant(id);
+  return constant_propagator_can_forward_propagatet(replace_const, ns)
+    .is_constant(id);
 }
 
 /// Do not call this when iterating over replace_const.expr_map!

src/ansi-c/c_typecheck_expr.cpp

@@ -4495,23 +4495,60 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
   throw 0;
 }
 
-class is_compile_time_constantt : public is_constantt
+/// Architecturally similar to \ref can_forward_propagatet, but specialized for
+/// what is a constexpr, i.e., an expression that can be fully evaluated at
+/// compile time.
+class is_compile_time_constantt
 {
 public:
-  explicit is_compile_time_constantt(const namespacet &ns) : is_constantt(ns)
+  explicit is_compile_time_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:
-  bool is_constant(const exprt &e) const override
+  const namespacet &ns;
+
+  /// This function determines what expressions are to be propagated as
+  /// "constants"
+  bool is_constant(const exprt &e) const
   {
     if(e.id() == ID_infinity)
       return true;
-    else
-      return is_constantt::is_constant(e);
+
+    if(e.is_constant())
+      return true;
+
+    if(e.id() == ID_address_of)
+    {
+      return is_constant_address_of(to_address_of_expr(e).object());
+    }
+    else if(
+      e.id() == ID_typecast || e.id() == ID_array_of || e.id() == ID_plus ||
+      e.id() == ID_mult || e.id() == ID_array || e.id() == ID_with ||
+      e.id() == ID_struct || e.id() == ID_union || e.id() == ID_empty_union ||
+      e.id() == ID_equal || e.id() == ID_notequal || e.id() == ID_lt ||
+      e.id() == ID_le || e.id() == ID_gt || e.id() == ID_ge ||
+      e.id() == ID_if || e.id() == ID_not || e.id() == ID_and ||
+      e.id() == ID_or || e.id() == ID_bitnot || e.id() == ID_bitand ||
+      e.id() == ID_bitor || e.id() == ID_bitxor)
+    {
+      return std::all_of(
+        e.operands().begin(), e.operands().end(), [this](const exprt &op) {
+          return is_constant(op);
+        });
+    }
+
+    return false;
   }
 
-  bool is_constant_address_of(const exprt &e) const override
+  /// this function determines which reference-typed expressions are constant
+  bool is_constant_address_of(const exprt &e) const
   {
     if(e.id() == ID_symbol)
     {
@@ -4522,8 +4559,27 @@ class is_compile_time_constantt : public is_constantt
       return true;
     else if(e.id() == ID_label)
       return true;
-    else
-      return is_constantt::is_constant_address_of(e);
+    else if(e.id() == ID_index)
+    {
+      const index_exprt &index_expr = to_index_expr(e);
+
+      return is_constant_address_of(index_expr.array()) &&
+             is_constant(index_expr.index());
+    }
+    else if(e.id() == ID_member)
+    {
+      return is_constant_address_of(to_member_expr(e).compound());
+    }
+    else if(e.id() == ID_dereference)
+    {
+      const dereference_exprt &deref = to_dereference_expr(e);
+
+      return is_constant(deref.pointer());
+    }
+    else if(e.id() == ID_string_constant)
+      return true;
+
+    return false;
   }
 };
 

src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp

@@ -66,7 +66,7 @@ assignst dfcc_infer_loop_assigns(
   // widen or drop targets that depend on loop-locals or are non-constant,
   // ie. depend on other locations assigned by the loop.
   // e.g: if the loop assigns {i, a[i]}, then a[i] is non-constant.
-  havoc_utils_is_constantt is_constant(assigns, ns);
+  havoc_utils_can_forward_propagatet is_constant(assigns, ns);
   assignst result;
   for(const auto &expr : assigns)
   {

src/goto-instrument/contracts/utils.cpp

@@ -342,7 +342,7 @@ void widen_assigns(assignst &assigns, const namespacet &ns)
 {
   assignst result;
 
-  havoc_utils_is_constantt is_constant(assigns, ns);
+  havoc_utils_can_forward_propagatet is_constant(assigns, ns);
 
   for(const auto &e : assigns)
   {

src/goto-instrument/havoc_utils.h

@@ -24,22 +24,25 @@ class goto_programt;
 typedef std::set<exprt> assignst;
 
 /// \brief A class containing utility functions for havocing expressions.
-class havoc_utils_is_constantt : public is_constantt
+class havoc_utils_can_forward_propagatet : public can_forward_propagatet
 {
 public:
-  explicit havoc_utils_is_constantt(const assignst &mod, const namespacet &ns)
-    : is_constantt(ns), assigns(mod)
+  explicit havoc_utils_can_forward_propagatet(
+    const assignst &mod,
+    const namespacet &ns)
+    : can_forward_propagatet(ns), assigns(mod)
   {
   }
 
   bool is_constant(const exprt &expr) const override
   {
-    // Besides the "usual" constants (checked in is_constantt::is_constant),
-    // we also treat unmodified symbols as constants
+    // Besides the "usual" constants (checked in
+    // can_forward_propagatet::is_constant), we also treat unmodified symbols as
+    // constants
     if(expr.id() == ID_symbol && assigns.find(expr) == assigns.end())
       return true;
 
-    return is_constantt::is_constant(expr);
+    return can_forward_propagatet::is_constant(expr);
   }
 
 protected:
@@ -102,7 +105,7 @@ class havoc_utilst
 
 protected:
   const assignst &assigns;
-  const havoc_utils_is_constantt is_constant;
+  const havoc_utils_can_forward_propagatet is_constant;
 };
 
 #endif // CPROVER_GOTO_INSTRUMENT_HAVOC_UTILS_H

src/goto-symex/goto_state.cpp

@@ -7,11 +7,12 @@ Author: Romain Brenguier, [email protected]
 \*******************************************************************/
 
 #include "goto_state.h"
-#include "goto_symex_is_constant.h"
-#include "goto_symex_state.h"
 
 #include <util/format_expr.h>
 
+#include "goto_symex_can_forward_propagate.h"
+#include "goto_symex_state.h"
+
 /// Print the constant propagation map in a human-friendly format.
 /// This is primarily for use from the debugger; please don't delete me just
 /// because there aren't any current callers.
@@ -91,7 +92,7 @@ void goto_statet::apply_condition(
     if(is_ssa_expr(rhs))
       std::swap(lhs, rhs);
 
-    if(is_ssa_expr(lhs) && goto_symex_is_constantt(ns)(rhs))
+    if(is_ssa_expr(lhs) && goto_symex_can_forward_propagatet(ns)(rhs))
     {
       const ssa_exprt &ssa_lhs = to_ssa_expr(lhs);
       INVARIANT(
@@ -141,7 +142,7 @@ void goto_statet::apply_condition(
     if(is_ssa_expr(rhs))
       std::swap(lhs, rhs);
 
-    if(!is_ssa_expr(lhs) || !goto_symex_is_constantt(ns)(rhs))
+    if(!is_ssa_expr(lhs) || !goto_symex_can_forward_propagatet(ns)(rhs))
       return;
 
     if(rhs.is_true())

src/goto-symex/goto_symex_is_constant.h renamed to src/goto-symex/goto_symex_can_forward_propagate.h

@@ -9,16 +9,17 @@ Author: Michael Tautschig, [email protected]
 /// \file
 /// GOTO Symex constant propagation
 
-#ifndef CPROVER_GOTO_SYMEX_GOTO_SYMEX_IS_CONSTANT_H
-#define CPROVER_GOTO_SYMEX_GOTO_SYMEX_IS_CONSTANT_H
+#ifndef CPROVER_GOTO_SYMEX_GOTO_SYMEX_CAN_FORWARD_PROPAGATE_H
+#define CPROVER_GOTO_SYMEX_GOTO_SYMEX_CAN_FORWARD_PROPAGATE_H
 
 #include <util/expr.h>
 #include <util/expr_util.h>
 
-class goto_symex_is_constantt : public is_constantt
+class goto_symex_can_forward_propagatet : public can_forward_propagatet
 {
 public:
-  explicit goto_symex_is_constantt(const namespacet &ns) : is_constantt(ns)
+  explicit goto_symex_can_forward_propagatet(const namespacet &ns)
+    : can_forward_propagatet(ns)
   {
   }
 
@@ -56,8 +57,8 @@ class goto_symex_is_constantt : public is_constantt
 #endif
     }
 
-    return is_constantt::is_constant(expr);
+    return can_forward_propagatet::is_constant(expr);
   }
 };
 
-#endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_IS_CONSTANT_H
+#endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_CAN_FORWARD_PROPAGATE_H

src/goto-symex/goto_symex_state.cpp

@@ -23,7 +23,7 @@ Author: Daniel Kroening, [email protected]
 #include <analyses/dirty.h>
 #include <pointer-analysis/add_failed_symbols.h>
 
-#include "goto_symex_is_constant.h"
+#include "goto_symex_can_forward_propagate.h"
 #include "symex_target_equation.h"
 
 static void get_l1_name(exprt &expr);
@@ -112,7 +112,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(ns)(rhs))
+  if(!is_shared && record_value && goto_symex_can_forward_propagatet(ns)(rhs))
   {
     const auto propagation_entry = propagation.find(l1_identifier);
     if(!propagation_entry.has_value())

src/goto-symex/symex_goto.cpp

@@ -22,7 +22,7 @@ Author: Daniel Kroening, [email protected]
 #include <pointer-analysis/value_set_dereference.h>
 
 #include "goto_symex.h"
-#include "goto_symex_is_constant.h"
+#include "goto_symex_can_forward_propagate.h"
 #include "path_storage.h"
 
 #include <algorithm>
@@ -204,7 +204,7 @@ static optionalt<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
   if(!symbol_expr_lhs)
     return {};
 
-  if(!goto_symex_is_constantt(ns)(rhs))
+  if(!goto_symex_can_forward_propagatet(ns)(rhs))
     return {};
 
   return try_evaluate_pointer_comparison(

src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp

@@ -179,7 +179,7 @@ void enumerative_loop_contracts_synthesizert::synthesize_assigns(
     if(new_assign.id() == ID_index || new_assign.id() == ID_dereference)
     {
       address_of_exprt address_of_new_assigns(new_assign);
-      havoc_utils_is_constantt is_constant(assigns_map[loop_id], ns);
+      havoc_utils_can_forward_propagatet is_constant(assigns_map[loop_id], ns);
       if(!is_constant(address_of_new_assigns))
       {
         new_assign = pointer_object(address_of_new_assigns);