package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file annot.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
(**************************************************************************)
(*                                                                        *)
(*  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 path = {
  loc : location ;
  typ : typ ;
  step: step ;
}

and step =
  | Var of varinfo
  | AddrOf of path
  | Star of path
  | Shift of path
  | Index of path * int
  | Field of path * fieldinfo
  | Cast of typ * path

type region = {
  rname: string option ;
  rpath: path list ;
}

(* -------------------------------------------------------------------------- *)
(* ---  Printers                                                          --- *)
(* -------------------------------------------------------------------------- *)

let atomic = function
  | Var _ | AddrOf _ | Star _ | Index _ | Field _ -> true
  | Shift _ | Cast _ -> false

let rec pp_step fmt = function
  | Var x -> Varinfo.pretty fmt x
  | Field(p,f) -> pfield p f fmt
  | Index(a,n) -> Format.fprintf fmt "%a[%d]" pp_atom a n
  | Shift a -> Format.fprintf fmt "%a+(..)" pp_atom a
  | Star a -> Format.fprintf fmt "*%a" pp_atom a
  | AddrOf a -> Format.fprintf fmt "&%a" pp_atom a
  | Cast(t,a) -> Format.fprintf fmt "(%a)@,%a" Typ.pretty t pp_atom a

and pfield p fd fmt =
  match p.step with
  | Star p -> Format.fprintf fmt "%a->%a" pp_atom p Fieldinfo.pretty fd
  | _ -> Format.fprintf fmt "%a.%a" pp_atom p Fieldinfo.pretty fd

and pp_atom fmt a =
  if atomic a.step then pp_step fmt a.step
  else Format.fprintf fmt "@[<hov 2>(%a)@]" pp_step a.step

and pp_path fmt a = pp_step fmt a.step

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_path fmt p ;
      List.iter (Format.fprintf fmt ",@ %a" pp_path) 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: path list ;
  mutable specs: region list ;
}

let error (env:env) ~loc msg = env.context.error loc msg

let parse_variable (env:env) ~loc x =
  match env.context.find_var x with
  | { lv_origin = Some v } -> { loc ; typ = v.vtype ; step = Var v }
  | _ -> error env ~loc "Variable '%s' is not a C-variable" x

let parse_field env ~loc comp f =
  try Cil.getCompField comp f with Not_found ->
    error env ~loc "No field '%s' in compound type '%s'" f comp.cname

let parse_compinfo env ~loc typ =
  try Cil.getCompType typ with Not_found ->
    error env ~loc "Expected compound type for term"

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_typ 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_variable env ~loc x
  | PLunop( Ustar , p ) ->
    let lv = parse_lpath env p in
    if Cil.isPointerType lv.typ then
      let te = Cil.typeOf_pointed lv.typ in
      { loc ; step = Star lv ; typ = te }
    else
      error env ~loc "Pointer-type expected for operator '*'"
  | PLunop( Uamp , p ) ->
    let lv = parse_lpath env p in
    let typ = TPtr( lv.typ , [] ) in
    { loc ; step = AddrOf lv ; typ }
  | PLbinop( p , Badd , rg ) ->
    parse_lrange env rg ;
    let { typ } as lv = parse_lpath env p in
    if Cil.isPointerType typ then
      { loc ; step = Shift lv ; typ = typ }
    else
    if Cil.isArrayType typ then
      let te = Cil.typeOf_array_elem typ in
      { loc ; step = Shift lv ; typ = TPtr(te,[]) }
    else
      error env ~loc "Pointer-type expected for operator '+'"
  | PLdot( p , f ) ->
    let lv = parse_lpath env p in
    let comp = parse_compinfo env ~loc:lv.loc lv.typ in
    let fd = parse_field env ~loc comp f in
    { loc ; step = Field(lv,fd) ; typ = 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 { typ } as lv = parse_lpath env p in
    if Cil.isPointerType typ then
      let pointed = Cil.typeOf_pointed typ in
      let ls = { loc ; step = Shift lv ; typ } in
      { loc ; step = Star ls ; typ = pointed }
    else
    if Cil.isArrayType typ then
      let elt,size = Cil.typeOf_array_elem_size typ in
      { loc ; step = Index(lv,Z.to_int @@ Option.get size) ; typ = 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_typ env ~loc t in
    { loc ; step = Cast(ty,lv) ; typ = 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 id = try Hashtbl.find registry id with Not_found -> []
let of_extension = function
  | { ext_name="region" ; ext_kind = Ext_id k } -> of_extid k
  | _ -> []
let of_code_annot = function
  | { annot_content = AExtended(_,_,e) } -> of_extension e
  | _ -> []

let of_behavior bhv = List.concat_map of_extension bhv.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 () =
  begin
    Acsl_extension.register_behavior
      ~plugin:"region" "region" typecheck ~printer false ;
    Acsl_extension.register_code_annot
      ~plugin:"region" "alias" typecheck ~printer false ;
  end


(* -------------------------------------------------------------------------- *)
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct