diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 8a93f58d6d4..653083fcf07 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -32,6 +33,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "anonymous_member.h" #include "padding.h" +bool is_lvalue(const exprt &expr); + void c_typecheck_baset::typecheck_expr(exprt &expr) { if(expr.id()==ID_already_typechecked) @@ -2085,6 +2088,47 @@ exprt c_typecheck_baset::do_special_functions( return same_object_expr; } + else if(identifier == CPROVER_PREFIX "points_to_valid_memory") + { + if(expr.arguments().size()!=2) + { + err_location(f_op); + error() << "points_to_valid_memory expects two operands" << eom; + throw 0; + } + if(!is_lvalue(expr.arguments().front())) + { + err_location(f_op); + error() << "ptr argument to points_to_valid_memory" + << " must be an lvalue" << eom; + throw 0; + } + + exprt same_object_expr; + if(expr.arguments().size() == 2) + { + // TODO: We should add some way to enforce that the second argument + // has a reasonable type (coercible to __CPROVER_size_t). +#if 0 + if(expr.arguments()[1].type() <[cannot be coerced to size_t]>) + { + err_location(f_op); + error() << "size argument to points_to_valid_memory" + << " must be coercible to size_t" << eom; + throw 0; + } +#endif + same_object_expr = + points_to_valid_memory(expr.arguments()[0], expr.arguments()[1]); + } + else + { + UNREACHABLE; + } + same_object_expr.add_source_location()=source_location; + + return same_object_expr; + } else if(identifier==CPROVER_PREFIX "buffer_size") { if(expr.arguments().size()!=1) diff --git a/src/ansi-c/cprover_builtin_headers.h b/src/ansi-c/cprover_builtin_headers.h index 0b05aa245e7..4d9b6740d66 100644 --- a/src/ansi-c/cprover_builtin_headers.h +++ b/src/ansi-c/cprover_builtin_headers.h @@ -6,6 +6,7 @@ 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_points_to_valid_memory(const void *, __CPROVER_size_t); __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 2f91ac42e00..305e4d88d42 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -3521,6 +3521,9 @@ std::string expr2ct::convert_with_precedence( else if(src.id()==ID_good_pointer) return convert_function(src, "GOOD_POINTER", precedence=16); + else if(src.id()==ID_points_to_valid_memory) + return convert_function(src, "POINTS_TO_VALID_MEMORY", precedence=16); + else if(src.id()==ID_object_size) return convert_function(src, "OBJECT_SIZE", precedence=16); diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index 87885153a33..8c0b5eb710c 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -32,6 +32,7 @@ SRC = accelerate/accelerate.cpp \ document_properties.cpp \ dot.cpp \ dump_c.cpp \ + expand_pointer_predicates.cpp \ full_slicer.cpp \ function.cpp \ function_modifies.cpp \ diff --git a/src/goto-instrument/expand_pointer_predicates.cpp b/src/goto-instrument/expand_pointer_predicates.cpp new file mode 100644 index 00000000000..9958692e956 --- /dev/null +++ b/src/goto-instrument/expand_pointer_predicates.cpp @@ -0,0 +1,220 @@ +/*******************************************************************\ + +Module: Expand pointer predicates in assertions/assumptions. + +Author: Klaas Pruiksma + +Date: June 2018 + +\*******************************************************************/ + +/// \file +/// Replace pointer predicates (e.g. __CPROVER_points_to_valid_memory) +/// in assumptions and assertions with suitable expressions and additional +/// instructions. + +#include "expand_pointer_predicates.h" + +#include + +#include +#include +#include +#include +#include +#include +#include +#include + +#include + +class expand_pointer_predicatest +{ +public: + expand_pointer_predicatest( + symbol_tablet &_symbol_table, + goto_functionst &_goto_functions): + ns(_symbol_table), + symbol_table(_symbol_table), + goto_functions(_goto_functions), + local_bitvector_analysis(nullptr) + { + } + + void operator()(); + +protected: + namespacet ns; + symbol_tablet &symbol_table; + goto_functionst &goto_functions; + local_bitvector_analysist *local_bitvector_analysis; + + void expand_pointer_predicates(); + + void expand_assumption( + goto_programt &program, + goto_programt::targett target, + exprt &assume_expr); + + void expand_assertion(exprt &assert_expr); + + const symbolt &new_tmp_symbol( + const typet &type, + const source_locationt &source_location); +}; + +bool is_lvalue(const exprt &expr); + +void expand_pointer_predicatest::expand_pointer_predicates() +{ + Forall_goto_functions(f_it, goto_functions) + { + goto_functionst::goto_functiont &goto_function = f_it->second; + local_bitvector_analysist local_bitvector_analysis_obj(goto_function); + local_bitvector_analysis = &local_bitvector_analysis_obj; + Forall_goto_program_instructions(i_it, goto_function.body) + { + if(i_it->is_assert()) + { + expand_assertion(i_it->guard); + } + else if(i_it->is_assume()) + { + expand_assumption( + goto_function.body, + i_it, + i_it->guard); + local_bitvector_analysis_obj = + local_bitvector_analysist(goto_function); + local_bitvector_analysis = &local_bitvector_analysis_obj; + } + else + { + continue; + } + } + } +} + +void expand_pointer_predicatest::expand_assumption( + goto_programt &program, + goto_programt::targett target, + exprt &assume_expr) +{ + goto_programt assume_code; + for(depth_iteratort it=assume_expr.depth_begin(); + it != assume_expr.depth_end();) + { + if(it->id() == ID_points_to_valid_memory) + { + exprt &valid_memory_expr = it.mutate(); + exprt &pointer_expr = valid_memory_expr.op0(); + exprt size_expr = valid_memory_expr.op1(); + simplify(size_expr, ns); + + // This should be forced by typechecking. + INVARIANT(pointer_expr.type().id() == ID_pointer && + is_lvalue(pointer_expr), + "Invalid argument to valid_pointer."); + + local_bitvector_analysist::flagst flags = + local_bitvector_analysis->get(target, pointer_expr); + // Only create a new object if the pointer may be uninitialized. + if(flags.is_uninitialized() || flags.is_unknown()) + { + typet object_type = type_from_size(size_expr, ns); + + // Decl a new variable (which is therefore unconstrained) + goto_programt::targett d = assume_code.add_instruction(DECL); + d->function = target->function; + d->source_location = assume_expr.source_location(); + const symbol_exprt obj = + new_tmp_symbol(object_type, d->source_location).symbol_expr(); + d->code=code_declt(obj); + + exprt rhs; + if(object_type.id() == ID_array) + { + rhs = typecast_exprt( + address_of_exprt( + index_exprt(obj, from_integer(0, index_type()))), + pointer_expr.type()); + } + else + { + rhs = address_of_exprt(obj); + } + + // Point the relevant pointer to the new object + goto_programt::targett a = assume_code.add_instruction(ASSIGN); + a->function = target->function; + a->source_location = assume_expr.source_location(); + a->code = code_assignt(pointer_expr, rhs); + a->code.add_source_location() = assume_expr.source_location(); + } + + // Because some uses of this occur before deallocated, dead, and malloc + // objects are initialized, we need to make some additional assumptions + // to clarify that our newly allocated object is not dead, deallocated, + // or outside the bounds of a malloc region. + + exprt check_expr = + points_to_valid_memory_def(pointer_expr, size_expr, ns); + valid_memory_expr.swap(check_expr); + it.next_sibling_or_parent(); + } + else { + ++it; + } + } + + program.destructive_insert(target, assume_code); +} + +void expand_pointer_predicatest::expand_assertion(exprt &assert_expr) +{ + for(depth_iteratort it = assert_expr.depth_begin(); + it != assert_expr.depth_end();) + { + if(it->id() == ID_points_to_valid_memory) + { + // Build an expression that checks validity. + exprt &valid_memory_expr = it.mutate(); + exprt &pointer_expr = valid_memory_expr.op0(); + exprt &size_expr = valid_memory_expr.op1(); + + exprt check_expr = + points_to_valid_memory_def(pointer_expr, size_expr, ns); + valid_memory_expr.swap(check_expr); + it.next_sibling_or_parent(); + } + else + { + ++it; + } + } +} + +const symbolt &expand_pointer_predicatest::new_tmp_symbol( + const typet &type, + const source_locationt &source_location) +{ + return get_fresh_aux_symbol( + type, + id2string(source_location.get_function()), + "tmp_epp", + source_location, + ID_C, + symbol_table); +} + +void expand_pointer_predicatest::operator()() +{ + expand_pointer_predicates(); +} + +void expand_pointer_predicates(goto_modelt &goto_model) +{ + expand_pointer_predicatest(goto_model.symbol_table, + goto_model.goto_functions)(); +} diff --git a/src/goto-instrument/expand_pointer_predicates.h b/src/goto-instrument/expand_pointer_predicates.h new file mode 100644 index 00000000000..37d41d1023b --- /dev/null +++ b/src/goto-instrument/expand_pointer_predicates.h @@ -0,0 +1,23 @@ +/*******************************************************************\ + +Module: Expand pointer predicates in assertions/assumptions. + +Author: Klaas Pruiksma + +Date: June 2018 + +\*******************************************************************/ + +/// \file +/// Replace pointer predicates (e.g. __CPROVER_points_to_valid_memory) +/// in assumptions and assertions with suitable expressions and additional +/// instructions. + +#ifndef CPROVER_GOTO_INSTRUMENT_EXPAND_POINTER_PREDICATES_H +#define CPROVER_GOTO_INSTRUMENT_EXPAND_POINTER_PREDICATES_H + +class goto_modelt; + +void expand_pointer_predicates(goto_modelt &goto_model); + +#endif // CPROVER_GOTO_INSTRUMENT_EXPAND_POINTER_PREDICATES_H diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 4582509df7d..197b1eb730c 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -76,6 +76,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "document_properties.h" #include "dot.h" #include "dump_c.h" +#include "expand_pointer_predicates.h" #include "full_slicer.h" #include "function.h" #include "havoc_loops.h" @@ -1053,6 +1054,11 @@ void goto_instrument_parse_optionst::instrument_goto_program() code_contracts(goto_model); } + if(cmdline.isset("expand-pointer-predicates")) + { + expand_pointer_predicates(goto_model); + } + // replace function pointers, if explicitly requested if(cmdline.isset("remove-function-pointers")) { @@ -1622,6 +1628,7 @@ void goto_instrument_parse_optionst::help() " --no-caching disable caching of intermediate results during transitive function inlining\n" // NOLINT(*) " --log log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*) " --remove-function-pointers replace function pointers by case statement over function calls\n" // NOLINT(*) + " --expand-pointer-predicates Expands predicates about pointers (e.g. __CPROVER_points_to_valid_memory) into a form useable by CBMC\n" // NOLINT(*) HELP_REMOVE_CALLS_NO_BODY HELP_REMOVE_CONST_FUNCTION_POINTERS " --add-library add models of C library functions\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 706083df63e..fcc72f04a24 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -88,6 +88,7 @@ Author: Daniel Kroening, kroening@kroening.com "(list-symbols)(list-undefined-functions)" \ "(z3)(add-library)(show-dependence-graph)" \ "(horn)(skip-loops):(apply-code-contracts)(model-argc-argv):" \ + "(expand-pointer-predicates)" \ "(show-threaded)(list-calls-args)" \ "(undefined-function-is-assume-false)" \ "(remove-function-body):"\ diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index cbe45869e06..0d258c3cb6b 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -615,20 +616,6 @@ void goto_convertt::do_array_op( copy(array_op_statement, OTHER, dest); } -bool is_lvalue(const exprt &expr) -{ - if(expr.id()==ID_index) - return is_lvalue(to_index_expr(expr).op0()); - else if(expr.id()==ID_member) - return is_lvalue(to_member_expr(expr).op0()); - else if(expr.id()==ID_dereference) - return true; - else if(expr.id()==ID_symbol) - return true; - else - return false; -} - exprt make_va_list(const exprt &expr) { // we first strip any typecast diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index 34a26fa1846..05d5374c55f 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -14,32 +14,12 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include #include -inline static typet c_sizeof_type_rec(const exprt &expr) -{ - const irept &sizeof_type=expr.find(ID_C_c_sizeof_type); - - if(!sizeof_type.is_nil()) - { - return static_cast(sizeof_type); - } - else if(expr.id()==ID_mult) - { - forall_operands(it, expr) - { - typet t=c_sizeof_type_rec(*it); - if(t.is_not_nil()) - return t; - } - } - - return nil_typet(); -} - void goto_symext::symex_allocate( statet &state, const exprt &lhs, @@ -66,62 +46,12 @@ void goto_symext::symex_allocate( } else { - exprt tmp_size=size; + exprt tmp_size = size; state.rename(tmp_size, ns); // to allow constant propagation - simplify(tmp_size, ns); - - // special treatment for sizeof(T)*x - { - typet tmp_type=c_sizeof_type_rec(tmp_size); - - if(tmp_type.is_not_nil()) - { - // Did the size get multiplied? - mp_integer elem_size=pointer_offset_size(tmp_type, ns); - mp_integer alloc_size; - - if(elem_size<0) - { - } - else if(to_integer(tmp_size, alloc_size) && - tmp_size.id()==ID_mult && - tmp_size.operands().size()==2 && - (tmp_size.op0().is_constant() || - tmp_size.op1().is_constant())) - { - exprt s=tmp_size.op0(); - if(s.is_constant()) - { - s=tmp_size.op1(); - PRECONDITION(c_sizeof_type_rec(tmp_size.op0()) == tmp_type); - } - else - PRECONDITION(c_sizeof_type_rec(tmp_size.op1()) == tmp_type); - - object_type=array_typet(tmp_type, s); - } - else - { - if(alloc_size==elem_size) - object_type=tmp_type; - else - { - mp_integer elements=alloc_size/elem_size; - - if(elements*elem_size==alloc_size) - object_type=array_typet( - tmp_type, from_integer(elements, tmp_size.type())); - } - } - } - } - - if(object_type.is_nil()) - object_type=array_typet(unsigned_char_type(), tmp_size); + object_type = type_from_size(tmp_size, ns); // we introduce a fresh symbol for the size // to prevent any issues of the size getting ever changed - if(object_type.id()==ID_array && !to_array_type(object_type).size().is_constant()) { diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp index 8d3c3ca3d59..869bc09e06a 100644 --- a/src/util/expr_util.cpp +++ b/src/util/expr_util.cpp @@ -10,15 +10,115 @@ Author: Daniel Kroening, kroening@kroening.com #include "expr_util.h" #include +#include "c_types.h" #include "expr.h" #include "expr_iterator.h" #include "fixedbv.h" #include "ieee_float.h" +#include "simplify_expr.h" #include "std_expr.h" #include "symbol.h" #include "namespace.h" +#include "pointer_offset_size.h" #include "arith_tools.h" +inline static typet c_sizeof_type_rec(const exprt &expr) +{ + const irept &sizeof_type=expr.find(ID_C_c_sizeof_type); + + if(!sizeof_type.is_nil()) + { + return static_cast(sizeof_type); + } + else if(expr.id()==ID_mult) + { + forall_operands(it, expr) + { + typet t=c_sizeof_type_rec(*it); + if(t.is_not_nil()) + return t; + } + } + + return nil_typet(); +} + +typet type_from_size(const exprt &size, const namespacet &ns) +{ + exprt tmp_size = size; + simplify(tmp_size, ns); + typet tmp_type=c_sizeof_type_rec(tmp_size); + + // Default to char[size] if nothing better can be found. + typet result_type = array_typet(unsigned_char_type(), tmp_size); + + if(tmp_type.is_not_nil()) + { + // Did the size get multiplied? + mp_integer elem_size=pointer_offset_size(tmp_type, ns); + mp_integer alloc_size; + + if(elem_size<0) + { + // If this occurs, then either tmp_type contains some type with invalid + // ID or tmp_type contains a bitvector of negative size. Neither of these + // should ever happen, and if one does, it suggests a failure in CBMC + // rather than a failure on the part of the user. + UNREACHABLE; + } + // Case for constant size (in case it is a multiple of the element size) + else if(!to_integer(tmp_size, alloc_size)) + { + if(alloc_size==elem_size) + { + result_type=tmp_type; + } + else if((alloc_size / elem_size) * elem_size == alloc_size) + { + // Allocation size is a multiple of the element size + result_type=array_typet( + tmp_type, from_integer(alloc_size / elem_size, tmp_size.type())); + } + } + // Special case for constant * sizeof + else if(tmp_size.id() == ID_mult && + tmp_size.operands().size() == 2 && + (tmp_size.op0().is_constant() || + tmp_size.op1().is_constant())) + { + exprt s = tmp_size.op0(); + if(s.is_constant()) + { + s=tmp_size.op1(); + PRECONDITION(c_sizeof_type_rec(tmp_size.op0()) == tmp_type); + } + else + { + PRECONDITION(c_sizeof_type_rec(tmp_size.op1()) == tmp_type); + } + + result_type = array_typet(tmp_type, s); + } + } + + POSTCONDITION(result_type.is_not_nil()); + return result_type; +} + +bool is_lvalue(const exprt &expr) +{ + if(expr.id()==ID_index) + return is_lvalue(to_index_expr(expr).array()); + else if(expr.id()==ID_member) + return is_lvalue(to_member_expr(expr).compound()); + else if(expr.id()==ID_dereference) + return true; + else if(expr.id()==ID_symbol) + return true; + else + return false; +} + exprt make_binary(const exprt &expr) { const exprt::operandst &operands=expr.operands(); diff --git a/src/util/expr_util.h b/src/util/expr_util.h index 5c7d37b0b95..9572dc243cd 100644 --- a/src/util/expr_util.h +++ b/src/util/expr_util.h @@ -30,6 +30,21 @@ class symbolt; class typet; class namespacet; +/// Creates a type with size (in bytes) equal to the size argument. +/// Makes use of sizeof() in the argument to avoid unnecessary use of byte +/// arrays. +/// \param size: An expression describing the size (in bytes) of the desired +/// type. +/// \param ns : A namespace for symbol type lookups. +/// \return A type with size given by the argument \a size. +/// If \a size is of the form n*sizeof(T) (or sizeof(T)*n), then this +/// type will be T[n]. If \a size is of the form sizeof(T), then this +/// type will be T. Otherwise, the type will be unsigned char[size]. +typet type_from_size(const exprt &size, const namespacet &ns); + +/// Returns true iff the argument is (syntactically) an lvalue. +bool is_lvalue(const exprt &expr); + /// splits an expression with >=3 operands into nested binary expressions exprt make_binary(const exprt &); diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index fcda57ce383..67015daaf32 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -222,6 +222,7 @@ 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_ONE(points_to_valid_memory) 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 668054bc493..2018f1f3390 100644 --- a/src/util/pointer_predicates.cpp +++ b/src/util/pointer_predicates.cpp @@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "cprover_prefix.h" #include "namespace.h" #include "pointer_offset_size.h" +#include "simplify_expr.h" #include "std_expr.h" #include "symbol.h" @@ -143,6 +144,59 @@ exprt invalid_pointer(const exprt &pointer) return unary_exprt(ID_invalid_pointer, pointer, bool_typet()); } +exprt points_to_valid_memory(const exprt &pointer, const exprt &size) +{ + return binary_exprt(pointer, ID_points_to_valid_memory, size, bool_typet()); +} + +exprt points_to_valid_memory_def( + const exprt &pointer, + const exprt &size, + const namespacet &ns) +{ + const not_exprt not_null(null_pointer(pointer)); + + const not_exprt not_deallocated(deallocated(pointer, ns)); + + const not_exprt not_dead(dead_object(pointer, ns)); + + const not_exprt not_invalid(invalid_pointer(pointer)); + + const or_exprt malloc_in_bounds( + not_exprt(malloc_object(pointer, ns)), + and_exprt( + not_exprt(dynamic_object_lower_bound( + pointer, + ns, + nil_exprt())), + not_exprt(dynamic_object_upper_bound( + pointer, + ns, + size)))); + + const or_exprt dynamic_in_bounds( + dynamic_object(pointer), + and_exprt( + not_exprt(object_lower_bound( + pointer, + ns, + nil_exprt())), + not_exprt(object_upper_bound( + pointer, + ns, + size)))); + + exprt check_expr = conjunction({ + not_null, + not_deallocated, + not_dead, + not_invalid, + malloc_in_bounds, + dynamic_in_bounds}); + + return simplify_expr(check_expr, ns); +} + exprt dynamic_object_lower_bound( const exprt &pointer, const namespacet &ns, diff --git a/src/util/pointer_predicates.h b/src/util/pointer_predicates.h index f83588df8fe..dfdfb63afe6 100644 --- a/src/util/pointer_predicates.h +++ b/src/util/pointer_predicates.h @@ -31,6 +31,11 @@ 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 points_to_valid_memory(const exprt &pointer, const exprt &size); +exprt points_to_valid_memory_def( + const exprt &pointer, + const exprt &size, + const namespacet &); exprt dynamic_object_lower_bound( const exprt &pointer, const namespacet &,