From deaf811571d0efadd26f55fd181ec9c0135ebfab Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 16 Dec 2020 12:26:31 +0100
Subject: [PATCH] [Eva] Improves the evaluation of ACSL quantifications.
---
src/plugins/value/legacy/eval_terms.ml | 53 ++++++++++++++++++++++----
1 file changed, 45 insertions(+), 8 deletions(-)
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 5de658b98e5..4aa65ced1f4 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -335,6 +335,25 @@ let bind_logic_vars env lvs =
let state, logic_vars = List.fold_left bind_one (state, env.logic_vars) lvs in
overwrite_current_state { env with logic_vars } state
+let copy_logic_vars ~src ~dst lvars =
+ let copy_one env lvar =
+ match Logic_utils.unroll_type lvar.lv_type with
+ | Linteger | Lreal ->
+ let value = LogicVarEnv.find lvar src.logic_vars in
+ let logic_vars = LogicVarEnv.add lvar value env.logic_vars in
+ { env with logic_vars }
+ | _ ->
+ try
+ let base, _ = c_logic_var lvar in
+ match Model.find_base base (env_current_state src) with
+ | `Bottom | `Top -> env
+ | `Value offsm ->
+ let state = Model.add_base base offsm (env_current_state env) in
+ overwrite_current_state env state
+ with Cil.SizeOfError _ -> unsupported_lvar lvar
+ in
+ List.fold_left copy_one dst lvars
+
let unbind_logic_vars env lvs =
let unbind_one (state, logic_vars) lv =
match Logic_utils.unroll_type lv.lv_type with
@@ -2417,14 +2436,32 @@ and eval_predicate env pred =
| Pforall (varl, p') | Pexists (varl, p') ->
begin
- try
- let env = bind_logic_vars env varl in
- let r = do_eval env p' in
- match p.pred_content with
- | Pexists _ -> if r = False then False else Unknown
- | Pforall _ -> if r = True then True else Unknown
- | _ -> assert false
- with LogicEvalError _ee -> Unknown (* No error display? *)
+ (* If [p'] is true (or false) for all possible values of [varl],
+ then so is Pforall(varl, p') and Pexists(varl, p'). *)
+ let env = bind_logic_vars env varl in
+ let r = do_eval env p' in
+ if r <> Unknown then r else
+ (* Otherwise:
+ - if [p'] evaluates to [false] for at least some values of [varl],
+ then Pforall (varl, p') is false.
+ - if [p'] evaluates to [true] for at least some values of [varl],
+ then Pexists (varl, p') is true.
+
+ In order to find such values, we reduce the environment by assuming
+ [p'] is true (for Pexists) or false (for Pforall), and then we
+ reevaluate [p'] with these values. *)
+ let positive =
+ match p.pred_content with Pforall _ -> false | _ -> true
+ in
+ let reduced_env = reduce_by_predicate ~alarm_mode env positive p' in
+ (* Reduce the values of logical variables [varl] in [env] according to
+ [reduced_env]. To be more precise, we could reduce them to
+ singleton values — for instance by using the interval bounds. *)
+ let env = copy_logic_vars ~src:reduced_env ~dst:env varl in
+ match p.pred_content, do_eval env p' with
+ | Pexists _, True -> True
+ | Pforall _, False -> False
+ | _ -> Unknown
end
| Pnot p -> begin match do_eval env p with
--
GitLab