From 36b0a957bd8035e96b213937662dc86e8c1aed71 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Tue, 23 Aug 2016 17:50:49 -0700 Subject: [PATCH] setup for creating very simple absint checkers Reviewed By: cristianoc Differential Revision: D3734044 fbshipit-source-id: 014b0d9 --- infer/src/checkers/SimpleChecker.ml | 108 ++++++++++++++++++++++++++++ infer/src/checkers/procCfg.ml | 4 ++ infer/src/checkers/procCfg.mli | 1 + infer/src/unit/schedulerTests.ml | 1 + 4 files changed, 114 insertions(+) create mode 100644 infer/src/checkers/SimpleChecker.ml diff --git a/infer/src/checkers/SimpleChecker.ml b/infer/src/checkers/SimpleChecker.ml new file mode 100644 index 000000000..23fb535cf --- /dev/null +++ b/infer/src/checkers/SimpleChecker.ml @@ -0,0 +1,108 @@ +(* + * 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! Utils + +module F = Format +module L = Logging + +(** functor that makes it easy to write a basic abstract interpretation checker by lifting + a type, comparison function, reporting function, and exec function into an analyzer *) + +module type Spec = sig + type astate (** what state do you want to propagate? *) + + (** implement the state the analysis should start from here *) + val initial : astate + + (** implement how an instruction changes your state here. + input is the previous state, current instruction, current node kind, current procedure and + type environment. + *) + val exec_instr : astate -> Sil.instr -> Cfg.Node.nodekind -> Procname.t -> Tenv.t -> astate + + (** log errors here. + input is a state, location where the state occurs in the source, and the current procedure. + *) + val report : astate -> Location.t -> Procname.t -> unit + + val compare : astate -> astate -> int +end + +module type S = sig + (** add YourChecker.checker to registerCallbacks.ml to run your checker *) + val checker : Callbacks.proc_callback_args -> unit +end + +module Make (Spec : Spec) : S = struct + + (* powerset domain over Spec.astate *) + module Domain = struct + include + AbstractDomain.FiniteSet + (PrettyPrintable.MakePPSet( + struct + type t = Spec.astate + let compare = Spec.compare + let pp_element _ _ = () + end) + ) + + let initial = singleton Spec.initial + + let widen ~prev ~next ~num_iters = + let iters_befor_timeout = 1000 in + (* failsafe for accidental non-finite height domains *) + if num_iters >= iters_befor_timeout + then + failwith + ("Stopping analysis after 1000 iterations without convergence." ^ + "Make sure your domain is finite height.") + else widen ~prev ~next ~num_iters + end + + module TransferFunctions (CFG : ProcCfg.S) = struct + module CFG = CFG + module Domain = Domain + type extras = ProcData.no_extras + + let exec_instr astate_set proc_data node instr = + let node_kind = CFG.kind node in + let pname = Cfg.Procdesc.get_proc_name proc_data.ProcData.pdesc in + Domain.fold + (fun astate acc -> + Domain.add (Spec.exec_instr astate instr node_kind pname proc_data.ProcData.tenv) acc) + astate_set + Domain.empty + end + + module Analyzer = + AbstractInterpreter.Make + (ProcCfg.Exceptional) + (Scheduler.ReversePostorder) + (TransferFunctions) + + let checker { Callbacks.proc_desc; proc_name; tenv; } = + let nodes = Cfg.Procdesc.get_nodes proc_desc in + let do_reporting node_id state = + let astate_set = state.AbstractInterpreter.post in + if not (Domain.is_empty astate_set) + then + (* should never fail since keys in the invariant map should always be real node id's *) + let node = + IList.find + (fun node -> Cfg.Node.id_compare node_id (Cfg.Node.get_id node) = 0) + nodes in + Domain.iter + (fun astate -> + Spec.report astate (ProcCfg.Exceptional.loc node) proc_name) + astate_set in + let inv_map = Analyzer.exec_pdesc (ProcData.make_default proc_desc tenv) in + Analyzer.M.iter do_reporting inv_map +end diff --git a/infer/src/checkers/procCfg.ml b/infer/src/checkers/procCfg.ml index e6d1b93bd..c6b6d106e 100644 --- a/infer/src/checkers/procCfg.ml +++ b/infer/src/checkers/procCfg.ml @@ -23,6 +23,7 @@ module type Node = sig val kind : t -> Cfg.Node.nodekind val id : t -> id + val loc : t -> Location.t val underlying_id : t -> Cfg.Node.id val id_compare : id -> id -> int val pp_id : F.formatter -> id -> unit @@ -34,6 +35,7 @@ module DefaultNode = struct let kind = Cfg.Node.get_kind let id = Cfg.Node.get_id + let loc = Cfg.Node.get_loc let underlying_id = id let id_compare = Cfg.Node.id_compare let pp_id = Cfg.Node.pp_id @@ -49,6 +51,8 @@ module InstrNode = struct let id t = underlying_id t, Node_index + let loc t = Cfg.Node.get_loc t + let index_compare index1 index2 = match index1, index2 with | Node_index, Node_index -> 0 | Instr_index i1, Instr_index i2 -> int_compare i1 i2 diff --git a/infer/src/checkers/procCfg.mli b/infer/src/checkers/procCfg.mli index 333ca0a26..e373056da 100644 --- a/infer/src/checkers/procCfg.mli +++ b/infer/src/checkers/procCfg.mli @@ -19,6 +19,7 @@ module type Node = sig val kind : t -> Cfg.Node.nodekind val id : t -> id + val loc : t -> Location.t val underlying_id : t -> Cfg.Node.id val id_compare : id -> id -> int val pp_id : Format.formatter -> id -> unit diff --git a/infer/src/unit/schedulerTests.ml b/infer/src/unit/schedulerTests.ml index 895b8bf89..067381a21 100644 --- a/infer/src/unit/schedulerTests.ml +++ b/infer/src/unit/schedulerTests.ml @@ -22,6 +22,7 @@ module MockNode = struct let instr_ids _ = [] let to_instr_nodes _ = assert false let id n = n + let loc _ = assert false let underlying_id _ = assert false let kind _ = Cfg.Node.Stmt_node "" let id_compare = int_compare