From 3b0eca1622c0266541fda8d6a68ad0b5e8df8399 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Mon, 7 Feb 2022 16:57:45 +0100
Subject: [PATCH] [Scope] Use the new Eva API
---
src/plugins/scope/datascope.ml | 50 ++++++++++++++++-----------------
src/plugins/scope/datascope.mli | 6 ----
src/plugins/scope/defs.ml | 24 ++++++++--------
src/plugins/scope/dpds_gui.ml | 14 ++++-----
src/plugins/scope/zones.ml | 32 +++++++++++++--------
5 files changed, 64 insertions(+), 62 deletions(-)
diff --git a/src/plugins/scope/datascope.ml b/src/plugins/scope/datascope.ml
index 26d5806673e..3a1617d69c4 100644
--- a/src/plugins/scope/datascope.ml
+++ b/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
diff --git a/src/plugins/scope/datascope.mli b/src/plugins/scope/datascope.mli
index b34a8589757..9b93221fe4f 100644
--- a/src/plugins/scope/datascope.mli
+++ b/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
diff --git a/src/plugins/scope/defs.ml b/src/plugins/scope/defs.ml
index 565500c763b..0aede3dd05e 100644
--- a/src/plugins/scope/defs.ml
+++ b/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
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
diff --git a/src/plugins/scope/dpds_gui.ml b/src/plugins/scope/dpds_gui.ml
index d9d87225b1b..b3798da4e55 100644
--- a/src/plugins/scope/dpds_gui.ml
+++ b/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
diff --git a/src/plugins/scope/zones.ml b/src/plugins/scope/zones.ml
index 9a9e18e7c26..0b1ecae374a 100644
--- a/src/plugins/scope/zones.ml
+++ b/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;
--
GitLab