package frama-c

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

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

(* Helpers *)
let is_positive e = F.p_leq F.e_zero e (* 0 <= n *)
let is_negative e = F.p_lt e F.e_zero  (* n < 0 *)

(* Requires 2^i < n && 0 <= i < j *)
let rec log2m i j n =
  let b = Integer.two_power_of_int j in
  if Integer.lt b n then log2m j (2*j) n else
    (* 2^i < n <= 2^j *)
  if Integer.equal b n then j else
    (* 2^i < n < 2^j *)
    log2d i j n

(* Requires 2^i < n < 2 ^j && 0 <= i < j *)
and log2d i j n =
  if succ i = j then i else
    let k = (i+j)/2 in
    let a = Integer.two_power_of_int k in
    let c = Integer.compare a n in
    if c > 0 then log2d i k n else (* a=2^k > n *)
    if c < 0 then log2d k j n else (* a=2^k < n *)
      k

(* Theorem LAND-1: derived from Cbits.uint_land_range
   exists i, 0 <= e_i <= n
   -----------------------------
   0 <= land(e_1,...,e_n) <= n

   Theorem LAND-2: partially derived from Cbits.sint_land_inf
   forall i, -2^p <= e_i <= n < 0
   -------------------------------------------
   -2^p <= land(e_1,...,e_n) <= e_i <= n < 0
*)

let land_leq ~positive es n = (* land(e_1,...,e_n) <= n *)
  if Integer.(le zero n) then
    (* From theorem LAND-1 when 0<=n:
       (exist i, 0 <= e_i <= n) |- 0 <= land(e_1,...,e_n) <= n *)
    let a = F.e_zint n in
    let case1 = F.p_any (fun e -> F.p_and (is_positive e) (F.p_leq e a)) es in
    if positive then case1 else
      (* From theorem LAND-2: when 0 <= n
         (forall i, e_i < 0) && -1 <= 0 <= n |- land(e_1,...e_n) <= -1 <= 0 <= n *)
      let case2 = F.p_any is_negative es in
      F.p_or case1 case2
  else if positive then raise Not_found else
    (* From theorem LAND-2 when n<0:
       (forall i, e_i <= n < 0) |- land(e_1,...,e_n) <= n < 0*)
    let a = F.e_zint n in
    let case1 = F.p_any (fun e -> F.p_leq e a) es in
    if Integer.(lt n minus_one) then case1 else
      (* From theorem LAND-2: when -1 == n
         (forall i, e_i < 0) && -1 <= 0 <= n |- land(e_1,...e_n) <= -1 <= 0 <= n *)
      let case2 = F.p_any is_negative es in
      F.p_or case1 case2

let leq_land ~positive n es = (* n <= land(e_1,...,e_n) *)
  if Integer.(le n zero) then
    (* From theorem LAND-1 when n<=0:
       (exist i, n <= 0 <= e_i) |- n <= 0 <= land(e_1,...,e_n) *)
    F.p_any is_positive es
  else
  if positive then raise Not_found else
    let p = log2m 0 1 (Integer.neg n) in
    (* Have n <= -2^p < 0
       From theorem LAND-2: when n <= -2^p < 0
       (forall i, n <= -2^p <= e_i < 0) |- n <= land(e_1,...e_n) < 0 *)
    let a = F.e_zint Integer.(neg (two_power_of_int p)) in
    F.p_all (fun e -> F.p_and (is_negative e) (F.p_lt a e)) es

(* Theorem LOR-1: partially derived from Cbits.uint_lor_inf
   forall i, 0 <= e_i <= 2^p-1
   -----------------------------
   forall i, 0 <= e_i <= lor(e_1,...,e_n) <= 2^p-1

   Theorem LOR-2: derived from Cbits.sint_lor_range
   exist i, e_i <= n < 0
   -----------------------------
   n <= lor(e_1,...,e_n) < 0
*)

let lor_leq ~positive es n = (* lor(e_1,...,e_n) <= n *)
  if Integer.(le zero n) then
    let p = log2m 0 1 (Integer.succ n) in
    (* Have 0 <= 2^p <= n+1, hence 0 <= 2^p-1 <= n.
       From theorem LOR-1 when 0 <= 2^p-1 <= n
       (forall i, 0<= e_i <= 2^p-1 <=n) ==> 0<=lor(e_1,...,e_n) <= 2^p-1 <=n *)
    let a = F.e_zint (Integer.two_power_of_int p) in
    let case1 = F.p_all (fun e -> F.p_and (is_positive e) (F.p_lt e a)) es in
    if positive then case1 else
      (* From theorem LOR-2 when 0<=n:
         (exist i, e_i < 0 <= n) |- lor(e_1,...,e_n) < 0 <= n*)
      let case2 = F.p_any is_negative es in
      F.p_or case1 case2
  else
    raise Not_found

let leq_lor ~positive n es = (* n <= lor(e_1,...,e_n) *)
  if Integer.(le zero n) then
    (* From theorem LOR-1 when 0<=n:
       (forall i, 0 <= n <= e_i) |- 0 <= n <= lor(e_1,...,e_n) *)
    let a = F.e_zint n in
    F.p_all (fun e -> F.p_leq a e) es
  else
  if positive then raise Not_found
  else
    (* From theorem LOR-1 when n<0:
       (forall i, n < 0 <= e_i) |- n < 0 <= lor(e_1,...,e_n) *)
    let case1 = F.p_all is_positive es in
    (* From theorem LOR-2 when n<0:
         (exist i, n <= e_i < 0) |- n <= lor(e_1,...,e_n) < 0 *)
    let a = F.e_zint n in
    let case2 = F.p_any (fun e -> F.p_and (F.p_leq a e) (is_negative e)) es in
    F.p_or case1 case2

(* -------------------------------------------------------------------------- *)
(* --- Patterns                                                           --- *)
(* -------------------------------------------------------------------------- *)

type pattern =
  | LEQ of pattern * pattern
  | LT of pattern * pattern
  | INT
  | LAND
  | LOR

type sigma = {
  plor : bool ;
  pland : bool ;
  mutable bound : Integer.t ;
  mutable terms : F.term list ;
}

let rec pmatch s p e =
  let open Qed.Logic in
  match p , F.repr e with
  | LEQ(p,q) , Leq(a,b)
  | LT(p,q) , Lt(a,b)
    -> pmatch s p a ; pmatch s q b
  | INT , Kint n -> s.bound <- n
  | LAND , Fun(f,es) when f == Cint.f_land -> s.terms <- es
  | LOR , Fun(f,es) when f == Cint.f_lor -> s.terms <- es
  | _ -> raise Exit

let matches s p e = try pmatch s p e ; true with Exit -> false

let patterns : (pattern * (sigma -> F.pred)) list =
  [
    LEQ(INT,LAND) , (fun s -> leq_land ~positive:s.pland s.bound s.terms) ;
    LT(INT,LAND) , (fun s -> leq_land ~positive:s.pland (Integer.succ s.bound) s.terms) ;
    LEQ(LAND,INT) , (fun s -> land_leq ~positive:s.pland s.terms s.bound) ;
    LT(LAND,INT) , (fun s -> land_leq ~positive:s.pland s.terms (Integer.pred s.bound)) ;
    LEQ(INT,LOR) , (fun s -> leq_lor ~positive:s.plor s.bound s.terms) ;
    LT(INT,LOR) , (fun s -> leq_lor ~positive:s.plor (Integer.succ s.bound) s.terms) ;
    LEQ(LOR,INT) , (fun s -> lor_leq ~positive:s.plor s.terms s.bound) ;
    LT(LOR,INT) , (fun s -> lor_leq ~positive:s.plor s.terms (Integer.pred s.bound)) ;
  ]

let select_goal ~pland ~plor g =
  try
    let s = { pland ; plor ; bound = Integer.zero ; terms = [] } in
    let (_,f) = List.find (fun (p,_) -> matches s p g) patterns in
    Some (f s)
  with Not_found -> None

let rec split_goals ~pland ~plor others ranges = function
  | [] -> List.rev others , List.rev ranges
  | g::gs ->
    begin
      match select_goal ~pland ~plor g with
      | None -> split_goals ~pland ~plor (F.p_bool g::others) ranges gs
      | Some g' -> split_goals ~pland ~plor others (g'::ranges) gs
    end

let range_goal g' (hs,_) = ["bit-range" , (hs,g')]
let range_goals gs' (hs,_) = List.map (fun g' -> "bit-range" , (hs,g')) gs'
let other_goals ps (hs,_) = List.map (fun p -> "split" , (hs,p)) ps

open Tactical

let positive_land =
  Tactical.checkbox
    ~id:"positive-land"
    ~title:"Pos."
    ~descr:"Requires to obtain a result from (at least one) positive operands"
    ~default:true ()

let positive_lor =
  Tactical.checkbox
    ~id:"positive-lor"
    ~title:"Neg."
    ~descr:"Restrict to obtain a positive result from (all) positive operands"
    ~default:true ()

class bitrange =
  object(self)
    inherit Tactical.make
        ~id:"Wp.bitrange"
        ~title:"Bit Range"
        ~descr:"Compute bounds of bitwise operators."
        ~params:[snd positive_land;snd positive_lor]

    method select feedback = function
      | Clause(Goal p) ->
        begin
          let goals =
            let e = F.e_prop p in
            match F.repr e with
            | Qed.Logic.And es -> es
            | Qed.Logic.Leq _ | Qed.Logic.Lt _ -> [e]
            | _ -> raise Not_found
          in
          let pland = self#get_field (fst positive_land) in
          let plor = self#get_field (fst positive_lor) in
          let others,ranges = split_goals ~pland ~plor [] [] goals in
          if ranges = [] then Tactical.Not_applicable else
            begin
              if others = [] then
                feedback#set_title "Split & Bit Range(s)"
              else
                feedback#set_title "Bit Range(s)" ;
              Tactical.Applicable
                (fun seq -> other_goals others seq @
                            range_goals ranges seq)
            end
        end
      | Inside(Goal p,e) ->
        begin
          let g = F.e_prop p in
          match F.repr g with
          | Qed.Logic.And es when List.memq e es ->
            begin
              let pland = self#get_field (fst positive_land) in
              let plor = self#get_field (fst positive_lor) in
              match select_goal ~pland ~plor g with
              | Some g' -> Tactical.Applicable(range_goal g')
              | None -> Tactical.Not_applicable
            end
          | _ -> Tactical.Not_applicable
        end
      | _ -> Tactical.Not_applicable
  end

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

(* -------------------------------------------------------------------------- *)
(* --- Auto Bitrange                                                      --- *)
(* -------------------------------------------------------------------------- *)

let is_bitwised e =
  let open Qed.Logic in
  match F.repr e with
  | Fun(f,_) -> List.memq f Cint.f_bitwised
  | _ -> false

class autobitrange =
  object

    method id = "wp:bitrange"
    method title = "Auto Bit-Range"
    method descr = "Compute bounds of bitwise operations."

    method search push (seq : Conditions.sequent) =
      let goal = snd seq in
      let open Qed.Logic in
      match F.e_expr goal with
      | Lt(x,y) | Leq(x,y) when is_bitwised x || is_bitwised y ->
        push (strategy Tactical.(Clause (Goal goal)))
      | _ -> ()
  end

let () = Strategy.register (new autobitrange)
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