@ -457,121 +457,77 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
Typ . Procname . pp callee_pname
Typ . Procname . pp callee_pname
end
end
| NoEffect ->
| NoEffect ->
match
match get_summary pdesc callee_pname actuals ~ f_resolve_id loc tenv with
get_summary pdesc callee_pname actuals ~ f_resolve_id loc tenv with
| Some ( callee_threads , callee_locks , callee_accesses , return_attributes ) ->
| Some ( callee_threads , callee_locks , callee_accesses , return_attributes ) ->
let call_site = CallSite . make callee_pname loc in
let update_caller_accesses pre callee_accesses caller_accesses =
let combine_accesses_for_pre pre ~ caller_accesses ~ callee_accesses =
let combined_accesses =
let combined_accesses =
PathDomain . with_callsite
PathDomain . with_callsite callee_accesses ( CallSite . make callee_pname loc )
( AccessDomain . get_accesses pre callee_accesses ) call_site
| > PathDomain . join ( AccessDomain . get_accesses pre caller_accesses ) in
| > PathDomain . join ( AccessDomain . get_accesses pre caller_accesses ) in
AccessDomain . add pre combined_accesses caller_accesses in
AccessDomain . add pre combined_accesses caller_accesses in
let locks' = callee_locks | | astate . locks in
let locks = callee_locks | | astate . locks in
let threads' = callee_threads | | astate . threads in
let threads = callee_threads | | astate . threads in
let astate' =
let unprotected = is_unprotected locks pdesc in
let unprotected = is_unprotected locks' pdesc in
(* add [ownership_accesses] to the [accesses_acc] with a protected pre if [exp]
let add_conditional_accesses index accesses_acc ( actual_exp , actual_typ ) =
is owned , and an appropriate unprotected pre otherwise * )
if is_constant actual_exp
let add_ownership_access ownership_accesses ( actual_exp , typ ) accesses_acc =
then
if is_constant actual_exp
(* the actual is a constant, so it's owned in the caller. *)
then
accesses_acc
(* the actual is a constant, so it's owned in the caller. *)
else
accesses_acc
let callee_conditional_accesses =
else
PathDomain . with_callsite
match AccessPath . of_lhs_exp actual_exp typ ~ f_resolve_id with
( AccessDomain . get_accesses ( ProtectedIf ( Some index ) ) callee_accesses )
| Some actual_access_path ->
call_site in
if is_owned actual_access_path astate . attribute_map
begin
then
match AccessPath . of_lhs_exp actual_exp actual_typ ~ f_resolve_id with
(* the actual passed to the current callee is owned. drop all the
| Some actual_access_path ->
conditional accesses for that actual , since they're all safe * )
if is_owned actual_access_path astate . attribute_map
accesses_acc
else
let pre =
if unprotected
then
then
(* the actual passed to the current callee is owned. drop all the
conditional accesses for that actual , since they're all safe * )
accesses_acc
else
let base = fst actual_access_path in
let base = fst actual_access_path in
begin
match FormalMap . get_formal_index base extras with
match FormalMap . get_formal_index base extras with
| Some formal_index ->
| Some formal_index ->
(* the actual passed to the current callee is rooted in a
let pre =
formal * )
if unprotected
AccessPrecondition . ProtectedIf ( Some formal_index )
then AccessPrecondition . ProtectedIf ( Some formal_index )
| None ->
else AccessPrecondition . Protected in
match
(* the actual passed to the current callee is rooted in a
AttributeMapDomain . get_conditional_ownership_index
formal . add to conditional accesses * )
actual_access_path
PathDomain . Sinks . fold
astate . attribute_map
( AccessDomain . add_access pre )
with
( PathDomain . sinks callee_conditional_accesses )
| Some formal_index ->
accesses_acc
(* access path conditionally owned if [formal_index] is
| None ->
owned * )
begin
AccessPrecondition . ProtectedIf ( Some formal_index )
match
| None ->
AttributeMapDomain . get_conditional_ownership_index
(* access path not rooted in a formal and not
actual_access_path
conditionally owned * )
astate . attribute_map
AccessPrecondition . unprotected
with
else
| ( Some formal_index ) ->
(* access protected by held lock *)
let pre =
AccessPrecondition . Protected in
if unprotected
update_caller_accesses pre ownership_accesses accesses_acc
then
| None ->
AccessPrecondition . ProtectedIf ( Some formal_index )
(* couldn't find access path, don't know if it's owned *)
else
update_caller_accesses
AccessPrecondition . Protected in
AccessPrecondition . unprotected ownership_accesses accesses_acc in
(* access path conditionally owned, add to protected
let accesses =
accesses if lock held , protected - if accesses
let update_accesses pre callee_accesses accesses_acc = match pre with
otherwise * )
| AccessPrecondition . Protected ->
PathDomain . Sinks . fold
update_caller_accesses pre callee_accesses accesses_acc
( AccessDomain . add_access pre )
| AccessPrecondition . ProtectedIf None ->
( PathDomain . sinks callee_conditional_accesses )
let pre' =
accesses_acc
if unprotected
| None ->
then pre
(* access path not owned and not rooted in a formal.
else AccessPrecondition . Protected in
add to protected accesses if lock held , unprotected
update_caller_accesses pre' callee_accesses accesses_acc
accesses otherwise * )
| AccessPrecondition . ProtectedIf ( Some index ) ->
let pre =
add_ownership_access
if unprotected
callee_accesses ( List . nth_exn actuals index ) accesses_acc in
then AccessPrecondition . unprotected
AccessDomain . fold update_accesses callee_accesses astate . accesses in
else AccessPrecondition . Protected in
PathDomain . Sinks . fold
( AccessDomain . add_access pre )
( PathDomain . sinks callee_conditional_accesses )
accesses_acc
end
end
| None ->
PathDomain . Sinks . fold
( AccessDomain . add_access AccessPrecondition . unprotected )
( PathDomain . sinks callee_conditional_accesses )
accesses_acc
end in
let combined_safe_accesses =
combine_accesses_for_pre
AccessPrecondition . Protected
~ caller_accesses : astate . accesses
~ callee_accesses in
let unsafe_accesses =
if unprotected
then
combine_accesses_for_pre
AccessPrecondition . unprotected
~ caller_accesses : combined_safe_accesses
~ callee_accesses
else
(* add callee unsafe accesses to caller safe accesses *)
let combined_accesses =
PathDomain . with_callsite
( AccessDomain . get_accesses
AccessPrecondition . unprotected callee_accesses ) call_site
| > PathDomain . join
( AccessDomain . get_accesses
AccessPrecondition . Protected combined_safe_accesses ) in
AccessDomain . add
AccessPrecondition . Protected combined_accesses combined_safe_accesses in
let accesses =
List . foldi ~ f : add_conditional_accesses ~ init : unsafe_accesses actuals in
{ astate with accesses ; } in
let attribute_map =
let attribute_map =
propagate_return_attributes
propagate_return_attributes
ret_opt
ret_opt
@ -580,7 +536,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
astate . attribute_map
astate . attribute_map
~ f_resolve_id
~ f_resolve_id
extras in
extras in
{ astate ' with locks = locks' ; threads = threads' ; attribute_map ; }
{ astate with locks ; threads ; accesses ; attribute_map ; }
| None ->
| None ->
if is_box callee_pname
if is_box callee_pname
then
then