package frama-c

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

Source file AssignsCompleteness.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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    CEA (Commissariat a l'energie atomique et aux energies              *)
(*         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

module Completeness = struct
  module KfParam = struct
    include Cil_datatype.Kf
    let label = None
  end

  module Data =
    Datatype.Pair
      (Datatype.Bool)
      (Datatype.Function(KfParam)(Datatype.Unit))

  include State_builder.Hashtbl
      (Cil_datatype.Kf.Hashtbl)
      (Data)
      (struct
        let name = "RefUsage.AssignsCompleteness.Callbacks"
        let size = 17
        let dependencies = [ Ast.self ]
      end)
end

exception Incomplete_assigns of (string list * string)

let wkey_pedantic = Wp_parameters.register_warn_category "pedantic-assigns"

type ('a, 'b) result = Ok of 'a | Error of 'b

let collect_assigns kf =
  let opt_try f p = function None -> f p | Some x -> Some x in
  let fold_assigns bhv =
    let folder _ a acc = match a, acc with
      | WritesAny, _ -> None
      | _, None      -> Some a
      | _, Some acc  -> Some (Logic_utils.concat_assigns acc a)
    in
    Annotations.fold_assigns folder kf bhv None
  in
  let find_default () =
    match fold_assigns Cil.default_behavior_name with
    | None -> None
    | Some x -> Some [x]
  in
  let incompletes = ref [] in
  let find_complete () =
    let fold_behaviors names =
      let folder l name = match (fold_assigns name) with
        | None -> raise (Incomplete_assigns(names, name))
        | Some a -> a :: l
      in
      try Some (List.fold_left folder [] names)
      with Incomplete_assigns(bhv_l,b) ->
        incompletes := (bhv_l, b) :: !incompletes ;
        None
    in
    Annotations.fold_complete (fun _ -> opt_try fold_behaviors) kf None
  in
  (* First:
     - try to find default behavior assigns, if we cannot get it
     - try to find a "complete behaviors" set where each behavior has assigns
       As assigns and froms are over-approximations, the result (if it exists)
       must cover all assigned memory locations and all data dependencies.
  *)
  match opt_try find_complete () (opt_try find_default () None) with
  | None -> Error !incompletes
  | Some r -> Ok r

let pretty_behaviors_errors fmt l =
  let pp_complete =
    Pretty_utils.pp_list ~pre:"{" ~suf:"}" ~sep:", " Format.pp_print_string
  in
  let pp_bhv_error fmt (bhv_l, name) =
    Format.fprintf fmt
      "- in complete behaviors: %a@\n  No assigns for (at least) '%s'@\n"
      pp_complete bhv_l name
  in
  match l with
  | [] -> Format.fprintf fmt ""
  | l -> Format.fprintf fmt "%a" (Pretty_utils.pp_list pp_bhv_error) l

let check_assigns kf assigns =
  let complete = (true, fun _ -> ()) in
  let incomplete (_status, current) warning =
    let new_warning kf =
      current kf ;
      warning kf ;
    in
    (false, new_warning)
  in
  let vassigns acc a =
    let res_t = Kernel_function.get_return_type kf in
    let assigns_result ({ it_content=t }, _) = Logic_utils.is_result t in
    let froms = match a with WritesAny -> [] | Writes l -> l in
    let acc =
      if Cil.isPointerType res_t && not (List.exists assigns_result froms) then
        incomplete acc
          begin fun kf ->
            Wp_parameters.warning ~wkey:wkey_pedantic
              ~once:true ~source:(fst (Kernel_function.get_location kf))
              "No 'assigns \\result \\from ...' specification for function '%a'\
               returning pointer type.@ Callers assumptions might be imprecise."
              Kernel_function.pretty kf ;
          end
      else acc
    in
    let vfrom acc = function
      | t, FromAny when Logic_typing.is_pointer_type t.it_content.term_type ->
        incomplete acc
          begin fun _kf ->
            Wp_parameters.warning ~wkey:wkey_pedantic
              ~once:true ~source:(fst t.it_content.term_loc)
              "No \\from specification for assigned pointer '%a'.@ \
               Callers assumptions might be imprecise."
              Cil_printer.pp_identified_term t
          end
      | _ -> acc
    in List.fold_left vfrom acc froms
  in
  match assigns with
  | Error l ->
    false,
    begin fun kf ->
      Wp_parameters.warning ~wkey:wkey_pedantic
        ~once:true ~source:(fst (Kernel_function.get_location kf))
        "No 'assigns' specification for function '%a'.@\n%a\
         Callers assumptions might be imprecise."
        Kernel_function.pretty kf
        pretty_behaviors_errors l
    end
  | Ok l ->
    List.fold_left vassigns complete l

let memo_compute kf =
  Completeness.memo (fun kf -> check_assigns kf (collect_assigns kf)) kf

let compute kf =
  ignore (memo_compute kf)

let is_complete kf =
  fst(memo_compute kf)

let warn kf =
  snd(memo_compute kf) kf
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