Expression rewriting may enable further constant propagation

The included regression test is an example the requires interleaving of
simplification and constant propagation.

Author: tautschnig

regression/goto-analyzer/constant_propagation_14/test.desc

@@ -1,9 +1,9 @@
-FUTURE
+KNOWNBUG
 main.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] file main.c line 11 function main, assertion tmp_if_expr: SUCCESS$
-^\[main.assertion.2\] file main.c line 12 function main, assertion tmp_if_expr\$1: FAILURE$
+^\[main.assertion.2\] file main.c line 12 function main, assertion tmp_if_expr\$0: FAILURE \(if reachable\)$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_18/main.c

@@ -0,0 +1,8 @@
+#include <assert.h>
+
+int main()
+{
+  int i = 1;
+  int *p = &i;
+  assert(*p == 1);
+}

regression/goto-analyzer/constant_propagation_18/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--constants --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file main.c line 7 function main, assertion \*p == 1: SUCCESS$
+--
+^warning: ignoring

src/analyses/constant_propagator.cpp

@@ -576,8 +576,25 @@ bool constant_propagator_domaint::replace_constants_and_simplify(
   exprt &expr,
   const namespacet &ns)
 {
-  bool did_not_change_anything = known_values.replace_const.replace(expr);
-  did_not_change_anything &= simplify(expr, ns);
+  bool did_not_change_anything = true;
+
+  // iterate constant propagation and simplification until we cannot
+  // constant-propagate any further - a prime example is pointer dereferencing,
+  // where constant propagation may have a value of the pointer, the simplifier
+  // takes care of evaluating dereferencing, and we might then have the value of
+  // the resulting symbol known to constant propagation and thus replace the
+  // dereferenced expression by a constant
+  while(!known_values.replace_const.replace(expr))
+  {
+    did_not_change_anything = false;
+    simplify(expr, ns);
+  }
+
+  // even if we haven't been able to constant-propagate anything, run the
+  // simplifier on the expression
+  if(did_not_change_anything)
+    did_not_change_anything &= simplify(expr, ns);
+
   return did_not_change_anything;
 }