From ac0b12acbf226fafe0b1e7c0c456bc31be67bae9 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 26 Jun 2016 13:22:00 +0000 Subject: [PATCH 1/5] Mark internal functions static --- src/goto-programs/remove_complex.cpp | 18 +++++++++--------- src/goto-programs/remove_vector.cpp | 14 +++++++------- 2 files changed, 16 insertions(+), 16 deletions(-) diff --git a/src/goto-programs/remove_complex.cpp b/src/goto-programs/remove_complex.cpp index 553a70dab50..d48d432f55c 100644 --- a/src/goto-programs/remove_complex.cpp +++ b/src/goto-programs/remove_complex.cpp @@ -12,9 +12,6 @@ Date: September 2014 #include "remove_complex.h" -void remove_complex(typet &); -void remove_complex(exprt &); - /*******************************************************************\ Function: complex_member @@ -27,7 +24,7 @@ Function: complex_member \*******************************************************************/ -exprt complex_member(const exprt &expr, irep_idt id) +static exprt complex_member(const exprt &expr, irep_idt id) { if(expr.id()==ID_struct && expr.operands().size()==2) { @@ -60,7 +57,9 @@ Purpose: removes complex data type \*******************************************************************/ -void remove_complex(exprt &expr) +static void remove_complex(typet &); + +static void remove_complex(exprt &expr) { if(expr.id()==ID_typecast) { @@ -200,7 +199,7 @@ Purpose: removes complex data type \*******************************************************************/ -void remove_complex(typet &type) +static void remove_complex(typet &type) { if(type.id()==ID_struct || type.id()==ID_union) { @@ -250,7 +249,7 @@ Purpose: removes complex data type \*******************************************************************/ -void remove_complex(symbolt &symbol) +static void remove_complex(symbolt &symbol) { remove_complex(symbol.value); remove_complex(symbol.type); @@ -286,7 +285,8 @@ Purpose: removes complex data type \*******************************************************************/ -void remove_complex(goto_functionst::goto_functiont &goto_function) +static void remove_complex( + goto_functionst::goto_functiont &goto_function) { remove_complex(goto_function.type); @@ -309,7 +309,7 @@ Purpose: removes complex data type \*******************************************************************/ -void remove_complex(goto_functionst &goto_functions) +static void remove_complex(goto_functionst &goto_functions) { Forall_goto_functions(it, goto_functions) remove_complex(it->second); diff --git a/src/goto-programs/remove_vector.cpp b/src/goto-programs/remove_vector.cpp index 90df83ca43b..02d9d2e8fab 100644 --- a/src/goto-programs/remove_vector.cpp +++ b/src/goto-programs/remove_vector.cpp @@ -12,8 +12,6 @@ Date: September 2014 #include "remove_vector.h" -void remove_vector(typet &); -void remove_vector(exprt &); /*******************************************************************\ @@ -27,7 +25,9 @@ Purpose: removes vector data type \*******************************************************************/ -void remove_vector(exprt &expr) +static void remove_vector(typet &); + +static void remove_vector(exprt &expr) { Forall_operands(it, expr) remove_vector(*it); @@ -109,7 +109,7 @@ Purpose: removes vector data type \*******************************************************************/ -void remove_vector(typet &type) +static void remove_vector(typet &type) { if(type.id()==ID_struct || type.id()==ID_union) { @@ -155,7 +155,7 @@ Purpose: removes vector data type \*******************************************************************/ -void remove_vector(symbolt &symbol) +static void remove_vector(symbolt &symbol) { remove_vector(symbol.value); remove_vector(symbol.type); @@ -173,7 +173,7 @@ Purpose: removes vector data type \*******************************************************************/ -void remove_vector(symbol_tablet &symbol_table) +static void remove_vector(symbol_tablet &symbol_table) { Forall_symbols(it, symbol_table.symbols) remove_vector(it->second); @@ -214,7 +214,7 @@ Purpose: removes vector data type \*******************************************************************/ -void remove_vector(goto_functionst &goto_functions) +static void remove_vector(goto_functionst &goto_functions) { Forall_goto_functions(it, goto_functions) remove_vector(it->second); From 8ae5ccad4270db9d67e6271034e7f1c612ac47e9 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 26 Jun 2016 13:23:39 +0000 Subject: [PATCH 2/5] remove_complex: modify expressions only when necessary --- src/goto-programs/remove_complex.cpp | 90 ++++++++++++++++++++++++++++ 1 file changed, 90 insertions(+) diff --git a/src/goto-programs/remove_complex.cpp b/src/goto-programs/remove_complex.cpp index d48d432f55c..ed5e916f9f3 100644 --- a/src/goto-programs/remove_complex.cpp +++ b/src/goto-programs/remove_complex.cpp @@ -47,6 +47,90 @@ static exprt complex_member(const exprt &expr, irep_idt id) /*******************************************************************\ +Function: have_to_remove_complex + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +static bool have_to_remove_complex(const typet &type); + +static bool have_to_remove_complex(const exprt &expr) +{ + if(expr.id()==ID_typecast && + to_typecast_expr(expr).op().type().id()==ID_complex && + expr.type().id()!=ID_complex) + return true; + + if(expr.type().id()==ID_complex) + { + if(expr.id()==ID_plus || expr.id()==ID_minus || + expr.id()==ID_mult || expr.id()==ID_div) + return true; + else if(expr.id()==ID_unary_minus) + return true; + else if(expr.id()==ID_complex) + return true; + else if(expr.id()==ID_typecast) + return true; + } + + if(expr.id()==ID_complex_real) + return true; + else if(expr.id()==ID_complex_imag) + return true; + + if(have_to_remove_complex(expr.type())) + return true; + + forall_operands(it, expr) + if(have_to_remove_complex(*it)) + return true; + + return false; +} + +/*******************************************************************\ + +Function: have_to_remove_complex + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +static bool have_to_remove_complex(const typet &type) +{ + if(type.id()==ID_struct || type.id()==ID_union) + { + const struct_union_typet &struct_union_type= + to_struct_union_type(type); + for(struct_union_typet::componentst::const_iterator + it=struct_union_type.components().begin(); + it!=struct_union_type.components().end(); + it++) + if(have_to_remove_complex(it->type())) + return true; + } + else if(type.id()==ID_pointer || + type.id()==ID_vector || + type.id()==ID_array) + return have_to_remove_complex(type.subtype()); + else if(type.id()==ID_complex) + return true; + + return false; +} + +/*******************************************************************\ + Function: remove_complex Inputs: @@ -61,6 +145,9 @@ static void remove_complex(typet &); static void remove_complex(exprt &expr) { + if(!have_to_remove_complex(expr)) + return; + if(expr.id()==ID_typecast) { assert(expr.operands().size()==1); @@ -201,6 +288,9 @@ Purpose: removes complex data type static void remove_complex(typet &type) { + if(!have_to_remove_complex(type)) + return; + if(type.id()==ID_struct || type.id()==ID_union) { struct_union_typet &struct_union_type= From a77377e45211c0060a36ac5fdba528b7fd9ea1a0 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 26 Jun 2016 13:24:45 +0000 Subject: [PATCH 3/5] remove_vector: modify expressions only when necessary --- src/goto-programs/remove_vector.cpp | 80 +++++++++++++++++++++++++++++ 1 file changed, 80 insertions(+) diff --git a/src/goto-programs/remove_vector.cpp b/src/goto-programs/remove_vector.cpp index 02d9d2e8fab..f7b63e42d4f 100644 --- a/src/goto-programs/remove_vector.cpp +++ b/src/goto-programs/remove_vector.cpp @@ -12,6 +12,80 @@ Date: September 2014 #include "remove_vector.h" +/*******************************************************************\ + +Function: have_to_remove_vector + +Inputs: + +Outputs: + +Purpose: + +\*******************************************************************/ + +static bool have_to_remove_vector(const typet &type); + +static bool have_to_remove_vector(const exprt &expr) +{ + if(expr.type().id()==ID_vector) + { + if(expr.id()==ID_plus || expr.id()==ID_minus || + expr.id()==ID_mult || expr.id()==ID_div || + expr.id()==ID_mod || expr.id()==ID_bitxor || + expr.id()==ID_bitand || expr.id()==ID_bitor) + return true; + else if(expr.id()==ID_unary_minus || expr.id()==ID_bitnot) + return true; + else if(expr.id()==ID_vector) + return true; + } + + if(have_to_remove_vector(expr.type())) + return true; + + forall_operands(it, expr) + if(have_to_remove_vector(*it)) + return true; + + return false; +} + +/*******************************************************************\ + +Function: have_to_remove_vector + +Inputs: + +Outputs: + +Purpose: + +\*******************************************************************/ + +static bool have_to_remove_vector(const typet &type) +{ + if(type.id()==ID_struct || type.id()==ID_union) + { + const struct_union_typet &struct_union_type= + to_struct_union_type(type); + + for(struct_union_typet::componentst::const_iterator + it=struct_union_type.components().begin(); + it!=struct_union_type.components().end(); + it++) + if(have_to_remove_vector(it->type())) + return true; + } + else if(type.id()==ID_pointer || + type.id()==ID_complex || + type.id()==ID_array) + return have_to_remove_vector(type.subtype()); + else if(type.id()==ID_vector) + return true; + + return false; +} /*******************************************************************\ @@ -29,6 +103,9 @@ static void remove_vector(typet &); static void remove_vector(exprt &expr) { + if(!have_to_remove_vector(expr)) + return; + Forall_operands(it, expr) remove_vector(*it); @@ -111,6 +188,9 @@ Purpose: removes vector data type static void remove_vector(typet &type) { + if(!have_to_remove_vector(type)) + return; + if(type.id()==ID_struct || type.id()==ID_union) { struct_union_typet &struct_union_type= From d08c44aa1349c440325525fb7daa58fa9c18c75c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 25 Jun 2016 21:01:32 +0200 Subject: [PATCH 4/5] Apply adjust_float_expressions, rewrite_union just once per expression These should be applied once across all goto functions instead of possibly applying them multiple times to the same source expression during symbolic execution. Signed-off-by: Michael Tautschnig --- src/cbmc/cbmc_parse_options.cpp | 6 ++ src/goto-symex/adjust_float_expressions.cpp | 72 +++++++++++++++++++++ src/goto-symex/adjust_float_expressions.h | 11 +++- src/goto-symex/rewrite_union.cpp | 63 ++++++++++++++++++ src/goto-symex/rewrite_union.h | 13 +++- src/goto-symex/symex_clean_expr.cpp | 4 -- src/path-symex/path_symex_state_read.cpp | 21 ++---- src/symex/symex_parse_options.cpp | 5 ++ 8 files changed, 171 insertions(+), 24 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 35a5002572d..73255cfeb63 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -39,6 +39,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include +#include + #include #include #include @@ -891,10 +894,13 @@ bool cbmc_parse_optionst::process_goto_program( remove_returns(symbol_table, goto_functions); remove_vector(symbol_table, goto_functions); remove_complex(symbol_table, goto_functions); + rewrite_union(goto_functions, ns); // add generic checks status() << "Generic Property Instrumentation" << eom; goto_check(ns, options, goto_functions); + // checks don't know about adjusted float expressions + adjust_float_expressions(goto_functions, ns); // ignore default/user-specified initialization // of variables with static lifetime diff --git a/src/goto-symex/adjust_float_expressions.cpp b/src/goto-symex/adjust_float_expressions.cpp index 94048db8e5f..97ef7f56fe2 100644 --- a/src/goto-symex/adjust_float_expressions.cpp +++ b/src/goto-symex/adjust_float_expressions.cpp @@ -13,6 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include "adjust_float_expressions.h" /*******************************************************************\ @@ -32,6 +34,15 @@ void adjust_float_expressions( exprt &expr, const namespacet &ns) { + if(expr.id()==ID_floatbv_plus || + expr.id()==ID_floatbv_minus || + expr.id()==ID_floatbv_mult || + expr.id()==ID_floatbv_div || + expr.id()==ID_floatbv_div || + expr.id()==ID_floatbv_rem || + expr.id()==ID_floatbv_typecast) + return; + Forall_operands(it, expr) adjust_float_expressions(*it, ns); @@ -126,3 +137,64 @@ void adjust_float_expressions( } } } + +/*******************************************************************\ + +Function: adjust_float_expressions + +Inputs: + +Outputs: + +Purpose: + +\*******************************************************************/ + +static void adjust_float_expressions( + goto_functionst::goto_functiont &goto_function, + const namespacet &ns) +{ + Forall_goto_program_instructions(it, goto_function.body) + { + adjust_float_expressions(it->code, ns); + adjust_float_expressions(it->guard, ns); + } +} + +/*******************************************************************\ + +Function: adjust_float_expressions + +Inputs: + +Outputs: + +Purpose: + +\*******************************************************************/ + +void adjust_float_expressions( + goto_functionst &goto_functions, + const namespacet &ns) +{ + Forall_goto_functions(it, goto_functions) + adjust_float_expressions(it->second, ns); +} + +/*******************************************************************\ + +Function: adjust_float_expressions + +Inputs: + +Outputs: + +Purpose: + +\*******************************************************************/ + +void adjust_float_expressions(goto_modelt &goto_model) +{ + namespacet ns(goto_model.symbol_table); + adjust_float_expressions(goto_model.goto_functions, ns); +} diff --git a/src/goto-symex/adjust_float_expressions.h b/src/goto-symex/adjust_float_expressions.h index c8c87260996..f8547c59fa8 100644 --- a/src/goto-symex/adjust_float_expressions.h +++ b/src/goto-symex/adjust_float_expressions.h @@ -9,11 +9,18 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H #define CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H -#include -#include +class exprt; +class namespacet; +class goto_functionst; +class goto_modelt; void adjust_float_expressions( exprt &expr, const namespacet &ns); +void adjust_float_expressions( + goto_functionst &goto_functions, + const namespacet &ns); +void adjust_float_expressions(goto_modelt &goto_model); + #endif // CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H diff --git a/src/goto-symex/rewrite_union.cpp b/src/goto-symex/rewrite_union.cpp index 26b9282dfdf..d96768e2234 100644 --- a/src/goto-symex/rewrite_union.cpp +++ b/src/goto-symex/rewrite_union.cpp @@ -11,6 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include #include "rewrite_union.h" @@ -57,3 +59,64 @@ void rewrite_union( expr=tmp; } } + +/*******************************************************************\ + +Function: rewrite_union + +Inputs: + +Outputs: + +Purpose: + +\*******************************************************************/ + +static void rewrite_union( + goto_functionst::goto_functiont &goto_function, + const namespacet &ns) +{ + Forall_goto_program_instructions(it, goto_function.body) + { + rewrite_union(it->code, ns); + rewrite_union(it->guard, ns); + } +} + +/*******************************************************************\ + +Function: rewrite_union + +Inputs: + +Outputs: + +Purpose: + +\*******************************************************************/ + +void rewrite_union( + goto_functionst &goto_functions, + const namespacet &ns) +{ + Forall_goto_functions(it, goto_functions) + rewrite_union(it->second, ns); +} + +/*******************************************************************\ + +Function: rewrite_union + +Inputs: + +Outputs: + +Purpose: + +\*******************************************************************/ + +void rewrite_union(goto_modelt &goto_model) +{ + namespacet ns(goto_model.symbol_table); + rewrite_union(goto_model.goto_functions, ns); +} diff --git a/src/goto-symex/rewrite_union.h b/src/goto-symex/rewrite_union.h index 8f406960bc2..7215e0bf0a4 100644 --- a/src/goto-symex/rewrite_union.h +++ b/src/goto-symex/rewrite_union.h @@ -9,11 +9,20 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_SYMEX_REWRITE_UNION_H #define CPROVER_GOTO_SYMEX_REWRITE_UNION_H -#include -#include +#include + +class exprt; +class namespacet; +class goto_functionst; +class goto_modelt; void rewrite_union( exprt &expr, const namespacet &ns); +void rewrite_union( + goto_functionst &goto_functions, + const namespacet &ns); +void rewrite_union(goto_modelt &goto_model); + #endif // CPROVER_GOTO_SYMEX_REWRITE_UNION_H diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp index 338854922b3..807c24d872a 100644 --- a/src/goto-symex/symex_clean_expr.cpp +++ b/src/goto-symex/symex_clean_expr.cpp @@ -13,8 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include "adjust_float_expressions.h" -#include "rewrite_union.h" #include "goto_symex.h" /*******************************************************************\ @@ -199,9 +197,7 @@ void goto_symext::clean_expr( statet &state, const bool write) { - rewrite_union(expr, ns); replace_nondet(expr); dereference(expr, state, write); replace_array_equal(expr); - adjust_float_expressions(expr, ns); } diff --git a/src/path-symex/path_symex_state_read.cpp b/src/path-symex/path_symex_state_read.cpp index 33aab3c5fc5..72fbc683f1c 100644 --- a/src/path-symex/path_symex_state_read.cpp +++ b/src/path-symex/path_symex_state_read.cpp @@ -11,9 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include -#include - #include "path_symex_state.h" //#define DEBUG @@ -41,21 +38,13 @@ exprt path_symex_statet::read(const exprt &src, bool propagate) //std::cout << "path_symex_statet::read " << src.pretty() << std::endl; #endif - // This has five phases! - // 1. Floating-point expression adjustment (rounding mode) - // 2. Rewrite unions into byte operators - // 3. Dereferencing, including propagation of pointers. - // 4. Rewriting to SSA symbols - // 5. Simplifier - - exprt tmp1=src; - adjust_float_expressions(tmp1, var_map.ns); - - exprt tmp2=tmp1; - rewrite_union(tmp2, var_map.ns); + // This has three phases! + // 1. Dereferencing, including propagation of pointers. + // 2. Rewriting to SSA symbols + // 3. Simplifier // we force propagation for dereferencing - exprt tmp3=dereference_rec(tmp2, true); + exprt tmp3=dereference_rec(src, true); exprt tmp4=instantiate_rec(tmp3, propagate); diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp index 7a9227e6f58..575dcb833bb 100644 --- a/src/symex/symex_parse_options.cpp +++ b/src/symex/symex_parse_options.cpp @@ -33,6 +33,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include +#include + #include #include @@ -359,6 +362,8 @@ bool symex_parse_optionst::process_goto_program(const optionst &options) remove_complex(goto_model); remove_vector(goto_model); remove_virtual_functions(goto_model); + rewrite_union(goto_model); + adjust_float_expressions(goto_model); // recalculate numbers, etc. goto_model.goto_functions.update(); From 979d120db4c137bd5998fecf8c2f90f64dae97a6 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 26 Jun 2016 13:29:15 +0000 Subject: [PATCH 5/5] rewrite_union, adjust_float_expressions: modify expressions only when necessary --- src/goto-symex/adjust_float_expressions.cpp | 71 +++++++++++++++++++-- src/goto-symex/rewrite_union.cpp | 37 +++++++++++ 2 files changed, 103 insertions(+), 5 deletions(-) diff --git a/src/goto-symex/adjust_float_expressions.cpp b/src/goto-symex/adjust_float_expressions.cpp index 97ef7f56fe2..46dee137447 100644 --- a/src/goto-symex/adjust_float_expressions.cpp +++ b/src/goto-symex/adjust_float_expressions.cpp @@ -19,19 +19,18 @@ Author: Daniel Kroening, kroening@kroening.com /*******************************************************************\ -Function: adjust_float_expressions +Function: have_to_adjust_float_expressions Inputs: Outputs: - Purpose: This adds the rounding mode to floating-point operations, - including those in vectors and complex numbers. + Purpose: \*******************************************************************/ -void adjust_float_expressions( - exprt &expr, +static bool have_to_adjust_float_expressions( + const exprt &expr, const namespacet &ns) { if(expr.id()==ID_floatbv_plus || @@ -41,6 +40,68 @@ void adjust_float_expressions( expr.id()==ID_floatbv_div || expr.id()==ID_floatbv_rem || expr.id()==ID_floatbv_typecast) + return false; + + const typet &type=ns.follow(expr.type()); + + if(type.id()==ID_floatbv || + (type.id()==ID_complex && + ns.follow(type.subtype()).id()==ID_floatbv)) + { + if(expr.id()==ID_plus || expr.id()==ID_minus || + expr.id()==ID_mult || expr.id()==ID_div || + expr.id()==ID_rem) + return true; + } + + if(expr.id()==ID_typecast) + { + const typecast_exprt &typecast_expr=to_typecast_expr(expr); + + const typet &src_type=typecast_expr.op().type(); + const typet &dest_type=typecast_expr.type(); + + if(dest_type.id()==ID_floatbv && + src_type.id()==ID_floatbv) + return true; + else if(dest_type.id()==ID_floatbv && + (src_type.id()==ID_c_bool || + src_type.id()==ID_signedbv || + src_type.id()==ID_unsignedbv || + src_type.id()==ID_c_enum_tag)) + return true; + else if((dest_type.id()==ID_signedbv || + dest_type.id()==ID_unsignedbv || + dest_type.id()==ID_c_enum_tag) && + src_type.id()==ID_floatbv) + return true; + } + + forall_operands(it, expr) + if(have_to_adjust_float_expressions(*it, ns)) + return true; + + return false; +} + +/*******************************************************************\ + +Function: adjust_float_expressions + + Inputs: + + Outputs: + + Purpose: This adds the rounding mode to floating-point operations, + including those in vectors and complex numbers. + +\*******************************************************************/ + +void adjust_float_expressions( + exprt &expr, + const namespacet &ns) +{ + if(!have_to_adjust_float_expressions(expr, ns)) return; Forall_operands(it, expr) diff --git a/src/goto-symex/rewrite_union.cpp b/src/goto-symex/rewrite_union.cpp index d96768e2234..420d03e6a63 100644 --- a/src/goto-symex/rewrite_union.cpp +++ b/src/goto-symex/rewrite_union.cpp @@ -19,6 +19,40 @@ Author: Daniel Kroening, kroening@kroening.com /*******************************************************************\ +Function: have_to_rewrite_union + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +static bool have_to_rewrite_union( + const exprt &expr, + const namespacet &ns) +{ + if(expr.id()==ID_member) + { + const exprt &op=to_member_expr(expr).struct_op(); + const typet &op_type=ns.follow(op.type()); + + if(op_type.id()==ID_union) + return true; + } + else if(expr.id()==ID_union) + return true; + + forall_operands(it, expr) + if(have_to_rewrite_union(*it, ns)) + return true; + + return false; +} + +/*******************************************************************\ + Function: rewrite_union Inputs: @@ -34,6 +68,9 @@ void rewrite_union( exprt &expr, const namespacet &ns) { + if(!have_to_rewrite_union(expr, ns)) + return; + Forall_operands(it, expr) rewrite_union(*it, ns);