package frama-c

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

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

(* -------------------------------------------------------------------------- *)
(* --- Generic Sigma Factory                                              --- *)
(* -------------------------------------------------------------------------- *)

open Lang.F

module Make
    (C : Sigs.Chunk)
    (H : Qed.Collection.S with type t = C.t) :
  Sigs.Sigma with type chunk = C.t
              and module Chunk = H =
struct

  type chunk = C.t
  module Chunk = H
  type domain = H.Set.t

  let empty = H.Set.empty
  let union = H.Set.union

  type t = { id : int ; mutable map : var H.map }

  let id = ref 0 (* for debugging purpose *)
  let build map = let k = !id in incr id ; { id = k ; map = map }
  let create () = build H.Map.empty
  let copy s = build s.map

  let newchunk c =
    Lang.freshvar ~basename:(C.basename_of_chunk c) (C.tau_of_chunk c)

  let merge a b =
    let pa = ref Passive.empty in
    let pb = ref Passive.empty in
    let merge_chunk c x y =
      if Var.equal x y then x else
        let z = newchunk c in
        pa := Passive.bind ~fresh:z ~bound:x !pa ;
        pb := Passive.bind ~fresh:z ~bound:y !pb ;
        z in
    let w = H.Map.union merge_chunk a.map b.map in
    build w , !pa , !pb

  type kind =
    | Used of Lang.F.var
    | Unused

  let merge_list l =
    (* Get a map of the chunks (the data is not important) *)
    let union = List.fold_left (fun acc e -> H.Map.union (fun _ v1 _ -> v1) acc e.map) H.Map.empty l in
    (* The goal is to build a matrix chunk -> elt of the list -> Used/Unused
    *)
    (* Set the data of the map to []. *)
    let union = H.Map.map (fun _ -> []) union in
    (* For each elements of the list tell if each chunk is used *)
    let merge _ m e =
      match m, e with
      | Some m, Some e -> Some (Used e::m)
      | Some m, None -> Some (Unused::m)
      | None, _ -> assert false in
    let union = List.fold_left (fun acc e -> H.Map.merge merge acc e.map) union
        (* important so that the list in the map are in the correct order *)
        (List.rev l) in
    (* Build the passive for each element of the list, and the final domain *)
    let p = ref (List.map (fun _ -> Passive.empty) l) in
    let map c l =
      match List.filter (fun x -> not (Unused = x)) l with
      | [] -> assert false
      (* If all the sigmas use the same variable *)
      | (Used a)::l when List.for_all (function | Unused -> true | Used x -> Var.equal x a) l ->
        a
      | _ ->
        let z = newchunk c in
        let map2 p = function
          | Unused -> p
          | Used a -> Passive.bind ~fresh:z ~bound:a p
        in
        p := List.map2 map2 !p l;
        z
    in
    let union = H.Map.mapi map union in
    build union , !p

  let choose a b =
    let merge_chunck _ x y = if Var.compare x y <= 0 then x else y in
    build (H.Map.union merge_chunck a.map b.map)

  let get w c =
    try H.Map.find c w.map
    with Not_found ->
      let x = newchunk c in
      w.map <- H.Map.add c x w.map ; x

  let mem w c = H.Map.mem c w.map

  let join a b =
    if a == b then Passive.empty else
      let p = ref Passive.empty in
      H.Map.iter2
        (fun chunk x y ->
           match x,y with
           | Some x , Some y -> p := Passive.join x y !p
           | Some x , None -> b.map <- H.Map.add chunk x b.map
           | None , Some y -> a.map <- H.Map.add chunk y a.map
           | None , None -> ())
        a.map b.map ; !p

  let assigned ~pre ~post written =
    let p = ref Bag.empty in
    H.Map.iter2
      (fun chunk x y ->
         if not (H.Set.mem chunk written) then
           match x,y with
           | Some x , Some y when x != y ->
             p := Bag.add (p_equal (e_var x) (e_var y)) !p
           | Some x , None -> post.map <- H.Map.add chunk x post.map
           | None , Some y -> pre.map <- H.Map.add chunk y pre.map
           | _ -> ())
      pre.map post.map ; !p

  let value w c = e_var (get w c)

  let iter f w = H.Map.iter f w.map
  let iter2 f w1 w2 = H.Map.iter2 f w1.map w2.map

  let havoc w xs =
    let ys = H.Set.mapping newchunk xs in
    build (H.Map.union (fun _c _old y -> y) w.map ys)

  let havoc_chunk w c =
    let x = newchunk c in
    build (H.Map.add c x w.map)

  let havoc_any ~call w =
    let framer c x = if call && C.is_framed c then x else newchunk c in
    build (H.Map.mapi framer w.map)

  let remove_chunks w xs =
    build (H.Map.filter (fun c _ -> not (H.Set.mem c xs)) w.map)

  let domain w = H.Map.domain w.map

  let pretty fmt w =
    begin
      Format.fprintf fmt "@[<hov 2>@@%s%d[" C.self w.id ;
      H.Map.iter
        (fun c x -> Format.fprintf fmt "@ %a:%a" C.pretty c Var.pretty x) w.map ;
      Format.fprintf fmt " ]@]" ;
    end

  let writes seq =
    let effect = ref Chunk.Set.empty in
    iter2
      (fun chunk u v ->
         let written =
           match u,v with
           | Some x , Some y -> not (Var.equal x y)
           | None , Some _ -> true
           | Some _ , None -> false (* no need to create a new so it is the same *)
           | None, None -> assert false
         in
         if written then effect := Chunk.Set.add chunk !effect
      ) seq.Sigs.pre seq.Sigs.post ;
    !effect

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