From 20b536644ae23db40ed45e129d8d2d3557b67be1 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 9 Nov 2017 15:21:25 +0000 Subject: [PATCH 1/7] Add validate and can_cast method to string_exprt --- src/util/string_expr.h | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/util/string_expr.h b/src/util/string_expr.h index f0e080a8ec7..c9d54470d3b 100644 --- a/src/util/string_expr.h +++ b/src/util/string_expr.h @@ -241,4 +241,18 @@ inline const refined_string_exprt &to_string_expr(const exprt &expr) return static_cast(expr); } +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_struct && base.operands().size() == 2; +} + +inline void validate_expr(const refined_string_exprt &x) +{ + INVARIANT(x.id() == ID_struct, "refined string exprs are struct"); + validate_operands(x, 2, "refined string expr has length and content fields"); + INVARIANT(x.length().type().id() == ID_signedbv, "length is an unsigned int"); + INVARIANT(x.content().type().id() == ID_array, "content is an array"); +} + #endif From 946b6e2cb76ca5a8f7f41c222725f2b61f8d5f24 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 15 Nov 2017 20:11:59 +0000 Subject: [PATCH 2/7] Extend numeric_cast for constant expressions This requires moving some declarations to arith_tools, because overload needs to be declared in the same struct. This also adds a numeric_cast_v function which returns a value instead of an optional but an invariant can fail. --- src/util/arith_tools.h | 125 +++++++++++++++++++++++++++++++++++++++++ src/util/mp_arith.h | 67 ---------------------- 2 files changed, 125 insertions(+), 67 deletions(-) diff --git a/src/util/arith_tools.h b/src/util/arith_tools.h index ebb243952f4..93fb4d315f2 100644 --- a/src/util/arith_tools.h +++ b/src/util/arith_tools.h @@ -11,6 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_UTIL_ARITH_TOOLS_H #include "mp_arith.h" +#include "optional.h" +#include "invariant.h" class exprt; class constant_exprt; @@ -18,14 +20,137 @@ class typet; // this one will go away // returns 'true' on error +/// \deprecated: use the constant_exprt version instead bool to_integer(const exprt &expr, mp_integer &int_value); // returns 'true' on error +/// \deprecated: use numeric_cast instead bool to_integer(const constant_exprt &expr, mp_integer &int_value); // returns 'true' on error bool to_unsigned_integer(const constant_exprt &expr, unsigned &uint_value); +/// Numerical cast provides a unified way of converting from one numerical type +/// to another. +/// Generic case doesn't exist, this has to be specialized for different types. +template +struct numeric_castt final +{ +}; + +/// Convert expression to mp_integer +template <> +struct numeric_castt final +{ + optionalt operator()(const exprt &expr) const + { + mp_integer out; + if(to_integer(expr, out)) + return {}; + return out; + } +}; + +/// Convert mp_integer or expr to any integral type +template +struct numeric_castt::value>::type> +{ +private: + // Unchecked conversion from mp_integer when T is signed + template ::value, int>::type = 0> + static auto get_val(const mp_integer &mpi) -> decltype(mpi.to_long()) + { + return mpi.to_long(); + } + + // Unchecked conversion from mp_integer when T is unsigned + template ::value, int>::type = 0> + static auto get_val(const mp_integer &mpi) -> decltype(mpi.to_ulong()) + { + return mpi.to_ulong(); + } + +public: + // Conversion from mp_integer to integral type T + optionalt operator()(const mp_integer &mpi) const + { +#if !defined(_MSC_VER) || _MSC_VER >= 1900 + static_assert( + std::numeric_limits::max() <= + std::numeric_limits::max() && + std::numeric_limits::min() >= + std::numeric_limits::min(), + "Numeric cast only works for types smaller than long long"); +#else + // std::numeric_limits<> methods are not declared constexpr in old versions + // of VS + PRECONDITION( + std::numeric_limits::max() <= + std::numeric_limits::max() && + std::numeric_limits::min() >= + std::numeric_limits::min()); +#endif + if( + mpi <= std::numeric_limits::max() && + mpi >= std::numeric_limits::min()) + // to_long converts to long long which is the largest signed numeric type + return static_cast(get_val(mpi)); + else + return {}; + } + + // Conversion from expression + optionalt operator()(const exprt &expr) const + { + if(auto mpi_opt = numeric_castt{}(expr)) + return numeric_castt{}(*mpi_opt); + else + return {}; + } +}; + +/// Converts an expression to any integral type +/// \tparam Target: type to convert to +/// \param arg: expression to convert +/// \return optional integer of type Target if conversion is possible, +/// empty optional otherwise. +template +optionalt numeric_cast(const exprt &arg) +{ + return numeric_castt{}(arg); +} + +/// Convert an mp_integer to integral type Target +/// An invariant with fail with message "Bad conversion" if conversion +/// is not possible. +/// \tparam Target: type to convert to +/// \param arg: mp_integer +/// \return value of type Target +template +Target numeric_cast_v(const mp_integer &arg) +{ + const auto maybe = numeric_castt{}(arg); + INVARIANT(maybe, "Bad conversion"); + return *maybe; +} + +/// Convert an expression to integral type Target +/// An invariant with fail with message "Bad conversion" if conversion +/// is not possible. +/// \tparam Target: type to convert to +/// \param arg: constant expression +/// \return value of type Target +template +Target numeric_cast_v(const exprt &arg) +{ + const auto maybe = numeric_castt{}(arg); + INVARIANT(maybe, "Bad conversion"); + return *maybe; +} + // PRECONDITION(false) in case of unsupported type constant_exprt from_integer(const mp_integer &int_value, const typet &type); diff --git a/src/util/mp_arith.h b/src/util/mp_arith.h index 4cdabf9326f..6783e581051 100644 --- a/src/util/mp_arith.h +++ b/src/util/mp_arith.h @@ -62,71 +62,4 @@ unsigned integer2unsigned(const mp_integer &); const mp_integer mp_zero=string2integer("0"); -/// Numerical cast provides a unified way of converting from one numerical type -/// to another. -/// Generic case doesn't exist, this has to be specialized for different types. -template -struct numeric_castt final -{ -}; - -/// Convert mp_integer to any signed type -/// \tparam T: type to convert to -/// \param mpi: mp_integer to convert -/// \return optional integer of type T if conversion is possible, -/// empty optional otherwise. -template -struct numeric_castt::value && - std::is_signed::value>::type> -{ - static optionalt numeric_cast(const mp_integer &mpi) - { - static_assert( - std::numeric_limits::max() <= - std::numeric_limits::max() && - std::numeric_limits::min() >= - std::numeric_limits::min(), - "Numeric cast only works for types smaller than long long"); - if( - mpi <= std::numeric_limits::max() && - mpi >= std::numeric_limits::min()) - // to_long converts to long long which is the largest signed numeric type - return {static_cast(mpi.to_long())}; - else - return {}; - } -}; - -/// Convert mp_integer to any unsigned type -/// \tparam T: type to convert to -/// \param mpi: mp_integer to convert -/// \return optional integer of type T if conversion is possible, -/// empty optional otherwise. -template -struct numeric_castt::value && - !std::is_signed::value>::type> -{ - static optionalt numeric_cast(const mp_integer &mpi) - { - static_assert( - std::numeric_limits::max() <= - std::numeric_limits::max() && - std::numeric_limits::min() >= - std::numeric_limits::min(), - "Numeric cast only works for types smaller than unsigned long long"); - if(mpi <= std::numeric_limits::max() && mpi >= 0) - return {static_cast(mpi.to_ulong())}; - else - return {}; - } -}; - -template -optionalt numeric_cast(const mp_integer &mpi) -{ - return numeric_castt::numeric_cast(mpi); -} - #endif // CPROVER_UTIL_MP_ARITH_H From fc294f8c1d5d2f6d5141766c581f8772abecc6a5 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 15 Nov 2017 17:18:26 +0000 Subject: [PATCH 3/7] Use numeric_cast instead of refinement/expr_cast --- ...ng_constraint_generator_transformation.cpp | 6 ++-- src/solvers/refinement/string_refinement.cpp | 29 +++++++++---------- 2 files changed, 17 insertions(+), 18 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_transformation.cpp b/src/solvers/refinement/string_constraint_generator_transformation.cpp index 37a697a26cd..c865699b4dd 100644 --- a/src/solvers/refinement/string_constraint_generator_transformation.cpp +++ b/src/solvers/refinement/string_constraint_generator_transformation.cpp @@ -13,7 +13,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include #include -#include "expr_cast.h" +#include /// Reduce or extend a string to have the given length /// @@ -442,8 +442,8 @@ static optionalt> to_char_pair( return std::make_pair(expr1, expr2); const auto expr1_str = get_string_expr(expr1); const auto expr2_str = get_string_expr(expr2); - const auto expr1_length=expr_cast(expr1_str.length()); - const auto expr2_length=expr_cast(expr2_str.length()); + const auto expr1_length = numeric_cast(expr1_str.length()); + const auto expr2_length = numeric_cast(expr2_str.length()); if(expr1_length && expr2_length && *expr1_length==1 && *expr2_length==1) return std::make_pair(exprt(expr1_str[0]), exprt(expr2_str[0])); return { }; diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 0b48caff4c3..193bd68b3c7 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -22,12 +22,11 @@ Author: Alberto Griggio, alberto.griggio@gmail.com #include #include #include -#include +#include #include #include #include #include -#include "expr_cast.h" static exprt substitute_array_with_expr(const exprt &expr, const exprt &index); @@ -852,7 +851,6 @@ static optionalt get_array( /// \return a string static std::string string_of_array(const array_exprt &arr) { - unsigned n; if(arr.type().id()!=ID_array) return std::string(""); @@ -1010,7 +1008,7 @@ exprt fill_in_array_with_expr( std::map initial_map; // Set the last index to be sure the array will have the right length - const auto &array_size_opt = expr_cast(array_type.size()); + const auto &array_size_opt = numeric_cast(array_type.size()); if(array_size_opt && *array_size_opt > 0) initial_map.emplace( *array_size_opt - 1, @@ -1022,7 +1020,8 @@ exprt fill_in_array_with_expr( // statements const with_exprt &with_expr = to_with_expr(it); const exprt &then_expr=with_expr.new_value(); - const auto index=expr_cast_v(with_expr.where()); + const auto index = + numeric_cast_v(to_constant_expr(with_expr.where())); if( index < string_max_length && (!array_size_opt || index < *array_size_opt)) initial_map.emplace(index, then_expr); @@ -1047,7 +1046,7 @@ exprt fill_in_array_expr(const array_exprt &expr, std::size_t string_max_length) // Map of the parts of the array that are initialized std::map initial_map; - const auto &array_size_opt = expr_cast(array_type.size()); + const auto &array_size_opt = numeric_cast(array_type.size()); if(array_size_opt && *array_size_opt > 0) initial_map.emplace( @@ -1180,14 +1179,14 @@ static exprt negation_of_not_contains_constraint( const exprt &ubu=axiom.univ_upper_bound(); if(lbu.id()==ID_constant && ubu.id()==ID_constant) { - const auto lb_int=expr_cast(lbu); - const auto ub_int=expr_cast(ubu); + const auto lb_int = numeric_cast(lbu); + const auto ub_int = numeric_cast(ubu); if(!lb_int || !ub_int || *ub_int<=*lb_int) return false_exprt(); } - const auto lbe=expr_cast_v(axiom.exists_lower_bound()); - const auto ube=expr_cast_v(axiom.exists_upper_bound()); + const auto lbe = numeric_cast_v(axiom.exists_lower_bound()); + const auto ube = numeric_cast_v(axiom.exists_upper_bound()); // If the premise is false, the implication is trivially true, so the // negation is false. @@ -1230,8 +1229,8 @@ static exprt negation_of_constraint(const string_constraintt &axiom) const exprt &ub=axiom.upper_bound(); if(lb.id()==ID_constant && ub.id()==ID_constant) { - const auto lb_int=expr_cast(lb); - const auto ub_int=expr_cast(ub); + const auto lb_int = numeric_cast(lb); + const auto ub_int = numeric_cast(ub); if(!lb_int || !ub_int || ub_int<=lb_int) return false_exprt(); } @@ -1786,7 +1785,7 @@ static void add_to_index_set( exprt i) { simplify(i, ns); - const bool is_size_t=expr_cast(i).has_value(); + const bool is_size_t = numeric_cast(i).has_value(); if(i.id()!=ID_constant || is_size_t) { std::vector sub_arrays; @@ -2047,7 +2046,7 @@ exprt substitute_array_lists(exprt expr, size_t string_max_length) { const exprt &index=expr.operands()[i]; const exprt &value=expr.operands()[i+1]; - const auto index_value=expr_cast(index); + const auto index_value = numeric_cast(index); if(!index.is_constant() || (index_value && *index_value(length)) + if(const auto n = numeric_cast(length)) { exprt arr_model = array_exprt(array_typet(arr.type().subtype(), length)); From 5683fb5f9b17824ca5b75ecec4a833a9b33d0b32 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 1 Dec 2017 06:56:54 +0000 Subject: [PATCH 4/7] Use numeric_cast instead of other conversion This is to demonstrate the use of numeric_cast --- src/solvers/refinement/string_refinement.cpp | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 193bd68b3c7..b3aa7fe26fc 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -794,12 +794,13 @@ static optionalt get_array( return {}; } - unsigned n; - if(to_unsigned_integer(to_constant_expr(size_val), n)) + auto n_opt = numeric_cast(size_val); + if(!n_opt) { stream << "(sr::get_array) size is not valid" << eom; return {}; } + unsigned n = *n_opt; const array_typet ret_type(char_type, from_integer(n, index_type)); array_exprt ret(ret_type); @@ -824,9 +825,11 @@ static optionalt get_array( for(size_t i = 0; i < arr_val.operands().size(); i += 2) { exprt index = arr_val.operands()[i]; - unsigned idx; - if(!to_unsigned_integer(to_constant_expr(index), idx) && idx(index)) + { + if(*idx < n) + initial_map[*idx] = arr_val.operands()[i + 1]; + } } // Pad the concretized values to the left to assign the uninitialized @@ -855,8 +858,7 @@ static std::string string_of_array(const array_exprt &arr) return std::string(""); exprt size_expr=to_array_type(arr.type()).size(); - PRECONDITION(size_expr.id()==ID_constant); - to_unsigned_integer(to_constant_expr(size_expr), n); + auto n = numeric_cast_v(size_expr); return utf16_constant_array_to_java(arr, n); } From 898f965eb428364461d1b02a894bb4e40e7cb746 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 8 Nov 2017 11:01:54 +0000 Subject: [PATCH 5/7] Remove solvers/refinement/expr_cast.h numeric_cast can now be used instead. --- src/solvers/refinement/expr_cast.h | 71 ------------------------------ 1 file changed, 71 deletions(-) delete mode 100644 src/solvers/refinement/expr_cast.h diff --git a/src/solvers/refinement/expr_cast.h b/src/solvers/refinement/expr_cast.h deleted file mode 100644 index 6ab795860ea..00000000000 --- a/src/solvers/refinement/expr_cast.h +++ /dev/null @@ -1,71 +0,0 @@ -/*******************************************************************\ - -Module: exprt conversion functions - -Author: Diffblue ltd. All Rights Reserved - -\*******************************************************************/ - -/// \file -/// Abstraction Refinement Loop - -#ifndef CPROVER_SOLVERS_REFINEMENT_EXPR_CAST_H -#define CPROVER_SOLVERS_REFINEMENT_EXPR_CAST_H - -#include - -/// Convert exprt to a specific type. Remove empty optional if -/// conversion cannot be performed -/// Generic case doesn't exist, specialize for different types accordingly -/// TODO: this should go to util -template -struct expr_cast_implt final { }; - -template<> -struct expr_cast_implt final -{ - optionalt operator()(const exprt &expr) const - { - mp_integer out; - if(to_integer(expr, out)) - return {}; - return out; - } -}; - -template<> -struct expr_cast_implt final -{ - optionalt operator()(const exprt &expr) const - { - if(const auto tmp=expr_cast_implt()(expr)) - if(tmp->is_long() && *tmp>=0) - return tmp->to_long(); - return {}; - } -}; - -template <> -struct expr_cast_implt final -{ - optionalt operator()(const exprt &expr) const - { - if(is_refined_string_type(expr.type())) - return to_string_expr(expr); - return {}; - } -}; - -template -optionalt expr_cast(const exprt& expr) -{ return expr_cast_implt()(expr); } - -template -T expr_cast_v(const exprt &expr) -{ - const auto maybe=expr_cast(expr); - INVARIANT(maybe, "Bad conversion"); - return *maybe; -} - -#endif // CPROVER_SOLVERS_REFINEMENT_EXPR_CAST_H From 77b7d772bf700c4193a7f8de710351431442d838 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 7 Dec 2017 10:02:40 +0000 Subject: [PATCH 6/7] Change length argument type to size_t --- src/solvers/refinement/string_constraint_generator.h | 4 ++-- src/solvers/refinement/string_constraint_generator_format.cpp | 4 ++-- src/solvers/refinement/string_refinement.cpp | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 4f47794981c..1f00a0bbe7e 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -373,7 +373,7 @@ exprt get_numeric_value_from_character( size_t max_printed_string_length(const typet &type, unsigned long ul_radix); -std::string utf16_constant_array_to_java( - const array_exprt &arr, unsigned length); +std::string +utf16_constant_array_to_java(const array_exprt &arr, std::size_t length); #endif diff --git a/src/solvers/refinement/string_constraint_generator_format.cpp b/src/solvers/refinement/string_constraint_generator_format.cpp index 7a5902f7e70..03a6f788d28 100644 --- a/src/solvers/refinement/string_constraint_generator_format.cpp +++ b/src/solvers/refinement/string_constraint_generator_format.cpp @@ -417,8 +417,8 @@ exprt string_constraint_generatort::add_axioms_for_format( /// \param length: an unsigned value representing the length of the array /// \return String of length `length` represented by the array assuming each /// field in `arr` represents a character. -std::string utf16_constant_array_to_java( - const array_exprt &arr, unsigned int length) +std::string +utf16_constant_array_to_java(const array_exprt &arr, std::size_t length) { std::wstring out(length, '?'); unsigned int c; diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index b3aa7fe26fc..ec765736000 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -858,7 +858,7 @@ static std::string string_of_array(const array_exprt &arr) return std::string(""); exprt size_expr=to_array_type(arr.type()).size(); - auto n = numeric_cast_v(size_expr); + auto n = numeric_cast_v(size_expr); return utf16_constant_array_to_java(arr, n); } From 9a811d8699af0262b4f2ee4eb61269c7efa1ee3f Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 7 Dec 2017 10:04:00 +0000 Subject: [PATCH 7/7] Change type of size to std::size_t --- src/solvers/refinement/string_refinement.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index ec765736000..8ff90e94676 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -794,13 +794,13 @@ static optionalt get_array( return {}; } - auto n_opt = numeric_cast(size_val); + auto n_opt = numeric_cast(size_val); if(!n_opt) { stream << "(sr::get_array) size is not valid" << eom; return {}; } - unsigned n = *n_opt; + std::size_t n = *n_opt; const array_typet ret_type(char_type, from_integer(n, index_type)); array_exprt ret(ret_type);