package frama-c

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

Source file TacSplit.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
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
(**************************************************************************)
(*                                                                        *)
(*  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

module PartitionsQQ : sig
  val destructs_qq :
    Lang.F.pool -> is_forall:bool ->
    Lang.F.QED.term ->
    Lang.F.Vars.t * Lang.F.QED.term

  val get : vars:Lang.F.Vars.t -> Lang.F.term list ->
    int * Lang.F.term list list
end
= struct
  let dkey = Wp_parameters.register_category "tac_split_quantifiers" (* debugging key *)
  let debug fmt = Wp_parameters.debug ~dkey fmt

  let destructs_qq pool ~is_forall t =
    let ctx,a = F.e_open ~pool ~forall:is_forall ~exists:(not is_forall) ~lambda:false t in
    let vars = List.fold_left (fun vars (_,var) -> F.Vars.add var vars) F.Vars.empty ctx
    in vars, a

  type kind_t = Root of F.Tset.t | Node of node_t
  and  node_t = { var: F.Var.t;
                  mutable rank: int;
                  mutable kind: kind_t
                }
  type var2node_t = node_t F.Vmap.t

  let is_root root = match root.kind with
    | Node _ -> false
    | Root _ -> true

  let find (map:var2node_t) var =
    let find_root var root = function
      | None -> (* adds an empty root partition for that [var] *)
        root := Some { var; rank=0; kind=(Root F.Tset.empty) };
        debug ". . find(%a)= %a (inserted)@." Lang.F.pp_var var Lang.F.pp_var var ;
        !root
      | (Some { kind=(Root _); var=debug_var }) as old ->
        debug ". . find(%a)= %a@." Lang.F.pp_var var Lang.F.pp_var debug_var ;
        root := old ;
        old
      | Some ({ kind=(Node _) } as node) ->
        debug ". . find(%a)=" Lang.F.pp_var var ;
        let rec find_aux node =
          debug " %a" Lang.F.pp_var node.var ;
          match node.kind with
          | Node y ->
            let r = find_aux y in
            node.kind <- Node r ; r
          | Root _ -> node
        in
        root := Some (find_aux node);
        debug "@." ;
        !root
    in
    let root = ref None in
    let map = F.Vmap.change find_root var root map in
    let root = match !root with
      | None -> assert false
      | Some root -> root
    in
    assert (is_root root);
    map,root

  let union ((map:var2node_t),rootX) varY =
    debug "< union(%a,%a)@." Lang.F.pp_var rootX.var Lang.F.pp_var varY ;
    assert (is_root rootX);
    let map,rootY = find map varY in
    assert ((rootX == rootY) = (0 = F.Var.compare rootX.var rootY.var)) ;
    if rootX == rootY then begin
      debug "> union(%a,%a)=%a@." Lang.F.pp_var rootX.var Lang.F.pp_var varY Lang.F.pp_var rootX.var ;
      map,rootX
    end
    else
      let terms root = match root.kind with
        | Node _ -> assert false
        | Root terms -> terms
      in
      let root, node =
        if rootX.rank < rootY.rank then rootY, rootX
        else (if rootX.rank = rootY.rank then rootX.rank <- 1+rootX.rank;
              rootX,rootY)
      in
      root.kind <- Root (F.Tset.union (terms rootX) (terms rootY));
      node.kind <- Node root ;
      assert (is_root root);
      debug "> union(%a,%a)=%a@." Lang.F.pp_var rootX.var Lang.F.pp_var varY Lang.F.pp_var root.var ;
      map,root

  let partitions ~vars es =
    let debug_term_nth = ref 0 in
    let partitions (set,map) term =
      incr debug_term_nth ;
      let vars = F.Vars.inter vars (Lang.F.vars term) in
      match F.Vars.elements vars with
      | [] ->
        debug "- term #%d: no vars -> %a@." !debug_term_nth Lang.F.pp_term term;
        (F.Tset.add term set), map (* closed term partition *)
      | var::others -> (* term partition bound to variables *)
        debug "- term #%d: nb vars=%d -> %a@." !debug_term_nth (1+List.length others) Lang.F.pp_term term;
        let map,root = List.fold_left union (find map var) others in
        (* adds the current term to the partition *)
        (match root.kind with
         | Node _ -> assert false
         | Root terms ->
           root.kind <- Root (F.Tset.add term terms));
        set,map
    in
    debug "------------@.Partitions(vars #%d,terms #%d)@." (F.Vars.cardinal vars) (List.length es);
    List.fold_left partitions (F.Tset.empty,F.Vmap.empty) es

  let extract (set,map) =
    debug "------------@.Extract@.no vars: nb terms = %d@." (F.Tset.cardinal set);
    let acc = if F.Tset.is_empty set then 0, [] else 1, [set] in
    let extract var node ((nb_parts,parts) as acc) =
      if 0 != F.Var.compare node.var var then acc
      else match node.kind with
        | Root part -> assert (not (F.Tset.is_empty part));
          debug "var %a, nb terms = %d@." Lang.F.pp_var var (F.Tset.cardinal part);
          (nb_parts+1),part::parts
        | Node _ -> acc
    in
    let ((nb_part,_) as r) = F.Vmap.fold extract map acc in
    assert (nb_part > 0);
    r

  let get ~vars es =
    let nbparts, parts = extract (partitions ~vars es) in
    let sorted_ts e = List.sort Lang.F.compare @@ Lang.F.Tset.elements e in
    let sort_es = List.sort (Extlib.list_compare Lang.F.compare) in
    let parts = sort_es @@ List.map sorted_ts parts in
    nbparts, parts
end

open Lang.F
open Conditions
open Tactical

(* -------------------------------------------------------------------------- *)
(* --- Split Tactical                                                     --- *)
(* -------------------------------------------------------------------------- *)
let bind qq ~vars p = F.Vars.fold (F.e_bind qq) vars p

class split =
  object
    inherit Tactical.make
        ~id:"Wp.split"
        ~title:"Split"
        ~descr:"Decompose logical connectives and conditionals."
        ~params:[]

    method select feedback (s : Tactical.selection) =
      let split_cmp at title x y =
        feedback#set_title title ;
        feedback#set_descr
          "Decompose into three comparisons (lt, eq, gt)." ;
        let cases = [
          "Lt",F.p_bool (e_lt x y);
          "Eq",F.p_bool (e_eq x y);
          "Gt",F.p_bool (e_lt y x);
        ] in
        Applicable (Tactical.insert ?at cases)
      in
      let split_leq at x y = split_cmp at "Split (<=)" x y in
      let split_eq at x y = split_cmp at "Split (=)" x y in
      let split_neq at x y = split_cmp at "Split (<>)" x y in
      let split_lt at x y =
        let x = if F.is_int x then F.(e_add x e_one) else x in
        split_cmp at "Split (<)" x y
      in
      match s with
      | Empty | Compose _ | Multi _ -> Not_applicable
      | Inside(_,e) ->
        begin
          let at = Tactical.at s in
          let open Qed.Logic in
          match Lang.F.repr e with
          | Leq(x,y) -> split_leq at x y
          | Lt(x,y) -> split_lt at x y
          | Eq(x,y) when not (is_prop x || is_prop y) -> split_eq at x y
          | Neq(x,y) when not (is_prop x || is_prop y) -> split_neq at x y
          | _ when F.is_prop e ->
            feedback#set_title "Split (true,false)" ;
            feedback#set_descr "Decompose between boolean values." ;
            let cases = ["True",F.p_bool e;"False",F.p_not (F.p_bool e)] in
            let at = Tactical.at s in
            Applicable (Tactical.insert ?at cases)
          | _ -> Not_applicable
        end
      | Clause(Goal p) ->
        begin
          let open Qed.Logic in
          match Lang.F.e_expr p with
          | Bind (Exists,_,_) -> begin
              let vars,q = PartitionsQQ.destructs_qq feedback#pool ~is_forall:false (e_prop p) in
              match Lang.F.repr q with
              | If (c,p,q) ->
                if F.Vars.is_empty (F.Vars.inter (F.vars c) vars) then
                  begin
                    (* unbound condition: proceed by case *)
                    feedback#set_title "Split (exists if)" ;
                    feedback#set_descr
                      "Split unbound condition into branches." ;
                    let p = F.e_imply [c] (bind Exists ~vars p) in
                    let q = F.e_imply [e_not c] (bind Exists ~vars q) in
                    Applicable (Tactical.split [
                        "Then" , F.p_bool p ;
                        "Else" , F.p_bool q ;
                      ])
                  end
                else
                  begin
                    feedback#set_title "Split (rewrite exists if)" ;
                    feedback#set_descr
                      "Rewrite into a disjunction \
                       and distribute the quantifier under." ;
                    let p = bind Exists ~vars (F.e_and [c;p]) in
                    let q = bind Exists ~vars (F.e_and [(e_not c); q]) in
                    let cases = [ "Split" , F.p_bool (F.e_or [p;q]) ] in
                    Applicable (Tactical.split cases)
                  end
              | Or es ->
                feedback#set_title "Split (exists or)" ;
                feedback#set_descr
                  "Distributes the quantifier under the disjunction." ;
                let p = F.e_or (List.map (bind Exists ~vars) es) in
                let cases = [ "Split" , F.p_bool p ] in
                Applicable (Tactical.split cases)
              | Imply (es, p) ->
                feedback#set_title "Split (exists imply)" ;
                feedback#set_descr
                  "Distributes the quantifier under the implication." ;
                let p = F.e_imply (List.map (bind Forall ~vars) es)
                    (bind Exists ~vars p) in
                let cases = [ "Split" , F.p_bool p ] in
                Applicable (Tactical.split cases)
              | And es ->
                let nb_parts,parts = PartitionsQQ.get ~vars es in
                if nb_parts=1 then Not_applicable
                else begin
                  feedback#set_title "Split (exists and)" ;
                  feedback#set_descr
                    "Decompose the quantifier into %d parts." nb_parts ;
                  let bind es =
                    bind Exists ~vars (F.e_and es) in
                  let goal i n es =
                    Printf.sprintf "Goal %d/%d" i n , F.p_bool (bind es) in
                  Applicable (Tactical.split (Tactical.mapi goal parts))
                end
              | _ -> Not_applicable
            end
          | And es ->
            let n = List.length es in
            feedback#set_title "Split (and)" ;
            feedback#set_descr
              "Decompose between the %d parts of the conjunction." n ;
            let goal i n e = Printf.sprintf "Goal %d/%d" i n , F.p_bool e in
            Applicable (Tactical.split (Tactical.mapi goal es))
          | Eq(x,y) when (F.is_prop x) && (F.is_prop y) ->
            feedback#set_title "Split (iff)" ;
            feedback#set_descr "Turn equivalence into implications." ;
            let p = F.p_bool (F.e_imply [x] y) in
            let q = F.p_bool (F.e_imply [y] x) in
            let cases = [ "Necessity" , p ; "Sufficiency" , q ] in
            Applicable (Tactical.split cases)
          | Neq(x,y) when (F.is_prop x) && (F.is_prop y) ->
            feedback#set_title "Split (xor)" ;
            feedback#set_descr "Turn dis-equivalence into implications" ;
            let p = F.p_bool (F.e_imply [x] (e_not y)) in
            let q = F.p_bool (F.e_imply [y] (e_not x)) in
            let cases = [ "Necessity" , p ; "Sufficiency" , q ] in
            Applicable (Tactical.split cases)
          | If(c,p,q) -> (* Split + intro *)
            feedback#set_title "Split (if)" ;
            feedback#set_descr "Decompose conditional into branches." ;
            let p = F.p_bool (F.e_imply [c] p) in
            let q = F.p_bool (F.e_imply [e_not c] q) in
            let cases = [ "Then" , p ; "Else" , q ] in
            Applicable (Tactical.split cases)
          | _ ->
            Not_applicable
        end
      | Clause(Step step) ->
        begin
          match step.condition with
          | State _ | Probe _ -> Not_applicable
          | Branch(p,_,_) ->
            feedback#set_title "Split (branch)" ;
            feedback#set_descr "Decompose conditional into branches." ;
            let cases = [ "Then" , p ; "Else" , p_not p ] in
            Applicable (Tactical.insert ~at:step.id cases)
          | Either seqs ->
            let n = List.length seqs in
            feedback#set_title "Split (switch)" ;
            feedback#set_descr "Decompose each %d cases." n ;
            let either i n s = Printf.sprintf "Case %d/%d" i n , Either [s] in
            let cases = Tactical.mapi either seqs in
            Applicable (Tactical.replace ~at:step.id cases)
          | (Type p | Have p | When p | Core p | Init p) ->
            begin
              let open Qed.Logic in
              match F.e_expr p with
              | Bind (Forall,_,_) -> begin
                  let vars,q = PartitionsQQ.destructs_qq feedback#pool ~is_forall:true (e_prop p) in
                  match Lang.F.repr q with
                  | If (c,p,q) ->
                    if F.Vars.is_empty (F.Vars.inter (F.vars c) vars) then
                      begin (* unbound condition: so, the If is considered as a disjunction *)
                        feedback#set_title "Split (forall if)" ;
                        feedback#set_descr "Decompose unbound conditional into branches." ;
                        let p = F.p_bool (F.e_and [c; (bind Exists ~vars p)]) in
                        let q = F.p_bool (F.e_and [(e_not c); (bind Exists ~vars q)]) in
                        let cases = [ "Then" , When p ; "Else" , When q ] in
                        Applicable (Tactical.replace ~at:step.id cases)
                      end
                    else
                      begin
                        feedback#set_title "Split (rewrite forall if)" ;
                        feedback#set_descr "Rewrite the conjunction and distribute the quantifier." ;
                        let p = bind Exists ~vars (F.e_imply [c] p) in
                        let q = bind Exists ~vars (F.e_imply [e_not c] q) in
                        let cases = [ "Split (rewrite exists if)" , When (F.p_bool (F.e_and [p;q])) ] in
                        Applicable (Tactical.replace ~at:step.id cases)
                      end
                  | And es ->
                    feedback#set_title "Split (forall and)" ;
                    feedback#set_descr "Distributes the quantifier under the conjunction." ;
                    let p = F.p_bool (F.e_and (List.map (bind Forall ~vars) es)) in
                    let cases = [ "Split (distrib forall and)" , When p ] in
                    Applicable (Tactical.replace ~at:step.id cases)
                  | Or es ->
                    let nb_parts,parts = PartitionsQQ.get ~vars es in
                    if nb_parts=1 then Not_applicable
                    else begin
                      feedback#set_title "Split (forall or)" ;
                      feedback#set_descr "Decompose the quantifier between %d parts of the disjunction." nb_parts ;
                      let bind es = bind Forall ~vars (F.e_or es) in
                      let goal i n es = Printf.sprintf "Goal %d/%d" i n , When (F.p_bool (bind es)) in
                      let cases = Tactical.mapi goal parts in
                      Applicable (Tactical.replace ~at:step.id cases)
                    end
                  | _ -> Not_applicable
                end
              | Or xs ->
                let n = List.length xs in
                feedback#set_title "Split (or)" ;
                feedback#set_descr "Distinguish the %d parts of the disjunction." n ;
                let hyp i n e = Printf.sprintf "Case %d/%d" i n , When (F.p_bool e) in
                let cases = Tactical.mapi hyp xs in
                Applicable (Tactical.replace ~at:step.id cases)
              | Eq(x,y) when (F.is_prop x)&&(F.is_prop y) ->
                feedback#set_title "Split (iff)";
                feedback#set_descr "Decompose equivalence into booleans." ;
                let p = F.p_bool x in
                let q = F.p_bool y in
                let cases = [
                  "Both True" , When F.(p_and p q) ;
                  "Both False" , When F.(p_and (p_not p) (p_not q)) ;
                ] in
                Applicable (Tactical.replace ~at:step.id cases)
              | Neq(x,y) when (F.is_prop x)&&(F.is_prop y) ->
                feedback#set_title "Split (xor)";
                feedback#set_descr "Decompose Dis-equivalence into booleans." ;
                let p = F.p_bool x in
                let q = F.p_bool y in
                let cases = [
                  "True/False" , When F.(p_and p (p_not q)) ;
                  "False/True" , When F.(p_and (p_not p) q) ;
                ] in
                Applicable (Tactical.replace ~at:step.id cases)
              | Neq(x,y) when not (is_prop x || is_prop y) ->
                split_neq (Some step.id) x y
              | Eq(x,y) when not (is_prop x || is_prop y) ->
                split_eq (Some step.id) x y
              | Lt(x,y) ->
                split_lt (Some step.id) x y
              | Leq(x,y) ->
                split_leq (Some step.id) x y
              | If(c,p,q) ->
                feedback#set_title "Split (if)" ;
                feedback#set_descr "Split conditional into branches." ;
                let p = F.p_bool (F.e_and [c;p]) in
                let q = F.p_bool (F.e_and [e_not c;q]) in
                let cases = [ "Then" , When p ; "Else" , When q ] in
                Applicable (Tactical.replace ~at:step.id cases)
              | And ps ->
                let cond p = (* keep original kind of step *)
                  match step.condition with
                  | Type _ -> Type p
                  | Have _ -> Have p
                  | When _ -> When p
                  | Core _ -> Core p
                  | Init _ -> Init p
                  | _ -> assert false (* see above pattern matching *)
                in
                feedback#set_title "Split (conjunction)" ;
                feedback#set_descr "Split conjunction into different steps." ;
                let ps = List.map (fun p -> cond @@ p_bool p) ps in
                Applicable (Tactical.replace_step ~at:step.id ps)
              | _ ->
                Not_applicable
            end
        end

  end

let tactical = Tactical.export (new split)
let strategy = Strategy.make tactical ~arguments:[]

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