diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index bc2d25e3edeec9aa496db2bb54df3355916a4fc0..d5d488ff22b009b0dea86cc055aec6f620158d9c 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -63,7 +63,8 @@ SRC_ANALYSES:= \
exit_points \
lscope \
interval \
- typing
+ typing \
+ bound_variables
SRC_ANALYSES:=$(addprefix src/analyses/, $(SRC_ANALYSES))
# code generator
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 6b448f789441d6b8d95e5a5a1acd19e4d2ded92c..b0a81804aefdf99a1ce61a91cfa906ad0c131a87 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -25,6 +25,9 @@
Plugin E-ACSL <next-release>
############################
+-* E-ACSL [2021-07-30] Fix incorrect evaluation of quantified
+ predicates when a strict guard overlaps with the type of the
+ bound variable (unlikely in practice) (frama-c/e-acsl#149).
- E-ACSL [2021-07-06] Add support for the extended quantifier \sum.
-* E-ACSL [2021-06-22] Fix a crash that occured when using certain
combinations of nested blocks and annotations.
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index 7f24e72705c0e02ecd7c80e03048f3fed66aaa35..f6e7a2458dea59fa67cbdf6a689c8ea05d0ac378 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/src/plugins/e-acsl/headers/header_spec.txt
@@ -67,6 +67,8 @@ share/e-acsl/observation_model/e_acsl_observation_model.c: CEA_LGPL_OR_PROPRIETA
share/e-acsl/observation_model/e_acsl_observation_model.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/e_acsl.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/e_acsl_rtl.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/analyses/bound_variables.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/analyses/bound_variables.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/exit_points.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/exit_points.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/interval.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml
new file mode 100644
index 0000000000000000000000000000000000000000..c893fa97761bd74b106b4ab6ce5107d1186765a9
--- /dev/null
+++ b/src/plugins/e-acsl/src/analyses/bound_variables.ml
@@ -0,0 +1,730 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-2020 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** Module for preprocessing the quantified predicates. Predicates with
+ quantifiers are hard to translate, so we delegate some of the work to a
+ preprocessing phase. At the end of this phase, all the quantified predicates
+ should have an associated preprocessed form [vars * goal] where - [vars] is a
+ list of guarded variables in the right order - [goal] is the predicate under
+ the quantifications The guarded variables in the list [vars] are of type
+ [term * logic_var * term * predicate option], where a tuple [(t1,v,t2,p)]
+ indicates that v is a logic variable with the two guards t1 <= x < t2 and p
+ is an additional optional guard to intersect the first guard with the
+ provided type for the variable v *)
+
+open Cil_types
+open Cil
+open Cil_datatype
+
+(** [error_msg quantif msg pp x] creates an error message from the string [msg]
+ containing the value [x] pretty-printed by [pp] and the predicate [quantif]
+ pretty-printed. *)
+let error_msg quantif msg pp x =
+ let msg1 = Format.asprintf msg pp x in
+ let msg2 =
+ Format.asprintf "@[ in quantification@ %a@]"
+ Printer.pp_predicate quantif
+ in
+ msg1 ^ msg2
+
+
+(** A module to work with quantifiers at preprocessing time. We create
+ a datatype to hash quantified predicates by simply giving the hash
+ of their first variable.
+*)
+module Quantified_predicate =
+ Datatype.Make_with_collections
+ (struct
+ include Cil_datatype.Predicate
+ let name = "E_ACSL.Quantified_predicate"
+ let hash (p:predicate) = match p.pred_content with
+ | Pforall(lvs,_)
+ | Pexists(lvs,_) ->
+ begin match lvs with
+ |[] -> 0
+ |lv::_ -> Cil_datatype.Logic_var.hash lv
+ end
+ | _ -> assert false
+ (* The function compare should never be used since we only use this
+ datatype for hashtables *)
+ let compare _ _ = assert false
+ let equal (p1:predicate) p2 = p1 == p2
+ let structural_descr = Structural_descr.t_abstract
+ let rehash = Datatype.identity
+ let mem_project = Datatype.never_any_project
+ end)
+
+(******************************************************************************)
+(** Storing the preprocessed quantifiers *)
+(******************************************************************************)
+
+(** In order to retrieve the preprocessed form of a quantified predicate
+ * we store it in a hash table. *)
+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 clear : unit -> unit
+end = struct
+
+ let tbl = Quantified_predicate.Hashtbl.create 97
+
+ 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
+ "The preprocessed form of predicate %a was not found."
+ 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
+
+ let add_guard_for_small_type lv p =
+ Cil_datatype.Logic_var.Hashtbl.add guard_tbl lv p
+
+ let clear () =
+ Cil_datatype.Logic_var.Hashtbl.clear guard_tbl;
+ Quantified_predicate.Hashtbl.clear tbl
+end
+
+let get_preprocessed_quantifier = Quantifier.get
+let get_guard_for_small_type = Quantifier.get_guard_for_small_type
+let clear_guards = Quantifier.clear
+
+(** Helper module to process the constraints in the quantification and extract
+ guards for the quantified variables. *)
+module Constraints: sig
+ (** Context type manipulated by the functions of the module. *)
+ type t
+
+ (** [empty quantif bounded_vars] creates an empty context from a
+ quantification predicate and the list of bounded variables for the
+ predicate. *)
+ val empty: predicate -> logic_var list -> t
+
+ (** [get_bounded_var ctxt t] returns the logic var corresponding to the given
+ term if the term is a variable ([TLval(Tvar _, TNoOffset)]) that is a
+ bounded variable for the quantification being processed, or [None]
+ otherwise. *)
+ val get_bounded_var: term -> t -> logic_var option
+
+ (** [has_unguarded_bounded_vars ctxt] returns true iff some bounded variables
+ in [ctxt] do not have a guard extracted from the quantification
+ predicate. *)
+ val has_unguarded_bounded_vars: t -> bool
+
+ (** [add_lower_bound ctxt t r lv] adds the lower bound [t r lv] to the list
+ of guards for the quantification.
+ @raises Typing_error if a lower bound already exists for [lv]. *)
+ val add_lower_bound: term -> relation -> logic_var -> t -> t
+
+ (** [add_linked_upper_bound ctxt lv1 r lv2] adds a link between two bounded
+ variables with still incomplete guards. [lv1] should already have at least
+ a lower bound.
+ @raises Typing_error if [lv1] do not have an existing lower bound. *)
+ val add_linked_upper_bound: logic_var -> relation -> logic_var -> t -> t
+
+ (** [add_upper_bound ctxt lv r t] adds the upper bound [lv r t] to the list of
+ guards for the quantification.
+ For each existing linked relation [lv' r' lv], also adds the upper bound
+ [lv' r'' t] to the list of guards, with [r''] being the strictest relation
+ between [r]Â and [r'].
+ @raises Typing_error if either [lv] or [lv'] does not have an existing
+ lower bound. *)
+ val add_upper_bound: logic_var -> relation -> term -> t -> t
+
+ (** [check_validity ctxt] checks the validity of the quantification after
+ processing.
+ @raises Typing_error if some bound (lower or upper) cound not be extracted
+ from the quantification for each bounded variable. *)
+ val check_validity: t -> unit
+
+ (** [retrieve_guards ctxt] returns the list of guards for the bounded
+ variables of the quantification, in the order in which they must be
+ generated, ie. if [j] depends on [i] then the guard for [i] will be before
+ the guard for [j] in the list.
+ [check_validity ctxt] must have been called before calling
+ [retrieve_guards]. *)
+ val retrieve_guards: t -> (term * relation * logic_var * relation * term) list
+
+ (** [raise_error ctxt msg] raises a [Typing_error] exception with the given
+ message after appending the quantification from the context. *)
+ val raise_error: string -> t -> 'a
+
+ (** [error_invalid_pred ?warn_rel ctxt p] raises a [Typing_error] exception
+ with a message indicating that the predicate [p] is not valid in the
+ quantification. Depending on the state of [ctxt], more information about
+ missing bounds is added to the message. If [warn_rel] is [true], then a
+ reminder that only [Rle] and [Rlt] are allowed to guard quantified
+ variables is added to the message. *)
+ val raise_error_invalid_pred: ?warn_rel:bool -> predicate -> t -> 'a
+end = struct
+ type t = {
+ (** Quantification predicate being analyzed. *)
+ quantif: predicate;
+ (** Variables of the quantification that still need guards. *)
+ bounded_vars: Logic_var.Set.t;
+ (** Bounded variables list in reverse order in which they must be
+ generated. *)
+ rev_order: Logic_var.t list;
+ (** Table associating a bounded variable with its guard. *)
+ guards: (term * relation * (relation * term) option) Logic_var.Map.t;
+ (** Table associating a bounded variable with a relation with another
+ bounded variable. *)
+ linked_upper_bounds: (logic_var * relation) Logic_var.Map.t;
+ }
+
+ let empty quantif bounded_vars =
+ (* Check that the bounded vars have integer type and store them in a set. *)
+ let bounded_vars =
+ List.fold_left
+ (fun s v ->
+ let v =
+ match v.lv_type with
+ | Ctype ty when isIntegralType ty -> v
+ | Linteger -> v
+ | Ltype _ as ty when Logic_const.is_boolean_type ty -> v
+ | Ctype _ | Ltype _ | Lvar _ | Lreal | Larrow _ ->
+ Error.not_yet
+ (error_msg
+ quantif
+ "@[non integer variable %a@]"
+ Printer.pp_logic_var v)
+ in
+ Logic_var.Set.add v s
+ )
+ Logic_var.Set.empty
+ bounded_vars
+ in
+ {
+ quantif;
+ bounded_vars;
+ rev_order = [];
+ guards = Logic_var.Map.empty;
+ linked_upper_bounds = Logic_var.Map.empty;
+ }
+
+ let get_bounded_var t ctxt =
+ let rec aux t =
+ match t.term_node with
+ | TLogic_coerce(_, t) -> aux t
+ | TLval(TVar lv, TNoOffset) when Logic_var.Set.mem lv ctxt.bounded_vars ->
+ Some lv
+ | _ -> None
+ in
+ aux t
+
+ let has_unguarded_bounded_vars ctxt =
+ not (Logic_var.Set.is_empty ctxt.bounded_vars)
+
+ (** Pretty printer for a guard, represented by a tuple
+ [(term, relation, logic_var, relation, term)]. *)
+ let pp_guard fmt (t1, r1, lv, r2, t2) =
+ Format.fprintf
+ fmt
+ "@[%a %a %a %a %a@]"
+ Printer.pp_term t1
+ Printer.pp_relation r1
+ Printer.pp_logic_var lv
+ Printer.pp_relation r2
+ Printer.pp_term t2
+
+ (** Pretty printer for a lower bound, represented by the tuple
+ [(term, relation, logic_var)]. *)
+ let pp_lbound fmt (t, r, lv) =
+ Format.fprintf
+ fmt
+ "@[%a %a %a@]"
+ Printer.pp_term t
+ Printer.pp_relation r
+ Printer.pp_logic_var lv
+
+ (** Pretty printer for a bound between two quantified variables,
+ represented by the tuple [(logic_var, relation, logic_var)]. *)
+ let pp_linked_bound fmt (lv1, r, lv2) =
+ Format.fprintf
+ fmt
+ "@[%a %a %a@]"
+ Printer.pp_logic_var lv1
+ Printer.pp_relation r
+ Printer.pp_logic_var lv2
+
+ let add_lower_bound t r lv ctxt =
+ match Logic_var.Map.find_opt lv ctxt.guards with
+ | None ->
+ { ctxt with
+ guards = Logic_var.Map.add lv (t, r, None) ctxt.guards; }
+ | Some (t', r', None) ->
+ let msg =
+ Format.asprintf
+ "@[found existing lower bound %a@ when processing %a@ \
+ in quantification@ %a@]"
+ pp_lbound (t', r', lv)
+ pp_lbound (t, r, lv)
+ Printer.pp_predicate ctxt.quantif
+ in
+ Error.untypable msg
+ | Some (t1', r1', Some (r2', t2')) ->
+ let msg =
+ Format.asprintf
+ "@[found existing guard %a@ when processing %a@ \
+ in quantification@ %a@]"
+ pp_guard (t1', r1', lv, r2', t2')
+ pp_lbound (t, r, lv)
+ Printer.pp_predicate ctxt.quantif
+ in
+ Error.untypable msg
+
+ let add_linked_upper_bound lv1 r lv2 ctxt =
+ if Logic_var.Map.mem lv1 ctxt.guards then begin
+ { ctxt with
+ linked_upper_bounds =
+ Logic_var.Map.add lv2
+ (lv1, r)
+ ctxt.linked_upper_bounds; }
+ end else
+ let msg=
+ Format.asprintf
+ "@[missing lower bound for %a@ when processing the linked upper \
+ bound %a@ in quantification@ %a@]"
+ Printer.pp_logic_var lv1
+ pp_linked_bound (lv1, r, lv2)
+ Printer.pp_predicate ctxt.quantif
+ in
+ Error.untypable msg
+
+ let add_upper_bound lv r t ctxt =
+ (* Select the strictest relation between [r1] and [r2], with both relations
+ being either [Rlt] or [Rle]. *)
+ let strictest_relation r1 r2 =
+ match r1, r2 with
+ | (Rlt | Rle), Rlt | Rlt, Rle -> Rlt
+ | Rle, Rle -> Rle
+ | _, _ ->
+ Options.fatal
+ "invalid relations %a and %a in quantification %a"
+ Printer.pp_relation r1
+ Printer.pp_relation r2
+ Printer.pp_predicate ctxt.quantif
+ in
+ (* Replace the guard for [lv] to add the upper bound [lv r t], and
+ recursively walk the bounds linked to [lv] to also add upper bounds. *)
+ let rec replace_guard lv r t ctxt =
+ try
+ let lower_bound_t, lower_bound_r, _ =
+ Logic_var.Map.find lv ctxt.guards
+ in
+ let ctxt =
+ { ctxt with
+ guards =
+ Logic_var.Map.add
+ lv
+ (lower_bound_t, lower_bound_r, Some (r, t))
+ ctxt.guards; }
+ in
+ let ctxt =
+ { ctxt with
+ bounded_vars = Logic_var.Set.remove lv ctxt.bounded_vars; }
+ in
+ let need_upper_bound =
+ Logic_var.Map.find_opt lv ctxt.linked_upper_bounds
+ in
+ let ctxt =
+ match need_upper_bound with
+ | Some (lv', r') ->
+ let ctxt =
+ { ctxt with
+ linked_upper_bounds =
+ Logic_var.Map.remove lv ctxt.linked_upper_bounds; }
+ in
+ replace_guard lv' (strictest_relation r r') t ctxt
+ | None -> ctxt
+ in
+ { ctxt with rev_order = lv :: ctxt.rev_order }
+ with Not_found ->
+ Error.untypable
+ (error_msg ctxt.quantif
+ "@[missing lower bound for %a@]"
+ Printer.pp_logic_var lv)
+ in
+ replace_guard lv r t ctxt
+
+ let check_validity ctxt =
+ if not (Logic_var.Map.is_empty ctxt.linked_upper_bounds) then
+ let msg =
+ let iter_keys f map_seq =
+ Seq.iter
+ (fun (key, _) -> f key)
+ map_seq
+ in
+ Format.asprintf
+ "@[missing upper bound%s for %a@ in quantification@ %a@]"
+ (if Logic_var.Map.cardinal ctxt.linked_upper_bounds = 1 then ""
+ else "s")
+ (Pretty_utils.pp_iter
+ ~sep:", "
+ iter_keys
+ Printer.pp_logic_var)
+ (Logic_var.Map.to_seq ctxt.linked_upper_bounds)
+ Printer.pp_predicate ctxt.quantif
+ in
+ Error.untypable msg
+ else if not (Logic_var.Set.is_empty ctxt.bounded_vars) then
+ let msg =
+ Format.asprintf
+ "@[missing lower bound%s for %a@ in quantification@ %a@]"
+ (if Logic_var.Set.cardinal ctxt.bounded_vars = 1 then "" else "s")
+ (Pretty_utils.pp_iter
+ ~sep:", "
+ Logic_var.Set.iter
+ Printer.pp_logic_var)
+ ctxt.bounded_vars
+ Printer.pp_predicate ctxt.quantif
+ in
+ Error.untypable msg
+
+ let retrieve_guards ctxt =
+ List.fold_left
+ (fun acc lv ->
+ match Logic_var.Map.find_opt lv ctxt.guards with
+ | Some (t1, r1, Some (r2, t2)) ->
+ (t1, r1, lv, r2, t2) :: acc
+
+ (* The error cases should not occur if the traversal of the
+ quantification was completed and [check_validity] was called
+ successfully. *)
+ | Some (_, _, None) ->
+ Options.fatal
+ "Missing upper bound when trying to retrieve the guard for %a"
+ Printer.pp_logic_var lv
+ | None -> Options.fatal "Missing guard for %a" Printer.pp_logic_var lv
+ )
+ []
+ ctxt.rev_order
+
+ let raise_error msg ctxt =
+ let msg2 =
+ Format.asprintf "@[ in quantification@ %a@]"
+ Printer.pp_predicate ctxt.quantif
+ in
+ Error.untypable (msg ^ msg2)
+
+ let raise_error_invalid_pred ?(warn_rel=false) p ctxt =
+ (* Extract the set of variables that have another variable for upper bound.
+ They will be considered valid for the purpose of the error message, ie.
+ if we have the relation [0 < i < j] with [0 < i] as an incomplete guard
+ and [i < j] as a linked upper bound, then the error is about [j] not
+ having an upper bound, not about [i]. *)
+ let linked_upper_bounds =
+ Logic_var.Map.fold
+ (fun _ (lv, _) acc -> Logic_var.Set.add lv acc)
+ ctxt.linked_upper_bounds
+ Logic_var.Set.empty
+ in
+
+ let missing_guards, missing_upper_bounds =
+ Logic_var.Set.fold
+ (fun lv (missing_guards, missing_upper_bounds) ->
+ match Logic_var.Map.find_opt lv ctxt.guards with
+ | Some (_, _, None)
+ when not (Logic_var.Set.mem lv linked_upper_bounds) ->
+ (* A variable with an incomplete constraint and without a linked
+ upper bound has a missing upper bound. *)
+ missing_guards, lv :: missing_upper_bounds
+ | None ->
+ (* A variable without a constraint has a missing guard. *)
+ lv :: missing_guards, missing_upper_bounds
+ | _ ->
+ (* Otherwise the variable either has a complete constraint, or an
+ incomplete constraint but with a linked upper bound. *)
+ missing_guards, missing_upper_bounds)
+ ctxt.bounded_vars
+ ([], [])
+ in
+
+ let msg =
+ Format.asprintf
+ "@[invalid guard %a@ in quantification@ %a.@ \
+ %a@,%a@ \
+ %t@]"
+ Printer.pp_predicate p Printer.pp_predicate ctxt.quantif
+ (Pretty_utils.pp_list
+ ~pre:"@[Missing guard for "
+ ~sep:",@ "
+ ~suf:".@]"
+ Printer.pp_logic_var)
+ (List.rev missing_guards)
+ (Pretty_utils.pp_list
+ ~pre:"@[Missing upper bound for "
+ ~sep:",@ "
+ ~suf:".@]"
+ Printer.pp_logic_var)
+ (List.rev missing_upper_bounds)
+ (fun fmt ->
+ if warn_rel then
+ Format.fprintf fmt
+ "@[Only %a and %a are allowed to guard quantifier variables@]"
+ Printer.pp_relation Rlt Printer.pp_relation Rle)
+ in
+ Error.untypable msg
+
+end
+
+(******************************************************************************)
+(** Syntactical analysis *)
+(******************************************************************************)
+
+(** [extract_constraint ctxt t1 r t2] populates the quantification context
+ [ctxt] with the constraint [t1 r t2], either adding a lower bound if [t2] is
+ a bounded variable or adding an upper bound if [t1] is a bounded variable.
+ @raises Typing_error if no constraint can be extracted or if the constraint
+ is invalid (no bounded variable in [t1] or [t2] for instance). *)
+let extract_constraint ctxt t1 r t2 =
+ (* Return the logic var corresponding to the given term or [None] if the term
+ is not a variable ([TLval(TVar _, TNoOffset)]). *)
+ let rec _get_logic_var_opt t =
+ match t.term_node with
+ | TLogic_coerce(_, t) -> _get_logic_var_opt t
+ | TLval(TVar x, TNoOffset) -> Some x
+ | _ -> None
+ in
+ (* Process the given relation *)
+ let lv1 = Constraints.get_bounded_var t1 ctxt in
+ let lv2 = Constraints.get_bounded_var t2 ctxt in
+ match lv1, lv2 with
+ | None, Some lv2 -> (* t1 value, t2 variable: store lower bound *)
+ Constraints.add_lower_bound t1 r lv2 ctxt
+ | Some lv1, None -> (* t1 variable, t2 value: store upper bound *)
+ Constraints.add_upper_bound lv1 r t2 ctxt
+ | Some lv1, Some lv2 ->
+ (* t1 variable, t2 variable: store link between t1 and t2 *)
+ let ctxt = Constraints.add_linked_upper_bound lv1 r lv2 ctxt in
+ Constraints.add_lower_bound t1 r lv2 ctxt
+ | None, None -> (* t1 value, t2 value: error *)
+ let msg =
+ Format.asprintf
+ "@[invalid constraint %a %a %a, both operands are constants or \
+ already bounded@]"
+ Printer.pp_term t1
+ Printer.pp_relation r
+ Printer.pp_term t2
+ in
+ Constraints.raise_error msg ctxt
+
+(** [visit_quantif_relations ~is_forall ctxt p] traverses the predicate [p] of
+ the quantification being analyzed in the context [ctxt] from left to right
+ as long as the predicate is [Pimplies], [Pand] or [Prel(Rlt |Â Rle)], and
+ calls [extract_constraint] on each relation [Rlt] or [Rle] it encounters
+ until all the guards of the quantification have been found or the predicate
+ is finished. If [is_forall] is [true] then the predicate being traversed is
+ a universal quantification, otherwise it is an existential quantification.
+ The function returns a tuple [ctxt, goal_opt] where [ctxt] is the
+ quantification context and [goal_opt] is either [None] if the goal of the
+ quantification has not been found yet or [Some goal] if [goal] is the
+ predicate corresponding to the goal of the quantification.
+ @raises Typing_error if the predicate contains something other than
+ [Pimplies], [Pand] or [Prel] with a relation that is neither [Rlt] nor
+ [Rle]. *)
+let rec visit_quantif_relations ~is_forall ctxt p =
+ match p.pred_content with
+ | Pimplies(lhs, rhs) ->
+ let ctxt, _ = visit_quantif_relations ~is_forall ctxt lhs in
+ if is_forall then begin
+ if Constraints.has_unguarded_bounded_vars ctxt then
+ visit_quantif_relations ~is_forall ctxt rhs
+ else
+ ctxt, Some rhs
+ end else
+ let msg =
+ Format.asprintf
+ "@[invalid quantification guard, expecting '%s' to continue@ \
+ bounding variables,@ found '%s'@]"
+ (if Kernel.Unicode.get () then Utf8_logic.conj else "&&")
+ (if Kernel.Unicode.get () then Utf8_logic.implies else "==>")
+ in
+ Constraints.raise_error msg ctxt
+ | Pand(lhs, rhs) ->
+ let ctxt, _ = visit_quantif_relations ~is_forall ctxt lhs in
+ if Constraints.has_unguarded_bounded_vars ctxt then
+ visit_quantif_relations ~is_forall ctxt rhs
+ else if not is_forall then
+ ctxt, Some rhs
+ else
+ let msg =
+ Format.asprintf
+ "@[invalid quantification predicate, expecting '%s' to@ \
+ separate the hypotheses from the goal, found '%s'@]"
+ (if Kernel.Unicode.get () then Utf8_logic.implies else "==>")
+ (if Kernel.Unicode.get () then Utf8_logic.conj else "&&")
+ in
+ Constraints.raise_error msg ctxt
+ | Prel((Rlt | Rle) as r, t1, t2) ->
+ let ctxt = extract_constraint ctxt t1 r t2 in
+ ctxt, None
+ | Prel _ ->
+ Constraints.raise_error_invalid_pred ~warn_rel:true p ctxt
+ | _ ->
+ Constraints.raise_error_invalid_pred p ctxt
+
+(** [compute_quantif_guards ~is_forall quantif bounded_vars p] computes the
+ guards for the bounded variables [bounded_vars] of the quantification
+ [quantif] from the predicate [p]. If [is_forall] is [true] then [quantif] is
+ a universal quantification, otherwise [quantif] is an existential
+ quantification.
+ The function returns the list of guards for the variables and the goal
+ predicate of the quantification. *)
+let compute_quantif_guards ~is_forall quantif bounded_vars p =
+ (* Traverse the predicate of the quantification to extract the guards of the
+ bounded variables. *)
+ let ctxt = Constraints.empty quantif bounded_vars in
+ let ctxt, goal = visit_quantif_relations ~is_forall ctxt p in
+ (* Check the validity of the result of the traversal. *)
+ Constraints.check_validity ctxt;
+ if Option.is_none goal then
+ let msg =
+ Format.asprintf
+ "@[no goal found in quantification@ %a@]"
+ Printer.pp_predicate quantif
+ in
+ Error.untypable msg
+ else
+ (* Traversal is valid, the guards and the goal can be retrieved and
+ returned. *)
+ let guards = Constraints.retrieve_guards ctxt in
+ let goal = Option.get goal in
+ guards, goal
+
+(******************************************************************************)
+(** Type intersection *)
+(******************************************************************************)
+
+(* It could happen that the bounds provided for a quantifier [lv] are bigger
+ than its type. [bounds_for_small_type] 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 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 () = Typing.compute_quantif_guards_ref := compute_quantif_guards
+
+(** Take 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 *)
+let normalize_guard ~loc (t1, rel1, lv, rel2, t2) =
+ let t_plus_one t =
+ let tone = Cil.lone ~loc () in
+ Logic_const.term ~loc (TBinOp(PlusA, t, tone)) Linteger
+ in
+ (* this function only manipulate guards that were already
+ processed by compute_quantif_guards, which only outputs
+ guards with the constructors Rlt and Rle*)
+ let t1 = match rel1 with
+ | Rlt ->
+ t_plus_one t1
+ | Rle ->
+ t1
+ | Rgt | Rge | Req | Rneq ->
+ assert false
+ in
+ let t2 = match rel2 with
+ | Rlt ->
+ t2
+ | Rle ->
+ t_plus_one 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
diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.mli b/src/plugins/e-acsl/src/analyses/bound_variables.mli
new file mode 100644
index 0000000000000000000000000000000000000000..bd32dc7b576334137289266931c9fb51f6d99257
--- /dev/null
+++ b/src/plugins/e-acsl/src/analyses/bound_variables.mli
@@ -0,0 +1,42 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-2020 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+open Cil_datatype
+
+
+val compute_guards: location -> is_forall:bool -> predicate -> Logic_var.t list -> predicate -> unit
+(** Take a predicate starting with a quantifier and store the scope of its variable *)
+
+val get_preprocessed_quantifier: predicate -> (term * logic_var * term) list * predicate
+(** @return the preprocessed of a quantified predicate
+ the [(term * logic_var * term) list] is the list of all the quantified variables
+ along with their syntactic guards, and the [predicate] is the goal: the original
+ predicate with all the quantifiers removed *)
+
+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 clear_guards : unit -> unit
+(** Clear the table of guard conditions for quantified variables *)
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index ec1f3a3da2641700bb4a10d49969c8da2bd7ce71..1f817c3d3457620a9c0d64458cab9a5a41d0fa4e 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -231,6 +231,17 @@ let rec interv_of_typ ty = match Cil.unrollType ty with
| TNamed _ ->
assert false
+let rec extended_interv_of_typ ty = match interv_of_typ ty with
+ | Ival iv ->
+ let l,u = Ival.min_int iv, Ival.max_int iv in
+ let u = match u with
+ | Some u -> Some (Integer.add u Integer.one)
+ | None -> None
+ in
+ Ival (Ival.inject_range l u);
+ | Rational | Real | Nan | Float (_,_) as i
+ -> i
+
(* Compute the interval of the extended quantifier \sum, \product and \numof.
[lbd_ival] is the interval of the lambda term, [k_ival] is the interval of the
quantifier and [name] is the identifier of the extended quantifier (\sum,
diff --git a/src/plugins/e-acsl/src/analyses/interval.mli b/src/plugins/e-acsl/src/analyses/interval.mli
index d2b95afa0d1f52943af02ee78e2378fe6096b415..a06fa4145334c5b5670925a1bd116e3281573acb 100644
--- a/src/plugins/e-acsl/src/analyses/interval.mli
+++ b/src/plugins/e-acsl/src/analyses/interval.mli
@@ -79,6 +79,13 @@ val interv_of_typ: Cil_types.typ -> t
@raise Is_a_real if the given type is a float type.
@raise Not_a_number if the given type does not represent any number. *)
+val extended_interv_of_typ: Cil_types.typ -> t
+(** @return the interval [n..m+1] when interv_of_typ returns [n..m].
+ It is in particular useful for computing bounds of quantified variables.
+ @raise Is_a_real if the given type is a float type.
+ @raise Not_a_number if the given type does not represent any number. *)
+
+
(* ************************************************************************** *)
(** {3 Environment for interval computations} *)
(* ************************************************************************** *)
diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index 24775347413b7975db7d758f4c61ae1adcdf6b5a..dce4af58bf9d22d69fa087552a06223d74ab2865 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -445,7 +445,7 @@ let transfer ~from env = match from.env_stack, env.env_stack with
type where = Before | Middle | After
let pop_and_get ?(split=false) env stmt ~global_clear where =
let split = split && stmt.labels = [] in
- (* Options.feedback "pop_and_get from %a (%b)" Printer.pp_stmt stmt split;*)
+ (* Options.feedback "pop_and_get from %a (%b)" Printer.pp_stmt stmt split; *)
let local_env, tl = top env in
let clear =
if global_clear then begin
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index 44a7f433c60d80379ba5de293f8730efd9dcccb6..dae5dc6c27e651ab6cffeafd718d4619878bb54d 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -831,6 +831,7 @@ let reset_all ast =
Logic_functions.reset ();
Literal_strings.reset ();
Global_observer.reset ();
+ Bound_variables.clear_guards ();
Typing.clear ();
(* reset some kernel states: *)
(* reset the CFG that has been heavily modified by the code generation step *)
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index c6d6e726ba7e5f183f42551b3bba4e57472811ad..eba5a6884df10a98ab4fa6cb95c70f4f48de59fc 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -200,75 +200,15 @@ let handle_annotations env kf stmt =
(**************************************************************************)
(**************************** Nested loops ********************************)
(**************************************************************************)
-
-(* It could happen that the bounds provided for a quantifier [lv] are bigger
- than its type. [bounds_for_small_type] 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 bounds_for_small_type ~loc (t1, lv, t2) =
- match lv.lv_type with
- | Ltype _ | Lvar _ | Lreal | Larrow _ ->
- Options.abort "quantification over non-integer type is not part of E-ACSL"
-
- | 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.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 (Rle, lv_term, guard_upper) in
- let guard = Logic_const.pand ~loc (guard_lower, guard_upper) in
- t1, t2, Some guard
-
let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
let term_to_exp = !term_to_exp_ref in
match lscope_vars with
| [] ->
mk_innermost_block env
| Lscope.Lvs_quantif(t1, rel1, logic_x, rel2, t2) :: lscope_vars' ->
- let t1, t2, guard_for_small_type_opt =
- bounds_for_small_type ~loc (t1, logic_x, t2)
- in
+ assert (rel1 == Rle && rel2 == Rlt);
+ Typing.type_term ~use_gmp_opt:false t1;
+ Typing.type_term ~use_gmp_opt:false t2;
let ctx =
let ty1 = Typing.get_number_ty t1 in
let ty2 = Typing.get_number_ty t2 in
@@ -286,41 +226,14 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
ty;
res
in
- let t1 = match rel1 with
- | Rlt ->
- let t = t_plus_one t1 in
- Typing.type_term ~use_gmp_opt:false ~ctx t;
- t
- | Rle ->
- t1
- | Rgt | Rge | Req | Rneq ->
- assert false
- in
- let t2_one, bop2 = match rel2 with
- | Rlt ->
- t2, Lt
- | Rle ->
- (* we increment the loop counter one more time (at the end of the
- loop). Thus to prevent overflow, check the type of [t2+1]
- instead of [t2]. *)
- t_plus_one t2, Le
- | Rgt | Rge | Req | Rneq ->
- assert false
- in
- Typing.type_term ~use_gmp_opt:false ~ctx t2_one;
- let ctx_one =
- let ty1 = Typing.get_number_ty t1 in
- let ty2 = Typing.get_number_ty t2_one in
- Typing.join ty1 ty2
- in
let ty =
- try Typing.typ_of_number_ty ctx_one
+ try Typing.typ_of_number_ty ctx
with Typing.Not_a_number -> assert false
in
(* loop counter corresponding to the quantified variable *)
let var_x, x, env = Env.Logic_binding.add ~ty env kf logic_x in
let lv_x = var var_x in
- let env = match ctx_one with
+ let env = match ctx with
| Typing.C_integer _ -> env
| Typing.Gmpz -> Env.add_stmt env kf (Gmp.init ~loc x)
| Typing.(C_float _ | Rational | Real | Nan) -> assert false
@@ -337,13 +250,22 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
~global_clear:false
Env.Middle
in
- (* generate the guard [x bop t2] *)
+ (* generate the guard [x < t2] *)
let block_to_stmt b = Smart_stmt.block_stmt b in
let tlv = Logic_const.tvar ~loc logic_x in
+ (* if [t2] is of the form [t2'+1], generate the guard [x <= t2']
+ to avoid the extra addition (relevant when computing with GMP) *)
let guard =
- (* must copy [t2] to force being typed again *)
- Logic_const.term ~loc
- (TBinOp(bop2, tlv, { t2 with term_node = t2.term_node } )) Linteger
+ match t2.term_node with
+ | TBinOp (PlusA, t2_minus_one, {term_node = TConst(Integer (n, _))}) when Integer.is_one n ->
+ Logic_const.term ~loc
+ (TBinOp(Le, tlv, { t2_minus_one with term_node = t2_minus_one.term_node }))
+ Linteger
+ | _ ->
+ (* must copy [t2] to force it being typed again *)
+ Logic_const.term ~loc
+ (TBinOp(Lt, tlv, { t2 with term_node = t2.term_node } ))
+ Linteger
in
Typing.type_term ~use_gmp_opt:false ~ctx:Typing.c_int guard;
let guard_exp, env = term_to_exp kf (Env.push env) guard in
@@ -361,7 +283,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
let guard = block_to_stmt guard_blk in
(* increment the loop counter [x++];
previous typing ensures that [x++] fits type [ty] *)
- let tlv_one = t_plus_one ~ty:ctx_one tlv in
+ let tlv_one = t_plus_one ~ty:ctx tlv in
let incr, env = term_to_exp kf (Env.push env) tlv_one in
let next_blk, env = Env.pop_and_get
env
@@ -371,6 +293,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
in
(* generate the whole loop *)
let next = block_to_stmt next_blk in
+ let guard_for_small_type_opt = Bound_variables.get_guard_for_small_type logic_x in
let stmts, env = match guard_for_small_type_opt with
| None ->
guard :: body @ [ next ], env
diff --git a/src/plugins/e-acsl/src/code_generator/quantif.ml b/src/plugins/e-acsl/src/code_generator/quantif.ml
index 2e95c2c5699ccc1b585919ac6bbf0703bb3684b0..4ca10accdffd58208f41e97c7de496bc134c0127 100644
--- a/src/plugins/e-acsl/src/code_generator/quantif.ml
+++ b/src/plugins/e-acsl/src/code_generator/quantif.ml
@@ -22,526 +22,15 @@
open Cil_types
open Cil
-open Cil_datatype
(** Forward reference for [Translate.predicate_to_exp]. *)
let predicate_to_exp_ref
: (kernel_function -> Env.t -> predicate -> exp * Env.t) ref
= Extlib.mk_fun "predicate_to_exp_ref"
-(** [error_msg quantif msg pp x] creates an error message from the string [msg]
- containing the value [x] pretty-printed by [pp] and the predicate [quantif]
- pretty-printed. *)
-let error_msg quantif msg pp x =
- let msg1 = Format.asprintf msg pp x in
- let msg2 =
- Format.asprintf "@[ in quantification@ %a@]"
- Printer.pp_predicate quantif
- in
- msg1 ^ msg2
-
-(** Helper module to process the constraints in the quantification and extract
- guards for the quantified variables. *)
-module Constraints: sig
- (** Context type manipulated by the functions of the module. *)
- type t
-
- (** [empty quantif bounded_vars] creates an empty context from a
- quantification predicate and the list of bounded variables for the
- predicate. *)
- val empty: predicate -> logic_var list -> t
-
- (** [get_bounded_var ctxt t] returns the logic var corresponding to the given
- term if the term is a variable ([TLval(Tvar _, TNoOffset)]) that is a
- bounded variable for the quantification being processed, or [None]
- otherwise. *)
- val get_bounded_var: term -> t -> logic_var option
-
- (** [has_unguarded_bounded_vars ctxt] returns true iff some bounded variables
- in [ctxt] do not have a guard extracted from the quantification
- predicate. *)
- val has_unguarded_bounded_vars: t -> bool
-
- (** [add_lower_bound ctxt t r lv] adds the lower bound [t r lv] to the list
- of guards for the quantification.
- @raises Typing_error if a lower bound already exists for [lv]. *)
- val add_lower_bound: term -> relation -> logic_var -> t -> t
-
- (** [add_linked_upper_bound ctxt lv1 r lv2] adds a link between two bounded
- variables with still incomplete guards. [lv1] should already have at least
- a lower bound.
- @raises Typing_error if [lv1] do not have an existing lower bound. *)
- val add_linked_upper_bound: logic_var -> relation -> logic_var -> t -> t
-
- (** [add_upper_bound ctxt lv r t] adds the upper bound [lv r t] to the list of
- guards for the quantification.
- For each existing linked relation [lv' r' lv], also adds the upper bound
- [lv' r'' t] to the list of guards, with [r''] being the strictest relation
- between [r]Â and [r'].
- @raises Typing_error if either [lv] or [lv'] does not have an existing
- lower bound. *)
- val add_upper_bound: logic_var -> relation -> term -> t -> t
-
- (** [check_validity ctxt] checks the validity of the quantification after
- processing.
- @raises Typing_error if some bound (lower or upper) cound not be extracted
- from the quantification for each bounded variable. *)
- val check_validity: t -> unit
-
- (** [retrieve_guards ctxt] returns the list of guards for the bounded
- variables of the quantification, in the order in which they must be
- generated, ie. if [j] depends on [i] then the guard for [i] will be before
- the guard for [j] in the list.
- [check_validity ctxt] must have been called before calling
- [retrieve_guards]. *)
- val retrieve_guards: t -> (term * relation * logic_var * relation * term) list
-
- (** [raise_error ctxt msg] raises a [Typing_error] exception with the given
- message after appending the quantification from the context. *)
- val raise_error: string -> t -> 'a
-
- (** [error_invalid_pred ?warn_rel ctxt p] raises a [Typing_error] exception
- with a message indicating that the predicate [p] is not valid in the
- quantification. Depending on the state of [ctxt], more information about
- missing bounds is added to the message. If [warn_rel] is [true], then a
- reminder that only [Rle] and [Rlt] are allowed to guard quantified
- variables is added to the message. *)
- val raise_error_invalid_pred: ?warn_rel:bool -> predicate -> t -> 'a
-end = struct
- type t = {
- (** Quantification predicate being analyzed. *)
- quantif: predicate;
- (** Variables of the quantification that still need guards. *)
- bounded_vars: Logic_var.Set.t;
- (** Bounded variables list in reverse order in which they must be
- generated. *)
- rev_order: Logic_var.t list;
- (** Table associating a bounded variable with its guard. *)
- guards: (term * relation * (relation * term) option) Logic_var.Map.t;
- (** Table associating a bounded variable with a relation with another
- bounded variable. *)
- linked_upper_bounds: (logic_var * relation) Logic_var.Map.t;
- }
-
- let empty quantif bounded_vars =
- (* Check that the bounded vars have integer type and store them in a set. *)
- let bounded_vars =
- List.fold_left
- (fun s v ->
- let v =
- match v.lv_type with
- | Ctype ty when isIntegralType ty -> v
- | Linteger -> v
- | Ltype _ as ty when Logic_const.is_boolean_type ty -> v
- | Ctype _ | Ltype _ | Lvar _ | Lreal | Larrow _ ->
- Error.not_yet
- (error_msg
- quantif
- "@[non integer variable %a@]"
- Printer.pp_logic_var v)
- in
- Logic_var.Set.add v s
- )
- Logic_var.Set.empty
- bounded_vars
- in
- {
- quantif;
- bounded_vars;
- rev_order = [];
- guards = Logic_var.Map.empty;
- linked_upper_bounds = Logic_var.Map.empty;
- }
-
- let get_bounded_var t ctxt =
- let rec aux t =
- match t.term_node with
- | TLogic_coerce(_, t) -> aux t
- | TLval(TVar lv, TNoOffset) when Logic_var.Set.mem lv ctxt.bounded_vars ->
- Some lv
- | _ -> None
- in
- aux t
-
- let has_unguarded_bounded_vars ctxt =
- not (Logic_var.Set.is_empty ctxt.bounded_vars)
-
- (** Pretty printer for a guard, represented by a tuple
- [(term, relation, logic_var, relation, term)]. *)
- let pp_guard fmt (t1, r1, lv, r2, t2) =
- Format.fprintf
- fmt
- "@[%a %a %a %a %a@]"
- Printer.pp_term t1
- Printer.pp_relation r1
- Printer.pp_logic_var lv
- Printer.pp_relation r2
- Printer.pp_term t2
-
- (** Pretty printer for a lower bound, represented by the tuple
- [(term, relation, logic_var)]. *)
- let pp_lbound fmt (t, r, lv) =
- Format.fprintf
- fmt
- "@[%a %a %a@]"
- Printer.pp_term t
- Printer.pp_relation r
- Printer.pp_logic_var lv
-
- (** Pretty printer for a bound between two quantified variables,
- represented by the tuple [(logic_var, relation, logic_var)]. *)
- let pp_linked_bound fmt (lv1, r, lv2) =
- Format.fprintf
- fmt
- "@[%a %a %a@]"
- Printer.pp_logic_var lv1
- Printer.pp_relation r
- Printer.pp_logic_var lv2
-
- let add_lower_bound t r lv ctxt =
- match Logic_var.Map.find_opt lv ctxt.guards with
- | None ->
- { ctxt with
- guards = Logic_var.Map.add lv (t, r, None) ctxt.guards; }
- | Some (t', r', None) ->
- let msg =
- Format.asprintf
- "@[found existing lower bound %a@ when processing %a@ \
- in quantification@ %a@]"
- pp_lbound (t', r', lv)
- pp_lbound (t, r, lv)
- Printer.pp_predicate ctxt.quantif
- in
- Error.untypable msg
- | Some (t1', r1', Some (r2', t2')) ->
- let msg =
- Format.asprintf
- "@[found existing guard %a@ when processing %a@ \
- in quantification@ %a@]"
- pp_guard (t1', r1', lv, r2', t2')
- pp_lbound (t, r, lv)
- Printer.pp_predicate ctxt.quantif
- in
- Error.untypable msg
-
- let add_linked_upper_bound lv1 r lv2 ctxt =
- if Logic_var.Map.mem lv1 ctxt.guards then begin
- { ctxt with
- linked_upper_bounds =
- Logic_var.Map.add lv2
- (lv1, r)
- ctxt.linked_upper_bounds; }
- end else
- let msg=
- Format.asprintf
- "@[missing lower bound for %a@ when processing the linked upper \
- bound %a@ in quantification@ %a@]"
- Printer.pp_logic_var lv1
- pp_linked_bound (lv1, r, lv2)
- Printer.pp_predicate ctxt.quantif
- in
- Error.untypable msg
-
- let add_upper_bound lv r t ctxt =
- (* Select the strictest relation between [r1] and [r2], with both relations
- being either [Rlt] or [Rle]. *)
- let strictest_relation r1 r2 =
- match r1, r2 with
- | (Rlt | Rle), Rlt | Rlt, Rle -> Rlt
- | Rle, Rle -> Rle
- | _, _ ->
- Options.fatal
- "invalid relations %a and %a in quantification %a"
- Printer.pp_relation r1
- Printer.pp_relation r2
- Printer.pp_predicate ctxt.quantif
- in
- (* Replace the guard for [lv] to add the upper bound [lv r t], and
- recursively walk the bounds linked to [lv] to also add upper bounds. *)
- let rec replace_guard lv r t ctxt =
- try
- let lower_bound_t, lower_bound_r, _ =
- Logic_var.Map.find lv ctxt.guards
- in
- let ctxt =
- { ctxt with
- guards =
- Logic_var.Map.add
- lv
- (lower_bound_t, lower_bound_r, Some (r, t))
- ctxt.guards; }
- in
- let ctxt =
- { ctxt with
- bounded_vars = Logic_var.Set.remove lv ctxt.bounded_vars; }
- in
- let need_upper_bound =
- Logic_var.Map.find_opt lv ctxt.linked_upper_bounds
- in
- let ctxt =
- match need_upper_bound with
- | Some (lv', r') ->
- let ctxt =
- { ctxt with
- linked_upper_bounds =
- Logic_var.Map.remove lv ctxt.linked_upper_bounds; }
- in
- replace_guard lv' (strictest_relation r r') t ctxt
- | None -> ctxt
- in
- { ctxt with rev_order = lv :: ctxt.rev_order }
- with Not_found ->
- Error.untypable
- (error_msg ctxt.quantif
- "@[missing lower bound for %a@]"
- Printer.pp_logic_var lv)
- in
- replace_guard lv r t ctxt
-
- let check_validity ctxt =
- if not (Logic_var.Map.is_empty ctxt.linked_upper_bounds) then
- let msg =
- let iter_keys f map_seq =
- Seq.iter
- (fun (key, _) -> f key)
- map_seq
- in
- Format.asprintf
- "@[missing upper bound%s for %a@ in quantification@ %a@]"
- (if Logic_var.Map.cardinal ctxt.linked_upper_bounds = 1 then ""
- else "s")
- (Pretty_utils.pp_iter
- ~sep:", "
- iter_keys
- Printer.pp_logic_var)
- (Logic_var.Map.to_seq ctxt.linked_upper_bounds)
- Printer.pp_predicate ctxt.quantif
- in
- Error.untypable msg
- else if not (Logic_var.Set.is_empty ctxt.bounded_vars) then
- let msg =
- Format.asprintf
- "@[missing lower bound%s for %a@ in quantification@ %a@]"
- (if Logic_var.Set.cardinal ctxt.bounded_vars = 1 then "" else "s")
- (Pretty_utils.pp_iter
- ~sep:", "
- Logic_var.Set.iter
- Printer.pp_logic_var)
- ctxt.bounded_vars
- Printer.pp_predicate ctxt.quantif
- in
- Error.untypable msg
-
- let retrieve_guards ctxt =
- List.fold_left
- (fun acc lv ->
- match Logic_var.Map.find_opt lv ctxt.guards with
- | Some (t1, r1, Some (r2, t2)) ->
- (t1, r1, lv, r2, t2) :: acc
-
- (* The error cases should not occur if the traversal of the
- quantification was completed and [check_validity] was called
- successfully. *)
- | Some (_, _, None) ->
- Options.fatal
- "Missing upper bound when trying to retrieve the guard for %a"
- Printer.pp_logic_var lv
- | None -> Options.fatal "Missing guard for %a" Printer.pp_logic_var lv
- )
- []
- ctxt.rev_order
-
- let raise_error msg ctxt =
- let msg2 =
- Format.asprintf "@[ in quantification@ %a@]"
- Printer.pp_predicate ctxt.quantif
- in
- Error.untypable (msg ^ msg2)
-
- let raise_error_invalid_pred ?(warn_rel=false) p ctxt =
- (* Extract the set of variables that have another variable for upper bound.
- They will be considered valid for the purpose of the error message, ie.
- if we have the relation [0 < i < j] with [0 < i] as an incomplete guard
- and [i < j] as a linked upper bound, then the error is about [j] not
- having an upper bound, not about [i]. *)
- let linked_upper_bounds =
- Logic_var.Map.fold
- (fun _ (lv, _) acc -> Logic_var.Set.add lv acc)
- ctxt.linked_upper_bounds
- Logic_var.Set.empty
- in
-
- let missing_guards, missing_upper_bounds =
- Logic_var.Set.fold
- (fun lv (missing_guards, missing_upper_bounds) ->
- match Logic_var.Map.find_opt lv ctxt.guards with
- | Some (_, _, None)
- when not (Logic_var.Set.mem lv linked_upper_bounds) ->
- (* A variable with an incomplete constraint and without a linked
- upper bound has a missing upper bound. *)
- missing_guards, lv :: missing_upper_bounds
- | None ->
- (* A variable without a constraint has a missing guard. *)
- lv :: missing_guards, missing_upper_bounds
- | _ ->
- (* Otherwise the variable either has a complete constraint, or an
- incomplete constraint but with a linked upper bound. *)
- missing_guards, missing_upper_bounds)
- ctxt.bounded_vars
- ([], [])
- in
-
- let msg =
- Format.asprintf
- "@[invalid guard %a@ in quantification@ %a.@ \
- %a@,%a@ \
- %t@]"
- Printer.pp_predicate p Printer.pp_predicate ctxt.quantif
- (Pretty_utils.pp_list
- ~pre:"@[Missing guard for "
- ~sep:",@ "
- ~suf:".@]"
- Printer.pp_logic_var)
- (List.rev missing_guards)
- (Pretty_utils.pp_list
- ~pre:"@[Missing upper bound for "
- ~sep:",@ "
- ~suf:".@]"
- Printer.pp_logic_var)
- (List.rev missing_upper_bounds)
- (fun fmt ->
- if warn_rel then
- Format.fprintf fmt
- "@[Only %a and %a are allowed to guard quantifier variables@]"
- Printer.pp_relation Rlt Printer.pp_relation Rle)
- in
- Error.untypable msg
-end
-
-(** [extract_constraint ctxt t1 r t2] populates the quantification context
- [ctxt] with the constraint [t1 r t2], either adding a lower bound if [t2] is
- a bounded variable or adding an upper bound if [t1] is a bounded variable.
- @raises Typing_error if no constraint can be extracted or if the constraint
- is invalid (no bounded variable in [t1] or [t2] for instance). *)
-let extract_constraint ctxt t1 r t2 =
- (* Return the logic var corresponding to the given term or [None] if the term
- is not a variable ([TLval(TVar _, TNoOffset)]). *)
- let rec _get_logic_var_opt t =
- match t.term_node with
- | TLogic_coerce(_, t) -> _get_logic_var_opt t
- | TLval(TVar x, TNoOffset) -> Some x
- | _ -> None
- in
- (* Process the given relation *)
- let lv1 = Constraints.get_bounded_var t1 ctxt in
- let lv2 = Constraints.get_bounded_var t2 ctxt in
- match lv1, lv2 with
- | None, Some lv2 -> (* t1 value, t2 variable: store lower bound *)
- Constraints.add_lower_bound t1 r lv2 ctxt
- | Some lv1, None -> (* t1 variable, t2 value: store upper bound *)
- Constraints.add_upper_bound lv1 r t2 ctxt
- | Some lv1, Some lv2 ->
- (* t1 variable, t2 variable: store link between t1 and t2 *)
- let ctxt = Constraints.add_linked_upper_bound lv1 r lv2 ctxt in
- Constraints.add_lower_bound t1 r lv2 ctxt
- | None, None -> (* t1 value, t2 value: error *)
- let msg =
- Format.asprintf
- "@[invalid constraint %a %a %a, both operands are constants or \
- already bounded@]"
- Printer.pp_term t1
- Printer.pp_relation r
- Printer.pp_term t2
- in
- Constraints.raise_error msg ctxt
-
-(** [visit_quantif_relations ~is_forall ctxt p] traverses the predicate [p] of
- the quantification being analyzed in the context [ctxt] from left to right
- as long as the predicate is [Pimplies], [Pand] or [Prel(Rlt |Â Rle)], and
- calls [extract_constraint] on each relation [Rlt] or [Rle] it encounters
- until all the guards of the quantification have been found or the predicate
- is finished. If [is_forall] is [true] then the predicate being traversed is
- a universal quantification, otherwise it is an existential quantification.
- The function returns a tuple [ctxt, goal_opt] where [ctxt] is the
- quantification context and [goal_opt] is either [None] if the goal of the
- quantification has not been found yet or [Some goal] if [goal] is the
- predicate corresponding to the goal of the quantification.
- @raises Typing_error if the predicate contains something other than
- [Pimplies], [Pand] or [Prel] with a relation that is neither [Rlt] nor
- [Rle]. *)
-let rec visit_quantif_relations ~is_forall ctxt p =
- match p.pred_content with
- | Pimplies(lhs, rhs) ->
- let ctxt, _ = visit_quantif_relations ~is_forall ctxt lhs in
- if is_forall then begin
- if Constraints.has_unguarded_bounded_vars ctxt then
- visit_quantif_relations ~is_forall ctxt rhs
- else
- ctxt, Some rhs
- end else
- let msg =
- Format.asprintf
- "@[invalid quantification guard, expecting '%s' to continue@ \
- bounding variables,@ found '%s'@]"
- (if Kernel.Unicode.get () then Utf8_logic.conj else "&&")
- (if Kernel.Unicode.get () then Utf8_logic.implies else "==>")
- in
- Constraints.raise_error msg ctxt
- | Pand(lhs, rhs) ->
- let ctxt, _ = visit_quantif_relations ~is_forall ctxt lhs in
- if Constraints.has_unguarded_bounded_vars ctxt then
- visit_quantif_relations ~is_forall ctxt rhs
- else if not is_forall then
- ctxt, Some rhs
- else
- let msg =
- Format.asprintf
- "@[invalid quantification predicate, expecting '%s' to@ \
- separate the hypotheses from the goal, found '%s'@]"
- (if Kernel.Unicode.get () then Utf8_logic.implies else "==>")
- (if Kernel.Unicode.get () then Utf8_logic.conj else "&&")
- in
- Constraints.raise_error msg ctxt
- | Prel((Rlt | Rle) as r, t1, t2) ->
- let ctxt = extract_constraint ctxt t1 r t2 in
- ctxt, None
- | Prel _ ->
- Constraints.raise_error_invalid_pred ~warn_rel:true p ctxt
- | _ ->
- Constraints.raise_error_invalid_pred p ctxt
-
-(** [compute_quantif_guards ~is_forall quantif bounded_vars p] computes the
- guards for the bounded variables [bounded_vars] of the quantification
- [quantif] from the predicate [p]. If [is_forall] is [true] then [quantif] is
- a universal quantification, otherwise [quantif] is an existential
- quantification.
- The function returns the list of guards for the variables and the goal
- predicate of the quantification. *)
-let compute_quantif_guards ~is_forall quantif bounded_vars p =
- (* Traverse the predicate of the quantification to extract the guards of the
- bounded variables. *)
- let ctxt = Constraints.empty quantif bounded_vars in
- let ctxt, goal = visit_quantif_relations ~is_forall ctxt p in
- (* Check the validity of the result of the traversal. *)
- Constraints.check_validity ctxt;
- if Option.is_none goal then
- let msg =
- Format.asprintf
- "@[no goal found in quantification@ %a@]"
- Printer.pp_predicate quantif
- in
- Error.untypable msg
- else
- (* Traversal is valid, the guards and the goal can be retrieved and
- returned. *)
- let guards = Constraints.retrieve_guards ctxt in
- let goal = Option.get goal in
- guards, goal
-
-let () = Typing.compute_quantif_guards_ref := compute_quantif_guards
(* It could happen that the bounds provided for a quantified [lv] are empty
- in the sense that [min <= lv <= max] but [min > max]. In such cases, \true
+ in the sense that [min <= lv < max] but [min > max + 1]. In such cases, \true
(or \false depending on the quantification) should be generated instead of
nested loops.
[has_empty_quantif_with_false_negative] partially detects such cases:
@@ -551,31 +40,28 @@ let rec has_empty_quantif_with_false_negative = function
| [] ->
(* case 2 *)
false
- | (t1, rel1, _, rel2, t2) :: guards ->
+ | (t1, _, t2) :: guards ->
let iv1 = Interval.(extract_ival (infer t1)) in
let iv2 = Interval.(extract_ival (infer t2)) in
let lower_bound, _ = Ival.min_and_max iv1 in
let _, upper_bound = Ival.min_and_max iv2 in
- match lower_bound, upper_bound with
- | Some lower_bound, Some upper_bound ->
- let res =
- match rel1, rel2 with
- | Rle, Rle -> Integer.gt lower_bound upper_bound
- | Rle, Rlt | Rlt, Rle -> Integer.ge lower_bound upper_bound
- | Rlt, Rlt -> Integer.ge lower_bound (Z.sub upper_bound Z.one)
- | _ -> assert false
- in
- res (* case 1 *) || has_empty_quantif_with_false_negative guards
- | None, _ | _, None ->
- has_empty_quantif_with_false_negative guards
+ 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
+ | None, _ | _, None ->
+ has_empty_quantif_with_false_negative guards
+ end
+
module Label_ids =
State_builder.Counter(struct let name = "E_ACSL.Label_ids" end)
-let convert kf env loc ~is_forall quantif bounded_vars p =
+let convert kf env loc ~is_forall quantif =
(* guarded quantification over integers (or a subtype of integer) *)
- let guards, goal = compute_quantif_guards ~is_forall quantif bounded_vars p in
- match has_empty_quantif_with_false_negative guards, is_forall with
+ let bound_vars, goal = Bound_variables.get_preprocessed_quantifier quantif in
+ match has_empty_quantif_with_false_negative bound_vars, is_forall with
| true, true ->
Cil.one ~loc, env
| true, false ->
@@ -590,14 +76,14 @@ let convert kf env loc ~is_forall quantif bounded_vars p =
if is_forall then o, z, fun x -> x
else z, o, fun e -> new_exp ~loc:e.eloc (UnOp(LNot, e, intType))
in
- (* transform [guards] into [lscope_var list],
+ (* transform [bound_vars] into [lscope_var list],
and update logic scope in the process *)
let lvs_guards, env = List.fold_right
- (fun (t1, rel1, lv, rel2, t2) (lvs_guards, env) ->
- let lvs = Lscope.Lvs_quantif(t1, rel1, lv, rel2, t2) in
+ (fun (t1, lv, t2) (lvs_guards, env) ->
+ let lvs = Lscope.Lvs_quantif (t1, Rle, lv, Rlt, t2) in
let env = Env.Logic_scope.extend env lvs in
lvs :: lvs_guards, env)
- guards
+ bound_vars
([], env)
in
let var_res, res, env =
@@ -658,11 +144,13 @@ let convert kf env loc ~is_forall quantif bounded_vars p =
let quantif_to_exp kf env p =
let loc = p.pred_loc in
match p.pred_content with
- | Pforall(bounded_vars, ({ pred_content = Pimplies(_, _) } as p')) ->
- convert kf env loc ~is_forall:true p bounded_vars p'
+ | Pforall(bounded_vars, ({pred_content = Pimplies(_, _) } as p')) ->
+ Bound_variables.compute_guards loc ~is_forall:true p bounded_vars p';
+ convert kf env loc ~is_forall:true p
| Pforall _ -> Error.not_yet "unguarded \\forall quantification"
| Pexists(bounded_vars, ({ pred_content = Pand(_, _) } as p')) ->
- convert kf env loc ~is_forall:false p bounded_vars p'
+ Bound_variables.compute_guards loc ~is_forall:false p bounded_vars p';
+ convert kf env loc ~is_forall:false p
| Pexists _ -> Error.not_yet "unguarded \\exists quantification"
| _ -> assert false
diff --git a/src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.res.oracle
index d3fb6e9662ef3e3af24a8631b3a1ac5f86024967..072289b594d3d42d3ca7ccf0cfffafb5640c869c 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.res.oracle
@@ -24,7 +24,7 @@
assert
\initialized(__gen_e_acsl_at_6 +
(int)((int)((int)(__gen_e_acsl_u_3 - 9) * 32) +
- (int)((int)(__gen_e_acsl_v_3 - -5) - 1)));
+ (int)(__gen_e_acsl_v_3 - -4)));
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:45: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:43: Warning:
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c b/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c
index fd6454b1e06eb2d6ca9f59d962381e4b9298424c..46951ce87513b423dadef689c42e265455fe0090 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c
@@ -142,9 +142,9 @@ int main(void)
int __gen_e_acsl_u_7;
__gen_e_acsl_u_7 = 42;
*(__gen_e_acsl_at_7 + ((__gen_e_acsl_u_6 - 10) * 300 + (
- ((__gen_e_acsl_v_6 - -10) - 1) * 100 + (
- (__gen_e_acsl_w_2 - 100) - 1)))) =
- (((n - (long)__gen_e_acsl_u_6) + __gen_e_acsl_u_7) + __gen_e_acsl_v_6) + __gen_e_acsl_w_2 > 0L;
+ (__gen_e_acsl_v_6 - -9) * 100 + (
+ __gen_e_acsl_w_2 - 101)))) = (((
+ n - (long)__gen_e_acsl_u_6) + __gen_e_acsl_u_7) + __gen_e_acsl_v_6) + __gen_e_acsl_w_2 > 0L;
}
__gen_e_acsl_w_2 ++;
}
@@ -167,7 +167,7 @@ int main(void)
else __gen_e_acsl_if_2 = 3;
if (__gen_e_acsl_v_4 <= __gen_e_acsl_if_2) ; else break;
}
- *(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_4 - 9) * 32 + ((__gen_e_acsl_v_4 - -5) - 1))) =
+ *(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_4 - 9) * 32 + (__gen_e_acsl_v_4 - -4))) =
(n + (long)__gen_e_acsl_u_4) + __gen_e_acsl_v_4 > 0L;
__gen_e_acsl_v_4 ++;
}
@@ -189,7 +189,7 @@ int main(void)
long __gen_e_acsl_if;
if (__gen_e_acsl_u_2 > 0) __gen_e_acsl_if = n + (long)__gen_e_acsl_k_2;
else __gen_e_acsl_if = __gen_e_acsl_u_2 + __gen_e_acsl_v_2;
- *(__gen_e_acsl_at_3 + ((__gen_e_acsl_u_2 - 9) * 11 + ((__gen_e_acsl_v_2 - -5) - 1))) =
+ *(__gen_e_acsl_at_3 + ((__gen_e_acsl_u_2 - 9) * 11 + (__gen_e_acsl_v_2 - -4))) =
__gen_e_acsl_if > 0L;
}
__gen_e_acsl_v_2 ++;
@@ -271,15 +271,14 @@ int main(void)
(long)((int)(
(long)((int)(
__gen_e_acsl_u - 9L)) * 11L)) + (int)(
- (int)(__gen_e_acsl_v - -5L) - 1))),
+ __gen_e_acsl_v - -4L))),
sizeof(int),
(void *)__gen_e_acsl_at_3,
(void *)(& __gen_e_acsl_at_3));
__e_acsl_assert(__gen_e_acsl_valid_read_3,1,"RTE","main",
- "mem_access:\n \\valid_read(__gen_e_acsl_at_3 +\n (int)((int)((int)(__gen_e_acsl_u - 9) * 11) +\n (int)((int)(__gen_e_acsl_v - -5) - 1)))",
+ "mem_access:\n \\valid_read(__gen_e_acsl_at_3 +\n (int)((int)((int)(__gen_e_acsl_u - 9) * 11) +\n (int)(__gen_e_acsl_v - -4)))",
"tests/arith/at_on-purely-logic-variables.c",34);
- if (*(__gen_e_acsl_at_3 + ((__gen_e_acsl_u - 9) * 11 + ((
- __gen_e_acsl_v - -5) - 1))))
+ if (*(__gen_e_acsl_at_3 + ((__gen_e_acsl_u - 9) * 11 + (__gen_e_acsl_v - -4))))
;
else {
__gen_e_acsl_forall = 0;
@@ -333,7 +332,7 @@ int main(void)
__gen_e_acsl_k_4 = -9 + 1;
while (1) {
if (__gen_e_acsl_k_4 < 0) ; else break;
- *(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_4 - -9) - 1)) = m + (long)__gen_e_acsl_k_4;
+ *(__gen_e_acsl_at_5 + (__gen_e_acsl_k_4 - -8)) = m + (long)__gen_e_acsl_k_4;
__gen_e_acsl_k_4 ++;
}
}
@@ -349,16 +348,15 @@ int main(void)
if (__gen_e_acsl_k_3 < 0) ; else break;
{
int __gen_e_acsl_valid_read_5;
- __gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_5 + (
- (int)(
- __gen_e_acsl_k_3 - -9L) - 1)),
+ __gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_5 + (int)(
+ __gen_e_acsl_k_3 - -8L)),
sizeof(long),
(void *)__gen_e_acsl_at_5,
(void *)(& __gen_e_acsl_at_5));
__e_acsl_assert(__gen_e_acsl_valid_read_5,1,"RTE","main",
- "mem_access:\n \\valid_read(__gen_e_acsl_at_5 + (int)((int)(__gen_e_acsl_k_3 - -9) - 1))",
+ "mem_access: \\valid_read(__gen_e_acsl_at_5 + (int)(__gen_e_acsl_k_3 - -8))",
"tests/arith/at_on-purely-logic-variables.c",41);
- if (! (*(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_3 - -9) - 1)) == 0L))
+ if (! (*(__gen_e_acsl_at_5 + (__gen_e_acsl_k_3 - -8)) == 0L))
;
else {
__gen_e_acsl_exists_3 = 1;
@@ -399,23 +397,21 @@ int main(void)
(long)((int)(
(long)((int)(
__gen_e_acsl_u_3 - 9L)) * 32L)) + (int)(
- (int)(__gen_e_acsl_v_3 - -5L) - 1))),
+ __gen_e_acsl_v_3 - -4L))),
sizeof(int),
(void *)__gen_e_acsl_at_6,
(void *)(& __gen_e_acsl_at_6));
__e_acsl_assert(__gen_e_acsl_valid_read_6,1,"RTE","main",
- "mem_access:\n \\valid_read(__gen_e_acsl_at_6 +\n (int)((int)((int)(__gen_e_acsl_u_3 - 9) * 32) +\n (int)((int)(__gen_e_acsl_v_3 - -5) - 1)))",
+ "mem_access:\n \\valid_read(__gen_e_acsl_at_6 +\n (int)((int)((int)(__gen_e_acsl_u_3 - 9) * 32) +\n (int)(__gen_e_acsl_v_3 - -4)))",
"tests/arith/at_on-purely-logic-variables.c",45);
/*@ assert
Eva: initialization:
\initialized(__gen_e_acsl_at_6 +
(int)((int)((int)(__gen_e_acsl_u_3 - 9) * 32)
- +
- (int)((int)(__gen_e_acsl_v_3 - -5) - 1)));
+ + (int)(__gen_e_acsl_v_3 - -4)));
*/
if (*(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_3 - 9) * 32 + (
- (__gen_e_acsl_v_3 - -5) - 1))))
- ;
+ __gen_e_acsl_v_3 - -4)))) ;
else {
__gen_e_acsl_forall_2 = 0;
goto e_acsl_end_loop6;
@@ -483,20 +479,18 @@ int main(void)
__gen_e_acsl_u_5 - 10L)) * 300L)) + (int)(
(long)((int)(
(long)((int)(
- (int)(
- __gen_e_acsl_v_5 - -10L) - 1)) * 100L)) + (int)(
- (long)((int)(
- __gen_e_acsl_w - 100L)) - 1L)))),
+ __gen_e_acsl_v_5 - -9L)) * 100L)) + (int)(
+ __gen_e_acsl_w - 101L)))),
sizeof(int),
(void *)__gen_e_acsl_at_7,
(void *)(& __gen_e_acsl_at_7));
__e_acsl_assert(__gen_e_acsl_valid_read_7,1,"RTE","main",
- "mem_access:\n \\valid_read(__gen_e_acsl_at_7 +\n (int)((int)((int)(__gen_e_acsl_u_5 - 10) * 300) +\n (int)((int)((int)((int)(__gen_e_acsl_v_5 - -10) - 1) *\n 100)\n + (int)((int)(__gen_e_acsl_w - 100) - 1))))",
+ "mem_access:\n \\valid_read(__gen_e_acsl_at_7 +\n (int)((int)((int)(__gen_e_acsl_u_5 - 10) * 300) +\n (int)((int)((int)(__gen_e_acsl_v_5 - -9) * 100) +\n (int)(__gen_e_acsl_w - 101))))",
"tests/arith/at_on-purely-logic-variables.c",
57);
if (! *(__gen_e_acsl_at_7 + ((__gen_e_acsl_u_5 - 10) * 300 + (
- ((__gen_e_acsl_v_5 - -10) - 1) * 100 + (
- (__gen_e_acsl_w - 100) - 1)))))
+ (__gen_e_acsl_v_5 - -9) * 100 + (
+ __gen_e_acsl_w - 101)))))
;
else {
__gen_e_acsl_exists_7 = 1;
@@ -617,8 +611,7 @@ void __gen_e_acsl_f(int *t)
__e_acsl_assert(__gen_e_acsl_valid_read_3,1,"RTE","f",
"mem_access: \\valid_read(t + (int)(__gen_e_acsl_n_3 - 1))",
"tests/arith/at_on-purely-logic-variables.c",7);
- *(__gen_e_acsl_at_2 + ((__gen_e_acsl_n_3 - 1) - 1)) = *(t + (
- __gen_e_acsl_n_3 - 1)) > 5;
+ *(__gen_e_acsl_at_2 + (__gen_e_acsl_n_3 - 2)) = *(t + (__gen_e_acsl_n_3 - 1)) > 5;
}
__gen_e_acsl_n_3 ++;
}
@@ -636,7 +629,7 @@ void __gen_e_acsl_f(int *t)
__e_acsl_assert(__gen_e_acsl_valid_read,1,"RTE","f",
"mem_access: \\valid_read(t + __gen_e_acsl_n_2)",
"tests/arith/at_on-purely-logic-variables.c",7);
- *(__gen_e_acsl_at + ((__gen_e_acsl_n_2 - 1) - 1)) = *(t + __gen_e_acsl_n_2) == 12;
+ *(__gen_e_acsl_at + (__gen_e_acsl_n_2 - 2)) = *(t + __gen_e_acsl_n_2) == 12;
}
__gen_e_acsl_n_2 ++;
}
@@ -656,26 +649,24 @@ void __gen_e_acsl_f(int *t)
int __gen_e_acsl_valid_read_2;
int __gen_e_acsl_and;
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(__gen_e_acsl_at + (int)(
- (long)((int)(
- __gen_e_acsl_n - 1L)) - 1L)),
+ __gen_e_acsl_n - 2L)),
sizeof(int),
(void *)__gen_e_acsl_at,
(void *)(& __gen_e_acsl_at));
__e_acsl_assert(__gen_e_acsl_valid_read_2,1,"RTE","f",
- "mem_access:\n \\valid_read(__gen_e_acsl_at + (int)((int)(__gen_e_acsl_n - 1) - 1))",
+ "mem_access: \\valid_read(__gen_e_acsl_at + (int)(__gen_e_acsl_n - 2))",
"tests/arith/at_on-purely-logic-variables.c",7);
- if (*(__gen_e_acsl_at + ((__gen_e_acsl_n - 1) - 1))) {
+ if (*(__gen_e_acsl_at + (__gen_e_acsl_n - 2))) {
int __gen_e_acsl_valid_read_4;
__gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_2 + (int)(
- (long)((int)(
- __gen_e_acsl_n - 1L)) - 1L)),
+ __gen_e_acsl_n - 2L)),
sizeof(int),
(void *)__gen_e_acsl_at_2,
(void *)(& __gen_e_acsl_at_2));
__e_acsl_assert(__gen_e_acsl_valid_read_4,1,"RTE","f",
- "mem_access:\n \\valid_read(__gen_e_acsl_at_2 + (int)((int)(__gen_e_acsl_n - 1) - 1))",
+ "mem_access: \\valid_read(__gen_e_acsl_at_2 + (int)(__gen_e_acsl_n - 2))",
"tests/arith/at_on-purely-logic-variables.c",7);
- __gen_e_acsl_and = *(__gen_e_acsl_at_2 + ((__gen_e_acsl_n - 1) - 1));
+ __gen_e_acsl_and = *(__gen_e_acsl_at_2 + (__gen_e_acsl_n - 2));
}
else __gen_e_acsl_and = 0;
if (__gen_e_acsl_and) ;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c b/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
index d94bbc392cb7536b2c48179a9c0da1371e196cd5..f84cfba6458ecf2235e9cef3f3a2156c4237bff1 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
@@ -314,7 +314,7 @@ int main(void)
{
__e_acsl_mpz_t __gen_e_acsl__2;
__e_acsl_mpz_t __gen_e_acsl_add;
- __gmpz_init_set_ui(__gen_e_acsl__2,1UL);
+ __gmpz_init_set_str(__gen_e_acsl__2,"1",10);
__gmpz_init(__gen_e_acsl_add);
__gmpz_add(__gen_e_acsl_add,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_i_4),
diff --git a/src/plugins/e-acsl/tests/bts/issue-eacsl-149.c b/src/plugins/e-acsl/tests/bts/issue-eacsl-149.c
new file mode 100644
index 0000000000000000000000000000000000000000..64c896816225bc4e3c40874e3ae0bb8a6a8e34f6
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/issue-eacsl-149.c
@@ -0,0 +1,7 @@
+#include <limits.h>
+
+int main (int argc, char *argv[]) {
+ /*@ assert \exists unsigned int x; -1 < x < 5 && x == 0;*/
+ /*@ assert !(\forall unsigned int x; -1 < x < 5 ==> x != 0);*/
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-149.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-149.c
new file mode 100644
index 0000000000000000000000000000000000000000..f8be21500b2e3acf531f87309718cba4c249f1fb
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-149.c
@@ -0,0 +1,54 @@
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+int main(int argc, char **argv)
+{
+ int __retres;
+ {
+ int __gen_e_acsl_exists;
+ int __gen_e_acsl_x;
+ __gen_e_acsl_exists = 0;
+ /*@ assert
+ Eva: signed_overflow: (unsigned int)((int)(-1)) + 1 ≤ 2147483647;
+ */
+ __gen_e_acsl_x = (unsigned int)(-1) + 1;
+ while (1) {
+ if (__gen_e_acsl_x < 5) ; else break;
+ if (! (__gen_e_acsl_x == 0)) ;
+ else {
+ __gen_e_acsl_exists = 1;
+ goto e_acsl_end_loop1;
+ }
+ __gen_e_acsl_x ++;
+ }
+ e_acsl_end_loop1: ;
+ __e_acsl_assert(__gen_e_acsl_exists,1,"Assertion","main",
+ "\\exists unsigned int x; -1 < x < 5 && x == 0",
+ "tests/bts/issue-eacsl-149.c",4);
+ }
+ /*@ assert ∃ unsigned int x; -1 < x < 5 ∧ x ≡ 0; */ ;
+ {
+ int __gen_e_acsl_forall;
+ int __gen_e_acsl_x_2;
+ __gen_e_acsl_forall = 1;
+ __gen_e_acsl_x_2 = (unsigned int)(-1) + 1;
+ while (1) {
+ if (__gen_e_acsl_x_2 < 5) ; else break;
+ if (__gen_e_acsl_x_2 != 0) ;
+ else {
+ __gen_e_acsl_forall = 0;
+ goto e_acsl_end_loop2;
+ }
+ __gen_e_acsl_x_2 ++;
+ }
+ e_acsl_end_loop2: ;
+ __e_acsl_assert(! __gen_e_acsl_forall,1,"Assertion","main",
+ "!(\\forall unsigned int x; -1 < x < 5 ==> x != 0)",
+ "tests/bts/issue-eacsl-149.c",5);
+ }
+ /*@ assert ¬(∀ unsigned int x; -1 < x < 5 ⇒ x ≢ 0); */ ;
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue69.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue69.c
index c54c761be1bb180fb37e033f7f3743ffe17320a8..d703479245e0c336419a59d7edd94154720e66c1 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue69.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue69.c
@@ -10,7 +10,7 @@ int main(void)
__gen_e_acsl_forall = 1;
__gen_e_acsl_c = (unsigned char)4;
while (1) {
- if (__gen_e_acsl_c <= 255) ; else break;
+ if (__gen_e_acsl_c < 256) ; else break;
{
int __gen_e_acsl_and;
if (0 <= __gen_e_acsl_c) __gen_e_acsl_and = __gen_e_acsl_c <= 255;
@@ -42,9 +42,9 @@ int main(void)
while (1) {
{
int __gen_e_acsl_and_2;
- if (-128 <= __gen_e_acsl_u) __gen_e_acsl_and_2 = __gen_e_acsl_u <= 127;
+ if (-128 <= __gen_e_acsl_u) __gen_e_acsl_and_2 = __gen_e_acsl_u < 128;
else __gen_e_acsl_and_2 = 0;
- __e_acsl_assert(__gen_e_acsl_and_2,1,"RTE","main","-128 <= u <= 127",
+ __e_acsl_assert(__gen_e_acsl_and_2,1,"RTE","main","-128 <= u < 128",
"tests/bts/issue69.c",11);
}
if (__gen_e_acsl_u < __gen_e_acsl_m) ; else break;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-149.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-149.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..7d556feb94e7297c6c986b727ae07354af5aacd4
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-149.res.oracle
@@ -0,0 +1,4 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/bts/issue-eacsl-149.c:4: Warning:
+ signed overflow. assert (unsigned int)((int)(-1)) + 1 ≤ 2147483647;
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-149.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-149.e-acsl.err.log
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391