Pointer cleanup #1154

kroening · 2017-07-19T11:43:43Z

This is in preparation for giving pointers a width (much like integers), using constructors and a service function to produce pointer and reference types whenever appropriate.

Split off PR #970.

tautschnig · 2017-07-19T11:46:35Z

src/ansi-c/ansi_c_entry_point.cpp

@@ -327,8 +327,7 @@ bool ansi_c_entry_point(
        zero_string.type().set(ID_size, "infinity");
        exprt index(ID_index, char_type());
        index.copy_to_operands(zero_string, from_integer(0, uint_type()));
-        exprt address_of("address_of", pointer_typet());
-        address_of.type().subtype()=char_type();
+        exprt address_of("address_of", pointer_type(char_type()));


Please use address_of_exprt

Happy to approve once pushed.

tautschnig · 2017-07-19T11:47:53Z

src/cpp/cpp_constructor.cpp

-    address_of.type().subtype()=object_tc.type();
-    address_of.copy_to_operands(object_tc);
+    exprt address_of=
+      address_of_exprt(object_tc, pointer_type(object_tc.type()));


address_of_exprt address_of(object_tc...);

tautschnig · 2017-07-19T11:48:13Z

src/cpp/cpp_destructor.cpp

-    address_of.type().subtype()=object.type();
-    address_of.copy_to_operands(object);
+    exprt address_of=
+      address_of_exprt(object, pointer_type(object.type()));


tautschnig · 2017-07-19T11:48:39Z

src/cpp/cpp_typecheck_conversions.cpp

+  index_exprt index(
+    expr,
+    from_integer(0, index_type()),
+    expr.type().subtype());


The third argument is not necessary

tautschnig · 2017-07-19T11:49:36Z

src/cpp/cpp_typecheck_conversions.cpp

-                  expr_pfrom, pto, expr_ptmp, tmp_rank))
+            // try derived-to-base conversion
+            exprt expr_pfrom=
+              address_of_exprt(expr, pointer_type(expr.type()));


addres_of_exprt expr_pfrom...

tautschnig · 2017-07-19T11:55:08Z

src/goto-symex/auto_objects.cpp

@@ -67,7 +67,9 @@ void goto_symext::initialize_auto_object(
      // could be NULL nondeterministically

      address_of_exprt address_of_expr=
-        address_of_exprt(make_auto_object(type.subtype()));
+        address_of_exprt(


Use constructor, not assignment

tautschnig · 2017-07-19T11:55:28Z

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected]

 #include <util/namespace.h>
 #include <util/std_expr.h>
+#include <util/c_types.h>


Nit picking as above

tautschnig · 2017-07-19T11:55:38Z

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/ieee_float.h>
 #include <util/simplify_expr.h>
+#include <util/c_types.h>


Nit picking as above

tautschnig · 2017-07-19T11:56:44Z

src/solvers/smt2/smt2_conv.cpp

@@ -23,6 +23,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/base_type.h>
 #include <util/string2int.h>
 #include <util/invariant.h>
+#include <util/c_types.h>


Nit picking as above

tautschnig · 2017-07-19T11:58:22Z

src/util/std_expr.cpp

+
+\*******************************************************************/
+
+address_of_exprt::address_of_exprt(const exprt &_op):


Is this actually being used? Most (all?) calls above appear to use a two-argument constructor

Now using it more.

tautschnig · 2017-07-20T09:57:20Z

src/ansi-c/ansi_c_entry_point.cpp


        if(argv_symbol.type.subtype()!=address_of.type())
          address_of.make_typecast(argv_symbol.type.subtype());

        // assign argv[*] to the address of a string-object
-        exprt array_of("array_of", argv_symbol.type);
-        array_of.copy_to_operands(address_of);
+        exprt array_of=array_of_exprt(address_of, argv_symbol.type);


Could use array_of_exprt array_of(... here

tautschnig · 2017-07-20T09:58:13Z

src/ansi-c/ansi_c_entry_point.cpp


-          exprt index_expr(ID_index, arg1.type().subtype());
+          exprt index_expr(ID_index, pointer_type.subtype());


index_exprt index_expr(...) and the lines below should be eliminated

tautschnig · 2017-07-20T09:58:48Z

src/ansi-c/ansi_c_entry_point.cpp


-          exprt index_expr(ID_index, arg2.type().subtype());
+          exprt index_expr(ID_index, pointer_type.subtype());


index_exprt index_expr(... and again code below to be eliminated

tautschnig · 2017-07-20T10:00:52Z

src/cpp/cpp_typecheck_conversions.cpp

@@ -1715,10 +1698,9 @@ bool cpp_typecheckt::const_typecast(
    if(new_expr.type()!=type.subtype())
      return false;

-    exprt address_of(ID_address_of, type);
-    address_of.copy_to_operands(expr);
+    exprt address_of=address_of_exprt(expr, to_pointer_type(type));


Might be a candidate for address_of_exprt address_of(...

Unfortunately not, as this might turn into a dereference expression.

tautschnig · 2017-07-20T10:02:23Z

src/goto-programs/string_instrumentation.cpp

@@ -825,14 +825,12 @@ void string_instrumentationt::do_strerror(
  }

  // return a pointer to some magic buffer
-  exprt index=exprt(ID_index, char_type());
-  index.copy_to_operands(
+  exprt index=index_exprt(


index_exprt index(...

kroening mentioned this pull request Jul 19, 2017

Pointers get a width #970

Merged

tautschnig requested changes Jul 19, 2017

View reviewed changes

kroening force-pushed the pointer-cleanup branch 2 times, most recently from 894a5b3 to c73ee7a Compare July 20, 2017 09:54

tautschnig requested changes Jul 20, 2017

View reviewed changes

kroening force-pushed the pointer-cleanup branch from c73ee7a to 9dd44d6 Compare July 20, 2017 13:25

tautschnig approved these changes Jul 20, 2017

View reviewed changes

Daniel Kroening added 5 commits July 20, 2017 15:02

get rid of typet(ID_pointer)

d0c9bd3

use pointer_type() instead of pointer_typet()

13f3d5f

address_of now needs a pointer type

636655d

removed an assert

d430319

include order cleanup

db71221

kroening force-pushed the pointer-cleanup branch from 9dd44d6 to db71221 Compare July 20, 2017 14:02

tautschnig merged commit f8b8f9e into master Jul 20, 2017

tautschnig deleted the pointer-cleanup branch July 20, 2017 18:24

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Pointer cleanup #1154

Pointer cleanup #1154

kroening commented Jul 19, 2017

tautschnig Jul 19, 2017

kroening Jul 19, 2017

tautschnig Jul 19, 2017

tautschnig Jul 19, 2017

kroening Jul 19, 2017

tautschnig Jul 19, 2017

kroening Jul 19, 2017

tautschnig Jul 19, 2017

kroening Jul 19, 2017

tautschnig Jul 19, 2017

kroening Jul 19, 2017

tautschnig Jul 19, 2017

kroening Jul 20, 2017

tautschnig Jul 19, 2017

tautschnig Jul 19, 2017

tautschnig Jul 19, 2017

tautschnig Jul 19, 2017

kroening Jul 20, 2017

tautschnig Jul 20, 2017

tautschnig Jul 20, 2017

tautschnig Jul 20, 2017

tautschnig Jul 20, 2017

kroening Jul 20, 2017

tautschnig Jul 20, 2017


		\*******************************************************************/

		address_of_exprt::address_of_exprt(const exprt &_op):


		exprt index_expr(ID_index, arg1.type().subtype());
		exprt index_expr(ID_index, pointer_type.subtype());


		exprt index_expr(ID_index, arg2.type().subtype());
		exprt index_expr(ID_index, pointer_type.subtype());

Pointer cleanup #1154

Pointer cleanup #1154

Conversation

kroening commented Jul 19, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment