From e5d3eee20903061765f86c4964d0473f0d17e914 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 3 Apr 2019 13:39:59 +0200
Subject: [PATCH] [Eva] In abstract domains, update can return Bottom.
---
src/plugins/value/domains/abstract_domain.mli | 2 +-
src/plugins/value/domains/apron/apron_domain.ok.ml | 14 +++++---------
src/plugins/value/domains/cvalue/cvalue_domain.ml | 2 +-
.../value/domains/cvalue/cvalue_transfer.ml | 12 +++++++-----
src/plugins/value/domains/domain_builder.ml | 4 ++--
src/plugins/value/domains/domain_product.ml | 5 +++--
.../value/domains/equality/equality_domain.ml | 2 +-
src/plugins/value/domains/gauges/gauges_domain.ml | 12 +++++-------
src/plugins/value/domains/inout_domain.ml | 2 +-
src/plugins/value/domains/offsm_domain.ml | 4 ++--
src/plugins/value/domains/simple_memory.ml | 9 +++++----
src/plugins/value/domains/symbolic_locs.ml | 8 ++++----
src/plugins/value/domains/unit_domain.ml | 2 +-
src/plugins/value/engine/transfer_stmt.ml | 2 +-
src/plugins/value/register.ml | 11 ++++++-----
15 files changed, 45 insertions(+), 46 deletions(-)
diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index f2dc9ff30e5..b512325ade4 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -186,7 +186,7 @@ module type Transfer = sig
(** [update valuation t] updates the state [t] by the values of expressions
and the locations of lvalues stored in [valuation]. *)
- val update : valuation -> state -> state
+ val update : valuation -> state -> state or_bottom
(** [assign kinstr lv expr v valuation state] is the transfer function for the
assignment [lv = expr] for [state]. It must return the state where the
diff --git a/src/plugins/value/domains/apron/apron_domain.ok.ml b/src/plugins/value/domains/apron/apron_domain.ok.ml
index 27aa29d81c1..e69f47ab862 100644
--- a/src/plugins/value/domains/apron/apron_domain.ok.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ok.ml
@@ -451,11 +451,7 @@ module Make
let array = Tcons1.array_make env (List.length constraints) in
List.iteri (fun i c -> Tcons1.array_set array i c) constraints;
let st = Abstract1.meet_tcons_array man state array in
- if debug && Abstract1.is_bottom man st then
- Value_parameters.result ~current:true ~once:true
- "Bottom with state %a and constraints %a@."
- Abstract1.print state (fun fmt a -> Tcons1.array_print fmt a) array;
- st
+ if Abstract1.is_bottom man st then `Bottom else `Value st
let _constraint_to_typ env state vars =
let aux (var_apron, vi) =
@@ -615,11 +611,11 @@ module Make
in
let constraints = Valuation.fold gather_constraints valuation [] in
if constraints = []
- then state
+ then `Value state
else meet_with_constraints env state constraints
let assign _stmt lvalue expr _value valuation state =
- let state = update valuation state in
+ update valuation state >>- fun state ->
try
let state =
try
@@ -642,7 +638,7 @@ module Make
let assume _stmt exp bool valuation state =
- let state = update valuation state in
+ update valuation state >>- fun state ->
try
let env = Abstract1.env state in
let eval = make_eval state in
@@ -656,7 +652,7 @@ module Make
| Out_of_Scope _ -> `Value state
let start_call _stmt call valuation state =
- let state = update valuation state in
+ update valuation state >>- fun state ->
let eval = make_eval state in
let oracle = make_oracle valuation in
let process_argument (vars, acc) arg =
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index 798c4ea72f7..995298130d6 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -227,7 +227,7 @@ module State = struct
module T = Cvalue_transfer.Transfer (Valuation)
- let update valuation (s, clob) = T.update valuation s, clob
+ let update valuation (s, clob) = T.update valuation s >>-: fun s -> s, clob
let assign stmt lv expr assigned valuation (s, clob) =
T.assign stmt lv expr assigned valuation s >>-: fun s ->
diff --git a/src/plugins/value/domains/cvalue/cvalue_transfer.ml b/src/plugins/value/domains/cvalue/cvalue_transfer.ml
index a53f6cf775e..1e9065ac7f3 100644
--- a/src/plugins/value/domains/cvalue/cvalue_transfer.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_transfer.ml
@@ -90,11 +90,7 @@ module Transfer
else t
| _ -> t
in
- let s = Valuation.fold process valuation t in
- s
-
- let assume _stmt _expr _positive valuation state = `Value (update valuation state)
-
+ Valuation.fold process valuation t
(* ---------------------------------------------------------------------- *)
(* Assignments *)
@@ -246,4 +242,10 @@ module Transfer
let typ = Cil.typeOf expr in
Eval_op.pretty_offsetmap typ fmt offsm
| _ -> Format.fprintf fmt "%s" (Unicode.top_string ())
+
+
+ (* ----------------- Export assumption functions -------------------------- *)
+
+ let update valuation state = `Value (update valuation state)
+ let assume _stmt _expr _positive = update
end
diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml
index 108c1c4eada..b27b01329e1 100644
--- a/src/plugins/value/domains/domain_builder.ml
+++ b/src/plugins/value/domains/domain_builder.ml
@@ -79,7 +79,7 @@ module Make_Minimal
and type loc = location)
= struct
- let update _valuation state = state
+ let update _valuation state = `Value state
let assign kinstr lv expr _value _valuation state =
Domain.assign kinstr lv.Eval.lval expr state
@@ -227,7 +227,7 @@ module Complete_Simple_Cvalue (Domain: Simpler_domains.Simple_Cvalue)
let record valuation = { find = find valuation;
find_loc = find_loc valuation; }
- let update _valuation state = state
+ let update _valuation state = `Value state
let assign kinstr lv expr value valuation state =
Domain.assign kinstr lv expr value (record valuation) state
let assume stmt expr positive valuation state =
diff --git a/src/plugins/value/domains/domain_product.ml b/src/plugins/value/domains/domain_product.ml
index 35ada8461cc..fffc784d6c8 100644
--- a/src/plugins/value/domains/domain_product.ml
+++ b/src/plugins/value/domains/domain_product.ml
@@ -161,8 +161,9 @@ module Make
module Right_Transfer = Right.Transfer (Right_Valuation)
let update valuation (left, right) =
- Left_Transfer.update valuation left,
- Right_Transfer.update valuation right
+ Left_Transfer.update valuation left >>- fun left ->
+ Right_Transfer.update valuation right >>-: fun right ->
+ left, right
let assign stmt lv expr value valuation (left, right) =
Left_Transfer.assign stmt lv expr value valuation left >>- fun left ->
diff --git a/src/plugins/value/domains/equality/equality_domain.ml b/src/plugins/value/domains/equality/equality_domain.ml
index 69f1c355b3a..7ccb02c9721 100644
--- a/src/plugins/value/domains/equality/equality_domain.ml
+++ b/src/plugins/value/domains/equality/equality_domain.ml
@@ -338,7 +338,7 @@ module Make
let deps = HCESet.fold (add_one_dep valuation) lvalues.read deps in
HCESet.fold (add_one_dep valuation) lvalues.addr deps
- let update _valuation state = state
+ let update _valuation state = `Value state
let is_singleton = match get_cvalue with
| None -> fun _ -> false
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index e726348a907..1af31275192 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -1199,19 +1199,16 @@ module D_Impl : Abstract_domain.S_with_Structure
let assume_exp_bot valuation e r state =
state >>- assume_exp valuation e r
- let assume_valuation valuation state =
+ let update valuation state =
let assume_one = assume_exp_bot valuation in
Valuation.fold assume_one valuation (`Value state)
- let update valuation state =
- Bottom.non_bottom (assume_valuation valuation state)
-
- let assume _ _ _ = assume_valuation
+ let assume _ _ _ = update
exception Unassignable
let assign _kinstr lv e _assignment valuation (state:state) =
- let state = update valuation state in
+ update valuation state >>- fun state ->
let to_loc lv =
match Valuation.find_loc valuation lv with
| `Value r -> Precise_locs.imprecise_location r.loc
@@ -1242,8 +1239,9 @@ module D_Impl : Abstract_domain.S_with_Structure
match function_calls_handling with
| FullInterprocedural -> update valuation state
| IntraproceduralAll
- | IntraproceduralNonReferenced -> G.empty
+ | IntraproceduralNonReferenced -> `Value G.empty
in
+ state >>- fun state ->
(* track [arg.formal] into [state]. Important for functions that
receive a size as argument. *)
let aux_arg state arg =
diff --git a/src/plugins/value/domains/inout_domain.ml b/src/plugins/value/domains/inout_domain.ml
index bd2e643f14d..12ba3cd1528 100644
--- a/src/plugins/value/domains/inout_domain.ml
+++ b/src/plugins/value/domains/inout_domain.ml
@@ -264,7 +264,7 @@ module Internal
let finalize_call _stmt _call ~pre ~post =
`Value (Transfer.catenate pre post)
- let update _valuation state = state
+ let update _valuation state = `Value state
let show_expr _valuation _state _fmt _expr = ()
end
diff --git a/src/plugins/value/domains/offsm_domain.ml b/src/plugins/value/domains/offsm_domain.ml
index c2653e2de79..9eb0b4ef308 100644
--- a/src/plugins/value/domains/offsm_domain.ml
+++ b/src/plugins/value/domains/offsm_domain.ml
@@ -129,7 +129,7 @@ module Internal : Domain_builder.InputDomain
and type valuation := Valuation.t
= struct
- let update _valuation st = st (* TODO? *)
+ let update _valuation st = `Value st (* TODO? *)
let kill loc state =
Memory.add_binding ~exact:true state loc V_Or_Uninitialized.top
@@ -171,7 +171,7 @@ module Internal : Domain_builder.InputDomain
let finalize_call _stmt _call ~pre:_ ~post = `Value post
- let start_call _stmt _call valuation state = `Value (update valuation state)
+ let start_call _stmt _call valuation state = update valuation state
let show_expr _valuation _state _fmt _expr = ()
end
diff --git a/src/plugins/value/domains/simple_memory.ml b/src/plugins/value/domains/simple_memory.ml
index 4f27194587e..f312b589f11 100644
--- a/src/plugins/value/domains/simple_memory.ml
+++ b/src/plugins/value/domains/simple_memory.ml
@@ -247,25 +247,26 @@ module Make_Internal (Info: sig val name: string end) (Value: Value) = struct
(* This function fills [state] according to the information available
in [valuation]. This information is computed by Eva's engine for
all the expressions involved in the current statement. *)
- let update valuation state =
+ let assume_valuation valuation state =
Valuation.fold (assume_exp valuation) valuation state
(* Abstraction of an assignment. *)
let assign _kinstr lv _expr value valuation state =
(* Update the state with the information obtained from evaluating
[lv] and [e] *)
- let state = update valuation state in
+ let state = assume_valuation valuation state in
(* Extract the abstract value *)
let value = Eval.value_assigned value in
(* Store the information [lv = e;] in the state *)
let state = bind_loc lv.lloc lv.ltyp value state in
`Value state
+ let update valuation state = `Value (assume_valuation valuation state)
+
(* Abstraction of a conditional. All information inferred by the engine
is present in the valuation, and must be stored in the memory
abstraction of the domain itself. *)
- let assume _stmt _expr _pos valuation state =
- `Value (update valuation state)
+ let assume _stmt _expr _pos = update
let start_call _stmt call _valuation state =
let bind_argument state argument =
diff --git a/src/plugins/value/domains/symbolic_locs.ml b/src/plugins/value/domains/symbolic_locs.ml
index 952cf517636..42db4cd7cb5 100644
--- a/src/plugins/value/domains/symbolic_locs.ml
+++ b/src/plugins/value/domains/symbolic_locs.ml
@@ -540,7 +540,7 @@ module Internal : Domain_builder.InputDomain
state
| _ -> state
in
- Valuation.fold aux valuation state
+ `Value (Valuation.fold aux valuation state)
let store_value valuation lv loc state v =
let loc = Precise_locs.imprecise_location loc in
@@ -568,14 +568,14 @@ module Internal : Domain_builder.InputDomain
(* perform [lv = e] in [state] *)
let assign _kinstr lv _e v valuation state =
- let state = update valuation state in
+ update valuation state >>- fun state ->
match v with
| Copy (_, vc) -> store_copy valuation lv lv.lloc state vc
| Assign v -> store_value valuation lv.lval lv.lloc state v
- let assume _stmt _exp _pos valuation state = `Value (update valuation state)
+ let assume _stmt _exp _pos valuation state = update valuation state
- let start_call _stmt _call valuation state = `Value (update valuation state)
+ let start_call _stmt _call valuation state = update valuation state
let finalize_call _stmt _call ~pre:_ ~post = `Value post
diff --git a/src/plugins/value/domains/unit_domain.ml b/src/plugins/value/domains/unit_domain.ml
index 62aba6028cf..4bb14526c7b 100644
--- a/src/plugins/value/domains/unit_domain.ml
+++ b/src/plugins/value/domains/unit_domain.ml
@@ -66,7 +66,7 @@ module Make
and type loc = location)
= struct
- let update _ _ = ()
+ let update _ _ = `Value ()
let assign _ _ _ _ _ _ = `Value ()
let assume _ _ _ _ _ = `Value ()
let start_call _ _ _ _ = `Value ()
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 2a2ac4ca72b..d3edae41ba2 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -412,7 +412,7 @@ module Make
valuation >>- fun valuation ->
Eva.assume ~valuation state argument.concrete post_value
in
- List.fold_left reduce_one_argument valuation reductions >>-: fun valuation ->
+ List.fold_left reduce_one_argument valuation reductions >>- fun valuation ->
TF.update valuation state
(* -------------------- Treat the results of a call ----------------------- *)
diff --git a/src/plugins/value/register.ml b/src/plugins/value/register.ml
index c3ec4215b3a..08b9174733a 100644
--- a/src/plugins/value/register.ml
+++ b/src/plugins/value/register.ml
@@ -191,6 +191,9 @@ let bot_state = function
| `Bottom -> Cvalue.Model.bottom
| `Value s -> s
+let update valuation state =
+ bot_state (Transfer.update valuation state >>-: Cvalue_domain.project)
+
let rec eval_deps state e =
match e.enode with
| SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ | Const _ ->
@@ -240,7 +243,7 @@ let eval_expr_with_valuation ?with_alarms deps state expr=
match eval with
| `Bottom -> (Cvalue.Model.bottom, deps, Cvalue.V.bottom), None
| `Value (valuation, result) ->
- let state = Cvalue_domain.project (Transfer.update valuation state) in
+ let state = update valuation state in
(state, deps, result), Some valuation
(* Compatibility layer between the old API of eval_exprs and the new evaluation
@@ -274,8 +277,7 @@ module Eval = struct
let eval, _alarms =
Eva.reduce state expr positive
in
- bot_state (eval >>-: fun valuation ->
- Cvalue_domain.project (Transfer.update valuation state))
+ bot_state (eval >>-: fun valuation -> update valuation state)
let lval_to_precise_loc_deps_state ?with_alarms ~deps state ~reduce_valid_index:(_:bool) lval =
@@ -295,8 +297,7 @@ module Eval = struct
notify_opt with_alarms alarms;
match eval with
| `Bottom -> Cvalue.Model.bottom, deps, Precise_locs.loc_bottom, (Cil.typeOfLval lval)
- | `Value (valuation, loc, typ) ->
- Cvalue_domain.project (Transfer.update valuation state), deps, loc, typ
+ | `Value (valuation, loc, typ) -> update valuation state, deps, loc, typ
let lval_to_loc_deps_state ?with_alarms ~deps state ~reduce_valid_index lv =
let state, deps, pl, typ =
--
GitLab