24gdb_value_extractort::gdb_value_extractort(
26 const std::vector<std::string> &args)
28 symbol_table(symbol_table),
35gdb_value_extractort::memory_scopet::memory_scopet(
36 const memory_addresst &begin,
45size_t gdb_value_extractort::memory_scopet::address2size_t(
46 const memory_addresst &point)
const
51mp_integer gdb_value_extractort::memory_scopet::distance(
52 const memory_addresst &point,
55 auto point_int = address2size_t(point);
57 return (point_int - begin_int) / member_size;
60std::vector<gdb_value_extractort::memory_scopet>::iterator
61gdb_value_extractort::find_dynamic_allocation(
irep_idt name)
64 dynamically_allocated.begin(),
65 dynamically_allocated.end(),
66 [&name](
const memory_scopet &scope) { return scope.id() == name; });
69std::vector<gdb_value_extractort::memory_scopet>::iterator
70gdb_value_extractort::find_dynamic_allocation(
const memory_addresst &point)
73 dynamically_allocated.begin(),
74 dynamically_allocated.end(),
75 [&point](
const memory_scopet &memory_scope) {
76 return memory_scope.contains(point);
82 const auto scope_it = find_dynamic_allocation(name);
83 if(scope_it == dynamically_allocated.end())
86 return scope_it->size();
89std::optional<std::string> gdb_value_extractort::get_malloc_pointee(
90 const memory_addresst &point,
93 const auto scope_it = find_dynamic_allocation(point);
94 if(scope_it == dynamically_allocated.end())
97 const auto pointer_distance = scope_it->distance(point, member_size);
99 (pointer_distance > 0 ?
"+" +
integer2string(pointer_distance) :
"");
106 return *maybe_size / CHAR_BIT;
109void gdb_value_extractort::analyze_symbols(
110 const std::list<std::string> &symbols)
113 for(
const auto &
id : symbols)
115 const symbolt &symbol = ns.lookup(
id);
117 symbol.
type.
id() != ID_pointer ||
120 const symbol_exprt &symbol_expr = ns.lookup(
id).symbol_expr();
123 const std::string c_expr = c_converter.convert(aoe);
124 const pointer_valuet &value = gdb_api.get_memory(c_expr);
125 CHECK_RETURN(value.pointee.empty() || (
id == value.pointee));
127 memory_map[id] = value;
131 const std::string c_symbol = c_converter.convert(symbol.
symbol_expr());
132 const pointer_valuet &symbol_value = gdb_api.get_memory(c_symbol);
133 size_t symbol_size = gdb_api.query_malloc_size(c_symbol);
136 dynamically_allocated.emplace_back(
137 symbol_value.address, symbol_size,
id);
138 memory_map[id] = symbol_value;
142 for(
const auto &
id : symbols)
148void gdb_value_extractort::analyze_symbol(
const irep_idt &symbol_name)
150 const symbolt &symbol = ns.lookup(symbol_name);
160 const exprt target_expr =
161 get_expr_value(symbol_expr, *zero_expr, symbol.
location);
163 add_assignment(symbol_expr, target_expr);
170 process_outstanding_assignments();
174std::string gdb_value_extractort::get_snapshot_as_c_code()
178 allocate_objects.declare_created_symbols(generated_code);
180 for(
auto const &pair : assignments)
185 return c_converter.convert(generated_code);
189symbol_tablet gdb_value_extractort::get_snapshot_as_symbol_table()
193 for(
const auto &pair : assignments)
198 INVARIANT(symbol_table.has_symbol(
id),
"symbol must exist in symbol table");
200 const symbolt &symbol = symbol_table.lookup_ref(
id);
202 symbolt snapshot_symbol(symbol);
203 snapshot_symbol.value = pair.second;
205 snapshot.
insert(snapshot_symbol);
209 for(
const auto &pair : symbol_table)
211 const symbolt &symbol = pair.second;
222void gdb_value_extractort::add_assignment(
const exprt &lhs,
const exprt &value)
224 if(assignments.count(lhs) == 0)
225 assignments.emplace(std::make_pair(lhs, value));
228exprt gdb_value_extractort::get_char_pointer_value(
230 const memory_addresst &memory_location,
237 auto it = values.find(memory_location);
239 if(it == values.end())
241 std::string c_expr = c_converter.convert(expr);
242 pointer_valuet value = gdb_api.get_memory(c_expr);
253 assignments, dummy, init.type()));
255 add_assignment(new_symbol, init);
257 values.insert(std::make_pair(memory_location, new_symbol));
274exprt gdb_value_extractort::get_pointer_to_member_value(
276 const pointer_valuet &pointer_value,
280 const auto &memory_location = pointer_value.address;
281 std::string memory_location_string = memory_location.string();
285 std::string struct_name;
287 if(pointer_value.has_known_offset())
289 std::string member_offset_string;
291 pointer_value.pointee,
'+', struct_name, member_offset_string,
true);
296 struct_name = pointer_value.pointee;
300 const symbolt *struct_symbol = symbol_table.lookup(struct_name);
303 if(!has_known_memory_location(struct_name))
305 memory_map[struct_name] = gdb_api.get_memory(struct_name);
306 analyze_symbol(
irep_idt{struct_name});
309 const auto &struct_symbol_expr = struct_symbol->
symbol_expr();
310 if(struct_symbol->
type.
id() == ID_array)
318 if(struct_symbol->
type.
id() == ID_pointer)
332 maybe_member_expr.has_value(),
"structure doesn't have member");
337 return *maybe_member_expr;
340exprt gdb_value_extractort::get_pointer_to_function_value(
342 const pointer_valuet &pointer_value,
349 const auto &function_name = pointer_value.pointee;
351 const auto function_symbol = symbol_table.lookup(function_name);
352 if(function_symbol ==
nullptr)
355 "input source code does not contain function: " + function_name};
358 return function_symbol->symbol_expr();
361exprt gdb_value_extractort::get_non_char_pointer_value(
363 const pointer_valuet &value,
368 const auto &memory_location = value.address;
371 auto it = values.find(memory_location);
373 if(it == values.end())
375 if(!value.pointee.empty() && value.pointee != c_converter.convert(expr))
377 analyze_symbol(value.pointee);
378 const auto pointee_symbol = symbol_table.lookup(value.pointee);
380 const auto pointee_symbol_expr = pointee_symbol->symbol_expr();
381 return pointee_symbol_expr;
384 values.insert(std::make_pair(memory_location,
nil_exprt()));
399 mp_integer allocated_size = get_malloc_size(c_converter.convert(expr));
401 const auto number_of_elements = allocated_size / get_type_size(target_type);
402 if(allocated_size != 1 && number_of_elements > 1)
406 for(
size_t i = 0; i < number_of_elements; i++)
408 const auto sub_expr_value = get_expr_value(
412 elements.push_back(sub_expr_value);
417 const typet target_array_type =
424 const auto array_symbol =
425 allocate_objects.allocate_automatic_local_object(
426 assignments, array_dummy, target_array_type);
429 add_assignment(array_symbol, new_array);
430 values[memory_location] = array_symbol;
437 assignments, dummy, target_type));
441 const exprt target_expr =
442 get_expr_value(dereference_expr, *zero_expr, location);
444 add_assignment(new_symbol, target_expr);
446 values[memory_location] = new_symbol;
452 const auto &known_value = it->second;
454 if(find_dynamic_allocation(memory_location) != dynamically_allocated.end())
456 if(known_value.is_not_nil() && known_value.type() != expected_type)
465bool gdb_value_extractort::points_to_member(
466 pointer_valuet &pointer_value,
469 if(pointer_value.has_known_offset())
472 if(pointer_value.pointee.empty())
474 const auto maybe_pointee = get_malloc_pointee(
475 pointer_value.address, get_type_size(expected_type.
base_type()));
476 if(maybe_pointee.has_value())
477 pointer_value.pointee = *maybe_pointee;
478 if(pointer_value.pointee.find(
"+") != std::string::npos)
482 const symbolt *pointee_symbol = symbol_table.lookup(pointer_value.pointee);
483 if(pointee_symbol ==
nullptr)
485 const auto &pointee_type = pointee_symbol->
type;
486 return pointee_type.
id() == ID_struct_tag ||
487 pointee_type.id() == ID_union_tag || pointee_type.id() == ID_array ||
488 pointee_type.id() == ID_struct || pointee_type.id() == ID_union;
491exprt gdb_value_extractort::get_pointer_value(
493 const exprt &zero_expr,
501 std::string c_expr = c_converter.convert(expr);
502 const auto known_pointer = memory_map.find(c_expr);
504 pointer_valuet value = (known_pointer == memory_map.end() ||
505 known_pointer->second.pointee == c_expr)
506 ? gdb_api.get_memory(c_expr)
507 : known_pointer->second;
511 const auto memory_location = value.address;
513 if(!memory_location.is_null())
518 const auto target_expr =
519 get_pointer_to_member_value(expr, value, location);
523 return std::move(result_expr);
529 const auto target_expr =
530 get_pointer_to_function_value(expr, value, location);
534 return std::move(result_expr);
538 const auto target_expr =
540 ? get_char_pointer_value(expr, memory_location, location)
541 : get_non_char_pointer_value(expr, value, location);
544 if(target_expr.is_nil())
546 outstanding_assignments[expr] = memory_location;
554 if(target_expr.type().id() == ID_array)
556 const auto result_indexed_expr = get_subexpression_at_offset(
557 target_expr, 0, to_pointer_type(zero_expr.type()).base_type(), ns);
558 CHECK_RETURN(result_indexed_expr.has_value());
559 if(result_indexed_expr->type() == zero_expr.type())
560 return *result_indexed_expr;
561 const address_of_exprt result_expr{*result_indexed_expr};
563 return std::move(result_expr);
567 if(target_expr.type() == zero_expr.
type())
572 if(result_expr.type() != zero_expr.
type())
574 return std::move(result_expr);
580exprt gdb_value_extractort::get_array_value(
590 exprt new_array(array);
592 for(
size_t i = 0; i < new_array.operands().size(); ++i)
598 operand = get_expr_value(index_expr, operand, location);
604exprt gdb_value_extractort::get_expr_value(
606 const exprt &zero_expr,
618 std::string c_expr = c_converter.convert(expr);
619 const auto maybe_value = gdb_api.get_value(c_expr);
620 if(!maybe_value.has_value())
622 const std::string value = *maybe_value;
633 std::string c_expr = c_converter.convert(expr);
634 const auto maybe_value = gdb_api.get_value(c_expr);
635 if(!maybe_value.has_value() || maybe_value->empty())
637 const std::string value = *maybe_value;
642 else if(type.
id() == ID_c_bool)
646 std::string c_expr = c_converter.convert(expr);
647 const auto maybe_value = gdb_api.get_value(c_expr);
648 if(!maybe_value.has_value())
650 const std::string value = *maybe_value;
654 else if(type.
id() == ID_c_enum)
658 std::string c_expr = c_converter.convert(expr);
659 const auto maybe_value = gdb_api.get_value(c_expr);
660 if(!maybe_value.has_value())
662 const std::string value = *maybe_value;
666 else if(type.
id() == ID_struct_tag)
668 return get_struct_value(expr, zero_expr, location);
670 else if(type.
id() == ID_array)
672 return get_array_value(expr, zero_expr, location);
674 else if(type.
id() == ID_pointer)
678 return get_pointer_value(expr, zero_expr, location);
680 else if(type.
id() == ID_union_tag)
682 return get_union_value(expr, zero_expr, location);
687exprt gdb_value_extractort::get_struct_value(
689 const exprt &zero_expr,
697 exprt new_expr(zero_expr);
700 const struct_typet &struct_type = ns.follow_tag(struct_tag_type);
702 for(
size_t i = 0; i < new_expr.operands().size(); ++i)
708 "struct member must not be of code type");
717 operand = get_expr_value(member_expr, operand, location);
723exprt gdb_value_extractort::get_union_value(
725 const exprt &zero_expr,
733 exprt new_expr(zero_expr);
736 const union_typet &union_type = ns.follow_tag(union_tag_type);
740 auto &operand = new_expr.operands()[0];
745void gdb_value_extractort::process_outstanding_assignments()
747 for(
const auto &pair : outstanding_assignments)
750 add_assignment(pair.first, aoe);
754std::string gdb_value_extractort::get_gdb_value(
const exprt &expr)
756 std::string c_expr = c_converter.convert(expr);
757 const auto maybe_value = gdb_api.get_value(c_expr);
High-level interface to gdb.
unsignedbv_typet size_type()
pointer_typet pointer_type(const typet &subtype)
bitvector_typet c_index_type()
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
This file contains functions, that should support test for underlying c types, in cases where this is...
bool is_c_integral_type(const typet &type)
This function checks, whether the type has been some kind of integer type in the c program.
bool id2boolean(const std::string &bool_value)
Convert id to a Boolean value.
constant_exprt from_c_boolean_value(bool bool_value, const typet &type)
This function creates a constant representing either 0 or 1 as value of type type.
constant_exprt convert_member_name_to_enum_value(const irep_idt &member_name, const c_enum_typet &c_enum)
This function creates a constant representing the bitvector encoded integer value of a string in the ...
bool is_c_char_type(const typet &type)
This function checks, whether this has been a char type in the c program.
Operator to return the address of an object.
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
Array constructor from list of elements.
const typet & element_type() const
The type of the elements of the array.
A goto_instruction_codet representing an assignment in the program.
A codet representing sequential composition of program statements.
void add(const codet &code)
virtual std::string what() const
A human readable description of what went wrong.
Operator to dereference a pointer.
Base class for all expressions.
std::vector< exprt > operandst
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
const irep_idt & id() const
Extract member of struct or union.
The plus expression Associativity is not specified.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
A struct tag type, i.e., struct_typet with an identifier.
Structure type, corresponds to C style structs.
const componentst & components() const
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
The symbol table base class interface.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
source_locationt location
Source code location of definition of symbol.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
Semantic type conversion.
The type of an expression, extends irept.
A union tag type, i.e., union_typet with an identifier.
std::optional< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Expression Initialization.
const std::string & id2string(const irep_idt &d)
const mp_integer string2integer(const std::string &n, unsigned base)
const std::string integer2string(const mp_integer &n, unsigned base)
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
std::optional< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
std::optional< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
std::size_t safe_string2size_t(const std::string &str, int base)
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Used for configuring the behaviour of expr2c and type2c.