Replace objectt in value_set_fivrns.*

Owen Jones · Owen Jones · commit c54389259b18 · 2017-11-30T11:47:03.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_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp
@@ -134,8 +134,8 @@ void value_set_fivrnst::output_entry(
     {
       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+='*';
 
@@ -211,8 +211,8 @@ exprt value_set_fivrnst::to_expr(object_map_dt::const_iterator 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();
 
@@ -476,32 +476,31 @@ void value_set_fivrnst::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_from(dest, it->first, object);
+        insert_from(dest, it->first, offset);
       }
 
       return;
@@ -689,17 +688,16 @@ void value_set_fivrnst::get_reference_set_rec(
         if(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_from(dest, index_expr, o);
       }
@@ -738,7 +736,7 @@ void value_set_fivrnst::get_reference_set_rec(
       }
       else
       {
-        objectt o=it->second;
+        offsett o = it->second;
 
         exprt member_expr(ID_member, expr.type());
         member_expr.copy_to_operands(object);
@@ -983,7 +981,7 @@ void value_set_fivrnst::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_to(new_object_map, tmp, o);
@@ -1331,39 +1329,39 @@ void value_set_fivrnst::apply_code(
 bool value_set_fivrnst::insert_to(
   object_mapt &dest,
   object_numberingt::number_type n,
-  const objectt &object) const
+  const offsett &offset) const
 {
   object_map_dt &map = dest.write();
   if(map.find(n)==map.end())
   {
-//    std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';
+    //    std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';
     // new
-    map[n]=object;
+    map[n] = offset;
     map.set_valid_at(n, to_function, to_target_index);
     return true;
   }
   else
   {
-//    std::cout << "UPD " << n << '\n';
-    objectt &old=map[n];
+    //    std::cout << "UPD " << n << '\n';
+    offsett &old_offset = map[n];
 
     bool res = map.set_valid_at(n, to_function, to_target_index);
 
-    if(old.offset_is_set && object.offset_is_set)
+    if(old_offset && offset)
     {
-      if(old.offset==object.offset)
+      if(*old_offset == *offset)
         return res;
       else
       {
-        old.offset_is_set=false;
+        old_offset.reset();
         return true;
       }
     }
-    else if(!old.offset_is_set)
+    else if(!old_offset)
       return res;
     else
     {
-      old.offset_is_set=false;
+      old_offset.reset();
       return true;
     }
   }
@@ -1372,39 +1370,39 @@ bool value_set_fivrnst::insert_to(
 bool value_set_fivrnst::insert_from(
   object_mapt &dest,
   object_numberingt::number_type n,
-  const objectt &object) const
+  const offsett &offset) const
 {
   object_map_dt &map = dest.write();
   if(map.find(n)==map.end())
   {
-//    std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';
+    //    std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';
     // new
-    map[n]=object;
+    map[n] = offset;
     map.set_valid_at(n, from_function, from_target_index);
     return true;
   }
   else
   {
-//    std::cout << "UPD " << n << '\n';
-    objectt &old=map[n];
+    //    std::cout << "UPD " << n << '\n';
+    offsett &old_offset = map[n];
 
     bool res = map.set_valid_at(n, from_function, from_target_index);
 
-    if(old.offset_is_set && object.offset_is_set)
+    if(old_offset && offset)
     {
-      if(old.offset==object.offset)
+      if(*old_offset == *offset)
         return res;
       else
       {
-        old.offset_is_set=false;
+        old_offset.reset();
         return true;
       }
     }
-    else if(!old.offset_is_set)
+    else if(!old_offset)
       return res;
     else
     {
-      old.offset_is_set=false;
+      old_offset.reset();
       return true;
     }
   }
diff --git a/src/pointer-analysis/value_set_fivrns.h b/src/pointer-analysis/value_set_fivrns.h
@@ -51,33 +51,21 @@ class value_set_fivrnst
 
   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(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
   {
   public:
     object_map_dt() {}
     static const object_map_dt blank;
 
-    typedef std::map<object_numberingt::number_type, objectt> objmapt;
+    typedef std::map<object_numberingt::number_type, offsett> objmapt;
     objmapt objmap;
 
     // NOLINTNEXTLINE(readability/identifiers)
@@ -97,19 +85,19 @@ class value_set_fivrnst
     bool empty() const { return objmap.empty(); }
     void clear() { objmap.clear(); validity_ranges.clear(); }
 
-    objectt &operator[](object_numberingt::number_type k)
+    offsett &operator[](object_numberingt::number_type k)
     {
       return objmap[k];
     }
 
     // operator[] is the only way to insert something!
     std::pair<iterator, bool>
-    insert(const std::pair<object_numberingt::number_type, objectt> &)
+    insert(const std::pair<object_numberingt::number_type, offsett> &)
     {
       UNREACHABLE;
     }
     iterator
-    insert(iterator, const std::pair<object_numberingt::number_type, objectt> &)
+    insert(iterator, const std::pair<object_numberingt::number_type, offsett> &)
     {
       UNREACHABLE;
     }
@@ -160,28 +148,26 @@ class value_set_fivrnst
 
   bool insert_to(object_mapt &dest, const exprt &src) const
   {
-    return insert_to(dest, object_numbering.number(src), objectt());
+    return insert_to(dest, object_numbering.number(src), offsett());
   }
 
   bool insert_to(
     object_mapt &dest,
     const exprt &src,
-    const mp_integer &offset) const
+    const mp_integer &offset_value) const
   {
-    return insert_to(dest, object_numbering.number(src), objectt(offset));
+    return insert_to(dest, object_numbering.number(src), offsett(offset_value));
   }
 
   bool insert_to(
     object_mapt &dest,
     object_numberingt::number_type n,
-    const objectt &object) const;
+    const offsett &offset) const;
 
-  bool insert_to(
-    object_mapt &dest,
-    const exprt &expr,
-    const objectt &object) const
+  bool
+  insert_to(object_mapt &dest, const exprt &expr, const offsett &offset) const
   {
-    return insert_to(dest, object_numbering.number(expr), object);
+    return insert_to(dest, object_numbering.number(expr), offset);
   }
 
   bool insert_from(object_mapt &dest, object_map_dt::const_iterator it) const
@@ -191,28 +177,27 @@ class value_set_fivrnst
 
   bool insert_from(object_mapt &dest, const exprt &src) const
   {
-    return insert_from(dest, object_numbering.number(src), objectt());
+    return insert_from(dest, object_numbering.number(src), offsett());
   }
 
   bool insert_from(
     object_mapt &dest,
     const exprt &src,
-    const mp_integer &offset) const
+    const mp_integer &offset_value) const
   {
-    return insert_from(dest, object_numbering.number(src), objectt(offset));
+    return insert_from(
+      dest, object_numbering.number(src), offsett(offset_value));
   }
 
   bool insert_from(
     object_mapt &dest,
     object_numberingt::number_type n,
-    const objectt &object) const;
+    const offsett &offset) const;
 
-  bool insert_from(
-    object_mapt &dest,
-    const exprt &expr,
-    const objectt &object) const
+  bool
+  insert_from(object_mapt &dest, const exprt &expr, const offsett &offset) const
   {
-    return insert_from(dest, object_numbering.number(expr), object);
+    return insert_from(dest, object_numbering.number(expr), offset);
   }
 
   struct entryt

Original file line number	Diff line number	Diff line change
`@@ -134,8 +134,8 @@ void value_set_fivrnst::output_entry(`
`134`	`134`	`{`
`135`	`135`	`result+=from_expr(ns, identifier, o)+", ";`
`136`	`136`
`137`		`- if(o_it->second.offset_is_set)`
`138`		`- result+=integer2string(o_it->second.offset)+"";`
	`137`	`+ if(o_it->second)`
	`138`	`+ result += integer2string(*o_it->second) + "";`
`139`	`139`	`else`
`140`	`140`	`result+='*';`
`141`	`141`
`@@ -211,8 +211,8 @@ exprt value_set_fivrnst::to_expr(object_map_dt::const_iterator it) const`
`211`	`211`
`212`	`212`	`od.object()=object;`
`213`	`213`
`214`		`- if(it->second.offset_is_set)`
`215`		`- od.offset()=from_integer(it->second.offset, index_type());`
	`214`	`+ if(it->second)`
	`215`	`+ od.offset() = from_integer(*it->second, index_type());`
`216`	`216`
`217`	`217`	`od.type()=od.object().type();`
`218`	`218`
`@@ -476,32 +476,31 @@ void value_set_fivrnst::get_value_set_rec(`
`476`	`476`
`477`	`477`	`forall_objects(it, pointer_expr_set.read())`
`478`	`478`	`{`
`479`		`- objectt object=it->second;`
	`479`	`+ offsett offset = it->second;`
`480`	`480`
`481`		`- if(object.offset_is_zero() &&`
`482`		`- expr.operands().size()==2)`
	`481`	`+ if(offset_is_zero(offset) && expr.operands().size() == 2)`
`483`	`482`	`{`
`484`	`483`	`if(expr.op0().type().id()!=ID_pointer)`
`485`	`484`	`{`
`486`	`485`	`mp_integer i;`
`487`	`486`	`if(to_integer(expr.op0(), i))`
`488`		`- object.offset_is_set=false;`
	`487`	`+ offset.reset();`
`489`	`488`	`else`
`490`		`- object.offset=(expr.id()==ID_plus)? i : -i;`
	`489`	`+ *offset = (expr.id() == ID_plus) ? i : -i;`
`491`	`490`	`}`
`492`	`491`	`else`
`493`	`492`	`{`
`494`	`493`	`mp_integer i;`
`495`	`494`	`if(to_integer(expr.op1(), i))`
`496`		`- object.offset_is_set=false;`
	`495`	`+ offset.reset();`
`497`	`496`	`else`
`498`		`- object.offset=(expr.id()==ID_plus)? i : -i;`
	`497`	`+ *offset = (expr.id() == ID_plus) ? i : -i;`
`499`	`498`	`}`
`500`	`499`	`}`
`501`	`500`	`else`
`502`		`- object.offset_is_set=false;`
	`501`	`+ offset.reset();`
`503`	`502`
`504`		`- insert_from(dest, it->first, object);`
	`503`	`+ insert_from(dest, it->first, offset);`
`505`	`504`	`}`
`506`	`505`
`507`	`506`	`return;`
`@@ -689,17 +688,16 @@ void value_set_fivrnst::get_reference_set_rec(`
`689`	`688`	`if(ns.follow(object.type())!=array_type)`
`690`	`689`	`index_expr.make_typecast(array.type());`
`691`	`690`
`692`		`- objectt o=a_it->second;`
	`691`	`+ offsett o = a_it->second;`
`693`	`692`	`mp_integer i;`
`694`	`693`
`695`	`694`	`if(offset.is_zero())`
`696`	`695`	`{`
`697`	`696`	`}`
`698`		`- else if(!to_integer(offset, i) &&`
`699`		`- o.offset_is_zero())`
`700`		`- o.offset=i;`
	`697`	`+ else if(!to_integer(offset, i) && offset_is_zero(o))`
	`698`	`+ *o = i;`
`701`	`699`	`else`
`702`		`- o.offset_is_set=false;`
	`700`	`+ o.reset();`
`703`	`701`
`704`	`702`	`insert_from(dest, index_expr, o);`
`705`	`703`	`}`
`@@ -738,7 +736,7 @@ void value_set_fivrnst::get_reference_set_rec(`
`738`	`736`	`}`
`739`	`737`	`else`
`740`	`738`	`{`
`741`		`- objectt o=it->second;`
	`739`	`+ offsett o = it->second;`
`742`	`740`
`743`	`741`	`exprt member_expr(ID_member, expr.type());`
`744`	`742`	`member_expr.copy_to_operands(object);`
`@@ -983,7 +981,7 @@ void value_set_fivrnst::do_free(`
`983`	`981`	`else`
`984`	`982`	`{`
`985`	`983`	`// adjust`
`986`		`- objectt o=o_it->second;`
	`984`	`+ offsett o = o_it->second;`
`987`	`985`	`exprt tmp(object);`
`988`	`986`	`to_dynamic_object_expr(tmp).valid()=exprt(ID_unknown);`
`989`	`987`	`insert_to(new_object_map, tmp, o);`
`@@ -1331,39 +1329,39 @@ void value_set_fivrnst::apply_code(`
`1331`	`1329`	`bool value_set_fivrnst::insert_to(`
`1332`	`1330`	`object_mapt &dest,`
`1333`	`1331`	`object_numberingt::number_type n,`
`1334`		`- const objectt &object) const`
	`1332`	`+ const offsett &offset) const`
`1335`	`1333`	`{`
`1336`	`1334`	`object_map_dt &map = dest.write();`
`1337`	`1335`	`if(map.find(n)==map.end())`
`1338`	`1336`	`{`
`1339`		`-// std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';`
	`1337`	`+ // std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';`
`1340`	`1338`	`// new`
`1341`		`- map[n]=object;`
	`1339`	`+ map[n] = offset;`
`1342`	`1340`	`map.set_valid_at(n, to_function, to_target_index);`
`1343`	`1341`	`return true;`
`1344`	`1342`	`}`
`1345`	`1343`	`else`
`1346`	`1344`	`{`
`1347`		`-// std::cout << "UPD " << n << '\n';`
`1348`		`- objectt &old=map[n];`
	`1345`	`+ // std::cout << "UPD " << n << '\n';`
	`1346`	`+ offsett &old_offset = map[n];`
`1349`	`1347`
`1350`	`1348`	`bool res = map.set_valid_at(n, to_function, to_target_index);`
`1351`	`1349`
`1352`		`- if(old.offset_is_set && object.offset_is_set)`
	`1350`	`+ if(old_offset && offset)`
`1353`	`1351`	`{`
`1354`		`- if(old.offset==object.offset)`
	`1352`	`+ if(old_offset == offset)`
`1355`	`1353`	`return res;`
`1356`	`1354`	`else`
`1357`	`1355`	`{`
`1358`		`- old.offset_is_set=false;`
	`1356`	`+ old_offset.reset();`
`1359`	`1357`	`return true;`
`1360`	`1358`	`}`
`1361`	`1359`	`}`
`1362`		`- else if(!old.offset_is_set)`
	`1360`	`+ else if(!old_offset)`
`1363`	`1361`	`return res;`
`1364`	`1362`	`else`
`1365`	`1363`	`{`
`1366`		`- old.offset_is_set=false;`
	`1364`	`+ old_offset.reset();`
`1367`	`1365`	`return true;`
`1368`	`1366`	`}`
`1369`	`1367`	`}`
`@@ -1372,39 +1370,39 @@ bool value_set_fivrnst::insert_to(`
`1372`	`1370`	`bool value_set_fivrnst::insert_from(`
`1373`	`1371`	`object_mapt &dest,`
`1374`	`1372`	`object_numberingt::number_type n,`
`1375`		`- const objectt &object) const`
	`1373`	`+ const offsett &offset) const`
`1376`	`1374`	`{`
`1377`	`1375`	`object_map_dt &map = dest.write();`
`1378`	`1376`	`if(map.find(n)==map.end())`
`1379`	`1377`	`{`
`1380`		`-// std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';`
	`1378`	`+ // std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';`
`1381`	`1379`	`// new`
`1382`		`- map[n]=object;`
	`1380`	`+ map[n] = offset;`
`1383`	`1381`	`map.set_valid_at(n, from_function, from_target_index);`
`1384`	`1382`	`return true;`
`1385`	`1383`	`}`
`1386`	`1384`	`else`
`1387`	`1385`	`{`
`1388`		`-// std::cout << "UPD " << n << '\n';`
`1389`		`- objectt &old=map[n];`
	`1386`	`+ // std::cout << "UPD " << n << '\n';`
	`1387`	`+ offsett &old_offset = map[n];`
`1390`	`1388`
`1391`	`1389`	`bool res = map.set_valid_at(n, from_function, from_target_index);`
`1392`	`1390`
`1393`		`- if(old.offset_is_set && object.offset_is_set)`
	`1391`	`+ if(old_offset && offset)`
`1394`	`1392`	`{`
`1395`		`- if(old.offset==object.offset)`
	`1393`	`+ if(old_offset == offset)`
`1396`	`1394`	`return res;`
`1397`	`1395`	`else`
`1398`	`1396`	`{`
`1399`		`- old.offset_is_set=false;`
	`1397`	`+ old_offset.reset();`
`1400`	`1398`	`return true;`
`1401`	`1399`	`}`
`1402`	`1400`	`}`
`1403`		`- else if(!old.offset_is_set)`
	`1401`	`+ else if(!old_offset)`
`1404`	`1402`	`return res;`
`1405`	`1403`	`else`
`1406`	`1404`	`{`
`1407`		`- old.offset_is_set=false;`
	`1405`	`+ old_offset.reset();`
`1408`	`1406`	`return true;`
`1409`	`1407`	`}`
`1410`	`1408`	`}`