cprover
pensieve.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Vincent Nimal
6 
7 \*******************************************************************/
8 
9 #include "pensieve.h"
10 
11 #include <util/cprover_prefix.h>
12 #include <util/namespace.h>
13 #include <util/message.h>
14 
16 #include <goto-instrument/rw_set.h>
18 
20  value_setst &value_sets,
21  symbol_tablet &symbol_table,
22  goto_functionst &goto_functions,
23  unsigned unwinding_bound,
24  unsigned input_max_po_trans,
25  bool render_po,
26  bool render_file,
27  bool render_function,
28  bool naive_mode,
29  message_handlert &message_handler)
30 {
31  messaget message(message_handler);
32 
33  message.status() << "--------" << messaget::eom;
34 
35  // all access to shared variables is pushed into assignments
36  Forall_goto_functions(f_it, goto_functions)
37  if(f_it->first!=CPROVER_PREFIX "initialize" &&
38  f_it->first!=goto_functionst::entry_point())
39  introduce_temporaries(value_sets, symbol_table, f_it->first,
40  f_it->second.body,
41 #ifdef LOCAL_MAY
42  f_it->second,
43 #endif
44  message);
45  message.status() << "Temporary variables added" << messaget::eom;
46 
47  unsigned max_thds = 0;
48 
49  instrumenter_pensievet instrumenter(symbol_table, goto_functions, message);
50  max_thds=instrumenter.goto2graph_cfg(value_sets, Power, true, no_loop);
51  message.status() << "Abstract event graph computed" << messaget::eom;
52 
53  if(input_max_po_trans!=0)
54  instrumenter.set_parameters_collection(0, input_max_po_trans);
55  else
56  instrumenter.set_parameters_collection(max_thds);
57 
58  /* necessary for correct printings */
59  namespacet ns(symbol_table);
60 
61  if(naive_mode)
62  instrumenter.collect_pairs_naive(ns);
63  else
64  instrumenter.collect_pairs(ns);
65 
66  /* removes potential skips */
67  Forall_goto_functions(f_it, goto_functions)
68  remove_skip(f_it->second.body);
69 
70  // update counters etc.
71  goto_functions.update();
72 }
unsigned goto2graph_cfg(value_setst &value_sets, memory_modelt model, bool no_dependencies, loop_strategyt duplicate_body)
goes through CFG and build a static abstract event graph overapproximating the read/write relations f...
Definition: goto2graph.cpp:93
#define CPROVER_PREFIX
void introduce_temporaries(value_setst &value_sets, symbol_tablet &symbol_table, const irep_idt &function, goto_programt &goto_program, messaget &message)
all access to shared variables is pushed into assignments
Definition: weak_memory.cpp:38
mstreamt & status()
Definition: message.h:238
Definition: wmm.h:23
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
Fence insertion following criteria of Pensieve (PPoPP&#39;05)
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
void collect_pairs_naive(namespacet &ns)
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 collect_pairs(namespacet &ns)
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
Definition: remove_skip.cpp:71
#define Forall_goto_functions(it, functions)
void set_parameters_collection(unsigned _max_var=0, unsigned _max_po_trans=0, bool _ignore_arrays=false)
Definition: goto2graph.h:362
Definition: wmm.h:40
Program Transformation.
Race Detection for Threaded Goto Programs.