Merge pull request #5800 from tautschnig/array-ssa

Array-element sensitive SSA: avoid string-to-integer-to-string

Author: kroening

scripts/expected_doxygen_warnings.txt

@@ -83,7 +83,7 @@ warning: Include graph for 'cbmc_parse_options.cpp' not generated, too many node
 warning: Include graph for 'goto_instrument_parse_options.cpp' not generated, too many nodes (97), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'goto_functions.h' not generated, too many nodes (66), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'goto_model.h' not generated, too many nodes (109), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'arith_tools.h' not generated, too many nodes (183), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'arith_tools.h' not generated, too many nodes (182), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'c_types.h' not generated, too many nodes (111), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'config.h' not generated, too many nodes (85), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'exception_utils.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

src/util/ssa_expr.cpp

@@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <sstream>
 
-#include "arith_tools.h"
 #include "pointer_expr.h"
 
 /// If \p expr is:
@@ -29,8 +28,7 @@ initialize_ssa_identifier(std::ostream &os, const exprt &expr)
   }
   if(auto index = expr_try_dynamic_cast<index_exprt>(expr))
   {
-    const auto idx =
-      numeric_cast_v<mp_integer>(to_constant_expr(index->index()));
+    const irep_idt &idx = to_constant_expr(index->index()).get_value();
     return initialize_ssa_identifier(os, index->array()) << "[[" << idx << "]]";
   }
   if(auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr))
@@ -77,8 +75,7 @@ static void build_ssa_identifier_rec(
 
     build_ssa_identifier_rec(index.array(), l0, l1, l2, os, l1_object_os);
 
-    const mp_integer idx =
-      numeric_cast_v<mp_integer>(to_constant_expr(index.index()));
+    const irep_idt &idx = to_constant_expr(index.index()).get_value();
     os << "[[" << idx << "]]";
     l1_object_os << "[[" << idx << "]]";
   }