From 7064483955114ea637bab7bdf5fe7f1811b23115 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 3 Mar 2016 02:15:12 +0000 Subject: [PATCH 1/6] simplify_typecast: simplify more pointer arithmetic --- src/util/simplify_expr.cpp | 22 +++++++++++++++++++--- 1 file changed, 19 insertions(+), 3 deletions(-) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 8482bfc32a5..47bed02b6ca 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -318,12 +318,14 @@ bool simplify_exprt::simplify_typecast(exprt &expr) // (int)((T*)0 + int) -> (int)(sizeof(T)*(size_t)int) if NULL is zero if(config.ansi_c.NULL_is_zero && (expr_type.id()==ID_signedbv || expr_type.id()==ID_unsignedbv) && + op_type.id()==ID_pointer && expr.op0().id()==ID_plus && expr.op0().operands().size()==2 && - expr.op0().op0().id()==ID_typecast && + ((expr.op0().op0().id()==ID_typecast && expr.op0().op0().operands().size()==1 && - expr.op0().op0().op0().is_zero() && - op_type.id()==ID_pointer) + expr.op0().op0().op0().is_zero()) || + (expr.op0().op0().is_constant() && + to_constant_expr(expr.op0().op0()).get_value()==ID_NULL))) { mp_integer sub_size=pointer_offset_size(op_type.subtype(), ns); if(sub_size!=-1) @@ -727,6 +729,20 @@ bool simplify_exprt::simplify_typecast(exprt &expr) return false; } } + else if(operand.id()==ID_address_of) + { + const exprt &o=to_address_of_expr(operand).object(); + + // turn &array into &array[0] when casting to pointer-to-element-type + if(o.type().id()==ID_array && + base_type_eq(expr_type, pointer_type(o.type().subtype()), ns)) + { + expr=address_of_exprt(index_exprt(o, from_integer(0, size_type()))); + + simplify_rec(expr); + return false; + } + } return true; } From ddd3d03188107fda99371c869edf661dba24eca1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 5 Feb 2016 08:12:38 +0000 Subject: [PATCH 2/6] Extended simplify for byte_update, typing --- src/util/simplify_expr.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 47bed02b6ca..decefa03781 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2132,6 +2132,14 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr) return false; } + + if(result_expr.is_not_nil()) + { + simplify_rec(result_expr); + expr.swap(result_expr); + + return false; + } } // replace elements of array or struct expressions, possibly using From 77236cc346cb905d4a5e5060c1478fe809ac0182 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 3 Mar 2016 02:24:11 +0000 Subject: [PATCH 3/6] Avoid nesting of ID_with/byte_update by rewriting byte_extract to use the root object --- src/goto-symex/symex_clean_expr.cpp | 31 +++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp index a894403c819..5179c5f88f1 100644 --- a/src/goto-symex/symex_clean_expr.cpp +++ b/src/goto-symex/symex_clean_expr.cpp @@ -67,11 +67,13 @@ void goto_symext::process_array_expr_rec( expr.swap(tmp); } else + { Forall_operands(it, expr) { typet t=it->type(); process_array_expr_rec(*it, t); } + } if(!base_type_eq(expr.type(), type, ns)) { @@ -166,6 +168,28 @@ void goto_symext::replace_array_equal(exprt &expr) replace_array_equal(*it); } +/// Rewrite index/member expressions in byte_extract to offset +static void adjust_byte_extract_rec(exprt &expr, const namespacet &ns) +{ + Forall_operands(it, expr) + adjust_byte_extract_rec(*it, ns); + + if(expr.id()==ID_byte_extract_big_endian || + expr.id()==ID_byte_extract_little_endian) + { + byte_extract_exprt &be=to_byte_extract_expr(expr); + if(be.op().id()==ID_symbol && + to_ssa_expr(be.op()).get_original_expr().get_bool(ID_C_invalid_object)) + return; + + object_descriptor_exprt ode; + ode.build(expr, ns); + + be.op()=ode.root_object(); + be.offset()=ode.offset(); + } +} + void goto_symext::clean_expr( exprt &expr, statet &state, @@ -173,5 +197,12 @@ void goto_symext::clean_expr( { replace_nondet(expr); dereference(expr, state, write); + + // make sure all remaining byte extract operations use the root + // object to avoid nesting of with/update and byte_update when on + // lhs + if(write) + adjust_byte_extract_rec(expr, ns); + replace_array_equal(expr); } From 81943f2c9ef9ec2f794ee90071823a575dba093c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 3 Jan 2017 13:45:43 +0000 Subject: [PATCH 4/6] Split ID_and/ID_or vs ID_xor simplification The code paths are vastly different, and splitting thus enables optimisations. --- src/util/simplify_expr_boolean.cpp | 121 ++++++++++++++--------------- 1 file changed, 60 insertions(+), 61 deletions(-) diff --git a/src/util/simplify_expr_boolean.cpp b/src/util/simplify_expr_boolean.cpp index 238dfd384c9..99a548927e1 100644 --- a/src/util/simplify_expr_boolean.cpp +++ b/src/util/simplify_expr_boolean.cpp @@ -72,21 +72,60 @@ bool simplify_exprt::simplify_boolean(exprt &expr) return false; } } - else if(expr.id()==ID_or || - expr.id()==ID_and || - expr.id()==ID_xor) + else if(expr.id()==ID_xor) { - if(operands.empty()) - return true; - bool result=true; - exprt::operandst::const_iterator last; - bool last_set=false; - bool negate=false; - for(exprt::operandst::iterator it=operands.begin(); + for(exprt::operandst::const_iterator it=operands.begin(); + it!=operands.end();) + { + if(it->type().id()!=ID_bool) + return true; + + bool erase; + + if(it->is_true()) + { + erase=true; + negate=!negate; + } + else + erase=it->is_false(); + + if(erase) + { + it=operands.erase(it); + result=false; + } + else + it++; + } + + if(operands.empty()) + { + expr.make_bool(negate); + return false; + } + else if(operands.size()==1) + { + exprt tmp(operands.front()); + if(negate) + tmp.make_not(); + expr.swap(tmp); + return false; + } + + return result; + } + else if(expr.id()==ID_and || expr.id()==ID_or) + { + std::unordered_set expr_set; + + bool result=true; + + for(exprt::operandst::const_iterator it=operands.begin(); it!=operands.end();) { if(it->type().id()!=ID_bool) @@ -106,21 +145,9 @@ bool simplify_exprt::simplify_boolean(exprt &expr) return false; } - bool erase; - - if(expr.id()==ID_and) - erase=is_true; - else if(is_true && expr.id()==ID_xor) - { - erase=true; - negate=!negate; - } - else - erase=is_false; - - if(last_set && *it==*last && - (expr.id()==ID_or || expr.id()==ID_and)) - erase=true; // erase duplicate operands + bool erase= + (expr.id()==ID_and ? is_true : is_false) || + !expr_set.insert(*it).second; if(erase) { @@ -128,55 +155,27 @@ bool simplify_exprt::simplify_boolean(exprt &expr) result=false; } else - { - last=it; - last_set=true; it++; - } } // search for a and !a - if(expr.id()==ID_and || expr.id()==ID_or) - { - // first gather all the a's with !a - - std::unordered_set expr_set; - - forall_operands(it, expr) - if(it->id()==ID_not && - it->operands().size()==1 && - it->type().id()==ID_bool) - expr_set.insert(it->op0()); - - // now search for a - - if(!expr_set.empty()) + for(const exprt &op : operands) + if(op.id()==ID_not && + op.operands().size()==1 && + op.type().id()==ID_bool && + expr_set.find(op.op0())!=expr_set.end()) { - forall_operands(it, expr) - { - if(it->id()!=ID_not && - expr_set.find(*it)!=expr_set.end()) - { - expr.make_bool(expr.id()==ID_or); - return false; - } - } + expr.make_bool(expr.id()==ID_or); + return false; } - } if(operands.empty()) { - if(expr.id()==ID_and || negate) - expr=true_exprt(); - else - expr=false_exprt(); - + expr.make_bool(expr.id()==ID_and); return false; } else if(operands.size()==1) { - if(negate) - expr.op0().make_not(); exprt tmp(operands.front()); expr.swap(tmp); return false; From 71e9642f0a341448f4863bb8feea22efd977e0a2 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 6 Jan 2017 23:58:03 +0000 Subject: [PATCH 5/6] Extensions to simplify_byte_extract Further simplify extracts from arrays and structs --- src/util/simplify_expr.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index decefa03781..670f933f8f6 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -1842,6 +1842,7 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr) 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()); @@ -1902,7 +1903,7 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr) simplify_member(expr.op()); expr.offset()= from_integer(offset-m_offset_bits/8, expr.offset().type()); - simplify_rec(expr.offset()); + simplify_rec(expr); return false; } From 14c00dc5987e5a6796c96884c52164f4437cf98c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 6 Jun 2017 05:56:30 +0000 Subject: [PATCH 6/6] Simplify all expressions generated by flatten_byte_operators We construct several non-trivial expressions that, e.g., contain sums over constants. As these expressions may be passed to array post-processing (flatten_byte_operators is in particular used with unbounded arrays) this can have a significant impact on the size of array index sets. --- .../flattening/flatten_byte_operators.cpp | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/solvers/flattening/flatten_byte_operators.cpp b/src/solvers/flattening/flatten_byte_operators.cpp index 34d166044e8..896ada763c9 100644 --- a/src/solvers/flattening/flatten_byte_operators.cpp +++ b/src/solvers/flattening/flatten_byte_operators.cpp @@ -242,12 +242,12 @@ exprt flatten_byte_extract( byte_extract_exprt tmp(unpacked); tmp.type()=subtype; - tmp.offset()=simplify_expr(new_offset, ns); + tmp.offset()=new_offset; array.copy_to_operands(flatten_byte_extract(tmp, ns)); } - return array; + return simplify_expr(array, ns); } } else if(type.id()==ID_struct) @@ -277,13 +277,13 @@ exprt flatten_byte_extract( byte_extract_exprt tmp(unpacked); tmp.type()=comp.type(); - tmp.offset()=simplify_expr(new_offset, ns); + tmp.offset()=new_offset; s.move_to_operands(tmp); } if(!failed) - return s; + return simplify_expr(s, ns); } const exprt &root=unpacked.op(); @@ -333,7 +333,7 @@ exprt flatten_byte_extract( { concatenation_exprt concatenation(src.type()); concatenation.operands().swap(op); - return concatenation; + return simplify_expr(concatenation, ns); } } @@ -413,7 +413,7 @@ exprt flatten_byte_update( result.swap(with_expr); } - return result; + return simplify_expr(result, ns); } else // sub_size!=1 { @@ -512,7 +512,7 @@ exprt flatten_byte_update( result=with_expr; } - return result; + return simplify_expr(result, ns); } } else @@ -583,7 +583,7 @@ exprt flatten_byte_update( // original_bits |= newvalue bitor_exprt bitor_expr(bitand_expr, value_shifted); - return bitor_expr; + return simplify_expr(bitor_expr, ns); } else {