zones.ml 14.14 KiB
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
module R = Datascope.R
let debug1 fmt = R.debug ~level:1 fmt
let debug2 fmt = R.debug ~level:2 fmt
open Cil_datatype
open Cil_types
type t_zones = Locations.Zone.t Stmt.Hashtbl.t
module Data = struct
type t = Locations.Zone.t
let bottom = Locations.Zone.bottom
let equal = Locations.Zone.equal
let intersects = Locations.Zone.valid_intersects
let merge = Locations.Zone.join (* over-approx *)
let diff = Locations.Zone.diff (* over-approx *)
let pretty fmt z = Format.fprintf fmt "@[<h 1>%a@]" Locations.Zone.pretty z
let exp_zone stmt exp = !Db.From.find_deps_no_transitivity stmt exp
end
module Ctx = struct
type t = Data.t Stmt.Hashtbl.t
let create = Stmt.Hashtbl.create
let find = Stmt.Hashtbl.find
let add ctx k d =
let d =
try let old_d = find ctx k in Data.merge old_d d with Not_found -> d
in Stmt.Hashtbl.replace ctx k d
(* let mem = Stmt.Hashtbl.mem : useless because Ctx has to be initialized to bot *)
let _pretty fmt infos =
Stmt.Hashtbl.iter
(fun k d -> Format.fprintf fmt "Stmt:%d -> %a@\n" k.sid Data.pretty d)
infos
end
let compute_new_data old_zone l_zone l_dpds exact r_dpds =
if (Data.intersects old_zone l_zone) then
let zone = if exact then Data.diff old_zone l_zone else old_zone in
let zone = Data.merge zone l_dpds in
let zone = Data.merge zone r_dpds in
(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
| None -> false, data
| Some lval ->
let ret_dpds = froms.Function_Froms.deps_return in
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 =
get_lval_zones ~for_writing:true stmt lval in
compute_new_data data l_zone l_dpds exact r_dpds
in data
(* we need [data_after] zone after the call, so we need to add the dpds
* of each output that intersects this zone.
* Moreover, we need to add the part of [data_after] that has not been
* modified for sure. *)
let process_froms data_after froms =
let from_table = froms.Function_Froms.deps_table in
let process_out_call out deps (to_prop, used, new_data) =
let out_dpds = Function_Froms.DepsOrUnassigned.to_zone deps in
let default = Function_Froms.DepsOrUnassigned.may_be_unassigned deps in
let exact = not default in
(* be careful to compare out with data_after and not new_data *)
if (Data.intersects data_after out) then
let to_prop = if exact then Data.diff to_prop out else to_prop in
let new_data = Data.merge new_data out_dpds in
(to_prop, true, new_data)
else (to_prop, used, new_data)
in
let to_prop =
(* part of data_after that we need to compute before call :
* = data_after minus all exact outputs.
* Don't use [data_after - (merge out)] to avoid approximation in merge *)
data_after in
let new_data = Data.bottom in (* add out_dpds when out intersects data_after*)
let used = false in (* is the call needed ? *)
let to_prop, used, new_data =
match from_table with
| Function_Froms.Memory.Bottom -> to_prop, used, new_data
| Function_Froms.Memory.Top ->
let v = Function_Froms.DepsOrUnassigned.top in
process_out_call Locations.Zone.top v (to_prop, used, new_data)
| Function_Froms.Memory.Map m ->
Function_Froms.Memory.fold process_out_call m (to_prop, used, new_data)
in let data = Data.merge to_prop new_data in
(used, data)
let process_call_args data called_kf stmt args =
let param_list = Kernel_function.get_formals called_kf in
let asgn_arg_to_param data param arg =
let param_zone = Locations.zone_of_varinfo param in
let arg_dpds = Data.exp_zone stmt arg in
let exact = true in (* param is always a variable so asgn is exact *)
let _used, data =
compute_new_data data param_zone Data.bottom exact arg_dpds in
(* can ignore 'used' because if we need param, we already know that the
* call is needed *)
data
in
let rec do_param_arg data param_list args =
match param_list, args with
| [], [] -> data
| p :: param_list, a :: args ->
let data = asgn_arg_to_param data p a in
do_param_arg data param_list args | [], _ -> (* call to a variadic function *)
(* warning already sent during 'from' computation. *)
(* TODO : merge the remaining args in data ?... *)
data
| _, [] -> R.abort "call to a function with to few arguments"
in do_param_arg data param_list args
let process_one_call data stmt lvaloption froms =
let res_used, data = process_call_res data stmt lvaloption froms in
let out_used, data = process_froms data froms in
let used = res_used || out_used in
used, data
let process_call data_after stmt lvaloption funcexp args _loc =
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 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 = 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)
(false, Data.bottom)
l
in
if used then
let data =
(* no problem of order because parameters are disjoint for sure *)
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
else begin
assert (R.verify (Data.equal data data_after)
"if statement not used, data doesn't change !");
used, data
end
module Computer (Param:sig val states : Ctx.t end) = struct
let name = "Zones"
let debug = false
let used_stmts = ref []
let add_used_stmt stmt = used_stmts := stmt :: !used_stmts
let get_and_reset_used_stmts () =
let stmts = !used_stmts in used_stmts := [] ; stmts
type t = Data.t
let pretty = Data.pretty
module StmtStartData = struct
type data = t
let clear () = Stmt.Hashtbl.clear Param.states
let mem = Stmt.Hashtbl.mem Param.states
let find = Stmt.Hashtbl.find Param.states
let replace = Stmt.Hashtbl.replace Param.states
let add = Stmt.Hashtbl.add Param.states let iter f = Stmt.Hashtbl.iter f Param.states
let length () = Stmt.Hashtbl.length Param.states
end
let combineStmtStartData _stmt ~old new_ =
if Data.equal new_ old then None else Some new_
let combineSuccessors = Data.merge
let doStmt _stmt = Dataflow2.Default
let do_assign stmt lval exp data =
let l_dpds, exact, l_zone =
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
data
let doInstr stmt instr data =
match instr with
| Set (lval, exp, _) -> Dataflow2.Done (do_assign stmt lval exp data)
| Local_init (v, AssignInit i, _) ->
let rec aux lv i acc =
match i with
| SingleInit e -> do_assign stmt lv e data
| CompoundInit(ct, initl) ->
let implicit = true in
let doinit o i _ data = aux (Cil.addOffsetLval o lv) i data in
Cil.foldLeftCompound ~implicit ~doinit ~ct ~initl ~acc
in
Dataflow2.Done (aux (Cil.var v) i data)
| Call (lvaloption,funcexp,args,loc) ->
let used, data = process_call data stmt lvaloption funcexp args loc in
let _ = if used then add_used_stmt stmt in
Dataflow2.Done data
| Local_init(v, ConsInit(f, args, k), l) ->
let used, data =
Cil.treat_constructor_as_func (process_call data stmt) v f args k l
in
if used then add_used_stmt stmt;
Dataflow2.Done data
| Skip _ | Code_annot _ | Asm _ -> Dataflow2.Default
let filterStmt _stmt _next = true
let funcExitData = Data.bottom
end
let compute_ctrl_info pdg ctrl_part used_stmts =
let module CtrlComputer = Computer (struct let states = ctrl_part end) in
let module CtrlCompute = Dataflow2.Backwards(CtrlComputer) in
let seen = Stmt.Hashtbl.create 50 in
let rec add_node_ctrl_nodes new_stmts node =
let ctrl_nodes = !Db.Pdg.direct_ctrl_dpds pdg node in
List.fold_left add_ctrl_node new_stmts ctrl_nodes
and add_ctrl_node new_stmts ctrl_node =
debug2 "[zones] add ctrl node %a@." PdgTypes.Node.pretty ctrl_node;
match PdgTypes.Node.stmt ctrl_node with
| None -> (* node without stmt : add its ctrl_dpds *)
add_node_ctrl_nodes new_stmts ctrl_node
| Some stmt ->
debug2 "[zones] node %a is stmt %d@."
PdgTypes.Node.pretty ctrl_node stmt.sid;
if Stmt.Hashtbl.mem seen stmt then new_stmts
else
let ctrl_zone = match stmt.skind with
| Switch (exp,_,_,_) | If (exp,_,_,_) -> Data.exp_zone stmt exp
| _ -> Data.bottom in Ctx.add ctrl_part stmt ctrl_zone;
Stmt.Hashtbl.add seen stmt ();
debug2 "[zones] add ctrl zone %a at stmt %d@."
Data.pretty ctrl_zone stmt.sid;
stmt::new_stmts
and add_stmt_ctrl new_stmts stmt =
debug1 "[zones] add ctrl of stmt %d@." stmt.sid;
if Stmt.Hashtbl.mem seen stmt then new_stmts
else begin
Stmt.Hashtbl.add seen stmt ();
match !Db.Pdg.find_simple_stmt_nodes pdg stmt with
| [] -> []
| n::_ -> add_node_ctrl_nodes new_stmts n
end
in
let rec add_stmts_ctrl stmts all_used_stmts =
let all_used_stmts = stmts @ all_used_stmts in
let new_stmts = List.fold_left add_stmt_ctrl [] stmts in
let preds = List.fold_left (fun acc s -> s.preds @ acc) [] new_stmts in
if preds <> [] then CtrlCompute.compute preds;
let used_stmts = CtrlComputer.get_and_reset_used_stmts () in
if used_stmts = [] then all_used_stmts
else add_stmts_ctrl used_stmts all_used_stmts
in
add_stmts_ctrl used_stmts []
let compute kf stmt lval =
let f = Kernel_function.get_definition kf in
let dpds, _exact, zone =
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;
let data_part = Ctx.create 50 in
List.iter (fun s -> Ctx.add data_part s Data.bottom) f.sallstmts;
let _ = Ctx.add data_part stmt zone in
let module DataComputer = Computer (struct let states = data_part end) in
let module DataCompute = Dataflow2.Backwards(DataComputer) in
let _ = DataCompute.compute stmt.preds in
let ctrl_part = data_part (* Ctx.create 50 *) in
(* it is confusing to have 2 part in the provided information,
* because in fact, it means nothing to separate them.
* So let's put everything in the same object *)
let used_stmts = DataComputer.get_and_reset_used_stmts () in
let all_used_stmts =
if used_stmts = [] then []
else compute_ctrl_info (!Db.Pdg.get kf) ctrl_part used_stmts
in
let all_used_stmts =
List.fold_left
(fun e acc -> Stmt.Hptset.add acc e) Stmt.Hptset.empty all_used_stmts
in
all_used_stmts, data_part
let get stmt_zones stmt =
try Ctx.find stmt_zones stmt with Not_found -> Data.bottom
let pretty fmt stmt_zones =
let pp s d = Format.fprintf fmt "Stmt:%d -> %a@." s.sid Data.pretty d in
Stmt.Hashtbl.iter_sorted pp stmt_zones
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
let build_zones kf stmt lval =
(* TODO: Journal.register *)
(* (Datatype.func Kernel_type.kernel_function
(Datatype.func Kernel_type.stmt
(Datatype.func Kernel_type.lval
(Datatype.couple Kernel_type.stmt_set zones_ty)))))
*) if stmt.preds = []
then Stmt.Hptset.empty, Ctx.create 0
else compute kf stmt lval
let get_zones =
(* TODO: Journal.register *)
(*(Datatype.func zones_ty (Datatype.func Kernel_type.stmt data_ty)))*)
get
let pretty_zones =
(* TODO: Journal.register *)
(*( Datatype.func Datatype.formatter (Datatype.func zones_ty Datatype.unit)))*)
pretty