31 #ifdef POINTER_ANALYSIS_FI 116 catch(
const std::string e)
127 catch(std::bad_alloc)
173 status() <<
"remove soundly function pointers" <<
eom;
183 status() <<
"Replace pthread_creates by __CPROVER_ASYNC_0:" <<
eom;
195 status() <<
"Propagate Constant Function Pointers" <<
eom;
203 status() <<
"Function Pointer Removal" <<
eom;
212 #ifdef POINTER_ANALYSIS_FI 219 value_set_analysis(goto_functions);
228 status() <<
"Shared variables accesses detection" <<
eom;
237 status() <<
"Shared variables accesses detection (CF)" <<
eom;
246 status() <<
"Detection of variables declared volatile" <<
eom;
258 const unsigned unwind_loops=
262 const unsigned max_po_trans=
286 status() <<
"Fence detection for " << mm
287 <<
" via critical cycles and ILP" <<
eom;
305 const unsigned unwind_loops =
309 const unsigned max_var =
313 const unsigned max_po_trans =
319 status() <<
"Adding weak memory (TSO) Instrumentation" <<
eom;
324 status() <<
"Adding weak memory (PSO) Instrumentation" <<
eom;
329 status() <<
"Adding weak memory (RMO) Instrumentation" <<
eom;
334 status() <<
"Adding weak memory (Power) Instrumentation" <<
eom;
339 status() <<
"Unknown weak memory model" <<
eom;
411 " musketeer [-?] [-h] [--help] show help\n" 416 " --mm <tso,pso,rmo,power> detects all the fences to insert for a weak\n" 419 "Alternative methods:\n" 422 " --all-shared detects and fences all the accesses to shared\n" 423 " variables (context insensitive)\n" 425 " --all-shared-aeg detects all the accesses to shared variables\n" 426 " (context sensitive)\n" 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" 432 " --naive detects all the pairs to be delayed in a naive\n" 433 " approach (context sensitive)\n" 437 " --remove-function-pointers removes soundly function pointers based on\n" 438 " their signatures\n" 440 " --async replaces all the pthread_creates by CPROVER_ASYNC\n" 441 " --const-function-pointer-propagation\n" 443 " propagates the constant pointers to functions\n" 445 " --scc detects cycles in parallel (one thread/SCC)\n" 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" 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" 456 " --ignore-arrays ignores cycles with multiple accesses to the\n"
#define MUSKETEER_VERSION
symbol_tablet symbol_table
void instrument_goto_program(goto_functionst &goto_functions)
void remove_asm(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes assembler
Remove Indirect Function Calls.
instrumentation_strategyt
virtual void register_languages()
unsigned unsafe_string2unsigned(const std::string &str, int base)
void fence_all_shared_aeg(message_handlert &message_handler, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions)
void link_to_library(goto_modelt &goto_model, message_handlert &message_handler)
std::string get_value(char option) const
void fence_volatile(message_handlert &message_handler, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions)
static mstreamt & eom(mstreamt &m)
Weak Memory Instrumentation for Threaded Goto Programs.
Remove 'asm' statements by compiling into suitable standard code.
Fence insertion following criteria of Pensieve (PPoPP'05)
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 compute_loop_numbers()
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)
Constant Function Pointer Propagation.
bool read_goto_binary(const std::string &filename, goto_modelt &dest, message_handlert &message_handler)
virtual bool isset(char option) const
virtual int doit()
invoke main modules
void get_goto_program(goto_functionst &goto_functions)
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)
void set_from_symbol_table(const symbol_tablet &)
void propagate_const_function_pointers(symbol_tablet &symbol_table, goto_functionst &goto_functions, message_handlert &message_handler)
message_handlert & get_message_handler()
void replace_async(const namespacet &ns, goto_functionst &goto_functions)
void set_verbosity(unsigned _verbosity)
Value Set Propagation (flow insensitive)
void set_option(const std::string &option, const bool value)
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.
virtual void help()
display command line help
void label_properties(goto_modelt &goto_model)
Field-insensitive, location-sensitive may-alias analysis.
ui_message_handlert ui_message_handler
void fence_all_shared(message_handlert &message_handler, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions)
Race Detection for Threaded Goto Programs.