new type system (still unused, but compiled)

src/plugins/e-acsl/Makefile.in

@@ -62,6 +62,7 @@ PLUGIN_CMO:= local_config \
 	env \
 	interval \
 	typing \
+	new_typing \
 	quantif \
 	translate \
 	loops \

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 =

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
 

src/plugins/e-acsl/new_typing.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  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:
+*)

src/plugins/e-acsl/new_typing.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  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:
+*)