From 42b70b26c470c700588ce6bffda408a8d3df6189 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 10 Sep 2024 12:31:59 +0000 Subject: [PATCH 1/2] Move is_null_pointer to constant_exprt Removes one of the functions from the expr_util translation unit that is supposed to be deprecated. --- src/analyses/custom_bitvector_analysis.cpp | 6 +++--- src/analyses/invariant_set.cpp | 2 +- src/ansi-c/c_typecheck_expr.cpp | 4 ++-- src/ansi-c/expr2c.cpp | 3 +-- src/cpp/cpp_typecheck_conversions.cpp | 2 +- src/cprover/bv_pointers_wide.cpp | 2 +- src/goto-instrument/dump_c.cpp | 4 ++-- src/goto-instrument/goto_program2code.cpp | 2 +- src/goto-programs/xml_expr.cpp | 3 +-- src/goto-symex/shadow_memory_util.cpp | 4 +--- src/goto-symex/symex_goto.cpp | 2 +- src/goto-synthesizer/cegis_verifier.cpp | 2 +- src/pointer-analysis/value_set.cpp | 3 +-- src/pointer-analysis/value_set_fi.cpp | 3 +-- src/solvers/flattening/bv_pointers.cpp | 3 +-- src/solvers/smt2/smt2_conv.cpp | 2 +- .../smt2_incremental/convert_expr_to_smt.cpp | 3 +-- src/util/arith_tools.cpp | 2 +- src/util/expr_util.cpp | 17 +-------------- src/util/expr_util.h | 2 ++ src/util/format_expr.cpp | 2 +- src/util/simplify_expr.cpp | 2 +- src/util/simplify_expr_int.cpp | 8 +++---- src/util/simplify_expr_pointer.cpp | 8 +++---- src/util/simplify_utils.cpp | 2 +- src/util/std_expr.cpp | 21 +++++++++++++++++++ src/util/std_expr.h | 5 +++++ 27 files changed, 62 insertions(+), 57 deletions(-) diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp index 7687ee51e5c..a6d252f99e6 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/src/analyses/custom_bitvector_analysis.cpp @@ -349,7 +349,7 @@ void custom_bitvector_domaint::transform( { if( lhs.is_constant() && - is_null_pointer(to_constant_expr(lhs))) // NULL means all + to_constant_expr(lhs).is_null_pointer()) // NULL means all { if(mode==modet::CLEAR_MAY) { @@ -478,7 +478,7 @@ void custom_bitvector_domaint::transform( { if( lhs.is_constant() && - is_null_pointer(to_constant_expr(lhs))) // NULL means all + to_constant_expr(lhs).is_null_pointer()) // NULL means all { if(mode==modet::CLEAR_MAY) { @@ -716,7 +716,7 @@ exprt custom_bitvector_domaint::eval( if( pointer.is_constant() && - is_null_pointer(to_constant_expr(pointer))) // NULL means all + to_constant_expr(pointer).is_null_pointer()) // NULL means all { if(src.id() == ID_get_may) { diff --git a/src/analyses/invariant_set.cpp b/src/analyses/invariant_set.cpp index 49c3c8b2324..f05476766e7 100644 --- a/src/analyses/invariant_set.cpp +++ b/src/analyses/invariant_set.cpp @@ -121,7 +121,7 @@ std::string inv_object_storet::build_string(const exprt &expr) const if(expr.is_constant()) { // NULL? - if(is_null_pointer(to_constant_expr(expr))) + if(to_constant_expr(expr).is_null_pointer()) return "0"; const auto i = numeric_cast(expr); diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 5e398ab2698..35bc45cb257 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -1672,13 +1672,13 @@ void c_typecheck_baset::typecheck_expr_trinary(if_exprt &expr) // (at least that's how GCC behaves) if( to_pointer_type(operands[1].type()).base_type().id() == ID_empty && - tmp1.is_constant() && is_null_pointer(to_constant_expr(tmp1))) + tmp1.is_constant() && to_constant_expr(tmp1).is_null_pointer()) { implicit_typecast(operands[1], operands[2].type()); } else if( to_pointer_type(operands[2].type()).base_type().id() == ID_empty && - tmp2.is_constant() && is_null_pointer(to_constant_expr(tmp2))) + tmp2.is_constant() && to_constant_expr(tmp2).is_null_pointer()) { implicit_typecast(operands[2], operands[1].type()); } diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 3257a74f270..07003ead306 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -1983,7 +1982,7 @@ std::string expr2ct::convert_constant( } else if(type.id()==ID_pointer) { - if(is_null_pointer(src)) + if(src.is_null_pointer()) { if(configuration.use_library_macros) dest = "NULL"; diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp index 41ec14ef5c2..b7df8895878 100644 --- a/src/cpp/cpp_typecheck_conversions.cpp +++ b/src/cpp/cpp_typecheck_conversions.cpp @@ -603,7 +603,7 @@ bool cpp_typecheckt::standard_conversion_pointer_to_member( if(expr.get_bool(ID_C_lvalue)) return false; - if(expr.is_constant() && is_null_pointer(to_constant_expr(expr))) + if(expr.is_constant() && to_constant_expr(expr).is_null_pointer()) { new_expr = typecast_exprt::conditional_cast(expr, type); return true; diff --git a/src/cprover/bv_pointers_wide.cpp b/src/cprover/bv_pointers_wide.cpp index 8cb9e7b46a3..9197306f0b1 100644 --- a/src/cprover/bv_pointers_wide.cpp +++ b/src/cprover/bv_pointers_wide.cpp @@ -387,7 +387,7 @@ bvt bv_pointers_widet::convert_pointer_type(const exprt &expr) { const constant_exprt &c = to_constant_expr(expr); - if(is_null_pointer(c)) + if(c.is_null_pointer()) return encode(pointer_logic.get_null_object(), type); else { diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index 8f6800b35b8..6b2ee20f07d 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -1399,7 +1399,7 @@ void dump_ct::cleanup_expr(exprt &expr) } // add a typecast for NULL else if( - u.op().is_constant() && is_null_pointer(to_constant_expr(u.op())) && + u.op().is_constant() && to_constant_expr(u.op()).is_null_pointer() && to_pointer_type(u.op().type()).base_type().id() == ID_empty) { const struct_union_typet::componentt &comp= @@ -1459,7 +1459,7 @@ void dump_ct::cleanup_expr(exprt &expr) // add a typecast for NULL or 0 if( argument.is_constant() && - is_null_pointer(to_constant_expr(argument))) + to_constant_expr(argument).is_null_pointer()) { const typet &comp_type= to_union_type(type).components().front().type(); diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index 94c3351236d..6f18202d305 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -311,7 +311,7 @@ goto_programt::const_targett goto_program2codet::convert_assign_varargs( const exprt this_va_list_expr = target->assign_lhs(); const exprt &r = skip_typecast(target->assign_rhs()); - if(r.is_constant() && is_null_pointer(to_constant_expr(r))) + if(r.is_constant() && to_constant_expr(r).is_null_pointer()) { code_function_callt f( symbol_exprt("va_end", code_typet({}, empty_typet())), diff --git a/src/goto-programs/xml_expr.cpp b/src/goto-programs/xml_expr.cpp index da90516dace..a07ce2cbe21 100644 --- a/src/goto-programs/xml_expr.cpp +++ b/src/goto-programs/xml_expr.cpp @@ -16,7 +16,6 @@ Author: Daniel Kroening #include #include #include -#include #include #include #include @@ -221,7 +220,7 @@ xmlt xml(const exprt &expr, const namespacet &ns) result.name = "pointer"; result.set_attribute( "binary", integer2binary(bvrep2integer(value, width, false), width)); - if(is_null_pointer(constant_expr)) + if(constant_expr.is_null_pointer()) result.data = "NULL"; } else if(type.id() == ID_bool) diff --git a/src/goto-symex/shadow_memory_util.cpp b/src/goto-symex/shadow_memory_util.cpp index b86a725b067..ebc6dde0867 100644 --- a/src/goto-symex/shadow_memory_util.cpp +++ b/src/goto-symex/shadow_memory_util.cpp @@ -319,9 +319,7 @@ bool contains_null_or_invalid( const std::vector &value_set, const exprt &address) { - if( - address.id() == ID_constant && address.type().id() == ID_pointer && - to_constant_expr(address).is_zero()) + if(address.is_constant() && to_constant_expr(address).is_null_pointer()) { for(const auto &e : value_set) { diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 404f04fec72..4e8d8523d68 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -91,7 +91,7 @@ static std::optional> try_evaluate_pointer_comparison( if( skip_typecast(other_operand).id() != ID_address_of && - (!constant_expr || !is_null_pointer(*constant_expr))) + (!constant_expr || !constant_expr->is_null_pointer())) { return {}; } diff --git a/src/goto-synthesizer/cegis_verifier.cpp b/src/goto-synthesizer/cegis_verifier.cpp index dd32b5eec57..5c4e91ebfc9 100644 --- a/src/goto-synthesizer/cegis_verifier.cpp +++ b/src/goto-synthesizer/cegis_verifier.cpp @@ -71,7 +71,7 @@ get_checked_pointer_from_null_pointer_check(const exprt &violation) // NULL == ptr if( can_cast_expr(lhs_pointer) && - is_null_pointer(*expr_try_dynamic_cast(lhs_pointer))) + expr_try_dynamic_cast(lhs_pointer)->is_null_pointer()) { return rhs_pointer; } diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index fca7edf08d0..b2d7a4fd867 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -621,7 +620,7 @@ void value_sett::get_value_set_rec( else if(expr.is_constant()) { // check if NULL - if(is_null_pointer(to_constant_expr(expr))) + if(to_constant_expr(expr).is_null_pointer()) { insert( dest, diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index 5d595cccb4b..bf634d07264 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -532,7 +531,7 @@ void value_set_fit::get_value_set_rec( else if(expr.is_constant()) { // check if NULL - if(is_null_pointer(to_constant_expr(expr))) + if(to_constant_expr(expr).is_null_pointer()) { insert( dest, diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index a022801df4b..931ad4a0634 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -443,7 +442,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr) { const constant_exprt &c = to_constant_expr(expr); - if(is_null_pointer(c)) + if(c.is_null_pointer()) return encode(pointer_logic.get_null_object(), type); else { diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index b5c5366658c..0269cf67e69 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -3379,7 +3379,7 @@ void smt2_convt::convert_constant(const constant_exprt &expr) } else if(expr_type.id()==ID_pointer) { - if(is_null_pointer(expr)) + if(expr.is_null_pointer()) { out << "(_ bv0 " << boolbv_width(expr_type) << ")"; diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index dc4efc6fb3d..614a3659319 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -6,7 +6,6 @@ #include #include #include -#include #include #include #include @@ -329,7 +328,7 @@ struct sort_based_literal_convertert : public smt_sort_const_downcast_visitort static smt_termt convert_expr_to_smt(const constant_exprt &constant_literal) { - if(is_null_pointer(constant_literal)) + if(constant_literal.is_null_pointer()) { const size_t bit_width = type_checked_cast(constant_literal.type()).get_width(); diff --git a/src/util/arith_tools.cpp b/src/util/arith_tools.cpp index 4b14ec6ec7f..87babfb8b68 100644 --- a/src/util/arith_tools.cpp +++ b/src/util/arith_tools.cpp @@ -25,7 +25,7 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value) if(type_id==ID_pointer) { - if(is_null_pointer(expr)) + if(expr.is_null_pointer()) { int_value=0; return false; diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp index 7e4739a7372..e272918c364 100644 --- a/src/util/expr_util.cpp +++ b/src/util/expr_util.cpp @@ -369,20 +369,5 @@ exprt make_and(exprt a, exprt b) bool is_null_pointer(const constant_exprt &expr) { - if(expr.type().id() != ID_pointer) - return false; - - if(expr.get_value() == ID_NULL) - return true; - - // We used to support "0" (when NULL_is_zero), but really front-ends should - // resolve this and generate ID_NULL instead. -#if 0 - return config.ansi_c.NULL_is_zero && expr.value_is_zero_string(); -#else - INVARIANT( - !expr.value_is_zero_string() || !config.ansi_c.NULL_is_zero, - "front-end should use ID_NULL"); - return false; -#endif + return expr.is_null_pointer(); } diff --git a/src/util/expr_util.h b/src/util/expr_util.h index b423dcdd9fb..eefe6903f37 100644 --- a/src/util/expr_util.h +++ b/src/util/expr_util.h @@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com * \date Sun Jul 31 21:54:44 BST 2011 */ +#include "deprecate.h" #include "irep.h" #include @@ -116,6 +117,7 @@ exprt make_and(exprt a, exprt b); /// Returns true if \p expr has a pointer type and a value NULL; it also returns /// true when \p expr has value zero and NULL_is_zero is true; returns false in /// all other cases. +DEPRECATED(SINCE(2024, 9, 10, "use constant_exprt::is_null_pointer() instead")) bool is_null_pointer(const constant_exprt &expr); #endif // CPROVER_UTIL_EXPR_UTIL_H diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp index 582edeaa093..bd9b2f70e3c 100644 --- a/src/util/format_expr.cpp +++ b/src/util/format_expr.cpp @@ -194,7 +194,7 @@ static std::ostream &format_rec(std::ostream &os, const constant_exprt &src) return os << ieee_floatt(src); else if(type == ID_pointer) { - if(is_null_pointer(src)) + if(src.is_null_pointer()) return os << ID_NULL; else if( src.get_value() == "INVALID" || src.get_value().starts_with("INVALID-")) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 266de986ac4..af6f3c55186 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -906,7 +906,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr) (op_plus_expr.op0().id() == ID_typecast && to_typecast_expr(op_plus_expr.op0()).op().is_zero()) || (op_plus_expr.op0().is_constant() && - is_null_pointer(to_constant_expr(op_plus_expr.op0())))) + to_constant_expr(op_plus_expr.op0()).is_null_pointer())) { auto sub_size = pointer_offset_size(to_pointer_type(op_type).base_type(), ns); diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 473f75bb450..2087564a387 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -1538,8 +1538,8 @@ static bool eliminate_common_addends(exprt &op0, exprt &op1) // we can't eliminate zeros if( op0.is_zero() || op1.is_zero() || - (op0.is_constant() && is_null_pointer(to_constant_expr(op0))) || - (op1.is_constant() && is_null_pointer(to_constant_expr(op1)))) + (op0.is_constant() && to_constant_expr(op0).is_null_pointer()) || + (op1.is_constant() && to_constant_expr(op1).is_null_pointer())) { return true; } @@ -1736,7 +1736,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_rhs_is_constant( const constant_exprt &op1_constant = to_constant_expr(expr.op1()); - if(is_null_pointer(op1_constant)) + if(op1_constant.is_null_pointer()) { // the address of an object is never NULL @@ -1799,7 +1799,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_rhs_is_constant( exprt ptr = simplify_object(expr.op0()).expr; // NULL + N == NULL is N == 0 - if(ptr.is_constant() && is_null_pointer(to_constant_expr(ptr))) + if(ptr.is_constant() && to_constant_expr(ptr).is_null_pointer()) return make_boolean_expr(offset.is_zero()); // &x + N == NULL is false when the offset is in bounds else if(auto address_of = expr_try_dynamic_cast(ptr)) diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index 1511717dd94..0b83e117456 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -38,7 +38,7 @@ static bool is_dereference_integer_object( { const constant_exprt &constant = to_constant_expr(pointer); - if(is_null_pointer(constant)) + if(constant.is_null_pointer()) { address=0; return true; @@ -398,7 +398,7 @@ simplify_exprt::simplify_pointer_offset(const pointer_offset_exprt &expr) { const constant_exprt &c_ptr = to_constant_expr(ptr); - if(is_null_pointer(c_ptr)) + if(c_ptr.is_null_pointer()) { return from_integer(0, expr.type()); } @@ -571,7 +571,7 @@ simplify_exprt::simplify_is_dynamic_object(const unary_exprt &expr) } // NULL is not dynamic - if(op.is_constant() && is_null_pointer(to_constant_expr(op))) + if(op.is_constant() && to_constant_expr(op).is_null_pointer()) return false_exprt(); // &something depends on the something @@ -619,7 +619,7 @@ simplify_exprt::simplify_is_invalid_pointer(const unary_exprt &expr) } // NULL is not invalid - if(op.is_constant() && is_null_pointer(to_constant_expr(op))) + if(op.is_constant() && to_constant_expr(op).is_null_pointer()) { return false_exprt(); } diff --git a/src/util/simplify_utils.cpp b/src/util/simplify_utils.cpp index 3b61acd4d08..624d43e3f22 100644 --- a/src/util/simplify_utils.cpp +++ b/src/util/simplify_utils.cpp @@ -439,7 +439,7 @@ expr2bits(const exprt &expr, bool little_endian, const namespacet &ns) } else if(type.id() == ID_pointer) { - if(config.ansi_c.NULL_is_zero && is_null_pointer(to_constant_expr(expr))) + if(config.ansi_c.NULL_is_zero && to_constant_expr(expr).is_null_pointer()) return std::string(to_bitvector_type(type).get_width(), '0'); else return {}; diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp index 50cb5684220..0a3b94b6fb6 100644 --- a/src/util/std_expr.cpp +++ b/src/util/std_expr.cpp @@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "std_expr.h" +#include "config.h" #include "namespace.h" #include "pointer_expr.h" #include "range.h" @@ -21,6 +22,26 @@ bool constant_exprt::value_is_zero_string() const return val.find_first_not_of('0')==std::string::npos; } +bool constant_exprt::is_null_pointer() const +{ + if(type().id() != ID_pointer) + return false; + + if(get_value() == ID_NULL) + return true; + + // We used to support "0" (when NULL_is_zero), but really front-ends should + // resolve this and generate ID_NULL instead. +#if 0 + return config.ansi_c.NULL_is_zero && value_is_zero_string(); +#else + INVARIANT( + !value_is_zero_string() || !config.ansi_c.NULL_is_zero, + "front-end should use ID_NULL"); + return false; +#endif +} + void constant_exprt::check(const exprt &expr, const validation_modet vm) { nullary_exprt::check(expr, vm); diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 431de0bfa00..e27e5b5f1e9 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -3004,6 +3004,11 @@ class constant_exprt : public nullary_exprt bool value_is_zero_string() const; + /// Returns true if \p expr has a pointer type and a value NULL; it also + /// returns true when \p expr has value zero and NULL_is_zero is true; returns + /// false in all other cases. + bool is_null_pointer() const; + static void check( const exprt &expr, const validation_modet vm = validation_modet::INVARIANT); From 7b47e9f7ba88870c5b100558f56ae87adb004844 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 10 Sep 2024 14:55:22 +0000 Subject: [PATCH 2/2] is_null_pointer: remove code path that is no longer necessary It seems all front-ends have been updated. --- src/util/std_expr.cpp | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp index 0a3b94b6fb6..1da4141bd14 100644 --- a/src/util/std_expr.cpp +++ b/src/util/std_expr.cpp @@ -30,16 +30,12 @@ bool constant_exprt::is_null_pointer() const if(get_value() == ID_NULL) return true; - // We used to support "0" (when NULL_is_zero), but really front-ends should - // resolve this and generate ID_NULL instead. -#if 0 - return config.ansi_c.NULL_is_zero && value_is_zero_string(); -#else + // We used to support "0" (when NULL_is_zero), but really front-ends should + // resolve this and generate ID_NULL instead. INVARIANT( !value_is_zero_string() || !config.ansi_c.NULL_is_zero, "front-end should use ID_NULL"); return false; -#endif } void constant_exprt::check(const exprt &expr, const validation_modet vm)