From 3c33631bb81ecbd082bb3f6502e26df619c330c5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 29 Jun 2021 14:47:47 +0200
Subject: [PATCH] [Eva] In abstract domains, changes the signature of
[interpret_acsl_extension].
This function now takes a logical environment, as [evaluate_predicate] and
[reduce_by_predicate].
---
src/plugins/value/domains/abstract_domain.mli | 3 ++-
src/plugins/value/domains/cvalue/cvalue_domain.ml | 2 +-
src/plugins/value/domains/domain_builder.ml | 9 +++++----
src/plugins/value/domains/domain_builder.mli | 3 ++-
src/plugins/value/domains/domain_product.ml | 7 ++++---
src/plugins/value/domains/taint_domain.ml | 2 +-
src/plugins/value/engine/transfer_logic.ml | 14 +++++++++++---
src/plugins/value/engine/transfer_logic.mli | 3 ++-
8 files changed, 28 insertions(+), 15 deletions(-)
diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index 9d3603ad580..dcd64ed8222 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -412,7 +412,8 @@ module type S = sig
(** Interprets an ACSL extension.
Defined by {!Domain_builder.Complete} as the identity. *)
- val interpret_acsl_extension: acsl_extension -> state -> state
+ val interpret_acsl_extension:
+ acsl_extension -> state logic_environment -> state -> state
(** {3 Scoping and initialization } *)
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index 22f0af53515..3bc961572d7 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -316,7 +316,7 @@ module State = struct
then `Value (state, clob)
else `Bottom
- let interpret_acsl_extension _extension state = state
+ let interpret_acsl_extension _extension _env state = state
let evaluate_from_clause state deps =
(* Evaluates the contents of one element of the from clause, topify them,
diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml
index 7c05474f1b5..d5b24f78bd2 100644
--- a/src/plugins/value/domains/domain_builder.ml
+++ b/src/plugins/value/domains/domain_builder.ml
@@ -39,7 +39,8 @@ module type LeafDomain = sig
t Abstract_domain.logic_environment -> t -> predicate -> Alarmset.status
val reduce_by_predicate:
t Abstract_domain.logic_environment -> t -> predicate -> bool -> t or_bottom
- val interpret_acsl_extension: acsl_extension -> t -> t
+ val interpret_acsl_extension:
+ acsl_extension -> t Abstract_domain.logic_environment -> t -> t
val enter_loop: stmt -> t -> t
val incr_loop_counter: stmt -> t -> t
@@ -65,7 +66,7 @@ module Complete (Domain: InputDomain) = struct
let evaluate_predicate _env _state _predicate = Alarmset.Unknown
let reduce_by_predicate _env state _predicate _positive = `Value state
- let interpret_acsl_extension _extension state = state
+ let interpret_acsl_extension _extension _env state = state
let enter_loop _stmt state = state
let incr_loop_counter _stmt state = state
@@ -546,8 +547,8 @@ module Restrict
then Some (f state, mode)
else x
- let interpret_acsl_extension extension =
- lift (Domain.interpret_acsl_extension extension)
+ let interpret_acsl_extension extension env =
+ lift (Domain.interpret_acsl_extension extension (lift_env env))
let enter_scope kind varinfos = lift (Domain.enter_scope kind varinfos)
let leave_scope kf varinfos = lift (Domain.leave_scope kf varinfos)
diff --git a/src/plugins/value/domains/domain_builder.mli b/src/plugins/value/domains/domain_builder.mli
index 4c38846e01f..3fd93d21184 100644
--- a/src/plugins/value/domains/domain_builder.mli
+++ b/src/plugins/value/domains/domain_builder.mli
@@ -45,7 +45,8 @@ module type LeafDomain = sig
t Abstract_domain.logic_environment -> t -> predicate -> Alarmset.status
val reduce_by_predicate:
t Abstract_domain.logic_environment -> t -> predicate -> bool -> t or_bottom
- val interpret_acsl_extension: acsl_extension -> t -> t
+ val interpret_acsl_extension:
+ acsl_extension -> t Abstract_domain.logic_environment -> t -> t
val enter_loop: stmt -> t -> t
val incr_loop_counter: stmt -> t -> t
diff --git a/src/plugins/value/domains/domain_product.ml b/src/plugins/value/domains/domain_product.ml
index ceda6361b5f..3adc09a4532 100644
--- a/src/plugins/value/domains/domain_product.ml
+++ b/src/plugins/value/domains/domain_product.ml
@@ -263,9 +263,10 @@ module Make
Right.reduce_by_predicate right_env right pred positive >>-: fun right ->
left, right
- let interpret_acsl_extension extension (left, right) =
- Left.interpret_acsl_extension extension left,
- Right.interpret_acsl_extension extension right
+ let interpret_acsl_extension extension env (left, right) =
+ let left_env, right_env = split_logic_env env in
+ Left.interpret_acsl_extension extension left_env left,
+ Right.interpret_acsl_extension extension right_env right
let enter_scope kind vars (left, right) =
Left.enter_scope kind vars left, Right.enter_scope kind vars right
diff --git a/src/plugins/value/domains/taint_domain.ml b/src/plugins/value/domains/taint_domain.ml
index 60a72b4b7da..d0ef3151485 100644
--- a/src/plugins/value/domains/taint_domain.ml
+++ b/src/plugins/value/domains/taint_domain.ml
@@ -512,7 +512,7 @@ let interpret_taint_logic (module Abstract: Abstractions.S) : (module Abstractio
in
`Value (Abstract.Dom.set key taint state)
- let interpret_acsl_extension extension state =
+ let interpret_acsl_extension extension _env state =
if String.equal extension.ext_name "taint"
|| String.equal extension.ext_name "taints"
then
diff --git a/src/plugins/value/engine/transfer_logic.ml b/src/plugins/value/engine/transfer_logic.ml
index 367c0c0e8e7..95f0220637e 100644
--- a/src/plugins/value/engine/transfer_logic.ml
+++ b/src/plugins/value/engine/transfer_logic.ml
@@ -304,7 +304,8 @@ module type LogicDomain = sig
t Abstract_domain.logic_environment -> t -> predicate -> Alarmset.status
val reduce_by_predicate:
t Abstract_domain.logic_environment -> t -> predicate -> bool -> t or_bottom
- val interpret_acsl_extension: acsl_extension -> t -> t
+ val interpret_acsl_extension:
+ acsl_extension -> t Abstract_domain.logic_environment -> t -> t
end
module Make
@@ -505,8 +506,11 @@ module Make
let states =
eval_and_reduce kf b active k posts states build_prop build_env
in
+ let interpret_extension extension state =
+ Domain.interpret_acsl_extension extension (build_env state) state
+ in
List.fold_left
- (fun acc e -> States.map (Domain.interpret_acsl_extension e) acc)
+ (fun acc e -> States.map (interpret_extension e) acc)
states b.b_extended
in
List.fold_left check_one_behavior post_states behaviors
@@ -711,7 +715,11 @@ module Make
| AVariant _ | AAssigns _ | AAllocation _
| AStmtSpec _ (*TODO*) -> states
| AExtended (_, _, extension) ->
- States.map (Domain.interpret_acsl_extension extension) states
+ let interpret_extension extension state =
+ let env = here_env ~pre:initial_state ~here:state in
+ Domain.interpret_acsl_extension extension env state
+ in
+ States.map (interpret_extension extension) states
end
diff --git a/src/plugins/value/engine/transfer_logic.mli b/src/plugins/value/engine/transfer_logic.mli
index 11ab601df13..99b9b94b2c6 100644
--- a/src/plugins/value/engine/transfer_logic.mli
+++ b/src/plugins/value/engine/transfer_logic.mli
@@ -73,7 +73,8 @@ module type LogicDomain = sig
t Abstract_domain.logic_environment -> t -> predicate -> Alarmset.status
val reduce_by_predicate:
t Abstract_domain.logic_environment -> t -> predicate -> bool -> t or_bottom
- val interpret_acsl_extension: acsl_extension -> t -> t
+ val interpret_acsl_extension:
+ acsl_extension -> t Abstract_domain.logic_environment -> t -> t
end
module Make
--
GitLab