Commit 09ae99c4 authored by Julien Signoles's avatar Julien Signoles
Browse files

[interval] fix a bug when a logic function call does not return an integer

[typing] uniformize a bit more Is_a_real and Not_a_number
parent d570208e
......@@ -30,6 +30,8 @@ open Cil_types
(* Basic datatypes and operations *)
(* ********************************************************************* *)
(* TODO RATIONAL: both exceptions should be handle in the same way in this
module *)
exception Is_a_real
exception Not_a_number
......@@ -57,21 +59,18 @@ let rec interv_of_typ_with_real ty is_real = match Cil.unrollType ty with
| TEnum(enuminfo, _) ->
interv_of_typ_with_real (TInt (enuminfo.ekind, [])) is_real
| TFloat _ ->
(* TODO RATIONAL: examine TODO below. In particular this case is equivalent
* to the next case when [Real.is_t ty]. *)
(* TODO: Do not systematically consider floats as reals for efficiency *)
Ival.bottom, true
raise Is_a_real
| _ when Real.is_t ty ->
(* TODO RATIONAL: why bottom and not top? Why not raising Is_a_real? *)
Ival.bottom, true
| _ ->
raise Is_a_real
| TVoid _ | TPtr _ | TArray _ | TFun _ | TComp _ | TBuiltin_va_list _ ->
raise Not_a_number
| TNamed _ ->
assert false
let interv_of_logic_typ = function
| Ctype ty -> interv_of_typ_with_real ty false
| Linteger -> Ival.inject_range None None, false
| Lreal -> Ival.bottom, true
(* TODO RATIONAL: why bottom and not top? Why not raising Is_a_real? *)
| Lreal -> raise Is_a_real
| Ltype _ -> Error.not_yet "user-defined logic type"
| Lvar _ -> Error.not_yet "type variable"
| Larrow _ -> Error.not_yet "functional type"
......@@ -99,6 +98,7 @@ module rec Env: sig
val remove: Cil_types.logic_var -> unit
val replace: Cil_types.logic_var -> Ival.t -> unit
end = struct
open Cil_datatype
let tbl: Ival.t Logic_var.Hashtbl.t = Logic_var.Hashtbl.create 7
......@@ -113,7 +113,7 @@ end = struct
end
(* Environment for handling recursive logic functions *)
(* Environment for handling logic functions *)
and Logic_function_env: sig
val widen:
infer_with_real:(term -> bool -> Ival.t * bool) -> term -> Ival.t
......@@ -327,7 +327,11 @@ let rec infer_with_real t is_real =
List.iter (fun lv -> Env.remove lv) li.l_profile;
fixpoint i
in
fixpoint Ival.bottom
let i = fixpoint Ival.bottom in
(* call [interv_of_logic_typ] in order to raise Is_a_real or Not_a_number
when the function does not return an integer *)
Extlib.may (fun lty -> ignore (interv_of_logic_typ lty)) li.l_type;
i
| LBnone
| LBreads _ ->
(match li.l_type with
......
......@@ -127,10 +127,7 @@ let generate_kf ~loc fname env ret_ty params_ty li =
parameters *)
Gmp.Z.t_ptr ()
| Typing.C_type ik -> TInt(ik, [])
| Typing.Real ->
(* TODO RATIONAL: implement this case *)
assert false
| Typing.Nan -> Typing.typ_of_lty lvi.lv_type
| Typing.Real | Typing.Nan -> Typing.typ_of_lty lvi.lv_type
in
(* build the formals: cannot use [Cil.makeFormal] since the function
does not yet exist *)
......@@ -192,12 +189,15 @@ let generate_kf ~loc fname env ret_ty params_ty li =
before generating the code (code generation invokes typing) *)
let env =
let add env lvi vi =
(match vi.vtype with
| TInt _ as ty -> Interval.Env.add lvi (Interval.interv_of_typ ty)
| ty ->
(* TODO RATIONAL: what to do with rationals? *)
if Gmp.Z.is_t ty then
Interval.Env.add lvi (Ival.inject_range None None));
let i =
try
Interval.interv_of_typ vi.vtype
with
| Interval.Not_a_number
| Interval.Is_a_real ->
Ival.inject_range None None
in
Interval.Env.add lvi i;
Env.Logic_binding.add_binding env lvi vi
in
List.fold_left2 add env li.l_profile params
......
......@@ -66,7 +66,7 @@ let name_of_mpz_arith_bop = function
type strnum =
| Str_Z (* integers *)
| Str_R (* reals *)
| C_number (* integers AND floats) included *)
| C_number (* integers and floats included *)
(* convert [e] in a way that it is compatible with the given typing context. *)
let add_cast ~loc ?name env ctx strnum t_opt e =
......@@ -235,15 +235,19 @@ let conditional_to_exp ?(name="if") loc t_opt e1 (e2, env2) (e3, env3) =
let rec thost_to_host kf env th = match th with
| TVar { lv_origin = Some v } ->
Var (Visitor_behavior.Get.varinfo (Env.get_behavior env) v), env, v.vname
let v' = Visitor_behavior.Get.varinfo (Env.get_behavior env) v in
Var v', env, v.vname
| TVar ({ lv_origin = None } as logic_v) ->
Var (Env.Logic_binding.get env logic_v), env, logic_v.lv_name
let v' = Env.Logic_binding.get env logic_v in
Var v', env, logic_v.lv_name
| TResult _typ ->
let vis = Env.get_visitor env in
let kf = Extlib.the vis#current_kf in
let lhost = Misc.result_lhost kf in
(match lhost with
| Var v -> Var (Visitor_behavior.Get.varinfo (Env.get_behavior env) v), env, "result"
| Var v ->
let v' = Visitor_behavior.Get.varinfo (Env.get_behavior env) v in
Var v', env, "result"
| _ -> assert false)
| TMem t ->
let e, env = term_to_exp kf env t in
......
......@@ -52,7 +52,7 @@ module D =
Datatype.Make_with_collections
(struct
type t = number_ty
let name = "E_ACSL.New_typing.t"
let name = "E_ACSL.Typing.t"
let reprs = [ Gmpz; Real; Nan; c_int ]
include Datatype.Undefined
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment