[loop-invariance] Make InvariantModels based on ProcName

Reviewed By: mbouaziz

Differential Revision: D13971492

fbshipit-source-id: c47d6b858
master
Ezgi Çiçek 6 years ago committed by Facebook Github Bot
parent 6af46027bf
commit 50b1533921

@ -75,7 +75,9 @@ let do_report summary Call.({pname; loc}) ~issue loop_head_loc =
Reporting.log_error summary ~loc ~ltr issue message
let model_satisfies ~f tenv pname = InvariantModels.Call.dispatch tenv pname [] |> Option.exists ~f
let model_satisfies ~f tenv pname =
InvariantModels.ProcName.dispatch tenv pname |> Option.exists ~f
let get_issue_to_report tenv Call.({pname; node; params}) integer_type_widths inferbo_invariant_map
=

@ -34,9 +34,9 @@ let startsWith prefix _ s = String.is_prefix ~prefix s
(* matches get*Value *)
let getStarValue tenv s = startsWith "get" tenv s && endsWith "Value" tenv s
module Call = struct
let dispatch : (Tenv.t, model) ProcnameDispatcher.Call.dispatcher =
let open ProcnameDispatcher.Call in
module ProcName = struct
let dispatch : (Tenv.t, model) ProcnameDispatcher.ProcName.dispatcher =
let open ProcnameDispatcher.ProcName in
make_dispatcher
[ +invariant_builtins <>--> VariantForHoisting
; +(fun _ name -> BuiltinDecl.is_declared (Typ.Procname.from_string_c_fun name))

@ -26,7 +26,7 @@ let is_defined_outside loop_nodes reaching_defs var =
let get_purity tenv ~is_inv_by_default callee_pname args =
(* Take into account purity behavior of modeled functions *)
let all_params_modified = PurityDomain.all_params_modified args in
match Models.Call.dispatch tenv callee_pname args with
match Models.ProcName.dispatch tenv callee_pname with
| Some inv ->
PurityDomain.with_purity (InvariantModels.is_invariant inv) all_params_modified
| None -> (

@ -149,7 +149,7 @@ module TransferFunctions = struct
(Domain.all_params_modified args))
in
Domain.join astate
( match InvariantModels.Call.dispatch tenv called_pname [] with
( match InvariantModels.ProcName.dispatch tenv called_pname with
| Some inv ->
Domain.with_purity (InvariantModels.is_invariant inv) (Lazy.force matching_modified)
| None -> (

Loading…
Cancel
Save