[Topl] add doc and change TOPL -> Topl

Summary:
Copied the documentation from a document created by rgrig
(thanks!!).

Reviewed By: rgrig

Differential Revision: D27325829

fbshipit-source-id: 118e1a2be

infer/documentation/checkers/Topl.md

@@ -0,0 +1,97 @@
+# Topl
+
+## What is it?
+
+Topl is an analysis framework, built on top of Infer, for statically finding violations of temporal properties. Many analyses can be encoded as temporal properties supported by Topl, such as taint analysis. As a simple example, suppose that we don't want a value returned by method `source()` to be sent as an argument to a method `sink()`. This can be specified as follows:
+
+```
+property Taint
+  prefix "Main"
+  start -> start: *
+  start -> tracking: source(Ret) => x := Ret
+  tracking -> error: sink(Arg, VoidRet) when x == Arg
+```
+
+This specifies an automaton called `Taint` that has three states (`start`, `tracking`, `error`). Two of those states (`start` and `error`) have special meaning; other states (`tracking`) can have any names. The first transition (`start → tracking`) is taken when a method called `source()` is called, and its return value is stored in a register called `x`; the second transition (`tracking → error`) is taken when a method called `sink()` is called, but only if its argument equals what was previously saved in register `x`.
+This property is violated in the following Java code:
+
+```
+public class Main {
+  static void f() { g(tito(source())); }
+  static void g(Object x) { h(x); }
+  static void h(Object x) { sink(x); }
+  static Object tito(Object x) { return x; }
+  static Object source() { return "dirty"; }
+  static void sink(Object x) {}
+}
+```
+
+Note that `source()` and `sink()` are not called from the same method, and that the “dirty” object is passed around a few times before finally reaching the sink. Assuming that the property is in a file `taint.topl` and the Java code in a file `Main.java`, you can invoke Infer with the following command:
+
+```
+infer --topl --topl-properties taint.topl  -- javac Main.java
+```
+
+It will display the following error:
+
+```
+Main.java:2: error: Topl Error
+  property Taint reaches state error.
+  1.   public class Main {
+  2. >   static void f() { g(tito(source())); }
+  3.     static void g(Object x) { h(x); }
+  4.     static void h(Object x) { sink(x); }
+```
+
+To get a full trace, use the command
+
+```
+infer explore
+```
+
+## Specifying Properties
+
+A property is a nondeterministic automaton that can remember values in registers. An execution that drives the automaton from the start state to the error state will make Infer report an issue, and the trace that it produces will indicate which parts of the program drive which transitions of the automaton.
+
+The general form of a property is the following:
+
+```
+property *Name
+*  message "Optional error message" // This line can be missing
+  prefix "Prefix" // There can be zero, one, or more prefix declarations
+  sourceState -> targetState: *Pattern*(Arg1,...,ArgN,Ret) when *Condition* => *Action*
+```
+
+The property name and the optional error message are used for reporting issues. The prefix declarations are used to simplify Patterns. The core of the property is the list of transitions.
+
+Each transition has a source state and a target state. The special transition label * means that the transition is always taken. Typically, there is a transition
+
+```
+  start -> start: *
+```
+
+meaning that the property can start anywhere, not just at the beginning of a method.
+
+Otherwise, the label on a transition contains:
+
+* a *Pattern*, which indicates what kind of instruction in the program drives this transition;
+* a list of transition variable bindings (above named Arg1, ..., but any identifier starting with uppercase letters works);
+* possibly a boolean Condition, which can refer to transition variables and to registers;
+* possibly and Action, which is a list sequence of assignments of the form *register* := *TransitionVariable* (registers do not need to be declared, and any identifier starting with a lowercase letter works).
+
+There are two types of patterns:
+
+* a regex that matches method names
+    * if the regex uses non-letters (such as dots) it must be within double-quotes; otherwise, double quotes are optional
+    * the prefix declarations are used to add potential prefixes to the regex. The combine regex is essentially “(prefix_regex_a | prefix_regex_b) transition_pattern_regex“
+    * for a method with n arguments, there must be n+1 transition variables to get a match. The first n transition variables get bound to the argument values, and the last transition variable gets bound to the return value. *This is true even for the case in which the return type is void*.
+* the special keyword **#ArrayWrite**. In that case, there should be two transition variables like “(Array, Index)” — Array gets bound to the array object, and Index gets bound to the index at which the write happens.
+
+For several examples, see https://github.com/facebook/infer/tree/master/infer/tests/codetoanalyze/java/topl
+
+## Limitations
+
+* By design, some problems may be missed. Topl is built on Pulse, which attempts to minimize false positives, at the cost of sometimes having false negatives.
+* Analysis time increases exponentially with the number of registers used in properties.
+    * In theory, there should be no significant slowdown if registers belong to different properties, but the implementation is not yet optimized.
+    * If there are many registers within the same property, then the slowdown is unavoidable (without some significant breakthrough). However, the maximum number of registers we ever used for one practical property was 3.

infer/man/man1/infer-analyze.txt

@@ -411,9 +411,9 @@ OPTIONS
            (Conversely: --no-starvation-only)
 
        --topl
-           Activates: checker topl: Detects errors based on user-provided
-           state machines describing multi-object monitors. (Conversely:
-           --no-topl)
+           Activates: checker topl: Detect errors based on user-provided
+           state machines describing temporal properties over multiple
+           objects. (Conversely: --no-topl)
 
        --topl-only
            Activates: Enable topl and disable all other checkers (Conversely:

infer/man/man1/infer-full.txt

@@ -1257,9 +1257,9 @@ OPTIONS
            @ThreadSafe           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).
+           Activates: checker topl: Detect errors based on user-provided
+           state machines describing temporal properties over multiple
+           objects. (Conversely: --no-topl)           See also infer-analyze(1).
 
        --topl-only
            Activates: Enable topl and disable all other checkers (Conversely:
@@ -2126,7 +2126,7 @@ INTERNAL OPTIONS
            scheduler. (Conversely: --no-trace-ondemand)
 
        --trace-topl
-           Activates: Detailed tracing information during TOPL analysis
+           Activates: Detailed tracing information during Topl analysis
            (Conversely: --no-trace-topl)
 
        --tv-commit commit

infer/man/man1/infer.txt

@@ -1257,9 +1257,9 @@ OPTIONS
            @ThreadSafe           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).
+           Activates: checker topl: Detect errors based on user-provided
+           state machines describing temporal properties over multiple
+           objects. (Conversely: --no-topl)           See also infer-analyze(1).
 
        --topl-only
            Activates: Enable topl and disable all other checkers (Conversely:

infer/src/backend/dune

@@ -10,9 +10,9 @@
   (:standard -open Core -open IStdlib -open IStd -open OpenSource -open
     ATDGenerated -open IBase -open IR -open Absint -open Biabduction -open BO
     -open Nullsafe -open Pulselib -open Checkers -open Costlib -open Quandary
-    -open TOPLlib -open Concurrency -open Labs -open Dotnet))
+    -open Topllib -open Concurrency -open Labs -open Dotnet))
  (libraries core memtrace IStdlib ATDGenerated IBase IR Absint Biabduction
-   Nullsafe BO Checkers Costlib Quandary TOPLlib Concurrency Labs Dotnet)
+   Nullsafe BO Checkers Costlib Quandary Topllib Concurrency Labs Dotnet)
  (preprocess
   (pps ppx_compare ppx_fields_conv ppx_yojson_conv)))
 

infer/src/base/Checker.ml

@@ -37,7 +37,7 @@ type t =
   | SIOF
   | SelfInBlock
   | Starvation
-  | TOPL
+  | Topl
   | Uninit
 [@@deriving equal, enumerate]
 
@@ -409,12 +409,14 @@ let config_unsafe checker =
       ; cli_flags= Some {deprecated= []; show_in_help= true}
       ; enabled_by_default= true
       ; activates= [] }
-  | TOPL ->
+  | Topl ->
       { id= "topl"
-      ; kind= UserFacing {title= "TOPL"; markdown_body= ""}
+      ; kind=
+          UserFacing {title= "Topl"; markdown_body= [%blob "../../documentation/checkers/Topl.md"]}
       ; support= supports_clang_and_java_experimental
       ; short_documentation=
-          "Detects errors based on user-provided state machines describing multi-object monitors."
+          "Detect errors based on user-provided state machines describing temporal properties over \
+           multiple objects."
       ; cli_flags= Some {deprecated= []; show_in_help= true}
       ; enabled_by_default= false
       ; activates= [Pulse] }

infer/src/base/Checker.mli

@@ -36,7 +36,7 @@ type t =
   | SIOF
   | SelfInBlock
   | Starvation
-  | TOPL
+  | Topl
   | Uninit
 [@@deriving equal, enumerate]
 

infer/src/base/Config.ml

@@ -2500,7 +2500,7 @@ and trace_ondemand =
 
 
 and trace_topl =
-  CLOpt.mk_bool ~long:"trace-topl" "Detailed tracing information during TOPL analysis"
+  CLOpt.mk_bool ~long:"trace-topl" "Detailed tracing information during Topl analysis"
 
 
 and tv_commit =

infer/src/base/IssueType.ml

@@ -920,7 +920,10 @@ let complexity_increase ~kind ~is_on_ui_thread =
   register_cost ~kind ~is_on_ui_thread "%s_COMPLEXITY_INCREASE"
 
 
-let topl_error = register ~id:"TOPL_ERROR" Error TOPL ~user_documentation:"Experimental."
+let topl_error =
+  register ~id:"TOPL_ERROR" Error Topl
+    ~user_documentation:"A violation of a Topl property (user-specified)."
+
 
 let uninitialized_value =
   register ~id:"UNINITIALIZED_VALUE" Error Uninit

infer/src/dune.in

@@ -99,7 +99,7 @@ let infertop_stanza =
  (modes byte_complete)
  (modules Infertop)
  (flags (:standard -open Core -open IStdlib -open IStd))
- (libraries %s utop Absint ASTLanguage ATDGenerated Backend IBase Biabduction BO Checkers Concurrency Costlib CStubs IR IStdlib Labs Dotnet Nullsafe Pulselib Quandary Integration TestDeterminators TOPLlib UnitTests)
+ (libraries %s utop Absint ASTLanguage ATDGenerated Backend IBase Biabduction BO Checkers Concurrency Costlib CStubs IR IStdlib Labs Dotnet Nullsafe Pulselib Quandary Integration TestDeterminators Topllib UnitTests)
  (link_flags (-linkall -warn-error -31))
  (preprocess (pps ppx_compare))
  (promote (until-clean) (into ../bin))

infer/src/pulse/PulseAbductiveDomain.ml

@@ -99,7 +99,7 @@ type t =
 [@@deriving compare, equal, yojson_of]
 
 let pp f {post; pre; topl; path_condition; skipped_calls} =
-  F.fprintf f "@[<v>%a@;%a@;PRE=[%a]@;skipped_calls=%a@;TOPL=%a@]" PathCondition.pp path_condition
+  F.fprintf f "@[<v>%a@;%a@;PRE=[%a]@;skipped_calls=%a@;Topl=%a@]" PathCondition.pp path_condition
     PostDomain.pp post PreDomain.pp pre SkippedCalls.pp skipped_calls PulseTopl.pp_state topl
 
 

infer/src/pulse/PulseTopl.ml

@@ -246,7 +246,7 @@ let get env x =
   | Some v ->
       v
   | None ->
-      L.die InternalError "TOPL: Cannot find %s. Should be caught by static checks" x
+      L.die InternalError "Topl: Cannot find %s. Should be caught by static checks" x
 
 
 let set = List.Assoc.add ~equal:String.equal
@@ -378,7 +378,7 @@ let dummy_tenv = Tenv.create ()
 
 let is_unsat_expensive path_condition pruned =
   let _path_condition, unsat, _new_eqs =
-    (* Not enabling dynamic type reasoning in TOPL for now *)
+    (* Not enabling dynamic type reasoning in Topl for now *)
     PathCondition.is_unsat_expensive dummy_tenv
       ~get_dynamic_type:(fun _ -> None)
       (Constraint.prune_path pruned path_condition)
@@ -614,6 +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 TOPL IssueType.topl_error message
+        Reporting.log_issue proc_desc err_log ~loc ~ltr Topl IssueType.topl_error message
   in
   List.iter ~f:report_simple_state state

infer/src/pulse/dune

@@ -8,7 +8,7 @@
  (public_name infer.Pulselib)
  (flags
   (:standard -open Core -open IR -open IStdlib -open IStd -open ATDGenerated
-    -open IBase -open Absint -open BO -open TOPLlib -open Nullsafe))
- (libraries core IStdlib ATDGenerated IBase IR Absint BO TOPLlib Nullsafe)
+    -open IBase -open Absint -open BO -open Topllib -open Nullsafe))
+ (libraries core IStdlib ATDGenerated IBase IR Absint BO Topllib Nullsafe)
  (preprocess
   (pps ppx_yojson_conv ppx_compare ppx_variants_conv)))

infer/src/topl/Topl.ml

@@ -25,4 +25,4 @@ let properties = lazy (List.concat_map ~f:parse Config.topl_properties)
 
 let automaton () = ToplAutomaton.make (Lazy.force properties)
 
-let is_active () = Config.is_checker_enabled TOPL && not (List.is_empty (Lazy.force properties))
+let is_active () = Config.is_checker_enabled Topl && not (List.is_empty (Lazy.force properties))

infer/src/topl/ToplAutomaton.mli

@@ -7,7 +7,7 @@
 
 open! IStd
 
-(* An automaton is a different representation for a set of TOPL properties: states and transitions
+(* An automaton is a different representation for a set of Topl properties: states and transitions
    are identified by nonnegative integers; and transitions are grouped by their source. Also, the
    meaning of transition labels does not depend on context (e.g., prefixes are now included).
 

infer/src/topl/dune

@@ -10,8 +10,8 @@
  (modules ToplParser))
 
 (library
- (name TOPLlib)
- (public_name infer.TOPLlib)
+ (name Topllib)
+ (public_name infer.Topllib)
  (flags
   (:standard -open Core -open IR -open IStdlib -open IStd -open ATDGenerated
     -open IBase -open Absint -open Biabduction))

scripts/toplevel_init

@@ -29,7 +29,7 @@ open Pulselib;;
 open Checkers;;
 open Costlib;;
 open Quandary;;
-open TOPLlib;;
+open Topllib;;
 open Concurrency;;
 open Labs;;
 open OpenSource;;

website/docs/all-issue-types.md

@@ -2230,7 +2230,7 @@ These annotations can be found at `com.facebook.infer.annotation.*`.
 
 Reported as "Topl Error" by [topl](/docs/next/checker-topl).
 
-Experimental.
+A violation of a Topl property (user-specified).
 ## UNINITIALIZED_VALUE
 
 Reported as "Uninitialized Value" by [uninit](/docs/next/checker-uninit).