From 0f0423e1881f6f807b95e152f6598f5053e2bc22 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 26 May 2020 09:44:24 +0200
Subject: [PATCH] [wp] Adds type constraints on memory chunks when RTE is on
---
src/plugins/wp/LogicCompiler.ml | 9 ++-
src/plugins/wp/MemEmpty.ml | 1 +
src/plugins/wp/MemRegion.ml | 2 +
src/plugins/wp/MemTyped.ml | 71 ++++++++++++++++---
src/plugins/wp/MemVar.ml | 3 +
src/plugins/wp/MemZeroAlias.ml | 2 +
src/plugins/wp/Sigs.ml | 4 ++
src/plugins/wp/cfgWP.ml | 10 ++-
.../wp/tests/wp_acsl/oracle/logic.res.oracle | 61 +++-------------
9 files changed, 96 insertions(+), 67 deletions(-)
diff --git a/src/plugins/wp/LogicCompiler.ml b/src/plugins/wp/LogicCompiler.ml
index 6a09fa82d14..8c88a3af10b 100644
--- a/src/plugins/wp/LogicCompiler.ml
+++ b/src/plugins/wp/LogicCompiler.ml
@@ -317,7 +317,13 @@ struct
let f = Context.get cframe in
f.triggers <- tg :: f.triggers
- let guards f = Lang.hypotheses f.gamma
+ let make_chunk_constraints f =
+ if not (Wp_parameters.RTE.get()) then []
+ else LabelMap.fold (fun _ s l -> M.is_well_formed s :: l) f.labels []
+
+ let guards f =
+ let constraints = in_frame f (fun () -> make_chunk_constraints f) () in
+ Lang.hypotheses f.gamma @ constraints
(* -------------------------------------------------------------------------- *)
(* --- Environments --- *)
@@ -438,6 +444,7 @@ struct
let used = List.filter used_var sigv in
let parp = List.map snd used in
let sigp = List.map (fun (lv,_) -> Sig_value lv) used in
+ let domain = make_chunk_constraints frame @ domain in
let (parm,sigm) =
LabelMap.fold
(fun label sigma acc ->
diff --git a/src/plugins/wp/MemEmpty.ml b/src/plugins/wp/MemEmpty.ml
index fc58ebd54ac..f10f6da7cef 100644
--- a/src/plugins/wp/MemEmpty.ml
+++ b/src/plugins/wp/MemEmpty.ml
@@ -94,6 +94,7 @@ let loc_of_int _ _ = ()
let int_of_loc _ () = e_zero
let domain _obj _l = Sigma.Chunk.Set.empty
+let is_well_formed _s = p_true
let source = "Empty Model"
diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml
index 18a27402314..b717626bea9 100644
--- a/src/plugins/wp/MemRegion.ml
+++ b/src/plugins/wp/MemRegion.ml
@@ -700,6 +700,8 @@ let domain _obj = function
| Lfld(_,_,_,ovl) -> Heap.of_overlay (map()) ovl
| Larr(r,_,_,_,_,_) -> Heap.of_region (map()) r
+let is_well_formed _s = Lang.F.p_true
+
let region_of_loc = function
| (GarbledMix | Index _) as l -> error "Can not find region of %a" pretty l
| Lref(r,_,_) | Lraw(r,_,_,_) | Lmem(r,_,_,_)
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index e1317a92d94..fa4cb6ad40a 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -117,7 +117,7 @@ let pointer = Context.create "MemTyped.pointer"
(* -------------------------------------------------------------------------- *)
type chunk =
- | M_int
+ | M_int of Ctypes.c_int
| M_char
| M_f32
| M_f64
@@ -128,16 +128,20 @@ module Chunk =
struct
type t = chunk
let self = "typed"
+ let int_rank = function
+ | CBool -> 0
+ | k -> Ctypes.i_bytes k * (if Ctypes.signed k then 2 else 1)
+
let rank = function
- | M_int -> 0
- | M_char -> 1
- | M_f32 -> 2
- | M_f64 -> 3
- | M_pointer -> 4
- | T_alloc -> 5
+ | M_char -> -1
+ | M_int i -> int_rank i
+ | M_f32 -> 17
+ | M_f64 -> 18
+ | M_pointer -> 19
+ | T_alloc -> 20
let hash = rank
let name = function
- | M_int -> "Mint"
+ | M_int _ -> "Mint"
| M_char -> "Mchar"
| M_f32 -> "Mf32"
| M_f64 -> "Mf64"
@@ -147,13 +151,13 @@ struct
let equal = (=)
let pretty fmt c = Format.pp_print_string fmt (name c)
let val_of_chunk = function
- | M_int | M_char -> L.Int
+ | M_int _ | M_char -> L.Int
| M_f32 -> Cfloat.tau_of_float Ctypes.Float32
| M_f64 -> Cfloat.tau_of_float Ctypes.Float64
| M_pointer -> t_addr
| T_alloc -> L.Int
let tau_of_chunk = function
- | M_int | M_char -> L.Array(t_addr,L.Int)
+ | M_int _ | M_char -> L.Array(t_addr,L.Int)
| 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)
@@ -171,7 +175,7 @@ type loc = term (* of type addr *)
(* --- Utilities on locations --- *)
(* -------------------------------------------------------------------------- *)
-let m_int i = if Ctypes.is_char i then M_char else M_int
+let m_int i = if Ctypes.is_char i then M_char else M_int i
let m_float = function Float32 -> M_f32 | Float64 -> M_f64
let rec footprint = function
@@ -871,6 +875,51 @@ let frames obj addr = function
let basename = Chunk.basename_of_chunk m in
MemMemory.frames ~addr ~offset ~sizeof ~basename tau
+(* -------------------------------------------------------------------------- *)
+(* --- Chunk element type --- *)
+(* -------------------------------------------------------------------------- *)
+
+module ChunkContent = WpContext.Generator(Chunk)
+ (struct
+ let name = "MemTyped.ChunkContent"
+ type key = Chunk.t
+ type data = lfun
+
+ let int_kind = function
+ | M_char -> Ctypes.c_char ()
+ | M_int k -> k
+ | _ -> failwith "MemTyped asked constraint for non int type"
+
+ let generate c =
+ let k = int_kind c in
+ let p = Lang.freshvar ~basename:"m" (Chunk.tau_of_chunk c) in
+ let m = e_var p in
+ let name = Format.asprintf "is_%a_chunk" Ctypes.pp_int k in
+ let lfun = Lang.generated_p name in
+ let l = Lang.freshvar ~basename:"l" (Lang.t_addr()) in
+ let is_int = Cint.range k in
+ let def = p_forall [l] (is_int (F.e_get m (e_var l))) in
+ Definitions.define_symbol {
+ d_lfun = lfun ; d_types = 0 ;
+ d_params = [p] ;
+ d_definition = Predicate(Def, def) ;
+ d_cluster = cluster ~id:"Chunk" ~title:"Chunk type constraint" () ;
+ } ;
+ lfun
+
+ let compile = Lang.local generate
+ end)
+
+let is_chunk sigma = function
+ | M_int _ | M_char as m ->
+ F.p_call (ChunkContent.get m) [ Sigma.value sigma m ]
+ | _ ->
+ p_true
+
+let is_well_formed sigma =
+ let open Sigma in
+ p_conj (Chunk.Set.fold (fun c l -> is_chunk sigma c :: l) (domain sigma) [])
+
(* -------------------------------------------------------------------------- *)
(* --- Loader --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index fd09f824c2c..e07a9ad259a 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -1267,6 +1267,9 @@ struct
(fun m s -> Heap.Set.add (Mem m) s)
(M.domain obj (mloc_of_loc l)) Heap.Set.empty
+ let is_well_formed sigma =
+ M.is_well_formed sigma.mem
+
(* -------------------------------------------------------------------------- *)
end
diff --git a/src/plugins/wp/MemZeroAlias.ml b/src/plugins/wp/MemZeroAlias.ml
index 19f271238f1..c734daed7a6 100644
--- a/src/plugins/wp/MemZeroAlias.ml
+++ b/src/plugins/wp/MemZeroAlias.ml
@@ -183,6 +183,8 @@ let domain _obj l =
try Heap.Set.singleton (fst (access l))
with _ -> Heap.Set.empty
+let is_well_formed _s = p_true
+
let value sigma l =
let m,ks = access l in
let x = Sigma.get sigma m in
diff --git a/src/plugins/wp/Sigs.ml b/src/plugins/wp/Sigs.ml
index 72d1972ac59..6f8f2636cae 100644
--- a/src/plugins/wp/Sigs.ml
+++ b/src/plugins/wp/Sigs.ml
@@ -412,6 +412,10 @@ sig
the given C-type. It is safe to retun an over-approximation of the
chunks involved. *)
+ val is_well_formed : sigma -> pred
+ (** Provides the constraint corresponding to the kind of data stored by all
+ chunks in sigma. *)
+
val load : sigma -> c_object -> loc -> loc value
(** Return the value of the object of the given type at the given location in
the given memory state. *)
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index 6108632979a..b8389519cc2 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -207,11 +207,15 @@ struct
let intersect_vc vc p =
Vars.intersect (F.varsp p) vc.vars || Conditions.intersect p vc.hyps
- let state_vc ?descr ?stmt state vc =
+ let state_vc ?descr ?stmt sigma state vc =
let path = match stmt with
| None -> vc.path
| Some s -> S.add s vc.path in
- let hyps = Conditions.state ?stmt ?descr state vc.hyps in
+ let hyps =
+ if not (Wp_parameters.RTE.get()) then vc.hyps
+ else Conditions.domain [M.is_well_formed sigma] vc.hyps
+ in
+ let hyps = Conditions.state ?stmt ?descr state hyps in
{ vc with path ; hyps }
let assume_vc ?descr ?hpid ?stmt ?warn
@@ -640,7 +644,7 @@ struct
| Some { labels = lbl::_ } ->
Some (Pretty_utils.to_string Printer.pp_label lbl) in
let state = Mstate.state state sigma in
- gmap (state_vc ?descr ?stmt state) vcs
+ gmap (state_vc ?descr ?stmt sigma state) vcs
with Not_found -> vcs
let label wenv stmt label wp =
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
index e519f55833a..85d318865a1 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
@@ -71,19 +71,10 @@ Let a = global(G_tr_35).
Let a_1 = shift___anonstruct_Point_1(a, 2).
Let a_2 = shift___anonstruct_Point_1(a, 1).
Let a_3 = shift___anonstruct_Point_1(a, 0).
-Let a_4 = shiftfield_F4_bytes(global(G_buint_41)).
Let m = Array1_S1(a, 3, Mint_0).
Assume {
Type: IsArray1S1(m) /\ IsArray1S1(Array1_S1(a_3, 3, Mint_0)).
(* Initializer *)
- Init: Mint_0[shift_uint8(a_4, 0)] = 1.
- (* Initializer *)
- Init: Mint_0[shift_uint8(a_4, 1)] = 2.
- (* Initializer *)
- Init: Mint_0[shift_uint8(a_4, 2)] = 4.
- (* Initializer *)
- Init: Mint_0[shift_uint8(a_4, 3)] = 8.
- (* Initializer *)
Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
(* Initializer *)
Init: Mint_0[shiftfield_F1_y(a_3)] = 11.
@@ -105,19 +96,10 @@ Let a = global(G_tr_35).
Let a_1 = shift___anonstruct_Point_1(a, 2).
Let a_2 = shift___anonstruct_Point_1(a, 1).
Let a_3 = shift___anonstruct_Point_1(a, 0).
-Let a_4 = shiftfield_F4_bytes(global(G_buint_41)).
Let m = Array1_S1(a, 3, Mint_0).
Assume {
Type: IsArray1S1(m) /\ IsArray1S1(Array1_S1(a_3, 3, Mint_0)).
(* Initializer *)
- Init: Mint_0[shift_uint8(a_4, 0)] = 1.
- (* Initializer *)
- Init: Mint_0[shift_uint8(a_4, 1)] = 2.
- (* Initializer *)
- Init: Mint_0[shift_uint8(a_4, 2)] = 4.
- (* Initializer *)
- Init: Mint_0[shift_uint8(a_4, 3)] = 8.
- (* Initializer *)
Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
(* Initializer *)
Init: Mint_0[shiftfield_F1_y(a_3)] = 11.
@@ -139,19 +121,10 @@ Let a = global(G_tr_35).
Let a_1 = shift___anonstruct_Point_1(a, 2).
Let a_2 = shift___anonstruct_Point_1(a, 1).
Let a_3 = shift___anonstruct_Point_1(a, 0).
-Let a_4 = shiftfield_F4_bytes(global(G_buint_41)).
Let m = Array1_S1(a_3, 3, Mint_0).
Assume {
Type: IsArray1S1(Array1_S1(a, 3, Mint_0)) /\ IsArray1S1(m).
(* Initializer *)
- Init: Mint_0[shift_uint8(a_4, 0)] = 1.
- (* Initializer *)
- Init: Mint_0[shift_uint8(a_4, 1)] = 2.
- (* Initializer *)
- Init: Mint_0[shift_uint8(a_4, 2)] = 4.
- (* Initializer *)
- Init: Mint_0[shift_uint8(a_4, 3)] = 8.
- (* Initializer *)
Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
(* Initializer *)
Init: Mint_0[shiftfield_F1_y(a_3)] = 11.
@@ -220,37 +193,21 @@ Goal Pre-condition 'qed_ok' in 'main':
tests/wp_acsl/logic.i:55: warning from wp:
- Warning: Hide sub-term definition
Reason: Logic cast to struct (Buint) from (unsigned int) not implemented yet
-Let a = global(G_tr_35).
-Let a_1 = shift___anonstruct_Point_1(a, 2).
-Let a_2 = shift___anonstruct_Point_1(a, 1).
-Let a_3 = shift___anonstruct_Point_1(a, 0).
-Let a_4 = global(G_buint_41).
-Let a_5 = shiftfield_F4_bytes(a_4).
-Let a_6 = Load_S4(a_4, Mint_0).
+Let a = global(G_buint_41).
+Let a_1 = shiftfield_F4_bytes(a).
+Let a_2 = Load_S4(a, Mint_0).
Assume {
- Type: IsS4(a_6).
- (* Initializer *)
- Init: Mint_0[shift_uint8(a_5, 0)] = 1.
- (* Initializer *)
- Init: Mint_0[shift_uint8(a_5, 1)] = 2.
- (* Initializer *)
- Init: Mint_0[shift_uint8(a_5, 2)] = 4.
- (* Initializer *)
- Init: Mint_0[shift_uint8(a_5, 3)] = 8.
- (* Initializer *)
- Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
+ Type: IsS4(a_2).
(* Initializer *)
- Init: Mint_0[shiftfield_F1_y(a_3)] = 11.
+ Init: Mint_0[shift_uint8(a_1, 0)] = 1.
(* Initializer *)
- Init: Mint_0[shiftfield_F1_x(a_2)] = 20.
+ Init: Mint_0[shift_uint8(a_1, 1)] = 2.
(* Initializer *)
- Init: Mint_0[shiftfield_F1_y(a_2)] = 21.
+ Init: Mint_0[shift_uint8(a_1, 2)] = 4.
(* Initializer *)
- Init: Mint_0[shiftfield_F1_x(a_1)] = 30.
- (* Initializer *)
- Init: Mint_0[shiftfield_F1_y(a_1)] = 31.
+ Init: Mint_0[shift_uint8(a_1, 3)] = 8.
}
-Prove: EqS4(a_6, w).
+Prove: EqS4(a_2, w).
------------------------------------------------------------
--
GitLab