logic_utils.mli 18.1 KB
Newer Older
1
2
3
4
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
Andre Maroneze's avatar
Andre Maroneze committed
5
(*  Copyright (C) 2007-2020                                               *)
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
(*    CEA   (Commissariat à l'énergie atomique et aux énergies            *)
(*           alternatives)                                                *)
(*    INRIA (Institut National de Recherche en Informatique et en         *)
(*           Automatique)                                                 *)
(*                                                                        *)
(*  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).            *)
(*                                                                        *)
(**************************************************************************)

(** Utilities for ACSL constructs.
    @plugin development guide *)

open Cil_types

(** exception raised when a parsed logic expression is
    syntactically not well-formed. *)
32
exception Not_well_formed of location * string
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

(** basic utilities for logic terms and predicates. See also {! Logic_const}
    to build terms and predicates.
    @plugin development guide *)

(** add a logic function in the environment.
    See {!Logic_env.add_logic_function_gen}*)
val add_logic_function : logic_info -> unit

(** {2 Types} *)

(** instantiate type variables in a logic type. *)
val instantiate :
  (string * logic_type) list ->
  logic_type -> logic_type
[@@deprecated "Use Logic_const.instantiate instead."]

(** [is_instance_of poly t1 t2] returns [true] if [t1] can be derived from [t2]
    by instantiating some of the type variable in [poly].

    @since Magnesium-20151001
*)
val is_instance_of: string list -> logic_type -> logic_type -> bool

(** expands logic type definitions. If the [unroll_typedef] flag is set to
    [true] (this is the default), C typedef will be expanded as well. *)
val unroll_type : ?unroll_typedef:bool -> logic_type -> logic_type

(** [isLogicType test typ] is [false] for pure logic types and the result
    of test for C types.
    In case of a set type, the function tests the element type.
*)
val isLogicType : (typ -> bool) -> logic_type -> bool

(** {3 Predefined tests over types} *)
val isLogicArrayType : logic_type -> bool

(** @modify Chlorine-20180501 old behavior renamed as [isLogicAnyCharType] *)
val isLogicCharType : logic_type -> bool

(** @since Chlorine-20180501 *)
val isLogicAnyCharType : logic_type -> bool
val isLogicVoidType : logic_type -> bool
val isLogicPointerType : logic_type -> bool
val isLogicVoidPointerType : logic_type -> bool

(** {3 Type conversions} *)

(** @return the equivalent C type.
    @raise Failure if the type is purely logical *)
val logicCType : logic_type -> typ

(** transforms an array into pointer. *)
val array_to_ptr : logic_type -> logic_type

88
(** C type to logic type, with implicit conversion for arithmetic types.
Andre Maroneze's avatar
Andre Maroneze committed
89
    @since 21.0-Scandium
90
*)
91
val coerce_type : typ -> logic_type
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113

(** {2 Predicates} *)

(** @deprecated use Logic_const.pred_of_id_pred instead *)
val predicate_of_identified_predicate: identified_predicate -> predicate
[@@ deprecated "Use Logic_const.pred_of_id_pred instead"]

(** transforms \old and \at(,Old) into \at(,L) for L a label pointing
    to the given statement, creating one if needed. *)
val translate_old_label: stmt -> predicate -> predicate

(** {2 Terms} *)

(** [true] if the term denotes a C array. *)
val is_C_array : term -> bool

(** creates a TStartOf from an TLval. *)
val mk_logic_StartOf : term -> term

(** creates an AddrOf from a TLval. The given logic type is the
    type of the lval.
    @since Neon-20140301 *)
114
val mk_logic_AddrOf: ?loc:location -> term_lval -> logic_type -> term
115
116
117
118
119
120
121
122
123
124
125
126

(** [true] if the term is a pointer. *)
val isLogicPointer : term -> bool

(** creates either a TStartOf or the corresponding TLval. *)
val mk_logic_pointer_or_StartOf : term -> term

(** creates a logic cast if required, with some automatic simplifications being
    performed automatically. If [force] is [true], the cast will always
    be inserted. Otherwise (which is the default), [mk_cast typ t] will return
    [t] if it is already of type [typ]

127
    @modify Aluminium-20160501 added [force] optional argument *)
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
val mk_cast: ?loc:location -> ?force:bool -> typ -> term -> term


(** [array_with_range arr size] returns the logic term [array'+{0..(size-1)}],
    [array'] being [array] cast to a pointer to char *)
val array_with_range: exp -> term -> term

(** Removes TLogic_coerce at head of term. *)
val remove_logic_coerce: term -> term

(** [numeric_coerce typ t] returns a term with the same value as [t]
    and of type [typ].  [typ] which should be [Linteger] or
    [Lreal]. [numeric_coerce] tries to avoid unnecessary type conversions
    in [t]. In particular, [numeric_coerce (int)cst Linteger], where [cst]
    fits in int will be directly [cst], without any coercion.

144
145
146
147
    Also coerce recursively the sub-terms of t-set expressions
    (range, union, inter and comprehension) and lift the associated
    set type.

148
    @since Magnesium-20151001
Andre Maroneze's avatar
Andre Maroneze committed
149
    @modify 21.0-Scandium
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
*)
val numeric_coerce: logic_type -> term -> term

(** {2 Predicates} *)

(** \valid_index *)
(* val mk_pvalid_index: ?loc:location -> term * term -> predicate *)

(** \valid_range *)
(* val mk_pvalid_range: ?loc:location -> term * term * term -> predicate *)

val pointer_comparable: ?loc:location -> term -> term -> predicate
(** \pointer_comparable
    @since Fluorine-20130401 *)

165
(** {2 Conversion from exp to term} *)
Loïc Correnson's avatar
Loïc Correnson committed
166

167
val expr_to_term : ?coerce:bool -> exp -> term
168
(** Returns a logic term that has exactly the same semantics as the
169
170
171
    original C-expression. The type of the resulting term is determined
    by the [~coerce] flag as follows:
    - when [~coerce:false] is given (the default) the term has the same
172
      c-type as the original expression.
173
174
175
    - when [~coerce:true] is given, if the original expression has an int or
      float type, then the returned term is coerced into the integer or real
      logic type, respectively.
176

177
    Remark: when the original expression is a comparison, it is evaluated as
178
    an [int] or an [integer] depending on the [~coerce] flag.
179
180
181
    To obtain a boolean or predicate, use [expr_to_boolean] or
    [expr_to_predicate] instead.

Andre Maroneze's avatar
Andre Maroneze committed
182
    @modify 21.0-Scandium
183
184
185
186
187
188
*)

val expr_to_predicate: exp -> predicate
(** Returns a predicate semantically equivalent to the condition
    of the original C-expression.

189
    This is different from [expr_to_term e |> scalar_term_to_predicate]
Loïc Correnson's avatar
Loïc Correnson committed
190
    since C-relations are translated into logic ones.
191
192
193
194

    @raise Fatal error if the expression is not a comparison and cannot be
           compared to zero.
    @since Sulfur-20171101
Andre Maroneze's avatar
Andre Maroneze committed
195
    @modify 21.0-Scandium
196
197
*)

198
199
200
201
202
203
204
205
206
val expr_to_ipredicate: exp -> identified_predicate
(** Returns a predicate semantically equivalent to the condition
    of the original C-expression.

    Identical to [expr_to_predicate e |> Logic_const.new_predicate].

    @raise Fatal error if the expression is not a comparison and cannot be
           compared to zero.
    @since Sulfur-20171101
Andre Maroneze's avatar
Andre Maroneze committed
207
    @modify 21.0-Scandium
208
209
210
211
212
213
*)

val expr_to_boolean: exp -> term
(** Returns a boolean term semantically equivalent to the condition
    of the original C-expression.

214
    This is different from [expr_to_term e |> scalar_term_to_predicate]
Loïc Correnson's avatar
Loïc Correnson committed
215
    since C-relations are translated into logic ones.
216
217
218
219

    @raise Fatal error if the expression is not a comparison and cannot be
           compared to zero.
    @since Sulfur-20171101
Andre Maroneze's avatar
Andre Maroneze committed
220
    @modify 21.0-Scandium
221
222
*)

Loïc Correnson's avatar
Loïc Correnson committed
223
224
225
226
227
228
229
230
231
232
233
234
val is_zero_comparable: term -> bool
(** [true] if the given term has a type for which a comparison to 0 exists
    (i.e. scalar C types, logic integers and reals).

    @since Sulfur-20171101
*)

val scalar_term_to_boolean: term -> term
(** Compare the given term with the constant 0 (of the appropriate type)
    to return the result of the comparison [e <> 0] as a boolean term.

    @raise Fatal error if the argument cannot be compared to 0
Andre Maroneze's avatar
Andre Maroneze committed
235
    @since 21.0-Scandium
Loïc Correnson's avatar
Loïc Correnson committed
236
237
*)

238
239
240
241
242
243
244
245
val scalar_term_to_predicate: term -> predicate
(** Compare the given term with the constant 0 (of the appropriate type)
    to return the result of the comparison [e <> 0].

    @raise Fatal error if the argument cannot be compared to 0
    @since Sulfur-20171101
*)

246
247
248
val lval_to_term_lval : lval -> term_lval
val host_to_term_lhost : lhost -> term_lhost
val offset_to_term_offset : offset -> term_offset
249
250
251
252

val constant_to_lconstant: constant -> logic_constant
val lconstant_to_constant: logic_constant-> constant

253
254
255
256
257
258
(** Parse the given string as a float or real logic constant.

    The parsed literal is always kept as it is in the resulting term.
    The returned term is either a real constant or
    real constant casted into a C-float type.

Loïc Correnson's avatar
Loïc Correnson committed
259
260
261
    Unsuffixed literals are considered as real numbers.
    Literals suffixed by [f|d|l] or [F|D|L] are considered
    as float constants of the associated kind. *)
262
val parse_float : ?loc:location -> string -> term
263

Loïc Correnson's avatar
Loïc Correnson committed
264
265
(** {2 Various Utilities} *)

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
(** [remove_term_offset o] returns [o] without its last offset and
    this last offset. *)
val remove_term_offset :
  term_offset -> term_offset * term_offset

(** true if \result is included in the lval. *)
val lval_contains_result : term_lhost -> bool

(** true if \result is included in the offset. *)
val loffset_contains_result : term_offset -> bool

(** true if \result is included in the term *)
val contains_result : term -> bool

(** returns the body of the given predicate.
    @raise Not_found if the logic_info is not the definition of a predicate. *)
val get_pred_body :
  logic_info -> predicate

(** true if the term is \result or an offset of \result. *)
val is_result : term -> bool

val lhost_c_type : term_lhost -> typ

(** [true] if the predicate is Ptrue.
    @since Nitrogen-20111001 *)
val is_trivially_true: predicate -> bool

(** [true] if the predicate is Pfalse
    @since Nitrogen-20111001 *)
val is_trivially_false: predicate -> bool

298
299
300
301
302
(** {2 Code annotations} *)

(** Does the annotation apply to the next statement (e.g. a statement
    contract). Also false for loop-related annotations.

Andre Maroneze's avatar
Andre Maroneze committed
303
    @since 21.0-Scandium
304
305
306
*)
val is_annot_next_stmt: code_annotation -> bool

307
308
309
310
311
312
313
314
(** {2 Global annotations} *)

(** add an attribute to a global annotation
    @since Phosphorus-20170501-beta1
*)
val add_attribute_glob_annot:
  attribute -> global_annotation -> global_annotation

315
316
317
(** {2 Contracts } *)

(** [true] if the behavior has only an assigns clause.
318
    @since 22.0-Titanium
319
320
321
322
*)
val behavior_has_only_assigns: behavior -> bool

(** [true] if the only non-empty fields of the contract are assigns clauses
323
    @since 22.0-Titanium
324
325
326
*)
val funspec_has_only_assigns: funspec -> bool

327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
(** {2 Structural equality between annotations} *)

val is_same_list: ('a -> 'a -> bool) -> 'a list -> 'a list -> bool

val is_same_logic_label :
  logic_label -> logic_label -> bool

(**
   @since Nitrogen-20111001
*)
val is_same_pconstant: Logic_ptree.constant -> Logic_ptree.constant -> bool

val is_same_type : logic_type -> logic_type -> bool
val is_same_var : logic_var -> logic_var -> bool
val is_same_logic_signature :
  logic_info -> logic_info -> bool
val is_same_logic_profile :
  logic_info -> logic_info -> bool
val is_same_builtin_profile :
  builtin_logic_info -> builtin_logic_info -> bool
val is_same_logic_ctor_info :
  logic_ctor_info -> logic_ctor_info -> bool

(** @deprecated Nitrogen-20111001 use {!Cil.compareConstant} instead. *)
val is_same_constant : constant -> constant -> bool
val is_same_term : term -> term -> bool
val is_same_logic_info : logic_info -> logic_info -> bool
val is_same_logic_body : logic_body -> logic_body -> bool
val is_same_indcase :
  string * logic_label list * string list *
  predicate ->
  string * logic_label list * string list *
  predicate -> bool
val is_same_tlval : term_lval -> term_lval -> bool
val is_same_lhost : term_lhost -> term_lhost -> bool
val is_same_offset : term_offset -> term_offset -> bool
val is_same_predicate_node : predicate_node -> predicate_node -> bool
val is_same_predicate : predicate -> predicate -> bool
val is_same_identified_predicate :
  identified_predicate -> identified_predicate -> bool
val is_same_identified_term :
  identified_term -> identified_term -> bool
val is_same_deps : deps -> deps -> bool
val is_same_allocation :
  allocation -> allocation -> bool
val is_same_assigns :
  assigns -> assigns -> bool
val is_same_variant : variant -> variant -> bool
val is_same_post_cond :
  termination_kind * identified_predicate ->
  termination_kind * identified_predicate -> bool
val is_same_behavior : funbehavior -> funbehavior -> bool
val is_same_spec : funspec -> funspec -> bool
val is_same_logic_type_def :
  logic_type_def -> logic_type_def -> bool
val is_same_logic_type_info :
  logic_type_info -> logic_type_info -> bool
val is_same_loop_pragma : loop_pragma -> loop_pragma -> bool
val is_same_slice_pragma : slice_pragma -> slice_pragma -> bool
val is_same_impact_pragma : impact_pragma -> impact_pragma -> bool
val is_same_pragma : pragma -> pragma -> bool
val is_same_code_annotation : code_annotation -> code_annotation -> bool
val is_same_global_annotation : global_annotation -> global_annotation -> bool
val is_same_axiomatic :
  global_annotation list -> global_annotation list -> bool
(** @since Oxygen-20120901 *)
val is_same_model_info: model_info -> model_info -> bool

val is_same_lexpr: Logic_ptree.lexpr -> Logic_ptree.lexpr -> bool

(** hash function compatible with is_same_term *)
val hash_term: term -> int

(** comparison compatible with is_same_term *)
val compare_term: term -> term -> int

val hash_predicate: predicate -> int

val compare_predicate: predicate -> predicate -> int

(** {2 Merging contracts} *)

val get_behavior_names : spec -> string list

(** Concatenates two assigns if both are defined,
    returns WritesAny if one (or both) of them is WritesAny.
    @since Nitrogen-20111001 *)
val concat_assigns: assigns -> assigns -> assigns

(** merge assigns: take the one that is defined and select an arbitrary one
    if both are, emitting a warning unless both are syntactically the same. *)
val merge_assigns : assigns -> assigns -> assigns

(** Concatenates two allocation clauses if both are defined,
    returns FreeAllocAny if one (or both) of them is FreeAllocAny.
    @since Nitrogen-20111001 *)
val concat_allocation: allocation -> allocation -> allocation

(** merge allocation: take the one that is defined and select an arbitrary one
    if both are, emitting a warning unless both are syntactically the same.
    @since Oxygen-20120901 *)
val merge_allocation : allocation -> allocation -> allocation

val merge_behaviors :
431
  ?oldloc:location -> silent:bool -> funbehavior list -> funbehavior list -> funbehavior list
432

433
(** [merge_funspec ?oldloc oldspec newspec] merges [newspec] into [oldspec].
434
    If the funspec belongs to a kernel function, do not forget to call
435
    {!Kernel_function.set_spec} after merging.
Andre Maroneze's avatar
Andre Maroneze committed
436
    @modify 20.0-Calcium add optional parameter [oldloc].
437
*)
438
val merge_funspec :
439
  ?oldloc:location -> ?silent_about_merging_behav:bool ->
440
  funspec -> funspec -> unit
441
442
443
444
445
446
447
448
449
450
451

(** Reset the given funspec to empty.
    @since Nitrogen-20111001 *)
val clear_funspec: funspec -> unit

(** {2 Discriminating code_annotations} *)
(** Functions below allows to test a special kind of code_annotation.
    Use them in conjunction with {!Annotations.get_filter} to retrieve
    a particular kind of annotations associated to a statement. *)

val is_assert : code_annotation -> bool
452
val is_check : code_annotation -> bool
453
454
455
456
457
val is_contract : code_annotation -> bool
val is_stmt_invariant : code_annotation -> bool
val is_loop_invariant : code_annotation -> bool
val is_invariant : code_annotation -> bool
val is_variant : code_annotation -> bool
458
val is_allocation: code_annotation -> bool
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
val is_assigns : code_annotation -> bool
val is_pragma : code_annotation -> bool
val is_loop_pragma : code_annotation -> bool
val is_slice_pragma : code_annotation -> bool
val is_impact_pragma : code_annotation -> bool
val is_loop_annot : code_annotation -> bool

val is_trivial_annotation : code_annotation -> bool

val is_property_pragma : pragma -> bool
(** Should this pragma be proved by plugins *)

val extract_loop_pragma :
  code_annotation list -> loop_pragma list
val extract_contract :
  code_annotation list -> (string list * funspec) list

(** {2 Constant folding} *)

val constFoldTermToInt: ?machdep:bool -> term -> Integer.t option

(**
   A [cilVisitor] (by copy) that simplifies expressions of the type
   [const int x = v], where [v] is an integer and [x] is a global variable.
   Requires a mapping from [varinfo] to [init option]
   (e.g. based on [Globals.Vars.find]).

   @since Silicon-20161101
*)
class simplify_const_lval: (varinfo -> init option) -> Cil.cilVisitor

(** {2 Type-checking hackery} *)

(** give complete types to terms that refer to a variable whose type
    has been completed after its use in an annotation. Internal use only.
    @since Neon-20140301 *)
val complete_types: file -> unit

(** {2 Parsing hackery} *)
(** Values that control the various modes of the parser and lexer for logic.
    Use with care.
*)

val kw_c_mode : bool ref
val enter_kw_c_mode : unit -> unit
val exit_kw_c_mode : unit -> unit
val is_kw_c_mode : unit -> bool
val rt_type_mode : bool ref
val enter_rt_type_mode : unit -> unit
val exit_rt_type_mode : unit -> unit
val is_rt_type_mode : unit -> bool

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