From 50b1533921b1ff0fd8d193882fe93d08981cf17f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Wed, 6 Feb 2019 06:20:21 -0800 Subject: [PATCH] [loop-invariance] Make InvariantModels based on ProcName Reviewed By: mbouaziz Differential Revision: D13971492 fbshipit-source-id: c47d6b858 --- infer/src/checkers/hoisting.ml | 4 +++- infer/src/checkers/invariantModels.ml | 6 +++--- infer/src/checkers/loopInvariant.ml | 2 +- infer/src/checkers/purity.ml | 2 +- 4 files changed, 8 insertions(+), 6 deletions(-) diff --git a/infer/src/checkers/hoisting.ml b/infer/src/checkers/hoisting.ml index e4249c1c0..f8311ddce 100644 --- a/infer/src/checkers/hoisting.ml +++ b/infer/src/checkers/hoisting.ml @@ -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 = diff --git a/infer/src/checkers/invariantModels.ml b/infer/src/checkers/invariantModels.ml index 1c5076101..46fbd3a83 100644 --- a/infer/src/checkers/invariantModels.ml +++ b/infer/src/checkers/invariantModels.ml @@ -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)) diff --git a/infer/src/checkers/loopInvariant.ml b/infer/src/checkers/loopInvariant.ml index 40927b26c..f7e10153a 100644 --- a/infer/src/checkers/loopInvariant.ml +++ b/infer/src/checkers/loopInvariant.ml @@ -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 -> ( diff --git a/infer/src/checkers/purity.ml b/infer/src/checkers/purity.ml index b52db7477..710df5618 100644 --- a/infer/src/checkers/purity.ml +++ b/infer/src/checkers/purity.ml @@ -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 -> (