From e8abbf7699d67ff742e836a555f416d6e175d8ee Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 21 Aug 2019 15:27:27 +0200
Subject: [PATCH] [wp/region] use mem-loader and mem-memory into mem-typed
---
src/plugins/wp/Definitions.ml | 2 +
src/plugins/wp/Definitions.mli | 1 +
src/plugins/wp/Lang.mli | 3 +
src/plugins/wp/LogicAssigns.ml | 6 +-
src/plugins/wp/MemMemory.ml | 4 +-
src/plugins/wp/MemTyped.ml | 879 ++++--------------
src/plugins/wp/MemTyped.mli | 8 -
src/plugins/wp/MemVar.ml | 15 +-
src/plugins/wp/Sigs.ml | 2 +-
src/plugins/wp/TacHavoc.ml | 42 +-
.../tests/wp_bts/oracle/bts_2110.res.oracle | 18 +-
.../frama_c_hashtbl_solved.res.oracle | 4 +-
.../wp_plugin/oracle/inductive.res.oracle | 2 +-
src/plugins/wp/why3_api.ml | 3 +-
14 files changed, 218 insertions(+), 771 deletions(-)
diff --git a/src/plugins/wp/Definitions.ml b/src/plugins/wp/Definitions.ml
index 4d152b904f7..bc8debdd639 100644
--- a/src/plugins/wp/Definitions.ml
+++ b/src/plugins/wp/Definitions.ml
@@ -212,6 +212,8 @@ let newcluster ~id ?title ?position () =
let cluster ~id ?title ?position () =
Cluster.memoize (fun id -> newcluster ~id ?title ?position ()) id
+let dummy () = cluster ~id:"dummy" ()
+
let axiomatic ax =
Cluster.memoize
(fun id ->
diff --git a/src/plugins/wp/Definitions.mli b/src/plugins/wp/Definitions.mli
index 5814a70c952..cd93d34343d 100644
--- a/src/plugins/wp/Definitions.mli
+++ b/src/plugins/wp/Definitions.mli
@@ -28,6 +28,7 @@ open Lang.F
type cluster
+val dummy : unit -> cluster
val cluster : id:string -> ?title:string -> ?position:Filepath.position -> unit -> cluster
val axiomatic : axiomatic -> cluster
val section : logic_section -> cluster
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index 7ef00de80b2..1dd7541f7db 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -31,7 +31,10 @@ open Qed.Logic
type library = string
+(** Name for external prover.
+ In case a Qed.Engine.link is used, [F_subst] patterns
+ are not supported for Why-3. *)
type 'a infoprover = {
altergo: 'a;
why3 : 'a;
diff --git a/src/plugins/wp/LogicAssigns.ml b/src/plugins/wp/LogicAssigns.ml
index 024797e3177..8da52bbfe32 100644
--- a/src/plugins/wp/LogicAssigns.ml
+++ b/src/plugins/wp/LogicAssigns.ml
@@ -53,7 +53,8 @@ struct
| [] -> Bag.concat (M.Sigma.assigned ~pre:s.pre ~post:s.post D.empty) hs
| [obj,sloc] ->
- let hs_sloc = Bag.list (M.assigned s obj sloc) in
+ let eq_sloc = M.assigned s obj sloc in
+ let hs_sloc = Bag.list (List.map Cvalues.equation eq_sloc) in
let hs_sdom = M.Sigma.assigned ~pre:s.pre ~post:s.post (dsloc obj sloc) in
Bag.concat (Bag.concat hs_sloc hs_sdom) hs
@@ -61,7 +62,8 @@ struct
let sigma = M.Sigma.havoc s.post (dsloc obj sloc) in
let s_local = { pre = sigma ; post = s.post } in
let s_other = { pre = s.pre ; post = sigma } in
- let hs_sloc = Bag.list (M.assigned s_local obj sloc) in
+ let eq_sloc = M.assigned s_local obj sloc in
+ let hs_sloc = Bag.list (List.map Cvalues.equation eq_sloc) in
assigned_seq (Bag.concat hs_sloc hs) s_other tail
let apply_assigns (s:sigma sequence) (r: M.loc Sigs.region) =
diff --git a/src/plugins/wp/MemMemory.ml b/src/plugins/wp/MemMemory.ml
index 8568209bc57..1ea1e473997 100644
--- a/src/plugins/wp/MemMemory.ml
+++ b/src/plugins/wp/MemMemory.ml
@@ -35,12 +35,12 @@ let a_addr = Lang.datatype ~library "addr"
let t_addr = L.Data(a_addr,[])
let f_base = Lang.extern_f ~library ~result:L.Int
~link:{altergo = Qed.Engine.F_subst("%1.base");
- why3 = Qed.Engine.F_subst("%1.base");
+ why3 = Qed.Engine.F_call "base";
coq = Qed.Engine.F_subst("(base %1)");
} "base"
let f_offset = Lang.extern_f ~library ~result:L.Int
~link:{altergo = Qed.Engine.F_subst("%1.offset");
- why3 = Qed.Engine.F_subst("%1.offset");
+ why3 = Qed.Engine.F_call "offset";
coq = Qed.Engine.F_subst("(offset %1)");
} "offset"
let f_shift = Lang.extern_f ~library ~result:t_addr "shift"
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 414d5f49fcf..c93c76e5288 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -31,63 +31,38 @@ open Lang
open Lang.F
open Sigs
open Definitions
+open MemMemory
let dkey_layout = Wp_parameters.register_category "layout"
module L = Qed.Logic
+(* -------------------------------------------------------------------------- *)
+(* --- Model Configuration --- *)
+(* -------------------------------------------------------------------------- *)
+
let datatype = "MemTyped"
let hypotheses () = []
-let library = "memory"
-
-let a_addr = Lang.datatype ~library "addr"
-let t_addr = L.Data(a_addr,[])
-let f_base = Lang.extern_f ~library ~result:L.Int
- ~link:{altergo = Qed.Engine.F_subst("%1.base");
- why3 = Qed.Engine.F_call("base");
- coq = Qed.Engine.F_subst("(base %1)");
- } "base"
-let f_offset = Lang.extern_f ~library ~result:L.Int
- ~link:{altergo = Qed.Engine.F_subst("%1.offset");
- why3 = Qed.Engine.F_call("offset");
- coq = Qed.Engine.F_subst("(offset %1)");
- } "offset"
-let f_shift = Lang.extern_f ~library ~result:t_addr "shift"
-let f_global = Lang.extern_f ~library ~result:t_addr ~category:L.Injection "global"
-let f_null = Lang.extern_f ~library ~result:t_addr "null"
-let f_base_offset = Lang.extern_f ~library ~category:Qed.Logic.Injection ~result:L.Int "base_offset"
-
-let ty_havoc = function
- | Some l :: _ -> l
- | _ -> raise Not_found
+let configure () =
+ begin
+ Context.set Lang.pointer (fun _ -> t_addr) ;
+ Context.set Cvalues.null (p_equal a_null) ;
+ end
-let l_havoc = Qed.Engine.{
- coq = F_call "fhavoc" ;
- altergo = F_call "havoc" ;
- why3 = F_call "havoc" ;
- }
-
-let p_valid_rd = Lang.extern_fp ~library "valid_rd"
-let p_valid_rw = Lang.extern_fp ~library "valid_rw"
-let p_invalid = Lang.extern_fp ~library "invalid"
-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_havoc ~link:l_havoc "havoc"
-let f_region = Lang.extern_f ~library ~result:L.Int "region" (* base -> region *)
-let p_framed = Lang.extern_fp ~library "framed" (* m-pointer -> prop *)
-let p_linked = Lang.extern_fp ~library "linked" (* allocation-table -> prop *)
-let p_sconst = Lang.extern_fp ~library "sconst" (* int-memory -> prop *)
-let a_lt = Lang.extern_p ~library ~bool:"addr_lt_bool" ~prop:"addr_lt" ()
-let a_leq = Lang.extern_p ~library ~bool:"addr_le_bool" ~prop:"addr_le" ()
-
-let a_addr_of_int = Lang.extern_f
- ~category:L.Injection
- ~library ~result:t_addr "addr_of_int"
-
-let a_int_of_addr = Lang.extern_f
- ~category:L.Injection
- ~library ~result:L.Int "int_of_addr"
+let configure_ia =
+ let no_binder = { bind = fun _ f v -> f v } in
+ fun _vertex -> no_binder
+
+(* -------------------------------------------------------------------------- *)
+(* --- Model Parameters --- *)
+(* -------------------------------------------------------------------------- *)
+
+type pointer = NoCast | Fits | Unsafe
+let pointer = Context.create "MemTyped.pointer"
+
+(* -------------------------------------------------------------------------- *)
+(* --- Model Semantics --- *)
+(* -------------------------------------------------------------------------- *)
(*
@@ -132,270 +107,6 @@ let a_int_of_addr = Lang.extern_f
*)
-(* -------------------------------------------------------------------------- *)
-(* --- Utilities --- *)
-(* -------------------------------------------------------------------------- *)
-
-let a_null = F.constant (e_fun f_null [])
-let a_base p = e_fun f_base [p]
-let a_offset p = e_fun f_offset [p]
-let a_global b = e_fun f_global [b]
-let a_base_offset k = e_fun f_base_offset [k]
-let a_shift l k = e_fun f_shift [l;k]
-let a_addr b k = a_shift (a_global b) k
-
-(* -------------------------------------------------------------------------- *)
-(* --- Qed Simplifiers --- *)
-(* -------------------------------------------------------------------------- *)
-
-(*
- Pointer arithmetic for structure access and array access could be
- defined directly using the record [{ base = p.base; offset = p.offset
- + c*i + c' }]. However that gives very bad triggers for the memory
- model axiomatization, so `shift p (c*i+c')` was used instead. It is
- not sufficient for user axiomatisation because memory access in
- axioms require trigger with arithmetic operators which is badly
- handled by provers. So for each c and c', ie for each kind of
- structure access and array access a specific function is used
- `shift_xxx`.
-
- Moreover no simplification of `shift_xxx` is done for keeping the
- same terms in axioms and the goal. `base` and `offset` function
- simplify all the `shift_xxx` because it seems they don't appear
- often in axioms and they are useful for simplifying `separated`,
- `assigns` and pointer comparisons in goals.
-
- To sum up memory access should match, but not `\base`, `\offset`,
- `\separated`, ...
-*)
-
-type registered_shift =
- | RS_Field of fieldinfo * term (* offset of the field *)
- | RS_Shift of Z.t (* size of the element *)
-
-module RegisterShift = Model.Static
- (struct
- type key = lfun
- type data = registered_shift
- let name = "MemTyped.RegisterShift"
- include Lang.Fun
- end)
-
-let phi_base l =
- match F.repr l with
- | L.Fun(f,p::_) when RegisterShift.mem f -> a_base p
- | L.Fun(f,[p;_]) when f==f_shift -> a_base p
- | L.Fun(f,[b]) when f==f_global -> b
- | L.Fun(f,[]) when f==f_null -> e_zero
- | _ -> raise Not_found
-
-let phi_offset l = match F.repr l with
- | L.Fun(f,[p;k]) when f==f_shift -> e_add (a_offset p) k
- | L.Fun(f,_) when f==f_global || f==f_null -> F.e_zero
- | L.Fun(f,p::args) ->
- begin match RegisterShift.get f, args with
- | Some (RS_Field(_,offset)), [] -> e_add offset (a_offset p)
- | Some (RS_Shift size), [k] -> e_add (a_offset p) ((F.e_times size) k)
- | Some _, _ -> assert false (* constructed at one place only *)
- | None, _ -> raise Not_found
- end
- | _ -> raise Not_found
-
-let eq_shift a b =
- let p = a_base a in
- let q = a_base b in
- let i = a_offset a in
- let j = a_offset b in
- if i==j then F.p_equal p q else
- match F.is_equal p q with
- | L.No -> F.p_false
- | L.Yes -> F.p_equal i j
- | L.Maybe -> raise Not_found
-
-let phi_shift f p i =
- match F.repr p with
- | L.Fun(g,[q;j]) when f == g -> F.e_fun f [q;F.e_add i j]
- | _ -> raise Not_found
-
-(* -------------------------------------------------------------------------- *)
-(* --- Simplifier for 'separated' --- *)
-(* -------------------------------------------------------------------------- *)
-
-(*
-logic a : int
-logic b : int
-logic S : prop
-
-predicate separated = a <= 0 or b <= 0 or S
-*)
-
-let r_separated = function
- | [p;a;q;b] ->
- if a == F.e_one && b == F.e_one then F.e_neq p q
- else
- begin
- let a_negative = F.e_leq a F.e_zero in
- let b_negative = F.e_leq b F.e_zero in
- if a_negative == e_true || b_negative == e_true then e_true else
- let bp = a_base p in
- let bq = a_base q in
- let open Qed.Logic in
- match F.is_true (F.e_eq bp bq) with
- | No -> e_true (* Have S *)
- | Yes when (a_negative == e_false && b_negative == e_false) ->
- (* Reduced to S *)
- let p_ofs = a_offset p in
- let q_ofs = a_offset q in
- let p_ofs' = F.e_add p_ofs a in
- let q_ofs' = F.e_add q_ofs b in
- F.e_or [ F.e_leq q_ofs' p_ofs ;
- F.e_leq p_ofs' q_ofs ]
- | _ -> raise Not_found
- end
- | _ -> raise Not_found
-
-let is_separated args = F.is_true (r_separated args)
-
-(* -------------------------------------------------------------------------- *)
-(* --- Simplifier for 'included' --- *)
-(* -------------------------------------------------------------------------- *)
-
-(*
-logic a : int
-logic b : int
-
-predicate R = p.base = q.base
- /\ (q.offset <= p.offset)
- /\ (p.offset + a <= q.offset + b)
-
-predicate included = 0 < a -> ( 0 <= b and R )
-predicate a_empty = a <= 0
-predicate b_negative = b < 0
-
-lemma SAME_P: p=q -> (R <-> a<=b)
-lemma SAME_A: a=b -> (R <-> p=q)
-
-goal INC_P: p=q -> (included <-> ( 0 < a -> a <= b )) (by SAME_P)
-goal INC_A: a=b -> 0 < a -> (included <-> R) (by SAME_A)
-goal INC_1: a_empty -> (included <-> true)
-goal INC_2: b_negative -> (included <-> a_empty)
-goal INC_3: not R -> (included <-> a_empty)
-goal INC_4: not a_empty -> not b_negative -> (included <-> R)
-*)
-
-let r_included = function
- | [p;a;q;b] ->
- if F.e_eq p q == F.e_true
- then F.e_imply [F.e_lt F.e_zero a] (F.e_leq a b) (* INC_P *)
- else
- if (F.e_eq a b == F.e_true) && (F.e_lt F.e_zero a == F.e_true)
- then F.e_eq p q (* INC_A *)
- else
- begin
- let a_empty = F.e_leq a F.e_zero in
- let b_negative = F.e_lt b F.e_zero in
- if a_empty == F.e_true then F.e_true (* INC_1 *) else
- if b_negative == F.e_true then a_empty (* INC_2 *) else
- let bp = a_base p in
- let bq = a_base q in
- let open Qed.Logic in
- match F.is_true (F.e_eq bp bq) with
- | No -> a_empty (* INC_3 *)
- | Yes when (a_empty == e_false && b_negative == e_false) ->
- (* INC_4 *)
- let p_ofs = a_offset p in
- let q_ofs = a_offset q in
- if a == b then F.e_eq p_ofs q_ofs
- else
- let p_ofs' = e_add p_ofs a in
- let q_ofs' = e_add q_ofs b in
- e_and [ F.e_leq q_ofs p_ofs ; F.e_leq p_ofs' q_ofs' ]
- | _ -> raise Not_found
- end
- | _ -> raise Not_found
-
-(* -------------------------------------------------------------------------- *)
-(* --- Simplifier for 'havoc' --- *)
-(* -------------------------------------------------------------------------- *)
-
-(* havoc(m_undef, havoc(_undef,m0,p0,a0), p1,a1) =
- - havoc(m_undef, m0, p1,a1) WHEN included (p1,a1,p0,a0) *)
-let r_havoc = function
- | [undef1;m1;p1;a1] -> begin
- match F.repr m1 with
- | L.Fun( f , [_undef0;m0;p0;a0] ) when f == f_havoc -> begin
- let open Qed.Logic in
- match F.is_true (r_included [p0;a0;p1;a1]) with
- | Yes -> F.e_fun f_havoc [undef1;m0;p1;a1]
- | _ -> raise Not_found
- end
- | _ -> raise Not_found
- end
- | _ -> raise Not_found
-
-(* havoc(undef,m,p,a)[k] =
- - undef[k] WHEN separated (p,a,k,1)
- - m[k] WHEN NOT separated (p,a,k,1)
-*)
-let r_get_havoc = function
- | [undef;m;p;a] ->
- (fun _ k ->
- match is_separated [p;a;k;e_one] with
- | L.Yes -> F.e_get m k
- | L.No -> F.e_get undef k
- | _ -> raise Not_found)
- | _ -> raise Not_found
-
-(* -------------------------------------------------------------------------- *)
-(* --- Simplifier for int/addr conversion --- *)
-(* -------------------------------------------------------------------------- *)
-
-let phi_int_of_addr p =
- if p == a_null then F.e_zero else
- match F.repr p with
- | L.Fun(f,[a]) when f == a_addr_of_int -> a
- | _ -> raise Not_found
-
-let phi_addr_of_int p =
- if p == F.e_zero then a_null else
- match F.repr p with
- | L.Fun(f,[a]) when f == a_int_of_addr -> a
- | _ -> raise Not_found
-
-(* -------------------------------------------------------------------------- *)
-(* --- Simplifier Registration --- *)
-(* -------------------------------------------------------------------------- *)
-
-let () = Context.register
- begin fun () ->
- F.set_builtin_1 f_base phi_base ;
- F.set_builtin_1 f_offset phi_offset ;
- F.set_builtin_2 f_shift (phi_shift f_shift) ;
- F.set_builtin_eqp f_shift eq_shift ;
- F.set_builtin_eqp f_global eq_shift ;
- F.set_builtin p_separated r_separated ;
- F.set_builtin p_included r_included ;
- F.set_builtin f_havoc r_havoc ;
- F.set_builtin_get f_havoc r_get_havoc ;
- F.set_builtin_1 a_addr_of_int phi_addr_of_int ;
- F.set_builtin_1 a_int_of_addr phi_int_of_addr ;
- end
-
-(* -------------------------------------------------------------------------- *)
-(* --- Model Parameters --- *)
-(* -------------------------------------------------------------------------- *)
-
-let configure () =
- begin
- Context.set Lang.pointer (fun _ -> t_addr) ;
- Context.set Cvalues.null (p_equal a_null) ;
- end
-let no_binder = { bind = fun _ f v -> f v }
-let configure_ia _ = no_binder
-
-type pointer = NoCast | Fits | Unsafe
-let pointer = Context.create "MemTyped.pointer"
-
(* -------------------------------------------------------------------------- *)
(* --- Chunks --- *)
(* -------------------------------------------------------------------------- *)
@@ -430,9 +141,6 @@ struct
let compare a b = rank a - rank b
let equal = (=)
let pretty fmt c = Format.pp_print_string fmt (name c)
- let key_of_chunk = function
- | M_int | M_char | M_f32 | M_f64 | M_pointer -> t_addr
- | T_alloc -> L.Int
let val_of_chunk = function
| M_int | M_char -> L.Int
| M_f32 -> Cfloat.tau_of_float Ctypes.Float32
@@ -474,24 +182,13 @@ and footprint_comp c =
Heap.Set.union ft (footprint (object_of f.ftype))
) Heap.Set.empty c.cfields
-let signature ft =
- let s = Sigma.create () in
- let xs = ref [] in
- let cs = ref [] in
- Heap.Set.iter
- (fun c ->
- cs := c :: !cs ;
- xs := (Sigma.get s c) :: !xs ;
- ) ft ;
- List.rev !xs , List.rev !cs , s
-
-let memories sigma ft = List.map (Sigma.value sigma) ft
+let domain obj _l = footprint obj
-let rec size_of_object = function
+let rec length_of_object = function
| C_int _ | C_float _ | C_pointer _ -> 1
- | C_comp c -> size_of_comp c
+ | C_comp c -> length_of_comp c
| C_array { arr_flat = Some { arr_size = n } ; arr_element = elt } ->
- n * (size_of_typ elt)
+ n * (length_of_typ elt)
| C_array _ as a ->
if Wp_parameters.ExternArrays.get () then
max_int
@@ -499,20 +196,20 @@ let rec size_of_object = function
Warning.error ~source:"Typed Model"
"Undefined array-size (%a)" Ctypes.pretty a
-and size_of_typ t = size_of_object (object_of t)
-and size_of_field f = size_of_typ f.ftype
-and size_of_comp c =
+and length_of_typ t = length_of_object (object_of t)
+and length_of_field f = length_of_typ f.ftype
+and length_of_comp c =
(* union field are considered as struct field *)
List.fold_left
- (fun s f -> s + size_of_field f)
+ (fun s f -> s + length_of_field f)
0 c.cfields
-let offset_of_field f =
+let position_of_field f =
let rec fnext k f = function
| [] -> assert false
| g::gs ->
if Fieldinfo.equal f g then k
- else fnext (k + size_of_field g) f gs
+ else fnext (k + length_of_field g) f gs
in fnext 0 f f.fcomp.cfields
(* -------------------------------------------------------------------------- *)
@@ -531,15 +228,32 @@ let occurs x l = F.occurs x l
(* --- Generated Axiomatization --- *)
(* -------------------------------------------------------------------------- *)
-let loadrec = ref (fun _ _ _ -> assert false)
-
let cluster_globals () =
Definitions.cluster ~id:"Globals" ~title:"Global Variables" ()
-let cluster_memory () =
- Definitions.cluster ~id:"Compound" ~title:"Memory Compound Updates" ()
+type shift =
+ | RS_Field of fieldinfo * int (* offset of the field *)
+ | RS_Index of int (* size of the shift *)
-let cluster_dummy () = Definitions.cluster ~id:"dummy" ()
+let phi_base = function
+ | p::_ -> a_base p
+ | _ -> raise Not_found
+
+let phi_field offset = function
+ | [p] -> e_add (a_offset p) (F.e_int offset)
+ | _ -> raise Not_found
+
+let phi_index size = function
+ | [p;k] -> e_add (a_offset p) (F.e_fact size k)
+ | _ -> raise Not_found
+
+module RegisterShift = Model.Static
+ (struct
+ type key = lfun
+ type data = shift
+ let name = "MemTyped.RegisterShift"
+ include Lang.Fun
+ end)
module ShiftFieldDef = Model.StaticGenerator(Cil_datatype.Fieldinfo)
(struct
@@ -550,19 +264,19 @@ module ShiftFieldDef = Model.StaticGenerator(Cil_datatype.Fieldinfo)
let generate f =
let result = t_addr in
let lfun = Lang.generated_f ~result "shiftfield_%s" (Lang.field_id f) in
- let offset = (F.e_int (offset_of_field f)) in
+ let position = position_of_field f in
(* Since its a generated it is the unique name given *)
let xloc = Lang.freshvar ~basename:"p" t_addr in
let loc = e_var xloc in
- let def = a_shift loc offset in
+ let def = a_shift loc (F.e_int position) in
let dfun = Definitions.Function( result , Def , def) in
- RegisterShift.define lfun (RS_Field(f,offset)) ;
- F.set_builtin_eqp lfun eq_shift ;
+ RegisterShift.define lfun (RS_Field(f,position)) ;
+ MemMemory.register ~base:phi_base ~offset:(phi_field position) lfun ;
{
d_lfun = lfun ; d_types = 0 ;
d_params = [xloc] ;
d_definition = dfun ;
- d_cluster = cluster_dummy () ;
+ d_cluster = Definitions.dummy () ;
}
let compile = Lang.local generate
@@ -575,7 +289,7 @@ module ShiftField = Model.Generator(Cil_datatype.Fieldinfo)
type data = lfun
let compile fd =
let dfun = ShiftFieldDef.get fd in
- let d_cluster = cluster_memory () in
+ let d_cluster = MemLoader.cluster () in
Definitions.define_symbol { dfun with d_cluster } ;
dfun.d_lfun
end)
@@ -611,22 +325,22 @@ module ShiftGen = Model.StaticGenerator(Cobj)
let generate obj =
let result = t_addr in
let shift = Lang.generated_f ~result "shift_%s" (c_object_id obj) in
- let size = Integer.of_int (size_of_object obj) in
+ let size = length_of_object obj in
(* Since its a generated it is the unique name given *)
let xloc = Lang.freshvar ~basename:"p" t_addr in
let loc = e_var xloc in
let xk = Lang.freshvar ~basename:"k" Qed.Logic.Int in
let k = e_var xk in
- let def = a_shift loc (F.e_times size k) in
+ let def = a_shift loc (F.e_fact size k) in
let dfun = Definitions.Function( result , Def , def) in
- RegisterShift.define shift (RS_Shift size) ;
- F.set_builtin_eqp shift eq_shift ;
- F.set_builtin_2 shift (phi_shift shift) ;
+ RegisterShift.define shift (RS_Index size) ;
+ MemMemory.register ~base:phi_base ~offset:(phi_index size)
+ ~linear:true shift ;
{
d_lfun = shift ; d_types = 0 ;
d_params = [xloc;xk] ;
d_definition = dfun ;
- d_cluster = cluster_dummy () ;
+ d_cluster = Definitions.dummy () ;
}
let compile = Lang.local generate
@@ -640,7 +354,7 @@ module Shift = Model.Generator(Cobj)
type data = lfun
let compile obj =
let dfun = ShiftGen.get obj in
- let d_cluster = cluster_memory () in
+ let d_cluster = MemLoader.cluster () in
Definitions.define_symbol { dfun with d_cluster } ;
dfun.d_lfun
end)
@@ -740,6 +454,10 @@ module STRING = Model.Generator(LITERAL)
end)
+(* -------------------------------------------------------------------------- *)
+(* --- Base Registration --- *)
+(* -------------------------------------------------------------------------- *)
+
module RegisterBASE = Model.Static
(struct
type key = lfun
@@ -764,22 +482,20 @@ module BASE = Model.Generator(Varinfo)
l_cluster = cluster_globals () ;
}
+ let sizeof x =
+ Warning.handle
+ ~handler:(fun _ -> None)
+ ~effect:(Printf.sprintf "No allocation size for variable '%s'" x.vname)
+ (fun obj -> Some (length_of_object obj))
+ (Ctypes.object_of x.vtype)
+
let linked prefix x base =
let name = prefix ^ "_linked" in
- let obj = Ctypes.object_of x.vtype in
- let size =
- if x.vglob then
- Warning.handle
- ~handler:(fun _ -> None)
- ~effect:(Printf.sprintf "No allocation size for variable '%s'" x.vname)
- (fun obj -> Some (size_of_object obj))
- obj
- else Some 0
- in
+ let size = if x.vglob then sizeof x else Some 0 in
match size with
| None -> ()
| Some size ->
- let a = Lang.freshvar ~basename:"alloc" (Chunk.tau_of_chunk T_alloc) in
+ let a = Lang.freshvar ~basename:"alloc" t_malloc in
let m = e_var a in
let m_linked = p_call p_linked [m] in
let base_size = p_equal (F.e_get m base) (e_int size) in
@@ -817,215 +533,6 @@ module BASE = Model.Generator(Varinfo)
let compile = Lang.local generate
end)
-
-(* Add frame lemmas for generated logical function *)
-module MONOTONIC :
-sig
- val generate :
- string -> lfun -> var list -> chunk list -> (term list -> term) -> unit
-end =
-struct
-
- type env = {
- lfun : lfun ;
- sigma : sigma ;
- vars : var list ;
- params : term list ;
- range : term ;
- chunks : chunk list ;
- memories : term list ;
- }
-
- let _cluster () = Definitions.cluster ~id:"TypedMemory" ()
- (* projectified *)
-
- let update env c m =
- List.map
- (fun c' ->
- if Chunk.equal c c' then m else Sigma.value env.sigma c'
- ) env.chunks
-
- let separated env q k = F.p_call p_separated [List.hd env.params;env.range;q;k]
- let included env q k = F.p_call p_included [List.hd env.params;env.range;q;k]
-
- let generate_update prefix env c =
- let name = prefix ^ "_update_" ^ Chunk.name c in
- let q = e_var (Lang.freshvar ~basename:"q" (Chunk.key_of_chunk c)) in
- let v = e_var (Lang.freshvar ~basename:"v" (Chunk.val_of_chunk c)) in
- let phi = e_fun env.lfun (env.params @ env.memories) in
- let mem' = e_set (Sigma.value env.sigma c) q v in
- let phi' = e_fun env.lfun (env.params @ update env c mem') in
- let lemma = p_imply (separated env q e_one) (p_equal phi' phi) in
- Definitions.define_lemma {
- l_assumed = true ;
- l_name = name ; l_types = 0 ;
- l_triggers = [[Trigger.of_term phi']] ;
- l_forall = F.p_vars lemma ;
- l_lemma = lemma ;
- l_cluster = cluster_memory () ;
- }
-
- let generate_eqmem prefix env c =
- let name = prefix ^ "_eqmem_" ^ Chunk.name c in
- let q = e_var (Lang.freshvar ~basename:"q" (Chunk.key_of_chunk c)) in
- let k = e_var (Lang.freshvar ~basename:"k" L.Int) in
- let phi = e_fun env.lfun (env.params @ env.memories) in
- let mem = Sigma.value env.sigma c in
- let mem' = e_var (Lang.freshen (Sigma.get env.sigma c)) in
- let phi' = e_fun env.lfun (env.params @ update env c mem') in
- let eqmem = F.p_call p_eqmem [mem;mem';q;k] in
- let lemma = p_hyps [included env q k;eqmem] (p_equal phi' phi) in
- Definitions.define_lemma {
- l_assumed = true ;
- l_name = name ; l_types = 0 ;
- l_triggers = [
- [Trigger.of_pred eqmem ; Trigger.of_term phi ] ;
- [Trigger.of_pred eqmem ; Trigger.of_term phi'] ;
- ] ;
- l_forall = F.p_vars lemma ;
- l_lemma = lemma ;
- l_cluster = cluster_memory () ;
- }
-
- let generate_havoc prefix env c =
- let name = prefix ^ "_havoc_" ^ Chunk.name c in
- let q = e_var (Lang.freshvar ~basename:"q" (Chunk.key_of_chunk c)) in
- let k = e_var (Lang.freshvar ~basename:"k" L.Int) in
- let phi = e_fun env.lfun (env.params @ env.memories) in
- let mem = Sigma.value env.sigma c in
- let mem' = e_var (Lang.freshen (Sigma.get env.sigma c)) in
- let m_undef = e_var (Lang.freshen (Sigma.get env.sigma c)) in
- let phi' = e_fun env.lfun (env.params @ update env c mem') in
- let havoc = p_equal mem' (F.e_fun f_havoc [m_undef;mem;q;k]) in
- let lemma = p_hyps [separated env q k;havoc] (p_equal phi' phi) in
- Definitions.define_lemma {
- l_assumed = true ;
- l_name = name ; l_types = 0 ;
- l_triggers = [
- [ Trigger.of_pred havoc ; Trigger.of_term phi ] ;
- [ Trigger.of_pred havoc ; Trigger.of_term phi'] ;
- ] ;
- l_forall = F.p_vars lemma ;
- l_lemma = lemma ;
- l_cluster = cluster_memory () ;
- }
-
- let generate prefix lfun xs cs range =
- let sigma = Sigma.create () in
- let xp = Lang.freshvar ~basename:"p" t_addr in
- let xs = List.map Lang.freshen xs in
- let ps = List.map e_var xs in
- let ms = memories sigma cs in
- let env = {
- sigma = sigma ; lfun = lfun ;
- vars = xp::xs ; params = e_var xp::ps ;
- chunks = cs ; memories = ms ;
- range = range ps ;
- } in
- List.iter
- (fun chunk ->
- generate_update prefix env chunk ;
- generate_eqmem prefix env chunk ;
- generate_havoc prefix env chunk ;
- ) cs
-
-end
-
-module COMP = Model.Generator(Compinfo)
- (struct
- let name = "MemTyped.COMP"
- type key = compinfo
- type data = lfun * chunk list
-
- let generate c =
- let result = Lang.tau_of_comp c in
- let lfun = Lang.generated_f ~result "Load_%s" (Lang.comp_id c) in
- (* Since its a generated it is the unique name given *)
- let prefix = Lang.Fun.debug lfun in
- let xmem,ft,sigma = signature (footprint_comp c) in
- let xloc = Lang.freshvar ~basename:"p" t_addr in
- let loc = e_var xloc in
- let def = List.map
- (fun f ->
- Cfield f , !loadrec sigma (object_of f.ftype) (field loc f)
- ) c.cfields in
- let dfun = Definitions.Function( result , Def , e_record def ) in
- Definitions.define_symbol {
- d_lfun = lfun ; d_types = 0 ;
- d_params = xloc :: xmem ;
- d_definition = dfun ;
- d_cluster = cluster_memory () ;
- } ;
- let range = e_int (size_of_comp c) in
- MONOTONIC.generate prefix lfun [] ft (fun _ -> range) ;
- lfun , ft
-
- let compile = Lang.local generate
- end)
-
-module ARRAY = Model.Generator(Matrix.NATURAL)
- (struct
- open Matrix
- let name = "MemTyped.ARRAY"
- type key = matrix
- type data = lfun * chunk list
-
- let generate (obj,ds) =
- let result = Matrix.tau obj ds in
- let lfun = Lang.generated_f ~result "Array%s_%s"
- (Matrix.id ds) (Matrix.natural_id obj) in
- let prefix = Lang.Fun.debug lfun in
- let axiom = prefix ^ "_access" in
- let xmem,ft,sigma = signature (footprint obj) in
- let xloc = Lang.freshvar ~basename:"p" t_addr in
- let loc = e_var xloc in
- let denv = Matrix.denv ds in
- let phi = e_fun lfun (loc :: denv.size_val @ List.map e_var xmem) in
- let arr = List.fold_left e_get phi denv.index_val in
- let elt = !loadrec sigma obj (shift loc obj (e_sum denv.index_offset)) in
- let lemma = p_hyps denv.index_range (p_equal arr elt) in
- let cluster = cluster_memory () in
- Definitions.define_symbol {
- d_lfun = lfun ; d_types = 0 ;
- d_params = xloc :: denv.size_var @ xmem ;
- d_definition = Logic result ;
- d_cluster = cluster ;
- } ;
- Definitions.define_lemma {
- l_assumed = true ;
- l_name = axiom ; l_types = 0 ;
- l_forall = F.p_vars lemma ;
- l_triggers = [[Trigger.of_term arr]] ;
- l_lemma = lemma ;
- l_cluster = cluster ;
- } ;
- if denv.monotonic then
- MONOTONIC.generate prefix lfun denv.size_var ft F.e_prod ;
- lfun , ft
-
- let compile = Lang.local generate
- end)
-
-(* -------------------------------------------------------------------------- *)
-(* --- Loading Elementary Values --- *)
-(* -------------------------------------------------------------------------- *)
-
-let loadvalue sigma obj l = match obj with
- | C_int i -> F.e_get (Sigma.value sigma (m_int i)) l
- | C_float f -> F.e_get (Sigma.value sigma (m_float f)) l
- | C_pointer _ -> F.e_get (Sigma.value sigma M_pointer) l
- | C_comp c ->
- let phi,cs = COMP.get c in
- e_fun phi (l :: memories sigma cs)
- | C_array a ->
- let m = Matrix.of_array a in
- let phi,cs = ARRAY.get m in
- e_fun phi ( l :: Matrix.size m @ memories sigma cs )
-
-let () = loadrec := loadvalue
-
-let load sigma obj l = Val (loadvalue sigma obj l)
-
(* -------------------------------------------------------------------------- *)
(* --- Locations --- *)
(* -------------------------------------------------------------------------- *)
@@ -1045,13 +552,12 @@ let cvar x =
let pointer_loc t = t
let pointer_val t = t
-let get_alloc sigma l = F.e_get (Sigma.value sigma T_alloc) (a_base l)
-let get_last sigma l = e_add (get_alloc sigma l) e_minus_one
+let allocated sigma l = F.e_get (Sigma.value sigma T_alloc) (a_base l)
let base_addr l = a_addr (a_base l) e_zero
let base_offset l = a_base_offset (a_offset l)
let block_length sigma obj l =
- e_fact (Ctypes.sizeof_object obj) (get_alloc sigma l)
+ e_fact (Ctypes.sizeof_object obj) (allocated sigma l)
(* -------------------------------------------------------------------------- *)
(* --- Cast --- *)
@@ -1349,99 +855,80 @@ let cast s l =
"%a" pp_mismatch s ; l
end
-let loc_of_int _ v = F.e_fun a_addr_of_int [v]
-let int_of_loc _ l = F.e_fun a_int_of_addr [l]
+let loc_of_int _ v = F.e_fun f_addr_of_int [v]
+let int_of_loc _ l = F.e_fun f_int_of_addr [l]
(* -------------------------------------------------------------------------- *)
-(* --- Updates --- *)
+(* --- Frames --- *)
(* -------------------------------------------------------------------------- *)
-let domain obj _l = footprint obj
-
-let updated s c l v =
- let m1 = Sigma.value s.pre c in
- let m2 = Sigma.value s.post c in
- [Set(m2,F.e_set m1 l v)]
-
-let havoc_range s obj l n =
- let ps = ref [] in
- Heap.Set.iter
- (fun c ->
- let basename = (Chunk.basename_of_chunk c)^"_undef" in
- let tau = Chunk.tau_of_chunk c in
- let m_undef = e_var (Lang.freshvar ~basename tau) in
- let m1 = Sigma.value s.pre c in
- let m2 = Sigma.value s.post c in
- ps := (p_equal m2 (F.e_fun f_havoc [m_undef;m1;l;n])) :: !ps
- ) (footprint obj) ; !ps
-
-let havoc s obj l = havoc_range s obj l (e_int (size_of_object obj))
-
-let eqmem s obj l =
- let ps = ref [] in
- let n = e_int (size_of_object obj) in
- Heap.Set.iter
- (fun c ->
- let m1 = Sigma.value s.pre c in
- let m2 = Sigma.value s.post c in
- if m1 != m2 then
- ps := F.p_call p_eqmem [m1;m2;l;n] :: !ps
- ) (footprint obj) ; !ps
+let frames obj addr = function
+ | T_alloc -> []
+ | m ->
+ let offset = F.e_int (length_of_object obj) in
+ let sizeof = F.e_one in
+ let tau = Chunk.val_of_chunk m in
+ let basename = Chunk.basename_of_chunk m in
+ MemMemory.frames ~addr ~offset ~sizeof ~basename tau
(* -------------------------------------------------------------------------- *)
-(* --- Copy --- *)
+(* --- Loader --- *)
(* -------------------------------------------------------------------------- *)
-let stored s obj l v =
- match obj with
- | C_int i -> updated s (m_int i) l v
- | C_float f -> updated s (m_float f) l v
- | C_pointer _ -> updated s M_pointer l v
- | C_comp _ | C_array _ ->
- Set(loadvalue s.post obj l, v) ::
- (List.map (fun p -> Assert p) (havoc s obj l))
+module MODEL =
+struct
+ module Chunk = Chunk
+ module Sigma = Sigma
+ let name = "MemTyped.LOADER"
+ type nonrec loc = loc
+ let field = field
+ let shift = shift
+ let sizeof = length_of_object
+ let domain = domain
+ let frames = frames
+ let to_addr l = l
+ let to_region_pointer l = 0,l
+ let of_region_pointer _ _ l = l
+
+ let load_int sigma i l = F.e_get (Sigma.value sigma (m_int i)) l
+ let load_float sigma f l = F.e_get (Sigma.value sigma (m_float f)) l
+ let load_pointer sigma _t l = F.e_get (Sigma.value sigma M_pointer) l
+
+ let last sigma obj l =
+ let n = length_of_object obj in
+ e_sub (F.e_div (allocated sigma l) (F.e_int n)) e_one
+
+ let havoc obj loc ~length chunk ~fresh ~current =
+ if chunk <> T_alloc then
+ let n = F.e_fact (length_of_object obj) length in
+ F.e_fun f_havoc [fresh;current;loc;n]
+ else fresh
+
+ let eqmem obj loc _chunk m1 m2 =
+ F.p_call p_eqmem [m1;m2;loc;e_int (length_of_object obj)]
+
+ let eqmem_forall obj loc _chunk m1 m2 =
+ let xp = Lang.freshvar ~basename:"p" t_addr in
+ let p = F.e_var xp in
+ let n = F.e_int (length_of_object obj) in
+ let separated = F.p_call p_separated [p;e_one;loc;n] in
+ let equal = p_equal (e_get m1 p) (e_get m2 p) in
+ [xp],separated,equal
-let copied s obj p q = stored s obj p (loadvalue s.pre obj q)
+ let updated sigma c l v = c , F.e_set (Sigma.value sigma c) l v
-(* -------------------------------------------------------------------------- *)
-(* --- Assignation --- *)
-(* -------------------------------------------------------------------------- *)
+ let store_int sigma i l v = updated sigma (m_int i) l v
+ let store_float sigma f l v = updated sigma (m_float f) l v
+ let store_pointer sigma _ty l v = updated sigma M_pointer l v
-let assigned_loc s obj l =
- match obj with
- | C_int _ | C_float _ | C_pointer _ ->
- let x = Lang.freshvar ~basename:"v" (Lang.tau_of_object obj) in
- List.map Cvalues.equation (stored s obj l (e_var x))
- | C_comp _ | C_array _ ->
- havoc s obj l
-
-let equal_loc s obj l =
- match obj with
- | C_int _ | C_float _ | C_pointer _ ->
- [p_equal (loadvalue s.pre obj l) (loadvalue s.post obj l)]
- | C_comp _ | C_array _ -> eqmem s obj l
-
-let assigned_range s obj l a b =
- let l = shift l obj a in
- let n = e_fact (size_of_object obj) (e_range a b) in
- havoc_range s obj l n
-
-let assigned s obj = function
- | Sloc l -> assigned_loc s obj l
- | Sdescr(xs,l,p) ->
- let xa = Lang.freshvar ~basename:"p" t_addr in
- let la = F.e_var xa in
- let n = F.e_int (size_of_object obj) in
- let sep = F.p_call p_separated [la;n;l;n] in
- let sep_all = F.p_forall xs (F.p_imply p sep) in
- let eq_loc = F.p_conj (equal_loc s obj la) in
- [F.p_forall [xa] (F.p_imply sep_all eq_loc)]
- | Sarray(l,obj,n) ->
- assigned_range s obj l e_zero (e_int (n-1))
- | Srange(l,obj,u,v) ->
- let a = match u with Some a -> a | None -> e_zero in
- let b = match v with Some b -> b | None -> get_last s.pre l in
- assigned_range s obj l a b
+end
+
+module LOADER = MemLoader.Make(MODEL)
+
+let load = LOADER.load
+let stored = LOADER.stored
+let copied = LOADER.copied
+let assigned = LOADER.assigned
(* -------------------------------------------------------------------------- *)
(* --- Loc Comparison --- *)
@@ -1455,11 +942,11 @@ let loc_compare f_cmp i_cmp p q =
let is_null l = p_equal l null
let loc_eq = p_equal
let loc_neq = p_neq
-let loc_lt = loc_compare a_lt p_lt
-let loc_leq = loc_compare a_leq p_leq
+let loc_lt = loc_compare p_addr_lt p_lt
+let loc_leq = loc_compare p_addr_le p_leq
let loc_diff obj p q =
let delta = e_sub (a_offset p) (a_offset q) in
- let size = e_int (size_of_object obj) in
+ let size = e_int (length_of_object obj) in
e_div delta size
(* -------------------------------------------------------------------------- *)
@@ -1475,10 +962,10 @@ let s_invalid sigma p n =
let segment phi = function
| Rloc(obj,l) ->
- phi l (e_int (size_of_object obj))
+ phi l (e_int (length_of_object obj))
| Rrange(l,obj,Some a,Some b) ->
let l = shift l obj a in
- let n = e_fact (size_of_object obj) (e_range a b) in
+ let n = e_fact (length_of_object obj) (e_range a b) in
phi l n
| Rrange(l,_,a,b) ->
Wp_parameters.abort ~current:true
@@ -1508,7 +995,7 @@ let scope seq scope xs =
(fun m x ->
let size = match scope with
| Sigs.Leave -> 0
- | Sigs.Enter -> size_of_typ x.vtype
+ | Sigs.Enter -> length_of_typ x.vtype
in F.e_set m (BASE.get x) (e_int size))
(Sigma.value seq.pre T_alloc) xs in
[ p_equal (Sigma.value seq.post T_alloc) alloc ]
@@ -1516,58 +1003,18 @@ let scope seq scope xs =
let global _sigma p = p_leq (e_fun f_region [a_base p]) e_zero
(* -------------------------------------------------------------------------- *)
-(* --- Domain --- *)
+(* --- Segments --- *)
(* -------------------------------------------------------------------------- *)
-type range =
- | LOC of term * term (* loc - size *)
- | RANGE of term * Vset.set (* base - range offset *)
+let included =
+ let addrof l = l in
+ let sizeof = length_of_object in
+ MemMemory.included ~shift ~addrof ~sizeof
-let range = function
- | Rloc(obj,l) ->
- LOC( l , e_int (size_of_object obj) )
- | Rrange(l,obj,Some a,Some b) ->
- let l = shift l obj a in
- let n = e_fact (size_of_object obj) (e_range a b) in
- LOC( l , n )
- | Rrange(l,_obj,None,None) ->
- RANGE( a_base l , Vset.range None None )
- | Rrange(l,obj,Some a,None) ->
- let se = size_of_object obj in
- RANGE( a_base l , Vset.range (Some (e_fact se a)) None )
- | Rrange(l,obj,None,Some b) ->
- let se = size_of_object obj in
- RANGE( a_base l , Vset.range None (Some (e_fact se b)) )
-
-let range_set = function
- | LOC(l,n) ->
- let a = a_offset l in
- let b = e_add a n in
- a_base l , Vset.range (Some a) (Some b)
- | RANGE(base,set) -> base , set
-
-let r_included r1 r2 =
- match r1 , r2 with
- | LOC(l1,n1) , LOC(l2,n2) ->
- p_call p_included [l1;n1;l2;n2]
- | _ ->
- let base1,set1 = range_set r1 in
- let base2,set2 = range_set r2 in
- p_if (p_equal base1 base2)
- (Vset.subset set1 set2)
- (Vset.is_empty set1)
-
-let r_disjoint r1 r2 =
- match r1 , r2 with
- | LOC(l1,n1) , LOC(l2,n2) ->
- p_call p_separated [l1;n1;l2;n2]
- | _ ->
- let base1,set1 = range_set r1 in
- let base2,set2 = range_set r2 in
- p_imply (p_equal base1 base2) (Vset.disjoint set1 set2)
-
-let included s1 s2 = r_included (range s1) (range s2)
-let separated s1 s2 = r_disjoint (range s1) (range s2)
+let separated =
+ let addrof l = l in
+ let sizeof = length_of_object in
+ MemMemory.separated ~shift ~addrof ~sizeof
(* -------------------------------------------------------------------------- *)
(* --- State Model --- *)
@@ -1584,7 +1031,7 @@ let rec lookup_a e =
and lookup_f f es =
try match RegisterShift.find f , es with
| RS_Field(fd,_) , [e] -> Mstate.field (lookup_lv e) fd
- | RS_Shift _ , [e;k] -> Mstate.index (lookup_lv e) k
+ | RS_Index _ , [e;k] -> Mstate.index (lookup_lv e) k
| _ -> raise Not_found
with Not_found when es = [] ->
Sigs.(Mvar (RegisterBASE.find f),[])
diff --git a/src/plugins/wp/MemTyped.mli b/src/plugins/wp/MemTyped.mli
index 6c23647b4fe..5bd5298918c 100644
--- a/src/plugins/wp/MemTyped.mli
+++ b/src/plugins/wp/MemTyped.mli
@@ -28,11 +28,3 @@ include Sigs.Model
type pointer = NoCast | Fits | Unsafe
val pointer : pointer Context.value
-val f_havoc : Lang.lfun
-val p_separated : Lang.lfun
-val p_included : Lang.lfun
-val p_valid_rd : Lang.lfun
-val p_valid_rw : Lang.lfun
-val p_invalid : Lang.lfun
-val a_base : Lang.F.term -> Lang.F.term
-val a_offset : Lang.F.term -> Lang.F.term
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index b4d8a304b5e..58845184bfd 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -1016,14 +1016,15 @@ struct
let eqk = p_forall (y::ys) (p_imply ek (p_equal ak bk)) in
assigned_path (eqk :: hs) xs ys ae be ofs
- let assigned_descr s xs mem x ofs p =
+ let assigned_genset s xs mem x ofs p =
let valid = valid_offset_path s.post Sigs.RW mem x ofs in
let a = get_term s.pre x in
let b = get_term s.post x in
let a_ofs = access a ofs in
let b_ofs = access b ofs in
let p_sloc = p_forall xs (p_hyps [valid;p_not p] (p_equal a_ofs b_ofs)) in
- assigned_path [p_sloc] xs [] a b ofs
+ let conds = assigned_path [p_sloc] xs [] a b ofs in
+ List.map (fun p -> Assert p) conds
(* -------------------------------------------------------------------------- *)
(* --- Assigned --- *)
@@ -1034,8 +1035,7 @@ struct
| Val((CVAL|CREF),_,[]) -> [] (* full update *)
| Val((CVAL|CREF),_,_) as vloc ->
let v = Lang.freshvar ~basename:"v" (Lang.tau_of_object obj) in
- let eqs = stored seq obj vloc (e_var v) in
- List.map Cvalues.equation eqs
+ stored seq obj vloc (e_var v)
| Val((HEAP|CTXT|CARR) as m,x,ofs) ->
M.assigned (mseq_of_seq seq) obj (Sloc (mloc_of_path m x ofs))
| Loc l ->
@@ -1048,8 +1048,7 @@ struct
| Val((CVAL|CREF),_,_) as vloc ->
let te = Lang.tau_of_object elt in
let v = Lang.freshvar ~basename:"v" Qed.Logic.(Array(Int,te)) in
- let eqs = stored seq obj vloc (e_var v) in
- List.map Cvalues.equation eqs
+ stored seq obj vloc (e_var v)
| Val((HEAP|CTXT|CARR) as m,x,ofs) ->
let l = mloc_of_path m x ofs in
M.assigned (mseq_of_seq seq) obj (Sarray(l,elt,n))
@@ -1067,7 +1066,7 @@ struct
let k = Lang.freshvar ~basename:"k" Qed.Logic.Int in
let p = Vset.in_range (e_var k) a b in
let ofs = ofs_shift elt (e_var k) ofs in
- assigned_descr seq [k] m x ofs p
+ assigned_genset seq [k] m x ofs p
let assigned_descr seq obj xs l p =
match l with
@@ -1077,7 +1076,7 @@ struct
| Val((HEAP|CTXT|CARR) as m,x,ofs) ->
M.assigned (mseq_of_seq seq) obj (Sdescr(xs,mloc_of_path m x ofs,p))
| Val((CVAL|CREF) as m,x,ofs) ->
- assigned_descr seq xs m x ofs p
+ assigned_genset seq xs m x ofs p
let assigned seq obj = function
| Sloc l -> assigned_loc seq obj l
diff --git a/src/plugins/wp/Sigs.ml b/src/plugins/wp/Sigs.ml
index a91e7770466..add077d6028 100644
--- a/src/plugins/wp/Sigs.ml
+++ b/src/plugins/wp/Sigs.ml
@@ -434,7 +434,7 @@ sig
location [loc] which is represented by [t] in [sigma.post].
*)
- val assigned : sigma sequence -> c_object -> loc sloc -> pred list
+ val assigned : sigma sequence -> c_object -> loc sloc -> equation list
(**
Return a set of formula that express that two memory state are the same
except at the given set of memory location.
diff --git a/src/plugins/wp/TacHavoc.ml b/src/plugins/wp/TacHavoc.ml
index 9b7034cc308..9e68996a899 100644
--- a/src/plugins/wp/TacHavoc.ml
+++ b/src/plugins/wp/TacHavoc.ml
@@ -35,7 +35,7 @@ let lookup_havoc e =
| L.Aget( m , p ) ->
begin
match F.repr m with
- | L.Fun( f , [mr;m0;a;n] ) when f == MemTyped.f_havoc ->
+ | L.Fun( f , [mr;m0;a;n] ) when f == MemMemory.f_havoc ->
Some( mr , m0 , a , n , p )
| _ -> None
end
@@ -55,7 +55,7 @@ class havoc =
| None -> Not_applicable
| Some(mr,m0,a,n,p) ->
let separated =
- F.p_call MemTyped.p_separated
+ F.p_call MemMemory.p_separated
[ p ; F.e_int 1 ; a ; n ] in
let process = Tactical.rewrite ?at [
"Unassigned" , separated , e , F.e_get m0 p ;
@@ -70,11 +70,11 @@ class havoc =
let separated ?at property =
match F.e_expr property with
- | L.Fun( f , [p;n;q;m] ) when f == MemTyped.p_separated ->
- let base_p = MemTyped.a_base p in
- let ofs_p = MemTyped.a_offset p in
- let base_q = MemTyped.a_base q in
- let ofs_q = MemTyped.a_offset q in
+ | L.Fun( f , [p;n;q;m] ) when f == MemMemory.p_separated ->
+ let base_p = MemMemory.a_base p in
+ let ofs_p = MemMemory.a_offset p in
+ let base_q = MemMemory.a_base q in
+ let ofs_q = MemMemory.a_offset q in
let eq_base = F.p_equal base_p base_q in
let on_left = F.p_leq (F.e_add ofs_p n) ofs_q in
let on_right = F.p_leq (F.e_add ofs_q m) ofs_p in
@@ -110,8 +110,8 @@ class separated =
(* -------------------------------------------------------------------------- *)
let invalid m p n =
- let base = MemTyped.a_base p in
- let offset = MemTyped.a_offset p in
+ let base = MemMemory.a_base p in
+ let offset = MemMemory.a_offset p in
let malloc = F.e_get m base in
"Invalid",
F.p_imply
@@ -121,8 +121,8 @@ let invalid m p n =
(F.p_leq (F.e_add offset n) F.e_zero))
let valid_rd m p n =
- let base = MemTyped.a_base p in
- let offset = MemTyped.a_offset p in
+ let base = MemMemory.a_base p in
+ let offset = MemMemory.a_offset p in
let malloc = F.e_get m base in
"Valid (Read)",
F.p_imply
@@ -132,8 +132,8 @@ let valid_rd m p n =
(F.p_leq (F.e_add offset n) malloc))
let valid_rw m p n =
- let base = MemTyped.a_base p in
- let offset = MemTyped.a_offset p in
+ let base = MemMemory.a_base p in
+ let offset = MemMemory.a_offset p in
let malloc = F.e_get m base in
"Valid (Read & Write)",
F.p_imply
@@ -145,10 +145,10 @@ let valid_rw m p n =
])
let included p a q b =
- let p_base = MemTyped.a_base p in
- let q_base = MemTyped.a_base q in
- let p_offset = MemTyped.a_offset p in
- let q_offset = MemTyped.a_offset q in
+ let p_base = MemMemory.a_base p in
+ let q_base = MemMemory.a_base q in
+ let p_offset = MemMemory.a_offset p in
+ let q_offset = MemMemory.a_offset q in
"Included",
F.p_imply
(F.p_lt F.e_zero a)
@@ -161,10 +161,10 @@ let included p a q b =
]))
let lookup f = function
- | [p;a;q;b] when f == MemTyped.p_included -> included p a q b
- | [m;p;n] when f == MemTyped.p_invalid -> invalid m p n
- | [m;p;n] when f == MemTyped.p_valid_rd -> valid_rd m p n
- | [m;p;n] when f == MemTyped.p_valid_rw -> valid_rw m p n
+ | [p;a;q;b] when f == MemMemory.p_included -> included p a q b
+ | [m;p;n] when f == MemMemory.p_invalid -> invalid m p n
+ | [m;p;n] when f == MemMemory.p_valid_rd -> valid_rd m p n
+ | [m;p;n] when f == MemMemory.p_valid_rw -> valid_rw m p n
| _ -> raise Not_found
let unfold ?at e f es =
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
index 9cf4378ece6..feda6936719 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
@@ -66,17 +66,17 @@ theory Compound
not q = p -> Load_S2_A p (set mint q v) = Load_S2_A p mint
axiom Q_Load_S2_A_eqmem_Mint :
- forall mint:addr -> int, mint1:addr -> int, k:int, p:addr, q:addr
- [eqmem mint mint1 q k, Load_S2_A p mint| eqmem mint mint1 q k,
- Load_S2_A p mint1].
- included p 1 q k ->
- eqmem mint mint1 q k -> Load_S2_A p mint1 = Load_S2_A p mint
+ forall mint:addr -> int, mint1:addr -> int, n:int, p:addr, q:addr
+ [Load_S2_A p mint, eqmem mint mint1 q n| Load_S2_A p mint1,
+ eqmem mint mint1 q n].
+ included p 1 q n ->
+ eqmem mint mint1 q n -> Load_S2_A p mint1 = Load_S2_A p mint
axiom Q_Load_S2_A_havoc_Mint :
- forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, k:int, p:
- addr, q:addr [Load_S2_A p mint| Load_S2_A p mint1].
- havoc mint2 mint q k = mint1 ->
- separated p 1 q k -> Load_S2_A p mint1 = Load_S2_A p mint
+ forall mint:addr -> int, mint1:addr -> int, n:int, p:addr, q:addr
+ [Load_S2_A p (havoc mint1 mint q n)].
+ separated p 1 q n ->
+ Load_S2_A p (havoc mint1 mint q n) = Load_S2_A p mint
end
[wp:print-generated]
theory WP
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
index 63ef86ba980..747410102e8 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
@@ -118,7 +118,7 @@ eq_string 11 4 (52..64) 15 100%
hash 6 1 (12..24) 7 100%
size 2 - 2 100%
init 8 5 (80..104) 13 100%
-add 24 15 (208..256) 39 100%
+add 24 15 (224..272) 39 100%
mem_binding 18 8 (800..896) 26 100%
-------------------------------------------------------------
[wp] Running WP plugin...
@@ -283,6 +283,6 @@ eq_string 11 7 (56..80) 18 100%
hash 7 3 (44..56) 10 100%
size 2 1 (16..28) 3 100%
init 10 8 (88..112) 18 100%
-add 30 24 (208..256) 54 100%
+add 30 24 (224..272) 54 100%
mem_binding 25 15 (800..896) 40 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
index 9acab6dd84f..7095462df43 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
@@ -6,7 +6,7 @@
[wp:print-generated]
"WPOUT/typed/Compound.v"
(* ---------------------------------------------------------- *)
- (* --- Memory Compound Updates --- *)
+ (* --- Memory Compound Loader --- *)
(* ---------------------------------------------------------- *)
Require Import ZArith.
diff --git a/src/plugins/wp/why3_api.ml b/src/plugins/wp/why3_api.ml
index 1d4c70adb63..73df3e4c6a8 100644
--- a/src/plugins/wp/why3_api.ml
+++ b/src/plugins/wp/why3_api.ml
@@ -450,7 +450,8 @@ let rec of_term ~cnv expected t : Why3.Term.term =
in
match lfun_name f, expected with
| F_call s, _ -> apply_from_ns' s l sort
- | Qed.Engine.F_subst _, _ -> Wp_parameters.not_yet_implemented "lfun with subst"
+ | Qed.Engine.F_subst _, _ ->
+ raise (Invalid_argument "Can not export 'F_subst' pattern to why-3")
| Qed.Engine.F_left s, _ | Qed.Engine.F_assoc s, _ ->
let rec aux = function
| [] -> Wp_parameters.fatal "Empty application"
--
GitLab