diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index e280480a6..1554d63b3 100644 --- a/infer/man/man1/infer-full.txt +++ b/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), diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt index 8c859da50..c501217fd 100644 --- a/infer/man/man1/infer-report.txt +++ b/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), diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 308e620f4..d0a8e75a2 100644 --- a/infer/man/man1/infer.txt +++ b/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), diff --git a/infer/src/IR/Exp.ml b/infer/src/IR/Exp.ml index 83f4a54a5..495eac6f8 100644 --- a/infer/src/IR/Exp.ml +++ b/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 _ -> diff --git a/infer/src/IR/Exp.mli b/infer/src/IR/Exp.mli index 6bf88b335..f022aa6c4 100644 --- a/infer/src/IR/Exp.mli +++ b/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. *) diff --git a/infer/src/IR/Mangled.ml b/infer/src/IR/Mangled.ml index 758fc6ffb..e212f596c 100644 --- a/infer/src/IR/Mangled.ml +++ b/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 diff --git a/infer/src/IR/Mangled.mli b/infer/src/IR/Mangled.mli index da7b629e5..994657d6a 100644 --- a/infer/src/IR/Mangled.mli +++ b/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 diff --git a/infer/src/IR/Pvar.ml b/infer/src/IR/Pvar.ml index 4d7464a50..89156131a 100644 --- a/infer/src/IR/Pvar.ml +++ b/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} diff --git a/infer/src/IR/Pvar.mli b/infer/src/IR/Pvar.mli index da389cdad..b8937e646 100644 --- a/infer/src/IR/Pvar.mli +++ b/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 diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml index 07cd36b23..762c1af36 100644 --- a/infer/src/IR/Typ.ml +++ b/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 diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index 54d09ad41..916de9729 100644 --- a/infer/src/backend/ondemand.ml +++ b/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) diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 3d9dd3729..e88d07a54 100644 --- a/infer/src/base/IssueType.ml +++ b/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" diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index 5dc7d578c..48fd3f167 100644 --- a/infer/src/base/IssueType.mli +++ b/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 diff --git a/infer/src/topl/Topl.ml b/infer/src/topl/Topl.ml index 8cde595f6..80f8d456c 100644 --- a/infer/src/topl/Topl.ml +++ b/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 diff --git a/infer/src/topl/Topl.mli b/infer/src/topl/Topl.mli index 69fad433b..04fccb166 100644 --- a/infer/src/topl/Topl.mli +++ b/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. *) diff --git a/infer/src/topl/ToplAutomaton.ml b/infer/src/topl/ToplAutomaton.ml index b23544b45..30c96a73c 100644 --- a/infer/src/topl/ToplAutomaton.ml +++ b/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 diff --git a/infer/src/topl/ToplAutomaton.mli b/infer/src/topl/ToplAutomaton.mli index 08d7ba4d6..20fb76df4 100644 --- a/infer/src/topl/ToplAutomaton.mli +++ b/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. *) diff --git a/infer/src/topl/ToplMonitor.ml b/infer/src/topl/ToplMonitor.ml index 80417211a..7ec7ed396 100644 --- a/infer/src/topl/ToplMonitor.ml +++ b/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 diff --git a/infer/src/topl/ToplUtils.ml b/infer/src/topl/ToplUtils.ml index ce406672e..cbc032ed9 100644 --- a/infer/src/topl/ToplUtils.ml +++ b/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) diff --git a/infer/src/topl/ToplUtils.mli b/infer/src/topl/ToplUtils.mli index d741575f2..edd568b7a 100644 --- a/infer/src/topl/ToplUtils.mli +++ b/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 diff --git a/infer/tests/codetoanalyze/java/topl/Iterators.java b/infer/tests/codetoanalyze/java/topl/Iterators.java index ea917c73a..98662e3bc 100644 --- a/infer/tests/codetoanalyze/java/topl/Iterators.java +++ b/infer/tests/codetoanalyze/java/topl/Iterators.java @@ -7,8 +7,28 @@ import java.util.*; class Iterators { - void hasNextBad_FN(List x) { - Iterator i = x.iterator(); + void hasNextOk(List xs) { + Iterator i = xs.iterator(); + if (i.hasNext()) i.next(); + } + + void hasNextBad(List xs) { + Iterator i = xs.iterator(); + i.next(); + } + + void hasNextInterproceduralBad(List xs) { + getSingleElementOk(xs.iterator()); + } + + void hasNextInterproceduralOk(List xs) { + Iterator i = xs.iterator(); + if (i.hasNext()) { + getSingleElementOk(i); + } + } + + void getSingleElementOk(Iterator i) { i.next(); } } diff --git a/infer/tests/codetoanalyze/java/topl/Makefile b/infer/tests/codetoanalyze/java/topl/Makefile index a27ae2b56..4ba8f6464 100644 --- a/infer/tests/codetoanalyze/java/topl/Makefile +++ b/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) diff --git a/infer/tests/codetoanalyze/java/topl/hasnext.topl b/infer/tests/codetoanalyze/java/topl/hasnext.topl new file mode 100644 index 000000000..47bf2a882 --- /dev/null +++ b/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) diff --git a/infer/tests/codetoanalyze/java/topl/issues.exp b/infer/tests/codetoanalyze/java/topl/issues.exp index e69de29bb..6606e736d 100644 --- a/infer/tests/codetoanalyze/java/topl/issues.exp +++ b/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, []