From 563ba56f215ef99694be2716f1e7febafe091953 Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Tue, 5 Mar 2019 15:14:41 -0500 Subject: [PATCH 1/5] Whitespace fix --- src/util/expr_util.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp index acb9dc99dbf..2e3e449cd07 100644 --- a/src/util/expr_util.cpp +++ b/src/util/expr_util.cpp @@ -33,6 +33,7 @@ bool is_lvalue(const exprt &expr) else return false; } + exprt make_binary(const exprt &expr) { const exprt::operandst &operands=expr.operands(); From 7c5ae5aa023ad7e7a8f84bac845fd2983124a7a5 Mon Sep 17 00:00:00 2001 From: klaas Date: Mon, 18 Jun 2018 17:09:40 -0400 Subject: [PATCH 2/5] 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 | 41 ++++ src/ansi-c/cprover_builtin_headers.h | 1 + src/ansi-c/expr2c.cpp | 3 + src/goto-instrument/Makefile | 1 + .../expand_pointer_predicates.cpp | 211 ++++++++++++++++++ .../expand_pointer_predicates.h | 23 ++ .../goto_instrument_parse_options.cpp | 7 + .../goto_instrument_parse_options.h | 1 + src/goto-symex/symex_builtin_functions.cpp | 71 +----- src/util/expr_util.cpp | 95 +++++++- src/util/expr_util.h | 12 + src/util/irep_ids.def | 1 + src/util/pointer_predicates.cpp | 41 ++++ src/util/pointer_predicates.h | 5 + 14 files changed, 439 insertions(+), 74 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 40fc7c21b78..f251ac5d572 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -34,6 +34,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "anonymous_member.h" #include "padding.h" +bool is_lvalue(const exprt &expr); + void c_typecheck_baset::typecheck_expr(exprt &expr) { if(expr.id()==ID_already_typechecked) @@ -2109,6 +2111,45 @@ 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) + { + if( + expr.arguments()[1].type() != ID_unsignedbv && + expr.arguments()[1].type() != ID_signedbv) + { + err_location(f_op); + error() << "size argument to points_to_valid_memory" + << " must be coercible to size_t" << eom; + throw 0; + } + same_object_expr = + points_to_valid_memory(expr.arguments()[0], expr.arguments()[1]); + } + else + { + 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 a00ee818d62..b68ed81018f 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -3432,6 +3432,9 @@ std::string expr2ct::convert_with_precedence( else if(src.id()==ID_good_pointer) return convert_function(src, "GOOD_POINTER", precedence=16); + else if(src.id() == ID_points_to_valid_memory) + return convert_function(src, "POINTS_TO_VALID_MEMORY", precedence = 16); + else if(src.id()==ID_object_size) return convert_function(src, "OBJECT_SIZE", precedence=16); diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index 8dc28944f66..04c393eb75a 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -32,6 +32,7 @@ SRC = accelerate/accelerate.cpp \ document_properties.cpp \ dot.cpp \ dump_c.cpp \ + expand_pointer_predicates.cpp \ full_slicer.cpp \ function.cpp \ function_modifies.cpp \ diff --git a/src/goto-instrument/expand_pointer_predicates.cpp b/src/goto-instrument/expand_pointer_predicates.cpp new file mode 100644 index 00000000000..c9e866eec89 --- /dev/null +++ b/src/goto-instrument/expand_pointer_predicates.cpp @@ -0,0 +1,211 @@ +/*******************************************************************\ + +Module: Expand pointer predicates in assertions/assumptions. + +Author: Klaas Pruiksma + +Date: June 2018 + +\*******************************************************************/ + +/// \file +/// Replace pointer predicates (e.g. __CPROVER_points_to_valid_memory) +/// in assumptions and assertions with suitable expressions and additional +/// instructions. + +#include "expand_pointer_predicates.h" + +#include + +#include +#include +#include +#include +#include +#include +#include +#include + +#include + +class expand_pointer_predicatest +{ +public: + expand_pointer_predicatest( + symbol_tablet &_symbol_table, + goto_functionst &_goto_functions) + : ns(_symbol_table), + symbol_table(_symbol_table), + goto_functions(_goto_functions), + local_bitvector_analysis(nullptr) + { + } + + void operator()(); + +protected: + namespacet ns; + symbol_tablet &symbol_table; + goto_functionst &goto_functions; + local_bitvector_analysist *local_bitvector_analysis; + + void expand_pointer_predicates(); + + void expand_assumption( + goto_functionst::goto_functiont &, + goto_programt::targett target, + exprt &assume_expr); + + void expand_assertion(exprt &assert_expr); + + const symbolt & + new_tmp_symbol(const typet &type, const source_locationt &source_location); +}; + +bool is_lvalue(const exprt &expr); + +void expand_pointer_predicatest::expand_pointer_predicates() +{ + Forall_goto_functions(f_it, goto_functions) + { + goto_functionst::goto_functiont &goto_function = f_it->second; + Forall_goto_program_instructions(i_it, goto_function.body) + { + if(i_it->is_assert()) + { + expand_assertion(i_it->guard); + } + else if(i_it->is_assume()) + { + expand_assumption(goto_function, i_it, i_it->guard); + } + else + { + continue; + } + } + } +} + +void expand_pointer_predicatest::expand_assumption( + goto_functionst::goto_functiont &goto_function, + goto_programt::targett target, + exprt &assume_expr) +{ + goto_programt &program = goto_function.body; + local_bitvector_analysist local_bitvector_analysis(goto_function, ns); + goto_programt assume_code; + for(depth_iteratort it = assume_expr.depth_begin(); + it != assume_expr.depth_end();) + { + if(it->id() == ID_points_to_valid_memory) + { + exprt &valid_memory_expr = it.mutate(); + exprt &pointer_expr = valid_memory_expr.op0(); + exprt size_expr = valid_memory_expr.op1(); + simplify(size_expr, ns); + + // This should be forced by typechecking. + INVARIANT( + pointer_expr.type().id() == ID_pointer && is_lvalue(pointer_expr), + "Invalid argument to valid_pointer."); + + local_bitvector_analysist::flagst flags = + local_bitvector_analysis.get(target, pointer_expr); + // Only create a new object if the pointer may be uninitialized. + if(flags.is_uninitialized() || flags.is_unknown()) + { + typet object_type = type_from_size(size_expr, ns); + + // Decl a new variable (which is therefore unconstrained) + goto_programt::targett d = assume_code.add_instruction(DECL); + d->source_location = assume_expr.source_location(); + const symbol_exprt obj = + new_tmp_symbol(object_type, d->source_location).symbol_expr(); + d->code = code_declt(obj); + + exprt rhs; + if(object_type.id() == ID_array) + { + rhs = typecast_exprt( + address_of_exprt(index_exprt(obj, from_integer(0, index_type()))), + pointer_expr.type()); + } + else + { + rhs = address_of_exprt(obj); + } + + // Point the relevant pointer to the new object + goto_programt::targett a = assume_code.add_instruction(ASSIGN); + a->source_location = assume_expr.source_location(); + a->code = code_assignt(pointer_expr, rhs); + a->code.add_source_location() = assume_expr.source_location(); + } + + // Because some uses of this occur before deallocated, dead, and malloc + // objects are initialized, we need to make some additional assumptions + // to clarify that our newly allocated object is not dead, deallocated, + // or outside the bounds of a malloc region. + + exprt check_expr = + points_to_valid_memory_def(pointer_expr, size_expr, ns); + valid_memory_expr.swap(check_expr); + it.next_sibling_or_parent(); + } + else + { + ++it; + } + } + + program.destructive_insert(target, assume_code); +} + +void expand_pointer_predicatest::expand_assertion(exprt &assert_expr) +{ + for(depth_iteratort it = assert_expr.depth_begin(); + it != assert_expr.depth_end();) + { + if(it->id() == ID_points_to_valid_memory) + { + // Build an expression that checks validity. + exprt &valid_memory_expr = it.mutate(); + exprt &pointer_expr = valid_memory_expr.op0(); + exprt &size_expr = valid_memory_expr.op1(); + + exprt check_expr = + points_to_valid_memory_def(pointer_expr, size_expr, ns); + valid_memory_expr.swap(check_expr); + it.next_sibling_or_parent(); + } + else + { + ++it; + } + } +} + +const symbolt &expand_pointer_predicatest::new_tmp_symbol( + const typet &type, + const source_locationt &source_location) +{ + return get_fresh_aux_symbol( + type, + id2string(source_location.get_function()), + "tmp_epp", + source_location, + ID_C, + symbol_table); +} + +void expand_pointer_predicatest::operator()() +{ + expand_pointer_predicates(); +} + +void expand_pointer_predicates(goto_modelt &goto_model) +{ + expand_pointer_predicatest( + goto_model.symbol_table, goto_model.goto_functions)(); +} diff --git a/src/goto-instrument/expand_pointer_predicates.h b/src/goto-instrument/expand_pointer_predicates.h new file mode 100644 index 00000000000..37d41d1023b --- /dev/null +++ b/src/goto-instrument/expand_pointer_predicates.h @@ -0,0 +1,23 @@ +/*******************************************************************\ + +Module: Expand pointer predicates in assertions/assumptions. + +Author: Klaas Pruiksma + +Date: June 2018 + +\*******************************************************************/ + +/// \file +/// Replace pointer predicates (e.g. __CPROVER_points_to_valid_memory) +/// in assumptions and assertions with suitable expressions and additional +/// instructions. + +#ifndef CPROVER_GOTO_INSTRUMENT_EXPAND_POINTER_PREDICATES_H +#define CPROVER_GOTO_INSTRUMENT_EXPAND_POINTER_PREDICATES_H + +class goto_modelt; + +void expand_pointer_predicates(goto_modelt &goto_model); + +#endif // CPROVER_GOTO_INSTRUMENT_EXPAND_POINTER_PREDICATES_H diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 1b868cdce13..15574ba15c0 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -82,6 +82,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "document_properties.h" #include "dot.h" #include "dump_c.h" +#include "expand_pointer_predicates.h" #include "full_slicer.h" #include "function.h" #include "havoc_loops.h" @@ -1068,6 +1069,11 @@ void goto_instrument_parse_optionst::instrument_goto_program() code_contracts(goto_model); } + if(cmdline.isset("expand-pointer-predicates")) + { + expand_pointer_predicates(goto_model); + } + // replace function pointers, if explicitly requested if(cmdline.isset("remove-function-pointers")) { @@ -1665,6 +1671,7 @@ void goto_instrument_parse_optionst::help() " --no-caching disable caching of intermediate results during transitive function inlining\n" // NOLINT(*) " --log log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*) " --remove-function-pointers replace function pointers by case statement over function calls\n" // NOLINT(*) + " --expand-pointer-predicates Expands predicates about pointers (e.g. __CPROVER_points_to_valid_memory) into a form useable by CBMC\n" // NOLINT(*) HELP_REMOVE_CALLS_NO_BODY HELP_REMOVE_CONST_FUNCTION_POINTERS " --add-library add models of C library functions\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 647ec904b0b..3ba111b923d 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -93,6 +93,7 @@ Author: Daniel Kroening, kroening@kroening.com "(list-symbols)(list-undefined-functions)" \ "(z3)(add-library)(show-dependence-graph)" \ "(horn)(skip-loops):(apply-code-contracts)(model-argc-argv):" \ + "(expand-pointer-predicates)" \ "(show-threaded)(list-calls-args)" \ "(undefined-function-is-assume-false)" \ "(remove-function-body):"\ diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index 105f4fe5ba8..b38e4cadf7d 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -23,27 +24,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -inline static optionalt c_sizeof_type_rec(const exprt &expr) -{ - const irept &sizeof_type=expr.find(ID_C_c_sizeof_type); - - if(!sizeof_type.is_nil()) - { - return static_cast(sizeof_type); - } - else if(expr.id()==ID_mult) - { - forall_operands(it, expr) - { - const auto t = c_sizeof_type_rec(*it); - if(t.has_value()) - return t; - } - } - - return {}; -} - void goto_symext::symex_allocate( statet &state, const exprt &lhs, @@ -74,54 +54,7 @@ void goto_symext::symex_allocate( // to allow constant propagation exprt tmp_size = state.rename(size, ns); simplify(tmp_size, ns); - - // special treatment for sizeof(T)*x - { - const auto tmp_type = c_sizeof_type_rec(tmp_size); - - if(tmp_type.has_value()) - { - // Did the size get multiplied? - auto elem_size = pointer_offset_size(*tmp_type, ns); - const auto alloc_size = numeric_cast(tmp_size); - - if(!elem_size.has_value() || *elem_size==0) - { - } - else if( - !alloc_size.has_value() && tmp_size.id() == ID_mult && - tmp_size.operands().size() == 2 && - (tmp_size.op0().is_constant() || tmp_size.op1().is_constant())) - { - exprt s=tmp_size.op0(); - if(s.is_constant()) - { - s=tmp_size.op1(); - PRECONDITION(*c_sizeof_type_rec(tmp_size.op0()) == *tmp_type); - } - else - PRECONDITION(*c_sizeof_type_rec(tmp_size.op1()) == *tmp_type); - - object_type = array_typet(*tmp_type, s); - } - else if(alloc_size.has_value()) - { - if(*alloc_size == *elem_size) - object_type = *tmp_type; - else - { - mp_integer elements = *alloc_size / (*elem_size); - - if(elements * (*elem_size) == *alloc_size) - object_type = - array_typet(*tmp_type, from_integer(elements, tmp_size.type())); - } - } - } - } - - if(!object_type.has_value()) - object_type=array_typet(unsigned_char_type(), tmp_size); + object_type = type_from_size(tmp_size, ns); // we introduce a fresh symbol for the size // to prevent any issues of the size getting ever changed diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp index 2e3e449cd07..349434baa2c 100644 --- a/src/util/expr_util.cpp +++ b/src/util/expr_util.cpp @@ -8,17 +8,102 @@ Author: Daniel Kroening, kroening@kroening.com #include "expr_util.h" -#include -#include - +#include "arith_tools.h" +#include "c_types.h" #include "expr.h" #include "expr_iterator.h" #include "fixedbv.h" #include "ieee_float.h" +#include "namespace.h" +#include "pointer_offset_size.h" +#include "simplify_expr.h" #include "std_expr.h" #include "symbol.h" -#include "namespace.h" -#include "arith_tools.h" +#include +#include + +inline static optionalt c_sizeof_type_rec(const exprt &expr) +{ + const irept &sizeof_type = expr.find(ID_C_c_sizeof_type); + + if(!sizeof_type.is_nil()) + { + return static_cast(sizeof_type); + } + else if(expr.id() == ID_mult) + { + forall_operands(it, expr) + { + const auto t = c_sizeof_type_rec(*it); + if(t.has_value()) + return t; + } + } + + return {}; +} + +typet type_from_size(const exprt &size, const namespacet &ns) +{ + auto tmp_type = c_sizeof_type_rec(size); + + // Default to char[size] if nothing better can be found. + typet result_type = array_typet(unsigned_char_type(), size); + + if(tmp_type.has_value()) + { + // Did the size get multiplied? + auto elem_size = pointer_offset_size(*tmp_type, ns); + const auto alloc_size = numeric_cast(size); + + if(!elem_size.has_value() || *elem_size < 0) + { + // If this occurs, then either tmp_type contains some type with invalid + // ID or tmp_type contains a bitvector of negative size. Neither of these + // should ever happen, and if one does, it suggests a failure in CBMC + // rather than a failure on the part of the user. + UNREACHABLE; + } + else if(*elem_size == 0) + { + } + // Case for constant size (in case it is a multiple of the element size) + else if(alloc_size.has_value()) + { + if(alloc_size == *elem_size) + { + result_type = *tmp_type; + } + else if((*alloc_size / *elem_size) * (*elem_size) == *alloc_size) + { + // Allocation size is a multiple of the element size + result_type = array_typet( + *tmp_type, from_integer(*alloc_size / *elem_size, size.type())); + } + } + // Special case for constant * sizeof + else if( + size.id() == ID_mult && size.operands().size() == 2 && + (size.op0().is_constant() || size.op1().is_constant())) + { + exprt s = size.op0(); + if(s.is_constant()) + { + s = size.op1(); + PRECONDITION(c_sizeof_type_rec(size.op0()) == tmp_type); + } + else + { + PRECONDITION(c_sizeof_type_rec(size.op1()) == tmp_type); + } + + result_type = array_typet(*tmp_type, s); + } + } + + POSTCONDITION(result_type.is_not_nil()); + return result_type; +} bool is_lvalue(const exprt &expr) { diff --git a/src/util/expr_util.h b/src/util/expr_util.h index bc0b5099071..122ca212029 100644 --- a/src/util/expr_util.h +++ b/src/util/expr_util.h @@ -30,6 +30,18 @@ class symbolt; class typet; class namespacet; +/// Creates a type with size (in bytes) equal to the size argument. +/// Makes use of sizeof() in the argument to avoid unnecessary use of byte +/// arrays. +/// \param size: An expression describing the size (in bytes) of the desired +/// type. +/// \param ns : A namespace for symbol type lookups. +/// \return A type with size given by the argument \a size. +/// If \a size is of the form n*sizeof(T) (or sizeof(T)*n), then this +/// type will be T[n]. If \a size is of the form sizeof(T), then this +/// type will be T. Otherwise, the type will be unsigned char[size]. +typet type_from_size(const exprt &size, const namespacet &ns); + /// Returns true iff the argument is (syntactically) an lvalue. bool is_lvalue(const exprt &expr); diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index ca216365e18..f6f0c4f7272 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -218,6 +218,7 @@ IREP_ID_TWO(C_invalid_object, #invalid_object) IREP_ID_ONE(pointer_offset) IREP_ID_ONE(pointer_object) IREP_ID_TWO(invalid_pointer, invalid-pointer) +IREP_ID_ONE(points_to_valid_memory) IREP_ID_ONE(ieee_float_equal) IREP_ID_ONE(ieee_float_notequal) IREP_ID_ONE(isnan) diff --git a/src/util/pointer_predicates.cpp b/src/util/pointer_predicates.cpp index 0b111fb8f04..b88a2254cde 100644 --- a/src/util/pointer_predicates.cpp +++ b/src/util/pointer_predicates.cpp @@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "cprover_prefix.h" #include "namespace.h" #include "pointer_offset_size.h" +#include "simplify_expr.h" #include "std_expr.h" #include "symbol.h" @@ -144,6 +145,46 @@ exprt invalid_pointer(const exprt &pointer) return unary_exprt(ID_invalid_pointer, pointer, bool_typet()); } +exprt points_to_valid_memory(const exprt &pointer, const exprt &size) +{ + return binary_exprt(pointer, ID_points_to_valid_memory, size, bool_typet()); +} + +exprt points_to_valid_memory_def( + const exprt &pointer, + const exprt &size, + const namespacet &ns) +{ + const not_exprt not_null(null_pointer(pointer)); + + const not_exprt not_deallocated(deallocated(pointer, ns)); + + const not_exprt not_dead(dead_object(pointer, ns)); + + const not_exprt not_invalid(invalid_pointer(pointer)); + + const or_exprt malloc_in_bounds( + not_exprt(malloc_object(pointer, ns)), + and_exprt( + not_exprt(dynamic_object_lower_bound(pointer, nil_exprt())), + not_exprt(dynamic_object_upper_bound(pointer, ns, size)))); + + const or_exprt dynamic_in_bounds( + dynamic_object(pointer), + and_exprt( + not_exprt(object_lower_bound(pointer, nil_exprt())), + not_exprt(object_upper_bound(pointer, size)))); + + exprt check_expr = conjunction({not_null, + not_deallocated, + not_dead, + not_invalid, + malloc_in_bounds, + dynamic_in_bounds}); + + return simplify_expr(check_expr, ns); +} + exprt dynamic_object_lower_bound( const exprt &pointer, const exprt &offset) diff --git a/src/util/pointer_predicates.h b/src/util/pointer_predicates.h index 2771d52f31c..a0118f5b412 100644 --- a/src/util/pointer_predicates.h +++ b/src/util/pointer_predicates.h @@ -33,6 +33,11 @@ exprt null_object(const exprt &pointer); exprt null_pointer(const exprt &pointer); exprt integer_address(const exprt &pointer); exprt invalid_pointer(const exprt &pointer); +exprt points_to_valid_memory(const exprt &pointer, const exprt &size); +exprt points_to_valid_memory_def( + const exprt &pointer, + const exprt &size, + const namespacet &); exprt dynamic_object_lower_bound( const exprt &pointer, const exprt &offset); From 2684caa9f3720c905f675efc8f9bb3227b270f2d Mon Sep 17 00:00:00 2001 From: klaas Date: Mon, 30 Jul 2018 14:33:13 -0400 Subject: [PATCH 3/5] 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 | 22 ++++++++++++++++++++-- src/ansi-c/cprover_builtin_headers.h | 2 +- 2 files changed, 21 insertions(+), 3 deletions(-) diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index f251ac5d572..3f88ee3b42f 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2113,10 +2113,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())) @@ -2142,6 +2142,24 @@ 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(); + auto expr_size = size_of_expr(base_type, *this); + if(!expr_size) + { + error().source_location = expr.source_location(); + error() << "cannot determine size of pointed-to memory region" << eom; + throw 0; + } + + expr_size->add(ID_C_c_sizeof_type) = base_type; + + same_object_expr = + points_to_valid_memory(expr.arguments()[0], *expr_size); + } else { UNREACHABLE; 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 026a611a194376510f60e86ca8de34f0386b757e Mon Sep 17 00:00:00 2001 From: klaas Date: Mon, 30 Jul 2018 14:35:47 -0400 Subject: [PATCH 4/5] 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..f64909c5e27 --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates5/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--pointer-check --expand-pointer-predicates +^\[main.assertion.1\] line \d+ Variable length assert: SUCCESS$ +^\[main.assertion.2\] line \d+ assertion x_pointer\[\(signed long( long)? int\)2\] == 5: SUCCESS$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/regression/goto-instrument/expand-pointer-predicates6/main.c b/regression/goto-instrument/expand-pointer-predicates6/main.c new file mode 100644 index 00000000000..a8b4931a4b1 --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates6/main.c @@ -0,0 +1,21 @@ +#include + +struct my_struct +{ + int *field1; + int *field2; +}; + +void example(struct my_struct *s) +{ + s->field2 = malloc(sizeof(*(s->field2))); +} + +int main() +{ + struct my_struct *s; + __CPROVER_assume(__CPROVER_points_to_valid_memory(s)); + example(s); + __CPROVER_assert(__CPROVER_points_to_valid_memory(s->field2), ""); + return 0; +} diff --git a/regression/goto-instrument/expand-pointer-predicates6/test.desc b/regression/goto-instrument/expand-pointer-predicates6/test.desc new file mode 100644 index 00000000000..2456c5f7d92 --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates6/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--pointer-check --expand-pointer-predicates +^\[main.assertion.1\] line \d+ assertion: SUCCESS$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/regression/goto-instrument/expand-pointer-predicates7/main.c b/regression/goto-instrument/expand-pointer-predicates7/main.c new file mode 100644 index 00000000000..5f18fb9fa1f --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates7/main.c @@ -0,0 +1,22 @@ +#include + +struct my_struct +{ + int *field; +}; + +void example(struct my_struct *s) +{ + __CPROVER_assume(__CPROVER_points_to_valid_memory(s)); + size_t size; + __CPROVER_assume(size == sizeof(*(s->field))); + __CPROVER_assume(__CPROVER_points_to_valid_memory(s->field, size)); + int read = *(s->field); +} + +int main() +{ + struct my_struct *s; + example(s); + return 0; +} diff --git a/regression/goto-instrument/expand-pointer-predicates7/test.desc b/regression/goto-instrument/expand-pointer-predicates7/test.desc new file mode 100644 index 00000000000..c28c5c3d48b --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates7/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--pointer-check --expand-pointer-predicates +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/regression/goto-instrument/expand-pointer-predicates8/main.c b/regression/goto-instrument/expand-pointer-predicates8/main.c new file mode 100644 index 00000000000..766ea1525f9 --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates8/main.c @@ -0,0 +1,16 @@ +#include + +int main() +{ + int *x; + int *y; + __CPROVER_assume(__CPROVER_points_to_valid_memory(x, 2 * sizeof(int))); + __CPROVER_assume(__CPROVER_points_to_valid_memory(y, 2 * sizeof(int) - 1)); + (void)(x[0]); // Should succeed + (void)(x[1]); // Should succeed + (void)(x[2]); // Should fail + (void)(x[-1]); // Should fail + (void)(y[0]); // Should succeed + (void)(y[1]); // Should fail + return 0; +} diff --git a/regression/goto-instrument/expand-pointer-predicates8/test.desc b/regression/goto-instrument/expand-pointer-predicates8/test.desc new file mode 100644 index 00000000000..cffb9599ada --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates8/test.desc @@ -0,0 +1,16 @@ +CORE +main.c +--pointer-check --expand-pointer-predicates +^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: dead object in x\[\(signed long( long)? int\)0\]: SUCCESS$ +^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)0\]: SUCCESS$ +^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)1\]: SUCCESS$ +^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)2\]: FAILURE$ +^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)-1\]: FAILURE$ +^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: dead object in y\[\(signed long( long)? int\)0\]: SUCCESS$ +^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: pointer outside object bounds in y\[\(signed long( long)? int\)0\]: SUCCESS$ +^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: pointer outside object bounds in y\[\(signed long( long)? int\)1\]: FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/regression/goto-instrument/expand-pointer-predicates9/main.c b/regression/goto-instrument/expand-pointer-predicates9/main.c new file mode 100644 index 00000000000..bb80cf4c996 --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates9/main.c @@ -0,0 +1,11 @@ +#include + +int main() +{ + char *x; + __CPROVER_assume(__CPROVER_points_to_valid_memory(x)); + (void)(*x); // Should succeed + (void)(*(x + 1)); // Should fail + (void)(*(x - 1)); // Should fail + return 0; +} diff --git a/regression/goto-instrument/expand-pointer-predicates9/test.desc b/regression/goto-instrument/expand-pointer-predicates9/test.desc new file mode 100644 index 00000000000..4c8dde65ec2 --- /dev/null +++ b/regression/goto-instrument/expand-pointer-predicates9/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--pointer-check --expand-pointer-predicates +^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: dead object in \*x: SUCCESS$ +^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: pointer outside object bounds in \*x: SUCCESS$ +^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)1\]: FAILURE$ +^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: pointer outside object bounds in \*\(x - \(signed long( long)? int\)1\): FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- From f53b62ba430b7fa877bea8639a3470f58d8225a3 Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Wed, 6 Mar 2019 09:42:19 -0500 Subject: [PATCH 5/5] Check 2nd arg to points_to_valid_memory is size_t This commit ensures that the second argument to the __CPROVER_points_to_valid_memory directive can be coerced to a size_t, and adds a test to check for the failing case. --- regression/contracts/argument_sanity/main.c | 5 +++++ regression/contracts/argument_sanity/main.mod | Bin 0 -> 5952 bytes regression/contracts/argument_sanity/test.desc | 9 +++++++++ src/ansi-c/c_typecheck_expr.cpp | 6 +++--- 4 files changed, 17 insertions(+), 3 deletions(-) create mode 100644 regression/contracts/argument_sanity/main.c create mode 100644 regression/contracts/argument_sanity/main.mod create mode 100644 regression/contracts/argument_sanity/test.desc diff --git a/regression/contracts/argument_sanity/main.c b/regression/contracts/argument_sanity/main.c new file mode 100644 index 00000000000..742b16a4e7e --- /dev/null +++ b/regression/contracts/argument_sanity/main.c @@ -0,0 +1,5 @@ +int main() +{ + int *r; + __CPROVER_points_to_valid_memory(r, "huh?"); +} diff --git a/regression/contracts/argument_sanity/main.mod b/regression/contracts/argument_sanity/main.mod new file mode 100644 index 0000000000000000000000000000000000000000..f74debcaba567d58d74eff8c1ca9806f0c835ab1 GIT binary patch literal 5952 zcmaJ_33wFc8UFv>WXTj*HRVV`TVn%QTQDvlMifF2!~;ik>d|5yW_Ksa$Yy7q-3^4M zRXkDgz!McbB8rG2A`*^8ZbXi7dX!sxx6<1CuD;*=|Lo3cQ+RkDX6O6g@BQxYpIau5 zySQX18*R3vGHpx^*QD*N6EpRM9WyePon)Lb^|VGSVY0v*%7xLamB9#Y?N;c_n%Q0ga+i7DZk1Ms;q)jJXJI!#WH5)T)W6_pa ztz$MhW;zX=+L)cpI7Td!t~H#dY>S!9=xHNqffOK51Zwa;oiUObR{C}zf}h?A)>vu1 z(Ezi!o^ET2+6h+5LV=`}U@UY@(e;ZaUw!4Z6Ry@<%ob446Q(h3pdGylj98Ah7*>)U zQ#yhd0l&IOkF?d4G~>}$rasB1Tk%XYD_fw{xvEQ{t5iJ^tcmHFwv@?~S%Fxy;ow{- zbi}8}aAM6?2Jl(O)ajw1?FbY>%~wXN;hu13KrQd}suCeHR+W^Hd9DuN9roeHO(U)g z!Ud$m0;zXdHtDAvepVSdg4hO6c_84uLJ$!I3qE7))B(gjW~4JrJ8fLvnQG8Ask{fw z{_4ZZ@L?`SpZfv=Tpm`#eFf`&&nY84(haRfB5Sh#>jLNCr!~ALYNSn8@w5`bGgE`T zS>J;`YckCa*<;1w{DUy!pu*}ZUA3*fq3G)1fn9JW3cRxgUa7>ZeM%YTMfB`l-J!zMdB9x&+(m%r2*8K{9QLjf@#3a7^ml1Sc60|w zWv!#Dcm)K*cK~+>;SLwLBLwcb?f$IgPcAkU)#S3?F^_oeO zP?&XF|MzLwx)s#6lC7hKtz(3(Wko?Av&DD5D9F;Dd`PwcZVTYb>jm6cVPdU>6Tuj} z*$3y?*<_psM~fXdL1;4&HdCKy5D4Q0p^I`#B%kjMqLjw1^WhZHG688MlNd8VTnEH; z;51%VeeiTPVSskAfS)J`Ub0FVcD`3mGH2A_cs6mhPesZ~nR*O-sX|u+bu~HeQUP?C z;CcB=3iV{S#mgkQtkZ{4M3YK7@48L^b^>rxRg65LhOZFR)VGx3`KfV|J0@mLQcR^Q zkwlPM6igY8(PAR8(rhx~ebw^PnB9`1G0E5!D}CyzUs-50XcsxY5*k-3th(}QVS*-1 zII}4B+6v$CBKB^9f2qn>0CWY+_-<6Yh8$jo7If{sg%&Hvs2aXbn0Ni_O5X9Y?|s72 zx#%4WUANq)Sj=;9UJm%>3LEx)m_9`y-0+GLp&9mtv3lHp+%1?d4c6lT!-%f@fw2EZ zVgL2g{#v)hZ(QcXDY8F}to03-WdK_S!}TgPJQYaBqY5n?XU9OTTsFCryd2SrGWFen znMhcvw3WsJ!>*c|*4*Y}l{9B$bpNc~1}fV? zr99L~MAY&#)QZMzGUhIKP0-<5_=L-E)Tqd)Q4TyiPjOgB@Ck(t=@AMY^}!bzZKu7K zljBFF`bl**{DRo{yx0ZH?=jP8B#`IF)E_LaL9#KTTpUIdm{s)eXy;@p1 zO(;zWrTwJR3O8nnP2H(WH``8zHk^FfZGy5*P}V{X*|(J)QgZx|G%zW2*+SP1MfqVb z=}y;lceE5VEdkmRXsS#JxSIu>vqs5hZ-dCWo7Z-WX*<|_Mft7;-df-pik9DzKgheCWP~6FG1IkOu%c!_?Yne?akKO+67*fICyr{b7d^ zp&i++Hrg<@2iuQ8(~mki?gzBl>vkj4eq3!O9`Hh;+BI%M{qAR-Upg(YIqK*z*cxae@2PqJD+gm11KrR9^{=| zdx%$SbNM{9!-rj8sj)|--TlZzbGX{@D1QhQ9JAB-VKsL>llKUl!=LvtEAj*m2Qg*U;@IZZ@)K z`34^h6^)Kt5nY#9=o!4r;a^8^gTm%)2t3ED)RX*qKANWKWOh|(uJ5RhOQ=H^Dr!A! z0S|RZy~Erp*y$6MDIhC!C-8TYlV6ZdUMQXH?L%UZS;*)6Ac|r|3mk2yGfl^a_45HZ zp8#K!fG$B2{1Fi@QVgx>E7VyBNTW0lWyYc$wlgMaFB2>?Vu(am4EtQoF>J zArUWLQ#SgvNf+dA-5UYD5zs-JhOF1Cyh?kGkCeA}x9S?zb}Np1kJV^lHD1awgHU0w z^C~2IqgoH|XH55Aw2Y6Bn=#yi;EKlZ8$@Q1+OV9z#WN1BrTFt1{+zU%amB+O zb|wEvOmy1DDw*twS`bJ*eo7iUF$LG(RI=z5Qk0?7b2oc!l2*>OtWm&fWq;8WAntQ0iORYCJCHsK+q71p28S zZN`oQ?3gtCIDdqoPSB%{4VO#-umGD%V4ybDclaY5{+KfTr^xi5xtV?|a%wLM;0_#< zqnklN9^>bH2e-4CRF;}8&`Jtae&IRrmwYaGzzgIwS?&eL`R+Hpegy)*Cc4wr_TON& z0sB^=s;652TYj;DkC07CXj-ZC?41XLOFzNElXUO`wf%RvA>-gEaj=dKLcXpb&wdZ- zPf2=^+WrSjdr03UO`45_a^+`p-+@2kz@O;A5|rJaIeH`0UXdrJ$OBV+@_&K+UrBxe zDvNT+U+D=uD0J1z%`#~ z^+I~AlpgDoz7x`Sku;dx9l*y!rkyIJ`%3A)KIz$zzK5g-s_pj%@ZpMS_XUn}cMWq_ n(m4TlUW5m$4Lhld2fE+V++r9k@do?w?hm*#go+3e_ov(E<&@