[semdiff] Python migration checker: fix conversion crashes and false positives

infer/src/integration/InferCommandImplementation.ml

@@ -426,8 +426,13 @@ let report_diff () =
 let python_file_to_textual file =
   if not (Py.is_initialized ()) then Py.initialize ~interpreter:Version.python_exe () ;
   let source = In_channel.with_file file ~f:In_channel.input_all in
+  (* Compile both sides under the same canonical filename. The filename becomes the module name,
+     which is embedded in the qualified names of nested procedures (comprehensions, generator
+     expressions, lambdas). Using the real path ("previous/f.py" vs "current/f.py") would make every
+     such nested name differ between the two sides, so any function containing a comprehension would
+     never compare equal — a pervasive false positive for the semdiff migration checks. *)
   let code =
-    match FFI.from_string ~source ~filename:file with
+    match FFI.from_string ~source ~filename:"semdiff_module.py" with
     | Ok code ->
         code
     | Error (kind, err) ->

infer/src/semdiff/Semdiff.ml

@@ -6,6 +6,7 @@
  *)
 
 open! IStd
+module F = Format
 module L = Logging
 
 let semdiff_with_eqsat ~debug ~previous_file ~current_file previous_src current_src =
@@ -78,6 +79,16 @@ let proc_fun_name (proc : Textual.ProcDesc.t) =
 
 let is_module_body name = String.is_substring name ~substring:"__module_body__"
 
+(* A procedure a codemod did not touch is trivially equivalent. Comparing the location-free
+   pretty-print is a cheap sufficient check (locations don't affect semantics) that lets us skip the
+   PEG conversion + bisimulation entirely for unchanged functions — the vast majority in a typical
+   file — avoiding their (sometimes >60s) cost. *)
+let proc_structurally_equal proc_old proc_new =
+  String.equal
+    (F.asprintf "%a" (Textual.ProcDesc.pp ~show_location:false) proc_old)
+    (F.asprintf "%a" (Textual.ProcDesc.pp ~show_location:false) proc_new)
+
+
 let semdiff_b007_textual ~debug (module_old : Textual.Module.t) (module_new : Textual.Module.t) =
   let procs_old = extract_procs module_old in
   let procs_new = extract_procs module_new in
@@ -91,12 +102,14 @@ let semdiff_b007_textual ~debug (module_old : Textual.Module.t) (module_new : Te
               if debug then L.user_error "Procedure %s not found in current file@." name ;
               true (* procedure removed — not a migration concern *)
           | Some proc_new -> (
-            match TextualPegDiff.check_b007_migration ~debug proc_old proc_new with
-            | result ->
-                result
-            | exception CongruenceClosureRewrite.Rule.FuelExhausted _ ->
-                if debug then L.user_error "Fuel exhausted for procedure %s@." name ;
-                false ) )
+              if proc_structurally_equal proc_old proc_new then true
+              else
+                match TextualPegDiff.check_b007_migration ~debug proc_old proc_new with
+                | result ->
+                    result
+                | exception CongruenceClosureRewrite.Rule.FuelExhausted _ ->
+                    if debug then L.user_error "Fuel exhausted for procedure %s@." name ;
+                    false ) )
   in
   if all_accepted then [] else [Diff.dummy_explicit]
 
@@ -114,17 +127,19 @@ let semdiff_b006_textual ~debug (module_old : Textual.Module.t) (module_new : Te
               if debug then L.user_error "Procedure %s not found in current file@." name ;
               true (* procedure removed — not a migration concern *)
           | Some proc_new -> (
-              let defaults_old = StructuredPeg.extract_defaults module_old proc_old in
-              let defaults_new = StructuredPeg.extract_defaults module_new proc_new in
-              match
-                TextualPegDiff.check_b006_migration ~debug ~defaults_old ~defaults_new proc_old
-                  proc_new
-              with
-              | result ->
-                  result
-              | exception CongruenceClosureRewrite.Rule.FuelExhausted _ ->
-                  if debug then L.user_error "Fuel exhausted for procedure %s@." name ;
-                  false ) )
+              if proc_structurally_equal proc_old proc_new then true
+              else
+                let defaults_old = StructuredPeg.extract_defaults module_old proc_old in
+                let defaults_new = StructuredPeg.extract_defaults module_new proc_new in
+                match
+                  TextualPegDiff.check_b006_migration ~debug ~defaults_old ~defaults_new proc_old
+                    proc_new
+                with
+                | result ->
+                    result
+                | exception CongruenceClosureRewrite.Rule.FuelExhausted _ ->
+                    if debug then L.user_error "Fuel exhausted for procedure %s@." name ;
+                    false ) )
   in
   if all_accepted then [] else [Diff.dummy_explicit]
 

infer/src/semdiff/StructuredIR.ml

@@ -265,13 +265,33 @@ let of_cfg nodes start =
     in
     aux 0 context
   in
+  (* Desugar Textual SSA block parameters into plain assignments at the jump site: a
+     [jmp target(arg0, ...)] reaching a block [#target(p0, ...)] is modelled as [p_i = arg_i]
+     executed on the edge. Combined with the @phi merge of idents at join points, this gives the
+     standard phi semantics without a dedicated phi node in the structured IR. *)
+  let ssa_param_bindings (nc : T.Terminator.node_call) : T.Instr.t list =
+    match T.NodeName.Map.find_opt nc.label node_map with
+    | Some tnode when not (List.is_empty tnode.ssa_parameters) -> (
+      match List.zip tnode.ssa_parameters nc.ssa_args with
+      | Ok pairs ->
+          List.map pairs ~f:(fun ((id, _typ), arg) ->
+              T.Instr.Let {id= Some id; exp= arg; loc= T.Location.Unknown} )
+      | Unequal_lengths ->
+          [] )
+    | _ ->
+        []
+  in
   let rec do_tree label ~context =
     match T.NodeName.Map.find_opt label node_map with
     | None ->
         Instrs {label; instrs= []}
     | Some node ->
         let kids = dtree_kids label in
-        let merge_kids = sort_by_rpo (List.filter kids ~f:is_merge) in
+        (* Merge children are nested as blocks with [node_within] making the list head the OUTERMOST
+           block. A forward edge between two merges goes from the smaller-rpo to the larger-rpo node
+           (e.g. the b13 -> b14 chain of `if a and b:`), so the larger-rpo merge must be the outer
+           block to stay reachable from the inner one. Hence descending rpo order. *)
+        let merge_kids = sort_by_rpo (List.filter kids ~f:is_merge) |> List.rev in
         let is_loop =
           is_loop_header label
           && not
@@ -298,8 +318,12 @@ let of_cfg nodes start =
         Return {label; exp}
     | [], Throw exp ->
         Throw {label; exp}
-    | [], Jump [{label= target; _}] ->
-        do_branch label target ~context
+    | [], Jump [nc] -> (
+      match ssa_param_bindings nc with
+      | [] ->
+          do_branch label nc.label ~context
+      | bindings ->
+          Seq (Instrs {label; instrs= bindings}, do_branch label nc.label ~context) )
     | [], If {bexp; then_; else_} ->
         If
           { label
@@ -310,8 +334,9 @@ let of_cfg nodes start =
         Seq (Instrs {label; instrs}, Return {label= fresh_label (); exp})
     | instrs, Throw exp ->
         Seq (Instrs {label; instrs}, Throw {label= fresh_label (); exp})
-    | instrs, Jump [{label= target; _}] ->
-        Seq (Instrs {label; instrs}, do_branch label target ~context)
+    | instrs, Jump [nc] ->
+        Seq
+          (Instrs {label; instrs= instrs @ ssa_param_bindings nc}, do_branch label nc.label ~context)
     | instrs, If {bexp; then_; else_} ->
         Seq
           ( Instrs {label; instrs}
@@ -324,8 +349,12 @@ let of_cfg nodes start =
         Instrs {label; instrs= node.instrs}
   and translate_branch source (term : T.Terminator.t) ~context =
     match term with
-    | Jump [{label= target; _}] ->
-        do_branch source target ~context
+    | Jump [nc] -> (
+      match ssa_param_bindings nc with
+      | [] ->
+          do_branch source nc.label ~context
+      | bindings ->
+          Seq (Instrs {label= source; instrs= bindings}, do_branch source nc.label ~context) )
     | Ret exp ->
         Return {label= fresh_label (); exp}
     | Throw exp ->

infer/src/semdiff/StructuredPeg.ml

@@ -363,7 +363,22 @@ let merge_envs (env : Env.t) ~cond ~(env_then : Env.t) ~(env_else : Env.t) =
             None )
       env_then.locals env_else.locals
   in
-  {env with Env.state; locals}
+  (* SSA idents (incl. desugared block parameters) bound differently on each branch reconverge as a
+     @phi, exactly like named locals. Without this the join would drop one branch's binding and a
+     use after the merge would fail with "unknown ident". *)
+  let ident_map =
+    T.Ident.Map.merge
+      (fun _id a b ->
+        match (a, b) with
+        | Some x, Some y ->
+            if CC.is_equiv cc x y then Some x else Some (mk_term cc "@phi" [cond; x; y])
+        | (Some _ as x), None | None, (Some _ as x) ->
+            x
+        | None, None ->
+            None )
+      env_then.ident_map env_else.ident_map
+  in
+  {env with Env.state; locals; ident_map}
 
 
 (* ---------- StructuredIR → PEG conversion ---------- *)

infer/src/semdiff/TextualPegDiff.ml

@@ -45,6 +45,23 @@ let dict_rules =
      ($builtins.py_has_next_iter ?S1 ($builtins.py_get_iter ?S2 (@dict_keys ?S3 ?D)))" ]
 
 
+(* has_next over items()/keys()/values() (resp. enumerate L / L) all agree because the lengths agree.
+   Canonicalising them to a single form lets the OUTER loop's has_next bridge in nested-loop bodies,
+   where it sits under matching get_iter/has_next wrappers and is never reached by the directional
+   accept rules. These are applied ONLY as rewrites for the migration check (length is direction-
+   independent); the VALUE projection stays directional via the accept rules, so a reverse migration
+   — whose value access does not match an accept rule — is still rejected. Canonicalising to a SINGLE
+   target (keys) is essential: two targets would leave keys()/values() e-nodes in one class and the
+   structural bisimulation could pick different ones per side and wrongly diverge. *)
+let b007_has_next_bridges =
+  [ "($builtins.py_has_next_iter ?S1 ($builtins.py_get_iter ?S2 (@enumerate ?L))) ==> \
+     ($builtins.py_has_next_iter ?S1 ($builtins.py_get_iter ?S2 ?L))"
+  ; "($builtins.py_has_next_iter ?S1 ($builtins.py_get_iter ?S2 (@dict_items ?S3 ?D))) ==> \
+     ($builtins.py_has_next_iter ?S1 ($builtins.py_get_iter ?S2 (@dict_keys ?S3 ?D)))"
+  ; "($builtins.py_has_next_iter ?S1 ($builtins.py_get_iter ?S2 (@dict_values ?S3 ?D))) ==> \
+     ($builtins.py_has_next_iter ?S1 ($builtins.py_get_iter ?S2 (@dict_keys ?S3 ?D)))" ]
+
+
 (* B006 (mutable default argument) rewrite rules. Parameters with a default are modelled as
    @phi(@is_default(p), <default>, @arg(p)) (see StructuredPeg). These rules normalise the codemod's
    "if p is None: p = <literal>" guard against that model so the migrated and original functions
@@ -80,6 +97,12 @@ let gen_rules cc ~theta_count : Rewrite.Rule.t list =
   parse_rules cc (("(@phi ?C ?X ?X) ==> ?X" :: theta_rules) @ enumerate_rules @ dict_rules)
 
 
+(* Rules for the directional B007 migration check: structural simplification plus the has_next
+   length-bridges only. The value projection stays handled by the (directional) accept rules. *)
+let gen_b007_rules cc ~theta_count : Rewrite.Rule.t list =
+  gen_structural_rules cc ~theta_count @ parse_rules cc b007_has_next_bridges
+
+
 (* Bisimulation: coinductive equivalence check for cyclic PEG terms (@theta).
    Uses a separate union-find (does not modify the CC) to track assumed equivalences. *)
 module BisimUF = struct
@@ -288,8 +311,10 @@ let check_b007_migration ?(debug = false) (proc_old : Textual.ProcDesc.t)
   with
   | Ok (atom_old, eqs_old, loops_old), Ok (atom_new, eqs_new, loops_new)
     when Int.equal loops_old loops_new ->
-      (* Only structural simplification rules — no B007-specific bidirectional rewrites *)
-      let rules = gen_structural_rules cc ~theta_count:loops_old in
+      (* Structural simplification plus the has_next length-bridges (see [gen_b007_rules]). The
+         has_next bridges as rewrites handle the outer loop of a nested body, which the directional
+         accept rules cannot reach; the value projection stays directional via the accept rules. *)
+      let rules = gen_b007_rules cc ~theta_count:loops_old in
       let _rounds = Rewrite.Rule.full_rewrite cc rules in
       let theta_headers =
         List.init loops_old ~f:(fun i -> CC.mk_header cc (F.asprintf "@theta_%d" i))

infer/src/semdiff/unit/TextualToPegTest.ml

@@ -103,6 +103,98 @@ let%test_module "textual to peg" =
         |}]
 
 
+    (* Regression test for SSA block parameters: a merge block declares an SSA parameter (#b3(n4))
+       bound by the predecessors' jump arguments (jmp b3(value)) — how the Python frontend lowers a
+       conditional value (e.g. `v = a if c else b`). The jump args are desugared into per-edge
+       assignments and reconverge as a @phi at the join; before that support, n4 was never bound and
+       conversion died with "unknown ident n4". *)
+    let%expect_test "if branch with ssa block parameter (phi via jump args)" =
+      convert_and_print
+        {|
+        .source_language = "python"
+        define .args = "c" foo(globals: *PyGlobals, locals: *PyLocals) : *PyObject {
+          #b0:
+              n1 = locals
+              n2 = $builtins.py_load_fast("c", n1)
+              if $builtins.py_bool(n2) then jmp b1 else jmp b2
+
+          #b1:
+              jmp b3($builtins.py_make_string("Y"))
+
+          #b2:
+              jmp b3($builtins.py_make_string("N"))
+
+          #b3(n4: *PyObject):
+              _ = $builtins.py_store_fast("v", n1, n4)
+              ret n4
+        }
+        |} ;
+      [%expect
+        {|
+        === foo ===
+        Equations:
+        c      = @param:c  [param]
+        n1     = (@load (@lvar locals))  [let]
+        n2     = @param:c  [load_fast: locals]
+        n4     = ($builtins.py_make_string (@str Y))  [let]
+        n4     = ($builtins.py_make_string (@str N))  [let]
+        v      = (@phi
+                     ($builtins.py_bool @param:c)
+                     ($builtins.py_make_string (@str Y))
+                     ($builtins.py_make_string (@str N)))  [store_fast: locals]
+        PEG: (@ret
+                 @state0
+                 (@phi
+                     ($builtins.py_bool @param:c)
+                     ($builtins.py_make_string (@str Y))
+                     ($builtins.py_make_string (@str N))))
+        |}]
+
+
+    (* Regression test for chained merge blocks (e.g. `if a and b:`): b3 is a merge of b0/b1 and
+       itself jumps to b4, another merge (of b2/b3). The forward edge b3 -> b4 requires b4 to be the
+       OUTER block of the two, otherwise of_cfg died with "br target b4 not found in context". *)
+    let%expect_test "chained merge blocks (if a and b)" =
+      convert_and_print
+        {|
+        .source_language = "python"
+        define foo(globals: *PyGlobals, locals: *PyLocals) : *PyObject {
+          #b0:
+              n1 = locals
+              n2 = $builtins.py_make_int(0)
+              if $builtins.py_bool(n2) then jmp b1 else jmp b3
+
+          #b1:
+              n3 = $builtins.py_make_int(1)
+              if $builtins.py_bool(n3) then jmp b2 else jmp b3
+
+          #b2:
+              _ = $builtins.py_store_fast("x", n1, $builtins.py_make_int(1))
+              jmp b4
+
+          #b3:
+              _ = $builtins.py_store_fast("x", n1, $builtins.py_make_int(2))
+              jmp b4
+
+          #b4:
+              n4 = $builtins.py_load_fast("x", n1)
+              ret n4
+        }
+        |} ;
+      [%expect
+        {|
+        === foo ===
+        Equations:
+        n1     = (@load (@lvar locals))  [let]
+        n2     = ($builtins.py_make_int 0)  [let]
+        n3     = ($builtins.py_make_int 1)  [let]
+        x      = ($builtins.py_make_int 1)  [store_fast: locals]
+        x      = ($builtins.py_make_int 2)  [store_fast: locals]
+        n4     = ($builtins.py_make_int 2)  [load_fast: locals]
+        PEG: (@ret @state0 ($builtins.py_make_int 2))
+        |}]
+
+
     let%expect_test "equivalence: same semantics, different ident names" =
       let text1 =
         {|

infer/tests/codetoanalyze/python/semdiff-b007/current/equal_items_to_keys_nested.py

@@ -0,0 +1,11 @@
+# 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.
+
+def f(d):
+    out = []
+    for k in d.keys():
+        for e in k:
+            out.append(e)
+    return out

infer/tests/codetoanalyze/python/semdiff-b007/current/equal_items_to_values_nested.py

@@ -0,0 +1,11 @@
+# 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.
+
+def f(d):
+    out = []
+    for v in d.values():
+        for e in v:
+            out.append(e)
+    return out

infer/tests/codetoanalyze/python/semdiff-b007/previous/equal_items_to_keys_nested.py

@@ -0,0 +1,11 @@
+# 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.
+
+def f(d):
+    out = []
+    for k, v in d.items():
+        for e in k:
+            out.append(e)
+    return out

infer/tests/codetoanalyze/python/semdiff-b007/previous/equal_items_to_values_nested.py

@@ -0,0 +1,11 @@
+# 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.
+
+def f(d):
+    out = []
+    for k, v in d.items():
+        for e in v:
+            out.append(e)
+    return out