1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3
4 Module Name:
5
6 trail.h
7
8 Abstract:
9
10 <abstract>
11
12 Author:
13
14 Leonardo de Moura (leonardo) 2008-06-02.
15
16 Revision History:
17
18 --*/
19 #pragma once
20
21 #include "util/obj_hashtable.h"
22 #include "util/region.h"
23 #include "util/obj_ref.h"
24 #include "util/vector.h"
25
26 template<typename Ctx>
27 class trail {
28 public:
~trail()29 virtual ~trail() {
30 }
31 virtual void undo(Ctx & ctx) = 0;
32 };
33
34 template<typename Ctx, typename T>
35 class value_trail : public trail<Ctx> {
36 T & m_value;
37 T m_old_value;
38
39 public:
value_trail(T & value)40 value_trail(T & value):
41 m_value(value),
42 m_old_value(value) {
43 }
44
value_trail(T & value,T const & new_value)45 value_trail(T & value, T const& new_value):
46 m_value(value),
47 m_old_value(value) {
48 m_value = new_value;
49 }
50
~value_trail()51 ~value_trail() override {
52 }
53
undo(Ctx & ctx)54 void undo(Ctx & ctx) override {
55 m_value = m_old_value;
56 }
57 };
58
59
60
61 template<typename Ctx, typename T, typename Ts>
62 class scoped_value_trail : public trail<Ctx> {
63 T & m_value;
64 Ts & m_values;
65
66 public:
scoped_value_trail(T & value,Ts & values)67 scoped_value_trail(T & value, Ts& values):
68 m_value(value),
69 m_values(values) {
70 }
71
~scoped_value_trail()72 ~scoped_value_trail() override {
73 }
74
undo(Ctx & ctx)75 void undo(Ctx & ctx) override {
76 m_value = m_values.back();
77 m_values.pop_back();
78 }
79 };
80
81
82 template<typename Ctx>
83 class reset_flag_trail : public trail<Ctx> {
84 bool & m_value;
85 public:
reset_flag_trail(bool & value)86 reset_flag_trail(bool & value):
87 m_value(value) {
88 }
89
~reset_flag_trail()90 ~reset_flag_trail() override {
91 }
92
undo(Ctx & ctx)93 void undo(Ctx & ctx) override {
94 m_value = false;
95 }
96 };
97
98 template<typename Ctx, typename T>
99 class set_ptr_trail : public trail<Ctx> {
100 T * & m_ptr;
101 public:
set_ptr_trail(T * & ptr)102 set_ptr_trail(T * & ptr):
103 m_ptr(ptr) {
104 SASSERT(m_ptr == 0);
105 }
106
undo(Ctx & ctx)107 void undo(Ctx & ctx) override {
108 m_ptr = nullptr;
109 }
110 };
111
112 template<typename Ctx, typename T, bool CallDestructors=true>
113 class restore_size_trail : public trail<Ctx> {
114 vector<T, CallDestructors> & m_vector;
115 unsigned m_old_size;
116 public:
restore_size_trail(vector<T,CallDestructors> & v,unsigned sz)117 restore_size_trail(vector<T, CallDestructors> & v, unsigned sz):
118 m_vector(v),
119 m_old_size(sz) {
120 }
restore_size_trail(vector<T,CallDestructors> & v)121 restore_size_trail(vector<T, CallDestructors> & v):
122 m_vector(v),
123 m_old_size(v.size()) {
124 }
~restore_size_trail()125 ~restore_size_trail() override {
126 }
undo(Ctx & ctx)127 void undo(Ctx & ctx) override {
128 m_vector.shrink(m_old_size);
129 }
130 };
131
132 template<typename Ctx, typename T, bool CallDestructors=true>
133 class vector_value_trail : public trail<Ctx> {
134 vector<T, CallDestructors> & m_vector;
135 unsigned m_idx;
136 T m_old_value;
137 public:
vector_value_trail(vector<T,CallDestructors> & v,unsigned idx)138 vector_value_trail(vector<T, CallDestructors> & v, unsigned idx):
139 m_vector(v),
140 m_idx(idx),
141 m_old_value(v[idx]) {
142 }
143
~vector_value_trail()144 ~vector_value_trail() override {
145 }
146
undo(Ctx & ctx)147 void undo(Ctx & ctx) override {
148 m_vector[m_idx] = m_old_value;
149 }
150 };
151
152 template<typename Ctx, typename V, typename T>
153 class vector2_value_trail : public trail<Ctx> {
154 V & m_vector;
155 unsigned m_i;
156 unsigned m_j;
157 T m_old_value;
158 public:
vector2_value_trail(V & v,unsigned i,unsigned j)159 vector2_value_trail(V& v, unsigned i, unsigned j):
160 m_vector(v),
161 m_i(i),
162 m_j(j),
163 m_old_value(v[i][j]) {
164 }
165
~vector2_value_trail()166 ~vector2_value_trail() override {
167 }
168
undo(Ctx & ctx)169 void undo(Ctx & ctx) override {
170 m_vector[m_i][m_j] = m_old_value;
171 }
172 };
173
174
175 template<typename Ctx, typename D, typename R>
176 class insert_obj_map : public trail<Ctx> {
177 obj_map<D,R>& m_map;
178 D* m_obj;
179 public:
insert_obj_map(obj_map<D,R> & t,D * o)180 insert_obj_map(obj_map<D,R>& t, D* o) : m_map(t), m_obj(o) {}
~insert_obj_map()181 ~insert_obj_map() override {}
undo(Ctx & ctx)182 void undo(Ctx & ctx) override { m_map.remove(m_obj); }
183 };
184
185 template<typename Ctx, typename D, typename R>
186 class remove_obj_map : public trail<Ctx> {
187 obj_map<D,R>& m_map;
188 D* m_obj;
189 R m_value;
190 public:
remove_obj_map(obj_map<D,R> & t,D * o,R v)191 remove_obj_map(obj_map<D,R>& t, D* o, R v) : m_map(t), m_obj(o), m_value(v) {}
~remove_obj_map()192 ~remove_obj_map() override {}
undo(Ctx & ctx)193 void undo(Ctx & ctx) override { m_map.insert(m_obj, m_value); }
194 };
195
196 template<typename Ctx, typename M, typename D>
197 class insert_map : public trail<Ctx> {
198 M& m_map;
199 D m_obj;
200 public:
insert_map(M & t,D o)201 insert_map(M& t, D o) : m_map(t), m_obj(o) {}
~insert_map()202 ~insert_map() override {}
undo(Ctx & ctx)203 void undo(Ctx & ctx) override { m_map.remove(m_obj); }
204 };
205
206
207 template<typename Ctx, typename M, typename Mgr, typename D>
208 class insert_ref_map : public trail<Ctx> {
209 Mgr& m;
210 M& m_map;
211 D m_obj;
212 public:
insert_ref_map(Mgr & m,M & t,D o)213 insert_ref_map(Mgr& m, M& t, D o) : m(m), m_map(t), m_obj(o) {}
~insert_ref_map()214 virtual ~insert_ref_map() {}
undo(Ctx & ctx)215 virtual void undo(Ctx & ctx) { m_map.remove(m_obj); m.dec_ref(m_obj); }
216 };
217
218 template<typename Ctx, typename Mgr, typename D, typename R>
219 class insert_ref2_map : public trail<Ctx> {
220 Mgr& m;
221 obj_map<D,R*>& m_map;
222 D* m_obj;
223 R* m_val;
224 public:
insert_ref2_map(Mgr & m,obj_map<D,R * > & t,D * o,R * r)225 insert_ref2_map(Mgr& m, obj_map<D,R*>& t, D*o, R*r) : m(m), m_map(t), m_obj(o), m_val(r) {}
~insert_ref2_map()226 virtual ~insert_ref2_map() {}
undo(Ctx & ctx)227 virtual void undo(Ctx & ctx) { m_map.remove(m_obj); m.dec_ref(m_obj); m.dec_ref(m_val); }
228 };
229
230
231 template<typename Ctx, typename V>
232 class push_back_vector : public trail<Ctx> {
233 V & m_vector;
234 public:
push_back_vector(V & v)235 push_back_vector(V & v):
236 m_vector(v) {
237 }
238
undo(Ctx & ctx)239 void undo(Ctx & ctx) override {
240 m_vector.pop_back();
241 }
242 };
243
244 template<typename Ctx, typename T>
245 class set_vector_idx_trail : public trail<Ctx> {
246 ptr_vector<T> & m_vector;
247 unsigned m_idx;
248 public:
set_vector_idx_trail(ptr_vector<T> & v,unsigned idx)249 set_vector_idx_trail(ptr_vector<T> & v, unsigned idx):
250 m_vector(v),
251 m_idx(idx) {
252 }
253
~set_vector_idx_trail()254 ~set_vector_idx_trail() override {
255 }
256
undo(Ctx & ctx)257 void undo(Ctx & ctx) override {
258 m_vector[m_idx] = 0;
259 }
260 };
261
262 template<typename Ctx, typename T, bool CallDestructors=true>
263 class pop_back_trail : public trail<Ctx> {
264 vector<T, CallDestructors> & m_vector;
265 T m_value;
266 public:
pop_back_trail(vector<T,CallDestructors> & v)267 pop_back_trail(vector<T, CallDestructors> & v):
268 m_vector(v),
269 m_value(m_vector.back()) {
270 }
271
undo(Ctx & ctx)272 virtual void undo(Ctx & ctx) {
273 m_vector.push_back(m_value);
274 }
275 };
276
277 template<typename Ctx, typename T, bool CallDestructors=true>
278 class pop_back2_trail : public trail<Ctx> {
279 vector<T, CallDestructors> & m_vector;
280 typedef vector<vector<T, CallDestructors>, true> vector_t;
281 unsigned m_index;
282 T m_value;
283 public:
pop_back2_trail(vector<T,CallDestructors> & v,unsigned index)284 pop_back2_trail(vector<T, CallDestructors> & v, unsigned index):
285 m_vector(v),
286 m_index(index),
287 m_value(m_vector[index].back()) {
288 }
289
undo(Ctx & ctx)290 virtual void undo(Ctx & ctx) {
291 m_vector[m_index].push_back(m_value);
292 }
293 };
294
295
296
297 template<typename Ctx, typename T, bool CallDestructors=true>
298 class push_back_trail : public trail<Ctx> {
299 vector<T, CallDestructors> & m_vector;
300 public:
push_back_trail(vector<T,CallDestructors> & v)301 push_back_trail(vector<T, CallDestructors> & v):
302 m_vector(v) {
303 }
304
undo(Ctx & ctx)305 void undo(Ctx & ctx) override {
306 m_vector.pop_back();
307 }
308 };
309
310 template<typename Ctx, typename T, bool CallDestructors=true>
311 class push_back2_trail : public trail<Ctx> {
312 typedef vector<vector<T, CallDestructors>, true> vector_t;
313 vector_t & m_vector;
314 unsigned m_index;
315 public:
push_back2_trail(vector_t & v,unsigned index)316 push_back2_trail(vector_t & v, unsigned index) :
317 m_vector(v),
318 m_index(index) {
319 }
320
undo(Ctx & ctx)321 virtual void undo(Ctx & ctx) {
322 m_vector[m_index].pop_back();
323 }
324 };
325
326 template<typename Ctx>
327 class set_bitvector_trail : public trail<Ctx> {
328 bool_vector & m_vector;
329 unsigned m_idx;
330 public:
set_bitvector_trail(bool_vector & v,unsigned idx)331 set_bitvector_trail(bool_vector & v, unsigned idx):
332 m_vector(v),
333 m_idx(idx) {
334 SASSERT(m_vector[m_idx] == false);
335 m_vector[m_idx] = true;
336 }
337
undo(Ctx & ctx)338 void undo(Ctx & ctx) override {
339 m_vector[m_idx] = false;
340 }
341 };
342
343
344 template<typename Ctx, typename T, bool CallDestructors = true>
345 class history_trail : public trail<Ctx> {
346 vector<T, CallDestructors>& m_dst;
347 unsigned m_idx;
348 vector<T, CallDestructors>& m_hist;
349 public:
history_trail(vector<T,CallDestructors> & v,unsigned idx,vector<T,CallDestructors> & hist)350 history_trail(vector<T, CallDestructors>& v, unsigned idx, vector<T, CallDestructors>& hist) :
351 m_dst(v),
352 m_idx(idx),
353 m_hist(hist) {}
354
~history_trail()355 ~history_trail() override {
356 }
357
undo(Ctx & ctx)358 void undo(Ctx& ctx) override {
359 m_dst[m_idx] = m_hist.back();
360 m_hist.pop_back();
361 }
362 };
363
364
365 template<typename Ctx, typename T>
366 class new_obj_trail : public trail<Ctx> {
367 T * m_obj;
368 public:
new_obj_trail(T * obj)369 new_obj_trail(T * obj):
370 m_obj(obj) {
371 }
372
undo(Ctx & ctx)373 void undo(Ctx & ctx) override {
374 dealloc(m_obj);
375 }
376 };
377
378 template<typename Ctx, typename M, typename T>
379 class obj_ref_trail : public trail<Ctx> {
380 obj_ref<T,M> m_obj;
381 public:
obj_ref_trail(obj_ref<T,M> & obj)382 obj_ref_trail(obj_ref<T,M>& obj):
383 m_obj(obj) {
384 }
385
undo(Ctx & ctx)386 virtual void undo(Ctx & ctx) {
387 m_obj.reset();
388 }
389 };
390
391 template<typename Ctx, typename T>
392 class insert_obj_trail : public trail<Ctx> {
393 obj_hashtable<T>& m_table;
394 T* m_obj;
395 public:
insert_obj_trail(obj_hashtable<T> & t,T * o)396 insert_obj_trail(obj_hashtable<T>& t, T* o) : m_table(t), m_obj(o) {}
~insert_obj_trail()397 ~insert_obj_trail() override {}
undo(Ctx & ctx)398 void undo(Ctx & ctx) override { m_table.remove(m_obj); }
399 };
400
401
402 template<typename Ctx, typename T>
403 class remove_obj_trail : public trail<Ctx> {
404 obj_hashtable<T>& m_table;
405 T* m_obj;
406 public:
remove_obj_trail(obj_hashtable<T> & t,T * o)407 remove_obj_trail(obj_hashtable<T>& t, T* o) : m_table(t), m_obj(o) {}
~remove_obj_trail()408 virtual ~remove_obj_trail() {}
undo(Ctx & ctx)409 virtual void undo(Ctx & ctx) { m_table.insert(m_obj); }
410 };
411
412
413 template<typename Ctx>
undo_trail_stack(Ctx & ctx,ptr_vector<trail<Ctx>> & s,unsigned old_size)414 void undo_trail_stack(Ctx & ctx, ptr_vector<trail<Ctx> > & s, unsigned old_size) {
415 SASSERT(old_size <= s.size());
416 typename ptr_vector<trail<Ctx> >::iterator begin = s.begin() + old_size;
417 typename ptr_vector<trail<Ctx> >::iterator it = s.end();
418 while (it != begin) {
419 --it;
420 (*it)->undo(ctx);
421 }
422 s.shrink(old_size);
423 }
424
425 template<typename Ctx>
426 class trail_stack {
427 Ctx & m_ctx;
428 ptr_vector<trail<Ctx> > m_trail_stack;
429 unsigned_vector m_scopes;
430 region m_region;
431 public:
trail_stack(Ctx & c)432 trail_stack(Ctx & c):m_ctx(c) {}
433
~trail_stack()434 ~trail_stack() {}
435
get_region()436 region & get_region() { return m_region; }
437
reset()438 void reset() {
439 pop_scope(m_scopes.size());
440 // Undo trail objects stored at lvl 0 (avoid memory leaks if lvl 0 contains new_obj_trail objects).
441 undo_trail_stack(m_ctx, m_trail_stack, 0);
442 }
443
push_ptr(trail<Ctx> * t)444 void push_ptr(trail<Ctx> * t) { m_trail_stack.push_back(t); }
445
446 template<typename TrailObject>
push(TrailObject const & obj)447 void push(TrailObject const & obj) { m_trail_stack.push_back(new (m_region) TrailObject(obj)); }
448
get_num_scopes()449 unsigned get_num_scopes() const { return m_scopes.size(); }
450
push_scope()451 void push_scope() { m_region.push_scope(); m_scopes.push_back(m_trail_stack.size()); }
452
pop_scope(unsigned num_scopes)453 void pop_scope(unsigned num_scopes) {
454 if (num_scopes == 0) return;
455 unsigned lvl = m_scopes.size();
456 SASSERT(num_scopes <= lvl);
457 unsigned new_lvl = lvl - num_scopes;
458 unsigned old_size = m_scopes[new_lvl];
459 undo_trail_stack(m_ctx, m_trail_stack, old_size);
460 m_scopes.shrink(new_lvl);
461 m_region.pop_scope(num_scopes);
462 }
463 };
464
465