[erl-frontend] Support tuples

Summary: Add support for tuples, including expressions, pattern matching and pulse models. Tuples are modeled similarly to `Cons` (lists): they have a dynamic type (including the size of the tuple) and elements as fields.

Reviewed By: mmarescotti

Differential Revision: D29875650

fbshipit-source-id: f0262a42c

infer/src/IR/BuiltinDecl.ml

@@ -88,6 +88,8 @@ let __erlang_make_cons = create_procname "__erlang_make_cons"
 
 let __erlang_make_nil = create_procname "__erlang_make_nil"
 
+let __erlang_make_tuple = create_procname "__erlang_make_tuple"
+
 let __exit = create_procname "_exit"
 
 let __objc_bridge_transfer = create_procname "__objc_bridge_transfer"

infer/src/IR/BuiltinDecl.mli

@@ -25,6 +25,8 @@ val __erlang_make_cons : Procname.t
 
 val __erlang_make_nil : Procname.t
 
+val __erlang_make_tuple : Procname.t
+
 val __infer_initializer_list : Procname.t
 
 val __infer_skip_function : Procname.t

infer/src/IR/ErlangTypeName.ml

@@ -8,7 +8,7 @@
 open! IStd
 
 (* TODO: Add other types as they are needed by translation (otherwise it's dead code). *)
-type t = Any | Cons | Nil [@@deriving compare, yojson_of]
+type t = Any | Cons | Nil | Tuple of int [@@deriving compare, yojson_of]
 
 let pp f = function
   | Any ->
@@ -17,6 +17,14 @@ let pp f = function
       Format.fprintf f "ErlangNil"
   | Cons ->
       Format.fprintf f "ErlangCons"
+  | Tuple arity ->
+      Format.fprintf f "ErlangTuple%d" arity
 
 
 let to_string name = Format.asprintf "%a" pp name
+
+let cons_head = "head"
+
+let cons_tail = "tail"
+
+let tuple_field_names size = List.init size ~f:(Printf.sprintf "elem%d")

infer/src/erlang/ErlangTranslator.ml

@@ -240,26 +240,22 @@ let rec translate_pattern env (value : Ident.t) {Ast.line; simple_expression} :
   let any = ptr_typ_of_name Any in
   let (Present procdesc) = env.procdesc in
   let procname = Procdesc.get_proc_name procdesc in
+  let load_field id field typ : Sil.instr =
+    (* x=value.field *)
+    let field = Fieldname.make (ErlangType typ) field in
+    Load
+      {id; e= Lfield (Var value, field, typ_of_name typ); root_typ= any; typ= any; loc= env.location}
+  in
   match simple_expression with
   | Cons {head; tail} ->
-      let id = Ident.create_fresh Ident.knormal in
+      let is_right_type_id = Ident.create_fresh Ident.knormal in
-      let start = Node.make_stmt env [has_type env ~result:id ~value Cons] in
+      let start = Node.make_stmt env [has_type env ~result:is_right_type_id ~value Cons] in
-      let right_type_node = Node.make_if env true (Var id) in
+      let right_type_node = Node.make_if env true (Var is_right_type_id) in
-      let wrong_type_node = Node.make_if env false (Var id) in
+      let wrong_type_node = Node.make_if env false (Var is_right_type_id) in
-      let load id field : Sil.instr =
-        (* x=value.field *)
-        let field = Fieldname.make (ErlangType Cons) field in
-        Load
-          { id
-          ; e= Lfield (Var value, field, typ_of_name Cons)
-          ; root_typ= any
-          ; typ= any
-          ; loc= env.location }
-      in
       let head_value = Ident.create_fresh Ident.knormal in
       let tail_value = Ident.create_fresh Ident.knormal in
-      let head_load = load head_value "head" in
+      let head_load = load_field head_value ErlangTypeName.cons_head Cons in
-      let tail_load = load tail_value "tail" in
+      let tail_load = load_field tail_value ErlangTypeName.cons_tail Cons in
       let unpack_node = Node.make_stmt env [head_load; tail_load] in
       let head_matcher = translate_pattern env head_value head in
       let tail_matcher = translate_pattern env tail_value tail in
@@ -286,6 +282,33 @@ let rec translate_pattern env (value : Ident.t) {Ast.line; simple_expression} :
       let exit_failure = Node.make_if env false (Var id) in
       start |~~> [exit_success; exit_failure] ;
       {start; exit_success; exit_failure}
+  | Tuple exprs ->
+      let is_right_type_id = Ident.create_fresh Ident.knormal in
+      let tuple_typ : ErlangTypeName.t = Tuple (List.length exprs) in
+      let start = Node.make_stmt env [has_type env ~result:is_right_type_id ~value tuple_typ] in
+      let right_type_node = Node.make_if env true (Var is_right_type_id) in
+      let wrong_type_node = Node.make_if env false (Var is_right_type_id) in
+      let value_ids = List.map ~f:(function _ -> Ident.create_fresh Ident.knormal) exprs in
+      let field_names = ErlangTypeName.tuple_field_names (List.length exprs) in
+      let load_instructions =
+        List.map
+          ~f:(function one_value, one_field -> load_field one_value one_field tuple_typ)
+          (List.zip_exn value_ids field_names)
+      in
+      let unpack_node = Node.make_stmt env load_instructions in
+      let matchers =
+        List.map
+          ~f:(function one_expr, one_value -> translate_pattern env one_value one_expr)
+          (List.zip_exn exprs value_ids)
+      in
+      let submatcher = Block.all env matchers in
+      let exit_failure = Node.make_nop env in
+      start |~~> [right_type_node; wrong_type_node] ;
+      right_type_node |~~> [unpack_node] ;
+      unpack_node |~~> [submatcher.start] ;
+      wrong_type_node |~~> [exit_failure] ;
+      submatcher.exit_failure |~~> [exit_failure] ;
+      {start; exit_success= submatcher.exit_success; exit_failure}
   | UnaryOperator _ ->
       (* Unary op pattern must evaluate to number, so just delegate to expression translation *)
       let id = Ident.create_fresh Ident.knormal in
@@ -517,6 +540,24 @@ and translate_expression env {Ast.line; simple_expression} =
         let fun_exp = Exp.Const (Cfun BuiltinDecl.__erlang_make_nil) in
         let instruction = Sil.Call ((ret_var, any), fun_exp, [], env.location, CallFlags.default) in
         Block.make_instruction env [instruction]
+    | Tuple exprs ->
+        let exprs_with_ids = List.map ~f:(fun e -> (e, Ident.create_fresh Ident.knormal)) exprs in
+        let expr_blocks =
+          let f (one_expr, one_id) =
+            let result = Present (Exp.Var one_id) in
+            translate_expression {env with result} one_expr
+          in
+          List.map ~f exprs_with_ids
+        in
+        let fun_exp = Exp.Const (Cfun BuiltinDecl.__erlang_make_tuple) in
+        let exprs_ids_and_types =
+          List.map ~f:(function _, id -> (Exp.Var id, any)) exprs_with_ids
+        in
+        let call_instruction =
+          Sil.Call ((ret_var, any), fun_exp, exprs_ids_and_types, env.location, CallFlags.default)
+        in
+        let call_block = Block.make_instruction env [call_instruction] in
+        Block.all env (expr_blocks @ [call_block])
     | UnaryOperator (op, e) ->
         let id = Ident.create_fresh Ident.knormal in
         let block = translate_expression {env with result= Present (Exp.Var id)} e in

infer/src/pulse/PulseModels.ml

@@ -1557,11 +1557,13 @@ module Erlang = struct
     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
+      PulseOperations.write_field path location ~ref:addr_cons (field ErlangTypeName.cons_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
+      PulseOperations.write_field path location ~ref:addr_cons (field ErlangTypeName.cons_tail)
+        ~obj:addr_tail astate
     in
     let<+> astate = PulseOperations.write_deref path location ~ref:addr_tail ~obj:tail astate in
     let astate =
@@ -1569,6 +1571,38 @@ module Erlang = struct
       PulseOperations.add_dynamic_type typ addr_cons_val astate
     in
     PulseOperations.write_id ret_id addr_cons astate
+
+
+  let make_tuple (args : 'a ProcnameDispatcher.Call.FuncArg.t list) : model =
+   fun {location; path; ret= ret_id, _} astate ->
+    let tuple_size = List.length args in
+    let tuple_typ_name : Typ.name = ErlangType (Tuple tuple_size) in
+    let event = ValueHistory.Allocation {f= Model "{}"; location} in
+    let addr_tuple_val = AbstractValue.mk_fresh () in
+    let addr_tuple = (addr_tuple_val, [event]) in
+    let addr_elems = List.map ~f:(function _ -> (AbstractValue.mk_fresh (), [event])) args in
+    let mk_field name = Fieldname.make tuple_typ_name name in
+    let field_names = ErlangTypeName.tuple_field_names tuple_size in
+    let get_payload (arg : 'a ProcnameDispatcher.Call.FuncArg.t) = arg.arg_payload in
+    let arg_payloads = List.map ~f:get_payload args in
+    let addr_elems_fields_payloads =
+      List.zip_exn addr_elems (List.zip_exn field_names arg_payloads)
+    in
+    let write_field_and_deref astate (addr_elem, (field_name, payload)) =
+      let* astate =
+        PulseOperations.write_field path location ~ref:addr_tuple (mk_field field_name)
+          ~obj:addr_elem astate
+      in
+      PulseOperations.write_deref path location ~ref:addr_elem ~obj:payload astate
+    in
+    let<+> astate =
+      List.fold_result addr_elems_fields_payloads ~init:astate ~f:write_field_and_deref
+    in
+    let astate =
+      let typ = Typ.mk_struct tuple_typ_name in
+      PulseOperations.add_dynamic_type typ addr_tuple_val astate
+    in
+    PulseOperations.write_id ret_id addr_tuple astate
 end
 
 module StringSet = Caml.Set.Make (String)
@@ -1645,6 +1679,7 @@ module ProcNameDispatcher = struct
         ; +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_tuple) &++> Erlang.make_tuple
         ; +BuiltinDecl.(match_builtin __erlang_make_nil) <>--> Erlang.make_nil
         ; +BuiltinDecl.(match_builtin __erlang_error_badmatch) <>--> Erlang.error_badmatch
         ; +BuiltinDecl.(match_builtin __erlang_error_case_clause) <>--> Erlang.error_case_clause

infer/tests/codetoanalyze/erlang/features/issues.exp

@@ -46,3 +46,11 @@ codetoanalyze/erlang/features/src/short_circuit.erl, test_and_Bad/0, -7, NO_MATC
 codetoanalyze/erlang/features/src/short_circuit.erl, test_andalso_Bad/0, -15, NO_MATCHING_FUNCTION_CLAUSE, no_bucket, ERROR, [calling context starts here,in call to `accepts_one/1`,no matching function clause here]
 codetoanalyze/erlang/features/src/short_circuit.erl, test_or_Bad/0, -23, NO_MATCHING_FUNCTION_CLAUSE, no_bucket, ERROR, [calling context starts here,in call to `accepts_one/1`,no matching function clause here]
 codetoanalyze/erlang/features/src/short_circuit.erl, test_orelse_Bad/0, -31, NO_MATCHING_FUNCTION_CLAUSE, no_bucket, ERROR, [calling context starts here,in call to `accepts_one/1`,no matching function clause here]
+codetoanalyze/erlang/features/src/tuples.erl, first/1, 0, NO_MATCHING_FUNCTION_CLAUSE, no_bucket, ERROR, [*** LATENT ***,no matching function clause here]
+codetoanalyze/erlang/features/src/tuples.erl, second/1, 0, NO_MATCHING_FUNCTION_CLAUSE, no_bucket, ERROR, [*** LATENT ***,no matching function clause here]
+codetoanalyze/erlang/features/src/tuples.erl, test_first_Bad/0, -12, NO_MATCHING_FUNCTION_CLAUSE, no_bucket, ERROR, [calling context starts here,in call to `warn/1`,no matching function clause here]
+codetoanalyze/erlang/features/src/tuples.erl, test_nested_Bad/0, -48, NO_MATCHING_FUNCTION_CLAUSE, no_bucket, ERROR, [calling context starts here,in call to `warn/1`,no matching function clause here]
+codetoanalyze/erlang/features/src/tuples.erl, test_second_Bad/0, -24, NO_MATCHING_FUNCTION_CLAUSE, no_bucket, ERROR, [calling context starts here,in call to `warn/1`,no matching function clause here]
+codetoanalyze/erlang/features/src/tuples.erl, test_third_Bad/0, -36, NO_MATCHING_FUNCTION_CLAUSE, no_bucket, ERROR, [calling context starts here,in call to `warn/1`,no matching function clause here]
+codetoanalyze/erlang/features/src/tuples.erl, third/1, 0, NO_MATCHING_FUNCTION_CLAUSE, no_bucket, ERROR, [*** LATENT ***,no matching function clause here]
+codetoanalyze/erlang/features/src/tuples.erl, warn/1, 0, NO_MATCHING_FUNCTION_CLAUSE, no_bucket, ERROR, [*** LATENT ***,no matching function clause here]

infer/tests/codetoanalyze/erlang/features/src/tuples.erl

@@ -0,0 +1,72 @@
+% 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(tuples).
+
+-export([
+    test_first_Ok/0,
+    test_first_Bad/0,
+    test_second_Ok/0,
+    test_second_Bad/0,
+    test_third_Ok/0,
+    test_third_Bad/0,
+    test_nested_Ok/0,
+    test_nested_Bad/0
+]).
+
+% Call this method with warn(1) to trigger a warning to expect
+warn(0) -> ok.
+
+first({X, _, _}) -> X.
+second({_, Y, _}) -> Y.
+third({_, _, Z}) -> Z.
+
+test_first_Ok() ->
+    N = first({1, 2, 3}),
+    case N of
+        1 -> ok
+    end.
+
+test_first_Bad() ->
+    N = first({1, 2, 3}),
+    case N of
+        1 -> warn(1)
+    end.
+
+test_second_Ok() ->
+    N = second({1, 2, 3}),
+    case N of
+        2 -> ok
+    end.
+
+test_second_Bad() ->
+    N = second({1, 2, 3}),
+    case N of
+        2 -> warn(1)
+    end.
+
+test_third_Ok() ->
+    N = third({1, 2, 3}),
+    case N of
+        3 -> ok
+    end.
+
+test_third_Bad() ->
+    N = third({1, 2, 3}),
+    case N of
+        3 -> warn(1)
+    end.
+
+test_nested_Ok() ->
+    N = first(second({1, {2, 3, 4}, 5})),
+    case N of
+        2 -> ok
+    end.
+
+test_nested_Bad() ->
+    N = first(second({1, {2, 3, 4}, 5})),
+    case N of
+        2 -> warn(1)
+    end.

infer/tests/codetoanalyze/erlang/nonmatch/issues.exp

@@ -28,3 +28,18 @@ codetoanalyze/erlang/nonmatch/src/match.erl, match_test_e_Bad/0, -15, NO_MATCHIN
 codetoanalyze/erlang/nonmatch/src/match.erl, match_test_g_Bad/0, 7, NO_MATCHING_FUNCTION_CLAUSE, no_bucket, ERROR, [calling context starts here,in call to `only_accepts_one/1`,no matching function clause here]
 codetoanalyze/erlang/nonmatch/src/match.erl, only_accepts_one/1, 0, NO_MATCHING_FUNCTION_CLAUSE, no_bucket, ERROR, [*** LATENT ***,no matching function clause here]
 codetoanalyze/erlang/nonmatch/src/match.erl, tail/1, 0, NO_MATCHING_FUNCTION_CLAUSE, no_bucket, ERROR, [*** LATENT ***,no matching function clause here]
+codetoanalyze/erlang/nonmatch/src/tuples.erl, accepts_empty/1, 0, NO_MATCHING_FUNCTION_CLAUSE, no_bucket, ERROR, [*** LATENT ***,no matching function clause here]
+codetoanalyze/erlang/nonmatch/src/tuples.erl, accepts_tuple_of_two/1, 0, NO_MATCHING_FUNCTION_CLAUSE, no_bucket, ERROR, [*** LATENT ***,no matching function clause here]
+codetoanalyze/erlang/nonmatch/src/tuples.erl, first_from_at_most_three/1, 0, NO_MATCHING_FUNCTION_CLAUSE, no_bucket, ERROR, [*** LATENT ***,no matching function clause here]
+codetoanalyze/erlang/nonmatch/src/tuples.erl, test_elements2_Bad/0, 2, NO_MATCH_OF_RHS, no_bucket, ERROR, [no match of RHS here]
+codetoanalyze/erlang/nonmatch/src/tuples.erl, test_elements3_Bad/0, 2, NO_MATCH_OF_RHS, no_bucket, ERROR, [no match of RHS here]
+codetoanalyze/erlang/nonmatch/src/tuples.erl, test_elements_partial3_Bad/0, 2, NO_MATCH_OF_RHS, no_bucket, ERROR, [no match of RHS here]
+codetoanalyze/erlang/nonmatch/src/tuples.erl, test_elements_partial4_Bad/0, 2, NO_MATCH_OF_RHS, no_bucket, ERROR, [no match of RHS here]
+codetoanalyze/erlang/nonmatch/src/tuples.erl, test_empty2_Bad/0, -5, NO_MATCHING_FUNCTION_CLAUSE, no_bucket, ERROR, [calling context starts here,in call to `accepts_empty/1`,no matching function clause here]
+codetoanalyze/erlang/nonmatch/src/tuples.erl, test_empty3_Bad/0, -8, NO_MATCHING_FUNCTION_CLAUSE, no_bucket, ERROR, [calling context starts here,in call to `accepts_empty/1`,no matching function clause here]
+codetoanalyze/erlang/nonmatch/src/tuples.erl, test_first4_Bad/0, -13, NO_MATCHING_FUNCTION_CLAUSE, no_bucket, ERROR, [calling context starts here,in call to `first_from_at_most_three/1`,no matching function clause here]
+codetoanalyze/erlang/nonmatch/src/tuples.erl, test_first5_Bad/0, -16, NO_MATCHING_FUNCTION_CLAUSE, no_bucket, ERROR, [calling context starts here,in call to `first_from_at_most_three/1`,no matching function clause here]
+codetoanalyze/erlang/nonmatch/src/tuples.erl, test_nested3_Bad/0, 2, NO_MATCH_OF_RHS, no_bucket, ERROR, [no match of RHS here]
+codetoanalyze/erlang/nonmatch/src/tuples.erl, test_nested4_Bad/0, 2, NO_MATCH_OF_RHS, no_bucket, ERROR, [no match of RHS here]
+codetoanalyze/erlang/nonmatch/src/tuples.erl, test_size2_Bad/0, -5, NO_MATCHING_FUNCTION_CLAUSE, no_bucket, ERROR, [calling context starts here,in call to `accepts_tuple_of_two/1`,no matching function clause here]
+codetoanalyze/erlang/nonmatch/src/tuples.erl, test_size3_Bad/0, -8, NO_MATCHING_FUNCTION_CLAUSE, no_bucket, ERROR, [calling context starts here,in call to `accepts_tuple_of_two/1`,no matching function clause here]

infer/tests/codetoanalyze/erlang/nonmatch/src/tuples.erl

@@ -0,0 +1,120 @@
+% 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(tuples).
+
+-export([
+    test_size1_Ok/0,
+    test_size2_Bad/0,
+    test_size3_Bad/0,
+    test_elements1_Ok/0,
+    test_elements2_Bad/0,
+    test_elements3_Bad/0,
+    test_elements_partial1_Ok/0,
+    test_elements_partial2_Ok/0,
+    test_elements_partial3_Bad/0,
+    test_elements_partial4_Bad/0,
+    test_nested1_Ok/0,
+    test_nested2_Ok/0,
+    test_nested3_Bad/0,
+    test_nested4_Bad/0,
+    test_first1_Ok/0,
+    test_first2_Ok/0,
+    test_first3_Ok/0,
+    test_first4_Bad/0,
+    test_first5_Bad/0
+]).
+
+accepts_tuple_of_two({_, _}) -> ok.
+
+test_size1_Ok() ->
+    accepts_tuple_of_two({1, 2}).
+
+test_size2_Bad() ->
+    accepts_tuple_of_two({1, 2, 3}).
+
+test_size3_Bad() ->
+    accepts_tuple_of_two({1}).
+
+test_elements1_Ok() ->
+    T = {1, 2},
+    {1, 2} = T,
+    ok.
+
+test_elements2_Bad() ->
+    T = {1, 2},
+    {1, 3} = T,
+    ok.
+
+test_elements3_Bad() ->
+    T = {1, 2},
+    {1, 2, 3} = T,
+    ok.
+
+test_elements_partial1_Ok() ->
+    T = {1, 2},
+    {1, _} = T,
+    ok.
+
+test_elements_partial2_Ok() ->
+    T = {1, 2},
+    {_, 2} = T,
+    ok.
+
+test_elements_partial3_Bad() ->
+    T = {1, 2},
+    {2, _} = T,
+    ok.
+
+test_elements_partial4_Bad() ->
+    T = {1, 2},
+    {_, 1} = T,
+    ok.
+
+test_nested1_Ok() ->
+    T = {1, {1, 2}, 3},
+    {_, {_, 2}, 3} = T.
+
+test_nested2_Ok() ->
+    T = {{1, 2, 3}, {1, 2}, 3},
+    {_, {_, 2}, 3} = T.
+
+test_nested3_Bad() ->
+    T = {1, {1, 2, 3}, 3},
+    {_, {_, 2}, 3} = T.
+
+test_nested4_Bad() ->
+    T = {1, {1, 2}, 5},
+    {_, {_, 2}, 3} = T.
+
+first_from_at_most_three({X}) -> X;
+first_from_at_most_three({X, _}) -> X;
+first_from_at_most_three({X, _, _}) -> X.
+
+test_first1_Ok() ->
+    first_from_at_most_three({1}).
+
+test_first2_Ok() ->
+    first_from_at_most_three({1, 2}).
+
+test_first3_Ok() ->
+    first_from_at_most_three({1, 2, 3}).
+
+test_first4_Bad() ->
+    first_from_at_most_three({}).
+
+test_first5_Bad() ->
+    first_from_at_most_three({1, 2, 3, 4}).
+
+accepts_empty({}) -> ok.
+
+test_empty1_Ok() ->
+    accepts_empty({}).
+
+test_empty2_Bad() ->
+    accepts_empty({1}).
+
+test_empty3_Bad() ->
+    accepts_empty({1, 2}).