From ddfd35107cd1f86931557d3d50d75544fb9440d9 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Mon, 7 Mar 2016 08:51:01 -0800 Subject: [PATCH] unit tests for abstract interpreter Reviewed By: dkgi Differential Revision: D2997610 fb-gh-sync-id: 733b45e shipit-source-id: 733b45e --- infer/src/unit/abstractInterpreterTests.ml | 167 ++++++++++++++++++ infer/src/unit/analyzerTester.ml | 189 +++++++++++++++++++++ infer/src/unit/inferunit.ml | 2 +- 3 files changed, 357 insertions(+), 1 deletion(-) create mode 100644 infer/src/unit/abstractInterpreterTests.ml create mode 100644 infer/src/unit/analyzerTester.ml diff --git a/infer/src/unit/abstractInterpreterTests.ml b/infer/src/unit/abstractInterpreterTests.ml new file mode 100644 index 000000000..74cc5cd68 --- /dev/null +++ b/infer/src/unit/abstractInterpreterTests.ml @@ -0,0 +1,167 @@ +(* + * 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 + +(** Test the generic abstract interpreter by using a simple path counting domain. Path counting is + actually a decent stress test--if you join too much/too little, you'll over/under-count, and + you'll diverge at loops if you don't widen *) + +module PathCountDomain = struct + + type astate = + | PathCount of int + | Top + + let make_path_count c = + (* guarding against overflow *) + if c < 0 + then Top + else PathCount c + + let bot = make_path_count 0 + + let init = make_path_count 1 + + let is_bot = function + | PathCount c -> c = 0 + | Top -> false + + let lteq ~lhs ~rhs = match lhs, rhs with + | PathCount c1, PathCount c2 -> c1 <= c2 + | _, Top -> true + | Top, PathCount _ -> false + + let join a1 a2 = match a1, a2 with + | PathCount c1, PathCount c2 -> make_path_count (c1 + c2) + | Top, _ | PathCount _, Top -> Top + + let widen ~prev:_ ~next:_ ~num_iters:_ = Top + + let pp fmt = function + | PathCount c -> F.fprintf fmt "%d" c + | Top -> F.fprintf fmt "T" + +end + +module PathCountTransferFunctions = struct + type astate = PathCountDomain.astate + + (* just propagate the current path count *) + let exec_instr astate _ = astate +end + + +module TestInterpreter = AnalyzerTester.Make + (ProcCfg.Forward) + (Scheduler.ReversePostorder) + (PathCountDomain) + (PathCountTransferFunctions) + +let tests = + let open OUnit2 in + let open AnalyzerTester.StructuredSil in + let test_list = [ + "straightline", + [ + invariant "1"; + invariant "1" + ]; + "if", + [ + invariant "1"; + If (unknown_exp, [], []); + invariant "2"; + ]; + "if_then", + [ + If (unknown_exp, + [invariant "1"], + [] + ); + invariant "2" + ]; + "if_else", + [ + If (unknown_exp, + [], + [invariant "1"] + ); + invariant "2" + ]; + "if_then_else", + [ + If (unknown_exp, + [invariant "1"], + [invariant "1"]; + ); + invariant "2" + ]; + "nested_if_then", + [ + If (unknown_exp, + [If (unknown_exp, [], []); + invariant "2"], + [] + ); + invariant "3" + ]; + "nested_if_else", + [ + If (unknown_exp, + [], + [If (unknown_exp, [], []); + invariant "2"] + ); + invariant "3" + ]; + "nested_if_then_else", + [ + If (unknown_exp, + [If (unknown_exp, [], []); + invariant "2"], + [If (unknown_exp, [], []); + invariant "2"] + ); + invariant "4" + ]; + "if_diamond", + [ + invariant "1"; + If (unknown_exp, [], []); + invariant "2"; + If (unknown_exp, [], []); + invariant "4" + ]; + "loop", + [ + invariant "1"; + While (unknown_exp, [invariant "T"]); + invariant "T" + ]; + "if_in_loop", + [ + While (unknown_exp, + [If (unknown_exp, [], []); + invariant "T"] + ); + invariant "T"; + ]; + "nested_loop_visit", + [ + invariant "1"; + While (unknown_exp, + [invariant "T"; + While (unknown_exp, + [invariant "T"]); + invariant "T"]); + invariant "T"; + ]; + ] |> TestInterpreter.create_tests in + "analyzer_tests_suite">:::test_list diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml new file mode 100644 index 000000000..fbaa6f626 --- /dev/null +++ b/infer/src/unit/analyzerTester.ml @@ -0,0 +1,189 @@ +(* + * 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 + +open AbstractDomain +open TransferFunctions + +(** utilities for writing abstract domains/transfer function tests *) + +(** structured language that makes it easy to write small test programs in OCaml *) +module StructuredSil = struct + type assertion = string + type label = int + + type structured_instr = + | Cmd of Sil.instr + | If of Sil.exp * structured_instr list * structured_instr list + | While of Sil.exp * structured_instr list + | Invariant of assertion * label (* gets autotranslated into assertions about abstract state *) + + type structured_program = structured_instr list + + let rec pp_structured_instr fmt = function + | Cmd instr -> (Sil.pp_instr pe_text) fmt instr + | If (exp, then_instrs, else_instrs) -> + (* TODO (t10287763): indent bodies of if/while *) + F.fprintf fmt "if (%a) {@.%a@.} else {@.%a@.}" + (Sil.pp_exp pe_text) exp + pp_structured_instr_list then_instrs + pp_structured_instr_list else_instrs + | While (exp, instrs) -> + F.fprintf fmt "while (%a) {@.%a@.}" (Sil.pp_exp pe_text) exp pp_structured_instr_list instrs + | Invariant (inv_str, label) -> + F.fprintf fmt "invariant %d: %s" label inv_str + + and pp_structured_instr_list fmt instrs = + F.pp_print_list + ~pp_sep:F.pp_print_newline + (fun fmt instr -> F.fprintf fmt "%a" pp_structured_instr instr) + fmt + instrs + + let pp_structured_program = pp_structured_instr_list + + let dummy_typ = Sil.Tvoid + let dummy_loc = Location.dummy + let dummy_procname = Procname.empty + + let label_counter = ref 0 + + let fresh_label () = + incr label_counter; + !label_counter + + let invariant inv_str = + Invariant (inv_str, fresh_label ()) + + let var_of_str str = + Sil.Lvar (Sil.mk_pvar (Mangled.from_string str) dummy_procname) + + let unknown_exp = + var_of_str "__unknown__" + +end + +module Make + (C : ProcCfg.Wrapper with type node = Cfg.Node.t) + (S : Scheduler.S) + (A : AbstractDomain) + (T : TransferFunctions with type astate = A.astate) = struct + + open StructuredSil + + module I = AbstractInterpreter.Make (C) (S) (A) (T) + module M = ProcCfg.NodeIdMap (C) + + type assert_map = string M.t + + let structured_program_to_cfg program = + let cfg = Cfg.Node.create_cfg () in + let pdesc = + Cfg.Procdesc.create cfg (ProcAttributes.default dummy_procname !Config.curr_language) in + + let create_node kind cmds = + let no_tmp_idents = [] in + Cfg.Node.create cfg dummy_loc kind cmds pdesc no_tmp_idents in + let set_succs cur_node succs = + let no_exc_succs = [] in + Cfg.Node.set_succs_exn cur_node succs no_exc_succs in + let mk_prune_nodes_for_cond cond_exp if_kind = + let mk_prune_node cond_exp if_kind true_branch = + let prune_instr = Sil.Prune (cond_exp, dummy_loc, true_branch, if_kind) in + create_node (Cfg.Node.Prune_node (true_branch, if_kind, "")) [prune_instr] in + let true_prune_node = mk_prune_node cond_exp if_kind true in + let false_prune_node = + let negated_cond_exp = Sil.UnOp (Sil.LNot, cond_exp, None) in + mk_prune_node negated_cond_exp if_kind false in + true_prune_node, false_prune_node in + + let rec structured_instr_to_node (last_node, assert_map) = function + | Cmd cmd -> + let node = create_node (Cfg.Node.Stmt_node "") [cmd] in + set_succs last_node [node]; + node, assert_map + | If (exp, then_instrs, else_instrs) -> + let then_prune_node, else_prune_node = mk_prune_nodes_for_cond exp Sil.Ik_if in + set_succs last_node [then_prune_node; else_prune_node]; + let then_branch_end_node, assert_map' = + structured_instrs_to_node then_prune_node assert_map then_instrs in + let else_branch_end_node, assert_map'' = + structured_instrs_to_node else_prune_node assert_map' else_instrs in + let join_node = create_node Cfg.Node.Join_node [] in + set_succs then_branch_end_node [join_node]; + set_succs else_branch_end_node [join_node]; + join_node, assert_map'' + | While (exp, body_instrs) -> + let loop_head_join_node = create_node Cfg.Node.Join_node [] in + set_succs last_node [loop_head_join_node]; + let true_prune_node, false_prune_node = mk_prune_nodes_for_cond exp Sil.Ik_while in + set_succs loop_head_join_node [true_prune_node; false_prune_node]; + let loop_body_end_node, assert_map' = + structured_instrs_to_node true_prune_node assert_map body_instrs in + let loop_exit_node = create_node (Cfg.Node.Skip_node "") [] in + set_succs loop_body_end_node [loop_head_join_node]; + set_succs false_prune_node [loop_exit_node]; + loop_exit_node, assert_map' + | Invariant (inv_str, inv_label) -> + let n_id = C.node_id last_node in + (* add the assertion to be checked after analysis converges *) + last_node, M.add n_id (inv_str, inv_label) assert_map + and structured_instrs_to_node last_node assert_map instrs = + IList.fold_left + (fun acc instr -> structured_instr_to_node acc instr) (last_node, assert_map) instrs in + + let start_node = create_node (Cfg.Node.Start_node pdesc) [] in + Cfg.Procdesc.set_start_node pdesc start_node; + let last_node, assert_map = structured_instrs_to_node start_node M.empty program in + let exit_node = create_node (Cfg.Node.Exit_node pdesc) [] in + set_succs last_node [exit_node]; + Cfg.Procdesc.set_exit_node pdesc exit_node; + pdesc, assert_map + + let create_test test_program _ = + let pdesc, assert_map = structured_program_to_cfg test_program in + let inv_map = I.exec_pdesc pdesc in + + let collect_invariant_mismatches node_id (inv_str, inv_label) error_msgs_acc = + let node_id_post = + try + let state = M.find node_id inv_map in + state.post + with Not_found -> A.bot in + let post_str = pp_to_string A.pp node_id_post in + if inv_str <> post_str then + let error_msg = + F.fprintf F.str_formatter + "> Expected state %s at invariant %d, but found state %s" + inv_str inv_label post_str + |> F.flush_str_formatter in + error_msg :: error_msgs_acc + else error_msgs_acc in + + match M.fold collect_invariant_mismatches assert_map [] with + | [] -> () (* no mismatches, test passed *) + | error_msgs -> + let mismatches_str = + F.pp_print_list + (fun fmt error_msg -> F.fprintf fmt "%s" error_msg) F.str_formatter + (IList.rev error_msgs) + |> F.flush_str_formatter in + let assert_fail_message = + F.fprintf F.str_formatter "Error while analyzing@.%a:@.%s@." + pp_structured_program test_program mismatches_str + |> F.flush_str_formatter in + OUnit2.assert_failure assert_fail_message + + let create_tests tests = + let open OUnit2 in + IList.map (fun (name, test_program) -> name>::create_test test_program) tests + +end diff --git a/infer/src/unit/inferunit.ml b/infer/src/unit/inferunit.ml index 38c2b7736..256987abc 100644 --- a/infer/src/unit/inferunit.ml +++ b/infer/src/unit/inferunit.ml @@ -13,7 +13,7 @@ let () = let open OUnit2 in let tests = [ SchedulerTests.tests; - AbstractInterpreter.UnitTests.tests; + AbstractInterpreterTests.tests; ] in let test_suite = "all" >::: tests in OUnit2.run_test_tt_main test_suite