Implement vojdani privatization invariant_global based on protection

Author: sim642

src/analyses/basePriv.ml

@@ -829,8 +829,28 @@ 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 g) in (* TODO: read-write locks *)
+    if LockDomain.MustLockset.is_all locks || LockDomain.MustLockset.is_empty locks then (* TODO: output unprotected invariant with empty lockset? *)
+      Invariant.none
+    else (
+      let read_global g = getg g in (* TODO: read top for others? or 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