Merge pull request #1656 from goblint/traces-vojdani-invariant

Fix Vojdani privatization `invariant_global`

src/analyses/basePriv.ml

@@ -829,8 +829,30 @@ struct
       vf g;
     | _ -> ()
 
-  let invariant_global ask getg g =
-    ValueDomain.invariant_global getg g
+  let invariant_global (ask: Q.ask) getg g =
+    let locks = ask.f (Q.MustProtectingLocks {global = g; write = false}) in
+    if LockDomain.MustLockset.is_all locks then
+      Invariant.none
+    else (
+      (* Only read g as protected, everything else (e.g. pointed to variables) may be unprotected.
+         See 56-witness/69-ghost-ptr-protection and https://github.com/goblint/analyzer/pull/1394#discussion_r1698136411. *)
+      let read_global g' = if CilType.Varinfo.equal g' g then getg g' else VD.top () in (* TODO: Could be more precise for at least those which might not have all same protecting locks? *)
+      let inv = ValueDomain.invariant_global read_global g in
+      (* Very conservative about multiple protecting mutexes: invariant is not claimed when any of them is held.
+         It should be possible to be more precise because writes only happen with all of them held,
+         but conjunction is unsound when one of the mutexes is temporarily unlocked.
+         Hypothetical read-protection is also somehow relevant. *)
+      LockDomain.MustLockset.fold (fun m acc ->
+          if LockDomain.MustLock.equal m (LockDomain.MustLock.of_var LibraryFunctions.verifier_atomic_var) then
+            acc
+          else if ask.f (GhostVarAvailable (Locked m)) then (
+            let var = WitnessGhost.to_varinfo (Locked m) in
+            Invariant.(of_exp (Lval (GoblintCil.var var)) || acc) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
+          )
+          else
+            Invariant.none
+        ) locks inv
+    )
 
   let invariant_vars ask getg st = protected_vars ask
 end
@@ -1010,7 +1032,7 @@ struct
     | `Left g' -> (* unprotected *)
       ValueDomain.invariant_global (fun g -> getg (V.unprotected g)) g'
     | `Right g' -> (* protected *)
-      let locks = ask.f (Q.MustProtectingLocks g') in
+      let locks = ask.f (Q.MustProtectingLocks {global = g'; write = true}) in
       if LockDomain.MustLockset.is_all locks || LockDomain.MustLockset.is_empty locks then
         Invariant.none
       else if VD.equal (getg (V.protected g')) (getg (V.unprotected g')) then

src/analyses/mutexAnalysis.ml

@@ -226,8 +226,8 @@ struct
         true
       else *)
       MustLockset.mem ml protecting
-    | Queries.MustProtectingLocks g ->
-      protecting ~write:true Strong g
+    | Queries.MustProtectingLocks {global; write} ->
+      protecting ~write Strong global
     | Queries.MustLockset ->
       let held_locks = MustLocksetRW.to_must_lockset (MustLocksetRW.filter snd ls) in
       held_locks

src/domains/queries.ml

@@ -53,6 +53,7 @@ type maybepublic = {global: CilType.Varinfo.t; write: bool; protection: Protecti
 type maybepublicwithout = {global: CilType.Varinfo.t; write: bool; without_mutex: LockDomain.MustLock.t; protection: Protection.t} [@@deriving ord, hash]
 type mustbeprotectedby = {mutex: LockDomain.MustLock.t; global: CilType.Varinfo.t; write: bool; protection: Protection.t} [@@deriving ord, hash]
 type mustprotectedvars = {mutex: LockDomain.MustLock.t; write: bool} [@@deriving ord, hash]
+type mustprotectinglocks = {global: CilType.Varinfo.t; write: bool} [@@deriving ord, hash]
 type access =
   | Memory of {exp: CilType.Exp.t; var_opt: CilType.Varinfo.t option; kind: AccessKind.t} (** Memory location access (race). *)
   | Point (** Program point and state access (MHP), independent of memory location. *)
@@ -117,7 +118,7 @@ type _ t =
   | MustJoinedThreads: ConcDomain.MustThreadSet.t t
   | ThreadsJoinedCleanly: MustBool.t t
   | MustProtectedVars: mustprotectedvars -> VS.t t
-  | MustProtectingLocks: CilType.Varinfo.t -> LockDomain.MustLockset.t t
+  | MustProtectingLocks: mustprotectinglocks -> LockDomain.MustLockset.t t
   | Invariant: invariant_context -> Invariant.t t
   | InvariantGlobal: Obj.t -> Invariant.t t (** Argument must be of corresponding [Spec.V.t]. *)
   | WarnGlobal: Obj.t -> Unit.t t (** Argument must be of corresponding [Spec.V.t]. *)
@@ -405,7 +406,7 @@ struct
       | Any (IterSysVars (vq1, vf1)), Any (IterSysVars (vq2, vf2)) -> VarQuery.compare vq1 vq2 (* not comparing fs *)
       | Any (MutexType m1), Any (MutexType m2) -> Mval.Unit.compare m1 m2
       | Any (MustProtectedVars m1), Any (MustProtectedVars m2) -> compare_mustprotectedvars m1 m2
-      | Any (MustProtectingLocks g1), Any (MustProtectingLocks g2) -> CilType.Varinfo.compare g1 g2
+      | Any (MustProtectingLocks g1), Any (MustProtectingLocks g2) -> compare_mustprotectinglocks g1 g2
       | Any (MayBeModifiedSinceSetjmp e1), Any (MayBeModifiedSinceSetjmp e2) -> JmpBufDomain.BufferEntry.compare e1 e2
       | Any (MustBeSingleThreaded {since_start=s1;}),  Any (MustBeSingleThreaded {since_start=s2;}) -> Stdlib.compare s1 s2
       | Any (TmpSpecial lv1), Any (TmpSpecial lv2) -> Mval.Exp.compare lv1 lv2
@@ -451,7 +452,7 @@ struct
     | Any (InvariantGlobal vi) -> Hashtbl.hash vi
     | Any (YamlEntryGlobal (vi, task)) -> Hashtbl.hash vi (* TODO: hash task *)
     | Any (MustProtectedVars m) -> hash_mustprotectedvars m
-    | Any (MustProtectingLocks g) -> CilType.Varinfo.hash g
+    | Any (MustProtectingLocks g) -> hash_mustprotectinglocks g
     | Any (MayBeModifiedSinceSetjmp e) -> JmpBufDomain.BufferEntry.hash e
     | Any (MustBeSingleThreaded {since_start}) -> Hashtbl.hash since_start
     | Any (TmpSpecial lv) -> Mval.Exp.hash lv

tests/regression/13-privatized/74-mutex.t

@@ -277,7 +277,102 @@ Same with ghost_instrumentation and invariant_set entries.
         value: '! multithreaded || (m_locked || used == 0)'
         format: c_expression
 
-Same with mutex-meet.
+Same protected invariant with vojdani but no unprotected invariant.
+
+  $ goblint --enable ana.sv-comp.functions --set ana.base.privatization vojdani --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types '["flow_insensitive_invariant", "ghost_instrumentation"]' 74-mutex.c
+  [Success][Assert] Assertion "used == 0" will succeed (74-mutex.c:37:3-37:29)
+  [Warning][Deadcode] Function 'producer' has dead code:
+    on line 26 (74-mutex.c:26-26)
+  [Warning][Deadcode] Logical lines of code (LLoC) summary:
+    live: 14
+    dead: 1
+    total lines: 15
+  [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (74-mutex.c:19:10-19:11)
+  [Info][Witness] witness generation summary:
+    location invariants: 0
+    loop invariants: 0
+    flow-insensitive invariants: 1
+    total generation entries: 2
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: ghost_instrumentation
+    content:
+      ghost_variables:
+      - name: m_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: 74-mutex.c
+          file_hash: $FILE_HASH
+          line: 20
+          column: 5
+          function: producer
+        updates:
+        - variable: m_locked
+          value: "1"
+          format: c_expression
+      - location:
+          file_name: 74-mutex.c
+          file_hash: $FILE_HASH
+          line: 23
+          column: 5
+          function: producer
+        updates:
+        - variable: m_locked
+          value: "0"
+          format: c_expression
+      - location:
+          file_name: 74-mutex.c
+          file_hash: $FILE_HASH
+          line: 34
+          column: 3
+          function: main
+        updates:
+        - variable: multithreaded
+          value: "1"
+          format: c_expression
+      - location:
+          file_name: 74-mutex.c
+          file_hash: $FILE_HASH
+          line: 36
+          column: 3
+          function: main
+        updates:
+        - variable: m_locked
+          value: "1"
+          format: c_expression
+      - location:
+          file_name: 74-mutex.c
+          file_hash: $FILE_HASH
+          line: 38
+          column: 3
+          function: main
+        updates:
+        - variable: m_locked
+          value: "0"
+          format: c_expression
+  - entry_type: flow_insensitive_invariant
+    flow_insensitive_invariant:
+      string: '! multithreaded || (m_locked || used == 0)'
+      type: assertion
+      format: C
+
+Same as protection with mutex-meet.
 
   $ goblint --enable ana.sv-comp.functions --set ana.base.privatization mutex-meet --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types '["flow_insensitive_invariant", "ghost_instrumentation"]' 74-mutex.c
   [Success][Assert] Assertion "used == 0" will succeed (74-mutex.c:37:3-37:29)

tests/regression/56-witness/64-ghost-multiple-protecting.t

@@ -337,6 +337,168 @@ protection-read has precise protected invariant for g2.
       type: assertion
       format: C
 
+  $ goblint --set ana.base.privatization vojdani --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types '["flow_insensitive_invariant", "ghost_instrumentation"]' 64-ghost-multiple-protecting.c
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 19
+    dead: 0
+    total lines: 19
+  [Info][Witness] witness generation summary:
+    location invariants: 0
+    loop invariants: 0
+    flow-insensitive invariants: 2
+    total generation entries: 3
+  [Info][Race] Memory locations race summary:
+    safe: 2
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 2
+
+vojdani has precise protected invariant for g2, but no unprotected invariants.
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: ghost_instrumentation
+    content:
+      ghost_variables:
+      - name: m1_locked
+        scope: global
+        type: int
+        initial:
+          value: "0"
+          format: c_expression
+      - name: m2_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: 64-ghost-multiple-protecting.c
+          file_hash: $FILE_HASH
+          line: 9
+          column: 3
+          function: t_fun
+        updates:
+        - variable: m1_locked
+          value: "1"
+          format: c_expression
+      - location:
+          file_name: 64-ghost-multiple-protecting.c
+          file_hash: $FILE_HASH
+          line: 10
+          column: 3
+          function: t_fun
+        updates:
+        - variable: m2_locked
+          value: "1"
+          format: c_expression
+      - location:
+          file_name: 64-ghost-multiple-protecting.c
+          file_hash: $FILE_HASH
+          line: 13
+          column: 3
+          function: t_fun
+        updates:
+        - variable: m2_locked
+          value: "0"
+          format: c_expression
+      - location:
+          file_name: 64-ghost-multiple-protecting.c
+          file_hash: $FILE_HASH
+          line: 14
+          column: 3
+          function: t_fun
+        updates:
+        - variable: m1_locked
+          value: "0"
+          format: c_expression
+      - location:
+          file_name: 64-ghost-multiple-protecting.c
+          file_hash: $FILE_HASH
+          line: 16
+          column: 3
+          function: t_fun
+        updates:
+        - variable: m1_locked
+          value: "1"
+          format: c_expression
+      - location:
+          file_name: 64-ghost-multiple-protecting.c
+          file_hash: $FILE_HASH
+          line: 17
+          column: 3
+          function: t_fun
+        updates:
+        - variable: m2_locked
+          value: "1"
+          format: c_expression
+      - location:
+          file_name: 64-ghost-multiple-protecting.c
+          file_hash: $FILE_HASH
+          line: 19
+          column: 3
+          function: t_fun
+        updates:
+        - variable: m2_locked
+          value: "0"
+          format: c_expression
+      - location:
+          file_name: 64-ghost-multiple-protecting.c
+          file_hash: $FILE_HASH
+          line: 20
+          column: 3
+          function: t_fun
+        updates:
+        - variable: m2_locked
+          value: "1"
+          format: c_expression
+      - location:
+          file_name: 64-ghost-multiple-protecting.c
+          file_hash: $FILE_HASH
+          line: 22
+          column: 3
+          function: t_fun
+        updates:
+        - variable: m2_locked
+          value: "0"
+          format: c_expression
+      - location:
+          file_name: 64-ghost-multiple-protecting.c
+          file_hash: $FILE_HASH
+          line: 23
+          column: 3
+          function: t_fun
+        updates:
+        - variable: m1_locked
+          value: "0"
+          format: c_expression
+      - location:
+          file_name: 64-ghost-multiple-protecting.c
+          file_hash: $FILE_HASH
+          line: 29
+          column: 3
+          function: main
+        updates:
+        - variable: multithreaded
+          value: "1"
+          format: c_expression
+  - entry_type: flow_insensitive_invariant
+    flow_insensitive_invariant:
+      string: '! multithreaded || (m2_locked || (m1_locked || g2 == 0))'
+      type: assertion
+      format: C
+  - entry_type: flow_insensitive_invariant
+    flow_insensitive_invariant:
+      string: '! multithreaded || (m2_locked || (m1_locked || g1 == 0))'
+      type: assertion
+      format: C
+
   $ goblint --set ana.base.privatization mutex-meet --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types '["flow_insensitive_invariant", "ghost_instrumentation"]' 64-ghost-multiple-protecting.c
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 19