From a14c61e8f2f41c74df1e2c8666119e60a8188cc9 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 5 Jan 2021 10:01:51 +0100
Subject: [PATCH] [kernel] Robustify some fields treatments
---
src/kernel_internals/typing/cabs2cil.ml | 13 ++--
src/kernel_internals/typing/mergecil.ml | 82 ++++++++++---------------
2 files changed, 39 insertions(+), 56 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index b91f906f540..711d6633ecf 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -3744,7 +3744,7 @@ let find_field_offset cond (fidlist: fieldinfo list) : offset =
| fid :: rest when prefix anonCompFieldName fid.fname -> begin
match unrollType fid.ftype with
| TComp (ci, _, _) ->
- (try let off = search (Extlib.the ci.cfields) in Field(fid,off)
+ (try let off = search (Extlib.opt_conv [] ci.cfields) in Field(fid,off)
with Not_found -> search rest (* Continue searching *))
| _ ->
abort_context "unnamed field type is not a struct/union"
@@ -3755,7 +3755,7 @@ let find_field_offset cond (fidlist: fieldinfo list) : offset =
let findField n comp =
try
- find_field_offset (fun x -> x.fname = n) (Extlib.the comp.cfields)
+ find_field_offset (fun x -> x.fname = n) (Extlib.opt_conv [] comp.cfields)
with Not_found ->
abort_context "Cannot find field %s in type %s" n (Cil.compFullName comp)
@@ -5549,16 +5549,17 @@ and makeCompType ghost (isstruct: bool)
"Empty %s is allowed only in GCC or MSVC mode"
(if comp.cstruct then "struct" else "union");
List.iter check flds;
- if comp.cfields <> Some [] && comp.cfields <> None then begin
+ if comp.cfields <> None then begin
+ let old_fields = Extlib.the comp.cfields in
(* This appears to be a multiply defined structure. This can happen from
* a construct like "typedef struct foo { ... } A, B;". This is dangerous
* because at the time B is processed some forward references in { ... }
* appear as backward references, which could lead to circularity in
* the type structure. We do a thorough check and then we reuse the type
* for A *)
- if List.length (Extlib.opt_conv [] comp.cfields) <> List.length flds
+ if List.length old_fields <> List.length flds
|| (List.exists2 (fun f1 f2 -> not (Cil_datatype.Typ.equal f1.ftype f2.ftype))
- (Extlib.opt_conv [] comp.cfields) flds)
+ old_fields flds)
then
Kernel.error ~once:true ~current:true
"%s seems to be multiply defined" (compFullName comp)
@@ -8327,7 +8328,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
[(A.NEXT_INIT, A.SINGLE_INIT oneinit)]
else
(* If this is a GNU extension with field-to-union cast find the field *)
- let fi = findField (Extlib.the ci.cfields) in
+ let fi = findField (Extlib.opt_conv [] ci.cfields) in
(* Change the designator and redo *)
doInit
local_env asconst add_implicit_ensures preinit so acc
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index 2dc0f65e999..ead5136f1f6 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -2164,64 +2164,46 @@ class renameVisitorClass =
})
| _ -> DoChildren
+ method private update_field f =
+ (* See if the compinfo was changed *)
+ if f.fcomp.creferenced then None
+ else begin
+ match
+ PlainMerging.findReplacement true sEq !currentFidx f.fcomp.cname
+ with
+ None -> None (* We did not replace it *)
+ | Some (ci', _oldfidx) -> begin
+ (* First, find out the index of the original field *)
+ let rec indexOf (i: int) = function
+ | [] -> Kernel.fatal "Cannot find field %s in %s"
+ f.fname (compFullName f.fcomp)
+ | f' :: _ when f' == f -> i
+ | _ :: rest -> indexOf (i + 1) rest
+ in
+ let index = indexOf 0 (Extlib.opt_conv [] f.fcomp.cfields) in
+ let ci'_fields = Extlib.opt_conv [] ci'.cfields in
+ if List.length ci'_fields <= index then
+ Kernel.fatal "Too few fields in replacement %s for %s"
+ (compFullName ci')
+ (compFullName f.fcomp);
+ Some (List.nth ci'_fields index)
+ end
+ end
+
(* The Field offset might need to be changed to use new compinfo *)
method! voffs = function
Field (f, o) -> begin
- (* See if the compinfo was changed *)
- if f.fcomp.creferenced then
- DoChildren
- else begin
- match
- PlainMerging.findReplacement true sEq !currentFidx f.fcomp.cname
- with
- None -> DoChildren (* We did not replace it *)
- | Some (ci', _oldfidx) -> begin
- (* First, find out the index of the original field *)
- let rec indexOf (i: int) = function
- [] -> Kernel.fatal "Cannot find field %s in %s"
- f.fname (compFullName f.fcomp)
- | f' :: _ when f' == f -> i
- | _ :: rest -> indexOf (i + 1) rest
- in
- let index = indexOf 0 (Extlib.the f.fcomp.cfields) in
- if List.length (Extlib.the ci'.cfields) <= index then
- Kernel.fatal "Too few fields in replacement %s for %s"
- (compFullName ci')
- (compFullName f.fcomp);
- let f' = List.nth (Extlib.the ci'.cfields) index in
- ChangeDoChildrenPost (Field (f', o), fun x -> x)
- end
- end
+ match self#update_field f with
+ | None -> DoChildren
+ | Some f' -> ChangeDoChildrenPost (Field (f', o), fun x -> x)
end
| _ -> DoChildren
method! vterm_offset = function
TField (f, o) -> begin
- (* See if the compinfo was changed *)
- if f.fcomp.creferenced then
- DoChildren
- else begin
- match
- PlainMerging.findReplacement true sEq !currentFidx f.fcomp.cname
- with
- None -> DoChildren (* We did not replace it *)
- | Some (ci', _oldfidx) -> begin
- (* First, find out the index of the original field *)
- let rec indexOf (i: int) = function
- [] -> Kernel.fatal "Cannot find field %s in %s"
- f.fname (compFullName f.fcomp)
- | f' :: _ when f' == f -> i
- | _ :: rest -> indexOf (i + 1) rest
- in
- let index = indexOf 0 (Extlib.the f.fcomp.cfields) in
- if List.length (Extlib.the ci'.cfields) <= index then
- Kernel.fatal "Too few fields in replacement %s for %s"
- (compFullName ci')
- (compFullName f.fcomp);
- let f' = List.nth (Extlib.the ci'.cfields) index in
- ChangeDoChildrenPost (TField (f', o), fun x -> x)
- end
- end
+ match self#update_field f with
+ | None -> DoChildren
+ | Some f' -> ChangeDoChildrenPost (TField (f', o), fun x -> x)
end
| TModel(f,o) ->
(match
--
GitLab