package frama-c

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

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

(* -------------------------------------------------------------------------- *)
(* --- Cache Management                                                   --- *)
(* -------------------------------------------------------------------------- *)

type mode = NoCache | Update | Replay | Rebuild | Offline | Cleanup

let hits = ref 0
let miss = ref 0
let removed = ref 0
let cleanup = Hashtbl.create 0
(* used entries, never to be reset since cleanup is performed at exit *)

let get_hits () = !hits
let get_miss () = !miss
let get_removed () = !removed

let mark_cache ~mode hash =
  if mode = Cleanup || Wp_parameters.is_interactive () then
    Hashtbl.replace cleanup hash ()

module CACHEDIR = WpContext.StaticGenerator(Datatype.Unit)
    (struct
      type key = unit
      type data = Filepath.Normalized.t
      let name = "Wp.Cache.dir"
      let compile () =
        try
          if not (Wp_parameters.CacheEnv.get()) then
            raise Not_found ;
          let gdir = Sys.getenv "FRAMAC_WP_CACHEDIR" in
          if gdir = "" then raise Not_found ;
          Filepath.Normalized.of_string gdir
        with Not_found ->
        try
          let gdir = Wp_parameters.CacheDir.get() in
          if gdir = "" then raise Not_found ;
          Filepath.Normalized.of_string gdir
        with Not_found ->
          Wp_parameters.get_session_dir ~force:false "cache"
    end)

let get_dir () = (CACHEDIR.get () :> string)

let is_session_dir path =
  0 = Filepath.Normalized.compare
    path (Wp_parameters.get_session_dir ~force:false "cache")

let get_usable_dir ?(make=false) () =
  let path = CACHEDIR.get () in
  let parents = is_session_dir path in
  if not (Filepath.exists path) && make then
    ignore (Extlib.mkdir ~parents path 0o755);
  if not (Filepath.is_dir path) then begin
    Wp_parameters.warning ~current:false ~once:true
      "Cache path %a is not a directory"
      Filepath.Normalized.pretty path;
    raise Not_found
  end;
  path

let has_dir () =
  try
    if not (Wp_parameters.CacheEnv.get()) then
      raise Not_found ;
    Sys.getenv "FRAMAC_WP_CACHEDIR" <> ""
  with Not_found -> Wp_parameters.CacheDir.get () <> ""

let is_global_cache () = Wp_parameters.CacheDir.get () <> ""

(* -------------------------------------------------------------------------- *)
(* --- Cache Management                                                   --- *)
(* -------------------------------------------------------------------------- *)

let parse_mode ~origin ~fallback = function
  | "none" -> NoCache
  | "update" -> Update
  | "replay" -> Replay
  | "rebuild" -> Rebuild
  | "offline" -> Offline
  | "cleanup" -> Cleanup
  | "" -> raise Not_found
  | m ->
    Wp_parameters.warning ~current:false
      "Unknown %s mode %S (use %s instead)" origin m fallback ;
    raise Not_found

module MODE = WpContext.StaticGenerator(Datatype.Unit)
    (struct
      type key = unit
      type data = mode
      let name = "Wp.Cache.mode"
      let compile () =
        try
          if not (Wp_parameters.CacheEnv.get()) then
            raise Not_found ;
          let origin = "FRAMAC_WP_CACHE" in
          parse_mode ~origin ~fallback:"-wp-cache" (Sys.getenv origin)
        with Not_found ->
        try
          let mode = Wp_parameters.Cache.get() in
          parse_mode ~origin:"-wp-cache" ~fallback:"none" mode
        with Not_found ->
          if Wp_parameters.has_session () || has_dir ()
          then Update else NoCache
    end)

let get_mode = MODE.get
let set_mode m = MODE.set () m

let is_active = function
  | NoCache -> false
  | Replay | Offline | Update | Rebuild | Cleanup -> true

let is_updating = function
  | NoCache | Replay | Offline -> false
  | Update | Rebuild | Cleanup -> true

let time_fits time = function
  | None | Some 0.0 -> true
  | Some limit -> time <= limit

let steps_fits steps = function
  | None | Some 0 -> true
  | Some limit -> steps <= limit

let time_seized time = function
  | None | Some 0.0 -> false
  | Some limit -> limit <= time

let steps_seized steps steplimit =
  steps <> 0 &&
  match steplimit with
  | None | Some 0 -> false
  | Some limit -> limit <= steps

let promote ?timeout ?steplimit (res : VCS.result) =
  match res.verdict with
  | VCS.NoResult | VCS.Computing _ | VCS.Invalid | VCS.Failed -> VCS.no_result
  | VCS.Valid | VCS.Unknown ->
    if not (steps_fits res.prover_steps steplimit) then
      { res with verdict = Stepout }
    else
    if not (time_fits res.prover_time timeout) then
      { res with verdict = Timeout }
    else res
  | VCS.Timeout | VCS.Stepout ->
    if steps_seized res.prover_steps steplimit then
      { res with verdict = Stepout }
    else
    if time_seized res.prover_time timeout then
      { res with verdict = Timeout }
    else (* can be run a longer time or widely *)
      VCS.no_result

let file_from_hash hash =
  let dir = get_usable_dir ~make:true () in
  let file = Printf.sprintf "%s/%s.json" (dir:>string) hash in
  file

let get_cache_result ~mode hash =
  match mode with
  | NoCache | Rebuild -> VCS.no_result
  | Update | Cleanup | Replay | Offline ->
    try
      let hash = Lazy.force hash in
      let file = file_from_hash hash in
      let path = Filepath.Normalized.of_string file in
      if not (Filepath.exists path) then VCS.no_result
      else
        try
          mark_cache ~mode hash ;
          Json.load_file path |> ProofScript.result_of_json
        with err ->
          Wp_parameters.warning ~current:false ~once:true
            "invalid cache entry (%s)" (Printexc.to_string err) ;
          VCS.no_result
    with Not_found -> VCS.no_result

let set_cache_result ~mode hash prover result =
  match mode with
  | NoCache | Replay | Offline -> ()
  | Rebuild | Update | Cleanup ->
    let hash = Lazy.force hash in
    try
      let file = file_from_hash hash in
      let path = Filepath.Normalized.of_string file in
      mark_cache ~mode hash ;
      ProofScript.json_of_result (VCS.Why3 prover) result
      |> Json.save_file path
    with err ->
      Wp_parameters.warning ~current:false ~once:true
        "can not update cache (%s)" (Printexc.to_string err)

let clear_result ~digest prover goal =
  try
    let hash = digest prover goal in
    let file = file_from_hash hash in
    Extlib.safe_remove file
  with err ->
    Wp_parameters.warning ~current:false ~once:true
      "can not clean cache entry (%s)" (Printexc.to_string err)

let cleanup_cache () =
  let mode = get_mode () in
  if mode = Cleanup && (!hits > 0 || !miss > 0) then
    try
      let dir = (get_usable_dir ():>string) in
      if is_global_cache () then
        Wp_parameters.warning ~current:false ~once:true
          "Cleanup mode deactivated with global cache."
      else
        Array.iter
          (fun f ->
             if Filename.check_suffix f ".json" then
               let hash = Filename.chop_suffix f ".json" in
               if not (Hashtbl.mem cleanup hash) then
                 begin
                   incr removed ;
                   Extlib.safe_remove (Printf.sprintf "%s/%s" dir f) ;
                 end
          ) (Sys.readdir dir) ;
    with
    | Unix.Unix_error _ as exn ->
      Wp_parameters.warning ~current:false
        "Can not cleanup cache (%s)" (Printexc.to_string exn)
    | Not_found ->
      Wp_parameters.warning ~current:false
        "Cannot cleanup cache"

type 'a digest =
  Why3Provers.t -> 'a -> string

type 'a runner =
  timeout:float option -> steplimit:int option -> Why3Provers.t -> 'a ->
  VCS.result Task.task

let get_result ~digest ~runner ~timeout ~steplimit prover goal =
  let mode = get_mode () in
  match mode with
  | NoCache -> runner ~timeout ~steplimit prover goal
  | Offline ->
    let hash = lazy (digest prover goal) in
    let result = get_cache_result ~mode hash |> VCS.cached in
    if VCS.is_verdict result then incr hits else incr miss ;
    Task.return result
  | Update | Replay | Rebuild | Cleanup ->
    let hash = lazy (digest prover goal) in
    let result =
      get_cache_result ~mode hash
      |> promote ?timeout ?steplimit |> VCS.cached in
    if VCS.is_verdict result
    then
      begin
        incr hits ;
        Task.return result
      end
    else
      Task.finally
        (runner ~timeout ~steplimit prover goal)
        begin function
          | Task.Result result when VCS.is_verdict result ->
            incr miss ;
            set_cache_result ~mode hash prover result
          | _ -> ()
        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