Refactor race warnings (accesses) to use global invariant on master

conf/svcomp.json

@@ -16,6 +16,7 @@
       "threadreturn",
       "mallocWrapper",
       "mutex",
+      "access",
       "escape",
       "expRelation",
       "var_eq",

conf/svcomp21.json

@@ -15,6 +15,7 @@
       "threadflag",
       "mallocWrapper",
       "mutex",
+      "access",
       "escape",
       "expRelation",
       "var_eq",

conf/svcomp22.json

@@ -15,6 +15,7 @@
       "threadflag",
       "mallocWrapper",
       "mutex",
+      "access",
       "escape",
       "expRelation",
       "var_eq",

src/analyses/accessAnalysis.ml

@@ -0,0 +1,231 @@
+(** Access and data race analysis. *)
+
+module M = Messages
+module LF = LibraryFunctions
+open Prelude.Ana
+open Analyses
+open GobConfig
+
+
+(** Access and data race analyzer without base --- this is the new standard *)
+module Spec =
+struct
+  include Analyses.DefaultSpec
+
+  let name () = "access"
+
+  (** Add current lockset alongside to the base analysis domain. Global data is collected using dirty side-effecting. *)
+  module D = Lattice.Unit
+  module C = Lattice.Unit
+
+  module G =
+  struct
+    include Access.PM
+
+    let leq x y = !GU.postsolving || leq x y (* HACK: to pass verify*)
+  end
+  module V = Printable.Prod (Access.LVOpt) (Access.T)
+
+  let safe       = ref 0
+  let vulnerable = ref 0
+  let unsafe     = ref 0
+
+  let init marshal =
+    safe := 0;
+    vulnerable := 0;
+    unsafe := 0
+
+  let side_access ctx ty lv_opt ls_opt (conf, w, loc, e, lp) =
+    if !GU.should_warn then (
+      let d =
+        let open Access in
+        PM.singleton ls_opt (
+          AS.singleton (conf, w, loc, e, lp)
+        )
+      in
+      ctx.sideg (lv_opt, ty) d
+    )
+    else
+      ctx.sideg (lv_opt, ty) (G.bot ()) (* HACK: just to pass validation with MCP DomVariantLattice *)
+
+  let do_access (ctx: (D.t, G.t, C.t, V.t) ctx) (w:bool) (reach:bool) (conf:int) (e:exp) =
+    let open Queries in
+    let part_access ctx (e:exp) (vo:varinfo option) (w: bool) =
+      ctx.emit (Access {var_opt=vo; write=w});
+      (*partitions & locks*)
+      ctx.ask (PartAccess {exp=e; var_opt=vo; write=w})
+    in
+    let add_access conf vo oo =
+      let (po,pd) = part_access ctx e vo w in
+      Access.add (side_access ctx) e w conf vo oo (po,pd);
+    in
+    let add_access_struct conf ci =
+      let (po,pd) = part_access ctx e None w in
+      Access.add_struct (side_access ctx) e w conf (`Struct (ci,`NoOffset)) None (po,pd)
+    in
+    let has_escaped g = ctx.ask (Queries.MayEscape g) in
+    (* The following function adds accesses to the lval-set ls
+       -- this is the common case if we have a sound points-to set. *)
+    let on_lvals ls includes_uk =
+      let ls = LS.filter (fun (g,_) -> g.vglob || has_escaped g) ls in
+      let conf = if reach then conf - 20 else conf in
+      let conf = if includes_uk then conf - 10 else conf in
+      let f (var, offs) =
+        let coffs = Lval.CilLval.to_ciloffs offs in
+        if CilType.Varinfo.equal var dummyFunDec.svar then
+          add_access conf None (Some coffs)
+        else
+          add_access conf (Some var) (Some coffs)
+      in
+      LS.iter f ls
+    in
+    let reach_or_mpt = if reach then ReachableFrom e else MayPointTo e in
+    match ctx.ask reach_or_mpt with
+    | ls when not (LS.is_top ls) && not (Queries.LS.mem (dummyFunDec.svar,`NoOffset) ls) ->
+      (* the case where the points-to set is non top and does not contain unknown values *)
+      on_lvals ls false
+    | ls when not (LS.is_top ls) ->
+      (* the case where the points-to set is non top and contains unknown values *)
+      let includes_uk = ref false in
+      (* now we need to access all fields that might be pointed to: is this correct? *)
+      begin match ctx.ask (ReachableUkTypes e) with
+        | ts when Queries.TS.is_top ts ->
+          includes_uk := true
+        | ts ->
+          if Queries.TS.is_empty ts = false then
+            includes_uk := true;
+          let f = function
+            | TComp (ci, _) ->
+              add_access_struct (conf - 50) ci
+            | _ -> ()
+          in
+          Queries.TS.iter f ts
+      end;
+      on_lvals ls !includes_uk
+    | _ ->
+      add_access (conf - 60) None None
+
+  let access_one_top ?(force=false) ctx write reach exp =
+    (* ignore (Pretty.printf "access_one_top %b %b %a:\n" write reach d_exp exp); *)
+    if force || ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) then (
+      let conf = 110 in
+      if reach || write then do_access ctx write reach conf exp;
+      Access.distribute_access_exp (do_access ctx) false false conf exp;
+    )
+
+  (** We just lift start state, global and dependency functions: *)
+  let startstate v = ()
+  let threadenter ctx lval f args = [()]
+  let exitstate  v = ()
+
+
+  (** Transfer functions: *)
+
+  let assign ctx lval rval : D.t =
+    (* ignore global inits *)
+    if !GU.global_initialization then ctx.local else begin
+      access_one_top ctx true  false (AddrOf lval);
+      access_one_top ctx false false rval;
+      ctx.local
+    end
+
+  let branch ctx exp tv : D.t =
+    access_one_top ctx false false exp;
+    ctx.local
+
+  let return ctx exp fundec : D.t =
+    begin match exp with
+      | Some exp -> access_one_top ctx false false exp
+      | None -> ()
+    end;
+    ctx.local
+
+  let body ctx f : D.t =
+    ctx.local
+
+  let special ctx lv f arglist : D.t =
+    match (LF.classify f.vname arglist, f.vname) with
+    (* TODO: remove cases *)
+    | _, "_lock_kernel" ->
+      ctx.local
+    | _, "_unlock_kernel" ->
+      ctx.local
+    | `Lock (failing, rw, nonzero_return_when_aquired), _
+      -> ctx.local
+    | `Unlock, "__raw_read_unlock"
+    | `Unlock, "__raw_write_unlock"  ->
+      ctx.local
+    | `Unlock, _ ->
+      ctx.local
+    | _, "spinlock_check" -> ctx.local
+    | _, "acquire_console_sem" when get_bool "kernel" ->
+      ctx.local
+    | _, "release_console_sem" when get_bool "kernel" ->
+      ctx.local
+    | _, "__builtin_prefetch" | _, "misc_deregister" ->
+      ctx.local
+    | _, "__VERIFIER_atomic_begin" when get_bool "ana.sv-comp.functions" ->
+      ctx.local
+    | _, "__VERIFIER_atomic_end" when get_bool "ana.sv-comp.functions" ->
+      ctx.local
+    | _, "pthread_cond_wait"
+    | _, "pthread_cond_timedwait" ->
+      ctx.local
+    | _, x ->
+      let arg_acc act =
+        match LF.get_threadsafe_inv_ac x with
+        | Some fnc -> (fnc act arglist)
+        | _ -> arglist
+      in
+      List.iter (access_one_top ctx false true) (arg_acc `Read);
+      List.iter (access_one_top ctx true  true ) (arg_acc `Write);
+      (match lv with
+      | Some x -> access_one_top ctx true false (AddrOf x)
+      | None -> ());
+      ctx.local
+
+  let enter ctx lv f args : (D.t * D.t) list =
+    [(ctx.local,ctx.local)]
+
+  let combine ctx lv fexp f args fc al =
+    access_one_top ctx false false fexp;
+    begin match lv with
+      | None      -> ()
+      | Some lval -> access_one_top ctx true false (AddrOf lval)
+    end;
+    List.iter (access_one_top ctx false false) args;
+    al
+
+
+  let threadspawn ctx lval f args fctx =
+    (* must explicitly access thread ID lval because special to pthread_create doesn't if singlethreaded before *)
+    begin match lval with
+    | None -> ()
+    | Some lval -> access_one_top ~force:true ctx true false (AddrOf lval) (* must force because otherwise doesn't if singlethreaded before *)
+    end;
+    ctx.local
+
+  let query ctx (type a) (q: a Queries.t): a Queries.result =
+    match q with
+    | WarnGlobal g ->
+      let g: V.t = Obj.obj g in
+      (* ignore (Pretty.printf "WarnGlobal %a\n" CilType.Varinfo.pretty g); *)
+      let pm = ctx.global g in
+      Access.print_accesses g pm;
+      Access.incr_summary safe vulnerable unsafe g pm
+    | _ -> Queries.Result.top q
+
+  let finalize () =
+    let total = !safe + !unsafe + !vulnerable in
+    if total > 0 then (
+      ignore (Pretty.printf "\nSummary for all memory locations:\n");
+      ignore (Pretty.printf "\tsafe:        %5d\n" !safe);
+      ignore (Pretty.printf "\tvulnerable:  %5d\n" !vulnerable);
+      ignore (Pretty.printf "\tunsafe:      %5d\n" !unsafe);
+      ignore (Pretty.printf "\t-------------------\n");
+      ignore (Pretty.printf "\ttotal:       %5d\n" total)
+    )
+end
+
+let _ =
+  MCP.register_analysis (module Spec : MCPSpec)

src/analyses/mCP.ml

@@ -533,11 +533,6 @@ struct
       in
       List.map (fun (n,d) -> n, spec_assign n d) xs
 
-  let finalize () =
-    let r = finalize () in
-    Access.print_result ();
-    r
-
   let rec do_splits ctx pv (xs:(int * (Obj.t * Events.t list)) list) =
     let split_one n (d,emits) =
       let nv = assoc_replace (n,d) pv in
@@ -661,7 +656,7 @@ struct
     else
       let asked' = QuerySet.add (Any q) asked in
       let sides = ref [] in
-      let f a (n,(module S:MCPSpec),d) =
+      let f ~q a (n,(module S:MCPSpec),d) =
         let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
           { local  = obj d
           ; node   = ctx.node
@@ -689,12 +684,16 @@ struct
       | Queries.PrintFullState ->
         ignore (Pretty.printf "Current State:\n%a\n\n" D.pretty ctx.local);
         ()
+      | Queries.WarnGlobal g ->
+        (* WarnGlobal is special: it only goes to corresponding analysis and the argument variant is unlifted for it *)
+        let (n, g): V.t = Obj.obj g in
+        f ~q:(WarnGlobal (Obj.repr g)) (Result.top ()) (n, spec n, assoc n ctx.local)
       (* | EvalInt e ->
         (* TODO: only query others that actually respond to EvalInt *)
         (* 2x speed difference on SV-COMP nla-digbench-scaling/ps6-ll_valuebound5.c *)
         f (Result.top ()) (!base_id, spec !base_id, assoc !base_id ctx.local) *)
       | _ ->
-        let r = fold_left f (Result.top ()) @@ spec_list ctx.local in
+        let r = fold_left (f ~q) (Result.top ()) @@ spec_list ctx.local in
         do_sideg ctx !sides;
         r