cprover
clobber_parse_options.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symex Command Line Options Processing
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "clobber_parse_options.h"
13 
14 #include <iostream>
15 #include <fstream>
16 #include <cstdlib>
17 
18 #include <util/string2int.h>
19 #include <util/config.h>
20 #include <util/language.h>
21 #include <util/options.h>
22 #include <util/memory_info.h>
23 
24 #include <ansi-c/ansi_c_language.h>
25 #include <cpp/cpp_language.h>
26 
31 #include <goto-programs/loop_ids.h>
35 
36 #include <goto-instrument/dump_c.h>
37 
38 #include <langapi/mode.h>
39 
40 #include <cbmc/version.h>
41 
42 // #include "clobber_instrumenter.h"
43 
46  language_uit(cmdline, ui_message_handler),
47  ui_message_handler(cmdline, "CLOBBER " CBMC_VERSION)
48 {
49 }
50 
52 {
53  // this is our default verbosity
55 
56  if(cmdline.isset("verbosity"))
57  {
58  v=unsafe_string2int(cmdline.get_value("verbosity"));
59  if(v<0)
60  v=0;
61  else if(v>10)
62  v=10;
63  }
64 
66 }
67 
69 {
70  if(config.set(cmdline))
71  {
72  usage_error();
73  exit(1);
74  }
75 
76  if(cmdline.isset("debug-level"))
77  options.set_option("debug-level", cmdline.get_value("debug-level"));
78 
79  if(cmdline.isset("unwindset"))
80  options.set_option("unwindset", cmdline.get_value("unwindset"));
81 
82  // all checks supported by goto_check
84 
85  // check assertions
86  if(cmdline.isset("no-assertions"))
87  options.set_option("assertions", false);
88  else
89  options.set_option("assertions", true);
90 
91  // use assumptions
92  if(cmdline.isset("no-assumptions"))
93  options.set_option("assumptions", false);
94  else
95  options.set_option("assumptions", true);
96 
97  // magic error label
98  if(cmdline.isset("error-label"))
99  options.set_option("error-label", cmdline.get_value("error-label"));
100 }
101 
104 {
105  if(cmdline.isset("version"))
106  {
107  std::cout << CBMC_VERSION << '\n';
108  return 0;
109  }
110 
113 
114  //
115  // command line options
116  //
117 
118  optionst options;
119  get_command_line_options(options);
120 
121  eval_verbosity();
122 
123  goto_functionst goto_functions;
124 
125  try
126  {
127  if(get_goto_program(options, goto_functions))
128  return 6;
129 
130  label_properties(goto_functions);
131 
132  if(cmdline.isset("show-properties"))
133  {
134  const namespacet ns(symbol_table);
135  show_properties(ns, get_ui(), goto_functions);
136  return 0;
137  }
138 
139  set_properties(goto_functions);
140 
141  // do instrumentation
142 
143  const namespacet ns(symbol_table);
144 
145  std::ofstream out("simulator.c");
146 
147  if(!out)
148  throw std::string("failed to create file simulator.c");
149 
150  dump_c(goto_functions, true, false, ns, out);
151 
152  status() << "instrumentation complete; compile and execute simulator.c"
153  << eom;
154 
155  return 0;
156  }
157 
158  catch(const std::string error_msg)
159  {
160  error() << error_msg << messaget::eom;
161  return 8;
162  }
163 
164  catch(const char *error_msg)
165  {
166  error() << error_msg << messaget::eom;
167  return 8;
168  }
169 
170  catch(std::bad_alloc)
171  {
172  error() << "Out of memory" << messaget::eom;
173  return 8;
174  }
175 
176  #if 0
177  // let's log some more statistics
178  debug() << "Memory consumption:" << messaget::endl;
179  memory_info(debug());
180  debug() << eom;
181  #endif
182 }
183 
185 {
186  if(cmdline.isset("property"))
187  ::set_properties(goto_functions, cmdline.get_values("property"));
188 
189  return false;
190 }
191 
193  const optionst &options,
194  goto_functionst &goto_functions)
195 {
196  if(cmdline.args.empty())
197  {
198  error() << "Please provide a program to verify" << eom;
199  return true;
200  }
201 
202  {
203  if(cmdline.args.size()==1 &&
205  {
206  status() << "Reading GOTO program from file" << eom;
207 
209  symbol_table, goto_functions, get_message_handler()))
210  return true;
211 
213 
214  if(cmdline.isset("show-symbol-table"))
215  {
217  return true;
218  }
219 
220  irep_idt entry_point=goto_functions.entry_point();
221 
222  if(symbol_table.symbols.find(entry_point)==symbol_table.symbols.end())
223  {
224  error() << "The goto binary has no entry point; please complete linking"
225  << eom;
226  return true;
227  }
228  }
229  else if(cmdline.isset("show-parse-tree"))
230  {
231  if(cmdline.args.size()!=1)
232  {
233  error() << "Please give one source file only" << eom;
234  return true;
235  }
236 
237  std::string filename=cmdline.args[0];
238 
239  #ifdef _MSC_VER
240  std::ifstream infile(widen(filename));
241  #else
242  std::ifstream infile(filename);
243  #endif
244 
245  if(!infile)
246  {
247  error() << "failed to open input file `" << filename << "'" << eom;
248  return true;
249  }
250 
251  languaget *language=get_language_from_filename(filename);
252 
253  if(language==nullptr)
254  {
255  error() << "failed to figure out type of file `" << filename << "'"
256  << eom;
257  return true;
258  }
259 
261 
262  status() << "Parsing " << filename << eom;
263 
264  if(language->parse(infile, filename))
265  {
266  error() << "PARSING ERROR" << eom;
267  return true;
268  }
269 
270  language->show_parse(std::cout);
271  return true;
272  }
273  else
274  {
275  if(parse() ||
276  typecheck() ||
277  final())
278  return true;
279 
280  // we no longer need any parse trees or language files
281  clear_parse();
282 
283  if(cmdline.isset("show-symbol-table"))
284  {
286  return true;
287  }
288 
289  irep_idt entry_point=goto_functions.entry_point();
290 
291  if(symbol_table.symbols.find(entry_point)==symbol_table.symbols.end())
292  {
293  error() << "No entry point; please provide a main function" << eom;
294  return true;
295  }
296 
297  status() << "Generating GOTO Program" << eom;
298 
299  goto_convert(symbol_table, goto_functions, ui_message_handler);
300  }
301 
302  // finally add the library
303  #if 0
305  #endif
306 
307  if(process_goto_program(options, goto_functions))
308  return true;
309  }
310 
311  return false;
312 }
313 
315  const optionst &options,
316  goto_functionst &goto_functions)
317 {
318  {
320 
321  // do partial inlining
322  status() << "Partial Inlining" << eom;
323  goto_partial_inline(goto_functions, ns, ui_message_handler);
324 
325  // add generic checks
326  status() << "Generic Property Instrumentation" << eom;
327  goto_check(ns, options, goto_functions);
328 
329  // recalculate numbers, etc.
330  goto_functions.update();
331 
332  // add loop ids
333  goto_functions.compute_loop_numbers();
334 
335  // if we aim to cover, replace
336  // all assertions by false to prevent simplification
337 
338  if(cmdline.isset("cover-assertions"))
339  make_assertions_false(goto_functions);
340 
341  // show it?
342  if(cmdline.isset("show-loops"))
343  {
344  show_loop_ids(get_ui(), goto_functions);
345  return true;
346  }
347 
348  // show it?
349  if(cmdline.isset("show-goto-functions"))
350  {
351  show_goto_functions(ns, get_ui(), goto_functions);
352  return true;
353  }
354  }
355 
356  return false;
357 }
358 
359 #if 0
360 void clobber_parse_optionst::report_properties(
361  const path_searcht::property_mapt &property_map)
362 {
363  for(const auto &prop_pair : property_map)
364  {
365  if(get_ui()==ui_message_handlert::XML_UI)
366  {
367  xmlt xml_result("result");
368  xml_result.set_attribute("claim", id2string(prop_pair.first));
369 
370  std::string status_string;
371 
372  switch(prop_pair.second.status)
373  {
374  case path_searcht::PASS: status_string="OK"; break;
375  case path_searcht::FAIL: status_string="FAILURE"; break;
376  case path_searcht::NOT_REACHED: status_string="OK"; break;
377  }
378 
379  xml_result.set_attribute("status", status_string);
380 
381  std::cout << xml_result << "\n";
382  }
383  else
384  {
385  status() << "[" << prop_pair.first << "] "
386  << prop_pair.second.description << ": ";
387  switch(prop_pair.second.status)
388  {
389  case path_searcht::PASS: status() << "OK"; break;
390  case path_searcht::FAIL: status() << "FAILED"; break;
391  case path_searcht::NOT_REACHED: status() << "OK"; break;
392  }
393  status() << eom;
394  }
395 
396  if(cmdline.isset("show-trace") &&
397  prop_pair.second.status==path_searcht::FAIL)
398  show_counterexample(prop_pair.second.error_trace);
399  }
400 
401  if(!cmdline.isset("property"))
402  {
403  status() << eom;
404 
405  unsigned failed=0;
406 
407  for(const auto &prop_pair : property_map)
408  if(prop_pair.second.status==path_searcht::FAIL)
409  failed++;
410 
411  status() << "** " << failed
412  << " of " << property_map.size() << " failed"
413  << eom;
414  }
415 }
416 #endif
417 
419 {
420  result() << "VERIFICATION SUCCESSFUL" << eom;
421 
422  switch(get_ui())
423  {
425  break;
426 
428  {
429  xmlt xml("cprover-status");
430  xml.data="SUCCESS";
431  std::cout << xml;
432  std::cout << '\n';
433  }
434  break;
435 
436  default:
437  assert(false);
438  }
439 }
440 
442  const goto_tracet &error_trace)
443 {
444  const namespacet ns(symbol_table);
445 
446  switch(get_ui())
447  {
449  std::cout << "\nCounterexample:\n";
450  show_goto_trace(std::cout, ns, error_trace);
451  break;
452 
454  {
455  xmlt xml;
456  convert(ns, error_trace, xml);
457  std::cout << xml << '\n';
458  }
459  break;
460 
461  default:
462  assert(false);
463  }
464 }
465 
467 {
468  result() << "VERIFICATION FAILED" << eom;
469 
470  switch(get_ui())
471  {
473  break;
474 
476  {
477  xmlt xml("cprover-status");
478  xml.data="FAILURE";
479  std::cout << xml;
480  std::cout << '\n';
481  }
482  break;
483 
484  default:
485  assert(false);
486  }
487 }
488 
491 {
492  std::cout <<
493  "\n"
494  "* * CLOBBER " CBMC_VERSION " - Copyright (C) 2014 ";
495 
496  std::cout << "(" << (sizeof(void *)*8) << "-bit version)";
497 
498  std::cout << " * *\n";
499 
500  std::cout <<
501  "* * Daniel Kroening * *\n"
502  "* * University of Oxford * *\n"
503  "* * kroening@kroening.com * *\n"
504  "\n"
505  "Usage: Purpose:\n"
506  "\n"
507  " symex [-?] [-h] [--help] show help\n"
508  " symex file.c ... source file names\n"
509  "\n"
510  "Frontend options:\n"
511  " -I path set include path (C/C++)\n"
512  " -D macro define preprocessor macro (C/C++)\n"
513  " --preprocess stop after preprocessing\n"
514  " --16, --32, --64 set width of int\n"
515  " --LP64, --ILP64, --LLP64,\n"
516  " --ILP32, --LP32 set width of int, long and pointers\n"
517  " --little-endian allow little-endian word-byte conversions\n"
518  " --big-endian allow big-endian word-byte conversions\n"
519  " --unsigned-char make \"char\" unsigned by default\n"
520  " --show-parse-tree show parse tree\n"
521  " --show-symbol-table show symbol table\n"
523  " --ppc-macos set MACOS/PPC architecture\n"
524  " --mm model set memory model (default: sc)\n"
525  " --arch set architecture (default: "
526  << configt::this_architecture() << ")\n"
527  " --os set operating system (default: "
528  << configt::this_operating_system() << ")\n"
529  #ifdef _WIN32
530  " --gcc use GCC as preprocessor\n"
531  #endif
532  " --no-arch don't set up an architecture\n"
533  " --no-library disable built-in abstract C library\n"
534  // NOLINTNEXTLINE(whitespace/line_length)
535  " --round-to-nearest IEEE floating point rounding mode (default)\n"
536  " --round-to-plus-inf IEEE floating point rounding mode\n"
537  " --round-to-minus-inf IEEE floating point rounding mode\n"
538  " --round-to-zero IEEE floating point rounding mode\n"
539  "\n"
540  "Program instrumentation options:\n"
542  " --show-properties show the properties\n"
543  " --no-assertions ignore user assertions\n"
544  " --no-assumptions ignore user assumptions\n"
545  " --error-label label check that label is unreachable\n"
546  "\n"
547  "Symex options:\n"
548  " --function name set main function name\n"
549  " --property nr only check one specific property\n"
550  " --depth nr limit search depth\n"
551  " --context-bound nr limit number of context switches\n"
552  " --unwind nr unwind nr times\n"
553  "\n"
554  "Other options:\n"
555  " --version show version and exit\n"
556  " --xml-ui use XML-formatted output\n"
557  "\n";
558 }
symbol_tablet symbol_table
Definition: language_ui.h:24
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:90
bool set_properties(goto_functionst &goto_functions)
void show_counterexample(const class goto_tracet &)
mstreamt & result()
Definition: message.h:233
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition: loop_ids.cpp:21
void goto_convert(const codet &code, symbol_tablet &symbol_table, goto_programt &dest, message_handlert &message_handler)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
virtual bool parse()
Definition: language_ui.cpp:37
Command Line Parsing.
ui_message_handlert ui_message_handler
std::wstring widen(const char *s)
Definition: unicode.cpp:56
std::map< irep_idt, property_entryt > property_mapt
Definition: path_search.h:102
mstreamt & status()
Definition: message.h:238
void goto_check(const namespacet &ns, const optionst &options, goto_functionst::goto_functiont &goto_function)
uit get_ui()
Definition: language_ui.h:47
void make_assertions_false(goto_modelt &goto_model)
languaget * new_ansi_c_language()
bool is_goto_binary(const std::string &filename)
Read Goto Programs.
Dump C from Goto Program.
std::string get_value(char option) const
Definition: cmdline.cpp:46
void show_properties(const namespacet &ns, const irep_idt &identifier, ui_message_handlert::uit ui, const goto_programt &goto_program)
virtual bool typecheck()
Definition: language_ui.cpp:99
virtual void show_symbol_table(bool brief=false)
void show_goto_trace(std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace)
Definition: goto_trace.cpp:239
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
configt config
Definition: config.cpp:21
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:25
void goto_partial_inline(goto_modelt &goto_model, message_handlert &message_handler, unsigned smallfunc_limit, bool adjust_function)
Inline all function calls to functions either marked as "inlined" or smaller than smallfunc_limit (by...
Set the properties to check.
#define HELP_GOTO_CHECK
Definition: goto_check.h:41
virtual int doit()
invoke main modules
bool set(const cmdlinet &cmdline)
Definition: config.cpp:727
bool read_goto_binary(const std::string &filename, goto_modelt &dest, message_handlert &message_handler)
argst args
Definition: cmdline.h:35
virtual bool isset(char option) const
Definition: cmdline.cpp:30
symbolst symbols
Definition: symbol_table.h:57
#define CLOBBER_OPTIONS
virtual void help()
display command line help
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:174
C++ Language Module.
TO_BE_DOCUMENTED.
Definition: namespace.h:62
Function Inlining.
static mstreamt & endl(mstreamt &m)
Definition: message.h:211
Abstract interface to support a programming language.
Loop IDs.
Definition: xml.h:18
Traces of GOTO Programs.
languaget * new_cpp_language()
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:122
void convert(const goto_functionst::goto_functiont &function, xmlt &xml)
takes a goto_function and creates an according xml structure
std::string data
Definition: xml.h:30
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check.h:55
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1091
bool get_goto_program(const optionst &options, goto_functionst &goto_functions)
bool process_goto_program(const optionst &options, goto_functionst &goto_functions)
virtual void show_parse(std::ostream &out)=0
virtual void clear_parse()
Definition: language_ui.h:36
static irep_idt this_operating_system()
Definition: config.cpp:1258
mstreamt & debug()
Definition: message.h:253
message_handlert & get_message_handler()
Definition: message.h:127
Goto Programs with Functions.
#define HELP_SHOW_GOTO_FUNCTIONS
languaget * get_language_from_filename(const std::string &filename)
Definition: mode.cpp:51
clobber_parse_optionst(int argc, const char **argv)
void memory_info(std::ostream &out)
Definition: memory_info.cpp:28
void dump_c(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const namespacet &ns, std::ostream &out)
Definition: dump_c.cpp:1644
mstreamt & error()
Definition: message.h:223
void set_verbosity(unsigned _verbosity)
Definition: message.h:44
#define CBMC_VERSION
Definition: version.h:4
Options.
virtual void usage_error()
Show the properties.
void register_language(language_factoryt factory)
Definition: mode.cpp:31
void set_option(const std::string &option, const bool value)
Definition: options.cpp:24
TO_BE_DOCUMENTED.
Definition: goto_trace.h:146
void show_goto_functions(const namespacet &ns, ui_message_handlert::uit ui, const goto_functionst &goto_functions)
virtual bool parse(std::istream &instream, const std::string &path)=0
void get_command_line_options(optionst &options)
int unsafe_string2int(const std::string &str, int base)
Definition: string2int.cpp:61
void label_properties(goto_modelt &goto_model)
static irep_idt this_architecture()
Definition: config.cpp:1148