diff --git a/regression/taint/aliasing1/aliasing1.class b/regression/goto-analyzer/taint-aliasing1/aliasing1.class similarity index 100% rename from regression/taint/aliasing1/aliasing1.class rename to regression/goto-analyzer/taint-aliasing1/aliasing1.class diff --git a/regression/taint/aliasing1/aliasing1.java b/regression/goto-analyzer/taint-aliasing1/aliasing1.java similarity index 100% rename from regression/taint/aliasing1/aliasing1.java rename to regression/goto-analyzer/taint-aliasing1/aliasing1.java diff --git a/regression/taint/aliasing1/taint.json b/regression/goto-analyzer/taint-aliasing1/taint.json similarity index 100% rename from regression/taint/aliasing1/taint.json rename to regression/goto-analyzer/taint-aliasing1/taint.json diff --git a/regression/goto-analyzer/taint-aliasing1/test.desc b/regression/goto-analyzer/taint-aliasing1/test.desc new file mode 100644 index 00000000000..49818c9c42b --- /dev/null +++ b/regression/goto-analyzer/taint-aliasing1/test.desc @@ -0,0 +1,9 @@ +CORE +aliasing1.class +--taint taint.json +^EXIT=0$ +^SIGNAL=0$ +^file aliasing1.java line 10( function .*)?: There is a flow \(taint rule my_sink\)$ +-- +^file aliasing1.java line 8( function .*)?: There is a flow \(taint rule my_sink\)$ +^warning: ignoring diff --git a/regression/taint/basic1/basic1.class b/regression/goto-analyzer/taint-basic1/basic1.class similarity index 100% rename from regression/taint/basic1/basic1.class rename to regression/goto-analyzer/taint-basic1/basic1.class diff --git a/regression/taint/basic1/basic1.java b/regression/goto-analyzer/taint-basic1/basic1.java similarity index 100% rename from regression/taint/basic1/basic1.java rename to regression/goto-analyzer/taint-basic1/basic1.java diff --git a/regression/taint/basic1/taint.json b/regression/goto-analyzer/taint-basic1/taint.json similarity index 100% rename from regression/taint/basic1/taint.json rename to regression/goto-analyzer/taint-basic1/taint.json diff --git a/regression/goto-analyzer/taint-basic1/test.desc b/regression/goto-analyzer/taint-basic1/test.desc new file mode 100644 index 00000000000..0da443b9d31 --- /dev/null +++ b/regression/goto-analyzer/taint-basic1/test.desc @@ -0,0 +1,9 @@ +CORE +basic1.class +--taint taint.json +^EXIT=0$ +^SIGNAL=0$ +^file basic1.java line 8( function .*)?: There is a T1 flow \(taint rule my_h1\)$ +^file basic1.java line 11( function .*)?: There is a T2 flow \(taint rule my_h2\)$ +-- +^warning: ignoring diff --git a/regression/taint/basic2/basic2.class b/regression/goto-analyzer/taint-basic2/basic2.class similarity index 100% rename from regression/taint/basic2/basic2.class rename to regression/goto-analyzer/taint-basic2/basic2.class diff --git a/regression/taint/basic2/basic2.java b/regression/goto-analyzer/taint-basic2/basic2.java similarity index 100% rename from regression/taint/basic2/basic2.java rename to regression/goto-analyzer/taint-basic2/basic2.java diff --git a/regression/taint/basic2/taint.json b/regression/goto-analyzer/taint-basic2/taint.json similarity index 100% rename from regression/taint/basic2/taint.json rename to regression/goto-analyzer/taint-basic2/taint.json diff --git a/regression/goto-analyzer/taint-basic2/test.desc b/regression/goto-analyzer/taint-basic2/test.desc new file mode 100644 index 00000000000..b40e010d8f2 --- /dev/null +++ b/regression/goto-analyzer/taint-basic2/test.desc @@ -0,0 +1,9 @@ +CORE +basic2.class +--taint taint.json +^EXIT=0$ +^SIGNAL=0$ +^file basic2.java line 8( function .*)?: There is a T1 flow \(taint rule my_h1\)$ +^file basic2.java line 11( function .*)?: There is a T2 flow \(taint rule my_h2\)$ +-- +^warning: ignoring diff --git a/regression/taint/interface1/interface1.class b/regression/goto-analyzer/taint-interface1/interface1.class similarity index 97% rename from regression/taint/interface1/interface1.class rename to regression/goto-analyzer/taint-interface1/interface1.class index 31a3578bcdf..056ea5d7b3a 100644 Binary files a/regression/taint/interface1/interface1.class and b/regression/goto-analyzer/taint-interface1/interface1.class differ diff --git a/regression/taint/interface1/interface1.java b/regression/goto-analyzer/taint-interface1/interface1.java similarity index 100% rename from regression/taint/interface1/interface1.java rename to regression/goto-analyzer/taint-interface1/interface1.java diff --git a/regression/goto-analyzer/taint-interface1/my_I.class b/regression/goto-analyzer/taint-interface1/my_I.class new file mode 100644 index 00000000000..f2560c4dda7 Binary files /dev/null and b/regression/goto-analyzer/taint-interface1/my_I.class differ diff --git a/regression/goto-analyzer/taint-interface1/some_class.class b/regression/goto-analyzer/taint-interface1/some_class.class new file mode 100644 index 00000000000..b3261423efd Binary files /dev/null and b/regression/goto-analyzer/taint-interface1/some_class.class differ diff --git a/regression/taint/interface1/taint.json b/regression/goto-analyzer/taint-interface1/taint.json similarity index 100% rename from regression/taint/interface1/taint.json rename to regression/goto-analyzer/taint-interface1/taint.json diff --git a/regression/goto-analyzer/taint-interface1/test.desc b/regression/goto-analyzer/taint-interface1/test.desc new file mode 100644 index 00000000000..bbbbdcd0443 --- /dev/null +++ b/regression/goto-analyzer/taint-interface1/test.desc @@ -0,0 +1,8 @@ +CORE +interface1.class +--taint taint.json +^EXIT=0$ +^SIGNAL=0$ +^file interface1.java line 18( function .*)?: There is a flow! \(taint rule sink_rule\)$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/taint-interproc1/interproc1.class b/regression/goto-analyzer/taint-interproc1/interproc1.class new file mode 100644 index 00000000000..6d8559b3085 Binary files /dev/null and b/regression/goto-analyzer/taint-interproc1/interproc1.class differ diff --git a/regression/goto-analyzer/taint-interproc1/interproc1.java b/regression/goto-analyzer/taint-interproc1/interproc1.java new file mode 100644 index 00000000000..d092c38a536 --- /dev/null +++ b/regression/goto-analyzer/taint-interproc1/interproc1.java @@ -0,0 +1,19 @@ +class interproc1 +{ + static void my_method() + { + Object o=null; + + my_f(o); // T1 source + my_g(o); + } + + static void my_g(Object p) + { + my_h(p); // T1 sink + } + + static void my_f(Object p) { } + static void my_h(Object p) { } +}; + diff --git a/regression/goto-analyzer/taint-interproc1/taint.json b/regression/goto-analyzer/taint-interproc1/taint.json new file mode 100644 index 00000000000..26fadfb2775 --- /dev/null +++ b/regression/goto-analyzer/taint-interproc1/taint.json @@ -0,0 +1,4 @@ +[ +{ "id": "my_f", "kind": "source", "where": "parameter1", "taint": "T1", "function": "interproc1.my_f" }, +{ "id": "my_h1", "kind": "sink", "where": "parameter1", "taint": "T1", "function": "interproc1.my_h", "message": "There is a T1 flow" } +] diff --git a/regression/goto-analyzer/taint-interproc1/test.desc b/regression/goto-analyzer/taint-interproc1/test.desc new file mode 100644 index 00000000000..1a60e0a17f0 --- /dev/null +++ b/regression/goto-analyzer/taint-interproc1/test.desc @@ -0,0 +1,8 @@ +CORE +interproc1.class +--taint taint.json +^EXIT=0$ +^SIGNAL=0$ +^file interproc1.java line 13( function .*)?: There is a T1 flow \(taint rule my_h1\)$ +-- +^warning: ignoring diff --git a/regression/taint/map1/map1.class b/regression/goto-analyzer/taint-map1/map1.class similarity index 100% rename from regression/taint/map1/map1.class rename to regression/goto-analyzer/taint-map1/map1.class diff --git a/regression/taint/map1/map1.java b/regression/goto-analyzer/taint-map1/map1.java similarity index 100% rename from regression/taint/map1/map1.java rename to regression/goto-analyzer/taint-map1/map1.java diff --git a/regression/taint/map1/taint.json b/regression/goto-analyzer/taint-map1/taint.json similarity index 100% rename from regression/taint/map1/taint.json rename to regression/goto-analyzer/taint-map1/taint.json diff --git a/regression/goto-analyzer/taint-map1/test.desc b/regression/goto-analyzer/taint-map1/test.desc new file mode 100644 index 00000000000..5d7ad41dc91 --- /dev/null +++ b/regression/goto-analyzer/taint-map1/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +map1.class +--taint taint.json +^EXIT=0$ +^SIGNAL=0$ +^file map1.java line 12( function .*)?: There is a flow \(taint rule my_sink\)$ +-- +^warning: ignoring diff --git a/regression/taint/Makefile b/regression/taint/Makefile deleted file mode 100644 index 40dbe9c53be..00000000000 --- a/regression/taint/Makefile +++ /dev/null @@ -1,19 +0,0 @@ -default: tests.log - -test: - @../test.pl -c ../../../src/goto-analyzer/goto-analyzer - -tests.log: ../test.pl - @../test.pl -c ../../../src/goto-analyzer/goto-analyzer - -show: - @for dir in *; do \ - if [ -d "$$dir" ]; then \ - vim -o "$$dir/*.java" "$$dir/*.out"; \ - fi; \ - done; - -clean: - find -name '*.out' -execdir $(RM) '{}' \; - find -name '*.gb' -execdir $(RM) '{}' \; - $(RM) tests.log diff --git a/regression/taint/aliasing1/test.desc b/regression/taint/aliasing1/test.desc deleted file mode 100644 index a0ac6401d67..00000000000 --- a/regression/taint/aliasing1/test.desc +++ /dev/null @@ -1,9 +0,0 @@ -CORE -aliasing1.class ---taint taint.json -^EXIT=0$ -^SIGNAL=0$ -^file aliasing1.java line 10: There is a flow \(taint rule my_sink\)$ --- -^file aliasing1.java line 8: There is a flow \(taint rule my_sink\)$ -^warning: ignoring diff --git a/regression/taint/basic1/test.desc b/regression/taint/basic1/test.desc deleted file mode 100644 index c4384ac9655..00000000000 --- a/regression/taint/basic1/test.desc +++ /dev/null @@ -1,9 +0,0 @@ -CORE -basic1.class ---taint taint.json -^EXIT=0$ -^SIGNAL=0$ -^file basic1.java line 8: There is a T1 flow \(taint rule my_h1\)$ -^file basic1.java line 11: There is a T2 flow \(taint rule my_h2\)$ --- -^warning: ignoring diff --git a/regression/taint/basic2/test.desc b/regression/taint/basic2/test.desc deleted file mode 100644 index 428281280c8..00000000000 --- a/regression/taint/basic2/test.desc +++ /dev/null @@ -1,9 +0,0 @@ -CORE -basic2.class ---taint taint.json -^EXIT=0$ -^SIGNAL=0$ -^file basic2.java line 8: There is a T1 flow \(taint rule my_h1\)$ -^file basic2.java line 11: There is a T2 flow \(taint rule my_h2\)$ --- -^warning: ignoring diff --git a/regression/taint/interface1/test.desc b/regression/taint/interface1/test.desc deleted file mode 100644 index 6ac81f15786..00000000000 --- a/regression/taint/interface1/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -interface1.class ---taint taint.json -^EXIT=0$ -^SIGNAL=0$ -^file interface1.java line 18: There is a flow! \(taint rule sink_rule\)$ --- -^warning: ignoring diff --git a/regression/taint/map1/test.desc b/regression/taint/map1/test.desc deleted file mode 100644 index 5526aa21b3a..00000000000 --- a/regression/taint/map1/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -map1.class ---taint taint.json -^EXIT=0$ -^SIGNAL=0$ -^file map1.java line 12: There is a flow \(taint rule my_sink\)$ --- -^warning: ignoring diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp index face9d8ae67..fd64d085850 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/src/analyses/custom_bitvector_analysis.cpp @@ -210,9 +210,6 @@ void custom_bitvector_domaint::transform( ai_baset &ai, const namespacet &ns) { - if(has_values.is_false()) - return; - // upcast of ai custom_bitvector_analysist &cba= static_cast(ai); @@ -337,6 +334,54 @@ void custom_bitvector_domaint::transform( } } } + else + { + goto_programt::const_targett next=from; + ++next; + + // only if there is an actual call, i.e., we have a body + if(next!=to) + { + const code_typet &code_type= + to_code_type(ns.lookup(identifier).type); + + code_function_callt::argumentst::const_iterator arg_it= + code_function_call.arguments().begin(); + for(const auto ¶m : code_type.parameters()) + { + const irep_idt &p_identifier=param.get_identifier(); + if(p_identifier.empty()) + continue; + + // there may be a mismatch in the number of arguments + if(arg_it==code_function_call.arguments().end()) + break; + + // assignments arguments -> parameters + symbol_exprt p=ns.lookup(p_identifier).symbol_expr(); + // may alias other stuff + std::set lhs_set=cba.aliases(p, from); + + vectorst rhs_vectors=get_rhs(*arg_it); + + for(const auto &lhs : lhs_set) + { + assign_lhs(lhs, rhs_vectors); + } + + // is it a pointer? + if(p.type().id()==ID_pointer) + { + dereference_exprt lhs_deref(p); + dereference_exprt rhs_deref(*arg_it); + vectorst rhs_vectors=get_rhs(rhs_deref); + assign_lhs(lhs_deref, rhs_vectors); + } + + ++arg_it; + } + } + } } } break; @@ -484,44 +529,55 @@ bool custom_bitvector_domaint::merge( locationt from, locationt to) { - if(b.has_values.is_false()) - return false; // no change - - if(has_values.is_false()) - { - *this=b; - return true; // change - } - - bool changed=false; + bool changed=has_values.is_false(); + has_values=tvt::unknown(); // first do MAY - for(const auto &bit : may_bits) + bitst::iterator it=may_bits.begin(); + for(const auto &bit : b.may_bits) { - bit_vectort &a_bits=may_bits[bit.first]; - bit_vectort old=a_bits; - a_bits|=bit.second; - if(old!=a_bits) + while(it!=may_bits.end() && it->firstfirst) + { + may_bits.insert(it, bit); changed=true; + } + else if(it!=may_bits.end()) + { + bit_vectort &a_bits=it->second; + bit_vectort old=a_bits; + a_bits|=bit.second; + if(old!=a_bits) + changed=true; + + ++it; + } } // now do MUST - for(auto &bit : must_bits) + it=must_bits.begin(); + for(auto &bit : b.must_bits) { - bitst::const_iterator b_it= - b.must_bits.find(bit.first); - - if(b_it==b.must_bits.end()) + while(it!=must_bits.end() && it->firstfirst) { - bit_vectort old=bit.second; - bit.second&=bit.second; - if(old!=bit.second) + must_bits.insert(it, bit); + changed=true; + } + else if(it!=must_bits.end()) + { + bit_vectort &a_bits=it->second; + bit_vectort old=a_bits; + a_bits&=bit.second; + if(old!=a_bits) changed=true; + + ++it; } } diff --git a/src/analyses/custom_bitvector_analysis.h b/src/analyses/custom_bitvector_analysis.h index ff2884cc2ec..5ef03adbaf2 100644 --- a/src/analyses/custom_bitvector_analysis.h +++ b/src/analyses/custom_bitvector_analysis.h @@ -87,7 +87,7 @@ class custom_bitvector_domaint:public ai_domain_baset tvt has_values; - custom_bitvector_domaint():has_values(true) + custom_bitvector_domaint():has_values(false) { } @@ -145,6 +145,7 @@ class custom_bitvector_analysist:public ait protected: virtual void initialize(const goto_functionst &_goto_functions) { + ait::initialize(_goto_functions); local_may_alias_factory(_goto_functions); }