diff --git a/infer/src/checkers/copyPropagation.ml b/infer/src/checkers/copyPropagation.ml index cd0a8e137..161ee2d7a 100644 --- a/infer/src/checkers/copyPropagation.ml +++ b/infer/src/checkers/copyPropagation.ml @@ -89,11 +89,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct 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) -> 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, _, _, _) -> - (* 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 | Sil.Letderef _ (* 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 *) astate 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)) diff --git a/infer/src/unit/addressTakenTests.ml b/infer/src/unit/addressTakenTests.ml index f3e323bf4..85f7e5cb3 100644 --- a/infer/src/unit/addressTakenTests.ml +++ b/infer/src/unit/addressTakenTests.ml @@ -31,12 +31,12 @@ let tests = let test_list = [ "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 }" ]; "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 ]; "address_not_taken_letderef_instr1", @@ -51,23 +51,23 @@ let tests = ]; "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 }"; - var_assign_var ~rhs_typ:int_ptr_typ "c" "d"; + var_assign_addrof_var ~rhs_typ:int_ptr_typ "c" "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 }" ]; "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"]); invariant "{ &b }" ]; "if_conservative1", [ 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 }" @@ -75,27 +75,27 @@ let tests = "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"] + [var_assign_addrof_var ~rhs_typ:int_ptr_typ "a" "b"], + [var_assign_addrof_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"] + [var_assign_addrof_var ~rhs_typ:int_ptr_typ "a" "b"] ); invariant "{ &b }" ]; "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 }"; 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 }"; - 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 }" ]; ] |> TestInterpreter.create_tests ProcData.empty_extras in diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index 0a0e2f1c7..df9a6b431 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -123,7 +123,8 @@ module StructuredSil = struct let rhs_exp = Sil.Var (ident_of_str rhs) in 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 rhs_exp = var_of_str rhs in make_set ~rhs_typ ~lhs_exp ~rhs_exp diff --git a/infer/src/unit/copyPropagationTests.ml b/infer/src/unit/copyPropagationTests.ml index db7830191..2b87b3426 100644 --- a/infer/src/unit/copyPropagationTests.ml +++ b/infer/src/unit/copyPropagationTests.ml @@ -21,16 +21,6 @@ let tests = 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_letderef_id_no_gen", [ id_assign_id "b" "a"; (* means b = *a *) @@ -41,7 +31,6 @@ let tests = id_set_id "b" "a"; (* means *b = a *) assert_empty ]; - "id_set_id_no_kill", [ id_assign_var "b" "a"; @@ -54,10 +43,10 @@ let tests = id_assign_var "b" "a"; invariant "{ b$0 -> &a }" ]; - "var_assign_var_gen", + "var_assign_addrof_var_no_gen", [ - var_assign_var "b" "a"; - invariant "{ &b -> &a }" + var_assign_addrof_var "b" "a"; (* means b = &a *) + assert_empty ]; "var_assign_id_gen", [ @@ -66,130 +55,112 @@ let tests = ]; "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 }" + 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", [ - var_assign_var "b" "a"; - invariant "{ &b -> &a }"; + id_assign_var "b" "a"; + invariant "{ b$0 -> &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 }" + id_assign_var "b" "a"; + invariant "{ b$0 -> &a }"; + var_assign_id "a" "c"; + invariant "{ &a -> c$0 }" ]; "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 }" + 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_var "b" "a"; + var_assign_id "b" "a"; If (unknown_exp, - [invariant "{ &b -> &a }"; - var_assign_var "a" "b"; - invariant "{ &a -> &b }"], + [invariant "{ &b -> a$0 }"; + var_assign_id "b" "c"; + invariant "{ &b -> c$0 }"], [] ); assert_empty ]; "if1", [ - var_assign_var "b" "a"; - var_assign_var "c" "b"; + var_assign_id "b" "a"; + var_assign_id "c" "d"; If (unknown_exp, - [invariant "{ &b -> &a, &c -> &b }"; - var_assign_var "c" "d"], - [invariant "{ &b -> &a, &c -> &b }"] + [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 }" + invariant "{ &b -> a$0 }" ]; "if2", [ If (unknown_exp, - [var_assign_var "a" "b"], - [var_assign_var "a" "b"] + [var_assign_id "a" "b"], + [var_assign_id "a" "b"] ); - invariant "{ &a -> &b }" + invariant "{ &a -> b$0 }" ]; "if3", [ If (unknown_exp, - [var_assign_var "a" "b"], - [var_assign_var "a" "c"] + [var_assign_id "a" "b"], + [var_assign_id "a" "c"] ); assert_empty ]; "nested_if", [ - var_assign_var "b" "a"; - var_assign_var "c" "b"; + var_assign_id "b" "a"; + var_assign_id "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 "{ &b -> a$0, &c -> b$0 }"; + var_assign_id "b" "d"; + invariant "{ &b -> d$0, &c -> b$0 }"], [] ) ], [] ); - invariant "{ &c -> &b }" + invariant "{ &c -> b$0 }" ]; "loop_as_if", [ - var_assign_var "b" "a"; + var_assign_id "b" "a"; While (unknown_exp, - [var_assign_var "a" "b"] + [var_assign_id "b" "c"] ); assert_empty ]; "easy_loop_invariant", [ - var_assign_var "b" "a"; + var_assign_id "b" "a"; While (unknown_exp, - [var_assign_var "c" "b"; - invariant "{ &b -> &a, &c -> &b }"] + [var_assign_id "c" "d"; + invariant "{ &b -> a$0, &c -> d$0 }"] ); - invariant "{ &b -> &a }" + invariant "{ &b -> a$0 }" ]; "empty_loop", [ - var_assign_var "b" "a"; + var_assign_id "b" "a"; While (unknown_exp, []); - var_assign_var "c" "b"; - invariant "{ &b -> &a, &c -> &b }" + var_assign_id "c" "b"; + invariant "{ &b -> a$0, &c -> b$0 }" ]; ] |> TestInterpreter.create_tests ProcData.empty_extras in "copy_propagation_test_suite">:::test_list diff --git a/infer/src/unit/livenessTests.ml b/infer/src/unit/livenessTests.ml index 5128eeae2..8ba4ba6d8 100644 --- a/infer/src/unit/livenessTests.ml +++ b/infer/src/unit/livenessTests.ml @@ -33,32 +33,32 @@ let tests = "basic_live", [ invariant "{ &b }"; - var_assign_var "a" "b" + id_assign_var "a" "b" ]; "basic_live_then_dead", [ assert_empty; var_assign_int "b" 1; invariant "{ &b }"; - var_assign_var "a" "b" + id_assign_var "a" "b" ]; "iterative_live", [ invariant "{ &b, &d, &f }"; - var_assign_var "e" "f"; + id_assign_var "e" "f"; invariant "{ &b, &d }"; - var_assign_var "c" "d"; + id_assign_var "c" "d"; invariant "{ &b }"; - var_assign_var "a" "b" + id_assign_var "a" "b" ]; "live_kill_live", [ invariant "{ &b }"; - var_assign_var "c" "b"; + id_assign_var "c" "b"; assert_empty; var_assign_int "b" 1; invariant "{ &b }"; - var_assign_var "a" "b" + id_assign_var "a" "b" ]; "basic_live_letderef", [ @@ -112,7 +112,7 @@ let tests = [ invariant "{ &b }"; If (unknown_cond, - [var_assign_var "a" "b"], + [id_assign_var "a" "b"], [] ) ]; @@ -120,8 +120,8 @@ let tests = [ invariant "{ &b, &d }"; If (unknown_cond, - [var_assign_var "a" "b"], - [var_assign_var "c" "d"] + [id_assign_var "a" "b"], + [id_assign_var "c" "d"] ) ]; "if_conservative_kill", @@ -132,17 +132,17 @@ let tests = [] ); invariant "{ &b }"; - var_assign_var "a" "b" + id_assign_var "a" "b" ]; "if_conservative_kill_live", [ invariant "{ &b, &d }"; If (unknown_cond, [var_assign_int "b" 1], - [var_assign_var "c" "d"] + [id_assign_var "c" "d"] ); invariant "{ &b }"; - var_assign_var "a" "b" + id_assign_var "a" "b" ]; "if_precise1", [ @@ -150,10 +150,10 @@ let tests = If (unknown_cond, [var_assign_int "b" 1; invariant "{ &b }"; - var_assign_var "a" "b"], + id_assign_var "a" "b"], [var_assign_int "d" 1; invariant "{ &d }"; - var_assign_var "c" "d"] + id_assign_var "c" "d"] ) ]; "if_precise2", @@ -164,13 +164,13 @@ let tests = [var_assign_int "b" 1] ); invariant "{ &b }"; - var_assign_var "a" "b" + id_assign_var "a" "b" ]; "loop_as_if1", [ invariant "{ &b }"; While (unknown_cond, - [var_assign_var "a" "b"] + [id_assign_var "a" "b"] ) ]; "loop_as_if2", @@ -180,16 +180,16 @@ let tests = [var_assign_int "b" 1] ); invariant "{ &b }"; - var_assign_var "a" "b" + id_assign_var "a" "b" ]; "loop_before_after", [ invariant "{ &b, &d }"; While (unknown_cond, - [var_assign_var "b" "d"] + [id_assign_var "b" "d"] ); invariant "{ &b }"; - var_assign_var "a" "b" + id_assign_var "a" "b" ]; ] |> TestInterpreter.create_tests ProcData.empty_extras in "liveness_test_suite">:::test_list