cprover
musketeer_parse_options.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Main Module
4 
5 Author:
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <fstream>
15 #include <iostream>
16 #include <memory>
17 
18 #include <util/config.h>
19 #include <util/options.h>
20 #include <util/string2int.h>
21 
30 
31 #ifdef POINTER_ANALYSIS_FI
33 #else
35 #endif
36 
39 
41 
42 #include <goto-instrument/rw_set.h>
44 
46 #include "version.h"
47 #include "fencer.h"
48 #include "fence_shared.h"
49 #include "pensieve.h"
50 #include "replace_async.h"
51 #include "infer_mode.h"
52 
54 {
55  unsigned int v=8; // default
56 
57  if(cmdline.isset("verbosity"))
58  {
60  if(v>10)
61  v=10;
62  }
63 
65 }
66 
69 {
70  if(cmdline.isset("version"))
71  {
72  std::cout << MUSKETEER_VERSION << '\n';
73  return 0;
74  }
75 
76  if(cmdline.args.size()!=1 && cmdline.args.size()!=2)
77  {
78  help();
79  return 0;
80  }
81 
82  set_verbosity();
83 
84  try
85  {
87 
88  goto_functionst goto_functions;
89 
90  get_goto_program(goto_functions);
91 
92  instrument_goto_program(goto_functions);
93 
94  // write new binary?
95  if(cmdline.args.size()==2)
96  {
97  status() << "Writing GOTO program to " << cmdline.args[1] << eom;
98 
100  cmdline.args[1], symbol_table, goto_functions, get_message_handler()))
101  return 1;
102  else
103  return 0;
104  }
105 
106  // help();
107  return 0;
108  }
109 
110  catch(const char *e)
111  {
112  error() << e << eom;
113  return 11;
114  }
115 
116  catch(const std::string e)
117  {
118  error() << e << eom;
119  return 11;
120  }
121 
122  catch(int)
123  {
124  return 11;
125  }
126 
127  catch(std::bad_alloc)
128  {
129  error() << "Out of memory" << eom;
130  return 11;
131  }
132 }
133 
135  goto_functionst &goto_functions)
136 {
137  status() << "Reading GOTO program from " << cmdline.args[0] << eom;
138 
140  symbol_table, goto_functions, get_message_handler()))
141  throw 0;
142 
144 }
145 
147  goto_functionst &goto_functions)
148 {
149  optionst options;
150 
151  // unwind loops
152  if(cmdline.isset("unwind"))
153  {
154  status() << "Unwinding loops" << eom;
155  options.set_option("unwind", cmdline.get_value("unwind"));
156  }
157 
158  // we add the library, as some analyses benefit
159 
161 
163 
164  if( cmdline.isset("mm")
165  || cmdline.isset("all-shared")
166  || cmdline.isset("volatile")
167  || cmdline.isset("pensieve")
168  || cmdline.isset("naive")
169  || cmdline.isset("all-shared-aeg") )
170  {
171  if(cmdline.isset("remove-function-pointers"))
172  {
173  status() << "remove soundly function pointers" << eom;
176  symbol_table,
177  goto_functions,
178  cmdline.isset("pointer-check"));
179  }
180 
181  if(cmdline.isset("async"))
182  {
183  status() << "Replace pthread_creates by __CPROVER_ASYNC_0:" << eom;
184  replace_async(ns, goto_functions);
185  goto_functions.update();
186  }
187 
188  // do partial inlining
189  status() << "Partial Inlining" << eom;
190  goto_partial_inline(goto_functions, ns, ui_message_handler);
191 
192  if(cmdline.isset("const-function-pointer-propagation"))
193  {
194  /* propagate const pointers to functions */
195  status() << "Propagate Constant Function Pointers" << eom;
198  }
199 
200  // goto_functions.output(ns, std::cout);
201  // return;
202 #if 0
203  status() << "Function Pointer Removal" << eom;
206  symbol_table,
207  goto_functions,
208  cmdline.isset("pointer-check");
209 #endif
210 
211  status() << "Pointer Analysis" << eom;
212 #ifdef POINTER_ANALYSIS_FI
213  value_set_analysis_fit value_set_analysis(ns);
214 #else
215  value_set_analysist value_set_analysis(ns);
216 #endif
217 
218 #ifndef LOCAL_MAY
219  value_set_analysis(goto_functions);
220 #endif
221 
222  status() << "Removing asm code" << eom;
223  remove_asm(symbol_table, goto_functions);
224  goto_functions.update();
225 
226  if(cmdline.isset("all-shared"))
227  {
228  status() << "Shared variables accesses detection" << eom;
229  fence_all_shared(get_message_handler(), value_set_analysis, symbol_table,
230  goto_functions);
231  // simple analysis, coupled with script to insert;
232  // does not transform the goto-binary
233  return;
234  }
235  if(cmdline.isset("all-shared-aeg"))
236  {
237  status() << "Shared variables accesses detection (CF)" << eom;
238  fence_all_shared_aeg(get_message_handler(), value_set_analysis,
239  symbol_table, goto_functions);
240  // simple analysis, coupled with script to insert;
241  // does not transform the goto-binary
242  return;
243  }
244  else if(cmdline.isset("volatile"))
245  {
246  status() << "Detection of variables declared volatile" << eom;
247 
248  fence_volatile(get_message_handler(), value_set_analysis, symbol_table,
249  goto_functions);
250  // simple analysis, coupled with script to insert;
251  // does not transform the goto-binary
252  return;
253  }
254  else if(cmdline.isset("pensieve") || cmdline.isset("naive"))
255  {
256  status() << "Delay-set analysis" << eom;
257 
258  const unsigned unwind_loops=
259  cmdline.isset("unwind") ?
261 
262  const unsigned max_po_trans=
263  cmdline.isset("max-po-trans") ?
264  unsafe_string2unsigned(cmdline.get_value("max-po-trans")) : 0;
265 
267  value_set_analysis,
268  symbol_table,
269  goto_functions,
270  unwind_loops,
271  max_po_trans,
272  !cmdline.isset("no-po-rendering"),
273  cmdline.isset("render-cluster-file"),
274  cmdline.isset("render-cluster-function"),
275  cmdline.isset("naive"),
277  // simple analysis, coupled with script to insert;
278  // does not transform the goto-binary
279  return;
280  }
281  else if(cmdline.isset("mm"))
282  {
283  std::string mm=cmdline.get_value("mm");
284  memory_modelt model;
285 
286  status() << "Fence detection for " << mm
287  << " via critical cycles and ILP" << eom;
288 
289  // strategy of instrumentation
290  instrumentation_strategyt inst_strategy;
291  if(cmdline.isset("one-event-per-cycle"))
292  inst_strategy=one_event_per_cycle;
293  else if(cmdline.isset("minimum-interference"))
294  inst_strategy=min_interference;
295  else if(cmdline.isset("read-first"))
296  inst_strategy=read_first;
297  else if(cmdline.isset("write-first"))
298  inst_strategy=write_first;
299  else if(cmdline.isset("my-events"))
300  inst_strategy=my_events;
301  else
302  /* default: instruments all unsafe pairs */
303  inst_strategy=all;
304 
305  const unsigned unwind_loops =
306  cmdline.isset("unwind") ?
308 
309  const unsigned max_var =
310  cmdline.isset("max-var") ?
311  unsafe_string2unsigned(cmdline.get_value("max-var")) : 0;
312 
313  const unsigned max_po_trans =
314  cmdline.isset("max-po-trans") ?
315  unsafe_string2unsigned(cmdline.get_value("max-po-trans")) : 0;
316 
317  if(mm=="tso")
318  {
319  status() << "Adding weak memory (TSO) Instrumentation" << eom;
320  model=TSO;
321  }
322  else if(mm=="pso")
323  {
324  status() << "Adding weak memory (PSO) Instrumentation" << eom;
325  model=PSO;
326  }
327  else if(mm=="rmo")
328  {
329  status() << "Adding weak memory (RMO) Instrumentation" << eom;
330  model=RMO;
331  }
332  else if(mm=="power")
333  {
334  status() << "Adding weak memory (Power) Instrumentation" << eom;
335  model=Power;
336  }
337  else
338  {
339  status/*error*/() << "Unknown weak memory model" << eom;
340  model=Unknown;
341  }
342 
343  /* inference mode */
344  infer_modet infer_mode=INFER;
345 
346  if(cmdline.isset("userdef"))
347  infer_mode=USER_DEF;
348 
350 
351  if(cmdline.isset("force-loop-duplication"))
352  loops=all_loops;
353  if(cmdline.isset("no-loop-duplication"))
354  loops=no_loop;
355 
356  /*if(model!=Unknown)*/
358  model,
359  value_set_analysis,
360  symbol_table,
361  goto_functions,
362  cmdline.isset("scc"),
363  inst_strategy,
364  unwind_loops,
365  !cmdline.isset("cfg-kill"),
366  cmdline.isset("no-dependencies"),
367  loops,
368  max_var,
369  max_po_trans,
370  !cmdline.isset("no-po-rendering"),
371  cmdline.isset("render-cluster-file"),
372  cmdline.isset("render-cluster-function"),
373  cmdline.isset("cav11"),
374  cmdline.isset("hide-internals"),
375  cmdline.isset("print-graph"),
376  infer_mode,
378  cmdline.isset("ignore-arrays"));
379  }
380  }
381 
382  // add failed symbols
384 
385  // recalculate numbers, etc.
386  goto_functions.update();
387 
388  // add loop ids
389  goto_functions.compute_loop_numbers();
390 
391  // label the assertions
392  label_properties(goto_functions);
393 }
394 
397 {
398  std::cout <<
399  "\n"
400  "* * musketeer " MUSKETEER_VERSION " * *\n"
401  "\n"
402  " ~__\n"
403  " |)\n"
404  " /|_____\n"
405  " / |\n"
406  " /|\n"
407  " / |\n"
408  "\n"
409  "Usage: Purpose:\n"
410  "\n"
411  " musketeer [-?] [-h] [--help] show help\n"
412  "\n"
413  "Main options:\n"
414  "\n"
415  // NOLINTNEXTLINE(whitespace/line_length)
416  " --mm <tso,pso,rmo,power> detects all the fences to insert for a weak\n"
417  " memory model\n"
418  "\n"
419  "Alternative methods:\n"
420  "\n"
421  // NOLINTNEXTLINE(whitespace/line_length)
422  " --all-shared detects and fences all the accesses to shared\n"
423  " variables (context insensitive)\n"
424  // NOLINTNEXTLINE(whitespace/line_length)
425  " --all-shared-aeg detects all the accesses to shared variables\n"
426  " (context sensitive)\n"
427  // NOLINTNEXTLINE(whitespace/line_length)
428  " --volatile detects all the accesses to volatile variables\n"
429  " --pensieve detects all the pairs to be delayed with\n"
430  " Pensieve's criteria (context sensitive)\n"
431  // NOLINTNEXTLINE(whitespace/line_length)
432  " --naive detects all the pairs to be delayed in a naive\n"
433  " approach (context sensitive)\n"
434  "\n"
435  "Options:\n"
436  "\n"
437  " --remove-function-pointers removes soundly function pointers based on\n"
438  " their signatures\n"
439  // NOLINTNEXTLINE(whitespace/line_length)
440  " --async replaces all the pthread_creates by CPROVER_ASYNC\n"
441  " --const-function-pointer-propagation\n"
442  // NOLINTNEXTLINE(whitespace/line_length)
443  " propagates the constant pointers to functions\n"
444  // NOLINTNEXTLINE(whitespace/line_length)
445  " --scc detects cycles in parallel (one thread/SCC)\n"
446  // NOLINTNEXTLINE(whitespace/line_length)
447  " --force-loop-duplication duplicates the bodies of all the loops, and not\n"
448  " only those with arrays accesses\n"
449  " --no-loop-duplication constructs back-edges for all the loops\n"
450  // NOLINTNEXTLINE(whitespace/line_length)
451  " --no-dependencies ignores existing dependencies in the program\n"
452  " --print-graph prints the AEG into graph.dot\n"
453  " --max-po-var <n> limits the number of variables per cycle\n"
454  " --max-po-trans <n> limits the size of pos^+ in terms of pos\n"
455  // NOLINTNEXTLINE(whitespace/line_length)
456  " --ignore-arrays ignores cycles with multiple accesses to the\n"
457  " same array\n"
458  "\n";
459 }
Fence inference.
#define MUSKETEER_VERSION
Definition: version.h:4
symbol_tablet symbol_table
Definition: language_ui.h:24
void instrument_goto_program(goto_functionst &goto_functions)
void remove_asm(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes assembler
Definition: remove_asm.cpp:317
Remove Indirect Function Calls.
instrumentation_strategyt
Definition: wmm.h:26
mstreamt & status()
Definition: message.h:238
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:66
Definition: wmm.h:23
Definition: wmm.h:39
void fence_all_shared_aeg(message_handlert &message_handler, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions)
Read Goto Programs.
Command Line Parsing.
std::string get_value(char option) const
Definition: cmdline.cpp:46
Definition: wmm.h:22
void fence_volatile(message_handlert &message_handler, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions)
Pointer Dereferencing.
Definition: wmm.h:30
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
Weak Memory Instrumentation for Threaded Goto Programs.
configt config
Definition: config.cpp:21
Remove &#39;asm&#39; statements by compiling into suitable standard code.
Fence insertion following criteria of Pensieve (PPoPP&#39;05)
loop_strategyt
Definition: wmm.h:36
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.
void fence_weak_memory(memory_modelt model, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions, bool SCC, instrumentation_strategyt event_strategy, unsigned unwinding_bound, bool no_cfg_kill, bool no_dependencies, loop_strategyt duplicate_body, unsigned input_max_var, unsigned input_max_po_trans, bool render_po, bool render_file, bool render_function, bool cav11_option, bool hide_internals, bool print_graph, infer_modet mode, message_handlert &message_handler, bool ignore_arrays)
Definition: fencer.cpp:25
Constant Function Pointer Propagation.
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
memory_modelt
Definition: wmm.h:17
Value Set Propagation.
virtual int doit()
invoke main modules
void get_goto_program(goto_functionst &goto_functions)
TO_BE_DOCUMENTED.
Definition: namespace.h:62
Function Inlining.
Definition: wmm.h:21
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 fence_pensieve(value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions, unsigned unwinding_bound, unsigned input_max_po_trans, bool render_po, bool render_file, bool render_function, bool naive_mode, message_handlert &message_handler)
Definition: pensieve.cpp:19
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1091
Definition: wmm.h:32
void propagate_const_function_pointers(symbol_tablet &symbol_table, goto_functionst &goto_functions, message_handlert &message_handler)
message_handlert & get_message_handler()
Definition: message.h:127
Definition: wmm.h:19
Definition: wmm.h:20
mstreamt & error()
Definition: message.h:223
void replace_async(const namespacet &ns, goto_functionst &goto_functions)
Definition: replace_async.h:21
void set_verbosity(unsigned _verbosity)
Definition: message.h:44
Options.
Value Set Propagation (flow insensitive)
Definition: wmm.h:40
void set_option(const std::string &option, const bool value)
Definition: options.cpp:24
void add_failed_symbols(symbol_tablet &symbol_table)
bool write_goto_binary(std::ostream &out, const symbol_tablet &lsymbol_table, const goto_functionst &functions, int version)
Writes a goto program to disc.
Program Transformation.
virtual void help()
display command line help
void label_properties(goto_modelt &goto_model)
Write GOTO binaries.
infer_modet
Definition: infer_mode.h:13
(naive) Fence insertion
Field-insensitive, location-sensitive may-alias analysis.
void fence_all_shared(message_handlert &message_handler, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions)
Definition: wmm.h:28
Race Detection for Threaded Goto Programs.