Add ghost_instrumentation support to mutexGhosts

src/analyses/mutexGhosts.ml

@@ -10,17 +10,19 @@ struct
   include UnitAnalysis.Spec
   let name () = "mutexGhosts"
 
-  module ThreadCreate = Printable.UnitConf (struct let name = "threadcreate" end)
+  (* module ThreadCreate = Printable.UnitConf (struct let name = "threadcreate" end) *)
   module V =
   struct
-    include Printable.Either3 (Node) (LockDomain.MustLock) (ThreadCreate)
+    include Printable.Either3 (Node) (LockDomain.MustLock) (BoolDomain.Bool)
     let node x = `Left x
     let lock x = `Middle x
-    let threadcreate = `Right ()
+    let threadcreate = `Right false
+    let update = `Right true
     let is_write_only = function
       | `Left _ -> false
       | `Middle _ -> true
-      | `Right _ -> false
+      | `Right false -> false
+      | `Right true -> true
   end
 
   module Locked =
@@ -53,9 +55,11 @@ struct
       | `Bot -> NodeSet.bot ()
       | `Lifted2 (`Lifted2 x) -> x
       | _ -> failwith "MutexGhosts.threadcreate"
+    let update = threadcreate
     let create_node node = `Lifted1 node
     let create_lock lock = `Lifted2 (`Lifted1 lock)
     let create_threadcreate threadcreate = `Lifted2 (`Lifted2 threadcreate)
+    let create_update = create_threadcreate
   end
 
   let mustlock_of_addr (addr: LockDomain.Addr.t): LockDomain.MustLock.t option =
@@ -69,6 +73,7 @@ struct
       | Events.Lock (l, _) when not (LockDomain.Addr.equal l verifier_atomic_addr) ->
         ctx.sideg (V.node ctx.prev_node) (G.create_node (Locked.singleton l, Unlocked.bot (), MultiThread.bot ()));
         if !AnalysisState.postsolving then (
+          ctx.sideg V.update (G.create_update (NodeSet.singleton ctx.prev_node));
           let (locked, _, _) = G.node (ctx.global (V.node ctx.prev_node)) in
           if Locked.cardinal locked > 1 then (
             Locked.iter (fun lock ->
@@ -81,6 +86,7 @@ struct
       | Events.Unlock l when not (LockDomain.Addr.equal l verifier_atomic_addr) ->
         ctx.sideg (V.node ctx.prev_node) (G.create_node (Locked.bot (), Unlocked.singleton l, MultiThread.bot ()));
         if !AnalysisState.postsolving then (
+          ctx.sideg V.update (G.create_update (NodeSet.singleton ctx.prev_node));
           let (_, unlocked, _) = G.node (ctx.global (V.node ctx.prev_node)) in
           if Locked.cardinal unlocked > 1 then (
             Locked.iter (fun lock ->
@@ -91,7 +97,9 @@ struct
           );
         )
       | Events.EnterMultiThreaded ->
-        ctx.sideg (V.node ctx.prev_node) (G.create_node (Locked.bot (), Unlocked.bot (), true))
+        ctx.sideg (V.node ctx.prev_node) (G.create_node (Locked.bot (), Unlocked.bot (), true));
+        if !AnalysisState.postsolving then
+          ctx.sideg V.update (G.create_update (NodeSet.singleton ctx.prev_node));
       | _ -> ()
     end;
     ctx.local
@@ -113,7 +121,7 @@ struct
     | YamlEntryGlobal (g, task) ->
       let g: V.t = Obj.obj g in
       begin match g with
-        | `Left g' ->
+        | `Left g' when YamlWitness.entry_type_enabled YamlWitnessType.GhostVariable.entry_type && YamlWitness.entry_type_enabled YamlWitnessType.GhostUpdate.entry_type ->
           let (locked, unlocked, multithread) = G.node (ctx.global g) in
           let g = g' in
           let entries =
@@ -161,6 +169,70 @@ struct
               entries
           in
           entries
+        | `Right true when YamlWitness.entry_type_enabled YamlWitnessType.GhostInstrumentation.entry_type ->
+          let nodes = G.update (ctx.global g) in
+          let (variables, location_updates) = NodeSet.fold (fun node (variables, location_updates) ->
+              let (locked, unlocked, multithread) = G.node (ctx.global (V.node node)) in
+              let variables' =
+                (* TODO: do variable_entry-s only once *)
+                Locked.fold (fun l acc ->
+                    match mustlock_of_addr l with
+                    | Some l when ghost_var_available ctx (Locked l) ->
+                      let variable = WitnessGhost.variable' (Locked l) in
+                      if BatList.mem_cmp YamlWitnessType.GhostInstrumentation.Variable.compare variable acc then (* TODO: be efficient *)
+                        acc
+                      else
+                        variable :: acc
+                    | _ ->
+                      acc
+                  ) (Locked.union locked unlocked) variables
+              in
+              let updates =
+                Locked.fold (fun l acc ->
+                    match mustlock_of_addr l with
+                    | Some l when ghost_var_available ctx (Locked l) ->
+                      let update = WitnessGhost.update' (Locked l) GoblintCil.one in
+                      update :: acc
+                    | _ ->
+                      acc
+                  ) locked []
+              in
+              let updates =
+                Unlocked.fold (fun l acc ->
+                    match mustlock_of_addr l with
+                    | Some l when ghost_var_available ctx (Locked l) ->
+                      let update = WitnessGhost.update' (Locked l) GoblintCil.zero in
+                      update :: acc
+                    | _ ->
+                      acc
+                  ) unlocked updates
+              in
+              let (variables', updates) =
+                if not (GobConfig.get_bool "exp.earlyglobs") && multithread then (
+                  if ghost_var_available ctx Multithreaded then (
+                    let variable = WitnessGhost.variable' Multithreaded in
+                    let update = WitnessGhost.update' Multithreaded GoblintCil.one in
+                    let variables' =
+                      if BatList.mem_cmp YamlWitnessType.GhostInstrumentation.Variable.compare variable variables' then (* TODO: be efficient *)
+                        variables'
+                      else
+                        variable :: variables'
+                    in
+                    (variables', update :: updates)
+                  )
+                  else
+                    (variables', updates)
+                )
+                else
+                  (variables', updates)
+              in
+              let location_update = WitnessGhost.location_update' ~node ~updates in
+              (variables', location_update :: location_updates)
+            ) nodes ([], [])
+          in
+          let entry = WitnessGhost.instrumentation_entry ~task ~variables ~location_updates in
+          Queries.YS.singleton entry
+        | `Left _ -> Queries.Result.top q
         | `Middle _ -> Queries.Result.top q
         | `Right _ -> Queries.Result.top q
       end

src/witness/witnessGhost.ml

@@ -1,7 +1,7 @@
 (** Ghost variables for YAML witnesses. *)
 
 let enabled () =
-  YamlWitness.entry_type_enabled YamlWitnessType.GhostVariable.entry_type && YamlWitness.entry_type_enabled YamlWitnessType.GhostUpdate.entry_type
+  (YamlWitness.entry_type_enabled YamlWitnessType.GhostVariable.entry_type && YamlWitness.entry_type_enabled YamlWitnessType.GhostUpdate.entry_type) || YamlWitness.entry_type_enabled YamlWitnessType.GhostInstrumentation.entry_type
 
 module Var = WitnessGhostVar
 
@@ -24,3 +24,23 @@ let update_entry ~task ~node x e =
   let variable = name_varinfo x in
   let expression = CilType.Exp.show e in
   YamlWitness.Entry.ghost_update ~task ~location ~variable ~expression
+
+let variable' x =
+  let variable = name_varinfo x in
+  let type_ = String.trim (CilType.Typ.show (typ x)) in (* CIL printer puts space at the end of some types *)
+  let initial = CilType.Exp.show (initial x) in
+  YamlWitness.Entry.ghost_variable' ~variable ~type_ ~initial
+
+let update' x e =
+  let variable = name_varinfo x in
+  let expression = CilType.Exp.show e in
+  YamlWitness.Entry.ghost_update' ~variable ~expression
+
+let location_update' ~node ~updates =
+  let loc = Node.location node in
+  let location_function = (Node.find_fundec node).svar.vname in
+  let location = YamlWitness.Entry.location ~location:loc ~location_function in
+  YamlWitness.Entry.ghost_location_update' ~location ~updates
+
+let instrumentation_entry ~task ~variables ~location_updates =
+  YamlWitness.Entry.ghost_instrumentation ~task ~variables ~location_updates

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

@@ -148,6 +148,93 @@ Earlyglobs shouldn't cause protected writes in multithreaded mode from being imm
     unsafe: 0
     total memory locations: 1
 
+Same with ghost_instrumentation entry.
+
+  $ goblint --enable ana.sv-comp.functions --set ana.base.privatization protection --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:
+    total generation entries: 3
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: ghost_instrumentation
+    ghost_variables:
+    - name: multithreaded
+      scope: global
+      type: int
+      initial: "0"
+    - name: m_locked
+      scope: global
+      type: int
+      initial: "0"
+    ghost_updates:
+    - location:
+        file_name: 74-mutex.c
+        file_hash: $FILE_HASH
+        line: 38
+        column: 3
+        function: main
+      updates:
+      - ghost_variable: m_locked
+        expression: "0"
+    - location:
+        file_name: 74-mutex.c
+        file_hash: $FILE_HASH
+        line: 36
+        column: 3
+        function: main
+      updates:
+      - ghost_variable: m_locked
+        expression: "1"
+    - location:
+        file_name: 74-mutex.c
+        file_hash: $FILE_HASH
+        line: 34
+        column: 3
+        function: main
+      updates:
+      - ghost_variable: multithreaded
+        expression: "1"
+    - location:
+        file_name: 74-mutex.c
+        file_hash: $FILE_HASH
+        line: 23
+        column: 5
+        function: producer
+      updates:
+      - ghost_variable: m_locked
+        expression: "0"
+    - location:
+        file_name: 74-mutex.c
+        file_hash: $FILE_HASH
+        line: 20
+        column: 5
+        function: producer
+      updates:
+      - ghost_variable: m_locked
+        expression: "1"
+  - entry_type: flow_insensitive_invariant
+    flow_insensitive_invariant:
+      string: '! multithreaded || (m_locked || used == 0)'
+      type: assertion
+      format: C
+  - entry_type: flow_insensitive_invariant
+    flow_insensitive_invariant:
+      string: '! multithreaded || (0 <= used && used <= 1)'
+      type: assertion
+      format: C
+
 Same 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_variable", "ghost_update"]' 74-mutex.c