From cfe2a65d6f5bf9e1c5019cf9f0fd0497aee9e640 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 30 Sep 2020 10:55:35 +0200
Subject: [PATCH] [wp] Hypotheses to validate at post
---
src/plugins/wp/MemoryContext.ml | 104 +++++++++++++++++++++++---------
1 file changed, 76 insertions(+), 28 deletions(-)
diff --git a/src/plugins/wp/MemoryContext.ml b/src/plugins/wp/MemoryContext.ml
index b3012f74718..2a410dec83e 100644
--- a/src/plugins/wp/MemoryContext.ml
+++ b/src/plugins/wp/MemoryContext.ml
@@ -50,6 +50,7 @@ type partition = {
globals : zone list ; (* [ &G , G[...], ... ] *)
to_heap : zone list ; (* [ p, ... ] *)
context : zone list ; (* [ p+(..), ... ] *)
+ by_addr : zone list ;
}
(* -------------------------------------------------------------------------- *)
@@ -60,12 +61,13 @@ let empty = {
globals = [] ;
context = [] ;
to_heap = [] ;
+ by_addr = [] ;
}
let set x p w =
match p with
| NotUsed -> w
- | ByAddr -> w
+ | ByAddr -> { w with by_addr = Var x :: w.by_addr }
| ByRef | InContext ->
if Cil.isFunctionType x.vtype then w else
{ w with context = Ptr x :: w.context }
@@ -192,6 +194,10 @@ let global_zones partition =
let context_zones partition =
List.map (fun z -> [z]) partition.context
+let addr_of_zones partition =
+ let comp a b = Cil_datatype.Typ.compare (type_of_zone a) (type_of_zone b) in
+ List.sort comp partition.by_addr
+
let heap_zones partition =
let comp a b = Cil_datatype.Typ.compare (type_of_zone a) (type_of_zone b) in
List.sort comp partition.to_heap
@@ -199,7 +205,7 @@ let heap_zones partition =
(* Note that this function does not return separated zone lists, but well-typed
zone lists.
*)
-let heaps partition =
+let well_type_zones zone_function partition =
let rec partition_by_type t acc l =
match l, acc with
| [], _ ->
@@ -211,7 +217,9 @@ let heaps partition =
| x :: l, acc ->
partition_by_type (type_of_zone x) ([x] :: acc) l
in
- partition_by_type Cil.voidType [] (heap_zones partition)
+ partition_by_type Cil.voidType [] (zone_function partition)
+
+let heaps = well_type_zones heap_zones
let main_separation loc globals context heaps =
match heaps, context with
@@ -232,16 +240,11 @@ let assigned_locations kf filter =
let add_from l (e, _ds) =
if filter e.it_content then e :: l else l
in
- let add_assign kf _emitter assigns l = match assigns with
- | WritesAny ->
- Wp_parameters.warning
- ~wkey:Wp_parameters.wkey_imprecise_hypotheses_assigns ~once:true
- "No assigns for function '%a', model hypotheses will be imprecise"
- Kernel_function.pretty kf ;
- l
+ let add_assign _emitter assigns l = match assigns with
+ | WritesAny -> l
| Writes froms -> List.fold_left add_from l froms
in
- Annotations.fold_assigns (add_assign kf) kf Cil.default_behavior_name []
+ Annotations.fold_assigns add_assign kf Cil.default_behavior_name []
let assigned_via_pointers kf =
let rec assigned_via_pointer t =
@@ -260,24 +263,67 @@ let assigned_via_pointers kf =
in
assigned_locations kf assigned_via_pointer
+let post_term t =
+ let exception Post_value in
+ let v = object
+ inherit Cil.nopCilVisitor
+ method! vlogic_label = function
+ | BuiltinLabel(Post) -> raise Post_value
+ | _ -> Cil.SkipChildren
+ method! vterm_lval = function
+ | TResult _, _ -> raise Post_value
+ | _ -> Cil.DoChildren
+ end in
+ try ignore (Cil.visitCilTerm v t) ; false
+ with Post_value -> true
+
+let simpl_pred_list l =
+ List.sort_uniq Logic_utils.compare_predicate
+ (List.filter (fun p -> not(Logic_utils.is_trivially_true p)) l)
+
let clauses_of_partition kf loc p =
let globals = global_zones p in
let main_sep =
main_separation loc globals (context_zones p) (heaps p)
in
- let assigns_sep =
+ let assigns_sep_req, assigns_sep_ens =
let addr_of t = addr_of_lval ~loc t.it_content in
- List.map
- (fun t -> term_separated_from_regions loc (addr_of t) globals)
- (assigned_via_pointers kf)
+ let folder (req, ens) t =
+ let sep = term_separated_from_regions loc (addr_of t) globals in
+ if post_term t.it_content then (req, sep :: ens) else (sep :: req, ens)
+ in
+ List.fold_left folder ([],[]) (assigned_via_pointers kf)
+ in
+ let context_validity = List.map (valid_region loc) (context_zones p) in
+ let reqs = main_sep @ assigns_sep_req @ context_validity in
+ let reqs = simpl_pred_list reqs in
+ let ens = simpl_pred_list assigns_sep_ens in
+ reqs, ens
+
+let addr_of_vars = well_type_zones addr_of_zones
+
+let ptr_or_ptr_set { term_type = t } =
+ let open Logic_typing in
+ is_pointer_type t || (is_set_type t && is_pointer_type (type_of_element t))
+
+let escaping_formals kf loc p =
+ let ret_t = Kernel_function.get_return_type kf in
+ let addr_of t = addr_of_lval ~loc t.it_content in
+ let asgnd_ptrs =
+ Extlib.filter_map
+ (* Search assigned pointers via a pointer,
+ e.g. 'assigns *p ;' with '*p' of type pointer or set of pointers *)
+ (fun t -> ptr_or_ptr_set t.it_content) addr_of (assigned_via_pointers kf)
in
- let context_validity =
- List.map (valid_region loc) (context_zones p)
+ let asgnd_ptrs =
+ if Cil.isPointerType ret_t then tresult ~loc ret_t :: asgnd_ptrs
+ else asgnd_ptrs
in
- let reqs = main_sep @ assigns_sep @ context_validity in
- let reqs = List.filter (fun p -> not(Logic_utils.is_trivially_true p)) reqs in
- let reqs = List.sort_uniq Logic_utils.compare_predicate reqs in
- reqs
+ let local_zone = function Var v -> v.vformal | _ -> false in
+ let local_partition = { p with by_addr = List.filter local_zone p.by_addr } in
+ let locals = addr_of_vars local_partition in
+ simpl_pred_list
+ (List.map (fun t -> term_separated_from_regions loc t locals) asgnd_ptrs)
module Table =
State_builder.Hashtbl
@@ -292,16 +338,18 @@ module Table =
let compute_behavior kf name hypotheses_computer =
let partition = hypotheses_computer kf in
let loc = Kernel_function.get_location kf in
- let reqs = clauses_of_partition kf loc partition in
- let reqs = List.map Logic_const.new_predicate reqs in
- match reqs with
- | [] -> None
- | l1 ->
+ let reqs, ens = clauses_of_partition kf loc partition in
+ let ens = escaping_formals kf loc partition @ ens in
+ let reqs = List.map new_predicate reqs in
+ let ens = List.map (fun p -> Normal, new_predicate p) ens in
+ match reqs, ens with
+ | [], [] -> None
+ | reqs, ens ->
Some {
b_name = name ;
- b_requires = l1 ;
+ b_requires = reqs ;
b_assumes = [] ;
- b_post_cond = [] ;
+ b_post_cond = ens ;
b_assigns = WritesAny ;
b_allocation = FreeAllocAny ;
b_extended = []
--
GitLab