cprover
symex_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 "symex_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 #include <util/unicode.h>
24 
25 #include <ansi-c/ansi_c_language.h>
26 #include <cpp/cpp_language.h>
28 
34 #include <goto-programs/loop_ids.h>
45 
48 
49 #include <goto-instrument/cover.h>
50 
51 #include <langapi/mode.h>
52 
53 #include <cbmc/version.h>
54 
55 #include <path-symex/locs.h>
56 
57 #include "path_search.h"
58 
59 symex_parse_optionst::symex_parse_optionst(int argc, const char **argv):
61  language_uit(cmdline, ui_message_handler),
62  ui_message_handler(cmdline, "Symex " CBMC_VERSION)
63 {
64 }
65 
67 {
68  // this is our default verbosity
70 
71  if(cmdline.isset("verbosity"))
72  {
73  v=unsafe_string2int(cmdline.get_value("verbosity"));
74  if(v<0)
75  v=0;
76  else if(v>10)
77  v=10;
78  }
79 
81 }
82 
84 {
85  if(config.set(cmdline))
86  {
87  usage_error();
88  exit(1);
89  }
90 
91  if(cmdline.isset("debug-level"))
92  options.set_option("debug-level", cmdline.get_value("debug-level"));
93 
94  if(cmdline.isset("unwindset"))
95  options.set_option("unwindset", cmdline.get_value("unwindset"));
96 
97  // all checks supported by goto_check
99 
100  // check assertions
101  if(cmdline.isset("no-assertions"))
102  options.set_option("assertions", false);
103  else
104  options.set_option("assertions", true);
105 
106  // use assumptions
107  if(cmdline.isset("no-assumptions"))
108  options.set_option("assumptions", false);
109  else
110  options.set_option("assumptions", true);
111 
112  // magic error label
113  if(cmdline.isset("error-label"))
114  options.set_option("error-label", cmdline.get_values("error-label"));
115 }
116 
119 {
120  if(cmdline.isset("version"))
121  {
122  std::cout << CBMC_VERSION << '\n';
123  return 0;
124  }
125 
129 
130  //
131  // command line options
132  //
133 
134  optionst options;
135  get_command_line_options(options);
136 
137  eval_verbosity();
138 
140  return 6;
141 
142  if(process_goto_program(options))
143  return 6;
144 
146 
147  if(cmdline.isset("show-properties"))
148  {
150  return 0;
151  }
152 
153  if(set_properties())
154  return 7;
155 
156  if(cmdline.isset("show-locs"))
157  {
159  locst locs(ns);
161  locs.output(std::cout);
162  return 0;
163  }
164 
165  // do actual Symex
166 
167  try
168  {
170  path_searcht path_search(ns);
171 
173 
174  if(cmdline.isset("depth"))
175  path_search.set_depth_limit(
177 
178  if(cmdline.isset("context-bound"))
179  path_search.set_context_bound(
180  unsafe_string2unsigned(cmdline.get_value("context-bound")));
181 
182  if(cmdline.isset("branch-bound"))
183  path_search.set_branch_bound(
184  unsafe_string2unsigned(cmdline.get_value("branch-bound")));
185 
186  if(cmdline.isset("unwind"))
187  path_search.set_unwind_limit(
189 
190  if(cmdline.isset("max-search-time"))
191  path_search.set_time_limit(
192  safe_string2unsigned(cmdline.get_value("max-search-time")));
193 
194  if(cmdline.isset("dfs"))
195  path_search.set_dfs();
196 
197  if(cmdline.isset("bfs"))
198  path_search.set_bfs();
199 
200  if(cmdline.isset("locs"))
201  path_search.set_locs();
202 
203  if(cmdline.isset("show-vcc"))
204  {
205  path_search.show_vcc=true;
206  path_search(goto_model.goto_functions);
207  return 0;
208  }
209 
210  path_search.eager_infeasibility=
211  cmdline.isset("eager-infeasibility");
212 
213  if(cmdline.isset("cover"))
214  {
215  // test-suite generation
216  path_search(goto_model.goto_functions);
217  report_cover(path_search.property_map);
218  return 0;
219  }
220  else
221  {
222  // do actual symex, for assertion checking
223  switch(path_search(goto_model.goto_functions))
224  {
226  report_properties(path_search.property_map);
227  report_success();
228  return 0;
229 
231  report_properties(path_search.property_map);
232  report_failure();
233  return 10;
234 
235  default:
236  return 8;
237  }
238  }
239  }
240 
241  catch(const std::string error_msg)
242  {
243  error() << error_msg << messaget::eom;
244  return 8;
245  }
246 
247  catch(const char *error_msg)
248  {
249  error() << error_msg << messaget::eom;
250  return 8;
251  }
252 
253  #if 0
254  // let's log some more statistics
255  debug() << "Memory consumption:" << messaget::endl;
256  memory_info(debug());
257  debug() << eom;
258  #endif
259 }
260 
262 {
263  try
264  {
265  if(cmdline.isset("property"))
266  ::set_properties(
268  }
269 
270  catch(const char *e)
271  {
272  error() << e << eom;
273  return true;
274  }
275 
276  catch(const std::string e)
277  {
278  error() << e << eom;
279  return true;
280  }
281 
282  catch(int)
283  {
284  return true;
285  }
286 
287  return false;
288 }
289 
291 {
292  try
293  {
294  // we add the library
296 
297  // do partial inlining
298  status() << "Partial Inlining" << eom;
300 
301  // add generic checks
302  status() << "Generic Property Instrumentation" << eom;
303  goto_check(options, goto_model);
304 
305  // remove stuff
308  // remove function pointers
309  status() << "Removal of function pointers and virtual functions" << eom;
312  goto_model,
313  cmdline.isset("pointer-check"));
314  // Java virtual functions -> explicit dispatch tables:
316  // Java throw and catch -> explicit exceptional return variables:
318  // Java instanceof -> clsid comparison:
322 
323  // recalculate numbers, etc.
325 
326  // add loop ids
328 
329  if(cmdline.isset("drop-unused-functions"))
330  {
331  // Entry point will have been set before and function pointers removed
332  status() << "Removing unused functions" << eom;
334  }
335 
336  if(cmdline.isset("cover"))
337  {
338  std::string criterion=cmdline.get_value("cover");
339 
341 
342  if(criterion=="assertion" || criterion=="assertions")
344  else if(criterion=="path" || criterion=="paths")
346  else if(criterion=="branch" || criterion=="branches")
348  else if(criterion=="location" || criterion=="locations")
350  else if(criterion=="decision" || criterion=="decisions")
352  else if(criterion=="condition" || criterion=="conditions")
354  else if(criterion=="mcdc")
356  else if(criterion=="cover")
358  else
359  {
360  error() << "unknown coverage criterion" << eom;
361  return true;
362  }
363 
364  status() << "Instrumenting coverage goals" << eom;
367  }
368 
369  // show it?
370  if(cmdline.isset("show-loops"))
371  {
373  return true;
374  }
375 
376  // show it?
377  if(cmdline.isset("show-goto-functions"))
378  {
380  return true;
381  }
382  }
383 
384  catch(const char *e)
385  {
386  error() << e << eom;
387  return true;
388  }
389 
390  catch(const std::string e)
391  {
392  error() << e << eom;
393  return true;
394  }
395 
396  catch(int)
397  {
398  return true;
399  }
400 
401  catch(std::bad_alloc)
402  {
403  error() << "Out of memory" << eom;
404  return true;
405  }
406 
407  return false;
408 }
409 
411  const path_searcht::property_mapt &property_map)
412 {
414  status() << "\n** Results:" << eom;
415 
416  for(path_searcht::property_mapt::const_iterator
417  it=property_map.begin();
418  it!=property_map.end();
419  it++)
420  {
422  {
423  xmlt xml_result("result");
424  xml_result.set_attribute("claim", id2string(it->first));
425 
426  std::string status_string;
427 
428  switch(it->second.status)
429  {
430  case path_searcht::SUCCESS: status_string="SUCCESS"; break;
431  case path_searcht::FAILURE: status_string="FAILURE"; break;
432  case path_searcht::NOT_REACHED: status_string="SUCCESS"; break;
433  }
434 
435  xml_result.set_attribute("status", status_string);
436 
437  std::cout << xml_result << "\n";
438  }
439  else
440  {
441  status() << "[" << it->first << "] "
442  << it->second.description << ": ";
443  switch(it->second.status)
444  {
445  case path_searcht::SUCCESS: status() << "SUCCESS"; break;
446  case path_searcht::FAILURE: status() << "FAILURE"; break;
447  case path_searcht::NOT_REACHED: status() << "SUCCESS"; break;
448  }
449  status() << eom;
450  }
451 
452  if((cmdline.isset("show-trace") ||
453  cmdline.isset("trace")) &&
454  it->second.is_failure())
455  show_counterexample(it->second.error_trace);
456  }
457 
458  if(!cmdline.isset("property"))
459  {
460  status() << eom;
461 
462  unsigned failed=0;
463 
464  for(path_searcht::property_mapt::const_iterator
465  it=property_map.begin();
466  it!=property_map.end();
467  it++)
468  if(it->second.is_failure())
469  failed++;
470 
471  status() << "** " << failed
472  << " of " << property_map.size() << " failed"
473  << eom;
474  }
475 }
476 
478 {
479  result() << "VERIFICATION SUCCESSFUL" << eom;
480 
481  switch(get_ui())
482  {
484  break;
485 
487  {
488  xmlt xml("cprover-status");
489  xml.data="SUCCESS";
490  std::cout << xml;
491  std::cout << '\n';
492  }
493  break;
494 
495  default:
496  assert(false);
497  }
498 }
499 
501  const goto_tracet &error_trace)
502 {
504 
505  switch(get_ui())
506  {
508  std::cout << '\n' << "Counterexample:" << '\n';
509  show_goto_trace(std::cout, ns, error_trace);
510  break;
511 
513  {
514  xmlt xml;
515  convert(ns, error_trace, xml);
516  std::cout << xml << std::flush;
517  }
518  break;
519 
520  default:
521  assert(false);
522  }
523 }
524 
526 {
527  result() << "VERIFICATION FAILED" << eom;
528 
529  switch(get_ui())
530  {
532  break;
533 
535  {
536  xmlt xml("cprover-status");
537  xml.data="FAILURE";
538  std::cout << xml;
539  std::cout << '\n';
540  }
541  break;
542 
543  default:
544  assert(false);
545  }
546 }
547 
550 {
551  std::cout <<
552  "\n"
553  "* * Symex " CBMC_VERSION " - Copyright (C) 2013 ";
554 
555  std::cout << "(" << (sizeof(void *)*8) << "-bit version)";
556 
557  std::cout << " * *\n";
558 
559  std::cout <<
560  "* * Daniel Kroening * *\n"
561  "* * University of Oxford * *\n"
562  "* * kroening@kroening.com * *\n"
563  "\n"
564  "Usage: Purpose:\n"
565  "\n"
566  " symex [-?] [-h] [--help] show help\n"
567  " symex file.c ... source file names\n"
568  "\n"
569  "Analysis options:\n"
570  // NOLINTNEXTLINE(whitespace/line_length)
571  " --show-properties show the properties, but don't run analysis\n"
572  " --property id only check one specific property\n"
573  // NOLINTNEXTLINE(whitespace/line_length)
574  " --stop-on-fail stop analysis once a failed property is detected\n"
575  // NOLINTNEXTLINE(whitespace/line_length)
576  " --trace give a counterexample trace for failed properties\n"
577  "\n"
578  "Frontend options:\n"
579  " -I path set include path (C/C++)\n"
580  " -D macro define preprocessor macro (C/C++)\n"
581  " --preprocess stop after preprocessing\n"
582  " --16, --32, --64 set width of int\n"
583  " --LP64, --ILP64, --LLP64,\n"
584  " --ILP32, --LP32 set width of int, long and pointers\n"
585  " --little-endian allow little-endian word-byte conversions\n"
586  " --big-endian allow big-endian word-byte conversions\n"
587  " --unsigned-char make \"char\" unsigned by default\n"
588  " --show-parse-tree show parse tree\n"
589  " --show-symbol-table show symbol table\n"
591  " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
592  " --ppc-macos set MACOS/PPC architecture\n"
593  " --mm model set memory model (default: sc)\n"
594  " --arch set architecture (default: "
595  << configt::this_architecture() << ")\n"
596  " --os set operating system (default: "
597  << configt::this_operating_system() << ")\n"
598  #ifdef _WIN32
599  " --gcc use GCC as preprocessor\n"
600  #endif
601  " --no-arch don't set up an architecture\n"
602  " --no-library disable built-in abstract C library\n"
603  // NOLINTNEXTLINE(whitespace/line_length)
604  " --round-to-nearest IEEE floating point rounding mode (default)\n"
605  " --round-to-plus-inf IEEE floating point rounding mode\n"
606  " --round-to-minus-inf IEEE floating point rounding mode\n"
607  " --round-to-zero IEEE floating point rounding mode\n"
608  " --function name set main function name\n"
609  "\n"
610  "Program instrumentation options:\n"
612  " --no-assertions ignore user assertions\n"
613  " --no-assumptions ignore user assumptions\n"
614  " --error-label label check that label is unreachable\n"
615  "\n"
616  "Symex options:\n"
617  " --unwind nr unwind nr times\n"
618  " --depth nr limit search depth\n"
619  " --context-bound nr limit number of context switches\n"
620  " --branch-bound nr limit number of branches taken\n"
621  " --max-search-time s limit search to approximately s seconds\n"
622  "\n"
623  "Other options:\n"
624  " --version show version and exit\n"
625  " --xml-ui use XML-formatted output\n"
626  " --verbosity # verbosity level\n"
627  "\n";
628 }
coverage_criteriont
Definition: cover.h:22
Command Line Parsing.
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
Symbolic Execution.
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 report_cover(const path_searcht::property_mapt &)
Definition: symex_cover.cpp:46
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
Remove function exceptional returns.
property_mapt property_map
Definition: path_search.h:103
Remove Instance-of Operators.
Remove Indirect Function Calls.
std::map< irep_idt, property_entryt > property_mapt
Definition: path_search.h:102
Remove Virtual Function (Method) Calls.
mstreamt & status()
Definition: message.h:238
void remove_unused_functions(goto_functionst &functions, message_handlert &message_handler)
void goto_check(const namespacet &ns, const optionst &options, goto_functionst::goto_functiont &goto_function)
uit get_ui()
Definition: language_ui.h:47
void set_branch_bound(int limit)
Definition: path_search.h:53
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:66
languaget * new_ansi_c_language()
Read Goto Programs.
Remove the &#39;complex&#39; data type by compilation into structs.
bool process_goto_program(const optionst &options)
virtual void help()
display command line help
std::string get_value(char option) const
Definition: cmdline.cpp:46
ui_message_handlert ui_message_handler
void show_properties(const namespacet &ns, const irep_idt &identifier, ui_message_handlert::uit ui, const goto_programt &goto_program)
symbol_tablet symbol_table
Definition: goto_model.h:25
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 remove_exceptions(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes throws/CATCH-POP/CATCH-PUSH
void output(std::ostream &out) const
Definition: locs.cpp:84
void remove_virtual_functions(const symbol_tablet &symbol_table, goto_functionst &goto_functions)
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
#define SYMEX_OPTIONS
Unused function removal.
bool set(const cmdlinet &cmdline)
Definition: config.cpp:727
virtual bool isset(char option) const
Definition: cmdline.cpp:30
void remove_instanceof(symbol_tablet &symbol_table, goto_functionst &goto_functions)
See function above.
Initialize a Goto Program.
void instrument_cover_goals(const symbol_tablet &symbol_table, goto_programt &goto_program, coverage_criteriont criterion)
Definition: cover.cpp:832
void set_dfs()
Definition: path_search.h:98
void get_command_line_options(optionst &options)
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.
bool remove_function_pointers(message_handlert &_message_handler, symbol_tablet &symbol_table, const goto_functionst &goto_functions, goto_programt &goto_program, bool add_safety_assertion, bool only_remove_const_fps)
void set_time_limit(int limit)
Definition: path_search.h:63
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
void set_depth_limit(int limit)
Definition: path_search.h:43
std::string data
Definition: xml.h:30
bool eager_infeasibility
Definition: path_search.h:69
void adjust_float_expressions(exprt &expr, const namespacet &ns)
This adds the rounding mode to floating-point operations, including those in vectors and complex numb...
languaget * new_java_bytecode_language()
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check.h:55
Symbolic Execution.
void set_bfs()
Definition: path_search.h:99
void set_unwind_limit(int limit)
Definition: path_search.h:58
unsigned safe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:51
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
Definition: locs.h:39
void set_context_bound(int limit)
Definition: path_search.h:48
void report_properties(const path_searcht::property_mapt &)
symex_parse_optionst(int argc, const char **argv)
Path-based Symbolic Execution.
void set_locs()
Definition: path_search.h:100
void memory_info(std::ostream &out)
Definition: memory_info.cpp:28
mstreamt & error()
Definition: message.h:223
Remove the &#39;vector&#39; data type by compilation into arrays.
void set_verbosity(unsigned _verbosity)
Definition: message.h:44
#define CBMC_VERSION
Definition: version.h:4
CFG made of Program Locations, built from goto_functionst.
Options.
virtual void usage_error()
Show the properties.
void rewrite_union(exprt &expr, const namespacet &ns)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL, 0, v)
void register_language(language_factoryt factory)
Definition: mode.cpp:31
Coverage Instrumentation.
virtual int doit()
invoke main modules
void set_option(const std::string &option, const bool value)
Definition: options.cpp:24
TO_BE_DOCUMENTED.
Definition: goto_trace.h:146
static void remove_complex(typet &)
removes complex data type
void show_goto_functions(const namespacet &ns, ui_message_handlert::uit ui, const goto_functionst &goto_functions)
int unsafe_string2int(const std::string &str, int base)
Definition: string2int.cpp:61
void label_properties(goto_modelt &goto_model)
bool initialize_goto_model(goto_modelt &goto_model, const cmdlinet &cmdline, message_handlert &message_handler)
goto_functionst goto_functions
Definition: goto_model.h:26
static void remove_vector(typet &)
removes vector data type
static irep_idt this_architecture()
Definition: config.cpp:1148
void show_counterexample(const class goto_tracet &)
void build(const goto_functionst &goto_functions)
Definition: locs.cpp:20