From 621d615db766e0c6407e68c369417b70f8ffddb0 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 13 Jan 2012 15:41:45 +0000
Subject: [PATCH] [e-acsl] type system implemented. Yet unused and untested.
---
src/plugins/e-acsl/TODO | 1 +
src/plugins/e-acsl/VERSION | 2 +-
src/plugins/e-acsl/quantif.ml | 2 +
src/plugins/e-acsl/typing.ml | 302 ++++++++++++++++++++++++++++++++++
src/plugins/e-acsl/typing.mli | 11 ++
src/plugins/e-acsl/visit.ml | 2 +-
6 files changed, 318 insertions(+), 2 deletions(-)
diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index f8142741410..fa3093d4668 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -21,6 +21,7 @@
(par ex pour indiquer le nom de la variable d'origine, ou son rôle)
- vérifier le code de la division et du modulo
(div et modulo mathématiques différents des div et modulo de l'ANSI C99)
+- NULL implemented as 0
##############
# KNOWN BUGS #
diff --git a/src/plugins/e-acsl/VERSION b/src/plugins/e-acsl/VERSION
index 49d59571fbf..209580245f3 100644
--- a/src/plugins/e-acsl/VERSION
+++ b/src/plugins/e-acsl/VERSION
@@ -1 +1 @@
-0.1
+0.1+dev
diff --git a/src/plugins/e-acsl/quantif.ml b/src/plugins/e-acsl/quantif.ml
index f50d0132f65..0f8764acea5 100644
--- a/src/plugins/e-acsl/quantif.ml
+++ b/src/plugins/e-acsl/quantif.ml
@@ -82,6 +82,8 @@ let compute_quantif_guards quantif bounded_vars hyps =
Error.untypable msg);
List.rev acc
+let () = Typing.compute_quantif_guards_ref := compute_quantif_guards
+
module Label_ids =
State_builder.Counter(struct let name = "E_ACSL.Label_ids" end)
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 4f131e9563a..e325ed68c14 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -117,6 +117,308 @@ let is_representable _n k _s = match k with
| ILongLong | IULongLong ->
false
+(******************************************************************************)
+(* NEW TYPE SYSTEM *)
+(******************************************************************************)
+
+open Cil_datatype
+
+module BI = My_bigint
+
+type eacsl_typ =
+ | Interv of BI.t * BI.t
+ | Z
+ | No_integral(* of logic_type*)
+
+let typ_of_eacsl_typ = function
+ | Interv(l, u) ->
+ let is_pos = BI.ge l BI.zero in
+ (try
+ let mk k = TInt(k, []) in
+ let ty_l = mk (intKindForValue l is_pos) in
+ let ty_u = mk (intKindForValue u is_pos) in
+ arithmeticConversion ty_l ty_u
+ with Not_found ->
+ Mpz.t)
+ | Z -> Mpz.t
+ | No_integral(* _*) -> assert false
+
+let eacsl_typ_of_typ = function
+ | TInt(k, _) as ty ->
+ let n = bitsSizeOf ty in
+ let l, u =
+ if isSigned k then min_signed_number n, max_signed_number n
+ else BI.zero, max_unsigned_number n
+ in
+ Interv(l, u)
+ | _ -> No_integral
+
+exception Cannot_compare
+let meet ty1 ty2 = match ty1, ty2 with
+ | Interv(l1, u1), Interv(l2, u2) -> Interv(BI.max l1 l2, BI.min u1 u2)
+ | Interv _, Z -> ty1
+ | Z, Interv _ -> ty2
+ | Z, Z -> Z
+ | No_integral, No_integral -> No_integral
+ | (Z | Interv _), No_integral
+ | No_integral, (Z | Interv _) -> raise Cannot_compare
+
+let join ty1 ty2 = match ty1, ty2 with
+ | Interv(l1, u1), Interv(l2, u2) -> Interv(BI.min l1 l2, BI.max u1 u2)
+ | Interv _, Z | Z, Interv _ | Z, Z -> Z
+ | No_integral, No_integral -> No_integral
+ | (Z | Interv _), No_integral
+ | No_integral, (Z | Interv _) -> raise Cannot_compare
+
+module Global_env: sig
+ val get: term -> typ
+ val add: term -> eacsl_typ -> unit
+ val clear: unit -> unit
+end = struct
+
+ module H = Hashtbl.Make
+ (struct
+ type t = term
+ let equal (t1:term) t2 = t1 == t2
+ let hash = Term.hash
+ end)
+
+ let tbl = H.create 17
+
+ let clear () = H.clear tbl
+ let get t = try H.find tbl t with Not_found -> assert false
+
+ let add t typ =
+ assert (not (H.mem tbl t));
+ H.add tbl t (typ_of_eacsl_typ typ)
+
+end
+
+let typ_of_term = Global_env.get
+
+let int_to_interv n =
+ let b = BI.of_int n in
+ Interv (b, b)
+
+let rec type_constant = function
+ | CInt64(n, _, _) -> Interv(n, n)
+ | CChr c -> type_constant (charConstToInt c)
+ | CStr _ | CWStr _ | CReal _ | CEnum _ -> No_integral
+
+let size_of ty =
+ try int_to_interv (sizeOf_int ty)
+ with SizeOfError _ -> eacsl_typ_of_typ ulongLongType
+
+let align_of ty = int_to_interv (alignOf_int ty)
+
+let rec type_term env t =
+ let ty = match t.term_node with
+ | TConst c -> type_constant c
+ | TLval lv -> type_term_lval env t.term_type lv
+ | TSizeOf ty -> size_of ty
+ | TSizeOfE t ->
+ ignore (type_term env t);
+ let ty = match t.term_type with
+ | Ctype ty -> ty
+ | _ -> assert false
+ in
+ size_of ty
+ | TSizeOfStr s -> int_to_interv (String.length s + 1 (* '\0' *))
+ | TAlignOf ty -> align_of ty
+ | TAlignOfE t ->
+ ignore (type_term env t);
+ let ty = match t.term_type with
+ | Ctype ty -> ty
+ | _ -> assert false
+ in
+ align_of ty
+ | TUnOp(Neg, t) ->
+ unary_arithmetic
+ (fun l u -> let opp = BI.sub BI.zero in opp u, opp l) env t
+ | TUnOp(BNot, _) -> Error.not_yet "missing unary bitwise operator"
+ | TUnOp(LNot, t) ->
+ ignore (type_term env t);
+ Interv(BI.zero, BI.one)
+ | TBinOp(PlusA, t1, t2) ->
+ let add l1 u1 l2 u2 = BI.add l1 l2, BI.add u1 u2 in
+ binary_arithmetic add env t1 t2
+ | TBinOp((PlusPI | IndexPI | MinusPI | MinusPP), t1, t2) ->
+ ignore (type_term env t1);
+ ignore (type_term env t2);
+ No_integral
+ | TBinOp(MinusA, t1, t2) ->
+ let sub l1 u1 l2 u2 = BI.sub l1 u2, BI.sub u1 l2 in
+ binary_arithmetic sub env t1 t2
+ | TBinOp(Mult, t1, t2) ->
+ let mul l1 u1 l2 u2 =
+ (* probably not the most efficient, but the shortest *)
+ let a = BI.mul l1 l2 in
+ let b = BI.mul l1 u2 in
+ let c = BI.mul u1 l2 in
+ let d = BI.mul u1 u2 in
+ BI.min a (BI.min b (BI.min c d)), BI.max a (BI.max b (BI.max c d))
+ in
+ binary_arithmetic mul env t1 t2
+ | TBinOp(Div, t1, t2) ->
+ let div l1 u1 l2 u2 =
+ (* probably not the most efficient, but the shortest *)
+ let a = BI.div l1 l2 in
+ let b = BI.div l1 u2 in
+ let c = BI.div u1 l2 in
+ let d = BI.div u1 u2 in
+ BI.min a (BI.min b (BI.min c d)), BI.max a (BI.max b (BI.max c d))
+ in
+ binary_arithmetic div env t1 t2
+ | TBinOp(Mod, _t1, _t2) ->
+ Error.not_yet "modulo"
+ | TBinOp(Shiftlt, _t1, _t2) | TBinOp(Shiftrt, _t1, _t2) ->
+ Error.not_yet "left/right shift"
+ | TBinOp((Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr), t1, t2) ->
+ ignore (type_term env t1);
+ ignore (type_term env t2);
+ Interv(BI.zero, BI.one)
+ | TBinOp((BAnd | BXor | BOr), _t1, _t2) ->
+ Error.not_yet "missing binary bitwise operator"
+ | TCastE(ty, t) ->
+ let ty_t = type_term env t in
+ let ty_c = eacsl_typ_of_typ ty in
+ (try meet ty_c ty_t with Cannot_compare -> ty_c)
+ | TAddrOf _ | TStartOf _ -> No_integral
+ | Tapp _ -> Error.not_yet "applying logic function"
+ | Tlambda _ -> Error.not_yet "functional"
+ | TDataCons _ -> Error.not_yet "constructor"
+ | Tif(t1, t2, t3) ->
+ ignore (type_term env t1);
+ let ty2 = type_term env t2 in
+ let ty3 = type_term env t3 in
+ (try join ty2 ty3 with Cannot_compare -> assert false)
+ | Tat(t, _) -> type_term env t
+ | Tbase_addr _ -> Error.not_yet "\\base_addr"
+ | Tblock_length _ -> Error.not_yet "\\block_length"
+ | Tnull -> int_to_interv 0
+ | TCoerce _ -> Error.not_yet "coercion" (* Jessie specific *)
+ | TCoerceE _ -> Error.not_yet "expression coercion" (* Jessie specific *)
+ | TUpdate _ -> Error.not_yet "functional update"
+ | Ttypeof _ -> Error.not_yet "typeof"
+ | Ttype _ -> Error.not_yet "C type"
+ | Tempty_set -> Error.not_yet "empty tset"
+ | Tunion _ -> Error.not_yet "union of tsets"
+ | Tinter _ -> Error.not_yet "intersection of tsets"
+ | Tcomprehension _ -> Error.not_yet "tset comprehension"
+ | Trange _ -> Error.not_yet "range"
+ | Tlet _ -> Error.not_yet "let binding"
+ in
+ Global_env.add t ty;
+ ty
+
+and type_term_lval env ty (h, o) =
+ type_term_offset env o;
+ type_term_lhost env ty h
+
+and type_term_lhost env lty = function
+ | TVar lv -> (try Logic_var.Map.find lv env with Not_found -> assert false)
+ | TResult ty -> eacsl_typ_of_typ ty
+ | TMem t ->
+ ignore (type_term env t);
+ match lty with
+ | Ctype ty -> eacsl_typ_of_typ ty
+ | Linteger -> Z
+ | Ltype _ | Lvar _ | Lreal | Larrow _ -> No_integral
+
+and type_term_offset env = function
+ | TNoOffset -> ()
+ | TField(_, o) -> type_term_offset env o
+ | TIndex(t, o) ->
+ ignore (type_term env t);
+ type_term_offset env o
+
+and unary_arithmetic op env t =
+ let ty = type_term env t in
+ match ty with
+ | Interv(l, u) ->
+ let l, u = op l u in
+ Interv (l, u)
+ | Z -> Z
+ | No_integral -> assert false
+
+and binary_arithmetic op env t1 t2 =
+ let ty1 = type_term env t1 in
+ let ty2 = type_term env t2 in
+ match ty1, ty2 with
+ | Interv(l1, u1), Interv(l2, u2) ->
+ let l, u = op l1 u1 l2 u2 in
+ Interv (l, u)
+ | No_integral, _ | _, No_integral -> assert false
+ | _, Z | Z, _ -> Z
+
+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"
+
+let rec type_predicate_named env p = match p.content with
+ | Pfalse | Ptrue -> ()
+ | Papp _ -> Error.not_yet "logic function application"
+ | Pseparated _ -> Error.not_yet "separated"
+ | Prel(_, t1, t2) ->
+ ignore (type_term env t1);
+ ignore (type_term env t2)
+ | Pand(p1, p2) | Por(p1, p2) | Pxor(p1, p2) | Pimplies(p1, p2)
+ | Piff(p1, p2) ->
+ type_predicate_named env p1;
+ type_predicate_named env p2
+ | Pnot p -> type_predicate_named env p
+ | Pif(t, p1, p2) ->
+ ignore (type_term env t);
+ type_predicate_named env p1;
+ type_predicate_named env p2
+ | Plet _ -> Error.not_yet "let _ = _ in _"
+ | Pforall(bounded_vars, { content = Pimplies(hyps, goal) })
+ | Pexists(bounded_vars, { content = Pimplies(hyps, goal) }) ->
+ type_predicate_named env hyps;
+ let env =
+ List.fold_left
+ (fun _env (t1, r1, x, r2, t2) ->
+ let ty1 = type_term env t1 in
+ let ty1 = match ty1, r1 with
+ | Interv(l, u), Rlt -> Interv(BI.add l BI.one, BI.add u BI.one)
+ | Interv(l, u), Rle -> Interv(l, u)
+ | Z, (Rlt | Rle) -> Z
+ | _, _ -> assert false
+ in
+ let ty2 = type_term env t2 in
+ (* add one here, since we increment the loop counter one more time
+ before going out the loop. *)
+ let ty2 = match ty2, r2 with
+ | Interv(l, u), Rlt -> Interv(l, u)
+ | Interv(l, u), Rle -> Interv(BI.add l BI.one, BI.add u BI.one)
+ | Z, (Rlt | Rle) -> Z
+ | _, _ -> assert false
+ in
+ Logic_var.Map.add x (join ty1 ty2) env)
+ env
+ (!compute_quantif_guards_ref p bounded_vars hyps)
+ 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
+ | Pvalid _ -> Error.not_yet "\\valid"
+ | Pvalid_index _ -> Error.not_yet "\\valid_index"
+ | Pvalid_range _ -> Error.not_yet "\\valid_range"
+ | Pfresh _ -> Error.not_yet "\\fresh"
+ | Psubtype _ -> Error.not_yet "subtyping relation" (* Jessie specific *)
+ | Pinitialized _ -> Error.not_yet "\\initialized"
+
+let type_id_predicate env p =
+ type_predicate_named
+ env
+ { name = []; loc = Location.unknown; content = p.ip_content }
+
+let type_predicate p =
+ Global_env.clear ();
+ type_id_predicate Logic_var.Map.empty p
+
(*
Local Variables:
compile-command: "make"
diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli
index cbfa80a6b37..6c321b3283a 100644
--- a/src/plugins/e-acsl/typing.mli
+++ b/src/plugins/e-acsl/typing.mli
@@ -37,6 +37,17 @@ val is_representable: My_bigint.t -> ikind -> string option -> bool
(** Is the given constant representable?
(See [Cil_types.CInt64] for details about arguments *)
+(******************************************************************************)
+(* NEW TYPE SYSTEM *)
+(******************************************************************************)
+
+val type_predicate: identified_predicate -> unit
+val typ_of_term: term -> typ
+
+val compute_quantif_guards_ref
+ : (predicate named -> logic_var list -> predicate named ->
+ (term * relation * logic_var * relation * term) list) ref
+
(*
Local Variables:
compile-command: "make"
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index faa1d7d2d00..57f19623d97 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -407,7 +407,7 @@ let rec named_predicate_to_exp env p =
Logic_const.pimplies ~loc (p2, p1)))
| Pnot p ->
let e, env = named_predicate_to_exp env p in
- new_exp ~loc (UnOp(LNot, e, TInt(IInt, []))), env
+ new_exp ~loc (UnOp(LNot, e, intType)), env
| Pif(t, p2, p3) ->
let e1, env1 = term_to_exp env (Ctype intType) t in
let (_, env2 as res2) = named_predicate_to_exp (Env.push env1) p2 in
--
GitLab