From bf21b4410770d96e349db359ac13f02c42c58597 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 2 Aug 2019 10:40:08 +0200
Subject: [PATCH] [Eva] Auto loop unroll: new strategy to reduce an expression
from a condition.
Relies on the computation of the mathematical complement of ival.
---
.../value/partitioning/auto_loop_unroll.ml | 50 ++++++++++++++-----
1 file changed, 38 insertions(+), 12 deletions(-)
diff --git a/src/plugins/value/partitioning/auto_loop_unroll.ml b/src/plugins/value/partitioning/auto_loop_unroll.ml
index 384533297e5..37e2b81bbcb 100644
--- a/src/plugins/value/partitioning/auto_loop_unroll.ml
+++ b/src/plugins/value/partitioning/auto_loop_unroll.ml
@@ -233,6 +233,17 @@ module Make (Abstract: Abstractions.Eva) = struct
let (>>) v f = match v with `Value v -> f v | _ -> None
let (>>=) v f = match v with Some v -> f v | None -> None
+ let cvalue_complement typ cvalue =
+ let open Eval_typ in
+ match Eval_typ.classify_as_scalar typ with
+ | Some (TSFloat _ | TSPtr _) | None -> None
+ | Some (TSInt ik) ->
+ try
+ let ival = Cvalue.V.project_ival cvalue in
+ Ival.complement_int_under ~size:ik.i_bits ~signed:ik.i_signed ival
+ >> fun ival -> Some (Cvalue.V.inject_ival ival)
+ with Cvalue.V.Not_based_on_null -> None
+
(* Reduces the condition "[condition] = [positive]" to a sufficient hypothesis
on the value of the expression [expr]: computes a value [v] such that
if the expression [expr] evaluates to [v], then [condition] = [positive].
@@ -241,18 +252,33 @@ module Make (Abstract: Abstractions.Eva) = struct
and in the given valuation. *)
let reduce_to_expr valuation ~expr ~condition ~positive =
let state = Abstract.Dom.top in
- (* Assumes that the [condition] is [positive]. *)
- fst (Eval.reduce ~valuation state condition positive)
- >> fun resulting_valuation ->
- (* Finds the value of [expr] in the resulting valuation. *)
- Valuation.find resulting_valuation expr >> fun record ->
- record.value.v >> fun value ->
- (* If the value of [expr] is top, no reduction has been performed. *)
- if Val.(equal top value) then None
- else
- (* Otherwise, re-evaluate the condition with the hypothesis that [expr]
- evaluates to [value]. If the condition is satisfied, then
- [expr] ∈ [value] ⇒ [condition] = [positive]. *)
+ (* Reduces [expr] by assuming that [condition] is [positive]. *)
+ let reduce positive =
+ (* Assumes that [condition] is [positive]. *)
+ fst (Eval.reduce ~valuation state condition positive) >> fun valuation ->
+ (* Finds the value of [expr] in the resulting valuation. *)
+ Valuation.find valuation expr >> fun record ->
+ record.value.v >> fun value ->
+ (* If the new value of [expr] is top, no reduction has been performed. *)
+ if Val.(equal top value) then None else Some (value, record)
+ in
+ (* Different strategies whether cvalue is present. *)
+ match Val.get Main_values.CVal.key with
+ | Some get_cvalue ->
+ (* Assumes that [condition] is NOT [positive]. *)
+ reduce (not positive) >>= fun (value, _record) ->
+ (* [value] is an over-approximation of the values of [expr] for which
+ [condition] is NOT positive; its complement is an under-approximation
+ of the values for which [condition] is positive. *)
+ let cvalue = get_cvalue value in
+ cvalue_complement (Cil.typeOf expr) cvalue >>= fun cvalue ->
+ Some (Val.set Main_values.CVal.key cvalue Val.top)
+ | None ->
+ (* Assumes that [condition] is [positive]. Returns an over-approximation
+ of the values for which [condition] is [positive]. *)
+ reduce positive >>= fun (value, record) ->
+ (* Evaluates [condition] with the hypothesis [expr] ∈ [value], to check
+ whether [expr] ∈ [value] ⇒ [condition] = [positive]. *)
let valuation = Valuation.add valuation expr record in
fst (Eval.evaluate ~valuation ~reduction:false state condition)
>> fun (_valuation, v) ->
--
GitLab