address-taken analysis and tests

Reviewed By: jeremydubreil

Differential Revision: D3066722

fb-gh-sync-id: 0239cc7
shipit-source-id: 0239cc7

infer/src/checkers/abstractDomain.ml

@@ -53,3 +53,17 @@ module BottomLiftedAbstractDomain (A : AbstractDomain) : AbstractDomain = struct
     | NonBottom astate -> A.pp fmt astate
 
 end
+
+(* lift a set to a domain. the elements of the set should be drawn from a *finite* collection of
+   possible values, since the widening operator here is just union. *)
+module FiniteSetDomain (S : PrettyPrintable.PPSet) = struct
+  include S
+  type astate = t
+
+  let initial = empty
+  let is_bottom _ = false
+  let (<=) ~lhs ~rhs = subset lhs rhs
+  let join = union
+  let widen ~prev ~next ~num_iters:_ = union prev next
+
+end

infer/src/checkers/addressTaken.ml

@@ -0,0 +1,50 @@
+(*
+ * 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 PvarSet = PrettyPrintable.MakePPSet(struct
+    type t = Sil.pvar
+    let compare = Sil.pvar_compare
+    let pp_element = (Sil.pp_pvar pe_text)
+  end)
+
+module Domain = AbstractDomain.FiniteSetDomain(PvarSet)
+
+module TransferFunctions = struct
+  type astate = Domain.astate
+
+  let rec add_address_taken_pvars exp astate = match exp with
+    | Sil.Lvar pvar ->
+        Domain.add pvar astate
+    | Sil.Cast (_, e) | UnOp (_, e, _) | Lfield (e, _, _) ->
+        add_address_taken_pvars e astate
+    | Sil.BinOp (_, e1, e2) | Lindex (e1, e2) ->
+        add_address_taken_pvars e1 astate
+        |> add_address_taken_pvars e2
+    | Sil.Const (Cclosure _ | Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cattribute _ | Cexn _ | Cclass _
+                | Cptr_to_fld _)
+    | Var _ | Sizeof _ ->
+        astate
+
+  let exec_instr astate = function
+    | Sil.Set (_, Tptr _, rhs_exp, _) ->
+        add_address_taken_pvars rhs_exp astate
+    | Sil.Call (_, _, actuals, _, _) ->
+        let add_actual_by_ref astate_acc = function
+          | actual_exp, Sil.Tptr _ -> add_address_taken_pvars actual_exp astate_acc
+          | _ -> astate_acc in
+        IList.fold_left add_actual_by_ref astate actuals
+    | Sil.Set _ | Letderef _ | Prune _ | Nullify _ | Abstract _ | Remove_temps _ | Stackop _
+    | Declare_locals _ | Goto_node _ ->
+        astate
+
+end
+
+module Analyzer =
+  AbstractInterpreter.Make
+    (ProcCfg.Forward) (Scheduler.ReversePostorder) (Domain) (TransferFunctions)

infer/src/unit/addressTakenTests.ml

@@ -0,0 +1,101 @@
+(*
+ * 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.Forward)
+    (Scheduler.ReversePostorder)
+    (AddressTaken.Domain)
+    (AddressTaken.TransferFunctions)
+
+let tests =
+  let open OUnit2 in
+  let open AnalyzerTester.StructuredSil in
+  let assert_empty = invariant "{  }" in
+  let int_typ = Sil.Tint IInt in
+  let int_ptr_typ = Sil.Tptr (int_typ, Pk_pointer) in
+  let fun_ptr_typ = Sil.Tptr (Tfun false, Pk_pointer) in
+  let closure_exp captured_pvars =
+    let mk_captured_var str = (ident_of_str str, pvar_of_str str, int_ptr_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 test_list = [
+    "address_taken_set_instr",
+    [
+      var_assign_var ~rhs_typ:int_ptr_typ "a" "b";
+      invariant "{ &b }"
+    ];
+    "address_not_taken_set_instr",
+    [
+      var_assign_var ~rhs_typ:int_typ "a" "b";
+      assert_empty
+    ];
+    "address_not_taken_letderef_instr1",
+    [
+      id_assign_var ~rhs_typ:int_ptr_typ "a" "b";
+      assert_empty
+    ];
+    "address_not_taken_letderef_instr2",
+    [
+      id_assign_var ~rhs_typ:int_typ "a" "b";
+      assert_empty
+    ];
+    "take_multiple_addresses",
+    [
+      var_assign_var ~rhs_typ:int_ptr_typ "a" "b";
+      invariant "{ &b }";
+      var_assign_var ~rhs_typ:int_ptr_typ "c" "d";
+      invariant "{ &b, &d }";
+      var_assign_var ~rhs_typ:int_typ "e" "f";
+      invariant "{ &b, &d }"
+    ];
+    "address_not_taken_closure",
+    [
+      var_assign_var ~rhs_typ:int_ptr_typ "a" "b";
+      var_assign_exp ~rhs_typ:fun_ptr_typ "c" (closure_exp ["d"; "e"]);
+      invariant "{ &b }"
+    ];
+    "if_conservative1",
+    [
+      If (unknown_exp,
+          [var_assign_var ~rhs_typ:int_ptr_typ "a" "b"],
+          []
+         );
+      invariant "{ &b }"
+    ];
+    "if_conservative2",
+    [
+      If (unknown_exp,
+          [var_assign_var ~rhs_typ:int_ptr_typ "a" "b"],
+          [var_assign_var ~rhs_typ:int_ptr_typ "c" "d"]
+         );
+      invariant "{ &b, &d }"
+    ];
+    "loop_as_if",
+    [
+      While (unknown_exp,
+             [var_assign_var ~rhs_typ:int_ptr_typ "a" "b"]
+            );
+      invariant "{ &b }"
+    ];
+    "loop_before_after",
+    [
+      var_assign_var ~rhs_typ:int_ptr_typ "a" "b";
+      invariant "{ &b }";
+      While (unknown_exp,
+             [var_assign_var ~rhs_typ:int_ptr_typ "c" "d"]
+            );
+      invariant "{ &b, &d }";
+      var_assign_var ~rhs_typ:int_ptr_typ "e" "f";
+      invariant "{ &b, &d, &f }"
+    ];
+  ] |> TestInterpreter.create_tests in
+  "address_taken_suite">:::test_list

infer/src/unit/analyzerTester.ml

@@ -63,8 +63,11 @@ module StructuredSil = struct
   let invariant inv_str =
     Invariant (inv_str, fresh_label ())
 
+  let pvar_of_str str =
+    Sil.mk_pvar (Mangled.from_string str) dummy_procname
+
   let var_of_str str =
-    Sil.Lvar (Sil.mk_pvar (Mangled.from_string str) dummy_procname)
+    Sil.Lvar (pvar_of_str str)
 
   let ident_of_str str =
     Ident.create_normal (Ident.string_to_name str) 0
@@ -72,36 +75,40 @@ module StructuredSil = struct
   let unknown_exp =
     var_of_str "__unknown__"
 
-  let make_letderef lhs_id rhs_exp =
+  let make_letderef ~rhs_typ lhs_id rhs_exp =
-    Cmd (Sil.Letderef (lhs_id, rhs_exp, dummy_typ, dummy_loc))
+    Cmd (Sil.Letderef (lhs_id, rhs_exp, rhs_typ, dummy_loc))
 
-  let make_set ~lhs_exp ~rhs_exp =
+  let make_set ~rhs_typ ~lhs_exp ~rhs_exp =
-    Cmd (Sil.Set (lhs_exp, dummy_typ, rhs_exp, dummy_loc))
+    Cmd (Sil.Set (lhs_exp, rhs_typ, rhs_exp, dummy_loc))
 
-  let id_assign_id lhs rhs =
+  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 lhs_id rhs_exp
+    make_letderef ~rhs_typ lhs_id rhs_exp
 
-  let id_assign_var lhs rhs =
+  let id_assign_var ?(rhs_typ=dummy_typ) lhs rhs =
     let lhs_id = ident_of_str lhs in
     let rhs_exp = var_of_str rhs in
-    make_letderef lhs_id rhs_exp
+    make_letderef ~rhs_typ lhs_id rhs_exp
 
-  let var_assign_int lhs rhs =
+  let var_assign_exp ~rhs_typ lhs rhs_exp =
     let lhs_exp = var_of_str lhs in
+    make_set ~rhs_typ ~lhs_exp ~rhs_exp
+
+  let var_assign_int lhs rhs =
     let rhs_exp = Sil.exp_int (Sil.Int.of_int rhs) in
-    make_set ~lhs_exp ~rhs_exp
+    let rhs_typ = Sil.Tint Sil.IInt in
+    var_assign_exp ~rhs_typ lhs rhs_exp
 
-  let var_assign_id lhs rhs =
+  let var_assign_id ?(rhs_typ=dummy_typ) lhs rhs =
     let lhs_exp = var_of_str lhs in
     let rhs_exp = Sil.Var (ident_of_str rhs) in
-    make_set ~lhs_exp ~rhs_exp
+    make_set ~rhs_typ ~lhs_exp ~rhs_exp
 
-  let var_assign_var lhs rhs =
+  let var_assign_var ?(rhs_typ=dummy_typ) lhs rhs =
     let lhs_exp = var_of_str lhs in
     let rhs_exp = var_of_str rhs in
-    make_set ~lhs_exp ~rhs_exp
+    make_set ~rhs_typ ~lhs_exp ~rhs_exp
 
 end
 

infer/src/unit/inferunit.ml

@@ -12,9 +12,10 @@
 let () =
   let open OUnit2 in
   let tests = [
-    SchedulerTests.tests;
     AbstractInterpreterTests.tests;
+    AddressTakenTests.tests;
     CopyPropagationTests.tests;
+    SchedulerTests.tests;
   ] in
   let test_suite = "all" >::: tests in
   OUnit2.run_test_tt_main test_suite