cprover
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 #include "analyze_symbol.h"
15 #include "gdb_api.h"
16 
17 #include <algorithm>
18 #include <fstream>
19 
20 #include <ansi-c/ansi_c_language.h>
21 
25 
26 #include <langapi/mode.h>
27 
28 #include <util/config.h>
29 #include <util/exit_codes.h>
30 #include <util/message.h>
31 #include <util/string_utils.h>
32 #include <util/version.h>
33 
35  int argc,
36  const char *argv[])
39  argc,
40  argv,
41  std::string("MEMORY-ANALYZER ") + CBMC_VERSION),
42  message(ui_message_handler)
43 {
44 }
45 
47 {
48  if(cmdline.isset("version"))
49  {
50  message.status() << CBMC_VERSION << '\n';
51  return CPROVER_EXIT_SUCCESS;
52  }
53 
55 
56  if(cmdline.args.size() < 1)
57  {
59  "no binary provided for analysis", "<binary> <args>");
60  }
61 
62  if(!cmdline.isset("symbols"))
63  {
65  "need to provide symbols to analyse via --symbols", "--symbols");
66  }
67 
68  const bool core_file = cmdline.isset("core-file");
69  const bool breakpoint = cmdline.isset("breakpoint");
70 
71  if(core_file && breakpoint)
72  {
74  "cannot start gdb from both core-file and breakpoint",
75  "--core-file/--breakpoint");
76  }
77 
78  if(!core_file && !breakpoint)
79  {
81  "need to provide either core-file or breakpoint for gdb",
82  "--core-file/--breakpoint");
83  }
84 
85  const bool output_file = cmdline.isset("output-file");
86  const bool symtab_snapshot = cmdline.isset("symtab-snapshot");
87 
88  if(symtab_snapshot && output_file)
89  {
91  "printing to a file is not supported for symbol table snapshot output",
92  "--symtab-snapshot");
93  }
94 
96 
97  std::string binary = cmdline.args.front();
98 
99  const std::string symbol_list(cmdline.get_value("symbols"));
100  std::vector<std::string> result = split_string(symbol_list, ',', true, true);
101 
103 
104  if(!opt.has_value())
105  {
107  "cannot read goto binary '" + binary + "'");
108  }
109 
110  const goto_modelt goto_model(std::move(opt.value()));
111 
112  gdb_value_extractort gdb_value_extractor(
113  goto_model.symbol_table, cmdline.args);
114  gdb_value_extractor.create_gdb_process();
115 
116  if(core_file)
117  {
118  std::string core_file = cmdline.get_value("core-file");
119  gdb_value_extractor.run_gdb_from_core(core_file);
120  }
121  else if(breakpoint)
122  {
123  std::string breakpoint = cmdline.get_value("breakpoint");
124  gdb_value_extractor.run_gdb_to_breakpoint(breakpoint);
125  }
126 
127  std::vector<irep_idt> result_ids(result.size());
128  std::transform(
129  result.begin(), result.end(), result_ids.begin(), [](std::string &name) {
130  return irep_idt{name};
131  });
132  gdb_value_extractor.analyze_symbols(result_ids);
133 
134  std::ofstream file;
135 
136  if(output_file)
137  {
138  file.open(cmdline.get_value("output-file"));
139  }
140 
141  std::ostream &out =
142  output_file ? (std::ostream &)file : (std::ostream &)message.result();
143 
144  if(symtab_snapshot)
145  {
146  symbol_tablet snapshot = gdb_value_extractor.get_snapshot_as_symbol_table();
147  show_symbol_table(snapshot, ui_message_handler);
148  }
149  else
150  {
151  std::string snapshot = gdb_value_extractor.get_snapshot_as_c_code();
152  out << snapshot;
153  }
154 
155  if(output_file)
156  {
157  file.close();
158  }
159  else
160  {
161  message.result() << messaget::eom;
162  }
163 
164  return CPROVER_EXIT_SUCCESS;
165 }
166 
168 {
169  message.status()
170  << '\n'
171  << banner_string("Memory-Analyzer", CBMC_VERSION) << '\n'
172  << align_center_with_border("Copyright (C) 2019") << '\n'
173  << align_center_with_border("Malte Mues, Diffblue Ltd.") << '\n'
174  << align_center_with_border("info@diffblue.com") << '\n'
175  << '\n'
176  << "Usage: Purpose:\n"
177  << '\n'
178  << " memory-analyzer [-?] [-h] [--help] show help\n"
179  << " memory-analyzer --version show"
180  << " version\n"
181  << " memory-analyzer --symbols <symbol-list> <options> <binary> analyze"
182  << " binary\n"
183  << "\n"
184  << " --core-file <file> analyze from core file\n"
185  << " --breakpoint <breakpoint> analyze from breakpoint\n"
186  << " --symbols <symbol-list> list of symbols to analyze\n"
187  << " --symtab-snapshot output snapshot as symbol table\n"
188  << " --output-file <file> write snapshot to file\n"
189  << " --json-ui output snapshot in JSON format\n"
190  << messaget::eom;
191 }
cmdlinet::args
argst args
Definition: cmdline.h:91
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
parse_options_baset::ui_message_handler
ui_message_handlert ui_message_handler
Definition: parse_options.h:42
parse_options_baset
Definition: parse_options.h:20
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:29
string_utils.h
messaget::status
mstreamt & status() const
Definition: message.h:414
deserialization_exceptiont
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
Definition: exception_utils.h:73
memory_analyzer_parse_optionst::message
messaget message
Definition: memory_analyzer_parse_options.h:39
file
Definition: kdev_t.h:19
goto_model.h
Symbol Table + CFG.
goto_modelt
Definition: goto_model.h:26
mode.h
messaget::eom
static eomt eom
Definition: message.h:297
show_symbol_table
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
Definition: show_symbol_table.cpp:268
version.h
gdb_api.h
Low-level interface to gdb.
gdb_value_extractort::create_gdb_process
void create_gdb_process()
Definition: analyze_symbol.h:62
message
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
Definition: static_verifier.cpp:74
split_string
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Definition: string_utils.cpp:40
CBMC_VERSION
const char * CBMC_VERSION
banner_string
std::string banner_string(const std::string &front_end, const std::string &version)
Definition: parse_options.cpp:163
gdb_value_extractort
Interface for extracting values from GDB (building on gdb_apit)
Definition: analyze_symbol.h:35
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:47
show_symbol_table.h
Show the symbol table.
gdb_value_extractort::run_gdb_to_breakpoint
bool run_gdb_to_breakpoint(const std::string &breakpoint)
Definition: analyze_symbol.h:66
read_goto_binary.h
Read Goto Programs.
analyze_symbol.h
High-level interface to gdb.
config
configt config
Definition: config.cpp:24
register_language
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:38
MEMORY_ANALYZER_OPTIONS
#define MEMORY_ANALYZER_OPTIONS
Definition: memory_analyzer_parse_options.h:20
ansi_c_language.h
memory_analyzer_parse_optionst::doit
int doit() override
Definition: memory_analyzer_parse_options.cpp:46
memory_analyzer_parse_optionst::memory_analyzer_parse_optionst
memory_analyzer_parse_optionst(int argc, const char *argv[])
Definition: memory_analyzer_parse_options.cpp:34
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
exit_codes.h
Document and give macros for the exit codes of CPROVER binaries.
memory_analyzer_parse_optionst::help
void help() override
Definition: memory_analyzer_parse_options.cpp:167
new_ansi_c_language
std::unique_ptr< languaget > new_ansi_c_language()
Definition: ansi_c_language.cpp:143
binary
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:204
config.h
read_goto_binary
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.
Definition: read_goto_binary.cpp:59
memory_analyzer_parse_options.h
This code does the command line parsing for the memory-analyzer tool.
CPROVER_EXIT_SUCCESS
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Definition: exit_codes.h:16
message.h
invalid_command_line_argument_exceptiont
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition: exception_utils.h:38
parse_options_baset::cmdline
cmdlinet cmdline
Definition: parse_options.h:28
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
align_center_with_border
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
Definition: parse_options.cpp:150
gdb_value_extractort::run_gdb_from_core
void run_gdb_from_core(const std::string &corefile)
Definition: analyze_symbol.h:70