diff --git a/.gitignore b/.gitignore index 6d7072a53..d073e2a0d 100644 --- a/.gitignore +++ b/.gitignore @@ -57,6 +57,7 @@ duplicates.txt /infer/tests/build_systems/java_test_determinator/*.test /infer/tests/build_systems/java_source_parser/*.test /infer/tests/codetoanalyze/dotnet/*/*.json +/infer/tests/codetoanalyze/erlang/**/_build /_release /infer-source diff --git a/Makefile b/Makefile index f0522fd97..afec2a72f 100644 --- a/Makefile +++ b/Makefile @@ -148,6 +148,15 @@ endif endif # HAS_OBJC endif # BUILD_C_ANALYZERS +ifeq ($(BUILD_ERLANG_ANALYZERS),yes) +ifneq ($(REBAR3),no) +DIRECT_TESTS += \ + erlang_nonmatch \ + +BUILD_SYSTEMS_TESTS += rebar3 +endif +endif # BUILD_ERLANG_ANALYZERS + ifeq ($(BUILD_JAVA_ANALYZERS),yes) BUILD_SYSTEMS_TESTS += \ differential_interesting_paths_filter \ @@ -212,19 +221,13 @@ endif ifneq ($(ANT),no) BUILD_SYSTEMS_TESTS += ant endif - - - ifneq ($(BUCK),no) BUILD_SYSTEMS_TESTS += buck_java_flavor endif ifneq ($(MVN),no) BUILD_SYSTEMS_TESTS += mvn endif -ifneq ($(REBAR3),no) -BUILD_SYSTEMS_TESTS += rebar3 -endif -endif +endif # BUILD_JAVA_ANALYZERS DIRECT_TESTS += \ dotnet_arithmetic \ diff --git a/configure.ac b/configure.ac index a03dff6ee..7cd45acb2 100644 --- a/configure.ac +++ b/configure.ac @@ -276,6 +276,12 @@ AS_IF([test "$OPAM" != "no"], [ AC_SUBST([OPAMROOT]) AC_SUBST([OPAMSWITCH]) +if test "x$enable_erlang_analyzers" = "xyes"; then + AC_CHECK_TOOL([ESCRIPT], [escript], [no]) + AC_CHECK_TOOL([REBAR3], [rebar3], [no]) +fi +# end if($enable_erlang_analyzers) + if test "x$enable_java_analyzers" = "xyes"; then AC_CHECK_TOOL([JAVA], [java], [no]) AC_CHECK_TOOL([JAVAC], [javac], [no]) @@ -386,7 +392,6 @@ if test x"$NDKBUILD" = x"no"; then fi AC_CHECK_TOOL([NINJA], [ninja], [no]) -AC_CHECK_TOOL([REBAR3], [rebar3], [no]) AC_CHECK_TOOL([XCPRETTY], [xcpretty], [no]) AC_CHECK_TOOL([SED], [sed], [no]) diff --git a/infer/documentation/issues/NONEXHAUSTIVE_PATTERN_MATCH.md b/infer/documentation/issues/NONEXHAUSTIVE_PATTERN_MATCH.md new file mode 100644 index 000000000..4dfad9f8e --- /dev/null +++ b/infer/documentation/issues/NONEXHAUSTIVE_PATTERN_MATCH.md @@ -0,0 +1,10 @@ +## Nonexhaustive pattern match in Erlang + +Reports an error when a function clause is missing. + +For example, if we call `tail([])` and the full definition of `tail` is +```erlang +tail([_|Xs]) -> Xs. +``` + +The error is also reported if the failing pattern match is in a `case` expression. diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 5775801a5..70e78eca0 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -544,6 +544,7 @@ OPTIONS NIL_BLOCK_CALL (enabled by default), NIL_INSERTION_INTO_COLLECTION (enabled by default), NIL_MESSAGING_TO_NON_POD (enabled by default), + NONEXHAUSTIVE_PATTERN_MATCH (enabled by default), NULLPTR_DEREFERENCE (enabled by default), NULL_DEREFERENCE (enabled by default), OPTIONAL_EMPTY_ACCESS (enabled by default), diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt index 2afbfb9e6..aaa77feee 100644 --- a/infer/man/man1/infer-report.txt +++ b/infer/man/man1/infer-report.txt @@ -221,6 +221,7 @@ OPTIONS NIL_BLOCK_CALL (enabled by default), NIL_INSERTION_INTO_COLLECTION (enabled by default), NIL_MESSAGING_TO_NON_POD (enabled by default), + NONEXHAUSTIVE_PATTERN_MATCH (enabled by default), NULLPTR_DEREFERENCE (enabled by default), NULL_DEREFERENCE (enabled by default), OPTIONAL_EMPTY_ACCESS (enabled by default), diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 3aa10dc91..d9e446c67 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -544,6 +544,7 @@ OPTIONS NIL_BLOCK_CALL (enabled by default), NIL_INSERTION_INTO_COLLECTION (enabled by default), NIL_MESSAGING_TO_NON_POD (enabled by default), + NONEXHAUSTIVE_PATTERN_MATCH (enabled by default), NULLPTR_DEREFERENCE (enabled by default), NULL_DEREFERENCE (enabled by default), OPTIONAL_EMPTY_ACCESS (enabled by default), diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index ebf8ecf62..a015cd63c 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -804,6 +804,11 @@ let nil_messaging_to_non_pod = ~user_documentation:[%blob "../../documentation/issues/NIL_MESSAGING_TO_NON_POD.md"] +let nonexhaustive_pattern_match = + register ~id:"NONEXHAUSTIVE_PATTERN_MATCH" Error Pulse + ~user_documentation:[%blob "../../documentation/issues/NONEXHAUSTIVE_PATTERN_MATCH.md"] + + let null_dereference = register ~id:"NULL_DEREFERENCE" Error Biabduction ~user_documentation:"See [NULLPTR_DEREFERENCE](#nullptr_dereference)." diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index d4db52979..cbd92d179 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -282,6 +282,8 @@ val nil_insertion_into_collection : t val nil_messaging_to_non_pod : t +val nonexhaustive_pattern_match : t + val null_dereference : t val nullptr_dereference : t diff --git a/infer/src/erlang/ErlangTranslator.ml b/infer/src/erlang/ErlangTranslator.ml index a63fef0d3..9699b07ca 100644 --- a/infer/src/erlang/ErlangTranslator.ml +++ b/infer/src/erlang/ErlangTranslator.ml @@ -11,9 +11,9 @@ module L = Logging let mangled_arg (n : int) : Mangled.t = Mangled.from_string (Printf.sprintf "$arg%d" n) -let typ_of_name (name : ErlangTypeName.t) : Typ.t = - Typ.mk (Tptr (Typ.mk (Tstruct (ErlangType name)), Pk_pointer)) +let typ_of_name (name : ErlangTypeName.t) : Typ.t = Typ.mk (Tstruct (ErlangType name)) +let ptr_typ_of_name (name : ErlangTypeName.t) : Typ.t = Typ.mk (Tptr (typ_of_name name, Pk_pointer)) module UnqualifiedFunction = struct module T = struct @@ -33,23 +33,27 @@ end type module_name = string [@@deriving sexp_of] -type environment = +type absent = Absent + +type 'a present = Present of 'a + +type ('procdesc, 'result) environment = { current_module: module_name (** used to qualify function names *) ; exports: UnqualifiedFunction.Set.t (** used to determine public/private access *) ; imports: module_name UnqualifiedFunction.Map.t (** used to resolve function names *) ; location: Location.t (** used to tag nodes and instructions being created *) - ; procdesc: (Procdesc.t option[@sexp.opaque]) (** imperative, being built *) - ; result: (Exp.t option[@sexp.opaque]) (** where to store the result value (if any) *) } + ; procdesc: ('procdesc[@sexp.opaque]) + ; result: ('result[@sexp.opaque]) } [@@deriving sexp_of] -let get_environment module_ : environment = +let get_environment module_ = let init = { current_module= Printf.sprintf "%s:unknown_module" __FILE__ ; exports= UnqualifiedFunction.Set.empty ; imports= UnqualifiedFunction.Map.empty (* TODO: auto-import from module "erlang" *) ; location= Location.dummy - ; procdesc= None - ; result= None } + ; procdesc= Absent + ; result= Absent } in let f env (form : Ast.form) = match form.simple_form with @@ -89,8 +93,8 @@ let update_location line env = (** Groups several helpers used to create nodes. *) module Node = struct - let make env kind instructions = - let procdesc = Option.value_exn env.procdesc in + let make (env : (Procdesc.t present, _) environment) kind instructions = + let (Present procdesc) = env.procdesc in Procdesc.create_node procdesc env.location kind instructions @@ -198,7 +202,7 @@ module Block = struct let make_load env id e typ = - let procdesc = Option.value_exn env.procdesc in + let (Present procdesc) = env.procdesc in let procname = Procdesc.get_proc_name procdesc in let temp_pvar = Pvar.mk_tmp "LoadBlock" procname in let instructions = @@ -210,7 +214,7 @@ end let has_type env ~result ~value (name : ErlangTypeName.t) : Sil.instr = let fun_exp : Exp.t = Const (Cfun BuiltinDecl.__instanceof) in - let any = typ_of_name Any in + let any = ptr_typ_of_name Any in let args : (Exp.t * Typ.t) list = [ (Var value, any) ; ( Sizeof @@ -227,8 +231,8 @@ let has_type env ~result ~value (name : ErlangTypeName.t) : Sil.instr = are storing the corresponding values; otherwise, the [exit_failure] node is reached. *) let rec translate_pattern env (value : Ident.t) {Ast.line; simple_expression} : Block.t = let env = update_location line env in - let any = typ_of_name Any in - let procdesc = Option.value_exn env.procdesc in + let any = ptr_typ_of_name Any in + let (Present procdesc) = env.procdesc in let procname = Procdesc.get_proc_name procdesc in match simple_expression with | Cons {head; tail} -> @@ -296,19 +300,20 @@ let rec translate_pattern env (value : Ident.t) {Ast.line; simple_expression} : let rec translate_expression env {Ast.line; simple_expression} = let env = update_location line env in - let any = typ_of_name Any in - let procdesc = Option.value_exn env.procdesc in + let any = ptr_typ_of_name Any in + let (Present result) = env.result in + let (Present procdesc) = env.procdesc in let procname = Procdesc.get_proc_name procdesc in let ret_var = - match env.result with Some (Var ret_var) -> ret_var | _ -> Ident.create_fresh Ident.knormal + match result with Exp.Var ret_var -> ret_var | _ -> Ident.create_fresh Ident.knormal in let expression_block : Block.t = match simple_expression with | BinaryOperator (e1, op, e2) -> let id1 = Ident.create_fresh Ident.knormal in let id2 = Ident.create_fresh Ident.knormal in - let block1 = translate_expression {env with result= Some (Var id1)} e1 in - let block2 = translate_expression {env with result= Some (Var id2)} e2 in + let block1 = translate_expression {env with result= Present (Exp.Var id1)} e1 in + let block2 = translate_expression {env with result= Present (Exp.Var id2)} e2 in let make_simple_op_block sil_op = Block.make_load env ret_var (Exp.BinOp (sil_op, Var id1, Var id2)) any in @@ -369,7 +374,7 @@ let rec translate_expression env {Ast.line; simple_expression} = let args_with_ids = List.map ~f:(fun a -> (a, Ident.create_fresh Ident.knormal)) args in let args_blocks = let f (one_arg_expression, one_arg_ret_var) = - let result = Some (Exp.Var one_arg_ret_var) in + let result = Present (Exp.Var one_arg_ret_var) in translate_expression {env with result} one_arg_expression in List.map ~f args_with_ids @@ -385,7 +390,7 @@ let rec translate_expression env {Ast.line; simple_expression} = Block.all env (args_blocks @ [call_block]) | Case {expression; cases} -> let id = Ident.create_fresh Ident.knormal in - let expr_block = translate_expression {env with result= Some (Var id)} expression in + let expr_block = translate_expression {env with result= Present (Exp.Var id)} expression in let blocks = Block.any env (List.map ~f:(translate_case_clause env [id]) cases) in let crash_node = Node.make_pattern_fail env in let {Block.start; exit_success; exit_failure} = Block.all env [expr_block; blocks] in @@ -395,8 +400,8 @@ let rec translate_expression env {Ast.line; simple_expression} = | Cons {head; tail} -> let head_var = Ident.create_fresh Ident.knormal in let tail_var = Ident.create_fresh Ident.knormal in - let head_block = translate_expression {env with result= Some (Var head_var)} head in - let tail_block = translate_expression {env with result= Some (Var tail_var)} tail in + let head_block = translate_expression {env with result= Present (Exp.Var head_var)} head in + let tail_block = translate_expression {env with result= Present (Exp.Var tail_var)} tail in let fun_exp = Exp.Const (Cfun BuiltinDecl.__erlang_make_cons) in let args : (Exp.t * Typ.t) list = [(Var head_var, any); (Var tail_var, any)] in let call_instruction = @@ -431,10 +436,10 @@ let rec translate_expression env {Ast.line; simple_expression} = Block.make_success env in (* Add extra nodes/instructions to store return value if needed *) - match env.result with - | None | Some (Var _) -> + match result with + | Exp.Var _ -> expression_block - | Some result -> + | _ -> let store_instr = Sil.Store {e1= result; root_typ= any; typ= any; e2= Var ret_var; loc= env.location} in @@ -445,7 +450,8 @@ let rec translate_expression env {Ast.line; simple_expression} = and translate_body env body : Block.t = let blocks = let f rev_blocks one_expression = - let env = {env with result= None} in + let id = Ident.create_fresh Ident.knormal in + let env = {env with result= Present (Exp.Var id)} in translate_expression env one_expression :: rev_blocks in let f_last rev_blocks one_expression = translate_expression env one_expression :: rev_blocks in @@ -467,7 +473,7 @@ and translate_case_clause env (values : Ident.t list) {Ast.line= _; patterns; gu (* TODO: Evaluate the guards. *) matchers_block.exit_success |~~> [body_block.start] ; let () = - let procdesc = Option.value_exn env.procdesc in + let (Present procdesc) = env.procdesc in body_block.exit_failure |~~> [Procdesc.get_exit_node procdesc] in { start= matchers_block.start @@ -482,7 +488,7 @@ let translate_one_function env cfg function_ clauses = let module_name = env.current_module in Procname.make_erlang ~module_name ~function_name ~arity in - let any = typ_of_name Any in + let any = ptr_typ_of_name Any in let attributes = let default = ProcAttributes.default env.location.file name in let access : ProcAttributes.access = if Set.mem env.exports uf_name then Public else Private in @@ -497,7 +503,9 @@ let translate_one_function env cfg function_ clauses = Procdesc.set_exit_node procdesc exit_node ; procdesc in - let env = {env with procdesc= Some procdesc; result= Some (Exp.Lvar (Pvar.get_ret_pvar name))} in + let env = + {env with procdesc= Present procdesc; result= Present (Exp.Lvar (Pvar.get_ret_pvar name))} + in let idents, loads = let load (formal, typ) = let id = Ident.create_fresh Ident.knormal in diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml index b603f1e3d..5abc4869f 100644 --- a/infer/src/pulse/PulseDiagnostic.ml +++ b/infer/src/pulse/PulseDiagnostic.ml @@ -12,24 +12,32 @@ module Invalidation = PulseInvalidation module Trace = PulseTrace module ValueHistory = PulseValueHistory +type calling_context = (CallEvent.t * Location.t) list [@@deriving compare, equal] + type access_to_invalid_address = - { calling_context: (CallEvent.t * Location.t) list + { calling_context: calling_context ; invalidation: Invalidation.t ; invalidation_trace: Trace.t ; access_trace: Trace.t ; must_be_valid_reason: Invalidation.must_be_valid_reason option } [@@deriving compare, equal] -type read_uninitialized_value = {calling_context: (CallEvent.t * Location.t) list; trace: Trace.t} +type nonexhaustive_pattern_match = {calling_context: calling_context; location: Location.t} +[@@deriving compare, equal] + +type read_uninitialized_value = {calling_context: calling_context; trace: Trace.t} [@@deriving compare, equal] let yojson_of_access_to_invalid_address = [%yojson_of: _] +let yojson_of_nonexhaustive_pattern_match = [%yojson_of: _] + let yojson_of_read_uninitialized_value = [%yojson_of: _] type t = | AccessToInvalidAddress of access_to_invalid_address | MemoryLeak of {procname: Procname.t; allocation_trace: Trace.t; location: Location.t} + | NonexhaustivePatternMatch of nonexhaustive_pattern_match | ReadUninitializedValue of read_uninitialized_value | StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t} [@@deriving equal] @@ -41,7 +49,9 @@ let get_location = function | AccessToInvalidAddress {calling_context= (_, location) :: _} | ReadUninitializedValue {calling_context= (_, location) :: _} -> (* report at the call site that triggers the bug *) location - | MemoryLeak {location} | StackVariableAddressEscape {location} -> + | MemoryLeak {location} + | NonexhaustivePatternMatch {location} + | StackVariableAddressEscape {location} -> location @@ -164,6 +174,8 @@ let get_message diagnostic = "%s memory leak. Memory dynamically allocated at line %d %a is not freed after the last \ access at %a" pulse_start_msg allocation_line pp_allocation_trace allocation_trace Location.pp location + | NonexhaustivePatternMatch {calling_context= _; location} -> + F.asprintf "%s nonexhaustive pattern match at %a" pulse_start_msg Location.pp location | ReadUninitializedValue {calling_context; trace} -> let root_var = PulseTrace.find_map trace ~f:(function VariableDeclared (pvar, _) -> Some pvar | _ -> None) @@ -297,6 +309,9 @@ let get_trace = function ~pp_immediate:(fun fmt -> F.fprintf fmt "allocated by `%a` here" Procname.pp procname) allocation_trace @@ [Errlog.make_trace_element 0 location "memory becomes unreachable here" []] + | NonexhaustivePatternMatch {calling_context; location} -> + get_trace_calling_context calling_context + @@ [Errlog.make_trace_element 0 location "no pattern match here" []] | ReadUninitializedValue {calling_context; trace} -> get_trace_calling_context calling_context @@ Trace.add_to_errlog ~nesting:0 @@ -318,6 +333,8 @@ let get_issue_type = function Invalidation.issue_type_of_cause invalidation must_be_valid_reason | MemoryLeak _ -> IssueType.pulse_memory_leak + | NonexhaustivePatternMatch _ -> + IssueType.nonexhaustive_pattern_match | ReadUninitializedValue _ -> IssueType.uninitialized_value_pulse | StackVariableAddressEscape _ -> diff --git a/infer/src/pulse/PulseDiagnostic.mli b/infer/src/pulse/PulseDiagnostic.mli index f624b575e..717ee1559 100644 --- a/infer/src/pulse/PulseDiagnostic.mli +++ b/infer/src/pulse/PulseDiagnostic.mli @@ -11,8 +11,10 @@ module Invalidation = PulseInvalidation module Trace = PulseTrace module ValueHistory = PulseValueHistory +type calling_context = (CallEvent.t * Location.t) list [@@deriving compare, equal] + type access_to_invalid_address = - { calling_context: (CallEvent.t * Location.t) list + { calling_context: calling_context (** the list of function calls leading to the issue being realised, in outermost-to-innermost order, which is an additional common prefix to the traces in the record *) @@ -26,8 +28,11 @@ type access_to_invalid_address = ; must_be_valid_reason: Invalidation.must_be_valid_reason option } [@@deriving compare, equal, yojson_of] +type nonexhaustive_pattern_match = {calling_context: calling_context; location: Location.t} +[@@deriving compare, equal, yojson_of] + type read_uninitialized_value = - { calling_context: (CallEvent.t * Location.t) list + { calling_context: calling_context (** the list of function calls leading to the issue being realised, which is an additional common prefix to the traces in the record *) ; trace: Trace.t @@ -39,6 +44,7 @@ type read_uninitialized_value = type t = | AccessToInvalidAddress of access_to_invalid_address | MemoryLeak of {procname: Procname.t; allocation_trace: Trace.t; location: Location.t} + | NonexhaustivePatternMatch of nonexhaustive_pattern_match | ReadUninitializedValue of read_uninitialized_value | StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t} [@@deriving equal] diff --git a/infer/src/pulse/PulseLatentIssue.ml b/infer/src/pulse/PulseLatentIssue.ml index c0926f625..8749ae50a 100644 --- a/infer/src/pulse/PulseLatentIssue.ml +++ b/infer/src/pulse/PulseLatentIssue.ml @@ -12,12 +12,15 @@ module Arithmetic = PulseArithmetic type t = | AccessToInvalidAddress of Diagnostic.access_to_invalid_address + | NonexhaustivePatternMatch of Diagnostic.nonexhaustive_pattern_match | ReadUninitializedValue of Diagnostic.read_uninitialized_value [@@deriving compare, equal, yojson_of] let to_diagnostic = function | AccessToInvalidAddress access_to_invalid_address -> Diagnostic.AccessToInvalidAddress access_to_invalid_address + | NonexhaustivePatternMatch nonexhaustive_pattern_match -> + Diagnostic.NonexhaustivePatternMatch nonexhaustive_pattern_match | ReadUninitializedValue read_uninitialized_value -> Diagnostic.ReadUninitializedValue read_uninitialized_value @@ -25,6 +28,9 @@ let to_diagnostic = function let add_call call_and_loc = function | AccessToInvalidAddress access -> AccessToInvalidAddress {access with calling_context= call_and_loc :: access.calling_context} + | NonexhaustivePatternMatch nonmatch -> + NonexhaustivePatternMatch + {nonmatch with calling_context= call_and_loc :: nonmatch.calling_context} | ReadUninitializedValue read -> ReadUninitializedValue {read with calling_context= call_and_loc :: read.calling_context} @@ -47,5 +53,7 @@ let should_report (astate : AbductiveDomain.summary) (diagnostic : Diagnostic.t) `ReportNow | AccessToInvalidAddress latent -> if is_manifest astate then `ReportNow else `DelayReport (AccessToInvalidAddress latent) + | NonexhaustivePatternMatch latent -> + if is_manifest astate then `ReportNow else `DelayReport (NonexhaustivePatternMatch latent) | ReadUninitializedValue latent -> if is_manifest astate then `ReportNow else `DelayReport (ReadUninitializedValue latent) diff --git a/infer/src/pulse/PulseLatentIssue.mli b/infer/src/pulse/PulseLatentIssue.mli index 99e4a95a6..8532b25e8 100644 --- a/infer/src/pulse/PulseLatentIssue.mli +++ b/infer/src/pulse/PulseLatentIssue.mli @@ -15,6 +15,7 @@ module AbductiveDomain = PulseAbductiveDomain type t = | AccessToInvalidAddress of Diagnostic.access_to_invalid_address + | NonexhaustivePatternMatch of Diagnostic.nonexhaustive_pattern_match | ReadUninitializedValue of Diagnostic.read_uninitialized_value [@@deriving compare, equal, yojson_of] diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index b964b56a9..181b10504 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -1506,6 +1506,52 @@ module Android = struct List.rev_append astate_null astate_not_null end +module Erlang = struct + let pattern_fail : model = + fun {location} astate -> + [ Error + (ReportableError + {astate; diagnostic= NonexhaustivePatternMatch {calling_context= []; location}}) ] + + + let make_nil : model = + fun {location; ret= ret_id, _} astate -> + let event = ValueHistory.Allocation {f= Model "[]"; location} in + let addr_nil_val = AbstractValue.mk_fresh () in + let addr_nil = (addr_nil_val, [event]) in + let astate = + let typ = Typ.mk_struct (ErlangType Nil) in + PulseOperations.add_dynamic_type typ addr_nil_val astate + in + let astate = PulseOperations.write_id ret_id addr_nil astate in + [Ok (ContinueProgram astate)] + + + let make_cons head tail : model = + fun {location; path; ret= ret_id, _} astate -> + let event = ValueHistory.Allocation {f= Model "[X|Xs]"; location} in + let addr_head_val = AbstractValue.mk_fresh () in + let addr_tail_val = AbstractValue.mk_fresh () in + let addr_cons_val = AbstractValue.mk_fresh () in + let addr_head = (addr_head_val, [event]) in + let addr_tail = (addr_tail_val, [event]) in + let addr_cons = (addr_cons_val, [event]) in + let field name = Fieldname.make (ErlangType Cons) name in + let<*> astate = + PulseOperations.write_field path location ~ref:addr_cons (field "head") ~obj:addr_head astate + in + let<*> astate = PulseOperations.write_deref path location ~ref:addr_head ~obj:head astate in + let<*> astate = + PulseOperations.write_field path location ~ref:addr_cons (field "tail") ~obj:addr_tail astate + in + let<+> astate = PulseOperations.write_deref path location ~ref:addr_tail ~obj:tail astate in + let astate = + let typ = Typ.mk_struct (ErlangType Cons) in + PulseOperations.add_dynamic_type typ addr_cons_val astate + in + PulseOperations.write_id ret_id addr_cons astate +end + module StringSet = Caml.Set.Make (String) module ProcNameDispatcher = struct @@ -1578,6 +1624,10 @@ module ProcNameDispatcher = struct <>$ capt_arg_payload $+...$--> Misc.id_first_arg ~desc:"cast" ; +BuiltinDecl.(match_builtin abort) <>--> Misc.early_exit ; +BuiltinDecl.(match_builtin exit) <>--> Misc.early_exit + ; +BuiltinDecl.(match_builtin __erlang_make_cons) + <>$ capt_arg_payload $+ capt_arg_payload $--> Erlang.make_cons + ; +BuiltinDecl.(match_builtin __erlang_make_nil) <>--> Erlang.make_nil + ; +BuiltinDecl.(match_builtin __erlang_pattern_fail) <>--> Erlang.pattern_fail ; +BuiltinDecl.(match_builtin __infer_initializer_list) <>$ capt_arg_payload $+...$--> Misc.id_first_arg ~desc:"infer_init_list" diff --git a/infer/src/pulse/PulseReport.ml b/infer/src/pulse/PulseReport.ml index 23dce0753..4f59c4659 100644 --- a/infer/src/pulse/PulseReport.ml +++ b/infer/src/pulse/PulseReport.ml @@ -46,7 +46,10 @@ let is_nullsafe_error tenv diagnostic jn = being equal to the value being dereferenced *) let is_constant_deref_without_invalidation (diagnostic : Diagnostic.t) = match diagnostic with - | MemoryLeak _ | ReadUninitializedValue _ | StackVariableAddressEscape _ -> + | MemoryLeak _ + | NonexhaustivePatternMatch _ + | ReadUninitializedValue _ + | StackVariableAddressEscape _ -> false | AccessToInvalidAddress {invalidation; access_trace} -> ( match invalidation with diff --git a/infer/tests/codetoanalyze/erlang/nonmatch/Makefile b/infer/tests/codetoanalyze/erlang/nonmatch/Makefile new file mode 100644 index 000000000..790a5f490 --- /dev/null +++ b/infer/tests/codetoanalyze/erlang/nonmatch/Makefile @@ -0,0 +1,17 @@ +# 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 = --pulse-only --debug-exceptions --project-root $(TESTS_DIR) \ + --pulse-report-latent-issues +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/nonmatch/issues.exp b/infer/tests/codetoanalyze/erlang/nonmatch/issues.exp new file mode 100644 index 000000000..e90da4684 --- /dev/null +++ b/infer/tests/codetoanalyze/erlang/nonmatch/issues.exp @@ -0,0 +1,6 @@ +codetoanalyze/erlang/nonmatch/src/nonmatch.erl, assert_empty/1, 0, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [*** LATENT ***,no pattern match here] +codetoanalyze/erlang/nonmatch/src/nonmatch.erl, assert_second_is_nil/1, 0, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [*** LATENT ***,no pattern match here] +codetoanalyze/erlang/nonmatch/src/nonmatch.erl, list_match_test_a/0, -4, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [calling context starts here,in call to `tail/1`,no pattern match here] +codetoanalyze/erlang/nonmatch/src/nonmatch.erl, list_match_test_b/0, -8, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [calling context starts here,in call to `assert_empty/1`,no pattern match here] +codetoanalyze/erlang/nonmatch/src/nonmatch.erl, list_match_test_c/0, -12, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [calling context starts here,in call to `assert_second_is_nil/1`,no pattern match here] +codetoanalyze/erlang/nonmatch/src/nonmatch.erl, tail/1, 0, NONEXHAUSTIVE_PATTERN_MATCH, no_bucket, ERROR, [*** LATENT ***,no pattern match here] diff --git a/infer/tests/codetoanalyze/erlang/nonmatch/rebar.config b/infer/tests/codetoanalyze/erlang/nonmatch/rebar.config new file mode 100644 index 000000000..aaf3ae0ed --- /dev/null +++ b/infer/tests/codetoanalyze/erlang/nonmatch/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, [nonmatch]} +]}. diff --git a/infer/tests/codetoanalyze/erlang/nonmatch/src/nonmatch.app.src b/infer/tests/codetoanalyze/erlang/nonmatch/src/nonmatch.app.src new file mode 100644 index 000000000..5398609fb --- /dev/null +++ b/infer/tests/codetoanalyze/erlang/nonmatch/src/nonmatch.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, nonmatch, [ + {description, "An Erlang app that is missing many patterns"}, + {vsn, "0.1.0"}, + {registered, []}, + {applications, [ + kernel, + stdlib + ]}, + {modules, []} +]}. diff --git a/infer/tests/codetoanalyze/erlang/nonmatch/src/nonmatch.erl b/infer/tests/codetoanalyze/erlang/nonmatch/src/nonmatch.erl new file mode 100644 index 000000000..e801ed2d0 --- /dev/null +++ b/infer/tests/codetoanalyze/erlang/nonmatch/src/nonmatch.erl @@ -0,0 +1,28 @@ +% 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(nonmatch). + +-export([list_match_test_a/0, list_match_test_b/0, list_match_test_c/0]). + +tail([_ | Xs]) -> Xs. +assert_empty([]) -> ok. +assert_second_is_nil([_, [] | _]) -> ok. + +list_match_test_a() -> + tail([1, 2]), + tail([1]), + tail([]). + +list_match_test_b() -> + assert_empty([]), + assert_empty([1]), + assert_empty([1, 2]). + +list_match_test_c() -> + % FP (T94492137) + assert_second_is_nil([1, [], 2]), + assert_second_is_nil([1, []]), + assert_second_is_nil([1, [2], 3]). diff --git a/infer/tests/erlang.make b/infer/tests/erlang.make new file mode 100644 index 000000000..b9794a339 --- /dev/null +++ b/infer/tests/erlang.make @@ -0,0 +1,10 @@ +# 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. +include $(TESTS_DIR)/infer.make + +infer-out$(TEST_SUFFIX)/report.json: $(SOURCES) $(TESTS_DIR)/.inferconfig $(MAKEFILE_LIST) + $(QUIET)$(call silent_on_success,Testing infer/erlang in $(TEST_REL_DIR),\ + $(INFER_BIN) --results-dir $(@D) --dump-duplicate-symbols \ + $(INFER_OPTIONS) -- rebar3 compile)