From 888521a2abdf44a1ea4800e31ef42d8a0c344992 Mon Sep 17 00:00:00 2001 From: Akos Hajdu Date: Wed, 21 Jul 2021 09:00:03 -0700 Subject: [PATCH] [erl-frontend] Support short circuit logic operators (andalso, orelse) Summary: Add support for short circuit counterparts (andalso, orelse) of the logic operators (and, or). Reviewed By: skcho Differential Revision: D29815177 fbshipit-source-id: 98d28deed --- infer/src/erlang/ErlangTranslator.ml | 123 +++++++++++------- .../codetoanalyze/erlang/features/issues.exp | 9 ++ .../erlang/features/src/logic.erl | 48 +++++++ .../erlang/features/src/short_circuit.erl | 56 ++++++++ 4 files changed, 187 insertions(+), 49 deletions(-) create mode 100644 infer/tests/codetoanalyze/erlang/features/src/short_circuit.erl diff --git a/infer/src/erlang/ErlangTranslator.ml b/infer/src/erlang/ErlangTranslator.ml index 152cd322c..c1efab9e5 100644 --- a/infer/src/erlang/ErlangTranslator.ml +++ b/infer/src/erlang/ErlangTranslator.ml @@ -102,6 +102,17 @@ module Node = struct make env (Stmt_node kind) instructions + let make_load env id e typ = + 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 = + [ Sil.Store {e1= Lvar temp_pvar; e2= e; root_typ= typ; typ; loc= env.location} + ; Sil.Load {id; e= Lvar temp_pvar; root_typ= typ; typ; loc= env.location} ] + in + make_stmt env ~kind:ErlangExpression instructions + + let make_nop env = make_stmt env [] let make_join env = make env Join_node [] @@ -202,14 +213,9 @@ module Block = struct let make_load env id e typ = - 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 = - [ Sil.Store {e1= Lvar temp_pvar; e2= e; root_typ= typ; typ; loc= env.location} - ; Sil.Load {id; e= Lvar temp_pvar; root_typ= typ; typ; loc= env.location} ] - in - make_instruction env instructions + let exit_success = Node.make_load env id e typ in + let exit_failure = Node.make_nop env in + {start= exit_success; exit_success; exit_failure} end let has_type env ~result ~value (name : ErlangTypeName.t) : Sil.instr = @@ -353,51 +359,70 @@ and translate_expression env {Ast.line; simple_expression} = in let expression_block : Block.t = match simple_expression with - | BinaryOperator (e1, op, e2) -> + | 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= 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 + let block1 : Block.t = translate_expression {env with result= Present (Exp.Var id1)} e1 in + let block2 : Block.t = translate_expression {env with result= Present (Exp.Var id2)} e2 in + let make_simple_eager sil_op = + let op_block = Block.make_load env ret_var (Exp.BinOp (sil_op, Var id1, Var id2)) any in + Block.all env [block1; block2; op_block] in - let op_block = - match op with - | Add -> - make_simple_op_block (PlusA None) - | And -> - make_simple_op_block LAnd - | AtLeast -> - make_simple_op_block Ge - | AtMost -> - make_simple_op_block Le - (* TODO: proper modeling of equal vs exactly equal T95767672 *) - | Equal | ExactlyEqual -> - make_simple_op_block Eq - (* TODO: proper modeling of not equal vs exactly not equal T95767672 *) - | ExactlyNotEqual | NotEqual -> - make_simple_op_block Ne - | Greater -> - make_simple_op_block Gt - | IDiv -> - make_simple_op_block Div - | Less -> - make_simple_op_block Lt - | Mul -> - make_simple_op_block (Mult None) - | Or -> - make_simple_op_block LOr - | Rem -> - make_simple_op_block Mod (* TODO: check semantics of Rem vs Mod *) - | Sub -> - make_simple_op_block (MinusA None) - | todo -> - L.debug Capture Verbose - "@[todo ErlangTranslator.translate_expression(BinaryOperator) %s@." - (Sexp.to_string (Ast.sexp_of_binary_operator todo)) ; - Block.make_success env + let make_short_circuit_logic ~short_circuit_when_lhs_is = + let start = Node.make_nop env in + let id1_cond = Node.make_if env short_circuit_when_lhs_is (Var id1) in + let id2_cond = Node.make_if env (not short_circuit_when_lhs_is) (Var id1) in + let store_id1 = Node.make_load env ret_var (Var id1) any in + let store_id2 = Node.make_load env ret_var (Var id2) any in + let exit_success = Node.make_nop env in + let exit_failure = Node.make_nop env in + start |~~> [id1_cond; id2_cond] ; + id1_cond |~~> [store_id1] ; + store_id1 |~~> [exit_success] ; + id2_cond |~~> [block2.start] ; + block2.exit_success |~~> [store_id2] ; + block2.exit_failure |~~> [exit_failure] ; + store_id2 |~~> [exit_success] ; + Block.all env [block1; {start; exit_success; exit_failure}] in - Block.all env [block1; block2; op_block] + match op with + | Add -> + make_simple_eager (PlusA None) + | And -> + make_simple_eager LAnd + | AndAlso -> + make_short_circuit_logic ~short_circuit_when_lhs_is:false + | AtLeast -> + make_simple_eager Ge + | AtMost -> + make_simple_eager Le + (* TODO: proper modeling of equal vs exactly equal T95767672 *) + | Equal | ExactlyEqual -> + make_simple_eager Eq + (* TODO: proper modeling of not equal vs exactly not equal T95767672 *) + | ExactlyNotEqual | NotEqual -> + make_simple_eager Ne + | Greater -> + make_simple_eager Gt + | IDiv -> + make_simple_eager Div + | Less -> + make_simple_eager Lt + | Mul -> + make_simple_eager (Mult None) + | Or -> + make_simple_eager LOr + | OrElse -> + make_short_circuit_logic ~short_circuit_when_lhs_is:true + | Rem -> + make_simple_eager Mod (* TODO: check semantics of Rem vs Mod *) + | Sub -> + make_simple_eager (MinusA None) + | todo -> + L.debug Capture Verbose + "@[todo ErlangTranslator.translate_expression(BinaryOperator) %s@." + (Sexp.to_string (Ast.sexp_of_binary_operator todo)) ; + Block.all env [block1; block2; Block.make_success env] ) | Block body -> translate_body env body | Call diff --git a/infer/tests/codetoanalyze/erlang/features/issues.exp b/infer/tests/codetoanalyze/erlang/features/issues.exp index f7d2bb189..87c599ed9 100644 --- a/infer/tests/codetoanalyze/erlang/features/issues.exp +++ b/infer/tests/codetoanalyze/erlang/features/issues.exp @@ -30,5 +30,14 @@ codetoanalyze/erlang/features/src/comparison.erl, test_not_equal_Bad2/0, 3, NO_T codetoanalyze/erlang/features/src/logic.erl, test_and00_Bad/0, 1, NO_TRUE_BRANCH_IN_IF, no_bucket, ERROR, [no true branch in if expression here] codetoanalyze/erlang/features/src/logic.erl, test_and01_Bad/0, 1, NO_TRUE_BRANCH_IN_IF, no_bucket, ERROR, [no true branch in if expression here] codetoanalyze/erlang/features/src/logic.erl, test_and10_Bad/0, 1, NO_TRUE_BRANCH_IN_IF, no_bucket, ERROR, [no true branch in if expression here] +codetoanalyze/erlang/features/src/logic.erl, test_andalso00_Bad/0, 1, NO_TRUE_BRANCH_IN_IF, no_bucket, ERROR, [no true branch in if expression here] +codetoanalyze/erlang/features/src/logic.erl, test_andalso01_Bad/0, 1, NO_TRUE_BRANCH_IN_IF, no_bucket, ERROR, [no true branch in if expression here] +codetoanalyze/erlang/features/src/logic.erl, test_andalso10_Bad/0, 1, NO_TRUE_BRANCH_IN_IF, no_bucket, ERROR, [no true branch in if expression here] codetoanalyze/erlang/features/src/logic.erl, test_or00_Bad/0, 1, NO_TRUE_BRANCH_IN_IF, no_bucket, ERROR, [no true branch in if expression here] +codetoanalyze/erlang/features/src/logic.erl, test_orelse00_Bad/0, 1, NO_TRUE_BRANCH_IN_IF, no_bucket, ERROR, [no true branch in if expression here] codetoanalyze/erlang/features/src/logic.erl, test_unot_Bad/0, 1, NO_TRUE_BRANCH_IN_IF, no_bucket, ERROR, [no true branch in if expression here] +codetoanalyze/erlang/features/src/short_circuit.erl, accepts_one/1, 0, NO_MATCHING_FUNCTION_CLAUSE, no_bucket, ERROR, [*** LATENT ***,no matching function clause here] +codetoanalyze/erlang/features/src/short_circuit.erl, test_and_Bad/0, -7, 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_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] diff --git a/infer/tests/codetoanalyze/erlang/features/src/logic.erl b/infer/tests/codetoanalyze/erlang/features/src/logic.erl index 41cec455c..a056cbdaa 100644 --- a/infer/tests/codetoanalyze/erlang/features/src/logic.erl +++ b/infer/tests/codetoanalyze/erlang/features/src/logic.erl @@ -14,10 +14,18 @@ test_and01_Bad/0, test_and10_Bad/0, test_and11_Ok/0, + test_andalso00_Bad/0, + test_andalso01_Bad/0, + test_andalso10_Bad/0, + test_andalso11_Ok/0, test_or00_Bad/0, test_or01_Ok/0, test_or10_Ok/0, test_or11_Ok/0, + test_orelse00_Bad/0, + test_orelse01_Ok/0, + test_orelse10_Ok/0, + test_orelse11_Ok/0, test_unot_Ok/0, test_unot_Bad/0 ]). @@ -42,6 +50,26 @@ test_and11_Ok() -> ?T and ?T -> ok end. +test_andalso00_Bad() -> + if + ?F andalso ?F -> ok + end. + +test_andalso01_Bad() -> + if + ?F andalso ?T -> ok + end. + +test_andalso10_Bad() -> + if + ?T andalso ?F -> ok + end. + +test_andalso11_Ok() -> + if + ?T andalso ?T -> ok + end. + test_or00_Bad() -> if ?F or ?F -> ok @@ -62,6 +90,26 @@ test_or11_Ok() -> ?T or ?T -> ok end. +test_orelse00_Bad() -> + if + ?F orelse ?F -> ok + end. + +test_orelse01_Ok() -> + if + ?F orelse ?T -> ok + end. + +test_orelse10_Ok() -> + if + ?T orelse ?F -> ok + end. + +test_orelse11_Ok() -> + if + ?T orelse ?T -> ok + end. + test_unot_Ok() -> if not ?F -> ok diff --git a/infer/tests/codetoanalyze/erlang/features/src/short_circuit.erl b/infer/tests/codetoanalyze/erlang/features/src/short_circuit.erl new file mode 100644 index 000000000..2cc69d456 --- /dev/null +++ b/infer/tests/codetoanalyze/erlang/features/src/short_circuit.erl @@ -0,0 +1,56 @@ +% 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(short_circuit). + +% Workaround until we support true/false atoms +-define(T, (1 == 1)). +-define(F, (1 == 0)). + +-export([ + test_and_Ok/0, + test_and_Bad/0, + test_andalso_Ok/0, + test_andalso_Bad/0, + test_or_Ok/0, + test_or_Bad/0, + test_orelse_Ok/0, + test_orelse_Bad/0 +]). + +accepts_one(1) -> + true. + +test_and_Ok() -> + % All fine here + ?T and accepts_one(1). + +test_and_Bad() -> + % Fails because no short circuit + ?F and accepts_one(0). + +test_andalso_Ok() -> + % Ok because short circuit + ?F andalso accepts_one(0). + +test_andalso_Bad() -> + % Fails because LHS comes first + accepts_one(0) andalso ?F. + +test_or_Ok() -> + % All fine here + ?F or accepts_one(1). + +test_or_Bad() -> + % Fails because no short circuit + ?T or accepts_one(0). + +test_orelse_Ok() -> + % Ok because short circuit + ?T orelse accepts_one(0). + +test_orelse_Bad() -> + % Fails because LHS comes first + accepts_one(0) orelse ?T.