Merge pull request #1703 from goblint/issue_1647

Fix flaky cram tests where `vid`s leak into witnesses
goblint · Mar 5, 2025 · 50e8ab9 · 50e8ab9
2 parents b90ee73 + fcdcf13
commit 50e8ab9
Show file tree

Hide file tree

Showing 3 changed files with 42 additions and 14 deletions.
diff --git a/tests/regression/56-witness/66-ghost-alloc-lock.t b/tests/regression/56-witness/66-ghost-alloc-lock.t
@@ -16,17 +16,18 @@
     unsafe: 0
     total memory locations: 4
 
-  $ yamlWitnessStrip < witness.yml
+  $ (yamlWitnessStrip < witness.yml) > new-stripped.yml
+  $ ./strip-ghost-alloc.sh new-stripped.yml
   - entry_type: ghost_instrumentation
     content:
       ghost_variables:
-      - name: alloc_m559918035_locked
+      - name: ALLOC_VAR1_LOCKED
         scope: global
         type: int
         initial:
           value: "0"
           format: c_expression
-      - name: alloc_m861095507_locked
+      - name: ALLOC_VAR2_LOCKED
         scope: global
         type: int
         initial:
@@ -46,7 +47,7 @@
           column: 3
           function: t_fun
         updates:
-        - variable: alloc_m559918035_locked
+        - variable: ALLOC_VAR1_LOCKED
           value: "1"
           format: c_expression
       - location:
@@ -56,7 +57,7 @@
           column: 3
           function: t_fun
         updates:
-        - variable: alloc_m559918035_locked
+        - variable: ALLOC_VAR1_LOCKED
           value: "0"
           format: c_expression
       - location:
@@ -66,7 +67,7 @@
           column: 3
           function: t_fun
         updates:
-        - variable: alloc_m861095507_locked
+        - variable: ALLOC_VAR2_LOCKED
           value: "1"
           format: c_expression
       - location:
@@ -76,7 +77,7 @@
           column: 3
           function: t_fun
         updates:
-        - variable: alloc_m861095507_locked
+        - variable: ALLOC_VAR2_LOCKED
           value: "0"
           format: c_expression
       - location:
@@ -96,7 +97,7 @@
           column: 3
           function: main
         updates:
-        - variable: alloc_m559918035_locked
+        - variable: ALLOC_VAR1_LOCKED
           value: "1"
           format: c_expression
       - location:
@@ -106,7 +107,7 @@
           column: 3
           function: main
         updates:
-        - variable: alloc_m559918035_locked
+        - variable: ALLOC_VAR1_LOCKED
           value: "0"
           format: c_expression
       - location:
@@ -116,7 +117,7 @@
           column: 3
           function: main
         updates:
-        - variable: alloc_m861095507_locked
+        - variable: ALLOC_VAR2_LOCKED
           value: "1"
           format: c_expression
       - location:
@@ -126,17 +127,17 @@
           column: 3
           function: main
         updates:
-        - variable: alloc_m861095507_locked
+        - variable: ALLOC_VAR2_LOCKED
           value: "0"
           format: c_expression
   - entry_type: flow_insensitive_invariant
     flow_insensitive_invariant:
-      string: '! multithreaded || (alloc_m861095507_locked || g2 == 0)'
+      string: '! multithreaded || (ALLOC_VAR2_LOCKED || g2 == 0)'
       type: assertion
       format: C
   - entry_type: flow_insensitive_invariant
     flow_insensitive_invariant:
-      string: '! multithreaded || (alloc_m559918035_locked || g1 == 0)'
+      string: '! multithreaded || (ALLOC_VAR1_LOCKED || g1 == 0)'
       type: assertion
       format: C
   - entry_type: flow_insensitive_invariant

diff --git a/tests/regression/56-witness/dune b/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 strip-ghost-alloc.sh)))
 
 (cram
  (applies_to 54-witness-lifter-abortUnless)

diff --git a/tests/regression/56-witness/strip-ghost-alloc.sh b/tests/regression/56-witness/strip-ghost-alloc.sh
@@ -0,0 +1,27 @@
+#!/bin/bash
+
+# Check if the correct number of arguments are provided
+if [ "$#" -ne 1 ]; then
+    echo "Usage: $0 <file>"
+    exit 1
+fi
+
+file="$1"
+
+# 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 the file
+var1=$(extract_variables "$file" | sed -n '1p')
+var2=$(extract_variables "$file" | sed -n '2p')
+
+# Check if both variables were found
+if [ -z "$var1" ] || [ -z "$var2" ]; then
+    echo "Error: Could not find two occurrences of the pattern 'alloc_m[0-9]+_locked' in the file."
+    exit 1
+fi
+
+# Rename variables and print the modified file to stdout
+sed -e "s/$var1/ALLOC_VAR1_LOCKED/g" -e "s/$var2/ALLOC_VAR2_LOCKED/g" "$file"