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/config.h>
19 #include <util/options.h>
20 #include <util/memory_info.h>
21 
22 #include <ansi-c/ansi_c_language.h>
23 #include <cpp/cpp_language.h>
24 
29 #include <goto-programs/loop_ids.h>
32 
33 #include <goto-instrument/dump_c.h>
34 
35 #include <langapi/mode.h>
36 
37 
40  language_uit(cmdline, ui_message_handler),
41  ui_message_handler(cmdline, "CLOBBER " CBMC_VERSION)
42 {
43 }
44 
46 {
47  if(config.set(cmdline))
48  {
49  usage_error();
50  exit(1);
51  }
52 
53  if(cmdline.isset("debug-level"))
54  options.set_option("debug-level", cmdline.get_value("debug-level"));
55 
56  if(cmdline.isset("unwindset"))
57  options.set_option("unwindset", cmdline.get_value("unwindset"));
58 
59  // all checks supported by goto_check
61 
62  // check assertions
63  if(cmdline.isset("no-assertions"))
64  options.set_option("assertions", false);
65  else
66  options.set_option("assertions", true);
67 
68  // use assumptions
69  if(cmdline.isset("no-assumptions"))
70  options.set_option("assumptions", false);
71  else
72  options.set_option("assumptions", true);
73 
74  // magic error label
75  if(cmdline.isset("error-label"))
76  options.set_option("error-label", cmdline.get_value("error-label"));
77 }
78 
81 {
82  if(cmdline.isset("version"))
83  {
84  std::cout << CBMC_VERSION << '\n';
85  return 0;
86  }
87 
90 
91  //
92  // command line options
93  //
94 
95  optionst options;
96  get_command_line_options(options);
97 
100 
101  goto_modelt goto_model;
102 
103  try
104  {
106 
107 
108  // show it?
109  if(cmdline.isset("show-loops"))
110  {
111  show_loop_ids(get_ui(), goto_model);
112  return 6;
113  }
114 
115  // show it?
116  if(
117  cmdline.isset("show-goto-functions") ||
118  cmdline.isset("list-goto-functions"))
119  {
121  goto_model,
124  cmdline.isset("list-goto-functions"));
125  return 6;
126  }
127 
128  label_properties(goto_model);
129 
130  if(cmdline.isset("show-properties"))
131  {
132  show_properties(goto_model, get_message_handler(), get_ui());
133  return 0;
134  }
135 
136  set_properties(goto_model.goto_functions);
137 
138  // do instrumentation
139 
140  const namespacet ns(goto_model.symbol_table);
141 
142  std::ofstream out("simulator.c");
143 
144  if(!out)
145  throw std::string("failed to create file simulator.c");
146 
147  dump_c(goto_model.goto_functions, true, false, false, ns, out);
148 
149  status() << "instrumentation complete; compile and execute simulator.c"
150  << eom;
151 
152  return 0;
153  }
154 
155  catch(const std::string &error_msg)
156  {
157  error() << error_msg << messaget::eom;
158  return 8;
159  }
160 
161  catch(const char *error_msg)
162  {
163  error() << error_msg << messaget::eom;
164  return 8;
165  }
166 
167  catch(const std::bad_alloc &)
168  {
169  error() << "Out of memory" << messaget::eom;
170  return 8;
171  }
172 
173  #if 0
174  // let's log some more statistics
175  debug() << "Memory consumption:" << messaget::endl;
176  memory_info(debug());
177  debug() << eom;
178  #endif
179 }
180 
182 {
183  if(cmdline.isset("property"))
184  ::set_properties(goto_functions, cmdline.get_values("property"));
185 
186  return false;
187 }
188 
190  const optionst &options,
191  goto_modelt &goto_model)
192 {
193  {
194  // do partial inlining
195  status() << "Partial Inlining" << eom;
197 
198  // add generic checks
199  status() << "Generic Property Instrumentation" << eom;
200  goto_check(options, goto_model);
201 
202  // recalculate numbers, etc.
203  goto_model.goto_functions.update();
204 
205  // add loop ids
207 
208  // if we aim to cover, replace
209  // all assertions by false to prevent simplification
210 
211  if(cmdline.isset("cover-assertions"))
212  make_assertions_false(goto_model);
213  }
214 
215  return false;
216 }
217 
218 #if 0
219 void clobber_parse_optionst::report_properties(
220  const path_searcht::property_mapt &property_map)
221 {
222  for(const auto &prop_pair : property_map)
223  {
224  if(get_ui()==ui_message_handlert::XML_UI)
225  {
226  xmlt xml_result("result");
227  xml_result.set_attribute("claim", id2string(prop_pair.first));
228 
229  std::string status_string;
230 
231  switch(prop_pair.second.status)
232  {
233  case path_searcht::PASS: status_string="OK"; break;
234  case path_searcht::FAIL: status_string="FAILURE"; break;
235  case path_searcht::NOT_REACHED: status_string="OK"; break;
236  }
237 
238  xml_result.set_attribute("status", status_string);
239 
240  std::cout << xml_result << "\n";
241  }
242  else
243  {
244  status() << "[" << prop_pair.first << "] "
245  << prop_pair.second.description << ": ";
246  switch(prop_pair.second.status)
247  {
248  case path_searcht::PASS: status() << "OK"; break;
249  case path_searcht::FAIL: status() << "FAILED"; break;
250  case path_searcht::NOT_REACHED: status() << "OK"; break;
251  }
252  status() << eom;
253  }
254 
255  if(cmdline.isset("show-trace") &&
256  prop_pair.second.status==path_searcht::FAIL)
257  show_counterexample(prop_pair.second.error_trace);
258  }
259 
260  if(!cmdline.isset("property"))
261  {
262  status() << eom;
263 
264  unsigned failed=0;
265 
266  for(const auto &prop_pair : property_map)
267  if(prop_pair.second.status==path_searcht::FAIL)
268  failed++;
269 
270  status() << "** " << failed
271  << " of " << property_map.size() << " failed"
272  << eom;
273  }
274 }
275 #endif
276 
278 {
279  result() << "VERIFICATION SUCCESSFUL" << eom;
280 
281  switch(get_ui())
282  {
284  break;
285 
287  {
288  xmlt xml("cprover-status");
289  xml.data="SUCCESS";
290  std::cout << xml;
291  std::cout << '\n';
292  }
293  break;
294 
295  default:
296  UNREACHABLE;
297  }
298 }
299 
301  const goto_tracet &error_trace)
302 {
303  const namespacet ns(symbol_table);
304 
305  switch(get_ui())
306  {
308  std::cout << "\nCounterexample:\n";
309  show_goto_trace(std::cout, ns, error_trace);
310  break;
311 
313  {
314  xmlt xml;
315  convert(ns, error_trace, xml);
316  std::cout << xml << '\n';
317  }
318  break;
319 
320  default:
321  UNREACHABLE;
322  }
323 }
324 
326 {
327  result() << "VERIFICATION FAILED" << eom;
328 
329  switch(get_ui())
330  {
332  break;
333 
335  {
336  xmlt xml("cprover-status");
337  xml.data="FAILURE";
338  std::cout << xml;
339  std::cout << '\n';
340  }
341  break;
342 
343  default:
344  UNREACHABLE;
345  }
346 }
347 
350 {
351  // clang-format off
352  std::cout << '\n' << banner_string("CLOBBER", CBMC_VERSION) << '\n'
353  <<
354  "* * Copyright (C) 2014 * *\n"
355  "* * Daniel Kroening * *\n"
356  "* * University of Oxford * *\n"
357  "* * kroening@kroening.com * *\n"
358  "\n"
359  "Usage: Purpose:\n"
360  "\n"
361  " symex [-?] [-h] [--help] show help\n"
362  " symex file.c ... source file names\n"
363  "\n"
364  "Frontend options:\n"
365  " -I path set include path (C/C++)\n"
366  " -D macro define preprocessor macro (C/C++)\n"
367  " --preprocess stop after preprocessing\n"
368  " --16, --32, --64 set width of int\n"
369  " --LP64, --ILP64, --LLP64,\n"
370  " --ILP32, --LP32 set width of int, long and pointers\n"
371  " --little-endian allow little-endian word-byte conversions\n"
372  " --big-endian allow big-endian word-byte conversions\n"
373  " --unsigned-char make \"char\" unsigned by default\n"
374  " --show-parse-tree show parse tree\n"
375  " --show-symbol-table show loaded symbol table\n"
377  " --ppc-macos set MACOS/PPC architecture\n"
378  " --mm model set memory model (default: sc)\n"
379  " --arch set architecture (default: "
380  << configt::this_architecture() << ")\n"
381  " --os set operating system (default: "
382  << configt::this_operating_system() << ")\n"
383  #ifdef _WIN32
384  " --gcc use GCC as preprocessor\n"
385  #endif
386  " --no-arch don't set up an architecture\n"
387  " --no-library disable built-in abstract C library\n"
388  // NOLINTNEXTLINE(whitespace/line_length)
389  " --round-to-nearest IEEE floating point rounding mode (default)\n"
390  " --round-to-plus-inf IEEE floating point rounding mode\n"
391  " --round-to-minus-inf IEEE floating point rounding mode\n"
392  " --round-to-zero IEEE floating point rounding mode\n"
393  "\n"
394  "Program instrumentation options:\n"
396  " --show-properties show the properties\n"
397  " --no-assertions ignore user assertions\n"
398  " --no-assumptions ignore user assumptions\n"
399  " --error-label label check that label is unreachable\n"
400  "\n"
401  "Symex options:\n"
402  " --function name set main function name\n"
403  " --property nr only check one specific property\n"
404  " --depth nr limit search depth\n"
405  " --context-bound nr limit number of context switches\n"
406  " --unwind nr unwind nr times\n"
407  "\n"
408  "Other options:\n"
409  " --version show version and exit\n"
410  " --xml-ui use XML-formatted output\n"
411  "\n";
412  // clang-format on
413 }
symbol_tablet symbol_table
Definition: language_ui.h:25
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:110
void show_counterexample(const class goto_tracet &)
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition: loop_ids.cpp:21
std::unique_ptr< languaget > new_cpp_language()
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
Command Line Parsing.
ui_message_handlert ui_message_handler
uit get_ui() const
Definition: ui_message.h:37
uit get_ui()
Definition: language_ui.h:48
void compute_loop_numbers()
static unsigned eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest...
Definition: message.cpp:78
void make_assertions_false(goto_modelt &goto_model)
Read Goto Programs.
Dump C from Goto Program.
std::string get_value(char option) const
Definition: cmdline.cpp:45
void show_goto_trace(std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace)
Definition: goto_trace.cpp:247
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
void show_goto_functions(const namespacet &ns, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_functionst &goto_functions, bool list_only)
configt config
Definition: config.cpp:23
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:25
bool set_properties(goto_functionst &)
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:42
virtual int doit()
invoke main modules
bool set(const cmdlinet &cmdline)
Definition: config.cpp:737
void dump_c(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &ns, std::ostream &out)
Definition: dump_c.cpp:1400
virtual bool isset(char option) const
Definition: cmdline.cpp:27
Initialize a Goto Program.
#define CLOBBER_OPTIONS
virtual void help()
display command line help
bool process_goto_program(const optionst &options, goto_modelt &)
mstreamt & error() const
Definition: message.h:302
C++ Language Module.
TO_BE_DOCUMENTED.
Definition: namespace.h:74
Function Inlining.
static mstreamt & endl(mstreamt &m)
Definition: message.h:290
Loop IDs.
Definition: xml.h:18
Traces of GOTO Programs.
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_tablet &symbol_table, message_handlert &message_handler)
std::string data
Definition: xml.h:30
std::string banner_string(const std::string &front_end, const std::string &version)
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check.h:56
void goto_check(const namespacet &ns, const optionst &options, const irep_idt &mode, goto_functionst::goto_functiont &goto_function)
void get_command_line_options(optionst &)
static irep_idt this_operating_system()
Definition: config.cpp:1309
message_handlert & get_message_handler()
Definition: message.h:153
mstreamt & result() const
Definition: message.h:312
mstreamt & status() const
Definition: message.h:317
#define HELP_SHOW_GOTO_FUNCTIONS
clobber_parse_optionst(int argc, const char **argv)
#define UNREACHABLE
Definition: invariant.h:250
goto_modelt initialize_goto_model(const cmdlinet &cmdline, message_handlert &message_handler)
void memory_info(std::ostream &out)
Definition: memory_info.cpp:28
std::unique_ptr< languaget > new_ansi_c_language()
Options.
virtual void usage_error()
Show the properties.
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
void set_option(const std::string &option, const bool value)
Definition: options.cpp:24
TO_BE_DOCUMENTED.
Definition: goto_trace.h:152
mstreamt & debug() const
Definition: message.h:332
void label_properties(goto_modelt &goto_model)
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
static irep_idt this_architecture()
Definition: config.cpp:1212
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)