From cae15f7b46791c904cf577223ec8a1562a2a3ef5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 4 Oct 2024 13:38:12 +0200
Subject: [PATCH] [wp/region] refactor functor signatures
---
src/plugins/wp/Factory.ml | 42 ++---
src/plugins/wp/MemRegion.ml | 37 ++++-
src/plugins/wp/MemRegion.mli | 37 ++++-
src/plugins/wp/RegionAnalysis.ml | 267 +++++++++++-------------------
src/plugins/wp/RegionAnalysis.mli | 40 +----
5 files changed, 185 insertions(+), 238 deletions(-)
diff --git a/src/plugins/wp/Factory.ml b/src/plugins/wp/Factory.ml
index 2b5fa1ebb62..22804c75a39 100644
--- a/src/plugins/wp/Factory.ml
+++ b/src/plugins/wp/Factory.ml
@@ -193,6 +193,10 @@ struct
let iter = refusage_iter
end
+module Static = MemVar.Static
+module MemRegion = MemRegion.Make(RegionAnalysis)(MemBytes)
+module MemEva = MemVal.Make(MemVal.Eva)
+
(* -------------------------------------------------------------------------- *)
(* --- Generator & Model --- *)
(* -------------------------------------------------------------------------- *)
@@ -200,20 +204,17 @@ end
(* Each model must be instanciated statically because of registered memory
models identifiers and Frama-C states *)
-module Register(V : MemVar.VarUsage)(M : Sigs.Model)
+module MakeVar(V : MemVar.VarUsage)(M : Sigs.Model)
= MemVar.Make(MakeVarUsage(V))(M)
-
-module Model_Hoare_Raw = Register(MemVar.Raw)(MemEmpty)
-module Model_Hoare_Ref = Register(Ref)(MemEmpty)
-
-module Model_Typed_Var = Register(Var)(MemTyped)
-module Model_Typed_Ref = Register(Ref)(MemTyped)
-module Model_Bytes_Var = Register(Var)(MemBytes)
-module Model_Bytes_Ref = Register(Ref)(MemBytes)
-module Model_Caveat = Register(Caveat)(MemTyped)
-
-module MemVal = MemVal.Make(MemVal.Eva)
+module Model_Hoare_Raw = MakeVar(MemVar.Raw)(MemEmpty)
+module Model_Hoare_Ref = MakeVar(Ref)(MemEmpty)
+module Model_Typed_Var = MakeVar(Var)(MemTyped)
+module Model_Typed_Ref = MakeVar(Ref)(MemTyped)
+module Model_Bytes_Var = MakeVar(Var)(MemBytes)
+module Model_Bytes_Ref = MakeVar(Ref)(MemBytes)
+module Model_Caveat = MakeVar(Caveat)(MemTyped)
+module Model_Region = MakeVar(Static)(MemRegion)
module MakeCompiler(M:Sigs.Model) =
struct
@@ -223,7 +224,6 @@ struct
module A = LogicAssigns.Make(M)(L)
end
-
module Comp_MemZeroAlias = MakeCompiler(MemZeroAlias)
module Comp_Hoare_Raw = MakeCompiler(Model_Hoare_Raw)
@@ -232,20 +232,12 @@ module Comp_Hoare_Ref = MakeCompiler(Model_Hoare_Ref)
module Comp_MemTyped = MakeCompiler(MemTyped)
module Comp_Typed_Var = MakeCompiler(Model_Typed_Var)
module Comp_Typed_Ref = MakeCompiler(Model_Typed_Ref)
-
module Comp_Caveat = MakeCompiler(Model_Caveat)
-
module Comp_MemBytes = MakeCompiler(MemBytes)
module Comp_Bytes_Var = MakeCompiler(Model_Bytes_Var)
module Comp_Bytes_Ref = MakeCompiler(Model_Bytes_Ref)
-
-module Comp_MemVal = MakeCompiler(MemVal)
-module Comp_Region =
- MakeCompiler
- (MemVar.Make
- (MemVar.Static)
- (MemRegion.Make(RegionAnalysis.R)(MemBytes)))
-
+module Comp_Region = MakeCompiler(Model_Region)
+module Comp_MemEva = MakeCompiler(MemEva)
let compiler mheap mvar : (module Sigs.Compiler) =
match mheap , mvar with
@@ -256,7 +248,7 @@ let compiler mheap mvar : (module Sigs.Compiler) =
| Typed _ , Raw -> (module Comp_MemTyped)
| Typed _ , Var -> (module Comp_Typed_Var)
| Typed _ , Ref -> (module Comp_Typed_Ref)
- | Eva, _ -> (module Comp_MemVal)
+ | Eva, _ -> (module Comp_MemEva)
| Bytes, Raw -> (module Comp_MemBytes)
| Bytes, Var -> (module Comp_Bytes_Var)
| Bytes, Ref -> (module Comp_Bytes_Ref)
@@ -269,7 +261,7 @@ let compiler mheap mvar : (module Sigs.Compiler) =
let configure_mheap = function
| Hoare -> MemEmpty.configure ()
| ZeroAlias -> MemZeroAlias.configure ()
- | Eva -> MemVal.configure ()
+ | Eva -> MemEva.configure ()
| Bytes -> MemBytes.configure ()
| Typed p ->
let rollback_memtyped = MemTyped.configure () in
diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml
index a4a7a81650b..321b1d90c35 100644
--- a/src/plugins/wp/MemRegion.ml
+++ b/src/plugins/wp/MemRegion.ml
@@ -33,6 +33,41 @@ open MemMemory
module L = Qed.Logic
+module type RegionProxy =
+sig
+ type region
+ val null : unit -> region
+
+ val hash : region -> int
+ val equal : region -> region -> bool
+ val compare : region -> region -> int
+ val pretty : Format.formatter -> region -> unit
+
+ type primitive = | Int of c_int | Float of c_float | Ptr
+ type kind = Single of primitive | Many of primitive | Garbled
+ val kind : region -> kind
+ val pp_kind : Format.formatter -> kind -> unit
+
+ val tau_of_region : region -> tau
+ val points_to : region -> region option
+
+ val separated : region -> region -> bool
+ val included : region -> region -> bool
+
+ val cvar : varinfo -> region option
+ val field : region -> fieldinfo -> region option
+ val shift : region -> c_object -> term -> region option
+ val base_addr : region -> region
+
+ val literal : eid:int -> Cstring.cst -> region option
+ val pointer_loc : unit -> region option
+ val loc_of_int : unit -> region option
+
+ val id_of_region : region -> int
+ val region_of_id : int -> region option
+
+end
+
module type ModelWithLoader = sig
include Sigs.Model
@@ -62,7 +97,7 @@ module type ModelWithLoader = sig
val init_footprint : c_object -> loc -> Sigma.domain
end
-module Make (R:RegionAnalysis.API) (M:ModelWithLoader) (* : Sigs.Model *) =
+module Make (R:RegionProxy) (M:ModelWithLoader) : Sigs.Model =
struct
type region = R.region
diff --git a/src/plugins/wp/MemRegion.mli b/src/plugins/wp/MemRegion.mli
index 79038b5d194..43dbc77001c 100644
--- a/src/plugins/wp/MemRegion.mli
+++ b/src/plugins/wp/MemRegion.mli
@@ -29,6 +29,41 @@ open Sigs
(* --- Region Memory Model --- *)
(* -------------------------------------------------------------------------- *)
+module type RegionProxy =
+sig
+ type region
+ val null : unit -> region
+
+ val hash : region -> int
+ val equal : region -> region -> bool
+ val compare : region -> region -> int
+ val pretty : Format.formatter -> region -> unit
+
+ type primitive = | Int of c_int | Float of c_float | Ptr
+ type kind = Single of primitive | Many of primitive | Garbled
+ val kind : region -> kind
+ val pp_kind : Format.formatter -> kind -> unit
+
+ val tau_of_region : region -> tau
+ val points_to : region -> region option
+
+ val separated : region -> region -> bool
+ val included : region -> region -> bool
+
+ val cvar : varinfo -> region option
+ val field : region -> fieldinfo -> region option
+ val shift : region -> c_object -> term -> region option
+ val base_addr : region -> region
+
+ val literal : eid:int -> Cstring.cst -> region option
+ val pointer_loc : unit -> region option
+ val loc_of_int : unit -> region option
+
+ val id_of_region : region -> int
+ val region_of_id : int -> region option
+
+end
+
module type ModelWithLoader =
sig
include Sigs.Model
@@ -59,4 +94,4 @@ sig
val init_footprint : c_object -> loc -> domain
end
-module Make : RegionAnalysis.API -> ModelWithLoader -> Sigs.Model
+module Make : RegionProxy -> ModelWithLoader -> Sigs.Model
diff --git a/src/plugins/wp/RegionAnalysis.ml b/src/plugins/wp/RegionAnalysis.ml
index cb4b7e03ab2..355fc677b96 100644
--- a/src/plugins/wp/RegionAnalysis.ml
+++ b/src/plugins/wp/RegionAnalysis.ml
@@ -24,201 +24,124 @@ open Cil_types
open Ctypes
open Lang.F
+type region = Region.node
-(* -------------------------------------------------------------------------- *)
-(* --- Region Analysis API for Region Memory Model --- *)
-(* -------------------------------------------------------------------------- *)
+let get_map () = match WpContext.get_scope () with
+ | WpContext.Kf f -> Region.map f
+ | WpContext.Global -> Wp_parameters.not_yet_implemented "[WP/RegionAnalysis.ml] get_map: No global region analysis yet"
-module type API = sig
- type region
- val null : unit -> region
+let null () : region =
+ Warning.emit ~severe:false ~source:"Region Memory Model"
+ ~effect:"Create null pointer value" "NULL" ;
+ Wp_parameters.not_yet_implemented "[WP/RegionAnalysis.ml] null: cannot create null region"
+let id_of_region region = Region.uid (get_map ()) region
- val hash : region -> int
- val equal : region -> region -> bool
- val compare : region -> region -> int
- val pretty : Format.formatter -> region -> unit
+let region_of_id id =
+ try Some (Region.find (get_map ()) id)
+ with Not_found -> None
- type primitive = | Int of c_int | Float of c_float | Ptr
- type kind = Single of primitive | Many of primitive | Garbled
- val kind : region -> kind
- val pp_kind : Format.formatter -> kind -> unit
+let hash = Region.id
- val tau_of_region : region -> tau
- val points_to : region -> region option
+let equal r1 r2 = (Region.id r1 = Region.id r2)
- val separated : region -> region -> bool
- val included : region -> region -> bool
+let compare r1 r2 = Int.compare (Region.id r1) (Region.id r2)
- val cvar : varinfo -> region option
- val field : region -> fieldinfo -> region option
- val shift : region -> c_object -> term -> region option
- val base_addr : region -> region
+let pretty fmt r = Format.fprintf fmt "R%03d" @@ Region.id r
- val literal : eid:int -> Cstring.cst -> region option
- val pointer_loc : unit -> region option
- val loc_of_int : unit -> region option
+type primitive = | Int of c_int | Float of c_float | Ptr
+type kind = Single of primitive | Many of primitive | Garbled
- val id_of_region : region -> int
- val region_of_id : int -> region option
-end
+let pp_primitive fmt = function
+ | Int i -> Ctypes.pp_int fmt i
+ | Float f -> Ctypes.pp_float fmt f
+ | Ptr -> Format.pp_print_string fmt "void*"
+let pp_kind fmt = function
+ | Many p -> Format.fprintf fmt "[%a]" pp_primitive p
+ | Single p -> pp_primitive fmt p
+ | Garbled -> Format.pp_print_string fmt "Garbled"
+let types r =
+ let module Tset = Cil_datatype.Typ.Set in
+ let pool = ref Tset.empty in
+ let add ty = pool := Tset.add ty !pool in
+ let map = get_map () in
+ List.iter add @@ Region.reads map r ;
+ List.iter add @@ Region.writes map r ;
+ List.iter add @@ Region.shifts map r ;
+ Tset.elements !pool
-(* -------------------------------------------------------------------------- *)
-(* --- Region Analysis for Region Memory Model --- *)
-(* -------------------------------------------------------------------------- *)
-
-module R (*: API*) =
-struct
-
- type region = Region.node
-
- let get_map () = match WpContext.get_scope () with
- | WpContext.Kf f -> Region.map f
- | WpContext.Global -> Wp_parameters.not_yet_implemented "[WP/RegionAnalysis.ml] get_map: No global region analysis yet"
-
- let null () : region =
- Warning.emit ~severe:false ~source:"Region Memory Model"
- ~effect:"Create null pointer value" "NULL" ;
- Wp_parameters.not_yet_implemented "[WP/RegionAnalysis.ml] null: cannot create null region"
-
-
- let id_of_region region = Region.uid (get_map ()) region
-
- let region_of_id id =
- try Some (Region.find (get_map ()) id)
- with Not_found -> None
-
- let hash = Region.id
-
- let equal r1 r2 = (Region.id r1 = Region.id r2)
-
- let compare r1 r2 = Int.compare (Region.id r1) (Region.id r2)
-
- let pretty fmt r = Format.fprintf fmt "R%03d" @@ Region.id r
-
- type primitive = | Int of c_int | Float of c_float | Ptr
- type kind = Single of primitive | Many of primitive | Garbled
-
- let pp_primitive fmt = function
- | Int i -> Ctypes.pp_int fmt i
- | Float f -> Ctypes.pp_float fmt f
- | Ptr -> Format.pp_print_string fmt "void*"
- let pp_kind fmt = function
- | Many p -> Format.fprintf fmt "[%a]" pp_primitive p
- | Single p -> pp_primitive fmt p
- | Garbled -> Format.pp_print_string fmt "Garbled"
-
- module CollectionCObject = Qed.Collection.Make(struct
- type t = Ctypes.c_object
- let compare = Ctypes.compare
- let hash = Ctypes.hash
- let equal = Ctypes.equal
- end)
-
- module CObjects = CollectionCObject.Set
-
- let types r =
- let map = get_map () in
- let add_type set ty = CObjects.add (Ctypes.object_of ty) set in
- let types = CObjects.empty in
- let types = List.fold_left add_type types @@ Region.reads map r in
- let types = List.fold_left add_type types @@ Region.writes map r in
- let types = List.fold_left add_type types @@ Region.shifts map r in
- types
-
- (** Internal handling of region kinds *)
- module KindCompile = struct
- (* Data : WpContext.Data with type key = Key.t *)
- type key = region
- type data = kind
- let name = "WP.RegionAnalysis.R"
- let compile region : kind = match CObjects.elements @@ types region with
- | [] ->
- Warning.emit ~severe:false ~source:"RegionAnalysis.KindCompile.compile"
- ~effect:"Access type list is empty" "%a" pretty region ;
- Garbled
- | [ Ctypes.C_int cint ] -> Many (Int cint)
- | [ Ctypes.C_float cfloat ] -> Many (Float cfloat)
- | [ Ctypes.C_pointer _ ] -> Many Ptr
- | [ Ctypes.C_comp _ ] -> Garbled
- | [ Ctypes.C_array _ ] -> Garbled
- | _ :: _ :: _ -> Garbled
- end
-
-
- (* Keeping track of the decision to apply which memory model to each region *)
- module Kind = WpContext.Generator(struct
+(* Keeping track of the decision to apply which memory model to each region *)
+module Kind = WpContext.Generator
+ (struct
(* Key : WPContext.Key *)
type t = region
let compare = compare
let pretty = pretty
- end)(KindCompile)
-
- let kind = Kind.get
-
-
- let tau_of_region region : tau = match CObjects.elements @@ types region with
- | _ :: _ :: _ ->
- Warning.emit ~severe:false ~source:"RegionAnalysis.tau_of_region"
- ~effect:"Access type list is more than a singleton" "%a" pretty region ;
- assert false
- | [] ->
- Warning.emit ~severe:false ~source:"RegionAnalysis.tau_of_region"
- ~effect:"Access type list is empty" "%a" pretty region ;
- assert false
- | [ ty ] -> Lang.tau_of_object ty
-
- let points_to region = Region.points_to (get_map ()) region
+ end)
+ (struct
+ (* Data : WpContext.Data with type key = Key.t *)
+ type key = region
+ type data = kind
+ let name = "Wp.RegionAnalysis.R"
+ let compile region : kind =
+ match types region with
+ | [ty] ->
+ begin
+ match Ctypes.object_of ty with
+ | C_int i -> Many (Int i)
+ | C_float f -> Many (Float f)
+ | C_pointer _ -> Many Ptr
+ | _ -> Garbled
+ end
+ | _ -> Garbled
+ end)
- (*
+let kind = Kind.get
- if not (Layout.fits ~dst:s.post ~src:s.pre) then
- Warning.emit ~severe:false ~source:"Region Memory Model"
- ~effect:"Keep pointer value"
- "%a" pp_mismatch s ; l
+let tau_of_region region : tau =
+ match types region with
+ | [ ty ] -> Lang.tau_of_ctype ty
+ | _ -> (*TODO*) assert false
+let points_to region = Region.points_to (get_map ()) region
- *)
+let separated r1 r2 = Region.separated (get_map ()) r1 r2
- let separated r1 r2 = Region.separated (get_map ()) r1 r2
+let included r1 r2 = Region.included (get_map ()) r1 r2
- let included r1 r2 = Region.included (get_map ()) r1 r2
+let cvar var =
+ try Some (Region.cvar (get_map ()) var)
+ with Not_found ->
+ Warning.emit ~severe:false ~source:"RegionAnalysis.cvar"
+ ~effect:"No region found for C variable" "%a" Printer.pp_varinfo var ;
+ None
- let cvar var =
- try Some (Region.cvar (get_map ()) var)
- with Not_found ->
- Warning.emit ~severe:false ~source:"RegionAnalysis.cvar"
- ~effect:"No region found for C variable" "%a" Printer.pp_varinfo var ;
- None
+let field (region: region) (fd: fieldinfo) : region option =
+ try Some (Region.field (get_map ()) region fd)
+ with Not_found ->
+ Warning.emit ~severe:false
+ ~source:"RegionAnalysis.field"
+ ~effect:"No region found for field"
+ "No region for field %a from region %a"
+ Printer.pp_field fd pretty region;
+ None
- let field (region: region) (fd: fieldinfo) : region option =
- try Some (Region.field (get_map ()) region fd)
- with Not_found ->
+let shift region ty offset =
+ let rec aux = function
+ | [] ->
Warning.emit ~severe:false
- ~source:"RegionAnalysis.field"
- ~effect:"No region found for field"
- "No region for field %a from region %a"
- Printer.pp_field fd pretty region;
+ ~source:"RegionAnalysis.shift"
+ ~effect:"No region found"
+ "No region for shift %a from region %a"
+ QED.pretty offset pretty region;
None
-
- let shift region ty offset =
- let rec aux = function
- | [] ->
- Warning.emit ~severe:false
- ~source:"RegionAnalysis.shift"
- ~effect:"No region found"
- "No region for shift %a from region %a"
- QED.pretty offset pretty region;
- None
- | typ :: rest ->
- try Some (Region.index (get_map ()) region typ)
- with Not_found -> aux rest
- in aux @@ Ctypes.object_to ty
-
- let base_addr _ = assert false
- let literal ~eid _ = ignore eid ; assert false
- let pointer_loc () = assert false
- let loc_of_int () = assert false
-
-end
+ | typ :: rest ->
+ try Some (Region.index (get_map ()) region typ)
+ with Not_found -> aux rest
+ in aux @@ Ctypes.object_to ty
+
+let base_addr _ = assert false
+let literal ~eid _ = ignore eid ; assert false
+let pointer_loc () = assert false
+let loc_of_int () = assert false
diff --git a/src/plugins/wp/RegionAnalysis.mli b/src/plugins/wp/RegionAnalysis.mli
index a50d0bc4bd8..ebce9717a1d 100644
--- a/src/plugins/wp/RegionAnalysis.mli
+++ b/src/plugins/wp/RegionAnalysis.mli
@@ -20,46 +20,8 @@
(* *)
(**************************************************************************)
-open Cil_types
-open Ctypes
-open Lang.F
-
(* -------------------------------------------------------------------------- *)
(* --- Region Analysis API for Region Memory Model --- *)
(* -------------------------------------------------------------------------- *)
-module type API = sig
- type region
- val null : unit -> region
-
-
- val hash : region -> int
- val equal : region -> region -> bool
- val compare : region -> region -> int
- val pretty : Format.formatter -> region -> unit
-
- type primitive = | Int of c_int | Float of c_float | Ptr
- type kind = Single of primitive | Many of primitive | Garbled
- val kind : region -> kind
- val pp_kind : Format.formatter -> kind -> unit
-
- val tau_of_region : region -> tau
- val points_to : region -> region option
-
- val separated : region -> region -> bool
- val included : region -> region -> bool
-
- val cvar : varinfo -> region option
- val field : region -> fieldinfo -> region option
- val shift : region -> c_object -> term -> region option
- val base_addr : region -> region
-
- val literal : eid:int -> Cstring.cst -> region option
- val pointer_loc : unit -> region option
- val loc_of_int : unit -> region option
-
- val id_of_region : region -> int
- val region_of_id : int -> region option
-end
-
-module R : API
+include MemRegion.RegionProxy
--
GitLab