package frama-c

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

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

(* -------------------------------------------------------------------------- *)
(* --- Prover Implementation against Task API                             --- *)
(* -------------------------------------------------------------------------- *)

open Task
open Wpo

let dispatch ?(config=VCS.default) mode prover wpo =
  begin
    match prover with
    | Qed | Tactical -> Task.return VCS.no_result
    | Why3 prover ->
      let smoke = Wpo.is_smoke_test wpo in
      let kf = match Wpo.get_scope wpo with
        | Global -> None
        | Kf kf -> Some kf
      in
      ProverWhy3.prove
        ~timeout:(VCS.get_timeout ?kf ~smoke config)
        ~steplimit:(VCS.get_stepout config)
        ~memlimit:(VCS.get_memlimit config)
        ~mode ~prover wpo
  end

let started ?start wpo =
  match start with
  | None -> ()
  | Some f -> f wpo

let signal ?progress wpo msg =
  match progress with
  | None -> ()
  | Some f -> f wpo msg

let update ?result wpo prover res =
  Wpo.set_result wpo prover res ;
  match result with
  | None -> ()
  | Some f -> f wpo prover res

let run_prover wpo ?config ?(mode=Batch) ?progress ?result prover =
  signal ?progress wpo (VCS.name_of_prover prover) ;
  dispatch ?config mode prover wpo >>>
  fun status ->
  let res = match status with
    | Task.Result r -> r
    | Task.Canceled -> VCS.no_result
    | Task.Timeout t -> VCS.timeout t
    | Task.Failed exn -> VCS.failed (error exn)
  in
  let res = { res with solver_time = Wpo.qed_time wpo } in
  update ?result wpo prover res ;
  Task.return (VCS.is_valid res)

let simplify ?start ?result ?(commit=false) wpo =
  Server.Main.async
    (fun wpo ->
       let r = Wpo.get_result wpo VCS.Qed in
       VCS.( r.verdict == Valid ) ||
       begin
         started ?start wpo ;
         let ok = Wpo.reduce wpo in
         if commit || ok then
           let time = qed_time wpo in
           let verdict = if ok then VCS.Valid else VCS.Unknown in
           let presult = VCS.result ~time verdict in
           (update ?result wpo VCS.Qed presult ; ok)
         else false
       end)
    wpo

let prove wpo ?config ?mode ?start ?progress ?result prover =
  simplify ?start ?result wpo >>= fun succeed ->
  if succeed
  then Task.return true
  else (run_prover wpo ?config ?mode ?progress ?result prover)

let spawn wpo ~delayed
    ?config ?start ?progress ?result ?success ?pool provers =
  let provers = List.filter (fun (_,p) -> p <> Qed) provers in
  if provers<>[] then
    let monitor = match success with
      | None -> None
      | Some on_success ->
        Some
          begin function
            | None -> on_success wpo None
            | Some prover ->
              let r = Wpo.get_result wpo VCS.Qed in
              let prover =
                if VCS.( r.verdict == Valid ) then VCS.Qed else prover in
              on_success wpo (Some prover)
          end in
    let process (mode,prover) =
      prove wpo ?config ~mode ?start ?progress ?result prover in
    let all = Wp_parameters.RunAllProvers.get() in
    let smoke = Wpo.is_smoke_test wpo in
    ProverTask.spawn ?monitor ?pool ~all ~smoke
      (List.map
         (fun mp ->
            let prover = snd mp in
            let task = if delayed then Task.later process mp else process mp in
            prover , task
         ) provers)
  else
    let process = simplify ?start ?result ~commit:true wpo >>= fun ok ->
      begin
        match success with
        | None -> ()
        | Some on_success ->
          on_success wpo (if ok then Some VCS.Qed else None) ;
      end ;
      Task.return ()
    in
    let thread = Task.thread process in
    let server = ProverTask.server () in
    Task.spawn server ?pool thread

(* -------------------------------------------------------------------------- *)
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