From f0a5db6427b8b3c94a29efd2c079518a2c6f0d9a Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@gmail.com>
Date: Tue, 19 Jul 2022 10:36:58 +0200
Subject: [PATCH] [e-acsl] first review
---
.../e-acsl/src/analyses/analyses_datatype.ml | 17 +++++++-------
.../e-acsl/src/analyses/analyses_datatype.mli | 22 +++++++++++++------
src/plugins/e-acsl/src/analyses/interval.ml | 12 +++++-----
3 files changed, 31 insertions(+), 20 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
index a3cf92e62ec..eaf5abc2297 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
+++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
@@ -395,14 +395,15 @@ module Logic_env
let new_lq_bind =
try Logic_var.Map.update x update env.let_quantif_bind
with Not_found ->
- match Logic_var.Map.find_opt x env.profile with
- | Some i ->
- (* The profile must remain unchanged, so if the variable is bound in the
- profile, we add the refined interval in the other bindings, which are
- checked first when finding the interval *)
- Logic_var.Map.add x (!ival_meet_ref i ival) env.let_quantif_bind
- | None -> Options.abort "updating a variable not in environment"
- in {env with let_quantif_bind = new_lq_bind}
+ match Logic_var.Map.find_opt x env.profile with
+ | Some i ->
+ (* The profile must remain unchanged, so if the variable is bound in
+ the profile, we add the refined interval in the other bindings,
+ which are checked first when finding the interval *)
+ Logic_var.Map.add x (!ival_meet_ref i ival) env.let_quantif_bind
+ | None -> Options.abort "updating a variable not in environment"
+ in
+ {env with let_quantif_bind = new_lq_bind}
end
diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
index 7a60fddb59c..9aa1e9e288f 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
+++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
@@ -76,20 +76,28 @@ module LFProf: Datatype.S_with_collections
- an association list for variables bound by a let or a quantification *)
module Logic_env : sig
type t
- (* forward reference to meet of intervals *)
+
+ (** forward reference to meet of intervals *)
val ival_meet_ref : (ival -> ival -> ival) ref
- (* add a new binding for a let or a quantification binder only *)
+
+ (** add a new binding for a let or a quantification binder only *)
val add : t -> logic_var -> ival -> t
- (* the empty environment *)
+
+ (** the empty environment *)
val empty : t
- (* create a new environment from a profile, for function calls *)
+
+ (** create a new environment from a profile, for function calls *)
val make : Profile.t -> t
- (* find a logic variable in the environment *)
+
+ (** 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
+
+ (** get the profile of the logic environment, i.e. bindings through function
arguments *)
val get_profile : t -> Profile.t
- (* refine the interval of a logic variable *)
+
+ (** refine the interval of a logic variable : replace an interval with a
+ more precise one *)
val refine : t -> logic_var -> ival -> t
end
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index 3c2a82a9282..c4810803071 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -687,7 +687,8 @@ let rec infer ~force ~logic_env t =
| Tif (t1, t2, t3) ->
ignore (infer ~force ~logic_env t1);
let logic_env_tbranch, logic_env_fbranch =
- compute_logic_env_if_branches logic_env t1 in
+ compute_logic_env_if_branches logic_env t1
+ in
let i2 = infer ~force ~logic_env:logic_env_tbranch t2 in
let i3 = infer ~force ~logic_env:logic_env_fbranch t3 in
Error.map2 join i2 i3
@@ -878,7 +879,6 @@ and infer_term_host ~force ~logic_env thost =
Printer.pp_typ ty
Printer.pp_term t
-
and infer_term_offset ~force ~logic_env t =
match t with
| TNoOffset -> ()
@@ -888,18 +888,20 @@ and infer_term_offset ~force ~logic_env t =
ignore (infer ~force ~logic_env t);
infer_term_offset ~force ~logic_env toff
+(* Update the interval of variables when they appear in a comparison of the form
+ [x op t] or [t op x] *)
and compute_logic_env_if_branches logic_env t =
let get_res = Error.map (fun x -> x) in
let ival v = infer ~force:false ~logic_env v in
let add_ub logic_env x v =
let max = Ival.max_int (Error.map extract_ival (ival v)) in
Logic_env.refine logic_env x (Ival (Ival.inject_range None max))
- and add_lb logic_env x v =
+ in
+ let add_lb logic_env x v =
let min = Ival.min_int (Error.map extract_ival (ival v)) in
Logic_env.refine logic_env x (Ival (Ival.inject_range min None))
- and add_eq logic_env x v =
- Logic_env.refine logic_env x (get_res (ival v))
in
+ let add_eq logic_env x v = Logic_env.refine logic_env x (get_res (ival v)) in
let t_branch, f_branch =
match t.term_node with
| TBinOp(op, {term_node = TLval(TVar x, TNoOffset)}, v) ->
--
GitLab