diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml
index b637d7e2edc9026f8fd234d12b2b531060683856..2875f8b2248389a4b31d1d60b335e956a57d8fe7 100644
--- a/src/plugins/e-acsl/env.ml
+++ b/src/plugins/e-acsl/env.ml
@@ -331,13 +331,14 @@ module Logic_binding = struct
in
Error.not_yet msg
in
- let v, e, env = new_var
- ~loc:Location.unknown
- env
- ~name:logic_v.lv_name
- None
- ty
- (fun _ _ -> [])
+ let v, e, env =
+ new_var
+ ~loc:Location.unknown
+ env
+ ~name:logic_v.lv_name
+ None
+ ty
+ (fun _ _ -> [])
in
v, e, add_binding env logic_v v
diff --git a/src/plugins/e-acsl/gmp.ml b/src/plugins/e-acsl/gmp.ml
index 33c7013de586574a9c5631dff29d7c7d70213492..477eaa6f801d7cd5ead60a69fb5cb5c5507c4c7c 100644
--- a/src/plugins/e-acsl/gmp.ml
+++ b/src/plugins/e-acsl/gmp.ml
@@ -35,43 +35,47 @@ let mk_dummy_type_info_ref () =
module type S = sig
val t: unit -> typ
- val set_t: typeinfo -> unit
+ val t_as_ptr: unit -> typ
val is_now_referenced: unit -> unit
val is_t: typ -> bool
end
module Make(X: sig end) = struct
+
let t_torig_ref = mk_dummy_type_info_ref ()
- let set_t ty = t_torig_ref := ty
- let is_now_referenced () = !t_torig_ref.treferenced <- true
- let t () = TNamed(!t_torig_ref, [])
- let is_t ty = Cil_datatype.Typ.equal ty (t ())
-end
+ let t_struct_torig_ref = mk_dummy_type_info_ref ()
-module Z = struct
+ let set_t ty = t_torig_ref := ty
+ let set_t_struct ty = t_struct_torig_ref := ty
- include Make(struct end)
+ let is_now_referenced () = !t_torig_ref.treferenced <- true
- let t_struct_torig_ref = mk_dummy_type_info_ref ()
- let set_t_struct ty = t_struct_torig_ref := ty
+ let t () = TNamed(!t_torig_ref, [])
- (* TODO: why not a pointer here (but an array of size 1 instead? *)
- (* TODO: should be const *)
- let t_ptr () =
- TNamed(
+ (* create a unique shared representation in order to use [==] in [is_t] *)
+ let t_as_ptr_info =
+ lazy
{
torig_name = "";
- tname = "__e_acsl_mpz_struct *";
+ tname = !t_struct_torig_ref.tname ^ " *";
ttype = TArray(
TNamed(!t_struct_torig_ref, []),
Some (Cil.one ~loc:Cil_datatype.Location.unknown),
{scache = Not_Computed},
[]);
treferenced = true;
- },
- [])
+ }
+
+ let t_as_ptr () = TNamed (Lazy.force t_as_ptr_info, [])
+
+ let is_t ty = match ty with
+ | TNamed(tinfo, []) ->
+ tinfo == !t_torig_ref || tinfo == Lazy.force t_as_ptr_info
+ | _ -> false
+
end
+module Z = Make(struct end)
module Q = Make(struct end)
(**************************************************************************)
@@ -83,26 +87,26 @@ let init_t () =
let set_mp_t = object (self)
inherit Cil.nopCilVisitor
- (* exit after having initialized both Z.t and Q.t *)
- val mutable visited = false
+ (* exit after having initialized the 4 values (for Z.t and Q.t) *)
+ val mutable visited = 0
method private set f info =
f info;
- if visited then
+ if visited = 3 then
raise Exit
else begin
- visited <- true;
+ visited <- visited + 1;
Cil.SkipChildren
end
method !vglob = function
- | GType({ torig_name = s } as info, _) when s = "__e_acsl_mpz_t" ->
- self#set Z.set_t info
- | GType({ torig_name = s } as info, _) when s = "__e_acsl_mpz_struct" ->
- self#set Z.set_t_struct info
- | GType({ torig_name = s } as info, _) when s = "__e_acsl_mpq_t" ->
- self#set Q.set_t info
- | _ ->
- Cil.SkipChildren
+ | GType({ torig_name = name } as info, _) ->
+ if name = "__e_acsl_mpz_t" then self#set Z.set_t info
+ else if name = "__e_acsl_mpz_struct" then self#set Z.set_t_struct info
+ else if name = "__e_acsl_mpq_t" then self#set Q.set_t info
+ else if name = "__e_acsl_mpq_struct" then self#set Q.set_t_struct info
+ else Cil.SkipChildren
+ | _ ->
+ Cil.SkipChildren
end in
try Cil.visitCilFileSameGlobals set_mp_t (Ast.get ()) with Exit -> ()
diff --git a/src/plugins/e-acsl/gmp.mli b/src/plugins/e-acsl/gmp.mli
index 78431aeecfd727b9620f6b184f0824568f0fb2e5..4dcab5e720f67978f340b127bd18b63a338c4b17 100644
--- a/src/plugins/e-acsl/gmp.mli
+++ b/src/plugins/e-acsl/gmp.mli
@@ -33,7 +33,7 @@ val init_t: unit -> unit
module type S = sig
val t: unit -> typ
- val set_t: typeinfo -> unit
+ val t_as_ptr: unit -> typ (** type equivalent to [t] but seen as a pointer *)
val is_now_referenced: unit -> unit
val is_t: typ -> bool
end
@@ -41,8 +41,6 @@ end
(** Representation of the unbounded integer type at runtime *)
module Z: sig
include S
- val t_ptr: unit -> typ
- (** type "_mpz_struct *" *)
end
(** Representation of the rational type at runtime *)
diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml
index 80625645dac9c8ed6ec2f58bc5bf1295d21b08f3..6bb1048937f95a9673be6f73887aa154695e7188 100644
--- a/src/plugins/e-acsl/interval.ml
+++ b/src/plugins/e-acsl/interval.ml
@@ -90,6 +90,17 @@ let ikind_of_interv i =
| None, Some _ | Some _, None ->
Kernel.fatal ~current:true "ival: %a" Ival.pretty i
+(* function call profiles (intervals for their formal parameters) *)
+module Profile = struct
+ include Datatype.List_with_collections
+ (Ival)
+ (struct
+ let module_name = "E_ACSL.Interval.Logic_function_env.Profile"
+ end)
+ let is_included p1 p2 = List.for_all2 Ival.is_included p1 p2
+ let _join p1 p2 = List.map2 Ival.join p1 p2 (* TODO: to be removed *)
+end
+
(* Imperative environments *)
module rec Env: sig
val clear: unit -> unit
@@ -102,6 +113,9 @@ end = struct
open Cil_datatype
let tbl: Ival.t Logic_var.Hashtbl.t = Logic_var.Hashtbl.create 7
+ (* TODO: when adding, also join with the old value (if any). Would certainly
+ be the correct way to handle a \let in a recursive logic functions (if the
+ \let body depends on one formal) *)
let add = Logic_var.Hashtbl.add tbl
let remove = Logic_var.Hashtbl.remove tbl
let replace = Logic_var.Hashtbl.replace tbl
@@ -121,11 +135,19 @@ and Logic_function_env: sig
val clear: unit -> unit
end = struct
- module Profile =
- Datatype.List_with_collections
- (Ival)
+ (* The environment associates to each term (denoting a logic function
+ application) a profile, i.e. the list of intervals for its formal
+ parameters. It helps to type these applications.
+
+ For each pair of function name and profile, an interval containing the
+ result is also stored. It helps to generate the function definitions for
+ each logic function (for each function, one definition per profile) . *)
+
+ module Terms = Hashtbl.Make
(struct
- let module_name = "E_ACSL.Interval.Logic_function_env.Profile"
+ type t = term
+ let equal = (==)
+ let hash = Cil_datatype.Term.hash
end)
module LF =
@@ -136,9 +158,12 @@ end = struct
let module_name = "E_ACSL.Interval.Logic_function_env.LF"
end)
- let tbl = LF.Hashtbl.create 7
+ let terms: Profile.t Terms.t = Terms.create 7
+ let named_profiles = LF.Hashtbl.create 7
- let clear () = LF.Hashtbl.clear tbl
+ let clear () =
+ Terms.clear terms;
+ LF.Hashtbl.clear named_profiles
let interv_of_typ_containing_interv i =
try
@@ -148,11 +173,20 @@ end = struct
(* infinity *)
Ival.inject_range None None, false
- let extract_profile ~infer_with_real t = match t.term_node with
+ let rec map3 f l1 l2 l3 = match l1, l2, l3 with
+ | [], [], [] -> []
+ | x1 :: l1, x2 :: l2, x3 :: l3 -> f x1 x2 x3 :: map3 f l1 l2 l3
+ | _, _, _ -> invalid_arg "E_ACSL.Interval.map3"
+
+ let extract_profile ~infer_with_real old_profile t = match t.term_node with
| Tapp(li, _, args) ->
+ let old_profile = match old_profile with
+ | None -> List.map (fun _ -> Ival.bottom) li.l_profile
+ | Some p -> p
+ in
li.l_var_info.lv_name,
- List.map2
- (fun param arg ->
+ map3
+ (fun param old_i arg ->
try
(* TODO RATIONAL: what if a rational is used as argument or
returned? *)
@@ -161,29 +195,46 @@ end = struct
faster, and to generate fewer specialized functions *)
let larger_i, _is_real = interv_of_typ_containing_interv i in
(* TODO RATIONAL: what to do with is_real? *)
- Env.add param larger_i;
- larger_i
+ (* merge the old profile and the new one *)
+ let new_i = Ival.join larger_i old_i in
+ Env.add param new_i;
+ new_i
with Not_a_number ->
(* no need to add [param] to the environment *)
Ival.bottom)
li.l_profile
+ old_profile
args
| _ ->
assert false
- let widen ~infer_with_real t i =
- let p = extract_profile ~infer_with_real t in
+ let widen_one_callsite ~infer_with_real old_profile t i =
+ let (_,p as named_p) = extract_profile ~infer_with_real old_profile t in
try
- let old_i = LF.Hashtbl.find tbl p in
- if Ival.is_included i old_i then true, old_i
+ let old_i = LF.Hashtbl.find named_profiles named_p in
+ if Ival.is_included i old_i then true, p, old_i
else begin
let j = Ival.join i old_i in
- LF.Hashtbl.replace tbl p j;
- false, j
+ LF.Hashtbl.replace named_profiles named_p j;
+ false, p, j
+ end
+ with Not_found ->
+ LF.Hashtbl.add named_profiles named_p i;
+ false, p, i
+
+ let widen ~infer_with_real t i =
+ try
+ let old_p = Terms.find terms t in
+ let b, new_p, i = widen_one_callsite ~infer_with_real (Some old_p) t i in
+ if Profile.is_included new_p old_p then b, i
+ else begin
+ Terms.replace terms t new_p;
+ false, i
end
with Not_found ->
- LF.Hashtbl.add tbl p i;
- false, i
+ let b, p, i = widen_one_callsite ~infer_with_real None t i in
+ Terms.add terms t p;
+ b, i
end
diff --git a/src/plugins/e-acsl/logic_functions.ml b/src/plugins/e-acsl/logic_functions.ml
index f865b09c954bcaf76ff2e7ceb6139a3b4557c110..f688b954836842a39eca24a22da1be98733597ed 100644
--- a/src/plugins/e-acsl/logic_functions.ml
+++ b/src/plugins/e-acsl/logic_functions.ml
@@ -125,9 +125,10 @@ let generate_kf ~loc fname env ret_ty params_ty li =
| Typing.Gmpz ->
(* GMP's integer are arrays: consider them as pointers in function's
parameters *)
- Gmp.Z.t_ptr ()
+ Gmp.Z.t_as_ptr ()
| Typing.C_type ik -> TInt(ik, [])
- | Typing.Real | Typing.Nan -> Typing.typ_of_lty lvi.lv_type
+ | Typing.Real -> assert false (* TODO RATIONAL: to be implemented *)
+ | Typing.Nan -> Typing.typ_of_lty lvi.lv_type
in
(* build the formals: cannot use [Cil.makeFormal] since the function
does not yet exist *)
diff --git a/src/plugins/e-acsl/tests/gmp/let.c b/src/plugins/e-acsl/tests/gmp/let.c
index b42c297fbcc19fee3f6f07a7b579594ea16c4c2f..d7245e3560e00727a1bce494dc6021118ff213ed 100644
--- a/src/plugins/e-acsl/tests/gmp/let.c
+++ b/src/plugins/e-acsl/tests/gmp/let.c
@@ -39,4 +39,4 @@ int main(void) {
/*@ assert (\let u = s; u.x) > 0; */ ;
return 0;
-}
\ No newline at end of file
+}