From 33c4faca8f32f343b3c252b067dd04a8f79097c2 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 15 Feb 2021 17:13:08 +0100
Subject: [PATCH] [wp] Dispatch nullable in Factory
---
src/plugins/wp/Factory.ml | 15 +++++++++++----
src/plugins/wp/MemVar.ml | 14 +++++++-------
src/plugins/wp/MemoryContext.ml | 32 +++++++++++++++++++++++++-------
src/plugins/wp/MemoryContext.mli | 4 +++-
4 files changed, 46 insertions(+), 19 deletions(-)
diff --git a/src/plugins/wp/Factory.ml b/src/plugins/wp/Factory.ml
index cdb4593efb4..f35c4a52596 100644
--- a/src/plugins/wp/Factory.ml
+++ b/src/plugins/wp/Factory.ml
@@ -111,6 +111,10 @@ module type Proxy = sig
(Cil_types.varinfo -> unit) -> unit
end
+let nullable_status x =
+ if RefUsage.is_nullable x then MemoryContext.Nullable
+ else Valid
+
module MakeVarUsage(V : Proxy) : MemVar.VarUsage =
struct
let datatype = "VarUsage." ^ V.datatype
@@ -124,7 +128,7 @@ struct
let module S = Datatype.String.Set in
let open MemoryContext in
if S.mem x.vname (get_addr ()) then ByAddr else
- if S.mem x.vname (get_ctxt ()) then InContext else
+ if S.mem x.vname (get_ctxt ()) then InContext (nullable_status x) else
if S.mem x.vname (get_refs ()) then ByRef else
if S.mem x.vname (get_vars ()) then ByValue else
V.param x
@@ -182,16 +186,19 @@ let refusage_param ~byref ~context x =
| RefUsage.NoAccess -> MemoryContext.NotUsed
| RefUsage.ByAddr -> MemoryContext.ByAddr
| RefUsage.ByValue ->
- if context && is_formal_ptr x then MemoryContext.InContext
+ if context && is_formal_ptr x then
+ MemoryContext.InContext (nullable_status x)
else if is_ptr x && not (is_fun_ptr x) then MemoryContext.ByShift
else MemoryContext.ByValue
| RefUsage.ByRef ->
if byref
- then MemoryContext.ByRef
+ then
+ if RefUsage.is_nullable x then MemoryContext.InContext Nullable
+ else MemoryContext.ByRef
else MemoryContext.ByValue
| RefUsage.ByArray ->
if context && is_formal_ptr x
- then MemoryContext.InArray
+ then MemoryContext.InArray (nullable_status x)
else MemoryContext.ByShift
let refusage_iter ?kf ~init f = RefUsage.iter ?kf ~init (fun x _usage -> f x)
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index 2776f437fd7..70e14713b79 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -104,7 +104,7 @@ struct
match V.param x with
| ByRef ->
"ra_" ^ LogicUsage.basename x
- | NotUsed | ByValue | ByShift | ByAddr | InContext | InArray ->
+ | NotUsed | ByValue | ByShift | ByAddr | InContext _ | InArray _ ->
"ta_" ^ LogicUsage.basename x
let is_framed = is_framed_var
end
@@ -600,7 +600,7 @@ struct
let pp_var_model fmt = function
| ByValue | ByShift | NotUsed -> Format.pp_print_string fmt "non-aliased" (* cf. -wp-unalias-vars *)
| ByRef -> Format.pp_print_string fmt "by reference" (* cf. -wp-ref-vars *)
- | InContext | InArray -> Format.pp_print_string fmt "in an isolated context" (* cf. -wp-context-vars *)
+ | InContext _ | InArray _ -> Format.pp_print_string fmt "in an isolated context" (* cf. -wp-context-vars *)
| ByAddr -> Format.pp_print_string fmt "aliased" (* cf. -wp-alias-vars *)
let pretty fmt = function
@@ -631,7 +631,7 @@ struct
let cvar x = match V.param x with
| NotUsed | ByValue | ByShift -> Val(CVAL,x,[])
| ByAddr -> Val(HEAP,x,[])
- | InContext | InArray | ByRef -> Ref x
+ | InContext _ | InArray _ | ByRef -> Ref x
(* -------------------------------------------------------------------------- *)
(* --- Lifting --- *)
@@ -730,9 +730,9 @@ struct
let load sigma obj = function
| Ref x ->
begin match V.param x with
- | ByRef -> Sigs.Loc(Val(CREF,x,[]))
- | InContext -> Sigs.Loc(Val(CTXT,x,[]))
- | InArray -> Sigs.Loc(Val(CARR,x,[]))
+ | ByRef -> Sigs.Loc(Val(CREF,x,[]))
+ | InContext _ -> Sigs.Loc(Val(CTXT,x,[]))
+ | InArray _ -> Sigs.Loc(Val(CARR,x,[]))
| NotUsed | ByAddr | ByValue | ByShift -> assert false
end
| Val((CREF|CVAL),x,ofs) ->
@@ -1180,7 +1180,7 @@ struct
let is_mvar_alloc x =
match V.param x with
- | ByRef | InContext | InArray | NotUsed -> false
+ | ByRef | InContext _ | InArray _ | NotUsed -> false
| ByValue | ByShift | ByAddr -> true
let alloc sigma xs =
diff --git a/src/plugins/wp/MemoryContext.ml b/src/plugins/wp/MemoryContext.ml
index e337a196331..fcdb60c025d 100644
--- a/src/plugins/wp/MemoryContext.ml
+++ b/src/plugins/wp/MemoryContext.ml
@@ -24,16 +24,23 @@
(* --- Variable Partitionning --- *)
(* -------------------------------------------------------------------------- *)
-type param = NotUsed | ByAddr | ByValue | ByShift | ByRef | InContext | InArray
+type validity = Valid | Nullable
+type param =
+ | NotUsed | ByAddr | ByValue | ByShift | ByRef
+ | InContext of validity | InArray of validity
+
+let nullable_string = function
+ | Valid -> ""
+ | Nullable -> "(nullable)"
let pp_param fmt = function
| NotUsed -> Format.pp_print_string fmt "not used"
| ByAddr -> Format.pp_print_string fmt "in heap"
| ByValue -> Format.pp_print_string fmt "by value"
| ByShift -> Format.pp_print_string fmt "by value with shift"
- | ByRef -> Format.pp_print_string fmt "by ref."
- | InContext -> Format.pp_print_string fmt "in context"
- | InArray -> Format.pp_print_string fmt "in array"
+ | ByRef -> Format.pp_print_string fmt "by ref"
+ | InContext n -> Format.pp_print_string fmt ("in context" ^ nullable_string n)
+ | InArray n -> Format.pp_print_string fmt ("in array" ^ nullable_string n)
(* -------------------------------------------------------------------------- *)
(* --- Separation Hypotheses --- *)
@@ -50,6 +57,7 @@ type partition = {
globals : zone list ; (* [ &G , G[...], ... ] *)
to_heap : zone list ; (* [ p, ... ] *)
context : zone list ; (* [ p+(..), ... ] *)
+ nullable : zone list ; (* [ p+(..), ... ] but can be NULL *)
by_addr : zone list ; (* [ &(x + ..), ... ] *)
}
@@ -60,6 +68,7 @@ type partition = {
let empty = {
globals = [] ;
context = [] ;
+ nullable = [] ;
to_heap = [] ;
by_addr = [] ;
}
@@ -68,12 +77,21 @@ let set x p w =
match p with
| NotUsed -> w
| ByAddr -> { w with by_addr = Var x :: w.by_addr }
- | ByRef | InContext ->
+ | ByRef ->
if Cil.isFunctionType x.vtype then w else
{ w with context = Ptr x :: w.context }
- | InArray ->
+ | InContext v ->
+ if Cil.isFunctionType x.vtype then w else
+ begin match v with
+ | Nullable -> { w with nullable = Ptr x :: w.nullable }
+ | Valid -> { w with context = Ptr x :: w.context }
+ end
+ | InArray v ->
if Cil.isFunctionType x.vtype then w else
- { w with context = Arr x :: w.context }
+ begin match v with
+ | Nullable -> { w with nullable = Arr x :: w.nullable }
+ | Valid -> { w with context = Arr x :: w.context }
+ end
| ByValue | ByShift ->
if x.vghost then w else
if Cil.isFunctionType x.vtype then w else
diff --git a/src/plugins/wp/MemoryContext.mli b/src/plugins/wp/MemoryContext.mli
index c0698fa9ea1..9cf4ea56bfc 100644
--- a/src/plugins/wp/MemoryContext.mli
+++ b/src/plugins/wp/MemoryContext.mli
@@ -22,7 +22,9 @@
open Cil_types
-type param = NotUsed | ByAddr | ByValue | ByShift | ByRef | InContext | InArray
+type validity = Valid | Nullable
+type param = NotUsed | ByAddr | ByValue | ByShift | ByRef
+ | InContext of validity | InArray of validity
val pp_param: Format.formatter -> param -> unit
--
GitLab