diff --git a/regression/contracts/argument_sanity/main.c b/regression/contracts/argument_sanity/main.c new file mode 100644 index 00000000000..742b16a4e7e --- /dev/null +++ b/regression/contracts/argument_sanity/main.c @@ -0,0 +1,5 @@ +int main() +{ + int *r; + __CPROVER_points_to_valid_memory(r, "huh?"); +} diff --git a/regression/contracts/argument_sanity/main.mod b/regression/contracts/argument_sanity/main.mod new file mode 100644 index 00000000000..f74debcaba5 Binary files /dev/null and b/regression/contracts/argument_sanity/main.mod differ diff --git a/regression/contracts/argument_sanity/test.desc b/regression/contracts/argument_sanity/test.desc new file mode 100644 index 00000000000..c78b9571c16 --- /dev/null +++ b/regression/contracts/argument_sanity/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--apply-code-contracts +^EXIT=1$ +^SIGNAL=0$ +^main.c:\d+:\d+: error: size argument to points_to_valid_memory must be coercible to size_t$ +^CONVERSION ERROR$ +-- +-- diff --git a/regression/goto-instrument/expand-pointer-predicates1/main.c b/regression/goto-instrument/expand-pointer-predicates1/main.c new file mode 100644 index 00000000000..acf68d8fa87 --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates1/main.c @@ -0,0 +1,7 @@ +int main() +{ + int *x; + __CPROVER_assume(__CPROVER_points_to_valid_memory(x)); + *x = 1; + return 0; +} diff --git a/regression/goto-instrument/expand-pointer-predicates1/test.desc b/regression/goto-instrument/expand-pointer-predicates1/test.desc new file mode 100644 index 00000000000..c28c5c3d48b --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--pointer-check --expand-pointer-predicates +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/regression/goto-instrument/expand-pointer-predicates2/main.c b/regression/goto-instrument/expand-pointer-predicates2/main.c new file mode 100644 index 00000000000..8205fbd42e0 --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates2/main.c @@ -0,0 +1,7 @@ +int main() +{ + int *x; + __CPROVER_assume(__CPROVER_points_to_valid_memory(x, sizeof(int))); + *x = 1; + return 0; +} diff --git a/regression/goto-instrument/expand-pointer-predicates2/test.desc b/regression/goto-instrument/expand-pointer-predicates2/test.desc new file mode 100644 index 00000000000..c28c5c3d48b --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates2/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--pointer-check --expand-pointer-predicates +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/regression/goto-instrument/expand-pointer-predicates3/main.c b/regression/goto-instrument/expand-pointer-predicates3/main.c new file mode 100644 index 00000000000..f4f7ce609dd --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates3/main.c @@ -0,0 +1,8 @@ +int main() +{ + int *x; + __CPROVER_assume(__CPROVER_points_to_valid_memory(x, sizeof(int))); + __CPROVER_assert( + __CPROVER_points_to_valid_memory(x, sizeof(int)), "Assert matches assume"); + return 0; +} diff --git a/regression/goto-instrument/expand-pointer-predicates3/test.desc b/regression/goto-instrument/expand-pointer-predicates3/test.desc new file mode 100644 index 00000000000..c28c5c3d48b --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates3/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--pointer-check --expand-pointer-predicates +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/regression/goto-instrument/expand-pointer-predicates4/main.c b/regression/goto-instrument/expand-pointer-predicates4/main.c new file mode 100644 index 00000000000..a4c9c33cfa8 --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates4/main.c @@ -0,0 +1,7 @@ +int main() +{ + int x; + int *y = &x; + __CPROVER_assert(__CPROVER_points_to_valid_memory(y), "Assert works on &"); + return 0; +} diff --git a/regression/goto-instrument/expand-pointer-predicates4/test.desc b/regression/goto-instrument/expand-pointer-predicates4/test.desc new file mode 100644 index 00000000000..c28c5c3d48b --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates4/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--pointer-check --expand-pointer-predicates +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/regression/goto-instrument/expand-pointer-predicates5/main.c b/regression/goto-instrument/expand-pointer-predicates5/main.c new file mode 100644 index 00000000000..9e898c16e14 --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates5/main.c @@ -0,0 +1,19 @@ +struct bar +{ + int w; + int x; + int y; + int z; +}; + +int main() +{ + struct bar s; + s.z = 5; + int *x_pointer = &(s.x); + __CPROVER_assert( + __CPROVER_points_to_valid_memory(x_pointer, 3 * sizeof(int)), + "Variable length assert"); + assert(x_pointer[2] == 5); + return 0; +} diff --git a/regression/goto-instrument/expand-pointer-predicates5/test.desc b/regression/goto-instrument/expand-pointer-predicates5/test.desc new file mode 100644 index 00000000000..f64909c5e27 --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates5/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--pointer-check --expand-pointer-predicates +^\[main.assertion.1\] line \d+ Variable length assert: SUCCESS$ +^\[main.assertion.2\] line \d+ assertion x_pointer\[\(signed long( long)? int\)2\] == 5: SUCCESS$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/regression/goto-instrument/expand-pointer-predicates6/main.c b/regression/goto-instrument/expand-pointer-predicates6/main.c new file mode 100644 index 00000000000..a8b4931a4b1 --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates6/main.c @@ -0,0 +1,21 @@ +#include + +struct my_struct +{ + int *field1; + int *field2; +}; + +void example(struct my_struct *s) +{ + s->field2 = malloc(sizeof(*(s->field2))); +} + +int main() +{ + struct my_struct *s; + __CPROVER_assume(__CPROVER_points_to_valid_memory(s)); + example(s); + __CPROVER_assert(__CPROVER_points_to_valid_memory(s->field2), ""); + return 0; +} diff --git a/regression/goto-instrument/expand-pointer-predicates6/test.desc b/regression/goto-instrument/expand-pointer-predicates6/test.desc new file mode 100644 index 00000000000..2456c5f7d92 --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates6/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--pointer-check --expand-pointer-predicates +^\[main.assertion.1\] line \d+ assertion: SUCCESS$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/regression/goto-instrument/expand-pointer-predicates7/main.c b/regression/goto-instrument/expand-pointer-predicates7/main.c new file mode 100644 index 00000000000..5f18fb9fa1f --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates7/main.c @@ -0,0 +1,22 @@ +#include + +struct my_struct +{ + int *field; +}; + +void example(struct my_struct *s) +{ + __CPROVER_assume(__CPROVER_points_to_valid_memory(s)); + size_t size; + __CPROVER_assume(size == sizeof(*(s->field))); + __CPROVER_assume(__CPROVER_points_to_valid_memory(s->field, size)); + int read = *(s->field); +} + +int main() +{ + struct my_struct *s; + example(s); + return 0; +} diff --git a/regression/goto-instrument/expand-pointer-predicates7/test.desc b/regression/goto-instrument/expand-pointer-predicates7/test.desc new file mode 100644 index 00000000000..c28c5c3d48b --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates7/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--pointer-check --expand-pointer-predicates +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/regression/goto-instrument/expand-pointer-predicates8/main.c b/regression/goto-instrument/expand-pointer-predicates8/main.c new file mode 100644 index 00000000000..766ea1525f9 --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates8/main.c @@ -0,0 +1,16 @@ +#include + +int main() +{ + int *x; + int *y; + __CPROVER_assume(__CPROVER_points_to_valid_memory(x, 2 * sizeof(int))); + __CPROVER_assume(__CPROVER_points_to_valid_memory(y, 2 * sizeof(int) - 1)); + (void)(x[0]); // Should succeed + (void)(x[1]); // Should succeed + (void)(x[2]); // Should fail + (void)(x[-1]); // Should fail + (void)(y[0]); // Should succeed + (void)(y[1]); // Should fail + return 0; +} diff --git a/regression/goto-instrument/expand-pointer-predicates8/test.desc b/regression/goto-instrument/expand-pointer-predicates8/test.desc new file mode 100644 index 00000000000..cffb9599ada --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates8/test.desc @@ -0,0 +1,16 @@ +CORE +main.c +--pointer-check --expand-pointer-predicates +^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: dead object in x\[\(signed long( long)? int\)0\]: SUCCESS$ +^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)0\]: SUCCESS$ +^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)1\]: SUCCESS$ +^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)2\]: FAILURE$ +^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)-1\]: FAILURE$ +^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: dead object in y\[\(signed long( long)? int\)0\]: SUCCESS$ +^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: pointer outside object bounds in y\[\(signed long( long)? int\)0\]: SUCCESS$ +^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: pointer outside object bounds in y\[\(signed long( long)? int\)1\]: FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/regression/goto-instrument/expand-pointer-predicates9/main.c b/regression/goto-instrument/expand-pointer-predicates9/main.c new file mode 100644 index 00000000000..bb80cf4c996 --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates9/main.c @@ -0,0 +1,11 @@ +#include + +int main() +{ + char *x; + __CPROVER_assume(__CPROVER_points_to_valid_memory(x)); + (void)(*x); // Should succeed + (void)(*(x + 1)); // Should fail + (void)(*(x - 1)); // Should fail + return 0; +} diff --git a/regression/goto-instrument/expand-pointer-predicates9/test.desc b/regression/goto-instrument/expand-pointer-predicates9/test.desc new file mode 100644 index 00000000000..4c8dde65ec2 --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates9/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--pointer-check --expand-pointer-predicates +^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: dead object in \*x: SUCCESS$ +^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: pointer outside object bounds in \*x: SUCCESS$ +^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)1\]: FAILURE$ +^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: pointer outside object bounds in \*\(x - \(signed long( long)? int\)1\): FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 40fc7c21b78..a97d46659e4 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -34,6 +34,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) @@ -2109,6 +2111,63 @@ 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 && expr.arguments().size() != 1) + { + error().source_location = f_op.source_location(); + error() << "points_to_valid_memory expects one or two operands" << eom; + throw 0; + } + if(!is_lvalue(expr.arguments().front())) + { + error().source_location = f_op.source_location(); + error() << "ptr argument to points_to_valid_memory" + << " must be an lvalue" << eom; + throw 0; + } + + exprt same_object_expr; + if(expr.arguments().size() == 2) + { + if( + expr.arguments()[1].type().id() != ID_unsignedbv && + expr.arguments()[1].type().id() != ID_signedbv) + { + error().source_location = f_op.source_location(); + error() << "size argument to points_to_valid_memory" + << " must be coercible to size_t" << eom; + throw 0; + } + same_object_expr = + points_to_valid_memory(expr.arguments()[0], expr.arguments()[1]); + } + else if(expr.arguments().size() == 1) + { + PRECONDITION(expr.arguments()[0].type().id() == ID_pointer); + + const typet &base_type = expr.arguments()[0].type().subtype(); + auto expr_size = size_of_expr(base_type, *this); + if(!expr_size) + { + error().source_location = expr.source_location(); + error() << "cannot determine size of pointed-to memory region" << eom; + throw 0; + } + + expr_size->add(ID_C_c_sizeof_type) = base_type; + + same_object_expr = + points_to_valid_memory(expr.arguments()[0], *expr_size); + } + 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 14f282af610..a8fb4272163 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_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 a00ee818d62..b68ed81018f 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -3432,6 +3432,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 8dc28944f66..04c393eb75a 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..c9e866eec89 --- /dev/null +++ b/src/goto-instrument/expand_pointer_predicates.cpp @@ -0,0 +1,211 @@ +/*******************************************************************\ + +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_functionst::goto_functiont &, + 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; + 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, i_it, i_it->guard); + } + else + { + continue; + } + } + } +} + +void expand_pointer_predicatest::expand_assumption( + goto_functionst::goto_functiont &goto_function, + goto_programt::targett target, + exprt &assume_expr) +{ + goto_programt &program = goto_function.body; + local_bitvector_analysist local_bitvector_analysis(goto_function, ns); + 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->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->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 1b868cdce13..15574ba15c0 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -82,6 +82,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" @@ -1068,6 +1069,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")) { @@ -1665,6 +1671,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 647ec904b0b..3ba111b923d 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -93,6 +93,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-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index 105f4fe5ba8..b38e4cadf7d 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -23,27 +24,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -inline static optionalt 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) - { - const auto t = c_sizeof_type_rec(*it); - if(t.has_value()) - return t; - } - } - - return {}; -} - void goto_symext::symex_allocate( statet &state, const exprt &lhs, @@ -74,54 +54,7 @@ void goto_symext::symex_allocate( // to allow constant propagation exprt tmp_size = state.rename(size, ns); simplify(tmp_size, ns); - - // special treatment for sizeof(T)*x - { - const auto tmp_type = c_sizeof_type_rec(tmp_size); - - if(tmp_type.has_value()) - { - // Did the size get multiplied? - auto elem_size = pointer_offset_size(*tmp_type, ns); - const auto alloc_size = numeric_cast(tmp_size); - - if(!elem_size.has_value() || *elem_size==0) - { - } - else if( - !alloc_size.has_value() && 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.has_value()) - { - 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.has_value()) - 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 diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp index acb9dc99dbf..349434baa2c 100644 --- a/src/util/expr_util.cpp +++ b/src/util/expr_util.cpp @@ -8,17 +8,102 @@ Author: Daniel Kroening, kroening@kroening.com #include "expr_util.h" -#include -#include - +#include "arith_tools.h" +#include "c_types.h" #include "expr.h" #include "expr_iterator.h" #include "fixedbv.h" #include "ieee_float.h" +#include "namespace.h" +#include "pointer_offset_size.h" +#include "simplify_expr.h" #include "std_expr.h" #include "symbol.h" -#include "namespace.h" -#include "arith_tools.h" +#include +#include + +inline static optionalt 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) + { + const auto t = c_sizeof_type_rec(*it); + if(t.has_value()) + return t; + } + } + + return {}; +} + +typet type_from_size(const exprt &size, const namespacet &ns) +{ + auto tmp_type = c_sizeof_type_rec(size); + + // Default to char[size] if nothing better can be found. + typet result_type = array_typet(unsigned_char_type(), size); + + if(tmp_type.has_value()) + { + // Did the size get multiplied? + auto elem_size = pointer_offset_size(*tmp_type, ns); + const auto alloc_size = numeric_cast(size); + + if(!elem_size.has_value() || *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; + } + else if(*elem_size == 0) + { + } + // Case for constant size (in case it is a multiple of the element size) + else if(alloc_size.has_value()) + { + 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, size.type())); + } + } + // Special case for constant * sizeof + else if( + size.id() == ID_mult && size.operands().size() == 2 && + (size.op0().is_constant() || size.op1().is_constant())) + { + exprt s = size.op0(); + if(s.is_constant()) + { + s = size.op1(); + PRECONDITION(c_sizeof_type_rec(size.op0()) == tmp_type); + } + else + { + PRECONDITION(c_sizeof_type_rec(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) { @@ -33,6 +118,7 @@ bool is_lvalue(const exprt &expr) 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 bc0b5099071..122ca212029 100644 --- a/src/util/expr_util.h +++ b/src/util/expr_util.h @@ -30,6 +30,18 @@ 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); diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index ca216365e18..f6f0c4f7272 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -218,6 +218,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 0b111fb8f04..b88a2254cde 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" @@ -144,6 +145,46 @@ 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, 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, nil_exprt())), + not_exprt(object_upper_bound(pointer, 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 exprt &offset) diff --git a/src/util/pointer_predicates.h b/src/util/pointer_predicates.h index 2771d52f31c..a0118f5b412 100644 --- a/src/util/pointer_predicates.h +++ b/src/util/pointer_predicates.h @@ -33,6 +33,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 exprt &offset);