[topl] Cheap port to Pulse.

Summary:
Report errors found by running Topl on top of Pulse, when using
--topl-pulse. Topl tests now run on top of Pulse.

Reviewed By: jvillard

Differential Revision: D23030771

fbshipit-source-id: 8770c2902

infer/man/man1/infer-full.txt

@@ -495,7 +495,8 @@ OPTIONS
              STRONG_SELF_NOT_CHECKED (enabled by default),
              Symexec_memory_error (enabled by default),
              THREAD_SAFETY_VIOLATION (enabled by default),
-             TOPL_ERROR (enabled by default),
+             TOPL_BIABD_ERROR (enabled by default),
+             TOPL_PULSE_ERROR (enabled by default),
              UNINITIALIZED_VALUE (enabled by default),
              UNREACHABLE_CODE (enabled by default),
              UNTRUSTED_BUFFER_ACCESS (disabled by default),

infer/man/man1/infer-report.txt

@@ -214,7 +214,8 @@ OPTIONS
              STRONG_SELF_NOT_CHECKED (enabled by default),
              Symexec_memory_error (enabled by default),
              THREAD_SAFETY_VIOLATION (enabled by default),
-             TOPL_ERROR (enabled by default),
+             TOPL_BIABD_ERROR (enabled by default),
+             TOPL_PULSE_ERROR (enabled by default),
              UNINITIALIZED_VALUE (enabled by default),
              UNREACHABLE_CODE (enabled by default),
              UNTRUSTED_BUFFER_ACCESS (disabled by default),

infer/man/man1/infer.txt

@@ -495,7 +495,8 @@ OPTIONS
              STRONG_SELF_NOT_CHECKED (enabled by default),
              Symexec_memory_error (enabled by default),
              THREAD_SAFETY_VIOLATION (enabled by default),
-             TOPL_ERROR (enabled by default),
+             TOPL_BIABD_ERROR (enabled by default),
+             TOPL_PULSE_ERROR (enabled by default),
              UNINITIALIZED_VALUE (enabled by default),
              UNREACHABLE_CODE (enabled by default),
              UNTRUSTED_BUFFER_ACCESS (disabled by default),

infer/src/base/IssueType.ml

@@ -860,8 +860,12 @@ let complexity_increase ~kind ~is_on_ui_thread =
   register_cost ~kind ~is_on_ui_thread "%s_COMPLEXITY_INCREASE"
 
 
-let topl_error =
+let topl_biabd_error =
-  register ~id:"TOPL_ERROR" Error ToplOnBiabduction ~user_documentation:"Experimental."
+  register ~id:"TOPL_BIABD_ERROR" Error ToplOnBiabduction ~user_documentation:"Experimental."
+
+
+let topl_pulse_error =
+  register ~id:"TOPL_PULSE_ERROR" Error ToplOnPulse ~user_documentation:"Experimental."
 
 
 let uninitialized_value =

infer/src/base/IssueType.mli

@@ -308,7 +308,9 @@ val symexec_memory_error : t
 
 val thread_safety_violation : t
 
-val topl_error : t
+val topl_biabd_error : t
+
+val topl_pulse_error : t
 
 val uninitialized_value : t
 

infer/src/pulse/PulseCItv.ml

@@ -174,6 +174,8 @@ let is_equal_to_zero = function
       false
 
 
+let as_int = function Between (Int l, Int u) when IntLit.eq l u -> IntLit.to_int l | _ -> None
+
 let has_empty_intersection a1 a2 =
   match (a1, a2) with
   | Outside _, Outside _ ->

infer/src/pulse/PulseCItv.mli

@@ -15,6 +15,9 @@ val equal_to : IntLit.t -> t
 
 val is_equal_to_zero : t -> bool
 
+val as_int : t -> int option
+(** [as_int v] returns [Some x] if [v] is known to be [x] *)
+
 val pp : F.formatter -> t -> unit
 
 type abduction_result =

infer/src/pulse/PulseFormula.ml

@@ -1383,3 +1383,10 @@ let simplify ~keep phi =
 let is_known_zero phi v =
   Var.Map.find_opt (VarUF.find phi.var_eqs v :> Var.t) phi.linear_eqs
   |> Option.exists ~f:LinArith.is_zero
+
+
+let as_int phi v =
+  let maybe_int q = if Z.equal (Q.den q) Z.one then Q.to_int q else None in
+  let open Option.Monad_infix in
+  Var.Map.find_opt (VarUF.find phi.var_eqs v :> Var.t) phi.linear_eqs
+  >>= LinArith.get_as_const >>= maybe_int

infer/src/pulse/PulseFormula.mli

@@ -56,6 +56,8 @@ val and_fold_subst_variables :
 
 val is_known_zero : t -> Var.t -> bool
 
+val as_int : t -> Var.t -> int option
+
 (** {3 Notations} *)
 
 include sig

infer/src/pulse/PulsePathCondition.ml

@@ -378,3 +378,10 @@ let is_unsat_expensive phi =
         (false_, true)
     | Sat formula ->
         ({phi with formula}, false)
+
+
+let as_int phi v =
+  (* TODO(rgrigore): Ask BoItvs too. *)
+  IList.force_until_first_some
+    [ lazy (CItvs.find_opt v phi.citvs |> Option.value_map ~default:None ~f:CItv.as_int)
+    ; lazy (Formula.as_int phi.formula v) ]

infer/src/pulse/PulsePathCondition.mli

@@ -57,3 +57,7 @@ val is_unsat_cheap : t -> bool
 
 val is_unsat_expensive : t -> t * bool
 (** whether the state contains a contradiction, only call this when you absolutely have to *)
+
+val as_int : t -> AbstractValue.t -> int option
+(** [as_int phi t] returns an integer x such that [phi |- t = x], if known for sure; see also
+    [is_known_zero] *)

infer/src/topl/Topl.ml

@@ -227,6 +227,11 @@ let conjoin_props env post pre =
   List.fold ~init:post ~f:(Prop.prop_atom_and env) (Prop.get_pure pre)
 
 
+let message_of_state state =
+  let property, _vname = ToplAutomaton.vname (Lazy.force automaton) state in
+  Printf.sprintf "property %s reaches error" property
+
+
 (** For each (pre, post) pair of symbolic heaps and each (start, error) pair of Topl automata
     states, define
 
@@ -252,8 +257,8 @@ let add_errors_biabduction {InterproceduralAnalysis.proc_desc; tenv; err_log} bi
           L.die InternalError "Topl.add_errors should only be called after RE_EXECUTION"
       in
       let extract_specs x = BiabductionSummary.(normalized_specs_to_specs x.preposts) in
-      Option.iter ~f:check_phase biabduction_summary ;
+      check_phase biabduction_summary ;
-      Option.value_map ~default:[] ~f:extract_specs biabduction_summary
+      extract_specs biabduction_summary
     in
     let subscript varname sub = Printf.sprintf "%s_%s" varname sub in
     let subscript_pre varname = subscript varname "pre" in
@@ -279,11 +284,10 @@ let add_errors_biabduction {InterproceduralAnalysis.proc_desc; tenv; err_log} bi
             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 = message_of_state error in
-              let message = Printf.sprintf "property %s reaches error" property in
               tt "WARN@\n" ;
-              Reporting.log_issue proc_desc err_log ToplOnBiabduction IssueType.topl_error ~loc
+              Reporting.log_issue proc_desc err_log ToplOnBiabduction IssueType.topl_biabd_error
-                message )
+                ~loc message )
           in
           (* Don't warn if [lookup_static_var] fails. *)
           Option.iter ~f:handle_state_post_value (lookup_static_var tenv state_var post)
@@ -300,9 +304,48 @@ let add_errors_biabduction {InterproceduralAnalysis.proc_desc; tenv; err_log} bi
     List.iter ~f:handle_preposts preposts
 
 
-let add_errors_pulse _analysis_data _summary =
+let add_errors_pulse {InterproceduralAnalysis.proc_desc; err_log} pulse_summary =
-  (* TODO(rgrigore): Do something similar to add_errors_biabduction, but for pulse summaries. *)
+  let pulse_summary =
-  ()
+    let f = function PulseExecutionDomain.ContinueProgram s -> Some s | _ -> None in
+    List.filter_map ~f pulse_summary
+  in
+  let proc_name = Procdesc.get_proc_name proc_desc in
+  if not (ToplUtils.is_synthesized proc_name) then
+    let start_to_error =
+      Lazy.force automaton |> ToplAutomaton.get_start_error_pairs |> Int.Table.of_alist_exn
+    in
+    let topl_property_var = Var.of_pvar ToplUtils.topl_class_pvar in
+    let topl_state_field = HilExp.Access.FieldAccess (ToplUtils.make_field ToplName.state) in
+    let check_pre_post pre_post =
+      let open IOption.Let_syntax in
+      let path_condition = pre_post.PulseAbductiveDomain.path_condition in
+      let get_topl_state_opt pulse_state =
+        let stack = pulse_state.PulseBaseDomain.stack in
+        let heap = pulse_state.PulseBaseDomain.heap in
+        let* topl_property_addr, _ = PulseBaseStack.find_opt topl_property_var stack in
+        let* state_addr, _ =
+          PulseBaseMemory.find_edge_opt topl_property_addr topl_state_field heap
+        in
+        let* state_val, _ =
+          PulseBaseMemory.find_edge_opt state_addr HilExp.Access.Dereference heap
+        in
+        PulsePathCondition.as_int path_condition state_val
+      in
+      let* pre_topl = get_topl_state_opt (pre_post.PulseAbductiveDomain.pre :> PulseBaseDomain.t) in
+      let* post_topl =
+        get_topl_state_opt (pre_post.PulseAbductiveDomain.post :> PulseBaseDomain.t)
+      in
+      let* error_topl = Int.Table.find start_to_error pre_topl in
+      if Int.equal post_topl error_topl then Some error_topl else None
+    in
+    let errors = List.filter_map ~f:check_pre_post pulse_summary in
+    let errors = Int.Set.to_list (Int.Set.of_list errors) in
+    let loc = Procdesc.get_loc proc_desc in
+    let report error_state =
+      let m = message_of_state error_state in
+      Reporting.log_issue proc_desc err_log ToplOnPulse IssueType.topl_pulse_error ~loc m
+    in
+    List.iter ~f:report errors
 
 
 let sourcefile () =
@@ -318,7 +361,7 @@ let cfg () =
 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 ;
+  if is_active () then Option.iter ~f:(postprocess analysis_data) summary ;
   summary
 
 

infer/src/topl/ToplUtils.ml

@@ -28,12 +28,13 @@ let topl_call ret_id (ret_typ : Typ.desc) loc method_name arg_ts : Sil.instr =
   Sil.Call ((ret_id, Typ.mk ret_typ), e_fun, arg_ts, loc, CallFlags.default)
 
 
-let topl_class_exp =
+let topl_class_pvar =
   let class_name = Mangled.from_string ToplName.topl_property in
-  let var_name = Pvar.mk_global class_name in
+  Pvar.mk_global class_name
-  Exp.Lvar var_name
 
 
+let topl_class_exp = Exp.Lvar topl_class_pvar
+
 let make_field field_name =
   Fieldname.make (Typ.Name.Java.from_string ToplName.topl_property) field_name
 

infer/src/topl/ToplUtils.mli

@@ -17,6 +17,8 @@ val topl_class_name : Typ.Name.t
 
 val topl_class_typ : Typ.t
 
+val topl_class_pvar : Pvar.t
+
 val static_var : string -> Exp.t
 
 val local_var : Procname.t -> string -> Exp.t

infer/tests/codetoanalyze/java/topl/Makefile

@@ -5,7 +5,7 @@
 
 TESTS_DIR = ../../..
 
-SUBDIRS = baos compareArgs hasnext skip servlet
+SUBDIRS = baos compareArgs hasnext skip servlet slowIter
 
 test-%:
 	$(MAKE) -C $* test

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-biabd-only
+INFER_OPTIONS = --pulse-max-disjuncts 400 --topl-properties baos.topl --topl-pulse-only
 INFERPRINT_OPTIONS = --issues-tests
 
 SOURCES = $(wildcard *.java)

infer/tests/codetoanalyze/java/topl/baos/issues.exp

@@ -1,5 +1,5 @@
-codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.FP_dOk(byte[]):byte[], 0, TOPL_ERROR, no_bucket, ERROR, []
+codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.FP_dOk(byte[]):byte[], 0, TOPL_PULSE_ERROR, no_bucket, ERROR, []
-codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.FP_eOk(byte[]):byte[], 0, TOPL_ERROR, no_bucket, ERROR, []
+codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.FP_eOk(byte[]):byte[], 0, TOPL_PULSE_ERROR, no_bucket, ERROR, []
-codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.aBad():void, 0, TOPL_ERROR, no_bucket, ERROR, []
+codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.aBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, []
-codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.bBad():void, 0, TOPL_ERROR, no_bucket, ERROR, []
+codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.bBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, []
-codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.cBad():void, 0, TOPL_ERROR, no_bucket, ERROR, []
+codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.cBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, []

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-biabd-only
+INFER_OPTIONS = --pulse-max-disjuncts 50 --topl-properties CompareArgs.topl --topl-pulse-only
 INFERPRINT_OPTIONS = --issues-tests
 
 SOURCES = $(wildcard *.java)

infer/tests/codetoanalyze/java/topl/compareArgs/issues.exp

@@ -1,2 +1,2 @@
-codetoanalyze/java/topl/compareArgs/CompareArgs.java, CompareArgs.aBad():void, 0, TOPL_ERROR, no_bucket, ERROR, []
+codetoanalyze/java/topl/compareArgs/CompareArgs.java, CompareArgs.aBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, []
-codetoanalyze/java/topl/compareArgs/CompareArgs.java, CompareArgs.cBad():void, 0, TOPL_ERROR, no_bucket, ERROR, []
+codetoanalyze/java/topl/compareArgs/CompareArgs.java, CompareArgs.cBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, []

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-biabd-only
+INFER_OPTIONS = --pulse-max-disjuncts 50 --topl-properties hasnext.topl --topl-pulse-only
 INFERPRINT_OPTIONS = --issues-tests
 
 SOURCES = $(wildcard *.java)

infer/tests/codetoanalyze/java/topl/hasnext/issues.exp

@@ -1,3 +1,3 @@
-codetoanalyze/java/topl/hasnext/Iterators.java, Iterators.hasNextBad(java.util.List):void, 0, TOPL_ERROR, no_bucket, ERROR, []
+codetoanalyze/java/topl/hasnext/Iterators.java, Iterators.hasNextBad(java.util.List):void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, []
-codetoanalyze/java/topl/hasnext/Iterators.java, Iterators.hasNextInterproceduralBad(java.util.List):void, 0, TOPL_ERROR, no_bucket, ERROR, []
+codetoanalyze/java/topl/hasnext/Iterators.java, Iterators.hasNextInterproceduralBad(java.util.List):void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, []
-codetoanalyze/java/topl/hasnext/ScannerFail.java, ScannerFail.readBad():void, 0, TOPL_ERROR, no_bucket, ERROR, []
+codetoanalyze/java/topl/hasnext/ScannerFail.java, ScannerFail.readBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, []

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-biabd-only
+INFER_OPTIONS = --pulse-max-disjuncts 100 --topl-properties servlet.topl --topl-pulse-only
 INFERPRINT_OPTIONS = --issues-tests
 TEST_CLASSPATH = javax.servlet-api-4.0.1.jar
 

infer/tests/codetoanalyze/java/topl/servlet/issues.exp

@@ -1,3 +1,3 @@
-codetoanalyze/java/topl/servlet/ServletTests.java, ServletTests.aBad(javax.servlet.ServletResponse):void, 0, TOPL_ERROR, no_bucket, ERROR, []
+codetoanalyze/java/topl/servlet/ServletTests.java, ServletTests.aBad(javax.servlet.ServletResponse):void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, []
-codetoanalyze/java/topl/servlet/ServletTests.java, ServletTests.bBad(javax.servlet.ServletResponse):void, 0, TOPL_ERROR, no_bucket, ERROR, []
+codetoanalyze/java/topl/servlet/ServletTests.java, ServletTests.bBad(javax.servlet.ServletResponse):void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, []
-codetoanalyze/java/topl/servlet/ServletTests.java, ServletTests.cBad(javax.servlet.ServletRequest,javax.servlet.ServletResponse,javax.servlet.RequestDispatcher):void, 0, TOPL_ERROR, no_bucket, ERROR, []
+codetoanalyze/java/topl/servlet/ServletTests.java, ServletTests.cBad(javax.servlet.ServletRequest,javax.servlet.ServletResponse,javax.servlet.RequestDispatcher):void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, []

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-biabd-only
+INFER_OPTIONS = --pulse-max-disjuncts 1500 --topl-properties slowIter.topl --topl-pulse-only
 INFERPRINT_OPTIONS = --issues-tests
 
 SOURCES = $(wildcard *.java)

infer/tests/codetoanalyze/java/topl/slowIter/SlowIterTests.java

@@ -8,8 +8,7 @@
 import java.util.Map;
 
 class SlowIterTests {
-  // T62611635
+  static <K, V> void aBad(Map<K, V> m) {
-  static <K, V> void FN_aBad(Map<K, V> m) {
     for (K k : m.keySet()) {
       System.out.printf("%s -> %s\n", k, m.get(k));
     }
@@ -22,7 +21,7 @@ class SlowIterTests {
   }
 
   // Inter-procedural variant of aBad.
-  static <K, V> void FN_bBad(Map<K, V> m) {
+  static <K, V> void bBad(Map<K, V> m) {
     for (K k : m.keySet()) {
       print(k, m);
     }

infer/tests/codetoanalyze/java/topl/slowIter/issues.exp

@@ -0,0 +1,2 @@
+codetoanalyze/java/topl/slowIter/SlowIterTests.java, SlowIterTests.aBad(java.util.Map):void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, []
+codetoanalyze/java/topl/slowIter/SlowIterTests.java, SlowIterTests.bBad(java.util.Map):void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, []