From 6e3b3ad4a68ce17ebad4d86f471ff47d022b7ec9 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 21 Apr 2021 16:01:20 +0200
Subject: [PATCH] [wp] Move always_initialized in Cvalues
---
src/plugins/wp/Cvalues.ml | 3 +++
src/plugins/wp/Cvalues.mli | 1 +
src/plugins/wp/MemTyped.ml | 3 +--
src/plugins/wp/MemVar.ml | 18 +++++++++---------
4 files changed, 14 insertions(+), 11 deletions(-)
diff --git a/src/plugins/wp/Cvalues.ml b/src/plugins/wp/Cvalues.ml
index 5c8b21c9784..d26aee33e7d 100644
--- a/src/plugins/wp/Cvalues.ml
+++ b/src/plugins/wp/Cvalues.ml
@@ -133,6 +133,9 @@ and init_comp_value value ci =
let initialized_obj = init_value e_true
let uninitialized_obj = init_value e_false
+let always_initialized x =
+ (x.vformal || x.vglob) && not @@ Cil.isStructOrUnionType x.vtype
+
(* -------------------------------------------------------------------------- *)
(* --- Length of empty compinfos --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Cvalues.mli b/src/plugins/wp/Cvalues.mli
index 01fd0ed8bdf..c9d70fa788f 100644
--- a/src/plugins/wp/Cvalues.mli
+++ b/src/plugins/wp/Cvalues.mli
@@ -99,6 +99,7 @@ val logic_constant : logic_constant -> term
val constant_exp : exp -> term
val constant_term : Cil_types.term -> term
+val always_initialized: varinfo -> bool
val initialized_obj: c_object -> term
val uninitialized_obj: c_object -> term
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 802617a661a..abf67a6cb7c 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -579,8 +579,7 @@ module BASE = WpContext.Generator(Varinfo)
let initialization prefix x base =
match sizeof x with
- | Some size
- when (x.vformal || x.vglob) && not(Cil.isStructOrUnionType x.vtype) ->
+ | Some size when Cvalues.always_initialized x ->
let a = Lang.freshvar ~basename:"init" t_init in
let m = e_var a in
let init_access =
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index c2897b53872..f52667de01c 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -738,9 +738,6 @@ struct
(* --- Memory Load --- *)
(* -------------------------------------------------------------------------- *)
- let always_init vi =
- (vi.vglob || vi.vformal) && not @@ Cil.isStructOrUnionType vi.vtype
-
let rec access_gen kind a = function
| [] -> a
| Field f :: ofs -> access_gen kind (e_getfield a (Cfield (f, kind))) ofs
@@ -786,7 +783,7 @@ struct
let load_init sigma obj = function
| Ref _ ->
e_true
- | Val((CREF|CVAL),x,_) when always_init x ->
+ | Val((CREF|CVAL),x,_) when Cvalues.always_initialized x ->
Cvalues.initialized_obj obj
| Val((CREF|CVAL),x,ofs) ->
access_init (get_init_term sigma x) ofs
@@ -1148,7 +1145,7 @@ struct
| Val(m,x,p) ->
if is_heap_allocated m then
M.initialized sigma.mem (Rloc(obj,mloc_of_loc l))
- else if always_init x then
+ else if Cvalues.always_initialized x then
try valid_offset RW (vobject m x) p
with ShiftMismatch -> shift_mismatch l
else
@@ -1174,7 +1171,7 @@ struct
let p, a, b = normalize elt p in
let in_array = valid_range RW (vobject m x) p (elt, a, b) in
let initialized =
- if always_init x then p_true
+ if Cvalues.always_initialized x then p_true
else initialized_range sigma (vobject m x) x p a b
in
F.p_imply (F.p_leq a b) (p_and in_array initialized)
@@ -1263,7 +1260,8 @@ struct
| Leave -> []
| Enter ->
let init_status v =
- if v.vdefined || always_init v || not @@ is_mvar_alloc v then None
+ if v.vdefined || Cvalues.always_initialized v || not@@ is_mvar_alloc v
+ then None
else
let i = Cvalues.uninitialized_obj (Ctypes.object_of v.vtype) in
Some (Lang.F.p_equal (access_init (get_init_term seq.post v) []) i)
@@ -1377,7 +1375,7 @@ struct
(* -------------------------------------------------------------------------- *)
let rec monotonic_initialized seq obj x ofs =
- if always_init x then p_true
+ if Cvalues.always_initialized x then p_true
else
match obj with
(* Structure initialization is not monotonic *)
@@ -1611,7 +1609,9 @@ struct
let domain obj l =
match l with
| Ref x | Val((CVAL|CREF),x,_) ->
- let init = if not @@ always_init x then [ Init x ] else [] in
+ let init =
+ if not @@ Cvalues.always_initialized x then [ Init x ] else []
+ in
Heap.Set.of_list ((Var x) :: init)
| Loc _ | Val((CTXT _|CARR _|HEAP),_,_) ->
M.Heap.Set.fold
--
GitLab