[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

@@ -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

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

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

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)] ) }

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= ""}

infer/src/base/Checker.mli

@@ -33,7 +33,8 @@ type t =
   | SIOF
   | SelfInBlock
   | Starvation
-  | TOPL
+  | ToplOnBiabduction
+  | ToplOnPulse
   | Uninit
 [@@deriving equal, enumerate]
 

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

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

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. *)

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))
 )

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)

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)

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)

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
 

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)

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)