[ocamlformat] Reformat repo with new version

Reviewed By: jvillard

Differential Revision: D21583046

fbshipit-source-id: ee4793880
master
Josh Berdine 5 years ago committed by Facebook GitHub Bot
parent cfc861a186
commit 65f369cf35

@ -46,14 +46,14 @@ and t =
val equal : t -> t -> bool val equal : t -> t -> bool
(** Equality for expressions. *) (** Equality for expressions. *)
module Set : Caml.Set.S with type elt = t
(** Set of expressions. *) (** Set of expressions. *)
module Set : Caml.Set.S with type elt = t
module Map : Caml.Map.S with type key = t
(** Map with expression keys. *) (** Map with expression keys. *)
module Map : Caml.Map.S with type key = t
module Hash : Caml.Hashtbl.S with type key = t
(** Hashtable with expression keys. *) (** Hashtable with expression keys. *)
module Hash : Caml.Hashtbl.S with type key = t
val is_null_literal : t -> bool val is_null_literal : t -> bool

@ -20,11 +20,11 @@ val get_field_name : t -> string
val is_java : t -> bool val is_java : t -> bool
module Set : Caml.Set.S with type elt = t
(** Set for fieldnames *) (** Set for fieldnames *)
module Set : Caml.Set.S with type elt = t
module Map : Caml.Map.S with type key = t
(** Map for fieldnames *) (** Map for fieldnames *)
module Map : Caml.Map.S with type key = t
val is_java_outer_instance : t -> bool val is_java_outer_instance : t -> bool
(** Check if the field is the synthetic this$n of a nested class, used to access the n-th outer (** Check if the field is the synthetic this$n of a nested class, used to access the n-th outer

@ -28,14 +28,14 @@ type kind [@@deriving compare]
val equal_kind : kind -> kind -> bool val equal_kind : kind -> kind -> bool
(** Equality for kind. *) (** Equality for kind. *)
module Set : Caml.Set.S with type elt = t
(** Set for identifiers. *) (** Set for identifiers. *)
module Set : Caml.Set.S with type elt = t
module Hash : Caml.Hashtbl.S with type key = t
(** Hash table with ident as key. *) (** Hash table with ident as key. *)
module Hash : Caml.Hashtbl.S with type key = t
module Map : Caml.Map.S with type key = t
(** Map with ident as key. *) (** Map with ident as key. *)
module Map : Caml.Map.S with type key = t
module HashQueue : Hash_queue.S with type key = t module HashQueue : Hash_queue.S with type key = t

@ -42,8 +42,8 @@ val is_self : t -> bool
val rename : f:(string -> string) -> t -> t val rename : f:(string -> string) -> t -> t
(** Maps over both the plain and the mangled components. *) (** Maps over both the plain and the mangled components. *)
module Set : Caml.Set.S with type elt = t
(** Set of Mangled. *) (** Set of Mangled. *)
module Set : Caml.Set.S with type elt = t
module Map : Caml.Map.S with type key = t
(** Map with Mangled as key *) (** Map with Mangled as key *)
module Map : Caml.Map.S with type key = t

@ -420,17 +420,17 @@ end
(* =============== END of module Node =============== *) (* =============== END of module Node =============== *)
module NodeMap = Caml.Map.Make (Node)
(** Map over nodes *) (** Map over nodes *)
module NodeMap = Caml.Map.Make (Node)
module NodeHash = Hashtbl.Make (Node)
(** Hash table with nodes as keys. *) (** Hash table with nodes as keys. *)
module NodeHash = Hashtbl.Make (Node)
module NodeSet = Node.NodeSet
(** Set of nodes. *) (** Set of nodes. *)
module NodeSet = Node.NodeSet
module IdMap = Node.IdMap
(** Map with node id keys. *) (** Map with node id keys. *)
module IdMap = Node.IdMap
(** procedure description *) (** procedure description *)
type t = type t =

@ -176,17 +176,17 @@ module Node : sig
val compute_key : t -> NodeKey.t val compute_key : t -> NodeKey.t
end end
module IdMap : PrettyPrintable.PPMap with type key = Node.id
(** Map with node id keys. *) (** Map with node id keys. *)
module IdMap : PrettyPrintable.PPMap with type key = Node.id
module NodeHash : Caml.Hashtbl.S with type key = Node.t
(** Hash table with nodes as keys. *) (** Hash table with nodes as keys. *)
module NodeHash : Caml.Hashtbl.S with type key = Node.t
module NodeMap : Caml.Map.S with type key = Node.t
(** Map over nodes. *) (** Map over nodes. *)
module NodeMap : Caml.Map.S with type key = Node.t
module NodeSet : Caml.Set.S with type elt = Node.t
(** Set of nodes. *) (** Set of nodes. *)
module NodeSet : Caml.Set.S with type elt = Node.t
(** procedure descriptions *) (** procedure descriptions *)
@ -310,8 +310,8 @@ val is_captured_var : t -> Var.t -> bool
val has_modify_in_block_attr : t -> Pvar.t -> bool val has_modify_in_block_attr : t -> Pvar.t -> bool
module SQLite : SqliteUtils.Data with type t = t option
(** per-procedure CFGs are stored in the SQLite "procedures" table as NULL if the procedure has no (** per-procedure CFGs are stored in the SQLite "procedures" table as NULL if the procedure has no
CFG *) CFG *)
module SQLite : SqliteUtils.Data with type t = t option
val load : Procname.t -> t option val load : Procname.t -> t option

@ -224,18 +224,18 @@ val is_java_autogen_method : t -> bool
val is_objc_method : t -> bool val is_objc_method : t -> bool
module Hash : Caml.Hashtbl.S with type key = t
(** Hash tables with proc names as keys. *) (** Hash tables with proc names as keys. *)
module Hash : Caml.Hashtbl.S with type key = t
module LRUHash : LRUHashtbl.S with type key = t module LRUHash : LRUHashtbl.S with type key = t
module HashQueue : Hash_queue.S with type key = t module HashQueue : Hash_queue.S with type key = t
module Map : PrettyPrintable.PPMap with type key = t
(** Maps from proc names. *) (** Maps from proc names. *)
module Map : PrettyPrintable.PPMap with type key = t
module Set : PrettyPrintable.PPSet with type elt = t
(** Sets of proc names. *) (** Sets of proc names. *)
module Set : PrettyPrintable.PPSet with type elt = t
module SQLite : sig module SQLite : sig
val serialize : t -> Sqlite3.Data.t val serialize : t -> Sqlite3.Data.t

@ -169,5 +169,5 @@ val materialized_cpp_temporary : string
val rename : f:(string -> string) -> t -> t val rename : f:(string -> string) -> t -> t
module Set : PrettyPrintable.PPSet with type elt = t
(** Sets of pvars. *) (** Sets of pvars. *)
module Set : PrettyPrintable.PPSet with type elt = t

@ -9,8 +9,8 @@ module L = Logging
(** Module for Type Environments. *) (** Module for Type Environments. *)
module TypenameHash = Caml.Hashtbl.Make (Typ.Name)
(** Hash tables on type names. *) (** Hash tables on type names. *)
module TypenameHash = Caml.Hashtbl.Make (Typ.Name)
module TypenameHashNormalizer = MaximumSharing.ForHashtbl (TypenameHash) module TypenameHashNormalizer = MaximumSharing.ForHashtbl (TypenameHash)

@ -111,10 +111,10 @@ module type Make = functor (CFG : PreProcCfg) -> S with module CFG = CFG
module Bourdoncle_SCC (CFG : PreProcCfg) = struct module Bourdoncle_SCC (CFG : PreProcCfg) = struct
module CFG = CFG module CFG = CFG
module Dfn = CFG.Node.IdMap
(** [dfn] contains a DFS pre-order indexing. A node is not in the map if it has never been (** [dfn] contains a DFS pre-order indexing. A node is not in the map if it has never been
visited. A node's dfn is +oo if it has been fully visited (head of cross-edges) or we want to visited. A node's dfn is +oo if it has been fully visited (head of cross-edges) or we want to
hide it for building a subcomponent partition (head of highest back-edges). *) hide it for building a subcomponent partition (head of highest back-edges). *)
module Dfn = CFG.Node.IdMap
(* (*
Unlike Bourdoncle's paper version or OCamlGraph implementation, this implementation handles Unlike Bourdoncle's paper version or OCamlGraph implementation, this implementation handles

@ -74,6 +74,6 @@ end
module type Make = functor (CFG : PreProcCfg) -> S with module CFG = CFG module type Make = functor (CFG : PreProcCfg) -> S with module CFG = CFG
module Bourdoncle_SCC : Make
(** Implementation of Bourdoncle's "Hierarchical decomposition of a directed graph into strongly (** Implementation of Bourdoncle's "Hierarchical decomposition of a directed graph into strongly
connected components and subcomponents". See [Bou] Figure 4, page 10. *) connected components and subcomponents". See [Bou] Figure 4, page 10. *)
module Bourdoncle_SCC : Make

@ -38,8 +38,8 @@ include (* ocaml ignores the warning suppression at toplevel, hence the [include
sig sig
[@@@warning "-60"] [@@@warning "-60"]
module Empty : S with type t = unit
(** a trivial domain *) (** a trivial domain *)
module Empty : S with type t = unit
end end
(** A domain with an explicit bottom value *) (** A domain with an explicit bottom value *)
@ -253,13 +253,13 @@ include sig
end end
end end
module BooleanAnd : S with type t = bool
(** Boolean domain ordered by p || ~q. Useful when you want a boolean that's true only when it's (** Boolean domain ordered by p || ~q. Useful when you want a boolean that's true only when it's
true in both conditional branches. *) true in both conditional branches. *)
module BooleanAnd : S with type t = bool
module BooleanOr : WithBottom with type t = bool
(** Boolean domain ordered by ~p || q. Useful when you want a boolean that's true only when it's (** Boolean domain ordered by ~p || q. Useful when you want a boolean that's true only when it's
true in one conditional branch. *) true in one conditional branch. *)
module BooleanOr : WithBottom with type t = bool
module type MaxCount = sig module type MaxCount = sig
val max : int val max : int
@ -271,8 +271,8 @@ end
module CountDomain (MaxCount : MaxCount) : sig module CountDomain (MaxCount : MaxCount) : sig
include WithBottom with type t = private int include WithBottom with type t = private int
include WithTop with type t := t
(** top is maximum value *) (** top is maximum value *)
include WithTop with type t := t
val increment : t -> t val increment : t -> t
(** bump the count by one if it is less than the max *) (** bump the count by one if it is less than the max *)
@ -287,11 +287,11 @@ end
(** Domain keeping a non-negative count with a bounded maximum value. [join] is minimum and [top] is (** Domain keeping a non-negative count with a bounded maximum value. [join] is minimum and [top] is
zero. *) zero. *)
module DownwardIntDomain (MaxCount : MaxCount) : sig module DownwardIntDomain (MaxCount : MaxCount) : sig
include WithTop with type t = private int
(** top is zero *) (** top is zero *)
include WithTop with type t = private int
include WithBottom with type t := t
(** bottom is the provided maximum *) (** bottom is the provided maximum *)
include WithBottom with type t := t
val increment : t -> t val increment : t -> t
(** bump the count by one if this won't cross the maximum *) (** bump the count by one if this won't cross the maximum *)

@ -402,8 +402,7 @@ module AbstractInterpreterCommon (TransferFunctions : NodeTransferFunctions) = s
(* shadowed for HTML debug *) (* shadowed for HTML debug *)
let compute_pre cfg node inv_map = let compute_pre cfg node inv_map =
AnalysisCallbacks.html_debug_new_node_session (Node.underlying_node node) ~kind:`ComputePre AnalysisCallbacks.html_debug_new_node_session (Node.underlying_node node) ~kind:`ComputePre
~pp_name:(TransferFunctions.pp_session_name node) ~f:(fun () -> compute_pre cfg node inv_map ~pp_name:(TransferFunctions.pp_session_name node) ~f:(fun () -> compute_pre cfg node inv_map)
)
(** compute and return an invariant map for [pdesc] *) (** compute and return an invariant map for [pdesc] *)

@ -63,13 +63,13 @@ end
module type Make = functor (TransferFunctions : TransferFunctions.SIL) -> module type Make = functor (TransferFunctions : TransferFunctions.SIL) ->
S with module TransferFunctions = TransferFunctions S with module TransferFunctions = TransferFunctions
module MakeRPO : Make
(** create an intraprocedural abstract interpreter from transfer functions using the reverse (** create an intraprocedural abstract interpreter from transfer functions using the reverse
post-order scheduler *) post-order scheduler *)
module MakeRPO : Make
module MakeWTO : Make
(** create an intraprocedural abstract interpreter from transfer functions using Bourdoncle's (** create an intraprocedural abstract interpreter from transfer functions using Bourdoncle's
strongly connected component weak topological order *) strongly connected component weak topological order *)
module MakeWTO : Make
(** In the disjunctive interpreter, the domain is a set of abstract states representing a (** In the disjunctive interpreter, the domain is a set of abstract states representing a
disjunction between these states. The transfer functions are executed on each state in the disjunction between these states. The transfer functions are executed on each state in the

@ -22,7 +22,6 @@ module type S = sig
(** map from access -> nodes. a leaf is encoded as an empty map *) (** map from access -> nodes. a leaf is encoded as an empty map *)
| Star (** special leaf for starred access paths *) | Star (** special leaf for starred access paths *)
include AbstractDomain.WithBottom with type t = node BaseMap.t
(** map from base var -> access subtree. Here's how to represent a few different kinds of trace * (** map from base var -> access subtree. Here's how to represent a few different kinds of trace *
access path associations: access path associations:
@ -35,6 +34,7 @@ module type S = sig
(x.f, T1), (x.g, T2) := { x |-> (empty, Subtree { f |-> (T1, Subtree {}), (x.f, T1), (x.g, T2) := { x |-> (empty, Subtree { f |-> (T1, Subtree {}),
g |-> (T2, Subtree {}) }) } g |-> (T2, Subtree {}) }) }
]} *) ]} *)
include AbstractDomain.WithBottom with type t = node BaseMap.t
val empty_node : node val empty_node : node

@ -24,8 +24,8 @@ end
module type CallPrinter = PrettyPrintable.PrintableType with type t = CallSite.t module type CallPrinter = PrettyPrintable.PrintableType with type t = CallSite.t
module DefaultCallPrinter : CallPrinter
(** Printer which outputs "Method call: <monospaced procname>" *) (** Printer which outputs "Method call: <monospaced procname>" *)
module DefaultCallPrinter : CallPrinter
module type TraceElem = sig module type TraceElem = sig
type elem_t type elem_t
@ -33,8 +33,8 @@ module type TraceElem = sig
(** An [elem] which occured at [loc], after the chain of steps (usually calls) in [trace]. *) (** An [elem] which occured at [loc], after the chain of steps (usually calls) in [trace]. *)
type t = private {elem: elem_t; loc: Location.t; trace: CallSite.t list} type t = private {elem: elem_t; loc: Location.t; trace: CallSite.t list}
include Element with type t := t
(** Both [pp] and [describe] simply call the same function on the trace element. *) (** Both [pp] and [describe] simply call the same function on the trace element. *)
include Element with type t := t
val make : elem_t -> Location.t -> t val make : elem_t -> Location.t -> t
@ -48,8 +48,8 @@ module type TraceElem = sig
val with_callsite : t -> CallSite.t -> t val with_callsite : t -> CallSite.t -> t
(** Push given callsite onto trace, extending the call chain by one. *) (** Push given callsite onto trace, extending the call chain by one. *)
module FiniteSet : FiniteSet with type elt = t
(** A powerset of traces. *) (** A powerset of traces. *)
module FiniteSet : FiniteSet with type elt = t
end end
(* The [compare] function produced ignores traces but *not* locations *) (* The [compare] function produced ignores traces but *not* locations *)

@ -23,20 +23,20 @@ end
module type S = sig module type S = sig
include Spec include Spec
include AbstractDomain.WithBottom
(** bottom = this trace has no source or sink data *) (** bottom = this trace has no source or sink data *)
include AbstractDomain.WithBottom
module Sources : sig module Sources : sig
module Known : module type of AbstractDomain.FiniteSet (Source)
(** Set of sources returned by callees of the current function *) (** Set of sources returned by callees of the current function *)
module Known : module type of AbstractDomain.FiniteSet (Source)
module FootprintConfig : AccessTree.Config module FootprintConfig : AccessTree.Config
module Footprint : module type of AccessTree.PathSet (FootprintConfig)
(** Set of access paths representing the sources that may flow in from the caller *) (** Set of access paths representing the sources that may flow in from the caller *)
module Footprint : module type of AccessTree.PathSet (FootprintConfig)
module Sanitizers : module type of AbstractDomain.FiniteSet (Sanitizer)
(** Set of sanitizers that have been applied to these sources *) (** Set of sanitizers that have been applied to these sources *)
module Sanitizers : module type of AbstractDomain.FiniteSet (Sanitizer)
type t = {known: Known.t; footprint: Footprint.t; sanitizers: Sanitizers.t} type t = {known: Known.t; footprint: Footprint.t; sanitizers: Sanitizers.t}

@ -6,8 +6,8 @@
*) *)
open! IStd open! IStd
exception ProcnameAlreadyLocked of Procname.t
(** for the Restart scheduler: raise when a worker tries to analyze a procedure already being (** for the Restart scheduler: raise when a worker tries to analyze a procedure already being
analyzed by another process *) analyzed by another process *)
exception ProcnameAlreadyLocked of Procname.t
type target = Procname of Procname.t | File of SourceFile.t type target = Procname of Procname.t | File of SourceFile.t

@ -13,8 +13,8 @@ open! IStd
module type S = sig module type S = sig
module CFG : ProcCfg.S module CFG : ProcCfg.S
module Domain : AbstractDomain.S
(** abstract domain whose state we propagate *) (** abstract domain whose state we propagate *)
module Domain : AbstractDomain.S
(** read-only extra state (results of previous analyses, globals, etc.) *) (** read-only extra state (results of previous analyses, globals, etc.) *)
type analysis_data type analysis_data

@ -7,13 +7,13 @@
open! IStd open! IStd
exception ALParserInvariantViolationException of string
(** Raised when the parser encounters a violation of a certain invariant *) (** Raised when the parser encounters a violation of a certain invariant *)
exception ALParserInvariantViolationException of string
type exc_info type exc_info
exception ALFileException of exc_info
(** Raised when any exception from the lexer/parser of AL is caught, to include source-location info *) (** Raised when any exception from the lexer/parser of AL is caught, to include source-location info *)
exception ALFileException of exc_info
val create_exc_info : string -> Lexing.lexbuf -> exc_info val create_exc_info : string -> Lexing.lexbuf -> exc_info

@ -231,13 +231,11 @@ let rec is_node_successor_of ~is_successor:succ_node node =
| Stmt _ -> | Stmt _ ->
let node_succ_stmts = get_successor_stmts node in let node_succ_stmts = get_successor_stmts node in
List.exists node_succ_stmts ~f:(fun (s : Clang_ast_t.stmt) -> List.exists node_succ_stmts ~f:(fun (s : Clang_ast_t.stmt) ->
ast_node_equal (Stmt s) succ_node || is_node_successor_of ~is_successor:succ_node (Stmt s) ast_node_equal (Stmt s) succ_node || is_node_successor_of ~is_successor:succ_node (Stmt s) )
)
| Decl _ -> | Decl _ ->
let node_succ_decls = get_successor_decls node in let node_succ_decls = get_successor_decls node in
List.exists node_succ_decls ~f:(fun (d : Clang_ast_t.decl) -> List.exists node_succ_decls ~f:(fun (d : Clang_ast_t.decl) ->
ast_node_equal (Decl d) succ_node || is_node_successor_of ~is_successor:succ_node (Decl d) ast_node_equal (Decl d) succ_node || is_node_successor_of ~is_successor:succ_node (Decl d) )
)
let get_direct_successor_nodes an = let get_direct_successor_nodes an =

@ -55,8 +55,7 @@ let fields =
let pp pe f payloads = let pp pe f payloads =
List.iter fields ~f:(fun (F {field; name; pp}) -> List.iter fields ~f:(fun (F {field; name; pp}) ->
Field.get field payloads |> Option.iter ~f:(fun x -> F.fprintf f "%s: %a@\n" name (pp pe) x) Field.get field payloads |> Option.iter ~f:(fun x -> F.fprintf f "%s: %a@\n" name (pp pe) x) )
)
let empty = let empty =

@ -156,8 +156,8 @@ module Liveness = struct
instructions for each pvar in to_nullify afer we finish the analysis. Nullify instructions instructions for each pvar in to_nullify afer we finish the analysis. Nullify instructions
speed up the analysis by enabling it to GC state that will no longer be read. *) speed up the analysis by enabling it to GC state that will no longer be read. *)
module NullifyTransferFunctions = struct module NullifyTransferFunctions = struct
module Domain = AbstractDomain.Pair (VarDomain) (VarDomain)
(** (reaching non-nullified vars) * (vars to nullify) *) (** (reaching non-nullified vars) * (vars to nullify) *)
module Domain = AbstractDomain.Pair (VarDomain) (VarDomain)
module CFG = ProcCfg.Exceptional module CFG = ProcCfg.Exceptional

@ -592,7 +592,7 @@ let normalize_path_in_args_being_parsed ?(f = Fn.id) ~is_anon_arg str =
[Arg.parse_argv_dynamic ~current:arg_being_parsed !args_to_parse ...]. *) [Arg.parse_argv_dynamic ~current:arg_being_parsed !args_to_parse ...]. *)
let root = Unix.getcwd () in let root = Unix.getcwd () in
let abs_path = Utils.filename_to_absolute ~root str in let abs_path = Utils.filename_to_absolute ~root str in
!args_to_parse.((!arg_being_parsed + if is_anon_arg then 0 else 1)) <- f abs_path ; !args_to_parse.(!arg_being_parsed + if is_anon_arg then 0 else 1) <- f abs_path ;
abs_path ) abs_path )
else str else str

@ -16,8 +16,8 @@ exception InferInternalError of string
exception InferUserError of string exception InferUserError of string
exception InferExit of int
(** This can be used to avoid scattering exit invocations all over the codebase *) (** This can be used to avoid scattering exit invocations all over the codebase *)
exception InferExit of int
(** kind of error for [die], with similar semantics as [Logging.{external,internal,user}_error] *) (** kind of error for [die], with similar semantics as [Logging.{external,internal,user}_error] *)
type error = ExternalError | InternalError | UserError type error = ExternalError | InternalError | UserError

@ -134,8 +134,7 @@ let create_results_dir () =
L.progress "Deleting results dir because --force-delete-results-dir was passed@." ; L.progress "Deleting results dir because --force-delete-results-dir was passed@." ;
remove_results_dir () ) remove_results_dir () )
else else
L.die UserError "ERROR: %s@\nPlease remove '%s' and try again" error Config.results_dir L.die UserError "ERROR: %s@\nPlease remove '%s' and try again" error Config.results_dir ) ;
) ;
Unix.mkdir_p Config.results_dir ; Unix.mkdir_p Config.results_dir ;
Unix.mkdir_p (get_path Temporary) ; Unix.mkdir_p (get_path Temporary) ;
Unix.mkdir_p (get_path Specs) ; Unix.mkdir_p (get_path Specs) ;

@ -9,11 +9,11 @@ open! IStd
type t [@@deriving compare] type t [@@deriving compare]
module Map : Caml.Map.S with type key = t
(** Maps from source_file *) (** Maps from source_file *)
module Map : Caml.Map.S with type key = t
module Set : Caml.Set.S with type elt = t
(** Set of source files *) (** Set of source files *)
module Set : Caml.Set.S with type elt = t
module Hash : Caml.Hashtbl.S with type key = t module Hash : Caml.Hashtbl.S with type key = t

@ -7,9 +7,9 @@
open! IStd open! IStd
exception Error of string
(** The functions in this module tend to raise more often than their counterparts in [Sqlite3]. In (** The functions in this module tend to raise more often than their counterparts in [Sqlite3]. In
particular, they may raise if the [Sqlite3.Rc.t] result of certain operations is unexpected. *) particular, they may raise if the [Sqlite3.Rc.t] result of certain operations is unexpected. *)
exception Error of string
val check_result_code : Sqlite3.db -> log:string -> Sqlite3.Rc.t -> unit val check_result_code : Sqlite3.db -> log:string -> Sqlite3.Rc.t -> unit
(** Assert that the result is either [Sqlite3.Rc.OK] or [Sqlite3.Rc.ROW]. If the result is not (** Assert that the result is either [Sqlite3.Rc.OK] or [Sqlite3.Rc.ROW]. If the result is not

@ -17,8 +17,8 @@ type failure_kind =
| FKrecursion_timeout of int (** max recursion level exceeded *) | FKrecursion_timeout of int (** max recursion level exceeded *)
| FKcrash of string (** uncaught exception or failed assertion *) | FKcrash of string (** uncaught exception or failed assertion *)
exception Analysis_failure_exe of failure_kind
(** failure that prevented analysis from finishing *) (** failure that prevented analysis from finishing *)
exception Analysis_failure_exe of failure_kind
let exn_not_failure = function Analysis_failure_exe _ -> false | _ -> true let exn_not_failure = function Analysis_failure_exe _ -> false | _ -> true

@ -59,8 +59,8 @@ type failure_kind =
| FKrecursion_timeout of int (** max recursion level exceeded *) | FKrecursion_timeout of int (** max recursion level exceeded *)
| FKcrash of string (** uncaught exception or failed assertion *) | FKcrash of string (** uncaught exception or failed assertion *)
exception Analysis_failure_exe of failure_kind
(** Timeout exception *) (** Timeout exception *)
exception Analysis_failure_exe of failure_kind
val exn_not_failure : exn -> bool val exn_not_failure : exn -> bool
(** check that the exception is not a timeout exception *) (** check that the exception is not a timeout exception *)

@ -44,8 +44,8 @@ module Jprop : sig
(** Extract the toplevel jprop of a prop *) (** Extract the toplevel jprop of a prop *)
end end
module Visitedset : Caml.Set.S with type elt = Procdesc.Node.id * int list
(** set of visited nodes: node id and list of lines of all the instructions *) (** set of visited nodes: node id and list of lines of all the instructions *)
module Visitedset : Caml.Set.S with type elt = Procdesc.Node.id * int list
(** A spec consists of: (** A spec consists of:

@ -7,8 +7,8 @@
open! IStd open! IStd
include BUILTINS.S with type t = Builtin.registered
(** Models for the builtin functions supported *) (** Models for the builtin functions supported *)
include BUILTINS.S with type t = Builtin.registered
val init : unit -> unit val init : unit -> unit
(** Clients of Builtin module should call this before Builtin module is used. WARNING: builtins are (** Clients of Builtin module should call this before Builtin module is used. WARNING: builtins are

@ -161,8 +161,8 @@ val equal_hpred : ?inst:bool -> hpred -> hpred -> bool
(** Equality function for hpred. The inst:: parameter specifies whether instumentations should also (** Equality function for hpred. The inst:: parameter specifies whether instumentations should also
be considered (false by default). *) be considered (false by default). *)
module HpredSet : Caml.Set.S with type elt = hpred
(** Sets of heap predicates *) (** Sets of heap predicates *)
module HpredSet : Caml.Set.S with type elt = hpred
(** {2 Compaction} *) (** {2 Compaction} *)

@ -19,8 +19,8 @@ type retain_cycle_edge = Object of retain_cycle_edge_obj | Block of Procname.t *
to model the cycle structure. The next element from the end of the list is the head. *) to model the cycle structure. The next element from the end of the list is the head. *)
type t = {rc_head: retain_cycle_edge; rc_elements: retain_cycle_edge list} type t = {rc_head: retain_cycle_edge; rc_elements: retain_cycle_edge list}
module Set : Caml.Set.S with type elt = t
(** Set for retain cycles. *) (** Set for retain cycles. *)
module Set : Caml.Set.S with type elt = t
val d_retain_cycle : t -> unit val d_retain_cycle : t -> unit

@ -8,8 +8,8 @@
open! IStd open! IStd
open AbstractDomain.Types open AbstractDomain.Types
module ItvThresholds : AbstractDomain.FiniteSetS with type elt = Z.t
(** Set of integers for threshold widening *) (** Set of integers for threshold widening *)
module ItvThresholds : AbstractDomain.FiniteSetS with type elt = Z.t
(** Domain for recording which operations are used for evaluating interval values *) (** Domain for recording which operations are used for evaluating interval values *)
module ItvUpdatedBy : sig module ItvUpdatedBy : sig

@ -627,7 +627,8 @@ module StdVector = struct
let set_size {location} locs new_size mem = let set_size {location} locs new_size mem =
Dom.Mem.transform_mem locs mem ~f:(fun v -> Dom.Val.set_array_length location ~length:new_size v) Dom.Mem.transform_mem locs mem ~f:(fun v ->
Dom.Val.set_array_length location ~length:new_size v )
let empty elt_typ vec_arg = let empty elt_typ vec_arg =

@ -305,8 +305,8 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
(fun symbol polynomial acc -> (fun symbol polynomial acc ->
Option.bind acc ~f:(fun acc -> Option.bind acc ~f:(fun acc ->
Option.bind (S.int_ub symbol) ~f:(fun s_ub -> Option.bind (S.int_ub symbol) ~f:(fun s_ub ->
Option.map (int_ub polynomial) ~f:(fun p_ub -> NonNegativeInt.((s_ub * p_ub) + acc)) Option.map (int_ub polynomial) ~f:(fun p_ub -> NonNegativeInt.((s_ub * p_ub) + acc)) ) )
) ) ) )
terms (Some const) terms (Some const)
@ -315,7 +315,8 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
fun ~lhs ~rhs -> fun ~lhs ~rhs ->
phys_equal lhs rhs phys_equal lhs rhs
|| (NonNegativeInt.leq ~lhs:lhs.const ~rhs:rhs.const && M.le ~le_elt:leq lhs.terms rhs.terms) || (NonNegativeInt.leq ~lhs:lhs.const ~rhs:rhs.const && M.le ~le_elt:leq lhs.terms rhs.terms)
|| Option.exists (int_ub lhs) ~f:(fun lhs_ub -> NonNegativeInt.leq ~lhs:lhs_ub ~rhs:(int_lb rhs)) || Option.exists (int_ub lhs) ~f:(fun lhs_ub ->
NonNegativeInt.leq ~lhs:lhs_ub ~rhs:(int_lb rhs) )
let rec xcompare ~lhs ~rhs = let rec xcompare ~lhs ~rhs =

@ -138,8 +138,8 @@ module Created = struct
end end
module MethodCalls = struct module MethodCalls = struct
module IsChecked = AbstractDomain.BooleanOr
(** if the method calls are checked and reported *) (** if the method calls are checked and reported *)
module IsChecked = AbstractDomain.BooleanOr
module S = AbstractDomain.InvertedSet (MethodCallPrefix) module S = AbstractDomain.InvertedSet (MethodCallPrefix)

@ -87,7 +87,8 @@ let exec_call analysis_data callee args loc astate =
load_type analysis_data loc typ astate load_type analysis_data loc typ astate
| _ -> | _ ->
(* invokeinterface / invokespecial / invokestatic / invokevirtual / new *) (* invokeinterface / invokespecial / invokestatic / invokevirtual / new *)
List.fold args ~init:astate ~f:(fun acc (exp, _) -> add_loads_of_exp analysis_data loc exp acc) List.fold args ~init:astate ~f:(fun acc (exp, _) ->
add_loads_of_exp analysis_data loc exp acc )
|> do_call analysis_data callee loc |> do_call analysis_data callee loc

@ -35,17 +35,17 @@ end
module ControlDepSet = AbstractDomain.FiniteSet (CVar) module ControlDepSet = AbstractDomain.FiniteSet (CVar)
module ControlMap = PrettyPrintable.MakePPMap (Var)
(** Map control var -> loop head location *) (** Map control var -> loop head location *)
module ControlMap = PrettyPrintable.MakePPMap (Var)
module GuardNodes = AbstractDomain.FiniteSet (Procdesc.Node) module GuardNodes = AbstractDomain.FiniteSet (Procdesc.Node)
module LoopHeads = Procdesc.NodeSet module LoopHeads = Procdesc.NodeSet
module ExitNodeToLoopHeads = Procdesc.NodeMap
(** Map exit node -> loop head set *) (** Map exit node -> loop head set *)
module ExitNodeToLoopHeads = Procdesc.NodeMap
module LoopHeadToGuardNodes = Procdesc.NodeMap
(** Map loop head -> prune nodes in the loop guard *) (** Map loop head -> prune nodes in the loop guard *)
module LoopHeadToGuardNodes = Procdesc.NodeMap
type loop_control_maps = type loop_control_maps =
{ exit_map: LoopHeads.t ExitNodeToLoopHeads.t { exit_map: LoopHeads.t ExitNodeToLoopHeads.t

@ -9,16 +9,16 @@ open! IStd
module LoopHead = Procdesc.Node module LoopHead = Procdesc.Node
module LoopHeads = Procdesc.NodeSet module LoopHeads = Procdesc.NodeSet
module ControlMap : module type of PrettyPrintable.MakePPMap (Var)
(** Map control var -> loop head location *) (** Map control var -> loop head location *)
module ControlMap : module type of PrettyPrintable.MakePPMap (Var)
module GuardNodes : module type of AbstractDomain.FiniteSet (Procdesc.Node) module GuardNodes : module type of AbstractDomain.FiniteSet (Procdesc.Node)
module ExitNodeToLoopHeads = Procdesc.NodeMap
(** Map exit node -> loop head set *) (** Map exit node -> loop head set *)
module ExitNodeToLoopHeads = Procdesc.NodeMap
module LoopHeadToGuardNodes = Procdesc.NodeMap
(** Map loop head -> prune nodes in the loop guard *) (** Map loop head -> prune nodes in the loop guard *)
module LoopHeadToGuardNodes = Procdesc.NodeMap
type invariant_map type invariant_map

@ -14,8 +14,8 @@ module VarSet = AbstractDomain.FiniteSet (Var)
let debug fmt = L.(debug Analysis Medium) fmt let debug fmt = L.(debug Analysis Medium) fmt
module LoopHeadToLoopNodes = Procdesc.NodeMap
(** Map loop header node -> all nodes in the loop *) (** Map loop header node -> all nodes in the loop *)
module LoopHeadToLoopNodes = Procdesc.NodeMap
let is_defined_outside loop_nodes reaching_defs var = let is_defined_outside loop_nodes reaching_defs var =
ReachingDefs.ReachingDefsMap.find_opt var reaching_defs ReachingDefs.ReachingDefsMap.find_opt var reaching_defs
@ -260,8 +260,8 @@ let get_inv_vars_in_loop tenv reaching_defs_invariant_map ~is_pure_by_default ~g
find_fixpoint InvariantVars.empty find_fixpoint InvariantVars.empty
module LoopHeadToInvVars = Procdesc.NodeMap
(** Map loop head -> invariant vars in loop *) (** Map loop head -> invariant vars in loop *)
module LoopHeadToInvVars = Procdesc.NodeMap
type invariant_map = VarSet.t LoopHeadToInvVars.t type invariant_map = VarSet.t LoopHeadToInvVars.t

@ -15,11 +15,11 @@ module LoopNodes : module type of AbstractDomain.FiniteSet (Procdesc.Node)
module VarSet : module type of AbstractDomain.FiniteSet (Var) module VarSet : module type of AbstractDomain.FiniteSet (Var)
module LoopHeadToLoopNodes = Procdesc.NodeMap
(** Map loop header node -> all nodes in the loop *) (** Map loop header node -> all nodes in the loop *)
module LoopHeadToLoopNodes = Procdesc.NodeMap
module LoopHeadToInvVars = Procdesc.NodeMap
(** Map loop head -> invariant vars in loop *) (** Map loop head -> invariant vars in loop *)
module LoopHeadToInvVars = Procdesc.NodeMap
type invariant_map = VarsInLoop.t Procdesc.NodeMap.t type invariant_map = VarsInLoop.t Procdesc.NodeMap.t

@ -8,16 +8,16 @@ open! IStd
module F = Format module F = Format
module NodeCFG = ProcCfg.Normal module NodeCFG = ProcCfg.Normal
module Defs = AbstractDomain.FiniteSet (Procdesc.Node)
(** The node in which the reaching definition x := e is defined. (** The node in which the reaching definition x := e is defined.
A definition x :=e, declared at node N, reaches the current node if there is a path from node N A definition x :=e, declared at node N, reaches the current node if there is a path from node N
to the current node such that x is not modified along the path **) to the current node such that x is not modified along the path **)
module Defs = AbstractDomain.FiniteSet (Procdesc.Node)
(* even though we only add singletons (defs), the set is needed for joins *) (* even though we only add singletons (defs), the set is needed for joins *)
module ReachingDefsMap = AbstractDomain.Map (Var) (Defs)
(** Map var -> its reaching definition *) (** Map var -> its reaching definition *)
module ReachingDefsMap = AbstractDomain.Map (Var) (Defs)
(* forward transfer function for reaching definitions *) (* forward transfer function for reaching definitions *)
module TransferFunctionsReachingDefs (CFG : ProcCfg.S) = struct module TransferFunctionsReachingDefs (CFG : ProcCfg.S) = struct

@ -7,14 +7,14 @@
open! IStd open! IStd
module Defs : module type of AbstractDomain.FiniteSet (Procdesc.Node)
(** The node in which the reaching definition x := e is defined. (** The node in which the reaching definition x := e is defined.
A definition x :=e, declared at node N, reaches the current node if there is a path from node N A definition x :=e, declared at node N, reaches the current node if there is a path from node N
to the current node such that x is not modified along the path **) to the current node such that x is not modified along the path **)
module Defs : module type of AbstractDomain.FiniteSet (Procdesc.Node)
module ReachingDefsMap : module type of AbstractDomain.Map (Var) (Defs)
(** Map var -> its reaching definition *) (** Map var -> its reaching definition *)
module ReachingDefsMap : module type of AbstractDomain.Map (Var) (Defs)
type invariant_map type invariant_map

@ -8,8 +8,8 @@
open! IStd open! IStd
module F = Format module F = Format
module D = UninitDomain.Domain
(** Forward analysis to compute uninitialized variables at each program point *) (** Forward analysis to compute uninitialized variables at each program point *)
module D = UninitDomain.Domain
module MaybeUninitVars = UninitDomain.MaybeUninitVars module MaybeUninitVars = UninitDomain.MaybeUninitVars
module AliasedVars = AbstractDomain.FiniteSet (UninitDomain.VarPair) module AliasedVars = AbstractDomain.FiniteSet (UninitDomain.VarPair)

@ -50,8 +50,7 @@ let do_source_file (translation_unit_context : CFrontend_config.translation_unit
L.(debug Capture Verbose) L.(debug Capture Verbose)
"@\n Start building call/cfg graph for '%a'....@\n" SourceFile.pp source_file ; "@\n Start building call/cfg graph for '%a'....@\n" SourceFile.pp source_file ;
let cfg = compute_icfg translation_unit_context tenv ast in let cfg = compute_icfg translation_unit_context tenv ast in
L.(debug Capture Verbose) L.(debug Capture Verbose) "@\n End building call/cfg graph for '%a'.@\n" SourceFile.pp source_file ;
"@\n End building call/cfg graph for '%a'.@\n" SourceFile.pp source_file ;
NullabilityPreanalysis.analysis cfg tenv ; NullabilityPreanalysis.analysis cfg tenv ;
SourceFiles.add source_file cfg (Tenv.FileLocal tenv) (Some integer_type_widths) ; SourceFiles.add source_file cfg (Tenv.FileLocal tenv) (Some integer_type_widths) ;
if Config.debug_mode then Tenv.store_debug_file_for_source source_file tenv ; if Config.debug_mode then Tenv.store_debug_file_for_source source_file tenv ;

@ -3217,8 +3217,8 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
let field_exp = Exp.Lfield (ret_exp, field_name, typ) in let field_exp = Exp.Lfield (ret_exp, field_name, typ) in
let args = let args =
type_info_objc :: (field_exp, void_typ) type_info_objc :: (field_exp, void_typ)
:: Option.value_map ~default:[] res_trans_subexpr ~f:(fun trans_result -> [trans_result.return] :: Option.value_map ~default:[] res_trans_subexpr ~f:(fun trans_result ->
) [trans_result.return] )
in in
let call_instr = Sil.Call ((ret_id, typ), sil_fun, args, sil_loc, CallFlags.default) in let call_instr = Sil.Call ((ret_id, typ), sil_fun, args, sil_loc, CallFlags.default) in
let res_control = {empty_control with instrs= [call_instr]} in let res_control = {empty_control with instrs= [call_instr]} in

@ -662,8 +662,8 @@ let acquire ?tenv ({lock_state; critical_pairs} as astate) ~procname ~loc locks
let event = Event.make_acquire lock in let event = Event.make_acquire lock in
add_critical_pair ?tenv lock_state event astate.thread ~loc acc ) add_critical_pair ?tenv lock_state event astate.thread ~loc acc )
; lock_state= ; lock_state=
List.fold locks ~init:lock_state ~f:(fun acc lock -> LockState.acquire ~procname ~loc lock acc) List.fold locks ~init:lock_state ~f:(fun acc lock ->
} LockState.acquire ~procname ~loc lock acc ) }
let make_call_with_event new_event ~loc astate = let make_call_with_event new_event ~loc astate =

@ -25,8 +25,8 @@ end
module LoopNodes = AbstractDomain.FiniteSet (Procdesc.Node) module LoopNodes = AbstractDomain.FiniteSet (Procdesc.Node)
module HoistCalls = AbstractDomain.FiniteSet (Call) module HoistCalls = AbstractDomain.FiniteSet (Call)
module LoopHeadToHoistInstrs = Procdesc.NodeMap
(** Map loop_header -> instrs that can be hoisted out of the loop *) (** Map loop_header -> instrs that can be hoisted out of the loop *)
module LoopHeadToHoistInstrs = Procdesc.NodeMap
(* A loop-invariant function call C(args) at node N can be hoisted out of the loop if (* A loop-invariant function call C(args) at node N can be hoisted out of the loop if
* *

@ -124,8 +124,7 @@ module CostsSummary = struct
let json_degrees = let json_degrees =
DegreeMap.bindings paired_counts.degrees DegreeMap.bindings paired_counts.degrees
|> List.map ~f:(fun (key, {current; previous}) -> |> List.map ~f:(fun (key, {current; previous}) ->
`Assoc [("degree", `Int key); ("current", `Int current); ("previous", `Int previous)] `Assoc [("degree", `Int key); ("current", `Int current); ("previous", `Int previous)] )
)
in in
let create_assoc current previous = let create_assoc current previous =
`Assoc [("current", `Int current); ("previous", `Int previous)] `Assoc [("current", `Int current); ("previous", `Int previous)]

@ -321,8 +321,7 @@ let process_all_summaries_and_issues ~issues_outf ~costs_outf =
!all_issues ; !all_issues ;
(* Issues that are generated and stored outside of summaries by linter and checkers *) (* Issues that are generated and stored outside of summaries by linter and checkers *)
List.iter (ResultsDirEntryName.get_issues_directories ()) ~f:(fun dir_name -> List.iter (ResultsDirEntryName.get_issues_directories ()) ~f:(fun dir_name ->
IssueLog.load dir_name |> IssueLog.iter ~f:(write_lint_issues filters issues_outf linereader) IssueLog.load dir_name |> IssueLog.iter ~f:(write_lint_issues filters issues_outf linereader) ) ;
) ;
() ()

@ -14,9 +14,9 @@ open Sawja_pack
instruction. *) instruction. *)
type jump_kind = Next | Jump of int | Exit type jump_kind = Next | Jump of int | Exit
module NodeTbl : Caml.Hashtbl.S with type key = Procdesc.Node.t
(** Hastable for storing nodes that correspond to if-instructions. These are used when adding the (** Hastable for storing nodes that correspond to if-instructions. These are used when adding the
edges in the contrl flow graph. *) edges in the contrl flow graph. *)
module NodeTbl : Caml.Hashtbl.S with type key = Procdesc.Node.t
(** data structure for saving the three structures tht contain the intermediate representation of a (** data structure for saving the three structures tht contain the intermediate representation of a
file: the type environment, the control graph and the control flow graph *) file: the type environment, the control graph and the control flow graph *)

@ -74,9 +74,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let pp_session_name _node fmt = F.pp_print_string fmt "resource leaks" let pp_session_name _node fmt = F.pp_print_string fmt "resource leaks"
end end
module CFG = ProcCfg.Normal
(** 5(a) Type of CFG to analyze--Exceptional to follow exceptional control-flow edges, Normal to (** 5(a) Type of CFG to analyze--Exceptional to follow exceptional control-flow edges, Normal to
ignore them *) ignore them *)
module CFG = ProcCfg.Normal
(* Create an intraprocedural abstract interpreter from the transfer functions we defined *) (* Create an intraprocedural abstract interpreter from the transfer functions we defined *)
module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG)) module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG))

@ -76,9 +76,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let pp_session_name _node fmt = F.pp_print_string fmt "resource leaks" let pp_session_name _node fmt = F.pp_print_string fmt "resource leaks"
end end
module CFG = ProcCfg.Normal
(** 5(a) Type of CFG to analyze--Exceptional to follow exceptional control-flow edges, Normal to (** 5(a) Type of CFG to analyze--Exceptional to follow exceptional control-flow edges, Normal to
ignore them *) ignore them *)
module CFG = ProcCfg.Normal
(* Create an intraprocedural abstract interpreter from the transfer functions we defined *) (* Create an intraprocedural abstract interpreter from the transfer functions we defined *)
module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG)) module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG))

@ -76,9 +76,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let pp_session_name _node fmt = F.pp_print_string fmt "resource leaks" let pp_session_name _node fmt = F.pp_print_string fmt "resource leaks"
end end
module CFG = ProcCfg.Normal
(** 5(a) Type of CFG to analyze--Exceptional to follow exceptional control-flow edges, Normal to (** 5(a) Type of CFG to analyze--Exceptional to follow exceptional control-flow edges, Normal to
ignore them *) ignore them *)
module CFG = ProcCfg.Normal
(* Create an intraprocedural abstract interpreter from the transfer functions we defined *) (* Create an intraprocedural abstract interpreter from the transfer functions we defined *)
module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG)) module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG))

@ -76,9 +76,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let pp_session_name _node fmt = F.pp_print_string fmt "resource leaks" let pp_session_name _node fmt = F.pp_print_string fmt "resource leaks"
end end
module CFG = ProcCfg.Normal
(** 5(a) Type of CFG to analyze--Exceptional to follow exceptional control-flow edges, Normal to (** 5(a) Type of CFG to analyze--Exceptional to follow exceptional control-flow edges, Normal to
ignore them *) ignore them *)
module CFG = ProcCfg.Normal
(* Create an intraprocedural abstract interpreter from the transfer functions we defined *) (* Create an intraprocedural abstract interpreter from the transfer functions we defined *)
module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG)) module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG))

@ -90,9 +90,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let pp_session_name _node fmt = F.pp_print_string fmt "resource leaks lab" let pp_session_name _node fmt = F.pp_print_string fmt "resource leaks lab"
end end
module CFG = ProcCfg.Normal
(** 5(a) Type of CFG to analyze--Exceptional to follow exceptional control-flow edges, Normal to (** 5(a) Type of CFG to analyze--Exceptional to follow exceptional control-flow edges, Normal to
ignore them *) ignore them *)
module CFG = ProcCfg.Normal
(* Create an intraprocedural abstract interpreter from the transfer functions we defined *) (* Create an intraprocedural abstract interpreter from the transfer functions we defined *)
module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG)) module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG))

@ -97,9 +97,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let pp_session_name _node fmt = F.pp_print_string fmt "resource leaks lab" let pp_session_name _node fmt = F.pp_print_string fmt "resource leaks lab"
end end
module CFG = ProcCfg.Normal
(** 5(a) Type of CFG to analyze--Exceptional to follow exceptional control-flow edges, Normal to (** 5(a) Type of CFG to analyze--Exceptional to follow exceptional control-flow edges, Normal to
ignore them *) ignore them *)
module CFG = ProcCfg.Normal
(* Create an intraprocedural abstract interpreter from the transfer functions we defined *) (* Create an intraprocedural abstract interpreter from the transfer functions we defined *)
module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG)) module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG))

@ -68,9 +68,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let pp_session_name _node fmt = F.pp_print_string fmt "resource leaks" let pp_session_name _node fmt = F.pp_print_string fmt "resource leaks"
end end
module CFG = ProcCfg.Normal
(** 5(a) Type of CFG to analyze--Exceptional to follow exceptional control-flow edges, Normal to (** 5(a) Type of CFG to analyze--Exceptional to follow exceptional control-flow edges, Normal to
ignore them *) ignore them *)
module CFG = ProcCfg.Normal
(* Create an intraprocedural abstract interpreter from the transfer functions we defined *) (* Create an intraprocedural abstract interpreter from the transfer functions we defined *)
module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG)) module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG))

@ -129,7 +129,6 @@ let final_constructor_typestates_lazy tenv curr_pname typecheck_proc =
lazy lazy
(let constructors_current_class = (let constructors_current_class =
pname_and_pdescs_with tenv curr_pname (fun (pname, _) -> pname_and_pdescs_with tenv curr_pname (fun (pname, _) ->
Procname.is_constructor pname && equal_class_opt (get_class pname) (get_class curr_pname) Procname.is_constructor pname && equal_class_opt (get_class pname) (get_class curr_pname) )
)
in in
final_typestates constructors_current_class tenv typecheck_proc ) final_typestates constructors_current_class tenv typecheck_proc )

@ -54,8 +54,7 @@ let assert_anonymous_equal actual expected_name_to_ids case_name =
actual actual
|> IOption.if_none_eval ~f:(fun () -> |> IOption.if_none_eval ~f:(fun () ->
assert_failure assert_failure
(F.sprintf "%s: Did not find anonymous class info for %s" case_name anonymous_name) (F.sprintf "%s: Did not find anonymous class info for %s" case_name anonymous_name) )
)
in in
assert_summaries_equal actual_summaries expected_summary_ids anonymous_name case_name ) assert_summaries_equal actual_summaries expected_summary_ids anonymous_name case_name )

@ -78,8 +78,9 @@ module PostDomain : BaseDomainSig = struct
end end
(* NOTE: [PreDomain] and [Domain] theoretically differ in that [PreDomain] should be the inverted lattice of [Domain], but since we never actually join states or check implication the two collapse into one. *) (* NOTE: [PreDomain] and [Domain] theoretically differ in that [PreDomain] should be the inverted lattice of [Domain], but since we never actually join states or check implication the two collapse into one. *)
module PreDomain : BaseDomainSig = PostDomain
(** represents the inferred pre-condition at each program point, biabduction style *) (** represents the inferred pre-condition at each program point, biabduction style *)
module PreDomain : BaseDomainSig = PostDomain
(** biabduction-style pre/post state + skipped calls *) (** biabduction-style pre/post state + skipped calls *)
type t = type t =

@ -41,15 +41,15 @@ module type BaseDomainSig = sig
val pp : F.formatter -> t -> unit val pp : F.formatter -> t -> unit
end end
module PostDomain : BaseDomainSig
(** The post abstract state at each program point, or current state. *) (** The post abstract state at each program point, or current state. *)
module PostDomain : BaseDomainSig
module PreDomain : BaseDomainSig
(** The inferred pre-condition at each program point, biabduction style. (** The inferred pre-condition at each program point, biabduction style.
NOTE: [PreDomain] and [Domain] theoretically differ in that [PreDomain] should be the inverted NOTE: [PreDomain] and [Domain] theoretically differ in that [PreDomain] should be the inverted
lattice of [Domain], but since we never actually join states or check implication the two lattice of [Domain], but since we never actually join states or check implication the two
collapse into one. * *) collapse into one. * *)
module PreDomain : BaseDomainSig
(** biabduction-style pre/post state + skipped calls *) (** biabduction-style pre/post state + skipped calls *)
type t = private type t = private

@ -8,15 +8,15 @@
open! IStd open! IStd
module ExecutionDomain = PulseExecutionDomain module ExecutionDomain = PulseExecutionDomain
module AbductiveDomain = PulseAbductiveDomain
(** if you do any mutations of the state in pulse you probably want this module *) (** if you do any mutations of the state in pulse you probably want this module *)
module AbductiveDomain = PulseAbductiveDomain
module Stack = AbductiveDomain.Stack module Stack = AbductiveDomain.Stack
module Memory = AbductiveDomain.Memory module Memory = AbductiveDomain.Memory
module AddressAttributes = AbductiveDomain.AddressAttributes module AddressAttributes = AbductiveDomain.AddressAttributes
module BaseDomain = PulseBaseDomain
(** use only if you know what you are doing or you risk break bi-abduction *) (** use only if you know what you are doing or you risk break bi-abduction *)
module BaseDomain = PulseBaseDomain
module BaseStack = PulseBaseStack module BaseStack = PulseBaseStack
module BaseMemory = PulseBaseMemory module BaseMemory = PulseBaseMemory

@ -20,8 +20,7 @@ let check_addr_access location (address, history) astate =
let access_trace = Trace.Immediate {location; history} in let access_trace = Trace.Immediate {location; history} in
AddressAttributes.check_valid access_trace address astate AddressAttributes.check_valid access_trace address astate
|> Result.map_error ~f:(fun (invalidation, invalidation_trace) -> |> Result.map_error ~f:(fun (invalidation, invalidation_trace) ->
(Diagnostic.AccessToInvalidAddress {invalidation; invalidation_trace; access_trace}, astate) (Diagnostic.AccessToInvalidAddress {invalidation; invalidation_trace; access_trace}, astate) )
)
module Closures = struct module Closures = struct
@ -46,8 +45,7 @@ module Closures = struct
let mk_capture_edges captured = let mk_capture_edges captured =
List.foldi captured ~init:Memory.Edges.empty ~f:(fun id edges captured_addr_trace -> List.foldi captured ~init:Memory.Edges.empty ~f:(fun id edges captured_addr_trace ->
Memory.Edges.add (HilExp.Access.FieldAccess (mk_fake_field ~id)) captured_addr_trace edges Memory.Edges.add (HilExp.Access.FieldAccess (mk_fake_field ~id)) captured_addr_trace edges )
)
let check_captured_addresses action lambda_addr (astate : t) = let check_captured_addresses action lambda_addr (astate : t) =

@ -294,8 +294,8 @@ let eval_unop unop_addr unop addr ({satisfiable; bo_itvs; citvs; pudge} as phi)
let prune_bo_with_bop ~negated v_opt arith bop arith' phi = let prune_bo_with_bop ~negated v_opt arith bop arith' phi =
match match
Option.both v_opt (if negated then Binop.negate bop else Some bop) Option.both v_opt (if negated then Binop.negate bop else Some bop)
|> Option.map ~f:(fun (v, positive_bop) -> (v, Itv.ItvPure.prune_binop positive_bop arith arith') |> Option.map ~f:(fun (v, positive_bop) ->
) (v, Itv.ItvPure.prune_binop positive_bop arith arith') )
with with
| None -> | None ->
phi phi

@ -471,8 +471,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
let trace, subtree = let trace, subtree =
Option.value ~default:TaintDomain.empty_node (TaintDomain.get_node access_path astate) Option.value ~default:TaintDomain.empty_node (TaintDomain.get_node access_path astate)
in in
TaintDomain.add_node access_path (TraceDomain.add_source source trace, subtree) astate TaintDomain.add_node access_path (TraceDomain.add_source source trace, subtree) astate )
)
else astate else astate

@ -54,5 +54,4 @@ let tests =
"LRUHashtble" "LRUHashtble"
>::: List.map inputs ~f:(fun (name, input, expected) -> >::: List.map inputs ~f:(fun (name, input, expected) ->
name name
>:: fun _ -> assert_equal (input () |> LRUHash.bindings |> List.sort ~compare) expected >:: fun _ -> assert_equal (input () |> LRUHash.bindings |> List.sort ~compare) expected )
)

@ -347,8 +347,7 @@ let classes r =
Subst.fold r.rep ~init:Term.Map.empty ~f:(fun ~key ~data cls -> Subst.fold r.rep ~init:Term.Map.empty ~f:(fun ~key ~data cls ->
match classify key with match classify key with
| Interpreted | Atomic -> add key data cls | Interpreted | Atomic -> add key data cls
| Uninterpreted -> add (Term.map ~f:(Subst.apply r.rep) key) data cls | Uninterpreted -> add (Term.map ~f:(Subst.apply r.rep) key) data cls )
)
let cls_of r e = let cls_of r e =
let e' = Subst.apply r.rep e in let e' = Subst.apply r.rep e in
@ -1004,8 +1003,7 @@ let solve_concat_extracts r us x (classes, subst, us_xs) =
Some trm Some trm
| _ -> rep_ito_us ) | _ -> rep_ito_us )
in in
Term.memory ~siz:(Term.agg_size_exn e) ~arr:rep_ito_us :: suffix Term.memory ~siz:(Term.agg_size_exn e) ~arr:rep_ito_us :: suffix ) )
) )
|> List.min_elt ~compare:[%compare: Term.t list] |> List.min_elt ~compare:[%compare: Term.t list]
with with
| Some extracts -> | Some extracts ->
@ -1130,8 +1128,7 @@ let wrap tmr f call =
report ~name ~elapsed ~aggregate ~count ; report ~name ~elapsed ~aggregate ~count ;
if Float.(elapsed > !dump_threshold) then ( if Float.(elapsed > !dump_threshold) then (
dump_threshold := 2. *. !dump_threshold ; dump_threshold := 2. *. !dump_threshold ;
Format.eprintf "@\n%a@\n@." Sexp.pp_hum (sexp_of_call (call ())) ) Format.eprintf "@\n%a@\n@." Sexp.pp_hum (sexp_of_call (call ())) ) ) ;
) ;
r r
in in
if not [%debug] then f () if not [%debug] then f ()

@ -750,8 +750,8 @@ let rec simplify_ us rev_xss q =
(starN (starN
( {q with us= Var.Set.union q.us q.xs; xs= emp.xs; djns= []} ( {q with us= Var.Set.union q.us q.xs; xs= emp.xs; djns= []}
:: List.map q.djns ~f:(fun djn -> :: List.map q.djns ~f:(fun djn ->
orN (List.map djn ~f:(fun sjn -> simplify_ us rev_xss sjn)) orN (List.map djn ~f:(fun sjn -> simplify_ us rev_xss sjn)) )
) )) ))
in in
(* try to solve equations in cong for variables in xss *) (* try to solve equations in cong for variables in xss *)
let subst = Equality.solve_for_vars (us :: List.rev rev_xss) q.cong in let subst = Equality.solve_for_vars (us :: List.rev rev_xss) q.cong in

@ -16,9 +16,9 @@ type op1 =
signed integer. That is, it two's-complement--decodes the low [n] signed integer. That is, it two's-complement--decodes the low [n]
bits of the infinite two's-complement encoding of [arg]. *) bits of the infinite two's-complement encoding of [arg]. *)
| Unsigned of {bits: int} | Unsigned of {bits: int}
(** [Ap1 (Unsigned {bits= n}, arg)] is [arg] interpreted as an (** [Ap1 (Unsigned {bits= n}, arg)] is [arg] interpreted as an [n]-bit
[n]-bit unsigned integer. That is, it unsigned-binary--decodes the unsigned integer. That is, it unsigned-binary--decodes the low [n]
low [n] bits of the infinite two's-complement encoding of [arg]. *) bits of the infinite two's-complement encoding of [arg]. *)
| Convert of {src: Typ.t; dst: Typ.t} | Convert of {src: Typ.t; dst: Typ.t}
(** [Ap1 (Convert {src; dst}, arg)] is [arg] converted from type [src] (** [Ap1 (Convert {src; dst}, arg)] is [arg] converted from type [src]
to type [dst], possibly with loss of information. The [src] and to type [dst], possibly with loss of information. The [src] and

Loading…
Cancel
Save