diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml
index 88e38a22e7215954cce28f7f9847f6fc73eb96f1..b1c754cfc2e00144cf62369d8095d9d261a7871c 100644
--- a/src/plugins/e-acsl/src/analyses/bound_variables.ml
+++ b/src/plugins/e-acsl/src/analyses/bound_variables.ml
@@ -79,13 +79,14 @@ module Quantified_predicate =
(******************************************************************************)
(* Memoization module to store the preprocessed form of a quantified predicate *)
-module Preprocessed_quantifier: sig
+module Quantifier: sig
val add: predicate -> (term * logic_var * term) list -> predicate -> unit
val get: predicate -> (term * logic_var * term) list * predicate
(** getter and setter for the additional guard that intersects with the type
of the variable *)
val get_guard_for_small_type : logic_var -> predicate option
- val add_guard_for_small_type : logic_var -> predicate option -> unit
+ val add_guard_for_small_type : logic_var -> predicate -> unit
+ val replace : predicate -> (term * logic_var * term) list -> predicate -> unit
val clear : unit -> unit
end = struct
@@ -94,7 +95,6 @@ end = struct
let guard_tbl = Cil_datatype.Logic_var.Hashtbl.create 97
let get p =
- (* Options.feedback "Get preprocessed form of predicate %a" Printer.pp_predicate p; *)
try Quantified_predicate.Hashtbl.find tbl p
with Not_found ->
Options.fatal
@@ -102,28 +102,31 @@ end = struct
Printer.pp_predicate p
let add p guarded_vars goal =
- (* Options.feedback "Adding preprocessed form of predicate %a" Printer.pp_predicate p; *)
Quantified_predicate.Hashtbl.add tbl p (guarded_vars, goal)
let get_guard_for_small_type x =
- try Cil_datatype.Logic_var.Hashtbl.find guard_tbl x
- with Not_found ->
- Options.fatal
- "The typing guard for the variable %a was not found."
- Printer.pp_logic_var x
+ try Some (Cil_datatype.Logic_var.Hashtbl.find guard_tbl x)
+ with Not_found -> None
let add_guard_for_small_type lv p =
Cil_datatype.Logic_var.Hashtbl.add guard_tbl lv p
+ let replace p guarded_vars goal =
+ Quantified_predicate.Hashtbl.replace tbl p (guarded_vars, goal)
+
let clear () =
Cil_datatype.Logic_var.Hashtbl.clear guard_tbl;
Quantified_predicate.Hashtbl.clear tbl
end
+(** Getters and setters *)
let get_preprocessed_quantifier = Quantifier.get
let get_guard_for_small_type = Quantifier.get_guard_for_small_type
+let add_guard_for_small_type = Quantifier.add_guard_for_small_type
+let replace = Quantifier.replace
let clear_guards = Quantifier.clear
+
(** Helper module to process the constraints in the quantification and extract
guards for the quantified variables. *)
module Constraints: sig
@@ -628,13 +631,9 @@ let compute_quantif_guards ~is_forall quantif bounded_vars p =
guards, goal
-let () = Typing.compute_quantif_guards_ref := compute_quantif_guards
-
-(** Take a guard and put it in normal form
+(** Takes a guard and put it in normal form
[t1 <= x < t2] so that [t1] is the first value
- taken by [x] and [t2] is the last one.
- This step also adds the extra guard if the type
- of the quantified variable is small *)
+ taken by [x] and [t2] is the last one. *)
let normalize_guard ~loc (t1, rel1, lv, rel2, t2) =
let t_plus_one t =
let tone = Cil.lone ~loc () in
@@ -659,12 +658,100 @@ let normalize_guard ~loc (t1, rel1, lv, rel2, t2) =
| Rgt | Rge | Req | Rneq ->
assert false
in
- let t1, t2, guard_for_small_type = bounds_for_small_types ~loc (t1, lv, t2) in
- Quantifier.add_guard_for_small_type lv guard_for_small_type;
t1, lv, t2
+
let compute_guards loc ~is_forall p bounded_vars hyps =
let guards,goal = compute_quantif_guards p ~is_forall bounded_vars hyps in
(* transform [guards] into [lscope_var list] *)
let normalized_guards = List.map (normalize_guard ~loc) guards
in Quantifier.add p normalized_guards goal
+
+module Preprocessor : sig
+ val compute : file -> unit
+ val compute_annot : code_annotation -> unit
+ val compute_predicate : predicate -> unit
+end
+= struct
+
+ let process_quantif ~loc p =
+ Cil.CurrentLoc.set loc;
+ match p.pred_content with
+ | Pforall(bound_vars, ({ pred_content = Pimplies(_, _) } as goal)) ->
+ compute_guards loc ~is_forall:true p bound_vars goal
+ | Pexists(bound_vars, ({ pred_content = Pand(_, _) } as goal)) ->
+ compute_guards loc ~is_forall:false p bound_vars goal
+ | Pforall _ -> Error.not_yet "unguarded \\forall quantification"
+ | Pexists _ -> Error.not_yet "unguarded \\exists quantification"
+ | _ -> ()
+
+ let preprocessor = object
+ inherit Visitor.frama_c_inplace
+
+ (* Only logic functions and logic predicates are handled.
+ E-acsl simply ignores all the other global annotations *)
+ method !vannotation annot =
+ match annot with
+ | Dfun_or_pred _ -> Cil.DoChildren
+ | _ -> Cil.SkipChildren
+
+ (* Ignore the annotations attached to statements from the RTL *)
+ method !vglob_aux =
+ function
+ (* library functions and built-ins *)
+ | GVarDecl(vi, _) | GVar(vi, _, _)
+ | GFunDecl(_, vi, _) | GFun({ svar = vi }, _) when Builtins.mem vi.vname ->
+ Cil.SkipChildren
+
+ | GVarDecl(vi, _) | GVar(vi, _, _) | GFun({ svar = vi }, _)
+ when Misc.is_fc_or_compiler_builtin vi ->
+ Cil.SkipChildren
+ | g when Rtl.Symbols.mem_global g ->
+ Cil.SkipChildren
+
+ (* generated function declaration: nothing to do *)
+ | GFunDecl(_, vi, _) when Misc.is_fc_stdlib_generated vi ->
+ Cil.SkipChildren
+
+ | GFun({svar = vi}, _) ->
+ let kf = try Globals.Functions.get vi with Not_found -> assert false in
+ if Functions.check kf then Cil.DoChildren else Cil.SkipChildren
+
+ | GAnnot _ -> Cil.DoChildren
+
+ (* other globals: nothing to do *)
+ | GFunDecl _
+ | GVarDecl _
+ | GVar _
+ | GType _
+ | GCompTag _
+ | GCompTagDecl _
+ | GEnumTag _
+ | GEnumTagDecl _
+ | GAsm _
+ | GPragma _
+ | GText _
+ -> Cil.SkipChildren
+
+ method !vpredicate p =
+ let loc = p.pred_loc in
+ match Preprocess_predicates.get_preprocessed_form p with
+ | PoT_pred p -> Error.generic_handle (process_quantif ~loc) () p;
+ Cil.DoChildren
+ | PoT_term _ -> Cil.DoChildren
+
+ end
+
+ let compute ast =
+ Visitor.visitFramacFileSameGlobals preprocessor ast
+
+ let compute_annot annot =
+ ignore (Visitor.visitFramacCodeAnnotation preprocessor annot)
+
+ let compute_predicate p =
+ ignore (Visitor.visitFramacPredicate preprocessor p)
+end
+
+let preprocess = Preprocessor.compute
+let preprocess_annot = Preprocessor.compute_annot
+let preprocess_predicate = Preprocessor.compute_predicate
diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.mli b/src/plugins/e-acsl/src/analyses/bound_variables.mli
index bd32dc7b576334137289266931c9fb51f6d99257..51041a1f1915f157c24b903a486582b1b06fa502 100644
--- a/src/plugins/e-acsl/src/analyses/bound_variables.mli
+++ b/src/plugins/e-acsl/src/analyses/bound_variables.mli
@@ -33,10 +33,27 @@ val get_preprocessed_quantifier: predicate -> (term * logic_var * term) list * p
along with their syntactic guards, and the [predicate] is the goal: the original
predicate with all the quantifiers removed *)
+val add_guard_for_small_type : logic_var -> predicate -> unit
+(** Adds an optional additional guard condition that comes from the typing *)
+
val get_guard_for_small_type : logic_var -> predicate option
(** @return the optional additional guard for a quantified logic variables. It may
happen that the syntactic guard of the variable can be refined with the type
of the variable, this additional predicate translates this refinement *)
+val replace : predicate -> (term * logic_var * term) list -> predicate -> unit
+(** Replace the computed guards. This is because the typing sometimes simplifies the
+ computed bounds, so we allow for storing new bounds *)
+
val clear_guards : unit -> unit
(** Clear the table of guard conditions for quantified variables *)
+
+val preprocess : file -> unit
+(** Preprocess all the quantified predicates in the ast and store the result
+ in an hashtable *)
+
+val preprocess_annot : code_annotation -> unit
+(** Preprocess the quantified in a given code annotation *)
+
+val preprocess_predicate : predicate -> unit
+(** Preprocess the quantified predicate in a given predicate *)
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index 0f1094d579d4bad8f02c6bb3feca1c84d8ec3678..7e6a9b3c90ce19623dac955393040fbebc70b64a 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -595,8 +595,10 @@ and type_term_offset = function
let ctx = type_offset t in
ignore (type_term ~use_gmp_opt:false ~ctx t);
type_term_offset toff
-(* It could happen that the bounds provided for a quantifier [lv] are bigger
- than its type. [bounds_for_small_type] handles such cases
+(* [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
@@ -608,49 +610,79 @@ and type_term_offset = function
- 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 bounds_for_small_types ~loc (t1, lv, t2) =
- match lv.lv_type with
- | Ltype _ | Lvar _ | Lreal | Larrow _ ->
- Error.not_yet "quantification over non-integer type"
- | Linteger ->
- t1, t2, None
- | Ctype ty ->
- let iv1 = Interval.(extract_ival (infer t1)) in
- let iv2 = Interval.(extract_ival (infer t2)) in
- (* Ival.join is NOT correct here:
- Eg: (Ival.join [-3..-3] [300..300]) gives {-3, 300}
- but NOT [-3..300] *)
- let iv = Ival.inject_range (Ival.min_int iv1) (Ival.max_int iv2) in
- let ity = Interval.extract_ival (Interval.extended_interv_of_typ ty) in
- if Ival.is_included iv ity then
- (* case 1 *)
- t1, t2, None
- else if Ival.is_singleton_int iv1 && Ival.is_singleton_int iv2 then begin
- (* case 2 *)
- let i = Ival.meet iv ity in
- (* now we potentially have a better interval for [lv]
- ==> update the binding *)
- Interval.Env.replace lv (Interval.Ival i);
- (* the smaller bounds *)
- let min, max = Misc.finite_min_and_max i in
- let t1 = Logic_const.tint ~loc min in
- let t2 = Logic_const.tint ~loc max in
- let ctx = Typing.number_ty_of_typ ~post:false ty in
- (* we are assured that we will not have a GMP,
- once again because we intersected with [ity] *)
- Typing.type_term ~use_gmp_opt:false ~ctx t1;
- Typing.type_term ~use_gmp_opt:false ~ctx t2;
- t1, t2, None
- end else
- (* case 3 *)
- let min, max = Misc.finite_min_and_max 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
- t1, t2, Some guard
+let type_bound_variables ~loc ~dep ~lenv (t1, lv, t2) =
+ let i1 = Interval.(extract_ival (infer t1)) in
+ let i2 = Interval.(extract_ival (infer t2)) in
+ (* Ival.join is NOT correct here:
+ Eg: (Ival.join [-3..-3] [300..300]) gives {-3, 300}
+ but NOT [-3..300] *)
+ let i = Ival.inject_range (Ival.min_int i1) (Ival.max_int i2) in
+ (* let i = Interval.join i1 i2 in *)
+ let ctx = match lv.lv_type with
+ | Linteger -> mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx:Gmpz (Interval.Ival i))
+ | Ctype ty ->
+ (match Cil.unrollType ty with
+ | TInt(ik, _) -> mk_ctx ~use_gmp_opt:true (C_integer ik)
+ | ty ->
+ Options.fatal "unexpected type %a for quantified variable %a"
+ Printer.pp_typ ty
+ Printer.pp_logic_var lv)
+ | lty ->
+ Options.fatal "unexpected 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 iv1 = Interval.(extract_ival (infer t1)) in
+ * let iv2 = Interval.(extract_ival (infer t2)) in
+ * (\* Ival.join is NOT correct here:
+ * Eg: (Ival.join [-3..-3] [300..300]) gives {-3, 300}
+ * but NOT [-3..300] *\)
+ * let iv = Ival.inject_range (Ival.min_int iv1) (Ival.max_int iv2) in *)
+ let ity = Interval.extract_ival (Interval.extended_interv_of_typ ty) in
+ if Ival.is_included i ity then
+ (* case 1 *)
+ t1, t2, i
+ else if Ival.is_singleton_int i1 && Ival.is_singleton_int i2 then begin
+ (* case 2 *)
+ let i = Ival.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 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 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
+ Bound_variables.add_guard_for_small_type lv guard;
+ t1, t2, i
+ 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 ~dep ~lenv t1);
+ ignore (type_term ~use_gmp_opt:false ~ctx ~dep ~lenv 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
+ | C_integer _ -> i
+ | Gmpz -> Ival.inject_range None None (* [ -\infty; +\infty ] *)
+ | C_float _ | Rational | Real | Nan ->
+ Options.fatal "unexpected quantification over %a" D.pretty ctx
+ in
+ Interval.Env.add lv (Interval.Ival i);
+ (t1, lv, t2)
let rec type_predicate p =
Cil.CurrentLoc.set p.pred_loc;
@@ -709,66 +741,18 @@ let rec type_predicate p =
ignore (type_term ~use_gmp_opt:true li_t);
(type_predicate p).ty
- | Pforall(bounded_vars, ({ pred_content = Pimplies(_, _) } as p'))
- | Pexists(bounded_vars, ({ pred_content = Pand(_, _) } as p')) ->
- let is_forall =
- match p.pred_content with
- | Pforall _ -> true
- | Pexists _ -> false
- | _ -> assert false
- in
+
+ | Pforall(_, { pred_content = Pimplies(_, _) })
+ | Pexists(_, { pred_content = Pand(_, _) }) ->
let guards, goal =
- !compute_quantif_guards_ref ~is_forall p bounded_vars p'
- in
- let iv_plus_one iv =
- Interval.Ival (Ival.add_singleton_int Integer.one iv)
+ Bound_variables.get_preprocessed_quantifier p
in
- List.iter
- (fun (t1, r1, x, r2, t2) ->
- let i1 = Interval.infer t1 in
- let i1 = match r1, i1 with
- | Rlt, Interval.Ival iv -> iv_plus_one iv
- | Rle, _ -> i1
- | _ -> assert false
- in
- let i2 = Interval.infer t2 in
- (* add one to [i2], since we increment the loop counter one more
- time before going outside the loop. *)
- let i2 = match r2, i2 with
- | Rlt, _ -> i2
- | Rle, Interval.Ival iv -> iv_plus_one iv
- | _ -> assert false
- in
- let i = Interval.join i1 i2 in
- let ctx = match x.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, _) -> mk_ctx ~use_gmp_opt:true (C_integer ik)
- | ty ->
- Options.fatal "unexpected type %a for quantified variable %a"
- Printer.pp_typ ty
- Printer.pp_logic_var x)
- | lty ->
- Options.fatal "unexpected type %a for quantified variable %a"
- Printer.pp_logic_type lty
- Printer.pp_logic_var x
- 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 t1);
- ignore (type_term ~use_gmp_opt:false ~ctx 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
- | C_integer _ -> i
- | Gmpz -> Interval.top_ival (* [ -\infty; +\infty ] *)
- | C_float _ | Rational | Real | Nan ->
- Options.fatal "unexpected quantification over %a" D.pretty ctx
- in
- Interval.Env.add x i)
- guards;
- (type_predicate goal).ty
+ let guards =
+ List.map
+ (fun (t1, x, t2) ->
+ type_bound_variables ~loc:p.pred_loc ~dep ~lenv (t1, x, t2))
+ guards
+ in Bound_variables.replace p guards goal;
| Pseparated tlist ->
List.iter
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index 275d229ff01904b1f55aecb28d20e529aed981cb..e865ccb14bbe3b6f649337e495a9098158a3149a 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -864,6 +864,7 @@ let inject () =
Project.pretty (Project.current ());
Gmp_types.init ();
let ast = Ast.get () in
+ Bound_variables.preprocess ast;
Preprocess_typing.type_program ast;
inject_in_file ast;
reset_all ast;