package frama-c

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

Source file register.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
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2023                                               *)
(*    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
open Locations

let () = Db.Value.compute := Analysis.compute
let () = Parameters.ForceValues.set_output_dependencies [Self.state]

let main () =
  (* Value computations *)
  if Parameters.ForceValues.get () then Analysis.compute ();
  if Analysis.is_computed () then Red_statuses.report ()

let () = Db.Main.extend main


(* "access" functions before evaluation, registered in Db.Value *)
let access_value_of_lval kinstr lv =
  let state = Db.Value.get_state kinstr in
  snd (!Db.Value.eval_lval None state lv)

let access_value_of_expr kinstr e =
  let state = Db.Value.get_state kinstr in
  !Db.Value.eval_expr state e

let access_value_of_location kinstr loc =
  let state = Db.Value.get_state kinstr in
  Db.Value.find state loc

let find_deps_term_no_transitivity_state state t =
  try
    let env = Eval_terms.env_only_here state in
    let r = Eval_terms.eval_term ~alarm_mode:Eval_terms.Ignore env t in
    r.Eval_terms.ldeps
  with Eval_terms.LogicEvalError _ -> raise Db.From.Not_lval

let find_deps_no_transitivity stmt expr =
  Results.(before stmt |> expr_deps expr)

let find_deps_no_transitivity_state state expr =
  Results.(in_cvalue_state state |> expr_deps expr)

let eval_predicate ~pre ~here p =
  let open Eval_terms in
  let env = env_annot ~pre ~here () in
  match eval_predicate env p with
  | True -> Property_status.True
  | False -> Property_status.False_if_reachable
  | Unknown -> Property_status.Dont_know

let () =
  Db.Value.is_called := Function_calls.is_called;
  Db.Value.callers := Function_calls.callsites;
  Db.Value.use_spec_instead_of_definition :=
    Function_calls.use_spec_instead_of_definition;
  Db.Value.assigns_outputs_to_zone :=
    (fun s ~result a -> Logic_inout.assigns_outputs_to_zone ~result s a);
  Db.Value.assigns_inputs_to_zone := Logic_inout.assigns_inputs_to_zone;
  Db.Value.access := access_value_of_lval;
  Db.Value.access_location := access_value_of_location;
  Db.Value.access_expr := access_value_of_expr;
  Db.Value.Logic.eval_predicate := eval_predicate;
  Db.Value.valid_behaviors := Logic_inout.valid_behaviors;
  Db.From.find_deps_term_no_transitivity_state :=
    find_deps_term_no_transitivity_state;
  Db.From.find_deps_no_transitivity := find_deps_no_transitivity;
  Db.From.find_deps_no_transitivity_state := find_deps_no_transitivity_state;


  (* -------------------------------------------------------------------------- *)
  (*                    Register Evaluation Functions                           *)
  (* -------------------------------------------------------------------------- *)

open Eval

module CVal = struct
  include Main_values.CVal
  let structure = Abstract.Value.Leaf (key, (module Main_values.CVal))
end

module Val = struct
  include CVal
  include Structure.Open (Abstract.Value) (CVal)
  let reduce t = t
end

module Eva =
  Evaluation.Make
    (Val)
    (Main_locations.PLoc)
    (Cvalue_domain.State)

let inject_cvalue state = state, Locals_scoping.bottom ()

let bot_value = function
  | `Bottom -> Cvalue.V.bottom
  | `Value v -> v

let bot_state = function
  | `Bottom -> Cvalue.Model.bottom
  | `Value s -> s

let update valuation state =
  let domain_valuation = Eva.to_domain_valuation valuation in
  bot_state (Cvalue_domain.State.update domain_valuation state >>-: fst)

let rec eval_deps state e =
  match e.enode with
  | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ | Const _ ->
    Locations.Zone.bottom
  | Lval lv -> eval_deps_lval state lv
  | BinOp (_,e1,e2,_) ->
    Locations.Zone.join (eval_deps state e1) (eval_deps state e2)
  | CastE (_,e) | UnOp (_,e,_) ->
    eval_deps state e
  | AddrOf lv | StartOf lv -> eval_deps_addr state lv
and eval_deps_lval state lv =
  let for_writing = false in
  let deps = eval_deps_addr state lv in
  let loc =
    fst (Eva.lvaluate ~for_writing state lv)
    >>-: fun (_valuation, loc, _typ) -> loc
  in
  match loc with
  | `Bottom -> deps
  | `Value loc ->
    let deps_lv = Precise_locs.enumerate_valid_bits Read loc in
    Locations.Zone.join deps deps_lv
and eval_deps_addr state (h, o:lval) =
  Locations.Zone.join (eval_deps_host state h) (eval_deps_offset state o)
and eval_deps_host state h = match h with
  | Var _ -> Locations.Zone.bottom
  | Mem e -> eval_deps state e
and eval_deps_offset state o = match o with
  | NoOffset -> Locations.Zone.bottom
  | Field (_, o) -> eval_deps_offset state o
  | Index (i, o) ->
    Locations.Zone.join (eval_deps state i) (eval_deps_offset state o)

let notify_opt with_alarms alarms =
  Option.iter (fun mode -> Alarmset.notify mode alarms) with_alarms

let eval_expr_with_valuation ?with_alarms deps state expr=
  let state = inject_cvalue state in
  let deps = match deps with
    | None -> None
    | Some deps ->
      let deps' = eval_deps state expr in
      Some (Locations.Zone.join deps' deps)
  in
  let eval, alarms = Eva.evaluate state expr in
  notify_opt with_alarms alarms;
  match eval with
  | `Bottom -> (Cvalue.Model.bottom, deps, Cvalue.V.bottom), None
  | `Value (valuation, result) ->
    let state = update valuation state in
    (state, deps, result), Some valuation

(* Compatibility layer between the old API of eval_exprs and the new evaluation
   scheme. *)
module Eval = struct

  let eval_expr ?with_alarms state expr =
    let state = inject_cvalue state in
    let eval, alarms = Eva.evaluate ~reduction:false state expr in
    notify_opt with_alarms alarms;
    bot_value (eval >>-: snd)

  let eval_lval ?with_alarms deps state lval =
    let expr = Eva_utils.lval_to_exp lval in
    let res, valuation = eval_expr_with_valuation ?with_alarms deps state expr in
    let typ = match valuation with
      | None -> Cil.typeOfLval lval
      | Some valuation -> match Eva.Valuation.find_loc valuation lval with
        | `Value record -> record.typ
        | `Top -> Cil.typeOfLval lval
    in
    let state, deps, v = res in
    state, deps, v, typ

  let eval_expr_with_deps_state ?with_alarms deps state expr =
    fst (eval_expr_with_valuation ?with_alarms deps state expr)


  let reduce_by_cond state expr positive =
    let state = inject_cvalue state in
    let eval, _alarms =
      Eva.reduce state expr positive
    in
    bot_state (eval >>-: fun valuation -> update valuation state)


  let lval_to_precise_loc_deps_state ?with_alarms ~deps state ~reduce_valid_index:(_:bool) lval =
    if not (Cvalue.Model.is_reachable state)
    then state, deps, Precise_locs.loc_bottom, (Cil.typeOfLval lval)
    else
      let state = inject_cvalue state in
      let deps = match deps with
        | None -> None
        | Some deps ->
          let deps' = eval_deps_addr state lval in
          Some (Locations.Zone.join deps' deps)
      in
      let eval, alarms =
        Eva.lvaluate ~for_writing:false state lval
      in
      notify_opt with_alarms alarms;
      match eval with
      | `Bottom -> Cvalue.Model.bottom, deps, Precise_locs.loc_bottom, (Cil.typeOfLval lval)
      | `Value (valuation, loc, typ) -> update valuation state, deps, loc, typ

  let lval_to_loc_deps_state ?with_alarms ~deps state ~reduce_valid_index lv =
    let state, deps, pl, typ =
      lval_to_precise_loc_deps_state
        ?with_alarms ~deps state ~reduce_valid_index lv
    in
    state, deps, Precise_locs.imprecise_location pl, typ

  let lval_to_precise_loc_state ?with_alarms state lv =
    let state, _, r, typ =
      lval_to_precise_loc_deps_state
        ?with_alarms ~deps:None ~reduce_valid_index:(Kernel.SafeArrays.get ())
        state lv
    in
    state, r, typ

  and lval_to_loc_state ?with_alarms state lv =
    let state, _, r, typ =
      lval_to_loc_deps_state
        ?with_alarms ~deps:None ~reduce_valid_index:(Kernel.SafeArrays.get ())
        state lv
    in
    state, r, typ

  let lval_to_precise_loc ?with_alarms state lv =
    let _, r, _typ = lval_to_precise_loc_state ?with_alarms state lv in
    r

  let lval_to_loc ?with_alarms state lv =
    let _, r, _typ = lval_to_loc_state ?with_alarms state lv in
    r


  let resolv_func_vinfo ?with_alarms deps state funcexp =
    let open Cil_types in
    let state = inject_cvalue state in
    let deps = match funcexp.enode with
      | Lval (Var _, NoOffset) -> deps
      | Lval (Mem v, _) ->
        begin match deps with
          | None -> None
          | Some deps ->
            let deps' = eval_deps state v in
            Some (Locations.Zone.join deps' deps)
        end
      | _ -> assert false
    in
    let kfs, alarms = Eva.eval_function_exp funcexp state in
    notify_opt with_alarms alarms;
    let kfs = match kfs with
      | `Bottom -> Kernel_function.Hptset.empty
      | `Value kfs ->
        List.fold_left
          (fun acc (kf, _) -> Kernel_function.Hptset.add kf acc)
          Kernel_function.Hptset.empty kfs
    in
    kfs, deps

end

module type Eval = module type of Eval

(* Functions to register in Db.Value that depend on evaluation functions. *)
module Export (Eval : Eval) = struct

  open Eval

  let lval_to_loc_with_deps_state ?with_alarms state ~deps lv =
    let _state, deps, r, _ =
      lval_to_loc_deps_state
        ?with_alarms
        ~deps:(Some deps)
        ~reduce_valid_index:(Kernel.SafeArrays.get ())
        state
        lv
    in
    Option.value ~default:Locations.Zone.bottom deps, r

  let lval_to_loc_with_deps kinstr ?with_alarms ~deps lv =
    let state = Db.Value.noassert_get_state kinstr in
    lval_to_loc_with_deps_state ?with_alarms  state ~deps lv

  let lval_to_loc_kinstr kinstr ?with_alarms lv =
    let state = Db.Value.noassert_get_state kinstr in
    lval_to_loc ?with_alarms state lv

  let lval_to_precise_loc_with_deps_state_alarm ?with_alarms state ~deps lv =
    let _state, deps, ploc, _ =
      lval_to_precise_loc_deps_state ?with_alarms
        ~deps ~reduce_valid_index:(Kernel.SafeArrays.get ()) state lv
    in
    let deps = Option.value ~default:Locations.Zone.bottom deps in
    deps, ploc

  let lval_to_precise_loc_with_deps_state =
    lval_to_precise_loc_with_deps_state_alarm ?with_alarms:None

  let lval_to_zone kinstr ?with_alarms lv =
    let state_to_joined_zone state acc =
      let _, r =
        lval_to_precise_loc_with_deps_state_alarm ?with_alarms state ~deps:None lv
      in
      let zone = Precise_locs.enumerate_valid_bits Read r in
      Locations.Zone.join acc zone
    in
    Db.Value.fold_state_callstack
      state_to_joined_zone Locations.Zone.bottom ~after:false kinstr

  let lval_to_zone_state state lv =
    let _, r = lval_to_precise_loc_with_deps_state state ~deps:None lv in
    Precise_locs.enumerate_valid_bits Read r

  let lval_to_zone_with_deps_state state ~for_writing ~deps lv =
    let deps, r = lval_to_precise_loc_with_deps_state state ~deps lv in
    let r = (* No write effect if [lv] is const *)
      if for_writing && (Eva_utils.is_const_write_invalid (Cil.typeOfLval lv))
      then Precise_locs.loc_bottom
      else r
    in
    let access = if for_writing then Write else Read in
    let zone = Precise_locs.enumerate_valid_bits access r in
    let exact = Precise_locs.valid_cardinal_zero_or_one ~for_writing r in
    deps, zone, exact


  let lval_to_offsetmap_aux ?with_alarms state lv =
    let loc =
      Locations.valid_part Read
        (lval_to_loc ?with_alarms state lv)
    in
    match loc.Locations.size with
    | Int_Base.Top -> None
    | Int_Base.Value size ->
      match Cvalue.Model.copy_offsetmap loc.Locations.loc size state with
      | `Bottom -> None
      | `Value m -> Some m

  let lval_to_offsetmap kinstr ?with_alarms lv =
    let state = Db.Value.noassert_get_state kinstr in
    lval_to_offsetmap_aux ?with_alarms state lv

  let lval_to_offsetmap_state state lv =
    lval_to_offsetmap_aux state lv


  let expr_to_kernel_function_state ?with_alarms state ~deps exp =
    let r, deps = resolv_func_vinfo ?with_alarms deps state exp in
    Option.value ~default:Locations.Zone.bottom deps, r

  let expr_to_kernel_function kinstr ?with_alarms ~deps exp =
    let state_to_joined_kernel_function state (z_acc, kf_acc) =
      let z, kf =
        expr_to_kernel_function_state ?with_alarms state ~deps exp
      in
      Locations.Zone.join z z_acc,
      Kernel_function.Hptset.union kf kf_acc
    in
    Db.Value.fold_state_callstack
      state_to_joined_kernel_function
      ((match deps with None -> Locations.Zone.bottom | Some z -> z),
       Kernel_function.Hptset.empty)
      ~after:false kinstr

  let expr_to_kernel_function_state =
    expr_to_kernel_function_state ?with_alarms:None
end


module type Export = module type of (Export (Eval))

let register (module Eval: Eval) (module Export: Export) =
  let open Export in
  Db.Value.eval_expr := Eval.eval_expr;
  Db.Value.eval_expr_with_state :=
    (fun ?with_alarms state expr ->
       let (s, _, v) =
         Eval.eval_expr_with_deps_state ?with_alarms None state expr
       in
       s, v);
  Db.Value.reduce_by_cond := Eval.reduce_by_cond;
  Db.Value.eval_lval :=
    (fun ?with_alarms deps state lval ->
       let _, deps, r, _ = Eval.eval_lval ?with_alarms deps state lval in
       deps, r);
  Db.Value.lval_to_loc_with_deps := lval_to_loc_with_deps;
  Db.Value.lval_to_loc_with_deps_state :=
    lval_to_loc_with_deps_state ?with_alarms:None;
  Db.Value.lval_to_loc := lval_to_loc_kinstr;
  Db.Value.lval_to_loc_state := Eval.lval_to_loc ?with_alarms:None;
  Db.Value.lval_to_zone_state := lval_to_zone_state;
  Db.Value.lval_to_zone := lval_to_zone;
  Db.Value.lval_to_zone_with_deps_state := lval_to_zone_with_deps_state;
  Db.Value.lval_to_precise_loc_state := Eval.lval_to_precise_loc_state;
  Db.Value.lval_to_precise_loc_with_deps_state :=
    lval_to_precise_loc_with_deps_state;
  Db.Value.lval_to_offsetmap := lval_to_offsetmap;
  Db.Value.lval_to_offsetmap_state := lval_to_offsetmap_state;
  Db.Value.expr_to_kernel_function := expr_to_kernel_function;
  Db.Value.expr_to_kernel_function_state := expr_to_kernel_function_state;
  ()


let () = Db.Value.initial_state_only_globals := Analysis.cvalue_initial_state

let () = Db.Value.verify_assigns_froms := Logic_inout.verify_assigns

let () =
  let eval = (module Eval : Eval) in
  let export = (module Export ((val eval : Eval)) : Export) in
  register eval export;;


(*
Local Variables:
compile-command: "make -C ../../.."
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