Make the custom bitvector analysis actually work

1. has_values was not initialised or used correctly. Fix-up for bda847f
2. merge would never include new values from the other element and was a no-op
for the "must" case.

Author: tautschnig

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<custom_bitvector_analysist &>(ai);
@@ -484,44 +481,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;
     }
   }
 

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<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);
   }