package frama-c

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

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

let title_no_revert = "Revert (current: a & m -> a % m+1)"
let title_revert = "Revert (current: m & a -> a % m+1)"

let v_revert,p_revert =
  Tactical.checkbox ~id:"Wp.modmask.revert"
    ~title:title_no_revert
    ~descr:"Changes operands for modulo."
    ~default:false ()

class modmask =
  object(self)
    inherit Tactical.make
        ~id:"Wp.modmask"
        ~title:"Mod-Mask"
        ~descr:"Converts modulo from/to bitmask."
        ~params:[p_revert]

    method select feedback selection =
      let open Lang.N in
      let open Lang.F in
      let open Qed.Logic in

      let e = Tactical.selected selection in
      let at = Tactical.at selection in

      let on_cond = Tactical.condition in
      let replace_with d v = Tactical.rewrite ?at [ d, Lang.F.p_true, e, v ] in

      let update_title ~hard =
        feedback#set_title "Mod-Mask%s" (if hard then " (hard)" else "")
      in
      let update_field ~enabled =
        let revert = self#get_field v_revert in
        let title = if revert then title_revert else title_no_revert in
        feedback#update_field ~enabled v_revert ;
        feedback#update_field ~title v_revert
      in
      let update_display ~hard ~active_field =
        update_title ~hard ;
        update_field ~enabled:active_field
      in
      match Lang.F.repr e with
      | Mod(a, m) ->
        begin
          try
            let m = Cint.l_lsl e_one @@ Cint.match_power2 m in
            let n = Cint.l_and a (m - e_one) in
            let cond = a >= e_zero in

            update_display ~hard:false ~active_field:false ;
            Applicable (on_cond "Mask Guard" cond @@ replace_with "Mask" n)

          with Not_found ->
            let power_of_2 =
              let v = Lang.freshvar ~basename:"n" Lang.t_int in
              let tv = e_var v in
              p_exists [v] ((e_zero <= tv) &&: (m = Cint.l_lsl e_one tv))
            in
            let cond = ((a >= e_zero) &&: (e_zero < m) &&: power_of_2) in
            let n = Cint.l_and a (m - e_one) in

            update_display ~hard:true ~active_field:false ;
            Applicable (on_cond "Mask Guard" cond @@ replace_with "Mask" n)
        end

      | Fun( f , [ a ; b ] ) when Lang.Fun.equal f Cint.f_land ->
        begin
          try
            let a, m =
              try b, Cint.match_power2_minus1 a
              with Not_found -> a, Cint.match_power2_minus1 b
            in

            let cond = a >= e_zero in
            let n = a mod (Cint.l_lsl e_one m) in

            update_display ~hard:false ~active_field:false ;
            Applicable (on_cond "Mod Guard" cond @@ replace_with "Mod" n)

          with Not_found ->
            let a, m = if self#get_field v_revert then b, a else a, b in
            let plus_1_power_of_2 =
              let v = Lang.freshvar ~basename:"n" Lang.t_int in
              let tv = e_var v in
              p_exists [v] (e_zero <= tv &&: (m + e_one = Cint.l_lsl e_one tv))
            in
            let cond =
              ((a >= e_zero) &&: (e_zero <= m) &&: (plus_1_power_of_2)) in
            let n = a mod (m + e_one) in

            update_display ~hard:true ~active_field:true ;
            Applicable (on_cond "Mod Guard" cond @@ replace_with "Mod" n)
        end

      | _ ->
        update_display ~hard:false ~active_field:false ;
        Not_applicable
  end

let modmask = Tactical.export (new modmask)
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