Experiment with unassume for mutex analysis

src/analyses/apron/relationAnalysis.apron.ml

@@ -708,7 +708,7 @@ struct
       Priv.escape man.node (Analyses.ask_of_man man) man.global man.sideg st escaped
     | Assert exp ->
       assert_fn man exp true
-    | Events.Unassume {exp = e; tokens} ->
+    | Events.Unassume {value = Exp e; tokens} ->
       let e_orig = e in
       let ask = Analyses.ask_of_man man in
       let e = replace_deref_exps man.ask e in

src/analyses/base.ml

@@ -3126,7 +3126,7 @@ struct
       set ~man man.local (eval_lv ~man man.local lval) (Cilfacade.typeOfLval lval) (Thread (ValueDomain.Threads.singleton tid))
     | Events.Assert exp ->
       assert_fn man exp true
-    | Events.Unassume {exp; tokens} ->
+    | Events.Unassume {value = Exp exp; tokens} ->
       Timing.wrap "base unassume" (unassume man exp) tokens
     | Events.Longjmped {lval} ->
       begin match lval with

src/analyses/mutexAnalysis.ml

@@ -260,6 +260,20 @@ struct
             M.info_noloc ~category:Race "Mutex %a read-write protects %d variable(s): %a" LockDomain.MustLock.pretty m s VarSet.pretty protected
           )
       end
+    | YamlEntryGlobal (g, task) ->
+      let g: V.t = Obj.obj g in
+      begin match g with
+        | `Left g' when YamlWitness.entry_type_enabled YamlWitnessType.ProtectedBy.entry_type -> (* protecting *)
+          let protecting = GProtecting.get ~write:false Strong (G.protecting (man.global g)) in (* readwrite protecting *)
+          MustLockset.fold (fun mutex acc ->
+              let variable = g'.vname in
+              let mutex = LockDomain.MustLock.show mutex in
+              let entry = YamlWitness.Entry.protected_by ~task ~variable ~mutex in
+              Queries.YS.add entry acc
+            ) protecting (Queries.YS.empty ())
+        | _ -> (* protected *)
+          Queries.Result.top q
+      end
     | _ -> Queries.Result.top q
 
   module A =
@@ -345,6 +359,13 @@ struct
              old_access None None *) (* TODO: what about this case? *)
       end;
       man.local
+    | Unassume {value = ProtectedBy {global; mutexes}; tokens} ->
+      let s = GProtecting.make ~write:true ~recovered:false mutexes in
+      WideningTokenLifter.with_side_tokens (WideningTokenLifter.TS.of_list tokens) (fun () ->
+          man.sideg (V.protecting global) (G.create_protecting s);
+        );
+      M.info ~category:Witness "mutex unassumed %a protected_by: %a" CilType.Varinfo.pretty global MustLockset.pretty mutexes;
+      man.local
     | _ ->
       event man e oman (* delegate to must lockset analysis *)
 

src/analyses/unassumeAnalysis.ml

@@ -9,6 +9,7 @@ module Cil = GoblintCil.Cil
 module NH = CfgTools.NH
 module FH = Hashtbl.Make (CilType.Fundec)
 module EH = Hashtbl.Make (CilType.Exp)
+module VH = Hashtbl.Make (CilType.Varinfo)
 
 module Spec =
 struct
@@ -37,6 +38,13 @@ struct
   let fun_pres: Cil.exp FH.t = FH.create 100
   let pre_invs: inv EH.t NH.t = NH.create 100
 
+  type prot = {
+    mutex: LockDomain.MustLock.t;
+    token: WideningToken.t;
+  }
+
+  let prots: prot VH.t = VH.create 100
+
   let init _ =
     Locator.clear location_locator;
     Locator.clear loop_locator;
@@ -85,6 +93,7 @@ struct
     NH.clear invs;
     FH.clear fun_pres;
     NH.clear pre_invs;
+    VH.clear prots;
 
     let unassume_entry (entry: YamlWitnessType.Entry.t) =
       let uuid = entry.metadata.uuid in
@@ -227,6 +236,34 @@ struct
         List.iteri validate_invariant invariant_set.content
       in
 
+      let unassume_protected_by (protected_by: YamlWitnessType.ProtectedBy.t) =
+        match InvariantParser.parse_cabs protected_by.variable with
+        | Ok variable_cabs ->
+          begin match InvariantParser.parse_cil inv_parser ~fundec:Cil.dummyFunDec ~loc:Cil.dummyFunDec.svar.vdecl variable_cabs with (* TODO: parsing in global scope *)
+            | Ok (Lval (Var variable, NoOffset)) -> (* TODO: support offsets *)
+              begin
+                match InvariantParser.parse_cabs protected_by.mutex with
+                | Ok variable_cabs ->
+                  begin match InvariantParser.parse_cil inv_parser ~fundec:Cil.dummyFunDec ~loc:Cil.dummyFunDec.svar.vdecl variable_cabs with (* TODO: parsing in global scope *)
+                    | Ok (Lval (Var mutex, NoOffset)) -> (* TODO: support offsets *)
+                      VH.add prots variable {mutex = LockDomain.MustLock.of_var mutex; token = (uuid, None)}
+                    | Ok _ ->
+                      M.error ~category:Witness "not a variable: %s" protected_by.mutex
+                    | Error e ->
+                      M.error ~category:Witness "CIL couldn't parse mutex: %s" protected_by.mutex
+                  end
+                | Error e ->
+                  M.error ~category:Witness "Frontc couldn't parse mutex: %s" protected_by.mutex
+              end
+            | Ok _ ->
+              M.error ~category:Witness "not a variable: %s" protected_by.variable
+            | Error e ->
+              M.error ~category:Witness "CIL couldn't parse variable: %s" protected_by.variable
+          end
+        | Error e ->
+          M.error ~category:Witness "Frontc couldn't parse variable: %s" protected_by.variable
+      in
+
       match YamlWitness.entry_type_enabled target_type, entry.entry_type with
       | true, LocationInvariant x ->
         unassume_location_invariant x
@@ -236,7 +273,9 @@ struct
         unassume_precondition_loop_invariant x
       | true, InvariantSet x ->
         unassume_invariant_set x
-      | false, (LocationInvariant _ | LoopInvariant _ | PreconditionLoopInvariant _ | InvariantSet _) ->
+      | true, ProtectedBy x ->
+        unassume_protected_by x
+      | false, (LocationInvariant _ | LoopInvariant _ | PreconditionLoopInvariant _ | InvariantSet _ | ProtectedBy _) ->
         M.info_noloc ~category:Witness "disabled entry of type %s" target_type
       | _ ->
         M.warn_noloc ~category:Witness "cannot unassume entry of type %s" target_type
@@ -262,8 +301,8 @@ struct
       M.info ~category:Witness "unassume invariant: %a" CilType.Exp.pretty e;
       if not !AnalysisState.postsolving then (
         if not (GobConfig.get_bool "ana.unassume.precheck" && Queries.ID.to_bool (man.ask (EvalInt e)) = Some false) then (
-          let tokens = x.token :: List.map (fun {token; _} -> token) xs in
-          man.emit (Unassume {exp = e; tokens});
+          let tokens = x.token :: List.map (fun ({token; _}: inv) -> token) xs in
+          man.emit (Unassume {value = Exp e; tokens});
           List.iter WideningTokenLifter.add tokens
         )
       );
@@ -311,6 +350,21 @@ struct
 
   (* not in sync, query, entry, threadenter because they aren't final transfer function on edge *)
   (* not in vdecl, return, threadspawn because unnecessary targets for invariants? *)
+
+  let event man e oman =
+    begin match e with
+      | Events.EnterMultiThreaded ->
+        VH.to_seq_keys prots
+        |> Seq.iter (fun global ->
+            let ps = VH.find_all prots global in
+            let mutexes = LockDomain.MustLockset.of_list @@ List.map (fun {mutex; _} -> mutex) ps in
+            let tokens = List.map (fun {token; _} -> token) ps in
+            man.emit (Unassume {value = ProtectedBy {global; mutexes}; tokens});
+            List.iter WideningTokenLifter.add tokens
+          )
+      | _ -> ()
+    end;
+    man.local
 end
 
 let _ =

src/analyses/varEq.ml

@@ -569,7 +569,7 @@ struct
 
   let event man e oman =
     match e with
-    | Events.Unassume {exp; _} ->
+    | Events.Unassume {value = Exp exp; _} ->
       (* Unassume must forget equalities,
          otherwise var_eq may still have a numeric first iteration equality
          while base has unassumed, causing unnecessary extra evals. *)

src/config/options.schema.json

@@ -2726,7 +2726,8 @@
                   "precondition_loop_invariant_certificate",
                   "invariant_set",
                   "violation_sequence",
-                  "ghost_instrumentation"
+                  "ghost_instrumentation",
+                  "protected_by"
                 ]
               },
               "default": [

src/domains/events.ml

@@ -3,6 +3,10 @@
 open GoblintCil
 open Pretty
 
+type unassume =
+  | Exp of CilType.Exp.t
+  | ProtectedBy of {global: CilType.Varinfo.t; mutexes: LockDomain.MustLockset.t}
+
 type t =
   | Lock of LockDomain.AddrRW.t
   | Unlock of LockDomain.Addr.t
@@ -14,7 +18,7 @@ type t =
   | Assign of {lval: CilType.Lval.t; exp: CilType.Exp.t} (** Used to simulate old [man.assign]. *) (* TODO: unused *)
   | UpdateExpSplit of exp (** Used by expsplit analysis to evaluate [exp] on post-state. *)
   | Assert of exp
-  | Unassume of {exp: CilType.Exp.t; tokens: WideningToken.t list}
+  | Unassume of {value: unassume; tokens: WideningToken.t list}
   | Longjmped of {lval: CilType.Lval.t option}
 
 (** Should event be emitted after transfer function raises [Deadcode]? *)
@@ -45,5 +49,6 @@ let pretty () = function
   | Assign {lval; exp} -> dprintf "Assign {lval=%a, exp=%a}" CilType.Lval.pretty lval CilType.Exp.pretty exp
   | UpdateExpSplit exp -> dprintf "UpdateExpSplit %a" d_exp exp
   | Assert exp -> dprintf "Assert %a" d_exp exp
-  | Unassume {exp; tokens} -> dprintf "Unassume {exp=%a; tokens=%a}" d_exp exp (d_list ", " WideningToken.pretty) tokens
+  | Unassume {value = Exp exp; tokens} -> dprintf "Unassume {value=Exp %a; tokens=%a}" CilType.Exp.pretty exp (d_list ", " WideningToken.pretty) tokens
+  | Unassume {value = ProtectedBy {global; mutexes}; tokens} -> dprintf "Unassume {value=ProtectedBy {global=%a; mutexes=%a}; tokens=%a}" CilType.Varinfo.pretty global LockDomain.MustLockset.pretty mutexes (d_list ", " WideningToken.pretty) tokens
   | Longjmped {lval} -> dprintf "Longjmped {lval=%a}" (docOpt (CilType.Lval.pretty ())) lval

src/witness/yamlWitness.ml

@@ -177,6 +177,15 @@ struct
       };
     metadata = metadata ~task ();
   }
+
+  (* non-standard extension *)
+  let protected_by ~task ~variable ~(mutex): Entry.t = {
+    entry_type = ProtectedBy {
+        variable;
+        mutex;
+      };
+    metadata = metadata ~task ();
+  }
 end
 
 let yaml_entries_to_file yaml_entries file =
@@ -402,7 +411,7 @@ struct
 
     (* Generate flow-insensitive entries (ghost instrumentation) *)
     let entries =
-      if entry_type_enabled YamlWitnessType.GhostInstrumentation.entry_type then (
+      if entry_type_enabled YamlWitnessType.GhostInstrumentation.entry_type || entry_type_enabled YamlWitnessType.ProtectedBy.entry_type then (
         (* TODO: only at most one ghost_instrumentation entry can ever be produced, so this fold and deduplication is overkill *)
         let module EntrySet = Queries.YS in
         fst @@ GHT.fold (fun g v accs ->
@@ -944,6 +953,54 @@ struct
         None
       in
 
+      let validate_protected_by (protected_by: YamlWitnessType.ProtectedBy.t) =
+        match InvariantParser.parse_cabs protected_by.variable with
+        | Ok variable_cabs ->
+          begin match InvariantParser.parse_cil inv_parser ~fundec:Cil.dummyFunDec ~loc:Cil.dummyFunDec.svar.vdecl variable_cabs with (* TODO: parsing in global scope *)
+            | Ok (Lval (Var variable, NoOffset)) -> (* TODO: support offsets *)
+              begin
+                match InvariantParser.parse_cabs protected_by.mutex with
+                | Ok variable_cabs ->
+                  begin match InvariantParser.parse_cil inv_parser ~fundec:Cil.dummyFunDec ~loc:Cil.dummyFunDec.svar.vdecl variable_cabs with (* TODO: parsing in global scope *)
+                    | Ok (Lval (Var mutex, NoOffset)) -> (* TODO: support offsets *)
+                      if R.ask_global (MustBeProtectedBy {mutex = LockDomain.MustLock.of_var mutex; global = variable; write = false; protection = Strong}) then (
+                        incr cnt_confirmed;
+                        M.success ~category:Witness "protection confirmed";
+                      )
+                      else (
+                        incr cnt_unconfirmed;
+                        M.warn ~category:Witness "protection unconfirmed";
+                      );
+                      None
+                    | Ok _ ->
+                      incr cnt_error;
+                      M.error ~category:Witness "not a variable: %s" protected_by.mutex;
+                      None
+                    | Error e ->
+                      incr cnt_error;
+                      M.error ~category:Witness "CIL couldn't parse mutex: %s" protected_by.mutex;
+                      None
+                  end
+                | Error e ->
+                  incr cnt_error;
+                  M.error ~category:Witness "Frontc couldn't parse mutex: %s" protected_by.mutex;
+                  None
+              end
+            | Ok _ ->
+              incr cnt_error;
+              M.error ~category:Witness "not a variable: %s" protected_by.variable;
+              None
+            | Error e ->
+              incr cnt_error;
+              M.error ~category:Witness "CIL couldn't parse variable: %s" protected_by.variable;
+              None
+          end
+        | Error e ->
+          incr cnt_error;
+          M.error ~category:Witness "Frontc couldn't parse variable: %s" protected_by.variable;
+          None
+      in
+
       match entry_type_enabled target_type, entry.entry_type with
       | true, LocationInvariant x ->
         validate_location_invariant x
@@ -955,7 +1012,9 @@ struct
         validate_invariant_set x
       | true, ViolationSequence x ->
         validate_violation_sequence x
-      | false, (LocationInvariant _ | LoopInvariant _ | PreconditionLoopInvariant _ | InvariantSet _ | ViolationSequence _) ->
+      | true, ProtectedBy x ->
+        validate_protected_by x
+      | false, (LocationInvariant _ | LoopInvariant _ | PreconditionLoopInvariant _ | InvariantSet _ | ViolationSequence _ | ProtectedBy _) ->
         incr cnt_disabled;
         M.info_noloc ~category:Witness "disabled entry of type %s" target_type;
         None

src/witness/yamlWitnessType.ml

@@ -783,6 +783,29 @@ struct
     {ghost_variables; ghost_updates}
 end
 
+module ProtectedBy =
+struct
+  type t = {
+    variable: string; (* TODO: rename to data? *)
+    mutex: string;
+  }
+  [@@deriving eq, ord, hash]
+
+  let entry_type = "protected_by"
+
+  let to_yaml' {variable; mutex} =
+    [
+      ("variable", `String variable);
+      ("mutex", `String mutex);
+    ]
+
+  let of_yaml y =
+    let open GobYaml in
+    let+ variable = y |> find "variable" >>= to_string
+    and+ mutex = y |> find "mutex" >>= to_string in
+    {variable; mutex}
+end
+
 (* TODO: could maybe use GADT, but adds ugly existential layer to entry type pattern matching *)
 module EntryType =
 struct
@@ -796,6 +819,7 @@ struct
     | InvariantSet of InvariantSet.t
     | ViolationSequence of ViolationSequence.t
     | GhostInstrumentation of GhostInstrumentation.t
+    | ProtectedBy of ProtectedBy.t
   [@@deriving eq, ord, hash]
 
   let entry_type = function
@@ -808,6 +832,7 @@ struct
     | InvariantSet _ -> InvariantSet.entry_type
     | ViolationSequence _ -> ViolationSequence.entry_type
     | GhostInstrumentation _ -> GhostInstrumentation.entry_type
+    | ProtectedBy _ -> ProtectedBy.entry_type
 
   let to_yaml' = function
     | LocationInvariant x -> LocationInvariant.to_yaml' x
@@ -819,6 +844,7 @@ struct
     | InvariantSet x -> InvariantSet.to_yaml' x
     | ViolationSequence x -> ViolationSequence.to_yaml' x
     | GhostInstrumentation x -> GhostInstrumentation.to_yaml' x
+    | ProtectedBy x -> ProtectedBy.to_yaml' x
 
   let of_yaml y =
     let open GobYaml in
@@ -850,6 +876,9 @@ struct
     else if entry_type = GhostInstrumentation.entry_type then
       let+ x = y |> GhostInstrumentation.of_yaml in
       GhostInstrumentation x
+    else if entry_type = ProtectedBy.entry_type then
+      let+ x = y |> ProtectedBy.of_yaml in
+      ProtectedBy x
     else
       Error (`Msg ("entry_type " ^ entry_type))
 end

tests/util/yamlWitnessStripCommon.ml

@@ -79,6 +79,8 @@ struct
           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);
         }
+      | ProtectedBy x ->
+        ProtectedBy x (* no location to strip *)
     in
     {entry_type}