[topl] Simple error reporting.

Reviewed By: jvillard

Differential Revision: D15875271

fbshipit-source-id: 148206be9

infer/man/man1/infer-full.txt

@@ -453,6 +453,7 @@ OPTIONS
              TAINTED_BUFFER_ACCESS (enabled by default),
              TAINTED_MEMORY_ALLOCATION (enabled by default),
              THREAD_SAFETY_VIOLATION (enabled by default),
+             TOPL_ERROR (enabled by default),
              UNARY_MINUS_APPLIED_TO_UNSIGNED_EXPRESSION (disabled by
            default),
              UNINITIALIZED_VALUE (enabled by default),

infer/man/man1/infer-report.txt

@@ -193,6 +193,7 @@ OPTIONS
              TAINTED_BUFFER_ACCESS (enabled by default),
              TAINTED_MEMORY_ALLOCATION (enabled by default),
              THREAD_SAFETY_VIOLATION (enabled by default),
+             TOPL_ERROR (enabled by default),
              UNARY_MINUS_APPLIED_TO_UNSIGNED_EXPRESSION (disabled by
            default),
              UNINITIALIZED_VALUE (enabled by default),

infer/man/man1/infer.txt

@@ -453,6 +453,7 @@ OPTIONS
              TAINTED_BUFFER_ACCESS (enabled by default),
              TAINTED_MEMORY_ALLOCATION (enabled by default),
              THREAD_SAFETY_VIOLATION (enabled by default),
+             TOPL_ERROR (enabled by default),
              UNARY_MINUS_APPLIED_TO_UNSIGNED_EXPRESSION (disabled by
            default),
              UNINITIALIZED_VALUE (enabled by default),

infer/src/IR/Exp.ml

@@ -313,6 +313,34 @@ let rec gen_program_vars =
 
 let program_vars e = Sequence.Generator.run (gen_program_vars e)
 
+let rec rename_pvars ~(f : string -> string) : t -> t =
+  let re e = rename_pvars ~f e in
+  let rv v = Pvar.rename ~f v in
+  function
+  | UnOp (op, e, t) ->
+      UnOp (op, re e, t)
+  | BinOp (op, e1, e2) ->
+      BinOp (op, re e1, re e2)
+  | Exn e ->
+      Exn (re e)
+  | Closure {name; captured_vars} ->
+      let captured_vars = List.map ~f:(function e, v, t -> (re e, rv v, t)) captured_vars in
+      Closure {name; captured_vars}
+  | Cast (t, e) ->
+      Cast (t, re e)
+  | Lvar v ->
+      Lvar (rv v)
+  | Lfield (e, fld, t) ->
+      Lfield (re e, fld, t)
+  | Lindex (e1, e2) ->
+      Lindex (re e1, re e2)
+  | Sizeof {typ; nbytes; dynamic_length; subtype} ->
+      let dynamic_length = Option.map ~f:re dynamic_length in
+      Sizeof {typ; nbytes; dynamic_length; subtype}
+  | e (* Should have only cases without subexpressions. *) ->
+      e
+
+
 let zero_of_type typ =
   match typ.Typ.desc with
   | Typ.Tint _ ->

infer/src/IR/Exp.mli

@@ -130,6 +130,10 @@ val ident_mem : t -> Ident.t -> bool
 val program_vars : t -> Pvar.t Sequence.t
 (** all the program variables appearing in the expression *)
 
+val rename_pvars : f:(string -> string) -> t -> t
+(** Rename all Pvars according to the function [f]. WARNING: You want to rename pvars before you
+combine expressions from different symbolic states, which you RARELY want to.*)
+
 val fold_captured : f:('a -> t -> 'a) -> t -> 'a -> 'a
 (** Fold over the expressions captured by this expression. *)
 

infer/src/IR/Mangled.ml

@@ -42,6 +42,11 @@ let self = from_string "self"
 
 let is_self = function {plain= "self"} -> true | _ -> false
 
+let rename ~f {plain; mangled} =
+  let plain = f plain in
+  let mangled = Option.map ~f mangled in
+  {plain; mangled}
+
 module Set = Caml.Set.Make (struct
   type nonrec t = t
 

infer/src/IR/Mangled.mli

@@ -39,6 +39,9 @@ val self : t [@@warning "-32"]
 
 val is_self : t -> bool
 
+val rename : f:(string -> string) -> t -> t
+(** Maps over both the plain and the mangled components. *)
+
 (** Set of Mangled. *)
 module Set : Caml.Set.S with type elt = t
 

infer/src/IR/Pvar.ml

@@ -281,3 +281,9 @@ let get_initializer_pname {pv_name; pv_kind} =
       else Some (Typ.Procname.from_string_c_fun name)
   | _ ->
       None
+
+
+let rename ~f {pv_name; pv_kind} =
+  let pv_name = Mangled.rename ~f pv_name in
+  let pv_hash = name_hash pv_name in
+  {pv_hash; pv_name; pv_kind}

infer/src/IR/Pvar.mli

@@ -152,3 +152,5 @@ val get_name_of_local_with_procname : t -> Mangled.t
 var and the name of the procname in case of locals *)
 
 val materialized_cpp_temporary : string
+
+val rename : f:(string -> string) -> t -> t

infer/src/IR/Typ.ml

@@ -1436,7 +1436,6 @@ module Fieldname = struct
     | _ ->
         None
 
-
   module Clang = struct
     let from_class_name class_name field_name = Clang {class_name; field_name}
   end

infer/src/backend/ondemand.ml

@@ -231,7 +231,9 @@ let analyze_proc ?caller_pdesc callee_pdesc =
     in
     current_taskbar_status := Some (t0, status) ;
     !ProcessPoolState.update_status t0 status ;
-    callbacks.analyze_ondemand summary pdesc
+    let summary = callbacks.analyze_ondemand summary pdesc in
+    if Topl.is_active () then Topl.add_errors callbacks.exe_env summary ;
+    summary
   in
   Some (run_proc_analysis analyze_proc ~caller_pdesc callee_pdesc)
 

infer/src/base/IssueType.ml

@@ -415,6 +415,8 @@ let complexity_increase ~kind ~is_on_cold_start =
   from_cost_string ~kind ~is_on_cold_start "%s_COMPLEXITY_INCREASE"
 
 
+let topl_error = from_string "TOPL_ERROR"
+
 let unary_minus_applied_to_unsigned_expression =
   from_string ~enabled:false "UNARY_MINUS_APPLIED_TO_UNSIGNED_EXPRESSION"
 

infer/src/base/IssueType.mli

@@ -293,6 +293,8 @@ val tainted_memory_allocation : t
 
 val thread_safety_violation : t
 
+val topl_error : t
+
 val unary_minus_applied_to_unsigned_expression : t
 
 val uninitialized_value : t

infer/src/topl/Topl.ml

@@ -154,7 +154,127 @@ let instrument tenv procdesc =
     let f _node = instrument_instruction in
     tt "instrument\n" ;
     let _updated = Procdesc.replace_instrs_by procdesc ~f in
-    tt "add types %d\n" !max_args ; add_types tenv ; tt "done\n" )
+    tt "add types %d@\n" !max_args ; add_types tenv ; tt "done@\n" )
+
+
+(** [lookup_static_var var prop] expects [var] to have the form [Exp.Lfield (obj, fieldname)],
+and looks up inside the spatial part of [prop]. This function is currently used only to get
+around some limitations:
+  (a) one cannot do boolean-conjunction on symbolic heaps; and
+  (b) the prover fails to see that 0!=o.f * o|-f->0 is inconsistent
+*)
+let lookup_static_var env (var : Exp.t) (prop : 'a Prop.t) : Exp.t option =
+  let from_strexp = function Sil.Eexp (e, _) -> Some e | _ -> None in
+  let get_field field (f, e) = if Typ.Fieldname.equal field f then from_strexp e else None in
+  let get_strexp field = function
+    | Sil.Estruct (fs, _inst) ->
+        List.find_map ~f:(get_field field) fs
+    | _ ->
+        None
+  in
+  let get_hpred obj field = function
+    | Sil.Hpointsto (obj', se, _typ) when Exp.equal obj obj' ->
+        get_strexp field se
+    | _ ->
+        None
+  in
+  match var with
+  | Exp.Lfield (obj, field, _typ) ->
+      let iter = Prop.prop_iter_create prop in
+      let iter = Option.bind ~f:(fun x -> Prop.prop_iter_find x (get_hpred obj field)) iter in
+      let state = Option.map ~f:(Prop.prop_iter_current env) iter in
+      Option.map ~f:snd state
+  | _ ->
+      None
+
+
+let is_inconsistent env query =
+  tt "ask if inconsistent: %a@\n" (Prop.pp_prop Pp.text) query ;
+  let prover_result = Prover.check_inconsistency_base env query in
+  tt "prover_result = %b@\n" prover_result ;
+  prover_result
+
+
+let conjoin_props env post pre =
+  (* PRE: p and q have no footprints: that would make no sense in pre/posts. *)
+  (* TODO: Ideally, this should be boolean-conjunction. The function [Dom.prop_partial_meet]
+    comes close but fails in all practical cases. *)
+  List.fold ~init:post ~f:(Prop.prop_atom_and env) (Prop.get_pure pre)
+
+
+(**
+For each (pre, post) pair of symbolic heaps and each (start, error) pair of Topl automata states,
+define
+  φ := pre & post & (state_pre==start)
+  ψ := φ & (state_post!=error)
+where & stands for boolean conjunction, in pre all program variables get suffix "_pre", and in post
+all program variables get suffix "_post".
+
+Warn when φ is consistent and ψ is inconsistent. (TODO: experiment with asking if it is not forced
+but *possible* to get to error.)
+
+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 exe_env summary =
+  let proc_desc = summary.Summary.proc_desc in
+  let proc_name = Procdesc.get_proc_name proc_desc in
+  if not (ToplUtils.is_synthesized proc_name) then
+    let env = Exe_env.get_tenv exe_env proc_name in
+    let preposts : Prop.normal BiabductionSummary.spec list =
+      let biabduction_summary = summary.Summary.payloads.Payloads.biabduction in
+      let check_phase x =
+        if not BiabductionSummary.(equal_phase x.phase RE_EXECUTION) then
+          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 ;
+      Option.value_map ~default:[] ~f:extract_specs biabduction_summary
+    in
+    let subscript varname sub = Printf.sprintf "%s_%s" varname sub in
+    let subscript_pre varname = subscript varname "pre" in
+    let subscript_post varname = subscript varname "post" in
+    let state_var = ToplUtils.static_var ToplName.state in
+    let handle_preposts BiabductionSummary.{pre; posts} =
+      let pre = BiabductionSummary.Jprop.to_prop pre in
+      tt "PRE = %a@\n" (Prop.pp_prop Pp.text) pre ;
+      let handle_start_error start_pre_value (start, error) =
+        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)
+        in
+        let pre_start = Prop.conjoin_eq env 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)
+            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 property, _vname = ToplAutomaton.vname (Lazy.force automaton) error in
+              let message = Printf.sprintf "property %s reaches error" property in
+              tt "INCONSISTENT (WARN)@\n" ;
+              Reporting.log_error summary IssueType.topl_error ~loc message )
+            else tt "CONSISTENT (do NOT warn)@\n"
+          in
+          (* Don't warn if [lookup_static_var] fails. *)
+          Option.iter ~f:handle_state_post_value (lookup_static_var env state_var post)
+        in
+        List.iter ~f:handle_post posts
+      in
+      let start_error_pairs = ToplAutomaton.get_start_error_pairs (Lazy.force automaton) in
+      let handle_state_pre_value state_pre_value =
+        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)
+    in
+    List.iter ~f:handle_preposts preposts
 
 
 let sourcefile = ToplMonitor.sourcefile

infer/src/topl/Topl.mli

@@ -20,6 +20,9 @@ val instrument : Tenv.t -> Procdesc.t -> unit
 (** Inserts calls to the TOPL automaton. Mutates the arguments: it is the caller's responsibility
 to instrument procedures at most once. *)
 
+val add_errors : Exe_env.t -> Summary.t -> unit
+(** Adds error using {!Reporting}. *)
+
 val sourcefile : SourceFile.t
 (** The (fake) sourcefile in which synthesized code resides. *)
 

infer/src/topl/ToplAutomaton.ml

@@ -57,7 +57,7 @@ let make properties =
   let transitions : transition array =
     let f p =
       let prefix_pname pname =
-        "^\\(\\|" ^ String.concat ~sep:"\\|" p.ToplAst.prefixes ^ "\\)\\." ^ pname ^ "()$"
+        "^\\(\\|" ^ String.concat ~sep:"\\|" p.ToplAst.prefixes ^ "\\)\\." ^ pname ^ "("
       in
       let f t =
         let source = vindex ToplAst.(p.name, t.source) in
@@ -88,6 +88,8 @@ let make properties =
 
 let outgoing a i = a.outgoing.(i)
 
+let vname a i = a.states.(i)
+
 let vcount a = Array.length a.states
 
 let transition a i = a.transitions.(i)
@@ -95,3 +97,15 @@ let transition a i = a.transitions.(i)
 let tcount a = Array.length a.transitions
 
 let max_args a = a.max_args
+
+let get_start_error_pairs a =
+  let starts = String.Table.create () ~size:(2 * vcount a) in
+  let errors = String.Table.create () ~size:(2 * vcount a) in
+  let record dict keep index (property, name) =
+    if String.equal keep name then Hashtbl.add_exn dict ~key:property ~data:index
+  in
+  Array.iteri ~f:(record starts "start") a.states ;
+  Array.iteri ~f:(record errors "error") a.states ;
+  let f ~key:_ = function `Both (x, y) -> Some (x, y) | _ -> None in
+  let pairs = Hashtbl.merge starts errors ~f in
+  Hashtbl.data pairs

infer/src/topl/ToplAutomaton.mli

@@ -23,6 +23,8 @@ open! IStd
 *)
 type t
 
+type vname = ToplAst.property_name * ToplAst.vertex
+
 type vindex = int (* from 0 to vcount()-1, inclusive *)
 
 type tindex = int (* from 0 to tcount()-1, inclusive *)
@@ -33,6 +35,8 @@ val make : ToplAst.t list -> t
 
 val outgoing : t -> vindex -> tindex list
 
+val vname : t -> vindex -> vname
+
 val vcount : t -> int
 
 val transition : t -> tindex -> transition
@@ -40,3 +44,8 @@ val transition : t -> tindex -> transition
 val tcount : t -> int
 
 val max_args : t -> int
+
+val get_start_error_pairs : t -> (vindex * vindex) list
+(** Returns pairs [(i,j)] of vertex indices corresponding to pairs [((p, "start"), (p, "error"))] of
+vertex names, where [p] ranges over property names.
+POST: no vertex index occurs more than once in the result. *)

infer/src/topl/ToplMonitor.ml

@@ -171,8 +171,6 @@ let gen_maybe_call ret_id : node_generator =
   stmt_node [ToplUtils.topl_call ret_id (Tint IBool) sourcefile_location ToplName.maybe []]
 
 
-let constant (x : int) : Exp.t = Exp.int (IntLit.of_int x)
-
 let arguments_count proc_name = List.length (Typ.Procname.get_parameters proc_name)
 
 (* NOTE: The order of parameters must correspond to what gets generated by [call_save_args]. *)
@@ -264,7 +262,7 @@ let generate_execute_state automaton proc_name =
   in
   let body =
     gen_if
-      (Exp.eq (ToplUtils.static_var ToplName.state) (constant state))
+      (Exp.eq (ToplUtils.static_var ToplName.state) (ToplUtils.constant_int state))
       branch_for_right_state skip
   in
   procedure proc_name body

infer/src/topl/ToplUtils.ml

@@ -40,6 +40,8 @@ let static_var x : Exp.t =
 
 let local_var proc_name x : Exp.t = Exp.Lvar (Pvar.mk (Mangled.from_string x) proc_name)
 
+let constant_int (x : int) : Exp.t = Exp.int (IntLit.of_int x)
+
 let is_synthesized = function
   | Typ.Procname.Java j ->
       String.equal ToplName.topl_property (Typ.Procname.Java.get_class_name j)

infer/src/topl/ToplUtils.mli

@@ -21,6 +21,8 @@ val static_var : string -> Exp.t
 
 val local_var : Typ.Procname.t -> string -> Exp.t
 
+val constant_int : int -> Exp.t
+
 val topl_call :
   Ident.t -> Typ.desc -> Location.t -> string -> (Exp.t * Typ.t) sexp_list -> Sil.instr
 (** Call a TOPL function; that is, a static member of "topl.Property" with java.lang.Object arguments

infer/tests/codetoanalyze/java/topl/Iterators.java

@@ -7,8 +7,28 @@
 import java.util.*;
 
 class Iterators {
-  void hasNextBad_FN(List<Integer> x) {
-    Iterator<Integer> i = x.iterator();
+  void hasNextOk(List<Integer> xs) {
+    Iterator<Integer> i = xs.iterator();
+    if (i.hasNext()) i.next();
+  }
+
+  void hasNextBad(List<Integer> xs) {
+    Iterator<Integer> i = xs.iterator();
+    i.next();
+  }
+
+  void hasNextInterproceduralBad(List<Integer> xs) {
+    getSingleElementOk(xs.iterator());
+  }
+
+  void hasNextInterproceduralOk(List<Integer> xs) {
+    Iterator<Integer> i = xs.iterator();
+    if (i.hasNext()) {
+      getSingleElementOk(i);
+    }
+  }
+
+  void getSingleElementOk(Iterator<Integer> i) {
     i.next();
   }
 }

infer/tests/codetoanalyze/java/topl/Makefile

@@ -5,7 +5,7 @@
 
 TESTS_DIR = ../../..
 
-INFER_OPTIONS = --topl-properties tomcat.topl --topl-properties iterators.topl --biabduction-only
+INFER_OPTIONS = --topl-properties hasnext.topl --biabduction-only
 INFERPRINT_OPTIONS = --issues-tests
 
 SOURCES = $(wildcard *.java)

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

@@ -0,0 +1,8 @@
+property HasNext
+  prefix "Iterator"
+  prefix "List"
+  start -> start: *
+  start -> invalid: I = iterator(*)
+  invalid -> valid: hasNext(i)
+  valid -> invalid: next(i)
+  invalid -> error: next(i)

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

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