[typing] fix typing of recursive logic function

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
 

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 -> ()

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 *)

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
 

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 *)

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
+}