From 5f755f8fa24b3b098bdeb1b2da954da6b39b8304 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Thu, 2 Feb 2017 22:52:40 +0100
Subject: [PATCH 1/2] fix shift overflow in irep_hash_container

The return value of `inline size_t operator()(const packedt &p) const` is
`size_t`, the contents of `packedt` is `unsigned`. The result is computed as the
XOR of all contents of the `packedt` vector, shifted to the left `n` times,
where `n` is the index in the `packedt`. Shifting for more than the bits of the
type in `packedt` (here unsigned) is undefined behavior.

This patch removes the UB by i) using size_t type instead of unsigned int and
ii) by using irep_hash/hash_combine to compute the hash of the container, seeded
with the input container size.

The erroneous behaviour was observed in `ansi-c/extern1` regression test.
---
 src/util/irep_hash_container.cpp |  4 ++--
 src/util/irep_hash_container.h   | 16 +++++++++-------
 2 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/src/util/irep_hash_container.cpp b/src/util/irep_hash_container.cpp
index 98ccf14ae40..c79d7a921ba 100644
--- a/src/util/irep_hash_container.cpp
+++ b/src/util/irep_hash_container.cpp
@@ -21,7 +21,7 @@ Function: irep_hash_container_baset::number
 
 \*******************************************************************/
 
-unsigned irep_hash_container_baset::number(const irept &irep)
+size_t irep_hash_container_baset::number(const irept &irep)
 {
   // the ptr-hash provides a speedup of up to 3x
 
@@ -32,7 +32,7 @@ unsigned irep_hash_container_baset::number(const irept &irep)
 
   packedt packed;
   pack(irep, packed);
-  unsigned id=numbering.number(packed);
+  size_t id=numbering.number(packed);
 
   ptr_hash[&irep.read()]=id;
 
diff --git a/src/util/irep_hash_container.h b/src/util/irep_hash_container.h
index 45894b9d79d..5628e1d0ba0 100644
--- a/src/util/irep_hash_container.h
+++ b/src/util/irep_hash_container.h
@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <cstdlib>  // for size_t
 #include <vector>
 
+#include "irep_hash.h"
 #include "numbering.h"
 
 class irept;
@@ -19,9 +20,9 @@ class irept;
 class irep_hash_container_baset
 {
 public:
-  unsigned number(const irept &irep);
+  size_t number(const irept &irep);
 
-  irep_hash_container_baset(bool _full):full(_full)
+  explicit irep_hash_container_baset(bool _full):full(_full)
   {
   }
 
@@ -44,20 +45,21 @@ class irep_hash_container_baset
     }
   };
 
-  typedef std::unordered_map<const void *, unsigned, pointer_hash> ptr_hasht;
+  typedef std::unordered_map<const void *, size_t, pointer_hash>
+    ptr_hasht;
   ptr_hasht ptr_hash;
 
   // this is the second level: content
 
-  typedef std::vector<unsigned> packedt;
+  typedef std::vector<size_t> packedt;
 
   struct vector_hash
   {
     inline size_t operator()(const packedt &p) const
     {
-      size_t result=p.size();
-      for(unsigned i=0; i<p.size(); i++)
-        result^=p[i]<<i;
+      size_t result=p.size(); // seed
+      for(auto elem : p)
+        result=hash_combine(result, elem);
       return result;
     }
   };

From 528fdbbd6a329bb64afd2e523ea9ba12f59616cb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.gudemann@gmail.com>
Date: Fri, 3 Feb 2017 17:23:29 +0100
Subject: [PATCH 2/2] fix type names for linter

---
 src/util/irep_hash_container.h | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/util/irep_hash_container.h b/src/util/irep_hash_container.h
index 5628e1d0ba0..7e796ab6791 100644
--- a/src/util/irep_hash_container.h
+++ b/src/util/irep_hash_container.h
@@ -37,7 +37,7 @@ class irep_hash_container_baset
 
   // this is the first level: address of the content
 
-  struct pointer_hash
+  struct pointer_hasht
   {
     inline size_t operator()(const void *p) const
     {
@@ -45,7 +45,7 @@ class irep_hash_container_baset
     }
   };
 
-  typedef std::unordered_map<const void *, size_t, pointer_hash>
+  typedef std::unordered_map<const void *, size_t, pointer_hasht>
     ptr_hasht;
   ptr_hasht ptr_hash;
 
@@ -53,7 +53,7 @@ class irep_hash_container_baset
 
   typedef std::vector<size_t> packedt;
 
-  struct vector_hash
+  struct vector_hasht
   {
     inline size_t operator()(const packedt &p) const
     {
@@ -64,7 +64,7 @@ class irep_hash_container_baset
     }
   };
 
-  typedef hash_numbering<packedt, vector_hash> numberingt;
+  typedef hash_numbering<packedt, vector_hasht> numberingt;
   numberingt numbering;
 
   void pack(const irept &irep, packedt &);