|
|
@ -18,7 +18,6 @@ module TypSet = Sil.TypSet
|
|
|
|
module TypMap = Sil.TypMap
|
|
|
|
module TypMap = Sil.TypMap
|
|
|
|
|
|
|
|
|
|
|
|
type lifecycle_trace = (Procname.t * Sil.typ option) list
|
|
|
|
type lifecycle_trace = (Procname.t * Sil.typ option) list
|
|
|
|
type callback_trace = (Sil.exp * Sil.typ) list
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(** list of instrs and temporary variables created during inhabitation and a cache of types that
|
|
|
|
(** list of instrs and temporary variables created during inhabitation and a cache of types that
|
|
|
|
* have already been inhabited *)
|
|
|
|
* have already been inhabited *)
|
|
|
@ -30,6 +29,20 @@ type env = { instrs : Sil.instr list;
|
|
|
|
pc : Location.t;
|
|
|
|
pc : Location.t;
|
|
|
|
harness_name : Procname.java }
|
|
|
|
harness_name : Procname.java }
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let procdesc_from_name cfg pname =
|
|
|
|
|
|
|
|
let pdesc_ref = ref None in
|
|
|
|
|
|
|
|
Cfg.iter_proc_desc cfg
|
|
|
|
|
|
|
|
(fun cfg_pname pdesc ->
|
|
|
|
|
|
|
|
if Procname.equal cfg_pname pname then
|
|
|
|
|
|
|
|
pdesc_ref := Some pdesc
|
|
|
|
|
|
|
|
);
|
|
|
|
|
|
|
|
!pdesc_ref
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let formals_from_name cfg pname =
|
|
|
|
|
|
|
|
match procdesc_from_name cfg pname with
|
|
|
|
|
|
|
|
| Some pdesc -> Cfg.Procdesc.get_formals pdesc
|
|
|
|
|
|
|
|
| None -> []
|
|
|
|
|
|
|
|
|
|
|
|
(** add an instruction to the env, update tmp_vars, and bump the pc *)
|
|
|
|
(** add an instruction to the env, update tmp_vars, and bump the pc *)
|
|
|
|
let env_add_instr instr tmp_vars env =
|
|
|
|
let env_add_instr instr tmp_vars env =
|
|
|
|
let incr_pc pc = { pc with Location.line = pc.Location.line + 1 } in
|
|
|
|
let incr_pc pc = { pc with Location.line = pc.Location.line + 1 } in
|
|
|
@ -40,33 +53,6 @@ let cf_alloc = Sil.cf_default
|
|
|
|
|
|
|
|
|
|
|
|
let fun_exp_from_name proc_name = Sil.Const (Sil.Cfun (proc_name))
|
|
|
|
let fun_exp_from_name proc_name = Sil.Const (Sil.Cfun (proc_name))
|
|
|
|
|
|
|
|
|
|
|
|
let source_dir_from_name proc_name proc_file_map =
|
|
|
|
|
|
|
|
let source_file = Procname.Map.find proc_name proc_file_map in
|
|
|
|
|
|
|
|
DB.source_dir_from_source_file source_file
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let cfg_from_name proc_name proc_file_map =
|
|
|
|
|
|
|
|
let source_dir = source_dir_from_name proc_name proc_file_map in
|
|
|
|
|
|
|
|
let cfg_fname = DB.source_dir_get_internal_file source_dir ".cfg" in
|
|
|
|
|
|
|
|
match Cfg.load_cfg_from_file cfg_fname with
|
|
|
|
|
|
|
|
| Some cfg -> cfg
|
|
|
|
|
|
|
|
| None -> assert false
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let cg_from_name proc_name proc_file_map =
|
|
|
|
|
|
|
|
let source_dir = source_dir_from_name proc_name proc_file_map in
|
|
|
|
|
|
|
|
let cg_fname = DB.source_dir_get_internal_file source_dir ".cg" in
|
|
|
|
|
|
|
|
match Cg.load_from_file cg_fname with
|
|
|
|
|
|
|
|
| Some cfg -> cfg
|
|
|
|
|
|
|
|
| None -> assert false
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let procdesc_from_name proc_name proc_file_map =
|
|
|
|
|
|
|
|
match Cfg.Procdesc.find_from_name (cfg_from_name proc_name proc_file_map) proc_name with
|
|
|
|
|
|
|
|
| Some proc_desc -> proc_desc
|
|
|
|
|
|
|
|
| None -> assert false
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let formals_from_name proc_name proc_file_map =
|
|
|
|
|
|
|
|
let procdesc = procdesc_from_name proc_name proc_file_map in
|
|
|
|
|
|
|
|
Cfg.Procdesc.get_formals procdesc
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let local_name_cntr = ref 0
|
|
|
|
let local_name_cntr = ref 0
|
|
|
|
|
|
|
|
|
|
|
|
let create_fresh_local_name () =
|
|
|
|
let create_fresh_local_name () =
|
|
|
@ -92,7 +78,8 @@ let inhabit_alloc sizeof_typ ret_typ alloc_kind env =
|
|
|
|
(inhabited_exp, env_add_instr call_instr [retval] env)
|
|
|
|
(inhabited_exp, env_add_instr call_instr [retval] env)
|
|
|
|
|
|
|
|
|
|
|
|
(** find or create a Sil expression with type typ *)
|
|
|
|
(** find or create a Sil expression with type typ *)
|
|
|
|
let rec inhabit_typ typ proc_file_map env =
|
|
|
|
(* TODO: this should be done in a differnt way: just make typ a param of the harness procedure *)
|
|
|
|
|
|
|
|
let rec inhabit_typ 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 with
|
|
|
@ -110,8 +97,7 @@ let rec inhabit_typ typ proc_file_map env =
|
|
|
|
| Sil.Tstruct { Sil.csu = Csu.Class _; def_methods } ->
|
|
|
|
| Sil.Tstruct { Sil.csu = Csu.Class _; def_methods } ->
|
|
|
|
let is_suitable_constructor p =
|
|
|
|
let is_suitable_constructor p =
|
|
|
|
let try_get_non_receiver_formals p =
|
|
|
|
let try_get_non_receiver_formals p =
|
|
|
|
try get_non_receiver_formals (formals_from_name p proc_file_map)
|
|
|
|
get_non_receiver_formals (formals_from_name cfg p) in
|
|
|
|
with Not_found -> [] in
|
|
|
|
|
|
|
|
Procname.is_constructor p && IList.for_all (fun (_, typ) ->
|
|
|
|
Procname.is_constructor p && IList.for_all (fun (_, typ) ->
|
|
|
|
not (TypSet.mem typ env.cur_inhabiting)) (try_get_non_receiver_formals p) in
|
|
|
|
not (TypSet.mem typ env.cur_inhabiting)) (try_get_non_receiver_formals p) in
|
|
|
|
IList.filter (fun p -> is_suitable_constructor p) def_methods
|
|
|
|
IList.filter (fun p -> is_suitable_constructor p) def_methods
|
|
|
@ -121,7 +107,7 @@ let rec inhabit_typ typ proc_file_map 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 constructor (allocated_obj_exp, ptr_to_typ) proc_file_map env in
|
|
|
|
inhabit_constructor constructor (allocated_obj_exp, ptr_to_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 =
|
|
|
@ -154,21 +140,21 @@ let rec inhabit_typ typ proc_file_map env =
|
|
|
|
cur_inhabiting = env.cur_inhabiting })
|
|
|
|
cur_inhabiting = env.cur_inhabiting })
|
|
|
|
|
|
|
|
|
|
|
|
(** inhabit each of the types in the formals list *)
|
|
|
|
(** inhabit each of the types in the formals list *)
|
|
|
|
and inhabit_args formals proc_file_map env =
|
|
|
|
and inhabit_args formals cfg env =
|
|
|
|
let inhabit_arg (_, formal_typ) (args, env) =
|
|
|
|
let inhabit_arg (_, formal_typ) (args, env) =
|
|
|
|
let (exp, env) = inhabit_typ formal_typ proc_file_map env in
|
|
|
|
let (exp, env) = inhabit_typ formal_typ cfg env in
|
|
|
|
((exp, formal_typ) :: args, env) in
|
|
|
|
((exp, formal_typ) :: args, env) in
|
|
|
|
IList.fold_right inhabit_arg formals ([], env)
|
|
|
|
IList.fold_right inhabit_arg formals ([], env)
|
|
|
|
|
|
|
|
|
|
|
|
(** create Sil that calls the constructor in constr_name on allocated_obj and inhabits the
|
|
|
|
(** create Sil that calls the constructor in constr_name on allocated_obj and inhabits the
|
|
|
|
* remaining arguments *)
|
|
|
|
* remaining arguments *)
|
|
|
|
and inhabit_constructor constr_name (allocated_obj, obj_type) proc_file_map env =
|
|
|
|
and inhabit_constructor constr_name (allocated_obj, obj_type) cfg env =
|
|
|
|
try
|
|
|
|
try
|
|
|
|
(* this lookup can fail when we try to get the procdesc of a procedure from a different
|
|
|
|
(* this lookup can fail when we try to get the procdesc of a procedure from a different
|
|
|
|
* module. this could be solved with a whole - program class hierarchy analysis *)
|
|
|
|
* module. this could be solved with a whole - program class hierarchy analysis *)
|
|
|
|
let (args, env) =
|
|
|
|
let (args, env) =
|
|
|
|
let non_receiver_formals = tl_or_empty (formals_from_name constr_name proc_file_map) in
|
|
|
|
let non_receiver_formals = tl_or_empty (formals_from_name cfg constr_name) in
|
|
|
|
inhabit_args non_receiver_formals proc_file_map env in
|
|
|
|
inhabit_args non_receiver_formals cfg env in
|
|
|
|
let constr_instr =
|
|
|
|
let constr_instr =
|
|
|
|
let fun_exp = fun_exp_from_name constr_name in
|
|
|
|
let fun_exp = fun_exp_from_name constr_name in
|
|
|
|
Sil.Call ([], fun_exp, (allocated_obj, obj_type) :: args, env.pc, Sil.cf_default) in
|
|
|
|
Sil.Call ([], fun_exp, (allocated_obj, obj_type) :: args, env.pc, Sil.cf_default) in
|
|
|
@ -186,47 +172,24 @@ let inhabit_call_with_args procname procdesc args env =
|
|
|
|
env_add_instr call_instr retval env
|
|
|
|
env_add_instr call_instr retval env
|
|
|
|
|
|
|
|
|
|
|
|
(** create Sil that inhabits args to and calls proc_name *)
|
|
|
|
(** create Sil that inhabits args to and calls proc_name *)
|
|
|
|
let inhabit_call (procname, receiver) proc_file_map env =
|
|
|
|
let inhabit_call (procname, receiver) cfg env =
|
|
|
|
try
|
|
|
|
try
|
|
|
|
let procdesc = procdesc_from_name procname proc_file_map in
|
|
|
|
match procdesc_from_name cfg procname with
|
|
|
|
(* swap the type of the 'this' formal with the receiver type, if there is one *)
|
|
|
|
| Some procdesc ->
|
|
|
|
let formals = match (Cfg.Procdesc.get_formals procdesc, receiver) with
|
|
|
|
(* swap the type of the 'this' formal with the receiver type, if there is one *)
|
|
|
|
| ((name, _) :: formals, Some receiver) -> (name, receiver) :: formals
|
|
|
|
let formals = match (Cfg.Procdesc.get_formals procdesc, receiver) with
|
|
|
|
| (formals, None) -> formals
|
|
|
|
| ((name, _) :: formals, Some receiver) -> (name, receiver) :: formals
|
|
|
|
| ([], Some _) ->
|
|
|
|
| (formals, None) -> formals
|
|
|
|
L.err
|
|
|
|
| ([], Some _) ->
|
|
|
|
"Expected at least one formal to bind receiver to in method %a@." Procname.pp procname;
|
|
|
|
L.err
|
|
|
|
assert false in
|
|
|
|
"Expected at least one formal to bind receiver to in method %a@."
|
|
|
|
let (args, env) = inhabit_args formals proc_file_map env in
|
|
|
|
Procname.pp procname;
|
|
|
|
inhabit_call_with_args procname procdesc args env
|
|
|
|
assert false in
|
|
|
|
|
|
|
|
let (args, env) = inhabit_args formals cfg env in
|
|
|
|
|
|
|
|
inhabit_call_with_args procname procdesc args env
|
|
|
|
|
|
|
|
| None -> env
|
|
|
|
with Not_found -> env
|
|
|
|
with Not_found -> env
|
|
|
|
|
|
|
|
|
|
|
|
let inhabit_fld_trace flds proc_file_map env =
|
|
|
|
|
|
|
|
let invoke_cb (fld_exp, fld_typ) env =
|
|
|
|
|
|
|
|
let lhs = Ident.create_fresh Ident.knormal in
|
|
|
|
|
|
|
|
let fld_read_instr =
|
|
|
|
|
|
|
|
Sil.Letderef (lhs, fld_exp, fld_typ, env.pc) in
|
|
|
|
|
|
|
|
let env = env_add_instr fld_read_instr [lhs] env in
|
|
|
|
|
|
|
|
match fld_typ with
|
|
|
|
|
|
|
|
| Sil.Tptr (Sil.Tstruct { Sil.csu = Csu.Class _; def_methods }, _) ->
|
|
|
|
|
|
|
|
let inhabit_cb_call procname env =
|
|
|
|
|
|
|
|
try
|
|
|
|
|
|
|
|
let procdesc = procdesc_from_name procname proc_file_map in
|
|
|
|
|
|
|
|
(* replace receiver arg with the value read from the field, inhabit other args *)
|
|
|
|
|
|
|
|
let (args, env) =
|
|
|
|
|
|
|
|
let formals = Cfg.Procdesc.get_formals procdesc in
|
|
|
|
|
|
|
|
inhabit_args (tl_or_empty formals) proc_file_map env in
|
|
|
|
|
|
|
|
inhabit_call_with_args procname procdesc ((Sil.Var lhs, fld_typ) :: args) env
|
|
|
|
|
|
|
|
with Not_found ->
|
|
|
|
|
|
|
|
(* TODO (t4645631): investigate why this failure occurs *)
|
|
|
|
|
|
|
|
env in
|
|
|
|
|
|
|
|
IList.fold_left (fun env procname ->
|
|
|
|
|
|
|
|
if not (Procname.is_constructor procname) &&
|
|
|
|
|
|
|
|
not (Procname.java_is_access_method procname) then inhabit_cb_call procname env
|
|
|
|
|
|
|
|
else env) env def_methods
|
|
|
|
|
|
|
|
| _ -> assert false in
|
|
|
|
|
|
|
|
IList.fold_left (fun env fld -> invoke_cb fld env) env flds
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(** create a dummy file for the harness and associate them in the exe_env *)
|
|
|
|
(** create a dummy file for the harness and associate them in the exe_env *)
|
|
|
|
let create_dummy_harness_file harness_name =
|
|
|
|
let create_dummy_harness_file harness_name =
|
|
|
|
let dummy_file_name =
|
|
|
|
let dummy_file_name =
|
|
|
@ -260,29 +223,23 @@ let add_harness_to_cg harness_name harness_node cg =
|
|
|
|
|
|
|
|
|
|
|
|
(** create and fill the appropriate nodes and add them to the harness cfg. also add the harness
|
|
|
|
(** create and fill the appropriate nodes and add them to the harness cfg. also add the harness
|
|
|
|
* proc to the cg *)
|
|
|
|
* proc to the cg *)
|
|
|
|
let setup_harness_cfg harness_name env source_dir cg =
|
|
|
|
let setup_harness_cfg harness_name env cg cfg =
|
|
|
|
(* each procedure has different scope: start names from id 0 *)
|
|
|
|
(* each procedure has different scope: start names from id 0 *)
|
|
|
|
Ident.NameGenerator.reset ();
|
|
|
|
Ident.NameGenerator.reset ();
|
|
|
|
|
|
|
|
|
|
|
|
let cfg_file = DB.source_dir_get_internal_file source_dir ".cfg" in
|
|
|
|
|
|
|
|
let harness_cfg = match Cfg.load_cfg_from_file cfg_file with
|
|
|
|
|
|
|
|
| Some cfg -> cfg
|
|
|
|
|
|
|
|
| None -> assert false in
|
|
|
|
|
|
|
|
let cg_file = DB.source_dir_get_internal_file source_dir ".cg" in
|
|
|
|
|
|
|
|
let procdesc =
|
|
|
|
let procdesc =
|
|
|
|
let proc_attributes =
|
|
|
|
let proc_attributes =
|
|
|
|
{ (ProcAttributes.default (Procname.Java harness_name) Config.Java) with
|
|
|
|
{ (ProcAttributes.default (Procname.Java harness_name) Config.Java) with
|
|
|
|
ProcAttributes.is_defined = true;
|
|
|
|
ProcAttributes.is_defined = true;
|
|
|
|
loc = env.pc;
|
|
|
|
loc = env.pc;
|
|
|
|
} in
|
|
|
|
} in
|
|
|
|
Cfg.Procdesc.create harness_cfg proc_attributes in
|
|
|
|
Cfg.Procdesc.create cfg proc_attributes in
|
|
|
|
let harness_node =
|
|
|
|
let harness_node =
|
|
|
|
(* important to reverse the list or there will be scoping issues! *)
|
|
|
|
(* important to reverse the list or there will be scoping issues! *)
|
|
|
|
let instrs = (IList.rev env.instrs) in
|
|
|
|
let instrs = (IList.rev env.instrs) in
|
|
|
|
let nodekind = Cfg.Node.Stmt_node "method_body" in
|
|
|
|
let nodekind = Cfg.Node.Stmt_node "method_body" in
|
|
|
|
Cfg.Node.create harness_cfg env.pc nodekind instrs procdesc env.tmp_vars in
|
|
|
|
Cfg.Node.create cfg env.pc nodekind instrs procdesc env.tmp_vars in
|
|
|
|
let (start_node, exit_node) =
|
|
|
|
let (start_node, exit_node) =
|
|
|
|
let create_node kind = Cfg.Node.create harness_cfg env.pc kind [] procdesc [] in
|
|
|
|
let create_node kind = Cfg.Node.create cfg env.pc kind [] procdesc [] in
|
|
|
|
let start_kind = Cfg.Node.Start_node procdesc in
|
|
|
|
let start_kind = Cfg.Node.Start_node procdesc in
|
|
|
|
let exit_kind = Cfg.Node.Exit_node procdesc in
|
|
|
|
let exit_kind = Cfg.Node.Exit_node procdesc in
|
|
|
|
(create_node start_kind, create_node exit_kind) in
|
|
|
|
(create_node start_kind, create_node exit_kind) in
|
|
|
@ -291,21 +248,13 @@ let setup_harness_cfg harness_name env source_dir cg =
|
|
|
|
Cfg.Node.add_locals_ret_declaration start_node [];
|
|
|
|
Cfg.Node.add_locals_ret_declaration start_node [];
|
|
|
|
Cfg.Node.set_succs_exn start_node [harness_node] [exit_node];
|
|
|
|
Cfg.Node.set_succs_exn start_node [harness_node] [exit_node];
|
|
|
|
Cfg.Node.set_succs_exn harness_node [exit_node] [exit_node];
|
|
|
|
Cfg.Node.set_succs_exn harness_node [exit_node] [exit_node];
|
|
|
|
add_harness_to_cg harness_name harness_node cg;
|
|
|
|
add_harness_to_cg harness_name harness_node cg
|
|
|
|
(* save out the cg and cfg so that they will be accessible in the next phase of the analysis *)
|
|
|
|
|
|
|
|
Cg.store_to_file cg_file cg;
|
|
|
|
|
|
|
|
Cfg.store_cfg_to_file cfg_file false harness_cfg
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(** create a procedure named harness_name that calls each of the methods in trace in the specified
|
|
|
|
(** create a procedure named harness_name that calls each of the methods in trace in the specified
|
|
|
|
* order with the specified receiver and add it to the execution environment *)
|
|
|
|
* order with the specified receiver and add it to the execution environment *)
|
|
|
|
let inhabit_trace trace cb_flds harness_name proc_file_map =
|
|
|
|
let inhabit_trace trace harness_name cg cfg =
|
|
|
|
if IList.length trace > 0 then
|
|
|
|
if IList.length trace > 0 then
|
|
|
|
(* pick an arbitrary cg and cfg to piggyback the harness code onto *)
|
|
|
|
let source_file = Cg.get_source cg in
|
|
|
|
let (source_dir, source_file, cg) =
|
|
|
|
|
|
|
|
let (proc_name, source_file) = Procname.Map.choose proc_file_map in
|
|
|
|
|
|
|
|
let cg = cg_from_name proc_name proc_file_map in
|
|
|
|
|
|
|
|
(source_dir_from_name proc_name proc_file_map, source_file, cg) in
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let harness_file = create_dummy_harness_file harness_name in
|
|
|
|
let harness_file = create_dummy_harness_file harness_name in
|
|
|
|
let start_line = (Cg.get_nLOC cg) + 1 in
|
|
|
|
let start_line = (Cg.get_nLOC cg) + 1 in
|
|
|
|
let empty_env =
|
|
|
|
let empty_env =
|
|
|
@ -316,14 +265,9 @@ let inhabit_trace trace cb_flds harness_name proc_file_map =
|
|
|
|
pc = pc;
|
|
|
|
pc = pc;
|
|
|
|
cur_inhabiting = TypSet.empty;
|
|
|
|
cur_inhabiting = TypSet.empty;
|
|
|
|
harness_name = harness_name; } in
|
|
|
|
harness_name = harness_name; } in
|
|
|
|
(* synthesize the harness body *)
|
|
|
|
(* invoke lifecycle methods *)
|
|
|
|
let env'' =
|
|
|
|
let env'' = IList.fold_left (fun env to_call -> inhabit_call to_call cfg env) empty_env trace in
|
|
|
|
(* invoke lifecycle methods *)
|
|
|
|
|
|
|
|
let env' =
|
|
|
|
|
|
|
|
IList.fold_left (fun env to_call -> inhabit_call to_call proc_file_map env) empty_env trace in
|
|
|
|
|
|
|
|
(* invoke callbacks *)
|
|
|
|
|
|
|
|
inhabit_fld_trace cb_flds proc_file_map env' in
|
|
|
|
|
|
|
|
try
|
|
|
|
try
|
|
|
|
setup_harness_cfg harness_name env'' source_dir cg;
|
|
|
|
setup_harness_cfg harness_name env'' cg cfg;
|
|
|
|
write_harness_to_file (IList.rev env''.instrs) harness_file
|
|
|
|
write_harness_to_file (IList.rev env''.instrs) harness_file
|
|
|
|
with Not_found -> ()
|
|
|
|
with Not_found -> ()
|
|
|
|