Make invariant_set and ghost_instrumentation deterministic in tests

goblint · Aug 20, 2024 · 431b34d · 431b34d
1 parent e9e652d
commit 431b34d
Show file tree

Hide file tree

Showing 2 changed files with 29 additions and 23 deletions.
diff --git a/tests/regression/13-privatized/74-mutex.t b/tests/regression/13-privatized/74-mutex.t
@@ -170,33 +170,33 @@ Same with ghost_instrumentation and invariant_set entries.
   $ yamlWitnessStrip < witness.yml
   - entry_type: ghost_instrumentation
     ghost_variables:
-    - name: multithreaded
+    - name: m_locked
       scope: global
       type: int
       initial: "0"
-    - name: m_locked
+    - name: multithreaded
       scope: global
       type: int
       initial: "0"
     ghost_updates:
     - location:
         file_name: 74-mutex.c
         file_hash: $FILE_HASH
-        line: 38
-        column: 3
-        function: main
+        line: 20
+        column: 5
+        function: producer
       updates:
       - ghost_variable: m_locked
-        expression: "0"
+        expression: "1"
     - location:
         file_name: 74-mutex.c
         file_hash: $FILE_HASH
-        line: 36
-        column: 3
-        function: main
+        line: 23
+        column: 5
+        function: producer
       updates:
       - ghost_variable: m_locked
-        expression: "1"
+        expression: "0"
     - location:
         file_name: 74-mutex.c
         file_hash: $FILE_HASH
@@ -209,21 +209,21 @@ Same with ghost_instrumentation and invariant_set entries.
     - location:
         file_name: 74-mutex.c
         file_hash: $FILE_HASH
-        line: 23
-        column: 5
-        function: producer
+        line: 36
+        column: 3
+        function: main
       updates:
       - ghost_variable: m_locked
-        expression: "0"
+        expression: "1"
     - location:
         file_name: 74-mutex.c
         file_hash: $FILE_HASH
-        line: 20
-        column: 5
-        function: producer
+        line: 38
+        column: 3
+        function: main
       updates:
       - ghost_variable: m_locked
-        expression: "1"
+        expression: "0"
   - entry_type: invariant_set
     content:
     - invariant:
@@ -234,7 +234,7 @@ Same with ghost_instrumentation and invariant_set entries.
           line: 36
           column: 3
           function: main
-        value: '! multithreaded || (m_locked || used == 0)'
+        value: '! multithreaded || (0 <= used && used <= 1)'
         format: c_expression
     - invariant:
         type: location_invariant
@@ -244,7 +244,7 @@ Same with ghost_instrumentation and invariant_set entries.
           line: 36
           column: 3
           function: main
-        value: '! multithreaded || (0 <= used && used <= 1)'
+        value: '! multithreaded || (m_locked || used == 0)'
         format: c_expression
 
 Same with mutex-meet.

diff --git a/tests/util/yamlWitnessStrip.ml b/tests/util/yamlWitnessStrip.ml
@@ -27,7 +27,10 @@ struct
       {invariant_type}
     in
     let ghost_location_update_strip_file_hash (x: GhostInstrumentation.LocationUpdate.t): GhostInstrumentation.LocationUpdate.t =
-      {x with location = location_strip_file_hash x.location}
+      {
+        location = location_strip_file_hash x.location;
+        updates = List.sort GhostInstrumentation.Update.compare x.updates
+      }
     in
     let entry_type: EntryType.t =
       match entry_type with
@@ -44,13 +47,16 @@ struct
       | PreconditionLoopInvariantCertificate x ->
         PreconditionLoopInvariantCertificate {x with target = target_strip_file_hash x.target}
       | InvariantSet x ->
-        InvariantSet {content = List.map invariant_strip_file_hash x.content}
+        InvariantSet {content = List.sort InvariantSet.Invariant.compare (List.map invariant_strip_file_hash x.content)} (* Sort, so order is deterministic regardless of Goblint. *)
       | GhostVariable x ->
         GhostVariable x (* no location to strip *)
       | GhostUpdate x ->
         GhostUpdate {x with location = location_strip_file_hash x.location}
       | GhostInstrumentation x ->
-        GhostInstrumentation {x with ghost_updates = List.map ghost_location_update_strip_file_hash x.ghost_updates}
+        GhostInstrumentation { (* Sort, so order is deterministic regardless of Goblint. *)
+          ghost_variables = List.sort GhostInstrumentation.Variable.compare x.ghost_variables;
+          ghost_updates = List.sort GhostInstrumentation.LocationUpdate.compare (List.map ghost_location_update_strip_file_hash x.ghost_updates);
+        }
     in
     {entry_type}