[erl-frontend] First Erlang test with warnings

Summary:
The gist of this diff is a set of Pulse models for the built-ins
that have been put in Sil by the Erlang frontend:
  - __erlang_make_nil, for creating an empty list like []
  - __erlang_make_cons, for creating a nonempty list like [1|[]]
  - __erlang_pattern_fail, which marks that no pattern matched
The models for the first two update the abstract state. The model for
the third generates a reportable error.

The diff also includes a test.

And also a few bugfixes:
  - a type ErlangAny was used sometimes instead of ErlangAny*
  - a load that was meant to be n=13 was instead n=*13;
    changed to (*tmp=13; n=*tmp)
  - the Makefile's guard for the rebar build-system test was inside the large
    guard for java analyzers; of course, we don't need java to run rebar

Reviewed By: jvillard

Differential Revision: D29230161

fbshipit-source-id: c8fd6d88a

.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
 

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 \

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])

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.

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),

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),

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),

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)."

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

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

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 _ ->

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]

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)

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]
 

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"

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

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)

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]

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]}
+]}.

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, []}
+]}.

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]).

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)