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

[infer] Add type in binary operator

Browse Source 
Reviewed By: mbouaziz

Differential Revision: D10216263

fbshipit-source-id: 84f0fa936
master
Sungkeun Cho 6 years ago committed by Facebook Github Bot
parent eca0b491d6
commit d94ba863c6
17 changed files with 197 additions and 160 deletions
Show Stats Download Patch File Download Diff File

20
infer/src/IR/Binop.ml
Unescape View File

@ -9,14 +9,18 @@
(** The Smallfoot Intermediate Language: Binary Operators *) (** The Smallfoot Intermediate Language: Binary Operators *)
open! IStd open! IStd
type ikind_option_for_binop = Typ.ikind option
let compare_ikind_option_for_binop _ _ = 0
(** Binary operations *) (** Binary operations *)
type t = type t =
| PlusA (** arithmetic + *) | PlusA of ikind_option_for_binop (** arithmetic + *)
| PlusPI (** pointer + integer *) | PlusPI (** pointer + integer *)
| MinusA (** arithmetic - *) | MinusA of ikind_option_for_binop (** arithmetic - *)
| MinusPI (** pointer - integer *) | MinusPI (** pointer - integer *)
| MinusPP (** pointer - pointer *) | MinusPP (** pointer - pointer *)
| Mult (** * *) | Mult of ikind_option_for_binop (** * *)
| Div (** / *) | Div (** / *)
| Mod (** % *) | Mod (** % *)
| Shiftlt (** shift left *) | Shiftlt (** shift left *)
@ -39,22 +43,22 @@ let equal = [%compare.equal: t]
(** This function returns true if the operation is injective (** This function returns true if the operation is injective
wrt. each argument: op(e,-) and op(-, e) is injective for all e. wrt. each argument: op(e,-) and op(-, e) is injective for all e.
The return value false means "don't know". *) The return value false means "don't know". *)
let injective = function PlusA | PlusPI | MinusA | MinusPI | MinusPP -> true | _ -> false let injective = function PlusA _ | PlusPI | MinusA _ | MinusPI | MinusPP -> true | _ -> false
(** This function returns true if 0 is the right unit of [binop]. (** This function returns true if 0 is the right unit of [binop].
The return value false means "don't know". *) The return value false means "don't know". *)
let is_zero_runit = function PlusA | PlusPI | MinusA | MinusPI | MinusPP -> true | _ -> false let is_zero_runit = function PlusA _ | PlusPI | MinusA _ | MinusPI | MinusPP -> true | _ -> false
let text = function let text = function
| PlusA -> | PlusA _ ->
"+" "+"
| PlusPI -> | PlusPI ->
"+" "+"
| MinusA | MinusPP -> | MinusA _ | MinusPP ->
"-" "-"
| MinusPI -> | MinusPI ->
"-" "-"
| Mult -> | Mult _ ->
"*" "*"
| Div -> | Div ->
"/" "/"

6
infer/src/IR/Binop.mli
Unescape View File

@ -11,12 +11,12 @@ open! IStd
(** Binary operations *) (** Binary operations *)
type t = type t =
| PlusA (** arithmetic + *) | PlusA of Typ.ikind option (** arithmetic + *)
| PlusPI (** pointer + integer *) | PlusPI (** pointer + integer *)
| MinusA (** arithmetic - *) | MinusA of Typ.ikind option (** arithmetic - *)
| MinusPI (** pointer - integer *) | MinusPI (** pointer - integer *)
| MinusPP (** pointer - pointer *) | MinusPP (** pointer - pointer *)
| Mult (** * *) | Mult of Typ.ikind option (** * *)
| Div (** / *) | Div (** / *)
| Mod (** % *) | Mod (** % *)
| Shiftlt (** shift left *) | Shiftlt (** shift left *)

2
infer/src/IR/Exp.ml
Unescape View File

@ -192,7 +192,7 @@ let rec pp_ pe pp_t f e =
let pp_exp = pp_ pe pp_t in let pp_exp = pp_ pe pp_t in
let print_binop_stm_output e1 op e2 = let print_binop_stm_output e1 op e2 =
match (op : Binop.t) with match (op : Binop.t) with
| Eq | Ne | PlusA | Mult -> | Eq | Ne | PlusA _ | Mult _ ->
F.fprintf f "(%a %s %a)" pp_exp e2 (Binop.str pe op) pp_exp e1 F.fprintf f "(%a %s %a)" pp_exp e2 (Binop.str pe op) pp_exp e1
| Lt -> | Lt ->
F.fprintf f "(%a %s %a)" pp_exp e2 (Binop.str pe Gt) pp_exp e1 F.fprintf f "(%a %s %a)" pp_exp e2 (Binop.str pe Gt) pp_exp e1

6
infer/src/IR/HilExp.ml
Unescape View File

@ -215,13 +215,13 @@ and eval = function
Some c Some c
| BinaryOperator (Binop.Div, e1, e2) -> ( | BinaryOperator (Binop.Div, e1, e2) -> (
try eval_arithmetic_binop IntLit.div e1 e2 with Division_by_zero -> None ) try eval_arithmetic_binop IntLit.div e1 e2 with Division_by_zero -> None )
| BinaryOperator (Binop.MinusA, e1, e2) -> | BinaryOperator (Binop.MinusA _, e1, e2) ->
eval_arithmetic_binop IntLit.sub e1 e2 eval_arithmetic_binop IntLit.sub e1 e2
| BinaryOperator (Binop.Mod, e1, e2) -> | BinaryOperator (Binop.Mod, e1, e2) ->
eval_arithmetic_binop IntLit.rem e1 e2 eval_arithmetic_binop IntLit.rem e1 e2
| BinaryOperator (Binop.Mult, e1, e2) -> | BinaryOperator (Binop.Mult _, e1, e2) ->
eval_arithmetic_binop IntLit.mul e1 e2 eval_arithmetic_binop IntLit.mul e1 e2
| BinaryOperator (Binop.PlusA, e1, e2) -> | BinaryOperator (Binop.PlusA _, e1, e2) ->
eval_arithmetic_binop IntLit.add e1 e2 eval_arithmetic_binop IntLit.add e1 e2
| _ -> | _ ->
(* TODO: handle bitshifting cases, port eval_binop from RacerD.ml *) (* TODO: handle bitshifting cases, port eval_binop from RacerD.ml *)

5
infer/src/IR/Typ.ml
Unescape View File

@ -184,6 +184,11 @@ let void = mk Tvoid
let void_star = mk (Tptr (mk Tvoid, Pk_pointer)) let void_star = mk (Tptr (mk Tvoid, Pk_pointer))
let get_ikind_opt {desc} = match desc with Tint ikind -> Some ikind | _ -> None
(* TODO: size_t should be implementation-dependent. *)
let size_t = IULong
let escape pe = if Pp.equal_print_kind pe.Pp.kind Pp.HTML then Escape.escape_xml else ident let escape pe = if Pp.equal_print_kind pe.Pp.kind Pp.HTML then Escape.escape_xml else ident
(** Pretty print a type with all the details, using the C syntax. *) (** Pretty print a type with all the details, using the C syntax. *)

6
infer/src/IR/Typ.mli
Unescape View File

@ -120,6 +120,12 @@ val void : t
val void_star : t val void_star : t
(** void* type *) (** void* type *)
val get_ikind_opt : t -> ikind option
(** Get ikind if the type is integer. *)
val size_t : ikind
(** ikind of size_t *)
module Name : sig module Name : sig
(** Named types. *) (** Named types. *)
type t = name [@@deriving compare] type t = name [@@deriving compare]

6
infer/src/biabduction/Absarray.ml
Unescape View File

@ -405,7 +405,7 @@ let generic_strexp_abstract tenv (abstraction_name : string) (p_in : Prop.normal
let index_is_pointed_to tenv (p : Prop.normal Prop.t) (path : StrexpMatch.path) (index : Exp.t) : let index_is_pointed_to tenv (p : Prop.normal Prop.t) (path : StrexpMatch.path) (index : Exp.t) :
bool = bool =
let indices = let indices =
let index_plus_one = Exp.BinOp (Binop.PlusA, index, Exp.one) in let index_plus_one = Exp.BinOp (Binop.PlusA None, index, Exp.one) in
[index; index_plus_one] [index; index_plus_one]
in in
let add_index_to_paths = let add_index_to_paths =
@ -448,8 +448,8 @@ let blur_array_index tenv (p : Prop.normal Prop.t) (path : StrexpMatch.path) (in
Prop.set p2 ~sigma:sigma' Prop.set p2 ~sigma:sigma'
in in
let p4 = let p4 =
let index_next = Exp.BinOp (Binop.PlusA, index, Exp.one) in let index_next = Exp.BinOp (Binop.PlusA None, index, Exp.one) in
let fresh_index_next = Exp.BinOp (Binop.PlusA, fresh_index, Exp.one) in let fresh_index_next = Exp.BinOp (Binop.PlusA None, fresh_index, Exp.one) in
let map = [(index, fresh_index); (index_next, fresh_index_next)] in let map = [(index, fresh_index); (index_next, fresh_index_next)] in
prop_replace_path_index tenv p3 path map prop_replace_path_index tenv p3 path map
in in

38
infer/src/biabduction/Dom.ml
Unescape View File

@ -455,7 +455,7 @@ end = struct
false false
in in
let add_and_gen_eq e e' n = let add_and_gen_eq e e' n =
let e_plus_n = Exp.BinOp (Binop.PlusA, e, Exp.int n) in let e_plus_n = Exp.BinOp (Binop.PlusA None, e, Exp.int n) in
Prop.mk_eq tenv e_plus_n e' Prop.mk_eq tenv e_plus_n e'
in in
let rec f_eqs_entry ((e1, e2, e) as entry) eqs_acc t_seen = function let rec f_eqs_entry ((e1, e2, e) as entry) eqs_acc t_seen = function
@ -562,7 +562,7 @@ end = struct
match e with match e with
| Exp.Const _ -> | Exp.Const _ ->
[] []
| Exp.Lvar _ | Exp.Var _ | Exp.BinOp (Binop.PlusA, Exp.Var _, _) -> | Exp.Lvar _ | Exp.Var _ | Exp.BinOp (Binop.PlusA _, Exp.Var _, _) ->
let is_same_e (e1, e2, _) = Exp.equal e (select side e1 e2) in let is_same_e (e1, e2, _) = Exp.equal e (select side e1 e2) in
let assoc = List.filter ~f:is_same_e !tbl in let assoc = List.filter ~f:is_same_e !tbl in
List.map ~f:(fun (e1, e2, _) -> select side_op e1 e2) assoc List.map ~f:(fun (e1, e2, _) -> select side_op e1 e2) assoc
@ -588,15 +588,19 @@ end = struct
let res = ref [] in let res = ref [] in
let f v = let f v =
match (v, side) with match (v, side) with
| (Exp.BinOp (Binop.PlusA, e1', Exp.Const (Const.Cint i)), e2, e'), Lhs when Exp.equal e e1' | (Exp.BinOp (Binop.PlusA _, e1', Exp.Const (Const.Cint i)), e2, e'), Lhs
-> when Exp.equal e e1' ->
let c' = Exp.int (IntLit.neg i) in let c' = Exp.int (IntLit.neg i) in
let v' = (e1', Exp.BinOp (Binop.PlusA, e2, c'), Exp.BinOp (Binop.PlusA, e', c')) in let v' =
(e1', Exp.BinOp (Binop.PlusA None, e2, c'), Exp.BinOp (Binop.PlusA None, e', c'))
in
res := v' :: !res res := v' :: !res
| (e1, Exp.BinOp (Binop.PlusA, e2', Exp.Const (Const.Cint i)), e'), Rhs when Exp.equal e e2' | (e1, Exp.BinOp (Binop.PlusA _, e2', Exp.Const (Const.Cint i)), e'), Rhs
-> when Exp.equal e e2' ->
let c' = Exp.int (IntLit.neg i) in let c' = Exp.int (IntLit.neg i) in
let v' = (Exp.BinOp (Binop.PlusA, e1, c'), e2', Exp.BinOp (Binop.PlusA, e', c')) in let v' =
(Exp.BinOp (Binop.PlusA None, e1, c'), e2', Exp.BinOp (Binop.PlusA None, e', c'))
in
res := v' :: !res res := v' :: !res
| _ -> | _ ->
() ()
@ -943,20 +947,20 @@ let rec exp_partial_join (e1 : Exp.t) (e2 : Exp.t) : Exp.t =
| Exp.Var id, Exp.Lvar _ | Exp.Lvar _, Exp.Var id -> | Exp.Var id, Exp.Lvar _ | Exp.Lvar _, Exp.Var id ->
if Ident.is_normal id then ( L.d_strln "failure reason 21" ; raise Sil.JoinFail ) if Ident.is_normal id then ( L.d_strln "failure reason 21" ; raise Sil.JoinFail )
else Rename.extend e1 e2 Rename.ExtFresh else Rename.extend e1 e2 Rename.ExtFresh
| Exp.BinOp (Binop.PlusA, Exp.Var id1, Exp.Const _), Exp.Var id2 | Exp.BinOp (Binop.PlusA _, Exp.Var id1, Exp.Const _), Exp.Var id2
| Exp.Var id1, Exp.BinOp (Binop.PlusA, Exp.Var id2, Exp.Const _) | Exp.Var id1, Exp.BinOp (Binop.PlusA _, Exp.Var id2, Exp.Const _)
when ident_same_kind_primed_footprint id1 id2 -> when ident_same_kind_primed_footprint id1 id2 ->
Rename.extend e1 e2 Rename.ExtFresh Rename.extend e1 e2 Rename.ExtFresh
| Exp.BinOp (Binop.PlusA, Exp.Var id1, Exp.Const (Const.Cint c1)), Exp.Const (Const.Cint c2) | Exp.BinOp (Binop.PlusA _, Exp.Var id1, Exp.Const (Const.Cint c1)), Exp.Const (Const.Cint c2)
when can_rename id1 -> when can_rename id1 ->
let c2' = c2 -- c1 in let c2' = c2 -- c1 in
let e_res = Rename.extend (Exp.Var id1) (Exp.int c2') Rename.ExtFresh in let e_res = Rename.extend (Exp.Var id1) (Exp.int c2') Rename.ExtFresh in
Exp.BinOp (Binop.PlusA, e_res, Exp.int c1) Exp.BinOp (Binop.PlusA None, e_res, Exp.int c1)
| Exp.Const (Const.Cint c1), Exp.BinOp (Binop.PlusA, Exp.Var id2, Exp.Const (Const.Cint c2)) | Exp.Const (Const.Cint c1), Exp.BinOp (Binop.PlusA _, Exp.Var id2, Exp.Const (Const.Cint c2))
when can_rename id2 -> when can_rename id2 ->
let c1' = c1 -- c2 in let c1' = c1 -- c2 in
let e_res = Rename.extend (Exp.int c1') (Exp.Var id2) Rename.ExtFresh in let e_res = Rename.extend (Exp.int c1') (Exp.Var id2) Rename.ExtFresh in
Exp.BinOp (Binop.PlusA, e_res, Exp.int c2) Exp.BinOp (Binop.PlusA None, e_res, Exp.int c2)
| Exp.Cast (t1, e1), Exp.Cast (t2, e2) -> | Exp.Cast (t1, e1), Exp.Cast (t2, e2) ->
if not (Typ.equal t1 t2) then ( L.d_strln "failure reason 22" ; raise Sil.JoinFail ) if not (Typ.equal t1 t2) then ( L.d_strln "failure reason 22" ; raise Sil.JoinFail )
else else
@ -1011,11 +1015,11 @@ let rec exp_partial_join (e1 : Exp.t) (e2 : Exp.t) : Exp.t =
and length_partial_join len1 len2 = and length_partial_join len1 len2 =
match (len1, len2) with match (len1, len2) with
| Exp.BinOp (Binop.PlusA, e1, Exp.Const c1), Exp.BinOp (Binop.PlusA, e2, Exp.Const c2) -> | Exp.BinOp (Binop.PlusA _, e1, Exp.Const c1), Exp.BinOp (Binop.PlusA _, e2, Exp.Const c2) ->
let e' = exp_partial_join e1 e2 in let e' = exp_partial_join e1 e2 in
let c' = exp_partial_join (Exp.Const c1) (Exp.Const c2) in let c' = exp_partial_join (Exp.Const c1) (Exp.Const c2) in
Exp.BinOp (Binop.PlusA, e', c') Exp.BinOp (Binop.PlusA None, e', c')
| Exp.BinOp (Binop.PlusA, _, _), Exp.BinOp (Binop.PlusA, _, _) -> | Exp.BinOp (Binop.PlusA _, _, _), Exp.BinOp (Binop.PlusA _, _, _) ->
Rename.extend len1 len2 Rename.ExtFresh Rename.extend len1 len2 Rename.ExtFresh
| Exp.Var id1, Exp.Var id2 when Ident.equal id1 id2 -> | Exp.Var id1, Exp.Var id2 when Ident.equal id1 id2 ->
len1 len1

132
infer/src/biabduction/Prop.ml
Unescape View File

@ -543,7 +543,7 @@ let exp_collapse_consecutive_indices_prop (typ : Typ.t) exp =
let rec exp_remove (e0 : Exp.t) = let rec exp_remove (e0 : Exp.t) =
match e0 with match e0 with
| Lindex (Lindex (base, e1), e2) -> | Lindex (Lindex (base, e1), e2) ->
let e0' : Exp.t = Lindex (base, BinOp (PlusA, e1, e2)) in let e0' : Exp.t = Lindex (base, BinOp (PlusA None, e1, e2)) in
exp_remove e0' exp_remove e0'
| _ -> | _ ->
e0 e0
@ -712,7 +712,7 @@ module Normalize = struct
Exp.bool (IntLit.leq n m) Exp.bool (IntLit.leq n m)
| Const (Cfloat v), Const (Cfloat w) -> | Const (Cfloat v), Const (Cfloat w) ->
Exp.bool (v <= w) Exp.bool (v <= w)
| BinOp (PlusA, e3, Const (Cint n)), Const (Cint m) -> | BinOp (PlusA _, e3, Const (Cint n)), Const (Cint m) ->
BinOp (Le, e3, Exp.int (m -- n)) BinOp (Le, e3, Exp.int (m -- n))
| e1', e2' -> | e1', e2' ->
Exp.le e1' e2' ) Exp.le e1' e2' )
@ -722,11 +722,11 @@ module Normalize = struct
Exp.bool (IntLit.lt n m) Exp.bool (IntLit.lt n m)
| Const (Cfloat v), Const (Cfloat w) -> | Const (Cfloat v), Const (Cfloat w) ->
Exp.bool (v < w) Exp.bool (v < w)
| Const (Cint n), BinOp (MinusA, f1, f2) -> | Const (Cint n), BinOp ((MinusA _ as ominus), f1, f2) ->
BinOp (Le, BinOp (MinusA, f2, f1), Exp.int (IntLit.minus_one -- n)) BinOp (Le, BinOp (ominus, f2, f1), Exp.int (IntLit.minus_one -- n))
| BinOp (MinusA, f1, f2), Const (Cint n) -> | BinOp ((MinusA _ as ominus), f1, f2), Const (Cint n) ->
Exp.le (BinOp (MinusA, f1, f2)) (Exp.int (n -- IntLit.one)) Exp.le (BinOp (ominus, f1, f2)) (Exp.int (n -- IntLit.one))
| BinOp (PlusA, e3, Const (Cint n)), Const (Cint m) -> | BinOp (PlusA _, e3, Const (Cint n)), Const (Cint m) ->
BinOp (Lt, e3, Exp.int (m -- n)) BinOp (Lt, e3, Exp.int (m -- n))
| e1', e2' -> | e1', e2' ->
Exp.lt e1' e2' ) Exp.lt e1' e2' )
@ -788,18 +788,23 @@ module Normalize = struct
BinOp (LOr, e1', e2') ) BinOp (LOr, e1', e2') )
| BinOp (PlusPI, Lindex (ep, e1), e2) -> | BinOp (PlusPI, Lindex (ep, e1), e2) ->
(* array access with pointer arithmetic *) (* array access with pointer arithmetic *)
let e' : Exp.t = BinOp (PlusA, e1, e2) in let e' : Exp.t = BinOp (PlusA None, e1, e2) in
eval (Exp.Lindex (ep, e')) eval (Exp.Lindex (ep, e'))
| BinOp (PlusPI, BinOp (PlusPI, e11, e12), e2) -> | BinOp (PlusPI, BinOp (PlusPI, e11, e12), e2) ->
(* take care of pattern ((ptr + off1) + off2) *) (* take care of pattern ((ptr + off1) + off2) *)
(* progress: convert inner +I to +A *) (* progress: convert inner +I to +A *)
let e2' : Exp.t = BinOp (PlusA, e12, e2) in let e2' : Exp.t = BinOp (PlusA None, e12, e2) in
eval (Exp.BinOp (PlusPI, e11, e2')) eval (Exp.BinOp (PlusPI, e11, e2'))
| BinOp ((PlusA as oplus), e1, e2) | BinOp ((PlusPI as oplus), e1, e2) -> ( | BinOp ((PlusA _ as oplus), e1, e2) | BinOp ((PlusPI as oplus), e1, e2) -> (
let e1' = eval e1 in let e1' = eval e1 in
let e2' = eval e2 in let e2' = eval e2 in
let isPlusA = Binop.equal oplus Binop.PlusA in let isPlusA, ominus =
let ominus = if isPlusA then Binop.MinusA else Binop.MinusPI in match oplus with
| Binop.PlusA topt ->
(true, Binop.MinusA topt)
| _ ->
(false, Binop.MinusPI)
in
let ( +++ ) (x : Exp.t) (y : Exp.t) : Exp.t = let ( +++ ) (x : Exp.t) (y : Exp.t) : Exp.t =
match (x, y) with match (x, y) with
| _, Const (Cint i) when IntLit.iszero i -> | _, Const (Cint i) when IntLit.iszero i ->
@ -827,7 +832,7 @@ module Normalize = struct
(* pattern for arrays and extensible structs: (* pattern for arrays and extensible structs:
sizeof(struct s {... t[l]}) + k * sizeof(t)) = sizeof(struct s {... t[l + k]}) *) sizeof(struct s {... t[l]}) + k * sizeof(t)) = sizeof(struct s {... t[l + k]}) *)
| ( Sizeof ({typ; dynamic_length= len1_opt} as sizeof_data) | ( Sizeof ({typ; dynamic_length= len1_opt} as sizeof_data)
, BinOp (Mult, len2, Sizeof {typ= elt; dynamic_length= None}) ) , BinOp (Mult _, len2, Sizeof {typ= elt; dynamic_length= None}) )
when isPlusA && extensible_array_element_typ_equal elt typ -> when isPlusA && extensible_array_element_typ_equal elt typ ->
let len = match len1_opt with Some len1 -> len1 +++ len2 | None -> len2 in let len = match len1_opt with Some len1 -> len1 +++ len2 | None -> len2 in
Sizeof {sizeof_data with dynamic_length= Some len} Sizeof {sizeof_data with dynamic_length= Some len}
@ -841,15 +846,15 @@ module Normalize = struct
Exp.float (v +. w) Exp.float (v +. w)
| UnOp (Neg, f1, _), f2 | f2, UnOp (Neg, f1, _) -> | UnOp (Neg, f1, _), f2 | f2, UnOp (Neg, f1, _) ->
BinOp (ominus, f2, f1) BinOp (ominus, f2, f1)
| BinOp (PlusA, e, Const (Cint n1)), Const (Cint n2) | BinOp (PlusA _, e, Const (Cint n1)), Const (Cint n2)
| BinOp (PlusPI, e, Const (Cint n1)), Const (Cint n2) | BinOp (PlusPI, e, Const (Cint n1)), Const (Cint n2)
| Const (Cint n2), BinOp (PlusA, e, Const (Cint n1)) | Const (Cint n2), BinOp (PlusA _, e, Const (Cint n1))
| Const (Cint n2), BinOp (PlusPI, e, Const (Cint n1)) -> | Const (Cint n2), BinOp (PlusPI, e, Const (Cint n1)) ->
e +++ Exp.int (n1 ++ n2) e +++ Exp.int (n1 ++ n2)
| BinOp (MinusA, Const (Cint n1), e), Const (Cint n2) | BinOp (MinusA _, Const (Cint n1), e), Const (Cint n2)
| Const (Cint n2), BinOp (MinusA, Const (Cint n1), e) -> | Const (Cint n2), BinOp (MinusA _, Const (Cint n1), e) ->
Exp.int (n1 ++ n2) --- e Exp.int (n1 ++ n2) --- e
| BinOp (MinusA, e1, e2), e3 -> | BinOp (MinusA _, e1, e2), e3 ->
(* (e1-e2)+e3 --> e1 + (e3-e2) *) (* (e1-e2)+e3 --> e1 + (e3-e2) *)
(* progress: brings + to the outside *) (* progress: brings + to the outside *)
eval (e1 +++ (e3 --- e2)) eval (e1 +++ (e3 --- e2))
@ -863,11 +868,12 @@ module Normalize = struct
if abs && isPlusA then Exp.get_undefined false if abs && isPlusA then Exp.get_undefined false
else if abs && not isPlusA then e1' +++ Exp.get_undefined false else if abs && not isPlusA then e1' +++ Exp.get_undefined false
else e1' +++ e2' ) else e1' +++ e2' )
| BinOp ((MinusA as ominus), e1, e2) | BinOp ((MinusPI as ominus), e1, e2) -> ( | BinOp ((MinusA _ as ominus), e1, e2) | BinOp ((MinusPI as ominus), e1, e2) -> (
let e1' = eval e1 in let e1' = eval e1 in
let e2' = eval e2 in let e2' = eval e2 in
let isMinusA = Binop.equal ominus Binop.MinusA in let oplus =
let oplus = if isMinusA then Binop.PlusA else Binop.PlusPI in match ominus with Binop.MinusA topt -> Binop.PlusA topt | _ -> Binop.PlusPI
in
let ( +++ ) x y : Exp.t = BinOp (oplus, x, y) in let ( +++ ) x y : Exp.t = BinOp (oplus, x, y) in
let ( --- ) x y : Exp.t = BinOp (ominus, x, y) in let ( --- ) x y : Exp.t = BinOp (ominus, x, y) in
if Exp.equal e1' e2' then Exp.zero if Exp.equal e1' e2' then Exp.zero
@ -893,7 +899,7 @@ module Normalize = struct
if abs then Exp.get_undefined false else e1' --- e2' ) if abs then Exp.get_undefined false else e1' --- e2' )
| BinOp (MinusPP, e1, e2) -> | BinOp (MinusPP, e1, e2) ->
if abs then Exp.get_undefined false else BinOp (MinusPP, eval e1, eval e2) if abs then Exp.get_undefined false else BinOp (MinusPP, eval e1, eval e2)
| BinOp (Mult, e1, e2) -> ( | BinOp ((Mult _ as omult), e1, e2) -> (
let e1' = eval e1 in let e1' = eval e1 in
let e2' = eval e2 in let e2' = eval e2 in
match (e1', e2') with match (e1', e2') with
@ -914,11 +920,11 @@ module Normalize = struct
| Const (Cfloat v), Const (Cfloat w) -> | Const (Cfloat v), Const (Cfloat w) ->
Exp.float (v *. w) Exp.float (v *. w)
| Var _, Var _ -> | Var _, Var _ ->
BinOp (Mult, e1', e2') BinOp (omult, e1', e2')
| _, Sizeof _ | Sizeof _, _ -> | _, Sizeof _ | Sizeof _, _ ->
BinOp (Mult, e1', e2') BinOp (omult, e1', e2')
| _, _ -> | _, _ ->
if abs then Exp.get_undefined false else BinOp (Mult, e1', e2') ) if abs then Exp.get_undefined false else BinOp (omult, e1', e2') )
| BinOp (Div, e1, e2) -> ( | BinOp (Div, e1, e2) -> (
let e1' = eval e1 in let e1' = eval e1 in
let e2' = eval e2 in let e2' = eval e2 in
@ -969,7 +975,7 @@ module Normalize = struct
| _, Const (Cint m) when IntLit.iszero m -> | _, Const (Cint m) when IntLit.iszero m ->
eval e1 eval e1
| _, Const (Cint m) when IntLit.isone m -> | _, Const (Cint m) when IntLit.isone m ->
eval (Exp.BinOp (PlusA, e1, e1)) eval (Exp.BinOp (PlusA None, e1, e1))
| Const (Cint m), _ when IntLit.iszero m -> | Const (Cint m), _ when IntLit.iszero m ->
e1 e1
| _ -> | _ ->
@ -1036,7 +1042,7 @@ module Normalize = struct
eval (Exp.BinOp (PlusPI, Lvar pv, e2)) eval (Exp.BinOp (PlusPI, Lvar pv, e2))
| Lindex (BinOp (PlusPI, ep, e1), e2) -> | Lindex (BinOp (PlusPI, ep, e1), e2) ->
(* array access with pointer arithmetic *) (* array access with pointer arithmetic *)
let e' : Exp.t = BinOp (PlusA, e1, e2) in let e' : Exp.t = BinOp (PlusA None, e1, e2) in
eval (Exp.Lindex (ep, e')) eval (Exp.Lindex (ep, e'))
| Lindex (e1, e2) -> | Lindex (e1, e2) ->
let e1' = eval e1 in let e1' = eval e1 in
@ -1077,19 +1083,19 @@ module Normalize = struct
(* base <= n case *) (* base <= n case *)
let nbase = exp_normalize_noabs tenv Sil.sub_empty base in let nbase = exp_normalize_noabs tenv Sil.sub_empty base in
match nbase with match nbase with
| BinOp (PlusA, base', Const (Cint n')) -> | BinOp (PlusA _, base', Const (Cint n')) ->
let new_offset = Exp.int (n -- n') in let new_offset = Exp.int (n -- n') in
let new_e : Exp.t = BinOp (Le, base', new_offset) in let new_e : Exp.t = BinOp (Le, base', new_offset) in
Aeq (new_e, Exp.one) Aeq (new_e, Exp.one)
| BinOp (PlusA, Const (Cint n'), base') -> | BinOp (PlusA _, Const (Cint n'), base') ->
let new_offset = Exp.int (n -- n') in let new_offset = Exp.int (n -- n') in
let new_e : Exp.t = BinOp (Le, base', new_offset) in let new_e : Exp.t = BinOp (Le, base', new_offset) in
Aeq (new_e, Exp.one) Aeq (new_e, Exp.one)
| BinOp (MinusA, base', Const (Cint n')) -> | BinOp (MinusA _, base', Const (Cint n')) ->
let new_offset = Exp.int (n ++ n') in let new_offset = Exp.int (n ++ n') in
let new_e : Exp.t = BinOp (Le, base', new_offset) in let new_e : Exp.t = BinOp (Le, base', new_offset) in
Aeq (new_e, Exp.one) Aeq (new_e, Exp.one)
| BinOp (MinusA, Const (Cint n'), base') -> | BinOp (MinusA _, Const (Cint n'), base') ->
let new_offset = Exp.int (n' -- n -- IntLit.one) in let new_offset = Exp.int (n' -- n -- IntLit.one) in
let new_e : Exp.t = BinOp (Lt, new_offset, base') in let new_e : Exp.t = BinOp (Lt, new_offset, base') in
Aeq (new_e, Exp.one) Aeq (new_e, Exp.one)
@ -1104,19 +1110,19 @@ module Normalize = struct
(* n < base case *) (* n < base case *)
let nbase = exp_normalize_noabs tenv Sil.sub_empty base in let nbase = exp_normalize_noabs tenv Sil.sub_empty base in
match nbase with match nbase with
| BinOp (PlusA, base', Const (Cint n')) -> | BinOp (PlusA _, base', Const (Cint n')) ->
let new_offset = Exp.int (n -- n') in let new_offset = Exp.int (n -- n') in
let new_e : Exp.t = BinOp (Lt, new_offset, base') in let new_e : Exp.t = BinOp (Lt, new_offset, base') in
Aeq (new_e, Exp.one) Aeq (new_e, Exp.one)
| BinOp (PlusA, Const (Const.Cint n'), base') -> | BinOp (PlusA _, Const (Const.Cint n'), base') ->
let new_offset = Exp.int (n -- n') in let new_offset = Exp.int (n -- n') in
let new_e : Exp.t = BinOp (Lt, new_offset, base') in let new_e : Exp.t = BinOp (Lt, new_offset, base') in
Aeq (new_e, Exp.one) Aeq (new_e, Exp.one)
| BinOp (MinusA, base', Const (Cint n')) -> | BinOp (MinusA _, base', Const (Cint n')) ->
let new_offset = Exp.int (n ++ n') in let new_offset = Exp.int (n ++ n') in
let new_e : Exp.t = BinOp (Lt, new_offset, base') in let new_e : Exp.t = BinOp (Lt, new_offset, base') in
Aeq (new_e, Exp.one) Aeq (new_e, Exp.one)
| BinOp (MinusA, Const (Cint n'), base') -> | BinOp (MinusA _, Const (Cint n'), base') ->
let new_offset = Exp.int (n' -- n -- IntLit.one) in let new_offset = Exp.int (n' -- n -- IntLit.one) in
let new_e : Exp.t = BinOp (Le, base', new_offset) in let new_e : Exp.t = BinOp (Le, base', new_offset) in
Aeq (new_e, Exp.one) Aeq (new_e, Exp.one)
@ -1139,11 +1145,11 @@ module Normalize = struct
match e with match e with
| Const (Cint n) -> | Const (Cint n) ->
([], [], n) ([], [], n)
| BinOp (PlusA, e1, e2) | BinOp (PlusPI, e1, e2) -> | BinOp (PlusA _, e1, e2) | BinOp (PlusPI, e1, e2) ->
let pos1, neg1, n1 = exp_to_posnegoff e1 in let pos1, neg1, n1 = exp_to_posnegoff e1 in
let pos2, neg2, n2 = exp_to_posnegoff e2 in let pos2, neg2, n2 = exp_to_posnegoff e2 in
(pos1 @ pos2, neg1 @ neg2, n1 ++ n2) (pos1 @ pos2, neg1 @ neg2, n1 ++ n2)
| BinOp (MinusA, e1, e2) | BinOp (MinusPI, e1, e2) | BinOp (MinusPP, e1, e2) -> | BinOp (MinusA _, e1, e2) | BinOp (MinusPI, e1, e2) | BinOp (MinusPP, e1, e2) ->
let pos1, neg1, n1 = exp_to_posnegoff e1 in let pos1, neg1, n1 = exp_to_posnegoff e1 in
let pos2, neg2, n2 = exp_to_posnegoff e2 in let pos2, neg2, n2 = exp_to_posnegoff e2 in
(pos1 @ neg2, neg1 @ pos2, n1 -- n2) (pos1 @ neg2, neg1 @ pos2, n1 -- n2)
@ -1179,7 +1185,7 @@ module Normalize = struct
| [e] -> | [e] ->
e e
| e :: el -> | e :: el ->
BinOp (PlusA, e, exp_list_to_sum el) BinOp (PlusA None, e, exp_list_to_sum el)
in in
let norm_from_exp e : Exp.t = let norm_from_exp e : Exp.t =
match normalize_posnegoff (exp_to_posnegoff e) with match normalize_posnegoff (exp_to_posnegoff e) with
@ -1190,7 +1196,7 @@ module Normalize = struct
| pos, [], n -> | pos, [], n ->
BinOp (Le, exp_list_to_sum pos, Exp.int (IntLit.zero -- n)) BinOp (Le, exp_list_to_sum pos, Exp.int (IntLit.zero -- n))
| pos, neg, n -> | pos, neg, n ->
let lhs_e : Exp.t = BinOp (MinusA, exp_list_to_sum pos, exp_list_to_sum neg) in let lhs_e : Exp.t = BinOp (MinusA None, exp_list_to_sum pos, exp_list_to_sum neg) in
BinOp (Le, lhs_e, Exp.int (IntLit.zero -- n)) BinOp (Le, lhs_e, Exp.int (IntLit.zero -- n))
in in
let ineq = let ineq =
@ -1198,10 +1204,10 @@ module Normalize = struct
in in
match ineq with match ineq with
| BinOp (Le, e1, e2) -> | BinOp (Le, e1, e2) ->
let e : Exp.t = BinOp (MinusA, e1, e2) in let e : Exp.t = BinOp (MinusA None, e1, e2) in
mk_inequality tenv (norm_from_exp e) mk_inequality tenv (norm_from_exp e)
| BinOp (Lt, e1, e2) -> | BinOp (Lt, e1, e2) ->
let e : Exp.t = BinOp (MinusA, BinOp (MinusA, e1, e2), Exp.minus_one) in let e : Exp.t = BinOp (MinusA None, BinOp (MinusA None, e1, e2), Exp.minus_one) in
mk_inequality tenv (norm_from_exp e) mk_inequality tenv (norm_from_exp e)
| _ -> | _ ->
a a
@ -1214,15 +1220,15 @@ module Normalize = struct
let a = Sil.atom_sub sub a0 in let a = Sil.atom_sub sub a0 in
let rec normalize_eq (eq : Exp.t * Exp.t) = let rec normalize_eq (eq : Exp.t * Exp.t) =
match eq with match eq with
| BinOp (PlusA, e1, Const (Cint n1)), Const (Cint n2) | BinOp (PlusA _, e1, Const (Cint n1)), Const (Cint n2)
(* e1+n1==n2 ---> e1==n2-n1 *) (* e1+n1==n2 ---> e1==n2-n1 *)
| BinOp (PlusPI, e1, Const (Cint n1)), Const (Cint n2) -> | BinOp (PlusPI, e1, Const (Cint n1)), Const (Cint n2) ->
(e1, Exp.int (n2 -- n1)) (e1, Exp.int (n2 -- n1))
| BinOp (MinusA, e1, Const (Cint n1)), Const (Cint n2) | BinOp (MinusA _, e1, Const (Cint n1)), Const (Cint n2)
(* e1-n1==n2 ---> e1==n1+n2 *) (* e1-n1==n2 ---> e1==n1+n2 *)
| BinOp (MinusPI, e1, Const (Cint n1)), Const (Cint n2) -> | BinOp (MinusPI, e1, Const (Cint n1)), Const (Cint n2) ->
(e1, Exp.int (n1 ++ n2)) (e1, Exp.int (n1 ++ n2))
| BinOp (MinusA, Const (Cint n1), e1), Const (Cint n2) -> | BinOp (MinusA _, Const (Cint n1), e1), Const (Cint n2) ->
(* n1-e1 == n2 -> e1==n1-n2 *) (* n1-e1 == n2 -> e1==n1-n2 *)
(e1, Exp.int (n1 -- n2)) (e1, Exp.int (n1 -- n2))
| Lfield (e1', fld1, _), Lfield (e2', fld2, _) -> | Lfield (e1', fld1, _), Lfield (e2', fld2, _) ->
@ -1231,13 +1237,13 @@ module Normalize = struct
if Exp.equal idx1 idx2 then normalize_eq (e1', e2') if Exp.equal idx1 idx2 then normalize_eq (e1', e2')
else if Exp.equal e1' e2' then normalize_eq (idx1, idx2) else if Exp.equal e1' e2' then normalize_eq (idx1, idx2)
else eq else eq
| BinOp ((PlusA | PlusPI | MinusA | MinusPI), e1, e2), e1' when Exp.equal e1 e1' -> | BinOp ((PlusA _ | PlusPI | MinusA _ | MinusPI), e1, e2), e1' when Exp.equal e1 e1' ->
(e2, Exp.int IntLit.zero) (e2, Exp.int IntLit.zero)
| BinOp ((PlusA | PlusPI), e2, e1), e1' when Exp.equal e1 e1' -> | BinOp ((PlusA _ | PlusPI), e2, e1), e1' when Exp.equal e1 e1' ->
(e2, Exp.int IntLit.zero) (e2, Exp.int IntLit.zero)
| e1', BinOp ((PlusA | PlusPI | MinusA | MinusPI), e1, e2) when Exp.equal e1 e1' -> | e1', BinOp ((PlusA _ | PlusPI | MinusA _ | MinusPI), e1, e2) when Exp.equal e1 e1' ->
(e2, Exp.int IntLit.zero) (e2, Exp.int IntLit.zero)
| e1', BinOp ((PlusA | PlusPI), e2, e1) when Exp.equal e1 e1' -> | e1', BinOp ((PlusA _ | PlusPI), e2, e1) when Exp.equal e1 e1' ->
(e2, Exp.int IntLit.zero) (e2, Exp.int IntLit.zero)
| _ -> | _ ->
eq eq
@ -1454,32 +1460,44 @@ module Normalize = struct
let hpred' = mk_ptsto_exp tenv Fld_init (root, size, None) inst in let hpred' = mk_ptsto_exp tenv Fld_init (root, size, None) inst in
replace_hpred hpred' replace_hpred hpred'
| ( Earray | ( Earray
(BinOp (Mult, Sizeof {typ= t; dynamic_length= None; subtype= st1}, x), esel, inst) (BinOp (Mult _, Sizeof {typ= t; dynamic_length= None; subtype= st1}, x), esel, inst)
, Sizeof {typ= {desc= Tarray {elt}} as arr} ) , Sizeof {typ= {desc= Tarray {elt}} as arr} )
when Typ.equal t elt -> when Typ.equal t elt ->
let dynamic_length = Some x in let dynamic_length = Some x in
let sizeof_data = {Exp.typ= arr; nbytes= None; dynamic_length; subtype= st1} in let sizeof_data = {Exp.typ= arr; nbytes= None; dynamic_length; subtype= st1} in
let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof sizeof_data, None) inst in let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof sizeof_data, None) inst in
replace_hpred (replace_array_contents hpred' esel) replace_hpred (replace_array_contents hpred' esel)
| ( Earray (BinOp (Mult, x, Sizeof {typ; dynamic_length= None; subtype}), esel, inst) | ( Earray (BinOp (Mult _, x, Sizeof {typ; dynamic_length= None; subtype}), esel, inst)
, Sizeof {typ= {desc= Tarray {elt}} as arr} ) , Sizeof {typ= {desc= Tarray {elt}} as arr} )
when Typ.equal typ elt -> when Typ.equal typ elt ->
let sizeof_data = {Exp.typ= arr; nbytes= None; dynamic_length= Some x; subtype} in let sizeof_data = {Exp.typ= arr; nbytes= None; dynamic_length= Some x; subtype} in
let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof sizeof_data, None) inst in let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof sizeof_data, None) inst in
replace_hpred (replace_array_contents hpred' esel) replace_hpred (replace_array_contents hpred' esel)
| ( Earray (BinOp (Mult, Sizeof {typ; dynamic_length= Some len; subtype}, x), esel, inst) | ( Earray
( BinOp ((Mult _ as omult), Sizeof {typ; dynamic_length= Some len; subtype}, x)
, esel
, inst )
, Sizeof {typ= {desc= Tarray {elt}} as arr} ) , Sizeof {typ= {desc= Tarray {elt}} as arr} )
when Typ.equal typ elt -> when Typ.equal typ elt ->
let sizeof_data = let sizeof_data =
{Exp.typ= arr; nbytes= None; dynamic_length= Some (Exp.BinOp (Mult, x, len)); subtype} { Exp.typ= arr
; nbytes= None
; dynamic_length= Some (Exp.BinOp (omult, x, len))
; subtype }
in in
let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof sizeof_data, None) inst in let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof sizeof_data, None) inst in
replace_hpred (replace_array_contents hpred' esel) replace_hpred (replace_array_contents hpred' esel)
| ( Earray (BinOp (Mult, x, Sizeof {typ; dynamic_length= Some len; subtype}), esel, inst) | ( Earray
( BinOp ((Mult _ as omult), x, Sizeof {typ; dynamic_length= Some len; subtype})
, esel
, inst )
, Sizeof {typ= {desc= Tarray {elt}} as arr} ) , Sizeof {typ= {desc= Tarray {elt}} as arr} )
when Typ.equal typ elt -> when Typ.equal typ elt ->
let sizeof_data = let sizeof_data =
{Exp.typ= arr; nbytes= None; dynamic_length= Some (Exp.BinOp (Mult, x, len)); subtype} { Exp.typ= arr
; nbytes= None
; dynamic_length= Some (Exp.BinOp (omult, x, len))
; subtype }
in in
let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof sizeof_data, None) inst in let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof sizeof_data, None) inst in
replace_hpred (replace_array_contents hpred' esel) replace_hpred (replace_array_contents hpred' esel)
@ -1957,7 +1975,7 @@ let sigma_get_array_indices sigma =
let compute_reindexing_from_indices list = let compute_reindexing_from_indices list =
let get_id_offset (e : Exp.t) = let get_id_offset (e : Exp.t) =
match e with match e with
| BinOp (PlusA, Var id, Const (Cint offset)) -> | BinOp (PlusA _, Var id, Const (Cint offset)) ->
if Ident.is_primed id then Some (id, offset) else None if Ident.is_primed id then Some (id, offset) else None
| _ -> | _ ->
None None
@ -1984,7 +2002,7 @@ let compute_reindexing_from_indices list =
let id, offset = match get_id_offset x with None -> assert false | Some io -> io in let id, offset = match get_id_offset x with None -> assert false | Some io -> io in
let base_new : Exp.t = Var (Ident.create_fresh Ident.kprimed) in let base_new : Exp.t = Var (Ident.create_fresh Ident.kprimed) in
let offset_new = Exp.int (IntLit.neg offset) in let offset_new = Exp.int (IntLit.neg offset) in
let exp_new : Exp.t = BinOp (PlusA, base_new, offset_new) in let exp_new : Exp.t = BinOp (PlusA None, base_new, offset_new) in
(id, exp_new) (id, exp_new)
in in
let reindexing = List.map ~f:transform list_passed in let reindexing = List.map ~f:transform list_passed in
@ -2016,7 +2034,7 @@ let prop_rename_array_indices tenv prop =
let indices = sigma_get_array_indices prop.sigma in let indices = sigma_get_array_indices prop.sigma in
let not_same_base_lt_offsets (e1 : Exp.t) (e2 : Exp.t) = let not_same_base_lt_offsets (e1 : Exp.t) (e2 : Exp.t) =
match (e1, e2) with match (e1, e2) with
| BinOp (PlusA, e1', Const (Cint n1')), BinOp (PlusA, e2', Const (Cint n2')) -> | BinOp (PlusA _, e1', Const (Cint n1')), BinOp (PlusA _, e2', Const (Cint n2')) ->
not (Exp.equal e1' e2' && IntLit.lt n1' n2') not (Exp.equal e1' e2' && IntLit.lt n1' n2')
| _ -> | _ ->
true true

68
infer/src/biabduction/Prover.ml
Unescape View File

@ -87,17 +87,17 @@ end = struct
let equal = [%compare.equal: t] let equal = [%compare.equal: t]
let to_leq (e1, e2, n) = (Exp.BinOp (Binop.MinusA, e1, e2), Exp.int n) let to_leq (e1, e2, n) = (Exp.BinOp (Binop.MinusA None, e1, e2), Exp.int n)
let to_lt (e1, e2, n) = let to_lt (e1, e2, n) =
(Exp.int (IntLit.zero -- n -- IntLit.one), Exp.BinOp (Binop.MinusA, e2, e1)) (Exp.int (IntLit.zero -- n -- IntLit.one), Exp.BinOp (Binop.MinusA None, e2, e1))
let to_triple entry = entry let to_triple entry = entry
let from_leq acc (e1, e2) = let from_leq acc (e1, e2) =
match (e1, e2) with match (e1, e2) with
| ( Exp.BinOp (Binop.MinusA, (Exp.Var id11 as e11), (Exp.Var id12 as e12)) | ( Exp.BinOp (Binop.MinusA _, (Exp.Var id11 as e11), (Exp.Var id12 as e12))
, Exp.Const (Const.Cint n) ) , Exp.Const (Const.Cint n) )
when not (Ident.equal id11 id12) -> ( when not (Ident.equal id11 id12) -> (
match IntLit.to_signed n with match IntLit.to_signed n with
@ -112,7 +112,7 @@ end = struct
let from_lt acc (e1, e2) = let from_lt acc (e1, e2) =
match (e1, e2) with match (e1, e2) with
| ( Exp.Const (Const.Cint n) | ( Exp.Const (Const.Cint n)
, Exp.BinOp (Binop.MinusA, (Exp.Var id21 as e21), (Exp.Var id22 as e22)) ) , Exp.BinOp (Binop.MinusA _, (Exp.Var id21 as e21), (Exp.Var id22 as e22)) )
when not (Ident.equal id21 id22) -> ( when not (Ident.equal id21 id22) -> (
match IntLit.to_signed n with match IntLit.to_signed n with
| None -> | None ->
@ -496,11 +496,11 @@ end = struct
match (e1, e2) with match (e1, e2) with
| Exp.Const (Const.Cint n1), Exp.Const (Const.Cint n2) -> | Exp.Const (Const.Cint n1), Exp.Const (Const.Cint n2) ->
IntLit.leq n1 n2 IntLit.leq n1 n2
| ( Exp.BinOp (Binop.MinusA, Exp.Sizeof {nbytes= Some nb1}, Exp.Sizeof {nbytes= Some nb2}) | ( Exp.BinOp (Binop.MinusA _, Exp.Sizeof {nbytes= Some nb1}, Exp.Sizeof {nbytes= Some nb2})
, Exp.Const (Const.Cint n2) ) -> , Exp.Const (Const.Cint n2) ) ->
(* [ sizeof(t1) - sizeof(t2) <= n2 ] *) (* [ sizeof(t1) - sizeof(t2) <= n2 ] *)
IntLit.(leq (sub (of_int nb1) (of_int nb2)) n2) IntLit.(leq (sub (of_int nb1) (of_int nb2)) n2)
| ( Exp.BinOp (Binop.MinusA, Exp.Sizeof {typ= t1}, Exp.Sizeof {typ= t2}) | ( Exp.BinOp (Binop.MinusA _, Exp.Sizeof {typ= t1}, Exp.Sizeof {typ= t2})
, Exp.Const (Const.Cint n2) ) , Exp.Const (Const.Cint n2) )
when IntLit.isminusone n2 && type_size_comparable t1 t2 -> when IntLit.isminusone n2 && type_size_comparable t1 t2 ->
(* [ sizeof(t1) - sizeof(t2) <= -1 ] *) (* [ sizeof(t1) - sizeof(t2) <= -1 ] *)
@ -639,8 +639,8 @@ let check_equal tenv prop e1_0 e2_0 =
let check_equal () = Exp.equal n_e1 n_e2 in let check_equal () = Exp.equal n_e1 n_e2 in
let check_equal_const () = let check_equal_const () =
match (n_e1, n_e2) with match (n_e1, n_e2) with
| Exp.BinOp (Binop.PlusA, e1, Exp.Const (Const.Cint d)), e2 | Exp.BinOp (Binop.PlusA _, e1, Exp.Const (Const.Cint d)), e2
| e2, Exp.BinOp (Binop.PlusA, e1, Exp.Const (Const.Cint d)) -> | e2, Exp.BinOp (Binop.PlusA _, e1, Exp.Const (Const.Cint d)) ->
if Exp.equal e1 e2 then IntLit.iszero d else false if Exp.equal e1 e2 then IntLit.iszero d else false
| Exp.Const c1, Exp.Lindex (Exp.Const c2, Exp.Const (Const.Cint i)) when IntLit.iszero i -> | Exp.Const c1, Exp.Lindex (Exp.Const c2, Exp.Const (Const.Cint i)) when IntLit.iszero i ->
Const.equal c1 c2 Const.equal c1 c2
@ -693,9 +693,9 @@ let get_bounds tenv prop e0 =
let e_norm = Prop.exp_normalize_prop ~destructive:true tenv prop e0 in let e_norm = Prop.exp_normalize_prop ~destructive:true tenv prop e0 in
let e_root, off = let e_root, off =
match e_norm with match e_norm with
| Exp.BinOp (Binop.PlusA, e, Exp.Const (Const.Cint n1)) -> | Exp.BinOp (Binop.PlusA _, e, Exp.Const (Const.Cint n1)) ->
(e, IntLit.neg n1) (e, IntLit.neg n1)
| Exp.BinOp (Binop.MinusA, e, Exp.Const (Const.Cint n1)) -> | Exp.BinOp (Binop.MinusA _, e, Exp.Const (Const.Cint n1)) ->
(e, n1) (e, n1)
| _ -> | _ ->
(e_norm, IntLit.zero) (e_norm, IntLit.zero)
@ -719,20 +719,20 @@ let check_disequal tenv prop e1 e2 =
| Exp.Const c1, Exp.Lindex (Exp.Const c2, Exp.Const (Const.Cint d)) -> | Exp.Const c1, Exp.Lindex (Exp.Const c2, Exp.Const (Const.Cint d)) ->
if IntLit.iszero d then not (Const.equal c1 c2) (* offset=0 is no offset *) if IntLit.iszero d then not (Const.equal c1 c2) (* offset=0 is no offset *)
else Const.equal c1 c2 (* same base, different offsets *) else Const.equal c1 c2 (* same base, different offsets *)
| ( Exp.BinOp (Binop.PlusA, e1, Exp.Const (Const.Cint d1)) | ( Exp.BinOp (Binop.PlusA _, e1, Exp.Const (Const.Cint d1))
, Exp.BinOp (Binop.PlusA, e2, Exp.Const (Const.Cint d2)) ) -> , Exp.BinOp (Binop.PlusA _, e2, Exp.Const (Const.Cint d2)) ) ->
if Exp.equal e1 e2 then IntLit.neq d1 d2 else false if Exp.equal e1 e2 then IntLit.neq d1 d2 else false
| Exp.BinOp (Binop.PlusA, e1, Exp.Const (Const.Cint d)), e2 | Exp.BinOp (Binop.PlusA _, e1, Exp.Const (Const.Cint d)), e2
| e2, Exp.BinOp (Binop.PlusA, e1, Exp.Const (Const.Cint d)) -> | e2, Exp.BinOp (Binop.PlusA _, e1, Exp.Const (Const.Cint d)) ->
if Exp.equal e1 e2 then not (IntLit.iszero d) else false if Exp.equal e1 e2 then not (IntLit.iszero d) else false
| Exp.Lindex (Exp.Const c1, Exp.Const (Const.Cint d)), Exp.Const c2 -> | Exp.Lindex (Exp.Const c1, Exp.Const (Const.Cint d)), Exp.Const c2 ->
if IntLit.iszero d then not (Const.equal c1 c2) else Const.equal c1 c2 if IntLit.iszero d then not (Const.equal c1 c2) else Const.equal c1 c2
| Exp.Lindex (Exp.Const c1, Exp.Const d1), Exp.Lindex (Exp.Const c2, Exp.Const d2) -> | Exp.Lindex (Exp.Const c1, Exp.Const d1), Exp.Lindex (Exp.Const c2, Exp.Const d2) ->
Const.equal c1 c2 && not (Const.equal d1 d2) Const.equal c1 c2 && not (Const.equal d1 d2)
| Exp.Const (Const.Cint n), Exp.BinOp (Binop.Mult, Exp.Sizeof _, e21) | Exp.Const (Const.Cint n), Exp.BinOp (Binop.Mult _, Exp.Sizeof _, e21)
| Exp.Const (Const.Cint n), Exp.BinOp (Binop.Mult, e21, Sizeof _) | Exp.Const (Const.Cint n), Exp.BinOp (Binop.Mult _, e21, Sizeof _)
| Exp.BinOp (Binop.Mult, Exp.Sizeof _, e21), Exp.Const (Const.Cint n) | Exp.BinOp (Binop.Mult _, Exp.Sizeof _, e21), Exp.Const (Const.Cint n)
| Exp.BinOp (Binop.Mult, e21, Exp.Sizeof _), Exp.Const (Const.Cint n) -> | Exp.BinOp (Binop.Mult _, e21, Exp.Sizeof _), Exp.Const (Const.Cint n) ->
IntLit.iszero n && not (Exp.is_zero e21) IntLit.iszero n && not (Exp.is_zero e21)
| Exp.Lvar pv0, Exp.Lvar pv1 -> | Exp.Lvar pv0, Exp.Lvar pv1 ->
(* Addresses of any two local vars must be different *) (* Addresses of any two local vars must be different *)
@ -831,7 +831,7 @@ let check_le_normalized tenv prop e1 e2 =
(* L.d_str "check_le_normalized "; Sil.d_exp e1; L.d_str " "; Sil.d_exp e2; L.d_ln (); *) (* L.d_str "check_le_normalized "; Sil.d_exp e1; L.d_str " "; Sil.d_exp e2; L.d_ln (); *)
let eL, eR, off = let eL, eR, off =
match (e1, e2) with match (e1, e2) with
| Exp.BinOp (Binop.MinusA, f1, f2), Exp.Const (Const.Cint n) -> | Exp.BinOp (Binop.MinusA _, f1, f2), Exp.Const (Const.Cint n) ->
if Exp.equal f1 f2 then (Exp.zero, Exp.zero, n) else (f1, f2, n) if Exp.equal f1 f2 then (Exp.zero, Exp.zero, n) else (f1, f2, n)
| _ -> | _ ->
(e1, e2, IntLit.zero) (e1, e2, IntLit.zero)
@ -1354,10 +1354,10 @@ let exp_imply tenv calc_missing (subs : subst2) e1_in e2_in : subst2 =
match (e1, e2) with match (e1, e2) with
| Exp.Var v1, Exp.Var v2 -> | Exp.Var v1, Exp.Var v2 ->
var_imply subs v1 v2 var_imply subs v1 v2
| Exp.BinOp ((PlusA | PlusPI | MinusA | MinusPI), Exp.Var v1, e2), Exp.Var v2 | Exp.BinOp ((PlusA _ | PlusPI | MinusA _ | MinusPI), Exp.Var v1, e2), Exp.Var v2
when Ident.equal v1 v2 -> when Ident.equal v1 v2 ->
do_imply subs e2 Exp.zero do_imply subs e2 Exp.zero
| Exp.BinOp ((PlusA | PlusPI), e2, Exp.Var v1), Exp.Var v2 when Ident.equal v1 v2 -> | Exp.BinOp ((PlusA _ | PlusPI), e2, Exp.Var v1), Exp.Var v2 when Ident.equal v1 v2 ->
do_imply subs e2 Exp.zero do_imply subs e2 Exp.zero
| e1, Exp.Var v2 -> | e1, Exp.Var v2 ->
let occurs_check v e = let occurs_check v e =
@ -1372,16 +1372,16 @@ let exp_imply tenv calc_missing (subs : subst2) e1_in e2_in : subst2 =
let sub2' = extend_sub (snd subs) v2 e1 in let sub2' = extend_sub (snd subs) v2 e1 in
(fst subs, sub2') (fst subs, sub2')
else raise (IMPL_EXC ("expressions not equal", subs, EXC_FALSE_EXPS (e1, e2))) else raise (IMPL_EXC ("expressions not equal", subs, EXC_FALSE_EXPS (e1, e2)))
| e1, Exp.BinOp (Binop.PlusA, (Exp.Var v2 as e2), e2') | e1, Exp.BinOp (Binop.PlusA _, (Exp.Var v2 as e2), e2')
when Ident.is_primed v2 || Ident.is_footprint v2 -> when Ident.is_primed v2 || Ident.is_footprint v2 ->
(* here e2' could also be a variable that we could try to substitute (as in the next match (* here e2' could also be a variable that we could try to substitute (as in the next match
case), but we ignore that to avoid backtracking *) case), but we ignore that to avoid backtracking *)
let e' = Exp.BinOp (Binop.MinusA, e1, e2') in let e' = Exp.BinOp (Binop.MinusA None, e1, e2') in
do_imply subs (Prop.exp_normalize_noabs tenv Sil.sub_empty e') e2 do_imply subs (Prop.exp_normalize_noabs tenv Sil.sub_empty e') e2
| e1, Exp.BinOp (Binop.PlusA, e2, (Exp.Var v2 as e2')) | e1, Exp.BinOp (Binop.PlusA _, e2, (Exp.Var v2 as e2'))
when Ident.is_primed v2 || Ident.is_footprint v2 -> when Ident.is_primed v2 || Ident.is_footprint v2 ->
(* symmetric of above case *) (* symmetric of above case *)
let e' = Exp.BinOp (Binop.MinusA, e1, e2') in let e' = Exp.BinOp (Binop.MinusA None, e1, e2') in
do_imply subs (Prop.exp_normalize_noabs tenv Sil.sub_empty e') e2 do_imply subs (Prop.exp_normalize_noabs tenv Sil.sub_empty e') e2
| Exp.Var id, Exp.Lvar pv when Ident.is_footprint id && Pvar.is_local pv -> | Exp.Var id, Exp.Lvar pv when Ident.is_footprint id && Pvar.is_local pv ->
(* Footprint var could never be the same as local address *) (* Footprint var could never be the same as local address *)
@ -1405,14 +1405,14 @@ let exp_imply tenv calc_missing (subs : subst2) e1_in e2_in : subst2 =
| Exp.Const (Const.Cint _), Exp.BinOp (Binop.PlusPI, _, _) -> | Exp.Const (Const.Cint _), Exp.BinOp (Binop.PlusPI, _, _) ->
raise raise
(IMPL_EXC ("pointer+index cannot evaluate to a constant", subs, EXC_FALSE_EXPS (e1, e2))) (IMPL_EXC ("pointer+index cannot evaluate to a constant", subs, EXC_FALSE_EXPS (e1, e2)))
| Exp.Const (Const.Cint n1), Exp.BinOp (Binop.PlusA, f1, Exp.Const (Const.Cint n2)) -> | Exp.Const (Const.Cint n1), Exp.BinOp (Binop.PlusA _, f1, Exp.Const (Const.Cint n2)) ->
do_imply subs (Exp.int (n1 -- n2)) f1 do_imply subs (Exp.int (n1 -- n2)) f1
| Exp.BinOp (op1, e1, f1), Exp.BinOp (op2, e2, f2) when Binop.equal op1 op2 -> | Exp.BinOp (op1, e1, f1), Exp.BinOp (op2, e2, f2) when Binop.equal op1 op2 ->
do_imply (do_imply subs e1 e2) f1 f2 do_imply (do_imply subs e1 e2) f1 f2
| Exp.BinOp (Binop.PlusA, Exp.Var v1, e1), e2 -> | Exp.BinOp (Binop.PlusA _, Exp.Var v1, e1), e2 ->
do_imply subs (Exp.Var v1) (Exp.BinOp (Binop.MinusA, e2, e1)) do_imply subs (Exp.Var v1) (Exp.BinOp (Binop.MinusA None, e2, e1))
| Exp.BinOp (Binop.PlusPI, Exp.Lvar pv1, e1), e2 -> | Exp.BinOp (Binop.PlusPI, Exp.Lvar pv1, e1), e2 ->
do_imply subs (Exp.Lvar pv1) (Exp.BinOp (Binop.MinusA, e2, e1)) do_imply subs (Exp.Lvar pv1) (Exp.BinOp (Binop.MinusA None, e2, e1))
| ( Exp.Sizeof {typ= t1; dynamic_length= None; subtype= st1} | ( Exp.Sizeof {typ= t1; dynamic_length= None; subtype= st1}
, Exp.Sizeof {typ= t2; dynamic_length= None; subtype= st2} ) , Exp.Sizeof {typ= t2; dynamic_length= None; subtype= st2} )
when Typ.equal t1 t2 && Subtype.equal_modulo_flag st1 st2 -> when Typ.equal t1 t2 && Subtype.equal_modulo_flag st1 st2 ->
@ -1479,9 +1479,9 @@ let path_to_id path =
let array_len_imply tenv calc_missing subs len1 len2 indices2 = let array_len_imply tenv calc_missing subs len1 len2 indices2 =
match (len1, len2) with match (len1, len2) with
| _, Exp.Var _ | _, Exp.Var _
| _, Exp.BinOp (Binop.PlusA, Exp.Var _, _) | _, Exp.BinOp (Binop.PlusA _, Exp.Var _, _)
| _, Exp.BinOp (Binop.PlusA, _, Exp.Var _) | _, Exp.BinOp (Binop.PlusA _, _, Exp.Var _)
| Exp.BinOp (Binop.Mult, _, _), _ -> ( | Exp.BinOp (Binop.Mult _, _, _), _ -> (
try exp_imply tenv calc_missing subs len1 len2 with IMPL_EXC (s, subs', x) -> try exp_imply tenv calc_missing subs len1 len2 with IMPL_EXC (s, subs', x) ->
raise (IMPL_EXC ("array len:" ^ s, subs', x)) ) raise (IMPL_EXC ("array len:" ^ s, subs', x)) )
| _ -> | _ ->
@ -1806,7 +1806,7 @@ let expand_hpred_pointer =
let hpred' = Sil.Hpointsto (e, Sil.Earray (len, [(ind, se)], Sil.inst_none), t') in let hpred' = Sil.Hpointsto (e, Sil.Earray (len, [(ind, se)], Sil.inst_none), t') in
expand true true hpred' expand true true hpred'
| Sil.Hpointsto (Exp.BinOp (Binop.PlusPI, e1, e2), Sil.Earray (len, esel, inst), t) -> | Sil.Hpointsto (Exp.BinOp (Binop.PlusPI, e1, e2), Sil.Earray (len, esel, inst), t) ->
let shift_exp e = Exp.BinOp (Binop.PlusA, e, e2) in let shift_exp e = Exp.BinOp (Binop.PlusA None, e, e2) in
let len' = shift_exp len in let len' = shift_exp len in
let esel' = List.map ~f:(fun (e, se) -> (shift_exp e, se)) esel in let esel' = List.map ~f:(fun (e, se) -> (shift_exp e, se)) esel in
let hpred' = Sil.Hpointsto (e1, Sil.Earray (len', esel', inst), t) in let hpred' = Sil.Hpointsto (e1, Sil.Earray (len', esel', inst), t) in
@ -2520,7 +2520,7 @@ let check_array_bounds tenv (sub1, sub2) prop =
(* L.d_strln_color Orange "check_bound "; (* L.d_strln_color Orange "check_bound ";
Sil.d_exp len1; L.d_str " "; Sil.d_exp len2; L.d_ln(); *) Sil.d_exp len1; L.d_str " "; Sil.d_exp len2; L.d_ln(); *)
let indices_to_check = let indices_to_check =
[Exp.BinOp (Binop.PlusA, len2, Exp.minus_one)] [Exp.BinOp (Binop.PlusA None, len2, Exp.minus_one)]
(* only check len *) (* only check len *)
in in
List.iter ~f:(fail_if_le len1) indices_to_check List.iter ~f:(fail_if_le len1) indices_to_check

10
infer/src/biabduction/Rearrange.ml
Unescape View File

@ -37,7 +37,7 @@ let check_bad_index tenv pname p len index loc =
Prover.check_atom tenv p index_too_large || Prover.check_atom tenv p index_negative Prover.check_atom tenv p index_too_large || Prover.check_atom tenv p index_negative
in in
let index_provably_in_bound () = let index_provably_in_bound () =
let len_minus_one = Exp.BinOp (Binop.PlusA, len, Exp.minus_one) in let len_minus_one = Exp.BinOp (Binop.PlusA None, len, Exp.minus_one) in
let index_not_too_large = let index_not_too_large =
Prop.mk_inequality tenv (Exp.BinOp (Binop.Le, index, len_minus_one)) Prop.mk_inequality tenv (Exp.BinOp (Binop.Le, index, len_minus_one))
in in
@ -457,11 +457,7 @@ let mk_ptsto_exp_footprint pname tenv orig_prop (lexp, typ) max_stamp inst :
raise (Exceptions.Dangling_pointer_dereference (None, err_desc, __POS__)) ) ; raise (Exceptions.Dangling_pointer_dereference (None, err_desc, __POS__)) ) ;
let off_foot, eqs = laundry_offset_for_footprint max_stamp off in let off_foot, eqs = laundry_offset_for_footprint max_stamp off in
let subtype = let subtype =
match !Language.curr_language with match !Language.curr_language with Clang -> Subtype.exact | Java -> Subtype.subtypes
| Clang ->
Subtype.exact
| Java ->
Subtype.subtypes
in in
let create_ptsto footprint_part off0 = let create_ptsto footprint_part off0 =
match (root, off0, typ.Typ.desc) with match (root, off0, typ.Typ.desc) with
@ -1600,7 +1596,7 @@ let check_dereference_error tenv pdesc (prop : Prop.normal Prop.t) lexp loc =
(* try to remove an offset if any, and find the attribute there *) (* try to remove an offset if any, and find the attribute there *)
let root_no_offset = let root_no_offset =
match root with match root with
| Exp.BinOp ((Binop.PlusPI | Binop.PlusA | Binop.MinusPI | Binop.MinusA), base, _) -> | Exp.BinOp ((Binop.PlusPI | Binop.PlusA _ | Binop.MinusPI | Binop.MinusA _), base, _) ->
base base
| _ -> | _ ->
root root

6
infer/src/bufferoverrun/bufferOverrunDomainRelation.ml
Unescape View File

@ -677,11 +677,11 @@ module Make (Manager : Manager_S) = struct
match (raw_of_exp' e1, raw_of_exp' e2) with match (raw_of_exp' e1, raw_of_exp' e2) with
| Some re1, Some re2 -> ( | Some re1, Some re2 -> (
match bop with match bop with
| Binop.PlusA -> | Binop.PlusA _ ->
Some (raw_bop_make Texpr1.Add re1 re2) Some (raw_bop_make Texpr1.Add re1 re2)
| Binop.MinusA -> | Binop.MinusA _ ->
Some (raw_bop_make Texpr1.Sub re1 re2) Some (raw_bop_make Texpr1.Sub re1 re2)
| Binop.Mult -> | Binop.Mult _ ->
Some (raw_bop_make Texpr1.Mul re1 re2) Some (raw_bop_make Texpr1.Mul re1 re2)
| _ -> | _ ->
try_get_sym_f e ) try_get_sym_f e )

8
infer/src/bufferoverrun/bufferOverrunModels.ml
Unescape View File

@ -65,8 +65,8 @@ let no_check _model_env _mem cond_set = cond_set
- array size - array size
- flexible array size *) - flexible array size *)
let get_malloc_info : Exp.t -> Typ.t * Int.t option * Exp.t * Exp.t option = function let get_malloc_info : Exp.t -> Typ.t * Int.t option * Exp.t * Exp.t option = function
| Exp.BinOp (Binop.Mult, Exp.Sizeof {typ; nbytes}, length) | Exp.BinOp (Binop.Mult _, Exp.Sizeof {typ; nbytes}, length)
| Exp.BinOp (Binop.Mult, length, Exp.Sizeof {typ; nbytes}) -> | Exp.BinOp (Binop.Mult _, length, Exp.Sizeof {typ; nbytes}) ->
(typ, nbytes, length, None) (typ, nbytes, length, None)
(* In Java all arrays are dynamically allocated *) (* In Java all arrays are dynamically allocated *)
| Exp.Sizeof {typ; nbytes; dynamic_length= Some arr_length} when Language.curr_language_is Java | Exp.Sizeof {typ; nbytes; dynamic_length= Some arr_length} when Language.curr_language_is Java
@ -128,7 +128,7 @@ let malloc size_exp =
let calloc size_exp stride_exp = let calloc size_exp stride_exp =
let byte_size_exp = Exp.BinOp (Binop.Mult, size_exp, stride_exp) in let byte_size_exp = Exp.BinOp (Binop.Mult (Some Typ.size_t), size_exp, stride_exp) in
malloc byte_size_exp malloc byte_size_exp
@ -171,7 +171,7 @@ let realloc src_exp size_exp =
let placement_new size_exp (src_exp1, t1) src_arg2_opt = let placement_new size_exp (src_exp1, t1) src_arg2_opt =
match (t1.Typ.desc, src_arg2_opt) with match (t1.Typ.desc, src_arg2_opt) with
| Tint _, None | Tint _, Some (_, {Typ.desc= Tint _}) -> | Tint _, None | Tint _, Some (_, {Typ.desc= Tint _}) ->
malloc (Exp.BinOp (Binop.PlusA, size_exp, src_exp1)) malloc (Exp.BinOp (Binop.PlusA (Some Typ.size_t), size_exp, src_exp1))
| Tstruct (CppClass (name, _)), None | Tstruct (CppClass (name, _)), None
when [%compare.equal: string list] (QualifiedCppName.to_list name) ["std"; "nothrow_t"] -> when [%compare.equal: string list] (QualifiedCppName.to_list name) ["std"; "nothrow_t"] ->
malloc size_exp malloc size_exp

6
infer/src/bufferoverrun/bufferOverrunSemantics.ml
Unescape View File

@ -198,17 +198,17 @@ and eval_binop : Binop.t -> Exp.t -> Exp.t -> Mem.astate -> Val.t =
let v1 = eval e1 mem in let v1 = eval e1 mem in
let v2 = eval e2 mem in let v2 = eval e2 mem in
match binop with match binop with
| Binop.PlusA -> | Binop.PlusA _ ->
Val.plus_a v1 v2 Val.plus_a v1 v2
| Binop.PlusPI -> | Binop.PlusPI ->
Val.plus_pi v1 v2 Val.plus_pi v1 v2
| Binop.MinusA -> | Binop.MinusA _ ->
Val.minus_a v1 v2 Val.minus_a v1 v2
| Binop.MinusPI -> | Binop.MinusPI ->
Val.minus_pi v1 v2 Val.minus_pi v1 v2
| Binop.MinusPP -> | Binop.MinusPP ->
Val.minus_pp v1 v2 Val.minus_pp v1 v2
| Binop.Mult -> | Binop.Mult _ ->
Val.mult v1 v2 Val.mult v1 v2
| Binop.Div -> | Binop.Div ->
Val.div v1 v2 Val.div v1 v2

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

@ -19,11 +19,11 @@ let compound_assignment_binary_operation_instruction boi_kind (e1, t1) typ e2 lo
let bop = let bop =
match boi_kind with match boi_kind with
| `AddAssign -> | `AddAssign ->
if Typ.is_pointer t1 then Binop.PlusPI else Binop.PlusA if Typ.is_pointer t1 then Binop.PlusPI else Binop.PlusA (Typ.get_ikind_opt typ)
| `SubAssign -> | `SubAssign ->
if Typ.is_pointer t1 then Binop.MinusPI else Binop.MinusA if Typ.is_pointer t1 then Binop.MinusPI else Binop.MinusA (Typ.get_ikind_opt typ)
| `MulAssign -> | `MulAssign ->
Binop.Mult Binop.Mult (Typ.get_ikind_opt typ)
| `DivAssign -> | `DivAssign ->
Binop.Div Binop.Div
| `ShlAssign -> | `ShlAssign ->
@ -66,9 +66,9 @@ let binary_operation_instruction source_range boi ((e1, t1) as e1_with_typ) typ
| `Add -> | `Add ->
if Typ.is_pointer t1 then (binop_exp Binop.PlusPI, []) if Typ.is_pointer t1 then (binop_exp Binop.PlusPI, [])
else if Typ.is_pointer t2 then (binop_exp ~change_order:true Binop.PlusPI, []) else if Typ.is_pointer t2 then (binop_exp ~change_order:true Binop.PlusPI, [])
else (binop_exp Binop.PlusA, []) else (binop_exp (Binop.PlusA (Typ.get_ikind_opt typ)), [])
| `Mul -> | `Mul ->
(binop_exp Binop.Mult, []) (binop_exp (Binop.Mult (Typ.get_ikind_opt typ)), [])
| `Div -> | `Div ->
(binop_exp Binop.Div, []) (binop_exp Binop.Div, [])
| `Rem -> | `Rem ->
@ -76,7 +76,7 @@ let binary_operation_instruction source_range boi ((e1, t1) as e1_with_typ) typ
| `Sub -> | `Sub ->
if Typ.is_pointer t1 then if Typ.is_pointer t1 then
if Typ.is_pointer t2 then (binop_exp Binop.MinusPP, []) else (binop_exp Binop.MinusPI, []) if Typ.is_pointer t2 then (binop_exp Binop.MinusPP, []) else (binop_exp Binop.MinusPI, [])
else (binop_exp Binop.MinusA, []) else (binop_exp (Binop.MinusA (Typ.get_ikind_opt typ)), [])
| `Shl -> | `Shl ->
(binop_exp Binop.Shiftlt, []) (binop_exp Binop.Shiftlt, [])
| `Shr -> | `Shr ->
@ -129,13 +129,13 @@ let unary_operation_instruction translation_unit_context uoi e typ loc =
| `PostInc -> | `PostInc ->
let id = Ident.create_fresh Ident.knormal in let id = Ident.create_fresh Ident.knormal in
let instr1 = Sil.Load (id, e, typ, loc) in let instr1 = Sil.Load (id, e, typ, loc) in
let bop = if Typ.is_pointer typ then Binop.PlusPI else Binop.PlusA in let bop = if Typ.is_pointer typ then Binop.PlusPI else Binop.PlusA (Typ.get_ikind_opt typ) in
let e_plus_1 = Exp.BinOp (bop, Exp.Var id, Exp.Const (Const.Cint IntLit.one)) in let e_plus_1 = Exp.BinOp (bop, Exp.Var id, Exp.Const (Const.Cint IntLit.one)) in
(Exp.Var id, [instr1; Sil.Store (e, typ, e_plus_1, loc)]) (Exp.Var id, [instr1; Sil.Store (e, typ, e_plus_1, loc)])
| `PreInc -> | `PreInc ->
let id = Ident.create_fresh Ident.knormal in let id = Ident.create_fresh Ident.knormal in
let instr1 = Sil.Load (id, e, typ, loc) in let instr1 = Sil.Load (id, e, typ, loc) in
let bop = if Typ.is_pointer typ then Binop.PlusPI else Binop.PlusA in let bop = if Typ.is_pointer typ then Binop.PlusPI else Binop.PlusA (Typ.get_ikind_opt typ) in
let e_plus_1 = Exp.BinOp (bop, Exp.Var id, Exp.Const (Const.Cint IntLit.one)) in let e_plus_1 = Exp.BinOp (bop, Exp.Var id, Exp.Const (Const.Cint IntLit.one)) in
let exp = let exp =
if CGeneral_utils.is_cpp_translation translation_unit_context then e else e_plus_1 if CGeneral_utils.is_cpp_translation translation_unit_context then e else e_plus_1
@ -144,13 +144,17 @@ let unary_operation_instruction translation_unit_context uoi e typ loc =
| `PostDec -> | `PostDec ->
let id = Ident.create_fresh Ident.knormal in let id = Ident.create_fresh Ident.knormal in
let instr1 = Sil.Load (id, e, typ, loc) in let instr1 = Sil.Load (id, e, typ, loc) in
let bop = if Typ.is_pointer typ then Binop.MinusPI else Binop.MinusA in let bop =
if Typ.is_pointer typ then Binop.MinusPI else Binop.MinusA (Typ.get_ikind_opt typ)
in
let e_minus_1 = Exp.BinOp (bop, Exp.Var id, Exp.Const (Const.Cint IntLit.one)) in let e_minus_1 = Exp.BinOp (bop, Exp.Var id, Exp.Const (Const.Cint IntLit.one)) in
(Exp.Var id, [instr1; Sil.Store (e, typ, e_minus_1, loc)]) (Exp.Var id, [instr1; Sil.Store (e, typ, e_minus_1, loc)])
| `PreDec -> | `PreDec ->
let id = Ident.create_fresh Ident.knormal in let id = Ident.create_fresh Ident.knormal in
let instr1 = Sil.Load (id, e, typ, loc) in let instr1 = Sil.Load (id, e, typ, loc) in
let bop = if Typ.is_pointer typ then Binop.MinusPI else Binop.MinusA in let bop =
if Typ.is_pointer typ then Binop.MinusPI else Binop.MinusA (Typ.get_ikind_opt typ)
in
let e_minus_1 = Exp.BinOp (bop, Exp.Var id, Exp.Const (Const.Cint IntLit.one)) in let e_minus_1 = Exp.BinOp (bop, Exp.Var id, Exp.Const (Const.Cint IntLit.one)) in
let exp = let exp =
if CGeneral_utils.is_cpp_translation translation_unit_context then e else e_minus_1 if CGeneral_utils.is_cpp_translation translation_unit_context then e else e_minus_1
@ -254,4 +258,4 @@ let sil_const_plus_one const =
| Exp.Const (Const.Cint n) -> | Exp.Const (Const.Cint n) ->
Exp.Const (Const.Cint (IntLit.add n IntLit.one)) Exp.Const (Const.Cint (IntLit.add n IntLit.one))
| _ -> | _ ->
Exp.BinOp (Binop.PlusA, const, Exp.Const (Const.Cint IntLit.one)) Exp.BinOp (Binop.PlusA None, const, Exp.Const (Const.Cint IntLit.one))

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

@ -345,7 +345,7 @@ let create_alloc_instrs ~alloc_builtin ?size_exp ?placement_args_exps sil_loc fu
let sizeof_exp = let sizeof_exp =
match size_exp with match size_exp with
| Some exp -> | Some exp ->
Exp.BinOp (Binop.Mult, sizeof_exp_, exp) Exp.BinOp (Binop.Mult (Some Typ.size_t), sizeof_exp_, exp)
| None -> | None ->
sizeof_exp_ sizeof_exp_
in in

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

@ -177,14 +177,14 @@ let get_constant (c : JBir.const) =
Const.Cstr (JBasics.jstr_pp jstr) Const.Cstr (JBasics.jstr_pp jstr)
let get_binop binop = let get_binop typ binop =
match binop with match binop with
| JBir.Add _ -> | JBir.Add _ ->
Binop.PlusA Binop.PlusA (Typ.get_ikind_opt typ)
| JBir.Sub _ -> | JBir.Sub _ ->
Binop.MinusA Binop.MinusA (Typ.get_ikind_opt typ)
| JBir.Mult _ -> | JBir.Mult _ ->
Binop.Mult Binop.Mult (Typ.get_ikind_opt typ)
| JBir.Div _ -> | JBir.Div _ ->
Binop.Div Binop.Div
| JBir.Rem _ -> | JBir.Rem _ ->
@ -543,7 +543,7 @@ let rec expression (context : JContext.t) pc expr =
let instrs = (instrs1 @ (deref_array_instr :: instrs2)) @ [load_instr] in let instrs = (instrs1 @ (deref_array_instr :: instrs2)) @ [load_instr] in
(instrs, Exp.Var id, type_of_expr) (instrs, Exp.Var id, type_of_expr)
| other_binop -> | other_binop ->
let sil_binop = get_binop other_binop in let sil_binop = get_binop type_of_expr other_binop in
let sil_expr = Exp.BinOp (sil_binop, sil_ex1, sil_ex2) in let sil_expr = Exp.BinOp (sil_binop, sil_ex1, sil_ex2) in
(instrs1 @ instrs2, sil_expr, type_of_expr) ) (instrs1 @ instrs2, sil_expr, type_of_expr) )
| JBir.Field (ex, cn, fs) -> | JBir.Field (ex, cn, fs) ->

Write Preview
Loading…
Cancel
Save