From 7eba62c9edd72fb9927b5aa05df927b1151934db Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 9 Sep 2020 08:35:21 -0700 Subject: [PATCH] [doc] update documentation on building checkers Summary: - freshen up /docs/next/absint-framework to give sensible advice, and delete outdated bits that are now in the API docs so they remain fresh - delete SimpleChecker.ml as it's just a source of bitrot - delete the "adding checkers" page as it's completely outdated and subsumed by the "AI framework" page + the labs. Reviewed By: jberdine Differential Revision: D23597271 fbshipit-source-id: 78b541746 --- infer/src/backend/registerCheckers.ml | 7 - infer/src/checkers/SimpleChecker.ml | 96 ---------- infer/src/checkers/SimpleChecker.mli | 26 --- website/docs/04-absint-framework.md | 263 +++++++------------------- website/docs/04-adding-checkers.md | 210 -------------------- website/sidebars.js | 2 +- 6 files changed, 69 insertions(+), 535 deletions(-) delete mode 100644 infer/src/checkers/SimpleChecker.ml delete mode 100644 infer/src/checkers/SimpleChecker.mli delete mode 100644 website/docs/04-adding-checkers.md diff --git a/infer/src/backend/registerCheckers.ml b/infer/src/backend/registerCheckers.ml index c0c3f52e5..4390d0c99 100644 --- a/infer/src/backend/registerCheckers.ml +++ b/infer/src/backend/registerCheckers.ml @@ -11,13 +11,6 @@ open! IStd module F = Format -(* make sure SimpleChecker.ml is not dead code *) -let () = - if false then - let module SC = SimpleChecker.Make in - () - - type callback_fun = | Procedure of Callbacks.proc_callback_t | DynamicDispatch of Callbacks.proc_callback_t diff --git a/infer/src/checkers/SimpleChecker.ml b/infer/src/checkers/SimpleChecker.ml deleted file mode 100644 index 4e1596397..000000000 --- a/infer/src/checkers/SimpleChecker.ml +++ /dev/null @@ -1,96 +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 F = Format -module L = Logging - -(** functor that makes it easy to write a basic abstract interpretation checker by lifting a type, - comparison function, reporting function, and exec function into an analyzer *) - -module type Spec = sig - (** what state do you want to propagate? *) - type t - - val initial : t - (** implement the state the analysis should start from here *) - - val exec_instr : t -> Sil.instr -> Procdesc.Node.nodekind -> Procname.t -> Tenv.t -> t - (** implement how an instruction changes your state here. input is the previous state, current - instruction, current node kind, current procedure and type environment. *) - - val report : t -> Location.t -> Procname.t -> unit - (** log errors here. input is a state, location where the state occurs in the source, and the - current procedure. *) - - val compare : t -> t -> int -end - -module type S = sig - val checker : IntraproceduralAnalysis.t -> unit - (** add YourChecker.checker to registerCallbacks.ml to run your checker *) -end - -module Make (Spec : Spec) : S = struct - (* powerset domain over Spec.t *) - module Domain = struct - include AbstractDomain.FiniteSet (struct - type t = Spec.t - - let compare = Spec.compare - - let pp _ _ = () - end) - - let widen ~prev ~next ~num_iters = - let iters_befor_timeout = 1000 in - (* failsafe for accidental non-finite height domains *) - if num_iters >= iters_befor_timeout then - L.(die InternalError) - "Stopping analysis after 1000 iterations without convergence. Make sure your domain is \ - finite height." - else widen ~prev ~next ~num_iters - end - - module TransferFunctions (CFG : ProcCfg.S) = struct - module CFG = CFG - module Domain = Domain - - type analysis_data = IntraproceduralAnalysis.t - - let exec_instr astate_set {IntraproceduralAnalysis.proc_desc; tenv} node instr = - let node_kind = CFG.Node.kind node in - let pname = Procdesc.get_proc_name proc_desc in - Domain.fold - (fun astate acc -> Domain.add (Spec.exec_instr astate instr node_kind pname tenv) acc) - astate_set Domain.empty - - - let pp_session_name _node fmt = F.pp_print_string fmt "simple checker" - end - - module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions (ProcCfg.Exceptional)) - - let checker ({IntraproceduralAnalysis.proc_desc} as analysis_data) = - let proc_name = Procdesc.get_proc_name proc_desc in - let nodes = Procdesc.get_nodes proc_desc in - let do_reporting node_id state = - let astate_set = state.AbstractInterpreter.State.post in - if not (Domain.is_empty astate_set) then - (* should never fail since keys in the invariant map should always be real node id's *) - let node = - List.find_exn - ~f:(fun node -> Procdesc.Node.equal_id node_id (Procdesc.Node.get_id node)) - nodes - in - Domain.iter - (fun astate -> Spec.report astate (ProcCfg.Exceptional.Node.loc node) proc_name) - astate_set - in - let inv_map = Analyzer.exec_pdesc analysis_data ~initial:Domain.empty proc_desc in - Analyzer.InvariantMap.iter do_reporting inv_map -end diff --git a/infer/src/checkers/SimpleChecker.mli b/infer/src/checkers/SimpleChecker.mli deleted file mode 100644 index ecd0a7fc5..000000000 --- a/infer/src/checkers/SimpleChecker.mli +++ /dev/null @@ -1,26 +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 type Spec = sig - type t - - val initial : t - - val exec_instr : t -> Sil.instr -> Procdesc.Node.nodekind -> Procname.t -> Tenv.t -> t - - val report : t -> Location.t -> Procname.t -> unit - - val compare : t -> t -> int -end - -module type S = sig - val checker : IntraproceduralAnalysis.t -> unit -end - -module Make (Spec : Spec) : S diff --git a/website/docs/04-absint-framework.md b/website/docs/04-absint-framework.md index af3244fe5..d230c6936 100644 --- a/website/docs/04-absint-framework.md +++ b/website/docs/04-absint-framework.md @@ -6,14 +6,13 @@ title: Building checkers with the Infer.AI framework Infer.AI is a framework for quickly developing abstract interpretation-based checkers (intraprocedural or interprocedural). You define only: -(1) An abstract domain (type of abstract state plus `<=`, `join`, and `widen` +1. An abstract domain (type of abstract state plus `<=`, `join`, and `widen` operations) - -(2) Transfer functions (a transformer that takes an abstract state as input and +2. Transfer functions (a transformer that takes an abstract state as input and produces an abstract state as output) -and then you have an analysis that can run on all of the languages Infer -supports (C, Obj-C, C++, and Java)! +What you get in exchange is an analysis that can run on all of the +languages Infer supports (C, Objective-C, C++, and Java)! This guide covers how to use the framework. For background on why we built the framework and how it works, check out these @@ -44,14 +43,13 @@ There are basically three important bits here: defining the domain, defining the transfer functions, and then passing the pieces to the framework to create an an analysis. Let's break down the third bit: -``` -module Analyzer = - AbstractInterpreter.Make - (ProcCfg.Backward(ProcCfg.Exceptional)) - (TransferFunctions) +```OCaml +module CFG = ProcCfg.OneInstrPerNode (ProcCfg.Backward (ProcCfg.Exceptional)) +module CheckerAnalyzer = + AbstractInterpreter.MakeRPO (TransferFunctions (CheckerMode) (CFG)) ``` -The `ProcCfg.Backward(ProcCfg.Exceptional)` part says: "I want the direction of +The `ProcCfg.Backward (ProcCfg.Exceptional)` part says: "I want the direction of iteration to be backward" (since liveness is a backward analysis), and "I want to the analysis to follow exceptional edges". For a forward analysis that ignores exceptional edges, you would do `ProcCfg.Normal` instead (and many other @@ -60,45 +58,46 @@ combinations are possible; take a look at for more). And finally, the `TransferFunctions` part says "Use the transfer functions I defined above". -Now you have an `Analyzer` module that exposes useful functions like +Now you have a `CheckerAnalyzer` module that exposes useful functions +like [`compute_post`](https://github.com/facebook/infer/blob/master/infer/src/absint/AbstractInterpreter.mli#L30) (take a procedure as input and compute a postcondition) and [`exec_pdesc`](https://github.com/facebook/infer/blob/master/infer/src/absint/AbstractInterpreter.mli#L36) -(take a procedure and compute an invariant map from node id's to the pre/post at -each node). The next step is to hook your checker up to the Infer CLI. For the -liveness analysis, you would do this by exposing a function for running the -checker on a single procedure: - -``` -let checker { Callbacks.proc_desc; tenv; } = - match Analyzer.compute_post (ProcData.make_default proc_desc tenv) with - | Some post -> Logging.progress "Computed post %a for %a" Analyzer.Domain.pp post Typ.Procname.pp (Procdesc.get_proc_name proc_desc); +(take a procedure and compute an invariant map from node id's to the +pre/post at each node). The next step is to hook your checker up to +the Infer command-line interface (CLI). For the liveness analysis, you +would do this by exposing a function for running the checker on a +single procedure: + +```OCaml +let checker ({IntraproceduralAnalysis.proc_desc; err_log} as analysis_data) = + match Analyzer.compute_post analysis_data ~initial:Domain.empty with + | Some post -> + Logging.progress "Computed post %a for %a" + Domain.pp post Procname.pp (Procdesc.get_proc_name proc_desc); | None -> () ``` -and then adding `Liveness.checker, checkers_enabled` to the list of registered -checkers -[here](https://github.com/facebook/infer/blob/master/infer/src/checkers/registerCheckers.ml#L42). +and then adding `Liveness.checker` to the list of registered checkers +in +[registerCheckers.ml](https://github.com/facebook/infer/blob/master/infer/src/backend/registerCheckers.ml) +(search for "Liveness"). -you can then run `infer run -a checkers -- ` to run your +you can then run `infer run --liveness-only -- ` to run your checker on real code. See [here](/docs/analyzing-apps-or-projects) for more details on the build systems supported by Infer. Other examples of simple intraprocedural checkers are [addressTaken.ml](https://github.com/facebook/infer/blob/master/infer/src/checkers/addressTaken.ml) and -[copyPropagation.ml](https://github.com/facebook/infer/blob/master/infer/src/checkers/copyPropagation.ml). +[Siof.ml](https://github.com/facebook/infer/blob/master/infer/src/checkers/Siof.ml). -## Basic error reporting +## Error reporting -Useful analyses have output. Basic printing to stderr or stderr is good for -debugging, but to report a programmer-readable error that is tied to a source -code location, you'll want to use `Reporting.log_error`. Some examples of -error-logging code: -[1](https://github.com/facebook/infer/blob/master/infer/src/concurrency/RacerD.ml#L166), -[2](https://github.com/facebook/infer/blob/master/infer/src/checkers/annotationReachability.ml#L224), -or -[3](https://github.com/facebook/infer/blob/master/infer/src/quandary/TaintAnalysis.ml#L186). +Useful analyses have output. Basic printing to stderr or stderr is +good for debugging, but to report a programmer-readable error that is +tied to a source code location, you'll want to use +[`Reporting.log_issue`](/odoc/next/infer/Absint/Reporting/index.html#val-log_issue). ## By example: interprocedural analysis @@ -110,187 +109,61 @@ more; global analyses cannot be expressed in this framework. To make your checker interprocedural, you need to: -(1) Define the type of procedure summaries for your analysis and add some -boilerplate for storing your data alongside the summaries for other analyses +1. Define the type of procedure summaries for your analysis and let +registerCheckers.ml know that your checker is interprocedural -(2) Add logic for (a) using summaries in your transfer functions and (b) +2. Add logic for (a) using summaries in your transfer functions and (b) converting your intraprocedural abstract state to a summary. A good example to look at here is -[siof.ml](https://github.com/facebook/infer/blob/master/infer/src/checkers/Siof.ml). +[Siof.ml](https://github.com/facebook/infer/blob/master/infer/src/checkers/Siof.ml). Step (1) is just: -``` -module Summary = Summary.Make (struct - type summary = SiofDomain.astate +```OCaml +(* in src/checkers/SiofDomain.ml *) +(* note that as a result the type of summaries is the same as the type of domain + elements *) +module Summary = ... +include Summary + + +(* in src/backend/Payloads.ml: register the payload of the analyzer *) +type t = + { ... + ; siof: SiofDomain.Summary.t option + ... } - let update_payload astate payload = - { payload with Specs.siof = Some astate } - let read_from_payload payload = - payload.Specs.siof - end) +(* in src/backend/registerCheckers.ml *) +let all_checkers = [ ... + ; {checker= SIOF; callbacks= [(interprocedural Payloads.Fields.siof Siof.checker, Clang)]} + ... ] ``` -along with adding the `Specs.siof` -[field](https://github.com/facebook/infer/blob/master/infer/src/backend/specs.ml#L329) -to the `Specs.payload` record -[type](https://github.com/facebook/infer/blob/master/infer/src/backend/specs.ml#L321). Here, the type of the abstract state and the type of the summary are the same, which makes things easier for us (no logic to convert an abstract state to a summary). Part (2a) is -[here](https://github.com/facebook/infer/blob/master/infer/src/checkers/Siof.ml#L65): +[here](https://github.com/facebook/infer/blob/be4ddc48f6330b7b788d899ce12ca51b4d673530/infer/src/checkers/Siof.ml#L168) +and uses the `analyze_dependency` callback provided by the framework: ``` -match Summary.read_summary pdesc callee_pname with +match analyze_dependency callee_pname with ``` -This says: "read the summary for `callee_pname` from procedure `pdesc` with type -environment `tenv`". You must then add logic for applying the summary to the +This says: "read the summary for `callee_pname`, possibly computing it +first". You must then add logic for applying the summary to the current abstract state (often, this is as simple as doing a join). -Because our summary type is the same as the abstract state, part (2b) can be -done for us by making use of the convenient -`AbstractInterpreter.Interprocedural` -[functor](https://github.com/facebook/infer/blob/master/infer/src/absint/AbstractInterpreter.mli#L19) -(for an example of what to do when the types are different, take a look at -[Quandary](https://github.com/facebook/infer/blob/master/infer/src/quandary/TaintAnalysis.ml#L540)): - -``` -module Interprocedural = Analyzer.Interprocedural (Summary) -``` - -This `Interprocedural` module will automatically do the work of computing and -storing the summary for us. All we need to do is change the exposed `checker` -function registered in `registerCheckers.ml` to call `Interprocedural.checker` -instead: - -``` -let checker callback = - ignore(Interprocedural.checker callback ProcData.empty_extras in) -``` +Because our summary type is the same as the abstract state, part (2b) +here simply consists in return the post computed by the analysis as +the procedure's summary, using `Analyzer.compute_post`. That's it! We now have an interprocedural analysis. -One very important note here: a current (and soon-to-be-lifted) limitation -prevents us from running multiple interprocedural checkers at the same time. If -you register an interprocedural checker, be sure to unregister the other other -ones. Otherwise, there's a risk that the checkers will clobber each other's -results. - -## Relevant code - -Some pointers to useful code for building new analyses, and to the -implementation of the framework for the interested: - -Domain combinators: - -- `AbstractDomain.BottomLifted`, `AbstractDomain.FiniteSet`, - `AbstractDomain.Map`, `AbstractDomain.Pair` (all in - [AbstractDomain](https://github.com/facebook/infer/blob/master/infer/src/checkers/AbstractDomain.mli)) - -Domains and domain building blocks: - -- [AccessPath](https://github.com/facebook/infer/blob/master/infer/src/checkers/accessPath.mli) -- [AccessPathDomains](https://github.com/facebook/infer/blob/master/infer/src/checkers/accessPathDomains.mli) -- [AccessTree](https://github.com/facebook/infer/blob/master/infer/src/checkers/accessTree.ml) - -Reporting errors with interprocedural traces: - -- Examples: - [`SiofTrace.ml`](https://github.com/facebook/infer/blob/master/infer/src/checkers/SiofTrace.ml), - [`JavaTrace.ml`](https://github.com/facebook/infer/blob/master/infer/src/quandary/JavaTrace.ml), - [`CppTrace.ml`](https://github.com/facebook/infer/blob/master/infer/src/quandary/CppTrace.ml). -- Implementation: - [`Trace`](https://github.com/facebook/infer/blob/master/infer/src/checkers/Trace.mli) - -Implementation: - -- [`AbstractDomain`](https://github.com/facebook/infer/blob/master/infer/src/absint/AbstractDomain.ml) -- [`TransferFunctions`](https://github.com/facebook/infer/blob/master/infer/src/absint/AbstractInterpreter.mli) -- [`AbstractInterpreter`](https://github.com/facebook/infer/blob/master/infer/src/absint/AbstractInterpreter.mli) -- [`ProcCFG`](https://github.com/facebook/infer/blob/master/infer/src/absint/ProcCfg.mli) -- [`Summary`](https://github.com/facebook/infer/blob/master/infer/src/absint/Summary.ml) -- [`Scheduler`](https://github.com/facebook/infer/blob/master/infer/src/absint/Scheduler.ml) - -## IR basics: SIL, CFG's, `tenv`'s, `procdesc`'s, and `procname`'s - -All of the languages analyzed by Infer are converted into a common intermediate -representation. A program is represented as a control-flow graph -([CFG](https://github.com/facebook/infer/blob/master/infer/src/IR/Cfg.rei)) -whose nodes contain lists of instructions in the SIL language. SIL is a small -low-level language that has some similarities with C, LLVM -[IR](http://llvm.org/docs/LangRef.html), and -[Boogie](https://research.microsoft.com/en-us/um/people/leino/papers/krml178.pdf). - -[Expressions](https://github.com/facebook/infer/blob/master/infer/src/IR/Exp.rei#L25) -are literals, program variables (`Pvar`'s), temporary variables (`Ident`'s), a -field offset from a struct (OO features like objects are lowered into struct's), -or an index offset from an array. - -There are four interesting kinds of -[instructions](https://github.com/facebook/infer/blob/master/infer/src/IR/Sil.rei#L38): -`Load` for reading into a temporary variable, `Store` for writing to a program -variable, field of a struct, or an array, `Prune e` (often called `assume` in -other PL formalisms) blocks execution unless the expression `e` evaluates to -true, and `Call` represents function calls. - -Instructions and expressions have -[types](https://github.com/facebook/infer/blob/master/infer/src/IR/Typ.rei#L76). -A `Tstruct` (think: object) type has a -[`Typename`](https://github.com/facebook/infer/blob/master/infer/src/IR/Typename.rei#L13), -and it is often useful to look up metadata about the type (what fields does it -have, what methods does it declare, what is its superclass, etc.) in the type -environment, or -[`tenv`](https://github.com/facebook/infer/blob/master/infer/src/IR/Tenv.rei#L37). - -A procedure description or -[`procdesc`](https://github.com/facebook/infer/blob/master/infer/src/IR/Procdesc.rei) -(sometimes abbreviated `pdesc`) is an abstraction of a procedure declaration: it -stores the CFG of the procedure, its signature, its annotations, and so on. - -A procedure name or -[`procname`](https://github.com/facebook/infer/blob/master/infer/src/IR/Procname.rei) -(sometimes abbreviated `pname`) is an abstraction of a called procedure name. -One procname may correspond to multiple (or zero) `procdesc`'s after resolution. - -## Framework-specific IR: `ProcCFG`, `ProcData`, and `extras` - -The abstract interpretation framework has a few additional constructs that are -worth explaining. - -A -[`ProcCfG`](https://github.com/facebook/infer/blob/master/infer/src/absint/procCfg.mli) -represents the CFG of a _single_ procedure whereas (perhaps confusingly) a -[`Cfg`](https://github.com/facebook/infer/blob/master/infer/src/IR/Cfg.rei) is -the CFG for an entire file. A `ProcCfg` is really a customizable view of the -underlying procedure CFG; we can get a view the CFG with its edges backward -(`ProcCfg.Backward`), with or without exceptional edges (`Normal`/`Exceptional`, -respectively), or with each node holding at most one instruction -(`OneInstrPerNode`). - -[`ProcData`](https://github.com/facebook/infer/blob/master/infer/src/absint/procData.mli) -is a container that holds all of the read-only information required to analyze a -single procedure: procedure description, and `extras`. The `extras` are custom -read-only data that are computed before analysis begins, and can be accessed -from the transfer functions. Most often, no extras are required for analysis -(`ProcData.empty_extras`), but it can be useful to stash information like a map -from a formal to its -[index](https://github.com/facebook/infer/blob/master/infer/src/quandary/TaintAnalysis.ml#L88) -or an invariant -[map](https://github.com/facebook/infer/blob/master/infer/src/backend/preanal.ml#L115) -from a prior analysis in the extras. - -## How it works - -Coming soon. - -## Intro: abstract interpretation - -Coming soon. - -## How do I make an analysis compositional? - -Coming soon. +To go deeper, jump to the [lab +exercise](https://github.com/facebook/infer/blob/master/infer/src/labs/README.md) +and to the [API documentation](internal-API/), e.g. for the +[Absint](/odoc/next/infer/Absint.html) and +[IR](/odoc/next/infer/IR.html) modules. diff --git a/website/docs/04-adding-checkers.md b/website/docs/04-adding-checkers.md deleted file mode 100644 index 18e4161d7..000000000 --- a/website/docs/04-adding-checkers.md +++ /dev/null @@ -1,210 +0,0 @@ ---- -id: adding-checkers -title: Simple intraprocedural checkers ---- - -## How can I create my own checkers? - -Infer Checkers provide a framework to perform intra-procedural static analyses. -Since this is an open source project, everyone is welcome to contribute with new -great checkers. In this page, we will create a very basic checker - a detector -for every time the output method `java.io.PrintStream.println` is called. This -should be enough to get you started. - -## Before you start - -Make sure you are able to successfully build Infer and your developer -environment is set up: - -``` -./build-infer.sh -make devsetup -``` - -Get familiar with Infer checkers and run Infer with some examples: - -``` -infer run -- javac Hello.java -``` - -In addition, get familiar with the Control Flow Graph (CFG) that Infer generates -for you: - -``` -infer run -g -- javac Hello.java -dot -Tpdf infer-out/captured/Hello.java*/icfg.dot -o icfg.pdf -open icfg.pdf -``` - -This will give you further information about the analysis that is being done, -including the CFG in dot format. It is important that you understand the -generated CFG since this is the abstraction of code that Checkers will analyze. - -Infer is built with [OCaml](https://ocaml.org). This is a programming language -that combines both functional and imperative programming. If you are not -familiar with OCaml, it might be hard at the beginning to understand the code. -Take your time to review the -[basics](https://ocaml.org/learn/tutorials/basics.html) and do some -[exercises](https://ocaml.org/learn/tutorials/99problems.html). - -## Let's go - -The directory `infer/src/absint` contains utilities for the abstract -interpretation framework that checkers are based on. - -Looking into `infer/src/checkers` we can find some simple checkers. Most of them -are implemented as a module created from a `TransferFunctions` module that is -turned into an analyzer by applying one of the `AbstractInterpreter.Make*` -functors, together with a `checker` function that calls into it. You can start -by copying the code for one of these and modify it (eg -checkers/SimpleChecker.ml). For example: - -```ocaml -module TransferFunctions = struct - ... - let exec_instr astate proc_data cfg_node (instr : Sil.instr) = - match instr with - | pattern -> - ST.report_error - proc_name - proc_desc - "CHECKERS_MY_SIMPLE_CHECKER" - location - "A description of my simple checker" - | _ -> astate -end - -module Analyzer = AbstractInterpreter.Make (TransferFunctions) - -let checker {Callbacks.exe_env; summary; get_procs_in_file} : Summary.t = - let proc_name = Summary.get_proc_name summary in - let tenv = Exe_env.get_tenv exe_env proc_name in - let proc_data = ProcData.make_default summary tenv in - ignore (Analyzer.compute_post proc_data ~initial) ; - summary -``` - -Checkers implement a function that detects a given pattern for our specific -checker and then calls `AbstractInterpreter.Make` to iterate over all the nodes -of the CFG. - -So now we need to know how to create our pattern. As an example, consider the -following: - -```ocaml -Sil.Call (_, Sil.Const (Sil.Cfun pn), _, loc, _) -``` - -This pattern matches every function call. In our code, it would look like: - -```ocaml - let exec_instr astate proc_data cfg_node (instr : Sil.instr) = - match instr with - | Call (_, Const (Cfun pn), _, loc, _) -> - ST.report_error - proc_name - proc_desc - "CHECKERS_MY_SIMPLE_CHECKER" - location - "A description of my simple checker" - | _ -> astate -``` - -The `absint/PatternMatch.ml` module contains the -`java_proc_name_with_class_method` function which we can use for matching the -required pattern. - -Each node is represented using the type `instr` from the Smallfoot Intermediate -Language (SIL). Take a look at `IR/Sil.mli` to get familiar with all the types. -All source code languages supported by Infer are converted to this -representation. - -In this particular example, `Sil.Call` has the following information: - -```ocaml -Sil.Call ( - list_of_return_values, - Sil.Const (Const.Cfun name_of_function), - list_of_arguments, - location, - call_flags -) -``` - -I hope this looks straight forward. Argument `call_flags` holds information -about the function, such as whether it is virtual or not. Again, this is -specified in the file `Sil.mli`. - -The Checker we have written so far is able to detect every single function call. -Now, we have to detect whether a specific function call is actually calling -`java.io.PrintStream.println`. - -Let's try this: - -```ocaml - let is_println pln = match pln with - | Procname.Java pn_java -> - PatternMatch.java_proc_name_with_class_method - pn_java "java.io.PrintStream" "println" - | _ -> - false in - - let exec_instr astate proc_data cfg_node (instr : Sil.instr) = - match instr with - | Call (_, Const (Cfun pn), _, loc, _) when is_println pn -> - ST.report_error - proc_name - proc_desc - "CHECKERS_MY_SIMPLE_CHECKER" - location - "A description of my simple checker" - | _ -> astate - -``` - -Can you spot the difference? A new restriction was added to our pattern -- -`is_println` expression helps us to check whether the current method is a -`java.io.PrintStream.println` method or not. - -So our implementation is done. Now we have to register it as an enabled Checker -in `checkers/registerCheckers.ml`. - -Assuming the code is in SimpleCheckers.ml, you would register your checker as a -_java_checker_ in `checkers/registerCheckers.ml` by adding it to the -`all_checkers` list: - -```ocaml -let all_checkers = - [ { name= "my simple checker" - ; active= true - ; callbacks= [(Procedure SimpleChecker.checker, Language.Java)] } - ; (* the rest of the list as it was there *) - ... ] -``` - -Build Infer with `./build-infer.sh` and your first Checker is ready! - -If you want you can try with this java example: - -```java -/*Hello.java*/ -class Hello { - int println(){ - return 0; - } - int test() { - String s = "Hello World"; - System.out.println(s); - s = null; - println(); - return s.length(); - } -} -``` - -Notice that only `System.out.println` is being detected. - -All set! You are ready to create your own Checkers! Infer is an open source -project and you are more than welcome to contribute. Take a look at the -[Github](https://github.com/facebook/infer/) page and feel free to fork or even -open an issue if you're facing any trouble. diff --git a/website/sidebars.js b/website/sidebars.js index d7aa24300..28a879af1 100644 --- a/website/sidebars.js +++ b/website/sidebars.js @@ -32,7 +32,7 @@ module.exports = { "about-Infer", "separation-logic-and-bi-abduction", ], - Contribute: ["absint-framework", "adding-checkers", "internal-API"], + Contribute: ["absint-framework", "internal-API"], Versions: ["versions"], }, };