package frama-c

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

Source file TacLemma.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
(**************************************************************************)
(*                                                                        *)
(*  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
open Definitions

module L = Qed.Logic

(* -------------------------------------------------------------------------- *)
(* --- Browser                                                           ---- *)
(* -------------------------------------------------------------------------- *)

let named l = {
  vid = l.l_name ;
  title = l.l_name ;
  descr = Pretty_utils.to_string F.pp_pred l.l_lemma ;
  value = l ;
}

class browser ?on_cluster f cluster =
  object(self)

    (* Base Visitor *)
    inherit Definitions.visitor cluster
    method section _ = ()
    method on_library _ = ()
    method on_type _ _ = ()
    method on_comp _ _ = ()
    method on_icomp _ _ = ()
    method on_dfun _ = ()
    method! vtypes = ()
    method! vsymbols = ()
    method! vself = self#vlemmas

    (* Cluster & Lemmas *)

    method on_cluster c =
      match on_cluster with
      | None -> (new browser ~on_cluster:self#vcluster f c)#vlemmas
      | Some visitor -> visitor c

    method on_dlemma l = f (named l)
  end

let browse f s =
  if WpContext.is_defined () then
    begin
      let main = Definitions.cluster ~id:"browser" () in
      let visitor = new browser f main in
      let selection = Tactical.selected s in
      visitor#vterm selection
    end

(* -------------------------------------------------------------------------- *)
(* --- Search Lemma Tactical                                              --- *)
(* -------------------------------------------------------------------------- *)

type env = {
  feedback : Tactical.feedback ;
  lemma : F.pred ;
  descr : string ;
}

type lemma = Definitions.dlemma Tactical.named

let find thm = named (Definitions.find_name thm)

let search,psearch =
  Tactical.search ~id:"lemma" ~title:"Lemma" ~descr:"Lemma to instantiate."
    ~browse ~find ()


let fresh pool { l_forall ; l_lemma } =
  let vars = List.map (F.alpha pool) l_forall in
  let sigma = Lang.subst l_forall (List.map F.e_var vars) in
  vars , F.p_subst sigma l_lemma

class instance =
  object(self)
    inherit Tactical.make ~id:"Wp.lemma"
        ~title:"Lemma"
        ~descr:"Search and instantiate lemmas."
        ~params:(psearch :: TacInstance.params)

    method private hide (feedback : Tactical.feedback) fields =
      List.iter
        (fun fd -> feedback#update_field ~enabled:false fd)
        fields

    method private wrap env vars fields =
      match vars , fields with
      | x::xs , fd::fields ->
        let title = Pretty_utils.to_string F.pp_var x in
        let value = self#get_field fd in
        let tau = F.tau_of_var x in
        env.feedback#update_field ~enabled:true
          ~title ~tooltip:env.descr
          ~range:(match tau with L.Int -> true | _ -> false)
          ~filter:(TacInstance.filter tau) fd ;
        let bindings,lemma = self#wrap env xs fields in
        (x,value)::bindings , lemma
      | _ ->
        self#hide env.feedback fields ;
        [] , F.p_forall vars env.lemma

    method select feedback = function
      | Empty -> Not_applicable
      | selection ->
        begin match self#get_field search with
          | None ->
            self#hide feedback TacInstance.fields ;
            Not_configured
          | Some Tactical.{ title ; value = dlem } ->
            let fields = TacInstance.fields in
            let vars,lemma = fresh feedback#pool dlem in
            let descr = Pretty_utils.to_string F.pp_pred lemma in
            let bindings,lemma =
              self#wrap { feedback ; descr ; lemma } vars fields in
            match TacInstance.cardinal 1000 bindings with
            | Some n ->
              if n > 1 then
                feedback#set_descr "Generates %d instances." n ;
              let at = Tactical.at selection in
              Applicable
                (TacInstance.instance_have ~title ?at bindings lemma)
            | None ->
              feedback#set_error "More than 1,000 instances" ;
              Not_configured
        end
  end

let tactical = Tactical.export (new instance)

let strategy ?(priority=1.0) ?(at = Tactical.int 0) lemma values =
  Strategy.{
    priority ; tactical ; selection = at ;
    arguments =
      arg search (try Some (find lemma) with Not_found -> None) ::
      TacInstance.wrap TacInstance.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