From a71caccc801d0cde7b2bd42001c866282542e02a Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Mon, 21 Mar 2016 20:35:04 -0700 Subject: [PATCH] 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 | 14 ++++ infer/src/checkers/addressTaken.ml | 50 +++++++++++++ infer/src/unit/addressTakenTests.ml | 101 +++++++++++++++++++++++++++ infer/src/unit/analyzerTester.ml | 37 ++++++---- infer/src/unit/inferunit.ml | 3 +- 5 files changed, 189 insertions(+), 16 deletions(-) create mode 100644 infer/src/checkers/addressTaken.ml create mode 100644 infer/src/unit/addressTakenTests.ml diff --git a/infer/src/checkers/abstractDomain.ml b/infer/src/checkers/abstractDomain.ml index 338f92aac..fc9291b7e 100644 --- a/infer/src/checkers/abstractDomain.ml +++ b/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 diff --git a/infer/src/checkers/addressTaken.ml b/infer/src/checkers/addressTaken.ml new file mode 100644 index 000000000..25a655cbc --- /dev/null +++ b/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) diff --git a/infer/src/unit/addressTakenTests.ml b/infer/src/unit/addressTakenTests.ml new file mode 100644 index 000000000..154066826 --- /dev/null +++ b/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 diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index e8d7a4e05..fc9df706b 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/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 = - Cmd (Sil.Letderef (lhs_id, rhs_exp, dummy_typ, dummy_loc)) + let make_letderef ~rhs_typ lhs_id rhs_exp = + Cmd (Sil.Letderef (lhs_id, rhs_exp, rhs_typ, dummy_loc)) - let make_set ~lhs_exp ~rhs_exp = - Cmd (Sil.Set (lhs_exp, dummy_typ, rhs_exp, dummy_loc)) + let make_set ~rhs_typ ~lhs_exp ~rhs_exp = + 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 diff --git a/infer/src/unit/inferunit.ml b/infer/src/unit/inferunit.ml index 39092b577..267bf7008 100644 --- a/infer/src/unit/inferunit.ml +++ b/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