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

[infer] Use inline record for Typ.Tarray

Browse Source 
Summary: It uses the inline record type for `Typ.Tarray`.

Reviewed By: mbouaziz

Differential Revision: D7042272

fbshipit-source-id: c793016
master
Sungkeun Cho 7 years ago committed by Facebook Github Bot
parent f55f382a78
commit 373e6b39cc
21 changed files with 104 additions and 94 deletions
Show Stats Download Patch File Download Diff File

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

@ -161,7 +161,7 @@ module Raw = struct
if include_array_indexes then of_exp_ index_exp typ [] [] else [] if include_array_indexes then of_exp_ index_exp typ [] [] else []
in in
let array_access = ArrayAccess (typ, index_access_paths) in let array_access = ArrayAccess (typ, index_access_paths) in
let array_typ = Typ.mk (Tarray (typ, None, None)) in let array_typ = Typ.mk_array typ in
of_exp_ root_exp array_typ (array_access :: accesses) acc of_exp_ root_exp array_typ (array_access :: accesses) acc
| Exp.Cast (cast_typ, cast_exp) -> | Exp.Cast (cast_typ, cast_exp) ->
of_exp_ cast_exp cast_typ [] acc of_exp_ cast_exp cast_typ [] acc

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

@ -127,7 +127,7 @@ module T = struct
| Tptr of t * ptr_kind (** pointer type *) | Tptr of t * ptr_kind (** pointer type *)
| Tstruct of name (** structured value type name *) | Tstruct of name (** structured value type name *)
| TVar of string (** type variable (ie. C++ template variables) *) | TVar of string (** type variable (ie. C++ template variables) *)
| Tarray of t * IntLit.t option * IntLit.t option | Tarray of {elt: t; length: IntLit.t option; stride: IntLit.t option}
(** array type with statically fixed length and stride *) (** array type with statically fixed length and stride *)
[@@deriving compare] [@@deriving compare]
@ -185,6 +185,10 @@ let mk ?default ?quals desc : t =
mk_aux ?default ?quals desc mk_aux ?default ?quals desc
let mk_array ?default ?quals ?length ?stride elt : t =
mk ?default ?quals (Tarray {elt; length; stride})
let void_star = mk (Tptr (mk Tvoid, Pk_pointer)) let void_star = mk (Tptr (mk Tvoid, Pk_pointer))
let merge_quals quals1 quals2 = let merge_quals quals1 quals2 =
@ -222,9 +226,9 @@ let rec pp_full pe f typ =
F.fprintf f "%a(%s)" (pp_full pe) typ (ptr_kind_string pk |> escape pe) F.fprintf f "%a(%s)" (pp_full pe) typ (ptr_kind_string pk |> escape pe)
| Tptr (typ, pk) -> | Tptr (typ, pk) ->
F.fprintf f "%a%s" (pp_full pe) typ (ptr_kind_string pk |> escape pe) F.fprintf f "%a%s" (pp_full pe) typ (ptr_kind_string pk |> escape pe)
| Tarray (typ, static_len, static_stride) -> | Tarray {elt; length; stride} ->
let pp_int_opt fmt = function Some x -> IntLit.pp fmt x | None -> F.fprintf fmt "_" in let pp_int_opt fmt = function Some x -> IntLit.pp fmt x | None -> F.fprintf fmt "_" in
F.fprintf f "%a[%a*%a]" (pp_full pe) typ pp_int_opt static_len pp_int_opt static_stride F.fprintf f "%a[%a*%a]" (pp_full pe) elt pp_int_opt length pp_int_opt stride
in in
F.fprintf f "%a%a" pp_desc typ pp_quals typ F.fprintf f "%a%a" pp_desc typ pp_quals typ
@ -279,10 +283,10 @@ let rec sub_type subst generic_typ : t =
mk ~quals:(merge_quals t.quals generic_typ.quals) t.desc mk ~quals:(merge_quals t.quals generic_typ.quals) t.desc
| None -> | None ->
generic_typ ) generic_typ )
| Tarray (typ, arg1, arg2) -> | Tarray {elt= typ; length; stride} ->
let typ' = sub_type subst typ in let typ' = sub_type subst typ in
if phys_equal typ typ' then generic_typ if phys_equal typ typ' then generic_typ
else mk ~default:generic_typ (Tarray (typ', arg1, arg2)) else mk_array ~default:generic_typ typ' ?length ?stride
| Tptr (typ, arg) -> | Tptr (typ, arg) ->
let typ' = sub_type subst typ in let typ' = sub_type subst typ in
if phys_equal typ typ' then generic_typ else mk ~default:generic_typ (Tptr (typ', arg)) if phys_equal typ typ' then generic_typ else mk ~default:generic_typ (Tptr (typ', arg))
@ -483,7 +487,7 @@ let strip_ptr typ = match typ.desc with Tptr (t, _) -> t | _ -> assert false
(** If an array type, return the type of the element. (** If an array type, return the type of the element.
If not, return the default type if given, otherwise raise an exception *) If not, return the default type if given, otherwise raise an exception *)
let array_elem default_opt typ = let array_elem default_opt typ =
match typ.desc with Tarray (t_el, _, _) -> t_el | _ -> unsome "array_elem" default_opt match typ.desc with Tarray {elt} -> elt | _ -> unsome "array_elem" default_opt
let is_class_of_kind check_fun typ = let is_class_of_kind check_fun typ =
@ -650,7 +654,7 @@ module Procname = struct
mk (Tfloat FDouble) mk (Tfloat FDouble)
| typ_str when String.contains typ_str '[' -> | typ_str when String.contains typ_str '[' ->
let stripped_typ = String.sub typ_str ~pos:0 ~len:(String.length typ_str - 2) in let stripped_typ = String.sub typ_str ~pos:0 ~len:(String.length typ_str - 2) in
mk (Tptr (mk (Tarray (java_from_string stripped_typ, None, None)), Pk_pointer)) mk (Tptr (mk_array (java_from_string stripped_typ), Pk_pointer))
| typ_str -> | typ_str ->
mk (Tstruct (Name.Java.from_string typ_str)) mk (Tstruct (Name.Java.from_string typ_str))
in in
@ -1057,6 +1061,7 @@ module Procname = struct
| _ -> | _ ->
QualifiedCppName.empty QualifiedCppName.empty
(** Convert a proc name to a filename *) (** Convert a proc name to a filename *)
let to_concrete_filename ?crc_only pname = let to_concrete_filename ?crc_only pname =
(* filenames for clang procs are REVERSED qualifiers with '#' as separator *) (* filenames for clang procs are REVERSED qualifiers with '#' as separator *)
@ -1266,8 +1271,8 @@ module Struct = struct
(** the element typ of the final extensible array in the given typ, if any *) (** the element typ of the final extensible array in the given typ, if any *)
let rec get_extensible_array_element_typ ~lookup (typ: T.t) = let rec get_extensible_array_element_typ ~lookup (typ: T.t) =
match typ.desc with match typ.desc with
| Tarray (typ, _, _) -> | Tarray {elt} ->
Some typ Some elt
| Tstruct name -> ( | Tstruct name -> (
match lookup name with match lookup name with
| Some {fields} -> ( | Some {fields} -> (

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

@ -78,8 +78,8 @@ and desc =
| Tptr of t * ptr_kind (** pointer type *) | Tptr of t * ptr_kind (** pointer type *)
| Tstruct of name (** structured value type name *) | Tstruct of name (** structured value type name *)
| TVar of string (** type variable (ie. C++ template variables) *) | TVar of string (** type variable (ie. C++ template variables) *)
| Tarray of t * IntLit.t option * IntLit.t option | Tarray of {elt: t; length: IntLit.t option; stride: IntLit.t option}
(** array type with statically fixed stride and length *) (** array type with statically fixed length and stride *)
[@@deriving compare] [@@deriving compare]
and name = and name =
@ -109,6 +109,9 @@ and template_spec_info =
val mk : ?default:t -> ?quals:type_quals -> desc -> t val mk : ?default:t -> ?quals:type_quals -> desc -> t
(** Create Typ.t from given desc. if [default] is passed then use its value to set other fields such as quals *) (** Create Typ.t from given desc. if [default] is passed then use its value to set other fields such as quals *)
val mk_array : ?default:t -> ?quals:type_quals -> ?length:IntLit.t -> ?stride:IntLit.t -> t -> t
(** Create an array type from a given element type. If [length] or [stride] value is given, use them as static length and size. *)
val void_star : t val void_star : t
(** void* type *) (** void* type *)

9
infer/src/backend/BuiltinDefn.ml
Unescape View File

@ -45,7 +45,7 @@ let extract_array_type typ =
| Typ.Tarray _ -> | Typ.Tarray _ ->
Some typ Some typ
| Typ.Tptr (elt, _) -> | Typ.Tptr (elt, _) ->
Some (Typ.mk ~default:typ (Tarray (elt, None, None))) Some (Typ.mk_array ~default:typ elt)
| _ -> | _ ->
None None
@ -556,10 +556,11 @@ let execute_alloc mk can_return_null {Builtin.pdesc; tenv; prop_; path; ret_id;
| Exp.Lfield _ | Exp.Lfield _
| Exp.Lindex _ -> | Exp.Lindex _ ->
e e
| Exp.Sizeof {typ= {Typ.desc= Tarray ({Typ.desc= Tint ik}, _, _)}; dynamic_length= Some len} | Exp.Sizeof {typ= {Typ.desc= Tarray {elt= {Typ.desc= Tint ik}}}; dynamic_length= Some len}
when Typ.ikind_is_char ik -> when Typ.ikind_is_char ik ->
evaluate_char_sizeof len evaluate_char_sizeof len
| Exp.Sizeof {typ= {Typ.desc= Tarray ({Typ.desc= Tint ik}, Some len, _)}; dynamic_length= None} | Exp.Sizeof
{typ= {Typ.desc= Tarray {elt= {Typ.desc= Tint ik}; length= Some len}}; dynamic_length= None}
when Typ.ikind_is_char ik -> when Typ.ikind_is_char ik ->
evaluate_char_sizeof (Exp.Const (Const.Cint len)) evaluate_char_sizeof (Exp.Const (Const.Cint len))
| Exp.Sizeof _ -> | Exp.Sizeof _ ->
@ -585,7 +586,7 @@ let execute_alloc mk can_return_null {Builtin.pdesc; tenv; prop_; path; ret_id;
in in
let cnt_te = let cnt_te =
Exp.Sizeof Exp.Sizeof
{ typ= Typ.mk (Tarray (Typ.mk (Tint Typ.IChar), None, Some (IntLit.of_int 1))) { typ= Typ.mk_array (Typ.mk (Tint Typ.IChar)) ~stride:(IntLit.of_int 1)
; nbytes= None ; nbytes= None
; dynamic_length= Some size_exp' ; dynamic_length= Some size_exp'
; subtype= Subtype.exact } ; subtype= Subtype.exact }

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

@ -85,7 +85,7 @@ end = struct
get_strexp_at_syn_offsets tenv se' t' syn_offs' get_strexp_at_syn_offsets tenv se' t' syn_offs'
| None -> | None ->
fail () ) fail () )
| Sil.Earray (_, esel, _), Typ.Tarray (t', _, _), (Index ind) :: syn_offs' -> | Sil.Earray (_, esel, _), Typ.Tarray {elt= t'}, (Index ind) :: syn_offs' ->
let se' = snd (List.find_exn ~f:(fun (i', _) -> Exp.equal i' ind) esel) in let se' = snd (List.find_exn ~f:(fun (i', _) -> Exp.equal i' ind) esel) in
get_strexp_at_syn_offsets tenv se' t' syn_offs' get_strexp_at_syn_offsets tenv se' t' syn_offs'
| _ -> | _ ->
@ -115,7 +115,7 @@ end = struct
Sil.Estruct (fsel', inst) Sil.Estruct (fsel', inst)
| None -> | None ->
assert false ) assert false )
| Sil.Earray (len, esel, inst), Tarray (t', _, _), (Index idx) :: syn_offs' -> | Sil.Earray (len, esel, inst), Tarray {elt= t'}, (Index idx) :: syn_offs' ->
let se' = snd (List.find_exn ~f:(fun (i', _) -> Exp.equal i' idx) esel) in let se' = snd (List.find_exn ~f:(fun (i', _) -> Exp.equal i' idx) esel) in
let se_mod = replace_strexp_at_syn_offsets tenv se' t' syn_offs' update in let se_mod = replace_strexp_at_syn_offsets tenv se' t' syn_offs' update in
let esel' = let esel' =
@ -181,8 +181,8 @@ end = struct
find_offset_fsel sigma_other hpred root offs fsel fields typ find_offset_fsel sigma_other hpred root offs fsel fields typ
| None -> | None ->
() ) () )
| Sil.Earray (_, esel, _), Tarray (t, _, _) -> | Sil.Earray (_, esel, _), Tarray {elt} ->
find_offset_esel sigma_other hpred root offs esel t find_offset_esel sigma_other hpred root offs esel elt
| _ -> | _ ->
() ()
and find_offset_fsel sigma_other hpred root offs fsel ftal typ = and find_offset_fsel sigma_other hpred root offs fsel ftal typ =
@ -474,7 +474,7 @@ let keep_only_indices tenv (p: Prop.normal Prop.t) (path: StrexpMatch.path) (ind
(** If the type is array, check whether we should do abstraction *) (** If the type is array, check whether we should do abstraction *)
let array_typ_can_abstract {Typ.desc} = let array_typ_can_abstract {Typ.desc} =
match desc with match desc with
| Tarray ({desc= Tptr ({desc= Tfun _}, _)}, _, _) -> | Tarray {elt= {desc= Tptr ({desc= Tfun _}, _)}} ->
false (* don't abstract arrays of pointers *) false (* don't abstract arrays of pointers *)
| _ -> | _ ->
true true

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

@ -1093,12 +1093,13 @@ and typ_partial_join (t1: Typ.t) (t2: Typ.t) =
when Typ.equal_ptr_kind pk1 pk2 && Typ.equal_quals t1.quals t2.quals -> when Typ.equal_ptr_kind pk1 pk2 && Typ.equal_quals t1.quals t2.quals ->
Typ.mk ~default:t1 (Tptr (typ_partial_join t1 t2, pk1)) Typ.mk ~default:t1 (Tptr (typ_partial_join t1 t2, pk1))
(* quals are the same for t1 and t2 *) (* quals are the same for t1 and t2 *)
| Typ.Tarray (typ1, len1, stride1), Typ.Tarray (typ2, len2, stride2) | ( Typ.Tarray {elt= typ1; length= len1; stride= stride1}
, Typ.Tarray {elt= typ2; length= len2; stride= stride2} )
when Typ.equal_quals typ1.quals typ2.quals -> when Typ.equal_quals typ1.quals typ2.quals ->
let t = typ_partial_join typ1 typ2 in let elt = typ_partial_join typ1 typ2 in
let len = static_length_partial_join len1 len2 in let length = static_length_partial_join len1 len2 in
let stride = static_length_partial_join stride1 stride2 in let stride = static_length_partial_join stride1 stride2 in
Typ.mk ~default:t1 (Tarray (t, len, stride)) Typ.mk_array ~default:t1 elt ?length ?stride
(* quals are the same for t1 and t2 *) (* quals are the same for t1 and t2 *)
| _ when Typ.equal t1 t2 -> | _ when Typ.equal t1 t2 ->
t1 (* common case *) t1 (* common case *)

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

@ -337,7 +337,7 @@ let rec dotty_mk_node pe sigma =
let n = !dotty_state_count in let n = !dotty_state_count in
incr dotty_state_count ; incr dotty_state_count ;
let do_hpred_lambda exp_color = function let do_hpred_lambda exp_color = function
| ( Sil.Hpointsto (e, Sil.Earray (e', l, _), Exp.Sizeof {typ= {Typ.desc= Tarray (t, _, _)}}) | ( Sil.Hpointsto (e, Sil.Earray (e', l, _), Exp.Sizeof {typ= {Typ.desc= Tarray {elt= t}}})
, lambda ) -> , lambda ) ->
incr dotty_state_count ; incr dotty_state_count ;
(* increment once more n+1 is the box for the array *) (* increment once more n+1 is the box for the array *)

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

@ -482,7 +482,7 @@ let rec create_strexp_of_type ~path tenv struct_init_mode (typ: Typ.t) len inst
Estruct (flds, inst) Estruct (flds, inst)
| _ -> | _ ->
Estruct ([], inst) ) Estruct ([], inst) )
| Tarray (_, len_opt, _), None -> | Tarray {length= len_opt}, None ->
let len = let len =
match len_opt with None -> Exp.get_undefined false | Some len -> Exp.Const (Cint len) match len_opt with None -> Exp.get_undefined false | Some len -> Exp.Const (Cint len)
in in
@ -548,7 +548,7 @@ let exp_collapse_consecutive_indices_prop (typ: Typ.t) exp =
match typ1.desc with Tint _ | Tfloat _ | Tstruct _ | Tvoid | Tfun _ -> true | _ -> false match typ1.desc with Tint _ | Tfloat _ | Tstruct _ | Tvoid | Tfun _ -> true | _ -> false
in in
let typ_is_one_step_from_base = let typ_is_one_step_from_base =
match typ.desc with Tptr (t, _) | Tarray (t, _, _) -> typ_is_base t | _ -> false match typ.desc with Tptr (t, _) | Tarray {elt= t} -> typ_is_base t | _ -> false
in in
let rec exp_remove (e0: Exp.t) = let rec exp_remove (e0: Exp.t) =
match e0 with match e0 with
@ -674,10 +674,10 @@ module Normalize = struct
e e
| Sizeof {nbytes= Some n} when destructive -> | Sizeof {nbytes= Some n} when destructive ->
Exp.Const (Const.Cint (IntLit.of_int n)) Exp.Const (Const.Cint (IntLit.of_int n))
| Sizeof {typ= {desc= Tarray ({desc= Tint ik}, _, _)}; dynamic_length= Some l} | Sizeof {typ= {desc= Tarray {elt= {desc= Tint ik}}}; dynamic_length= Some l}
when Typ.ikind_is_char ik && Language.curr_language_is Clang -> when Typ.ikind_is_char ik && Language.curr_language_is Clang ->
eval l eval l
| Sizeof {typ= {desc= Tarray ({desc= Tint ik}, Some l, _)}} | Sizeof {typ= {desc= Tarray {elt= {desc= Tint ik}; length= Some l}}}
when Typ.ikind_is_char ik && Language.curr_language_is Clang -> when Typ.ikind_is_char ik && Language.curr_language_is Clang ->
Const (Cint l) Const (Cint l)
| Sizeof _ -> | Sizeof _ ->
@ -947,12 +947,12 @@ module Normalize = struct
Exp.int (IntLit.div n m) Exp.int (IntLit.div n m)
| Const Cfloat v, Const Cfloat w -> | Const Cfloat v, Const Cfloat w ->
Exp.float (v /. w) Exp.float (v /. w)
| ( Sizeof {typ= {desc= Tarray (elt, _, _)}; dynamic_length= Some len} | ( Sizeof {typ= {desc= Tarray {elt}}; dynamic_length= Some len}
, Sizeof {typ= elt2; dynamic_length= None} ) , Sizeof {typ= elt2; dynamic_length= None} )
(* pattern: sizeof(elt[len]) / sizeof(elt) = len *) (* pattern: sizeof(elt[len]) / sizeof(elt) = len *)
when Typ.equal elt elt2 -> when Typ.equal elt elt2 ->
len len
| ( Sizeof {typ= {desc= Tarray (elt, Some len, _)}; dynamic_length= None} | ( Sizeof {typ= {desc= Tarray {elt; length= Some len}}; dynamic_length= None}
, Sizeof {typ= elt2; dynamic_length= None} ) , Sizeof {typ= elt2; dynamic_length= None} )
(* pattern: sizeof(elt[len]) / sizeof(elt) = len *) (* pattern: sizeof(elt[len]) / sizeof(elt) = len *)
when Typ.equal elt elt2 -> when Typ.equal elt elt2 ->
@ -1450,20 +1450,20 @@ module Normalize = struct
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, 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 (Mult, x, len)); subtype}
@ -1471,7 +1471,7 @@ module Normalize = struct
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, 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 (Mult, x, len)); subtype}

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

@ -40,7 +40,7 @@ let rec is_java_class tenv (typ: Typ.t) =
match typ.desc with match typ.desc with
| Tstruct name -> | Tstruct name ->
Typ.Name.Java.is_class name Typ.Name.Java.is_class name
| Tarray (inner_typ, _, _) | Tptr (inner_typ, _) -> | Tarray {elt= inner_typ} | Tptr (inner_typ, _) ->
is_java_class tenv inner_typ is_java_class tenv inner_typ
| _ -> | _ ->
false false
@ -454,7 +454,7 @@ end = struct
in in
List.iter ~f:(fun (f, se) -> strexp_extract (se, get_field_type f)) fsel List.iter ~f:(fun (f, se) -> strexp_extract (se, get_field_type f)) fsel
| Sil.Earray (len, isel, _), t -> | Sil.Earray (len, isel, _), t ->
let elt_t = match t with Some {Typ.desc= Tarray (t, _, _)} -> Some t | _ -> None in let elt_t = match t with Some {Typ.desc= Tarray {elt}} -> Some elt | _ -> None in
add_lt_minus1_e len ; add_lt_minus1_e len ;
List.iter List.iter
~f:(fun (idx, se) -> ~f:(fun (idx, se) ->
@ -1559,7 +1559,7 @@ let rec sexp_imply tenv source calc_index_frame calc_missing subs se1 se2 typ2
sexp_imply tenv source calc_index_frame calc_missing subs se1' se2 typ2 sexp_imply tenv source calc_index_frame calc_missing subs se1' se2 typ2
| Sil.Earray (len, _, _), Sil.Eexp (_, inst) -> | Sil.Earray (len, _, _), Sil.Eexp (_, inst) ->
let se2' = Sil.Earray (len, [(Exp.zero, se2)], inst) in let se2' = Sil.Earray (len, [(Exp.zero, se2)], inst) in
let typ2' = Typ.mk (Tarray (typ2, None, None)) in let typ2' = Typ.mk_array typ2 in
(* In the sexp_imply, struct_imply, array_imply, and sexp_imply_nolhs functions, the typ2 (* In the sexp_imply, struct_imply, array_imply, and sexp_imply_nolhs functions, the typ2
argument is only used by eventually passing its value to Typ.Struct.fld, Exp.Lfield, argument is only used by eventually passing its value to Typ.Struct.fld, Exp.Lfield,
Typ.Struct.fld, or Typ.array_elem. None of these are sensitive to the length field Typ.Struct.fld, or Typ.array_elem. None of these are sensitive to the length field
@ -1801,7 +1801,7 @@ let expand_hpred_pointer =
let t' = let t' =
match t with match t with
| Exp.Sizeof ({typ= t_} as sizeof_data) -> | Exp.Sizeof ({typ= t_} as sizeof_data) ->
Exp.Sizeof {sizeof_data with typ= Typ.mk (Tarray (t_, None, None))} Exp.Sizeof {sizeof_data with typ= Typ.mk_array t_}
| _ -> | _ ->
L.(die InternalError) "expand_hpred_pointer: Unexpected non-sizeof type in Lindex" L.(die InternalError) "expand_hpred_pointer: Unexpected non-sizeof type in Lindex"
in in
@ -1847,7 +1847,7 @@ module Subtyping_check = struct
match (t1.Typ.desc, t2.Typ.desc) with match (t1.Typ.desc, t2.Typ.desc) with
| Tstruct (JavaClass _ as cn1), Tstruct (JavaClass _ as cn2) -> | Tstruct (JavaClass _ as cn1), Tstruct (JavaClass _ as cn2) ->
Subtype.is_known_subtype tenv cn1 cn2 Subtype.is_known_subtype tenv cn1 cn2
| Tarray (dom_type1, _, _), Tarray (dom_type2, _, _) -> | Tarray {elt= dom_type1}, Tarray {elt= dom_type2} ->
check_subtype_java tenv dom_type1 dom_type2 check_subtype_java tenv dom_type1 dom_type2
| Tptr (dom_type1, _), Tptr (dom_type2, _) -> | Tptr (dom_type1, _), Tptr (dom_type2, _) ->
check_subtype_java tenv dom_type1 dom_type2 check_subtype_java tenv dom_type1 dom_type2
@ -1887,7 +1887,7 @@ module Subtyping_check = struct
(* and the algorithm will only work correctly if this is the case *) (* and the algorithm will only work correctly if this is the case *)
when Subtype.is_known_subtype tenv cn1 cn2 || Subtype.is_known_subtype tenv cn2 cn1 -> when Subtype.is_known_subtype tenv cn1 cn2 || Subtype.is_known_subtype tenv cn2 cn1 ->
Subtype.case_analysis tenv (cn1, st1) (cn2, st2) Subtype.case_analysis tenv (cn1, st1) (cn2, st2)
| Tarray (dom_type1, _, _), Tarray (dom_type2, _, _) -> | Tarray {elt= dom_type1}, Tarray {elt= dom_type2} ->
case_analysis_type tenv (dom_type1, st1) (dom_type2, st2) case_analysis_type tenv (dom_type1, st1) (dom_type2, st2)
| Tptr (dom_type1, _), Tptr (dom_type2, _) -> | Tptr (dom_type1, _), Tptr (dom_type2, _) ->
case_analysis_type tenv (dom_type1, st1) (dom_type2, st2) case_analysis_type tenv (dom_type1, st1) (dom_type2, st2)
@ -2354,7 +2354,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : subst2 *
match !Language.curr_language with match !Language.curr_language with
| Clang -> | Clang ->
Exp.Sizeof Exp.Sizeof
{ typ= Typ.mk (Tarray (Typ.mk (Tint Typ.IChar), Some len, Some (IntLit.of_int 1))) { typ= Typ.mk_array (Typ.mk (Tint Typ.IChar)) ~length:len ~stride:(IntLit.of_int 1)
; nbytes= None ; nbytes= None
; dynamic_length= None ; dynamic_length= None
; subtype= Subtype.exact } ; subtype= Subtype.exact }

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

@ -136,12 +136,12 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
let e' = Sil.array_clean_new_index footprint_part e in let e' = Sil.array_clean_new_index footprint_part e in
let len = Exp.Var (new_id ()) in let len = Exp.Var (new_id ()) in
let se = Sil.Earray (len, [(e', se')], inst) in let se = Sil.Earray (len, [(e', se')], inst) in
let res_t = Typ.mk (Tarray (res_t', None, None)) in let res_t = Typ.mk_array res_t' in
(Sil.Aeq (e, e') :: atoms', se, res_t) (Sil.Aeq (e, e') :: atoms', se, res_t)
| Tarray (t', len_, stride_), off | Tarray {elt= t'; length; stride}, off
-> ( -> (
let len = let len =
match len_ with None -> Exp.Var (new_id ()) | Some len -> Exp.Const (Const.Cint len) match length with None -> Exp.Var (new_id ()) | Some len -> Exp.Const (Const.Cint len)
in in
match off with match off with
| [] -> | [] ->
@ -153,7 +153,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
in in
let e' = Sil.array_clean_new_index footprint_part e in let e' = Sil.array_clean_new_index footprint_part e in
let se = Sil.Earray (len, [(e', se')], inst) in let se = Sil.Earray (len, [(e', se')], inst) in
let res_t = Typ.mk ~default:t (Tarray (res_t', len_, stride_)) in let res_t = Typ.mk_array ~default:t res_t' ?length ?stride in
(Sil.Aeq (e, e') :: atoms', se, res_t) (Sil.Aeq (e, e') :: atoms', se, res_t)
| (Sil.Off_fld _) :: _ -> | (Sil.Off_fld _) :: _ ->
assert false ) assert false )
@ -176,7 +176,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
in in
let e' = Sil.array_clean_new_index footprint_part e in let e' = Sil.array_clean_new_index footprint_part e in
let se = Sil.Earray (len, [(e', se')], inst) in let se = Sil.Earray (len, [(e', se')], inst) in
let res_t = mk_typ_f (Tarray (res_t', None, None)) in let res_t = mk_typ_f (Tarray {elt= res_t'; length= None; stride= None}) in
(Sil.Aeq (e, e') :: atoms', se, res_t) (Sil.Aeq (e, e') :: atoms', se, res_t)
| Tint _, _ | Tfloat _, _ | Tvoid, _ | Tfun _, _ | Tptr _, _ | TVar _, _ -> | Tint _, _ | Tfloat _, _ | Tvoid, _ | Tfun _, _ | Tptr _, _ | TVar _, _ ->
fail t off __POS__ fail t off __POS__
@ -275,10 +275,12 @@ let rec strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp
else Exp.Var (new_id ()) else Exp.Var (new_id ())
in in
let se_new = Sil.Earray (len, [(Exp.zero, se)], inst) in let se_new = Sil.Earray (len, [(Exp.zero, se)], inst) in
let typ_new = Typ.mk (Tarray (typ, None, None)) in let typ_new = Typ.mk_array typ in
strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp se_new typ_new off strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp se_new typ_new off
inst inst
| (Off_index e) :: off', Sil.Earray (len, esel, inst_arr), Tarray (typ', len_for_typ', stride) | ( (Off_index e) :: off'
, Sil.Earray (len, esel, inst_arr)
, Tarray {elt= typ'; length= len_for_typ'; stride} )
-> ( -> (
bounds_check tenv pname orig_prop len e (State.get_loc ()) ; bounds_check tenv pname orig_prop len e (State.get_loc ()) ;
match List.find ~f:(fun (e', _) -> Exp.equal e e') esel with match List.find ~f:(fun (e', _) -> Exp.equal e e') esel with
@ -293,7 +295,7 @@ let rec strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp
if Typ.equal res_typ' typ' || Int.equal (List.length res_esel') 1 then if Typ.equal res_typ' typ' || Int.equal (List.length res_esel') 1 then
( res_atoms' ( res_atoms'
, Sil.Earray (len, res_esel', inst_arr) , Sil.Earray (len, res_esel', inst_arr)
, Typ.mk ~default:typ (Tarray (res_typ', len_for_typ', stride)) ) , Typ.mk_array ~default:typ res_typ' ?length:len_for_typ' ?stride )
:: acc :: acc
else raise (Exceptions.Bad_footprint __POS__) else raise (Exceptions.Bad_footprint __POS__)
in in
@ -323,7 +325,7 @@ and array_case_analysis_index pname tenv orig_prop footprint_part kind max_stamp
in in
if index_in_array then if index_in_array then
let array_default = Sil.Earray (array_len, array_cont, inst_arr) in let array_default = Sil.Earray (array_len, array_cont, inst_arr) in
let typ_default = Typ.mk ~default:typ_array (Tarray (typ_cont, typ_array_len, None)) in let typ_default = Typ.mk_array ~default:typ_array typ_cont ?length:typ_array_len in
[([], array_default, typ_default)] [([], array_default, typ_default)]
else if !Config.footprint then else if !Config.footprint then
let atoms, elem_se, elem_typ = let atoms, elem_se, elem_typ =
@ -334,7 +336,7 @@ and array_case_analysis_index pname tenv orig_prop footprint_part kind max_stamp
List.sort ~cmp:[%compare : Exp.t * Sil.strexp] ((index, elem_se) :: array_cont) List.sort ~cmp:[%compare : Exp.t * Sil.strexp] ((index, elem_se) :: array_cont)
in in
let array_new = Sil.Earray (array_len, cont_new, inst_arr) in let array_new = Sil.Earray (array_len, cont_new, inst_arr) in
let typ_new = Typ.mk ~default:typ_array (Tarray (elem_typ, typ_array_len, None)) in let typ_new = Typ.mk_array ~default:typ_array elem_typ ?length:typ_array_len in
[(atoms, array_new, typ_new)] [(atoms, array_new, typ_new)]
else else
let res_new = let res_new =
@ -348,7 +350,7 @@ and array_case_analysis_index pname tenv orig_prop footprint_part kind max_stamp
List.sort ~cmp:[%compare : Exp.t * Sil.strexp] ((index, elem_se) :: array_cont) List.sort ~cmp:[%compare : Exp.t * Sil.strexp] ((index, elem_se) :: array_cont)
in in
let array_new = Sil.Earray (array_len, cont_new, inst_arr) in let array_new = Sil.Earray (array_len, cont_new, inst_arr) in
let typ_new = Typ.mk ~default:typ_array (Tarray (elem_typ, typ_array_len, None)) in let typ_new = Typ.mk_array ~default:typ_array elem_typ ?length:typ_array_len in
[(atoms, array_new, typ_new)] [(atoms, array_new, typ_new)]
in in
let rec handle_case acc isel_seen_rev = function let rec handle_case acc isel_seen_rev = function
@ -366,7 +368,7 @@ and array_case_analysis_index pname tenv orig_prop footprint_part kind max_stamp
let atoms_new = Sil.Aeq (index, i) :: atoms' in let atoms_new = Sil.Aeq (index, i) :: atoms' in
let isel_new = list_rev_and_concat isel_seen_rev ((i, se') :: isel_unseen) in let isel_new = list_rev_and_concat isel_seen_rev ((i, se') :: isel_unseen) in
let array_new = Sil.Earray (array_len, isel_new, inst_arr) in let array_new = Sil.Earray (array_len, isel_new, inst_arr) in
let typ_new = Typ.mk ~default:typ_array (Tarray (typ', typ_array_len, None)) in let typ_new = Typ.mk_array ~default:typ_array typ' ?length:typ_array_len in
(atoms_new, array_new, typ_new) :: acc' ) (atoms_new, array_new, typ_new) :: acc' )
~init:[] atoms_se_typ_list ~init:[] atoms_se_typ_list
in in
@ -1324,7 +1326,7 @@ let type_at_offset tenv texp off =
None ) None )
| None -> | None ->
None ) None )
| (Off_index _) :: off', Tarray (typ', _, _) -> | (Off_index _) :: off', Tarray {elt= typ'} ->
strip_offset off' typ' strip_offset off' typ'
| _ -> | _ ->
None None
@ -1390,7 +1392,7 @@ let rec iter_rearrange pname tenv lexp typ_from_instr prop iter inst
| _ -> | _ ->
typ_from_instr ) typ_from_instr )
| (Sil.Off_index _) :: off -> | (Sil.Off_index _) :: off ->
Typ.mk (Tarray (root_typ_of_offsets off, None, None)) Typ.mk_array (root_typ_of_offsets off)
| _ -> | _ ->
typ_from_instr typ_from_instr
in in

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

@ -40,8 +40,8 @@ let unroll_type tenv (typ: Typ.t) (off: Sil.offset) =
try fldlist_assoc fld (fields @ statics) with Not_found -> fail Typ.Fieldname.to_string fld ) try fldlist_assoc fld (fields @ statics) with Not_found -> fail Typ.Fieldname.to_string fld )
| None -> | None ->
fail Typ.Fieldname.to_string fld ) fail Typ.Fieldname.to_string fld )
| Tarray (typ', _, _), Off_index _ -> | Tarray {elt}, Off_index _ ->
typ' elt
| _, Off_index Const Cint i when IntLit.iszero i -> | _, Off_index Const Cint i when IntLit.iszero i ->
typ typ
| _ -> | _ ->
@ -141,7 +141,9 @@ let rec apply_offlist pdesc tenv p fp_root nullify_struct (root_lexp, strexp, ty
| (Sil.Off_fld _) :: _, _, _ -> | (Sil.Off_fld _) :: _, _, _ ->
pp_error () ; pp_error () ;
assert false assert false
| (Sil.Off_index idx) :: offlist', Sil.Earray (len, esel, inst1), Typ.Tarray (t', len', stride') | ( (Sil.Off_index idx) :: offlist'
, Sil.Earray (len, esel, inst1)
, Typ.Tarray {elt= t'; length= len'; stride= stride'} )
-> ( -> (
let nidx = Prop.exp_normalize_prop tenv p idx in let nidx = Prop.exp_normalize_prop tenv p idx in
match List.find ~f:(fun ese -> Prover.check_equal tenv p nidx (fst ese)) esel with match List.find ~f:(fun ese -> Prover.check_equal tenv p nidx (fst ese)) esel with
@ -154,7 +156,7 @@ let rec apply_offlist pdesc tenv p fp_root nullify_struct (root_lexp, strexp, ty
if Exp.equal idx_ese' (fst ese) then (idx_ese', res_se') else ese if Exp.equal idx_ese' (fst ese) then (idx_ese', res_se') else ese
in in
let res_se = Sil.Earray (len, List.map ~f:replace_ese esel, inst1) in let res_se = Sil.Earray (len, List.map ~f:replace_ese esel, inst1) in
let res_t = Typ.mk ~default:typ (Tarray (res_t', len', stride')) in let res_t = Typ.mk_array ~default:typ res_t' ?length:len' ?stride:stride' in
(res_e', res_se, res_t, res_pred_insts_op') (res_e', res_se, res_t, res_pred_insts_op')
| None -> | None ->
(* return a nondeterministic value if the index is not found after rearrangement *) (* return a nondeterministic value if the index is not found after rearrangement *)

14
infer/src/bufferoverrun/bufferOverrunChecker.ml
Unescape View File

@ -66,18 +66,18 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
BoUtils.Exec.decl_sym_arr BoUtils.Exec.decl_sym_arr
~decl_sym_val:(decl_sym_val ~is_last_field:false) ~decl_sym_val:(decl_sym_val ~is_last_field:false)
pname tenv node location ~depth loc typ ~inst_num ~new_sym_num ~new_alloc_num mem pname tenv node location ~depth loc typ ~inst_num ~new_sym_num ~new_alloc_num mem
| Typ.Tarray (typ, opt_int_lit, _) -> | Typ.Tarray {elt; length} ->
let size = let size =
match opt_int_lit with match length with
| Some int_lit when is_last_field && (IntLit.iszero int_lit || IntLit.isone int_lit) -> | Some length when is_last_field && (IntLit.iszero length || IntLit.isone length) ->
Some (Itv.make_sym pname new_sym_num) Some (Itv.make_sym pname new_sym_num)
| _ -> | _ ->
Option.map ~f:Itv.of_int_lit opt_int_lit Option.map ~f:Itv.of_int_lit length
in in
let offset = Itv.zero in let offset = Itv.zero in
BoUtils.Exec.decl_sym_arr BoUtils.Exec.decl_sym_arr
~decl_sym_val:(decl_sym_val ~is_last_field:false) ~decl_sym_val:(decl_sym_val ~is_last_field:false)
pname tenv node location ~depth loc typ ~offset ?size ~inst_num ~new_sym_num pname tenv node location ~depth loc elt ~offset ?size ~inst_num ~new_sym_num
~new_alloc_num mem ~new_alloc_num mem
| Typ.Tstruct typename -> ( | Typ.Tstruct typename -> (
match Models.TypName.dispatch typename with match Models.TypName.dispatch typename with
@ -257,8 +257,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
(* array allocation in stack e.g., int arr[10] *) (* array allocation in stack e.g., int arr[10] *)
let rec decl_local pname node location loc typ ~inst_num ~dimension mem = let rec decl_local pname node location loc typ ~inst_num ~dimension mem =
match typ.Typ.desc with match typ.Typ.desc with
| Typ.Tarray (typ, length, stride0) -> | Typ.Tarray {elt= typ; length; stride} ->
let stride = Option.map ~f:IntLit.to_int stride0 in let stride = Option.map ~f:IntLit.to_int stride in
BoUtils.Exec.decl_local_array ~decl_local pname node location loc typ ~length BoUtils.Exec.decl_local_array ~decl_local pname node location loc typ ~length
?stride ~inst_num ~dimension mem ?stride ~inst_num ~dimension mem
| Typ.Tstruct typname -> ( | Typ.Tstruct typname -> (

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

@ -177,12 +177,12 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct
let set_array_length array length_exp = let set_array_length array length_exp =
let exec {pname; node} mem = let exec {pname; node} mem =
match array with match array with
| Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray (typ, _, stride0)} -> | Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray {elt; stride}} ->
let length = Sem.eval length_exp mem |> Dom.Val.get_itv in let length = Sem.eval length_exp mem |> Dom.Val.get_itv in
let stride = Option.map ~f:IntLit.to_int stride0 in let stride = Option.map ~f:IntLit.to_int stride in
let v = Sem.eval_array_alloc pname node typ ?stride Itv.zero length 0 1 in let v = Sem.eval_array_alloc pname node elt ?stride Itv.zero length 0 1 in
mem |> Dom.Mem.add_stack (Loc.of_pvar array_pvar) v mem |> Dom.Mem.add_stack (Loc.of_pvar array_pvar) v
|> set_uninitialized node typ (Dom.Val.get_array_locs v) |> set_uninitialized node elt (Dom.Val.get_array_locs v)
| _ -> | _ ->
L.(die InternalError) "Unexpected type of first argument for __set_array_length()" L.(die InternalError) "Unexpected type of first argument for __set_array_length()"
and check = check_alloc_size length_exp in and check = check_alloc_size length_exp in

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

@ -68,10 +68,10 @@ module Make (CFG : ProcCfg.S) = struct
4 4
| Typ.Tstruct _ | Typ.TVar _ -> | Typ.Tstruct _ | Typ.TVar _ ->
4 (* TODO *) 4 (* TODO *)
| Typ.Tarray (_, Some length, Some stride) -> | Typ.Tarray {length= Some length; stride= Some stride} ->
IntLit.to_int stride * IntLit.to_int length IntLit.to_int stride * IntLit.to_int length
| Typ.Tarray (typ, Some length, None) -> | Typ.Tarray {elt; length= Some length; stride= None} ->
sizeof typ * IntLit.to_int length sizeof elt * IntLit.to_int length
| _ -> | _ ->
4 4

2
infer/src/bufferoverrun/bufferOverrunUtils.ml
Unescape View File

@ -136,7 +136,7 @@ module Make (CFG : ProcCfg.S) = struct
let field_loc = PowLoc.append_field locs ~fn:field_name in let field_loc = PowLoc.append_field locs ~fn:field_name in
let mem = let mem =
match field_typ.Typ.desc with match field_typ.Typ.desc with
| Tarray (typ, Some length, stride) -> | Tarray {elt= typ; length= Some length; stride} ->
let length = Itv.of_int_lit length in let length = Itv.of_int_lit length in
let length = let length =
Option.value_map dyn_length ~default:length ~f:(fun dyn_length -> Option.value_map dyn_length ~default:length ~f:(fun dyn_length ->

4
infer/src/checkers/uninit.ml
Unescape View File

@ -296,8 +296,8 @@ let get_locals cfg tenv pdesc =
to the fields one level down *) to the fields one level down *)
| _ -> | _ ->
acc ) acc )
| Typ.Tarray (t', _, _) -> | Typ.Tarray {elt} ->
(fst base_ap, [AccessPath.ArrayAccess (t', [])]) :: acc (fst base_ap, [AccessPath.ArrayAccess (elt, [])]) :: acc
| _ -> | _ ->
base_ap :: acc ) base_ap :: acc )
~init:[] (Procdesc.get_locals cfg) ~init:[] (Procdesc.get_locals cfg)

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

@ -403,7 +403,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
assert false assert false
in in
List.map ~f:fill_typ_with_zero field_exps |> flatten_res_trans List.map ~f:fill_typ_with_zero field_exps |> flatten_res_trans
| Tarray (field_typ, Some n, _) -> | Tarray {elt= field_typ; length= Some n} ->
let size = IntLit.to_int n in let size = IntLit.to_int n in
let indices = CGeneral_utils.list_range 0 (size - 1) in let indices = CGeneral_utils.list_range 0 (size - 1) in
List.map indices ~f:(fun i -> List.map indices ~f:(fun i ->
@ -2142,8 +2142,8 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
in in
let all_res_trans = let all_res_trans =
match var_typ.Typ.desc with match var_typ.Typ.desc with
| Typ.Tarray (typ_inside, _, _) -> | Typ.Tarray {elt} ->
initListExpr_array_trans trans_state_pri init_stmt_info stmts var_exp typ_inside initListExpr_array_trans trans_state_pri init_stmt_info stmts var_exp elt
| Tstruct _ -> | Tstruct _ ->
initListExpr_struct_trans trans_state_pri init_stmt_info stmts var_exp var_typ initListExpr_struct_trans trans_state_pri init_stmt_info stmts var_exp var_typ
| Tint _ | Tfloat _ | Tptr _ -> | Tint _ | Tfloat _ | Tptr _ ->
@ -2740,7 +2740,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
match res_trans_new.exps with match res_trans_new.exps with
| [(var_exp, ({desc= Tptr (t, _)} as var_typ))] when is_dyn_array -> | [(var_exp, ({desc= Tptr (t, _)} as var_typ))] when is_dyn_array ->
(* represent dynamic array as Tarray *) (* represent dynamic array as Tarray *)
(var_exp, Typ.mk ~default:var_typ (Typ.Tarray (t, None, None))) (var_exp, Typ.mk_array ~default:var_typ t)
| [(var_exp, {desc= Tptr (t, _)})] when not is_dyn_array -> | [(var_exp, {desc= Tptr (t, _)})] when not is_dyn_array ->
(var_exp, t) (var_exp, t)
| _ -> | _ ->

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

@ -92,7 +92,7 @@ let rec build_array_type translate_decl tenv (qual_type: Clang_ast_t.qual_type)
let array_type = qual_type_to_sil_type translate_decl tenv qual_type in let array_type = qual_type_to_sil_type translate_decl tenv qual_type in
let length = Option.map ~f:IntLit.of_int length_opt in let length = Option.map ~f:IntLit.of_int length_opt in
let stride = Option.map ~f:IntLit.of_int stride_opt in let stride = Option.map ~f:IntLit.of_int stride_opt in
Typ.Tarray (array_type, length, stride) Typ.Tarray {elt= array_type; length; stride}
and type_desc_of_attr_type translate_decl tenv type_info attr_info = and type_desc_of_attr_type translate_decl tenv type_info attr_info =
match type_info.Clang_ast_t.ti_desugared_type with match type_info.Clang_ast_t.ti_desugared_type with

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

@ -545,7 +545,7 @@ let rec expression (context: JContext.t) pc expr =
match binop with match binop with
| JBir.ArrayLoad _ -> | JBir.ArrayLoad _ ->
(* add an instruction that dereferences the array *) (* add an instruction that dereferences the array *)
let array_typ = Typ.mk (Tarray (type_of_expr, None, None)) in let array_typ = Typ.mk_array type_of_expr in
let deref_array_instr = create_sil_deref sil_ex1 array_typ loc in let deref_array_instr = create_sil_deref sil_ex1 array_typ loc in
let id = Ident.create_fresh Ident.knormal in let id = Ident.create_fresh Ident.knormal in
let load_instr = Sil.Load (id, Exp.Lindex (sil_ex1, sil_ex2), type_of_expr, loc) in let load_instr = Sil.Load (id, Exp.Lindex (sil_ex1, sil_ex2), type_of_expr, loc) in
@ -739,7 +739,7 @@ let get_array_length context pc expr_list content_type =
in in
let instrs, sil_len_exprs = List.fold_right ~f:get_expr_instr expr_list ~init:([], []) in let instrs, sil_len_exprs = List.fold_right ~f:get_expr_instr expr_list ~init:([], []) in
let get_array_type_len sil_len_expr (content_type, _) = let get_array_type_len sil_len_expr (content_type, _) =
(Typ.mk (Tarray (content_type, None, None)), Some sil_len_expr) (Typ.mk_array content_type, Some sil_len_expr)
in in
let array_type, array_len = let array_type, array_len =
List.fold_right ~f:get_array_type_len sil_len_exprs ~init:(content_type, None) List.fold_right ~f:get_array_type_len sil_len_exprs ~init:(content_type, None)

12
infer/src/java/jTransType.ml
Unescape View File

@ -81,7 +81,7 @@ let rec get_named_type vt : Typ.t =
match ot with match ot with
| JBasics.TArray vt -> | JBasics.TArray vt ->
let content_type = get_named_type vt in let content_type = get_named_type vt in
Typ.mk (Tptr (Typ.mk (Tarray (content_type, None, None)), Typ.Pk_pointer)) Typ.mk (Tptr (Typ.mk_array content_type, Typ.Pk_pointer))
| JBasics.TClass cn -> | JBasics.TClass cn ->
Typ.mk (Tptr (Typ.mk (Tstruct (typename_of_classname cn)), Typ.Pk_pointer)) Typ.mk (Tptr (Typ.mk (Tstruct (typename_of_classname cn)), Typ.Pk_pointer))
@ -89,7 +89,7 @@ let rec get_named_type vt : Typ.t =
let rec create_array_type typ dim = let rec create_array_type typ dim =
if dim > 0 then if dim > 0 then
let content_typ = create_array_type typ (dim - 1) in let content_typ = create_array_type typ (dim - 1) in
Typ.mk (Tptr (Typ.mk (Tarray (content_typ, None, None)), Typ.Pk_pointer)) Typ.mk (Tptr (Typ.mk_array content_typ, Typ.Pk_pointer))
else typ else typ
@ -412,7 +412,7 @@ let rec object_type program tenv ot =
| JBasics.TClass cn -> | JBasics.TClass cn ->
get_class_type program tenv cn get_class_type program tenv cn
| JBasics.TArray at -> | JBasics.TArray at ->
Typ.mk (Tptr (Typ.mk (Tarray (value_type program tenv at, None, None)), Typ.Pk_pointer)) Typ.mk (Tptr (Typ.mk_array (value_type program tenv at), Typ.Pk_pointer))
(** translate a value type *) (** translate a value type *)
@ -456,11 +456,7 @@ let get_var_type context var =
let extract_array_type typ = let extract_array_type typ =
match typ.Typ.desc with match typ.Typ.desc with Typ.Tptr ({desc= Tarray {elt}}, Typ.Pk_pointer) -> elt | _ -> typ
| Typ.Tptr ({desc= Tarray (vtyp, _, _)}, Typ.Pk_pointer) ->
vtyp
| _ ->
typ
(** translate the type of an expression, looking in the method signature for formal parameters (** translate the type of an expression, looking in the method signature for formal parameters

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

@ -21,7 +21,7 @@ let tests =
let yF = make_access_path "y" ["f"] in let yF = make_access_path "y" ["f"] in
let xArr = let xArr =
let dummy_typ = Typ.mk Tvoid in let dummy_typ = Typ.mk Tvoid in
let dummy_arr_typ = Typ.mk (Tarray (dummy_typ, None, None)) in let dummy_arr_typ = Typ.mk_array dummy_typ in
let base = make_base "x" ~typ:dummy_arr_typ in let base = make_base "x" ~typ:dummy_arr_typ in
(base, [make_array_access dummy_typ]) (base, [make_array_access dummy_typ])
in in

Write Preview
Loading…
Cancel
Save