diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index e00e0c0ea..17fcb676c 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/infer/man/man1/infer-analyze.txt @@ -401,23 +401,14 @@ OPTIONS Activates: Enable starvation and disable all other checkers (Conversely: --no-starvation-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) + --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) --no-uninit Deactivates: checker uninit: Warns when values are used before diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index e867956a0..16c14e5d6 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -560,8 +560,7 @@ OPTIONS Symexec_memory_error (enabled by default), THREAD_SAFETY_VIOLATION (enabled by default), THREAD_SAFETY_VIOLATION_NULLSAFE (enabled by default), - TOPL_BIABD_ERROR (enabled by default), - TOPL_PULSE_ERROR (enabled by default), + TOPL_ERROR (enabled by default), UNINITIALIZED_VALUE (enabled by default), UNREACHABLE_CODE (enabled by default), UNTRUSTED_BUFFER_ACCESS (disabled by default), @@ -1255,23 +1254,14 @@ OPTIONS Specify custom annotations that should be considered aliases of @ThreadSafe 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 + Activates: checker topl: Detects errors based on user-provided + state machines describing multi-object monitors. (Conversely: + --no-topl) 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). + --topl-only + Activates: Enable topl and disable all other checkers (Conversely: + --no-topl-only) See also infer-analyze(1). --no-uninit Deactivates: checker uninit: Warns when values are used before @@ -2084,15 +2074,7 @@ INTERNAL OPTIONS --topl-properties +path [EXPERIMENTAL] Specify a file containing a temporal property - definition (e.g., jdk.topl). One needs to also select one of the three implementations, by - enabling one of the following checkers - --pulse will run pulse with updated transfer functions - --topl-pulse [SLOW] uses SIL-instrumentation, runs pulse, and - analyzes pulse summaries - --topl-biabd [SLOW] uses SIL-instrumentation, runs biabduction, - and analyzes biabduction summaries - Note that enabling topl-pulse or topl-biabd will disable the - first implementation using updated pulse transfer functions. + definition (e.g., jdk.topl). --topl-properties-reset Set --topl-properties to the empty list. diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt index f057b2cf4..7e8293069 100644 --- a/infer/man/man1/infer-report.txt +++ b/infer/man/man1/infer-report.txt @@ -245,8 +245,7 @@ OPTIONS Symexec_memory_error (enabled by default), THREAD_SAFETY_VIOLATION (enabled by default), THREAD_SAFETY_VIOLATION_NULLSAFE (enabled by default), - TOPL_BIABD_ERROR (enabled by default), - TOPL_PULSE_ERROR (enabled by default), + TOPL_ERROR (enabled by default), UNINITIALIZED_VALUE (enabled by default), UNREACHABLE_CODE (enabled by default), UNTRUSTED_BUFFER_ACCESS (disabled by default), diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 87ca28133..37b8c4338 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -560,8 +560,7 @@ OPTIONS Symexec_memory_error (enabled by default), THREAD_SAFETY_VIOLATION (enabled by default), THREAD_SAFETY_VIOLATION_NULLSAFE (enabled by default), - TOPL_BIABD_ERROR (enabled by default), - TOPL_PULSE_ERROR (enabled by default), + TOPL_ERROR (enabled by default), UNINITIALIZED_VALUE (enabled by default), UNREACHABLE_CODE (enabled by default), UNTRUSTED_BUFFER_ACCESS (disabled by default), @@ -1255,23 +1254,14 @@ OPTIONS Specify custom annotations that should be considered aliases of @ThreadSafe 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 + Activates: checker topl: Detects errors based on user-provided + state machines describing multi-object monitors. (Conversely: + --no-topl) 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). + --topl-only + Activates: Enable topl and disable all other checkers (Conversely: + --no-topl-only) See also infer-analyze(1). --no-uninit Deactivates: checker uninit: Warns when values are used before diff --git a/infer/src/IR/Exp.ml b/infer/src/IR/Exp.ml index 6c2487cb7..0d1ceb8d7 100644 --- a/infer/src/IR/Exp.ml +++ b/infer/src/IR/Exp.ml @@ -155,8 +155,6 @@ let minus_one = int IntLit.minus_one (** Create integer constant corresponding to the boolean value *) let bool b = if b then one else zero -let and_2ary e1 e2 = BinOp (LAnd, e1, e2) - (** Create expression [e1 == e2] *) let eq e1 e2 = BinOp (Eq, e1, e2) @@ -169,12 +167,6 @@ let le e1 e2 = BinOp (Le, e1, e2) (** Create expression [e1 < e2] *) let lt e1 e2 = BinOp (Lt, e1, e2) -let nary_of_2ary op_2ary zero es = - match es with [] -> zero | e :: es -> List.fold ~init:e ~f:op_2ary es - - -let and_nary = nary_of_2ary and_2ary one - let fold_captured ~f exp acc = let rec fold_captured_ exp captured_acc = match exp with @@ -361,34 +353,6 @@ 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, m -> (re e, rv v, t, m)) 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 eb744c8a5..8dcfa4c5d 100644 --- a/infer/src/IR/Exp.mli +++ b/infer/src/IR/Exp.mli @@ -117,9 +117,6 @@ val le : t -> t -> t val lt : t -> t -> t (** Create expression [e1 < e2] *) -val and_nary : t list -> t -(** Create expression [e1 && e2 && e3 && ...] *) - val free_vars : t -> Ident.t Sequence.t (** all the idents appearing in the expression *) @@ -131,10 +128,6 @@ 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/Instrs.mli b/infer/src/IR/Instrs.mli index 46f73fe31..9fd7dd213 100644 --- a/infer/src/IR/Instrs.mli +++ b/infer/src/IR/Instrs.mli @@ -44,6 +44,7 @@ val concat_map_and_fold : by threading an accumulator. Preserve physical equality. **) val concat_map : not_reversed t -> f:(Sil.instr -> Sil.instr array) -> not_reversed t + [@@warning "-32"] (** replace every instruction [instr] with the list [f instr]. Preserve physical equality. **) val reverse_order : not_reversed t -> reversed t diff --git a/infer/src/IR/Mangled.ml b/infer/src/IR/Mangled.ml index 6dc36349a..c4e365a36 100644 --- a/infer/src/IR/Mangled.ml +++ b/infer/src/IR/Mangled.ml @@ -42,12 +42,6 @@ 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 = PrettyPrintable.MakePPSet (struct type nonrec t = t [@@deriving compare] diff --git a/infer/src/IR/Mangled.mli b/infer/src/IR/Mangled.mli index 7d7e3e1bb..e582998c8 100644 --- a/infer/src/IR/Mangled.mli +++ b/infer/src/IR/Mangled.mli @@ -39,9 +39,6 @@ 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 : PrettyPrintable.PPSet with type elt = t diff --git a/infer/src/IR/Procdesc.ml b/infer/src/IR/Procdesc.ml index 7b975cc51..d8a8664d5 100644 --- a/infer/src/IR/Procdesc.ml +++ b/infer/src/IR/Procdesc.ml @@ -281,15 +281,6 @@ module Node = struct true ) - (** Like [replace_instrs], but 1 instr gets replaced by 0, 1, or more instructions. *) - let replace_instrs_by node ~f = - let instrs' = Instrs.concat_map node.instrs ~f:(f node) in - if phys_equal instrs' node.instrs then false - else ( - node.instrs <- instrs' ; - true ) - - let pp_stmt fmt = function | AssertionFailure -> F.pp_print_string fmt "Assertion failure" @@ -620,11 +611,6 @@ let replace_instrs_by_using_context pdesc ~f ~update_context ~context_at_node = update_nodes pdesc ~update -let replace_instrs_by pdesc ~f = - let update node = Node.replace_instrs_by ~f node in - update_nodes pdesc ~update - - (** fold between two nodes or until we reach a branching structure *) let fold_slope_range = let rec aux node visited acc ~f = diff --git a/infer/src/IR/Procdesc.mli b/infer/src/IR/Procdesc.mli index edf6e2ac3..63d40ae3b 100644 --- a/infer/src/IR/Procdesc.mli +++ b/infer/src/IR/Procdesc.mli @@ -306,10 +306,6 @@ val replace_instrs_by_using_context : (** Like [replace_instrs_using_context], but slower, and each instruction may be replaced by 0, 1, or more instructions. *) -val replace_instrs_by : t -> f:(Node.t -> Sil.instr -> Sil.instr array) -> bool -(** Like [replace_instrs], but slower, and each instruction may be replaced by 0, 1, or more - instructions. *) - val iter_nodes : (Node.t -> unit) -> t -> unit (** iterate over all the nodes of a procedure *) diff --git a/infer/src/IR/Pvar.ml b/infer/src/IR/Pvar.ml index 9500db72b..02001f5f9 100644 --- a/infer/src/IR/Pvar.ml +++ b/infer/src/IR/Pvar.ml @@ -318,12 +318,6 @@ let swap_proc_in_local_pvar pvar proc_name = match pvar.pv_kind with Local_var _ -> {pvar with pv_kind= Local_var proc_name} | _ -> pvar -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} - - let is_objc_static_local_of_proc_name pname pvar = (* local static name is of the form procname_varname *) let var_name = Mangled.to_string (get_name pvar) in diff --git a/infer/src/IR/Pvar.mli b/infer/src/IR/Pvar.mli index 8d9a54fb0..fa0fd9d3a 100644 --- a/infer/src/IR/Pvar.mli +++ b/infer/src/IR/Pvar.mli @@ -173,8 +173,6 @@ val materialized_cpp_temporary : string val swap_proc_in_local_pvar : t -> Procname.t -> t -val rename : f:(string -> string) -> t -> t - (** Sets of pvars. *) module Set : PrettyPrintable.PPSet with type elt = t diff --git a/infer/src/backend/InferAnalyze.ml b/infer/src/backend/InferAnalyze.ml index 66f27cf3f..1039349c8 100644 --- a/infer/src/backend/InferAnalyze.ml +++ b/infer/src/backend/InferAnalyze.ml @@ -45,13 +45,10 @@ let proc_name_of_uid = let analyze_target : (TaskSchedulerTypes.target, string) Tasks.doer = let analyze_source_file exe_env source_file = - if Topl.is_shallow_active () then DB.Results_dir.init (Topl.sourcefile ()) ; DB.Results_dir.init source_file ; L.task_progress SourceFile.pp source_file ~f:(fun () -> try Ondemand.analyze_file exe_env source_file ; - if Topl.is_shallow_active () && Config.debug_mode then - DotCfg.emit_frontend_cfg (Topl.sourcefile ()) (Topl.cfg ()) ; if Config.write_html then Printer.write_all_html_files source_file ; None with TaskSchedulerTypes.ProcnameAlreadyLocked {dependency_filename} -> diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index 68a91c3bd..56e21c47f 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -68,10 +68,7 @@ let should_be_analyzed proc_attributes = (not (is_active proc_name)) (* avoid infinite loops *) && not (already_analyzed proc_name) -let get_proc_attr proc_name = - IList.force_until_first_some - [lazy (Summary.OnDisk.proc_resolve_attributes proc_name); lazy (Topl.get_proc_attr proc_name)] - +let get_proc_attr proc_name = Summary.OnDisk.proc_resolve_attributes proc_name let procedure_should_be_analyzed proc_name = match get_proc_attr proc_name with @@ -300,8 +297,7 @@ let register_callee ?caller_summary callee_pname = let get_proc_desc callee_pname = IList.force_until_first_some [ lazy (Procdesc.load callee_pname) - ; lazy (Option.map ~f:Summary.get_proc_desc (Summary.OnDisk.get callee_pname)) - ; lazy (Topl.get_proc_desc callee_pname) ] + ; lazy (Option.map ~f:Summary.get_proc_desc (Summary.OnDisk.get callee_pname)) ] let analyze_callee exe_env ?caller_summary callee_pname = diff --git a/infer/src/backend/registerCheckers.ml b/infer/src/backend/registerCheckers.ml index 405d510d8..9f5adda62 100644 --- a/infer/src/backend/registerCheckers.ml +++ b/infer/src/backend/registerCheckers.ml @@ -149,11 +149,7 @@ let all_checkers = ; (interprocedural Payloads.Fields.quandary ClangTaintAnalysis.checker, Clang) ] } ; { checker= Pulse ; callbacks= - (let checker = - if Config.is_checker_enabled ToplOnPulse then PulseToplShallow.analyze Pulse.checker - else Pulse.checker - in - let pulse = interprocedural Payloads.Fields.pulse checker in + (let pulse = interprocedural Payloads.Fields.pulse Pulse.checker in [(pulse, Clang); (pulse, Java)] ) } ; { checker= Impurity ; callbacks= @@ -179,10 +175,7 @@ let all_checkers = ; { checker= Biabduction ; callbacks= (let biabduction = - dynamic_dispatch Payloads.Fields.biabduction - ( if Config.is_checker_enabled ToplOnBiabduction then - Topl.analyze_with_biabduction Interproc.analyze_procedure - else Interproc.analyze_procedure ) + dynamic_dispatch Payloads.Fields.biabduction Interproc.analyze_procedure in [(biabduction, Clang); (biabduction, Java); (biabduction, CIL)] ) } ; { checker= AnnotationReachability diff --git a/infer/src/base/Checker.ml b/infer/src/base/Checker.ml index f8769ee39..9aff84f05 100644 --- a/infer/src/base/Checker.ml +++ b/infer/src/base/Checker.ml @@ -37,8 +37,7 @@ type t = | SIOF | SelfInBlock | Starvation - | ToplOnBiabduction - | ToplOnPulse + | TOPL | Uninit [@@deriving equal, enumerate] @@ -410,17 +409,8 @@ let config_unsafe checker = ; cli_flags= Some {deprecated= []; show_in_help= true} ; enabled_by_default= true ; activates= [] } - | ToplOnBiabduction -> - { id= "topl-biabd" - ; 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= [Biabduction] } - | ToplOnPulse -> - { id= "topl-pulse" + | TOPL -> + { id= "topl" ; kind= UserFacing {title= "TOPL"; markdown_body= ""} ; support= supports_clang_and_java_experimental ; short_documentation= diff --git a/infer/src/base/Checker.mli b/infer/src/base/Checker.mli index c47510f51..1258183f2 100644 --- a/infer/src/base/Checker.mli +++ b/infer/src/base/Checker.mli @@ -36,8 +36,7 @@ type t = | SIOF | SelfInBlock | Starvation - | ToplOnBiabduction - | ToplOnPulse + | TOPL | Uninit [@@deriving equal, enumerate] diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 86a009375..99c90e8b5 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -2407,15 +2407,7 @@ and topl_max_disjuncts = and topl_properties = CLOpt.mk_path_list ~default:[] ~long:"topl-properties" - "[EXPERIMENTAL] Specify a file containing a temporal property definition (e.g., jdk.topl).\n\ - One needs to also select one of the three implementations, by enabling one of the following \ - checkers\n\ - $(b,--pulse) will run pulse with updated transfer functions\n\ - $(b,--topl-pulse) [SLOW] uses SIL-instrumentation, runs pulse, and analyzes pulse summaries\n\ - $(b,--topl-biabd) [SLOW] uses SIL-instrumentation, runs biabduction, and analyzes \ - biabduction summaries\n\ - Note that enabling topl-pulse or topl-biabd will disable the first implementation using \ - updated pulse transfer functions." + "[EXPERIMENTAL] Specify a file containing a temporal property definition (e.g., jdk.topl)." and profiler_samples = diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 6a1e3f51f..02fe7007d 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -920,13 +920,7 @@ let complexity_increase ~kind ~is_on_ui_thread = register_cost ~kind ~is_on_ui_thread "%s_COMPLEXITY_INCREASE" -let topl_biabd_error = - 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 topl_error = register ~id:"TOPL_ERROR" Error TOPL ~user_documentation:"Experimental." let uninitialized_value = register ~id:"UNINITIALIZED_VALUE" Error Uninit diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index e9ce20a5b..0dd06689a 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -326,9 +326,7 @@ val thread_safety_violation : t val thread_safety_violation_nullsafe : t -val topl_biabd_error : t - -val topl_pulse_error : t +val topl_error : t val uninitialized_value : t diff --git a/infer/src/biabduction/Predicates.mli b/infer/src/biabduction/Predicates.mli index ecf33ef1a..c70644a62 100644 --- a/infer/src/biabduction/Predicates.mli +++ b/infer/src/biabduction/Predicates.mli @@ -351,8 +351,6 @@ val hpred_sub : subst -> hpred -> hpred (** {2 Functions for replacing occurrences of expressions.} *) -val exp_replace_exp : (Exp.t * Exp.t) list -> Exp.t -> Exp.t - val atom_replace_exp : (Exp.t * Exp.t) list -> atom -> atom val hpred_replace_exp : (Exp.t * Exp.t) list -> hpred -> hpred diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 0261e5f1b..b008e27e4 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -181,7 +181,7 @@ module PulseTransferFunctions = struct r in let exec_states_res = - if Topl.is_deep_active () then + if Topl.is_active () then match callee_pname with | Some callee_pname -> topl_small_step call_loc callee_pname func_args ret exec_states_res @@ -323,7 +323,7 @@ module PulseTransferFunctions = struct write_function lhs_addr_hist astate ) in let astates = - if Topl.is_deep_active () then + if Topl.is_active () then List.map astates ~f:(fun result -> let+ astate = result in topl_store_step loc ~lhs:lhs_exp ~rhs:rhs_exp astate ) diff --git a/infer/src/pulse/PulseCItv.ml b/infer/src/pulse/PulseCItv.ml index 40b97da17..8b1615319 100644 --- a/infer/src/pulse/PulseCItv.ml +++ b/infer/src/pulse/PulseCItv.ml @@ -182,8 +182,6 @@ let is_not_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 _ -> diff --git a/infer/src/pulse/PulseCItv.mli b/infer/src/pulse/PulseCItv.mli index a3452749b..07702a7b3 100644 --- a/infer/src/pulse/PulseCItv.mli +++ b/infer/src/pulse/PulseCItv.mli @@ -18,9 +18,6 @@ val is_equal_to_zero : t -> bool val is_not_equal_to_zero : t -> bool (** whether this is literally [≠0] *) -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 = diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml index 7fa5e9337..196e9b988 100644 --- a/infer/src/pulse/PulseFormula.ml +++ b/infer/src/pulse/PulseFormula.ml @@ -1748,13 +1748,6 @@ let is_known_zero phi v = |> 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.both.var_eqs v :> Var.t) phi.both.linear_eqs - >>= LinArith.get_as_const >>= maybe_int - - (** test if [phi.known ⊢ phi.pruned] *) let has_no_assumptions phi = Atom.Set.for_all (fun atom -> Formula.Normalizer.implies_atom phi.known atom) phi.pruned diff --git a/infer/src/pulse/PulseFormula.mli b/infer/src/pulse/PulseFormula.mli index 4c16d1574..04657888c 100644 --- a/infer/src/pulse/PulseFormula.mli +++ b/infer/src/pulse/PulseFormula.mli @@ -72,8 +72,6 @@ val and_fold_subst_variables : val is_known_zero : t -> Var.t -> bool -val as_int : t -> Var.t -> int option - val has_no_assumptions : t -> bool val get_var_repr : t -> Var.t -> Var.t diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml index 5ba7b1bf1..bc04d7bba 100644 --- a/infer/src/pulse/PulseInterproc.ml +++ b/infer/src/pulse/PulseInterproc.ml @@ -744,7 +744,7 @@ let apply_prepost ~is_isl_error_prepost callee_proc_name call_location ~callee_p ~actuals call_state in let astate = - if Topl.is_deep_active () then + if Topl.is_active () then AbductiveDomain.Topl.large_step ~call_location ~callee_proc_name ~substitution:call_state.subst ~condition:call_state.astate.path_condition ~callee_prepost:pre_post.AbductiveDomain.topl call_state.astate diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 7acd7067e..28ebf5983 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -316,7 +316,7 @@ let write_id id new_addr_loc astate = Stack.add (Var.of_id id) new_addr_loc asta let havoc_id id loc_opt astate = (* Topl needs to track the return value of a method; even if nondet now, it may be pruned later. *) - if Topl.is_deep_active () || Stack.mem (Var.of_id id) astate then + if Topl.is_active () || Stack.mem (Var.of_id id) astate then write_id id (AbstractValue.mk_fresh (), loc_opt) astate else astate diff --git a/infer/src/pulse/PulsePathCondition.ml b/infer/src/pulse/PulsePathCondition.ml index 4cd067c51..dce47f36a 100644 --- a/infer/src/pulse/PulsePathCondition.ml +++ b/infer/src/pulse/PulsePathCondition.ml @@ -437,13 +437,6 @@ let is_unsat_expensive tenv ~get_dynamic_type phi = ({phi with formula}, false, new_eqs) -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) ] - - let has_no_assumptions phi = Formula.has_no_assumptions phi.formula let get_var_repr phi v = Formula.get_var_repr phi.formula v diff --git a/infer/src/pulse/PulsePathCondition.mli b/infer/src/pulse/PulsePathCondition.mli index 01cd30434..e098c0b9d 100644 --- a/infer/src/pulse/PulsePathCondition.mli +++ b/infer/src/pulse/PulsePathCondition.mli @@ -84,10 +84,6 @@ val is_unsat_expensive : Tenv.t -> get_dynamic_type:(AbstractValue.t -> Typ.t option) -> t -> t * bool * new_eqs (** 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] *) - val has_no_assumptions : t -> bool (** whether the current path is independent of any calling context *) diff --git a/infer/src/pulse/PulseTopl.ml b/infer/src/pulse/PulseTopl.ml index aecd5eed8..09bbcdacf 100644 --- a/infer/src/pulse/PulseTopl.ml +++ b/infer/src/pulse/PulseTopl.ml @@ -134,7 +134,7 @@ end = struct (Ge, r, l) | _ -> L.die InternalError - "PulseTopl.negate_predicate should handle all outputs of ToplUtils.binop_to" + "PulseTopl.negate_predicate should handle all outputs of PulseTopl.binop_to" let negate disjunction = IList.product (List.map ~f:(List.map ~f:negate_predicate) disjunction) @@ -238,7 +238,7 @@ let start () = ~f:(fun c -> {pre= c; post= c; pruned= Constraint.true_; last_step= None}) configurations in - if Topl.is_deep_active () then mk_simple_states () else (* Avoids work later *) [] + if Topl.is_active () then mk_simple_states () else (* Avoids work later *) [] let get env x = @@ -251,6 +251,21 @@ let get env x = let set = List.Assoc.add ~equal:String.equal +let binop_to : ToplAst.binop -> Binop.t = function + | OpEq -> + Eq + | OpNe -> + Ne + | OpGe -> + Ge + | OpGt -> + Gt + | OpLe -> + Le + | OpLt -> + Lt + + let eval_guard memory tcontext guard : Constraint.t = let operand_of_value (value : ToplAst.value) : PathCondition.operand = match value with @@ -266,7 +281,7 @@ let eval_guard memory tcontext guard : Constraint.t = | Binop (binop, l, r) -> let l = operand_of_value l in let r = operand_of_value r in - let binop = ToplUtils.binop_to binop in + let binop = binop_to binop in Constraint.and_predicate (Constraint.make binop l r) pruned | Value v -> let v = operand_of_value v in @@ -599,7 +614,6 @@ let report_errors proc_desc err_log state = let loc = Procdesc.get_loc proc_desc in let ltr = make_trace 0 [] 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 + Reporting.log_issue proc_desc err_log ~loc ~ltr TOPL IssueType.topl_error message in List.iter ~f:report_simple_state state diff --git a/infer/src/pulse/PulseToplShallow.ml b/infer/src/pulse/PulseToplShallow.ml deleted file mode 100644 index 64508f0e2..000000000 --- a/infer/src/pulse/PulseToplShallow.ml +++ /dev/null @@ -1,56 +0,0 @@ -(* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) - -open! IStd - -let add_errors {InterproceduralAnalysis.proc_desc; err_log} (pulse_summary : PulseSummary.t) = - let pulse_summary = - let f = function PulseExecutionDomain.ContinueProgram s -> Some s | _ -> None in - List.filter_map ~f (pulse_summary :> PulseExecutionDomain.t list) - in - let proc_name = Procdesc.get_proc_name proc_desc in - if not (ToplUtils.is_synthesized proc_name) then - let start_to_error = - Topl.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 = - Format.asprintf "%a" ToplAutomaton.pp_message_of_state (Topl.automaton (), error_state) - in - Reporting.log_issue proc_desc err_log ToplOnPulse IssueType.topl_pulse_error ~loc m - in - List.iter ~f:report errors - - -let analyze pulse analysis_data = Topl.analyze_with add_errors pulse analysis_data diff --git a/infer/src/pulse/PulseToplShallow.mli b/infer/src/pulse/PulseToplShallow.mli deleted file mode 100644 index 1610d9099..000000000 --- a/infer/src/pulse/PulseToplShallow.mli +++ /dev/null @@ -1,12 +0,0 @@ -(* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) - -open! IStd - -val analyze : PulseSummary.t Topl.analysis_transformer -(** 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. *) diff --git a/infer/src/topl/Topl.ml b/infer/src/topl/Topl.ml index 3565ea287..e2f0cd75d 100644 --- a/infer/src/topl/Topl.ml +++ b/infer/src/topl/Topl.ml @@ -8,8 +8,6 @@ open! IStd module L = Logging -let tt = ToplUtils.debug - let parse topl_file = let f ch = let lexbuf = Lexing.from_channel ch in @@ -25,327 +23,6 @@ let parse topl_file = let properties = lazy (List.concat_map ~f:parse Config.topl_properties) -let automaton = lazy (ToplAutomaton.make (Lazy.force properties)) - -let is_shallow_requested () = - Config.is_checker_enabled Checker.ToplOnBiabduction - || Config.is_checker_enabled Checker.ToplOnPulse - - -let is_shallow_active () = is_shallow_requested () && not (List.is_empty (Lazy.force properties)) - -let is_deep_active () = - (not (is_shallow_requested ())) && not (List.is_empty (Lazy.force properties)) - - -let get_proc_desc proc_name = - (* Avoid calling [ToplMonitor.generate] when inactive to avoid side-effects. *) - if is_shallow_active () then ToplMonitor.generate (Lazy.force automaton) proc_name else None - - -let get_proc_attr proc_name = - (* TODO: optimize -- don't generate body just to get attributes *) - Option.map ~f:Procdesc.get_attributes (get_proc_desc proc_name) - - -let get_transitions_count () = ToplAutomaton.tcount (Lazy.force automaton) - -(* NOTE: Code instrumentation only handles ProcedureNamePattern patterns. *) - -(** Checks whether the method name and the number of arguments matches the conditions in a - transition label. Possible optimization: also evaluate if arguments equal certain constants. *) -let evaluate_static_guard label_o (e_fun, arg_ts) = - let pname_of_label label = - match label.ToplAst.pattern with - | ProcedureNamePattern pname -> - pname - | _ -> - L.die UserError - "Topl: The implementation based on SIL-instrumentation only supports ProcedureNamePattern" - in - let evaluate_nonany label = - let match_name () = - match e_fun with - | Exp.Const (Const.Cfun n) -> - (* TODO: perhaps handle inheritance *) - let name = Procname.hashable_name n in - let re = Str.regexp (pname_of_label label) in - let result = Str.string_match re name 0 in - tt " check name='%s'@\n" name ; - result - | _ -> - tt " check name-unknown@\n" ; - false - in - let pattern_len = Option.map ~f:List.length label.ToplAst.arguments in - let match_args () = - let arg_len = 1 + List.length arg_ts in - (* patterns include the return value *) - tt " check arg-len=%d@\n" arg_len ; - Option.value_map ~default:true ~f:(Int.equal arg_len) pattern_len - in - tt "match name-pattern='%s' arg-len-pattern=%a@\n" (pname_of_label label) (Pp.option Int.pp) - pattern_len ; - let log f = - f () - || - ( tt " match result FALSE@\n" ; - false ) - in - log match_args && log match_name - && - ( tt " match result TRUE@\n" ; - true ) - in - Option.value_map ~default:true ~f:evaluate_nonany label_o - - -(** For each transition in the automaton, evaluate its static guard. *) -let get_active_transitions e_fun arg_ts = - let a = Lazy.force automaton in - let f i = evaluate_static_guard (ToplAutomaton.transition a i).label (e_fun, arg_ts) in - Array.init (ToplAutomaton.tcount a) ~f - - -let set_transitions loc active_transitions = - let store i b = - let value = if b then Exp.one else Exp.zero in - Sil.Store - { e1= ToplUtils.static_var (ToplName.transition i) - ; root_typ= ToplUtils.topl_class_typ - ; typ= ToplUtils.topl_class_typ - ; e2= value - ; loc } - in - Array.mapi ~f:store active_transitions - - -let call_save_args loc ret_id ret_typ arg_ts = - let dummy_ret_id = Ident.create_fresh Ident.knormal in - [| ToplUtils.topl_call dummy_ret_id Tvoid loc ToplName.save_args - (arg_ts @ [(Exp.Var ret_id, ret_typ)]) |] - - -let call_execute loc = - let dummy_ret_id = Ident.create_fresh Ident.knormal in - [|ToplUtils.topl_call dummy_ret_id Tvoid loc ToplName.execute []|] - - -let instrument_instruction = function - | Sil.Call ((ret_id, ret_typ), e_fun, arg_ts, loc, _call_flags) as i -> - let active_transitions = get_active_transitions e_fun arg_ts in - let instrument = - let a = Lazy.force automaton in - let is_interesting t active = active && not (ToplAutomaton.is_skip a t) in - Array.existsi ~f:is_interesting active_transitions - in - if not instrument then (* optimization *) [|i|] - else - let i1s = set_transitions loc active_transitions in - let i2s = call_save_args loc ret_id ret_typ arg_ts in - let i3s = call_execute loc in - Array.concat [[|i|]; i1s; i2s; i3s] - | i -> - [|i|] - - -(* PRE: Calling [Tenv.mk_struct tenv ] twice is a no-op. *) -let add_types tenv = - let get_registers () = - let a = Lazy.force automaton in - let h = String.Table.create () in - let record reg = Hashtbl.set h ~key:reg ~data:() in - let record_value = function ToplAst.Register reg -> record reg | _ -> () in - let record_predicate = - ToplAst.( - function - | Binop (_, v1, v2) -> - record_value v1 ; - record_value v2 - | Value v -> - record_value v) - in - let record_assignment (reg, _) = record reg in - let record_label label = - List.iter ~f:record_predicate label.ToplAst.condition ; - List.iter ~f:record_assignment label.ToplAst.action - in - for i = 0 to ToplAutomaton.tcount a - 1 do - Option.iter ~f:record_label (ToplAutomaton.transition a i).label - done ; - Hashtbl.keys h - in - let transition_field i = - (ToplUtils.make_field (ToplName.transition i), Typ.mk (Tint IBool), []) - in - let saved_arg_field i = (ToplUtils.make_field (ToplName.saved_arg i), ToplUtils.any_type, []) in - let register_field name = (ToplUtils.make_field (ToplName.reg name), ToplUtils.any_type, []) in - let statics = - let state = (ToplUtils.make_field ToplName.state, Typ.mk (Tint IInt), []) in - let transitions = List.init (get_transitions_count ()) ~f:transition_field in - let saved_args = List.init (ToplAutomaton.max_args (Lazy.force automaton)) ~f:saved_arg_field in - let registers = List.map ~f:register_field (get_registers ()) in - List.concat [[state]; transitions; saved_args; registers] - in - let _topl_class = Tenv.mk_struct tenv ToplUtils.topl_class_name ~statics in - () - - -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 proc_desc ~f in - tt "add types@\n" ; - 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: - - + one cannot do boolean-conjunction on symbolic heaps; and - + 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 Predicates.Eexp (e, _) -> Some e | _ -> None in - let get_field field (f, e) = if Fieldname.equal field f then from_strexp e else None in - let get_strexp field = function - | Predicates.Estruct (fs, _inst) -> - List.find_map ~f:(get_field field) fs - | _ -> - None - in - let get_hpred obj field = function - | Predicates.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_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 = - 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 - check_phase 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 - 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 tenv (Prop.prop_expmap (Exp.rename_pvars ~f:subscript_pre) pre) - 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 tenv (Prop.prop_expmap (Exp.rename_pvars ~f:subscript_post) post) - in - 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 message = - Format.asprintf "%a" ToplAutomaton.pp_message_of_state (Lazy.force automaton, error) - in - tt "WARN@\n" ; - Reporting.log_issue proc_desc err_log ToplOnBiabduction IssueType.topl_biabd_error - ~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) - 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 tenv state_var pre) - in - List.iter ~f:handle_preposts preposts - - -let sourcefile () = - if not (is_shallow_active ()) then - L.die InternalError "Called Topl.sourcefile when Topl is inactive" ; - ToplMonitor.sourcefile () - - -let cfg () = - if not (is_shallow_active ()) then L.die InternalError "Called Topl.cfg when Topl is inactive" ; - ToplMonitor.cfg () - - -let analyze_with postprocess analyze analysis_data = - if is_shallow_active () then instrument analysis_data ; - let summary = analyze analysis_data in - if is_shallow_active () then Option.iter ~f:(postprocess analysis_data) summary ; - summary - - -let analyze_with_biabduction biabduction analysis_data = - analyze_with add_errors_biabduction biabduction analysis_data - - -let automaton () = Lazy.force automaton - -type 'summary analysis = 'summary InterproceduralAnalysis.t -> 'summary option - -type 'summary postprocess = 'summary InterproceduralAnalysis.t -> 'summary -> unit +let automaton () = ToplAutomaton.make (Lazy.force properties) -type 'summary analysis_transformer = 'summary analysis -> 'summary analysis +let is_active () = Config.is_checker_enabled TOPL && not (List.is_empty (Lazy.force properties)) diff --git a/infer/src/topl/Topl.mli b/infer/src/topl/Topl.mli index 33120403c..ca840bd93 100644 --- a/infer/src/topl/Topl.mli +++ b/infer/src/topl/Topl.mli @@ -10,36 +10,5 @@ open! IStd val automaton : unit -> ToplAutomaton.t (** Return the automaton representing all Topl properties. *) -val is_shallow_active : unit -> bool -(** Return whether the Topl based on Sil instrumentation is active. *) - -val is_deep_active : unit -> bool +val is_active : unit -> bool (** Return whether PulseTopl is active. *) - -val get_proc_attr : Procname.t -> ProcAttributes.t option -(** [get_proc_attr proc_name] returns the attributes of [get_proc_desc proc_name] *) - -val get_proc_desc : Procname.t -> Procdesc.t option -(** Return a synthesized Procdesc.t, when it corresponds to instrumentation for a TOPL property. *) - -val sourcefile : unit -> SourceFile.t -(** The (fake) sourcefile in which synthesized code resides. This function has a side-effect, - because that's how [SourceFile] works, so do NOT call when Topl is inactive. *) - -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.*) - -type 'summary analysis = 'summary InterproceduralAnalysis.t -> 'summary option - -type 'summary postprocess = 'summary InterproceduralAnalysis.t -> 'summary -> unit - -type 'summary analysis_transformer = 'summary analysis -> 'summary analysis - -val analyze_with : 'summary postprocess -> 'summary analysis_transformer -(** [analyze_with analyze postprocess analysis_data] calls [analyze] and then [postprocess] on - [analysis_data] *) - -val analyze_with_biabduction : BiabductionSummary.t analysis_transformer -(** 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. *) diff --git a/infer/src/topl/ToplAutomaton.ml b/infer/src/topl/ToplAutomaton.ml index 8c9c08f9a..b3cdbc4ec 100644 --- a/infer/src/topl/ToplAutomaton.ml +++ b/infer/src/topl/ToplAutomaton.ml @@ -8,7 +8,11 @@ open! IStd module L = Logging -let tt = ToplUtils.debug +let tt fmt = + let mode = if Config.trace_topl then Logging.Quiet else Logging.Verbose in + Logging.debug Analysis mode "ToplTrace: " ; + Logging.debug Analysis mode fmt + module Vname = struct module T = struct @@ -140,35 +144,10 @@ let make properties = {states; nondets; transitions; skips; outgoing; vindex; max_args} -let outgoing a i = a.outgoing.(i) - let vname a i = a.states.(i) -let is_nondet a i = a.nondets.(i) - let vcount a = Array.length a.states -let transition a i = a.transitions.(i) - -let is_skip a i = a.skips.(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 - - let registers a = (* TODO(rgrigore): cache *) let do_assignment acc (r, _v) = String.Set.add acc r in diff --git a/infer/src/topl/ToplAutomaton.mli b/infer/src/topl/ToplAutomaton.mli index 40367d316..7a601f42d 100644 --- a/infer/src/topl/ToplAutomaton.mli +++ b/infer/src/topl/ToplAutomaton.mli @@ -33,29 +33,10 @@ type transition = {source: vindex; target: vindex; label: ToplAst.label option} val make : ToplAst.t list -> t -val outgoing : t -> vindex -> tindex list - -val is_nondet : t -> vindex -> bool - val vcount : t -> int -val transition : t -> tindex -> transition - val tfilter_map : t -> f:(transition -> 'a option) -> 'a list -val is_skip : t -> tindex -> bool -(** A transition is *skip* when it has no action, its guard is implied by all other guards, and its - target equals its source. [is_skip automaton t] returns true when it can prove that [t] is skip.*) - -val tcount : t -> int - -val max_args : t -> int - -val get_start_error_pairs : t -> (vindex * vindex) list -(** Return 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. *) - val registers : t -> ToplAst.register_name list val pp_message_of_state : Format.formatter -> t * tindex -> unit diff --git a/infer/src/topl/ToplMonitor.ml b/infer/src/topl/ToplMonitor.ml deleted file mode 100644 index c1afc06b3..000000000 --- a/infer/src/topl/ToplMonitor.ml +++ /dev/null @@ -1,389 +0,0 @@ -(* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) - -open! IStd -module L = Logging - -let sourcefile = - (* Avoid side-effect when [sourcefile ()] is never called. *) - let x = - lazy - (let pid = Pid.to_int (Unix.getpid ()) in - SourceFile.create (Printf.sprintf "SynthesizedToplProperty%d.java" pid) ) - in - fun () -> Lazy.force x - - -let cfg = - let x = lazy (Cfg.create ()) in - fun () -> Lazy.force x - - -let sourcefile_location () = Location.none (sourcefile ()) - -let type_of_paramtyp (_t : Procname.Parameter.t) : Typ.t = ToplUtils.any_type - -(** NOTE: Similar to [JTrans.formals_from_signature]. *) -let formals_of_procname proc_name = - let params = Procname.get_parameters proc_name in - let new_arg_name = - let n = ref (-1) in - fun () -> - incr n ; - ToplName.arg !n - in - let f t = - let name = Mangled.from_string (new_arg_name ()) in - let typ = type_of_paramtyp t in - (name, typ) - in - List.map ~f params - - -type node_creator = Procdesc.Node.nodekind -> Sil.instr list -> Procdesc.Node.t - -type succ_setter = Procdesc.Node.t -> Procdesc.Node.t list -> unit - -type block = {start_node: Procdesc.Node.t; exit_node: Procdesc.Node.t} - -(** [node_generator]s are the main concept used for organizing the code below. The main property of - node generators is that they compose, because of their return type. The two arguments - ([node_creator] and [succ_setter]) are there mainly to ensure that there is a thin interface - with the underlying (heavily imperative) cfg data-structure from [Procdesc]. *) -type node_generator = node_creator -> succ_setter -> block - -let procedure proc_name (make_body : node_generator) : Procdesc.t = - let attr = - let formals = formals_of_procname proc_name in - let is_defined = true in - let loc = sourcefile_location () in - {(ProcAttributes.default (sourcefile ()) proc_name) with formals; is_defined; loc} - in - let proc_desc = Cfg.create_proc_desc (cfg ()) attr in - let create_node kind instrs = - Procdesc.create_node proc_desc (sourcefile_location ()) kind instrs - in - let exit_node = create_node Procdesc.Node.Exit_node [] in - let set_succs node succs = - Procdesc.node_set_succs proc_desc node ~normal:succs ~exn:[exit_node] - in - let {start_node= body_start; exit_node= body_exit} = make_body create_node set_succs in - let start_node = create_node Procdesc.Node.Start_node [] in - set_succs start_node [body_start] ; - set_succs body_exit [exit_node] ; - Procdesc.set_start_node proc_desc start_node ; - Procdesc.set_exit_node proc_desc exit_node ; - proc_desc - - -let sequence (gens : node_generator list) : node_generator = - fun create_node set_succs -> - let blocks = List.map ~f:(fun g -> g create_node set_succs) gens in - (* NOTE: Possible optimization: fuse successive stmt nodes, by concatenating instructions. *) - let rec connect n = function - | [] -> - n - | p :: qs -> - set_succs n.exit_node [p.start_node] ; - connect p qs - in - match blocks with - | [] -> - let n = create_node (Procdesc.Node.Stmt_node Procdesc.Node.MethodBody) [] in - {start_node= n; exit_node= n} - | n :: ns -> - let p = connect n ns in - {start_node= n.start_node; exit_node= p.exit_node} - - -(** Substitutes a fresh logical variable for any subexpression that is not an operator, a logical - variable or a constant. Also returns assignments from subexpressions to the logical variables - that replaced them. The goal is to get a Sil.Prune condition in a shape friendly to symbolic - execution. *) -let pure_exp e : Exp.t * Sil.instr list = - let rec pluck = - let open Exp in - let open Sequence.Generator in - function - | UnOp (_, e, _) -> - pluck e - | BinOp (_, e1, e2) -> - all_unit [pluck e1; pluck e2] - | Var _ | Const _ -> - return () - | e -> - yield e - in - let es = Sequence.to_list (Sequence.Generator.run (pluck e)) in - let es = List.dedup_and_sort ~compare:Exp.compare es in - let pairs = List.map ~f:(fun e -> (e, Ident.create_fresh Ident.knormal)) es in - let subst = List.map ~f:(function e, id -> (e, Exp.Var id)) pairs in - let e' = Predicates.exp_replace_exp subst e in - let mk_load (e, id) = - Sil.Load - {id; e; root_typ= ToplUtils.any_type; typ= ToplUtils.any_type; loc= sourcefile_location ()} - in - let loads = List.map ~f:mk_load pairs in - (e', loads) - - -let gen_if (condition : Exp.t) (true_branch : node_generator) (false_branch : node_generator) : - node_generator = - (* NOTE: in [condition]: biabduction dislikes pvars; pulse dislikes boolean connectives. The main - difficulty in the code below is to take care of these restrictions. *) - fun create_node set_succs -> - let atom_if atom_condition start : (*false*) Procdesc.Node.t * (*true*) Procdesc.Node.t = - (* PRE: [atom_condition] contains no pvars *) - let prune c b = - let node_type = Procdesc.Node.Prune_node (b, Ik_if, PruneNodeKind_MethodBody) in - let instr = Sil.Prune (c, sourcefile_location (), b, Ik_if) in - create_node node_type [instr] - in - let prune_false = prune (UnOp (LNot, atom_condition, None)) false in - let prune_true = prune atom_condition true in - set_succs start [prune_false; prune_true] ; - (prune_false, prune_true) - in - let n_to_1 xs y = List.iter ~f:(fun x -> set_succs x [y]) xs in - let default_node_kind = Procdesc.Node.Stmt_node MethodBody in - let rec mk_if acc condition start = - (* [mk_if ([],[]) condition start] creates Prune nodes (coming after node [start]) and returns a - pair of node lists (fs, ts) where [fs] are nodes that should continue with the false-branch - and [ts] are nodes that should continue with the true-branch. *) - match (condition : Exp.t) with - | UnOp (LNot, c, _) -> - Tuple2.swap (mk_if (Tuple2.swap acc) c start) - | BinOp (LAnd, l, r) -> - let l_false, l_true = mk_if acc l start in - let r_start = - let join = create_node default_node_kind [] in - n_to_1 l_true join ; - join - in - mk_if (l_false, []) r r_start - | BinOp (LOr, l, r) -> - let neg x = Exp.UnOp (LNot, x, None) in - let condition = neg (BinOp (LAnd, neg l, neg r)) in - mk_if acc condition start - | _ -> - (* maybe in Core will have Tuple2.zip one day? *) - let lift f (l1, r1) (l2, r2) = (f l1 l2, f r1 r2) in - lift List.cons (atom_if condition start) acc - in - let condition, preamble = pure_exp condition in - let start_node = create_node default_node_kind preamble in - let exit_node = create_node default_node_kind [] in - let before_false, before_true = mk_if ([], []) condition start_node in - let {start_node= false_start_node; exit_node= false_exit_node} = - false_branch create_node set_succs - in - let {start_node= true_start_node; exit_node= true_exit_node} = - true_branch create_node set_succs - in - n_to_1 before_false false_start_node ; - n_to_1 before_true true_start_node ; - n_to_1 [false_exit_node; true_exit_node] exit_node ; - {start_node; exit_node} - - -let stmt_node instrs : node_generator = - fun create_node _set_succs -> - let node = create_node (Procdesc.Node.Stmt_node Procdesc.Node.MethodBody) instrs in - {start_node= node; exit_node= node} - - -let sil_assign lhs rhs = - let tempvar = Ident.create_fresh Ident.knormal in - [ Sil.Load - { id= tempvar - ; e= rhs - ; root_typ= ToplUtils.any_type - ; typ= ToplUtils.any_type - ; loc= sourcefile_location () } - ; Sil.Store - { e1= lhs - ; root_typ= ToplUtils.any_type - ; typ= ToplUtils.any_type - ; e2= Exp.Var tempvar - ; loc= sourcefile_location () } ] - - -let assign lhs rhs : node_generator = stmt_node (sil_assign lhs rhs) - -let simple_call function_name : node_generator = - let ret_id = Ident.create_fresh Ident.knormal in - stmt_node [ToplUtils.topl_call ret_id Tvoid (sourcefile_location ()) function_name []] - - -let gen_maybe_call ret_id : node_generator = - stmt_node [ToplUtils.topl_call ret_id (Tint IBool) (sourcefile_location ()) ToplName.maybe []] - - -let arguments_count proc_name = List.length (Procname.get_parameters proc_name) - -(* NOTE: The order of parameters must correspond to what gets generated by [Topl.call_save_args]. *) -let generate_save_args automaton proc_name = - if arguments_count proc_name < 1 then - L.die InternalError "ToplMonitor: saveArgs() needs at least one argument" ; - let n = Int.min (arguments_count proc_name) (ToplAutomaton.max_args automaton) in - let local_var = ToplUtils.local_var proc_name in - procedure proc_name - (sequence - (List.init n ~f:(fun i -> - assign (ToplUtils.static_var (ToplName.saved_arg i)) (local_var (ToplName.arg i)) ))) - - -let generate_execute automaton proc_name = - let call_execute_state i = simple_call (ToplName.execute_state i) in - let fresh_var () = Exp.Var (Ident.create_fresh Ident.knormal) in - let calls = List.init (ToplAutomaton.vcount automaton) ~f:call_execute_state in - let havoc_event_data = - List.init (ToplAutomaton.max_args automaton) ~f:(fun i -> - assign (ToplUtils.static_var (ToplName.saved_arg i)) (fresh_var ()) ) - in - let havoc_transitions = - List.init (ToplAutomaton.tcount automaton) ~f:(fun i -> - assign (ToplUtils.static_var (ToplName.transition i)) (fresh_var ()) ) - in - let all = List.concat [calls; havoc_event_data; havoc_transitions] in - procedure proc_name (sequence all) - - -let generate_execute_state automaton proc_name = - let state : ToplAutomaton.vindex = - let re = Str.regexp "execute_state_\\([0-9]*\\)$" in - let mname = Procname.get_method proc_name in - if Str.string_match re mname 0 then int_of_string (Str.matched_group 1 mname) - else L.die InternalError "ToplMonitor.generate_execute_state called for %s" mname - in - let binding_of t : ToplAst.variable_name -> ToplName.t = - match (ToplAutomaton.transition automaton t).label with - | None -> - fun _ -> L.die InternalError "ToplMonitor: There are no bindings for any-labels." - | Some label -> - let table = String.Table.create () in - let add n v = - match Hashtbl.add ~key:v ~data:n table with - | `Duplicate -> - L.die UserError "ToplMonitor: ill-formed label (%s bound multiple times)" v - | `Ok -> - () - in - Option.iter ~f:(List.iteri ~f:(fun i -> add (ToplName.saved_arg i))) label.ToplAst.arguments ; - let find v = - match Hashtbl.find table v with - | Some arg -> - arg - | None -> - L.die UserError "ToplMonitor: ill-formed label (%s not bound)" v - in - find - in - let condition maybe t : Exp.t = - let binding_of = binding_of t in - let make_condition label = - let exp_of_value = - let open ToplAst in - function - | Constant (LiteralInt x) -> - Exp.Const (Const.Cint (IntLit.of_int x)) - | Register i -> - ToplUtils.static_var (ToplName.reg i) - | Binding v -> - ToplUtils.static_var (binding_of v) - in - let predicate = function - | ToplAst.Binop (op, v1, v2) -> - Exp.BinOp (ToplUtils.binop_to op, exp_of_value v1, exp_of_value v2) - | ToplAst.Value v -> - exp_of_value v - in - List.map ~f:predicate label.ToplAst.condition - in - let condition = - Option.value_map ~default:[] ~f:make_condition (ToplAutomaton.transition automaton t).label - in - let all_conjuncts = - Option.to_list maybe @ (ToplUtils.static_var (ToplName.transition t) :: condition) - in - Exp.and_nary all_conjuncts - in - let skip : node_generator = sequence [] in - let action t : node_generator = - let binding_of = binding_of t in - let transition = ToplAutomaton.transition automaton t in - let all_actions = - let reg_var_assign (reg, var) = - assign (ToplUtils.static_var (ToplName.reg reg)) (ToplUtils.static_var (binding_of var)) - in - let l_assign l = List.map ~f:reg_var_assign l.ToplAst.action in - let lo_assign = Option.value_map ~default:[] ~f:l_assign in - stmt_node - [ Sil.Store - { e1= ToplUtils.static_var ToplName.state - ; root_typ= Typ.mk (Tint IInt) - ; typ= Typ.mk (Tint IInt) - ; e2= Exp.int (IntLit.of_int transition.target) - ; loc= sourcefile_location () } ] - :: lo_assign transition.label - in - sequence all_actions - in - let branch_for_right_state : node_generator = - let check_transition_maybe t (false_branch : node_generator) : node_generator = - let tempid = Ident.create_fresh Ident.knormal in - let tempvar = Exp.Var tempid in - sequence [gen_maybe_call tempid; gen_if (condition (Some tempvar) t) (action t) false_branch] - in - let check_transition t (false_branch : node_generator) : node_generator = - gen_if (condition None t) (action t) false_branch - in - let transitions = ToplAutomaton.outgoing automaton state in - let fold f init = List.fold_right ~init ~f transitions in - let detbranches = fold check_transition skip in - if ToplAutomaton.is_nondet automaton state then fold check_transition_maybe detbranches - else detbranches - in - let body = - gen_if - (Exp.eq (ToplUtils.static_var ToplName.state) (ToplUtils.constant_int state)) - branch_for_right_state skip - in - procedure proc_name body - - -(** INV: For the code generated here, the underlying analysis infers the spec "returned value can be - anything" *) -let generate_maybe _automaton proc_name = procedure proc_name (sequence []) - -let name_matches re proc_name = Str.string_match re (Procname.get_method proc_name) 0 - -let has_name s = name_matches (Str.regexp (s ^ "$")) - -let is_save_args = has_name ToplName.save_args - -let is_execute = has_name ToplName.execute - -let is_execute_state = has_name "execute_state_[0-9]*" - -let is_maybe = has_name ToplName.maybe - -let maybe_synthesize_it automaton proc_name = - if ToplUtils.is_synthesized proc_name then - if is_save_args proc_name then Some (generate_save_args automaton proc_name) - else if is_execute proc_name then Some (generate_execute automaton proc_name) - else if is_execute_state proc_name then Some (generate_execute_state automaton proc_name) - else if is_maybe proc_name then Some (generate_maybe automaton proc_name) - else - L.die InternalError "TOPL instrumentation introduced a call to a method that is not generated" - else None - - -let generate automaton proc_name = - IList.force_until_first_some - [ lazy (Procname.Hash.find_opt (cfg ()) proc_name) - ; lazy (maybe_synthesize_it automaton proc_name) ] diff --git a/infer/src/topl/ToplMonitor.mli b/infer/src/topl/ToplMonitor.mli deleted file mode 100644 index d7590c45f..000000000 --- a/infer/src/topl/ToplMonitor.mli +++ /dev/null @@ -1,21 +0,0 @@ -(* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) - -open! IStd - -val generate : ToplAutomaton.t -> Procname.t -> Procdesc.t option -(** [generate automaton proc_name] returns a CFG, provided that [proc_name] is a recognized - procedure name *) - -val sourcefile : unit -> SourceFile.t -(** For debug. *) - -val cfg : unit -> Cfg.t -(** For debug. This datastructure accumulates all the procedures that were synthesized by the - current process. If the implementation is correct, then different processes synthesize the same - procedures, given the same set of Topl properties. However, for debug, we print the - datastructure in a filename that contains the PID, which is why [sourcefile] is exposed. *) diff --git a/infer/src/topl/ToplName.ml b/infer/src/topl/ToplName.ml deleted file mode 100644 index 1dd441ade..000000000 --- a/infer/src/topl/ToplName.ml +++ /dev/null @@ -1,32 +0,0 @@ -(* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) - -open! IStd - -type t = string - -let p = Printf.sprintf - -let topl_property = "topl.Property" - -let transition = p "transition%d" - -let arg = p "arg%d" - -let saved_arg = p "savedArg%d" - -let reg = p "reg_%s" - -let state = "state" - -let maybe = "maybe" - -let execute = "execute" - -let execute_state = p "execute_state_%d" - -let save_args = "saveArgs" diff --git a/infer/src/topl/ToplName.mli b/infer/src/topl/ToplName.mli deleted file mode 100644 index 8b226b9c5..000000000 --- a/infer/src/topl/ToplName.mli +++ /dev/null @@ -1,30 +0,0 @@ -(* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) - -open! IStd - -type t = string - -val topl_property : t - -val transition : int -> t - -val arg : int -> t - -val saved_arg : int -> t - -val reg : string -> t - -val state : t - -val maybe : t - -val execute : t - -val execute_state : int -> t - -val save_args : t diff --git a/infer/src/topl/ToplUtils.ml b/infer/src/topl/ToplUtils.ml deleted file mode 100644 index 2d0f18f95..000000000 --- a/infer/src/topl/ToplUtils.ml +++ /dev/null @@ -1,64 +0,0 @@ -(* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) - -open! IStd - -let any_type : Typ.t = - let classname = Typ.mk (Tstruct StdTyp.Name.Java.java_lang_object) in - Typ.mk (Tptr (classname, Pk_pointer)) - - -let topl_class_name : Typ.Name.t = Typ.Name.Java.from_string ToplName.topl_property - -let topl_class_typ = Typ.mk (Tstruct topl_class_name) - -let topl_call ret_id (ret_typ : Typ.desc) loc method_name arg_ts : Sil.instr = - let e_fun = - let return_type = Some StdTyp.void in - let parameters = List.map arg_ts ~f:(fun _ -> StdTyp.Java.pointer_to_java_lang_object) in - Exp.Const - (Const.Cfun - (Procname.make_java ~class_name:topl_class_name ~return_type ~method_name ~parameters - ~kind:Procname.Java.Static ())) - in - Sil.Call ((ret_id, Typ.mk ret_typ), e_fun, arg_ts, loc, CallFlags.default) - - -let topl_class_pvar = - let class_name = Mangled.from_string ToplName.topl_property in - Pvar.mk_global class_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 - - -let static_var x : Exp.t = Exp.Lfield (topl_class_exp, make_field x, topl_class_typ) - -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 - | Procname.Java j -> - String.equal ToplName.topl_property (Procname.Java.get_class_name j) - | _ -> - false - - -let binop_to = - let open ToplAst in - let open Binop in - function OpEq -> Eq | OpNe -> Ne | OpGe -> Ge | OpGt -> Gt | OpLe -> Le | OpLt -> Lt - - -let debug fmt = - let mode = if Config.trace_topl then Logging.Quiet else Logging.Verbose in - Logging.debug Analysis mode "ToplTrace: " ; - Logging.debug Analysis mode fmt diff --git a/infer/src/topl/ToplUtils.mli b/infer/src/topl/ToplUtils.mli deleted file mode 100644 index d96cd7bf5..000000000 --- a/infer/src/topl/ToplUtils.mli +++ /dev/null @@ -1,38 +0,0 @@ -(* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) - -open! IStd - -(* This file collects several utilities that are used both for instrumentation (Topl) and for -code generation (ToplMonitor). *) - -val any_type : Typ.t -(** For now, Topl is untyped. The "any" type is simulated with "java.lang.Object". *) - -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 - -val constant_int : int -> Exp.t - -val topl_call : Ident.t -> Typ.desc -> Location.t -> string -> (Exp.t * Typ.t) list -> Sil.instr -(** Call a TOPL function; that is, a static member of "topl.Property" with java.lang.Object - arguments and return [ret_id] of type [ret_typ].*) - -val is_synthesized : Procname.t -> bool - -val debug : ('a, Format.formatter, unit) IStd.format -> 'a - -val make_field : string -> Fieldname.t - -val binop_to : ToplAst.binop -> Binop.t diff --git a/infer/tests/codetoanalyze/java/topl/baos/Makefile b/infer/tests/codetoanalyze/java/topl/baos/Makefile index 1dcf6a443..36fc258ff 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 = --topl-properties baos.topl --pulse-only +INFER_OPTIONS = --topl-properties baos.topl --topl-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 1f109b322..0bb571e7f 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, [call to GZIPOutputStream.(OutputStream),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 GZIPOutputStream.(OutputStream),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()] +codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.FP_dOk(byte[]):byte[], 0, TOPL_ERROR, no_bucket, ERROR, [call to GZIPOutputStream.(OutputStream),call to void FilterOutputStream.write(byte[]),call to byte[] ByteArrayOutputStream.toByteArray()] +codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.FP_eOk(byte[]):byte[], 0, TOPL_ERROR, no_bucket, ERROR, [call to GZIPOutputStream.(OutputStream),call to void FilterOutputStream.write(byte[]),call to byte[] ByteArrayOutputStream.toByteArray()] +codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.aBad():void, 0, TOPL_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_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_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/compareArgs/Makefile b/infer/tests/codetoanalyze/java/topl/compareArgs/Makefile index 74902bccc..3b682a86a 100644 --- a/infer/tests/codetoanalyze/java/topl/compareArgs/Makefile +++ b/infer/tests/codetoanalyze/java/topl/compareArgs/Makefile @@ -5,7 +5,7 @@ TESTS_DIR = ../../../.. -INFER_OPTIONS = --topl-properties CompareArgs.topl --pulse-only +INFER_OPTIONS = --topl-properties CompareArgs.topl --topl-only INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.java) diff --git a/infer/tests/codetoanalyze/java/topl/compareArgs/issues.exp b/infer/tests/codetoanalyze/java/topl/compareArgs/issues.exp index 46445ec04..cc94002c5 100644 --- a/infer/tests/codetoanalyze/java/topl/compareArgs/issues.exp +++ b/infer/tests/codetoanalyze/java/topl/compareArgs/issues.exp @@ -1,2 +1,2 @@ -codetoanalyze/java/topl/compareArgs/CompareArgs.java, CompareArgs.aBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to int CompareArgs.max(int[],int,int)] -codetoanalyze/java/topl/compareArgs/CompareArgs.java, CompareArgs.cBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to int CompareArgs.max(int[],int,int)] +codetoanalyze/java/topl/compareArgs/CompareArgs.java, CompareArgs.aBad():void, 0, TOPL_ERROR, no_bucket, ERROR, [call to int CompareArgs.max(int[],int,int)] +codetoanalyze/java/topl/compareArgs/CompareArgs.java, CompareArgs.cBad():void, 0, TOPL_ERROR, no_bucket, ERROR, [call to int CompareArgs.max(int[],int,int)] diff --git a/infer/tests/codetoanalyze/java/topl/hasnext/Makefile b/infer/tests/codetoanalyze/java/topl/hasnext/Makefile index ca72641cd..1331eb3c6 100644 --- a/infer/tests/codetoanalyze/java/topl/hasnext/Makefile +++ b/infer/tests/codetoanalyze/java/topl/hasnext/Makefile @@ -5,7 +5,7 @@ TESTS_DIR = ../../../.. -INFER_OPTIONS = --topl-properties hasnext.topl --pulse-only +INFER_OPTIONS = --topl-properties hasnext.topl --topl-only INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.java) diff --git a/infer/tests/codetoanalyze/java/topl/hasnext/issues.exp b/infer/tests/codetoanalyze/java/topl/hasnext/issues.exp index 2d0e83612..2c42d0bf2 100644 --- a/infer/tests/codetoanalyze/java/topl/hasnext/issues.exp +++ b/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_PULSE_ERROR, no_bucket, ERROR, [call to Iterator List.iterator(),call to Object Iterator.next()] -codetoanalyze/java/topl/hasnext/Iterators.java, Iterators.hasNextInterproceduralBad(java.util.List):void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to Iterator List.iterator(),call to void Iterators.getSingleElementOk(Iterator),call to Object Iterator.next()] -codetoanalyze/java/topl/hasnext/ScannerFail.java, ScannerFail.readBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to Scanner ScannerFail.getScanner(),call to Scanner.(InputStream),call to String Scanner.next()] +codetoanalyze/java/topl/hasnext/Iterators.java, Iterators.hasNextBad(java.util.List):void, 0, TOPL_ERROR, no_bucket, ERROR, [call to Iterator List.iterator(),call to Object Iterator.next()] +codetoanalyze/java/topl/hasnext/Iterators.java, Iterators.hasNextInterproceduralBad(java.util.List):void, 0, TOPL_ERROR, no_bucket, ERROR, [call to Iterator List.iterator(),call to void Iterators.getSingleElementOk(Iterator),call to Object Iterator.next()] +codetoanalyze/java/topl/hasnext/ScannerFail.java, ScannerFail.readBad():void, 0, TOPL_ERROR, no_bucket, ERROR, [call to Scanner ScannerFail.getScanner(),call to Scanner.(InputStream),call to String Scanner.next()] diff --git a/infer/tests/codetoanalyze/java/topl/immutableArray/Makefile b/infer/tests/codetoanalyze/java/topl/immutableArray/Makefile index 8328ddcb8..9d2c9b13d 100644 --- a/infer/tests/codetoanalyze/java/topl/immutableArray/Makefile +++ b/infer/tests/codetoanalyze/java/topl/immutableArray/Makefile @@ -5,7 +5,7 @@ TESTS_DIR = ../../../.. -INFER_OPTIONS = --topl-properties immutableArray.topl --pulse-only +INFER_OPTIONS = --topl-properties immutableArray.topl --topl-only INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.java) diff --git a/infer/tests/codetoanalyze/java/topl/immutableArray/issues.exp b/infer/tests/codetoanalyze/java/topl/immutableArray/issues.exp index af8ff86ba..695d6409d 100644 --- a/infer/tests/codetoanalyze/java/topl/immutableArray/issues.exp +++ b/infer/tests/codetoanalyze/java/topl/immutableArray/issues.exp @@ -1,4 +1,4 @@ -codetoanalyze/java/topl/immutableArray/ImmutableArray.java, ImmutableArray.badA():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to int[] ImmutableArray.getTestArray(),write to array] -codetoanalyze/java/topl/immutableArray/ImmutableArray.java, ImmutableArray.badABC():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to int[] ImmutableArray.getTestArray(),write to array] -codetoanalyze/java/topl/immutableArray/ImmutableArray.java, ImmutableArray.badB():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to int[] ImmutableArray.getTestArray(),write to array] -codetoanalyze/java/topl/immutableArray/ImmutableArray.java, ImmutableArray.badC():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to int[] ImmutableArray.getTestArray(),call to void ImmutableArray.otherMutateArray(int[]),write to array] +codetoanalyze/java/topl/immutableArray/ImmutableArray.java, ImmutableArray.badA():void, 0, TOPL_ERROR, no_bucket, ERROR, [call to int[] ImmutableArray.getTestArray(),write to array] +codetoanalyze/java/topl/immutableArray/ImmutableArray.java, ImmutableArray.badABC():void, 0, TOPL_ERROR, no_bucket, ERROR, [call to int[] ImmutableArray.getTestArray(),write to array] +codetoanalyze/java/topl/immutableArray/ImmutableArray.java, ImmutableArray.badB():void, 0, TOPL_ERROR, no_bucket, ERROR, [call to int[] ImmutableArray.getTestArray(),write to array] +codetoanalyze/java/topl/immutableArray/ImmutableArray.java, ImmutableArray.badC():void, 0, TOPL_ERROR, no_bucket, ERROR, [call to int[] ImmutableArray.getTestArray(),call to void ImmutableArray.otherMutateArray(int[]),write to array] diff --git a/infer/tests/codetoanalyze/java/topl/servlet/Makefile b/infer/tests/codetoanalyze/java/topl/servlet/Makefile index 04bd01cf3..c6ebf4276 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 = --topl-properties servlet.topl --pulse-only +INFER_OPTIONS = --topl-properties servlet.topl --topl-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 471cccbd8..0171d89b1 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, [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)] +codetoanalyze/java/topl/servlet/ServletTests.java, ServletTests.aBad(javax.servlet.ServletResponse):void, 0, TOPL_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_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_ERROR, no_bucket, ERROR, [call to PrintWriter ServletResponse.getWriter(),call to void RequestDispatcher.forward(ServletRequest,ServletResponse)] diff --git a/infer/tests/codetoanalyze/java/topl/skip/Makefile b/infer/tests/codetoanalyze/java/topl/skip/Makefile index f7ff9003a..a567332fe 100644 --- a/infer/tests/codetoanalyze/java/topl/skip/Makefile +++ b/infer/tests/codetoanalyze/java/topl/skip/Makefile @@ -6,7 +6,7 @@ TESTS_DIR = ../../../.. INFER_OPTIONS = --seconds-per-iteration 100 --symops-per-iteration 100000 --topl-properties SkipAfterRemove.topl --topl-biabd-only -#INFER_OPTIONS = --topl-properties SkipAfterRemove.topl --pulse-only +#INFER_OPTIONS = --topl-properties SkipAfterRemove.topl --topl-only INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.java) diff --git a/infer/tests/codetoanalyze/java/topl/slowIter/Makefile b/infer/tests/codetoanalyze/java/topl/slowIter/Makefile index 840a1a2a9..c84e27d87 100644 --- a/infer/tests/codetoanalyze/java/topl/slowIter/Makefile +++ b/infer/tests/codetoanalyze/java/topl/slowIter/Makefile @@ -5,7 +5,7 @@ TESTS_DIR = ../../../.. -INFER_OPTIONS = --topl-properties slowIter.topl --pulse-only +INFER_OPTIONS = --topl-properties slowIter.topl --topl-only INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.java) diff --git a/infer/tests/codetoanalyze/java/topl/slowIter/issues.exp b/infer/tests/codetoanalyze/java/topl/slowIter/issues.exp index 264bb46ac..df141016b 100644 --- a/infer/tests/codetoanalyze/java/topl/slowIter/issues.exp +++ b/infer/tests/codetoanalyze/java/topl/slowIter/issues.exp @@ -1,2 +1,2 @@ -codetoanalyze/java/topl/slowIter/SlowIterTests.java, SlowIterTests.aBad(java.util.Map):void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to Set Map.keySet(),call to Iterator Set.iterator(),call to Object Iterator.next(),call to Object Map.get(Object)] -codetoanalyze/java/topl/slowIter/SlowIterTests.java, SlowIterTests.bBad(java.util.Map):void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to Set Map.keySet(),call to Iterator Set.iterator(),call to Object Iterator.next(),call to void SlowIterTests.print(Object,Map),call to Object Map.get(Object)] +codetoanalyze/java/topl/slowIter/SlowIterTests.java, SlowIterTests.aBad(java.util.Map):void, 0, TOPL_ERROR, no_bucket, ERROR, [call to Set Map.keySet(),call to Iterator Set.iterator(),call to Object Iterator.next(),call to Object Map.get(Object)] +codetoanalyze/java/topl/slowIter/SlowIterTests.java, SlowIterTests.bBad(java.util.Map):void, 0, TOPL_ERROR, no_bucket, ERROR, [call to Set Map.keySet(),call to Iterator Set.iterator(),call to Object Iterator.next(),call to void SlowIterTests.print(Object,Map),call to Object Map.get(Object)] diff --git a/infer/tests/codetoanalyze/java/topl/taint/Makefile b/infer/tests/codetoanalyze/java/topl/taint/Makefile index 220e5a3a8..962eba26d 100644 --- a/infer/tests/codetoanalyze/java/topl/taint/Makefile +++ b/infer/tests/codetoanalyze/java/topl/taint/Makefile @@ -5,7 +5,7 @@ TESTS_DIR = ../../../.. -INFER_OPTIONS = --topl-properties Taint.topl --pulse-only +INFER_OPTIONS = --topl-properties Taint.topl --topl-only INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.java) diff --git a/infer/tests/codetoanalyze/java/topl/taint/issues.exp b/infer/tests/codetoanalyze/java/topl/taint/issues.exp index cd05cbb43..b45fea61d 100644 --- a/infer/tests/codetoanalyze/java/topl/taint/issues.exp +++ b/infer/tests/codetoanalyze/java/topl/taint/issues.exp @@ -1 +1 @@ -codetoanalyze/java/topl/taint/Taint.java, Taint.fBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to String Taint.badString(),call to StringBuilder.(),call to StringBuilder StringBuilder.append(String),call to String StringBuilder.toString(),call to StringBuilder.(),call to StringBuilder StringBuilder.append(String),call to String StringBuilder.toString(),call to void Taint.sendToDb(String)] +codetoanalyze/java/topl/taint/Taint.java, Taint.fBad():void, 0, TOPL_ERROR, no_bucket, ERROR, [call to String Taint.badString(),call to StringBuilder.(),call to StringBuilder StringBuilder.append(String),call to String StringBuilder.toString(),call to StringBuilder.(),call to StringBuilder StringBuilder.append(String),call to String StringBuilder.toString(),call to void Taint.sendToDb(String)]