From bb64ea679d67a392ef9ab0e1f512682421a3ad14 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 13 Feb 2018 18:11:05 +0000 Subject: [PATCH 1/2] clean up symex_assign vs. symex_assign_rec --- src/goto-symex/auto_objects.cpp | 2 +- src/goto-symex/goto_symex.h | 3 +-- src/goto-symex/symex_assign.cpp | 16 ++-------------- src/goto-symex/symex_builtin_functions.cpp | 10 +++++----- src/goto-symex/symex_function_call.cpp | 8 ++++---- src/goto-symex/symex_main.cpp | 2 +- 6 files changed, 14 insertions(+), 27 deletions(-) diff --git a/src/goto-symex/auto_objects.cpp b/src/goto-symex/auto_objects.cpp index 2338b102593..b41a3e01c74 100644 --- a/src/goto-symex/auto_objects.cpp +++ b/src/goto-symex/auto_objects.cpp @@ -76,7 +76,7 @@ void goto_symext::initialize_auto_object( address_of_expr); code_assignt assignment(expr, rhs); - symex_assign_rec(state, assignment); + symex_assign(state, assignment); } } } diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index ded5082fe1c..4af4e55d51b 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -305,8 +305,7 @@ class goto_symext virtual void do_simplify(exprt &expr); // virtual void symex_block(statet &state, const codet &code); - void symex_assign_rec(statet &state, const code_assignt &code); - virtual void symex_assign(statet &state, const code_assignt &code); + void symex_assign(statet &state, const code_assignt &code); // havocs the given object void havoc_rec(statet &, const guardt &, const exprt &); diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index 8369ef5db2f..036b1644ee6 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -20,18 +20,6 @@ Author: Daniel Kroening, kroening@kroening.com // #define USE_UPDATE -void goto_symext::symex_assign_rec( - statet &state, - const code_assignt &code) -{ - code_assignt deref_code=code; - - clean_expr(deref_code.lhs(), state, true); - clean_expr(deref_code.rhs(), state, false); - - symex_assign(state, deref_code); -} - void goto_symext::symex_assign( statet &state, const code_assignt &code) @@ -39,8 +27,8 @@ void goto_symext::symex_assign( exprt lhs=code.lhs(); exprt rhs=code.rhs(); - replace_nondet(lhs); - replace_nondet(rhs); + clean_expr(lhs, state, true); + clean_expr(rhs, state, false); if(rhs.id()==ID_side_effect) { diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index 9bf02bf1e2e..cbf9f822d1c 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -151,7 +151,7 @@ void goto_symext::symex_allocate( code_assignt assignment(size_symbol.symbol_expr(), size); size=assignment.lhs(); - symex_assign_rec(state, assignment); + symex_assign(state, assignment); } } @@ -187,7 +187,7 @@ void goto_symext::symex_allocate( if(zero_value.is_not_nil()) { code_assignt assignment(value_symbol.symbol_expr(), zero_value); - symex_assign_rec(state, assignment); + symex_assign(state, assignment); } else throw "failed to zero initialize dynamic object"; @@ -212,7 +212,7 @@ void goto_symext::symex_allocate( if(rhs.type()!=lhs.type()) rhs.make_typecast(lhs.type()); - symex_assign_rec(state, code_assignt(lhs, rhs)); + symex_assign(state, code_assignt(lhs, rhs)); } irep_idt get_symbol(const exprt &src) @@ -276,7 +276,7 @@ void goto_symext::symex_gcc_builtin_va_arg_next( } } - symex_assign_rec(state, code_assignt(lhs, rhs)); + symex_assign(state, code_assignt(lhs, rhs)); } irep_idt get_string_argument_rec(const exprt &src) @@ -458,7 +458,7 @@ void goto_symext::symex_cpp_new( else rhs.copy_to_operands(symbol.symbol_expr()); - symex_assign_rec(state, code_assignt(lhs, rhs)); + symex_assign(state, code_assignt(lhs, rhs)); } void goto_symext::symex_cpp_delete( diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index 9e88e8ab8e8..cfd98415367 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -130,7 +130,7 @@ void goto_symext::parameter_assignments( } } - symex_assign_rec(state, code_assignt(lhs, rhs)); + symex_assign(state, code_assignt(lhs, rhs)); } if(it1!=arguments.end()) @@ -162,7 +162,7 @@ void goto_symext::parameter_assignments( symbol_exprt lhs=symbol_exprt(id, it1->type()); - symex_assign_rec(state, code_assignt(lhs, *it1)); + symex_assign(state, code_assignt(lhs, *it1)); } } else if(it1!=arguments.end()) @@ -275,7 +275,7 @@ void goto_symext::symex_function_call_code( side_effect_expr_nondett rhs(call.lhs().type()); rhs.add_source_location()=call.source_location(); code_assignt code(call.lhs(), rhs); - symex_assign_rec(state, code); + symex_assign(state, code); } symex_transition(state); @@ -455,7 +455,7 @@ void goto_symext::return_assignment(statet &state) "assignment.lhs().type():\n"+assignment.lhs().type().pretty()+"\n"+ "assignment.rhs().type():\n"+assignment.rhs().type().pretty(); - symex_assign_rec(state, assignment); + symex_assign(state, assignment); } } else diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 9ffa9438aaa..3273041479d 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -293,7 +293,7 @@ void goto_symext::symex_step( case ASSIGN: if(!state.guard.is_false()) - symex_assign_rec(state, to_code_assign(instruction.code)); + symex_assign(state, to_code_assign(instruction.code)); symex_transition(state); break; From 9ba7fe29cdadb82bdc4c2d25063ab3c1cbca6d50 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 13 Feb 2018 18:19:23 +0000 Subject: [PATCH 2/2] cleanup of some noise (mostly obvious declarators) in the goto_symext class --- src/goto-symex/goto_symex.h | 208 +++++++++++++++++------------------- 1 file changed, 100 insertions(+), 108 deletions(-) diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 4af4e55d51b..773aa721d70 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -84,9 +84,9 @@ class goto_symext /// footprint, so if keeping the state around is not necessary, /// clients should instead call goto_symext::symex_from_entry_point_of(). virtual void symex_with_state( - statet &state, - const goto_functionst &goto_functions, - const goto_programt &goto_program); + statet &, + const goto_functionst &, + const goto_programt &); /// Symexes from the first instruction and the given state, terminating as /// soon as the last instruction is reached. This is useful to explicitly @@ -97,8 +97,8 @@ class goto_symext /// \param first Entry point in form of a first instruction. /// \param limit Final instruction, which itself will not be symexed. virtual void symex_instruction_range( - statet &state, - const goto_functionst &goto_functions, + statet &, + const goto_functionst &, goto_programt::const_targett first, goto_programt::const_targett limit); @@ -111,8 +111,8 @@ class goto_symext /// \param limit final instruction, which itself will not /// be symexed. void initialize_entry_point( - statet &state, - const goto_functionst &goto_functions, + statet &, + const goto_functionst &, goto_programt::const_targett pc, goto_programt::const_targett limit); @@ -121,16 +121,16 @@ class goto_symext /// \param state Current GOTO symex step. /// \param goto_functions GOTO model to symex. void symex_threaded_step( - statet &state, const goto_functionst &goto_functions); + statet &, const goto_functionst &); /** execute just one step */ virtual void symex_step( - const goto_functionst &goto_functions, - statet &state); + const goto_functionst &, + statet &); public: // these bypass the target maps - virtual void symex_step_goto(statet &state, bool taken); + virtual void symex_step_goto(statet &, bool taken); // statistics unsigned total_vccs, remaining_vccs; @@ -160,37 +160,33 @@ class goto_symext // b) remove pointer dereferencing // c) rewrite array_equal expression into equality void clean_expr( - exprt &expr, statet &state, bool write); - - void replace_array_equal(exprt &expr); - void trigger_auto_object(const exprt &expr, statet &state); - void initialize_auto_object(const exprt &expr, statet &state); - void process_array_expr(exprt &expr); - void process_array_expr_rec(exprt &expr, const typet &type) const; - exprt make_auto_object(const typet &type); - - virtual void dereference( - exprt &expr, - statet &state, - const bool write); + exprt &, statet &, bool write); + + void replace_array_equal(exprt &); + void trigger_auto_object(const exprt &, statet &); + void initialize_auto_object(const exprt &, statet &); + void process_array_expr(exprt &); + void process_array_expr_rec(exprt &, const typet &) const; + exprt make_auto_object(const typet &); + virtual void dereference(exprt &, statet &, const bool write); void dereference_rec( - exprt &expr, - statet &state, - guardt &guard, + exprt &, + statet &, + guardt &, const bool write); void dereference_rec_address_of( - exprt &expr, - statet &state, - guardt &guard); + exprt &, + statet &, + guardt &); static bool is_index_member_symbol_if(const exprt &expr); exprt address_arithmetic( - const exprt &expr, - statet &state, - guardt &guard, + const exprt &, + statet &, + guardt &, bool keep_array); // guards @@ -199,9 +195,10 @@ class goto_symext // symex virtual void symex_transition( - statet &state, + statet &, goto_programt::const_targett to, bool is_backwards_goto=false); + virtual void symex_transition(statet &state) { goto_programt::const_targett next=state.source.pc; @@ -209,31 +206,28 @@ class goto_symext symex_transition(state, next); } - virtual void symex_goto(statet &state); - virtual void symex_start_thread(statet &state); - virtual void symex_atomic_begin(statet &state); - virtual void symex_atomic_end(statet &state); - virtual void symex_decl(statet &state); - virtual void symex_decl(statet &state, const symbol_exprt &expr); - virtual void symex_dead(statet &state); - - virtual void symex_other( - const goto_functionst &goto_functions, - statet &state); + virtual void symex_goto(statet &); + virtual void symex_start_thread(statet &); + virtual void symex_atomic_begin(statet &); + virtual void symex_atomic_end(statet &); + virtual void symex_decl(statet &); + virtual void symex_decl(statet &, const symbol_exprt &expr); + virtual void symex_dead(statet &); + virtual void symex_other(const goto_functionst &, statet &); virtual void vcc( - const exprt &expr, + const exprt &, const std::string &msg, - statet &state); + statet &); - virtual void symex_assume(statet &state, const exprt &cond); + virtual void symex_assume(statet &, const exprt &cond); // gotos - void merge_gotos(statet &state); + void merge_gotos(statet &); virtual void merge_goto( const statet::goto_statet &goto_state, - statet &state); + statet &); void merge_value_sets( const statet::goto_statet &goto_state, @@ -241,7 +235,7 @@ class goto_symext void phi_function( const statet::goto_statet &goto_state, - statet &state); + statet &); // determine whether to unwind a loop -- true indicates abort, // with false we continue. @@ -249,33 +243,33 @@ class goto_symext const symex_targett::sourcet &source, unsigned unwind); - virtual void loop_bound_exceeded(statet &state, const exprt &guard); + virtual void loop_bound_exceeded(statet &, const exprt &guard); // function calls - void pop_frame(statet &state); - void return_assignment(statet &state); + void pop_frame(statet &); + void return_assignment(statet &); virtual void no_body(const irep_idt &identifier) { } virtual void symex_function_call( - const goto_functionst &goto_functions, - statet &state, - const code_function_callt &call); + const goto_functionst &, + statet &, + const code_function_callt &); - virtual void symex_end_of_function(statet &state); + virtual void symex_end_of_function(statet &); virtual void symex_function_call_symbol( - const goto_functionst &goto_functions, - statet &state, - const code_function_callt &call); + const goto_functionst &, + statet &, + const code_function_callt &); virtual void symex_function_call_code( - const goto_functionst &goto_functions, - statet &state, - const code_function_callt &call); + const goto_functionst &, + statet &, + const code_function_callt &); virtual bool get_unwind_recursion( const irep_idt &identifier, @@ -284,28 +278,26 @@ class goto_symext void parameter_assignments( const irep_idt function_identifier, - const goto_functionst::goto_functiont &goto_function, - statet &state, + const goto_functionst::goto_functiont &, + statet &, const exprt::operandst &arguments); void locality( const irep_idt function_identifier, - statet &state, - const goto_functionst::goto_functiont &goto_function); + statet &, + const goto_functionst::goto_functiont &); void add_end_of_function( exprt &code, const irep_idt &identifier); // exceptions + void symex_throw(statet &); + void symex_catch(statet &); - void symex_throw(statet &state); - void symex_catch(statet &state); - - virtual void do_simplify(exprt &expr); + virtual void do_simplify(exprt &); - // virtual void symex_block(statet &state, const codet &code); - void symex_assign(statet &state, const code_assignt &code); + void symex_assign(statet &, const code_assignt &); // havocs the given object void havoc_rec(statet &, const guardt &, const exprt &); @@ -313,77 +305,77 @@ class goto_symext typedef symex_targett::assignment_typet assignment_typet; void symex_assign_rec( - statet &state, + statet &, const exprt &lhs, const exprt &full_lhs, const exprt &rhs, - guardt &guard, - assignment_typet assignment_type); + guardt &, + assignment_typet); void symex_assign_symbol( - statet &state, + statet &, const ssa_exprt &lhs, const exprt &full_lhs, const exprt &rhs, - guardt &guard, - assignment_typet assignment_type); + guardt &, + assignment_typet); void symex_assign_typecast( - statet &state, + statet &, const typecast_exprt &lhs, const exprt &full_lhs, const exprt &rhs, - guardt &guard, - assignment_typet assignment_type); + guardt &, + assignment_typet); void symex_assign_array( - statet &state, + statet &, const index_exprt &lhs, const exprt &full_lhs, const exprt &rhs, - guardt &guard, - assignment_typet assignment_type); + guardt &, + assignment_typet); void symex_assign_struct_member( - statet &state, + statet &, const member_exprt &lhs, const exprt &full_lhs, const exprt &rhs, - guardt &guard, - assignment_typet assignment_type); + guardt &, + assignment_typet); void symex_assign_if( - statet &state, + statet &, const if_exprt &lhs, const exprt &full_lhs, const exprt &rhs, - guardt &guard, - assignment_typet assignment_type); + guardt &, + assignment_typet); void symex_assign_byte_extract( - statet &state, + statet &, const byte_extract_exprt &lhs, const exprt &full_lhs, const exprt &rhs, - guardt &guard, - assignment_typet assignment_type); + guardt &, + assignment_typet); static exprt add_to_lhs(const exprt &lhs, const exprt &what); virtual void symex_gcc_builtin_va_arg_next( - statet &state, const exprt &lhs, const side_effect_exprt &code); + statet &, const exprt &lhs, const side_effect_exprt &); virtual void symex_allocate( - statet &state, const exprt &lhs, const side_effect_exprt &code); - virtual void symex_cpp_delete(statet &state, const codet &code); + statet &, const exprt &lhs, const side_effect_exprt &); + virtual void symex_cpp_delete(statet &, const codet &); virtual void symex_cpp_new( - statet &state, const exprt &lhs, const side_effect_exprt &code); - virtual void symex_fkt(statet &state, const code_function_callt &code); - virtual void symex_macro(statet &state, const code_function_callt &code); - virtual void symex_trace(statet &state, const code_function_callt &code); - virtual void symex_printf(statet &state, const exprt &lhs, const exprt &rhs); - virtual void symex_input(statet &state, const codet &code); - virtual void symex_output(statet &state, const codet &code); + statet &, const exprt &lhs, const side_effect_exprt &); + virtual void symex_fkt(statet &, const code_function_callt &); + virtual void symex_macro(statet &, const code_function_callt &); + virtual void symex_trace(statet &, const code_function_callt &); + virtual void symex_printf(statet &, const exprt &lhs, const exprt &rhs); + virtual void symex_input(statet &, const codet &); + virtual void symex_output(statet &, const codet &); static unsigned nondet_count; static unsigned dynamic_counter; - void read(exprt &expr); - void replace_nondet(exprt &expr); - void rewrite_quantifiers(exprt &expr, statet &state); + void read(exprt &); + void replace_nondet(exprt &); + void rewrite_quantifiers(exprt &, statet &); }; #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_H