From 12c3a8bb2fa9df3c01decce12a0d95b201e52bbb Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Fri, 17 Sep 2021 17:22:04 +0200
Subject: [PATCH] [Eva] api: Implements equalities extraction
---
src/plugins/value/utils/results.ml | 25 +++++++++++++++++++++++--
src/plugins/value/utils/results.mli | 2 +-
2 files changed, 24 insertions(+), 3 deletions(-)
diff --git a/src/plugins/value/utils/results.ml b/src/plugins/value/utils/results.ml
index c74ee12715f..2ee26e12af1 100644
--- a/src/plugins/value/utils/results.ml
+++ b/src/plugins/value/utils/results.ml
@@ -254,8 +254,29 @@ struct
let callstacks req =
Response.callstacks (get_by_callstack req)
- let equality_class _exp _req =
- raise Not_implemented (* Where is the key for Equality_domain ? *)
+ let equality_class exp req =
+ let open Equality in
+ match A.Dom.get Equality_domain.key with
+ | None ->
+ Result.error DisabledDomain
+ | Some extract ->
+ let hce = Hcexprs.HCE.of_exp exp in
+ let extract' state =
+ let equalities = Equality_domain.project (extract state) in
+ NonTrivial (Set.find hce equalities)
+ and reduce e1 e2 =
+ match e1, e2 with
+ | Trivial, _ | _, Trivial -> Trivial
+ | NonTrivial e1, NonTrivial e2 -> Equality.inter e1 e2
+ in
+ let r = match Response.map_join extract' reduce (get req) with
+ | (`Top | `Bottom) as r -> r
+ | `Value Trivial -> `Top
+ | `Value (NonTrivial e) ->
+ let l = Equality.elements e in
+ `Value (List.map Hcexprs.HCE.to_exp l)
+ in
+ convert r
let as_cvalue_model req =
match A.Dom.get Cvalue_domain.State.key with
diff --git a/src/plugins/value/utils/results.mli b/src/plugins/value/utils/results.mli
index b70dd4a4bcc..50b1505f08d 100644
--- a/src/plugins/value/utils/results.mli
+++ b/src/plugins/value/utils/results.mli
@@ -57,7 +57,7 @@ val filter_callstack : (callstack -> bool) -> request -> request
(* State requests *)
val callstacks : request -> callstack list
-val equality_class : Cil_types.exp -> request -> Cil_types.exp list option
+val equality_class : Cil_types.exp -> request -> Cil_types.exp list result
val as_cvalue_model : request -> Cvalue.Model.t result
(* Evaluation *)
--
GitLab