[frontend] Move Preanalysis to frontend so that it is run always

Summary:
I realized that there was a discrepancy in the # of instructions between whether we run a single analysis or multiple analyses at the same time. It turns out that in biabduction, bufferoverrun and other HIL analyses we did Preanalysis step (which adds scope instructions and invokes liveness etc.) but not in others. This discrepancy results in inconsistent analysis results (e.g. in the new inefficient-keyset-iterator) that rely on instructions. We should be consistent. Hence, we now invoke Preanalysis in the frontend and remove all other uses in the rest of the checkers.

Consequently, I had to update the inefficient-keyset-checker to take the CFG resulting from Preanalysis with extra scoping instructions.

Reviewed By: mbouaziz, ngorogiannis, jvillard

Differential Revision: D15803492

fbshipit-source-id: 4e21eb610
master
Ezgi Çiçek 6 years ago committed by Facebook Github Bot
parent 46f5667823
commit be85296759

@ -117,8 +117,7 @@ module MakeAbstractInterpreterWithConfig
type domain = TransferFunctions.Domain.t type domain = TransferFunctions.Domain.t
let compute_post ({ProcData.pdesc; tenv} as proc_data) ~initial = let compute_post proc_data ~initial =
Preanal.do_preanalysis pdesc tenv ;
let initial' = (initial, Bindings.empty) in let initial' = (initial, Bindings.empty) in
let pp_instr (_, bindings) instr = let pp_instr (_, bindings) instr =
match LowerHilInterpreter.hil_instr_of_sil bindings instr with match LowerHilInterpreter.hil_instr_of_sil bindings instr with

@ -1164,14 +1164,12 @@ let print_icfg source fmt cfg =
if Config.dotty_cfg_libs || SourceFile.equal loc.Location.file source then if Config.dotty_cfg_libs || SourceFile.equal loc.Location.file source then
F.fprintf fmt "%a@\n" (pp_cfgnode pdesc) node F.fprintf fmt "%a@\n" (pp_cfgnode pdesc) node
in in
let print_pdesc tenv_opt pdesc = let print_pdesc pdesc =
Option.iter tenv_opt ~f:(fun tenv -> Preanal.do_preanalysis pdesc tenv) ;
Procdesc.get_nodes pdesc Procdesc.get_nodes pdesc
|> List.sort ~compare:Procdesc.Node.compare |> List.sort ~compare:Procdesc.Node.compare
|> List.iter ~f:(fun node -> print_node pdesc node) |> List.iter ~f:(fun node -> print_node pdesc node)
in in
let tenv = Tenv.load source in Cfg.iter_sorted cfg ~f:(fun pdesc -> print_pdesc pdesc)
Cfg.iter_sorted cfg ~f:(fun pdesc -> print_pdesc tenv pdesc)
let write_icfg_dotty_to_file source cfg fname = let write_icfg_dotty_to_file source cfg fname =

@ -1224,7 +1224,6 @@ let perform_transition proc_cfg tenv proc_name summary =
let analyze_procedure_aux summary exe_env tenv proc_desc : Summary.t = let analyze_procedure_aux summary exe_env tenv proc_desc : Summary.t =
let proc_name = Procdesc.get_proc_name proc_desc in let proc_name = Procdesc.get_proc_name proc_desc in
let proc_cfg = ProcCfg.Exceptional.from_pdesc proc_desc in let proc_cfg = ProcCfg.Exceptional.from_pdesc proc_desc in
Preanal.do_preanalysis proc_desc tenv ;
let summaryfp = let summaryfp =
BiabductionConfig.run_in_footprint_mode (analyze_proc summary exe_env tenv) proc_cfg BiabductionConfig.run_in_footprint_mode (analyze_proc summary exe_env tenv) proc_cfg
|> perform_transition proc_cfg tenv proc_name |> perform_transition proc_cfg tenv proc_name

@ -311,7 +311,6 @@ let get_local_decls : Procdesc.t -> local_decls =
let compute_invariant_map : let compute_invariant_map :
Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t -> get_proc_summary_and_formals -> invariant_map = Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t -> get_proc_summary_and_formals -> invariant_map =
fun pdesc tenv integer_type_widths get_proc_summary_and_formals -> fun pdesc tenv integer_type_widths get_proc_summary_and_formals ->
Preanal.do_preanalysis pdesc tenv ;
let cfg = CFG.from_pdesc pdesc in let cfg = CFG.from_pdesc pdesc in
let pdata = let pdata =
let oenv = Dom.OndemandEnv.mk pdesc tenv integer_type_widths in let oenv = Dom.OndemandEnv.mk pdesc tenv integer_type_widths in

@ -33,7 +33,7 @@ let find_first_arg_id ~fun_name ~lhs_f = function
*) *)
let find_first_arg_pvar node ~fun_name = let find_first_arg_pvar node ~fun_name =
let instrs = Procdesc.Node.get_instrs node in let instrs = Procdesc.Node.get_instrs node in
if Int.equal (Instrs.count instrs) 4 then if Instrs.count instrs >= 4 then
let instr_arr = Instrs.get_underlying_not_reversed instrs in let instr_arr = Instrs.get_underlying_not_reversed instrs in
match instr_arr.(3) with match instr_arr.(3) with
| Sil.Store (Exp.Lvar _, _, Exp.Var rhs_id, _) -> | Sil.Store (Exp.Lvar _, _, Exp.Var rhs_id, _) ->
@ -48,7 +48,7 @@ let report_matching_get summary pvar loop_nodes : unit =
LoopNodes.iter LoopNodes.iter
(fun node -> (fun node ->
let instrs = Procdesc.Node.get_instrs node in let instrs = Procdesc.Node.get_instrs node in
if Int.equal (Instrs.count instrs) 5 then if Instrs.count instrs >= 5 then
let instr_arr = Instrs.get_underlying_not_reversed instrs in let instr_arr = Instrs.get_underlying_not_reversed instrs in
find_first_arg_id ~fun_name:"get" ~lhs_f:(fun _ -> true) instr_arr.(3) find_first_arg_id ~fun_name:"get" ~lhs_f:(fun _ -> true) instr_arr.(3)
|> Option.iter ~f:(fun arg_id -> |> Option.iter ~f:(fun arg_id ->

@ -55,7 +55,8 @@ let do_source_file (translation_unit_context : CFrontend_config.translation_unit
(* This part below is a boilerplate in every frontends. *) (* This part below is a boilerplate in every frontends. *)
(* This could be moved in the cfg_infer module *) (* This could be moved in the cfg_infer module *)
NullabilityPreanalysis.analysis cfg tenv ; NullabilityPreanalysis.analysis cfg tenv ;
SourceFiles.add source_file cfg (FileLocal tenv) (Some integer_type_widths) ; Typ.Procname.Hash.iter (fun _ pdesc -> Preanal.do_preanalysis pdesc tenv) cfg ;
SourceFiles.add source_file cfg (Tenv.FileLocal tenv) (Some integer_type_widths) ;
if Config.debug_mode then Tenv.store_debug_file_for_source source_file tenv ; if Config.debug_mode then Tenv.store_debug_file_for_source source_file tenv ;
if if
Config.debug_mode || Config.testing_mode || Config.frontend_tests Config.debug_mode || Config.testing_mode || Config.frontend_tests

@ -19,7 +19,8 @@ let init_global_state source_file =
JContext.reset_exn_node_table () JContext.reset_exn_node_table ()
let store_icfg source_file cfg = let store_icfg tenv source_file cfg =
Typ.Procname.Hash.iter (fun _ pdesc -> Preanal.do_preanalysis pdesc tenv) cfg ;
SourceFiles.add source_file cfg Tenv.Global None ; SourceFiles.add source_file cfg Tenv.Global None ;
if Config.debug_mode || Config.frontend_tests then Dotty.print_icfg_dotty source_file cfg ; if Config.debug_mode || Config.frontend_tests then Dotty.print_icfg_dotty source_file cfg ;
() ()
@ -34,7 +35,7 @@ let do_source_file linereader classes program tenv source_basename package_opt s
JFrontend.compute_source_icfg linereader classes program tenv source_basename package_opt JFrontend.compute_source_icfg linereader classes program tenv source_basename package_opt
source_file source_file
in in
store_icfg source_file cfg store_icfg tenv source_file cfg
let capture_libs linereader program tenv = let capture_libs linereader program tenv =
@ -48,7 +49,8 @@ let capture_libs linereader program tenv =
let fake_source_file = SourceFile.from_abs_path (JFrontend.path_of_cached_classname cn) in let fake_source_file = SourceFile.from_abs_path (JFrontend.path_of_cached_classname cn) in
init_global_state fake_source_file ; init_global_state fake_source_file ;
let cfg = JFrontend.compute_class_icfg fake_source_file linereader program tenv node in let cfg = JFrontend.compute_class_icfg fake_source_file linereader program tenv node in
store_icfg fake_source_file cfg ; JFrontend.cache_classname cn store_icfg tenv fake_source_file cfg ;
JFrontend.cache_classname cn
in in
JBasics.ClassMap.iter (capture_class tenv) (JClasspath.get_classmap program) JBasics.ClassMap.iter (capture_class tenv) (JClasspath.get_classmap program)

Loading…
Cancel
Save