@@ -887,7 +887,9 @@ void interpretert::execute_function_call()
887887 if (it!=function_input_vars.end ())
888888 {
889889 std::vector<mp_integer> value;
890- evaluate (it->second .front (),value);
890+ assert (it->second .size () != 0 );
891+ assert (it->second .front ().assignments .size () != 0 );
892+ evaluate (it->second .front ().assignments .back ().value ,value);
891893 if (return_value_address>0 )
892894 {
893895 assign (return_value_address,value);
@@ -1160,7 +1162,10 @@ void interpretert::list_non_bodied(const goto_programt::instructionst &instructi
11601162 unsigned return_address=integer2unsigned (evaluate_address (code_assign.lhs ()));
11611163 if ((return_address > 0 ) && (return_address<memory.size ()))
11621164 {
1163- function_input_vars[f_id].push_back (get_value (code_assign.lhs ().type (),return_address));
1165+ function_assignmentt retval = {irep_idt (), get_value (code_assign.lhs ().type (),return_address)};
1166+ function_assignmentst defnlist = { retval };
1167+ // Add an actual calling context instead of a blank irep if our caller needs it.
1168+ function_input_vars[f_id].push_back ({irep_idt (), defnlist});
11641169 }
11651170 }
11661171 }
@@ -1375,12 +1380,15 @@ void interpretert::prune_inputs(input_varst &inputs,list_input_varst& function_i
13751380{
13761381 for (list_input_varst::iterator it=function_inputs.begin (); it!=function_inputs.end ();it++) {
13771382 const exprt size=from_integer (it->second .size (), integer_typet ());
1378- array_typet type=array_typet (it->second .front ().type (),size);
1383+ assert (it->second .front ().assignments .size () != 0 );
1384+ const auto & first_function_assigns = it->second .front ().assignments ;
1385+ const auto & toplevel_definition = first_function_assigns.back ().value ;
1386+ array_typet type=array_typet (toplevel_definition.type (),size);
13791387 array_exprt list (type);
13801388 list.reserve_operands (it->second .size ());
1381- for (std::list<exprt>::iterator l_it= it->second . begin ();l_it!=it-> second . end ();l_it++ )
1389+ for (auto l_it : it->second )
13821390 {
1383- list.copy_to_operands (* l_it);
1391+ list.copy_to_operands (l_it. assignments . back (). value );
13841392 }
13851393 inputs[it->first ]=list;
13861394 }
@@ -1482,7 +1490,8 @@ interpretert::input_varst& interpretert::load_counter_example_inputs(
14821490 irep_idt f_id;
14831491 if (is_opaque_function (pc,f_id)!=0 )
14841492 {
1485- function_inputs[f_id].push_front (inputs[id]);
1493+ // TODO: save/restore the full data structure?
1494+ function_inputs[f_id].push_front ({ irep_idt (), { { irep_idt (), inputs[id] } } });
14861495 }
14871496 }
14881497 it++;
@@ -1519,6 +1528,74 @@ calls_opaque_stub_ret calls_opaque_stub(const code_function_callt& callinst, con
15191528 return NOT_OPAQUE_STUB;
15201529}
15211530
1531+ // Get the current value of capture_symbol plus the values of any symbols referenced in its fields.
1532+ // Store them in 'captured' in bottom-up order.
1533+ void interpretert::get_value_tree (const irep_idt& capture_symbol, const input_varst& inputs, function_assignmentst& captured)
1534+ {
1535+
1536+ // Circular reference?
1537+ for (auto already_captured : captured)
1538+ if (already_captured.id == capture_symbol)
1539+ return ;
1540+
1541+ auto findit = inputs.find (capture_symbol);
1542+ if (findit == inputs.end ())
1543+ {
1544+ std::cout << " Stub method returned without defining " " . Did the program trace end inside a stub?\n "
1545+ return ;
1546+ }
1547+
1548+ exprt defined = findit->second ;
1549+
1550+ bool isnull = false ;
1551+
1552+ if (defined.type ().id () == ID_pointer)
1553+ {
1554+
1555+ auto struct_ty = defined.type ().subtype ();
1556+ assert (struct_ty.id () == ID_struct);
1557+
1558+ std::vector<mp_integer> pointer_as_bytes;
1559+ evaluate (defined, pointer_as_bytes);
1560+ isnull = true ;
1561+ for (auto b : pointer_as_bytes)
1562+ if (!b.is_zero ())
1563+ isnull = false ;
1564+
1565+ if (!isnull)
1566+ {
1567+ std::vector<mp_integer> struct_as_bytes;
1568+ evaluate (dereference_exprt (defined, struct_ty), struct_as_bytes);
1569+ defined = get_value (struct_ty, struct_as_bytes);
1570+ }
1571+
1572+ }
1573+
1574+ if (!isnull)
1575+ {
1576+
1577+ const auto & defined_struct = to_struct_expr (defined);
1578+ const auto & struct_type = to_struct_type (defined.type ());
1579+ const auto & members = struct_type.components ();
1580+ unsigned idx = 0 ;
1581+ assert (defined_struct.operands ().size () == members.size ());
1582+ // Assumption: all object trees captured this way refer directly to particular
1583+ // symex::dynamic_object expressions, which are always address-of-symbol constructions.
1584+ forall_operands (opit, defined_struct) {
1585+ if (members[idx].type ().id () == ID_pointer)
1586+ {
1587+ const auto & referee = to_symbol_expr (to_address_of_expr (*opit).object ()).get_identifier ();
1588+ get_value_tree (referee, inputs, captured);
1589+ }
1590+ ++idx;
1591+ }
1592+
1593+ }
1594+
1595+ captured.push_back ({capture_symbol, defined});
1596+
1597+ }
1598+
15221599interpretert::input_varst& interpretert::load_counter_example_inputs (
15231600 const goto_tracet &trace, list_input_varst& function_inputs, const bool filtered) {
15241601 show=false ;
@@ -1531,7 +1608,7 @@ interpretert::input_varst& interpretert::load_counter_example_inputs(
15311608 throw " main not found"
15321609
15331610 irep_idt previous_assigned_symbol;
1534-
1611+
15351612 initialise (true );
15361613 goto_tracet::stepst::const_reverse_iterator it=trace.steps .rbegin ();
15371614 if (it!=trace.steps .rend ()) targetAssert=it->pc ;
@@ -1543,46 +1620,26 @@ interpretert::input_varst& interpretert::load_counter_example_inputs(
15431620 {
15441621
15451622 case NOT_OPAQUE_STUB:
1546- continue ;
1623+ break ;
15471624 case SIMPLE_OPAQUE_STUB:
15481625 {
15491626 // Simple opaque function that returns a primitive. The assignment after
15501627 // this (before it in trace order) will have given the value assigned to its return nondet.
15511628 if (previous_assigned_symbol != irep_idt ())
1552- function_inputs[called].push_front (inputs[previous_assigned_symbol]);
1629+ {
1630+ function_assignmentst single_defn = { { previous_assigned_symbol, inputs[previous_assigned_symbol] } };
1631+ function_inputs[called].push_front ({ function->first , single_defn });
1632+ }
15531633 break ;
15541634 }
15551635 case COMPLEX_OPAQUE_STUB:
15561636 {
15571637 // Complex stub: capture the value of capture_symbol instead of whatever happened
1558- // to have been defined most recently.
1559- // It will receive a pointer, so deref it to capture the object state.
1560- exprt defined = inputs[capture_symbol];
1561- if (defined == exprt ())
1562- {
1563- std::cout << " Stub method " " returned without defining " " . Did the program trace end inside a stub?\n "
1564- continue ;
1565- }
1566- assert (defined.type ().id () == ID_pointer);
1567-
1568- auto struct_ty = defined.type ().subtype ();
1569- assert (struct_ty.id () == ID_struct);
1570-
1571- std::vector<mp_integer> pointer_as_bytes;
1572- evaluate (defined, pointer_as_bytes);
1573- bool isnull = true ;
1574- for (auto b : pointer_as_bytes)
1575- if (!b.is_zero ())
1576- isnull = false ;
1577-
1578- if (!isnull)
1579- {
1580- std::vector<mp_integer> struct_as_bytes;
1581- evaluate (dereference_exprt (defined, struct_ty), struct_as_bytes);
1582- defined = get_value (struct_ty, struct_as_bytes);
1583- }
1584-
1585- function_inputs[called].push_front (defined);
1638+ // to have been defined most recently. Also capture any other referenced objects.
1639+ function_assignmentst defined;
1640+ get_value_tree (capture_symbol, inputs, defined);
1641+ if (defined.size () != 0 ) // Definition found?
1642+ function_inputs[called].push_front ({ function->first , defined });
15861643 break ;
15871644 }
15881645
0 commit comments