[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

@@ -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 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
-        let op_block =
         match op with
         | Add ->
-              make_simple_op_block (PlusA None)
+            make_simple_eager (PlusA None)
         | And ->
-              make_simple_op_block LAnd
+            make_simple_eager LAnd
+        | AndAlso ->
+            make_short_circuit_logic ~short_circuit_when_lhs_is:false
         | AtLeast ->
-              make_simple_op_block Ge
+            make_simple_eager Ge
         | AtMost ->
-              make_simple_op_block Le
+            make_simple_eager Le
         (* TODO: proper modeling of equal vs exactly equal T95767672 *)
         | Equal | ExactlyEqual ->
-              make_simple_op_block Eq
+            make_simple_eager Eq
         (* TODO: proper modeling of not equal vs exactly not equal T95767672 *)
         | ExactlyNotEqual | NotEqual ->
-              make_simple_op_block Ne
+            make_simple_eager Ne
         | Greater ->
-              make_simple_op_block Gt
+            make_simple_eager Gt
         | IDiv ->
-              make_simple_op_block Div
+            make_simple_eager Div
         | Less ->
-              make_simple_op_block Lt
+            make_simple_eager Lt
         | Mul ->
-              make_simple_op_block (Mult None)
+            make_simple_eager (Mult None)
         | Or ->
-              make_simple_op_block LOr
+            make_simple_eager LOr
+        | OrElse ->
+            make_short_circuit_logic ~short_circuit_when_lhs_is:true
         | Rem ->
-              make_simple_op_block Mod (* TODO: check semantics of Rem vs Mod *)
+            make_simple_eager Mod (* TODO: check semantics of Rem vs Mod *)
         | Sub ->
-              make_simple_op_block (MinusA None)
+            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.make_success env
-        in
-        Block.all env [block1; block2; op_block]
+            Block.all env [block1; block2; Block.make_success env] )
     | Block body ->
         translate_body env body
     | Call

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]

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

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.