Central implementation of syntactic equality of instructions and goto programs

Author: tautschnig

src/goto-programs/goto_program.cpp

@@ -634,3 +634,40 @@ void goto_programt::compute_incoming_edges()
   }
 }
 
+bool goto_programt::instructiont::equal(const instructiont &other) const
+{
+  return type == other.type && code == other.code && guard == other.guard &&
+         targets.size() == other.targets.size() && labels == other.labels;
+}
+
+bool goto_programt::equal(const goto_programt &other) const
+{
+  if(instructions.size() != other.instructions.size())
+    return false;
+
+  goto_programt::const_targett other_it = other.instructions.begin();
+  for(const auto &ins : instructions)
+  {
+    if(!ins.equal(*other_it))
+      return false;
+
+    long jump_difference1 = 0;
+    if(!ins.targets.empty())
+    {
+      jump_difference1 =
+        ins.get_target()->location_number - ins.location_number;
+    }
+    long jump_difference2 = 0;
+    if(!other_it->targets.empty())
+    {
+      jump_difference2 =
+        other_it->get_target()->location_number - other_it->location_number;
+    }
+    if(jump_difference1 != jump_difference2)
+      return false;
+
+    ++other_it;
+  }
+
+  return true;
+}

src/goto-programs/goto_program.h

@@ -360,6 +360,12 @@ class goto_programt
       instruction_id_builder << type;
       return instruction_id_builder.str();
     }
+
+    /// Syntactic equality: two instructiont are equal if they have the same
+    /// type, code, guard, number of targets, and labels. All other members can
+    /// only be evaluated in the context of a goto_programt (see
+    /// goto_programt::equal).
+    bool equal(const instructiont &other) const;
   };
 
   // Never try to change this to vector-we mutate the list while iterating
@@ -611,6 +617,11 @@ class goto_programt
   typedef std::set<irep_idt> decl_identifierst;
   /// get the variables in decl statements
   void get_decl_identifiers(decl_identifierst &decl_identifiers) const;
+
+  /// Syntactic equality: two goto_programt are equal if, and only if, they have
+  /// the same number of instructions, each pair of instructions compares equal,
+  /// and relative jumps have the same distance.
+  bool equal(const goto_programt &other) const;
 };
 
 template <typename Target>