Hash-based loop identifiers

compute_loop_hashes() uses AST fingerprinting based on loop structure.
This yields loop identifiers that are stable across unrelated code
changes.

Author: tautschnig

regression/cbmc/loop-hash-nested/test.c

@@ -0,0 +1,19 @@
+// Test program with nested loops
+// Each loop should have a unique hash identifier
+
+int main()
+{
+  int sum = 0;
+
+  // Outer loop
+  for(int i = 0; i < 3; i++)
+  {
+    // Inner loop
+    for(int j = 0; j < 3; j++)
+    {
+      sum += i * j;
+    }
+  }
+
+  return sum;
+}

regression/cbmc/loop-hash-nested/test.desc

@@ -0,0 +1,8 @@
+CORE
+test.c
+--show-loops --unwind 10
+^EXIT=0$
+^SIGNAL=0$
+^main\.hash_[0-9]+$
+--
+^warning: ignoring

regression/cbmc/loop-hash-stability/test.c

@@ -0,0 +1,24 @@
+// Test program to demonstrate hash-based loop identification
+// The loop identifiers should remain stable even when we add
+// unrelated code before or after the loops.
+
+int main()
+{
+  int sum = 0;
+
+  // Loop 1: Simple for loop
+  for(int i = 0; i < 10; i++)
+  {
+    sum += i;
+  }
+
+  // Loop 2: While loop
+  int j = 0;
+  while(j < 5)
+  {
+    sum += j * 2;
+    j++;
+  }
+
+  return sum;
+}

regression/cbmc/loop-hash-stability/test.desc

@@ -0,0 +1,8 @@
+CORE
+test.c
+--show-loops --unwind 10
+^EXIT=0$
+^SIGNAL=0$
+^main\.hash_[0-9]+$
+--
+^warning: ignoring

regression/cbmc/loop-hash-stability/test_modified.c

@@ -0,0 +1,38 @@
+// Modified test program with pseudo-loops added before the real loops
+// The real loops should maintain their hash identifiers
+
+int main()
+{
+  int sum = 0;
+
+  // Add some pseudo-loops (do-while-0 pattern) that should not affect
+  // the hash values of the real loops below
+  do
+  {
+    sum += 1;
+  } while(0);
+  do
+  {
+    sum += 2;
+  } while(0);
+  do
+  {
+    sum += 3;
+  } while(0);
+
+  // Loop 1: Simple for loop (same as before)
+  for(int i = 0; i < 10; i++)
+  {
+    sum += i;
+  }
+
+  // Loop 2: While loop (same as before)
+  int j = 0;
+  while(j < 5)
+  {
+    sum += j * 2;
+    j++;
+  }
+
+  return sum;
+}

regression/cbmc/loop-hash-stability/test_modified.desc

@@ -0,0 +1,8 @@
+CORE
+test_modified.c
+--show-loops --unwind 10
+^EXIT=0$
+^SIGNAL=0$
+^main\.hash_[0-9]+$
+--
+^warning: ignoring

regression/cbmc/loop-hash-types/test.c

@@ -0,0 +1,31 @@
+// Test program with different loop types
+// Each loop should have a unique hash identifier
+
+int main()
+{
+  int sum = 0;
+
+  // For loop
+  for(int i = 0; i < 5; i++)
+  {
+    sum += i;
+  }
+
+  // While loop
+  int j = 0;
+  while(j < 5)
+  {
+    sum += j;
+    j++;
+  }
+
+  // Do-while loop
+  int k = 0;
+  do
+  {
+    sum += k;
+    k++;
+  } while(k < 5);
+
+  return sum;
+}

regression/cbmc/loop-hash-types/test.desc

@@ -0,0 +1,8 @@
+CORE
+test.c
+--show-loops --unwind 10
+^EXIT=0$
+^SIGNAL=0$
+^main\.hash_[0-9]+$
+--
+^warning: ignoring

regression/goto-programs/CMakeLists.txt

@@ -0,0 +1,3 @@
+# CMake configuration for goto-programs regression tests
+
+add_subdirectory(loop-hash-regression)

regression/goto-programs/Makefile

@@ -0,0 +1,19 @@
+# For goto-programs regression tests, see ../Makefile
+
+default: test
+
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+  exe=../../../src/goto-cc/goto-cl
+else
+  exe=../../../src/goto-cc/goto-cc
+endif
+
+test:
+	@../test.pl -p -c "../chain.sh $(exe) ../../../src/cbmc/cbmc"
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	find -name '*.gb' -execdir $(RM) '{}' \;