package frama-c

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

Source file mt_mutexes.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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2025                                               *)
(*    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 Mt_types
open Mt_thread
open Mt_cfg_types
open Mt_mutexes_types

(* -------------------------------------------------------------------------- *)
(* --- Checking that concurrent variables accesses are properly protected --- *)
(* -------------------------------------------------------------------------- *)


let mutexes_protecting_zones' accesses =
  let aux (z, set) =
    SetNodeIdAccess.fold
      (fun (rw, node, _id) acc ->
         let mutexes = node.cfgn_context.locked_mutexes in
         let mut = match rw with
           | Read -> { mutexes_for_write = Unaccessed;
                       mutexes_for_read = Mutexes mutexes }
           | Write _ -> { mutexes_for_read = Unaccessed;
                          mutexes_for_write = Mutexes mutexes }
           | ReadAloc _ -> { mutexes_for_read = Mutexes mutexes;
                             mutexes_for_write = Unaccessed }
           | WriteAloc _ -> { mutexes_for_read = Unaccessed;
                              mutexes_for_write = Mutexes mutexes }
         in
         MutexesByZone.add_binding ~exact:false acc z mut
      ) set MutexesByZone.empty
  in
  let r1 = List.map aux accesses in
  let z = List.fold_left
      (fun r r' -> MutexesByZone.join r r') MutexesByZone.empty r1
  in z


(* Pretty a value of type [Mt_shared_vars.Precise.list_accesses]
   with the mutex information at each node concatenated to the output *)
let pretty_with_mutexes =
  Mt_shared_vars.Precise.pretty_concurrent_accesses
    ~f:(fun fmt (_, node, _) ->
        let mutexes = node.cfgn_context.locked_mutexes in
        if MutexPresence.is_empty mutexes then
          Format.fprintf fmt ",@ unprotected"
        else
          Format.fprintf fmt ",@ @[<hov>protected by %a@]"
            MutexPresence.pretty mutexes ;
        if Mt_options.PrintCallstacks.get ()
        then Format.fprintf fmt ",@ // %a" Callstack.pretty node.cfgn_stack
      ) ();
;;

type protection = Unprotected | Priority | Protected of Mutex.Set.t

let pretty_protection fmt = function
  | Unprotected -> Format.fprintf fmt "unprotected"
  | Priority -> Format.fprintf fmt "protected by priorities"
  | Protected set ->
    Format.fprintf fmt "@[<hov 2>protected by %a@]"
      (Pretty_utils.pp_iter Mutex.Set.iter Mutex.pretty) set

let pretty_protection_per_thread fmt (th_read, th_write, protection) =
  Format.fprintf fmt "@[<hov 2>Read by %a,@ Write by %a:@ %a@]"
    Thread.pretty th_read Thread.pretty th_write
    pretty_protection protection

type zone_protection =
  (Locations.Zone.t * (Thread.t * Thread.t * protection) list) list

let pretty_zone_protection fmt (z, l) =
  Format.fprintf fmt "@[<hv 2>@[%a@]:@ %a@]"
    Locations.Zone.pretty z
    (Pretty_utils.pp_list ~pre:"" ~suf:"" pretty_protection_per_thread) l

let check_protection analysis (l: Mt_shared_vars.Precise.list_accesses) : zone_protection =
  let aux (z, s) =
    let m_read = ref Thread.Map.empty in
    let m_write = ref Thread.Map.empty in
    (* YYY: we disregard information about accesses that may not be possibly
       simultaneous *)
    let add th node map =
      let mutexes' = MutexPresence.only_present node.cfgn_context.locked_mutexes in
      try
        let mutexes = Thread.Map.find th map in
        let inter = Mutex.Set.inter mutexes mutexes' in
        Thread.Map.add th inter map
      with Not_found -> Thread.Map.add th mutexes' map
    in
    let aux_nodes (op, n, th) =
      match op with
      | Read ->    m_read  := add th n !m_read
      | Write _ -> m_write := add th n !m_write
      | ReadAloc _ -> m_read := add th n !m_read
      | WriteAloc _ -> m_write := add th n !m_write
    in
    SetNodeIdAccess.iter aux_nodes s;
    let classify_access th_read read th_write write classified =
      if not (Thread.equal th_read th_write) then begin
        let th_read_state = Mt_thread.thread_state analysis th_read in
        let th_write_state = Mt_thread.thread_state analysis th_write in
        let protection =
          match th_read_state.th_priority, th_write_state.th_priority with
          | PPriority p1, PPriority p2 when p1 > p2 ->
            (* Protection by mutexes not needed, th_read cannot be preempted *)
            Priority
          | _ ->
            let both_mutexes = Mutex.Set.inter read write in
            if Mutex.Set.is_empty both_mutexes
            then Unprotected
            else Protected both_mutexes
        in
        (th_read, th_write, protection) :: classified
      end
      else classified
    in
    let protections =
      Thread.Map.fold (fun th_read read acc ->
          Thread.Map.fold (fun th_write write acc ->
              classify_access th_read read th_write write acc
            ) !m_write acc
        ) !m_read []
    in
    (z, protections)
  in
  List.map aux l

let pretty_protections fmt l =
  Pretty_utils.pp_list
    ~pre:"@[<v>" ~suf:"@]" ~sep:"@ " pretty_zone_protection fmt l

let ill_protected (accesses: Mt_shared_vars.Precise.list_accesses) (protections: zone_protection) =
  let res = Cil_datatype.Stmt.Hashtbl.create 16 in
  let aux (z, nodes) (z', protections) =
    assert (z == z');
    let aux (th_read, _th_write, protect) =
      if protect = Unprotected then
        let aux (op, node, th) =
          if Thread.equal th th_read && op = Read then begin
            let stmts = CfgNode.node_stmt node in
            let aux stmt =
              let prev =
                try Cil_datatype.Stmt.Hashtbl.find res stmt
                with Not_found -> Locations.Zone.bottom
              in
              let z = Locations.Zone.join prev z in
              Cil_datatype.Stmt.Hashtbl.replace res stmt z
            in
            List.iter aux stmts
          end
        in
        SetNodeIdAccess.iter aux nodes
    in
    List.iter aux protections
  in
  List.iter2 aux accesses protections;
  res

let need_sync stmtsh =
  let aux stmt z acc =
    (* YYY: detection should be improved to handle unspecified sequences. *)
    match stmt.preds with
    | [stmt] when Mt_cil.is_call_to_sync stmt -> acc
    | _ -> (stmt, z) :: acc
  in
  Cil_datatype.Stmt.Hashtbl.fold aux stmtsh []
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