From 3d817b2bf7cae65556cc61a6d100b9d355cf1a5b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 6 Jan 2021 22:48:11 +0000 Subject: [PATCH] Move expr2bits, bits2expr, try_get_string_data_array to simplify_utils They do not have any dependency on the simplify_exprt class (and thus don't need to be class members). Similarly, try_get_string_data_array has nothing to do with the simplify_exprt functions. --- scripts/expected_doxygen_warnings.txt | 6 +- src/goto-symex/goto_symex.cpp | 1 + src/util/simplify_expr.cpp | 326 +---------------------- src/util/simplify_expr.h | 19 -- src/util/simplify_expr_class.h | 6 - src/util/simplify_expr_int.cpp | 5 +- src/util/simplify_expr_struct.cpp | 5 +- src/util/simplify_utils.cpp | 321 ++++++++++++++++++++++ src/util/simplify_utils.h | 31 +++ unit/solvers/lowering/byte_operators.cpp | 28 +- unit/util/simplify_expr.cpp | 11 +- 11 files changed, 388 insertions(+), 371 deletions(-) diff --git a/scripts/expected_doxygen_warnings.txt b/scripts/expected_doxygen_warnings.txt index 0fc8ca5c1ee..2766e483dc5 100644 --- a/scripts/expected_doxygen_warnings.txt +++ b/scripts/expected_doxygen_warnings.txt @@ -85,17 +85,17 @@ warning: Included by graph for 'goto_functions.h' not generated, too many nodes warning: Included by graph for 'goto_model.h' not generated, too many nodes (109), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'arith_tools.h' not generated, too many nodes (181), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'c_types.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. -warning: Included by graph for 'config.h' not generated, too many nodes (84), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. +warning: Included by graph for 'config.h' not generated, too many nodes (85), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'exception_utils.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'expr.h' not generated, too many nodes (88), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'expr_util.h' not generated, too many nodes (60), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'invariant.h' not generated, too many nodes (187), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'irep.h' not generated, too many nodes (62), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'message.h' not generated, too many nodes (116), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. -warning: Included by graph for 'namespace.h' not generated, too many nodes (111), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. +warning: Included by graph for 'namespace.h' not generated, too many nodes (112), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'prefix.h' not generated, too many nodes (86), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (76), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'std_code.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. -warning: Included by graph for 'std_expr.h' not generated, too many nodes (246), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. +warning: Included by graph for 'std_expr.h' not generated, too many nodes (247), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'std_types.h' not generated, too many nodes (124), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'symbol_table.h' not generated, too many nodes (95), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp index 751eb89afa6..fbe561095b3 100644 --- a/src/goto-symex/goto_symex.cpp +++ b/src/goto-symex/goto_symex.cpp @@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 1c80f8f86ac..3e233ce24fb 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -10,11 +10,9 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include "arith_tools.h" #include "byte_operators.h" #include "c_types.h" #include "config.h" -#include "endianness_map.h" #include "expr_util.h" #include "fixedbv.h" #include "invariant.h" @@ -27,9 +25,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "rational_tools.h" #include "simplify_utils.h" #include "std_expr.h" -#include "string_constant.h" #include "string_expr.h" -#include "symbol.h" // #define DEBUGX @@ -1564,313 +1560,6 @@ simplify_exprt::resultt<> simplify_exprt::simplify_object(const exprt &expr) return unchanged(expr); } -optionalt simplify_exprt::bits2expr( - const std::string &bits, - const typet &type, - bool little_endian) -{ - // bits start at lowest memory address - auto type_bits = pointer_offset_bits(type, ns); - - if(!type_bits.has_value() || *type_bits != bits.size()) - return {}; - - if( - type.id() == ID_unsignedbv || type.id() == ID_signedbv || - type.id() == ID_floatbv || type.id() == ID_fixedbv || - type.id() == ID_c_bit_field || type.id() == ID_pointer || - type.id() == ID_bv) - { - endianness_mapt map(type, little_endian, ns); - - std::string tmp=bits; - for(std::string::size_type i=0; itype() = type; - return *val; - } - else - return {}; - } - else if(type.id()==ID_c_enum_tag) - { - auto val = - bits2expr(bits, ns.follow_tag(to_c_enum_tag_type(type)), little_endian); - if(val.has_value()) - { - val->type() = type; - return *val; - } - else - return {}; - } - else if(type.id()==ID_union) - { - // find a suitable member - const union_typet &union_type=to_union_type(type); - const union_typet::componentst &components= - union_type.components(); - - for(const auto &component : components) - { - auto val = bits2expr(bits, component.type(), little_endian); - if(!val.has_value()) - continue; - - return union_exprt(component.get_name(), *val, type); - } - } - else if(type.id() == ID_union_tag) - { - auto val = - bits2expr(bits, ns.follow_tag(to_union_tag_type(type)), little_endian); - if(val.has_value()) - { - val->type() = type; - return *val; - } - else - return {}; - } - else if(type.id()==ID_struct) - { - const struct_typet &struct_type=to_struct_type(type); - const struct_typet::componentst &components= - struct_type.components(); - - struct_exprt result({}, type); - result.reserve_operands(components.size()); - - mp_integer m_offset_bits=0; - for(const auto &component : components) - { - const auto m_size = pointer_offset_bits(component.type(), ns); - CHECK_RETURN(m_size.has_value() && *m_size>=0); - - std::string comp_bits = std::string( - bits, - numeric_cast_v(m_offset_bits), - numeric_cast_v(*m_size)); - - auto comp = bits2expr(comp_bits, component.type(), little_endian); - if(!comp.has_value()) - return {}; - result.add_to_operands(std::move(*comp)); - - m_offset_bits += *m_size; - } - - return std::move(result); - } - else if(type.id() == ID_struct_tag) - { - auto val = - bits2expr(bits, ns.follow_tag(to_struct_tag_type(type)), little_endian); - if(val.has_value()) - { - val->type() = type; - return *val; - } - else - return {}; - } - else if(type.id()==ID_array) - { - const array_typet &array_type=to_array_type(type); - const auto &size_expr = array_type.size(); - - PRECONDITION(size_expr.is_constant()); - - const std::size_t number_of_elements = - numeric_cast_v(to_constant_expr(size_expr)); - - const auto el_size_opt = pointer_offset_bits(array_type.subtype(), ns); - CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0); - - const std::size_t el_size = numeric_cast_v(*el_size_opt); - - array_exprt result({}, array_type); - result.reserve_operands(number_of_elements); - - for(std::size_t i = 0; i < number_of_elements; ++i) - { - std::string el_bits=std::string(bits, i*el_size, el_size); - auto el = bits2expr(el_bits, array_type.subtype(), little_endian); - if(!el.has_value()) - return {}; - result.add_to_operands(std::move(*el)); - } - - return std::move(result); - } - else if(type.id() == ID_vector) - { - const vector_typet &vector_type = to_vector_type(type); - - const std::size_t n_el = numeric_cast_v(vector_type.size()); - - const auto el_size_opt = pointer_offset_bits(vector_type.subtype(), ns); - CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0); - - const std::size_t el_size = numeric_cast_v(*el_size_opt); - - vector_exprt result({}, vector_type); - result.reserve_operands(n_el); - - for(std::size_t i = 0; i < n_el; ++i) - { - std::string el_bits = std::string(bits, i * el_size, el_size); - auto el = bits2expr(el_bits, vector_type.subtype(), little_endian); - if(!el.has_value()) - return {}; - result.add_to_operands(std::move(*el)); - } - - return std::move(result); - } - else if(type.id() == ID_complex) - { - const complex_typet &complex_type = to_complex_type(type); - - const auto sub_size_opt = pointer_offset_bits(complex_type.subtype(), ns); - CHECK_RETURN(sub_size_opt.has_value() && *sub_size_opt > 0); - - const std::size_t sub_size = numeric_cast_v(*sub_size_opt); - - auto real = bits2expr( - bits.substr(0, sub_size), complex_type.subtype(), little_endian); - auto imag = - bits2expr(bits.substr(sub_size), complex_type.subtype(), little_endian); - if(!real.has_value() || !imag.has_value()) - return {}; - - return complex_exprt(*real, *imag, complex_type); - } - - return {}; -} - -optionalt simplify_exprt::expr2bits( - const exprt &expr, - bool little_endian) -{ - // extract bits from lowest to highest memory address - const typet &type = expr.type(); - - if(expr.id()==ID_constant) - { - const auto &value = to_constant_expr(expr).get_value(); - - if( - type.id() == ID_unsignedbv || type.id() == ID_signedbv || - type.id() == ID_floatbv || type.id() == ID_fixedbv || - type.id() == ID_c_bit_field || type.id() == ID_bv) - { - const auto width = to_bitvector_type(type).get_width(); - - endianness_mapt map(type, little_endian, ns); - - std::string result(width, ' '); - - for(std::string::size_type i = 0; i < width; ++i) - result[map.map_bit(i)] = get_bvrep_bit(value, width, i) ? '1' : '0'; - - return result; - } - else if(type.id() == ID_pointer) - { - if(value == ID_NULL && config.ansi_c.NULL_is_zero) - return std::string('0', to_bitvector_type(type).get_width()); - else - return {}; - } - else if(type.id() == ID_c_enum_tag) - { - const auto &c_enum_type = ns.follow_tag(to_c_enum_tag_type(type)); - return expr2bits(constant_exprt(value, c_enum_type), little_endian); - } - else if(type.id() == ID_c_enum) - { - return expr2bits( - constant_exprt(value, to_c_enum_type(type).subtype()), little_endian); - } - } - else if(expr.id() == ID_string_constant) - { - return expr2bits(to_string_constant(expr).to_array_expr(), little_endian); - } - else if(expr.id()==ID_union) - { - return expr2bits(to_union_expr(expr).op(), little_endian); - } - else if( - expr.id() == ID_struct || expr.id() == ID_array || expr.id() == ID_vector || - expr.id() == ID_complex) - { - std::string result; - forall_operands(it, expr) - { - auto tmp=expr2bits(*it, little_endian); - if(!tmp.has_value()) - return {}; // failed - result+=tmp.value(); - } - - return result; - } - - return {}; -} - -optionalt> -try_get_string_data_array(const exprt &content, const namespacet &ns) -{ - if(content.id() != ID_address_of) - { - return {}; - } - - const auto &array_pointer = to_address_of_expr(content); - - if(array_pointer.object().id() != ID_index) - { - return {}; - } - - const auto &array_start = to_index_expr(array_pointer.object()); - - if(array_start.array().id() != ID_symbol || - array_start.array().type().id() != ID_array) - { - return {}; - } - - const auto &array = to_symbol_expr(array_start.array()); - - const symbolt *symbol_ptr = nullptr; - - if(ns.lookup(array.get_identifier(), symbol_ptr) || - symbol_ptr->value.id() != ID_array) - { - return {}; - } - - const auto &char_seq = to_array_expr(symbol_ptr->value); - - return optionalt>(char_seq); -} - simplify_exprt::resultt<> simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr) { @@ -1958,9 +1647,10 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr) if(expr.op().id()==ID_array_of && to_array_of_expr(expr.op()).op().id()==ID_constant) { - const auto const_bits_opt= - expr2bits(to_array_of_expr(expr.op()).op(), - byte_extract_id()==ID_byte_extract_little_endian); + const auto const_bits_opt = expr2bits( + to_array_of_expr(expr.op()).op(), + byte_extract_id() == ID_byte_extract_little_endian, + ns); if(!const_bits_opt.has_value()) return unchanged(expr); @@ -1979,7 +1669,7 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr) numeric_cast_v(*el_size)); auto tmp = bits2expr( - el_bits, expr.type(), expr.id() == ID_byte_extract_little_endian); + el_bits, expr.type(), expr.id() == ID_byte_extract_little_endian, ns); if(tmp.has_value()) return std::move(*tmp); @@ -1998,8 +1688,8 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr) } // extract bits of a constant - const auto bits= - expr2bits(expr.op(), expr.id()==ID_byte_extract_little_endian); + const auto bits = + expr2bits(expr.op(), expr.id() == ID_byte_extract_little_endian, ns); // make sure we don't lose bits with structs containing flexible array members const bool struct_has_flexible_array_member = has_subtype( @@ -2028,7 +1718,7 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr) numeric_cast_v(*el_size)); auto tmp = bits2expr( - bits_cut, expr.type(), expr.id() == ID_byte_extract_little_endian); + bits_cut, expr.type(), expr.id() == ID_byte_extract_little_endian, ns); if(tmp.has_value()) return std::move(*tmp); diff --git a/src/util/simplify_expr.h b/src/util/simplify_expr.h index 7035720ab21..3f34c0486dd 100644 --- a/src/util/simplify_expr.h +++ b/src/util/simplify_expr.h @@ -10,12 +10,8 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_SIMPLIFY_EXPR_H #define CPROVER_UTIL_SIMPLIFY_EXPR_H -class array_exprt; class exprt; class namespacet; -class refined_string_exprt; - -#include // // simplify an expression @@ -31,19 +27,4 @@ bool simplify( // this is the preferred interface exprt simplify_expr(exprt src, const namespacet &ns); -/// Get char sequence from content field of a refined string expression -/// -/// If `content` is of the form `&id[e]`, where `id` is an array-typed symbol -/// expression (and `e` is any expression), return the value of the symbol `id` -/// (as given by the `value` field of the symbol in the namespace `ns`); -/// otherwise return an empty optional. -/// -/// \param content: content field of a refined string expression -/// \param ns: namespace -/// \return array expression representing the char sequence which forms the -/// content of the refined string expression, empty optional if the content -/// cannot be determined -optionalt> -try_get_string_data_array(const exprt &content, const namespacet &ns); - #endif // CPROVER_UTIL_SIMPLIFY_EXPR_H diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index c0f9a53cfb3..b8b9c31bef8 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -236,12 +236,6 @@ class simplify_exprt type.id()==ID_bv; } - // bit-level conversions - optionalt - bits2expr(const std::string &bits, const typet &type, bool little_endian); - - optionalt expr2bits(const exprt &, bool little_endian); - protected: const namespacet &ns; #ifdef DEBUG_ON_DEMAND diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index fd8b425463e..74f23ce3e4b 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "pointer_offset_size.h" #include "rational.h" #include "rational_tools.h" +#include "simplify_utils.h" #include "std_expr.h" simplify_exprt::resultt<> @@ -1054,7 +1055,7 @@ simplify_exprt::simplify_extractbits(const extractbits_exprt &expr) if(expr.src().is_constant()) { - const auto svalue = expr2bits(expr.src(), true); + const auto svalue = expr2bits(expr.src(), true, ns); if(!svalue.has_value() || svalue->size() != *width) return unchanged(expr); @@ -1063,7 +1064,7 @@ simplify_exprt::simplify_extractbits(const extractbits_exprt &expr) numeric_cast_v(*end), numeric_cast_v(*start - *end + 1)); - auto result = bits2expr(extracted_value, expr.type(), true); + auto result = bits2expr(extracted_value, expr.type(), true, ns); if(!result.has_value()) return unchanged(expr); diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp index 8237d0565a2..9a8afc58485 100644 --- a/src/util/simplify_expr_struct.cpp +++ b/src/util/simplify_expr_struct.cpp @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "invariant.h" #include "namespace.h" #include "pointer_offset_size.h" +#include "simplify_utils.h" #include "std_expr.h" simplify_exprt::resultt<> @@ -189,7 +190,7 @@ simplify_exprt::simplify_member(const member_exprt &expr) if(target_size.has_value()) { mp_integer target_bits = target_size.value() * 8; - const auto bits=expr2bits(op, true); + const auto bits = expr2bits(op, true, ns); if(bits.has_value() && mp_integer(bits->size())>=target_bits) @@ -197,7 +198,7 @@ simplify_exprt::simplify_member(const member_exprt &expr) std::string bits_cut = std::string(*bits, 0, numeric_cast_v(target_bits)); - auto tmp = bits2expr(bits_cut, expr.type(), true); + auto tmp = bits2expr(bits_cut, expr.type(), true, ns); if(tmp.has_value()) return std::move(*tmp); diff --git a/src/util/simplify_utils.cpp b/src/util/simplify_utils.cpp index aeeddd48d3e..9193dc58473 100644 --- a/src/util/simplify_utils.cpp +++ b/src/util/simplify_utils.cpp @@ -8,6 +8,16 @@ Author: Daniel Kroening, kroening@kroening.com #include "simplify_utils.h" +#include "arith_tools.h" +#include "byte_operators.h" +#include "config.h" +#include "endianness_map.h" +#include "namespace.h" +#include "pointer_offset_size.h" +#include "std_expr.h" +#include "string_constant.h" +#include "symbol.h" + #include /// sort operands of an expression according to ordering defined by operator< @@ -164,3 +174,314 @@ bool sort_and_join(exprt &expr) return no_change; } + +optionalt bits2expr( + const std::string &bits, + const typet &type, + bool little_endian, + const namespacet &ns) +{ + // bits start at lowest memory address + auto type_bits = pointer_offset_bits(type, ns); + + if(!type_bits.has_value() || *type_bits != bits.size()) + return {}; + + if( + type.id() == ID_unsignedbv || type.id() == ID_signedbv || + type.id() == ID_floatbv || type.id() == ID_fixedbv || + type.id() == ID_c_bit_field || type.id() == ID_pointer || + type.id() == ID_bv) + { + endianness_mapt map(type, little_endian, ns); + + std::string tmp = bits; + for(std::string::size_type i = 0; i < bits.size(); ++i) + tmp[i] = bits[map.map_bit(i)]; + + std::reverse(tmp.begin(), tmp.end()); + + mp_integer i = binary2integer(tmp, false); + return constant_exprt(integer2bvrep(i, bits.size()), type); + } + else if(type.id() == ID_c_enum) + { + auto val = + bits2expr(bits, to_c_enum_type(type).subtype(), little_endian, ns); + if(val.has_value()) + { + val->type() = type; + return *val; + } + else + return {}; + } + else if(type.id() == ID_c_enum_tag) + { + auto val = bits2expr( + bits, ns.follow_tag(to_c_enum_tag_type(type)), little_endian, ns); + if(val.has_value()) + { + val->type() = type; + return *val; + } + else + return {}; + } + else if(type.id() == ID_union) + { + // find a suitable member + const union_typet &union_type = to_union_type(type); + const union_typet::componentst &components = union_type.components(); + + for(const auto &component : components) + { + auto val = bits2expr(bits, component.type(), little_endian, ns); + if(!val.has_value()) + continue; + + return union_exprt(component.get_name(), *val, type); + } + } + else if(type.id() == ID_union_tag) + { + auto val = bits2expr( + bits, ns.follow_tag(to_union_tag_type(type)), little_endian, ns); + if(val.has_value()) + { + val->type() = type; + return *val; + } + else + return {}; + } + else if(type.id() == ID_struct) + { + const struct_typet &struct_type = to_struct_type(type); + const struct_typet::componentst &components = struct_type.components(); + + struct_exprt result({}, type); + result.reserve_operands(components.size()); + + mp_integer m_offset_bits = 0; + for(const auto &component : components) + { + const auto m_size = pointer_offset_bits(component.type(), ns); + CHECK_RETURN(m_size.has_value() && *m_size >= 0); + + std::string comp_bits = std::string( + bits, + numeric_cast_v(m_offset_bits), + numeric_cast_v(*m_size)); + + auto comp = bits2expr(comp_bits, component.type(), little_endian, ns); + if(!comp.has_value()) + return {}; + result.add_to_operands(std::move(*comp)); + + m_offset_bits += *m_size; + } + + return std::move(result); + } + else if(type.id() == ID_struct_tag) + { + auto val = bits2expr( + bits, ns.follow_tag(to_struct_tag_type(type)), little_endian, ns); + if(val.has_value()) + { + val->type() = type; + return *val; + } + else + return {}; + } + else if(type.id() == ID_array) + { + const array_typet &array_type = to_array_type(type); + const auto &size_expr = array_type.size(); + + PRECONDITION(size_expr.is_constant()); + + const std::size_t number_of_elements = + numeric_cast_v(to_constant_expr(size_expr)); + + const auto el_size_opt = pointer_offset_bits(array_type.subtype(), ns); + CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0); + + const std::size_t el_size = numeric_cast_v(*el_size_opt); + + array_exprt result({}, array_type); + result.reserve_operands(number_of_elements); + + for(std::size_t i = 0; i < number_of_elements; ++i) + { + std::string el_bits = std::string(bits, i * el_size, el_size); + auto el = bits2expr(el_bits, array_type.subtype(), little_endian, ns); + if(!el.has_value()) + return {}; + result.add_to_operands(std::move(*el)); + } + + return std::move(result); + } + else if(type.id() == ID_vector) + { + const vector_typet &vector_type = to_vector_type(type); + + const std::size_t n_el = numeric_cast_v(vector_type.size()); + + const auto el_size_opt = pointer_offset_bits(vector_type.subtype(), ns); + CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0); + + const std::size_t el_size = numeric_cast_v(*el_size_opt); + + vector_exprt result({}, vector_type); + result.reserve_operands(n_el); + + for(std::size_t i = 0; i < n_el; ++i) + { + std::string el_bits = std::string(bits, i * el_size, el_size); + auto el = bits2expr(el_bits, vector_type.subtype(), little_endian, ns); + if(!el.has_value()) + return {}; + result.add_to_operands(std::move(*el)); + } + + return std::move(result); + } + else if(type.id() == ID_complex) + { + const complex_typet &complex_type = to_complex_type(type); + + const auto sub_size_opt = pointer_offset_bits(complex_type.subtype(), ns); + CHECK_RETURN(sub_size_opt.has_value() && *sub_size_opt > 0); + + const std::size_t sub_size = numeric_cast_v(*sub_size_opt); + + auto real = bits2expr( + bits.substr(0, sub_size), complex_type.subtype(), little_endian, ns); + auto imag = bits2expr( + bits.substr(sub_size), complex_type.subtype(), little_endian, ns); + if(!real.has_value() || !imag.has_value()) + return {}; + + return complex_exprt(*real, *imag, complex_type); + } + + return {}; +} + +optionalt +expr2bits(const exprt &expr, bool little_endian, const namespacet &ns) +{ + // extract bits from lowest to highest memory address + const typet &type = expr.type(); + + if(expr.id() == ID_constant) + { + const auto &value = to_constant_expr(expr).get_value(); + + if( + type.id() == ID_unsignedbv || type.id() == ID_signedbv || + type.id() == ID_floatbv || type.id() == ID_fixedbv || + type.id() == ID_c_bit_field || type.id() == ID_bv) + { + const auto width = to_bitvector_type(type).get_width(); + + endianness_mapt map(type, little_endian, ns); + + std::string result(width, ' '); + + for(std::string::size_type i = 0; i < width; ++i) + result[map.map_bit(i)] = get_bvrep_bit(value, width, i) ? '1' : '0'; + + return result; + } + else if(type.id() == ID_pointer) + { + if(value == ID_NULL && config.ansi_c.NULL_is_zero) + return std::string('0', to_bitvector_type(type).get_width()); + else + return {}; + } + else if(type.id() == ID_c_enum_tag) + { + const auto &c_enum_type = ns.follow_tag(to_c_enum_tag_type(type)); + return expr2bits(constant_exprt(value, c_enum_type), little_endian, ns); + } + else if(type.id() == ID_c_enum) + { + return expr2bits( + constant_exprt(value, to_c_enum_type(type).subtype()), + little_endian, + ns); + } + } + else if(expr.id() == ID_string_constant) + { + return expr2bits( + to_string_constant(expr).to_array_expr(), little_endian, ns); + } + else if(expr.id() == ID_union) + { + return expr2bits(to_union_expr(expr).op(), little_endian, ns); + } + else if( + expr.id() == ID_struct || expr.id() == ID_array || expr.id() == ID_vector || + expr.id() == ID_complex) + { + std::string result; + forall_operands(it, expr) + { + auto tmp = expr2bits(*it, little_endian, ns); + if(!tmp.has_value()) + return {}; // failed + result += tmp.value(); + } + + return result; + } + + return {}; +} + +optionalt> +try_get_string_data_array(const exprt &content, const namespacet &ns) +{ + if(content.id() != ID_address_of) + { + return {}; + } + + const auto &array_pointer = to_address_of_expr(content); + + if(array_pointer.object().id() != ID_index) + { + return {}; + } + + const auto &array_start = to_index_expr(array_pointer.object()); + + if( + array_start.array().id() != ID_symbol || + array_start.array().type().id() != ID_array) + { + return {}; + } + + const auto &array = to_symbol_expr(array_start.array()); + + const symbolt *symbol_ptr = nullptr; + + if( + ns.lookup(array.get_identifier(), symbol_ptr) || + symbol_ptr->value.id() != ID_array) + { + return {}; + } + + const auto &char_seq = to_array_expr(symbol_ptr->value); + + return optionalt>(char_seq); +} diff --git a/src/util/simplify_utils.h b/src/util/simplify_utils.h index 33e294f4e96..a0ad7abc57d 100644 --- a/src/util/simplify_utils.h +++ b/src/util/simplify_utils.h @@ -11,9 +11,40 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_UTIL_SIMPLIFY_UTILS_H #include "expr.h" +#include "optional.h" + +#include + +class array_exprt; +class namespacet; bool sort_operands(exprt::operandst &operands); bool sort_and_join(exprt &expr); +// bit-level conversions +optionalt bits2expr( + const std::string &bits, + const typet &type, + bool little_endian, + const namespacet &ns); + +optionalt +expr2bits(const exprt &, bool little_endian, const namespacet &ns); + +/// Get char sequence from content field of a refined string expression +/// +/// If `content` is of the form `&id[e]`, where `id` is an array-typed symbol +/// expression (and `e` is any expression), return the value of the symbol `id` +/// (as given by the `value` field of the symbol in the namespace `ns`); +/// otherwise return an empty optional. +/// +/// \param content: content field of a refined string expression +/// \param ns: namespace +/// \return array expression representing the char sequence which forms the +/// content of the refined string expression, empty optional if the content +/// cannot be determined +optionalt> +try_get_string_data_array(const exprt &content, const namespacet &ns); + #endif // CPROVER_UTIL_SIMPLIFY_UTILS_H diff --git a/unit/solvers/lowering/byte_operators.cpp b/unit/solvers/lowering/byte_operators.cpp index 6784d588e65..559012dc6d1 100644 --- a/unit/solvers/lowering/byte_operators.cpp +++ b/unit/solvers/lowering/byte_operators.cpp @@ -19,7 +19,7 @@ #include #include #include -#include +#include #include #include #include @@ -211,8 +211,6 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]") complex_typet(s16), complex_typet(u64)}; - simplify_exprt simp(ns); - THEN("byte_extract lowering yields the expected value") { for(const auto &endianness : @@ -232,10 +230,11 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]") REQUIRE(type_bits); const auto type_bits_int = numeric_cast_v(*type_bits); REQUIRE(type_bits_int <= oss.str().size()); - const auto s = simp.bits2expr( + const auto s = bits2expr( oss.str().substr(0, type_bits_int), t1, - endianness == ID_byte_extract_little_endian); + endianness == ID_byte_extract_little_endian, + ns); REQUIRE(s.has_value()); for(const auto &t2 : types) @@ -258,10 +257,11 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]") const auto type_bits_2_int = numeric_cast_v(*type_bits_2); REQUIRE(type_bits_2_int <= oss.str().size()); - const auto r = simp.bits2expr( + const auto r = bits2expr( oss.str().substr(0, type_bits_2_int), t2, - endianness == ID_byte_extract_little_endian); + endianness == ID_byte_extract_little_endian, + ns); REQUIRE(r.has_value()); const byte_extract_exprt be( @@ -362,8 +362,6 @@ SCENARIO("byte_update_lowering", "[core][solvers][lowering][byte_update]") // complex_typet(u64) }; - simplify_exprt simp(ns); - THEN("byte_update lowering yields the expected value") { for(const auto &endianness : @@ -384,8 +382,8 @@ SCENARIO("byte_update_lowering", "[core][solvers][lowering][byte_update]") const auto type_bits_int = numeric_cast_v(*type_bits); REQUIRE(type_bits_int <= oss.str().size()); const std::string s_string = oss.str().substr(0, type_bits_int); - const auto s = simp.bits2expr( - s_string, t1, endianness == ID_byte_update_little_endian); + const auto s = bits2expr( + s_string, t1, endianness == ID_byte_update_little_endian, ns); REQUIRE(s.has_value()); for(const auto &t2 : types) @@ -409,14 +407,14 @@ SCENARIO("byte_update_lowering", "[core][solvers][lowering][byte_update]") numeric_cast_v(*type_bits_2); REQUIRE(type_bits_2_int <= oss.str().size()); const std::string u_string = oss.str().substr(0, type_bits_2_int); - const auto u = simp.bits2expr( - u_string, t2, endianness == ID_byte_update_little_endian); + const auto u = bits2expr( + u_string, t2, endianness == ID_byte_update_little_endian, ns); REQUIRE(u.has_value()); std::string r_string = s_string; r_string.replace(16, u_string.size(), u_string); - const auto r = simp.bits2expr( - r_string, t1, endianness == ID_byte_update_little_endian); + const auto r = bits2expr( + r_string, t1, endianness == ID_byte_update_little_endian, ns); REQUIRE(r.has_value()); const byte_update_exprt bu( diff --git a/unit/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp index 15ba59a65ab..0fbc466b0a7 100644 --- a/unit/util/simplify_expr.cpp +++ b/unit/util/simplify_expr.cpp @@ -16,7 +16,7 @@ Author: Michael Tautschnig #include #include #include -#include +#include #include #include @@ -88,24 +88,23 @@ TEST_CASE("expr2bits and bits2expr respect bit order", "[core][util]") { symbol_tablet symbol_table; namespacet ns(symbol_table); - simplify_exprt simp(ns); exprt deadbeef = from_integer(0xdeadbeef, unsignedbv_typet(32)); - const auto le = simp.expr2bits(deadbeef, true); + const auto le = expr2bits(deadbeef, true, ns); REQUIRE(le.has_value()); REQUIRE(le->size() == 32); const auto should_be_deadbeef1 = - simp.bits2expr(*le, unsignedbv_typet(32), true); + bits2expr(*le, unsignedbv_typet(32), true, ns); REQUIRE(deadbeef == *should_be_deadbeef1); - const auto be = simp.expr2bits(deadbeef, false); + const auto be = expr2bits(deadbeef, false, ns); REQUIRE(be.has_value()); REQUIRE(be->size() == 32); const auto should_be_deadbeef2 = - simp.bits2expr(*be, unsignedbv_typet(32), false); + bits2expr(*be, unsignedbv_typet(32), false, ns); REQUIRE(deadbeef == *should_be_deadbeef2); }