Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use record as Access.A type instead of a quintuple #1170

Merged
merged 3 commits into from
Sep 15, 2023
Merged

Use record as Access.A type instead of a quintuple #1170

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
a1464e1
Use record as Access.A type instead of a quintuple
karoliineh Sep 14, 2023
929b658
Inline d_msg () to doc in access
karoliineh Sep 14, 2023
60952d9
Pass access as a variable instead of destructing the record
karoliineh Sep 15, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
33 changes: 17 additions & 16 deletions src/analyses/raceAnalysis.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -225,9 +225,9 @@ struct
| _ ->
()

let side_access ctx (conf, w, loc, e, a) ((memoroot, offset) as memo) =
let side_access ctx Access.A.{conf; kind; node; exp; acc} ((memoroot, offset) as memo) =
if !AnalysisState.should_warn then
ctx.sideg (V.access memoroot) (G.create_access (OffsetTrie.singleton offset (`Lifted (Access.AS.singleton (conf, w, loc, e, a)))));
ctx.sideg (V.access memoroot) (G.create_access (OffsetTrie.singleton offset (`Lifted (Access.AS.singleton {conf; kind; node; exp; acc}))));
karoliineh marked this conversation as resolved.
Show resolved Hide resolved
side_vars ctx memo

(** Side-effect empty access set for prefix-type_suffix race checking. *)
Expand Down Expand Up @@ -302,24 +302,24 @@ struct
) (G.vars (ctx.global (V.vars g)))
| _ -> Queries.Result.top q

let event ctx e octx =
match e with
| Events.Access {exp=e; lvals; kind; reach} when ThreadFlag.is_currently_multi (Analyses.ask_of_ctx ctx) -> (* threadflag query in post-threadspawn ctx *)
let event ctx exp octx =
match exp with
| Events.Access {exp; lvals; kind; reach} when ThreadFlag.is_currently_multi (Analyses.ask_of_ctx ctx) -> (* threadflag query in post-threadspawn ctx *)
(* must use original (pre-assign, etc) ctx queries *)
let conf = 110 in
let module LS = Queries.LS in
let part_access (vo:varinfo option): MCPAccess.A.t =
(*partitions & locks*)
Obj.obj (octx.ask (PartAccess (Memory {exp=e; var_opt=vo; kind})))
Obj.obj (octx.ask (PartAccess (Memory {exp; var_opt=vo; kind})))
in
let loc = Option.get !Node.current_node in
let node = Option.get !Node.current_node in
let add_access conf voffs =
let a = part_access (Option.map fst voffs) in
Access.add ~side:(side_access octx (conf, kind, loc, e, a)) ~side_empty:(side_access_empty octx) e voffs;
let acc = part_access (Option.map fst voffs) in
Access.add ~side:(side_access octx {conf; kind; node; exp; acc}) ~side_empty:(side_access_empty octx) exp voffs;
in
let add_access_struct conf ci =
let a = part_access None in
Access.add_one ~side:(side_access octx (conf, kind, loc, e, a)) (`Type (TSComp (ci.cstruct, ci.cname, [])), `NoOffset)
let acc = part_access None in
Access.add_one ~side:(side_access octx {conf; kind; node; exp; acc}) (`Type (TSComp (ci.cstruct, ci.cname, [])), `NoOffset)
in
let has_escaped g = octx.ask (Queries.MayEscape g) in
(* The following function adds accesses to the lval-set ls
Expand All @@ -345,7 +345,7 @@ struct
(* 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 octx.ask (ReachableUkTypes e) with
begin match octx.ask (ReachableUkTypes exp) with
| ts when Queries.TS.is_top ts ->
includes_uk := true
| ts ->
Expand All @@ -370,12 +370,13 @@ struct
(* perform shallow and deep invalidate according to Library descriptors *)
let desc = LibraryFunctions.find f in
if List.mem LibraryDesc.ThreadUnsafe desc.attrs then (
let e = Lval (Var f, NoOffset) in
let exp = Lval (Var f, NoOffset) in
let conf = 110 in
let loc = Option.get !Node.current_node in
let kind = AccessKind.Call in
let node = Option.get !Node.current_node in
let vo = Some f in
let a = Obj.obj (ctx.ask (PartAccess (Memory {exp=e; var_opt=vo; kind=Call}))) in
side_access ctx (conf, Call, loc, e, a) ((`Var f), `NoOffset) ;
let acc = Obj.obj (ctx.ask (PartAccess (Memory {exp; var_opt=vo; kind}))) in
side_access ctx {conf; kind; node; exp; acc} ((`Var f), `NoOffset) ;
);
ctx.local

Expand Down
31 changes: 17 additions & 14 deletions src/domains/access.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -329,12 +329,18 @@ and distribute_access_type f = function
module A =
struct
include Printable.Std
type t = int * AccessKind.t * Node.t * CilType.Exp.t * MCPAccess.A.t [@@deriving eq, ord, hash]
type t = {
conf : int;
kind : AccessKind.t;
node : Node.t;
exp : CilType.Exp.t;
acc : MCPAccess.A.t;
} [@@deriving eq, ord, hash]

let name () = "access"

let pretty () (conf, kind, node, e, lp) =
Pretty.dprintf "%d, %a, %a, %a, %a" conf AccessKind.pretty kind CilType.Location.pretty (Node.location node) CilType.Exp.pretty e MCPAccess.A.pretty lp
let pretty () {conf; kind; node; exp; acc} =
Pretty.dprintf "%d, %a, %a, %a, %a" conf AccessKind.pretty kind CilType.Location.pretty (Node.location node) CilType.Exp.pretty exp MCPAccess.A.pretty acc

include Printable.SimplePretty (
struct
Expand All @@ -343,28 +349,26 @@ struct
end
)

let conf (conf, _, _, _, _) = conf

let relift (conf, kind, node, e, a) =
(conf, kind, node, e, MCPAccess.A.relift a)
let relift {conf; kind; node; exp; acc} =
{conf; kind; node; exp; acc = MCPAccess.A.relift acc}
end

module AS =
struct
include SetDomain.Make (A)

let max_conf accs =
accs |> elements |> List.map A.conf |> (List.max ~cmp:Int.compare)
accs |> elements |> List.map (fun {A.conf; _} -> conf) |> (List.max ~cmp:Int.compare)
end


(* Check if two accesses may race and if yes with which confidence *)
let may_race (conf,(kind: AccessKind.t),loc,e,a) (conf2,(kind2: AccessKind.t),loc2,e2,a2) =
let may_race A.{kind; acc; _} A.{kind=kind2; acc=acc2; _} =
if kind = Read && kind2 = Read then
false (* two read/read accesses do not race *)
else if not (get_bool "ana.race.free") && (kind = Free || kind2 = Free) then
false
else if not (MCPAccess.A.may_race a a2) then
else if not (MCPAccess.A.may_race acc acc2) then
false (* analysis-specific information excludes race *)
else
true
Expand Down Expand Up @@ -487,7 +491,7 @@ let race_conf accs =
if AS.cardinal accs = 1 then ( (* singleton component *)
let acc = AS.choose accs in
if may_race acc acc then (* self-race *)
Some (A.conf acc)
Some (acc.conf)
else
None
)
Expand Down Expand Up @@ -516,9 +520,8 @@ let print_accesses memo grouped_accs =
let allglobs = get_bool "allglobs" in
let race_threshold = get_int "warn.race-threshold" in
let msgs race_accs =
let h (conf,kind,node,e,a) =
let d_msg () = dprintf "%a with %a (conf. %d)" AccessKind.pretty kind MCPAccess.A.pretty a conf in
let doc = dprintf "%t (exp: %a)" d_msg d_exp e in
let h A.{conf; kind; node; exp; acc} =
let doc = dprintf "%a with %a (conf. %d) (exp: %a)" AccessKind.pretty kind MCPAccess.A.pretty acc conf d_exp exp in
(doc, Some (Messages.Location.Node node))
in
AS.elements race_accs
Expand Down
Loading