From 238c1e4a58aa06f9fe55594292f1b50d2f614847 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 30 Dec 2015 16:34:58 +0100
Subject: [PATCH] new type system (still unused, but compiled)
---
src/plugins/e-acsl/Makefile.in | 1 +
src/plugins/e-acsl/interval.ml | 2 +
src/plugins/e-acsl/interval.mli | 1 +
src/plugins/e-acsl/new_typing.ml | 379 ++++++++++++++++++++++++++++++
src/plugins/e-acsl/new_typing.mli | 68 ++++++
5 files changed, 451 insertions(+)
create mode 100644 src/plugins/e-acsl/new_typing.ml
create mode 100644 src/plugins/e-acsl/new_typing.mli
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 2cdb78a96a9..48159fd39ff 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -62,6 +62,7 @@ PLUGIN_CMO:= local_config \
env \
interval \
typing \
+ new_typing \
quantif \
translate \
loops \
diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml
index 4b7384905d8..c5db5e55354 100644
--- a/src/plugins/e-acsl/interval.ml
+++ b/src/plugins/e-acsl/interval.ml
@@ -67,6 +67,8 @@ let interv_of_unknown_block =
(let u = Integer.div (Bit_utils.max_bit_address ()) Integer.eight in
make Integer.zero u)
+let add i n = { lower = Integer.add i.lower n; upper = Integer.add i.upper n }
+
(* intervals as a lattice *)
let meet i1 i2 =
diff --git a/src/plugins/e-acsl/interval.mli b/src/plugins/e-acsl/interval.mli
index 95176f8958b..f6a906c3c2b 100644
--- a/src/plugins/e-acsl/interval.mli
+++ b/src/plugins/e-acsl/interval.mli
@@ -36,6 +36,7 @@ end
val interv_of_typ: Cil_types.typ -> t
+val add: t -> Integer.t -> t
val join: t -> t -> t
val meet: t -> t -> t
diff --git a/src/plugins/e-acsl/new_typing.ml b/src/plugins/e-acsl/new_typing.ml
new file mode 100644
index 00000000000..f30a8c15d30
--- /dev/null
+++ b/src/plugins/e-acsl/new_typing.ml
@@ -0,0 +1,379 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-2015 *)
+(* 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 license/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+(* Implement Figure 4 of J. Signoles' JFLA'15 paper "Rester statique pour
+ devenir plus rapide, plus précis et plus mince". *)
+
+let dkey = Options.dkey_typing
+
+let compute_quantif_guards_ref
+ : (predicate named -> logic_var list -> predicate named ->
+ (term * relation * logic_var * relation * term) list) ref
+ = Extlib.mk_fun "compute_quantif_guards_ref"
+
+(******************************************************************************)
+(** Datatypes and memoization *)
+(******************************************************************************)
+
+type integer_ty =
+ | Gmp
+ | C_type of ikind
+
+let c_int = C_type IInt
+
+include Datatype.Make
+(struct
+ type t = integer_ty
+ let name = "E_ACSL.Typing.t"
+ let reprs = [ Gmp; c_int ]
+ include Datatype.Undefined
+
+ let compare ty1 ty2 = match ty1, ty2 with
+ | C_type i1, C_type i2 ->
+ if i1 = i2 then 0
+ else if Cil.intTypeIncluded i1 i2 then -1 else 1
+ | C_type _, Gmp -> -1
+ | Gmp, C_type _ -> 1
+ | Gmp, Gmp -> 0
+
+ let equal = Datatype.from_compare
+
+ let pretty fmt = function
+ | Gmp -> Format.fprintf fmt "gmp"
+ | C_type k -> Printer.pp_ikind fmt k
+ end)
+
+type computed_info =
+ { ty: t; (* type required for the term *)
+ cast: t option; (* if not [None], type of the context which the term
+ must be casted to. If [None], no cast needed. *)
+ }
+
+module Memo: sig
+ val memo: (term -> computed_info) -> term -> computed_info
+ val get: term -> computed_info
+ val clear: unit -> unit
+end = struct
+
+ module H = Hashtbl.Make(struct
+ type t = term
+ let equal (t1:term) t2 = t1 == t2
+ let hash = Cil_datatype.Term.hash
+ end)
+
+ let tbl = H.create 97
+
+ let get t =
+ try H.find tbl t
+ with Not_found ->
+ Options.fatal "type of term '%a' was never computed." Printer.pp_term t
+
+ let memo f t =
+ try H.find tbl t
+ with Not_found ->
+ let x = f t in
+ H.add tbl t x;
+ x
+
+ let clear () = H.clear tbl
+
+end
+
+(******************************************************************************)
+(** {2 Coercion rules} *)
+(******************************************************************************)
+
+(* Compute the smallest type (bigger than [int]) which can contain the whole
+ interval. It is the \theta operator of the JFLA's paper. *)
+let ty_of_interv i =
+ let open Interval in
+ let is_pos = Integer.ge i.lower Integer.zero in
+ try
+ let lkind = Cil.intKindForValue i.lower is_pos in
+ let ukind = Cil.intKindForValue i.upper is_pos in
+ let kind = if Cil.intTypeIncluded lkind ukind then ukind else lkind in
+ (* int whenever possible to prevent superfluous casts in the generated
+ code *)
+ if Cil.intTypeIncluded kind IInt then c_int else C_type kind
+ with Cil.Not_representable ->
+ Gmp
+
+let coerce ~ctx ty =
+ if compare ty ctx = 1 then begin
+ (* type larger than the expected context,
+ so we must introduce an explicit cast *)
+ { ty = ty; cast = Some ctx }
+ end else
+ (* only add an explicit cast if the context is [Gmp] and [ty] is not *)
+ if ctx = Gmp && ty <> Gmp then { ty = ty; cast = Some Gmp }
+ else { ty = ty; cast = None }
+
+(******************************************************************************)
+(** {2 Typing} *)
+(******************************************************************************)
+
+exception Not_an_integer
+
+let rec type_term env ~ctx t =
+ let infer t =
+ Cil.CurrentLoc.set t.term_loc;
+ match t.term_node with
+ | TConst (Integer _ | LChr _)
+ | TLval _
+ | TSizeOf _
+ | TSizeOfE _
+ | TSizeOfStr _
+ | TAlignOf _
+ | TAlignOfE _
+ | TBinOp (MinusPP, _, _)
+ | Tblock_length(_, _)
+ | Tnull ->
+ let i = Interval.infer env t in
+ ty_of_interv i
+
+ | TUnOp (_, t') ->
+ let i = Interval.infer env t in
+ let i' = Interval.infer env t' in
+ let ctx = ty_of_interv (Interval.join i i') in
+ ignore (type_term env ~ctx t');
+ ctx
+
+ | TBinOp((PlusA | MinusA | Mult | Div | Mod | Shiftlt | Shiftrt), t1, t2) ->
+ let i = Interval.infer env t in
+ let i1 = Interval.infer env t1 in
+ let i2 = Interval.infer env t2 in
+ let ctx = ty_of_interv (Interval.join i (Interval.join i1 i2)) in
+ ignore (type_term env ~ctx t1);
+ ignore (type_term env ~ctx t2);
+ ctx
+ | TBinOp ((Lt | Gt | Le | Ge | Eq | Ne), t1, t2) ->
+ assert (compare ctx c_int >= 1);
+ let i1 = Interval.infer env t1 in
+ let i2 = Interval.infer env t2 in
+ let ctx = ty_of_interv (Interval.join i1 i2) in
+ ignore (type_term env ~ctx t1);
+ ignore (type_term env ~ctx t2);
+ ctx
+ | TBinOp ((LAnd | LOr), t1, t2) ->
+ assert (compare ctx c_int >= 1);
+ let i1 = Interval.infer env t1 in
+ let i2 = Interval.infer env t2 in
+ (* both operands fit in an int. *)
+ ignore (type_term env ~ctx:c_int t1);
+ ignore (type_term env ~ctx:c_int t2);
+ ty_of_interv (Interval.join i1 i2)
+
+ | TBinOp (BAnd, _, _) -> Error.not_yet "bitwise and"
+ | TBinOp (BXor, _, _) -> Error.not_yet "bitwise xor"
+ | TBinOp (BOr, _, _) -> Error.not_yet "bitwise or"
+
+ | TCastE _
+ | TCoerce _ ->
+ let i = Interval.infer env t in
+ (* nothing to do more: [i] is already more precise than what we could
+ infer from the arguments of the cast. Also, do not type the internal
+ term: possibly it is not even an integer *)
+ ty_of_interv i
+ | Tif (t1, t2, t3) ->
+ ignore (type_term env ~ctx:c_int t1);
+ let i = Interval.infer env t in
+ let i2 = Interval.infer env t2 in
+ let i3 = Interval.infer env t3 in
+ let ctx = ty_of_interv (Interval.join i (Interval.join i2 i3)) in
+ ignore (type_term env ~ctx t2);
+ ignore (type_term env ~ctx t3);
+ ctx
+ | Tat (t, _) -> (type_term env ~ctx t).ty
+ | TLogic_coerce (_, t) -> (type_term env ~ctx t).ty
+ | TCoerceE (t1, t2) ->
+ let i = Interval.infer env t in
+ let i1 = Interval.infer env t1 in
+ let i2 = Interval.infer env t2 in
+ let ty = ty_of_interv (Interval.join i (Interval.join i1 i2)) in
+ ignore (type_term env ty t1);
+ ignore (type_term env ty t2);
+ ty
+
+ | Tapp (_,_,_) -> Error.not_yet "logic function application"
+ | Tunion _ -> Error.not_yet "tset union"
+ | Tinter _ -> Error.not_yet "tset intersection"
+ | Tcomprehension (_,_,_) -> Error.not_yet "tset comprehension"
+ | Trange (_,_) -> Error.not_yet "trange"
+ | Tlet (_,_) -> Error.not_yet "let binding"
+
+ | TConst (LStr _ | LWStr _ | LReal _ | LEnum _)
+ | TBinOp (PlusPI,_,_)
+ | TBinOp (IndexPI,_,_)
+ | TBinOp (MinusPI,_,_)
+ | TAddrOf _
+ | TStartOf _
+ | Toffset _
+ | Tlambda (_,_)
+ | TDataCons (_,_)
+ | Tbase_addr (_,_)
+ | TUpdate (_,_,_)
+ | Ttypeof _
+ | Ttype _
+ | Tempty_set -> raise Not_an_integer
+ in
+ Memo.memo (fun t -> let ty = infer t in coerce ~ctx ty) t
+
+(* TODO: maybe useful to memoize the result (only for relations)? *)
+let rec type_predicate_named env p =
+ Cil.CurrentLoc.set p.loc;
+ let ty = match p.content with
+ | Pfalse | Ptrue -> c_int
+ | Papp _ -> Error.not_yet "logic function application"
+ | Pseparated _ -> Error.not_yet "\\separated"
+ | Pdangling _ -> Error.not_yet "\\dangling"
+ | Prel(_, t1, t2) ->
+ let i1 = Interval.infer env t1 in
+ let i2 = Interval.infer env t2 in
+ let i = Interval.join i1 i2 in
+ let ctx = ty_of_interv i in
+ ignore (type_term env ~ctx t1);
+ ignore (type_term env ~ctx t2);
+ ctx
+ | Pand(p1, p2)
+ | Por(p1, p2)
+ | Pxor(p1, p2)
+ | Pimplies(p1, p2)
+ | Piff(p1, p2) ->
+ ignore (type_predicate_named env p1);
+ ignore (type_predicate_named env p2);
+ c_int
+ | Pnot p ->
+ ignore (type_predicate_named env p);
+ c_int
+ | Pif(t, p1, p2) ->
+ ignore (type_term env ~ctx:c_int t);
+ ignore (type_predicate_named env p1);
+ ignore (type_predicate_named env p2);
+ c_int
+ | Plet _ -> Error.not_yet "let _ = _ in _"
+ | Pforall(bounded_vars, { content = Pimplies(hyps, goal) })
+ | Pexists(bounded_vars, { content = Pand(hyps, goal) }) ->
+ let guards = !compute_quantif_guards_ref p bounded_vars hyps in
+ let env =
+ List.fold_left
+ (fun env (t1, r1, x, r2, t2) ->
+ let i1 = Interval.infer env t1 in
+ let i1 = match r1 with
+ | Rlt -> Interval.add i1 Integer.one
+ | Rle -> i1
+ | _ -> assert false
+ in
+ let i2 = Interval.infer env t2 in
+ (* add one to [i2], since we increment the loop counter one more
+ time before going out the loop. *)
+ let i2 = match r2 with
+ | Rlt -> i2
+ | Rle -> Interval.add i2 Integer.one
+ | _ -> assert false
+ in
+ let i = Interval.join i1 i2 in
+ let ctx = ty_of_interv i in
+ ignore (type_term env ~ctx t1);
+ ignore (type_term env ~ctx t2);
+ Interval.Env.add x i env)
+ env
+ guards
+ in
+ type_predicate_named env goal
+
+ | Pforall _ -> Error.not_yet "unguarded \\forall quantification"
+ | Pexists _ -> Error.not_yet "unguarded \\exists quantification"
+ | Pat(p, _) -> type_predicate_named env p
+ | Pfresh _ -> Error.not_yet "\\fresh"
+ | Psubtype _ -> Error.not_yet "subtyping relation" (* Jessie specific *)
+ | Pinitialized _
+ | Pfreeable _
+ | Pallocable _
+ | Pvalid _
+ | Pvalid_read _ ->
+ c_int
+ in
+ (coerce ~ctx:c_int ty).ty
+
+let type_named_predicate ?(must_clear=true) p =
+ if not (Options.Gmp_only.get ()) then begin
+ Options.feedback ~dkey ~level:3 "typing predicate %a."
+ Printer.pp_predicate_named p;
+ if must_clear then Memo.clear ();
+ ignore (type_predicate_named Interval.Env.empty p)
+ end
+
+let generic_typ get_ty t =
+ Cil.CurrentLoc.set t.term_loc;
+ if Options.Gmp_only.get () then
+ (match t.term_type with
+ | Linteger -> Mpz.t ()
+ | Ctype ty when Cil.isIntegralType ty -> Mpz.t ()
+ | Ctype ty -> ty
+ | Ltype _ as ty when Logic_const.is_boolean_type ty -> Mpz.t ()
+ | Ltype _ -> Error.not_yet "typing of user-defined logic type"
+ | Lvar _ -> Error.not_yet "type variable"
+ | Lreal -> TFloat(FLongDouble, [])
+ | Larrow _ -> Error.not_yet "functional type")
+ else
+ let info = Memo.get t in
+ match get_ty info with
+ | Gmp -> Mpz.t ()
+ | C_type ik -> TInt(ik, [])
+
+let typ_of_term = generic_typ (fun i -> i.ty)
+
+let cast_of_term t =
+ try
+ Some
+ (generic_typ
+ (fun i ->
+ match i.cast with None -> raise Exit | Some ty -> ty)
+ t)
+ with Exit ->
+ None
+
+let clear = Memo.clear
+
+(******************************************************************************)
+(** {2 Other typing-related functions} *)
+(******************************************************************************)
+
+let is_representable n k =
+ if Options.Gmp_only.get () then
+ match k with
+ | IBool | IChar | ISChar | IUChar | IInt | IUInt | IShort | IUShort
+ | ILong | IULong ->
+ true
+ | ILongLong | IULongLong ->
+ (* no GMP initializer from a long long *)
+ false
+ else
+ Integer.ge n Integer.min_int64 && Integer.le n Integer.max_int64
+
+(*
+Local Variables:
+compile-command: "make"
+End:
+*)
diff --git a/src/plugins/e-acsl/new_typing.mli b/src/plugins/e-acsl/new_typing.mli
new file mode 100644
index 00000000000..4bd4aeb94c3
--- /dev/null
+++ b/src/plugins/e-acsl/new_typing.mli
@@ -0,0 +1,68 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-2015 *)
+(* 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 license/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+(******************************************************************************)
+(** {2 Typing} *)
+(******************************************************************************)
+
+type integer_ty =
+ | Gmp
+ | C_type of ikind
+
+val type_named_predicate: ?must_clear:bool -> predicate named -> unit
+(** Compute the type of each term of the given predicate. *)
+
+val typ_of_term: term -> typ
+(** Get the type of the given term. {!type_named_predicate} must already have
+ been called on the englobing predicate. *)
+
+val cast_of_term: term -> typ option
+(** Get the type which the given term must be converted to after its translation
+ (if any). {!type_named_predicate} must already have been called on the
+ englobing predicate. *)
+
+val clear: unit -> unit
+(** Remove all the previously computed types. *)
+
+(******************************************************************************)
+(** {2 Other typing-related functions} *)
+(******************************************************************************)
+
+val is_representable: Integer.t -> ikind -> bool
+(** Is the given constant representable in the given kind? *)
+
+(******************************************************************************)
+(** {2 Internal stuff} *)
+(******************************************************************************)
+
+val compute_quantif_guards_ref
+ : (predicate named -> logic_var list -> predicate named ->
+ (term * relation * logic_var * relation * term) list) ref
+(** Forward reference. *)
+
+(*
+Local Variables:
+compile-command: "make"
+End:
+*)
--
GitLab