package frama-c

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

Source file TacInstance.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
(**************************************************************************)
(*                                                                        *)
(*  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 Lang
open Tactical

module L = Qed.Logic

(* -------------------------------------------------------------------------- *)
(* --- Instance Tactical                                                  --- *)
(* -------------------------------------------------------------------------- *)

let descr = function
  | 1 -> "First parameter."
  | 2 -> "Second parameter."
  | 3 -> "Third parameter."
  | n -> Printf.sprintf "%d-th parameter." n

let mkparam k =
  Tactical.composer
    ~id:(Printf.sprintf "P%d" k)
    ~title:(Printf.sprintf "#%d" k)
    ~descr:(descr k) ()

let fields,params = List.split (List.map mkparam [1;2;3;4;5;6;7;8;9;10])

let rec has_binder q p =
  match F.repr p with
  | L.Bind(q0,_,_) -> q = q0
  | L.Imply(_,p) -> has_binder q p
  | _ -> false

type bindings = (F.var * selection) list
type env = {
  binder : L.binder ;
  feedback : Tactical.feedback ;
  mutable index : int ;
}

let rec complexity = function
  | [] -> Integer.one
  | (_,v) :: bindings ->
    match v with
    | Tactical.Compose(Tactical.Range(a,b)) when a < b ->
      let n = Integer.of_int (b+1-a) in
      Integer.mul n (complexity bindings)
    | _ -> complexity bindings

let cardinal limit bindings =
  let n = complexity bindings in
  if Integer.le n (Integer.of_int limit)
  then Some (Integer.to_int_exn n) else None

let rec bind_exists bindings property =
  match bindings with
  | [] -> property
  | (x,v) :: bindings ->
    let closed =
      if Tactical.is_empty v then
        Lang.F.p_bind L.Exists x property
      else
        let value = Tactical.selected v in
        Lang.F.p_subst_var x value property
    in bind_exists bindings closed

let rec range x a b w =
  if a <= b then
    ( Printf.sprintf "%s-%d" (fst w) a ,
      Lang.F.p_subst_var x (F.e_int a) (snd w) )
    :: range x (succ a) b w
  else []

let rec bind_ranges pool = function
  | [] -> pool
  | (x,a,b) :: ranges ->
    bind_ranges (List.concat (List.map (range x a b) pool)) ranges

let rec bind_forall ranges bindings property =
  match bindings with
  | (x,v) :: bindings ->
    begin
      match v with
      | Tactical.Compose(Tactical.Range(a,b)) when a < b ->
        bind_forall ((x,a,b)::ranges) bindings property
      | Tactical.Empty ->
        bind_forall ranges bindings (Lang.F.p_bind L.Forall x property)
      | _ ->
        let value = Tactical.selected v in
        bind_forall ranges bindings (Lang.F.p_subst_var x value property)
    end
  | [] ->
    bind_ranges [ "Instance" , property ] ranges

let instance_goal ?(title="Witness") bindings property sequent =
  [ title, (fst sequent , bind_exists bindings property) ]

let instance_have ?(title="Instance") ?at bindings property sequent =
  let clauses = List.map
      (fun (descr,p) -> Conditions.(step ~descr (Have p)))
      (bind_forall [] bindings property) in
  let step = match clauses with
    | [single] -> single
    | _ -> Conditions.(step (Either [sequence clauses]))
  in [ title , Conditions.insert ?at step sequent ]

let bind ~side bindings property : Tactical.process =
  match side with
  | None ->
    instance_goal ~title:"Witness" bindings property
  | Some (s : Conditions.step) ->
    instance_have ?title:s.descr ~at:s.id bindings property

let filter tau e =
  try F.Tau.equal tau (F.typeof e)
  with Not_found -> true (* allowed to not restrict usage *)

let fieldname ~range k x =
  Format.asprintf "%s (%a)%t"
    (descr k) F.Tau.pretty (F.tau_of_var x)
    (fun fmt -> if range then Format.pp_print_string fmt "(accept range)")

class instance =
  object(self)
    inherit Tactical.make ~id:"Wp.instance"
        ~title:"Instance"
        ~descr:"Instantiate properties."
        ~params

    method private wrap env lemma fields =
      match F.repr lemma , fields with
      | L.Imply(hs,p) , _ when env.binder = L.Forall &&
                               has_binder env.binder p ->
        let bindings,property = self#wrap env p fields in
        bindings, F.e_imply hs property
      | L.Bind(q,tau,phi) , fd :: fields when q = env.binder ->
        env.index <- succ env.index ;
        let x = F.fresh env.feedback#pool tau in
        let v = self#get_field fd in
        let range = match tau with L.Int -> true | _ -> false in
        let tooltip = fieldname ~range env.index x in
        env.feedback#update_field
          ~tooltip ~range ~enabled:true ~filter:(filter tau) fd ;
        let lemma = F.QED.e_unbind x phi in
        let bindings,property = self#wrap env lemma fields in
        (x,v) :: bindings , property
      | _ ->
        List.iter (env.feedback#update_field ~enabled:false) fields ;
        [] , lemma

    method private configure ~side feedback p =
      let binder = match side with None -> L.Exists | Some _ -> L.Forall in
      let lemma = F.e_prop p in
      if has_binder binder lemma then
        let env = { index = 0 ; feedback ; binder } in
        let bindings,phi = self#wrap env lemma fields in
        if List.exists (fun (_,v) -> not (Tactical.is_empty v)) bindings
        then
          match cardinal 1000 bindings with
          | Some n ->
            if n > 1 then
              feedback#set_descr "Generates %d instances." n ;
            Applicable (bind ~side bindings (F.p_bool phi))
          | None ->
            feedback#set_error "More than 1,000 instances." ;
            Not_configured
        else Not_configured
      else
        Not_applicable

    method select feedback sel =
      match sel with
      | Inside(Step s,t) when F.is_prop t ->
        let hs = Conditions.have s in
        let p = F.p_bool t in
        begin match F.p_expr hs with
          | L.And ps when List.memq p ps ->
            self#configure ~side:(Some s) feedback p
          | _ -> Not_applicable
        end
      | Clause(Step s) ->
        let open Conditions in
        begin match s.condition with
          | Have p | When p | Init p | Core p ->
            self#configure ~side:(Some s) feedback p
          | _ -> Not_applicable
        end
      | Clause(Goal p) ->
        self#configure ~side:None feedback p
      | _ -> Not_applicable

  end

let tactical = Tactical.export (new instance)

let rec wrap fs vs =
  match fs , vs with
  | f :: fs , v :: vs ->
    Strategy.arg f v :: (wrap fs vs)
  | fs , _ ->
    List.map (fun f -> Strategy.arg f Empty) fs

let strategy ?(priority=1.0) selection values =
  Strategy.{
    priority ; tactical ; selection ;
    arguments = wrap fields values ;
  }
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