Rename is_constantt (and it's children) to can_forward_propagatet

There is too much ambiguity in what could be called a "constant," and we
really mean "this expression can be forward propagated."

Author: tautschnig

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/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

@@ -341,7 +341,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, romain.brenguier@diffblue.com
 \*******************************************************************/
 
 #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, tautschn@amazon.com
 /// \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, kroening@kroening.com
 #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, kroening@kroening.com
 #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

@@ -160,7 +160,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);

src/util/expr_util.cpp

@@ -226,7 +226,7 @@ const exprt &skip_typecast(const exprt &expr)
 
 /// This function determines what expressions are to be propagated as
 /// "constants"
-bool is_constantt::is_constant(const exprt &expr) const
+bool can_forward_propagatet::is_constant(const exprt &expr) const
 {
   if(
     expr.id() == ID_symbol || expr.id() == ID_nondet_symbol ||
@@ -306,7 +306,7 @@ bool is_constantt::is_constant(const exprt &expr) const
 }
 
 /// this function determines which reference-typed expressions are constant
-bool is_constantt::is_constant_address_of(const exprt &expr) const
+bool can_forward_propagatet::is_constant_address_of(const exprt &expr) const
 {
   if(expr.id() == ID_symbol)
   {