From 65d9b00f4e6d049704892fd64dab18e40ad66778 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 12 Jan 2023 18:43:41 +0100
Subject: [PATCH] [Eva] Minor optimization of partitioning splits on ACSL
predicates.
Splits on ACSL predicates do not try to split and reduce states in which the
predicate is already satisfied or refuted.
---
src/plugins/eva/partitioning/partition.ml | 33 ++++++++++++-----------
1 file changed, 18 insertions(+), 15 deletions(-)
diff --git a/src/plugins/eva/partitioning/partition.ml b/src/plugins/eva/partitioning/partition.ml
index bb041388413..4c8675e975e 100644
--- a/src/plugins/eva/partitioning/partition.ml
+++ b/src/plugins/eva/partitioning/partition.ml
@@ -470,21 +470,24 @@ struct
let states = function _ -> Abstract.Dom.top in
Abstract_domain.{ states; result = None }
in
- let source = fst (predicate.Cil_types.pred_loc) in
- let aux positive =
- let+ state' =
- Abstract.Dom.reduce_by_predicate env state predicate positive in
- let x = Abstract.Dom.evaluate_predicate env state' predicate in
- if x == Unknown
- then begin
- Self.warning ~source ~once:true
- "failing to learn perfectly from split predicate";
- if Abstract.Dom.equal state' state then raise Operation_failed
- end;
- let value = if positive then Integer.one else Integer.zero in
- value, state'
- in
- Bottom.list_values [ aux true; aux false ]
+ match Abstract.Dom.evaluate_predicate env state predicate with
+ | True -> [ Integer.one, state ]
+ | False -> [ Integer.zero, state ]
+ | Unknown ->
+ let source = fst (predicate.Cil_types.pred_loc) in
+ let aux positive =
+ let+ state' =
+ Abstract.Dom.reduce_by_predicate env state predicate positive in
+ let x = Abstract.Dom.evaluate_predicate env state' predicate in
+ if x == Unknown
+ then
+ Self.warning ~source ~once:true
+ "failing to learn perfectly from split predicate";
+ if Abstract.Dom.equal state' state then raise Operation_failed;
+ let value = if positive then Integer.one else Integer.zero in
+ value, state'
+ in
+ Bottom.list_values [ aux true; aux false ]
(* --- Applying partitioning actions onto flows --------------------------- *)
--
GitLab