From ef1d8b99c59833d1eba5c5bd33235cde9bafb1bb Mon Sep 17 00:00:00 2001
From: Pierre Nigron <pierre.nigron@cea.fr>
Date: Tue, 18 Jul 2023 13:58:59 +0200
Subject: [PATCH] WIP: [cabs2cil] Stricter checking of global initializers
---
src/kernel_internals/typing/cabs2cil.ml | 67 +++++++++++++++++++------
src/kernel_services/ast_queries/cil.ml | 62 +++++++++++++++--------
src/kernel_services/ast_queries/cil.mli | 24 ++++++---
3 files changed, 112 insertions(+), 41 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index b6422e80307..a2393c647bb 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -818,20 +818,7 @@ let get_formals vi =
let initGlobals () =
theFile := [];
theFileTypes := [];
- Cil_datatype.Varinfo.Hashtbl.clear theFileVars;
-;;
-
-let cabsPushGlobal (g: global) =
- pushGlobal g ~types:theFileTypes ~variables:theFile;
- (match g with
- | GVar (vi, _, _) | GVarDecl (vi, _)
- | GFun ({svar = vi}, _) | GFunDecl (_, vi, _) ->
- (* Do 'add' and not 'replace' here, as we may store both
- declarations and definitions for the same varinfo *)
- Cil_datatype.Varinfo.Hashtbl.add theFileVars vi g
- | _ -> ()
- );
-;;
+ Cil_datatype.Varinfo.Hashtbl.clear theFileVars
(* Keep track of some variable ids that must be turned into definitions. We
@@ -845,6 +832,8 @@ let mustTurnIntoDef: bool IH.t = IH.create 117
(* Globals that have already been defined. Indexed by the variable name. *)
let alreadyDefined: (string, location) H.t = H.create 117
+let isDefined vi = H.mem alreadyDefined vi.vorig_name
+
(* Globals that were created due to static local variables. We chose their
* names to be distinct from any global encountered at the time. But we might
* see a global with conflicting name later in the file. *)
@@ -876,6 +865,54 @@ let fileGlobals () =
revonto (revonto [] !theFile) !theFileTypes
+class checkGlobal = object
+ inherit nopCilVisitor
+
+
+ method! vglob = function
+ | GVar _ -> DoChildren
+ | _ -> SkipChildren
+
+ method! vexpr exp =
+ begin
+ match exp.enode with
+ | SizeOfE _ ->
+ (* sizeOf doesn't depend on the definitions *)
+ ()
+ | _ ->
+ let problematic_var : string option ref = ref None in
+ let is_varinfo_cst vi =
+ let res = Cil.isConstType vi.vtype && isDefined vi in
+ if not res then problematic_var := Some vi.vorig_name;
+ res
+ in
+ if not(isConstant ~is_varinfo_cst exp)
+ then
+ match !problematic_var with
+ | Some name ->
+ Kernel.error ~once:true ~current:true
+ ("%s is not a compile-time constant") name
+ | None ->
+ Kernel.error ~once:true ~current:true
+ "Initializer element is not a compile-time constant";
+ end;
+ SkipChildren
+
+end
+
+let cabsPushGlobal (g: global) =
+ ignore (visitCilGlobal (new checkGlobal) g);
+ pushGlobal g ~types:theFileTypes ~variables:theFile;
+ (match g with
+ | GVar (vi, _, _) | GVarDecl (vi, _)
+ | GFun ({svar = vi}, _) | GFunDecl (_, vi, _) ->
+ (* Do 'add' and not 'replace' here, as we may store both
+ declarations and definitions for the same varinfo *)
+ Cil_datatype.Varinfo.Hashtbl.add theFileVars vi g
+ | _ -> ()
+ )
+
+
(********* ENVIRONMENTS ***************)
(* The environment is kept in two distinct data structures. A hash table maps
@@ -8899,9 +8936,9 @@ and createGlobal ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool * C
if vi.vstorage = Extern then
vi.vstorage <- NoStorage; (* equivalent and canonical *)
- H.add alreadyDefined vi.vname (CurrentLoc.get ());
IH.remove mustTurnIntoDef vi.vid;
cabsPushGlobal (GVar(vi, {init = init}, CurrentLoc.get ()));
+ H.add alreadyDefined vi.vname (CurrentLoc.get ());
vi
end else begin
if not (isFunctionType vi.vtype) &&
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index d5a6b27c12b..c3520bf1688 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -830,6 +830,7 @@ let id = Fun.id
let alphabetabeta _ x = x
let alphabetafalse _ _ = false
let alphatrue _ = true
+let alphafalse _ = false
module Extensions = struct
let initialized = ref false
@@ -5802,32 +5803,53 @@ let isVariadicListType t = match unrollTypeSkel t with
| TBuiltin_va_list _ -> true
| _ -> false
-let rec isConstantGen f e = match e.enode with
+let rec isConstantGen lit_only is_varinfo_cst f e = match e.enode with
| Const c -> f c
- | UnOp (_, e, _) -> isConstantGen f e
- | BinOp (_, e1, e2, _) -> isConstantGen f e1 && isConstantGen f e2
- | Lval (Var vi, NoOffset) ->
- (vi.vglob && isArrayType vi.vtype || isFunctionType vi.vtype)
+ | UnOp (_, e, _) -> isConstantGen lit_only is_varinfo_cst f e
+ | BinOp (_, e1, e2, _) ->
+ isConstantGen lit_only is_varinfo_cst f e1 &&
+ isConstantGen lit_only is_varinfo_cst f e2
+ | Lval (Var vi, _) ->
+ is_varinfo_cst vi ||
+ (vi.vglob && isArrayType vi.vtype) ||
+ isFunctionType vi.vtype
| Lval _ -> false
| SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ -> true
(* see ISO 6.6.6 *)
| CastE(t,{ enode = Const(CReal _)}) when isIntegralType t -> true
- | CastE (_, e) -> isConstantGen f e
- | AddrOf (Var vi, off) | StartOf (Var vi, off)
- -> vi.vglob && isConstantOffsetGen f off
- | AddrOf (Mem e, off) | StartOf(Mem e, off)
- -> isConstantGen f e && isConstantOffsetGen f off
-
-and isConstantOffsetGen f = function
+ | CastE(t, e) ->
+ begin
+ match t, typeOf e with
+ | TInt (i, _), TPtr _ ->
+ (* gcc/clang/ccomp consider a non-truncated pointer to be a constant.
+ If it is truncated, we check whether we already know its value. *)
+ bytesSizeOfInt theMachine.upointKind <= bytesSizeOfInt i ||
+ isConstantGen true is_varinfo_cst f e
+ | _ -> isConstantGen lit_only is_varinfo_cst f e
+ end
+ | AddrOf (Var vi, off) | StartOf (Var vi, off) ->
+ not lit_only &&
+ vi.vglob &&
+ isConstantOffsetGen lit_only is_varinfo_cst f off
+ | AddrOf (Mem e, off) | StartOf(Mem e, off) ->
+ isConstantGen lit_only is_varinfo_cst f e &&
+ isConstantOffsetGen lit_only is_varinfo_cst f off
+
+and isConstantOffsetGen lit_only is_varinfo_cst f = function
NoOffset -> true
- | Field(_fi, off) -> isConstantOffsetGen f off
- | Index(e, off) -> isConstantGen f e && isConstantOffsetGen f off
-
-let isConstant e = isConstantGen alphatrue e
-let isConstantOffset o = isConstantOffsetGen alphatrue o
-
-let isIntegerConstant e =
- isConstantGen
+ | Field(_fi, off) -> isConstantOffsetGen lit_only is_varinfo_cst f off
+ | Index(e, off) ->
+ isConstantGen lit_only is_varinfo_cst f e &&
+ isConstantOffsetGen lit_only is_varinfo_cst f off
+
+let isConstant ?(is_varinfo_cst = alphafalse) e =
+ isConstantGen false is_varinfo_cst alphatrue e
+let isConstantOffset ?(is_varinfo_cst = alphafalse) o =
+ isConstantOffsetGen false is_varinfo_cst alphatrue o
+
+let isIntegerConstant ?(is_varinfo_cst = alphafalse) e =
+ isConstantGen false
+ is_varinfo_cst
(function
| CInt64 _ | CChr _ | CEnum _ -> true
| CStr _ | CWStr _ | CReal _ -> false)
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 8b63fb51b24..92213780da7 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -841,14 +841,26 @@ val kfloat: loc:location -> fkind -> float -> exp
character or an integer constant *)
val isInteger: exp -> Integer.t option
-(** True if the expression is a compile-time constant *)
-val isConstant: exp -> bool
+(** True if the expression is a compile-time constant.
+ [is_varinfo_cst] indicates whether a variable should
+ be considered as having a constant content. Defaults to
+ [false].
-(** True if the expression is a compile-time integer constant *)
-val isIntegerConstant: exp -> bool
+ @before Frama-C+dev [is_varinfo_cst] does not exist
+*)
+val isConstant: ?is_varinfo_cst:(varinfo -> bool) -> exp -> bool
+
+(** True if the expression is a compile-time integer constant
+
+ @before Frama-C+dev [is_varinfo_cst] does not exist
+*)
+val isIntegerConstant: ?is_varinfo_cst:(varinfo -> bool) -> exp -> bool
+
+(** True if the given offset contains only field names or constant indices.
-(** True if the given offset contains only field names or constant indices. *)
-val isConstantOffset: offset -> bool
+ @before Frama-C+dev [is_varinfo_cst] does not exist
+*)
+val isConstantOffset: ?is_varinfo_cst:(varinfo -> bool) -> offset -> bool
(** True if the given expression is a (possibly cast'ed) integer or character
constant with value zero *)
--
GitLab