[pdg] Uses the new Eva API instead of Db.Value.

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 =

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 ->

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,

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 () =

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

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

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...