package frama-c

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

Source file mt_interferences.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
(**************************************************************************)
(*                                                                        *)
(*  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).            *)
(*                                                                        *)
(**************************************************************************)

let concurrent_writes shared_bases =
  let module Analyzer = (val Analysis.current_analyzer ()) in
  let module ALoc = Analysis_location in
  match Analyzer.Dom.get Mt_domain.Domain.key with
  (* Domain disabled, no information about writes *)
  | None -> ALoc.Local.Set.empty
  (* Domain enabled *)
  | Some _extract ->
    let add_aloc stmt cs _state acc =
      let aloc = ALoc.Local (stmt, cs) in
      (* TODO: Maybe take the memory read/written for all callstacks of the
         given statement? (can be done directly by Inout_memory). *)
      let filter = Inout_memory.keep_globals_only in
      let memory = Inout_memory.memory_at ~filter aloc in
      let written_bases = Locations.Zone.get_bases memory.written in
      if Base.SetLattice.(intersects (inject shared_bases) written_bases)
      then ALoc.Local.Set.add (stmt, cs) acc
      else acc
    in
    let add_stmt acc stmt =
      let is_write_stmt = match stmt.Cil_types.skind with
        | Cil_types.Instr (Set _ | Call _ | Local_init _) -> true
        | _ -> false
      in
      if is_write_stmt
      then match Analyzer.get_stmt_state_by_callstack ~after:true stmt with
        | `Top | `Bottom -> acc (* TODO: handle Tops *)
        | `Value table ->
          Callstack.Hashtbl.fold (add_aloc stmt) table acc
      else acc
    in
    let add_kf kf acc =
      match kf.Cil_types.fundec with
      | Declaration _ -> acc
      | Definition (fundec,_) ->
        List.fold_left add_stmt acc fundec.Cil_types.sallstmts
    in
    Globals.Functions.fold add_kf ALoc.Local.Set.empty

let shared_bases analysis_state =
  let shared_zones = analysis_state.Mt_thread.concurrent_accesses in
  match Locations.Zone.get_bases shared_zones with
  | Top -> assert false
  | Set zones ->  zones

let add_last_analysis analysis_state =
  let module Analyzer = (val Analysis.current_analyzer ()) in
  let bases = shared_bases analysis_state in
  let writes = concurrent_writes bases in
  let thread = analysis_state.curr_thread.th_eva_thread in
  match Analyzer.Interferences.add_last_analysis thread writes bases with
  | Updated ->
    Mt_thread.iter_threads analysis_state
      (fun th -> Mt_thread.ThreadState.recompute_because th InterferencesChanged)
  | NoChanges ->
    ()
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