[Scope] Use the new Eva API

src/plugins/scope/datascope.ml

@@ -80,53 +80,49 @@ module InitSid = struct
     Format.fprintf fmt "Lmap = %a@\n" LM.pretty lmap
 end
 
-let get_lval_zones ~for_writing stmt lval =
-  let state = Db.Value.get_stmt_state stmt in
-  let dpds, zone, exact =
-    !Db.Value.lval_to_zone_with_deps_state
-      state ~deps:(Some Locations.Zone.bottom) ~for_writing lval
-  in
-  dpds, exact, zone
+let get_writes stmt lval =
+  Eva.Results.(
+    before stmt |> eval_address lval |> as_zone ~access:Write |>
+    default Locations.Zone.bottom)
+
+let get_reads stmt lval =
+  Eva.Results.(before stmt |> lval_deps lval)
 
 (** Add to [stmt] to [lmap] for all the locations modified by the statement.
  * Something to do only for calls and assignments.
  * *)
 let register_modified_zones lmap stmt =
   let register lmap zone = InitSid.add_zone lmap zone stmt in
-  let aux_out kf out =
+  let aux_out out kf =
     let inout= !Db.Operational_inputs.get_internal_precise ~stmt kf in
     Locations.Zone.join out inout.Inout_type.over_outputs
   in
   match stmt.skind with
   | Instr (Set (lval, _, _)) ->
-    let _dpds, _, zone =
-      get_lval_zones ~for_writing:true  stmt lval
-    in
+    let zone = get_writes stmt lval in
     register lmap zone
   | Instr (Local_init(v, i, _)) ->
-    let _, _, zone = get_lval_zones ~for_writing:true stmt (Cil.var v) in
+    let zone = get_writes stmt (Cil.var v) in
     let lmap_init = register lmap zone in
     (match i with
      | AssignInit _ -> lmap_init
      | ConsInit(f,_,_) ->
        let kf = Globals.Functions.get f in
-       let out = aux_out kf Locations.Zone.bottom in
+       let out = aux_out Locations.Zone.bottom kf in
        register lmap_init out)
   | Instr (Call (dst,funcexp,_args,_)) ->
     begin
       let lmap = match dst with
         | None -> lmap
         | Some lval ->
-          let _dpds, _, zone =
-            get_lval_zones ~for_writing:true stmt lval
-          in
+          let zone = get_writes stmt lval in
           register lmap zone
       in
-      let _, kfs =
-        !Db.Value.expr_to_kernel_function ~deps:None (Kstmt stmt) funcexp
+      let kfs =
+        Eva.Results.(before stmt |> eval_callee funcexp |> default [])
       in
       let out =
-        Kernel_function.Hptset.fold aux_out kfs Locations.Zone.bottom
+        List.fold_left aux_out Locations.Zone.bottom kfs
       in
       register lmap out
     end
@@ -141,7 +137,7 @@ let compute kf =
   let f = Kernel_function.get_definition kf in
   let do_stmt lmap s =
     Cil.CurrentLoc.set (Cil_datatype.Stmt.loc s);
-    if Db.Value.is_reachable_stmt s
+    if Eva.Results.is_reachable s
     then register_modified_zones lmap s
     else lmap
   in
@@ -361,7 +357,11 @@ let compute_escaping_zones s1 s2 =
   let bases = List.fold_left filter Base.Hptset.empty locals in
   if Base.Hptset.is_empty bases
   then Locations.Zone.bottom
-  else gather_escaping_zones bases (Db.Value.get_stmt_state s1)
+  else
+    match Eva.Results.(before s1 |> as_cvalue_model) with
+    | Ok state -> gather_escaping_zones bases state
+    | Error Bottom -> Locations.Zone.bottom
+    | Error _ -> Locations.Zone.top
 
 (* type pair_stmts = stmt * stmt *)
 module PairStmts =
@@ -392,7 +392,7 @@ module ModifEdge =
   Cil_state_builder.Kernel_function_hashtbl(HashPairStmtsZone)
     (struct
       let name = "Scope.Datatscope.ModifsEdge"
-      let dependencies = [Db.Value.self]
+      let dependencies = [Eva.Analysis.self]
       let size = 16
     end)
 
@@ -410,9 +410,7 @@ let is_modified_by_edge kf z s1 s2 =
  * @raise Kernel_function.No_Definition if [kf] has no definition
 *)
 let get_data_scope_at_stmt kf stmt lval =
-  let dpds, _, zone = get_lval_zones ~for_writing:false stmt lval in
-  (* TODO : is there something to do with 'exact' ? *)
-  let zone = Locations.Zone.join dpds zone in
+  let zone = get_reads stmt lval in
   let allstmts, info = compute kf in
   let modif_stmts = InitSid.find info zone in
   let modifs_edge = is_modified_by_edge kf zone in
@@ -594,7 +592,7 @@ class check_annot_visitor = object(self)
 
   method! vglob_aux g = match g with
     | GFun (fdec, _loc) when
-        !Db.Value.is_called (Option.get self#current_kf) &&
+        Eva.Results.is_called (Option.get self#current_kf) &&
         not (!Db.Value.no_results fdec)
       ->
       Cil.DoChildren

src/plugins/scope/datascope.mli

@@ -37,9 +37,3 @@ val rm_asserts : unit -> unit
 
 (** for internal use *)
 module R: Plugin.General_services
-
-val get_lval_zones:
-  for_writing:bool ->
-  Cil_types.stmt ->
-  Cil_types.lval ->
-  Locations.Zone.t * bool * Locations.Zone.t

src/plugins/scope/defs.ml

@@ -62,10 +62,8 @@ let rec add_callee_nodes z acc nodes =
       (fun node acc2 ->
          match !Db.Pdg.node_key node with
          | PdgIndex.Key.SigCallKey (cid, PdgIndex.Signature.Out out_key) ->
-           let callees =
-             Db.Value.call_to_kernel_function (PdgIndex.Key.call_from_id cid)
-           in
-           Kernel_function.Hptset.fold (fun kf (new_nodes, acc) ->
+           let callees = Eva.Results.callee (PdgIndex.Key.call_from_id cid) in
+           List.fold_left (fun (new_nodes, acc) kf ->
                let callee_pdg = !Db.Pdg.get kf in
                let outputs = match out_key with
                  | PdgIndex.Signature.OutLoc out ->
@@ -78,8 +76,8 @@ let rec add_callee_nodes z acc nodes =
                in
                let outputs = List.map fst outputs in
                add_list_to_set outputs new_nodes, add_list_to_set outputs acc)
-             callees
              acc2
+             callees
          | _ -> acc2)
       nodes
       (NSet.empty, acc)
@@ -134,7 +132,7 @@ let rec add_caller_nodes z kf acc (undef, nodes) =
     let acc_undef, caller_nodes =
       List.fold_left (add_one_call_nodes pdg) (None, NSet.empty) stmts
     in add_caller_nodes z kf (NSet.union caller_nodes acc) (acc_undef, caller_nodes)
-  in List.fold_left add_one_caller_nodes acc (!Db.Value.callers kf)
+  in List.fold_left add_one_caller_nodes acc (Eva.Results.callsites kf)
 
 let compute_aux kf stmt zone =
   debug1 "[Defs.compute] for %a at sid:%d in '%a'@."
@@ -168,9 +166,10 @@ let compute kf stmt lval =
     let defs = NSet.fold add_node nodes Stmt.Hptset.empty in
     (defs, undef)
   in
-  !Db.Value.compute ();
-  let zone = !Db.Value.lval_to_zone (Kstmt stmt) lval in
-  Option.map extract (compute_aux kf stmt zone)
+  Eva.Analysis.compute ();
+  let zone = Eva.Results.(before stmt |> eval_address lval |> as_zone) in
+  Option.bind (Result.to_option zone) (compute_aux kf stmt) |>
+  Option.map extract
 
 (* Variation of the function above. For each PDG node that has been found,
    we find whether it directly modifies [zone] through an affectation
@@ -219,8 +218,11 @@ let compute_with_def_type_zone kf stmt zone =
   Option.map extract (compute_aux kf stmt zone)
 
 let compute_with_def_type kf stmt lval =
-  !Db.Value.compute ();
-  let zone = !Db.Value.lval_to_zone (Kstmt stmt) lval in
+  Eva.Analysis.compute ();
+  let zone =
+    Eva.Results.(before stmt |> eval_address lval |> as_zone) |>
+    Result.value ~default:Locations.Zone.bottom
+  in
   compute_with_def_type_zone kf stmt zone
 
 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)

src/plugins/scope/dpds_gui.ml

@@ -114,7 +114,7 @@ struct include State_builder.Ref
     (Stmt.Hptset)
     (struct
       let name = Info.name
-      let dependencies = [ Db.Value.self ]
+      let dependencies = [ Eva.Analysis.self ]
       let default () = Stmt.Hptset.empty
     end)
 
@@ -137,7 +137,7 @@ struct
       (Stmt.Map.Make(Datatype.String.Set))
       (struct
         let name = Info.name
-        let dependencies = [ Db.Value.self ]
+        let dependencies = [ Eva.Analysis.self ]
         let default () = Stmt.Map.empty
       end)
 
@@ -222,7 +222,7 @@ module Pscope (* : (DpdCmdSig with type t_in = code_annotation) *) = struct
       (Code_annotation)
       (struct
         let name = "Dpds_gui.Highlighter.Pscope_warn"
-        let dependencies = [ Db.Value.self ]
+        let dependencies = [ Eva.Analysis.self ]
       end)
 
   let clear () = Pscope.clear(); Pscope_warn.clear()
@@ -323,7 +323,7 @@ module Zones : (DpdCmdSig with type t_in = lval)  = struct
          (Stmt.Hptset))
       (struct
         let name = "Dpds_gui.Highlighter.ZonesState"
-        let dependencies = [ Db.Value.self ]
+        let dependencies = [ Eva.Analysis.self ]
       end)
     let set s =
       set s;
@@ -392,7 +392,7 @@ module DpdsState =
     (Stmt)
     (struct
       let name = "Dpds_gui.Highlighter.DpdsState"
-      let dependencies = [ Db.Value.self ]
+      let dependencies = [ Eva.Analysis.self ]
     end)
 
 let reset () =
@@ -469,7 +469,7 @@ let highlighter (buffer:Design.reactive_buffer) localizable ~start ~stop =
   with Not_found -> ()
 
 let check_value (main_ui:Design.main_window_extension_points) =
-  if Db.Value.is_computed () then true
+  if Eva.Analysis.is_computed () then true
   else
     let answer = GToolbox.question_box
         ~title:("Eva Needed")
@@ -478,7 +478,7 @@ let check_value (main_ui:Design.main_window_extension_points) =
          ^"Do you want to run Eva with its current settings now?")
     in
     if answer = 1 then
-      match main_ui#full_protect ~cancelable:true !Db.Value.compute with
+      match main_ui#full_protect ~cancelable:true Eva.Analysis.compute with
       | Some _ ->
         main_ui#redisplay (); (* New alarms *)
         true

src/plugins/scope/zones.ml

@@ -64,6 +64,14 @@ let compute_new_data old_zone l_zone l_dpds exact r_dpds =
     (true, zone)
   else (false, old_zone)
 
+let get_lval_zones ~for_writing stmt lval =
+  let state = Db.Value.get_stmt_state stmt in
+  let dpds, zone, exact =
+    !Db.Value.lval_to_zone_with_deps_state
+      state ~deps:(Some Locations.Zone.bottom) ~for_writing lval
+  in
+  dpds, exact, zone
+
 (* the call result can be processed like a normal assignment *)
 let process_call_res data stmt lvaloption froms =
   let data = match lvaloption with
@@ -73,7 +81,7 @@ let process_call_res data stmt lvaloption froms =
       let r_dpds = Function_Froms.Memory.collapse_return ret_dpds in
       let r_dpds = Function_Froms.Deps.to_zone r_dpds in
       let l_dpds, exact, l_zone =
-        Datascope.get_lval_zones ~for_writing:true  stmt lval in
+        get_lval_zones ~for_writing:true  stmt lval in
       compute_new_data data l_zone l_dpds exact r_dpds
   in data
 
@@ -144,20 +152,21 @@ let process_one_call data stmt lvaloption froms =
   used, data
 
 let process_call data_after stmt lvaloption funcexp args _loc =
-  let funcexp_dpds, called_functions =
-    !Db.Value.expr_to_kernel_function
-      (Kstmt stmt) ~deps:(Some Data.bottom) funcexp
+  let funcexp_dpds = Eva.Results.(before stmt |> expr_deps funcexp)
+  and called_functions =
+    Eva.Results.(before stmt |> eval_callee funcexp) |>
+    Result.value ~default:[]
   in
   let used, data =
     try
       let froms = !Db.From.Callwise.find (Kstmt stmt) in
       process_one_call data_after stmt lvaloption froms
     with Not_found -> (* don't have callwise (-calldeps option) *)
-      let do_call kf acc =
+      let do_call acc kf =
         (* notice that we use the same old data for each possible call *)
         (process_one_call data_after stmt lvaloption (!Db.From.get kf))::acc
       in
-      let l = Kernel_function.Hptset.fold do_call called_functions [] in
+      let l = List.fold_left do_call [] called_functions in
       (* in l, we have one result for each possible function called *)
       List.fold_left
         (fun (acc_u,acc_d) (u,d) -> (acc_u || u), Data.merge acc_d d)
@@ -167,10 +176,9 @@ let process_call data_after stmt lvaloption funcexp args _loc =
   if used then
     let data =
       (* no problem of order because parameters are disjoint for sure *)
-      Kernel_function.Hptset.fold
-        (fun kf data -> process_call_args data kf stmt args)
-        called_functions
-        data
+      List.fold_left
+        (fun data kf -> process_call_args data kf stmt args)
+        data called_functions
     in
     let data =  Data.merge funcexp_dpds data in
     used, data
@@ -213,7 +221,7 @@ module Computer (Param:sig val states : Ctx.t end) = struct
 
   let do_assign stmt lval exp data =
     let l_dpds, exact, l_zone =
-      Datascope.get_lval_zones ~for_writing:true stmt lval in
+      get_lval_zones ~for_writing:true stmt lval in
     let r_dpds = Data.exp_zone stmt exp in
     let used, data = compute_new_data data l_zone l_dpds exact r_dpds in
     let _ = if used then add_used_stmt stmt in
@@ -299,7 +307,7 @@ let compute_ctrl_info pdg ctrl_part used_stmts =
 let compute kf stmt lval =
   let f = Kernel_function.get_definition kf in
   let dpds, _exact, zone =
-    Datascope.get_lval_zones ~for_writing:false stmt lval in
+    get_lval_zones ~for_writing:false stmt lval in
   let zone = Data.merge dpds zone in
   debug1 "[zones] build for %a before %d in %a@\n"
     Data.pretty zone stmt.sid Kernel_function.pretty kf;