@ -32,6 +32,18 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
actuals
actuals
let rec get_access_expr ( hilexp : HilExp . t ) =
match hilexp with
| AccessExpression access_exp ->
Some access_exp
| Cast ( _ , hilexp ) | Exception hilexp | UnaryOperator ( _ , hilexp , _ ) ->
get_access_expr hilexp
| BinaryOperator _ | Closure _ | Constant _ | Sizeof _ ->
None
let get_access_expr_list actuals = List . map actuals ~ f : get_access_expr
let do_assume assume_exp ( astate : Domain . t ) =
let do_assume assume_exp ( astate : Domain . t ) =
let open Domain in
let open Domain in
let add_thread_choice ( acc : Domain . t ) bool_value =
let add_thread_choice ( acc : Domain . t ) bool_value =
@ -79,20 +91,17 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| > Option . fold ~ init : astate ~ f : ( Domain . schedule_work loc thread )
| > Option . fold ~ init : astate ~ f : ( Domain . schedule_work loc thread )
in
in
let work_opt =
let work_opt =
match actuals with
match get_access_expr_list actuals with
| HilExp . AccessExpression executor :: HilExp . AccessExpression runnable :: _
| Some executor :: Some runnable :: _ when StarvationModels . schedules_work tenv callee ->
when StarvationModels . schedules_work tenv callee ->
let thread =
let thread =
get_exp_attributes tenv executor astate
get_exp_attributes tenv executor astate
| > Option . bind ~ f : ( function Attribute . WorkScheduler c -> Some c | _ -> None )
| > Option . bind ~ f : ( function Attribute . WorkScheduler c -> Some c | _ -> None )
| > Option . value ~ default : StarvationModels . ForUnknownThread
| > Option . value ~ default : StarvationModels . ForUnknownThread
in
in
Some ( runnable , thread )
Some ( runnable , thread )
| HilExp . AccessExpression runnable :: _
| Some runnable :: _ when StarvationModels . schedules_work_on_ui_thread tenv callee ->
when StarvationModels . schedules_work_on_ui_thread tenv callee ->
Some ( runnable , StarvationModels . ForUIThread )
Some ( runnable , StarvationModels . ForUIThread )
| HilExp . AccessExpression runnable :: _
| Some runnable :: _ when StarvationModels . schedules_work_on_bg_thread tenv callee ->
when StarvationModels . schedules_work_on_bg_thread tenv callee ->
Some ( runnable , StarvationModels . ForNonUIThread )
Some ( runnable , StarvationModels . ForNonUIThread )
| _ ->
| _ ->
None
None
@ -101,9 +110,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let do_assignment tenv lhs_access_exp rhs_exp ( astate : Domain . t ) =
let do_assignment tenv lhs_access_exp rhs_exp ( astate : Domain . t ) =
HilExp . get_access_exprs rhs_exp
get_access_expr rhs_exp
| > List . filter_map ~ f : ( fun exp -> get_exp_attributes tenv exp astate )
| > Option . bind ~ f : ( fun exp -> get_exp_attributes tenv exp astate )
| > List . reduce ~ f : Domain . Attribute . join
| > Option . value_map ~ default : astate ~ f : ( fun attribute ->
| > Option . value_map ~ default : astate ~ f : ( fun attribute ->
let attributes = Domain . AttributeDomain . add lhs_access_exp attribute astate . attributes in
let attributes = Domain . AttributeDomain . add lhs_access_exp attribute astate . attributes in
{ astate with attributes } )
{ astate with attributes } )
@ -113,6 +121,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let open Domain in
let open Domain in
let make_ret_attr return_attribute = { empty_summary with return_attribute } in
let make_ret_attr return_attribute = { empty_summary with return_attribute } in
let make_thread thread = { empty_summary with thread } in
let make_thread thread = { empty_summary with thread } in
let actuals_acc_exps = get_access_expr_list actuals in
let get_returned_executor_summary () =
let get_returned_executor_summary () =
StarvationModels . get_returned_executor ~ attrs_of_pname tenv callee actuals
StarvationModels . get_returned_executor ~ attrs_of_pname tenv callee actuals
| > Option . map ~ f : ( fun thread_constraint -> make_ret_attr ( WorkScheduler thread_constraint ) )
| > Option . map ~ f : ( fun thread_constraint -> make_ret_attr ( WorkScheduler thread_constraint ) )
@ -129,12 +138,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
None
None
in
in
let get_future_is_done_summary () =
let get_future_is_done_summary () =
match actuals with
if StarvationModels . is_future_is_done tenv callee actuals then
| HilExp . AccessExpression future :: _
List . hd actuals_acc_exps | > Option . join
when StarvationModels . is_future_is_done tenv callee actuals ->
| > Option . map ~ f : ( fun future -> make_ret_attr ( FutureDoneGuard future ) )
Some ( make_ret_attr ( FutureDoneGuard future ) )
else None
| _ ->
None
in
in
let get_mainLooper_summary () =
let get_mainLooper_summary () =
if StarvationModels . is_getMainLooper tenv callee actuals then
if StarvationModels . is_getMainLooper tenv callee actuals then
@ -144,10 +151,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let get_callee_summary () = Payload . read ~ caller_summary : summary ~ callee_pname : callee in
let get_callee_summary () = Payload . read ~ caller_summary : summary ~ callee_pname : callee in
let treat_handler_constructor () =
let treat_handler_constructor () =
if StarvationModels . is_handler_constructor tenv callee actuals then
if StarvationModels . is_handler_constructor tenv callee actuals then
match actuals with
match actuals _acc_exps with
| HilExp . AccessExpression receiver :: HilExp . AccessExpression exp :: _ ->
| Some receiver :: Some looper :: _ ->
let constr =
let constr =
AttributeDomain . find_opt exp astate . attributes
AttributeDomain . find_opt looper astate . attributes
| > Option . bind ~ f : ( function Attribute . Looper c -> Some c | _ -> None )
| > Option . bind ~ f : ( function Attribute . Looper c -> Some c | _ -> None )
| > Option . value ~ default : StarvationModels . ForUnknownThread
| > Option . value ~ default : StarvationModels . ForUnknownThread
in
in
@ -161,13 +168,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
in
in
let treat_thread_constructor () =
let treat_thread_constructor () =
if StarvationModels . is_thread_constructor tenv callee actuals then
if StarvationModels . is_thread_constructor tenv callee actuals then
match actuals with
match actuals _acc_exps with
| HilExp . AccessExpression receiver :: rest ->
| Some receiver :: rest ->
( match rest with
( match rest with
| HilExp . AccessExpression exp1 :: HilExp . AccessExpression exp2 :: _ ->
| Some exp1 :: Some exp2 :: _ ->
(* two additional arguments, either could be a runnable, see docs *)
(* two additional arguments, either could be a runnable, see docs *)
[ exp1 ; exp2 ]
[ exp1 ; exp2 ]
| HilExp . AccessExpression runnable :: _ ->
| Some runnable :: _ ->
(* either just one argument, or more but 2nd is not an access expression *)
(* either just one argument, or more but 2nd is not an access expression *)
[ runnable ]
[ runnable ]
| _ ->
| _ ->