diff --git a/src/plugins/pdg/annot.ml b/src/plugins/pdg/annot.ml index 7bfa2eb708f0c78b5f86acaab1328a9f02527c47..d76dc95c38da8546bce3569b83ddcadbb3fbfa54 100644 --- a/src/plugins/pdg/annot.ml +++ b/src/plugins/pdg/annot.ml @@ -106,7 +106,7 @@ let find_code_annot_nodes pdg stmt annot = Pdg_parameters.debug "[pdg:annotation] CodeAnnot-%d stmt %d : %a @." annot.annot_id stmt.sid Printer.pp_code_annotation annot; - if Db.Value.is_reachable_stmt stmt then + if Eva.Results.is_reachable stmt then begin let kf = PdgTypes.Pdg.get_kf pdg in let (data_info, decl_label_info), pragmas = diff --git a/src/plugins/pdg/build.ml b/src/plugins/pdg/build.ml index 6b5be2c31fa08deedea5532993759c686f387bb7..4c2bd6202f7d9bf8b4e91887c318447f15b091c5 100644 --- a/src/plugins/pdg/build.ml +++ b/src/plugins/pdg/build.ml @@ -465,12 +465,20 @@ let create_fun_output_node pdg state dpds = | Some state -> add_dpds pdg new_node Dpd.Data state dpds | None -> (* return is unreachable *) () +let find_return_lval kf = + let stmt = Kernel_function.find_return kf in + match stmt with + | { skind = Return (Some {enode = Lval lval}, _)} -> stmt, lval + | _ -> assert false + (** add a node corresponding to the returned value. *) let add_retres pdg state ret_stmt retres_loc_dpds retres_decls = let key_return = Key.stmt_key ret_stmt in let return_node = add_elem pdg key_return in - let retres_loc = Db.Value.find_return_loc pdg.fct in - let retres = Locations.(enumerate_valid_bits Read retres_loc) in + let retres = + let stmt, lval = find_return_lval pdg.fct in + Eva.Results.(before stmt |> eval_address ~for_writing:false lval |> as_zone) + in add_dpds pdg return_node Dpd.Data state retres_loc_dpds; add_decl_dpds pdg return_node Dpd.Data retres_decls; let new_state = Pdg_state.add_loc_node state ~exact:true retres return_node in @@ -600,11 +608,11 @@ let finalize_pdg pdg from_opt = = location + exact + dependencies + declarations *) let get_lval_infos lval stmt = let decl = Cil.extract_varinfos_from_lval lval in - let state = Db.Value.get_stmt_state stmt in - let dpds, z_loc, exact = - !Db.Value.lval_to_zone_with_deps_state - state ~deps:(Some Locations.Zone.bottom) ~for_writing:true lval - in + let request = Eva.Results.before stmt in + let address = Eva.Results.eval_address ~for_writing:true lval request in + let z_loc = Eva.Results.as_zone address in + let exact = Eva.Results.is_singleton address in + let dpds = Eva.Results.address_deps lval request in (z_loc, exact, dpds, decl) (** process assignment {v lval = exp; v} @@ -700,15 +708,17 @@ let process_call pdg state stmt lvaloption funcexp argl _loc = ignore (add_elem pdg (Key.call_ctrl_key stmt)); let arg_nodes = process_args pdg state_before_call stmt argl in let state_with_args = state in - let funcexp_dpds, called_functions = - !Db.Value.expr_to_kernel_function - (Kstmt stmt) ~deps:(Some Locations.Zone.bottom) funcexp + let called_functions = Eva.Results.callee stmt in + let funcexp_dpds = + match funcexp.enode with + | Lval lval -> Eva.Results.(before stmt |> address_deps lval) + | _ -> assert false in let mixed_froms = try let froms = !Db.From.Callwise.find (Kstmt stmt) in Some froms with Not_found -> None (* don't have callwise analysis (-calldeps option) *) in - let process_simple_call called_kf acc = + let process_simple_call acc called_kf = let state_with_inputs = process_call_params pdg state_with_args stmt called_kf arg_nodes in @@ -724,7 +734,7 @@ let process_call pdg state stmt lvaloption funcexp argl _loc = in r :: acc in let state_for_each_call = - Kernel_function.Hptset.fold process_simple_call called_functions [] + List.fold_left process_simple_call [] called_functions in let new_state = match state_for_each_call with @@ -773,7 +783,7 @@ let process_jump_stmt pdg ctrl_dpds_infos jump = let controlled_stmts = CtrlDpds.get_jump_controlled_stmts ctrl_dpds_infos jump in - let real = Db.Value.is_reachable_stmt jump in + let real = Eva.Results.is_reachable jump in if not real then debug "[process_jump_stmt] stmt %d is not a real jump@." jump.sid; process_jump pdg jump (real, controlled_stmts) @@ -791,7 +801,7 @@ let process_loop_stmt pdg ctrl_dpds_infos loop = let controlled_stmts = CtrlDpds.get_loop_controlled_stmts ctrl_dpds_infos loop in - let real_loop = List.exists (Db.Value.is_reachable_stmt) back_edges in + let real_loop = List.exists Eva.Results.is_reachable back_edges in if not real_loop then debug "[process_loop_stmt] stmt %d is not a real loop@." loop.sid; process_jump pdg loop (real_loop, controlled_stmts) @@ -812,11 +822,11 @@ let process_return _current_function pdg state stmt ret_exp = add_retres pdg state stmt loc_exp decls_exp | None -> let controlled_stmt = Cil_datatype.Stmt.Hptset.empty in - let real = Db.Value.is_reachable_stmt stmt in + let real = Eva.Results.is_reachable stmt in process_jump pdg stmt (real, controlled_stmt); state in - if Db.Value.is_reachable_stmt stmt then + if Eva.Results.is_reachable stmt then Pdg_state.store_last_state pdg.states last_state module Computer @@ -866,7 +876,7 @@ module Computer Db.yield (); pdg_debug "doInstr sid:%d : %a" stmt.sid Printer.pp_instr instr; match instr with - | _ when not (Db.Value.is_reachable_stmt stmt) -> + | _ when not (Eva.Results.is_reachable stmt) -> pdg_debug "stmt sid:%d is unreachable : skip.@." stmt.sid ; Pdg_state.bottom | Local_init (v, AssignInit i, _) -> @@ -977,7 +987,7 @@ let compute_pdg_for_f kf = let ctrl_dpds_infos = ctrl_dpds_infos end) in - if Db.Value.is_reachable_stmt start then + if Eva.Results.is_reachable start then begin let module Compute = Dataflows.Simple_forward(Fenv)(Computer) in Array.iteri (fun ord value -> diff --git a/src/plugins/pdg/marks.ml b/src/plugins/pdg/marks.ml index 628611b95e3219ef821b9c759a298aab848d9fa3..272b5b1ad9fe0928b90ed766e1c06a0345f5afcc 100644 --- a/src/plugins/pdg/marks.ml +++ b/src/plugins/pdg/marks.ml @@ -63,7 +63,7 @@ let translate_in_marks pdg_called in_new_marks let translate pdg rqs call = in_marks_to_caller pdg call (m2m (Some call) pdg) ~rqs in_new_marks in - let build rqs (caller, _) = + let build rqs caller = let pdg_caller = !Db.Pdg.get caller in let caller_rqs = try @@ -77,8 +77,7 @@ let translate_in_marks pdg_called in_new_marks in (pdg_caller, caller_rqs)::rqs in - let res = List.fold_left build other_rqs (!Db.Value.callers kf_called) in - res + List.fold_left build other_rqs (Eva.Results.callers kf_called) let call_out_marks_to_called called_pdg m2m ?(rqs=[]) out_marks = let build rqs (out_key, m) = @@ -98,7 +97,7 @@ let call_out_marks_to_called called_pdg m2m ?(rqs=[]) out_marks = List.fold_left build rqs out_marks let translate_out_mark _pdg m2m other_rqs (call, l) = - let add_list l_out_m called_kf rqs = + let add_list l_out_m rqs called_kf = let called_pdg = !Db.Pdg.get called_kf in let m2m = m2m (Some call) called_pdg in try @@ -111,8 +110,8 @@ let translate_out_mark _pdg m2m other_rqs (call, l) = * *) rqs in - let all_called = Db.Value.call_to_kernel_function call in - Kernel_function.Hptset.fold (add_list l) all_called other_rqs + let all_called = Eva.Results.callee call in + List.fold_left (add_list l) other_rqs all_called (** [add_new_marks_to_rqs pdg new_marks other_rqs] translates [new_marks] * that were computed during intraprocedural propagation into requests, diff --git a/src/plugins/pdg/register.ml b/src/plugins/pdg/register.ml index ff00ddbddf132d7f679ae9f6080ce314e82c7160..4f707e7ffeb43572c405893f74411acb98b2b560 100644 --- a/src/plugins/pdg/register.ml +++ b/src/plugins/pdg/register.ml @@ -123,7 +123,7 @@ let () = Pdg_parameters.BuildAll.set_output_dependencies deps let compute_for_kf kf = let all = Pdg_parameters.BuildAll.get () in - (all && !Db.Value.is_called kf) || + (all && Eva.Results.is_called kf) || Kernel_function.Set.mem kf (Pdg_parameters.BuildFct.get ()) let compute () = diff --git a/src/plugins/pdg/sets.ml b/src/plugins/pdg/sets.ml index 9fff226ac9021220f29429141aad38420c15d95c..89b83596775910a2d19721723910ccdd42e323e1 100644 --- a/src/plugins/pdg/sets.ml +++ b/src/plugins/pdg/sets.ml @@ -215,7 +215,7 @@ let find_call_stmts kf ~caller = match List.filter (fun (f, _) -> Kernel_function.equal f caller) - (!Db.Value.callers kf) + (Eva.Results.callsites kf) with | [] -> [] | [ _, callsites ] -> assert (callsites <> []); callsites diff --git a/tests/pdg/oracle/top_pdg_input.res.oracle b/tests/pdg/oracle/top_pdg_input.res.oracle index 72f904673274a5504962f083902fd9626ec5e46a..b26af8c3d53534959a87ff13679b46921c6bef2d 100644 --- a/tests/pdg/oracle/top_pdg_input.res.oracle +++ b/tests/pdg/oracle/top_pdg_input.res.oracle @@ -285,8 +285,6 @@ Cannot filter: dumping raw memory (including unchanged variables) [pdg] done for function fun_asm [pdg] computing for function main_asm [pdg] done for function main_asm -[pdg] computing for function no_results -[pdg] Top for function no_results [pdg] ====== PDG GRAPH COMPUTED ====== [pdg] PDG for fun_asm {n47}: InCtrl @@ -333,5 +331,3 @@ Cannot filter: dumping raw memory (including unchanged variables) -[--d]-> 61 {n63}: OutRet -[--d]-> 62 -[pdg] PDG for no_results - Top PDG diff --git a/tests/slicing/oracle/min_call.res.oracle b/tests/slicing/oracle/min_call.res.oracle index 858153ee93740c28d7b7379d50f8de6beca11e87..f3607c3ab3b4940722b6795cd9097a58361a414b 100644 --- a/tests/slicing/oracle/min_call.res.oracle +++ b/tests/slicing/oracle/min_call.res.oracle @@ -104,10 +104,10 @@ [slicing] applying all slicing requests... [slicing] applying 1 actions... [slicing] applying actions: 1/1... -[pdg] computing for function f -[pdg] done for function f [pdg] computing for function g [pdg] done for function g +[pdg] computing for function f +[pdg] done for function f Project1 - result1 : [slicing] exporting project to 'Sliced code'... [slicing] applying all slicing requests... @@ -464,14 +464,14 @@ void f_slice_1(void) [slicing] applying all slicing requests... [slicing] applying 0 actions... Slicing project worklist [default] = -[f = (n:26 ,<[acd], [---]>)(n:33 ,<[acd], [---]>)(n:41 ,<[acd], [---]>)][g = (n:60 , +[f = (n:45 ,<[acd], [---]>)(n:52 ,<[acd], [---]>)(n:60 ,<[acd], [---]>)][g = (n:27 , <[acd], [---]>)] Slicing project worklist [default] = -[f_slice_1 = choose_call for call 17][f_slice_1 = choose_call for call 16][f_slice_1 = choose_call for call 15][g = propagate (n:68 , +[f_slice_1 = choose_call for call 17][f_slice_1 = choose_call for call 16][f_slice_1 = choose_call for call 15][g = propagate (n:35 , <[acd], -[---]>)][Appli : calls to f][g = (n:60 ,<[acd], [---]>)] +[---]>)][Appli : calls to f][g = (n:27 ,<[acd], [---]>)] [slicing] applying all slicing requests... [slicing] applying 6 actions...