From eefe05b24073adcb0a8ea1bd0244cdd547fa5792 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 13 Jul 2016 15:57:22 -0700 Subject: [PATCH] Refactor Sil.Subtype into separate Subtype module Summary: Move Sil.Subtype module into separate Subtype module. Reviewed By: dulmarod Differential Revision: D3548084 fbshipit-source-id: 52fcade --- infer/src/IR/Sil.re | 288 ------------------------ infer/src/IR/Sil.rei | 31 --- infer/src/IR/Subtype.re | 341 +++++++++++++++++++++++++++++ infer/src/IR/Subtype.rei | 62 ++++++ infer/src/backend/abs.ml | 2 +- infer/src/backend/dom.ml | 2 +- infer/src/backend/interproc.ml | 4 +- infer/src/backend/modelBuiltins.ml | 10 +- infer/src/backend/prover.ml | 22 +- infer/src/backend/rearrange.ml | 8 +- infer/src/backend/symExec.ml | 6 +- infer/src/backend/tabulation.ml | 4 +- infer/src/clang/cTrans.ml | 8 +- infer/src/clang/cTrans_utils.ml | 4 +- infer/src/harness/inhabit.ml | 2 +- infer/src/java/jTrans.ml | 16 +- infer/src/java/jTransExn.ml | 2 +- infer/src/java/jTransType.mli | 2 +- 18 files changed, 449 insertions(+), 365 deletions(-) create mode 100644 infer/src/IR/Subtype.re create mode 100644 infer/src/IR/Subtype.rei diff --git a/infer/src/IR/Sil.re b/infer/src/IR/Sil.re index 007e1a805..2e3934f51 100644 --- a/infer/src/IR/Sil.re +++ b/infer/src/IR/Sil.re @@ -66,294 +66,6 @@ type dangling_kind = type path_pos = (Procname.t, int); -/** module for subtypes, to be used with Sizeof info */ -let module Subtype = { - let list_to_string list => { - let rec aux list => - switch list { - | [] => "" - | [el, ...rest] => - let s = aux rest; - if (s == "") { - Typename.name el - } else { - Typename.name el ^ ", " ^ s - } - }; - if (IList.length list == 0) { - "( sub )" - } else { - "- {" ^ aux list ^ "}" - } - }; - type t' = - | Exact /** denotes the current type only */ - | Subtypes of (list Typename.t); - - /** denotes the current type and a list of types that are not their subtypes */ - type kind = | CAST | INSTOF | NORMAL; - type t = (t', kind); - let module SubtypesPair = { - type t = (Typename.t, Typename.t); - let compare (e1: t) (e2: t) :int => pair_compare Typename.compare Typename.compare e1 e2; - }; - let module SubtypesMap = Map.Make SubtypesPair; - type subtMap = SubtypesMap.t bool; - let subtMap: ref subtMap = ref SubtypesMap.empty; - let check_subtype f c1 c2 => - try (SubtypesMap.find (c1, c2) !subtMap) { - | Not_found => - let is_subt = f c1 c2; - subtMap := SubtypesMap.add (c1, c2) is_subt !subtMap; - is_subt - }; - let flag_to_string flag => - switch flag { - | CAST => "(cast)" - | INSTOF => "(instof)" - | NORMAL => "" - }; - let pp f (t, flag) => - if Config.print_types { - switch t { - | Exact => F.fprintf f "%s" (flag_to_string flag) - | Subtypes list => F.fprintf f "%s" (list_to_string list ^ flag_to_string flag) - } - }; - let exact = (Exact, NORMAL); - let all_subtypes = Subtypes []; - let subtypes = (all_subtypes, NORMAL); - let subtypes_cast = (all_subtypes, CAST); - let subtypes_instof = (all_subtypes, INSTOF); - let is_cast t => snd t == CAST; - let is_instof t => snd t == INSTOF; - let list_intersect equal l1 l2 => { - let in_l2 a => IList.mem equal a l2; - IList.filter in_l2 l1 - }; - let join_flag flag1 flag2 => - switch (flag1, flag2) { - | (CAST, _) => CAST - | (_, CAST) => CAST - | (_, _) => NORMAL - }; - let join (s1, flag1) (s2, flag2) => { - let s = - switch (s1, s2) { - | (Exact, _) => s2 - | (_, Exact) => s1 - | (Subtypes l1, Subtypes l2) => Subtypes (list_intersect Typename.equal l1 l2) - }; - let flag = join_flag flag1 flag2; - (s, flag) - }; - let subtypes_compare l1 l2 => IList.compare Typename.compare l1 l2; - let compare_flag flag1 flag2 => - switch (flag1, flag2) { - | (CAST, CAST) => 0 - | (INSTOF, INSTOF) => 0 - | (NORMAL, NORMAL) => 0 - | (CAST, _) => (-1) - | (_, CAST) => 1 - | (INSTOF, NORMAL) => (-1) - | (NORMAL, INSTOF) => 1 - }; - let compare_subt s1 s2 => - switch (s1, s2) { - | (Exact, Exact) => 0 - | (Exact, _) => (-1) - | (_, Exact) => 1 - | (Subtypes l1, Subtypes l2) => subtypes_compare l1 l2 - }; - let compare t1 t2 => pair_compare compare_subt compare_flag t1 t2; - let equal_modulo_flag (st1, _) (st2, _) => compare_subt st1 st2 == 0; - let update_flag c1 c2 flag flag' => - switch flag { - | INSTOF => - if (Typename.equal c1 c2) { - flag - } else { - flag' - } - | _ => flag' - }; - let change_flag st_opt c1 c2 flag' => - switch st_opt { - | Some st => - switch st { - | (Exact, flag) => - let new_flag = update_flag c1 c2 flag flag'; - Some (Exact, new_flag) - | (Subtypes t, flag) => - let new_flag = update_flag c1 c2 flag flag'; - Some (Subtypes t, new_flag) - } - | None => None - }; - let normalize_subtypes t_opt c1 c2 flag1 flag2 => { - let new_flag = update_flag c1 c2 flag1 flag2; - switch t_opt { - | Some t => - switch t { - | Exact => Some (t, new_flag) - | Subtypes l => Some (Subtypes (IList.sort Typename.compare l), new_flag) - } - | None => None - } - }; - let subtypes_to_string t => - switch (fst t) { - | Exact => "ex" ^ flag_to_string (snd t) - | Subtypes l => list_to_string l ^ flag_to_string (snd t) - }; - /* c is a subtype when it does not appear in the list l of no-subtypes */ - let is_subtype f c l => - try { - ignore (IList.find (f c) l); - false - } { - | Not_found => true - }; - let is_strict_subtype f c1 c2 => f c1 c2 && not (Typename.equal c1 c2); - /* checks for redundancies when adding c to l - Xi in A - { X1,..., Xn } is redundant in two cases: - 1) not (Xi <: A) because removing the subtypes of Xi has no effect unless Xi is a subtype of A - 2) Xi <: Xj because the subtypes of Xi are a subset of the subtypes of Xj */ - let check_redundancies f c l => { - let aux (l, add) ci => { - let (l, should_add) = - if (f ci c) { - (l, true) - } else if (f c ci) { - ([ci, ...l], false) - } else { - ([ci, ...l], true) - }; - (l, add && should_add) - }; - IList.fold_left aux ([], true) l - }; - let rec updates_head f c l => - switch l { - | [] => [] - | [ci, ...rest] => - if (is_strict_subtype f ci c) { - [ci, ...updates_head f c rest] - } else { - updates_head f c rest - } - }; - /* adds the classes of l2 to l1 and checks that no redundancies or inconsistencies will occur - A - { X1,..., Xn } is inconsistent if A <: Xi for some i */ - let rec add_not_subtype f c1 l1 l2 => - switch l2 { - | [] => l1 - | [c, ...rest] => - if (f c1 c) { - add_not_subtype f c1 l1 rest - } else { - /* checks for inconsistencies */ - let (l1', should_add) = check_redundancies f c l1; /* checks for redundancies */ - let rest' = add_not_subtype f c1 l1' rest; - if should_add { - [c, ...rest'] - } else { - rest' - } - } - }; - let get_subtypes (c1, (st1, flag1)) (c2, (st2, flag2)) f is_interface => { - let is_sub = f c1 c2; - let (pos_st, neg_st) = - switch (st1, st2) { - | (Exact, Exact) => - if is_sub { - (Some st1, None) - } else { - (None, Some st1) - } - | (Exact, Subtypes l2) => - if (is_sub && is_subtype f c1 l2) { - (Some st1, None) - } else { - (None, Some st1) - } - | (Subtypes l1, Exact) => - if is_sub { - (Some st1, None) - } else { - let l1' = updates_head f c2 l1; - if (is_subtype f c2 l1) { - (Some (Subtypes l1'), Some (Subtypes (add_not_subtype f c1 l1 [c2]))) - } else { - (None, Some st1) - } - } - | (Subtypes l1, Subtypes l2) => - if (is_interface c2 || is_sub) { - if (is_subtype f c1 l2) { - let l2' = updates_head f c1 l2; - (Some (Subtypes (add_not_subtype f c1 l1 l2')), None) - } else { - (None, Some st1) - } - } else if ( - (is_interface c1 || f c2 c1) && is_subtype f c2 l1 - ) { - let l1' = updates_head f c2 l1; - ( - Some (Subtypes (add_not_subtype f c2 l1' l2)), - Some (Subtypes (add_not_subtype f c1 l1 [c2])) - ) - } else { - (None, Some st1) - } - }; - (normalize_subtypes pos_st c1 c2 flag1 flag2, normalize_subtypes neg_st c1 c2 flag1 flag2) - }; - let case_analysis_basic (c1, st) (c2, (_, flag2)) f => { - let (pos_st, neg_st) = - if (f c1 c2) { - (Some st, None) - } else if (f c2 c1) { - switch st { - | (Exact, _) => - if (Typename.equal c1 c2) { - (Some st, None) - } else { - (None, Some st) - } - | (Subtypes _, _) => - if (Typename.equal c1 c2) { - (Some st, None) - } else { - (Some st, Some st) - } - } - } else { - (None, Some st) - }; - (change_flag pos_st c1 c2 flag2, change_flag neg_st c1 c2 flag2) - }; - - /** [case_analysis (c1, st1) (c2,st2) f] performs case analysis on [c1 <: c2] - according to [st1] and [st2] - where f c1 c2 is true if c1 is a subtype of c2. - get_subtypes returning a pair: - - whether [st1] and [st2] admit [c1 <: c2], and in case return the updated subtype [st1] - - whether [st1] and [st2] admit [not(c1 <: c2)], - and in case return the updated subtype [st1] */ - let case_analysis (c1, st1) (c2, st2) f is_interface => { - let f = check_subtype f; - if Config.subtype_multirange { - get_subtypes (c1, st1) (c2, st2) f is_interface - } else { - case_analysis_basic (c1, st1) (c2, st2) f - } - }; -}; - - /** Flags for a procedure call */ type call_flags = { cf_virtual: bool, diff --git a/infer/src/IR/Sil.rei b/infer/src/IR/Sil.rei index debc5d9e0..705649cad 100644 --- a/infer/src/IR/Sil.rei +++ b/infer/src/IR/Sil.rei @@ -54,37 +54,6 @@ type dangling_kind = type path_pos = (Procname.t, int); -/** module for subtypes, to be used with Sizeof info */ -let module Subtype: { - type t; - let exact: t; /** denotes the current type only */ - let subtypes: t; /** denotes the current type and any subtypes */ - let subtypes_cast: t; - let subtypes_instof: t; - let join: t => t => t; - - /** [case_analysis (c1, st1) (c2,st2) f] performs case analysis on [c1 <: c2] according - to [st1] and [st2] where f c1 c2 is true if c1 is a subtype of c2. - get_subtypes returning a pair: - - whether [st1] and [st2] admit [c1 <: c2], and in case return the updated subtype [st1] - - whether [st1] and [st2] admit [not(c1 <: c2)], and in case return - the updated subtype [st1] */ - let case_analysis: - (Typename.t, t) => - (Typename.t, t) => - (Typename.t => Typename.t => bool) => - (Typename.t => bool) => - (option t, option t); - let check_subtype: (Typename.t => Typename.t => bool) => Typename.t => Typename.t => bool; - let subtypes_to_string: t => string; - let is_cast: t => bool; - let is_instof: t => bool; - - /** equality ignoring flags in the subtype */ - let equal_modulo_flag: t => t => bool; -}; - - /** Flags for a procedure call */ type call_flags = { cf_virtual: bool, diff --git a/infer/src/IR/Subtype.re b/infer/src/IR/Subtype.re new file mode 100644 index 000000000..66f4837b5 --- /dev/null +++ b/infer/src/IR/Subtype.re @@ -0,0 +1,341 @@ +/* + * vim: set ft=rust: + * vim: set ft=reason: + * + * Copyright (c) 2009 - 2013 Monoidics ltd. + * Copyright (c) 2013 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +open! Utils; + + +/** The Smallfoot Intermediate Language: Subtypes */ +let module L = Logging; + +let module F = Format; + +let list_to_string list => { + let rec aux list => + switch list { + | [] => "" + | [el, ...rest] => + let s = aux rest; + if (s == "") { + Typename.name el + } else { + Typename.name el ^ ", " ^ s + } + }; + if (IList.length list == 0) { + "( sub )" + } else { + "- {" ^ aux list ^ "}" + } +}; + +type t' = + | Exact /** denotes the current type only */ + | Subtypes of (list Typename.t); + + +/** denotes the current type and a list of types that are not their subtypes */ +type kind = | CAST | INSTOF | NORMAL; + +type t = (t', kind); + +let module SubtypesPair = { + type t = (Typename.t, Typename.t); + let compare (e1: t) (e2: t) :int => pair_compare Typename.compare Typename.compare e1 e2; +}; + +let module SubtypesMap = Map.Make SubtypesPair; + +type subtMap = SubtypesMap.t bool; + +let subtMap: ref subtMap = ref SubtypesMap.empty; + +let check_subtype f c1 c2 => + try (SubtypesMap.find (c1, c2) !subtMap) { + | Not_found => + let is_subt = f c1 c2; + subtMap := SubtypesMap.add (c1, c2) is_subt !subtMap; + is_subt + }; + +let flag_to_string flag => + switch flag { + | CAST => "(cast)" + | INSTOF => "(instof)" + | NORMAL => "" + }; + +let pp f (t, flag) => + if Config.print_types { + switch t { + | Exact => F.fprintf f "%s" (flag_to_string flag) + | Subtypes list => F.fprintf f "%s" (list_to_string list ^ flag_to_string flag) + } + }; + +let exact = (Exact, NORMAL); + +let all_subtypes = Subtypes []; + +let subtypes = (all_subtypes, NORMAL); + +let subtypes_cast = (all_subtypes, CAST); + +let subtypes_instof = (all_subtypes, INSTOF); + +let is_cast t => snd t == CAST; + +let is_instof t => snd t == INSTOF; + +let list_intersect equal l1 l2 => { + let in_l2 a => IList.mem equal a l2; + IList.filter in_l2 l1 +}; + +let join_flag flag1 flag2 => + switch (flag1, flag2) { + | (CAST, _) => CAST + | (_, CAST) => CAST + | (_, _) => NORMAL + }; + +let join (s1, flag1) (s2, flag2) => { + let s = + switch (s1, s2) { + | (Exact, _) => s2 + | (_, Exact) => s1 + | (Subtypes l1, Subtypes l2) => Subtypes (list_intersect Typename.equal l1 l2) + }; + let flag = join_flag flag1 flag2; + (s, flag) +}; + +let subtypes_compare l1 l2 => IList.compare Typename.compare l1 l2; + +let compare_flag flag1 flag2 => + switch (flag1, flag2) { + | (CAST, CAST) => 0 + | (INSTOF, INSTOF) => 0 + | (NORMAL, NORMAL) => 0 + | (CAST, _) => (-1) + | (_, CAST) => 1 + | (INSTOF, NORMAL) => (-1) + | (NORMAL, INSTOF) => 1 + }; + +let compare_subt s1 s2 => + switch (s1, s2) { + | (Exact, Exact) => 0 + | (Exact, _) => (-1) + | (_, Exact) => 1 + | (Subtypes l1, Subtypes l2) => subtypes_compare l1 l2 + }; + +let compare t1 t2 => pair_compare compare_subt compare_flag t1 t2; + +let equal_modulo_flag (st1, _) (st2, _) => compare_subt st1 st2 == 0; + +let update_flag c1 c2 flag flag' => + switch flag { + | INSTOF => + if (Typename.equal c1 c2) { + flag + } else { + flag' + } + | _ => flag' + }; + +let change_flag st_opt c1 c2 flag' => + switch st_opt { + | Some st => + switch st { + | (Exact, flag) => + let new_flag = update_flag c1 c2 flag flag'; + Some (Exact, new_flag) + | (Subtypes t, flag) => + let new_flag = update_flag c1 c2 flag flag'; + Some (Subtypes t, new_flag) + } + | None => None + }; + +let normalize_subtypes t_opt c1 c2 flag1 flag2 => { + let new_flag = update_flag c1 c2 flag1 flag2; + switch t_opt { + | Some t => + switch t { + | Exact => Some (t, new_flag) + | Subtypes l => Some (Subtypes (IList.sort Typename.compare l), new_flag) + } + | None => None + } +}; + +let subtypes_to_string t => + switch (fst t) { + | Exact => "ex" ^ flag_to_string (snd t) + | Subtypes l => list_to_string l ^ flag_to_string (snd t) + }; + +/* c is a subtype when it does not appear in the list l of no-subtypes */ +let is_subtype f c l => + try { + ignore (IList.find (f c) l); + false + } { + | Not_found => true + }; + +let is_strict_subtype f c1 c2 => f c1 c2 && not (Typename.equal c1 c2); + +/* checks for redundancies when adding c to l + Xi in A - { X1,..., Xn } is redundant in two cases: + 1) not (Xi <: A) because removing the subtypes of Xi has no effect unless Xi is a subtype of A + 2) Xi <: Xj because the subtypes of Xi are a subset of the subtypes of Xj */ +let check_redundancies f c l => { + let aux (l, add) ci => { + let (l, should_add) = + if (f ci c) { + (l, true) + } else if (f c ci) { + ([ci, ...l], false) + } else { + ([ci, ...l], true) + }; + (l, add && should_add) + }; + IList.fold_left aux ([], true) l +}; + +let rec updates_head f c l => + switch l { + | [] => [] + | [ci, ...rest] => + if (is_strict_subtype f ci c) { + [ci, ...updates_head f c rest] + } else { + updates_head f c rest + } + }; + +/* adds the classes of l2 to l1 and checks that no redundancies or inconsistencies will occur + A - { X1,..., Xn } is inconsistent if A <: Xi for some i */ +let rec add_not_subtype f c1 l1 l2 => + switch l2 { + | [] => l1 + | [c, ...rest] => + if (f c1 c) { + add_not_subtype f c1 l1 rest + } else { + /* checks for inconsistencies */ + let (l1', should_add) = check_redundancies f c l1; /* checks for redundancies */ + let rest' = add_not_subtype f c1 l1' rest; + if should_add { + [c, ...rest'] + } else { + rest' + } + } + }; + +let get_subtypes (c1, (st1, flag1)) (c2, (st2, flag2)) f is_interface => { + let is_sub = f c1 c2; + let (pos_st, neg_st) = + switch (st1, st2) { + | (Exact, Exact) => + if is_sub { + (Some st1, None) + } else { + (None, Some st1) + } + | (Exact, Subtypes l2) => + if (is_sub && is_subtype f c1 l2) { + (Some st1, None) + } else { + (None, Some st1) + } + | (Subtypes l1, Exact) => + if is_sub { + (Some st1, None) + } else { + let l1' = updates_head f c2 l1; + if (is_subtype f c2 l1) { + (Some (Subtypes l1'), Some (Subtypes (add_not_subtype f c1 l1 [c2]))) + } else { + (None, Some st1) + } + } + | (Subtypes l1, Subtypes l2) => + if (is_interface c2 || is_sub) { + if (is_subtype f c1 l2) { + let l2' = updates_head f c1 l2; + (Some (Subtypes (add_not_subtype f c1 l1 l2')), None) + } else { + (None, Some st1) + } + } else if ( + (is_interface c1 || f c2 c1) && is_subtype f c2 l1 + ) { + let l1' = updates_head f c2 l1; + ( + Some (Subtypes (add_not_subtype f c2 l1' l2)), + Some (Subtypes (add_not_subtype f c1 l1 [c2])) + ) + } else { + (None, Some st1) + } + }; + (normalize_subtypes pos_st c1 c2 flag1 flag2, normalize_subtypes neg_st c1 c2 flag1 flag2) +}; + +let case_analysis_basic (c1, st) (c2, (_, flag2)) f => { + let (pos_st, neg_st) = + if (f c1 c2) { + (Some st, None) + } else if (f c2 c1) { + switch st { + | (Exact, _) => + if (Typename.equal c1 c2) { + (Some st, None) + } else { + (None, Some st) + } + | (Subtypes _, _) => + if (Typename.equal c1 c2) { + (Some st, None) + } else { + (Some st, Some st) + } + } + } else { + (None, Some st) + }; + (change_flag pos_st c1 c2 flag2, change_flag neg_st c1 c2 flag2) +}; + + +/** [case_analysis (c1, st1) (c2,st2) f] performs case analysis on [c1 <: c2] + according to [st1] and [st2] + where f c1 c2 is true if c1 is a subtype of c2. + get_subtypes returning a pair: + - whether [st1] and [st2] admit [c1 <: c2], and in case return the updated subtype [st1] + - whether [st1] and [st2] admit [not(c1 <: c2)], + and in case return the updated subtype [st1] */ +let case_analysis (c1, st1) (c2, st2) f is_interface => { + let f = check_subtype f; + if Config.subtype_multirange { + get_subtypes (c1, st1) (c2, st2) f is_interface + } else { + case_analysis_basic (c1, st1) (c2, st2) f + } +}; diff --git a/infer/src/IR/Subtype.rei b/infer/src/IR/Subtype.rei new file mode 100644 index 000000000..b3a6e2a9f --- /dev/null +++ b/infer/src/IR/Subtype.rei @@ -0,0 +1,62 @@ +/* + * vim: set ft=rust: + * vim: set ft=reason: + * + * Copyright (c) 2009 - 2013 Monoidics ltd. + * Copyright (c) 2013 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +open! Utils; + + +/** The Smallfoot Intermediate Language: Subtypes */ +let module L = Logging; + +let module F = Format; + +type t; + +let compare: t => t => int; + +let pp: F.formatter => t => unit; + +let exact: t; /** denotes the current type only */ + +let subtypes: t; /** denotes the current type and any subtypes */ + +let subtypes_cast: t; + +let subtypes_instof: t; + +let join: t => t => t; + + +/** [case_analysis (c1, st1) (c2,st2) f] performs case analysis on [c1 <: c2] according + to [st1] and [st2] where f c1 c2 is true if c1 is a subtype of c2. + get_subtypes returning a pair: + - whether [st1] and [st2] admit [c1 <: c2], and in case return the updated subtype [st1] + - whether [st1] and [st2] admit [not(c1 <: c2)], and in case return + the updated subtype [st1] */ +let case_analysis: + (Typename.t, t) => + (Typename.t, t) => + (Typename.t => Typename.t => bool) => + (Typename.t => bool) => + (option t, option t); + +let check_subtype: (Typename.t => Typename.t => bool) => Typename.t => Typename.t => bool; + +let subtypes_to_string: t => string; + +let is_cast: t => bool; + +let is_instof: t => bool; + + +/** equality ignoring flags in the subtype */ +let equal_modulo_flag: t => t => bool; diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index 3464593ea..0e869ca4c 100644 --- a/infer/src/backend/abs.ml +++ b/infer/src/backend/abs.ml @@ -968,7 +968,7 @@ let get_var_retain_cycle _prop = | Some pvar -> [((sexp pvar, t), f, e')] | _ -> (match find_block e with | Some blk -> [((sexp blk, t), f, e')] - | _ -> [((sexp (Sil.Sizeof (t, None, Sil.Subtype.exact)), t), f, e')]) in + | _ -> [((sexp (Sil.Sizeof (t, None, Subtype.exact)), t), f, e')]) in (* returns the pvars of the first cycle we find in sigma. *) (* This is an heuristic that works if there is one cycle. *) (* In case there are more than one cycle we may return not necessarily*) diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml index cbeb773c0..4b840a3c2 100644 --- a/infer/src/backend/dom.ml +++ b/infer/src/backend/dom.ml @@ -963,7 +963,7 @@ let rec exp_partial_join (e1: Sil.exp) (e2: Sil.exp) : Sil.exp = Sil.Lindex(e1'', e2'') | Sil.Sizeof (t1, len1, st1), Sil.Sizeof (t2, len2, st2) -> Sil.Sizeof - (typ_partial_join t1 t2, dynamic_length_partial_join len1 len2, Sil.Subtype.join st1 st2) + (typ_partial_join t1 t2, dynamic_length_partial_join len1 len2, Subtype.join st1 st2) | _ -> L.d_str "exp_partial_join no match "; Sil.d_exp e1; L.d_str " "; Sil.d_exp e2; L.d_ln (); raise IList.Fail diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 73ae9a3d2..d12f8a62d 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -807,8 +807,8 @@ let prop_init_formals_seed tenv new_formals (prop : 'a Prop.t) : Prop.exposed Pr let sigma_new_formals = let do_formal (pv, typ) = let texp = match !Config.curr_language with - | Config.Clang -> Sil.Sizeof (typ, None, Sil.Subtype.exact) - | Config.Java -> Sil.Sizeof (typ, None, Sil.Subtype.subtypes) in + | Config.Clang -> Sil.Sizeof (typ, None, Subtype.exact) + | Config.Java -> Sil.Sizeof (typ, None, Subtype.subtypes) in Prop.mk_ptsto_lvar (Some tenv) Prop.Fld_init Sil.inst_formal (pv, texp, None) in IList.map do_formal new_formals in let sigma_seed = diff --git a/infer/src/backend/modelBuiltins.ml b/infer/src/backend/modelBuiltins.ml index a2770053d..26983930d 100644 --- a/infer/src/backend/modelBuiltins.ml +++ b/infer/src/backend/modelBuiltins.ml @@ -74,7 +74,7 @@ let add_array_to_prop pdesc prop_ lexp typ = | Some arr_typ -> let len = Sil.Var (Ident.create_fresh Ident.kfootprint) in let s = mk_empty_array_rearranged len in - let hpred = Prop.mk_ptsto n_lexp s (Sil.Sizeof (arr_typ, Some len, Sil.Subtype.exact)) in + let hpred = Prop.mk_ptsto n_lexp s (Sil.Sizeof (arr_typ, Some len, Subtype.exact)) in let sigma = Prop.get_sigma prop in let sigma_fp = Prop.get_sigma_footprint prop in let prop'= Prop.replace_sigma (hpred:: sigma) prop in @@ -155,13 +155,13 @@ let create_type tenv n_lexp typ prop = | Typ.Tptr (typ', _) -> let sexp = Sil.Estruct ([], Sil.inst_none) in let typ'' = Tenv.expand_type tenv typ' in - let texp = Sil.Sizeof (typ'', None, Sil.Subtype.subtypes) in + let texp = Sil.Sizeof (typ'', None, Subtype.subtypes) in let hpred = Prop.mk_ptsto n_lexp sexp texp in Some hpred | Typ.Tarray _ -> let len = Sil.Var (Ident.create_fresh Ident.kfootprint) in let sexp = mk_empty_array len in - let texp = Sil.Sizeof (typ, None, Sil.Subtype.subtypes) in + let texp = Sil.Sizeof (typ, None, Subtype.subtypes) in let hpred = Prop.mk_ptsto n_lexp sexp texp in Some hpred | _ -> None in @@ -788,7 +788,7 @@ let execute_alloc mk can_return_null let n_size_exp' = evaluate_char_sizeof n_size_exp in Prop.exp_normalize_prop prop n_size_exp', prop in let cnt_te = - Sil.Sizeof (Typ.Tarray (Typ.Tint Typ.IChar, None), Some size_exp', Sil.Subtype.exact) in + Sil.Sizeof (Typ.Tarray (Typ.Tint Typ.IChar, None), Some size_exp', Subtype.exact) in let id_new = Ident.create_fresh Ident.kprimed in let exp_new = Sil.Var id_new in let ptsto_new = @@ -1159,7 +1159,7 @@ let execute_objc_alloc_no_fail { Builtin.pdesc; tenv; ret_ids; loc; } = let alloc_fun = Sil.Const (Const.Cfun __objc_alloc_no_fail) in let ptr_typ = Typ.Tptr (typ, Typ.Pk_pointer) in - let sizeof_typ = Sil.Sizeof (typ, None, Sil.Subtype.exact) in + let sizeof_typ = Sil.Sizeof (typ, None, Subtype.exact) in let alloc_fun_exp = match alloc_fun_opt with | Some pname -> [Sil.Const (Const.Cfun pname), Typ.Tvoid] diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index 663f7c2e1..6e9e70f18 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -1436,7 +1436,7 @@ let expand_hpred_pointer calc_index_frame hpred : bool * bool * Sil.hpred = | Sil.Hpointsto (Sil.Lfield (e, fld, typ_fld), se, t) -> let t' = match t, typ_fld with | _, Typ.Tstruct _ -> (* the struct type of fld is known *) - Sil.Sizeof (typ_fld, None, Sil.Subtype.exact) + Sil.Sizeof (typ_fld, None, Subtype.exact) | Sil.Sizeof (t1, len, st), _ -> (* the struct type of fld is not known -- typically Tvoid *) Sil.Sizeof @@ -1507,7 +1507,7 @@ struct let check_subclass tenv c1 c2 = let f = check_subclass_tenv tenv in - Sil.Subtype.check_subtype f c1 c2 + Subtype.check_subtype f c1 c2 (** check that t1 and t2 are the same primitive type *) let check_subtype_basic_type t1 t2 = @@ -1563,7 +1563,7 @@ struct Typ.Tstruct { Typ.csu = Csu.Class Csu.Java; struct_name = Some c2 } -> let cn1 = Typename.TN_csu (Csu.Class Csu.Java, c1) and cn2 = Typename.TN_csu (Csu.Class Csu.Java, c2) in - Sil.Subtype.case_analysis (cn1, st1) (cn2, st2) + Subtype.case_analysis (cn1, st1) (cn2, st2) (check_subclass tenv) (is_interface tenv) | Typ.Tarray (dom_type1, _), Typ.Tarray (dom_type2, _) -> @@ -1577,7 +1577,7 @@ struct if (Typename.equal cn1 serializable_type || Typename.equal cn1 cloneable_type || Typename.equal cn1 object_type) && - st1 <> Sil.Subtype.exact then Some st1, None + st1 <> Subtype.exact then Some st1, None else (None, Some st1) | _ -> if check_subtype_basic_type t1 t2 then Some st1, None @@ -1593,7 +1593,7 @@ struct (* and not in ObjC because of being weakly typed, *) (* and the algorithm will only work correctly if this is the case *) if check_subclass tenv cn1 cn2 || check_subclass tenv cn2 cn1 then - Sil.Subtype.case_analysis (cn1, st1) (cn2, st2) (check_subclass tenv) + Subtype.case_analysis (cn1, st1) (cn2, st2) (check_subclass tenv) (is_interface tenv) else None, Some st1 | _ -> None, Some st1 @@ -1623,7 +1623,7 @@ let cast_exception tenv texp1 texp2 e1 subs = let _ = match texp1, texp2 with | Sil.Sizeof (t1, _, _), Sil.Sizeof (t2, _, st2) -> if Config.developer_mode || - (Sil.Subtype.is_cast st2 && + (Subtype.is_cast st2 && not (Subtyping_check.check_subtype tenv t1 t2)) then ProverState.checks := Class_cast_check (texp1, texp2, e1) :: !ProverState.checks | _ -> () in @@ -1654,7 +1654,7 @@ let texp_equal_modulo_subtype_flag texp1 texp2 = match texp1, texp2 with | Sil.Sizeof (t1, len1, st1), Sil.Sizeof (t2, len2, st2) -> Typ.equal t1 t2 && (opt_equal Sil.exp_equal len1 len2) - && Sil.Subtype.equal_modulo_flag st1 st2 + && Subtype.equal_modulo_flag st1 st2 | _ -> Sil.exp_equal texp1 texp2 (** check implication between type expressions *) @@ -1740,7 +1740,7 @@ let handle_parameter_subtype tenv prop1 sigma2 subs (e1, se1, texp1) (se2, texp2 then begin let pos_type_opt, _ = Subtyping_check.subtype_case_analysis tenv - (Sil.Sizeof (t1, None, Sil.Subtype.subtypes)) + (Sil.Sizeof (t1, None, Subtype.subtypes)) (Sil.Sizeof (t2_ptsto, len2, sub2)) in match pos_type_opt with | Some t1_noptr -> @@ -1972,14 +1972,14 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 * let const_string_texp = match !Config.curr_language with | Config.Clang -> - Sil.Sizeof (Typ.Tarray (Typ.Tint Typ.IChar, Some len), None, Sil.Subtype.exact) + Sil.Sizeof (Typ.Tarray (Typ.Tint Typ.IChar, Some len), None, Subtype.exact) | Config.Java -> let object_type = Typename.TN_csu (Csu.Class Csu.Java, Mangled.from_string "java.lang.String") in let typ = match Tenv.lookup tenv object_type with | Some typ -> typ | None -> assert false in - Sil.Sizeof (Typ.Tstruct typ, None, Sil.Subtype.exact) in + Sil.Sizeof (Typ.Tstruct typ, None, Subtype.exact) in Sil.Hpointsto (root, sexp, const_string_texp) in let mk_constant_class_hpred s = (* creat an hpred from a constant class *) let root = Sil.Const (Const.Cclass (Ident.string_to_name s)) in @@ -1993,7 +1993,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 * let typ = match Tenv.lookup tenv class_type with | Some typ -> typ | None -> assert false in - Sil.Sizeof (Typ.Tstruct typ, None, Sil.Subtype.exact) in + Sil.Sizeof (Typ.Tstruct typ, None, Subtype.exact) in Sil.Hpointsto (root, sexp, class_texp) in try (match move_primed_lhs_from_front subs sigma2 with diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index 777312295..7d7d6eb10 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -255,7 +255,7 @@ let rec _strexp_extend_values let len = match se with | Sil.Eexp (_, Sil.Ialloc) -> Sil.exp_one (* if allocated explicitly, we know len is 1 *) | _ -> - if Config.type_size then Sil.exp_one (* Sil.Sizeof (typ, Sil.Subtype.exact) *) + if Config.type_size then Sil.exp_one (* Sil.Sizeof (typ, Subtype.exact) *) else Sil.Var (new_id ()) in let se_new = Sil.Earray (len, [(Sil.exp_zero, se)], inst) in let typ_new = Typ.Tarray (typ, None) in @@ -405,7 +405,7 @@ let strexp_extend_values if Config.trace_rearrange then L.d_strln "exiting strexp_extend_values"; let len, st = match te with | Sil.Sizeof(_, len, st) -> (len, st) - | _ -> None, Sil.Subtype.exact in + | _ -> None, Subtype.exact in IList.map (fun (atoms', se', typ') -> (laundry_atoms @ atoms', se', Sil.Sizeof (typ', len, st))) atoms_se_typ_list_filtered @@ -436,8 +436,8 @@ let mk_ptsto_exp_footprint end; let off_foot, eqs = laundry_offset_for_footprint max_stamp off in let st = match !Config.curr_language with - | Config.Clang -> Sil.Subtype.exact - | Config.Java -> Sil.Subtype.subtypes in + | Config.Clang -> Subtype.exact + | Config.Java -> Subtype.subtypes in let create_ptsto footprint_part off0 = match root, off0, typ with | Sil.Lvar pvar, [], Typ.Tfun _ -> let fun_name = Procname.from_string_c_fun (Mangled.to_string (Pvar.get_name pvar)) in diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index b06be748e..e4b24f2d4 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -796,7 +796,7 @@ let do_error_checks node_opt instr pname pdesc = match node_opt with let add_strexp_to_footprint strexp abducted_pv typ prop = let abducted_lvar = Sil.Lvar abducted_pv in let lvar_pt_fpvar = - let sizeof_exp = Sil.Sizeof (typ, None, Sil.Subtype.subtypes) in + let sizeof_exp = Sil.Sizeof (typ, None, Subtype.subtypes) in Prop.mk_ptsto abducted_lvar strexp sizeof_exp in let sigma_fp = Prop.get_sigma_footprint prop in Prop.normalize (Prop.replace_sigma_footprint (lvar_pt_fpvar :: sigma_fp) prop) @@ -1271,7 +1271,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path ret_old_path [Prop.exist_quantify (Sil.fav_from_list temps) prop_] | Sil.Declare_locals (ptl, _) -> let sigma_locals = - let add_None (x, y) = (x, Sil.Sizeof (y, None, Sil.Subtype.exact), None) in + let add_None (x, y) = (x, Sil.Sizeof (y, None, Subtype.exact), None) in let sigma_locals () = IList.map (Prop.mk_ptsto_lvar (Some tenv) Prop.Fld_init Sil.inst_initial) @@ -1382,7 +1382,7 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call let havoc_actual_by_ref (actual, actual_typ) prop = let actual_pt_havocd_var = let havocd_var = Sil.Var (Ident.create_fresh Ident.kprimed) in - let sizeof_exp = Sil.Sizeof (Typ.strip_ptr actual_typ, None, Sil.Subtype.subtypes) in + let sizeof_exp = Sil.Sizeof (Typ.strip_ptr actual_typ, None, Subtype.subtypes) in Prop.mk_ptsto actual (Sil.Eexp (havocd_var, Sil.Inone)) sizeof_exp in replace_actual_hpred actual actual_pt_havocd_var prop in IList.fold_left (fun p var -> havoc_actual_by_ref var p) prop actuals_by_ref diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 4385d0da1..da060f2db 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -474,7 +474,7 @@ let texp_star texp1 texp2 = | _ -> t1 in match texp1, texp2 with | Sil.Sizeof (t1, len1, st1), Sil.Sizeof (t2, _, st2) -> - Sil.Sizeof (typ_star t1 t2, len1, Sil.Subtype.join st1 st2) + Sil.Sizeof (typ_star t1 t2, len1, Subtype.join st1 st2) | _ -> texp1 @@ -868,7 +868,7 @@ let mk_actual_precondition prop actual_params formal_params = Prop.mk_ptsto (Sil.Lvar formal_var) (Sil.Eexp (actual_e, Sil.inst_actual_precondition)) - (Sil.Sizeof (actual_t, None, Sil.Subtype.exact)) in + (Sil.Sizeof (actual_t, None, Subtype.exact)) in let instantiated_formals = IList.map mk_instantiation formals_actuals in let actual_pre = Prop.prop_sigma_star prop instantiated_formals in Prop.normalize actual_pre diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index 89ac4410e..bb358c9f0 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -216,7 +216,7 @@ struct CTypes_decl.objc_class_name_to_sil_type trans_state.context.CContext.tenv class_name in let expanded_type = CTypes.expand_structured_type trans_state.context.CContext.tenv typ in { empty_res_trans with - exps = [(Sil.Sizeof(expanded_type, None, Sil.Subtype.exact), Typ.Tint Typ.IULong)] } + exps = [(Sil.Sizeof(expanded_type, None, Subtype.exact), Typ.Tint Typ.IULong)] } let add_reference_if_glvalue typ expr_info = (* glvalue definition per C++11:*) @@ -428,7 +428,7 @@ struct | Some tp -> CTypes_decl.type_ptr_to_sil_type tenv tp | None -> typ in (* Some default type since the type is missing *) { empty_res_trans with - exps = [(Sil.Sizeof (sizeof_typ, None, Sil.Subtype.exact), sizeof_typ)] } + exps = [(Sil.Sizeof (sizeof_typ, None, Subtype.exact), sizeof_typ)] } | k -> Printing.log_stats "\nWARNING: Missing translation of Uniry_Expression_Or_Trait of kind: \ %s . Expression ignored, returned -1... \n" @@ -2180,7 +2180,7 @@ struct let trans_state_pri = PriorityNode.try_claim_priority_node trans_state stmt_info in let trans_state' = { trans_state_pri with succ_nodes = [] } in let context = trans_state.context in - let subtypes = Sil.Subtype.subtypes_cast in + let subtypes = Subtype.subtypes_cast in let tenv = context.CContext.tenv in let sil_loc = CLocation.get_sil_location stmt_info context in let cast_type = CTypes_decl.type_ptr_to_sil_type tenv cast_type_ptr in @@ -2243,7 +2243,7 @@ struct let fun_name = ModelBuiltins.__cxx_typeid in let sil_fun = Sil.Const (Const.Cfun fun_name) in let ret_id = Ident.create_fresh Ident.knormal in - let type_info_objc = (Sil.Sizeof (typ, None, Sil.Subtype.exact), Typ.Tvoid) in + let type_info_objc = (Sil.Sizeof (typ, None, Subtype.exact), Typ.Tvoid) in let field_name_decl = Ast_utils.make_qual_name_decl ["type_info"; "std"] "__type_name" in let field_name = General_utils.mk_class_field_name field_name_decl in let ret_exp = Sil.Var ret_id in diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml index cc1759be0..44111ad38 100644 --- a/infer/src/clang/cTrans_utils.ml +++ b/infer/src/clang/cTrans_utils.ml @@ -296,7 +296,7 @@ let create_alloc_instrs context sil_loc function_type fname size_exp_opt procnam function_type, styp | _ -> Typ.Tptr (function_type, Typ.Pk_pointer), function_type in let function_type_np = CTypes.expand_structured_type context.CContext.tenv function_type_np in - let sizeof_exp_ = Sil.Sizeof (function_type_np, None, Sil.Subtype.exact) in + let sizeof_exp_ = Sil.Sizeof (function_type_np, None, Subtype.exact) in let sizeof_exp = match size_exp_opt with | Some exp -> Sil.BinOp (Binop.Mult, sizeof_exp_, exp) | None -> sizeof_exp_ in @@ -367,7 +367,7 @@ let create_cast_instrs context exp cast_from_typ cast_to_typ sil_loc = let ret_id = Ident.create_fresh Ident.knormal in let typ = CTypes.remove_pointer_to_typ cast_to_typ in let cast_typ_no_pointer = CTypes.expand_structured_type context.CContext.tenv typ in - let sizeof_exp = Sil.Sizeof (cast_typ_no_pointer, None, Sil.Subtype.exact) in + let sizeof_exp = Sil.Sizeof (cast_typ_no_pointer, None, Subtype.exact) in let pname = ModelBuiltins.__objc_cast in let args = [(exp, cast_from_typ); (sizeof_exp, Typ.Tint Typ.IULong)] in let stmt_call = diff --git a/infer/src/harness/inhabit.ml b/infer/src/harness/inhabit.ml index 51c8be257..f428d3264 100644 --- a/infer/src/harness/inhabit.ml +++ b/infer/src/harness/inhabit.ml @@ -73,7 +73,7 @@ let inhabit_alloc sizeof_typ sizeof_len ret_typ alloc_kind env = let inhabited_exp = Sil.Var retval in let call_instr = let fun_new = fun_exp_from_name alloc_kind in - let sizeof_exp = Sil.Sizeof (sizeof_typ, sizeof_len, Sil.Subtype.exact) in + let sizeof_exp = Sil.Sizeof (sizeof_typ, sizeof_len, Subtype.exact) in let args = [(sizeof_exp, Typ.Tptr (ret_typ, Typ.Pk_pointer))] in Sil.Call ([retval], fun_new, args, env.pc, cf_alloc) in (inhabited_exp, env_add_instr call_instr env) diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index f60a6a6cb..a16bc4dec 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -456,8 +456,8 @@ let rec expression context pc expr = | JBir.InstanceOf ot | JBir.Cast ot -> let subtypes = (match unop with - | JBir.InstanceOf _ -> Sil.Subtype.subtypes_instof - | JBir.Cast _ -> Sil.Subtype.subtypes_cast + | JBir.InstanceOf _ -> Subtype.subtypes_instof + | JBir.Cast _ -> Subtype.subtypes_cast | _ -> assert false) in let sizeof_expr = JTransType.sizeof_of_object_type program tenv ot subtypes in @@ -650,7 +650,7 @@ let get_array_length context pc expr_list content_type = (Typ.Tarray (content_type, None), Some sil_len_expr) in let array_type, array_len = IList.fold_right get_array_type_len sil_len_exprs (content_type, None) in - let array_size = Sil.Sizeof (array_type, array_len, Sil.Subtype.exact) in + let array_size = Sil.Sizeof (array_type, array_len, Subtype.exact) in (instrs, array_size) let detect_loop entry_pc impl = @@ -900,7 +900,7 @@ let rec instruction context pc instr : translation = let builtin_new = Sil.Const (Const.Cfun ModelBuiltins.__new) in let class_type = JTransType.get_class_type program tenv cn in let class_type_np = JTransType.get_class_type_no_pointer program tenv cn in - let sizeof_exp = Sil.Sizeof (class_type_np, None, Sil.Subtype.exact) in + let sizeof_exp = Sil.Sizeof (class_type_np, None, Subtype.exact) in let args = [(sizeof_exp, class_type)] in let ret_id = Ident.create_fresh Ident.knormal in let new_instr = Sil.Call([ret_id], builtin_new, args, loc, Sil.cf_default) in @@ -1014,7 +1014,7 @@ let rec instruction context pc instr : translation = and npe_cn = JBasics.make_cn JConfig.npe_cl in let class_type = JTransType.get_class_type program tenv npe_cn and class_type_np = JTransType.get_class_type_no_pointer program tenv npe_cn in - let sizeof_exp = Sil.Sizeof (class_type_np, None, Sil.Subtype.exact) in + let sizeof_exp = Sil.Sizeof (class_type_np, None, Subtype.exact) in let args = [(sizeof_exp, class_type)] in let ret_id = Ident.create_fresh Ident.knormal in let new_instr = Sil.Call([ret_id], builtin_new, args, loc, Sil.cf_default) in @@ -1067,7 +1067,7 @@ let rec instruction context pc instr : translation = let out_of_bound_cn = JBasics.make_cn JConfig.out_of_bound_cl in let class_type = JTransType.get_class_type program tenv out_of_bound_cn and class_type_np = JTransType.get_class_type_no_pointer program tenv out_of_bound_cn in - let sizeof_exp = Sil.Sizeof (class_type_np, None, Sil.Subtype.exact) in + let sizeof_exp = Sil.Sizeof (class_type_np, None, Subtype.exact) in let args = [(sizeof_exp, class_type)] in let ret_id = Ident.create_fresh Ident.knormal in let new_instr = Sil.Call([ret_id], builtin_new, args, loc, Sil.cf_default) in @@ -1089,7 +1089,7 @@ let rec instruction context pc instr : translation = and instrs, sil_expr, _ = expression context pc expr and ret_id = Ident.create_fresh Ident.knormal and sizeof_expr = - JTransType.sizeof_of_object_type program tenv object_type Sil.Subtype.subtypes_instof in + JTransType.sizeof_of_object_type program tenv object_type Subtype.subtypes_instof in let check_cast = Sil.Const (Const.Cfun ModelBuiltins.__instanceof) in let args = [(sil_expr, sil_type); (sizeof_expr, Typ.Tvoid)] in let call = Sil.Call([ret_id], check_cast, args, loc, Sil.cf_default) in @@ -1106,7 +1106,7 @@ let rec instruction context pc instr : translation = and cce_cn = JBasics.make_cn JConfig.cce_cl in let class_type = JTransType.get_class_type program tenv cce_cn and class_type_np = JTransType.get_class_type_no_pointer program tenv cce_cn in - let sizeof_exp = Sil.Sizeof (class_type_np, None, Sil.Subtype.exact) in + let sizeof_exp = Sil.Sizeof (class_type_np, None, Subtype.exact) in let args = [(sizeof_exp, class_type)] in let ret_id = Ident.create_fresh Ident.knormal in let new_instr = Sil.Call([ret_id], builtin_new, args, loc, Sil.cf_default) in diff --git a/infer/src/java/jTransExn.ml b/infer/src/java/jTransExn.ml index f3302ffc1..8ddd01a2a 100644 --- a/infer/src/java/jTransExn.ml +++ b/infer/src/java/jTransExn.ml @@ -69,7 +69,7 @@ let translate_exceptions context exit_nodes get_body_nodes handler_table = let instanceof_builtin = Sil.Const (Const.Cfun ModelBuiltins.__instanceof) in let args = [ (Sil.Var id_exn_val, Typ.Tptr(exn_type, Typ.Pk_pointer)); - (Sil.Sizeof (exn_type, None, Sil.Subtype.exact), Typ.Tvoid)] in + (Sil.Sizeof (exn_type, None, Subtype.exact), Typ.Tvoid)] in Sil.Call ([id_instanceof], instanceof_builtin, args, loc, Sil.cf_default) in let if_kind = Sil.Ik_switch in let instr_prune_true = Sil.Prune (Sil.Var id_instanceof, loc, true, if_kind) in diff --git a/infer/src/java/jTransType.mli b/infer/src/java/jTransType.mli index 537927de6..caa2a57de 100644 --- a/infer/src/java/jTransType.mli +++ b/infer/src/java/jTransType.mli @@ -45,7 +45,7 @@ val is_closeable : JClasspath.program -> Tenv.t -> Typ.t -> bool val object_type : JClasspath.program -> Tenv.t -> JBasics.object_type -> Typ.t (** create sizeof expressions from the object type and the list of subtypes *) -val sizeof_of_object_type : JClasspath.program -> Tenv.t -> JBasics.object_type -> Sil.Subtype.t +val sizeof_of_object_type : JClasspath.program -> Tenv.t -> JBasics.object_type -> Subtype.t -> Sil.exp (** transforms a Java type to a Typ.t. *)