Replace objectt in value_set_fi.*

Owen Jones · Owen Jones · commit 5ecee627b60b · 2017-11-30T11:43:17.000Z
typedef optional&lt;mp_integer&gt; to offsett and use that instead of objectt. This
reduces code and gets rid of an unintuitive class name.
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
@@ -102,8 +102,8 @@ void value_set_fit::output(
       {
         result="<"+from_expr(ns, identifier, o)+", ";
 
-        if(o_it->second.offset_is_set)
-          result+=integer2string(o_it->second.offset)+"";
+        if(o_it->second)
+          result += integer2string(*o_it->second) + "";
         else
           result+='*';
 
@@ -197,13 +197,12 @@ void value_set_fit::flatten_rec(
             t_it!=temp.write().end();
             t_it++)
         {
-          if(t_it->second.offset_is_set &&
-             it->second.offset_is_set)
+          if(t_it->second && it->second)
           {
-            t_it->second.offset += it->second.offset;
+            *t_it->second += *it->second;
           }
           else
-            t_it->second.offset_is_set=false;
+            t_it->second.reset();
         }
 
         forall_objects(oit, temp.read())
@@ -217,7 +216,7 @@ void value_set_fit::flatten_rec(
   if(generalize_index) // this means we had recursive symbols in there
   {
     Forall_objects(it, dest.write())
-      it->second.offset_is_set = false;
+      it->second.reset();
   }
 
   seen.erase(identifier + e.suffix);
@@ -235,8 +234,8 @@ exprt value_set_fit::to_expr(const object_map_dt::value_type &it) const
 
   od.object()=object;
 
-  if(it.second.offset_is_set)
-    od.offset()=from_integer(it.second.offset, index_type());
+  if(it.second)
+    od.offset() = from_integer(*it.second, index_type());
 
   od.type()=od.object().type();
 
@@ -324,13 +323,12 @@ void value_set_fit::get_value_set(
             t_it!=temp.write().end();
             t_it++)
         {
-          if(t_it->second.offset_is_set &&
-             it->second.offset_is_set)
+          if(t_it->second && it->second)
           {
-            t_it->second.offset += it->second.offset;
+            *t_it->second += *it->second;
           }
           else
-            t_it->second.offset_is_set=false;
+            t_it->second.reset();
 
           flat_map.write()[t_it->first]=t_it->second;
         }
@@ -573,32 +571,31 @@ void value_set_fit::get_value_set_rec(
 
       forall_objects(it, pointer_expr_set.read())
       {
-        objectt object=it->second;
+        offsett offset = it->second;
 
-        if(object.offset_is_zero() &&
-           expr.operands().size()==2)
+        if(offset_is_zero(offset) && expr.operands().size() == 2)
         {
           if(expr.op0().type().id()!=ID_pointer)
           {
             mp_integer i;
             if(to_integer(expr.op0(), i))
-              object.offset_is_set=false;
+              offset.reset();
             else
-              object.offset=(expr.id()==ID_plus)? i : -i;
+              *offset = (expr.id() == ID_plus) ? i : -i;
           }
           else
           {
             mp_integer i;
             if(to_integer(expr.op1(), i))
-              object.offset_is_set=false;
+              offset.reset();
             else
-              object.offset=(expr.id()==ID_plus)? i : -i;
+              *offset = (expr.id() == ID_plus) ? i : -i;
           }
         }
         else
-          object.offset_is_set=false;
+          offset.reset();
 
-        insert(dest, it->first, object);
+        insert(dest, it->first, offset);
       }
 
       return;
@@ -737,13 +734,12 @@ void value_set_fit::get_reference_set(
             t_it!=omt.write().end();
             t_it++)
         {
-          if(t_it->second.offset_is_set &&
-             it->second.offset_is_set)
+          if(t_it->second && it->second)
           {
-            t_it->second.offset += it->second.offset;
+            *t_it->second += *it->second;
           }
           else
-            t_it->second.offset_is_set=false;
+            t_it->second.reset();
         }
 
         forall_objects(it, omt.read())
@@ -826,13 +822,12 @@ void value_set_fit::get_reference_set_sharing_rec(
               t_it!=t2.write().end();
               t_it++)
           {
-            if(t_it->second.offset_is_set &&
-               it->second.offset_is_set)
+            if(t_it->second && it->second)
             {
-              t_it->second.offset += it->second.offset;
+              *t_it->second += *it->second;
             }
             else
-              t_it->second.offset_is_set=false;
+              t_it->second.reset();
           }
 
           forall_objects(it2, t2.read())
@@ -889,17 +884,16 @@ void value_set_fit::get_reference_set_sharing_rec(
            ns.follow(object.type())!=array_type)
           index_expr.make_typecast(array.type());
 
-        objectt o=a_it->second;
+        offsett o = a_it->second;
         mp_integer i;
 
         if(offset.is_zero())
         {
         }
-        else if(!to_integer(offset, i) &&
-                o.offset_is_zero())
-          o.offset=i;
+        else if(!to_integer(offset, i) && offset_is_zero(o))
+          *o = i;
         else
-          o.offset_is_set=false;
+          o.reset();
 
         insert(dest, index_expr, o);
       }
@@ -936,7 +930,7 @@ void value_set_fit::get_reference_set_sharing_rec(
       }
       else
       {
-        objectt o=it->second;
+        offsett o = it->second;
 
         exprt member_expr(ID_member, expr.type());
         member_expr.copy_to_operands(object);
@@ -1189,7 +1183,7 @@ void value_set_fit::do_free(
         else
         {
           // adjust
-          objectt o=o_it->second;
+          offsett o = o_it->second;
           exprt tmp(object);
           to_dynamic_object_expr(tmp).valid()=exprt(ID_unknown);
           insert(new_object_map, tmp, o);
diff --git a/src/pointer-analysis/value_set_fi.h b/src/pointer-analysis/value_set_fi.h
@@ -52,28 +52,17 @@ class value_set_fit
 
   typedef irep_idt idt;
 
-  class objectt
+  /// Represents the offset into an object: either a unique integer offset,
+  /// or an unknown value, represented by `!offset`.
+  typedef optionalt<mp_integer> offsett;
+  bool offset_is_zero(const offsett &offset) const
   {
-  public:
-    objectt():offset_is_set(false)
-    {
-    }
-
-    explicit objectt(const mp_integer &_offset):
-      offset(_offset),
-      offset_is_set(true)
-    {
-    }
-
-    mp_integer offset;
-    bool offset_is_set;
-    bool offset_is_zero() const
-    { return offset_is_set && offset.is_zero(); }
-  };
+    return offset && offset->is_zero();
+  }
 
   class object_map_dt
   {
-    typedef std::map<object_numberingt::number_type, objectt> data_typet;
+    typedef std::map<object_numberingt::number_type, offsett> data_typet;
     data_typet data;
 
   public:
@@ -94,7 +83,7 @@ class value_set_fit
 
     size_t size() const { return data.size(); }
 
-    objectt &operator[](object_numberingt::number_type i)
+    offsett &operator[](object_numberingt::number_type i)
     {
       return data[i];
     }
@@ -127,55 +116,55 @@ class value_set_fit
 
   bool insert(object_mapt &dest, const exprt &src) const
   {
-    return insert(dest, object_numbering.number(src), objectt());
+    return insert(dest, object_numbering.number(src), offsett());
   }
 
   bool insert(
     object_mapt &dest,
     const exprt &src,
-    const mp_integer &offset) const
+    const mp_integer &offset_value) const
   {
-    return insert(dest, object_numbering.number(src), objectt(offset));
+    return insert(dest, object_numbering.number(src), offsett(offset_value));
   }
 
   bool insert(
     object_mapt &dest,
     object_numberingt::number_type n,
-    const objectt &object) const
+    const offsett &offset) const
   {
     if(dest.read().find(n)==dest.read().end())
     {
       // new
-      dest.write()[n]=object;
+      dest.write()[n] = offset;
       return true;
     }
     else
     {
-      objectt &old=dest.write()[n];
+      offsett &old_offset = dest.write()[n];
 
-      if(old.offset_is_set && object.offset_is_set)
+      if(old_offset && offset)
       {
-        if(old.offset==object.offset)
+        if(*old_offset == *offset)
           return false;
         else
         {
-          old.offset_is_set=false;
+          old_offset.reset();
           return true;
         }
       }
-      else if(!old.offset_is_set)
+      else if(!old_offset)
         return false;
       else
       {
-        old.offset_is_set=false;
+        old_offset.reset();
         return true;
       }
     }
   }
 
-  bool insert(object_mapt &dest, const exprt &expr, const objectt &object) const
+  bool insert(object_mapt &dest, const exprt &expr, const offsett &offset) const
   {
-    return insert(dest, object_numbering.number(expr), object);
+    return insert(dest, object_numbering.number(expr), offset);
   }
 
   struct entryt

Original file line number	Diff line number	Diff line change
`@@ -102,8 +102,8 @@ void value_set_fit::output(`
`102`	`102`	`{`
`103`	`103`	`result="<"+from_expr(ns, identifier, o)+", ";`
`104`	`104`
`105`		`- if(o_it->second.offset_is_set)`
`106`		`- result+=integer2string(o_it->second.offset)+"";`
	`105`	`+ if(o_it->second)`
	`106`	`+ result += integer2string(*o_it->second) + "";`
`107`	`107`	`else`
`108`	`108`	`result+='*';`
`109`	`109`
`@@ -197,13 +197,12 @@ void value_set_fit::flatten_rec(`
`197`	`197`	`t_it!=temp.write().end();`
`198`	`198`	`t_it++)`
`199`	`199`	`{`
`200`		`- if(t_it->second.offset_is_set &&`
`201`		`- it->second.offset_is_set)`
	`200`	`+ if(t_it->second && it->second)`
`202`	`201`	`{`
`203`		`- t_it->second.offset += it->second.offset;`
	`202`	`+ t_it->second += it->second;`
`204`	`203`	`}`
`205`	`204`	`else`
`206`		`- t_it->second.offset_is_set=false;`
	`205`	`+ t_it->second.reset();`
`207`	`206`	`}`
`208`	`207`
`209`	`208`	`forall_objects(oit, temp.read())`
`@@ -217,7 +216,7 @@ void value_set_fit::flatten_rec(`
`217`	`216`	`if(generalize_index) // this means we had recursive symbols in there`
`218`	`217`	`{`
`219`	`218`	`Forall_objects(it, dest.write())`
`220`		`- it->second.offset_is_set = false;`
	`219`	`+ it->second.reset();`
`221`	`220`	`}`
`222`	`221`
`223`	`222`	`seen.erase(identifier + e.suffix);`
`@@ -235,8 +234,8 @@ exprt value_set_fit::to_expr(const object_map_dt::value_type &it) const`
`235`	`234`
`236`	`235`	`od.object()=object;`
`237`	`236`
`238`		`- if(it.second.offset_is_set)`
`239`		`- od.offset()=from_integer(it.second.offset, index_type());`
	`237`	`+ if(it.second)`
	`238`	`+ od.offset() = from_integer(*it.second, index_type());`
`240`	`239`
`241`	`240`	`od.type()=od.object().type();`
`242`	`241`
`@@ -324,13 +323,12 @@ void value_set_fit::get_value_set(`
`324`	`323`	`t_it!=temp.write().end();`
`325`	`324`	`t_it++)`
`326`	`325`	`{`
`327`		`- if(t_it->second.offset_is_set &&`
`328`		`- it->second.offset_is_set)`
	`326`	`+ if(t_it->second && it->second)`
`329`	`327`	`{`
`330`		`- t_it->second.offset += it->second.offset;`
	`328`	`+ t_it->second += it->second;`
`331`	`329`	`}`
`332`	`330`	`else`
`333`		`- t_it->second.offset_is_set=false;`
	`331`	`+ t_it->second.reset();`
`334`	`332`
`335`	`333`	`flat_map.write()[t_it->first]=t_it->second;`
`336`	`334`	`}`
`@@ -573,32 +571,31 @@ void value_set_fit::get_value_set_rec(`
`573`	`571`
`574`	`572`	`forall_objects(it, pointer_expr_set.read())`
`575`	`573`	`{`
`576`		`- objectt object=it->second;`
	`574`	`+ offsett offset = it->second;`
`577`	`575`
`578`		`- if(object.offset_is_zero() &&`
`579`		`- expr.operands().size()==2)`
	`576`	`+ if(offset_is_zero(offset) && expr.operands().size() == 2)`
`580`	`577`	`{`
`581`	`578`	`if(expr.op0().type().id()!=ID_pointer)`
`582`	`579`	`{`
`583`	`580`	`mp_integer i;`
`584`	`581`	`if(to_integer(expr.op0(), i))`
`585`		`- object.offset_is_set=false;`
	`582`	`+ offset.reset();`
`586`	`583`	`else`
`587`		`- object.offset=(expr.id()==ID_plus)? i : -i;`
	`584`	`+ *offset = (expr.id() == ID_plus) ? i : -i;`
`588`	`585`	`}`
`589`	`586`	`else`
`590`	`587`	`{`
`591`	`588`	`mp_integer i;`
`592`	`589`	`if(to_integer(expr.op1(), i))`
`593`		`- object.offset_is_set=false;`
	`590`	`+ offset.reset();`
`594`	`591`	`else`
`595`		`- object.offset=(expr.id()==ID_plus)? i : -i;`
	`592`	`+ *offset = (expr.id() == ID_plus) ? i : -i;`
`596`	`593`	`}`
`597`	`594`	`}`
`598`	`595`	`else`
`599`		`- object.offset_is_set=false;`
	`596`	`+ offset.reset();`
`600`	`597`
`601`		`- insert(dest, it->first, object);`
	`598`	`+ insert(dest, it->first, offset);`
`602`	`599`	`}`
`603`	`600`
`604`	`601`	`return;`
`@@ -737,13 +734,12 @@ void value_set_fit::get_reference_set(`
`737`	`734`	`t_it!=omt.write().end();`
`738`	`735`	`t_it++)`
`739`	`736`	`{`
`740`		`- if(t_it->second.offset_is_set &&`
`741`		`- it->second.offset_is_set)`
	`737`	`+ if(t_it->second && it->second)`
`742`	`738`	`{`
`743`		`- t_it->second.offset += it->second.offset;`
	`739`	`+ t_it->second += it->second;`
`744`	`740`	`}`
`745`	`741`	`else`
`746`		`- t_it->second.offset_is_set=false;`
	`742`	`+ t_it->second.reset();`
`747`	`743`	`}`
`748`	`744`
`749`	`745`	`forall_objects(it, omt.read())`
`@@ -826,13 +822,12 @@ void value_set_fit::get_reference_set_sharing_rec(`
`826`	`822`	`t_it!=t2.write().end();`
`827`	`823`	`t_it++)`
`828`	`824`	`{`
`829`		`- if(t_it->second.offset_is_set &&`
`830`		`- it->second.offset_is_set)`
	`825`	`+ if(t_it->second && it->second)`
`831`	`826`	`{`
`832`		`- t_it->second.offset += it->second.offset;`
	`827`	`+ t_it->second += it->second;`
`833`	`828`	`}`
`834`	`829`	`else`
`835`		`- t_it->second.offset_is_set=false;`
	`830`	`+ t_it->second.reset();`
`836`	`831`	`}`
`837`	`832`
`838`	`833`	`forall_objects(it2, t2.read())`
`@@ -889,17 +884,16 @@ void value_set_fit::get_reference_set_sharing_rec(`
`889`	`884`	`ns.follow(object.type())!=array_type)`
`890`	`885`	`index_expr.make_typecast(array.type());`
`891`	`886`
`892`		`- objectt o=a_it->second;`
	`887`	`+ offsett o = a_it->second;`
`893`	`888`	`mp_integer i;`
`894`	`889`
`895`	`890`	`if(offset.is_zero())`
`896`	`891`	`{`
`897`	`892`	`}`
`898`		`- else if(!to_integer(offset, i) &&`
`899`		`- o.offset_is_zero())`
`900`		`- o.offset=i;`
	`893`	`+ else if(!to_integer(offset, i) && offset_is_zero(o))`
	`894`	`+ *o = i;`
`901`	`895`	`else`
`902`		`- o.offset_is_set=false;`
	`896`	`+ o.reset();`
`903`	`897`
`904`	`898`	`insert(dest, index_expr, o);`
`905`	`899`	`}`
`@@ -936,7 +930,7 @@ void value_set_fit::get_reference_set_sharing_rec(`
`936`	`930`	`}`
`937`	`931`	`else`
`938`	`932`	`{`
`939`		`- objectt o=it->second;`
	`933`	`+ offsett o = it->second;`
`940`	`934`
`941`	`935`	`exprt member_expr(ID_member, expr.type());`
`942`	`936`	`member_expr.copy_to_operands(object);`
`@@ -1189,7 +1183,7 @@ void value_set_fit::do_free(`
`1189`	`1183`	`else`
`1190`	`1184`	`{`
`1191`	`1185`	`// adjust`
`1192`		`- objectt o=o_it->second;`
	`1186`	`+ offsett o = o_it->second;`
`1193`	`1187`	`exprt tmp(object);`
`1194`	`1188`	`to_dynamic_object_expr(tmp).valid()=exprt(ID_unknown);`
`1195`	`1189`	`insert(new_object_map, tmp, o);`
Original file line number	Diff line number	Diff line change
`@@ -52,28 +52,17 @@ class value_set_fit`
`52`	`52`
`53`	`53`	`typedef irep_idt idt;`
`54`	`54`
`55`		`- class objectt`
	`55`	`+ /// Represents the offset into an object: either a unique integer offset,`
	`56`	+ /// or an unknown value, represented by `!offset`.
	`57`	`+ typedef optionalt<mp_integer> offsett;`
	`58`	`+ bool offset_is_zero(const offsett &offset) const`
`56`	`59`	`{`
`57`		`- public:`
`58`		`- objectt():offset_is_set(false)`
`59`		`- {`
`60`		`- }`
`61`		`-`
`62`		`- explicit objectt(const mp_integer &_offset):`
`63`		`- offset(_offset),`
`64`		`- offset_is_set(true)`
`65`		`- {`
`66`		`- }`
`67`		`-`
`68`		`- mp_integer offset;`
`69`		`- bool offset_is_set;`
`70`		`- bool offset_is_zero() const`
`71`		`- { return offset_is_set && offset.is_zero(); }`
`72`		`- };`
	`60`	`+ return offset && offset->is_zero();`
	`61`	`+ }`
`73`	`62`
`74`	`63`	`class object_map_dt`
`75`	`64`	`{`
`76`		`- typedef std::map<object_numberingt::number_type, objectt> data_typet;`
	`65`	`+ typedef std::map<object_numberingt::number_type, offsett> data_typet;`
`77`	`66`	`data_typet data;`
`78`	`67`
`79`	`68`	`public:`
`@@ -94,7 +83,7 @@ class value_set_fit`
`94`	`83`
`95`	`84`	`size_t size() const { return data.size(); }`
`96`	`85`
`97`		`- objectt &operator[](object_numberingt::number_type i)`
	`86`	`+ offsett &operator[](object_numberingt::number_type i)`
`98`	`87`	`{`
`99`	`88`	`return data[i];`
`100`	`89`	`}`
`@@ -127,55 +116,55 @@ class value_set_fit`
`127`	`116`
`128`	`117`	`bool insert(object_mapt &dest, const exprt &src) const`
`129`	`118`	`{`
`130`		`- return insert(dest, object_numbering.number(src), objectt());`
	`119`	`+ return insert(dest, object_numbering.number(src), offsett());`
`131`	`120`	`}`
`132`	`121`
`133`	`122`	`bool insert(`
`134`	`123`	`object_mapt &dest,`
`135`	`124`	`const exprt &src,`
`136`		`- const mp_integer &offset) const`
	`125`	`+ const mp_integer &offset_value) const`
`137`	`126`	`{`
`138`		`- return insert(dest, object_numbering.number(src), objectt(offset));`
	`127`	`+ return insert(dest, object_numbering.number(src), offsett(offset_value));`
`139`	`128`	`}`
`140`	`129`
`141`	`130`	`bool insert(`
`142`	`131`	`object_mapt &dest,`
`143`	`132`	`object_numberingt::number_type n,`
`144`		`- const objectt &object) const`
	`133`	`+ const offsett &offset) const`
`145`	`134`	`{`
`146`	`135`	`if(dest.read().find(n)==dest.read().end())`
`147`	`136`	`{`
`148`	`137`	`// new`
`149`		`- dest.write()[n]=object;`
	`138`	`+ dest.write()[n] = offset;`
`150`	`139`	`return true;`
`151`	`140`	`}`
`152`	`141`	`else`
`153`	`142`	`{`
`154`		`- objectt &old=dest.write()[n];`
	`143`	`+ offsett &old_offset = dest.write()[n];`
`155`	`144`
`156`		`- if(old.offset_is_set && object.offset_is_set)`
	`145`	`+ if(old_offset && offset)`
`157`	`146`	`{`
`158`		`- if(old.offset==object.offset)`
	`147`	`+ if(old_offset == offset)`
`159`	`148`	`return false;`
`160`	`149`	`else`
`161`	`150`	`{`
`162`		`- old.offset_is_set=false;`
	`151`	`+ old_offset.reset();`
`163`	`152`	`return true;`
`164`	`153`	`}`
`165`	`154`	`}`
`166`		`- else if(!old.offset_is_set)`
	`155`	`+ else if(!old_offset)`
`167`	`156`	`return false;`
`168`	`157`	`else`
`169`	`158`	`{`
`170`		`- old.offset_is_set=false;`
	`159`	`+ old_offset.reset();`
`171`	`160`	`return true;`
`172`	`161`	`}`
`173`	`162`	`}`
`174`	`163`	`}`
`175`	`164`
`176`		`- bool insert(object_mapt &dest, const exprt &expr, const objectt &object) const`
	`165`	`+ bool insert(object_mapt &dest, const exprt &expr, const offsett &offset) const`
`177`	`166`	`{`
`178`		`- return insert(dest, object_numbering.number(expr), object);`
	`167`	`+ return insert(dest, object_numbering.number(expr), offset);`
`179`	`168`	`}`
`180`	`169`
`181`	`170`	`struct entryt`