CBMC
memory_analyzer_parse_options.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Memory Analyzer
4 
5 Author: Malte Mues <mail.mues@gmail.com>
6  Daniel Poetzl
7 
8 \*******************************************************************/
9 
12 
14 
15 #include <util/config.h>
16 #include <util/exit_codes.h>
17 #include <util/help_formatter.h>
18 #include <util/message.h>
19 #include <util/version.h>
20 
24 
25 #include <ansi-c/ansi_c_language.h>
26 #include <langapi/mode.h>
27 
28 #include "analyze_symbol.h"
29 
30 #include <fstream> // IWYU pragma: keep
31 #include <iostream>
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  std::cout << CBMC_VERSION << '\n';
57  return CPROVER_EXIT_SUCCESS;
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 
106 
107  if(!opt.has_value())
108  {
110  "cannot read goto binary '" + binary + "'");
111  }
112 
113  const goto_modelt goto_model(std::move(opt.value()));
114 
115  gdb_value_extractort gdb_value_extractor(
116  goto_model.symbol_table, cmdline.args);
117  gdb_value_extractor.create_gdb_process();
118 
119  if(core_file)
120  {
121  std::string core_file = cmdline.get_value("core-file");
122  gdb_value_extractor.run_gdb_from_core(core_file);
123  }
124  else if(breakpoint)
125  {
126  std::string breakpoint = cmdline.get_value("breakpoint");
127  gdb_value_extractor.run_gdb_to_breakpoint(breakpoint);
128  }
129 
130  gdb_value_extractor.analyze_symbols(
132 
133  std::ofstream file;
134 
135  if(output_file)
136  {
137  file.open(cmdline.get_value("output-file"));
138  }
139 
140  std::ostream &out =
141  output_file ? (std::ostream &)file : (std::ostream &)message.result();
142 
143  if(symtab_snapshot)
144  {
145  symbol_tablet snapshot = gdb_value_extractor.get_snapshot_as_symbol_table();
147  }
148  else
149  {
150  std::string snapshot = gdb_value_extractor.get_snapshot_as_c_code();
151  out << snapshot;
152  }
153 
154  if(output_file)
155  {
156  file.close();
157  }
158  else
159  {
161  }
162 
163  return CPROVER_EXIT_SUCCESS;
164 }
165 
167 {
168  std::cout << '\n'
169  << banner_string("Memory-Analyzer", CBMC_VERSION) << '\n'
170  << align_center_with_border("Copyright (C) 2019") << '\n'
171  << align_center_with_border("Malte Mues, Diffblue Ltd.") << '\n'
172  << align_center_with_border("info@diffblue.com") << '\n';
173 
174  // clang-format off
175  std::cout << help_formatter(
176  "\n"
177  "Usage: \tPurpose:\n"
178  "\n"
179  " {bmemory-analyzer} [{y-?}] [{y-h}] [{y--help}] \t show this help\n"
180  " {bmemory-analyzer} {y--version} \t show version\n"
181  " {bmemory-analyzer} [options] {y--symbols} {usymbol-list} {ubinary} \t"
182  " analyze {ubinary}\n"
183  "\n"
184  "Main options:\n"
185  " {y--core-file} {ufile_name} \t analyze from core file {ufile_name}\n"
186  " {y--breakpoint} {uname} \t analyze from breakpoint {uname}\n"
187  " {y--symbols} {usymbol-list} \t list of symbols to analyze\n"
188  " {y--symtab-snapshot} \t output snapshot as symbol table\n"
189  " {y--output-file} {ufile_name} \t write snapshot to file {ufile_name}\n"
190  " {y--json-ui} \t output snapshot in JSON format\n"
191  "\n");
192  // clang-format on
193 }
High-level interface to gdb.
std::unique_ptr< languaget > new_ansi_c_language()
configt config
Definition: config.cpp:25
unsigned char opt
Definition: cegis.c:20
std::string get_value(char option) const
Definition: cmdline.cpp:48
virtual bool isset(char option) const
Definition: cmdline.cpp:30
std::list< std::string > get_comma_separated_values(const char *option) const
Collect all occurrences of option option and split their values on each comma, merging them into a si...
Definition: cmdline.cpp:131
argst args
Definition: cmdline.h:154
bool set(const cmdlinet &cmdline)
Definition: config.cpp:863
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)
std::string get_snapshot_as_c_code()
Get memory snapshot as C code.
void analyze_symbols(const std::list< std::string > &symbols)
For each input symbol in symbols: map its value address to its symbol_exprt (via the values map) and ...
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 ...
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:31
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[])
mstreamt & result() const
Definition: message.h:401
static eomt eom
Definition: message.h:289
ui_message_handlert ui_message_handler
Definition: parse_options.h:45
The symbol table.
Definition: symbol_table.h:14
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.
Help Formatter.
static help_formattert help_formatter(const std::string &s)
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:187
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
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_table_baset &symbol_table, ui_message_handlert &ui)
Show the symbol table.
const char * CBMC_VERSION