Commit 7a91deaf authored by Julien Signoles's avatar Julien Signoles
Browse files

[typing] mutable environment in inference system

[typing] fix bug in on-the-fly typing when translating quantification
[typing] update a few oracles
parent e30616b8
......@@ -85,10 +85,10 @@ let join i1 i2 =
module Env = struct
open Cil_datatype
type t = interv Logic_var.Map.t
let empty = Logic_var.Map.empty
let add = Logic_var.Map.add
let find = Logic_var.Map.find
let tbl: interv Logic_var.Hashtbl.t = Logic_var.Hashtbl.create 7
let clear () = Logic_var.Hashtbl.clear tbl
let add = Logic_var.Hashtbl.add tbl
let find = Logic_var.Hashtbl.find tbl
end
(* ********************************************************************* *)
......@@ -112,7 +112,7 @@ let infer_sizeof ty =
let infer_alignof ty = singleton_of_int (Cil.bytesAlignOf ty)
let rec infer env t =
let rec infer t =
let get_cty t = match t.term_type with Ctype ty -> ty | _ -> assert false in
match t.term_node with
| TConst (Integer (n,_)) -> make n n
......@@ -126,7 +126,7 @@ let rec infer env t =
in
let n = Integer.of_int (find_idx 0 enumitem.eihost.eitems) in
make n n
| TLval lv -> infer_term_lval env lv
| TLval lv -> infer_term_lval lv
| TSizeOf ty -> infer_sizeof ty
| TSizeOfE t -> infer_sizeof (get_cty t)
| TSizeOfStr str -> singleton_of_int (String.length str + 1 (* '\0' *))
......@@ -134,10 +134,10 @@ let rec infer env t =
| TAlignOfE t -> infer_alignof (get_cty t)
| TUnOp (Neg, t) ->
let { lower; upper } = infer env t in
let { lower; upper } = infer t in
make (Integer.neg upper) (Integer.neg lower)
| TUnOp (BNot, t) ->
let { lower; upper } = infer env t in
let { lower; upper } = infer t in
let nl = Integer.lognot lower in
let nu = Integer.lognot upper in
make (Integer.min nl nu) (Integer.max nl nu)
......@@ -146,20 +146,20 @@ let rec infer env t =
| TBinOp ((Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr), _, _) ->
make Integer.zero Integer.one
| TBinOp (PlusA, t1, t2) ->
let i1 = infer env t1 in
let i2 = infer env t2 in
let i1 = infer t1 in
let i2 = infer t2 in
make (Integer.add i1.lower i2.lower) (Integer.add i1.upper i2.upper)
| TBinOp (MinusA, t1, t2) ->
let i1 = infer env t1 in
let i2 = infer env t2 in
let i1 = infer t1 in
let i2 = infer t2 in
make (Integer.sub i1.lower i2.upper) (Integer.sub i1.upper i2.lower)
| TBinOp (Mult, t1, t2) ->
let i1 = infer env t1 in
let i2 = infer env t2 in
let i1 = infer t1 in
let i2 = infer t2 in
combine Integer.mul i1 i2
| TBinOp (Div, t1, t2) ->
let i1 = infer env t1 in
let i2 = infer env t2 in
let i1 = infer t1 in
let i2 = infer t2 in
if Integer.le i2.lower Integer.zero && Integer.ge i2.upper Integer.zero then
(* 0 \in i2 *)
let l = Integer.min i1.lower (Integer.neg i1.upper) in
......@@ -172,8 +172,8 @@ let rec infer env t =
in
combine div i1 i2
| TBinOp (Mod, t1, t2) ->
let i1 = infer env t1 in
let i2 = infer env t2 in
let i1 = infer t1 in
let i2 = infer t2 in
(* the sign of the result is the sign of [t1];
also no more elements than [t2-1] and no more than [t1] *)
let nb1 = Integer.max (Integer.abs i1.lower) (Integer.abs i1.upper) in
......@@ -198,14 +198,14 @@ let rec infer env t =
| TCastE (ty, t)
| TCoerce (t, ty) ->
let it = infer env t in
let it = infer t in
let ity = interv_of_typ ty in
meet it ity
| Tif (_, t2, t3) ->
let i2 = infer env t2 in
let i3 = infer env t3 in
let i2 = infer t2 in
let i3 = infer t3 in
join i2 i3
| Tat (t, _) -> infer env t
| Tat (t, _) -> infer t
| TBinOp (MinusPP, t, _) ->
(match Cil.unrollType (get_cty t) with
| TArray(_, _, { scache = Computed n }, _) ->
......@@ -221,10 +221,10 @@ let rec infer env t =
| TArray _ | TPtr _ -> Lazy.force interv_of_unknown_block
| _ -> assert false)
| Tnull -> singleton_of_int 0
| TLogic_coerce (_, t) -> infer env t
| TLogic_coerce (_, t) -> infer t
| TCoerceE (t1, t2) ->
let i1 = infer env t1 in
let i2 = infer env t2 in
let i1 = infer t1 in
let i2 = infer t2 in
meet i1 i2
| Tapp (_,_,_) -> Error.not_yet "logic function application"
......@@ -248,16 +248,16 @@ let rec infer env t =
| Ttype _
| Tempty_set -> raise Not_an_integer
and infer_term_lval env (host, offset as tlv) =
and infer_term_lval (host, offset as tlv) =
match offset with
| TNoOffset -> infer_term_host env host
| TNoOffset -> infer_term_host host
| _ ->
let ty = Logic_utils.logicCType (Cil.typeOfTermLval tlv) in
interv_of_typ ty
and infer_term_host env = function
and infer_term_host = function
| TVar v ->
(try Env.find v env
(try Env.find v
with Not_found -> interv_of_typ (Logic_utils.logicCType v.lv_type))
| TResult ty -> interv_of_typ ty
| TMem t ->
......
......@@ -29,9 +29,8 @@ type interv = private { lower: Integer.t; upper: Integer.t }
include Datatype.S with type t = interv
module Env: sig
type t
val empty: t
val add: Cil_types.logic_var -> interv -> t -> t
val clear: unit -> unit
val add: Cil_types.logic_var -> interv -> unit
end
val interv_of_typ: Cil_types.typ -> t
......@@ -41,7 +40,7 @@ val join: t -> t -> t
val meet: t -> t -> t
exception Not_an_integer
val infer: Env.t -> Cil_types.term -> t
val infer: Cil_types.term -> t
(** [infer t] infers the smallest possible integer interval which the values
of the term can fit in. Assume than the type of [t] is an integral type.
@raise Not_an_integer if the type of the term is not a subtype of
......
......@@ -168,7 +168,6 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
let ty2 = Typing.get_integer_ty t2 in
Typing.join ty1 ty2
in
let ty = Typing.typ_of_integer_ty ctx in
let t_plus_one t =
Logic_const.term ~loc
(TBinOp(PlusA, t, Logic_const.tinteger ~loc 1))
......@@ -177,7 +176,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
let t1 = match rel1 with
| Rlt ->
let t = t_plus_one t1 in
Typing.type_term ~ctx t;
Typing.type_term ~force:true ~ctx t;
t
| Rle -> t1
| Rgt | Rge | Req | Rneq -> assert false
......@@ -186,35 +185,46 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
| 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]
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 ~ctx t2_one;
Typing.type_term ~force:true ~ctx t2_one;
let ctx_one =
let ty1 = Typing.get_integer_ty t1 in
let ty2 = Typing.get_integer_ty t2_one in
Typing.join ty1 ty2
in
let ty = Typing.typ_of_integer_ty ctx_one in
(* loop counter corresponding to the quantified variable *)
let var_x, x, env = Env.Logic_binding.add ~ty env logic_x in
let lv_x = var var_x in
let env =
if Gmpz.is_t ty then Env.add_stmt env (Gmpz.init ~loc x) else env
let env = match ctx_one with
| Typing.C_type _ -> env
| Typing.Gmp -> Env.add_stmt env (Gmpz.init ~loc x)
| Typing.Other -> assert false
in
let llv = cvar_to_lvar var_x in
(* build the inner loops and loop body *)
let body, env = mk_for_loop env tl in
(* initialize the loop counter to [t1] *)
let e1, env = term_to_exp kf (Env.push env) t1 in
let init_blk, env =
Env.pop_and_get
env
(Gmpz.affect ~loc:e1.eloc lv_x x e1)
~global_clear:false
Env.Middle
let init_blk, env =
Env.pop_and_get
env
(Gmpz.affect ~loc:e1.eloc lv_x x e1)
~global_clear:false
Env.Middle
in
(* generate the guard [x bop t2] *)
let stmts_block b = [ mkStmt ~valid_sid:true (Block b) ] in
let tlv = Logic_const.tvar ~loc llv in
let guard = Logic_const.term ~loc (TBinOp(bop2, tlv, t2)) Linteger in
Typing.type_term ~ctx:Typing.c_int guard;
let tlv = Logic_const.tvar ~loc logic_x in
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
in
Typing.type_term ~force:true ~ctx:Typing.c_int guard;
let guard_exp, env = term_to_exp kf (Env.push env) guard in
let break_stmt = mkStmt ~valid_sid:true (Break guard_exp.eloc) in
let guard_blk, env =
......@@ -232,7 +242,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
(* increment the loop counter [x++] *)
let tlv_one = t_plus_one tlv in
(* previous typing ensures that [x++] fits type [ty] *)
Typing.type_term ~ctx tlv_one;
Typing.type_term ~force:true ~ctx:ctx_one tlv_one;
let incr, env = term_to_exp kf (Env.push env) tlv_one in
let next_blk, env =
Env.pop_and_get
......
......@@ -161,7 +161,7 @@ int __gen_e_acsl_search(int elt)
__gen_e_acsl_forall = 0;
goto e_acsl_end_loop3;
}
__gen_e_acsl_i = (int)(__gen_e_acsl_i + 1L);
__gen_e_acsl_i ++;
}
e_acsl_end_loop3: ;
__e_acsl_assert(__gen_e_acsl_forall,(char *)"Precondition",
......@@ -184,7 +184,7 @@ int __gen_e_acsl_search(int elt)
__gen_e_acsl_forall_2 = 0;
goto e_acsl_end_loop5;
}
__gen_e_acsl_j_2 = (int)(__gen_e_acsl_j_2 + 1L);
__gen_e_acsl_j_2 ++;
}
e_acsl_end_loop5: ;
__gen_e_acsl_at_2 = __gen_e_acsl_forall_2;
......@@ -205,7 +205,7 @@ int __gen_e_acsl_search(int elt)
__gen_e_acsl_exists = 1;
goto e_acsl_end_loop4;
}
__gen_e_acsl_j = (int)(__gen_e_acsl_j + 1L);
__gen_e_acsl_j ++;
}
e_acsl_end_loop4: ;
__gen_e_acsl_at = __gen_e_acsl_exists;
......
......@@ -30,7 +30,7 @@ int main(int argc, char **argv)
if (__gen_e_acsl_k < argc) ; else break;
{
int __gen_e_acsl_valid_3;
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)(argv + __gen_e_acsl_k),
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)(argv + (unsigned long)__gen_e_acsl_k),
sizeof(char *));
if (__gen_e_acsl_valid_3) ;
else {
......@@ -38,7 +38,7 @@ int main(int argc, char **argv)
goto e_acsl_end_loop1;
}
}
__gen_e_acsl_k ++;
__gen_e_acsl_k = (int)(__gen_e_acsl_k + 1L);
}
e_acsl_end_loop1: ;
__e_acsl_assert(__gen_e_acsl_forall,(char *)"Assertion",(char *)"main",
......@@ -53,7 +53,7 @@ int main(int argc, char **argv)
int __gen_e_acsl_eq;
__gen_e_acsl_block_length = __e_acsl_block_length((void *)argv);
__gmpz_init_set_ui(__gen_e_acsl_block_length_2,__gen_e_acsl_block_length);
__gmpz_init_set_si(__gen_e_acsl_,((long)argc + (long)1) * 8L);
__gmpz_init_set_si(__gen_e_acsl_,(argc + 1) * 8);
__gen_e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_block_length_2),
(__mpz_struct const *)(__gen_e_acsl_));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
......@@ -65,29 +65,32 @@ int main(int argc, char **argv)
/*@ assert *(argv+argc) ≡ \null; */
{
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(argv + argc),
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(argv + (unsigned long)argc),
sizeof(char *));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(argv+argc)",15);
/*@ assert Value: mem_access: \valid_read(argv+argc); */
__e_acsl_assert(*(argv + argc) == (void *)0,(char *)"Assertion",
(char *)"main",(char *)"*(argv+argc) == \\null",15);
(char *)"mem_access: \\valid_read(argv+(unsigned long)argc)",
15);
/*@ assert Value: mem_access: \valid_read(argv+(unsigned long)argc); */
__e_acsl_assert(*(argv + (unsigned long)argc) == (void *)0,
(char *)"Assertion",(char *)"main",
(char *)"*(argv+argc) == \\null",15);
}
/*@ assert ¬\valid(*(argv+argc)); */
{
int __gen_e_acsl_initialized;
int __gen_e_acsl_and;
__gen_e_acsl_initialized = __e_acsl_initialized((void *)(argv + argc),
__gen_e_acsl_initialized = __e_acsl_initialized((void *)(argv + (unsigned long)argc),
sizeof(char *));
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid_read_2;
int __gen_e_acsl_valid_4;
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(argv + argc),
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(argv + (unsigned long)argc),
sizeof(char *));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(argv+argc)",16);
/*@ assert Value: mem_access: \valid_read(argv+argc); */
__gen_e_acsl_valid_4 = __e_acsl_valid((void *)*(argv + argc),
(char *)"mem_access: \\valid_read(argv+(unsigned long)argc)",
16);
/*@ assert Value: mem_access: \valid_read(argv+(unsigned long)argc); */
__gen_e_acsl_valid_4 = __e_acsl_valid((void *)*(argv + (unsigned long)argc),
sizeof(char));
__gen_e_acsl_and = __gen_e_acsl_valid_4;
}
......@@ -100,23 +103,27 @@ int main(int argc, char **argv)
{
int len;
size_t tmp;
/*@ assert Value: mem_access: \valid_read(argv+i); */
tmp = __gen_e_acsl_strlen((char const *)*(argv + i));
len = (int)tmp;
/*@ assert \valid(*(argv+i)); */
{
int __gen_e_acsl_initialized_2;
int __gen_e_acsl_and_2;
__gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(argv + i),
__gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(argv + (unsigned long)i),
sizeof(char *));
if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_valid_read_3;
int __gen_e_acsl_valid_5;
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(argv + i),
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(argv + (unsigned long)i),
sizeof(char *));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",
(char *)"main",
(char *)"mem_access: \\valid_read(argv+i)",19);
__gen_e_acsl_valid_5 = __e_acsl_valid((void *)*(argv + i),
(char *)"mem_access: \\valid_read(argv+(unsigned long)i)",
19);
/*@ assert Value: mem_access: \valid_read(argv+(unsigned long)i);
*/
__gen_e_acsl_valid_5 = __e_acsl_valid((void *)*(argv + (unsigned long)i),
sizeof(char));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_5;
}
......@@ -129,19 +136,22 @@ int main(int argc, char **argv)
int __gen_e_acsl_forall_2;
long __gen_e_acsl_k_2;
__gen_e_acsl_forall_2 = 1;
__gen_e_acsl_k_2 = (long)0;
__gen_e_acsl_k_2 = 0;
while (1) {
if (__gen_e_acsl_k_2 <= (long)len) ; else break;
if (__gen_e_acsl_k_2 <= len) ; else break;
{
int __gen_e_acsl_valid_read_4;
int __gen_e_acsl_valid_6;
__gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(
argv + i),
argv + (unsigned long)i),
sizeof(char *));
__e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",
(char *)"main",
(char *)"mem_access: \\valid_read(argv+i)",20);
__gen_e_acsl_valid_6 = __e_acsl_valid((void *)(*(argv + i) + __gen_e_acsl_k_2),
(char *)"mem_access: \\valid_read(argv+(unsigned long)i)",
20);
/*@ assert Value: mem_access: \valid_read(argv+(unsigned long)i);
*/
__gen_e_acsl_valid_6 = __e_acsl_valid((void *)(*(argv + (unsigned long)i) + (unsigned long)__gen_e_acsl_k_2),
sizeof(char));
if (__gen_e_acsl_valid_6) ;
else {
......
......@@ -6,18 +6,21 @@ FRAMAC_SHARE/libc/string.h:91:[e-acsl] warning: E-ACSL construct `logic function
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:91:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:93:[e-acsl] warning: E-ACSL construct `applying logic function' is not yet supported.
FRAMAC_SHARE/libc/string.h:93:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/e-acsl-runtime/mainargs.c:12:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/mainargs.c:13:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/mainargs.c:15:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/mainargs.c:15:[value] warning: out of bounds read. assert \valid_read(argv+argc);
tests/e-acsl-runtime/mainargs.c:15:[kernel] warning: out of bounds read. assert \valid_read(argv+(unsigned long)argc);
tests/e-acsl-runtime/mainargs.c:16:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/mainargs.c:16:[value] warning: out of bounds read. assert \valid_read(argv+argc);
tests/e-acsl-runtime/mainargs.c:16:[kernel] warning: out of bounds read. assert \valid_read(argv+(unsigned long)argc);
FRAMAC_SHARE/libc/string.h:91:[value] warning: function __gen_e_acsl_strlen: precondition 'valid_string_src' got status unknown.
FRAMAC_SHARE/libc/string.h:91:[value] warning: function strlen: precondition 'valid_string_src' got status unknown.
FRAMAC_SHARE/libc/string.h:93:[value] warning: function __gen_e_acsl_strlen: postcondition got status unknown.
tests/e-acsl-runtime/mainargs.c:19:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/mainargs.c:20:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/mainargs.c:18:[kernel] warning: out of bounds read. assert \valid_read(argv+i);
tests/e-acsl-runtime/mainargs.c:19:[kernel] warning: out of bounds read. assert \valid_read(argv+(unsigned long)i);
tests/e-acsl-runtime/mainargs.c:20:[kernel] warning: out of bounds read. assert \valid_read(argv+(unsigned long)i);
......@@ -12,7 +12,7 @@
__e_acsl_heap_size ∈ [--..--]
tests/gmp/quantif.i:9:[value] warning: assertion got status unknown.
[value] using specification for function __gmpz_init
[value] using specification for function __gmpz_init_set_si
[value] using specification for function __gmpz_init_set_ui
[value] using specification for function __gmpz_set
[value] using specification for function __gmpz_clear
tests/gmp/quantif.i:9:[value] entering loop for the first time
......@@ -29,6 +29,7 @@ tests/gmp/quantif.i:12:[value] entering loop for the first time
tests/gmp/quantif.i:16:[value] warning: assertion got status unknown.
tests/gmp/quantif.i:16:[value] entering loop for the first time
tests/gmp/quantif.i:21:[value] warning: assertion got status unknown.
[value] using specification for function __gmpz_set_si
tests/gmp/quantif.i:21:[value] entering loop for the first time
tests/gmp/quantif.i:25:[value] warning: assertion got status unknown.
tests/gmp/quantif.i:25:[value] entering loop for the first time
......
......@@ -151,6 +151,7 @@ let constant_to_exp ~loc t = function
raise Cil.Not_representable
| (None | Some _), _ -> Cil.kinteger64 ~loc ~kind ?repr n, false
with Cil.Not_representable ->
(* too big integer *)
Cil.mkString ~loc (Integer.to_string n), true)
| LStr s -> Cil.new_exp ~loc (Const (CStr s)), false
......@@ -297,7 +298,7 @@ and context_insensitive_term_to_exp kf env t =
(* [!t] is converted into [t == 0] *)
let zero = Logic_const.tinteger 0 in
let ctx = Typing.get_integer_ty t in
Typing.type_term ~ctx zero;
Typing.type_term ~force:false ~ctx zero;
let e, env =
comparison_to_exp kf ~loc ~name:"not" env Typing.gmp Eq t zero (Some t)
in
......@@ -341,7 +342,7 @@ and context_insensitive_term_to_exp kf env t =
possible values of [t2] *)
(* guarding divisions and modulos *)
let zero = Logic_const.tinteger 0 in
Typing.type_term ~ctx zero;
Typing.type_term ~force:false ~ctx zero;
(* do not generate [e2] from [t2] twice *)
let guard, env =
let name = name_of_binop bop ^ "_guard" in
......@@ -805,7 +806,7 @@ let term_to_exp typ t =
| TInt(ik, _) -> Typing.ikind ik
| _ -> Typing.c_int (* useless, but required *)
in
Typing.type_term ~ctx t;
Typing.type_term ~force:false ~ctx t;
let env = Env.empty (new Visitor.frama_c_copy Project_skeleton.dummy) in
let env = Env.push env in
let env = Env.rte env false in
......
......@@ -45,18 +45,21 @@ let gmp = Gmp
let c_int = C_type IInt
let ikind ik = C_type ik
let join ty1 ty2 = match ty1, ty2 with
| Other, Other -> Other
| Other, (Gmp | C_type _) | (Gmp | C_type _), Other ->
Options.fatal "[typing] join failure: integer and non integer type"
| Gmp, _ | _, Gmp -> Gmp
| C_type i1, C_type i2 ->
let ty = Cil.arithmeticConversion (TInt(i1, [])) (TInt(i2, [])) in
match ty with
| TInt(i, _) -> C_type i
| _ ->
Options.fatal "[typing] join failure: unexpected result %a"
Printer.pp_typ ty
let join ty1 ty2 =
if Options.Gmp_only.get () then Gmp
else
match ty1, ty2 with
| Other, Other -> Other
| Other, (Gmp | C_type _) | (Gmp | C_type _), Other ->
Options.fatal "[typing] join failure: integer and non integer type"
| Gmp, _ | _, Gmp -> Gmp
| C_type i1, C_type i2 ->
let ty = Cil.arithmeticConversion (TInt(i1, [])) (TInt(i2, [])) in
match ty with
| TInt(i, _) -> C_type i
| _ ->
Options.fatal "[typing] join failure: unexpected result %a"
Printer.pp_typ ty
exception Not_an_integer
let typ_of_integer_ty = function
......@@ -165,14 +168,14 @@ let coerce ~ctx ~op ty =
(** {2 Type system} *)
(******************************************************************************)
let mk_ctx ?(force=false) c =
let mk_ctx ~force c =
if force then c
else match c with
| Other -> Other
| Gmp | C_type _ -> if Options.Gmp_only.get () then Gmp else c
let rec type_term env ?force ~ctx t =
let ctx = mk_ctx ?force ctx in
let rec type_term ~force ~ctx t =
let ctx = mk_ctx ~force ctx in
let dup ty = ty, ty in
let infer t =
Cil.CurrentLoc.set t.term_loc;
......@@ -183,22 +186,21 @@ let rec type_term env ?force ~ctx t =
| TAlignOf _ ->
let ty =
try
let i = Interval.infer env t in
let i = Interval.infer t in
ty_of_interv ~ctx i
with Interval.Not_an_integer ->
Other
in
dup ty
| TLval tlv ->
let ty =
try
let i = Interval.infer env t in
let i = Interval.infer t in
ty_of_interv ~ctx i
with Interval.Not_an_integer ->
Other
in
type_term_lval env tlv;
type_term_lval tlv;
dup ty
| Toffset(_, t')
......@@ -207,9 +209,9 @@ let rec type_term env ?force ~ctx t =
| TAlignOfE t' ->
let ty =
try
let i = Interval.infer env t in
let i = Interval.infer t in
(* [t'] must be typed, but it is a pointer *)
ignore (type_term env ~ctx:Other t');
ignore (type_term ~force:false ~ctx:Other t');
ty_of_interv ~ctx i
with Interval.Not_an_integer ->
assert false
......@@ -219,10 +221,10 @@ let rec type_term env ?force ~ctx t =
| TBinOp (MinusPP, t1, t2) ->
let ty =
try
let i = Interval.infer env t in
let i = Interval.infer t in
(* [t1] and [t2] must be typed, but they are pointers *)
ignore (type_term env ~ctx:Other t1);
ignore (type_term env ~ctx:Other t2);
ignore (type_term ~force:false ~ctx:Other t1);
ignore (type_term ~force:false ~ctx:Other t2);
ty_of_interv ~ctx i
with Interval.Not_an_integer ->
assert false
......@@ -232,13 +234,13 @@ let rec type_term env ?force ~ctx t =
| TUnOp (unop, t') ->
let ctx =
try
let i = Interval.infer env t in
let i' = Interval.infer env t' in
mk_ctx (ty_of_interv ~ctx (Interval.join i i'))
let i = Interval.infer t in
let i' = Interval.infer t' in
mk_ctx ~force:false (ty_of_interv ~ctx (Interval.join i i'))
with Interval.Not_an_integer ->