[erlang] Translate variable pattern as equality check or assignment

Summary: Previously we translated variable patterns as an assignment which is incorrect, as variables cannot be bound again in Erlang. The diff below uses scope pre-analysis to determine first usages of variables. This diff then translates variable patterns accordingly to either an assignment or an equality check.

Reviewed By: mmarescotti

Differential Revision: D62151464

fbshipit-source-id: 6969a1392bb74cb1ab9994d4ca5ceb6cd8e453db

infer/src/erlang/ErlangTranslator.ml

@@ -521,17 +521,28 @@ and translate_pattern_number_expression (env : (_, _) Env.t) value location simp
 
 
 and translate_pattern_variable (env : (_, _) Env.t) value vname scope : Block.t =
-  (* We also assign to _ so that stuff like f()->_=1. works. But if we start checking for
-     re-binding, we should exclude _ from such checks. *)
-  let procname = (scope_exn scope).procname in
-  let store : Sil.instr =
-    let e1 : Exp.t = Lvar (Pvar.mk (Mangled.from_string vname) procname) in
-    let e2 : Exp.t = Var value in
-    Store {e1; typ= any_typ; e2; loc= env.location}
-  in
-  let exit_success = Node.make_stmt env [store] in
-  let exit_failure = Node.make_nop env in
-  {start= exit_success; exit_success; exit_failure}
+  let var_scope = scope_exn scope in
+  let var_exp = Exp.Lvar (Pvar.mk (Mangled.from_string vname) var_scope.procname) in
+  if var_scope.is_first_use then
+    let store : Sil.instr =
+      let e1 = var_exp in
+      let e2 = Exp.Var value in
+      Store {e1; typ= any_typ; e2; loc= env.location}
+    in
+    let exit_success = Node.make_stmt env [store] in
+    let exit_failure = Node.make_nop env in
+    {start= exit_success; exit_success; exit_failure}
+  else
+    let var_id = mk_fresh_id () in
+    let load_instr = Sil.Load {id= var_id; e= var_exp; typ= any_typ; loc= env.location} in
+    let is_equal = mk_fresh_id () in
+    let eq_instr =
+      builtin_call env is_equal BuiltinDecl.__erlang_equal [Exp.Var var_id; Exp.Var value]
+    in
+    let eq_block = Block.make_instruction env [load_instr; eq_instr] in
+    let is_equal, unbox_block = unbox_bool env (Var is_equal) in
+    let check_eq_block = Block.make_branch env [] is_equal in
+    Block.all env [eq_block; unbox_block; check_eq_block]
 
 
 and translate_guard_expression (env : (_, _) Env.t) (expression : Ast.expression) : Exp.t * Block.t

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

@@ -269,6 +269,8 @@ features_lc:test_filtered2_Bad/0: expected_crash
 features_lc:test_filtered2_Ok/0: ok
 features_lc:test_gen_after_filter_Bad/0: expected_crash
 features_lc:test_gen_after_filter_Ok/0: ok
+features_lc:test_scoping1_Ok/0: ok
+features_lc:test_scoping2_Ok/0: ok
 features_lc:test_simple1_Bad/0: expected_crash
 features_lc:test_simple1_Ok/0: ok
 features_lc:test_simple1a_Bad/0: case_clause
@@ -564,16 +566,16 @@ nonmatch_atoms:test_match7_Bad/0: function_clause
 
 ----- nonmatch_case_expr -----
 nonmatch_case_expr:fn_test_arg_Bad/0: case_clause
-nonmatch_case_expr:fn_test_constant_vs_arg_Bad/0: case_clause
-nonmatch_case_expr:fn_test_local_var_Bad/0: case_clause
 nonmatch_case_expr:test_arg_Ok/0: ok
 nonmatch_case_expr:test_case_simple1_Ok/0: ok
 nonmatch_case_expr:test_case_simple2_Ok/0: ok
 nonmatch_case_expr:test_case_simple3_Bad/0: case_clause
 nonmatch_case_expr:test_case_tail1_Ok/0: ok
 nonmatch_case_expr:test_case_tail2_Ok/0: ok
 nonmatch_case_expr:test_case_tail3_Bad/0: case_clause
+nonmatch_case_expr:test_constant_vs_arg_Bad/0: case_clause
 nonmatch_case_expr:test_constant_vs_arg_Ok/0: ok
+nonmatch_case_expr:test_local_var_Bad/0: case_clause
 nonmatch_case_expr:test_local_var_Ok/0: ok
 
 ----- nonmatch_case_guards -----
@@ -661,13 +663,7 @@ nonmatch_maps:test_update_match_in_function_Ok/0: ok
 nonmatch_maps:test_update_old_value_Ok/0: ok
 
 ----- nonmatch_match_expr -----
-nonmatch_match_expr:fn_test_match_func_arg_Bad/0: badmatch
 nonmatch_match_expr:fn_test_match_func_args_Bad/0: badmatch
-nonmatch_match_expr:fn_test_match_with_var_Bad/0: badmatch
-nonmatch_match_expr:fn_test_match_with_var_swapped_Bad/0: badmatch
-nonmatch_match_expr:fn_test_not_real_anon_match1_Bad/0: badmatch
-nonmatch_match_expr:fn_test_not_real_anon_match2_Bad/0: badmatch
-nonmatch_match_expr:fn_test_simple_match_Bad/0: badmatch
 nonmatch_match_expr:test_match_a_Ok/0: ok
 nonmatch_match_expr:test_match_anonymus_Ok/0: ok
 nonmatch_match_expr:test_match_b_Bad/0: badmatch
@@ -677,6 +673,7 @@ nonmatch_match_expr:test_match_e_Bad/0: function_clause
 nonmatch_match_expr:test_match_eager_Bad/0: badmatch
 nonmatch_match_expr:test_match_eager_Ok/0: ok
 nonmatch_match_expr:test_match_f_Ok/0: ok
+nonmatch_match_expr:test_match_func_arg_Bad/0: badmatch
 nonmatch_match_expr:test_match_func_arg_Ok/0: ok
 nonmatch_match_expr:test_match_func_args_Ok/0: ok
 nonmatch_match_expr:test_match_g_Bad/0: function_clause
@@ -689,8 +686,13 @@ nonmatch_match_expr:test_match_in_pattern_f_Bad/0: case_clause
 nonmatch_match_expr:test_match_nested1_Ok/0: ok
 nonmatch_match_expr:test_match_nested2_Bad/0: badmatch
 nonmatch_match_expr:test_match_nested3_Bad/0: badmatch
+nonmatch_match_expr:test_match_with_var_Bad/0: badmatch
 nonmatch_match_expr:test_match_with_var_Ok/0: ok
+nonmatch_match_expr:test_match_with_var_swapped_Bad/0: badmatch
 nonmatch_match_expr:test_match_with_var_swapped_Ok/0: ok
+nonmatch_match_expr:test_not_real_anon_match1_Bad/0: badmatch
+nonmatch_match_expr:test_not_real_anon_match2_Bad/0: badmatch
+nonmatch_match_expr:test_simple_match_Bad/0: badmatch
 
 ----- nonmatch_maybe -----
 nonmatch_maybe:test_maybe1_Ok/0: ok

infer/tests/codetoanalyze/erlang/pulse-taint/simple/pulse_taint_simple.erl

@@ -93,7 +93,7 @@ test_taint10_Ok() ->
     sink(not_tainted).
 
 test_taint11_Ok() ->
-    X = source(),
+    _X = source(),
     X = not_tainted,
     sink(X).
 

infer/tests/codetoanalyze/erlang/pulse/features/features_lc.erl

@@ -30,7 +30,9 @@
     test_two_gen2_Bad/0,
     test_bad_gen_Bad/0,
     test_gen_after_filter_Ok/0,
-    test_gen_after_filter_Bad/0
+    test_gen_after_filter_Bad/0,
+    test_scoping1_Ok/0,
+    test_scoping2_Ok/0
 ]).
 
 test_empty_Ok() ->
@@ -133,3 +135,14 @@ test_gen_after_filter_Ok() ->
 test_gen_after_filter_Bad() ->
     L = [X || X <- [1,2], X < 2, _Y <- accepts_one(X)],
     ?CRASH_IF_EQUAL([1], L).
+
+test_scoping1_Ok() ->
+    _ = [X || X <- [1]],
+    % This X is different from the one in the list comprehension
+    X = 2,
+    _ = X.
+
+test_scoping2_Ok() ->
+    % Both Xs are different ones
+    _ = [X || X <- [1]],
+    _ = [X || X <- [2]].

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

@@ -322,6 +322,11 @@ codetoanalyze/erlang/pulse/nonmatch/nonmatch_case_expr.erl, case_simple/1, 1, NO
 codetoanalyze/erlang/pulse/nonmatch/nonmatch_case_expr.erl, tail_with_case/1, 1, NO_MATCHING_CASE_CLAUSE_LATENT, no_bucket, ERROR, [no matching case clause here]
 codetoanalyze/erlang/pulse/nonmatch/nonmatch_case_expr.erl, test_case_simple3_Bad/0, 1, NO_MATCHING_CASE_CLAUSE, no_bucket, ERROR, [calling context starts here,in call to `case_simple/1`,no matching case clause here]
 codetoanalyze/erlang/pulse/nonmatch/nonmatch_case_expr.erl, test_case_tail3_Bad/0, 1, NO_MATCHING_CASE_CLAUSE, no_bucket, ERROR, [calling context starts here,in call to `tail_with_case/1`,no matching case clause here]
+codetoanalyze/erlang/pulse/nonmatch/nonmatch_case_expr.erl, fp_crash_if_different/2, 2, NO_MATCHING_CASE_CLAUSE, no_bucket, ERROR, [no matching case clause here]
+codetoanalyze/erlang/pulse/nonmatch/nonmatch_case_expr.erl, crash_if_not_one/1, 3, NO_MATCHING_CASE_CLAUSE_LATENT, no_bucket, ERROR, [no matching case clause here]
+codetoanalyze/erlang/pulse/nonmatch/nonmatch_case_expr.erl, test_local_var_Bad/0, 1, NO_MATCHING_CASE_CLAUSE, no_bucket, ERROR, [calling context starts here,in call to `crash_if_not_one/1`,no matching case clause here]
+codetoanalyze/erlang/pulse/nonmatch/nonmatch_case_expr.erl, crash_if_not_one_constant/1, 2, NO_MATCHING_CASE_CLAUSE_LATENT, no_bucket, ERROR, [no matching case clause here]
+codetoanalyze/erlang/pulse/nonmatch/nonmatch_case_expr.erl, test_constant_vs_arg_Bad/0, 1, NO_MATCHING_CASE_CLAUSE, no_bucket, ERROR, [calling context starts here,in call to `crash_if_not_one_constant/1`,no matching case clause here]
 codetoanalyze/erlang/pulse/nonmatch/nonmatch_case_guards.erl, accepts_positive/1, 1, NO_MATCHING_CASE_CLAUSE_LATENT, no_bucket, ERROR, [no matching case clause here]
 codetoanalyze/erlang/pulse/nonmatch/nonmatch_case_guards.erl, accepts_positive2/1, 1, NO_MATCHING_CASE_CLAUSE_LATENT, no_bucket, ERROR, [no matching case clause here]
 codetoanalyze/erlang/pulse/nonmatch/nonmatch_case_guards.erl, test_accepts_positive_Bad/0, 1, NO_MATCHING_CASE_CLAUSE, no_bucket, ERROR, [calling context starts here,in call to `accepts_positive/1`,no matching case clause here]
@@ -385,6 +390,16 @@ codetoanalyze/erlang/pulse/nonmatch/nonmatch_match_expr.erl, test_match_nested2_
 codetoanalyze/erlang/pulse/nonmatch/nonmatch_match_expr.erl, test_match_nested3_Bad/0, 1, NO_MATCH_OF_RHS, no_bucket, ERROR, [no match of RHS here]
 codetoanalyze/erlang/pulse/nonmatch/nonmatch_match_expr.erl, test_match_eager_Bad/0, 2, NO_MATCH_OF_RHS, no_bucket, ERROR, [no match of RHS here]
 codetoanalyze/erlang/pulse/nonmatch/nonmatch_match_expr.erl, only_accepts_one/1, 0, NO_MATCHING_FUNCTION_CLAUSE_LATENT, no_bucket, ERROR, [no matching function clause here]
+codetoanalyze/erlang/pulse/nonmatch/nonmatch_match_expr.erl, fp_crash_if_different/2, 1, NO_MATCH_OF_RHS, no_bucket, ERROR, [no match of RHS here]
+codetoanalyze/erlang/pulse/nonmatch/nonmatch_match_expr.erl, crash_if_not_one/1, 1, NO_MATCH_OF_RHS_LATENT, no_bucket, ERROR, [no match of RHS here]
+codetoanalyze/erlang/pulse/nonmatch/nonmatch_match_expr.erl, test_match_func_arg_Bad/0, 1, NO_MATCH_OF_RHS, no_bucket, ERROR, [calling context starts here,in call to `crash_if_not_one/1`,no match of RHS here]
+codetoanalyze/erlang/pulse/nonmatch/nonmatch_match_expr.erl, crash_if_not_one_with_var/1, 2, NO_MATCH_OF_RHS_LATENT, no_bucket, ERROR, [no match of RHS here]
+codetoanalyze/erlang/pulse/nonmatch/nonmatch_match_expr.erl, test_match_with_var_Bad/0, 1, NO_MATCH_OF_RHS, no_bucket, ERROR, [calling context starts here,in call to `crash_if_not_one_with_var/1`,no match of RHS here]
+codetoanalyze/erlang/pulse/nonmatch/nonmatch_match_expr.erl, crash_if_not_one_with_var_swapped/1, 2, NO_MATCH_OF_RHS_LATENT, no_bucket, ERROR, [no match of RHS here]
+codetoanalyze/erlang/pulse/nonmatch/nonmatch_match_expr.erl, test_match_with_var_swapped_Bad/0, 1, NO_MATCH_OF_RHS, no_bucket, ERROR, [calling context starts here,in call to `crash_if_not_one_with_var_swapped/1`,no match of RHS here]
+codetoanalyze/erlang/pulse/nonmatch/nonmatch_match_expr.erl, test_simple_match_Bad/0, 2, NO_MATCH_OF_RHS, no_bucket, ERROR, [no match of RHS here]
+codetoanalyze/erlang/pulse/nonmatch/nonmatch_match_expr.erl, test_not_real_anon_match1_Bad/0, 3, NO_MATCH_OF_RHS, no_bucket, ERROR, [no match of RHS here]
+codetoanalyze/erlang/pulse/nonmatch/nonmatch_match_expr.erl, test_not_real_anon_match2_Bad/0, 3, NO_MATCH_OF_RHS, no_bucket, ERROR, [no match of RHS here]
 codetoanalyze/erlang/pulse/nonmatch/nonmatch_maybe.erl, test_maybe4_Bad/0, 1, NO_MATCHING_ELSE_CLAUSE, no_bucket, ERROR, [no matching else clause here]
 codetoanalyze/erlang/pulse/nonmatch/nonmatch_records.erl, accepts_rabbits/1, 0, NO_MATCHING_FUNCTION_CLAUSE_LATENT, no_bucket, ERROR, [no matching function clause here]
 codetoanalyze/erlang/pulse/nonmatch/nonmatch_records.erl, test_type_Bad/0, 1, NO_MATCHING_FUNCTION_CLAUSE, no_bucket, ERROR, [calling context starts here,in call to `accepts_rabbits/1`,no matching function clause here]

infer/tests/codetoanalyze/erlang/pulse/nonmatch/nonmatch_case_expr.erl

@@ -15,9 +15,9 @@
     test_arg_Ok/0,
     fn_test_arg_Bad/0,
     test_local_var_Ok/0,
-    fn_test_local_var_Bad/0,
+    test_local_var_Bad/0,
     test_constant_vs_arg_Ok/0,
-    fn_test_constant_vs_arg_Bad/0
+    test_constant_vs_arg_Bad/0
 ]).
 
 case_simple(X) ->
@@ -45,16 +45,17 @@ test_case_tail2_Ok() ->
 test_case_tail3_Bad() ->
     tail_with_case([]).
 
-crash_if_different(A, B) ->
+% Currently FP because equality model for unknown types
+fp_crash_if_different(A, B) ->
     % The matching of A against the bound B should be compiled to an equality check.
     case A of
         B -> ok
     end.
 
 test_arg_Ok() ->
-    crash_if_different(0, 0).
+    fp_crash_if_different(0, 0).
 fn_test_arg_Bad() ->
-    crash_if_different(0, 1).
+    fp_crash_if_different(0, 1).
 
 crash_if_not_one(A) ->
     B = 1,
@@ -66,7 +67,7 @@ crash_if_not_one(A) ->
 test_local_var_Ok() ->
     crash_if_not_one(1).
 
-fn_test_local_var_Bad() ->
+test_local_var_Bad() ->
     crash_if_not_one(2).
 
 crash_if_not_one_constant(A) ->
@@ -78,5 +79,5 @@ crash_if_not_one_constant(A) ->
 test_constant_vs_arg_Ok() ->
     crash_if_not_one_constant(1).
 
-fn_test_constant_vs_arg_Bad() ->
+test_constant_vs_arg_Bad() ->
     crash_if_not_one_constant(2).

infer/tests/codetoanalyze/erlang/pulse/nonmatch/nonmatch_match_expr.erl

@@ -27,15 +27,15 @@
     test_match_func_args_Ok/0,
     fn_test_match_func_args_Bad/0,
     test_match_func_arg_Ok/0,
-    fn_test_match_func_arg_Bad/0,
+    test_match_func_arg_Bad/0,
     test_match_with_var_Ok/0,
-    fn_test_match_with_var_Bad/0,
+    test_match_with_var_Bad/0,
     test_match_with_var_swapped_Ok/0,
-    fn_test_match_with_var_swapped_Bad/0,
-    fn_test_simple_match_Bad/0,
+    test_match_with_var_swapped_Bad/0,
+    test_simple_match_Bad/0,
     test_match_anonymus_Ok/0,
-    fn_test_not_real_anon_match1_Bad/0,
-    fn_test_not_real_anon_match2_Bad/0
+    test_not_real_anon_match1_Bad/0,
+    test_not_real_anon_match2_Bad/0
 ]).
 
 tail([_ | Xs]) -> Xs.
@@ -132,22 +132,23 @@ two() -> 2.
 
 %% Tests for matching against already bound variables
 
-crash_if_different(A, B) ->
+% Currently FP because equality model for unknown types
+fp_crash_if_different(A, B) ->
     A = B.
 
 test_match_func_args_Ok() ->
-    crash_if_different(1, 1).
+    fp_crash_if_different(1, 1).
 
 fn_test_match_func_args_Bad() ->
-    crash_if_different(1, 2).
+    fp_crash_if_different(1, 2).
 
 crash_if_not_one(A) ->
     A = 1.
 
 test_match_func_arg_Ok() ->
     crash_if_not_one(1).
 
-fn_test_match_func_arg_Bad() ->
+test_match_func_arg_Bad() ->
     crash_if_not_one(2).
 
 crash_if_not_one_with_var(A) ->
@@ -157,7 +158,7 @@ crash_if_not_one_with_var(A) ->
 test_match_with_var_Ok() ->
     crash_if_not_one_with_var(1).
 
-fn_test_match_with_var_Bad() ->
+test_match_with_var_Bad() ->
     crash_if_not_one_with_var(2).
 
 crash_if_not_one_with_var_swapped(A) ->
@@ -167,23 +168,23 @@ crash_if_not_one_with_var_swapped(A) ->
 test_match_with_var_swapped_Ok() ->
     crash_if_not_one_with_var_swapped(1).
 
-fn_test_match_with_var_swapped_Bad() ->
+test_match_with_var_swapped_Bad() ->
     crash_if_not_one_with_var_swapped(2).
 
-fn_test_simple_match_Bad() ->
+test_simple_match_Bad() ->
     A = 1,
     A = 2.
 
 test_match_anonymus_Ok() ->
     _ = 1,
     _ = 2.
 
-fn_test_not_real_anon_match1_Bad() ->
+test_not_real_anon_match1_Bad() ->
     % `_` is the only truly anonymus name
     _A = 1,
     _A = 2.
 
-fn_test_not_real_anon_match2_Bad() ->
+test_not_real_anon_match2_Bad() ->
     % `_` is the only truly anonymus name
     __ = 1,
     __ = 2.