From 86aae0b8ed2c24da24497430155bd44d9ebceb83 Mon Sep 17 00:00:00 2001 From: Radu Grigore Date: Wed, 24 Apr 2019 06:39:31 -0700 Subject: [PATCH] [topl] Synthesize trivial procedures. Summary: TOPL properties are essentially automata, which will be modeled as a set of procedures. The code-to-analyze makes calls into these procedures, thereby driving the automaton. In this commit, these calls do not do anything. The point is to prepare the hook-up mechanism. Reviewed By: jvillard Differential Revision: D14819650 fbshipit-source-id: d95ecdb3d --- infer/src/IR/Instrs.ml | 9 +++ infer/src/IR/Instrs.mli | 6 ++ infer/src/IR/Procdesc.ml | 26 +++++- infer/src/IR/Procdesc.mli | 4 + infer/src/IR/Sil.mli | 2 +- infer/src/IR/Typ.ml | 19 +++-- infer/src/IR/Typ.mli | 1 + infer/src/backend/exe_env.ml | 2 +- infer/src/backend/ondemand.ml | 16 ++-- infer/src/backend/printer.ml | 5 +- infer/src/biabduction/SymExec.ml | 4 +- infer/src/biabduction/interproc.ml | 2 +- infer/src/istd/IList.ml | 2 + infer/src/istd/IList.mli | 4 + infer/src/topl/Topl.ml | 125 +++++++++++++++++++++++++++++ infer/src/topl/Topl.mli | 14 +++- 16 files changed, 216 insertions(+), 25 deletions(-) diff --git a/infer/src/IR/Instrs.ml b/infer/src/IR/Instrs.ml index 886a6b025..5b37fa4e5 100644 --- a/infer/src/IR/Instrs.ml +++ b/infer/src/IR/Instrs.ml @@ -91,6 +91,15 @@ let map_changed = if phys_equal instrs instrs' then t else NotReversed instrs' +let concat_map_changed ~equal (NotReversed instrs as t) ~f = + let instrs' = Array.concat_map ~f instrs in + if + Int.equal (Array.length instrs) (Array.length instrs') + && Array.for_all2_exn ~f:equal instrs instrs' + then t + else NotReversed instrs' + + let reverse_order (NotReversed instrs) = Reversed (RevArray.of_rev_array instrs) (* Functions on both reversed and non-reversed arrays *) diff --git a/infer/src/IR/Instrs.mli b/infer/src/IR/Instrs.mli index 80cd12c8f..a973d819a 100644 --- a/infer/src/IR/Instrs.mli +++ b/infer/src/IR/Instrs.mli @@ -33,6 +33,12 @@ val map_changed : -> f:(Sil.instr -> Sil.instr) -> not_reversed_t +val concat_map_changed : + equal:(Sil.instr -> Sil.instr -> bool) + -> not_reversed_t + -> f:(Sil.instr -> Sil.instr array) + -> not_reversed_t + val reverse_order : not_reversed_t -> reversed t val is_empty : _ t -> bool diff --git a/infer/src/IR/Procdesc.ml b/infer/src/IR/Procdesc.ml index f856acc82..bb0e19d5b 100644 --- a/infer/src/IR/Procdesc.ml +++ b/infer/src/IR/Procdesc.ml @@ -228,6 +228,15 @@ module Node = struct true ) + (** Like [replace_instrs], but 1 instr gets replaced by 0, 1, or more instructions. *) + let replace_instrs_by node ~f = + let instrs' = Instrs.concat_map_changed ~equal:phys_equal node.instrs ~f:(f node) in + if phys_equal instrs' node.instrs then false + else ( + node.instrs <- instrs' ; + true ) + + let pp_stmt fmt = function | AssertionFailure -> F.pp_print_string fmt "Assertion failure" @@ -508,13 +517,22 @@ let find_map_instrs pdesc ~f = find_map_nodes ~f:find_map_node pdesc -let replace_instrs pdesc ~f = - let f updated node = - Node.replace_instrs ~f node || (* do not short-circuit [Node.replace_instrs] *) updated - in +let update_nodes pdesc ~(update : Node.t -> bool) : bool = + let f acc node = update node || acc in + (* do not shortcut call to [update] *) fold_nodes pdesc ~init:false ~f +let replace_instrs pdesc ~f = + let update node = Node.replace_instrs ~f node in + update_nodes pdesc ~update + + +let replace_instrs_by pdesc ~f = + let update node = Node.replace_instrs_by ~f node in + update_nodes pdesc ~update + + (** fold between two nodes or until we reach a branching structure *) let fold_slope_range = let rec aux node visited acc ~f = diff --git a/infer/src/IR/Procdesc.mli b/infer/src/IR/Procdesc.mli index 309490ff7..1b06d0ee0 100644 --- a/infer/src/IR/Procdesc.mli +++ b/infer/src/IR/Procdesc.mli @@ -261,6 +261,10 @@ val replace_instrs : t -> f:(Node.t -> Sil.instr -> Sil.instr) -> bool (** Map and replace the instructions to be executed. Returns true if at least one substitution occured. *) +val replace_instrs_by : t -> f:(Node.t -> Sil.instr -> Sil.instr array) -> bool +(** Like [replace_instrs], but slower, and each instruction may be replaced +by 0, 1, or more instructions. *) + val iter_nodes : (Node.t -> unit) -> t -> unit (** iterate over all the nodes of a procedure *) diff --git a/infer/src/IR/Sil.mli b/infer/src/IR/Sil.mli index 31ff0468e..d0ca41eea 100644 --- a/infer/src/IR/Sil.mli +++ b/infer/src/IR/Sil.mli @@ -48,7 +48,7 @@ type instr = [*lexp1:typ = exp2] where [lexp1] is an expression denoting a heap address [typ] is the root type of [lexp1] - [exp2] is the expression whose value is store. *) + [exp2] is the expression whose value is stored. *) | Prune of Exp.t * Location.t * bool * if_kind (** prune the state based on [exp=1], the boolean indicates whether true branch *) | Call of (Ident.t * Typ.t) * Exp.t * (Exp.t * Typ.t) list * Location.t * CallFlags.t diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml index fda61124c..07df413c9 100644 --- a/infer/src/IR/Typ.ml +++ b/infer/src/IR/Typ.ml @@ -982,6 +982,7 @@ module Procname = struct | Block of Block.t | ObjC_Cpp of ObjC_Cpp.t | WithBlockParameters of t * Block.block_name list + | Topl_method of Java.t [@@deriving compare] let equal = [%compare.equal: t] @@ -1024,6 +1025,8 @@ module Procname = struct match t with | Java j -> Java {j with class_name= new_class} + | Topl_method j -> + Topl_method {j with class_name= new_class} | ObjC_Cpp osig -> ObjC_Cpp {osig with class_name= new_class} | WithBlockParameters (base, blocks) -> @@ -1060,7 +1063,7 @@ module Procname = struct ObjC_Cpp {osig with method_name= new_method_name} | WithBlockParameters (base, blocks) -> WithBlockParameters (objc_cpp_replace_method_name base new_method_name, blocks) - | C _ | Block _ | Linters_dummy_method | Java _ -> + | C _ | Block _ | Linters_dummy_method | Java _ | Topl_method _ -> t @@ -1074,7 +1077,7 @@ module Procname = struct QualifiedCppName.to_qual_string name | Block {name} -> name - | Java j -> + | Java j | Topl_method j -> j.method_name | Linters_dummy_method -> "Linters_dummy_method" @@ -1097,6 +1100,8 @@ module Procname = struct Language.Clang | Java _ -> Language.Java + | Topl_method _ -> + Language.Java (** [is_constructor pname] returns true if [pname] is a constructor *) @@ -1141,7 +1146,7 @@ module Procname = struct (** Very verbose representation of an existing Procname.t *) let rec to_unique_id pn = match pn with - | Java j -> + | Java j | Topl_method j -> Java.to_string j Verbose | C osig -> C.to_string osig Verbose @@ -1158,7 +1163,7 @@ module Procname = struct (** Convert a proc name to a string for the user to see *) let rec to_string p = match p with - | Java j -> + | Java j | Topl_method j -> Java.to_string j Non_verbose | C osig -> C.to_string osig Non_verbose @@ -1175,7 +1180,7 @@ module Procname = struct (** Convenient representation of a procname for external tools (e.g. eclipse plugin) *) let rec to_simplified_string ?(withclass = false) p = match p with - | Java j -> + | Java j | Topl_method j -> Java.to_string ~withclass j Simple | C osig -> C.to_string osig Simple @@ -1213,7 +1218,7 @@ module Procname = struct List.map ~f:(fun par -> Parameter.ClangParameter par) clang_params in match procname with - | Java j -> + | Java j | Topl_method j -> List.map ~f:(fun par -> Parameter.JavaParameter par) (Java.get_parameters j) | C osig -> clang_param_to_param (C.get_parameters osig) @@ -1253,6 +1258,8 @@ module Procname = struct match procname with | Java j -> Java (Java.replace_parameters (params_to_java_params new_parameters) j) + | Topl_method j -> + Topl_method (Java.replace_parameters (params_to_java_params new_parameters) j) | C osig -> C (C.replace_parameters (params_to_clang_params new_parameters) osig) | ObjC_Cpp osig -> diff --git a/infer/src/IR/Typ.mli b/infer/src/IR/Typ.mli index f0b084604..b3b960a1c 100644 --- a/infer/src/IR/Typ.mli +++ b/infer/src/IR/Typ.mli @@ -503,6 +503,7 @@ being the name of the struct, [None] means the parameter is of some other type. | Block of Block.t | ObjC_Cpp of ObjC_Cpp.t | WithBlockParameters of t * Block.block_name list + | Topl_method of Java.t [@@deriving compare] val block_name_of_procname : t -> Block.block_name diff --git a/infer/src/backend/exe_env.ml b/infer/src/backend/exe_env.ml index 8f5f117b7..ce1071d89 100644 --- a/infer/src/backend/exe_env.ml +++ b/infer/src/backend/exe_env.ml @@ -85,7 +85,7 @@ let java_global_tenv = let get_column_value ~value_on_java ~file_data_to_value ~column_name exe_env proc_name = match proc_name with - | Typ.Procname.Java _ -> + | Typ.Procname.Java _ | Typ.Procname.Topl_method _ -> Lazy.force value_on_java | _ -> ( match get_file_data exe_env proc_name with diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index ec3610792..9b4e0346c 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -59,8 +59,13 @@ let should_be_analyzed proc_attributes = (not (is_active proc_name)) (* avoid infinite loops *) && not (already_analyzed proc_name) +let get_proc_attr proc_name = + IList.pick_first_some + [lazy (Topl.get_proc_attr proc_name); lazy (Summary.proc_resolve_attributes proc_name)] + + let procedure_should_be_analyzed proc_name = - match Summary.proc_resolve_attributes proc_name with + match get_proc_attr proc_name with | Some proc_attributes when Config.reactive_capture && not proc_attributes.is_defined -> (* try to capture procedure first *) let defined_proc_attributes = OndemandCapture.try_capture proc_attributes in @@ -270,11 +275,10 @@ let analyze_proc_desc ~caller_pdesc callee_pdesc = (** Find a proc desc for the procedure, perhaps loading it from disk. *) let get_proc_desc callee_pname = - match Procdesc.load callee_pname with - | Some _ as pdesc_opt -> - pdesc_opt - | None -> - Option.map ~f:Summary.get_proc_desc (Summary.get callee_pname) + IList.pick_first_some + [ lazy (Procdesc.load callee_pname) + ; lazy (Topl.get_proc_desc callee_pname) + ; lazy (Option.map ~f:Summary.get_proc_desc (Summary.get callee_pname)) ] (** analyze_proc_name ?caller_pdesc proc_name performs an on-demand analysis of proc_name triggered diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index fea014c5f..aa66f1174 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -210,9 +210,10 @@ let node_finish_session node = let write_proc_html pdesc = if Config.write_html then ( let pname = Procdesc.get_proc_name pdesc in - let source = (Procdesc.get_loc pdesc).file in + let loc = Procdesc.get_loc pdesc in + let source = loc.file in let nodes = List.sort ~compare:Procdesc.Node.compare (Procdesc.get_nodes pdesc) in - let linenum = (Procdesc.Node.get_loc (List.hd_exn nodes)).Location.line in + let linenum = loc.Location.line in let fd, fmt = Io_infer.Html.create source [Typ.Procname.to_filename pname] in F.fprintf fmt "

Procedure %a

@\n" (Io_infer.Html.pp_line_link source diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml index 5fa0bc53d..cedeede57 100644 --- a/infer/src/biabduction/SymExec.ml +++ b/infer/src/biabduction/SymExec.ml @@ -1274,7 +1274,7 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_ : Prop.normal Prop.t) let skip_loop = match ik with | Sil.Ik_while | Sil.Ik_for -> - not (IntLit.iszero i) (* skip wile(1) and for (;1;) *) + not (IntLit.iszero i) (* skip while(1) and for (;1;) *) | Sil.Ik_dowhile -> true (* skip do..while *) | Sil.Ik_land_lor -> @@ -1333,7 +1333,7 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_ : Prop.normal Prop.t) let ret_annots = proc_attrs.ProcAttributes.method_annotation.return in exec_skip_call ~reason resolved_pname ret_annots proc_attrs.ProcAttributes.ret_type ) ) - | Java callee_pname_java -> + | Java callee_pname_java | Topl_method callee_pname_java -> let norm_prop, norm_args = normalize_params tenv current_pname prop_ actual_params in let url_handled_args = call_constructor_url_update_args callee_pname norm_args in let resolved_pnames = diff --git a/infer/src/biabduction/interproc.ml b/infer/src/biabduction/interproc.ml index 3702192b7..882e4af01 100644 --- a/infer/src/biabduction/interproc.ml +++ b/infer/src/biabduction/interproc.ml @@ -1258,7 +1258,7 @@ let analyze_procedure_aux summary exe_env tenv proc_desc : Summary.t = let analyze_procedure {Callbacks.summary; proc_desc; tenv; exe_env} : Summary.t = (* make sure models have been registered *) BuiltinDefn.init () ; - if not (List.is_empty Config.topl_properties) then Topl.init () ; + if Topl.active () then Topl.instrument tenv proc_desc ; try analyze_procedure_aux summary exe_env tenv proc_desc with exn -> IExn.reraise_if exn ~f:(fun () -> not (Exceptions.handle_exception exn)) ; diff --git a/infer/src/istd/IList.ml b/infer/src/istd/IList.ml index 74ebdb1ff..60aa6722b 100644 --- a/infer/src/istd/IList.ml +++ b/infer/src/istd/IList.ml @@ -182,6 +182,8 @@ let remove_first = fun list ~f -> aux list ~f [] +let pick_first_some lazies = List.find_map lazies ~f:Lazy.force + let pp_print_list ~max ?(pp_sep = Format.pp_print_cut) pp_v ppf = let rec aux n = function | [] -> diff --git a/infer/src/istd/IList.mli b/infer/src/istd/IList.mli index 61d519ac1..d740b2b20 100644 --- a/infer/src/istd/IList.mli +++ b/infer/src/istd/IList.mli @@ -46,6 +46,10 @@ val opt_cons : 'a option -> 'a list -> 'a list val remove_first : 'a list -> f:('a -> bool) -> 'a list option +val pick_first_some : 'a option lazy_t list -> 'a option +(** [pick_first_some xs] forces the computation of each element of [xs] and returns the first +that matches (Some _); or, if no such element exists, it returns None. *) + val pp_print_list : max:int -> ?pp_sep:(Format.formatter -> unit -> unit) diff --git a/infer/src/topl/Topl.ml b/infer/src/topl/Topl.ml index aaf393b00..31d957b9e 100644 --- a/infer/src/topl/Topl.ml +++ b/infer/src/topl/Topl.ml @@ -29,3 +29,128 @@ let init () = if not !initialized then ( properties := List.concat_map ~f:parse Config.topl_properties ; initialized := true ) + + +let active () = + init () ; + not (List.is_empty !properties) + + +let cfg = Cfg.create () + +let sourcefile = SourceFile.create "SynthesizedToplProperty.java" + +let sourcefile_location = Location.none sourcefile + +(** The procedure description and its nodes will have location [sourcefile_location]. *) +let empty_proc_desc proc_name = + let attr = + {(ProcAttributes.default sourcefile proc_name) with is_defined= true; loc= sourcefile_location} + in + let proc_desc = Cfg.create_proc_desc cfg attr in + let start_node = + Procdesc.create_node proc_desc sourcefile_location Procdesc.Node.Start_node [] + in + let exit_node = Procdesc.create_node proc_desc sourcefile_location Procdesc.Node.Exit_node [] in + Procdesc.node_set_succs_exn proc_desc start_node [exit_node] [exit_node] ; + Procdesc.set_start_node proc_desc start_node ; + Procdesc.set_exit_node proc_desc exit_node ; + proc_desc + + +let get_proc_desc = function + | Typ.Procname.Topl_method _ as proc_name -> + init () ; + (* TODO: generate code *) + Some (empty_proc_desc proc_name) + | _ -> + None + + +let get_proc_attr proc_name = + (* TODO: optimize -- don't generate body just to get attributes *) + Option.map ~f:Procdesc.get_attributes (get_proc_desc proc_name) + + +(** TODO *) +let get_transitions_count () = 1 + +(** TODO: For now, just makes sure that *some* synthetic method gets called, so that the hookup +mechanism gets tested. Later, it will need to compile TOPL properties into one automaton, number +its transitions, and use that information to implement this function. *) +let get_active_transitions _e_fun _arg_ts = + let result = [|true|] in + if not (Int.equal (Array.length result) (get_transitions_count ())) then + L.(die InternalError) "get_active_transitions should compute one bool for each transition" ; + result + + +let topl_class_exp = + let class_name = Mangled.from_string "topl.Property" in + let var_name = Pvar.mk_global class_name in + Exp.Lvar var_name + + +let topl_class_name : Typ.Name.t = Typ.Name.Java.from_string "topl.Property" + +let topl_class_typ = Typ.mk (Tstruct topl_class_name) + +let transition_field_name i = Typ.Fieldname.Java.from_string (Printf.sprintf "transition%d" i) + +let transition_var i = Exp.Lfield (topl_class_exp, transition_field_name i, topl_class_typ) + +let set_transitions loc active_transitions = + let store i b = + let value = if b then Exp.one else Exp.zero in + Sil.Store (transition_var i, topl_class_typ, value, loc) + in + Array.mapi ~f:store active_transitions + + +(** TODO *) +let call_save_args _loc _ret_id _ret_typ _arg_ts = [||] + +let call_execute loc = + let ret_id = Ident.create_fresh Ident.knormal in + let ret_typ = Typ.mk Tvoid in + let ret_typ_name = Some (Typ.Name.Java.Split.make JConfig.void) in + let e_fun = + Exp.Const + (Const.Cfun + (Typ.Procname.Topl_method + (Typ.Procname.Java.make topl_class_name ret_typ_name "execute" [] + Typ.Procname.Java.Static))) + in + [|Sil.Call ((ret_id, ret_typ), e_fun, [], loc, CallFlags.default)|] + + +let instrument_instruction = function + | Sil.Call ((ret_id, ret_typ), e_fun, arg_ts, loc, _call_flags) as i -> + let active_transitions = get_active_transitions e_fun arg_ts in + if not (Array.exists ~f:(fun x -> x) active_transitions) then [|i|] + else + let i1s = set_transitions loc active_transitions in + let i2s = call_save_args loc ret_id ret_typ arg_ts in + let i3s = call_execute loc in + Array.concat [[|i|]; i1s; i2s; i3s] + | i -> + [|i|] + + +(* PRE: Calling [Tenv.mk_struct tenv ] twice is a no-op. *) +let add_types tenv = + let transition_field i = (transition_field_name i, Typ.mk (Tint IBool), []) in + let rec transitions n = + if Int.equal n 0 then [] else transition_field (n - 1) :: transitions (n - 1) + in + let statics = transitions (get_transitions_count ()) in + let _topl_class = Tenv.mk_struct tenv topl_class_name ~statics in + () + + +let instrument tenv procdesc = + init () ; + add_types tenv ; + let f _node = instrument_instruction in + let _updated = Procdesc.replace_instrs_by procdesc ~f in + () diff --git a/infer/src/topl/Topl.mli b/infer/src/topl/Topl.mli index 324a04f88..4ccf7b0c0 100644 --- a/infer/src/topl/Topl.mli +++ b/infer/src/topl/Topl.mli @@ -7,5 +7,15 @@ open! IStd -val init : unit -> unit -(** Parse properties, mentioned by [Config.topl_properties]. Does this only once. *) +val active : unit -> bool +(** Returns whether the TOPL analysis is active. *) + +val get_proc_attr : Typ.Procname.t -> ProcAttributes.t option +(** [get_proc_attr proc_name] returns the attributes of [get_proc_desc proc_name] *) + +val get_proc_desc : Typ.Procname.t -> Procdesc.t option +(** Returns a synthesized Procdesc.t, when it corresponds to instrumentation for a TOPL property. *) + +val instrument : Tenv.t -> Procdesc.t -> unit +(** Inserts calls to the TOPL automaton. Mutates the arguments: it is the caller's responsibility +to instrument procedures at most once. *)