Merge pull request #529 from goblint/part-access-refactor

Generalize pairwise race detection

Author: michael-schwarz

src/analyses/accessAnalysis.ml

@@ -19,7 +19,7 @@ struct
 
   module G =
   struct
-    include Access.PM
+    include Access.AS
 
     let leq x y = !GU.postsolving || leq x y (* HACK: to pass verify*)
   end
@@ -34,37 +34,29 @@ struct
     vulnerable := 0;
     unsafe := 0
 
-  let side_access ctx ty lv_opt ls_opt (conf, mhp, w, loc, e, lp) =
-    if !GU.should_warn then (
-      let d =
-        let open Access in
-        PM.singleton ls_opt (
-          AS.singleton (conf, mhp, 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 side_access ctx ty lv_opt (conf, w, loc, e, a) =
+    let d =
+      if !GU.should_warn then
+        Access.AS.singleton (conf, w, loc, e, a)
+      else
+        G.bot () (* HACK: just to pass validation with MCP DomVariantLattice *)
+    in
+    ctx.sideg (lv_opt, ty) d
 
   let do_access (ctx: (D.t, G.t, C.t, V.t) ctx) (w:bool) (reach:bool) (conf:int) (e:exp) =
-    let tid = ctx.ask CurrentThreadId in
-    let created = ctx.ask CreatedThreads in
-    let joined = ctx.ask MustJoinedThreads in
-    let mhp:MHP.t = {tid=tid; created=created; must_joined=joined } in
     let open Queries in
-    let part_access ctx (e:exp) (vo:varinfo option) (w: bool) =
+    let part_access ctx (e:exp) (vo:varinfo option) (w: bool): MCPAccess.A.t =
       ctx.emit (Access {var_opt=vo; write=w});
       (*partitions & locks*)
-      ctx.ask (PartAccess {exp=e; var_opt=vo; write=w})
+      Obj.obj (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 mhp vo oo (po,pd);
+      let a = part_access ctx e vo w in
+      Access.add (side_access ctx) e w conf vo oo a;
     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 mhp (`Struct (ci,`NoOffset)) None (po,pd)
+      let a = part_access ctx e None w in
+      Access.add_struct (side_access ctx) e w conf (`Struct (ci,`NoOffset)) None a
     in
     let has_escaped g = ctx.ask (Queries.MayEscape g) in
     (* The following function adds accesses to the lval-set ls
@@ -213,9 +205,9 @@ struct
     | 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
+      let accs = ctx.global g in
+      Access.print_accesses g accs;
+      Access.incr_summary safe vulnerable unsafe g accs
     | _ -> Queries.Result.top q
 
   let finalize () =

src/analyses/apron/apronAnalysis.apron.ml

@@ -278,7 +278,7 @@ struct
         | _ -> false (* remove everything else (globals, global privs) *)
       )
     in
-    let unify_apr = A.unify Man.mgr new_apr new_fun_apr in (* TODO: unify_with *)
+    let unify_apr = ApronDomain.A.unify Man.mgr new_apr new_fun_apr in (* TODO: unify_with *)
     if M.tracing then M.tracel "combine" "apron unifying %a %a = %a\n" AD.pretty new_apr AD.pretty new_fun_apr AD.pretty unify_apr;
     let unify_st = {fun_st with apr = unify_apr} in
     if AD.type_tracked (Cilfacade.fundec_return_type f) then (