[IR] add type qualifiers to Typ.t

Reviewed By: jberdine, jvillard

Differential Revision: D4867359

fbshipit-source-id: eef5be0
master
Andrzej Kotulski 8 years ago committed by Facebook Github Bot
parent 5de8161f89
commit 029499cd9d

@ -201,7 +201,7 @@ let get_correct_type_from_objc_class_name type_name =>
switch (find_tenv_from_class_of_proc class_method) { switch (find_tenv_from_class_of_proc class_method) {
| Some tenv => | Some tenv =>
*/ */
Some (Typ.Tstruct type_name); Some (Typ.mk (Tstruct type_name));
type t = { type t = {
num_bindings: int, num_bindings: int,

@ -350,7 +350,7 @@ let specialize_types_proc callee_pdesc resolved_pdesc substitutions => {
let convert_pvar pvar => Pvar.mk (Pvar.get_name pvar) resolved_pname; let convert_pvar pvar => Pvar.mk (Pvar.get_name pvar) resolved_pname;
let mk_ptr_typ typename => let mk_ptr_typ typename =>
/* Only consider pointers from Java objects for now */ /* Only consider pointers from Java objects for now */
Typ.Tptr (Typ.Tstruct typename) Typ.Pk_pointer; Typ.mk (Tptr (Typ.mk (Tstruct typename)) Typ.Pk_pointer);
let convert_exp = let convert_exp =
fun fun
| Exp.Lvar origin_pvar => Exp.Lvar (convert_pvar origin_pvar) | Exp.Lvar origin_pvar => Exp.Lvar (convert_pvar origin_pvar)
@ -363,7 +363,10 @@ let specialize_types_proc callee_pdesc resolved_pdesc substitutions => {
let convert_instr instrs => let convert_instr instrs =>
fun fun
| Sil.Load | Sil.Load
id (Exp.Lvar origin_pvar as origin_exp) (Typ.Tptr (Tstruct origin_typename) Pk_pointer) loc => { id
(Exp.Lvar origin_pvar as origin_exp)
{Typ.desc: Tptr {desc: Tstruct origin_typename} Pk_pointer}
loc => {
let specialized_typname = let specialized_typname =
try (Mangled.Map.find (Pvar.get_name origin_pvar) substitutions) { try (Mangled.Map.find (Pvar.get_name origin_pvar) substitutions) {
| Not_found => origin_typename | Not_found => origin_typename
@ -371,9 +374,9 @@ let specialize_types_proc callee_pdesc resolved_pdesc substitutions => {
subst_map := Ident.IdentMap.add id specialized_typname !subst_map; subst_map := Ident.IdentMap.add id specialized_typname !subst_map;
[Sil.Load id (convert_exp origin_exp) (mk_ptr_typ specialized_typname) loc, ...instrs] [Sil.Load id (convert_exp origin_exp) (mk_ptr_typ specialized_typname) loc, ...instrs]
} }
| Sil.Load id (Exp.Var origin_id as origin_exp) (Typ.Tstruct _ as origin_typ) loc => { | Sil.Load id (Exp.Var origin_id as origin_exp) ({Typ.desc: Tstruct _} as origin_typ) loc => {
let updated_typ = let updated_typ: Typ.t =
try (Typ.Tstruct (Ident.IdentMap.find origin_id !subst_map)) { try (Typ.mk default::origin_typ (Tstruct (Ident.IdentMap.find origin_id !subst_map))) {
| Not_found => origin_typ | Not_found => origin_typ
}; };
[Sil.Load id (convert_exp origin_exp) updated_typ loc, ...instrs] [Sil.Load id (convert_exp origin_exp) updated_typ loc, ...instrs]
@ -474,8 +477,8 @@ let specialize_types callee_pdesc resolved_pname args => {
List.fold2_exn List.fold2_exn
f::( f::(
fun (params, subts) (param_name, param_typ) (_, arg_typ) => fun (params, subts) (param_name, param_typ) (_, arg_typ) =>
switch arg_typ { switch arg_typ.Typ.desc {
| Typ.Tptr (Tstruct typename) Pk_pointer => | Tptr {desc: Tstruct typename} Pk_pointer =>
/* Replace the type of the parameter by the type of the argument */ /* Replace the type of the parameter by the type of the argument */
([(param_name, arg_typ), ...params], Mangled.Map.add param_name typename subts) ([(param_name, arg_typ), ...params], Mangled.Map.add param_name typename subts)
| _ => ([(param_name, param_typ), ...params], subts) | _ => ([(param_name, param_typ), ...params], subts)

@ -73,14 +73,14 @@ let of_sil ~f_resolve_id (instr : Sil.instr) =
| Call (ret_opt, call_exp, formals, loc, call_flags) -> | Call (ret_opt, call_exp, formals, loc, call_flags) ->
let hil_ret = Option.map ~f:(fun (ret_id, ret_typ) -> Var.of_id ret_id, ret_typ) ret_opt in let hil_ret = Option.map ~f:(fun (ret_id, ret_typ) -> Var.of_id ret_id, ret_typ) ret_opt in
let hil_call = let hil_call =
match HilExp.of_sil ~f_resolve_id call_exp Typ.Tvoid with match HilExp.of_sil ~f_resolve_id call_exp (Typ.mk Tvoid) with
| Constant (Cfun procname) -> Direct procname | Constant (Cfun procname) -> Direct procname
| AccessPath access_path -> Indirect access_path | AccessPath access_path -> Indirect access_path
| call_exp -> invalid_argf "Unexpected call expression %a" HilExp.pp call_exp in | call_exp -> invalid_argf "Unexpected call expression %a" HilExp.pp call_exp in
let formals = List.map ~f:(fun (exp, typ) -> HilExp.of_sil ~f_resolve_id exp typ) formals in let formals = List.map ~f:(fun (exp, typ) -> HilExp.of_sil ~f_resolve_id exp typ) formals in
Instr (Call (hil_ret, hil_call, formals, call_flags, loc)) Instr (Call (hil_ret, hil_call, formals, call_flags, loc))
| Prune (exp, loc, true_branch, if_kind) -> | Prune (exp, loc, true_branch, if_kind) ->
let hil_exp = HilExp.of_sil ~f_resolve_id exp (Typ.Tint Typ.IBool) in let hil_exp = HilExp.of_sil ~f_resolve_id exp (Typ.mk (Tint IBool)) in
let branch = if true_branch then `Then else `Else in let branch = if true_branch then `Then else `Else in
Instr (Assume (hil_exp, branch, if_kind, loc)) Instr (Assume (hil_exp, branch, if_kind, loc))
| Nullify _ | Remove_temps _ | Nullify _ | Remove_temps _

@ -309,12 +309,12 @@ let add_by_call_to_opt problem_str tags proc_name_opt =
problem_str ^ " " ^ by_call_to tags proc_name problem_str ^ " " ^ by_call_to tags proc_name
| None -> problem_str | None -> problem_str
let rec format_typ = function let rec format_typ typ = match typ.Typ.desc with
| Typ.Tptr (typ, _) when Config.curr_language_is Config.Java -> | Typ.Tptr (t, _) when Config.curr_language_is Config.Java ->
format_typ typ format_typ t
| Typ.Tstruct name -> | Typ.Tstruct name ->
Typ.Name.name name Typ.Name.name name
| typ -> | _ ->
Typ.to_string typ Typ.to_string typ
let format_field f = let format_field f =
@ -771,7 +771,7 @@ let desc_leak hpred_type_opt value_str_opt resource_opt resource_action_opt loc
MF.monospaced_to_string s, " to ", " on " in MF.monospaced_to_string s, " to ", " on " in
let typ_str = let typ_str =
match hpred_type_opt with match hpred_type_opt with
| Some (Exp.Sizeof (Tstruct name, _, _)) when Typ.Name.is_class name -> | Some (Exp.Sizeof ({desc=Tstruct name}, _, _)) when Typ.Name.is_class name ->
" of type " ^ MF.monospaced_to_string (Typ.Name.name name) ^ " " " of type " ^ MF.monospaced_to_string (Typ.Name.name name) ^ " "
| _ -> " " in | _ -> " " in
let desc_str = let desc_str =

@ -205,7 +205,7 @@ struct
List.mem ~equal:String.equal core_graphics_types o List.mem ~equal:String.equal core_graphics_types o
let rec is_core_lib lib typ = let rec is_core_lib lib typ =
match typ with match typ.Typ.desc with
| Typ.Tptr (styp, _ ) -> | Typ.Tptr (styp, _ ) ->
is_core_lib lib styp is_core_lib lib styp
| Typ.Tstruct name -> | Typ.Tstruct name ->

@ -99,6 +99,6 @@ let default proc_name language => {
objc_accessor: None, objc_accessor: None,
proc_flags: proc_flags_empty (), proc_flags: proc_flags_empty (),
proc_name, proc_name,
ret_type: Typ.Tvoid, ret_type: Typ.mk Typ.Tvoid,
source_file_captured: SourceFile.invalid source_file_captured: SourceFile.invalid
}; };

@ -229,7 +229,7 @@ let hpred_get_lhs h =>
/** {2 Comparision and Inspection Functions} */ /** {2 Comparision and Inspection Functions} */
let has_objc_ref_counter tenv hpred => let has_objc_ref_counter tenv hpred =>
switch hpred { switch hpred {
| Hpointsto _ _ (Sizeof (Tstruct name) _ _) => | Hpointsto _ _ (Sizeof {desc: Tstruct name} _ _) =>
switch (Tenv.lookup tenv name) { switch (Tenv.lookup tenv name) {
| Some {fields} => List.exists f::Typ.Struct.is_objc_ref_counter_field fields | Some {fields} => List.exists f::Typ.Struct.is_objc_ref_counter_field fields
| _ => false | _ => false
@ -240,7 +240,7 @@ let has_objc_ref_counter tenv hpred =>
/** Returns the zero value of a type, for int, float and ptr types, None othwewise */ /** Returns the zero value of a type, for int, float and ptr types, None othwewise */
let zero_value_of_numerical_type_option typ => let zero_value_of_numerical_type_option typ =>
switch typ { switch typ.Typ.desc {
| Typ.Tint _ => Some (Exp.Const (Cint IntLit.zero)) | Typ.Tint _ => Some (Exp.Const (Cint IntLit.zero))
| Typ.Tfloat _ => Some (Exp.Const (Cfloat 0.0)) | Typ.Tfloat _ => Some (Exp.Const (Cfloat 0.0))
| Typ.Tptr _ => Some (Exp.Const (Cint IntLit.null)) | Typ.Tptr _ => Some (Exp.Const (Cint IntLit.null))

@ -123,9 +123,11 @@ let ptr_kind_string =
type static_length = option IntLit.t [@@deriving compare]; type static_length = option IntLit.t [@@deriving compare];
module T = { module T = {
type type_quals = {is_const: bool, is_volatile: bool} [@@deriving compare];
/** types for sil (structured) expressions */ /** types for sil (structured) expressions */
type t = type t = {desc, quals: type_quals} [@@deriving compare]
and desc =
| Tint ikind /** integer type */ | Tint ikind /** integer type */
| Tfloat fkind /** float type */ | Tfloat fkind /** float type */
| Tvoid /** void type */ | Tvoid /** void type */
@ -146,12 +148,33 @@ module T = {
| NoTemplate | NoTemplate
| Template (QualifiedCppName.t, list (option t)) | Template (QualifiedCppName.t, list (option t))
[@@deriving compare]; [@@deriving compare];
let equal_desc = [%compare.equal : desc];
let equal_quals = [%compare.equal : type_quals];
let equal = [%compare.equal : t]; let equal = [%compare.equal : t];
let hash = Hashtbl.hash; let hash = Hashtbl.hash;
}; };
include T; include T;
let mk_type_quals ::default=? ::is_const=? ::is_volatile=? () => {
let default_ = {is_const: false, is_volatile: false};
let mk_aux ::default=default_ ::is_const=default.is_const ::is_volatile=default.is_volatile () => {
is_const,
is_volatile
};
mk_aux ::?default ::?is_const ::?is_volatile ()
};
let is_const {is_const} => is_const;
let is_volatile {is_volatile} => is_volatile;
let mk ::default=? ::quals=? desc :t => {
let default_ = {desc, quals: mk_type_quals ()};
let mk_aux ::default=default_ ::quals=default.quals desc => {desc, quals};
mk_aux ::?default ::?quals desc
};
module Name = { module Name = {
type t = name [@@deriving compare]; type t = name [@@deriving compare];
let equal = [%compare.equal : t]; let equal = [%compare.equal : t];
@ -253,8 +276,8 @@ module Tbl = Hashtbl.Make T;
/** Pretty print a type with all the details, using the C syntax. */ /** Pretty print a type with all the details, using the C syntax. */
let rec pp_full pe f => let rec pp_full pe f {desc} =>
fun switch desc {
| Tstruct tname => | Tstruct tname =>
if (Pp.equal_print_kind pe.Pp.kind Pp.HTML) { if (Pp.equal_print_kind pe.Pp.kind Pp.HTML) {
F.fprintf f "%s" (Name.name tname |> Escape.escape_xml) F.fprintf f "%s" (Name.name tname |> Escape.escape_xml)
@ -266,17 +289,17 @@ let rec pp_full pe f =>
| Tvoid => F.fprintf f "void" | Tvoid => F.fprintf f "void"
| Tfun false => F.fprintf f "_fn_" | Tfun false => F.fprintf f "_fn_"
| Tfun true => F.fprintf f "_fn_noreturn_" | Tfun true => F.fprintf f "_fn_noreturn_"
| Tptr ((Tarray _ | Tfun _) as typ) pk => | Tptr ({desc: Tarray _ | Tfun _} as typ) pk =>
F.fprintf f "%a(%s)" (pp_full pe) typ (ptr_kind_string pk) F.fprintf f "%a(%s)" (pp_full pe) typ (ptr_kind_string pk)
| Tptr typ pk => F.fprintf f "%a%s" (pp_full pe) typ (ptr_kind_string pk) | Tptr typ pk => F.fprintf f "%a%s" (pp_full pe) typ (ptr_kind_string pk)
| Tarray typ static_len => { | Tarray typ static_len =>
let pp_array_static_len fmt => ( let pp_array_static_len fmt => (
fun fun
| Some static_len => IntLit.pp fmt static_len | Some static_len => IntLit.pp fmt static_len
| None => F.fprintf fmt "_" | None => F.fprintf fmt "_"
); );
F.fprintf f "%a[%a]" (pp_full pe) typ pp_array_static_len static_len F.fprintf f "%a[%a]" (pp_full pe) typ pp_array_static_len static_len
}; };
/** Pretty print a type. Do nothing by default. */ /** Pretty print a type. Do nothing by default. */
@ -300,10 +323,11 @@ let d_full (t: t) => L.add_print_action (L.PTtyp_full, Obj.repr t);
/** dump a list of types. */ /** dump a list of types. */
let d_list (tl: list t) => L.add_print_action (L.PTtyp_list, Obj.repr tl); let d_list (tl: list t) => L.add_print_action (L.PTtyp_list, Obj.repr tl);
let name = let name typ =>
fun switch typ.desc {
| Tstruct name => Some name | Tstruct name => Some name
| _ => None; | _ => None
};
let unsome s => let unsome s =>
fun fun
@ -315,21 +339,23 @@ let unsome s =>
/** turn a *T into a T. fails if [typ] is not a pointer type */ /** turn a *T into a T. fails if [typ] is not a pointer type */
let strip_ptr = let strip_ptr typ =>
fun switch typ.desc {
| Tptr t _ => t | Tptr t _ => t
| _ => assert false; | _ => 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 => let array_elem default_opt typ =>
fun switch typ.desc {
| Tarray t_el _ => t_el | Tarray t_el _ => t_el
| _ => unsome "array_elem" default_opt; | _ => unsome "array_elem" default_opt
};
let is_class_of_kind check_fun typ => let is_class_of_kind check_fun typ =>
switch typ { switch typ.desc {
| Tstruct tname => check_fun tname | Tstruct tname => check_fun tname
| _ => false | _ => false
}; };
@ -341,13 +367,13 @@ let is_cpp_class = is_class_of_kind Name.Cpp.is_class;
let is_java_class = is_class_of_kind Name.Java.is_class; let is_java_class = is_class_of_kind Name.Java.is_class;
let rec is_array_of_cpp_class typ => let rec is_array_of_cpp_class typ =>
switch typ { switch typ.desc {
| Tarray typ _ => is_array_of_cpp_class typ | Tarray typ _ => is_array_of_cpp_class typ
| _ => is_cpp_class typ | _ => is_cpp_class typ
}; };
let is_pointer_to_cpp_class typ => let is_pointer_to_cpp_class typ =>
switch typ { switch typ.desc {
| Tptr t _ => is_cpp_class t | Tptr t _ => is_cpp_class t
| _ => false | _ => false
}; };
@ -364,23 +390,23 @@ let is_block_type typ => has_block_prefix (to_string typ);
/** Java types by name */ /** Java types by name */
let rec java_from_string = let rec java_from_string: string => t =
fun fun
| "" | ""
| "void" => Tvoid | "void" => mk Tvoid
| "int" => Tint IInt | "int" => mk (Tint IInt)
| "byte" => Tint IShort | "byte" => mk (Tint IShort)
| "short" => Tint IShort | "short" => mk (Tint IShort)
| "boolean" => Tint IBool | "boolean" => mk (Tint IBool)
| "char" => Tint IChar | "char" => mk (Tint IChar)
| "long" => Tint ILong | "long" => mk (Tint ILong)
| "float" => Tfloat FFloat | "float" => mk (Tfloat FFloat)
| "double" => Tfloat FDouble | "double" => 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); let stripped_typ = String.sub typ_str pos::0 len::(String.length typ_str - 2);
Tptr (Tarray (java_from_string stripped_typ) None) Pk_pointer mk (Tptr (mk (Tarray (java_from_string stripped_typ) None)) Pk_pointer)
} }
| typ_str => Tstruct (Name.Java.from_string typ_str); | typ_str => mk (Tstruct (Name.Java.from_string typ_str));
type typ = t [@@deriving compare]; type typ = t [@@deriving compare];
@ -950,11 +976,13 @@ module Procname = {
/** Return the return type of [pname_java]. */ /** Return the return type of [pname_java]. */
let java_proc_return_typ pname_java => let java_proc_return_typ pname_java :t => {
switch (java_from_string (Procname.java_get_return_type pname_java)) { let typ = java_from_string (Procname.java_get_return_type pname_java);
| Tstruct _ as typ => Tptr typ Pk_pointer switch typ.desc {
| typ => typ | Tstruct _ => mk (Tptr typ Pk_pointer)
}; | _ => typ
}
};
module Struct = { module Struct = {
type field = (Fieldname.t, T.t, Annot.Item.t) [@@deriving compare]; type field = (Fieldname.t, T.t, Annot.Item.t) [@@deriving compare];
@ -1032,7 +1060,7 @@ module 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) =>
switch typ { switch typ.desc {
| Tarray typ _ => Some typ | Tarray typ _ => Some typ
| Tstruct name => | Tstruct name =>
switch (lookup name) { switch (lookup name) {
@ -1048,7 +1076,7 @@ module Struct = {
/** If a struct type with field f, return the type of f. If not, return the default */ /** If a struct type with field f, return the type of f. If not, return the default */
let fld_typ ::lookup ::default fn (typ: T.t) => let fld_typ ::lookup ::default fn (typ: T.t) =>
switch typ { switch typ.desc {
| Tstruct name => | Tstruct name =>
switch (lookup name) { switch (lookup name) {
| Some {fields} => | Some {fields} =>
@ -1059,9 +1087,9 @@ module Struct = {
| _ => default | _ => default
}; };
let get_field_type_and_annotation ::lookup fn (typ: T.t) => let get_field_type_and_annotation ::lookup fn (typ: T.t) =>
switch typ { switch typ.desc {
| Tstruct name | Tstruct name
| Tptr (Tstruct name) _ => | Tptr {desc: Tstruct name} _ =>
switch (lookup name) { switch (lookup name) {
| Some {fields, statics} => | Some {fields, statics} =>
List.find_map List.find_map
@ -1073,7 +1101,7 @@ module Struct = {
let objc_ref_counter_annot = [({Annot.class_name: "ref_counter", parameters: []}, false)]; let objc_ref_counter_annot = [({Annot.class_name: "ref_counter", parameters: []}, false)];
/** Field used for objective-c reference counting */ /** Field used for objective-c reference counting */
let objc_ref_counter_field = (Fieldname.hidden, T.Tint IInt, objc_ref_counter_annot); let objc_ref_counter_field = (Fieldname.hidden, mk (T.Tint IInt), objc_ref_counter_annot);
let is_objc_ref_counter_field (fld, _, a) => let is_objc_ref_counter_field (fld, _, a) =>
Fieldname.is_hidden fld && Annot.Item.equal a objc_ref_counter_annot; Fieldname.is_hidden fld && Annot.Item.equal a objc_ref_counter_annot;
}; };

@ -69,9 +69,21 @@ let equal_ptr_kind: ptr_kind => ptr_kind => bool;
/** statically determined length of an array type, if any */ /** statically determined length of an array type, if any */
type static_length = option IntLit.t [@@deriving compare]; type static_length = option IntLit.t [@@deriving compare];
type type_quals [@@deriving compare];
let mk_type_quals:
default::type_quals? => is_const::bool? => is_volatile::bool? => unit => type_quals;
let is_const: type_quals => bool;
let is_volatile: type_quals => bool;
/** types for sil (structured) expressions */
/** types for sil (structured) expressions */ /** types for sil (structured) expressions */
type t = type t = {desc, quals: type_quals} [@@deriving compare]
and desc =
| Tint ikind /** integer type */ | Tint ikind /** integer type */
| Tfloat fkind /** float type */ | Tfloat fkind /** float type */
| Tvoid /** void type */ | Tvoid /** void type */
@ -93,6 +105,10 @@ and template_spec_info =
| Template (QualifiedCppName.t, list (option t)) | Template (QualifiedCppName.t, list (option t))
[@@deriving compare]; [@@deriving compare];
/** Create Typ.t from given desc. if [default] is passed then use its value to set other fields such as quals */
let mk: default::t? => quals::type_quals? => desc => t;
module Name: { module Name: {
/** Named types. */ /** Named types. */
@ -160,6 +176,10 @@ module Name: {
/** Equality for types. */ /** Equality for types. */
let equal: t => t => bool; let equal: t => t => bool;
let equal_desc: desc => desc => bool;
let equal_quals: type_quals => type_quals => bool;
/** Sets of types. */ /** Sets of types. */
module Set: Caml.Set.S with type elt = t; module Set: Caml.Set.S with type elt = t;

@ -228,8 +228,8 @@ let find_arithmetic_problem tenv proc_node_session prop exp =
let rec walk = function let rec walk = function
| Exp.Var _ -> () | Exp.Var _ -> ()
| Exp.UnOp (Unop.Neg, e, Some ( | Exp.UnOp (Unop.Neg, e, Some (
(Typ.Tint ({Typ.desc=Tint
(Typ.IUChar | Typ.IUInt | Typ.IUShort | Typ.IULong | Typ.IULongLong) as typ))) -> (Typ.IUChar | Typ.IUInt | Typ.IUShort | Typ.IULong | Typ.IULongLong)} as typ))) ->
uminus_unsigned := (e, typ) :: !uminus_unsigned uminus_unsigned := (e, typ) :: !uminus_unsigned
| Exp.UnOp(_, e, _) -> walk e | Exp.UnOp(_, e, _) -> walk e
| Exp.BinOp(op, e1, e2) -> | Exp.BinOp(op, e1, e2) ->
@ -319,7 +319,7 @@ let find_equal_formal_path tenv e prop =
match strexp with match strexp with
| Sil.Eexp (exp2, _) when Exp.equal exp2 e -> | Sil.Eexp (exp2, _) when Exp.equal exp2 e ->
(match find_in_sigma exp1 seen_hpreds with (match find_in_sigma exp1 seen_hpreds with
| Some vfs -> Some (Exp.Lfield (vfs, field, Typ.Tvoid)) | Some vfs -> Some (Exp.Lfield (vfs, field, Typ.mk Tvoid))
| None -> None) | None -> None)
| _ -> None) fields ~init:None | _ -> None) fields ~init:None
| _ -> None) prop.Prop.sigma ~init:None in | _ -> None) prop.Prop.sigma ~init:None in

@ -41,13 +41,13 @@ let mk_empty_array_rearranged len =
let extract_array_type typ = let extract_array_type typ =
if (Config.curr_language_is Config.Java) then if (Config.curr_language_is Config.Java) then
match typ with match typ.Typ.desc with
| Typ.Tptr (Typ.Tarray _ as arr, _) -> Some arr | Typ.Tptr ({Typ.desc=Tarray _} as arr, _) -> Some arr
| _ -> None | _ -> None
else else
match typ with match typ.Typ.desc with
| Typ.Tarray _ as arr -> Some arr | Typ.Tarray _ -> Some typ
| Typ.Tptr (elt, _) -> Some (Typ.Tarray (elt, None)) | Typ.Tptr (elt, _) -> Some (Typ.mk ~default:typ (Tarray (elt, None)))
| _ -> None | _ -> None
(** Return a result from a procedure call. *) (** Return a result from a procedure call. *)
@ -155,7 +155,7 @@ let create_type tenv n_lexp typ prop =
prop prop
| None -> | None ->
let mhpred = let mhpred =
match typ with match typ.Typ.desc with
| Typ.Tptr (typ', _) -> | Typ.Tptr (typ', _) ->
let sexp = Sil.Estruct ([], Sil.inst_none) in let sexp = Sil.Estruct ([], Sil.inst_none) in
let texp = Exp.Sizeof (typ', None, Subtype.subtypes) in let texp = Exp.Sizeof (typ', None, Subtype.subtypes) in
@ -237,7 +237,7 @@ let execute___instanceof_cast ~instof
let val1, prop__ = check_arith_norm_exp tenv pname val1_ prop_ in let val1, prop__ = check_arith_norm_exp tenv pname val1_ prop_ in
let texp2, prop = check_arith_norm_exp tenv pname texp2_ prop__ in let texp2, prop = check_arith_norm_exp tenv pname texp2_ prop__ in
let is_cast_to_reference = let is_cast_to_reference =
match typ1 with match typ1.desc with
| Typ.Tptr (_, Typ.Pk_reference) -> true | Typ.Tptr (_, Typ.Pk_reference) -> true
| _ -> false in | _ -> false in
(* In Java, we throw an exception, in C++ we return 0 in case of a cast to a pointer, *) (* In Java, we throw an exception, in C++ we return 0 in case of a cast to a pointer, *)
@ -457,7 +457,7 @@ let execute___objc_counter_update
{ Builtin.pdesc; tenv; prop_; path; args; loc; } { Builtin.pdesc; tenv; prop_; path; args; loc; }
: Builtin.ret_typ = : Builtin.ret_typ =
match args with match args with
| [(lexp, (Typ.Tstruct _ as typ | Tptr (Tstruct _ as typ, _)))] -> | [(lexp, ({Typ.desc=Tstruct _} as typ | {desc=Tptr ({desc=Tstruct _} as typ, _)}))] ->
(* Assumes that lexp is a temp n$1 that has the value of the object. *) (* Assumes that lexp is a temp n$1 that has the value of the object. *)
(* This is the case as a call f(o) it's translates as n$1=*&o; f(n$1) *) (* This is the case as a call f(o) it's translates as n$1=*&o; f(n$1) *)
(* n$2 = *n$1.hidden *) (* n$2 = *n$1.hidden *)
@ -480,7 +480,7 @@ let execute___objc_counter_update
removed from the list of args. *) removed from the list of args. *)
let get_suppress_npe_flag args = let get_suppress_npe_flag args =
match args with match args with
| (Exp.Const (Const.Cint i), Typ.Tint Typ.IBool):: args' when IntLit.isone i -> | (Exp.Const (Const.Cint i), {Typ.desc=Tint Typ.IBool}):: args' when IntLit.isone i ->
false, args' (* this is a CFRelease/CFRetain *) false, args' (* this is a CFRelease/CFRetain *)
| _ -> true, args | _ -> true, args
@ -750,13 +750,13 @@ let execute_alloc mk can_return_null
Exp.BinOp (bop, evaluate_char_sizeof e1', evaluate_char_sizeof e2') Exp.BinOp (bop, evaluate_char_sizeof e1', evaluate_char_sizeof e2')
| Exp.Exn _ | Exp.Closure _ | Exp.Const _ | Exp.Cast _ | Exp.Lvar _ | Exp.Lfield _ | Exp.Exn _ | Exp.Closure _ | Exp.Const _ | Exp.Cast _ | Exp.Lvar _ | Exp.Lfield _
| Exp.Lindex _ -> e | Exp.Lindex _ -> e
| Exp.Sizeof (Typ.Tarray (Typ.Tint ik, _), Some len, _) when Typ.ikind_is_char ik -> | Exp.Sizeof ({Typ.desc=Tarray ({Typ.desc=Tint ik}, _)}, Some len, _) when Typ.ikind_is_char ik ->
evaluate_char_sizeof len evaluate_char_sizeof len
| Exp.Sizeof (Typ.Tarray (Typ.Tint ik, Some len), None, _) when Typ.ikind_is_char ik -> | Exp.Sizeof ({Typ.desc=Tarray ({Typ.desc=Tint ik}, Some len)}, None, _) when Typ.ikind_is_char ik ->
evaluate_char_sizeof (Exp.Const (Const.Cint len)) evaluate_char_sizeof (Exp.Const (Const.Cint len))
| Exp.Sizeof _ -> e in | Exp.Sizeof _ -> e in
let size_exp, procname = match args with let size_exp, procname = match args with
| [(Exp.Sizeof (Tstruct (ObjcClass _ as name) as s, len, subt), _)] -> | [(Exp.Sizeof ({Typ.desc=Tstruct (ObjcClass _ as name)} as s, len, subt), _)] ->
let struct_type = let struct_type =
match AttributesTable.get_correct_type_from_objc_class_name name with match AttributesTable.get_correct_type_from_objc_class_name name with
| Some struct_type -> struct_type | Some struct_type -> struct_type
@ -776,7 +776,7 @@ let execute_alloc mk can_return_null
let n_size_exp' = evaluate_char_sizeof n_size_exp in let n_size_exp' = evaluate_char_sizeof n_size_exp in
Prop.exp_normalize_prop tenv prop n_size_exp', prop in Prop.exp_normalize_prop tenv prop n_size_exp', prop in
let cnt_te = let cnt_te =
Exp.Sizeof (Typ.Tarray (Typ.Tint Typ.IChar, None), Some size_exp', Subtype.exact) in Exp.Sizeof (Typ.mk (Tarray (Typ.mk (Tint Typ.IChar), None)), Some size_exp', Subtype.exact) in
let id_new = Ident.create_fresh Ident.kprimed in let id_new = Ident.create_fresh Ident.kprimed in
let exp_new = Exp.Var id_new in let exp_new = Exp.Var id_new in
let ptsto_new = let ptsto_new =
@ -817,7 +817,7 @@ let execute___cxx_typeid ({ Builtin.pdesc; tenv; prop_; args; loc} as r)
~default:typ_ in ~default:typ_ in
let typ_string = Typ.to_string typ in let typ_string = Typ.to_string typ in
let set_instr = let set_instr =
Sil.Store (field_exp, Typ.Tvoid, Exp.Const (Const.Cstr typ_string), loc) in Sil.Store (field_exp, Typ.mk Tvoid, Exp.Const (Const.Cstr typ_string), loc) in
SymExec.instrs ~mask_errors:true tenv pdesc [set_instr] res SymExec.instrs ~mask_errors:true tenv pdesc [set_instr] res
| _ -> res) | _ -> res)
| _ -> raise (Exceptions.Wrong_argument_number __POS__) | _ -> raise (Exceptions.Wrong_argument_number __POS__)
@ -933,7 +933,7 @@ let execute___infer_fail { Builtin.pdesc; tenv; prop_; path; args; loc; }
| _ -> | _ ->
raise (Exceptions.Wrong_argument_number __POS__) in raise (Exceptions.Wrong_argument_number __POS__) in
let set_instr = let set_instr =
Sil.Store (Exp.Lvar Sil.custom_error, Typ.Tvoid, Exp.Const (Const.Cstr error_str), loc) in Sil.Store (Exp.Lvar Sil.custom_error, Typ.mk Tvoid, Exp.Const (Const.Cstr error_str), loc) in
SymExec.instrs ~mask_errors:true tenv pdesc [set_instr] [(prop_, path)] SymExec.instrs ~mask_errors:true tenv pdesc [set_instr] [(prop_, path)]
(* translate builtin assertion failure *) (* translate builtin assertion failure *)
@ -946,18 +946,18 @@ let execute___assert_fail { Builtin.pdesc; tenv; prop_; path; args; loc; }
| _ -> | _ ->
raise (Exceptions.Wrong_argument_number __POS__) in raise (Exceptions.Wrong_argument_number __POS__) in
let set_instr = let set_instr =
Sil.Store (Exp.Lvar Sil.custom_error, Typ.Tvoid, Exp.Const (Const.Cstr error_str), loc) in Sil.Store (Exp.Lvar Sil.custom_error, Typ.mk Tvoid, Exp.Const (Const.Cstr error_str), loc) in
SymExec.instrs ~mask_errors:true tenv pdesc [set_instr] [(prop_, path)] SymExec.instrs ~mask_errors:true tenv pdesc [set_instr] [(prop_, path)]
let execute_objc_alloc_no_fail let execute_objc_alloc_no_fail
symb_state typ alloc_fun_opt symb_state typ alloc_fun_opt
{ Builtin.pdesc; tenv; ret_id; loc; } = { Builtin.pdesc; tenv; ret_id; loc; } =
let alloc_fun = Exp.Const (Const.Cfun BuiltinDecl.__objc_alloc_no_fail) in let alloc_fun = Exp.Const (Const.Cfun BuiltinDecl.__objc_alloc_no_fail) in
let ptr_typ = Typ.Tptr (typ, Typ.Pk_pointer) in let ptr_typ = Typ.mk (Tptr (typ, Typ.Pk_pointer)) in
let sizeof_typ = Exp.Sizeof (typ, None, Subtype.exact) in let sizeof_typ = Exp.Sizeof (typ, None, Subtype.exact) in
let alloc_fun_exp = let alloc_fun_exp =
match alloc_fun_opt with match alloc_fun_opt with
| Some pname -> [Exp.Const (Const.Cfun pname), Typ.Tvoid] | Some pname -> [Exp.Const (Const.Cfun pname), Typ.mk Tvoid]
| None -> [] in | None -> [] in
let alloc_instr = let alloc_instr =
Sil.Call Sil.Call
@ -969,7 +969,7 @@ let execute_objc_NSArray_alloc_no_fail builtin_args symb_state pname =
let ret_typ = let ret_typ =
match builtin_args.Builtin.ret_id with match builtin_args.Builtin.ret_id with
| Some (_, typ) -> typ | Some (_, typ) -> typ
| None -> Typ.Tptr (Tvoid, Pk_pointer) in | None -> Typ.mk (Tptr (Typ.mk Tvoid, Pk_pointer)) in
execute_objc_alloc_no_fail symb_state ret_typ (Some pname) builtin_args execute_objc_alloc_no_fail symb_state ret_typ (Some pname) builtin_args
let execute_NSArray_arrayWithObjects_count builtin_args = let execute_NSArray_arrayWithObjects_count builtin_args =
@ -988,7 +988,7 @@ let execute_objc_NSDictionary_alloc_no_fail symb_state pname builtin_args =
let ret_typ = let ret_typ =
match builtin_args.Builtin.ret_id with match builtin_args.Builtin.ret_id with
| Some (_, typ) -> typ | Some (_, typ) -> typ
| None -> Typ.Tptr (Tvoid, Pk_pointer) in | None -> Typ.mk (Tptr (Typ.mk Tvoid, Pk_pointer)) in
execute_objc_alloc_no_fail symb_state ret_typ (Some pname) builtin_args execute_objc_alloc_no_fail symb_state ret_typ (Some pname) builtin_args
let execute___objc_dictionary_literal builtin_args = let execute___objc_dictionary_literal builtin_args =

@ -407,17 +407,17 @@ let mk_rules_for_dll tenv (para : Sil.hpara_dll) : rule list =
(****************** Start of Predicate Discovery ******************) (****************** Start of Predicate Discovery ******************)
let typ_get_recursive_flds tenv typ_exp = let typ_get_recursive_flds tenv typ_exp =
let filter typ (_, (t: Typ.t), _) = let filter typ (_, (t: Typ.t), _) =
match t with match t.desc with
| Tstruct _ | Tint _ | Tfloat _ | Tvoid | Tfun _ -> | Tstruct _ | Tint _ | Tfloat _ | Tvoid | Tfun _ ->
false false
| Tptr (Tstruct _ as typ', _) -> | Tptr ({desc=Tstruct _} as typ', _) ->
Typ.equal typ' typ Typ.equal typ' typ
| Tptr _ | Tarray _ -> | Tptr _ | Tarray _ ->
false false
in in
match typ_exp with match typ_exp with
| Exp.Sizeof (typ, _, _) -> ( | Exp.Sizeof (typ, _, _) -> (
match typ with match typ.desc with
| Tstruct name -> ( | Tstruct name -> (
match Tenv.lookup tenv name with match Tenv.lookup tenv name with
| Some { fields } -> List.map ~f:fst3 (List.filter ~f:(filter typ) fields) | Some { fields } -> List.map ~f:fst3 (List.filter ~f:(filter typ) fields)
@ -988,7 +988,7 @@ let remove_opt _prop =
let cycle_has_weak_or_unretained_or_assign_field tenv cycle = let cycle_has_weak_or_unretained_or_assign_field tenv cycle =
(* returns items annotation for field fn in struct t *) (* returns items annotation for field fn in struct t *)
let get_item_annotation (t: Typ.t) fn = let get_item_annotation (t: Typ.t) fn =
match t with match t.desc with
| Tstruct name -> ( | Tstruct name -> (
let equal_fn (fn', _, _) = Fieldname.equal fn fn' in let equal_fn (fn', _, _) = Fieldname.equal fn fn' in
match Tenv.lookup tenv name with match Tenv.lookup tenv name with

@ -71,7 +71,7 @@ end = struct
L.d_str "t: "; Typ.d_full t; L.d_ln (); L.d_str "t: "; Typ.d_full t; L.d_ln ();
assert false assert false
in in
match se, t, syn_offs with match se, t.desc, syn_offs with
| _, _, [] -> (se, t) | _, _, [] -> (se, t)
| Sil.Estruct (fsel, _), Tstruct name, Field (fld, _) :: syn_offs' -> ( | Sil.Estruct (fsel, _), Tstruct name, Field (fld, _) :: syn_offs' -> (
match Tenv.lookup tenv name with match Tenv.lookup tenv name with
@ -92,7 +92,7 @@ end = struct
(** Replace a strexp at the given syntactic offset list *) (** Replace a strexp at the given syntactic offset list *)
let rec replace_strexp_at_syn_offsets tenv se (t: Typ.t) syn_offs update = let rec replace_strexp_at_syn_offsets tenv se (t: Typ.t) syn_offs update =
match se, t, syn_offs with match se, t.desc, syn_offs with
| _, _, [] -> | _, _, [] ->
update se update se
| Sil.Estruct (fsel, inst), Tstruct name, Field (fld, _) :: syn_offs' -> ( | Sil.Estruct (fsel, inst), Tstruct name, Field (fld, _) :: syn_offs' -> (
@ -163,7 +163,7 @@ end = struct
let path = (root, offs') in let path = (root, offs') in
if pred (path, se, typ) then found := (sigma, hpred, offs') :: !found if pred (path, se, typ) then found := (sigma, hpred, offs') :: !found
else begin else begin
match se, typ with match se, typ.desc with
| Sil.Estruct (fsel, _), Tstruct name -> ( | Sil.Estruct (fsel, _), Tstruct name -> (
match Tenv.lookup tenv name with match Tenv.lookup tenv name with
| Some { fields } -> | Some { fields } ->
@ -442,8 +442,8 @@ let keep_only_indices tenv
(** 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 = function let array_typ_can_abstract {Typ.desc} = match desc with
| Typ.Tarray (Typ.Tptr (Typ.Tfun _, _), _) -> false (* don't abstract arrays of pointers *) | Tarray ({desc=Tptr ({desc=Tfun _}, _)}, _) -> false (* don't abstract arrays of pointers *)
| _ -> true | _ -> true
(** This function checks whether we can apply an abstraction to a strexp *) (** This function checks whether we can apply an abstraction to a strexp *)
@ -540,7 +540,7 @@ let check_after_array_abstraction tenv prop =
let rec check_se root offs typ = function let rec check_se root offs typ = function
| Sil.Eexp _ -> () | Sil.Eexp _ -> ()
| Sil.Earray (_, esel, _) -> (* check that no more than 2 elements are in the array *) | Sil.Earray (_, esel, _) -> (* check that no more than 2 elements are in the array *)
let typ_elem = Typ.array_elem (Some Typ.Tvoid) typ in let typ_elem = Typ.array_elem (Some (Typ.mk Tvoid)) typ in
if List.length esel > 2 && array_typ_can_abstract typ then if List.length esel > 2 && array_typ_can_abstract typ then
if List.for_all ~f:(check_index root offs) esel then () if List.for_all ~f:(check_index root offs) esel then ()
else report_error prop else report_error prop
@ -549,11 +549,11 @@ let check_after_array_abstraction tenv prop =
esel esel
| Sil.Estruct (fsel, _) -> | Sil.Estruct (fsel, _) ->
List.iter ~f:(fun (f, se) -> List.iter ~f:(fun (f, se) ->
let typ_f = Typ.Struct.fld_typ ~lookup ~default:Tvoid f typ in let typ_f = Typ.Struct.fld_typ ~lookup ~default:(Typ.mk Tvoid) f typ in
check_se root (offs @ [Sil.Off_fld (f, typ)]) typ_f se) fsel in check_se root (offs @ [Sil.Off_fld (f, typ)]) typ_f se) fsel in
let check_hpred = function let check_hpred = function
| Sil.Hpointsto (root, se, texp) -> | Sil.Hpointsto (root, se, texp) ->
let typ = Exp.texp_to_typ (Some Typ.Tvoid) texp in let typ = Exp.texp_to_typ (Some (Typ.mk Tvoid)) texp in
check_se root [] typ se check_se root [] typ se
| Sil.Hlseg _ | Sil.Hdllseg _ -> () in | Sil.Hlseg _ | Sil.Hdllseg _ -> () in
let check_sigma sigma = List.iter ~f:check_hpred sigma in let check_sigma sigma = List.iter ~f:check_hpred sigma in

@ -995,13 +995,14 @@ and static_length_partial_join l1 l2 =
and dynamic_length_partial_join l1 l2 = and dynamic_length_partial_join l1 l2 =
option_partial_join (fun len1 len2 -> Some (length_partial_join len1 len2)) l1 l2 option_partial_join (fun len1 len2 -> Some (length_partial_join len1 len2)) l1 l2
and typ_partial_join t1 t2 = match t1, t2 with and typ_partial_join (t1 : Typ.t) (t2 : Typ.t) = match t1.desc, t2.desc with
| Typ.Tptr (t1, pk1), Typ.Tptr (t2, pk2) when Typ.equal_ptr_kind pk1 pk2 -> | Typ.Tptr (t1, pk1), Typ.Tptr (t2, pk2)
Typ.Tptr (typ_partial_join t1 t2, pk1) when Typ.equal_ptr_kind pk1 pk2 && Typ.equal_quals t1.quals t2.quals ->
| Typ.Tarray (typ1, len1), Typ.Tarray (typ2, len2) -> Typ.mk ~default:t1 (Tptr (typ_partial_join t1 t2, pk1)) (* quals are the same for t1 and t2 *)
| Typ.Tarray (typ1, len1), Typ.Tarray (typ2, len2) when Typ.equal_quals typ1.quals typ2.quals ->
let t = typ_partial_join typ1 typ2 in let t = typ_partial_join typ1 typ2 in
let len = static_length_partial_join len1 len2 in let len = static_length_partial_join len1 len2 in
Typ.Tarray (t, len) Typ.mk ~default:t1 (Tarray (t, len)) (* quals are the same for t1 and t2 *)
| _ when Typ.equal t1 t2 -> t1 (* common case *) | _ when Typ.equal t1 t2 -> t1 (* common case *)
| _ -> | _ ->
L.d_str "typ_partial_join no match "; L.d_str "typ_partial_join no match ";

@ -298,7 +298,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.Tarray (t, _), _, _)), lambda) -> | (Sil.Hpointsto (e, Sil.Earray (e', l, _), Exp.Sizeof ({Typ.desc=Tarray (t, _)}, _, _)), lambda) ->
incr dotty_state_count; (* increment once more n+1 is the box for the array *) incr dotty_state_count; (* increment once more n+1 is the box for the array *)
let e_color_str = color_to_str (exp_color e) in let e_color_str = color_to_str (exp_color e) in
let e_color_str'= color_to_str (exp_color e') in let e_color_str'= color_to_str (exp_color e') in

@ -511,9 +511,9 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
(Pvar.is_local pvar || Pvar.is_global pvar) && (Pvar.is_local pvar || Pvar.is_global pvar) &&
not (Pvar.is_frontend_tmp pvar) && not (Pvar.is_frontend_tmp pvar) &&
match hpred_typ_opt, find_typ_without_ptr prop pvar with match hpred_typ_opt, find_typ_without_ptr prop pvar with
| Some (Exp.Sizeof (t1, _, _)), Some (Exp.Sizeof (Typ.Tptr (t2, _), _, _)) -> | Some (Exp.Sizeof (t1, _, _)), Some (Exp.Sizeof ({Typ.desc=Tptr (t2, _)}, _, _)) ->
Typ.equal t1 t2 Typ.equal t1 t2
| Some (Exp.Sizeof (Typ.Tint _, _, _)), Some (Exp.Sizeof (Typ.Tint _, _, _)) | Some (Exp.Sizeof ({Typ.desc=Tint _}, _, _)), Some (Exp.Sizeof ({Typ.desc=Tint _}, _, _))
when is_file -> (* must be a file opened with "open" *) when is_file -> (* must be a file opened with "open" *)
true true
| _ -> false in | _ -> false in
@ -581,7 +581,7 @@ let vpath_find tenv prop _exp : DExp.t option * Typ.t option =
(match lexp with (match lexp with
| Exp.Lvar pv -> | Exp.Lvar pv ->
let typo = match texp with let typo = match texp with
| Exp.Sizeof (Tstruct name, _, _) -> ( | Exp.Sizeof ({Typ.desc=Tstruct name}, _, _) -> (
match Tenv.lookup tenv name with match Tenv.lookup tenv name with
| Some {fields} -> | Some {fields} ->
List.find ~f:(fun (f', _, _) -> Fieldname.equal f' f) fields |> List.find ~f:(fun (f', _, _) -> Fieldname.equal f' f) fields |>

@ -664,7 +664,7 @@ let report_context_leaks pname sigma tenv =
| Some path -> path | Some path -> path
| None -> assert false (* a path must exist in order for a leak to be reported *) in | None -> assert false (* a path must exist in order for a leak to be reported *) in
let err_desc = let err_desc =
Errdesc.explain_context_leak pname (Typ.Tstruct name) fld_name leak_path in Errdesc.explain_context_leak pname (Typ.mk (Tstruct name)) fld_name leak_path in
let exn = Exceptions.Context_leak (err_desc, __POS__) in let exn = Exceptions.Context_leak (err_desc, __POS__) in
Reporting.log_error pname exn) Reporting.log_error pname exn)
context_exps in context_exps in
@ -672,7 +672,7 @@ let report_context_leaks pname sigma tenv =
let context_exps = let context_exps =
List.fold List.fold
~f:(fun exps hpred -> match hpred with ~f:(fun exps hpred -> match hpred with
| Sil.Hpointsto (_, Eexp (exp, _), Sizeof (Tptr (Tstruct name, _), _, _)) | Sil.Hpointsto (_, Eexp (exp, _), Sizeof ({desc=Tptr ({desc=Tstruct name}, _)}, _, _))
when not (Exp.is_null_literal exp) when not (Exp.is_null_literal exp)
&& AndroidFramework.is_context tenv name && AndroidFramework.is_context tenv name
&& not (AndroidFramework.is_application tenv name) -> && not (AndroidFramework.is_application tenv name) ->

@ -30,7 +30,7 @@ let add_dispatch_calls pdesc cg tenv =
when call_flags_is_dispatch call_flags -> when call_flags_is_dispatch call_flags ->
(* the frontend should not populate the list of targets *) (* the frontend should not populate the list of targets *)
assert (List.is_empty call_flags.CallFlags.cf_targets); assert (List.is_empty call_flags.CallFlags.cf_targets);
let receiver_typ_no_ptr = match receiver_typ with let receiver_typ_no_ptr = match receiver_typ.Typ.desc with
| Typ.Tptr (typ', _) -> | Typ.Tptr (typ', _) ->
typ' typ'
| _ -> | _ ->

@ -466,12 +466,12 @@ let rec create_strexp_of_type tenv struct_init_mode (typ : Typ.t) len inst : Sil
if Config.curr_language_is Config.Java && if Config.curr_language_is Config.Java &&
Sil.equal_inst inst Sil.Ialloc Sil.equal_inst inst Sil.Ialloc
then then
match typ with match typ.desc with
| Tfloat _ -> Exp.Const (Cfloat 0.0) | Tfloat _ -> Exp.Const (Cfloat 0.0)
| _ -> Exp.zero | _ -> Exp.zero
else else
create_fresh_var () in create_fresh_var () in
match typ, len with match typ.desc, len with
| (Tint _ | Tfloat _ | Tvoid | Tfun _ | Tptr _), None -> | (Tint _ | Tfloat _ | Tvoid | Tfun _ | Tptr _), None ->
Eexp (init_value (), inst) Eexp (init_value (), inst)
| Tstruct name, _ -> ( | Tstruct name, _ -> (
@ -529,7 +529,7 @@ let rec pi_sorted_remove_redundant (pi : pi) = match pi with
let sigma_get_unsigned_exps sigma = let sigma_get_unsigned_exps sigma =
let uexps = ref [] in let uexps = ref [] in
let do_hpred (hpred : Sil.hpred) = match hpred with let do_hpred (hpred : Sil.hpred) = match hpred with
| Hpointsto (_, Eexp (e, _), Sizeof (Tint ik, _, _)) | Hpointsto (_, Eexp (e, _), Sizeof ({desc=Tint ik}, _, _))
when Typ.ikind_is_unsigned ik -> when Typ.ikind_is_unsigned ik ->
uexps := e :: !uexps uexps := e :: !uexps
| _ -> () in | _ -> () in
@ -541,13 +541,13 @@ let sigma_get_unsigned_exps sigma =
to ensure the soundness of this collapsing. *) to ensure the soundness of this collapsing. *)
let exp_collapse_consecutive_indices_prop (typ : Typ.t) exp = let exp_collapse_consecutive_indices_prop (typ : Typ.t) exp =
let typ_is_base (typ1 : Typ.t) = let typ_is_base (typ1 : Typ.t) =
match typ1 with match typ1.desc with
| Tint _ | Tfloat _ | Tstruct _ | Tvoid | Tfun _ -> | Tint _ | Tfloat _ | Tstruct _ | Tvoid | Tfun _ ->
true true
| _ -> | _ ->
false in false in
let typ_is_one_step_from_base = let typ_is_one_step_from_base =
match typ with match typ.desc with
| Tptr (t, _) | Tarray (t, _) -> | Tptr (t, _) | Tarray (t, _) ->
typ_is_base t typ_is_base t
| _ -> | _ ->
@ -712,10 +712,10 @@ module Normalize = struct
Closure { c with captured_vars; } Closure { c with captured_vars; }
| Const _ -> | Const _ ->
e e
| Sizeof (Tarray (Tint ik, _), Some l, _) | Sizeof ({desc=Tarray ({desc=Tint ik}, _)}, Some l, _)
when Typ.ikind_is_char ik && Config.curr_language_is Config.Clang -> when Typ.ikind_is_char ik && Config.curr_language_is Config.Clang ->
eval l eval l
| Sizeof (Tarray (Tint ik, Some l), _, _) | Sizeof ({desc=Tarray ({desc=Tint ik}, Some l)}, _, _)
when Typ.ikind_is_char ik && Config.curr_language_is Config.Clang -> when Typ.ikind_is_char ik && Config.curr_language_is Config.Clang ->
Const (Cint l) Const (Cint l)
| Sizeof _ -> | Sizeof _ ->
@ -991,11 +991,11 @@ 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 (Tarray (elt, _), Some len, _), Sizeof (elt2, None, _) | Sizeof ({desc=Tarray (elt, _)}, Some len, _), Sizeof (elt2, 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 (Tarray (elt, Some len), None, _), Sizeof (elt2, None, _) | Sizeof ({desc=Tarray (elt, Some len)}, None, _), Sizeof (elt2, 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 ->
Const (Cint len) Const (Cint len)
@ -1372,28 +1372,28 @@ module Normalize = struct
let normalized_cnt = strexp_normalize tenv sub cnt in let normalized_cnt = strexp_normalize tenv sub cnt in
let normalized_te = texp_normalize tenv sub te in let normalized_te = texp_normalize tenv sub te in
begin match normalized_cnt, normalized_te with begin match normalized_cnt, normalized_te with
| Earray (Exp.Sizeof _ as size, [], inst), Sizeof (Tarray _, _, _) -> | Earray (Exp.Sizeof _ as size, [], inst), Sizeof ({desc=Tarray _}, _, _) ->
(* check for an empty array whose size expression is (Sizeof type), and turn the array (* check for an empty array whose size expression is (Sizeof type), and turn the array
into a strexp of the given type *) into a strexp of the given type *)
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 (BinOp (Mult, Sizeof (t, None, st1), x), esel, inst), | Earray (BinOp (Mult, Sizeof (t, None, st1), x), esel, inst),
Sizeof (Tarray (elt, _) as arr, _, _) when Typ.equal t elt -> Sizeof ({desc=Tarray (elt, _)} as arr, _, _) when Typ.equal t elt ->
let len = Some x in let len = Some x in
let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof (arr, len, st1), None) inst in let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof (arr, len, st1), None) inst in
replace_hpred (replace_array_contents hpred' esel) replace_hpred (replace_array_contents hpred' esel)
| Earray (BinOp (Mult, x, Sizeof (t, None, st1)), esel, inst), | Earray (BinOp (Mult, x, Sizeof (t, None, st1)), esel, inst),
Sizeof (Tarray (elt, _) as arr, _, _) when Typ.equal t elt -> Sizeof ({desc=Tarray (elt, _)} as arr, _, _) when Typ.equal t elt ->
let len = Some x in let len = Some x in
let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof (arr, len, st1), None) inst in let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof (arr, len, st1), None) inst in
replace_hpred (replace_array_contents hpred' esel) replace_hpred (replace_array_contents hpred' esel)
| Earray (BinOp (Mult, Sizeof (t, Some len, st1), x), esel, inst), | Earray (BinOp (Mult, Sizeof (t, Some len, st1), x), esel, inst),
Sizeof (Tarray (elt, _) as arr, _, _) when Typ.equal t elt -> Sizeof ({desc=Tarray (elt, _)} as arr, _, _) when Typ.equal t elt ->
let len = Some (Exp.BinOp(Mult, x, len)) in let len = Some (Exp.BinOp(Mult, x, len)) in
let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof (arr, len, st1), None) inst in let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof (arr, len, st1), None) inst in
replace_hpred (replace_array_contents hpred' esel) replace_hpred (replace_array_contents hpred' esel)
| Earray (BinOp (Mult, x, Sizeof (t, Some len, st1)), esel, inst), | Earray (BinOp (Mult, x, Sizeof (t, Some len, st1)), esel, inst),
Sizeof (Tarray (elt, _) as arr, _, _) when Typ.equal t elt -> Sizeof ({desc=Tarray (elt, _)} as arr, _, _) when Typ.equal t elt ->
let len = Some (Exp.BinOp(Mult, x, len)) in let len = Some (Exp.BinOp(Mult, x, len)) in
let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof (arr, len, st1), None) inst in let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof (arr, len, st1), None) inst in
replace_hpred (replace_array_contents hpred' esel) replace_hpred (replace_array_contents hpred' esel)

@ -37,7 +37,7 @@ let rec remove_redundancy have_same_key acc = function
else remove_redundancy have_same_key (x:: acc) l else remove_redundancy have_same_key (x:: acc) l
let rec is_java_class tenv (typ: Typ.t) = let rec is_java_class tenv (typ: Typ.t) =
match typ with match typ.desc with
| Tstruct name -> Typ.Name.Java.is_class name | Tstruct name -> Typ.Name.Java.is_class name
| Tarray (inner_typ, _) | Tptr (inner_typ, _) -> is_java_class tenv inner_typ | Tarray (inner_typ, _) | Tptr (inner_typ, _) -> is_java_class tenv inner_typ
| _ -> false | _ -> false
@ -170,7 +170,7 @@ end = struct
end end
(** Return true if the two types have sizes which can be compared *) (** Return true if the two types have sizes which can be compared *)
let type_size_comparable t1 t2 = match t1, t2 with let type_size_comparable t1 t2 = match t1.Typ.desc, t2.Typ.desc with
| Typ.Tint _, Typ.Tint _ -> true | Typ.Tint _, Typ.Tint _ -> true
| _ -> false | _ -> false
@ -187,7 +187,7 @@ let type_size_compare t1 t2 =
let n1 = ik_size ik1 in let n1 = ik_size ik1 in
let n2 = ik_size ik2 in let n2 = ik_size ik2 in
n1 - n2 in n1 - n2 in
match t1, t2 with match t1.Typ.desc, t2.Typ.desc with
| Typ.Tint ik1, Typ.Tint ik2 -> | Typ.Tint ik1, Typ.Tint ik2 ->
Some (ik_compare ik1 ik2) Some (ik_compare ik1 ik2)
| _ -> None | _ -> None
@ -380,7 +380,7 @@ end = struct
let add_lt_minus1_e e = let add_lt_minus1_e e =
lts := (Exp.minus_one, e)::!lts in lts := (Exp.minus_one, e)::!lts in
let type_opt_is_unsigned = function let type_opt_is_unsigned = function
| Some Typ.Tint ik -> Typ.ikind_is_unsigned ik | Some {Typ.desc=Tint ik} -> Typ.ikind_is_unsigned ik
| _ -> false in | _ -> false in
let type_of_texp = function let type_of_texp = function
| Exp.Sizeof (t, _, _) -> Some t | Exp.Sizeof (t, _, _) -> Some t
@ -400,7 +400,7 @@ end = struct
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 let elt_t = match t with
| Some Typ.Tarray (t, _) -> Some t | Some {Typ.desc=Tarray (t, _)} -> Some t
| _ -> None in | _ -> None in
add_lt_minus1_e len; add_lt_minus1_e len;
List.iter ~f:(fun (idx, se) -> List.iter ~f:(fun (idx, se) ->
@ -1339,11 +1339,12 @@ 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.Tarray (typ2, None) in let typ2' = Typ.mk (Tarray (typ2, None)) 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
of Tarray, so forgetting the length of typ2' here is not a problem. *) of Tarray, so forgetting the length of typ2' here is not a problem. Not one of those
functions use typ.quals either *)
sexp_imply tenv source true calc_missing subs se1 se2' typ2' (* calculate index_frame because the rhs is a singleton array *) sexp_imply tenv source true calc_missing subs se1 se2' typ2' (* calculate index_frame because the rhs is a singleton array *)
| _ -> | _ ->
d_impl_err ("sexp_imply not implemented", subs, (EXC_FALSE_SEXPS (se1, se2))); d_impl_err ("sexp_imply not implemented", subs, (EXC_FALSE_SEXPS (se1, se2)));
@ -1357,7 +1358,7 @@ and struct_imply tenv source calc_missing subs fsel1 fsel2 typ2 : subst2 * ((Fie
begin begin
match Fieldname.compare f1 f2 with match Fieldname.compare f1 f2 with
| 0 -> | 0 ->
let typ' = Typ.Struct.fld_typ ~lookup ~default:Typ.Tvoid f2 typ2 in let typ' = Typ.Struct.fld_typ ~lookup ~default:(Typ.mk Tvoid) f2 typ2 in
let subs', se_frame, se_missing = let subs', se_frame, se_missing =
sexp_imply tenv (Exp.Lfield (source, f2, typ2)) false calc_missing subs se1 se2 typ' in sexp_imply tenv (Exp.Lfield (source, f2, typ2)) false calc_missing subs se1 se2 typ' in
let subs'', fld_frame, fld_missing = struct_imply tenv source calc_missing subs' fsel1' fsel2' typ2 in let subs'', fld_frame, fld_missing = struct_imply tenv source calc_missing subs' fsel1' fsel2' typ2 in
@ -1372,7 +1373,7 @@ and struct_imply tenv source calc_missing subs fsel1 fsel2 typ2 : subst2 * ((Fie
let subs', fld_frame, fld_missing = struct_imply tenv source calc_missing subs fsel1' fsel2 typ2 in let subs', fld_frame, fld_missing = struct_imply tenv source calc_missing subs fsel1' fsel2 typ2 in
subs', ((f1, se1) :: fld_frame), fld_missing subs', ((f1, se1) :: fld_frame), fld_missing
| _ -> | _ ->
let typ' = Typ.Struct.fld_typ ~lookup ~default:Typ.Tvoid f2 typ2 in let typ' = Typ.Struct.fld_typ ~lookup ~default:(Typ.mk Tvoid) f2 typ2 in
let subs' = let subs' =
sexp_imply_nolhs tenv (Exp.Lfield (source, f2, typ2)) calc_missing subs se2 typ' in sexp_imply_nolhs tenv (Exp.Lfield (source, f2, typ2)) calc_missing subs se2 typ' in
let subs', fld_frame, fld_missing = struct_imply tenv source calc_missing subs' fsel1 fsel2' typ2 in let subs', fld_frame, fld_missing = struct_imply tenv source calc_missing subs' fsel1 fsel2' typ2 in
@ -1380,7 +1381,7 @@ and struct_imply tenv source calc_missing subs fsel1 fsel2 typ2 : subst2 * ((Fie
subs', fld_frame, fld_missing' subs', fld_frame, fld_missing'
end end
| [], (f2, se2) :: fsel2' -> | [], (f2, se2) :: fsel2' ->
let typ' = Typ.Struct.fld_typ ~lookup ~default:Typ.Tvoid f2 typ2 in let typ' = Typ.Struct.fld_typ ~lookup ~default:(Typ.mk Tvoid) f2 typ2 in
let subs' = sexp_imply_nolhs tenv (Exp.Lfield (source, f2, typ2)) calc_missing subs se2 typ' in let subs' = sexp_imply_nolhs tenv (Exp.Lfield (source, f2, typ2)) calc_missing subs se2 typ' in
let subs'', fld_frame, fld_missing = struct_imply tenv source calc_missing subs' [] fsel2' typ2 in let subs'', fld_frame, fld_missing = struct_imply tenv source calc_missing subs' [] fsel2' typ2 in
subs'', fld_frame, (f2, se2):: fld_missing subs'', fld_frame, (f2, se2):: fld_missing
@ -1388,7 +1389,7 @@ and struct_imply tenv source calc_missing subs fsel1 fsel2 typ2 : subst2 * ((Fie
and array_imply tenv source calc_index_frame calc_missing subs esel1 esel2 typ2 and array_imply tenv source calc_index_frame calc_missing subs esel1 esel2 typ2
: subst2 * ((Exp.t * Sil.strexp) list) * ((Exp.t * Sil.strexp) list) : subst2 * ((Exp.t * Sil.strexp) list) * ((Exp.t * Sil.strexp) list)
= =
let typ_elem = Typ.array_elem (Some Typ.Tvoid) typ2 in let typ_elem = Typ.array_elem (Some (Typ.mk Tvoid)) typ2 in
match esel1, esel2 with match esel1, esel2 with
| _,[] -> subs, esel1, [] | _,[] -> subs, esel1, []
| (e1, se1) :: esel1', (e2, se2) :: esel2' -> | (e1, se1) :: esel1', (e2, se2) :: esel2' ->
@ -1498,7 +1499,7 @@ let expand_hpred_pointer =
| Sil.Hpointsto (Lfield (adr_base, fld, adr_typ), cnt, cnt_texp) -> | Sil.Hpointsto (Lfield (adr_base, fld, adr_typ), cnt, cnt_texp) ->
let cnt_texp' = let cnt_texp' =
match match
match adr_typ with match adr_typ.desc with
| Tstruct name -> ( | Tstruct name -> (
match Tenv.lookup tenv name with match Tenv.lookup tenv name with
| Some _ -> | Some _ ->
@ -1518,7 +1519,7 @@ let expand_hpred_pointer =
incr count ; incr count ;
let fields = [(fld, cnt_typ, Annot.Item.empty)] in let fields = [(fld, cnt_typ, Annot.Item.empty)] in
ignore (Tenv.mk_struct tenv ~fields name) ; ignore (Tenv.mk_struct tenv ~fields name) ;
Exp.Sizeof (Tstruct name, len, st) Exp.Sizeof (Typ.mk (Tstruct name), len, st)
| _ -> | _ ->
(* type of struct at adr_base and of contents are both unknown: give up *) (* type of struct at adr_base and of contents are both unknown: give up *)
raise (Failure "expand_hpred_pointer: Unexpected non-sizeof type in Lfield") in raise (Failure "expand_hpred_pointer: Unexpected non-sizeof type in Lfield") in
@ -1526,7 +1527,7 @@ let expand_hpred_pointer =
expand true true hpred' expand true true hpred'
| Sil.Hpointsto (Exp.Lindex (e, ind), se, t) -> | Sil.Hpointsto (Exp.Lindex (e, ind), se, t) ->
let t' = match t with let t' = match t with
| Exp.Sizeof (t_, len, st) -> Exp.Sizeof (Typ.Tarray (t_, None), len, st) | Exp.Sizeof (t_, len, st) -> Exp.Sizeof (Typ.mk (Tarray (t_, None)), len, st)
| _ -> raise (Failure "expand_hpred_pointer: Unexpected non-sizeof type in Lindex") in | _ -> raise (Failure "expand_hpred_pointer: Unexpected non-sizeof type in Lindex") in
let len = match t' with let len = match t' with
| Exp.Sizeof (_, Some len, _) -> len | Exp.Sizeof (_, Some len, _) -> len
@ -1547,7 +1548,7 @@ struct
(** check that t1 and t2 are the same primitive type *) (** check that t1 and t2 are the same primitive type *)
let check_subtype_basic_type t1 t2 = let check_subtype_basic_type t1 t2 =
match t2 with match t2.Typ.desc with
| Typ.Tint Typ.IInt | Typ.Tint Typ.IBool | Typ.Tint Typ.IInt | Typ.Tint Typ.IBool
| Typ.Tint Typ.IChar | Typ.Tfloat Typ.FDouble | Typ.Tint Typ.IChar | Typ.Tfloat Typ.FDouble
| Typ.Tfloat Typ.FFloat | Typ.Tint Typ.ILong | Typ.Tfloat Typ.FFloat | Typ.Tint Typ.ILong
@ -1556,7 +1557,7 @@ struct
(** check if t1 is a subtype of t2, in Java *) (** check if t1 is a subtype of t2, in Java *)
let rec check_subtype_java tenv (t1: Typ.t) (t2: Typ.t) = let rec check_subtype_java tenv (t1: Typ.t) (t2: Typ.t) =
match t1, t2 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 (dom_type1, _), Tarray (dom_type2, _) ->
@ -1580,7 +1581,7 @@ struct
| _ -> false | _ -> false
let rec case_analysis_type tenv ((t1: Typ.t), st1) ((t2: Typ.t), st2) = let rec case_analysis_type tenv ((t1: Typ.t), st1) ((t2: Typ.t), st2) =
match t1, t2 with match t1.desc, t2.desc with
| Tstruct (JavaClass _ as cn1), Tstruct (JavaClass _ as cn2) -> | Tstruct (JavaClass _ as cn1), Tstruct (JavaClass _ as cn2) ->
Subtype.case_analysis tenv (cn1, st1) (cn2, st2) Subtype.case_analysis tenv (cn1, st1) (cn2, st2)
| Tstruct (JavaClass _ as cn1), Tarray _ | Tstruct (JavaClass _ as cn1), Tarray _
@ -1642,7 +1643,7 @@ let cast_exception tenv texp1 texp2 e1 subs =
Note: [pname] wil never be included in the returned result *) Note: [pname] wil never be included in the returned result *)
let get_overrides_of tenv supertype pname = let get_overrides_of tenv supertype pname =
let typ_has_method pname (typ: Typ.t) = let typ_has_method pname (typ: Typ.t) =
match typ with match typ.desc with
| Tstruct name -> ( | Tstruct name -> (
match Tenv.lookup tenv name with match Tenv.lookup tenv name with
| Some { methods } -> | Some { methods } ->
@ -1652,7 +1653,7 @@ let get_overrides_of tenv supertype pname =
) )
| _ -> false in | _ -> false in
let gather_overrides tname _ overrides_acc = let gather_overrides tname _ overrides_acc =
let typ = Typ.Tstruct tname in let typ = Typ.mk (Tstruct tname) in (* TODO shouldn't really create type here...*)
(* get all types in the type environment that are non-reflexive subtypes of [supertype] *) (* get all types in the type environment that are non-reflexive subtypes of [supertype] *)
if not (Typ.equal typ supertype) && Subtyping_check.check_subtype tenv typ supertype then if not (Typ.equal typ supertype) && Subtyping_check.check_subtype tenv typ supertype then
(* only select the ones that implement [pname] as overrides *) (* only select the ones that implement [pname] as overrides *)
@ -1677,7 +1678,7 @@ let texp_imply tenv subs texp1 texp2 e1 calc_missing =
let types_subject_to_dynamic_cast = let types_subject_to_dynamic_cast =
match texp1, texp2 with match texp1, texp2 with
| Exp.Sizeof (typ1, _, _), Exp.Sizeof (typ2, _, _) -> ( | Exp.Sizeof (typ1, _, _), Exp.Sizeof (typ2, _, _) -> (
match typ1, typ2 with match typ1.desc, typ2.desc with
| (Tstruct _ | Tarray _), (Tstruct _ | Tarray _) -> | (Tstruct _ | Tarray _), (Tstruct _ | Tarray _) ->
is_java_class tenv typ1 is_java_class tenv typ1
|| (Typ.is_cpp_class typ1 && Typ.is_cpp_class typ2) || (Typ.is_cpp_class typ1 && Typ.is_cpp_class typ2)
@ -1742,7 +1743,7 @@ let handle_parameter_subtype tenv prop1 sigma2 subs (e1, se1, texp1) (se2, texp2
| _ -> false in | _ -> false in
if List.exists ~f:filter sigma2 then !sub_opt else None in if List.exists ~f:filter sigma2 then !sub_opt else None in
let add_subtype () = match texp1, texp2, se1, se2 with let add_subtype () = match texp1, texp2, se1, se2 with
| Exp.Sizeof (Tptr (t1, _), None, _), Exp.Sizeof (Tptr (t2, _), None, _), | Exp.Sizeof ({desc=Tptr (t1, _)}, None, _), Exp.Sizeof ({desc=Tptr (t2, _)}, None, _),
Sil.Eexp (e1', _), Sil.Eexp (e2', _) Sil.Eexp (e1', _), Sil.Eexp (e2', _)
when not (is_allocated_lhs e1') -> when not (is_allocated_lhs e1') ->
begin begin
@ -1783,7 +1784,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
(match Prop.prop_iter_current tenv iter1' with (match Prop.prop_iter_current tenv iter1' with
| Sil.Hpointsto (e1, se1, texp1), _ -> | Sil.Hpointsto (e1, se1, texp1), _ ->
(try (try
let typ2 = Exp.texp_to_typ (Some Typ.Tvoid) texp2 in let typ2 = Exp.texp_to_typ (Some (Typ.mk Tvoid)) texp2 in
let typing_frame, typing_missing = texp_imply tenv subs texp1 texp2 e1 calc_missing in let typing_frame, typing_missing = texp_imply tenv subs texp1 texp2 e1 calc_missing in
let se1' = sexp_imply_preprocess se1 texp1 se2 in let se1' = sexp_imply_preprocess se1 texp1 se2 in
let subs', fld_frame, fld_missing = sexp_imply tenv e1 calc_index_frame calc_missing subs se1' se2 typ2 in let subs', fld_frame, fld_missing = sexp_imply tenv e1 calc_index_frame calc_missing subs se1' se2 typ2 in
@ -1988,10 +1989,10 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
let const_string_texp = let const_string_texp =
match !Config.curr_language with match !Config.curr_language with
| Config.Clang -> | Config.Clang ->
Exp.Sizeof (Typ.Tarray (Typ.Tint Typ.IChar, Some len), None, Subtype.exact) Exp.Sizeof (Typ.mk (Tarray (Typ.mk (Tint Typ.IChar), Some len)), None, Subtype.exact)
| Config.Java -> | Config.Java ->
let object_type = Typ.Name.Java.from_string "java.lang.String" in let object_type = Typ.Name.Java.from_string "java.lang.String" in
Exp.Sizeof (Tstruct object_type, None, Subtype.exact) in Exp.Sizeof (Typ.mk (Tstruct object_type), None, Subtype.exact) in
Sil.Hpointsto (root, sexp, const_string_texp) in Sil.Hpointsto (root, sexp, const_string_texp) in
let mk_constant_class_hpred s = (* creat an hpred from a constant class *) let mk_constant_class_hpred s = (* creat an hpred from a constant class *)
let root = Exp.Const (Const.Cclass (Ident.string_to_name s)) in let root = Exp.Const (Const.Cclass (Ident.string_to_name s)) in
@ -2001,7 +2002,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
Sil.Eexp ((Exp.Const (Const.Cstr s), Sil.Inone)))], Sil.inst_none) in Sil.Eexp ((Exp.Const (Const.Cstr s), Sil.Inone)))], Sil.inst_none) in
let class_texp = let class_texp =
let class_type = Typ.Name.Java.from_string "java.lang.Class" in let class_type = Typ.Name.Java.from_string "java.lang.Class" in
Exp.Sizeof (Tstruct class_type, None, Subtype.exact) in Exp.Sizeof (Typ.mk (Tstruct class_type), None, Subtype.exact) in
Sil.Hpointsto (root, sexp, class_texp) in Sil.Hpointsto (root, sexp, class_texp) in
try try
(match move_primed_lhs_from_front subs sigma2 with (match move_primed_lhs_from_front subs sigma2 with
@ -2036,7 +2037,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
| None -> | None ->
let subs' = match hpred2' with let subs' = match hpred2' with
| Sil.Hpointsto (e2, se2, te2) -> | Sil.Hpointsto (e2, se2, te2) ->
let typ2 = Exp.texp_to_typ (Some Typ.Tvoid) te2 in let typ2 = Exp.texp_to_typ (Some (Typ.mk Tvoid)) te2 in
sexp_imply_nolhs tenv e2 calc_missing subs se2 typ2 sexp_imply_nolhs tenv e2 calc_missing subs se2 typ2
| _ -> subs in | _ -> subs in
ProverState.add_missing_sigma [hpred2']; ProverState.add_missing_sigma [hpred2'];

@ -100,7 +100,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
L.d_str "create_struct_values type:"; Typ.d_full t; L.d_str "create_struct_values type:"; Typ.d_full t;
L.d_str " off: "; Sil.d_offset_list off; L.d_ln(); L.d_str " off: "; Sil.d_offset_list off; L.d_ln();
raise (Exceptions.Bad_footprint pos) in raise (Exceptions.Bad_footprint pos) in
match t, off with match t.desc, off with
| Tstruct _, [] -> | Tstruct _, [] ->
([], Sil.Estruct ([], inst), t) ([], Sil.Estruct ([], inst), t)
| Tstruct name, (Off_fld (f, _)) :: off' -> ( | Tstruct name, (Off_fld (f, _)) :: off' -> (
@ -133,7 +133,7 @@ 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.Tarray (res_t', None) in let res_t = Typ.mk (Tarray (res_t', None)) in
(Sil.Aeq (e, e') :: atoms', se, res_t) (Sil.Aeq (e, e') :: atoms', se, res_t)
| Tarray (t', len_), off -> | Tarray (t', len_), off ->
let len = match len_ with let len = match len_ with
@ -149,7 +149,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
pname tenv orig_prop footprint_part kind max_stamp t' off' inst in pname tenv orig_prop footprint_part kind max_stamp t' off' inst 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.Tarray (res_t', len_) in let res_t = Typ.mk ~default:t (Tarray (res_t', len_)) 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
@ -159,16 +159,16 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
([], Sil.Eexp (Exp.Var id, inst), t) ([], Sil.Eexp (Exp.Var id, inst), t)
| (Tint _ | Tfloat _ | Tvoid | Tfun _ | Tptr _), (Off_index e) :: off' -> | (Tint _ | Tfloat _ | Tvoid | Tfun _ | Tptr _), (Off_index e) :: off' ->
(* In this case, we lift t to the t array. *) (* In this case, we lift t to the t array. *)
let t' = match t with let t', mk_typ_f = match t.Typ.desc with
| Typ.Tptr(t', _) -> t' | Typ.Tptr(t', _) -> t', (function desc -> Typ.mk ~default:t desc)
| _ -> t in | _ -> t, fun desc -> Typ.mk desc in
let len = Exp.Var (new_id ()) in let len = Exp.Var (new_id ()) in
let atoms', se', res_t' = let atoms', se', res_t' =
create_struct_values create_struct_values
pname tenv orig_prop footprint_part kind max_stamp t' off' inst in pname tenv orig_prop footprint_part kind max_stamp t' off' inst 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.Tarray (res_t', None) in let res_t = mk_typ_f (Tarray (res_t', None)) in
(Sil.Aeq(e, e') :: atoms', se, res_t) (Sil.Aeq(e, e') :: atoms', se, res_t)
| Tint _, _ | Tfloat _, _ | Tvoid, _ | Tfun _, _ | Tptr _, _ -> | Tint _, _ | Tfloat _, _ | Tvoid, _ | Tfun _, _ | Tptr _, _ ->
fail t off __POS__ fail t off __POS__
@ -194,7 +194,7 @@ let rec _strexp_extend_values
let new_id () = let new_id () =
incr max_stamp; incr max_stamp;
Ident.create kind !max_stamp in Ident.create kind !max_stamp in
match off, se, typ with match off, se, typ.desc with
| [], Sil.Eexp _, _ | [], Sil.Eexp _, _
| [], Sil.Estruct _, _ -> | [], Sil.Estruct _, _ ->
[([], se, typ)] [([], se, typ)]
@ -261,7 +261,7 @@ let rec _strexp_extend_values
if Config.type_size then Exp.one (* Exp.Sizeof (typ, Subtype.exact) *) if Config.type_size then Exp.one (* Exp.Sizeof (typ, Subtype.exact) *)
else Exp.Var (new_id ()) in else Exp.Var (new_id ()) 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.Tarray (typ, None) in let typ_new = Typ.mk (Tarray (typ, None)) in
_strexp_extend_values _strexp_extend_values
pname tenv orig_prop footprint_part kind max_stamp se_new typ_new off inst pname tenv orig_prop footprint_part kind max_stamp se_new typ_new off inst
| (Off_index e) :: off', Sil.Earray (len, esel, inst_arr), Tarray (typ', len_for_typ') -> ( | (Off_index e) :: off', Sil.Earray (len, esel, inst_arr), Tarray (typ', len_for_typ') -> (
@ -277,7 +277,7 @@ let rec _strexp_extend_values
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.Tarray (res_typ', len_for_typ') ) , Typ.mk ~default:typ (Tarray (res_typ', len_for_typ')) )
:: acc :: acc
else else
raise (Exceptions.Bad_footprint __POS__) in raise (Exceptions.Bad_footprint __POS__) in
@ -286,7 +286,7 @@ let rec _strexp_extend_values
array_case_analysis_index pname tenv orig_prop array_case_analysis_index pname tenv orig_prop
footprint_part kind max_stamp footprint_part kind max_stamp
len esel len esel
len_for_typ' typ' len_for_typ' typ' typ
e off' inst_arr inst e off' inst_arr inst
) )
| _, _, _ -> | _, _, _ ->
@ -295,7 +295,7 @@ let rec _strexp_extend_values
and array_case_analysis_index pname tenv orig_prop and array_case_analysis_index pname tenv orig_prop
footprint_part kind max_stamp footprint_part kind max_stamp
array_len array_cont array_len array_cont
typ_array_len typ_cont typ_array_len typ_cont typ_array
index off inst_arr inst index off inst_arr inst
= =
let check_sound t' = let check_sound t' =
@ -310,7 +310,7 @@ and array_case_analysis_index pname tenv orig_prop
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.Tarray (typ_cont, typ_array_len) in let typ_default = Typ.mk ~default:typ_array (Tarray (typ_cont, typ_array_len)) in
[([], array_default, typ_default)] [([], array_default, typ_default)]
else if !Config.footprint then begin else if !Config.footprint then begin
let atoms, elem_se, elem_typ = let atoms, elem_se, elem_typ =
@ -319,7 +319,7 @@ and array_case_analysis_index pname tenv orig_prop
check_sound elem_typ; check_sound elem_typ;
let cont_new = List.sort ~cmp:[%compare: Exp.t * Sil.strexp] ((index, elem_se):: array_cont) in let cont_new = List.sort ~cmp:[%compare: Exp.t * Sil.strexp] ((index, elem_se):: array_cont) 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.Tarray (elem_typ, typ_array_len) in let typ_new = Typ.mk ~default:typ_array (Tarray (elem_typ, typ_array_len)) in
[(atoms, array_new, typ_new)] [(atoms, array_new, typ_new)]
end end
else begin else begin
@ -333,7 +333,7 @@ and array_case_analysis_index pname tenv orig_prop
let cont_new = let cont_new =
List.sort ~cmp:[%compare: Exp.t * Sil.strexp] ((index, elem_se):: array_cont) in List.sort ~cmp:[%compare: Exp.t * Sil.strexp] ((index, elem_se):: array_cont) 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.Tarray (elem_typ, typ_array_len) in let typ_new = Typ.mk ~default:typ_array (Tarray (elem_typ, typ_array_len)) in
[(atoms, array_new, typ_new)] [(atoms, array_new, typ_new)]
end in end in
let rec handle_case acc isel_seen_rev = function let rec handle_case acc isel_seen_rev = function
@ -349,7 +349,7 @@ and array_case_analysis_index pname tenv orig_prop
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.Tarray (typ', typ_array_len) in let typ_new = Typ.mk ~default:typ_array (Tarray (typ', typ_array_len)) in
(atoms_new, array_new, typ_new):: acc') (atoms_new, array_new, typ_new):: acc')
~init:[] ~init:[]
atoms_se_typ_list in atoms_se_typ_list in
@ -443,7 +443,7 @@ let mk_ptsto_exp_footprint
let st = match !Config.curr_language with let st = match !Config.curr_language with
| Config.Clang -> Subtype.exact | Config.Clang -> Subtype.exact
| Config.Java -> Subtype.subtypes in | Config.Java -> Subtype.subtypes in
let create_ptsto footprint_part off0 = match root, off0, typ with let create_ptsto footprint_part off0 = match root, off0, typ.Typ.desc with
| Exp.Lvar pvar, [], Typ.Tfun _ -> | Exp.Lvar pvar, [], Typ.Tfun _ ->
let fun_name = Typ.Procname.from_string_c_fun (Mangled.to_string (Pvar.get_name pvar)) in let fun_name = Typ.Procname.from_string_c_fun (Mangled.to_string (Pvar.get_name pvar)) in
let fun_exp = Exp.Const (Const.Cfun fun_name) in let fun_exp = Exp.Const (Const.Cfun fun_name) in
@ -738,7 +738,7 @@ let add_guarded_by_constraints tenv prop lexp pdesc =
let match_on_field_type typ flds = let match_on_field_type typ flds =
match String.rsplit2 guarded_by_str0 ~on:'.' with match String.rsplit2 guarded_by_str0 ~on:'.' with
| Some (class_part, field_part) -> | Some (class_part, field_part) ->
let typ_matches_guarded_by _ = function let typ_matches_guarded_by _ {Typ.desc} = match desc with
| Typ.Tptr (ptr_typ, _) -> | Typ.Tptr (ptr_typ, _) ->
String.is_suffix ~suffix:class_part (Typ.to_string ptr_typ); String.is_suffix ~suffix:class_part (Typ.to_string ptr_typ);
| _ -> | _ ->
@ -763,35 +763,35 @@ let add_guarded_by_constraints tenv prop lexp pdesc =
List.find_map List.find_map
~f:(function [@warning "-57"] (* FIXME: silenced warning may be legit *) ~f:(function [@warning "-57"] (* FIXME: silenced warning may be legit *)
| Sil.Hpointsto ((Const (Cclass clazz) as lhs_exp), _, Exp.Sizeof (typ, _, _)) | Sil.Hpointsto ((Const (Cclass clazz) as lhs_exp), _, Exp.Sizeof (typ, _, _))
| Sil.Hpointsto (_, Sil.Eexp (Const (Cclass clazz) as lhs_exp, _), Exp.Sizeof (typ, _, _)) | Sil.Hpointsto (_, Sil.Eexp (Const (Cclass clazz) as lhs_exp, _), Exp.Sizeof (typ, _, _))
when guarded_by_str_is_class guarded_by_str0 (Ident.name_to_string clazz) -> when guarded_by_str_is_class guarded_by_str0 (Ident.name_to_string clazz) ->
Some (Sil.Eexp (lhs_exp, Sil.inst_none), typ) Some (Sil.Eexp (lhs_exp, Sil.inst_none), typ)
| Sil.Hpointsto (_, Estruct (flds, _), Exp.Sizeof (typ, _, _)) -> | Sil.Hpointsto (_, Estruct (flds, _), Exp.Sizeof (typ, _, _)) ->
begin begin
(* first, try to find a field that exactly matches the guarded-by string *) (* first, try to find a field that exactly matches the guarded-by string *)
match get_fld_strexp_and_typ typ (is_guarded_by_fld guarded_by_str0) flds with match get_fld_strexp_and_typ typ (is_guarded_by_fld guarded_by_str0) flds with
| None when guarded_by_str_is_this guarded_by_str0 -> | None when guarded_by_str_is_this guarded_by_str0 ->
(* if the guarded-by string is "OuterClass.this", look for "this$n" for some n. (* if the guarded-by string is "OuterClass.this", look for "this$n" for some n.
note that this is a bit sketchy when there are mutliple this$n's, but there's note that this is a bit sketchy when there are mutliple this$n's, but there's
nothing we can do to disambiguate them. *) nothing we can do to disambiguate them. *)
get_fld_strexp_and_typ get_fld_strexp_and_typ
typ typ
(fun f _ -> Fieldname.java_is_outer_instance f) (fun f _ -> Fieldname.java_is_outer_instance f)
flds flds
| None -> | None ->
(* can't find an exact match. try a different convention. *) (* can't find an exact match. try a different convention. *)
match_on_field_type typ flds match_on_field_type typ flds
| Some _ as res_opt -> | Some _ as res_opt ->
res_opt res_opt
end end
| Sil.Hpointsto (Lvar pvar, rhs_exp, Exp.Sizeof (typ, _, _)) | Sil.Hpointsto (Lvar pvar, rhs_exp, Exp.Sizeof (typ, _, _))
when (guarded_by_str_is_current_class_this guarded_by_str0 pname || when (guarded_by_str_is_current_class_this guarded_by_str0 pname ||
guarded_by_str_is_super_class_this guarded_by_str0 pname guarded_by_str_is_super_class_this guarded_by_str0 pname
) && Pvar.is_this pvar -> ) && Pvar.is_this pvar ->
Some (rhs_exp, typ) Some (rhs_exp, typ)
| _ -> | _ ->
None) None)
sigma in sigma in
(* warn if the access to [lexp] is not protected by the [guarded_by_fld_str] lock *) (* warn if the access to [lexp] is not protected by the [guarded_by_fld_str] lock *)
let enforce_guarded_access_ accessed_fld guarded_by_str prop = let enforce_guarded_access_ accessed_fld guarded_by_str prop =
@ -814,7 +814,7 @@ let add_guarded_by_constraints tenv prop lexp pdesc =
let rec is_read_write_lock typ = let rec is_read_write_lock typ =
let str_is_read_write_lock str = String.is_suffix ~suffix:"ReadWriteUpdateLock" str || let str_is_read_write_lock str = String.is_suffix ~suffix:"ReadWriteUpdateLock" str ||
String.is_suffix ~suffix:"ReadWriteLock" str in String.is_suffix ~suffix:"ReadWriteLock" str in
match typ with match typ.Typ.desc with
| Typ.Tstruct name -> str_is_read_write_lock (Typ.Name.name name) | Typ.Tstruct name -> str_is_read_write_lock (Typ.Name.name name)
| Typ.Tptr (typ, _) -> is_read_write_lock typ | Typ.Tptr (typ, _) -> is_read_write_lock typ
| _ -> false in | _ -> false in
@ -1128,7 +1128,7 @@ let iter_rearrange_pe_dllseg_last tenv recurse_on_iters default_case_iter iter p
(** find the type at the offset from the given type expression, if any *) (** find the type at the offset from the given type expression, if any *)
let type_at_offset tenv texp off = let type_at_offset tenv texp off =
let rec strip_offset (off: Sil.offset list) (typ: Typ.t) = let rec strip_offset (off: Sil.offset list) (typ: Typ.t) =
match off, typ with match off, typ.desc with
| [], _ -> Some typ | [], _ -> Some typ
| (Off_fld (f, _)) :: off', Tstruct name -> ( | (Off_fld (f, _)) :: off', Tstruct name -> (
match Tenv.lookup tenv name with match Tenv.lookup tenv name with
@ -1184,22 +1184,22 @@ let rec iter_rearrange
inst: (Sil.offset list) Prop.prop_iter list = inst: (Sil.offset list) Prop.prop_iter list =
let rec root_typ_of_offsets = function let rec root_typ_of_offsets = function
| Sil.Off_fld (f, fld_typ) :: _ -> ( | Sil.Off_fld (f, fld_typ) :: _ -> (
match fld_typ with match fld_typ.desc with
| Tstruct _ as struct_typ -> | Tstruct _ ->
(* access through field: get the struct type from the field *) (* access through field: get the struct type from the field *)
if Config.trace_rearrange then begin if Config.trace_rearrange then begin
L.d_increase_indent 1; L.d_increase_indent 1;
L.d_str "iter_rearrange: root of lexp accesses field "; L.d_strln (Fieldname.to_string f); L.d_str "iter_rearrange: root of lexp accesses field "; L.d_strln (Fieldname.to_string f);
L.d_str " struct type from field: "; Typ.d_full struct_typ; L.d_ln(); L.d_str " struct type from field: "; Typ.d_full fld_typ; L.d_ln();
L.d_decrease_indent 1; L.d_decrease_indent 1;
L.d_ln(); L.d_ln();
end; end;
struct_typ fld_typ
| _ -> | _ ->
typ_from_instr typ_from_instr
) )
| Sil.Off_index _ :: off -> | Sil.Off_index _ :: off ->
Typ.Tarray (root_typ_of_offsets off, None) Typ.mk (Tarray (root_typ_of_offsets off, None))
| _ -> | _ ->
typ_from_instr in typ_from_instr in
let typ = root_typ_of_offsets (Sil.exp_get_offsets lexp) in let typ = root_typ_of_offsets (Sil.exp_get_offsets lexp) in
@ -1286,7 +1286,7 @@ let is_weak_captured_var pdesc var_name =
match pname with match pname with
| Block _ -> | Block _ ->
let is_weak_captured (var, typ) = let is_weak_captured (var, typ) =
match typ with match typ.Typ.desc with
| Typ.Tptr (_, Pk_objc_weak) -> | Typ.Tptr (_, Pk_objc_weak) ->
String.equal var_name (Mangled.to_string var) String.equal var_name (Mangled.to_string var)
| _ -> false in | _ -> false in

@ -27,7 +27,7 @@ let unroll_type tenv (typ: Typ.t) (off: Sil.offset) =
L.d_str "Type : "; Typ.d_full typ; L.d_ln (); L.d_str "Type : "; Typ.d_full typ; L.d_ln ();
raise (Exceptions.Bad_footprint __POS__) raise (Exceptions.Bad_footprint __POS__)
in in
match (typ, off) with match (typ.desc, off) with
| Tstruct name, Off_fld (fld, _) -> ( | Tstruct name, Off_fld (fld, _) -> (
match Tenv.lookup tenv name with match Tenv.lookup tenv name with
| Some { fields; statics } -> ( | Some { fields; statics } -> (
@ -91,7 +91,7 @@ let rec apply_offlist
L.d_str "offlist : "; Sil.d_offset_list offlist; L.d_ln (); L.d_str "offlist : "; Sil.d_offset_list offlist; L.d_ln ();
L.d_str "type : "; Typ.d_full typ; L.d_ln (); L.d_str "type : "; Typ.d_full typ; L.d_ln ();
L.d_str "prop : "; Prop.d_prop p; L.d_ln (); L.d_ln () in L.d_str "prop : "; Prop.d_prop p; L.d_ln (); L.d_ln () in
match offlist, strexp, typ with match offlist, strexp, typ.Typ.desc with
| [], Sil.Eexp (e, inst_curr), _ -> | [], Sil.Eexp (e, inst_curr), _ ->
let inst_is_uninitialized = function let inst_is_uninitialized = function
| Sil.Ialloc -> | Sil.Ialloc ->
@ -183,7 +183,7 @@ let rec apply_offlist
then (idx_ese', res_se') then (idx_ese', res_se')
else ese in else ese 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.Tarray (res_t', len') in let res_t = Typ.mk ~default:typ (Tarray (res_t', len')) 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 *)
@ -520,7 +520,7 @@ let resolve_typename prop receiver_exp =
| _ :: hpreds -> loop hpreds in | _ :: hpreds -> loop hpreds in
loop prop.Prop.sigma in loop prop.Prop.sigma in
match typexp_opt with match typexp_opt with
| Some (Exp.Sizeof (Tstruct name, _, _)) -> Some name | Some (Exp.Sizeof ({desc=Tstruct name}, _, _)) -> Some name
| _ -> None | _ -> None
(** If the dynamic type of the receiver actual T_actual is a subtype of the reciever type T_formal (** If the dynamic type of the receiver actual T_actual is a subtype of the reciever type T_formal
@ -535,7 +535,7 @@ let resolve_virtual_pname tenv prop actuals callee_pname call_flags : Typ.Procna
begin begin
let name = Typ.Procname.java_get_class_type_name pname_java in let name = Typ.Procname.java_get_class_type_name pname_java in
match Tenv.lookup tenv name with match Tenv.lookup tenv name with
| Some _ -> Typ.Tptr (Tstruct name, Pk_pointer) | Some _ -> Typ.mk (Typ.Tptr (Typ.mk (Tstruct name), Pk_pointer))
| None -> fallback_typ | None -> fallback_typ
end end
| _ -> | _ ->
@ -855,7 +855,7 @@ let add_constraints_on_retval tenv pdesc prop ret_exp ~has_nullable_annot typ ca
then then
prop (* don't assume nonnull if the procedure is annotated with @Nullable *) prop (* don't assume nonnull if the procedure is annotated with @Nullable *)
else else
match typ with match typ.Typ.desc with
| Typ.Tptr _ -> Prop.conjoin_neq tenv exp Exp.zero prop | Typ.Tptr _ -> Prop.conjoin_neq tenv exp Exp.zero prop
| _ -> prop in | _ -> prop in
let add_tainted_post ret_exp callee_pname prop = let add_tainted_post ret_exp callee_pname prop =
@ -892,7 +892,7 @@ let add_taint prop lhs_id rhs_exp pname tenv =
else else
prop in prop in
match rhs_exp with match rhs_exp with
| Exp.Lfield (_, fieldname, (Tstruct typname | Tptr (Tstruct typname, _))) -> | Exp.Lfield (_, fieldname, ({desc=Tstruct typname} | {desc=Tptr ({desc=Tstruct typname}, _)})) ->
begin begin
match Tenv.lookup tenv typname with match Tenv.lookup tenv typname with
| Some struct_typ -> add_attribute_if_field_tainted prop fieldname struct_typ | Some struct_typ -> add_attribute_if_field_tainted prop fieldname struct_typ
@ -1309,8 +1309,8 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call
else else
if !Config.footprint then if !Config.footprint then
let prop', abduced_strexp = let prop', abduced_strexp =
match actual_typ with match actual_typ.Typ.desc with
| Typ.Tptr ((Tstruct _) as typ, _) -> | Typ.Tptr ({desc=Tstruct _} as typ, _) ->
(* for struct types passed by reference, do abduction on the fields of the (* for struct types passed by reference, do abduction on the fields of the
struct *) struct *)
add_struct_value_to_footprint tenv abduced_ref_pv typ prop add_struct_value_to_footprint tenv abduced_ref_pv typ prop
@ -1319,10 +1319,10 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call
let (prop', fresh_fp_var) = let (prop', fresh_fp_var) =
add_to_footprint tenv abduced_ref_pv typ prop in add_to_footprint tenv abduced_ref_pv typ prop in
prop', Sil.Eexp (fresh_fp_var, Sil.Inone) prop', Sil.Eexp (fresh_fp_var, Sil.Inone)
| typ -> | _ ->
failwith failwith
("No need for abduction on non-pointer type " ^ ("No need for abduction on non-pointer type " ^
(Typ.to_string typ)) in (Typ.to_string actual_typ)) in
(* replace [actual] |-> _ with [actual] |-> [fresh_fp_var] *) (* replace [actual] |-> _ with [actual] |-> [fresh_fp_var] *)
let filtered_sigma = let filtered_sigma =
List.map List.map
@ -1440,7 +1440,7 @@ and unknown_or_scan_call ~is_scan ret_type_option ret_annots
let actuals_by_ref = let actuals_by_ref =
List.filter_mapi List.filter_mapi
~f:(fun i actual -> match actual with ~f:(fun i actual -> match actual with
| (Exp.Lvar _ as e, (Typ.Tptr _ as t)) -> Some (e, t, i) | (Exp.Lvar _ as e, ({Typ.desc=Tptr _} as t)) -> Some (e, t, i)
| _ -> None) | _ -> None)
args in args in
let has_nullable_annot = Annotations.ia_is_nullable ret_annots in let has_nullable_annot = Annotations.ia_is_nullable ret_annots in
@ -1536,7 +1536,7 @@ and sym_exec_objc_getter field_name ret_typ tenv ret_id pdesc pname loc args pro
| Some (ret_id, _) -> ret_id | Some (ret_id, _) -> ret_id
| None -> assert false in | None -> assert false in
match args with match args with
| [(lexp, (Typ.Tstruct _ as typ | Tptr (Tstruct _ as typ, _)))] -> | [(lexp, ({Typ.desc=Tstruct _} as typ | {desc=Tptr ({desc=Tstruct _} as typ, _)}))] ->
let field_access_exp = Exp.Lfield (lexp, field_name, typ) in let field_access_exp = Exp.Lfield (lexp, field_name, typ) in
execute_load execute_load
~report_deref_errors:false pname pdesc tenv ret_id field_access_exp ret_typ loc prop ~report_deref_errors:false pname pdesc tenv ret_id field_access_exp ret_typ loc prop
@ -1546,7 +1546,7 @@ and sym_exec_objc_setter field_name _ tenv _ pdesc pname loc args prop =
L.d_strln ("No custom setter found. Executing the ObjC builtin setter with ivar "^ L.d_strln ("No custom setter found. Executing the ObjC builtin setter with ivar "^
(Fieldname.to_string field_name)^"."); (Fieldname.to_string field_name)^".");
match args with match args with
| (lexp1, (Typ.Tstruct _ as typ1 | Tptr (typ1, _))) :: (lexp2, typ2) :: _ -> | (lexp1, ({Typ.desc=Tstruct _} as typ1 | {Typ.desc=Tptr (typ1, _)})) :: (lexp2, typ2) :: _ ->
let field_access_exp = Exp.Lfield (lexp1, field_name, typ1) in let field_access_exp = Exp.Lfield (lexp1, field_name, typ1) in
execute_store ~report_deref_errors:false pname pdesc tenv field_access_exp typ2 lexp2 loc prop execute_store ~report_deref_errors:false pname pdesc tenv field_access_exp typ2 lexp2 loc prop
| _ -> raise (Exceptions.Wrong_argument_number __POS__) | _ -> raise (Exceptions.Wrong_argument_number __POS__)
@ -1570,7 +1570,7 @@ and proc_call summary {Builtin.pdesc; tenv; prop_= pre; path; ret_id; args= actu
let ret_typ = Specs.get_ret_type summary in let ret_typ = Specs.get_ret_type summary in
let check_return_value_ignored () = let check_return_value_ignored () =
(* check if the return value of the call is ignored, and issue a warning *) (* check if the return value of the call is ignored, and issue a warning *)
let is_ignored = match ret_typ, ret_id with let is_ignored = match ret_typ.Typ.desc, ret_id with
| Typ.Tvoid, _ -> false | Typ.Tvoid, _ -> false
| _, None -> true | _, None -> true
| _, Some (id, _) -> Errdesc.id_is_assigned_then_dead (State.get_node ()) id in | _, Some (id, _) -> Errdesc.id_is_assigned_then_dead (State.get_node ()) id in

@ -470,7 +470,7 @@ let texp_star tenv texp1 texp2 =
| 0 -> ftal_sub ftal1' ftal2' | 0 -> ftal_sub ftal1' ftal2'
| _ -> ftal_sub ftal1 ftal2' end in | _ -> ftal_sub ftal1 ftal2' end in
let typ_star (t1: Typ.t) (t2: Typ.t) = let typ_star (t1: Typ.t) (t2: Typ.t) =
match t1, t2 with match t1.desc, t2.desc with
| Tstruct name1, Tstruct name2 | Tstruct name1, Tstruct name2
when Typ.Name.is_same_type name1 name2 -> ( when Typ.Name.is_same_type name1 name2 -> (
match Tenv.lookup tenv name1, Tenv.lookup tenv name2 with match Tenv.lookup tenv name1, Tenv.lookup tenv name2 with
@ -634,7 +634,7 @@ let prop_get_exn_name pname prop =
let ret_pvar = Exp.Lvar (Pvar.get_ret_pvar pname) in let ret_pvar = Exp.Lvar (Pvar.get_ret_pvar pname) in
let rec search_exn e = function let rec search_exn e = function
| [] -> None | [] -> None
| Sil.Hpointsto (e1, _, Sizeof (Tstruct name, _, _)) :: _ | Sil.Hpointsto (e1, _, Sizeof ({desc=Tstruct name}, _, _)) :: _
when Exp.equal e1 e -> when Exp.equal e1 e ->
Some name Some name
| _ :: tl -> search_exn e tl in | _ :: tl -> search_exn e tl in

@ -41,7 +41,7 @@ struct
| Exp.BinOp (Binop.Mult, Exp.Sizeof (typ, _, _), size) | Exp.BinOp (Binop.Mult, Exp.Sizeof (typ, _, _), size)
| Exp.BinOp (Binop.Mult, size, Exp.Sizeof (typ, _, _)) -> (typ, size) | Exp.BinOp (Binop.Mult, size, Exp.Sizeof (typ, _, _)) -> (typ, size)
| Exp.Sizeof (typ, _, _) -> (typ, Exp.one) | Exp.Sizeof (typ, _, _) -> (typ, Exp.one)
| x -> (Typ.Tint Typ.IChar, x) | x -> (Typ.mk (Tint Typ.IChar), x)
let model_malloc let model_malloc
: Typ.Procname.t -> (Ident.t * Typ.t) option -> (Exp.t * Typ.t) list -> CFG.node : Typ.Procname.t -> (Ident.t * Typ.t) option -> (Exp.t * Typ.t) list -> CFG.node
@ -50,7 +50,7 @@ struct
match ret with match ret with
| Some (id, _) -> | Some (id, _) ->
let set_uninitialized typ loc mem = let set_uninitialized typ loc mem =
match typ with match typ.Typ.desc with
| Typ.Tint _ | Typ.Tint _
| Typ.Tfloat _ -> | Typ.Tfloat _ ->
Dom.Mem.weak_update_heap loc Dom.Val.top_itv mem Dom.Mem.weak_update_heap loc Dom.Val.top_itv mem
@ -125,7 +125,7 @@ struct
let loc = let loc =
Loc.of_allocsite (Sem.get_allocsite pname node inst_num dimension) Loc.of_allocsite (Sem.get_allocsite pname node inst_num dimension)
in in
match typ with match typ.Typ.desc with
| Typ.Tarray (typ, Some len) -> | Typ.Tarray (typ, Some len) ->
declare_array pname node loc typ len ~inst_num declare_array pname node loc typ len ~inst_num
~dimension:(dimension + 1) mem ~dimension:(dimension + 1) mem
@ -152,7 +152,7 @@ struct
mem |> Dom.Mem.find_heap loc |> Dom.Val.get_all_locs |> PowLoc.choose mem |> Dom.Mem.find_heap loc |> Dom.Val.get_all_locs |> PowLoc.choose
in in
let field = Loc.append_field loc fn in let field = Loc.append_field loc fn in
match typ with match typ.Typ.desc with
| Typ.Tint _ | Typ.Tint _
| Typ.Tfloat _ -> | Typ.Tfloat _ ->
let v = Dom.Val.make_sym pname sym_num in let v = Dom.Val.make_sym pname sym_num in
@ -166,7 +166,7 @@ struct
(Dom.Mem.add_heap field v mem, sym_num + 4) (Dom.Mem.add_heap field v mem, sym_num + 4)
| _ -> (mem, sym_num) | _ -> (mem, sym_num)
in in
match typ with match typ.Typ.desc with
| Typ.Tstruct typename -> | Typ.Tstruct typename ->
(match Tenv.lookup tenv typename with (match Tenv.lookup tenv typename with
| Some str -> | Some str ->
@ -179,7 +179,7 @@ struct
= fun pdesc tenv node inst_num mem -> = fun pdesc tenv node inst_num mem ->
let pname = Procdesc.get_proc_name pdesc in let pname = Procdesc.get_proc_name pdesc in
let add_formal (mem, inst_num, sym_num) (pvar, typ) = let add_formal (mem, inst_num, sym_num) (pvar, typ) =
match typ with match typ.Typ.desc with
| Typ.Tint _ -> | Typ.Tint _ ->
let v = Dom.Val.make_sym pname sym_num in let v = Dom.Val.make_sym pname sym_num in
let mem = Dom.Mem.add_heap (Loc.of_pvar pvar) v mem in let mem = Dom.Mem.add_heap (Loc.of_pvar pvar) v mem in
@ -233,7 +233,7 @@ struct
= fun mem { pdesc; tenv; extras } node instr -> = fun mem { pdesc; tenv; extras } node instr ->
let pname = Procdesc.get_proc_name pdesc in let pname = Procdesc.get_proc_name pdesc in
let try_decl_arr (mem, inst_num) (pvar, typ) = let try_decl_arr (mem, inst_num) (pvar, typ) =
match typ with match typ.Typ.desc with
| Typ.Tarray (typ, Some len) -> | Typ.Tarray (typ, Some len) ->
let loc = Loc.of_var (Var.of_pvar pvar) in let loc = Loc.of_var (Var.of_pvar pvar) in
let mem = let mem =

@ -43,15 +43,15 @@ struct
| Typ.FDouble | Typ.FLongDouble -> 8 | Typ.FDouble | Typ.FLongDouble -> 8
(* NOTE: assume 32bit machine *) (* NOTE: assume 32bit machine *)
let rec sizeof : Typ.t -> int let rec sizeof (typ : Typ.t) : int =
= function match typ.desc with
| Typ.Tint ikind -> sizeof_ikind ikind | Typ.Tint ikind -> sizeof_ikind ikind
| Typ.Tfloat fkind -> sizeof_fkind fkind | Typ.Tfloat fkind -> sizeof_fkind fkind
| Typ.Tvoid -> 1 | Typ.Tvoid -> 1
| Typ.Tptr (_, _) -> 4 | Typ.Tptr (_, _) -> 4
| Typ.Tstruct _ -> 4 (* TODO *) | Typ.Tstruct _ -> 4 (* TODO *)
| Typ.Tarray (typ, Some ilit) -> sizeof typ * IntLit.to_int ilit | Typ.Tarray (typ, Some ilit) -> sizeof typ * IntLit.to_int ilit
| _ -> 4 | _ -> 4
let rec must_alias : Exp.t -> Exp.t -> Mem.astate -> bool let rec must_alias : Exp.t -> Exp.t -> Mem.astate -> bool
= fun e1 e2 m -> = fun e1 e2 m ->
@ -372,8 +372,8 @@ struct
add_pair_val v1' v2' pairs add_pair_val v1' v2' pairs
in in
let add_pair_ptr typ v1 v2 pairs = let add_pair_ptr typ v1 v2 pairs =
match typ with match typ.Typ.desc with
| Typ.Tptr (Typ.Tstruct typename, _) -> | Typ.Tptr ({desc=Tstruct typename}, _) ->
(match Tenv.lookup tenv typename with (match Tenv.lookup tenv typename with
| Some str -> | Some str ->
let fns = List.map ~f:get_field_name str.Typ.Struct.fields in let fns = List.map ~f:get_field_name str.Typ.Struct.fields in

@ -192,7 +192,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let is_safe_access access prefix_path tenv = let is_safe_access access prefix_path tenv =
match access, AccessPath.Raw.get_typ prefix_path tenv with match access, AccessPath.Raw.get_typ prefix_path tenv with
| AccessPath.FieldAccess fieldname, | AccessPath.FieldAccess fieldname,
Some (Typ.Tstruct typename | Tptr (Tstruct typename, _)) -> Some ({Typ.desc=Tstruct typename} | {desc=Tptr ({desc=Tstruct typename}, _)}) ->
begin begin
match Tenv.lookup tenv typename with match Tenv.lookup tenv typename with
| Some struct_typ -> | Some struct_typ ->
@ -257,7 +257,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
match List.rev accesses, match List.rev accesses,
AccessPath.Raw.get_typ (AccessPath.Raw.truncate access_path) tenv with AccessPath.Raw.get_typ (AccessPath.Raw.truncate access_path) tenv with
| AccessPath.FieldAccess fieldname :: _, | AccessPath.FieldAccess fieldname :: _,
Some (Typ.Tstruct typename | Tptr (Tstruct typename, _)) -> Some {Typ.desc=Tstruct typename | Tptr ({Typ.desc=Tstruct typename}, _)} ->
begin begin
match Tenv.lookup tenv typename with match Tenv.lookup tenv typename with
| Some struct_typ -> | Some struct_typ ->
@ -482,8 +482,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
is_annotated_synchronized base_typename container_field tenv is_annotated_synchronized base_typename container_field tenv
| [AccessPath.FieldAccess container_field] -> | [AccessPath.FieldAccess container_field] ->
begin begin
match base_typ with match base_typ.Typ.desc with
| Typ.Tstruct base_typename | Tptr (Tstruct base_typename, _) -> | Typ.Tstruct base_typename | Tptr ({Typ.desc=Tstruct base_typename}, _) ->
is_annotated_synchronized base_typename container_field tenv is_annotated_synchronized base_typename container_field tenv
| _ -> | _ ->
false false
@ -557,7 +557,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| Sil.Call (Some (ret_id, _), Const (Cfun callee_pname), | Sil.Call (Some (ret_id, _), Const (Cfun callee_pname),
(target_exp, target_typ) :: (Exp.Sizeof (cast_typ, _, _), _) :: _ , _, _) (target_exp, target_typ) :: (Exp.Sizeof (cast_typ, _, _), _) :: _ , _, _)
when Typ.Procname.equal callee_pname BuiltinDecl.__cast -> when Typ.Procname.equal callee_pname BuiltinDecl.__cast ->
let lhs_access_path = AccessPath.of_id ret_id (Typ.Tptr (cast_typ, Pk_pointer)) in let lhs_access_path = AccessPath.of_id ret_id (Typ.mk (Tptr (cast_typ, Pk_pointer))) in
let attribute_map = let attribute_map =
propagate_attributes propagate_attributes
lhs_access_path target_exp target_typ ~f_resolve_id astate.attribute_map extras in lhs_access_path target_exp target_typ ~f_resolve_id astate.attribute_map extras in
@ -710,7 +710,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
astate in astate in
begin begin
match ret_opt with match ret_opt with
| Some (_, (Typ.Tint ILong | Tfloat FDouble)) -> | Some (_, {Typ.desc=Tint ILong | Tfloat FDouble}) ->
(* writes to longs and doubles are not guaranteed to be atomic in Java, so don't (* writes to longs and doubles are not guaranteed to be atomic in Java, so don't
bother tracking whether a returned long or float value is functional *) bother tracking whether a returned long or float value is functional *)
astate_callee astate_callee

@ -112,7 +112,7 @@ let of_exp exp0 typ0 ~(f_resolve_id : Var.t -> Raw.t option) =
of_exp_ root_exp root_exp_typ (field_access :: accesses) acc of_exp_ root_exp root_exp_typ (field_access :: accesses) acc
| Exp.Lindex (root_exp, _) -> | Exp.Lindex (root_exp, _) ->
let array_access = ArrayAccess typ in let array_access = ArrayAccess typ in
let array_typ = Typ.Tarray (typ, None) in let array_typ = Typ.mk (Tarray (typ, None)) 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

@ -31,11 +31,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
astate astate
let exec_instr astate _ _ = function let exec_instr astate _ _ = function
| Sil.Store (_, Tptr _, rhs_exp, _) -> | Sil.Store (_, {desc=Tptr _}, rhs_exp, _) ->
add_address_taken_pvars rhs_exp astate add_address_taken_pvars rhs_exp astate
| Sil.Call (_, _, actuals, _, _) -> | Sil.Call (_, _, actuals, _, _) ->
let add_actual_by_ref astate_acc = function let add_actual_by_ref astate_acc = function
| actual_exp, Typ.Tptr _ -> add_address_taken_pvars actual_exp astate_acc | actual_exp, {Typ.desc=Tptr _} -> add_address_taken_pvars actual_exp astate_acc
| _ -> astate_acc in | _ -> astate_acc in
List.fold ~f:add_actual_by_ref ~init:astate actuals List.fold ~f:add_actual_by_ref ~init:astate actuals
| Sil.Store _ | Load _ | Prune _ | Nullify _ | Abstract _ | Remove_temps _ | Sil.Store _ | Load _ | Prune _ | Nullify _ | Abstract _ | Remove_temps _

@ -201,8 +201,8 @@ let callback_check_write_to_parcel_java
let expr_match () = Exp.is_this this_expr in let expr_match () = Exp.is_this this_expr in
let type_match () = let type_match () =
let class_name = Typ.Name.Java.from_string "android.os.Parcelable" in let class_name = Typ.Name.Java.from_string "android.os.Parcelable" in
match this_type with match this_type.Typ.desc with
| Typ.Tptr (Tstruct name, _) | Tstruct name -> | Typ.Tptr ({desc=Tstruct name}, _) | Tstruct name ->
PatternMatch.is_immediate_subtype tenv name class_name PatternMatch.is_immediate_subtype tenv name class_name
| _ -> false in | _ -> false in
method_match () && expr_match () && type_match () in method_match () && expr_match () && type_match () in
@ -213,8 +213,8 @@ let callback_check_write_to_parcel_java
proc_desc pname_java ["android.os.Parcel"] in proc_desc pname_java ["android.os.Parcel"] in
let parcel_constructors tenv typ = let parcel_constructors tenv typ =
match typ with match typ.Typ.desc with
| Typ.Tptr (Tstruct name, _) -> ( | Typ.Tptr ({desc=Tstruct name}, _) -> (
match Tenv.lookup tenv name with match Tenv.lookup tenv name with
| Some { methods } -> List.filter ~f:is_parcel_constructor methods | Some { methods } -> List.filter ~f:is_parcel_constructor methods
| None -> [] | None -> []
@ -325,11 +325,11 @@ let callback_monitor_nullcheck { Callbacks.proc_desc; idenv; summary } =
let formals = Procdesc.get_formals proc_desc in let formals = Procdesc.get_formals proc_desc in
let class_formals = let class_formals =
let is_class_type (p, typ) = let is_class_type (p, typ) =
match typ with match typ.Typ.desc with
| Typ.Tptr _ when String.equal (Mangled.to_string p) "this" -> | Typ.Tptr _ when String.equal (Mangled.to_string p) "this" ->
false (* no need to null check 'this' *) false (* no need to null check 'this' *)
| Typ.Tstruct _ -> true | Typ.Tstruct _ -> true
| Typ.Tptr (Typ.Tstruct _, _) -> true | Typ.Tptr ({desc=Tstruct _}, _) -> true
| _ -> false in | _ -> false in
List.filter ~f:is_class_type formals in List.filter ~f:is_class_type formals in
List.map ~f:fst class_formals) in List.map ~f:fst class_formals) in

@ -99,7 +99,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let kill_ret_id (id,_) = let kill_ret_id (id,_) =
Domain.kill_copies_with_var (Var.of_id id) astate in Domain.kill_copies_with_var (Var.of_id id) astate in
let kill_actuals_by_ref astate_acc = function let kill_actuals_by_ref astate_acc = function
| (Exp.Lvar pvar, Typ.Tptr _) -> Domain.kill_copies_with_var (Var.of_pvar pvar) astate_acc | (Exp.Lvar pvar, {Typ.desc=Tptr _}) -> Domain.kill_copies_with_var (Var.of_pvar pvar) astate_acc
| _ -> astate_acc in | _ -> astate_acc in
let astate' = Option.value_map ~f:kill_ret_id ~default:astate ret_id in let astate' = Option.value_map ~f:kill_ret_id ~default:astate ret_id in
if Config.curr_language_is Config.Java if Config.curr_language_is Config.Java

@ -26,8 +26,8 @@ let callback_fragment_retains_view_java
(* TODO: complain if onDestroyView is not defined, yet the Fragment has View fields *) (* TODO: complain if onDestroyView is not defined, yet the Fragment has View fields *)
(* TODO: handle fields nullified in callees in the same file *) (* TODO: handle fields nullified in callees in the same file *)
let is_on_destroy_view = String.equal (Typ.Procname.java_get_method pname_java) "onDestroyView" in let is_on_destroy_view = String.equal (Typ.Procname.java_get_method pname_java) "onDestroyView" in
let fld_typ_is_view = function let fld_typ_is_view typ = match typ.Typ.desc with
| Typ.Tptr (Tstruct tname, _) -> AndroidFramework.is_view tenv tname | Typ.Tptr ({desc=Tstruct tname}, _) -> AndroidFramework.is_view tenv tname
| _ -> false in | _ -> false in
(* is [fldname] a View type declared by [class_typename]? *) (* is [fldname] a View type declared by [class_typename]? *)
let is_declared_view_typ class_typename (fldname, fld_typ, _) = let is_declared_view_typ class_typename (fldname, fld_typ, _) =
@ -47,7 +47,7 @@ let callback_fragment_retains_view_java
~f:(fun (fname, fld_typ, _) -> ~f:(fun (fname, fld_typ, _) ->
if not (Fieldname.Set.mem fname fields_nullified) then if not (Fieldname.Set.mem fname fields_nullified) then
report_error report_error
(Tstruct class_typename) fname fld_typ summary proc_desc) (Typ.mk (Tstruct class_typename)) fname fld_typ summary proc_desc)
declared_view_fields declared_view_fields
| _ -> () | _ -> ()
end end

@ -25,8 +25,8 @@ type taint_spec = {
} }
let type_is_object typ = let type_is_object typ =
match typ with match typ.Typ.desc with
| Typ.Tptr (Tstruct name, _) -> Typ.Name.equal name Typ.Name.Java.java_lang_object | Tptr ({desc=Tstruct name}, _) -> Typ.Name.equal name Typ.Name.Java.java_lang_object
| _ -> false | _ -> false
let java_proc_name_with_class_method pn_java class_with_path method_name = let java_proc_name_with_class_method pn_java class_with_path method_name =
@ -74,8 +74,8 @@ let get_this_type proc_attributes = match proc_attributes.ProcAttributes.formals
| _ -> None | _ -> None
let type_get_direct_supertypes tenv (typ: Typ.t) = let type_get_direct_supertypes tenv (typ: Typ.t) =
match typ with match typ.desc with
| Tptr (Tstruct name, _) | Tptr ({desc=Tstruct name}, _)
| Tstruct name -> ( | Tstruct name -> (
match Tenv.lookup tenv name with match Tenv.lookup tenv name with
| Some { supers } -> supers | Some { supers } -> supers
@ -84,13 +84,13 @@ let type_get_direct_supertypes tenv (typ: Typ.t) =
| _ -> | _ ->
[] []
let type_get_class_name = function let type_get_class_name {Typ.desc} = match desc with
| Typ.Tptr (typ, _) -> Typ.name typ | Typ.Tptr (typ, _) -> Typ.name typ
| _ -> None | _ -> None
let type_get_annotation tenv (typ: Typ.t): Annot.Item.t option = let type_get_annotation tenv (typ: Typ.t): Annot.Item.t option =
match typ with match typ.desc with
| Tptr (Tstruct name, _) | Tptr ({desc=Tstruct name}, _)
| Tstruct name -> ( | Tstruct name -> (
match Tenv.lookup tenv name with match Tenv.lookup tenv name with
| Some { annots } -> Some annots | Some { annots } -> Some annots
@ -112,7 +112,7 @@ let type_has_supertype
let supers = type_get_direct_supertypes tenv typ in let supers = type_get_direct_supertypes tenv typ in
let match_supertype cn = let match_supertype cn =
let match_name () = Typ.Name.equal cn class_name in let match_name () = Typ.Name.equal cn class_name in
let has_indirect_supertype () = has_supertype (Typ.Tstruct cn) (Typ.Set.add typ visited) in let has_indirect_supertype () = has_supertype (Typ.mk (Tstruct cn)) (Typ.Set.add typ visited) in
(match_name () || has_indirect_supertype ()) in (match_name () || has_indirect_supertype ()) in
List.exists ~f:match_supertype supers in List.exists ~f:match_supertype supers in
has_supertype typ Typ.Set.empty has_supertype typ Typ.Set.empty
@ -121,7 +121,8 @@ let type_is_nested_in_direct_supertype tenv t n =
let is_nested_in cn1 cn2 = String.is_prefix ~prefix:(Typ.Name.name cn1 ^ "$") (Typ.Name.name cn2) in let is_nested_in cn1 cn2 = String.is_prefix ~prefix:(Typ.Name.name cn1 ^ "$") (Typ.Name.name cn2) in
List.exists ~f:(is_nested_in n) (type_get_direct_supertypes tenv t) List.exists ~f:(is_nested_in n) (type_get_direct_supertypes tenv t)
let rec get_type_name = function let rec get_type_name {Typ.desc} =
match desc with
| Typ.Tstruct name -> | Typ.Tstruct name ->
Typ.Name.name name Typ.Name.name name
| Typ.Tptr (t, _) -> get_type_name t | Typ.Tptr (t, _) -> get_type_name t
@ -130,8 +131,8 @@ let rec get_type_name = function
let get_field_type_name tenv let get_field_type_name tenv
(typ: Typ.t) (typ: Typ.t)
(fieldname: Fieldname.t): string option = (fieldname: Fieldname.t): string option =
match typ with match typ.desc with
| Tstruct name | Tptr (Tstruct name, _) -> ( | Tstruct name | Tptr ({desc=Tstruct name}, _) -> (
match Tenv.lookup tenv name with match Tenv.lookup tenv name with
| Some { fields } -> ( | Some { fields } -> (
match List.find match List.find
@ -245,10 +246,10 @@ let get_java_method_call_formal_signature = function
let type_is_class typ = let type_is_class typ =
match typ with match typ.Typ.desc with
| Typ.Tptr (Typ.Tstruct _, _) -> true | Tptr ({desc=Tstruct _}, _) -> true
| Typ.Tptr (Typ.Tarray _, _) -> true | Tptr ({desc=Tarray _}, _) -> true
| Typ.Tstruct _ -> true | Tstruct _ -> true
| _ -> false | _ -> false
let initializer_classes = let initializer_classes =
@ -349,7 +350,7 @@ let override_exists f tenv proc_name =
let type_name = Typ.Name.Java.from_string (Typ.Procname.java_get_class_name proc_name_java) in let type_name = Typ.Name.Java.from_string (Typ.Procname.java_get_class_name proc_name_java) in
List.exists List.exists
~f:(super_type_exists tenv) ~f:(super_type_exists tenv)
(type_get_direct_supertypes tenv (Typ.Tstruct type_name)) (type_get_direct_supertypes tenv (Typ.mk (Tstruct type_name)))
| _ -> | _ ->
false (* Only java supported at the moment *) false (* Only java supported at the moment *)

@ -14,15 +14,15 @@ open! IStd
module L = Logging module L = Logging
let add_pointer_to_typ typ = let add_pointer_to_typ typ =
Typ.Tptr(typ, Typ.Pk_pointer) Typ.mk (Tptr(typ, Typ.Pk_pointer))
let remove_pointer_to_typ typ = let remove_pointer_to_typ typ =
match typ with match typ.Typ.desc with
| Typ.Tptr(typ, Typ.Pk_pointer) -> typ | Typ.Tptr(typ, Typ.Pk_pointer) -> typ
| _ -> typ | _ -> typ
let objc_classname_of_type typ = let objc_classname_of_type typ =
match typ with match typ.Typ.desc with
| Typ.Tstruct name -> name | Typ.Tstruct name -> name
| Typ.Tfun _ -> Typ.Name.Objc.from_string CFrontend_config.objc_object | Typ.Tfun _ -> Typ.Name.Objc.from_string CFrontend_config.objc_object
| _ -> | _ ->
@ -31,8 +31,8 @@ let objc_classname_of_type typ =
Typ.Name.Objc.from_string "undefined" Typ.Name.Objc.from_string "undefined"
let is_class typ = let is_class typ =
match typ with match typ.Typ.desc with
| Typ.Tptr (Tstruct name, _) -> | Typ.Tptr ({desc=Tstruct name}, _) ->
String.equal (Typ.Name.name name) CFrontend_config.objc_class String.equal (Typ.Name.name name) CFrontend_config.objc_class
| _ -> false | _ -> false

@ -158,15 +158,16 @@ and get_superclass_list_cpp tenv decl =
let get_super_field super_decl = get_record_typename ~tenv super_decl in let get_super_field super_decl = get_record_typename ~tenv super_decl in
List.map ~f:get_super_field base_decls List.map ~f:get_super_field base_decls
and get_record_struct_type tenv definition_decl = and get_record_struct_type tenv definition_decl : Typ.t =
let open Clang_ast_t in let open Clang_ast_t in
match definition_decl with match definition_decl with
| ClassTemplateSpecializationDecl (_, _, _, type_ptr, _, _, record_decl_info, _, _) | ClassTemplateSpecializationDecl (_, _, _, type_ptr, _, _, record_decl_info, _, _)
| CXXRecordDecl (_, _, _, type_ptr, _, _, record_decl_info, _) | CXXRecordDecl (_, _, _, type_ptr, _, _, record_decl_info, _)
| RecordDecl (_, _, _, type_ptr, _, _, record_decl_info) -> | RecordDecl (_, _, _, type_ptr, _, _, record_decl_info) ->
let sil_typename = get_record_typename ~tenv definition_decl in let sil_typename = get_record_typename ~tenv definition_decl in
let sil_type = Typ.mk (Tstruct sil_typename) in
(match Tenv.lookup tenv sil_typename with (match Tenv.lookup tenv sil_typename with
| Some _ -> Typ.Tstruct sil_typename (* just reuse what is already in tenv *) | Some _ -> sil_type (* just reuse what is already in tenv *)
| None -> | None ->
let is_complete_definition = record_decl_info.Clang_ast_t.rdi_is_complete_definition in let is_complete_definition = record_decl_info.Clang_ast_t.rdi_is_complete_definition in
let extra_fields = let extra_fields =
@ -177,7 +178,7 @@ and get_record_struct_type tenv definition_decl =
if Typ.Name.Cpp.is_class sil_typename then Annot.Class.cpp if Typ.Name.Cpp.is_class sil_typename then Annot.Class.cpp
else Annot.Item.empty (* No annotations for structs *) in else Annot.Item.empty (* No annotations for structs *) in
if is_complete_definition then ( if is_complete_definition then (
CAst_utils.update_sil_types_map type_ptr (Typ.Tstruct sil_typename); CAst_utils.update_sil_types_map type_ptr sil_type;
let non_statics = get_struct_fields tenv definition_decl in let non_statics = get_struct_fields tenv definition_decl in
let fields = CGeneral_utils.append_no_duplicates_fields non_statics extra_fields in let fields = CGeneral_utils.append_no_duplicates_fields non_statics extra_fields in
let statics = [] in (* Note: We treat static field same as global variables *) let statics = [] in (* Note: We treat static field same as global variables *)
@ -186,16 +187,14 @@ and get_record_struct_type tenv definition_decl =
let specialization = get_template_specialization tenv definition_decl in let specialization = get_template_specialization tenv definition_decl in
Tenv.mk_struct tenv ~fields ~statics ~methods ~supers ~annots ~specialization Tenv.mk_struct tenv ~fields ~statics ~methods ~supers ~annots ~specialization
sil_typename |> ignore; sil_typename |> ignore;
let sil_type = Typ.Tstruct sil_typename in
CAst_utils.update_sil_types_map type_ptr sil_type; CAst_utils.update_sil_types_map type_ptr sil_type;
sil_type sil_type
) else ( ) else (
(* There is no definition for that struct in whole translation unit. (* There is no definition for that struct in whole translation unit.
Put empty struct into tenv to prevent backend problems *) Put empty struct into tenv to prevent backend problems *)
ignore (Tenv.mk_struct tenv ~fields:extra_fields sil_typename); ignore (Tenv.mk_struct tenv ~fields:extra_fields sil_typename);
let tvar_type = Typ.Tstruct sil_typename in CAst_utils.update_sil_types_map type_ptr sil_type;
CAst_utils.update_sil_types_map type_ptr tvar_type; sil_type))
tvar_type))
| _ -> assert false | _ -> assert false
and add_types_from_decl_to_tenv tenv decl = and add_types_from_decl_to_tenv tenv decl =
@ -220,8 +219,8 @@ let get_type_from_expr_info ei tenv =
type_ptr_to_sil_type tenv tp type_ptr_to_sil_type tenv tp
let class_from_pointer_type tenv type_ptr = let class_from_pointer_type tenv type_ptr =
match type_ptr_to_sil_type tenv type_ptr with match (type_ptr_to_sil_type tenv type_ptr).Typ.desc with
| Typ.Tptr(Typ.Tstruct typename, _) -> typename | Tptr({desc=Tstruct typename}, _) -> typename
| _ -> assert false | _ -> assert false
let get_class_type_np tenv expr_info obj_c_message_expr_info = let get_class_type_np tenv expr_info obj_c_message_expr_info =

@ -26,7 +26,7 @@ let assignment_arc_mode e1 typ e2 loc rhs_owning_method is_e1_decl =
let mk_call procname e t = let mk_call procname e t =
let bi_retain = Exp.Const (Const.Cfun procname) in let bi_retain = Exp.Const (Const.Cfun procname) in
Sil.Call (None, bi_retain, [(e, t)], loc, CallFlags.default) in Sil.Call (None, bi_retain, [(e, t)], loc, CallFlags.default) in
match typ with match typ.Typ.desc with
| Typ.Tptr (_, Typ.Pk_pointer) when not rhs_owning_method && not is_e1_decl -> | Typ.Tptr (_, Typ.Pk_pointer) when not rhs_owning_method && not is_e1_decl ->
(* for __strong e1 = e2 the semantics is*) (* for __strong e1 = e2 the semantics is*)
(* retain(e2); tmp=e1; e1=e2; release(tmp); *) (* retain(e2); tmp=e1; e1=e2; release(tmp); *)

@ -44,7 +44,7 @@ let enum_decl decl =
match decl with match decl with
| EnumDecl (_, _, _, type_ptr, decl_list, _, _) -> | EnumDecl (_, _, _, type_ptr, decl_list, _, _) ->
add_enum_constants_to_map (List.rev decl_list); add_enum_constants_to_map (List.rev decl_list);
let sil_type = Typ.Tint Typ.IInt in let sil_type = Typ.mk (Typ.Tint Typ.IInt) in
CAst_utils.update_sil_types_map type_ptr sil_type; CAst_utils.update_sil_types_map type_ptr sil_type;
sil_type sil_type

@ -37,7 +37,7 @@ let fields_superclass tenv interface_decl_info =
let build_sil_field type_ptr_to_sil_type tenv field_name type_ptr prop_attributes = let build_sil_field type_ptr_to_sil_type tenv field_name type_ptr prop_attributes =
let prop_atts = List.map ~f:Clang_ast_j.string_of_property_attribute prop_attributes in let prop_atts = List.map ~f:Clang_ast_j.string_of_property_attribute prop_attributes in
let annotation_from_type t = let annotation_from_type t =
match t with match t.Typ.desc with
| Typ.Tptr (_, Typ.Pk_objc_weak) -> [Config.weak] | Typ.Tptr (_, Typ.Pk_objc_weak) -> [Config.weak]
| Typ.Tptr (_, Typ.Pk_objc_unsafe_unretained) -> [Config.unsafe_unret] | Typ.Tptr (_, Typ.Pk_objc_unsafe_unretained) -> [Config.unsafe_unret]
| _ -> [] in | _ -> [] in
@ -87,8 +87,8 @@ let add_missing_fields tenv class_name missing_fields =
| _ -> () | _ -> ()
let modelled_fields_in_classes = let modelled_fields_in_classes =
[("NSData", "_bytes", Typ.Tptr (Typ.Tvoid, Typ.Pk_pointer)); [("NSData", "_bytes", Typ.mk (Tptr (Typ.mk Tvoid, Typ.Pk_pointer)));
("NSArray", "elementData", Typ.Tint Typ.IInt)] ("NSArray", "elementData", Typ.mk (Tint Typ.IInt))]
let modelled_field class_name_info = let modelled_field class_name_info =
let modelled_field_in_class res (class_name, field_name, typ) = let modelled_field_in_class res (class_name, field_name, typ) =

@ -62,8 +62,8 @@ let get_class_param function_method_decl_info =
let should_add_return_param return_type ~is_objc_method = let should_add_return_param return_type ~is_objc_method =
match return_type with match return_type.Typ.desc with
| Typ.Tstruct _ -> not is_objc_method | Tstruct _ -> not is_objc_method
| _ -> false | _ -> false
let is_objc_method function_method_decl_info = let is_objc_method function_method_decl_info =
@ -112,8 +112,8 @@ let get_parameters trans_unit_ctx tenv function_method_decl_info =
let _, mangled = CGeneral_utils.get_var_name_mangled name_info var_decl_info in let _, mangled = CGeneral_utils.get_var_name_mangled name_info var_decl_info in
let param_typ = CType_decl.type_ptr_to_sil_type tenv qt.Clang_ast_t.qt_type_ptr in let param_typ = CType_decl.type_ptr_to_sil_type tenv qt.Clang_ast_t.qt_type_ptr in
let qt_type_ptr = let qt_type_ptr =
match param_typ with match param_typ.Typ.desc with
| Typ.Tstruct _ when CGeneral_utils.is_cpp_translation trans_unit_ctx -> | Tstruct _ when CGeneral_utils.is_cpp_translation trans_unit_ctx ->
Ast_expressions.create_reference_type qt.Clang_ast_t.qt_type_ptr Ast_expressions.create_reference_type qt.Clang_ast_t.qt_type_ptr
| _ -> qt.Clang_ast_t.qt_type_ptr in | _ -> qt.Clang_ast_t.qt_type_ptr in
(mangled, {qt with qt_type_ptr}) (mangled, {qt with qt_type_ptr})
@ -127,7 +127,7 @@ let get_return_val_and_param_types tenv function_method_decl_info =
let return_typ = CType_decl.type_ptr_to_sil_type tenv return_type_ptr in let return_typ = CType_decl.type_ptr_to_sil_type tenv return_type_ptr in
let is_objc_method = is_objc_method function_method_decl_info in let is_objc_method = is_objc_method function_method_decl_info in
if should_add_return_param return_typ ~is_objc_method then if should_add_return_param return_typ ~is_objc_method then
Ast_expressions.create_void_type, Some (Typ.Tptr (return_typ, Typ.Pk_pointer)) Ast_expressions.create_void_type, Some (CType.add_pointer_to_typ return_typ)
else return_type_ptr, None else return_type_ptr, None
let build_method_signature trans_unit_ctx tenv decl_info procname function_method_decl_info let build_method_signature trans_unit_ctx tenv decl_info procname function_method_decl_info
@ -263,7 +263,7 @@ let get_class_name_method_call_from_receiver_kind context obj_c_message_expr_inf
(CType.objc_classname_of_type sil_type) (CType.objc_classname_of_type sil_type)
| `Instance -> | `Instance ->
(match act_params with (match act_params with
| (_, Typ.Tptr(t, _)):: _ | (_, {Typ.desc=Tptr(t, _)}):: _
| (_, t):: _ -> CType.objc_classname_of_type t | (_, t):: _ -> CType.objc_classname_of_type t
| _ -> assert false) | _ -> assert false)
| `SuperInstance ->get_superclass_curr_class_objc context | `SuperInstance ->get_superclass_curr_class_objc context
@ -442,7 +442,7 @@ let create_external_procdesc cfg proc_name is_objc_inst_method type_opt =
(match type_opt with (match type_opt with
| Some (ret_type, arg_types) -> | Some (ret_type, arg_types) ->
ret_type, List.map ~f:(fun typ -> (Mangled.from_string "x", typ)) arg_types ret_type, List.map ~f:(fun typ -> (Mangled.from_string "x", typ)) arg_types
| None -> Typ.Tvoid, []) in | None -> Typ.mk Typ.Tvoid, []) in
let loc = Location.dummy in let loc = Location.dummy in
let proc_attributes = let proc_attributes =
{ (ProcAttributes.default proc_name Config.Clang) with { (ProcAttributes.default proc_name Config.Clang) with

@ -74,7 +74,7 @@ struct
not (CTrans_utils.is_owning_name method_name) && not (CTrans_utils.is_owning_name method_name) &&
ObjcInterface_decl.is_pointer_to_objc_class typ then ObjcInterface_decl.is_pointer_to_objc_class typ then
let fname = BuiltinDecl.__set_autorelease_attribute in let fname = BuiltinDecl.__set_autorelease_attribute in
let ret_id = Some (Ident.create_fresh Ident.knormal, Typ.Tvoid) in let ret_id = Some (Ident.create_fresh Ident.knormal, Typ.mk Typ.Tvoid) in
(* TODO(jjb): change ret_id to None? *) (* TODO(jjb): change ret_id to None? *)
let stmt_call = let stmt_call =
Sil.Call (ret_id, Exp.Const (Const.Cfun fname), [(exp, typ)], sil_loc, CallFlags.default) in Sil.Call (ret_id, Exp.Const (Const.Cfun fname), [(exp, typ)], sil_loc, CallFlags.default) in
@ -118,7 +118,7 @@ struct
Logging.out_debug "-----> field: '%s'\n" (Fieldname.to_string fn)) fields; Logging.out_debug "-----> field: '%s'\n" (Fieldname.to_string fn)) fields;
let block_typename = Typ.Name.Objc.from_string block_name in let block_typename = Typ.Name.Objc.from_string block_name in
ignore (Tenv.mk_struct tenv ~fields block_typename); ignore (Tenv.mk_struct tenv ~fields block_typename);
let block_type = Typ.Tstruct block_typename in let block_type = Typ.mk (Typ.Tstruct block_typename) in
let trans_res = let trans_res =
CTrans_utils.alloc_trans CTrans_utils.alloc_trans
trans_state loc (Ast_expressions.dummy_stmt_info ()) block_type true None in trans_state loc (Ast_expressions.dummy_stmt_info ()) block_type true None in
@ -128,7 +128,7 @@ struct
let mblock = Mangled.from_string block_name in let mblock = Mangled.from_string block_name in
let block_var = Pvar.mk mblock procname in let block_var = Pvar.mk mblock procname in
let declare_block_local = let declare_block_local =
Sil.Declare_locals ([(block_var, Typ.Tptr (block_type, Typ.Pk_pointer))], loc) in Sil.Declare_locals ([(block_var, CType.add_pointer_to_typ block_type)], loc) in
let set_instr = Sil.Store (Exp.Lvar block_var, block_type, Exp.Var id_block, loc) in let set_instr = Sil.Store (Exp.Lvar block_var, block_type, Exp.Var id_block, loc) in
let create_field_exp (var, typ) = let create_field_exp (var, typ) =
let id = Ident.create_fresh Ident.knormal in let id = Ident.create_fresh Ident.knormal in
@ -158,7 +158,7 @@ struct
match es with match es with
| [] -> [] | [] -> []
| (Exp.Closure {name; captured_vars}, | (Exp.Closure {name; captured_vars},
(Typ.Tptr((Typ.Tfun _), _ ) as t)) :: es' -> ({Typ.desc=Tptr({Typ.desc=Tfun _}, _ )} as t)) :: es' ->
let app = let app =
let function_name = make_function_name t name in let function_name = make_function_name t name in
let args = List.map ~f:(make_arg t) captured_vars in let args = List.map ~f:(make_arg t) captured_vars in
@ -207,23 +207,23 @@ struct
try try
f trans_state stmt f trans_state stmt
with Self.SelfClassException class_name -> with Self.SelfClassException class_name ->
let typ = Typ.Tstruct class_name in let typ = Typ.mk (Tstruct class_name) in
{ empty_res_trans with { empty_res_trans with
exps = [(Exp.Sizeof (typ, None, Subtype.exact), Tint IULong)] } exps = [Exp.Sizeof (typ, None, Subtype.exact), Typ.mk (Tint IULong)] }
let add_reference_if_glvalue typ expr_info = let add_reference_if_glvalue (typ : Typ.t) expr_info =
(* glvalue definition per C++11:*) (* glvalue definition per C++11:*)
(* http://en.cppreference.com/w/cpp/language/value_category *) (* http://en.cppreference.com/w/cpp/language/value_category *)
let is_glvalue = match expr_info.Clang_ast_t.ei_value_kind with let is_glvalue = match expr_info.Clang_ast_t.ei_value_kind with
| `LValue | `XValue -> true | `LValue | `XValue -> true
| `RValue -> false in | `RValue -> false in
match is_glvalue, typ with match is_glvalue, typ.desc with
| true, Typ.Tptr (_, Typ.Pk_reference) -> | true, Tptr (_, Pk_reference) ->
(* reference of reference is not allowed in C++ - it's most likely frontend *) (* reference of reference is not allowed in C++ - it's most likely frontend *)
(* trying to add same reference to same type twice*) (* trying to add same reference to same type twice*)
(* this is hacky and should be fixed (t9838691) *) (* this is hacky and should be fixed (t9838691) *)
typ typ
| true, _ -> Typ.Tptr (typ, Typ.Pk_reference) | true, _ -> Typ.mk (Tptr (typ, Pk_reference))
| _ -> typ | _ -> typ
(** Execute translation and then possibly adjust the type of the result of translation: (** Execute translation and then possibly adjust the type of the result of translation:
@ -273,14 +273,14 @@ struct
Procdesc.append_locals procdesc [(Pvar.get_name pvar, typ)]; Procdesc.append_locals procdesc [(Pvar.get_name pvar, typ)];
Exp.Lvar pvar, typ Exp.Lvar pvar, typ
let create_call_instr trans_state return_type function_sil params_sil sil_loc let create_call_instr trans_state (return_type : Typ.t) function_sil params_sil sil_loc
call_flags ~is_objc_method = call_flags ~is_objc_method =
let ret_id = if (Typ.equal return_type Typ.Tvoid) then None let ret_id = if (Typ.equal_desc return_type.desc Typ.Tvoid) then None
else Some (Ident.create_fresh Ident.knormal, return_type) in else Some (Ident.create_fresh Ident.knormal, return_type) in
let ret_id', params, initd_exps, ret_exps = let ret_id', params, initd_exps, ret_exps =
(* Assumption: should_add_return_param will return true only for struct types *) (* Assumption: should_add_return_param will return true only for struct types *)
if CMethod_trans.should_add_return_param return_type ~is_objc_method then if CMethod_trans.should_add_return_param return_type ~is_objc_method then
let param_type = Typ.Tptr (return_type, Typ.Pk_pointer) in let param_type = Typ.mk (Typ.Tptr (return_type, Typ.Pk_pointer)) in
let var_exp = match trans_state.var_exp_typ with let var_exp = match trans_state.var_exp_typ with
| Some (exp, _) -> exp | Some (exp, _) -> exp
| _ -> | _ ->
@ -391,7 +391,7 @@ struct
let cxxScalarValueInitExpr_trans trans_state expr_info = let cxxScalarValueInitExpr_trans trans_state expr_info =
let typ = CType_decl.get_type_from_expr_info expr_info trans_state.context.CContext.tenv in let typ = CType_decl.get_type_from_expr_info expr_info trans_state.context.CContext.tenv in
(* constant will be different depending on type *) (* constant will be different depending on type *)
let zero_opt = match typ with let zero_opt = match typ.desc with
| Typ.Tfloat _ | Typ.Tptr _ | Typ.Tint _ -> Some (Sil.zero_value_of_numerical_type typ) | Typ.Tfloat _ | Typ.Tptr _ | Typ.Tint _ -> Some (Sil.zero_value_of_numerical_type typ)
| Typ.Tvoid -> None | Typ.Tvoid -> None
| _ -> Some (Exp.Const (Const.Cint IntLit.zero)) in | _ -> Some (Exp.Const (Const.Cint IntLit.zero)) in
@ -493,13 +493,13 @@ struct
let field_typ = CType_decl.type_ptr_to_sil_type context.tenv type_ptr in let field_typ = CType_decl.type_ptr_to_sil_type context.tenv type_ptr in
let (obj_sil, class_typ) = extract_exp_from_list pre_trans_result.exps let (obj_sil, class_typ) = extract_exp_from_list pre_trans_result.exps
"WARNING: in Field dereference we expect to know the object\n" in "WARNING: in Field dereference we expect to know the object\n" in
let is_pointer_typ = match class_typ with let is_pointer_typ = match class_typ.desc with
| Typ.Tptr _ -> true | Typ.Tptr _ -> true
| _ -> false in | _ -> false in
let class_typ = let class_typ =
match class_typ with match class_typ.desc with
| Typ.Tptr (t, _) -> t | Typ.Tptr (t, _) -> t
| t -> t in | _ -> class_typ in
Logging.out_debug "Type is '%s' @." (Typ.to_string class_typ); Logging.out_debug "Type is '%s' @." (Typ.to_string class_typ);
let field_name = CGeneral_utils.mk_class_field_name name_info in let field_name = CGeneral_utils.mk_class_field_name name_info in
let field_exp = Exp.Lfield (obj_sil, field_name, class_typ) in let field_exp = Exp.Lfield (obj_sil, field_name, class_typ) in
@ -549,12 +549,12 @@ struct
| [] -> [], [] | [] -> [], []
(* We need to add a dereference before a method call to find null dereferences when *) (* We need to add a dereference before a method call to find null dereferences when *)
(* calling a method with null *) (* calling a method with null *)
| [(exp, Typ.Tptr (typ, _) )] when decl_kind <> `CXXConstructor -> | [(exp, {Typ.desc=Tptr (typ, _)})] when decl_kind <> `CXXConstructor ->
let no_id = Ident.create_none () in let no_id = Ident.create_none () in
let extra_instrs = [Sil.Load (no_id, exp, typ, sil_loc)] in let extra_instrs = [Sil.Load (no_id, exp, typ, sil_loc)] in
pre_trans_result.exps, extra_instrs pre_trans_result.exps, extra_instrs
| [(_, Typ.Tptr _ )] -> pre_trans_result.exps, [] | [(_, {Typ.desc=Tptr _})] -> pre_trans_result.exps, []
| [(sil, typ)] -> [(sil, Typ.Tptr (typ, Typ.Pk_reference))], [] | [(sil, typ)] -> [(sil, Typ.mk (Tptr (typ, Typ.Pk_reference)))], []
| _ -> assert false | _ -> assert false
) )
else else
@ -625,10 +625,10 @@ struct
let _, _, type_ptr = CAst_utils.get_info_from_decl_ref decl_ref in let _, _, type_ptr = CAst_utils.get_info_from_decl_ref decl_ref in
let ast_typ = CType_decl.type_ptr_to_sil_type context.tenv type_ptr in let ast_typ = CType_decl.type_ptr_to_sil_type context.tenv type_ptr in
let typ = let typ =
match ast_typ with match ast_typ.Typ.desc with
| Tstruct _ when decl_ref.dr_kind = `ParmVar -> | Tstruct _ when decl_ref.dr_kind = `ParmVar ->
if CGeneral_utils.is_cpp_translation context.translation_unit_context then if CGeneral_utils.is_cpp_translation context.translation_unit_context then
Typ.Tptr (ast_typ, Pk_reference) Typ.mk (Tptr (ast_typ, Pk_reference))
else ast_typ else ast_typ
| _ -> ast_typ in | _ -> ast_typ in
let procname = Procdesc.get_proc_name context.procdesc in let procname = Procdesc.get_proc_name context.procdesc in
@ -641,12 +641,12 @@ struct
if (CType.is_class typ) then if (CType.is_class typ) then
raise (Self.SelfClassException class_typename) raise (Self.SelfClassException class_typename)
else else
let typ = CType.add_pointer_to_typ (Typ.Tstruct class_typename) in let typ = CType.add_pointer_to_typ (Typ.mk (Tstruct class_typename)) in
[(var_exp, typ)] [(var_exp, typ)]
else [(var_exp, typ)] in else [(var_exp, typ)] in
Logging.out_debug "\n\n PVAR ='%s'\n\n" (Pvar.to_string pvar); Logging.out_debug "\n\n PVAR ='%s'\n\n" (Pvar.to_string pvar);
let res_trans = { empty_res_trans with exps } in let res_trans = { empty_res_trans with exps } in
match typ with match typ.desc with
| Tptr (_, Pk_reference) -> | Tptr (_, Pk_reference) ->
(* dereference pvar due to the behavior of reference types in clang's AST *) (* dereference pvar due to the behavior of reference types in clang's AST *)
dereference_value_from_result sil_loc res_trans ~strip_pointer:false dereference_value_from_result sil_loc res_trans ~strip_pointer:false
@ -876,7 +876,7 @@ struct
(Logging.out_debug "ERROR: stmt_list and res_trans_par.exps must have same size\n"; (Logging.out_debug "ERROR: stmt_list and res_trans_par.exps must have same size\n";
assert false) in assert false) in
let act_params = if is_cf_retain_release then let act_params = if is_cf_retain_release then
(Exp.Const (Const.Cint IntLit.one), Typ.Tint Typ.IBool) :: act_params (Exp.Const (Const.Cint IntLit.one), Typ.mk (Tint Typ.IBool)) :: act_params
else act_params in else act_params in
let res_trans_call = let res_trans_call =
let cast_trans_fun = cast_trans act_params sil_loc function_type in let cast_trans_fun = cast_trans act_params sil_loc function_type in
@ -973,7 +973,7 @@ struct
let class_type = CType_decl.get_type_from_expr_info ei context.CContext.tenv in let class_type = CType_decl.get_type_from_expr_info ei context.CContext.tenv in
Procdesc.append_locals procdesc [(Pvar.get_name pvar, class_type)]; Procdesc.append_locals procdesc [(Pvar.get_name pvar, class_type)];
Exp.Lvar pvar, class_type in Exp.Lvar pvar, class_type in
let this_type = Typ.Tptr (class_type, Typ.Pk_pointer) in let this_type = CType.add_pointer_to_typ class_type in
let this_res_trans = { empty_res_trans with let this_res_trans = { empty_res_trans with
exps = [(var_exp, this_type)]; exps = [(var_exp, this_type)];
initd_exps = [var_exp]; initd_exps = [var_exp];
@ -983,13 +983,13 @@ struct
to be extra Load instruction before returning the trans_result of constructorExpr. to be extra Load instruction before returning the trans_result of constructorExpr.
There is no LValueToRvalue cast in the AST afterwards since clang doesn't know There is no LValueToRvalue cast in the AST afterwards since clang doesn't know
that class type is translated as pointer type. It gets added here instead. *) that class type is translated as pointer type. It gets added here instead. *)
let extra_res_trans = match class_type with let extra_res_trans = match class_type.desc with
| Typ.Tptr _ -> dereference_value_from_result sil_loc tmp_res_trans ~strip_pointer:false | Typ.Tptr _ -> dereference_value_from_result sil_loc tmp_res_trans ~strip_pointer:false
| _ -> tmp_res_trans in | _ -> tmp_res_trans in
let res_trans_callee = decl_ref_trans trans_state this_res_trans si decl_ref let res_trans_callee = decl_ref_trans trans_state this_res_trans si decl_ref
~is_constructor_init:false in ~is_constructor_init:false in
let res_trans = cxx_method_construct_call_trans trans_state_pri res_trans_callee let res_trans = cxx_method_construct_call_trans trans_state_pri res_trans_callee
params_stmt si Typ.Tvoid false extra_res_trans in params_stmt si (Typ.mk Tvoid) false extra_res_trans in
{ res_trans with exps=extra_res_trans.exps } { res_trans with exps=extra_res_trans.exps }
and cxx_destructor_call_trans trans_state si this_res_trans class_type_ptr = and cxx_destructor_call_trans trans_state si this_res_trans class_type_ptr =
@ -997,7 +997,7 @@ struct
let res_trans_callee = destructor_deref_trans trans_state this_res_trans class_type_ptr si in let res_trans_callee = destructor_deref_trans trans_state this_res_trans class_type_ptr si in
let is_cpp_call_virtual = res_trans_callee.is_cpp_call_virtual in let is_cpp_call_virtual = res_trans_callee.is_cpp_call_virtual in
if res_trans_callee.exps <> [] then if res_trans_callee.exps <> [] then
cxx_method_construct_call_trans trans_state_pri res_trans_callee [] si Typ.Tvoid cxx_method_construct_call_trans trans_state_pri res_trans_callee [] si (Typ.mk Tvoid)
is_cpp_call_virtual empty_res_trans is_cpp_call_virtual empty_res_trans
else empty_res_trans else empty_res_trans
@ -1202,7 +1202,7 @@ struct
Logging.out_debug " No short-circuit condition\n"; Logging.out_debug " No short-circuit condition\n";
let res_trans_cond = let res_trans_cond =
if is_null_stmt cond then { if is_null_stmt cond then {
empty_res_trans with exps = [(Exp.Const (Const.Cint IntLit.one), (Typ.Tint Typ.IBool))] empty_res_trans with exps = [(Exp.Const (Const.Cint IntLit.one), Typ.mk (Tint Typ.IBool))]
} }
(* Assumption: If it's a null_stmt, it is a loop with no bound, so we set condition to 1 *) (* Assumption: If it's a null_stmt, it is a loop with no bound, so we set condition to 1 *)
else else
@ -1613,7 +1613,7 @@ struct
and initListExpr_trans trans_state stmt_info expr_info stmts = and initListExpr_trans trans_state stmt_info expr_info stmts =
let context = trans_state.context in let context = trans_state.context in
let tenv = context.tenv in let tenv = context.tenv in
let is_array typ = match typ with | Typ.Tarray _ -> true | _ -> false in let is_array typ = match typ.Typ.desc with | Typ.Tarray _ -> true | _ -> false in
let (var_exp, typ) = let (var_exp, typ) =
match trans_state.var_exp_typ with match trans_state.var_exp_typ with
| Some var_exp_typ -> var_exp_typ | Some var_exp_typ -> var_exp_typ
@ -1906,7 +1906,7 @@ struct
let pvar = Pvar.mk (Mangled.from_string name) procname in let pvar = Pvar.mk (Mangled.from_string name) procname in
let id = Ident.create_fresh Ident.knormal in let id = Ident.create_fresh Ident.knormal in
let instr = Sil.Load (id, Exp.Lvar pvar, ret_param_typ, sil_loc) in let instr = Sil.Load (id, Exp.Lvar pvar, ret_param_typ, sil_loc) in
let ret_typ = match ret_param_typ with Typ.Tptr (t, _) -> t | _ -> assert false in let ret_typ = match ret_param_typ.desc with Typ.Tptr (t, _) -> t | _ -> assert false in
Exp.Var id, ret_typ, [instr] Exp.Var id, ret_typ, [instr]
| None -> | None ->
Exp.Lvar (Procdesc.get_ret_var procdesc), ret_type, [] in Exp.Lvar (Procdesc.get_ret_var procdesc), ret_type, [] in
@ -2003,7 +2003,7 @@ struct
let context = trans_state.context in let context = trans_state.context in
let sil_loc = CLocation.get_sil_location stmt_info context in let sil_loc = CLocation.get_sil_location stmt_info context in
let fname = BuiltinDecl.__objc_release_autorelease_pool in let fname = BuiltinDecl.__objc_release_autorelease_pool in
let ret_id = Some (Ident.create_fresh Ident.knormal, Typ.Tvoid) in let ret_id = Some (Ident.create_fresh Ident.knormal, Typ.mk Tvoid) in
(* TODO(jjb): change ret_id to None? *) (* TODO(jjb): change ret_id to None? *)
let autorelease_pool_vars = CVar_decl.compute_autorelease_pool_vars context stmts in let autorelease_pool_vars = CVar_decl.compute_autorelease_pool_vars context stmts in
let stmt_call = let stmt_call =
@ -2068,7 +2068,7 @@ struct
| _ -> assert false | _ -> assert false
and initListExpr_initializers_trans trans_state var_exp n stmts typ is_dyn_array stmt_info = and initListExpr_initializers_trans trans_state var_exp n stmts typ is_dyn_array stmt_info =
let (var_exp_inside, typ_inside) = match typ with let (var_exp_inside, typ_inside) = match typ.Typ.desc with
| Typ.Tarray (t, _) when Typ.is_array_of_cpp_class typ -> | Typ.Tarray (t, _) when Typ.is_array_of_cpp_class typ ->
Exp.Lindex (var_exp, Exp.Const (Const.Cint (IntLit.of_int n))), t Exp.Lindex (var_exp, Exp.Const (Const.Cint (IntLit.of_int n))), t
| _ when is_dyn_array -> | _ when is_dyn_array ->
@ -2129,7 +2129,7 @@ struct
let stmt_opt = CAst_utils.get_stmt_opt cxx_new_expr_info.Clang_ast_t.xnei_initializer_expr in let stmt_opt = CAst_utils.get_stmt_opt cxx_new_expr_info.Clang_ast_t.xnei_initializer_expr in
let trans_state_init = { trans_state_pri with succ_nodes = []; } in let trans_state_init = { trans_state_pri with succ_nodes = []; } in
let var_exp_typ = match res_trans_new.exps with let var_exp_typ = match res_trans_new.exps with
| [var_exp, Typ.Tptr (t, _)] -> (var_exp, t) | [var_exp, {Typ.desc=Tptr (t, _)}] -> (var_exp, t)
| _ -> assert false in | _ -> assert false in
(* Need a new stmt_info for the translation of the initializer, so that it can create nodes *) (* Need a new stmt_info for the translation of the initializer, so that it can create nodes *)
(* if it needs to, with the same stmt_info it doesn't work. *) (* if it needs to, with the same stmt_info it doesn't work. *)
@ -2224,14 +2224,14 @@ struct
let tenv = context.CContext.tenv in let tenv = context.CContext.tenv in
let sil_loc = CLocation.get_sil_location stmt_info context in let sil_loc = CLocation.get_sil_location stmt_info context in
let cast_type = CType_decl.type_ptr_to_sil_type tenv cast_type_ptr in let cast_type = CType_decl.type_ptr_to_sil_type tenv cast_type_ptr in
let sizeof_expr = match cast_type with let sizeof_expr = match cast_type.desc with
| Typ.Tptr (typ, _) -> Exp.Sizeof (typ, None, subtypes) | Typ.Tptr (typ, _) -> Exp.Sizeof (typ, None, subtypes)
| _ -> assert false in | _ -> assert false in
let builtin = Exp.Const (Const.Cfun BuiltinDecl.__cast) in let builtin = Exp.Const (Const.Cfun BuiltinDecl.__cast) in
let stmt = match stmts with [stmt] -> stmt | _ -> assert false in let stmt = match stmts with [stmt] -> stmt | _ -> assert false in
let res_trans_stmt = exec_with_glvalue_as_reference instruction trans_state' stmt in let res_trans_stmt = exec_with_glvalue_as_reference instruction trans_state' stmt in
let exp = match res_trans_stmt.exps with | [e] -> e | _ -> assert false in let exp = match res_trans_stmt.exps with | [e] -> e | _ -> assert false in
let args = [exp; (sizeof_expr, Typ.Tvoid)] in let args = [exp; (sizeof_expr, Typ.mk Tvoid)] in
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Ident.create_fresh Ident.knormal in
let call = Sil.Call (Some (ret_id, cast_type), builtin, args, sil_loc, CallFlags.default) in let call = Sil.Call (Some (ret_id, cast_type), builtin, args, sil_loc, CallFlags.default) in
let res_ex = Exp.Var ret_id in let res_ex = Exp.Var ret_id in
@ -2272,7 +2272,7 @@ struct
and cxxPseudoDestructorExpr_trans () = and cxxPseudoDestructorExpr_trans () =
let fun_name = Typ.Procname.from_string_c_fun CFrontend_config.infer_skip_fun in let fun_name = Typ.Procname.from_string_c_fun CFrontend_config.infer_skip_fun in
{ empty_res_trans with exps = [(Exp.Const (Const.Cfun fun_name), Typ.Tvoid)] } { empty_res_trans with exps = [(Exp.Const (Const.Cfun fun_name), Typ.mk Tvoid)] }
and cxxTypeidExpr_trans trans_state stmt_info stmts expr_info = and cxxTypeidExpr_trans trans_state stmt_info stmts expr_info =
let tenv = trans_state.context.CContext.tenv in let tenv = trans_state.context.CContext.tenv in
@ -2288,12 +2288,13 @@ struct
let fun_name = BuiltinDecl.__cxx_typeid in let fun_name = BuiltinDecl.__cxx_typeid in
let sil_fun = Exp.Const (Const.Cfun fun_name) in let sil_fun = Exp.Const (Const.Cfun fun_name) in
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Ident.create_fresh Ident.knormal in
let type_info_objc = (Exp.Sizeof (typ, None, Subtype.exact), Typ.Tvoid) in let void_typ = Typ.mk Tvoid in
let type_info_objc = (Exp.Sizeof (typ, None, Subtype.exact), void_typ) in
let field_name_decl = CAst_utils.make_qual_name_decl ["type_info"; "std"] "__type_name" in let field_name_decl = CAst_utils.make_qual_name_decl ["type_info"; "std"] "__type_name" in
let field_name = CGeneral_utils.mk_class_field_name field_name_decl in let field_name = CGeneral_utils.mk_class_field_name field_name_decl in
let ret_exp = Exp.Var ret_id in let ret_exp = Exp.Var ret_id in
let field_exp = Exp.Lfield (ret_exp, field_name, typ) in let field_exp = Exp.Lfield (ret_exp, field_name, typ) in
let args = type_info_objc :: (field_exp, Typ.Tvoid) :: res_trans_subexpr.exps in let args = type_info_objc :: (field_exp, void_typ) :: res_trans_subexpr.exps in
let call_instr = Sil.Call (Some (ret_id, typ), sil_fun, args, sil_loc, CallFlags.default) in let call_instr = Sil.Call (Some (ret_id, typ), sil_fun, args, sil_loc, CallFlags.default) in
let res_trans_call = { empty_res_trans with let res_trans_call = { empty_res_trans with
instrs = [call_instr]; instrs = [call_instr];
@ -2616,7 +2617,7 @@ struct
implicitValueInitExpr_trans trans_state expr_info implicitValueInitExpr_trans trans_state expr_info
| GenericSelectionExpr _ (* to be fixed when we dump the right info in the ast *) | GenericSelectionExpr _ (* to be fixed when we dump the right info in the ast *)
| SizeOfPackExpr _ -> | SizeOfPackExpr _ ->
{ empty_res_trans with exps = [(Exp.get_undefined false, Typ.Tvoid)] } { empty_res_trans with exps = [(Exp.get_undefined false, Typ.mk Tvoid)] }
| GCCAsmStmt (stmt_info, stmts) -> | GCCAsmStmt (stmt_info, stmts) ->
gccAsmStmt_trans trans_state stmt_info stmts gccAsmStmt_trans trans_state stmt_info stmts
@ -2683,7 +2684,7 @@ struct
"WARNING: There should be one expression for 'this' in constructor. \n" in "WARNING: There should be one expression for 'this' in constructor. \n" in
(* Hack: Strip pointer from type here since cxxConstructExpr_trans expects it this way *) (* Hack: Strip pointer from type here since cxxConstructExpr_trans expects it this way *)
(* it will add pointer back before making it a parameter to a call *) (* it will add pointer back before making it a parameter to a call *)
let class_typ = match this_typ with Typ.Tptr (t, _) -> t | _ -> assert false in let class_typ = match this_typ.Typ.desc with Tptr (t, _) -> t | _ -> assert false in
{ this_res_trans with exps = [this_exp, class_typ] } { this_res_trans with exps = [this_exp, class_typ] }
| `Member (decl_ref) -> | `Member (decl_ref) ->
decl_ref_trans trans_state' this_res_trans child_stmt_info decl_ref decl_ref_trans trans_state' this_res_trans child_stmt_info decl_ref

@ -25,7 +25,7 @@ let extract_item_from_singleton l warning_string failure_val =
| [item] -> item | [item] -> item
| _ -> Logging.err_debug "%s" warning_string; failure_val | _ -> Logging.err_debug "%s" warning_string; failure_val
let dummy_exp = (Exp.minus_one, Typ.Tint Typ.IInt) let dummy_exp = (Exp.minus_one, Typ.mk (Tint Typ.IInt))
(* Extract the element of a singleton list. If the list is not a singleton *) (* Extract the element of a singleton list. If the list is not a singleton *)
(* Gives a warning and return -1 as standard value indicating something *) (* Gives a warning and return -1 as standard value indicating something *)
@ -294,20 +294,20 @@ end
(** This function handles ObjC new/alloc and C++ new calls *) (** This function handles ObjC new/alloc and C++ new calls *)
let create_alloc_instrs sil_loc function_type fname size_exp_opt procname_opt = let create_alloc_instrs sil_loc function_type fname size_exp_opt procname_opt =
let function_type, function_type_np = let function_type, function_type_np =
match function_type with match function_type.Typ.desc with
| Typ.Tptr (styp, Typ.Pk_pointer) | Tptr (styp, Typ.Pk_pointer)
| Typ.Tptr (styp, Typ.Pk_objc_weak) | Tptr (styp, Typ.Pk_objc_weak)
| Typ.Tptr (styp, Typ.Pk_objc_unsafe_unretained) | Tptr (styp, Typ.Pk_objc_unsafe_unretained)
| Typ.Tptr (styp, Typ.Pk_objc_autoreleasing) -> | Tptr (styp, Typ.Pk_objc_autoreleasing) ->
function_type, styp function_type, styp
| _ -> Typ.Tptr (function_type, Typ.Pk_pointer), function_type in | _ -> CType.add_pointer_to_typ function_type, function_type in
let sizeof_exp_ = Exp.Sizeof (function_type_np, None, Subtype.exact) in let sizeof_exp_ = Exp.Sizeof (function_type_np, None, Subtype.exact) in
let sizeof_exp = match size_exp_opt with let sizeof_exp = match size_exp_opt with
| Some exp -> Exp.BinOp (Binop.Mult, sizeof_exp_, exp) | Some exp -> Exp.BinOp (Binop.Mult, sizeof_exp_, exp)
| None -> sizeof_exp_ in | None -> sizeof_exp_ in
let exp = (sizeof_exp, Typ.Tint Typ.IULong) in let exp = (sizeof_exp, Typ.mk (Tint Typ.IULong)) in
let procname_arg = match procname_opt with let procname_arg = match procname_opt with
| Some procname -> [Exp.Const (Const.Cfun (procname)), Typ.Tvoid] | Some procname -> [Exp.Const (Const.Cfun (procname)), Typ.mk Tvoid]
| None -> [] in | None -> [] in
let args = exp :: procname_arg in let args = exp :: procname_arg in
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Ident.create_fresh Ident.knormal in
@ -379,7 +379,7 @@ let create_cast_instrs exp cast_from_typ cast_to_typ sil_loc =
let typ = CType.remove_pointer_to_typ cast_to_typ in let typ = CType.remove_pointer_to_typ cast_to_typ in
let sizeof_exp = Exp.Sizeof (typ, None, Subtype.exact) in let sizeof_exp = Exp.Sizeof (typ, None, Subtype.exact) in
let pname = BuiltinDecl.__objc_cast in let pname = BuiltinDecl.__objc_cast in
let args = [(exp, cast_from_typ); (sizeof_exp, Typ.Tint Typ.IULong)] in let args = [(exp, cast_from_typ); (sizeof_exp, Typ.mk (Tint Typ.IULong))] in
let stmt_call = let stmt_call =
Sil.Call (ret_id_typ, Exp.Const (Const.Cfun pname), args, sil_loc, CallFlags.default) in Sil.Call (ret_id_typ, Exp.Const (Const.Cfun pname), args, sil_loc, CallFlags.default) in
(stmt_call, Exp.Var ret_id) (stmt_call, Exp.Var ret_id)
@ -401,7 +401,7 @@ let dereference_var_sil (exp, typ) sil_loc =
assigned to it *) assigned to it *)
let dereference_value_from_result sil_loc trans_result ~strip_pointer = let dereference_value_from_result sil_loc trans_result ~strip_pointer =
let (obj_sil, class_typ) = extract_exp_from_list trans_result.exps "" in let (obj_sil, class_typ) = extract_exp_from_list trans_result.exps "" in
let typ_no_ptr = match class_typ with | Typ.Tptr (typ, _) -> typ | _ -> assert false in let typ_no_ptr = match class_typ.Typ.desc with | Tptr (typ, _) -> typ | _ -> assert false in
let cast_typ = if strip_pointer then typ_no_ptr else class_typ in let cast_typ = if strip_pointer then typ_no_ptr else class_typ in
let cast_inst, cast_exp = dereference_var_sil (obj_sil, cast_typ) sil_loc in let cast_inst, cast_exp = dereference_var_sil (obj_sil, cast_typ) sil_loc in
{ trans_result with { trans_result with
@ -445,7 +445,7 @@ let cast_operation trans_state cast_kind exps cast_typ sil_loc is_objc_bridged =
let trans_assertion_failure sil_loc (context : CContext.t) = let trans_assertion_failure sil_loc (context : CContext.t) =
let assert_fail_builtin = Exp.Const (Const.Cfun BuiltinDecl.__infer_fail) in let assert_fail_builtin = Exp.Const (Const.Cfun BuiltinDecl.__infer_fail) in
let args = [Exp.Const (Const.Cstr Config.default_failure_name), Typ.Tvoid] in let args = [Exp.Const (Const.Cstr Config.default_failure_name), Typ.mk Tvoid] in
let call_instr = Sil.Call (None, assert_fail_builtin, args, sil_loc, CallFlags.default) in let call_instr = Sil.Call (None, assert_fail_builtin, args, sil_loc, CallFlags.default) in
let exit_node = Procdesc.get_exit_node (CContext.get_procdesc context) let exit_node = Procdesc.get_exit_node (CContext.get_procdesc context)
and failure_node = and failure_node =
@ -581,7 +581,7 @@ struct
let typ, self_expr, ins = let typ, self_expr, ins =
let t' = let t' =
CType.add_pointer_to_typ CType.add_pointer_to_typ
(Typ.Tstruct (CContext.get_curr_class_typename context)) in (Typ.mk (Tstruct (CContext.get_curr_class_typename context))) in
let e = Exp.Lvar (Pvar.mk (Mangled.from_string CFrontend_config.self) procname) in let e = Exp.Lvar (Pvar.mk (Mangled.from_string CFrontend_config.self) procname) in
let id = Ident.create_fresh Ident.knormal in let id = Ident.create_fresh Ident.knormal in
t', Exp.Var id, [Sil.Load (id, e, t', loc)] in t', Exp.Var id, [Sil.Load (id, e, t', loc)] in
@ -658,7 +658,8 @@ let rec contains_opaque_value_expr s =
(* checks if a unary operator is a logic negation applied to integers*) (* checks if a unary operator is a logic negation applied to integers*)
let is_logical_negation_of_int tenv ei uoi = let is_logical_negation_of_int tenv ei uoi =
match CType_decl.type_ptr_to_sil_type tenv ei.Clang_ast_t.ei_type_ptr, uoi.Clang_ast_t.uoi_kind with match (CType_decl.type_ptr_to_sil_type tenv ei.Clang_ast_t.ei_type_ptr).desc,
uoi.Clang_ast_t.uoi_kind with
| Typ.Tint _,`LNot -> true | Typ.Tint _,`LNot -> true
| _, _ -> false | _, _ -> false
@ -710,8 +711,8 @@ let is_block_enumerate_function mei =
let var_or_zero_in_init_list tenv e typ ~return_zero:return_zero = let var_or_zero_in_init_list tenv e typ ~return_zero:return_zero =
let rec var_or_zero_in_init_list' e typ tns = let rec var_or_zero_in_init_list' e typ tns =
let open CGeneral_utils in let open CGeneral_utils in
match typ with match typ.Typ.desc with
| Typ.Tstruct tn -> ( | Tstruct tn -> (
match Tenv.lookup tenv tn with match Tenv.lookup tenv tn with
| Some { fields } -> | Some { fields } ->
let lh_exprs = let lh_exprs =
@ -722,7 +723,7 @@ let var_or_zero_in_init_list tenv e typ ~return_zero:return_zero =
| None -> | None ->
assert false assert false
) )
| Typ.Tarray (arrtyp, Some n) -> | Tarray (arrtyp, Some n) ->
let size = IntLit.to_int n in let size = IntLit.to_int n in
let indices = list_range 0 (size - 1) in let indices = list_range 0 (size - 1) in
let index_constants = let index_constants =
@ -733,10 +734,10 @@ let var_or_zero_in_init_list tenv e typ ~return_zero:return_zero =
let exp_types = zip lh_exprs lh_types in let exp_types = zip lh_exprs lh_types in
List.map ~f:(fun (e, t) -> List.map ~f:(fun (e, t) ->
List.concat (var_or_zero_in_init_list' e t tns)) exp_types List.concat (var_or_zero_in_init_list' e t tns)) exp_types
| Typ.Tint _ | Typ.Tfloat _ | Typ.Tptr _ -> | Tint _ | Tfloat _ | Tptr _ ->
let exp = if return_zero then Sil.zero_value_of_numerical_type typ else e in let exp = if return_zero then Sil.zero_value_of_numerical_type typ else e in
[ [(exp, typ)] ] [ [(exp, typ)] ]
| Typ.Tfun _ | Typ.Tvoid | Typ.Tarray _ -> assert false in | Tfun _ | Tvoid | Tarray _ -> assert false in
List.concat (var_or_zero_in_init_list' e typ String.Set.empty) List.concat (var_or_zero_in_init_list' e typ String.Set.empty)
(* (*

@ -15,42 +15,42 @@ let get_builtin_objc_typename builtin_type =
| `ObjCClass -> Typ.Name.C.from_string CFrontend_config.objc_class | `ObjCClass -> Typ.Name.C.from_string CFrontend_config.objc_class
let get_builtin_objc_type builtin_type = let get_builtin_objc_type builtin_type =
let typ = Typ.Tstruct (get_builtin_objc_typename builtin_type) in let typ = Typ.mk (Tstruct (get_builtin_objc_typename builtin_type)) in
match builtin_type with match builtin_type with
| `ObjCId -> typ | `ObjCId -> typ
| `ObjCClass -> Typ.Tptr (typ, Typ.Pk_pointer) | `ObjCClass -> Typ.mk (Tptr (typ, Typ.Pk_pointer))
let sil_type_of_builtin_type_kind builtin_type_kind = let sil_type_of_builtin_type_kind builtin_type_kind =
match builtin_type_kind with match builtin_type_kind with
| `Void -> Typ.Tvoid | `Void -> Typ.mk Tvoid
| `Bool -> Typ.Tint Typ.IBool | `Bool -> Typ.mk (Tint IBool)
| `Char_U -> Typ.Tint Typ.IUChar | `Char_U -> Typ.mk (Tint IUChar)
| `UChar -> Typ.Tint Typ.IUChar | `UChar -> Typ.mk (Tint IUChar)
| `WChar_U -> Typ.Tint Typ.IUChar | `WChar_U -> Typ.mk (Tint IUChar)
| `Char_S -> Typ.Tint Typ.IChar | `Char_S -> Typ.mk (Tint IChar)
| `SChar -> Typ.Tint Typ.ISChar | `SChar -> Typ.mk (Tint ISChar)
| `WChar_S | `WChar_S
| `Char16 | `Char16
| `Char32 -> Typ.Tint Typ.IChar | `Char32 -> Typ.mk (Tint IChar)
| `UShort | `UShort
| `Short -> Typ.Tint Typ.IShort | `Short -> Typ.mk (Tint IShort)
| `UInt | `UInt
| `UInt128 -> Typ.Tint Typ.IUInt | `UInt128 -> Typ.mk (Tint IUInt)
| `ULong -> Typ.Tint Typ.IULong | `ULong -> Typ.mk (Tint IULong)
| `ULongLong -> Typ.Tint Typ.IULongLong | `ULongLong -> Typ.mk (Tint IULongLong)
| `Int | `Int
| `Int128 -> Typ.Tint Typ.IInt | `Int128 -> Typ.mk (Tint IInt)
| `Long -> Typ.Tint Typ.ILong | `Long -> Typ.mk (Tint ILong)
| `LongLong -> Typ.Tint Typ.ILongLong | `LongLong -> Typ.mk (Tint ILongLong)
| `Half -> Typ.Tint Typ.IShort (*?*) | `Half -> Typ.mk (Tint IShort) (*?*)
| `Float -> Typ.Tfloat Typ.FFloat | `Float -> Typ.mk (Tfloat FFloat)
| `Double -> Typ.Tfloat Typ.FDouble | `Double -> Typ.mk (Tfloat FDouble)
| `LongDouble -> Typ.Tfloat Typ.FLongDouble | `LongDouble -> Typ.mk (Tfloat FLongDouble)
| `NullPtr -> Typ.Tint Typ.IInt | `NullPtr -> Typ.mk (Tint IInt)
| `ObjCId -> get_builtin_objc_type `ObjCId | `ObjCId -> get_builtin_objc_type `ObjCId
| `ObjCClass -> get_builtin_objc_type `ObjCClass | `ObjCClass -> get_builtin_objc_type `ObjCClass
| _ -> Typ.Tvoid | _ -> Typ.mk Tvoid
let pointer_attribute_of_objc_attribute attr_info = let pointer_attribute_of_objc_attribute attr_info =
match attr_info.Clang_ast_t.ati_lifetime with match attr_info.Clang_ast_t.ati_lifetime with
@ -62,7 +62,7 @@ let pointer_attribute_of_objc_attribute attr_info =
let rec build_array_type translate_decl tenv type_ptr n_opt = let rec build_array_type translate_decl tenv type_ptr n_opt =
let array_type = type_ptr_to_sil_type translate_decl tenv type_ptr in let array_type = type_ptr_to_sil_type translate_decl tenv type_ptr in
let len = Option.map ~f:(fun n -> IntLit.of_int64 (Int64.of_int n)) n_opt in let len = Option.map ~f:(fun n -> IntLit.of_int64 (Int64.of_int n)) n_opt in
Typ.Tarray (array_type, len) Typ.mk (Tarray (array_type, len))
and sil_type_of_attr_type translate_decl tenv type_info attr_info = and sil_type_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
@ -70,14 +70,14 @@ and sil_type_of_attr_type translate_decl tenv type_info attr_info =
(match CAst_utils.get_type type_ptr with (match CAst_utils.get_type type_ptr with
| Some Clang_ast_t.ObjCObjectPointerType (_, {Clang_ast_t.qt_type_ptr}) -> | Some Clang_ast_t.ObjCObjectPointerType (_, {Clang_ast_t.qt_type_ptr}) ->
let typ = type_ptr_to_sil_type translate_decl tenv qt_type_ptr in let typ = type_ptr_to_sil_type translate_decl tenv qt_type_ptr in
Typ.Tptr (typ, pointer_attribute_of_objc_attribute attr_info) Typ.mk (Tptr (typ, pointer_attribute_of_objc_attribute attr_info))
| _ -> type_ptr_to_sil_type translate_decl tenv type_ptr) | _ -> type_ptr_to_sil_type translate_decl tenv type_ptr)
| None -> Typ.Tvoid | None -> Typ.mk Tvoid
and sil_type_of_c_type translate_decl tenv c_type = and sil_type_of_c_type translate_decl tenv c_type : Typ.t =
let open Clang_ast_t in let open Clang_ast_t in
match c_type with match c_type with
| NoneType _ -> Typ.Tvoid | NoneType _ -> Typ.mk Tvoid
| BuiltinType (_, builtin_type_kind) -> | BuiltinType (_, builtin_type_kind) ->
sil_type_of_builtin_type_kind builtin_type_kind sil_type_of_builtin_type_kind builtin_type_kind
| PointerType (_, {Clang_ast_t.qt_type_ptr}) | PointerType (_, {Clang_ast_t.qt_type_ptr})
@ -85,12 +85,12 @@ and sil_type_of_c_type translate_decl tenv c_type =
let typ = type_ptr_to_sil_type translate_decl tenv qt_type_ptr in let typ = type_ptr_to_sil_type translate_decl tenv qt_type_ptr in
if Typ.equal typ (get_builtin_objc_type `ObjCClass) then if Typ.equal typ (get_builtin_objc_type `ObjCClass) then
typ typ
else Typ.Tptr (typ, Typ.Pk_pointer) else Typ.mk (Tptr (typ, Typ.Pk_pointer))
| ObjCObjectType (_, objc_object_type_info) -> | ObjCObjectType (_, objc_object_type_info) ->
type_ptr_to_sil_type translate_decl tenv objc_object_type_info.Clang_ast_t.base_type type_ptr_to_sil_type translate_decl tenv objc_object_type_info.Clang_ast_t.base_type
| BlockPointerType (_, type_ptr) -> | BlockPointerType (_, type_ptr) ->
let typ = type_ptr_to_sil_type translate_decl tenv type_ptr in let typ = type_ptr_to_sil_type translate_decl tenv type_ptr in
Typ.Tptr (typ, Typ.Pk_pointer) Typ.mk (Tptr (typ, Typ.Pk_pointer))
| IncompleteArrayType (_, type_ptr) | IncompleteArrayType (_, type_ptr)
| DependentSizedArrayType (_, type_ptr) | DependentSizedArrayType (_, type_ptr)
| VariableArrayType (_, type_ptr) -> | VariableArrayType (_, type_ptr) ->
@ -99,7 +99,7 @@ and sil_type_of_c_type translate_decl tenv c_type =
build_array_type translate_decl tenv type_ptr (Some n) build_array_type translate_decl tenv type_ptr (Some n)
| FunctionProtoType _ | FunctionProtoType _
| FunctionNoProtoType _ -> | FunctionNoProtoType _ ->
Typ.Tfun false Typ.mk (Tfun false)
| ParenType (_, type_ptr) -> | ParenType (_, type_ptr) ->
type_ptr_to_sil_type translate_decl tenv type_ptr type_ptr_to_sil_type translate_decl tenv type_ptr
| DecayedType (_, type_ptr) -> | DecayedType (_, type_ptr) ->
@ -110,20 +110,20 @@ and sil_type_of_c_type translate_decl tenv c_type =
| ElaboratedType (type_info) -> | ElaboratedType (type_info) ->
(match type_info.Clang_ast_t.ti_desugared_type with (match type_info.Clang_ast_t.ti_desugared_type with
Some type_ptr -> type_ptr_to_sil_type translate_decl tenv type_ptr Some type_ptr -> type_ptr_to_sil_type translate_decl tenv type_ptr
| None -> Typ.Tvoid) | None -> Typ.mk Tvoid)
| ObjCInterfaceType (_, pointer) -> | ObjCInterfaceType (_, pointer) ->
decl_ptr_to_sil_type translate_decl tenv pointer decl_ptr_to_sil_type translate_decl tenv pointer
| RValueReferenceType (_, {Clang_ast_t.qt_type_ptr}) | RValueReferenceType (_, {Clang_ast_t.qt_type_ptr})
| LValueReferenceType (_, {Clang_ast_t.qt_type_ptr}) -> | LValueReferenceType (_, {Clang_ast_t.qt_type_ptr}) ->
let typ = type_ptr_to_sil_type translate_decl tenv qt_type_ptr in let typ = type_ptr_to_sil_type translate_decl tenv qt_type_ptr in
Typ.Tptr (typ, Typ.Pk_reference) Typ.mk (Tptr (typ, Typ.Pk_reference))
| AttributedType (type_info, attr_info) -> | AttributedType (type_info, attr_info) ->
sil_type_of_attr_type translate_decl tenv type_info attr_info sil_type_of_attr_type translate_decl tenv type_info attr_info
| _ -> (* TypedefType, etc *) | _ -> (* TypedefType, etc *)
let type_info = Clang_ast_proj.get_type_tuple c_type in let type_info = Clang_ast_proj.get_type_tuple c_type in
match type_info.Clang_ast_t.ti_desugared_type with match type_info.Clang_ast_t.ti_desugared_type with
| Some typ -> type_ptr_to_sil_type translate_decl tenv typ | Some typ -> type_ptr_to_sil_type translate_decl tenv typ
| None -> Typ.Tvoid | None -> Typ.mk Tvoid
and decl_ptr_to_sil_type translate_decl tenv decl_ptr = and decl_ptr_to_sil_type translate_decl tenv decl_ptr =
let open Clang_ast_t in let open Clang_ast_t in
@ -143,11 +143,11 @@ and decl_ptr_to_sil_type translate_decl tenv decl_ptr =
| Some _ -> | Some _ ->
Logging.err_debug "Warning: Wrong decl found for pointer %s " Logging.err_debug "Warning: Wrong decl found for pointer %s "
(Clang_ast_j.string_of_pointer decl_ptr); (Clang_ast_j.string_of_pointer decl_ptr);
Typ.Tvoid Typ.mk Tvoid
| None -> | None ->
Logging.err_debug "Warning: Decl pointer %s not found." Logging.err_debug "Warning: Decl pointer %s not found."
(Clang_ast_j.string_of_pointer decl_ptr); (Clang_ast_j.string_of_pointer decl_ptr);
Typ.Tvoid Typ.mk Tvoid
and clang_type_ptr_to_sil_type translate_decl tenv type_ptr = and clang_type_ptr_to_sil_type translate_decl tenv type_ptr =
try try
@ -158,7 +158,7 @@ and clang_type_ptr_to_sil_type translate_decl tenv type_ptr =
let sil_type = sil_type_of_c_type translate_decl tenv c_type in let sil_type = sil_type_of_c_type translate_decl tenv c_type in
CAst_utils.update_sil_types_map type_ptr sil_type; CAst_utils.update_sil_types_map type_ptr sil_type;
sil_type sil_type
| _ -> Typ.Tvoid) | _ -> Typ.mk Tvoid)
and type_ptr_to_sil_type translate_decl tenv type_ptr = and type_ptr_to_sil_type translate_decl tenv type_ptr =
match type_ptr with match type_ptr with
@ -166,12 +166,12 @@ and type_ptr_to_sil_type translate_decl tenv type_ptr =
| Clang_ast_extend.Builtin kind -> sil_type_of_builtin_type_kind kind | Clang_ast_extend.Builtin kind -> sil_type_of_builtin_type_kind kind
| Clang_ast_extend.PointerOf typ -> | Clang_ast_extend.PointerOf typ ->
let sil_typ = type_ptr_to_sil_type translate_decl tenv typ in let sil_typ = type_ptr_to_sil_type translate_decl tenv typ in
Typ.Tptr (sil_typ, Typ.Pk_pointer) Typ.mk (Tptr (sil_typ, Pk_pointer))
| Clang_ast_extend.ReferenceOf typ -> | Clang_ast_extend.ReferenceOf typ ->
let sil_typ = type_ptr_to_sil_type translate_decl tenv typ in let sil_typ = type_ptr_to_sil_type translate_decl tenv typ in
Typ.Tptr (sil_typ, Typ.Pk_reference) Typ.mk (Tptr (sil_typ, Pk_reference))
| Clang_ast_extend.ClassType typename -> | Clang_ast_extend.ClassType typename ->
Typ.Tstruct typename Typ.mk (Tstruct typename)
| Clang_ast_extend.DeclPtr ptr -> decl_ptr_to_sil_type translate_decl tenv ptr | Clang_ast_extend.DeclPtr ptr -> decl_ptr_to_sil_type translate_decl tenv ptr
| Clang_ast_extend.ErrorType -> Typ.Tvoid | Clang_ast_extend.ErrorType -> Typ.mk Tvoid
| _ -> raise (invalid_arg "unknown variant for type_ptr") | _ -> raise (invalid_arg "unknown variant for type_ptr")

@ -68,8 +68,9 @@ let get_base_class_name_from_category decl =
let process_category type_ptr_to_sil_type tenv class_name decl_info decl_list = let process_category type_ptr_to_sil_type tenv class_name decl_info decl_list =
let decl_fields = CField_decl.get_fields type_ptr_to_sil_type tenv decl_list in let decl_fields = CField_decl.get_fields type_ptr_to_sil_type tenv decl_list in
let class_tn_name = Typ.Name.Objc.from_qual_name class_name in let class_tn_name = Typ.Name.Objc.from_qual_name class_name in
let class_tn_type = Typ.mk (Typ.Tstruct class_tn_name) in
let decl_key = Clang_ast_extend.DeclPtr decl_info.Clang_ast_t.di_pointer in let decl_key = Clang_ast_extend.DeclPtr decl_info.Clang_ast_t.di_pointer in
CAst_utils.update_sil_types_map decl_key (Typ.Tstruct class_tn_name); CAst_utils.update_sil_types_map decl_key class_tn_type;
(match Tenv.lookup tenv class_tn_name with (match Tenv.lookup tenv class_tn_name with
| Some ({ fields } as struct_typ) -> | Some ({ fields } as struct_typ) ->
let new_fields = CGeneral_utils.append_no_duplicates_fields decl_fields fields in let new_fields = CGeneral_utils.append_no_duplicates_fields decl_fields fields in
@ -78,7 +79,7 @@ let process_category type_ptr_to_sil_type tenv class_name decl_info decl_list =
~default:struct_typ ~fields:new_fields ~statics:[] ~methods:[] class_tn_name ); ~default:struct_typ ~fields:new_fields ~statics:[] ~methods:[] class_tn_name );
Logging.out_debug " Updating info for class '%a' in tenv\n" QualifiedCppName.pp class_name Logging.out_debug " Updating info for class '%a' in tenv\n" QualifiedCppName.pp class_name
| _ -> ()); | _ -> ());
Typ.Tstruct class_tn_name class_tn_type
let category_decl type_ptr_to_sil_type tenv decl = let category_decl type_ptr_to_sil_type tenv decl =
let open Clang_ast_t in let open Clang_ast_t in

@ -19,8 +19,8 @@ open! IStd
module L = Logging module L = Logging
let is_pointer_to_objc_class typ = let is_pointer_to_objc_class typ =
match typ with match typ.Typ.desc with
| Typ.Tptr (typ, _) when Typ.is_objc_class typ -> true | Tptr (typ, _) when Typ.is_objc_class typ -> true
| _ -> false | _ -> false
let get_super_interface_decl otdi_super = let get_super_interface_decl otdi_super =
@ -78,8 +78,9 @@ let add_class_to_tenv type_ptr_to_sil_type tenv decl_info name_info decl_list oc
let class_name = CAst_utils.get_qualified_name name_info in let class_name = CAst_utils.get_qualified_name name_info in
Logging.out_debug "ADDING: ObjCInterfaceDecl for '%a'\n" QualifiedCppName.pp class_name; Logging.out_debug "ADDING: ObjCInterfaceDecl for '%a'\n" QualifiedCppName.pp class_name;
let interface_name = Typ.Name.Objc.from_qual_name class_name in let interface_name = Typ.Name.Objc.from_qual_name class_name in
let interface_type = Typ.mk (Tstruct interface_name) in
let decl_key = Clang_ast_extend.DeclPtr decl_info.Clang_ast_t.di_pointer in let decl_key = Clang_ast_extend.DeclPtr decl_info.Clang_ast_t.di_pointer in
CAst_utils.update_sil_types_map decl_key (Typ.Tstruct interface_name); CAst_utils.update_sil_types_map decl_key interface_type;
let decl_supers, decl_fields = let decl_supers, decl_fields =
create_supers_fields type_ptr_to_sil_type tenv decl_list create_supers_fields type_ptr_to_sil_type tenv decl_list
ocidi.Clang_ast_t.otdi_super ocidi.Clang_ast_t.otdi_super
@ -113,7 +114,7 @@ let add_class_to_tenv type_ptr_to_sil_type tenv decl_info name_info decl_list oc
Logging.out_debug " >>>OK. Found typ='%a'\n" Logging.out_debug " >>>OK. Found typ='%a'\n"
(Typ.Struct.pp Pp.text interface_name) st (Typ.Struct.pp Pp.text interface_name) st
| None -> Logging.out_debug " >>>NOT Found!!\n"); | None -> Logging.out_debug " >>>NOT Found!!\n");
Typ.Tstruct interface_name interface_type
(* Interface_type_info has the name of instance variables and the name of methods. *) (* Interface_type_info has the name of instance variables and the name of methods. *)
let interface_declaration type_ptr_to_sil_type tenv decl = let interface_declaration type_ptr_to_sil_type tenv decl =
@ -143,7 +144,7 @@ let interface_impl_declaration type_ptr_to_sil_type tenv decl =
CField_decl.add_missing_fields tenv class_name fields; CField_decl.add_missing_fields tenv class_name fields;
let class_tn_name = Typ.Name.Objc.from_qual_name class_name in let class_tn_name = Typ.Name.Objc.from_qual_name class_name in
let decl_key = Clang_ast_extend.DeclPtr decl_info.Clang_ast_t.di_pointer in let decl_key = Clang_ast_extend.DeclPtr decl_info.Clang_ast_t.di_pointer in
let class_typ = Typ.Tstruct class_tn_name in let class_typ = Typ.mk (Tstruct class_tn_name) in
CAst_utils.update_sil_types_map decl_key class_typ; CAst_utils.update_sil_types_map decl_key class_typ;
class_typ class_typ
| _ -> assert false | _ -> assert false

@ -26,11 +26,12 @@ let protocol_decl type_ptr_to_sil_type tenv decl =
(* It may turn out that we need a more specific treatment for protocols*) (* It may turn out that we need a more specific treatment for protocols*)
Logging.out_debug "ADDING: ObjCProtocolDecl for '%a'\n" QualifiedCppName.pp name; Logging.out_debug "ADDING: ObjCProtocolDecl for '%a'\n" QualifiedCppName.pp name;
let protocol_name = Typ.Name.Objc.protocol_from_qual_name name in let protocol_name = Typ.Name.Objc.protocol_from_qual_name name in
let protocol_type = Typ.mk (Tstruct protocol_name) in
let decl_key = Clang_ast_extend.DeclPtr decl_info.Clang_ast_t.di_pointer in let decl_key = Clang_ast_extend.DeclPtr decl_info.Clang_ast_t.di_pointer in
CAst_utils.update_sil_types_map decl_key (Typ.Tstruct protocol_name); CAst_utils.update_sil_types_map decl_key protocol_type;
ignore( Tenv.mk_struct tenv ~methods:[] protocol_name ); ignore( Tenv.mk_struct tenv ~methods:[] protocol_name );
add_protocol_super type_ptr_to_sil_type tenv obj_c_protocol_decl_info; add_protocol_super type_ptr_to_sil_type tenv obj_c_protocol_decl_info;
Typ.Tstruct protocol_name protocol_type
| _ -> assert false | _ -> assert false
let is_protocol decl = let is_protocol decl =

@ -117,7 +117,7 @@ let check_condition tenv case_zero find_canonical_duplicate curr_pdesc
(* That always happens in the bytecode generated by try-with-resources. *) (* That always happens in the bytecode generated by try-with-resources. *)
let loc = Procdesc.Node.get_loc node in let loc = Procdesc.Node.get_loc node in
let throwable_found = ref false in let throwable_found = ref false in
let typ_is_throwable = function let typ_is_throwable {Typ.desc} = match desc with
| Typ.Tstruct (Typ.JavaClass _ as name) -> | Typ.Tstruct (Typ.JavaClass _ as name) ->
String.equal (Typ.Name.name name) "java.lang.Throwable" String.equal (Typ.Name.name name) "java.lang.Throwable"
| _ -> false in | _ -> false in
@ -242,7 +242,7 @@ let check_constructor_initialization tenv
if Typ.Procname.is_constructor curr_pname if Typ.Procname.is_constructor curr_pname
then begin then begin
match PatternMatch.get_this_type (Procdesc.get_attributes curr_pdesc) with match PatternMatch.get_this_type (Procdesc.get_attributes curr_pdesc) with
| Some (Tptr (Tstruct name as ts, _)) -> ( | Some ({desc=Tptr ({desc=Tstruct name} as ts, _)}) -> (
match Tenv.lookup tenv name with match Tenv.lookup tenv name with
| Some { fields } -> | Some { fields } ->
let do_field (fn, ft, _) = let do_field (fn, ft, _) =

@ -479,7 +479,7 @@ let typecheck_instr
(* check if there are errors in exp1 *) (* check if there are errors in exp1 *)
let typecheck_expr_for_errors typestate1 exp1 loc1 : unit = let typecheck_expr_for_errors typestate1 exp1 loc1 : unit =
ignore (typecheck_expr_simple typestate1 exp1 Typ.Tvoid TypeOrigin.Undef loc1) in ignore (typecheck_expr_simple typestate1 exp1 (Typ.mk Tvoid) TypeOrigin.Undef loc1) in
match instr with match instr with
| Sil.Remove_temps (idl, _) -> | Sil.Remove_temps (idl, _) ->
@ -565,7 +565,7 @@ let typecheck_instr
TypeState.add_id TypeState.add_id
id id
( (
Typ.Tint (Typ.IInt), Typ.mk (Tint (Typ.IInt)),
TypeAnnotation.const AnnotatedSignature.Nullable false TypeOrigin.New, TypeAnnotation.const AnnotatedSignature.Nullable false TypeOrigin.New,
[loc] [loc]
) )
@ -1006,7 +1006,7 @@ let typecheck_instr
Pvar.mk (Mangled.from_string e_str) curr_pname in Pvar.mk (Mangled.from_string e_str) curr_pname in
let e1 = Exp.Lvar pvar in let e1 = Exp.Lvar pvar in
let (typ, ta, _) = let (typ, ta, _) =
typecheck_expr_simple typestate e1 Typ.Tvoid TypeOrigin.ONone loc in typecheck_expr_simple typestate e1 (Typ.mk Tvoid) TypeOrigin.ONone loc in
let range = (typ, ta, [loc]) in let range = (typ, ta, [loc]) in
let typestate1 = TypeState.add pvar range typestate in let typestate1 = TypeState.add pvar range typestate in
typestate1, e1, EradicateChecks.From_containsKey typestate1, e1, EradicateChecks.From_containsKey
@ -1027,7 +1027,6 @@ let typecheck_instr
| Exp.Lvar pvar -> | Exp.Lvar pvar ->
pvar_apply loc handle_pvar typestate2 pvar pvar_apply loc handle_pvar typestate2 pvar
| _ -> typestate2 in | _ -> typestate2 in
begin match c with begin match c with
| Exp.BinOp (Binop.Eq, Exp.Const (Const.Cint i), e) | Exp.BinOp (Binop.Eq, Exp.Const (Const.Cint i), e)
| Exp.BinOp (Binop.Eq, e, Exp.Const (Const.Cint i)) when IntLit.iszero i -> | Exp.BinOp (Binop.Eq, e, Exp.Const (Const.Cint i)) when IntLit.iszero i ->
@ -1039,7 +1038,7 @@ let typecheck_instr
typestate, e, EradicateChecks.From_condition in typestate, e, EradicateChecks.From_condition in
let e', typestate2 = convert_complex_exp_to_pvar node' false e1 typestate1 loc in let e', typestate2 = convert_complex_exp_to_pvar node' false e1 typestate1 loc in
let (typ, ta, _) = let (typ, ta, _) =
typecheck_expr_simple typestate2 e' Typ.Tvoid TypeOrigin.ONone loc in typecheck_expr_simple typestate2 e' (Typ.mk Tvoid) TypeOrigin.ONone loc in
if checks.eradicate then if checks.eradicate then
EradicateChecks.check_zero tenv EradicateChecks.check_zero tenv
@ -1086,7 +1085,7 @@ let typecheck_instr
end in end in
let e', typestate2 = convert_complex_exp_to_pvar node' false e1 typestate1 loc in let e', typestate2 = convert_complex_exp_to_pvar node' false e1 typestate1 loc in
let (typ, ta, _) = let (typ, ta, _) =
typecheck_expr_simple typestate2 e' Typ.Tvoid TypeOrigin.ONone loc in typecheck_expr_simple typestate2 e' (Typ.mk Tvoid) TypeOrigin.ONone loc in
if checks.eradicate then if checks.eradicate then
EradicateChecks.check_nonzero tenv find_canonical_duplicate curr_pdesc EradicateChecks.check_nonzero tenv find_canonical_duplicate curr_pdesc

@ -21,7 +21,7 @@ let try_create_lifecycle_trace name lifecycle_name lifecycle_procs tenv =
| Typ.JavaClass _ -> | Typ.JavaClass _ ->
if PatternMatch.is_subtype tenv name lifecycle_name && if PatternMatch.is_subtype tenv name lifecycle_name &&
not (AndroidFramework.is_android_lib_class name) then not (AndroidFramework.is_android_lib_class name) then
let ptr_to_struct_typ = Some (Typ.Tptr (Tstruct name, Pk_pointer)) in let ptr_to_struct_typ = Some (Typ.mk (Tptr (Typ.mk (Tstruct name), Pk_pointer))) in
List.fold List.fold
~f:(fun trace lifecycle_proc -> ~f:(fun trace lifecycle_proc ->
(* given a lifecycle subclass T, resolve the call T.lifecycle_proc() to the procname (* given a lifecycle subclass T, resolve the call T.lifecycle_proc() to the procname

@ -74,7 +74,7 @@ let inhabit_alloc sizeof_typ sizeof_len ret_typ alloc_kind env =
let call_instr = let call_instr =
let fun_new = fun_exp_from_name alloc_kind in let fun_new = fun_exp_from_name alloc_kind in
let sizeof_exp = Exp.Sizeof (sizeof_typ, sizeof_len, Subtype.exact) in let sizeof_exp = Exp.Sizeof (sizeof_typ, sizeof_len, Subtype.exact) in
let args = [(sizeof_exp, Typ.Tptr (ret_typ, Typ.Pk_pointer))] in let args = [(sizeof_exp, Typ.mk (Tptr (ret_typ, Typ.Pk_pointer)))] in
Sil.Call (Some (retval, ret_typ), fun_new, args, env.pc, cf_alloc) in Sil.Call (Some (retval, ret_typ), fun_new, args, env.pc, cf_alloc) in
(inhabited_exp, env_add_instr call_instr env) (inhabited_exp, env_add_instr call_instr env)
@ -83,19 +83,19 @@ let inhabit_alloc sizeof_typ sizeof_len ret_typ alloc_kind env =
let rec inhabit_typ tenv typ cfg env = let rec inhabit_typ tenv typ cfg env =
try (TypMap.find typ env.cache, env) try (TypMap.find typ env.cache, env)
with Not_found -> with Not_found ->
let inhabit_internal typ env = match typ with let inhabit_internal typ env = match typ.Typ.desc with
| Typ.Tptr (Typ.Tarray (inner_typ, Some _), Typ.Pk_pointer) -> | Typ.Tptr ({desc=Tarray (inner_typ, Some _)}, Typ.Pk_pointer) ->
let len = Exp.Const (Const.Cint (IntLit.one)) in let len = Exp.Const (Const.Cint (IntLit.one)) in
let arr_typ = Typ.Tarray (inner_typ, Some IntLit.one) in let arr_typ = Typ.mk (Tarray (inner_typ, Some IntLit.one)) in
inhabit_alloc arr_typ (Some len) typ BuiltinDecl.__new_array env inhabit_alloc arr_typ (Some len) typ BuiltinDecl.__new_array env
| Typ.Tptr (typ, Typ.Pk_pointer) as ptr_to_typ -> | Typ.Tptr (typ, Typ.Pk_pointer) ->
(* TODO (t4575417): this case does not work correctly for enums, but they are currently (* TODO (t4575417): this case does not work correctly for enums, but they are currently
* broken in Infer anyway (see t4592290) *) * broken in Infer anyway (see t4592290) *)
let (allocated_obj_exp, env) = inhabit_alloc typ None typ BuiltinDecl.__new env in let (allocated_obj_exp, env) = inhabit_alloc typ None typ BuiltinDecl.__new env in
(* select methods that are constructors and won't force us into infinite recursion because (* select methods that are constructors and won't force us into infinite recursion because
* we are already inhabiting one of their argument types *) * we are already inhabiting one of their argument types *)
let get_all_suitable_constructors (typ: Typ.t) = let get_all_suitable_constructors (typ: Typ.t) =
match typ with match typ.desc with
| Tstruct name when Typ.Name.is_class name -> ( | Tstruct name when Typ.Name.is_class name -> (
match Tenv.lookup tenv name with match Tenv.lookup tenv name with
| Some { methods } -> | Some { methods } ->
@ -116,7 +116,7 @@ let rec inhabit_typ tenv typ cfg env =
(* arbitrarily choose a constructor for typ and invoke it. eventually, we may want to (* arbitrarily choose a constructor for typ and invoke it. eventually, we may want to
* nondeterministically call all possible constructors instead *) * nondeterministically call all possible constructors instead *)
let env = let env =
inhabit_constructor tenv constructor (allocated_obj_exp, ptr_to_typ) cfg env in inhabit_constructor tenv constructor (allocated_obj_exp, typ) cfg env in
(* try to get the unqualified name as a class (e.g., Object for java.lang.Object so we (* try to get the unqualified name as a class (e.g., Object for java.lang.Object so we
* we can use it as a descriptive local variable name in the harness *) * we can use it as a descriptive local variable name in the harness *)
let typ_class_name = let typ_class_name =
@ -133,14 +133,14 @@ let rec inhabit_typ tenv typ cfg env =
let fresh_local_exp = let fresh_local_exp =
Exp.Lvar (Pvar.mk typ_class_name (Typ.Procname.Java env.harness_name)) in Exp.Lvar (Pvar.mk typ_class_name (Typ.Procname.Java env.harness_name)) in
let write_to_local_instr = let write_to_local_instr =
Sil.Store (fresh_local_exp, ptr_to_typ, allocated_obj_exp, env.pc) in Sil.Store (fresh_local_exp, typ, allocated_obj_exp, env.pc) in
let env' = env_add_instr write_to_local_instr env in let env' = env_add_instr write_to_local_instr env in
let fresh_id = Ident.create_fresh Ident.knormal in let fresh_id = Ident.create_fresh Ident.knormal in
let read_from_local_instr = Sil.Load (fresh_id, fresh_local_exp, ptr_to_typ, env'.pc) in let read_from_local_instr = Sil.Load (fresh_id, fresh_local_exp, typ, env'.pc) in
(Exp.Var fresh_id, env_add_instr read_from_local_instr env') (Exp.Var fresh_id, env_add_instr read_from_local_instr env')
| Typ.Tint (_) -> (Exp.Const (Const.Cint (IntLit.zero)), env) | Typ.Tint (_) -> (Exp.Const (Const.Cint (IntLit.zero)), env)
| Typ.Tfloat (_) -> (Exp.Const (Const.Cfloat 0.0), env) | Typ.Tfloat (_) -> (Exp.Const (Const.Cfloat 0.0), env)
| typ -> | _ ->
L.err "Couldn't inhabit typ: %a@." (Typ.pp Pp.text) typ; L.err "Couldn't inhabit typ: %a@." (Typ.pp Pp.text) typ;
assert false in assert false in
let (inhabited_exp, env') = let (inhabited_exp, env') =
@ -173,7 +173,7 @@ and inhabit_constructor tenv constr_name (allocated_obj, obj_type) cfg env =
let inhabit_call_with_args procname procdesc args env = let inhabit_call_with_args procname procdesc args env =
let retval = let retval =
let ret_typ = Procdesc.get_ret_type procdesc in let ret_typ = Procdesc.get_ret_type procdesc in
let is_void = Typ.equal ret_typ Typ.Tvoid in let is_void = Typ.equal_desc ret_typ.Typ.desc Typ.Tvoid in
if is_void then None else Some (Ident.create_fresh Ident.knormal, ret_typ) in if is_void then None else Some (Ident.create_fresh Ident.knormal, ret_typ) in
let call_instr = let call_instr =
let fun_exp = fun_exp_from_name procname in let fun_exp = fun_exp_from_name procname in

@ -175,7 +175,7 @@ let translate_locals program tenv formals bytecode jbir_code =
Array.fold Array.fold
~f:(fun accu jbir_var -> ~f:(fun accu jbir_var ->
let var = Mangled.from_string (JBir.var_name_g jbir_var) in let var = Mangled.from_string (JBir.var_name_g jbir_var) in
collect accu (var, Typ.Tvoid)) collect accu (var, Typ.mk Tvoid))
~init:with_bytecode_vars ~init:with_bytecode_vars
(JBir.vars jbir_code) in (JBir.vars jbir_code) in
snd with_jbir_vars snd with_jbir_vars
@ -426,13 +426,13 @@ let rec expression (context : JContext.t) pc expr =
| JBir.Neg _ -> (instrs, Exp.UnOp (Unop.Neg, sil_ex, Some type_of_expr), type_of_expr) | JBir.Neg _ -> (instrs, Exp.UnOp (Unop.Neg, sil_ex, Some type_of_expr), type_of_expr)
| JBir.ArrayLength -> | JBir.ArrayLength ->
let array_typ_no_ptr = let array_typ_no_ptr =
match type_of_ex with match type_of_ex.Typ.desc with
| Typ.Tptr (typ, _) -> typ | Typ.Tptr (typ, _) -> typ
| _ -> type_of_ex in | _ -> type_of_ex in
let deref = create_sil_deref sil_ex array_typ_no_ptr loc in let deref = create_sil_deref sil_ex array_typ_no_ptr loc in
let args = [(sil_ex, type_of_ex)] in let args = [(sil_ex, type_of_ex)] in
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Ident.create_fresh Ident.knormal in
let ret_typ = Typ.Tint IInt in let ret_typ = Typ.mk (Tint IInt) in
let call_instr = let call_instr =
Sil.Call Sil.Call
(Some (ret_id, ret_typ), builtin_get_array_length, args, loc, CallFlags.default) in (Some (ret_id, ret_typ), builtin_get_array_length, args, loc, CallFlags.default) in
@ -453,10 +453,10 @@ let rec expression (context : JContext.t) pc expr =
| JBir.InstanceOf _ -> Exp.Const (Const.Cfun BuiltinDecl.__instanceof) | JBir.InstanceOf _ -> Exp.Const (Const.Cfun BuiltinDecl.__instanceof)
| JBir.Cast _ -> Exp.Const (Const.Cfun BuiltinDecl.__cast) | JBir.Cast _ -> Exp.Const (Const.Cfun BuiltinDecl.__cast)
| _ -> assert false) in | _ -> assert false) in
let args = [(sil_ex, type_of_ex); (sizeof_expr, Typ.Tvoid)] in let args = [(sil_ex, type_of_ex); (sizeof_expr, Typ.mk Tvoid)] in
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Ident.create_fresh Ident.knormal in
let call = let call =
Sil.Call (Some (ret_id, Tint IBool), builtin, args, loc, CallFlags.default) in Sil.Call (Some (ret_id, Typ.mk (Tint IBool)), builtin, args, loc, CallFlags.default) in
let res_ex = Exp.Var ret_id in let res_ex = Exp.Var ret_id in
(instrs @ [call], res_ex, type_of_expr) (instrs @ [call], res_ex, type_of_expr)
end end
@ -467,7 +467,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.Tarray (type_of_expr, None) in let array_typ = Typ.mk (Tarray (type_of_expr, None)) 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 = let load_instr =
@ -548,7 +548,7 @@ let method_invocation
match sil_obj_expr with match sil_obj_expr with
| Exp.Var _ when is_non_constructor_call && not Config.report_runtime_exceptions -> | Exp.Var _ when is_non_constructor_call && not Config.report_runtime_exceptions ->
let obj_typ_no_ptr = let obj_typ_no_ptr =
match sil_obj_type with match sil_obj_type.Typ.desc with
| Typ.Tptr (typ, _) -> typ | Typ.Tptr (typ, _) -> typ
| _ -> sil_obj_type in | _ -> sil_obj_type in
[create_sil_deref sil_obj_expr obj_typ_no_ptr loc] [create_sil_deref sil_obj_expr obj_typ_no_ptr loc]
@ -571,7 +571,7 @@ let method_invocation
let callee_fun = Exp.Const (Const.Cfun callee_procname) in let callee_fun = Exp.Const (Const.Cfun callee_procname) in
let return_type = let return_type =
match JBasics.ms_rtype ms with match JBasics.ms_rtype ms with
| None -> Typ.Tvoid | None -> Typ.mk Tvoid
| Some vt -> JTransType.value_type program tenv vt in | Some vt -> JTransType.value_type program tenv vt in
let call_ret_instrs sil_var = let call_ret_instrs sil_var =
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Ident.create_fresh Ident.knormal in
@ -621,7 +621,7 @@ let get_array_length context pc expr_list content_type =
(instrs @ other_instrs, sil_len_expr :: other_exprs) in (instrs @ other_instrs, sil_len_expr :: other_exprs) 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.Tarray (content_type, None), Some sil_len_expr) in (Typ.mk (Tarray (content_type, None)), Some sil_len_expr) 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) in List.fold_right ~f:get_array_type_len sil_len_exprs ~init:(content_type, None) in
let array_size = Exp.Sizeof (array_type, array_len, Subtype.exact) in let array_size = Exp.Sizeof (array_type, array_len, Subtype.exact) in
@ -689,7 +689,7 @@ let assume_not_null loc sil_expr =
let not_null_expr = let not_null_expr =
Exp.BinOp (Binop.Ne, sil_expr, Exp.null) in Exp.BinOp (Binop.Ne, sil_expr, Exp.null) in
let assume_call_flag = { CallFlags.default with CallFlags.cf_noreturn = true; } in let assume_call_flag = { CallFlags.default with CallFlags.cf_noreturn = true; } in
let call_args = [(not_null_expr, Typ.Tint Typ.IBool)] in let call_args = [(not_null_expr, Typ.mk (Tint Typ.IBool))] in
Sil.Call (None, builtin_infer_assume, call_args, loc, assume_call_flag) Sil.Call (None, builtin_infer_assume, call_args, loc, assume_call_flag)
@ -711,7 +711,7 @@ let rec instruction (context : JContext.t) pc instr : translation =
let instrs, sil_expr, sil_type = expression context pc expr in let instrs, sil_expr, sil_type = expression context pc expr in
let builtin_const = Exp.Const (Const.Cfun builtin) in let builtin_const = Exp.Const (Const.Cfun builtin) in
let instr = Sil.Call (None, builtin_const, [(sil_expr, sil_type)], loc, CallFlags.default) in let instr = Sil.Call (None, builtin_const, [(sil_expr, sil_type)], loc, CallFlags.default) in
let typ_no_ptr = match sil_type with let typ_no_ptr = match sil_type.Typ.desc with
| Typ.Tptr (typ, _) -> typ | Typ.Tptr (typ, _) -> typ
| _ -> sil_type in | _ -> sil_type in
let deref_instr = create_sil_deref sil_expr typ_no_ptr loc in let deref_instr = create_sil_deref sil_expr typ_no_ptr loc in
@ -1009,7 +1009,7 @@ let rec instruction (context : JContext.t) pc instr : translation =
and sizeof_expr = and sizeof_expr =
JTransType.sizeof_of_object_type program tenv object_type Subtype.subtypes_instof in JTransType.sizeof_of_object_type program tenv object_type Subtype.subtypes_instof in
let check_cast = Exp.Const (Const.Cfun BuiltinDecl.__instanceof) in let check_cast = Exp.Const (Const.Cfun BuiltinDecl.__instanceof) in
let args = [(sil_expr, sil_type); (sizeof_expr, Typ.Tvoid)] in let args = [(sil_expr, sil_type); (sizeof_expr, Typ.mk Tvoid)] in
let call = Sil.Call (Some (ret_id, ret_type), check_cast, args, loc, CallFlags.default) in let call = Sil.Call (Some (ret_id, ret_type), check_cast, args, loc, CallFlags.default) in
let res_ex = Exp.Var ret_id in let res_ex = Exp.Var ret_id in
let is_instance_node = let is_instance_node =

@ -65,16 +65,16 @@ let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handle
| Some cn -> cn in | Some cn -> cn in
match JTransType.get_class_type match JTransType.get_class_type
context.program (JContext.get_tenv context) class_name with context.program (JContext.get_tenv context) class_name with
| Typ.Tptr (typ, _) -> typ | {Typ.desc=Tptr (typ, _)} -> typ
| _ -> assert false in | _ -> assert false in
let id_instanceof = Ident.create_fresh Ident.knormal in let id_instanceof = Ident.create_fresh Ident.knormal in
let instr_call_instanceof = let instr_call_instanceof =
let instanceof_builtin = Exp.Const (Const.Cfun BuiltinDecl.__instanceof) in let instanceof_builtin = Exp.Const (Const.Cfun BuiltinDecl.__instanceof) in
let args = [ let args = [
(Exp.Var id_exn_val, Typ.Tptr(exn_type, Typ.Pk_pointer)); (Exp.Var id_exn_val, Typ.mk (Tptr(exn_type, Typ.Pk_pointer)));
(Exp.Sizeof (exn_type, None, Subtype.exact), Typ.Tvoid)] in (Exp.Sizeof (exn_type, None, Subtype.exact), Typ.mk Tvoid)] in
Sil.Call Sil.Call
(Some (id_instanceof, Tint IBool), instanceof_builtin, args, loc, CallFlags.default) in (Some (id_instanceof, Typ.mk (Tint IBool)), instanceof_builtin, args, loc, CallFlags.default) in
let if_kind = Sil.Ik_switch in let if_kind = Sil.Ik_switch in
let instr_prune_true = Sil.Prune (Exp.Var id_instanceof, loc, true, if_kind) in let instr_prune_true = Sil.Prune (Exp.Var id_instanceof, loc, true, if_kind) in
let instr_prune_false = let instr_prune_false =

@ -18,32 +18,32 @@ open Sawja_pack
exception Type_tranlsation_error of string exception Type_tranlsation_error of string
let basic_type = function let basic_type = function
| `Int -> Typ.Tint Typ.IInt | `Int -> Typ.mk (Tint Typ.IInt)
| `Bool -> Typ.Tint Typ.IBool | `Bool -> Typ.mk (Tint Typ.IBool)
| `Byte -> Typ.Tint Typ.IChar | `Byte -> Typ.mk (Tint Typ.IChar)
| `Char -> Typ.Tint Typ.IChar | `Char -> Typ.mk (Tint Typ.IChar)
| `Double -> Typ.Tfloat Typ.FDouble | `Double -> Typ.mk (Tfloat Typ.FDouble)
| `Float -> Typ.Tfloat Typ.FFloat | `Float -> Typ.mk (Tfloat Typ.FFloat)
| `Long -> Typ.Tint Typ.ILong | `Long -> Typ.mk (Tint Typ.ILong)
| `Short -> Typ.Tint Typ.IShort | `Short -> Typ.mk (Tint Typ.IShort)
let cast_type = function let cast_type = function
| JBir.F2I | JBir.F2I
| JBir.L2I | JBir.L2I
| JBir.D2I -> Typ.Tint Typ.IInt | JBir.D2I -> Typ.mk (Typ.Tint Typ.IInt)
| JBir.D2L | JBir.D2L
| JBir.F2L | JBir.F2L
| JBir.I2L -> Typ.Tint Typ.ILong | JBir.I2L -> Typ.mk (Typ.Tint Typ.ILong)
| JBir.I2F | JBir.I2F
| JBir.L2F | JBir.L2F
| JBir.D2F -> Typ.Tfloat Typ.FFloat | JBir.D2F -> Typ.mk (Typ.Tfloat Typ.FFloat)
| JBir.L2D | JBir.L2D
| JBir.F2D | JBir.F2D
| JBir.I2D -> Typ.Tfloat Typ.FDouble | JBir.I2D -> Typ.mk (Typ.Tfloat Typ.FDouble)
| JBir.I2B -> Typ.Tint Typ.IBool | JBir.I2B -> Typ.mk (Typ.Tint Typ.IBool)
| JBir.I2C -> Typ.Tint Typ.IChar | JBir.I2C -> Typ.mk (Typ.Tint Typ.IChar)
| JBir.I2S -> Typ.Tint Typ.IShort | JBir.I2S -> Typ.mk (Typ.Tint Typ.IShort)
let const_type const = let const_type const =
@ -61,7 +61,7 @@ let typename_of_classname cn =
Typ.Name.Java.from_string (JBasics.cn_name cn) Typ.Name.Java.from_string (JBasics.cn_name cn)
let rec get_named_type vt = let rec get_named_type vt : Typ.t =
match vt with match vt with
| JBasics.TBasic bt -> basic_type bt | JBasics.TBasic bt -> basic_type bt
| JBasics.TObject ot -> | JBasics.TObject ot ->
@ -69,13 +69,14 @@ let rec get_named_type vt =
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.Tptr (Typ.Tarray (content_type, None), Typ.Pk_pointer) Typ.mk (Tptr (Typ.mk (Tarray (content_type, None)), Typ.Pk_pointer))
| JBasics.TClass cn -> Typ.Tptr (Typ.Tstruct (typename_of_classname cn), Typ.Pk_pointer) | JBasics.TClass cn ->
Typ.mk (Tptr (Typ.mk (Tstruct (typename_of_classname cn)), Typ.Pk_pointer))
end end
let extract_cn_type_np typ = let extract_cn_type_np typ =
match typ with match typ.Typ.desc with
| Typ.Tptr(vtyp, Typ.Pk_pointer) -> | Typ.Tptr(vtyp, Typ.Pk_pointer) ->
vtyp vtyp
| _ -> typ | _ -> typ
@ -83,12 +84,12 @@ let extract_cn_type_np typ =
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.Tptr(Typ.Tarray (content_typ, None), Typ.Pk_pointer) Typ.mk (Tptr(Typ.mk (Tarray (content_typ, None)), Typ.Pk_pointer))
else typ else typ
let extract_cn_no_obj typ = let extract_cn_no_obj typ =
match typ with match typ.Typ.desc with
| Typ.Tptr (Tstruct (JavaClass _ as name), Pk_pointer) -> | Typ.Tptr ({desc=Tstruct (JavaClass _ as name)}, Pk_pointer) ->
let class_name = JBasics.make_cn (Typ.Name.name name) in let class_name = JBasics.make_cn (Typ.Name.name name) in
if JBasics.cn_equal class_name JBasics.java_lang_object then None if JBasics.cn_equal class_name JBasics.java_lang_object then None
else else
@ -340,10 +341,10 @@ and get_class_struct_typ program tenv cn =
let get_class_type_no_pointer program tenv cn = let get_class_type_no_pointer program tenv cn =
ignore (get_class_struct_typ program tenv cn); ignore (get_class_struct_typ program tenv cn);
Typ.Tstruct (typename_of_classname cn) Typ.mk (Tstruct (typename_of_classname cn))
let get_class_type program tenv cn = let get_class_type program tenv cn =
Typ.Tptr (get_class_type_no_pointer program tenv cn, Pk_pointer) Typ.mk (Tptr (get_class_type_no_pointer program tenv cn, Pk_pointer))
(** return true if [field_name] is the autogenerated C.$assertionsDisabled field for class C *) (** return true if [field_name] is the autogenerated C.$assertionsDisabled field for class C *)
let is_autogenerated_assert_field field_name = let is_autogenerated_assert_field field_name =
@ -362,7 +363,8 @@ let is_closeable program tenv typ =
let rec object_type program tenv ot = let rec object_type program tenv ot =
match ot with match ot with
| JBasics.TClass cn -> get_class_type program tenv cn | JBasics.TClass cn -> get_class_type program tenv cn
| JBasics.TArray at -> Typ.Tptr (Typ.Tarray (value_type program tenv at, None), Typ.Pk_pointer) | JBasics.TArray at ->
Typ.mk (Tptr (Typ.mk (Tarray (value_type program tenv at, None)), Typ.Pk_pointer))
(** translate a value type *) (** translate a value type *)
and value_type program tenv vt = and value_type program tenv vt =
@ -373,7 +375,7 @@ and value_type program tenv vt =
(** Translate object types into Exp.Sizeof expressions *) (** Translate object types into Exp.Sizeof expressions *)
let sizeof_of_object_type program tenv ot subtypes = let sizeof_of_object_type program tenv ot subtypes =
match object_type program tenv ot with match (object_type program tenv ot).Typ.desc with
| Typ.Tptr (typ, _) -> | Typ.Tptr (typ, _) ->
Exp.Sizeof (typ, None, subtypes) Exp.Sizeof (typ, None, subtypes)
| _ -> | _ ->
@ -407,8 +409,8 @@ let get_var_type context var =
let extract_array_type typ = let extract_array_type typ =
match typ with match typ.Typ.desc with
| Typ.Tptr(Typ.Tarray (vtyp, _), Typ.Pk_pointer) -> vtyp | Typ.Tptr({desc=Tarray (vtyp, _)}, Typ.Pk_pointer) -> vtyp
| _ -> typ | _ -> typ
@ -433,7 +435,7 @@ let rec expr_type (context : JContext.t) expr =
specified in ms. *) specified in ms. *)
let return_type program tenv ms = let return_type program tenv ms =
match JBasics.ms_rtype ms with match JBasics.ms_rtype ms with
| None -> Typ.Tvoid | None -> Typ.mk Tvoid
| Some vt -> value_type program tenv vt | Some vt -> value_type program tenv vt

@ -24,8 +24,8 @@ include
| _ -> assert false | _ -> assert false
let handle_unknown_call pname ret_typ_opt actuals tenv = let handle_unknown_call pname ret_typ_opt actuals tenv =
let types_match typ class_string tenv = match typ with let types_match typ class_string tenv = match typ.Typ.desc with
| Typ.Tptr (Tstruct original_typename, _) -> | Typ.Tptr ({desc=Tstruct original_typename}, _) ->
PatternMatch.supertype_exists PatternMatch.supertype_exists
tenv tenv
(fun typename _ -> String.equal (Typ.Name.name typename) class_string) (fun typename _ -> String.equal (Typ.Name.name typename) class_string)
@ -45,10 +45,10 @@ include
[] []
| _ when Typ.Procname.is_constructor pname -> | _ when Typ.Procname.is_constructor pname ->
[TaintSpec.Propagate_to_receiver] [TaintSpec.Propagate_to_receiver]
| _, _, (Some Typ.Tvoid | None) when not is_static -> | _, _, (Some {Typ.desc=Tvoid} | None) when not is_static ->
(* for instance methods with no return value, propagate the taint to the receiver *) (* for instance methods with no return value, propagate the taint to the receiver *)
[TaintSpec.Propagate_to_receiver] [TaintSpec.Propagate_to_receiver]
| classname, _, Some (Typ.Tptr _ | Tstruct _) -> | classname, _, Some ({Typ.desc=Tptr _ | Tstruct _}) ->
begin begin
match actuals with match actuals with
| (_, receiver_typ) :: _ | (_, receiver_typ) :: _
@ -70,8 +70,8 @@ include
failwithf "Non-Java procname %a in Java analysis@." Typ.Procname.pp pname failwithf "Non-Java procname %a in Java analysis@." Typ.Procname.pp pname
let is_taintable_type typ= let is_taintable_type typ=
match typ with match typ.Typ.desc with
| Typ.Tptr (Tstruct (JavaClass typename), _) | Tstruct (JavaClass typename) -> | Typ.Tptr ({desc=Tstruct (JavaClass typename)}, _) | Tstruct (JavaClass typename) ->
begin begin
match Mangled.to_string_full typename with match Mangled.to_string_full typename with
| "android.content.Intent" | "android.content.Intent"

@ -85,8 +85,8 @@ module SourceKind = struct
name, typ, None in name, typ, None in
let taint_formals_with_types type_strs kind formals = let taint_formals_with_types type_strs kind formals =
let taint_formal_with_types ((formal_name, formal_typ) as formal) = let taint_formal_with_types ((formal_name, formal_typ) as formal) =
let matches_classname = match formal_typ with let matches_classname = match formal_typ.Typ.desc with
| Typ.Tptr (Tstruct typename, _) -> | Tptr ({desc=Tstruct typename}, _) ->
List.mem ~equal:String.equal type_strs (Typ.Name.name typename) List.mem ~equal:String.equal type_strs (Typ.Name.name typename)
| _ -> | _ ->
false in false in

@ -203,9 +203,9 @@ module Make (TaintSpecification : TaintSpec.S) = struct
match AccessPath.of_lhs_exp actual_exp actual_typ ~f_resolve_id with match AccessPath.of_lhs_exp actual_exp actual_typ ~f_resolve_id with
| Some actual_ap_raw -> | Some actual_ap_raw ->
let actual_ap = let actual_ap =
let is_array_typ = match actual_typ with let is_array_typ = match actual_typ.Typ.desc with
| Typ.Tptr (Tarray _, _) (* T* [] (Java-style) *) | Typ.Tptr ({desc=Tarray _}, _) (* T* [] (Java-style) *)
| Tptr (Tptr _, _) (* T** (C/C++ style 1) *) | Tptr ({desc=Tptr _}, _) (* T** (C/C++ style 1) *)
| Tarray _ (* T[] C/C++ style 2 *) -> | Tarray _ (* T[] C/C++ style 2 *) ->
true true
| _ -> | _ ->
@ -330,7 +330,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
astate astate
| Sil.Store (Exp.Lvar lhs_pvar, _, rhs_exp, _) | Sil.Store (Exp.Lvar lhs_pvar, _, rhs_exp, _)
when Pvar.is_return lhs_pvar && Exp.is_null_literal rhs_exp && when Pvar.is_return lhs_pvar && Exp.is_null_literal rhs_exp &&
Typ.equal Tvoid (Procdesc.get_ret_type proc_data.pdesc) -> Typ.equal_desc Tvoid (Procdesc.get_ret_type proc_data.pdesc).desc ->
(* similar to the case above; the Java frontend translates "return no exception" as (* similar to the case above; the Java frontend translates "return no exception" as
`return null` in a void function *) `return null` in a void function *)
astate astate

@ -24,8 +24,8 @@ let tests =
let initial = BoundedCallTree.Domain.empty in let initial = BoundedCallTree.Domain.empty in
let f_proc_name = Typ.Procname.from_string_c_fun "f" in let f_proc_name = Typ.Procname.from_string_c_fun "f" in
let g_proc_name = Typ.Procname.from_string_c_fun "g" in let g_proc_name = Typ.Procname.from_string_c_fun "g" in
let g_args = [((Exp.Const (Const.Cint (IntLit.one))), (Typ.Tint IInt))] in let g_args = [((Exp.Const (Const.Cint (IntLit.one))), (Typ.mk (Tint IInt)))] in
let g_ret_id = Some (ident_of_str "r", Typ.Tint IInt) in let g_ret_id = Some (ident_of_str "r", Typ.mk (Tint IInt)) in
let class_name = "com.example.SomeClass" in let class_name = "com.example.SomeClass" in
let file_name = "SomeClass.java" in let file_name = "SomeClass.java" in
let trace = Stacktrace.make "java.lang.NullPointerException" let trace = Stacktrace.make "java.lang.NullPointerException"

@ -105,9 +105,9 @@ let tests =
call_sink_with_exp (Exp.Var (ident_of_str actual_str)) in call_sink_with_exp (Exp.Var (ident_of_str actual_str)) in
let assign_id_to_field root_str fld_str rhs_id_str = let assign_id_to_field root_str fld_str rhs_id_str =
let rhs_exp = Exp.Var (ident_of_str rhs_id_str) in let rhs_exp = Exp.Var (ident_of_str rhs_id_str) in
make_store ~rhs_typ:Typ.Tvoid (Exp.Var (ident_of_str root_str)) fld_str ~rhs_exp in make_store ~rhs_typ:(Typ.mk Tvoid) (Exp.Var (ident_of_str root_str)) fld_str ~rhs_exp in
let read_field_to_id lhs_id_str root_str fld_str = let read_field_to_id lhs_id_str root_str fld_str =
make_load_fld ~rhs_typ:Typ.Tvoid lhs_id_str fld_str (Exp.Var (ident_of_str root_str)) in make_load_fld ~rhs_typ:(Typ.mk Tvoid) lhs_id_str fld_str (Exp.Var (ident_of_str root_str)) in
let assert_empty = invariant "{ }" in let assert_empty = invariant "{ }" in
(* hack: register an empty analyze_ondemand to prevent a crash because the callback is unset *) (* hack: register an empty analyze_ondemand to prevent a crash because the callback is unset *)
let analyze_ondemand _ summary _ = summary in let analyze_ondemand _ summary _ = summary in
@ -257,7 +257,7 @@ let tests =
"source -> sink via cast", "source -> sink via cast",
[ [
assign_to_source "ret_id"; assign_to_source "ret_id";
cast_id_to_id "cast_id" Typ.Tvoid "ret_id"; cast_id_to_id "cast_id" (Typ.mk Tvoid) "ret_id";
call_sink "cast_id"; call_sink "cast_id";
invariant "{ ret_id$0 => (SOURCE -> SINK) }"; invariant "{ ret_id$0 => (SOURCE -> SINK) }";
]; ];

@ -113,7 +113,7 @@ let tests =
let append = let append =
let append_ _ = let append_ _ =
let call_site = CallSite.dummy in let call_site = CallSite.dummy in
let footprint_ap = AccessPath.Exact (AccessPath.of_id (Ident.create_none ()) Typ.Tvoid) in let footprint_ap = AccessPath.Exact (AccessPath.of_id (Ident.create_none ()) (Typ.mk Tvoid)) in
let dummy_pdesc = let dummy_pdesc =
Cfg.create_proc_desc Cfg.create_proc_desc
(Cfg.create_cfg ()) (Cfg.create_cfg ())

@ -12,7 +12,7 @@ open! IStd
let make_var var_str = let make_var var_str =
Pvar.mk (Mangled.from_string var_str) Typ.Procname.empty_block Pvar.mk (Mangled.from_string var_str) Typ.Procname.empty_block
let make_base ?(typ=Typ.Tvoid) base_str = let make_base ?(typ=Typ.mk Tvoid) base_str =
AccessPath.base_of_pvar (make_var base_str) typ AccessPath.base_of_pvar (make_var base_str) typ
let make_fieldname = Fieldname.Java.from_string let make_fieldname = Fieldname.Java.from_string

@ -21,8 +21,8 @@ let tests =
let xFG = make_access_path "x" ["f"; "g";] in let xFG = make_access_path "x" ["f"; "g";] in
let yF = make_access_path "y" ["f"] in let yF = make_access_path "y" ["f"] in
let xArr = let xArr =
let dummy_typ = Typ.Tvoid in let dummy_typ = Typ.mk Tvoid in
let dummy_arr_typ = Typ.Tarray (dummy_typ, None) in let dummy_arr_typ = Typ.mk (Tarray (dummy_typ, None)) 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] in base, [make_array_access dummy_typ] in
@ -74,7 +74,7 @@ let tests =
let of_exp_test = let of_exp_test =
let f_resolve_id _ = None in let f_resolve_id _ = None in
let dummy_typ = Typ.Tvoid in let dummy_typ = Typ.mk Tvoid in
let check_make_ap exp expected_ap ~f_resolve_id = let check_make_ap exp expected_ap ~f_resolve_id =
let make_ap exp = let make_ap exp =

@ -70,7 +70,7 @@ let tests =
let f = make_field_access "f" in let f = make_field_access "f" in
let g = make_field_access "g" in let g = make_field_access "g" in
let array = make_array_access Typ.Tvoid in let array = make_array_access (Typ.mk Tvoid) in
let x = AccessPath.Exact (make_access_path "x" []) in let x = AccessPath.Exact (make_access_path "x" []) in
let xF = AccessPath.Exact (make_access_path "x" ["f"]) in let xF = AccessPath.Exact (make_access_path "x" ["f"]) in

@ -17,9 +17,9 @@ let tests =
let open OUnit2 in let open OUnit2 in
let open AnalyzerTester.StructuredSil in let open AnalyzerTester.StructuredSil in
let assert_empty = invariant "{ }" in let assert_empty = invariant "{ }" in
let int_typ = Typ.Tint IInt in let int_typ = Typ.mk (Tint IInt) in
let int_ptr_typ = Typ.Tptr (int_typ, Pk_pointer) in let int_ptr_typ = Typ.mk (Tptr (int_typ, Pk_pointer)) in
let fun_ptr_typ = Typ.Tptr (Tfun false, Pk_pointer) in let fun_ptr_typ = Typ.mk (Tptr (Typ.mk (Tfun false), Pk_pointer)) in
let closure_exp captureds = let closure_exp captureds =
let mk_captured_var str = (Exp.Var (ident_of_str str), pvar_of_str str, int_ptr_typ) in let mk_captured_var str = (Exp.Var (ident_of_str str), pvar_of_str str, int_ptr_typ) in
let captured_vars = List.map ~f:mk_captured_var captureds in let captured_vars = List.map ~f:mk_captured_var captureds in

@ -59,7 +59,7 @@ module StructuredSil = struct
let pp_structured_program = pp_structured_instr_list let pp_structured_program = pp_structured_instr_list
let dummy_typ = Typ.Tvoid let dummy_typ = Typ.mk Tvoid
let dummy_loc = Location.dummy let dummy_loc = Location.dummy
let dummy_procname = Typ.Procname.empty_block let dummy_procname = Typ.Procname.empty_block
@ -132,7 +132,7 @@ module StructuredSil = struct
let var_assign_int lhs rhs = let var_assign_int lhs rhs =
let rhs_exp = Exp.int (IntLit.of_int rhs) in let rhs_exp = Exp.int (IntLit.of_int rhs) in
let rhs_typ = Typ.Tint Typ.IInt in let rhs_typ = Typ.mk (Tint Typ.IInt) in
var_assign_exp ~rhs_typ lhs rhs_exp var_assign_exp ~rhs_typ lhs rhs_exp
let var_assign_id ?(rhs_typ=dummy_typ) lhs rhs = let var_assign_id ?(rhs_typ=dummy_typ) lhs rhs =

@ -18,7 +18,7 @@ let tests =
let open OUnit2 in let open OUnit2 in
let open AnalyzerTester.StructuredSil in let open AnalyzerTester.StructuredSil in
let assert_empty = invariant "{ }" in let assert_empty = invariant "{ }" in
let fun_ptr_typ = Typ.Tptr (Tfun false, Pk_pointer) in let fun_ptr_typ = Typ.mk (Tptr (Typ.mk (Tfun false), Pk_pointer)) in
let closure_exp captured_pvars = let closure_exp captured_pvars =
let mk_captured_var str = (Exp.Var (ident_of_str str), pvar_of_str str, dummy_typ) in let mk_captured_var str = (Exp.Var (ident_of_str str), pvar_of_str str, dummy_typ) in
let captured_vars = List.map ~f:mk_captured_var captured_pvars in let captured_vars = List.map ~f:mk_captured_var captured_pvars in
@ -97,7 +97,7 @@ let tests =
"dead_after_call_with_retval", "dead_after_call_with_retval",
[ [
assert_empty; assert_empty;
call_unknown (Some ("y", Typ.Tint IInt)) []; call_unknown (Some ("y", Typ.mk (Tint IInt))) [];
invariant "{ y$0 }"; invariant "{ y$0 }";
id_assign_id "x" "y"; id_assign_id "x" "y";
]; ];

Loading…
Cancel
Save