12 #ifndef CPROVER_MUSKETEER_FENCE_INSERTER_H 13 #define CPROVER_MUSKETEER_FENCE_INSERTER_H 43 if(map_from_e.find(e) != map_from_e.end())
48 map_to_e.insert(std::pair<unsigned, edget>(unique, e));
70 unsigned add_edge(
const edget &e) {
return var.add_edge(e); }
73 return invisible_var.add_edge(e);
94 void mip_set_var(
ilpt &ilp,
unsigned &i);
95 void mip_set_cst(
ilpt &ilp,
unsigned &i);
99 unsigned const_constraints_number,
100 unsigned const_unique);
106 enum fence_typet { Fence=0, Dp=1, Lwfence=2, Branching=3, Ctlfence=4 };
112 std::set<event_idt>
po;
123 unsigned col_to_var(
unsigned u)
const;
125 unsigned var_fence_to_col(
fence_typet f,
unsigned var)
const;
135 void compute_fence_options();
138 void print_vars()
const;
145 instrumenter(instr), map_to_e(var.map_to_e), map_from_e(var.map_from_e),
146 constraints_number(0), model(
TSO), const_graph_visitor(*this),
147 unique(var.unique), fence_options(0), cycles_visitor(*this),
148 epsilon(0.001), with_freq(false)
153 instrumenter(instr), map_to_e(var.map_to_e), map_from_e(var.map_from_e),
154 constraints_number(0), model(_model), const_graph_visitor(*this),
155 unique(var.unique), fence_options(0), cycles_visitor(*this),
156 epsilon(0.001), with_freq(false)
170 void print_to_file();
171 void print_to_file_2();
172 void print_to_file_3();
173 void print_to_file_4();
179 return remove_extra(copy);
184 if(copy.find(
"::")==std::string::npos)
186 return copy.substr(copy.find_last_of(
"::")+1);
190 typet type_component(
191 std::list<std::string>::const_iterator it,
192 std::list<std::string>::const_iterator end,
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.
std::map< edget, unsigned > & map_from_e
fence_insertert(instrumentert &instr)
const std::string & id2string(const irep_idt &d)
const_graph_visitort const_graph_visitor
to retrieve the concrete graph edges involved in the (abstract) cycles
virtual void process_cycles_selection()
std::list< std::set< event_idt > > powr_constraints
event_grapht::critical_cyclet::delayt edget
fence_insertert(instrumentert &instr, memory_modelt _model)
std::map< edget, fence_typet > fenced_edges
unsigned add_invisible_edge(const edget &e)
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)
event_grapht::critical_cyclet::delayt edget
virtual bool filter_cycles(unsigned cycle_id) const
std::list< std::set< event_idt > > porr_constraints
cycles visitor for computing edges involved for fencing
graph visitor for computing edges involved for fencing
std::list< std::set< event_idt > > com_constraints
instrumentert & instrumenter
static std::string remove_extra(const irep_idt &id)
cycles_visitort cycles_visitor
std::list< std::set< event_idt > > porw_constraints
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