Merge pull request diffblue#103 from trtikm/security_scanner__extended_expressivity_PR

Added support of suppression of tokens (enabling the sanitisation).

Author: NathanJPhillips

src/cbmc.config

@@ -1,2 +1,2 @@
 // ADD PREDEFINED MACROS HERE!
-#define __cplusplus 201103
+#define USE_BOOST

src/goto-analyzer/taint_summary.cpp

@@ -514,6 +514,7 @@ static void  build_substituted_summary(
           }
           substituted_summary.insert({
               lhs,
+              // TODO: Do apply suppression here!!
               substituted_svalue //suppression(substituted_svalue,lvalue_svalue.second.suppression())
               });
         }

src/goto-analyzer/taint_summary_dump.cpp

@@ -52,19 +52,17 @@ void  taint_dump_svalue_in_html(
         ostr << "T" << symbol;
        first = false;
     }
-//    if (!svalue.suppression().empty())
-//      ostr << " <b>\\</b> ";
-//    first = true;
-//    for (auto const&  symbol : svalue.suppression())
-//    {
-//       ostr << (first ? "" : " <b>&#x2210;</b> ");
-//       auto const  name_it = taint_spec_names.find(symbol);
-//       if (name_it != taint_spec_names.cend())
-//         ostr << name_it->second;
-//       else
-//         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

@@ -1,4 +1,4 @@
-/*******************************************************************	\
+/*******************************************************************\
 
 Module: taint_svalue
 
@@ -10,34 +10,58 @@ This module defines the structure of symbolic expressions. A symbolic expression
 is an abstract value assigned to a memmory access path. This module is related
 to the summary based taint analysis.
 
-@ Copyright Diffblue, Ltd.
+@ Copyright DiffBlue, Ltd.
 
 \*******************************************************************/
 
 #include <goto-analyzer/taint_svalue.h>
 #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_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)
 {}
 
 taint_svaluet::taint_svaluet()
   : tokens()
   , vars()
   , conds()
+  , suppressions()
 {}
 
 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())
 {
 }
 
@@ -54,16 +78,49 @@ void taint_svaluet::join(const taint_svaluet &other)
   vars.insert(other.get_vars().cbegin(),other.get_vars().cend());
 #endif
   conds.insert(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.insert(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_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)
 {}
 
 
@@ -75,20 +132,21 @@ 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_conds() == b.get_conds() &&
+         a.get_suppressions() == b.get_suppressions()
          ;
 }
 
@@ -120,6 +178,10 @@ bool  proper_subset(const taint_svaluet &a, const taint_svaluet &b)
     if (b.get_conds().count(elem) == 0ULL)
       return false;
 
+  // TODO: this condition should be improved!
+  if (!(a.get_suppressions() == b.get_suppressions()))
+    return false;
+
   return true;
 }
 
@@ -130,15 +192,29 @@ 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_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();
+}
 
 
 //taint_svaluet  suppression(