Skip to content
Snippets Groups Projects
Commit 97209797 authored by Julien Signoles's avatar Julien Signoles
Browse files

[e-acsl] fixed several bugs in type system

parent 621d615d
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/typing.ml
+ 92
− 64
View file @ 97209797
......@@ -128,7 +128,7 @@ module BI = My_bigint
type eacsl_typ =
| Interv of BI.t * BI.t
| Z
| No_integral(* of logic_type*)
| No_integral of logic_type
let typ_of_eacsl_typ = function
| Interv(l, u) ->
......@@ -141,7 +141,12 @@ let typ_of_eacsl_typ = function
with Not_found ->
Mpz.t)
| Z -> Mpz.t
| No_integral(* _*) -> assert false
| No_integral (Ctype ty) -> ty
| No_integral (Ltype _) -> Error.not_yet "typing of user-defined logic type"
| No_integral (Lvar _) -> Error.not_yet "type variable"
| No_integral Linteger -> assert false
| No_integral Lreal -> Error.not_yet "real numbers"
| No_integral (Larrow _) -> Error.not_yet "functional type"
let eacsl_typ_of_typ = function
| TInt(k, _) as ty ->
......@@ -151,7 +156,7 @@ let eacsl_typ_of_typ = function
else BI.zero, max_unsigned_number n
in
Interv(l, u)
| _ -> No_integral
| ty -> No_integral (Ctype ty)
exception Cannot_compare
let meet ty1 ty2 = match ty1, ty2 with
......@@ -159,16 +164,18 @@ let meet ty1 ty2 = match ty1, ty2 with
| 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
| No_integral t1, No_integral t2 when Logic_type.equal t1 t2 -> ty1
| 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
| No_integral t1, No_integral t2 when Logic_type.equal t1 t2 -> ty1
| No_integral _, No_integral _
| (Z | Interv _), No_integral _
| No_integral _, (Z | Interv _) -> raise Cannot_compare
module Global_env: sig
val get: term -> typ
......@@ -189,21 +196,26 @@ end = struct
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)
let ty = typ_of_eacsl_typ typ in
try
let old = H.find tbl t in
assert (Typ.equal old ty)
with Not_found ->
H.add tbl t ty
end
let typ_of_term = Global_env.get
let clear = Global_env.clear
let int_to_interv n =
let b = BI.of_int n in
Interv (b, b)
let rec type_constant = function
let rec type_constant ty = function
| CInt64(n, _, _) -> Interv(n, n)
| CChr c -> type_constant (charConstToInt c)
| CStr _ | CWStr _ | CReal _ | CEnum _ -> No_integral
| CChr c -> type_constant ty (charConstToInt c)
| CStr _ | CWStr _ | CReal _ | CEnum _ -> No_integral ty
let size_of ty =
try int_to_interv (sizeOf_int ty)
......@@ -212,30 +224,31 @@ let size_of ty =
let align_of ty = int_to_interv (alignOf_int ty)
let rec type_term env t =
let lty = t.term_type in
let get_cty t = match t.term_type with Ctype ty -> ty | _ -> assert false in
let ty = match t.term_node with
| TConst c -> type_constant c
| TLval lv -> type_term_lval env t.term_type lv
| TConst c -> type_constant lty c
| TLval lv -> type_term_lval env lty 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
size_of (get_cty t)
| 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
align_of (get_cty t)
| 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(BNot, t) ->
unary_arithmetic
(fun l u ->
let nl = BI.lognot l in
let nu = BI.lognot u in
BI.min nl nu, BI.max nl nu)
env
t
| TUnOp(LNot, t) ->
ignore (type_term env t);
Interv(BI.zero, BI.one)
......@@ -245,32 +258,28 @@ let rec type_term env t =
| TBinOp((PlusPI | IndexPI | MinusPI | MinusPP), t1, t2) ->
ignore (type_term env t1);
ignore (type_term env t2);
No_integral
No_integral lty
| 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(Mult, t1, t2) -> signed_rule BI.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))
let div a b =
try BI.c_div a b
with Division_by_zero ->
(* either the generated code will be dead (e.g. [false && 1/0])
or it contains a potential RTE and thus it is actually equivalent
to dead code. In any case, any type is correct at this point and
we generate the less restrictive one (0 is always representable)
in order to be as more precise as possible. *)
BI.zero
in
signed_rule div env t1 t2
| TBinOp(Mod, t1, t2) ->
let modu a b =
try BI.c_rem a b with Division_by_zero -> BI.zero (* see Div *)
in
binary_arithmetic div env t1 t2
| TBinOp(Mod, _t1, _t2) ->
Error.not_yet "modulo"
signed_rule modu env t1 t2
| 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) ->
......@@ -283,7 +292,9 @@ let rec type_term env 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
| TAddrOf lv | TStartOf lv ->
ignore (type_term_lval env lty lv);
No_integral lty
| Tapp _ -> Error.not_yet "applying logic function"
| Tlambda _ -> Error.not_yet "functional"
| TDataCons _ -> Error.not_yet "constructor"
......@@ -316,14 +327,23 @@ and type_term_lval env ty (h, 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)
| TVar lv ->
(try Logic_var.Map.find lv env
with Not_found ->
(* C variable *)
(* match lty with*) (* don't work yet: see bts #1064 *)
match lv.lv_type with
| Ctype ty -> eacsl_typ_of_typ ty
| _ ->
Options.fatal "invalid type for logic var %a: %a"
Logic_var.pretty lv Logic_type.pretty lv.lv_type)
| 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
| Ltype _ | Lvar _ | Lreal | Larrow _ -> No_integral lty
and type_term_offset env = function
| TNoOffset -> ()
......@@ -339,7 +359,7 @@ and unary_arithmetic op env t =
let l, u = op l u in
Interv (l, u)
| Z -> Z
| No_integral -> assert false
| No_integral _ -> assert false
and binary_arithmetic op env t1 t2 =
let ty1 = type_term env t1 in
......@@ -348,9 +368,21 @@ and binary_arithmetic op env t1 t2 =
| Interv(l1, u1), Interv(l2, u2) ->
let l, u = op l1 u1 l2 u2 in
Interv (l, u)
| No_integral, _ | _, No_integral -> assert false
| No_integral _, _ | _, No_integral _ -> assert false
| _, Z | Z, _ -> Z
and signed_rule op env t1 t2 =
(* probably not the most efficient way to compute the result, but the
shortest *)
let compute l1 u1 l2 u2 =
let a = op l1 l2 in
let b = op l1 u2 in
let c = op u1 l2 in
let d = op 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 compute env t1 t2
let compute_quantif_guards_ref
: (predicate named -> logic_var list -> predicate named ->
(term * relation * logic_var * relation * term) list) ref
......@@ -374,11 +406,10 @@ let rec type_predicate_named env p = match p.content with
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;
| Pexists(bounded_vars, { content = Pand(hyps, goal) }) ->
let env =
List.fold_left
(fun _env (t1, r1, x, r2, t2) ->
(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)
......@@ -399,6 +430,7 @@ let rec type_predicate_named env p = match p.content with
env
(!compute_quantif_guards_ref p bounded_vars hyps)
in
type_predicate_named env hyps;
type_predicate_named env goal
| Pforall _ -> Error.not_yet "unguarded \\forall quantification"
| Pexists _ -> Error.not_yet "unguarded \\exists quantification"
......@@ -410,14 +442,10 @@ let rec type_predicate_named env p = match p.content with
| 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
let type_named_predicate p =
Options.debug ~level:2 "typing predicate %a" d_predicate_named p;
clear ();
type_predicate_named Logic_var.Map.empty p
(*
Local Variables:
......
src/plugins/e-acsl/typing.mli
+ 2
− 1
View file @ 97209797
......@@ -41,8 +41,9 @@ val is_representable: My_bigint.t -> ikind -> string option -> bool
(* NEW TYPE SYSTEM *)
(******************************************************************************)
val type_predicate: identified_predicate -> unit
val type_named_predicate: predicate named -> unit
val typ_of_term: term -> typ
val clear: unit -> unit
val compute_quantif_guards_ref
: (predicate named -> logic_var list -> predicate named ->
......
src/plugins/e-acsl/visit.ml
+ 18
− 18
View file @ 97209797
......@@ -443,6 +443,14 @@ let assumes_predicate bhv =
Logic_const.ptrue
bhv.b_assumes
let convert_named_predicate env p =
Typing.type_named_predicate p;
let e, env = named_predicate_to_exp env p in
assert (Typ.equal (typeOf e) intType);
Env.add_stmt
env
(Misc.mk_e_acsl_guard ~reverse:true (Env.annotation_kind env) e p)
let convert_preconditions env behaviors =
let env = Env.set_annotation_kind env Misc.Precondition in
let do_behavior env b =
......@@ -455,10 +463,7 @@ let convert_preconditions env behaviors =
~loc
(assumes_pred, Logic_const.unamed ~loc p.ip_content)
in
let e, env = named_predicate_to_exp env p in
Env.add_stmt
env
(Misc.mk_e_acsl_guard ~reverse:true (Env.annotation_kind env) e p))
convert_named_predicate env p)
env
b.b_requires
in
......@@ -484,10 +489,7 @@ let convert_postconditions env behaviors =
~loc
(Logic_const.pold ~loc assumes_pred, Logic_const.unamed ~loc p)
in
let e, env = named_predicate_to_exp env p in
Env.add_stmt
env
(Misc.mk_e_acsl_guard ~reverse:true (Env.annotation_kind env) e p)
convert_named_predicate env p
| Exits | Breaks | Continues | Returns ->
Error.not_yet "@[abnormal termination case in behavior@]")
env
......@@ -510,13 +512,6 @@ let convert_pre_spec env spec =
let convert_post_spec env spec =
Error.handle (fun env -> convert_postconditions env spec.spec_behavior) env
let convert_named_predicate env p =
let e, env = named_predicate_to_exp env p in
assert (Typ.equal (typeOf e) intType);
Env.add_stmt
env
(Misc.mk_e_acsl_guard ~reverse:true (Env.annotation_kind env) e p)
let convert_pre_code_annotation env annot =
let convert env = match annot.annot_content with
| AAssert(l, p) | AInvariant(l, false (* invariant as assertion *), p)
......@@ -735,10 +730,15 @@ class e_acsl_visitor prj generate = object (self)
end
let do_visit ?(prj=Project.current ()) generate =
let vis = new e_acsl_visitor prj generate in
let vis =
Extlib.try_finally
~finally:Typing.clear
(new e_acsl_visitor prj)
generate
in
first_global := true;
(* explicit type annotation in order to check that no new method is introduced
by error *)
(* explicit type annotation in order to check that no new method is
introduced by error *)
(vis : Visitor.frama_c_visitor)
(*
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment