pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[racerd] make nontrivial domain types private

Browse Source 
Reviewed By: da319

Differential Revision: D6348769

fbshipit-source-id: dd76eb7
master
Sam Blackshear 7 years ago committed by Facebook Github Bot
parent 181959216b
commit dbfbf9cf01
3 changed files with 29 additions and 17 deletions
Show Stats Download Patch File Download Diff File

25
infer/src/concurrency/RacerD.ml
Unescape View File

@ -172,7 +172,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
&& not (has_return_annot thread_safe_or_thread_confined pname)
then
let open Domain in
let pre = AccessPrecondition.make locks threads proc_data.pdesc in
let pre = AccessPrecondition.make_protected locks threads proc_data.pdesc in
AccessDomain.add_access pre (TraceElem.make_unannotated_call_access pname loc) attribute_map
else attribute_map
@ -223,17 +223,17 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
then acc
else
let pre =
match AccessPrecondition.make locks threads proc_data.pdesc with
match AccessPrecondition.make_protected locks threads proc_data.pdesc with
| AccessPrecondition.Protected _ as excluder ->
excluder
| _ ->
match OwnershipDomain.get_owned base_access_path ownership with
| OwnershipAbstractValue.OwnedIf formal_indexes ->
AccessPrecondition.Unprotected formal_indexes
AccessPrecondition.make_unprotected formal_indexes
| OwnershipAbstractValue.Owned ->
assert false
| OwnershipAbstractValue.Unowned ->
AccessPrecondition.TotallyUnprotected
AccessPrecondition.totally_unprotected
in
add_field_accesses pre base_access_path acc accesses
in
@ -361,8 +361,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let container_access =
TraceElem.make_container_access receiver_ap ~is_write callee_pname callee_loc
in
AccessDomain.add_access (Unprotected (IntSet.singleton 0)) container_access
AccessDomain.empty
AccessDomain.add_access
(AccessPrecondition.make_unprotected (IntSet.singleton 0))
container_access AccessDomain.empty
in
Some
{ locks= false
@ -577,7 +578,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
accesses_acc
else
let pre =
match AccessPrecondition.make locks threads pdesc with
match AccessPrecondition.make_protected locks threads pdesc with
| AccessPrecondition.Protected _ as excluder (* access protected *) ->
excluder
| _ ->
@ -586,7 +587,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| OwnershipAbstractValue.OwnedIf formal_indexes ->
(* the actual passed to the current callee is rooted in a
formal *)
AccessPrecondition.Unprotected formal_indexes
AccessPrecondition.make_unprotected formal_indexes
| OwnershipAbstractValue.Unowned | OwnershipAbstractValue.Owned ->
match
OwnershipDomain.get_owned actual_access_path astate.ownership
@ -594,18 +595,18 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| OwnershipAbstractValue.OwnedIf formal_indexes ->
(* access path conditionally owned if [formal_indexes] are
owned *)
AccessPrecondition.Unprotected formal_indexes
AccessPrecondition.make_unprotected formal_indexes
| OwnershipAbstractValue.Owned ->
assert false
| OwnershipAbstractValue.Unowned ->
(* access path not rooted in a formal and not conditionally
owned *)
AccessPrecondition.TotallyUnprotected
AccessPrecondition.totally_unprotected
in
update_caller_accesses pre ownership_accesses accesses_acc
| _ ->
(* couldn't find access path, don't know if it's owned *)
update_caller_accesses AccessPrecondition.TotallyUnprotected
update_caller_accesses AccessPrecondition.totally_unprotected
ownership_accesses accesses_acc
in
let accesses =
@ -614,7 +615,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| AccessPrecondition.Protected _ ->
update_caller_accesses pre callee_accesses accesses_acc
| AccessPrecondition.TotallyUnprotected ->
let pre' = AccessPrecondition.make locks threads pdesc in
let pre' = AccessPrecondition.make_protected locks threads pdesc in
update_caller_accesses pre' callee_accesses accesses_acc
| AccessPrecondition.Unprotected formal_indexes ->
IntSet.fold

9
infer/src/concurrency/RacerDDomain.ml
Unescape View File

@ -371,7 +371,7 @@ module AccessPrecondition = struct
(IntSet.elements indexes)
let make locks thread pdesc =
let make_protected locks thread pdesc =
let is_main_thread = ThreadsDomain.is_any_but_self thread in
let locked = locks || Procdesc.is_java_synchronized pdesc in
if not locked && not is_main_thread then TotallyUnprotected
@ -379,6 +379,13 @@ module AccessPrecondition = struct
else if locked then Protected Excluder.Lock
else Protected Excluder.Thread
let make_unprotected indexes =
assert (not (IntSet.is_empty indexes)) ;
Unprotected indexes
let totally_unprotected = TotallyUnprotected
end
module AccessDomain = struct

10
infer/src/concurrency/RacerDDomain.mli
Unescape View File

@ -11,7 +11,7 @@ open! IStd
module F = Format
module Access : sig
type t =
type t = private
| Read of AccessPath.t (** Field or array read *)
| Write of AccessPath.t (** Field or array write *)
| ContainerRead of AccessPath.t * Typ.Procname.t (** Read of container object *)
@ -163,7 +163,7 @@ module Excluder : sig
end
module AccessPrecondition : sig
type t =
type t = private
| Protected of Excluder.t
(** access potentially protected for mutual exclusion by
lock or thread or both *)
@ -175,7 +175,11 @@ module AccessPrecondition : sig
val pp : F.formatter -> t -> unit
val make : LocksDomain.astate -> ThreadsDomain.astate -> Procdesc.t -> t
val make_protected : LocksDomain.astate -> ThreadsDomain.astate -> Procdesc.t -> t
val make_unprotected : IntSet.t -> t
val totally_unprotected : t
end
(** map of access precondition |-> set of accesses. the map should hold all accesses to a

Write Preview
Loading…
Cancel
Save