Commit 014fffbd authored by David Bühler's avatar David Bühler Committed by Andre Maroneze
Browse files

[Eva] Comments the Domain_builder.Restrict functor and Domain_mode signature.

parent 2930745b
......@@ -262,6 +262,7 @@ module Restrict
open Domain_mode
(* Defines the join and the narrow of different modes. *)
module Mode = struct
include Mode
......@@ -277,11 +278,19 @@ module Restrict
let narrow = merge (||)
(* Map that binds functions to their analysis mode. *)
let functions_map =
(fun map (kf, mode) -> Kernel_function.Map.add kf mode map)
Kernel_function.Map.empty Scope.functions
(* This module propagates states of type [(state * mode) option]:
- None is propagated as long as no functions from [Scope.functions]
is analyzed.
- then the current [mode] is propagated alongside the state. Queries and
transfer functions are applied accordingly. The current mode is replaced
at function calls by [mode.calls]. *)
module Info = struct let module_name = ^ " restricted" end
module D = Datatype.Pair_with_collections (Domain) (Mode) (Info)
......@@ -301,6 +310,9 @@ module Restrict
| None ->
| Some (state, _mode) -> state
(* When the first function from [Scope.functions] is encountered, starts the
analysis with the state computed by this function. It is an empty state in
which the global variables exist and may have any values. *)
let compute_starting_state () =
let empty = Domain.empty () in
let var_kind = Abstract_domain.Global in
......@@ -310,6 +322,8 @@ module Restrict
Globals.Vars.fold init empty
(* Do not recompute each time the starting state. Do not compute the starting
state too early either, in case it depends on analysis options. *)
let get_starting_state =
let starting_state = ref None in
fun () ->
......@@ -347,8 +361,8 @@ module Restrict
(* ----- Queries ---------------------------------------------------------- *)
let default_query = `Value (, None), Alarmset.all
(* Applies the [query] only if the current mode allows the domain to read.
Otherwise, returns [default]. *)
let make_query default query = function
| None -> default
| Some (state, mode) ->
......@@ -356,6 +370,8 @@ module Restrict
then query state
else default
let default_query = `Value (, None), Alarmset.all
let extract_expr oracle state expr =
make_query default_query (fun s -> Domain.extract_expr oracle s expr) state
......@@ -376,6 +392,8 @@ module Restrict
(* ----- Transfer functions ----------------------------------------------- *)
(* Applies the transfer function [f] only if the current mode allows the
domain to write. Otherwise, returns the state unchanged. *)
let make_transfer f = function
| None -> `Value None
| Some (state, mode) ->
......@@ -387,6 +405,9 @@ module Restrict
let assume stmt expr positive valuation =
make_transfer (Domain.assume stmt expr positive valuation)
(* Applies the [assign] transfer function according to the current mode.
In any case, removes from the state the properties depending on the memory
location modified by the assignment. *)
let assign kinstr lvalue expr assigned valuation = function
| None -> `Value None
| Some (state, mode) ->
......@@ -398,6 +419,10 @@ module Restrict
let state = Domain.logic_assign None lvalue.lloc state in
`Value (Some (state, mode))
(* Starts an analysis at call [call] with state [state]. The domain was not
enabled before this call: the concrete arguments may contain variables that
have never been introduced into the state, so we should not use them. This
function only introduce the formal parameters in the state. *)
let start_analysis call state =
let formals = (fun argument -> argument.formal) call.arguments in
let kind = Abstract_domain.Formal call.kf in
......@@ -406,7 +431,16 @@ module Restrict
let state = List.fold_left initialize state formals in
(* When interpreting a function call:
- if the mode of the function called allows the domain to infer properties,
use [start_call] and [finalize_call] as normal. If the current mode did
not allow the domain to infer properties, use [start_analysis] instead.
- otherwise, only propagate the state from the call site to kill the
properties that depend on locations written in the called functions. *)
let start_call stmt call valuation state =
(* Starts the call with mode [new_mode]. [previous_mode] is the current mode
of the caller. *)
let start_call_with_mode ?previous_mode ~new_mode state =
if new_mode.current.write
......@@ -418,6 +452,9 @@ module Restrict
`Value (Some (start_analysis call state, new_mode))
else `Value (Some (state, new_mode))
(* If an analysis mode is defined for the called function in [Scope],
then this mode becomes the new current mode. Otherwise, use the [calls]
field of the previous mode. *)
let called_mode = Kernel_function.Map.find_opt call.kf functions_map in
match state, called_mode with
| Some (state, previous_mode), Some new_mode ->
......@@ -483,6 +520,7 @@ module Restrict
let enter_scope kind varinfos = lift (Domain.enter_scope kind varinfos)
let leave_scope kf varinfos = lift (Domain.leave_scope kf varinfos)
(* Uses the mode of the 'main' function to start the analysis. *)
let empty () =
let main_kf = fst (Globals.entry_point ()) in
match Kernel_function.Map.find_opt main_kf functions_map with
......@@ -56,6 +56,11 @@ module Complete_Simple_Cvalue
and type location = Precise_locs.precise_location
and type state = Domain.t
(* Restricts an abstract domain on specific functions. The domain will only be
enabled on the given functions. Moreover, a mode is associated to each of
these functions, allowing (or not) the domain to infer or use properties
in the current function and in all functions called from it.
See {!Domain_mode} for more details. *)
module Restrict
(Value: Abstract_value.S)
(Domain: Abstract.Domain.Internal with type value = Value.t)
......@@ -20,14 +20,30 @@
(* *)
(** This module defines the mode to restrict an abstract domains on specific
functions. *)
(** Permission for an abstract domain to read/write its state.
If [write] is true, the domain infers new properties when interpreting
assignments, assumptions, and logical assertions. Otherwise, it only
propagates already known properties as long as they hold.
If [read] is true, the domain uses its inferred properties to improve
the evaluation of expressions by extracting information from its state.
It can also evaluate logical assertions. *)
type permission = { read: bool; write: bool; }
(** Mode for the analysis of a function [f]:
- [current] is the read/write permission for [f].
- [calls] is the read/write permission for all functions called from [f]. *)
type mode = { current: permission; calls: permission; }
(** Datatype for modes. *)
module Mode : sig
include Datatype.S_with_collections with type t = mode
val all: t
val all: t (** Default mode: all permissions are granted. *)
(** A function associated with an analysis mode. *)
type function_mode = Kernel_function.t * mode
module Function_Mode:
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment