diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index 958147981d2e6ef21740a6be8a9ac9d4f0eb7f3f..15e3a7347292bec6e963e8d9d9bc77ae880caebe 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -406,29 +406,38 @@ module Id_term_in_profile =
Datatype.Pair_with_collections
(Misc.Id_term)
(Profile)
- (struct let module_name = "E_ACSL.Typing.Id_term_in_profile" end)
+ (struct let module_name = "E_ACSL.Interval.Id_term_in_profile" end)
-module Logic_environment : sig
+(* logic environment: interval of all bound variables. It is built of two
+ components
+ - a profile for variables bound through functions arguments
+ - an association list for variables bound by a let or a quantification *)
+module Logic_env : sig
type t
+ (* add a new binding for a let or a quantification binder*)
val add_let_quantif_binding : t -> logic_var -> ival -> t
- val create : logic_var list -> ival list -> t
+ (* create a new environment from a profile, for function calls *)
+ val make : logic_var list -> ival list -> t
+ (* find a logic variable in the environment *)
val find : t -> logic_var -> ival
+ (* get the profile of the logic environment, i.e. bindings through function
+ arguments*)
val get_profile : t -> ival list
end
= struct
- type env = (logic_var * ival) list
-
type t = { profile : logic_var list * Profile.t;
- let_quantif_bind : env}
+ let_quantif_bind : (logic_var * ival) list}
let add_let_quantif_binding env x i =
{ env with let_quantif_bind = (x, i) :: env.let_quantif_bind }
- let create args params_ival =
+ let make args params_ival =
{ profile = args , params_ival;
let_quantif_bind = [] }
let find env x =
+ (* Programs typically do not have many variables simulatneously bound, so a
+ linear search is fine here*)
try List.assoc x env.let_quantif_bind
with Not_found ->
let rec find = function
@@ -456,8 +465,8 @@ module LF_env : sig
val fixpoint :
infer : (
- ?force_infer:bool ->
- logic_env: Logic_environment.t ->
+ force:bool ->
+ logic_env: Logic_env.t ->
term ->
ival Error.result) ->
logic_info ->
@@ -469,13 +478,16 @@ module LF_env : sig
end
= struct
+ (* Environment to handle recursive functions: this environment stores the
+ logic functions that we have already started inferring along with their
+ profiles. This is necessary for the fixpoint algorithm. *)
module LFProf =
Datatype.Pair_with_collections (Cil_datatype.Logic_info) (Profile)
(struct
let module_name = "E_ACSL.Interval.LF_env.LFProf"
end)
- let tbl = LFProf.Hashtbl.create 97
+ let tbl = LFProf.Hashtbl.create 17
let clear () = LFProf.Hashtbl.clear tbl
@@ -486,18 +498,19 @@ end
let contain li = object
inherit Visitor.frama_c_inplace
- method !vpredicate p =
+ method! vpredicate p =
match p.pred_content with
| Papp (li_app,_,_) when Cil_datatype.Logic_info.equal li li_app ->
raise Recursive;
| _ -> Cil.DoChildren
- method !vterm t =
+ method! vterm t =
match t.term_node with
| Tapp(li_app,_,_) when Cil_datatype.Logic_info.equal li li_app ->
raise Recursive
| _ -> Cil.DoChildren
+ method! vlogic_type _ = Cil.SkipChildren
end
let is_rec li =
@@ -508,7 +521,8 @@ end
| LBterm t ->
(try ignore (Visitor.visitFramacTerm (contain li) t); false
with Recursive -> true)
- | LBreads _ | LBnone |LBinductive _ -> false
+ | LBreads _ | LBnone -> false
+ | LBinductive _ -> Error.not_yet "Inductive"
let interv_of_typ_containing_interv = function
| Float _ | Rational | Real | Nan as x ->
@@ -520,15 +534,15 @@ end
with Cil.Not_representable ->
top_ival
- let rec fixpoint ~(infer : ?force_infer:bool ->
- logic_env:Logic_environment.t ->
+ let rec fixpoint ~(infer : force:bool ->
+ logic_env:Logic_env.t ->
term ->
ival Error.result)
li args_ival t' ival =
- LFProf.Hashtbl.replace tbl (li,args_ival) ival;
+ LFProf.Hashtbl.replace tbl (li, args_ival) ival;
let get_res = Error.map (fun x -> x) in
- let logic_env = Logic_environment.create li.l_profile args_ival in
- let inferred_ival = get_res (infer ~force_infer:true ~logic_env t') in
+ let logic_env = Logic_env.make li.l_profile args_ival in
+ let inferred_ival = get_res (infer ~force:true ~logic_env t') in
if is_included inferred_ival ival
then
ival
@@ -537,18 +551,11 @@ end
end
-(* Memoization module which retrieves the computed info of some terms. If the
- info is already computed for a term, it is never recomputed *)
+(* Memoization module which retrieves the computed info of some terms *)
module Memo: sig
val memo:
- force_infer:bool ->
- profile:Profile.t ->
- (term -> ival) ->
- term ->
- ival Error.result
- val get: profile:Profile.t -> term -> ival Error.result
- val get_widened_profile: Profile.t -> term -> Profile.t
- val add_widened_profile: Profile.t -> term -> Profile.t -> unit
+ force_infer:bool -> Profile.t -> (term -> ival) -> term -> ival Error.result
+ val get: Profile.t -> term -> ival Error.result
val clear: unit -> unit
end = struct
(* The comparison over terms is the physical equality. It cannot be the
@@ -561,99 +568,94 @@ end = struct
new terms (see module {!Quantif}) which must be typed. The term
corresponding to the bound variable [x] is actually used twice: once in
the guard and once for encoding [x+1] when incrementing it. *)
- let tbl : ival Error.result Misc.Id_term.Hashtbl.t =
+ let nondep_tbl : ival Error.result Misc.Id_term.Hashtbl.t =
Misc.Id_term.Hashtbl.create 97
(* The interval of the logic function
- \\@ logic integer f (integer x) = x + 1;
+ //@ logic integer f (integer x) = x + 1;
depends on the interval of [x]. The same term [x+1] can be infered to be
in different intervals if the function [f] is applied several times with
different arguments. In this case, we add the interval of [x] as a key
to retrieve the type of [x+1].
There are two other kinds of binders for logical variables: [TLet] and
the quantifiers, however in those cases, a term is only ever translated
- once. Since we test with physical equality, the information is not needed
- to determine the environment.*)
+ once. *)
let dep_tbl : ival Error.result Id_term_in_profile.Hashtbl.t
= Id_term_in_profile.Hashtbl.create 97
- let widened_profile_tbl : Profile.t Id_term_in_profile.Hashtbl.t
- = Id_term_in_profile.Hashtbl.create 97
-
- let get_widened_profile profile t =
- Id_term_in_profile.Hashtbl.find_def
- widened_profile_tbl
- (t,profile)
- profile
-
- let add_widened_profile profile t args_ival =
- Id_term_in_profile.Hashtbl.add
- widened_profile_tbl
- (t,profile)
- args_ival
-
- let get_dep profile t =
- try Id_term_in_profile.Hashtbl.find dep_tbl (t,profile)
- with Not_found -> Error.not_memoized ()
-
- let get_nondep t =
- try Misc.Id_term.Hashtbl.find tbl t
- with Not_found -> Error.not_memoized ()
-
- let get ~profile t =
- match profile with
- | [] -> get_nondep t
- | _::_ -> get_dep profile t
-
- let memo_nondep ~force_infer f t =
- if force_infer then
- let x =
- try
- Result.Ok (f t);
- with Error.Not_yet _ | Error.Typing_error _ as exn -> Result.Error exn
- in
- Misc.Id_term.Hashtbl.replace tbl t x;
- x
- else
- try Misc.Id_term.Hashtbl.find tbl t
- with Not_found ->
+ (* Small functor to access the result of a memoized inference *)
+ module Accesses (X : Datatype.S_with_collections)
+ (Tbl: sig val tbl : ival Error.result X.Hashtbl.t end)
+ : sig
+ val get : X.Hashtbl.key -> ival Error.result
+ val memo : force_infer:bool -> (term -> ival) -> term -> X.Hashtbl.key ->
+ (ival, exn) Result.t
+ end = struct
+ let get k =
+ try X.Hashtbl.find Tbl.tbl k
+ with Not_found -> Error.not_memoized ()
+
+ let memo ~force_infer f t k =
+ if force_infer then
let x =
- try
- Result.Ok (f t);
+ try Result.Ok (f t);
with Error.Not_yet _ | Error.Typing_error _ as exn -> Result.Error exn
in
- Misc.Id_term.Hashtbl.add tbl t x;
+ X.Hashtbl.replace Tbl.tbl k x;
x
+ else
+ try X.Hashtbl.find Tbl.tbl k
+ with Not_found ->
+ let x =
+ try Result.Ok (f t);
+ with Error.Not_yet _ | Error.Typing_error _ as exn -> Result.Error exn
+ in
+ X.Hashtbl.add Tbl.tbl k x;
+ x
+ end
- let memo_dep ~force_infer f t profile =
- if force_infer then
- let x =
- try Result.Ok (f t)
- with Error.Not_yet _ | Error.Typing_error _ as exn -> Result.Error exn
- in
- Id_term_in_profile.Hashtbl.replace dep_tbl (t, profile) x;
- x
- else
- try
- Id_term_in_profile.Hashtbl.find dep_tbl (t, profile)
- with Not_found ->
- let x =
- try Result.Ok (f t)
- with Error.Not_yet _ | Error.Typing_error _ as exn -> Result.Error exn
- in
- Id_term_in_profile.Hashtbl.add dep_tbl (t, profile) x;
- x
+ module Nondep = Accesses (Misc.Id_term) (struct let tbl = nondep_tbl end)
+ module Dep = Accesses (Id_term_in_profile) (struct let tbl = dep_tbl end)
- let memo ~force_infer ~profile f t =
+ let get profile t =
match profile with
- | [] -> memo_nondep ~force_infer f t
- | _::_ -> memo_dep ~force_infer f t profile
+ | [] -> Nondep.get t
+ | _ :: _ -> Dep.get (t,profile)
+
+ let memo ~force_infer profile f t =
+ match profile with
+ | [] -> Nondep.memo ~force_infer f t t
+ | _::_ -> Dep.memo ~force_infer f t (t,profile)
let clear () =
Options.feedback ~level:4 "clearing the typing tables";
- Misc.Id_term.Hashtbl.clear tbl;
+ Misc.Id_term.Hashtbl.clear nondep_tbl;
Id_term_in_profile.Hashtbl.clear dep_tbl
+end
+
+(* For recursive functions, it is necessary to use a widened profile to query
+ the table (because of the fixpoint algorithm). This module associates to a
+ term in a profile, the profile that should be used to query the table *)
+module Widened_profile: sig
+ val get: Profile.t -> term -> Profile.t
+ val add: Profile.t -> term -> Profile.t -> unit
+ val clear: unit -> unit
+end = struct
+
+ let widened_profile_tbl : Profile.t Id_term_in_profile.Hashtbl.t
+ = Id_term_in_profile.Hashtbl.create 97
+
+ let get profile t =
+ Id_term_in_profile.Hashtbl.find_def widened_profile_tbl (t, profile) profile
+
+ let add profile t args_ival =
+ Id_term_in_profile.Hashtbl.add widened_profile_tbl (t, profile) args_ival
+
+ let clear () =
+ Options.feedback ~level:4 "clearing the typing tables";
+ Id_term_in_profile.Hashtbl.clear widened_profile_tbl
+
end
@@ -768,12 +770,10 @@ let infer_sum_product oper lambda min max = match lambda, min, max with
| Z.Overflow (* if the exponent of \product is too high *) -> top_ival)
| _ -> Error.not_yet "extended quantifiers with non-integer parameters"
-let rec infer ?(force_infer=false) ~logic_env t =
+let rec infer ~force ~logic_env t =
let get_cty t = match t.term_type with Ctype ty -> ty | _ -> assert false in
let get_res = Error.map (fun x -> x) in
let t = Logic_normalizer.get_term t in
- let infer_full = infer
- and infer = infer ~force_infer in
let compute t =
match t.term_node with
| TConst (Integer (n, _)) -> singleton n
@@ -787,87 +787,87 @@ let rec infer ?(force_infer=false) ~logic_env t =
in
let n = Integer.of_int (find_idx 0 enumitem.eihost.eitems) in
singleton n
- | TLval lv -> infer_term_lval ~logic_env lv
+ | TLval lv -> infer_term_lval ~force ~logic_env lv
| TSizeOf ty -> infer_sizeof ty
| TSizeOfE t ->
- ignore (infer ~logic_env t);
+ ignore (infer ~force ~logic_env t);
infer_sizeof (get_cty t)
| TSizeOfStr str -> singleton_of_int (String.length str + 1 (* '\0' *))
| TAlignOf ty -> infer_alignof ty
| TAlignOfE t ->
- ignore (infer ~logic_env t);
+ ignore (infer ~force ~logic_env t);
infer_alignof (get_cty t)
| TUnOp (Neg, t) ->
- let i = infer ~logic_env t in
+ let i = infer ~force ~logic_env t in
Error.map (lift_unop Ival.neg_int) i
| TUnOp (BNot, t) ->
- let i = infer ~logic_env t in
+ let i = infer ~force ~logic_env t in
Error.map (lift_unop Ival.bitwise_signed_not) i
| TUnOp (LNot, t) ->
- ignore(infer ~logic_env t);
+ ignore (infer ~force ~logic_env t);
Ival Ival.zero_or_one
| TBinOp ((Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr), t1, t2) ->
- ignore(infer ~logic_env t1);
- ignore(infer ~logic_env t2);
+ ignore (infer ~force ~logic_env t1);
+ ignore (infer ~force ~logic_env t2);
Ival Ival.zero_or_one
| TBinOp (PlusA, t1, t2) ->
- let i1 = infer ~logic_env t1 in
- let i2 = infer ~logic_env t2 in
+ let i1 = infer ~force ~logic_env t1 in
+ let i2 = infer ~force ~logic_env t2 in
Error.map2 (lift_arith_binop Ival.add_int) i1 i2
| TBinOp (MinusA, t1, t2) ->
- let i1 = infer ~logic_env t1 in
- let i2 = infer ~logic_env t2 in
+ let i1 = infer ~force ~logic_env t1 in
+ let i2 = infer ~force ~logic_env t2 in
Error.map2 (lift_arith_binop Ival.sub_int) i1 i2
| TBinOp (Mult, t1, t2) ->
- let i1 = infer ~logic_env t1 in
- let i2 = infer ~logic_env t2 in
+ let i1 = infer ~force ~logic_env t1 in
+ let i2 = infer ~force ~logic_env t2 in
Error.map2 (lift_arith_binop Ival.mul) i1 i2
| TBinOp (Div, t1, t2) ->
- let i1 = infer ~logic_env t1 in
- let i2 = infer ~logic_env t2 in
+ let i1 = infer ~force ~logic_env t1 in
+ let i2 = infer ~force ~logic_env t2 in
Error.map2 (lift_arith_binop Ival.div) i1 i2
| TBinOp (Mod, t1, t2) ->
- let i1 = infer ~logic_env t1 in
- let i2 = infer ~logic_env t2 in
+ let i1 = infer ~force ~logic_env t1 in
+ let i2 = infer ~force ~logic_env t2 in
Error.map2 (lift_arith_binop Ival.c_rem) i1 i2
| TBinOp (Shiftlt, t1, t2) ->
- let i1 = infer ~logic_env t1 in
- let i2 = infer ~logic_env t2 in
+ let i1 = infer ~force ~logic_env t1 in
+ let i2 = infer ~force ~logic_env t2 in
Error.map2 (lift_arith_binop Ival.shift_left) i1 i2
| TBinOp (Shiftrt, t1, t2) ->
- let i1 = infer ~logic_env t1 in
- let i2 = infer ~logic_env t2 in
+ let i1 = infer ~force ~logic_env t1 in
+ let i2 = infer ~force ~logic_env t2 in
Error.map2 (lift_arith_binop Ival.shift_right) i1 i2
| TBinOp (BAnd, t1, t2) ->
- let i1 = infer ~logic_env t1 in
- let i2 = infer ~logic_env t2 in
+ let i1 = infer ~force ~logic_env t1 in
+ let i2 = infer ~force ~logic_env t2 in
Error.map2 (lift_arith_binop Ival.bitwise_and) i1 i2
| TBinOp (BXor, t1, t2) ->
- let i1 = infer ~logic_env t1 in
- let i2 = infer ~logic_env t2 in
+ let i1 = infer ~force ~logic_env t1 in
+ let i2 = infer ~force ~logic_env t2 in
Error.map2 (lift_arith_binop Ival.bitwise_xor) i1 i2
| TBinOp (BOr, t1, t2) ->
- let i1 = infer ~logic_env t1 in
- let i2 = infer ~logic_env t2 in
+ let i1 = infer ~force ~logic_env t1 in
+ let i2 = infer ~force ~logic_env t2 in
Error.map2 (lift_arith_binop Ival.bitwise_or) i1 i2
| TCastE (ty, t) ->
- let src = infer ~logic_env t in
+ let src = infer ~force ~logic_env t in
let dst = interv_of_typ ty in
Error.map (fun src -> cast ~src ~dst) src
| Tif (t1, t2, t3) ->
- ignore (infer ~logic_env t1);
- let i2 = infer ~logic_env t2 in
- let i3 = infer ~logic_env t3 in
+ ignore (infer ~force ~logic_env t1);
+ let i2 = infer ~force ~logic_env t2 in
+ let i3 = infer ~force ~logic_env t3 in
Error.map2 join i2 i3
| Tat (t, _) ->
- get_res (infer ~logic_env t)
- | TBinOp (MinusPP, t, t2) ->
- ignore(infer ~logic_env t);
- ignore(infer ~logic_env t2);
- (match Cil.unrollType (get_cty t) with
+ get_res (infer ~force ~logic_env t)
+ | TBinOp (MinusPP, t1, t2) ->
+ ignore (infer ~force ~logic_env t1);
+ ignore (infer ~force ~logic_env t2);
+ (match Cil.unrollType (get_cty t1) with
| TArray(_, _, _) as ta ->
begin
try
@@ -884,7 +884,7 @@ let rec infer ?(force_infer=false) ~logic_env t =
| _ -> assert false)
| Tblock_length (_, t)
| Toffset(_, t) ->
- ignore (infer ~logic_env t);
+ ignore (infer ~force ~logic_env t);
(match Cil.unrollType (get_cty t) with
| TArray(_, _, _) as ta ->
begin
@@ -898,59 +898,49 @@ let rec infer ?(force_infer=false) ~logic_env t =
| TPtr _ -> Lazy.force interv_of_unknown_block
| _ -> assert false)
| Tnull -> singleton_of_int 0
- | TLogic_coerce (_, t) -> get_res (infer ~logic_env t)
+ | TLogic_coerce (_, t) -> get_res (infer ~force ~logic_env t)
| Tapp (li,_,args) ->
(match li.l_body with
- | LBpred p ->
- let args_ival =
+ | LBpred _ | LBterm _ ->
+ let profile =
List.map
- (fun arg -> get_res (infer ~logic_env arg))
+ (fun arg -> get_res (infer ~force ~logic_env arg))
args
in
- let logic_env = Logic_environment.create li.l_profile args_ival in
- ignore (infer_predicate ~logic_env p);
- Ival Ival.zero_or_one
- | LBterm t' ->
- if LF_env.is_rec li
- then
- let profile,args_ival =
- let profile =
- List.map
- (fun arg -> (get_res (infer ~logic_env arg)))
- args
- in
- profile, (List.map LF_env.interv_of_typ_containing_interv profile)
- in
- Memo.add_widened_profile profile t' args_ival;
- try let res = LF_env.find li args_ival in
- res;
- with Not_found ->
- LF_env.fixpoint ~infer:infer_full li args_ival t' (Ival Ival.bottom)
- else
- let args_ival =
- List.map
- (fun arg -> get_res (infer ~logic_env arg))
- args
- in
- let logic_env = Logic_environment.create li.l_profile args_ival in
- get_res (infer ~logic_env t')
+ (match li.l_body with
+ | LBpred p ->
+ let logic_env = Logic_env.make li.l_profile profile in
+ ignore (infer_predicate ~logic_env p);
+ Ival Ival.zero_or_one
+ | LBterm t' when LF_env.is_rec li ->
+ let
+ args_ival = List.map LF_env.interv_of_typ_containing_interv profile
+ in
+ Widened_profile.add profile t' args_ival;
+ (try LF_env.find li args_ival
+ with Not_found ->
+ LF_env.fixpoint ~infer li args_ival t' (Ival Ival.bottom))
+ | LBterm t' ->
+ let logic_env = Logic_env.make li.l_profile profile in
+ get_res (infer ~force ~logic_env t')
+ | _ -> assert false)
| LBnone when li.l_var_info.lv_name = "\\sum" ||
li.l_var_info.lv_name = "\\product" ->
(match args with
| [ t1; t2; { term_node = Tlambda([ k ], _) } as lambda ] ->
- let t1_iv = infer ~logic_env t1 in
- let t2_iv = infer ~logic_env t2 in
+ let t1_iv = infer ~force ~logic_env t1 in
+ let t2_iv = infer ~force ~logic_env t2 in
let k_iv = Error.map2 join t1_iv t2_iv in
let logic_env_with_k =
- Logic_environment.add_let_quantif_binding logic_env k k_iv
+ Logic_env.add_let_quantif_binding logic_env k k_iv
in
- let lambda_iv = infer ~logic_env:logic_env_with_k lambda in
+ let lambda_iv = infer ~force ~logic_env:logic_env_with_k lambda in
Error.map3 (infer_sum_product li.l_var_info) lambda_iv t1_iv t2_iv
| _ -> Error.not_yet "extended quantifiers without lambda term")
| LBnone
| LBreads _ ->
List.iter
- (fun arg -> ignore (infer ~logic_env arg))
+ (fun arg -> ignore (infer ~force ~logic_env arg))
args;
(match li.l_type with
| None -> assert false
@@ -962,8 +952,8 @@ let rec infer ?(force_infer=false) ~logic_env t =
| Tinter _ -> Error.not_yet "tset intersection"
| Tcomprehension (_,_,_) -> Error.not_yet "tset comprehension"
| Trange(Some n1, Some n2) ->
- let i1 = infer ~logic_env n1 in
- let i2 = infer ~logic_env n2 in
+ let i1 = infer ~force ~logic_env n1 in
+ let i2 = infer ~force ~logic_env n2 in
Error.map2 join i1 i2
| Trange(None, _) | Trange(_, None) ->
Options.abort "unbounded ranges are not part of E-ACSl"
@@ -971,41 +961,41 @@ let rec infer ?(force_infer=false) ~logic_env t =
| Tlet (li,t) ->
let li_t = Misc.term_of_li li in
let li_v = li.l_var_info in
- let i1 = infer ~logic_env li_t in
+ let i1 = infer ~force ~logic_env li_t in
let logic_env =
- Error.map (Logic_environment.add_let_quantif_binding logic_env li_v) i1
+ Error.map (Logic_env.add_let_quantif_binding logic_env li_v) i1
in
- get_res (infer ~logic_env t)
+ get_res (infer ~force ~logic_env t)
| TConst (LReal lr) ->
if lr.r_lower = lr.r_upper then Float(FDouble, Some lr.r_nearest)
else Rational
| Tlambda ([ _ ],lt) ->
- get_res (infer ~logic_env lt)
+ get_res (infer ~force ~logic_env lt)
| TStartOf lv
| TAddrOf lv ->
- ignore (infer_term_lval ~logic_env lv);
+ ignore (infer_term_lval ~force ~logic_env lv);
Nan
| TBinOp (PlusPI, t1 ,t2)
| TBinOp (MinusPI, t1, t2) ->
- ignore(infer ~logic_env t1);
- ignore(infer ~logic_env t2);
+ ignore (infer ~force ~logic_env t1);
+ ignore (infer ~force ~logic_env t2);
Nan
| Tbase_addr (_,t)
| Ttypeof t ->
- ignore(infer ~logic_env t);
+ ignore (infer ~force ~logic_env t);
Nan
|TDataCons(_,l) ->
- List.iter (fun t -> ignore (infer ~logic_env t)) l;
+ List.iter (fun t -> ignore (infer ~force ~logic_env t)) l;
Nan
| TUpdate(t1, toff, t2) ->
- ignore (infer ~logic_env t1);
- ignore (infer ~logic_env t2);
- infer_term_offset ~logic_env toff;
+ ignore (infer ~force ~logic_env t1);
+ ignore (infer ~force ~logic_env t2);
+ infer_term_offset ~force ~logic_env toff;
Nan
| Tlambda (_,_)
@@ -1013,25 +1003,26 @@ let rec infer ?(force_infer=false) ~logic_env t =
| Ttype _
| Tempty_set ->
Nan
- in Memo.memo
- ~force_infer
- ~profile:(Logic_environment.get_profile logic_env)
+ in
+ Memo.memo
+ ~force_infer:force
+ (Logic_env.get_profile logic_env)
compute
t
-and infer_term_lval ~logic_env (host, offset as tlv) =
+and infer_term_lval ~force ~logic_env (host, offset as tlv) =
match offset with
- | TNoOffset -> infer_term_host ~logic_env host
+ | TNoOffset -> infer_term_host ~force ~logic_env host
| _ ->
- ignore(infer_term_host ~logic_env host);
- infer_term_offset ~logic_env offset;
+ ignore (infer_term_host ~force ~logic_env host);
+ infer_term_offset ~force ~logic_env offset;
let ty = Logic_utils.logicCType (Cil.typeOfTermLval tlv) in
interv_of_typ ty
-and infer_term_host ~logic_env thost =
+and infer_term_host ~force ~logic_env thost =
match thost with
| TVar v ->
- (try Logic_environment.find logic_env v with Not_found ->
+ (try Logic_env.find logic_env v with Not_found ->
match v.lv_type with
| Linteger -> top_ival
| Ctype (TFloat(fk, _)) -> Float(fk, None)
@@ -1041,7 +1032,7 @@ and infer_term_host ~logic_env thost =
| TResult ty ->
interv_of_typ ty
| TMem t ->
- ignore(infer ~logic_env t);
+ ignore (infer ~force ~logic_env t);
let ty = Logic_utils.logicCType t.term_type in
match Cil.unrollType ty with
| TPtr(ty, _) | TArray(ty, _, _) ->
@@ -1052,14 +1043,14 @@ and infer_term_host ~logic_env thost =
Printer.pp_term t
-and infer_term_offset ~logic_env t =
+and infer_term_offset ~force ~logic_env t =
match t with
| TNoOffset -> ()
| TField(_, toff)
- | TModel(_, toff) -> infer_term_offset ~logic_env toff
+ | TModel(_, toff) -> infer_term_offset ~force ~logic_env toff
| TIndex(t, toff) ->
- ignore (infer ~logic_env t);
- infer_term_offset ~logic_env toff
+ ignore (infer ~force ~logic_env t);
+ infer_term_offset ~force ~logic_env toff
(* [type_bound_variables] infers an interval associated with each of
the provided bounds of a quantified variable, and provides a term
@@ -1078,8 +1069,8 @@ and infer_term_offset ~logic_env t =
Return: R with a guard guaranteeing that [lv] does not overflow *)
and infer_bound_variable ~loc ~logic_env (t1, lv, t2) =
let get_res = Error.map (fun x -> x) in
- let i1 = get_res (infer ~logic_env t1) in
- let i2 = get_res (infer ~logic_env t2) in
+ let i1 = get_res (infer ~force:false ~logic_env t1) in
+ let i2 = get_res (infer ~force:false ~logic_env t2) in
let i = widen (join i1 i2) in
let t1, t2, i =
match lv.lv_type with
@@ -1115,9 +1106,9 @@ and infer_bound_variable ~loc ~logic_env (t1, lv, t2) =
Bound_variables.add_guard_for_small_type lv guard;
t1, t2, i
in
- ignore (infer ~logic_env t1);
- ignore (infer ~logic_env t2);
- Logic_environment.add_let_quantif_binding logic_env lv i, (t1, lv, t2)
+ ignore (infer ~force:false ~logic_env t1);
+ ignore (infer ~force:false ~logic_env t2);
+ Logic_env.add_let_quantif_binding logic_env lv i, (t1, lv, t2)
and infer_predicate ~logic_env p =
let get_res = Error.map (fun x -> x) in
@@ -1129,10 +1120,10 @@ and infer_predicate ~logic_env p =
| LBpred p ->
let args_ival =
List.map
- (fun arg -> get_res (infer ~logic_env arg))
+ (fun arg -> get_res (infer ~force:false ~logic_env arg))
args
in
- let logic_env = Logic_environment.create li.l_profile args_ival in
+ let logic_env = Logic_env.make li.l_profile args_ival in
ignore (infer_predicate ~logic_env p)
| LBnone -> ()
| LBreads _ -> ()
@@ -1143,8 +1134,8 @@ and infer_predicate ~logic_env p =
)
| Pdangling _ -> ()
| Prel(_, t1, t2) ->
- ignore (infer ~logic_env t1);
- ignore (infer ~logic_env t2)
+ ignore (infer ~force:false ~logic_env t1);
+ ignore (infer ~force:false ~logic_env t2)
| Pand(p1, p2)
| Por(p1, p2)
| Pxor(p1, p2)
@@ -1155,17 +1146,17 @@ and infer_predicate ~logic_env p =
| Pnot p ->
infer_predicate ~logic_env p;
| Pif(t, p1, p2) ->
- ignore (infer ~logic_env t);
+ ignore (infer ~force:false ~logic_env t);
infer_predicate ~logic_env p1;
infer_predicate ~logic_env p2
| Plet(li, p) ->
let li_t = Misc.term_of_li li in
let li_v = li.l_var_info in
- let i = infer ~logic_env li_t in
+ let i = infer ~force:false ~logic_env li_t in
let logic_env =
- Error.map (Logic_environment.add_let_quantif_binding logic_env li_v) i
+ Error.map (Logic_env.add_let_quantif_binding logic_env li_v) i
in
- (infer_predicate ~logic_env p)
+ infer_predicate ~logic_env p
| Pforall _
| Pexists _ ->
let guards, goal =
@@ -1176,7 +1167,8 @@ and infer_predicate ~logic_env p =
Printer.pp_predicate
in
let loc = p.pred_loc in
- let rec do_analysis guards new_guards logic_env = match guards with
+ let rec do_analysis guards new_guards logic_env =
+ match guards with
| [] -> logic_env, new_guards
| guard :: guards ->
let logic_env, new_guard =
@@ -1189,7 +1181,7 @@ and infer_predicate ~logic_env p =
infer_predicate ~logic_env goal
| Pseparated tlist ->
List.iter
- (fun t -> ignore (infer ~logic_env t))
+ (fun t -> ignore (infer ~force:false ~logic_env t))
tlist;
| Pinitialized(_, t)
| Pfreeable(_, t)
@@ -1198,7 +1190,7 @@ and infer_predicate ~logic_env p =
| Pvalid_read(_, t)
| Pobject_pointer(_,t)
| Pvalid_function t ->
- ignore (infer ~logic_env t);
+ ignore (infer ~force:false ~logic_env t);
| Pat(p, _) -> infer_predicate ~logic_env p
| Pfresh _ -> Error.not_yet "\\fresh"
@@ -1218,14 +1210,13 @@ let typer_visitor ~logic_env = object
(* Do not raise a warning for e-acsl errors at preprocessing time,
those errrors are stored in the table and warnings are raised at
translation time *)
- let _ = try infer_predicate ~logic_env p
- with Error.Not_yet _ | Error.Typing_error _ -> ()
- in
+ (try infer_predicate ~logic_env p
+ with Error.Not_yet _ | Error.Typing_error _ -> ());
Cil.SkipChildren
end
let infer_program ast =
- let visitor = typer_visitor ~logic_env:(Logic_environment.create [] []) in
+ let visitor = typer_visitor ~logic_env:(Logic_env.make [] []) in
visitor#visit_file ast
let preprocess_predicate ~logic_env p =
@@ -1237,27 +1228,26 @@ let preprocess_code_annot ~logic_env annot =
ignore @@ visitor#visit_code_annot annot
let preprocess_term ~logic_env t =
- ignore (infer ~logic_env t)
+ ignore (infer ~force:false ~logic_env t)
-let get_p ~profile t =
+let get_from_profile ~profile t =
let t = Logic_normalizer.get_term t in
Error.retrieve_preprocessing
"Interval inference"
- (Memo.get ~profile)
+ (Memo.get profile)
t
Printer.pp_term
let get ~logic_env =
- get_p ~profile:(Logic_environment.get_profile logic_env)
+ get_from_profile ~profile:(Logic_env.get_profile logic_env)
-let get_widened_profile = Memo.get_widened_profile
+let get_widened_profile = Widened_profile.get
let clear () =
Memo.clear();
+ Widened_profile.clear();
LF_env.clear()
-type profile = Profile.t
-
(*
Local Variables:
compile-command: "make -C ../../../../.."
diff --git a/src/plugins/e-acsl/src/analyses/interval.mli b/src/plugins/e-acsl/src/analyses/interval.mli
index e48971fa400c3ddb8d77aca07a7d83f7ca4aa496..3cd608d064774d5f96345cacc17df1c61bf6d3bd 100644
--- a/src/plugins/e-acsl/src/analyses/interval.mli
+++ b/src/plugins/e-acsl/src/analyses/interval.mli
@@ -89,39 +89,48 @@ val extended_interv_of_typ: Cil_types.typ -> t
@raise Not_a_number if the given type does not represent any number. *)
val plus_one : ival -> ival
+(** @return the result of adding one to an interval. This is because when we
+ have a condition [x<t], we need to generate [t+1] *)
(* ************************************************************************** *)
(** {3 Environment for interval computations} *)
(* ************************************************************************** *)
+(** profile which maps logic variables that are function parameters to their
+ interval depending on the arguments at the callsite of the function *)
module Profile:
Datatype.S_with_collections with type t = ival list
-type profile = Profile.t
-
-module Logic_environment: sig
+(** logic environment which maps logic variables to their interval. It is
+ composed of:
+ - a profile for bindings of function arguments
+ - additional bindings for let and quantification binds *)
+module Logic_env: sig
type t
- val create: Cil_types.logic_var list -> ival list -> t
+ (* make a new environment with no bindings for let and quantifications, and
+ a profile, to be called at a function callsite. The two lists are assumed
+ to have the same length *)
+ val make: Cil_types.logic_var list -> ival list -> t
val add_let_quantif_binding: t -> Cil_types.logic_var -> ival -> t
- val get_profile: t -> profile
+ val get_profile: t -> Profile.t
end
(* ************************************************************************** *)
(** {3 Inference system} *)
(* ************************************************************************** *)
+(* The inference phase infers the smallest possible integer interval which the
+ values of the term can fit in. *)
-(* val infer: Logic_environment.t -> Cil_types.term -> t *)
-(* [infer t] infers the smallest possible integer interval which the values
- of the term can fit in.
+val get_from_profile: profile:Profile.t -> Cil_types.term -> t
+(** @return the value computed by the interval inference phase
@raise Is_a_real if the term is either a float or a real.
- @raise Not_a_number if the term does not represent any number. *)
-
-val get_p: profile:Profile.t -> Cil_types.term -> t
-(** @return the value computed by the interval inference phase *)
+ @raise Not_a_number if the term does not represent any
+ number.*)
-val get: logic_env:Logic_environment.t -> Cil_types.term -> t
-(** @return the value computed by the interval inference phase, same as [get]
- but with a full-fledged logic environment instead of a function profile *)
+val get: logic_env:Logic_env.t -> Cil_types.term -> t
+(** @return the value computed by the interval inference phase, same as
+ [get_from_profile] but with a full-fledged logic environment instead of a
+ function profile *)
(*****************************************************************************)
@@ -133,17 +142,17 @@ val infer_program : Cil_types.file -> unit
in a program *)
val preprocess_predicate :
- logic_env:Logic_environment.t -> Cil_types.predicate -> unit
+ logic_env:Logic_env.t -> Cil_types.predicate -> unit
(** compute and store the type of all the terms in a code annotation *)
val preprocess_code_annot :
- logic_env:Logic_environment.t -> Cil_types.code_annotation -> unit
+ logic_env:Logic_env.t -> Cil_types.code_annotation -> unit
(** compute and store the type of all the terms in a code annotation *)
val preprocess_term :
- logic_env:Logic_environment.t -> Cil_types.term -> unit
+ logic_env:Logic_env.t -> Cil_types.term -> unit
-val get_widened_profile : profile -> Cil_types.term -> profile
+val get_widened_profile : Profile.t -> Cil_types.term -> Profile.t
val clear : unit -> unit
diff --git a/src/plugins/e-acsl/src/analyses/memory_tracking.ml b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
index cdc91675c2118fa80c2f13657bb20d3a7ba73369..96b6b3ae3c3784ecaa79f0bc2448f9bd71ce4f64 100644
--- a/src/plugins/e-acsl/src/analyses/memory_tracking.ml
+++ b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
@@ -493,7 +493,7 @@ module rec Transfer
in
if stmt.ghost then
let rtes = Rte.stmt kf stmt in
- let logic_env = Interval.Logic_environment.create [] [] in
+ let logic_env = Interval.Logic_env.make [] [] in
List.iter (Typing.preprocess_rte ~logic_env) rtes;
List.fold_left
(fun state a -> register_code_annot kf a state) state rtes
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index 532ea8c1b6663827c161464b21ede47c38a671a1..e7f4c04262e42fa8da45e2e8101850aff5d9222b 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -193,7 +193,7 @@ module Memo: sig
(term -> computed_info) ->
term ->
computed_info Error.result
- val get: profile:Interval.profile -> term -> computed_info Error.result
+ val get: profile:Interval.Profile.t -> term -> computed_info Error.result
val clear: unit -> unit
end = struct
@@ -277,6 +277,15 @@ end
(** {2 Coercion rules} *)
(******************************************************************************)
+let assert_nan = function
+ | Nan -> ()
+ | C_integer _
+ | C_float _
+ | Gmpz
+ | Rational
+ | Real -> Options.abort "got a number type where NaN was expected"
+
+
(* 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 ?ctx ?(use_gmp_opt = false) = function
@@ -332,7 +341,7 @@ let number_ty_of_typ ~post ty =
| TVoid _ | TPtr _ | TArray _ | TFun _ | TComp _ | TBuiltin_va_list _ -> Nan
| TNamed _ -> assert false
-let ty_of_logic_ty ?term ?profile lty =
+let ty_of_logic_ty ?term ~profile lty =
let get_ty = function
| Linteger -> Gmpz
| Ctype ty -> number_ty_of_typ ~post:false ty
@@ -344,13 +353,9 @@ let ty_of_logic_ty ?term ?profile lty =
match term with
| None -> get_ty lty
| Some t ->
- let profile = match profile with
- | None -> assert false
- | Some profile -> profile
- in
if Options.Gmp_only.get () && lty = Linteger then Gmpz
else
- let i = Interval.get_p ~profile t in
+ let i = Interval.get_from_profile ~profile t in
ty_of_interv i
(******************************************************************************)
@@ -372,7 +377,7 @@ let mk_ctx ~use_gmp_opt = function
In that case, it cannot be a GMP, so it must be coerced to an integral type
in that case *)
let type_offset ~profile t =
- let i = Interval.get_p ~profile t in
+ let i = Interval.get_from_profile ~profile t in
match ty_of_interv i with
| Gmpz -> C_integer ILongLong (* largest possible type *)
| ty -> ty
@@ -410,14 +415,14 @@ let rec type_term
| TSizeOf _
| TSizeOfStr _
| TAlignOf _ ->
- let i = Interval.get_p ~profile t in
+ let i = Interval.get_from_profile ~profile t in
(* a constant or a left value directly under a lambda should be a gmp
if the infered context for the lambda is gmp *)
let ty = ty_of_interv ?ctx ~use_gmp_opt:under_lambda i in
dup ty
| TLval tlv ->
- let i = Interval.get_p ~profile t in
+ let i = Interval.get_from_profile ~profile t in
let ty = ty_of_interv ?ctx ~use_gmp_opt:under_lambda i in
type_term_lval ~profile tlv;
(* Options.feedback "Type : %a" D.pretty ty; *)
@@ -427,14 +432,14 @@ let rec type_term
| Tblock_length(_, t')
| TSizeOfE t'
| TAlignOfE t' ->
- let i = Interval.get_p ~profile t in
+ let i = Interval.get_from_profile ~profile t in
(* [t'] must be typed, but it is a pointer *)
ignore (type_term ~use_gmp_opt:true ~ctx:Nan ~profile t');
let ty = ty_of_interv ?ctx i in
dup ty
| TBinOp (MinusPP, t1, t2) ->
- let i = Interval.get_p ~profile t in
+ let i = Interval.get_from_profile ~profile t in
(* [t1] and [t2] must be typed, but they are pointers *)
ignore (type_term ~use_gmp_opt:true ~ctx:Nan ~profile t1);
ignore (type_term ~use_gmp_opt:true ~ctx:Nan ~profile t2);
@@ -442,8 +447,8 @@ let rec type_term
dup ty
| TUnOp (unop, t') ->
- let i = Interval.get_p ~profile t in
- let i' = Interval.get_p ~profile t' in
+ let i = Interval.get_from_profile ~profile t in
+ let i' = Interval.get_from_profile ~profile t' in
let ctx_res, ctx = compute_ctx ?ctx (Interval.join i i') in
ignore (type_term ~use_gmp_opt:true ~arith_operand:true ~ctx ~profile t');
(match unop with
@@ -453,9 +458,9 @@ let rec type_term
| TBinOp ((PlusA | MinusA | Mult | Div | Mod | Shiftlt | Shiftrt | BAnd
| BOr | BXor), t1, t2)
->
- let i = Interval.get_p ~profile t in
- let i1 = Interval.get_p ~profile t1 in
- let i2 = Interval.get_p ~profile t2 in
+ let i = Interval.get_from_profile ~profile t in
+ let i1 = Interval.get_from_profile ~profile t1 in
+ let i2 = Interval.get_from_profile ~profile t2 in
let ctx_res, ctx =
compute_ctx ?ctx (Interval.join i (Interval.join i1 i2))
in
@@ -476,8 +481,8 @@ let rec type_term
| TBinOp ((Lt | Gt | Le | Ge | Eq | Ne), t1, t2) ->
assert (match ctx with None -> true | Some c -> D.compare c c_int >= 0);
- let i1 = Interval.get_p ~profile t1 in
- let i2 = Interval.get_p ~profile t2 in
+ let i1 = Interval.get_from_profile ~profile t1 in
+ let i2 = Interval.get_from_profile ~profile t2 in
let ctx =
mk_ctx ~use_gmp_opt:true (ty_of_interv ?ctx (Interval.join i1 i2))
in
@@ -490,8 +495,8 @@ let rec type_term
c_int, ty
| TBinOp ((LAnd | LOr), t1, t2) ->
- let i1 = Interval.get_p ~profile t1 in
- let i2 = Interval.get_p ~profile t2 in
+ let i1 = Interval.get_from_profile ~profile t1 in
+ let i2 = Interval.get_from_profile ~profile t2 in
let ty = ty_of_interv ?ctx (Interval.join i1 i2) in
(* both operands fit in an int. *)
ignore (type_term ~use_gmp_opt:true ~ctx:c_int ~profile t1);
@@ -500,7 +505,7 @@ let rec type_term
| TCastE(_, t') ->
(* compute the smallest interval from the whole term [t] *)
- let i = Interval.get_p ~profile t in
+ let i = Interval.get_from_profile ~profile t in
(* nothing more to do: [i] is already more precise than what we could
infer from the arguments of the cast. *)
let ctx = ty_of_interv ?ctx i in
@@ -512,9 +517,9 @@ let rec type_term
mk_ctx ~use_gmp_opt:false c_int (* an int must be generated *)
in
ignore (type_term ~use_gmp_opt:false ~ctx:ctx1 ~profile t1);
- let i = Interval.get_p ~profile t in
- let i2 = Interval.get_p ~profile t2 in
- let i3 = Interval.get_p ~profile t3 in
+ let i = Interval.get_from_profile ~profile t in
+ let i2 = Interval.get_from_profile ~profile t2 in
+ let i3 = Interval.get_from_profile ~profile t3 in
let ctx = ty_of_interv ?ctx (Interval.join i (Interval.join i2 i3)) in
let ctx = mk_ctx ~use_gmp_opt:true ctx in
ignore (type_term ~use_gmp_opt:true ~ctx ~profile t2);
@@ -548,13 +553,13 @@ let rec type_term
let typ_arg lvi arg =
(* a built-in is a C function, so the context is necessarily a C
type. *)
- let ctx = ty_of_logic_ty lvi.lv_type in
+ let ctx = ty_of_logic_ty ~profile lvi.lv_type in
ignore (type_term ~use_gmp_opt:false ~ctx ~profile arg)
in
List.iter2 typ_arg li.l_profile args;
(* [li.l_type is [None] for predicate only: not possible here.
Thus using [Option.get] is fine *)
- dup (ty_of_logic_ty (Option.get li.l_type))
+ dup (ty_of_logic_ty ~profile (Option.get li.l_type))
else begin
(* TODO: what if the type of the parameter is smaller than the infered
type of the argument? For now, it is silently ignored (both
@@ -586,7 +591,7 @@ let rec type_term
?ctx
~profile x))
args;
- let new_profile = List.map (Interval.get_p ~profile) args in
+ let new_profile = List.map (Interval.get_from_profile ~profile) args in
Stack.push
(fun () ->
ignore (type_predicate ~profile:new_profile p))
@@ -615,7 +620,7 @@ let rec type_term
?ctx
~profile x))
args;
- let new_profile = List.map (Interval.get_p ~profile) args in
+ let new_profile = List.map (Interval.get_from_profile ~profile) args in
let new_profile = Interval.get_widened_profile new_profile t_body in
let gmp,ctx_body = match li.l_type with
| Some (Ctype typ) ->
@@ -625,35 +630,33 @@ let rec type_term
in
Stack.push
(fun () ->
- ignore (type_term
- ~use_gmp_opt:false
- ~under_lambda:true
- ~arith_operand
- ?ctx:ctx_body
- ~profile:new_profile
- t_body))
+ ignore
+ (type_term
+ ~use_gmp_opt:false
+ ~under_lambda:true
+ ~arith_operand
+ ?ctx:ctx_body
+ ~profile:new_profile
+ t_body))
pending_typing;
dup (ty_of_interv
?ctx:ctx_body
~use_gmp_opt:(gmp && use_gmp_opt)
- (Interval.get_p ~profile t))
+ (Interval.get_from_profile ~profile t))
| LBnone ->
(match args with
| [ t1; t2; {term_node = Tlambda([ _ ], _)} as lambda ] ->
- let ty_bound = Interval.(plus_one (get_p ~profile t2)) in
- let ty_bound =
- ty_of_interv (Interval.join ty_bound (Interval.get_p ~profile t1))
- in
+ let range = Interval.(plus_one (get_from_profile ~profile t2)) in
+ let range = Interval.(join range (get_from_profile ~profile t1)) in
+ let range = ty_of_interv range in
ignore
(type_term
- ~use_gmp_opt:true ~arith_operand:true ~ctx:ty_bound ~profile t1);
+ ~use_gmp_opt:true ~arith_operand:true ~ctx:range ~profile t1);
ignore
(type_term
- ~use_gmp_opt:true ~arith_operand:true ~ctx:ty_bound ~profile t2);
- let ty =
- ty_of_interv (Interval.get_p ~profile t) ~use_gmp_opt:true ?ctx
- in
- (* Options.feedback "type of extended quantifier: %a" D.pretty ty; *)
+ ~use_gmp_opt:true ~arith_operand:true ~ctx:range ~profile t2);
+ let ival = Interval.get_from_profile ~profile t in
+ let ty = ty_of_interv ival ~use_gmp_opt:true ?ctx in
ignore (type_term ~use_gmp_opt:true ?ctx ~profile lambda);
dup ty
| [ ] | [ _ ] | [ _; _ ] | _ :: _ :: _ :: _ ->
@@ -678,7 +681,7 @@ let rec type_term
| Trange(Some n1, Some n2) ->
ignore (type_term ~use_gmp_opt ~profile n1);
ignore (type_term ~use_gmp_opt ~profile n2);
- let i = Interval.get_p ~profile t in
+ let i = Interval.get_from_profile ~profile t in
let ty = ty_of_interv ?ctx i in
dup ty
@@ -719,7 +722,8 @@ and type_term_lhost ~profile t = match t with
| TVar _
| TResult _ -> ()
| TMem t ->
- ignore (type_term ~use_gmp_opt:false ~ctx:Nan ~profile t)
+ let computed_ty = type_term ~use_gmp_opt:false ~ctx:Nan ~profile t
+ in assert_nan computed_ty.ty
and type_term_offset ~profile t = match t with
| TNoOffset -> ()
@@ -731,8 +735,8 @@ and type_term_offset ~profile t = match t with
type_term_offset ~profile toff
and number_ty_bound_variable ~profile (t1, lv, t2) =
- let i1 = Interval.get_p ~profile t1 in
- let i2 = Interval.get_p ~profile t2 in
+ let i1 = Interval.get_from_profile ~profile t1 in
+ let i2 = Interval.get_from_profile ~profile t2 in
let i = Interval.(widen (join i1 i2)) in
match lv.lv_type with
| Linteger ->
@@ -752,7 +756,7 @@ and number_ty_bound_variable ~profile (t1, lv, t2) =
Printer.pp_logic_var lv
and type_bound_variables ~profile (t1, lv, t2) =
- let ctx= number_ty_bound_variable ~profile (t1, lv, t2) in
+ let ctx = number_ty_bound_variable ~profile (t1, lv, t2) in
(* forcing when typing bounds prevents to generate an extra useless
GMP variable when --e-acsl-gmp-only *)
ignore(type_term ~use_gmp_opt:false ~ctx ~profile t1);
@@ -770,10 +774,9 @@ and type_predicate ~profile p =
match li.l_body with
| LBpred p ->
List.iter
- (fun x -> ignore
- (type_term ~use_gmp_opt: true ~profile x))
+ (fun x -> ignore (type_term ~use_gmp_opt: true ~profile x))
args;
- let new_profile = List.map (Interval.get_p ~profile) args in
+ let new_profile = List.map (Interval.get_from_profile ~profile) args in
ignore (type_predicate ~profile:new_profile p);
| LBnone -> ()
| LBreads _ -> ()
@@ -785,8 +788,8 @@ and type_predicate ~profile p =
c_int
| Pdangling _ -> Error.not_yet "\\dangling"
| Prel(_, t1, t2) ->
- let i1 = Interval.get_p ~profile t1 in
- let i2 = Interval.get_p ~profile t2 in
+ let i1 = Interval.get_from_profile ~profile t1 in
+ let i2 = Interval.get_from_profile ~profile t2 in
let i = Interval.join i1 i2 in
let ctx = mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx:c_int i) in
ignore (type_term ~use_gmp_opt:true ~ctx ~profile t1);
@@ -826,8 +829,7 @@ and type_predicate ~profile p =
Printer.pp_predicate
in
List.iter
- (fun (t1, x, t2) ->
- type_bound_variables ~profile (t1, x, t2))
+ (fun (t1, x, t2) -> type_bound_variables ~profile (t1, x, t2))
guards;
(type_predicate ~profile goal).ty
end
@@ -867,7 +869,7 @@ let type_named_predicate ~profile p =
done
let unsafe_set t ?ctx ~logic_env ty =
- let profile = Interval.Logic_environment.get_profile logic_env in
+ let profile = Interval.Logic_env.get_profile logic_env in
let ctx = match ctx with None -> ty | Some ctx -> ctx in
let mk _ = coerce ~arith_operand:false ~ctx ~op:ty ty in
ignore (Memo.memo mk ~profile t)
@@ -877,15 +879,15 @@ let unsafe_set t ?ctx ~logic_env ty =
(******************************************************************************)
let get_number_ty ~logic_env t =
- let profile = Interval.Logic_environment.get_profile logic_env in
+ let profile = Interval.Logic_env.get_profile logic_env in
(Error.retrieve_preprocessing "typing" (Memo.get ~profile) t Printer.pp_term).ty
let get_integer_op ~logic_env t =
- let profile = Interval.Logic_environment.get_profile logic_env in
+ let profile = Interval.Logic_env.get_profile logic_env in
(Error.retrieve_preprocessing "typing" (Memo.get ~profile) t Printer.pp_term).op
let get_integer_op_of_predicate ~logic_env p =
- let profile = Interval.Logic_environment.get_profile logic_env in
+ let profile = Interval.Logic_env.get_profile logic_env in
(type_predicate ~profile p).op
(* {!typ_of_integer}, but handle the not-integer cases. *)
@@ -901,26 +903,26 @@ let extract_typ t ty =
| Larrow _ -> Error.not_yet "unsupported logic type: type arrow"
let get_typ ~logic_env t =
- let profile = Interval.Logic_environment.get_profile logic_env in
+ let profile = Interval.Logic_env.get_profile logic_env in
let info =
Error.retrieve_preprocessing "typing" (Memo.get ~profile) t Printer.pp_term in
extract_typ t info.ty
let get_op ~logic_env t =
- let profile = Interval.Logic_environment.get_profile logic_env in
+ let profile = Interval.Logic_env.get_profile logic_env in
let info =
Error.retrieve_preprocessing "typing" (Memo.get ~profile) t Printer.pp_term in
extract_typ t info.op
let get_cast ~logic_env t =
- let profile = Interval.Logic_environment.get_profile logic_env in
+ let profile = Interval.Logic_env.get_profile logic_env in
let info =
Error.retrieve_preprocessing "typing" (Memo.get ~profile) t Printer.pp_term in
try Option.map typ_of_number_ty info.cast
with Not_a_number -> None
let get_cast_of_predicate ~logic_env p =
- let profile = Interval.Logic_environment.get_profile logic_env in
+ let profile = Interval.Logic_env.get_profile logic_env in
let info = type_predicate ~profile p in
try Option.map typ_of_number_ty info.cast
with Not_a_number -> assert false
@@ -955,7 +957,7 @@ let preprocess_predicate ~logic_env p =
Logic_normalizer.preprocess_predicate p;
Bound_variables.preprocess_predicate p;
Interval.preprocess_predicate ~logic_env p;
- let profile = Interval.Logic_environment.get_profile logic_env in
+ let profile = Interval.Logic_env.get_profile logic_env in
let visitor = typing_visitor profile in
ignore @@ visitor#visit_predicate p
@@ -963,12 +965,12 @@ let preprocess_rte ~logic_env rte =
Logic_normalizer.preprocess_annot rte;
Bound_variables.preprocess_annot rte;
ignore (Interval.preprocess_code_annot ~logic_env rte);
- let profile = Interval.Logic_environment.get_profile logic_env in
+ let profile = Interval.Logic_env.get_profile logic_env in
type_code_annot profile rte
let preprocess_term ~use_gmp_opt ?ctx ~logic_env t =
ignore (Interval.preprocess_term ~logic_env t);
- let profile = Interval.Logic_environment.get_profile logic_env in
+ let profile = Interval.Logic_env.get_profile logic_env in
ignore (type_term ~use_gmp_opt ?ctx ~profile t);
(*
diff --git a/src/plugins/e-acsl/src/analyses/typing.mli b/src/plugins/e-acsl/src/analyses/typing.mli
index 67dce8431e25332de8c7fe0dbdf54c6ea823648e..2a256562d4b5bcdfbd629dfe0230cc8820b75eb1 100644
--- a/src/plugins/e-acsl/src/analyses/typing.mli
+++ b/src/plugins/e-acsl/src/analyses/typing.mli
@@ -60,9 +60,6 @@ type number_ty = private
| Real
| Nan
-(* module Function_params_ty: *)
-(* Datatype.S_with_collections with type t = number_ty list *)
-
(** {3 Smart constructors} *)
val c_int: number_ty
@@ -94,27 +91,12 @@ val join: number_ty -> number_ty -> number_ty
the other argument is also {!Other}. In this case, the result is [Other]. *)
val number_ty_bound_variable:
- profile:Interval.profile ->
- term * logic_var * term ->
- number_ty
+ profile:Interval.Profile.t -> term * logic_var * term -> number_ty
+(** return the type of a quantified logic variable *)
(******************************************************************************)
(** {2 Typing} *)
(******************************************************************************)
-
-(* val type_term: *)
-(* use_gmp_opt:bool -> *)
-(* ?ctx:number_ty -> *)
-(* ?profile:Interval.Profile.t -> *)
-(* term -> *)
-(* unit *)
-(** Compute the type of each subterm of the given term in the given context. If
- [use_gmp_opt] is false, then the conversion to the given context is done
- even if -e-acsl-gmp-only is set. *)
-
-(* val type_named_predicate: ?profile:Interval.Profile.t -> predicate -> unit *)
-(** Compute the type of each term of the given predicate. *)
-
val clear: unit -> unit
(** Remove all the previously computed types. *)
@@ -124,36 +106,36 @@ val clear: unit -> unit
{!type_named_predicate} has been previously computed for the given term or
predicate. *)
-val get_number_ty: logic_env:Interval.Logic_environment.t -> term -> number_ty
+val get_number_ty: logic_env:Interval.Logic_env.t -> term -> number_ty
(** @return the infered type for the given term. *)
-val get_integer_op: logic_env:Interval.Logic_environment.t -> term -> number_ty
+val get_integer_op: logic_env:Interval.Logic_env.t -> term -> number_ty
(** @return the infered type for the top operation of the given term.
It is meaningless to call this function over a non-arithmetical/logical
operator. *)
val get_integer_op_of_predicate:
- logic_env:Interval.Logic_environment.t -> predicate -> number_ty
+ logic_env:Interval.Logic_env.t -> predicate -> number_ty
(** @return the infered type for the top operation of the given predicate. *)
-val get_typ: logic_env:Interval.Logic_environment.t -> term -> typ
+val get_typ: logic_env:Interval.Logic_env.t -> term -> typ
(** Get the type which the given term must be generated to. *)
-val get_op: logic_env:Interval.Logic_environment.t -> term -> typ
+val get_op: logic_env:Interval.Logic_env.t -> term -> typ
(** Get the type which the operation on top of the given term must be generated
to. *)
-val get_cast: logic_env:Interval.Logic_environment.t -> term -> typ option
+val get_cast: logic_env:Interval.Logic_env.t -> term -> typ option
(** Get the type which the given term must be converted to (if any). *)
val get_cast_of_predicate:
- logic_env:Interval.Logic_environment.t -> predicate -> typ option
+ logic_env:Interval.Logic_env.t -> predicate -> typ option
(** Like {!get_cast}, but for predicates. *)
val unsafe_set:
term ->
?ctx:number_ty ->
- logic_env:Interval.Logic_environment.t ->
+ logic_env:Interval.Logic_env.t ->
number_ty ->
unit
(** Register that the given term has the given type in the given context (if
@@ -175,13 +157,13 @@ val type_program : file -> unit
in a program *)
val preprocess_predicate :
- logic_env:Interval.Logic_environment.t ->
+ logic_env:Interval.Logic_env.t ->
predicate ->
unit
(** compute and store the types of all the terms in a given predicate *)
val preprocess_rte :
- logic_env:Interval.Logic_environment.t ->
+ logic_env:Interval.Logic_env.t ->
code_annotation ->
unit
(** compute and store the type of all the terms in a code annotation *)
@@ -189,7 +171,7 @@ val preprocess_rte :
val preprocess_term:
use_gmp_opt:bool ->
?ctx:number_ty ->
- logic_env:Interval.Logic_environment.t ->
+ logic_env:Interval.Logic_env.t ->
term ->
unit
(** Compute the type of each subterm of the given term in the given context. If
diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index ff427392a4b1cd48a2af6d0536dfc1a7da3c0d54..6303f0f94b3836181da7e4e460229a939d7ae6f4 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -77,7 +77,7 @@ type t = {
(* list of loop environment for each currently visited loops *)
cpt: int;
(* counter used when generating variables *)
- logic_env_stack: Interval.Logic_environment.t list;
+ logic_env_stack: Interval.Logic_env.t list;
(* type of variables used in calls to logic functions and predicates *)
kinstr: kinstr;
(* Current kinstr of the environment *)
@@ -112,7 +112,7 @@ let empty =
var_mapping = Logic_var.Map.empty;
loop_envs = [];
cpt = 0;
- logic_env_stack = [ Interval.Logic_environment.create [] [] ];
+ logic_env_stack = [ Interval.Logic_env.make [] [] ];
kinstr = Kglobal }
let top env = match env.env_stack with
@@ -543,32 +543,32 @@ end
module Logic_env = struct
let push_new env l_profile profile =
- {env with logic_env_stack =
- (Interval.Logic_environment.create l_profile profile) ::
- (env.logic_env_stack)}
+ let logic_env_stack =
+ Interval.Logic_env.make l_profile profile :: env.logic_env_stack
+ in
+ {env with logic_env_stack = logic_env_stack}
let add_let_quantif_binding env x ival =
match env.logic_env_stack with
| curr::_ as logic_env ->
- {env
- with logic_env_stack =
- (Interval.Logic_environment.add_let_quantif_binding curr x ival) ::
- logic_env}
- | [] -> Options.fatal
- "logic environment stack is empty"
+ let logic_env_stack =
+ Interval.Logic_env.add_let_quantif_binding curr x ival :: logic_env
+ in
+ {env with logic_env_stack = logic_env_stack}
+ | [] -> Options.fatal "logic environment stack is empty"
let get env =
match env.logic_env_stack with
| curr::_ -> curr
- | [] -> Options.fatal
- "logic environment stack is empty"
+ | [] -> Options.fatal "logic environment stack is empty"
+
+ let get_profile env =
+ Interval.Logic_env.get_profile (get env)
let pop env =
match env.logic_env_stack with
| _::stacked -> {env with logic_env_stack = stacked}
- | [] -> Options.fatal
- "logic environment stack is empty"
-
+ | [] -> Options.fatal "logic environment stack is empty"
end
diff --git a/src/plugins/e-acsl/src/code_generator/env.mli b/src/plugins/e-acsl/src/code_generator/env.mli
index 8d5aa5c00c5337f0e11761232c136d0c1f2ecfc8..c6ce8041e037db479a5c59ad507675cd523d7476 100644
--- a/src/plugins/e-acsl/src/code_generator/env.mli
+++ b/src/plugins/e-acsl/src/code_generator/env.mli
@@ -179,7 +179,8 @@ val generate_rte: t -> bool
module Logic_env: sig
val push_new: t -> logic_var list -> Interval.ival list -> t
val add_let_quantif_binding : t -> logic_var -> Interval.ival -> t
- val get: t -> Interval.Logic_environment.t
+ val get: t -> Interval.Logic_env.t
+ val get_profile : t -> Interval.Profile.t
val pop: t -> t
end
diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.ml b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
index 2ab49544212baaa8c2f1889ba3f893bdfea3127c..47857b638039cba9be0697afb836f99fcdcb3564 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -458,14 +458,8 @@ let app_to_exp ~adata ~loc ?tapp kf env ?eargs li targs =
List.fold_right2
(fun targ earg (params_ty, params_ival ,args, adata, env) ->
let logic_env = Env.Logic_env.get env in
- let param_ty =
- Typing.get_number_ty
- ~logic_env
- targ
- in
- let param_ival =
- Interval.get ~logic_env targ
- in
+ let param_ty = Typing.get_number_ty ~logic_env targ in
+ let param_ival = Interval.get ~logic_env targ in
let e, env =
try
let ty = Typing.typ_of_number_ty param_ty in
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index 7a6bb463a645ed071706fef99cabb2c1aa845281..f7f52b781ff12961f22f29fbd5abdc7aacb25ab8 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -289,7 +289,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
assert (rel1 == Rle && rel2 == Rlt);
let ctx =
Typing.number_ty_bound_variable
- ~profile:(Interval.Logic_environment.get_profile (Env.Logic_env.get env))
+ ~profile:(Env.Logic_env.get_profile env)
(t1, logic_x, t2)
in
let t_plus_one ~ty t =
diff --git a/src/plugins/e-acsl/src/code_generator/quantif.ml b/src/plugins/e-acsl/src/code_generator/quantif.ml
index 2b1f17bb74ecc3d0dd94c30fcaa3a8042d9d09fe..89d2a800aa7c815ba9b7b3b001750c848147a5f4 100644
--- a/src/plugins/e-acsl/src/code_generator/quantif.ml
+++ b/src/plugins/e-acsl/src/code_generator/quantif.ml
@@ -64,8 +64,8 @@ let rec has_empty_quantif_with_false_negative ~logic_env = function
let () =
Labels.has_empty_quantif_ref :=
- has_empty_quantif_with_false_negative
- ~logic_env:(Interval.Logic_environment.create [] [])
+ let logic_env = Interval.Logic_env.make [] [] in
+ has_empty_quantif_with_false_negative ~logic_env
(* Since we do not support logic functions with labels, we do not need to
pass an actual logic environment *)
@@ -81,11 +81,9 @@ let convert kf env loc ~is_forall quantif =
quantif
Printer.pp_predicate
in
- match (has_empty_quantif_with_false_negative
- ~logic_env:(Env.Logic_env.get env)
- bound_vars),
- is_forall
- with
+ let logic_env = Env.Logic_env.get env in
+ let empty = has_empty_quantif_with_false_negative ~logic_env bound_vars in
+ match empty, is_forall with
| true, true ->
Cil.one ~loc, env
| true, false ->
@@ -107,8 +105,8 @@ let convert kf env loc ~is_forall quantif =
let lvs = Lvs_quantif (t1, Rle, lv, Rlt, t2) in
let env = Env.Logic_scope.extend env lvs in
let logic_env = Env.Logic_env.get env in
- let env = Env.Logic_env.add_let_quantif_binding env lv
- Interval.(join (get ~logic_env t1) (get ~logic_env t2)) in
+ let i = Interval.(join (get ~logic_env t1) (get ~logic_env t2)) in
+ let env = Env.Logic_env.add_let_quantif_binding env lv i in
lvs :: lvs_guards, env)
([], env)
bound_vars
@@ -165,8 +163,8 @@ let convert kf env loc ~is_forall quantif =
end_loop.labels <- label :: end_loop.labels;
end_loop_ref := end_loop;
let env = Env.add_stmt env end_loop in
- let
- env = List.fold_left
+ let env =
+ List.fold_left
(fun env _ -> Env.Logic_env.pop env)
env
lvs_guards
diff --git a/src/plugins/e-acsl/src/code_generator/translate_ats.ml b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
index 5ce9da77b6243bc1a971465643c800e1e3495497..68e1ed5baca5a65e818a6d460c13b931f444d25a 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_ats.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
@@ -260,7 +260,7 @@ let pretranslate_to_exp ~loc kf env pot =
Options.debug ~level:4 "pre-translating %a in profile '%a'"
Pred_or_term.pretty pot
Interval.Profile.pretty
- (Interval.Logic_environment.get_profile (Env.Logic_env.get env));
+ (Env.Logic_env.get_profile env);
let e, env, t_opt =
let adata = Assert.no_data in
match pot with
@@ -300,16 +300,17 @@ let pretranslate_to_exp_with_lscope ~loc ~lscope kf env pot =
"pre-translating %a in local environment '%a' with lscope '%a'"
Pred_or_term.pretty pot
Interval.Profile.pretty
- (Interval.Logic_environment.get_profile (Env.Logic_env.get env))
+ (Env.Logic_env.get_profile env)
Lscope.D.pretty lscope;
let term_to_exp = !term_to_exp_ref in
let lscope_vars = Lscope.get_all lscope in
let lscope_vars = List.rev lscope_vars in
let rec add_lscope_to_logic_env env = function
| [] -> env
- | (Lvs_quantif(t1,_,x,_,t2)::lscope) ->
+ | Lvs_quantif(t1,_,x,_,t2)::lscope ->
let logic_env = Env.Logic_env.get env in
- let i = Interval.join
+ let i =
+ Interval.join
(Interval.get ~logic_env t1)
(Interval.get ~logic_env t2)
in
diff --git a/src/plugins/e-acsl/src/code_generator/translate_terms.ml b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
index 8611ef82c2ff07f0a16c6ff7f84874552dc269fa..63cb0e747fa2fdd5cdc4384940e555f3ee69ee8a 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_terms.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
@@ -869,7 +869,7 @@ and to_exp ~adata ?inplace kf env t =
Options.feedback ~dkey ~level:4 "translating term %a (rte? %b)in local \
environment '%a'"
Printer.pp_term t generate_rte Interval.Profile.pretty
- (Interval.Logic_environment.get_profile (Env.Logic_env.get env));
+ (Env.Logic_env.get_profile env);
let logic_env = Env.Logic_env.get env in
let t = Logic_normalizer.get_term t in
Extlib.flatten
@@ -922,7 +922,7 @@ let untyped_to_exp typ t =
| _ -> Typing.nan
in
let ctx = Option.map ctx_of_typ typ in
- let logic_env = Interval.Logic_environment.create [] [] in
+ let logic_env = Interval.Logic_env.make [] [] in
Typing.preprocess_term ~use_gmp_opt:true ~logic_env ?ctx t;
let env = Env.push Env.empty in
let env = Env.set_rte env false in
diff --git a/src/plugins/e-acsl/src/libraries/error.ml b/src/plugins/e-acsl/src/libraries/error.ml
index 4e23a5700617c12c04c759a50299d4b4a17b115f..008b0352355ed5f6b8670889f89d3cf2e3c18a50 100644
--- a/src/plugins/e-acsl/src/libraries/error.ml
+++ b/src/plugins/e-acsl/src/libraries/error.ml
@@ -136,14 +136,14 @@ module Make_with_opt(P: sig val phase:Options.category option end): S = struct
let map2 f a b =
match a,b with
| Result.Ok a, Result.Ok b -> f a b
- | Result.Ok _, Result.Error e -> raise e
+ | Result.Ok _, Result.Error e
| Result.Error e, _ -> raise e
let map3 f a b c =
match a,b,c with
| Result.Ok a, Result.Ok b, Result.Ok c -> f a b c
- | Result.Ok _, Result.Ok _, Result.Error e -> raise e
- | Result.Ok _, Result.Error e, _ -> raise e
+ | Result.Ok _, Result.Ok _, Result.Error e
+ | Result.Ok _, Result.Error e, _
| Result.Error e, _, _ -> raise e
end