From 72694d159d5c2334b3dc83fb8566dd2c1a5a2681 Mon Sep 17 00:00:00 2001 From: Marius Melemciuc Date: Tue, 14 Mar 2017 16:42:06 +0000 Subject: [PATCH 1/2] Added usage of dynamic-objects with recency Replaced the creation of plain dynamic-objects with dynamic-objects flagged with recency at the malloc allocation site. --- src/pointer-analysis/value_set.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index c3e4dee0cf1..2519a100a19 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -808,11 +808,12 @@ void value_sett::get_value_set_rec( const typet &dynamic_type= static_cast(expr.find("#type")); - dynamic_object_exprt dynamic_object(dynamic_type); - dynamic_object.set_instance(location_number); - dynamic_object.valid()=true_exprt(); + // Create the most-recent-allocation dynamic-object + dynamic_object_exprt dynamic_object_recent(dynamic_type, true); + dynamic_object_recent.set_instance(location_number); + dynamic_object_recent.valid()=true_exprt(); - insert(dest, dynamic_object, 0); + insert(dest, dynamic_object_recent, 0); } else if(statement==ID_cpp_new || statement==ID_cpp_new_array) From 9b728a796dffbe842086a4207106106e36a9a571 Mon Sep 17 00:00:00 2001 From: Marius Melemciuc Date: Tue, 28 Mar 2017 13:18:12 +0100 Subject: [PATCH 2/2] Propagated changes of dynamic-objects' recency Applied the changes introduced by the recency property of dynamic-objects. Added function to get the dynamic-objects' name. Added separate function that returns the name of the dynamic-object sent as a read-only parameter. This function is added in a new file, pointer-analysis/dynamic_object_name.h. --- src/pointer-analysis/dynamic_object_name.h | 58 ++++++++++++++++++++++ src/pointer-analysis/value_set.cpp | 22 ++++---- src/pointer-analysis/value_set.h | 4 +- src/pointer-analysis/value_set_fi.cpp | 22 ++++---- src/pointer-analysis/value_set_fi.h | 6 ++- src/pointer-analysis/value_set_fivr.cpp | 22 ++++---- src/pointer-analysis/value_set_fivr.h | 7 ++- src/pointer-analysis/value_set_fivrns.cpp | 22 ++++---- src/pointer-analysis/value_set_fivrns.h | 7 ++- 9 files changed, 123 insertions(+), 47 deletions(-) create mode 100644 src/pointer-analysis/dynamic_object_name.h diff --git a/src/pointer-analysis/dynamic_object_name.h b/src/pointer-analysis/dynamic_object_name.h new file mode 100644 index 00000000000..aaeefaad5e8 --- /dev/null +++ b/src/pointer-analysis/dynamic_object_name.h @@ -0,0 +1,58 @@ +/*******************************************************************\ + +Module: Dynamic object name + +Author: Marius-Constantin Melemciuc + +Date: April 2017 + +@ Copyright Diffblue, Ltd. + +\*******************************************************************/ + +#ifndef CPROVER_POINTER_ANALYSIS_DYNAMIC_OBJECT_NAME_H +#define CPROVER_POINTER_ANALYSIS_DYNAMIC_OBJECT_NAME_H + +#include + +#include + +/*******************************************************************\ + +Function: get_dynamic_object_name + + Inputs: dynamic_object: The dynamic-object. + + Outputs: The name of the dynamic-object, composed of the + "value_set::dynamic_object", + it's instance, + and the keyword "most_recent_allocation" or + "any_allocation". + + Purpose: To generate a name for dynamic-objects suitable for use + in the LHS of value-set maps. + +\*******************************************************************/ + +inline std::string get_dynamic_object_name( + const dynamic_object_exprt &dynamic_object) +{ + std::string name= + "value_set::dynamic_object"+ + std::to_string(dynamic_object.get_instance()); + + if(dynamic_object.get_recency()== + dynamic_object_exprt::recencyt::MOST_RECENT_ALLOCATION) + { + name+=as_string(ID_most_recent_allocation); + } + else if(dynamic_object.get_recency()== + dynamic_object_exprt::recencyt::ANY_ALLOCATION) + { + name+=as_string(ID_any_allocation); + } + + return name; +} + +#endif // CPROVER_POINTER_ANALYSIS_DYNAMIC_OBJECT_NAME_H diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 2519a100a19..75c644f28c1 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -28,6 +28,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "value_set.h" #include "add_failed_symbols.h" +#include "dynamic_object_name.h" const value_sett::object_map_dt value_sett::object_map_dt::blank; object_numberingt value_sett::object_numbering; @@ -903,10 +904,7 @@ void value_sett::get_value_set_rec( { const dynamic_object_exprt &dynamic_object= to_dynamic_object_expr(expr); - - const std::string prefix= - "value_set::dynamic_object"+ - std::to_string(dynamic_object.get_instance()); + std::string prefix=get_dynamic_object_name(dynamic_object); // first try with suffix const std::string full_name=prefix+suffix; @@ -1467,9 +1465,12 @@ void value_sett::do_free( { const dynamic_object_exprt &dynamic_object= to_dynamic_object_expr(object); + dynamic_object_idt key_dynamic_object=std::make_pair( + dynamic_object.get_instance(), + dynamic_object.get_recency()); if(dynamic_object.valid().is_true()) - to_mark.insert(dynamic_object.get_instance()); + to_mark.insert(key_dynamic_object); } } @@ -1498,7 +1499,11 @@ void value_sett::do_free( const dynamic_object_exprt &dynamic_object= to_dynamic_object_expr(object); - if(to_mark.count(dynamic_object.get_instance())==0) + dynamic_object_idt key_dynamic_object=std::make_pair( + dynamic_object.get_instance(), + dynamic_object.get_recency()); + + if(to_mark.count(key_dynamic_object)==0) set(new_object_map, o_it); else { @@ -1565,10 +1570,7 @@ void value_sett::assign_rec( { const dynamic_object_exprt &dynamic_object= to_dynamic_object_expr(lhs); - - const std::string name= - "value_set::dynamic_object"+ - std::to_string(dynamic_object.get_instance()); + std::string name=get_dynamic_object_name(dynamic_object); entryt &e=get_entry(entryt(name, suffix), lhs.type(), ns); diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h index e863a969744..2f359e4130d 100644 --- a/src/pointer-analysis/value_set.h +++ b/src/pointer-analysis/value_set.h @@ -126,7 +126,9 @@ class value_sett typedef std::set expr_sett; - typedef std::set dynamic_object_id_sett; + typedef std::pair + dynamic_object_idt; + typedef std::set dynamic_object_id_sett; #ifdef USE_DSTRING typedef std::map valuest; diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index 0fbcd7dec00..976f68ab490 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "value_set_fi.h" +#include "dynamic_object_name.h" const value_set_fit::object_map_dt value_set_fit::object_map_dt::blank; object_numberingt value_set_fit::object_numbering; @@ -771,11 +772,7 @@ void value_set_fit::get_value_set_rec( { const dynamic_object_exprt &dynamic_object= to_dynamic_object_expr(expr); - - const std::string name= - "value_set::dynamic_object"+ - std::to_string(dynamic_object.get_instance())+ - suffix; + std::string name=get_dynamic_object_name(dynamic_object)+suffix; // look it up valuest::const_iterator v_it=values.find(name); @@ -1330,9 +1327,12 @@ void value_set_fit::do_free( { const dynamic_object_exprt &dynamic_object= to_dynamic_object_expr(object); + dynamic_object_idt key_dynamic_object=std::make_pair( + dynamic_object.get_instance(), + dynamic_object.get_recency()); if(dynamic_object.valid().is_true()) - to_mark.insert(dynamic_object.get_instance()); + to_mark.insert(key_dynamic_object); } } @@ -1357,8 +1357,11 @@ void value_set_fit::do_free( { const dynamic_object_exprt &dynamic_object= to_dynamic_object_expr(object); + dynamic_object_idt key_dynamic_object=std::make_pair( + dynamic_object.get_instance(), + dynamic_object.get_recency()); - if(to_mark.count(dynamic_object.get_instance())==0) + if(to_mark.count(key_dynamic_object)==0) set(new_object_map, o_it); else { @@ -1447,10 +1450,7 @@ void value_set_fit::assign_rec( { const dynamic_object_exprt &dynamic_object= to_dynamic_object_expr(lhs); - - const std::string name= - "value_set::dynamic_object"+ - std::to_string(dynamic_object.get_instance()); + std::string name=get_dynamic_object_name(dynamic_object); if(make_union(get_entry(name, suffix).object_map, values_rhs)) changed = true; diff --git a/src/pointer-analysis/value_set_fi.h b/src/pointer-analysis/value_set_fi.h index 13defa545ae..c268e6394c9 100644 --- a/src/pointer-analysis/value_set_fi.h +++ b/src/pointer-analysis/value_set_fi.h @@ -20,6 +20,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "object_numbering.h" +#include + class value_set_fit { public: @@ -155,7 +157,9 @@ class value_set_fit typedef std::unordered_set expr_sett; - typedef std::unordered_set dynamic_object_id_sett; + typedef std::pair + dynamic_object_idt; + typedef std::set dynamic_object_id_sett; #ifdef USE_DSTRING typedef std::map valuest; diff --git a/src/pointer-analysis/value_set_fivr.cpp b/src/pointer-analysis/value_set_fivr.cpp index e06d73b245b..7b65acd9f06 100644 --- a/src/pointer-analysis/value_set_fivr.cpp +++ b/src/pointer-analysis/value_set_fivr.cpp @@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com, #include #include "value_set_fivr.h" +#include "dynamic_object_name.h" const value_set_fivrt::object_map_dt value_set_fivrt::object_map_dt::blank; object_numberingt value_set_fivrt::object_numbering; @@ -897,11 +898,7 @@ void value_set_fivrt::get_value_set_rec( { const dynamic_object_exprt &dynamic_object= to_dynamic_object_expr(expr); - - const std::string name= - "value_set::dynamic_object"+ - std::to_string(dynamic_object.get_instance())+ - suffix; + std::string name=get_dynamic_object_name(dynamic_object)+suffix; // look it up valuest::const_iterator v_it=values.find(name); @@ -1454,9 +1451,12 @@ void value_set_fivrt::do_free( { const dynamic_object_exprt &dynamic_object= to_dynamic_object_expr(object); + dynamic_object_idt key_dynamic_object=std::make_pair( + dynamic_object.get_instance(), + dynamic_object.get_recency()); if(dynamic_object.valid().is_true()) - to_mark.insert(dynamic_object.get_instance()); + to_mark.insert(key_dynamic_object); } } @@ -1481,8 +1481,11 @@ void value_set_fivrt::do_free( { const dynamic_object_exprt &dynamic_object= to_dynamic_object_expr(object); + dynamic_object_idt key_dynamic_object=std::make_pair( + dynamic_object.get_instance(), + dynamic_object.get_recency()); - if(to_mark.count(dynamic_object.get_instance())==0) + if(to_mark.count(key_dynamic_object)==0) set(new_object_map, o_it); else { @@ -1585,10 +1588,7 @@ void value_set_fivrt::assign_rec( { const dynamic_object_exprt &dynamic_object= to_dynamic_object_expr(lhs); - - const std::string name= - "value_set::dynamic_object"+ - std::to_string(dynamic_object.get_instance()); + std::string name=get_dynamic_object_name(dynamic_object); entryt &temp_entry=get_temporary_entry(name, suffix); diff --git a/src/pointer-analysis/value_set_fivr.h b/src/pointer-analysis/value_set_fivr.h index e12563252ae..ea3f82ac603 100644 --- a/src/pointer-analysis/value_set_fivr.h +++ b/src/pointer-analysis/value_set_fivr.h @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -20,6 +21,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "object_numbering.h" +#include + class value_set_fivrt { public: @@ -216,7 +219,9 @@ class value_set_fivrt typedef std::unordered_set expr_sett; - typedef std::unordered_set dynamic_object_id_sett; + typedef std::pair + dynamic_object_idt; + typedef std::set dynamic_object_id_sett; #ifdef USE_DSTRING typedef std::map valuest; diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp index 4591bdd938d..a50e1a0edbc 100644 --- a/src/pointer-analysis/value_set_fivrns.cpp +++ b/src/pointer-analysis/value_set_fivrns.cpp @@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com, #include #include "value_set_fivrns.h" +#include "dynamic_object_name.h" const value_set_fivrnst::object_map_dt value_set_fivrnst::object_map_dt::blank; object_numberingt value_set_fivrnst::object_numbering; @@ -671,11 +672,7 @@ void value_set_fivrnst::get_value_set_rec( { const dynamic_object_exprt &dynamic_object= to_dynamic_object_expr(expr); - - const std::string name= - "value_set::dynamic_object"+ - std::to_string(dynamic_object.get_instance())+ - suffix; + std::string name=get_dynamic_object_name(dynamic_object)+suffix; // look it up valuest::const_iterator v_it=values.find(name); @@ -1113,9 +1110,12 @@ void value_set_fivrnst::do_free( { const dynamic_object_exprt &dynamic_object= to_dynamic_object_expr(object); + dynamic_object_idt key_dynamic_object=std::make_pair( + dynamic_object.get_instance(), + dynamic_object.get_recency()); if(dynamic_object.valid().is_true()) - to_mark.insert(dynamic_object.get_instance()); + to_mark.insert(key_dynamic_object); } } @@ -1140,8 +1140,11 @@ void value_set_fivrnst::do_free( { const dynamic_object_exprt &dynamic_object= to_dynamic_object_expr(object); + dynamic_object_idt key_dynamic_object=std::make_pair( + dynamic_object.get_instance(), + dynamic_object.get_recency()); - if(to_mark.count(dynamic_object.get_instance())==0) + if(to_mark.count(key_dynamic_object)==0) set(new_object_map, o_it); else { @@ -1220,10 +1223,7 @@ void value_set_fivrnst::assign_rec( { const dynamic_object_exprt &dynamic_object= to_dynamic_object_expr(lhs); - - const std::string name= - "value_set::dynamic_object"+ - std::to_string(dynamic_object.get_instance()); + std::string name=get_dynamic_object_name(dynamic_object); entryt &temp_entry = get_temporary_entry(name, suffix); diff --git a/src/pointer-analysis/value_set_fivrns.h b/src/pointer-analysis/value_set_fivrns.h index f3afc204ef2..89c987b85a6 100644 --- a/src/pointer-analysis/value_set_fivrns.h +++ b/src/pointer-analysis/value_set_fivrns.h @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -21,6 +22,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "object_numbering.h" +#include + class value_set_fivrnst { public: @@ -216,7 +219,9 @@ class value_set_fivrnst typedef std::unordered_set expr_sett; - typedef std::unordered_set dynamic_object_id_sett; + typedef std::pair + dynamic_object_idt; + typedef std::set dynamic_object_id_sett; #ifdef USE_DSTRING typedef std::map valuest;