Merge pull request diffblue#107 from trtikm/feature/removed-suppression

Removed suppression

Author: NathanJPhillips

src/goto-analyzer/taint_summary.cpp

@@ -1142,47 +1142,16 @@ taint_numbered_lvalue_svalue_mapt  transform(
     else if (I.code.get_statement() == "clear_may")
     {
       assert(I.code.operands().size() == 2UL);
-      auto const  taint_name = find_taint_value(I.code.op1(),taint_spec_names);
-      if (taint_name!=invalid_taint)
+      const taint_lvaluet lvalue = I.code.op0();
+      // simplify_expr(find_taint_expression(I.code.op0()), ns);
+      if (lvsa == nullptr)
+        assign(result,taint_object_numbering.number(lvalue),taint_make_bottom());
+      else
       {
-        taint_lvaluet const  lvalue =I.code.op0();
-        // simplify_expr(find_taint_expression(I.code.op0()), ns);
-        if (lvsa == nullptr)
-        {
-          auto lvalue_number=taint_object_numbering.number(lvalue);
-          taint_svaluet rvalue = taint_make_bottom();
-          {
-            auto const  it = a.find(lvalue_number);
-            if (it != a.end())
-            {
-              taint_set_of_svarst symbols = it->second.get_vars();
-              symbols.erase(taint_name);
-              if (!symbols.empty())
-                rvalue = taint_make_bottom();//taint_svaluet(symbols,{taint_name},false,false);
-            }
-          }
-          assign(result,lvalue_number,rvalue);
-        }
-        else
-        {
-          taint_numbered_lvalues_sett lhs;
-          collect_lvsa_access_paths(lvalue,ns,lhs,*lvsa,Iit,taint_object_numbering);
-          if (lhs.size() == 1UL)
-          {
-            taint_svaluet rvalue = taint_make_bottom();
-            {
-              auto const  it = a.find(*lhs.cbegin());
-              if (it != a.end())
-              {
-                taint_set_of_svarst symbols = it->second.get_vars();
-                symbols.erase(taint_name);
-                if (!symbols.empty())
-                  rvalue = taint_make_bottom();//taint_svaluet(symbols,{taint_name},false,false);
-              }
-            }
-            assign(result,*lhs.cbegin(),rvalue);
-          }
-        }
+        taint_numbered_lvalues_sett lhs;
+        collect_lvsa_access_paths(lvalue,ns,lhs,*lvsa,Iit,taint_object_numbering);
+        if (lhs.size() == 1UL)
+          assign(result,*lhs.cbegin(),taint_make_bottom());
       }
     }
     else if(I.code.get_statement()==ID_array_set)

src/goto-analyzer/taint_summary_dump.cpp

@@ -52,17 +52,6 @@ void  taint_dump_svalue_in_html(
         ostr << "T" << symbol;
        first = false;
     }
-    if (!svalue.get_suppressions().empty())
-    {
-      ostr << " <b>\\</b> ";
-      //first = true;
-      for (auto const&  token_sets : svalue.get_suppressions())
-      {
-         //ostr << (first ? "" : " <b>&#x2210;</b> ");
-         ostr << "X" << token_sets.first << " ";
-         //first = false;
-      }
-    }
   }
 }
 

src/goto-analyzer/taint_svalue.cpp

@@ -18,50 +18,20 @@ to the summary based taint analysis.
 #include <algorithm>
 
 
-cond_suppression_idt get_fresh_cond_suppression_id()
-{
-  static cond_suppression_idt id = 0ULL;
-  return ++id;
-}
-
-taint_token_suppressiont::taint_token_suppressiont(
-    const taint_set_of_svarst &in_vars,
-    const cond_suppression_idt in_cond_suppression_id
-    )
-  : vars(in_vars)
-  , cond_suppression_id(in_cond_suppression_id)
-{}
-
-void taint_token_suppressiont::insert(const taint_set_of_svarst &in_vars)
-{
-  vars.insert(in_vars.cbegin(),in_vars.cend());
-}
-
-
 taint_svaluet::taint_svaluet(
     const taint_set_of_tokenst  &in_tokens,
     const taint_set_of_svarst  &in_vars,
-    const taint_set_of_condst  &in_conds,
-    const taint_set_of_token_suppressionst &in_suppressions
-    )
-  : tokens(in_tokens)
-  , vars(in_vars)
-  , conds(in_conds.cbegin(),in_conds.cend())
-  , suppressions(in_suppressions)
+    const taint_set_of_condst  &in_conds)
+  : tokens(in_tokens), vars(in_vars), conds(in_conds.cbegin(),in_conds.cend())
 {}
 
 taint_svaluet::taint_svaluet()
-  : tokens()
-  , vars()
-  , conds()
-  , suppressions()
+  : tokens(), vars(), conds()
 {}
 
 taint_svaluet::taint_svaluet(const taint_svaluet &other)
-  : tokens(other.get_tokens())
-  , vars(other.get_vars())
-  , conds(other.get_conds().cbegin(),other.get_conds().cend())
-  , suppressions(other.get_suppressions())
+  : tokens(other.get_tokens()), vars(other.get_vars()),
+    conds(other.get_conds().cbegin(),other.get_conds().cend())
 {
 }
 
@@ -71,49 +41,14 @@ void taint_svaluet::join(const taint_svaluet &other)
   tokens.insert(other.get_tokens().cbegin(),other.get_tokens().cend());
   vars.insert(other.get_vars().cbegin(),other.get_vars().cend());
   conds.insert(conds.end(),other.get_conds().cbegin(),other.get_conds().cend());
-  suppressions.insert(other.get_suppressions().cbegin(),
-                      other.get_suppressions().cend());
-}
-
-void taint_svaluet::suppress(const taint_tokent token)
-{
-  tokens.erase(token);
-
-  cond_suppression_idt cond_suppression_id;
-  auto it = suppressions.find(token);
-  if (it == suppressions.end())
-  {
-    cond_suppression_id = get_fresh_cond_suppression_id();
-    it = suppressions.insert({token,{get_vars(),cond_suppression_id}}).first;
-  }
-  else
-  {
-    cond_suppression_id = it->second.get_cond_suppression_id();
-    it->second.insert(get_vars());
-  }
-
-  taint_set_of_condst new_conds;
-  for (auto& cond : conds)
-  {
-    taint_condt  tmp = cond;
-    tmp.insert(cond_suppression_id);
-    new_conds.push_back(tmp);
-  }
-  using std::swap;
-  swap(new_conds,conds);
 }
 
 
 taint_condt::taint_condt(
     const std::vector<taint_tokent> &in_tested_symbols,
     const std::vector<taint_svaluet> &in_conditionals,
-    const taint_svaluet &in_result,
-    const taint_set_of_cond_suppression_idst in_suppression_ids
-    )
-  : tested_symbols(in_tested_symbols)
-  , conditionals(in_conditionals)
-  , result(in_result)
-  , suppression_ids(in_suppression_ids)
+    const taint_svaluet &in_result)
+  : tested_symbols(in_tested_symbols), conditionals(in_conditionals), result(in_result)
 {}
 
 
@@ -125,22 +60,20 @@ taint_svaluet  taint_make_symbol()
 
 taint_svaluet  taint_make_symbol(const taint_symbolic_variablet svar)
 {
-  return {{},{svar},{},{}};
+  return {{},{svar},{}};
 }
 
 
 taint_svaluet  taint_make_bottom()
 {
-  return {{},{},{},{}};
+  return {{},{},{}};
 }
 
 bool equal(const taint_svaluet &a, const taint_svaluet &b)
 {
   return a.get_tokens() == b.get_tokens() &&
          a.get_vars() == b.get_vars() &&
-         a.get_conds() == b.get_conds() &&
-         a.get_suppressions() == b.get_suppressions()
-         ;
+         a.get_conds() == b.get_conds();
 }
 
 bool  proper_subset(const taint_svaluet &a, const taint_svaluet &b)
@@ -171,10 +104,6 @@ bool  proper_subset(const taint_svaluet &a, const taint_svaluet &b)
     if (find(b.get_conds().begin(),b.get_conds().end(),elem) == b.get_conds().end())
       return false;
 
-  // TODO: this condition should be improved!
-  if (!(a.get_suppressions() == b.get_suppressions()))
-    return false;
-
   return true;
 }
 
@@ -185,80 +114,18 @@ taint_svaluet join(const taint_svaluet &a, const taint_svaluet &b)
   return result;
 }
 
-taint_svaluet suppress(const taint_svaluet &a, const taint_tokent token)
-{
-  taint_svaluet result=a;
-  result.suppress(token);
-  return result;
-}
-
-
 bool operator==(const taint_condt &a, const taint_condt &b)
 {
   return a.get_tested_symbols() == b.get_tested_symbols() &&
          a.get_conditionals() == b.get_conditionals() &&
-         a.get_result_expression() == b.get_result_expression() &&
-         a.get_suppression_ids() == b.get_suppression_ids()
-         ;
-}
-
-bool operator==(const taint_token_suppressiont &a,
-                const taint_token_suppressiont &b)
-{
-  return a.get_cond_suppression_id() == b.get_cond_suppression_id() &&
-         a.get_vars() == a.get_vars();
+         a.get_result_expression() == b.get_result_expression();
 }
 
-
-//taint_svaluet  suppression(
-//    taint_svaluet const&  a,
-//    taint_svaluet::supressiont const&  sub)
-//{
-//  if (a.is_bottom() || a.is_top() || sub.empty())
-//    return a;
-
-//  taint_set_of_svarst  result_set;
-//  std::vector<taint_symbolic_variablet> result_vector;
-//  std::set_difference(
-//      a.get_vars().cbegin(),a.get_vars().cend(),
-//      sub.cbegin(),sub.cend(),
-//      std::inserter(result_vector,result_vector.end())
-//      );
-//#ifdef USE_BOOST
-//  result_set.insert(boost::container::ordered_unique_range_t(),result_vector.begin(),result_vector.end());
-//#else
-//  result.insert(result_vector.begin(),result_vector.end());
-//#endif
-
-//  if (result_set.empty())
-//    return taint_make_bottom();
-
-//  taint_svaluet::supressiont  result_suppression;
-//  std::set_union(
-//      a.suppression().cbegin(),a.suppression().cend(),
-//      sub.cbegin(),sub.cend(),
-//      std::inserter(result_suppression,result_suppression.end())
-//      );
-
-//  return {result_set,result_suppression,false,false};
-//}
-
 //void taint_svaluet::add_all(const taint_svaluet& other)
 //{
 //  if(m_is_top)
 //    return;
 //  if(other.m_expression.size())
 //    m_is_bottom=false;
-//#ifdef USE_BOOST
-//  m_expression.insert(boost::container::ordered_unique_range_t(),other.m_expression.begin(),other.m_expression.end());
-//#else
 //  m_expression.insert(other.m_expression.begin(),other.m_expression.end());
-//#endif
-//  taint_svaluet::supressiont  result_suppression;
-//  std::set_intersection(
-//    suppression().cbegin(),suppression().cend(),
-//    other.suppression().cbegin(),other.suppression().cend(),
-//    std::inserter(result_suppression,result_suppression.end())
-//  );
-//  m_suppression=std::move(result_suppression);
 //}