diff --git a/Makefile b/Makefile index c8205e325..2d51a50d9 100644 --- a/Makefile +++ b/Makefile @@ -141,6 +141,7 @@ DIRECT_TESTS += \ java_quandary \ java_racerd \ java_starvation \ + java_topl \ java_tracing \ ifneq ($(ANT),no) diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 98662364a..4b411f1a6 100644 --- a/infer/man/man1/infer-full.txt +++ b/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) diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 39fed9c3e..48611c084 100644 --- a/infer/src/base/Config.ml +++ b/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 diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 8e00e0610..f392a9328 100644 --- a/infer/src/base/Config.mli +++ b/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 diff --git a/infer/src/biabduction/interproc.ml b/infer/src/biabduction/interproc.ml index 7a3459a07..190cab3bb 100644 --- a/infer/src/biabduction/interproc.ml +++ b/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 ; diff --git a/infer/src/deadcode/Makefile b/infer/src/deadcode/Makefile index 9c8fa3fd3..3b1b396ce 100644 --- a/infer/src/deadcode/Makefile +++ b/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 diff --git a/infer/src/dune.in b/infer/src/dune.in index d51c077e2..b903281b9 100644 --- a/infer/src/dune.in +++ b/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) diff --git a/infer/src/topl/Topl.ml b/infer/src/topl/Topl.ml new file mode 100644 index 000000000..0de60fc86 --- /dev/null +++ b/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 ) diff --git a/infer/src/topl/Topl.mli b/infer/src/topl/Topl.mli new file mode 100644 index 000000000..324a04f88 --- /dev/null +++ b/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. *) diff --git a/infer/src/topl/ToplAst.ml b/infer/src/topl/ToplAst.ml new file mode 100644 index 000000000..fd9f5a18d --- /dev/null +++ b/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} diff --git a/infer/src/topl/ToplLexer.mll b/infer/src/topl/ToplLexer.mll new file mode 100644 index 000000000..75cc3283d --- /dev/null +++ b/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 +} diff --git a/infer/src/topl/ToplParser.mly b/infer/src/topl/ToplParser.mly new file mode 100644 index 000000000..2bd5913e8 --- /dev/null +++ b/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 INDENT (* The lexer uses this token only internally. *) +%token CONSTANT +%token ID +%token 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 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 } + +%% diff --git a/infer/tests/codetoanalyze/java/topl/Makefile b/infer/tests/codetoanalyze/java/topl/Makefile new file mode 100644 index 000000000..ca917b0ff --- /dev/null +++ b/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 diff --git a/infer/tests/codetoanalyze/java/topl/TomcatFail.java b/infer/tests/codetoanalyze/java/topl/TomcatFail.java new file mode 100644 index 000000000..8e004205e --- /dev/null +++ b/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() {} +} diff --git a/infer/tests/codetoanalyze/java/topl/issues.exp b/infer/tests/codetoanalyze/java/topl/issues.exp new file mode 100644 index 000000000..e69de29bb diff --git a/infer/tests/codetoanalyze/java/topl/tomcat.topl b/infer/tests/codetoanalyze/java/topl/tomcat.topl new file mode 100644 index 000000000..bc09a9a12 --- /dev/null +++ b/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 + prefix + prefix + start -> start: * + start -> tracking: R = > + 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: (*, *, r) + gotWriter -> error: (*, *, r) + gotStream -> error: (*, *, 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 + 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 + 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)