Commit d396efac authored by Julien Signoles's avatar Julien Signoles
Browse files

[typing] full support of real numbers

parent a3084f08
......@@ -95,10 +95,7 @@ let rec sizes_and_shifts_from_quantifs ~loc kf lscope sizes_and_shifts =
| _ ->
Options.fatal "Unexpected comparison operator"
in
let i =
try Interval.infer t_size
with Interval.Not_a_number | Interval.Is_a_real -> assert false
in
let iv = Interval.(extract_ival (infer t_size)) in
(* The EXACT amount of memory that is needed can be known at runtime. This
is because the tightest bounds for the variables can be known at runtime.
Example: In the following predicate
......@@ -116,7 +113,7 @@ let rec sizes_and_shifts_from_quantifs ~loc kf lscope sizes_and_shifts =
beneficial. In particular, though we may allocate more memory than
needed, the number of reads/writes into it is the same in both cases.
Conclusion: over-approximate [t_size] *)
let t_size = match Ival.min_and_max i with
let t_size = match Ival.min_and_max iv with
| _, Some max ->
Logic_const.tint ~loc max
| _, None ->
......@@ -233,9 +230,9 @@ let to_exp ~loc kf env pot label =
Cil.intType
| Misc.PoT_term t ->
begin match Typing.get_number_ty t with
| Typing.C_type _ | Typing.Nan ->
| Typing.(C_integer _ | C_float _ | Nan) ->
Typing.get_typ t
| Typing.Real ->
| Typing.(Rational | Real) ->
Error.not_yet "\\at on purely logic variables and over real type"
| Typing.Gmpz ->
Error.not_yet "\\at on purely logic variables and over gmp type"
......@@ -259,20 +256,19 @@ let to_exp ~loc kf env pot label =
in
Typing.type_term ~use_gmp_opt:false t_size;
let malloc_stmt = match Typing.get_number_ty t_size with
| Typing.C_type IInt ->
| Typing.C_integer IInt ->
let e_size, _ = term_to_exp kf env t_size in
let e_size = Cil.constFold false e_size in
let malloc_stmt =
Misc.mk_call ~loc ~result:(Cil.var vi) "malloc" [e_size]
in
malloc_stmt
| Typing.C_type _ | Typing.Gmpz ->
| Typing.(C_integer _ | C_float _ | Gmpz) ->
Error.not_yet
"\\at on purely logic variables that needs to allocate \
too much memory (bigger than int_max bytes)"
| Typing.Real | Typing.Nan ->
Options.fatal
"quantification over non-integer type is not part of E-ACSL"
too much memory (bigger than int_max bytes)"
| Typing.(Rational | Real | Nan) ->
Error.not_yet "quantification over non-integer type"
in
let free_stmt = Misc.mk_call ~loc "free" [e] in
(* The list of stmts returned by the current closure are inserted
......@@ -306,7 +302,7 @@ let to_exp ~loc kf env pot label =
[ Cil.mkStmt ~valid_sid:true (Block block) ], env
| Misc.PoT_term t ->
begin match Typing.get_number_ty t with
| Typing.C_type _ | Typing.Nan ->
| Typing.(C_integer _ | C_float _ | Nan) ->
let env = Env.push env in
let lval, env = lval_at_index ~loc kf env (e_at, vi_at, t_index) in
let e, env = term_to_exp kf env t in
......@@ -320,7 +316,7 @@ let to_exp ~loc kf env pot label =
(* We CANNOT return [block.bstmts] because it does NOT contain
variable declarations. *)
[ Cil.mkStmt ~valid_sid:true (Block block) ], env
| Typing.Real ->
| Typing.(Rational | Real) ->
Error.not_yet "\\at on purely logic variables and over real type"
| Typing.Gmpz ->
Error.not_yet "\\at on purely logic variables and over gmp type"
......
......@@ -30,20 +30,151 @@ open Cil_types
(* Basic datatypes and operations *)
(* ********************************************************************* *)
exception Is_a_real
exception Not_a_number
type ival =
| Ival of Ival.t
| Float of fkind * float option (* a float constant, if any *)
| Rational
| Real
| Nan
module D =
Datatype.Make_with_collections
(struct
type t = ival
let name = "E_ACSL.Interval.t"
let reprs = [ Float (FFloat, Some 0.); Rational; Real; Nan ]
include Datatype.Undefined
let compare i1 i2 =
if i1 == i2 then 0
else
match i1, i2 with
| Ival i1, Ival i2 ->
Ival.compare i1 i2
| Float (k1, f1), Float (k2, f2) ->
(* faster to compare a kind than a float *)
let n = Stdlib.compare k1 k2 in
if n = 0 then Stdlib.compare f1 f2 else n
| Ival _, (Float _ | Rational | Real | Nan)
| Float _, (Rational | Real | Nan)
| Rational, (Real | Nan)
| Real, Nan ->
-1
| Nan, (Ival _ | Float _ | Rational | Real)
| Real, (Ival _ | Float _ | Rational)
| Rational, (Ival _ | Float _)
| Float _, Ival _ ->
1
| Rational, Rational | Real, Real | Nan, Nan ->
assert false
let equal = Datatype.from_compare
let hash = function
| Ival i -> 7 * Ival.hash i
| Float(k, f) -> 17 * Hashtbl.hash f + 97 * Hashtbl.hash k
| Rational -> 787
| Real -> 1011
| Nan -> 1277
let pretty fmt = function
| Ival i -> Ival.pretty fmt i
| Float(_, Some f) -> Format.pp_print_float fmt f
| Float(FFloat, None) -> Format.pp_print_string fmt "float"
| Float(FDouble, None) -> Format.pp_print_string fmt "double"
| Float(FLongDouble, None) -> Format.pp_print_string fmt "long double"
| Rational -> Format.pp_print_string fmt "Rational"
| Real -> Format.pp_print_string fmt "Real"
| Nan -> Format.pp_print_string fmt "NaN"
end)
let is_included i1 i2 = match i1, i2 with
| Ival i1, Ival i2 -> Ival.is_included i1 i2
| Float(k1, f1), Float(k2, f2) ->
Stdlib.compare k1 k2 <= 0
&& (match f1, f2 with
| None, None | Some _, None -> true
| None, Some _ -> false
| Some f1, Some f2 -> f1 = f2)
| (Ival _ | Float _ | Rational), (Rational | Real)
| Real, Real
| Nan, Nan ->
true
(* floats and integer are not comparable: *)
| Ival _, Float _ | Float _, Ival _
(* nan is comparable to noone, but itself: *)
| (Ival _ | Float _ | Rational | Real), Nan
| Nan, (Ival _ | Float _ | Rational | Real)
(* cases for reals and rationals: *)
| Real, (Ival _ | Float _ | Rational)
| Rational, (Ival _ | Float _) ->
false
let lift_unop f = function
| Ival iv -> Ival (f iv)
| Float _ ->
(* any unary operator over a float generates a rational
TODO: actually, certainly possible to generate a float *)
Rational
| Rational | Real | Nan as i -> i
let lift_binop ~safe_float f i1 i2 = match i1, i2 with
| Ival i1, Ival i2 ->
Ival (f i1 i2)
| Float(k1, _), Float(k2, _) when safe_float ->
let k = if Stdlib.compare k1 k2 >= 0 then k1 else k2 in
Float(k, None (* lost value, if any before *))
| (Ival _ | Float _ | Rational), (Float _ | Rational)
| (Float _ | Rational), Ival _ ->
(* any binary operator over a float or a rational generates a rational *)
Rational
| (Ival _ | Float _ | Rational | Real), Real
| Real, (Ival _ | Float _ | Rational) ->
Real
| (Ival _ | Float _ | Rational | Real | Nan), Nan
| Nan, (Ival _ | Float _ | Rational | Real) ->
Nan
let join = lift_binop ~safe_float:true Ival.join
(* TODO: soundness of any downcast is not checked *)
let cast ~src ~dst = match src, dst with
| Ival i1, Ival i2 ->
Ival (Ival.meet i1 i2)
| _, Float(_, Some _) ->
assert false
| Rational, Real
| Float _, (Rational | Real) ->
src
| _, _ ->
(* No need to optimize the other cases: if someone writes a cast
(in particular, from integer to float/real or conversely), it is
certainly on purpose . *)
dst
(* constructors *)
(* ********************************************************************* *)
(* constructors and destructors *)
(* ********************************************************************* *)
let singleton_of_int n = Ival.inject_singleton (Integer.of_int n)
let extract_ival = function
| Ival iv -> iv
| Float _ | Rational | Real | Nan -> assert false
let bottom = Ival Ival.bottom
let top_ival = Ival (Ival.inject_range None None)
let singleton n = Ival (Ival.inject_singleton n)
let singleton_of_int n = singleton (Integer.of_int n)
let ival min max = Ival (Ival.inject_range (Some min) (Some max))
let interv_of_unknown_block =
(* since we have no idea of the size of this block, we take the largest
possible one which is unfortunately quite large *)
lazy
(Ival.inject_range
(Some Integer.zero)
(Some (Bit_utils.max_byte_address ())))
lazy (ival Integer.zero (Bit_utils.max_byte_address ()))
(* ********************************************************************* *)
(* main algorithm *)
(* ********************************************************************* *)
(* The boolean indicates whether we have real numbers *)
let rec interv_of_typ ty = match Cil.unrollType ty with
......@@ -53,29 +184,31 @@ let rec interv_of_typ ty = match Cil.unrollType ty with
if Cil.isSigned k then Cil.min_signed_number n, Cil.max_signed_number n
else Integer.zero, Cil.max_unsigned_number n
in
Ival.inject_range (Some l) (Some u)
ival l u
| TEnum(enuminfo, _) ->
interv_of_typ (TInt (enuminfo.ekind, []))
| TFloat _ ->
raise Is_a_real
interv_of_typ (TInt(enuminfo.ekind, []))
| _ when Gmp.Z.is_t ty ->
top_ival
| TFloat (k, _) ->
Float(k, None)
| _ when Real.is_t ty ->
raise Is_a_real
Rational (* only rationals are implemented *)
| TVoid _ | TPtr _ | TArray _ | TFun _ | TComp _ | TBuiltin_va_list _ ->
raise Not_a_number
Nan
| TNamed _ ->
assert false
let interv_of_logic_typ = function
| Ctype ty -> interv_of_typ ty
| Linteger -> Ival.inject_range None None
| Lreal -> raise Is_a_real
| Linteger -> top_ival
| Lreal -> Real
| Ltype _ -> Error.not_yet "user-defined logic type"
| Lvar _ -> Error.not_yet "type variable"
| Larrow _ -> Error.not_yet "functional type"
| Larrow _ -> Nan
let ikind_of_interv i =
if Ival.is_bottom i then IInt
else match Ival.min_and_max i with
let ikind_of_ival iv =
if Ival.is_bottom iv then IInt
else match Ival.min_and_max iv with
| Some l, Some u ->
let is_pos = Integer.ge l Integer.zero in
let lkind = Cil.intKindForValue l is_pos in
......@@ -85,31 +218,31 @@ let ikind_of_interv i =
(* convert the kind to [IInt] whenever smaller. *)
if Cil.intTypeIncluded kind IInt then IInt else kind
| None, None -> raise Cil.Not_representable (* GMP *)
(* TODO: do not raise an exception, but returns a value instead *)
| None, Some _ | Some _, None ->
Kernel.fatal ~current:true "unexpected ival: %a" Ival.pretty i
Kernel.fatal ~current:true "unexpected ival: %a" Ival.pretty iv
(* function call profiles (intervals for their formal parameters) *)
module Profile = struct
include Datatype.List_with_collections
(Ival)
(D)
(struct
let module_name = "E_ACSL.Interval.Logic_function_env.Profile"
end)
let is_included p1 p2 = List.for_all2 Ival.is_included p1 p2
let _join p1 p2 = List.map2 Ival.join p1 p2 (* TODO: to be removed *)
let is_included p1 p2 = List.for_all2 is_included p1 p2
end
(* Imperative environments *)
module rec Env: sig
val clear: unit -> unit
val add: Cil_types.logic_var -> Ival.t -> unit
val find: Cil_types.logic_var -> Ival.t
val add: Cil_types.logic_var -> ival -> unit
val find: Cil_types.logic_var -> ival
val remove: Cil_types.logic_var -> unit
val replace: Cil_types.logic_var -> Ival.t -> unit
val replace: Cil_types.logic_var -> ival -> unit
end = struct
open Cil_datatype
let tbl: Ival.t Logic_var.Hashtbl.t = Logic_var.Hashtbl.create 7
let tbl: ival Logic_var.Hashtbl.t = Logic_var.Hashtbl.create 7
(* TODO: when adding, also join with the old value (if any). Would certainly
be the correct way to handle a \let in a recursive logic functions (if the
......@@ -127,7 +260,7 @@ end
(* Environment for handling logic functions *)
and Logic_function_env: sig
val widen: infer:(term -> Ival.t) -> term -> Ival.t -> bool * Ival.t
val widen: infer:(term -> ival) -> term -> ival -> bool * ival
val clear: unit -> unit
end = struct
......@@ -161,13 +294,15 @@ end = struct
Terms.clear terms;
LF.Hashtbl.clear named_profiles
let interv_of_typ_containing_interv i =
try
let kind = ikind_of_interv i in
interv_of_typ (TInt(kind, []))
with Cil.Not_representable ->
(* infinity *)
Ival.inject_range None None
let interv_of_typ_containing_interv = function
| Float _ | Rational | Real | Nan as x ->
x
| Ival i ->
try
let kind = ikind_of_ival i in
interv_of_typ (TInt(kind, []))
with Cil.Not_representable ->
top_ival
let rec map3 f l1 l2 l3 = match l1, l2, l3 with
| [], [], [] -> []
......@@ -177,24 +312,20 @@ end = struct
let extract_profile ~infer old_profile t = match t.term_node with
| Tapp(li, _, args) ->
let old_profile = match old_profile with
| None -> List.map (fun _ -> Ival.bottom) li.l_profile
| None -> List.map (fun _ -> bottom) li.l_profile
| Some p -> p
in
li.l_var_info.lv_name,
map3
(fun param old_i arg ->
try
let i = infer arg in
(* over-approximation of the interval to reach the fixpoint
faster, and to generate fewer specialized functions *)
let larger_i = interv_of_typ_containing_interv i in
(* merge the old profile and the new one *)
let new_i = Ival.join larger_i old_i in
Env.add param new_i;
new_i
with Not_a_number ->
(* no need to add [param] to the environment *)
Ival.bottom)
let i = infer arg in
(* over-approximation of the interval to reach the fixpoint
faster, and to generate fewer specialized functions *)
let larger_i = interv_of_typ_containing_interv i in
(* merge the old profile and the new one *)
let new_i = join larger_i old_i in
Env.add param new_i;
new_i)
li.l_profile
old_profile
args
......@@ -205,9 +336,9 @@ end = struct
let (_, p as named_p) = extract_profile ~infer old_profile t in
try
let old_i = LF.Hashtbl.find named_profiles named_p in
if Ival.is_included i old_i then true, p, old_i
if is_included i old_i then true, p, old_i
else begin
let j = Ival.join i old_i in
let j = join i old_i in
LF.Hashtbl.replace named_profiles named_p j;
false, p, j
end
......@@ -244,17 +375,17 @@ let infer_alignof ty = singleton_of_int (Cil.bytesAlignOf ty)
let rec infer t =
let get_cty t = match t.term_type with Ctype ty -> ty | _ -> assert false in
match t.term_node with
| TConst (Integer (n, _)) -> Ival.inject_singleton n
| TConst (Integer (n, _)) -> singleton n
| TConst (LChr c) ->
let n = Cil.charConstToInt c in
Ival.inject_singleton n
singleton n
| TConst (LEnum enumitem) ->
let rec find_idx n = function
| [] -> assert false
| ei :: l -> if ei == enumitem then n else find_idx (n + 1) l
in
let n = Integer.of_int (find_idx 0 enumitem.eihost.eitems) in
Ival.inject_singleton n
singleton n
| TLval lv -> infer_term_lval lv
| TSizeOf ty -> infer_sizeof ty
| TSizeOfE t -> infer_sizeof (get_cty t)
......@@ -264,66 +395,53 @@ let rec infer t =
| TUnOp (Neg, t) ->
let i = infer t in
Ival.neg_int i
lift_unop Ival.neg_int i
| TUnOp (BNot, t) ->
let i = infer t in
Ival.bitwise_signed_not i
lift_unop Ival.bitwise_signed_not i
| TUnOp (LNot, _)
| TBinOp ((Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr), _, _) ->
Ival.zero_or_one
Ival Ival.zero_or_one
| TBinOp (PlusA, t1, t2) ->
let i1 = infer t1 in
let i2 = infer t2 in
Ival.add_int i1 i2
lift_binop ~safe_float:false Ival.add_int i1 i2
| TBinOp (MinusA, t1, t2) ->
let i1 = infer t1 in
let i2 = infer t2 in
Ival.sub_int i1 i2
lift_binop ~safe_float:false Ival.sub_int i1 i2
| TBinOp (Mult, t1, t2) ->
let i1 = infer t1 in
let i2 = infer t2 in
Ival.mul i1 i2
lift_binop ~safe_float:false Ival.mul i1 i2
| TBinOp (Div, t1, t2) ->
let i1 = infer t1 in
let i2 = infer t2 in
Ival.div i1 i2
lift_binop ~safe_float:false Ival.div i1 i2
| TBinOp (Mod, t1, t2) ->
let i1 = infer t1 in
let i2 = infer t2 in
Ival.c_rem i1 i2
lift_binop ~safe_float:false Ival.c_rem i1 i2
| TBinOp (Shiftlt , _, _) -> Error.not_yet "right shift"
| TBinOp (Shiftrt , _, _) -> Error.not_yet "left shift"
| TBinOp (BAnd, _, _) -> Error.not_yet "bitwise and"
| TBinOp (BXor, t1, t2) ->
let i1 = infer t1 in
let i2 = infer t2 in
Ival.bitwise_xor i1 i2
lift_binop ~safe_float:false Ival.bitwise_xor i1 i2
| TBinOp (BOr, t1, t2) ->
let i1 = infer t1 in
let i2 = infer t2 in
Ival.bitwise_or i1 i2
lift_binop ~safe_float:false Ival.bitwise_or i1 i2
| TCastE (ty, t) ->
(try
let it = infer t in
let ity = interv_of_typ ty in
Ival.meet it ity
with Not_a_number ->
if Cil.isIntegralType ty then begin
(* heterogeneous cast from a non-integral term to an integral type:
consider that one eventually gets an integral type even if it is
not sure. *)
Options.warning
~once:true "possibly unsafe cast from term '%a' to type '%a'."
Printer.pp_term t
Printer.pp_typ ty;
interv_of_typ ty
end else
raise Not_a_number)
let src = infer t in
let dst = interv_of_typ ty in
cast ~src ~dst
| Tif (_, t2, t3) ->
let i2 = infer t2 in
let i3 = infer t3 in
Ival.join i2 i3
join i2 i3
| Tat (t, _) ->
infer t
| TBinOp (MinusPP, t, _) ->
......@@ -332,10 +450,7 @@ let rec infer t =
(* the second argument must be in the same block than [t]. Consequently
the result of the difference belongs to [0; \block_length(t)] *)
let nb_bytes = if n mod 8 = 0 then n / 8 else n / 8 + 1 in
let i =
Ival.inject_range (Some Integer.zero) (Some (Integer.of_int nb_bytes))
in
i
ival Integer.zero (Integer.of_int nb_bytes)
| TArray _ | TPtr _ ->
Lazy.force interv_of_unknown_block
| _ -> assert false)
......@@ -353,7 +468,7 @@ let rec infer t =
| Tapp (li, _, _args) ->
(match li.l_body with
| LBpred _ ->
Ival.zero_or_one
Ival Ival.zero_or_one
| LBterm t' ->
let rec fixpoint i =
let is_included, new_i =
......@@ -367,11 +482,7 @@ let rec infer t =
List.iter (fun lv -> Env.remove lv) li.l_profile;
fixpoint i
in
let i = fixpoint Ival.bottom in
(* call [interv_of_logic_typ] in order to raise Is_a_real or Not_a_number
when the function does not return an integer *)
Extlib.may (fun lty -> ignore (interv_of_logic_typ lty)) li.l_type;
i
fixpoint bottom
| LBnone
| LBreads _ ->
(match li.l_type with
......@@ -386,7 +497,7 @@ let rec infer t =
| Trange(Some n1, Some n2) ->
let i1 = infer n1 in
let i2 = infer n2 in
Ival.join i1 i2
join i1 i2
| Trange(None, _) | Trange(_, None) ->
Options.abort "unbounded ranges are not part of E-ACSl"
......@@ -398,8 +509,9 @@ let rec infer t =
let i2 = infer t in
Env.remove li_v;
i2
| TConst (LReal _) ->
raise Is_a_real
| TConst (LReal lr) ->
if lr.r_lower = lr.r_upper then Float(FDouble, Some lr.r_nearest)
else Rational
| TConst (LStr _ | LWStr _)
| TBinOp (PlusPI,_,_)
| TBinOp (IndexPI,_,_)
......@@ -413,7 +525,7 @@ let rec infer t =
| Ttypeof _
| Ttype _
| Tempty_set ->
raise Not_a_number
Nan
and infer_term_lval (host, offset as tlv) =
match offset with
......@@ -425,11 +537,11 @@ and infer_term_lval (host, offset as tlv) =
and infer_term_host thost =
match thost with
| TVar v ->
(try Env.find v
with Not_found ->
(try Env.find v with Not_found ->
match v.lv_type with
| Linteger -> Ival.inject_range None None
| Ctype (TFloat _) | Lreal -> raise Is_a_real
| Linteger -> top_ival
| Ctype (TFloat(fk, _)) -> Float(fk, None)
| Lreal -> Real
| Ctype _ -> interv_of_typ (Logic_utils.logicCType v.lv_type)
| Ltype _ | Lvar _ | Larrow _ -> Options.fatal "unexpected logic type")
| TResult ty ->
......@@ -444,6 +556,8 @@ and infer_term_host thost =
Printer.pp_typ ty
Printer.pp_term t
include D
(*
Local Variables:
compile-command: "make"
......
......@@ -51,15 +51,30 @@
(** {3 Useful operations on intervals} *)
(* ************************************************************************** *)
exception Is_a_real
exception Not_a_number
type ival =
| Ival of Ival.t
| Float of Cil_types.fkind * float option
| Rational
| Real
| Nan
val ikind_of_interv: Ival.t -> Cil_types.ikind
include Datatype.S_with_collections with type t = ival
val is_included: t -> t -> bool