diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 6cd61cd0df72fb115ee8edbb12bbbf1ab8c7bd68..84a71d10ca39d12752179023986396adb48e1d0d 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -2888,8 +2888,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
@@ -4650,6 +4650,7 @@ and makeVarInfoCabs
~(isformal: bool)
~(isglobal: bool)
?(isgenerated=false)
+ ?(referenced=false)
(ldecl : location)
(bt, sto, inline, attrs)
(n,ndt,a)
@@ -4666,7 +4667,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;
@@ -8224,11 +8226,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 c15193c0bc6ecb6c428627a689f7314d63359795..3ecc19e5a442e4ca82162a50cbe27b477aa3f44e 100644
--- a/src/kernel_internals/typing/rmtmps.ml
+++ b/src/kernel_internals/typing/rmtmps.ml
@@ -80,6 +80,12 @@ let rmUnusedStatic = ref false
let is_reachable t r = try InfoHashtbl.find t r with Not_found -> false
+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
+
(***********************************************************************
*
@@ -277,7 +283,8 @@ let isExportedRoot global =
Cil.hasAttribute "FC_BUILTIN" e.eattr ->
e.ename, true, "has FC_BUILTIN attribute"
| _ ->
- "", false, "neither function nor variable nor annotation"
+ (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;
@@ -328,14 +335,17 @@ class markReachableVisitor
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, _, _)
@@ -343,7 +353,10 @@ class markReachableVisitor
| GFunDecl (_,varinfo, _)
| GFun ({svar = varinfo}, _) ->
if not (hasAttribute "FC_BUILTIN" varinfo.vattr) then
- InfoHashtbl.replace reachable_tbl (Var varinfo) true;
+ begin
+ Kernel.debug ~dkey "marking reachable: function %s" varinfo.vname;
+ InfoHashtbl.replace reachable_tbl (Var varinfo) true;
+ end;
DoChildren
| GAnnot _ -> DoChildren
| _ ->
@@ -388,16 +401,16 @@ class markReachableVisitor
begin
let name = v.vname in
if v.vglob then
- Kernel.debug ~dkey "marking transitive use: global %s" name
+ Kernel.debug ~dkey "marking transitive use: global %s (%d)" name v.vid
else
- Kernel.debug ~dkey "marking transitive use: local %s" name;
+ 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" name;
+ Kernel.debug ~dkey "descending: global %s (%d)" name v.vid;
let descend global =
ignore (visitCilGlobal (self :> cilVisitor) global)
in
@@ -410,14 +423,14 @@ class markReachableVisitor
method private mark_enum e =
if not (is_reachable reachable_tbl (Enum e)) then
begin
- Kernel.debug ~dkey "marking transitive use: enum %s\n" e.ename;
+ 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\n" e.ename;
+ Kernel.debug ~dkey "not marking transitive use: enum %s" e.ename;
method! vexpr e =
match e.enode with
@@ -442,7 +455,7 @@ class markReachableVisitor
let old = is_reachable reachable_tbl (Comp c) in
if not old then
begin
- Kernel.debug ~dkey "marking transitive use: compound %s\n"
+ Kernel.debug ~dkey "marking transitive use: compound %s"
c.cname;
InfoHashtbl.replace reachable_tbl (Comp c) true;
@@ -457,7 +470,7 @@ class markReachableVisitor
let old = (is_reachable reachable_tbl (Type ti)) in
if not old then
begin
- Kernel.debug ~dkey "marking transitive use: typedef %s\n"
+ 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 *)
@@ -478,6 +491,38 @@ class markReachableVisitor
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
+
+ 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
@@ -522,28 +567,50 @@ let markReachable isRoot ast reachable_tbl =
*
**********************************************************************)
+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) ->
+ | GType (typeinfo, loc) ->
+ Kernel.debug ~source:(fst loc) ~dkey "referenced: type %s" typeinfo.tname;
typeinfo.treferenced <- true;
DoChildren
- | GCompTag (compinfo, _loc)
- | GCompTagDecl (compinfo, _loc) ->
+ | 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) ->
+ | 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) ->
+ | 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
@@ -553,16 +620,19 @@ class markReferencedVisitor = object
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
@@ -585,6 +655,7 @@ class markReferencedVisitor = object
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
@@ -592,7 +663,10 @@ class markReferencedVisitor = object
end
let markReferenced ast =
- visitCilFileSameGlobals (new markReferencedVisitor) ast
+ Kernel.debug ~dkey "starting markReferenced (AST has %d globals)"
+ (List.length ast.globals);
+ visitCilFileSameGlobals (new markReferencedVisitor) ast;
+ Kernel.debug ~dkey "finished markReferenced"
(**********************************************************************
*
@@ -778,7 +852,7 @@ let removeUnmarked isRoot ast reachable_tbl =
begin
(* along the way, record the interesting locals that were removed *)
let name = local.vname in
- (Kernel.debug ~dkey "removing local: %s\n" name);
+ (Kernel.debug ~dkey "removing local: %s" name);
if not (Str.string_match uninteresting name 0) then
removedLocals :=
(func.svar.vname ^ "::" ^ name) :: !removedLocals;
@@ -803,8 +877,28 @@ let removeUnmarked isRoot ast reachable_tbl =
(* all other globals are retained *)
| _ -> true
in
- let keptGlobals, _removedGlobals = List.partition filterGlobal ast.globals in
+ 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
@@ -835,6 +929,13 @@ let removeUnusedTemps ?(isRoot : rootsFilter = isExportedRoot) ast =
(* mark everything reachable from the global roots *)
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 *)
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/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 *)