[inferpython] raise error if ill-formed Python code object detected

Summary:
The symbolic execution of the operand stack assume each there
exist a static fixed size for each node. Some tests show it is not always the
case with Python 3.8. We just throw an explicit error and delay the resolution to Python 3.10.

Reviewed By: thizanne

Differential Revision:
D64832950

Privacy Context Container: L1208441

fbshipit-source-id: 07dd52f5014ee9b31f07e081785119d3b59d6853

infer/src/python/PyIR.ml

@@ -533,6 +533,7 @@ module Error = struct
     | LoadMethodExpected of Exp.opstack_symbol
     | CompareOp of int
     | CodeWithoutQualifiedName of FFI.Code.t
+    | IllFormedOpstack of int
     | UnpackSequence of int
     | UnexpectedExpression of Exp.opstack_symbol
     | FixpointComputationHeaderReachedTwice of int
@@ -558,6 +559,9 @@ module Error = struct
     | CodeWithoutQualifiedName {FFI.Code.co_name; co_firstlineno; co_filename} ->
         F.fprintf fmt "Unknown code object: %s, at line %d, in %s" co_name co_firstlineno
           co_filename
+    | IllFormedOpstack offset ->
+        F.fprintf fmt "bad operand stack: offset %d is reachable with two stacks of different sizes"
+          offset
     | UnpackSequence n ->
         F.fprintf fmt "UNPACK_SEQUENCE: invalid count %d" n
     | UnexpectedExpression exp ->
@@ -2508,9 +2512,15 @@ let build_cfg ~debug ~code_qual_name code =
     in
     let* st = process_node st code ~offset ~arity info in
     let arity = State.size st in
-    let arity_map =
-      List.fold successors ~init:arity_map ~f:(fun arity_map (succ, delta, _) ->
-          if IMap.mem succ arity_map then arity_map else IMap.add succ (arity + delta) arity_map )
+    let* arity_map =
+      List.fold_result successors ~init:arity_map ~f:(fun arity_map (succ, delta, _) ->
+          let succ_arity = arity + delta in
+          if IMap.mem succ arity_map then
+            let current_succ_arity = IMap.find succ arity_map in
+            if not (Int.equal current_succ_arity succ_arity) then
+              internal_error st (Error.IllFormedOpstack succ)
+            else Ok arity_map
+          else Ok (IMap.add succ succ_arity arity_map) )
     in
     Ok (st, arity_map)
   in

infer/src/python/unit/PyIRTestException.ml

@@ -830,8 +830,8 @@ def foo():
 |}
   in
   PyIR.test source ;
-  [%expect {|
-    IR error: Cannot pop, stack is empty |}]
+  [%expect
+    {| IR error: bad operand stack: offset 92 is reachable with two stacks of different sizes |}]
 
 
 let%expect_test _ =

infer/src/python/unit/PyIRTestLoop.ml

@@ -317,47 +317,4 @@ def main():
   PyIR.test source ;
   [%expect
     {|
-      module dummy:
-
-        function toplevel():
-          b0:
-            n0 <- $MakeFunction["main", "dummy.main", None, None, None, None]
-            TOPLEVEL[main] <- n0
-            return None
-
-
-        function dummy.main(i):
-          b0:
-            n0 <- GLOBAL[test]
-            n1 <- $Call(n0, None)
-            if n1 then jmp b1 else jmp b6
-
-          b1:
-            n2 <- GLOBAL[r]
-            n3 <- $Call(n2, None)
-            n4 <- $GetIter(n3, None)
-            jmp b2
-
-          b2:
-            n5 <- $NextIter(n4, None)
-            n6 <- $HasNextIter(n4, None)
-            if n6 then jmp b3 else jmp b4
-
-          b3:
-            LOCAL[i] <- n5
-            n11 <- GLOBAL[action]
-            n12 <- $Call(n11, None)
-            jmp b2
-
-          b4:
-            n7 <- GLOBAL[test]
-            n8 <- $Call(n7, None)
-            if n8 then jmp b5 else jmp b6(n4, n5)
-
-          b5:
-            n9 <- GLOBAL[action]
-            n10 <- $Call(n9, None)
-            jmp b4
-
-          b6:
-            return None |}]
+    IR error: bad operand stack: offset 38 is reachable with two stacks of different sizes |}]