Hash-based loop identifiers

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) '{}' \;

regression/goto-programs/chain.sh

@@ -0,0 +1,7 @@
+#!/usr/bin/env bash
+set -e
+goto_cc=$1
+cbmc=$2
+is_windows=$3
+shift 3
+exec "$@"

regression/goto-programs/loop-hash-nested-01/chain.sh

@@ -0,0 +1,17 @@
+#!/usr/bin/env bash
+
+set -e
+
+goto_cc=$1
+cbmc=$2
+is_windows=$3
+
+name="main"
+
+if [[ "${is_windows}" == "true" ]]; then
+  ${goto_cc} ${name}.c "/Fe${name}.gb"
+else
+  ${goto_cc} ${name}.c -o ${name}.gb
+fi
+
+${cbmc} --show-loops ${name}.gb | grep -E "Loop [0-9]+ hash:" | sed 's/.*hash: //' | sort -n

regression/goto-programs/loop-hash-nested-01/main.c

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

regression/goto-programs/loop-hash-nested-01/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--chain chain.sh
+^EXIT=0$
+^SIGNAL=0$
+^[0-9]+$
+^[0-9]+$

regression/goto-programs/loop-hash-sensitivity-01/chain.sh

@@ -0,0 +1,17 @@
+#!/usr/bin/env bash
+
+set -e
+
+goto_cc=$1
+cbmc=$2
+is_windows=$3
+
+name="main"
+
+if [[ "${is_windows}" == "true" ]]; then
+  ${goto_cc} ${name}.c "/Fe${name}.gb"
+else
+  ${goto_cc} ${name}.c -o ${name}.gb
+fi
+
+${cbmc} --show-loops ${name}.gb | grep -E "Loop [0-9]+ hash:" | sed 's/.*hash: //' | sort -n

regression/goto-programs/loop-hash-sensitivity-01/main.c

@@ -0,0 +1,24 @@
+// Test case: Loops with CHANGED CONDITIONS
+// These loops should have DIFFERENT hashes compared to test_location_stability.c
+// because the loop conditions are different
+
+int main()
+{
+  int sum = 0;
+
+  // Test loop 1: Changed upper bound from 10 to 20
+  for(int i = 0; i < 20; i++)
+  { // Changed: was i < 10
+    sum += i;
+  }
+
+  // Test loop 2: Changed condition operator
+  int j = 0;
+  while(j <= 5)
+  { // Changed: was j < 5
+    sum += j;
+    j++;
+  }
+
+  return sum;
+}

regression/goto-programs/loop-hash-sensitivity-01/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--chain chain.sh
+^EXIT=0$
+^SIGNAL=0$
+^[0-9]+$
+^[0-9]+$

regression/goto-programs/loop-hash-stability-01/chain.sh

@@ -0,0 +1,18 @@
+#!/usr/bin/env bash
+
+set -e
+
+goto_cc=$1
+cbmc=$2
+is_windows=$3
+
+name="main"
+
+if [[ "${is_windows}" == "true" ]]; then
+  ${goto_cc} ${name}.c "/Fe${name}.gb"
+else
+  ${goto_cc} ${name}.c -o ${name}.gb
+fi
+
+# Show loops and extract hash values
+${cbmc} --show-loops ${name}.gb | grep -E "Loop [0-9]+ hash:" | sed 's/.*hash: //' | sort -n

regression/goto-programs/loop-hash-stability-01/main.c

@@ -0,0 +1,31 @@
+// Test program with simple loops for hash stability verification
+// The loop hashes should remain stable across multiple runs
+
+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++;
+  }
+
+  // Loop 3: Do-while loop
+  int k = 0;
+  do
+  {
+    sum += k;
+    k++;
+  } while(k < 3);
+
+  return sum;
+}

regression/goto-programs/loop-hash-stability-01/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--chain chain.sh
+^EXIT=0$
+^SIGNAL=0$
+^[0-9]+$
+^[0-9]+$
+^[0-9]+$

regression/goto-programs/loop-hash-stability-02/chain.sh

@@ -0,0 +1,30 @@
+#!/usr/bin/env bash
+
+set -e
+
+goto_cc=$1
+cbmc=$2
+is_windows=$3
+
+if [[ "${is_windows}" == "true" ]]; then
+  ${goto_cc} original.c "/Feoriginal.gb"
+  ${goto_cc} shifted.c "/Feshifted.gb"
+else
+  ${goto_cc} original.c -o original.gb
+  ${goto_cc} shifted.c -o shifted.gb
+fi
+
+# Extract hashes from both versions
+hash1=$(${cbmc} --show-loops original.gb | grep -E "Loop [0-9]+ hash:" | sed 's/.*hash: //' | sort -n)
+hash2=$(${cbmc} --show-loops shifted.gb | grep -E "Loop [0-9]+ hash:" | sed 's/.*hash: //' | sort -n)
+
+# Compare - should be identical
+if [ "$hash1" == "$hash2" ]; then
+  echo "STABLE: Hashes match"
+  echo "$hash1"
+else
+  echo "UNSTABLE: Hashes differ"
+  echo "Original: $hash1"
+  echo "Shifted: $hash2"
+  exit 1
+fi