Skip to content

Commit 55b3640

Browse files
peterschrammelpeterschrammel
authored
Merge pull request diffblue#756 from mariusmc92/feature/recency-analysis
Added usage of dynamic-objects with recency
2 parents 28dc578 + 9b728a7 commit 55b3640

9 files changed

+128
-51
lines changed

‎src/pointer-analysis/dynamic_object_name.h

Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,58 @@
1+
/*******************************************************************\
2+
3+
Module: Dynamic object name
4+
5+
Author: Marius-Constantin Melemciuc
6+
7+
Date: April 2017
8+
9+
@ Copyright Diffblue, Ltd.
10+
11+
\*******************************************************************/
12+
13+
#ifndef CPROVER_POINTER_ANALYSIS_DYNAMIC_OBJECT_NAME_H
14+
#define CPROVER_POINTER_ANALYSIS_DYNAMIC_OBJECT_NAME_H
15+
16+
#include <string>
17+
18+
#include <util/std_expr.h>
19+
20+
/*******************************************************************\
21+
22+
Function: get_dynamic_object_name
23+
24+
Inputs: dynamic_object: The dynamic-object.
25+
26+
Outputs: The name of the dynamic-object, composed of the
27+
"value_set::dynamic_object",
28+
it's instance,
29+
and the keyword "most_recent_allocation" or
30+
"any_allocation".
31+
32+
Purpose: To generate a name for dynamic-objects suitable for use
33+
in the LHS of value-set maps.
34+
35+
\*******************************************************************/
36+
37+
inline std::string get_dynamic_object_name(
38+
const dynamic_object_exprt &dynamic_object)
39+
{
40+
std::string name=
41+
"value_set::dynamic_object"+
42+
std::to_string(dynamic_object.get_instance());
43+
44+
if(dynamic_object.get_recency()==
45+
dynamic_object_exprt::recencyt::MOST_RECENT_ALLOCATION)
46+
{
47+
name+=as_string(ID_most_recent_allocation);
48+
}
49+
else if(dynamic_object.get_recency()==
50+
dynamic_object_exprt::recencyt::ANY_ALLOCATION)
51+
{
52+
name+=as_string(ID_any_allocation);
53+
}
54+
55+
return name;
56+
}
57+
58+
#endif // CPROVER_POINTER_ANALYSIS_DYNAMIC_OBJECT_NAME_H

‎src/pointer-analysis/value_set.cpp

Lines changed: 17 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,7 @@ Author: Daniel Kroening, [email protected]
2828

2929
#include "value_set.h"
3030
#include "add_failed_symbols.h"
31+
#include "dynamic_object_name.h"
3132

3233
const value_sett::object_map_dt value_sett::object_map_dt::blank;
3334
object_numberingt value_sett::object_numbering;
@@ -808,11 +809,12 @@ void value_sett::get_value_set_rec(
808809
const typet &dynamic_type=
809810
static_cast<const typet &>(expr.find("#type"));
810811

811-
dynamic_object_exprt dynamic_object(dynamic_type);
812-
dynamic_object.set_instance(location_number);
813-
dynamic_object.valid()=true_exprt();
812+
// Create the most-recent-allocation dynamic-object
813+
dynamic_object_exprt dynamic_object_recent(dynamic_type, true);
814+
dynamic_object_recent.set_instance(location_number);
815+
dynamic_object_recent.valid()=true_exprt();
814816

815-
insert(dest, dynamic_object, 0);
817+
insert(dest, dynamic_object_recent, 0);
816818
}
817819
else if(statement==ID_cpp_new ||
818820
statement==ID_cpp_new_array)
@@ -902,10 +904,7 @@ void value_sett::get_value_set_rec(
902904
{
903905
const dynamic_object_exprt &dynamic_object=
904906
to_dynamic_object_expr(expr);
905-
906-
const std::string prefix=
907-
"value_set::dynamic_object"+
908-
std::to_string(dynamic_object.get_instance());
907+
std::string prefix=get_dynamic_object_name(dynamic_object);
909908

910909
// first try with suffix
911910
const std::string full_name=prefix+suffix;
@@ -1466,9 +1465,12 @@ void value_sett::do_free(
14661465
{
14671466
const dynamic_object_exprt &dynamic_object=
14681467
to_dynamic_object_expr(object);
1468+
dynamic_object_idt key_dynamic_object=std::make_pair(
1469+
dynamic_object.get_instance(),
1470+
dynamic_object.get_recency());
14691471

14701472
if(dynamic_object.valid().is_true())
1471-
to_mark.insert(dynamic_object.get_instance());
1473+
to_mark.insert(key_dynamic_object);
14721474
}
14731475
}
14741476

@@ -1497,7 +1499,11 @@ void value_sett::do_free(
14971499
const dynamic_object_exprt &dynamic_object=
14981500
to_dynamic_object_expr(object);
14991501

1500-
if(to_mark.count(dynamic_object.get_instance())==0)
1502+
dynamic_object_idt key_dynamic_object=std::make_pair(
1503+
dynamic_object.get_instance(),
1504+
dynamic_object.get_recency());
1505+
1506+
if(to_mark.count(key_dynamic_object)==0)
15011507
set(new_object_map, o_it);
15021508
else
15031509
{
@@ -1564,10 +1570,7 @@ void value_sett::assign_rec(
15641570
{
15651571
const dynamic_object_exprt &dynamic_object=
15661572
to_dynamic_object_expr(lhs);
1567-
1568-
const std::string name=
1569-
"value_set::dynamic_object"+
1570-
std::to_string(dynamic_object.get_instance());
1573+
std::string name=get_dynamic_object_name(dynamic_object);
15711574

15721575
entryt &e=get_entry(entryt(name, suffix), lhs.type(), ns);
15731576

‎src/pointer-analysis/value_set.h

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -126,7 +126,9 @@ class value_sett
126126

127127
typedef std::set<exprt> expr_sett;
128128

129-
typedef std::set<unsigned int> dynamic_object_id_sett;
129+
typedef std::pair<unsigned int, dynamic_object_exprt::recencyt>
130+
dynamic_object_idt;
131+
typedef std::set<dynamic_object_idt> dynamic_object_id_sett;
130132

131133
#ifdef USE_DSTRING
132134
typedef std::map<idt, entryt> valuest;

‎src/pointer-analysis/value_set_fi.cpp

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
2121
#include <ansi-c/c_types.h>
2222

2323
#include "value_set_fi.h"
24+
#include "dynamic_object_name.h"
2425

2526
const value_set_fit::object_map_dt value_set_fit::object_map_dt::blank;
2627
object_numberingt value_set_fit::object_numbering;
@@ -771,11 +772,7 @@ void value_set_fit::get_value_set_rec(
771772
{
772773
const dynamic_object_exprt &dynamic_object=
773774
to_dynamic_object_expr(expr);
774-
775-
const std::string name=
776-
"value_set::dynamic_object"+
777-
std::to_string(dynamic_object.get_instance())+
778-
suffix;
775+
std::string name=get_dynamic_object_name(dynamic_object)+suffix;
779776

780777
// look it up
781778
valuest::const_iterator v_it=values.find(name);
@@ -1330,9 +1327,12 @@ void value_set_fit::do_free(
13301327
{
13311328
const dynamic_object_exprt &dynamic_object=
13321329
to_dynamic_object_expr(object);
1330+
dynamic_object_idt key_dynamic_object=std::make_pair(
1331+
dynamic_object.get_instance(),
1332+
dynamic_object.get_recency());
13331333

13341334
if(dynamic_object.valid().is_true())
1335-
to_mark.insert(dynamic_object.get_instance());
1335+
to_mark.insert(key_dynamic_object);
13361336
}
13371337
}
13381338

@@ -1357,8 +1357,11 @@ void value_set_fit::do_free(
13571357
{
13581358
const dynamic_object_exprt &dynamic_object=
13591359
to_dynamic_object_expr(object);
1360+
dynamic_object_idt key_dynamic_object=std::make_pair(
1361+
dynamic_object.get_instance(),
1362+
dynamic_object.get_recency());
13601363

1361-
if(to_mark.count(dynamic_object.get_instance())==0)
1364+
if(to_mark.count(key_dynamic_object)==0)
13621365
set(new_object_map, o_it);
13631366
else
13641367
{
@@ -1447,10 +1450,7 @@ void value_set_fit::assign_rec(
14471450
{
14481451
const dynamic_object_exprt &dynamic_object=
14491452
to_dynamic_object_expr(lhs);
1450-
1451-
const std::string name=
1452-
"value_set::dynamic_object"+
1453-
std::to_string(dynamic_object.get_instance());
1453+
std::string name=get_dynamic_object_name(dynamic_object);
14541454

14551455
if(make_union(get_entry(name, suffix).object_map, values_rhs))
14561456
changed = true;

‎src/pointer-analysis/value_set_fi.h

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,8 @@ Author: Daniel Kroening, [email protected]
2020

2121
#include "object_numbering.h"
2222

23+
#include <util/std_expr.h>
24+
2325
class value_set_fit
2426
{
2527
public:
@@ -155,7 +157,9 @@ class value_set_fit
155157

156158
typedef std::unordered_set<exprt, irep_hash> expr_sett;
157159

158-
typedef std::unordered_set<unsigned int> dynamic_object_id_sett;
160+
typedef std::pair<unsigned int, dynamic_object_exprt::recencyt>
161+
dynamic_object_idt;
162+
typedef std::set<dynamic_object_idt> dynamic_object_id_sett;
159163

160164
#ifdef USE_DSTRING
161165
typedef std::map<idt, entryt> valuest;

‎src/pointer-analysis/value_set_fivr.cpp

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected],
2222
#include <ansi-c/c_types.h>
2323

2424
#include "value_set_fivr.h"
25+
#include "dynamic_object_name.h"
2526

2627
const value_set_fivrt::object_map_dt value_set_fivrt::object_map_dt::blank;
2728
object_numberingt value_set_fivrt::object_numbering;
@@ -897,11 +898,7 @@ void value_set_fivrt::get_value_set_rec(
897898
{
898899
const dynamic_object_exprt &dynamic_object=
899900
to_dynamic_object_expr(expr);
900-
901-
const std::string name=
902-
"value_set::dynamic_object"+
903-
std::to_string(dynamic_object.get_instance())+
904-
suffix;
901+
std::string name=get_dynamic_object_name(dynamic_object)+suffix;
905902

906903
// look it up
907904
valuest::const_iterator v_it=values.find(name);
@@ -1454,9 +1451,12 @@ void value_set_fivrt::do_free(
14541451
{
14551452
const dynamic_object_exprt &dynamic_object=
14561453
to_dynamic_object_expr(object);
1454+
dynamic_object_idt key_dynamic_object=std::make_pair(
1455+
dynamic_object.get_instance(),
1456+
dynamic_object.get_recency());
14571457

14581458
if(dynamic_object.valid().is_true())
1459-
to_mark.insert(dynamic_object.get_instance());
1459+
to_mark.insert(key_dynamic_object);
14601460
}
14611461
}
14621462

@@ -1481,8 +1481,11 @@ void value_set_fivrt::do_free(
14811481
{
14821482
const dynamic_object_exprt &dynamic_object=
14831483
to_dynamic_object_expr(object);
1484+
dynamic_object_idt key_dynamic_object=std::make_pair(
1485+
dynamic_object.get_instance(),
1486+
dynamic_object.get_recency());
14841487

1485-
if(to_mark.count(dynamic_object.get_instance())==0)
1488+
if(to_mark.count(key_dynamic_object)==0)
14861489
set(new_object_map, o_it);
14871490
else
14881491
{
@@ -1585,10 +1588,7 @@ void value_set_fivrt::assign_rec(
15851588
{
15861589
const dynamic_object_exprt &dynamic_object=
15871590
to_dynamic_object_expr(lhs);
1588-
1589-
const std::string name=
1590-
"value_set::dynamic_object"+
1591-
std::to_string(dynamic_object.get_instance());
1591+
std::string name=get_dynamic_object_name(dynamic_object);
15921592

15931593
entryt &temp_entry=get_temporary_entry(name, suffix);
15941594

‎src/pointer-analysis/value_set_fivr.h

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,13 +13,16 @@ Author: Daniel Kroening, [email protected]
1313
#include <list>
1414
#include <map>
1515
#include <unordered_set>
16+
#include <set>
1617

1718
#include <util/mp_arith.h>
1819
#include <util/namespace.h>
1920
#include <util/reference_counting.h>
2021

2122
#include "object_numbering.h"
2223

24+
#include <util/std_expr.h>
25+
2326
class value_set_fivrt
2427
{
2528
public:
@@ -216,7 +219,9 @@ class value_set_fivrt
216219

217220
typedef std::unordered_set<exprt, irep_hash> expr_sett;
218221

219-
typedef std::unordered_set<unsigned int> dynamic_object_id_sett;
222+
typedef std::pair<unsigned int, dynamic_object_exprt::recencyt>
223+
dynamic_object_idt;
224+
typedef std::set<dynamic_object_idt> dynamic_object_id_sett;
220225

221226
#ifdef USE_DSTRING
222227
typedef std::map<idt, entryt> valuest;

‎src/pointer-analysis/value_set_fivrns.cpp

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected],
2222
#include <ansi-c/c_types.h>
2323

2424
#include "value_set_fivrns.h"
25+
#include "dynamic_object_name.h"
2526

2627
const value_set_fivrnst::object_map_dt value_set_fivrnst::object_map_dt::blank;
2728
object_numberingt value_set_fivrnst::object_numbering;
@@ -671,11 +672,7 @@ void value_set_fivrnst::get_value_set_rec(
671672
{
672673
const dynamic_object_exprt &dynamic_object=
673674
to_dynamic_object_expr(expr);
674-
675-
const std::string name=
676-
"value_set::dynamic_object"+
677-
std::to_string(dynamic_object.get_instance())+
678-
suffix;
675+
std::string name=get_dynamic_object_name(dynamic_object)+suffix;
679676

680677
// look it up
681678
valuest::const_iterator v_it=values.find(name);
@@ -1113,9 +1110,12 @@ void value_set_fivrnst::do_free(
11131110
{
11141111
const dynamic_object_exprt &dynamic_object=
11151112
to_dynamic_object_expr(object);
1113+
dynamic_object_idt key_dynamic_object=std::make_pair(
1114+
dynamic_object.get_instance(),
1115+
dynamic_object.get_recency());
11161116

11171117
if(dynamic_object.valid().is_true())
1118-
to_mark.insert(dynamic_object.get_instance());
1118+
to_mark.insert(key_dynamic_object);
11191119
}
11201120
}
11211121

@@ -1140,8 +1140,11 @@ void value_set_fivrnst::do_free(
11401140
{
11411141
const dynamic_object_exprt &dynamic_object=
11421142
to_dynamic_object_expr(object);
1143+
dynamic_object_idt key_dynamic_object=std::make_pair(
1144+
dynamic_object.get_instance(),
1145+
dynamic_object.get_recency());
11431146

1144-
if(to_mark.count(dynamic_object.get_instance())==0)
1147+
if(to_mark.count(key_dynamic_object)==0)
11451148
set(new_object_map, o_it);
11461149
else
11471150
{
@@ -1220,10 +1223,7 @@ void value_set_fivrnst::assign_rec(
12201223
{
12211224
const dynamic_object_exprt &dynamic_object=
12221225
to_dynamic_object_expr(lhs);
1223-
1224-
const std::string name=
1225-
"value_set::dynamic_object"+
1226-
std::to_string(dynamic_object.get_instance());
1226+
std::string name=get_dynamic_object_name(dynamic_object);
12271227

12281228
entryt &temp_entry = get_temporary_entry(name, suffix);
12291229

0 commit comments

Comments
 (0)