diff --git a/regression/ansi-c/code_contracts1/main.c b/regression/ansi-c/code_contracts1/main.c new file mode 100644 index 00000000000..19f8efb226b --- /dev/null +++ b/regression/ansi-c/code_contracts1/main.c @@ -0,0 +1,17 @@ +int foo() +__CPROVER_ensures(__CPROVER_forall {int i; 1 == 1}) +{ + return 1; +} + +int bar() +__CPROVER_ensures(__CPROVER_forall {int i; 1 == 1} && + __CPROVER_return_value == 1) +{ + return 1; +} + +int main() { + foo(); + bar(); +} diff --git a/regression/ansi-c/code_contracts1/test.desc b/regression/ansi-c/code_contracts1/test.desc new file mode 100644 index 00000000000..466da18b2b5 --- /dev/null +++ b/regression/ansi-c/code_contracts1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ diff --git a/regression/contracts/function_apply_01/test.desc b/regression/contracts/function_apply_01/test.desc index abc8686ad8e..4f37c84c808 100644 --- a/regression/contracts/function_apply_01/test.desc +++ b/regression/contracts/function_apply_01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --apply-code-contracts ^EXIT=0$ @@ -6,4 +6,3 @@ main.c ^VERIFICATION SUCCESSFUL$ -- -- -Applying code contracts currently also checks them. diff --git a/regression/contracts/function_check_01/test.desc b/regression/contracts/function_check_01/test.desc index d9a2ec0a8ca..a44b7e292f5 100644 --- a/regression/contracts/function_check_01/test.desc +++ b/regression/contracts/function_check_01/test.desc @@ -1,11 +1,8 @@ CORE main.c ---apply-code-contracts +--check-code-contracts ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -- ---check-code-contracts not implemented yet. ---apply-code-contracts is the current name for the flag. This should be -updated as the flag changes. diff --git a/regression/contracts/function_check_04/test.desc b/regression/contracts/function_check_04/test.desc index db7ee5aa32a..1a229ae78d6 100644 --- a/regression/contracts/function_check_04/test.desc +++ b/regression/contracts/function_check_04/test.desc @@ -1,11 +1,8 @@ CORE main.c ---apply-code-contracts +--check-code-contracts ^\[main.assertion.1\] assertion x == 0: SUCCESS$ ^\[foo.1\] : FAILURE$ ^VERIFICATION FAILED$ -- -- ---check-code-contracts not implemented yet. ---apply-code-contracts is the current name for the flag. This should be -updated as the flag changes. diff --git a/regression/contracts/function_check_05/test.desc b/regression/contracts/function_check_05/test.desc index 77e210f10d8..49cdb0a73fe 100644 --- a/regression/contracts/function_check_05/test.desc +++ b/regression/contracts/function_check_05/test.desc @@ -1,10 +1,9 @@ -KNOWNBUG +CORE main.c --check-code-contracts ^\[main.assertion.1\] assertion y == 0: FAILURE$ ^\[main.assertion.2\] assertion z == 1: SUCCESS$ ^\[foo.1\] : SUCCESS$ -^VERIFICATION SUCCESSFUL$ +^VERIFICATION FAILED$ -- -- -Contract checking does not properly havoc function calls. diff --git a/regression/contracts/function_check_mem_01/main.c b/regression/contracts/function_check_mem_01/main.c index b63364f4d57..10d79cf8190 100644 --- a/regression/contracts/function_check_mem_01/main.c +++ b/regression/contracts/function_check_mem_01/main.c @@ -33,7 +33,7 @@ void foo(bar *x) __CPROVER_requires(__CPROVER_VALID_MEM(x, sizeof(bar))) { x->x += 1; - return + return; } int main() diff --git a/regression/contracts/function_check_mem_01/test.desc b/regression/contracts/function_check_mem_01/test.desc index b46799f781b..c45406ad744 100644 --- a/regression/contracts/function_check_mem_01/test.desc +++ b/regression/contracts/function_check_mem_01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --check-code-contracts ^EXIT=0$ diff --git a/regression/contracts/invar_check_01/test.desc b/regression/contracts/invar_check_01/test.desc index d9a2ec0a8ca..a44b7e292f5 100644 --- a/regression/contracts/invar_check_01/test.desc +++ b/regression/contracts/invar_check_01/test.desc @@ -1,11 +1,8 @@ CORE main.c ---apply-code-contracts +--check-code-contracts ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -- ---check-code-contracts not implemented yet. ---apply-code-contracts is the current name for the flag. This should be -updated as the flag changes. diff --git a/regression/contracts/invar_check_02/test.desc b/regression/contracts/invar_check_02/test.desc index d9a2ec0a8ca..a44b7e292f5 100644 --- a/regression/contracts/invar_check_02/test.desc +++ b/regression/contracts/invar_check_02/test.desc @@ -1,11 +1,8 @@ CORE main.c ---apply-code-contracts +--check-code-contracts ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -- ---check-code-contracts not implemented yet. ---apply-code-contracts is the current name for the flag. This should be -updated as the flag changes. diff --git a/regression/contracts/invar_check_03/test.desc b/regression/contracts/invar_check_03/test.desc index d9a2ec0a8ca..a44b7e292f5 100644 --- a/regression/contracts/invar_check_03/test.desc +++ b/regression/contracts/invar_check_03/test.desc @@ -1,11 +1,8 @@ CORE main.c ---apply-code-contracts +--check-code-contracts ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -- ---check-code-contracts not implemented yet. ---apply-code-contracts is the current name for the flag. This should be -updated as the flag changes. diff --git a/regression/contracts/invar_check_04/test.desc b/regression/contracts/invar_check_04/test.desc index 7414b7f58a6..f24cdd9f7e4 100644 --- a/regression/contracts/invar_check_04/test.desc +++ b/regression/contracts/invar_check_04/test.desc @@ -1,12 +1,9 @@ CORE main.c ---apply-code-contracts +--check-code-contracts ^\[main.1\] Loop invariant violated before entry: SUCCESS$ ^\[main.2\] Loop invariant not preserved: SUCCESS$ ^\[main.assertion.1\] assertion r == 0: FAILURE$ ^VERIFICATION FAILED$ -- -- ---check-code-contracts not implemented yet. ---apply-code-contracts is the current name for the flag. This should be -updated as the flag changes. diff --git a/regression/goto-instrument/slice19/test.desc b/regression/goto-instrument/slice19/test.desc index 03cff4a4fac..3793f7374e1 100644 --- a/regression/goto-instrument/slice19/test.desc +++ b/regression/goto-instrument/slice19/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --full-slice ^EXIT=0$ diff --git a/regression/goto-instrument/slice24/main.c b/regression/goto-instrument/slice24/main.c new file mode 100644 index 00000000000..2149d6ba087 --- /dev/null +++ b/regression/goto-instrument/slice24/main.c @@ -0,0 +1,14 @@ +#include +#include + +static void f(int *x) { *x = 5; } +static void g(int *x) { assert(*x == 5); } + +int main(int argc, char **argv) +{ + int *x = (int*)malloc(sizeof(int)); + f(x); + g(x); + + return 0; +} diff --git a/regression/goto-instrument/slice24/test.desc b/regression/goto-instrument/slice24/test.desc new file mode 100644 index 00000000000..3906443eafc --- /dev/null +++ b/regression/goto-instrument/slice24/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +main.c +--full-slice --add-library +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +Data dependencies across function calls are still not working correctly. diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index 24c0320af66..ada58117611 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -175,7 +175,9 @@ void dep_graph_domaint::data_dependencies( { bool found=false; for(const auto &wr : w_range.second) + { for(const auto &r_range : r_ranges) + { if(!found && may_be_def_use_pair(wr.first, wr.second, r_range.first, r_range.second)) @@ -184,6 +186,8 @@ void dep_graph_domaint::data_dependencies( data_deps.insert(w_range.first); found=true; } + } + } } dep_graph.reaching_definitions()[to].clear_cache(it->first); diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index 61e7467669b..4c9acbd01de 100644 --- a/src/analyses/goto_rw.cpp +++ b/src/analyses/goto_rw.cpp @@ -128,8 +128,6 @@ void rw_range_sett::get_objects_dereference( { const exprt &pointer=deref.pointer(); get_objects_rec(get_modet::READ, pointer); - if(mode!=get_modet::READ) - get_objects_rec(mode, pointer); } void rw_range_sett::get_objects_byte_extract( @@ -414,16 +412,19 @@ void rw_range_sett::get_objects_typecast( void rw_range_sett::get_objects_address_of(const exprt &object) { - if(object.id() == ID_string_constant || + if(object.id() == ID_symbol || + object.id() == ID_string_constant || object.id() == ID_label || object.id() == ID_array || object.id() == ID_null_object) // constant, nothing to do + { return; - else if(object.id()==ID_symbol) - get_objects_rec(get_modet::READ, object); + } else if(object.id()==ID_dereference) + { get_objects_rec(get_modet::READ, object); + } else if(object.id()==ID_index) { const index_exprt &index=to_index_expr(object); @@ -524,6 +525,11 @@ void rw_range_sett::get_objects_rec( get_objects_array(mode, to_array_expr(expr), range_start, size); else if(expr.id()==ID_struct) get_objects_struct(mode, to_struct_expr(expr), range_start, size); + else if(expr.id()==ID_dynamic_object) + { + const auto obj_instance = to_dynamic_object_expr(expr).get_instance(); + add(mode, "goto_rw::dynamic_object-" + std::to_string(obj_instance), 0, -1); + } else if(expr.id()==ID_symbol) { const symbol_exprt &symbol=to_symbol_expr(expr); @@ -564,11 +570,6 @@ void rw_range_sett::get_objects_rec( { // dereferencing may yield some weird ones, ignore these } - else if(mode==get_modet::LHS_W) - { - forall_operands(it, expr) - get_objects_rec(mode, *it); - } else throw "rw_range_sett: assignment to `"+expr.id_string()+"' not handled"; } @@ -605,6 +606,8 @@ void rw_range_set_value_sett::get_objects_dereference( exprt object=deref; dereference(target, object, ns, value_sets); + PRECONDITION(object.is_not_nil()); + range_spect new_size= to_range_spect(pointer_offset_bits(object.type(), ns)); diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp index 7788835f0db..e3fae64dceb 100644 --- a/src/analyses/reaching_definitions.cpp +++ b/src/analyses/reaching_definitions.cpp @@ -307,19 +307,19 @@ void rd_range_domaint::transform_assign( { const irep_idt &identifier=it->first; // ignore symex::invalid_object - const symbolt *symbol_ptr; - if(ns.lookup(identifier, symbol_ptr)) + const symbolt *symbol_ptr = nullptr; + bool not_found = ns.lookup(identifier, symbol_ptr); + if(not_found && has_prefix(id2string(identifier), "symex::invalid_object")) + { continue; - INVARIANT_STRUCTURED( - symbol_ptr!=nullptr, - nullptr_exceptiont, - "Symbol is in symbol table"); + } const range_domaint &ranges=rw_set.get_ranges(it); if(is_must_alias && (!rd.get_is_threaded()(from) || - (!symbol_ptr->is_shared() && + (symbol_ptr != nullptr && + symbol_ptr->is_shared() && !rd.get_is_dirty()(identifier)))) for(const auto &range : ranges) kill(identifier, range.first, range.second); diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index ee120fe00fd..07f3bf25910 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -760,11 +760,15 @@ void c_typecheck_baset::typecheck_declaration( typet ret_type=empty_typet(); if(new_symbol.type.id()==ID_code) ret_type=to_code_type(new_symbol.type).return_type(); - assert(parameter_map.empty()); if(ret_type.id()!=ID_empty) + { + DATA_INVARIANT( + parameter_map.empty(), "parameter map should be cleared"); parameter_map["__CPROVER_return_value"]=ret_type; + } typecheck_spec_expr(contract, ID_C_spec_ensures); - parameter_map.clear(); + if(ret_type.id()!=ID_empty) + parameter_map.clear(); if(contract.find(ID_C_spec_requires).is_not_nil()) new_symbol.type.add(ID_C_spec_requires)= diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index b8b0e7fe595..b598822b084 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2139,11 +2139,10 @@ exprt c_typecheck_baset::do_special_functions( throw 0; } - exprt dynamic_object_expr=exprt(ID_dynamic_object, expr.type()); - dynamic_object_expr.operands()=expr.arguments(); - dynamic_object_expr.add_source_location()=source_location; + exprt is_dynamic_object_expr = is_dynamic_object_exprt(expr.arguments()[0]); + is_dynamic_object_expr.add_source_location() = source_location; - return dynamic_object_expr; + return is_dynamic_object_expr; } else if(identifier==CPROVER_PREFIX "POINTER_OFFSET") { diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 80b5515dd0f..e5318b5e730 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -3580,8 +3580,8 @@ std::string expr2ct::convert_with_precedence( else if(src.id()==ID_invalid_pointer) return convert_function(src, "__CPROVER_invalid_pointer", precedence=16); - else if(src.id()==ID_dynamic_object) - return convert_function(src, "DYNAMIC_OBJECT", precedence=16); + else if(src.id()==ID_is_dynamic_object) + return convert_function(src, "IS_DYNAMIC_OBJECT", precedence=16); else if(src.id()=="is_zero_string") return convert_function(src, "IS_ZERO_STRING", precedence=16); diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 7a8412afcce..3409fbb8c12 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -13,17 +13,26 @@ Date: February 2016 #include "code_contracts.h" +#include +#include +#include #include +#include #include +#include #include -#include +#include #include +#include + #include "loop_utils.h" +enum class contract_opst { APPLY, CHECK }; + class code_contractst { public: @@ -32,77 +41,252 @@ class code_contractst goto_functionst &_goto_functions): ns(_symbol_table), symbol_table(_symbol_table), - goto_functions(_goto_functions), - temporary_counter(0) + goto_functions(_goto_functions) { } - void operator()(); + void operator()(contract_opst op_type); protected: namespacet ns; symbol_tablet &symbol_table; goto_functionst &goto_functions; - unsigned temporary_counter; - - std::unordered_set summarized; + void apply_code_contracts(); + void check_code_contracts(); void code_contracts(goto_functionst::goto_functiont &goto_function); + /// Applies (but does not check) a function contract. + /// This will assume that the contract holds, and then use that assumption + /// to remove the function call located at target. + /// \param goto_program The goto program containing the target callsite. + /// \param value_sets A value_setst object containing information about + /// aliasing in the goto program being analyzed + /// \param target An iterator pointing to the function call to be removed. void apply_contract( goto_programt &goto_program, + value_setst &value_sets, goto_programt::targett target); - void add_contract_check( - const irep_idt &function, + /// Applies (but does not check) a loop invariant. + /// This will assume that the loop invariant is indeed an invariant, and then + /// use that assumption to remove the loop. + /// \param goto_function The goto function containing the target loop. + /// \param value_sets A value_setst object containing information about + /// aliasing in the goto program being analyzed + /// \param loop_head An iterator pointing to the first instruction of the + /// target loop. + /// \param loop The loop being removed. + void apply_invariant( + goto_functionst::goto_functiont &goto_function, + value_setst &value_sets, + const goto_programt::targett loop_head, + const loopt &loop); + + /// Checks (but does not apply) a function contract. + /// This will build a code snippet to be inserted at dest which will check + // that the function contract is satisfied. + /// \param function_id The id of the function being checked. + /// \param goto_function The goto_function object for the function + /// being checked. + /// \param dest An iterator pointing to the place to insert checking code. + void check_contract( + const irep_idt &function_id, + goto_functionst::goto_functiont &goto_function, goto_programt &dest); + /// Checks and applies a loop invariant + /// This will replace the loop with a code snippet (based on the loop) which + /// will check that the loop invariant is indeed ian invariant, and then + /// use that invariant in what follows. + /// \param goto_function The goto function containing the target loop. + /// \param value_sets A value_setst object containing information about + /// aliasing in the goto program being analyzed + /// \param loop_head An iterator pointing to the first instruction of the + /// target loop. + /// \param loop The loop being removed. + void check_apply_invariant( + goto_functionst::goto_functiont &goto_function, + value_setst &value_sets, + const goto_programt::targett loop_head, + const loopt &loop); + const symbolt &new_tmp_symbol( const typet &type, const source_locationt &source_location); }; -static void check_apply_invariants( +void code_contractst::apply_contract( + goto_programt &goto_program, + value_setst &value_sets, + goto_programt::targett target) +{ + const code_function_callt &call=to_code_function_call(target->code); + // we don't handle function pointers. remove_function_pointers should have + // been invoked by this point. + PRECONDITION(call.function().id() == ID_symbol); + + const irep_idt &function= + to_symbol_expr(call.function()).get_identifier(); + const symbolt &f_sym=ns.lookup(function); + const code_typet &type=to_code_type(f_sym.type); + + exprt requires = + static_cast(type.find(ID_C_spec_requires)); + exprt ensures = + static_cast(type.find(ID_C_spec_ensures)); + + if(ensures.is_nil()) + { + // If there is no contract at all, we skip this function. + if(requires.is_nil()) + { + return; + } + else + { + // If there's no ensures but is a requires, treat it as ensures(true) + ensures = true_exprt(); + } + } + + // find out what can be written by the function + modifiest modifies; + + rw_range_set_value_sett rw_set(ns, value_sets); + goto_rw(goto_functions, function, rw_set); + forall_rw_range_set_w_objects(it, rw_set) + { + // Skip over local variables of the function being called, as well as + // variables not in the namespace (e.g. symex::invalid_object) + const symbolt *symbol_ptr; + if(!ns.lookup(it->first, symbol_ptr)) + { + const std::string &name_string = id2string(symbol_ptr->name); + std::string scope_prefix(id2string(ns.lookup(function).name)); + scope_prefix += "::"; + + if(name_string.find(scope_prefix) == std::string::npos) + { + modifies.insert(ns.lookup(it->first).symbol_expr()); + } + } + } + + // build the havocking code + goto_programt havoc_code; + build_havoc_code(target, modifies, havoc_code); + + // replace formal parameters by arguments, replace return + replace_symbolt replace; + + const irep_idt symbol_name = id2string(function) + RETURN_VALUE_SUFFIX; + const symbolt *existing_symbol = symbol_table.lookup(symbol_name); + // TODO: return value could be nil + if(existing_symbol != nullptr) + { + replace.insert("__CPROVER_return_value", existing_symbol->symbol_expr()); + } + + // formal parameters + code_function_callt::argumentst::const_iterator a_it= + call.arguments().begin(); + for(code_typet::parameterst::const_iterator + p_it=type.parameters().begin(); + p_it!=type.parameters().end() && + a_it!=call.arguments().end(); + ++p_it, ++a_it) + if(!p_it->get_identifier().empty()) + replace.insert(p_it->get_identifier(), *a_it); + + replace(requires); + replace(ensures); + + // Havoc the return value of the function call. + if(type.return_type()!=empty_typet()) + { + const exprt &lhs = call.lhs(); + const exprt &rhs = side_effect_expr_nondett(call.lhs().type()); + target->make_assignment(code_assignt(lhs, rhs)); + } + else + { + target->make_skip(); + } + + if(requires.is_not_nil()) + { + goto_programt::instructiont a(ASSERT); + a.guard=requires; + a.function=target->function; + a.source_location=target->source_location; + + goto_program.insert_before_swap(target, a); + ++target; + } + + goto_program.destructive_insert(target, havoc_code); + + { + goto_programt::targett a=goto_program.insert_after(target); + a->make_assumption(ensures); + a->function=target->function; + a->source_location=target->source_location; + } +} + +void code_contractst::apply_invariant( goto_functionst::goto_functiont &goto_function, - const local_may_aliast &local_may_alias, + value_setst &value_sets, const goto_programt::targett loop_head, const loopt &loop) { - assert(!loop.empty()); + PRECONDITION(!loop.empty()); // find the last back edge goto_programt::targett loop_end=loop_head; - for(loopt::const_iterator - it=loop.begin(); - it!=loop.end(); - ++it) - if((*it)->is_goto() && - (*it)->get_target()==loop_head && - (*it)->location_number>loop_end->location_number) - loop_end=*it; + for(const goto_programt::targett &inst : loop) + { + if(inst->is_goto() && + inst->get_target()==loop_head && + inst->location_number>loop_end->location_number) + { + loop_end=inst; + } + } - // see whether we have an invariant - exprt invariant= - static_cast( - loop_end->guard.find(ID_C_spec_loop_invariant)); + exprt invariant = static_cast( + loop_end->guard.find(ID_C_spec_loop_invariant)); if(invariant.is_nil()) + { return; + } // change H: loop; E: ... // to // H: assert(invariant); // havoc; // assume(invariant); - // if(guard) goto E: - // loop; - // assert(invariant); - // assume(false); + // assume(!guard); // E: ... // find out what can get changed in the loop modifiest modifies; - get_modifies(local_may_alias, loop, modifies); + + rw_range_set_value_sett rw_set(ns, value_sets); + for(const goto_programt::targett &inst : loop) + { + goto_rw(inst, rw_set); + } + forall_rw_range_set_w_objects(it, rw_set) + { + const symbolt *symbol_ptr; + if(!ns.lookup(it->first, symbol_ptr)) + { + modifies.insert(ns.lookup(it->first).symbol_expr()); + } + } // build the havocking code goto_programt havoc_code; @@ -127,163 +311,62 @@ static void check_apply_invariants( assume->source_location=loop_head->source_location; } - // non-deterministically skip the loop if it is a do-while loop - if(!loop_head->is_goto()) + // assume !guard { - goto_programt::targett jump=havoc_code.add_instruction(GOTO); - jump->guard = - side_effect_expr_nondett(bool_typet(), loop_head->source_location); - jump->targets.push_back(loop_end); - jump->function=loop_head->function; + goto_programt::targett assume = havoc_code.add_instruction(ASSUME); + if(loop_head->is_goto()) + { + assume->guard = loop_head->guard; + } + else + { + assume->guard = loop_end->guard; + assume->guard.make_not(); + } + assume->function = loop_head->function; + assume->source_location = loop_head->source_location; } - // Now havoc at the loop head. Use insert_swap to - // preserve jumps to loop head. - goto_function.body.insert_before_swap(loop_head, havoc_code); - - // assert the invariant at the end of the loop body + // Clear out loop body + for(const goto_programt::targett &inst : loop) { - goto_programt::instructiont a(ASSERT); - a.guard=invariant; - a.function=loop_end->function; - a.source_location=loop_end->source_location; - a.source_location.set_comment("Loop invariant not preserved"); - goto_function.body.insert_before_swap(loop_end, a); - ++loop_end; + inst->make_skip(); } - // change the back edge into assume(false) or assume(guard) - loop_end->targets.clear(); - loop_end->type=ASSUME; - if(loop_head->is_goto()) - loop_end->guard.make_false(); - else - loop_end->guard.make_not(); + // Now havoc at the loop head. Use insert_before_swap to + // preserve jumps to loop head. + goto_function.body.insert_before_swap(loop_head, havoc_code); + + // Remove all the skips we created. + remove_skip(goto_function.body); } -void code_contractst::apply_contract( - goto_programt &goto_program, - goto_programt::targett target) +void code_contractst::check_contract( + const irep_idt &function_id, + goto_functionst::goto_functiont &goto_function, + goto_programt &dest) { - const code_function_callt &call=to_code_function_call(target->code); - // we don't handle function pointers - if(call.function().id()!=ID_symbol) - return; + PRECONDITION(!dest.instructions.empty()); - const irep_idt &function= - to_symbol_expr(call.function()).get_identifier(); - const symbolt &f_sym=ns.lookup(function); - const code_typet &type=to_code_type(f_sym.type); + exprt requires = + static_cast(goto_function.type.find(ID_C_spec_requires)); + exprt ensures = + static_cast(goto_function.type.find(ID_C_spec_ensures)); - exprt requires= - static_cast(type.find(ID_C_spec_requires)); - exprt ensures= - static_cast(type.find(ID_C_spec_ensures)); - - // is there a contract? + // Nothing to check if ensures is nil. if(ensures.is_nil()) - return; - - // replace formal parameters by arguments, replace return - replace_symbolt replace; - - // TODO: return value could be nil - if(type.return_type()!=empty_typet()) - replace.insert("__CPROVER_return_value", call.lhs()); - - // formal parameters - code_function_callt::argumentst::const_iterator a_it= - call.arguments().begin(); - for(code_typet::parameterst::const_iterator - p_it=type.parameters().begin(); - p_it!=type.parameters().end() && - a_it!=call.arguments().end(); - ++p_it, ++a_it) - if(!p_it->get_identifier().empty()) - replace.insert(p_it->get_identifier(), *a_it); - - replace(requires); - replace(ensures); - - if(requires.is_not_nil()) { - goto_programt::instructiont a(ASSERT); - a.guard=requires; - a.function=target->function; - a.source_location=target->source_location; - - goto_program.insert_before_swap(target, a); - ++target; + return; } - target->make_assumption(ensures); - - summarized.insert(function); -} - -void code_contractst::code_contracts( - goto_functionst::goto_functiont &goto_function) -{ - local_may_aliast local_may_alias(goto_function); - natural_loops_mutablet natural_loops(goto_function.body); - - // iterate over the (natural) loops in the function - for(natural_loops_mutablet::loop_mapt::const_iterator - l_it=natural_loops.loop_map.begin(); - l_it!=natural_loops.loop_map.end(); - l_it++) - check_apply_invariants( - goto_function, - local_may_alias, - l_it->first, - l_it->second); - - // look at all function calls - Forall_goto_program_instructions(it, goto_function.body) - if(it->is_function_call()) - apply_contract(goto_function.body, it); -} - -const symbolt &code_contractst::new_tmp_symbol( - const typet &type, - const source_locationt &source_location) -{ - return get_fresh_aux_symbol( - type, - id2string(source_location.get_function()), - "tmp_cc", - source_location, - irep_idt(), - symbol_table); -} - -void code_contractst::add_contract_check( - const irep_idt &function, - goto_programt &dest) -{ - assert(!dest.instructions.empty()); - - goto_functionst::function_mapt::iterator f_it= - goto_functions.function_map.find(function); - assert(f_it!=goto_functions.function_map.end()); - - const goto_functionst::goto_functiont &gf=f_it->second; - - const exprt &requires= - static_cast(gf.type.find(ID_C_spec_requires)); - const exprt &ensures= - static_cast(gf.type.find(ID_C_spec_ensures)); - assert(ensures.is_not_nil()); - - // build: - // if(nondet) - // decl ret + // We build the following checking code: + // if(nondet) goto end // decl parameter1 ... // assume(requires) [optional] - // ret=function(parameter1, ...) + // function(parameter1, ...) // assert(ensures) - // assume(false) - // skip: ... + // end: + // skip // build skip so that if(nondet) can refer to it goto_programt tmp_skip; @@ -295,54 +378,44 @@ void code_contractst::add_contract_check( // if(nondet) goto_programt::targett g=check.add_instruction(); - g->make_goto( - skip, side_effect_expr_nondett(bool_typet(), skip->source_location)); + g->make_goto(skip, side_effect_expr_nondett(bool_typet())); g->function=skip->function; g->source_location=skip->source_location; // prepare function call including all declarations code_function_callt call; - call.function()=ns.lookup(function).symbol_expr(); + call.function()=ns.lookup(function_id).symbol_expr(); replace_symbolt replace; - // decl ret - if(gf.type.return_type()!=empty_typet()) + const irep_idt symbol_name = id2string(function_id) + RETURN_VALUE_SUFFIX; + const symbolt *existing_symbol = symbol_table.lookup(symbol_name); + // TODO: Handle void functions + if(existing_symbol != nullptr) { - goto_programt::targett d=check.add_instruction(DECL); - d->function=skip->function; - d->source_location=skip->source_location; - - symbol_exprt r= - new_tmp_symbol(gf.type.return_type(), - d->source_location).symbol_expr(); - d->code=code_declt(r); - - call.lhs()=r; - - replace.insert("__CPROVER_return_value", r); + replace.insert("__CPROVER_return_value", existing_symbol->symbol_expr()); } // decl parameter1 ... - for(code_typet::parameterst::const_iterator - p_it=gf.type.parameters().begin(); - p_it!=gf.type.parameters().end(); - ++p_it) + for(const auto &p_it : goto_function.type.parameters()) { goto_programt::targett d=check.add_instruction(DECL); d->function=skip->function; d->source_location=skip->source_location; symbol_exprt p= - new_tmp_symbol(p_it->type(), - d->source_location).symbol_expr(); + new_tmp_symbol(p_it.type(), d->source_location).symbol_expr(); d->code=code_declt(p); call.arguments().push_back(p); - if(!p_it->get_identifier().empty()) - replace.insert(p_it->get_identifier(), p); + if(!p_it.get_identifier().empty()) + replace.insert(p_it.get_identifier(), p); } + // rewrite any use of parameters + replace(requires); + replace(ensures); + // assume(requires) if(requires.is_not_nil()) { @@ -350,9 +423,6 @@ void code_contractst::add_contract_check( a->make_assumption(requires); a->function=skip->function; a->source_location=requires.source_location(); - - // rewrite any use of parameters - replace(a->guard); } // ret=function(parameter1, ...) @@ -367,39 +437,267 @@ void code_contractst::add_contract_check( a->function=skip->function; a->source_location=ensures.source_location(); - // rewrite any use of __CPROVER_return_value - replace(a->guard); - - // assume(false) - goto_programt::targett af=check.add_instruction(); - af->make_assumption(false_exprt()); - af->function=skip->function; - af->source_location=ensures.source_location(); - // prepend the new code to dest check.destructive_append(tmp_skip); dest.destructive_insert(dest.instructions.begin(), check); } -void code_contractst::operator()() +void code_contractst::check_apply_invariant( + goto_functionst::goto_functiont &goto_function, + value_setst &value_sets, + const goto_programt::targett loop_head, + const loopt &loop) { + PRECONDITION(!loop.empty()); + + // find the last back edge + goto_programt::targett loop_end=loop_head; + for(const goto_programt::targett &inst : loop) + if(inst->is_goto() && + inst->get_target()==loop_head && + inst->location_number>loop_end->location_number) + loop_end=inst; + + // see whether we have an invariant + exprt invariant= + static_cast( + loop_end->guard.find(ID_C_spec_loop_invariant)); + if(invariant.is_nil()) + { + return; + } + + // change H: loop; E: ... + // to + // H: assert(invariant); + // havoc writes of loop; + // assume(invariant); + // loop (minus the ending goto); + // assert(invariant); + // assume(!guard) + // E: + // ... + + // find out what can get changed in the loop + modifiest modifies; + + rw_range_set_value_sett rw_set(ns, value_sets); + for(const goto_programt::targett &inst : loop) + { + goto_rw(inst, rw_set); + } + forall_rw_range_set_w_objects(it, rw_set) + { + const symbolt *symbol_ptr; + if(!ns.lookup(it->first, symbol_ptr)) + { + modifies.insert(ns.lookup(it->first).symbol_expr()); + } + } + + // build the havocking code + goto_programt havoc_code; + + // assert the invariant + { + goto_programt::targett a=havoc_code.add_instruction(ASSERT); + a->guard=invariant; + a->function=loop_head->function; + a->source_location=loop_head->source_location; + a->source_location.set_comment("Loop invariant violated before entry"); + } + + // havoc variables that can be modified by the loop + build_havoc_code(loop_head, modifies, havoc_code); + + // assume the invariant + { + goto_programt::targett assume=havoc_code.add_instruction(ASSUME); + assume->guard=invariant; + assume->function=loop_head->function; + assume->source_location=loop_head->source_location; + } + + // assert the invariant at the end of the loop body + { + goto_programt::instructiont a(ASSERT); + a.guard=invariant; + a.function=loop_end->function; + a.source_location=loop_end->source_location; + a.source_location.set_comment("Loop invariant not preserved"); + + goto_function.body.insert_before_swap(loop_end, a); + ++loop_end; + } + + // change the back edge into assume(!guard) + loop_end->targets.clear(); + loop_end->type=ASSUME; + if(loop_head->is_goto()) + { + loop_end->guard = loop_head->guard; + } + else + { + loop_end->guard.make_not(); + } + + // Now havoc at the loop head. Use insert_before_swap to + // preserve jumps to loop head. + goto_function.body.insert_before_swap(loop_head, havoc_code); +} + +const symbolt &code_contractst::new_tmp_symbol( + const typet &type, + const source_locationt &source_location) +{ + return get_fresh_aux_symbol( + type, + id2string(source_location.get_function()), + "tmp_cc", + source_location, + ID_C, + symbol_table); +} + +{ + auto vs = util_make_unique(ns); + (*vs)(goto_functions); + std::unique_ptr value_sets = std::move(vs); + Forall_goto_functions(it, goto_functions) - code_contracts(it->second); + { + goto_functionst::goto_functiont &goto_function = it->second; + + natural_loops_mutablet natural_loops(goto_function.body); + + for(const auto &l_it : natural_loops.loop_map) + { + apply_invariant(goto_function, + *value_sets, + l_it.first, + l_it.second); + } + + Forall_goto_program_instructions(it, goto_function.body) + { + if(it->is_function_call()) + { + apply_contract(goto_function.body, *value_sets, it); + } + } + } + + goto_functions.update(); +} + +void code_contractst::check_code_contracts() +{ + auto vs = util_make_unique(ns); + (*vs)(goto_functions); + std::unique_ptr value_sets = std::move(vs); goto_functionst::function_mapt::iterator i_it= goto_functions.function_map.find(INITIALIZE_FUNCTION); - assert(i_it!=goto_functions.function_map.end()); + CHECK_RETURN(i_it!=goto_functions.function_map.end()); + goto_programt &init_function = i_it->second.body; - for(const auto &contract : summarized) - add_contract_check(contract, i_it->second.body); + Forall_goto_functions(it, goto_functions) + { + goto_functionst::goto_functiont &goto_function = it->second; + + natural_loops_mutablet natural_loops(goto_function.body); + + for(const auto &l_it : natural_loops.loop_map) + { + check_apply_invariant(goto_function, + *value_sets, + l_it.first, + l_it.second); + } + + Forall_goto_program_instructions(it, goto_function.body) + { + if(it->is_function_call()) + { + apply_contract(goto_function.body, *value_sets, it); + } + } + } - // remove skips - remove_skip(i_it->second.body); + Forall_goto_functions(it, goto_functions) + { + check_contract(it->first, it->second, init_function); + } + + // Partially initialize state + goto_programt init_code; + + goto_programt::targett d = init_code.add_instruction(DECL); + d->function = i_it->first; + // TODO add source location + // d->source_location = + + symbol_exprt tmp_var = + new_tmp_symbol(void_typet(), d->source_location).symbol_expr(); + d->code = code_declt(tmp_var); + d->code.add_source_location() = d->source_location; + + { + const symbol_exprt &deallocated_expr = + ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr(); + + goto_programt::targett a = init_code.add_instruction(ASSIGN); + a->function = i_it->first; + // TODO add source location + // a->source_location = + address_of_exprt rhs(tmp_var, to_pointer_type(deallocated_expr.type())); + a->code = code_assignt(deallocated_expr, rhs); + a->code.add_source_location() = a->source_location; + } + + { + const symbol_exprt &dead_expr = + ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr(); + + goto_programt::targett a = init_code.add_instruction(ASSIGN); + a->function = i_it->first; + // TODO add source location + // a->source_location = + address_of_exprt rhs(tmp_var, to_pointer_type(dead_expr.type())); + a->code = code_assignt(dead_expr, rhs); + a->code.add_source_location() = a->source_location; + } + + init_function.destructive_insert(init_function.instructions.begin(), + init_code); + + remove_skip(init_function); goto_functions.update(); } -void code_contracts(goto_modelt &goto_model) +void code_contractst::operator()(contract_opst op_type) +{ + switch(op_type) + { + case contract_opst::APPLY: + apply_code_contracts(); + break; + case contract_opst::CHECK: + check_code_contracts(); + break; + } +} + +void check_code_contracts(goto_modelt &goto_model) +{ + code_contractst(goto_model.symbol_table, goto_model.goto_functions) + (contract_opst::CHECK); +} + +void apply_code_contracts(goto_modelt &goto_model) { - code_contractst(goto_model.symbol_table, goto_model.goto_functions)(); + code_contractst(goto_model.symbol_table, goto_model.goto_functions) + (contract_opst::APPLY); } diff --git a/src/goto-instrument/code_contracts.h b/src/goto-instrument/code_contracts.h index dc02902c142..87395007fff 100644 --- a/src/goto-instrument/code_contracts.h +++ b/src/goto-instrument/code_contracts.h @@ -16,6 +16,19 @@ Date: February 2016 class goto_modelt; -void code_contracts(goto_modelt &); +void apply_code_contracts(goto_modelt &); +void check_code_contracts(goto_modelt &); + +// clang-format off +#define HELP_APPLY_CODE_CONTRACTS \ + " --apply-code-contracts Assume (without checking) that the contracts used in code hold\n" \ + " This will use __CPROVER_requires, __CPROVER_ensures,\n" \ + " and __CPROVER_loop_invariant as assumptions in order to avoid\n" \ + " checking code that is assumed to satisfy a specification.\n" +#define HELP_CHECK_CODE_CONTRACTS \ + " --check-code-contracts Assume (with checking) that the contracts used in code hold.\n" \ + " This differs from --apply-code-contracts in that in addition to\n" \ + " assuming specifications, it checks that they are correct.\n" +// clang-format on #endif // CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 4582509df7d..5d7a7a9b885 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1046,13 +1046,6 @@ void goto_instrument_parse_optionst::instrument_goto_program() goto_model.goto_functions.update(); } - // verify and set invariants and pre/post-condition pairs - if(cmdline.isset("apply-code-contracts")) - { - status() << "Applying Code Contracts" << eom; - code_contracts(goto_model); - } - // replace function pointers, if explicitly requested if(cmdline.isset("remove-function-pointers")) { @@ -1063,6 +1056,32 @@ void goto_instrument_parse_optionst::instrument_goto_program() do_remove_const_function_pointers_only(); } + // Use invariants and pre/post-condition pairs without checking them. + if(cmdline.isset("apply-code-contracts")) + { + // Code contracts depends on these other passes. + remove_function_pointers( + get_message_handler(), + goto_model, + cmdline.isset("pointer-check")); + do_remove_returns(); + status() << "Applying Code Contracts" << eom; + apply_code_contracts(goto_model); + } + + // Uses invariants and pre/post-condition pairs and verifies that they hold. + if(cmdline.isset("check-code-contracts")) + { + // Code contracts depends on these other passes. + remove_function_pointers( + get_message_handler(), + goto_model, + cmdline.isset("pointer-check")); + do_remove_returns(); + status() << "Checking Code Contracts" << eom; + check_code_contracts(goto_model); + } + if(cmdline.isset("function-inline")) { std::string function=cmdline.get_value("function-inline"); @@ -1574,6 +1593,8 @@ void goto_instrument_parse_optionst::help() " --undefined-function-is-assume-false\n" // NOLINTNEXTLINE(whitespace/line_length) " convert each call to an undefined function to assume(false)\n" + HELP_APPLY_CODE_CONTRACTS + HELP_CHECK_CODE_CONTRACTS HELP_REPLACE_FUNCTION_BODY "\n" "Loop transformations:\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 706083df63e..d8286c53c74 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -87,8 +87,8 @@ Author: Daniel Kroening, kroening@kroening.com "(interpreter)(show-reaching-definitions)" \ "(list-symbols)(list-undefined-functions)" \ "(z3)(add-library)(show-dependence-graph)" \ - "(horn)(skip-loops):(apply-code-contracts)(model-argc-argv):" \ - "(show-threaded)(list-calls-args)" \ + "(horn)(skip-loops):(apply-code-contracts)(check-code-contracts)" \ + "(model-argc-argv):(show-threaded)(list-calls-args)" \ "(undefined-function-is-assume-false)" \ "(remove-function-body):"\ OPT_AGGRESSIVE_SLICER \ diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index b22ced28326..4b4ee52609e 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -358,8 +358,12 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( // this is also our guard result.pointer_guard = dynamic_object(pointer_expr); - // can't remove here, turn into *p - result.value=dereference_exprt(pointer_expr, dereference_type); + // TODO should this be object or root_object? + // TODO It's unclear whether this is a good approach to take --- it + // successfully ensures that every (non-null) dereference points to + // something, making the write set computation work correctly, but dynamic + // objects do not seem to be intended to be used in this way. + result.value = object; if(options.get_bool_option("pointer-check")) { diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index 5cf7ade92c8..5a69827092c 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -45,21 +45,21 @@ literalt bv_pointerst::convert_rest(const exprt &expr) } } } - else if(expr.id()==ID_dynamic_object) + else if(expr.id()==ID_is_dynamic_object) { - if(operands.size()==1 && - operands[0].type().id()==ID_pointer) - { - // we postpone - literalt l=prop.new_variable(); + DATA_INVARIANT(operands.size() == 1 && + operands[0].type().id() == ID_pointer, + std::string("is_dynamic_object_exprt should have one") + + "operand, which should have pointer type."); + // we postpone + literalt l=prop.new_variable(); - postponed_list.push_back(postponedt()); - postponed_list.back().op=convert_bv(operands[0]); - postponed_list.back().bv.push_back(l); - postponed_list.back().expr=expr; + postponed_list.push_back(postponedt()); + postponed_list.back().op=convert_bv(operands[0]); + postponed_list.back().bv.push_back(l); + postponed_list.back().expr=expr; - return l; - } + return l; } else if(expr.id()==ID_lt || expr.id()==ID_le || expr.id()==ID_gt || expr.id()==ID_ge) @@ -735,7 +735,7 @@ void bv_pointerst::add_addr(const exprt &expr, bvt &bv) void bv_pointerst::do_postponed( const postponedt &postponed) { - if(postponed.expr.id()==ID_dynamic_object) + if(postponed.expr.id()==ID_is_dynamic_object) { const pointer_logict::objectst &objects= pointer_logic.objects; diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index c1b14961d76..95493bce85e 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -1367,7 +1367,7 @@ void smt2_convt::convert_expr(const exprt &expr) if(ext>0) out << ")"; // zero_extend } - else if(expr.id()==ID_dynamic_object) + else if(expr.id()==ID_is_dynamic_object) { convert_is_dynamic_object(expr); } diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index d0066054482..95f7bb6db77 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -448,6 +448,7 @@ IREP_ID_TWO(overflow_minus, overflow--) IREP_ID_TWO(overflow_mult, overflow-*) IREP_ID_TWO(overflow_unary_minus, overflow-unary-) IREP_ID_ONE(object_descriptor) +IREP_ID_ONE(is_dynamic_object) IREP_ID_ONE(dynamic_object) IREP_ID_TWO(C_dynamic, #dynamic) IREP_ID_ONE(object_size) diff --git a/src/util/pointer_predicates.cpp b/src/util/pointer_predicates.cpp index 668054bc493..0185d222e54 100644 --- a/src/util/pointer_predicates.cpp +++ b/src/util/pointer_predicates.cpp @@ -70,7 +70,7 @@ exprt dynamic_size(const namespacet &ns) exprt dynamic_object(const exprt &pointer) { - exprt dynamic_expr(ID_dynamic_object, bool_typet()); + exprt dynamic_expr(ID_is_dynamic_object, bool_typet()); dynamic_expr.copy_to_operands(pointer); return dynamic_expr; } diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index f7e442e40ef..23e19a4c239 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2266,8 +2266,8 @@ bool simplify_exprt::simplify_node(exprt &expr) result=simplify_byte_extract(to_byte_extract_expr(expr)) && result; else if(expr.id()==ID_pointer_object) result=simplify_pointer_object(expr) && result; - else if(expr.id()==ID_dynamic_object) - result=simplify_dynamic_object(expr) && result; + else if(expr.id()==ID_is_dynamic_object) + result=simplify_is_dynamic_object(expr) && result; else if(expr.id()==ID_invalid_pointer) result=simplify_invalid_pointer(expr) && result; else if(expr.id()==ID_object_size) diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index 5e192292666..3dd7d8601e1 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -96,7 +96,7 @@ class simplify_exprt bool simplify_pointer_object(exprt &expr); bool simplify_object_size(exprt &expr); bool simplify_dynamic_size(exprt &expr); - bool simplify_dynamic_object(exprt &expr); + bool simplify_is_dynamic_object(exprt &expr); bool simplify_invalid_pointer(exprt &expr); bool simplify_same_object(exprt &expr); bool simplify_good_pointer(exprt &expr); diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 6856c6a38fc..9c6c12635ab 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -1699,7 +1699,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr) expr.op0().operands().size()==1) { if(expr.op0().op0().id()==ID_symbol || - expr.op0().op0().id()==ID_dynamic_object || + expr.op0().op0().id()==ID_is_dynamic_object || expr.op0().op0().id()==ID_member || expr.op0().op0().id()==ID_index || expr.op0().op0().id()==ID_string_constant) @@ -1715,7 +1715,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr) expr.op0().op0().operands().size()==1) { if(expr.op0().op0().op0().id()==ID_symbol || - expr.op0().op0().op0().id()==ID_dynamic_object || + expr.op0().op0().op0().id()==ID_is_dynamic_object || expr.op0().op0().op0().id()==ID_member || expr.op0().op0().op0().id()==ID_index || expr.op0().op0().op0().id()==ID_string_constant) diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index b183c81890b..82764d52b10 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -464,7 +464,7 @@ bool simplify_exprt::simplify_inequality_pointer_object(exprt &expr) { if(op.operands().size()!=1 || (op.op0().id()!=ID_symbol && - op.op0().id()!=ID_dynamic_object && + op.op0().id()!=ID_is_dynamic_object && op.op0().id()!=ID_string_constant)) return true; } @@ -508,18 +508,20 @@ bool simplify_exprt::simplify_pointer_object(exprt &expr) return result; } -bool simplify_exprt::simplify_dynamic_object(exprt &expr) +bool simplify_exprt::simplify_is_dynamic_object(exprt &expr) { - if(expr.operands().size()!=1) - return true; + DATA_INVARIANT(expr.operands().size() == 1 && + expr.op0().type().id() == ID_pointer, + std::string("is_dynamic_object_exprt should have one") + + "operand, which should have pointer type."); exprt &op=expr.op0(); if(op.id()==ID_if && op.operands().size()==3) { if_exprt if_expr=lift_if(expr, 0); - simplify_dynamic_object(if_expr.true_case()); - simplify_dynamic_object(if_expr.false_case()); + simplify_is_dynamic_object(if_expr.true_case()); + simplify_is_dynamic_object(if_expr.false_case()); simplify_if(if_expr); expr.swap(if_expr); diff --git a/src/util/std_expr.h b/src/util/std_expr.h index e979f45ee69..bf44ed8451a 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -2106,6 +2106,54 @@ inline void validate_expr(const dynamic_object_exprt &value) } +/*! \brief Evaluates to true if the operand is a pointer to a dynamic object. +*/ +class is_dynamic_object_exprt:public unary_predicate_exprt +{ +public: + is_dynamic_object_exprt():unary_predicate_exprt(ID_is_dynamic_object) + { + } + + explicit is_dynamic_object_exprt(const exprt &op): + unary_predicate_exprt(ID_is_dynamic_object, op) + { + } +}; + +/*! \brief Cast a generic exprt to a \ref is_dynamic_object_exprt + * + * This is an unchecked conversion. \a expr must be known to be \ref + * is_dynamic_object_exprt. + * + * \param expr Source expression + * \return Object of type \ref is_dynamic_object_exprt + * + * \ingroup gr_std_expr +*/ +inline const is_dynamic_object_exprt &to_is_dynamic_object_expr( + const exprt &expr) +{ + PRECONDITION(expr.id()==ID_is_dynamic_object); + DATA_INVARIANT( + expr.operands().size()==1, + "is_dynamic_object must have one operand"); + return static_cast(expr); +} + +/*! \copydoc to_is_dynamic_object_expr(const exprt &) + * \ingroup gr_std_expr +*/ +inline is_dynamic_object_exprt &to_is_dynamic_object_expr(exprt &expr) +{ + PRECONDITION(expr.id()==ID_is_dynamic_object); + DATA_INVARIANT( + expr.operands().size()==1, + "is_dynamic_object must have one operand"); + return static_cast(expr); +} + + /*! \brief semantic type conversion */ class typecast_exprt:public unary_exprt