Make interpretation of "is constant" match that of goto_symex_statet::constant_propagation

Author: tautschnig

src/analyses/constant_propagator.cpp

@@ -278,30 +278,54 @@ bool constant_propagator_domaint::ai_simplify(
 
 bool constant_propagator_domaint::valuest::is_constant(const exprt &expr) const
 {
-  if(expr.id()==ID_side_effect &&
-     to_side_effect_expr(expr).get_statement()==ID_nondet)
-    return false;
+  if(expr.is_constant())
+    return true;
 
-  if(expr.id()==ID_side_effect &&
-     to_side_effect_expr(expr).get_statement()==ID_allocate)
-    return false;
+  if(expr.id() == ID_address_of)
+  {
+    const address_of_exprt &address_of_expr = to_address_of_expr(expr);
 
-  if(expr.id()==ID_symbol)
-    if(replace_const.expr_map.find(to_symbol_expr(expr).get_identifier())==
-       replace_const.expr_map.end())
-      return false;
+    return is_constant_address_of(address_of_expr.object());
+  }
+  else if(expr.id() == ID_typecast)
+  {
+    const typecast_exprt &typecast_expr = to_typecast_expr(expr);
 
-  if(expr.id()==ID_index)
-    return false;
+    return is_constant(typecast_expr.op());
+  }
+  else if(expr.id() == ID_array_of)
+  {
+    return is_constant(expr.op0());
+  }
+  else if(
+    expr.id() == ID_plus || expr.id() == ID_array ||
+    expr.id() == ID_struct || expr.id() == ID_union)
+  {
+    forall_operands(it, expr)
+      if(!is_constant(*it))
+        return false;
 
-  if(expr.id()==ID_address_of)
-    return is_constant_address_of(to_address_of_expr(expr).object());
+    return true;
+  }
+  // byte_update works, byte_extract may be out-of-bounds
+  else if(
+    expr.id() == ID_byte_update_big_endian ||
+    expr.id() == ID_byte_update_little_endian)
+  {
+    forall_operands(it, expr)
+      if(!is_constant(*it))
+        return false;
 
-  forall_operands(it, expr)
-    if(!is_constant(*it))
-      return false;
+    return true;
+  }
+  else if(expr.id() == ID_symbol)
+  {
+    return
+      replace_const.expr_map.find(to_symbol_expr(expr).get_identifier()) !=
+      replace_const.expr_map.end();
+  }
 
-  return true;
+  return false;
 }
 
 bool constant_propagator_domaint::valuest::is_constant_address_of(
@@ -320,7 +344,10 @@ bool constant_propagator_domaint::valuest::is_constant_address_of(
   if(expr.id()==ID_string_constant)
     return true;
 
-  return true;
+  if(expr.id()==ID_symbol)
+    return true;
+
+  return false;
 }
 
 /// Do not call this when iterating over replace_const.expr_map!