diff --git a/.Makefile.lint b/.Makefile.lint
index cdddb760969cc6f1075006562db65d2c0cc5af02..fc916bfa1e33d42ff2e73b588b496e21b2d85da4 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -23,8 +23,6 @@ ML_LINT_KO+=src/kernel_internals/typing/mergecil.ml
ML_LINT_KO+=src/kernel_internals/typing/mergecil.mli
ML_LINT_KO+=src/kernel_internals/typing/oneret.ml
ML_LINT_KO+=src/kernel_internals/typing/oneret.mli
-ML_LINT_KO+=src/kernel_internals/typing/rmtmps.ml
-ML_LINT_KO+=src/kernel_internals/typing/rmtmps.mli
ML_LINT_KO+=src/kernel_internals/typing/translate_lightweight.ml
ML_LINT_KO+=src/kernel_internals/typing/translate_lightweight.mli
ML_LINT_KO+=src/kernel_internals/typing/unroll_loops.ml
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index b09617ac5eb3413608e822429cb55b652cb349cb..2f297109e145abeccf4f84695fc285b976aadb02 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -2882,8 +2882,8 @@ let makeGlobalVarinfo (isadef: bool) (vi: varinfo) : varinfo * bool =
* local. This can happen when we declare an extern variable with
* global scope but we are in a local scope. *)
Kernel.debug ~dkey:Kernel.dkey_typing_global
- "makeGlobalVarinfo isadef=%B vi.vname=%s(%d)"
- isadef vi.vname vi.vid;
+ "makeGlobalVarinfo isadef=%B vi.vname=%s(%d), vreferenced=%B"
+ isadef vi.vname vi.vid vi.vreferenced;
(* This may throw an exception Not_found *)
let oldvi, oldloc = lookupGlobalVar vi.vname in
Kernel.debug ~dkey:Kernel.dkey_typing_global
@@ -4644,6 +4644,7 @@ and makeVarInfoCabs
~(isformal: bool)
~(isglobal: bool)
?(isgenerated=false)
+ ?(referenced=false)
(ldecl : location)
(bt, sto, inline, attrs)
(n,ndt,a)
@@ -4660,7 +4661,8 @@ and makeVarInfoCabs
Kernel.error ~once:true ~current:true "inline for a non-function: %s" n;
checkRestrictQualifierDeep vtype;
(* log "Looking at %s(%b): (%a)@." n isformal d_attrlist nattr;*)
- let vi = makeVarinfo ~temp:isgenerated isglobal isformal n vtype in
+ let vi = makeVarinfo ~referenced ~temp:isgenerated isglobal isformal n vtype
+ in
vi.vstorage <- sto;
vi.vattr <- nattr;
vi.vdecl <- ldecl;
@@ -8218,11 +8220,17 @@ and createGlobal ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool * A
let is_fc_builtin {A.expr_node=enode} =
match enode with A.VARIABLE "FC_BUILTIN" -> true | _ -> false
in
+ let is_fc_stdlib {A.expr_node=enode} =
+ match enode with A.VARIABLE v when v = fc_stdlib -> true | _ -> false
+ in
let isgenerated =
List.exists (fun (_,el) -> List.exists is_fc_builtin el) a
in
+ let islibc =
+ List.exists (fun (_,el) -> List.exists is_fc_stdlib el) a
+ in
(* Make a first version of the varinfo *)
- let vi = makeVarInfoCabs ~ghost ~isformal:false
+ let vi = makeVarInfoCabs ~ghost ~isformal:false ~referenced:islibc
~isglobal:true ~isgenerated (convLoc cloc) (t,s,b,attr_list) (n,ndt,a)
in
(* Add the variable to the environment before doing the initializer
diff --git a/src/kernel_internals/typing/rmtmps.ml b/src/kernel_internals/typing/rmtmps.ml
index 2cc4c84b91adf8d54d4ffb42b36ce889c651aa7c..e22c883010414384126989c604b625b02faefc05 100644
--- a/src/kernel_internals/typing/rmtmps.ml
+++ b/src/kernel_internals/typing/rmtmps.ml
@@ -46,69 +46,63 @@ let dkey = Kernel.dkey_rmtmps
open Extlib
open Cil_types
open Cil
-module H = Hashtbl
-(* Set on the command-line: *)
+(* Reachability of used data is stored in a table mapping [info] to [bool].
+ Note that due to mutability, we need to use our own Hashtbl module which
+ uses [Cil_datatype] equality functions. *)
+type info =
+ | Type of typeinfo
+ | Enum of enuminfo
+ | Comp of compinfo
+ | Var of varinfo
+
+module InfoHashtbl = Hashtbl.Make(struct
+ type t = info
+ let equal i1 i2 = match i1, i2 with
+ | Type t1, Type t2 -> Cil_datatype.Typeinfo.equal t1 t2
+ | Enum e1, Enum e2 -> Cil_datatype.Enuminfo.equal e1 e2
+ | Comp c1, Comp c2 -> Cil_datatype.Compinfo.equal c1 c2
+ | Var v1, Var v2 -> Cil_datatype.Varinfo.equal v1 v2
+ | _, _ -> false
+ let hash = function
+ | Type t -> Cil_datatype.Typeinfo.hash t
+ | Enum e -> Cil_datatype.Enuminfo.hash e
+ | Comp c -> Cil_datatype.Compinfo.hash c
+ | Var v -> Cil_datatype.Varinfo.hash v
+ end)
+
+(* Used by external plug-ins: *)
let keepUnused = ref false
+
+(* Possibly no longer used: *)
let rmUnusedInlines = ref false
let rmUnusedStatic = ref false
-(***********************************************************************
- *
- * Clearing of "referenced" bits
- *
- *)
-
+let is_reachable t r = try InfoHashtbl.find t r with Not_found -> false
-let clearReferencedBits file =
- let considerGlobal global =
- match global with
- | GType (info, _) ->
- info.treferenced <- false
-
- | GEnumTag (info, _)
- | GEnumTagDecl (info, _) ->
- Kernel.debug ~dkey "clearing mark: %a" Cil_printer.pp_global global;
- info.ereferenced <- false
-
- | GCompTag (info, _)
- | GCompTagDecl (info, _) ->
- info.creferenced <- false
-
- | GVar (vi, _, _)
- | GFunDecl (_, vi, _)
- | GVarDecl (vi, _) ->
- vi.vreferenced <- false
-
- | GFun ({svar = info} as func, _) ->
- info.vreferenced <- false;
- let clearMark local =
- local.vreferenced <- false
- in
- List.iter clearMark func.slocals
-
- | _ ->
- ()
- in
- iterGlobals file considerGlobal
+let pp_info fmt = function
+ | Type ti -> Format.fprintf fmt "%s" ti.tname
+ | Enum ei -> Format.fprintf fmt "%s" ei.ename
+ | Comp ci -> Format.fprintf fmt "%s" ci.cname
+ | Var vi -> Format.fprintf fmt "%s" vi.vname
(***********************************************************************
*
* Scanning and categorization of pragmas
*
- *)
+*)
(* collections of names of things to keep *)
-type collection = (string, unit) H.t
+type collection = (string, unit) Hashtbl.t
type keepers = {
- typedefs : collection;
- enums : collection;
- structs : collection;
- unions : collection;
- defines : collection;
- }
+ typedefs : collection;
+ enums : collection;
+ structs : collection;
+ unions : collection;
+ defines : collection;
+}
(* rapid transfer of control when we find a malformed pragma *)
@@ -117,17 +111,17 @@ exception Bad_pragma
(* CIL and CCured define several pragmas which prevent removal of
* various global varinfos. Here we scan for those pragmas and build
* up collections of the corresponding varinfos' names.
- *)
+*)
-let categorizePragmas file =
+let categorizePragmas ast =
(* names of things which should be retained *)
let keepers = {
- typedefs = H.create 1;
- enums = H.create 1;
- structs = H.create 1;
- unions = H.create 1;
- defines = H.create 1
+ typedefs = Hashtbl.create 1;
+ enums = Hashtbl.create 1;
+ structs = Hashtbl.create 1;
+ unions = Hashtbl.create 1;
+ defines = Hashtbl.create 1
} in
(* populate these name collections in light of each pragma *)
@@ -138,59 +132,59 @@ let categorizePragmas file =
in
function
- | GPragma (Attr ("cilnoremove" as directive, args), (location,_)) ->
- (* a very flexible pragma: can retain typedefs, enums,
- * structs, unions, or globals (functions or variables) *)
- begin
- let processArg arg =
- try
- match arg with
- | AStr specifier ->
- (* isolate and categorize one varinfo name *)
- let collection, name =
- (* Two words denotes a typedef, enum, struct, or
- * union, as in "type foo" or "enum bar". A
- * single word denotes a global function or
- * variable. *)
- let whitespace = Str.regexp "[ \t]+" in
- let words = Str.split whitespace specifier in
- match words with
- | ["type"; name] ->
- keepers.typedefs, name
- | ["enum"; name] ->
- keepers.enums, name
- | ["struct"; name] ->
- keepers.structs, name
- | ["union"; name] ->
- keepers.unions, name
- | [name] ->
- keepers.defines, name
- | _ ->
- raise Bad_pragma
- in
- H.add collection name ()
- | _ ->
- raise Bad_pragma
- with Bad_pragma ->
- badPragma location directive
- in
- List.iter processArg args
- end
- | GFunDecl (_,v, _) -> begin
- (* Look for alias attributes, e.g. Linux modules *)
- match filterAttributes "alias" v.vattr with
- | [] -> () (* ordinary prototype. *)
- | [ Attr("alias", [AStr othername]) ] ->
- H.add keepers.defines othername ()
- | _ ->
- Kernel.fatal ~current:true
- "Bad alias attribute at %a"
- Cil_printer.pp_location (CurrentLoc.get ())
- end
- | _ ->
- ()
+ | GPragma (Attr ("cilnoremove" as directive, args), (location,_)) ->
+ (* a very flexible pragma: can retain typedefs, enums,
+ * structs, unions, or globals (functions or variables) *)
+ begin
+ let processArg arg =
+ try
+ match arg with
+ | AStr specifier ->
+ (* isolate and categorize one varinfo name *)
+ let collection, name =
+ (* Two words denotes a typedef, enum, struct, or
+ * union, as in "type foo" or "enum bar". A
+ * single word denotes a global function or
+ * variable. *)
+ let whitespace = Str.regexp "[ \t]+" in
+ let words = Str.split whitespace specifier in
+ match words with
+ | ["type"; name] ->
+ keepers.typedefs, name
+ | ["enum"; name] ->
+ keepers.enums, name
+ | ["struct"; name] ->
+ keepers.structs, name
+ | ["union"; name] ->
+ keepers.unions, name
+ | [name] ->
+ keepers.defines, name
+ | _ ->
+ raise Bad_pragma
+ in
+ Hashtbl.add collection name ()
+ | _ ->
+ raise Bad_pragma
+ with Bad_pragma ->
+ badPragma location directive
+ in
+ List.iter processArg args
+ end
+ | GFunDecl (_,v, _) -> begin
+ (* Look for alias attributes, e.g. Linux modules *)
+ match filterAttributes "alias" v.vattr with
+ | [] -> () (* ordinary prototype. *)
+ | [ Attr("alias", [AStr othername]) ] ->
+ Hashtbl.add keepers.defines othername ()
+ | _ ->
+ Kernel.fatal ~current:true
+ "Bad alias attribute at %a"
+ Cil_printer.pp_location (CurrentLoc.get ())
+ end
+ | _ ->
+ ()
in
- iterGlobals file considerPragma;
+ iterGlobals ast considerPragma;
keepers
@@ -199,27 +193,27 @@ let categorizePragmas file =
*
* Root collection from pragmas
*
- *)
+*)
let isPragmaRoot keepers = function
| GType ({tname = name}, _) ->
- H.mem keepers.typedefs name
+ Hashtbl.mem keepers.typedefs name
| GEnumTag ({ename = name}, _)
| GEnumTagDecl ({ename = name}, _) ->
- H.mem keepers.enums name
+ Hashtbl.mem keepers.enums name
| GCompTag ({cname = name; cstruct = structure}, _)
| GCompTagDecl ({cname = name; cstruct = structure}, _) ->
- let collection = if structure then keepers.structs else keepers.unions in
- H.mem collection name
+ let collection = if structure then keepers.structs else keepers.unions in
+ Hashtbl.mem collection name
| GVar ({vname = name; vattr = attrs}, _, _)
| GVarDecl ({vname = name; vattr = attrs}, _)
| GFunDecl (_,{vname = name; vattr = attrs}, _)
| GFun ({svar = {vname = name; vattr = attrs}}, _) ->
- H.mem keepers.defines name ||
- hasAttribute "used" attrs
+ Hashtbl.mem keepers.defines name ||
+ hasAttribute "used" attrs
| _ ->
- false
+ false
@@ -227,15 +221,6 @@ let isPragmaRoot keepers = function
*
* Common root collecting utilities
*
- *)
-(*TODO:remove
-let traceRoot _reason _global =
-(* trace (dprintf "root (%s): %a@!" reason d_shortglobal global);*)
- true
-
-let traceNonRoot _reason _global =
-(* trace (dprintf "non-root (%s): %a@!" reason d_shortglobal global);*)
- false
*)
let hasExportingAttribute funvar =
let isExportingAttribute = function
@@ -245,13 +230,11 @@ let hasExportingAttribute funvar =
in
List.exists isExportingAttribute funvar.vattr
-
-
(***********************************************************************
*
* Root collection from external linkage
*
- *)
+*)
(* Exported roots are those global varinfos which are visible to the
@@ -264,43 +247,44 @@ let hasExportingAttribute funvar =
* - the function named "main"
* gcc incorrectly (according to C99) makes inline functions visible to
* the linker. So we can only remove inline functions on MSVC.
- *)
+*)
let isExportedRoot global =
let name, result, reason = match global with
- | GVar ({vstorage = Static} as v, _, _) when
- Cil.hasAttribute "FC_BUILTIN" v.vattr ->
- v.vname, true, "FC_BUILTIN attribute"
- | GVar ({vstorage = Static; vname}, _, _) -> vname, false, "static variable"
- | GVar (v,_,_) ->
- v.vname, true, "non-static variable"
- | GFun ({svar = v}, _) -> begin
- if hasExportingAttribute v then
- v.vname,true, "constructor or destructor function"
- else if v.vstorage = Static then
- v.vname, not !rmUnusedStatic, "static function"
- else if v.vinline && v.vstorage != Extern
- && (Cil.msvcMode () || !rmUnusedInlines) then
- v.vname, false, "inline function"
- else
- v.vname, true, "other function"
- end
- | GFunDecl(_,v,_) when hasAttribute "alias" v.vattr ->
- v.vname, true, "has GCC alias attribute"
- | GFunDecl(_,v,_) | GVarDecl(v,_) when hasAttribute "FC_BUILTIN" v.vattr ->
- v.vname, true, "has FC_BUILTIN attribute"
- | GAnnot _ -> "", true, "global annotation"
- | GType (t, _) when
- Cil.hasAttribute "FC_BUILTIN" (Cil.typeAttr t.ttype) ->
- t.tname, true, "has FC_BUILTIN attribute"
- | GCompTag (c,_) | GCompTagDecl (c,_) when
- Cil.hasAttribute "FC_BUILTIN" c.cattr ->
- c.cname, true, "has FC_BUILTIN attribute"
- | GEnumTag (e, _) | GEnumTagDecl (e,_) when
- Cil.hasAttribute "FC_BUILTIN" e.eattr ->
- e.ename, true, "has FC_BUILTIN attribute"
- | _ ->
- "", false, "neither function nor variable nor annotation"
+ | GVar ({vstorage = Static} as v, _, _) when
+ Cil.hasAttribute "FC_BUILTIN" v.vattr ->
+ v.vname, true, "FC_BUILTIN attribute"
+ | GVar ({vstorage = Static; vname}, _, _) -> vname, false, "static variable"
+ | GVar (v,_,_) ->
+ v.vname, true, "non-static variable"
+ | GFun ({svar = v}, _) -> begin
+ if hasExportingAttribute v then
+ v.vname,true, "constructor or destructor function"
+ else if v.vstorage = Static then
+ v.vname, not !rmUnusedStatic, "static function"
+ else if v.vinline && v.vstorage != Extern
+ && (Cil.msvcMode () || !rmUnusedInlines) then
+ v.vname, false, "inline function"
+ else
+ v.vname, true, "other function"
+ end
+ | GFunDecl(_,v,_) when hasAttribute "alias" v.vattr ->
+ v.vname, true, "has GCC alias attribute"
+ | GFunDecl(_,v,_) | GVarDecl(v,_) when hasAttribute "FC_BUILTIN" v.vattr ->
+ v.vname, true, "has FC_BUILTIN attribute"
+ | GAnnot _ -> "", true, "global annotation"
+ | GType (t, _) when
+ Cil.hasAttribute "FC_BUILTIN" (Cil.typeAttr t.ttype) ->
+ t.tname, true, "has FC_BUILTIN attribute"
+ | GCompTag (c,_) | GCompTagDecl (c,_) when
+ Cil.hasAttribute "FC_BUILTIN" c.cattr ->
+ c.cname, true, "has FC_BUILTIN attribute"
+ | GEnumTag (e, _) | GEnumTagDecl (e,_) when
+ Cil.hasAttribute "FC_BUILTIN" e.eattr ->
+ e.ename, true, "has FC_BUILTIN attribute"
+ | _ ->
+ (Format.asprintf "%a" Cil_types_debug.pp_global global), false,
+ "neither fundef nor vardef nor annotation"
in
Kernel.debug
~dkey "isExportedRoot %s -> %B, %s" name result reason;
@@ -312,25 +296,25 @@ let isExportedRoot global =
*
* Root collection for complete programs
*
- *)
+*)
(* Exported roots are "main()" and functions bearing a "constructor"
* or "destructor" attribute. These are the only things which must be
* retained in a complete program.
- *)
+*)
let isCompleteProgramRoot global =
let result = match global with
- | GFun ({svar = {vname = "main"; vstorage = vstorage}}, _) ->
+ | GFun ({svar = {vname = "main"; vstorage = vstorage}}, _) ->
vstorage <> Static
- | GFun (fundec, _)
- when hasExportingAttribute fundec.svar ->
+ | GFun (fundec, _)
+ when hasExportingAttribute fundec.svar ->
true
- | _ ->
+ | _ ->
false
in
-(* trace (dprintf "complete program root -> %b for %a@!" result d_shortglobal global);*)
+ (* trace (dprintf "complete program root -> %b for %a@!" result d_shortglobal global);*)
result
@@ -338,171 +322,211 @@ let isCompleteProgramRoot global =
*
* Transitive reachability closure from roots
*
- *)
+*)
(* This visitor recursively marks all reachable types and variables as used. *)
class markReachableVisitor
- ((globalMap: (string, Cil_types.global) H.t),
- (currentFunc: Cil_types.fundec option ref)) = object (self)
- inherit nopCilVisitor
-
- method! vglob = function
- | GType (typeinfo, _) ->
- typeinfo.treferenced <- true;
- DoChildren
- | GCompTag (compinfo, _)
- | GCompTagDecl (compinfo, _) ->
- compinfo.creferenced <- true;
- DoChildren
- | GEnumTag (enuminfo, _)
- | GEnumTagDecl (enuminfo, _) ->
- enuminfo.ereferenced <- true;
- DoChildren
- | GVar (varinfo, _, _)
- | GVarDecl (varinfo, _)
- | GFunDecl (_,varinfo, _)
- | GFun ({svar = varinfo}, _) ->
- if not (hasAttribute "FC_BUILTIN" varinfo.vattr) then
- varinfo.vreferenced <- true;
- DoChildren
- | GAnnot _ -> DoChildren
- | _ ->
- SkipChildren
-
- method! vstmt s =
- match s.skind with
- | TryCatch(_,c,_) ->
- List.iter
- (fun (decl,_) ->
- match decl with
- | Catch_exn(v,l) ->
- (* treat all variables declared in exn clause as used. *)
- ignore (self#vvrbl v);
- List.iter (fun (v,_) -> ignore (self#vvrbl v)) l
- | Catch_all -> ())
- c;
- DoChildren
- | _ -> DoChildren
+ (globalMap: (string, Cil_types.global) Hashtbl.t)
+ (currentFunc: Cil_types.fundec option ref)
+ (reachable_tbl: bool InfoHashtbl.t)
+ = object (self)
+ inherit nopCilVisitor
+
+ method! vglob = function
+ | GType (typeinfo, _) ->
+ Kernel.debug ~dkey "marking reachable: type %s" typeinfo.tname;
+ InfoHashtbl.replace reachable_tbl (Type typeinfo) true;
+ DoChildren
+ | GCompTag (compinfo, _)
+ | GCompTagDecl (compinfo, _) ->
+ Kernel.debug ~dkey "marking reachable: comp decl %s" compinfo.cname;
+ InfoHashtbl.replace reachable_tbl (Comp compinfo) true;
+ DoChildren
+ | GEnumTag (enuminfo, _)
+ | GEnumTagDecl (enuminfo, _) ->
+ Kernel.debug ~dkey "marking reachable: enum decl %s" enuminfo.ename;
+ InfoHashtbl.replace reachable_tbl (Enum enuminfo) true;
+ DoChildren
+ | GVar (varinfo, _, _)
+ | GVarDecl (varinfo, _)
+ | GFunDecl (_,varinfo, _)
+ | GFun ({svar = varinfo}, _) ->
+ if not (hasAttribute "FC_BUILTIN" varinfo.vattr) then
+ begin
+ Kernel.debug ~dkey "marking reachable: function %s" varinfo.vname;
+ InfoHashtbl.replace reachable_tbl (Var varinfo) true;
+ end;
+ DoChildren
+ | GAnnot _ -> DoChildren
+ | _ ->
+ SkipChildren
+
+ method! vstmt s =
+ match s.skind with
+ | TryCatch(_,c,_) ->
+ List.iter
+ (fun (decl,_) ->
+ match decl with
+ | Catch_exn(v,l) ->
+ (* treat all variables declared in exn clause as used. *)
+ ignore (self#vvrbl v);
+ List.iter (fun (v,_) -> ignore (self#vvrbl v)) l
+ | Catch_all -> ())
+ c;
+ DoChildren
+ | _ -> DoChildren
- method! vinst = function
- | Asm (_, tmpls, _, _) when Cil.msvcMode () ->
- (* If we have inline assembly on MSVC, we cannot tell which locals
- * are referenced. Keep them all *)
+ method! vinst = function
+ | Asm (_, tmpls, _, _) when Cil.msvcMode () ->
+ (* If we have inline assembly on MSVC, we cannot tell which locals
+ * are referenced. Keep them all *)
(match !currentFunc with
- Some fd ->
- List.iter (fun v ->
- let vre = Str.regexp_string (Str.quote v.vname) in
- if List.exists (fun tmp ->
- try ignore (Str.search_forward vre tmp 0); true
- with Not_found -> false)
- tmpls
- then
- v.vreferenced <- true) fd.slocals
- | _ -> assert false);
+ Some fd ->
+ List.iter (fun v ->
+ let vre = Str.regexp_string (Str.quote v.vname) in
+ if List.exists (fun tmp ->
+ try ignore (Str.search_forward vre tmp 0); true
+ with Not_found -> false)
+ tmpls
+ then
+ InfoHashtbl.replace reachable_tbl (Var v) true
+ ) fd.slocals
+ | _ -> assert false);
DoChildren
- | _ -> DoChildren
+ | _ -> DoChildren
+
+ method! vvrbl v =
+ if not (is_reachable reachable_tbl (Var v)) then
+ begin
+ let name = v.vname in
+ if v.vglob then
+ Kernel.debug ~dkey "marking transitive use: global %s (%d)" name v.vid
+ else
+ Kernel.debug ~dkey "marking transitive use: local %s (%d)" name v.vid;
+
+ (* If this is a global, we need to keep everything used in its
+ * definition and declarations. *)
+ InfoHashtbl.replace reachable_tbl (Var v) true;
+ if v.vglob then
+ begin
+ Kernel.debug ~dkey "descending: global %s (%d)" name v.vid;
+ let descend global =
+ ignore (visitCilGlobal (self :> cilVisitor) global)
+ in
+ let globals = Hashtbl.find_all globalMap name in
+ List.iter descend globals
+ end
+ end;
+ SkipChildren
+
+ method private mark_enum e =
+ if not (is_reachable reachable_tbl (Enum e)) then
+ begin
+ Kernel.debug ~dkey "marking transitive use: enum %s" e.ename;
+ InfoHashtbl.replace reachable_tbl (Enum e) true;
+ self#visitAttrs e.eattr;
+ (* Must visit the value attributed to the enum constants *)
+ ignore (visitCilEnumInfo (self:>cilVisitor) e);
+ end
+ else
+ Kernel.debug ~dkey "not marking transitive use: enum %s" e.ename;
- method! vvrbl v =
- if not v.vreferenced then
- begin
- let name = v.vname in
- if v.vglob then
- Kernel.debug ~dkey "marking transitive use: global %s" name
- else
- Kernel.debug ~dkey "marking transitive use: local %s" name;
-
- (* If this is a global, we need to keep everything used in its
- * definition and declarations. *)
- v.vreferenced <- true;
- if v.vglob then
- begin
- Kernel.debug ~dkey "descending: global %s" name;
- let descend global =
- ignore (visitCilGlobal (self :> cilVisitor) global)
- in
- let globals = Hashtbl.find_all globalMap name in
- List.iter descend globals
- end
- end;
- SkipChildren
+ method! vexpr e =
+ match e.enode with
+ Const (CEnum {eihost = ei}) -> self#mark_enum ei; DoChildren
+ | _ -> DoChildren
- method private mark_enum e =
- if not e.ereferenced then
- begin
- Kernel.debug ~dkey "marking transitive use: enum %s\n" e.ename;
- e.ereferenced <- true;
- self#visitAttrs e.eattr;
- (* Must visit the value attributed to the enum constants *)
- ignore (visitCilEnumInfo (self:>cilVisitor) e);
- end
- else
- Kernel.debug ~dkey "not marking transitive use: enum %s\n" e.ename;
-
- method! vexpr e =
- match e.enode with
- Const (CEnum {eihost = ei}) -> self#mark_enum ei; DoChildren
- | _ -> DoChildren
-
- method! vterm_node t =
- match t with
- TConst (LEnum {eihost = ei}) -> self#mark_enum ei; DoChildren
- | _ -> DoChildren
-
- method private visitAttrs attrs =
- ignore (visitCilAttributes (self :> cilVisitor) attrs)
-
- method! vtype typ =
- (match typ with
- | TEnum(e, attrs) ->
- self#visitAttrs attrs;
- self#mark_enum e
-
- | TComp(c, _, attrs) ->
- let old = c.creferenced in
- if not old then
- begin
- Kernel.debug ~dkey "marking transitive use: compound %s\n"
- c.cname;
- c.creferenced <- true;
-
- (* to recurse, we must ask explicitly *)
- let recurse f = ignore (self#vtype f.ftype) in
- List.iter recurse c.cfields;
- self#visitAttrs attrs;
- self#visitAttrs c.cattr
- end;
-
- | TNamed(ti, attrs) ->
- let old = ti.treferenced in
- if not old then
- begin
- Kernel.debug ~dkey "marking transitive use: typedef %s\n"
- ti.tname;
- ti.treferenced <- true;
-
- (* recurse deeper into the type referred-to by the typedef *)
- (* to recurse, we must ask explicitly *)
- ignore (self#vtype ti.ttype);
- self#visitAttrs attrs
- end;
-
- | TVoid a | TInt (_,a) | TFloat (_,a) | TBuiltin_va_list a ->
+ method! vterm_node t =
+ match t with
+ TConst (LEnum {eihost = ei}) -> self#mark_enum ei; DoChildren
+ | _ -> DoChildren
+
+ method private visitAttrs attrs =
+ ignore (visitCilAttributes (self :> cilVisitor) attrs)
+
+ method! vtype typ =
+ (match typ with
+ | TEnum(e, attrs) ->
+ self#visitAttrs attrs;
+ self#mark_enum e
+
+ | TComp(c, _, attrs) ->
+ let old = is_reachable reachable_tbl (Comp c) in
+ if not old then
+ begin
+ Kernel.debug ~dkey "marking transitive use: compound %s"
+ c.cname;
+ InfoHashtbl.replace reachable_tbl (Comp c) true;
+
+ (* to recurse, we must ask explicitly *)
+ let recurse f = ignore (self#vtype f.ftype) in
+ List.iter recurse c.cfields;
+ self#visitAttrs attrs;
+ self#visitAttrs c.cattr
+ end;
+
+ | TNamed(ti, attrs) ->
+ let old = (is_reachable reachable_tbl (Type ti)) in
+ if not old then
+ begin
+ Kernel.debug ~dkey "marking transitive use: typedef %s"
+ ti.tname;
+ InfoHashtbl.replace reachable_tbl (Type ti) true;
+ (* recurse deeper into the type referred-to by the typedef *)
+ (* to recurse, we must ask explicitly *)
+ ignore (self#vtype ti.ttype);
+ self#visitAttrs attrs
+ end;
+
+ | TVoid a | TInt (_,a) | TFloat (_,a) | TBuiltin_va_list a ->
self#visitAttrs a
- | TPtr(ty,a) -> ignore (self#vtype ty); self#visitAttrs a
- | TArray(ty,sz, _, a) ->
- ignore (self#vtype ty); self#visitAttrs a;
- Extlib.may (ignore $ (visitCilExpr (self:>cilVisitor))) sz
- | TFun (ty, args,_,a) ->
- ignore (self#vtype ty);
- Extlib.may (List.iter (fun (_,ty,_) -> ignore (self#vtype ty))) args;
- self#visitAttrs a
- );
- SkipChildren
-end
+ | TPtr(ty,a) -> ignore (self#vtype ty); self#visitAttrs a
+ | TArray(ty,sz, _, a) ->
+ ignore (self#vtype ty); self#visitAttrs a;
+ Extlib.may (ignore $ (visitCilExpr (self:>cilVisitor))) sz
+ | TFun (ty, args,_,a) ->
+ ignore (self#vtype ty);
+ Extlib.may (List.iter (fun (_,ty,_) -> ignore (self#vtype ty))) args;
+ self#visitAttrs a
+ );
+ SkipChildren
+ method! vlogic_var_decl lv =
+ Kernel.debug ~dkey "markReachable: found LOGIC VAR DECL for: %s (%d)\n" lv.lv_name lv.lv_id;
+ DoChildren
-let markReachable file isRoot =
+ method! vlogic_var_use lv =
+ Kernel.debug ~dkey "markReachable: found LOGIC VAR USE for: %s (%d)\n" lv.lv_name lv.lv_id;
+ match lv.lv_origin with
+ | None -> SkipChildren
+ | Some v ->
+ if not (is_reachable reachable_tbl (Var v)) then
+ begin
+ let name = v.vname in
+ if v.vglob then
+ Kernel.debug ~dkey "marking transitive use for logic var: global %s (%d)" name v.vid
+ else
+ Kernel.debug ~dkey "marking transitive use for logic var: local %s (%d)" name v.vid;
+
+ (* If this is a global, we need to keep everything used in its
+ * definition and declarations. *)
+ InfoHashtbl.replace reachable_tbl (Var v) true;
+ if v.vglob then
+ begin
+ Kernel.debug ~dkey "descending: global %s (%d)" name v.vid;
+ let descend global =
+ ignore (visitCilGlobal (self :> cilVisitor) global)
+ in
+ let globals = Hashtbl.find_all globalMap name in
+ List.iter descend globals
+ end
+ end;
+ SkipChildren
+ end
+
+
+let markReachable isRoot ast reachable_tbl =
(* build a mapping from global names back to their definitions &
* declarations *)
let globalMap = Hashtbl.create 137 in
@@ -512,31 +536,137 @@ let markReachable file isRoot =
| GVar (info, _, _)
| GFunDecl (_,info, _)
| GVarDecl (info, _) ->
- Hashtbl.add globalMap info.vname global
+ Hashtbl.add globalMap info.vname global
| _ ->
- ()
+ ()
in
- iterGlobals file considerGlobal;
+ iterGlobals ast considerGlobal;
let currentFunc = ref None in
(* mark everything reachable from the global roots *)
- let visitor = new markReachableVisitor (globalMap, currentFunc) in
+ let visitor = new markReachableVisitor globalMap currentFunc reachable_tbl in
let visitIfRoot global =
if isRoot global then
begin
-(* trace (dprintf "traversing root global: %a\n" d_shortglobal global);*)
+ (* trace (dprintf "traversing root global: %a\n" d_shortglobal global);*)
(match global with
- GFun(fd, _) -> currentFunc := Some fd
- | _ -> currentFunc := None);
- ignore (visitCilGlobal visitor global)
+ GFun(fd, _) -> currentFunc := Some fd
+ | _ -> currentFunc := None);
+ ignore (visitCilGlobal visitor global)
end
else
-(* trace (dprintf "skipping non-root global: %a\n" d_shortglobal global)*)
+ (* trace (dprintf "skipping non-root global: %a\n" d_shortglobal global)*)
()
in
- iterGlobals file visitIfRoot
+ iterGlobals ast visitIfRoot
+
+(**********************************************************************
+ *
+ * Marking of referenced infos
+ *
+ **********************************************************************)
+
+let global_type_and_name = function
+ | GType (t, _) -> "type " ^ t.tname
+ | GCompTag (c,_) -> "comp " ^ c.cname
+ | GCompTagDecl (c,_) -> "comp decl " ^ c.cname
+ | GEnumTag (e, _) -> "enum " ^ e.ename
+ | GEnumTagDecl (e,_) -> "enum decl " ^ e.ename
+ | GVarDecl(v,_) -> "var decl " ^ v.vname
+ | GFunDecl(_,v,_) -> "fun decl " ^ v.vname
+ | GVar (v, _, _) -> "var " ^ v.vname
+ | GFun ({svar = v}, _) -> "fun " ^ v.vname
+ | GAsm _ -> "<asm>"
+ | GPragma _ -> "<pragma>"
+ | GText _ -> "<text>"
+ | GAnnot _ -> "<annot>"
+
+class markReferencedVisitor = object
+ inherit nopCilVisitor
+
+ val dkey = Kernel.dkey_referenced
+
+ val inside_exp : exp Stack.t = Stack.create ()
+ val inside_typ : typ Stack.t = Stack.create ()
+
+ method! vglob = function
+ | GType (typeinfo, loc) ->
+ Kernel.debug ~source:(fst loc) ~dkey "referenced: type %s" typeinfo.tname;
+ typeinfo.treferenced <- true;
+ DoChildren
+ | GCompTag (compinfo, loc)
+ | GCompTagDecl (compinfo, loc) ->
+ Kernel.debug ~source:(fst loc) ~dkey "referenced: comp %s" compinfo.cname;
+ compinfo.creferenced <- true;
+ DoChildren
+ | GEnumTag (enuminfo, loc)
+ | GEnumTagDecl (enuminfo, loc) ->
+ Kernel.debug ~source:(fst loc) ~dkey "referenced: enum %s" enuminfo.ename;
+ enuminfo.ereferenced <- true;
+ DoChildren
+ | GVar (varinfo, _, loc)
+ | GVarDecl (varinfo, loc)
+ | GFunDecl (_,varinfo, loc)
+ | GFun ({svar = varinfo}, loc) ->
+ Kernel.debug ~dkey "referenced: var/fun %s@." varinfo.vname;
+ Kernel.debug ~source:(fst loc) ~dkey "referenced: fun %s" varinfo.vname;
+ varinfo.vreferenced <- true;
+ DoChildren
+ | GAnnot _ -> DoChildren
+ | _ ->
+ SkipChildren
+
+ method! vtype = function
+ | TNamed (ti, _) ->
+ if not (Stack.is_empty inside_typ) then begin
+ Kernel.debug ~current:true ~dkey "referenced: type %s" ti.tname;
+ ti.treferenced <- true;
+ end;
+ DoChildren
+ | TComp (ci, _, _) ->
+ if not (Stack.is_empty inside_typ) then begin
+ Kernel.debug ~current:true ~dkey "referenced: comp %s" ci.cname;
+ ci.creferenced <- true;
+ end;
+ DoChildren
+ | TEnum (ei, _) ->
+ if not (Stack.is_empty inside_typ) then begin
+ Kernel.debug ~current:true ~dkey "referenced: enum %s" ei.ename;
+ ei.ereferenced <- true;
+ end;
+ DoChildren
+ | TVoid _
+ | TInt _
+ | TFloat _
+ | TPtr _
+ | TArray _
+ | TFun _
+ | TBuiltin_va_list _ -> DoChildren
+
+ method! vexpr e =
+ match e.enode with
+ | SizeOf t | AlignOf t | UnOp (_, _, t) | BinOp (_, _, _, t) ->
+ Stack.push t inside_typ;
+ DoChildrenPost (fun e -> ignore (Stack.pop inside_typ); e)
+ | _ ->
+ Stack.push e inside_exp;
+ DoChildrenPost (fun e -> ignore (Stack.pop inside_exp); e)
+
+ method! vvrbl v =
+ if not (Stack.is_empty inside_exp) then begin
+ Kernel.debug ~current:true ~dkey "referenced: var %s" v.vname;
+ v.vreferenced <- true;
+ end;
+ SkipChildren
+
+end
+let markReferenced ast =
+ Kernel.debug ~dkey "starting markReferenced (AST has %d globals)"
+ (List.length ast.globals);
+ visitCilFileSameGlobals (new markReferencedVisitor) ast;
+ Kernel.debug ~dkey "finished markReferenced"
(**********************************************************************
*
@@ -551,88 +681,88 @@ let labelsToKeep is_removable ll =
let rec loop sofar = function
[] -> sofar, []
| l :: rest ->
- let newlabel, keepl =
- match l with
- | Case _ | Default _ -> sofar, true
- | Label (ln, _, _) as lab -> begin
- match is_removable lab, sofar with
- | true, ("", _) ->
- (* keep this one only if we have no label so far *)
- (ln, lab), false
- | true, _ -> sofar, false
- | false, (_, lab') when is_removable lab' ->
- (* this is an original label; prefer it to temporary or
- * missing labels *)
- (ln, lab), false
- | false, _ -> sofar, false
+ let newlabel, keepl =
+ match l with
+ | Case _ | Default _ -> sofar, true
+ | Label (ln, _, _) as lab -> begin
+ match is_removable lab, sofar with
+ | true, ("", _) ->
+ (* keep this one only if we have no label so far *)
+ (ln, lab), false
+ | true, _ -> sofar, false
+ | false, (_, lab') when is_removable lab' ->
+ (* this is an original label; prefer it to temporary or
+ * missing labels *)
+ (ln, lab), false
+ | false, _ -> sofar, false
end
- in
- let newlabel', rest' = loop newlabel rest in
- newlabel', (if keepl then l :: rest' else rest')
+ in
+ let newlabel', rest' = loop newlabel rest in
+ newlabel', (if keepl then l :: rest' else rest')
in
loop ("", Label("", Cil_datatype.Location.unknown, false)) ll
-class markUsedLabels is_removable (labelMap: (string, unit) H.t) =
+class markUsedLabels is_removable (labelMap: (string, unit) Hashtbl.t) =
let keep_label dest =
- let (ln, _), _ = labelsToKeep is_removable !dest.labels in
- if ln = "" then
- Kernel.fatal "Statement has no label:@\n%a" Cil_printer.pp_stmt !dest ;
- (* Mark it as used *)
- H.replace labelMap ln ()
-in
-let keep_label_logic = function
- | FormalLabel _ | BuiltinLabel _ -> ()
- | StmtLabel dest -> keep_label dest
-in
-object
- inherit nopCilVisitor
+ let (ln, _), _ = labelsToKeep is_removable !dest.labels in
+ if ln = "" then
+ Kernel.fatal "Statement has no label:@\n%a" Cil_printer.pp_stmt !dest ;
+ (* Mark it as used *)
+ Hashtbl.replace labelMap ln ()
+ in
+ let keep_label_logic = function
+ | FormalLabel _ | BuiltinLabel _ -> ()
+ | StmtLabel dest -> keep_label dest
+ in
+ object
+ inherit nopCilVisitor
- method! vstmt (s: stmt) =
- match s.skind with
- Goto (dest, _) -> keep_label dest; DoChildren
- | _ -> DoChildren
+ method! vstmt (s: stmt) =
+ match s.skind with
+ Goto (dest, _) -> keep_label dest; DoChildren
+ | _ -> DoChildren
- method! vterm_node t =
- begin
- match t with
- | Tat (_,lab) -> keep_label_logic lab
- | Tapp(_,labs,_) ->
+ method! vterm_node t =
+ begin
+ match t with
+ | Tat (_,lab) -> keep_label_logic lab
+ | Tapp(_,labs,_) ->
List.iter keep_label_logic labs
- | _ -> ()
- end;
- DoChildren
+ | _ -> ()
+ end;
+ DoChildren
- method! vpredicate_node t =
- begin
- match t with
- | Pat (_,lab) -> keep_label_logic lab
- | Papp(_,labs,_) ->
+ method! vpredicate_node t =
+ begin
+ match t with
+ | Pat (_,lab) -> keep_label_logic lab
+ | Papp(_,labs,_) ->
List.iter keep_label_logic labs
- | _ -> ()
- end;
- DoChildren
+ | _ -> ()
+ end;
+ DoChildren
- (* No need to go into expressions or types *)
- method! vexpr _ = SkipChildren
- method! vtype _ = SkipChildren
- end
+ (* No need to go into expressions or types *)
+ method! vexpr _ = SkipChildren
+ method! vtype _ = SkipChildren
+ end
-class removeUnusedLabels is_removable (labelMap: (string, unit) H.t) = object
+class removeUnusedLabels is_removable (labelMap: (string, unit) Hashtbl.t) = object
inherit nopCilVisitor
method! vstmt (s: stmt) =
let (ln, lab), lrest = labelsToKeep is_removable s.labels in
s.labels <-
- (if ln <> "" &&
- (H.mem labelMap ln || not (is_removable lab))
+ (if ln <> "" &&
+ (Hashtbl.mem labelMap ln || not (is_removable lab))
(* keep user-provided labels *)
- then (* We had labels *)
+ then (* We had labels *)
(lab :: lrest)
else
lrest);
DoChildren
- (* No need to go into expressions or instructions *)
+ (* No need to go into expressions or instructions *)
method! vexpr _ = SkipChildren
method! vinst _ = SkipChildren
method! vtype _ = SkipChildren
@@ -642,36 +772,7 @@ end
*
* Removal of unused varinfos
*
- *)
-
-
-(* regular expression matching names of uninteresting locals *)
-let uninteresting =
- let names = [
- (* Cil.makeTempVar *)
- "__cil_tmp";
-
- (* sm: I don't know where it comes from but these show up all over. *)
- (* this doesn't seem to do what I wanted.. *)
- "iter";
-
- (* various macros in glibc's <bits/string2.h> *)
- "__result";
- "__s"; "__s1"; "__s2";
- "__s1_len"; "__s2_len";
- "__retval"; "__len";
-
- (* various macros in glibc's <ctype.h> *)
- "__c"; "__res";
-
- (* We remove the __malloc variables *)
- ] in
-
- (* optional alpha renaming *)
- let alpha = "\\(___[0-9]+\\)?" in
-
- let pattern = "\\(" ^ (String.concat "\\|" names) ^ "\\)" ^ alpha ^ "$" in
- Str.regexp pattern
+*)
let label_removable = function
Label (_,_,user) -> not user
@@ -680,74 +781,94 @@ let label_removable = function
let remove_unused_labels ?(is_removable=label_removable) func =
(* We also want to remove unused labels. We do it all here, including
* marking the used labels *)
- let usedLabels:(string, unit) H.t = H.create 13 in
+ let usedLabels:(string, unit) Hashtbl.t = Hashtbl.create 13 in
ignore
(visitCilBlock (new markUsedLabels is_removable usedLabels) func.sbody);
(* And now we scan again and we remove them *)
ignore
(visitCilBlock (new removeUnusedLabels is_removable usedLabels) func.sbody)
-let removeUnmarked isRoot file =
+let removeUnmarked isRoot ast reachable_tbl =
let removedLocals = ref [] in
let filterGlobal global =
match global with
- (* unused global types, variables, and functions are simply removed *)
- | GType (t, _) ->
- t.treferenced ||
- Cil.hasAttribute "FC_BUILTIN" (Cil.typeAttr t.ttype)
- || isRoot global
- | GCompTag (c,_) | GCompTagDecl (c,_) ->
- c.creferenced ||
- Cil.hasAttribute "FC_BUILTIN" c.cattr || isRoot global
- | GEnumTag (e, _) | GEnumTagDecl (e,_) ->
- e.ereferenced ||
- Cil.hasAttribute "FC_BUILTIN" e.eattr || isRoot global
- | GVar (v, _, _) ->
- v.vreferenced ||
- Cil.hasAttribute "FC_BUILTIN" v.vattr || isRoot global
- | GVarDecl (v, _)
- | GFunDecl (_,v, _)->
- v.vreferenced ||
- Cil.hasAttribute "FC_BUILTIN" v.vattr ||
- (Cil.removeFormalsDecl v; isRoot global)
- (* keep FC_BUILTIN, as some plug-ins might want to use them later
- for semi-legitimate reasons. *)
- | GFun (func, _) ->
- (* if some generated temp variables are useless, remove them.
- Keep variables that were already present in the code.
- *)
- let filterLocal local =
- if local.vtemp && not local.vreferenced then
- begin
- (* along the way, record the interesting locals that were removed *)
- let name = local.vname in
- (Kernel.debug ~dkey "removing local: %s\n" name);
- if not (Str.string_match uninteresting name 0) then
- removedLocals :=
- (func.svar.vname ^ "::" ^ name) :: !removedLocals;
- false
- end else true
- in
- func.slocals <- List.filter filterLocal func.slocals;
- let remove_blocals = object
- inherit Cil.nopCilVisitor
- method! vblock b =
- b.blocals <- List.filter filterLocal b.blocals;
- DoChildren
- end
- in
- (func.svar.vreferenced
- || Cil.hasAttribute "FC_BUILTIN" func.svar.vattr
- || isRoot global) &&
- (ignore (visitCilBlock remove_blocals func.sbody);
- remove_unused_labels func;
- true)
-
- (* all other globals are retained *)
- | _ -> true
+ (* unused global types, variables, and functions are simply removed *)
+ | GType (t, _) ->
+ is_reachable reachable_tbl (Type t) ||
+ Cil.hasAttribute "FC_BUILTIN" (Cil.typeAttr t.ttype)
+ || isRoot global
+ | GCompTag (c,_) | GCompTagDecl (c,_) ->
+ is_reachable reachable_tbl (Comp c) ||
+ Cil.hasAttribute "FC_BUILTIN" c.cattr || isRoot global
+ | GEnumTag (e, _) | GEnumTagDecl (e,_) ->
+ is_reachable reachable_tbl (Enum e) ||
+ Cil.hasAttribute "FC_BUILTIN" e.eattr || isRoot global
+ | GVar (v, _, _) ->
+ is_reachable reachable_tbl (Var v) ||
+ Cil.hasAttribute "FC_BUILTIN" v.vattr || isRoot global
+ | GVarDecl (v, _)
+ | GFunDecl (_,v, _)->
+ is_reachable reachable_tbl (Var v) ||
+ Cil.hasAttribute "FC_BUILTIN" v.vattr ||
+ (if isRoot global then true else (Cil.removeFormalsDecl v; false))
+ (* keep FC_BUILTIN, as some plug-ins might want to use them later
+ for semi-legitimate reasons. *)
+ | GFun (func, _) ->
+ (* if some generated temp variables are useless, remove them.
+ Keep variables that were already present in the code.
+ *)
+ let filterLocal local =
+ if local.vtemp && not (is_reachable reachable_tbl (Var local)) then
+ begin
+ (* along the way, record the interesting locals that were removed *)
+ let name = local.vname in
+ (Kernel.debug ~dkey "removing local: %s" name);
+ removedLocals :=
+ (func.svar.vname ^ "::" ^ name) :: !removedLocals;
+ false
+ end else true
+ in
+ func.slocals <- List.filter filterLocal func.slocals;
+ let remove_blocals = object
+ inherit Cil.nopCilVisitor
+ method! vblock b =
+ b.blocals <- List.filter filterLocal b.blocals;
+ DoChildren
+ end
+ in
+ ((is_reachable reachable_tbl (Var func.svar))
+ || Cil.hasAttribute "FC_BUILTIN" func.svar.vattr
+ || isRoot global) &&
+ (ignore (visitCilBlock remove_blocals func.sbody);
+ remove_unused_labels func;
+ true)
+
+ (* all other globals are retained *)
+ | _ -> true
in
- file.globals <- List.filter filterGlobal file.globals;
+ let keptGlobals, removedGlobals = List.partition filterGlobal ast.globals in
+ ast.globals <- keptGlobals;
+ if Kernel.is_debug_key_enabled dkey then
+ List.iter (fun rg ->
+ Kernel.debug ~dkey "removing global: %s" (global_type_and_name rg)
+ ) removedGlobals;
+ if Kernel.is_debug_key_enabled dkey then
+ List.iter (fun rg ->
+ begin
+ match rg with
+ | GFunDecl (_s, vi, _) ->
+ begin
+ try
+ let kf = Globals.Functions.get vi in
+ Kernel.debug ~dkey "GFunDecl: %a@." Kernel_function.pretty_code kf
+ with Not_found ->
+ Kernel.debug ~dkey "GFunDecl: not found for %a@." Printer.pp_varinfo vi;
+ end
+ | _ -> ()
+ end;
+ Kernel.debug ~dkey "kept global %s (%a)" (global_type_and_name rg) Printer.pp_global rg
+ ) keptGlobals;
!removedLocals
@@ -755,42 +876,40 @@ let removeUnmarked isRoot file =
*
* Exported interface
*
- *)
+*)
type rootsFilter = global -> bool
-let isDefaultRoot = isExportedRoot
-
-let removeUnusedTemps ?(isRoot : rootsFilter = isDefaultRoot) file =
+let removeUnusedTemps ?(isRoot : rootsFilter = isExportedRoot) ast =
if not !keepUnused then
begin
Kernel.debug ~dkey "Removing unused temporaries" ;
(* digest any pragmas that would create additional roots *)
- let keepers = categorizePragmas file in
+ let keepers = categorizePragmas ast in
+ let reachable_tbl = InfoHashtbl.create 43 in
(* build up the root set *)
let isRoot global =
- isPragmaRoot keepers global ||
- isRoot global
+ isPragmaRoot keepers global ||
+ isRoot global
in
(* mark everything reachable from the global roots *)
- clearReferencedBits file;
- markReachable file isRoot;
+ markReachable isRoot ast reachable_tbl;
+
+ let elements =
+ InfoHashtbl.fold (fun k v acc -> Format.asprintf "%a:%B" pp_info k v :: acc)
+ reachable_tbl []
+ in
+ Kernel.debug ~dkey "reachable_tbl: %a"
+ (Pretty_utils.pp_list ~sep:"@\n" Format.pp_print_string) elements;
+
+ markReferenced ast;
(* take out the trash *)
- let removedLocals = removeUnmarked isRoot file in
-
- (* print which original source variables were removed *)
- if false && removedLocals != [] then
- let count = List.length removedLocals in
- if count > 2000 then
- (Kernel.warning "%d unused local variables removed" count)
- else
- (Kernel.warning "%d unused local variables removed:@!%a"
- count (Pretty_utils.pp_list ~sep:",@," Format.pp_print_string) removedLocals)
+ ignore (removeUnmarked isRoot ast reachable_tbl)
end
(*
diff --git a/src/kernel_internals/typing/rmtmps.mli b/src/kernel_internals/typing/rmtmps.mli
index c99591522f1790b69002d4ed3a572c01067441dd..510a6565b0551e9045c09aa3913ec2d8735dd80d 100644
--- a/src/kernel_internals/typing/rmtmps.mli
+++ b/src/kernel_internals/typing/rmtmps.mli
@@ -72,11 +72,10 @@
* Note that certain CIL- and CCured-specific pragmas induce
* additional global roots. This functionality is always present, and
* is not subject to replacement by "filterRoots".
- *)
+*)
type rootsFilter = Cil_types.global -> bool
-val isDefaultRoot : rootsFilter
val isExportedRoot : rootsFilter
val isCompleteProgramRoot : rootsFilter
@@ -84,10 +83,10 @@ val isCompleteProgramRoot : rootsFilter
val removeUnusedTemps: ?isRoot:rootsFilter -> Cil_types.file -> unit
(** removes unused labels for which [is_removable] is true.
-[is_removable] defaults to the negation of boolean flag of [Label]
-{i i.e.} only labels generated by CIL may be removed.
-@since Carbon-20101201
- *)
+ [is_removable] defaults to the negation of boolean flag of [Label]
+ {i i.e.} only labels generated by CIL may be removed.
+ @since Carbon-20101201
+*)
val remove_unused_labels:
?is_removable:(Cil_types.label -> bool) -> Cil_types.fundec -> unit
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 79da27bd41da6e97700185a0d1cf6801b9f1c812..c5e01b7134df44a227c6d801e2ab9e1e6f2c0da0 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -578,7 +578,7 @@ type attributeClass =
| x -> x
(* Make a varinfo. Used mostly as a helper function below *)
- let makeVarinfo ?(source=true) ?(temp=false) global formal name typ =
+ let makeVarinfo ?(source=true) ?(temp=false) ?(referenced=false) global formal name typ =
let vi =
{ vorig_name = name;
vname = name;
@@ -593,7 +593,7 @@ type attributeClass =
vattr = [];
vstorage = NoStorage;
vaddrof = false;
- vreferenced = false;
+ vreferenced = referenced;
vdescr = None;
vdescrpure = true;
vghost = false;
@@ -6280,16 +6280,16 @@ let need_cast ?(force=false) oldt newt =
let refresh_local_name fdec vi =
let new_name = findUniqueName fdec vi.vname in vi.vname <- new_name
- let makeLocal ?(temp=false) ?(formal=false) fdec name typ =
+ let makeLocal ?(temp=false) ?referenced ?(formal=false) fdec name typ =
(* a helper function *)
let name = findUniqueName fdec name in
fdec.smaxid <- 1 + fdec.smaxid;
- let vi = makeVarinfo ~temp false formal name typ in
+ let vi = makeVarinfo ~temp ?referenced false formal name typ in
vi
(* Make a local variable and add it to a function *)
- let makeLocalVar fdec ?scope ?(temp=false) ?(insert = true) name typ =
- let vi = makeLocal ~temp fdec name typ in
+ let makeLocalVar fdec ?scope ?(temp=false) ?referenced ?(insert = true) name typ =
+ let vi = makeLocal ~temp ?referenced fdec name typ in
refresh_local_name fdec vi;
if insert then
begin
@@ -6377,8 +6377,8 @@ let need_cast ?(force=false) oldt newt =
(* Make a global variable. Your responsibility to make sure that the name
* is unique *)
- let makeGlobalVar ?source ?temp name typ =
- makeVarinfo ?source ?temp true false name typ
+ let makeGlobalVar ?source ?temp ?referenced name typ =
+ makeVarinfo ?source ?temp ?referenced true false name typ
let mkPureExprInstr ~fundec ~scope ?loc e =
let loc = match loc with None -> e.eloc | Some l -> l in
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 799986722ec0afbc0e43e5acc5cffcd8fb59c5a0..60819b3c6ef5382920d8c8ae345a4d829dbd443e 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -672,10 +672,13 @@ val splitFunctionTypeVI:
[vtemp] field in type {!Cil_types.varinfo}.
The [source] argument defaults to [true], and corresponds to the field
[vsource] .
+ The [referenced] argument defaults to [false], and corresponds to the field
+ [vreferenced] .
The first unnamed argument specifies whether the varinfo is for a global and
the second is for formals. *)
val makeVarinfo:
- ?source:bool -> ?temp:bool -> bool -> bool -> string -> typ -> varinfo
+ ?source:bool -> ?temp:bool -> ?referenced:bool -> bool -> bool -> string ->
+ typ -> varinfo
(** Make a formal variable for a function declaration. Insert it in both the
sformals and the type of the function. You can optionally specify where to
@@ -696,7 +699,7 @@ val makeFormalVar: fundec -> ?where:string -> string -> typ -> varinfo
@modify Chlorine-20180501 the name of the variable is guaranteed to be fresh.
*)
val makeLocalVar:
- fundec -> ?scope:block -> ?temp:bool -> ?insert:bool
+ fundec -> ?scope:block -> ?temp:bool -> ?referenced:bool -> ?insert:bool
-> string -> typ -> varinfo
(** if needed, rename the given varinfo so that its [vname] does not
@@ -720,7 +723,8 @@ val makeTempVar: fundec -> ?insert:bool -> ?name:string -> ?descr:string ->
(** Make a global variable. Your responsibility to make sure that the name
is unique. [source] defaults to [true]. [temp] defaults to [false].*)
-val makeGlobalVar: ?source:bool -> ?temp:bool -> string -> typ -> varinfo
+val makeGlobalVar: ?source:bool -> ?temp:bool -> ?referenced:bool -> string ->
+ typ -> varinfo
(** Make a shallow copy of a [varinfo] and assign a new identifier.
If the original varinfo has an associated logic var, it is copied too and
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 3e49d89eeee42a19df6936e96e16b390e18ba209..1f1726189a09cf9422cab0e6a3d1c11e3c29f5cf 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -637,7 +637,7 @@ let () =
keep_unused_specified_function). This function is meant to be passed to
{!Rmtmps.removeUnusedTemps}. *)
let keep_entry_point ?(specs=Kernel.Keep_unused_specified_functions.get ()) g =
- Rmtmps.isDefaultRoot g ||
+ Rmtmps.isExportedRoot g ||
match g with
| GFun({svar = v; sspec = spec},_)
| GFunDecl(spec,v,_) ->
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 0c95ee14a2c78bdc8ccf69d66875628a261e63c9..9c4a3b5306acdf51c56a02afc958a2132237bf28 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -82,6 +82,7 @@ let dkey_loops = register_category "natural-loops"
let dkey_parser = register_category "parser"
let dkey_rmtmps = register_category "parser:rmtmps"
+let dkey_referenced = register_category "parser:referenced"
let dkey_pp = register_category "pp"
let dkey_compilation_db = register_category "pp:compilation-db"
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 06e4720e294a3e4c737f3c4adce2f988dbe72670..c837fb5a0919eddb59eabfe811336a46ccf66629 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -109,6 +109,8 @@ val dkey_prop_status_reg: category
val dkey_rmtmps: category
+val dkey_referenced: category
+
val dkey_task: category
val dkey_typing_global: category
diff --git a/src/plugins/variadic/va_build.ml b/src/plugins/variadic/va_build.ml
index 77f3bbaf0475a97369a8dfdd005d54874ffa7cd4..a5852d4a84d93ea6f773325fb1ed5b2bfa2fccb3 100644
--- a/src/plugins/variadic/va_build.ml
+++ b/src/plugins/variadic/va_build.ml
@@ -28,7 +28,7 @@ open Cil
let function_declaration ?vattr ~loc name typ mk_spec =
(* Build the varinfo *)
- let vi = makeGlobalVar name typ in
+ let vi = makeGlobalVar ~referenced:true name typ in
Extlib.may (fun extra_vattr -> vi.vattr <- vi.vattr @ extra_vattr) vattr;
vi.vdecl <- loc;
(* Build the formals *)