Fix Vojdani privatization protected variables in witnesses (closes #1713)

Author: sim642

src/analyses/apron/relationPriv.apron.ml

@@ -431,7 +431,7 @@ struct
 
   let iter_sys_vars getg vq vf = () (* TODO: or report singleton global for any Global query? *)
   let invariant_global ask getg g = Invariant.none
-  let invariant_vars ask getg st = protected_vars ask (* TODO: is this right? *)
+  let invariant_vars ask getg st = protected_vars ask ~kind:Write (* TODO: is this right? *)
 
   let finalize () = ()
 

src/analyses/basePriv.ml

@@ -357,7 +357,7 @@ struct
     | `Thread ->
       st
 
-  let invariant_vars ask getg st = protected_vars ask
+  let invariant_vars ask getg st = protected_vars ask ~kind:Write
 end
 
 module PerMutexMeetPrivBase =
@@ -856,7 +856,7 @@ struct
         ) locks inv
     )
 
-  let invariant_vars ask getg st = protected_vars ask
+  let invariant_vars ask getg st = protected_vars ask ~kind:ReadWrite
 end
 
 
@@ -1102,7 +1102,7 @@ struct
           ) locks inv
       )
 
-  let invariant_vars ask getg st = protected_vars ask
+  let invariant_vars ask getg st = protected_vars ask ~kind:Write
 end
 
 module AbstractLockCenteredGBase (WeakRange: Lattice.S) (SyncRange: Lattice.S) =

src/analyses/commonPriv.ml

@@ -101,9 +101,9 @@ struct
     not (VD.is_immediate_type x.vtype) &&
     ask.f (Q.MustBeProtectedBy {mutex=m; global=x; kind; protection})
 
-  let protected_vars (ask: Q.ask): varinfo list =
+  let protected_vars (ask: Q.ask) ~(kind): varinfo list =
     LockDomain.MustLockset.fold (fun ml acc ->
-        Q.VS.join (ask.f (Q.MustProtectedVars {mutex = ml; kind = Write})) acc
+        Q.VS.join (ask.f (Q.MustProtectedVars {mutex = ml; kind})) acc
       ) (ask.f Q.MustLockset) (Q.VS.empty ())
     |> Q.VS.elements
 end

tests/regression/13-privatized/19-publish-precision.t

@@ -150,7 +150,7 @@ Vojdani does not succeed on check in t_fun.
     dead: 0
     total lines: 20
   [Info][Witness] witness generation summary:
-    location invariants: 11
+    location invariants: 9
     loop invariants: 0
     flow-insensitive invariants: 0
     total generation entries: 1
@@ -160,7 +160,7 @@ Vojdani does not succeed on check in t_fun.
     unsafe: 0
     total memory locations: 1
 
-TODO: Vojdani should not have location_invariant-s on glob1 after locking mutex1 (line 11), only after mutex2.
+Vojdani should not have location_invariant-s on glob1 after locking mutex1 (line 11), only after mutex2.
 
   $ yamlWitnessStrip < witness.yml
   - entry_type: invariant_set
@@ -174,24 +174,6 @@ TODO: Vojdani should not have location_invariant-s on glob1 after locking mutex1
           function: t_fun
         value: (unsigned long )arg == 0UL
         format: c_expression
-    - invariant:
-        type: location_invariant
-        location:
-          file_name: 19-publish-precision.c
-          line: 11
-          column: 3
-          function: t_fun
-        value: 0 <= glob1
-        format: c_expression
-    - invariant:
-        type: location_invariant
-        location:
-          file_name: 19-publish-precision.c
-          line: 11
-          column: 3
-          function: t_fun
-        value: glob1 <= 127
-        format: c_expression
     - invariant:
         type: location_invariant
         location: