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: 78b541746master
Jules Villard
4 years ago
committed by
Facebook GitHub Bot
parent
8fde3f2479
commit
7eba62c9ed
@ -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
|
|
||||||
@ -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
|
|
||||||
@ -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.
|
|
||||||
Loading…
Reference in new issue