cprover
Loading...
Searching...
No Matches
analyze_symbol.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbol Analyzer
4
5Author: Malte Mues <mail.mues@gmail.com>
6 Daniel Poetzl
7
8\*******************************************************************/
9
10#include "analyze_symbol.h"
11
12#include <util/c_types.h>
13#include <util/c_types_util.h>
15#include <util/pointer_expr.h>
17#include <util/string2int.h>
19#include <util/string_utils.h>
20
21#include <climits>
22#include <cstdlib>
23
25 const symbol_tablet &symbol_table,
26 const std::vector<std::string> &args)
27 : gdb_api(args),
28 symbol_table(symbol_table),
29 ns(symbol_table),
30 c_converter(ns, expr2c_configurationt::clean_configuration),
31 allocate_objects(ID_C, source_locationt(), irep_idt{}, this->symbol_table)
32{
33}
34
36 const memory_addresst &begin,
37 const mp_integer &byte_size,
38 const irep_idt &name)
39 : begin_int(safe_string2size_t(begin.address_string, 0)),
40 byte_size(byte_size),
41 name(name)
42{
43}
44
46 const memory_addresst &point) const
47{
48 return safe_string2size_t(point.address_string, 0);
49}
50
52 const memory_addresst &point,
53 mp_integer member_size) const
54{
55 auto point_int = address2size_t(point);
56 CHECK_RETURN(check_containment(point_int));
57 return (point_int - begin_int) / member_size;
58}
59
60std::vector<gdb_value_extractort::memory_scopet>::iterator
62{
63 return std::find_if(
66 [&name](const memory_scopet &scope) { return scope.id() == name; });
67}
68
69std::vector<gdb_value_extractort::memory_scopet>::iterator
71{
72 return std::find_if(
75 [&point](const memory_scopet &memory_scope) {
76 return memory_scope.contains(point);
77 });
78}
79
81{
82 const auto scope_it = find_dynamic_allocation(name);
83 if(scope_it == dynamically_allocated.end())
84 return 1;
85 else
86 return scope_it->size();
87}
88
90 const memory_addresst &point,
91 mp_integer member_size)
92{
93 const auto scope_it = find_dynamic_allocation(point);
94 if(scope_it == dynamically_allocated.end())
95 return {};
96
97 const auto pointer_distance = scope_it->distance(point, member_size);
98 return id2string(scope_it->id()) +
99 (pointer_distance > 0 ? "+" + integer2string(pointer_distance) : "");
100}
101
103{
104 const auto maybe_size = pointer_offset_bits(type, ns);
105 CHECK_RETURN(maybe_size.has_value());
106 return *maybe_size / CHAR_BIT;
107}
108
109void gdb_value_extractort::analyze_symbols(const std::vector<irep_idt> &symbols)
110{
111 // record addresses of given symbols
112 for(const auto &id : symbols)
113 {
114 const symbolt &symbol = ns.lookup(id);
115 if(
116 symbol.type.id() != ID_pointer ||
118 {
119 const symbol_exprt &symbol_expr = ns.lookup(id).symbol_expr();
120 const address_of_exprt aoe(symbol_expr);
121
122 const std::string c_expr = c_converter.convert(aoe);
123 const pointer_valuet &value = gdb_api.get_memory(c_expr);
124 CHECK_RETURN(value.pointee.empty() || (id == value.pointee));
125
126 memory_map[id] = value;
127 }
128 else
129 {
130 const std::string c_symbol = c_converter.convert(symbol.symbol_expr());
131 const pointer_valuet &symbol_value = gdb_api.get_memory(c_symbol);
132 size_t symbol_size = gdb_api.query_malloc_size(c_symbol);
133
134 if(symbol_size > 1)
135 dynamically_allocated.emplace_back(
136 symbol_value.address, symbol_size, id);
137 memory_map[id] = symbol_value;
138 }
139 }
140
141 for(const auto &id : symbols)
142 {
143 analyze_symbol(id);
144 }
145}
146
148{
149 const symbolt &symbol = ns.lookup(symbol_name);
150 const symbol_exprt symbol_expr = symbol.symbol_expr();
151
152 try
153 {
154 const typet target_type = symbol.type;
155
156 const auto zero_expr = zero_initializer(target_type, symbol.location, ns);
157 CHECK_RETURN(zero_expr);
158
159 const exprt target_expr =
160 get_expr_value(symbol_expr, *zero_expr, symbol.location);
161
162 add_assignment(symbol_expr, target_expr);
163 }
164 catch(const gdb_interaction_exceptiont &e)
165 {
166 throw analysis_exceptiont(e.what());
167 }
168
170}
171
174{
175 code_blockt generated_code;
176
178
179 for(auto const &pair : assignments)
180 {
181 generated_code.add(code_assignt(pair.first, pair.second));
182 }
183
184 return c_converter.convert(generated_code);
185}
186
189{
190 symbol_tablet snapshot;
191
192 for(const auto &pair : assignments)
193 {
194 const symbol_exprt &symbol_expr = to_symbol_expr(pair.first);
195 const irep_idt id = symbol_expr.get_identifier();
196
197 INVARIANT(symbol_table.has_symbol(id), "symbol must exist in symbol table");
198
199 const symbolt &symbol = symbol_table.lookup_ref(id);
200
201 symbolt snapshot_symbol(symbol);
202 snapshot_symbol.value = pair.second;
203
204 snapshot.insert(snapshot_symbol);
205 }
206
207 // Also add type symbols to the snapshot
208 for(const auto &pair : symbol_table)
209 {
210 const symbolt &symbol = pair.second;
211
212 if(symbol.is_type)
213 {
214 snapshot.insert(symbol);
215 }
216 }
217
218 return snapshot;
219}
220
222{
223 if(assignments.count(lhs) == 0)
224 assignments.emplace(std::make_pair(lhs, value));
225}
226
228 const exprt &expr,
229 const memory_addresst &memory_location,
230 const source_locationt &location)
231{
232 PRECONDITION(expr.type().id() == ID_pointer);
234 PRECONDITION(!memory_location.is_null());
235
236 auto it = values.find(memory_location);
237
238 if(it == values.end())
239 {
240 std::string c_expr = c_converter.convert(expr);
241 pointer_valuet value = gdb_api.get_memory(c_expr);
242 CHECK_RETURN(value.string);
243
244 string_constantt init(*value.string);
246
247 symbol_exprt dummy("tmp", pointer_type(init.type()));
249
250 const symbol_exprt new_symbol =
252 assignments, dummy, init.type()));
253
254 add_assignment(new_symbol, init);
255
256 values.insert(std::make_pair(memory_location, new_symbol));
257
258 // check that we are returning objects of the right type
260 to_array_type(new_symbol.type()).element_type() ==
261 to_pointer_type(expr.type()).base_type());
262 return new_symbol;
263 }
264 else
265 {
267 to_array_type(it->second.type()).element_type() ==
268 to_pointer_type(expr.type()).base_type());
269 return it->second;
270 }
271}
272
274 const exprt &expr,
275 const pointer_valuet &pointer_value,
276 const source_locationt &location)
277{
278 PRECONDITION(expr.type().id() == ID_pointer);
279 const auto &memory_location = pointer_value.address;
280 std::string memory_location_string = memory_location.string();
281 PRECONDITION(memory_location_string != "0x0");
282 PRECONDITION(!pointer_value.pointee.empty());
283
284 std::string struct_name;
285 size_t member_offset;
286 if(pointer_value.has_known_offset())
287 {
288 std::string member_offset_string;
290 pointer_value.pointee, '+', struct_name, member_offset_string, true);
291 member_offset = safe_string2size_t(member_offset_string);
292 }
293 else
294 {
295 struct_name = pointer_value.pointee;
296 member_offset = 0;
297 }
298
299 const symbolt *struct_symbol = symbol_table.lookup(struct_name);
300 DATA_INVARIANT(struct_symbol != nullptr, "unknown struct");
301
302 if(!has_known_memory_location(struct_name))
303 {
304 memory_map[struct_name] = gdb_api.get_memory(struct_name);
305 analyze_symbol(irep_idt{struct_name});
306 }
307
308 const auto &struct_symbol_expr = struct_symbol->symbol_expr();
309 if(struct_symbol->type.id() == ID_array)
310 {
311 return index_exprt{
312 struct_symbol_expr,
315 index_type())};
316 }
317 if(struct_symbol->type.id() == ID_pointer)
318 {
319 return dereference_exprt{
320 plus_exprt{struct_symbol_expr,
322 expr.type()}};
323 }
324
325 const auto maybe_member_expr = get_subexpression_at_offset(
326 struct_symbol_expr,
329 ns);
331 maybe_member_expr.has_value(), "structure doesn't have member");
332
333 // check that we return the right type
335 maybe_member_expr->type() == to_pointer_type(expr.type()).base_type());
336 return *maybe_member_expr;
337}
338
340 const exprt &expr,
341 const pointer_valuet &pointer_value,
342 const source_locationt &location)
343{
344 PRECONDITION(expr.type().id() == ID_pointer);
345 PRECONDITION(to_pointer_type(expr.type()).base_type().id() == ID_code);
346 PRECONDITION(!pointer_value.address.is_null());
347
348 const auto &function_name = pointer_value.pointee;
349 CHECK_RETURN(!function_name.empty());
350 const auto function_symbol = symbol_table.lookup(function_name);
351 if(function_symbol == nullptr)
352 {
354 "input source code does not contain function: " + function_name};
355 }
356 CHECK_RETURN(function_symbol->type.id() == ID_code);
357 return function_symbol->symbol_expr();
358}
359
361 const exprt &expr,
362 const pointer_valuet &value,
363 const source_locationt &location)
364{
365 PRECONDITION(expr.type().id() == ID_pointer);
367 const auto &memory_location = value.address;
368 PRECONDITION(!memory_location.is_null());
369
370 auto it = values.find(memory_location);
371
372 if(it == values.end())
373 {
374 if(!value.pointee.empty() && value.pointee != c_converter.convert(expr))
375 {
376 analyze_symbol(value.pointee);
377 const auto pointee_symbol = symbol_table.lookup(value.pointee);
378 CHECK_RETURN(pointee_symbol != nullptr);
379 const auto pointee_symbol_expr = pointee_symbol->symbol_expr();
380 return pointee_symbol_expr;
381 }
382
383 values.insert(std::make_pair(memory_location, nil_exprt()));
384
385 const typet target_type = to_pointer_type(expr.type()).base_type();
386
387 symbol_exprt dummy("tmp", expr.type());
389
390 const auto zero_expr = zero_initializer(target_type, location, ns);
391 CHECK_RETURN(zero_expr);
392
393 // Check if pointer was dynamically allocated (via malloc). If so we will
394 // replace the pointee with a static array filled with values stored at the
395 // expected positions. Since the allocated size is over-approximation we may
396 // end up querying pass the allocated bounds and building larger array with
397 // meaningless values.
398 mp_integer allocated_size = get_malloc_size(c_converter.convert(expr));
399 // get the sizeof(target_type) and thus the number of elements
400 const auto number_of_elements = allocated_size / get_type_size(target_type);
401 if(allocated_size != 1 && number_of_elements > 1)
402 {
403 array_exprt::operandst elements;
404 // build the operands by querying for an index expression
405 for(size_t i = 0; i < number_of_elements; i++)
406 {
407 const auto sub_expr_value = get_expr_value(
409 *zero_expr,
410 location);
411 elements.push_back(sub_expr_value);
412 }
413 CHECK_RETURN(elements.size() == number_of_elements);
414
415 // knowing the number of elements we can build the type
416 const typet target_array_type =
417 array_typet{target_type, from_integer(elements.size(), index_type())};
418
419 array_exprt new_array{elements, to_array_type(target_array_type)};
420
421 // allocate a new symbol for the temporary static array
422 symbol_exprt array_dummy("tmp", pointer_type(target_array_type));
423 const auto array_symbol =
425 assignments, array_dummy, target_array_type);
426
427 // add assignment of value to newly created symbol
428 add_assignment(array_symbol, new_array);
429 values[memory_location] = array_symbol;
430 CHECK_RETURN(array_symbol.type().id() == ID_array);
431 return array_symbol;
432 }
433
434 const symbol_exprt new_symbol =
436 assignments, dummy, target_type));
437
438 dereference_exprt dereference_expr(expr);
439
440 const exprt target_expr =
441 get_expr_value(dereference_expr, *zero_expr, location);
442 // add assignment of value to newly created symbol
443 add_assignment(new_symbol, target_expr);
444
445 values[memory_location] = new_symbol;
446
447 return new_symbol;
448 }
449 else
450 {
451 const auto &known_value = it->second;
452 const auto &expected_type = to_pointer_type(expr.type()).base_type();
453 if(find_dynamic_allocation(memory_location) != dynamically_allocated.end())
454 return known_value;
455 if(known_value.is_not_nil() && known_value.type() != expected_type)
456 {
457 return symbol_exprt{to_symbol_expr(known_value).get_identifier(),
458 expected_type};
459 }
460 return known_value;
461 }
462}
463
465 pointer_valuet &pointer_value,
466 const pointer_typet &expected_type)
467{
468 if(pointer_value.has_known_offset())
469 return true;
470
471 if(pointer_value.pointee.empty())
472 {
473 const auto maybe_pointee = get_malloc_pointee(
474 pointer_value.address, get_type_size(expected_type.base_type()));
475 if(maybe_pointee.has_value())
476 pointer_value.pointee = *maybe_pointee;
477 if(pointer_value.pointee.find("+") != std::string::npos)
478 return true;
479 }
480
481 const symbolt *pointee_symbol = symbol_table.lookup(pointer_value.pointee);
482 if(pointee_symbol == nullptr)
483 return false;
484 const auto &pointee_type = pointee_symbol->type;
485 return pointee_type.id() == ID_struct_tag ||
486 pointee_type.id() == ID_union_tag || pointee_type.id() == ID_array ||
487 pointee_type.id() == ID_struct || pointee_type.id() == ID_union;
488}
489
491 const exprt &expr,
492 const exprt &zero_expr,
493 const source_locationt &location)
494{
495 PRECONDITION(zero_expr.id() == ID_constant);
496
497 PRECONDITION(expr.type().id() == ID_pointer);
498 PRECONDITION(expr.type() == zero_expr.type());
499
500 std::string c_expr = c_converter.convert(expr);
501 const auto known_pointer = memory_map.find(c_expr);
502
503 pointer_valuet value = (known_pointer == memory_map.end() ||
504 known_pointer->second.pointee == c_expr)
505 ? gdb_api.get_memory(c_expr)
506 : known_pointer->second;
507 if(!value.valid)
508 return zero_expr;
509
510 const auto memory_location = value.address;
511
512 if(!memory_location.is_null())
513 {
514 // pointers-to-char can point to members as well, e.g. char[]
515 if(points_to_member(value, to_pointer_type(expr.type())))
516 {
517 const auto target_expr =
518 get_pointer_to_member_value(expr, value, location);
519 CHECK_RETURN(target_expr.is_not_nil());
520 const address_of_exprt result_expr{target_expr};
521 CHECK_RETURN(result_expr.type() == zero_expr.type());
522 return std::move(result_expr);
523 }
524
525 // pointer to function
526 if(to_pointer_type(expr.type()).base_type().id() == ID_code)
527 {
528 const auto target_expr =
529 get_pointer_to_function_value(expr, value, location);
530 CHECK_RETURN(target_expr.is_not_nil());
531 const address_of_exprt result_expr{target_expr};
532 CHECK_RETURN(result_expr.type() == zero_expr.type());
533 return std::move(result_expr);
534 }
535
536 // non-member: split for char/non-char
537 const auto target_expr =
539 ? get_char_pointer_value(expr, memory_location, location)
540 : get_non_char_pointer_value(expr, value, location);
541
542 // postpone if we cannot resolve now
543 if(target_expr.is_nil())
544 {
545 outstanding_assignments[expr] = memory_location;
546 return zero_expr;
547 }
548
549 // the pointee was (probably) dynamically allocated (but the allocation
550 // would not be visible in the snapshot) so we pretend it is statically
551 // allocated (we have the value) and return address to the first element
552 // of the array (instead of the array as char*)
553 if(target_expr.type().id() == ID_array)
554 {
555 const auto result_indexed_expr = get_subexpression_at_offset(
556 target_expr, 0, to_pointer_type(zero_expr.type()).base_type(), ns);
557 CHECK_RETURN(result_indexed_expr.has_value());
558 if(result_indexed_expr->type() == zero_expr.type())
559 return *result_indexed_expr;
560 const address_of_exprt result_expr{*result_indexed_expr};
561 CHECK_RETURN(result_expr.type() == zero_expr.type());
562 return std::move(result_expr);
563 }
564
565 // if the types match return right away
566 if(target_expr.type() == zero_expr.type())
567 return target_expr;
568
569 // otherwise the address of target should type-match
570 const address_of_exprt result_expr{target_expr};
571 if(result_expr.type() != zero_expr.type())
572 return typecast_exprt{result_expr, zero_expr.type()};
573 return std::move(result_expr);
574 }
575
576 return zero_expr;
577}
578
580 const exprt &expr,
581 const exprt &array,
582 const source_locationt &location)
583{
584 PRECONDITION(array.id() == ID_array);
585
586 PRECONDITION(expr.type().id() == ID_array);
587 PRECONDITION(expr.type() == array.type());
588
589 exprt new_array(array);
590
591 for(size_t i = 0; i < new_array.operands().size(); ++i)
592 {
593 const index_exprt index_expr(expr, from_integer(i, index_type()));
594
595 exprt &operand = new_array.operands()[i];
596
597 operand = get_expr_value(index_expr, operand, location);
598 }
599
600 return new_array;
601}
602
604 const exprt &expr,
605 const exprt &zero_expr,
606 const source_locationt &location)
607{
608 PRECONDITION(expr.type() == zero_expr.type());
609
610 const typet &type = expr.type();
611 PRECONDITION(type.id() != ID_struct);
612
613 if(is_c_integral_type(type))
614 {
615 INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
616
617 std::string c_expr = c_converter.convert(expr);
618 const auto maybe_value = gdb_api.get_value(c_expr);
619 if(!maybe_value.has_value())
620 return zero_expr;
621 const std::string value = *maybe_value;
622
623 const mp_integer int_rep = string2integer(value);
624
625 return from_integer(int_rep, type);
626 }
627 else if(is_c_char_type(type))
628 {
629 INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
630
631 // check the char-value and return as bitvector-type value
632 std::string c_expr = c_converter.convert(expr);
633 const auto maybe_value = gdb_api.get_value(c_expr);
634 if(!maybe_value.has_value() || maybe_value->empty())
635 return zero_expr;
636 const std::string value = *maybe_value;
637
638 const mp_integer int_rep = value[0];
639 return from_integer(int_rep, type);
640 }
641 else if(type.id() == ID_c_bool)
642 {
643 INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
644
645 std::string c_expr = c_converter.convert(expr);
646 const auto maybe_value = gdb_api.get_value(c_expr);
647 if(!maybe_value.has_value())
648 return zero_expr;
649 const std::string value = *maybe_value;
650
651 return from_c_boolean_value(id2boolean(value), type);
652 }
653 else if(type.id() == ID_c_enum)
654 {
655 INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
656
657 std::string c_expr = c_converter.convert(expr);
658 const auto maybe_value = gdb_api.get_value(c_expr);
659 if(!maybe_value.has_value())
660 return zero_expr;
661 const std::string value = *maybe_value;
662
664 }
665 else if(type.id() == ID_struct_tag)
666 {
667 return get_struct_value(expr, zero_expr, location);
668 }
669 else if(type.id() == ID_array)
670 {
671 return get_array_value(expr, zero_expr, location);
672 }
673 else if(type.id() == ID_pointer)
674 {
675 INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
676
677 return get_pointer_value(expr, zero_expr, location);
678 }
679 else if(type.id() == ID_union_tag)
680 {
681 return get_union_value(expr, zero_expr, location);
682 }
684}
685
687 const exprt &expr,
688 const exprt &zero_expr,
689 const source_locationt &location)
690{
691 PRECONDITION(zero_expr.id() == ID_struct);
692
693 PRECONDITION(expr.type().id() == ID_struct_tag);
694 PRECONDITION(expr.type() == zero_expr.type());
695
696 exprt new_expr(zero_expr);
697
698 const struct_tag_typet &struct_tag_type = to_struct_tag_type(expr.type());
699 const struct_typet &struct_type = ns.follow_tag(struct_tag_type);
700
701 for(size_t i = 0; i < new_expr.operands().size(); ++i)
702 {
703 const struct_typet::componentt &component = struct_type.components()[i];
704
705 if(component.get_is_padding() || component.type().id() == ID_code)
706 {
707 continue;
708 }
709
710 exprt &operand = new_expr.operands()[i];
711 member_exprt member_expr(expr, component);
712
713 operand = get_expr_value(member_expr, operand, location);
714 }
715
716 return new_expr;
717}
718
720 const exprt &expr,
721 const exprt &zero_expr,
722 const source_locationt &location)
723{
724 PRECONDITION(zero_expr.id() == ID_union);
725
726 PRECONDITION(expr.type().id() == ID_union_tag);
727 PRECONDITION(expr.type() == zero_expr.type());
728
729 exprt new_expr(zero_expr);
730
731 const union_tag_typet &union_tag_type = to_union_tag_type(expr.type());
732 const union_typet &union_type = ns.follow_tag(union_tag_type);
733
734 CHECK_RETURN(new_expr.operands().size() == 1);
735 const union_typet::componentt &component = union_type.components()[0];
736 auto &operand = new_expr.operands()[0];
737 operand = get_expr_value(member_exprt{expr, component}, operand, location);
738 return new_expr;
739}
740
742{
743 for(const auto &pair : outstanding_assignments)
744 {
745 const address_of_exprt aoe(values[pair.second]);
746 add_assignment(pair.first, aoe);
747 }
748}
749
751{
752 std::string c_expr = c_converter.convert(expr);
753 const auto maybe_value = gdb_api.get_value(c_expr);
754 CHECK_RETURN(maybe_value.has_value());
755 return *maybe_value;
756}
High-level interface to gdb.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
bitvector_typet index_type()
Definition: c_types.cpp:22
unsignedbv_typet size_type()
Definition: c_types.cpp:68
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:302
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:202
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.
Definition: c_types_util.h:44
bool id2boolean(const std::string &bool_value)
Convert id to a Boolean value.
Definition: c_types_util.h:105
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.
Definition: c_types_util.h:122
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 ...
Definition: c_types_util.h:85
bool is_c_char_type(const typet &type)
This function checks, whether this has been a char type in the c program.
Definition: c_types_util.h:25
Operator to return the address of an object.
Definition: pointer_expr.h:361
exprt allocate_automatic_local_object(code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const irep_idt &basename_prefix="tmp")
Creates a local variable with automatic lifetime.
void declare_created_symbols(code_blockt &init_code)
Adds declarations for all non-static symbols created.
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
Array constructor from list of elements.
Definition: std_expr.h:1476
Arrays with given size.
Definition: std_types.h:763
bool is_complete() const
Definition: std_types.h:800
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:777
A codet representing an assignment in the program.
A codet representing sequential composition of program statements.
Definition: std_code.h:130
void add(const codet &code)
Definition: std_code.h:168
Operator to dereference a pointer.
Definition: pointer_expr.h:648
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
virtual std::string convert(const typet &src)
Definition: expr2c.cpp:214
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
optionalt< std::string > get_value(const std::string &expr)
Get the memory address pointed to by the given pointer expression.
Definition: gdb_api.cpp:487
size_t query_malloc_size(const std::string &pointer_expr)
Get the exact allocated size for a pointer pointer_expr.
Definition: gdb_api.cpp:58
pointer_valuet get_memory(const std::string &expr)
Get the value of a pointer associated with expr.
Definition: gdb_api.cpp:436
std::string what() const override
A human readable description of what went wrong.
Definition: gdb_api.h:235
std::string get_gdb_value(const exprt &expr)
Extract a stringified value from and c-converted expr.
exprt get_pointer_to_member_value(const exprt &expr, const pointer_valuet &pointer_value, const source_locationt &location)
Call get_subexpression_at_offset to get the correct member expression.
allocate_objectst allocate_objects
std::map< irep_idt, pointer_valuet > memory_map
Keep track of the memory location for the analyzed symbols.
std::map< exprt, memory_addresst > outstanding_assignments
Mapping pointer expression for which get_non_char_pointer_value returned nil expression to memory loc...
optionalt< std::string > get_malloc_pointee(const memory_addresst &point, mp_integer member_size)
Build the pointee string for address point assuming it points to a dynamic allocation of ā€˜n’ elements...
void analyze_symbol(const irep_idt &symbol_name)
Assign the gdb-extracted value for symbol_name to its symbol expression and then process outstanding ...
bool has_known_memory_location(const irep_idt &id) const
exprt get_char_pointer_value(const exprt &expr, const memory_addresst &memory_location, const source_locationt &location)
If memory_location is found among values then return the symbol expression associated with it.
exprt get_pointer_to_function_value(const exprt &expr, const pointer_valuet &pointer_value, const source_locationt &location)
Extract the function name from pointer_value, check it has a symbol and return the associated symbol ...
void process_outstanding_assignments()
Call add_assignment for each pair in outstanding_assignments.
exprt get_array_value(const exprt &expr, const exprt &array, const source_locationt &location)
Iterate over array and fill its operands with the results of calling get_expr_value on index expressi...
void add_assignment(const exprt &lhs, const exprt &value)
Create assignment lhs := value (see analyze_symbol)
std::vector< memory_scopet > dynamically_allocated
Keep track of the dynamically allocated memory.
std::map< exprt, exprt > assignments
Sequence of assignments collected during analyze_symbols.
std::string get_snapshot_as_c_code()
Get memory snapshot as C code.
std::map< memory_addresst, exprt > values
Storing pairs <address, symbol> such that at address is stored the value of symbol.
exprt get_expr_value(const exprt &expr, const exprt &zero_expr, const source_locationt &location)
Case analysis on the typet of expr 1) For integers, booleans, and enums: call gdb_apit::get_value dir...
gdb_value_extractort(const symbol_tablet &symbol_table, const std::vector< std::string > &args)
mp_integer get_type_size(const typet &type) const
Wrapper for call get_offset_pointer_bits.
void analyze_symbols(const std::vector< irep_idt > &symbols)
For each input symbol in symbols: map its value address to its symbol_exprt (via the values map) and ...
bool points_to_member(pointer_valuet &pointer_value, const pointer_typet &expected_type)
Analyzes the pointer_value to decide if it point to a struct or a union (or array)
mp_integer get_malloc_size(irep_idt name)
Search for the size of the allocated memory for name.
exprt get_pointer_value(const exprt &expr, const exprt &zero_expr, const source_locationt &location)
Call gdb_apit::get_memory on expr then split based on the points-to type being char type or not.
symbol_tablet symbol_table
External symbol table – extracted from read_goto_binary We only expect to analyse symbols located the...
exprt get_struct_value(const exprt &expr, const exprt &zero_expr, const source_locationt &location)
For each of the members of the struct: call get_expr_value.
std::vector< memory_scopet >::iterator find_dynamic_allocation(irep_idt name)
Search for a memory scope allocated under name.
exprt get_union_value(const exprt &expr, const exprt &zero_expr, const source_locationt &location)
For each of the members of the struct: call get_expr_value.
symbol_tablet get_snapshot_as_symbol_table()
Get memory snapshot as symbol table Build a new symbol_tablet and for each lhs symbol from collected ...
exprt get_non_char_pointer_value(const exprt &expr, const pointer_valuet &value, const source_locationt &location)
Similar to get_char_pointer_value.
const namespacet ns
Array index operator.
Definition: std_expr.h:1328
Thrown when we can't handle something in an input source file.
const irep_idt & id() const
Definition: irep.h:396
Extract member of struct or union.
Definition: std_expr.h:2667
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
The NIL expression.
Definition: std_expr.h:2874
The plus expression Associativity is not specified.
Definition: std_expr.h:914
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:449
Structure type, corresponds to C style structs.
Definition: std_types.h:231
const componentst & components() const
Definition: std_types.h:147
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The symbol table.
Definition: symbol_table.h:14
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Symbol table entry.
Definition: symbol.h:28
bool is_type
Definition: symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
exprt value
Initial value of symbol.
Definition: symbol.h:34
Semantic type conversion.
Definition: std_expr.h:1920
The type of an expression, extends irept.
Definition: type.h:29
A union tag type, i.e., union_typet with an identifier.
Definition: c_types.h:177
The union type.
Definition: c_types.h:125
optionalt< 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)
Definition: irep.h:47
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:54
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:103
nonstd::optional< T > optionalt
Definition: optional.h:35
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Pointer Logic.
BigInt mp_integer
Definition: smt_terms.h:12
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:48
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
std::size_t safe_string2size_t(const std::string &str, int base)
Definition: string2int.cpp:23
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.
Definition: expr2c.h:21
Memory address imbued with the explicit boolean data indicating if the address is null or not.
Definition: gdb_api.h:38
std::string string() const
Definition: gdb_api.h:57
std::string address_string
Definition: gdb_api.h:40
bool is_null() const
Definition: gdb_api.h:49
Data associated with the value of a pointer, i.e.
Definition: gdb_api.h:78
memory_addresst address
Definition: gdb_api.h:93
bool has_known_offset() const
Definition: gdb_api.h:98
std::string pointee
Definition: gdb_api.h:94
optionalt< std::string > string
Definition: gdb_api.h:96
mp_integer distance(const memory_addresst &point, mp_integer member_size) const
Compute the distance of point from the beginning of this scope.
memory_scopet(const memory_addresst &begin, const mp_integer &byte_size, const irep_idt &name)
size_t address2size_t(const memory_addresst &point) const
Convert base-16 memory address to a natural number.