From 53702e43e8205db9172769a538a0f2405df52b6c Mon Sep 17 00:00:00 2001 From: Cristiano Calcagno Date: Mon, 28 Mar 2016 00:06:27 -0700 Subject: [PATCH] Created IR folder for the intermediate representaion files. Reviewed By: jberdine Differential Revision: D3102560 fb-gh-sync-id: 0a865a6 fbshipit-source-id: 0a865a6 --- configure.ac | 2 +- docker/README.md | 2 +- examples/{README => README.md} | 26 +- infer/src/IR/README.md | 12 + infer/src/{backend => IR}/attributesTable.ml | 0 infer/src/{backend => IR}/attributesTable.mli | 0 infer/src/{backend => IR}/cfg.ml | 0 infer/src/{backend => IR}/cfg.mli | 12 +- infer/src/{backend => IR}/cg.ml | 0 infer/src/{backend => IR}/cg.mli | 0 infer/src/{backend => IR}/csu.ml | 0 infer/src/{backend => IR}/csu.mli | 0 infer/src/{backend => IR}/ident.ml | 0 infer/src/{backend => IR}/ident.mli | 0 infer/src/{backend => IR}/location.ml | 0 infer/src/{backend => IR}/location.mli | 0 infer/src/{backend => IR}/mangled.ml | 0 infer/src/{backend => IR}/mangled.mli | 0 infer/src/{backend => IR}/procAttributes.ml | 0 infer/src/{backend => IR}/procAttributes.mli | 0 infer/src/{backend => IR}/procname.ml | 0 infer/src/{backend => IR}/procname.mli | 0 infer/src/{backend => IR}/sil.ml | 255 +++++++++--------- infer/src/{backend => IR}/sil.mli | 207 +++++++------- infer/src/IR/tenv.ml | 81 ++++++ infer/src/IR/tenv.mli | 42 +++ infer/src/{backend => IR}/typename.ml | 0 infer/src/{backend => IR}/typename.mli | 0 infer/src/Makefile.in | 21 +- infer/src/backend/PROFILE_HOWTO | 12 - infer/src/backend/README.md | 8 + infer/src/backend/abs.ml | 6 +- infer/src/backend/abs.mli | 10 +- infer/src/backend/builtin.ml | 2 +- infer/src/backend/builtin.mli | 2 +- infer/src/backend/callbacks.ml | 4 +- infer/src/backend/callbacks.mli | 4 +- infer/src/backend/dom.mli | 4 +- infer/src/backend/errdesc.ml | 2 +- infer/src/backend/errdesc.mli | 4 +- infer/src/backend/exe_env.ml | 6 +- infer/src/backend/exe_env.mli | 2 +- infer/src/backend/inferanalyze.ml | 13 +- infer/src/backend/inferprint.ml | 44 ++- infer/src/backend/preanal.mli | 2 +- infer/src/backend/prop.mli | 7 +- infer/src/backend/prover.ml | 12 +- infer/src/backend/prover.mli | 10 +- infer/src/backend/rearrange.mli | 2 +- infer/src/backend/state.ml | 5 +- infer/src/backend/state.mli | 7 +- infer/src/backend/symExec.ml | 196 +++++++++----- infer/src/backend/symExec.mli | 6 +- infer/src/backend/tabulation.mli | 2 +- infer/src/checkers/README.md | 9 + infer/src/checkers/callbackChecker.ml | 2 +- infer/src/checkers/constantPropagation.mli | 2 +- infer/src/checkers/dataflow.ml | 4 +- infer/src/checkers/dataflow.mli | 4 +- .../checkers/fragmentRetainsViewChecker.ml | 4 +- infer/src/checkers/patternMatch.ml | 14 +- infer/src/checkers/patternMatch.mli | 4 +- infer/src/clang/README.md | 5 + infer/src/clang/cContext.ml | 4 +- infer/src/clang/cContext.mli | 8 +- infer/src/clang/cField_decl.ml | 6 +- infer/src/clang/cField_decl.mli | 10 +- infer/src/clang/cFrontend.ml | 4 +- infer/src/clang/cFrontend_checkers.ml | 2 +- infer/src/clang/cFrontend_decl.ml | 68 ++--- infer/src/clang/cFrontend_decl.mli | 4 +- infer/src/clang/cFrontend_errors.mli | 2 +- infer/src/clang/cFrontend_utils.ml | 10 +- infer/src/clang/cFrontend_utils.mli | 12 +- infer/src/clang/cMethod_trans.ml | 2 +- infer/src/clang/cMethod_trans.mli | 12 +- infer/src/clang/cModule_type.ml | 4 +- infer/src/clang/cTrans.ml | 2 +- infer/src/clang/cTrans_utils.ml | 2 +- infer/src/clang/cTrans_utils.mli | 5 +- infer/src/clang/cType_to_sil_type.mli | 4 +- infer/src/clang/cTypes.ml | 2 +- infer/src/clang/cTypes.mli | 2 +- infer/src/clang/cTypes_decl.ml | 8 +- infer/src/clang/cTypes_decl.mli | 18 +- infer/src/clang/objcCategory_decl.ml | 4 +- infer/src/clang/objcCategory_decl.mli | 4 +- infer/src/clang/objcInterface_decl.ml | 12 +- infer/src/clang/objcInterface_decl.mli | 6 +- infer/src/clang/objcProtocol_decl.ml | 2 +- infer/src/clang/objcProtocol_decl.mli | 2 +- infer/src/eradicate/README.md | 5 + infer/src/eradicate/eradicate.ml | 3 +- infer/src/eradicate/typeCheck.mli | 2 +- infer/src/eradicate/typeState.ml | 2 +- infer/src/eradicate/typeState.mli | 2 +- infer/src/harness/androidFramework.ml | 8 +- infer/src/harness/androidFramework.mli | 33 +-- infer/src/harness/harness.ml | 2 +- infer/src/harness/harness.mli | 2 +- infer/src/harness/stacktrace.ml | 2 +- infer/src/java/README.md | 5 + infer/src/java/jClasspath.ml | 4 +- infer/src/java/jClasspath.mli | 2 +- infer/src/java/jContext.ml | 2 +- infer/src/java/jContext.mli | 4 +- infer/src/java/jFrontend.mli | 4 +- infer/src/java/jMain.ml | 15 +- infer/src/java/jTrans.mli | 6 +- infer/src/java/jTransType.ml | 10 +- infer/src/java/jTransType.mli | 20 +- infer/src/llvm/lMain.ml | 2 +- infer/src/llvm/lTrans.ml | 12 +- 113 files changed, 874 insertions(+), 574 deletions(-) rename examples/{README => README.md} (55%) create mode 100644 infer/src/IR/README.md rename infer/src/{backend => IR}/attributesTable.ml (100%) rename infer/src/{backend => IR}/attributesTable.mli (100%) rename infer/src/{backend => IR}/cfg.ml (100%) rename infer/src/{backend => IR}/cfg.mli (96%) rename infer/src/{backend => IR}/cg.ml (100%) rename infer/src/{backend => IR}/cg.mli (100%) rename infer/src/{backend => IR}/csu.ml (100%) rename infer/src/{backend => IR}/csu.mli (100%) rename infer/src/{backend => IR}/ident.ml (100%) rename infer/src/{backend => IR}/ident.mli (100%) rename infer/src/{backend => IR}/location.ml (100%) rename infer/src/{backend => IR}/location.mli (100%) rename infer/src/{backend => IR}/mangled.ml (100%) rename infer/src/{backend => IR}/mangled.mli (100%) rename infer/src/{backend => IR}/procAttributes.ml (100%) rename infer/src/{backend => IR}/procAttributes.mli (100%) rename infer/src/{backend => IR}/procname.ml (100%) rename infer/src/{backend => IR}/procname.mli (100%) rename infer/src/{backend => IR}/sil.ml (95%) rename infer/src/{backend => IR}/sil.mli (88%) create mode 100644 infer/src/IR/tenv.ml create mode 100644 infer/src/IR/tenv.mli rename infer/src/{backend => IR}/typename.ml (100%) rename infer/src/{backend => IR}/typename.mli (100%) delete mode 100644 infer/src/backend/PROFILE_HOWTO create mode 100644 infer/src/backend/README.md create mode 100644 infer/src/checkers/README.md create mode 100644 infer/src/clang/README.md create mode 100644 infer/src/eradicate/README.md create mode 100644 infer/src/java/README.md diff --git a/configure.ac b/configure.ac index e4390f58d..c85fa21fc 100644 --- a/configure.ac +++ b/configure.ac @@ -15,7 +15,7 @@ AC_PREREQ([2.63]) AC_INIT([Infer], [0.8.0], [https://github.com/facebook/infer/issues/]) -AC_CONFIG_SRCDIR([infer/src/backend/sil.ml]) +AC_CONFIG_SRCDIR([infer/src/IR/sil.ml]) # WARNING: keep in sync with above INFER_MAJOR=0 diff --git a/docker/README.md b/docker/README.md index 40d44d49a..0bb1e9148 100644 --- a/docker/README.md +++ b/docker/README.md @@ -1,6 +1,6 @@ # docker images for Infer -This directory, 'docker/' inside the Infer repo, +This directory, `docker/` inside the Infer repo, contains a docker file to install Infer within a [docker](https://www.docker.com/) container. This can be used to quickly try Infer or to deploy Infer. diff --git a/examples/README b/examples/README.md similarity index 55% rename from examples/README rename to examples/README.md index 1c45dc712..bb1952caa 100644 --- a/examples/README +++ b/examples/README.md @@ -4,30 +4,30 @@ one simple programming error that is caught by Infer. Contents -------- -- Hello.java: try this example by running - infer -- javac Hello.java +- `Hello.java`: try this example by running +```infer -- javac Hello.java ``` -- Hello.m: try this example by running - infer -- clang -c Hello.m +- `Hello.m`: try this example by running + ```infer -- clang -c Hello.m``` -- hello.c: try this example by running - infer -- gcc -c hello.c +- `hello.c`: try this example by running + ```infer -- gcc -c hello.c``` In this case, note that Infer captures the gcc command and runs clang instead to parse C files. Thus you may get compiler errors and warnings that differ from gcc's. -- android_hello/: a sample Android app. Try this example by running - infer -- ./gradlew build +- `android_hello/`: a sample Android app. Try this example by running + ```infer -- ./gradlew build``` Make sure that you have the Android SDK 22 installed and up to date, and in particular the "Android SDK Build-tools" and "Android Support Repository". -- c_hello/: a sample make-based C project. Try this example by running - infer -- make +- `c_hello/`: a sample make-based C project. Try this example by running + ```infer -- make``` -- ios_hello/: a sample iOS app. Try this example by running - infer -- xcodebuild -target HelloWorldApp -configuration Debug -sdk iphonesimulator +- `ios_hello/`: a sample iOS app. Try this example by running + ```infer -- xcodebuild -target HelloWorldApp -configuration Debug -sdk iphonesimulator``` - java_hello/: a sample Java project. Try this example by running infer -- javac Pointers.java Resources.java Hello.java @@ -37,5 +37,5 @@ Note The infer toplevel command must be in your PATH for the commands above to succeed. Otherwise, modify the commands to use the correct path to infer, eg - ../infer/bin/infer -- javac Hello.java + ```../infer/bin/infer -- javac Hello.java``` diff --git a/infer/src/IR/README.md b/infer/src/IR/README.md new file mode 100644 index 000000000..9636d7266 --- /dev/null +++ b/infer/src/IR/README.md @@ -0,0 +1,12 @@ +# Intermediate Representation + +The Intermediate Representation is a format used by the back-end for analysis. It is produced by one of the front-ends, one for each program analyzed. + +The main entry point is the intermediate language in [Sil](sil.mli). + +The control flow graph module is [Cfg](cfg.mli). + +The call graph module is [Cg](cg.mli). + +The type environment module is [Tenv](tenv.mli). + diff --git a/infer/src/backend/attributesTable.ml b/infer/src/IR/attributesTable.ml similarity index 100% rename from infer/src/backend/attributesTable.ml rename to infer/src/IR/attributesTable.ml diff --git a/infer/src/backend/attributesTable.mli b/infer/src/IR/attributesTable.mli similarity index 100% rename from infer/src/backend/attributesTable.mli rename to infer/src/IR/attributesTable.mli diff --git a/infer/src/backend/cfg.ml b/infer/src/IR/cfg.ml similarity index 100% rename from infer/src/backend/cfg.ml rename to infer/src/IR/cfg.ml diff --git a/infer/src/backend/cfg.mli b/infer/src/IR/cfg.mli similarity index 96% rename from infer/src/backend/cfg.mli rename to infer/src/IR/cfg.mli index 48264480e..b6461ec94 100644 --- a/infer/src/backend/cfg.mli +++ b/infer/src/IR/cfg.mli @@ -32,7 +32,8 @@ module Procdesc : sig (** Create a procdesc *) val create : cfg -> ProcAttributes.t -> t - (** [remove cfg name remove_nodes] remove the procdesc [name] from the control flow graph [cfg]. *) + (** [remove cfg name remove_nodes] remove the procdesc [name] + from the control flow graph [cfg]. *) (** It also removes all the nodes from the procedure from the cfg if remove_nodes is true *) val remove: cfg -> Procname.t -> bool -> unit @@ -145,7 +146,8 @@ module Node : sig (** Append the instructions and temporaries to the list of instructions to execute *) val append_instrs_temps : t -> Sil.instr list -> Ident.t list -> unit - (** Add the instructions and temporaries at the beginning of the list of instructions to execute *) + (** Add the instructions and temporaries at the beginning + of the list of instructions to execute *) val prepend_instrs_temps : t -> Sil.instr list -> Ident.t list -> unit (** Add declarations for local variables and return variable to the node *) @@ -174,7 +176,8 @@ module Node : sig (** Get all the nodes *) val get_all_nodes : cfg -> t list - (** Get the (after/before) dead program variables. After/before indicated with the true/false flag. *) + (** Get the (after/before) dead program variables. + After/before indicated with the true/false flag. *) val get_dead_pvars: t -> bool -> Sil.pvar list (** Get the distance to the exit node, if it has been computed *) @@ -201,7 +204,8 @@ module Node : sig (** Get the predecessor nodes of the current node *) val get_preds : t -> t list - (** Get a list of unique nodes until the first branch starting from a node with subsequent applications of a generator function *) + (** Get a list of unique nodes until the first branch starting + from a node with subsequent applications of a generator function *) val get_generated_slope : t -> (t -> t list) -> t list (** Get the proc desc associated to the node *) diff --git a/infer/src/backend/cg.ml b/infer/src/IR/cg.ml similarity index 100% rename from infer/src/backend/cg.ml rename to infer/src/IR/cg.ml diff --git a/infer/src/backend/cg.mli b/infer/src/IR/cg.mli similarity index 100% rename from infer/src/backend/cg.mli rename to infer/src/IR/cg.mli diff --git a/infer/src/backend/csu.ml b/infer/src/IR/csu.ml similarity index 100% rename from infer/src/backend/csu.ml rename to infer/src/IR/csu.ml diff --git a/infer/src/backend/csu.mli b/infer/src/IR/csu.mli similarity index 100% rename from infer/src/backend/csu.mli rename to infer/src/IR/csu.mli diff --git a/infer/src/backend/ident.ml b/infer/src/IR/ident.ml similarity index 100% rename from infer/src/backend/ident.ml rename to infer/src/IR/ident.ml diff --git a/infer/src/backend/ident.mli b/infer/src/IR/ident.mli similarity index 100% rename from infer/src/backend/ident.mli rename to infer/src/IR/ident.mli diff --git a/infer/src/backend/location.ml b/infer/src/IR/location.ml similarity index 100% rename from infer/src/backend/location.ml rename to infer/src/IR/location.ml diff --git a/infer/src/backend/location.mli b/infer/src/IR/location.mli similarity index 100% rename from infer/src/backend/location.mli rename to infer/src/IR/location.mli diff --git a/infer/src/backend/mangled.ml b/infer/src/IR/mangled.ml similarity index 100% rename from infer/src/backend/mangled.ml rename to infer/src/IR/mangled.ml diff --git a/infer/src/backend/mangled.mli b/infer/src/IR/mangled.mli similarity index 100% rename from infer/src/backend/mangled.mli rename to infer/src/IR/mangled.mli diff --git a/infer/src/backend/procAttributes.ml b/infer/src/IR/procAttributes.ml similarity index 100% rename from infer/src/backend/procAttributes.ml rename to infer/src/IR/procAttributes.ml diff --git a/infer/src/backend/procAttributes.mli b/infer/src/IR/procAttributes.mli similarity index 100% rename from infer/src/backend/procAttributes.mli rename to infer/src/IR/procAttributes.mli diff --git a/infer/src/backend/procname.ml b/infer/src/IR/procname.ml similarity index 100% rename from infer/src/backend/procname.ml rename to infer/src/IR/procname.ml diff --git a/infer/src/backend/procname.mli b/infer/src/IR/procname.mli similarity index 100% rename from infer/src/backend/procname.mli rename to infer/src/IR/procname.mli diff --git a/infer/src/backend/sil.ml b/infer/src/IR/sil.ml similarity index 95% rename from infer/src/backend/sil.ml rename to infer/src/IR/sil.ml index ef2df7c30..488211d52 100644 --- a/infer/src/backend/sil.ml +++ b/infer/src/IR/sil.ml @@ -174,9 +174,15 @@ type res_act_kind = (** kind of dangling pointers *) type dangling_kind = - | DAuninit (** pointer is dangling because it is uninitialized *) - | DAaddr_stack_var (** pointer is dangling because it is the address of a stack variable which went out of scope *) - | DAminusone (** pointer is -1 *) + (** pointer is dangling because it is uninitialized *) + | DAuninit + + (** pointer is dangling because it is the address + of a stack variable which went out of scope *) + | DAaddr_stack_var + + (** pointer is -1 *) + | DAminusone (** kind of pointer *) type ptr_kind = @@ -392,7 +398,8 @@ module Subtype = struct if (is_sub) then (Some st1, None) else let l1' = updates_head f c2 l1 in - if (is_subtype f c2 l1) then (Some (Subtypes l1'), Some (Subtypes (add_not_subtype f c1 l1 [c2]))) + if (is_subtype f c2 l1) + then (Some (Subtypes l1'), Some (Subtypes (add_not_subtype f c1 l1 [c2]))) else (None, Some st1) | Subtypes l1, Subtypes l2 -> if (is_interface c2) || (is_sub) then @@ -402,7 +409,8 @@ module Subtype = struct else (None, Some st1) else if ((is_interface c1) || (f c2 c1)) && (is_subtype f c2 l1) then let l1' = updates_head f c2 l1 in - (Some (Subtypes (add_not_subtype f c2 l1' l2)), Some (Subtypes (add_not_subtype f c1 l1 [c2]))) + (Some (Subtypes (add_not_subtype f c2 l1' l2)), + Some (Subtypes (add_not_subtype f c1 l1 [c2]))) else (None, Some st1) in (normalize_subtypes pos_st c1 c2 flag1 flag2), (normalize_subtypes neg_st c1 c2 flag1 flag2) @@ -422,11 +430,13 @@ module Subtype = struct else (None, Some st) in (change_flag pos_st c1 c2 flag2), (change_flag neg_st c1 c2 flag2) - (** [case_analysis (c1, st1) (c2,st2) f] performs case analysis on [c1 <: c2] according to [st1] and [st2] + (** [case_analysis (c1, st1) (c2,st2) f] performs case analysis on [c1 <: c2] + according to [st1] and [st2] where f c1 c2 is true if c1 is a subtype of c2. get_subtypes returning a pair: - whether [st1] and [st2] admit [c1 <: c2], and in case return the updated subtype [st1] - - whether [st1] and [st2] admit [not(c1 <: c2)], and in case return the updated subtype [st1] *) + - whether [st1] and [st2] admit [not(c1 <: c2)], + and in case return the updated subtype [st1] *) let case_analysis (c1, st1) (c2, st2) f is_interface = let f = check_subtype f in if (!Config.subtype_multirange) then @@ -475,7 +485,8 @@ module Int : sig val two : t val zero : t end = struct - (* the first bool indicates whether this is an unsigned value, and the second whether it is a pointer *) + (* the first bool indicates whether this is an unsigned value, + and the second whether it is a pointer *) type t = bool * Int64.t * bool let area u i = match i < 0L, u with @@ -523,7 +534,8 @@ end = struct let neg (unsigned, i, ptr) = (unsigned, Int64.neg i, ptr) - let lift binop (unsigned1, i1, ptr1) (unsigned2, i2, ptr2) = (unsigned1 || unsigned2, binop i1 i2, ptr1 || ptr2) + let lift binop (unsigned1, i1, ptr1) (unsigned2, i2, ptr2) = + (unsigned1 || unsigned2, binop i1 i2, ptr1 || ptr2) let lift1 unop (unsigned, i, ptr) = (unsigned, unop i, ptr) @@ -687,17 +699,35 @@ and typ = | Tstruct of struct_typ (** Type for a structured value *) | Tarray of typ * exp (** array type with fixed size *) -(** program expressions *) + +(** Program expressions. *) and exp = - | Var of Ident.t (** pure variable: it is not an lvalue *) - | UnOp of unop * exp * typ option (** unary operator with type of the result if known *) - | BinOp of binop * exp * exp (** binary operator *) - | Const of const (** constants *) - | Cast of typ * exp (** type cast *) - | Lvar of pvar (** the address of a program variable *) - | Lfield of exp * Ident.fieldname * typ (** a field offset, the type is the surrounding struct type *) - | Lindex of exp * exp (** an array index offset: exp1[exp2] *) - | Sizeof of typ * Subtype.t (** a sizeof expression *) + (** Pure variable: it is not an lvalue *) + | Var of Ident.t + + (** Unary operator with type of the result if known *) + | UnOp of unop * exp * typ option + + (** Binary operator *) + | BinOp of binop * exp * exp + + (** Constants *) + | Const of const + + (** Type cast *) + | Cast of typ * exp + + (** The address of a program variable *) + | Lvar of pvar + + (** A field offset, the type is the surrounding struct type *) + | Lfield of exp * Ident.fieldname * typ + + (** An array index offset: [exp1\[exp2\]] *) + | Lindex of exp * exp + + (** A sizeof expression *) + | Sizeof of typ * Subtype.t (** Kind of prune instruction *) type if_kind = @@ -1401,7 +1431,10 @@ and attribute_compare (att1 : attribute) (att2 : attribute) : int = match att1, att2 with | Aresource ra1, Aresource ra2 -> let n = res_act_kind_compare ra1.ra_kind ra2.ra_kind in - if n <> 0 then n else resource_compare ra1.ra_res ra2.ra_res (* ignore other values beside resources: arbitrary merging into one *) + if n <> 0 + then n + (* ignore other values beside resources: arbitrary merging into one *) + else resource_compare ra1.ra_res ra2.ra_res | Aresource _, _ -> - 1 | _, Aresource _ -> 1 | Aautorelease, Aautorelease -> 0 @@ -1700,14 +1733,18 @@ let color_pre_wrapper pe f x = let color = pe.pe_cmap_norm (Obj.repr x) in if color != pe.pe_color then begin (if pe.pe_kind == PP_HTML then Io_infer.Html.pp_start_color else Latex.pp_color) f color; - if color == Red then ({ pe with pe_cmap_norm = colormap_red; pe_color = Red }, true) (** Al subexpressiona red *) + if color == Red + (** All subexpressiona red *) + then ({ pe with pe_cmap_norm = colormap_red; pe_color = Red }, true) else ({ pe with pe_color = color }, true) end else (pe, false) end else (pe, false) (** Close color annotation if changed *) let color_post_wrapper changed pe f = - if changed then (if pe.pe_kind == PP_HTML then Io_infer.Html.pp_end_color f () else Latex.pp_color f pe.pe_color) + if changed + then (if pe.pe_kind == PP_HTML then Io_infer.Html.pp_end_color f () + else Latex.pp_color f pe.pe_color) (** Print a sequence with difference mode if enabled. *) let pp_seq_diff pp pe0 f = @@ -1951,7 +1988,8 @@ and pp_vpath pe fmt vpath = | Some de -> pp_dexp fmt de | None -> () in if pe.pe_kind == PP_HTML then - F.fprintf fmt " %a{vpath: %a}%a" Io_infer.Html.pp_start_color Orange pp vpath Io_infer.Html.pp_end_color () + F.fprintf fmt " %a{vpath: %a}%a" + Io_infer.Html.pp_start_color Orange pp vpath Io_infer.Html.pp_end_color () else F.fprintf fmt "%a" pp vpath @@ -2249,7 +2287,6 @@ let pp_instr pe0 f instr = | Pop -> "Pop" in F.fprintf f "STACKOP.%s; %a" s Location.pp loc | Declare_locals (ptl, loc) -> - (* let pp_pvar_typ fmt (pvar, typ) = F.fprintf fmt "%a:%a" (pp_pvar pe) pvar (pp_typ_full pe) typ in *) let pp_pvar_typ fmt (pvar, _) = F.fprintf fmt "%a" (pp_pvar pe) pvar in F.fprintf f "DECLARE_LOCALS(%a); %a" (pp_comma_seq pp_pvar_typ) ptl Location.pp loc | Goto_node (e, loc) -> @@ -2400,7 +2437,8 @@ let rec pp_star_seq pp f = function (********* START OF MODULE Predicates **********) (** Module Predicates records the occurrences of predicates as parameters - of (doubly -)linked lists and Epara. Provides unique numbering for predicates and an iterator. *) + of (doubly -)linked lists and Epara. Provides unique numbering + for predicates and an iterator. *) module Predicates : sig (** predicate environment *) type env @@ -2499,8 +2537,10 @@ end = struct todo_dll =[]; } - (** iterator for predicates which are marked as todo in env, unless they have been visited already. - This can in turn extend the todo list for the nested predicates, which are then visited as well. + (** iterator for predicates which are marked as todo in env, + unless they have been visited already. + This can in turn extend the todo list for the nested predicates, + which are then visited as well. Can be applied only once, as it destroys the todo list *) let iter (env: env) f f_dll = while env.todo != [] || env.todo_dll != [] do @@ -2673,15 +2713,22 @@ let rec pp_sexp_env pe0 envo f se = begin match pe.pe_kind with | PP_TEXT | PP_HTML -> - let pp_diff f (n, se) = F.fprintf f "%a:%a" Ident.pp_fieldname n (pp_sexp_env pe envo) se in + let pp_diff f (n, se) = + F.fprintf f "%a:%a" Ident.pp_fieldname n (pp_sexp_env pe envo) se in F.fprintf f "{%a}%a" (pp_seq_diff pp_diff pe) fel (pp_inst_if_trace pe) inst | PP_LATEX -> - let pp_diff f (n, se) = F.fprintf f "%a:%a" (Ident.pp_fieldname_latex Latex.Boldface) n (pp_sexp_env pe envo) se in - F.fprintf f "\\{%a\\}%a" (pp_seq_diff pp_diff pe) fel (pp_inst_if_trace pe) inst + let pp_diff f (n, se) = + F.fprintf f "%a:%a" + (Ident.pp_fieldname_latex Latex.Boldface) n (pp_sexp_env pe envo) se in + F.fprintf f "\\{%a\\}%a" + (pp_seq_diff pp_diff pe) fel (pp_inst_if_trace pe) inst end | Earray (size, nel, inst) -> - let pp_diff f (i, se) = F.fprintf f "%a:%a" (pp_exp pe) i (pp_sexp_env pe envo) se in - F.fprintf f "[%a|%a]%a" (pp_exp pe) size (pp_seq_diff pp_diff pe) nel (pp_inst_if_trace pe) inst + let pp_diff f (i, se) = + F.fprintf f "%a:%a" + (pp_exp pe) i (pp_sexp_env pe envo) se in + F.fprintf f "[%a|%a]%a" + (pp_exp pe) size (pp_seq_diff pp_diff pe) nel (pp_inst_if_trace pe) inst end; color_post_wrapper changed pe0 f @@ -2696,31 +2743,53 @@ and pp_hpred_env pe0 envo f hpred = | _ -> pe in (match pe'.pe_kind with | PP_TEXT | PP_HTML -> - F.fprintf f "%a|->%a:%a" (pp_exp pe') e (pp_sexp_env pe' envo) se (pp_texp_simple pe') te + F.fprintf f "%a|->%a:%a" + (pp_exp pe') e (pp_sexp_env pe' envo) se (pp_texp_simple pe') te | PP_LATEX -> F.fprintf f "%a\\mapsto %a" (pp_exp pe') e (pp_sexp_env pe' envo) se) | Hlseg (k, hpara, e1, e2, elist) -> (match pe.pe_kind with | PP_TEXT | PP_HTML -> F.fprintf f "lseg%a(%a,%a,[%a],%a)" - pp_lseg_kind k (pp_exp pe) e1 (pp_exp pe) e2 (pp_comma_seq (pp_exp pe)) elist (pp_hpara_env pe envo) hpara + pp_lseg_kind k + (pp_exp pe) e1 + (pp_exp pe) e2 + (pp_comma_seq (pp_exp pe)) elist + (pp_hpara_env pe envo) hpara | PP_LATEX -> F.fprintf f "\\textsf{lseg}_{%a}(%a,%a,[%a],%a)" - pp_lseg_kind k (pp_exp pe) e1 (pp_exp pe) e2 (pp_comma_seq (pp_exp pe)) elist (pp_hpara_env pe envo) hpara) + pp_lseg_kind k + (pp_exp pe) e1 + (pp_exp pe) e2 + (pp_comma_seq (pp_exp pe)) elist + (pp_hpara_env pe envo) hpara) | Hdllseg (k, hpara_dll, iF, oB, oF, iB, elist) -> (match pe.pe_kind with | PP_TEXT | PP_HTML -> F.fprintf f "dllseg%a(%a,%a,%a,%a,[%a],%a)" - pp_lseg_kind k (pp_exp pe) iF (pp_exp pe) oB (pp_exp pe) oF (pp_exp pe) iB (pp_comma_seq (pp_exp pe)) elist (pp_hpara_dll_env pe envo) hpara_dll + pp_lseg_kind k + (pp_exp pe) iF + (pp_exp pe) oB + (pp_exp pe) oF + (pp_exp pe) iB + (pp_comma_seq (pp_exp pe)) elist + (pp_hpara_dll_env pe envo) hpara_dll | PP_LATEX -> F.fprintf f "\\textsf{dllseg}_{%a}(%a,%a,%a,%a,[%a],%a)" - pp_lseg_kind k (pp_exp pe) iF (pp_exp pe) oB (pp_exp pe) oF (pp_exp pe) iB (pp_comma_seq (pp_exp pe)) elist (pp_hpara_dll_env pe envo) hpara_dll) + pp_lseg_kind k + (pp_exp pe) iF + (pp_exp pe) oB + (pp_exp pe) oF + (pp_exp pe) iB + (pp_comma_seq (pp_exp pe)) elist + (pp_hpara_dll_env pe envo) hpara_dll) end; color_post_wrapper changed pe0 f and pp_hpara_env pe envo f hpara = match envo with | None -> - let (r, n, svars, evars, b) = (hpara.root, hpara.next, hpara.svars, hpara.evars, hpara.body) in + let (r, n, svars, evars, b) = + (hpara.root, hpara.next, hpara.svars, hpara.evars, hpara.body) in F.fprintf f "lam [%a,%a,%a]. exists [%a]. %a" (Ident.pp pe) r (Ident.pp pe) n @@ -2732,7 +2801,9 @@ and pp_hpara_env pe envo f hpara = match envo with and pp_hpara_dll_env pe envo f hpara_dll = match envo with | None -> - let (iF, oB, oF, svars, evars, b) = (hpara_dll.cell, hpara_dll.blink, hpara_dll.flink, hpara_dll.svars_dll, hpara_dll.evars_dll, hpara_dll.body_dll) in + let (iF, oB, oF, svars, evars, b) = + (hpara_dll.cell, hpara_dll.blink, hpara_dll.flink, + hpara_dll.svars_dll, hpara_dll.evars_dll, hpara_dll.body_dll) in F.fprintf f "lam [%a,%a,%a,%a]. exists [%a]. %a" (Ident.pp pe) iF (Ident.pp pe) oB @@ -3035,7 +3106,8 @@ and hpara_dll_fpv para = (** {2 Functions for computing free non-program variables} *) -(** Type of free variables. These include primed, normal and footprint variables. We keep a count of how many types the variables appear. *) +(** Type of free variables. These include primed, normal and footprint variables. + We keep a count of how many types the variables appear. *) type fav = Ident.t list ref let fav_new () = @@ -3054,7 +3126,8 @@ let fav_for_all fav predicate = let fav_exists fav predicate = IList.exists predicate !fav -(** flag to indicate whether fav's are stored in duplicate form -- only to be used with fav_to_list *) +(** flag to indicate whether fav's are stored in duplicate form. + Only to be used with fav_to_list *) let fav_duplicates = ref false (** extend [fav] with a [id] *) @@ -3185,7 +3258,8 @@ let hpred_fav = (** This function should be used before adding a new index to Earray. The [exp] is the newly created - index. This function "cleans" [exp] according to whether it is the footprint or current part of the prop. + index. This function "cleans" [exp] according to whether it is + the footprint or current part of the prop. The function faults in the re - execution mode, as an internal check of the tool. *) let array_clean_new_index footprint_part new_idx = if footprint_part && not !Config.footprint then assert false; @@ -3350,7 +3424,8 @@ let sub_symmetric_difference sub1_in sub2_in = module Typtbl = Hashtbl.Make (struct type t = typ let equal = typ_equal let hash = Hashtbl.hash end) -(** [sub_find filter sub] returns the expression associated to the first identifier that satisfies [filter]. Raise [Not_found] if there isn't one. *) +(** [sub_find filter sub] returns the expression associated to the first identifier + that satisfies [filter]. Raise [Not_found] if there isn't one. *) let sub_find filter (sub: subst) = snd (IList.find (fun (i, _) -> filter i) sub) @@ -3804,79 +3879,6 @@ let hpred_compact sh hpred = HpredHash.add sh.hpredh hpred' hpred'; hpred' -(** {2 Type Environment} *) -(** hash tables on strings *) - -module TypenameHash = - Hashtbl.Make(struct - type t = Typename.t - let equal tn1 tn2 = Typename.equal tn1 tn2 - let hash = Hashtbl.hash - end) - -(** Type for type environment. *) -type tenv = struct_typ TypenameHash.t - -(** Create a new type environment. *) -let create_tenv () = TypenameHash.create 1000 - -(** Check if typename is found in tenv *) -let tenv_mem tenv name = - TypenameHash.mem tenv name - -(** Look up a name in the global type environment. *) -let tenv_lookup tenv name = - try Some (TypenameHash.find tenv name) - with Not_found -> None - -(** Add a (name,type) pair to the global type environment. *) -let tenv_add tenv name struct_typ = - TypenameHash.replace tenv name struct_typ - -(** expand a type if it is a typename by looking it up in the type environment *) -let expand_type tenv typ = - match typ with - | Tvar tname -> - begin - match tenv_lookup tenv tname with - | None -> assert false - | Some struct_typ -> Tstruct struct_typ - end - | _ -> typ - -(** type environment used for parsing, to be set by the client of the parser module *) -let tenv_for_parsing = ref (create_tenv ()) - -(** Serializer for type environments *) -let tenv_serializer : tenv Serialization.serializer = Serialization.create_serializer Serialization.tenv_key - -let global_tenv: (tenv option) Lazy.t = - lazy (Serialization.from_file tenv_serializer (DB.global_tenv_fname ())) - -(** Load a type environment from a file *) -let load_tenv_from_file (filename : DB.filename) : tenv option = - if filename = DB.global_tenv_fname () then - Lazy.force global_tenv - else - Serialization.from_file tenv_serializer filename - -(** Save a type environment into a file *) -let store_tenv_to_file (filename : DB.filename) (tenv : tenv) = - Serialization.to_file tenv_serializer filename tenv - -let tenv_iter f tenv = - TypenameHash.iter f tenv - -let tenv_fold f tenv = - TypenameHash.fold f tenv - -let pp_tenv f (tenv : tenv) = - TypenameHash.iter - (fun name typ -> - Format.fprintf f "@[<6>NAME: %s@." (Typename.to_string name); - Format.fprintf f "@[<6>TYPE: %a@." (pp_struct_typ pe_text (fun _ () -> ())) typ) - tenv - (** {2 Functions for constructing or destructing entities in this module} *) (** [mk_pvar name proc_name] creates a program var with the given function name *) @@ -3887,7 +3889,8 @@ let mk_pvar (name: Mangled.t) (proc_name: Procname.t) : pvar = let get_ret_pvar pname = mk_pvar Ident.name_return pname -(** [mk_pvar_callee name proc_name] creates a program var for a callee function with the given function name *) +(** [mk_pvar_callee name proc_name] creates a program var + for a callee function with the given function name *) let mk_pvar_callee (name: Mangled.t) (proc_name: Procname.t) : pvar = { pv_name = name; pv_kind = Callee_var proc_name } @@ -3938,10 +3941,14 @@ let sigma_to_sigma_ne sigma : (atom list * hpred list) list = let g (eqs, sigma) = (eqs, hpred:: sigma) in IList.map g eqs_sigma_list | Hlseg(Lseg_PE, para, e1, e2, el) -> - let g (eqs, sigma) = [(Aeq(e1, e2):: eqs, sigma); (eqs, Hlseg(Lseg_NE, para, e1, e2, el):: sigma)] in + let g (eqs, sigma) = + [(Aeq(e1, e2):: eqs, sigma); + (eqs, Hlseg(Lseg_NE, para, e1, e2, el):: sigma)] in IList.flatten (IList.map g eqs_sigma_list) | Hdllseg(Lseg_PE, para_dll, e1, e2, e3, e4, el) -> - let g (eqs, sigma) = [(Aeq(e1, e3):: Aeq(e2, e4):: eqs, sigma); (eqs, Hdllseg(Lseg_NE, para_dll, e1, e2, e3, e4, el):: sigma)] in + let g (eqs, sigma) = + [(Aeq(e1, e3):: Aeq(e2, e4):: eqs, sigma); + (eqs, Hdllseg(Lseg_NE, para_dll, e1, e2, e3, e4, el):: sigma)] in IList.flatten (IList.map g eqs_sigma_list) in IList.fold_left f [([],[])] sigma else @@ -3968,7 +3975,8 @@ let hpara_instantiate para e1 e2 elist = (** [hpara_dll_instantiate para cell blink flink elist] instantiates [para] with [cell], [blink], [flink], and [elist]. If [para = lambda (x, y, z, xs). exists zs. b], - then the result of the instantiation is [b\[cell / x, blink / y, flink / z, elist / xs, _zs'/ zs\]] + then the result of the instantiation is + [b\[cell / x, blink / y, flink / z, elist / xs, _zs'/ zs\]] for some fresh [_zs'].*) let hpara_dll_instantiate (para: hpara_dll) cell blink flink elist = let subst_for_svars = @@ -3982,7 +3990,12 @@ let hpara_dll_instantiate (para: hpara_dll) cell blink flink elist = let g id id' = (id, Var id') in try (IList.map2 g para.evars_dll ids_evars) with Invalid_argument _ -> assert false in - let subst = sub_of_list ((para.cell, cell):: (para.blink, blink):: (para.flink, flink):: subst_for_svars@subst_for_evars) in + let subst = + sub_of_list + ((para.cell, cell) :: + (para.blink, blink) :: + (para.flink, flink) :: + subst_for_svars@subst_for_evars) in (ids_evars, IList.map (hpred_sub subst) para.body_dll) let custom_error = diff --git a/infer/src/backend/sil.mli b/infer/src/IR/sil.mli similarity index 88% rename from infer/src/backend/sil.mli rename to infer/src/IR/sil.mli index 483b3c95c..d8740bf2f 100644 --- a/infer/src/backend/sil.mli +++ b/infer/src/IR/sil.mli @@ -10,6 +10,8 @@ (** The Smallfoot Intermediate Language *) +module F = Format + (** {2 Programs and Types} *) (** Type to represent one @Annotation. *) @@ -115,9 +117,14 @@ type res_act_kind = (** kind of dangling pointers *) type dangling_kind = - | DAuninit (** pointer is dangling because it is uninitialized *) - | DAaddr_stack_var (** pointer is dangling because it is the address of a stack variable which went out of scope *) - | DAminusone (** pointer is -1 *) + (** pointer is dangling because it is uninitialized *) + | DAuninit + + (** pointer is dangling because it is the address of a stack variable which went out of scope *) + | DAaddr_stack_var + + (** pointer is -1 *) + | DAminusone (** kind of pointer *) type ptr_kind = @@ -159,7 +166,8 @@ module Int : sig type t val add : t -> t -> t - (** compare the value of the integers, notice this is different from const compare, which distinguished between signed and unsigned +1 *) + (** compare the value of the integers, notice this is different from const compare, + which distinguished between signed and unsigned +1 *) val compare_value : t -> t -> int val div : t -> t -> t val eq : t -> t -> bool @@ -185,7 +193,7 @@ module Int : sig val neq : t -> t -> bool val null : t (** null behaves like zero except for the function isnull *) val one : t - val pp : Format.formatter -> t -> unit + val pp : F.formatter -> t -> unit val rem : t -> t -> t val sub : t -> t -> t val to_int : t -> int @@ -326,15 +334,32 @@ and typ = (** Program expressions. *) and exp = - | Var of Ident.t (** pure variable: it is not an lvalue *) - | UnOp of unop * exp * typ option (** unary operator with type of the result if known *) - | BinOp of binop * exp * exp (** binary operator *) - | Const of const (** constants *) - | Cast of typ * exp (** type cast *) - | Lvar of pvar (** the address of a program variable *) - | Lfield of exp * Ident.fieldname * typ (** a field offset, the type is the surrounding struct type *) - | Lindex of exp * exp (** an array index offset: [exp1\[exp2\]] *) - | Sizeof of typ * Subtype.t (** a sizeof expression *) + (** Pure variable: it is not an lvalue *) + | Var of Ident.t + + (** Unary operator with type of the result if known *) + | UnOp of unop * exp * typ option + + (** Binary operator *) + | BinOp of binop * exp * exp + + (** Constants *) + | Const of const + + (** Type cast *) + | Cast of typ * exp + + (** The address of a program variable *) + | Lvar of pvar + + (** A field offset, the type is the surrounding struct type *) + | Lfield of exp * Ident.fieldname * typ + + (** An array index offset: [exp1\[exp2\]] *) + | Lindex of exp * exp + + (** A sizeof expression *) + | Sizeof of typ * Subtype.t (** Sets of types. *) module TypSet : Set.S with type elt = typ @@ -527,47 +552,6 @@ val exp_compact : sharing_env -> exp -> exp (** Return a compact representation of the exp *) val hpred_compact : sharing_env -> hpred -> hpred -(** {2 Type Environment} *) - -type tenv (** Type for type environment. *) - -(** Create a new type environment. *) -val create_tenv : unit -> tenv - -(** Check if typename is found in tenv *) -val tenv_mem : tenv -> Typename.t -> bool - -(** Look up a name in the global type environment. *) -val tenv_lookup : tenv -> Typename.t -> struct_typ option - -(** Add a (name,typ) pair to the global type environment. *) -val tenv_add : tenv -> Typename.t -> struct_typ -> unit - -(** expand a type if it is a typename by looking it up in the type environment *) -val expand_type : tenv -> typ -> typ - -(** type environment used for parsing, to be set by the client of the parser module *) -val tenv_for_parsing : tenv ref - -(** Load a type environment from a file *) -val load_tenv_from_file : DB.filename -> tenv option - -(** Save a type environment into a file *) -val store_tenv_to_file : DB.filename -> tenv -> unit - -(** iterate over a type environment *) -val tenv_iter : (Typename.t -> struct_typ -> unit) -> tenv -> unit - -val tenv_fold : (Typename.t -> struct_typ -> 'a -> 'a) -> tenv -> 'a -> 'a - -(** print a type environment *) -val pp_tenv : Format.formatter -> tenv -> unit - -(** Return the lhs expression of a hpred *) -val hpred_get_lhs : hpred -> exp - -(** Field used for objective-c reference counting *) -val objc_ref_counter_field : (Ident.fieldname * typ * item_annotation) (** {2 Comparision And Inspection Functions} *) @@ -660,7 +644,8 @@ val ikind_is_char : ikind -> bool (** Check wheter the integer kind is unsigned *) val ikind_is_unsigned : ikind -> bool -(** Convert an int64 into an Int.t given the kind: the int64 is interpreted as unsigned according to the kind *) +(** Convert an int64 into an Int.t given the kind: + the int64 is interpreted as unsigned according to the kind *) val int_of_int64_kind : int64 -> ikind -> Int.t (** Comparision for ptr_kind *) @@ -673,7 +658,8 @@ val typ_compare : typ -> typ -> int val typ_equal : typ -> typ -> bool (** Comparision for fieldnames * types * item annotations. *) -val fld_typ_ann_compare : Ident.fieldname * typ * item_annotation -> Ident.fieldname * typ * item_annotation -> int +val fld_typ_ann_compare : + Ident.fieldname * typ * item_annotation -> Ident.fieldname * typ * item_annotation -> int val unop_equal : unop -> unop -> bool @@ -764,10 +750,18 @@ val hpred_equal : hpred -> hpred -> bool val fld_strexp_compare : Ident.fieldname * strexp -> Ident.fieldname * strexp -> int -val fld_strexp_list_compare : (Ident.fieldname * strexp) list -> (Ident.fieldname * strexp) list -> int +val fld_strexp_list_compare : + (Ident.fieldname * strexp) list -> (Ident.fieldname * strexp) list -> int val exp_strexp_compare : exp * strexp -> exp * strexp -> int +(** Return the lhs expression of a hpred *) +val hpred_get_lhs : hpred -> exp + +(** Field used for objective-c reference counting *) +val objc_ref_counter_field : (Ident.fieldname * typ * item_annotation) + + (** Compare function for annotations. *) val annotation_compare : annotation -> annotation -> int @@ -795,10 +789,10 @@ val get_sentinel_func_attribute_value : func_attribute list -> (int * int) optio (** {2 Pretty Printing} *) (** Begin change color if using diff printing, return updated printenv and change status *) -val color_pre_wrapper : printenv -> Format.formatter -> 'a -> printenv * bool +val color_pre_wrapper : printenv -> F.formatter -> 'a -> printenv * bool (** Close color annotation if changed *) -val color_post_wrapper : bool -> printenv -> Format.formatter -> unit +val color_post_wrapper : bool -> printenv -> F.formatter -> unit (** String representation of a unary operator. *) val str_unop : unop -> string @@ -813,33 +807,35 @@ val mem_alloc_pname : mem_kind -> Procname.t val mem_dealloc_pname : mem_kind -> Procname.t (** Pretty print an annotation. *) -val pp_annotation : Format.formatter -> annotation -> unit +val pp_annotation : F.formatter -> annotation -> unit (** Pretty print a const. *) -val pp_const: printenv -> Format.formatter -> const -> unit +val pp_const: printenv -> F.formatter -> const -> unit (** Pretty print an item annotation. *) -val pp_item_annotation : Format.formatter -> item_annotation -> unit +val pp_item_annotation : F.formatter -> item_annotation -> unit val item_annotation_to_string : item_annotation -> string (** Pretty print a method annotation. *) -val pp_method_annotation : string -> Format.formatter -> method_annotation -> unit +val pp_method_annotation : string -> F.formatter -> method_annotation -> unit (** Pretty print a type. *) -val pp_typ : printenv -> Format.formatter -> typ -> unit +val pp_typ : printenv -> F.formatter -> typ -> unit + +val pp_struct_typ : printenv -> (F.formatter -> unit -> unit) -> F.formatter -> struct_typ -> unit (** Pretty print a type with all the details. *) -val pp_typ_full : printenv -> Format.formatter -> typ -> unit +val pp_typ_full : printenv -> F.formatter -> typ -> unit val typ_to_string : typ -> string (** [pp_type_decl pe pp_base pp_size f typ] pretty prints a type declaration. pp_base prints the variable for a declaration, or can be skip to print only the type pp_size prints the expression for the array size *) -val pp_type_decl: printenv -> (Format.formatter -> unit -> unit) -> - (printenv -> Format.formatter -> exp -> unit) -> - Format.formatter -> typ -> unit +val pp_type_decl: printenv -> (F.formatter -> unit -> unit) -> + (printenv -> F.formatter -> exp -> unit) -> + F.formatter -> typ -> unit (** Dump a type with all the details. *) val d_typ_full : typ -> unit @@ -848,16 +844,16 @@ val d_typ_full : typ -> unit val d_typ_list : typ list -> unit (** Pretty print a program variable. *) -val pp_pvar : printenv -> Format.formatter -> pvar -> unit +val pp_pvar : printenv -> F.formatter -> pvar -> unit (** Pretty print a pvar which denotes a value, not an address *) -val pp_pvar_value : printenv -> Format.formatter -> pvar -> unit +val pp_pvar_value : printenv -> F.formatter -> pvar -> unit (** Dump a program variable. *) val d_pvar : pvar -> unit (** Pretty print a list of program variables. *) -val pp_pvar_list : printenv -> Format.formatter -> pvar list -> unit +val pp_pvar_list : printenv -> F.formatter -> pvar list -> unit (** Dump a list of program variables. *) val d_pvar_list : pvar list -> unit @@ -869,13 +865,13 @@ val attribute_to_string : printenv -> attribute -> string val dexp_to_string : dexp -> string (** Pretty print a dexp. *) -val pp_dexp : Format.formatter -> dexp -> unit +val pp_dexp : F.formatter -> dexp -> unit (** Pretty print an expression. *) -val pp_exp : printenv -> Format.formatter -> exp -> unit +val pp_exp : printenv -> F.formatter -> exp -> unit (** Pretty print an expression with type. *) -val pp_exp_typ : printenv -> Format.formatter -> exp * typ -> unit +val pp_exp_typ : printenv -> F.formatter -> exp * typ -> unit (** Convert an expression to a string *) val exp_to_string : exp -> string @@ -884,28 +880,28 @@ val exp_to_string : exp -> string val d_exp : exp -> unit (** Pretty print a type. *) -val pp_texp : printenv -> Format.formatter -> exp -> unit +val pp_texp : printenv -> F.formatter -> exp -> unit (** Pretty print a type with all the details. *) -val pp_texp_full : printenv -> Format.formatter -> exp -> unit +val pp_texp_full : printenv -> F.formatter -> exp -> unit (** Dump a type expression with all the details. *) val d_texp_full : exp -> unit (** Pretty print a list of expressions. *) -val pp_exp_list : printenv -> Format.formatter -> exp list -> unit +val pp_exp_list : printenv -> F.formatter -> exp list -> unit (** Dump a list of expressions. *) val d_exp_list : exp list -> unit (** Pretty print an offset *) -val pp_offset : printenv -> Format.formatter -> offset -> unit +val pp_offset : printenv -> F.formatter -> offset -> unit (** Dump an offset *) val d_offset : offset -> unit (** Pretty print a list of offsets *) -val pp_offset_list : printenv -> Format.formatter -> offset list -> unit +val pp_offset_list : printenv -> F.formatter -> offset list -> unit (** Dump a list of offsets *) val d_offset_list : offset list -> unit @@ -917,22 +913,22 @@ val instr_get_loc : instr -> Location.t val instr_get_exps : instr -> exp list (** Pretty print an instruction. *) -val pp_instr : printenv -> Format.formatter -> instr -> unit +val pp_instr : printenv -> F.formatter -> instr -> unit (** Dump an instruction. *) val d_instr : instr -> unit (** Pretty print a list of instructions. *) -val pp_instr_list : printenv -> Format.formatter -> instr list -> unit +val pp_instr_list : printenv -> F.formatter -> instr list -> unit (** Dump a list of instructions. *) val d_instr_list : instr list -> unit (** Pretty print a value path *) -val pp_vpath : printenv -> Format.formatter -> vpath -> unit +val pp_vpath : printenv -> F.formatter -> vpath -> unit (** Pretty print an atom. *) -val pp_atom : printenv -> Format.formatter -> atom -> unit +val pp_atom : printenv -> F.formatter -> atom -> unit (** Dump an atom. *) val d_atom : atom -> unit @@ -941,37 +937,38 @@ val d_atom : atom -> unit val inst_to_string : inst -> string (** Pretty print a strexp. *) -val pp_sexp : printenv -> Format.formatter -> strexp -> unit +val pp_sexp : printenv -> F.formatter -> strexp -> unit (** Dump a strexp. *) val d_sexp : strexp -> unit (** Pretty print a strexp list. *) -val pp_sexp_list : printenv -> Format.formatter -> strexp list -> unit +val pp_sexp_list : printenv -> F.formatter -> strexp list -> unit (** Dump a strexp. *) val d_sexp_list : strexp list -> unit (** Pretty print a hpred. *) -val pp_hpred : printenv -> Format.formatter -> hpred -> unit +val pp_hpred : printenv -> F.formatter -> hpred -> unit (** Dump a hpred. *) val d_hpred : hpred -> unit (** Pretty print a hpara. *) -val pp_hpara : printenv -> Format.formatter -> hpara -> unit +val pp_hpara : printenv -> F.formatter -> hpara -> unit (** Pretty print a list of hparas. *) -val pp_hpara_list : printenv -> Format.formatter -> hpara list -> unit +val pp_hpara_list : printenv -> F.formatter -> hpara list -> unit (** Pretty print a hpara_dll. *) -val pp_hpara_dll : printenv -> Format.formatter -> hpara_dll -> unit +val pp_hpara_dll : printenv -> F.formatter -> hpara_dll -> unit (** Pretty print a list of hpara_dlls. *) -val pp_hpara_dll_list : printenv -> Format.formatter -> hpara_dll list -> unit +val pp_hpara_dll_list : printenv -> F.formatter -> hpara_dll list -> unit (** Module Predicates records the occurrences of predicates as parameters - of (doubly -)linked lists and Epara. Provides unique numbering for predicates and an iterator. *) + of (doubly -)linked lists and Epara. + Provides unique numbering for predicates and an iterator. *) module Predicates : sig (** predicate environment *) type env @@ -991,13 +988,14 @@ module Predicates : sig end (** Pretty print a hpred with optional predicate env *) -val pp_hpred_env : printenv -> Predicates.env option -> Format.formatter -> hpred -> unit +val pp_hpred_env : printenv -> Predicates.env option -> F.formatter -> hpred -> unit (** {2 Functions for traversing SIL data types} *) (** This function should be used before adding a new index to Earray. The [exp] is the newly created - index. This function "cleans" [exp] according to whether it is the footprint or current part of the prop. + index. This function "cleans" [exp] according to whether it is the + footprint or current part of the prop. The function faults in the re - execution mode, as an internal check of the tool. *) val array_clean_new_index : bool -> exp -> exp @@ -1045,7 +1043,8 @@ val array_typ_elem : typ option -> typ -> typ (** Return the root of [lexp]. *) val root_of_lexp : exp -> exp -(** Get an expression "undefined", the boolean indicates whether the undefined value goest into the footprint *) +(** Get an expression "undefined", the boolean indicates + whether the undefined value goest into the footprint *) val exp_get_undefined : bool -> exp (** Checks whether an expression denotes a location using pointer arithmetic. @@ -1099,14 +1098,16 @@ val hpara_fpv : hpara -> pvar list (** {2 Functions for computing free non-program variables} *) -(** Type of free variables. These include primed, normal and footprint variables. We remember the order in which variables are added. *) +(** Type of free variables. These include primed, normal and footprint variables. + We remember the order in which variables are added. *) type fav -(** flag to indicate whether fav's are stored in duplicate form -- only to be used with fav_to_list *) +(** flag to indicate whether fav's are stored in duplicate form. + Only to be used with fav_to_list *) val fav_duplicates : bool ref (** Pretty print a fav. *) -val pp_fav : printenv -> Format.formatter -> fav -> unit +val pp_fav : printenv -> F.formatter -> fav -> unit (** Create a new [fav]. *) val fav_new : unit -> fav @@ -1227,7 +1228,9 @@ val sub_join : subst -> subst -> subst and [subst2], respectively. *) val sub_symmetric_difference : subst -> subst -> subst * subst * subst -(** [sub_find filter sub] returns the expression associated to the first identifier that satisfies [filter]. Raise [Not_found] if there isn't one. *) +(** [sub_find filter sub] returns the expression associated to the first identifier + that satisfies [filter]. + Raise [Not_found] if there isn't one. *) val sub_find : (Ident.t -> bool) -> subst -> exp (** [sub_filter filter sub] restricts the domain of [sub] to the @@ -1308,7 +1311,8 @@ val mk_pvar : Mangled.t -> Procname.t -> pvar (** [get_ret_pvar proc_name] retuns the return pvar associated with the procedure name *) val get_ret_pvar : Procname.t -> pvar -(** [mk_pvar_callee name proc_name] creates a program var for a callee function with the given function name *) +(** [mk_pvar_callee name proc_name] creates a program var + for a callee function with the given function name *) val mk_pvar_callee : Mangled.t -> Procname.t -> pvar (** create a global variable with the given name *) @@ -1338,7 +1342,8 @@ val hpara_instantiate : hpara -> exp -> exp -> exp list -> Ident.t list * hpred (** [hpara_dll_instantiate para cell blink flink elist] instantiates [para] with [cell], [blink], [flink], and [elist]. If [para = lambda (x, y, z, xs). exists zs. b], - then the result of the instantiation is [b\[cell / x, blink / y, flink / z, elist / xs, _zs'/ zs\]] + then the result of the instantiation is + [b\[cell / x, blink / y, flink / z, elist / xs, _zs'/ zs\]] for some fresh [_zs'].*) val hpara_dll_instantiate : hpara_dll -> exp -> exp -> exp -> exp list -> Ident.t list * hpred list diff --git a/infer/src/IR/tenv.ml b/infer/src/IR/tenv.ml new file mode 100644 index 000000000..16ac71c9f --- /dev/null +++ b/infer/src/IR/tenv.ml @@ -0,0 +1,81 @@ +(* + * 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 for Type Environments. *) + +(** Hash tables on strings. *) +module TypenameHash = + Hashtbl.Make(struct + type t = Typename.t + let equal tn1 tn2 = Typename.equal tn1 tn2 + let hash = Hashtbl.hash + end) + +(** Type for type environment. *) +type t = Sil.struct_typ TypenameHash.t + +(** Create a new type environment. *) +let create () = TypenameHash.create 1000 + +(** Check if typename is found in tenv *) +let mem tenv name = + TypenameHash.mem tenv name + +(** Look up a name in the global type environment. *) +let lookup tenv name = + try Some (TypenameHash.find tenv name) + with Not_found -> None + +(** Add a (name,type) pair to the global type environment. *) +let add tenv name struct_typ = + TypenameHash.replace tenv name struct_typ + +(** expand a type if it is a typename by looking it up in the type environment *) +let expand_type tenv typ = + match typ with + | Sil.Tvar tname -> + begin + match lookup tenv tname with + | None -> + assert false + | Some struct_typ -> + Sil.Tstruct struct_typ + end + | _ -> typ + +(** Serializer for type environments *) +let tenv_serializer : t Serialization.serializer = + Serialization.create_serializer Serialization.tenv_key + +let global_tenv: (t option) Lazy.t = + lazy (Serialization.from_file tenv_serializer (DB.global_tenv_fname ())) + +(** Load a type environment from a file *) +let load_from_file (filename : DB.filename) : t option = + if filename = DB.global_tenv_fname () then + Lazy.force global_tenv + else + Serialization.from_file tenv_serializer filename + +(** Save a type environment into a file *) +let store_to_file (filename : DB.filename) (tenv : t) = + Serialization.to_file tenv_serializer filename tenv + +let iter f tenv = + TypenameHash.iter f tenv + +let fold f tenv = + TypenameHash.fold f tenv + +let pp fmt (tenv : t) = + TypenameHash.iter + (fun name typ -> + Format.fprintf fmt "@[<6>NAME: %s@." (Typename.to_string name); + Format.fprintf fmt "@[<6>TYPE: %a@." (Sil.pp_struct_typ pe_text (fun _ () -> ())) typ) + tenv diff --git a/infer/src/IR/tenv.mli b/infer/src/IR/tenv.mli new file mode 100644 index 000000000..9f1fe3713 --- /dev/null +++ b/infer/src/IR/tenv.mli @@ -0,0 +1,42 @@ +(* + * 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 for Type Environments. *) + +type t (** Type for type environment. *) + +(** Add a (name,typename) pair to the global type environment. *) +val add : t -> Typename.t -> Sil.struct_typ -> unit + +(** Create a new type environment. *) +val create : unit -> t + +(** Expand a type if it is a typename by looking it up in the type environment. *) +val expand_type : t -> Sil.typ -> Sil.typ + +(** Fold a function over the elements of the type environment. *) +val fold : (Typename.t -> Sil.struct_typ -> 'a -> 'a) -> t -> 'a -> 'a + +(** iterate over a type environment *) +val iter : (Typename.t -> Sil.struct_typ -> unit) -> t -> unit + +(** Look up a name in the global type environment. *) +val lookup : t -> Typename.t -> Sil.struct_typ option + +(** Load a type environment from a file *) +val load_from_file : DB.filename -> t option + +(** Check if typename is found in t *) +val mem : t -> Typename.t -> bool + +(** Save a type environment into a file *) +val store_to_file : DB.filename -> t -> unit + +(** print a type environment *) +val pp : Format.formatter -> t -> unit diff --git a/infer/src/backend/typename.ml b/infer/src/IR/typename.ml similarity index 100% rename from infer/src/backend/typename.ml rename to infer/src/IR/typename.ml diff --git a/infer/src/backend/typename.mli b/infer/src/IR/typename.mli similarity index 100% rename from infer/src/backend/typename.mli rename to infer/src/IR/typename.mli diff --git a/infer/src/Makefile.in b/infer/src/Makefile.in index e03304dbf..aea07723e 100644 --- a/infer/src/Makefile.in +++ b/infer/src/Makefile.in @@ -68,18 +68,16 @@ endif #### Backend declarations #### -BACKEND_SOURCES = backend - -INFERANALYZE_MAIN = $(BACKEND_SOURCES)/inferanalyze +INFERANALYZE_MAIN = backend/inferanalyze #### InferPrint declarations #### -INFERPRINT_ATDGEN_STUB_BASE = $(BACKEND_SOURCES)/jsonbug +INFERPRINT_ATDGEN_STUB_BASE = backend/jsonbug INFERPRINT_ATDGEN_STUB_ATD = $(INFERPRINT_ATDGEN_STUB_BASE).atd INFERPRINT_ATDGEN_SUFFIXES = _t.ml _t.mli _j.ml _j.mli INFERPRINT_ATDGEN_STUBS = $(addprefix $(INFERPRINT_ATDGEN_STUB_BASE), $(INFERPRINT_ATDGEN_SUFFIXES)) -INFERPRINT_MAIN = $(BACKEND_SOURCES)/inferprint +INFERPRINT_MAIN = backend/inferprint ### InferUnit declarations ### @@ -143,7 +141,8 @@ else EXTRA_DEPS = facebook endif -DEPENDENCIES = $(BACKEND_SOURCES) checkers eradicate facebook/checkers facebook/checkers/graphql facebook/scripts harness $(EXTRA_DEPS) +DEPENDENCIES = IR backend checkers eradicate harness \ + facebook/checkers facebook/checkers/graphql facebook/scripts $(EXTRA_DEPS) OCAMLBUILD = ocamlbuild $(OCAMLBUILD_OPTIONS) -j 0 $(addprefix -I , $(DEPENDENCIES)) @@ -272,8 +271,8 @@ ifneq ($(wildcard $(BUILD_DIR)/sanitize.sh),) $(BUILD_DIR)/sanitize.sh endif -version: $(BACKEND_SOURCES)/version.ml.in Makefile - TMPFILE=$$(mktemp $(BACKEND_SOURCES)/version.ml.tmp.XXXX); \ +version: backend/version.ml.in Makefile + TMPFILE=$$(mktemp backend/version.ml.tmp.XXXX); \ INFER_GIT_COMMIT=$$(git --work-tree=$(ROOT_DIR) --git-dir=$(ROOT_DIR)/.git rev-parse --short HEAD || printf "unknown"); \ INFER_GIT_BRANCH=$$(git --work-tree=$(ROOT_DIR) --git-dir=$(ROOT_DIR)/.git rev-parse --abbrev-ref HEAD || printf "unknown"); \ sed \ @@ -284,7 +283,7 @@ version: $(BACKEND_SOURCES)/version.ml.in Makefile -e "s|@INFER_GIT_COMMIT[@]|$$INFER_GIT_COMMIT|g" \ -e "s|@INFER_GIT_BRANCH[@]|$$INFER_GIT_BRANCH|g" \ $< > "$$TMPFILE"; \ - @INSTALL@ -m 644 -C "$$TMPFILE" $(BACKEND_SOURCES)/version.ml; \ + @INSTALL@ -m 644 -C "$$TMPFILE" backend/version.ml; \ rm -f "$$TMPFILE" $(BUILD_DIR): @@ -317,8 +316,8 @@ clean: ifeq (@ENABLE_OCAML_ANNOT@,yes) $(REMOVE_DIR) $(ANNOT_DIR) endif - $(REMOVE) $(BACKEND_SOURCES)/version.ml - $(REMOVE) $(BACKEND_SOURCES)/version.ml.tmp.* + $(REMOVE) backend/version.ml + $(REMOVE) backend/version.ml.tmp.* $(REMOVE) $(INFERJAVA_BIN) $(INFERCLANG_BIN) $(INFERLLVM_BIN) $(INFERUNIT_BIN) $(REMOVE) $(CHECKCOPYRIGHT_BIN) $(REMOVE) $(CLANG_ATDGEN_STUBS) diff --git a/infer/src/backend/PROFILE_HOWTO b/infer/src/backend/PROFILE_HOWTO deleted file mode 100644 index 05447f640..000000000 --- a/infer/src/backend/PROFILE_HOWTO +++ /dev/null @@ -1,12 +0,0 @@ -[Based on a linux machine] - -1) comment out the line - # PROFILE := true #To activate profiler -in cil/Makefile.in -2) configure -3) make -4) run test, e.g. - ./bin/cilly -c --doanalysis --test ../test/creation.c -5) display the profile info: - gprof ./obj/x86_LINUX/cilly.asm.exe - diff --git a/infer/src/backend/README.md b/infer/src/backend/README.md new file mode 100644 index 000000000..8c80359d8 --- /dev/null +++ b/infer/src/backend/README.md @@ -0,0 +1,8 @@ +# Back End + +The back end is responsible for the analysis of a project starting from an intermediate representation stored in the results directory, typically `infer-out`. + +The main entry point is module [Inferanalyze](inferanalyze.ml) which produces the back-end executable `InferAnalyze`. + +Module [Inferprint](inferprint.ml) produces the executable `InferPrint`, which is used to export analysis results. + diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index 08e40b439..6ce22c907 100644 --- a/infer/src/backend/abs.ml +++ b/infer/src/backend/abs.ml @@ -408,7 +408,7 @@ let typ_get_recursive_flds tenv typ_exp = match t with | Sil.Tvar _ | Sil.Tint _ | Sil.Tfloat _ | Sil.Tvoid | Sil.Tfun _ -> false | Sil.Tptr (Sil.Tvar tname', _) -> - let typ' = match Sil.tenv_lookup tenv tname' with + let typ' = match Tenv.lookup tenv tname' with | None -> L.err "@.typ_get_recursive: Undefined type %s@." (Typename.to_string tname'); t @@ -419,7 +419,7 @@ let typ_get_recursive_flds tenv typ_exp = in match typ_exp with | Sil.Sizeof (typ, _) -> - (match Sil.expand_type tenv typ with + (match Tenv.expand_type tenv typ with | Sil.Tint _ | Sil.Tvoid | Sil.Tfun _ | Sil.Tptr _ | Sil.Tfloat _ -> [] | Sil.Tstruct { Sil.instance_fields } -> IList.map (fun (x, _, _) -> x) (IList.filter (filter typ) instance_fields) @@ -1254,7 +1254,7 @@ let set_footprint_for_abs (p : 'a Prop.t) (p_foot : 'a Prop.t) local_stack_pvars Prop.replace_sigma_footprint sigma (Prop.replace_pi_footprint pi p) (** Abstract the footprint of prop *) -let abstract_footprint pname (tenv : Sil.tenv) (prop : Prop.normal Prop.t) : Prop.normal Prop.t = +let abstract_footprint pname (tenv : Tenv.t) (prop : Prop.normal Prop.t) : Prop.normal Prop.t = let (p, added_local_vars) = extract_footprint_for_abs prop in let p_abs = abstract_prop diff --git a/infer/src/backend/abs.mli b/infer/src/backend/abs.mli index ed2057864..14efa8249 100644 --- a/infer/src/backend/abs.mli +++ b/infer/src/backend/abs.mli @@ -14,27 +14,27 @@ type rules (** Abstract a proposition. *) -val abstract : Procname.t -> Sil.tenv -> Prop.normal Prop.t -> Prop.normal Prop.t +val abstract : Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t (** Check whether the prop contains junk. If it does, and [Config.allowleak] is true, remove the junk, otherwise raise a Leak exception. *) val abstract_junk : ?original_prop:Prop.normal Prop.t -> - Procname.t -> Sil.tenv -> Prop.normal Prop.t -> Prop.normal Prop.t + Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t (** Abstract a proposition but don't pay a SymOp *) -val abstract_no_symop : Procname.t -> Sil.tenv -> Prop.normal Prop.t -> Prop.normal Prop.t +val abstract_no_symop : Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t (** Get the current rules discoveres *) val get_current_rules : unit -> rules (** Abstract each proposition in [propset] *) -val lifted_abstract : Procname.t -> Sil.tenv -> Propset.t -> Propset.t +val lifted_abstract : Procname.t -> Tenv.t -> Propset.t -> Propset.t (** Remove redundant elements in an array, and check for junk afterwards *) val remove_redundant_array_elements : - Procname.t -> Sil.tenv -> Prop.normal Prop.t -> Prop.normal Prop.t + Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t (** Reset the abstraction rules discovered *) val reset_current_rules : unit -> unit diff --git a/infer/src/backend/builtin.ml b/infer/src/backend/builtin.ml index c233e9ea2..4f5189a5d 100644 --- a/infer/src/backend/builtin.ml +++ b/infer/src/backend/builtin.ml @@ -12,7 +12,7 @@ type args = { pdesc : Cfg.Procdesc.t; instr : Sil.instr; - tenv : Sil.tenv; + tenv : Tenv.t; prop_ : Prop.normal Prop.t; path : Paths.Path.t; ret_ids : Ident.t list; diff --git a/infer/src/backend/builtin.mli b/infer/src/backend/builtin.mli index 95b0deab6..bbc103e0c 100644 --- a/infer/src/backend/builtin.mli +++ b/infer/src/backend/builtin.mli @@ -12,7 +12,7 @@ type args = { pdesc : Cfg.Procdesc.t; instr : Sil.instr; - tenv : Sil.tenv; + tenv : Tenv.t; prop_ : Prop.normal Prop.t; path : Paths.Path.t; ret_ids : Ident.t list; diff --git a/infer/src/backend/callbacks.ml b/infer/src/backend/callbacks.ml index 925997c4c..d5dc53140 100644 --- a/infer/src/backend/callbacks.ml +++ b/infer/src/backend/callbacks.ml @@ -15,7 +15,7 @@ type proc_callback_args = { get_proc_desc : Procname.t -> Cfg.Procdesc.t option; get_procs_in_file : Procname.t -> Procname.t list; idenv : Idenv.t; - tenv : Sil.tenv; + tenv : Tenv.t; proc_name : Procname.t; proc_desc : Cfg.Procdesc.t; } @@ -25,7 +25,7 @@ type proc_callback_t = proc_callback_args -> unit type cluster_callback_t = Procname.t list -> (Procname.t -> Cfg.Procdesc.t option) -> - (Idenv.t * Sil.tenv * Procname.t * Cfg.Procdesc.t) list -> + (Idenv.t * Tenv.t * Procname.t * Cfg.Procdesc.t) list -> unit let procedure_callbacks = ref [] diff --git a/infer/src/backend/callbacks.mli b/infer/src/backend/callbacks.mli index 5b9020f37..f7ddfd893 100644 --- a/infer/src/backend/callbacks.mli +++ b/infer/src/backend/callbacks.mli @@ -13,7 +13,7 @@ type proc_callback_args = { get_proc_desc : Procname.t -> Cfg.Procdesc.t option; get_procs_in_file : Procname.t -> Procname.t list; idenv : Idenv.t; - tenv : Sil.tenv; + tenv : Tenv.t; proc_name : Procname.t; proc_desc : Cfg.Procdesc.t; } @@ -29,7 +29,7 @@ type proc_callback_t = proc_callback_args -> unit type cluster_callback_t = Procname.t list -> (Procname.t -> Cfg.Procdesc.t option) -> - (Idenv.t * Sil.tenv * Procname.t * Cfg.Procdesc.t) list -> + (Idenv.t * Tenv.t * Procname.t * Cfg.Procdesc.t) list -> unit (** register a procedure callback *) diff --git a/infer/src/backend/dom.mli b/infer/src/backend/dom.mli index 06ab2322e..e279bdd18 100644 --- a/infer/src/backend/dom.mli +++ b/infer/src/backend/dom.mli @@ -14,7 +14,7 @@ (** Join two pathsets *) val pathset_join : - Procname.t -> Sil.tenv -> Paths.PathSet.t -> Paths.PathSet.t -> Paths.PathSet.t * Paths.PathSet.t + Procname.t -> Tenv.t -> Paths.PathSet.t -> Paths.PathSet.t -> Paths.PathSet.t * Paths.PathSet.t val join_time : float ref @@ -23,7 +23,7 @@ val proplist_collapse_pre : Prop.normal Prop.t list -> Prop.normal Specs.Jprop.t val pathset_collapse : Paths.PathSet.t -> Paths.PathSet.t (** reduce the pathset only based on implication checking. *) -val pathset_collapse_impl : Procname.t -> Sil.tenv -> Paths.PathSet.t -> Paths.PathSet.t +val pathset_collapse_impl : Procname.t -> Tenv.t -> Paths.PathSet.t -> Paths.PathSet.t (** {2 Meet Operators} *) diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index cde23da68..5e631cd90 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -473,7 +473,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket = match hpred_typ_opt, find_pvar_typ_without_ptr prop pvar with | Some (Sil.Sizeof (t1, _)), Some (Sil.Sizeof (Sil.Tptr (_t2, _), _)) -> (try - let t2 = Sil.expand_type tenv _t2 in + let t2 = Tenv.expand_type tenv _t2 in Sil.typ_equal t1 t2 with exn when exn_not_failure exn -> false) | Some (Sil.Sizeof (Sil.Tint _, _)), Some (Sil.Sizeof (Sil.Tint _, _)) when is_file -> (* must be a file opened with "open" *) diff --git a/infer/src/backend/errdesc.mli b/infer/src/backend/errdesc.mli index bebf0c426..3bbaedfb0 100644 --- a/infer/src/backend/errdesc.mli +++ b/infer/src/backend/errdesc.mli @@ -117,7 +117,9 @@ val explain_tainted_value_reaching_sensitive_function : If the current instruction is a variable nullify, blame the variable. If it is an abstraction, blame any variable nullify at the current node. If there is an alloc attribute, print the function call and line number. *) -val explain_leak : Sil.tenv -> Sil.hpred -> 'a Prop.t -> Sil.attribute option -> string option -> Exceptions.exception_visibility * Localise.error_desc +val explain_leak : + Tenv.t -> Sil.hpred -> 'a Prop.t -> Sil.attribute option -> string option -> + Exceptions.exception_visibility * Localise.error_desc (** Produce a description of the memory access performed in the current instruction, if any. *) val explain_memory_access : Localise.deref_str -> 'a Prop.t -> Location.t -> Localise.error_desc diff --git a/infer/src/backend/exe_env.ml b/infer/src/backend/exe_env.ml index c5e32dce9..63f81a29c 100644 --- a/infer/src/backend/exe_env.ml +++ b/infer/src/backend/exe_env.ml @@ -17,7 +17,7 @@ type file_data = { source: DB.source_file; nLOC : int; tenv_file: DB.filename; - mutable tenv: Sil.tenv option; + mutable tenv: Tenv.t option; cfg_file: DB.filename; mutable cfg: Cfg.cfg option; } @@ -126,7 +126,7 @@ let get_source exe_env pname = let file_data_to_tenv file_data = if file_data.tenv == None - then file_data.tenv <- Sil.load_tenv_from_file file_data.tenv_file; + then file_data.tenv <- Tenv.load_from_file file_data.tenv_file; file_data.tenv let file_data_to_cfg file_data = @@ -135,7 +135,7 @@ let file_data_to_cfg file_data = file_data.cfg (** return the type environment associated to the procedure *) -let get_tenv exe_env proc_name : Sil.tenv = +let get_tenv exe_env proc_name : Tenv.t = match get_file_data exe_env proc_name with | None -> failwith ("get_tenv: file_data not found for" ^ Procname.to_string proc_name) diff --git a/infer/src/backend/exe_env.mli b/infer/src/backend/exe_env.mli index 1314deb1f..57e94c4ed 100644 --- a/infer/src/backend/exe_env.mli +++ b/infer/src/backend/exe_env.mli @@ -33,7 +33,7 @@ val get_cg : t -> Cg.t val get_source : t -> Procname.t -> DB.source_file option (** return the type environment associated to the procedure *) -val get_tenv : t -> Procname.t -> Sil.tenv +val get_tenv : t -> Procname.t -> Tenv.t (** return the cfg associated to the procedure *) val get_cfg : t -> Procname.t -> Cfg.cfg option diff --git a/infer/src/backend/inferanalyze.ml b/infer/src/backend/inferanalyze.ml index a6bc11a8b..6c1baea75 100644 --- a/infer/src/backend/inferanalyze.ml +++ b/infer/src/backend/inferanalyze.ml @@ -35,7 +35,9 @@ let ml_buckets_arg = ref "cf" let allow_specs_cleanup = ref false let version_string () = - "Infer version " ^ Version.versionString ^ "\nCopyright 2009 - present Facebook. All Rights Reserved.\n" + "Infer version " + ^ Version.versionString + ^ "\nCopyright 2009 - present Facebook. All Rights Reserved.\n" let print_version () = F.fprintf F.std_formatter "%s@." (version_string ()); @@ -300,7 +302,9 @@ let setup_logging () = let log_dir_name = "log" in let analyzer_out_name = "analyzer_out" in let analyzer_err_name = "analyzer_err" in - let log_dir = DB.filename_to_string (DB.Results_dir.path_to_filename DB.Results_dir.Abs_root [log_dir_name]) in + let log_dir = + DB.filename_to_string + (DB.Results_dir.path_to_filename DB.Results_dir.Abs_root [log_dir_name]) in DB.create_dir log_dir; let analyzer_out_file = if !out_file_cmdline = "" then Filename.concat log_dir analyzer_out_name @@ -358,7 +362,10 @@ let () = DB.Results_dir.clean_specs_dir (); let analyzer_out_of, analyzer_err_of = setup_logging () in - if (!Config.curr_language = Config.C_CPP) then Mleak_buckets.init_buckets !ml_buckets_arg; + + if !Config.curr_language = Config.C_CPP + then Mleak_buckets.init_buckets !ml_buckets_arg; + let finish_logging () = teardown_logging analyzer_out_of analyzer_err_of in diff --git a/infer/src/backend/inferprint.ml b/infer/src/backend/inferprint.ml index a00a13eae..3df30e6a5 100644 --- a/infer/src/backend/inferprint.ml +++ b/infer/src/backend/inferprint.ml @@ -244,7 +244,8 @@ let print_usage_exit err_s = (** return the list of the .specs files in the results dir and libs, if they're defined *) let load_specfiles () = let specs_files_in_dir dir = - let is_specs_file fname = not (Sys.is_directory fname) && Filename.check_suffix fname ".specs" in + let is_specs_file fname = + not (Sys.is_directory fname) && Filename.check_suffix fname ".specs" in let all_filenames = Array.to_list (Sys.readdir dir) in let all_filepaths = IList.map (fun fname -> Filename.concat dir fname) all_filenames in IList.filter is_specs_file all_filepaths in @@ -266,7 +267,8 @@ let begin_latex_file fmt = (** Write proc summary to latex file *) let write_summary_latex fmt summary = let proc_name = Specs.get_proc_name summary in - Latex.pp_section fmt ("Analysis of function " ^ (Latex.convert_string (Procname.to_string proc_name))); + Latex.pp_section fmt ("Analysis of function " + ^ (Latex.convert_string (Procname.to_string proc_name))); F.fprintf fmt "@[%a@]" (Specs.pp_summary (pe_latex Black) !whole_seconds) summary let error_desc_to_csv_string error_desc = @@ -294,10 +296,14 @@ let error_desc_to_xml_tags error_desc = Io_infer.Xml.create_tree label [] [(Io_infer.Xml.String contents)] in IList.map (fun (tag, value) -> subtree tag (Escape.escape_xml value)) tags -let get_bug_hash (kind: string) (type_str: string) (procedure_id: string) (filename: string) (node_key: int) (error_desc: Localise.error_desc) = +let get_bug_hash + (kind: string) (type_str: string) (procedure_id: string) (filename: string) + (node_key: int) (error_desc: Localise.error_desc) = let qualifier_tag_call_procedure = Localise.error_desc_get_tag_call_procedure error_desc in let qualifier_tag_value = Localise.error_desc_get_tag_value error_desc in - Hashtbl.hash(kind, type_str, procedure_id, filename, node_key, qualifier_tag_call_procedure, qualifier_tag_value) + Hashtbl.hash + (kind, type_str, procedure_id, filename, node_key, + qualifier_tag_call_procedure, qualifier_tag_value) let loc_trace_to_jsonbug_record trace_list ekind = match ekind with @@ -533,7 +539,9 @@ module BugsCsv = struct let err_desc_string = error_desc_to_csv_string error_desc in let err_advice_string = error_advice_to_csv_string error_desc in let qualifier_tag_xml = - let xml_node = Io_infer.Xml.create_tree Io_infer.Xml.tag_qualifier_tags [] (error_desc_to_xml_tags error_desc) in + let xml_node = + Io_infer.Xml.create_tree + Io_infer.Xml.tag_qualifier_tags [] (error_desc_to_xml_tags error_desc) in let p fmt () = F.fprintf fmt "%a" (Io_infer.Xml.pp_document false) xml_node in let s = pp_to_string p () in Escape.escape_csv s in @@ -693,7 +701,8 @@ module BugsXml = struct subtree Io_infer.Xml.tag_file filename; Io_infer.Xml.create_tree Io_infer.Xml.tag_trace [] (loc_trace_to_xml linereader ltr); subtree Io_infer.Xml.tag_key (string_of_int node_key); - Io_infer.Xml.create_tree Io_infer.Xml.tag_qualifier_tags [] (error_desc_to_xml_tags error_desc); + Io_infer.Xml.create_tree + Io_infer.Xml.tag_qualifier_tags [] (error_desc_to_xml_tags error_desc); subtree Io_infer.Xml.tag_hash (string_of_int bug_hash) ] @ @@ -965,7 +974,8 @@ let process_summary filters linereader stats (top_proc_set: Procname.Set.t) (fna let pp_simple_saved = !Config.pp_simple in Config.pp_simple := true; if !quiet then () - else L.out "Procedure: %a@\n%a@." Procname.pp proc_name (Specs.pp_summary pe_text !whole_seconds) summary; + else L.out "Procedure: %a@\n%a@." + Procname.pp proc_name (Specs.pp_summary pe_text !whole_seconds) summary; let error_filter error_desc error_name = let always_report () = Localise.error_desc_extract_tag_value error_desc "always_report" = "true" in @@ -995,7 +1005,10 @@ let process_summary filters linereader stats (top_proc_set: Procname.Set.t) (fna if not (DB.file_exists svg_file) || DB.file_modified_time dot_file > DB.file_modified_time svg_file then - ignore (Sys.command ("dot -Tsvg \"" ^ (DB.filename_to_string dot_file) ^ "\" >\"" ^ (DB.filename_to_string svg_file) ^"\"")) + ignore (Sys.command ("dot -Tsvg \"" ^ + (DB.filename_to_string dot_file) ^ + "\" >\"" ^ + (DB.filename_to_string svg_file) ^"\"")) end; if !xml_specs then begin let xml_file = DB.filename_add_suffix base ".xml" in @@ -1017,7 +1030,8 @@ let process_summary filters linereader stats (top_proc_set: Procname.Set.t) (fna module AnalysisResults = struct type t = (string * Specs.summary) list - let spec_files_from_cmdline = (* parse command-line arguments, and find spec files specified there *) + let spec_files_from_cmdline = + (* parse command-line arguments, and find spec files specified there *) let args = ref [] in let f arg = if not (Filename.check_suffix arg ".specs") && arg <> "." @@ -1082,7 +1096,8 @@ module AnalysisResults = struct iterate (** Serializer for analysis results *) - let analysis_results_serializer : t Serialization.serializer = Serialization.create_serializer Serialization.analysis_results_key + let analysis_results_serializer : t Serialization.serializer = + Serialization.create_serializer Serialization.analysis_results_key (** Load analysis_results from a file *) let load_analysis_results_from_file (filename : DB.filename) : t option = @@ -1093,7 +1108,8 @@ module AnalysisResults = struct Serialization.to_file analysis_results_serializer filename analysis_results (** Return an iterator over all the summaries. - If options - load_results or - save_results are used, all the summaries are loaded in memory *) + If options - load_results or - save_results are used, + all the summaries are loaded in memory *) let get_summary_iterator () = let iterator_of_summary_list r = fun f -> IList.iter f r in @@ -1119,7 +1135,8 @@ module AnalysisResults = struct end end -let compute_top_procedures = ref false (* warning: computing top procedures iterates over summaries twice *) +(* warning: computing top procedures iterates over summaries twice *) +let compute_top_procedures = ref false let () = Config.developer_mode := true; @@ -1141,7 +1158,8 @@ let () = do_outf bugs_xml (fun outf -> BugsXml.pp_bugs_open outf.fmt ()); do_outf report (fun outf -> Report.pp_header outf.fmt ()); let top_proc = TopProcedures.create () in - if !compute_top_procedures && (!procs_csv != None || !procs_xml != None) then iterate_summaries (TopProcedures.process_summary top_proc); + if !compute_top_procedures && (!procs_csv != None || !procs_xml != None) + then iterate_summaries (TopProcedures.process_summary top_proc); let top_proc_set = TopProcedures.top_set top_proc in let linereader = Printer.LineReader.create () in let stats = Stats.create () in diff --git a/infer/src/backend/preanal.mli b/infer/src/backend/preanal.mli index 6e8b845d5..431cf6cd0 100644 --- a/infer/src/backend/preanal.mli +++ b/infer/src/backend/preanal.mli @@ -11,5 +11,5 @@ (** Preanalysis for eliminating dead local variables *) (** Perform liveness analysis *) -val doit : ?f_translate_typ:(Sil.tenv -> string -> unit) option -> Cfg.cfg -> Cg.t -> Sil.tenv +val doit : ?f_translate_typ:(Tenv.t -> string -> unit) option -> Cfg.cfg -> Cg.t -> Tenv.t -> unit diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli index 6a6c90948..672399f0f 100644 --- a/infer/src/backend/prop.mli +++ b/infer/src/backend/prop.mli @@ -216,18 +216,19 @@ val mk_neq : exp -> exp -> atom val mk_eq : exp -> exp -> atom (** create a strexp of the given type, populating the structures if [expand_structs] is true *) -val create_strexp_of_type: Sil.tenv option -> struct_init_mode -> Sil.typ -> Sil.inst -> Sil.strexp +val create_strexp_of_type: Tenv.t option -> struct_init_mode -> Sil.typ -> Sil.inst -> Sil.strexp (** Construct a pointsto. *) val mk_ptsto : exp -> strexp -> exp -> hpred (** Construct a points-to predicate for an expression using either the provided expression [name] as base for fresh identifiers. *) -val mk_ptsto_exp : Sil.tenv option -> struct_init_mode -> exp * exp * exp option -> Sil.inst -> hpred +val mk_ptsto_exp : Tenv.t option -> struct_init_mode -> exp * exp * exp option -> Sil.inst -> hpred (** Construct a points-to predicate for a single program variable. If [expand_structs] is true, initialize the fields of structs with fresh variables. *) -val mk_ptsto_lvar : Sil.tenv option -> struct_init_mode -> Sil.inst -> pvar * exp * exp option -> hpred +val mk_ptsto_lvar : + Tenv.t option -> struct_init_mode -> Sil.inst -> pvar * exp * exp option -> hpred (** Construct a lseg predicate *) val mk_lseg : lseg_kind -> hpara -> exp -> exp -> exp list -> hpred diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index 27c25fd1e..f67fee77a 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -1453,7 +1453,7 @@ struct let cloneable_type = Typename.Java.from_string "java.lang.Cloneable" let is_interface tenv class_name = - match Sil.tenv_lookup tenv class_name with + match Tenv.lookup tenv class_name with | Some ({ Sil.csu = Csu.Class Csu.Java; struct_name = Some _ } as struct_typ) -> (IList.length struct_typ.Sil.instance_fields = 0) && (IList.length struct_typ.Sil.def_methods = 0) @@ -1471,7 +1471,7 @@ struct let check_subclass_tenv tenv c1 c2 = let rec check cn = Typename.equal cn c2 || is_root_class c2 || - match Sil.tenv_lookup tenv cn with + match Tenv.lookup tenv cn with | Some ({ Sil.struct_name = Some _; csu = Csu.Class _; superclasses }) -> IList.exists check superclasses | _ -> false in @@ -1618,7 +1618,7 @@ let get_overrides_of tenv supertype pname = if typ_has_method resolved_pname typ then (typ, resolved_pname) :: overrides_acc else overrides_acc else overrides_acc in - Sil.tenv_fold gather_overrides tenv [] + Tenv.fold gather_overrides tenv [] (** Check the equality of two types ignoring flags in the subtyping components *) let texp_equal_modulo_subtype_flag texp1 texp2 = match texp1, texp2 with @@ -1702,7 +1702,7 @@ let handle_parameter_subtype tenv prop1 sigma2 subs (e1, se1, texp1) (se2, texp2 Sil.Eexp(e1', _), Sil.Eexp(e2', _) when not (is_allocated_lhs e1') -> begin - let t1, t2 = Sil.expand_type tenv _t1, Sil.expand_type tenv _t2 in + let t1, t2 = Tenv.expand_type tenv _t1, Tenv.expand_type tenv _t2 in match type_rhs e2' with | Some (t2_ptsto , sub2) -> if not (Sil.typ_equal t1 t2) && Subtyping_check.check_subtype tenv t1 t2 @@ -1942,7 +1942,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 * | Config.Java -> let object_type = Typename.TN_csu (Csu.Class Csu.Java, Mangled.from_string "java.lang.String") in - let typ = match Sil.tenv_lookup tenv object_type with + let typ = match Tenv.lookup tenv object_type with | Some typ -> typ | None -> assert false in Sil.Sizeof (Sil.Tstruct typ, Sil.Subtype.exact) in @@ -1954,7 +1954,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 * let class_texp = let class_type = Typename.TN_csu (Csu.Class Csu.Java, Mangled.from_string "java.lang.Class") in - let typ = match Sil.tenv_lookup tenv class_type with + let typ = match Tenv.lookup tenv class_type with | Some typ -> typ | None -> assert false in Sil.Sizeof (Sil.Tstruct typ, Sil.Subtype.exact) in diff --git a/infer/src/backend/prover.mli b/infer/src/backend/prover.mli index 4eb1733b4..012b718e4 100644 --- a/infer/src/backend/prover.mli +++ b/infer/src/backend/prover.mli @@ -62,7 +62,7 @@ val get_bounds : Prop.normal Prop.t -> Sil.exp -> Sil.Int.t option * Sil.Int.t o (** {2 Abduction prover} *) (** [check_implication p1 p2] returns true if [p1|-p2] *) -val check_implication : Procname.t -> Sil.tenv -> Prop.normal Prop.t -> Prop.exposed Prop.t -> bool +val check_implication : Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.exposed Prop.t -> bool type check = | Bounds_check @@ -79,7 +79,7 @@ type implication_result = frame)] where [sub] is a substitution which instantiates the primed vars of [p1] and [p2], which are assumed to be disjoint. *) val check_implication_for_footprint : - Procname.t -> Sil.tenv -> Prop.normal Prop.t -> Prop.exposed Prop.t -> implication_result + Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.exposed Prop.t -> implication_result (** {2 Cover: miminum set of pi's whose disjunction is equivalent to true} *) @@ -97,15 +97,15 @@ module Subtyping_check : sig (** check_subtype t1 t2 checks whether t1 is a subtype of t2, given the type environment tenv. *) - val check_subtype : Sil.tenv -> Sil.typ -> Sil.typ -> bool + val check_subtype : Tenv.t -> Sil.typ -> Sil.typ -> bool (** subtype_case_analysis tenv tecp1 texp2 performs case analysis on [texp1 <: texp2], and returns the updated types in the true and false case, if they are possible *) - val subtype_case_analysis : Sil.tenv -> Sil.exp -> Sil.exp -> Sil.exp option * Sil.exp option + val subtype_case_analysis : Tenv.t -> Sil.exp -> Sil.exp -> Sil.exp option * Sil.exp option end -val get_overrides_of : Sil.tenv -> Sil.typ -> Procname.t -> (typ * Procname.t) list +val get_overrides_of : Tenv.t -> Sil.typ -> Procname.t -> (typ * Procname.t) list diff --git a/infer/src/backend/rearrange.mli b/infer/src/backend/rearrange.mli index 21f22c2b1..366580685 100644 --- a/infer/src/backend/rearrange.mli +++ b/infer/src/backend/rearrange.mli @@ -26,6 +26,6 @@ val check_call_to_objc_block_error : It returns an iterator with [lexp |-> strexp: typ] as current predicate and the path (an [offsetlist]) which leads to [lexp] as the iterator state. *) val rearrange : - ?report_deref_errors:bool -> Cfg.Procdesc.t -> Sil.tenv -> Sil.exp -> + ?report_deref_errors:bool -> Cfg.Procdesc.t -> Tenv.t -> Sil.exp -> Sil.typ -> Prop.normal Prop.t -> Location.t -> (Sil.offset list) Prop.prop_iter list diff --git a/infer/src/backend/state.ml b/infer/src/backend/state.ml index ab0704880..b902de8c9 100644 --- a/infer/src/backend/state.ml +++ b/infer/src/backend/state.ml @@ -51,7 +51,7 @@ type t = { mutable last_path : (Paths.Path.t * (Sil.path_pos option)) option; (** Last prop,tenv,pdesc seen *) - mutable last_prop_tenv_pdesc : (Prop.normal Prop.t * Sil.tenv * Cfg.Procdesc.t) option; + mutable last_prop_tenv_pdesc : (Prop.normal Prop.t * Tenv.t * Cfg.Procdesc.t) option; (** Last session seen *) mutable last_session : int; @@ -272,7 +272,8 @@ let extract_pre p tenv pdesc abstract_fun = (** return the normalized precondition extracted form the last prop seen, if any the abstraction function is a parameter to get around module dependencies *) -let get_normalized_pre (abstract_fun : Sil.tenv -> Prop.normal Prop.t -> Prop.normal Prop.t) : Prop.normal Prop.t option = +let get_normalized_pre (abstract_fun : Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t) + : Prop.normal Prop.t option = match get_prop_tenv_pdesc () with | None -> None | Some (prop, tenv, pdesc) -> diff --git a/infer/src/backend/state.mli b/infer/src/backend/state.mli index 75023b0cd..959df4beb 100644 --- a/infer/src/backend/state.mli +++ b/infer/src/backend/state.mli @@ -53,7 +53,8 @@ val get_node_id_key : unit -> int * int (** return the normalized precondition extracted form the last prop seen, if any the abstraction function is a parameter to get around module dependencies *) -val get_normalized_pre : (Sil.tenv -> Prop.normal Prop.t -> Prop.normal Prop.t) -> Prop.normal Prop.t option +val get_normalized_pre : + (Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t) -> Prop.normal Prop.t option (** Get last path seen in symbolic execution *) val get_path : unit -> Paths.Path.t * (Sil.path_pos option) @@ -62,7 +63,7 @@ val get_path : unit -> Paths.Path.t * (Sil.path_pos option) val get_path_pos : unit -> Sil.path_pos (** Get last last prop,tenv,pdesc seen in symbolic execution *) -val get_prop_tenv_pdesc : unit -> (Prop.normal Prop.t * Sil.tenv * Cfg.Procdesc.t) option +val get_prop_tenv_pdesc : unit -> (Prop.normal Prop.t * Tenv.t * Cfg.Procdesc.t) option (** Get last session seen in symbolic execution *) val get_session : unit -> int @@ -125,7 +126,7 @@ val set_node : Cfg.node -> unit val set_path : Paths.Path.t -> Sil.path_pos option -> unit (** Set last prop,tenv,pdesc seen in symbolic execution *) -val set_prop_tenv_pdesc : Prop.normal Prop.t -> Sil.tenv -> Cfg.Procdesc.t -> unit +val set_prop_tenv_pdesc : Prop.normal Prop.t -> Tenv.t -> Cfg.Procdesc.t -> unit (** Set last session seen in symbolic execution *) val set_session : int -> unit diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 8b7733c0b..6d488d0ed 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -20,7 +20,7 @@ let rec fldlist_assoc fld = function let rec unroll_type tenv typ off = match (typ, off) with | Sil.Tvar _, _ -> - let typ' = Sil.expand_type tenv typ in + let typ' = Tenv.expand_type tenv typ in unroll_type tenv typ' off | Sil.Tstruct { Sil.instance_fields; static_fields }, Sil.Off_fld (fld, _) -> begin @@ -102,7 +102,8 @@ let rec apply_offlist Ident.fieldname_is_hidden fieldname | _ -> false in let inst_new = match inst with - | Sil.Ilookup when inst_is_uninitialized inst_curr && not (is_hidden_field()) -> (* we are in a lookup of an uninitialized value *) + | Sil.Ilookup when inst_is_uninitialized inst_curr && not (is_hidden_field()) -> + (* we are in a lookup of an uninitialized value *) lookup_inst := Some inst_curr; let alloc_attribute_opt = if inst_curr = Sil.Iinitial then None @@ -137,7 +138,7 @@ let rec apply_offlist pdesc tenv p fp_root nullify_struct (root_lexp, strexp, typ) offlist_new f inst lookup_inst | (Sil.Off_fld (fld, fld_typ)):: offlist', Sil.Estruct (fsel, inst') -> begin - let typ' = Sil.expand_type tenv typ in + let typ' = Tenv.expand_type tenv typ in let struct_typ = match typ' with | Sil.Tstruct struct_typ -> @@ -170,7 +171,7 @@ let rec apply_offlist | (Sil.Off_index idx):: offlist', Sil.Earray (size, esel, inst1) -> let nidx = Prop.exp_normalize_prop p idx in begin - let typ' = Sil.expand_type tenv typ in + let typ' = Tenv.expand_type tenv typ in let t', size' = match typ' with Sil.Tarray (t', size') -> (t', size') | _ -> assert false in try let idx_ese', se' = IList.find (fun ese -> Prover.check_equal p nidx (fst ese)) esel in @@ -178,12 +179,17 @@ let rec apply_offlist apply_offlist pdesc tenv p fp_root nullify_struct (root_lexp, se', t') offlist' f inst lookup_inst in - let replace_ese ese = if Sil.exp_equal idx_ese' (fst ese) then (idx_ese', res_se') else ese in + let replace_ese ese = + if Sil.exp_equal idx_ese' (fst ese) + then (idx_ese', res_se') + else ese in let res_se = Sil.Earray(size, IList.map replace_ese esel, inst1) in let res_t = Sil.Tarray(res_t', size') in (res_e', res_se, res_t, res_pred_insts_op') - with Not_found -> (* return a nondeterministic value if the index is not found after rearrangement *) - L.d_str "apply_offlist: index "; Sil.d_exp idx; L.d_strln " not materialized -- returning nondeterministic value"; + with Not_found -> + (* return a nondeterministic value if the index is not found after rearrangement *) + L.d_str "apply_offlist: index "; Sil.d_exp idx; + L.d_strln " not materialized -- returning nondeterministic value"; let res_e' = Sil.Var (Ident.create_fresh Ident.kprimed) in (res_e', strexp, typ, None) end @@ -366,7 +372,9 @@ let dangerous_functions = let check_inherently_dangerous_function caller_pname callee_pname = if IList.exists (Procname.equal callee_pname) !dangerous_functions then - let exn = Exceptions.Inherently_dangerous_function (Localise.desc_inherently_dangerous_function callee_pname) in + let exn = + Exceptions.Inherently_dangerous_function + (Localise.desc_inherently_dangerous_function callee_pname) in let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop caller_pname) in Reporting.log_warning caller_pname ~pre: pre_opt exn @@ -394,7 +402,9 @@ let check_constant_string_dereference lexp = | Sil.BinOp(Sil.PlusPI, Sil.Const (Sil.Cstr s), e) | Sil.Lindex (Sil.Const (Sil.Cstr s), e) -> let value = match e with - | Sil.Const (Sil.Cint n) when Sil.Int.geq n Sil.Int.zero && Sil.Int.leq n (Sil.Int.of_int (String.length s)) -> + | Sil.Const (Sil.Cint n) + when Sil.Int.geq n Sil.Int.zero && + Sil.Int.leq n (Sil.Int.of_int (String.length s)) -> string_lookup s n | _ -> Sil.exp_get_undefined false in Some value @@ -449,17 +459,21 @@ let check_already_dereferenced pname cond prop = None in match dereferenced_line with | Some (id, (n, _)) -> - let desc = Errdesc.explain_null_test_after_dereference (Sil.Var id) (State.get_node ()) n (State.get_loc ()) in + let desc = + Errdesc.explain_null_test_after_dereference + (Sil.Var id) (State.get_node ()) n (State.get_loc ()) in let exn = (Exceptions.Null_test_after_dereference (desc, __POS__)) in let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in Reporting.log_warning pname ~pre: pre_opt exn | None -> () -(** Check whether symbolic execution de-allocated a stack variable or a constant string, raising an exception in that case *) +(** Check whether symbolic execution de-allocated a stack variable or a constant string, + raising an exception in that case *) let check_deallocate_static_memory prop_after = let check_deallocated_attribute = function - | Sil.Lvar pv, Sil.Aresource ({ Sil.ra_kind = Sil.Rrelease } as ra) when Sil.pvar_is_local pv || Sil.pvar_is_global pv -> + | Sil.Lvar pv, Sil.Aresource ({ Sil.ra_kind = Sil.Rrelease } as ra) + when Sil.pvar_is_local pv || Sil.pvar_is_global pv -> let freed_desc = Errdesc.explain_deallocate_stack_var pv ra in raise (Exceptions.Deallocate_stack_variable freed_desc) | Sil.Const (Sil.Cstr s), Sil.Aresource ({ Sil.ra_kind = Sil.Rrelease } as ra) -> @@ -487,7 +501,7 @@ let resolve_method tenv class_name proc_name = visited := Typename.Set.add class_name !visited; let right_proc_name = Procname.replace_class proc_name (Typename.name class_name) in - match Sil.tenv_lookup tenv class_name with + match Tenv.lookup tenv class_name with | Some { Sil.csu = Csu.Class _; def_methods; superclasses } -> if method_exists right_proc_name def_methods then Some right_proc_name @@ -542,7 +556,7 @@ let lookup_java_typ_from_string tenv typ_str = | typ_str -> (* non-primitive/non-array type--resolve it in the tenv *) let typename = Typename.TN_csu (Csu.Class Csu.Java, (Mangled.from_string typ_str)) in - match Sil.tenv_lookup tenv typename with + match Tenv.lookup tenv typename with | Some struct_typ -> Sil.Tstruct struct_typ | _ -> raise (Cannot_convert_string_to_typ typ_str) in loop typ_str @@ -704,7 +718,12 @@ let call_constructor_url_update_args pname actual_params = let parts = Str.split (Str.regexp_string "://") s in (match parts with | frst:: _ -> - if (frst = "http") || (frst = "ftp") || (frst = "https") || (frst = "mailto") || (frst = "jar") then + if frst = "http" || + frst = "ftp" || + frst = "https" || + frst = "mailto" || + frst = "jar" + then [this; (Sil.Const (Sil.Cstr frst), atype)] else actual_params | _ -> actual_params) @@ -718,14 +737,21 @@ let call_constructor_url_update_args pname actual_params = (* getters and setters using a builtin. *) let handle_objc_method_call actual_pars actual_params pre tenv ret_ids pdesc callee_pname loc path exec_call = - let path_description = "Message "^(Procname.to_simplified_string callee_pname)^" with receiver nil returns nil." in + let path_description = + "Message " ^ + (Procname.to_simplified_string callee_pname) ^ + " with receiver nil returns nil." in let receiver = (match actual_pars with | (e, _):: _ -> e - | _ -> raise (Exceptions.Internal_error - (Localise.verbatim_desc "In Objective-C instance method call there should be a receiver."))) in + | _ -> raise + (Exceptions.Internal_error + (Localise.verbatim_desc + "In Objective-C instance method call there should be a receiver."))) in let is_receiver_null = match actual_pars with - | (e, _):: _ when Sil.exp_equal e Sil.exp_zero || Option.is_some (Prop.get_objc_null_attribute pre e) -> true + | (e, _) :: _ + when Sil.exp_equal e Sil.exp_zero || + Option.is_some (Prop.get_objc_null_attribute pre e) -> true | _ -> false in let add_objc_null_attribute_or_nullify_result prop = match ret_ids with @@ -735,11 +761,17 @@ let handle_objc_method_call actual_pars actual_params pre tenv ret_ids pdesc cal Prop.add_or_replace_exp_attribute prop (Sil.Var ret_id) (Sil.Aobjc_null info) | None -> Prop.conjoin_eq (Sil.Var ret_id) Sil.exp_zero prop) | _ -> prop in - if is_receiver_null then (* objective-c instance method with a null receiver just return objc_null(res) *) + if is_receiver_null + then (* objective-c instance method with a null receiver just return objc_null(res) *) let path = Paths.Path.add_description path path_description in - L.d_strln ("Object-C method " ^ Procname.to_string callee_pname^ " called with nil receiver. Returning 0/nil"); - (* We wish to nullify the result. However, in some cases, we want to add the attribute OBJC_NULL to it so that we *) - (* can keep track of how this object became null, so that in a NPE we can separate it into a different error type *) + L.d_strln + ("Object-C method " ^ + Procname.to_string callee_pname ^ + " called with nil receiver. Returning 0/nil"); + (* We wish to nullify the result. However, in some cases, + we want to add the attribute OBJC_NULL to it so that we *) + (* can keep track of how this object became null, + so that in a NPE we can separate it into a different error type *) [(add_objc_null_attribute_or_nullify_result pre, path)] else let res = exec_call tenv ret_ids pdesc callee_pname loc actual_params pre path in @@ -978,9 +1010,12 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path let check_condition_always_true_false () = let report_condition_always_true_false i = let skip_loop = match ik with - | Sil.Ik_while | Sil.Ik_for -> not (Sil.Int.iszero i) (* skip wile(1) and for (;1;) *) - | Sil.Ik_dowhile -> true (* skip do..while *) - | Sil.Ik_land_lor -> true (* skip subpart of a condition obtained from compilation of && and || *) + | Sil.Ik_while | Sil.Ik_for -> + not (Sil.Int.iszero i) (* skip wile(1) and for (;1;) *) + | Sil.Ik_dowhile -> + true (* skip do..while *) + | Sil.Ik_land_lor -> + true (* skip subpart of a condition obtained from compilation of && and || *) | _ -> false in true_branch && not skip_loop in (* in comparisons, nil is translated as (void * ) 0 rather than 0 *) @@ -1150,10 +1185,12 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path Rearrange.check_call_to_objc_block_error current_pdesc prop_r fun_exp loc; Rearrange.check_dereference_error current_pdesc prop_r fun_exp loc; if call_flags.Sil.cf_noreturn then begin - L.d_str "Unknown function pointer with noreturn attribute "; Sil.d_exp fun_exp; L.d_strln ", diverging."; + L.d_str "Unknown function pointer with noreturn attribute "; + Sil.d_exp fun_exp; L.d_strln ", diverging."; execute_diverge prop_r path end else begin - L.d_str "Unknown function pointer "; Sil.d_exp fun_exp; L.d_strln ", returning undefined value."; + L.d_str "Unknown function pointer "; Sil.d_exp fun_exp; + L.d_strln ", returning undefined value."; let callee_pname = Procname.from_string_c_fun "__function_pointer__" in call_unknown_or_scan tenv false current_pdesc prop_r path ret_ids None n_actual_params callee_pname loc @@ -1210,7 +1247,8 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path let node_id = Sil.Int.to_int i in State.set_goto_node node_id; [(prop, path)] - | _ -> (* target not known, do nothing as the next nodes are set to the possible targets by the front-end *) + | _ -> (* target not known, do nothing as the next nodes + are set to the possible targets by the front-end *) [(prop, path)] end and execute_diverge prop path = @@ -1228,7 +1266,9 @@ and sym_exec_generated mask_errors tenv pdesc instrs ppl = let loc = (match ml_source with | Some ml_loc -> "at " ^ (ml_loc_to_string ml_loc) | None -> "") in - L.d_warning ("Generated Instruction Failed with: " ^ (Localise.to_string err_name)^loc ); L.d_ln(); + L.d_warning + ("Generated Instruction Failed with: " ^ + (Localise.to_string err_name)^loc ); L.d_ln(); [(p, path)] in let f plist instr = IList.flatten (IList.map (exe_instr instr) plist) in IList.fold_left f ppl instrs @@ -1271,7 +1311,9 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call add_to_footprint abducted_ref_pv typ prop in prop', Sil.Eexp (fresh_fp_var, Sil.Inone) | typ -> - failwith ("No need for abduction on non-pointer type " ^ (Sil.typ_to_string typ)) in + failwith + ("No need for abduction on non-pointer type " ^ + (Sil.typ_to_string typ)) in (* replace [actual] |-> _ with [actual] |-> [fresh_fp_var] *) let filtered_sigma = IList.map @@ -1454,9 +1496,9 @@ and sym_exec_objc_getter field_name ret_typ_opt tenv ret_ids pdesc pname loc arg | None -> assert false in match args with | [(lexp, typ)] -> - let typ' = (match Sil.expand_type tenv typ with + let typ' = (match Tenv.expand_type tenv typ with | Sil.Tstruct _ as s -> s - | Sil.Tptr (t, _) -> Sil.expand_type tenv t + | Sil.Tptr (t, _) -> Tenv.expand_type tenv t | _ -> assert false) in let field_access_exp = Sil.Lfield (lexp, field_name, typ') in execute_letderef @@ -1468,9 +1510,9 @@ and sym_exec_objc_setter field_name _ tenv _ pdesc pname loc args prop = (Ident.fieldname_to_string field_name)^"."); match args with | (lexp1, typ1) :: (lexp2, typ2)::_ -> - let typ1' = (match Sil.expand_type tenv typ1 with + let typ1' = (match Tenv.expand_type tenv typ1 with | Sil.Tstruct _ as s -> s - | Sil.Tptr (t, _) -> Sil.expand_type tenv t + | Sil.Tptr (t, _) -> Tenv.expand_type tenv t | _ -> assert false) in let field_access_exp = Sil.Lfield (lexp1, field_name, typ1') in execute_set ~report_deref_errors:false pname pdesc tenv field_access_exp typ2 lexp2 loc prop @@ -1493,7 +1535,8 @@ and sym_exec_call pdesc tenv pre path ret_ids actual_pars summary loc = let caller_pname = Cfg.Procdesc.get_proc_name pdesc in let callee_pname = Specs.get_proc_name summary in let ret_typ = Specs.get_ret_type summary in - let check_return_value_ignored () = (* check if the return value of the call is ignored, and issue a warning *) + let check_return_value_ignored () = + (* check if the return value of the call is ignored, and issue a warning *) let is_ignored = match ret_typ, ret_ids with | Sil.Tvoid, _ -> false | Sil.Tint _, _ when not (proc_is_defined callee_pname) -> @@ -1521,7 +1564,9 @@ and sym_exec_call pdesc tenv pre path ret_ids actual_pars summary loc = Errdesc.warning_err (State.get_loc ()) "likely use of variable-arguments function, or function prototype missing@."; - L.d_warning "likely use of variable-arguments function, or function prototype missing"; L.d_ln(); + L.d_warning + "likely use of variable-arguments function, or function prototype missing"; + L.d_ln(); L.d_str "actual parameters: "; Sil.d_exp_list (IList.map fst actual_pars); L.d_ln (); L.d_str "formal parameters: "; Sil.d_typ_list formal_types; L.d_ln (); actual_pars @@ -1558,7 +1603,9 @@ and sym_exec_wrapper handle_exn tenv pdesc instr ((prop: Prop.normal Prop.t), pa let ids_primed = Sil.fav_to_list fav in let ids_primed_normal = IList.map (fun id -> (id, Ident.create_fresh Ident.knormal)) ids_primed in - let ren_sub = Sil.sub_of_list (IList.map (fun (id1, id2) -> (id1, Sil.Var id2)) ids_primed_normal) in + let ren_sub = + Sil.sub_of_list (IList.map + (fun (id1, id2) -> (id1, Sil.Var id2)) ids_primed_normal) in let p' = Prop.normalize (Prop.prop_sub ren_sub p) in let fav_normal = Sil.fav_from_list (IList.map snd ids_primed_normal) in p', fav_normal in @@ -1630,7 +1677,8 @@ let lifted_sym_exec let pset2 = if Tabulation.prop_is_exn pname p && not (Sil.instr_is_auxiliary instr) && Cfg.Node.get_kind node <> Cfg.Node.exn_handler_kind - (* skip normal instructions if an exception was thrown, unless this is an exception handler node *) + (* skip normal instructions if an exception was thrown, + unless this is an exception handler node *) then begin L.d_str "Skipping instr "; Sil.d_instr instr; L.d_strln " due to exception"; @@ -1794,7 +1842,8 @@ module ModelBuiltins = struct Option.is_some (Prop.get_undef_attribute prop n_lexp) in is_undef && (!Config.angelic_execution || !Config.optimistic_cast) - (** Creates an object in the heap with a given type, when the object is not known to be null or when it doesn't + (** Creates an object in the heap with a given type, + when the object is not known to be null or when it doesn't appear already in the heap. *) let create_type tenv n_lexp typ prop = let prop_type = @@ -1808,7 +1857,7 @@ module ModelBuiltins = struct match typ with | Sil.Tptr (typ', _) -> let sexp = Sil.Estruct ([], Sil.inst_none) in - let typ'' = Sil.expand_type tenv typ' in + let typ'' = Tenv.expand_type tenv typ' in let texp = Sil.Sizeof (typ'', Sil.Subtype.subtypes) in let hpred = Prop.mk_ptsto n_lexp sexp texp in Some hpred @@ -1973,7 +2022,12 @@ module ModelBuiltins = struct (Sil.Aresource { ra with Sil.ra_res = ra_res }) | _ -> ( let pname = Sil.mem_alloc_pname Sil.Mnew in - let ra = { Sil.ra_kind = Sil.Racquire; Sil.ra_res = ra_res; Sil.ra_pname = pname; Sil.ra_loc = loc; Sil.ra_vpath = None } in + let ra = + { Sil.ra_kind = Sil.Racquire; + Sil.ra_res = ra_res; + Sil.ra_pname = pname; + Sil.ra_loc = loc; + Sil.ra_vpath = None } in Prop.add_or_replace_exp_attribute prop n_lexp (Sil.Aresource ra)) in [(prop', path)] @@ -1997,7 +2051,8 @@ module ModelBuiltins = struct set_resource_attribute prop path n_lexp loc Sil.Rlock | _ -> raise (Exceptions.Wrong_argument_number __POS__) - (** Set the resource attribute of the first real argument of method as ignore, the first argument is assumed to be "this" *) + (** Set the resource attribute of the first real argument of method as ignore, + the first argument is assumed to be "this" *) let execute___method_set_ignore_attribute { Builtin.pdesc; prop_; path; ret_ids; args; loc; } : Builtin.ret_typ = @@ -2044,7 +2099,8 @@ module ModelBuiltins = struct let filter_fld_hidden (f, _ ) = Ident.fieldname_is_hidden f in let has_fld_hidden fsel = IList.exists filter_fld_hidden fsel in let do_hpred in_foot hpred = match hpred with - | Sil.Hpointsto(e, Sil.Estruct (fsel, inst), texp) when Sil.exp_equal e n_lexp && (not (has_fld_hidden fsel)) -> + | Sil.Hpointsto(e, Sil.Estruct (fsel, inst), texp) + when Sil.exp_equal e n_lexp && (not (has_fld_hidden fsel)) -> let foot_e = Lazy.force foot_var in ret_val := Some foot_e; let se = Sil.Eexp(foot_e, Sil.inst_none) in @@ -2066,7 +2122,8 @@ module ModelBuiltins = struct [(prop'', path)] | _ -> raise (Exceptions.Wrong_argument_number __POS__) - (** take a pointer to a struct and a value, and set a hidden field in the struct to the given value *) + (** take a pointer to a struct and a value, + and set a hidden field in the struct to the given value *) let execute___set_hidden_field { Builtin.pdesc; prop_; path; args; } : Builtin.ret_typ = match args with @@ -2078,11 +2135,15 @@ module ModelBuiltins = struct let filter_fld_hidden (f, _ ) = Ident.fieldname_is_hidden f in let has_fld_hidden fsel = IList.exists filter_fld_hidden fsel in let do_hpred in_foot hpred = match hpred with - | Sil.Hpointsto(e, Sil.Estruct (fsel, inst), texp) when Sil.exp_equal e n_lexp1 && not in_foot -> + | Sil.Hpointsto(e, Sil.Estruct (fsel, inst), texp) + when Sil.exp_equal e n_lexp1 && not in_foot -> let se = Sil.Eexp(n_lexp2, Sil.inst_none) in - let fsel' = (Ident.fieldname_hidden, se) :: (IList.filter (fun x -> not (filter_fld_hidden x)) fsel) in + let fsel' = + (Ident.fieldname_hidden, se) :: + (IList.filter (fun x -> not (filter_fld_hidden x)) fsel) in Sil.Hpointsto(e, Sil.Estruct (fsel', inst), texp) - | Sil.Hpointsto(e, Sil.Estruct (fsel, inst), texp) when Sil.exp_equal e n_lexp1 && in_foot && not (has_fld_hidden fsel) -> + | Sil.Hpointsto(e, Sil.Estruct (fsel, inst), texp) + when Sil.exp_equal e n_lexp1 && in_foot && not (has_fld_hidden fsel) -> let foot_e = Lazy.force foot_var in let se = Sil.Eexp(foot_e, Sil.inst_none) in let fsel' = (Ident.fieldname_hidden, se) :: fsel in @@ -2103,11 +2164,13 @@ module ModelBuiltins = struct : Builtin.ret_typ = match args with | [(lexp, typ)] -> - let typ' = (match Sil.expand_type tenv typ with + let typ' = (match Tenv.expand_type tenv typ with | Sil.Tstruct _ as s -> s - | Sil.Tptr(t, _) -> Sil.expand_type tenv t + | Sil.Tptr(t, _) -> Tenv.expand_type tenv t | s' -> - L.d_str ("Trying to update hidden field of not a struc. Type: "^(Sil.typ_to_string s')); + L.d_str + ("Trying to update hidden field of not a struc. Type: " ^ + (Sil.typ_to_string s')); assert false) in (* Assumes that lexp is a temp n$1 that has the value of the object. *) (* This is the case as a call f(o) it's translates as n$1=*&o; f(n$1) *) @@ -2128,8 +2191,10 @@ module ModelBuiltins = struct suppress_npe_report tenv pdesc update_counter_instrs [(prop_, path)] | _ -> raise (Exceptions.Wrong_argument_number __POS__) - (* Given a list of args checks if the first is the flag indicating whether is a call to retain/release for which*) - (* we have to suppress NPE report or not. If the flag is present it is removed from the list of args. *) + (* Given a list of args checks if the first is the flag + indicating whether is a call to retain/release for which*) + (* we have to suppress NPE report or not. + If the flag is present it is removed from the list of args. *) let get_suppress_npe_flag args = match args with | (Sil.Const (Sil.Cint i), Sil.Tint Sil.IBool):: args' when Sil.Int.isone i -> @@ -2311,7 +2376,12 @@ module ModelBuiltins = struct | (Sil.Hpointsto(lexp, _, _), []) -> let prop = Prop.prop_iter_remove_curr_then_to_prop iter in let pname = Sil.mem_dealloc_pname mk in - let ra = { Sil.ra_kind = Sil.Rrelease; Sil.ra_res = Sil.Rmemory mk; Sil.ra_pname = pname; Sil.ra_loc = loc; Sil.ra_vpath = None } in + let ra = + { Sil.ra_kind = Sil.Rrelease; + Sil.ra_res = Sil.Rmemory mk; + Sil.ra_pname = pname; + Sil.ra_loc = loc; + Sil.ra_vpath = None } in (* mark value as freed *) let p_res = Prop.add_or_replace_exp_attribute_check_changed @@ -2403,7 +2473,12 @@ module ModelBuiltins = struct let prop_plus_ptsto = let pname = Sil.mem_alloc_pname mk in let prop' = Prop.normalize (Prop.prop_sigma_star prop [ptsto_new]) in - let ra = { Sil.ra_kind = Sil.Racquire; Sil.ra_res = Sil.Rmemory mk; Sil.ra_pname = pname; Sil.ra_loc = loc; Sil.ra_vpath = None } in + let ra = + { Sil.ra_kind = Sil.Racquire; + Sil.ra_res = Sil.Rmemory mk; + Sil.ra_pname = pname; + Sil.ra_loc = loc; + Sil.ra_vpath = None } in (* mark value as allocated *) Prop.add_or_replace_exp_attribute prop' exp_new (Sil.Aresource ra) in let prop_alloc = Prop.conjoin_eq (Sil.Var ret_id) exp_new prop_plus_ptsto in @@ -2455,7 +2530,8 @@ module ModelBuiltins = struct pdesc tenv prop_ path ret_ids [(routine_arg, snd arg)] callee_summary loc end | _ -> - L.d_str "pthread_create: unknown function "; Sil.d_exp routine_name; L.d_strln ", skipping call."; + L.d_str "pthread_create: unknown function "; + Sil.d_exp routine_name; L.d_strln ", skipping call."; [(prop_, path)]) | _ -> raise (Exceptions.Wrong_argument_number __POS__) @@ -2686,10 +2762,10 @@ module ModelBuiltins = struct "__set_untaint_attribute" (execute___set_attr Sil.Auntaint) let __set_locked_attribute = Builtin.register (* set the attribute of the parameter as locked *) - "__set_locked_attribute" execute___set_locked_attribute + "__set_locked_attribute" execute___set_locked_attribute let __set_unlocked_attribute = Builtin.register (* set the attribute of the parameter as unlocked *) - "__set_unlocked_attribute" execute___set_unlocked_attribute + "__set_unlocked_attribute" execute___set_unlocked_attribute let _ = Builtin.register "__throw" execute_skip let __unwrap_exception = Builtin.register @@ -2763,7 +2839,7 @@ module ModelBuiltins = struct ({ Builtin.tenv; } as builtin_args) symb_state = let nsarray_typ_ = Sil.Tvar (Typename.TN_csu (Csu.Class Csu.Objc, Mangled.from_string "NSArray")) in - let nsarray_typ = Sil.expand_type tenv nsarray_typ_ in + let nsarray_typ = Tenv.expand_type tenv nsarray_typ_ in execute_objc_alloc_no_fail symb_state nsarray_typ builtin_args let execute_NSArray_arrayWithObjects_count builtin_args = @@ -2795,7 +2871,7 @@ module ModelBuiltins = struct let nsdictionary_typ_ = Sil.Tvar (Typename.TN_csu (Csu.Class Csu.Objc, Mangled.from_string "NSDictionary")) in let nsdictionary_typ = - Sil.expand_type tenv nsdictionary_typ_ in + Tenv.expand_type tenv nsdictionary_typ_ in execute_objc_alloc_no_fail symb_state nsdictionary_typ builtin_args let execute___objc_dictionary_literal builtin_args = diff --git a/infer/src/backend/symExec.mli b/infer/src/backend/symExec.mli index f2476f4ce..402eb6fb0 100644 --- a/infer/src/backend/symExec.mli +++ b/infer/src/backend/symExec.mli @@ -11,17 +11,17 @@ (** Symbolic Execution *) (** Lookup Java types by name. *) -val lookup_java_typ_from_string : Sil.tenv -> string -> Sil.typ +val lookup_java_typ_from_string : Tenv.t -> string -> Sil.typ (** symbolic execution on the level of sets of propositions *) -val lifted_sym_exec : (exn -> unit) -> Sil.tenv -> Cfg.Procdesc.t -> +val lifted_sym_exec : (exn -> unit) -> Tenv.t -> Cfg.Procdesc.t -> Paths.PathSet.t -> Cfg.Node.t -> Sil.instr list -> Paths.PathSet.t (** OO method resolution: given a class name and a method name, climb the class hierarchy to find * the procname that the method name will actually resolve to at runtime. For example, if we have * a procname like Foo.toString() and Foo does not override toString(), we must resolve the call to * toString(). We will end up with Super.toString() where Super is some superclass of Foo. *) -val resolve_method : Sil.tenv -> Typename.t -> Procname.t -> Procname.t +val resolve_method : Tenv.t -> Typename.t -> Procname.t -> Procname.t (** {2 Functions for handling builtins } *) module ModelBuiltins : sig diff --git a/infer/src/backend/tabulation.mli b/infer/src/backend/tabulation.mli index 13a5057d4..c7c488aa2 100644 --- a/infer/src/backend/tabulation.mli +++ b/infer/src/backend/tabulation.mli @@ -42,7 +42,7 @@ val d_splitting : splitting -> unit (** Execute the function call and return the list of results with return value *) val exe_function_call: - Sil.tenv -> Ident.t list -> Cfg.Procdesc.t -> Procname.t -> Location.t -> + Tenv.t -> Ident.t list -> Cfg.Procdesc.t -> Procname.t -> Location.t -> (Sil.exp * Sil.typ) list -> Prop.normal Prop.t -> Paths.Path.t -> (Prop.normal Prop.t * Paths.Path.t) list diff --git a/infer/src/checkers/README.md b/infer/src/checkers/README.md new file mode 100644 index 000000000..4f98a712a --- /dev/null +++ b/infer/src/checkers/README.md @@ -0,0 +1,9 @@ +# Checkers + +Checkers is an infrastructure to facitilate writing lightweight checks starting from the Intermediate Representation [IR](../IR/README.md) of a project. + +Module [Checkers](checkers.mli) contains a number of sample checkers. + +Individual checkers can be activated using module [RegisterCheckers](registercheckers.ml). + + diff --git a/infer/src/checkers/callbackChecker.ml b/infer/src/checkers/callbackChecker.ml index 578b70df6..08267f18c 100644 --- a/infer/src/checkers/callbackChecker.ml +++ b/infer/src/checkers/callbackChecker.ml @@ -67,7 +67,7 @@ let callback_checker_main_java Typename.TN_csu (Csu.Class Csu.Java, Mangled.from_string (Procname.java_get_class_name proc_name_java)) in - match Sil.tenv_lookup tenv typename with + match Tenv.lookup tenv typename with | Some ({ struct_name = Some _; def_methods } as struct_typ) -> let typ = Sil.Tstruct struct_typ in let lifecycle_typs = get_or_create_lifecycle_typs tenv in diff --git a/infer/src/checkers/constantPropagation.mli b/infer/src/checkers/constantPropagation.mli index 9b8e6aac2..d11b81640 100644 --- a/infer/src/checkers/constantPropagation.mli +++ b/infer/src/checkers/constantPropagation.mli @@ -10,4 +10,4 @@ type const_map = Cfg.Node.t -> Sil.exp -> Sil.const option (** Build a const map lazily. *) -val build_const_map : Sil.tenv -> Cfg.Procdesc.t -> const_map +val build_const_map : Tenv.t -> Cfg.Procdesc.t -> const_map diff --git a/infer/src/checkers/dataflow.ml b/infer/src/checkers/dataflow.ml index 5d267be89..1c40cf4d6 100644 --- a/infer/src/checkers/dataflow.ml +++ b/infer/src/checkers/dataflow.ml @@ -21,7 +21,7 @@ module type DFStateType = sig val join : t -> t -> t (** Join two states (the old one is the first parameter). *) (** Perform a state transition on a node. *) - val do_node : Sil.tenv -> Cfg.Node.t -> t -> (t list) * (t list) + val do_node : Tenv.t -> Cfg.Node.t -> t -> (t list) * (t list) val proc_throws : Procname.t -> throws (** Can proc throw an exception? *) end @@ -35,7 +35,7 @@ module type DF = sig | Transition of state * state list * state list val join : state list -> state -> state - val run : Sil.tenv -> Cfg.Procdesc.t -> state -> (Cfg.Node.t -> transition) + val run : Tenv.t -> Cfg.Procdesc.t -> state -> (Cfg.Node.t -> transition) end (** Determine if the node can throw an exception. *) diff --git a/infer/src/checkers/dataflow.mli b/infer/src/checkers/dataflow.mli index 0fe947cd5..0ce0f0063 100644 --- a/infer/src/checkers/dataflow.mli +++ b/infer/src/checkers/dataflow.mli @@ -19,7 +19,7 @@ module type DFStateType = sig val join : t -> t -> t (** Join two states (the old one is the first parameter). *) (** Perform a state transition on a node. *) - val do_node : Sil.tenv -> Cfg.Node.t -> t -> (t list) * (t list) + val do_node : Tenv.t -> Cfg.Node.t -> t -> (t list) * (t list) val proc_throws : Procname.t -> throws (** Can proc throw an exception? *) end @@ -34,7 +34,7 @@ module type DF = sig val join : state list -> state -> state (** Run the dataflow analysis on a procedure starting from the given state. Returns a function to lookup the results of the analysis on every node *) - val run : Sil.tenv -> Cfg.Procdesc.t -> state -> (Cfg.Node.t -> transition) + val run : Tenv.t -> Cfg.Procdesc.t -> state -> (Cfg.Node.t -> transition) end (** Functor to create an instance of a dataflow analysis. *) diff --git a/infer/src/checkers/fragmentRetainsViewChecker.ml b/infer/src/checkers/fragmentRetainsViewChecker.ml index eb940365a..ad73ba579 100644 --- a/infer/src/checkers/fragmentRetainsViewChecker.ml +++ b/infer/src/checkers/fragmentRetainsViewChecker.ml @@ -27,7 +27,7 @@ let callback_fragment_retains_view_java let fld_typ_is_view = function | Sil.Tptr (Sil.Tvar tname, _) -> begin - match Sil.tenv_lookup tenv tname with + match Tenv.lookup tenv tname with | Some struct_typ -> AndroidFramework.is_view (Sil.Tstruct struct_typ) tenv | None -> false end @@ -40,7 +40,7 @@ let callback_fragment_retains_view_java begin let class_typename = Typename.Java.from_string (Procname.java_get_class_name pname_java) in - match Sil.tenv_lookup tenv class_typename with + match Tenv.lookup tenv class_typename with | Some ({ Sil.struct_name = Some _; instance_fields } as struct_typ) when AndroidFramework.is_fragment (Sil.Tstruct struct_typ) tenv -> let declared_view_fields = diff --git a/infer/src/checkers/patternMatch.ml b/infer/src/checkers/patternMatch.ml index dd7654c64..dc39d2538 100644 --- a/infer/src/checkers/patternMatch.ml +++ b/infer/src/checkers/patternMatch.ml @@ -73,7 +73,7 @@ let type_has_direct_supertype (typ : Sil.typ) (class_name : Typename.t) = IList.exists (fun cn -> Typename.equal cn class_name) (type_get_direct_supertypes typ) let type_has_supertype - (tenv: Sil.tenv) + (tenv: Tenv.t) (typ: Sil.typ) (class_name: Typename.t): bool = let rec has_supertype typ visited = @@ -81,13 +81,13 @@ let type_has_supertype false else begin - match Sil.expand_type tenv typ with + match Tenv.expand_type tenv typ with | Sil.Tptr (Sil.Tstruct { Sil.superclasses }, _) | Sil.Tstruct { Sil.superclasses } -> let match_supertype cn = let match_name () = Typename.equal cn class_name in let has_indirect_supertype () = - match Sil.tenv_lookup tenv cn with + match Tenv.lookup tenv cn with | Some supertype -> has_supertype (Sil.Tstruct supertype) (Sil.TypSet.add typ visited) | None -> false in @@ -255,14 +255,14 @@ let initializer_methods = [ (** Check if the type has in its supertypes from the initializer_classes list. *) let type_has_initializer - (tenv: Sil.tenv) + (tenv: Tenv.t) (t: Sil.typ): bool = let check_candidate class_name = type_has_supertype tenv t class_name in IList.exists check_candidate initializer_classes (** Check if the method is one of the known initializer methods. *) let method_is_initializer - (tenv: Sil.tenv) + (tenv: Tenv.t) (proc_attributes: ProcAttributes.t) : bool = match get_this_type proc_attributes with | Some this_type -> @@ -320,7 +320,7 @@ let proc_iter_overridden_methods f tenv proc_name = let do_super_type tenv super_class_name = let super_proc_name = Procname.replace_class proc_name (Typename.name super_class_name) in - match Sil.tenv_lookup tenv super_class_name with + match Tenv.lookup tenv super_class_name with | Some ({ Sil.def_methods }) -> let is_override pname = Procname.equal pname super_proc_name && @@ -337,7 +337,7 @@ let proc_iter_overridden_methods f tenv proc_name = let type_name = let class_name = Procname.java_get_class_name proc_name_java in Typename.TN_csu (Csu.Class Csu.Java, Mangled.from_string class_name) in - (match Sil.tenv_lookup tenv type_name with + (match Tenv.lookup tenv type_name with | Some curr_struct_typ -> IList.iter (do_super_type tenv) diff --git a/infer/src/checkers/patternMatch.mli b/infer/src/checkers/patternMatch.mli index e45cfc8e4..b1138f9e2 100644 --- a/infer/src/checkers/patternMatch.mli +++ b/infer/src/checkers/patternMatch.mli @@ -39,7 +39,7 @@ val has_formal_method_argument_type_names : Cfg.Procdesc.t -> Procname.java -> string list -> bool (** Check if the method is one of the known initializer methods. *) -val method_is_initializer : Sil.tenv -> ProcAttributes.t -> bool +val method_is_initializer : Tenv.t -> ProcAttributes.t -> bool (** Is this a getter proc name? *) val is_getter : Procname.java -> bool @@ -67,7 +67,7 @@ val proc_calls : (** Iterate over all the methods overridden by the procedure. Only Java supported at the moment. *) -val proc_iter_overridden_methods : (Procname.t -> unit) -> Sil.tenv -> Procname.t -> unit +val proc_iter_overridden_methods : (Procname.t -> unit) -> Tenv.t -> Procname.t -> unit val type_get_annotation : Sil.typ -> Sil.item_annotation option diff --git a/infer/src/clang/README.md b/infer/src/clang/README.md new file mode 100644 index 000000000..67aced4a2 --- /dev/null +++ b/infer/src/clang/README.md @@ -0,0 +1,5 @@ +# Clang Front-End + +This is the front-end for the clang compiler. + +The main entry point is [CMain](cmain.ml). \ No newline at end of file diff --git a/infer/src/clang/cContext.ml b/infer/src/clang/cContext.ml index f3460d6d2..72d5905cd 100644 --- a/infer/src/clang/cContext.ml +++ b/infer/src/clang/cContext.ml @@ -21,7 +21,7 @@ type curr_class = type t = { - tenv : Sil.tenv; + tenv : Tenv.t; cg : Cg.t; cfg : Cfg.cfg; procdesc : Cfg.Procdesc.t; @@ -116,7 +116,7 @@ let curr_class_hash curr_class = let create_curr_class tenv class_name ck = let class_tn_name = Typename.TN_csu (Csu.Class ck, (Mangled.from_string class_name)) in - match Sil.tenv_lookup tenv class_tn_name with + match Tenv.lookup tenv class_tn_name with | Some { Sil.superclasses } -> (let superclasses_names = IList.map Typename.name superclasses in match superclasses_names with diff --git a/infer/src/clang/cContext.mli b/infer/src/clang/cContext.mli index 6ddd6c9a0..b7674082c 100644 --- a/infer/src/clang/cContext.mli +++ b/infer/src/clang/cContext.mli @@ -19,7 +19,7 @@ type curr_class = type t = { - tenv : Sil.tenv; + tenv : Tenv.t; cg : Cg.t; cfg : Cfg.cfg; procdesc : Cfg.Procdesc.t; @@ -51,12 +51,12 @@ val curr_class_hash : curr_class -> int val is_objc_method : t -> bool -val get_tenv : t -> Sil.tenv +val get_tenv : t -> Tenv.t -val create_context : Sil.tenv -> Cg.t -> Cfg.cfg -> Cfg.Procdesc.t -> +val create_context : Tenv.t -> Cg.t -> Cfg.cfg -> Cfg.Procdesc.t -> curr_class -> Sil.typ option -> bool -> t option -> t -val create_curr_class : Sil.tenv -> string -> Csu.class_kind -> curr_class +val create_curr_class : Tenv.t -> string -> Csu.class_kind -> curr_class val add_block_static_var : t -> Procname.t -> (Sil.pvar * Sil.typ) -> unit diff --git a/infer/src/clang/cField_decl.ml b/infer/src/clang/cField_decl.ml index bb4f4eb38..bb726b22f 100644 --- a/infer/src/clang/cField_decl.ml +++ b/infer/src/clang/cField_decl.ml @@ -17,7 +17,7 @@ type field_type = Ident.fieldname * Sil.typ * (Sil.annotation * bool) list let rec get_fields_super_classes tenv super_class = Printing.log_out " ... Getting fields of superclass '%s'\n" (Typename.to_string super_class); - match Sil.tenv_lookup tenv super_class with + match Tenv.lookup tenv super_class with | None -> [] | Some { Sil.instance_fields; superclasses = super_class :: _ } -> let sc_fields = get_fields_super_classes tenv super_class in @@ -76,7 +76,7 @@ let rec get_fields type_ptr_to_sil_type tenv curr_class decl_list = let add_missing_fields tenv class_name ck fields = let mang_name = Mangled.from_string class_name in let class_tn_name = Typename.TN_csu (Csu.Class ck, mang_name) in - match Sil.tenv_lookup tenv class_tn_name with + match Tenv.lookup tenv class_tn_name with | Some ({ Sil.instance_fields } as struct_typ) -> let new_fields = General_utils.append_no_duplicates_fields instance_fields fields in let class_type_info = @@ -88,7 +88,7 @@ let add_missing_fields tenv class_name ck fields = struct_name = Some mang_name; } in Printing.log_out " Updating info for class '%s' in tenv\n" class_name; - Sil.tenv_add tenv class_tn_name class_type_info + Tenv.add tenv class_tn_name class_type_info | _ -> () (* checks if ivar is defined among a set of fields and if it is atomic *) diff --git a/infer/src/clang/cField_decl.mli b/infer/src/clang/cField_decl.mli index 2e6a915ad..9f5fdcb4b 100644 --- a/infer/src/clang/cField_decl.mli +++ b/infer/src/clang/cField_decl.mli @@ -12,18 +12,18 @@ open CFrontend_utils type field_type = Ident.fieldname * Sil.typ * (Sil.annotation * bool) list -val get_fields : Ast_utils.type_ptr_to_sil_type -> Sil.tenv -> CContext.curr_class -> +val get_fields : Ast_utils.type_ptr_to_sil_type -> Tenv.t -> CContext.curr_class -> Clang_ast_t.decl list -> field_type list val fields_superclass : - Sil.tenv -> Clang_ast_t.obj_c_interface_decl_info -> Csu.class_kind -> field_type list + Tenv.t -> Clang_ast_t.obj_c_interface_decl_info -> Csu.class_kind -> field_type list -val build_sil_field : Ast_utils.type_ptr_to_sil_type -> Sil.tenv -> Clang_ast_t.named_decl_info -> +val build_sil_field : Ast_utils.type_ptr_to_sil_type -> Tenv.t -> Clang_ast_t.named_decl_info -> Clang_ast_t.type_ptr -> Clang_ast_t.property_attribute list -> field_type -val add_missing_fields : Sil.tenv -> string -> Csu.class_kind -> field_type list -> unit +val add_missing_fields : Tenv.t -> string -> Csu.class_kind -> field_type list -> unit val is_ivar_atomic : Ident.fieldname -> Sil.struct_fields -> bool -val get_property_corresponding_ivar : Sil.tenv -> Ast_utils.type_ptr_to_sil_type -> string -> +val get_property_corresponding_ivar : Tenv.t -> Ast_utils.type_ptr_to_sil_type -> string -> Clang_ast_t.decl -> Ident.fieldname diff --git a/infer/src/clang/cFrontend.ml b/infer/src/clang/cFrontend.ml index 3c84f24a2..2b74ad92b 100644 --- a/infer/src/clang/cFrontend.ml +++ b/infer/src/clang/cFrontend.ml @@ -39,7 +39,7 @@ let init_global_state source_file = CFrontend_utils.General_utils.reset_block_counter () let do_source_file source_file ast = - let tenv = Sil.create_tenv () in + let tenv = Tenv.create () in CTypes_decl.add_predefined_types tenv; init_global_state source_file; Config.nLOC := FileLOC.file_get_loc (DB.source_file_to_string source_file); @@ -61,7 +61,7 @@ let do_source_file source_file ast = (* Printing.print_tenv tenv; *) (*Printing.print_procedures cfg; *) General_utils.sort_fields_tenv tenv; - Sil.store_tenv_to_file tenv_file tenv; + Tenv.store_to_file tenv_file tenv; if !CFrontend_config.stats_mode then Cfg.check_cfg_connectedness cfg; if !CFrontend_config.stats_mode || !CFrontend_config.debug_mode || !CFrontend_config.testing_mode then diff --git a/infer/src/clang/cFrontend_checkers.ml b/infer/src/clang/cFrontend_checkers.ml index d160cf527..b4e5586aa 100644 --- a/infer/src/clang/cFrontend_checkers.ml +++ b/infer/src/clang/cFrontend_checkers.ml @@ -108,7 +108,7 @@ let direct_atomic_property_access_warning context stmt_info ivar_name = Ast_utils.get_class_name_from_member n | _ -> Ident.create_fieldname (Mangled.from_string "") 0, "" in let tname = Typename.TN_csu (Csu.Class Csu.Objc, Mangled.from_string cname) in - let condition = match Sil.tenv_lookup tenv tname with + let condition = match Tenv.lookup tenv tname with | Some { Sil.instance_fields; static_fields } -> (* We give the warning when: (1) the property has the atomic attribute and diff --git a/infer/src/clang/cFrontend_decl.ml b/infer/src/clang/cFrontend_decl.ml index aef2905ab..8695ba64f 100644 --- a/infer/src/clang/cFrontend_decl.ml +++ b/infer/src/clang/cFrontend_decl.ml @@ -14,10 +14,11 @@ module L = Logging open CFrontend_utils module type CFrontend_decl = sig - val function_decl : Sil.tenv -> Cfg.cfg -> Cg.t -> Clang_ast_t.decl -> + val function_decl : Tenv.t -> Cfg.cfg -> Cg.t -> Clang_ast_t.decl -> CModule_type.block_data option -> unit - val translate_one_declaration : Sil.tenv -> Cg.t -> Cfg.cfg -> Clang_ast_t.decl -> Clang_ast_t.decl -> unit + val translate_one_declaration : + Tenv.t -> Cg.t -> Cfg.cfg -> Clang_ast_t.decl -> Clang_ast_t.decl -> unit end module CFrontend_decl_funct(T: CModule_type.CTranslation) : CFrontend_decl = @@ -176,8 +177,10 @@ struct (* di_parent_pointer has pointer to lexical context such as class.*) (* If it's not defined, then it's the same as parent in AST *) let class_decl = match decl_info.Clang_ast_t.di_parent_pointer with - | Some ptr -> Ast_utils.get_decl ptr - | None -> Some parent_dec in + | Some ptr -> + Ast_utils.get_decl ptr + | None -> + Some parent_dec in (match class_decl with | Some (CXXRecordDecl _ as d) | Some (ClassTemplateSpecializationDecl _ as d) -> @@ -185,33 +188,34 @@ struct let curr_class = CContext.ContextCls(class_name, None, []) in if !CFrontend_config.cxx_experimental then process_methods tenv cg cfg curr_class [dec] - | Some dec -> Printing.log_stats "Methods of %s skipped\n" (Ast_utils.string_of_decl dec) - | None -> ()) - | _ -> ()); - match dec with - (* Currently C/C++ record decl treated in the same way *) - | ClassTemplateSpecializationDecl (decl_info, _, _, _, decl_list, _, _, _) - | CXXRecordDecl (decl_info, _, _, _, decl_list, _, _, _) - | RecordDecl (decl_info, _, _, _, decl_list, _, _) when not decl_info.di_is_implicit -> - let is_method_decl decl = match decl with - | CXXMethodDecl _ | CXXConstructorDecl _ | CXXConversionDecl _ - | CXXDestructorDecl _ | FunctionTemplateDecl _ -> - true - | _ -> false in - let method_decls, no_method_decls = IList.partition is_method_decl decl_list in - IList.iter (translate_one_declaration tenv cg cfg dec) no_method_decls; - ignore (CTypes_decl.add_types_from_decl_to_tenv tenv dec); - IList.iter (translate_one_declaration tenv cg cfg dec) method_decls - | EnumDecl _ -> ignore (CEnum_decl.enum_decl dec) - | LinkageSpecDecl (_, decl_list, _) -> - Printing.log_out "ADDING: LinkageSpecDecl decl list\n"; - IList.iter (translate_one_declaration tenv cg cfg dec) decl_list - | NamespaceDecl (_, _, decl_list, _, _) -> - IList.iter (translate_one_declaration tenv cg cfg dec) decl_list - | ClassTemplateDecl (_, _, template_decl_info) - | FunctionTemplateDecl (_, _, template_decl_info) -> - let decl_list = template_decl_info.Clang_ast_t.tdi_specializations in - IList.iter (translate_one_declaration tenv cg cfg dec) decl_list - | _ -> () + | Some dec -> + Printing.log_stats "Methods of %s skipped\n" (Ast_utils.string_of_decl dec) + | None -> ()) + | _ -> ()); + match dec with + (* Currently C/C++ record decl treated in the same way *) + | ClassTemplateSpecializationDecl (decl_info, _, _, _, decl_list, _, _, _) + | CXXRecordDecl (decl_info, _, _, _, decl_list, _, _, _) + | RecordDecl (decl_info, _, _, _, decl_list, _, _) when not decl_info.di_is_implicit -> + let is_method_decl decl = match decl with + | CXXMethodDecl _ | CXXConstructorDecl _ | CXXConversionDecl _ + | CXXDestructorDecl _ | FunctionTemplateDecl _ -> + true + | _ -> false in + let method_decls, no_method_decls = IList.partition is_method_decl decl_list in + IList.iter (translate_one_declaration tenv cg cfg dec) no_method_decls; + ignore (CTypes_decl.add_types_from_decl_to_tenv tenv dec); + IList.iter (translate_one_declaration tenv cg cfg dec) method_decls + | EnumDecl _ -> ignore (CEnum_decl.enum_decl dec) + | LinkageSpecDecl (_, decl_list, _) -> + Printing.log_out "ADDING: LinkageSpecDecl decl list\n"; + IList.iter (translate_one_declaration tenv cg cfg dec) decl_list + | NamespaceDecl (_, _, decl_list, _, _) -> + IList.iter (translate_one_declaration tenv cg cfg dec) decl_list + | ClassTemplateDecl (_, _, template_decl_info) + | FunctionTemplateDecl (_, _, template_decl_info) -> + let decl_list = template_decl_info.Clang_ast_t.tdi_specializations in + IList.iter (translate_one_declaration tenv cg cfg dec) decl_list + | _ -> () end diff --git a/infer/src/clang/cFrontend_decl.mli b/infer/src/clang/cFrontend_decl.mli index 28e08df8b..1ffaa9104 100644 --- a/infer/src/clang/cFrontend_decl.mli +++ b/infer/src/clang/cFrontend_decl.mli @@ -10,10 +10,10 @@ (** Translate declarations **) module type CFrontend_decl = sig - val function_decl : Sil.tenv -> Cfg.cfg -> Cg.t -> Clang_ast_t.decl -> + val function_decl : Tenv.t -> Cfg.cfg -> Cg.t -> Clang_ast_t.decl -> CModule_type.block_data option -> unit - val translate_one_declaration : Sil.tenv -> Cg.t -> Cfg.cfg -> + val translate_one_declaration : Tenv.t -> Cg.t -> Cfg.cfg -> Clang_ast_t.decl -> Clang_ast_t.decl -> unit end diff --git a/infer/src/clang/cFrontend_errors.mli b/infer/src/clang/cFrontend_errors.mli index 622036bea..17714a2e6 100644 --- a/infer/src/clang/cFrontend_errors.mli +++ b/infer/src/clang/cFrontend_errors.mli @@ -14,5 +14,5 @@ val run_frontend_checkers_on_stmt : CTrans_utils.trans_state -> Clang_ast_t.stmt -> unit (* Run frontend checkers on a declaration *) -val run_frontend_checkers_on_decl : Sil.tenv -> Cg.t -> Cfg.cfg -> Clang_ast_t.decl -> unit +val run_frontend_checkers_on_decl : Tenv.t -> Cg.t -> Cfg.cfg -> Clang_ast_t.decl -> unit diff --git a/infer/src/clang/cFrontend_utils.ml b/infer/src/clang/cFrontend_utils.ml index fade40fe3..12814e7d7 100644 --- a/infer/src/clang/cFrontend_utils.ml +++ b/infer/src/clang/cFrontend_utils.ml @@ -39,7 +39,7 @@ struct pp Format.std_formatter fmt let print_tenv tenv = - Sil.tenv_iter (fun typname struct_t -> + Tenv.iter (fun typname struct_t -> match typname with | Typename.TN_csu (Csu.Class _, _) | Typename.TN_csu (Csu.Protocol, _) -> print_endline ( @@ -55,7 +55,7 @@ struct ) tenv let print_tenv_struct_unions tenv = - Sil.tenv_iter (fun typname struct_t -> + Tenv.iter (fun typname struct_t -> match typname with | Typename.TN_csu (Csu.Struct, _) | Typename.TN_csu (Csu.Union, _) -> print_endline ( @@ -98,7 +98,7 @@ end module Ast_utils = struct - type type_ptr_to_sil_type = Sil.tenv -> Clang_ast_t.type_ptr -> Sil.typ + type type_ptr_to_sil_type = Tenv.t -> Clang_ast_t.type_ptr -> Sil.typ let string_of_decl decl = let name = Clang_ast_proj.get_decl_kind_string decl in @@ -472,8 +472,8 @@ struct let sort_fields_tenv tenv = let sort_fields_struct typname st = let st' = { st with Sil.instance_fields = (sort_fields st.Sil.instance_fields) } in - Sil.tenv_add tenv typname st' in - Sil.tenv_iter sort_fields_struct tenv + Tenv.add tenv typname st' in + Tenv.iter sort_fields_struct tenv let rec collect_list_tuples l (a, a1, b, c, d) = match l with diff --git a/infer/src/clang/cFrontend_utils.mli b/infer/src/clang/cFrontend_utils.mli index 82457f5e6..7f3e44b00 100644 --- a/infer/src/clang/cFrontend_utils.mli +++ b/infer/src/clang/cFrontend_utils.mli @@ -21,9 +21,9 @@ sig val print_failure_info : string -> unit - val print_tenv : Sil.tenv -> unit + val print_tenv : Tenv.t -> unit - val print_tenv_struct_unions : Sil.tenv -> unit + val print_tenv_struct_unions : Tenv.t -> unit val print_procedures : Cfg.cfg -> unit @@ -115,12 +115,12 @@ sig val make_qual_name_decl : string list -> string -> Clang_ast_t.named_decl_info - type type_ptr_to_sil_type = Sil.tenv -> Clang_ast_t.type_ptr -> Sil.typ + type type_ptr_to_sil_type = Tenv.t -> Clang_ast_t.type_ptr -> Sil.typ - val add_type_from_decl_ref : type_ptr_to_sil_type -> Sil.tenv -> Clang_ast_t.decl_ref option -> + val add_type_from_decl_ref : type_ptr_to_sil_type -> Tenv.t -> Clang_ast_t.decl_ref option -> bool -> unit - val add_type_from_decl_ref_list : type_ptr_to_sil_type -> Sil.tenv -> Clang_ast_t.decl_ref list -> + val add_type_from_decl_ref_list : type_ptr_to_sil_type -> Tenv.t -> Clang_ast_t.decl_ref list -> unit end @@ -146,7 +146,7 @@ sig val sort_fields : (Ident.fieldname * Sil.typ * Sil.item_annotation) list -> (Ident.fieldname * Sil.typ * Sil.item_annotation) list - val sort_fields_tenv : Sil.tenv -> unit + val sort_fields_tenv : Tenv.t -> unit val collect_list_tuples : ('a list * 'b list * 'c list * 'd list * 'e list) list -> 'a list * 'b list * 'c list * 'd list * 'e list -> 'a list * 'b list * 'c list * 'd list * 'e list diff --git a/infer/src/clang/cMethod_trans.ml b/infer/src/clang/cMethod_trans.ml index 96abfe4c3..60c799c46 100644 --- a/infer/src/clang/cMethod_trans.ml +++ b/infer/src/clang/cMethod_trans.ml @@ -227,7 +227,7 @@ let get_superclass_curr_class_objc context = let retrive_super cname super_opt = let iname = Typename.TN_csu (Csu.Class Csu.Objc, Mangled.from_string cname) in Printing.log_out "Checking for superclass = '%s'\n\n%!" (Typename.to_string iname); - match Sil.tenv_lookup (CContext.get_tenv context) iname with + match Tenv.lookup (CContext.get_tenv context) iname with | Some { Sil.superclasses = super_name :: _ } -> Typename.name super_name | _ -> diff --git a/infer/src/clang/cMethod_trans.mli b/infer/src/clang/cMethod_trans.mli index e500ea137..cce66e997 100644 --- a/infer/src/clang/cMethod_trans.mli +++ b/infer/src/clang/cMethod_trans.mli @@ -22,7 +22,7 @@ type method_call_type = val should_add_return_param : Sil.typ -> is_objc_method:bool -> bool -val create_local_procdesc : Cfg.cfg -> Sil.tenv -> CMethod_signature.method_signature -> +val create_local_procdesc : Cfg.cfg -> Tenv.t -> CMethod_signature.method_signature -> Clang_ast_t.stmt list -> (Sil.pvar * Sil.typ) list -> bool -> bool val create_external_procdesc : Cfg.cfg -> Procname.t -> bool -> (Sil.typ * Sil.typ list) option -> unit @@ -33,20 +33,20 @@ val get_objc_method_data : Clang_ast_t.obj_c_message_expr_info -> val get_class_name_method_call_from_receiver_kind : CContext.t -> Clang_ast_t.obj_c_message_expr_info -> (Sil.exp * Sil.typ) list -> string -val get_class_name_method_call_from_clang : Sil.tenv -> Clang_ast_t.obj_c_message_expr_info -> +val get_class_name_method_call_from_clang : Tenv.t -> Clang_ast_t.obj_c_message_expr_info -> string option -val method_signature_of_decl : Sil.tenv -> Clang_ast_t.decl -> CModule_type.block_data option -> +val method_signature_of_decl : Tenv.t -> Clang_ast_t.decl -> CModule_type.block_data option -> CMethod_signature.method_signature * Clang_ast_t.stmt option * CModule_type.instr_type list -val method_signature_of_pointer : Sil.tenv -> Clang_ast_t.pointer -> +val method_signature_of_pointer : Tenv.t -> Clang_ast_t.pointer -> CMethod_signature.method_signature option -val get_method_name_from_clang : Sil.tenv -> CMethod_signature.method_signature option -> +val get_method_name_from_clang : Tenv.t -> CMethod_signature.method_signature option -> CMethod_signature.method_signature option val create_procdesc_with_pointer : CContext.t -> Clang_ast_t.pointer -> string option -> string -> Clang_ast_t.type_ptr -> Procname.t -val get_method_for_frontend_checks : Cfg.cfg -> Cg.t -> Sil.tenv -> string -> +val get_method_for_frontend_checks : Cfg.cfg -> Cg.t -> Tenv.t -> string -> Clang_ast_t.decl_info -> Cfg.Procdesc.t diff --git a/infer/src/clang/cModule_type.ml b/infer/src/clang/cModule_type.ml index 02b5c214d..6f08402ef 100644 --- a/infer/src/clang/cModule_type.ml +++ b/infer/src/clang/cModule_type.ml @@ -21,9 +21,9 @@ sig end module type CFrontend = sig - val function_decl : Sil.tenv -> Cfg.cfg -> Cg.t -> Clang_ast_t.decl -> + val function_decl : Tenv.t -> Cfg.cfg -> Cg.t -> Clang_ast_t.decl -> block_data option -> unit - val translate_one_declaration : Sil.tenv -> Cg.t -> Cfg.cfg -> + val translate_one_declaration : Tenv.t -> Cg.t -> Cfg.cfg -> Clang_ast_t.decl -> Clang_ast_t.decl -> unit end diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index c5f085faf..7f395c840 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -133,7 +133,7 @@ struct } in let block_type = Sil.Tstruct block_struct_typ in let block_name = Typename.TN_csu (Csu.Class Csu.Objc, mblock) in - Sil.tenv_add tenv block_name block_struct_typ; + Tenv.add tenv block_name block_struct_typ; let trans_res = CTrans_utils.alloc_trans trans_state loc (Ast_expressions.dummy_stmt_info ()) block_type true in let id_block = match trans_res.exps with | [(Sil.Var id, _)] -> id diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml index a2bdf9d4a..e13700b7b 100644 --- a/infer/src/clang/cTrans_utils.ml +++ b/infer/src/clang/cTrans_utils.ml @@ -658,7 +658,7 @@ let var_or_zero_in_init_list tenv e typ ~return_zero:return_zero = let open General_utils in match typ with | Sil.Tvar tn -> - (match Sil.tenv_lookup tenv tn with + (match Tenv.lookup tenv tn with | Some struct_typ -> var_or_zero_in_init_list' e (Sil.Tstruct struct_typ) tns | _ -> [[(e, typ)]] (*This case is an error, shouldn't happen.*)) | Sil.Tstruct { Sil.instance_fields } as type_struct -> diff --git a/infer/src/clang/cTrans_utils.mli b/infer/src/clang/cTrans_utils.mli index 6abd406a3..974da2aca 100644 --- a/infer/src/clang/cTrans_utils.mli +++ b/infer/src/clang/cTrans_utils.mli @@ -214,11 +214,12 @@ sig val is_var_self : Sil.pvar -> bool -> bool end -val is_logical_negation_of_int : Sil.tenv -> Clang_ast_t.expr_info -> Clang_ast_t.unary_operator_info -> bool +val is_logical_negation_of_int : + Tenv.t -> Clang_ast_t.expr_info -> Clang_ast_t.unary_operator_info -> bool val is_dispatch_function : Clang_ast_t.stmt list -> int option val is_block_enumerate_function : Clang_ast_t.obj_c_message_expr_info -> bool -val var_or_zero_in_init_list : Sil.tenv -> Sil.exp -> Sil.typ -> return_zero:bool -> +val var_or_zero_in_init_list : Tenv.t -> Sil.exp -> Sil.typ -> return_zero:bool -> (Sil.exp * Sil.typ) list diff --git a/infer/src/clang/cType_to_sil_type.mli b/infer/src/clang/cType_to_sil_type.mli index a2fa161ce..f80a38475 100644 --- a/infer/src/clang/cType_to_sil_type.mli +++ b/infer/src/clang/cType_to_sil_type.mli @@ -13,5 +13,5 @@ val get_builtin_objc_type : [< `ObjCClass | `ObjCId ] -> Sil.typ val sil_type_of_builtin_type_kind : Clang_ast_t.builtin_type_kind -> Sil.typ -val type_ptr_to_sil_type : (Sil.tenv -> Clang_ast_t.decl -> Sil.typ) -> - Sil.tenv -> Clang_ast_t.type_ptr -> Sil.typ +val type_ptr_to_sil_type : (Tenv.t -> Clang_ast_t.decl -> Sil.typ) -> + Tenv.t -> Clang_ast_t.type_ptr -> Sil.typ diff --git a/infer/src/clang/cTypes.ml b/infer/src/clang/cTypes.ml index 855764c1c..b4919d40b 100644 --- a/infer/src/clang/cTypes.ml +++ b/infer/src/clang/cTypes.ml @@ -85,7 +85,7 @@ let is_reference_type tp = let rec expand_structured_type tenv typ = match typ with | Sil.Tvar tn -> - (match Sil.tenv_lookup tenv tn with + (match Tenv.lookup tenv tn with | Some ts -> let t = Sil.Tstruct ts in Printing.log_out " Type expanded with type '%s' found in tenv@." (Sil.typ_to_string t); diff --git a/infer/src/clang/cTypes.mli b/infer/src/clang/cTypes.mli index 6b54f9c5b..2c7405c52 100644 --- a/infer/src/clang/cTypes.mli +++ b/infer/src/clang/cTypes.mli @@ -31,6 +31,6 @@ val is_block_type : Clang_ast_t.type_ptr -> bool val is_reference_type : Clang_ast_t.type_ptr -> bool -val expand_structured_type : Sil.tenv -> Sil.typ -> Sil.typ +val expand_structured_type : Tenv.t -> Sil.typ -> Sil.typ val get_name_from_type_pointer : string -> string * string diff --git a/infer/src/clang/cTypes_decl.ml b/infer/src/clang/cTypes_decl.ml index fb76fb246..f52d9b34e 100644 --- a/infer/src/clang/cTypes_decl.ml +++ b/infer/src/clang/cTypes_decl.ml @@ -25,7 +25,7 @@ let add_predefined_objc_types tenv = def_methods = []; struct_annotations = []; } in - Sil.tenv_add tenv class_typename objc_class_type_info; + Tenv.add tenv class_typename objc_class_type_info; let id_typename = CType_to_sil_type.get_builtin_objc_typename `ObjCId in let objc_object_type_info = { @@ -37,7 +37,7 @@ let add_predefined_objc_types tenv = def_methods = []; struct_annotations = []; } in - Sil.tenv_add tenv id_typename objc_object_type_info + Tenv.add tenv id_typename objc_object_type_info (* Whenever new type are added manually to the translation in ast_expressions, *) (* they should be added here too!! *) @@ -142,7 +142,7 @@ let add_struct_to_tenv tenv typ = | _ -> assert false in let mangled = CTypes.get_name_from_struct typ in let typename = Typename.TN_csu(csu, mangled) in - Sil.tenv_add tenv typename struct_typ + Tenv.add tenv typename struct_typ let rec get_struct_fields tenv decl = let open Clang_ast_t in @@ -200,7 +200,7 @@ and get_struct_cpp_class_declaration_type tenv decl = add_struct_to_tenv tenv sil_type; sil_type ) else ( - match Sil.tenv_lookup tenv sil_typename with + match Tenv.lookup tenv sil_typename with | Some struct_typ -> Sil.Tstruct struct_typ (* just reuse what is already in tenv *) | None -> (* This is first forward definition seen so far. Instead of adding *) diff --git a/infer/src/clang/cTypes_decl.mli b/infer/src/clang/cTypes_decl.mli index 2c25e9029..64f4c6b68 100644 --- a/infer/src/clang/cTypes_decl.mli +++ b/infer/src/clang/cTypes_decl.mli @@ -9,25 +9,25 @@ (** Processes types and record declarations by adding them to the tenv *) -val add_struct_to_tenv : Sil.tenv -> Sil.typ -> unit +val add_struct_to_tenv : Tenv.t -> Sil.typ -> unit val get_record_name : Clang_ast_t.decl -> string -val add_types_from_decl_to_tenv : Sil.tenv -> Clang_ast_t.decl -> Sil.typ +val add_types_from_decl_to_tenv : Tenv.t -> Clang_ast_t.decl -> Sil.typ (* Adds the predefined types objc_class which is a struct, *) (* and Class, which is a pointer to objc_class. *) -val add_predefined_types : Sil.tenv -> unit +val add_predefined_types : Tenv.t -> unit -val type_ptr_to_sil_type : Sil.tenv -> Clang_ast_t.type_ptr -> Sil.typ +val type_ptr_to_sil_type : Tenv.t -> Clang_ast_t.type_ptr -> Sil.typ -val class_from_pointer_type : Sil.tenv -> Clang_ast_t.type_ptr -> string +val class_from_pointer_type : Tenv.t -> Clang_ast_t.type_ptr -> string -val get_class_type_np : Sil.tenv -> Clang_ast_t.expr_info -> +val get_class_type_np : Tenv.t -> Clang_ast_t.expr_info -> Clang_ast_t.obj_c_message_expr_info -> Sil.typ -val get_type_curr_class_objc : Sil.tenv -> CContext.curr_class -> Sil.typ +val get_type_curr_class_objc : Tenv.t -> CContext.curr_class -> Sil.typ -val get_type_from_expr_info : Clang_ast_t.expr_info -> Sil.tenv -> Sil.typ +val get_type_from_expr_info : Clang_ast_t.expr_info -> Tenv.t -> Sil.typ -val objc_class_name_to_sil_type : Sil.tenv -> string -> Sil.typ +val objc_class_name_to_sil_type : Tenv.t -> string -> Sil.typ diff --git a/infer/src/clang/objcCategory_decl.ml b/infer/src/clang/objcCategory_decl.ml index 6ed59747e..38ccbca72 100644 --- a/infer/src/clang/objcCategory_decl.ml +++ b/infer/src/clang/objcCategory_decl.ml @@ -75,7 +75,7 @@ let process_category type_ptr_to_sil_type tenv curr_class decl_info decl_list = let class_tn_name = Typename.TN_csu (Csu.Class Csu.Objc, mang_name) in let decl_key = `DeclPtr decl_info.Clang_ast_t.di_pointer in Ast_utils.update_sil_types_map decl_key (Sil.Tvar class_tn_name); - (match Sil.tenv_lookup tenv class_tn_name with + (match Tenv.lookup tenv class_tn_name with | Some ({ Sil.instance_fields; def_methods } as struct_typ) -> let new_fields = General_utils.append_no_duplicates_fields fields instance_fields in let new_methods = General_utils.append_no_duplicates_methods methods def_methods in @@ -89,7 +89,7 @@ let process_category type_ptr_to_sil_type tenv curr_class decl_info decl_list = def_methods = new_methods; } in Printing.log_out " Updating info for class '%s' in tenv\n" class_name; - Sil.tenv_add tenv class_tn_name class_type_info + Tenv.add tenv class_tn_name class_type_info | _ -> ()); Sil.Tvar class_tn_name diff --git a/infer/src/clang/objcCategory_decl.mli b/infer/src/clang/objcCategory_decl.mli index d0280e99d..fc72edb4a 100644 --- a/infer/src/clang/objcCategory_decl.mli +++ b/infer/src/clang/objcCategory_decl.mli @@ -12,9 +12,9 @@ open CFrontend_utils -val category_decl : Ast_utils.type_ptr_to_sil_type -> Sil.tenv -> Clang_ast_t.decl -> Sil.typ +val category_decl : Ast_utils.type_ptr_to_sil_type -> Tenv.t -> Clang_ast_t.decl -> Sil.typ -val category_impl_decl : Ast_utils.type_ptr_to_sil_type -> Sil.tenv -> Clang_ast_t.decl -> Sil.typ +val category_impl_decl : Ast_utils.type_ptr_to_sil_type -> Tenv.t -> Clang_ast_t.decl -> Sil.typ val noname_category : string -> string diff --git a/infer/src/clang/objcInterface_decl.ml b/infer/src/clang/objcInterface_decl.ml index bdf5c00b2..a77c620a4 100644 --- a/infer/src/clang/objcInterface_decl.ml +++ b/infer/src/clang/objcInterface_decl.ml @@ -21,7 +21,7 @@ module L = Logging let is_pointer_to_objc_class tenv typ = match typ with | Sil.Tptr (Sil.Tvar (Typename.TN_csu (Csu.Class Csu.Objc, cname)), _) -> - (match Sil.tenv_lookup tenv (Typename.TN_csu (Csu.Class Csu.Objc, cname)) with + (match Tenv.lookup tenv (Typename.TN_csu (Csu.Class Csu.Objc, cname)) with | Some struct_typ when Sil.is_objc_class (Sil.Tstruct struct_typ) -> true | _ -> false) | Sil.Tptr (typ, _) when Sil.is_objc_class typ -> true @@ -112,7 +112,7 @@ let add_class_to_tenv type_ptr_to_sil_type tenv curr_class decl_info class_name Printing.log_out "type: '%s'\n" (Sil.typ_to_string ft)) fields_sc; (*In case we found categories, or partial definition of this class earlier and they are already in the tenv *) let fields, (superclasses : Typename.t list), methods = - match Sil.tenv_lookup tenv interface_name with + match Tenv.lookup tenv interface_name with | Some ({ Sil.instance_fields; superclasses; def_methods }) -> General_utils.append_no_duplicates_fields fields instance_fields, General_utils.append_no_duplicates_csu superclasses superclasses, @@ -134,10 +134,10 @@ let add_class_to_tenv type_ptr_to_sil_type tenv curr_class decl_info class_name def_methods = methods; struct_annotations = Sil.objc_class_annotation; } in - Sil.tenv_add tenv interface_name interface_type_info; + Tenv.add tenv interface_name interface_type_info; Printing.log_out " >>>Verifying that Typename '%s' is in tenv\n" (Typename.to_string interface_name); - (match Sil.tenv_lookup tenv interface_name with + (match Tenv.lookup tenv interface_name with | Some st -> Printing.log_out " >>>OK. Found typ='%s'\n" (Sil.typ_to_string (Sil.Tstruct st)) | None -> Printing.log_out " >>>NOT Found!!\n"); Sil.Tvar interface_name @@ -148,7 +148,7 @@ let add_missing_methods tenv class_name ck decl_info decl_list curr_class = let decl_key = `DeclPtr decl_info.Clang_ast_t.di_pointer in Ast_utils.update_sil_types_map decl_key (Sil.Tvar class_tn_name); begin - match Sil.tenv_lookup tenv class_tn_name with + match Tenv.lookup tenv class_tn_name with | Some ({ Sil.static_fields = []; csu = Csu.Class _; struct_name = Some _; @@ -156,7 +156,7 @@ let add_missing_methods tenv class_name ck decl_info decl_list curr_class = } as struct_typ) -> let methods = General_utils.append_no_duplicates_methods def_methods methods in let struct_typ' = { struct_typ with Sil.def_methods = methods; } in - Sil.tenv_add tenv class_tn_name struct_typ' + Tenv.add tenv class_tn_name struct_typ' | _ -> () end; Sil.Tvar class_tn_name diff --git a/infer/src/clang/objcInterface_decl.mli b/infer/src/clang/objcInterface_decl.mli index 0da3d1b84..54481a5b7 100644 --- a/infer/src/clang/objcInterface_decl.mli +++ b/infer/src/clang/objcInterface_decl.mli @@ -12,13 +12,13 @@ (** list of defined methods *) open CFrontend_utils -val interface_declaration : Ast_utils.type_ptr_to_sil_type -> Sil.tenv -> Clang_ast_t.decl -> +val interface_declaration : Ast_utils.type_ptr_to_sil_type -> Tenv.t -> Clang_ast_t.decl -> Sil.typ -val interface_impl_declaration : Ast_utils.type_ptr_to_sil_type -> Sil.tenv -> Clang_ast_t.decl -> +val interface_impl_declaration : Ast_utils.type_ptr_to_sil_type -> Tenv.t -> Clang_ast_t.decl -> Sil.typ -val is_pointer_to_objc_class : Sil.tenv -> Sil.typ -> bool +val is_pointer_to_objc_class : Tenv.t -> Sil.typ -> bool val get_curr_class : string -> Clang_ast_t.obj_c_interface_decl_info -> CContext.curr_class diff --git a/infer/src/clang/objcProtocol_decl.ml b/infer/src/clang/objcProtocol_decl.ml index da3aa2f97..495162514 100644 --- a/infer/src/clang/objcProtocol_decl.ml +++ b/infer/src/clang/objcProtocol_decl.ml @@ -41,7 +41,7 @@ let protocol_decl type_ptr_to_sil_type tenv decl = def_methods; struct_annotations = []; } in - Sil.tenv_add tenv protocol_name protocol_type_info; + Tenv.add tenv protocol_name protocol_type_info; add_protocol_super type_ptr_to_sil_type tenv obj_c_protocol_decl_info; Sil.Tvar protocol_name | _ -> assert false diff --git a/infer/src/clang/objcProtocol_decl.mli b/infer/src/clang/objcProtocol_decl.mli index 06c6725bc..ded0b9b22 100644 --- a/infer/src/clang/objcProtocol_decl.mli +++ b/infer/src/clang/objcProtocol_decl.mli @@ -12,6 +12,6 @@ open CFrontend_utils -val protocol_decl : Ast_utils.type_ptr_to_sil_type -> Sil.tenv -> Clang_ast_t.decl -> Sil.typ +val protocol_decl : Ast_utils.type_ptr_to_sil_type -> Tenv.t -> Clang_ast_t.decl -> Sil.typ val is_protocol : Clang_ast_t.decl -> bool diff --git a/infer/src/eradicate/README.md b/infer/src/eradicate/README.md new file mode 100644 index 000000000..973467eb5 --- /dev/null +++ b/infer/src/eradicate/README.md @@ -0,0 +1,5 @@ +# Eradicate @Nullable Checker + +Eradicate is a type checker for `@Nullable` annotations for Java. The goal is to eradicate null pointer exceptions. See [Eradicate](http://fbinfer.com/docs/eradicate.html). + +The main entry point is module [Eradicate](eradicate.mli). \ No newline at end of file diff --git a/infer/src/eradicate/eradicate.ml b/infer/src/eradicate/eradicate.ml index 650ff5093..6be1cc7b0 100644 --- a/infer/src/eradicate/eradicate.ml +++ b/infer/src/eradicate/eradicate.ml @@ -22,7 +22,8 @@ let verbose = Config.from_env_variable "ERADICATE_TYPINGS" (* print step-by-step tracing information *) let trace = Config.from_env_variable "ERADICATE_TRACE" -let check_field_initialization = true (* check that nonnullable fields are initialized in constructors *) +(* check that nonnullable fields are initialized in constructors *) +let check_field_initialization = true type parameters = TypeState.parameters diff --git a/infer/src/eradicate/typeCheck.mli b/infer/src/eradicate/typeCheck.mli index d27cea4b4..6362b83f3 100644 --- a/infer/src/eradicate/typeCheck.mli +++ b/infer/src/eradicate/typeCheck.mli @@ -25,7 +25,7 @@ type checks = } val typecheck_node : - Sil.tenv -> 'a TypeState.ext -> + Tenv.t -> 'a TypeState.ext -> bool ref -> checks -> Idenv.t -> get_proc_desc -> Procname.t -> Cfg.Procdesc.t -> find_canonical_duplicate -> Annotations.annotated_signature -> 'a TypeState.t -> diff --git a/infer/src/eradicate/typeState.ml b/infer/src/eradicate/typeState.ml index 440645e33..fda950992 100644 --- a/infer/src/eradicate/typeState.ml +++ b/infer/src/eradicate/typeState.ml @@ -23,7 +23,7 @@ type 'a ext = { empty : 'a; (** empty extension *) check_instr : (** check the extension for an instruction *) - Sil.tenv -> get_proc_desc -> Procname.t -> + Tenv.t -> get_proc_desc -> Procname.t -> Cfg.Procdesc.t -> 'a -> Sil.instr -> parameters -> 'a; join : 'a -> 'a -> 'a; (** join two extensions *) pp : Format.formatter -> 'a -> unit (** pretty print an extension *) diff --git a/infer/src/eradicate/typeState.mli b/infer/src/eradicate/typeState.mli index 0eb1141d1..3265d03f2 100644 --- a/infer/src/eradicate/typeState.mli +++ b/infer/src/eradicate/typeState.mli @@ -19,7 +19,7 @@ type 'a ext = { empty : 'a; (** empty extension *) check_instr : (** check the extension for an instruction *) - Sil.tenv -> get_proc_desc -> Procname.t -> + Tenv.t -> get_proc_desc -> Procname.t -> Cfg.Procdesc.t ->'a -> Sil.instr -> parameters -> 'a; join : 'a -> 'a -> 'a; (** join two extensions *) pp : Format.formatter -> 'a -> unit (** pretty print an extension *) diff --git a/infer/src/harness/androidFramework.ml b/infer/src/harness/androidFramework.ml index 6a62d269c..3350f1919 100644 --- a/infer/src/harness/androidFramework.ml +++ b/infer/src/harness/androidFramework.ml @@ -257,7 +257,7 @@ let get_all_supertypes typ tenv = superclasses | _ -> [] in let rec add_typ class_name typs = - match Sil.tenv_lookup tenv class_name with + match Tenv.lookup tenv class_name with | Some struct_typ -> let typ' = Sil.Tstruct struct_typ in get_supers_rec typ' (TypSet.add typ' typs) @@ -275,7 +275,7 @@ let is_subtype (typ0 : Sil.typ) (typ1 : Sil.typ) tenv = let is_subtype_package_class typ package classname tenv = let classname = Mangled.from_package_class package classname in - match Sil.tenv_lookup tenv (Typename.TN_csu (Csu.Class Csu.Java, classname)) with + match Tenv.lookup tenv (Typename.TN_csu (Csu.Class Csu.Java, classname)) with | Some found_struct_typ -> is_subtype typ (Sil.Tstruct found_struct_typ) tenv | _ -> false @@ -363,7 +363,7 @@ let get_callbacks_registered_by_proc procdesc tenv = (** given an Android framework type mangled string [lifecycle_typ] (e.g., android.app.Activity) and a list of method names [lifecycle_procs_strs], get the appropriate typ and procnames *) let get_lifecycle_for_framework_typ_opt lifecycle_typ lifecycle_proc_strs tenv = - match Sil.tenv_lookup tenv (Typename.TN_csu (Csu.Class Csu.Java, lifecycle_typ)) with + match Tenv.lookup tenv (Typename.TN_csu (Csu.Class Csu.Java, lifecycle_typ)) with | Some ({ Sil.csu = Csu.Class _; struct_name = Some _; def_methods } as lifecycle_typ) -> (* TODO (t4645631): collect the procedures for which is_java is returning false *) let lookup_proc lifecycle_proc = @@ -390,7 +390,7 @@ let get_lifecycles = android_lifecycles let is_subclass tenv cn1 classname_str = let typename = Typename.Java.from_string classname_str in - let lookup = Sil.tenv_lookup tenv in + let lookup = Tenv.lookup tenv in match lookup cn1, lookup typename with | Some typ1, Some typ2 -> is_subtype (Sil.Tstruct typ1) (Sil.Tstruct typ2) tenv diff --git a/infer/src/harness/androidFramework.mli b/infer/src/harness/androidFramework.mli index 6f7e5e309..a8a1a7389 100644 --- a/infer/src/harness/androidFramework.mli +++ b/infer/src/harness/androidFramework.mli @@ -13,24 +13,24 @@ val get_lifecycles : (string * string * string list) list (** return true if [typ] is a subclass of [lifecycle_typ] *) -val typ_is_lifecycle_typ : Sil.typ -> Sil.typ -> Sil.tenv -> bool +val typ_is_lifecycle_typ : Sil.typ -> Sil.typ -> Tenv.t -> bool (** return true if [typ] is a known callback class, false otherwise *) -val is_callback_class : Sil.typ -> Sil.tenv -> bool +val is_callback_class : Sil.typ -> Tenv.t -> bool (** return true if [typ] <: android.content.Context *) -val is_context : Sil.typ -> Sil.tenv -> bool +val is_context : Sil.typ -> Tenv.t -> bool (** return true if [typ] <: android.app.Application *) -val is_application : Sil.typ -> Sil.tenv -> bool +val is_application : Sil.typ -> Tenv.t -> bool (** return true if [typ] <: android.app.Activity *) -val is_activity : Sil.typ -> Sil.tenv -> bool +val is_activity : Sil.typ -> Tenv.t -> bool (** return true if [typ] <: android.view.View *) -val is_view : Sil.typ -> Sil.tenv -> bool +val is_view : Sil.typ -> Tenv.t -> bool -val is_fragment : Sil.typ -> Sil.tenv -> bool +val is_fragment : Sil.typ -> Tenv.t -> bool (** return true if [procname] is a special lifecycle cleanup method *) val is_destroy_method : Procname.t -> bool @@ -38,14 +38,15 @@ val is_destroy_method : Procname.t -> bool (** returns an option containing the var name and type of a callback registered by [procname], None if no callback is registered *) val get_callback_registered_by : - Procname.java -> (Sil.exp * Sil.typ) list -> Sil.tenv -> (Sil.exp * Sil.typ) option + Procname.java -> (Sil.exp * Sil.typ) list -> Tenv.t -> (Sil.exp * Sil.typ) option (** return a list of typ's corresponding to callback classes registered by [procdesc] *) -val get_callbacks_registered_by_proc : Cfg.Procdesc.t -> Sil.tenv -> Sil.typ list +val get_callbacks_registered_by_proc : Cfg.Procdesc.t -> Tenv.t -> Sil.typ list -(** given an Android framework type mangled string [lifecycle_typ] (e.g., android.app.Activity) and - a list of method names [lifecycle_procs_strs], get the appropriate typ and procnames *) -val get_lifecycle_for_framework_typ_opt : Mangled.t -> string list -> Sil.tenv -> (Sil.typ * Procname.t list) option +(** given an Android framework type mangled string [lifecycle_typ] (e.g., android.app.Activity) + and a list of method names [lifecycle_procs_strs], get the appropriate typ and procnames *) +val get_lifecycle_for_framework_typ_opt : + Mangled.t -> string list -> Tenv.t -> (Sil.typ * Procname.t list) option (** return true if [class_name] is the name of a class that belong to the Android framework *) val is_android_lib_class : Typename.t -> bool @@ -53,14 +54,14 @@ val is_android_lib_class : Typename.t -> bool (** Path to the android.jar file containing real code, not just the method stubs as in the SDK *) val non_stub_android_jar : unit -> string -val is_subclass : Sil.tenv -> Typename.t -> string -> bool +val is_subclass : Tenv.t -> Typename.t -> string -> bool (** [is_exception tenv class_name] checks if class_name is of type java.lang.Exception *) -val is_exception : Sil.tenv -> Typename.t -> bool +val is_exception : Tenv.t -> Typename.t -> bool (** [is_throwable tenv class_name] checks if class_name is of type java.lang.Throwable *) -val is_throwable : Sil.tenv -> Typename.t -> bool +val is_throwable : Tenv.t -> Typename.t -> bool (** [is_runtime_exception tenv class_name] checks if classname is of type java.lang.RuntimeException *) -val is_runtime_exception : Sil.tenv -> Typename.t -> bool +val is_runtime_exception : Tenv.t -> Typename.t -> bool diff --git a/infer/src/harness/harness.ml b/infer/src/harness/harness.ml index 560889e99..a5d13a8be 100644 --- a/infer/src/harness/harness.ml +++ b/infer/src/harness/harness.ml @@ -40,7 +40,7 @@ let create_harness cfg cg tenv = subclass of [lifecycle_typ] *) (* TODO: instead of iterating through the type environment, interate through the types declared in [cfg] *) - Sil.tenv_iter (fun _ struct_typ -> + Tenv.iter (fun _ struct_typ -> let typ = Sil.Tstruct struct_typ in match try_create_lifecycle_trace typ framework_typ framework_procs tenv with | [] -> () diff --git a/infer/src/harness/harness.mli b/infer/src/harness/harness.mli index b67d175cd..7994698b0 100644 --- a/infer/src/harness/harness.mli +++ b/infer/src/harness/harness.mli @@ -10,4 +10,4 @@ (** Automatically create a harness method to exercise code under test *) (** Generate a harness method for exe_env and add it to the execution environment *) -val create_harness : Cfg.cfg -> Cg.t -> Sil.tenv -> unit +val create_harness : Cfg.cfg -> Cg.t -> Tenv.t -> unit diff --git a/infer/src/harness/stacktrace.ml b/infer/src/harness/stacktrace.ml index 30b638be5..0dbd61bd4 100644 --- a/infer/src/harness/stacktrace.ml +++ b/infer/src/harness/stacktrace.ml @@ -41,7 +41,7 @@ let try_resolve_frame (str_frame : str_frame) exe_env tenv = (* find the class name in the tenv and get the procedure(s) whose names match the procedure name * in the stack trace. Note that the stack trace does not have any type or argument information; * the name is all that we have to go on *) - match Sil.tenv_lookup tenv (Typename.TN_csu (Csu.Class Csu.Java, class_name)) with + match Tenv.lookup tenv (Typename.TN_csu (Csu.Class Csu.Java, class_name)) with | Some Sil.Tstruct { Sil.csu = Csu.Class _; def_methods } -> let possible_calls = IList.filter diff --git a/infer/src/java/README.md b/infer/src/java/README.md new file mode 100644 index 000000000..e18b78766 --- /dev/null +++ b/infer/src/java/README.md @@ -0,0 +1,5 @@ +# Java Front-End + +This is the front-end for java compilers. + +The main entry point is [JMain](jmain.ml). \ No newline at end of file diff --git a/infer/src/java/jClasspath.ml b/infer/src/java/jClasspath.ml index ce606f10b..85ed9f830 100644 --- a/infer/src/java/jClasspath.ml +++ b/infer/src/java/jClasspath.ml @@ -22,7 +22,7 @@ let set_verbose_out path = let models_jar = ref "" -let models_tenv = ref (Sil.create_tenv ()) +let models_tenv = ref (Tenv.create ()) let load_models_tenv zip_channel = @@ -36,7 +36,7 @@ let load_models_tenv zip_channel = let models_tenv = try Zip.copy_entry_to_file zip_channel entry temp_tenv_file; - match Sil.load_tenv_from_file temp_tenv_filename with + match Tenv.load_from_file temp_tenv_filename with | None -> failwith "Models tenv file could not be loaded" | Some tenv -> tenv with diff --git a/infer/src/java/jClasspath.mli b/infer/src/java/jClasspath.mli index e5190aff9..dbee611bd 100644 --- a/infer/src/java/jClasspath.mli +++ b/infer/src/java/jClasspath.mli @@ -14,7 +14,7 @@ open Javalib_pack val models_jar : string ref (** Type environment of the models *) -val models_tenv : Sil.tenv ref +val models_tenv : Tenv.t ref (** Adds the set of procnames for the models of Java libraries so that methods with similar names are skipped during the capture *) diff --git a/infer/src/java/jContext.ml b/infer/src/java/jContext.ml index 09084ddfd..cfca379c6 100644 --- a/infer/src/java/jContext.ml +++ b/infer/src/java/jContext.ml @@ -24,7 +24,7 @@ type meth_kind = (** data *) type icfg = { - tenv : Sil.tenv; + tenv : Tenv.t; cg : Cg.t; cfg : Cfg.cfg; } diff --git a/infer/src/java/jContext.mli b/infer/src/java/jContext.mli index f1178fa12..f0692be2f 100644 --- a/infer/src/java/jContext.mli +++ b/infer/src/java/jContext.mli @@ -32,7 +32,7 @@ module NodeTbl : Hashtbl.S with type key = Cfg.Node.t representation of a file: the type environment, the control graph and the control flow graph *) type icfg = { - tenv : Sil.tenv; + tenv : Tenv.t; cg : Cg.t; cfg : Cfg.cfg; } @@ -63,7 +63,7 @@ val get_impl : t -> JBir.t val get_cn : t -> JBasics.class_name (** returns the type environment that corresponds to the current file. *) -val get_tenv : t -> Sil.tenv +val get_tenv : t -> Tenv.t (** returns the control graph that corresponds to the current file. *) val get_cg : t -> Cg.t diff --git a/infer/src/java/jFrontend.mli b/infer/src/java/jFrontend.mli index 853d66540..b3b797bef 100644 --- a/infer/src/java/jFrontend.mli +++ b/infer/src/java/jFrontend.mli @@ -25,7 +25,7 @@ val compute_source_icfg : Printer.LineReader.t -> JBasics.ClassSet.t -> JClasspath.program -> - Sil.tenv -> + Tenv.t -> string -> string option -> Cg.t * Cfg.cfg @@ -35,6 +35,6 @@ val compute_class_icfg : Inferconfig.NeverReturnNull.matcher -> Printer.LineReader.t -> JClasspath.program -> - Sil.tenv -> + Tenv.t -> JCode.jcode Javalib.interface_or_class -> Cg.t * Cfg.cfg diff --git a/infer/src/java/jMain.ml b/infer/src/java/jMain.ml index 01ea3b5e3..d94aee972 100644 --- a/infer/src/java/jMain.ml +++ b/infer/src/java/jMain.ml @@ -138,7 +138,8 @@ let capture_libs never_null_matcher linereader program tenv = | Javalib.JClass _ when JFrontend.is_classname_cached cn -> () | Javalib.JClass _ -> begin - let fake_source_file = JClasspath.java_source_file_from_path (JFrontend.path_of_cached_classname cn) in + let fake_source_file = + JClasspath.java_source_file_from_path (JFrontend.path_of_cached_classname cn) in init_global_state fake_source_file; let call_graph, cfg = JFrontend.compute_class_icfg never_null_matcher linereader program tenv node in @@ -154,18 +155,20 @@ let load_tenv () = let tenv = if DB.file_exists tenv_filename then begin - match Sil.load_tenv_from_file tenv_filename with - | None -> Sil.create_tenv () + match Tenv.load_from_file tenv_filename with + | None -> + Tenv.create () | Some _ when Config.analyze_models -> let error_msg = "Unexpected tenv file " ^ (DB.filename_to_string tenv_filename) ^ " found while generating the models" in failwith error_msg - | Some tenv -> tenv + | Some tenv -> + tenv end else - Sil.create_tenv () in + Tenv.create () in tenv @@ -176,7 +179,7 @@ let save_tenv tenv = (* TODO: this prevents per compilation step incremental analysis at this stage *) if DB.file_exists tenv_filename then DB.file_remove tenv_filename; JUtils.log "writing new tenv %s@." (DB.filename_to_string tenv_filename); - Sil.store_tenv_to_file tenv_filename tenv + Tenv.store_to_file tenv_filename tenv (* The program is loaded and translated *) diff --git a/infer/src/java/jTrans.mli b/infer/src/java/jTrans.mli index 26d4d1f11..ff1574f3e 100644 --- a/infer/src/java/jTrans.mli +++ b/infer/src/java/jTrans.mli @@ -27,11 +27,13 @@ type defined_status = | Called of Cfg.Procdesc.t (** returns the procedure description of the given method and creates it if it hasn't been created before *) -val get_method_procdesc : JClasspath.program -> Cfg.cfg -> Sil.tenv -> JBasics.class_name -> +val get_method_procdesc : JClasspath.program -> Cfg.cfg -> Tenv.t -> JBasics.class_name -> JBasics.method_signature -> Procname.method_kind -> defined_status (** [create_local_procdesc linereader cfg tenv program m] creates a procedure description for the method m and adds it to cfg *) -val create_local_procdesc : JClasspath.program -> Printer.LineReader.t -> Cfg.cfg -> Sil.tenv -> JCode.jcode Javalib.interface_or_class -> JCode.jcode Javalib.jmethod -> unit +val create_local_procdesc : + JClasspath.program -> Printer.LineReader.t -> Cfg.cfg -> Tenv.t -> + JCode.jcode Javalib.interface_or_class -> JCode.jcode Javalib.jmethod -> unit (** returns the implementation of a given method *) val get_implementation : JCode.jcode Javalib.concrete_method -> JBir.t diff --git a/infer/src/java/jTransType.ml b/infer/src/java/jTransType.ml index 48433695e..ae63ad30a 100644 --- a/infer/src/java/jTransType.ml +++ b/infer/src/java/jTransType.ml @@ -352,11 +352,11 @@ and create_sil_type program tenv cn = and get_class_type_no_pointer program tenv cn = let named_type = typename_of_classname cn in - match Sil.tenv_lookup tenv named_type with + match Tenv.lookup tenv named_type with | None -> (match create_sil_type program tenv cn with | (Sil.Tstruct struct_typ) as typ-> - Sil.tenv_add tenv named_type struct_typ; + Tenv.add tenv named_type struct_typ; typ | _ -> assert false) | Some struct_typ -> Sil.Tstruct struct_typ @@ -467,9 +467,9 @@ let return_type program tenv ms meth_kind = let add_models_types tenv = let add_type t typename struct_typ = - if not (Sil.tenv_mem t typename) then - Sil.tenv_add tenv typename struct_typ in - Sil.tenv_iter (add_type tenv) !JClasspath.models_tenv + if not (Tenv.mem t typename) then + Tenv.add tenv typename struct_typ in + Tenv.iter (add_type tenv) !JClasspath.models_tenv (* TODO #6604630: remove *) diff --git a/infer/src/java/jTransType.mli b/infer/src/java/jTransType.mli index 0d9037266..0dc2c59b8 100644 --- a/infer/src/java/jTransType.mli +++ b/infer/src/java/jTransType.mli @@ -28,33 +28,35 @@ val get_method_procname : (** [get_class_type_no_pointer program tenv cn] returns the sil type representation of the class without the pointer part *) -val get_class_type_no_pointer: JClasspath.program -> Sil.tenv -> JBasics.class_name -> Sil.typ +val get_class_type_no_pointer: JClasspath.program -> Tenv.t -> JBasics.class_name -> Sil.typ (** [get_class_type program tenv cn] returns the sil type representation of the class *) -val get_class_type : JClasspath.program -> Sil.tenv -> JBasics.class_name -> Sil.typ +val get_class_type : JClasspath.program -> Tenv.t -> JBasics.class_name -> Sil.typ (** return true if [field_name] is the autogenerated C.$assertionsDisabled field for class C *) val is_autogenerated_assert_field : Ident.fieldname -> bool (** [is_closeable program tenv typ] check if typ is an implemtation of the Closeable interface *) -val is_closeable : JClasspath.program -> Sil.tenv -> Sil.typ -> bool +val is_closeable : JClasspath.program -> Tenv.t -> Sil.typ -> bool (** transforms a Java object type to a Sil type *) -val object_type : JClasspath.program -> Sil.tenv -> JBasics.object_type -> Sil.typ +val object_type : JClasspath.program -> Tenv.t -> JBasics.object_type -> Sil.typ (** create sizeof expressions from the object type and the list of subtypes *) -val sizeof_of_object_type : JClasspath.program -> Sil.tenv -> JBasics.object_type -> Sil.Subtype.t +val sizeof_of_object_type : JClasspath.program -> Tenv.t -> JBasics.object_type -> Sil.Subtype.t -> Sil.exp (** transforms a Java type to a Sil type. *) -val value_type : JClasspath.program -> Sil.tenv -> JBasics.value_type -> Sil.typ +val value_type : JClasspath.program -> Tenv.t -> JBasics.value_type -> Sil.typ (** return the type of a formal parameter, looking up the class name in case of "this" *) -val param_type : JClasspath.program -> Sil.tenv -> JBasics.class_name -> JBir.var -> JBasics.value_type -> Sil.typ +val param_type : + JClasspath.program -> Tenv.t -> JBasics.class_name -> JBir.var -> JBasics.value_type -> Sil.typ (** Returns the return type of the method based on the return type specified in ms. If the method is the initialiser, return the type Object instead. *) -val return_type : JClasspath.program -> Sil.tenv -> JBasics.method_signature -> JContext.meth_kind -> Sil.typ +val return_type : + JClasspath.program -> Tenv.t -> JBasics.method_signature -> JContext.meth_kind -> Sil.typ (** translates the type of an expression *) val expr_type : JContext.t -> JBir.expr -> Sil.typ @@ -87,7 +89,7 @@ val vt_to_java_type : JBasics.value_type -> Procname.java_type val cn_to_java_type : JBasics.class_name -> Procname.java_type (** Add the types of the models to the type environment passed as parameter *) -val add_models_types : Sil.tenv -> unit +val add_models_types : Tenv.t -> unit (** list of methods that are never returning null *) val never_returning_null : Procname.java list diff --git a/infer/src/llvm/lMain.ml b/infer/src/llvm/lMain.ml index 069b59f42..975de3bac 100644 --- a/infer/src/llvm/lMain.ml +++ b/infer/src/llvm/lMain.ml @@ -62,7 +62,7 @@ let store_icfg tenv cg cfg = let store_tenv tenv = let tenv_filename = DB.global_tenv_fname () in if DB.file_exists tenv_filename then DB.file_remove tenv_filename; - Sil.store_tenv_to_file tenv_filename tenv + Tenv.store_to_file tenv_filename tenv let () = Arg.parse "INFERLLVM_ARGS" arg_desc (fun _ -> ()) usage; diff --git a/infer/src/llvm/lTrans.ml b/infer/src/llvm/lTrans.ml index 15f67952c..1270f5047 100644 --- a/infer/src/llvm/lTrans.ml +++ b/infer/src/llvm/lTrans.ml @@ -87,7 +87,10 @@ let rec trans_annotated_instructions | Global (Name var_name) | Local (Name var_name) -> let new_local = (Mangled.from_string var_name, trans_typ (Tptr tp)) in (sil_instrs, new_local :: locals) - | _ -> raise (ImproperTypeError "Not expecting alloca instruction to a numbered variable.") + | _ -> + raise + (ImproperTypeError + "Not expecting alloca instruction to a numbered variable.") end | Call (ret_var, func_var, typed_args) -> let new_sil_instr = Sil.Call ( @@ -145,7 +148,8 @@ let trans_function_def (cfg : Cfg.cfg) (cg: Cg.t) (metadata : LAst.metadata_map) (* link all nodes in a chain for now *) | [] -> Cfg.Node.set_succs_exn start_node [exit_node] [exit_node] | nd :: nds -> Cfg.Node.set_succs_exn start_node [nd] [exit_node]; link_nodes nd nds in - let (sil_instrs, locals) = trans_annotated_instructions cfg procdesc metadata annotated_instrs in + let (sil_instrs, locals) = + trans_annotated_instructions cfg procdesc metadata annotated_instrs in let nodes = IList.map (node_of_sil_instr cfg procdesc) sil_instrs in Cfg.Procdesc.set_start_node procdesc start_node; Cfg.Procdesc.set_exit_node procdesc exit_node; @@ -154,10 +158,10 @@ let trans_function_def (cfg : Cfg.cfg) (cg: Cg.t) (metadata : LAst.metadata_map) Cg.add_defined_node cg proc_name; IList.iter (Cg.add_edge cg proc_name) (callees_of_function_def func_def) -let trans_program : LAst.program -> Cfg.cfg * Cg.t * Sil.tenv = function +let trans_program : LAst.program -> Cfg.cfg * Cg.t * Tenv.t = function Program (func_defs, metadata) -> let cfg = Cfg.Node.create_cfg () in let cg = Cg.create () in - let tenv = Sil.create_tenv () in + let tenv = Tenv.create () in IList.iter (trans_function_def cfg cg metadata) func_defs; (cfg, cg, tenv)