cprover
fence_inserter.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: ILP construction for all cycles and resolution
4 
5 Author: Vincent Nimal
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_MUSKETEER_FENCE_INSERTER_H
13 #define CPROVER_MUSKETEER_FENCE_INSERTER_H
14 
17 
18 // Note: no forward declaration for instrumentert as we derive fence_insertert
20 
21 #include <set>
22 #include <map>
23 
24 #include "graph_visitor.h"
25 #include "cycles_visitor.h"
26 
27 class abstract_eventt;
28 class ilpt;
29 
30 // TODO: can be indirectly replaced by a list without redundancy
31 // (not a set though)
32 struct mip_vart
33 {
35 
36  unsigned unique;
37 
38  std::map<unsigned, edget> map_to_e;
39  std::map<edget, unsigned> map_from_e;
40 
41  unsigned add_edge(const edget &e)
42  {
43  if(map_from_e.find(e) != map_from_e.end())
44  return map_from_e[e];
45  else
46  {
47  ++unique;
48  map_to_e.insert(std::pair<unsigned, edget>(unique, e));
49  map_from_e[e] = unique;
50  return unique;
51  }
52  }
53 
55  {
56  }
57 };
58 
59 /* in essence: cycles + goto-prog -> ilp */
61 {
62 public:
64 
66 
68  std::map<unsigned, edget> &map_to_e;
69  std::map<edget, unsigned> &map_from_e;
70  unsigned add_edge(const edget &e) { return var.add_edge(e); }
71  unsigned add_invisible_edge(const edget &e)
72  {
73  return invisible_var.add_edge(e);
74  }
75 
77  std::size_t constraints_number;
79 
82 
83 protected:
84  unsigned &unique;
85  unsigned fence_options;
86 
87  /* MIP variables to edges in po^+/\C */
89 
90  /* MIP invisible variables (com) */
92 
93  /* MIP matrix construction */
94  void mip_set_var(ilpt &ilp, unsigned &i);
95  void mip_set_cst(ilpt &ilp, unsigned &i);
96  void mip_fill_matrix(
97  ilpt &ilp,
98  unsigned &i,
99  unsigned const_constraints_number,
100  unsigned const_unique);
101 
102  /* preprocessing (necessary as glpk static) and solving */
103  void preprocess();
104  void solve();
105 
106  enum fence_typet { Fence=0, Dp=1, Lwfence=2, Branching=3, Ctlfence=4 };
107  virtual unsigned fence_cost(fence_typet e) const;
108 
109  std::string to_string(fence_typet f) const;
110 
111  /* for the preprocessing */
112  std::set<event_idt> po;
113  std::list<std::set<event_idt> > powr_constraints;
114  std::list<std::set<event_idt> > poww_constraints;
115  std::list<std::set<event_idt> > porw_constraints;
116  std::list<std::set<event_idt> > porr_constraints;
117  std::list<std::set<event_idt> > com_constraints;
118 
119  /* to retrieve the edges involved in the cycles */
121 
122  /* conversion column <-> (MIP variable, fence type) */
123  unsigned col_to_var(unsigned u) const;
124  fence_typet col_to_fence(unsigned u) const;
125  unsigned var_fence_to_col(fence_typet f, unsigned var) const;
126 
127  /* for the frequencies sum */
128  const float epsilon;
129  const bool with_freq;
130  std::map<unsigned, float> freq_table;
131 
132  void import_freq();
133 
134  /* computes the fence options */
135  void compute_fence_options();
136 
137  /* debug */
138  void print_vars() const;
139 
140  /* storing final results */
141  std::map<edget, fence_typet> fenced_edges;
142 
143 public:
144  explicit fence_insertert(instrumentert &instr):
148  epsilon(0.001), with_freq(false)
149  {
150  }
151 
154  constraints_number(0), model(_model), const_graph_visitor(*this),
156  epsilon(0.001), with_freq(false)
157  {
158  }
159 
160  /* do it */
161  void compute();
162 
163  /* selection methods */
164  // Note: process_selection updates the selection of cycles in instrumenter,
165  // whereas filter just ignores some
166  virtual void process_cycles_selection() { }
167  virtual bool filter_cycles(unsigned cycle_id) const { return false; }
168 
169  /* prints final results */
170  void print_to_file();
171  void print_to_file_2();
172  void print_to_file_3();
173  void print_to_file_4();
174 
175  /* TODO: to be replaced eventually by ns.lookup and basename */
176  static std::string remove_extra(const irep_idt &id)
177  {
178  const std::string copy=id2string(id);
179  return remove_extra(copy);
180  }
181 
182  static std::string remove_extra(std::string copy)
183  {
184  if(copy.find("::")==std::string::npos)
185  return copy;
186  return copy.substr(copy.find_last_of("::")+1);
187  }
188 
189  typet get_type(const irep_idt &id);
191  std::list<std::string>::const_iterator it,
192  std::list<std::string>::const_iterator end,
193  const typet &type);
194 };
195 
196 #endif // CPROVER_MUSKETEER_FENCE_INSERTER_H
std::map< unsigned, edget > & map_to_e
normal variables used almost every time
The type of an expression.
Definition: type.h:20
std::map< edget, unsigned > & map_from_e
fence_insertert(instrumentert &instr)
Definition: ilp.h:78
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
const_graph_visitort const_graph_visitor
to retrieve the concrete graph edges involved in the (abstract) cycles
memory models
std::string to_string(fence_typet f) const
void print_vars() const
unsigned col_to_var(unsigned u) const
const bool with_freq
virtual void process_cycles_selection()
std::list< std::set< event_idt > > powr_constraints
graph of abstract events
typet get_type(const irep_idt &id)
event_grapht::critical_cyclet::delayt edget
unsigned fence_options
typet type_component(std::list< std::string >::const_iterator it, std::list< std::string >::const_iterator end, const typet &type)
fence_insertert(instrumentert &instr, memory_modelt _model)
std::map< edget, fence_typet > fenced_edges
memory_modelt
Definition: wmm.h:17
unsigned add_invisible_edge(const edget &e)
Instrumenter.
std::map< edget, unsigned > map_from_e
const memory_modelt model
unsigned add_edge(const edget &e)
static std::string remove_extra(std::string copy)
fence_typet col_to_fence(unsigned u) const
virtual unsigned fence_cost(fence_typet e) const
event_grapht::critical_cyclet::delayt edget
const float epsilon
virtual bool filter_cycles(unsigned cycle_id) const
std::set< event_idt > po
std::list< std::set< event_idt > > porr_constraints
unsigned & unique
unsigned var_fence_to_col(fence_typet f, unsigned var) const
cycles visitor for computing edges involved for fencing
void mip_fill_matrix(ilpt &ilp, unsigned &i, unsigned const_constraints_number, unsigned const_unique)
graph visitor for computing edges involved for fencing
std::list< std::set< event_idt > > com_constraints
instrumentert & instrumenter
mip_vart invisible_var
Definition: wmm.h:20
static std::string remove_extra(const irep_idt &id)
void mip_set_var(ilpt &ilp, unsigned &i)
cycles_visitort cycles_visitor
unsigned unique
std::list< std::set< event_idt > > porw_constraints
void mip_set_cst(ilpt &ilp, unsigned &i)
std::map< unsigned, edget > map_to_e
std::map< unsigned, float > freq_table
unsigned add_edge(const edget &e)
std::size_t constraints_number
number of constraints
std::list< std::set< event_idt > > poww_constraints