move pointer-related expression classes into separate header file

std_expr.h is by far the largest header file, which impedes on readability.
This commit moves the pointer-related expression classes into a separate
header file, following the pattern in mathematical_expr.h.

Author: kroening

jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp

@@ -12,9 +12,12 @@ Author: Diffblue Ltd.
 #include "create_array_with_type_intrinsic.h"
 
 #include <goto-programs/class_identifier.h>
+
 #include <java_bytecode/java_types.h>
+
 #include <util/fresh_symbol.h>
 #include <util/namespace.h>
+#include <util/pointer_expr.h>
 #include <util/symbol_table_base.h>
 
 /// Returns the symbol name for `org.cprover.CProver.createArrayWithType`

jbmc/src/java_bytecode/java_pointer_casts.cpp

@@ -11,9 +11,10 @@ Author: Daniel Kroening, [email protected]
 
 #include "java_pointer_casts.h"
 
+#include <util/namespace.h>
+#include <util/pointer_expr.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
-#include <util/namespace.h>
 
 #include "java_types.h"
 

jbmc/src/java_bytecode/java_trace_validation.cpp

@@ -11,9 +11,11 @@ Author: Jeannie Moulton
 #include <algorithm>
 
 #include <goto-programs/goto_trace.h>
+
 #include <util/byte_operators.h>
 #include <util/expr.h>
 #include <util/expr_util.h>
+#include <util/pointer_expr.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 

jbmc/src/java_bytecode/java_utils.h

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/message.h>
 #include <util/nodiscard.h>
 #include <util/optional.h>
+#include <util/pointer_expr.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
 

jbmc/unit/java-testing-utils/require_goto_statements.cpp

@@ -10,14 +10,18 @@ Author: Diffblue Ltd.
 
 #include <testing-utils/use_catch.h>
 
-#include <algorithm>
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/show_goto_functions.h>
+
 #include <java_bytecode/java_types.h>
+
 #include <util/expr_iterator.h>
 #include <util/expr_util.h>
+#include <util/pointer_expr.h>
 #include <util/suffix.h>
 
+#include <algorithm>
+
 /// Expand value of a function to include all child codets
 /// \param function_value: The value of the function (e.g. got by looking up
 ///  the function in the symbol table and getting the value)

jbmc/unit/java_bytecode/java_trace_validation/java_trace_validation.cpp

@@ -7,11 +7,15 @@ Author: Diffblue Ltd.
 \*******************************************************************/
 
 #include <goto-programs/goto_trace.h>
+
 #include <java_bytecode/java_trace_validation.h>
 #include <java_bytecode/java_types.h>
+
 #include <testing-utils/message.h>
 #include <testing-utils/use_catch.h>
+
 #include <util/byte_operators.h>
+#include <util/pointer_expr.h>
 
 TEST_CASE("java trace validation", "[core][java_trace_validation]")
 {

jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp

@@ -23,6 +23,7 @@ Author: Chris Smowton, [email protected]
 #include <util/config.h>
 #include <util/expr_util.h>
 #include <util/options.h>
+#include <util/pointer_expr.h>
 
 /// An example customised value_sett. It makes a series of small changes
 /// to the underlying value_sett logic, which can then be verified by the

jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp

@@ -11,7 +11,6 @@ Author: Jesse Sigal, [email protected]
 
 #include <java_bytecode/java_bytecode_language.h>
 #include <java_bytecode/java_types.h>
-#include <numeric>
 
 #include <langapi/language_util.h>
 #include <langapi/mode.h>
@@ -22,8 +21,11 @@ Author: Jesse Sigal, [email protected]
 #include <util/config.h>
 #include <util/mathematical_expr.h>
 #include <util/mathematical_types.h>
+#include <util/pointer_expr.h>
 #include <util/simplify_expr.h>
 
+#include <numeric>
+
 /// \class Types used throughout the test. Currently it is impossible to
 /// statically initialize this value, there is a PR to allow this
 /// diffblue/cbmc/pull/1213

scripts/expected_doxygen_warnings.txt

@@ -83,19 +83,20 @@ 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 (182), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'c_types.h' not generated, too many nodes (110), 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 '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.
 warning: Included by graph for 'expr.h' not generated, too many nodes (88), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'expr_util.h' not generated, too many nodes (60), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'expr_util.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'invariant.h' not generated, too many nodes (187), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'irep.h' not generated, too many nodes (62), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'message.h' not generated, too many nodes (116), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'namespace.h' not generated, too many nodes (112), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'namespace.h' not generated, too many nodes (113), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (101), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'prefix.h' not generated, too many nodes (86), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (76), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (77), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_code.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'std_expr.h' not generated, too many nodes (249), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'std_expr.h' not generated, too many nodes (248), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_types.h' not generated, too many nodes (124), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'symbol_table.h' not generated, too many nodes (95), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

src/analyses/ai_domain.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "ai_domain.h"
 
+#include <util/pointer_expr.h>
 #include <util/simplify_expr.h>
 
 jsont ai_domain_baset::output_json(const ai_baset &ai, const namespacet &ns)

src/analyses/custom_bitvector_analysis.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include "custom_bitvector_analysis.h"
 
 #include <util/expr_util.h>
+#include <util/pointer_expr.h>
 #include <util/simplify_expr.h>
 #include <util/string_constant.h>
 #include <util/xml_irep.h>

src/analyses/dirty.cpp

@@ -13,6 +13,7 @@ Date: March 2013
 
 #include "dirty.h"
 
+#include <util/pointer_expr.h>
 #include <util/std_expr.h>
 
 void dirtyt::build(const goto_functiont &goto_function)

src/analyses/escape_analysis.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include "escape_analysis.h"
 
 #include <util/cprover_prefix.h>
+#include <util/pointer_expr.h>
 #include <util/simplify_expr.h>
 
 bool escape_domaint::is_tracked(const symbol_exprt &symbol)

src/analyses/flow_insensitive_analysis.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #include "flow_insensitive_analysis.h"
 
 #include <util/expr_util.h>
+#include <util/pointer_expr.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
 

src/analyses/global_may_alias.cpp

@@ -11,6 +11,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "global_may_alias.h"
 
+#include <util/pointer_expr.h>
+
 /// Populate list of aliases for a given identifier in a context in
 /// which an object is being written to.
 /// \param lhs: A left hand side expression, containing an identifier.

src/analyses/goto_check.cpp

@@ -26,6 +26,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/invariant.h>
 #include <util/make_unique.h>
 #include <util/options.h>
+#include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
 #include <util/prefix.h>

src/analyses/goto_rw.cpp

@@ -20,6 +20,7 @@ Date: April 2010
 #include <util/endianness_map.h>
 #include <util/expr_util.h>
 #include <util/make_unique.h>
+#include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>
 #include <util/std_code.h>

src/analyses/invariant_set.cpp

@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/c_types.h>
 #include <util/expr_util.h>
 #include <util/namespace.h>
+#include <util/pointer_expr.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>

src/analyses/local_bitvector_analysis.cpp

@@ -14,11 +14,12 @@ Author: Daniel Kroening, [email protected]
 #include <iterator>
 #include <algorithm>
 
-#include <util/std_expr.h>
-#include <util/std_code.h>
+#include <util/c_types.h>
 #include <util/expr_util.h>
+#include <util/pointer_expr.h>
+#include <util/std_code.h>
+#include <util/std_expr.h>
 
-#include <util/c_types.h>
 #include <langapi/language_util.h>
 
 void local_bitvector_analysist::flagst::print(std::ostream &out) const

src/analyses/local_may_alias.cpp

@@ -15,8 +15,9 @@ Author: Daniel Kroening, [email protected]
 #include <algorithm>
 
 #include <util/arith_tools.h>
-#include <util/std_expr.h>
+#include <util/pointer_expr.h>
 #include <util/std_code.h>
+#include <util/std_expr.h>
 
 #include <util/c_types.h>
 #include <langapi/language_util.h>

src/analyses/local_safe_pointers.h

@@ -13,6 +13,8 @@ Author: Diffblue Ltd
 #define CPROVER_ANALYSES_LOCAL_SAFE_POINTERS_H
 
 #include <goto-programs/goto_program.h>
+
+#include <util/pointer_expr.h>
 #include <util/std_expr.h>
 
 /// A very simple, cheap analysis to determine when dereference operations are

src/analyses/static_analysis.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <memory>
 
 #include <util/expr_util.h>
+#include <util/pointer_expr.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
 

src/analyses/variable-sensitivity/abstract_enviroment.cpp

@@ -5,11 +5,10 @@
  Author: Thomas Kiley, [email protected]
 
 \*******************************************************************/
-#include <algorithm>
-#include <functional>
-#include <map>
-#include <ostream>
-#include <stack>
+
+#include "abstract_enviroment.h"
+
+#include "abstract_object_statistics.h"
 
 #include <analyses/ai.h>
 #include <analyses/variable-sensitivity/abstract_object.h>
@@ -18,10 +17,15 @@
 #include <analyses/variable-sensitivity/pointer_abstract_object.h>
 #include <analyses/variable-sensitivity/struct_abstract_object.h>
 #include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
+
+#include <util/pointer_expr.h>
 #include <util/simplify_expr.h>
 
-#include "abstract_enviroment.h"
-#include "abstract_object_statistics.h"
+#include <algorithm>
+#include <functional>
+#include <map>
+#include <ostream>
+#include <stack>
 
 #ifdef DEBUG
 #  include <iostream>

src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp

@@ -6,14 +6,17 @@
 
 \*******************************************************************/
 
-#include <ostream>
-
 #include "constant_pointer_abstract_object.h"
+
 #include <analyses/ai.h>
 #include <analyses/variable-sensitivity/abstract_enviroment.h>
+
+#include <util/pointer_expr.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
 
+#include <ostream>
+
 constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
   const typet &type)
   : pointer_abstract_objectt(type)

src/analyses/variable-sensitivity/write_stack.cpp

@@ -16,6 +16,7 @@
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/pointer_expr.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 

src/ansi-c/ansi_c_entry_point.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
+#include <util/pointer_expr.h>
 #include <util/string_constant.h>
 
 #include <goto-programs/goto_functions.h>

src/ansi-c/c_typecast.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/config.h>
 #include <util/expr_util.h>
 #include <util/mathematical_types.h>
+#include <util/pointer_expr.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/symbol.h>

src/ansi-c/c_typecheck_expr.cpp

@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/ieee_float.h>
 #include <util/mathematical_expr.h>
 #include <util/mathematical_types.h>
+#include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
 #include <util/prefix.h>

src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/cprover_prefix.h>
+#include <util/pointer_expr.h>
 #include <util/std_types.h>
 #include <util/string_constant.h>
 

src/ansi-c/c_typecheck_type.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/config.h>
 #include <util/fresh_symbol.h>
 #include <util/mathematical_types.h>
+#include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>
 

src/ansi-c/expr2c.cpp

@@ -23,6 +23,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/lispexpr.h>
 #include <util/lispirep.h>
 #include <util/namespace.h>
+#include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
 #include <util/prefix.h>

src/assembler/remove_asm.cpp

@@ -16,6 +16,7 @@ Date:   December 2014
 #include "remove_asm.h"
 
 #include <util/c_types.h>
+#include <util/pointer_expr.h>
 #include <util/string_constant.h>
 
 #include <goto-programs/goto_model.h>

src/cpp/cpp_constructor.cpp

@@ -12,9 +12,9 @@ Author: Daniel Kroening, [email protected]
 #include "cpp_typecheck.h"
 
 #include <util/arith_tools.h>
-#include <util/std_types.h>
-
 #include <util/c_types.h>
+#include <util/pointer_expr.h>
+#include <util/std_types.h>
 
 #include "cpp_util.h"
 

src/cpp/cpp_typecheck_code.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include "cpp_typecheck.h"
 
 #include <util/arith_tools.h>
+#include <util/pointer_expr.h>
 #include <util/source_location.h>
 
 #include "cpp_convert_type.h"

src/cpp/cpp_typecheck_constructor.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include "cpp_typecheck.h"
 
 #include <util/arith_tools.h>
+#include <util/pointer_expr.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>