cprover
memory_analyzer_parse_options.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Memory Analyzer
4
5Author: Malte Mues <mail.mues@gmail.com>
6 Daniel Poetzl
7
8\*******************************************************************/
9
12
14#include "analyze_symbol.h"
15
16#include <algorithm>
17#include <fstream>
18
20
24
25#include <langapi/mode.h>
26
27#include <util/config.h>
28#include <util/exit_codes.h>
29#include <util/message.h>
30#include <util/string_utils.h>
31#include <util/version.h>
32
34 int argc,
35 const char *argv[])
38 argc,
39 argv,
40 std::string("MEMORY-ANALYZER ") + CBMC_VERSION),
41 message(ui_message_handler)
42{
43}
44
46{
47 // For now only C is supported due to the additional challenges of
48 // mapping source code to debugging symbols in other languages.
50}
51
53{
54 if(cmdline.isset("version"))
55 {
56 message.status() << CBMC_VERSION << '\n';
58 }
59
61
62 if(cmdline.args.size() < 1)
63 {
65 "no binary provided for analysis", "<binary> <args>");
66 }
67
68 if(!cmdline.isset("symbols"))
69 {
71 "need to provide symbols to analyse via --symbols", "--symbols");
72 }
73
74 const bool core_file = cmdline.isset("core-file");
75 const bool breakpoint = cmdline.isset("breakpoint");
76
77 if(core_file && breakpoint)
78 {
80 "cannot start gdb from both core-file and breakpoint",
81 "--core-file/--breakpoint");
82 }
83
84 if(!core_file && !breakpoint)
85 {
87 "need to provide either core-file or breakpoint for gdb",
88 "--core-file/--breakpoint");
89 }
90
91 const bool output_file = cmdline.isset("output-file");
92 const bool symtab_snapshot = cmdline.isset("symtab-snapshot");
93
94 if(symtab_snapshot && output_file)
95 {
97 "printing to a file is not supported for symbol table snapshot output",
98 "--symtab-snapshot");
99 }
100
102
103 std::string binary = cmdline.args.front();
104
105 const std::string symbol_list(cmdline.get_value("symbols"));
106 std::vector<std::string> result = split_string(symbol_list, ',', true, true);
107
109
110 if(!opt.has_value())
111 {
113 "cannot read goto binary '" + binary + "'");
114 }
115
116 const goto_modelt goto_model(std::move(opt.value()));
117
118 gdb_value_extractort gdb_value_extractor(
119 goto_model.symbol_table, cmdline.args);
120 gdb_value_extractor.create_gdb_process();
121
122 if(core_file)
123 {
124 std::string core_file = cmdline.get_value("core-file");
125 gdb_value_extractor.run_gdb_from_core(core_file);
126 }
127 else if(breakpoint)
128 {
129 std::string breakpoint = cmdline.get_value("breakpoint");
130 gdb_value_extractor.run_gdb_to_breakpoint(breakpoint);
131 }
132
133 std::vector<irep_idt> result_ids(result.size());
135 result.begin(), result.end(), result_ids.begin(), [](std::string &name) {
136 return irep_idt{name};
137 });
138 gdb_value_extractor.analyze_symbols(result_ids);
139
140 std::ofstream file;
141
142 if(output_file)
143 {
144 file.open(cmdline.get_value("output-file"));
145 }
146
147 std::ostream &out =
148 output_file ? (std::ostream &)file : (std::ostream &)message.result();
149
150 if(symtab_snapshot)
151 {
152 symbol_tablet snapshot = gdb_value_extractor.get_snapshot_as_symbol_table();
153 show_symbol_table(snapshot, ui_message_handler);
154 }
155 else
156 {
157 std::string snapshot = gdb_value_extractor.get_snapshot_as_c_code();
158 out << snapshot;
159 }
160
161 if(output_file)
162 {
163 file.close();
164 }
165 else
166 {
167 message.result() << messaget::eom;
168 }
169
171}
172
174{
176 << '\n'
177 << banner_string("Memory-Analyzer", CBMC_VERSION) << '\n'
178 << align_center_with_border("Copyright (C) 2019") << '\n'
179 << align_center_with_border("Malte Mues, Diffblue Ltd.") << '\n'
180 << align_center_with_border("info@diffblue.com") << '\n'
181 << '\n'
182 << "Usage: Purpose:\n"
183 << '\n'
184 << " memory-analyzer [-?] [-h] [--help] show help\n"
185 << " memory-analyzer --version show"
186 << " version\n"
187 << " memory-analyzer --symbols <symbol-list> <options> <binary> analyze"
188 << " binary\n"
189 << "\n"
190 << " --core-file <file> analyze from core file\n"
191 << " --breakpoint <breakpoint> analyze from breakpoint\n"
192 << " --symbols <symbol-list> list of symbols to analyze\n"
193 << " --symtab-snapshot output snapshot as symbol table\n"
194 << " --output-file <file> write snapshot to file\n"
195 << " --json-ui output snapshot in JSON format\n"
196 << messaget::eom;
197}
static abstract_object_pointert transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
High-level interface to gdb.
std::unique_ptr< languaget > new_ansi_c_language()
std::string get_value(char option) const
Definition: cmdline.cpp:48
virtual bool isset(char option) const
Definition: cmdline.cpp:30
argst args
Definition: cmdline.h:145
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
Interface for extracting values from GDB (building on gdb_apit)
bool run_gdb_to_breakpoint(const std::string &breakpoint)
void run_gdb_from_core(const std::string &corefile)
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
memory_analyzer_parse_optionst(int argc, const char *argv[])
static eomt eom
Definition: message.h:297
mstreamt & status() const
Definition: message.h:414
ui_message_handlert ui_message_handler
Definition: parse_options.h:45
The symbol table.
Definition: symbol_table.h:14
configt config
Definition: config.cpp:25
Document and give macros for the exit codes of CPROVER binaries.
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Definition: exit_codes.h:16
Symbol Table + CFG.
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:206
This code does the command line parsing for the memory-analyzer tool.
#define MEMORY_ANALYZER_OPTIONS
void register_language(language_factoryt factory)
Register a language Note: registering a language is required for using the functions in language_util...
Definition: mode.cpp:39
STL namespace.
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
std::string banner_string(const std::string &front_end, const std::string &version)
static bool read_goto_binary(const std::string &filename, symbol_tablet &, goto_functionst &, message_handlert &)
Read a goto binary from a file, but do not update config.
Read Goto Programs.
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
Show the symbol table.
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Definition: kdev_t.h:19
const char * CBMC_VERSION