From e4671bfc915dc1856a160ff0995d27ee5d0fc1a6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 18 Jul 2022 15:12:35 +0200
Subject: [PATCH] [inout] Uses new Eva API instead of Db.Value.
---
src/plugins/inout/cumulative_analysis.mli | 4 +-
src/plugins/inout/derefs.ml | 6 +-
src/plugins/inout/inputs.ml | 77 +++++++-----------
src/plugins/inout/operational_inputs.ml | 95 ++++++++++-------------
src/plugins/inout/outputs.ml | 53 ++++++-------
src/plugins/inout/register.ml | 2 +-
6 files changed, 99 insertions(+), 138 deletions(-)
diff --git a/src/plugins/inout/cumulative_analysis.mli b/src/plugins/inout/cumulative_analysis.mli
index f98bd1b9848..a72397c8aa9 100644
--- a/src/plugins/inout/cumulative_analysis.mli
+++ b/src/plugins/inout/cumulative_analysis.mli
@@ -37,7 +37,7 @@ open Cil_types
val fold_implicit_initializer: typ -> bool
-val specialize_state_on_call: ?stmt:stmt -> kernel_function -> Db.Value.state
+val specialize_state_on_call: ?stmt:stmt -> kernel_function -> Cvalue.Model.t
(** If the given statement is a call to the given function,
enrich the superposed memory state at this statement with
the formal arguments of this function. This is usually more precise
@@ -50,7 +50,7 @@ val specialize_state_on_call: ?stmt:stmt -> kernel_function -> Db.Value.state
class virtual ['a] cumulative_visitor : object
inherit Visitor.frama_c_inplace
- method specialize_state_on_call: kernel_function -> Db.Value.state
+ method specialize_state_on_call: kernel_function -> Cvalue.Model.t
(** If the current statement is a call to the given function,
enrich the superposed memory state at this statement with
the formal arguments of this function. Useful to do an analysis
diff --git a/src/plugins/inout/derefs.ml b/src/plugins/inout/derefs.ml
index f7436ea3a5c..bac26387241 100644
--- a/src/plugins/inout/derefs.ml
+++ b/src/plugins/inout/derefs.ml
@@ -40,10 +40,8 @@ class virtual do_it_ = object(self)
begin match base with
| Var _ -> ()
| Mem e ->
- let state =
- Db.Value.get_state (Kstmt (Option.get self#current_stmt))
- in
- let r = !Db.Value.eval_expr state e in
+ let stmt = Option.get self#current_stmt in
+ let r = Eva.Results.(before stmt |> eval_exp e |> as_cvalue) in
let loc = loc_bytes_to_loc_bits r in
let size = Bit_utils.sizeof_lval lv in
self#join
diff --git a/src/plugins/inout/inputs.ml b/src/plugins/inout/inputs.ml
index 19e2f96f130..c9787b60363 100644
--- a/src/plugins/inout/inputs.ml
+++ b/src/plugins/inout/inputs.ml
@@ -45,55 +45,43 @@ class virtual do_it_ = object(self)
Cil.SkipChildren (* do not visit the additional lvals *)
| _ -> super#vstmt_aux s
+ (* On assignment and addrof, only read the lvalue address. *)
+ method private read_address lv =
+ let request = Eva.Results.before_kinstr self#current_kinstr in
+ let deps = Eva.Results.address_deps lv request in
+ self#join deps
+
method! vlval lv =
- let state = Db.Value.get_state self#current_kinstr in
- let deps, bits_loc, _exact =
- !Db.Value.lval_to_zone_with_deps_state
- state ~deps:(Some Zone.bottom) ~for_writing:false lv
- in
+ let request = Eva.Results.before_kinstr self#current_kinstr in
+ let deps = Eva.Results.lval_deps lv request in
self#join deps;
- self#join bits_loc;
Cil.SkipChildren
- method private do_assign lv =
- let deps,_loc =
- !Db.Value.lval_to_loc_with_deps (* loc ignored *)
- ~deps:Zone.bottom
- self#current_kinstr
- lv
- in
- (* Format.printf "do_assign deps:%a@."
- Zone.pretty deps; *)
+ method private do_arg_calls stmt f args =
+ let deps = Eva.Results.(before stmt |> expr_deps f) in
self#join deps;
-
- method private do_arg_calls f args =
- let state = Db.Value.get_state self#current_kinstr in
- (if Cvalue.Model.is_top state then
- self#join Zone.top
- else
- let deps_callees, callees =
- !Db.Value.expr_to_kernel_function_state
- ~deps:(Some Zone.bottom) state f
- in
- self#join deps_callees;
- Kernel_function.Hptset.iter
- (fun kf -> self#join (self#compute_kf kf)) callees;
- );
- List.iter
- (fun exp -> ignore (visitFramacExpr (self:>frama_c_visitor) exp)) args
+ let () =
+ match Eva.Results.(before stmt |> eval_callee f) with
+ | Ok callees ->
+ List.iter (fun kf -> self#join (self#compute_kf kf)) callees
+ | Error (Top | DisabledDomain) -> self#join Zone.top;
+ | Error Bottom -> ()
+ in
+ List.iter (fun e -> ignore (visitFramacExpr (self:>frama_c_visitor) e)) args;
method! vinst i =
- if Db.Value.is_reachable (Db.Value.get_state self#current_kinstr) then begin
+ let stmt = Option.get self#current_stmt in
+ if Eva.Results.is_reachable stmt then begin
match i with
| Set (lv,exp,_) ->
- self#do_assign lv;
+ self#read_address lv;
ignore (visitFramacExpr (self:>frama_c_visitor) exp);
Cil.SkipChildren
| Local_init(v, AssignInit i,_) ->
let rec aux lv = function
| SingleInit e ->
- self#do_assign lv;
+ self#read_address lv;
ignore (visitFramacExpr (self:>frama_c_visitor) e)
| CompoundInit (ct,initl) ->
(* No need to consider implicit zero-initializers, for which
@@ -109,15 +97,15 @@ class virtual do_it_ = object(self)
Cil.SkipChildren
| Call (lv_opt,exp,args,_) ->
- Option.iter self#do_assign lv_opt;
- self#do_arg_calls exp args;
+ Option.iter self#read_address lv_opt;
+ self#do_arg_calls stmt exp args;
Cil.SkipChildren
| Local_init(v, ConsInit(f, args, Plain_func), _) ->
- self#do_assign (Cil.var v);
- self#do_arg_calls (Cil.evar f) args;
+ self#read_address (Cil.var v);
+ self#do_arg_calls stmt (Cil.evar f) args;
Cil.SkipChildren
| Local_init(v, ConsInit(f, args, Constructor), _) ->
- self#do_arg_calls (Cil.evar f) (Cil.mkAddrOfVi v :: args);
+ self#do_arg_calls stmt (Cil.evar f) (Cil.mkAddrOfVi v :: args);
Cil.SkipChildren
| Skip _ | Asm _ | Code_annot _ -> Cil.DoChildren
end
@@ -126,12 +114,7 @@ class virtual do_it_ = object(self)
method! vexpr exp =
match exp.enode with
| AddrOf lv | StartOf lv ->
- let deps,_loc =
- !Db.Value.lval_to_loc_with_deps (* loc ignored *)
- ~deps:Zone.bottom
- self#current_kinstr lv
- in
- self#join deps;
+ self#read_address lv;
Cil.SkipChildren
| SizeOfE _ | AlignOfE _ | SizeOf _ | AlignOf _ ->
(* we're not evaluating an expression here: there's no input. *)
@@ -140,9 +123,9 @@ class virtual do_it_ = object(self)
method compute_funspec kf =
let state = self#specialize_state_on_call kf in
- let behaviors = !Db.Value.valid_behaviors kf state in
+ let behaviors = Eva.Logic_inout.valid_behaviors kf state in
let assigns = Ast_info.merge_assigns behaviors in
- !Db.Value.assigns_inputs_to_zone state assigns
+ Eva.Logic_inout.assigns_inputs_to_zone state assigns
method clean_kf_result (_ : kernel_function) (r: Locations.Zone.t) = r
end
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index bbb589d3f23..4e5041fc2fd 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -191,7 +191,7 @@ let eval_assigns kf state assigns =
}
let compute_using_prototype_state state kf =
- let behaviors = !Db.Value.valid_behaviors kf state in
+ let behaviors = Eva.Logic_inout.valid_behaviors kf state in
let assigns = Ast_info.merge_assigns behaviors in
eval_assigns kf state assigns
@@ -230,8 +230,9 @@ module CallwiseResults =
module Computer(Fenv:Dataflows.FUNCTION_ENV)(X:sig
val _version: string (* Debug: Callwise or functionwise *)
val _kf: kernel_function (* Debug: Function being analyzed *)
- val kf_pre_state: Db.Value.state (* Memory pre-state of the function. *)
- val stmt_state: stmt -> Db.Value.state (* Memory state at the given stmt *)
+ val kf_pre_state: Cvalue.Model.t (* Memory pre-state of the function. *)
+ val stmt_state: stmt -> Cvalue.Model.t (* Memory state at the given stmt *)
+ val stmt_request: stmt -> Eva.Results.request (* Request at the given stmt *)
val at_call: stmt -> kernel_function -> Inout_type.t (* Results of the
analysis for the given call. Must not contain locals or formals *)
end) = struct
@@ -289,8 +290,8 @@ module Computer(Fenv:Dataflows.FUNCTION_ENV)(X:sig
(* Transfer function on expression. *)
let transfer_exp s exp data =
- let state = X.stmt_state s in
- let inputs = !Db.From.find_deps_no_transitivity_state state exp in
+ let request = X.stmt_request s in
+ let inputs = Eva.Results.expr_deps exp request in
let new_inputs = Zone.diff inputs data.under_outputs_d in
store_non_terminating_inputs new_inputs;
{data with over_inputs_d = Zone.join data.over_inputs_d new_inputs}
@@ -298,12 +299,13 @@ module Computer(Fenv:Dataflows.FUNCTION_ENV)(X:sig
(* Initialized const variables should be included as outputs of the function,
so [for_writing] must be false for local initializations. It should be
true for all other instructions. *)
- let add_out ~for_writing state lv deps data =
- let deps, new_outs, exact =
- !Db.Value.lval_to_zone_with_deps_state state
- ~deps:(Some deps) ~for_writing lv
- in
+ let add_out ~for_writing request lv deps data =
+ let lv_address = Eva.Results.eval_address ~for_writing lv request in
+ let new_outs = Eva.Results.as_zone lv_address in
+ let exact = Eva.Results.is_singleton lv_address in
store_non_terminating_outputs new_outs;
+ let lv_deps = Eva.Results.address_deps lv request in
+ let deps = Zone.join lv_deps deps in
let new_inputs = Zone.diff deps data.under_outputs_d in
store_non_terminating_inputs new_inputs;
let new_sure_outs =
@@ -318,34 +320,21 @@ module Computer(Fenv:Dataflows.FUNCTION_ENV)(X:sig
over_outputs_d = Zone.join data.over_outputs_d new_outs }
let transfer_call ~for_writing s dest f args _loc data =
- let state = X.stmt_state s in
- let f_inputs, called =
- !Db.Value.expr_to_kernel_function_state
- ~deps:(Some Zone.bottom)
- state
- f
- in
- let acc_f_arg_inputs =
- (* add the inputs of [argl] to the inputs of the
- function expression *)
- List.fold_right
- (fun arg inputs ->
- let arg_inputs = !Db.From.find_deps_no_transitivity_state
- state arg
- in Zone.join inputs arg_inputs)
- args
- f_inputs
- in
+ let request = X.stmt_request s in
+ (* Join the inputs of [args] and of the function expression. *)
+ let eval_deps acc e = Zone.join acc (Eva.Results.expr_deps e request) in
+ let f_args_inputs = List.fold_left eval_deps Zone.bottom (f :: args) in
let data =
catenate
data
- { over_inputs_d = acc_f_arg_inputs ;
+ { over_inputs_d = f_args_inputs ;
under_outputs_d = Zone.bottom;
over_outputs_d = Zone.bottom; }
in
+ let called = Eva.Results.(eval_callee f request |> default []) in
let for_functions =
- Kernel_function.Hptset.fold
- (fun kf acc ->
+ List.fold_left
+ (fun acc kf ->
let res = X.at_call s kf in
store_non_terminating_subcall data.over_outputs_d res;
let for_function = {
@@ -354,15 +343,15 @@ module Computer(Fenv:Dataflows.FUNCTION_ENV)(X:sig
over_outputs_d = res.over_outputs_if_termination;
} in
join for_function acc)
- called
bottom
+ called
in
let result = catenate data for_functions in
let result =
(* Treatment for the possible assignment of the call result *)
(match dest with
| None -> result
- | Some lv -> add_out ~for_writing state lv Zone.bottom result)
+ | Some lv -> add_out ~for_writing request lv Zone.bottom result)
in result
(* Propagate all zones in predicates for the given statement, only in the case
@@ -395,18 +384,16 @@ module Computer(Fenv:Dataflows.FUNCTION_ENV)(X:sig
let transfer_instr stmt (i: instr) (data: t) =
match i with
| Set (lv, exp, _) ->
- let state = X.stmt_state stmt in
- let e_inputs =
- !Db.From.find_deps_no_transitivity_state state exp
- in
- add_out ~for_writing:true state lv e_inputs data
+ let request = X.stmt_request stmt in
+ let e_inputs = Eva.Results.expr_deps exp request in
+ add_out ~for_writing:true request lv e_inputs data
| Local_init (v, AssignInit i, _) ->
- let state = X.stmt_state stmt in
+ let request = X.stmt_request stmt in
let rec aux lv i acc =
match i with
| SingleInit e ->
- let e_inputs = !Db.From.find_deps_no_transitivity_state state e in
- add_out ~for_writing:false state lv e_inputs acc
+ let e_inputs = Eva.Results.expr_deps e request in
+ add_out ~for_writing:false request lv e_inputs acc
| CompoundInit(ct, initl) ->
(* Avoid folding implicit zero-initializer of large arrays. *)
let implicit = Cumulative_analysis.fold_implicit_initializer ct in
@@ -417,7 +404,7 @@ module Computer(Fenv:Dataflows.FUNCTION_ENV)(X:sig
zone of the array as outputs. It is exactly the written zone for
arrays of scalar elements. Nothing is read by zero-initializers,
so the inputs are empty. *)
- add_out ~for_writing:false state lv Zone.bottom acc
+ add_out ~for_writing:false request lv Zone.bottom acc
in
aux (Cil.var v) i data
| Call (lvaloption,funcexp,argl,loc) ->
@@ -433,8 +420,8 @@ module Computer(Fenv:Dataflows.FUNCTION_ENV)(X:sig
the condition. In this case, we just make sure that dead
edges get bottom, instead of the input state. *)
let transfer_guard stmt e t =
- let state = X.stmt_state stmt in
- let v_e = !Db.Value.eval_expr state e in
+ let request = X.stmt_request stmt in
+ let v_e = Eva.Results.(eval_exp e request |> as_cvalue) in
let t1 = Cil.unrollType (Cil.typeOf e) in
let do_then, do_else =
if Cil.isIntegralType t1 || Cil.isPointerType t1
@@ -473,7 +460,7 @@ module Computer(Fenv:Dataflows.FUNCTION_ENV)(X:sig
;;
let transfer_stmt s data =
- if Db.Value.is_reachable (X.stmt_state s)
+ if Cvalue.Model.is_reachable (X.stmt_state s)
then begin
transfer_annotations s;
transfer_stmt s data
@@ -663,20 +650,15 @@ module Callwise = struct
(* Returns the [kf] pre-state with respect to the single [call_stack]. *)
let kf_pre_state =
- match Db.Value.get_initial_state_callstack kf with
- | None ->
- Cvalue.Model.bottom
- | Some cs ->
- begin
- match Value_types.Callstack.Hashtbl.find_opt cs call_stack with
- | None -> Cvalue.Model.bottom
- | Some state -> state
- end
+ Eva.Results.(at_start_of kf |> in_callstack call_stack |>
+ get_cvalue_model)
let stmt_state stmt =
try Cil_datatype.Stmt.Hashtbl.find states stmt
with Not_found -> Cvalue.Model.bottom
+ let stmt_request stmt = Eva.Results.in_cvalue_state (stmt_state stmt)
+
let at_call stmt kf =
let _cur_kf, table = List.hd !call_inout_stack in
try
@@ -739,8 +721,9 @@ module FunctionWise = struct
let module Computer = Computer(Fenv)(struct
let _version = "functionwise"
let _kf = kf
- let kf_pre_state = Db.Value.get_initial_state kf
- let stmt_state s = Db.Value.get_stmt_state s
+ let kf_pre_state = Eva.Results.(at_start_of kf |> get_cvalue_model)
+ let stmt_state s = Eva.Results.(before s |> get_cvalue_model)
+ let stmt_request s = Eva.Results.before s
let at_call stmt kf = get_external_aux ~stmt kf
end) in
Stack.iter (fun g -> if kf == g then raise Exit) call_stack;
diff --git a/src/plugins/inout/outputs.ml b/src/plugins/inout/outputs.ml
index 8eb9a5f31d3..4d06b9f1a51 100644
--- a/src/plugins/inout/outputs.ml
+++ b/src/plugins/inout/outputs.ml
@@ -55,35 +55,32 @@ class virtual do_it_ = object(self)
self#join bits_loc
method! vinst i =
- if Db.Value.is_reachable (Db.Value.noassert_get_state self#current_kinstr)
+ let stmt = Option.get self#current_stmt in
+ if Eva.Results.is_reachable stmt
then
(* noassert needed for Eval.memoize. Not really satisfactory *)
begin
+ let assign_lval lval =
+ let for_writing = not (Cil.is_mutable_or_initialized lval) in
+ self#do_assign ~for_writing lval
+ in
match i with
| Set (lv,_,_) ->
- let for_writing = not (Cil.is_mutable_or_initialized lv) in
- self#do_assign ~for_writing lv
- | Call (lv_opt,exp,_,_) ->
- (match lv_opt with None -> ()
- | Some lv ->
- let for_writing =
- not (Cil.is_mutable_or_initialized lv)
- in
- self#do_assign ~for_writing lv);
- let state = Db.Value.get_state self#current_kinstr in
- if Cvalue.Model.is_top state then
- self#join Zone.top
- else
- let _, callees =
- !Db.Value.expr_to_kernel_function_state ~deps:None state exp in
- Kernel_function.Hptset.iter
- (fun kf ->
- let { Inout_type.over_outputs = z } =
- Operational_inputs.get_external_aux
- ?stmt:self#current_stmt kf
- in
- self#join z
- ) callees
+ assign_lval lv
+ | Call (lv_opt, exp, _, _) ->
+ begin
+ Option.iter assign_lval lv_opt;
+ let callees = Eva.Results.(before stmt |> eval_callee exp) in
+ match callees with
+ | Ok callees ->
+ let join_outputs kf =
+ let inout = Operational_inputs.get_external_aux ~stmt kf in
+ self#join inout.over_outputs
+ in
+ List.iter join_outputs callees
+ | Error (Top | DisabledDomain) -> self#join Zone.top
+ | Error Bottom -> ()
+ end
| Local_init (v, AssignInit i, _) ->
let rec aux lv = function
| SingleInit _ -> self#do_assign ~for_writing:false lv
@@ -102,8 +99,8 @@ class virtual do_it_ = object(self)
in
aux (Cil.var v) i
| Local_init (v, ConsInit(f, _, _),_) ->
- let state = Db.Value.get_state self#current_kinstr in
- if Cvalue.Model.is_top state then self#join Zone.top
+ if Cvalue.Model.is_top Eva.Results.(before stmt |> get_cvalue_model)
+ then self#join Zone.top
else begin
let { Inout_type.over_outputs = z } =
Operational_inputs.get_external_aux ?stmt:self#current_stmt
@@ -125,9 +122,9 @@ class virtual do_it_ = object(self)
method compute_funspec kf =
let state = self#specialize_state_on_call kf in
- let behaviors = !Db.Value.valid_behaviors kf state in
+ let behaviors = Eva.Logic_inout.valid_behaviors kf state in
let assigns = Ast_info.merge_assigns behaviors in
- !Db.Value.assigns_outputs_to_zone state ~result:None assigns
+ Eva.Logic_inout.assigns_outputs_to_zone state ~result:None assigns
end
module Analysis = Cumulative_analysis.Make(
diff --git a/src/plugins/inout/register.ml b/src/plugins/inout/register.ml
index 3e8e1949b55..f65fd3ad50b 100644
--- a/src/plugins/inout/register.ml
+++ b/src/plugins/inout/register.ml
@@ -52,7 +52,7 @@ let main () =
Eva.Analysis.compute ();
Callgraph.Uses.iter_in_rev_order
(fun kf ->
- if Kernel_function.is_definition kf && !Db.Value.is_called kf
+ if Kernel_function.is_definition kf && Eva.Results.is_called kf
then begin
if forceout
then Inout_parameters.result "%a" Outputs.pretty_internal kf ;
--
GitLab