From 9784ee0858e55ff7a5a72020a976e2a992565512 Mon Sep 17 00:00:00 2001 From: Radu Grigore Date: Wed, 29 Jul 2020 05:18:10 -0700 Subject: [PATCH] [topl] Prepare cheap port to pulse. Summary: The old --topl-only is now --topl-biabd-only, and there's also --topl-pulse-only. This is WIP: the latter runs pulse, but it doesn't yet extract Topl errors from pulse summaries. (The citv part of pulse path conditions appears to have the necessary information.) Reviewed By: jvillard Differential Revision: D22815250 fbshipit-source-id: a01792945 --- infer/man/man1/infer-analyze.txt | 25 +++++++--- infer/man/man1/infer-full.txt | 25 +++++++--- infer/man/man1/infer.txt | 25 +++++++--- infer/src/backend/registerCheckers.ml | 10 ++-- infer/src/base/Checker.ml | 16 ++++-- infer/src/base/Checker.mli | 3 +- infer/src/base/IssueType.ml | 4 +- infer/src/topl/Topl.ml | 50 ++++++++++++------- infer/src/topl/Topl.mli | 9 +++- infer/src/topl/dune | 4 +- .../codetoanalyze/java/topl/baos/Makefile | 2 +- .../java/topl/compareArgs/Makefile | 2 +- .../codetoanalyze/java/topl/hasnext/Makefile | 2 +- .../codetoanalyze/java/topl/servlet/Makefile | 2 +- .../codetoanalyze/java/topl/skip/Makefile | 2 +- .../codetoanalyze/java/topl/slowIter/Makefile | 2 +- 16 files changed, 123 insertions(+), 60 deletions(-) diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index 61419b540..401e517d1 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/infer/man/man1/infer-analyze.txt @@ -352,14 +352,23 @@ OPTIONS Activates: Enable starvation and disable all other checkers (Conversely: --no-starvation-only) - --topl - Activates: checker topl: Detects errors based on user-provided - state machines describing multi-object monitors. (Conversely: - --no-topl) - - --topl-only - Activates: Enable topl and disable all other checkers (Conversely: - --no-topl-only) + --topl-biabd + Activates: checker topl-biabd: Detects errors based on + user-provided state machines describing multi-object monitors. + (Conversely: --no-topl-biabd) + + --topl-biabd-only + Activates: Enable topl-biabd and disable all other checkers + (Conversely: --no-topl-biabd-only) + + --topl-pulse + Activates: checker topl-pulse: Detects errors based on + user-provided state machines describing multi-object monitors. + (Conversely: --no-topl-pulse) + + --topl-pulse-only + Activates: Enable topl-pulse and disable all other checkers + (Conversely: --no-topl-pulse-only) --no-uninit Deactivates: checker uninit: Warns when values are used before diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 668de9551..5f092ef7e 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -1114,14 +1114,23 @@ OPTIONS Specify custom annotations that should be considered aliases of @ThreadSafe See also infer-analyze(1). - --topl - Activates: checker topl: Detects errors based on user-provided - state machines describing multi-object monitors. (Conversely: - --no-topl) See also infer-analyze(1). - - --topl-only - Activates: Enable topl and disable all other checkers (Conversely: - --no-topl-only) See also infer-analyze(1). + --topl-biabd + Activates: checker topl-biabd: Detects errors based on + user-provided state machines describing multi-object monitors. + (Conversely: --no-topl-biabd) See also infer-analyze(1). + + --topl-biabd-only + Activates: Enable topl-biabd and disable all other checkers + (Conversely: --no-topl-biabd-only) See also infer-analyze(1). + + --topl-pulse + Activates: checker topl-pulse: Detects errors based on + user-provided state machines describing multi-object monitors. + (Conversely: --no-topl-pulse) See also infer-analyze(1). + + --topl-pulse-only + Activates: Enable topl-pulse and disable all other checkers + (Conversely: --no-topl-pulse-only) See also infer-analyze(1). --no-uninit Deactivates: checker uninit: Warns when values are used before diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index d12f6c0c1..0d317c539 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -1114,14 +1114,23 @@ OPTIONS Specify custom annotations that should be considered aliases of @ThreadSafe See also infer-analyze(1). - --topl - Activates: checker topl: Detects errors based on user-provided - state machines describing multi-object monitors. (Conversely: - --no-topl) See also infer-analyze(1). - - --topl-only - Activates: Enable topl and disable all other checkers (Conversely: - --no-topl-only) See also infer-analyze(1). + --topl-biabd + Activates: checker topl-biabd: Detects errors based on + user-provided state machines describing multi-object monitors. + (Conversely: --no-topl-biabd) See also infer-analyze(1). + + --topl-biabd-only + Activates: Enable topl-biabd and disable all other checkers + (Conversely: --no-topl-biabd-only) See also infer-analyze(1). + + --topl-pulse + Activates: checker topl-pulse: Detects errors based on + user-provided state machines describing multi-object monitors. + (Conversely: --no-topl-pulse) See also infer-analyze(1). + + --topl-pulse-only + Activates: Enable topl-pulse and disable all other checkers + (Conversely: --no-topl-pulse-only) See also infer-analyze(1). --no-uninit Deactivates: checker uninit: Warns when values are used before diff --git a/infer/src/backend/registerCheckers.ml b/infer/src/backend/registerCheckers.ml index 047836036..99e4c25bd 100644 --- a/infer/src/backend/registerCheckers.ml +++ b/infer/src/backend/registerCheckers.ml @@ -134,7 +134,11 @@ let all_checkers = ; (interprocedural Payloads.Fields.quandary ClangTaintAnalysis.checker, Clang) ] } ; { checker= Pulse ; callbacks= - (let pulse = interprocedural Payloads.Fields.pulse Pulse.checker in + (let checker = + if Config.is_checker_enabled ToplOnPulse then Topl.analyze_with_pulse Pulse.checker + else Pulse.checker + in + let pulse = interprocedural Payloads.Fields.pulse checker in [(pulse, Clang); (pulse, Java)] ) } ; { checker= Impurity ; callbacks= @@ -175,8 +179,8 @@ let all_checkers = ; callbacks= (let biabduction = dynamic_dispatch Payloads.Fields.biabduction - ( if Config.is_checker_enabled TOPL then - Topl.instrument_callback Interproc.analyze_procedure + ( if Config.is_checker_enabled ToplOnBiabduction then + Topl.analyze_with_biabduction Interproc.analyze_procedure else Interproc.analyze_procedure ) in [(biabduction, Clang); (biabduction, Java)] ) } diff --git a/infer/src/base/Checker.ml b/infer/src/base/Checker.ml index 97bf7ff35..24a450eb4 100644 --- a/infer/src/base/Checker.ml +++ b/infer/src/base/Checker.ml @@ -34,7 +34,8 @@ type t = | SIOF | SelfInBlock | Starvation - | TOPL + | ToplOnBiabduction + | ToplOnPulse | Uninit [@@deriving equal, enumerate] @@ -366,8 +367,8 @@ let config_unsafe checker = ; cli_flags= Some {deprecated= []; show_in_help= true} ; enabled_by_default= true ; activates= [] } - | TOPL -> - { id= "topl" + | ToplOnBiabduction -> + { id= "topl-biabd" ; kind= UserFacing {title= "TOPL"; markdown_body= ""} ; support= supports_clang_and_java_experimental ; short_documentation= @@ -375,6 +376,15 @@ let config_unsafe checker = ; cli_flags= Some {deprecated= []; show_in_help= true} ; enabled_by_default= false ; activates= [Biabduction] } + | ToplOnPulse -> + { id= "topl-pulse" + ; kind= UserFacing {title= "TOPL"; markdown_body= ""} + ; support= supports_clang_and_java_experimental + ; short_documentation= + "Detects errors based on user-provided state machines describing multi-object monitors." + ; cli_flags= Some {deprecated= []; show_in_help= true} + ; enabled_by_default= false + ; activates= [Pulse] } | Uninit -> { id= "uninit" ; kind= UserFacing {title= "Uninitialized Variable"; markdown_body= ""} diff --git a/infer/src/base/Checker.mli b/infer/src/base/Checker.mli index e5d5bce15..7e8560aae 100644 --- a/infer/src/base/Checker.mli +++ b/infer/src/base/Checker.mli @@ -33,7 +33,8 @@ type t = | SIOF | SelfInBlock | Starvation - | TOPL + | ToplOnBiabduction + | ToplOnPulse | Uninit [@@deriving equal, enumerate] diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 2f5a5caf9..a6a866cb6 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -860,7 +860,9 @@ let complexity_increase ~kind ~is_on_ui_thread = register_cost ~kind ~is_on_ui_thread "%s_COMPLEXITY_INCREASE" -let topl_error = register ~id:"TOPL_ERROR" Error TOPL ~user_documentation:"Experimental." +let topl_error = + register ~id:"TOPL_ERROR" Error ToplOnBiabduction ~user_documentation:"Experimental." + let uninitialized_value = register ~id:"UNINITIALIZED_VALUE" Error Uninit diff --git a/infer/src/topl/Topl.ml b/infer/src/topl/Topl.ml index 42f99b46c..47f56128b 100644 --- a/infer/src/topl/Topl.ml +++ b/infer/src/topl/Topl.ml @@ -172,11 +172,11 @@ let add_types tenv = () -let instrument tenv procdesc = - if not (ToplUtils.is_synthesized (Procdesc.get_proc_name procdesc)) then ( +let instrument {InterproceduralAnalysis.proc_desc; tenv; _} = + if not (ToplUtils.is_synthesized (Procdesc.get_proc_name proc_desc)) then ( let f _node = instrument_instruction in tt "instrument@\n" ; - let _updated = Procdesc.replace_instrs_by procdesc ~f in + let _updated = Procdesc.replace_instrs_by proc_desc ~f in tt "add types@\n" ; add_types tenv ; tt "done@\n" ) @@ -243,7 +243,7 @@ let conjoin_props env post pre = To compute (pre & post) the function [conjoin_props] from above is used, which returns a weaker formula: in particular, the spatial part of pre is dropped. To get around some limitations of the prover we also use [lookup_static_var]; if a call to this function fails, we don't warn. *) -let add_errors env proc_desc err_log biabduction_summary = +let add_errors_biabduction {InterproceduralAnalysis.proc_desc; tenv; err_log} biabduction_summary = let proc_name = Procdesc.get_proc_name proc_desc in if not (ToplUtils.is_synthesized proc_name) then let preposts : Prop.normal BiabductionSummary.spec list = @@ -266,26 +266,27 @@ let add_errors env proc_desc err_log biabduction_summary = let start_exp = Exp.int (IntLit.of_int start) in let error_exp = Exp.int (IntLit.of_int error) in let pre_start = - Prop.normalize env (Prop.prop_expmap (Exp.rename_pvars ~f:subscript_pre) pre) + Prop.normalize tenv (Prop.prop_expmap (Exp.rename_pvars ~f:subscript_pre) pre) in - let pre_start = Prop.conjoin_eq env start_exp start_pre_value pre_start in + let pre_start = Prop.conjoin_eq tenv start_exp start_pre_value pre_start in let handle_post (post, _path (* TODO: use for getting a trace*)) = let handle_state_post_value state_post_value = tt "POST = %a@\n" (Prop.pp_prop Pp.text) post ; let loc = Procdesc.get_loc proc_desc in let post = - Prop.normalize env (Prop.prop_expmap (Exp.rename_pvars ~f:subscript_post) post) + Prop.normalize tenv (Prop.prop_expmap (Exp.rename_pvars ~f:subscript_post) post) in - let phi = conjoin_props env post pre_start in - let psi = Prop.conjoin_neq env error_exp state_post_value phi in - if (not (is_inconsistent env phi)) && is_inconsistent env psi then ( + let phi = conjoin_props tenv post pre_start in + let psi = Prop.conjoin_neq tenv error_exp state_post_value phi in + if (not (is_inconsistent tenv phi)) && is_inconsistent tenv psi then ( let property, _vname = ToplAutomaton.vname (Lazy.force automaton) error in let message = Printf.sprintf "property %s reaches error" property in tt "WARN@\n" ; - Reporting.log_issue proc_desc err_log TOPL IssueType.topl_error ~loc message ) + Reporting.log_issue proc_desc err_log ToplOnBiabduction IssueType.topl_error ~loc + message ) in (* Don't warn if [lookup_static_var] fails. *) - Option.iter ~f:handle_state_post_value (lookup_static_var env state_var post) + Option.iter ~f:handle_state_post_value (lookup_static_var tenv state_var post) in List.iter ~f:handle_post posts in @@ -294,11 +295,16 @@ let add_errors env proc_desc err_log biabduction_summary = List.iter ~f:(handle_start_error state_pre_value) start_error_pairs in (* Don't warn if [lookup_static_var] fails. *) - Option.iter ~f:handle_state_pre_value (lookup_static_var env state_var pre) + Option.iter ~f:handle_state_pre_value (lookup_static_var tenv state_var pre) in List.iter ~f:handle_preposts preposts +let add_errors_pulse _analysis_data _summary = + (* TODO(rgrigore): Do something similar to add_errors_biabduction, but for pulse summaries. *) + () + + let sourcefile () = if not (is_active ()) then L.die InternalError "Called Topl.sourcefile when Topl is inactive" ; ToplMonitor.sourcefile () @@ -309,9 +315,15 @@ let cfg () = ToplMonitor.cfg () -let instrument_callback biabduction - ({InterproceduralAnalysis.proc_desc; tenv; err_log} as analysis_data) = - if is_active () then instrument tenv proc_desc ; - let biabduction_summary = biabduction analysis_data in - if is_active () then add_errors tenv proc_desc err_log biabduction_summary ; - biabduction_summary +let analyze_with analyze postprocess analysis_data = + if is_active () then instrument analysis_data ; + let summary = analyze analysis_data in + if is_active () then postprocess analysis_data summary ; + summary + + +let analyze_with_biabduction biabduction analysis_data = + analyze_with biabduction add_errors_biabduction analysis_data + + +let analyze_with_pulse pulse analysis_data = analyze_with pulse add_errors_pulse analysis_data diff --git a/infer/src/topl/Topl.mli b/infer/src/topl/Topl.mli index 341c13590..26e3de856 100644 --- a/infer/src/topl/Topl.mli +++ b/infer/src/topl/Topl.mli @@ -24,9 +24,16 @@ val cfg : unit -> Cfg.t (** The CFG of the synthesized code. This function has a side-effect, because that's how [Cfg] works, so do NOT call when Topl is inactive.*) -val instrument_callback : +val analyze_with_biabduction : (BiabductionSummary.t InterproceduralAnalysis.t -> BiabductionSummary.t option) -> BiabductionSummary.t InterproceduralAnalysis.t -> BiabductionSummary.t option (** Run biabduction with Topl instrumentation if active. Inserts calls to the TOPL automaton. Mutates the arguments: it is the caller's responsibility to instrument procedures at most once. *) + +val analyze_with_pulse : + (PulseSummary.t InterproceduralAnalysis.t -> PulseSummary.t option) + -> PulseSummary.t InterproceduralAnalysis.t + -> PulseSummary.t option +(** Run pulse with Topl instrumentation if active. Inserts calls to the TOPL automaton. Mutates the + arguments: it is the caller's responsibility to instrument procedures at most once. *) diff --git a/infer/src/topl/dune b/infer/src/topl/dune index 6f74df839..5b235c9c6 100644 --- a/infer/src/topl/dune +++ b/infer/src/topl/dune @@ -12,7 +12,7 @@ (public_name infer.TOPLlib) (flags (:standard -open Core -open IR -open IStdlib -open IStd -open ATDGenerated - -open IBase -open Absint -open Biabduction)) - (libraries core IStdlib ATDGenerated IBase IR Absint Biabduction) + -open IBase -open Absint -open Biabduction -open Pulselib)) + (libraries core IStdlib ATDGenerated IBase IR Absint Biabduction Pulselib) (preprocess (pps ppx_compare ppx_hash ppx_sexp_conv)) ) diff --git a/infer/tests/codetoanalyze/java/topl/baos/Makefile b/infer/tests/codetoanalyze/java/topl/baos/Makefile index 9ecf9d0e5..97a75295d 100644 --- a/infer/tests/codetoanalyze/java/topl/baos/Makefile +++ b/infer/tests/codetoanalyze/java/topl/baos/Makefile @@ -5,7 +5,7 @@ TESTS_DIR = ../../../.. -INFER_OPTIONS = --seconds-per-iteration 100 --symops-per-iteration 13000 --topl-properties baos.topl --topl-only +INFER_OPTIONS = --seconds-per-iteration 100 --symops-per-iteration 13000 --topl-properties baos.topl --topl-biabd-only INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.java) diff --git a/infer/tests/codetoanalyze/java/topl/compareArgs/Makefile b/infer/tests/codetoanalyze/java/topl/compareArgs/Makefile index d4310ee32..7775a698f 100644 --- a/infer/tests/codetoanalyze/java/topl/compareArgs/Makefile +++ b/infer/tests/codetoanalyze/java/topl/compareArgs/Makefile @@ -5,7 +5,7 @@ TESTS_DIR = ../../../.. -INFER_OPTIONS = --seconds-per-iteration 10 --symops-per-iteration 4000 --topl-properties CompareArgs.topl --topl-only +INFER_OPTIONS = --seconds-per-iteration 10 --symops-per-iteration 4000 --topl-properties CompareArgs.topl --topl-biabd-only INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.java) diff --git a/infer/tests/codetoanalyze/java/topl/hasnext/Makefile b/infer/tests/codetoanalyze/java/topl/hasnext/Makefile index 20a3377e6..1c2a9ea6c 100644 --- a/infer/tests/codetoanalyze/java/topl/hasnext/Makefile +++ b/infer/tests/codetoanalyze/java/topl/hasnext/Makefile @@ -5,7 +5,7 @@ TESTS_DIR = ../../../.. -INFER_OPTIONS = --seconds-per-iteration 100 --symops-per-iteration 10000 --topl-properties hasnext.topl --topl-only +INFER_OPTIONS = --seconds-per-iteration 100 --symops-per-iteration 10000 --topl-properties hasnext.topl --topl-biabd-only INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.java) diff --git a/infer/tests/codetoanalyze/java/topl/servlet/Makefile b/infer/tests/codetoanalyze/java/topl/servlet/Makefile index efde7f746..be0119489 100644 --- a/infer/tests/codetoanalyze/java/topl/servlet/Makefile +++ b/infer/tests/codetoanalyze/java/topl/servlet/Makefile @@ -5,7 +5,7 @@ TESTS_DIR = ../../../.. -INFER_OPTIONS = --seconds-per-iteration 20 --symops-per-iteration 60000 --topl-properties servlet.topl --topl-only +INFER_OPTIONS = --seconds-per-iteration 20 --symops-per-iteration 60000 --topl-properties servlet.topl --topl-biabd-only INFERPRINT_OPTIONS = --issues-tests TEST_CLASSPATH = javax.servlet-api-4.0.1.jar diff --git a/infer/tests/codetoanalyze/java/topl/skip/Makefile b/infer/tests/codetoanalyze/java/topl/skip/Makefile index ba90bf5f9..cb5d14635 100644 --- a/infer/tests/codetoanalyze/java/topl/skip/Makefile +++ b/infer/tests/codetoanalyze/java/topl/skip/Makefile @@ -5,7 +5,7 @@ TESTS_DIR = ../../../.. -INFER_OPTIONS = --seconds-per-iteration 100 --symops-per-iteration 100000 --topl-properties SkipAfterRemove.topl --topl-only +INFER_OPTIONS = --seconds-per-iteration 100 --symops-per-iteration 100000 --topl-properties SkipAfterRemove.topl --topl-biabd-only INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.java) diff --git a/infer/tests/codetoanalyze/java/topl/slowIter/Makefile b/infer/tests/codetoanalyze/java/topl/slowIter/Makefile index 168faf803..e68c16dfc 100644 --- a/infer/tests/codetoanalyze/java/topl/slowIter/Makefile +++ b/infer/tests/codetoanalyze/java/topl/slowIter/Makefile @@ -5,7 +5,7 @@ TESTS_DIR = ../../../.. -INFER_OPTIONS = --seconds-per-iteration 10 --symops-per-iteration 20000 --topl-properties slowIter.topl --topl-only +INFER_OPTIONS = --seconds-per-iteration 10 --symops-per-iteration 20000 --topl-properties slowIter.topl --topl-biabd-only INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.java)