Central implementation of syntactic equality of instructions and goto programs

Author: tautschnig

src/goto-programs/goto_program.cpp

@@ -634,3 +634,45 @@ void goto_programt::compute_incoming_edges()
   }
 }
 
+bool goto_programt::instructiont::equals(const instructiont &other) const
+{
+  // clang-format off
+  return
+    type == other.type &&
+    code == other.code &&
+    guard == other.guard &&
+    targets.size() == other.targets.size() &&
+    labels == other.labels;
+  // clang-format on
+}
+
+bool goto_programt::equals(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.equals(*other_it))
+      return false;
+
+    // the number of targets is the same as instructiont::equals returned "true"
+    auto other_target_it = other_it->targets.begin();
+    for(const auto t : ins.targets)
+    {
+      if(
+        t->location_number - ins.location_number !=
+        (*other_target_it)->location_number - other_it->location_number)
+      {
+        return false;
+      }
+
+      ++other_target_it;
+    }
+
+    ++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::equals).
+    bool equals(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 equals(const goto_programt &other) const;
 };
 
 template <typename Target>