From a18d7ec7e1adc67017695ad831dd6aa8cfec6263 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 16 Oct 2017 09:24:52 +0100 Subject: [PATCH] Revert "Value-set analysis: templatise and virtualise to facilitate customisation" --- 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 | 25 +- 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 | 137 +------ unit/Makefile | 1 - unit/pointer-analysis/CustomVSATest.jar | Bin 969 -> 0 bytes unit/pointer-analysis/CustomVSATest.java | 46 --- .../custom_value_set_analysis.cpp | 336 ------------------ 14 files changed, 172 insertions(+), 673 deletions(-) create mode 100644 src/pointer-analysis/value_set_domain.cpp delete mode 100644 unit/pointer-analysis/CustomVSATest.jar delete mode 100644 unit/pointer-analysis/CustomVSATest.java delete mode 100644 unit/pointer-analysis/custom_value_set_analysis.cpp diff --git a/src/goto-symex/postcondition.cpp b/src/goto-symex/postcondition.cpp index 519d66bfc71..4383439b72d 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.read_value_set(expr.op0(), expr_set, ns); + value_set.get_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 8aa2ec288d6..9911ba51e7d 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.read_value_set(expr, value_set, goto_symex.ns); + state.value_set.get_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 6af38c803c3..7e9837ac737 100644 --- a/src/pointer-analysis/Makefile +++ b/src/pointer-analysis/Makefile @@ -11,6 +11,7 @@ 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 b704f6a2964..3b080f66e62 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 406cac0f99c..40dd0cd520b 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::read_value_set( +void value_sett::get_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) - simplifier(tmp, ns); + simplify(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)) - simplifier(op1, ns); + simplify(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::read_reference_set( +void value_sett::get_reference_set( const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const @@ -1205,12 +1205,6 @@ 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); } } @@ -1488,7 +1482,7 @@ void value_sett::do_end_function( assign(lhs, rhs, ns, false, false); } -void value_sett::apply_code_rec( +void value_sett::apply_code( const codet &code, const namespacet &ns) { @@ -1497,7 +1491,7 @@ void value_sett::apply_code_rec( if(statement==ID_block) { forall_operands(it, code) - apply_code_rec(to_code(*it), ns); + apply_code(to_code(*it), ns); } else if(statement==ID_function_call) { @@ -1615,10 +1609,6 @@ 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'; @@ -1704,6 +1694,3 @@ 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 194209680bb..68c41f4ce16 100644 --- a/src/pointer-analysis/value_set.h +++ b/src/pointer-analysis/value_set.h @@ -24,20 +24,8 @@ class namespacet; class value_sett { - typedef std::function expr_simplifiert; - - static expr_simplifiert default_simplifier; - public: - value_sett(): - location_number(0), - simplifier(default_simplifier) - { - } - - explicit value_sett(expr_simplifiert simplifier): - location_number(0), - simplifier(std::move(simplifier)) + value_sett():location_number(0) { } @@ -178,7 +166,7 @@ class value_sett typedef std::unordered_map valuest; #endif - void read_value_set( + void get_value_set( const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const; @@ -225,10 +213,7 @@ class value_sett void apply_code( const codet &code, - const namespacet &ns) - { - apply_code_rec(code, ns); - } + const namespacet &ns); void assign( const exprt &lhs, @@ -247,7 +232,7 @@ class value_sett const exprt &lhs, const namespacet &ns); - void read_reference_set( + void get_reference_set( const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const; @@ -257,6 +242,13 @@ 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, @@ -280,75 +272,21 @@ class value_sett const exprt &src, exprt &dest) const; - void do_free( - const exprt &op, - const namespacet &ns); - - exprt make_member( - 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( + 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, + void do_free( + const exprt &op, 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) - { - } + exprt make_member( + const exprt &src, + const irep_idt &component_name, + 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 dc03dfc0b04..d4a3388142e 100644 --- a/src/pointer-analysis/value_set_analysis.cpp +++ b/src/pointer-analysis/value_set_analysis.cpp @@ -13,9 +13,74 @@ 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 d13f8903778..b41355abd73 100644 --- a/src/pointer-analysis/value_set_analysis.h +++ b/src/pointer-analysis/value_set_analysis.h @@ -14,80 +14,32 @@ 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; -template -class value_set_analysis_baset: +class value_set_analysist: public value_setst, - public static_analysist > + public static_analysist { public: - typedef value_set_domaint domaint; - typedef static_analysist baset; - typedef typename baset::locationt locationt; - - explicit value_set_analysis_baset(const namespacet &ns):baset(ns) + explicit value_set_analysist(const namespacet &_ns): + static_analysist(_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 - { - 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 - } - } - } + xmlt &dest) const; public: // interface value_sets @@ -96,12 +48,10 @@ class value_set_analysis_baset: const exprt &expr, value_setst::valuest &dest) { - (*this)[l].value_set.read_value_set(expr, dest, baset::ns); + (*this)[l].value_set.get_value_set(expr, dest, 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 new file mode 100644 index 00000000000..4b296b541df --- /dev/null +++ b/src/pointer-analysis/value_set_domain.cpp @@ -0,0 +1,56 @@ +/*******************************************************************\ + +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 163f3a183b3..e59250a0bc0 100644 --- a/src/pointer-analysis/value_set_domain.h +++ b/src/pointer-analysis/value_set_domain.h @@ -17,159 +17,44 @@ 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 { public: - VST value_set; + value_sett value_set; // overloading - bool merge(const value_set_domaint &other, locationt to) + bool merge(const value_set_domaint &other, locationt to) { - return value_set_make_union(value_set, other.value_set); + return value_set.make_union(other.value_set); } virtual void output( const namespacet &ns, std::ostream &out) const { - value_set_output(value_set, ns, out); + value_set.output(ns, out); } virtual void initialize( const namespacet &ns, locationt l) { - value_set_clear(value_set); + value_set.clear(); 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_read_reference_set(value_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( - value_set, 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(value_set, from_l->code, ns); - break; - - case ASSUME: - value_set_guard(value_set, 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( - value_set, to_l->function, code.arguments(), ns); - } - break; - - default: - { - // do nothing - } - } + value_set.get_reference_set(expr, dest, ns); } }; diff --git a/unit/Makefile b/unit/Makefile index 2b6c02e6580..c89872fc1d3 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -20,7 +20,6 @@ SRC += unit_tests.cpp \ miniBDD_new.cpp \ java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp \ java_bytecode/java_utils_test.cpp \ - pointer-analysis/custom_value_set_analysis.cpp \ solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp \ solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \ solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp \ diff --git a/unit/pointer-analysis/CustomVSATest.jar b/unit/pointer-analysis/CustomVSATest.jar deleted file mode 100644 index 8a5f9aaac701706d4c020542bf2021171788684d..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 969 zcmWIWW@Zs#;Nak3P{{Z3W*(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< diff --git a/unit/pointer-analysis/CustomVSATest.java b/unit/pointer-analysis/CustomVSATest.java deleted file mode 100644 index 7df3c6910a6..00000000000 --- a/unit/pointer-analysis/CustomVSATest.java +++ /dev/null @@ -1,46 +0,0 @@ - -public class CustomVSATest { - - public Object never_read; - - 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() { - - Object weak_local = new Object(); - // Under standard VSA the following should be a strong write; - // with our test custom VSA it will be weak. - weak_local = new Object(); - - // Normally this would set the value of `ignored`, but our custom - // VSA discards the instruction completely: - Object ignored = new Object(); - - // Similarly this write should have no effect: - Object no_write = new Object(); - - CustomVSATest vsa = new CustomVSATest(); - vsa.never_read = new Object(); - - // Again this should be disregarded: - Object read = vsa.never_read; - - // 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; - - effect = new Object(); - first_effect_read = effect; - - // 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 deleted file mode 100644 index eb43cd51af3..00000000000 --- a/unit/pointer-analysis/custom_value_set_analysis.cpp +++ /dev/null @@ -1,336 +0,0 @@ -/*******************************************************************\ - -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); - } -}