From 044b004b58d15e040c7a23af269171945f7ae95a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 6 May 2018 18:36:02 +0100 Subject: [PATCH 1/2] Use get_subexpression_at_offset in simplify_byte_extract --- .../value_set_dereference.cpp | 3 + src/util/pointer_offset_size.cpp | 3 +- src/util/simplify_expr.cpp | 111 ++---------------- 3 files changed, 11 insertions(+), 106 deletions(-) diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 549b247dceb..345bf20eb5a 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -29,6 +29,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include // global data, horrible @@ -471,6 +472,8 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( // try to build a member/index expression - do not use byte_extract exprt subexpr = get_subexpression_at_offset( root_object_subexpression, o.offset(), dereference_type, ns); + if(subexpr.is_not_nil()) + simplify(subexpr, ns); if(subexpr.is_not_nil() && subexpr.id() != byte_extract_id()) { // Successfully found a member, array index, or combination thereof diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp index 71da8a20900..95d1a6046c1 100644 --- a/src/util/pointer_offset_size.cpp +++ b/src/util/pointer_offset_size.cpp @@ -722,12 +722,11 @@ exprt get_subexpression_at_offset( } } - const byte_extract_exprt be( + return byte_extract_exprt( byte_extract_id(), expr, from_integer(offset_bytes, index_type()), target_type_raw); - return simplify_expr(be, ns); } exprt get_subexpression_at_offset( diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 499ec065ae4..a9fdceab3ba 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -1781,112 +1781,15 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr) } } - // rethink the remaining code to correctly handle big endian - if(expr.id()!=ID_byte_extract_little_endian) + // try to refine it down to extracting from a member or an index in an array + exprt subexpr = + get_subexpression_at_offset(expr.op(), offset, expr.type(), ns); + if(subexpr.is_nil() || subexpr == expr) return true; - // get type of object - const typet &op_type=ns.follow(expr.op().type()); - - if(op_type.id()==ID_array) - { - exprt result=expr.op(); - - // try proper array or string constant - for(const typet *op_type_ptr=&op_type; - op_type_ptr->id()==ID_array; - op_type_ptr=&(ns.follow(*op_type_ptr).subtype())) - { - DATA_INVARIANT(*el_size > 0, "arrays must not have zero-sized objects"); - DATA_INVARIANT( - (*el_size) % 8 == 0, - "array elements have a size in bits which is a multiple of bytes"); - - mp_integer el_bytes = (*el_size) / 8; - - if(base_type_eq(expr.type(), op_type_ptr->subtype(), ns) || - (expr.type().id()==ID_pointer && - op_type_ptr->subtype().id()==ID_pointer)) - { - if(offset%el_bytes==0) - { - offset/=el_bytes; - - result= - index_exprt( - result, - from_integer(offset, expr.offset().type())); - result.make_typecast(expr.type()); - - if(!base_type_eq(expr.type(), op_type_ptr->subtype(), ns)) - result.make_typecast(expr.type()); - - expr.swap(result); - simplify_rec(expr); - return false; - } - } - else - { - auto sub_size = pointer_offset_size(op_type_ptr->subtype(), ns); - - if(sub_size.has_value() && *sub_size > 0) - { - mp_integer index = offset / (*sub_size); - offset %= (*sub_size); - - result= - index_exprt( - result, - from_integer(index, expr.offset().type())); - } - } - } - } - else if(op_type.id()==ID_struct) - { - const struct_typet &struct_type= - to_struct_type(op_type); - const struct_typet::componentst &components= - struct_type.components(); - - mp_integer m_offset_bits=0; - for(const auto &component : components) - { - auto m_size = pointer_offset_bits(component.type(), ns); - if(!m_size.has_value() || *m_size <= 0) - break; - - if( - offset * 8 == m_offset_bits && *el_size == *m_size && - base_type_eq(expr.type(), component.type(), ns)) - { - member_exprt member(expr.op(), component.get_name(), component.type()); - simplify_member(member); - expr.swap(member); - - return false; - } - else if( - offset * 8 >= m_offset_bits && - offset * 8 + *el_size <= m_offset_bits + *m_size && - m_offset_bits % 8 == 0) - { - expr.op()= - member_exprt(expr.op(), component.get_name(), component.type()); - simplify_member(expr.op()); - expr.offset()= - from_integer(offset-m_offset_bits/8, expr.offset().type()); - simplify_rec(expr); - - return false; - } - - m_offset_bits += *m_size; - } - } - - return true; + simplify_rec(subexpr); + expr.swap(subexpr); + return false; } bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr) From d4296f16792e44a3a4fb3ba8e83f5c2706469afc Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 6 May 2018 18:46:07 +0100 Subject: [PATCH 2/2] Use get_subexpression_at_offset in pointer_logict We now support pointers into structs with zero-sized members, which is a GCC extension that we otherwise do support. --- regression/cbmc/Empty_struct2/main.c | 26 +++++++ regression/cbmc/Empty_struct2/test.desc | 8 +++ src/solvers/flattening/pointer_logic.cpp | 92 +++++++----------------- src/solvers/flattening/pointer_logic.h | 5 -- 4 files changed, 60 insertions(+), 71 deletions(-) create mode 100644 regression/cbmc/Empty_struct2/main.c create mode 100644 regression/cbmc/Empty_struct2/test.desc diff --git a/regression/cbmc/Empty_struct2/main.c b/regression/cbmc/Empty_struct2/main.c new file mode 100644 index 00000000000..b7ca99c7707 --- /dev/null +++ b/regression/cbmc/Empty_struct2/main.c @@ -0,0 +1,26 @@ +#include + +struct empty +{ +}; + +#pragma pack(1) +struct S +{ + char x; + struct empty e; + char y; +}; +#pragma pack() + +int main() +{ + struct S s; + assert(sizeof(struct S) == 2); + + struct empty *p = &s.e; + + assert(p == (char *)&s + 1); + + return 0; +} diff --git a/regression/cbmc/Empty_struct2/test.desc b/regression/cbmc/Empty_struct2/test.desc new file mode 100644 index 00000000000..9efefbc7362 --- /dev/null +++ b/regression/cbmc/Empty_struct2/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/solvers/flattening/pointer_logic.cpp b/src/solvers/flattening/pointer_logic.cpp index f3cae7926d0..ac2980e95d0 100644 --- a/src/solvers/flattening/pointer_logic.cpp +++ b/src/solvers/flattening/pointer_logic.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "pointer_logic.h" #include +#include #include #include #include @@ -98,76 +99,35 @@ exprt pointer_logict::pointer_expr( const exprt &object_expr=objects[pointer.object]; - exprt deep_object=object_rec(pointer.offset, type, object_expr); - - return address_of_exprt(deep_object, type); -} - -exprt pointer_logict::object_rec( - const mp_integer &offset, - const typet &pointer_type, - const exprt &src) const -{ - if(src.type().id()==ID_array) + typet subtype = type.subtype(); + // This is a gcc extension. + // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html + if(subtype.id() == ID_empty) + subtype = char_type(); + const exprt deep_object = + get_subexpression_at_offset(object_expr, pointer.offset, subtype, ns); + CHECK_RETURN(deep_object.is_not_nil()); + if(deep_object.id() != byte_extract_id()) + return address_of_exprt(deep_object, type); + + const byte_extract_exprt &be = to_byte_extract_expr(deep_object); + if(be.offset().is_zero()) + return address_of_exprt(be.op(), type); + + const auto subtype_bytes = pointer_offset_size(subtype, ns); + CHECK_RETURN(subtype_bytes.has_value() && *subtype_bytes > 0); + if(*subtype_bytes > pointer.offset) { - auto size = pointer_offset_size(src.type().subtype(), ns); - - if(!size.has_value() || *size == 0) - return src; - - mp_integer index = offset / (*size); - mp_integer rest = offset % (*size); - if(rest<0) - rest=-rest; - - index_exprt tmp(src.type().subtype()); - tmp.index()=from_integer(index, typet(ID_integer)); - tmp.array()=src; - - return object_rec(rest, pointer_type, tmp); + return plus_exprt( + address_of_exprt(be.op(), pointer_type(char_type())), + from_integer(pointer.offset, index_type())); } - else if(src.type().id()==ID_struct) + else { - const struct_typet::componentst &components= - to_struct_type(src.type()).components(); - - if(offset<0) - return src; - - mp_integer current_offset=0; - - for(const auto &c : components) - { - INVARIANT( - offset >= current_offset, - "when the object has not been found yet its offset must not be smaller" - "than the offset of the current struct component"); - - const typet &subtype=c.type(); - - const auto sub_size = pointer_offset_size(subtype, ns); - CHECK_RETURN(sub_size.has_value() && *sub_size != 0); - - mp_integer new_offset = current_offset + *sub_size; - - if(new_offset>offset) - { - // found it - member_exprt tmp(src, c); - - return object_rec( - offset-current_offset, pointer_type, tmp); - } - - current_offset=new_offset; - } - - return src; + return plus_exprt( + address_of_exprt(be.op(), pointer_type(char_type())), + from_integer(pointer.offset / *subtype_bytes, index_type())); } - else if(src.type().id()==ID_union) - return src; - - return src; } pointer_logict::pointer_logict(const namespacet &_ns):ns(_ns) diff --git a/src/solvers/flattening/pointer_logic.h b/src/solvers/flattening/pointer_logic.h index f1b791a7fd1..fb2f67aeb54 100644 --- a/src/solvers/flattening/pointer_logic.h +++ b/src/solvers/flattening/pointer_logic.h @@ -78,11 +78,6 @@ class pointer_logict exprt pointer_expr( const mp_integer &offset, const exprt &object) const; - - exprt object_rec( - const mp_integer &offset, - const typet &pointer_type, - const exprt &src) const; }; #endif // CPROVER_SOLVERS_FLATTENING_POINTER_LOGIC_H