From b29b107fc7b6a1f81675624aa83da13a6c4832ac Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 4 Mar 2024 15:22:54 +0100
Subject: [PATCH] [Eva] Fixes message about garbled mix generated by a
specification.
On assigns clause on struct, the message could be emitted even if no garbled
mix had been created, as the offsetmap for the struct was read as one cvalue,
which could be very imprecise.
Instead, this commit iters on the offsetmap and warn for each imprecise garbled
mix in the offsetmap, if any.
---
.../eva/engine/transfer_specification.ml | 19 +++++++++++--------
tests/libc/oracle/pwd_h.res.oracle | 6 ------
2 files changed, 11 insertions(+), 14 deletions(-)
diff --git a/src/plugins/eva/engine/transfer_specification.ml b/src/plugins/eva/engine/transfer_specification.ml
index eda7c02d067..c0520b22fcd 100644
--- a/src/plugins/eva/engine/transfer_specification.ml
+++ b/src/plugins/eva/engine/transfer_specification.ml
@@ -306,13 +306,15 @@ module Make
let env = make_env pre in
let assigns = get_assigns_for_behavior spec behavior in
let check_one_assign cvalue_state (assign, _) =
- match evaluate_location env retres_loc Assign assign with
- | None -> ()
- | Some location ->
- let loc = Precise_locs.imprecise_location (get_ploc location) in
- let cvalue = Cvalue.Model.find cvalue_state loc in
- begin
- match cvalue with
+ let location = evaluate_location env retres_loc Assign assign in
+ let precise_loc = Option.map get_ploc location in
+ let loc = Option.map Precise_locs.imprecise_location precise_loc in
+ match loc with
+ | None | Some Locations.{ size = Top } -> ()
+ | Some Locations.{ loc; size = Value size } ->
+ let offsm = Cvalue.Model.copy_offsetmap loc size cvalue_state in
+ let warn v =
+ match Cvalue.V_Or_Uninitialized.get_v v with
| Top (bases, origin) ->
if Origin.register_write bases origin then
Self.warning ~current:true ~once:true
@@ -321,7 +323,8 @@ module Make
a garbled mix of addresses@ for %a.@]"
Kernel_function.pretty kf pp_assign_clause (Assign, assign)
| _ -> ()
- end
+ in
+ Bottom.iter (Cvalue.V_Offsetmap.iter_on_values warn) offsm
in
let check_one_state state =
let cvalue_state = get_cvalue_or_top state in
diff --git a/tests/libc/oracle/pwd_h.res.oracle b/tests/libc/oracle/pwd_h.res.oracle
index 5dedb215f1a..6cdda1a2be9 100644
--- a/tests/libc/oracle/pwd_h.res.oracle
+++ b/tests/libc/oracle/pwd_h.res.oracle
@@ -7,9 +7,6 @@
[eva] computing for function getpwuid <- main.
Called from pwd_h.c:10.
[eva] using specification for function getpwuid
-[eva:garbled-mix:assigns] pwd_h.c:10:
- The specification of function getpwuid
- has generated a garbled mix of addresses for assigns clause __fc_pwd.
[eva] Done for function getpwuid
[eva:alarm] pwd_h.c:13: Warning: assertion got status unknown.
[eva:alarm] pwd_h.c:14: Warning: assertion got status unknown.
@@ -19,9 +16,6 @@
Called from pwd_h.c:18.
[eva] using specification for function getpwnam
[eva] pwd_h.c:18: function getpwnam: precondition 'valid_name' got status valid.
-[eva:garbled-mix:assigns] pwd_h.c:18:
- The specification of function getpwnam
- has generated a garbled mix of addresses for assigns clause __fc_pwd.
[eva] Done for function getpwnam
[eva:alarm] pwd_h.c:21: Warning: assertion got status unknown.
[eva:alarm] pwd_h.c:22: Warning: assertion got status unknown.
--
GitLab