From 6608ae46bd12189b229345b776cce657a625afd5 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 28 May 2020 14:19:14 +0200
Subject: [PATCH] [wp] Deals with globals in MemTyped
---
src/plugins/wp/MemLoader.ml | 31 ++++++++++--
src/plugins/wp/MemLoader.mli | 1 +
src/plugins/wp/MemMemory.ml | 7 ++-
src/plugins/wp/MemMemory.mli | 3 ++
src/plugins/wp/MemRegion.ml | 1 +
src/plugins/wp/MemTyped.ml | 50 +++++++++++++++----
src/plugins/wp/MemVar.ml | 1 +
.../wp/share/why3/frama_c_wp/memory.mlw | 11 +++-
8 files changed, 87 insertions(+), 18 deletions(-)
diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index 5e4fd439273..801cb06218e 100644
--- a/src/plugins/wp/MemLoader.ml
+++ b/src/plugins/wp/MemLoader.ml
@@ -80,6 +80,7 @@ sig
val store_pointer : Sigma.t -> typ -> loc -> term -> Chunk.t * term
val is_init_atom : Sigma.t -> loc -> term
+ val is_init_range : Sigma.t -> c_object -> loc -> term -> pred
val set_init_atom : Sigma.t -> loc -> term -> Chunk.t * term
val set_init : c_object -> loc -> length:term ->
Chunk.t -> current:term -> term
@@ -317,6 +318,19 @@ struct
let isinitrec = ref (fun _ _ _ -> assert false)
+ let initialization_lemma cluster name (sigma, obj, loc) (lfun, params) =
+ let high = p_call lfun (List.map F.e_var params) in
+ let low = M.is_init_range sigma obj loc e_one in
+ let lemma = p_equiv high low in
+ {
+ l_assumed = true ;
+ l_name = name ^ "_low" ; l_types = 0 ;
+ l_forall = F.p_vars lemma ;
+ l_triggers = [] ;
+ l_lemma = lemma ;
+ l_cluster = cluster ;
+ }
+
module IS_INIT_COMP = WpContext.Generator(COMP_KEY)
(struct
let name = M.name ^ ".IS_INIT_COMP"
@@ -329,6 +343,8 @@ struct
let obj = C_comp c in
let loc = M.of_region_pointer r obj v in (* t_pointer -> loc *)
let domain = M.init_footprint obj loc in
+ let cluster = cluster () in
+ (* Function Is_init *)
let name =
Format.asprintf "Is%s%a" (Lang.comp_init_id c) pp_rid r
in
@@ -342,8 +358,11 @@ struct
d_lfun = lfun ; d_types = 0 ;
d_params = x :: xms ;
d_definition = Predicate(Def , def) ;
- d_cluster = cluster () ;
+ d_cluster = cluster ;
} ;
+ (* Lemma for low-level view of the memory *)
+ Definitions.define_lemma
+ (initialization_lemma cluster name (sigma,obj,loc) (lfun,x::xms)) ;
lfun , chunks
let compile = Lang.local generate
@@ -371,12 +390,18 @@ struct
let ofs = e_sum denv.index_offset in
let vm = !isinitrec sigma obj_e (M.shift loc obj_e ofs) in
let def = p_forall denv.index_var (p_hyps denv.index_range vm) in
+ let cluster = cluster () in
Definitions.define_symbol {
d_lfun = lfun ; d_types = 0 ;
d_params = x :: denv.size_var @ xmem ;
d_definition = Predicate (Def, def) ;
- d_cluster = cluster () ;
+ d_cluster = cluster ;
} ;
+ (* Lemma for low-level view of the memory *)
+ Definitions.define_lemma
+ (initialization_lemma cluster name
+ (sigma, obj_a, loc)
+ (lfun, x :: denv.size_var @ xmem)) ;
lfun , chunks
let compile = Lang.local generate
@@ -471,7 +496,7 @@ struct
let stored seq obj loc value =
match obj with
| C_int _ | C_float _ | C_pointer _ ->
- updated_atom seq obj loc value :: [ updated_init_atom seq loc e_true ]
+ [ updated_atom seq obj loc value ; updated_init_atom seq loc e_true ]
| C_comp _ | C_array _ ->
let set_value = Set(loadvalue seq.post obj loc, value) in
set_value :: havoc seq obj loc @ set_init seq obj loc
diff --git a/src/plugins/wp/MemLoader.mli b/src/plugins/wp/MemLoader.mli
index 2cd1ed7a5db..177e2ce96b5 100644
--- a/src/plugins/wp/MemLoader.mli
+++ b/src/plugins/wp/MemLoader.mli
@@ -76,6 +76,7 @@ sig
val store_pointer : Sigma.t -> typ -> loc -> term -> Chunk.t * term
val is_init_atom : Sigma.t -> loc -> term
+ val is_init_range : Sigma.t -> c_object -> loc -> term -> pred
val set_init_atom : Sigma.t -> loc -> term -> Chunk.t * term
val set_init : c_object -> loc -> length:term ->
Chunk.t -> current:term -> term
diff --git a/src/plugins/wp/MemMemory.ml b/src/plugins/wp/MemMemory.ml
index 56849a666de..b7d7f2ba856 100644
--- a/src/plugins/wp/MemMemory.ml
+++ b/src/plugins/wp/MemMemory.ml
@@ -74,8 +74,6 @@ let p_separated = Lang.extern_fp ~library "separated"
let p_included = Lang.extern_fp ~library "included"
let p_eqmem = Lang.extern_fp ~library "eqmem"
let f_havoc = Lang.extern_f ~library ~typecheck:ty_fst_arg ~link:l_havoc "havoc"
-let f_set_init =
- Lang.extern_f ~library ~typecheck:ty_fst_arg ~link:l_set_init "set_init"
let p_monotonic = Lang.extern_fp ~library "monotonic_init"
let f_region = Lang.extern_f ~library ~result:L.Int "region" (* base -> region *)
let p_framed = Lang.extern_fp ~library "framed" (* m-pointer -> prop *)
@@ -83,6 +81,10 @@ let p_linked = Lang.extern_fp ~library "linked" (* allocation-table -> prop *)
let p_sconst = Lang.extern_fp ~library "sconst" (* int-memory -> prop *)
let p_addr_lt = Lang.extern_p ~library ~bool:"addr_lt_bool" ~prop:"addr_lt" ()
let p_addr_le = Lang.extern_p ~library ~bool:"addr_le_bool" ~prop:"addr_le" ()
+let f_set_init =
+ Lang.extern_f ~library ~typecheck:ty_fst_arg ~link:l_set_init "set_init"
+let p_cinits = Lang.extern_fp ~library "cinits" (* initializaton-table -> prop *)
+let p_is_init_r = Lang.extern_fp ~library "is_init_range"
let f_addr_of_int = Lang.extern_f
~category:L.Injection
@@ -98,6 +100,7 @@ let f_int_of_addr = Lang.extern_f
let t_mem t = L.Array(t_addr,t)
let t_malloc = L.Array(L.Int,L.Int)
+let t_init = L.Array(t_addr,L.Bool)
let a_null = F.constant (e_fun f_null [])
let a_base p = e_fun f_base [p]
diff --git a/src/plugins/wp/MemMemory.mli b/src/plugins/wp/MemMemory.mli
index bc7ccb47ffa..bd50be0f171 100644
--- a/src/plugins/wp/MemMemory.mli
+++ b/src/plugins/wp/MemMemory.mli
@@ -31,6 +31,7 @@ open Lang.F
val t_addr : tau
val t_malloc : tau (** allocation tables *)
+val t_init : tau (** initialization tables *)
val t_mem : tau -> tau (** t_addr indexed array *)
val a_null : term (** Null address. Same as [a_addr 0 0] *)
@@ -59,6 +60,8 @@ val p_addr_le : lfun
val p_linked : lfun
val p_framed : lfun
val p_sconst : lfun
+val p_cinits : lfun
+val p_is_init_r : lfun
val p_separated : lfun
val p_included : lfun
val p_valid_rd : lfun
diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml
index 1ed00876a4d..427bd92700c 100644
--- a/src/plugins/wp/MemRegion.ml
+++ b/src/plugins/wp/MemRegion.ml
@@ -819,6 +819,7 @@ struct
let _ = current in
assert false
let is_init_atom _ _ = assert false
+ let is_init_range _ _ _ _ = assert false
let monotonic_init _ _ = assert false
end
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 441376e8f85..f09f8b9249f 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -172,8 +172,8 @@ struct
| M_pointer -> L.Array(t_addr,t_addr)
| M_f32 -> L.Array(t_addr,Cfloat.tau_of_float Ctypes.Float32)
| M_f64 -> L.Array(t_addr,Cfloat.tau_of_float Ctypes.Float64)
- | T_alloc -> L.Array(L.Int,L.Int)
- | T_init -> L.Array(t_addr,L.Bool)
+ | T_alloc -> t_malloc
+ | T_init -> t_init
let basename_of_chunk = name
let is_framed _ = false
end
@@ -529,6 +529,28 @@ module BASE = WpContext.Generator(Varinfo)
l_cluster = cluster_globals () ;
}
+ let initialization prefix x base =
+ match sizeof x with
+ | Some size when x.vformal || x.vglob ->
+ let a = Lang.freshvar ~basename:"init" t_init in
+ let m = e_var a in
+ let init_access =
+ if size = 1 then
+ p_bool (F.e_get m (a_addr base e_zero))
+ else
+ F.p_call p_is_init_r [ m ; a_addr base e_zero ; e_int size ]
+ in
+ let m_init = p_call p_cinits [m] in
+ let init_prop = p_forall [a] (p_imply m_init init_access) in
+ Definitions.define_lemma {
+ l_assumed = true ;
+ l_name = prefix ^ "_init" ; l_types = 0 ;
+ l_triggers = [] ; l_forall = [] ;
+ l_lemma = init_prop ;
+ l_cluster = cluster_globals () ;
+ }
+ | _ -> ()
+
let generate x =
let acs_rd = Cil.typeHasQualifier "const" x.vtype in
let prefix =
@@ -550,6 +572,7 @@ module BASE = WpContext.Generator(Varinfo)
RegisterBASE.define lfun x ;
region prefix x base ;
linked prefix x base ;
+ initialization prefix x base ;
base
let compile = Lang.local generate
@@ -967,15 +990,6 @@ struct
F.e_fun f_havoc [fresh;current;loc;n]
else fresh
- let set_init obj loc ~length _chunk ~current =
- let n = F.e_fact (length_of_object obj) length in
- F.e_fun f_set_init [current;loc;n]
-
- let monotonic_init s1 s2 =
- let m1 = Sigma.value s1 T_init in
- let m2 = Sigma.value s2 T_init in
- F.p_call p_monotonic [m1; m2]
-
let eqmem obj loc _chunk m1 m2 =
F.p_call p_eqmem [m1;m2;loc;e_int (length_of_object obj)]
@@ -996,6 +1010,19 @@ struct
let set_init_atom sigma l v = updated sigma T_init l v
let is_init_atom sigma l = F.e_get (Sigma.value sigma T_init) l
+ let is_init_range sigma obj loc length =
+ let n = F.e_fact (length_of_object obj) length in
+ F.p_call p_is_init_r [ Sigma.value sigma T_init ; loc ; n ]
+
+ let set_init obj loc ~length _chunk ~current =
+ let n = F.e_fact (length_of_object obj) length in
+ F.e_fun f_set_init [current;loc;n]
+
+ let monotonic_init s1 s2 =
+ let m1 = Sigma.value s1 T_init in
+ let m2 = Sigma.value s2 T_init in
+ F.p_call p_monotonic [m1; m2]
+
end
module LOADER = MemLoader.Make(MODEL)
@@ -1063,6 +1090,7 @@ let frame sigma =
else []
in
wellformed_frame p_linked T_alloc @
+ wellformed_frame p_cinits T_init @
wellformed_frame p_sconst M_char @
wellformed_frame p_framed M_pointer
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index 25755526f67..32e840f7893 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -371,6 +371,7 @@ struct
let get_init s x = INIT.get s.init x
let get_init_term s x = e_var (get_init s x)
+
(* -------------------------------------------------------------------------- *)
(* --- State Pretty Printer --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/share/why3/frama_c_wp/memory.mlw b/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
index 0c1a3429cd0..a8b720a310a 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
@@ -69,8 +69,6 @@ theory Memory
function havoc (m0 m1 : map addr 'a) (p:addr) (a:int) : map addr 'a
- function set_init (m: map addr bool) (p:addr) (a:int) : map addr bool
-
predicate monotonic_init(m1 m2 : map addr bool) =
forall p: addr. m1[p] -> m2[p]
@@ -164,6 +162,15 @@ theory Memory
(Map.([]) (havoc m0 m1 p a) (q)) =
(if (separated q 1 p a) then (Map.([]) (m1) (q)) else (Map.([]) (m0) (q)))
+ (* Initialization memory *)
+
+ predicate cinits (map addr bool)
+
+ predicate is_init_range(m: map addr bool) (p: addr) (l: int) =
+ forall i : int. 0 <= i < l -> m[shift p i] = true
+
+ function set_init (m: map addr bool) (p:addr) (a:int) : map addr bool
+
lemma set_init_access :
forall m : map addr bool.
forall q p : addr.
--
GitLab