From 75e0727fc8c4e64558763e286eb0526fa68223f4 Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@gmail.com>
Date: Fri, 21 Jan 2022 14:55:17 +0100
Subject: [PATCH] [e-acsl] add interval inference for quantifiers
---
src/plugins/e-acsl/src/analyses/interval.ml | 82 ++++++++++-
src/plugins/e-acsl/src/analyses/typing.ml | 130 +++++-------------
src/plugins/e-acsl/src/analyses/typing.mli | 5 +
.../e-acsl/src/code_generator/loops.ml | 6 +-
.../e-acsl/src/code_generator/quantif.ml | 34 +++--
5 files changed, 146 insertions(+), 111 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index 12a48c77bd9..37c29cecc80 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -862,7 +862,65 @@ and infer_term_offset ~logic_env t =
ignore (infer ~logic_env t);
infer_term_offset ~logic_env toff
-let rec infer_predicate ~logic_env p =
+(* [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
+ [lv] are bigger than its type. [type_bound_variables] handles such cases
+ and provides smaller bounds whenever possible.
+ Let B be the inferred interval and R the range of [lv.typ]
+ - Case 1: B \subseteq R
+ Example: [\forall unsigned char c; 4 <= c <= 100 ==> 0 <= c <= 255]
+ Return: B
+ - Case 2: B \not\subseteq R and the bounds of B are inferred exactly
+ Example: [\forall unsigned char c; 4 <= c <= 300 ==> 0 <= c <= 255]
+ Return: B \intersect R
+ - Case 3: B \not\subseteq R and the bounds of B are NOT inferred exactly
+ 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 *)
+let rec 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 i = widen (join i1 i2) in
+ let t1, t2, i =
+ match lv.lv_type with
+ | Ltype _ | Lvar _ | Lreal | Larrow _ ->
+ Error.not_yet "quantification over non-integer type"
+ | Linteger -> t1, t2, i
+ | Ctype ty ->
+ let ity = extended_interv_of_typ ty in
+ if is_included i ity then
+ (* case 1 *)
+ t1, t2, i
+ else if is_singleton_int i1 &&
+ is_singleton_int i2 then
+ begin
+ (* case 2 *)
+ let i = meet i ity in
+ (* We can now update the bounds in the preprocessed form
+ that come from the meet of the two intervals *)
+ let min, max = Misc.finite_min_and_max (extract_ival i) in
+ let t1 = Logic_const.tint ~loc min in
+ let t2 = Logic_const.tint ~loc max in
+ t1, t2, i
+ end else
+ (* case 3 *)
+ let min, max = Misc.finite_min_and_max (extract_ival ity) in
+ let guard_lower = Logic_const.tint ~loc min in
+ let guard_upper = Logic_const.tint ~loc max in
+ let lv_term = Logic_const.tvar ~loc lv in
+ let guard_lower = Logic_const.prel ~loc (Rle, guard_lower, lv_term) in
+ let guard_upper = Logic_const.prel ~loc (Rlt, lv_term, guard_upper) in
+ let guard = Logic_const.pand ~loc (guard_lower, guard_upper) in
+ ignore (infer_predicate ~logic_env guard);
+ 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)
+
+and infer_predicate ~logic_env p =
match Logic_normalizer.get_pred p with
| PoT_term t -> ignore (infer ~logic_env t)
| PoT_pred p ->
@@ -896,8 +954,26 @@ let rec infer_predicate ~logic_env p =
in
(infer_predicate ~logic_env p)
| Pforall _
- | Pexists _ -> ()
- (* TODO: *)
+ | Pexists _ ->
+ let guards, goal =
+ Error.retrieve_preprocessing
+ "quantified predicate"
+ Bound_variables.get_preprocessed_quantifier
+ p
+ Printer.pp_predicate
+ in
+ let loc = p.pred_loc in
+ let rec do_analysis guards new_guards logic_env = match guards with
+ | [] -> logic_env, new_guards
+ | guard :: guards ->
+ let logic_env, new_guard =
+ infer_bound_variable ~loc ~logic_env guard
+ in
+ do_analysis guards (new_guard :: new_guards) logic_env
+ in
+ let logic_env, new_guards = do_analysis guards [] logic_env in
+ Bound_variables.replace p new_guards goal;
+ infer_predicate ~logic_env goal
| Pseparated tlist ->
List.iter
(fun t -> ignore (infer ~logic_env t))
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index 5df42089d01..ffffd7fb737 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -702,88 +702,33 @@ and type_term_offset ~profile t = match t with
ignore (type_term ~use_gmp_opt:false ~ctx ~profile t);
type_term_offset ~profile toff
-(* [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
- [lv] are bigger than its type. [type_bound_variables] handles such cases
- and provides smaller bounds whenever possible.
- Let B be the inferred interval and R the range of [lv.typ]
- - Case 1: B \subseteq R
- Example: [\forall unsigned char c; 4 <= c <= 100 ==> 0 <= c <= 255]
- Return: B
- - Case 2: B \not\subseteq R and the bounds of B are inferred exactly
- Example: [\forall unsigned char c; 4 <= c <= 300 ==> 0 <= c <= 255]
- Return: B \intersect R
- - Case 3: B \not\subseteq R and the bounds of B are NOT inferred exactly
- 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.get t1 in
- let i2 = Interval.get t2 in
+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 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)
- | Ctype ty ->
- (match Cil.unrollType ty with
- | TInt(ik, _) | TEnum({ ekind = ik }, _) ->
- mk_ctx ~use_gmp_opt:true (C_integer ik)
- | ty ->
- Options.fatal "unexpected C type %a for quantified variable %a"
- Printer.pp_typ ty
- Printer.pp_logic_var lv)
- | lty ->
- Options.fatal "unexpected logic type %a for quantified variable %a"
- Printer.pp_logic_type lty
- Printer.pp_logic_var lv
- in
- let t1, t2, i =
- match lv.lv_type with
- | Ltype _ | Lvar _ | Lreal | Larrow _ ->
- Error.not_yet "quantification over non-integer type"
- | Linteger -> t1, t2, i
- | Ctype ty ->
- let ity = Interval.extended_interv_of_typ ty in
- if Interval.is_included i ity then
- (* case 1 *)
- t1, t2, i
- else if Interval.is_singleton_int i1 &&
- Interval.is_singleton_int i2 then
- begin
- (* case 2 *)
- let i = Interval.meet i ity in
- (* We can now update the bounds in the preprocessed form
- that come from the meet of the two intervals *)
- let min, max = Misc.finite_min_and_max (Interval.extract_ival i) in
- let t1 = Logic_const.tint ~loc min in
- let t2 = Logic_const.tint ~loc max in
- t1, t2, i
- end else
- (* case 3 *)
- let min, max = Misc.finite_min_and_max (Interval.extract_ival ity) in
- let guard_lower = Logic_const.tint ~loc min in
- let guard_upper = Logic_const.tint ~loc max in
- let lv_term = Logic_const.tvar ~loc lv in
- let guard_lower = Logic_const.prel ~loc (Rle, guard_lower, lv_term) in
- let guard_upper = Logic_const.prel ~loc (Rlt, lv_term, guard_upper) in
- let guard = Logic_const.pand ~loc (guard_lower, guard_upper) in
- ignore (type_predicate ~profile guard);
- Bound_variables.add_guard_for_small_type lv guard;
- t1, t2, i
- in
+ match lv.lv_type with
+ | Linteger ->
+ mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx:Gmpz i)
+ | Ctype ty ->
+ (match Cil.unrollType ty with
+ | TInt(ik, _) | TEnum({ ekind = ik}, _)-> join
+ (ty_of_interv i)
+ (mk_ctx ~use_gmp_opt:true (C_integer ik))
+ | ty ->
+ Options.fatal "unexpected C type %a for quantified variable %a"
+ Printer.pp_typ ty
+ Printer.pp_logic_var lv)
+ | lty ->
+ Options.fatal "unexpected logic type %a for quantified variable %a"
+ Printer.pp_logic_type lty
+ Printer.pp_logic_var lv
+
+and type_bound_variables ~profile (t1, lv, t2) =
+ 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);
- 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 _ = 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
- (t1, lv, t2)
+ ignore(type_term ~use_gmp_opt:false ~ctx ~profile t1);
+ ignore(type_term ~use_gmp_opt:false ~ctx ~profile t2)
and type_predicate ~profile p =
let p = Logic_normalizer.get_pred p in
@@ -796,15 +741,12 @@ and type_predicate ~profile p =
begin
match li.l_body with
| LBpred p ->
- let typed_args =
- type_args
- ~use_gmp_opt:true
- ~profile
- li.l_profile
- args
- li.l_var_info.lv_name
- in
- ignore (type_predicate ~profile:typed_args p);
+ List.iter
+ (fun x -> ignore
+ (type_term ~use_gmp_opt: true ~profile x))
+ args;
+ let new_profile = List.map (Interval.get_p ~profile) args in
+ ignore (type_predicate ~profile:new_profile p);
| LBnone -> ()
| LBreads _ -> ()
| LBinductive _ -> ()
@@ -855,12 +797,10 @@ and type_predicate ~profile p =
p
Printer.pp_predicate
in
- let guards =
- List.map
- (fun (t1, x, t2) ->
- type_bound_variables ~loc:p.pred_loc ~profile (t1, x, t2))
- guards
- in Bound_variables.replace p guards goal;
+ List.iter
+ (fun (t1, x, t2) ->
+ type_bound_variables ~profile (t1, x, t2))
+ guards;
(type_predicate ~profile goal).ty
end
| Pseparated tlist ->
@@ -970,7 +910,7 @@ let typing_visitor profile = object
those errrors are stored in the table and warnings are raised at
translation time *)
ignore
- (try type_named_predicate ~lenv p
+ (try type_named_predicate ~profile p
with Error.Not_yet _ | Error.Typing_error _ -> ());
Cil.SkipChildren
end
diff --git a/src/plugins/e-acsl/src/analyses/typing.mli b/src/plugins/e-acsl/src/analyses/typing.mli
index 04da55ac107..67dce8431e2 100644
--- a/src/plugins/e-acsl/src/analyses/typing.mli
+++ b/src/plugins/e-acsl/src/analyses/typing.mli
@@ -93,6 +93,11 @@ val join: number_ty -> number_ty -> number_ty
semi-lattice. If one of the argument is {!Other}, the function assumes that
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
+
(******************************************************************************)
(** {2 Typing} *)
(******************************************************************************)
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index 5286d9e0dd3..7eb6fa62db3 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -290,9 +290,9 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
Typing.preprocess_term ~use_gmp_opt:false ~logic_env t1;
Typing.preprocess_term ~use_gmp_opt:false ~logic_env t2;
let ctx =
- let ty1 = Typing.get_number_ty ~logic_env t1 in
- let ty2 = Typing.get_number_ty ~logic_env t2 in
- Typing.join ty1 ty2
+ Typing.number_ty_bound_variable
+ ~profile:(Interval.Logic_environment.get_profile (Env.Logic_env.get env))
+ (t1, logic_x, t2)
in
let t_plus_one ?ty t =
(* whenever provided, [ty] is known to be the type of the result *)
diff --git a/src/plugins/e-acsl/src/code_generator/quantif.ml b/src/plugins/e-acsl/src/code_generator/quantif.ml
index 02d65f25a48..2b1f17bb74e 100644
--- a/src/plugins/e-acsl/src/code_generator/quantif.ml
+++ b/src/plugins/e-acsl/src/code_generator/quantif.ml
@@ -43,22 +43,23 @@ let predicate_to_exp_ref
[has_empty_quantif_with_false_negative] partially detects such cases:
Case 1: an empty quantification was detected for sure, return true.
Case 2: we don't know, return false. *)
-let rec has_empty_quantif_with_false_negative = function
+let rec has_empty_quantif_with_false_negative ~logic_env = function
| [] ->
(* case 2 *)
false
| (t1, _, t2) :: guards ->
- let iv1 = Interval.(extract_ival (get t1)) in
- let iv2 = Interval.(extract_ival (get t2)) in
+ let iv1 = Interval.(extract_ival (get ~logic_env t1)) in
+ let iv2 = Interval.(extract_ival (get ~logic_env t2)) in
let lower_bound, _ = Ival.min_and_max iv1 in
let _, upper_bound = Ival.min_and_max iv2 in
begin
match lower_bound, upper_bound with
| Some lower_bound, Some upper_bound ->
let res = lower_bound >= upper_bound in
- res (* case 1 *) || has_empty_quantif_with_false_negative guards
+ res (* case 1 *) ||
+ has_empty_quantif_with_false_negative guards ~logic_env
| None, _ | _, None ->
- has_empty_quantif_with_false_negative guards
+ has_empty_quantif_with_false_negative guards ~logic_env
end
let () =
@@ -80,7 +81,11 @@ let convert kf env loc ~is_forall quantif =
quantif
Printer.pp_predicate
in
- match has_empty_quantif_with_false_negative bound_vars, is_forall with
+ match (has_empty_quantif_with_false_negative
+ ~logic_env:(Env.Logic_env.get env)
+ bound_vars),
+ is_forall
+ with
| true, true ->
Cil.one ~loc, env
| true, false ->
@@ -96,14 +101,17 @@ let convert kf env loc ~is_forall quantif =
else z, o, fun e -> Smart_exp.lnot ~loc:e.eloc e
in
(* transform [bound_vars] into [lscope_var list],
- and update logic scope in the process *)
- let lvs_guards, env = List.fold_right
- (fun (t1, lv, t2) (lvs_guards, env) ->
+ and update logic scope and logic environment in the process *)
+ let lvs_guards, env = List.fold_left
+ (fun (lvs_guards, env) (t1, lv, t2) ->
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
lvs :: lvs_guards, env)
- bound_vars
([], env)
+ bound_vars
in
let var_res, res, env =
(* variable storing the result of the quantifier *)
@@ -157,6 +165,12 @@ 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
+ (fun env _ -> Env.Logic_env.pop env)
+ env
+ lvs_guards
+ in
res, env
end
--
GitLab