From fc6120c8f4b1ca8fd06e974bb4e37cf9567af2e6 Mon Sep 17 00:00:00 2001 From: klaas Date: Thu, 28 Jun 2018 12:04:05 -0400 Subject: [PATCH 1/5] Disambiguates two exprts with the same ID. This commit resolves an issue where ID_dynamic_object was used to label two semantically distinct exprts. One, with a single operand, was a boolean expression meaning that the operand is a pointer to a dynamic object. This has been renamed to ID_is_dynamic_object. The second, with two operands, is an exprt representing a dynamic object itself. This has stayed ID_dynamic_object. Disambiguating which meaning was intended in each case was relatively easy, as uses of these exprts frequently come with assertions about the number of operands, and so this was used to inform which instances of ID_dynamic_object should be changed and which should be left the same. --- regression/goto-instrument/slice19/test.desc | 2 +- src/ansi-c/c_typecheck_expr.cpp | 7 ++--- src/ansi-c/expr2c.cpp | 4 +-- src/solvers/flattening/bv_pointers.cpp | 4 +-- src/solvers/smt2/smt2_conv.cpp | 2 +- src/util/irep_ids.def | 1 + src/util/pointer_predicates.cpp | 2 +- src/util/simplify_expr.cpp | 4 +-- src/util/simplify_expr_class.h | 2 +- src/util/simplify_expr_int.cpp | 13 ++++---- src/util/simplify_expr_pointer.cpp | 12 ++++---- src/util/std_expr.h | 32 ++++++++++++++++++++ 12 files changed, 59 insertions(+), 26 deletions(-) diff --git a/regression/goto-instrument/slice19/test.desc b/regression/goto-instrument/slice19/test.desc index 03cff4a4fac..3793f7374e1 100644 --- a/regression/goto-instrument/slice19/test.desc +++ b/regression/goto-instrument/slice19/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --full-slice ^EXIT=0$ diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 40fc7c21b78..02e199dda42 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2165,11 +2165,10 @@ exprt c_typecheck_baset::do_special_functions( throw 0; } - exprt dynamic_object_expr=exprt(ID_dynamic_object, expr.type()); - dynamic_object_expr.operands()=expr.arguments(); - dynamic_object_expr.add_source_location()=source_location; + exprt is_dynamic_object_expr = is_dynamic_object_exprt(expr.arguments()[0]); + is_dynamic_object_expr.add_source_location() = source_location; - return dynamic_object_expr; + return is_dynamic_object_expr; } else if(identifier==CPROVER_PREFIX "POINTER_OFFSET") { diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index a00ee818d62..1684fb5f5ee 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -3486,8 +3486,8 @@ std::string expr2ct::convert_with_precedence( return convert_function( src, CPROVER_PREFIX "invalid_pointer", precedence = 16); - else if(src.id()==ID_dynamic_object) - return convert_function(src, "DYNAMIC_OBJECT", precedence=16); + else if(src.id() == ID_is_dynamic_object) + return convert_function(src, "IS_DYNAMIC_OBJECT", precedence = 16); else if(src.id()=="is_zero_string") return convert_function(src, "IS_ZERO_STRING", precedence=16); diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index 94ae7c9ce3d..83d68804823 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -45,7 +45,7 @@ literalt bv_pointerst::convert_rest(const exprt &expr) } } } - else if(expr.id()==ID_dynamic_object) + else if(expr.id() == ID_is_dynamic_object) { if(operands.size()==1 && operands[0].type().id()==ID_pointer) @@ -728,7 +728,7 @@ void bv_pointerst::add_addr(const exprt &expr, bvt &bv) void bv_pointerst::do_postponed( const postponedt &postponed) { - if(postponed.expr.id() == ID_dynamic_object) + if(postponed.expr.id() == ID_is_dynamic_object) { const pointer_logict::objectst &objects= pointer_logic.objects; diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 2a085fc9891..ce19b1fca29 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -1316,7 +1316,7 @@ void smt2_convt::convert_expr(const exprt &expr) if(ext>0) out << ")"; // zero_extend } - else if(expr.id() == ID_dynamic_object) + else if(expr.id() == ID_is_dynamic_object) { convert_is_dynamic_object(expr); } diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index ca216365e18..0f479a9a211 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -446,6 +446,7 @@ IREP_ID_TWO(overflow_minus, overflow--) IREP_ID_TWO(overflow_mult, overflow-*) IREP_ID_TWO(overflow_unary_minus, overflow-unary-) IREP_ID_ONE(object_descriptor) +IREP_ID_ONE(is_dynamic_object) IREP_ID_ONE(dynamic_object) IREP_ID_TWO(C_dynamic, #dynamic) IREP_ID_ONE(object_size) diff --git a/src/util/pointer_predicates.cpp b/src/util/pointer_predicates.cpp index 0b111fb8f04..72f41505b14 100644 --- a/src/util/pointer_predicates.cpp +++ b/src/util/pointer_predicates.cpp @@ -70,7 +70,7 @@ exprt dynamic_size(const namespacet &ns) exprt dynamic_object(const exprt &pointer) { - exprt dynamic_expr(ID_dynamic_object, bool_typet()); + exprt dynamic_expr(ID_is_dynamic_object, bool_typet()); dynamic_expr.copy_to_operands(pointer); return dynamic_expr; } diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index eed4a723368..be3b8dc9a60 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2403,9 +2403,9 @@ bool simplify_exprt::simplify_node(exprt &expr) result=simplify_byte_extract(to_byte_extract_expr(expr)) && result; else if(expr.id()==ID_pointer_object) result=simplify_pointer_object(expr) && result; - else if(expr.id() == ID_dynamic_object) + else if(expr.id() == ID_is_dynamic_object) { - result = simplify_dynamic_object(expr) && result; + result = simplify_is_dynamic_object(expr) && result; } else if(expr.id()==ID_invalid_pointer) result=simplify_invalid_pointer(expr) && result; diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index 9720d307e2e..da2e029f66a 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -96,7 +96,7 @@ class simplify_exprt bool simplify_pointer_object(exprt &expr); bool simplify_object_size(exprt &expr); bool simplify_dynamic_size(exprt &expr); - bool simplify_dynamic_object(exprt &expr); + bool simplify_is_dynamic_object(exprt &expr); bool simplify_invalid_pointer(exprt &expr); bool simplify_same_object(exprt &expr); bool simplify_good_pointer(exprt &expr); diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index b60b1593355..8efef95340b 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -1686,7 +1686,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr) { if( expr.op0().op0().id() == ID_symbol || - expr.op0().op0().id() == ID_dynamic_object || + expr.op0().op0().id() == ID_is_dynamic_object || expr.op0().op0().id() == ID_member || expr.op0().op0().id() == ID_index || expr.op0().op0().id() == ID_string_constant) @@ -1701,11 +1701,12 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr) expr.op0().op0().id()==ID_address_of && expr.op0().op0().operands().size()==1) { - if(expr.op0().op0().op0().id()==ID_symbol || - expr.op0().op0().op0().id()==ID_dynamic_object || - expr.op0().op0().op0().id()==ID_member || - expr.op0().op0().op0().id()==ID_index || - expr.op0().op0().op0().id()==ID_string_constant) + if( + expr.op0().op0().op0().id() == ID_symbol || + expr.op0().op0().op0().id() == ID_is_dynamic_object || + expr.op0().op0().op0().id() == ID_member || + expr.op0().op0().op0().id() == ID_index || + expr.op0().op0().op0().id() == ID_string_constant) { expr=false_exprt(); return false; diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index b54f51714a6..eecf2f31e21 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -468,7 +468,7 @@ bool simplify_exprt::simplify_inequality_pointer_object(exprt &expr) { if( op.operands().size() != 1 || - (op.op0().id() != ID_symbol && op.op0().id() != ID_dynamic_object && + (op.op0().id() != ID_symbol && op.op0().id() != ID_is_dynamic_object && op.op0().id() != ID_string_constant)) { return true; @@ -515,18 +515,18 @@ bool simplify_exprt::simplify_pointer_object(exprt &expr) return result; } -bool simplify_exprt::simplify_dynamic_object(exprt &expr) +bool simplify_exprt::simplify_is_dynamic_object(exprt &expr) { - if(expr.operands().size()!=1) - return true; + // This should hold as a result of the expr ID being is_dynamic_object. + PRECONDITION(expr.operands().size() == 1); exprt &op=expr.op0(); if(op.id()==ID_if && op.operands().size()==3) { if_exprt if_expr=lift_if(expr, 0); - simplify_dynamic_object(if_expr.true_case()); - simplify_dynamic_object(if_expr.false_case()); + simplify_is_dynamic_object(if_expr.true_case()); + simplify_is_dynamic_object(if_expr.false_case()); simplify_if(if_expr); expr.swap(if_expr); diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 5fc8683a5f4..e9a4aff64ef 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -2103,6 +2103,38 @@ inline dynamic_object_exprt &to_dynamic_object_expr(exprt &expr) return ret; } +/// Evaluates to true if the operand is a pointer to a dynamic object. +class is_dynamic_object_exprt : public unary_predicate_exprt +{ +public: + is_dynamic_object_exprt() : unary_predicate_exprt(ID_is_dynamic_object) + { + } + + explicit is_dynamic_object_exprt(const exprt &op) + : unary_predicate_exprt(ID_is_dynamic_object, op) + { + } +}; + +inline const is_dynamic_object_exprt & +to_is_dynamic_object_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_is_dynamic_object); + DATA_INVARIANT( + expr.operands().size() == 1, "is_dynamic_object must have one operand"); + return static_cast(expr); +} + +/// \copydoc to_is_dynamic_object_expr(const exprt &) +/// \ingroup gr_std_expr +inline is_dynamic_object_exprt &to_is_dynamic_object_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_is_dynamic_object); + DATA_INVARIANT( + expr.operands().size() == 1, "is_dynamic_object must have one operand"); + return static_cast(expr); +} /// \brief Semantic type conversion class typecast_exprt:public unary_exprt From feebc743309d5fa1624cba22b12821db7100a9a8 Mon Sep 17 00:00:00 2001 From: Owen Date: Tue, 2 Apr 2019 15:23:52 +0100 Subject: [PATCH 2/5] Rename ID_invalid_pointer to ID_is_invalid_pointer This is a more accurate name --- src/analyses/goto_check.cpp | 16 ++++++++-------- src/ansi-c/c_typecheck_expr.cpp | 6 +++--- src/ansi-c/cprover_builtin_headers.h | 2 +- src/ansi-c/expr2c.cpp | 8 ++++---- src/solvers/flattening/bv_pointers.cpp | 2 +- src/solvers/smt2/smt2_conv.cpp | 2 +- src/util/irep_ids.def | 2 +- src/util/pointer_predicates.cpp | 6 +++--- src/util/pointer_predicates.h | 2 +- src/util/simplify_expr.cpp | 4 ++-- src/util/simplify_expr_class.h | 2 +- src/util/simplify_expr_pointer.cpp | 2 +- 12 files changed, 27 insertions(+), 27 deletions(-) diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 7a1a8db0e24..c31af84c02b 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -1129,18 +1129,18 @@ goto_checkt::address_check(const exprt &address, const exprt &size) if(flags.is_unknown()) { - conditions.push_back(conditiont( - not_exprt(invalid_pointer(address)), - "pointer invalid")); + conditions.push_back( + conditiont(not_exprt(is_invalid_pointer(address)), "pointer invalid")); } if(flags.is_uninitialized()) { - conditions.push_back(conditiont( - or_exprt( - in_bounds_of_some_explicit_allocation, - not_exprt(invalid_pointer(address))), - "pointer uninitialized")); + conditions.push_back( + conditiont( + or_exprt( + in_bounds_of_some_explicit_allocation, + not_exprt(is_invalid_pointer(address))), + "pointer uninitialized")); } if(flags.is_unknown() || flags.is_dynamic_heap()) diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 02e199dda42..2f76ae70d1d 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2095,16 +2095,16 @@ exprt c_typecheck_baset::do_special_functions( return std::move(get_may_expr); } - else if(identifier==CPROVER_PREFIX "invalid_pointer") + else if(identifier == CPROVER_PREFIX "is_invalid_pointer") { if(expr.arguments().size()!=1) { error().source_location = f_op.source_location(); - error() << "invalid_pointer expects one operand" << eom; + error() << "is_invalid_pointer expects one operand" << eom; throw 0; } - exprt same_object_expr = invalid_pointer(expr.arguments().front()); + exprt same_object_expr = is_invalid_pointer(expr.arguments().front()); same_object_expr.add_source_location()=source_location; return same_object_expr; diff --git a/src/ansi-c/cprover_builtin_headers.h b/src/ansi-c/cprover_builtin_headers.h index 14f282af610..9bacbeb3794 100644 --- a/src/ansi-c/cprover_builtin_headers.h +++ b/src/ansi-c/cprover_builtin_headers.h @@ -5,7 +5,7 @@ void __CPROVER_precondition(__CPROVER_bool precondition, const char *description void __CPROVER_havoc_object(void *); __CPROVER_bool __CPROVER_equal(); __CPROVER_bool __CPROVER_same_object(const void *, const void *); -__CPROVER_bool __CPROVER_invalid_pointer(const void *); +__CPROVER_bool __CPROVER_is_invalid_pointer(const void *); __CPROVER_bool __CPROVER_is_zero_string(const void *); __CPROVER_size_t __CPROVER_zero_string_length(const void *); __CPROVER_size_t __CPROVER_buffer_size(const void *); diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 1684fb5f5ee..5ecf655e77e 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -3426,8 +3426,8 @@ std::string expr2ct::convert_with_precedence( else if(src.id() == ID_w_ok) return convert_function(src, "W_OK", precedence = 16); - else if(src.id()==ID_invalid_pointer) - return convert_function(src, "INVALID-POINTER", precedence=16); + else if(src.id() == ID_is_invalid_pointer) + return convert_function(src, "IS-INVALID-POINTER", precedence = 16); else if(src.id()==ID_good_pointer) return convert_function(src, "GOOD_POINTER", precedence=16); @@ -3482,9 +3482,9 @@ std::string expr2ct::convert_with_precedence( else if(src.id()=="pointer_cons") return convert_function(src, "POINTER_CONS", precedence=16); - else if(src.id()==ID_invalid_pointer) + else if(src.id() == ID_is_invalid_pointer) return convert_function( - src, CPROVER_PREFIX "invalid_pointer", precedence = 16); + src, CPROVER_PREFIX "is_invalid_pointer", precedence = 16); else if(src.id() == ID_is_dynamic_object) return convert_function(src, "IS_DYNAMIC_OBJECT", precedence = 16); diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index 83d68804823..6a61d2fa345 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -20,7 +20,7 @@ literalt bv_pointerst::convert_rest(const exprt &expr) const exprt::operandst &operands=expr.operands(); - if(expr.id()==ID_invalid_pointer) + if(expr.id() == ID_is_invalid_pointer) { if(operands.size()==1 && operands[0].type().id()==ID_pointer) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index ce19b1fca29..efd3519349a 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -1320,7 +1320,7 @@ void smt2_convt::convert_expr(const exprt &expr) { convert_is_dynamic_object(expr); } - else if(expr.id()==ID_invalid_pointer) + else if(expr.id() == ID_is_invalid_pointer) { DATA_INVARIANT( expr.operands().size() == 1, diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 0f479a9a211..7962b69722a 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -217,7 +217,7 @@ IREP_ID_ONE(invalid) IREP_ID_TWO(C_invalid_object, #invalid_object) IREP_ID_ONE(pointer_offset) IREP_ID_ONE(pointer_object) -IREP_ID_TWO(invalid_pointer, invalid-pointer) +IREP_ID_TWO(is_invalid_pointer, is-invalid-pointer) IREP_ID_ONE(ieee_float_equal) IREP_ID_ONE(ieee_float_notequal) IREP_ID_ONE(isnan) diff --git a/src/util/pointer_predicates.cpp b/src/util/pointer_predicates.cpp index 72f41505b14..0c66b8b578c 100644 --- a/src/util/pointer_predicates.cpp +++ b/src/util/pointer_predicates.cpp @@ -105,7 +105,7 @@ exprt good_pointer_def( const not_exprt not_null(null_pointer(pointer)); - const not_exprt not_invalid(invalid_pointer(pointer)); + const not_exprt not_invalid(is_invalid_pointer(pointer)); const or_exprt bad_other( object_lower_bound(pointer, nil_exprt()), @@ -139,9 +139,9 @@ exprt null_pointer(const exprt &pointer) return same_object(pointer, null_pointer); } -exprt invalid_pointer(const exprt &pointer) +exprt is_invalid_pointer(const exprt &pointer) { - return unary_exprt(ID_invalid_pointer, pointer, bool_typet()); + return unary_exprt(ID_is_invalid_pointer, pointer, bool_typet()); } exprt dynamic_object_lower_bound( diff --git a/src/util/pointer_predicates.h b/src/util/pointer_predicates.h index 2771d52f31c..f1d76f7ef53 100644 --- a/src/util/pointer_predicates.h +++ b/src/util/pointer_predicates.h @@ -32,7 +32,7 @@ exprt good_pointer_def(const exprt &pointer, const namespacet &); exprt null_object(const exprt &pointer); exprt null_pointer(const exprt &pointer); exprt integer_address(const exprt &pointer); -exprt invalid_pointer(const exprt &pointer); +exprt is_invalid_pointer(const exprt &pointer); exprt dynamic_object_lower_bound( const exprt &pointer, const exprt &offset); diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index be3b8dc9a60..40f417c1c81 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2407,8 +2407,8 @@ bool simplify_exprt::simplify_node(exprt &expr) { result = simplify_is_dynamic_object(expr) && result; } - else if(expr.id()==ID_invalid_pointer) - result=simplify_invalid_pointer(expr) && result; + else if(expr.id() == ID_is_invalid_pointer) + result = simplify_is_invalid_pointer(expr) && result; else if(expr.id()==ID_object_size) result=simplify_object_size(expr) && result; else if(expr.id()==ID_good_pointer) diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index da2e029f66a..83a73929d63 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -97,7 +97,7 @@ class simplify_exprt bool simplify_object_size(exprt &expr); bool simplify_dynamic_size(exprt &expr); bool simplify_is_dynamic_object(exprt &expr); - bool simplify_invalid_pointer(exprt &expr); + bool simplify_is_invalid_pointer(exprt &expr); bool simplify_same_object(exprt &expr); bool simplify_good_pointer(exprt &expr); bool simplify_object(exprt &expr); diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index eecf2f31e21..2efdd4cf791 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -571,7 +571,7 @@ bool simplify_exprt::simplify_is_dynamic_object(exprt &expr) return result; } -bool simplify_exprt::simplify_invalid_pointer(exprt &expr) +bool simplify_exprt::simplify_is_invalid_pointer(exprt &expr) { if(expr.operands().size()!=1) return true; From 53e9e6b7355100c7a7904ac3d1897e6fa9624ab7 Mon Sep 17 00:00:00 2001 From: Owen Date: Tue, 2 Apr 2019 15:33:36 +0100 Subject: [PATCH 3/5] Create is_invalid_pointer_exprt class --- src/util/pointer_predicates.cpp | 2 +- src/util/pointer_predicates.h | 15 +++++++++++---- 2 files changed, 12 insertions(+), 5 deletions(-) diff --git a/src/util/pointer_predicates.cpp b/src/util/pointer_predicates.cpp index 0c66b8b578c..2c77beda391 100644 --- a/src/util/pointer_predicates.cpp +++ b/src/util/pointer_predicates.cpp @@ -141,7 +141,7 @@ exprt null_pointer(const exprt &pointer) exprt is_invalid_pointer(const exprt &pointer) { - return unary_exprt(ID_is_invalid_pointer, pointer, bool_typet()); + return is_invalid_pointer_exprt{pointer}; } exprt dynamic_object_lower_bound( diff --git a/src/util/pointer_predicates.h b/src/util/pointer_predicates.h index f1d76f7ef53..d0a5b124e42 100644 --- a/src/util/pointer_predicates.h +++ b/src/util/pointer_predicates.h @@ -12,11 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_POINTER_PREDICATES_H #define CPROVER_UTIL_POINTER_PREDICATES_H -#define SYMEX_DYNAMIC_PREFIX "symex_dynamic::" +#include "std_expr.h" -class exprt; -class namespacet; -class typet; +#define SYMEX_DYNAMIC_PREFIX "symex_dynamic::" exprt same_object(const exprt &p1, const exprt &p2); exprt deallocated(const exprt &pointer, const namespacet &); @@ -47,4 +45,13 @@ exprt object_upper_bound( const exprt &pointer, const exprt &access_size); +class is_invalid_pointer_exprt : public unary_predicate_exprt +{ +public: + explicit is_invalid_pointer_exprt(exprt pointer) + : unary_predicate_exprt{ID_is_invalid_pointer, std::move(pointer)} + { + } +}; + #endif // CPROVER_UTIL_POINTER_PREDICATES_H From 4f3eea0b789f2811d3b797481776a4ea4337d0d7 Mon Sep 17 00:00:00 2001 From: Owen Date: Tue, 2 Apr 2019 15:36:33 +0100 Subject: [PATCH 4/5] Use is_invalid_pointer_exprt directly --- src/analyses/goto_check.cpp | 12 +++++------- src/ansi-c/c_typecheck_expr.cpp | 2 +- src/util/pointer_predicates.cpp | 7 +------ src/util/pointer_predicates.h | 1 - 4 files changed, 7 insertions(+), 15 deletions(-) diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index c31af84c02b..9f1fc15813f 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -1129,18 +1129,16 @@ goto_checkt::address_check(const exprt &address, const exprt &size) if(flags.is_unknown()) { - conditions.push_back( - conditiont(not_exprt(is_invalid_pointer(address)), "pointer invalid")); + conditions.push_back(conditiont{ + not_exprt{is_invalid_pointer_exprt{address}}, "pointer invalid"}); } if(flags.is_uninitialized()) { conditions.push_back( - conditiont( - or_exprt( - in_bounds_of_some_explicit_allocation, - not_exprt(is_invalid_pointer(address))), - "pointer uninitialized")); + conditiont{or_exprt{in_bounds_of_some_explicit_allocation, + not_exprt{is_invalid_pointer_exprt{address}}}, + "pointer uninitialized"}); } if(flags.is_unknown() || flags.is_dynamic_heap()) diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 2f76ae70d1d..2999043e7d9 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2104,7 +2104,7 @@ exprt c_typecheck_baset::do_special_functions( throw 0; } - exprt same_object_expr = is_invalid_pointer(expr.arguments().front()); + exprt same_object_expr = is_invalid_pointer_exprt{expr.arguments().front()}; same_object_expr.add_source_location()=source_location; return same_object_expr; diff --git a/src/util/pointer_predicates.cpp b/src/util/pointer_predicates.cpp index 2c77beda391..9fbe79d6435 100644 --- a/src/util/pointer_predicates.cpp +++ b/src/util/pointer_predicates.cpp @@ -105,7 +105,7 @@ exprt good_pointer_def( const not_exprt not_null(null_pointer(pointer)); - const not_exprt not_invalid(is_invalid_pointer(pointer)); + const not_exprt not_invalid{is_invalid_pointer_exprt{pointer}}; const or_exprt bad_other( object_lower_bound(pointer, nil_exprt()), @@ -139,11 +139,6 @@ exprt null_pointer(const exprt &pointer) return same_object(pointer, null_pointer); } -exprt is_invalid_pointer(const exprt &pointer) -{ - return is_invalid_pointer_exprt{pointer}; -} - exprt dynamic_object_lower_bound( const exprt &pointer, const exprt &offset) diff --git a/src/util/pointer_predicates.h b/src/util/pointer_predicates.h index d0a5b124e42..53be205d81c 100644 --- a/src/util/pointer_predicates.h +++ b/src/util/pointer_predicates.h @@ -30,7 +30,6 @@ exprt good_pointer_def(const exprt &pointer, const namespacet &); exprt null_object(const exprt &pointer); exprt null_pointer(const exprt &pointer); exprt integer_address(const exprt &pointer); -exprt is_invalid_pointer(const exprt &pointer); exprt dynamic_object_lower_bound( const exprt &pointer, const exprt &offset); From a9774ca9693696540cfb5d28a4e5999debe14c2b Mon Sep 17 00:00:00 2001 From: Owen Date: Tue, 2 Apr 2019 15:41:42 +0100 Subject: [PATCH 5/5] Use underscores instead of hyphens This matches the things around it better. --- src/ansi-c/expr2c.cpp | 2 +- src/util/irep_ids.def | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 5ecf655e77e..da3e16c4d11 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -3427,7 +3427,7 @@ std::string expr2ct::convert_with_precedence( return convert_function(src, "W_OK", precedence = 16); else if(src.id() == ID_is_invalid_pointer) - return convert_function(src, "IS-INVALID-POINTER", precedence = 16); + return convert_function(src, "IS_INVALID_POINTER", precedence = 16); else if(src.id()==ID_good_pointer) return convert_function(src, "GOOD_POINTER", precedence=16); diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 7962b69722a..0082f423b66 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -217,7 +217,7 @@ IREP_ID_ONE(invalid) IREP_ID_TWO(C_invalid_object, #invalid_object) IREP_ID_ONE(pointer_offset) IREP_ID_ONE(pointer_object) -IREP_ID_TWO(is_invalid_pointer, is-invalid-pointer) +IREP_ID_ONE(is_invalid_pointer) IREP_ID_ONE(ieee_float_equal) IREP_ID_ONE(ieee_float_notequal) IREP_ID_ONE(isnan)