From 6ee70ea3d75811eb99326677913c5b2c0b536e98 Mon Sep 17 00:00:00 2001 From: Dario Cattaruzza Date: Tue, 25 Oct 2016 16:14:56 +0100 Subject: [PATCH 1/9] get symbol of member --- src/util/std_expr.h | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 55229d45115..3338160e4f3 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -2962,6 +2962,17 @@ class member_exprt:public exprt { return op0(); } + + //Retrieves the object(symbol) this member corresponds to + inline const symbol_exprt &symbol() const + { + const exprt &op=op0(); + if (op.id()==ID_member) + { + return static_cast(op).symbol(); + } + return to_symbol_expr(op); + } }; /*! \brief Cast a generic exprt to a \ref member_exprt From 471473e0e33013630834652ab773b8fb7a5531ba Mon Sep 17 00:00:00 2001 From: Dario Cattaruzza Date: Tue, 25 Oct 2016 16:16:01 +0100 Subject: [PATCH 2/9] Auxiliary function for getting byte offsets of members --- src/util/pointer_offset_size.cpp | 58 ++++++++++++++++++++------------ src/util/pointer_offset_size.h | 15 +++++++++ 2 files changed, 52 insertions(+), 21 deletions(-) diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp index 4d1d15c82e7..4a989582c9b 100644 --- a/src/util/pointer_offset_size.cpp +++ b/src/util/pointer_offset_size.cpp @@ -21,6 +21,39 @@ Author: Daniel Kroening, kroening@kroening.com #include "pointer_offset_size.h" +member_offset_iterator::member_offset_iterator(const struct_typet& _type, + const namespacet& _ns) : + type(_type), + ns(_ns), + bit_field_bits(0), + current({0,0}) +{ +} + +member_offset_iterator& member_offset_iterator::operator++() +{ + if(current.second!=-1) // Already failed? + { + const auto& comp=type.components()[current.first]; + if(comp.type().id()==ID_c_bit_field) + { + // take the extra bytes needed + std::size_t w=to_c_bit_field_type(comp.type()).get_width(); + for(; w>bit_field_bits; ++current.second, bit_field_bits+=8); + bit_field_bits-=w; + } + else + { + const typet &subtype=comp.type(); + mp_integer sub_size=pointer_offset_size(subtype, ns); + if(sub_size==-1) current.second=-1; // give up + else current.second+=sub_size; + } + } + ++current.first; + return *this; +} + /*******************************************************************\ Function: member_offset @@ -39,35 +72,18 @@ mp_integer member_offset( const namespacet &ns) { const struct_typet::componentst &components=type.components(); - - mp_integer result=0; - std::size_t bit_field_bits=0; + member_offset_iterator offsets(type,ns); for(struct_typet::componentst::const_iterator it=components.begin(); - it!=components.end(); - it++) + it!=components.end() && offsets->second!=-1; + ++it, ++offsets) { if(it->get_name()==member) break; - - if(it->type().id()==ID_c_bit_field) - { - // take the extra bytes needed - std::size_t w=to_c_bit_field_type(it->type()).get_width(); - for(; w>bit_field_bits; ++result, bit_field_bits+=8); - bit_field_bits-=w; - } - else - { - const typet &subtype=it->type(); - mp_integer sub_size=pointer_offset_size(subtype, ns); - if(sub_size==-1) return -1; // give up - result+=sub_size; - } } - return result; + return offsets->second; } /*******************************************************************\ diff --git a/src/util/pointer_offset_size.h b/src/util/pointer_offset_size.h index 45f15b85c20..efecbd6f647 100644 --- a/src/util/pointer_offset_size.h +++ b/src/util/pointer_offset_size.h @@ -21,6 +21,21 @@ class constant_exprt; // these return -1 on failure +// Walks trhough a structure and gives a byte offset for each member +class member_offset_iterator { + typedef std::pair refst; + refst current; + const struct_typet &type; + const namespacet &ns; + size_t bit_field_bits; + public: + member_offset_iterator(const struct_typet& _type, + const namespacet& _ns); + member_offset_iterator& operator++(); + const refst& operator*() const { return current; } + const refst* operator->() const { return ¤t; } +}; + mp_integer member_offset( const struct_typet &type, const irep_idt &member, From 59746be02ff6697e39b89cd485e9dfbe3c82181d Mon Sep 17 00:00:00 2001 From: Dario Cattaruzza Date: Tue, 25 Oct 2016 16:16:43 +0100 Subject: [PATCH 3/9] Auxiliary function to check if the ssa has enough data to build an identifier --- src/util/ssa_expr.cpp | 15 +++++++++++++++ src/util/ssa_expr.h | 7 ++++++- 2 files changed, 21 insertions(+), 1 deletion(-) diff --git a/src/util/ssa_expr.cpp b/src/util/ssa_expr.cpp index 06a92e64f05..b7a229a1e58 100644 --- a/src/util/ssa_expr.cpp +++ b/src/util/ssa_expr.cpp @@ -69,6 +69,19 @@ static void build_ssa_identifier_rec( assert(false); } +/* Used to determine whether or not an identifier can be built + * before trying and getting an exception */ +bool ssa_exprt::can_build_identifier(const exprt &expr) +{ + if(expr.id()==ID_symbol) + return true; + else if(expr.id()==ID_member || + expr.id()==ID_index) + return can_build_identifier(expr.op0()); + else + return false; +} + /*******************************************************************\ Function: ssa_exprt::build_identifier @@ -94,3 +107,5 @@ irep_idt ssa_exprt::build_identifier( return oss.str(); } + + diff --git a/src/util/ssa_expr.h b/src/util/ssa_expr.h index d65a491f4c3..03e9cdb6d16 100644 --- a/src/util/ssa_expr.h +++ b/src/util/ssa_expr.h @@ -64,7 +64,7 @@ class ssa_exprt:public symbol_exprt inline const irep_idt get_l1_object_identifier() const { - #if 0 + #if 1 return get_l1_object().get_identifier(); #else // the above is the clean version, this is the fast one, making @@ -138,6 +138,11 @@ class ssa_exprt:public symbol_exprt const irep_idt &l0, const irep_idt &l1, const irep_idt &l2); + + /* Used to determine whether or not an identifier can be built + * before trying and getting an exception */ + static bool can_build_identifier(const exprt &src); + }; /*! \brief Cast a generic exprt to an \ref ssa_exprt From 019ef0c4d027fb485859ef83c018ad62e1b03117 Mon Sep 17 00:00:00 2001 From: Dario Cattaruzza Date: Tue, 25 Oct 2016 16:17:06 +0100 Subject: [PATCH 4/9] Bitwise operators for mpinteger --- src/util/mp_arith.cpp | 240 ++++++++++++++++++++++++++++++++++++++++++ src/util/mp_arith.h | 23 ++++ 2 files changed, 263 insertions(+) diff --git a/src/util/mp_arith.cpp b/src/util/mp_arith.cpp index b5a224c7977..7c3c7ea7409 100644 --- a/src/util/mp_arith.cpp +++ b/src/util/mp_arith.cpp @@ -17,6 +17,9 @@ Author: Daniel Kroening, kroening@kroening.com #include "mp_arith.h" #include "arith_tools.h" + +typedef BigInt::ullong_t ullong_t; + /*******************************************************************\ Function: >> @@ -315,3 +318,240 @@ unsigned integer2unsigned(const mp_integer &n) assert(ull <= std::numeric_limits::max()); return (unsigned)ull; } + + +/*******************************************************************\ + +Function: bitwise_or + + Inputs: + + Outputs: + + Purpose: bitwise or + bitwise operations only make sense on native objects, hence the + largest object size should be the largest available c++ integer + size (currently long long) + + +\*******************************************************************/ +mp_integer bitwise_or(const mp_integer &a, const mp_integer &b) +{ + ullong_t result=a.to_ulong()|b.to_ulong(); + return result; +} + +/*******************************************************************\ + +Function: bitwise_and + + Inputs: + + Outputs: + + Purpose: bitwise and + bitwise operations only make sense on native objects, hence the + largest object size should be the largest available c++ integer + size (currently long long) + + +\*******************************************************************/ +mp_integer bitwise_and(const mp_integer &a, const mp_integer &b) +{ + ullong_t result=a.to_ulong()&b.to_ulong(); + return result; +} + +/*******************************************************************\ + +Function: bitwise_xor + + Inputs: + + Outputs: + + Purpose: bitwise xor + bitwise operations only make sense on native objects, hence the + largest object size should be the largest available c++ integer + size (currently long long) + + +\*******************************************************************/ +mp_integer bitwise_xor(const mp_integer &a, const mp_integer &b) +{ + ullong_t result=a.to_ulong()^b.to_ulong(); + return result; +} + +/*******************************************************************\ + +Function: bitwise_neg + + Inputs: + + Outputs: + + Purpose: bitwise negation + bitwise operations only make sense on native objects, hence the + largest object size should be the largest available c++ integer + size (currently long long) + + +\*******************************************************************/ +mp_integer bitwise_neg(const mp_integer &a) +{ + ullong_t result=~a.to_ulong(); + return result; +} + + +/*******************************************************************\ + +Function: arith_left_shift + + Inputs: + + Outputs: + + Purpose: arithmetic left shift + bitwise operations only make sense on native objects, hence the + largest object size should be the largest available c++ integer + size (currently long long) + +\*******************************************************************/ +mp_integer arith_left_shift(const mp_integer &a, + const mp_integer &b,unsigned true_size) +{ + ullong_t shift=b.to_ulong(); + if (shift>true_size && a!=mp_zero) throw "shift value out of range"; + ullong_t result=a.to_ulong()<true_size) throw "shift value out of range"; + ullong_t sign=(1<<(true_size-1))&number; + ullong_t pad=(sign==0) ? 0 : ~(1<<(true_size-shift)-1); + ullong_t result=(number>>shift)|pad; + return result; +} + +/*******************************************************************\ + +Function: logic_left_shift + + Inputs: + + Outputs: + + Purpose: logic left shift + bitwise operations only make sense on native objects, hence the + largest object size should be the largest available c++ integer + size (currently long long) + + +\*******************************************************************/ +mp_integer logic_left_shift(const mp_integer &a, + const mp_integer &b,unsigned true_size) +{ + ullong_t shift=b.to_ulong(); + if (shift>true_size && a!=mp_zero) throw "shift value out of range"; + ullong_t result=a.to_ulong()<true_size) throw "shift value out of range"; + ullong_t result=a.to_ulong()>>shift; + return result; +} + +/*******************************************************************\ + +Function: rotate_right + + Inputs: + + Outputs: + + Purpose: rotates right (MSB=LSB) + bitwise operations only make sense on native objects, hence the + largest object size should be the largest available c++ integer + size (currently long long) + + +\*******************************************************************/ +mp_integer rotate_right(const mp_integer &a, + const mp_integer &b,unsigned true_size) +{ + ullong_t number=a.to_ulong(); + ullong_t shift=b.to_ulong(); + if (shift>true_size) throw "shift value out of range"; + ullong_t revShift=true_size-shift; + ullong_t filter=1<<(true_size-1); + ullong_t result=(number>>shift)|((number<true_size) throw "shift value out of range"; + ullong_t revShift=true_size-shift; + ullong_t filter=1<<(true_size-1); + ullong_t result=((number<>revShift); + return result; +} diff --git a/src/util/mp_arith.h b/src/util/mp_arith.h index 007e477b62b..3e9b9fdb013 100644 --- a/src/util/mp_arith.h +++ b/src/util/mp_arith.h @@ -19,6 +19,28 @@ typedef BigInt mp_integer; std::ostream& operator<<(std::ostream &, const mp_integer &); mp_integer operator>>(const mp_integer &, const mp_integer &); mp_integer operator<<(const mp_integer &, const mp_integer &); +mp_integer bitwise_or(const mp_integer &, const mp_integer &); +mp_integer bitwise_and(const mp_integer &, const mp_integer &); +mp_integer bitwise_xor(const mp_integer &, const mp_integer &); +mp_integer bitwise_neg(const mp_integer &); + +mp_integer arith_left_shift(const mp_integer &, + const mp_integer &,unsigned true_size); + +mp_integer arith_right_shift(const mp_integer &, + const mp_integer &,unsigned true_size); + +mp_integer logic_left_shift(const mp_integer &, + const mp_integer &,unsigned true_size); + +mp_integer logic_right_shift(const mp_integer &, + const mp_integer &,unsigned true_size); + +mp_integer rotate_right(const mp_integer &, + const mp_integer &,unsigned true_size); + +mp_integer rotate_left(const mp_integer &, + const mp_integer &,unsigned true_size); const std::string integer2string(const mp_integer &, unsigned base=10); const mp_integer string2integer(const std::string &, unsigned base=10); @@ -27,5 +49,6 @@ const mp_integer binary2integer(const std::string &, bool is_signed); mp_integer::ullong_t integer2ulong(const mp_integer &); std::size_t integer2size_t(const mp_integer &); unsigned integer2unsigned(const mp_integer &); +const mp_integer mp_zero=string2integer("0"); #endif From b484a6fc98ce2911cc9812ccae6fd4ede18e0b8e Mon Sep 17 00:00:00 2001 From: Dario Cattaruzza Date: Tue, 25 Oct 2016 16:18:08 +0100 Subject: [PATCH 5/9] Auxiliary function to retrieve tail of trace Added dead command to trace --- src/goto-programs/goto_trace.cpp | 6 +++++- src/goto-programs/goto_trace.h | 6 ++++++ 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index 8370e4b48f3..e35a9058ac1 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -67,6 +67,7 @@ void goto_trace_stept::output( case goto_trace_stept::ASSIGNMENT: out << "ASSIGNMENT"; break; case goto_trace_stept::GOTO: out << "GOTO"; break; case goto_trace_stept::DECL: out << "DECL"; break; + case goto_trace_stept::DEAD: out << "DEAD"; break; case goto_trace_stept::OUTPUT: out << "OUTPUT"; break; case goto_trace_stept::INPUT: out << "INPUT"; break; case goto_trace_stept::ATOMIC_BEGIN: out << "ATOMC_BEGIN"; break; @@ -75,7 +76,10 @@ void goto_trace_stept::output( case goto_trace_stept::SHARED_WRITE: out << "SHARED WRITE"; break; case goto_trace_stept::FUNCTION_CALL: out << "FUNCTION CALL"; break; case goto_trace_stept::FUNCTION_RETURN: out << "FUNCTION RETURN"; break; - default: assert(false); + default: { + out << "unknown type: " << type << std::endl; + assert(false); + } } if(type==ASSERT || type==ASSUME || type==GOTO) diff --git a/src/goto-programs/goto_trace.h b/src/goto-programs/goto_trace.h index b1629a5a6f5..478e28ca783 100644 --- a/src/goto-programs/goto_trace.h +++ b/src/goto-programs/goto_trace.h @@ -154,6 +154,12 @@ class goto_tracet steps.push_back(step); } + //Retrieves the final step in the trace + inline goto_trace_stept &get_last_step() + { + return steps.back(); + } + // delete all steps after (not including) s void trim_after(stepst::iterator s) { From 3bfe1e9536775b2e5a7790ece6eecf1c6da60e86 Mon Sep 17 00:00:00 2001 From: Dario Cattaruzza Date: Tue, 25 Oct 2016 16:33:23 +0100 Subject: [PATCH 6/9] Changes to interpreter to cover a number of java functions and objects including: bitwise operations variable size arrays dereferencing dead objects dynamical objects input enumeration (trace backtracking) --- src/goto-instrument/Makefile | 1 + .../goto_instrument_parse_options.cpp | 2 +- src/goto-programs/interpreter.cpp | 1777 ++++++++++++++++- src/goto-programs/interpreter.h | 5 +- src/goto-programs/interpreter_class.h | 125 +- src/goto-programs/interpreter_evaluate.cpp | 687 ++++++- 6 files changed, 2468 insertions(+), 129 deletions(-) diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index fd44907bb11..fddf70a5d51 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -37,6 +37,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../langapi/langapi$(LIBEXT) \ ../xmllang/xmllang$(LIBEXT) \ ../util/util$(LIBEXT) \ + ../json/json$(LIBEXT) \ ../solvers/solvers$(LIBEXT) INCLUDES= -I .. diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 3304c2529b7..9289b0fa89d 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -442,7 +442,7 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("interpreter")) { status() << "Starting interpreter" << eom; - interpreter(symbol_table, goto_functions); + interpreter(symbol_table, goto_functions, this); return 0; } diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index 9bc13619754..e03ef8b8f79 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -9,13 +9,23 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include +#include #include #include +#include +#include +#include +#include +#include +#include +#include #include "interpreter.h" #include "interpreter_class.h" +#include "remove_returns.h" /*******************************************************************\ @@ -31,8 +41,41 @@ Function: interpretert::operator() void interpretert::operator()() { + show=true; + message->status() << "0- Initialize:" << messaget::eom; + initialise(true); + try + { + std::cout << "Type h for help" << std::endl; + while(!done) command(); + message->status() << total_steps << "- Program End." + << messaget::endl << messaget::eom; + } + catch (const char *e) + { + message->error() << e << messaget::endl << messaget::eom; + } + while(!done) command(); +} + +/******************************************************************* + +Function: interpretert::initialise + + Inputs: + + Outputs: + + Purpose: Initialises the memory map of the interpreter and + [optionally] runs up to the entry point (thus doing + non-program initialization) + + \*******************************************************************/ + +void interpretert::initialise(bool init) { build_memory_map(); + total_steps=0; const goto_functionst::function_mapt::const_iterator main_it=goto_functions.function_map.find(goto_functionst::entry_point()); @@ -48,12 +91,22 @@ void interpretert::operator()() function=main_it; done=false; - - while(!done) - { + if(init) { + stack_depth=call_stack.size()+1; show_state(); - command(); - if(!done) step(); + step(); + while(!done && (stack_depth<=call_stack.size()) && (stack_depth>=0)) + { + show_state(); + step(); + } + while(!done && (call_stack.size()==0)) + { + show_state(); + step(); + } + clear_input_flags(); + input_vars.clear(); } } @@ -65,25 +118,28 @@ Function: interpretert::show_state Outputs: - Purpose: + Purpose: displays the current position of the pc and corresponding + code \*******************************************************************/ void interpretert::show_state() { - std::cout << std::endl; - std::cout << "----------------------------------------------------" - << std::endl; + if(!show) return; + message->status() << messaget::endl; + message->status() << total_steps+1 << " ----------------------------------------------------" + << messaget::endl; if(PC==function->second.body.instructions.end()) { - std::cout << "End of function `" - << function->first << "'" << std::endl; + message->status() << "End of function `" + << function->first << "'" << messaget::endl; } else - function->second.body.output_instruction(ns, function->first, std::cout, PC); - - std::cout << std::endl; + function->second.body.output_instruction(ns, function->first, + message->status(), PC); + + message->status() << messaget::eom; } /*******************************************************************\ @@ -94,14 +150,14 @@ Function: interpretert::command Outputs: - Purpose: + Purpose: reads a user command and rus it. \*******************************************************************/ void interpretert::command() { #define BUFSIZE 100 - char command[BUFSIZE]; + char command[BUFSIZE]; if(fgets(command, BUFSIZE-1, stdin)==NULL) { done=true; @@ -109,9 +165,121 @@ void interpretert::command() } char ch=tolower(command[0]); - if(ch=='q') done=true; + else if(ch=='h') + { + std::cout << "Interpreter help" << std::endl; + std::cout << "h: display this menu" << std::endl; + std::cout << "i: output program inputs" << std::endl; + std::cout << "id: output program inputs with det values for don cares" + << std::endl; + std::cout << "in: output program inputs with non-det values for don cares" + << std::endl; + std::cout << "it: output program inputs for last trace" << std::endl; + std::cout << "if: output program inputs ids for non-bodied function" + << std::endl; + std::cout << "i file: output program inputs for [json] file trace" + << std::endl; + std::cout << "j: output json trace" << std::endl; + std::cout << "m: output memory dump" << std::endl; + std::cout << "o: output goto trace" << std::endl; + std::cout << "q: quit" << std::endl; + std::cout << "r: run until completion" << std::endl; + std::cout << "s#: step a number of instructions" << std::endl; + std::cout << "sa: step across a function" << std::endl; + std::cout << "so: step out of a function" << std::endl; + } + else if(ch=='i') + { + ch=tolower(command[1]); + if(ch=='d') list_inputs(false); + else if(ch=='n') list_inputs(true); + else if(ch=='t') { + list_input_varst ignored; + side_effects_differencet diffs; + load_counter_example_inputs(steps, ignored, diffs); + } + else if(ch==' ') load_counter_example_inputs(command+3); + else if(ch=='f') { + list_non_bodied(); + show_state(); + return; + } + print_inputs(); + } + else if(ch=='j') + { + jsont json_steps; + convert(ns, steps, json_steps); + ch=tolower(command[1]); + if(ch==' ') { + std::ofstream file; + file.open(command+2); + if(file.is_open()) + { + json_steps.output(file); + file.close(); + return; + } + } + json_steps.output(message->result()); + } + else if(ch=='m') + { + ch=tolower(command[1]); + print_memory(ch=='i'); + } + else if(ch=='o') + { + ch=tolower(command[1]); + if(ch==' ') + { + std::ofstream file; + file.open(command+2); + if(file.is_open()) + { + steps.output(ns, file); + file.close(); + return; + } + } + steps.output(ns, message->result()); + } + else if(ch=='r') + { + ch=tolower(command[1]); + initialise(ch!='0'); + } + else if((ch=='s') || (ch==0)) + { + num_steps=1; + stack_depth=-1; + ch=tolower(command[1]); + if(ch=='e') + num_steps=-1; + else if(ch=='o') + stack_depth=call_stack.size(); + else if(ch=='a') + stack_depth=call_stack.size()+1; + else { + num_steps=atoi(command+1); + if(num_steps==0) num_steps=1; + } + while(!done && ((num_steps<0) || ((num_steps--)>0))) + { + step(); + show_state(); + } + while(!done && (stack_depth<=call_stack.size()) + && (stack_depth>=0)) + { + step(); + show_state(); + } + return; + } + show_state(); } /*******************************************************************\ @@ -122,12 +290,13 @@ Function: interpretert::step Outputs: - Purpose: + Purpose: performs a single step executiona and updates the pc \*******************************************************************/ void interpretert::step() { + total_steps++; if(PC==function->second.body.instructions.end()) { if(call_stack.empty()) @@ -136,7 +305,8 @@ void interpretert::step() { PC=call_stack.top().return_PC; function=call_stack.top().return_function; - stack_pointer=call_stack.top().old_stack_pointer; + //stack_pointer=call_stack.top().old_stack_pointer; + //TODO: this increases memory size quite quickly. Should check alternatives call_stack.pop(); } @@ -144,19 +314,26 @@ void interpretert::step() } next_PC=PC; - next_PC++; + next_PC++; + steps.add_step(goto_trace_stept()); + goto_trace_stept &trace_step=steps.get_last_step(); + trace_step.thread_nr=thread_id; + trace_step.pc=PC; switch(PC->type) { case GOTO: + trace_step.type=goto_trace_stept::GOTO; execute_goto(); break; case ASSUME: + trace_step.type=goto_trace_stept::ASSUME; execute_assume(); break; case ASSERT: + trace_step.type=goto_trace_stept::ASSERT; execute_assert(); break; @@ -165,15 +342,20 @@ void interpretert::step() break; case DECL: + trace_step.type=goto_trace_stept::DECL; execute_decl(); break; case SKIP: case LOCATION: + trace_step.type=goto_trace_stept::LOCATION; + break; case END_FUNCTION: + trace_step.type=goto_trace_stept::FUNCTION_RETURN; break; case RETURN: + trace_step.type=goto_trace_stept::FUNCTION_RETURN; if(call_stack.empty()) throw "RETURN without call"; @@ -189,14 +371,17 @@ void interpretert::step() break; case ASSIGN: + trace_step.type=goto_trace_stept::ASSIGNMENT; execute_assign(); break; case FUNCTION_CALL: + trace_step.type=goto_trace_stept::FUNCTION_CALL; execute_function_call(); break; case START_THREAD: + trace_step.type=goto_trace_stept::SPAWN; throw "START_THREAD not yet implemented"; case END_THREAD: @@ -204,18 +389,43 @@ void interpretert::step() break; case ATOMIC_BEGIN: + trace_step.type=goto_trace_stept::ATOMIC_BEGIN; throw "ATOMIC_BEGIN not yet implemented"; case ATOMIC_END: + trace_step.type=goto_trace_stept::ATOMIC_END; throw "ATOMIC_END not yet implemented"; case DEAD: - throw "DEAD not yet implemented"; - + trace_step.type=goto_trace_stept::DEAD; + break;//throw "DEAD not yet implemented"; + case THROW: + trace_step.type=goto_trace_stept::GOTO; + while(!done && (PC->type!=CATCH)) + { + if(PC==function->second.body.instructions.end()) + { + if(call_stack.empty()) + done=true; + else + { + PC=call_stack.top().return_PC; + function=call_stack.top().return_function; + call_stack.pop(); + } + } + else + { + next_PC=PC; + next_PC++; + } + } + break; + case CATCH: + break; default: throw "encountered instruction with undefined instruction type"; } - PC=next_PC; } @@ -227,7 +437,7 @@ Function: interpretert::execute_goto Outputs: - Purpose: + Purpose: executes a goto instruction \*******************************************************************/ @@ -253,20 +463,34 @@ Function: interpretert::execute_other Outputs: - Purpose: + Purpose: executes side effects of 'other' instructions \*******************************************************************/ void interpretert::execute_other() { const irep_idt &statement=PC->code.get_statement(); - if(statement==ID_expression) { assert(PC->code.operands().size()==1); std::vector rhs; evaluate(PC->code.op0(), rhs); } + else if(statement==ID_array_set) + { + std::vector tmp,rhs; + evaluate(PC->code.op1(), tmp); + mp_integer address=evaluate_address(PC->code.op0()); + unsigned size=get_size(PC->code.op0().type()); + while(rhs.size()error() << "!! failed to obtain rhs (" << rhs.size() << " vs. " + << size << ")" << messaget::endl << messaget::eom; + else + { + assign(address, rhs); + } + } else throw "unexpected OTHER statement: "+id2string(statement); } @@ -288,7 +512,203 @@ void interpretert::execute_decl() assert(PC->code.get_statement()==ID_decl); } -/*******************************************************************\ +/******************************************************************* + +Function: interpretert::get_component_id + + Inputs: an object and a memory offset + + Outputs: + + Purpose: retrieves the member at offset + + \*******************************************************************/ +irep_idt interpretert::get_component_id(const irep_idt &object,unsigned offset) +{ + const symbolt &symbol=ns.lookup(object); + const typet real_type=ns.follow(symbol.type); + if(real_type.id()!=ID_struct) + throw "request for member of non-struct"; + const struct_typet &struct_type=to_struct_type(real_type); + const struct_typet::componentst &components=struct_type.components(); + for(struct_typet::componentst::const_iterator it=components.begin(); + it!=components.end();++it) { + if(offset<=0) return it->id(); + unsigned size=get_size(it->type()); + assert(size>=0); + offset -= size; + } + return object; +} + +/******************************************************************* + +Function: interpretert::get_type + + Inputs: + + Outputs: + + Purpose: returns the type object corresponding to id + + \*******************************************************************/ +typet interpretert::get_type(const irep_idt &id) const +{ + dynamic_typest::const_iterator it=dynamic_types.find(id); + if (it==dynamic_types.end()) return symbol_table.lookup(id).type; + return it->second; +} + +/******************************************************************* + +Function: interpretert::get_value + + Inputs: + + Outputs: + + Purpose: retrives the constant value at memory location offset + as an object of type type + + \*******************************************************************/ +exprt interpretert::get_value(const typet &type, + unsigned offset,bool use_non_det) +{ + const typet real_type=ns.follow(type); + if(real_type.id()==ID_struct) { + exprt result=struct_exprt(real_type); + const struct_typet &struct_type=to_struct_type(real_type); + const struct_typet::componentst &components=struct_type.components(); + result.reserve_operands(components.size()); + for(struct_typet::componentst::const_iterator it=components.begin(); + it!=components.end();++it) { + unsigned size=get_size(it->type()); + assert(size>=0); + const exprt operand=get_value(it->type(), offset); + offset += size; + result.copy_to_operands(operand); + } + return result; + } else if(real_type.id()==ID_array) { + exprt result=array_exprt(to_array_type(real_type)); + const exprt &size_expr=static_cast(type.find(ID_size)); + unsigned subtype_size=get_size(type.subtype()); + mp_integer mp_count; + to_integer(size_expr, mp_count); + unsigned count=integer2unsigned(mp_count); + result.reserve_operands(count); + for(unsigned i=0;i=0)) + return side_effect_expr_nondett(type); + std::vector rhs; + rhs.push_back(memory[offset].value); + return get_value(type, rhs); +} + +/******************************************************************* + Function: interpretert::get_value + + Inputs: + + Outputs: + + Purpose: returns the value at offset in the form of type given a + memory buffer rhs which is typically a structured type + + \*******************************************************************/ +exprt interpretert::get_value(const typet &type, + std::vector &rhs,unsigned offset) +{ + const typet real_type=ns.follow(type); + + if(real_type.id()==ID_struct) { + exprt result=struct_exprt(real_type); + const struct_typet &struct_type=to_struct_type(real_type); + const struct_typet::componentst &components=struct_type.components(); + + result.reserve_operands(components.size()); + for(struct_typet::componentst::const_iterator it=components.begin(); + it!=components.end();++it) { + unsigned size=get_size(it->type()); + assert(size>=0); + const exprt operand=get_value(it->type(), rhs, offset); + offset += size; + result.copy_to_operands(operand); + } + + return result; + } else if(real_type.id()==ID_array) { + exprt result(ID_constant, type); + const exprt &size_expr=static_cast(type.find(ID_size)); + unsigned subtype_size=get_size(type.subtype()); + mp_integer mp_count; + to_integer(size_expr, mp_count); + unsigned count=integer2unsigned(mp_count); + result.reserve_operands(count); + for(unsigned i=0;ierror() << "pointer out of memory " << rhs[offset] << ">" + << memory.size() << messaget::endl << messaget::eom; + throw "pointer out of memory"; + } + return from_integer(rhs[offset], type); +} + +/******************************************************************* Function: interpretert::execute_assign @@ -296,7 +716,7 @@ Function: interpretert::execute_assign Outputs: - Purpose: + Purpose: executes the assign statement at the current pc value \*******************************************************************/ @@ -310,15 +730,41 @@ void interpretert::execute_assign() if(!rhs.empty()) { - mp_integer address=evaluate_address(code_assign.lhs()); + mp_integer address=evaluate_address(code_assign.lhs()); unsigned size=get_size(code_assign.lhs().type()); if(size!=rhs.size()) - std::cout << "!! failed to obtain rhs (" - << rhs.size() << " vs. " - << size << ")" << std::endl; + message->error() << "!! failed to obtain rhs (" << rhs.size() << " vs. " + << size << ")" << messaget::endl << messaget::eom; else + { + goto_trace_stept &trace_step=steps.get_last_step(); assign(address, rhs); + trace_step.full_lhs=code_assign.lhs(); + + /* TODO: need to look at other cases on ssa_exprt + * (derference should be handled on ssa) */ + const exprt &expr=trace_step.full_lhs; + if(ssa_exprt::can_build_identifier(trace_step.full_lhs)) + { + trace_step.lhs_object=ssa_exprt(trace_step.full_lhs); + } + trace_step.full_lhs_value=get_value(trace_step.full_lhs.type(),rhs); + trace_step.lhs_object_value=trace_step.full_lhs_value; + } + } + else if(code_assign.rhs().id()==ID_side_effect) + { + side_effect_exprt side_effect=to_side_effect_expr(code_assign.rhs()); + if(side_effect.get_statement()==ID_nondet) + { + unsigned address=integer2unsigned(evaluate_address(code_assign.lhs())); + unsigned size=get_size(code_assign.lhs().type()); + for (unsigned i=0;i &rhs) { - for(unsigned i=0; ierror() << "assertion failed" + << messaget::endl << messaget::eom; + } } /*******************************************************************\ @@ -411,8 +869,10 @@ void interpretert::execute_function_call() else if(a>=memory.size()) throw "out-of-range function call"; + goto_trace_stept &trace_step=steps.get_last_step(); const memory_cellt &cell=memory[integer2size_t(a)]; const irep_idt &identifier=cell.identifier; + trace_step.identifier=identifier; const goto_functionst::function_mapt::const_iterator f_it= goto_functions.function_map.find(identifier); @@ -430,15 +890,15 @@ void interpretert::execute_function_call() return_value_address=0; // values of the arguments - std::vector > argument_values; + std::vector>argument_values; argument_values.resize(function_call.arguments().size()); - for(std::size_t i=0; isecond.body_available()) { call_stack.push(stack_framet()); @@ -458,25 +918,10 @@ void interpretert::execute_function_call() it!=locals.end(); it++) { - const irep_idt &id=*it; + const irep_idt &id=*it; const symbolt &symbol=ns.lookup(id); - unsigned size=get_size(symbol.type); - - if(size!=0) - { - frame.local_map[id]=stack_pointer; + frame.local_map[id]=integer2unsigned(build_memory_map(id,symbol.type)); - for(unsigned i=0; i=memory.size()) memory.resize(address+1); - memory[address].value=0; - memory[address].identifier=id; - memory[address].offset=i; - } - - stack_pointer+=size; - } } // assign the arguments @@ -486,7 +931,7 @@ void interpretert::execute_function_call() if(argument_values.size()second.body.instructions.begin(); + next_PC=f_it->second.body.instructions.begin(); } else - throw "no body for "+id2string(identifier); + { + list_input_varst::iterator it= + function_input_vars.find(function_call.function().get(ID_identifier)); + if (it!=function_input_vars.end()) + { + std::vector value; + assert(it->second.size()!=0); + assert(it->second.front().return_assignments.size()!=0); + evaluate(it->second.front().return_assignments.back().value,value); + if (return_value_address>0) + { + assign(return_value_address,value); + } + if(function_call.lhs().is_not_nil()) + { + } + it->second.pop_front(); + return; + } + if (show) + message->error() << "no body for "+id2string(identifier) + << messaget::eom; + /* TODO:used to be throw. need some better approach? + * need to check state of buffers (and by refs) */ + } } /*******************************************************************\ @@ -511,7 +980,7 @@ Function: interpretert::build_memory_map Outputs: - Purpose: + Purpose: Creates a memory map of all static symbols in the program \*******************************************************************/ @@ -521,6 +990,10 @@ void interpretert::build_memory_map() memory.resize(1); memory[0].offset=0; memory[0].identifier="NULL-OBJECT"; + memory[0].initialised=0; + + num_dynamic_objects=0; + dynamic_types.clear(); // now do regular static symbols for(symbol_tablet::symbolst::const_iterator @@ -564,14 +1037,106 @@ void interpretert::build_memory_map(const symbolt &symbol) memory.resize(address+size); memory_map[symbol.name]=address; - for(unsigned i=0; i(type.find(ID_size)); + std::vector computed_size; + evaluate(size_expr,computed_size); + if(computed_size.size()==1 && + computed_size[0]>=0) + { + message->result() << "Concretised array with size " << computed_size[0] + << messaget::eom; + return array_typet(type.subtype(), + constant_exprt::integer_constant(computed_size[0].to_ulong())); + } + else { + message->error() << "Failed to concretise variable array" + << messaget::eom; + } + } + return type; +} + +/*******************************************************************\ + +Function: interpretert::build_memory_map + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ +mp_integer interpretert::build_memory_map(const irep_idt &id, + const typet &type) const +{ + typet alloc_type=concretise_type(type); + unsigned size=get_size(alloc_type); + std::map::iterator it = dynamic_types.find(id); + + if (it!=dynamic_types.end()) { + int offset=1; + + unsigned address = memory_map[id]; + + while (memory[address+offset].offset>0) offset++; + + // current size <= size already recorded + if(size<=offset) + return memory_map[id]; + + } + + /* the current size is bigger then the one previously recorded + * in the memory map */ + + if(size==0) size=1;// This is a hack to create existence + + if(size!=0) + { + unsigned address=memory.size(); + memory.resize(address+size); + memory_map[id]=address; + dynamic_types.insert(std::pair(id,alloc_type)); + + for(unsigned i=0;i i; + evaluate(size_expr,i); + if(i.size()==1) + { + // Go via the binary representation to reproduce any + // overflow behaviour. + exprt size_const=from_integer(i[0],size_expr.type()); + mp_integer size_mp; + assert(!to_integer(size_const,size_mp)); + return subtype_size*integer2unsigned(size_mp); + } else return subtype_size; } @@ -644,11 +1217,1073 @@ unsigned interpretert::get_size(const typet &type) const { return get_size(ns.follow(type)); } - else return 1; } -/*******************************************************************\ +/******************************************************************* + +Function: list_non_bodied + + Inputs: + + Outputs: + + Purpose: + + \*******************************************************************/ +void interpretert::list_non_bodied() { + int funcs=0; + function_input_vars.clear(); + for(goto_functionst::function_mapt::const_iterator f_it = + goto_functions.function_map.begin(); + f_it!=goto_functions.function_map.end(); f_it++) + { + if(f_it->second.body_available()) + { + list_non_bodied(f_it->second.body.instructions); + } + } + + message->result() << "non bodied varibles " << funcs << messaget::eom; + std::map::const_iterator it; +/*for(it=function_input_vars.begin(); it!=function_input_vars.end(); it++) + { + message->result() << it->first << "=" + << it->second.front() << messaget::endl; + }*/ + message->result() << messaget::eom; +} + +char interpretert::is_opaque_function( + const goto_programt::instructionst::const_iterator &it, + irep_idt &id) +{ + goto_programt::instructionst::const_iterator pc=it; + if (pc->is_assign()) + { + const code_assignt &code_assign=to_code_assign(pc->code); + if(code_assign.rhs().id()==ID_side_effect) + { + side_effect_exprt side_effect=to_side_effect_expr(code_assign.rhs()); + if(side_effect.get_statement()==ID_nondet) + { + pc--;//TODO: need to check if pc is not already at begin + if(pc->is_return()) pc--; + } + } + } + if(pc->type!=FUNCTION_CALL) return 0; + const code_function_callt &function_call=to_code_function_call(pc->code); + id=function_call.function().get(ID_identifier); + const goto_functionst::function_mapt::const_iterator f_it=goto_functions.function_map.find(id); + if(f_it==goto_functions.function_map.end()) + throw "failed to find function "+id2string(id); + if(f_it->second.body_available()) return 0; + if(function_call.lhs().is_not_nil()) return 1; + return -1; +} + +void interpretert::list_non_bodied( + const goto_programt::instructionst &instructions) +{ + for(goto_programt::instructionst::const_iterator f_it = + instructions.begin(); f_it!=instructions.end(); f_it++) + { + irep_idt f_id; + if(is_opaque_function(f_it,f_id)>0) + { + const code_assignt &code_assign=to_code_assign(f_it->code); + unsigned return_address= + integer2unsigned(evaluate_address(code_assign.lhs())); + if((return_address > 0) && (return_address rhs; + evaluate(it->second, rhs); + if(rhs.empty()) continue; + memory_mapt::const_iterator m_it1=memory_map.find(it->first); + if(m_it1==memory_map.end()) continue; + mp_integer address=m_it1->second; + unsigned size=get_size(it->second.type()); + if(size!=rhs.size()) continue; + assign(address, rhs); + } + clear_input_flags(); +} + +/******************************************************************* + Function: list_inputs + + Inputs: + + Outputs: + + Purpose: + + \*******************************************************************/ +void interpretert::list_inputs(bool use_non_det) { + input_vars.clear(); + for(unsigned long i=0;i=0) + continue; + if(strncmp(cell.identifier.c_str(), "__CPROVER", 9)==0) + continue; + + try { + typet symbol_type=get_type(cell.identifier); + if(use_non_det) { + exprt value=get_value(symbol_type, i - cell.offset); + input_vars.insert( + std::pair(cell.identifier, value)); + } else { + std::vector rhs; + while(memory[i].offset>0) + i--; + rhs.push_back(memory[i].value); + for(unsigned long j=i+1;j(cell.identifier, value)); + } + } catch (const char *e) { + } catch (const std::string e) { + } + for(unsigned long j=i+1; + (j=0) continue; + if (strncmp(cell.identifier.c_str(), "__CPROVER", 9)==0) continue; + if(inputs.find(cell.identifier)!=inputs.end()) + { + input_vars[cell.identifier]=inputs[cell.identifier]; + } + unsigned j=i+1; + while((j0)) j++; + i=j-1; + } + for (input_varst::iterator it=inputs.begin();it!=inputs.end();it++) + { + if ((it->second.type().id()==ID_pointer) && (it->second.has_operands())) + { + const exprt& op=it->second.op0(); + if((op.id()==ID_address_of) && (op.has_operands())) + { + mp_integer address=evaluate_address(op.op0()); + irep_idt id=memory[integer2unsigned(address)].identifier; + if(strncmp(id.c_str(),"symex_dynamic::dynamic_object",28)==0) + { + input_vars[it->first]=inputs[it->first]; + } + } + } + } +} + +/******************************************************************* + Function: print_inputs + + Inputs: + + Outputs: + + Purpose: + + \*******************************************************************/ +void interpretert::print_inputs() { + if(input_vars.size()<=0) + list_inputs(); + for(input_varst::iterator it=input_vars.begin();it!=input_vars.end(); + it++) { + message->result() << it->first << "=" + << from_expr(ns, it->first, it->second) << "[" + << it->second.type().id() << "]" << messaget::eom; + } + message->result() << messaget::eom; +} + +/******************************************************************* + Function: print_memory + + Inputs: + + Outputs: + + Purpose: + + \*******************************************************************/ +void interpretert::print_memory(bool input_flags) { + for(unsigned i=0;idebug() << cell.identifier << "[" << cell.offset << "]" + << "=" << cell.value << messaget::eom; + if(input_flags) message->debug() << "(" << (int)cell.initialised << ")" + << messaget::eom; + message->debug() << messaget::eom; + } +} + +/******************************************************************* + Function: getPC + + Inputs: + + Outputs: + + Purpose: retrieves the PC pointer for the given location + + \*******************************************************************/ +goto_programt::const_targett interpretert::getPC(const unsigned location, + bool &ok) +{ + goto_programt::const_targett no_location; + for(goto_functionst::function_mapt::const_iterator f_it = + goto_functions.function_map.begin(); + f_it!=goto_functions.function_map.end(); f_it++) + { + if(f_it->second.body_available()) + { + for(goto_programt::instructionst::const_iterator it = + f_it->second.body.instructions.begin(); + it!=f_it->second.body.instructions.end(); it++) + { + if (it->location_number==location) + { + ok=true; + return it; + } + } + } + } + ok=false; + return no_location; +} + +/******************************************************************* + Function: prune_inputs + + Inputs: + + Outputs: + + Purpose: cleans the list of inputs organising std vectors into arrays and filtering non-inputs if requested + + \*******************************************************************/ +void interpretert::prune_inputs(input_varst &inputs, + list_input_varst& function_inputs, + const bool filter) +{ + for(list_input_varst::iterator it=function_inputs.begin(); + it!=function_inputs.end();it++) + { + const exprt size=from_integer(it->second.size(), integer_typet()); + assert(it->second.front().return_assignments.size()!=0); + const auto& first_function_assigns=it->second.front().return_assignments; + const auto& toplevel_definition=first_function_assigns.back().value; + array_typet type=array_typet(toplevel_definition.type(),size); + array_exprt list(type); + list.reserve_operands(it->second.size()); + for(auto l_it : it->second) + { + list.copy_to_operands(l_it.return_assignments.back().value); + } + inputs[it->first]=list; + } + input_vars=inputs; + function_input_vars=function_inputs; + if(filter) + { + try + { + fill_inputs(inputs); + while(!done) { + show_state(); + step(); + } + } + catch (const char *e) + { + message->error() << e << messaget::eom; + } + list_inputs(); + list_inputs(inputs); + } +} + +/******************************************************************* + Function: load_counter_example_inputs + + Inputs: + + Outputs: + + Purpose: + + \*******************************************************************/ + +interpretert::input_varst& interpretert::load_counter_example_inputs( + const std::string &filename) { + jsont counter_example; + message_clientt message_client; + + if(parse_json(filename,message_client.get_message_handler(),counter_example)) + { + bool ok; + show=false; + stop_on_assertion=false; + + input_varst inputs; + list_input_varst function_inputs; + + function=goto_functions.function_map.find(goto_functionst::entry_point()); + if(function==goto_functions.function_map.end()) + throw "main not found"; + + initialise(true); + jsont::objectt::const_reverse_iterator it=counter_example.object.rbegin(); + if(it!=counter_example.object.rend()) + { + unsigned location= + integer2unsigned(string2integer(it->second["location"].value)); + targetAssert=getPC(location,ok); + } + + while(it!=counter_example.object.rend()) + { + const jsont &pc_object=it->second["location"]; + if (pc_object.kind==jsont::J_NULL) continue; + unsigned location=integer2unsigned(string2integer(pc_object.value)); + goto_programt::const_targett pc=getPC(location,ok); + if (!ok) continue; + const jsont &lhs_object=it->second["lhs"]; + if (lhs_object.kind==jsont::J_NULL) continue; + irep_idt id=lhs_object.value; + const jsont &val_object=it->second["value"]; + if (val_object.kind==jsont::J_NULL) continue; + if(pc->is_other() || pc->is_assign() || pc->is_function_call()) + { + const code_assignt &code_assign=to_code_assign(PC->code); + //TODO: the other and function_call may be different + mp_integer address; + const exprt &lhs=code_assign.lhs(); + exprt value=to_expr(ns, id, val_object.value); + symbol_exprt symbol_expr=to_symbol_expr( + (lhs.id()==ID_member) ? to_member_expr(lhs).symbol() : lhs); + irep_idt id=symbol_expr.get_identifier(); + address=evaluate_address(lhs); + if(address==0) { + address=build_memory_map(id,symbol_expr.type()); + } + std::vector rhs; + evaluate(value,rhs); + assign(address, rhs); + if(lhs.id()==ID_member) + { + address=evaluate_address(symbol_expr); + inputs[id]=get_value(symbol_expr.type(),integer2unsigned(address)); + } + else + { + inputs[id]=value; + } + irep_idt f_id; + if(is_opaque_function(pc,f_id)!=0) + { + // TODO: save/restore the full data structure? + function_inputs[f_id].push_front({ irep_idt(), + { { irep_idt(), inputs[id] } } }); + } + } + it++; + } + prune_inputs(inputs,function_inputs,true); + print_inputs(); + show=true; + stop_on_assertion=true; + } + return input_vars; +} + +/******************************************************************* + Function: get_assigned_symbol + + Inputs: Trace step + + Outputs: Symbol expression that the step assigned to + + Purpose: Looks through memberof expressions etc to find a root symbol. + + \*******************************************************************/ + +static symbol_exprt get_assigned_symbol(const exprt& expr) +{ + if(expr.id() == ID_symbol) + return to_symbol_expr(expr); + + if(expr.id() == ID_member || + expr.id() == ID_dereference || + expr.id() == ID_typecast || + expr.id() == ID_index || + expr.id() == ID_byte_extract_little_endian || + expr.id() == ID_byte_extract_big_endian) + return get_assigned_symbol(expr.op0()); + + // Try to handle opcodes I haven't thought of by looking for the + // only pointer-typed operand: + + const exprt* unique_pointer = 0; + + for(const auto& op : expr.operands()) + { + if(op.type().id() == ID_pointer) + { + if(!unique_pointer) + unique_pointer = &op; + else + { + unique_pointer = 0; + break; + } + } + } + + if(unique_pointer) + return get_assigned_symbol(*unique_pointer); + else + { + std::string error = "Failed to look through '" + as_string(expr.id()) + + "' in get_assigned_symbol."; + throw error; + } +} + +static symbol_exprt get_assigned_symbol(const goto_trace_stept& step) +{ + return get_assigned_symbol(step.full_lhs); +} + +/******************************************************************* + Function: calls_opaque_stub + + Inputs: Call instruction and symbol table + + Outputs: Returns COMPLEX_OPAQUE_STUB if the given instruction + calls a function with a synthetic stub modelling its + behaviour, or SIMPLE_OPAQUE_STUB if it is not available at all, + or NOT_OPAQUE_STUB otherwise. + In the first case, sets capture_symbol to the symbol name + the stub defines. In either stub case, sets f_id to the function + called. + + Purpose: Determine whether a call instruction targets an internal + function or some form of opaque function. + + \*******************************************************************/ + + + +bool calls_opaque_stub(const code_function_callt& callinst, + const symbol_tablet& symbol_table, irep_idt& f_id, irep_idt& capture_symbol) +{ + f_id=callinst.function().get(ID_identifier); + const symbolt& called_func=symbol_table.lookup(f_id); + capture_symbol=called_func.type.get("opaque_method_capture_symbol"); + if(capture_symbol!=irep_idt()) + return true; + else + return false; +} + +/******************************************************************* + Function: get_value_tree + + Inputs: Symbol to capture, map of current symbol ("input") values. + + Outputs: Populates captured with a top-down-ordered list of symbol + values containing every value reachable from capture_symbol. + For example, if capture_symbol contains a pointer to some + object x, captured will be populated with x's value and then + capture_symbol's. + + Purpose: Take a snapshot of state reachable from capture_symbol. + + \*******************************************************************/ + +// Get the current value of capture_symbol plus +// the values of any symbols referenced in its fields. +// Store them in 'captured' in bottom-up order. +void interpretert::get_value_tree(const irep_idt& capture_symbol, + function_assignmentst& captured) +{ + + // Circular reference? + for(auto already_captured : captured) + if(already_captured.id==capture_symbol) + return; + exprt defined=get_value(capture_symbol); + + captured.push_back({capture_symbol, defined}); + + if(defined.type().id()==ID_pointer) + { + get_value_tree(defined,captured); + } + else if(defined.type().id()==ID_struct || + defined.type().id()==ID_array) + { + /* Assumption: all object trees captured this way refer directly + * to particular symex::dynamic_object expressions, which are always + * address-of-symbol constructions.*/ + forall_operands(opit, defined) { + if(opit->type().id()==ID_pointer) + get_value_tree(*opit,captured); + } + } + else + { + // Primitive, just capture this. + } + +} + +void interpretert::get_value_tree(const exprt& capture_expr, + function_assignmentst& captured) +{ + assert(capture_expr.type().id()==ID_pointer); + if(capture_expr!=null_pointer_exprt(to_pointer_type(capture_expr.type()))) + { + const auto& referee=to_symbol_expr( + to_address_of_expr(capture_expr).object()).get_identifier(); + get_value_tree(referee,captured); + } +} + +// Wrapper for above, giving bottom-up ordering +void interpretert::get_value_tree_bu(const irep_idt& capture_symbol, + function_assignmentst& captured) +{ + get_value_tree(capture_symbol,captured); + std::reverse(captured.begin(),captured.end()); +} + + +static bool is_assign_step(const goto_trace_stept& step) +{ + return goto_trace_stept::ASSIGNMENT==step.type + && (step.pc->is_other() || step.pc->is_assign() + || step.pc->is_function_call()); +} + +static bool is_constructor_call(const goto_trace_stept& step, + const symbol_tablet& st) +{ + const auto& call=to_code_function_call(step.pc->code); + const auto& id=call.function().get(ID_identifier); + auto callee_type=st.lookup(id).type; + return callee_type.get_bool(ID_constructor); +} + +struct trace_stack_entry { + irep_idt func_name; + mp_integer this_address; + irep_idt capture_symbol; + bool is_super_call; + std::vector param_values; +}; + +static bool is_super_call(const trace_stack_entry& called, + const trace_stack_entry& caller) +{ + // If either call isn't an instance method, it's not a super call: + if(called.this_address==0 || caller.this_address==0) + return false; + + // If the this-addresses don't match, it's not a super call: + if(called.this_address!=caller.this_address) + return false; + + /* If the names (including class) match entirely, + * this is simply a recursive call:*/ + if(called.func_name == caller.func_name) + return false; + + // Check whether the mangled method names (disregarding class) match: + std::string calleds=as_string(called.func_name); + std::string callers=as_string(caller.func_name); + size_t calledoff=calleds.rfind('.'), calleroff=callers.rfind('.'); + if(calledoff==std::string::npos || calleroff==std::string::npos) + return false; + return calleds.substr(calledoff)==callers.substr(calleroff); +} + +mp_integer interpretert::get_this_address(const code_function_callt& call_code) +{ + if(!to_code_type(call_code.function().type()).has_this()) + return 0; + + std::vector this_address; + assert(call_code.arguments().size()!=0); + evaluate(call_code.arguments()[0],this_address); + if(this_address.size()==0) + { + message->warning() << "Failed to evaluate this-arg for " << + from_expr(ns,"",call_code.function()) << messaget::eom; + return 0; + } + assert(this_address.size()==1); + return this_address[0]; +} + +exprt interpretert::get_value(const irep_idt& id) +{ + // The dynamic type and the static symbol type may differ for VLAs, + // where the symbol carries a size expression and the dynamic type + // registry contains its actual length. + auto findit=dynamic_types.find(id); + typet get_type; + if(findit!=dynamic_types.end()) + get_type=findit->second; + else + get_type=symbol_table.lookup(id).type; + + symbol_exprt symbol_expr(id,get_type); + mp_integer whole_lhs_object_address=evaluate_address(symbol_expr); + + return get_value(get_type,integer2unsigned(whole_lhs_object_address)); +} + +const exprt & get_entry_function(const goto_functionst &gf) +{ + typedef goto_functionst::function_mapt function_mapt; + const function_mapt &fm=gf.function_map; + const irep_idt start(goto_functionst::entry_point()); + const function_mapt::const_iterator entry_func=fm.find(start); + assert(fm.end() != entry_func); + const goto_programt::instructionst &in=entry_func->second.body.instructions; + typedef goto_programt::instructionst::const_reverse_iterator reverse_target; + reverse_target codeit=in.rbegin(); + const reverse_target end=in.rend(); + assert(end != codeit); + // Tolerate 'dead' statements at the end of _start. + while(end!=codeit && codeit->code.get_statement()!=ID_function_call) + ++codeit; + assert(end != codeit); + const reverse_target call=codeit; + const code_function_callt &func_call=to_code_function_call(call->code); + const exprt &func_expr=func_call.function(); + return func_expr; +} + + +/******************************************************************* + Function: load_counter_example_inputs + + Inputs: + + Outputs: + + Purpose: + + \*******************************************************************/ + +interpretert::input_varst& interpretert::load_counter_example_inputs( + const goto_tracet &trace, list_input_varst& function_inputs, + side_effects_differencet &valuesDifference, const bool filtered) +{ + show=false; + stop_on_assertion=false; + + input_varst inputs; + + function=goto_functions.function_map.find(goto_functionst::entry_point()); + if(function==goto_functions.function_map.end()) + throw "main not found"; + + irep_idt previous_assigned_symbol; + + initialise(false); + + // First walk the trace forwards to initialise variable-length arrays + // whose size-expressions depend on context (e.g. int x = 5; int[] y = new int[x];) + // We also take the opportunity to save the results of evaluate_address and evaluate + // such that any non-constant expressions (e.g. the occasional byte_extract(..., i, ...) + // creeps in that needs the current value of local 'i') will be evaluated correctly. + + std::vector > > trace_eval; + std::vector trace_stack; + int outermost_constructor_depth=-1; + int expect_parameter_assignments=0; + + trace_stack.push_back( + {goto_functionst::entry_point(),0,irep_idt(),false,{}}); + + const exprt &func_expr = get_entry_function(goto_functions); + const irep_idt &func_name = to_symbol_expr(func_expr).get_identifier(); + const code_typet::parameterst ¶ms= + to_code_type(func_expr.type()).parameters(); + + std::map parameterSet; + + // mapping -> value + std::map,const exprt> valuesBefore; + + namespacet ns(symbol_table); + + for(const auto &p : params) + parameterSet.insert({id2string(p.get_identifier()), p.get_identifier()}); + + for(auto it=trace.steps.begin(),itend=trace.steps.end();it!=itend;++it) + { + const auto& step=*it; + if(is_assign_step(step)) + { + mp_integer address; + symbol_exprt symbol_expr=get_assigned_symbol(step); + irep_idt id=symbol_expr.get_identifier(); + + #ifdef DEBUG + message->status() << it->pc->function << ": " + << from_expr(ns,"",step.full_lhs) + << " <- " << from_expr(ns,"",step.full_lhs_value) + << messaget::eom; + #endif + + address=evaluate_address(step.full_lhs); + if(address==0) + address=build_memory_map(id,symbol_expr.type()); + + std::vector rhs; + evaluate(step.full_lhs_value,rhs); + if(rhs.size()==0) + { + evaluate(step.full_lhs,rhs); + if(rhs.size()!=0) + { + message->warning() << "symex::build_goto_trace couldn't evaluate this expression, but the interpreter could." << messaget::eom; + } + } + assign(address,rhs); + + if(expect_parameter_assignments!=0) + { + if(!--expect_parameter_assignments) + { + /* Just executed the last parameter assignment for a function + * we just entered. + * Capture the arguments of *every* call as it is entered, + * because we might need them for verification if it happens + * to call a super-method later.*/ + std::vector actual_params; + const auto& this_function=trace_stack.back().func_name; + const auto& formal_params= + to_code_type(symbol_table.lookup(this_function).type).parameters(); + std::vector direct_params; + bool is_constructor= + id2string(this_function).find("")!=std::string::npos; + + for(const auto& fp : formal_params) + { + /* Don't capture 'this' on entering a constructor, as it's + * uninitialised at this point. */ + if(is_constructor && fp.get_this()) + continue; + /* Note this will record the actual parameter values as well as + * anything reachable from them. We use a single actual_params + * list for all parameters to avoid redundancy e.g. if parameters + * or objects reachable from them alias, we only need to capture + * that subtree once.*/ + get_value_tree_bu(fp.get_identifier(),actual_params); + /* Set the actual direct params aside, so we can keep them in + * order at the back.*/ + direct_params.push_back(std::move(actual_params.back())); + actual_params.pop_back(); + } + + // Put the direct params back on the end of the list: + actual_params.insert(actual_params.end(),direct_params.begin(), + direct_params.end()); +#ifdef DEBUG + for(const auto& id_expr : actual_params) + message->status() << "Param " << id_expr.id << " = " << + from_expr(ns,"",id_expr.value) << messaget::eom; +#endif + trace_stack.back().param_values=std::move(actual_params); + + } + } + + trace_eval.push_back(std::make_pair(address, rhs)); + + /********* 8< **********/ + irep_idt identifier=step.lhs_object.get_identifier(); + auto param = parameterSet.find(id2string(identifier)); + if(param != parameterSet.end()) + { + const exprt &expr = step.full_lhs_value; + interpretert::function_assignmentst input_assigns; + get_value_tree(identifier, input_assigns); + for(const auto &assign : input_assigns) + { + const typet &tree_typ = ns.follow(assign.value.type()); + if(tree_typ.id()==ID_struct) + { + const struct_typet &struct_type=to_struct_type(tree_typ); + const struct_typet::componentst &components= + struct_type.components(); + const struct_exprt &struct_expr=to_struct_expr(assign.value); + const auto& ops=struct_expr.operands(); + for(size_t fieldidx=0,fieldlim=ops.size(); + fieldidx!=fieldlim;++fieldidx) + { + const exprt & expr = ops[fieldidx]; + // only look at atomic types for now + if(expr.type().id()==ID_signedbv || + expr.type().id()==ID_c_bool) + { + valuesBefore.insert({{assign.id, + components[fieldidx].get_name()}, expr}); + } + } + } + } + } + /********* 8< **********/ + } + else if(step.is_function_call()) + { + irep_idt called, capture_symbol; + bool is_cons=is_constructor_call(step,symbol_table); + // No need to intercept j.l.O's constructor since we know it doesn't do + // anything visible to the object's state. + // TODO: consider just supplying a constructor for it? + auto is_stub=calls_opaque_stub(to_code_function_call(step.pc->code), + symbol_table,called,capture_symbol); + bool is_jlo_cons=is_cons && + as_string(called).find("java.lang.Object")!=std::string::npos; + + mp_integer this_address= + get_this_address(to_code_function_call(step.pc->code)); + + trace_stack.push_back({called,this_address,irep_idt(),false,{}}); + + assert(expect_parameter_assignments==0 && + "Entered another function before the parameter assignment chain was done?"); + // Capture upcoming parameter assignments: + expect_parameter_assignments= + to_code_type(to_code_function_call(step.pc->code).function().type()).parameters().size(); + + bool is_super=(!is_cons) && trace_stack.size()!=0 && + is_super_call(trace_stack.back(),trace_stack[trace_stack.size()-2]); + trace_stack.back().is_super_call=is_super; + + if((!is_stub) || is_jlo_cons) + { + if(is_cons) + { + if(outermost_constructor_depth==-1) + outermost_constructor_depth=trace_stack.size()-1; + } + else + outermost_constructor_depth=-1; + } + else + { + /* Capture the value of capture_symbol instead of whatever happened + * to have been defined most recently. Also capture any other referenced + * objects. + * Capture after the stub finishes, or in the particular case of a + * constructor that makes opaque super-calls, after the outermost + * constructor finishes.*/ + if(is_cons && outermost_constructor_depth!=-1) + { + assert(outermost_constructor_depth < trace_stack.size()); + trace_stack[outermost_constructor_depth].capture_symbol=capture_symbol; + } + else if(trace_stack.back().is_super_call) + { + /* When a method calls the overridden method, capture the return value + * of the child method, as replacing the supercall is tricky using + * mocking tools. + * We could also consider generating a new method that can be stubbed.*/ + auto findit=trace_stack.rbegin(); + while(findit!=trace_stack.rend() && findit->is_super_call) + ++findit; + assert(findit!=trace_stack.rend()); + assert(findit->capture_symbol==irep_idt() + && "Stub somehow called a super-method?"); + findit->capture_symbol=as_string(findit->func_name)+RETURN_VALUE_SUFFIX; + } + else + trace_stack.back().capture_symbol=capture_symbol; + outermost_constructor_depth=-1; + } + } + else if(step.is_function_return()) + { + outermost_constructor_depth=-1; + assert(trace_stack.size()>=1); + assert(expect_parameter_assignments==0 && + "Exited function before the parameter assignment chain was done?"); + const auto& ret_func=trace_stack.back(); + if(ret_func.capture_symbol!=irep_idt()) + { + assert(trace_stack.size()>=2); + // We must record the value of stub_capture_symbol now. + function_assignmentst defined; + get_value_tree_bu(ret_func.capture_symbol,defined); + if(defined.size()!=0) // Definition found? + { + const auto& caller=trace_stack[trace_stack.size()-2].func_name; + function_inputs[ret_func.func_name].push_back({ + caller,std::move(defined),std::move(trace_stack.back().param_values)}); + } + } + trace_stack.pop_back(); + } + else if(step.type==goto_trace_stept::OUTPUT) + { + for(const auto &inputParam : parameterSet) + { + std::size_t found = (inputParam.first).rfind(id2string(step.io_id)); + if(found!=std::string::npos) + { + /* looping over io_args will ignore atomic types which won't have + * side effects*/ + interpretert::function_assignmentst output_assigns; + get_value_tree(inputParam.second, output_assigns); + const typet &typ = symbol_table.lookup(inputParam.second).type; + for(const auto &assign : output_assigns) + { + const typet &tree_typ = ns.follow(assign.value.type()); + if(tree_typ.id()==ID_struct) + { + const struct_typet &struct_type=to_struct_type(tree_typ); + const struct_typet::componentst &components= + struct_type.components(); + const struct_exprt &struct_expr=to_struct_expr(assign.value); + const auto& ops=struct_expr.operands(); + for(size_t fieldidx=0, fieldlim=ops.size(); + fieldidx!=fieldlim;fieldidx++) + { + const exprt &after_expr = ops[fieldidx]; + if(after_expr.type().id()==ID_signedbv || + after_expr.type().id()==ID_c_bool) + // after_expr.type().id()==ID_string || + // after_expr.type().id()==ID_floatbv) + { + auto findit=valuesBefore.find({assign.id, + components[fieldidx].get_name()}); + if(findit!=valuesBefore.end()) + { + const exprt &before_expr = findit->second; + assert(after_expr.type().id()==before_expr.type().id()); + mp_integer a, b; + to_integer(after_expr, a); + to_integer(before_expr, b); + if (a != b) + { + valuesDifference.insert({{assign.id, + components[fieldidx].get_name()}, + {before_expr, after_expr}}); + } + } + //TODO: decide what to do when a field wasn't reachable before + // (e.g. inaccessible due to a null pointer) + } + } + } + } + } + } + } + } + + // Now walk backwards to find object states on entering 'main'. + // TODO integrate this into the forwards walk as well. + + auto trace_eval_iter=trace_eval.rbegin(); + goto_tracet::stepst::const_reverse_iterator it=trace.steps.rbegin(); + if(it!=trace.steps.rend()) targetAssert=it->pc; + for(;it!=trace.steps.rend();++it) { + if(is_assign_step(*it)) + { + + assert(trace_eval_iter!=trace_eval.rend() && + "Assign steps failed to line up between fw and bw passes?"); + const auto& eval_result=*(trace_eval_iter++); + const auto& address=eval_result.first; + const auto& rhs=eval_result.second; + + assert(address!=0); + assign(address,rhs); + + symbol_exprt symbol_expr=get_assigned_symbol(*it); + irep_idt id=symbol_expr.get_identifier(); + + inputs[id]=get_value(id); + input_first_assignments[id]=it->pc->function; + } + } + + assert(trace_eval_iter==trace_eval.rend() && + "Backward interpreter walk didn't consume all eval entries?"); + + prune_inputs(inputs,function_inputs,filtered); + print_inputs(); + show=true; + stop_on_assertion=true; + return input_vars; +} + +/******************************************************************* Function: interpreter @@ -662,8 +2297,10 @@ Function: interpreter void interpreter( const symbol_tablet &symbol_table, - const goto_functionst &goto_functions) + const goto_functionst &goto_functions, + messaget *message_handler) { - interpretert interpreter(symbol_table, goto_functions); + interpretert interpreter(symbol_table,goto_functions, + message_handler,optionst()); interpreter(); } diff --git a/src/goto-programs/interpreter.h b/src/goto-programs/interpreter.h index 2d9ef8a0569..65cea749aa9 100644 --- a/src/goto-programs/interpreter.h +++ b/src/goto-programs/interpreter.h @@ -9,10 +9,13 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_INTERPRETER_H #define CPROVER_INTERPRETER_H +#include + #include "goto_functions.h" void interpreter( const symbol_tablet &symbol_table, - const goto_functionst &goto_functions); + const goto_functionst &goto_functions, + messaget *); #endif diff --git a/src/goto-programs/interpreter_class.h b/src/goto-programs/interpreter_class.h index 48e23036243..7b28eea103c 100644 --- a/src/goto-programs/interpreter_class.h +++ b/src/goto-programs/interpreter_class.h @@ -3,6 +3,10 @@ #include #include "goto_functions.h" +#include "goto_trace.h" +#include "json_goto_trace.h" +#include "util/message.h" +#include "util/options.h" /*******************************************************************\ @@ -15,26 +19,57 @@ class interpretert { public: + // An assertion that identifier 'id' carries value 'value' in some particular context. + struct function_assignmentt { + irep_idt id; + exprt value; + }; + + // A list of such assignments. + typedef std::vector function_assignmentst; + typedef std::map, + std::pair> side_effects_differencet; + interpretert( const symbol_tablet &_symbol_table, - const goto_functionst &_goto_functions): - symbol_table(_symbol_table), - ns(_symbol_table), + const goto_functionst &_goto_functions, + messaget *_message_handler, + const optionst& options): + symbol_table(_symbol_table), + ns(_symbol_table), goto_functions(_goto_functions) { + message = _message_handler; } void operator()(); friend class simplify_evaluatet; + typedef std::map input_varst; + typedef std::map input_var_functionst; + typedef std::map dynamic_typest; + + // An assignment list annotated with the calling context. + struct function_assignments_contextt { + irep_idt calling_function; + function_assignmentst return_assignments; + function_assignmentst param_assignments; + }; + + // list_input_varst maps function identifiers onto a vector of [name = value] assignments + // per call to that function. + typedef std::list function_assignments_contextst; + typedef std::map > list_input_varst; + typedef hash_map_cont memory_mapt; + protected: const symbol_tablet &symbol_table; const namespacet ns; const goto_functionst &goto_functions; - - typedef hash_map_cont memory_mapt; - memory_mapt memory_map; + messaget *message; + mutable dynamic_typest dynamic_types; + mutable memory_mapt memory_map; class memory_cellt { @@ -42,16 +77,33 @@ class interpretert irep_idt identifier; unsigned offset; mp_integer value; + mutable char initialised; }; typedef std::vector memoryt; - memoryt memory; + mutable memoryt memory; unsigned stack_pointer; void build_memory_map(); void build_memory_map(const symbolt &symbol); + mp_integer build_memory_map(const irep_idt &id,const typet &type) const; + typet concretise_type(const typet &type) const; unsigned get_size(const typet &type) const; + + irep_idt get_component_id(const irep_idt &object,unsigned offset); +public: + typet get_type(const irep_idt &id) const; + exprt get_value(const typet &type,unsigned offset=0,bool use_non_det = false); + exprt get_value(const typet &type,std::vector &rhs,unsigned offset=0); + exprt get_value(const irep_idt &id); + void get_value_tree(const irep_idt& capture_symbol, function_assignmentst& captured); + void get_value_tree_bu(const irep_idt& capture_symbol, function_assignmentst& captured); + void get_value_tree(const exprt& capture_expr, function_assignmentst& captured); + mp_integer get_this_address(const code_function_callt&); + char is_opaque_function(const goto_programt::instructionst::const_iterator &it,irep_idt &function_id); + + void step(); void execute_assert(); @@ -61,6 +113,11 @@ class interpretert void execute_function_call(); void execute_other(); void execute_decl(); + void clear_input_flags(); + + void allocate( + mp_integer address, + unsigned size); void assign( mp_integer address, @@ -81,14 +138,26 @@ class interpretert memory_mapt local_map; unsigned old_stack_pointer; }; - + typedef std::stack call_stackt; - call_stackt call_stack; + + call_stackt call_stack; + input_varst input_vars; + input_var_functionst input_first_assignments; + list_input_varst function_input_vars; goto_functionst::function_mapt::const_iterator function; - goto_programt::const_targett PC, next_PC; + goto_programt::const_targett PC, next_PC,targetAssert; + goto_tracet steps; bool done; - + bool show; + bool stop_on_assertion; + size_t num_steps; + size_t total_steps; + mutable int num_dynamic_objects; + size_t stack_depth; + int thread_id; + bool evaluate_boolean(const exprt &expr) const { std::vector v; @@ -97,11 +166,43 @@ class interpretert return v.front()!=0; } + bool extract_member_at( + std::vector::iterator& source_iter, + const std::vector::iterator source_end, + const typet& source_type, + mp_integer offset, + const typet& target_type, + std::vector &dest, + bool should_return_this) const; + + bool get_cell_byte_offset( + const typet& source_type, + mp_integer& cell_offset, + mp_integer& result) const; + void evaluate( const exprt &expr, std::vector &dest) const; - mp_integer evaluate_address(const exprt &expr) const; + mp_integer evaluate_address(const exprt &expr, bool fail_quietly=false) const; + void initialise(bool init); void show_state(); + + void list_inputs(bool use_non_det = false); + void list_inputs(input_varst &inputs); + void fill_inputs(input_varst &inputs); + void list_non_bodied(); + void list_non_bodied(const goto_programt::instructionst &instructions); + void print_inputs(); + void print_memory(bool input_flags); + + goto_programt::const_targett getPC(const unsigned location,bool &ok); + void prune_inputs(input_varst &inputs,list_input_varst& function_inputs, const bool filter); + + public: + input_varst& load_counter_example_inputs(const std::string &filename); + input_varst& load_counter_example_inputs(const goto_tracet &trace, list_input_varst& opaque_function_returns, side_effects_differencet &, const bool filtered=false); + const input_var_functionst& get_input_first_assignments() { return input_first_assignments; } + const dynamic_typest& get_dynamic_types() { return dynamic_types; } }; diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp index 97f041fd614..a5af374a1de 100644 --- a/src/goto-programs/interpreter_evaluate.cpp +++ b/src/goto-programs/interpreter_evaluate.cpp @@ -8,22 +8,26 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include +#include +#include #include "interpreter_class.h" /*******************************************************************\ -Function: interpretert::evaluate +Function: interpretert::read Inputs: Outputs: - Purpose: + Purpose: reads a memory address and loads it into the dest variable + marks cell as read before written if cell has never been written \*******************************************************************/ @@ -36,8 +40,11 @@ void interpretert::read( { mp_integer value; - if(address0) cell.initialised=0; + } +} + + +/*******************************************************************\ + +Function: interpretert::extract_member_at + + Inputs: + + Outputs: + + Purpose: +// Side-effect: moves source_iter forwards +// appropriately to the types it walks over. + +// Seems quite likely there's another recursion over datatypes that this +// could be merged with, but haven't found an ideal candidate yet. + +\*******************************************************************/ + +bool interpretert::extract_member_at( + std::vector::iterator& source_iter, + const std::vector::iterator source_end, + const typet& source_type, + mp_integer offset, + const typet& target_type, + std::vector &dest, + bool should_return_this) const +{ + // Should allow any primitive reinterpretation here. + bool return_this = should_return_this || + (offset==0 && + (source_type==target_type || + (source_type.id()==ID_pointer && target_type.id()==ID_pointer))); + + if(source_type.id()==ID_struct) + { + const auto& st=to_struct_type(source_type); + const struct_typet::componentst &components=st.components(); + member_offset_iterator offsets(st,ns); + while(offsets->firstsecond!=-1 + && offsets->second<=offset) + { + if(!extract_member_at(source_iter,source_end, + components[offsets->first].type(), + offset-offsets->second, + target_type,dest,return_this)) + return false; + ++offsets; + } + if(offsets->second==-1) + return false; + } + else if(source_type.id()==ID_array) + { + const auto& at=to_array_type(source_type); + std::vector array_size_vec; + evaluate(at.size(),array_size_vec); + if(array_size_vec.size()!=1) + return false; + mp_integer array_size=array_size_vec[0]; + mp_integer elem_size=pointer_offset_size(at.subtype(),ns); + if(elem_size==-1) + return false; + mp_integer array_idx=0; + while(offset>=0 && array_idx < array_size) + { + if(!extract_member_at(source_iter,source_end,at.subtype(), + offset,target_type,dest,return_this)) + return false; + offset-=elem_size; + ++array_idx; + } + } + else + { + if(return_this) + { + assert(source_iter!=source_end); + dest.push_back(*source_iter); + } + ++source_iter; + } + + return true; + +} + +/*******************************************************************\ + +Function: interpretert::get_cell_byte_offset + + Inputs: + + Outputs: + + Purpose: used for evaluating byte-extract op-codes + +\*******************************************************************/ + +bool interpretert::get_cell_byte_offset( + const typet& source_type, + mp_integer& cell_offset, + mp_integer& result) const +{ + if(source_type.id()==ID_struct) + { + const auto& st=to_struct_type(source_type); + const struct_typet::componentst &components=st.components(); + member_offset_iterator offsets(st,ns); + while(offsets->firstsecond!=-1) + { + if(!get_cell_byte_offset(components[offsets->first].type(), + cell_offset,result)) + { + if(result!=-1) + result+=offsets->second; + return false; + } + ++offsets; + } + if(offsets->second==-1) + { + result=-1; + return false; + } + } + else if(source_type.id()==ID_array) + { + const auto& at=to_array_type(source_type); + mp_integer elem_size=pointer_offset_size(at.subtype(),ns); + if(elem_size==-1) + { + result=-1; + return false; + } + if(at.size().id()!=ID_constant) + return false; + const auto& array_size_expr=to_constant_expr(at.size()); + mp_integer array_size; + if(to_integer(array_size_expr,array_size)) + { + result=-1; + return false; + } + + mp_integer array_idx; + while(cell_offset>=0 && array_idxtype().id()==ID_code) continue; + + unsigned sub_size=get_size(it->type()); + if(sub_size==0) continue; + + std::vector tmp; + evaluate(*it, tmp); + + if(tmp.size()==sub_size) + { + for(unsigned i=0; iwarning() << "string decoding not fully implemented " + << length << messaget::eom; + mp_integer tmp=value.get_no(); + dest.push_back(tmp); + return; + } else { mp_integer i; @@ -124,6 +410,167 @@ void interpretert::evaluate( dest.clear(); } + else if(expr.id()==ID_side_effect) + { + side_effect_exprt side_effect=to_side_effect_expr(expr); + if(side_effect.get_statement()==ID_nondet) + { + if (show) message->error() << "nondet not implemented" << messaget::eom; + return; + } + else if(side_effect.get_statement()==ID_malloc) + { + if (show) message->error() << "malloc not fully implemented " + << expr.type().subtype().pretty() + << messaget::eom; + std::stringstream buffer; + num_dynamic_objects++; + buffer <<"interpreter::malloc_object" << num_dynamic_objects; + irep_idt id(buffer.str().c_str()); + mp_integer address=build_memory_map(id,expr.type().subtype()); + //TODO: check array of type + dest.push_back(address); + return; + } + if (show) message->error() << "side effect not implemented " + << side_effect.get_statement() + << messaget::eom; + } + else if(expr.id()==ID_bitor) + { + if(expr.operands().size()<2) + throw id2string(expr.id())+" expects at least two operands"; + + mp_integer final=0; + forall_operands(it, expr) + { + std::vector tmp; + evaluate(*it, tmp); + if(tmp.size()==1) final=bitwise_or(final,tmp.front()); + } + dest.push_back(final); + return; + } + else if(expr.id()==ID_bitand) + { + if(expr.operands().size()<2) + throw id2string(expr.id())+" expects at least two operands"; + + mp_integer final=-1; + forall_operands(it, expr) + { + std::vector tmp; + evaluate(*it, tmp); + if(tmp.size()==1) final=bitwise_and(final,tmp.front()); + } + dest.push_back(final); + return; + } + else if(expr.id()==ID_bitxor) + { + if(expr.operands().size()<2) + throw id2string(expr.id())+" expects at least two operands"; + + mp_integer final=0; + forall_operands(it, expr) + { + std::vector tmp; + evaluate(*it, tmp); + if(tmp.size()==1) final=bitwise_xor(final,tmp.front()); + } + dest.push_back(final); + return; + } + else if(expr.id()==ID_bitnot) + { + if(expr.operands().size()!=1) + throw id2string(expr.id())+" expects one operand"; + std::vector tmp; + evaluate(expr.op0(), tmp); + if(tmp.size()==1) + { + dest.push_back(bitwise_neg(tmp.front())); + return; + } + } + else if(expr.id()==ID_shl) + { + if(expr.operands().size()!=2) + throw id2string(expr.id())+" expects two operands"; + + std::vector tmp0, tmp1; + evaluate(expr.op0(), tmp0); + evaluate(expr.op1(), tmp1); + if(tmp0.size()==1 && tmp1.size()==1) + { + mp_integer final=logic_left_shift(tmp0.front(),tmp1.front(), + get_size(expr.op0().type())); + dest.push_back(final); + return; + } + } + else if((expr.id()==ID_shr) || (expr.id()==ID_lshr)) + { + if(expr.operands().size()!=2) + throw id2string(expr.id())+" expects two operands"; + + std::vector tmp0, tmp1; + evaluate(expr.op0(), tmp0); + evaluate(expr.op1(), tmp1); + if(tmp0.size()==1 && tmp1.size()==1) + { + mp_integer final=logic_right_shift(tmp0.front(),tmp1.front(), + get_size(expr.op0().type())); + dest.push_back(final); + return; + } + } + else if(expr.id()==ID_ashr) + { + if(expr.operands().size()!=2) + throw id2string(expr.id())+" expects two operands"; + + std::vector tmp0, tmp1; + evaluate(expr.op0(), tmp0); + evaluate(expr.op1(), tmp1); + if(tmp0.size()==1 && tmp1.size()==1) + { + dest.push_back(tmp0.front()/power(2, tmp1.front())); + return; + } + } + else if(expr.id()==ID_ror) + { + if(expr.operands().size()!=2) + throw id2string(expr.id())+" expects two operands"; + + std::vector tmp0, tmp1; + evaluate(expr.op0(), tmp0); + evaluate(expr.op1(), tmp1); + if(tmp0.size()==1 && tmp1.size()==1) + { + mp_integer final=rotate_right(tmp0.front(),tmp1.front(), + get_size(expr.op0().type())); + dest.push_back(final); + return; + } + } + else if(expr.id()==ID_rol) + { + if(expr.operands().size()!=2) + throw id2string(expr.id())+" expects two operands"; + + std::vector tmp0, tmp1; + evaluate(expr.op0(), tmp0); + evaluate(expr.op1(), tmp1); + if(tmp0.size()==1 && tmp1.size()==1) + { + mp_integer final=rotate_left(tmp0.front(),tmp1.front(), + get_size(expr.op0().type())); + dest.push_back(final); + return; + } + } else if(expr.id()==ID_equal || expr.id()==ID_notequal || expr.id()==ID_le || @@ -187,20 +634,20 @@ void interpretert::evaluate( if(expr.operands().size()!=3) throw "if expects three operands"; - std::vector tmp0, tmp1, tmp2; + std::vector tmp0, tmp1; evaluate(expr.op0(), tmp0); - evaluate(expr.op1(), tmp1); - evaluate(expr.op2(), tmp2); - if(tmp0.size()==1 && tmp1.size()==1 && tmp2.size()==1) + if(tmp0.size()==1) { - const mp_integer &op0=tmp0.front(); - const mp_integer &op1=tmp1.front(); - const mp_integer &op2=tmp2.front(); - - dest.push_back(op0!=0?op1:op2); + if(tmp0.front()!=0) + evaluate(expr.op1(), tmp1); + else + evaluate(expr.op2(), tmp1); } + if(tmp1.size()==1) + dest.push_back(tmp1.front()); + return; } else if(expr.id()==ID_and) @@ -352,19 +799,115 @@ void interpretert::evaluate( { if(expr.operands().size()!=1) throw "address_of expects one operand"; - dest.push_back(evaluate_address(expr.op0())); return; } + else if(expr.id()==ID_pointer_offset) + { + if(expr.operands().size()!=1) + throw "pointer_offset expects one operand"; + if(expr.op0().type().id()!=ID_pointer) + throw "pointer_offset expects a pointer operand"; + std::vector result; + evaluate(expr.op0(),result); + if(result.size()==1) + { + // Return the distance, in bytes, between the address returned + // and the beginning of the underlying object. + mp_integer address=result[0]; + if(address > 0 && address < memory.size()) + { + const auto& memory_record=memory[integer2unsigned(address)]; + auto obj_type=get_type(memory_record.identifier); + + mp_integer offset=memory_record.offset; + mp_integer byte_offset=-1; + get_cell_byte_offset(obj_type,offset,byte_offset); + if(byte_offset!=-1) + dest.push_back(byte_offset); + } + } + return; + } + else if(expr.id()==ID_byte_extract_little_endian || + expr.id()==ID_byte_extract_big_endian) + { + if(expr.operands().size()!=2) + throw "byte_extract should have two operands"; + std::vector extract_offset; + evaluate(expr.op1(),extract_offset); + std::vector extract_from; + evaluate(expr.op0(),extract_from); + if(extract_offset.size()==1 && extract_from.size()!=0) + { + const typet& target_type=expr.type(); + auto extract_from_iter=extract_from.begin(); + + if(extract_member_at(extract_from_iter,extract_from.end(), + expr.op0().type(),extract_offset[0], + target_type,dest,false) + && dest.size()!=0) { + return; + } + } + } else if(expr.id()==ID_dereference || expr.id()==ID_index || expr.id()==ID_symbol || expr.id()==ID_member) { - mp_integer a=evaluate_address(expr); - dest.resize(get_size(expr.type())); - read(a, dest); - return; + mp_integer a=evaluate_address(expr, /*fail quietly=*/true); + if(a.is_zero() && expr.id()==ID_index) + { + // Try reading from a constant array: + std::vector idx; + evaluate(expr.op1(),idx); + if(idx.size()==1) + { + mp_integer read_from_index=idx[0]; + if(expr.op0().id()==ID_array) + { + const auto& ops=expr.op0().operands(); + assert(read_from_index.is_long()); + if(read_from_index >= 0 && read_from_index < ops.size()) + { + evaluate(ops[read_from_index.to_long()],dest); + if(dest.size()!=0) + return; + } + } + else if(expr.op0().id()=="array-list") + { + // This sort of construct comes from boolbv_get, but doesn't seem + // to have an exprt yet. Its operands are a list of key-value pairs. + const auto& ops=expr.op0().operands(); + assert(ops.size() % 2 == 0); + for(size_t listidx=0,listlim=ops.size();listidx!=listlim; listidx+=2) + { + std::vector elem_idx; + evaluate(ops[listidx],elem_idx); + assert(elem_idx.size()==1); + if(elem_idx[0]==read_from_index) + { + evaluate(ops[listidx+1],dest); + if(dest.size()!=0) + return; + else + break; + } + } + // If we fall out the end of this loop then the constant array-list + // didn't define an element matching the index we're looking for. + } + } + evaluate_address(expr); // Evaluate again to print error message. + } + else if(!a.is_zero()) + { + dest.resize(get_size(expr.type())); + read(a, dest); + return; + } } else if(expr.id()==ID_typecast) { @@ -397,31 +940,31 @@ void interpretert::evaluate( dest.push_back(binary2integer(s, false)); return; } - else if(expr.type().id()==ID_bool) + else if((expr.type().id()==ID_bool)||(expr.type().id()==ID_c_bool)) { dest.push_back(value!=0); return; } } } - else if(expr.id()==ID_ashr) + else if ((expr.id()==ID_array) || (expr.id()==ID_array_of)) { - if(expr.operands().size()!=2) - throw "ashr expects two operands"; - - std::vector tmp0, tmp1; - evaluate(expr.op0(), tmp0); - evaluate(expr.op1(), tmp1); - - if(tmp0.size()==1 && tmp1.size()==1) - dest.push_back(tmp0.front()/power(2, tmp1.front())); - + forall_operands(it,expr) { + evaluate(*it,dest); + } return; } - - std::cout << "!! failed to evaluate expression: " + else if (expr.id()==ID_nil) + { + dest.push_back(0); + return; + } +// if (!show) return; + message->error() << "!! failed to evaluate expression: " << from_expr(ns, function->first, expr) - << std::endl; + << messaget::eom; + message->error() << expr.id() << "[" << expr.type().id() << "]" + << messaget::eom; } /*******************************************************************\ @@ -436,18 +979,21 @@ Function: interpretert::evaluate_address \*******************************************************************/ -mp_integer interpretert::evaluate_address(const exprt &expr) const +mp_integer interpretert::evaluate_address(const exprt &expr, + bool fail_quietly) const { if(expr.id()==ID_symbol) { - const irep_idt &identifier=expr.get(ID_identifier); - + const irep_idt &identifier= + is_ssa_expr(expr) ? + to_ssa_expr(expr).get_original_name() : + expr.get(ID_identifier); + interpretert::memory_mapt::const_iterator m_it1= memory_map.find(identifier); - - if(m_it1!=memory_map.end()) - return m_it1->second; + if(m_it1!=memory_map.end()) return m_it1->second; + if(!call_stack.empty()) { interpretert::memory_mapt::const_iterator m_it2= @@ -456,6 +1002,10 @@ mp_integer interpretert::evaluate_address(const exprt &expr) const if(m_it2!=call_stack.top().local_map.end()) return m_it2->second; } + mp_integer address=memory.size(); + build_memory_map(to_symbol_expr(expr).get_identifier(),expr.type()); + return address; + } else if(expr.id()==ID_dereference) { @@ -477,7 +1027,11 @@ mp_integer interpretert::evaluate_address(const exprt &expr) const evaluate(expr.op1(), tmp1); if(tmp1.size()==1) - return evaluate_address(expr.op0())+tmp1.front(); + { + auto base=evaluate_address(expr.op0(),fail_quietly); + if(!base.is_zero()) + return base+tmp1.front(); + } } else if(expr.id()==ID_member) { @@ -506,12 +1060,55 @@ mp_integer interpretert::evaluate_address(const exprt &expr) const offset+=get_size(it->type()); } - return evaluate_address(expr.op0())+offset; + auto base=evaluate_address(expr.op0(),fail_quietly); + if(!base.is_zero()) + return base+offset; + } + else if(expr.id()==ID_byte_extract_little_endian || + expr.id()==ID_byte_extract_big_endian) + { + if(expr.operands().size()!=2) + throw "byte_extract should have two operands"; + std::vector extract_offset; + evaluate(expr.op1(),extract_offset); + std::vector extract_from; + evaluate(expr.op0(),extract_from); + if(extract_offset.size()==1 && extract_from.size()!=0) + { + const typet& target_type=expr.type(); + auto extract_from_iter=extract_from.begin(); + std::vector dest; + + /* Side-effect of extract_member_at: moves extract_from_iter to point + * after the extracted members.*/ + if(extract_member_at(extract_from_iter,extract_from.end(), + expr.op0().type(),extract_offset[0], + target_type,dest,false) + && dest.size()!=0) { + mp_integer walked_over_addresses= + std::distance(extract_from.begin(),extract_from_iter); + // Give address of first relevant cell. + walked_over_addresses-=dest.size(); + return evaluate_address(expr.op0(),fail_quietly)+walked_over_addresses; + } + } + } + else if(expr.id()==ID_if) + { + std::vector result; + if_exprt address_cond(expr.op0(), + address_of_exprt(expr.op1()), + address_of_exprt(expr.op2())); + evaluate(address_cond,result); + if(result.size()==1) + return result[0]; + } + if(!fail_quietly) + { + message->error() << "!! failed to evaluate address: " + << from_expr(ns, function->first, expr) + << messaget::eom; } - - std::cout << "!! failed to evaluate address: " - << from_expr(ns, function->first, expr) - << std::endl; return 0; } From ea882041174b8cdc117e1fe195facb4ff53083d9 Mon Sep 17 00:00:00 2001 From: Dario Cattaruzza Date: Thu, 10 Nov 2016 13:08:33 +0000 Subject: [PATCH 7/9] Interpreter class header guards Avoid crash from infinite array size --- src/goto-programs/interpreter_class.h | 5 +++++ src/goto-programs/interpreter_evaluate.cpp | 8 ++++++++ 2 files changed, 13 insertions(+) diff --git a/src/goto-programs/interpreter_class.h b/src/goto-programs/interpreter_class.h index 7b28eea103c..5ef120a5ccb 100644 --- a/src/goto-programs/interpreter_class.h +++ b/src/goto-programs/interpreter_class.h @@ -1,3 +1,6 @@ +#ifndef INTERPRETER_CLASSH +#define INTERPRETER_CLASSH + #include #include @@ -206,3 +209,5 @@ class interpretert const input_var_functionst& get_input_first_assignments() { return input_first_assignments; } const dynamic_typest& get_dynamic_types() { return dynamic_types; } }; + +#endif diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp index a5af374a1de..b8f3ae46c82 100644 --- a/src/goto-programs/interpreter_evaluate.cpp +++ b/src/goto-programs/interpreter_evaluate.cpp @@ -959,6 +959,14 @@ void interpretert::evaluate( dest.push_back(0); return; } + else if(expr.id()==ID_infinity) + { + if(expr.type().id()==ID_signedbv) + { + message->error() << "Infinite size arrays not supported" << messaget::eom; + return; + } + } // if (!show) return; message->error() << "!! failed to evaluate expression: " << from_expr(ns, function->first, expr) From 25e429f284205264e6d8da3630f183eadbe7d9f7 Mon Sep 17 00:00:00 2001 From: Dario Cattaruzza Date: Thu, 10 Nov 2016 13:27:03 +0000 Subject: [PATCH 8/9] _H for header guards --- src/goto-programs/interpreter_class.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/goto-programs/interpreter_class.h b/src/goto-programs/interpreter_class.h index 5ef120a5ccb..e95d997989b 100644 --- a/src/goto-programs/interpreter_class.h +++ b/src/goto-programs/interpreter_class.h @@ -1,5 +1,5 @@ -#ifndef INTERPRETER_CLASSH -#define INTERPRETER_CLASSH +#ifndef INTERPRETER_CLASS_H +#define INTERPRETER_CLASS_H #include From caca1d2fbfea2a1829f0a8804657acdfa3c8d293 Mon Sep 17 00:00:00 2001 From: Dario Cattaruzza Date: Thu, 24 Nov 2016 10:57:37 +0000 Subject: [PATCH 9/9] avoid throw in non-bodied function parameters and output (other) instruction --- src/goto-programs/interpreter.cpp | 185 ++++++++++++++++++-------- src/goto-programs/interpreter_class.h | 2 + 2 files changed, 128 insertions(+), 59 deletions(-) diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index e03ef8b8f79..885662c75de 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -112,6 +112,37 @@ void interpretert::initialise(bool init) { /*******************************************************************\ +/*******************************************************************\ + +Function: interpretert::get_is_variable_cprover + + Inputs: The cell to check for a CPROVER variable + + Outputs: True if the variable stored in the given cell is a CPROVER variable + + Purpose: To check a given cell for being a CPROVER variable + +\*******************************************************************/ +bool interpretert::get_is_variable_cprover( + const irep_idt &variable_id) +{ + constexpr char const *cprover_variable_prefix = "__CPROVER"; + constexpr int cprover_prefix_len = strlen(cprover_variable_prefix); + + const char *cell_identifier = variable_id.c_str(); + + if(strncmp(cell_identifier, cprover_variable_prefix, cprover_prefix_len) == 0) + { + return true; + } + else + { + return false; + } +} + +/*******************************************************************\ + Function: interpretert::show_state Inputs: @@ -491,6 +522,10 @@ void interpretert::execute_other() assign(address, rhs); } } + else if(statement==ID_output) + { + return; + } else throw "unexpected OTHER statement: "+id2string(statement); } @@ -1352,8 +1387,10 @@ void interpretert::list_inputs(bool use_non_det) { const memory_cellt &cell=memory[i]; if(cell.initialised>=0) continue; - if(strncmp(cell.identifier.c_str(), "__CPROVER", 9)==0) + if(get_is_variable_cprover(cell.identifier)) + { continue; + } try { typet symbol_type=get_type(cell.identifier); @@ -1400,7 +1437,12 @@ void interpretert::list_inputs(input_varst &inputs) { for(unsigned long i=0;i=0) continue; - if (strncmp(cell.identifier.c_str(), "__CPROVER", 9)==0) continue; + + if(get_is_variable_cprover(cell.identifier)) + { + continue; + } + if(inputs.find(cell.identifier)!=inputs.end()) { input_vars[cell.identifier]=inputs[cell.identifier]; @@ -1440,10 +1482,16 @@ void interpretert::list_inputs(input_varst &inputs) { void interpretert::print_inputs() { if(input_vars.size()<=0) list_inputs(); - for(input_varst::iterator it=input_vars.begin();it!=input_vars.end(); + + print_inputs(input_vars); +} + +void interpretert::print_inputs(const interpretert::input_varst &inputs) const +{ + for(input_varst::const_iterator it=inputs.begin();it!=inputs.end(); it++) { - message->result() << it->first << "=" - << from_expr(ns, it->first, it->second) << "[" + message->result() << it->first << "=" + << from_expr(ns, it->first, it->second) << "[" << it->second.type().id() << "]" << messaget::eom; } message->result() << messaget::eom; @@ -1539,6 +1587,7 @@ void interpretert::prune_inputs(input_varst &inputs, } input_vars=inputs; function_input_vars=function_inputs; + if(filter) { try @@ -1970,7 +2019,7 @@ interpretert::input_varst& interpretert::load_counter_example_inputs( const code_typet::parameterst ¶ms= to_code_type(func_expr.type()).parameters(); - std::map parameterSet; + std::map parameter_set; // mapping -> value std::map,const exprt> valuesBefore; @@ -1978,7 +2027,7 @@ interpretert::input_varst& interpretert::load_counter_example_inputs( namespacet ns(symbol_table); for(const auto &p : params) - parameterSet.insert({id2string(p.get_identifier()), p.get_identifier()}); + parameter_set.insert({id2string(p.get_identifier()), p.get_identifier()}); for(auto it=trace.steps.begin(),itend=trace.steps.end();it!=itend;++it) { @@ -2064,10 +2113,10 @@ interpretert::input_varst& interpretert::load_counter_example_inputs( /********* 8< **********/ irep_idt identifier=step.lhs_object.get_identifier(); - auto param = parameterSet.find(id2string(identifier)); - if(param != parameterSet.end()) + auto param = parameter_set.find(id2string(identifier)); + if(param != parameter_set.end()) { - const exprt &expr = step.full_lhs_value; + //const exprt &expr = step.full_lhs_value; interpretert::function_assignmentst input_assigns; get_value_tree(identifier, input_assigns); for(const auto &assign : input_assigns) @@ -2101,17 +2150,18 @@ interpretert::input_varst& interpretert::load_counter_example_inputs( { irep_idt called, capture_symbol; bool is_cons=is_constructor_call(step,symbol_table); + const code_function_callt &function_call= + to_code_function_call(step.pc->code); + // No need to intercept j.l.O's constructor since we know it doesn't do // anything visible to the object's state. // TODO: consider just supplying a constructor for it? - auto is_stub=calls_opaque_stub(to_code_function_call(step.pc->code), + auto is_stub=calls_opaque_stub(function_call, symbol_table,called,capture_symbol); bool is_jlo_cons=is_cons && as_string(called).find("java.lang.Object")!=std::string::npos; - mp_integer this_address= - get_this_address(to_code_function_call(step.pc->code)); - + mp_integer this_address=get_this_address(function_call); trace_stack.push_back({called,this_address,irep_idt(),false,{}}); assert(expect_parameter_assignments==0 && @@ -2119,6 +2169,24 @@ interpretert::input_varst& interpretert::load_counter_example_inputs( // Capture upcoming parameter assignments: expect_parameter_assignments= to_code_type(to_code_function_call(step.pc->code).function().type()).parameters().size(); + + // function to be called + mp_integer a=evaluate_address(function_call.function()); + + if((expect_parameter_assignments>0) && (a>0) && (asecond.body_available()) + { + message->warning() << "Call to non-bodied function expecting parameters ignored" + << messaget::eom; + expect_parameter_assignments=0; + } + } + + bool is_super=(!is_cons) && trace_stack.size()!=0 && is_super_call(trace_stack.back(),trace_stack[trace_stack.size()-2]); @@ -2126,44 +2194,44 @@ interpretert::input_varst& interpretert::load_counter_example_inputs( if((!is_stub) || is_jlo_cons) { - if(is_cons) - { - if(outermost_constructor_depth==-1) - outermost_constructor_depth=trace_stack.size()-1; - } - else - outermost_constructor_depth=-1; + if(is_cons) + { + if(outermost_constructor_depth==-1) + outermost_constructor_depth=trace_stack.size()-1; + } + else + outermost_constructor_depth=-1; } else { - /* Capture the value of capture_symbol instead of whatever happened - * to have been defined most recently. Also capture any other referenced - * objects. - * Capture after the stub finishes, or in the particular case of a - * constructor that makes opaque super-calls, after the outermost - * constructor finishes.*/ - if(is_cons && outermost_constructor_depth!=-1) - { - assert(outermost_constructor_depth < trace_stack.size()); - trace_stack[outermost_constructor_depth].capture_symbol=capture_symbol; - } - else if(trace_stack.back().is_super_call) - { - /* When a method calls the overridden method, capture the return value - * of the child method, as replacing the supercall is tricky using - * mocking tools. - * We could also consider generating a new method that can be stubbed.*/ - auto findit=trace_stack.rbegin(); - while(findit!=trace_stack.rend() && findit->is_super_call) - ++findit; - assert(findit!=trace_stack.rend()); - assert(findit->capture_symbol==irep_idt() + /* Capture the value of capture_symbol instead of whatever happened + * to have been defined most recently. Also capture any other referenced + * objects. + * Capture after the stub finishes, or in the particular case of a + * constructor that makes opaque super-calls, after the outermost + * constructor finishes.*/ + if(is_cons && outermost_constructor_depth!=-1) + { + assert(outermost_constructor_depth < trace_stack.size()); + trace_stack[outermost_constructor_depth].capture_symbol=capture_symbol; + } + else if(trace_stack.back().is_super_call) + { + /* When a method calls the overridden method, capture the return value + * of the child method, as replacing the supercall is tricky using + * mocking tools. + * We could also consider generating a new method that can be stubbed.*/ + auto findit=trace_stack.rbegin(); + while(findit!=trace_stack.rend() && findit->is_super_call) + ++findit; + assert(findit!=trace_stack.rend()); + assert(findit->capture_symbol==irep_idt() && "Stub somehow called a super-method?"); - findit->capture_symbol=as_string(findit->func_name)+RETURN_VALUE_SUFFIX; - } - else - trace_stack.back().capture_symbol=capture_symbol; - outermost_constructor_depth=-1; + findit->capture_symbol=as_string(findit->func_name)+RETURN_VALUE_SUFFIX; + } + else + trace_stack.back().capture_symbol=capture_symbol; + outermost_constructor_depth=-1; } } else if(step.is_function_return()) @@ -2176,21 +2244,21 @@ interpretert::input_varst& interpretert::load_counter_example_inputs( if(ret_func.capture_symbol!=irep_idt()) { assert(trace_stack.size()>=2); - // We must record the value of stub_capture_symbol now. - function_assignmentst defined; - get_value_tree_bu(ret_func.capture_symbol,defined); - if(defined.size()!=0) // Definition found? - { - const auto& caller=trace_stack[trace_stack.size()-2].func_name; - function_inputs[ret_func.func_name].push_back({ - caller,std::move(defined),std::move(trace_stack.back().param_values)}); - } + // We must record the value of stub_capture_symbol now. + function_assignmentst defined; + get_value_tree_bu(ret_func.capture_symbol,defined); + if(defined.size()!=0) // Definition found? + { + const auto& caller=trace_stack[trace_stack.size()-2].func_name; + function_inputs[ret_func.func_name].push_back({ + caller,std::move(defined),std::move(trace_stack.back().param_values)}); + } } trace_stack.pop_back(); } else if(step.type==goto_trace_stept::OUTPUT) { - for(const auto &inputParam : parameterSet) + for(const auto &inputParam : parameter_set) { std::size_t found = (inputParam.first).rfind(id2string(step.io_id)); if(found!=std::string::npos) @@ -2199,7 +2267,6 @@ interpretert::input_varst& interpretert::load_counter_example_inputs( * side effects*/ interpretert::function_assignmentst output_assigns; get_value_tree(inputParam.second, output_assigns); - const typet &typ = symbol_table.lookup(inputParam.second).type; for(const auto &assign : output_assigns) { const typet &tree_typ = ns.follow(assign.value.type()); diff --git a/src/goto-programs/interpreter_class.h b/src/goto-programs/interpreter_class.h index e95d997989b..7f5284e1728 100644 --- a/src/goto-programs/interpreter_class.h +++ b/src/goto-programs/interpreter_class.h @@ -192,12 +192,14 @@ class interpretert void initialise(bool init); void show_state(); + static bool get_is_variable_cprover(const irep_idt &variable_id); void list_inputs(bool use_non_det = false); void list_inputs(input_varst &inputs); void fill_inputs(input_varst &inputs); void list_non_bodied(); void list_non_bodied(const goto_programt::instructionst &instructions); void print_inputs(); + void print_inputs(const input_varst &inputs) const; void print_memory(bool input_flags); goto_programt::const_targett getPC(const unsigned location,bool &ok);