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

@@ -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

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

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