From aa163190aed4410ddf4d85c3a98e1e0feb22eeb4 Mon Sep 17 00:00:00 2001 From: klaas Date: Mon, 18 Jun 2018 17:09:40 -0400 Subject: [PATCH 01/16] Adds --expand-pointer-predicates to goto-instrument The --expand-pointer-predicates pass resolves pointer predicates (util/pointer_predicates.{cpp, h}) which have side effects and so require expanding into multiple instructions. Currently, the only such predicate that needs to be expanded is __CPROVER_points_to_valid_memory (name subject to change). The __CPROVER_points_to_valid_memory predicates takes two parameters, a pointer and a size. Semantically, __CPROVER_points_to_valid_memory(p, size) should be true if and only if p points to a memory object which is valid to read/write for at least size bytes past p. When used in assertions, this will be checked in a similar manner to how --pointer-check checks validity of a dereference. When used in assumptions, this predicate creates (if none exists already) an object for p to refer to, using local_bitvector_analysis to make that determination, and then makes assumptions (again corresponding to the assertions made by --pointer-check) about that object. --- src/ansi-c/c_typecheck_expr.cpp | 43 ++++ src/ansi-c/cprover_builtin_headers.h | 1 + src/ansi-c/expr2c.cpp | 3 + src/goto-instrument/Makefile | 1 + .../expand_pointer_predicates.cpp | 215 ++++++++++++++++++ .../expand_pointer_predicates.h | 23 ++ .../goto_instrument_parse_options.cpp | 7 + .../goto_instrument_parse_options.h | 1 + src/goto-symex/symex_builtin_functions.cpp | 76 +------ src/util/expr_util.cpp | 95 +++++++- src/util/expr_util.h | 12 + src/util/irep_ids.def | 1 + src/util/pointer_predicates.cpp | 42 ++++ src/util/pointer_predicates.h | 5 + 14 files changed, 447 insertions(+), 78 deletions(-) create mode 100644 src/goto-instrument/expand_pointer_predicates.cpp create mode 100644 src/goto-instrument/expand_pointer_predicates.h diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index b42818006aa..f8257f494d3 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -33,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) @@ -2128,6 +2130,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) + { + error().source_location = f_op.source_location(); + error() << "points_to_valid_memory expects 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) + { +// 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 14f282af610..d0c642f948e 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 5b4ca270dd7..d574c539d6f 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -3474,6 +3474,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 c2bb06a36d0..941c8fd35a6 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..248adc66260 --- /dev/null +++ b/src/goto-instrument/expand_pointer_predicates.cpp @@ -0,0 +1,215 @@ +/*******************************************************************\ + +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 f4b29d43e02..022ed724c77 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" @@ -1079,6 +1080,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")) { @@ -1669,6 +1675,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 a5179302446..cbf49345e6f 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -91,6 +91,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 b9bdf010261..8b9f3f75913 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 @@ -21,27 +22,6 @@ Author: Daniel Kroening, kroening@kroening.com #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, @@ -69,62 +49,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? - auto elem_size = pointer_offset_size(tmp_type, ns); - mp_integer alloc_size; - - if(!elem_size.has_value() || *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 b94d1ae2e8a..22897defbbe 100644 --- a/src/util/expr_util.cpp +++ b/src/util/expr_util.cpp @@ -8,17 +8,101 @@ 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 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? + optionalt elem_size = pointer_offset_size(tmp_type, ns); + mp_integer alloc_size; + + if(!elem_size || *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) { @@ -33,6 +117,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 b6fd76a8855..8798f7758f3 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -219,6 +219,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 93fb6f45c34..a28d252a511 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,47 @@ 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 &, From dc583e622cc40c15723b8e6764ae98e6ac6cb2e7 Mon Sep 17 00:00:00 2001 From: klaas Date: Mon, 30 Jul 2018 14:33:13 -0400 Subject: [PATCH 02/16] Adds a one-argument points_to_valid_memory This commit adds support for a one-argument form of __CPROVER_points_to_valid_memory, taking only a pointer, with no size. If ptr has type T*, then __CPROVER_points_to_valid_memory(ptr) is equivalent to __CPROVER_points_to_valid_memory(ptr, sizeof(T)). --- src/ansi-c/c_typecheck_expr.cpp | 15 +++++++++++++-- src/ansi-c/cprover_builtin_headers.h | 2 +- 2 files changed, 14 insertions(+), 3 deletions(-) diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index f8257f494d3..7b639f38142 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2132,10 +2132,10 @@ exprt c_typecheck_baset::do_special_functions( } else if(identifier == CPROVER_PREFIX "points_to_valid_memory") { - if(expr.arguments().size() != 2) + if(expr.arguments().size() != 2 && expr.arguments().size() != 1) { error().source_location = f_op.source_location(); - error() << "points_to_valid_memory expects two operands" << eom; + error() << "points_to_valid_memory expects one or two operands" << eom; throw 0; } if(!is_lvalue(expr.arguments().front())) @@ -2163,6 +2163,17 @@ exprt c_typecheck_baset::do_special_functions( 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(); + exprt sizeof_expr = size_of_expr(base_type, *this); + sizeof_expr.add(ID_C_c_sizeof_type) = base_type; + + same_object_expr = + points_to_valid_memory(expr.arguments()[0], sizeof_expr); + } else { UNREACHABLE; diff --git a/src/ansi-c/cprover_builtin_headers.h b/src/ansi-c/cprover_builtin_headers.h index d0c642f948e..a8fb4272163 100644 --- a/src/ansi-c/cprover_builtin_headers.h +++ b/src/ansi-c/cprover_builtin_headers.h @@ -6,7 +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_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 *); From 0d79dc4d87acf28f9238243c6ee97a0a917495ba Mon Sep 17 00:00:00 2001 From: klaas Date: Mon, 30 Jul 2018 14:35:47 -0400 Subject: [PATCH 03/16] Adds tests for --expand-pointer-predicates --- .../expand-pointer-predicates1/main.c | 7 ++++++ .../expand-pointer-predicates1/test.desc | 8 +++++++ .../expand-pointer-predicates2/main.c | 7 ++++++ .../expand-pointer-predicates2/test.desc | 8 +++++++ .../expand-pointer-predicates3/main.c | 8 +++++++ .../expand-pointer-predicates3/test.desc | 8 +++++++ .../expand-pointer-predicates4/main.c | 7 ++++++ .../expand-pointer-predicates4/test.desc | 8 +++++++ .../expand-pointer-predicates5/main.c | 19 ++++++++++++++++ .../expand-pointer-predicates5/test.desc | 10 +++++++++ .../expand-pointer-predicates6/main.c | 21 ++++++++++++++++++ .../expand-pointer-predicates6/test.desc | 9 ++++++++ .../expand-pointer-predicates7/main.c | 22 +++++++++++++++++++ .../expand-pointer-predicates7/test.desc | 8 +++++++ .../expand-pointer-predicates8/main.c | 16 ++++++++++++++ .../expand-pointer-predicates8/test.desc | 16 ++++++++++++++ .../expand-pointer-predicates9/main.c | 11 ++++++++++ .../expand-pointer-predicates9/test.desc | 12 ++++++++++ 18 files changed, 205 insertions(+) create mode 100644 regression/goto-instrument/expand-pointer-predicates1/main.c create mode 100644 regression/goto-instrument/expand-pointer-predicates1/test.desc create mode 100644 regression/goto-instrument/expand-pointer-predicates2/main.c create mode 100644 regression/goto-instrument/expand-pointer-predicates2/test.desc create mode 100644 regression/goto-instrument/expand-pointer-predicates3/main.c create mode 100644 regression/goto-instrument/expand-pointer-predicates3/test.desc create mode 100644 regression/goto-instrument/expand-pointer-predicates4/main.c create mode 100644 regression/goto-instrument/expand-pointer-predicates4/test.desc create mode 100644 regression/goto-instrument/expand-pointer-predicates5/main.c create mode 100644 regression/goto-instrument/expand-pointer-predicates5/test.desc create mode 100644 regression/goto-instrument/expand-pointer-predicates6/main.c create mode 100644 regression/goto-instrument/expand-pointer-predicates6/test.desc create mode 100644 regression/goto-instrument/expand-pointer-predicates7/main.c create mode 100644 regression/goto-instrument/expand-pointer-predicates7/test.desc create mode 100644 regression/goto-instrument/expand-pointer-predicates8/main.c create mode 100644 regression/goto-instrument/expand-pointer-predicates8/test.desc create mode 100644 regression/goto-instrument/expand-pointer-predicates9/main.c create mode 100644 regression/goto-instrument/expand-pointer-predicates9/test.desc 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..eca2be9cee2 --- /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\] Variable length assert: SUCCESS$ +^\[main.assertion.2\] 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..69d70b62e0f --- /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\] : 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..a15c074645c --- /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]+\] dereference failure: dead object in x\[\(signed long( long)? int\)0\]: SUCCESS$ +^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)0\]: SUCCESS$ +^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)1\]: SUCCESS$ +^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)2\]: FAILURE$ +^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)-1\]: FAILURE$ +^\[main.pointer_dereference.[0-9]+\] dereference failure: dead object in y\[\(signed long( long)? int\)0\]: SUCCESS$ +^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in y\[\(signed long( long)? int\)0\]: SUCCESS$ +^\[main.pointer_dereference.[0-9]+\] 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..4a9a4bf26fc --- /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]+\] dereference failure: dead object in \*x: SUCCESS$ +^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in \*x: SUCCESS$ +^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)1\]: FAILURE$ +^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in \*\(x - \(signed long( long)? int\)1\): FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- From 40bd1b350e54b5e87ab248e02d5f9a4237ca06a2 Mon Sep 17 00:00:00 2001 From: klaas Date: Wed, 23 May 2018 14:55:12 -0400 Subject: [PATCH 04/16] Splits code contracts into check(WIP) and apply The previous implementation of code-contracts has a single flag --apply-code-contracts, which created checks to verify that the contracts are satisfied and also used the contracts to abstract out the portions of code which had contracts provided. This commit splits that process into two parts, one of which only uses the contracts, without checking that they hold (--apply-code-contracts) and the other of which (incomplete as of this commit) both checks and applies, in a similar manner to the existing method. While it is clear that applying contracts without checking them is unsound, it is nevertheless useful in verifying large pieces of software in a modular fashion. If we verify a function to satisfy its specification from an arbitrary environment, then we can avoid needing to check that function again by using --apply-code-contracts. --- .gitignore | 2 + .../contracts/function_apply_01/test.desc | 3 +- .../contracts/function_check_04/test.desc | 2 +- regression/contracts/invar_check_01/test.desc | 2 +- regression/contracts/invar_check_02/test.desc | 2 +- regression/contracts/invar_check_03/test.desc | 2 +- regression/contracts/invar_check_04/test.desc | 2 +- src/goto-instrument/code_contracts.cpp | 254 ++++++++++++++---- src/goto-instrument/code_contracts.h | 3 +- .../goto_instrument_parse_options.cpp | 10 +- .../goto_instrument_parse_options.h | 4 +- 11 files changed, 223 insertions(+), 63 deletions(-) diff --git a/.gitignore b/.gitignore index 115ca57475c..51bb5f9f07e 100644 --- a/.gitignore +++ b/.gitignore @@ -65,6 +65,8 @@ jbmc/regression/**/tests-symex-driven-loading.log # files stored by editors *~ +.*.swp +.*.swo # libs downloaded by make [name]-download minisat*/ diff --git a/regression/contracts/function_apply_01/test.desc b/regression/contracts/function_apply_01/test.desc index abc8686ad8e..4f37c84c808 100644 --- a/regression/contracts/function_apply_01/test.desc +++ b/regression/contracts/function_apply_01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --apply-code-contracts ^EXIT=0$ @@ -6,4 +6,3 @@ main.c ^VERIFICATION SUCCESSFUL$ -- -- -Applying code contracts currently also checks them. diff --git a/regression/contracts/function_check_04/test.desc b/regression/contracts/function_check_04/test.desc index 20a7e46f099..3a6e25efd4a 100644 --- a/regression/contracts/function_check_04/test.desc +++ b/regression/contracts/function_check_04/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --apply-code-contracts ^\[main.assertion.1\] .* assertion x == 0: SUCCESS$ diff --git a/regression/contracts/invar_check_01/test.desc b/regression/contracts/invar_check_01/test.desc index d9a2ec0a8ca..7dafb10d751 100644 --- a/regression/contracts/invar_check_01/test.desc +++ b/regression/contracts/invar_check_01/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --apply-code-contracts ^EXIT=0$ diff --git a/regression/contracts/invar_check_02/test.desc b/regression/contracts/invar_check_02/test.desc index d9a2ec0a8ca..7dafb10d751 100644 --- a/regression/contracts/invar_check_02/test.desc +++ b/regression/contracts/invar_check_02/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --apply-code-contracts ^EXIT=0$ diff --git a/regression/contracts/invar_check_03/test.desc b/regression/contracts/invar_check_03/test.desc index d9a2ec0a8ca..7dafb10d751 100644 --- a/regression/contracts/invar_check_03/test.desc +++ b/regression/contracts/invar_check_03/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --apply-code-contracts ^EXIT=0$ diff --git a/regression/contracts/invar_check_04/test.desc b/regression/contracts/invar_check_04/test.desc index f8abcf720a5..9003de22839 100644 --- a/regression/contracts/invar_check_04/test.desc +++ b/regression/contracts/invar_check_04/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --apply-code-contracts ^\[main.1\] .* Loop invariant violated before entry: SUCCESS$ diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 98408f6accd..fac4f430624 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -25,6 +25,12 @@ Date: February 2016 #include "loop_utils.h" +enum class contract_opst +{ + APPLY, + CHECK +}; + class code_contractst { public: @@ -38,7 +44,7 @@ class code_contractst { } - void operator()(); + void operator()(contract_opst op_type); protected: namespacet ns; @@ -49,12 +55,21 @@ class code_contractst std::unordered_set summarized; + void apply_code_contracts(); + void check_code_contracts(); + void code_contracts(goto_functionst::goto_functiont &goto_function); void apply_contract( goto_programt &goto_program, goto_programt::targett target); + void apply_invariant( + goto_functionst::goto_functiont &goto_function, + const local_may_aliast &local_may_alias, + const goto_programt::targett loop_head, + const loopt &loop); + void add_contract_check( const irep_idt &function, goto_programt &dest); @@ -70,25 +85,28 @@ static void check_apply_invariants( const goto_programt::targett loop_head, const loopt &loop) { - assert(!loop.empty()); + PRECONDITION(!loop.empty()); // find the last back edge goto_programt::targett loop_end=loop_head; - for(loopt::const_iterator - it=loop.begin(); - it!=loop.end(); - ++it) - if((*it)->is_goto() && - (*it)->get_target()==loop_head && - (*it)->location_number>loop_end->location_number) - loop_end=*it; + for(const goto_programt::targett &inst : loop) + { + if( + inst->is_goto() && inst->get_target() == loop_head && + inst->location_number > loop_end->location_number) + { + loop_end = inst; + } + } // see whether we have an invariant exprt invariant= static_cast( loop_end->guard.find(ID_C_spec_loop_invariant)); if(invariant.is_nil()) + { return; + } // change H: loop; E: ... // to @@ -117,7 +135,7 @@ static void check_apply_invariants( a->source_location.set_comment("Loop invariant violated before entry"); } - // havoc variables being written to + // havoc variables that can be modified by the loop build_havoc_code(loop_head, modifies, havoc_code); // assume the invariant @@ -138,8 +156,8 @@ static void check_apply_invariants( jump->function=loop_head->function; } - // Now havoc at the loop head. Use insert_swap to - // preserve jumps to loop head. + // Now havoc at the loop head. Use insert_before_swap to preserve jumps to + // loop head. goto_function.body.insert_before_swap(loop_head, havoc_code); // assert the invariant at the end of the loop body @@ -176,14 +194,22 @@ void code_contractst::apply_contract( const symbolt &f_sym=ns.lookup(function); const code_typet &type=to_code_type(f_sym.type); - exprt requires= - static_cast(type.find(ID_C_spec_requires)); - exprt ensures= - static_cast(type.find(ID_C_spec_ensures)); + exprt requires = static_cast(type.find(ID_C_spec_requires)); + exprt ensures = static_cast(type.find(ID_C_spec_ensures)); - // is there a contract? if(ensures.is_nil()) - return; + { + // If there is no contract at all, we skip this function. + if(requires.is_nil()) + { + return; + } + else + { + // If there's no ensures but is a requires, treat it as ensures(true) + ensures = true_exprt(); + } + } // replace formal parameters by arguments, replace return replace_symbolt replace; @@ -222,12 +248,101 @@ void code_contractst::apply_contract( goto_program.insert_before_swap(target, a); ++target; } + // TODO: Havoc write set of the function between assert and ensure. target->make_assumption(ensures); summarized.insert(function); } +void code_contractst::apply_invariant( + goto_functionst::goto_functiont &goto_function, + const local_may_aliast &local_may_alias, + const goto_programt::targett loop_head, + const loopt &loop) +{ + assert(!loop.empty()); + + // find the last back edge + goto_programt::targett loop_end = loop_head; + for(const goto_programt::targett &inst : loop) + { + if( + inst->is_goto() && inst->get_target() == loop_head && + inst->location_number > loop_end->location_number) + { + loop_end = inst; + } + } + + exprt invariant = + static_cast(loop_end->guard.find(ID_C_spec_loop_invariant)); + if(invariant.is_nil()) + { + return; + } + + // change H: loop; E: ... + // to + // H: assert(invariant); + // havoc; + // assume(invariant); + // assume(!guard); + // E: ... + + // find out what can get changed in the loop + modifiest modifies; + get_modifies(local_may_alias, loop, modifies); + + // build the havocking code + goto_programt havoc_code; + + // assert the invariant + { + goto_programt::targett a = havoc_code.add_instruction(ASSERT); + a->guard = invariant; + a->function = loop_head->function; + a->source_location = loop_head->source_location; + a->source_location.set_comment("Loop invariant violated before entry"); + } + + // havoc variables that can be modified by the loop + build_havoc_code(loop_head, modifies, havoc_code); + + // assume the invariant + { + goto_programt::targett assume = havoc_code.add_instruction(ASSUME); + assume->guard = invariant; + assume->function = loop_head->function; + assume->source_location = loop_head->source_location; + } + + // assume !guard + // TODO: consider breaks snd how they're implemented. + // TODO: Also consider continues and whether they jump to loop end or head + { + goto_programt::targett assume = havoc_code.add_instruction(ASSUME); + + if(loop_head->is_goto()) + assume->guard = loop_head->guard; + else + assume->guard = boolean_negate(loop_end->guard); + + assume->function = loop_head->function; + assume->source_location = loop_head->source_location; + } + + // Clear out loop body + for(const goto_programt::targett &inst : loop) + { + inst->make_skip(); + } + + // Now havoc at the loop head. Use insert_before_swap to preserve jumps to + // loop head. + goto_function.body.insert_before_swap(loop_head, havoc_code); +} + void code_contractst::code_contracts( goto_functionst::goto_functiont &goto_function) { @@ -235,15 +350,11 @@ void code_contractst::code_contracts( natural_loops_mutablet natural_loops(goto_function.body); // iterate over the (natural) loops in the function - for(natural_loops_mutablet::loop_mapt::const_iterator - l_it=natural_loops.loop_map.begin(); - l_it!=natural_loops.loop_map.end(); - l_it++) + for(const auto &l_it : natural_loops.loop_map) + { check_apply_invariants( - goto_function, - local_may_alias, - l_it->first, - l_it->second); + goto_function, local_may_alias, l_it.first, l_it.second); + } // look at all function calls Forall_goto_program_instructions(it, goto_function.body) @@ -260,7 +371,7 @@ const symbolt &code_contractst::new_tmp_symbol( id2string(source_location.get_function()), "tmp_cc", source_location, - irep_idt(), + ID_C, symbol_table); } @@ -268,7 +379,7 @@ void code_contractst::add_contract_check( const irep_idt &function, goto_programt &dest) { - assert(!dest.instructions.empty()); + PRECONDITION(!dest.instructions.empty()); goto_functionst::function_mapt::iterator f_it= goto_functions.function_map.find(function); @@ -276,10 +387,8 @@ void code_contractst::add_contract_check( const goto_functionst::goto_functiont &gf=f_it->second; - const exprt &requires= - static_cast(gf.type.find(ID_C_spec_requires)); - const exprt &ensures= - static_cast(gf.type.find(ID_C_spec_ensures)); + exprt requires = static_cast(gf.type.find(ID_C_spec_requires)); + exprt ensures = static_cast(gf.type.find(ID_C_spec_ensures)); assert(ensures.is_not_nil()); // build: @@ -330,29 +439,29 @@ void code_contractst::add_contract_check( } // decl parameter1 ... - for(code_typet::parameterst::const_iterator - p_it=gf.type.parameters().begin(); - p_it!=gf.type.parameters().end(); - ++p_it) + for(const auto &p_it : gf.type.parameters()) { goto_programt::targett d=check.add_instruction(DECL); d->function=skip->function; d->source_location=skip->source_location; - symbol_exprt p= - new_tmp_symbol(p_it->type(), - d->source_location).symbol_expr(); + symbol_exprt p = + new_tmp_symbol(p_it.type(), d->source_location).symbol_expr(); d->code=code_declt(p); call.arguments().push_back(p); - if(!p_it->get_identifier().empty()) + if(!p_it.get_identifier().empty()) { - symbol_exprt cur_p(p_it->get_identifier(), p_it->type()); + symbol_exprt cur_p(p_it.get_identifier(), p_it.type()); replace.insert(cur_p, p); } } + // rewrite any use of parameters + replace(requires); + replace(ensures); + // assume(requires) if(requires.is_not_nil()) { @@ -360,9 +469,6 @@ void code_contractst::add_contract_check( a->make_assumption(requires); a->function=skip->function; a->source_location=requires.source_location(); - - // rewrite any use of parameters - replace(a->guard); } // ret=function(parameter1, ...) @@ -377,9 +483,6 @@ void code_contractst::add_contract_check( a->function=skip->function; a->source_location=ensures.source_location(); - // rewrite any use of __CPROVER_return_value - replace(a->guard); - // assume(false) goto_programt::targett af=check.add_instruction(); af->make_assumption(false_exprt()); @@ -391,10 +494,39 @@ void code_contractst::add_contract_check( dest.destructive_insert(dest.instructions.begin(), check); } -void code_contractst::operator()() +void code_contractst::apply_code_contracts() { Forall_goto_functions(it, goto_functions) + { + goto_functionst::goto_functiont &goto_function = it->second; + + // TODO: This aliasing check is insufficiently strong, in general. + local_may_aliast local_may_alias(goto_function); + natural_loops_mutablet natural_loops(goto_function.body); + + for(const auto &l_it : natural_loops.loop_map) + { + apply_invariant(goto_function, local_may_alias, l_it.first, l_it.second); + } + + Forall_goto_program_instructions(it, goto_function.body) + { + if(it->is_function_call()) + { + apply_contract(goto_function.body, it); + } + } + } + + goto_functions.update(); +} + +void code_contractst::check_code_contracts() +{ + Forall_goto_functions(it, goto_functions) + { code_contracts(it->second); + } goto_functionst::function_mapt::iterator i_it= goto_functions.function_map.find(INITIALIZE_FUNCTION); @@ -409,7 +541,27 @@ void code_contractst::operator()() goto_functions.update(); } -void code_contracts(goto_modelt &goto_model) +void code_contractst::operator()(contract_opst op_type) +{ + switch(op_type) + { + case contract_opst::APPLY: + apply_code_contracts(); + break; + case contract_opst::CHECK: + check_code_contracts(); + break; + } +} + +void check_code_contracts(goto_modelt &goto_model) +{ + code_contractst(goto_model.symbol_table, goto_model.goto_functions)( + contract_opst::CHECK); +} + +void apply_code_contracts(goto_modelt &goto_model) { - code_contractst(goto_model.symbol_table, goto_model.goto_functions)(); + code_contractst(goto_model.symbol_table, goto_model.goto_functions)( + contract_opst::APPLY); } diff --git a/src/goto-instrument/code_contracts.h b/src/goto-instrument/code_contracts.h index dc02902c142..7c7c02c09c0 100644 --- a/src/goto-instrument/code_contracts.h +++ b/src/goto-instrument/code_contracts.h @@ -16,6 +16,7 @@ Date: February 2016 class goto_modelt; -void code_contracts(goto_modelt &); +void apply_code_contracts(goto_modelt &); +void check_code_contracts(goto_modelt &); #endif // CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 022ed724c77..63e1a9e5eff 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1073,11 +1073,17 @@ void goto_instrument_parse_optionst::instrument_goto_program() goto_model.goto_functions.update(); } - // verify and set invariants and pre/post-condition pairs if(cmdline.isset("apply-code-contracts")) { status() << "Applying Code Contracts" << eom; - code_contracts(goto_model); + apply_code_contracts(goto_model); + } + + // verify and set invariants and pre/post-condition pairs + if(cmdline.isset("check-code-contracts")) + { + status() << "Checking Code Contracts" << eom; + check_code_contracts(goto_model); } if(cmdline.isset("expand-pointer-predicates")) diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index cbf49345e6f..bf27b38fcf6 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -90,9 +90,9 @@ Author: Daniel Kroening, kroening@kroening.com "(interpreter)(show-reaching-definitions)" \ "(list-symbols)(list-undefined-functions)" \ "(z3)(add-library)(show-dependence-graph)" \ - "(horn)(skip-loops):(apply-code-contracts)(model-argc-argv):" \ + "(horn)(skip-loops):(apply-code-contracts)(check-code-contracts)" \ "(expand-pointer-predicates)" \ - "(show-threaded)(list-calls-args)" \ + "(model-argc-argv):(show-threaded)(list-calls-args)" \ "(undefined-function-is-assume-false)" \ "(remove-function-body):"\ OPT_AGGRESSIVE_SLICER \ From bdebfb6dfd5952b4a325b895f62fbc8bf47ebf2d Mon Sep 17 00:00:00 2001 From: klaas Date: Fri, 25 May 2018 15:33:37 -0400 Subject: [PATCH 05/16] Reworks checking of code contracts This commit completes the work started in the previous commit by revising the existing contract-handling code into the new pass --check-code-contracts, which first applies all contracts and then checks them. By applying the contracts before checking begins, this checks the relative correctness of each function/loop with respect to the functions called by/loops contained in it. Since there can be no infinite sequence of nested functions/loops, these relative correctness results together imply the correctness of the overall program. We take this approach rather than checking entirely without using contracts because it allows significant reuse of results --- a function that is called many times only needs to be checked once, and all of its invocations will be abstracted out by the contract application. --- .gitignore | 2 + .../contracts/function_check_01/test.desc | 5 +- .../contracts/function_check_04/test.desc | 9 +- .../contracts/function_check_mem_01/main.c | 2 +- .../contracts/function_check_mem_01/test.desc | 2 +- regression/contracts/invar_check_01/test.desc | 7 +- regression/contracts/invar_check_02/test.desc | 7 +- regression/contracts/invar_check_03/test.desc | 7 +- regression/contracts/invar_check_04/test.desc | 9 +- src/goto-instrument/code_contracts.cpp | 355 ++++++++++++++++-- src/goto-instrument/loop_utils.cpp | 38 ++ src/goto-instrument/loop_utils.h | 6 + 12 files changed, 382 insertions(+), 67 deletions(-) diff --git a/.gitignore b/.gitignore index 51bb5f9f07e..362978b3a23 100644 --- a/.gitignore +++ b/.gitignore @@ -19,6 +19,8 @@ src/.settings/* # Visual Studio Debug/* Release/* +#vi(m) +*.swp # compilation files *.lo diff --git a/regression/contracts/function_check_01/test.desc b/regression/contracts/function_check_01/test.desc index d9a2ec0a8ca..a44b7e292f5 100644 --- a/regression/contracts/function_check_01/test.desc +++ b/regression/contracts/function_check_01/test.desc @@ -1,11 +1,8 @@ CORE main.c ---apply-code-contracts +--check-code-contracts ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -- ---check-code-contracts not implemented yet. ---apply-code-contracts is the current name for the flag. This should be -updated as the flag changes. diff --git a/regression/contracts/function_check_04/test.desc b/regression/contracts/function_check_04/test.desc index 3a6e25efd4a..3a3bc557bf7 100644 --- a/regression/contracts/function_check_04/test.desc +++ b/regression/contracts/function_check_04/test.desc @@ -1,11 +1,8 @@ -KNOWNBUG +CORE main.c ---apply-code-contracts +--check-code-contracts ^\[main.assertion.1\] .* assertion x == 0: SUCCESS$ -^\[foo.1\] line 9 : FAILURE$ +^\[foo.1\] .* : FAILURE$ ^VERIFICATION FAILED$ -- -- ---check-code-contracts not implemented yet. ---apply-code-contracts is the current name for the flag. This should be -updated as the flag changes. diff --git a/regression/contracts/function_check_mem_01/main.c b/regression/contracts/function_check_mem_01/main.c index b63364f4d57..10d79cf8190 100644 --- a/regression/contracts/function_check_mem_01/main.c +++ b/regression/contracts/function_check_mem_01/main.c @@ -33,7 +33,7 @@ void foo(bar *x) __CPROVER_requires(__CPROVER_VALID_MEM(x, sizeof(bar))) { x->x += 1; - return + return; } int main() diff --git a/regression/contracts/function_check_mem_01/test.desc b/regression/contracts/function_check_mem_01/test.desc index b46799f781b..c45406ad744 100644 --- a/regression/contracts/function_check_mem_01/test.desc +++ b/regression/contracts/function_check_mem_01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --check-code-contracts ^EXIT=0$ diff --git a/regression/contracts/invar_check_01/test.desc b/regression/contracts/invar_check_01/test.desc index 7dafb10d751..a44b7e292f5 100644 --- a/regression/contracts/invar_check_01/test.desc +++ b/regression/contracts/invar_check_01/test.desc @@ -1,11 +1,8 @@ -KNOWNBUG +CORE main.c ---apply-code-contracts +--check-code-contracts ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -- ---check-code-contracts not implemented yet. ---apply-code-contracts is the current name for the flag. This should be -updated as the flag changes. diff --git a/regression/contracts/invar_check_02/test.desc b/regression/contracts/invar_check_02/test.desc index 7dafb10d751..a44b7e292f5 100644 --- a/regression/contracts/invar_check_02/test.desc +++ b/regression/contracts/invar_check_02/test.desc @@ -1,11 +1,8 @@ -KNOWNBUG +CORE main.c ---apply-code-contracts +--check-code-contracts ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -- ---check-code-contracts not implemented yet. ---apply-code-contracts is the current name for the flag. This should be -updated as the flag changes. diff --git a/regression/contracts/invar_check_03/test.desc b/regression/contracts/invar_check_03/test.desc index 7dafb10d751..a44b7e292f5 100644 --- a/regression/contracts/invar_check_03/test.desc +++ b/regression/contracts/invar_check_03/test.desc @@ -1,11 +1,8 @@ -KNOWNBUG +CORE main.c ---apply-code-contracts +--check-code-contracts ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -- ---check-code-contracts not implemented yet. ---apply-code-contracts is the current name for the flag. This should be -updated as the flag changes. diff --git a/regression/contracts/invar_check_04/test.desc b/regression/contracts/invar_check_04/test.desc index 9003de22839..e5a66f2d71b 100644 --- a/regression/contracts/invar_check_04/test.desc +++ b/regression/contracts/invar_check_04/test.desc @@ -1,12 +1,11 @@ -KNOWNBUG +CORE main.c ---apply-code-contracts +--check-code-contracts +^EXIT=10$ +^SIGNAL=0$ ^\[main.1\] .* Loop invariant violated before entry: SUCCESS$ ^\[main.2\] .* Loop invariant not preserved: SUCCESS$ ^\[main.assertion.1\] .* assertion r == 0: FAILURE$ ^VERIFICATION FAILED$ -- -- ---check-code-contracts not implemented yet. ---apply-code-contracts is the current name for the flag. This should be -updated as the flag changes. diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index fac4f430624..c3ba6ed8fb3 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -70,6 +70,17 @@ class code_contractst const goto_programt::targett loop_head, const loopt &loop); + void check_contract( + const irep_idt &function_id, + goto_functionst::goto_functiont &goto_function, + goto_programt &dest); + + void check_apply_invariant( + goto_functionst::goto_functiont &goto_function, + const local_may_aliast &local_may_alias, + const goto_programt::targett loop_head, + const loopt &loop); + void add_contract_check( const irep_idt &function, goto_programt &dest); @@ -111,73 +122,113 @@ static void check_apply_invariants( // change H: loop; E: ... // to // H: assert(invariant); - // havoc; + // if(nondet) goto E: + // havoc reads and writes of loop; // assume(invariant); - // if(guard) goto E: + // assume(guard) [only for for/while loops] // loop; // assert(invariant); // assume(false); - // E: ... + // E: havoc writes of loop; + // assume(invariant) + // assume(!guard) + // ... // find out what can get changed in the loop modifiest modifies; get_modifies(local_may_alias, loop, modifies); + // find out what is used by the loop + usest uses; + get_uses(local_may_alias, loop, uses); + // build the havocking code - goto_programt havoc_code; + goto_programt havoc_all_code; + goto_programt havoc_writes_code; // assert the invariant { - goto_programt::targett a=havoc_code.add_instruction(ASSERT); + goto_programt::targett a = havoc_all_code.add_instruction(ASSERT); a->guard=invariant; a->function=loop_head->function; a->source_location=loop_head->source_location; a->source_location.set_comment("Loop invariant violated before entry"); } + // nondeterministically skip the loop + { + goto_programt::targett jump = havoc_all_code.add_instruction(GOTO); + jump->guard = side_effect_expr_nondett(bool_typet()); + jump->targets.push_back(loop_end); + jump->function = loop_head->function; + jump->source_location = loop_head->source_location; + } + // havoc variables that can be modified by the loop - build_havoc_code(loop_head, modifies, havoc_code); + build_havoc_code(loop_head, uses, havoc_all_code); // assume the invariant { - goto_programt::targett assume=havoc_code.add_instruction(ASSUME); + goto_programt::targett assume = havoc_all_code.add_instruction(ASSUME); assume->guard=invariant; assume->function=loop_head->function; assume->source_location=loop_head->source_location; } - // non-deterministically skip the loop if it is a do-while loop - if(!loop_head->is_goto()) + // assert the invariant at the end of the loop body { - goto_programt::targett jump=havoc_code.add_instruction(GOTO); - jump->guard = - side_effect_expr_nondett(bool_typet(), loop_head->source_location); - jump->targets.push_back(loop_end); - jump->function=loop_head->function; + goto_programt::targett a = goto_function.body.insert_before(loop_end); + a->type = ASSERT; + a->guard = invariant; + a->function = loop_end->function; + a->source_location = loop_end->source_location; + a->source_location.set_comment("Loop invariant not preserved"); } - // Now havoc at the loop head. Use insert_before_swap to preserve jumps to - // loop head. - goto_function.body.insert_before_swap(loop_head, havoc_code); + // assume false at the end of the loop to discharge the havocking + { + goto_programt::targett assume = goto_function.body.insert_before(loop_end); + assume->type = ASSUME; + assume->guard = false_exprt(); + assume->function = loop_end->function; + assume->source_location = loop_end->source_location; + } - // assert the invariant at the end of the loop body + build_havoc_code(loop_end, modifies, havoc_writes_code); + + // Assume the invariant (now after the loop) { - goto_programt::instructiont a(ASSERT); - a.guard=invariant; - a.function=loop_end->function; - a.source_location=loop_end->source_location; - a.source_location.set_comment("Loop invariant not preserved"); - goto_function.body.insert_before_swap(loop_end, a); - ++loop_end; + goto_programt::targett assume = havoc_writes_code.add_instruction(ASSUME); + assume->guard = invariant; + assume->function = loop_head->function; + assume->source_location = loop_head->source_location; } - // change the back edge into assume(false) or assume(guard) + // change the back edge into assume(!guard) loop_end->targets.clear(); loop_end->type=ASSUME; if(loop_head->is_goto()) - loop_end->guard = false_exprt(); + { + loop_end->guard = loop_head->guard; + } else + { loop_end->guard = boolean_negate(loop_end->guard); + } + + // Change the loop head to assume the guard if a for/while loop. + // This needs to be done after we case on what loop_head is in the previous + // section of setup. + if(loop_head->is_goto()) + loop_head->make_assumption(boolean_negate(loop_head->guard)); + + // Now havoc at the loop head. Use insert_before_swap to preserve jumps to + // loop head. + goto_function.body.insert_before_swap(loop_head, havoc_all_code); + + // Now havoc at the loop end. Use insert_before_swap to preserve jumps to loop + // end. + goto_function.body.insert_before_swap(loop_end, havoc_writes_code); } void code_contractst::apply_contract( @@ -282,6 +333,8 @@ void code_contractst::apply_invariant( return; } + // TODO: Allow for not havocking in the for/while case + // change H: loop; E: ... // to // H: assert(invariant); @@ -318,7 +371,7 @@ void code_contractst::apply_invariant( } // assume !guard - // TODO: consider breaks snd how they're implemented. + // TODO: consider breaks and how they're implemented. // TODO: Also consider continues and whether they jump to loop end or head { goto_programt::targett assume = havoc_code.add_instruction(ASSUME); @@ -341,6 +394,218 @@ void code_contractst::apply_invariant( // Now havoc at the loop head. Use insert_before_swap to preserve jumps to // loop head. goto_function.body.insert_before_swap(loop_head, havoc_code); + + // Remove all the skips we created. + remove_skip(goto_function.body); +} + +void code_contractst::check_contract( + const irep_idt &function_id, + goto_functionst::goto_functiont &goto_function, + goto_programt &dest) +{ + assert(!dest.instructions.empty()); + + exprt requires = + static_cast(goto_function.type.find(ID_C_spec_requires)); + exprt ensures = + static_cast(goto_function.type.find(ID_C_spec_ensures)); + + // Nothing to check if ensures is nil. + if(ensures.is_nil()) + { + return; + } + + // We build the following checking code: + // if(nondet) goto end + // decl ret + // decl parameter1 ... + // assume(requires) [optional] + // ret = function(parameter1, ...) + // assert(ensures) + // end: + // skip + + // build skip so that if(nondet) can refer to it + goto_programt tmp_skip; + goto_programt::targett skip = tmp_skip.add_instruction(SKIP); + skip->function = dest.instructions.front().function; + skip->source_location = ensures.source_location(); + + goto_programt check; + + // if(nondet) + goto_programt::targett g = check.add_instruction(); + g->make_goto(skip, side_effect_expr_nondett(bool_typet())); + g->function = skip->function; + g->source_location = skip->source_location; + + // prepare function call including all declarations + code_function_callt call; + call.function() = ns.lookup(function_id).symbol_expr(); + replace_symbolt replace; + + // decl ret + // TODO: Handle void functions + // void functions seem to be handled by goto-cc + if(goto_function.type.return_type() != empty_typet()) + { + goto_programt::targett d = check.add_instruction(DECL); + d->function = skip->function; + d->source_location = skip->source_location; + + symbol_exprt r = + new_tmp_symbol(goto_function.type.return_type(), d->source_location) + .symbol_expr(); + d->code = code_declt(r); + + call.lhs() = r; + + symbol_exprt old( + "__CPROVER_return_value", goto_function.type.return_type()); + replace.insert(old, r); + } + + // decl parameter1 ... + for(const auto &p_it : goto_function.type.parameters()) + { + goto_programt::targett d = check.add_instruction(DECL); + d->function = skip->function; + d->source_location = skip->source_location; + + symbol_exprt p = + new_tmp_symbol(p_it.type(), d->source_location).symbol_expr(); + d->code = code_declt(p); + + call.arguments().push_back(p); + + if(!p_it.get_identifier().empty()) + { + symbol_exprt old(p_it.get_identifier(), p_it.type()); + replace.insert(old, p); + } + } + + // assume(requires) + if(requires.is_not_nil()) + { + goto_programt::targett a = check.add_instruction(); + a->make_assumption(requires); + a->function = skip->function; + a->source_location = requires.source_location(); + + // rewrite any use of parameters + replace(a->guard); + } + + // ret=function(parameter1, ...) + goto_programt::targett f = check.add_instruction(); + f->make_function_call(call); + f->function = skip->function; + f->source_location = skip->source_location; + + // assert(ensures) + goto_programt::targett a = check.add_instruction(); + a->make_assertion(ensures); + a->function = skip->function; + a->source_location = ensures.source_location(); + + // rewrite any use of __CPROVER_return_value + replace(a->guard); + + // prepend the new code to dest + check.destructive_append(tmp_skip); + dest.destructive_insert(dest.instructions.begin(), check); +} + +void code_contractst::check_apply_invariant( + goto_functionst::goto_functiont &goto_function, + const local_may_aliast &local_may_alias, + const goto_programt::targett loop_head, + const loopt &loop) +{ + assert(!loop.empty()); + + // find the last back edge + goto_programt::targett loop_end = loop_head; + for(const goto_programt::targett &inst : loop) + if( + inst->is_goto() && inst->get_target() == loop_head && + inst->location_number > loop_end->location_number) + loop_end = inst; + + // see whether we have an invariant + exprt invariant = + static_cast(loop_end->guard.find(ID_C_spec_loop_invariant)); + if(invariant.is_nil()) + return; + + // change H: loop; E: ... + // to + // H: assert(invariant); + // havoc writes of loop; + // assume(invariant); + // loop (minus the ending goto); + // assert(invariant); + // assume(!guard) + // E: + // ... + + // find out what can get changed in the loop + modifiest modifies; + get_modifies(local_may_alias, loop, modifies); + + // build the havocking code + goto_programt havoc_code; + + // assert the invariant + { + goto_programt::targett a = havoc_code.add_instruction(ASSERT); + a->guard = invariant; + a->function = loop_head->function; + a->source_location = loop_head->source_location; + a->source_location.set_comment("Loop invariant violated before entry"); + } + + // havoc variables that can be modified by the loop + build_havoc_code(loop_head, modifies, havoc_code); + + // assume the invariant + { + goto_programt::targett assume = havoc_code.add_instruction(ASSUME); + assume->guard = invariant; + assume->function = loop_head->function; + assume->source_location = loop_head->source_location; + } + + // assert the invariant at the end of the loop body + { + goto_programt::instructiont a(ASSERT); + a.guard = invariant; + a.function = loop_end->function; + a.source_location = loop_end->source_location; + a.source_location.set_comment("Loop invariant not preserved"); + + goto_function.body.insert_before_swap(loop_end, a); + ++loop_end; + } + + // change the back edge into assume(!guard) + loop_end->targets.clear(); + loop_end->type = ASSUME; + if(loop_head->is_goto()) + { + loop_end->guard = loop_head->guard; + } + else + { + loop_end->guard = boolean_negate(loop_end->guard); + } + + // Now havoc at the loop head. Use insert_before_swap to preserve jumps to + // loop head. + goto_function.body.insert_before_swap(loop_head, havoc_code); } void code_contractst::code_contracts( @@ -523,17 +788,37 @@ void code_contractst::apply_code_contracts() void code_contractst::check_code_contracts() { - Forall_goto_functions(it, goto_functions) - { - code_contracts(it->second); - } - goto_functionst::function_mapt::iterator i_it= goto_functions.function_map.find(INITIALIZE_FUNCTION); assert(i_it!=goto_functions.function_map.end()); - for(const auto &contract : summarized) - add_contract_check(contract, i_it->second.body); + Forall_goto_functions(it, goto_functions) + { + goto_functionst::goto_functiont &goto_function = it->second; + + // TODO: This aliasing check is insufficiently strong, in general. + local_may_aliast local_may_alias(goto_function); + natural_loops_mutablet natural_loops(goto_function.body); + + for(const auto &l_it : natural_loops.loop_map) + { + check_apply_invariant( + goto_function, local_may_alias, l_it.first, l_it.second); + } + + Forall_goto_program_instructions(it, goto_function.body) + { + if(it->is_function_call()) + { + apply_contract(goto_function.body, it); + } + } + } + + Forall_goto_functions(it, goto_functions) + { + check_contract(it->first, it->second, i_it->second.body); + } // remove skips remove_skip(i_it->second.body); diff --git a/src/goto-instrument/loop_utils.cpp b/src/goto-instrument/loop_utils.cpp index 4ab59238bc9..feb6df47145 100644 --- a/src/goto-instrument/loop_utils.cpp +++ b/src/goto-instrument/loop_utils.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "loop_utils.h" +#include #include #include @@ -108,3 +109,40 @@ void get_modifies( } } } + +// TODO handle aliasing at all +void get_uses( + const local_may_aliast &local_may_alias, + const loopt &loop, + usest &uses) +{ + for(loopt::const_iterator i_it = loop.begin(); i_it != loop.end(); i_it++) + { + const goto_programt::instructiont &instruction = **i_it; + if(instruction.code.is_not_nil()) + { + for(const_depth_iteratort it = instruction.code.depth_begin(); + it != instruction.code.depth_end(); + ++it) + { + if((*it).id() == ID_symbol) + { + uses.insert(*it); + } + } + } + + if(instruction.guard.is_not_nil()) + { + for(const_depth_iteratort it = instruction.guard.depth_begin(); + it != instruction.guard.depth_end(); + ++it) + { + if((*it).id() == ID_symbol) + { + uses.insert(*it); + } + } + } + } +} diff --git a/src/goto-instrument/loop_utils.h b/src/goto-instrument/loop_utils.h index 57407ecec1b..1296374eff7 100644 --- a/src/goto-instrument/loop_utils.h +++ b/src/goto-instrument/loop_utils.h @@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com class local_may_aliast; typedef std::set modifiest; +typedef std::set usest; typedef const natural_loops_mutablet::natural_loopt loopt; void get_modifies( @@ -24,6 +25,11 @@ void get_modifies( const loopt &loop, modifiest &modifies); +void get_uses( + const local_may_aliast &local_may_alias, + const loopt &loop, + usest &uses); + void build_havoc_code( const goto_programt::targett loop_head, const modifiest &modifies, From 6166221560f355d2812e6846b43d28ac916aaa4b Mon Sep 17 00:00:00 2001 From: klaas Date: Wed, 1 Aug 2018 16:35:35 -0400 Subject: [PATCH 06/16] Removes some dead code. Several functions from the old implementation of code-contracts that were made dead by the previous commits are removed by this commit. Additionally, some variables which were formerly in use are no longer needed, and so are removed. --- src/goto-instrument/code_contracts.cpp | 344 ++----------------------- 1 file changed, 27 insertions(+), 317 deletions(-) diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index c3ba6ed8fb3..614096950f5 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -36,11 +36,10 @@ class code_contractst public: code_contractst( symbol_tablet &_symbol_table, - goto_functionst &_goto_functions): - ns(_symbol_table), + goto_functionst &_goto_functions) + : ns(_symbol_table), symbol_table(_symbol_table), - goto_functions(_goto_functions), - temporary_counter(0) + goto_functions(_goto_functions) { } @@ -51,10 +50,6 @@ class code_contractst symbol_tablet &symbol_table; goto_functionst &goto_functions; - unsigned temporary_counter; - - std::unordered_set summarized; - void apply_code_contracts(); void check_code_contracts(); @@ -81,156 +76,11 @@ class code_contractst const goto_programt::targett loop_head, const loopt &loop); - void add_contract_check( - const irep_idt &function, - goto_programt &dest); - const symbolt &new_tmp_symbol( const typet &type, const source_locationt &source_location); }; -static void check_apply_invariants( - goto_functionst::goto_functiont &goto_function, - const local_may_aliast &local_may_alias, - const goto_programt::targett loop_head, - const loopt &loop) -{ - PRECONDITION(!loop.empty()); - - // find the last back edge - goto_programt::targett loop_end=loop_head; - for(const goto_programt::targett &inst : loop) - { - if( - inst->is_goto() && inst->get_target() == loop_head && - inst->location_number > loop_end->location_number) - { - loop_end = inst; - } - } - - // see whether we have an invariant - exprt invariant= - static_cast( - loop_end->guard.find(ID_C_spec_loop_invariant)); - if(invariant.is_nil()) - { - return; - } - - // change H: loop; E: ... - // to - // H: assert(invariant); - // if(nondet) goto E: - // havoc reads and writes of loop; - // assume(invariant); - // assume(guard) [only for for/while loops] - // loop; - // assert(invariant); - // assume(false); - // E: havoc writes of loop; - // assume(invariant) - // assume(!guard) - // ... - - // find out what can get changed in the loop - modifiest modifies; - get_modifies(local_may_alias, loop, modifies); - - // find out what is used by the loop - usest uses; - get_uses(local_may_alias, loop, uses); - - // build the havocking code - goto_programt havoc_all_code; - goto_programt havoc_writes_code; - - // assert the invariant - { - goto_programt::targett a = havoc_all_code.add_instruction(ASSERT); - a->guard=invariant; - a->function=loop_head->function; - a->source_location=loop_head->source_location; - a->source_location.set_comment("Loop invariant violated before entry"); - } - - // nondeterministically skip the loop - { - goto_programt::targett jump = havoc_all_code.add_instruction(GOTO); - jump->guard = side_effect_expr_nondett(bool_typet()); - jump->targets.push_back(loop_end); - jump->function = loop_head->function; - jump->source_location = loop_head->source_location; - } - - // havoc variables that can be modified by the loop - build_havoc_code(loop_head, uses, havoc_all_code); - - // assume the invariant - { - goto_programt::targett assume = havoc_all_code.add_instruction(ASSUME); - assume->guard=invariant; - assume->function=loop_head->function; - assume->source_location=loop_head->source_location; - } - - // assert the invariant at the end of the loop body - { - goto_programt::targett a = goto_function.body.insert_before(loop_end); - a->type = ASSERT; - a->guard = invariant; - a->function = loop_end->function; - a->source_location = loop_end->source_location; - a->source_location.set_comment("Loop invariant not preserved"); - } - - // assume false at the end of the loop to discharge the havocking - { - goto_programt::targett assume = goto_function.body.insert_before(loop_end); - assume->type = ASSUME; - assume->guard = false_exprt(); - assume->function = loop_end->function; - assume->source_location = loop_end->source_location; - } - - build_havoc_code(loop_end, modifies, havoc_writes_code); - - // Assume the invariant (now after the loop) - { - goto_programt::targett assume = havoc_writes_code.add_instruction(ASSUME); - assume->guard = invariant; - assume->function = loop_head->function; - assume->source_location = loop_head->source_location; - } - - // change the back edge into assume(!guard) - loop_end->targets.clear(); - loop_end->type=ASSUME; - if(loop_head->is_goto()) - { - loop_end->guard = loop_head->guard; - } - else - { - loop_end->guard = boolean_negate(loop_end->guard); - } - - // Change the loop head to assume the guard if a for/while loop. - // This needs to be done after we case on what loop_head is in the previous - // section of setup. - if(loop_head->is_goto()) - loop_head->make_assumption(boolean_negate(loop_head->guard)); - - // Now havoc at the loop head. Use insert_before_swap to preserve jumps to - // loop head. - goto_function.body.insert_before_swap(loop_head, havoc_all_code); - - // Now havoc at the loop end. Use insert_before_swap to preserve jumps to loop - // end. - goto_function.body.insert_before_swap(loop_end, havoc_writes_code); -} - void code_contractst::apply_contract( goto_programt &goto_program, goto_programt::targett target) @@ -302,8 +152,6 @@ void code_contractst::apply_contract( // TODO: Havoc write set of the function between assert and ensure. target->make_assumption(ensures); - - summarized.insert(function); } void code_contractst::apply_invariant( @@ -429,17 +277,17 @@ void code_contractst::check_contract( // build skip so that if(nondet) can refer to it goto_programt tmp_skip; - goto_programt::targett skip = tmp_skip.add_instruction(SKIP); - skip->function = dest.instructions.front().function; - skip->source_location = ensures.source_location(); + goto_programt::targett skip=tmp_skip.add_instruction(SKIP); + skip->function=dest.instructions.front().function; + skip->source_location=ensures.source_location(); goto_programt check; // if(nondet) - goto_programt::targett g = check.add_instruction(); + goto_programt::targett g=check.add_instruction(); g->make_goto(skip, side_effect_expr_nondett(bool_typet())); - g->function = skip->function; - g->source_location = skip->source_location; + g->function=skip->function; + g->source_location=skip->source_location; // prepare function call including all declarations code_function_callt call; @@ -451,16 +299,16 @@ void code_contractst::check_contract( // void functions seem to be handled by goto-cc if(goto_function.type.return_type() != empty_typet()) { - goto_programt::targett d = check.add_instruction(DECL); - d->function = skip->function; - d->source_location = skip->source_location; + goto_programt::targett d=check.add_instruction(DECL); + d->function=skip->function; + d->source_location=skip->source_location; symbol_exprt r = new_tmp_symbol(goto_function.type.return_type(), d->source_location) .symbol_expr(); - d->code = code_declt(r); + d->code=code_declt(r); - call.lhs() = r; + call.lhs()=r; symbol_exprt old( "__CPROVER_return_value", goto_function.type.return_type()); @@ -470,13 +318,13 @@ void code_contractst::check_contract( // decl parameter1 ... for(const auto &p_it : goto_function.type.parameters()) { - goto_programt::targett d = check.add_instruction(DECL); - d->function = skip->function; - d->source_location = skip->source_location; + goto_programt::targett d=check.add_instruction(DECL); + d->function=skip->function; + d->source_location=skip->source_location; symbol_exprt p = new_tmp_symbol(p_it.type(), d->source_location).symbol_expr(); - d->code = code_declt(p); + d->code=code_declt(p); call.arguments().push_back(p); @@ -490,26 +338,26 @@ void code_contractst::check_contract( // assume(requires) if(requires.is_not_nil()) { - goto_programt::targett a = check.add_instruction(); + goto_programt::targett a=check.add_instruction(); a->make_assumption(requires); - a->function = skip->function; - a->source_location = requires.source_location(); + a->function=skip->function; + a->source_location=requires.source_location(); // rewrite any use of parameters replace(a->guard); } // ret=function(parameter1, ...) - goto_programt::targett f = check.add_instruction(); + goto_programt::targett f=check.add_instruction(); f->make_function_call(call); - f->function = skip->function; - f->source_location = skip->source_location; + f->function=skip->function; + f->source_location=skip->source_location; // assert(ensures) - goto_programt::targett a = check.add_instruction(); + goto_programt::targett a=check.add_instruction(); a->make_assertion(ensures); - a->function = skip->function; - a->source_location = ensures.source_location(); + a->function=skip->function; + a->source_location=ensures.source_location(); // rewrite any use of __CPROVER_return_value replace(a->guard); @@ -608,25 +456,6 @@ void code_contractst::check_apply_invariant( goto_function.body.insert_before_swap(loop_head, havoc_code); } -void code_contractst::code_contracts( - goto_functionst::goto_functiont &goto_function) -{ - local_may_aliast local_may_alias(goto_function); - natural_loops_mutablet natural_loops(goto_function.body); - - // iterate over the (natural) loops in the function - for(const auto &l_it : natural_loops.loop_map) - { - check_apply_invariants( - goto_function, local_may_alias, l_it.first, l_it.second); - } - - // look at all function calls - Forall_goto_program_instructions(it, goto_function.body) - if(it->is_function_call()) - apply_contract(goto_function.body, it); -} - const symbolt &code_contractst::new_tmp_symbol( const typet &type, const source_locationt &source_location) @@ -640,125 +469,6 @@ const symbolt &code_contractst::new_tmp_symbol( symbol_table); } -void code_contractst::add_contract_check( - const irep_idt &function, - goto_programt &dest) -{ - PRECONDITION(!dest.instructions.empty()); - - goto_functionst::function_mapt::iterator f_it= - goto_functions.function_map.find(function); - assert(f_it!=goto_functions.function_map.end()); - - const goto_functionst::goto_functiont &gf=f_it->second; - - exprt requires = static_cast(gf.type.find(ID_C_spec_requires)); - exprt ensures = static_cast(gf.type.find(ID_C_spec_ensures)); - assert(ensures.is_not_nil()); - - // build: - // if(nondet) - // decl ret - // decl parameter1 ... - // assume(requires) [optional] - // ret=function(parameter1, ...) - // assert(ensures) - // assume(false) - // skip: ... - - // build skip so that if(nondet) can refer to it - goto_programt tmp_skip; - goto_programt::targett skip=tmp_skip.add_instruction(SKIP); - skip->function=dest.instructions.front().function; - skip->source_location=ensures.source_location(); - - goto_programt check; - - // if(nondet) - goto_programt::targett g=check.add_instruction(); - g->make_goto( - skip, side_effect_expr_nondett(bool_typet(), skip->source_location)); - g->function=skip->function; - g->source_location=skip->source_location; - - // prepare function call including all declarations - code_function_callt call(ns.lookup(function).symbol_expr()); - replace_symbolt replace; - - // decl ret - if(gf.type.return_type()!=empty_typet()) - { - goto_programt::targett d=check.add_instruction(DECL); - d->function=skip->function; - d->source_location=skip->source_location; - - symbol_exprt r= - new_tmp_symbol(gf.type.return_type(), - d->source_location).symbol_expr(); - d->code=code_declt(r); - - call.lhs()=r; - - symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type()); - replace.insert(ret_val, r); - } - - // decl parameter1 ... - for(const auto &p_it : gf.type.parameters()) - { - goto_programt::targett d=check.add_instruction(DECL); - d->function=skip->function; - d->source_location=skip->source_location; - - symbol_exprt p = - new_tmp_symbol(p_it.type(), d->source_location).symbol_expr(); - d->code=code_declt(p); - - call.arguments().push_back(p); - - if(!p_it.get_identifier().empty()) - { - symbol_exprt cur_p(p_it.get_identifier(), p_it.type()); - replace.insert(cur_p, p); - } - } - - // rewrite any use of parameters - replace(requires); - replace(ensures); - - // assume(requires) - if(requires.is_not_nil()) - { - goto_programt::targett a=check.add_instruction(); - a->make_assumption(requires); - a->function=skip->function; - a->source_location=requires.source_location(); - } - - // ret=function(parameter1, ...) - goto_programt::targett f=check.add_instruction(); - f->make_function_call(call); - f->function=skip->function; - f->source_location=skip->source_location; - - // assert(ensures) - goto_programt::targett a=check.add_instruction(); - a->make_assertion(ensures); - a->function=skip->function; - a->source_location=ensures.source_location(); - - // assume(false) - goto_programt::targett af=check.add_instruction(); - af->make_assumption(false_exprt()); - af->function=skip->function; - af->source_location=ensures.source_location(); - - // prepend the new code to dest - check.destructive_append(tmp_skip); - dest.destructive_insert(dest.instructions.begin(), check); -} - void code_contractst::apply_code_contracts() { Forall_goto_functions(it, goto_functions) From 724ed5210250effbcdc760bb450f200ecb4f2b2d Mon Sep 17 00:00:00 2001 From: klaas Date: Wed, 1 Aug 2018 09:51:41 -0400 Subject: [PATCH 07/16] Cleans up some loops to have braces --- src/analyses/dependence_graph.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index e84ba05cb18..07d70522331 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -174,7 +174,9 @@ void dep_graph_domaint::data_dependencies( { bool found=false; for(const auto &wr : w_range.second) + { for(const auto &r_range : r_ranges) + { if(!found && may_be_def_use_pair(wr.first, wr.second, r_range.first, r_range.second)) @@ -183,6 +185,8 @@ void dep_graph_domaint::data_dependencies( data_deps.insert(w_range.first); found=true; } + } + } } dep_graph.reaching_definitions()[to].clear_cache(it->first); From 474be8fea3a06245b26ab499984d301b5985ce12 Mon Sep 17 00:00:00 2001 From: klaas Date: Thu, 28 Jun 2018 12:04:05 -0400 Subject: [PATCH 08/16] 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 | 2 +- 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 | 22 ++++----- src/util/simplify_expr_pointer.cpp | 18 ++++---- src/util/std_expr.h | 47 +++++++++++++++++++- 12 files changed, 79 insertions(+), 31 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 7b639f38142..79ebce402ef 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2238,7 +2238,7 @@ exprt c_typecheck_baset::do_special_functions( throw 0; } - exprt dynamic_object_expr=exprt(ID_dynamic_object, expr.type()); + exprt dynamic_object_expr = exprt(ID_is_dynamic_object, expr.type()); dynamic_object_expr.operands()=expr.arguments(); dynamic_object_expr.add_source_location()=source_location; diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index d574c539d6f..fba9dd763ba 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -3531,8 +3531,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 b6cd92369d9..5a55e8c0307 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) @@ -736,7 +736,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 5966fb87fd3..f3cbbf67c72 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -1399,7 +1399,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 8798f7758f3..10082ccaa63 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -449,6 +449,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 a28d252a511..e08ded41a97 100644 --- a/src/util/pointer_predicates.cpp +++ b/src/util/pointer_predicates.cpp @@ -71,7 +71,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 74a3cab7c93..97caf577944 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2152,8 +2152,8 @@ 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) - result=simplify_dynamic_object(expr) && result; + else if(expr.id() == ID_is_dynamic_object) + 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_object_size) diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index 5e192292666..3dd7d8601e1 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 e45bf34891e..837dc31edb5 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -1707,11 +1707,12 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr) if(expr.op0().id()==ID_address_of && expr.op0().operands().size()==1) { - if(expr.op0().op0().id()==ID_symbol || - expr.op0().op0().id()==ID_dynamic_object || - expr.op0().op0().id()==ID_member || - expr.op0().op0().id()==ID_index || - expr.op0().op0().id()==ID_string_constant) + if( + expr.op0().op0().id() == ID_symbol || + 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) { expr=false_exprt(); return false; @@ -1723,11 +1724,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 a5025f09b9b..2fe3690c673 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -467,10 +467,10 @@ bool simplify_exprt::simplify_inequality_pointer_object(exprt &expr) if(op.id()==ID_address_of) { - if(op.operands().size()!=1 || - (op.op0().id()!=ID_symbol && - op.op0().id()!=ID_dynamic_object && - op.op0().id()!=ID_string_constant)) + if( + op.operands().size() != 1 || + (op.op0().id() != ID_symbol && op.op0().id() != ID_is_dynamic_object && + op.op0().id() != ID_string_constant)) return true; } else if(op.id()!=ID_constant || @@ -513,18 +513,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 525ffab6b5a..6e42cd98104 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -2271,8 +2271,53 @@ inline void validate_expr(const dynamic_object_exprt &value) validate_operands(value, 2, "Dynamic object must have two operands"); } +/*! \brief 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) + { + } +}; + +/*! \brief Cast a generic exprt to a \ref is_dynamic_object_exprt + * + * This is an unchecked conversion. \a expr must be known to be \ref + * is_dynamic_object_exprt. + * + * \param expr Source expression + * \return Object of type \ref is_dynamic_object_exprt + * + * \ingroup gr_std_expr +*/ +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 +/*! \brief semantic type conversion +*/ class typecast_exprt:public unary_exprt { public: From 248accfc2471545c33d819f8b3077720cfb00350 Mon Sep 17 00:00:00 2001 From: klaas Date: Thu, 2 Aug 2018 16:54:10 -0400 Subject: [PATCH 09/16] Turns some checks into DATA_INVARIANTs --- src/solvers/flattening/bv_pointers.cpp | 22 +++++++++++----------- src/util/simplify_expr_pointer.cpp | 6 ++++-- 2 files changed, 15 insertions(+), 13 deletions(-) diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index 5a55e8c0307..c52f06caadf 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -47,19 +47,19 @@ literalt bv_pointerst::convert_rest(const exprt &expr) } else if(expr.id() == ID_is_dynamic_object) { - if(operands.size()==1 && - operands[0].type().id()==ID_pointer) - { - // we postpone - literalt l=prop.new_variable(); + DATA_INVARIANT( + operands.size() == 1 && operands[0].type().id() == ID_pointer, + std::string("is_dynamic_object_exprt should have one") + + "operand, which should have pointer type."); + // we postpone + literalt l = prop.new_variable(); - postponed_list.push_back(postponedt()); - postponed_list.back().op=convert_bv(operands[0]); - postponed_list.back().bv.push_back(l); - postponed_list.back().expr=expr; + postponed_list.push_back(postponedt()); + postponed_list.back().op = convert_bv(operands[0]); + postponed_list.back().bv.push_back(l); + postponed_list.back().expr = expr; - return l; - } + return l; } else if(expr.id()==ID_lt || expr.id()==ID_le || expr.id()==ID_gt || expr.id()==ID_ge) diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index 2fe3690c673..97b77096b99 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -515,8 +515,10 @@ bool simplify_exprt::simplify_pointer_object(exprt &expr) bool simplify_exprt::simplify_is_dynamic_object(exprt &expr) { - // This should hold as a result of the expr ID being is_dynamic_object. - PRECONDITION(expr.operands().size() == 1); + DATA_INVARIANT( + expr.operands().size() == 1 && expr.op0().type().id() == ID_pointer, + std::string("is_dynamic_object_exprt should have one") + + "operand, which should have pointer type."); exprt &op=expr.op0(); From 4a0ea4b70335bb0313d9e41a830472dc96a1d658 Mon Sep 17 00:00:00 2001 From: klaas Date: Fri, 25 May 2018 15:33:37 -0400 Subject: [PATCH 10/16] Fixes bugs making goto_rw too conservative When handling the case of pointers, goto_rw would mark both the object pointed to and the pointer itself as written. For example, if x = &i, the line `*x = 1' would yield a write set containing both x and i, instead of just i. This resolves that issue by ensuring that value_set_dereference always gives at least one object that the dereference can refer to. This also resolves a bug wherein &a is marked as reading from a by removing the ID_symbol special case from get_objects_address_of.A --- src/analyses/goto_rw.cpp | 28 ++++++++++--------- src/analyses/reaching_definitions.cpp | 17 +++++------ .../value_set_dereference.cpp | 8 ++++-- 3 files changed, 28 insertions(+), 25 deletions(-) diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index b2386f73f96..aee94eacffb 100644 --- a/src/analyses/goto_rw.cpp +++ b/src/analyses/goto_rw.cpp @@ -138,8 +138,6 @@ void rw_range_sett::get_objects_dereference( { const exprt &pointer=deref.pointer(); get_objects_rec(get_modet::READ, pointer); - if(mode!=get_modet::READ) - get_objects_rec(mode, pointer); } void rw_range_sett::get_objects_byte_extract( @@ -430,16 +428,18 @@ void rw_range_sett::get_objects_typecast( void rw_range_sett::get_objects_address_of(const exprt &object) { - if(object.id() == ID_string_constant || - object.id() == ID_label || - object.id() == ID_array || - object.id() == ID_null_object) + if( + object.id() == ID_symbol || object.id() == ID_string_constant || + object.id() == ID_label || object.id() == ID_array || + object.id() == ID_null_object) + { // constant, nothing to do return; - else if(object.id()==ID_symbol) - get_objects_rec(get_modet::READ, object); + } else if(object.id()==ID_dereference) + { get_objects_rec(get_modet::READ, object); + } else if(object.id()==ID_index) { const index_exprt &index=to_index_expr(object); @@ -543,6 +543,11 @@ void rw_range_sett::get_objects_rec( get_objects_array(mode, to_array_expr(expr), range_start, size); else if(expr.id()==ID_struct) get_objects_struct(mode, to_struct_expr(expr), range_start, size); + else if(expr.id() == ID_dynamic_object) + { + const auto obj_instance = to_dynamic_object_expr(expr).get_instance(); + add(mode, "goto_rw::dynamic_object-" + std::to_string(obj_instance), 0, -1); + } else if(expr.id()==ID_symbol) { const symbol_exprt &symbol=to_symbol_expr(expr); @@ -586,11 +591,6 @@ void rw_range_sett::get_objects_rec( { // dereferencing may yield some weird ones, ignore these } - else if(mode==get_modet::LHS_W) - { - forall_operands(it, expr) - get_objects_rec(mode, *it); - } else throw "rw_range_sett: assignment to `"+expr.id_string()+"' not handled"; } @@ -630,6 +630,8 @@ void rw_range_set_value_sett::get_objects_dereference( exprt object=deref; dereference(target, object, ns, value_sets); + PRECONDITION(object.is_not_nil()); + auto type_bits = pointer_offset_bits(object.type(), ns); range_spect new_size; diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp index e60efc7daa0..1c3586cf6da 100644 --- a/src/analyses/reaching_definitions.cpp +++ b/src/analyses/reaching_definitions.cpp @@ -319,20 +319,17 @@ void rd_range_domaint::transform_assign( { const irep_idt &identifier=it->first; // ignore symex::invalid_object - const symbolt *symbol_ptr; - if(ns.lookup(identifier, symbol_ptr)) + const symbolt *symbol_ptr = nullptr; + bool not_found = ns.lookup(identifier, symbol_ptr); + if(not_found && has_prefix(id2string(identifier), "symex::invalid_object")) continue; - INVARIANT_STRUCTURED( - symbol_ptr!=nullptr, - nullptr_exceptiont, - "Symbol is in symbol table"); const range_domaint &ranges=rw_set.get_ranges(it); - if(is_must_alias && - (!rd.get_is_threaded()(from) || - (!symbol_ptr->is_shared() && - !rd.get_is_dirty()(identifier)))) + if( + is_must_alias && (!rd.get_is_threaded()(from) || + (symbol_ptr != nullptr && symbol_ptr->is_shared() && + !rd.get_is_dirty()(identifier)))) for(const auto &range : ranges) kill(identifier, range.first, range.second); diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 7eb546f92aa..a658479f818 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -316,8 +316,12 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( // this is also our guard result.pointer_guard = dynamic_object(pointer_expr); - // can't remove here, turn into *p - result.value=dereference_exprt(pointer_expr, dereference_type); + // TODO should this be object or root_object? + // TODO It's unclear whether this is a good approach to take --- it + // successfully ensures that every (non-null) dereference points to + // something, making the write set computation work correctly, but dynamic + // objects do not seem to be intended to be used in this way. + result.value = object; } else if(root_object.id()==ID_integer_address) { From 21e6d39f89c231341a4996a72dcb08e06ad27df5 Mon Sep 17 00:00:00 2001 From: klaas Date: Tue, 31 Jul 2018 10:54:06 -0400 Subject: [PATCH 11/16] Adds slice24 test. --- regression/goto-instrument/slice24/main.c | 20 ++++++++++++++++++++ regression/goto-instrument/slice24/test.desc | 8 ++++++++ 2 files changed, 28 insertions(+) create mode 100644 regression/goto-instrument/slice24/main.c create mode 100644 regression/goto-instrument/slice24/test.desc diff --git a/regression/goto-instrument/slice24/main.c b/regression/goto-instrument/slice24/main.c new file mode 100644 index 00000000000..6989dc105d5 --- /dev/null +++ b/regression/goto-instrument/slice24/main.c @@ -0,0 +1,20 @@ +#include +#include + +static void f(int *x) +{ + *x = 5; +} +static void g(int *x) +{ + assert(*x == 5); +} + +int main(int argc, char **argv) +{ + int *x = (int *)malloc(sizeof(int)); + f(x); + g(x); + + return 0; +} diff --git a/regression/goto-instrument/slice24/test.desc b/regression/goto-instrument/slice24/test.desc new file mode 100644 index 00000000000..3906443eafc --- /dev/null +++ b/regression/goto-instrument/slice24/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +main.c +--full-slice --add-library +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +Data dependencies across function calls are still not working correctly. From 599ae6200e2d75412ab5b199953424e4334076b0 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 5 Jun 2018 11:19:42 +0000 Subject: [PATCH 12/16] Code contracts: match up introducing/removing parameter map modifications Code contracts that introduce local declarations result in nested typecheck_declaration calls. The artificial __CPROVER_return_value symbol must then be added/removed by a single call only. --- regression/ansi-c/code_contracts1/main.c | 21 +++++++++++++++++++++ regression/ansi-c/code_contracts1/test.desc | 8 ++++++++ src/ansi-c/c_typecheck_base.cpp | 8 ++++++-- 3 files changed, 35 insertions(+), 2 deletions(-) create mode 100644 regression/ansi-c/code_contracts1/main.c create mode 100644 regression/ansi-c/code_contracts1/test.desc diff --git a/regression/ansi-c/code_contracts1/main.c b/regression/ansi-c/code_contracts1/main.c new file mode 100644 index 00000000000..b2c1a16a0c6 --- /dev/null +++ b/regression/ansi-c/code_contracts1/main.c @@ -0,0 +1,21 @@ +int foo() __CPROVER_ensures(__CPROVER_forall { + int i; + 1 == 1 +}) +{ + return 1; +} + +int bar() __CPROVER_ensures(__CPROVER_forall { + int i; + 1 == 1 +} && __CPROVER_return_value == 1) +{ + return 1; +} + +int main() +{ + foo(); + bar(); +} diff --git a/regression/ansi-c/code_contracts1/test.desc b/regression/ansi-c/code_contracts1/test.desc new file mode 100644 index 00000000000..466da18b2b5 --- /dev/null +++ b/regression/ansi-c/code_contracts1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index 91466d3ed6c..1dcd025584c 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -743,11 +743,15 @@ void c_typecheck_baset::typecheck_declaration( typet ret_type=empty_typet(); if(new_symbol.type.id()==ID_code) ret_type=to_code_type(new_symbol.type).return_type(); - assert(parameter_map.empty()); if(ret_type.id()!=ID_empty) + { + DATA_INVARIANT( + parameter_map.empty(), "parameter map should be cleared"); parameter_map[CPROVER_PREFIX "return_value"] = ret_type; + } typecheck_spec_expr(contract, ID_C_spec_ensures); - parameter_map.clear(); + if(ret_type.id() != ID_empty) + parameter_map.clear(); if(contract.find(ID_C_spec_requires).is_not_nil()) new_symbol.type.add(ID_C_spec_requires)= From 878488020886d2c8534b99d6054b7326fe28e287 Mon Sep 17 00:00:00 2001 From: klaas Date: Wed, 1 Aug 2018 16:35:29 -0400 Subject: [PATCH 13/16] Adds havocking for function calls This commit changes the behaviour of --apply-code-contracts on function calls. Previously, when applying contracts, a function call would be replaced by an assertion that the precondition holds, followed by an assumption that the postcondition holds. This change inserts between that assert/assume pair code that sets all variables that could be modified by the function being called to be nondeterministic. --- src/goto-instrument/code_contracts.cpp | 49 +++++++++++++++++--------- 1 file changed, 32 insertions(+), 17 deletions(-) diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 614096950f5..411980dcfdb 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -23,6 +23,7 @@ Date: February 2016 #include +#include "function_modifies.h" #include "loop_utils.h" enum class contract_opst @@ -57,6 +58,7 @@ class code_contractst void apply_contract( goto_programt &goto_program, + const local_may_aliast &local_may_alias, goto_programt::targett target); void apply_invariant( @@ -83,6 +85,7 @@ class code_contractst void code_contractst::apply_contract( goto_programt &goto_program, + const local_may_aliast &local_may_alias, goto_programt::targett target) { const code_function_callt &call=to_code_function_call(target->code); @@ -112,6 +115,23 @@ void code_contractst::apply_contract( } } + // find out what can be written by the function + // TODO Use a better write-set analysis. + modifiest modifies; + function_modifiest function_modifies(goto_functions); + + // Handle return value of the function + if(call.lhs().is_not_nil()) + { + function_modifies.get_modifies_lhs( + local_may_alias, target, call.lhs(), modifies); + } + function_modifies(call.function(), modifies); + + // build the havocking code + goto_programt havoc_code; + build_havoc_code(target, modifies, havoc_code); + // replace formal parameters by arguments, replace return replace_symbolt replace; @@ -149,7 +169,9 @@ void code_contractst::apply_contract( goto_program.insert_before_swap(target, a); ++target; } - // TODO: Havoc write set of the function between assert and ensure. + + // TODO some sort of replacement on havoc code + goto_program.destructive_insert(target, havoc_code); target->make_assumption(ensures); } @@ -160,7 +182,7 @@ void code_contractst::apply_invariant( const goto_programt::targett loop_head, const loopt &loop) { - assert(!loop.empty()); + PRECONDITION(!loop.empty()); // find the last back edge goto_programt::targett loop_end = loop_head; @@ -181,8 +203,6 @@ void code_contractst::apply_invariant( return; } - // TODO: Allow for not havocking in the for/while case - // change H: loop; E: ... // to // H: assert(invariant); @@ -219,8 +239,6 @@ void code_contractst::apply_invariant( } // assume !guard - // TODO: consider breaks and how they're implemented. - // TODO: Also consider continues and whether they jump to loop end or head { goto_programt::targett assume = havoc_code.add_instruction(ASSUME); @@ -252,7 +270,7 @@ void code_contractst::check_contract( goto_functionst::goto_functiont &goto_function, goto_programt &dest) { - assert(!dest.instructions.empty()); + PRECONDITION(!dest.instructions.empty()); exprt requires = static_cast(goto_function.type.find(ID_C_spec_requires)); @@ -335,6 +353,10 @@ void code_contractst::check_contract( } } + // rewrite any use of parameters + replace(requires); + replace(ensures); + // assume(requires) if(requires.is_not_nil()) { @@ -342,9 +364,6 @@ void code_contractst::check_contract( a->make_assumption(requires); a->function=skip->function; a->source_location=requires.source_location(); - - // rewrite any use of parameters - replace(a->guard); } // ret=function(parameter1, ...) @@ -359,9 +378,6 @@ void code_contractst::check_contract( a->function=skip->function; a->source_location=ensures.source_location(); - // rewrite any use of __CPROVER_return_value - replace(a->guard); - // prepend the new code to dest check.destructive_append(tmp_skip); dest.destructive_insert(dest.instructions.begin(), check); @@ -373,7 +389,7 @@ void code_contractst::check_apply_invariant( const goto_programt::targett loop_head, const loopt &loop) { - assert(!loop.empty()); + PRECONDITION(!loop.empty()); // find the last back edge goto_programt::targett loop_end = loop_head; @@ -488,7 +504,7 @@ void code_contractst::apply_code_contracts() { if(it->is_function_call()) { - apply_contract(goto_function.body, it); + apply_contract(goto_function.body, local_may_alias, it); } } } @@ -520,7 +536,7 @@ void code_contractst::check_code_contracts() { if(it->is_function_call()) { - apply_contract(goto_function.body, it); + apply_contract(goto_function.body, local_may_alias, it); } } } @@ -530,7 +546,6 @@ void code_contractst::check_code_contracts() check_contract(it->first, it->second, i_it->second.body); } - // remove skips remove_skip(i_it->second.body); goto_functions.update(); From 98c9bf79e642696e5b10e842ec0cbc4b24a336a6 Mon Sep 17 00:00:00 2001 From: klaas Date: Thu, 2 Aug 2018 13:46:31 -0400 Subject: [PATCH 14/16] Fixes initialization for code contracts Because code contracts should be checked in an environment constrained only by the preconditions, we want to check contracts before initializing the dead and deallocated objects --- otherwise, we fail to check the cases where a pointer argument to a function points to a dead or deallocated object but is not NULL. This commit resolves these issues by temporarily initializing dead and deallocated objects to be the same fixed object before checking contracts, and then performing the standard initialization to NULL. --- src/goto-instrument/code_contracts.cpp | 50 ++++++++++++++++++++++++-- 1 file changed, 48 insertions(+), 2 deletions(-) diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 411980dcfdb..4200570b89b 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -13,6 +13,9 @@ Date: February 2016 #include "code_contracts.h" +#include +#include +#include #include #include #include @@ -517,6 +520,7 @@ void code_contractst::check_code_contracts() goto_functionst::function_mapt::iterator i_it= goto_functions.function_map.find(INITIALIZE_FUNCTION); assert(i_it!=goto_functions.function_map.end()); + goto_programt &init_function = i_it->second.body; Forall_goto_functions(it, goto_functions) { @@ -543,10 +547,52 @@ void code_contractst::check_code_contracts() Forall_goto_functions(it, goto_functions) { - check_contract(it->first, it->second, i_it->second.body); + check_contract(it->first, it->second, init_function); } - remove_skip(i_it->second.body); + // Partially initialize state + goto_programt init_code; + + goto_programt::targett d = init_code.add_instruction(DECL); + d->function = i_it->first; + // TODO add source location + // d->source_location = + + symbol_exprt tmp_var = + new_tmp_symbol(void_typet(), d->source_location).symbol_expr(); + d->code = code_declt(tmp_var); + d->code.add_source_location() = d->source_location; + + { + const symbol_exprt &deallocated_expr = + ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr(); + + goto_programt::targett a = init_code.add_instruction(ASSIGN); + a->function = i_it->first; + // TODO add source location + // a->source_location = + address_of_exprt rhs(tmp_var, to_pointer_type(deallocated_expr.type())); + a->code = code_assignt(deallocated_expr, rhs); + a->code.add_source_location() = a->source_location; + } + + { + const symbol_exprt &dead_expr = + ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr(); + + goto_programt::targett a = init_code.add_instruction(ASSIGN); + a->function = i_it->first; + // TODO add source location + // a->source_location = + address_of_exprt rhs(tmp_var, to_pointer_type(dead_expr.type())); + a->code = code_assignt(dead_expr, rhs); + a->code.add_source_location() = a->source_location; + } + + init_function.destructive_insert( + init_function.instructions.begin(), init_code); + + remove_skip(init_function); goto_functions.update(); } From 47d43e6ead58f6285ec86f1d5f27a6a34f9b9f17 Mon Sep 17 00:00:00 2001 From: klaas Date: Thu, 14 Jun 2018 15:36:58 -0400 Subject: [PATCH 15/16] Makes code contracts use goto_rw for write sets This change replaces the use of local_may_alias analysis in code contracts with the more accurate goto_rw analysis. These analyses are used to find the set of variables written to by a loop or function so that we know which variables to make nondeterministic when abstracting out those pieces of code. --- .../contracts/function_check_05/test.desc | 11 +- src/goto-instrument/code_contracts.cpp | 114 +++++++++++++----- src/goto-instrument/loop_utils.cpp | 38 ------ src/goto-instrument/loop_utils.h | 6 - 4 files changed, 92 insertions(+), 77 deletions(-) diff --git a/regression/contracts/function_check_05/test.desc b/regression/contracts/function_check_05/test.desc index 77e210f10d8..7c82bf97f02 100644 --- a/regression/contracts/function_check_05/test.desc +++ b/regression/contracts/function_check_05/test.desc @@ -1,10 +1,9 @@ -KNOWNBUG +CORE main.c --check-code-contracts -^\[main.assertion.1\] assertion y == 0: FAILURE$ -^\[main.assertion.2\] assertion z == 1: SUCCESS$ -^\[foo.1\] : SUCCESS$ -^VERIFICATION SUCCESSFUL$ +^\[main.assertion.1\] .* assertion y == 0: FAILURE$ +^\[main.assertion.2\] .* assertion z == 1: SUCCESS$ +^\[foo.1\] .* : SUCCESS$ +^VERIFICATION FAILED$ -- -- -Contract checking does not properly havoc function calls. diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 4200570b89b..19b77d004fe 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -18,15 +18,17 @@ Date: February 2016 #include #include #include +#include #include #include -#include +#include #include -#include "function_modifies.h" +#include + #include "loop_utils.h" enum class contract_opst @@ -61,12 +63,12 @@ class code_contractst void apply_contract( goto_programt &goto_program, - const local_may_aliast &local_may_alias, + value_setst &value_sets, goto_programt::targett target); void apply_invariant( goto_functionst::goto_functiont &goto_function, - const local_may_aliast &local_may_alias, + value_setst &value_sets, const goto_programt::targett loop_head, const loopt &loop); @@ -77,7 +79,7 @@ class code_contractst void check_apply_invariant( goto_functionst::goto_functiont &goto_function, - const local_may_aliast &local_may_alias, + value_setst &value_sets, const goto_programt::targett loop_head, const loopt &loop); @@ -88,7 +90,7 @@ class code_contractst void code_contractst::apply_contract( goto_programt &goto_program, - const local_may_aliast &local_may_alias, + value_setst &value_sets, goto_programt::targett target) { const code_function_callt &call=to_code_function_call(target->code); @@ -119,17 +121,27 @@ void code_contractst::apply_contract( } // find out what can be written by the function - // TODO Use a better write-set analysis. modifiest modifies; - function_modifiest function_modifies(goto_functions); - // Handle return value of the function - if(call.lhs().is_not_nil()) + rw_range_set_value_sett rw_set(ns, value_sets); + goto_rw(goto_functions, function, rw_set); + forall_rw_range_set_w_objects(it, rw_set) { - function_modifies.get_modifies_lhs( - local_may_alias, target, call.lhs(), modifies); + // Skip over local variables of the function being called, as well as + // variables not in the namespace (e.g. symex::invalid_object) + const symbolt *symbol_ptr; + if(!ns.lookup(it->first, symbol_ptr)) + { + const std::string &name_string = id2string(symbol_ptr->name); + std::string scope_prefix(id2string(ns.lookup(function).name)); + scope_prefix += "::"; + + if(name_string.find(scope_prefix) == std::string::npos) + { + modifies.insert(ns.lookup(it->first).symbol_expr()); + } + } } - function_modifies(call.function(), modifies); // build the havocking code goto_programt havoc_code; @@ -162,6 +174,18 @@ void code_contractst::apply_contract( replace(requires); replace(ensures); + // Havoc the return value of the function call. + if(type.return_type() != empty_typet()) + { + const exprt &lhs = call.lhs(); + const exprt &rhs = side_effect_expr_nondett(call.lhs().type()); + target->make_assignment(code_assignt(lhs, rhs)); + } + else + { + target->make_skip(); + } + if(requires.is_not_nil()) { goto_programt::instructiont a(ASSERT); @@ -173,15 +197,19 @@ void code_contractst::apply_contract( ++target; } - // TODO some sort of replacement on havoc code goto_program.destructive_insert(target, havoc_code); - target->make_assumption(ensures); + { + goto_programt::targett a = goto_program.insert_after(target); + a->make_assumption(ensures); + a->function = target->function; + a->source_location = target->source_location; + } } void code_contractst::apply_invariant( goto_functionst::goto_functiont &goto_function, - const local_may_aliast &local_may_alias, + value_setst &value_sets, const goto_programt::targett loop_head, const loopt &loop) { @@ -216,7 +244,20 @@ void code_contractst::apply_invariant( // find out what can get changed in the loop modifiest modifies; - get_modifies(local_may_alias, loop, modifies); + + rw_range_set_value_sett rw_set(ns, value_sets); + for(const goto_programt::targett &inst : loop) + { + goto_rw(inst, rw_set); + } + forall_rw_range_set_w_objects(it, rw_set) + { + const symbolt *symbol_ptr; + if(!ns.lookup(it->first, symbol_ptr)) + { + modifies.insert(ns.lookup(it->first).symbol_expr()); + } + } // build the havocking code goto_programt havoc_code; @@ -388,7 +429,7 @@ void code_contractst::check_contract( void code_contractst::check_apply_invariant( goto_functionst::goto_functiont &goto_function, - const local_may_aliast &local_may_alias, + value_setst &value_sets, const goto_programt::targett loop_head, const loopt &loop) { @@ -406,7 +447,9 @@ void code_contractst::check_apply_invariant( exprt invariant = static_cast(loop_end->guard.find(ID_C_spec_loop_invariant)); if(invariant.is_nil()) + { return; + } // change H: loop; E: ... // to @@ -421,7 +464,20 @@ void code_contractst::check_apply_invariant( // find out what can get changed in the loop modifiest modifies; - get_modifies(local_may_alias, loop, modifies); + + rw_range_set_value_sett rw_set(ns, value_sets); + for(const goto_programt::targett &inst : loop) + { + goto_rw(inst, rw_set); + } + forall_rw_range_set_w_objects(it, rw_set) + { + const symbolt *symbol_ptr; + if(!ns.lookup(it->first, symbol_ptr)) + { + modifies.insert(ns.lookup(it->first).symbol_expr()); + } + } // build the havocking code goto_programt havoc_code; @@ -490,24 +546,26 @@ const symbolt &code_contractst::new_tmp_symbol( void code_contractst::apply_code_contracts() { + auto vs = util_make_unique(ns); + (*vs)(goto_functions); + std::unique_ptr value_sets = std::move(vs); + Forall_goto_functions(it, goto_functions) { goto_functionst::goto_functiont &goto_function = it->second; - // TODO: This aliasing check is insufficiently strong, in general. - local_may_aliast local_may_alias(goto_function); natural_loops_mutablet natural_loops(goto_function.body); for(const auto &l_it : natural_loops.loop_map) { - apply_invariant(goto_function, local_may_alias, l_it.first, l_it.second); + apply_invariant(goto_function, *value_sets, l_it.first, l_it.second); } Forall_goto_program_instructions(it, goto_function.body) { if(it->is_function_call()) { - apply_contract(goto_function.body, local_may_alias, it); + apply_contract(goto_function.body, *value_sets, it); } } } @@ -517,6 +575,10 @@ void code_contractst::apply_code_contracts() void code_contractst::check_code_contracts() { + auto vs = util_make_unique(ns); + (*vs)(goto_functions); + std::unique_ptr value_sets = std::move(vs); + goto_functionst::function_mapt::iterator i_it= goto_functions.function_map.find(INITIALIZE_FUNCTION); assert(i_it!=goto_functions.function_map.end()); @@ -526,21 +588,19 @@ void code_contractst::check_code_contracts() { goto_functionst::goto_functiont &goto_function = it->second; - // TODO: This aliasing check is insufficiently strong, in general. - local_may_aliast local_may_alias(goto_function); natural_loops_mutablet natural_loops(goto_function.body); for(const auto &l_it : natural_loops.loop_map) { check_apply_invariant( - goto_function, local_may_alias, l_it.first, l_it.second); + goto_function, *value_sets, l_it.first, l_it.second); } Forall_goto_program_instructions(it, goto_function.body) { if(it->is_function_call()) { - apply_contract(goto_function.body, local_may_alias, it); + apply_contract(goto_function.body, *value_sets, it); } } } diff --git a/src/goto-instrument/loop_utils.cpp b/src/goto-instrument/loop_utils.cpp index feb6df47145..4ab59238bc9 100644 --- a/src/goto-instrument/loop_utils.cpp +++ b/src/goto-instrument/loop_utils.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "loop_utils.h" -#include #include #include @@ -109,40 +108,3 @@ void get_modifies( } } } - -// TODO handle aliasing at all -void get_uses( - const local_may_aliast &local_may_alias, - const loopt &loop, - usest &uses) -{ - for(loopt::const_iterator i_it = loop.begin(); i_it != loop.end(); i_it++) - { - const goto_programt::instructiont &instruction = **i_it; - if(instruction.code.is_not_nil()) - { - for(const_depth_iteratort it = instruction.code.depth_begin(); - it != instruction.code.depth_end(); - ++it) - { - if((*it).id() == ID_symbol) - { - uses.insert(*it); - } - } - } - - if(instruction.guard.is_not_nil()) - { - for(const_depth_iteratort it = instruction.guard.depth_begin(); - it != instruction.guard.depth_end(); - ++it) - { - if((*it).id() == ID_symbol) - { - uses.insert(*it); - } - } - } - } -} diff --git a/src/goto-instrument/loop_utils.h b/src/goto-instrument/loop_utils.h index 1296374eff7..57407ecec1b 100644 --- a/src/goto-instrument/loop_utils.h +++ b/src/goto-instrument/loop_utils.h @@ -17,7 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com class local_may_aliast; typedef std::set modifiest; -typedef std::set usest; typedef const natural_loops_mutablet::natural_loopt loopt; void get_modifies( @@ -25,11 +24,6 @@ void get_modifies( const loopt &loop, modifiest &modifies); -void get_uses( - const local_may_aliast &local_may_alias, - const loopt &loop, - usest &uses); - void build_havoc_code( const goto_programt::targett loop_head, const modifiest &modifies, From abe1f5aeb34cbbfd252c515945b11f5e014454e5 Mon Sep 17 00:00:00 2001 From: klaas Date: Wed, 18 Jul 2018 14:33:00 -0400 Subject: [PATCH 16/16] Adds comments & help to code_contracts This commit adds some documentation to code contracts, and adds code contracts help text to goto-instrument --- src/goto-instrument/code_contracts.cpp | 32 +++++++++++++++++++ src/goto-instrument/code_contracts.h | 12 +++++++ .../goto_instrument_parse_options.cpp | 2 ++ 3 files changed, 46 insertions(+) diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 19b77d004fe..0b1af7d57a6 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -61,22 +61,54 @@ class code_contractst void code_contracts(goto_functionst::goto_functiont &goto_function); + /// Applies (but does not check) a function contract. This will assume that + /// the contract holds, and then use that assumption to remove the function + /// call located at target. + /// \param goto_program The goto program containing the target call site. + /// \param value_sets A value_setst object containing information about + /// aliasing in the goto program being analyzed + /// \param target An iterator pointing to the function call to be removed. void apply_contract( goto_programt &goto_program, value_setst &value_sets, goto_programt::targett target); + /// Applies (but does not check) a loop invariant. This will assume that the + /// loop invariant is indeed an invariant, and then use that assumption to + /// remove the loop. + /// \param goto_function The goto function containing the target loop. + /// \param value_sets A value_setst object containing information about + /// aliasing in the goto program being analyzed + /// \param loop_head An iterator pointing to the first instruction of the + /// target loop. + /// \param loop The loop being removed. void apply_invariant( goto_functionst::goto_functiont &goto_function, value_setst &value_sets, const goto_programt::targett loop_head, const loopt &loop); + /// Checks (but does not apply) a function contract. This will build a code + /// snippet to be inserted at dest which will check that the function contract + /// is satisfied. + /// \param function_id The id of the function being checked. + /// \param goto_function The goto_function object for the function + /// being checked. + /// \param dest An iterator pointing to the place to insert checking code. void check_contract( const irep_idt &function_id, goto_functionst::goto_functiont &goto_function, goto_programt &dest); + /// Checks and applies a loop invariant This will replace the loop with a code + /// snippet (based on the loop) which will check that the loop invariant is + /// indeed an invariant, and then use that invariant in what follows. + /// \param goto_function The goto function containing the target loop. + /// \param value_sets A value_setst object containing information about + /// aliasing in the goto program being analyzed + /// \param loop_head An iterator pointing to the first instruction of the + /// target loop. + /// \param loop The loop being removed. void check_apply_invariant( goto_functionst::goto_functiont &goto_function, value_setst &value_sets, diff --git a/src/goto-instrument/code_contracts.h b/src/goto-instrument/code_contracts.h index 7c7c02c09c0..87395007fff 100644 --- a/src/goto-instrument/code_contracts.h +++ b/src/goto-instrument/code_contracts.h @@ -19,4 +19,16 @@ class goto_modelt; void apply_code_contracts(goto_modelt &); void check_code_contracts(goto_modelt &); +// clang-format off +#define HELP_APPLY_CODE_CONTRACTS \ + " --apply-code-contracts Assume (without checking) that the contracts used in code hold\n" \ + " This will use __CPROVER_requires, __CPROVER_ensures,\n" \ + " and __CPROVER_loop_invariant as assumptions in order to avoid\n" \ + " checking code that is assumed to satisfy a specification.\n" +#define HELP_CHECK_CODE_CONTRACTS \ + " --check-code-contracts Assume (with checking) that the contracts used in code hold.\n" \ + " This differs from --apply-code-contracts in that in addition to\n" \ + " assuming specifications, it checks that they are correct.\n" +// clang-format on + #endif // CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 63e1a9e5eff..989053e1862 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1633,6 +1633,8 @@ void goto_instrument_parse_optionst::help() " --undefined-function-is-assume-false\n" // NOLINTNEXTLINE(whitespace/line_length) " convert each call to an undefined function to assume(false)\n" + HELP_APPLY_CODE_CONTRACTS + HELP_CHECK_CODE_CONTRACTS HELP_REPLACE_FUNCTION_BODY "\n" "Loop transformations:\n"