Reviewed By: mbouaziz Differential Revision: D5576344 fbshipit-source-id: 581da42master
Sam Blackshear
8 years ago
committed by
Facebook Github Bot
parent
557faa4a46
commit
1157364a09
@ -1,110 +0,0 @@
|
|||||||
(*
|
|
||||||
* 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.
|
|
||||||
*)
|
|
||||||
|
|
||||||
open! IStd
|
|
||||||
module F = Format
|
|
||||||
module L = Logging
|
|
||||||
|
|
||||||
module Domain = struct
|
|
||||||
include Var.Map
|
|
||||||
|
|
||||||
type astate = Var.t Var.Map.t
|
|
||||||
|
|
||||||
(* return true if the key-value bindings in [rhs] are a subset of the key-value bindings in
|
|
||||||
[lhs] *)
|
|
||||||
let ( <= ) ~lhs ~rhs =
|
|
||||||
if phys_equal lhs rhs then true
|
|
||||||
else
|
|
||||||
Var.Map.for_all
|
|
||||||
(fun k v ->
|
|
||||||
try Var.equal v (Var.Map.find k lhs)
|
|
||||||
with Not_found -> false)
|
|
||||||
rhs
|
|
||||||
|
|
||||||
let join astate1 astate2 =
|
|
||||||
if phys_equal astate1 astate2 then astate1
|
|
||||||
else
|
|
||||||
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
|
|
||||||
Var.Map.merge keep_if_same astate1 astate2
|
|
||||||
|
|
||||||
let widen ~prev ~next ~num_iters:_ = join prev next
|
|
||||||
|
|
||||||
let pp fmt astate =
|
|
||||||
let pp_value = Var.pp in
|
|
||||||
Var.Map.pp ~pp_value fmt astate
|
|
||||||
|
|
||||||
let gen var1 var2 astate =
|
|
||||||
(* don't add tautological copies *)
|
|
||||||
if Var.equal var1 var2 then astate else Var.Map.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 Var.Map.add lhs_var (Var.Map.find rhs_var astate) astate_acc
|
|
||||||
with Not_found -> astate_acc
|
|
||||||
else (* copy is unaffected by killing [var]; keep it *)
|
|
||||||
Var.Map.add lhs_var rhs_var astate_acc
|
|
||||||
in
|
|
||||||
Var.Map.fold do_kill astate Var.Map.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 (Var.Map.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 (CFG : ProcCfg.S) = struct
|
|
||||||
module CFG = CFG
|
|
||||||
module Domain = Domain
|
|
||||||
|
|
||||||
type extras = ProcData.no_extras
|
|
||||||
|
|
||||||
let exec_instr astate _ _ = function
|
|
||||||
| Sil.Load (lhs_id, Exp.Lvar rhs_pvar, _, _) when not (Pvar.is_global rhs_pvar)
|
|
||||||
-> Domain.gen (Var.of_id lhs_id) (Var.of_pvar rhs_pvar) astate
|
|
||||||
| Sil.Store (Exp.Lvar lhs_pvar, _, Exp.Var rhs_id, _) when not (Pvar.is_global lhs_pvar)
|
|
||||||
-> Domain.kill_then_gen (Var.of_pvar lhs_pvar) (Var.of_id rhs_id) astate
|
|
||||||
| Sil.Store (Exp.Lvar lhs_pvar, _, _, _)
|
|
||||||
-> (* non-copy assignment; can only kill *)
|
|
||||||
Domain.kill_copies_with_var (Var.of_pvar lhs_pvar) astate
|
|
||||||
| Sil.Load _
|
|
||||||
(* lhs = *rhs where rhs isn't a pvar (or is a global). in any case, not a copy *)
|
|
||||||
(* note: since logical vars can't be reassigned, don't need to kill bindings for lhs id *)
|
|
||||||
| Sil.Store (Var _, _, _, _)
|
|
||||||
-> (* *lhs = rhs. not a copy, and not a write to lhs *)
|
|
||||||
astate
|
|
||||||
| Sil.Call (ret_id, _, actuals, _, _)
|
|
||||||
-> let kill_ret_id (id, _) = Domain.kill_copies_with_var (Var.of_id id) astate in
|
|
||||||
let kill_actuals_by_ref astate_acc = function
|
|
||||||
| Exp.Lvar pvar, {Typ.desc= Tptr _}
|
|
||||||
-> Domain.kill_copies_with_var (Var.of_pvar pvar) astate_acc
|
|
||||||
| _
|
|
||||||
-> astate_acc
|
|
||||||
in
|
|
||||||
let astate' = Option.value_map ~f:kill_ret_id ~default:astate ret_id in
|
|
||||||
if Config.curr_language_is Config.Java then astate'
|
|
||||||
(* Java doesn't have pass-by-reference *)
|
|
||||||
else List.fold ~f:kill_actuals_by_ref ~init:astate' actuals
|
|
||||||
| Sil.Store _ | Prune _ | Nullify _ | Abstract _ | Remove_temps _ | Declare_locals _
|
|
||||||
-> (* none of these can assign to program vars or logical vars *)
|
|
||||||
astate
|
|
||||||
end
|
|
||||||
@ -1,99 +0,0 @@
|
|||||||
(*
|
|
||||||
* 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.
|
|
||||||
*)
|
|
||||||
|
|
||||||
open! IStd
|
|
||||||
module F = Format
|
|
||||||
module TestInterpreter =
|
|
||||||
AnalyzerTester.Make (ProcCfg.Exceptional) (CopyPropagation.TransferFunctions)
|
|
||||||
|
|
||||||
let tests =
|
|
||||||
let open OUnit2 in
|
|
||||||
let open AnalyzerTester.StructuredSil in
|
|
||||||
let assert_empty = invariant "{ }" in
|
|
||||||
let test_list =
|
|
||||||
[ ("id_load_id_no_gen", [id_assign_id "b" "a"; (* means b = *a *)
|
|
||||||
assert_empty])
|
|
||||||
; ("id_set_id_no_gen", [id_set_id "b" "a"; (* means *b = a *)
|
|
||||||
assert_empty])
|
|
||||||
; ( "id_set_id_no_kill"
|
|
||||||
, [ id_assign_var "b" "a"
|
|
||||||
; invariant "{ b$0 -> &a }"
|
|
||||||
; id_set_id "b" "x"
|
|
||||||
; invariant "{ b$0 -> &a }" ] )
|
|
||||||
; ("id_assign_var_gen", [id_assign_var "b" "a"; invariant "{ b$0 -> &a }"])
|
|
||||||
; ( "var_assign_addrof_var_no_gen"
|
|
||||||
, [var_assign_addrof_var "b" "a"; (* means b = &a *)
|
|
||||||
assert_empty] )
|
|
||||||
; ("var_assign_id_gen", [var_assign_id "b" "a"; invariant "{ &b -> a$0 }"])
|
|
||||||
; ( "multi_command_gen"
|
|
||||||
, [ id_assign_var "b" "a"
|
|
||||||
; var_assign_id "c" "b"
|
|
||||||
; id_assign_var "d" "c"
|
|
||||||
; invariant "{ b$0 -> &a, d$0 -> &c, &c -> b$0 }" ] )
|
|
||||||
; ( "simple_kill"
|
|
||||||
, [id_assign_var "b" "a"; invariant "{ b$0 -> &a }"; var_assign_int "a" 1; assert_empty] )
|
|
||||||
; ( "kill_then_gen"
|
|
||||||
, [ id_assign_var "b" "a"
|
|
||||||
; invariant "{ b$0 -> &a }"
|
|
||||||
; var_assign_id "a" "c"
|
|
||||||
; invariant "{ &a -> c$0 }" ] )
|
|
||||||
; ( "same_copy"
|
|
||||||
, [ var_assign_id "b" "a"
|
|
||||||
; var_assign_id "c" "d"
|
|
||||||
; invariant "{ &b -> a$0, &c -> d$0 }"
|
|
||||||
; var_assign_id "c" "d"
|
|
||||||
; invariant "{ &b -> a$0, &c -> d$0 }" ] )
|
|
||||||
; ( "conservative_if"
|
|
||||||
, [ var_assign_id "b" "a"
|
|
||||||
; If
|
|
||||||
( unknown_exp
|
|
||||||
, [invariant "{ &b -> a$0 }"; var_assign_id "b" "c"; invariant "{ &b -> c$0 }"]
|
|
||||||
, [] )
|
|
||||||
; assert_empty ] )
|
|
||||||
; ( "if1"
|
|
||||||
, [ var_assign_id "b" "a"
|
|
||||||
; var_assign_id "c" "d"
|
|
||||||
; If
|
|
||||||
( unknown_exp
|
|
||||||
, [ invariant "{ &b -> a$0, &c -> d$0 }"
|
|
||||||
; var_assign_id "c" "e"
|
|
||||||
; invariant "{ &b -> a$0, &c -> e$0 }" ]
|
|
||||||
, [invariant "{ &b -> a$0, &c -> d$0 }"] )
|
|
||||||
; invariant "{ &b -> a$0 }" ] )
|
|
||||||
; ( "if2"
|
|
||||||
, [ If (unknown_exp, [var_assign_id "a" "b"], [var_assign_id "a" "b"])
|
|
||||||
; invariant "{ &a -> b$0 }" ] )
|
|
||||||
; ("if3", [If (unknown_exp, [var_assign_id "a" "b"], [var_assign_id "a" "c"]); assert_empty])
|
|
||||||
; ( "nested_if"
|
|
||||||
, [ var_assign_id "b" "a"
|
|
||||||
; var_assign_id "c" "b"
|
|
||||||
; If
|
|
||||||
( unknown_exp
|
|
||||||
, [ If
|
|
||||||
( var_of_str "unknown2"
|
|
||||||
, [ invariant "{ &b -> a$0, &c -> b$0 }"
|
|
||||||
; var_assign_id "b" "d"
|
|
||||||
; invariant "{ &b -> d$0, &c -> b$0 }" ]
|
|
||||||
, [] ) ]
|
|
||||||
, [] )
|
|
||||||
; invariant "{ &c -> b$0 }" ] )
|
|
||||||
; ( "loop_as_if"
|
|
||||||
, [var_assign_id "b" "a"; While (unknown_exp, [var_assign_id "b" "c"]); assert_empty] )
|
|
||||||
; ( "easy_loop_invariant"
|
|
||||||
, [ var_assign_id "b" "a"
|
|
||||||
; While (unknown_exp, [var_assign_id "c" "d"; invariant "{ &b -> a$0, &c -> d$0 }"])
|
|
||||||
; invariant "{ &b -> a$0 }" ] )
|
|
||||||
; ( "empty_loop"
|
|
||||||
, [ var_assign_id "b" "a"
|
|
||||||
; While (unknown_exp, [])
|
|
||||||
; var_assign_id "c" "b"
|
|
||||||
; invariant "{ &b -> a$0, &c -> b$0 }" ] ) ]
|
|
||||||
|> TestInterpreter.create_tests ProcData.empty_extras ~initial:CopyPropagation.Domain.empty
|
|
||||||
in
|
|
||||||
"copy_propagation_test_suite" >::: test_list
|
|
||||||
Loading…
Reference in new issue