[cleanup] remove EndBranches and terminated if_kind

Summary: Another relic of contexts, deleted earlier. We can simplify SIL again.

Reviewed By: ngorogiannis

Differential Revision:
D62031139

Privacy Context Container: L1208441

fbshipit-source-id: 55f6f3e9793e6847781df02ea23b4ab71154dac4

infer/src/IR/Sil.ml

@@ -11,29 +11,27 @@ module F = Format
 module L = Logging
 
 type if_kind =
-  | Ik_bexp of {terminated: bool}
+  | Ik_bexp
   | Ik_compexch
   | Ik_dowhile
   | Ik_for
-  | Ik_if of {terminated: bool}
+  | Ik_if
   | Ik_land_lor
   | Ik_while
   | Ik_switch
 [@@deriving compare, equal, hash, normalize]
 
 let pp_if_kind fmt = function
-  | Ik_bexp {terminated} ->
-      F.pp_print_string fmt "boolean exp" ;
-      if terminated then F.pp_print_string fmt " (terminated)"
+  | Ik_bexp ->
+      F.pp_print_string fmt "boolean exp"
   | Ik_compexch ->
       F.pp_print_string fmt "atomic compare exchange"
   | Ik_dowhile ->
       F.pp_print_string fmt "do while"
   | Ik_for ->
       F.pp_print_string fmt "for loop"
-  | Ik_if {terminated} ->
-      F.pp_print_string fmt "if" ;
-      if terminated then F.pp_print_string fmt " (terminated)"
+  | Ik_if ->
+      F.pp_print_string fmt "if"
   | Ik_land_lor ->
       F.pp_print_string fmt "obtained from && or ||"
   | Ik_while ->
@@ -42,17 +40,9 @@ let pp_if_kind fmt = function
       F.pp_print_string fmt "switch"
 
 
-let is_terminated_if_kind = function
-  | Ik_bexp {terminated} | Ik_if {terminated} ->
-      terminated
-  | Ik_compexch | Ik_dowhile | Ik_for | Ik_land_lor | Ik_while | Ik_switch ->
-      false
-
-
 type instr_metadata =
   | Abstract of Location.t
   | CatchEntry of {try_id: int; loc: Location.t}
-  | EndBranches
   | ExitScope of Var.t list * Location.t
   | Nullify of Pvar.t * Location.t
   | Skip
@@ -98,7 +88,7 @@ let location_of_instr_metadata = function
   | TryExit {loc}
   | VariableLifetimeBegins {loc} ->
       loc
-  | EndBranches | Skip ->
+  | Skip ->
       Location.dummy
 
 
@@ -110,7 +100,7 @@ let location_of_instr = function
 
 
 let exps_of_instr_metadata = function
-  | Abstract _ | CatchEntry _ | EndBranches ->
+  | Abstract _ | CatchEntry _ ->
       []
   | ExitScope (vars, _) ->
       List.map ~f:Var.to_exp vars
@@ -141,8 +131,6 @@ let pp_instr_metadata pe f = function
       F.fprintf f "APPLY_ABSTRACTION; [%a]" Location.pp loc
   | CatchEntry {loc} ->
       F.fprintf f "CATCH_ENTRY; [%a]" Location.pp loc
-  | EndBranches ->
-      F.fprintf f "END_BRANCHES"
   | ExitScope (vars, loc) ->
       F.fprintf f "EXIT_SCOPE(%a); [%a]" (Pp.seq ~sep:"," Var.pp) vars Location.pp loc
   | Nullify (pvar, loc) ->

infer/src/IR/Sil.mli

@@ -15,33 +15,22 @@ module F = Format
 
 (** Kind of prune instruction *)
 type if_kind =
-  | Ik_bexp of {terminated: bool}  (** boolean expressions, and exp ? exp : exp *)
+  | Ik_bexp  (** boolean expressions, and exp ? exp : exp *)
   | Ik_compexch  (** used in atomic compare exchange expressions *)
   | Ik_dowhile
   | Ik_for
-  | Ik_if of {terminated: bool}
+  | Ik_if
   | Ik_land_lor  (** obtained from translation of && or || *)
   | Ik_while
   | Ik_switch
 [@@deriving compare, equal]
 
 val pp_if_kind : F.formatter -> if_kind -> unit
 
-val is_terminated_if_kind : if_kind -> bool
-(** Whether an [if_kind] has a [true] [terminated] field, meaning that the conditional control flow
-    creates a temporary branching in the CFG of the procedure that is closed by a [Join] node
-    containing an [EndBranches] instruction. Frontends should try to terminate conditionals (by
-    setting the [terminated] flag and emitting an [EndBranches] instruction at the appropriate
-    point) whenever possible so some analyses can detect which instructions are executed under the
-    influence of a conditional more easily. *)
-
 type instr_metadata =
   | Abstract of Location.t
       (** a good place to apply abstraction, mostly used in the biabduction analysis *)
   | CatchEntry of {try_id: int; loc: Location.t}  (** entry of C++ catch blocks *)
-  | EndBranches
-      (** the end of a conditional control flow generated by an [if] statement whose [if_kind]
-          satisfies [is_terminated_if_kind] *)
   | ExitScope of Var.t list * Location.t  (** remove temporaries and dead program variables *)
   | Nullify of Pvar.t * Location.t  (** nullify stack variable *)
   | Skip  (** no-op *)

infer/src/backend/preanal.ml

@@ -345,9 +345,7 @@ module Liveness = struct
             (VarDomain.add (Var.of_pvar pvar) active_defs, to_nullify)
         | Store _
         | Prune _
-        | Metadata
-            (Abstract _ | CatchEntry _ | EndBranches | ExitScope _ | Skip | TryEntry _ | TryExit _)
-          ->
+        | Metadata (Abstract _ | CatchEntry _ | ExitScope _ | Skip | TryEntry _ | TryExit _) ->
             astate
         | Metadata (Nullify _) ->
             L.die InternalError

infer/src/biabduction/Paths.ml

@@ -497,25 +497,25 @@ end = struct
           | Procdesc.Node.Prune_node (is_true_branch, if_kind, _) ->
               let descr =
                 match (is_true_branch, if_kind) with
-                | true, Sil.Ik_if _ ->
+                | true, Ik_if ->
                     "Taking true branch"
-                | false, Sil.Ik_if _ ->
+                | false, Ik_if ->
                     "Taking false branch"
-                | true, (Sil.Ik_for | Sil.Ik_while | Sil.Ik_dowhile) ->
+                | true, (Ik_for | Ik_while | Ik_dowhile) ->
                     "Loop condition is true. Entering loop body"
-                | false, (Sil.Ik_for | Sil.Ik_while | Sil.Ik_dowhile) ->
+                | false, (Ik_for | Ik_while | Ik_dowhile) ->
                     "Loop condition is false. Leaving loop"
-                | true, Sil.Ik_switch ->
+                | true, Ik_switch ->
                     "Switch condition is true. Entering switch case"
-                | false, Sil.Ik_switch ->
+                | false, Ik_switch ->
                     "Switch condition is false. Skipping switch case"
-                | true, Sil.Ik_compexch ->
+                | true, Ik_compexch ->
                     "Pointer contains expected value. Writing desired to pointer"
-                | false, Sil.Ik_compexch ->
+                | false, Ik_compexch ->
                     "Pointer does not contain expected value. Writing to expected"
-                | true, (Sil.Ik_bexp _ | Sil.Ik_land_lor) ->
+                | true, (Ik_bexp | Ik_land_lor) ->
                     "Condition is true"
-                | false, (Sil.Ik_bexp _ | Sil.Ik_land_lor) ->
+                | false, (Ik_bexp | Ik_land_lor) ->
                     "Condition is false"
               in
               let node_tags = [Errlog.Condition is_true_branch] in

infer/src/biabduction/SymExec.ml

@@ -1314,8 +1314,7 @@ let rec sym_exec
   | Sil.Metadata (ExitScope (dead_vars, _)) ->
       let dead_ids = List.filter_map dead_vars ~f:Var.get_ident in
       ret_old_path [Prop.exist_quantify tenv dead_ids prop_]
-  | Sil.Metadata
-      (CatchEntry _ | EndBranches | Skip | TryEntry _ | TryExit _ | VariableLifetimeBegins _) ->
+  | Sil.Metadata (CatchEntry _ | Skip | TryEntry _ | TryExit _ | VariableLifetimeBegins _) ->
       ret_old_path [prop_]
 
 

infer/src/bufferoverrun/bufferOverrunAnalysis.ml

@@ -493,7 +493,6 @@ module TransferFunctions = struct
       | Metadata
           ( Abstract _
           | CatchEntry _
-          | EndBranches
           | Nullify _
           | Skip
           | TryEntry _

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -98,7 +98,7 @@ end
 
 let add_unreachable_code (cfg : CFG.t) (node : CFG.Node.t) instr rem_instrs (checks : Checks.t) =
   match instr with
-  | Sil.Prune (_, _, _, (Ik_land_lor | Ik_bexp _)) ->
+  | Sil.Prune (_, _, _, (Ik_land_lor | Ik_bexp)) ->
       checks
   | Sil.Prune (condition, location, true_branch, _) ->
       let unused_branch = UnusedBranch.{node; location; condition; true_branch} in

infer/src/clang/CAddImplicitDeallocImpl.ml

@@ -122,7 +122,7 @@ let dealloc_if_no_ref proc_desc (self_var, self_typ) =
     let node_kind = Procdesc.Node.Stmt_node node_name in
     Procdesc.create_node proc_desc location node_kind ref_count_instrs
   in
-  let if_kind = Sil.Ik_if {terminated= true} in
+  let if_kind = Sil.Ik_if in
   let dealloc_prune_node =
     let cond_exp = Exp.BinOp (Eq, Var count_id, Const (Cint IntLit.zero)) in
     let instr = Sil.Prune (cond_exp, location, true, if_kind) in

infer/src/clang/cScope.ml

@@ -126,8 +126,8 @@ module CXXTemporaries = struct
         (* temporaries created in branches need instrumentation markers to remember if they have
            been created or not during the evaluation of the expression *)
         visit_stmt ~bound_to_decl context cond ~marker temporaries
-        |> visit_stmt ~bound_to_decl context then_ ~marker:(Some (Sil.Ik_bexp {terminated= true}))
-        |> visit_stmt ~bound_to_decl context else_ ~marker:(Some (Sil.Ik_bexp {terminated= true}))
+        |> visit_stmt ~bound_to_decl context then_ ~marker:(Some Sil.Ik_bexp)
+        |> visit_stmt ~bound_to_decl context else_ ~marker:(Some Sil.Ik_bexp)
     | BinaryOperator (_, [lhs; rhs], _, {boi_kind= `LAnd | `LOr}) ->
         (* similarly to above, due to possible short-circuiting we are not sure that the RHS of [a
            && b] and [a || b] will be executed *)

infer/src/clang/cTrans.ml

@@ -1471,9 +1471,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
           ; Sil.Load {id= expected_id; e= expected_exp; typ; loc= sil_loc} ]
           @ desired_instrs
         in
-        let join_node =
-          Procdesc.create_node context.procdesc sil_loc Join_node [Sil.Metadata EndBranches]
-        in
+        let join_node = Procdesc.create_node context.procdesc sil_loc Join_node [] in
         Procdesc.node_set_succs context.procdesc join_node ~normal:trans_state.succ_nodes ~exn:[] ;
         let var_exp_typ =
           match trans_state.var_exp_typ with
@@ -2150,8 +2148,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
     in
     let var_typ = add_reference_if_glvalue typ expr_info in
     let join_node =
-      Procdesc.create_node trans_state.context.CContext.procdesc sil_loc Join_node
-        [Sil.Metadata EndBranches]
+      Procdesc.create_node trans_state.context.CContext.procdesc sil_loc Join_node []
     in
     Procdesc.node_set_succs context.procdesc join_node ~normal:succ_nodes ~exn:[] ;
     let var_exp_typ =
@@ -2170,7 +2167,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
         {trans_state with continuation= continuation'; succ_nodes= []; var_exp_typ= None}
       in
       exec_with_priority_exception trans_state' cond
-        (cond_trans ~if_kind:(Sil.Ik_bexp {terminated= true}) ~negate_cond:false)
+        (cond_trans ~if_kind:Sil.Ik_bexp ~negate_cond:false)
     in
     let trans_state = {trans_state with succ_nodes= [join_node]} in
     (* Note: by contruction prune nodes are leafs_nodes_cond *)
@@ -2402,9 +2399,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
       List.iter prune_nodes' ~f:(fun n ->
           Procdesc.node_set_succs context.procdesc n ~normal:nodes_branch ~exn:[] )
     in
-    let join_node =
-      Procdesc.create_node context.procdesc sil_loc Join_node [Sil.Metadata EndBranches]
-    in
+    let join_node = Procdesc.create_node context.procdesc sil_loc Join_node [] in
     Procdesc.node_set_succs context.procdesc join_node ~normal:trans_state.succ_nodes ~exn:[] ;
     let trans_state_join_succ = {trans_state with succ_nodes= [join_node]} in
     (* translate the condition expression *)
@@ -2413,7 +2408,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
       let continuation' = mk_cond_continuation trans_state.continuation in
       let trans_state'' = {trans_state with continuation= continuation'; succ_nodes= []} in
       let cond_stmt = CAst_utils.get_stmt_exn if_stmt_info.isi_cond source_range in
-      cond_trans ~if_kind:(Sil.Ik_if {terminated= true}) ~negate_cond:false trans_state'' cond_stmt
+      cond_trans ~if_kind:Sil.Ik_if ~negate_cond:false trans_state'' cond_stmt
     in
     (* translate the variable declaration inside the condition if present *)
     let res_trans_cond_var =
@@ -4549,10 +4544,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
              - [join_node] to join [dtor_trans_result] and [prune_false] and continue with the
              successor node(s) of the translation [trans_state.succ_nodes] *)
           let proc_desc = trans_state.context.procdesc in
-          let join_node =
-            Procdesc.create_node proc_desc sil_loc Join_node
-            @@ if Sil.is_terminated_if_kind if_kind then [Sil.Metadata EndBranches] else []
-          in
+          let join_node = Procdesc.create_node proc_desc sil_loc Join_node [] in
           Procdesc.node_set_succs proc_desc join_node ~normal:trans_state.succ_nodes ~exn:[] ;
           (* create dtor call as a new node connected to the join node, force new node creation by
              creating a fresh pointer and calling [force_claim_priority_node] *)

infer/src/cost/cost.ml

@@ -171,7 +171,6 @@ module InstrBasicCostWithReason = struct
     | Sil.Metadata
         ( Abstract _
         | CatchEntry _
-        | EndBranches
         | ExitScope _
         | Nullify _
         | Skip

infer/src/erlang/ErlangNode.ml

@@ -39,8 +39,8 @@ let make_if (env : (_, _) Env.t) branch expr =
     if branch then PruneNodeKind_TrueBranch else PruneNodeKind_FalseBranch
   in
   let condition : Exp.t = if branch then expr else UnOp (LNot, expr, Some (Typ.mk (Tint IBool))) in
-  let kind : Procdesc.Node.nodekind = Prune_node (branch, Ik_if {terminated= false}, prune_kind) in
-  let prune : Sil.instr = Prune (condition, env.location, branch, Ik_if {terminated= false}) in
+  let kind : Procdesc.Node.nodekind = Prune_node (branch, Ik_if, prune_kind) in
+  let prune : Sil.instr = Prune (condition, env.location, branch, Ik_if) in
   make env kind [prune]
 
 

infer/src/integration/CaptureSILJson.ml

@@ -129,10 +129,10 @@ let parse_ptr_kind (json : Safe.t) =
 
 let parse_if_kind (json : Safe.t) =
   let ifkind_map =
-    [ ("Ik_bexp", Sil.Ik_bexp {terminated= false})
+    [ ("Ik_bexp", Sil.Ik_bexp)
     ; ("Ik_dowhile", Sil.Ik_dowhile)
     ; ("Ik_for", Sil.Ik_for)
-    ; ("Ik_if", Sil.Ik_if {terminated= false})
+    ; ("Ik_if", Sil.Ik_if)
     ; ("Ik_land_lor", Sil.Ik_land_lor)
     ; ("Ik_while", Sil.Ik_while)
     ; ("Ik_switch", Sil.Ik_switch) ]

infer/src/java/jTrans.ml

@@ -1098,7 +1098,7 @@ let instruction (context : JContext.t) pc instr : translation =
         let sil_op = get_test_operator op in
         let sil_test_false = Exp.BinOp (sil_op, sil_ex1, sil_ex2) in
         let sil_test_true = Exp.UnOp (Unop.LNot, sil_test_false, None) in
-        let if_kind = Sil.Ik_if {terminated= false} in
+        let if_kind = Sil.Ik_if in
         let sil_instrs_true = Sil.Prune (sil_test_true, loc, true, if_kind) in
         let sil_instrs_false = Sil.Prune (sil_test_false, loc, false, if_kind) in
         let node_kind_true = Procdesc.Node.Prune_node (true, if_kind, PruneNodeKind_MethodBody) in

infer/src/pulse/Pulse.ml

@@ -1536,36 +1536,16 @@ module PulseTransferFunctions = struct
                 NonDisjDomain.set_captured_variables exp astate_n )
           in
           (astates, path, astate_n)
-      | Prune (condition, loc, is_then_branch, if_kind) ->
+      | Prune (condition, loc, _is_then_branch, _if_kind) ->
           let prune_result =
             let=* astate = check_config_usage analysis_data loc condition astate in
             PulseOperations.prune path loc ~condition astate
           in
-          let path =
-            match PulseOperationResult.sat_ok prune_result with
-            | None ->
-                path
-            | Some (_, hist) ->
-                if Sil.is_terminated_if_kind if_kind then
-                  let hist =
-                    ValueHistory.sequence
-                      (ConditionPassed {if_kind; is_then_branch; location= loc; timestamp})
-                      hist
-                  in
-                  {path with conditions= hist :: path.conditions}
-                else path
-          in
           let results =
             let<++> astate, _ = prune_result in
             astate
           in
           (PulseReport.report_exec_results analysis_data loc results, path, astate_n)
-      | Metadata EndBranches ->
-          (* We assume that terminated conditions are well-parenthesised, hence an [EndBranches]
-             instruction terminates the most recently seen terminated conditional. The empty case
-             shouldn't happen but let's not crash by the fault of possible errors in frontends. *)
-          let path = {path with conditions= List.tl path.conditions |> Option.value ~default:[]} in
-          ([ContinueProgram astate], path, astate_n)
       | Metadata (ExitScope (vars, location)) ->
           exit_scope vars location path astate astate_n analysis_data
       | Metadata (VariableLifetimeBegins {pvar; typ; loc; is_cpp_structured_binding})

infer/src/pulse/PulseValueHistory.ml

@@ -312,9 +312,9 @@ let pp_event_no_location fmt event =
         Pvar.pp_value_non_verbose captured_as
   | ConditionPassed {if_kind; is_then_branch} ->
       ( match (is_then_branch, if_kind) with
-      | true, Ik_if _ ->
+      | true, Ik_if ->
           "taking \"then\" branch"
-      | false, Ik_if _ ->
+      | false, Ik_if ->
           "taking \"else\" branch"
       | true, (Ik_for | Ik_while | Ik_dowhile) ->
           "loop condition is true; entering loop body"
@@ -328,9 +328,9 @@ let pp_event_no_location fmt event =
           "pointer contains expected value; writing desired to pointer"
       | false, Ik_compexch ->
           "pointer does not contain expected value; writing to expected"
-      | true, (Ik_bexp _ | Ik_land_lor) ->
+      | true, (Ik_bexp | Ik_land_lor) ->
           "condition is true"
-      | false, (Ik_bexp _ | Ik_land_lor) ->
+      | false, (Ik_bexp | Ik_land_lor) ->
           "condition is false" )
       |> F.pp_print_string fmt
   | CppTemporaryCreated _ ->

infer/src/textual/TextualSil.ml

@@ -708,7 +708,7 @@ module InstrBridge = struct
     | Prune {exp; loc} ->
         let e = ExpBridge.to_sil lang decls_env procname exp in
         let loc = LocationBridge.to_sil sourcefile loc in
-        Prune (e, loc, true, Ik_if {terminated= false})
+        Prune (e, loc, true, Ik_if)
     | Let {id; exp= Call {proc; args= [Typ typ]}; loc} when ProcDecl.is_allocate_object_builtin proc
       ->
         let typ = TypBridge.to_sil lang typ in
@@ -964,7 +964,7 @@ module NodeBridge = struct
       with
       | Some branch ->
           (* This is incomplete as Textual cannot distinguish between if/loops as well as the branch condition for now.*)
-          let if_kind = Sil.Ik_if {terminated= false} in
+          let if_kind = Sil.Ik_if in
           SilProcdesc.Node.Prune_node (branch, if_kind, PruneNodeKind_MethodBody)
       | None ->
           SilProcdesc.Node.Stmt_node MethodBody