diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 992cbd457..393b09bd0 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -31,6 +31,16 @@ let report_on_error_list {InterproceduralAnalysis.proc_desc; err_log} result = PulseReport.report_error proc_desc err_log result |> exec_list_of_list_result +let report_topl_errors proc_desc err_log summary = + let f = function + | ExecutionDomain.ContinueProgram astate -> + PulseTopl.report_errors proc_desc err_log (AbductiveDomain.Topl.get astate) + | _ -> + () + in + List.iter ~f summary + + let proc_name_of_call call_exp = match (call_exp : Exp.t) with | Const (Cfun proc_name) | Closure {name= proc_name} -> @@ -92,14 +102,14 @@ module PulseTransferFunctions = struct Ok exec_state - let topl_small_step procname arguments (return, _typ) exec_state_res = + let topl_small_step loc procname arguments (return, _typ) exec_state_res = let arguments = List.map arguments ~f:(fun {ProcnameDispatcher.Call.FuncArg.arg_payload} -> fst arg_payload) in let return = Var.of_id return in let do_astate astate = let return = Option.map ~f:fst (Stack.find_opt return astate) in - let topl_event = PulseTopl.Call {return; arguments; procname} in + let topl_event = PulseTopl.Call {return; arguments; procname; loc} in AbductiveDomain.Topl.small_step topl_event astate in let do_one_exec_state (exec_state : Domain.t) : Domain.t = @@ -157,7 +167,7 @@ module PulseTransferFunctions = struct if Topl.is_deep_active () then match callee_pname with | Some callee_pname -> - topl_small_step callee_pname func_args ret exec_state_res + topl_small_step call_loc callee_pname func_args ret exec_state_res | None -> (* skip, as above for non-topl *) exec_state_res else exec_state_res @@ -330,11 +340,13 @@ module DisjunctiveAnalyzer = let widen_policy = `UnderApproximateAfterNumIterations Config.pulse_widen_threshold end) -let checker ({InterproceduralAnalysis.proc_desc} as analysis_data) = +let checker ({InterproceduralAnalysis.proc_desc; err_log} as analysis_data) = AbstractValue.State.reset () ; let initial = [ExecutionDomain.mk_initial proc_desc] in match DisjunctiveAnalyzer.compute_post analysis_data ~initial proc_desc with | Some posts -> - Some (PulseSummary.of_posts proc_desc posts) + let summary = PulseSummary.of_posts proc_desc posts in + report_topl_errors proc_desc err_log summary ; + Some summary | None -> None diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 6f2502337..c9ef25858 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -496,4 +496,7 @@ module Topl = struct let large_step ~substitution ?(condition = PathCondition.true_) ~callee_prepost astate = {astate with topl= PulseTopl.large_step ~substitution ~condition ~callee_prepost astate.topl} + + + let get {topl} = topl end diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 9e6daf6ef..01e3f83cb 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -189,4 +189,6 @@ module Topl : sig -> callee_prepost:PulseTopl.state -> t -> t + + val get : summary -> PulseTopl.state end diff --git a/infer/src/pulse/PulseTopl.ml b/infer/src/pulse/PulseTopl.ml index 709e3417d..0ae9299de 100644 --- a/infer/src/pulse/PulseTopl.ml +++ b/infer/src/pulse/PulseTopl.ml @@ -11,7 +11,8 @@ module L = Logging type value = AbstractValue.t -type event = Call of {return: value option; arguments: value list; procname: Procname.t} +type event = + | Call of {return: value option; arguments: value list; procname: Procname.t; loc: Location.t} let pp_comma_seq f xs = Pp.comma_seq ~print_env:Pp.text_break f xs @@ -29,12 +30,19 @@ type configuration = {vertex: vertex; memory: (register * value) list} type predicate = Binop.t * PathCondition.operand * PathCondition.operand -type simple_state = +type step = + { step_event: event + ; step_predecessor: simple_state (** state before this step *) + ; step_type: step_type } + +and step_type = SmallStep + +(* TODO(rgrigore): | LargeStep of simple_state *) +and simple_state = { pre: configuration (** at the start of the procedure *) ; post: configuration (** at the current program point *) - ; pruned: predicate list (** path-condition for the automaton *) } - -(* TODO(rgrigore): use Formula.Atom.Set for [pruned]?? *) + ; pruned: predicate list (** path-condition for the automaton *) + ; last_step: step option (** for trace error reporting *) } (* TODO: include a hash of the automaton in a summary to avoid caching problems. *) (* TODO: limit the number of simple_states to some configurable number (default ~5) *) @@ -68,7 +76,7 @@ let start () = fun () -> List.map ~f:(fun r -> (r, AbstractValue.mk_fresh ())) registers in let configurations = List.map ~f:(fun vertex -> {vertex; memory= mk_memory ()}) starts in - List.map ~f:(fun c -> {pre= c; post= c; pruned= []}) configurations + List.map ~f:(fun c -> {pre= c; post= c; pruned= []; last_step= None}) configurations in if Topl.is_deep_active () then mk_simple_states () else (* Avoids work later *) [] @@ -214,39 +222,47 @@ let skip_pruned_of_nonskip_pruned nonskip_list = let small_step path_condition event simple_states = let tmatches = static_match event in - let evolve_transition memory (transition, tcontext) : (configuration * predicate list) list = + let evolve_transition (old : simple_state) (transition, tcontext) : state = + let mk ?(memory = old.post.memory) ?(pruned = []) significant = + let last_step = + if significant then Some {step_event= event; step_predecessor= old; step_type= SmallStep} + else old.last_step + in + (* NOTE: old pruned is discarded, because evolve_simple_state needs to see only new prunes + to determine skip transitions. It will then add back old prunes. *) + let post = {vertex= transition.ToplAutomaton.target; memory} in + {old with post; pruned; last_step} + in match transition.ToplAutomaton.label with | None -> (* "any" transition *) - [({vertex= transition.ToplAutomaton.target; memory}, [])] + let is_loop = Int.equal transition.ToplAutomaton.source transition.ToplAutomaton.target in + [mk (not is_loop)] | Some label -> + let memory = old.post.memory in let pruned = eval_guard memory tcontext label.ToplAst.condition in let memory = apply_action tcontext label.ToplAst.action memory in - [({vertex= transition.ToplAutomaton.target; memory}, pruned)] + [mk ~memory ~pruned true] in - let evolve_state_cond ({vertex; memory}, pruned) = - let path_condition = conjoin_pruned path_condition pruned in + let evolve_simple_state old = + let path_condition = conjoin_pruned path_condition old.pruned in let simplify result = - (* TODO(rgrigore): Remove from extra_pruned what is implied by path_condition *) - let f (_configuration, extra_pruned) = not (is_unsat path_condition extra_pruned) in + let f {pruned} = not (is_unsat path_condition pruned) in List.filter ~f result in let tmatches = - List.filter ~f:(fun (t, _) -> Int.equal vertex t.ToplAutomaton.source) tmatches + List.filter ~f:(fun (t, _) -> Int.equal old.post.vertex t.ToplAutomaton.source) tmatches in - let nonskip = simplify (List.concat_map ~f:(evolve_transition memory) tmatches) in + let nonskip = simplify (List.concat_map ~f:(evolve_transition old) tmatches) in let skip = - let nonskip_pruned_list = List.map ~f:snd nonskip in + let nonskip_pruned_list = List.map ~f:(fun {pruned} -> pruned) nonskip in let skip_pruned_list = skip_pruned_of_nonskip_pruned nonskip_pruned_list in - let f pruned = ({vertex; memory}, pruned) in + let f pruned = {old with pruned} (* keeps last_step from old *) in simplify (List.map ~f skip_pruned_list) in - let add_old_pruned (configuration, extra_pruned) = (configuration, extra_pruned @ pruned) in + let add_old_pruned s = {s with pruned= List.rev_append s.pruned old.pruned} in List.map ~f:add_old_pruned (List.rev_append nonskip skip) in - let evolve_simple_state {pre; post; pruned} = - List.map ~f:(fun (post, pruned) -> {pre; post; pruned}) (evolve_state_cond (post, pruned)) - in let result = List.concat_map ~f:evolve_simple_state simple_states in L.d_printfln "@[<2>PulseTopl.small_step:@;%a@ -> %a@]" pp_state simple_states pp_state result ; result @@ -259,7 +275,7 @@ let filter_for_summary path_condition state = let simplify ~keep state = - let simplify_simple_state {pre; post; pruned} = + let simplify_simple_state {pre; post; pruned; last_step} = (* NOTE(rgrigore): registers could be considered live for the program path_condition as well. That should improve precision, but I'm wary of altering what the Pulse program state is just because Topl is enabled. *) @@ -273,6 +289,31 @@ let simplify ~keep state = in let is_live_predicate (_op, l, r) = is_live_operand l && is_live_operand r in let pruned = List.filter ~f:is_live_predicate pruned in - {pre; post; pruned} + {pre; post; pruned; last_step} in List.map ~f:simplify_simple_state state + + +let report_errors proc_desc err_log state = + let a = Topl.automaton () in + let rec make_trace acc q = + match q.last_step with + | None -> + acc + | Some {step_event; step_predecessor; step_type= SmallStep} -> + let (Call {loc; procname}) = step_event in + let description = + Format.fprintf Format.str_formatter "@[call to %a@]" Procname.pp procname ; + Format.flush_str_formatter () + in + let e = Errlog.make_trace_element 0 loc description [] in + make_trace (e :: acc) step_predecessor + in + let report_simple_state q = + if ToplAutomaton.is_start a q.pre.vertex && ToplAutomaton.is_error a q.post.vertex then + let loc = Procdesc.get_loc proc_desc in + let ltr = make_trace [] q in + let message = Format.asprintf "%a" ToplAutomaton.pp_message_of_state (a, q.post.vertex) in + Reporting.log_issue proc_desc err_log ~loc ~ltr ToplOnPulse IssueType.topl_pulse_error message + in + List.iter ~f:report_simple_state state diff --git a/infer/src/pulse/PulseTopl.mli b/infer/src/pulse/PulseTopl.mli index ba576f987..42e833119 100644 --- a/infer/src/pulse/PulseTopl.mli +++ b/infer/src/pulse/PulseTopl.mli @@ -9,7 +9,8 @@ open! IStd type value = PulseAbstractValue.t -type event = Call of {return: value option; arguments: value list; procname: Procname.t} +type event = + | Call of {return: value option; arguments: value list; procname: Procname.t; loc: Location.t} type state @@ -36,4 +37,7 @@ val filter_for_summary : PulsePathCondition.t -> state -> state val simplify : keep:PulseAbstractValue.Set.t -> state -> state +val report_errors : Procdesc.t -> Errlog.t -> state -> unit +(** Calls [Reporting.log_issue] with error traces, if any. *) + val pp_state : Format.formatter -> state -> unit diff --git a/infer/src/topl/ToplAutomaton.ml b/infer/src/topl/ToplAutomaton.ml index cbac3abac..52e8b8708 100644 --- a/infer/src/topl/ToplAutomaton.ml +++ b/infer/src/topl/ToplAutomaton.ml @@ -196,3 +196,13 @@ let tfilter_map a ~f = Array.to_list (Array.filter_map ~f a.transitions) let pp_transition f {source; target; label} = Format.fprintf f "@[%d -> %d:@,%a@]" source target ToplAstOps.pp_label label + + +let has_name n a i = + let _property, name = vname a i in + String.equal name n + + +let is_start = has_name "start" + +let is_error = has_name "error" diff --git a/infer/src/topl/ToplAutomaton.mli b/infer/src/topl/ToplAutomaton.mli index 0aa48c56d..012118826 100644 --- a/infer/src/topl/ToplAutomaton.mli +++ b/infer/src/topl/ToplAutomaton.mli @@ -61,4 +61,8 @@ val starts : t -> vindex list val registers : t -> ToplAst.register_name list +val is_start : t -> vindex -> bool + +val is_error : t -> vindex -> bool + val pp_transition : Format.formatter -> transition -> unit diff --git a/infer/tests/codetoanalyze/java/topl/baos/Makefile b/infer/tests/codetoanalyze/java/topl/baos/Makefile index 9e575075c..1dcf6a443 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 = --pulse-max-disjuncts 400 --topl-properties baos.topl --topl-pulse-only +INFER_OPTIONS = --topl-properties baos.topl --pulse-only INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.java) diff --git a/infer/tests/codetoanalyze/java/topl/baos/issues.exp b/infer/tests/codetoanalyze/java/topl/baos/issues.exp index 407d07d02..c1c32a14d 100644 --- a/infer/tests/codetoanalyze/java/topl/baos/issues.exp +++ b/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_PULSE_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_PULSE_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_PULSE_ERROR, no_bucket, ERROR, [] +codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.FP_dOk(byte[]):byte[], 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to ByteArrayOutputStream.(int),call to void FilterOutputStream.write(byte[]),call to byte[] ByteArrayOutputStream.toByteArray()] +codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.FP_eOk(byte[]):byte[], 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to ByteArrayOutputStream.(int),call to void FilterOutputStream.write(byte[]),call to byte[] ByteArrayOutputStream.toByteArray()] +codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.aBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to ObjectOutputStream.(OutputStream),call to void ObjectOutputStream.writeObject(Object),call to byte[] ByteArrayOutputStream.toByteArray()] +codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.bBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to ObjectOutputStream.(OutputStream),call to void ObjectOutputStream.writeObject(Object),call to byte[] ByteArrayOutputStream.toByteArray()] +codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.cBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to DataOutputStream.(OutputStream),call to void DataOutputStream.writeLong(long),call to byte[] ByteArrayOutputStream.toByteArray()] diff --git a/infer/tests/codetoanalyze/java/topl/servlet/Makefile b/infer/tests/codetoanalyze/java/topl/servlet/Makefile index 91d84bafd..04bd01cf3 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 = --pulse-max-disjuncts 100 --topl-properties servlet.topl --topl-pulse-only +INFER_OPTIONS = --topl-properties servlet.topl --pulse-only INFERPRINT_OPTIONS = --issues-tests TEST_CLASSPATH = javax.servlet-api-4.0.1.jar diff --git a/infer/tests/codetoanalyze/java/topl/servlet/issues.exp b/infer/tests/codetoanalyze/java/topl/servlet/issues.exp index f4becec2d..471cccbd8 100644 --- a/infer/tests/codetoanalyze/java/topl/servlet/issues.exp +++ b/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_PULSE_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_PULSE_ERROR, no_bucket, ERROR, [] +codetoanalyze/java/topl/servlet/ServletTests.java, ServletTests.aBad(javax.servlet.ServletResponse):void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to PrintWriter ServletResponse.getWriter(),call to ServletOutputStream ServletResponse.getOutputStream()] +codetoanalyze/java/topl/servlet/ServletTests.java, ServletTests.bBad(javax.servlet.ServletResponse):void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to ServletOutputStream ServletResponse.getOutputStream(),call to PrintWriter ServletResponse.getWriter()] +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, [call to PrintWriter ServletResponse.getWriter(),call to void RequestDispatcher.forward(ServletRequest,ServletResponse)]