Merge pull request #1485 from diffblue/std_expr_typing

tautschnig · web-flow · commit 5191170c5ba6 · 2017-10-18T09:37:54.000+01:00
elaborate typing of std_expr expression classes
diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp
@@ -67,11 +67,17 @@ irep_idt custom_bitvector_domaint::object2id(const exprt &src)
     }
     else if(op.id()==ID_typecast)
     {
-      return object2id(dereference_exprt(to_typecast_expr(op).op()));
+      irep_idt op_id=object2id(to_typecast_expr(op).op());
+
+      if(op_id.empty())
+        return irep_idt();
+      else
+        return '*'+id2string(op_id);
     }
     else
     {
       irep_idt op_id=object2id(op);
+
       if(op_id.empty())
         return irep_idt();
       else
@@ -188,9 +194,8 @@ std::set<exprt> custom_bitvector_analysist::aliases(
     std::set<exprt> result;
 
     for(const auto &pointer : pointer_set)
-    {
-      result.insert(dereference_exprt(pointer));
-    }
+      if(pointer.type().id()==ID_pointer)
+        result.insert(dereference_exprt(pointer));
 
     result.insert(src);
 
@@ -300,36 +305,39 @@ void custom_bitvector_domaint::transform(
 
             exprt lhs=code_function_call.arguments()[0];
 
-            if(lhs.is_constant() &&
-               to_constant_expr(lhs).get_value()==ID_NULL) // NULL means all
+            if(lhs.type().id()==ID_pointer)
             {
-              if(mode==modet::CLEAR_MAY)
+              if(lhs.is_constant() &&
+                 to_constant_expr(lhs).get_value()==ID_NULL) // NULL means all
               {
-                for(auto &bit : may_bits)
-                  clear_bit(bit.second, bit_nr);
-
-                // erase blank ones
-                erase_blank_vectors(may_bits);
+                if(mode==modet::CLEAR_MAY)
+                {
+                  for(auto &bit : may_bits)
+                    clear_bit(bit.second, bit_nr);
+
+                  // erase blank ones
+                  erase_blank_vectors(may_bits);
+                }
+                else if(mode==modet::CLEAR_MUST)
+                {
+                  for(auto &bit : must_bits)
+                    clear_bit(bit.second, bit_nr);
+
+                  // erase blank ones
+                  erase_blank_vectors(must_bits);
+                }
               }
-              else if(mode==modet::CLEAR_MUST)
+              else
               {
-                for(auto &bit : must_bits)
-                  clear_bit(bit.second, bit_nr);
-
-                // erase blank ones
-                erase_blank_vectors(must_bits);
-              }
-            }
-            else
-            {
-              dereference_exprt deref(lhs);
+                dereference_exprt deref(lhs);
 
-              // may alias other stuff
-              std::set<exprt> lhs_set=cba.aliases(deref, from);
+                // may alias other stuff
+                std::set<exprt> lhs_set=cba.aliases(deref, from);
 
-              for(const auto &lhs : lhs_set)
-              {
-                set_bit(lhs, bit_nr, mode);
+                for(const auto &lhs : lhs_set)
+                {
+                  set_bit(lhs, bit_nr, mode);
+                }
               }
             }
           }
@@ -415,40 +423,43 @@ void custom_bitvector_domaint::transform(
 
         exprt lhs=instruction.code.op0();
 
-        if(lhs.is_constant() &&
-           to_constant_expr(lhs).get_value()==ID_NULL) // NULL means all
+        if(lhs.type().id()==ID_pointer)
         {
-          if(mode==modet::CLEAR_MAY)
+          if(lhs.is_constant() &&
+             to_constant_expr(lhs).get_value()==ID_NULL) // NULL means all
           {
-            for(bitst::iterator b_it=may_bits.begin();
-                b_it!=may_bits.end();
-                b_it++)
-              clear_bit(b_it->second, bit_nr);
+            if(mode==modet::CLEAR_MAY)
+            {
+              for(bitst::iterator b_it=may_bits.begin();
+                  b_it!=may_bits.end();
+                  b_it++)
+                clear_bit(b_it->second, bit_nr);
 
-            // erase blank ones
-            erase_blank_vectors(may_bits);
-          }
-          else if(mode==modet::CLEAR_MUST)
-          {
-            for(bitst::iterator b_it=must_bits.begin();
-                b_it!=must_bits.end();
-                b_it++)
-              clear_bit(b_it->second, bit_nr);
+              // erase blank ones
+              erase_blank_vectors(may_bits);
+            }
+            else if(mode==modet::CLEAR_MUST)
+            {
+              for(bitst::iterator b_it=must_bits.begin();
+                  b_it!=must_bits.end();
+                  b_it++)
+                clear_bit(b_it->second, bit_nr);
 
-            // erase blank ones
-            erase_blank_vectors(must_bits);
+              // erase blank ones
+              erase_blank_vectors(must_bits);
+            }
           }
-        }
-        else
-        {
-          dereference_exprt deref(lhs);
+          else
+          {
+            dereference_exprt deref(lhs);
 
-          // may alias other stuff
-          std::set<exprt> lhs_set=cba.aliases(deref, from);
+            // may alias other stuff
+            std::set<exprt> lhs_set=cba.aliases(deref, from);
 
-          for(const auto &lhs : lhs_set)
-          {
-            set_bit(lhs, bit_nr, mode);
+            for(const auto &lhs : lhs_set)
+            {
+              set_bit(lhs, bit_nr, mode);
+            }
           }
         }
       }
@@ -628,6 +639,9 @@ exprt custom_bitvector_domaint::eval(
 
       exprt pointer=src.op0();
 
+      if(pointer.type().id()!=ID_pointer)
+        return src;
+
       if(pointer.is_constant() &&
          to_constant_expr(pointer).get_value()==ID_NULL) // NULL means all
       {
diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp
@@ -2127,9 +2127,11 @@ void cpp_typecheck_resolvet::apply_template_args(
 
         DATA_INVARIANT(struct_type.has_component(new_symbol.name),
                        "method should exist in struct");
-        member_exprt member(code_type);
-        member.set_component_name(new_symbol.name);
-        member.struct_op()=*fargs.operands.begin();
+
+        member_exprt member(
+          *fargs.operands.begin(),
+          new_symbol.name,
+          code_type);
         member.add_source_location()=source_location;
         expr.swap(member);
         return;
diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp
@@ -417,7 +417,7 @@ void interpretert::execute_decl()
 
 /// retrieves the member at offset
 /// \par parameters: an object and a memory offset
-irep_idt interpretert::get_component_id(
+struct_typet::componentt interpretert::get_component(
   const irep_idt &object,
   unsigned offset)
 {
@@ -428,15 +428,16 @@ irep_idt interpretert::get_component_id(
 
   const struct_typet &struct_type=to_struct_type(real_type);
   const struct_typet::componentst &components=struct_type.components();
-  for(struct_typet::componentst::const_iterator it=components.begin();
-      it!=components.end(); it++)
+
+  for(const auto &c : components)
   {
     if(offset<=0)
-      return it->id();
-    size_t size=get_size(it->type());
-    offset-=size;
+      return c;
+
+    offset-=get_size(c.type());
   }
-  return object;
+
+  throw "access out of struct bounds";
 }
 
 /// returns the type object corresponding to id
@@ -600,6 +601,7 @@ exprt interpretert::get_value(
       result.set_value(ID_NULL);
       return result;
     }
+
     if(rhs[offset]<memory.size())
     {
       // We want the symbol pointed to
@@ -612,15 +614,18 @@ exprt interpretert::get_value(
 
       if(offset==0)
         return address_of_exprt(symbol_expr);
+
       if(ns.follow(type).id()==ID_struct)
       {
-        irep_idt member_id=get_component_id(identifier, offset);
-        member_exprt member_expr(symbol_expr, member_id);
+        const auto c=get_component(identifier, offset);
+        member_exprt member_expr(symbol_expr, c);
         return address_of_exprt(member_expr);
       }
+
       index_exprt index_expr(
         symbol_expr,
         from_integer(offset, integer_typet()));
+
       return index_expr;
     }
 
diff --git a/src/goto-programs/interpreter_class.h b/src/goto-programs/interpreter_class.h
@@ -16,12 +16,13 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/invariant.h>
+#include <util/std_types.h>
 #include <util/sparse_vector.h>
+#include <util/message.h>
 
 #include "goto_functions.h"
 #include "goto_trace.h"
 #include "json_goto_trace.h"
-#include "util/message.h"
 
 class interpretert:public messaget
 {
@@ -195,7 +196,10 @@ class interpretert:public messaget
   bool unbounded_size(const typet &);
   size_t get_size(const typet &type);
 
-  irep_idt get_component_id(const irep_idt &object, unsigned offset);
+  struct_typet::componentt get_component(
+    const irep_idt &object,
+    unsigned offset);
+
   typet get_type(const irep_idt &id) const;
   exprt get_value(
     const typet &type,
diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp
@@ -1333,19 +1333,24 @@ exprt string_abstractiont::member(const exprt &a, whatt what)
 {
   if(a.is_nil())
     return a;
+
   assert(type_eq(a.type(), string_struct, ns) ||
       is_ptr_string_struct(a.type()));
 
-  member_exprt result(build_type(what));
-  result.struct_op()=a.type().id()==ID_pointer?
+  exprt struct_op=
+    a.type().id()==ID_pointer?
     dereference_exprt(a, string_struct):a;
 
+  irep_idt component_name;
+
   switch(what)
   {
-  case whatt::IS_ZERO: result.set_component_name("is_zero"); break;
-  case whatt::SIZE: result.set_component_name("size"); break;
-  case whatt::LENGTH: result.set_component_name("length"); break;
+  case whatt::IS_ZERO: component_name="is_zero"; break;
+  case whatt::SIZE: component_name="size"; break;
+  case whatt::LENGTH: component_name="length"; break;
   }
 
+  member_exprt result(struct_op, component_name, build_type(what));
+
   return result;
 }
diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp
@@ -200,7 +200,7 @@ void linkingt::detailed_conflict_report_rec(
           conflict_path=conflict_path_before;
           conflict_path.type()=t1;
           conflict_path=
-            member_exprt(conflict_path, components1[i].get_name());
+            member_exprt(conflict_path, components1[i]);
 
           if(depth>0 &&
              parent_types.find(t1)==parent_types.end())
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
@@ -833,7 +833,7 @@ void value_sett::get_value_set_rec(
 
         found=true;
 
-        member_exprt member(expr.op0(), name, c_it->type());
+        member_exprt member(expr.op0(), *c_it);
         get_value_set_rec(member, dest, suffix, original_type, ns);
       }
     }
@@ -1050,9 +1050,7 @@ void value_sett::get_reference_set_rec(
       {
         objectt o=it->second;
 
-        member_exprt member_expr(expr.type());
-        member_expr.op0()=object;
-        member_expr.set_component_name(component_name);
+        member_exprt member_expr(object, component_name, expr.type());
 
         // We cannot introduce a cast from scalar to non-scalar,
         // thus, we can only adjust the types of structs and unions.
@@ -1121,9 +1119,7 @@ void value_sett::assign(
       if(subtype.id()==ID_code ||
          c_it->get_is_padding()) continue;
 
-      member_exprt lhs_member(subtype);
-      lhs_member.set_component_name(name);
-      lhs_member.op0()=lhs;
+      member_exprt lhs_member(lhs, name, subtype);
 
       exprt rhs_member;
 
@@ -1688,9 +1684,7 @@ exprt value_sett::make_member(
 
   // give up
   typet subtype=struct_union_type.component_type(component_name);
-  member_exprt member_expr(subtype);
-  member_expr.op0()=src;
-  member_expr.set_component_name(component_name);
+  member_exprt member_expr(src, component_name, subtype);
 
   return member_expr;
 }
diff --git a/src/solvers/flattening/pointer_logic.cpp b/src/solvers/flattening/pointer_logic.cpp
@@ -146,14 +146,11 @@ exprt pointer_logict::object_rec(
 
     mp_integer current_offset=0;
 
-    for(struct_typet::componentst::const_iterator
-        it=components.begin();
-        it!=components.end();
-        it++)
+    for(const auto &c : components)
     {
       assert(offset>=current_offset);
 
-      const typet &subtype=it->type();
+      const typet &subtype=c.type();
 
       mp_integer sub_size=pointer_offset_size(subtype, ns);
       assert(sub_size>0);
@@ -162,9 +159,7 @@ exprt pointer_logict::object_rec(
       if(new_offset>offset)
       {
         // found it
-        member_exprt tmp(subtype);
-        tmp.set_component_name(it->get_name());
-        tmp.op0()=src;
+        member_exprt tmp(src, c);
 
         return object_rec(
           offset-current_offset, pointer_type, tmp);
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
