liveness analysis and unit tests

Reviewed By: cristianoc

Differential Revision: D3080119

fb-gh-sync-id: a11a6ea
fbshipit-source-id: a11a6ea

infer/src/IR/sil.ml

@@ -3724,6 +3724,28 @@ let hpred_compact sh hpred =
 
 (** {2 Functions for constructing or destructing entities in this module} *)
 
+(** Extract the ids and pvars from an expression *)
+let exp_get_vars exp =
+  let rec exp_get_vars_ exp vars = match exp with
+    | Lvar pvar ->
+        (fst vars, pvar :: (snd vars))
+    | Var id ->
+        (id :: (fst vars), snd vars)
+    | Cast (_, e) | UnOp (_, e, _) | Lfield (e, _, _) | Const (Cexn e) ->
+        exp_get_vars_ e vars
+    | BinOp (_, e1, e2) | Lindex (e1, e2) ->
+        exp_get_vars_ e1 vars
+        |> exp_get_vars_ e2
+    | Const (Cclosure { captured_vars }) ->
+        IList.fold_left
+          (fun vars_acc (captured_exp, _, _) -> exp_get_vars_ captured_exp vars_acc)
+          vars
+          captured_vars
+    | Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cattribute _ | Cclass _ | Cptr_to_fld _)
+    | Sizeof _ ->
+        vars in
+  exp_get_vars_ exp ([], [])
+
 (** Compute the offset list of an expression *)
 let exp_get_offsets exp =
   let rec f offlist_past e = match e with

infer/src/IR/sil.mli

@@ -1247,6 +1247,9 @@ val hpred_replace_exp : (exp * exp) list -> hpred -> hpred
 
 (** {2 Functions for constructing or destructing entities in this module} *)
 
+(** Extract the ids and pvars from an expression *)
+val exp_get_vars : exp -> (Ident.t list * Pvar.t list)
+
 (** Compute the offset list of an expression *)
 val exp_get_offsets : exp -> offset list
 

infer/src/checkers/liveness.ml

@@ -0,0 +1,74 @@
+(*
+ * Copyright (c) 2016 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+module F = Format
+module L = Logging
+
+(** backward analysis for computing set of maybe-live variables at each program point *)
+
+module VarSet = PrettyPrintable.MakePPSet(struct
+    type t = CopyPropagation.var
+    let compare = CopyPropagation.var_compare
+    let pp_element = CopyPropagation.pp_var
+  end)
+
+module Domain = AbstractDomain.FiniteSetDomain(VarSet)
+
+(* compilers 101-style backward transfer functions for liveness analysis. gen a variable when it is
+   read, kill the variable when it is assigned *)
+module TransferFunctions = struct
+
+  type astate = Domain.astate
+
+  (* add all of the vars read in [exp] to the live set *)
+  let exp_add_live exp astate =
+    let (ids, pvars) = Sil.exp_get_vars exp in
+    let astate' =
+      IList.fold_left (fun astate_acc id -> Domain.add (LogicalVar id) astate_acc) astate ids in
+    IList.fold_left (fun astate_acc pvar -> Domain.add (ProgramVar pvar) astate_acc) astate' pvars
+
+  let exec_instr astate _ = function
+    | Sil.Letderef (lhs_id, rhs_exp, _, _)
+    | Sil.Set (Sil.Var lhs_id, _, rhs_exp, _) ->
+        Domain.remove (LogicalVar lhs_id) astate
+        |> exp_add_live rhs_exp
+    | Sil.Set (Lvar lhs_pvar, _, rhs_exp, _) ->
+        let astate' =
+          if Pvar.is_global lhs_pvar
+          then astate (* never kill globals *)
+          else Domain.remove (ProgramVar lhs_pvar) astate in
+        exp_add_live rhs_exp astate'
+    | Sil.Set (lhs_exp, _, rhs_exp, _) ->
+        exp_add_live lhs_exp astate
+        |> exp_add_live rhs_exp
+    | Sil.Prune (exp, _, _, _) | Sil.Goto_node (exp, _) ->
+        exp_add_live exp astate
+    | Sil.Call (ret_ids, call_exp, params, _, _) ->
+        IList.fold_right
+          (fun ret_id astate_acc -> Domain.remove (LogicalVar ret_id) astate_acc)
+          ret_ids
+          astate
+        |> exp_add_live call_exp
+        |> IList.fold_right exp_add_live (IList.map fst params)
+    | Sil.Declare_locals _ | Stackop _ ->
+        astate
+    | Sil.Nullify _ | Remove_temps _ | Abstract _ ->
+        failwith
+          "Nullify, Remove_temps, and Abstract instructions should be added after running liveness"
+
+end
+
+module Analyzer =
+  AbstractInterpreter.Make
+    (ProcCfg.Backward(ProcCfg.Forward))
+    (Scheduler.ReversePostorder)
+    (Domain)
+    (TransferFunctions)
+
+let checker { Callbacks.proc_desc; } = ignore(Analyzer.exec_pdesc proc_desc)

infer/src/checkers/procCfg.ml

@@ -68,7 +68,7 @@ module Forward : Wrapper with type node = Cfg.node = struct
 
 end
 
-module Backward (W : Wrapper) : Wrapper = struct
+module Backward (W : Wrapper) = struct
   include W
 
   let succs = W.preds

infer/src/unit/analyzerTester.ml

@@ -81,7 +81,11 @@ module StructuredSil = struct
   let make_set ~rhs_typ ~lhs_exp ~rhs_exp =
     Cmd (Sil.Set (lhs_exp, rhs_typ, rhs_exp, dummy_loc))
 
-  let id_assign_id  ?(rhs_typ=dummy_typ) lhs rhs =
+  let make_call ?(procname=dummy_procname) ret_ids args =
+    let call_exp = Sil.Const (Sil.Cfun procname) in
+    Cmd (Sil.Call (ret_ids, call_exp, args, dummy_loc, Sil.cf_default))
+
+  let id_assign_id ?(rhs_typ=dummy_typ) lhs rhs =
     let lhs_id = ident_of_str lhs in
     let rhs_exp = Sil.Var (ident_of_str rhs) in
     make_letderef ~rhs_typ lhs_id rhs_exp
@@ -110,6 +114,13 @@ module StructuredSil = struct
     let rhs_exp = var_of_str rhs in
     make_set ~rhs_typ ~lhs_exp ~rhs_exp
 
+  let call_unknown ret_id_strs arg_strs =
+    let args = IList.map (fun param_str -> (var_of_str param_str, dummy_typ)) arg_strs in
+    let ret_ids = IList.map ident_of_str ret_id_strs in
+    make_call ret_ids args
+
+  let call_unknown_no_ret arg_strs =
+    call_unknown [] arg_strs
 end
 
 module Make
@@ -173,10 +184,11 @@ module Make
           set_succs loop_body_end_node [loop_head_join_node];
           set_succs false_prune_node [loop_exit_node];
           loop_exit_node, assert_map'
-      | Invariant (inv_str, inv_label)  ->
-          let n_id = C.node_id last_node in
+      | Invariant (inv_str, inv_label) ->
+          let node = create_node (Cfg.Node.Stmt_node "Invariant") [] in
+          set_succs last_node [node];
           (* add the assertion to be checked after analysis converges *)
-          last_node, M.add n_id (inv_str, inv_label) assert_map
+          node, M.add (C.node_id node) (inv_str, inv_label) assert_map
     and structured_instrs_to_node last_node assert_map instrs =
       IList.fold_left
         (fun acc instr -> structured_instr_to_node acc instr) (last_node, assert_map) instrs in

infer/src/unit/inferunit.ml

@@ -15,6 +15,7 @@ let () =
     AbstractInterpreterTests.tests;
     AddressTakenTests.tests;
     CopyPropagationTests.tests;
+    LivenessTests.tests;
     SchedulerTests.tests;
   ] in
   let test_suite = "all" >::: tests in

infer/src/unit/livenessTests.ml

@@ -0,0 +1,189 @@
+(*
+ * Copyright (c) 2016 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+module F = Format
+
+module TestInterpreter = AnalyzerTester.Make
+    (ProcCfg.Backward (ProcCfg.Forward))
+    (Scheduler.ReversePostorder)
+    (Liveness.Domain)
+    (Liveness.TransferFunctions)
+
+let tests =
+  let open OUnit2 in
+  let open AnalyzerTester.StructuredSil in
+  let assert_empty = invariant "{  }" in
+  let fun_ptr_typ = Sil.Tptr (Tfun false, Pk_pointer) in
+  let closure_exp captured_pvars =
+    let mk_captured_var str = (Sil.Var (ident_of_str str), pvar_of_str str, dummy_typ) in
+    let captured_vars = IList.map mk_captured_var captured_pvars in
+    let closure = { Sil.name=dummy_procname; captured_vars; } in
+    Sil.Const (Cclosure closure) in
+  let unknown_cond =
+    (* don't want to use AnalyzerTest.unknown_exp because we'll treat it as a live var! *)
+    Sil.exp_zero in
+  let test_list = [
+    "basic_live",
+    [
+      invariant "{ &b }";
+      var_assign_var "a" "b"
+    ];
+    "basic_live_then_dead",
+    [
+      assert_empty;
+      var_assign_int "b" 1;
+      invariant "{ &b }";
+      var_assign_var "a" "b"
+    ];
+    "iterative_live",
+    [
+      invariant "{ &b, &d, &f }";
+      var_assign_var "e" "f";
+      invariant "{ &b, &d }";
+      var_assign_var "c" "d";
+      invariant "{ &b }";
+      var_assign_var "a" "b"
+    ];
+    "live_kill_live",
+    [
+      invariant "{ &b }";
+      var_assign_var "c" "b";
+      assert_empty;
+      var_assign_int "b" 1;
+      invariant "{ &b }";
+      var_assign_var "a" "b"
+    ];
+    "basic_live_letderef",
+    [
+      invariant "{ y$0 }";
+      id_assign_id "x" "y"
+    ];
+    "basic_live_then_kill_letderef",
+    [
+      invariant "{ z$0 }";
+      id_assign_id "y" "z";
+      invariant "{ y$0 }";
+      id_assign_id "x" "y"
+    ];
+    "if_exp_live",
+    [
+      assert_empty;
+      var_assign_int "x" 1;
+      invariant "{ &x }";
+      If (var_of_str "x", [], []);
+    ];
+    "while_exp_live",
+    [
+      assert_empty;
+      var_assign_int "x" 1;
+      invariant "{ &x }";
+      While (var_of_str "x", []);
+    ];
+    "call_params_live",
+    [
+      invariant "{ &a, &b, &c }";
+      call_unknown_no_ret ["a"; "b"; "c";]
+    ];
+    "dead_after_call_with_retval",
+    [
+      assert_empty;
+      call_unknown ["y"] [];
+      invariant "{ y$0 }";
+      id_assign_id "x" "y";
+    ];
+    "closure_captured_live",
+    [
+      invariant "{ b$0, c$0 }";
+      var_assign_exp ~rhs_typ:fun_ptr_typ "a" (closure_exp ["b"; "c"])
+    ];
+    "if_conservative_live1",
+    [
+      invariant "{ &b }";
+      If (unknown_cond,
+          [var_assign_var "a" "b"],
+          []
+         )
+    ];
+    "if_conservative_live2",
+    [
+      invariant "{ &b, &d }";
+      If (unknown_cond,
+          [var_assign_var "a" "b"],
+          [var_assign_var "c" "d"]
+         )
+    ];
+    "if_conservative_kill",
+    [
+      invariant "{ &b }";
+      If (unknown_cond,
+          [var_assign_int "b" 1],
+          []
+         );
+      invariant "{ &b }";
+      var_assign_var "a" "b"
+    ];
+    "if_conservative_kill_live",
+    [
+      invariant "{ &b, &d }";
+      If (unknown_cond,
+          [var_assign_int "b" 1],
+          [var_assign_var "c" "d"]
+         );
+      invariant "{ &b }";
+      var_assign_var "a" "b"
+    ];
+    "if_precise1",
+    [
+      assert_empty;
+      If (unknown_cond,
+          [var_assign_int "b" 1;
+           invariant "{ &b }";
+           var_assign_var "a" "b"],
+          [var_assign_int "d" 1;
+           invariant "{ &d }";
+           var_assign_var "c" "d"]
+         )
+    ];
+    "if_precise2",
+    [
+      assert_empty;
+      If (unknown_cond,
+          [var_assign_int "b" 2],
+          [var_assign_int "b" 1]
+         );
+      invariant "{ &b }";
+      var_assign_var "a" "b"
+    ];
+    "loop_as_if1",
+    [
+      invariant "{ &b }";
+      While (unknown_cond,
+             [var_assign_var "a" "b"]
+            )
+    ];
+    "loop_as_if2",
+    [
+      invariant "{ &b }";
+      While (unknown_cond,
+             [var_assign_int "b" 1]
+            );
+      invariant "{ &b }";
+      var_assign_var "a" "b"
+    ];
+    "loop_before_after",
+    [
+      invariant "{ &b, &d }";
+      While (unknown_cond,
+             [var_assign_var "b" "d"]
+            );
+      invariant "{ &b }";
+      var_assign_var "a" "b"
+    ];
+  ] |> TestInterpreter.create_tests in
+  "liveness_test_suite">:::test_list