Merge pull request #2718 from tautschnig/syntactic-eq

Central implementation of syntactic equality of instructions and goto programs

Author: tautschnig

jbmc/src/jdiff/java_syntactic_diff.cpp

@@ -70,9 +70,7 @@ bool java_syntactic_difft::operator()()
       continue;
     }
 
-    if(
-      it->second.body.instructions.size() !=
-      f_it->second.body.instructions.size())
+    if(!it->second.body.equals(f_it->second.body))
     {
       modified_functions.insert(it->first);
       continue;
@@ -86,22 +84,7 @@ bool java_syntactic_difft::operator()()
         i_it2 != f_it->second.body.instructions.end();
         ++i_it1, ++i_it2)
     {
-      long jump_difference1 = 0;
-      if(!i_it1->targets.empty())
-      {
-        jump_difference1 =
-          i_it1->get_target()->location_number - i_it1->location_number;
-      }
-      long jump_difference2 = 0;
-      if(!i_it2->targets.empty())
-      {
-        jump_difference2 =
-          i_it2->get_target()->location_number - i_it2->location_number;
-      }
-      if(
-        i_it1->code != i_it2->code || i_it1->function != i_it2->function ||
-        i_it1->type != i_it2->type || i_it1->guard != i_it2->guard ||
-        jump_difference1 != jump_difference2)
+      if(i_it1->function != i_it2->function)
       {
         modified_functions.insert(it->first);
         break;

src/goto-diff/syntactic_diff.cpp

@@ -69,8 +69,7 @@ bool syntactic_difft::operator()()
       continue;
     }
 
-    if(it->second.body.instructions.size() !=
-       f_it->second.body.instructions.size())
+    if(!it->second.body.equals(f_it->second.body))
     {
       modified_functions.insert(it->first);
       continue;
@@ -84,22 +83,7 @@ bool syntactic_difft::operator()()
         i_it2!=f_it->second.body.instructions.end();
         ++i_it1, ++i_it2)
     {
-      long jump_difference1 = 0;
-      if(!i_it1->targets.empty())
-      {
-        jump_difference1 =
-          i_it1->get_target()->location_number - i_it1->location_number;
-      }
-      long jump_difference2 = 0;
-      if(!i_it2->targets.empty())
-      {
-        jump_difference2 =
-          i_it2->get_target()->location_number - i_it2->location_number;
-      }
-      if(
-        i_it1->code != i_it2->code || i_it1->function != i_it2->function ||
-        i_it1->type != i_it2->type || i_it1->guard != i_it2->guard ||
-        jump_difference1 != jump_difference2)
+      if(i_it1->function != i_it2->function)
       {
         modified_functions.insert(it->first);
         break;

src/goto-diff/unified_diff.cpp

@@ -392,9 +392,7 @@ bool unified_difft::instructions_equal(
   const goto_programt::instructiont &ins1,
   const goto_programt::instructiont &ins2)
 {
-  return ins1.code == ins2.code && ins1.function == ins2.function &&
-         ins1.type == ins2.type && ins1.guard == ins2.guard &&
-         ins1.targets.size() == ins2.targets.size() &&
+  return ins1.equals(ins2) && ins1.function == ins2.function &&
          (ins1.targets.empty() ||
           instructions_equal(*ins1.get_target(), *ins2.get_target()));
 }

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

@@ -389,6 +389,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
@@ -640,6 +646,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>