Merge pull request #999 from tautschnig/fix-taint

Repair custom_bitvector_analysist

Author: Daniel Kroening

regression/taint/aliasing1/aliasing1.class renamed to regression/goto-analyzer/taint-aliasing1/aliasing1.class

@@ -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

regression/taint/aliasing1/aliasing1.java renamed to regression/goto-analyzer/taint-aliasing1/aliasing1.java

@@ -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

regression/taint/aliasing1/taint.json renamed to regression/goto-analyzer/taint-aliasing1/taint.json

@@ -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

regression/goto-analyzer/taint-aliasing1/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

regression/taint/basic1/basic1.class renamed to regression/goto-analyzer/taint-basic1/basic1.class

@@ -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) { }
+};
+

regression/taint/basic1/basic1.java renamed to regression/goto-analyzer/taint-basic1/basic1.java

@@ -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" }
+]

regression/taint/basic1/taint.json renamed to regression/goto-analyzer/taint-basic1/taint.json

@@ -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

regression/goto-analyzer/taint-basic1/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

regression/taint/basic2/basic2.class renamed to regression/goto-analyzer/taint-basic2/basic2.class

@@ -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<custom_bitvector_analysist &>(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 &param : 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<exprt> 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->first<bit.first)
+      ++it;
+    if(it==may_bits.end() || bit.first<it->first)
+    {
+      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->first<bit.first)
     {
-      bit.second=0;
+      it=must_bits.erase(it);
       changed=true;
     }
-    else
+    if(it==must_bits.end() || bit.first<it->first)
     {
-      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;
     }
   }
 

regression/taint/basic2/basic2.java renamed to regression/goto-analyzer/taint-basic2/basic2.java

@@ -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<custom_bitvector_domaint>
 protected:
   virtual void initialize(const goto_functionst &_goto_functions)
   {
+    ait<custom_bitvector_domaint>::initialize(_goto_functions);
     local_may_alias_factory(_goto_functions);
   }