pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Refactor Sil.Int into separate IntLit module

Browse Source 
Summary:
This diff refactors Sil.Int, which represents integer literals, into a
separate module IntLit.  There are no dependencies forcing Sil.Int to
be a submodule of Sil, and it is also no simpler as a submodule.

Reviewed By: cristianoc

Differential Revision: D3422910

fbshipit-source-id: 63013f2
master
Josh Berdine 9 years ago committed by Facebook Github Bot 3
parent 3828bdd544
commit a6a766b5f5
32 changed files with 535 additions and 457 deletions
Show Stats Download Patch File Download Diff File

139
infer/src/IR/IntLit.re
Unescape View File

@ -0,0 +1,139 @@
/*
* vim: set ft=rust:
* vim: set ft=reason:
*
* Copyright (c) 2009 - 2013 Monoidics ltd.
* Copyright (c) 2013 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*/
open! Utils;
let module F = Format;
/** signed and unsigned integer literals */
/* the first bool indicates whether this is an unsigned value,
and the second whether it is a pointer */
type t = (bool, Int64.t, bool);
let area u i =>
switch (i < 0L, u) {
| (true, false) => 1 /* only representable as signed */
| (false, _) => 2 /* in the intersection between signed and unsigned */
| (true, true) => 3 /* only representable as unsigned */
};
let to_signed (unsigned, i, ptr) =>
if (area unsigned i == 3) {
None
} else {
Some
/* not representable as signed */
(false, i, ptr)
};
let compare (unsigned1, i1, _) (unsigned2, i2, _) => {
let n = bool_compare unsigned1 unsigned2;
if (n != 0) {
n
} else {
Int64.compare i1 i2
}
};
let compare_value (unsigned1, i1, _) (unsigned2, i2, _) => {
let area1 = area unsigned1 i1;
let area2 = area unsigned2 i2;
let n = int_compare area1 area2;
if (n != 0) {
n
} else {
Int64.compare i1 i2
}
};
let eq i1 i2 => compare_value i1 i2 == 0;
let neq i1 i2 => compare_value i1 i2 != 0;
let leq i1 i2 => compare_value i1 i2 <= 0;
let lt i1 i2 => compare_value i1 i2 < 0;
let geq i1 i2 => compare_value i1 i2 >= 0;
let gt i1 i2 => compare_value i1 i2 > 0;
let of_int64 i => (false, i, false);
let of_int32 i => of_int64 (Int64.of_int32 i);
let of_int64_unsigned i unsigned => (unsigned, i, false);
let of_int i => of_int64 (Int64.of_int i);
let to_int (_, i, _) => Int64.to_int i;
let null = (false, 0L, true);
let zero = of_int 0;
let one = of_int 1;
let two = of_int 2;
let minus_one = of_int (-1);
let isone (_, i, _) => i == 1L;
let iszero (_, i, _) => i == 0L;
let isnull (_, i, ptr) => i == 0L && ptr;
let isminusone (unsigned, i, _) => not unsigned && i == (-1L);
let isnegative (unsigned, i, _) => not unsigned && i < 0L;
let neg (unsigned, i, ptr) => (unsigned, Int64.neg i, ptr);
let lift binop (unsigned1, i1, ptr1) (unsigned2, i2, ptr2) => (
unsigned1 || unsigned2,
binop i1 i2,
ptr1 || ptr2
);
let lift1 unop (unsigned, i, ptr) => (unsigned, unop i, ptr);
let add i1 i2 => lift Int64.add i1 i2;
let mul i1 i2 => lift Int64.mul i1 i2;
let div i1 i2 => lift Int64.div i1 i2;
let rem i1 i2 => lift Int64.rem i1 i2;
let logand i1 i2 => lift Int64.logand i1 i2;
let logor i1 i2 => lift Int64.logor i1 i2;
let logxor i1 i2 => lift Int64.logxor i1 i2;
let lognot i => lift1 Int64.lognot i;
let sub i1 i2 => add i1 (neg i2);
let pp f (unsigned, n, ptr) =>
if (ptr && n == 0L) {
F.fprintf f "null"
} else if unsigned {
F.fprintf f "%Lu" n
} else {
F.fprintf f "%Ld" n
};
let to_string i => pp_to_string pp i;

97
infer/src/IR/IntLit.rei
Unescape View File

@ -0,0 +1,97 @@
/*
* vim: set ft=rust:
* vim: set ft=reason:
*
* Copyright (c) 2009 - 2013 Monoidics ltd.
* Copyright (c) 2013 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*/
open! Utils;
let module F = Format;
/** signed and unsigned integer literals */
type t;
let add: t => t => t;
/** compare integers ignoring the distinction between pointers and non-pointers */
let compare: t => t => int;
/** compare the value of the integers, notice this is different from const compare,
which distinguished between signed and unsigned +1 */
let compare_value: t => t => int;
let div: t => t => t;
let eq: t => t => bool;
let of_int: int => t;
let of_int32: int32 => t;
let of_int64: int64 => t;
let of_int64_unsigned: int64 => bool => t;
let geq: t => t => bool;
let gt: t => t => bool;
let isminusone: t => bool;
let isnegative: t => bool;
let isnull: t => bool;
let isone: t => bool;
let iszero: t => bool;
let leq: t => t => bool;
let logand: t => t => t;
let lognot: t => t;
let logor: t => t => t;
let logxor: t => t => t;
let lt: t => t => bool;
let minus_one: t;
let mul: t => t => t;
let neg: t => t;
let neq: t => t => bool;
let null: t; /** null behaves like zero except for the function isnull */
let one: t;
let pp: F.formatter => t => unit;
let rem: t => t => t;
let sub: t => t => t;
let to_int: t => int;
let to_signed: t => option t; /** convert to signed if the value is representable */
let to_string: t => string;
let two: t;
let zero: t;

152
infer/src/IR/Sil.re
Unescape View File

@ -510,130 +510,6 @@ let module Subtype = {
};
/** module for signed and unsigned integers */
let module Int: {
type t;
let add: t => t => t;
let compare: t => t => int;
let compare_value: t => t => int;
let div: t => t => t;
let eq: t => t => bool;
let of_int: int => t;
let of_int32: int32 => t;
let of_int64: int64 => t;
let of_int64_unsigned: int64 => bool => t;
let geq: t => t => bool;
let gt: t => t => bool;
let isminusone: t => bool;
let isone: t => bool;
let isnegative: t => bool;
let isnull: t => bool;
let iszero: t => bool;
let leq: t => t => bool;
let logand: t => t => t;
let lognot: t => t;
let logor: t => t => t;
let logxor: t => t => t;
let lt: t => t => bool;
let minus_one: t;
let mul: t => t => t;
let neg: t => t;
let neq: t => t => bool;
let null: t;
let one: t;
let pp: Format.formatter => t => unit;
let rem: t => t => t;
let sub: t => t => t;
let to_int: t => int;
let to_signed: t => option t;
let to_string: t => string;
let two: t;
let zero: t;
} = {
/* the first bool indicates whether this is an unsigned value,
and the second whether it is a pointer */
type t = (bool, Int64.t, bool);
let area u i =>
switch (i < 0L, u) {
| (true, false) => 1 /* only representable as signed */
| (false, _) => 2 /* in the intersection between signed and unsigned */
| (true, true) => 3 /* only representable as unsigned */
};
let to_signed (unsigned, i, ptr) =>
if (area unsigned i == 3) {
None
} else {
Some
/* not representable as signed */
(false, i, ptr)
};
let compare (unsigned1, i1, _) (unsigned2, i2, _) => {
let n = bool_compare unsigned1 unsigned2;
if (n != 0) {
n
} else {
Int64.compare i1 i2
}
};
let compare_value (unsigned1, i1, _) (unsigned2, i2, _) => {
let area1 = area unsigned1 i1;
let area2 = area unsigned2 i2;
let n = int_compare area1 area2;
if (n != 0) {
n
} else {
Int64.compare i1 i2
}
};
let eq i1 i2 => compare_value i1 i2 == 0;
let neq i1 i2 => compare_value i1 i2 != 0;
let leq i1 i2 => compare_value i1 i2 <= 0;
let lt i1 i2 => compare_value i1 i2 < 0;
let geq i1 i2 => compare_value i1 i2 >= 0;
let gt i1 i2 => compare_value i1 i2 > 0;
let of_int64 i => (false, i, false);
let of_int32 i => of_int64 (Int64.of_int32 i);
let of_int64_unsigned i unsigned => (unsigned, i, false);
let of_int i => of_int64 (Int64.of_int i);
let to_int (_, i, _) => Int64.to_int i;
let null = (false, 0L, true);
let zero = of_int 0;
let one = of_int 1;
let two = of_int 2;
let minus_one = of_int (-1);
let isone (_, i, _) => i == 1L;
let iszero (_, i, _) => i == 0L;
let isnull (_, i, ptr) => i == 0L && ptr;
let isminusone (unsigned, i, _) => not unsigned && i == (-1L);
let isnegative (unsigned, i, _) => not unsigned && i < 0L;
let neg (unsigned, i, ptr) => (unsigned, Int64.neg i, ptr);
let lift binop (unsigned1, i1, ptr1) (unsigned2, i2, ptr2) => (
unsigned1 || unsigned2,
binop i1 i2,
ptr1 || ptr2
);
let lift1 unop (unsigned, i, ptr) => (unsigned, unop i, ptr);
let add i1 i2 => lift Int64.add i1 i2;
let mul i1 i2 => lift Int64.mul i1 i2;
let div i1 i2 => lift Int64.div i1 i2;
let rem i1 i2 => lift Int64.rem i1 i2;
let logand i1 i2 => lift Int64.logand i1 i2;
let logor i1 i2 => lift Int64.logor i1 i2;
let logxor i1 i2 => lift Int64.logxor i1 i2;
let lognot i => lift1 Int64.lognot i;
let sub i1 i2 => add i1 (neg i2);
let pp f (unsigned, n, ptr) =>
if (ptr && n == 0L) {
F.fprintf f "null"
} else if unsigned {
F.fprintf f "%Lu" n
} else {
F.fprintf f "%Ld" n
};
let to_string i => pp_to_string pp i;
};
/** Flags for a procedure call */
type call_flags = {
cf_virtual: bool,
@ -720,7 +596,7 @@ and attribute_category =
and closure = {name: Procname.t, captured_vars: list (exp, Pvar.t, typ)}
/** Constants */
and const =
| Cint of Int.t /** integer constants */
| Cint of IntLit.t /** integer constants */
| Cfun of Procname.t /** function names */
| Cstr of string /** string constants */
| Cfloat of float /** float constants */
@ -742,7 +618,7 @@ and struct_typ = {
struct_annotations: item_annotation /** annotations */
}
/** statically determined length of an array type, if any */
and static_length = option Int.t
and static_length = option IntLit.t
/** dynamically determined length of an array value, if any */
and dynamic_length = option exp
/** types for sil (structured) expressions */
@ -1005,9 +881,9 @@ let typ_strip_ptr =
let zero_value_of_numerical_type typ =>
switch typ {
| Tint _ => Const (Cint Int.zero)
| Tint _ => Const (Cint IntLit.zero)
| Tfloat _ => Const (Cfloat 0.0)
| Tptr _ => Const (Cint Int.null)
| Tptr _ => Const (Cint IntLit.null)
| _ => assert false
};
@ -1033,12 +909,12 @@ let fld_equal fld1 fld2 => fld_compare fld1 fld2 == 0;
let exp_is_zero =
fun
| Const (Cint n) => Int.iszero n
| Const (Cint n) => IntLit.iszero n
| _ => false;
let exp_is_null_literal =
fun
| Const (Cint n) => Int.isnull n
| Const (Cint n) => IntLit.isnull n
| _ => false;
let exp_is_this =
@ -1062,7 +938,7 @@ let ikind_is_unsigned =
| IULongLong => true
| _ => false;
let int_of_int64_kind i ik => Int.of_int64_unsigned i (ikind_is_unsigned ik);
let int_of_int64_kind i ik => IntLit.of_int64_unsigned i (ikind_is_unsigned ik);
let unop_compare o1 o2 =>
switch (o1, o2) {
@ -1414,7 +1290,7 @@ let const_kind_equal c1 c2 => {
let rec const_compare (c1: const) (c2: const) :int =>
switch (c1, c2) {
| (Cint i1, Cint i2) => Int.compare i1 i2
| (Cint i1, Cint i2) => IntLit.compare i1 i2
| (Cint _, _) => (-1)
| (_, Cint _) => 1
| (Cfun fn1, Cfun fn2) => Procname.compare fn1 fn2
@ -2311,7 +2187,7 @@ and attribute_to_string pe =>
| Aunsubscribed_observer => "UNSUBSCRIBED_OBSERVER"
and pp_const pe f =>
fun
| Cint i => Int.pp f i
| Cint i => IntLit.pp f i
| Cfun fn =>
switch pe.pe_kind {
| PP_HTML => F.fprintf f "_fun_%s" (Escape.escape_xml (Procname.to_string fn))
@ -2629,7 +2505,7 @@ let d_instr_list (il: list instr) => L.add_print_action (L.PTinstr_list, Obj.rep
let pp_atom pe0 f a => {
let (pe, changed) = color_pre_wrapper pe0 f a;
switch a {
| Aeq (BinOp op e1 e2) (Const (Cint i)) when Int.isone i =>
| Aeq (BinOp op e1 e2) (Const (Cint i)) when IntLit.isone i =>
switch pe.pe_kind {
| PP_TEXT
| PP_HTML => F.fprintf f "%a" (pp_exp pe) (BinOp op e1 e2)
@ -3400,19 +3276,19 @@ let exp_float v => Const (Cfloat v);
/** Integer constant 0 */
let exp_zero = exp_int Int.zero;
let exp_zero = exp_int IntLit.zero;
/** Null constant */
let exp_null = exp_int Int.null;
let exp_null = exp_int IntLit.null;
/** Integer constant 1 */
let exp_one = exp_int Int.one;
let exp_one = exp_int IntLit.one;
/** Integer constant -1 */
let exp_minus_one = exp_int Int.minus_one;
let exp_minus_one = exp_int IntLit.minus_one;
/** Create integer constant corresponding to the boolean value */

53
infer/src/IR/Sil.rei
Unescape View File

@ -168,49 +168,6 @@ let module Subtype: {
};
/** module for signed and unsigned integers */
let module Int: {
type t;
let add: t => t => t;
/** compare the value of the integers, notice this is different from const compare,
which distinguished between signed and unsigned +1 */
let compare_value: t => t => int;
let div: t => t => t;
let eq: t => t => bool;
let of_int: int => t;
let of_int32: int32 => t;
let of_int64: int64 => t;
let geq: t => t => bool;
let gt: t => t => bool;
let isminusone: t => bool;
let isnegative: t => bool;
let isnull: t => bool;
let isone: t => bool;
let iszero: t => bool;
let leq: t => t => bool;
let logand: t => t => t;
let lognot: t => t;
let logor: t => t => t;
let logxor: t => t => t;
let lt: t => t => bool;
let minus_one: t;
let mul: t => t => t;
let neg: t => t;
let neq: t => t => bool;
let null: t; /** null behaves like zero except for the function isnull */
let one: t;
let pp: F.formatter => t => unit;
let rem: t => t => t;
let sub: t => t => t;
let to_int: t => int;
let to_signed: t => option t; /** convert to signed if the value is representable */
let to_string: t => string;
let two: t;
let zero: t;
};
/** Flags for a procedure call */
type call_flags = {
cf_virtual: bool,
@ -293,7 +250,7 @@ and attribute_category =
and closure = {name: Procname.t, captured_vars: list (exp, Pvar.t, typ)}
/** Constants */
and const =
| Cint of Int.t /** integer constants */
| Cint of IntLit.t /** integer constants */
| Cfun of Procname.t /** function names */
| Cstr of string /** string constants */
| Cfloat of float /** float constants */
@ -315,7 +272,7 @@ and struct_typ = {
struct_annotations: item_annotation /** annotations */
}
/** statically determined length of an array type, if any */
and static_length = option Int.t
and static_length = option IntLit.t
/** dynamically determined length of an array value, if any */
and dynamic_length = option exp
/** Types for sil (structured) expressions. */
@ -674,9 +631,9 @@ let ikind_is_char: ikind => bool;
let ikind_is_unsigned: ikind => bool;
/** Convert an int64 into an Int.t given the kind:
/** Convert an int64 into an IntLit.t given the kind:
the int64 is interpreted as unsigned according to the kind */
let int_of_int64_kind: int64 => ikind => Int.t;
let int_of_int64_kind: int64 => ikind => IntLit.t;
/** Comparision for ptr_kind */
@ -1181,7 +1138,7 @@ let exp_minus_one: exp;
/** Create integer constant */
let exp_int: Int.t => exp;
let exp_int: IntLit.t => exp;
/** Create float constant */

4
infer/src/backend/abs.ml
Unescape View File

@ -781,7 +781,7 @@ let abstract_pure_part p ~(from_abstract_footprint: bool) =
| Sil.Aeq (Sil.Const (Sil.Cint i), Sil.BinOp (Sil.Lt, _, _))
| Sil.Aeq (Sil.BinOp (Sil.Lt, _, _), Sil.Const (Sil.Cint i))
| Sil.Aeq (Sil.Const (Sil.Cint i), Sil.BinOp (Sil.Le, _, _))
| Sil.Aeq (Sil.BinOp (Sil.Le, _, _), Sil.Const (Sil.Cint i)) when Sil.Int.isone i ->
| Sil.Aeq (Sil.BinOp (Sil.Le, _, _), Sil.Const (Sil.Cint i)) when IntLit.isone i ->
a :: pi
| Sil.Aeq (Sil.Var name, e) when not (Ident.is_primed name) ->
(match e with
@ -930,7 +930,7 @@ let should_raise_objc_leak hpred =
match hpred with
| Sil.Hpointsto(_, Sil.Estruct((fn, Sil.Eexp( (Sil.Const (Sil.Cint i)), _)):: _, _),
Sil.Sizeof (typ, _, _))
when Ident.fieldname_is_hidden fn && Sil.Int.gt i Sil.Int.zero (* counter > 0 *) ->
when Ident.fieldname_is_hidden fn && IntLit.gt i IntLit.zero (* counter > 0 *) ->
Mleak_buckets.should_raise_objc_leak typ
| _ -> None

3
infer/src/backend/absarray.ml
Unescape View File

@ -578,7 +578,8 @@ let remove_redundant_elements prop =
modified := true;
false in
match e, se with
| Sil.Const (Sil.Cint i), Sil.Eexp (Sil.Var id, _) when (not fp_part || Sil.Int.iszero i) && Ident.is_normal id = false && occurs_at_most_once id ->
| Sil.Const (Sil.Cint i), Sil.Eexp (Sil.Var id, _)
when (not fp_part || IntLit.iszero i) && not (Ident.is_normal id) && occurs_at_most_once id ->
remove () (* unknown value can be removed in re-execution mode or if the index is zero *)
| Sil.Var id, Sil.Eexp _ when Ident.is_normal id = false && occurs_at_most_once id ->
remove () (* index unknown can be removed *)

84
infer/src/backend/autounit.ml
Unescape View File

@ -15,24 +15,24 @@ open! Utils
module L = Logging
module F = Format
let (++) = Sil.Int.add
let (--) = Sil.Int.sub
let (++) = IntLit.add
let (--) = IntLit.sub
module IdMap = Map.Make (Ident) (** maps from identifiers *)
(** Constraint solving module *)
module Constraint : sig
(** Collect constraints on [vars] from [pi], and return a satisfying instantiation *)
val solve_from_pure : Sil.atom list -> Ident.t list -> Sil.Int.t IdMap.t
val solve_from_pure : Sil.atom list -> Ident.t list -> IntLit.t IdMap.t
end = struct
(** flag for debug mode of the module *)
let debug = false
(** denote a range of values [bottom] <= val <= [top], except [excluded] *)
type range =
{ mutable bottom: Sil.Int.t option; (** lower bound *)
mutable excluded: Sil.Int.t list; (** individual values not in range *)
mutable top: Sil.Int.t option; (** upper bound *) }
{ mutable bottom: IntLit.t option; (** lower bound *)
mutable excluded: IntLit.t list; (** individual values not in range *)
mutable top: IntLit.t option; (** upper bound *) }
type eval = range IdMap.t (** evaluation for variables *)
@ -44,8 +44,9 @@ end = struct
let pp_range id fmt rng =
let pp_opt fmt = function
| None -> F.fprintf fmt "_"
| Some n -> Sil.Int.pp fmt n in
F.fprintf fmt "%a <= %a <= %a [%a]" pp_opt rng.bottom (Ident.pp pe_text) id pp_opt rng.top (pp_comma_seq Sil.Int.pp) rng.excluded
| Some n -> IntLit.pp fmt n in
F.fprintf fmt "%a <= %a <= %a [%a]"
pp_opt rng.bottom (Ident.pp pe_text) id pp_opt rng.top (pp_comma_seq IntLit.pp) rng.excluded
(** pretty print an evaluation *)
let pp_eval fmt ev =
@ -64,22 +65,22 @@ end = struct
let gt_bottom i r =
match r.bottom with
| None -> true
| Some j -> Sil.Int.gt i j
| Some j -> IntLit.gt i j
let geq_bottom i r =
match r.bottom with
| None -> true
| Some j -> Sil.Int.geq i j
| Some j -> IntLit.geq i j
let lt_top i r =
match r.top with
| None -> true
| Some j -> Sil.Int.lt i j
| Some j -> IntLit.lt i j
let leq_top i r =
match r.top with
| None -> true
| Some j -> Sil.Int.leq i j
| Some j -> IntLit.leq i j
(** normalize [r]: the excluded elements must be strictly between bottom and top *)
let normalize r =
@ -87,17 +88,17 @@ end = struct
let rec normalize_bottom () = match r.bottom with
| None -> ()
| Some i ->
if IList.mem Sil.Int.eq i r.excluded then begin
r.excluded <- IList.filter (Sil.Int.neq i) r.excluded;
r.bottom <- Some (i ++ Sil.Int.one);
if IList.mem IntLit.eq i r.excluded then begin
r.excluded <- IList.filter (IntLit.neq i) r.excluded;
r.bottom <- Some (i ++ IntLit.one);
normalize_bottom ()
end in
let rec normalize_top () = match r.top with
| None -> ()
| Some i ->
if IList.mem Sil.Int.eq i r.excluded then begin
r.excluded <- IList.filter (Sil.Int.neq i) r.excluded;
r.top <- Some (i -- Sil.Int.one);
if IList.mem IntLit.eq i r.excluded then begin
r.excluded <- IList.filter (IntLit.neq i) r.excluded;
r.top <- Some (i -- IntLit.one);
normalize_top ()
end in
normalize_bottom ();
@ -112,7 +113,7 @@ end = struct
(** exclude one element from the range *)
let add_excluded r id i =
if geq_bottom i r && leq_top i r && not (IList.mem Sil.Int.eq i r.excluded)
if geq_bottom i r && leq_top i r && not (IList.mem IntLit.eq i r.excluded)
then begin
r.excluded <- i :: r.excluded;
normalize r;
@ -143,42 +144,49 @@ end = struct
let found = ref None in
let num_iter = IList.length rng.excluded in
let try_candidate candidate =
if geq_bottom candidate rng && leq_top candidate rng && not (IList.mem Sil.Int.eq candidate rng.excluded)
then (found := Some candidate; rng.bottom <- Some candidate; rng.top <- Some candidate; rng.excluded <- []) in
if geq_bottom candidate rng
&& leq_top candidate rng
&& not (IList.mem IntLit.eq candidate rng.excluded)
then (
found := Some candidate;
rng.bottom <- Some candidate;
rng.top <- Some candidate;
rng.excluded <- []
) in
let search_up () =
let base = match rng.bottom with None -> Sil.Int.zero | Some n -> n in
let base = match rng.bottom with None -> IntLit.zero | Some n -> n in
for i = 0 to num_iter do
if !found = None then
let candidate = Sil.Int.add base (Sil.Int.of_int i) in
let candidate = IntLit.add base (IntLit.of_int i) in
try_candidate candidate
done in
let search_down () =
let base = match rng.top with None -> Sil.Int.zero | Some n -> n in
let base = match rng.top with None -> IntLit.zero | Some n -> n in
for i = 0 to num_iter do
if !found = None then
let candidate = Sil.Int.sub base (Sil.Int.of_int i) in
let candidate = IntLit.sub base (IntLit.of_int i) in
try_candidate candidate
done in
search_up ();
if !found = None then search_down ();
if !found = None then
(L.err "Constraint Error: empty range %a@." (pp_range id) rng;
rng.top <- Some Sil.Int.zero;
rng.bottom <- Some Sil.Int.zero;
rng.top <- Some IntLit.zero;
rng.bottom <- Some IntLit.zero;
rng.excluded <- [])
(** return the solution if the id is solved (has unique solution) *)
let solved ev id =
let rng = IdMap.find id ev in
match rng.bottom, rng.top with
| Some n1, Some n2 when Sil.Int.eq n1 n2 -> Some n1
| Some n1, Some n2 when IntLit.eq n1 n2 -> Some n1
| _ -> None
let rec pi_iter do_le do_lt do_neq pi =
let do_atom a = match a with
| Sil.Aeq (Sil.BinOp (Sil.Le, e1, e2), Sil.Const (Sil.Cint i)) when Sil.Int.isone i ->
| Sil.Aeq (Sil.BinOp (Sil.Le, e1, e2), Sil.Const (Sil.Cint i)) when IntLit.isone i ->
do_le e1 e2
| Sil.Aeq (Sil.BinOp (Sil.Lt, e1, e2), Sil.Const (Sil.Cint i)) when Sil.Int.isone i ->
| Sil.Aeq (Sil.BinOp (Sil.Lt, e1, e2), Sil.Const (Sil.Cint i)) when IntLit.isone i ->
do_lt e1 e2
| Sil.Aeq _ -> ()
| Sil.Aneq (e1, e2) ->
@ -203,10 +211,10 @@ end = struct
| Some _, Some n -> add_bottom rng id n
| _ -> () in
let (+++) n1_op n2_op = match n1_op, n2_op with
| Some n1, Some n2 -> Some (Sil.Int.add n1 n2)
| Some n1, Some n2 -> Some (IntLit.add n1 n2)
| _ -> None in
let (---) n1_op n2_op = match n1_op, n2_op with
| Some n1, Some n2 -> Some (Sil.Int.sub n1 n2)
| Some n1, Some n2 -> Some (IntLit.sub n1 n2)
| _ -> None in
let do_le e1 e2 = match e1, e2 with
| Sil.Var id, Sil.Const (Sil.Cint n) ->
@ -226,12 +234,12 @@ end = struct
let do_lt e1 e2 = match e1, e2 with
| Sil.Const (Sil.Cint n), Sil.Var id ->
let rng = IdMap.find id ev in
add_bottom rng id (n ++ Sil.Int.one)
add_bottom rng id (n ++ IntLit.one)
| Sil.Const (Sil.Cint n), Sil.BinOp (Sil.PlusA, Sil.Var id1, Sil.Var id2) ->
let rng1 = IdMap.find id1 ev in
let rng2 = IdMap.find id2 ev in
update_bottom rng1 id1 (Some (n ++ Sil.Int.one) --- rng2.top);
update_bottom rng2 id2 (Some (n ++ Sil.Int.one) --- rng1.top)
update_bottom rng1 id1 (Some (n ++ IntLit.one) --- rng2.top);
update_bottom rng2 id2 (Some (n ++ IntLit.one) --- rng1.top)
| _ -> if debug then assert false in
let rec do_neq e1 e2 = match e1, e2 with
| Sil.Var id, Sil.Const (Sil.Cint n)
@ -511,13 +519,13 @@ let gen_init_vars code solutions idmap =
if not alloc then
let const = match typ with
| Sil.Tint _ | Sil.Tvoid ->
get_const id (Sil.Cint Sil.Int.zero)
get_const id (Sil.Cint IntLit.zero)
| Sil.Tfloat _ ->
Sil.Cfloat 0.0
| Sil.Tptr _ ->
get_const id (Sil.Cint Sil.Int.zero)
get_const id (Sil.Cint IntLit.zero)
| Sil.Tfun _ ->
Sil.Cint Sil.Int.zero
Sil.Cint IntLit.zero
| typ ->
L.err "do_vinfo type undefined: %a@." (Sil.pp_typ_full pe) typ;
assert false in

4
infer/src/backend/buckets.ml
Unescape View File

@ -72,14 +72,14 @@ let check_access access_opt de_opt =
let formal_param_used_in_call = ref false in
let has_call_or_sets_null node =
let rec exp_is_null exp = match exp with
| Sil.Const (Sil.Cint n) -> Sil.Int.iszero n
| Sil.Const (Sil.Cint n) -> IntLit.iszero n
| Sil.Cast (_, e) -> exp_is_null e
| Sil.Var _
| Sil.Lvar _ ->
begin
match State.get_const_map () node exp with
| Some (Sil.Cint n) ->
Sil.Int.iszero n
IntLit.iszero n
| _ -> false
end
| _ -> false in

50
infer/src/backend/dom.ml
Unescape View File

@ -15,8 +15,8 @@ open! Utils
module L = Logging
module F = Format
let (++) = Sil.Int.add
let (--) = Sil.Int.sub
let (++) = IntLit.add
let (--) = IntLit.sub
(** {2 Utility functions for ids} *)
@ -466,14 +466,14 @@ end = struct
let ineq_upper = Prop.mk_inequality (Sil.BinOp(Sil.Le, e, upper)) in
ineq_lower:: ineq_upper:: acc
let minus2_to_2 = IList.map Sil.Int.of_int [-2; -1; 0; 1; 2]
let minus2_to_2 = IList.map IntLit.of_int [-2; -1; 0; 1; 2]
let get_induced_pi () =
let t_sorted = IList.sort entry_compare !t in
let add_and_chk_eq e1 e1' n =
match e1, e1' with
| Sil.Const (Sil.Cint n1), Sil.Const (Sil.Cint n1') -> Sil.Int.eq (n1 ++ n) n1'
| Sil.Const (Sil.Cint n1), Sil.Const (Sil.Cint n1') -> IntLit.eq (n1 ++ n) n1'
| _ -> false in
let add_and_gen_eq e e' n =
let e_plus_n = Sil.BinOp(Sil.PlusA, e, Sil.exp_int n) in
@ -500,7 +500,8 @@ end = struct
let f_ineqs acc (e1, e2, e) =
match e1, e2 with
| Sil.Const (Sil.Cint n1), Sil.Const (Sil.Cint n2) ->
let strict_lower1, upper1 = if Sil.Int.leq n1 n2 then (n1 -- Sil.Int.one, n2) else (n2 -- Sil.Int.one, n1) in
let strict_lower1, upper1 =
if IntLit.leq n1 n2 then (n1 -- IntLit.one, n2) else (n2 -- IntLit.one, n1) in
let e_strict_lower1 = Sil.exp_int strict_lower1 in
let e_upper1 = Sil.exp_int upper1 in
get_induced_atom acc e_strict_lower1 e_upper1 e
@ -592,12 +593,12 @@ end = struct
let f v = match v, side with
| (Sil.BinOp (Sil.PlusA, e1', Sil.Const (Sil.Cint i)), e2, e'), Lhs
when Sil.exp_equal e e1' ->
let c' = Sil.exp_int (Sil.Int.neg i) in
let c' = Sil.exp_int (IntLit.neg i) in
let v' = (e1', Sil.BinOp(Sil.PlusA, e2, c'), Sil.BinOp (Sil.PlusA, e', c')) in
res := v'::!res
| (e1, Sil.BinOp (Sil.PlusA, e2', Sil.Const (Sil.Cint i)), e'), Rhs
when Sil.exp_equal e e2' ->
let c' = Sil.exp_int (Sil.Int.neg i) in
let c' = Sil.exp_int (IntLit.neg i) in
let v' = (Sil.BinOp(Sil.PlusA, e1, c'), e2', Sil.BinOp (Sil.PlusA, e', c')) in
res := v'::!res
| _ -> () in
@ -723,13 +724,13 @@ end = struct
| Sil.Aeq(Sil.BinOp(Sil.Le, e, e'), Sil.Const (Sil.Cint i))
| Sil.Aeq(Sil.Const (Sil.Cint i), Sil.BinOp(Sil.Le, e, e'))
when Sil.Int.isone i && (exp_contains_only_normal_ids e') ->
when IntLit.isone i && (exp_contains_only_normal_ids e') ->
let construct e0 = Prop.mk_inequality (Sil.BinOp(Sil.Le, e0, e')) in
build_other_atoms construct side e
| Sil.Aeq(Sil.BinOp(Sil.Lt, e', e), Sil.Const (Sil.Cint i))
| Sil.Aeq(Sil.Const (Sil.Cint i), Sil.BinOp(Sil.Lt, e', e))
when Sil.Int.isone i && (exp_contains_only_normal_ids e') ->
when IntLit.isone i && (exp_contains_only_normal_ids e') ->
let construct e0 = Prop.mk_inequality (Sil.BinOp(Sil.Lt, e', e0)) in
build_other_atoms construct side e
@ -975,7 +976,7 @@ and length_partial_join len1 len2 = match len1, len2 with
| _ -> exp_partial_join len1 len2
and static_length_partial_join l1 l2 =
option_partial_join (fun len1 len2 -> if Sil.Int.eq len1 len2 then Some len1 else None) l1 l2
option_partial_join (fun len1 len2 -> if IntLit.eq len1 len2 then Some len1 else None) l1 l2
and dynamic_length_partial_join l1 l2 =
option_partial_join (fun len1 len2 -> Some (length_partial_join len1 len2)) l1 l2
@ -1548,8 +1549,12 @@ let rec sigma_partial_meet' (sigma_acc: Prop.sigma) (sigma1_in: Prop.sigma) (sig
let sigma_partial_meet (sigma1: Prop.sigma) (sigma2: Prop.sigma) : Prop.sigma =
sigma_partial_meet' [] sigma1 sigma2
let widening_top = Sil.Int.of_int64 Int64.max_int -- Sil.Int.of_int 1000 (* nearly max_int but not so close to overflow *)
let widening_bottom = Sil.Int.of_int64 Int64.min_int ++ Sil.Int.of_int 1000 (* nearly min_int but not so close to underflow *)
let widening_top =
(* nearly max_int but not so close to overflow *)
IntLit.of_int64 Int64.max_int -- IntLit.of_int 1000
let widening_bottom =
(* nearly min_int but not so close to underflow *)
IntLit.of_int64 Int64.min_int ++ IntLit.of_int 1000
(** {2 Join and Meet for Pi} *)
let pi_partial_join mode
@ -1566,24 +1571,24 @@ let pi_partial_join mode
let len_list = ref [] in
let do_hpred = function
| Sil.Hpointsto (_, Sil.Earray (Sil.Const (Sil.Cint n), _, _), _) ->
(if Sil.Int.geq n Sil.Int.one then len_list := n :: !len_list)
(if IntLit.geq n IntLit.one then len_list := n :: !len_list)
| _ -> () in
IList.iter do_hpred (Prop.get_sigma prop);
!len_list in
let bounds =
let bounds1 = get_array_len ep1 in
let bounds2 = get_array_len ep2 in
let bounds_sorted = IList.sort Sil.Int.compare_value (bounds1@bounds2) in
IList.rev (IList.remove_duplicates Sil.Int.compare_value bounds_sorted) in
let bounds_sorted = IList.sort IntLit.compare_value (bounds1@bounds2) in
IList.rev (IList.remove_duplicates IntLit.compare_value bounds_sorted) in
let widening_atom a =
(* widening heuristic for upper bound: take the length of some array, -2 and -1 *)
match Prop.atom_exp_le_const a, bounds with
| Some (e, n), len :: _ ->
let first_try = Sil.Int.sub len Sil.Int.one in
let second_try = Sil.Int.sub len Sil.Int.two in
let first_try = IntLit.sub len IntLit.one in
let second_try = IntLit.sub len IntLit.two in
let bound =
if Sil.Int.leq n first_try then
if Sil.Int.leq n second_try then second_try else first_try
if IntLit.leq n first_try then
if IntLit.leq n second_try then second_try else first_try
else widening_top in
let a' = Prop.mk_inequality (Sil.BinOp(Sil.Le, e, Sil.exp_int bound)) in
Some a'
@ -1596,18 +1601,19 @@ let pi_partial_join mode
match Prop.atom_const_lt_exp a with
| None -> None
| Some (n, e) ->
let bound = if Sil.Int.leq Sil.Int.minus_one n then Sil.Int.minus_one else widening_bottom in
let bound =
if IntLit.leq IntLit.minus_one n then IntLit.minus_one else widening_bottom in
let a' = Prop.mk_inequality (Sil.BinOp(Sil.Lt, Sil.exp_int bound, e)) in
Some a'
end in
let is_stronger_le e n a =
match Prop.atom_exp_le_const a with
| None -> false
| Some (e', n') -> Sil.exp_equal e e' && Sil.Int.lt n' n in
| Some (e', n') -> Sil.exp_equal e e' && IntLit.lt n' n in
let is_stronger_lt n e a =
match Prop.atom_const_lt_exp a with
| None -> false
| Some (n', e') -> Sil.exp_equal e e' && Sil.Int.lt n n' in
| Some (n', e') -> Sil.exp_equal e e' && IntLit.lt n n' in
let join_atom_check_pre p a =
(* check for atoms in pre mode: fail if the negation is implied by the other side *)
let not_a = Prop.atom_negate a in

3
infer/src/backend/dotty.ml
Unescape View File

@ -327,7 +327,8 @@ let rec dotty_mk_node pe sigma =
let set_exps_neq_zero pi =
let f = function
| Sil.Aneq (e, Sil.Const (Sil.Cint i)) when Sil.Int.iszero i -> exps_neq_zero := e :: !exps_neq_zero
| Sil.Aneq (e, Sil.Const (Sil.Cint i)) when IntLit.iszero i ->
exps_neq_zero := e :: !exps_neq_zero
| _ -> () in
exps_neq_zero := [];
IList.iter f pi

2
infer/src/backend/errdesc.ml
Unescape View File

@ -175,7 +175,7 @@ let rec find_boolean_assignment node pvar true_branch : Cfg.Node.t option =
let find_instr n =
let filter = function
| Sil.Set (Sil.Lvar _pvar, _, Sil.Const (Sil.Cint i), _) when Pvar.equal pvar _pvar ->
Sil.Int.iszero i <> true_branch
IntLit.iszero i <> true_branch
| _ -> false in
IList.exists filter (Cfg.Node.get_instrs n) in
match Cfg.Node.get_preds node with

2
infer/src/backend/errdesc.mli
Unescape View File

@ -90,7 +90,7 @@ val explain_condition_is_assignment : Location.t -> Localise.error_desc
(** explain a condition which is always true or false *)
val explain_condition_always_true_false :
Sil.Int.t -> Sil.exp -> Cfg.Node.t -> Location.t -> Localise.error_desc
IntLit.t -> Sil.exp -> Cfg.Node.t -> Location.t -> Localise.error_desc
(** explain the escape of a stack variable address from its scope *)
val explain_stack_variable_address_escape :

6
infer/src/backend/localise.ml
Unescape View File

@ -372,13 +372,13 @@ let deref_str_array_bound size_opt index_opt =
let tags = Tags.create () in
let size_str_opt = match size_opt with
| Some n ->
let n_str = Sil.Int.to_string n in
let n_str = IntLit.to_string n in
Tags.add tags Tags.array_size n_str;
Some ("of size " ^ n_str)
| None -> None in
let index_str = match index_opt with
| Some n ->
let n_str = Sil.Int.to_string n in
let n_str = IntLit.to_string n in
Tags.add tags Tags.array_index n_str;
"index " ^ n_str
| None -> "an index" in
@ -594,7 +594,7 @@ let desc_condition_always_true_false i cond_str_opt loc =
let value = match cond_str_opt with
| None -> ""
| Some s -> s in
let tt_ff = if Sil.Int.iszero i then "false" else "true" in
let tt_ff = if IntLit.iszero i then "false" else "true" in
Tags.add tags Tags.value value;
let description = Format.sprintf
"Boolean condition %s is always %s %s"

4
infer/src/backend/localise.mli
Unescape View File

@ -156,7 +156,7 @@ val deref_str_freed : Sil.res_action -> deref_str
val deref_str_dangling : Sil.dangling_kind option -> deref_str
(** dereference strings for an array out of bound access *)
val deref_str_array_bound : Sil.Int.t option -> Sil.Int.t option -> deref_str
val deref_str_array_bound : IntLit.t option -> IntLit.t option -> deref_str
(** dereference strings for an uninitialized access whose lhs has the given attribute *)
val deref_str_uninitialized : Sil.attribute option -> deref_str
@ -195,7 +195,7 @@ val desc_comparing_floats_for_equality : Location.t -> error_desc
val desc_condition_is_assignment : Location.t -> error_desc
val desc_condition_always_true_false : Sil.Int.t -> string option -> Location.t -> error_desc
val desc_condition_always_true_false : IntLit.t -> string option -> Location.t -> error_desc
val desc_deallocate_stack_variable : string -> Procname.t -> Location.t -> error_desc

8
infer/src/backend/modelBuiltins.ml
Unescape View File

@ -492,7 +492,7 @@ let execute___objc_counter_update
removed from the list of args. *)
let get_suppress_npe_flag args =
match args with
| (Sil.Const (Sil.Cint i), Sil.Tint Sil.IBool):: args' when Sil.Int.isone i ->
| (Sil.Const (Sil.Cint i), Sil.Tint Sil.IBool):: args' when IntLit.isone i ->
false, args' (* this is a CFRelease/CFRetain *)
| _ -> true, args
@ -504,7 +504,7 @@ let execute___objc_retain_impl
| [(lexp, _)] ->
let prop = return_result lexp prop_ ret_ids in
execute___objc_counter_update
~mask_errors (Sil.PlusA) (Sil.Int.one)
~mask_errors (Sil.PlusA) (IntLit.one)
{ builtin_args with Builtin.prop_ = prop; args = args'; }
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
@ -524,7 +524,7 @@ let execute___objc_release_impl
: Builtin.ret_typ =
let mask_errors, args' = get_suppress_npe_flag args in
execute___objc_counter_update
~mask_errors Sil.MinusA Sil.Int.one
~mask_errors Sil.MinusA IntLit.one
{ builtin_args with Builtin.args = args'; }
let execute___objc_release builtin_args
@ -906,7 +906,7 @@ let execute___split_get_nth { Builtin.pdesc; prop_; path; ret_ids; args; }
let n_lexp3, prop = check_arith_norm_exp pname lexp3 prop___ in
(match n_lexp1, n_lexp2, n_lexp3 with
| Sil.Const (Sil.Cstr str1), Sil.Const (Sil.Cstr str2), Sil.Const (Sil.Cint n_sil) ->
(let n = Sil.Int.to_int n_sil in
(let n = IntLit.to_int n_sil in
try
let parts = Str.split (Str.regexp_string str2) str1 in
let n_part = IList.nth parts n in

154
infer/src/backend/prop.ml
Unescape View File

@ -426,21 +426,21 @@ let sub_normalize sub =
let sub' = Sil.sub_filter_pair f sub in
if Sil.sub_equal sub sub' then sub else sub'
let (--) = Sil.Int.sub
let (++) = Sil.Int.add
let (--) = IntLit.sub
let (++) = IntLit.add
let iszero_int_float = function
| Sil.Cint i -> Sil.Int.iszero i
| Sil.Cint i -> IntLit.iszero i
| Sil.Cfloat 0.0 -> true
| _ -> false
let isone_int_float = function
| Sil.Cint i -> Sil.Int.isone i
| Sil.Cint i -> IntLit.isone i
| Sil.Cfloat 1.0 -> true
| _ -> false
let isminusone_int_float = function
| Sil.Cint i -> Sil.Int.isminusone i
| Sil.Cint i -> IntLit.isminusone i
| Sil.Cfloat (-1.0) -> true
| _ -> false
@ -469,7 +469,7 @@ let sym_eval abs e =
| Sil.UnOp (Sil.LNot, e1, topt) ->
begin
match eval e1 with
| Sil.Const (Sil.Cint i) when Sil.Int.iszero i ->
| Sil.Const (Sil.Cint i) when IntLit.iszero i ->
Sil.exp_one
| Sil.Const (Sil.Cint _) ->
Sil.exp_zero
@ -484,7 +484,7 @@ let sym_eval abs e =
| Sil.UnOp (Sil.Neg, e2', _) ->
e2'
| Sil.Const (Sil.Cint i) ->
Sil.exp_int (Sil.Int.neg i)
Sil.exp_int (IntLit.neg i)
| Sil.Const (Sil.Cfloat v) ->
Sil.exp_float (-. v)
| Sil.Var id ->
@ -498,7 +498,7 @@ let sym_eval abs e =
| Sil.UnOp(Sil.BNot, e2', _) ->
e2'
| Sil.Const (Sil.Cint i) ->
Sil.exp_int (Sil.Int.lognot i)
Sil.exp_int (IntLit.lognot i)
| e1' ->
if abs then Sil.exp_get_undefined false else Sil.UnOp (Sil.BNot, e1', topt)
end
@ -506,7 +506,7 @@ let sym_eval abs e =
begin
match eval e1, eval e2 with
| Sil.Const (Sil.Cint n), Sil.Const (Sil.Cint m) ->
Sil.exp_bool (Sil.Int.leq n m)
Sil.exp_bool (IntLit.leq n m)
| Sil.Const (Sil.Cfloat v), Sil.Const (Sil.Cfloat w) ->
Sil.exp_bool (v <= w)
| Sil.BinOp (Sil.PlusA, e3, Sil.Const (Sil.Cint n)), Sil.Const (Sil.Cint m) ->
@ -518,14 +518,14 @@ let sym_eval abs e =
begin
match eval e1, eval e2 with
| Sil.Const (Sil.Cint n), Sil.Const (Sil.Cint m) ->
Sil.exp_bool (Sil.Int.lt n m)
Sil.exp_bool (IntLit.lt n m)
| Sil.Const (Sil.Cfloat v), Sil.Const (Sil.Cfloat w) ->
Sil.exp_bool (v < w)
| Sil.Const (Sil.Cint n), Sil.BinOp (Sil.MinusA, f1, f2) ->
Sil.BinOp
(Sil.Le, Sil.BinOp (Sil.MinusA, f2, f1), Sil.exp_int (Sil.Int.minus_one -- n))
(Sil.Le, Sil.BinOp (Sil.MinusA, f2, f1), Sil.exp_int (IntLit.minus_one -- n))
| Sil.BinOp(Sil.MinusA, f1 , f2), Sil.Const(Sil.Cint n) ->
Sil.exp_le (Sil.BinOp(Sil.MinusA, f1 , f2)) (Sil.exp_int (n -- Sil.Int.one))
Sil.exp_le (Sil.BinOp(Sil.MinusA, f1 , f2)) (Sil.exp_int (n -- IntLit.one))
| Sil.BinOp (Sil.PlusA, e3, Sil.Const (Sil.Cint n)), Sil.Const (Sil.Cint m) ->
Sil.BinOp (Sil.Lt, e3, Sil.exp_int (m -- n))
| e1', e2' ->
@ -539,7 +539,7 @@ let sym_eval abs e =
begin
match eval e1, eval e2 with
| Sil.Const (Sil.Cint n), Sil.Const (Sil.Cint m) ->
Sil.exp_bool (Sil.Int.eq n m)
Sil.exp_bool (IntLit.eq n m)
| Sil.Const (Sil.Cfloat v), Sil.Const (Sil.Cfloat w) ->
Sil.exp_bool (v = w)
| e1', e2' ->
@ -549,7 +549,7 @@ let sym_eval abs e =
begin
match eval e1, eval e2 with
| Sil.Const (Sil.Cint n), Sil.Const (Sil.Cint m) ->
Sil.exp_bool (Sil.Int.neq n m)
Sil.exp_bool (IntLit.neq n m)
| Sil.Const (Sil.Cfloat v), Sil.Const (Sil.Cfloat w) ->
Sil.exp_bool (v <> w)
| e1', e2' ->
@ -559,11 +559,11 @@ let sym_eval abs e =
let e1' = eval e1 in
let e2' = eval e2 in
begin match e1', e2' with
| Sil.Const (Sil.Cint i), _ when Sil.Int.iszero i ->
| Sil.Const (Sil.Cint i), _ when IntLit.iszero i ->
e1'
| Sil.Const (Sil.Cint _), _ ->
e2'
| _, Sil.Const (Sil.Cint i) when Sil.Int.iszero i ->
| _, Sil.Const (Sil.Cint i) when IntLit.iszero i ->
e2'
| _, Sil.Const (Sil.Cint _) ->
e1'
@ -575,11 +575,11 @@ let sym_eval abs e =
let e2' = eval e2 in
begin
match e1', e2' with
| Sil.Const (Sil.Cint i), _ when Sil.Int.iszero i ->
| Sil.Const (Sil.Cint i), _ when IntLit.iszero i ->
e2'
| Sil.Const (Sil.Cint _), _ ->
e1'
| _, Sil.Const (Sil.Cint i) when Sil.Int.iszero i ->
| _, Sil.Const (Sil.Cint i) when IntLit.iszero i ->
e1'
| _, Sil.Const (Sil.Cint _) ->
e2'
@ -601,12 +601,12 @@ let sym_eval abs e =
let isPlusA = oplus = Sil.PlusA in
let ominus = if isPlusA then Sil.MinusA else Sil.MinusPI in
let (+++) x y = match x, y with
| _, Sil.Const (Sil.Cint i) when Sil.Int.iszero i -> x
| Sil.Const (Sil.Cint i), Sil.Const (Sil.Cint j) -> Sil.Const (Sil.Cint (Sil.Int.add i j))
| _, Sil.Const (Sil.Cint i) when IntLit.iszero i -> x
| Sil.Const (Sil.Cint i), Sil.Const (Sil.Cint j) -> Sil.Const (Sil.Cint (IntLit.add i j))
| _ -> Sil.BinOp (oplus, x, y) in
let (---) x y = match x, y with
| _, Sil.Const (Sil.Cint i) when Sil.Int.iszero i -> x
| Sil.Const (Sil.Cint i), Sil.Const (Sil.Cint j) -> Sil.Const (Sil.Cint (Sil.Int.sub i j))
| _, Sil.Const (Sil.Cint i) when IntLit.iszero i -> x
| Sil.Const (Sil.Cint i), Sil.Const (Sil.Cint j) -> Sil.Const (Sil.Cint (IntLit.sub i j))
| _ -> Sil.BinOp (ominus, x, y) in
(* test if the extensible array at the end of [typ] has elements of type [elt] *)
let extensible_array_element_typ_equal elt typ =
@ -674,7 +674,7 @@ let sym_eval abs e =
| _, Sil.UnOp (Sil.Neg, f2, _) ->
eval (e1 +++ f2)
| _ , Sil.Const(Sil.Cint n) ->
eval (e1' +++ (Sil.exp_int (Sil.Int.neg n)))
eval (e1' +++ (Sil.exp_int (IntLit.neg n)))
| Sil.Const _, _ ->
e1' --- e2'
| Sil.Var _, Sil.Var _ ->
@ -703,7 +703,7 @@ let sym_eval abs e =
| _, Sil.Const c when isminusone_int_float c ->
eval (Sil.UnOp (Sil.Neg, e1', None))
| Sil.Const (Sil.Cint n), Sil.Const (Sil.Cint m) ->
Sil.exp_int (Sil.Int.mul n m)
Sil.exp_int (IntLit.mul n m)
| Sil.Const (Sil.Cfloat v), Sil.Const (Sil.Cfloat w) ->
Sil.exp_float (v *. w)
| Sil.Var _, Sil.Var _ ->
@ -726,7 +726,7 @@ let sym_eval abs e =
| _, Sil.Const c when isone_int_float c ->
e1'
| Sil.Const (Sil.Cint n), Sil.Const (Sil.Cint m) ->
Sil.exp_int (Sil.Int.div n m)
Sil.exp_int (IntLit.div n m)
| Sil.Const (Sil.Cfloat v), Sil.Const (Sil.Cfloat w) ->
Sil.exp_float (v /.w)
| Sil.Sizeof (Sil.Tarray (elt, _), Some len, _), Sil.Sizeof (elt2, None, _)
@ -745,14 +745,14 @@ let sym_eval abs e =
let e2' = eval e2 in
begin
match e1', e2' with
| _, Sil.Const (Sil.Cint i) when Sil.Int.iszero i ->
| _, Sil.Const (Sil.Cint i) when IntLit.iszero i ->
Sil.exp_get_undefined false
| Sil.Const (Sil.Cint i), _ when Sil.Int.iszero i ->
| Sil.Const (Sil.Cint i), _ when IntLit.iszero i ->
e1'
| _, Sil.Const (Sil.Cint i) when Sil.Int.isone i ->
| _, Sil.Const (Sil.Cint i) when IntLit.isone i ->
Sil.exp_zero
| Sil.Const (Sil.Cint n), Sil.Const (Sil.Cint m) ->
Sil.exp_int (Sil.Int.rem n m)
Sil.exp_int (IntLit.rem n m)
| _ ->
if abs then Sil.exp_get_undefined false else Sil.BinOp (Sil.Mod, e1', e2')
end
@ -764,12 +764,12 @@ let sym_eval abs e =
let e1' = eval e1 in
let e2' = eval e2 in
begin match e1', e2' with
| Sil.Const (Sil.Cint i), _ when Sil.Int.iszero i ->
| Sil.Const (Sil.Cint i), _ when IntLit.iszero i ->
e1'
| _, Sil.Const (Sil.Cint i) when Sil.Int.iszero i ->
| _, Sil.Const (Sil.Cint i) when IntLit.iszero i ->
e2'
| Sil.Const (Sil.Cint i1), Sil.Const(Sil.Cint i2) ->
Sil.exp_int (Sil.Int.logand i1 i2)
Sil.exp_int (IntLit.logand i1 i2)
| _ ->
if abs then Sil.exp_get_undefined false else Sil.BinOp (Sil.BAnd, e1', e2')
end
@ -777,12 +777,12 @@ let sym_eval abs e =
let e1' = eval e1 in
let e2' = eval e2 in
begin match e1', e2' with
| Sil.Const (Sil.Cint i), _ when Sil.Int.iszero i ->
| Sil.Const (Sil.Cint i), _ when IntLit.iszero i ->
e2'
| _, Sil.Const (Sil.Cint i) when Sil.Int.iszero i ->
| _, Sil.Const (Sil.Cint i) when IntLit.iszero i ->
e1'
| Sil.Const (Sil.Cint i1), Sil.Const(Sil.Cint i2) ->
Sil.exp_int (Sil.Int.logor i1 i2)
Sil.exp_int (IntLit.logor i1 i2)
| _ ->
if abs then Sil.exp_get_undefined false else Sil.BinOp (Sil.BOr, e1', e2')
end
@ -790,12 +790,12 @@ let sym_eval abs e =
let e1' = eval e1 in
let e2' = eval e2 in
begin match e1', e2' with
| Sil.Const (Sil.Cint i), _ when Sil.Int.iszero i ->
| Sil.Const (Sil.Cint i), _ when IntLit.iszero i ->
e2'
| _, Sil.Const (Sil.Cint i) when Sil.Int.iszero i ->
| _, Sil.Const (Sil.Cint i) when IntLit.iszero i ->
e1'
| Sil.Const (Sil.Cint i1), Sil.Const(Sil.Cint i2) ->
Sil.exp_int (Sil.Int.logxor i1 i2)
Sil.exp_int (IntLit.logxor i1 i2)
| _ ->
if abs then Sil.exp_get_undefined false else Sil.BinOp (Sil.BXor, e1', e2')
end
@ -806,7 +806,7 @@ let sym_eval abs e =
match e2' with
| Sil.Const (Sil.Cptr_to_fld (fn, typ)) ->
eval (Sil.Lfield(e1', fn, typ))
| Sil.Const (Sil.Cint i) when Sil.Int.iszero i ->
| Sil.Const (Sil.Cint i) when IntLit.iszero i ->
Sil.exp_zero (* cause a NULL dereference *)
| _ -> Sil.BinOp (Sil.PtrFld, e1', e2')
end
@ -852,21 +852,21 @@ let exp_normalize_noabs sub exp =
(** Return [true] if the atom is an inequality *)
let atom_is_inequality = function
| Sil.Aeq (Sil.BinOp (Sil.Le, _, _), Sil.Const (Sil.Cint i)) when Sil.Int.isone i -> true
| Sil.Aeq (Sil.BinOp (Sil.Lt, _, _), Sil.Const (Sil.Cint i)) when Sil.Int.isone i -> true
| Sil.Aeq (Sil.BinOp (Sil.Le, _, _), Sil.Const (Sil.Cint i)) when IntLit.isone i -> true
| Sil.Aeq (Sil.BinOp (Sil.Lt, _, _), Sil.Const (Sil.Cint i)) when IntLit.isone i -> true
| _ -> false
(** If the atom is [e<=n] return [e,n] *)
let atom_exp_le_const = function
| Sil.Aeq(Sil.BinOp (Sil.Le, e1, Sil.Const (Sil.Cint n)), Sil.Const (Sil.Cint i))
when Sil.Int.isone i ->
when IntLit.isone i ->
Some (e1, n)
| _ -> None
(** If the atom is [n<e] return [n,e] *)
let atom_const_lt_exp = function
| Sil.Aeq(Sil.BinOp (Sil.Lt, Sil.Const (Sil.Cint n), e1), Sil.Const (Sil.Cint i))
when Sil.Int.isone i ->
when IntLit.isone i ->
Some (n, e1)
| _ -> None
@ -890,12 +890,12 @@ let mk_inequality e =
let new_e = Sil.BinOp (Sil.Le, base', new_offset) in
Sil.Aeq (new_e, Sil.exp_one)
| Sil.BinOp(Sil.MinusA, Sil.Const (Sil.Cint n'), base') ->
let new_offset = Sil.exp_int (n' -- n -- Sil.Int.one) in
let new_offset = Sil.exp_int (n' -- n -- IntLit.one) in
let new_e = Sil.BinOp (Sil.Lt, new_offset, base') in
Sil.Aeq (new_e, Sil.exp_one)
| Sil.UnOp(Sil.Neg, new_base, _) ->
(* In this case, base = -new_base. Construct -n-1 < new_base. *)
let new_offset = Sil.exp_int (Sil.Int.zero -- n -- Sil.Int.one) in
let new_offset = Sil.exp_int (IntLit.zero -- n -- IntLit.one) in
let new_e = Sil.BinOp (Sil.Lt, new_offset, new_base) in
Sil.Aeq (new_e, Sil.exp_one)
| _ -> Sil.Aeq (e, Sil.exp_one))
@ -916,12 +916,12 @@ let mk_inequality e =
let new_e = Sil.BinOp (Sil.Lt, new_offset, base') in
Sil.Aeq (new_e, Sil.exp_one)
| Sil.BinOp(Sil.MinusA, Sil.Const (Sil.Cint n'), base') ->
let new_offset = Sil.exp_int (n' -- n -- Sil.Int.one) in
let new_offset = Sil.exp_int (n' -- n -- IntLit.one) in
let new_e = Sil.BinOp (Sil.Le, base', new_offset) in
Sil.Aeq (new_e, Sil.exp_one)
| Sil.UnOp(Sil.Neg, new_base, _) ->
(* In this case, base = -new_base. Construct new_base <= -n-1 *)
let new_offset = Sil.exp_int (Sil.Int.zero -- n -- Sil.Int.one) in
let new_offset = Sil.exp_int (IntLit.zero -- n -- IntLit.one) in
let new_e = Sil.BinOp (Sil.Le, new_base, new_offset) in
Sil.Aeq (new_e, Sil.exp_one)
| _ -> Sil.Aeq (e, Sil.exp_one))
@ -946,8 +946,8 @@ let inequality_normalize a =
(pos1@neg2, neg1@pos2, n1 -- n2)
| Sil.UnOp(Sil.Neg, e1, _) ->
let pos1, neg1, n1 = exp_to_posnegoff e1 in
(neg1, pos1, Sil.Int.zero -- n1)
| _ -> [e],[], Sil.Int.zero in
(neg1, pos1, IntLit.zero -- n1)
| _ -> [e],[], IntLit.zero in
(** sort and filter out expressions appearing in both the positive and negative part *)
let normalize_posnegoff (pos, neg, off) =
let pos' = IList.sort Sil.exp_compare pos in
@ -969,13 +969,13 @@ let inequality_normalize a =
let norm_from_exp e =
match normalize_posnegoff (exp_to_posnegoff e) with
| [],[], n -> Sil.BinOp(Sil.Le, Sil.exp_int n, Sil.exp_zero)
| [], neg, n -> Sil.BinOp(Sil.Lt, Sil.exp_int (n -- Sil.Int.one), exp_list_to_sum neg)
| pos, [], n -> Sil.BinOp(Sil.Le, exp_list_to_sum pos, Sil.exp_int (Sil.Int.zero -- n))
| [], neg, n -> Sil.BinOp(Sil.Lt, Sil.exp_int (n -- IntLit.one), exp_list_to_sum neg)
| pos, [], n -> Sil.BinOp(Sil.Le, exp_list_to_sum pos, Sil.exp_int (IntLit.zero -- n))
| pos, neg, n ->
let lhs_e = Sil.BinOp(Sil.MinusA, exp_list_to_sum pos, exp_list_to_sum neg) in
Sil.BinOp(Sil.Le, lhs_e, Sil.exp_int (Sil.Int.zero -- n)) in
Sil.BinOp(Sil.Le, lhs_e, Sil.exp_int (IntLit.zero -- n)) in
let ineq = match a with
| Sil.Aeq (ineq, Sil.Const (Sil.Cint i)) when Sil.Int.isone i ->
| Sil.Aeq (ineq, Sil.Const (Sil.Cint i)) when IntLit.isone i ->
ineq
| _ -> assert false in
match ineq with
@ -1018,7 +1018,7 @@ let atom_normalize sub a0 =
let handle_unary_negation e1 e2 =
match e1, e2 with
| Sil.UnOp (Sil.LNot, e1', _), Sil.Const (Sil.Cint i)
| Sil.Const (Sil.Cint i), Sil.UnOp (Sil.LNot, e1', _) when Sil.Int.iszero i ->
| Sil.Const (Sil.Cint i), Sil.UnOp (Sil.LNot, e1', _) when IntLit.iszero i ->
(e1', Sil.exp_zero, true)
| _ -> (e1, e2, false) in
let handle_boolean_operation from_equality e1 e2 =
@ -1042,9 +1042,9 @@ let atom_normalize sub a0 =
(** Negate an atom *)
let atom_negate = function
| Sil.Aeq (Sil.BinOp (Sil.Le, e1, e2), Sil.Const (Sil.Cint i)) when Sil.Int.isone i ->
| Sil.Aeq (Sil.BinOp (Sil.Le, e1, e2), Sil.Const (Sil.Cint i)) when IntLit.isone i ->
mk_inequality (Sil.exp_lt e2 e1)
| Sil.Aeq (Sil.BinOp (Sil.Lt, e1, e2), Sil.Const (Sil.Cint i)) when Sil.Int.isone i ->
| Sil.Aeq (Sil.BinOp (Sil.Lt, e1, e2), Sil.Const (Sil.Cint i)) when IntLit.isone i ->
mk_inequality (Sil.exp_le e2 e1)
| Sil.Aeq (e1, e2) -> Sil.Aneq (e1, e2)
| Sil.Aneq (e1, e2) -> Sil.Aeq (e1, e2)
@ -1217,7 +1217,7 @@ let pi_tighten_ineq pi =
| _ -> acc in
IList.fold_left get_disequality_info [] nonineq_list in
let is_neq e n =
IList.exists (fun (e', n') -> Sil.exp_equal e e' && Sil.Int.eq n n') diseq_list in
IList.exists (fun (e', n') -> Sil.exp_equal e e' && IntLit.eq n n') diseq_list in
let le_list_tightened =
let get_le_inequality_info acc a =
match atom_exp_le_const a with
@ -1226,7 +1226,7 @@ let pi_tighten_ineq pi =
let rec le_tighten le_list_done = function
| [] -> IList.rev le_list_done
| (e, n):: le_list_todo -> (* e <= n *)
if is_neq e n then le_tighten le_list_done ((e, n -- Sil.Int.one):: le_list_todo)
if is_neq e n then le_tighten le_list_done ((e, n -- IntLit.one):: le_list_todo)
else le_tighten ((e, n):: le_list_done) (le_list_todo) in
let le_list = IList.rev (IList.fold_left get_le_inequality_info [] ineq_list) in
le_tighten [] le_list in
@ -1238,8 +1238,8 @@ let pi_tighten_ineq pi =
let rec lt_tighten lt_list_done = function
| [] -> IList.rev lt_list_done
| (n, e):: lt_list_todo -> (* n < e *)
let n_plus_one = n ++ Sil.Int.one in
if is_neq e n_plus_one then lt_tighten lt_list_done ((n ++ Sil.Int.one, e):: lt_list_todo)
let n_plus_one = n ++ IntLit.one in
if is_neq e n_plus_one then lt_tighten lt_list_done ((n ++ IntLit.one, e):: lt_list_todo)
else lt_tighten ((n, e):: lt_list_done) (lt_list_todo) in
let lt_list = IList.rev (IList.fold_left get_lt_inequality_info [] ineq_list) in
lt_tighten [] lt_list in
@ -1259,10 +1259,10 @@ let pi_tighten_ineq pi =
| Sil.Aneq(Sil.Const (Sil.Cint n), e)
| Sil.Aneq(e, Sil.Const (Sil.Cint n)) ->
(not (IList.exists
(fun (e', n') -> Sil.exp_equal e e' && Sil.Int.lt n' n)
(fun (e', n') -> Sil.exp_equal e e' && IntLit.lt n' n)
le_list_tightened)) &&
(not (IList.exists
(fun (n', e') -> Sil.exp_equal e e' && Sil.Int.leq n n')
(fun (n', e') -> Sil.exp_equal e e' && IntLit.leq n n')
lt_list_tightened))
| _ -> true)
nonineq_list in
@ -1272,13 +1272,13 @@ let pi_tighten_ineq pi =
let rec pi_sorted_remove_redundant = function
| (Sil.Aeq(Sil.BinOp (Sil.Le, e1, Sil.Const (Sil.Cint n1)), Sil.Const (Sil.Cint i1)) as a1) ::
Sil.Aeq(Sil.BinOp (Sil.Le, e2, Sil.Const (Sil.Cint n2)), Sil.Const (Sil.Cint i2)) :: rest
when Sil.Int.isone i1 && Sil.Int.isone i2 && Sil.exp_equal e1 e2 && Sil.Int.lt n1 n2 ->
when IntLit.isone i1 && IntLit.isone i2 && Sil.exp_equal e1 e2 && IntLit.lt n1 n2 ->
(* second inequality redundant *)
pi_sorted_remove_redundant (a1 :: rest)
| Sil.Aeq(Sil.BinOp (Sil.Lt, Sil.Const (Sil.Cint n1), e1), Sil.Const (Sil.Cint i1)) ::
(Sil.Aeq(Sil.BinOp (Sil.Lt, Sil.Const (Sil.Cint n2), e2), Sil.Const (Sil.Cint i2)) as a2) ::
rest
when Sil.Int.isone i1 && Sil.Int.isone i2 && Sil.exp_equal e1 e2 && Sil.Int.lt n1 n2 ->
when IntLit.isone i1 && IntLit.isone i2 && Sil.exp_equal e1 e2 && IntLit.lt n1 n2 ->
(* first inequality redundant *)
pi_sorted_remove_redundant (a2 :: rest)
| a1:: a2:: rest ->
@ -1311,17 +1311,17 @@ let pi_normalize sub sigma pi0 =
when Sil.exp_equal e1 e2 ->
Sil.binop_injective op2 &&
Sil.binop_is_zero_runit op2 &&
not (Sil.const_equal (Sil.Cint Sil.Int.zero) c2)
not (Sil.const_equal (Sil.Cint IntLit.zero) c2)
| Sil.BinOp(op1, e1, Sil.Const(c1)), e2
when Sil.exp_equal e1 e2 ->
Sil.binop_injective op1 &&
Sil.binop_is_zero_runit op1 &&
not (Sil.const_equal (Sil.Cint Sil.Int.zero) c1)
not (Sil.const_equal (Sil.Cint IntLit.zero) c1)
| _ -> false in
let filter_useful_atom =
let unsigned_exps = lazy (sigma_get_unsigned_exps sigma) in
function
| Sil.Aneq ((Sil.Var _) as e, Sil.Const (Sil.Cint n)) when Sil.Int.isnegative n ->
| Sil.Aneq ((Sil.Var _) as e, Sil.Const (Sil.Cint n)) when IntLit.isnegative n ->
not (IList.exists (Sil.exp_equal e) (Lazy.force unsigned_exps))
| Sil.Aneq(e1, e2) ->
not (syntactically_different (e1, e2))
@ -1681,18 +1681,18 @@ let normalize_and_strengthen_atom (p : normal t) (a : Sil.atom) : Sil.atom =
let a' = atom_normalize p.sub a in
match a' with
| Sil.Aeq (Sil.BinOp (Sil.Le, Sil.Var id, Sil.Const (Sil.Cint n)), Sil.Const (Sil.Cint i))
when Sil.Int.isone i ->
let lower = Sil.exp_int (n -- Sil.Int.one) in
when IntLit.isone i ->
let lower = Sil.exp_int (n -- IntLit.one) in
let a_lower = Sil.Aeq (Sil.BinOp (Sil.Lt, lower, Sil.Var id), Sil.exp_one) in
if not (IList.mem Sil.atom_equal a_lower p.pi) then a'
else Sil.Aeq (Sil.Var id, Sil.exp_int n)
| Sil.Aeq (Sil.BinOp (Sil.Lt, Sil.Const (Sil.Cint n), Sil.Var id), Sil.Const (Sil.Cint i))
when Sil.Int.isone i ->
let upper = Sil.exp_int (n ++ Sil.Int.one) in
when IntLit.isone i ->
let upper = Sil.exp_int (n ++ IntLit.one) in
let a_upper = Sil.Aeq (Sil.BinOp (Sil.Le, Sil.Var id, upper), Sil.exp_one) in
if not (IList.mem Sil.atom_equal a_upper p.pi) then a'
else Sil.Aeq (Sil.Var id, upper)
| Sil.Aeq (Sil.BinOp (Sil.Ne, e1, e2), Sil.Const (Sil.Cint i)) when Sil.Int.isone i ->
| Sil.Aeq (Sil.BinOp (Sil.Ne, e1, e2), Sil.Const (Sil.Cint i)) when IntLit.isone i ->
Sil.Aneq (e1, e2)
| _ -> a'
@ -2190,7 +2190,7 @@ let compute_reindexing fav_add get_id_offset list =
let transform x =
let id, offset = match get_id_offset x with None -> assert false | Some io -> io in
let base_new = Sil.Var (Ident.create_fresh Ident.kprimed) in
let offset_new = Sil.exp_int (Sil.Int.neg offset) in
let offset_new = Sil.exp_int (IntLit.neg offset) in
let exp_new = Sil.BinOp(Sil.PlusA, base_new, offset_new) in
(id, exp_new) in
let reindexing = IList.map transform list_passed in
@ -2227,7 +2227,7 @@ let prop_rename_array_indices prop =
match e1, e2 with
| Sil.BinOp(Sil.PlusA, e1', Sil.Const (Sil.Cint n1')),
Sil.BinOp(Sil.PlusA, e2', Sil.Const (Sil.Cint n2')) ->
not (Sil.exp_equal e1' e2' && Sil.Int.lt n1' n2')
not (Sil.exp_equal e1' e2' && IntLit.lt n1' n2')
| _ -> true in
let rec select_minimal_indices indices_seen = function
| [] -> IList.rev indices_seen
@ -2781,8 +2781,8 @@ let trans_land_lor op ((idl1, stml1), e1) ((idl2, stml2), e2) loc =
let id = Ident.create_fresh Ident.knormal in
let prune_instr1, prune_res1, prune_instr2, prune_res2 =
let cond1, cond2, res = match op with
| Sil.LAnd -> e1, Sil.UnOp(Sil.LNot, e1, None), Sil.Int.zero
| Sil.LOr -> Sil.UnOp(Sil.LNot, e1, None), e1, Sil.Int.one
| Sil.LAnd -> e1, Sil.UnOp(Sil.LNot, e1, None), IntLit.zero
| Sil.LOr -> Sil.UnOp(Sil.LNot, e1, None), e1, IntLit.one
| _ -> assert false in
let cond_res1 = Sil.BinOp(Sil.Eq, Sil.Var id, e2) in
let cond_res2 = Sil.BinOp(Sil.Eq, Sil.Var id, Sil.exp_int res) in
@ -2834,7 +2834,7 @@ let find_equal_formal_path e prop =
(** translate an if-then-else expression *)
let trans_if_then_else ((idl1, stml1), e1) ((idl2, stml2), e2) ((idl3, stml3), e3) loc =
match sym_eval false e1 with
| Sil.Const (Sil.Cint i) when Sil.Int.iszero i -> (idl1@idl3, stml1@stml3), e3
| Sil.Const (Sil.Cint i) when IntLit.iszero i -> (idl1@idl3, stml1@stml3), e3
| Sil.Const (Sil.Cint _) -> (idl1@idl2, stml1@stml2), e2
| _ ->
let e1not = Sil.UnOp(Sil.LNot, e1, None) in

4
infer/src/backend/prop.mli
Unescape View File

@ -151,10 +151,10 @@ val mk_inequality : Sil.exp -> Sil.atom
val atom_is_inequality : Sil.atom -> bool
(** If the atom is [e<=n] return [e,n] *)
val atom_exp_le_const : Sil.atom -> (Sil.exp * Sil.Int.t) option
val atom_exp_le_const : Sil.atom -> (Sil.exp * IntLit.t) option
(** If the atom is [n<e] return [n,e] *)
val atom_const_lt_exp : Sil.atom -> (Sil.Int.t * Sil.exp) option
val atom_const_lt_exp : Sil.atom -> (IntLit.t * Sil.exp) option
(** Negate an atom *)
val atom_negate : Sil.atom -> Sil.atom

107
infer/src/backend/prover.ml
Unescape View File

@ -20,10 +20,10 @@ let decrease_indent_when_exception thunk =
with exn when SymOp.exn_not_failure exn -> (L.d_decrease_indent 1; raise exn)
let compute_max_from_nonempty_int_list l =
IList.hd (IList.rev (IList.sort Sil.Int.compare_value l))
IList.hd (IList.rev (IList.sort IntLit.compare_value l))
let compute_min_from_nonempty_int_list l =
IList.hd (IList.sort Sil.Int.compare_value l)
IList.hd (IList.sort IntLit.compare_value l)
let exp_pair_compare (e1, e2) (f1, f2) =
let c1 = Sil.exp_compare e1 f1 in
@ -47,8 +47,8 @@ let rec is_java_class = function
(** {2 Ordinary Theorem Proving} *)
let (++) = Sil.Int.add
let (--) = Sil.Int.sub
let (++) = IntLit.add
let (--) = IntLit.sub
(** Reasoning about constraints of the form x-y <= n *)
@ -57,31 +57,31 @@ module DiffConstr : sig
type t
val to_leq : t -> Sil.exp * Sil.exp
val to_lt : t -> Sil.exp * Sil.exp
val to_triple : t -> Sil.exp * Sil.exp * Sil.Int.t
val to_triple : t -> Sil.exp * Sil.exp * IntLit.t
val from_leq : t list -> Sil.exp * Sil.exp -> t list
val from_lt : t list -> Sil.exp * Sil.exp -> t list
val saturate : t list -> bool * t list
end = struct
type t = Sil.exp * Sil.exp * Sil.Int.t
type t = Sil.exp * Sil.exp * IntLit.t
let compare (e1, e2, n) (f1, f2, m) =
let c1 = exp_pair_compare (e1, e2) (f1, f2) in
if c1 <> 0 then c1 else Sil.Int.compare_value n m
if c1 <> 0 then c1 else IntLit.compare_value n m
let equal entry1 entry2 = compare entry1 entry2 = 0
let to_leq (e1, e2, n) =
Sil.BinOp(Sil.MinusA, e1, e2), Sil.exp_int n
let to_lt (e1, e2, n) =
Sil.exp_int (Sil.Int.zero -- n -- Sil.Int.one), Sil.BinOp(Sil.MinusA, e2, e1)
Sil.exp_int (IntLit.zero -- n -- IntLit.one), Sil.BinOp(Sil.MinusA, e2, e1)
let to_triple entry = entry
let from_leq acc (e1, e2) =
match e1, e2 with
| Sil.BinOp(Sil.MinusA, (Sil.Var id11 as e11), (Sil.Var id12 as e12)), Sil.Const (Sil.Cint n)
when not (Ident.equal id11 id12) ->
(match Sil.Int.to_signed n with
(match IntLit.to_signed n with
| None -> acc (* ignore: constraint algorithm only terminates on signed integers *)
| Some n' ->
(e11, e12, n') :: acc)
@ -90,10 +90,10 @@ end = struct
match e1, e2 with
| Sil.Const (Sil.Cint n), Sil.BinOp(Sil.MinusA, (Sil.Var id21 as e21), (Sil.Var id22 as e22))
when not (Ident.equal id21 id22) ->
(match Sil.Int.to_signed n with
(match IntLit.to_signed n with
| None -> acc (* ignore: constraint algorithm only terminates on signed integers *)
| Some n' ->
let m = Sil.Int.zero -- n' -- Sil.Int.one in
let m = IntLit.zero -- n' -- IntLit.one in
(e22, e21, m) :: acc)
| _ -> acc
@ -102,7 +102,7 @@ end = struct
| (f1, f2, m):: rest ->
let equal_e2_f1 = Sil.exp_equal e2 f1 in
let equal_e1_f2 = Sil.exp_equal e1 f2 in
if equal_e2_f1 && equal_e1_f2 && Sil.Int.lt (n ++ m) Sil.Int.zero then
if equal_e2_f1 && equal_e1_f2 && IntLit.lt (n ++ m) IntLit.zero then
true, [] (* constraints are inconsistent *)
else if equal_e2_f1 && equal_e1_f2 then
generate constr acc rest
@ -133,7 +133,7 @@ end = struct
let e1, e2, n = constr in
let f1, f2, m = constr' in
let c1 = exp_pair_compare (e1, e2) (f1, f2) in
if c1 = 0 && Sil.Int.lt n m then
if c1 = 0 && IntLit.lt n m then
combine acc_todos acc_seen constraints_new rest'
else if c1 = 0 then
combine acc_todos acc_seen rest constraints_old
@ -212,11 +212,11 @@ module Inequalities : sig
(** Check [t |- e1<e2]. Result [false] means "don't know". *)
val check_lt : t -> Sil.exp -> Sil.exp -> bool
(** Find a Sil.Int.t n such that [t |- e<=n] if possible. *)
val compute_upper_bound : t -> Sil.exp -> Sil.Int.t option
(** Find a IntLit.t n such that [t |- e<=n] if possible. *)
val compute_upper_bound : t -> Sil.exp -> IntLit.t option
(** Find a Sil.Int.t n such that [t |- n<e] if possible. *)
val compute_lower_bound : t -> Sil.exp -> Sil.Int.t option
(** Find a IntLit.t n such that [t |- n<e] if possible. *)
val compute_lower_bound : t -> Sil.exp -> IntLit.t option
(** Return [true] if a simple inconsistency is detected *)
val inconsistent : t -> bool
@ -265,7 +265,7 @@ end = struct
let have_same_key leq1 leq2 =
match leq1, leq2 with
| (e1, Sil.Const (Sil.Cint n1)), (e2, Sil.Const (Sil.Cint n2)) ->
Sil.exp_equal e1 e2 && Sil.Int.leq n1 n2
Sil.exp_equal e1 e2 && IntLit.leq n1 n2
| _, _ -> false in
remove_redundancy have_same_key [] leqs_sorted
let lts_sort_then_remove_redundancy lts =
@ -273,7 +273,7 @@ end = struct
let have_same_key lt1 lt2 =
match lt1, lt2 with
| (Sil.Const (Sil.Cint n1), e1), (Sil.Const (Sil.Cint n2), e2) ->
Sil.exp_equal e1 e2 && Sil.Int.geq n1 n2
Sil.exp_equal e1 e2 && IntLit.geq n1 n2
| _, _ -> false in
remove_redundancy have_same_key [] lts_sorted
@ -289,12 +289,12 @@ end = struct
let umap_add umap e new_upper =
try
let old_upper = Sil.ExpMap.find e umap in
if Sil.Int.leq old_upper new_upper then umap else Sil.ExpMap.add e new_upper umap
if IntLit.leq old_upper new_upper then umap else Sil.ExpMap.add e new_upper umap
with Not_found -> Sil.ExpMap.add e new_upper umap in
let lmap_add lmap e new_lower =
try
let old_lower = Sil.ExpMap.find e lmap in
if Sil.Int.geq old_lower new_lower then lmap else Sil.ExpMap.add e new_lower lmap
if IntLit.geq old_lower new_lower then lmap else Sil.ExpMap.add e new_lower lmap
with Not_found -> Sil.ExpMap.add e new_lower lmap in
let rec umap_create_from_leqs umap = function
| [] -> umap
@ -325,7 +325,7 @@ end = struct
try
let e1, e2, n = DiffConstr.to_triple constr (* e2 - e1 > -n-1 *) in
let lower1 = Sil.ExpMap.find e1 lmap in
let new_lower2 = lower1 -- n -- Sil.Int.one in
let new_lower2 = lower1 -- n -- IntLit.one in
let new_lmap = lmap_add lmap e2 new_lower2 in
lmap_improve_by_difference_constraints new_lmap constrs_rest
with Not_found ->
@ -357,9 +357,9 @@ end = struct
let process_atom = function
| Sil.Aneq (e1, e2) -> (* != *)
neqs := (e1, e2) :: !neqs
| Sil.Aeq (Sil.BinOp (Sil.Le, e1, e2), Sil.Const (Sil.Cint i)) when Sil.Int.isone i -> (* <= *)
| Sil.Aeq (Sil.BinOp (Sil.Le, e1, e2), Sil.Const (Sil.Cint i)) when IntLit.isone i -> (* <= *)
leqs := (e1, e2) :: !leqs
| Sil.Aeq (Sil.BinOp (Sil.Lt, e1, e2), Sil.Const (Sil.Cint i)) when Sil.Int.isone i -> (* < *)
| Sil.Aeq (Sil.BinOp (Sil.Lt, e1, e2), Sil.Const (Sil.Cint i)) when IntLit.isone i -> (* < *)
lts := (e1, e2) :: !lts
| Sil.Aeq _ -> () in
IList.iter process_atom pi;
@ -414,18 +414,19 @@ end = struct
let check_le { leqs = leqs; lts = lts; neqs = _ } e1 e2 =
(* L.d_str "check_le "; Sil.d_exp e1; L.d_str " "; Sil.d_exp e2; L.d_ln (); *)
match e1, e2 with
| Sil.Const (Sil.Cint n1), Sil.Const (Sil.Cint n2) -> Sil.Int.leq n1 n2
| Sil.Const (Sil.Cint n1), Sil.Const (Sil.Cint n2) -> IntLit.leq n1 n2
| Sil.BinOp (Sil.MinusA, Sil.Sizeof (t1, None, _), Sil.Sizeof (t2, None, _)),
Sil.Const(Sil.Cint n2)
when Sil.Int.isminusone n2 && type_size_comparable t1 t2 -> (* [ sizeof(t1) - sizeof(t2) <= -1 ] *)
when IntLit.isminusone n2 && type_size_comparable t1 t2 ->
(* [ sizeof(t1) - sizeof(t2) <= -1 ] *)
check_type_size_lt t1 t2
| e, Sil.Const (Sil.Cint n) -> (* [e <= n' <= n |- e <= n] *)
IList.exists (function
| e', Sil.Const (Sil.Cint n') -> Sil.exp_equal e e' && Sil.Int.leq n' n
| e', Sil.Const (Sil.Cint n') -> Sil.exp_equal e e' && IntLit.leq n' n
| _, _ -> false) leqs
| Sil.Const (Sil.Cint n), e -> (* [ n-1 <= n' < e |- n <= e] *)
IList.exists (function
| Sil.Const (Sil.Cint n'), e' -> Sil.exp_equal e e' && Sil.Int.leq (n -- Sil.Int.one) n'
| Sil.Const (Sil.Cint n'), e' -> Sil.exp_equal e e' && IntLit.leq (n -- IntLit.one) n'
| _, _ -> false) lts
| _ -> Sil.exp_equal e1 e2
@ -433,14 +434,14 @@ end = struct
let check_lt { leqs = leqs; lts = lts; neqs = _ } e1 e2 =
(* L.d_str "check_lt "; Sil.d_exp e1; L.d_str " "; Sil.d_exp e2; L.d_ln (); *)
match e1, e2 with
| Sil.Const (Sil.Cint n1), Sil.Const (Sil.Cint n2) -> Sil.Int.lt n1 n2
| Sil.Const (Sil.Cint n1), Sil.Const (Sil.Cint n2) -> IntLit.lt n1 n2
| Sil.Const (Sil.Cint n), e -> (* [n <= n' < e |- n < e] *)
IList.exists (function
| Sil.Const (Sil.Cint n'), e' -> Sil.exp_equal e e' && Sil.Int.leq n n'
| Sil.Const (Sil.Cint n'), e' -> Sil.exp_equal e e' && IntLit.leq n n'
| _, _ -> false) lts
| e, Sil.Const (Sil.Cint n) -> (* [e <= n' <= n-1 |- e < n] *)
IList.exists (function
| e', Sil.Const (Sil.Cint n') -> Sil.exp_equal e e' && Sil.Int.leq n' (n -- Sil.Int.one)
| e', Sil.Const (Sil.Cint n') -> Sil.exp_equal e e' && IntLit.leq n' (n -- IntLit.one)
| _, _ -> false) leqs
| _ -> false
@ -449,7 +450,7 @@ end = struct
let e1, e2 = if Sil.exp_compare _e1 _e2 <= 0 then _e1, _e2 else _e2, _e1 in
IList.exists (exp_pair_eq (e1, e2)) ineq.neqs || check_lt ineq e1 e2 || check_lt ineq e2 e1
(** Find a Sil.Int.t n such that [t |- e<=n] if possible. *)
(** Find a IntLit.t n such that [t |- e<=n] if possible. *)
let compute_upper_bound { leqs = leqs; lts = _; neqs = _ } e1 =
match e1 with
| Sil.Const (Sil.Cint n1) -> Some n1
@ -465,11 +466,11 @@ end = struct
if upper_list == [] then None
else Some (compute_min_from_nonempty_int_list upper_list)
(** Find a Sil.Int.t n such that [t |- n < e] if possible. *)
(** Find a IntLit.t n such that [t |- n < e] if possible. *)
let compute_lower_bound { leqs = _; lts = lts; neqs = _ } e1 =
match e1 with
| Sil.Const (Sil.Cint n1) -> Some (n1 -- Sil.Int.one)
| Sil.Sizeof _ -> Some Sil.Int.zero
| Sil.Const (Sil.Cint n1) -> Some (n1 -- IntLit.one)
| Sil.Sizeof _ -> Some IntLit.zero
| _ ->
let e_lower_list =
IList.filter (function
@ -525,11 +526,11 @@ let check_equal prop e1 e2 =
match n_e1, n_e2 with
| Sil.BinOp (Sil.PlusA, e1, Sil.Const (Sil.Cint d)), e2
| e2, Sil.BinOp (Sil.PlusA, e1, Sil.Const (Sil.Cint d)) ->
if Sil.exp_equal e1 e2 then Sil.Int.iszero d
if Sil.exp_equal e1 e2 then IntLit.iszero d
else false
| Sil.Const c1, Sil.Lindex(Sil.Const c2, Sil.Const (Sil.Cint i)) when Sil.Int.iszero i ->
| Sil.Const c1, Sil.Lindex(Sil.Const c2, Sil.Const (Sil.Cint i)) when IntLit.iszero i ->
Sil.const_equal c1 c2
| Sil.Lindex(Sil.Const c1, Sil.Const (Sil.Cint i)), Sil.Const c2 when Sil.Int.iszero i ->
| Sil.Lindex(Sil.Const c1, Sil.Const (Sil.Cint i)), Sil.Const c2 when IntLit.iszero i ->
Sil.const_equal c1 c2
| _, _ -> false in
let check_equal_pi () =
@ -564,11 +565,11 @@ let get_bounds prop _e =
let e_norm = Prop.exp_normalize_prop prop _e in
let e_root, off = match e_norm with
| Sil.BinOp (Sil.PlusA, e, Sil.Const (Sil.Cint n1)) ->
e, Sil.Int.neg n1
e, IntLit.neg n1
| Sil.BinOp (Sil.MinusA, e, Sil.Const (Sil.Cint n1)) ->
e, n1
| _ ->
e_norm, Sil.Int.zero in
e_norm, IntLit.zero in
let ineq = Inequalities.from_prop prop in
let upper_opt = Inequalities.compute_upper_bound ineq e_root in
let lower_opt = Inequalities.compute_lower_bound ineq e_root in
@ -587,18 +588,18 @@ let check_disequal prop e1 e2 =
| Sil.Const c1, Sil.Const c2 ->
(Sil.const_kind_equal c1 c2) && not (Sil.const_equal c1 c2)
| Sil.Const c1, Sil.Lindex(Sil.Const c2, Sil.Const (Sil.Cint d)) ->
if Sil.Int.iszero d
if IntLit.iszero d
then not (Sil.const_equal c1 c2) (* offset=0 is no offset *)
else Sil.const_equal c1 c2 (* same base, different offsets *)
| Sil.BinOp (Sil.PlusA, e1, Sil.Const (Sil.Cint d1)), Sil.BinOp (Sil.PlusA, e2, Sil.Const (Sil.Cint d2)) ->
if Sil.exp_equal e1 e2 then Sil.Int.neq d1 d2
if Sil.exp_equal e1 e2 then IntLit.neq d1 d2
else false
| Sil.BinOp (Sil.PlusA, e1, Sil.Const (Sil.Cint d)), e2
| e2, Sil.BinOp (Sil.PlusA, e1, Sil.Const (Sil.Cint d)) ->
if Sil.exp_equal e1 e2 then not (Sil.Int.iszero d)
if Sil.exp_equal e1 e2 then not (IntLit.iszero d)
else false
| Sil.Lindex(Sil.Const c1, Sil.Const (Sil.Cint d)), Sil.Const c2 ->
if Sil.Int.iszero d then not (Sil.const_equal c1 c2) else Sil.const_equal c1 c2
if IntLit.iszero d then not (Sil.const_equal c1 c2) else Sil.const_equal c1 c2
| Sil.Lindex(Sil.Const c1, Sil.Const d1), Sil.Lindex (Sil.Const c2, Sil.Const d2) ->
Sil.const_equal c1 c2 && not (Sil.const_equal d1 d2)
| _, _ -> false in
@ -677,14 +678,14 @@ let check_le_normalized prop e1 e2 =
then Sil.exp_zero, Sil.exp_zero, n
else f1, f2, n
| _ ->
e1, e2, Sil.Int.zero in
e1, e2, IntLit.zero in
let ineq = Inequalities.from_prop prop in
let upper_lower_check () =
let upperL_opt = Inequalities.compute_upper_bound ineq eL in
let lowerR_opt = Inequalities.compute_lower_bound ineq eR in
match upperL_opt, lowerR_opt with
| None, _ | _, None -> false
| Some upper1, Some lower2 -> Sil.Int.leq upper1 (lower2 ++ Sil.Int.one ++ off) in
| Some upper1, Some lower2 -> IntLit.leq upper1 (lower2 ++ IntLit.one ++ off) in
(upper_lower_check ())
|| (Inequalities.check_le ineq e1 e2)
|| (check_equal prop e1 e2)
@ -698,7 +699,7 @@ let check_lt_normalized prop e1 e2 =
let lower2_opt = Inequalities.compute_lower_bound ineq e2 in
match upper1_opt, lower2_opt with
| None, _ | _, None -> false
| Some upper1, Some lower2 -> Sil.Int.leq upper1 lower2 in
| Some upper1, Some lower2 -> IntLit.leq upper1 lower2 in
(upper_lower_check ()) || (Inequalities.check_lt ineq e1 e2)
(** Given an atom and a proposition returns a unique identifier.
@ -730,9 +731,9 @@ let check_atom prop a0 =
end;
match a with
| Sil.Aeq (Sil.BinOp (Sil.Le, e1, e2), Sil.Const (Sil.Cint i))
when Sil.Int.isone i -> check_le_normalized prop e1 e2
when IntLit.isone i -> check_le_normalized prop e1 e2
| Sil.Aeq (Sil.BinOp (Sil.Lt, e1, e2), Sil.Const (Sil.Cint i))
when Sil.Int.isone i -> check_lt_normalized prop e1 e2
when IntLit.isone i -> check_lt_normalized prop e1 e2
| Sil.Aeq (e1, e2) -> check_equal prop e1 e2
| Sil.Aneq (e1, e2) -> check_disequal prop e1 e2
@ -776,7 +777,7 @@ let check_inconsistency_two_hpreds prop =
if Sil.exp_equal iF e || Sil.exp_equal iB e then true
else f e (hpred:: sigma_seen) sigma_rest
| Sil.Hlseg (Sil.Lseg_PE, _, e1, Sil.Const (Sil.Cint i), _) as hpred :: sigma_rest
when Sil.Int.iszero i ->
when IntLit.iszero i ->
if Sil.exp_equal e1 e then true
else f e (hpred:: sigma_seen) sigma_rest
| Sil.Hlseg (Sil.Lseg_PE, _, e1, e2, _) as hpred :: sigma_rest ->
@ -789,7 +790,7 @@ let check_inconsistency_two_hpreds prop =
in f e_new [] sigma_new
else f e (hpred:: sigma_seen) sigma_rest
| Sil.Hdllseg (Sil.Lseg_PE, _, e1, _, Sil.Const (Sil.Cint i), _, _) as hpred :: sigma_rest
when Sil.Int.iszero i ->
when IntLit.iszero i ->
if Sil.exp_equal e1 e then true
else f e (hpred:: sigma_seen) sigma_rest
| Sil.Hdllseg (Sil.Lseg_PE, _, e1, _, e3, _, _) as hpred :: sigma_rest ->
@ -1947,10 +1948,10 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
| _ -> None)
| _ -> None in
let mk_constant_string_hpred s = (* create an hpred from a constant string *)
let len = Sil.Int.of_int (1 + String.length s) in
let len = IntLit.of_int (1 + String.length s) in
let root = Sil.Const (Sil.Cstr s) in
let sexp =
let index = Sil.exp_int (Sil.Int.of_int (String.length s)) in
let index = Sil.exp_int (IntLit.of_int (String.length s)) in
match !Config.curr_language with
| Config.Clang ->
Sil.Earray

4
infer/src/backend/prover.mli
Unescape View File

@ -59,7 +59,7 @@ val is_root : Prop.normal Prop.t -> exp -> exp -> offset list option
val expand_hpred_pointer : bool -> Sil.hpred -> bool * bool * Sil.hpred
(** Get upper and lower bounds of an expression, if any *)
val get_bounds : Prop.normal Prop.t -> Sil.exp -> Sil.Int.t option * Sil.Int.t option
val get_bounds : Prop.normal Prop.t -> Sil.exp -> IntLit.t option * IntLit.t option
(** {2 Abduction prover} *)
@ -91,7 +91,7 @@ val find_minimum_pure_cover : (Sil.atom list * 'a) list -> (Sil.atom list * 'a)
(** {2 Compute various lower or upper bounds} *)
(** Computer an upper bound of an expression *)
val compute_upper_bound_of_exp : Prop.normal Prop.t -> Sil.exp -> Sil.Int.t option
val compute_upper_bound_of_exp : Prop.normal Prop.t -> Sil.exp -> IntLit.t option
(** {2 Subtype checking} *)

2
infer/src/backend/rearrange.ml
Unescape View File

@ -301,7 +301,7 @@ and array_case_analysis_index pname tenv orig_prop
IList.exists (fun (i, _) -> Prover.check_equal Prop.prop_emp index i) array_cont in
let array_is_full =
match array_len with
| Sil.Const (Sil.Cint n') -> Sil.Int.geq (Sil.Int.of_int (IList.length array_cont)) n'
| Sil.Const (Sil.Cint n') -> IntLit.geq (IntLit.of_int (IList.length array_cont)) n'
| _ -> false in
if index_in_array then

24
infer/src/backend/symExec.ml
Unescape View File

@ -35,7 +35,7 @@ let rec unroll_type tenv typ off =
end
| Sil.Tarray (typ', _), Sil.Off_index _ ->
typ'
| _, Sil.Off_index (Sil.Const (Sil.Cint i)) when Sil.Int.iszero i ->
| _, Sil.Off_index (Sil.Const (Sil.Cint i)) when IntLit.iszero i ->
typ
| _ ->
L.d_strln ".... Invalid Field Access ....";
@ -314,7 +314,7 @@ let rec prune ~positive condition prop =
match condition with
| Sil.Var _ | Sil.Lvar _ ->
prune_ne ~positive condition Sil.exp_zero prop
| Sil.Const (Sil.Cint i) when Sil.Int.iszero i ->
| Sil.Const (Sil.Cint i) when IntLit.iszero i ->
if positive then Propset.empty else Propset.singleton prop
| Sil.Const (Sil.Cint _) | Sil.Sizeof _ | Sil.Const (Sil.Cstr _) | Sil.Const (Sil.Cclass _) ->
if positive then Propset.singleton prop else Propset.empty
@ -327,12 +327,12 @@ let rec prune ~positive condition prop =
| Sil.UnOp _ ->
assert false
| Sil.BinOp (Sil.Eq, e, Sil.Const (Sil.Cint i))
| Sil.BinOp (Sil.Eq, Sil.Const (Sil.Cint i), e) when Sil.Int.iszero i && not (Sil.Int.isnull i) ->
| Sil.BinOp (Sil.Eq, Sil.Const (Sil.Cint i), e) when IntLit.iszero i && not (IntLit.isnull i) ->
prune ~positive:(not positive) e prop
| Sil.BinOp (Sil.Eq, e1, e2) ->
prune_ne ~positive:(not positive) e1 e2 prop
| Sil.BinOp (Sil.Ne, e, Sil.Const (Sil.Cint i))
| Sil.BinOp (Sil.Ne, Sil.Const (Sil.Cint i), e) when Sil.Int.iszero i && not (Sil.Int.isnull i) ->
| Sil.BinOp (Sil.Ne, Sil.Const (Sil.Cint i), e) when IntLit.iszero i && not (IntLit.isnull i) ->
prune ~positive e prop
| Sil.BinOp (Sil.Ne, e1, e2) ->
prune_ne ~positive e1 e2 prop
@ -392,20 +392,20 @@ let call_should_be_skipped callee_pname summary =
(** In case of constant string dereference, return the result immediately *)
let check_constant_string_dereference lexp =
let string_lookup s n =
let c = try Char.code (String.get s (Sil.Int.to_int n)) with Invalid_argument _ -> 0 in
Sil.exp_int (Sil.Int.of_int c) in
let c = try Char.code (String.get s (IntLit.to_int n)) with Invalid_argument _ -> 0 in
Sil.exp_int (IntLit.of_int c) in
match lexp with
| Sil.BinOp(Sil.PlusPI, Sil.Const (Sil.Cstr s), e)
| Sil.Lindex (Sil.Const (Sil.Cstr s), e) ->
let value = match e with
| Sil.Const (Sil.Cint n)
when Sil.Int.geq n Sil.Int.zero &&
Sil.Int.leq n (Sil.Int.of_int (String.length s)) ->
when IntLit.geq n IntLit.zero &&
IntLit.leq n (IntLit.of_int (String.length s)) ->
string_lookup s n
| _ -> Sil.exp_get_undefined false in
Some value
| Sil.Const (Sil.Cstr s) ->
Some (string_lookup s Sil.Int.zero)
Some (string_lookup s IntLit.zero)
| _ -> None
(** Normalize an expression and check for arithmetic problems *)
@ -440,7 +440,7 @@ let check_already_dereferenced pname cond prop =
| Sil.UnOp(Sil.LNot, e, _) ->
is_check_zero e
| Sil.BinOp ((Sil.Eq | Sil.Ne), Sil.Const Sil.Cint i, Sil.Var id)
| Sil.BinOp ((Sil.Eq | Sil.Ne), Sil.Var id, Sil.Const Sil.Cint i) when Sil.Int.iszero i ->
| Sil.BinOp ((Sil.Eq | Sil.Ne), Sil.Var id, Sil.Const Sil.Cint i) when IntLit.iszero i ->
Some id
| _ -> None in
let dereferenced_line = match is_check_zero cond with
@ -1027,7 +1027,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
let report_condition_always_true_false i =
let skip_loop = match ik with
| Sil.Ik_while | Sil.Ik_for ->
not (Sil.Int.iszero i) (* skip wile(1) and for (;1;) *)
not (IntLit.iszero i) (* skip wile(1) and for (;1;) *)
| Sil.Ik_dowhile ->
true (* skip do..while *)
| Sil.Ik_land_lor ->
@ -1044,7 +1044,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
let node = State.get_node () in
let desc = Errdesc.explain_condition_always_true_false i cond node loc in
let exn =
Exceptions.Condition_always_true_false (desc, not (Sil.Int.iszero i), __POS__) in
Exceptions.Condition_always_true_false (desc, not (IntLit.iszero i), __POS__) in
let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop current_pname) in
Reporting.log_warning current_pname ~pre: pre_opt exn
| Sil.BinOp ((Sil.Eq | Sil.Ne), lhs, rhs)

2
infer/src/backend/tabulation.ml
Unescape View File

@ -722,7 +722,7 @@ let combine
let id_assigned_to_null id =
let filter = function
| Sil.Aeq (Sil.Var id', Sil.Const (Sil.Cint i)) ->
Ident.equal id id' && Sil.Int.isnull i
Ident.equal id id' && IntLit.isnull i
| _ -> false in
IList.exists filter split.missing_pi in
let f (e, inst_opt) = match e, inst_opt with

6
infer/src/checkers/checkTraceCallSequence.ml
Unescape View File

@ -259,7 +259,7 @@ module BooleanVars = struct
match normalize_instr instr with
| Sil.Prune (Sil.BinOp (Sil.Eq, _cond_e, Sil.Const (Sil.Cint i)), _, _, _)
when Sil.Int.iszero i ->
when IntLit.iszero i ->
let cond_e = Idenv.expand_expr idenv _cond_e in
let state' = match exp_boolean_var cond_e with
| Some name ->
@ -268,7 +268,7 @@ module BooleanVars = struct
| None -> state in
state'
| Sil.Prune (Sil.BinOp (Sil.Ne, _cond_e, Sil.Const (Sil.Cint i)), _, _, _)
when Sil.Int.iszero i ->
when IntLit.iszero i ->
let cond_e = Idenv.expand_expr idenv _cond_e in
let state' = match exp_boolean_var cond_e with
| Some name ->
@ -281,7 +281,7 @@ module BooleanVars = struct
let state' = match exp_boolean_var e1 with
| Some name ->
let b_opt = match e2 with
| Sil.Const (Sil.Cint i) -> Some (not (Sil.Int.iszero i))
| Sil.Const (Sil.Cint i) -> Some (not (IntLit.iszero i))
| _ -> None in
if verbose then
begin

12
infer/src/clang/cArithmetic_trans.ml
Unescape View File

@ -144,12 +144,12 @@ let unary_operation_instruction uoi e typ loc =
| `PostInc ->
let id = Ident.create_fresh Ident.knormal in
let instr1 = Sil.Letderef (id, e, typ, loc) in
let e_plus_1 = Sil.BinOp(Sil.PlusA, Sil.Var id, Sil.Const(Sil.Cint (Sil.Int.one))) in
let e_plus_1 = Sil.BinOp(Sil.PlusA, Sil.Var id, Sil.Const(Sil.Cint (IntLit.one))) in
(Sil.Var id, instr1::[Sil.Set (e, typ, e_plus_1, loc)])
| `PreInc ->
let id = Ident.create_fresh Ident.knormal in
let instr1 = Sil.Letderef (id, e, typ, loc) in
let e_plus_1 = Sil.BinOp(Sil.PlusA, Sil.Var id, Sil.Const(Sil.Cint (Sil.Int.one))) in
let e_plus_1 = Sil.BinOp(Sil.PlusA, Sil.Var id, Sil.Const(Sil.Cint (IntLit.one))) in
let exp = if General_utils.is_cpp_translation Config.clang_lang then
e
else
@ -158,12 +158,12 @@ let unary_operation_instruction uoi e typ loc =
| `PostDec ->
let id = Ident.create_fresh Ident.knormal in
let instr1 = Sil.Letderef (id, e, typ, loc) in
let e_minus_1 = Sil.BinOp(Sil.MinusA, Sil.Var id, Sil.Const(Sil.Cint (Sil.Int.one))) in
let e_minus_1 = Sil.BinOp(Sil.MinusA, Sil.Var id, Sil.Const(Sil.Cint (IntLit.one))) in
(Sil.Var id, instr1::[Sil.Set (e, typ, e_minus_1, loc)])
| `PreDec ->
let id = Ident.create_fresh Ident.knormal in
let instr1 = Sil.Letderef (id, e, typ, loc) in
let e_minus_1 = Sil.BinOp(Sil.MinusA, Sil.Var id, Sil.Const(Sil.Cint (Sil.Int.one))) in
let e_minus_1 = Sil.BinOp(Sil.MinusA, Sil.Var id, Sil.Const(Sil.Cint (IntLit.one))) in
let exp = if General_utils.is_cpp_translation Config.clang_lang then
e
else
@ -220,5 +220,5 @@ let bin_op_to_string boi =
let sil_const_plus_one const =
match const with
| Sil.Const (Sil.Cint n) ->
Sil.Const (Sil.Cint (Sil.Int.add n Sil.Int.one))
| _ -> Sil.BinOp (Sil.PlusA, const, Sil.Const (Sil.Cint (Sil.Int.one)))
Sil.Const (Sil.Cint (IntLit.add n IntLit.one))
| _ -> Sil.BinOp (Sil.PlusA, const, Sil.Const (Sil.Cint (IntLit.one)))

22
infer/src/clang/cTrans.ml
Unescape View File

@ -345,7 +345,7 @@ struct
So we implement it as the constant zero *)
let gNUNullExpr_trans trans_state expr_info =
let typ = CTypes_decl.get_type_from_expr_info expr_info trans_state.context.CContext.tenv in
let exp = Sil.Const (Sil.Cint (Sil.Int.zero)) in
let exp = Sil.Const (Sil.Cint (IntLit.zero)) in
{ empty_res_trans with exps = [(exp, typ)]}
let nullPtrExpr_trans trans_state expr_info =
@ -366,7 +366,7 @@ struct
let characterLiteral_trans trans_state expr_info n =
let typ = CTypes_decl.get_type_from_expr_info expr_info trans_state.context.CContext.tenv in
let exp = Sil.Const (Sil.Cint (Sil.Int.of_int n)) in
let exp = Sil.Const (Sil.Cint (IntLit.of_int n)) in
{ empty_res_trans with exps = [(exp, typ)]}
let floatingLiteral_trans trans_state expr_info float_string =
@ -381,7 +381,7 @@ struct
let exp =
try
let i = Int64.of_string integer_literal_info.Clang_ast_t.ili_value in
let exp = Sil.exp_int (Sil.Int.of_int64 i) in
let exp = Sil.exp_int (IntLit.of_int64 i) in
exp
with
| Failure _ ->
@ -398,7 +398,7 @@ struct
let zero_opt = match typ with
| Sil.Tfloat _ | Sil.Tptr _ | Sil.Tint _ -> Some (Sil.zero_value_of_numerical_type typ)
| Sil.Tvoid -> None
| _ -> Some (Sil.Const (Sil.Cint Sil.Int.zero)) in
| _ -> Some (Sil.Const (Sil.Cint IntLit.zero)) in
match zero_opt with
| Some zero -> { empty_res_trans with exps = [(zero, typ)] }
| _ -> empty_res_trans
@ -677,7 +677,7 @@ struct
(* get the sil value of the enum constant from the map or by evaluating it *)
and get_enum_constant_expr context enum_constant_pointer =
let zero = Sil.Const (Sil.Cint Sil.Int.zero) in
let zero = Sil.Const (Sil.Cint IntLit.zero) in
try
let (prev_enum_constant_opt, sil_exp_opt) =
Ast_utils.get_enum_constant_exp enum_constant_pointer in
@ -855,7 +855,7 @@ struct
NEED TO BE FIXED\n\n";
fix_param_exps_mismatch params_stmt params) in
let act_params = if is_cf_retain_release then
(Sil.Const (Sil.Cint Sil.Int.one), Sil.Tint Sil.IBool) :: act_params
(Sil.Const (Sil.Cint IntLit.one), Sil.Tint Sil.IBool) :: act_params
else act_params in
match
CTrans_utils.builtin_trans trans_state_pri sil_loc si function_type callee_pname_opt with
@ -1185,7 +1185,7 @@ struct
Printing.log_out " No short-circuit condition\n";
let res_trans_cond =
if is_null_stmt cond then {
empty_res_trans with exps = [(Sil.Const (Sil.Cint Sil.Int.one), (Sil.Tint Sil.IBool))]
empty_res_trans with exps = [(Sil.Const (Sil.Cint IntLit.one), (Sil.Tint Sil.IBool))]
}
(* Assumption: If it's a null_stmt, it is a loop with no bound, so we set condition to 1 *)
else
@ -2034,7 +2034,7 @@ struct
let (var_exp_inside, typ_inside) = match typ with
| Sil.Tarray (t, _)
| Sil.Tptr (t, _) when Sil.is_array_of_cpp_class typ || is_dyn_array ->
Sil.Lindex (var_exp, Sil.Const (Sil.Cint (Sil.Int.of_int n))), t
Sil.Lindex (var_exp, Sil.Const (Sil.Cint (IntLit.of_int n))), t
| _ -> var_exp, typ in
let trans_state' = { trans_state with var_exp_typ = Some (var_exp_inside, typ_inside) } in
match stmts with
@ -2085,7 +2085,7 @@ struct
(match res_trans_size.exps with
| [(exp, _)] -> Some exp, res_trans_size
| _ -> None, empty_res_trans)
| None -> Some (Sil.Const (Sil.Cint (Sil.Int.minus_one))), empty_res_trans
| None -> Some (Sil.Const (Sil.Cint (IntLit.minus_one))), empty_res_trans
else None, empty_res_trans in
let res_trans_new = cpp_new_trans trans_state_pri sil_loc typ size_exp_opt in
let stmt_opt = Ast_utils.get_stmt_opt cxx_new_expr_info.Clang_ast_t.xnei_initializer_expr in
@ -2099,8 +2099,8 @@ struct
if is_dyn_array && Sil.is_pointer_to_cpp_class typ then
let rec create_stmts stmt_opt size_exp_opt =
match stmt_opt, size_exp_opt with
| Some stmt, Some (Sil.Const (Sil.Cint n)) when not (Sil.Int.iszero n) ->
let n_minus_1 = Some ((Sil.Const (Sil.Cint (Sil.Int.sub n Sil.Int.one)))) in
| Some stmt, Some (Sil.Const (Sil.Cint n)) when not (IntLit.iszero n) ->
let n_minus_1 = Some ((Sil.Const (Sil.Cint (IntLit.sub n IntLit.one)))) in
stmt :: create_stmts stmt_opt n_minus_1
| _ -> [] in
let stmts = create_stmts stmt_opt size_exp_opt in

4
infer/src/clang/cTrans_utils.ml
Unescape View File

@ -685,10 +685,10 @@ let var_or_zero_in_init_list tenv e typ ~return_zero:return_zero =
IList.map (fun (e, t) ->
IList.flatten (var_or_zero_in_init_list' e t tns)) exp_types
| Sil.Tarray (arrtyp, Some n) ->
let size = Sil.Int.to_int n in
let size = IntLit.to_int n in
let indices = list_range 0 (size - 1) in
let index_constants =
IList.map (fun i -> (Sil.Const (Sil.Cint (Sil.Int.of_int i)))) indices in
IList.map (fun i -> (Sil.Const (Sil.Cint (IntLit.of_int i)))) indices in
let lh_exprs =
IList.map (fun index_expr -> Sil.Lindex (e, index_expr)) index_constants in
let lh_types = replicate size arrtyp in

2
infer/src/clang/cType_to_sil_type.ml
Unescape View File

@ -63,7 +63,7 @@ let pointer_attribute_of_objc_attribute attr_info =
let rec build_array_type translate_decl tenv type_ptr n_opt =
let array_type = type_ptr_to_sil_type translate_decl tenv type_ptr in
let len = Option.map (fun n -> Sil.Int.of_int64 (Int64.of_int n)) n_opt in
let len = Option.map (fun n -> IntLit.of_int64 (Int64.of_int n)) n_opt in
Sil.Tarray (array_type, len)
and sil_type_of_attr_type translate_decl tenv type_info attr_info =

8
infer/src/eradicate/typeCheck.ml
Unescape View File

@ -169,7 +169,7 @@ let rec typecheck_expr
(match TypeState.lookup_id id typestate with
| Some tr -> TypeState.range_add_locs tr [loc]
| None -> tr_default)
| Sil.Const (Sil.Cint i) when Sil.Int.iszero i ->
| Sil.Const (Sil.Cint i) when IntLit.iszero i ->
let (typ, _, locs) = tr_default in
if PatternMatch.type_is_class typ
then (typ, TypeAnnotation.const Annotations.Nullable true (TypeOrigin.Const loc), locs)
@ -707,7 +707,7 @@ let typecheck_instr
let do_instr = function
| Sil.Prune (Sil.BinOp (Sil.Eq, _cond_e, Sil.Const (Sil.Cint i)), _, _, _)
| Sil.Prune (Sil.BinOp (Sil.Eq, Sil.Const (Sil.Cint i), _cond_e), _, _, _)
when Sil.Int.iszero i ->
when IntLit.iszero i ->
let cond_e = Idenv.expand_expr_temps idenv cond_node _cond_e in
begin
match convert_complex_exp_to_pvar cond_node false cond_e typestate' loc with
@ -946,7 +946,7 @@ let typecheck_instr
match c with
| Sil.BinOp (Sil.Eq, Sil.Const (Sil.Cint i), e)
| Sil.BinOp (Sil.Eq, e, Sil.Const (Sil.Cint i)) when Sil.Int.iszero i ->
| Sil.BinOp (Sil.Eq, e, Sil.Const (Sil.Cint i)) when IntLit.iszero i ->
typecheck_expr_for_errors typestate e loc;
let typestate1, e1, from_call = match from_is_true_on_null e with
| Some e1 ->
@ -975,7 +975,7 @@ let typecheck_instr
end
| Sil.BinOp (Sil.Ne, Sil.Const (Sil.Cint i), e)
| Sil.BinOp (Sil.Ne, e, Sil.Const (Sil.Cint i)) when Sil.Int.iszero i ->
| Sil.BinOp (Sil.Ne, e, Sil.Const (Sil.Cint i)) when IntLit.iszero i ->
typecheck_expr_for_errors typestate e loc;
let typestate1, e1, from_call = match from_instanceof e with
| Some e1 -> (* (e1 instanceof C) implies (e1 != null) *)

6
infer/src/harness/inhabit.ml
Unescape View File

@ -85,8 +85,8 @@ let rec inhabit_typ typ cfg env =
with Not_found ->
let inhabit_internal typ env = match typ with
| Sil.Tptr (Sil.Tarray (inner_typ, Some _), Sil.Pk_pointer) ->
let len = Sil.Const (Sil.Cint (Sil.Int.one)) in
let arr_typ = Sil.Tarray (inner_typ, Some Sil.Int.one) in
let len = Sil.Const (Sil.Cint (IntLit.one)) in
let arr_typ = Sil.Tarray (inner_typ, Some IntLit.one) in
inhabit_alloc arr_typ (Some len) typ ModelBuiltins.__new_array env
| Sil.Tptr (typ, Sil.Pk_pointer) as ptr_to_typ ->
(* TODO (t4575417): this case does not work correctly for enums, but they are currently
@ -130,7 +130,7 @@ let rec inhabit_typ typ cfg env =
let fresh_id = Ident.create_fresh Ident.knormal in
let read_from_local_instr = Sil.Letderef (fresh_id, fresh_local_exp, ptr_to_typ, env'.pc) in
(Sil.Var fresh_id, env_add_instr read_from_local_instr env')
| Sil.Tint (_) -> (Sil.Const (Sil.Cint (Sil.Int.zero)), env)
| Sil.Tint (_) -> (Sil.Const (Sil.Cint (IntLit.zero)), env)
| Sil.Tfloat (_) -> (Sil.Const (Sil.Cfloat 0.0), env)
| typ ->
L.err "Couldn't inhabit typ: %a@." (Sil.pp_typ pe_text) typ;

18
infer/src/java/jTrans.ml
Unescape View File

@ -169,12 +169,12 @@ let locals_formals program tenv cn impl meth_kind =
let get_constant (c : JBir.const) =
match c with
| `Int i -> Sil.Cint (Sil.Int.of_int32 i)
| `ANull -> Sil.Cint Sil.Int.null
| `Int i -> Sil.Cint (IntLit.of_int32 i)
| `ANull -> Sil.Cint IntLit.null
| `Class ot -> Sil.Cclass (Ident.string_to_name (JTransType.object_type_to_string ot))
| `Double f -> Sil.Cfloat f
| `Float f -> Sil.Cfloat f
| `Long i64 -> Sil.Cint (Sil.Int.of_int64 i64)
| `Long i64 -> Sil.Cint (IntLit.of_int64 i64)
| `String jstr -> Sil.Cstr (JBasics.jstr_pp jstr)
let get_binop binop =
@ -653,14 +653,6 @@ let get_array_length context pc expr_list content_type =
let array_size = Sil.Sizeof (array_type, array_len, Sil.Subtype.exact) in
(instrs, array_size)
module Int =
struct
type t = int
let compare = (-)
end
module IntSet = Set.Make(Int)
let detect_loop entry_pc impl =
let code = (JBir.code impl) in
let pc_bound = Array.length code in
@ -1050,7 +1042,7 @@ let rec instruction context pc instr : translation =
let sil_assume_in_bound =
let sil_in_bound =
let sil_positive_index =
Sil.BinOp (Sil.Ge, sil_index_expr, Sil.Const (Sil.Cint Sil.Int.zero))
Sil.BinOp (Sil.Ge, sil_index_expr, Sil.Const (Sil.Cint IntLit.zero))
and sil_less_than_length =
Sil.BinOp (Sil.Lt, sil_index_expr, sil_length_expr) in
Sil.BinOp (Sil.LAnd, sil_positive_index, sil_less_than_length) in
@ -1063,7 +1055,7 @@ let rec instruction context pc instr : translation =
let sil_assume_out_of_bound =
let sil_out_of_bound =
let sil_negative_index =
Sil.BinOp (Sil.Lt, sil_index_expr, Sil.Const (Sil.Cint Sil.Int.zero))
Sil.BinOp (Sil.Lt, sil_index_expr, Sil.Const (Sil.Cint IntLit.zero))
and sil_greater_than_length =
Sil.BinOp (Sil.Gt, sil_index_expr, sil_length_expr) in
Sil.BinOp (Sil.LOr, sil_negative_index, sil_greater_than_length) in

4
infer/src/llvm/lTrans.ml
Unescape View File

@ -24,7 +24,7 @@ let ident_of_variable (var : LAst.variable) : Ident.t = (* TODO: use unique stam
let trans_variable (var : LAst.variable) : Sil.exp = Sil.Var (ident_of_variable var)
let trans_constant : LAst.constant -> Sil.exp = function
| Cint i -> Sil.Const (Sil.Cint (Sil.Int.of_int i))
| Cint i -> Sil.Const (Sil.Cint (IntLit.of_int i))
| Cnull -> Sil.exp_null
let trans_operand : LAst.operand -> Sil.exp = function
@ -36,7 +36,7 @@ let rec trans_typ : LAst.typ -> Sil.typ = function
| Tfloat -> Sil.Tfloat Sil.FFloat
| Tptr tp -> Sil.Tptr (trans_typ tp, Sil.Pk_pointer)
| Tvector (i, tp)
| Tarray (i, tp) -> Sil.Tarray (trans_typ tp, Some (Sil.Int.of_int i))
| Tarray (i, tp) -> Sil.Tarray (trans_typ tp, Some (IntLit.of_int i))
| Tfunc _ -> Sil.Tfun false
| Tlabel -> raise (ImproperTypeError "Tried to generate Sil type from LLVM label type.")
| Tmetadata -> raise (ImproperTypeError "Tried to generate Sil type from LLVM metadata type.")

2
infer/src/unit/analyzerTester.ml
Unescape View File

@ -114,7 +114,7 @@ module StructuredSil = struct
make_set ~rhs_typ ~lhs_exp ~rhs_exp
let var_assign_int lhs rhs =
let rhs_exp = Sil.exp_int (Sil.Int.of_int rhs) in
let rhs_exp = Sil.exp_int (IntLit.of_int rhs) in
let rhs_typ = Sil.Tint Sil.IInt in
var_assign_exp ~rhs_typ lhs rhs_exp

Write Preview
Loading…
Cancel
Save