Merge pull request diffblue#1289 from tautschnig/develop-interpreter-fixes

Replace 3-valued char by enum

Author: Daniel Kroening

src/goto-programs/interpreter.cpp

@@ -503,7 +503,9 @@ exprt interpretert::get_value(
     }
     return result;
   }
-  if(use_non_det && (memory[offset].initialized>=0))
+  if(use_non_det &&
+     memory[offset].initialized!=
+     memory_cellt::initializedt::WRITTEN_BEFORE_READ)
     return side_effect_expr_nondett(type);
   mp_vectort rhs;
   rhs.push_back(memory[offset].value);
@@ -681,15 +683,16 @@ void interpretert::execute_assign()
       size_t size=get_size(code_assign.lhs().type());
       for(size_t i=0; i<size; i++)
       {
-        memory[address+i].initialized=-1;
+        memory[address+i].initialized=
+          memory_cellt::initializedt::READ_BEFORE_WRITTEN;
       }
     }
   }
 }
 
 /// sets the memory at address with the given rhs value (up to sizeof(rhs))
 void interpretert::assign(
-  mp_integer address,
+  const mp_integer &address,
   const mp_vectort &rhs)
 {
   for(size_t i=0; i<rhs.size(); i++)
@@ -706,8 +709,8 @@ void interpretert::assign(
                  << "\n" << eom;
       }
       cell.value=rhs[i];
-      if(cell.initialized==0)
-        cell.initialized=1;
+      if(cell.initialized==memory_cellt::initializedt::UNKNOWN)
+        cell.initialized=memory_cellt::initializedt::WRITTEN_BEFORE_READ;
     }
   }
 }

src/goto-programs/interpreter_class.h

@@ -161,12 +161,18 @@ class interpretert:public messaget
   public:
     memory_cellt() :
     value(0),
-    initialized(0)
+    initialized(initializedt::UNKNOWN)
     {}
     mp_integer value;
     // Initialized is annotated even during reads
+    enum class initializedt
+    {
+      UNKNOWN,
+      WRITTEN_BEFORE_READ,
+      READ_BEFORE_WRITTEN
+    };
     // Set to 1 when written-before-read, -1 when read-before-written
-    mutable char initialized;
+    mutable initializedt initialized;
   };
 
   typedef sparse_vectort<memory_cellt> memoryt;
@@ -210,19 +216,19 @@ class interpretert:public messaget
   void clear_input_flags();
 
   void allocate(
-    mp_integer address,
+    const mp_integer &address,
     size_t size);
 
   void assign(
-    mp_integer address,
+    const mp_integer &address,
     const mp_vectort &rhs);
 
   void read(
-    mp_integer address,
+    const mp_integer &address,
     mp_vectort &dest) const;
 
   void read_unbounded(
-    mp_integer address,
+    const mp_integer &address,
     mp_vectort &dest) const;
 
   virtual void command();
@@ -273,12 +279,12 @@ class interpretert:public messaget
 
   bool byte_offset_to_memory_offset(
     const typet &source_type,
-    mp_integer byte_offset,
+    const mp_integer &byte_offset,
     mp_integer &result);
 
   bool memory_offset_to_byte_offset(
     const typet &source_type,
-    mp_integer cell_offset,
+    const mp_integer &cell_offset,
     mp_integer &result);
 
   void evaluate(

src/goto-programs/interpreter_evaluate.cpp

@@ -24,7 +24,7 @@ Author: Daniel Kroening, [email protected]
 /// reads a memory address and loads it into the dest variable marks cell as
 /// read before written if cell has never been written
 void interpretert::read(
-  mp_integer address,
+  const mp_integer &address,
   mp_vectort &dest) const
 {
   // copy memory region
@@ -36,8 +36,8 @@ void interpretert::read(
     {
       const memory_cellt &cell=memory[integer2size_t(address+i)];
       value=cell.value;
-      if(cell.initialized==0)
-        cell.initialized=-1;
+      if(cell.initialized==memory_cellt::initializedt::UNKNOWN)
+        cell.initialized=memory_cellt::initializedt::READ_BEFORE_WRITTEN;
     }
     else
       value=0;
@@ -47,7 +47,7 @@ void interpretert::read(
 }
 
 void interpretert::read_unbounded(
-  mp_integer address,
+  const mp_integer &address,
   mp_vectort &dest) const
 {
   // copy memory region
@@ -64,8 +64,8 @@ void interpretert::read_unbounded(
     {
       const memory_cellt &cell=memory[integer2size_t(address+i)];
       value=cell.value;
-      if(cell.initialized==0)
-        cell.initialized=-1;
+      if(cell.initialized==memory_cellt::initializedt::UNKNOWN)
+        cell.initialized=memory_cellt::initializedt::READ_BEFORE_WRITTEN;
     }
     else
       value=0;
@@ -76,7 +76,7 @@ void interpretert::read_unbounded(
 
 /// reserves memory block of size at address
 void interpretert::allocate(
-  mp_integer address,
+  const mp_integer &address,
   size_t size)
 {
   // clear memory region
@@ -86,7 +86,7 @@ void interpretert::allocate(
     {
       memory_cellt &cell=memory[integer2size_t(address+i)];
       cell.value=0;
-      cell.initialized=0;
+      cell.initialized=memory_cellt::initializedt::UNKNOWN;
     }
   }
 }
@@ -96,8 +96,9 @@ void interpretert::clear_input_flags()
 {
   for(auto &cell : memory)
   {
-    if(cell.second.initialized>0)
-      cell.second.initialized=0;
+    if(cell.second.initialized==
+       memory_cellt::initializedt::WRITTEN_BEFORE_READ)
+      cell.second.initialized=memory_cellt::initializedt::UNKNOWN;
   }
 }
 
@@ -147,7 +148,7 @@ bool interpretert::count_type_leaves(const typet &ty, mp_integer &result)
 /// \return Offset into a vector of interpreter values; returns true on error
 bool interpretert::byte_offset_to_memory_offset(
   const typet &source_type,
-  mp_integer offset,
+  const mp_integer &offset,
   mp_integer &result)
 {
   if(source_type.id()==ID_struct)
@@ -227,7 +228,7 @@ bool interpretert::byte_offset_to_memory_offset(
 /// \return The corresponding byte offset. Returns true on error
 bool interpretert::memory_offset_to_byte_offset(
   const typet &source_type,
-  mp_integer cell_offset,
+  const mp_integer &full_cell_offset,
   mp_integer &result)
 {
   if(source_type.id()==ID_struct)
@@ -236,6 +237,7 @@ bool interpretert::memory_offset_to_byte_offset(
     const struct_typet::componentst &components=st.components();
     member_offset_iterator offsets(st, ns);
     mp_integer previous_member_sizes;
+    mp_integer cell_offset=full_cell_offset;
     for(; offsets->first<components.size() && offsets->second!=-1; ++offsets)
     {
       const auto &component_type=components[offsets->first].type();
@@ -277,13 +279,14 @@ bool interpretert::memory_offset_to_byte_offset(
     mp_integer elem_count;
     if(count_type_leaves(at.subtype(), elem_count))
       return true;
-    mp_integer this_idx=cell_offset/elem_count;
+    mp_integer this_idx=full_cell_offset/elem_count;
     if(this_idx>=array_size_vec[0])
       return true;
     mp_integer subtype_result;
     bool ret=
-      memory_offset_to_byte_offset(at.subtype(),
-        cell_offset%elem_count,
+      memory_offset_to_byte_offset(
+        at.subtype(),
+        full_cell_offset%elem_count,
         subtype_result);
     result=subtype_result+(elem_size*this_idx);
     return ret;
@@ -292,7 +295,7 @@ bool interpretert::memory_offset_to_byte_offset(
   {
     // Primitive type.
     result=0;
-    return cell_offset!=0;
+    return full_cell_offset!=0;
   }
 }