From a2c16852b9bea9aafa40288b12784d2e6547e7c6 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 8 Mar 2017 11:29:14 +0000 Subject: [PATCH 1/4] Templatize and virtualize value-set analysis This templates value-set-analysis, so that it can be subclassed providing a value-set extension, and virtualizes value-set so it can similarly be extended. --- src/goto-symex/postcondition.cpp | 2 +- src/goto-symex/symex_dereference_state.cpp | 2 +- src/pointer-analysis/Makefile | 1 - src/pointer-analysis/show_value_sets.h | 2 +- src/pointer-analysis/value_set.cpp | 21 +++-- src/pointer-analysis/value_set.h | 98 ++++++++++++++++---- src/pointer-analysis/value_set_analysis.cpp | 65 ------------- src/pointer-analysis/value_set_analysis.h | 74 ++++++++++++--- src/pointer-analysis/value_set_domain.cpp | 56 ----------- src/pointer-analysis/value_set_domain.h | 57 ++++++++++-- unit/CustomVSATest.class | Bin 0 -> 890 bytes unit/CustomVSATest.java | 51 ++++++++++ 12 files changed, 261 insertions(+), 168 deletions(-) delete mode 100644 src/pointer-analysis/value_set_domain.cpp create mode 100644 unit/CustomVSATest.class create mode 100644 unit/CustomVSATest.java diff --git a/src/goto-symex/postcondition.cpp b/src/goto-symex/postcondition.cpp index 4383439b72d..519d66bfc71 100644 --- a/src/goto-symex/postcondition.cpp +++ b/src/goto-symex/postcondition.cpp @@ -174,7 +174,7 @@ bool postconditiont::is_used( // aliasing may happen here value_setst::valuest expr_set; - value_set.get_value_set(expr.op0(), expr_set, ns); + value_set.read_value_set(expr.op0(), expr_set, ns); std::unordered_set symbols; for(value_setst::valuest::const_iterator diff --git a/src/goto-symex/symex_dereference_state.cpp b/src/goto-symex/symex_dereference_state.cpp index 9911ba51e7d..8aa2ec288d6 100644 --- a/src/goto-symex/symex_dereference_state.cpp +++ b/src/goto-symex/symex_dereference_state.cpp @@ -81,7 +81,7 @@ void symex_dereference_statet::get_value_set( const exprt &expr, value_setst::valuest &value_set) { - state.value_set.get_value_set(expr, value_set, goto_symex.ns); + state.value_set.read_value_set(expr, value_set, goto_symex.ns); #if 0 std::cout << "**************************\n"; diff --git a/src/pointer-analysis/Makefile b/src/pointer-analysis/Makefile index 7e9837ac737..6af38c803c3 100644 --- a/src/pointer-analysis/Makefile +++ b/src/pointer-analysis/Makefile @@ -11,7 +11,6 @@ SRC = add_failed_symbols.cpp \ value_set_analysis_fivr.cpp \ value_set_analysis_fivrns.cpp \ value_set_dereference.cpp \ - value_set_domain.cpp \ value_set_domain_fi.cpp \ value_set_domain_fivr.cpp \ value_set_domain_fivrns.cpp \ diff --git a/src/pointer-analysis/show_value_sets.h b/src/pointer-analysis/show_value_sets.h index 3b080f66e62..b704f6a2964 100644 --- a/src/pointer-analysis/show_value_sets.h +++ b/src/pointer-analysis/show_value_sets.h @@ -12,10 +12,10 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_POINTER_ANALYSIS_SHOW_VALUE_SETS_H #define CPROVER_POINTER_ANALYSIS_SHOW_VALUE_SETS_H +#include #include class goto_modelt; -class value_set_analysist; void show_value_sets( ui_message_handlert::uit, diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 40dd0cd520b..5b0e50a30a8 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -311,7 +311,7 @@ bool value_sett::eval_pointer_offset( return mod; } -void value_sett::get_value_set( +void value_sett::read_value_set( const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const @@ -340,7 +340,7 @@ void value_sett::get_value_set( { exprt tmp(expr); if(!is_simplified) - simplify(tmp, ns); + simplifier(tmp, ns); get_value_set_rec(tmp, dest, "", tmp.type(), ns); } @@ -809,7 +809,7 @@ void value_sett::get_value_set_rec( exprt op1=expr.op1(); if(eval_pointer_offset(op1, ns)) - simplify(op1, ns); + simplifier(op1, ns); mp_integer op1_offset; const typet &op0_type=ns.follow(expr.op0().type()); @@ -908,7 +908,7 @@ void value_sett::dereference_rec( dest=src; } -void value_sett::get_reference_set( +void value_sett::read_reference_set( const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const @@ -1205,6 +1205,12 @@ void value_sett::assign( object_mapt values_rhs; get_value_set(rhs, values_rhs, ns, is_simplified); + // Permit custom subclass to alter the read values prior to write: + adjust_assign_rhs_values(rhs, ns, values_rhs); + + // Permit custom subclass to perform global side-effects prior to write: + apply_assign_side_effects(lhs, rhs, ns); + assign_rec(lhs, values_rhs, "", ns, add_to_sets); } } @@ -1482,7 +1488,7 @@ void value_sett::do_end_function( assign(lhs, rhs, ns, false, false); } -void value_sett::apply_code( +void value_sett::apply_code_rec( const codet &code, const namespacet &ns) { @@ -1491,7 +1497,7 @@ void value_sett::apply_code( if(statement==ID_block) { forall_operands(it, code) - apply_code(to_code(*it), ns); + apply_code_rec(to_code(*it), ns); } else if(statement==ID_function_call) { @@ -1694,3 +1700,6 @@ exprt value_sett::make_member( return member_expr; } + +value_sett::expr_simplifiert value_sett::default_simplifier= + [](exprt &e, const namespacet &ns) { simplify(e, ns); }; diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h index 68c41f4ce16..194209680bb 100644 --- a/src/pointer-analysis/value_set.h +++ b/src/pointer-analysis/value_set.h @@ -24,8 +24,20 @@ class namespacet; class value_sett { + typedef std::function expr_simplifiert; + + static expr_simplifiert default_simplifier; + public: - value_sett():location_number(0) + value_sett(): + location_number(0), + simplifier(default_simplifier) + { + } + + explicit value_sett(expr_simplifiert simplifier): + location_number(0), + simplifier(std::move(simplifier)) { } @@ -166,7 +178,7 @@ class value_sett typedef std::unordered_map valuest; #endif - void get_value_set( + void read_value_set( const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const; @@ -213,7 +225,10 @@ class value_sett void apply_code( const codet &code, - const namespacet &ns); + const namespacet &ns) + { + apply_code_rec(code, ns); + } void assign( const exprt &lhs, @@ -232,7 +247,7 @@ class value_sett const exprt &lhs, const namespacet &ns); - void get_reference_set( + void read_reference_set( const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const; @@ -242,13 +257,6 @@ class value_sett const namespacet &ns) const; protected: - void get_value_set_rec( - const exprt &expr, - object_mapt &dest, - const std::string &suffix, - const typet &original_type, - const namespacet &ns) const; - void get_value_set( const exprt &expr, object_mapt &dest, @@ -272,13 +280,6 @@ class value_sett const exprt &src, exprt &dest) const; - void assign_rec( - const exprt &lhs, - const object_mapt &values_rhs, - const std::string &suffix, - const namespacet &ns, - bool add_to_sets); - void do_free( const exprt &op, const namespacet &ns); @@ -287,6 +288,67 @@ class value_sett const exprt &src, const irep_idt &component_name, const namespacet &ns); + + // Expression simplification: + +private: + /// Expression simplification function; by default, plain old + /// util/simplify_expr, but can be customised by subclass. + expr_simplifiert simplifier; + +protected: + /// Run registered expression simplifier + void run_simplifier(exprt &e, const namespacet &ns) + { + simplifier(e, ns); + } + + // Subclass customisation points: + +protected: + /// Subclass customisation point for recursion over RHS expression: + virtual void get_value_set_rec( + const exprt &expr, + object_mapt &dest, + const std::string &suffix, + const typet &original_type, + const namespacet &ns) const; + + /// Subclass customisation point for recursion over LHS expression: + virtual void assign_rec( + const exprt &lhs, + const object_mapt &values_rhs, + const std::string &suffix, + const namespacet &ns, + bool add_to_sets); + + /// Subclass customisation point for applying code to this domain: + virtual void apply_code_rec( + const codet &code, + const namespacet &ns); + + private: + /// Subclass customisation point to filter or otherwise alter the value-set + /// returned from get_value_set before it is passed into assign. For example, + /// this is used in one subclass to tag and thus differentiate values that + /// originated in a particular place, vs. those that have been copied. + virtual void adjust_assign_rhs_values( + const exprt &rhs, + const namespacet &ns, + object_mapt &rhs_values) const + { + } + + /// Subclass customisation point to apply global side-effects to this domain, + /// after RHS values are read but before they are written. For example, this + /// is used in a recency-analysis plugin to demote existing most-recent + /// objects to general case ones. + virtual void apply_assign_side_effects( + const exprt &lhs, + const exprt &rhs, + const namespacet &ns) + { + } }; #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_H diff --git a/src/pointer-analysis/value_set_analysis.cpp b/src/pointer-analysis/value_set_analysis.cpp index d4a3388142e..dc03dfc0b04 100644 --- a/src/pointer-analysis/value_set_analysis.cpp +++ b/src/pointer-analysis/value_set_analysis.cpp @@ -13,74 +13,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include -#include #include -void value_set_analysist::initialize( - const goto_programt &goto_program) -{ - baset::initialize(goto_program); -} - -void value_set_analysist::initialize( - const goto_functionst &goto_functions) -{ - baset::initialize(goto_functions); -} - -void value_set_analysist::convert( - const goto_programt &goto_program, - const irep_idt &identifier, - xmlt &dest) const -{ - source_locationt previous_location; - - forall_goto_program_instructions(i_it, goto_program) - { - const source_locationt &location=i_it->source_location; - - if(location==previous_location) - continue; - - if(location.is_nil() || location.get_file().empty()) - continue; - - // find value set - const value_sett &value_set=(*this)[i_it].value_set; - - xmlt &i=dest.new_element("instruction"); - i.new_element()=::xml(location); - - for(value_sett::valuest::const_iterator - v_it=value_set.values.begin(); - v_it!=value_set.values.end(); - v_it++) - { - xmlt &var=i.new_element("variable"); - var.new_element("identifier").data= - id2string(v_it->first); - - #if 0 - const value_sett::expr_sett &expr_set= - v_it->second.expr_set(); - - for(value_sett::expr_sett::const_iterator - e_it=expr_set.begin(); - e_it!=expr_set.end(); - e_it++) - { - std::string value_str= - from_expr(ns, identifier, *e_it); - - var.new_element("value").data= - xmlt::escape(value_str); - } - #endif - } - } -} void convert( const goto_functionst &goto_functions, const value_set_analysist &value_set_analysis, diff --git a/src/pointer-analysis/value_set_analysis.h b/src/pointer-analysis/value_set_analysis.h index b41355abd73..d13f8903778 100644 --- a/src/pointer-analysis/value_set_analysis.h +++ b/src/pointer-analysis/value_set_analysis.h @@ -14,32 +14,80 @@ Author: Daniel Kroening, kroening@kroening.com #define USE_DEPRECATED_STATIC_ANALYSIS_H #include +#include +#include #include "value_set_domain.h" #include "value_sets.h" +#include "value_set.h" class xmlt; -class value_set_analysist: +template +class value_set_analysis_baset: public value_setst, - public static_analysist + public static_analysist > { public: - explicit value_set_analysist(const namespacet &_ns): - static_analysist(_ns) + typedef value_set_domaint domaint; + typedef static_analysist baset; + typedef typename baset::locationt locationt; + + explicit value_set_analysis_baset(const namespacet &ns):baset(ns) { } - typedef static_analysist baset; - - // overloading - virtual void initialize(const goto_programt &goto_program); - virtual void initialize(const goto_functionst &goto_functions); - void convert( const goto_programt &goto_program, const irep_idt &identifier, - xmlt &dest) const; + xmlt &dest) const + { + source_locationt previous_location; + + forall_goto_program_instructions(i_it, goto_program) + { + const source_locationt &location=i_it->source_location; + + if(location==previous_location) + continue; + + if(location.is_nil() || location.get_file().empty()) + continue; + + // find value set + const value_sett &value_set=(*this)[i_it].value_set; + + xmlt &i=dest.new_element("instruction"); + i.new_element()=::xml(location); + + for(value_sett::valuest::const_iterator + v_it=value_set.values.begin(); + v_it!=value_set.values.end(); + v_it++) + { + xmlt &var=i.new_element("variable"); + var.new_element("identifier").data= + id2string(v_it->first); + +#if 0 + const value_sett::expr_sett &expr_set= + v_it->second.expr_set(); + + for(value_sett::expr_sett::const_iterator + e_it=expr_set.begin(); + e_it!=expr_set.end(); + e_it++) + { + std::string value_str= + from_expr(ns, identifier, *e_it); + + var.new_element("value").data= + xmlt::escape(value_str); + } +#endif + } + } + } public: // interface value_sets @@ -48,10 +96,12 @@ class value_set_analysist: const exprt &expr, value_setst::valuest &dest) { - (*this)[l].value_set.get_value_set(expr, dest, ns); + (*this)[l].value_set.read_value_set(expr, dest, baset::ns); } }; +typedef value_set_analysis_baset value_set_analysist; + void convert( const goto_functionst &goto_functions, const value_set_analysist &value_set_analysis, diff --git a/src/pointer-analysis/value_set_domain.cpp b/src/pointer-analysis/value_set_domain.cpp deleted file mode 100644 index 4b296b541df..00000000000 --- a/src/pointer-analysis/value_set_domain.cpp +++ /dev/null @@ -1,56 +0,0 @@ -/*******************************************************************\ - -Module: Value Set - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Value Set - -#include "value_set_domain.h" - -#include - -void value_set_domaint::transform( - const namespacet &ns, - locationt from_l, - locationt to_l) -{ - switch(from_l->type) - { - case GOTO: - // ignore for now - break; - - case END_FUNCTION: - value_set.do_end_function(static_analysis_baset::get_return_lhs(to_l), ns); - break; - - case RETURN: - case OTHER: - case ASSIGN: - case DECL: - value_set.apply_code(from_l->code, ns); - break; - - case ASSUME: - value_set.guard(from_l->guard, ns); - break; - - case FUNCTION_CALL: - { - const code_function_callt &code= - to_code_function_call(from_l->code); - - value_set.do_function_call(to_l->function, code.arguments(), ns); - } - break; - - default: - { - // do nothing - } - } -} diff --git a/src/pointer-analysis/value_set_domain.h b/src/pointer-analysis/value_set_domain.h index e59250a0bc0..4b0e0a876cf 100644 --- a/src/pointer-analysis/value_set_domain.h +++ b/src/pointer-analysis/value_set_domain.h @@ -17,10 +17,11 @@ Author: Daniel Kroening, kroening@kroening.com #include "value_set.h" +template class value_set_domaint:public domain_baset { public: - value_sett value_set; + VST value_set; // overloading @@ -44,17 +45,59 @@ class value_set_domaint:public domain_baset value_set.location_number=l->location_number; } - virtual void transform( - const namespacet &ns, - locationt from_l, - locationt to_l); - virtual void get_reference_set( const namespacet &ns, const exprt &expr, value_setst::valuest &dest) { - value_set.get_reference_set(expr, dest, ns); + value_set.read_reference_set(expr, dest, ns); + } + + virtual void transform( + const namespacet &ns, + locationt from_l, + locationt to_l) + { + switch(from_l->type) + { + case GOTO: + // ignore for now + break; + + case END_FUNCTION: + { + value_set.do_end_function( + static_analysis_baset::get_return_lhs(to_l), ns); + break; + } + + // Note intentional fall-through here: + case RETURN: + case OTHER: + case ASSIGN: + case DECL: + case DEAD: + value_set.apply_code(from_l->code, ns); + break; + + case ASSUME: + value_set.guard(from_l->guard, ns); + break; + + case FUNCTION_CALL: + { + const code_function_callt &code= + to_code_function_call(from_l->code); + + value_set.do_function_call(to_l->function, code.arguments(), ns); + } + break; + + default: + { + // do nothing + } + } } }; diff --git a/unit/CustomVSATest.class b/unit/CustomVSATest.class new file mode 100644 index 0000000000000000000000000000000000000000..7a6b4ef057af4d530b711b5ce25a203599cf0700 GIT binary patch literal 890 zcmZ8gTW``}7=AuzX~EVp=3(p7BG>Tc8d&=BbW<{A* zft)W#GHiy@*%v6(4xN!x@f^Qf*=ZfhcJxfZ@`JGFc+HM0J#yxU{*fPy{b^2NM_{hD zIUGbmud(}bPY#r*Fk^MSpha;^%RF~|H+mtEEJy zw&OLN&{cT?YSDo^peSMkjy;ynQPWdA0mJQbM#~_8GE;EOHhs z*cL9R=pt+s`6*KTXc~liW+c>O?8&6h#ypV4dm&FdPqacW==HUq5Z@T2P@v7kUtf7yG_=qw-@i<@bIKIINhFjfHiGiWSy0+5z| Date: Fri, 22 Sep 2017 14:19:27 +0100 Subject: [PATCH 2/4] Value-set analysis: ignore DEAD statements We could be smarter with these; this at least enables us to process current standard GOTO programs. --- src/pointer-analysis/value_set.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 5b0e50a30a8..406cac0f99c 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -1615,6 +1615,10 @@ void value_sett::apply_code_rec( { // doesn't do anything } + else if(statement==ID_dead) + { + // ignore (could potentially prune value set in future) + } else { // std::cerr << code.pretty() << '\n'; From e669c12b3305ff4b166d644da867a07854a7d205 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 14 Sep 2017 14:06:50 +0100 Subject: [PATCH 3/4] Add unit tests for value-set-analysis customisation --- unit/CustomVSATest.class | Bin 890 -> 0 bytes unit/Makefile | 1 + unit/pointer-analysis/CustomVSATest.jar | Bin 0 -> 969 bytes .../{ => pointer-analysis}/CustomVSATest.java | 27 +- .../custom_value_set_analysis.cpp | 336 ++++++++++++++++++ 5 files changed, 348 insertions(+), 16 deletions(-) delete mode 100644 unit/CustomVSATest.class create mode 100644 unit/pointer-analysis/CustomVSATest.jar rename unit/{ => pointer-analysis}/CustomVSATest.java (54%) create mode 100644 unit/pointer-analysis/custom_value_set_analysis.cpp diff --git a/unit/CustomVSATest.class b/unit/CustomVSATest.class deleted file mode 100644 index 7a6b4ef057af4d530b711b5ce25a203599cf0700..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 890 zcmZ8gTW``}7=AuzX~EVp=3(p7BG>Tc8d&=BbW<{A* zft)W#GHiy@*%v6(4xN!x@f^Qf*=ZfhcJxfZ@`JGFc+HM0J#yxU{*fPy{b^2NM_{hD zIUGbmud(}bPY#r*Fk^MSpha;^%RF~|H+mtEEJy zw&OLN&{cT?YSDo^peSMkjy;ynQPWdA0mJQbM#~_8GE;EOHhs z*cL9R=pt+s`6*KTXc~liW+c>O?8&6h#ypV4dm&FdPqacW==HUq5Z@T2P@v7kUtf7yG_=qw-@i<@bIKIINhFjfHiGiWSy0+5z|*(j{<{BKL=j-;__snS@Z(Y5MyxzK6=gyqp9At3C_`%a6JuhD!Pv48Bt5`TA zUPvC1mXg-W_#v*U_I!z!#dC4dC*rEp7_Mf2D*9N&2zEsvmzIwU&<tSJbkU z!hEHB=6_%k-=%xUw@kdl-uvQ=8%N|H=zp4Am=>9>Fxxgg?cJH1#^v>Ye|{7`zQI7t3U28x-qHocxBL*Maue5-t8@v___Gn!OPB~n>@9Z zmgO$jaLKow)2FgFo76q%Z(djR?kJnszQX?e zV@IXVaX*=!-#JBWR_vVS*NYBpI5i(I`Y&z#~( zW*JR70&xr0_~~@Ky;a_E{^Q4^F4G=+x4hfKI6bf@_1gKi`pKN_KVFC&W1m&O^~l+l z`1yxawtXv~bjbXMb$p`v8kPJTufOs5O*%W_SJM@qmz!;bpWpodPil+G3*XB@m8(Qv z-aH^0QXu-hkeNU5ka5mK)@>j8Qunxv3Yqd0nBU8sUbFn;M71AYT@~KNd!Dn!J(6-| z)3iNUYGvrT+OJDbCrIb9nrqpelW}JMnLz3GcY7k&M@9w)GiFeVVPq0vKuz|rG!07j zr~sahL74zuD{?{vC3*y~1v24Uk+J}?37`av>@ZM*MS#OVCYIzI;LXYgQp5~|`+)RU Gu+stJC{fP< literal 0 HcmV?d00001 diff --git a/unit/CustomVSATest.java b/unit/pointer-analysis/CustomVSATest.java similarity index 54% rename from unit/CustomVSATest.java rename to unit/pointer-analysis/CustomVSATest.java index 154cf8d0f7c..7df3c6910a6 100644 --- a/unit/CustomVSATest.java +++ b/unit/pointer-analysis/CustomVSATest.java @@ -2,10 +2,12 @@ public class CustomVSATest { public Object never_read; - public Object normal_field; - public CustomVSATest unknown_field_ref; - public static CustomVSATest unknown_global_ref; + public static Object cause; + public static Object effect; + public static Object first_effect_read; + public static Object second_effect_read; + public static Object maybe_unknown_read; public static void test() { @@ -30,21 +32,14 @@ public static void test() { // This should acquire a "*" unknown-object, even though // it is obvious what it points to: Object maybe_unknown = new Object(); + maybe_unknown_read=maybe_unknown; - // Both of these fields, despite being initialised, should be - // considered to point to some unknown target, and so the reads - // through them return some unknown entity: + effect = new Object(); + first_effect_read = effect; - CustomVSATest outer = new CustomVSATest(); - outer.unknown_field_ref = new CustomVSATest(); - outer.unknown_field_ref.normal_field = new Object(); - - Object get_unknown_field = outer.unknown_field_ref.normal_field; - - unknown_global_ref = new CustomVSATest(); - unknown_global_ref.normal_field = new Object(); - - Object get_unknown_global = unknown_global_ref.normal_field; + // Under our custom VSA, this write should cause effect to become null: + cause = new Object(); + second_effect_read = effect; } diff --git a/unit/pointer-analysis/custom_value_set_analysis.cpp b/unit/pointer-analysis/custom_value_set_analysis.cpp new file mode 100644 index 00000000000..eb43cd51af3 --- /dev/null +++ b/unit/pointer-analysis/custom_value_set_analysis.cpp @@ -0,0 +1,336 @@ +/*******************************************************************\ + +Module: Value-set analysis tests + +Author: Chris Smowton, chris@smowton.net + +\*******************************************************************/ + +#include + +#include +#include +#include +#include +#include +#include +#include + +/// Counts calls to our custom simplifier, registered below: +int simplifies=0; + +/// An example customised value_sett. It makes a series of small changes +/// to the underlying value_sett logic, which can then be verified by the +/// test below: +/// * Writes to variables with 'ignored' in their name are ignored. +/// * Never propagate values via the field "never_read" +/// * Adds an ID_unknown to the value of variable "maybe_unknown" as it is read +/// * When a variable named `cause` is written, one named `effect` is zeroed. +class test_value_sett:public value_sett +{ +public: + test_value_sett(): + value_sett([this](exprt &e, const namespacet &ns) { simplifies++; }) + { + } + + static bool assigns_to_ignored_variable(const code_assignt &assign) + { + if(assign.lhs().id()!=ID_symbol) + return false; + const irep_idt &id=to_symbol_expr(assign.lhs()).get_identifier(); + return id2string(id).find("ignored")!=std::string::npos; + } + + void apply_code_rec(const codet &code, const namespacet &ns) override + { + // Ignore assignments to the local "ignored" + if(code.get_statement()==ID_assign && + assigns_to_ignored_variable(to_code_assign(code))) + { + return; + } + else + { + value_sett::apply_code_rec(code, ns); + } + } + + void assign_rec( + const exprt &lhs, + const object_mapt &values_rhs, + const std::string &suffix, + const namespacet &ns, + bool add_to_sets) override + { + // Disregard writes against variables containing 'no_write': + if(lhs.id()==ID_symbol) + { + const irep_idt &id=to_symbol_expr(lhs).get_identifier(); + if(id2string(id).find("no_write")!=std::string::npos) + return; + } + + value_sett::assign_rec(lhs, values_rhs, suffix, ns, add_to_sets); + } + + void get_value_set_rec( + const exprt &expr, + object_mapt &dest, + const std::string &suffix, + const typet &original_type, + const namespacet &ns) const override + { + // Ignore reads from fields named "never_read" + if(expr.id()==ID_member && + to_member_expr(expr).get_component_name()=="never_read") + { + return; + } + else + { + value_sett::get_value_set_rec( + expr, dest, suffix, original_type, ns); + } + } + + void adjust_assign_rhs_values( + const exprt &expr, + const namespacet &ns, + object_mapt &dest) const override + { + // Always add an ID_unknown to reads from variables containing + // "maybe_unknown": + exprt read_sym=expr; + while(read_sym.id()==ID_typecast) + read_sym=read_sym.op0(); + if(read_sym.id()==ID_symbol) + { + const irep_idt &id=to_symbol_expr(read_sym).get_identifier(); + if(id2string(id).find("maybe_unknown")!=std::string::npos) + insert(dest, exprt(ID_unknown, read_sym.type())); + } + } + + void apply_assign_side_effects( + const exprt &lhs, + const exprt &rhs, + const namespacet &ns) override + { + // Whenever someone touches the variable "cause", null the + // variable "effect": + if(lhs.id()==ID_symbol) + { + const irep_idt &id=to_symbol_expr(lhs).get_identifier(); + const auto &id_str=id2string(id); + auto find_idx=id_str.find("cause"); + if(find_idx!=std::string::npos) + { + std::string effect_id=id_str; + effect_id.replace(find_idx, 5, "effect"); + assign( + symbol_exprt(effect_id, lhs.type()), + null_pointer_exprt(to_pointer_type(lhs.type())), + ns, + true, + false); + } + } + } +}; + +typedef value_set_analysis_baset test_value_set_analysist; + +#define TEST_PREFIX "java::CustomVSATest." +#define TEST_FUNCTION_NAME TEST_PREFIX "test:()V" +#define TEST_LOCAL_PREFIX TEST_FUNCTION_NAME "::" + +template +static value_setst::valuest +get_values(const VST &value_set, const namespacet &ns, const exprt &expr) +{ + value_setst::valuest vals; + value_set.read_value_set(expr, vals, ns); + return vals; +} + +static std::size_t exprs_with_id( + const value_setst::valuest &exprs, const irep_idt &id) +{ + return std::count_if( + exprs.begin(), + exprs.end(), + [&id](const exprt &expr) + { + return expr.id()==id || + (expr.id()==ID_object_descriptor && + to_object_descriptor_expr(expr).object().id()==id); + }); +} + +SCENARIO("test_value_set_analysis", + "[core][pointer-analysis][value_set_analysis]") +{ + GIVEN("Normal and custom value-set analysis of CustomVSATest::test") + { + goto_modelt goto_model; + null_message_handlert null_output; + cmdlinet command_line; + + // This classpath is the default, but the config object + // is global and previous unit tests may have altered it + command_line.set("java-cp-include-files", "."); + config.java.classpath={"."}; + command_line.args.push_back("pointer-analysis/CustomVSATest.jar"); + + register_language(new_java_bytecode_language); + + bool model_init_failed= + initialize_goto_model(goto_model, command_line, null_output); + REQUIRE(!model_init_failed); + + namespacet ns(goto_model.symbol_table); + + // Fully inline the test program, to avoid VSA conflating + // constructor callsites confusing the results we're trying to check: + goto_function_inline(goto_model, TEST_FUNCTION_NAME, null_output); + + const goto_programt &test_function= + goto_model.goto_functions.function_map.at(TEST_PREFIX "test:()V").body; + + value_set_analysist::locationt test_function_end= + std::prev(test_function.instructions.end()); + + value_set_analysist normal_analysis(ns); + normal_analysis(goto_model.goto_functions); + const auto &normal_function_end_vs= + normal_analysis[test_function_end].value_set; + + test_value_set_analysist test_analysis(ns); + test_analysis(goto_model.goto_functions); + const auto &test_function_end_vs= + test_analysis[test_function_end].value_set; + + reference_typet jlo_ref_type=java_lang_object_type(); + + WHEN("Writing to a local named 'ignored'") + { + symbol_exprt written_symbol( + TEST_LOCAL_PREFIX "23::ignored", jlo_ref_type); + THEN("The normal analysis should write to it") + { + auto normal_exprs= + get_values(normal_function_end_vs, ns, written_symbol); + REQUIRE(exprs_with_id(normal_exprs, ID_dynamic_object)==1); + REQUIRE(exprs_with_id(normal_exprs, ID_unknown)==0); + } + THEN("The custom analysis should ignore the write to it") + { + auto test_exprs= + get_values(test_function_end_vs, ns, written_symbol); + REQUIRE(exprs_with_id(test_exprs, ID_dynamic_object)==0); + REQUIRE(exprs_with_id(test_exprs, ID_unknown)==1); + } + } + + WHEN("Writing to a local named 'no_write'") + { + symbol_exprt written_symbol( + TEST_LOCAL_PREFIX "31::no_write", jlo_ref_type); + THEN("The normal analysis should write to it") + { + auto normal_exprs= + get_values(normal_function_end_vs, ns, written_symbol); + REQUIRE(exprs_with_id(normal_exprs, ID_dynamic_object)==1); + REQUIRE(exprs_with_id(normal_exprs, ID_unknown)==0); + } + THEN("The custom analysis should ignore the write to it") + { + auto test_exprs= + get_values(test_function_end_vs, ns, written_symbol); + REQUIRE(exprs_with_id(test_exprs, ID_dynamic_object)==0); + REQUIRE(exprs_with_id(test_exprs, ID_unknown)==1); + } + } + + WHEN("Reading from a field named 'never_read'") + { + symbol_exprt written_symbol( + TEST_LOCAL_PREFIX "55::read", jlo_ref_type); + THEN("The normal analysis should find a dynamic object") + { + auto normal_exprs= + get_values(normal_function_end_vs, ns, written_symbol); + REQUIRE(exprs_with_id(normal_exprs, ID_dynamic_object)==1); + REQUIRE(exprs_with_id(normal_exprs, ID_unknown)==0); + } + THEN("The custom analysis should have no information about it") + { + auto test_exprs= + get_values(test_function_end_vs, ns, written_symbol); + REQUIRE(test_exprs.size()==0); + } + } + + WHEN("Reading from a variable named 'maybe_unknown'") + { + symbol_exprt written_symbol( + TEST_PREFIX "maybe_unknown_read", jlo_ref_type); + THEN("The normal analysis should find a dynamic object") + { + auto normal_exprs= + get_values(normal_function_end_vs, ns, written_symbol); + REQUIRE(exprs_with_id(normal_exprs, ID_dynamic_object)==1); + REQUIRE(exprs_with_id(normal_exprs, ID_unknown)==0); + } + THEN("The custom analysis should find a dynamic object " + "*and* an unknown entry") + { + auto test_exprs= + get_values(test_function_end_vs, ns, written_symbol); + REQUIRE(test_exprs.size()==2); + REQUIRE(exprs_with_id(test_exprs, ID_unknown)==1); + REQUIRE(exprs_with_id(test_exprs, ID_dynamic_object)==1); + } + } + + WHEN("Writing to a variable named 'cause'") + { + symbol_exprt read_before_cause_write( + TEST_PREFIX "first_effect_read", jlo_ref_type); + auto normal_exprs_before= + get_values(normal_function_end_vs, ns, read_before_cause_write); + auto test_exprs_before= + get_values(test_function_end_vs, ns, read_before_cause_write); + symbol_exprt read_after_cause_write( + TEST_PREFIX "second_effect_read", jlo_ref_type); + auto normal_exprs_after= + get_values(normal_function_end_vs, ns, read_after_cause_write); + auto test_exprs_after= + get_values(test_function_end_vs, ns, read_after_cause_write); + + THEN("Before writing to 'cause' both analyses should think 'effect' " + "points to some object") + { + REQUIRE(normal_exprs_before.size()==1); + REQUIRE(exprs_with_id(normal_exprs_before, ID_dynamic_object)==1); + + REQUIRE(test_exprs_before.size()==1); + REQUIRE(exprs_with_id(test_exprs_before, ID_dynamic_object)==1); + } + + THEN("After writing to 'cause', the normal analysis should see no change " + "to 'effect', while the custom analysis should see it changed") + { + REQUIRE(normal_exprs_after.size()==1); + REQUIRE(exprs_with_id(normal_exprs_after, ID_dynamic_object)==1); + + REQUIRE(test_exprs_after.size()==1); + REQUIRE(exprs_with_id(test_exprs_after, "NULL-object")==1); + } + } + + // Check that our custom simplifier was invoked during all of the above: + REQUIRE(simplifies>0); + } +} From a99b25418cfdc9cead164dc6f8794a0521ead084 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 13 Oct 2017 10:48:47 +0100 Subject: [PATCH 4/4] Indirect value_set_domaint -> value_sett operations via non-member functions These provide an oportunity for future implementers of value-sets not to have to conform to the same public interface as value_sett, e.g. to provide some type they can't or don't want to augment and provide non-member function specialisations instead. --- src/pointer-analysis/value_set_domain.h | 92 ++++++++++++++++++++++--- 1 file changed, 82 insertions(+), 10 deletions(-) diff --git a/src/pointer-analysis/value_set_domain.h b/src/pointer-analysis/value_set_domain.h index 4b0e0a876cf..163f3a183b3 100644 --- a/src/pointer-analysis/value_set_domain.h +++ b/src/pointer-analysis/value_set_domain.h @@ -17,6 +17,77 @@ Author: Daniel Kroening, kroening@kroening.com #include "value_set.h" +template class value_set_domaint; + +// Forwarders for value_set_domaint's calls against value_sett. +// Specialise these if for some reason you can't just write a member function, +// or for location numbers, expose the field. +template +inline bool value_set_make_union(VST &value_set, const VST &other) +{ + return value_set.make_union(other); +} + +template +inline void value_set_output( + const VST &value_set, const namespacet &ns, std::ostream &out) +{ + value_set.output(ns, out); +} + +template +inline void value_set_clear(VST &value_set) +{ + value_set.clear(); +} + +template +inline void value_set_set_location_number(VST &value_set, unsigned loc) +{ + value_set.location_number=loc; +} + +template +inline void value_set_read_reference_set( + const VST &value_set, + const exprt &expr, + value_setst::valuest &dest, + const namespacet &ns) +{ + value_set.read_reference_set(expr, dest, ns); +} + +template +inline void value_set_do_end_function( + VST &value_set, const exprt &return_expr, const namespacet &ns) +{ + value_set.do_end_function(return_expr, ns); +} + +template +inline void value_set_apply_code( + VST &value_set, const codet &code, const namespacet &ns) +{ + value_set.apply_code(code, ns); +} + +template +inline void value_set_guard( + VST &value_set, const exprt &guard, const namespacet &ns) +{ + value_set.guard(guard, ns); +} + +template +inline void value_set_do_function_call( + VST &value_set, + const irep_idt &function, + const exprt::operandst &arguments, + const namespacet &ns) +{ + value_set.do_function_call(function, arguments, ns); +} + template class value_set_domaint:public domain_baset { @@ -25,23 +96,23 @@ class value_set_domaint:public domain_baset // overloading - bool merge(const value_set_domaint &other, locationt to) + bool merge(const value_set_domaint &other, locationt to) { - return value_set.make_union(other.value_set); + return value_set_make_union(value_set, other.value_set); } virtual void output( const namespacet &ns, std::ostream &out) const { - value_set.output(ns, out); + value_set_output(value_set, ns, out); } virtual void initialize( const namespacet &ns, locationt l) { - value_set.clear(); + value_set_clear(value_set); value_set.location_number=l->location_number; } @@ -50,7 +121,7 @@ class value_set_domaint:public domain_baset const exprt &expr, value_setst::valuest &dest) { - value_set.read_reference_set(expr, dest, ns); + value_set_read_reference_set(value_set, expr, dest, ns); } virtual void transform( @@ -66,8 +137,8 @@ class value_set_domaint:public domain_baset case END_FUNCTION: { - value_set.do_end_function( - static_analysis_baset::get_return_lhs(to_l), ns); + value_set_do_end_function( + value_set, static_analysis_baset::get_return_lhs(to_l), ns); break; } @@ -77,11 +148,11 @@ class value_set_domaint:public domain_baset case ASSIGN: case DECL: case DEAD: - value_set.apply_code(from_l->code, ns); + value_set_apply_code(value_set, from_l->code, ns); break; case ASSUME: - value_set.guard(from_l->guard, ns); + value_set_guard(value_set, from_l->guard, ns); break; case FUNCTION_CALL: @@ -89,7 +160,8 @@ class value_set_domaint:public domain_baset const code_function_callt &code= to_code_function_call(from_l->code); - value_set.do_function_call(to_l->function, code.arguments(), ns); + value_set_do_function_call( + value_set, to_l->function, code.arguments(), ns); } break;