From 3e9d1bff160cf7c485f1bb730e04d0d6b87c2dc1 Mon Sep 17 00:00:00 2001 From: Radu Grigore Date: Wed, 18 Dec 2019 07:10:20 -0800 Subject: [PATCH] [topl] Bugfix in matching constructor names. Summary: The regexp was wrong. Reviewed By: ngorogiannis Differential Revision: D19035490 fbshipit-source-id: c91097f45 --- infer/src/topl/ToplAutomaton.ml | 4 ++- .../codetoanalyze/java/topl/ScannerFail.java | 25 +++++++++++++++++++ .../codetoanalyze/java/topl/hasnext.topl | 3 +++ .../tests/codetoanalyze/java/topl/issues.exp | 1 + 4 files changed, 32 insertions(+), 1 deletion(-) create mode 100644 infer/tests/codetoanalyze/java/topl/ScannerFail.java diff --git a/infer/src/topl/ToplAutomaton.ml b/infer/src/topl/ToplAutomaton.ml index e28adeb78..536c60553 100644 --- a/infer/src/topl/ToplAutomaton.ml +++ b/infer/src/topl/ToplAutomaton.ml @@ -62,7 +62,9 @@ let make properties = let f p = let prefix_pname pname = if String.equal ".*" pname then pname - else "^\\(\\|" ^ String.concat ~sep:"\\|" p.ToplAst.prefixes ^ "\\)\\." ^ pname ^ "(" + else + let ps = List.map ~f:(fun p -> "\\|" ^ p ^ "\\.") p.ToplAst.prefixes in + "^\\(" ^ String.concat ps ^ "\\)" ^ pname ^ "(" in let f t = let source = vindex ToplAst.(p.name, t.source) in diff --git a/infer/tests/codetoanalyze/java/topl/ScannerFail.java b/infer/tests/codetoanalyze/java/topl/ScannerFail.java new file mode 100644 index 000000000..d3ed60f97 --- /dev/null +++ b/infer/tests/codetoanalyze/java/topl/ScannerFail.java @@ -0,0 +1,25 @@ +/* + * 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. + */ +import java.util.Scanner; + +abstract class ScannerFail { + void readOk() { + Scanner scan = getScanner(); + while (scan.hasNext()) { + scan.next(); + } + } + + void readBad() { + Scanner scan = getScanner(); + scan.next(); + } + + Scanner getScanner() { + return new Scanner(System.in); + } +} diff --git a/infer/tests/codetoanalyze/java/topl/hasnext.topl b/infer/tests/codetoanalyze/java/topl/hasnext.topl index 8ca797e06..8a08339c5 100644 --- a/infer/tests/codetoanalyze/java/topl/hasnext.topl +++ b/infer/tests/codetoanalyze/java/topl/hasnext.topl @@ -1,8 +1,11 @@ property HasNext prefix "Iterator" prefix "List" + prefix "Scanner" start -> start: * start -> invalid: I = iterator(*) + start -> invalid: Scanner(I, *) // For constructors, biabduction has "this" as first argument invalid -> valid: B = hasNext(i) if B != 0 // in SIL, "true" is encoded as "not 0" valid -> invalid: next(i) invalid -> error: next(i) + diff --git a/infer/tests/codetoanalyze/java/topl/issues.exp b/infer/tests/codetoanalyze/java/topl/issues.exp index 97bf97ec0..984715fd6 100644 --- a/infer/tests/codetoanalyze/java/topl/issues.exp +++ b/infer/tests/codetoanalyze/java/topl/issues.exp @@ -5,3 +5,4 @@ codetoanalyze/java/topl/Iterators.java, Iterators.hasNextInterproceduralBad(java codetoanalyze/java/topl/Iterators.java, Iterators.hasNextInterproceduralBad(java.util.List):void, 1, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextInterproceduralBad(...),Skipping iterator(): unknown method,start of procedure saveArgs(...),return from a call to void Property.saveArgs(Object,List),start of procedure execute(),start of procedure execute_state_0(),Taking false branch,return from a call to void Property.execute_state_0(),start of procedure execute_state_1(),Taking true branch,start of procedure maybe(),return from a call to void Property.maybe(),Taking false branch,start of procedure maybe(),return from a call to void Property.maybe(),Taking false branch,Taking false branch,Taking false branch,return from a call to void Property.execute_state_1(),start of procedure execute_state_2(),Taking false branch,return from a call to void Property.execute_state_2(),start of procedure execute_state_3(),Taking false branch,return from a call to void Property.execute_state_3(),start of procedure execute_state_4(),Taking false branch,return from a call to void Property.execute_state_4(),start of procedure execute_state_5(),Taking false branch,return from a call to void Property.execute_state_5(),start of procedure execute_state_6(),Taking false branch,return from a call to void Property.execute_state_6(),start of procedure execute_state_7(),Taking false branch,return from a call to void Property.execute_state_7(),return from a call to void Property.execute(),start of procedure getSingleElementOk(...),Skipping next(): unknown method] codetoanalyze/java/topl/Iterators.java, Iterators.hasNextInterproceduralOk(java.util.List):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextInterproceduralOk(...),Skipping iterator(): unknown method,start of procedure saveArgs(...),return from a call to void Property.saveArgs(Object,List),start of procedure execute(),start of procedure execute_state_0(),Taking false branch,return from a call to void Property.execute_state_0(),start of procedure execute_state_1(),Taking true branch,start of procedure maybe(),return from a call to void Property.maybe(),Taking false branch,start of procedure maybe(),return from a call to void Property.maybe(),Taking false branch,Taking false branch,Taking false branch,return from a call to void Property.execute_state_1(),start of procedure execute_state_2(),Taking false branch,return from a call to void Property.execute_state_2(),start of procedure execute_state_3(),Taking false branch,return from a call to void Property.execute_state_3(),start of procedure execute_state_4(),Taking false branch,return from a call to void Property.execute_state_4(),start of procedure execute_state_5(),Taking false branch,return from a call to void Property.execute_state_5(),start of procedure execute_state_6(),Taking false branch,return from a call to void Property.execute_state_6(),start of procedure execute_state_7(),Taking false branch,return from a call to void Property.execute_state_7(),return from a call to void Property.execute()] codetoanalyze/java/topl/Iterators.java, Iterators.hasNextOk(java.util.List):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextOk(...),Skipping iterator(): unknown method,start of procedure saveArgs(...),return from a call to void Property.saveArgs(Object,List),start of procedure execute(),start of procedure execute_state_0(),Taking false branch,return from a call to void Property.execute_state_0(),start of procedure execute_state_1(),Taking true branch,start of procedure maybe(),return from a call to void Property.maybe(),Taking false branch,start of procedure maybe(),return from a call to void Property.maybe(),Taking false branch,Taking false branch,Taking false branch,return from a call to void Property.execute_state_1(),start of procedure execute_state_2(),Taking false branch,return from a call to void Property.execute_state_2(),start of procedure execute_state_3(),Taking false branch,return from a call to void Property.execute_state_3(),start of procedure execute_state_4(),Taking false branch,return from a call to void Property.execute_state_4(),start of procedure execute_state_5(),Taking false branch,return from a call to void Property.execute_state_5(),start of procedure execute_state_6(),Taking false branch,return from a call to void Property.execute_state_6(),start of procedure execute_state_7(),Taking false branch,return from a call to void Property.execute_state_7(),return from a call to void Property.execute()] +codetoanalyze/java/topl/ScannerFail.java, ScannerFail.readBad():void, 0, TOPL_ERROR, no_bucket, ERROR, []