[topl] Parser for temporal properties

Summary:
TOPL properties are essentially automata, which specify a bad pattern.
This commit is just a parser for them.

Reviewed By: jvillard

Differential Revision: D14477671

fbshipit-source-id: c38a8ef37

Makefile

@@ -141,6 +141,7 @@ DIRECT_TESTS += \
   java_quandary \
   java_racerd \
   java_starvation \
+  java_topl \
   java_tracing \
 
 ifneq ($(ANT),no)

infer/man/man1/infer-full.txt

@@ -1485,6 +1485,13 @@ INTERNAL OPTIONS
            Activates: Mode for testing, where no headers are translated, and
            dot files are created (clang only) (Conversely: --no-testing-mode)
 
+       --topl-properties +path
+           [EXPERIMENTAL] Specify a file containing a temporal property
+           definition (e.g., jdk.topl).
+
+       --topl-properties-reset
+           Set --topl-properties to the empty list.
+
        --trace-error
            Activates: Detailed tracing information during error explanation
            (Conversely: --no-trace-error)

infer/src/base/Config.ml

@@ -2136,6 +2136,11 @@ and test_filtering =
     "List all the files Infer can report on (should be called from the root of the project)"
 
 
+and topl_properties =
+  CLOpt.mk_path_list ~default:[] ~long:"topl-properties"
+    "[EXPERIMENTAL] Specify a file containing a temporal property definition (e.g., jdk.topl)."
+
+
 and profiler_samples =
   CLOpt.mk_path_opt ~long:"profiler-samples"
     "File containing the profiler samples when Infer is run Test Determinator mode with \
@@ -2989,6 +2994,8 @@ and testing_mode = !testing_mode
 
 and threadsafe_aliases = !threadsafe_aliases
 
+and topl_properties = !topl_properties
+
 and trace_error = !trace_error
 
 and trace_events = !trace_events

infer/src/base/Config.mli

@@ -654,6 +654,8 @@ val racerd : bool
 
 val threadsafe_aliases : Yojson.Basic.json
 
+val topl_properties : string list
+
 val trace_error : bool
 
 val trace_events : bool

infer/src/biabduction/interproc.ml

@@ -1257,6 +1257,7 @@ let analyze_procedure_aux summary exe_env tenv proc_desc : Summary.t =
 let analyze_procedure {Callbacks.summary; proc_desc; tenv; exe_env} : Summary.t =
   (* make sure models have been registered *)
   BuiltinDefn.init () ;
+  if not (List.is_empty Config.topl_properties) then Topl.init () ;
   try analyze_procedure_aux summary exe_env tenv proc_desc with exn ->
     IExn.reraise_if exn ~f:(fun () -> not (Exceptions.handle_exception exn)) ;
     Reporting.log_error_using_state summary exn ;

infer/src/deadcode/Makefile

@@ -46,7 +46,7 @@ depend:
 	ocamldep -native \
 	  -I IR -I absint -I atd -I backend -I base -I biabduction -I bufferoverrun -I checkers \
 	  -I clang -I concurrency -I facebook -I integration -I istd -I java \
-	  -I labs -I nullsafe -I quandary -I unit -I unit/clang -I deadcode \
+	  -I labs -I nullsafe -I quandary -I topl -I unit -I unit/clang -I deadcode \
 	   $(ml_src_files) > deadcode/.depend
 
 # circular dependency... not sure how to fix properly

infer/src/dune.in

@@ -23,6 +23,7 @@ let source_dirs =
        ; "labs"
        ; "nullsafe"
        ; "quandary"
+       ; "topl"
        ; "unit" ] )
 
 
@@ -50,7 +51,9 @@ let infer_cflags =
 let stanzas =
   ( if clang then ["(ocamllex types_lexer ctl_lexer)"; "(menhir (modules types_parser ctl_parser))"]
   else [] )
-  @ [ Format.sprintf
+  @ [ "(ocamllex ToplLexer)"
+    ; "(menhir (flags --unused-token INDENT) (modules ToplParser))"
+    ; Format.sprintf
         {|
 (library
  (name InferModules)

infer/src/topl/Topl.ml

@@ -0,0 +1,30 @@
+(*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * 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 initialized = ref false
+
+let properties = ref []
+
+let parse topl_file =
+  let f ch =
+    let lexbuf = Lexing.from_channel ch in
+    try ToplParser.properties (ToplLexer.token ()) lexbuf with ToplParser.Error ->
+      let Lexing.({pos_lnum; pos_bol; pos_cnum; _}) = Lexing.lexeme_start_p lexbuf in
+      let col = pos_cnum - pos_bol + 1 in
+      L.(die UserError) "@[%s:%d:%d: topl parse error@]@\n@?" topl_file pos_lnum col
+  in
+  try In_channel.with_file topl_file ~f with Sys_error msg ->
+    L.(die UserError) "@[topl:%s: %s@]@\n@?" topl_file msg
+
+
+let init () =
+  if not !initialized then (
+    properties := List.concat_map ~f:parse Config.topl_properties ;
+    initialized := true )

infer/src/topl/Topl.mli

@@ -0,0 +1,11 @@
+(*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * 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 init : unit -> unit
+(** Parse properties, mentioned by [Config.topl_properties]. Does this only once. *)

infer/src/topl/ToplAst.ml

@@ -0,0 +1,33 @@
+(*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * 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 register_name = string
+
+(** TODO: use Const.t *)
+type constant = string
+
+type value_pattern =
+  | Ignore
+  | SaveInRegister of register_name
+  | EqualToRegister of register_name
+  | EqualToConstant of constant
+
+(** a regular expression *)
+type procedure_name_pattern = string
+
+type label =
+  { return: value_pattern
+  ; procedure_name: procedure_name_pattern
+  ; arguments: value_pattern list option }
+
+type vertex = string
+
+type transition = {source: vertex; target: vertex; label: label}
+
+type t = {name: string; message: string option; prefixes: string list; transitions: transition list}

infer/src/topl/ToplLexer.mll

@@ -0,0 +1,76 @@
+(*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+{
+  open !IStd
+  open ToplParser
+
+  module L = Logging
+
+  let new_line x y lexbuf =
+    let m = x |> String.filter ~f:(Char.equal '\n') |> String.length in
+    let n = y |> String.length in
+    let open Lexing in
+    let lcp = lexbuf.lex_curr_p in
+    lexbuf.lex_curr_p <-
+      { lcp with pos_lnum = lcp.pos_lnum + m ; pos_bol = lcp.pos_cnum - n } ;
+    (INDENT n)
+
+  let quoted = Str.regexp "\\\\\\(.\\)"
+  let unquote x = Str.global_replace quoted "\\1" x
+
+  (* We open Caml, because ocamllex generates code that uses Array.make,
+  which is not available in Core. Ideally, this should go away. *)
+  open! Caml
+}
+
+let id_head = ['a'-'z' 'A'-'Z']
+let id_tail = ['a'-'z' 'A'-'Z' '0'-'9']*
+
+rule raw_token = parse
+  | '\t' { raise Error }
+  | ((' '* ("//" [^ '\n']*)? '\n')+ as x) (' '* as y) { new_line x y lexbuf }
+  | ' '+ { raw_token lexbuf }
+  | "->" { ARROW }
+  | '='  { ASGN }
+  | ':'  { COLON }
+  | ','  { COMMA }
+  | '('  { LP }
+  | ')'  { RP }
+  | '*'  { STAR }
+  | '<'  (([^ '<' '>' '\n' '\\'] | ('\\' _))* as x) '>' { CONSTANT (unquote x) }
+  | '"' ([^ '"' '\n']* as x) '"' { STRING x }
+  | "prefix" { PREFIX }
+  | "property" { PROPERTY }
+  | "message" { MESSAGE }
+  | id_head id_tail as id { ID id }
+  | eof { EOF }
+  | _ { raise Error }
+
+{
+  let token () =
+    let indents = ref [0] in
+    let scheduled_rc = ref 0 in
+    let last_indent () = match !indents with
+      | x :: _ -> x
+      | [] -> L.(die InternalError) "ToplLexer.indents should be nonempty"
+    in
+    let add_indent n = indents := n :: !indents in
+    let rec drop_to_indent n = match !indents with
+      | x :: xs when x > n -> (incr scheduled_rc; indents := xs; drop_to_indent n)
+      | x :: _  when x < n -> raise Error (* bad indentation *)
+      | _ -> ()
+    in
+    let rec step lexbuf =
+      if !scheduled_rc > 0 then (decr scheduled_rc; RC)
+      else match raw_token lexbuf with
+        | INDENT n when n > last_indent () -> (add_indent n; LC)
+        | INDENT n when n < last_indent () -> (drop_to_indent n; step lexbuf)
+        | INDENT _ -> step lexbuf
+        | t -> t
+    in
+    step
+}

infer/src/topl/ToplParser.mly

@@ -0,0 +1,76 @@
+/*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * 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 is_guard i = Char.is_lowercase i.[0]
+
+  let normalize_id i = String.uncapitalize i
+
+  let value_pattern_of_id i =
+    assert (String.length i > 0) ;
+    let j = normalize_id i in
+    if is_guard i then ToplAst.EqualToRegister j else ToplAst.SaveInRegister j
+%}
+
+%token <int> INDENT (* The lexer uses this token only internally. *)
+%token <string> CONSTANT
+%token <string> ID
+%token <string> STRING
+%token ARROW
+%token ASGN
+%token COLON
+%token COMMA
+%token EOF
+%token LC
+%token LP
+%token MESSAGE
+%token PREFIX
+%token PROPERTY
+%token RC
+%token RP
+%token STAR
+
+%start <ToplAst.t list> properties
+
+%%
+
+properties: ps=one_property* EOF { ps }
+
+one_property:
+    PROPERTY name=ID LC message=message? prefixes=prefix* transitions=transition* RC
+    { ToplAst.{name; message; prefixes; transitions} }
+
+message: MESSAGE s=STRING { s }
+
+prefix: PREFIX c=CONSTANT { c }
+
+transition:
+    source=ID ARROW target=ID COLON label=label
+    { ToplAst.{source; target; label} }
+
+label:
+    return=value_pattern ASGN c=call_pattern
+    { let procedure_name, arguments = c in ToplAst.{return; procedure_name; arguments} }
+  | c=call_pattern
+    { let procedure_name, arguments = c in ToplAst.{return=Ignore; procedure_name; arguments} }
+
+call_pattern: p=procedure_pattern a=arguments_pattern? { (p, a) }
+
+procedure_pattern:
+    i=ID { i }
+  | c=CONSTANT { c }
+  | STAR { ".*" }
+
+arguments_pattern: LP a=separated_list(COMMA, value_pattern) RP { a }
+
+value_pattern:
+    i=ID { value_pattern_of_id i }
+  | c=CONSTANT { ToplAst.EqualToConstant c }
+  | STAR { ToplAst.Ignore }
+
+%%

infer/tests/codetoanalyze/java/topl/Makefile

@@ -0,0 +1,13 @@
+# Copyright (c) 2019-present, Facebook, Inc.
+#
+# This source code is licensed under the MIT license found in the
+# LICENSE file in the root directory of this source tree.
+
+TESTS_DIR = ../../..
+
+INFER_OPTIONS = --topl-properties tomcat.topl --biabduction-only
+INFERPRINT_OPTIONS = --issues-tests
+
+SOURCES = $(wildcard *.java)
+
+include $(TESTS_DIR)/javac.make

infer/tests/codetoanalyze/java/topl/TomcatFail.java

@@ -0,0 +1,9 @@
+/*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+class TomcatFail {
+  void f() {}
+}

infer/tests/codetoanalyze/java/topl/tomcat.topl

@@ -0,0 +1,49 @@
+property ForwardUncommitted
+  message "A ServletResponse was forwarded before being committed."
+  // TODO assume InterleavedResponse_Weak
+  prefix <javax.servlet>
+  prefix <javax.servlet.{ServletOutputStream,ServletResponse}>
+  prefix <java.io.PrintWriter>
+  start -> start: *
+  start -> tracking: R = <ServletResponse.\<init\>>
+  tracking -> ok: flushBuffer(r)
+  tracking -> gotWriter: W = getWriter(r)
+  gotWriter -> ok: flush(w)
+  gotWrite -> ok: flushBuffer(r)
+  tracking -> gotStream: S = getOutputStream(r)
+  gotStream -> ok: flush(s)
+  gotStream -> ok: flushBuffer(r)
+  tracking -> error: <RequestDispatcher.forward>(*, *, r)
+  gotWriter -> error: <RequestDispatcher.forward>(*, *, r)
+  gotStream -> error: <RequestDispatcher.forward>(*, *, r)
+
+// The documentation of ServletResponse.getOutputStream says that "either this
+// method getWriter may be called to write to the body, not both." So,
+// technically, the property is InterleavedResponse1. However, this property is
+// broken, which is why we also have the weaker version InterleavedResponse2.
+property InterleavedResponse1
+  message "A ServletResponse was asked for both a writer and a stream."
+  prefix <javax.servlet.ServletResponse>
+  start -> start: *
+  start -> gotWriter: W = getWriter(R)
+  start -> gotStream: S = getOutputStream(R)
+  gotWriter -> error: getOutputStream(r)
+  gotStream -> error: getWriter(r)
+
+property InterleavedResponse2
+  // vertex names: w = got writer; W = used writer; similarly for s, S
+  message "Incompatible methods for putting data into a response were used."
+  prefix <javax.servlet.ServletResponse>
+  start -> start: *
+  start -> w: W = getWriter(R)
+  start -> s: S = getOutputStream(R)
+  w -> sw: S = getOutputStream(r)
+  s -> sw: W = getWriter(r)
+  w -> W: *(w)
+  sw -> sW: *(w)
+  s -> S: *(s)
+  sw -> Sw: *(s)
+  W -> sW: S = getOutputStream(r)
+  S -> Sw: W = getWriter(r)
+  sW -> error: *(s)
+  Sw -> error: *(w)