From dec843f5f53ced7a41bd3331de7be3c89a795b99 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Thu, 17 Mar 2016 10:31:23 -0700 Subject: [PATCH] copy-propagation analysis + tests Reviewed By: cristianoc Differential Revision: D3014280 fb-gh-sync-id: ce60320 shipit-source-id: ce60320 --- infer/src/backend/prettyPrintable.mli | 7 +- infer/src/checkers/copyPropagation.ml | 144 ++++++++++++++++++++ infer/src/checkers/registerCheckers.ml | 1 + infer/src/unit/analyzerTester.ml | 34 +++++ infer/src/unit/copyPropagationTests.ml | 181 +++++++++++++++++++++++++ infer/src/unit/inferunit.ml | 1 + 6 files changed, 365 insertions(+), 3 deletions(-) create mode 100644 infer/src/checkers/copyPropagation.ml create mode 100644 infer/src/unit/copyPropagationTests.ml diff --git a/infer/src/backend/prettyPrintable.mli b/infer/src/backend/prettyPrintable.mli index d404c7d67..f33cdea2c 100644 --- a/infer/src/backend/prettyPrintable.mli +++ b/infer/src/backend/prettyPrintable.mli @@ -36,12 +36,13 @@ module type PPMap = sig end module MakePPSet : functor (Ord : SetOrderedType) -> sig - include Set.S + include Set.S with type elt = Ord.t val pp_element : F.formatter -> Ord.t -> unit val pp : F.formatter -> t -> unit end module MakePPMap : functor (Ord : MapOrderedType) -> sig - include Map.S - val pp :pp_value:(F.formatter -> 'a -> unit) -> F.formatter -> 'a t -> unit + include Map.S with type key = Ord.t + val pp_key : F.formatter -> Ord.t -> unit + val pp : pp_value:(F.formatter -> 'a -> unit) -> F.formatter -> 'a t -> unit end diff --git a/infer/src/checkers/copyPropagation.ml b/infer/src/checkers/copyPropagation.ml new file mode 100644 index 000000000..06168a18c --- /dev/null +++ b/infer/src/checkers/copyPropagation.ml @@ -0,0 +1,144 @@ +(* + * 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 + +type var = + | ProgramVar of Sil.pvar + | LogicalVar of Ident.t + +let var_compare v1 v2 = match v1, v2 with + | ProgramVar pv1, ProgramVar pv2 -> Sil.pvar_compare pv1 pv2 + | LogicalVar sv1, LogicalVar sv2 -> Ident.compare sv1 sv2 + | ProgramVar _, _ -> 1 + | LogicalVar _, _ -> -1 + +let var_equal v1 v2 = + var_compare v1 v2 = 0 + +let pp_var fmt = function + | ProgramVar pv -> (Sil.pp_pvar pe_text) fmt pv + | LogicalVar id -> (Ident.pp pe_text) fmt id + +module Domain = struct + module VarMap = PrettyPrintable.MakePPMap(struct + type t = var + let compare = var_compare + let pp_key = pp_var + end) + + type astate = var VarMap.t + + let initial = VarMap.empty + + let is_bottom _ = false + + (* return true if the key-value bindings in [rhs] are a subset of the key-value bindings in + [lhs] *) + let (<=) ~lhs ~rhs = + VarMap.for_all + (fun k v -> + try var_equal v (VarMap.find k lhs) + with Not_found -> false) + rhs + + let join astate1 astate2 = + let keep_if_same _ v1_opt v2_opt = match v1_opt, v2_opt with + | Some v1, Some v2 -> + if var_equal v1 v2 then Some v1 else None + | _ -> None in + VarMap.merge keep_if_same astate1 astate2 + + let widen ~prev ~next ~num_iters:_= + join prev next + + let pp fmt astate = + let pp_value = pp_var in + VarMap.pp ~pp_value fmt astate + + let gen var1 var2 astate = + (* don't add tautological copies *) + if var_equal var1 var2 + then astate + else VarMap.add var1 var2 astate + + let kill_copies_with_var var astate = + let do_kill lhs_var rhs_var astate_acc = + if var_equal var lhs_var + then astate_acc (* kill copies vith [var] on lhs *) + else + if var_equal var rhs_var + then (* delete [var] = [rhs_var] copy, but add [lhs_var] = M(rhs_var) copy*) + try VarMap.add lhs_var (VarMap.find rhs_var astate) astate_acc + with Not_found -> astate_acc + else (* copy is unaffected by killing [var]; keep it *) + VarMap.add lhs_var rhs_var astate_acc in + VarMap.fold do_kill astate VarMap.empty + + (* kill the previous binding for [lhs_var], and add a new [lhs_var] -> [rhs_var] binding *) + let kill_then_gen lhs_var rhs_var astate = + let already_has_binding lhs_var rhs_var astate = + try var_equal rhs_var (VarMap.find lhs_var astate) + with Not_found -> false in + if var_equal lhs_var rhs_var || already_has_binding lhs_var rhs_var astate + then astate (* already have this binding; no need to kill or gen *) + else + kill_copies_with_var lhs_var astate + |> gen lhs_var rhs_var +end + +module TransferFunctions = struct + + type astate = Domain.astate + + let exec_instr astate = function + | Sil.Letderef (lhs_id, Sil.Var rhs_id, _, _) -> + (* note: logical vars are SSA, don't need to worry about overwriting existing bindings *) + Domain.gen (LogicalVar lhs_id) (LogicalVar rhs_id) astate + | Sil.Letderef (lhs_id, Sil.Lvar rhs_pvar, _, _) when not (Sil.pvar_is_global rhs_pvar) -> + Domain.gen (LogicalVar lhs_id) (ProgramVar rhs_pvar) astate + | Sil.Set (Sil.Lvar lhs_pvar, _, Sil.Var rhs_id, _) when not (Sil.pvar_is_global lhs_pvar) -> + Domain.kill_then_gen (ProgramVar lhs_pvar) (LogicalVar rhs_id) astate + | Sil.Set (Sil.Lvar lhs_pvar, _, Sil.Lvar rhs_pvar, _) + when not (Sil.pvar_is_global lhs_pvar || Sil.pvar_is_global rhs_pvar) -> + Domain.kill_then_gen (ProgramVar lhs_pvar) (ProgramVar rhs_pvar) astate + | Sil.Letderef (lhs_id, _, _, _) -> + (* non-copy assignment (or assignment to global); can only kill *) + Domain.kill_copies_with_var (LogicalVar lhs_id) astate + | Sil.Set (Sil.Lvar lhs_pvar, _, _, _) -> + (* non-copy assignment (or assignment to global); can only kill *) + Domain.kill_copies_with_var (ProgramVar lhs_pvar) astate + | Sil.Call (ret_ids, _, actuals, _, _) -> + let kill_ret_ids astate_acc id = + Domain.kill_copies_with_var (LogicalVar id) astate_acc in + let kill_actuals_by_ref astate_acc = function + | (Sil.Lvar pvar, Sil.Tptr _) -> Domain.kill_copies_with_var (ProgramVar pvar) astate_acc + | _ -> astate_acc in + let astate' = IList.fold_left kill_ret_ids astate ret_ids in + if !Config.curr_language = Config.Java + then astate' (* Java doesn't have pass-by-reference *) + else IList.fold_left kill_actuals_by_ref astate' actuals + | Sil.Set (Sil.Var _, _, _, _) -> + (* this should never happen *) + assert false + | Sil.Set _ | Sil.Prune _ | Sil.Nullify _ | Sil.Abstract _ | Sil.Remove_temps _ + | Sil.Declare_locals _ | Sil.Goto_node _ | Sil.Stackop _ -> + (* none of these can assign to program vars or logical vars *) + astate +end + +module Analyzer = + AbstractInterpreter.Make + (ProcCfg.Forward) + (Scheduler.ReversePostorder) + (Domain) + (TransferFunctions) + +let checker { Callbacks.proc_desc; } = ignore(Analyzer.exec_pdesc proc_desc) diff --git a/infer/src/checkers/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml index 0c2ada52d..29ed6f33a 100644 --- a/infer/src/checkers/registerCheckers.ml +++ b/infer/src/checkers/registerCheckers.ml @@ -27,6 +27,7 @@ let active_procedure_checkers () = Checkers.callback_check_write_to_parcel, false; Checkers.callback_find_deserialization, false; CheckTraceCallSequence.callback_check_trace_call_sequence, false; + CopyPropagation.checker, true; Dataflow.callback_test_dataflow, false; FragmentRetainsViewChecker.callback_fragment_retains_view, checkers_enabled; SqlChecker.callback_sql, false; diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index 13cf8bbf8..0a7595b7b 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -66,9 +66,43 @@ module StructuredSil = struct let var_of_str str = Sil.Lvar (Sil.mk_pvar (Mangled.from_string str) dummy_procname) + let ident_of_str str = + Ident.create_normal (Ident.string_to_name str) 0 + 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_set ~lhs_exp ~rhs_exp = + Cmd (Sil.Set (lhs_exp, dummy_typ, rhs_exp, dummy_loc)) + + let id_assign_id 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 + + let id_assign_var lhs rhs = + let lhs_id = ident_of_str lhs in + let rhs_exp = var_of_str rhs in + make_letderef lhs_id rhs_exp + + let var_assign_int lhs rhs = + let lhs_exp = var_of_str lhs in + let rhs_exp = Sil.exp_int (Sil.Int.of_int rhs) in + make_set ~lhs_exp ~rhs_exp + + let var_assign_id 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 + + let var_assign_var lhs rhs = + let lhs_exp = var_of_str lhs in + let rhs_exp = var_of_str rhs in + make_set ~lhs_exp ~rhs_exp + end module Make diff --git a/infer/src/unit/copyPropagationTests.ml b/infer/src/unit/copyPropagationTests.ml new file mode 100644 index 000000000..ca4931359 --- /dev/null +++ b/infer/src/unit/copyPropagationTests.ml @@ -0,0 +1,181 @@ +(* + * Copyright (c) 2015 - 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) + (CopyPropagation.Domain) + (CopyPropagation.TransferFunctions) + +let tests = + let open OUnit2 in + let open AnalyzerTester.StructuredSil in + let assert_empty = invariant "{ }" in + let test_list = [ + "var_tautology", + [ + var_assign_var "a" "a"; + assert_empty + ]; + "id_tautology", + [ + id_assign_id "a" "a"; + assert_empty + ]; + "id_assign_id_gen", + [ + id_assign_id "b" "a"; + invariant "{ b$0 -> a$0 }" + ]; + "id_assign_var_gen", + [ + id_assign_var "b" "a"; + invariant "{ b$0 -> &a }" + ]; + "var_assign_var_gen", + [ + var_assign_var "b" "a"; + invariant "{ &b -> &a }" + ]; + "var_assign_id_gen", + [ + var_assign_id "b" "a"; + invariant "{ &b -> a$0 }" + ]; + "multi_command_gen", + [ + var_assign_var "b" "a"; + var_assign_var "c" "b"; + var_assign_var "d" "c"; + invariant "{ &b -> &a, &c -> &b, &d -> &c }" + ]; + "simple_kill", + [ + var_assign_var "b" "a"; + invariant "{ &b -> &a }"; + var_assign_int "a" 1; + assert_empty + ]; + "kill_then_gen", + [ + var_assign_var "b" "a"; + invariant "{ &b -> &a }"; + var_assign_var "a" "b"; + invariant "{ &a -> &b }" + ]; + "harder_kill", + [ + var_assign_var "b" "a"; + var_assign_var "c" "b"; + var_assign_var "d" "c"; + invariant "{ &b -> &a, &c -> &b, &d -> &c }"; + var_assign_int "b" 1; + invariant "{ &c -> &a, &d -> &c }"; + var_assign_int "c" 1; + invariant "{ &d -> &a }" + ]; + "same_copy", + [ + var_assign_var "b" "a"; + var_assign_var "c" "b"; + invariant "{ &b -> &a, &c -> &b }"; + var_assign_var "c" "b"; + invariant "{ &b -> &a, &c -> &b }" + ]; + "no_cycles", + [ + var_assign_var "a" "b"; + invariant "{ &a -> &b }"; + var_assign_var "b" "a"; + invariant "{ &b -> &a }"; + var_assign_var "a" "a"; + invariant "{ &b -> &a }" + ]; + "conservative_if", + [ + var_assign_var "b" "a"; + If (unknown_exp, + [invariant "{ &b -> &a }"; + var_assign_var "a" "b"; + invariant "{ &a -> &b }"], + [] + ); + assert_empty + ]; + "if1", + [ + var_assign_var "b" "a"; + var_assign_var "c" "b"; + If (unknown_exp, + [invariant "{ &b -> &a, &c -> &b }"; + var_assign_var "c" "d"], + [invariant "{ &b -> &a, &c -> &b }"] + ); + invariant "{ &b -> &a }" + ]; + "if2", + [ + If (unknown_exp, + [var_assign_var "a" "b"], + [var_assign_var "a" "b"] + ); + invariant "{ &a -> &b }" + ]; + "if3", + [ + If (unknown_exp, + [var_assign_var "a" "b"], + [var_assign_var "a" "c"] + ); + assert_empty + ]; + "nested_if", + [ + var_assign_var "b" "a"; + var_assign_var "c" "b"; + If (unknown_exp, + [If (var_of_str "unknown2", + [ invariant "{ &b -> &a, &c -> &b }"; + var_assign_var "a" "b"; + invariant "{ &a -> &b, &c -> &b }"], + [] + ) + ], + [] + ); + invariant "{ &c -> &b }" + ]; + "loop_as_if", + [ + var_assign_var "b" "a"; + While (unknown_exp, + [var_assign_var "a" "b"] + ); + assert_empty + ]; + "easy_loop_invariant", + [ + var_assign_var "b" "a"; + While (unknown_exp, + [var_assign_var "c" "b"; + invariant "{ &b -> &a, &c -> &b }"] + ); + invariant "{ &b -> &a }" + ]; + "empty_loop", + [ + var_assign_var "b" "a"; + While (unknown_exp, []); + var_assign_var "c" "b"; + invariant "{ &b -> &a, &c -> &b }" + ]; + ] |> TestInterpreter.create_tests in + "copy_propagation_test_suite">:::test_list diff --git a/infer/src/unit/inferunit.ml b/infer/src/unit/inferunit.ml index 256987abc..39092b577 100644 --- a/infer/src/unit/inferunit.ml +++ b/infer/src/unit/inferunit.ml @@ -14,6 +14,7 @@ let () = let tests = [ SchedulerTests.tests; AbstractInterpreterTests.tests; + CopyPropagationTests.tests; ] in let test_suite = "all" >::: tests in OUnit2.run_test_tt_main test_suite