Skip to content

Commit

Permalink
[erlang] Order qualifiers left to right in comprehensions
Browse files Browse the repository at this point in the history
Summary:
Previously, if there was a (list/map) comprehension of the form `Expr || Gen1, Filter1, Gen2, Filter2, ...` we always rearranged it so that the generators came first: `Expr || Gen1, Gen2, ..., Filter1, Filter2, ...`.

Not sure why, though, because they should be evaluated left to right, and there can be cases where reordering results in different behavior, see new test added. I think when I first implemented this translation, it was conceptually easier to think of it as: "let's generate all the potential values using nested loops, and then check the filters once we have all the variables bound".

Reviewed By: rgrig, thizanne

Differential Revision: D62128527

fbshipit-source-id: 3a1dae52d56c60cadd85f04700d4adf4897b62f5
  • Loading branch information
hajduakos authored and facebook-github-bot committed Sep 5, 2024
1 parent 510ec11 commit af22ebe
Show file tree
Hide file tree
Showing 4 changed files with 47 additions and 30 deletions.
52 changes: 23 additions & 29 deletions infer/src/erlang/ErlangTranslator.ml
Original file line number Diff line number Diff line change
Expand Up @@ -987,32 +987,8 @@ and translate_expression_lambda (env : (_, _) Env.t) ret_var lambda_name cases p
(* Helper function for the main loop of translating list/map comprehensions, taking care of
generators and filters. *)
and translate_comprehension_loop (env : (_, _) Env.t) loop_body qualifiers : Block.t =
(* Surround expression with filters *)
let apply_one_filter (qual : Ast.qualifier) (acc : Block.t) : Block.t =
match qual with
| Filter expr ->
(* Check expression, execute inner block (accumulator) only if true *)
let result_id, filter_expr_block = translate_expression_to_fresh_id env expr in
let unboxed, unbox_block = unbox_bool env (Exp.Var result_id) in
let true_node = Node.make_if env true unboxed in
let false_node = Node.make_if env false unboxed in
let fail_node = Node.make_nop env in
let succ_node = Node.make_nop env in
let filter_expr_block = Block.all env [filter_expr_block; unbox_block] in
filter_expr_block.exit_success |~~> [true_node; false_node] ;
filter_expr_block.exit_failure |~~> [fail_node] ;
true_node |~~> [acc.start] ;
false_node |~~> [succ_node] ;
acc.exit_success |~~> [succ_node] ;
acc.exit_failure |~~> [fail_node] ;
{start= filter_expr_block.start; exit_success= succ_node; exit_failure= fail_node}
| _ ->
(* Ignore generators *)
acc
in
let loop_body_with_filters = List.fold_right qualifiers ~f:apply_one_filter ~init:loop_body in
(* Wrap filtered expression with loops for generators*)
let apply_one_gen (qual : Ast.qualifier) (acc : Block.t) : Block.t =
(* Surround expression with filters and and loops for generators *)
let apply_one_qualifier (qual : Ast.qualifier) (acc : Block.t) : Block.t =
(* Helper function for the common parts of list/map generators, namely taking elements from
the list one-by-one in a loop (maps are also converted to lists). *)
let make_gen gen_var (init_block : Block.t) mk_matcher : Block.t =
Expand Down Expand Up @@ -1050,6 +1026,22 @@ and translate_comprehension_loop (env : (_, _) Env.t) loop_body qualifiers : Blo
Block.any env (check_blocks @ [fail_block])
in
match qual with
| Filter expr ->
(* Check expression, execute inner block (accumulator) only if true *)
let result_id, filter_expr_block = translate_expression_to_fresh_id env expr in
let unboxed, unbox_block = unbox_bool env (Exp.Var result_id) in
let true_node = Node.make_if env true unboxed in
let false_node = Node.make_if env false unboxed in
let fail_node = Node.make_nop env in
let succ_node = Node.make_nop env in
let filter_expr_block = Block.all env [filter_expr_block; unbox_block] in
filter_expr_block.exit_success |~~> [true_node; false_node] ;
filter_expr_block.exit_failure |~~> [fail_node] ;
true_node |~~> [acc.start] ;
false_node |~~> [succ_node] ;
acc.exit_success |~~> [succ_node] ;
acc.exit_failure |~~> [fail_node] ;
{start= filter_expr_block.start; exit_success= succ_node; exit_failure= fail_node}
| Generator {pattern; expression} ->
let gen_var, init_block = translate_expression_to_fresh_id env expression in
let check_block = make_gen_checker gen_var [Nil; Cons] in
Expand Down Expand Up @@ -1085,10 +1077,12 @@ and translate_comprehension_loop (env : (_, _) Env.t) loop_body qualifiers : Blo
{matcher with start= key_val_load}
in
make_gen gen_var init_block mk_matcher
| _ ->
acc
| BitsGenerator _ ->
let unsupported = call_unsupported "bits_generator" 0 in
let call_instr = builtin_call env (mk_fresh_id ()) unsupported [] in
Block.all env [Block.make_instruction env [call_instr]; acc]
in
List.fold_right qualifiers ~f:apply_one_gen ~init:loop_body_with_filters
List.fold_right qualifiers ~f:apply_one_qualifier ~init:loop_body


and translate_expression_listcomprehension (env : (_, _) Env.t) ret_var expression qualifiers :
Expand Down
2 changes: 2 additions & 0 deletions infer/tests/codetoanalyze/erlang/compiler/issues.exp
Original file line number Diff line number Diff line change
Expand Up @@ -267,6 +267,8 @@ features_lc:test_filtered1_Bad/0: function_clause
features_lc:test_filtered1_Ok/0: ok
features_lc:test_filtered2_Bad/0: function_clause
features_lc:test_filtered2_Ok/0: ok
features_lc:test_gen_after_filter_Bad/0: function_clause
features_lc:test_gen_after_filter_Ok/0: ok
features_lc:test_simple1_Bad/0: function_clause
features_lc:test_simple1_Ok/0: ok
features_lc:test_simple1a_Bad/0: case_clause
Expand Down
21 changes: 20 additions & 1 deletion infer/tests/codetoanalyze/erlang/pulse/features/features_lc.erl
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,9 @@
test_two_gen1_Bad/0,
test_two_gen2_Ok/0,
test_two_gen2_Bad/0,
test_bad_gen_Bad/0
test_bad_gen_Bad/0,
test_gen_after_filter_Ok/0,
test_gen_after_filter_Bad/0
]).

% Call this method with warn(1) to trigger a warning to expect
Expand Down Expand Up @@ -182,3 +184,20 @@ test_two_gen2_Bad() ->

test_bad_gen_Bad() ->
[X || X <- #{}].


accepts_one(1) -> [ok].

test_gen_after_filter_Ok() ->
L = [X || X <- [1,2], X < 2, _Y <- accepts_one(X)],
case L of
[1] -> ok;
_ -> warn(1)
end.

test_gen_after_filter_Bad() ->
L = [X || X <- [1,2], X < 2, _Y <- accepts_one(X)],
case L of
[1] -> warn(1);
_ -> ok
end.
2 changes: 2 additions & 0 deletions infer/tests/codetoanalyze/erlang/pulse/issues.exp
Original file line number Diff line number Diff line change
Expand Up @@ -150,6 +150,8 @@ codetoanalyze/erlang/pulse/features/features_lc.erl, test_two_filters_Bad/0, 3,
codetoanalyze/erlang/pulse/features/features_lc.erl, test_two_gen1_Bad/0, 3, NO_MATCHING_FUNCTION_CLAUSE, no_bucket, ERROR, [calling context starts here,in call to `warn/1`,no matching function clause here]
codetoanalyze/erlang/pulse/features/features_lc.erl, test_two_gen2_Bad/0, 3, NO_MATCHING_FUNCTION_CLAUSE, no_bucket, ERROR, [calling context starts here,in call to `warn/1`,no matching function clause here]
codetoanalyze/erlang/pulse/features/features_lc.erl, test_bad_gen_Bad/0, 1, BAD_GENERATOR, no_bucket, ERROR, [bad generator here]
codetoanalyze/erlang/pulse/features/features_lc.erl, accepts_one/1, 0, NO_MATCHING_FUNCTION_CLAUSE_LATENT, no_bucket, ERROR, [no matching function clause here]
codetoanalyze/erlang/pulse/features/features_lc.erl, test_gen_after_filter_Bad/0, 3, NO_MATCHING_FUNCTION_CLAUSE, no_bucket, ERROR, [calling context starts here,in call to `warn/1`,no matching function clause here]
codetoanalyze/erlang/pulse/features/features_lists.erl, test_nil_Bad/0, 2, NO_MATCHING_CASE_CLAUSE, no_bucket, ERROR, [no matching case clause here]
codetoanalyze/erlang/pulse/features/features_lists.erl, test_cons1_Bad/0, 4, NO_MATCHING_CASE_CLAUSE, no_bucket, ERROR, [no matching case clause here]
codetoanalyze/erlang/pulse/features/features_lists.erl, test_cons2_Bad/0, 4, NO_MATCHING_CASE_CLAUSE, no_bucket, ERROR, [no matching case clause here]
Expand Down

0 comments on commit af22ebe

Please sign in to comment.