gmp.ml 7.25 KB
Newer Older
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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
(*                                                                        *)
(*  Copyright (C) 2012-2018                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         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 Cil_types

(**************************************************************************)
26
(***************************** mpz types***********************************)
27
28
(**************************************************************************)

29
let mk_dummy_type_info_ref () =
30
31
32
33
34
35
  ref
    { torig_name = "";
      tname = "";
      ttype = TVoid [];
      treferenced = false }

36
37
module type S = sig
  val t: unit -> typ
38
  val t_as_ptr: unit -> typ
39
40
41
42
43
  val is_now_referenced: unit -> unit
  val is_t: typ -> bool
end

module Make(X: sig end) = struct
44

45
  let t_torig_ref = mk_dummy_type_info_ref ()
46
  let t_struct_torig_ref = mk_dummy_type_info_ref ()
47

48
49
  let set_t ty = t_torig_ref := ty
  let set_t_struct ty = t_struct_torig_ref := ty
50

51
  let is_now_referenced () = !t_torig_ref.treferenced <- true
52

53
  let t () = TNamed(!t_torig_ref, [])
54

55
56
57
  (* create a unique shared representation in order to use [==] in [is_t] *)
  let t_as_ptr_info =
    lazy
58
59
      {
        torig_name = "";
60
        tname = !t_struct_torig_ref.tname ^ " *";
61
62
63
64
65
66
        ttype = TArray(
            TNamed(!t_struct_torig_ref, []),
            Some (Cil.one ~loc:Cil_datatype.Location.unknown),
            {scache = Not_Computed},
            []);
        treferenced = true;
67
68
69
70
71
72
73
74
75
      }

  let t_as_ptr () = TNamed (Lazy.force t_as_ptr_info, [])

  let is_t ty = match ty with
    | TNamed(tinfo, []) ->
      tinfo == !t_torig_ref || tinfo == Lazy.force t_as_ptr_info
    | _ -> false

76
77
end

78
module Z = Make(struct end)
79
module Q = Make(struct end)
80
81
82
83
84
85
86

(**************************************************************************)
(******************* Initialization of mpz and mpq types ******************)
(**************************************************************************)

let init_t () =
  Options.feedback ~level:2 "initializing GMP types.";
Julien Signoles's avatar
Julien Signoles committed
87
  let set_mp_t = object (self)
88
    inherit Cil.nopCilVisitor
Julien Signoles's avatar
Julien Signoles committed
89

90
91
    (* exit after having initialized the 4 values (for Z.t and Q.t) *)
    val mutable visited = 0
Julien Signoles's avatar
Julien Signoles committed
92
93
    method private set f info =
      f info;
94
      if visited = 3 then
Julien Signoles's avatar
Julien Signoles committed
95
96
        raise Exit
      else begin
97
        visited <- visited + 1;
Julien Signoles's avatar
Julien Signoles committed
98
99
100
        Cil.SkipChildren
      end

101
    method !vglob = function
102
103
104
105
106
107
108
109
      | GType({ torig_name = name } as info, _) ->
        if name = "__e_acsl_mpz_t" then self#set Z.set_t info
        else if name = "__e_acsl_mpz_struct" then self#set Z.set_t_struct info
        else if name = "__e_acsl_mpq_t" then self#set Q.set_t info
        else if name = "__e_acsl_mpq_struct" then self#set Q.set_t_struct info
        else Cil.SkipChildren
      | _ ->
        Cil.SkipChildren
Julien Signoles's avatar
Julien Signoles committed
110

111
  end in
Julien Signoles's avatar
Julien Signoles committed
112
  try Cil.visitCilFileSameGlobals set_mp_t (Ast.get ()) with Exit -> ()
113
114
115
116
117
118
119
120

(**************************************************************************)
(************************* Calls to builtins ******************************)
(**************************************************************************)

let apply_on_var ~loc funname e =
  let prefix =
    let ty = Cil.typeOf e in
121
122
    if Z.is_t ty then "__gmpz_"
    else if Q.is_t ty then "__gmpq_"
123
124
125
    else assert false
  in
  Misc.mk_call ~loc (prefix ^ funname) [ e ]
126

127
128
129
130
131
132
133
let init ~loc e = apply_on_var "init" ~loc e
let clear ~loc e = apply_on_var "clear" ~loc e

exception Longlong of ikind

let get_set_suffix_and_arg e =
  let ty = Cil.typeOf e in
134
  if Z.is_t ty || Q.is_t ty then "", [ e ]
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
  else
    match Cil.unrollType ty with
    | TInt(IChar, _) ->
      (if Cil.theMachine.Cil.theMachine.char_is_unsigned then "_ui"
       else "_si"),
      [ e ]
    | TInt((IBool | IUChar | IUInt | IUShort | IULong), _) ->
      "_ui", [ e ]
    | TInt((ISChar | IShort | IInt | ILong), _) -> "_si", [ e ]
    | TInt((ILongLong | IULongLong as ikind), _) -> raise (Longlong ikind)
    | TPtr(TInt(IChar, _), _) ->
      "_str",
      (* decimal base for the number given as string *)
      [ e; Cil.integer ~loc:e.eloc 10 ]
    | TFloat((FDouble | FFloat), _) ->
      (* FFloat is a strict subset of FDouble (modulo exceptional numbers)
151
         Hence, calling [set_d] for both of them is sound.
Julien Signoles's avatar
Julien Signoles committed
152
153
         HOWEVER: the machdep MUST NOT be vulnerable to double rounding
         [TODO] check the statement above *)
154
155
156
157
158
159
160
161
      "_d", [ e ]
    | TFloat(FLongDouble, _) ->
      Error.not_yet "creating gmp from long double"
    | _ ->
      assert false

let generic_affect ~loc fname lv ev e =
  let ty = Cil.typeOf ev in
Julien Signoles's avatar
Julien Signoles committed
162
  if Z.is_t ty || Q.is_t ty then begin
163
164
165
166
167
168
169
170
    let suf, args = get_set_suffix_and_arg e in
    Misc.mk_call ~loc (fname ^ suf) (ev :: args)
  end else
    Cil.mkStmtOneInstr ~valid_sid:true (Set(lv, e, e.eloc))

let init_set ~loc lv ev e =
  let fname =
    let ty = Cil.typeOf ev in
171
    if Z.is_t ty then
172
      "__gmpz_init_set"
173
    else if Q.is_t ty then
174
175
176
177
178
179
180
181
182
      Options.fatal "no __gmpq_init_set: init then set separately"
    else
      ""
  in
  try generic_affect ~loc fname lv ev e
  with
  | Longlong IULongLong ->
    (match e.enode with
    | Lval elv ->
183
      assert (Z.is_t (Cil.typeOf ev));
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
      let call = Misc.mk_call
        ~loc
        "__gmpz_import"
        [ ev;
          Cil.one ~loc;
          Cil.one ~loc;
          Cil.sizeOf ~loc (TInt(IULongLong, []));
          Cil.zero ~loc;
          Cil.zero ~loc;
          Cil.mkAddrOf ~loc elv ]
      in
      Cil.mkStmt ~valid_sid:true (Block (Cil.mkBlock [ init ~loc ev; call ]))
    | _ ->
      Error.not_yet "unsigned long long expression requiring GMP")
  | Longlong ILongLong ->
    Error.not_yet "long long requiring GMP"

let affect ~loc lv ev e =
  let fname =
    let ty = Cil.typeOf ev in
204
205
    if Z.is_t ty then "__gmpz_set"
    else if Q.is_t ty then "__gmpq_set"
206
207
208
209
210
211
212
213
214
215
216
    else ""
  in
  try generic_affect ~loc fname lv ev e
  with Longlong _ ->
    Error.not_yet "quantification over long long and requiring GMP"

(*
Local Variables:
compile-command: "make"
End:
*)