From f72b7fce2f5ca02dc9fbf5b5e1649ce869393fd8 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 23 Aug 2017 11:15:04 +0100 Subject: [PATCH 1/3] pointer_typet now requires a width --- regression/invariants/driver.cpp | 4 +++- src/cpp/cpp_typecheck_constructor.cpp | 6 ++---- src/cpp/cpp_typecheck_conversions.cpp | 10 ++-------- src/cpp/parse.cpp | 2 +- src/goto-symex/symex_builtin_functions.cpp | 10 +++++----- src/goto-symex/symex_dead.cpp | 7 +------ src/goto-symex/symex_decl.cpp | 7 +------ src/java_bytecode/java_bytecode_instrument.cpp | 4 ++-- .../java_string_library_preprocess.cpp | 3 +-- src/java_bytecode/java_types.cpp | 9 ++++----- src/path-symex/path_symex.cpp | 10 +++++----- src/pointer-analysis/value_set.cpp | 5 ++--- src/util/simplify_expr_pointer.cpp | 6 ++++-- .../does_remove_const/does_expr_lose_const.cpp | 14 ++++++++------ .../does_type_preserve_const_correctness.cpp | 12 +++++++----- .../is_type_at_least_as_const_as.cpp | 12 +++++++----- 16 files changed, 55 insertions(+), 66 deletions(-) diff --git a/regression/invariants/driver.cpp b/regression/invariants/driver.cpp index c0627bbd341..4c2fbaf5f2b 100644 --- a/regression/invariants/driver.cpp +++ b/regression/invariants/driver.cpp @@ -11,9 +11,11 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include #include + #include #include #include +#include /// An example of structured invariants-- this contains fields to /// describe the error to a catcher, and also produces a human-readable @@ -86,7 +88,7 @@ int main(int argc, char** argv) else if(arg=="data-invariant-string") DATA_INVARIANT(false, "Test invariant failure"); else if(arg=="irep") - INVARIANT_WITH_IREP(false, "error with irep", pointer_typet(void_typet())); + INVARIANT_WITH_IREP(false, "error with irep", pointer_type(void_typet())); else return 1; } diff --git a/src/cpp/cpp_typecheck_constructor.cpp b/src/cpp/cpp_typecheck_constructor.cpp index cfc645c5cb2..40b0fe18afd 100644 --- a/src/cpp/cpp_typecheck_constructor.cpp +++ b/src/cpp/cpp_typecheck_constructor.cpp @@ -223,8 +223,7 @@ void cpp_typecheckt::default_cpctor( cpp_declaratort parameter_tor; parameter_tor.add(ID_value).make_nil(); parameter_tor.set(ID_name, cpp_parameter); - parameter_tor.type()=reference_typet(); - parameter_tor.type().subtype().make_nil(); + parameter_tor.type()=reference_type(nil_typet()); parameter_tor.add_source_location()=source_location; // Parameter declaration @@ -388,9 +387,8 @@ void cpp_typecheckt::default_assignop( declarator_name.get_sub().push_back(irept("=")); declarator_type.id(ID_function_type); - declarator_type.subtype()=reference_typet(); + declarator_type.subtype()=reference_type(nil_typet()); declarator_type.subtype().add("#qualifier").make_nil(); - declarator_type.subtype().subtype().make_nil(); exprt &args=static_cast(declarator.type().add(ID_parameters)); args.add_source_location()=source_location; diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp index e3d314f44aa..c0bb71e9f33 100644 --- a/src/cpp/cpp_typecheck_conversions.cpp +++ b/src/cpp/cpp_typecheck_conversions.cpp @@ -1280,11 +1280,8 @@ bool cpp_typecheckt::reference_binding( if(reference_compatible(expr, type, rank)) { { - address_of_exprt tmp; + address_of_exprt tmp(expr, reference_type(expr.type())); tmp.add_source_location()=expr.source_location(); - tmp.object()=expr; - tmp.type()=pointer_type(tmp.op0().type()); - tmp.type().set(ID_C_reference, true); new_expr.swap(tmp); } @@ -1411,10 +1408,7 @@ bool cpp_typecheckt::reference_binding( if(user_defined_conversion_sequence(arg_expr, type.subtype(), new_expr, rank)) { - address_of_exprt tmp; - tmp.type()=pointer_type(new_expr.type()); - tmp.object()=new_expr; - tmp.type().set(ID_C_reference, true); + address_of_exprt tmp(new_expr, reference_type(new_expr.type())); tmp.add_source_location()=new_expr.source_location(); new_expr.swap(tmp); return true; diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index bcdc444de36..ee399b8af8d 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -3015,7 +3015,7 @@ bool Parser::optPtrOperator(typet &ptrs) if(t=='*') { - pointer_typet op; + typet op(ID_pointer); cpp_tokent tk; lex.get_token(tk); set_location(op, tk); diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index 8b317f3cdc3..327c31c5247 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -165,20 +165,20 @@ void goto_symext::symex_malloc( new_symbol_table.add(value_symbol); - address_of_exprt rhs; + exprt rhs; if(object_type.id()==ID_array) { - rhs.type()=pointer_type(value_symbol.type.subtype()); index_exprt index_expr(value_symbol.type.subtype()); index_expr.array()=value_symbol.symbol_expr(); index_expr.index()=from_integer(0, index_type()); - rhs.op0()=index_expr; + rhs=address_of_exprt( + index_expr, pointer_type(value_symbol.type.subtype())); } else { - rhs.op0()=value_symbol.symbol_expr(); - rhs.type()=pointer_type(value_symbol.type); + rhs=address_of_exprt( + value_symbol.symbol_expr(), pointer_type(value_symbol.type)); } if(rhs.type()!=lhs.type()) diff --git a/src/goto-symex/symex_dead.cpp b/src/goto-symex/symex_dead.cpp index eacf6d247a8..a3a2a03e740 100644 --- a/src/goto-symex/symex_dead.cpp +++ b/src/goto-symex/symex_dead.cpp @@ -45,12 +45,7 @@ void goto_symext::symex_dead(statet &state) exprt rhs; if(failed.is_not_nil()) - { - address_of_exprt address_of_expr; - address_of_expr.object()=failed; - address_of_expr.type()=code.op0().type(); - rhs=address_of_expr; - } + rhs=address_of_exprt(failed, to_pointer_type(code.op0().type())); else rhs=exprt(ID_invalid); diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp index eda7144f99b..3dbdc1e554c 100644 --- a/src/goto-symex/symex_decl.cpp +++ b/src/goto-symex/symex_decl.cpp @@ -60,12 +60,7 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr) exprt rhs; if(failed.is_not_nil()) - { - address_of_exprt address_of_expr; - address_of_expr.object()=failed; - address_of_expr.type()=expr.type(); - rhs=address_of_expr; - } + rhs=address_of_exprt(failed, to_pointer_type(expr.type())); else rhs=exprt(ID_invalid); diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp index ea00b1ac58a..dd29b0b5ec5 100644 --- a/src/java_bytecode/java_bytecode_instrument.cpp +++ b/src/java_bytecode/java_bytecode_instrument.cpp @@ -103,8 +103,8 @@ codet java_bytecode_instrumentt::throw_exception( get_message_handler()); } - pointer_typet exc_ptr_type; - exc_ptr_type.subtype()=symbol_typet(exc_class_name); + pointer_typet exc_ptr_type= + pointer_type(symbol_typet(exc_class_name)); // Allocate and throw an instance of the exception class: diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index a0de9bfc3c1..8e7947d9636 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -1304,8 +1304,7 @@ exprt java_string_library_preprocesst::get_object_at_index( { dereference_exprt deref_objs(argv, argv.type().subtype()); pointer_typet empty_pointer=pointer_type(empty_typet()); - pointer_typet pointer_of_pointer; - pointer_of_pointer.copy_to_subtypes(empty_pointer); + pointer_typet pointer_of_pointer=pointer_type(empty_pointer); member_exprt data_member(deref_objs, "data", pointer_of_pointer); plus_exprt data_pointer_plus_index( data_member, from_integer(index, java_int_type()), data_member.type()); diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp index 22d59cf95e0..c98616d06c0 100644 --- a/src/java_bytecode/java_types.cpp +++ b/src/java_bytecode/java_types.cpp @@ -67,7 +67,7 @@ typet java_boolean_type() reference_typet java_reference_type(const typet &subtype) { - return to_reference_type(reference_type(subtype)); + return reference_type(subtype); } reference_typet java_lang_object_type() @@ -246,11 +246,10 @@ typet java_type_from_string(const std::string &src) class_name[i]='.'; std::string identifier="java::"+class_name; + symbol_typet symbol_type(identifier); + symbol_type.set(ID_C_base_name, class_name); - reference_typet result; - result.subtype()=symbol_typet(identifier); - result.subtype().set(ID_C_base_name, class_name); - return result; + return java_reference_type(symbol_type); } default: diff --git a/src/path-symex/path_symex.cpp b/src/path-symex/path_symex.cpp index 0d8db5f979a..8f8f6f3707a 100644 --- a/src/path-symex/path_symex.cpp +++ b/src/path-symex/path_symex.cpp @@ -245,20 +245,20 @@ void path_symext::symex_malloc( value_symbol.type.set("#dynamic", true); value_symbol.mode=ID_C; - address_of_exprt rhs; + exprt rhs; if(object_type.id()==ID_array) { - rhs.type()=pointer_type(value_symbol.type.subtype()); index_exprt index_expr(value_symbol.type.subtype()); index_expr.array()=value_symbol.symbol_expr(); index_expr.index()=from_integer(0, index_type()); - rhs.op0()=index_expr; + rhs=address_of_exprt( + index_expr, pointer_type(value_symbol.type.subtype())); } else { - rhs.op0()=value_symbol.symbol_expr(); - rhs.type()=pointer_type(value_symbol.type); + rhs=address_of_exprt( + value_symbol.symbol_expr(), pointer_type(value_symbol.type)); } if(rhs.type()!=lhs.type()) diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 5571b4ab8f5..70d2ccb7629 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -1523,9 +1523,8 @@ void value_sett::apply_code( if(failed.is_not_nil()) { - address_of_exprt address_of_expr; - address_of_expr.object()=failed; - address_of_expr.type()=lhs.type(); + address_of_exprt address_of_expr( + failed, to_pointer_type(lhs.type())); assign(lhs, address_of_expr, ns, false, false); } else diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index 938ce023d7e..8f862f7aead 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -78,7 +78,8 @@ bool simplify_exprt::simplify_address_of_arg(exprt &expr) if(!to_integer(expr.op1(), index) && step_size!=-1) { - pointer_typet pointer_type; + pointer_typet pointer_type= + to_pointer_type(to_dereference_expr(expr.op0()).pointer().type()); pointer_type.subtype()=expr.type(); typecast_exprt typecast_expr( from_integer(step_size*index+address, index_type()), pointer_type); @@ -114,7 +115,8 @@ bool simplify_exprt::simplify_address_of_arg(exprt &expr) mp_integer offset=member_offset(struct_type, member, ns); if(offset!=-1) { - pointer_typet pointer_type; + pointer_typet pointer_type= + to_pointer_type(to_dereference_expr(expr.op0()).pointer().type()); pointer_type.subtype()=expr.type(); typecast_exprt typecast_expr( from_integer(address+offset, index_type()), pointer_type); diff --git a/unit/analyses/does_remove_const/does_expr_lose_const.cpp b/unit/analyses/does_remove_const/does_expr_lose_const.cpp index 80e223c93be..d24cce126a3 100644 --- a/unit/analyses/does_remove_const/does_expr_lose_const.cpp +++ b/unit/analyses/does_remove_const/does_expr_lose_const.cpp @@ -10,15 +10,17 @@ /// Does Remove Const Unit Tests #include -#include + #include #include #include +#include + #include #include +#include #include - SCENARIO("does_expr_lose_const", "[core][analyses][does_remove_const][does_expr_remove_const]") { @@ -43,23 +45,23 @@ SCENARIO("does_expr_lose_const", // pointer (can be reassigned) // to int (value can be changed) // int * - typet pointer_to_int_type=pointer_typet(non_const_primitive_type); + typet pointer_to_int_type=pointer_type(non_const_primitive_type); // const pointer (can't be reassigned) // to int (value can be changed) // int * const - typet const_pointer_to_int_type=pointer_typet(non_const_primitive_type); + typet const_pointer_to_int_type=pointer_type(non_const_primitive_type); const_qualifier.write(const_pointer_to_int_type); // pointer (can be reassigned) // to const int (value can't be changed) // const int * - typet pointer_to_const_int_type=pointer_typet(const_primitive_type); + typet pointer_to_const_int_type=pointer_type(const_primitive_type); // constant pointer (can't be reassigned) // to const int (value can't be changed) // const int * const - typet const_pointer_to_const_int_type=pointer_typet(const_primitive_type); + typet const_pointer_to_const_int_type=pointer_type(const_primitive_type); const_qualifier.write(const_pointer_to_const_int_type); symbol_exprt const_primitive_symbol( diff --git a/unit/analyses/does_remove_const/does_type_preserve_const_correctness.cpp b/unit/analyses/does_remove_const/does_type_preserve_const_correctness.cpp index 0f10081c49b..9b678ff1089 100644 --- a/unit/analyses/does_remove_const/does_type_preserve_const_correctness.cpp +++ b/unit/analyses/does_remove_const/does_type_preserve_const_correctness.cpp @@ -11,8 +11,10 @@ #include -#include +#include #include +#include + #include #include #include @@ -42,23 +44,23 @@ SCENARIO("does_type_preserve_const_correctness", // pointer (can be reassigned) // to int (value can be changed) // int * - typet pointer_to_int_type=pointer_typet(non_const_primitive_type); + typet pointer_to_int_type=pointer_type(non_const_primitive_type); // const pointer (can't be reassigned) // to int (value can be changed) // int * const - typet const_pointer_to_int_type=pointer_typet(non_const_primitive_type); + typet const_pointer_to_int_type=pointer_type(non_const_primitive_type); const_qualifier.write(const_pointer_to_int_type); // pointer (can be reassigned) // to const int (value can't be changed) // const int * - typet pointer_to_const_int_type=pointer_typet(const_primitive_type); + typet pointer_to_const_int_type=pointer_type(const_primitive_type); // constant pointer (can't be reassigned) // to const int (value can't be changed) // const int * const - typet const_pointer_to_const_int_type=pointer_typet(const_primitive_type); + typet const_pointer_to_const_int_type=pointer_type(const_primitive_type); const_qualifier.write(const_pointer_to_const_int_type); WHEN("Comparing int to int") diff --git a/unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp b/unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp index cfb2c647536..a85819bf301 100644 --- a/unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp +++ b/unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp @@ -11,8 +11,10 @@ #include -#include +#include #include +#include + #include #include #include @@ -42,23 +44,23 @@ SCENARIO("is_type_at_least_as_const", // pointer (can be reassigned) // to int (value can be changed) // int * - typet pointer_to_int_type=pointer_typet(non_const_primitive_type); + typet pointer_to_int_type=pointer_type(non_const_primitive_type); // const pointer (can't be reassigned) // to int (value can be changed) // int * const - typet const_pointer_to_int_type=pointer_typet(non_const_primitive_type); + typet const_pointer_to_int_type=pointer_type(non_const_primitive_type); const_qualifier.write(const_pointer_to_int_type); // pointer (can be reassigned) // to const int (value can't be changed) // const int * - typet pointer_to_const_int_type=pointer_typet(const_primitive_type); + typet pointer_to_const_int_type=pointer_type(const_primitive_type); // constant pointer (can't be reassigned) // to const int (value can't be changed) // const int * const - typet const_pointer_to_const_int_type=pointer_typet(const_primitive_type); + typet const_pointer_to_const_int_type=pointer_type(const_primitive_type); const_qualifier.write(const_pointer_to_const_int_type); WHEN("Comparing int to int") From ce863191ba19a365f8d7fc0a38d77f0896600113 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 28 May 2017 19:32:05 +0100 Subject: [PATCH 2/3] pointer types now have width --- src/ansi-c/ansi_c_convert_type.cpp | 7 +++++++ src/ansi-c/c_typecheck_type.cpp | 3 +++ src/cpp/cpp_typecheck_type.cpp | 4 ++++ src/util/c_types.cpp | 4 ++-- 4 files changed, 16 insertions(+), 2 deletions(-) diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp index 1a67c80c4fa..8c2c9d62628 100644 --- a/src/ansi-c/ansi_c_convert_type.cpp +++ b/src/ansi-c/ansi_c_convert_type.cpp @@ -216,6 +216,13 @@ void ansi_c_convert_typet::read_rec(const typet &type) { c_storage_spec.alias=type.subtype().get(ID_value); } + else if(type.id()==ID_pointer) + { + // pointers have a width, much like integers + pointer_typet tmp=to_pointer_type(type); + tmp.set_width(config.ansi_c.pointer_width); + other.push_back(tmp); + } else other.push_back(type); } diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index 393be7dbf54..1a3998de19d 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -76,7 +76,10 @@ void c_typecheck_baset::typecheck_type(typet &type) else if(type.id()==ID_array) typecheck_array_type(to_array_type(type)); else if(type.id()==ID_pointer) + { typecheck_type(type.subtype()); + INVARIANT(!type.get(ID_width).empty(), "pointers must have width"); + } else if(type.id()==ID_struct || type.id()==ID_union) typecheck_compound_type(to_struct_union_type(type)); diff --git a/src/cpp/cpp_typecheck_type.cpp b/src/cpp/cpp_typecheck_type.cpp index 41fcd49b68c..5258633b16e 100644 --- a/src/cpp/cpp_typecheck_type.cpp +++ b/src/cpp/cpp_typecheck_type.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include #include +#include #include @@ -81,6 +82,9 @@ void cpp_typecheckt::typecheck_type(typet &type) // the pointer might have a qualifier, but do subtype first typecheck_type(type.subtype()); + // we add a width, much like with integers + to_pointer_type(type).set_width(config.ansi_c.pointer_width); + // Check if it is a pointer-to-member if(type.find("to-member").is_not_nil()) { diff --git a/src/util/c_types.cpp b/src/util/c_types.cpp index 6c553f5adbc..b02dfdec7e7 100644 --- a/src/util/c_types.cpp +++ b/src/util/c_types.cpp @@ -296,12 +296,12 @@ signedbv_typet pointer_diff_type() pointer_typet pointer_type(const typet &subtype) { - return pointer_typet(subtype); + return pointer_typet(subtype, config.ansi_c.pointer_width); } reference_typet reference_type(const typet &subtype) { - return reference_typet(subtype); + return reference_typet(subtype, config.ansi_c.pointer_width); } typet void_type() From d3c0b5796fc9560bf62e37116764a17872073bae Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 15 Aug 2017 17:37:53 +0100 Subject: [PATCH 3/3] remove legacy constructors --- src/util/std_expr.h | 5 ----- src/util/std_types.h | 22 ---------------------- 2 files changed, 27 deletions(-) diff --git a/src/util/std_expr.h b/src/util/std_expr.h index a0dfbbcb948..3396398e73b 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -2599,11 +2599,6 @@ class address_of_exprt:public unary_exprt { } - address_of_exprt(): - unary_exprt(ID_address_of, pointer_typet()) - { - } - exprt &object() { return op0(); diff --git a/src/util/std_types.h b/src/util/std_types.h index 5c244e6728e..4d4a0763ca8 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -1367,16 +1367,6 @@ inline c_bit_field_typet &to_c_bit_field_type(typet &type) class pointer_typet:public bitvector_typet { public: - pointer_typet():bitvector_typet(ID_pointer) - { - } - - // this one will go away; use the one with width - explicit pointer_typet(const typet &_subtype): - bitvector_typet(ID_pointer, _subtype) - { - } - pointer_typet(const typet &_subtype, std::size_t width): bitvector_typet(ID_pointer, _subtype, width) { @@ -1418,18 +1408,6 @@ inline pointer_typet &to_pointer_type(typet &type) class reference_typet:public pointer_typet { public: - reference_typet() - { - set(ID_C_reference, true); - } - - // this one will go away; use the one with width - explicit reference_typet(const typet &_subtype): - pointer_typet(_subtype) - { - set(ID_C_reference, true); - } - reference_typet(const typet &_subtype, std::size_t _width): pointer_typet(_subtype, _width) {