From f5a59c116bdaec10018e4a69546edc55fa86271a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 11 Jun 2024 16:44:52 +0200
Subject: [PATCH] [region] region annotations
---
src/plugins/region/annot.ml | 257 +++++++++++++++++++++++++++++++++++
src/plugins/region/annot.mli | 53 ++++++++
2 files changed, 310 insertions(+)
create mode 100644 src/plugins/region/annot.ml
create mode 100644 src/plugins/region/annot.mli
diff --git a/src/plugins/region/annot.ml b/src/plugins/region/annot.ml
new file mode 100644
index 00000000000..ef71d881aad
--- /dev/null
+++ b/src/plugins/region/annot.ml
@@ -0,0 +1,257 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Logic_ptree
+open Cil_types
+open Cil_datatype
+
+(* -------------------------------------------------------------------------- *)
+(* --- Region Specifications --- *)
+(* -------------------------------------------------------------------------- *)
+
+type lpath = {
+ loc : location ;
+ ltype : typ ;
+ lnode : lnode ;
+}
+
+and lnode =
+ | L_var of varinfo
+ | L_region of string
+ | L_addr of lpath
+ | L_star of lpath
+ | L_index of lpath
+ | L_shift of lpath
+ | L_field of lpath * fieldinfo
+ | L_cast of typ * lpath
+
+type region = {
+ rname: string option ;
+ rpath: lpath list ;
+}
+
+(* -------------------------------------------------------------------------- *)
+(* --- Printers --- *)
+(* -------------------------------------------------------------------------- *)
+
+let atomic = function
+ | L_var _ | L_region _ | L_addr _ | L_star _ | L_index _ | L_field _ -> true
+ | L_shift _ | L_cast _ -> false
+
+let rec pp_lnode fmt = function
+ | L_var x -> Varinfo.pretty fmt x
+ | L_region a -> Format.pp_print_string fmt a
+ | L_field(p,f) -> pfield p f fmt
+ | L_index a -> Format.fprintf fmt "%a[..]" pp_latom a
+ | L_shift a -> Format.fprintf fmt "%a+(..)" pp_latom a
+ | L_star a -> Format.fprintf fmt "*%a" pp_latom a
+ | L_addr a -> Format.fprintf fmt "&%a" pp_latom a
+ | L_cast(t,a) -> Format.fprintf fmt "(%a)@,%a" Typ.pretty t pp_latom a
+
+and pfield p fd fmt =
+ match p.lnode with
+ | L_star p -> Format.fprintf fmt "%a->%a" pp_latom p Fieldinfo.pretty fd
+ | _ -> Format.fprintf fmt "%a.%a" pp_latom p Fieldinfo.pretty fd
+
+and pp_latom fmt a =
+ if atomic a.lnode then pp_lnode fmt a.lnode
+ else Format.fprintf fmt "@[<hov 2>(%a)@]" pp_lnode a.lnode
+
+and pp_lpath fmt a = pp_lnode fmt a.lnode
+
+let pp_named fmt = function None -> () | Some a -> Format.fprintf fmt "%s: " a
+
+let pp_region fmt r =
+ match r.rpath with
+ | [] -> Format.pp_print_string fmt "\null"
+ | p::ps ->
+ begin
+ Format.fprintf fmt "@[<hov 2>]" ;
+ pp_named fmt r.rname ;
+ pp_lpath fmt p ;
+ List.iter (Format.fprintf fmt ",@ %a" pp_lpath) ps ;
+ Format.fprintf fmt "@]" ;
+ end
+
+let pp_regions fmt = function
+ | [] -> Format.pp_print_string fmt "\null"
+ | r::rs ->
+ begin
+ Format.fprintf fmt "@[<hv 0>]" ;
+ pp_region fmt r ;
+ List.iter (Format.fprintf fmt ",@ %a" pp_region) rs ;
+ Format.fprintf fmt "@]" ;
+ end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Parsers --- *)
+(* -------------------------------------------------------------------------- *)
+
+type env = {
+ context: Logic_typing.typing_context ;
+ mutable named: string option ;
+ mutable paths: lpath list ;
+ mutable specs: region list ;
+}
+
+let error (env:env) ~loc msg = env.context.error loc msg
+
+let getCompoundType env ~loc typ =
+ match Cil.unrollType typ with
+ | TComp(comp,_) -> comp
+ | _ -> error env ~loc "Expected compound type for term"
+
+let parse_name (env:env) ~loc x =
+ try
+ match env.context.find_var x with
+ | { lv_origin = Some v } -> { loc ; ltype = v.vtype ; lnode = L_var v }
+ | _ -> error env ~loc "Variable '%s' is not a C-variable" x
+ with Not_found -> { loc ; ltype = TVoid [] ; lnode = L_region x }
+
+let parse_field env ~loc comp f =
+ try List.find (fun fd -> fd.fname = f) (Option.value ~default:[] comp.cfields)
+ with Not_found ->
+ error env ~loc "No field '%s' in compound type '%s'" f comp.cname
+
+let parse_lrange (env: env) (e : lexpr) =
+ match e.lexpr_node with
+ | PLrange(None,None) -> ()
+ | _ ->
+ error env ~loc:e.lexpr_loc "Unexpected index (use unspecified range only)"
+
+let parse_ltype env ~loc t =
+ let open Logic_typing in
+ let g = env.context in
+ let t = g.logic_type g loc g.pre_state t in
+ match Logic_utils.unroll_type t with
+ | Ctype typ -> typ
+ | _ -> error env ~loc "C-type expected for casting l-values"
+
+let rec parse_lpath (env:env) (e: lexpr) =
+ let loc = e.lexpr_loc in
+ match e.lexpr_node with
+ | PLvar x -> parse_name env ~loc x
+ | PLunop( Ustar , p ) ->
+ let lv = parse_lpath env p in
+ if Cil.isPointerType lv.ltype then
+ let te = Cil.typeOf_pointed lv.ltype in
+ { loc ; lnode = L_star lv ; ltype = te }
+ else
+ error env ~loc "Pointer-type expected for operator '&'"
+ | PLunop( Uamp , p ) ->
+ let lv = parse_lpath env p in
+ let ltype = TPtr( lv.ltype , [] ) in
+ { loc ; lnode = L_addr lv ; ltype }
+ | PLbinop( p , Badd , rg ) ->
+ parse_lrange env rg ;
+ let { ltype } as lv = parse_lpath env p in
+ if Cil.isPointerType ltype then
+ { loc ; lnode = L_shift lv ; ltype = ltype }
+ else
+ if Cil.isArrayType ltype then
+ let te = Cil.typeOf_array_elem ltype in
+ { loc ; lnode = L_shift lv ; ltype = TPtr(te,[]) }
+ else
+ error env ~loc "Pointer-type expected for operator '+'"
+ | PLdot( p , f ) ->
+ let lv = parse_lpath env p in
+ let comp = getCompoundType env ~loc:lv.loc lv.ltype in
+ let fd = parse_field env ~loc comp f in
+ { loc ; lnode = L_field(lv,fd) ; ltype = fd.ftype }
+ | PLarrow( p , f ) ->
+ let sp = { lexpr_loc = loc ; lexpr_node = PLunop(Ustar,p) } in
+ let pf = { lexpr_loc = loc ; lexpr_node = PLdot(sp,f) } in
+ parse_lpath env pf
+ | PLarrget( p , rg ) ->
+ parse_lrange env rg ;
+ let { ltype } as lv = parse_lpath env p in
+ if Cil.isPointerType ltype then
+ let pointed = Cil.typeOf_pointed ltype in
+ let ls = { loc ; lnode = L_shift lv ; ltype } in
+ { loc ; lnode = L_star ls ; ltype = pointed }
+ else
+ if Cil.isArrayType ltype then
+ let elt = Cil.typeOf_array_elem ltype in
+ { loc ; lnode = L_index lv ; ltype = elt }
+ else
+ error env ~loc:lv.loc "Pointer or array type expected"
+ | PLcast( t , a ) ->
+ let lv = parse_lpath env a in
+ let ty = parse_ltype env ~loc t in
+ { loc ; lnode = L_cast(ty,lv) ; ltype = ty }
+ | _ ->
+ error env ~loc "Unexpected expression for region spec"
+
+let rec parse_named_lpath (env:env) p =
+ match p.lexpr_node with
+ | PLnamed( name , p ) ->
+ if env.named <> None && env.paths <> [] then
+ begin
+ env.specs <- { rname = env.named ; rpath = env.paths } :: env.specs ;
+ env.paths <- [] ;
+ end ;
+ env.named <- Some name ;
+ parse_named_lpath env p
+ | _ ->
+ let path = parse_lpath env p in
+ env.paths <- path :: env.paths
+
+(* -------------------------------------------------------------------------- *)
+(* --- Spec Typechecking & Printing --- *)
+(* -------------------------------------------------------------------------- *)
+
+let kspec = ref 0
+let registry = Hashtbl.create 0
+
+let of_extid = Hashtbl.find registry
+let of_extrev = function
+ | { ext_name="region" ; ext_kind = Ext_id k } -> of_extid k
+ | _ -> raise Not_found
+let of_extension e = List.rev (of_extrev e)
+let of_behavior bhv =
+ List.fold_left
+ (fun acc e -> List.rev_append (try of_extrev e with Not_found -> []) acc)
+ [] bhv.Cil_types.b_extended
+
+let typecheck typing_context _loc ps =
+ let env = {
+ named = None ;
+ context = typing_context ;
+ paths = [] ; specs = [] ;
+ } in
+ List.iter (parse_named_lpath env) ps ;
+ let id = !kspec in incr kspec ;
+ let specs = { rname = env.named ; rpath = env.paths } :: env.specs in
+ Hashtbl.add registry id @@ List.rev specs ;
+ Ext_id id
+
+let printer _pp fmt = function
+ | Ext_id k ->
+ let rs = try Hashtbl.find registry k with Not_found -> [] in
+ pp_regions fmt rs
+ | _ -> ()
+
+let () =
+ Acsl_extension.register_behavior
+ ~plugin:"region" "alias" typecheck ~printer false
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/region/annot.mli b/src/plugins/region/annot.mli
new file mode 100644
index 00000000000..daea818874d
--- /dev/null
+++ b/src/plugins/region/annot.mli
@@ -0,0 +1,53 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+type lpath = {
+ loc : location ;
+ ltype : typ ;
+ lnode : lnode ;
+}
+
+and lnode =
+ | L_var of varinfo
+ | L_region of string
+ | L_addr of lpath
+ | L_star of lpath
+ | L_index of lpath
+ | L_shift of lpath
+ | L_field of lpath * fieldinfo
+ | L_cast of typ * lpath
+
+type region = {
+ rname: string option ;
+ rpath: lpath list ;
+}
+
+val pp_lnode : Format.formatter -> lnode -> unit
+val pp_latom : Format.formatter -> lpath -> unit
+val pp_lpath : Format.formatter -> lpath -> unit
+val pp_region : Format.formatter -> region -> unit
+val pp_regions : Format.formatter -> region list -> unit
+
+val of_extension : acsl_extension -> region list
+val of_behavior : behavior -> region list
--
GitLab