Fix flaky cram tests where vids leak into witnesses

tests/regression/56-witness/66-ghost-alloc-lock.t

@@ -16,136 +16,6 @@
     unsafe: 0
     total memory locations: 4
 
-  $ yamlWitnessStrip < witness.yml
-  - entry_type: ghost_instrumentation
-    content:
-      ghost_variables:
-      - name: alloc_m559918035_locked
-        scope: global
-        type: int
-        initial:
-          value: "0"
-          format: c_expression
-      - name: alloc_m861095507_locked
-        scope: global
-        type: int
-        initial:
-          value: "0"
-          format: c_expression
-      - name: multithreaded
-        scope: global
-        type: int
-        initial:
-          value: "0"
-          format: c_expression
-      ghost_updates:
-      - location:
-          file_name: 66-ghost-alloc-lock.c
-          file_hash: $FILE_HASH
-          line: 10
-          column: 3
-          function: t_fun
-        updates:
-        - variable: alloc_m559918035_locked
-          value: "1"
-          format: c_expression
-      - location:
-          file_name: 66-ghost-alloc-lock.c
-          file_hash: $FILE_HASH
-          line: 13
-          column: 3
-          function: t_fun
-        updates:
-        - variable: alloc_m559918035_locked
-          value: "0"
-          format: c_expression
-      - location:
-          file_name: 66-ghost-alloc-lock.c
-          file_hash: $FILE_HASH
-          line: 14
-          column: 3
-          function: t_fun
-        updates:
-        - variable: alloc_m861095507_locked
-          value: "1"
-          format: c_expression
-      - location:
-          file_name: 66-ghost-alloc-lock.c
-          file_hash: $FILE_HASH
-          line: 17
-          column: 3
-          function: t_fun
-        updates:
-        - variable: alloc_m861095507_locked
-          value: "0"
-          format: c_expression
-      - location:
-          file_name: 66-ghost-alloc-lock.c
-          file_hash: $FILE_HASH
-          line: 28
-          column: 3
-          function: main
-        updates:
-        - variable: multithreaded
-          value: "1"
-          format: c_expression
-      - location:
-          file_name: 66-ghost-alloc-lock.c
-          file_hash: $FILE_HASH
-          line: 30
-          column: 3
-          function: main
-        updates:
-        - variable: alloc_m559918035_locked
-          value: "1"
-          format: c_expression
-      - location:
-          file_name: 66-ghost-alloc-lock.c
-          file_hash: $FILE_HASH
-          line: 32
-          column: 3
-          function: main
-        updates:
-        - variable: alloc_m559918035_locked
-          value: "0"
-          format: c_expression
-      - location:
-          file_name: 66-ghost-alloc-lock.c
-          file_hash: $FILE_HASH
-          line: 33
-          column: 3
-          function: main
-        updates:
-        - variable: alloc_m861095507_locked
-          value: "1"
-          format: c_expression
-      - location:
-          file_name: 66-ghost-alloc-lock.c
-          file_hash: $FILE_HASH
-          line: 35
-          column: 3
-          function: main
-        updates:
-        - variable: alloc_m861095507_locked
-          value: "0"
-          format: c_expression
-  - entry_type: flow_insensitive_invariant
-    flow_insensitive_invariant:
-      string: '! multithreaded || (alloc_m861095507_locked || g2 == 0)'
-      type: assertion
-      format: C
-  - entry_type: flow_insensitive_invariant
-    flow_insensitive_invariant:
-      string: '! multithreaded || (alloc_m559918035_locked || g1 == 0)'
-      type: assertion
-      format: C
-  - entry_type: flow_insensitive_invariant
-    flow_insensitive_invariant:
-      string: '! multithreaded || (0 <= g2 && g2 <= 1)'
-      type: assertion
-      format: C
-  - entry_type: flow_insensitive_invariant
-    flow_insensitive_invariant:
-      string: '! multithreaded || (0 <= g1 && g1 <= 1)'
-      type: assertion
-      format: C
+  $ (yamlWitnessStrip < witness.yml) > new-stripped.yml
+  $ ./compare-ghost-alloc.sh 66-ghost-alloc-stripped.yml new-stripped.yml
+  The files are the same after renaming the variables.

tests/regression/56-witness/66-ghost-alloc-stripped.yml

@@ -0,0 +1,132 @@
+- entry_type: ghost_instrumentation
+  content:
+    ghost_variables:
+    - name: alloc_m559918035_locked
+      scope: global
+      type: int
+      initial:
+        value: "0"
+        format: c_expression
+    - name: alloc_m861095507_locked
+      scope: global
+      type: int
+      initial:
+        value: "0"
+        format: c_expression
+    - name: multithreaded
+      scope: global
+      type: int
+      initial:
+        value: "0"
+        format: c_expression
+    ghost_updates:
+    - location:
+        file_name: 66-ghost-alloc-lock.c
+        file_hash: $FILE_HASH
+        line: 10
+        column: 3
+        function: t_fun
+      updates:
+      - variable: alloc_m559918035_locked
+        value: "1"
+        format: c_expression
+    - location:
+        file_name: 66-ghost-alloc-lock.c
+        file_hash: $FILE_HASH
+        line: 13
+        column: 3
+        function: t_fun
+      updates:
+      - variable: alloc_m559918035_locked
+        value: "0"
+        format: c_expression
+    - location:
+        file_name: 66-ghost-alloc-lock.c
+        file_hash: $FILE_HASH
+        line: 14
+        column: 3
+        function: t_fun
+      updates:
+      - variable: alloc_m861095507_locked
+        value: "1"
+        format: c_expression
+    - location:
+        file_name: 66-ghost-alloc-lock.c
+        file_hash: $FILE_HASH
+        line: 17
+        column: 3
+        function: t_fun
+      updates:
+      - variable: alloc_m861095507_locked
+        value: "0"
+        format: c_expression
+    - location:
+        file_name: 66-ghost-alloc-lock.c
+        file_hash: $FILE_HASH
+        line: 28
+        column: 3
+        function: main
+      updates:
+      - variable: multithreaded
+        value: "1"
+        format: c_expression
+    - location:
+        file_name: 66-ghost-alloc-lock.c
+        file_hash: $FILE_HASH
+        line: 30
+        column: 3
+        function: main
+      updates:
+      - variable: alloc_m559918035_locked
+        value: "1"
+        format: c_expression
+    - location:
+        file_name: 66-ghost-alloc-lock.c
+        file_hash: $FILE_HASH
+        line: 32
+        column: 3
+        function: main
+      updates:
+      - variable: alloc_m559918035_locked
+        value: "0"
+        format: c_expression
+    - location:
+        file_name: 66-ghost-alloc-lock.c
+        file_hash: $FILE_HASH
+        line: 33
+        column: 3
+        function: main
+      updates:
+      - variable: alloc_m861095507_locked
+        value: "1"
+        format: c_expression
+    - location:
+        file_name: 66-ghost-alloc-lock.c
+        file_hash: $FILE_HASH
+        line: 35
+        column: 3
+        function: main
+      updates:
+      - variable: alloc_m861095507_locked
+        value: "0"
+        format: c_expression
+- entry_type: flow_insensitive_invariant
+  flow_insensitive_invariant:
+    string: '! multithreaded || (alloc_m861095507_locked || g2 == 0)'
+    type: assertion
+    format: C
+- entry_type: flow_insensitive_invariant
+  flow_insensitive_invariant:
+    string: '! multithreaded || (alloc_m559918035_locked || g1 == 0)'
+    type: assertion
+    format: C
+- entry_type: flow_insensitive_invariant
+  flow_insensitive_invariant:
+    string: '! multithreaded || (0 <= g2 && g2 <= 1)'
+    type: assertion
+    format: C
+- entry_type: flow_insensitive_invariant
+  flow_insensitive_invariant:
+    string: '! multithreaded || (0 <= g1 && g1 <= 1)'
+    type: assertion
+    format: C

tests/regression/56-witness/compare-ghost-alloc.sh

@@ -0,0 +1,45 @@
+#!/bin/bash
+
+# Check if the correct number of arguments are provided
+if [ "$#" -ne 2 ]; then
+    echo "Usage: $0 <file1> <file2>"
+    exit 1
+fi
+
+file1="$1"
+file2="$2"
+
+# Function to extract the first and second occurrences of the pattern
+extract_variables() {
+    grep -o -m 2 'alloc_m[0-9]\+_locked' "$1"
+}
+
+# Extract variables from both files
+var1_file1=$(extract_variables "$file1" | sed -n '1p')
+var2_file1=$(extract_variables "$file1" | sed -n '2p')
+var1_file2=$(extract_variables "$file2" | sed -n '1p')
+var2_file2=$(extract_variables "$file2" | sed -n '2p')
+
+# Check if the variables were found
+if [ -z "$var1_file1" ] || [ -z "$var2_file1" ] || [ -z "$var1_file2" ] || [ -z "$var2_file2" ]; then
+    echo "Error: Could not find the required pattern in one or both files."
+    exit 1
+fi
+
+# Create temporary files
+temp1=$(mktemp)
+temp2=$(mktemp)
+
+# Rename variables in both files
+sed -e "s/\b$var1_file1\b/TEMP_VAR1/g" -e "s/\b$var2_file1\b/TEMP_VAR2/g" "$file1" > "$temp1"
+sed -e "s/\b$var1_file2\b/TEMP_VAR1/g" -e "s/\b$var2_file2\b/TEMP_VAR2/g" "$file2" > "$temp2"
+
+# Compare the modified files
+if diff -q "$temp1" "$temp2" > /dev/null; then
+    echo "The files are the same after renaming the variables."
+else
+    echo "The files are different after renaming the variables."
+fi
+
+# Clean up temporary files
+rm "$temp1" "$temp2"

tests/regression/56-witness/dune

@@ -25,7 +25,7 @@
      (run %{update_suite} apron-unassume-set-tokens -q)))))
 
 (cram
- (deps (glob_files *.c) (glob_files ??-*.yml)))
+ (deps (glob_files *.c) (glob_files ??-*.yml) (glob_files compare-ghost-alloc.sh)))
 
 (cram
  (applies_to 54-witness-lifter-abortUnless)