From 24c29ebf106eb66a9ccd063aa8083fba7f91e56d Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@gmail.com>
Date: Fri, 21 Jan 2022 10:28:19 +0100
Subject: [PATCH] [e-acsl] linear typing for arithmetic operations
---
src/plugins/e-acsl/src/analyses/analyses.ml | 2 +
src/plugins/e-acsl/src/analyses/interval.ml | 425 +++++++++---------
src/plugins/e-acsl/src/analyses/interval.mli | 31 +-
src/plugins/e-acsl/src/analyses/typing.ml | 138 +++---
src/plugins/e-acsl/src/analyses/typing.mli | 29 +-
.../e-acsl/src/code_generator/quantif.ml | 4 +-
.../src/code_generator/translate_ats.ml | 11 +-
7 files changed, 326 insertions(+), 314 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/analyses.ml b/src/plugins/e-acsl/src/analyses/analyses.ml
index e2702e978ea..41266a7b2b3 100644
--- a/src/plugins/e-acsl/src/analyses/analyses.ml
+++ b/src/plugins/e-acsl/src/analyses/analyses.ml
@@ -29,6 +29,8 @@ let preprocess () =
Logic_normalizer.preprocess ast;
analyses_feedback "normalizing quantifiers";
Bound_variables.preprocess ast;
+ analyses_feedback "infering interval of annotations";
+ Interval.infer_program ast;
analyses_feedback "typing annotations";
Typing.type_program ast;
analyses_feedback
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index 13c92e32857..5cad1f3925a 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -25,8 +25,8 @@ open Cil_types
(* Implements Figure 3 of J. Signoles' JFLA'15 paper "Rester statique pour
devenir plus rapide, plus précis et plus mince".
Also implements a support for real numbers. *)
-
-module Error = Error.Make(struct let phase = Options.Dkey.interval end)
+let dkey = Options.Dkey.interval
+module Error = Error.Make(struct let phase = dkey end)
(* ********************************************************************* *)
(* Basic datatypes and operations *)
@@ -461,7 +461,7 @@ 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.or_error Misc.Id_term.Hashtbl.t =
+ let tbl : ival Error.result Misc.Id_term.Hashtbl.t =
Misc.Id_term.Hashtbl.create 97
(* The interval of the logic function
@@ -475,7 +475,7 @@ end = struct
once. Since we test with physical equality, the information is not needed
to determine the environment.*)
- let dep_tbl : ival Error.or_error Id_term_in_profile.Hashtbl.t
+ let dep_tbl : ival Error.result Id_term_in_profile.Hashtbl.t
= Id_term_in_profile.Hashtbl.create 97
let get_dep profile t =
@@ -518,7 +518,7 @@ end = struct
| _::_ -> memo_dep f t profile
let clear () =
- Options.feedback ~dkey ~level:4 "clearing the typing tables";
+ Options.feedback ~level:4 "clearing the typing tables";
Misc.Id_term.Hashtbl.clear tbl;
Id_term_in_profile.Hashtbl.clear dep_tbl
@@ -632,226 +632,159 @@ 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 t =
+let rec infer ~logic_env t =
let get_cty t = match t.term_type with Ctype ty -> ty | _ -> assert false in
- match t.term_node with
- | TConst (Integer (n, _)) -> singleton n
- | TConst (LChr c) ->
- let n = Cil.charConstToInt c in
- singleton n
- | TConst (LEnum enumitem) ->
- let rec find_idx n = function
- | [] -> assert false
- | ei :: l -> if ei == enumitem then n else find_idx (n + 1) l
- in
- let n = Integer.of_int (find_idx 0 enumitem.eihost.eitems) in
- singleton n
- | TLval lv -> infer_term_lval lv
- | TSizeOf ty -> infer_sizeof ty
- | TSizeOfE t -> infer_sizeof (get_cty t)
- | TSizeOfStr str -> singleton_of_int (String.length str + 1 (* '\0' *))
- | TAlignOf ty -> infer_alignof ty
- | TAlignOfE t -> infer_alignof (get_cty t)
-
- | TUnOp (Neg, t) ->
- let i = infer t in
- lift_unop Ival.neg_int i
- | TUnOp (BNot, t) ->
- let i = infer t in
- lift_unop Ival.bitwise_signed_not i
- | TUnOp (LNot, _)
- | TBinOp ((Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr), _, _) ->
- Ival Ival.zero_or_one
-
- | TBinOp (PlusA, t1, t2) ->
- let i1 = infer t1 in
- let i2 = infer t2 in
- lift_arith_binop Ival.add_int i1 i2
- | TBinOp (MinusA, t1, t2) ->
- let i1 = infer t1 in
- let i2 = infer t2 in
- lift_arith_binop Ival.sub_int i1 i2
- | TBinOp (Mult, t1, t2) ->
- let i1 = infer t1 in
- let i2 = infer t2 in
- lift_arith_binop Ival.mul i1 i2
- | TBinOp (Div, t1, t2) ->
- let i1 = infer t1 in
- let i2 = infer t2 in
- lift_arith_binop Ival.div i1 i2
- | TBinOp (Mod, t1, t2) ->
- let i1 = infer t1 in
- let i2 = infer t2 in
- lift_arith_binop Ival.c_rem i1 i2
- | TBinOp (Shiftlt, t1, t2) ->
- let i1 = infer t1 in
- let i2 = infer t2 in
- lift_arith_binop Ival.shift_left i1 i2
- | TBinOp (Shiftrt, t1, t2) ->
- let i1 = infer t1 in
- let i2 = infer t2 in
- lift_arith_binop Ival.shift_right i1 i2
- | TBinOp (BAnd, t1, t2) ->
- let i1 = infer t1 in
- let i2 = infer t2 in
- lift_arith_binop Ival.bitwise_and i1 i2
- | TBinOp (BXor, t1, t2) ->
- let i1 = infer t1 in
- let i2 = infer t2 in
- lift_arith_binop Ival.bitwise_xor i1 i2
- | TBinOp (BOr, t1, t2) ->
- let i1 = infer t1 in
- let i2 = infer t2 in
- lift_arith_binop Ival.bitwise_or i1 i2
- | TCastE (ty, t) ->
- let src = infer t in
- let dst = interv_of_typ ty in
- cast ~src ~dst
- | Tif (_, t2, t3) ->
- let i2 = infer t2 in
- let i3 = infer t3 in
- join i2 i3
- | Tat (t, _) ->
- infer t
- | TBinOp (MinusPP, t, _) ->
- (match Cil.unrollType (get_cty t) with
- | TArray(_, _, _) as ta ->
- begin
- try
- let n = Cil.bitsSizeOf ta in
- (* the second argument must be in the same block than [t].
- Consequently the result of the difference belongs to
- [0; \block_length(t)] *)
- let nb_bytes = if n mod 8 = 0 then n / 8 else n / 8 + 1 in
- ival Integer.zero (Integer.of_int nb_bytes)
- with Cil.SizeOfError _ ->
- Lazy.force interv_of_unknown_block
- end
- | TPtr _ ->
- Lazy.force interv_of_unknown_block
- | _ -> assert false)
- | Tblock_length (_, t)
- | Toffset(_, t) ->
- (match Cil.unrollType (get_cty t) with
- | TArray(_, _, _) as ta ->
- begin
- try
- let n = Cil.bitsSizeOf ta in
- let nb_bytes = if n mod 8 = 0 then n / 8 else n / 8 + 1 in
- singleton_of_int nb_bytes
- with Cil.SizeOfError _ ->
- Lazy.force interv_of_unknown_block
- end
- | TPtr _ -> Lazy.force interv_of_unknown_block
- | _ -> assert false)
- | Tnull -> singleton_of_int 0
- | TLogic_coerce (_, t) -> infer t
- | Tapp (li, lst, args) ->
- (match li.l_body with
- | LBpred _ ->
- Ival Ival.zero_or_one
- | LBterm t' ->
- let rec fixpoint i =
- let is_included, new_i =
- Logic_function_env.widen ~infer t i
- in
- if is_included then begin
- List.iter (fun lv -> Env.remove lv) li.l_profile;
- new_i
- end else
- let i = infer t' in
- List.iter (fun lv -> Env.remove lv) li.l_profile;
- fixpoint i
- in
- fixpoint bottom
- | 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 t1 in
- let t2_iv = infer t2 in
- let k_iv = join t1_iv t2_iv in
- Env.add k k_iv;
- let lambda_iv = infer lambda in
- Env.remove k;
- let t2incr =
- Logic_const.term (TBinOp(PlusA, t2, Cil.lone ())) Linteger
- in
- (* it is correct and precise to use k_ival to compute lambda_ival, but
- not during the code generation since the type used for k is the
- greatest type between the type of t1 and the type of t2+1, that is
- why the ival associated to k is updated *)
- Env.add k (join t1_iv (infer t2incr));
- (* k is removed during code generation, it is needed for generating
- the code of the lambda term *)
- infer_sum_product li.l_var_info lambda_iv t1_iv t2_iv
- | _ -> Error.not_yet "extended quantifiers without lambda term")
- | LBnone when li.l_var_info.lv_name = "\\numof" ->
- (match args with
- | [ t1; t2; { term_node = Tlambda([ k ], p) } ] ->
- let logic_info = Cil_const.make_logic_info "\\sum" in
- logic_info.l_type <- li.l_type;
- logic_info.l_tparams <- li.l_tparams;
- logic_info.l_labels <- li.l_labels;
- logic_info.l_profile <- li.l_profile;
- logic_info.l_body <- li.l_body;
- let numof_as_sum =
- let conditional_term =
- Logic_const.term
- (Tif(p, Cil.lone (), Cil.lzero ())) Linteger
- in
- let lambda_term =
- Logic_const.term (Tlambda([ k ], conditional_term)) Linteger
- in
- (Logic_const.term
- (Tapp(logic_info, lst, [ t1; t2; lambda_term ])) Linteger)
- in infer numof_as_sum
- | _ ->
- Options.fatal "unexpected input for an extended quantifier \\numof")
- | LBnone
- | LBreads _ ->
- (match li.l_type with
- | None -> assert false
- | Some ret_type -> interv_of_logic_typ ret_type)
- | LBinductive _ ->
- Error.not_yet "logic functions inductively defined")
-
- | Tunion _ -> Error.not_yet "tset union"
- | Tinter _ -> Error.not_yet "tset intersection"
- | Tcomprehension (_,_,_) -> Error.not_yet "tset comprehension"
- | Trange(Some n1, Some n2) ->
- let i1 = infer n1 in
- let i2 = infer n2 in
- join i1 i2
- | Trange(None, _) | Trange(_, None) ->
- Options.abort "unbounded ranges are not part of E-ACSl"
-
- | Tlet (li, t) ->
- let li_t = Misc.term_of_li li in
- let li_v = li.l_var_info in
- let i1 = infer li_t in
- Env.add li_v i1;
- let i2 = infer t in
- Env.remove li_v;
- i2
- | TConst (LReal lr) ->
- if lr.r_lower = lr.r_upper then Float(FDouble, Some lr.r_nearest)
- else Rational
- | Tlambda ([ _ ],lt) ->
- infer lt
- | Tlambda (_,_)
- | TConst (LStr _ | LWStr _)
- | TBinOp (PlusPI,_,_)
- | TBinOp (MinusPI,_,_)
- | TAddrOf _
- | TStartOf _
- | TDataCons (_,_)
- | Tbase_addr (_,_)
- | TUpdate (_,_,_)
- | Ttypeof _
- | Ttype _
- | Tempty_set ->
- Nan
+ let get_res = Error.map (fun x -> x) in
+ let compute t =
+ match t.term_node with
+ | TConst (Integer (n, _)) -> singleton n
+ | TConst (LChr c) ->
+ let n = Cil.charConstToInt c in
+ singleton n
+ | TConst (LEnum enumitem) ->
+ let rec find_idx n = function
+ | [] -> assert false
+ | ei :: l -> if ei == enumitem then n else find_idx (n + 1) l
+ in
+ let n = Integer.of_int (find_idx 0 enumitem.eihost.eitems) in
+ singleton n
+ | TLval lv -> infer_term_lval lv
+ | TSizeOf ty -> infer_sizeof ty
+ | TSizeOfE t -> infer_sizeof (get_cty t)
+ | TSizeOfStr str -> singleton_of_int (String.length str + 1 (* '\0' *))
+ | TAlignOf ty -> infer_alignof ty
+ | TAlignOfE t -> infer_alignof (get_cty t)
+
+ | TUnOp (Neg, t) ->
+ let i = infer ~logic_env t in
+ Error.map (lift_unop Ival.neg_int) i
+ | TUnOp (BNot, t) ->
+ let i = infer ~logic_env t in
+ Error.map (lift_unop Ival.bitwise_signed_not) i
+ | TUnOp (LNot, t) ->
+ ignore(infer ~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);
+ Ival Ival.zero_or_one
+
+ | TBinOp (PlusA, t1, t2) ->
+ let i1 = infer ~logic_env t1 in
+ let i2 = infer ~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
+ 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
+ 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
+ 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
+ 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
+ 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
+ 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
+ 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
+ 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
+ Error.map2 (lift_arith_binop Ival.bitwise_or) i1 i2
+ | TCastE (ty, t) ->
+ let src = infer ~logic_env t in
+ let dst = interv_of_typ ty in
+ Error.map (fun src -> cast ~src ~dst) src
+ | Tif (_, t2, t3) ->
+ let i2 = infer ~logic_env t2 in
+ let i3 = infer ~logic_env t3 in
+ Error.map2 join i2 i3
+ | Tat (t, _) ->
+ get_res (infer ~logic_env t)
+ | TBinOp (MinusPP, t, _) ->
+ (match Cil.unrollType (get_cty t) with
+ | TArray(_, _, _) as ta ->
+ begin
+ try
+ let n = Cil.bitsSizeOf ta in
+ (* the second argument must be in the same block than [t].
+ Consequently the result of the difference belongs to
+ [0; \block_length(t)] *)
+ let nb_bytes = if n mod 8 = 0 then n / 8 else n / 8 + 1 in
+ ival Integer.zero (Integer.of_int nb_bytes)
+ with Cil.SizeOfError _ ->
+ Lazy.force interv_of_unknown_block
+ end
+ | TPtr _ -> Lazy.force interv_of_unknown_block
+ | _ -> assert false)
+ | Tblock_length (_, t)
+ | Toffset(_, t) ->
+ (match Cil.unrollType (get_cty t) with
+ | TArray(_, _, _) as ta ->
+ begin
+ try
+ let n = Cil.bitsSizeOf ta in
+ let nb_bytes = if n mod 8 = 0 then n / 8 else n / 8 + 1 in
+ singleton_of_int nb_bytes
+ with Cil.SizeOfError _ ->
+ Lazy.force interv_of_unknown_block
+ end
+ | TPtr _ -> Lazy.force interv_of_unknown_block
+ | _ -> assert false)
+ | Tnull -> singleton_of_int 0
+ | TLogic_coerce (_, t) -> get_res (infer ~logic_env t)
+ | Tapp (_,_,_) -> assert false
+
+ | Tunion _ -> Error.not_yet "tset union"
+ | 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
+ Error.map2 join i1 i2
+ | Trange(None, _) | Trange(_, None) ->
+ Options.abort "unbounded ranges are not part of E-ACSl"
+
+ | Tlet (_,_) -> assert false
+ | 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)
+ | Tlambda (_,_)
+ | TConst (LStr _ | LWStr _)
+ | TBinOp (PlusPI,_,_)
+ | TBinOp (IndexPI,_,_)
+ | TBinOp (MinusPI,_,_)
+ | TAddrOf _
+ | TStartOf _
+ | TDataCons (_,_)
+ | Tbase_addr (_,_)
+ | TUpdate (_,_,_)
+ | Ttypeof _
+ | Ttype _
+ | Tempty_set ->
+ Nan
+ in Memo.memo ~profile:(logic_env.profile) compute t
and infer_term_lval (host, offset as tlv) =
match offset with
@@ -889,6 +822,50 @@ let infer t =
include D
+let typer_visitor ~logic_env = object
+ inherit E_acsl_visitor.visitor dkey
+
+ (* global logic functions and predicates are evaluated are callsites *)
+ method !glob_annot _ = Cil.SkipChildren
+
+ method !vterm t =
+ (* 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 ignore (infer ~logic_env t)
+ with Error.Not_yet _ | Error.Typing_error _ -> ()
+ in
+ Cil.SkipChildren
+end
+
+let infer_program ast =
+ let visitor = typer_visitor ~logic_env:(Logic_environment.create [] []) in
+ visitor#visit_file ast
+
+let preprocess_predicate ~logic_env p =
+ let visitor = typer_visitor ~logic_env in
+ ignore @@ visitor#visit_predicate p
+
+let preprocess_code_annot ~logic_env annot =
+ let visitor = typer_visitor ~logic_env in
+ ignore @@ visitor#visit_code_annot annot
+
+let preprocess_term ~logic_env t =
+ ignore (infer ~logic_env t)
+
+let get_p ~profile t =
+ let t = Logic_normalizer.get_term t in
+ Error.retrieve_preprocessing
+ "Interval inference"
+ (Memo.get ~profile)
+ t
+ Printer.pp_term
+
+let get ~logic_env =
+ get_p ~profile:(Logic_environment.get_profile logic_env)
+
+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 17faff5fc1c..98d4de40f61 100644
--- a/src/plugins/e-acsl/src/analyses/interval.mli
+++ b/src/plugins/e-acsl/src/analyses/interval.mli
@@ -109,12 +109,39 @@ end
(** {3 Inference system} *)
(* ************************************************************************** *)
-val infer: Cil_types.term -> t
-(** [infer t] infers the smallest possible integer interval which the values
+(* 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.
@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 *)
+
+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 *)
+
+
+(*****************************************************************************)
+(** {2 Interval processing} *)
+(*****************************************************************************)
+
+val infer_program : Cil_types.file -> unit
+(** compute and store the type of all the terms that will be translated
+ in a program *)
+
+val preprocess_predicate :
+ logic_env:Logic_environment.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
+(** 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
+
(*
Local Variables:
compile-command: "make -C ../../../../.."
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index d78ed712b88..4197e0974c2 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -332,7 +332,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 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,9 +344,13 @@ let ty_of_logic_ty ?term 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.infer t in
+ let i = Interval.get_p ~profile t in
ty_of_interv i
(******************************************************************************)
@@ -367,8 +371,8 @@ let mk_ctx ~use_gmp_opt = function
(* the number_ty corresponding to [t] whenever use as an offset.
In that case, it cannot be a GMP, so it must be coerced to an integral type
in that case *)
-let type_offset t =
- let i = Interval.infer t in
+let type_offset ~profile t =
+ let i = Interval.get_p ~profile t in
match ty_of_interv i with
| Gmpz -> C_integer ILongLong (* largest possible type *)
| ty -> ty
@@ -406,14 +410,14 @@ let rec type_term
| TSizeOf _
| TSizeOfStr _
| TAlignOf _ ->
- let i = Interval.infer t in
+ let i = Interval.get_p ~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.infer t in
+ let i = Interval.get_p ~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; *)
@@ -423,14 +427,14 @@ let rec type_term
| Tblock_length(_, t')
| TSizeOfE t'
| TAlignOfE t' ->
- let i = Interval.infer t in
+ let i = Interval.get_p ~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.infer t in
+ let i = Interval.get_p ~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);
@@ -438,8 +442,8 @@ let rec type_term
dup ty
| TUnOp (unop, t') ->
- let i = Interval.infer t in
- let i' = Interval.infer t' in
+ let i = Interval.get_p ~profile t in
+ let i' = Interval.get_p ~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
@@ -449,9 +453,9 @@ let rec type_term
| TBinOp ((PlusA | MinusA | Mult | Div | Mod | Shiftlt | Shiftrt | BAnd
| BOr | BXor), t1, t2)
->
- let i = Interval.infer t in
- let i1 = Interval.infer t1 in
- let i2 = Interval.infer t2 in
+ 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 ctx_res, ctx =
compute_ctx ?ctx (Interval.join i (Interval.join i1 i2))
in
@@ -472,8 +476,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.infer t1 in
- let i2 = Interval.infer t2 in
+ let i1 = Interval.get_p ~profile t1 in
+ let i2 = Interval.get_p ~profile t2 in
let ctx =
mk_ctx ~use_gmp_opt:true (ty_of_interv ?ctx (Interval.join i1 i2))
in
@@ -486,8 +490,8 @@ let rec type_term
c_int, ty
| TBinOp ((LAnd | LOr), t1, t2) ->
- let i1 = Interval.infer t1 in
- let i2 = Interval.infer t2 in
+ let i1 = Interval.get_p ~profile t1 in
+ let i2 = Interval.get_p ~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);
@@ -496,7 +500,7 @@ let rec type_term
| TCastE(_, t') ->
(* compute the smallest interval from the whole term [t] *)
- let i = Interval.infer t in
+ let i = Interval.get_p ~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
@@ -508,9 +512,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.infer t in
- let i2 = Interval.infer t2 in
- let i3 = Interval.infer t3 in
+ 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 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);
@@ -535,7 +539,7 @@ let rec type_term
| TBinOp ((PlusPI | MinusPI), t1, t2) ->
(* both [t1] and [t2] must be typed. *)
ignore (type_term ~use_gmp_opt:true ~ctx:Nan ~profile t1);
- let ctx = type_offset t2 in
+ let ctx = type_offset ~profile t2 in
ignore (type_term ~use_gmp_opt:false ~ctx ~profile t2);
dup Nan
@@ -570,8 +574,7 @@ let rec type_term
args
li.l_var_info.lv_name
in
- ignore (type_predicate ~profile:typed_args p);
- List.iter Interval.Env.remove li.l_profile)
+ ignore (type_predicate ~profile:typed_args p))
pending_typing;
dup c_int
| LBterm t_body ->
@@ -596,9 +599,7 @@ let rec type_term
the type of the parameters in the current function calls *)
ignore (type_term ~use_gmp_opt ~profile:typed_args t_body)
in
- let clear_env () = List.iter Interval.Env.remove li.l_profile in
Stack.push
- clear_env
pending_typing;
Stack.push
type_args_and_body
@@ -611,9 +612,9 @@ let rec type_term
let anonymous =
Logic_const.term (TBinOp(PlusA, t2, Cil.lone ())) Linteger
in
- let ty_bound = Interval.infer anonymous in
+ let ty_bound = Interval.get anonymous in
let ty_bound =
- ty_of_interv (Interval.join ty_bound (Interval.infer t1))
+ ty_of_interv (Interval.join ty_bound (Interval.get t1))
in
ignore
(type_term
@@ -621,7 +622,9 @@ let rec type_term
ignore
(type_term
~use_gmp_opt:true ~arith_operand:true ~ctx:ty_bound ~profile t2);
- let ty = ty_of_interv (Interval.infer t) ~use_gmp_opt:true ?ctx in
+ 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; *)
ignore (type_term ~use_gmp_opt:true ?ctx ~profile lambda);
dup ty
@@ -647,7 +650,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.infer t in
+ let i = Interval.get_p ~profile t in
let ty = ty_of_interv ?ctx i in
dup ty
@@ -694,28 +697,10 @@ and type_term_offset ~profile t = match t with
| TField(_, toff)
| TModel(_, toff) -> type_term_offset ~profile toff
| TIndex(t, toff) ->
- let ctx = type_offset t in
+ let ctx = type_offset ~profile t in
ignore (type_term ~use_gmp_opt:false ~ctx ~profile t);
type_term_offset ~profile toff
-and type_args params ~use_gmp_opt ~profile args fname =
- try
- List.fold_right2
- (fun lv t (typed_args : Function_params_ty.t) ->
- let ty_arg = (type_term ~use_gmp_opt ~lenv t).ty in
- begin
- try
- let typ_arg = typ_of_number_ty ty_arg in
- Interval.Env.add lv (Interval.interv_of_typ typ_arg)
- with Not_a_number -> ()
- end;
- ty_arg :: typed_args)
- params
- args
- []
- with Invalid_argument _ ->
- Options.fatal "[Tapp] unexpected number of arguments when calling %s" fname
-
(* [type_bound_variables] infers an interval associated with each of
the provided bounds of a quantified variable, and provides a term
accordingly. It could happen that the bounds provided for a quantifier
@@ -732,8 +717,8 @@ and type_args params ~use_gmp_opt ~profile args fname =
Example: [\let m = n > 0 ? 4 : 341; \forall char u; 1 < u < m ==> u > 0]
Return: R with a guard guaranteeing that [lv] does not overflow *)
and type_bound_variables ~loc ~profile (t1, lv, t2) =
- let i1 = Interval.infer t1 in
- let i2 = Interval.infer t2 in
+ let i1 = Interval.get t1 in
+ let i2 = Interval.get t2 in
let i = Interval.(widen (join i1 i2)) in
let ctx = match lv.lv_type with
| Linteger -> mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx:Gmpz i)
@@ -790,18 +775,16 @@ and type_bound_variables ~loc ~profile (t1, lv, t2) =
ignore (type_term ~use_gmp_opt:false ~ctx ~profile t2);
(* if we must generate GMP code, degrade the interval in order to
guarantee that [x] will be a GMP when typing the goal *)
- let i = match ctx with
+ let _ = match ctx with
| C_integer _ -> i
(* [ -\infty; +\infty ] *)
| Gmpz -> Interval.Ival (Ival.inject_range None None)
| C_float _ | Rational | Real | Nan ->
Options.fatal "unexpected quantification over %a" D.pretty ctx
in
- Interval.Env.add lv i;
(t1, lv, t2)
- <<<<<<< variant A
-and type_predicate ~lenv p =
+and type_predicate ~profile p =
let p = Logic_normalizer.get_pred p in
Cil.CurrentLoc.set p.pred_loc;
(* this pattern matching also follows the formal rules of the JFLA's paper *)
@@ -821,7 +804,6 @@ and type_predicate ~lenv p =
li.l_var_info.lv_name
in
ignore (type_predicate ~profile:typed_args p);
- List.iter Interval.Env.remove li.l_profile
| LBnone -> ()
| LBreads _ -> ()
| LBinductive _ -> ()
@@ -832,8 +814,8 @@ and type_predicate ~lenv p =
c_int
| Pdangling _ -> Error.not_yet "\\dangling"
| Prel(_, t1, t2) ->
- let i1 = Interval.infer t1 in
- let i2 = Interval.infer t2 in
+ let i1 = Interval.get_p ~profile t1 in
+ let i2 = Interval.get_p ~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);
@@ -882,9 +864,7 @@ and type_predicate ~lenv p =
end
| Pseparated tlist ->
List.iter
- (fun t ->
- ignore
- (type_term ~use_gmp_opt:false ~ctx:Nan ~lenv t))
+ (fun t -> ignore (type_term ~use_gmp_opt:false ~ctx:Nan ~profile t))
tlist;
c_int
| Pinitialized(_, t)
@@ -894,7 +874,7 @@ and type_predicate ~lenv p =
| Pvalid_read(_, t)
| Pobject_pointer(_,t)
| Pvalid_function t ->
- ignore (type_term ~use_gmp_opt:false ~ctx:Nan ~lenv t);
+ ignore (type_term ~use_gmp_opt:false ~ctx:Nan ~profile t);
c_int
| Pat(p, _) -> (type_predicate ~profile p).ty
| Pfresh _ -> Error.not_yet "\\fresh"
@@ -927,11 +907,17 @@ let unsafe_set t ?ctx ~logic_env ty =
(** {2 Getters} *)
(******************************************************************************)
-let get_number_ty ~profile t =
+let get_number_ty ~logic_env t =
+ let profile = Interval.Logic_environment.get_profile logic_env in
(Error.retrieve_preprocessing "typing" (Memo.get ~profile) t Printer.pp_term).ty
-let get_integer_op ~profile t =
+
+let get_integer_op ~logic_env t =
+ let profile = Interval.Logic_environment.get_profile logic_env in
(Error.retrieve_preprocessing "typing" (Memo.get ~profile) t Printer.pp_term).op
-let get_integer_op_of_predicate ~profile p = (type_predicate ~profile p).op
+
+let get_integer_op_of_predicate ~logic_env p =
+ let profile = Interval.Logic_environment.get_profile logic_env in
+ (type_predicate ~profile p).op
(* {!typ_of_integer}, but handle the not-integer cases. *)
let extract_typ t ty =
@@ -945,23 +931,27 @@ let extract_typ t ty =
| Lvar _ -> Error.not_yet "unsupported logic type: type variable"
| Larrow _ -> Error.not_yet "unsupported logic type: type arrow"
-let get_typ ~profile t =
+let get_typ ~logic_env t =
+ let profile = Interval.Logic_environment.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 ~profile t =
+let get_op ~logic_env t =
+ let profile = Interval.Logic_environment.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 ~profile t =
+let get_cast ~logic_env t =
+ let profile = Interval.Logic_environment.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 ~profile p =
+let get_cast_of_predicate ~logic_env p =
+ let profile = Interval.Logic_environment.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
@@ -992,15 +982,19 @@ let type_code_annot lenv annot =
let visitor = typing_visitor lenv in
ignore @@ visitor#visit_code_annot annot
-let preprocess_predicate profile p =
+let preprocess_predicate ~logic_env p =
Logic_normalizer.preprocess_predicate p;
Bound_variables.preprocess_predicate p;
- let visitor = typing_visitor lenv in
+ Interval.preprocess_predicate ~logic_env p;
+ let profile = Interval.Logic_environment.get_profile logic_env in
+ let visitor = typing_visitor profile in
ignore @@ visitor#visit_predicate p
-let preprocess_rte ~profile rte =
+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
type_code_annot profile rte
(*
diff --git a/src/plugins/e-acsl/src/analyses/typing.mli b/src/plugins/e-acsl/src/analyses/typing.mli
index c5fd4406cfb..8e01a914147 100644
--- a/src/plugins/e-acsl/src/analyses/typing.mli
+++ b/src/plugins/e-acsl/src/analyses/typing.mli
@@ -119,29 +119,30 @@ val clear: unit -> unit
{!type_named_predicate} has been previously computed for the given term or
predicate. *)
-val get_number_ty: profile:Interval.Profile.t -> term -> number_ty
+val get_number_ty: logic_env:Interval.Logic_environment.t -> term -> number_ty
(** @return the infered type for the given term. *)
-val get_integer_op: profile:Interval.Profile.t -> term -> number_ty
+val get_integer_op: logic_env:Interval.Logic_environment.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:
- profile:Interval.Profile.t -> predicate -> number_ty
+ logic_env:Interval.Logic_environment.t -> predicate -> number_ty
(** @return the infered type for the top operation of the given predicate. *)
-val get_typ: profile:Interval.Profile.t -> term -> typ
+val get_typ: logic_env:Interval.Logic_environment.t -> term -> typ
(** Get the type which the given term must be generated to. *)
-val get_op: profile:Interval.Profile.t -> term -> typ
+val get_op: logic_env:Interval.Logic_environment.t -> term -> typ
(** Get the type which the operation on top of the given term must be generated
to. *)
-val get_cast: profile:Interval.Profile.t -> term -> typ option
+val get_cast: logic_env:Interval.Logic_environment.t -> term -> typ option
(** Get the type which the given term must be converted to (if any). *)
-val get_cast_of_predicate: profile:Interval.Profile.t -> predicate -> typ option
+val get_cast_of_predicate:
+ logic_env:Interval.Logic_environment.t -> predicate -> typ option
(** Like {!get_cast}, but for predicates. *)
val unsafe_set:
@@ -160,14 +161,24 @@ val unsafe_set:
val typ_of_lty: logic_type -> typ
(** @return the C type that correponds to the given logic type. *)
+(*****************************************************************************)
+(** {2 Typing processing} *)
+(*****************************************************************************)
+
val type_program : file -> unit
(** compute and store the type of all the terms that will be translated
in a program *)
-val preprocess_predicate : Interval.Profile.t -> predicate -> unit
+val preprocess_predicate :
+ logic_env:Interval.Logic_environment.t ->
+ predicate ->
+ unit
(** compute and store the types of all the terms in a given predicate *)
-val preprocess_rte : profile:Interval.Profile.t -> code_annotation -> unit
+val preprocess_rte :
+ logic_env:Interval.Logic_environment.t ->
+ code_annotation ->
+ unit
(** compute and store the type of all the terms in a code annotation *)
(*
diff --git a/src/plugins/e-acsl/src/code_generator/quantif.ml b/src/plugins/e-acsl/src/code_generator/quantif.ml
index a73720ef31b..02d65f25a48 100644
--- a/src/plugins/e-acsl/src/code_generator/quantif.ml
+++ b/src/plugins/e-acsl/src/code_generator/quantif.ml
@@ -48,8 +48,8 @@ let rec has_empty_quantif_with_false_negative = function
(* case 2 *)
false
| (t1, _, t2) :: guards ->
- let iv1 = Interval.(extract_ival (infer t1)) in
- let iv2 = Interval.(extract_ival (infer t2)) in
+ let iv1 = Interval.(extract_ival (get t1)) in
+ let iv2 = Interval.(extract_ival (get t2)) in
let lower_bound, _ = Ival.min_and_max iv1 in
let _, upper_bound = Ival.min_and_max iv2 in
begin
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 3564526a8f5..cbeed7f335d 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_ats.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
@@ -92,7 +92,7 @@ end
where [t_size = tmax - tmin + (-1|0|1)] depending on whether the
inequalities are strict or large
and [t_shifted = lv - tmin + (-1|0)] (so that we start indexing at 0) *)
-let rec sizes_and_shifts_from_quantifs ~loc kf lscope sizes_and_shifts =
+let rec sizes_and_shifts_from_quantifs ~loc ~logic_env kf lscope sizes_and_shifts =
match lscope with
| [] ->
sizes_and_shifts
@@ -117,7 +117,7 @@ let rec sizes_and_shifts_from_quantifs ~loc kf lscope sizes_and_shifts =
| _ ->
Options.fatal "Unexpected comparison operator"
in
- let iv = Interval.(extract_ival (infer t_size)) in
+ let iv = Interval.(extract_ival (get ~logic_env t_size)) in
(* The EXACT amount of memory that is needed can be known at runtime. This
is because the tightest bounds for the variables can be known at runtime.
Example: In the following predicate
@@ -156,12 +156,12 @@ let rec sizes_and_shifts_from_quantifs ~loc kf lscope sizes_and_shifts =
in
(* Returning *)
let sizes_and_shifts = (t_size, t_shifted) :: sizes_and_shifts in
- sizes_and_shifts_from_quantifs ~loc kf lscope' sizes_and_shifts
+ sizes_and_shifts_from_quantifs ~loc ~logic_env kf lscope' sizes_and_shifts
| (Lvs_let(_, t) | Lvs_global(_, t)) :: _
when Misc.term_has_lv_from_vi t ->
Error.not_yet "\\at with logic variable linked to C variable"
| Lvs_let _ :: lscope' ->
- sizes_and_shifts_from_quantifs ~loc kf lscope' sizes_and_shifts
+ sizes_and_shifts_from_quantifs ~loc ~logic_env kf lscope' sizes_and_shifts
| Lvs_formal _ :: _ ->
Error.not_yet "\\at using formal variable of a logic function"
| Lvs_global _ :: _ ->
@@ -307,8 +307,9 @@ let pretranslate_to_exp_with_lscope ~loc ~lscope kf env pot =
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 logic_env = Env.Logic_env.get env in
let sizes_and_shifts =
- sizes_and_shifts_from_quantifs ~loc kf lscope_vars []
+ sizes_and_shifts_from_quantifs ~loc ~logic_env kf lscope_vars []
in
let logic_env = Env.Logic_env.get env in
(* Creating the pointer *)
--
GitLab