typing.mli 7.06 KB
 Julien Signoles committed Jun 09, 2016 1 2 (**************************************************************************) (* *)  Patrick Baudin committed Oct 15, 2018 3 (* This file is part of the Frama-C's E-ACSL plug-in. *)  Julien Signoles committed Jun 09, 2016 4 (* *)  Julien Signoles committed Nov 04, 2019 5 (* Copyright (C) 2012-2019 *)  Virgile Prevosto committed Apr 12, 2017 6 (* CEA (Commissariat à l'énergie atomique et aux énergies *)  Julien Signoles committed Jun 09, 2016 7 8 9 10 11 12 13 14 15 16 17 18 (* 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 *)  Virgile Prevosto committed Apr 12, 2017 19 (* for more details (enclosed in the file licenses/LGPLv2.1). *)  Julien Signoles committed Jun 09, 2016 20 21 22 (* *) (**************************************************************************)  Julien Signoles committed Jun 09, 2016 23 (** Type system which computes the smallest C type that may contain all the  Julien Signoles committed Jun 09, 2016 24  possible values of a given integer term or predicate. Also compute the  Julien Signoles committed Jun 09, 2016 25 26 27  required casts. It is based on interval inference of module {!Interval}. It implement Figure 4 of J. Signoles' JFLA'15 paper "Rester statique pour  Andre Maroneze committed Dec 05, 2017 28  devenir plus rapide, plus précis et plus mince".  Julien Signoles committed Jun 09, 2016 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45  Example: consider a variable [x] of type [int] and a variable [y] of type char on a (strange) architecture in which values of type [int] belongs to the interval [[-128;127]] and values of type [char] belongs to the interval [[-32;31]], while there are no other integral types. Then here are some information computed from the term [1+(x+1)/(y-64)] by the type system: 1. [x+1] must be a GMP (because of the potential overflow) 2. consequently [x], which is an [int], must be coerced into a GMP and the same for the number 1 in this addition. 3. [y-64] can be computed in an [int] (because the result belongs to the interval [[-96;-33]]). 4. [(x+1)/(y-64)] must be a GMP operation because the numerator is a GMP (see 1.). Consequently [y-64] must be coerced into a GMP too. However, the result belongs to the interval [[-3;3]] and thus can be safely coerced to an [int]. 5. Consequently the addition of the toplevel term [1+(x+1)/(y-64)] can safely be computed in [int]: its result belongs to [[-2;4]]. *)  Julien Signoles committed Jun 09, 2016 46   Julien Signoles committed Jun 09, 2016 47 48 49 open Cil_types (******************************************************************************)  Julien Signoles committed Jun 09, 2016 50 (** {2 Datatypes} *)  Julien Signoles committed Jun 09, 2016 51 52 (******************************************************************************)  Fonenantsoa Maurica committed Aug 02, 2019 53 54 55 (** Possible types infered by the system. *) type number_ty = private  Julien Signoles committed Aug 27, 2019 56 57  | C_integer of ikind | C_float of fkind  Fonenantsoa Maurica committed Aug 02, 2019 58  | Gmpz  Julien Signoles committed Aug 27, 2019 59  | Rational  Julien Signoles committed Aug 02, 2019 60  | Real  Fonenantsoa Maurica committed Aug 02, 2019 61  | Nan  Julien Signoles committed Jun 09, 2016 62   Fonenantsoa Maurica committed Aug 02, 2019 63 module Datatype: Datatype.S_with_collections with type t = number_ty  Julien Signoles committed Mar 01, 2017 64   Julien Signoles committed Jun 09, 2016 65 (** {3 Smart constructors} *)  Julien Signoles committed Jun 09, 2016 66   Fonenantsoa Maurica committed Aug 02, 2019 67 68 val c_int: number_ty val ikind: ikind -> number_ty  Julien Signoles committed Aug 27, 2019 69 val fkind: fkind -> number_ty  Fonenantsoa Maurica committed Aug 02, 2019 70 val gmpz: number_ty  Julien Signoles committed Aug 27, 2019 71 val rational: number_ty  Fonenantsoa Maurica committed Aug 02, 2019 72 val nan: number_ty  73   Fonenantsoa Maurica committed Aug 02, 2019 74 (** {3 Useful operations over {!number_ty}} *)  Julien Signoles committed Jun 09, 2016 75   Fonenantsoa Maurica committed Aug 02, 2019 76 77 78 exception Not_a_number val typ_of_number_ty: number_ty -> typ (** @return the C type corresponding to an {!number_ty}. That is [Gmp.z_t ()]  Julien Signoles committed Aug 02, 2019 79  for [Gmpz], [Real.t ()] for [Real] and [TInt(ik, [[]])] for [Ctype ik].  Fonenantsoa Maurica committed Aug 02, 2019 80  @raise Not_a_number in case of [Nan]. *)  Julien Signoles committed Jun 09, 2016 81   Fonenantsoa Maurica committed Aug 02, 2019 82 83 val number_ty_of_typ: typ -> number_ty (** Reverse of [typ_of_number_ty] *)  Fonenantsoa Maurica committed Sep 18, 2018 84   Fonenantsoa Maurica committed Aug 02, 2019 85 86 val join: number_ty -> number_ty -> number_ty (** {!number_ty} is a join-semi-lattice if you do not consider [Other]. If  Julien Signoles committed Jun 09, 2016 87 88  there is no [Other] in argument, this function computes the join of this semi-lattice. If one of the argument is {!Other}, the function assumes that  Julien Signoles committed Aug 23, 2019 89  the other argument is also {!Other}. In this case, the result is [Other]. *)  Julien Signoles committed Jun 09, 2016 90 91 92 93 94  (******************************************************************************) (** {2 Typing} *) (******************************************************************************)  Fonenantsoa Maurica committed Aug 02, 2019 95 val type_term: use_gmp_opt:bool -> ?ctx:number_ty -> term -> unit  Julien Signoles committed Jun 09, 2016 96 (** Compute the type of each subterm of the given term in the given context. If  Julien Signoles committed Apr 29, 2019 97 98  [use_gmp_opt] is false, then the conversion to the given context is done even if -e-acsl-gmp-only is set. *)  Julien Signoles committed Jun 09, 2016 99   Boris Yakobowski committed Aug 31, 2016 100 val type_named_predicate: ?must_clear:bool -> predicate -> unit  Julien Signoles committed Jun 09, 2016 101 102 103 104 105 106 107 108 109 110 111 (** Compute the type of each term of the given predicate. Set {!must_clear} to false in order to not reset the environment. *) val clear: unit -> unit (** Remove all the previously computed types. *) (** {3 Getters} Below, the functions assume that either {!type_term} or {!type_named_predicate} has been previously computed for the given term or predicate. *)  Julien Signoles committed Jun 09, 2016 112   Fonenantsoa Maurica committed Aug 02, 2019 113 114 val get_number_ty: term -> number_ty (** @return the infered type for the given term. *)  Julien Signoles committed Jun 09, 2016 115   Fonenantsoa Maurica committed Aug 02, 2019 116 117 val get_integer_op: term -> number_ty (** @return the infered type for the top operation of the given term.  Julien Signoles committed Jun 09, 2016 118 119 120  It is meaningless to call this function over a non-arithmetical/logical operator. *)  Fonenantsoa Maurica committed Aug 02, 2019 121 122 val get_integer_op_of_predicate: predicate -> number_ty (** @return the infered type for the top operation of the given predicate. *)  Julien Signoles committed Jun 09, 2016 123 124  val get_typ: term -> typ  Julien Signoles committed Jun 09, 2016 125 (** Get the type which the given term must be generated to. *)  Julien Signoles committed Jun 09, 2016 126   Julien Signoles committed Jun 09, 2016 127 val get_op: term -> typ  Julien Signoles committed Jun 09, 2016 128 129 (** Get the type which the operation on top of the given term must be generated to. *)  Julien Signoles committed Jun 09, 2016 130   Julien Signoles committed Jun 09, 2016 131 val get_cast: term -> typ option  Julien Signoles committed Jun 09, 2016 132 (** Get the type which the given term must be converted to (if any). *)  Julien Signoles committed Jun 09, 2016 133   Boris Yakobowski committed Aug 31, 2016 134 val get_cast_of_predicate: predicate -> typ option  Julien Signoles committed Jun 09, 2016 135 (** Like {!get_cast}, but for predicates. *)  Julien Signoles committed Jun 09, 2016 136   Fonenantsoa Maurica committed Aug 02, 2019 137 val unsafe_set: term -> ?ctx:number_ty -> number_ty -> unit  Julien Signoles committed Mar 01, 2017 138 139 140 (** Register that the given term has the given type in the given context (if any). No verification is done. *)  Fonenantsoa Maurica committed Oct 03, 2018 141 (*****************************************************************************)  Fonenantsoa Maurica committed Apr 29, 2019 142 (** {2 Typing/types-related utils} *)  Fonenantsoa Maurica committed Oct 03, 2018 143 144 (*****************************************************************************)  Julien Signoles committed Aug 27, 2019 145 val ty_of_interv: ?ctx:number_ty -> Interval.t -> number_ty  Fonenantsoa Maurica committed Oct 03, 2018 146 147 (* Compute the smallest type (bigger than [int]) which can contain the whole interval. It is the \theta operator of the JFLA's paper. *)  Fonenantsoa Maurica committed Oct 03, 2018 148   Fonenantsoa Maurica committed Apr 29, 2019 149 150 151 val typ_of_lty: logic_type -> typ (** @return the C type that correponds to the given logic type. *)  Julien Signoles committed Jun 09, 2016 152 153 154 155 156 (******************************************************************************) (** {2 Internal stuff} *) (******************************************************************************) val compute_quantif_guards_ref  Julien Signoles committed Dec 16, 2019 157 158  : (predicate -> logic_var list -> predicate -> (term * relation * logic_var * relation * term) list) ref  Julien Signoles committed Jun 09, 2016 159 160 161 162 (** Forward reference. *) (* Local Variables:  Julien Signoles committed Jan 09, 2020 163 compile-command: "make -C ../../../../.."  Julien Signoles committed Jun 09, 2016 164 165 End: *)