package frama-c

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

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

let select_op f =
  let rewrite descr u v = Tactical.rewrite [ descr , F.p_true , u , v ] in
  let rewrite_lsl e a n =
    (* from selection e='a<<n', rewrites the sequent 'Hs |- G' into:
       - Hs[e := a*2^n] |- G[e := a*2^n)] *)
    let b = F.e_mul a (F.e_int (1 lsl n)) in
    rewrite "shift" e b
  in
  let rewrite_lsr e a n =
    (* from selection e='a>>n', rewrites the sequent 'Hs |- G' into:
       - Hs |- 0<=a
       - Hs[e := a*2^n] |- G[e := a*2^n] *)
    let b = F.e_div a (F.e_int (1 lsl n)) in
    (fun seq -> ("positive" , (fst seq , F.p_leq F.e_zero a)) ::
                rewrite "shift" e b seq)
  in
  if f == Cint.f_lsl then rewrite_lsl else
  if f == Cint.f_lsr then rewrite_lsr else
    raise Not_found

let select_int n =
  match F.repr n with
  | Qed.Logic.Kint n ->
    (try Integer.to_int_exn n with Z.Overflow -> raise Not_found)
  | _ -> raise Not_found

class shift =
  object
    inherit Tactical.make
        ~id:"Wp.shift"
        ~title:"Logical Shift"
        ~descr:"Transform logical shifts into divisions and multiplications."
        ~params:[]

    method select feedback selection =
      let e = Tactical.selected selection in
      let open Qed.Logic in
      match F.repr e with
      | Fun( f , [a;n] ) ->
        begin
          let rewrite_shift = select_op f in
          let n = select_int n in
          if n > 64 then feedback#set_error "Too large shift (64 max.)" ;
          if n < 0 then feedback#set_error "Negative shift (0 min.)" ;
          Tactical.Applicable (rewrite_shift e a n)
        end
      | _ -> Tactical.Not_applicable

  end

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

(* -------------------------------------------------------------------------- *)
(* --- Auto Shift                                                         --- *)
(* -------------------------------------------------------------------------- *)

let is_shift e =
  try
    let open Qed.Logic in
    match F.repr e with
    | Fun( f , [_;n] ) ->
      let _ignore = select_op f in
      let _ = select_int n in
      true
    | _ -> false
  with Not_found -> false

let rec scan m f e =
  if not (F.Tset.mem e !m) then
    begin
      m := F.Tset.add e !m ;
      if is_shift e then f e else
      if F.lc_closed e then
        F.lc_iter (scan m f) e
    end

class autoshift =
  object

    method id = "wp:bitshift"
    method title = "Auto Bit-Shift"
    method descr = "Decompose logical shifts from current goal."

    method search push (seq : Conditions.sequent) =
      let goal = snd seq in
      let apply e =
        let selection = Tactical.(Inside(Goal goal,e)) in
        push (strategy ~priority:0.5 selection)
      in
      scan (ref F.Tset.empty) apply (F.e_prop goal)

  end

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