[inferpython][exec] factorial example

Summary:
Factorial is a good stress test. I fix a bug in STORE_NAME which requires
to modify global scope, not local scope. I'm also adding some arithmetic functions and
the capability to traverse non-cyclic CFGs.

Reviewed By: ngorogiannis

Differential Revision:
D64472005

Privacy Context Container: L1208441

fbshipit-source-id: 4c51f39ccae49c94599072ef9d261b49eab13698

infer/src/python/PyIRExec.ml

@@ -69,6 +69,15 @@ let expect_int ~who ?how = function
         how pp_pval v
 
 
+let expect_bool ~who ?how = function
+  | Bool b ->
+      b
+  | v ->
+      L.die InternalError "%s expects a bool%a and received %a" who
+        (Pp.option (fun fmt how -> F.fprintf fmt " as %s" how))
+        how pp_pval v
+
+
 let expect_2_args ~who = function
   | [arg1; arg2] ->
       (arg1, arg2)
@@ -206,38 +215,65 @@ let run {Module.name; toplevel; functions} =
       match (stmt : Stmt.t) with
       | Let {lhs; rhs} ->
           ssa_set lhs (eval_exp rhs)
-      | Store {lhs= {scope= Name | Fast; ident}; rhs} ->
+      | Store {lhs= {scope= Fast; ident}; rhs} ->
           locals_set ident (eval_exp rhs)
+      | Store {lhs= {scope= Name; ident}; rhs} ->
+          (* TODO: inside class body / module we will need a different behavior *)
+          globals_set ident (eval_exp rhs)
       | Store {lhs= {scope= Global; ident}; rhs} ->
           globals_set ident (eval_exp rhs)
       | Call {lhs; exp; args} ->
           let f = get_closure (eval_exp exp) in
           let args = List.map ~f:eval_exp args in
           ssa_set lhs (f args)
-      | BuiltinCall {lhs; call= BuiltinCaller.Function {qual_name}; args} ->
+      | BuiltinCall {lhs; call= Function {qual_name}; args} ->
           if not (Int.equal (List.length args) 4) then
             L.die InternalError "$BuiltinCall.Function expects 4 args and reveiced [%a]"
               (Pp.comma_seq Exp.pp) args ;
           let cfg = get_cfg qual_name in
           let eval = exec_cfg cfg in
           ssa_set lhs (Closure eval)
-      | BuiltinCall {lhs; call= BuiltinCaller.Inplace Add; args} ->
+      | BuiltinCall {lhs; call= Inplace Add; args} ->
           let who = "$BuiltinCall.Inplace.Add" in
           let arg1, arg2 = expect_2_args ~who args in
           let i1 = eval_exp arg1 |> expect_int ~who ~how:"as first argument" in
           let i2 = eval_exp arg2 |> expect_int ~who ~how:"as second argument" in
           ssa_set lhs (Int (Z.add i1 i2))
+      | BuiltinCall {lhs; call= Compare Le; args} ->
+          let who = "$BuiltinCall.Compare.Le" in
+          let arg1, arg2 = expect_2_args ~who args in
+          let i1 = eval_exp arg1 |> expect_int ~who ~how:"as first argument" in
+          let i2 = eval_exp arg2 |> expect_int ~who ~how:"as second argument" in
+          ssa_set lhs (Bool (Z.leq i1 i2))
+      | BuiltinCall {lhs; call= Binary Subtract; args} ->
+          let who = "$BuiltinCall.Binary.Subtract" in
+          let arg1, arg2 = expect_2_args ~who args in
+          let i1 = eval_exp arg1 |> expect_int ~who ~how:"as first argument" in
+          let i2 = eval_exp arg2 |> expect_int ~who ~how:"as second argument" in
+          ssa_set lhs (Int (Z.sub i1 i2))
+      | BuiltinCall {lhs; call= Binary Multiply; args} ->
+          let who = "$BuiltinCall.Binary.Subtract" in
+          let arg1, arg2 = expect_2_args ~who args in
+          let i1 = eval_exp arg1 |> expect_int ~who ~how:"as first argument" in
+          let i2 = eval_exp arg2 |> expect_int ~who ~how:"as second argument" in
+          ssa_set lhs (Int (Z.mul i1 i2))
       | SetAttr _ | StoreSubscript _ | CallMethod _ | BuiltinCall _ | SetupAnnotations ->
           todo "exec_stmt"
     in
-    let exec_terminator terminator =
+    let rec exec_terminator terminator =
       match (terminator : Terminator.t) with
       | Return exp ->
           eval_exp exp
+      | If {exp; then_; else_} ->
+          let test = eval_exp exp |> expect_bool ~who:"If terminator" in
+          if test then exec_node_call then_ else exec_node_call else_
       | _ ->
           todo "exec_terminator"
-    in
-    let exec_node {Node.ssa_parameters; stmts; last} args =
+    and exec_node_call {Terminator.label; ssa_args} =
+      let node = get_node label in
+      let args = List.map ~f:eval_exp ssa_args in
+      exec_node node args
+    and exec_node {Node.ssa_parameters; stmts; last} args =
       List.iter2_exn ssa_parameters args ~f:(fun ssa v -> ssa_set ssa v) ;
       List.iter stmts ~f:(fun (_loc, stmt) -> exec_stmt stmt) ;
       exec_terminator last

infer/src/python/unit/PyExecTest.ml

@@ -151,3 +151,57 @@ print('n =', n)
 
     Running interpreter:
     n = 5 |}]
+
+
+let%expect_test _ =
+  let source =
+    {|
+def fact(n):
+    if n<=0:
+        return 1
+    else:
+        return n * fact(n-1)
+
+print('fact(5) =', fact(5))
+|}
+  in
+  PyIR.test source ;
+  F.printf "Running interpreter:@\n" ;
+  PyIR.test ~run:PyIRExec.run source ;
+  [%expect
+    {|
+    module dummy:
+
+      function toplevel():
+        b0:
+          n0 <- $MakeFunction["fact", "dummy.fact"](None, None, None, None, None)
+          TOPLEVEL[fact] <- n0
+          n1 <- TOPLEVEL[print]
+          n2 <- TOPLEVEL[fact]
+          n3 <- $Call(n2, 5, None)
+          n4 <- $Call(n1, "fact(5) =", n3, None)
+          return None
+
+
+      function dummy.fact(n):
+        b0:
+          n0 <- LOCAL[n]
+          n1 <- $Compare.le(n0, 0, None)
+          if n1 then jmp b1 else jmp b2
+
+        b1:
+          return 1
+
+        b2:
+          n2 <- LOCAL[n]
+          n3 <- GLOBAL[fact]
+          n4 <- LOCAL[n]
+          n5 <- $Binary.Subtract(n4, 1, None)
+          n6 <- $Call(n3, n5, None)
+          n7 <- $Binary.Multiply(n2, n6, None)
+          return n7
+
+
+
+    Running interpreter:
+    fact(5) = 120 |}]

infer/tests/codetoanalyze/python/exec/main_test.py

@@ -27,3 +27,13 @@ def no_effect(k):
 no_effect(-1)
 print('n =', n)
 #stdout: n = 5
+
+# recursive function
+def fact(n):
+    if n<=0:
+        return 1
+    else:
+        return n * fact(n-1)
+
+print('fact(5) =', fact(5))
+#stdout: fact(5) = 120