pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

don't treat `x = &y` as a copy

Browse Source 
Reviewed By: jberdine

Differential Revision: D3424198

fbshipit-source-id: 5c0ef58
master
Sam Blackshear 9 years ago committed by Facebook Github Bot 3
parent b940c4dfac
commit c1b5a4b03e
5 changed files with 86 additions and 126 deletions
Show Stats Download Patch File Download Diff File

14
infer/src/checkers/copyPropagation.ml
Unescape View File

@ -89,11 +89,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
Domain.gen (Var.of_id lhs_id) (Var.of_pvar rhs_pvar) astate Domain.gen (Var.of_id lhs_id) (Var.of_pvar rhs_pvar) astate
| Sil.Set (Sil.Lvar lhs_pvar, _, Sil.Var rhs_id, _) when not (Pvar.is_global lhs_pvar) -> | Sil.Set (Sil.Lvar lhs_pvar, _, Sil.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 Domain.kill_then_gen (Var.of_pvar lhs_pvar) (Var.of_id rhs_id) astate
| Sil.Set (Sil.Lvar lhs_pvar, _, Sil.Lvar rhs_pvar, _)
when not (Pvar.is_global lhs_pvar || Pvar.is_global rhs_pvar) ->
Domain.kill_then_gen (Var.of_pvar lhs_pvar) (Var.of_pvar rhs_pvar) astate
| Sil.Set (Sil.Lvar lhs_pvar, _, _, _) -> | Sil.Set (Sil.Lvar lhs_pvar, _, _, _) ->
(* non-copy assignment (or assignment to global); can only kill *) (* non-copy assignment; can only kill *)
Domain.kill_copies_with_var (Var.of_pvar lhs_pvar) astate Domain.kill_copies_with_var (Var.of_pvar lhs_pvar) astate
| Sil.Letderef _ | Sil.Letderef _
(* lhs = *rhs where rhs isn't a pvar (or is a global). in any case, not a copy *) (* lhs = *rhs where rhs isn't a pvar (or is a global). in any case, not a copy *)
@ -116,12 +113,3 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
(* none of these can assign to program vars or logical vars *) (* none of these can assign to program vars or logical vars *)
astate astate
end end
module Analyzer =
AbstractInterpreter.Make
(ProcCfg.Exceptional)
(Scheduler.ReversePostorder)
(TransferFunctions)
let checker { Callbacks.proc_desc; tenv; } =
ignore(Analyzer.exec_pdesc (ProcData.make_default proc_desc tenv))

26
infer/src/unit/addressTakenTests.ml
Unescape View File

@ -31,12 +31,12 @@ let tests =
let test_list = [ let test_list = [
"address_taken_set_instr", "address_taken_set_instr",
[ [
var_assign_var ~rhs_typ:int_ptr_typ "a" "b"; var_assign_addrof_var ~rhs_typ:int_ptr_typ "a" "b";
invariant "{ &b }" invariant "{ &b }"
]; ];
"address_not_taken_set_instr", "address_not_taken_set_instr",
[ [
var_assign_var ~rhs_typ:int_typ "a" "b"; var_assign_addrof_var ~rhs_typ:int_typ "a" "b";
assert_empty assert_empty
]; ];
"address_not_taken_letderef_instr1", "address_not_taken_letderef_instr1",
@ -51,23 +51,23 @@ let tests =
]; ];
"take_multiple_addresses", "take_multiple_addresses",
[ [
var_assign_var ~rhs_typ:int_ptr_typ "a" "b"; var_assign_addrof_var ~rhs_typ:int_ptr_typ "a" "b";
invariant "{ &b }"; invariant "{ &b }";
var_assign_var ~rhs_typ:int_ptr_typ "c" "d"; var_assign_addrof_var ~rhs_typ:int_ptr_typ "c" "d";
invariant "{ &b, &d }"; invariant "{ &b, &d }";
var_assign_var ~rhs_typ:int_typ "e" "f"; var_assign_addrof_var ~rhs_typ:int_typ "e" "f";
invariant "{ &b, &d }" invariant "{ &b, &d }"
]; ];
"address_not_taken_closure", "address_not_taken_closure",
[ [
var_assign_var ~rhs_typ:int_ptr_typ "a" "b"; var_assign_addrof_var ~rhs_typ:int_ptr_typ "a" "b";
var_assign_exp ~rhs_typ:fun_ptr_typ "c" (closure_exp ["d"; "e"]); var_assign_exp ~rhs_typ:fun_ptr_typ "c" (closure_exp ["d"; "e"]);
invariant "{ &b }" invariant "{ &b }"
]; ];
"if_conservative1", "if_conservative1",
[ [
If (unknown_exp, If (unknown_exp,
[var_assign_var ~rhs_typ:int_ptr_typ "a" "b"], [var_assign_addrof_var ~rhs_typ:int_ptr_typ "a" "b"],
[] []
); );
invariant "{ &b }" invariant "{ &b }"
@ -75,27 +75,27 @@ let tests =
"if_conservative2", "if_conservative2",
[ [
If (unknown_exp, If (unknown_exp,
[var_assign_var ~rhs_typ:int_ptr_typ "a" "b"], [var_assign_addrof_var ~rhs_typ:int_ptr_typ "a" "b"],
[var_assign_var ~rhs_typ:int_ptr_typ "c" "d"] [var_assign_addrof_var ~rhs_typ:int_ptr_typ "c" "d"]
); );
invariant "{ &b, &d }" invariant "{ &b, &d }"
]; ];
"loop_as_if", "loop_as_if",
[ [
While (unknown_exp, While (unknown_exp,
[var_assign_var ~rhs_typ:int_ptr_typ "a" "b"] [var_assign_addrof_var ~rhs_typ:int_ptr_typ "a" "b"]
); );
invariant "{ &b }" invariant "{ &b }"
]; ];
"loop_before_after", "loop_before_after",
[ [
var_assign_var ~rhs_typ:int_ptr_typ "a" "b"; var_assign_addrof_var ~rhs_typ:int_ptr_typ "a" "b";
invariant "{ &b }"; invariant "{ &b }";
While (unknown_exp, While (unknown_exp,
[var_assign_var ~rhs_typ:int_ptr_typ "c" "d"] [var_assign_addrof_var ~rhs_typ:int_ptr_typ "c" "d"]
); );
invariant "{ &b, &d }"; invariant "{ &b, &d }";
var_assign_var ~rhs_typ:int_ptr_typ "e" "f"; var_assign_addrof_var ~rhs_typ:int_ptr_typ "e" "f";
invariant "{ &b, &d, &f }" invariant "{ &b, &d, &f }"
]; ];
] |> TestInterpreter.create_tests ProcData.empty_extras in ] |> TestInterpreter.create_tests ProcData.empty_extras in

3
infer/src/unit/analyzerTester.ml
Unescape View File

@ -123,7 +123,8 @@ module StructuredSil = struct
let rhs_exp = Sil.Var (ident_of_str rhs) in let rhs_exp = Sil.Var (ident_of_str rhs) in
make_set ~rhs_typ ~lhs_exp ~rhs_exp make_set ~rhs_typ ~lhs_exp ~rhs_exp
let var_assign_var ?(rhs_typ=dummy_typ) lhs rhs = (* x = &y *)
let var_assign_addrof_var ?(rhs_typ=dummy_typ) lhs rhs =
let lhs_exp = var_of_str lhs in let lhs_exp = var_of_str lhs in
let rhs_exp = var_of_str rhs in let rhs_exp = var_of_str rhs in
make_set ~rhs_typ ~lhs_exp ~rhs_exp make_set ~rhs_typ ~lhs_exp ~rhs_exp

129
infer/src/unit/copyPropagationTests.ml
Unescape View File

@ -21,16 +21,6 @@ let tests =
let open AnalyzerTester.StructuredSil in let open AnalyzerTester.StructuredSil in
let assert_empty = invariant "{ }" in let assert_empty = invariant "{ }" in
let test_list = [ let test_list = [
"var_tautology",
[
var_assign_var "a" "a";
assert_empty
];
"id_tautology",
[
id_assign_id "a" "a";
assert_empty
];
"id_letderef_id_no_gen", "id_letderef_id_no_gen",
[ [
id_assign_id "b" "a"; (* means b = *a *) id_assign_id "b" "a"; (* means b = *a *)
@ -41,7 +31,6 @@ let tests =
id_set_id "b" "a"; (* means *b = a *) id_set_id "b" "a"; (* means *b = a *)
assert_empty assert_empty
]; ];
"id_set_id_no_kill", "id_set_id_no_kill",
[ [
id_assign_var "b" "a"; id_assign_var "b" "a";
@ -54,10 +43,10 @@ let tests =
id_assign_var "b" "a"; id_assign_var "b" "a";
invariant "{ b$0 -> &a }" invariant "{ b$0 -> &a }"
]; ];
"var_assign_var_gen", "var_assign_addrof_var_no_gen",
[ [
var_assign_var "b" "a"; var_assign_addrof_var "b" "a"; (* means b = &a *)
invariant "{ &b -> &a }" assert_empty
]; ];
"var_assign_id_gen", "var_assign_id_gen",
[ [
@ -66,130 +55,112 @@ let tests =
]; ];
"multi_command_gen", "multi_command_gen",
[ [
var_assign_var "b" "a"; id_assign_var "b" "a";
var_assign_var "c" "b"; var_assign_id "c" "b";
var_assign_var "d" "c"; id_assign_var "d" "c";
invariant "{ &b -> &a, &c -> &b, &d -> &c }" invariant "{ b$0 -> &a, d$0 -> &c, &c -> b$0 }"
]; ];
"simple_kill", "simple_kill",
[ [
var_assign_var "b" "a"; id_assign_var "b" "a";
invariant "{ &b -> &a }"; invariant "{ b$0 -> &a }";
var_assign_int "a" 1; var_assign_int "a" 1;
assert_empty assert_empty
]; ];
"kill_then_gen", "kill_then_gen",
[ [
var_assign_var "b" "a"; id_assign_var "b" "a";
invariant "{ &b -> &a }"; invariant "{ b$0 -> &a }";
var_assign_var "a" "b"; var_assign_id "a" "c";
invariant "{ &a -> &b }" invariant "{ &a -> c$0 }"
];
"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", "same_copy",
[ [
var_assign_var "b" "a"; var_assign_id "b" "a";
var_assign_var "c" "b"; var_assign_id "c" "d";
invariant "{ &b -> &a, &c -> &b }"; invariant "{ &b -> a$0, &c -> d$0 }";
var_assign_var "c" "b"; var_assign_id "c" "d";
invariant "{ &b -> &a, &c -> &b }" invariant "{ &b -> a$0, &c -> d$0 }"
];
"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", "conservative_if",
[ [
var_assign_var "b" "a"; var_assign_id "b" "a";
If (unknown_exp, If (unknown_exp,
[invariant "{ &b -> &a }"; [invariant "{ &b -> a$0 }";
var_assign_var "a" "b"; var_assign_id "b" "c";
invariant "{ &a -> &b }"], invariant "{ &b -> c$0 }"],
[] []
); );
assert_empty assert_empty
]; ];
"if1", "if1",
[ [
var_assign_var "b" "a"; var_assign_id "b" "a";
var_assign_var "c" "b"; var_assign_id "c" "d";
If (unknown_exp, If (unknown_exp,
[invariant "{ &b -> &a, &c -> &b }"; [invariant "{ &b -> a$0, &c -> d$0 }";
var_assign_var "c" "d"], var_assign_id "c" "e";
[invariant "{ &b -> &a, &c -> &b }"] invariant "{ &b -> a$0, &c -> e$0 }";
],
[invariant "{ &b -> a$0, &c -> d$0 }"]
); );
invariant "{ &b -> &a }" invariant "{ &b -> a$0 }"
]; ];
"if2", "if2",
[ [
If (unknown_exp, If (unknown_exp,
[var_assign_var "a" "b"], [var_assign_id "a" "b"],
[var_assign_var "a" "b"] [var_assign_id "a" "b"]
); );
invariant "{ &a -> &b }" invariant "{ &a -> b$0 }"
]; ];
"if3", "if3",
[ [
If (unknown_exp, If (unknown_exp,
[var_assign_var "a" "b"], [var_assign_id "a" "b"],
[var_assign_var "a" "c"] [var_assign_id "a" "c"]
); );
assert_empty assert_empty
]; ];
"nested_if", "nested_if",
[ [
var_assign_var "b" "a"; var_assign_id "b" "a";
var_assign_var "c" "b"; var_assign_id "c" "b";
If (unknown_exp, If (unknown_exp,
[If (var_of_str "unknown2", [If (var_of_str "unknown2",
[ invariant "{ &b -> &a, &c -> &b }"; [ invariant "{ &b -> a$0, &c -> b$0 }";
var_assign_var "a" "b"; var_assign_id "b" "d";
invariant "{ &a -> &b, &c -> &b }"], invariant "{ &b -> d$0, &c -> b$0 }"],
[] []
) )
], ],
[] []
); );
invariant "{ &c -> &b }" invariant "{ &c -> b$0 }"
]; ];
"loop_as_if", "loop_as_if",
[ [
var_assign_var "b" "a"; var_assign_id "b" "a";
While (unknown_exp, While (unknown_exp,
[var_assign_var "a" "b"] [var_assign_id "b" "c"]
); );
assert_empty assert_empty
]; ];
"easy_loop_invariant", "easy_loop_invariant",
[ [
var_assign_var "b" "a"; var_assign_id "b" "a";
While (unknown_exp, While (unknown_exp,
[var_assign_var "c" "b"; [var_assign_id "c" "d";
invariant "{ &b -> &a, &c -> &b }"] invariant "{ &b -> a$0, &c -> d$0 }"]
); );
invariant "{ &b -> &a }" invariant "{ &b -> a$0 }"
]; ];
"empty_loop", "empty_loop",
[ [
var_assign_var "b" "a"; var_assign_id "b" "a";
While (unknown_exp, []); While (unknown_exp, []);
var_assign_var "c" "b"; var_assign_id "c" "b";
invariant "{ &b -> &a, &c -> &b }" invariant "{ &b -> a$0, &c -> b$0 }"
]; ];
] |> TestInterpreter.create_tests ProcData.empty_extras in ] |> TestInterpreter.create_tests ProcData.empty_extras in
"copy_propagation_test_suite">:::test_list "copy_propagation_test_suite">:::test_list

40
infer/src/unit/livenessTests.ml
Unescape View File

@ -33,32 +33,32 @@ let tests =
"basic_live", "basic_live",
[ [
invariant "{ &b }"; invariant "{ &b }";
var_assign_var "a" "b" id_assign_var "a" "b"
]; ];
"basic_live_then_dead", "basic_live_then_dead",
[ [
assert_empty; assert_empty;
var_assign_int "b" 1; var_assign_int "b" 1;
invariant "{ &b }"; invariant "{ &b }";
var_assign_var "a" "b" id_assign_var "a" "b"
]; ];
"iterative_live", "iterative_live",
[ [
invariant "{ &b, &d, &f }"; invariant "{ &b, &d, &f }";
var_assign_var "e" "f"; id_assign_var "e" "f";
invariant "{ &b, &d }"; invariant "{ &b, &d }";
var_assign_var "c" "d"; id_assign_var "c" "d";
invariant "{ &b }"; invariant "{ &b }";
var_assign_var "a" "b" id_assign_var "a" "b"
]; ];
"live_kill_live", "live_kill_live",
[ [
invariant "{ &b }"; invariant "{ &b }";
var_assign_var "c" "b"; id_assign_var "c" "b";
assert_empty; assert_empty;
var_assign_int "b" 1; var_assign_int "b" 1;
invariant "{ &b }"; invariant "{ &b }";
var_assign_var "a" "b" id_assign_var "a" "b"
]; ];
"basic_live_letderef", "basic_live_letderef",
[ [
@ -112,7 +112,7 @@ let tests =
[ [
invariant "{ &b }"; invariant "{ &b }";
If (unknown_cond, If (unknown_cond,
[var_assign_var "a" "b"], [id_assign_var "a" "b"],
[] []
) )
]; ];
@ -120,8 +120,8 @@ let tests =
[ [
invariant "{ &b, &d }"; invariant "{ &b, &d }";
If (unknown_cond, If (unknown_cond,
[var_assign_var "a" "b"], [id_assign_var "a" "b"],
[var_assign_var "c" "d"] [id_assign_var "c" "d"]
) )
]; ];
"if_conservative_kill", "if_conservative_kill",
@ -132,17 +132,17 @@ let tests =
[] []
); );
invariant "{ &b }"; invariant "{ &b }";
var_assign_var "a" "b" id_assign_var "a" "b"
]; ];
"if_conservative_kill_live", "if_conservative_kill_live",
[ [
invariant "{ &b, &d }"; invariant "{ &b, &d }";
If (unknown_cond, If (unknown_cond,
[var_assign_int "b" 1], [var_assign_int "b" 1],
[var_assign_var "c" "d"] [id_assign_var "c" "d"]
); );
invariant "{ &b }"; invariant "{ &b }";
var_assign_var "a" "b" id_assign_var "a" "b"
]; ];
"if_precise1", "if_precise1",
[ [
@ -150,10 +150,10 @@ let tests =
If (unknown_cond, If (unknown_cond,
[var_assign_int "b" 1; [var_assign_int "b" 1;
invariant "{ &b }"; invariant "{ &b }";
var_assign_var "a" "b"], id_assign_var "a" "b"],
[var_assign_int "d" 1; [var_assign_int "d" 1;
invariant "{ &d }"; invariant "{ &d }";
var_assign_var "c" "d"] id_assign_var "c" "d"]
) )
]; ];
"if_precise2", "if_precise2",
@ -164,13 +164,13 @@ let tests =
[var_assign_int "b" 1] [var_assign_int "b" 1]
); );
invariant "{ &b }"; invariant "{ &b }";
var_assign_var "a" "b" id_assign_var "a" "b"
]; ];
"loop_as_if1", "loop_as_if1",
[ [
invariant "{ &b }"; invariant "{ &b }";
While (unknown_cond, While (unknown_cond,
[var_assign_var "a" "b"] [id_assign_var "a" "b"]
) )
]; ];
"loop_as_if2", "loop_as_if2",
@ -180,16 +180,16 @@ let tests =
[var_assign_int "b" 1] [var_assign_int "b" 1]
); );
invariant "{ &b }"; invariant "{ &b }";
var_assign_var "a" "b" id_assign_var "a" "b"
]; ];
"loop_before_after", "loop_before_after",
[ [
invariant "{ &b, &d }"; invariant "{ &b, &d }";
While (unknown_cond, While (unknown_cond,
[var_assign_var "b" "d"] [id_assign_var "b" "d"]
); );
invariant "{ &b }"; invariant "{ &b }";
var_assign_var "a" "b" id_assign_var "a" "b"
]; ];
] |> TestInterpreter.create_tests ProcData.empty_extras in ] |> TestInterpreter.create_tests ProcData.empty_extras in
"liveness_test_suite">:::test_list "liveness_test_suite">:::test_list

Write Preview
Loading…
Cancel
Save