14
14
15
15
#include < pointer-analysis/dynamic_object_name.h>
16
16
17
+ #include < boost/range/algorithm.hpp>
18
+
17
19
void local_value_sett::make_union_adjusting_evs_types (
18
20
object_mapt &dest,
19
21
const object_mapt &src,
@@ -226,6 +228,104 @@ void local_value_sett::get_value_set_rec(
226
228
baset::get_value_set_rec (expr, dest, suffix, original_type, ns);
227
229
}
228
230
231
+ /* ******************************************************************\
232
+
233
+ Function: local_value_sett::apply_side_effects
234
+
235
+ Inputs: rhs: Right-hand-side of an assignment code
236
+ expression.
237
+ ns: Namespace.
238
+
239
+ Outputs:
240
+
241
+ Purpose: Applying side effects needed in Recency Analysis.
242
+
243
+ \*******************************************************************/
244
+
245
+ void local_value_sett::apply_side_effects (
246
+ const exprt &rhs,
247
+ const namespacet &ns)
248
+ {
249
+ if (rhs.id ()==ID_side_effect &&
250
+ rhs.get (ID_statement)==ID_malloc)
251
+ {
252
+ const typet &dynamic_type=
253
+ static_cast <const typet &>(rhs.find (" #type" ));
254
+
255
+ // Replace all the current most-recent-allocation dynamic-objects
256
+ // with the corresponding any-allocation ones
257
+ for (auto &value : values)
258
+ {
259
+ entryt &entry=value.second ;
260
+ object_map_dt &object_map=entry.object_map .write ();
261
+
262
+ // Look-up for the first appearance of the current
263
+ // most-recent dynamic-object in the current object-map
264
+ object_map_dt::iterator it=boost::range::find_if (
265
+ object_map,
266
+ [this ] (object_map_dt::reference object)
267
+ {
268
+ exprt &o=object_numbering[object.first ];
269
+ if (o.id ()!=ID_dynamic_object)
270
+ return false ;
271
+
272
+ dynamic_object_exprt &dynamic_object=to_dynamic_object_expr (o);
273
+
274
+ return dynamic_object.get_instance ()==location_number &&
275
+ dynamic_object.get_recency ()==
276
+ dynamic_object_exprt::recencyt::MOST_RECENT_ALLOCATION;
277
+ });
278
+
279
+ if (it==object_map.end ())
280
+ continue ;
281
+
282
+ // Delete the most-recent dynamic-object from the current object_map
283
+ object_map.erase (it);
284
+
285
+ int index_dynamic_object_recent=it->first ;
286
+
287
+ // Create the any-allocation dynamic-object
288
+ // by copying the existing most-recent one and adjusting the recency flag
289
+ dynamic_object_exprt dynamic_object_any_allocation=
290
+ to_dynamic_object_expr (object_numbering[index_dynamic_object_recent]);
291
+ dynamic_object_any_allocation.set_recency (false );
292
+
293
+ // Add the newly created any-allocation dynamic-object
294
+ // in the current rhs' object_map
295
+ insert (entry.object_map , dynamic_object_any_allocation, 0 );
296
+ }
297
+
298
+ const std::string name_most_recent=
299
+ prefix_dynamic_object+
300
+ std::to_string (location_number)+
301
+ id2string (ID_most_recent_allocation);
302
+ const std::string name_any_allocation=
303
+ prefix_dynamic_object+
304
+ std::to_string (location_number)+
305
+ id2string (ID_any_allocation);
306
+
307
+ // Iterates over the domain's entries and when we find the current
308
+ // most-recent-allocation dynamic-object, add its object-map
309
+ // to its correspondent any-allocation dynamic-object's object-map
310
+ for (auto &value : values)
311
+ {
312
+ entryt &entry=value.second ;
313
+
314
+ if (entry.identifier ==name_most_recent)
315
+ {
316
+ entryt &entry_any_allocation=get_entry (
317
+ entryt (name_any_allocation, entry.suffix ),
318
+ dynamic_type,
319
+ ns);
320
+
321
+ // Add into the any-allocation dynamic-object's object_map
322
+ // the most-recent-allocation dynamic-object's object_map
323
+ make_union (entry_any_allocation.object_map , entry.object_map );
324
+ }
325
+ }
326
+ }
327
+ }
328
+
229
329
void local_value_sett::assign (
230
330
const exprt &lhs,
231
331
const exprt &rhs,
@@ -288,6 +388,7 @@ void local_value_sett::assign(
288
388
}
289
389
}
290
390
#endif
391
+ apply_side_effects (rhs, ns);
291
392
292
393
assign_rec (lhs, values_rhs, " " , ns, add_to_sets);
293
394
}
@@ -334,9 +435,7 @@ void local_value_sett::assign_rec(
334
435
const dynamic_object_exprt &dynamic_object=
335
436
to_dynamic_object_expr (lhs);
336
437
337
- const std::string name=
338
- prefix_dynamic_object+
339
- std::to_string (dynamic_object.get_instance ());
438
+ std::string name=get_dynamic_object_name (dynamic_object);
340
439
341
440
typet declared_on_type;
342
441
std::string suffix_without_subtype_ignored;
@@ -346,12 +445,27 @@ void local_value_sett::assign_rec(
346
445
ns,
347
446
declared_on_type,
348
447
suffix_without_subtype_ignored);
349
- entryt &e=get_entry (
448
+
449
+ entryt &entry=get_entry (
350
450
entryt (name, suffix, declared_on_type),
351
451
lhs.type (),
352
452
ns);
353
453
354
- make_union (e.object_map , values_rhs);
454
+ if (dynamic_object.get_recency ()==
455
+ dynamic_object_exprt::recencyt::MOST_RECENT_ALLOCATION &&
456
+ !add_to_sets)
457
+ {
458
+ // We have to assign the values from the current rhs to the
459
+ // current most-recent dynamic-object's object-map
460
+
461
+ // Strong-update of the dynamic-object
462
+ entry.object_map =values_rhs;
463
+ }
464
+ else
465
+ {
466
+ // Weak-update of the dynamic-object
467
+ make_union (entry.object_map , values_rhs);
468
+ }
355
469
return ;
356
470
}
357
471
else if (lhs.id ()==ID_external_value_set)
0 commit comments