From 2ecfa422ac4ceb4574008b2cb1f46a26dfffb7d1 Mon Sep 17 00:00:00 2001 From: Radu Grigore Date: Mon, 5 Jul 2021 11:38:34 -0700 Subject: [PATCH] [topl] Update static matching for Erlang procedures. Summary: Topl matches procedure names against whatever Procname.hashable_name returns. For Java, it returns something like "java.util.ArrayList.add(...)", but for Erlang it used to return something like "add/1": no module and no parenthesis after. Now, Erlang returns "lists:add/1"; that is, it includes module name. Also, Topl doesn't insist anymore on having a paranthesis after the name. Differential Revision: D29520365 fbshipit-source-id: d23be1cc8 --- Makefile | 1 + infer/src/IR/Procname.ml | 2 + infer/src/topl/ToplAstOps.ml | 13 ++- infer/src/topl/ToplAutomaton.ml | 4 +- .../tests/codetoanalyze/erlang/topl/Makefile | 16 ++++ .../codetoanalyze/erlang/topl/issues.exp | 6 ++ .../codetoanalyze/erlang/topl/rebar.config | 11 +++ .../erlang/topl/src/topl_taint.app.src | 14 ++++ .../erlang/topl/src/topl_taint.erl | 84 +++++++++++++++++++ .../codetoanalyze/erlang/topl/taint.topl | 5 ++ 10 files changed, 152 insertions(+), 4 deletions(-) create mode 100644 infer/tests/codetoanalyze/erlang/topl/Makefile create mode 100644 infer/tests/codetoanalyze/erlang/topl/issues.exp create mode 100644 infer/tests/codetoanalyze/erlang/topl/rebar.config create mode 100644 infer/tests/codetoanalyze/erlang/topl/src/topl_taint.app.src create mode 100644 infer/tests/codetoanalyze/erlang/topl/src/topl_taint.erl create mode 100644 infer/tests/codetoanalyze/erlang/topl/taint.topl diff --git a/Makefile b/Makefile index afec2a72f..636bbfc17 100644 --- a/Makefile +++ b/Makefile @@ -152,6 +152,7 @@ ifeq ($(BUILD_ERLANG_ANALYZERS),yes) ifneq ($(REBAR3),no) DIRECT_TESTS += \ erlang_nonmatch \ + erlang_topl \ BUILD_SYSTEMS_TESTS += rebar3 endif diff --git a/infer/src/IR/Procname.ml b/infer/src/IR/Procname.ml index 7909bc5c2..80251ce20 100644 --- a/infer/src/IR/Procname.ml +++ b/infer/src/IR/Procname.ml @@ -897,6 +897,8 @@ let replace_csharp_inner_class_prefix_regex = replace_regex csharp_inner_class_p let hashable_name proc_name = match proc_name with + | Erlang pname -> + F.asprintf "%a" (Erlang.pp Verbose) pname | Java pname -> (* Strip autogenerated anonymous inner class numbers in order to keep the bug hash invariant when introducing new anonymous classes *) diff --git a/infer/src/topl/ToplAstOps.ml b/infer/src/topl/ToplAstOps.ml index 7d0f268ce..256b5bef5 100644 --- a/infer/src/topl/ToplAstOps.ml +++ b/infer/src/topl/ToplAstOps.ml @@ -7,12 +7,21 @@ open! IStd -let pp_raw_label f label = - match label.ToplAst.pattern with +let pp_variable_name f name = Format.fprintf f "%s" name + +let pp_pattern f (pattern : ToplAst.label_pattern) = + match pattern with | ArrayWritePattern -> Format.fprintf f "#ArrayWrite" | ProcedureNamePattern procedure_name -> Format.fprintf f "%s" procedure_name +let pp_raw_label f {ToplAst.pattern; arguments; condition= _; action= _} = + (* TODO: Print condition and action. *) + Format.fprintf f "%a %a when CONDITION => ACTION" pp_pattern pattern + (Pp.option (Pp.comma_seq pp_variable_name)) + arguments + + let pp_label = Pp.option pp_raw_label diff --git a/infer/src/topl/ToplAutomaton.ml b/infer/src/topl/ToplAutomaton.ml index 5f1493f7b..9137d7924 100644 --- a/infer/src/topl/ToplAutomaton.ml +++ b/infer/src/topl/ToplAutomaton.ml @@ -81,8 +81,8 @@ let make properties = let prefix_pname pname = if String.equal ".*" pname then pname else - let ps = List.map ~f:(fun p -> "\\|" ^ p ^ "\\.") p.ToplAst.prefixes in - "^\\(" ^ String.concat ps ^ "\\)" ^ pname ^ "(" + let ps = List.map ~f:(fun p -> "\\|" ^ p ^ ".") p.ToplAst.prefixes in + "^\\(" ^ String.concat ps ^ "\\)" ^ pname ^ "\\((\\|$\\)" in let prefix_pattern = ToplAst.( diff --git a/infer/tests/codetoanalyze/erlang/topl/Makefile b/infer/tests/codetoanalyze/erlang/topl/Makefile new file mode 100644 index 000000000..f0bac8851 --- /dev/null +++ b/infer/tests/codetoanalyze/erlang/topl/Makefile @@ -0,0 +1,16 @@ +# 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. + +TESTS_DIR = ../../.. + +# see explanations in cpp/biabduction/Makefile for the custom isystem +INFER_OPTIONS = --topl --topl-properties taint.topl --project-root $(TESTS_DIR) +INFERPRINT_OPTIONS = --issues-tests + +SOURCES = $(wildcard src/*.erl) + +include $(TESTS_DIR)/erlang.make + +infer-out/report.json: $(MAKEFILE_LIST) diff --git a/infer/tests/codetoanalyze/erlang/topl/issues.exp b/infer/tests/codetoanalyze/erlang/topl/issues.exp new file mode 100644 index 000000000..06ea55d26 --- /dev/null +++ b/infer/tests/codetoanalyze/erlang/topl/issues.exp @@ -0,0 +1,6 @@ +codetoanalyze/erlang/topl/src/topl_taint.erl, fp_test_f_Bad/0, 1, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [no pattern match here] +codetoanalyze/erlang/topl/src/topl_taint.erl, fp_test_g_Ok/0, 1, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [no pattern match here] +codetoanalyze/erlang/topl/src/topl_taint.erl, test_a_Bad/0, 0, TOPL_ERROR, no_bucket, ERROR, [call to source/0,call to sink/1] +codetoanalyze/erlang/topl/src/topl_taint.erl, test_d_Bad/0, 0, TOPL_ERROR, no_bucket, ERROR, [call to source/0,call to call_sink_indirectly/1,call to call_sink/1,call to sink/1] +codetoanalyze/erlang/topl/src/topl_taint.erl, test_h_Bad/0, 0, TOPL_ERROR, no_bucket, ERROR, [call to dirty_if_argument_nil/1,call to source/0,call to sink/1] +codetoanalyze/erlang/topl/src/topl_taint.erl, test_j_Bad/0, 1, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [no pattern match here] diff --git a/infer/tests/codetoanalyze/erlang/topl/rebar.config b/infer/tests/codetoanalyze/erlang/topl/rebar.config new file mode 100644 index 000000000..48d9fc065 --- /dev/null +++ b/infer/tests/codetoanalyze/erlang/topl/rebar.config @@ -0,0 +1,11 @@ +% 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. + +{erl_opts, []}. +{deps, []}. + +{shell, [ + {apps, [topl_taint]} +]}. diff --git a/infer/tests/codetoanalyze/erlang/topl/src/topl_taint.app.src b/infer/tests/codetoanalyze/erlang/topl/src/topl_taint.app.src new file mode 100644 index 000000000..971f3623f --- /dev/null +++ b/infer/tests/codetoanalyze/erlang/topl/src/topl_taint.app.src @@ -0,0 +1,14 @@ +% 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. +{application, topl_taint, [ + {description, "An Erlang app that leaks"}, + {vsn, "0.1.0"}, + {registered, []}, + {applications, [ + kernel, + stdlib + ]}, + {modules, []} +]}. diff --git a/infer/tests/codetoanalyze/erlang/topl/src/topl_taint.erl b/infer/tests/codetoanalyze/erlang/topl/src/topl_taint.erl new file mode 100644 index 000000000..1b3209b68 --- /dev/null +++ b/infer/tests/codetoanalyze/erlang/topl/src/topl_taint.erl @@ -0,0 +1,84 @@ +% 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. + +-module(topl_taint). + +-export([ + test_a_Bad/0, + test_b_Ok/0, + fn_test_c_Bad/0, + test_d_Bad/0, + test_e_Ok/0, + fp_test_f_Bad/0, + fp_test_g_Ok/0, + test_h_Bad/0, + test_i_Ok/0, + test_j_Bad/0 +]). + +test_a_Bad() -> + sink(source()). + +test_b_Ok() -> + sink(1). + +% FN because match not yet translated +fn_test_c_Bad() -> + X = source(), + sink(X). + +test_d_Bad() -> + call_sink_indirectly(tito(source())). + +test_e_Ok() -> + call_sink_indirectly(tito(ok)). + +% FP: T94670024 (bad, but wrong warning reported) +fp_test_f_Bad() -> + case one() + one() - two() =:= 0 of + true -> sink(dirty_if_argument_nil([])); + false -> sink(dirty_if_argument_nil([1])) + end. + +% FP: T94670024 +fp_test_g_Ok() -> + case one() + one() - two() =/= 0 of + true -> sink(dirty_if_argument_nil([])); + false -> sink(dirty_if_argument_nil([1])) + end. + +test_h_Bad() -> + case one() + one() of + 1 -> sink(dirty_if_argument_nil([ok])); + 2 -> sink(dirty_if_argument_nil([])) + end. + +test_i_Ok() -> + case two() of + 1 -> sink(dirty_if_argument_nil(bad)); + 2 -> sink(dirty_if_argument_nil([ok, ok, ok])) + end. + +% Bad because no case for 3 (not a topl property) +test_j_Bad() -> + case two() + two() - one() of + 1 -> sink(dirty_if_argument_nil(bad)); + 2 -> sink(dirty_if_argument_nil([ok, ok, ok])) + end. + +%% + +% tito = Taint-In Taint-Out +tito(X) -> X. +call_sink_indirectly(X) -> call_sink(X). +call_sink(X) -> sink(X). +dirty_if_argument_nil([]) -> source(); +dirty_if_argument_nil([X | _]) -> X. +one() -> 1. +two() -> 2. + +%% +source() -> dirty. +sink(_) -> ok. diff --git a/infer/tests/codetoanalyze/erlang/topl/taint.topl b/infer/tests/codetoanalyze/erlang/topl/taint.topl new file mode 100644 index 000000000..07a420a5d --- /dev/null +++ b/infer/tests/codetoanalyze/erlang/topl/taint.topl @@ -0,0 +1,5 @@ +property Taint + prefix "topl_taint" + start -> start: * + start -> tracking: "source/0"(Ret) => x := Ret + tracking -> error: "sink/1"(Arg, VoidRet) when x == Arg