From ae0cbc8af5382ee24d452a652491a13784265220 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Fri, 10 Dec 2021 22:08:56 +0100
Subject: [PATCH] [Eva] multidim: accept array iterations through *(p + i)
---
.../abstract_interp/abstract_memory.ml | 40 ++++++++++++++-----
.../abstract_interp/abstract_offset.ml | 32 ++++++++++++++-
.../abstract_interp/abstract_offset.mli | 1 +
src/plugins/value/domains/multidim_domain.ml | 12 +++++-
tests/value/multidim.c | 12 ++++++
tests/value/oracle/multidim.res.oracle | 34 ++++++++++++----
6 files changed, 111 insertions(+), 20 deletions(-)
diff --git a/src/kernel_services/abstract_interp/abstract_memory.ml b/src/kernel_services/abstract_interp/abstract_memory.ml
index dc13f84d1de..cb1d202d3d5 100644
--- a/src/kernel_services/abstract_interp/abstract_memory.ml
+++ b/src/kernel_services/abstract_interp/abstract_memory.ml
@@ -796,11 +796,23 @@ struct
and u2 = Option.get (Ival.max_int i2) in
Const (Integer.max u1 u2)
+ exception NoBound
+
let lower_const ~oracle b =
- Const (Option.get (Ival.min_int (to_ival ~oracle b))) (* TODO: handle exception *)
+ match Ival.min_int (to_ival ~oracle b) with
+ | Some l -> Const l
+ | None -> (* TODO: handle exception *)
+ Kernel.feedback ~current:true "cannot retrieve lower bound for %a in %a"
+ pretty b Ival.pretty (to_ival ~oracle b);
+ raise NoBound
let upper_const ~oracle b =
- Const (Option.get (Ival.min_int (to_ival ~oracle b))) (* TODO: handle exception *)
+ match Ival.max_int (to_ival ~oracle b) with
+ | Some u -> Const u
+ | None -> (* TODO: handle exception *)
+ Kernel.feedback ~current:true "cannot retrieve upper bound for %a in %a"
+ pretty b Ival.pretty (to_ival ~oracle b);
+ raise NoBound
let _operators oracle = operators (cmp ~oracle)
end
@@ -1526,15 +1538,23 @@ struct
let array_value = A.unify ~oracle aux a1.array_value a2.array_value in
Array { a1 with array_value }
| Array a, Raw b ->
- let array_value' = raw_to_array ~oracle Left a.array_value b in
- let array_value = A.unify ~oracle aux a.array_value array_value' in
- debug demerging "emerging unification between@.%a and@.%a result:@.%a" A.pretty a.array_value A.pretty array_value' A.pretty array_value;
- Array { a with array_value }
+ begin try
+ let array_value' = raw_to_array ~oracle Left a.array_value b in
+ let array_value = A.unify ~oracle aux a.array_value array_value' in
+ debug demerging "emerging unification between@.%a and@.%a result:@.%a" A.pretty a.array_value A.pretty array_value' A.pretty array_value;
+ Array { a with array_value }
+ with Bound.NoBound ->
+ weak_erase b m1 (* TODO: find a better way to handle this case *)
+ end
| Raw b, Array a ->
- let array_value' = raw_to_array ~oracle Right a.array_value b in
- let array_value = A.unify ~oracle aux array_value' a.array_value in
- debug demerging "emerging unification between@.%a and@.%a result:@.%a" A.pretty array_value' A.pretty a.array_value A.pretty array_value;
- Array { a with array_value }
+ begin try
+ let array_value' = raw_to_array ~oracle Right a.array_value b in
+ let array_value = A.unify ~oracle aux array_value' a.array_value in
+ debug demerging "emerging unification between@.%a and@.%a result:@.%a" A.pretty array_value' A.pretty a.array_value A.pretty array_value;
+ Array { a with array_value }
+ with Bound.NoBound ->
+ weak_erase b m2 (* TODO: find a better way to handle this case *)
+ end
| Struct s1, Struct s2 when are_structs_compatible s1 s2 ->
let struct_value = S.unify aux s1.struct_value s2.struct_value in
Struct { s1 with struct_value }
diff --git a/src/kernel_services/abstract_interp/abstract_offset.ml b/src/kernel_services/abstract_interp/abstract_offset.ml
index 2b546b54f12..84e6056507e 100644
--- a/src/kernel_services/abstract_interp/abstract_offset.ml
+++ b/src/kernel_services/abstract_interp/abstract_offset.ml
@@ -25,7 +25,8 @@ sig
type t
val pretty : Format.formatter -> t -> unit
- val append : t -> t -> t (* Does not check that the appened offset fits *)
+ val append : t -> t -> t
+ val add_index : (Cil_types.exp -> Int_val.t) -> t -> Cil_types.exp -> t
val join : t -> t -> t
val of_cil_offset : (Cil_types.exp -> Int_val.t) -> Cil_types.typ -> Cil_types.offset -> t
val of_ival : base_typ:Cil_types.typ -> typ:Cil_types.typ -> Ival.t -> t
@@ -63,6 +64,28 @@ struct
| Field (fi, s) -> Field (fi, append s o2)
| Index (e, i, t, s) -> Index (e, i, t, append s o2)
+ let add_index oracle base exp =
+ let rec aux = function
+ | NoOffset _ -> assert false
+ | Field (fi, s) -> Field (fi, aux s)
+ | Index (e, i, t, (NoOffset _ as s)) ->
+ begin
+ let idx' = Int_val.add i (oracle exp) in
+ let loc = Cil_datatype.Location.unknown in
+ let e = match e with (* If i is singleton, we can use this as the index expression *)
+ | None when Int_val.is_singleton i ->
+ let loc = Cil_datatype.Location.unknown in
+ Some (Cil.kinteger64 ~loc (Int_val.project_int i))
+ | e -> e
+ in
+ let e' = Option.map (Fun.flip (Cil.mkBinOp ~loc Cil_types.PlusA) exp) e in
+ (* TODO: is idx inside bounds ? *)
+ Index (e', idx', t, s)
+ end
+ | Index (e, i, t, s) -> Index (e, i, t, aux s)
+ in
+ aux base
+
let rec join o1 o2 =
match o1, o2 with
| NoOffset t, NoOffset t'
@@ -127,7 +150,7 @@ struct
let elem_size = Integer.of_int (Cil.bitsSizeOf elem_typ) in
if Integer.is_zero elem_size then (* array of elements of size 0 *)
if Int_val.is_zero ival then (* the whole range is valid *)
- let range = (array_range array_size) in
+ let range = array_range array_size in
Extlib.the ~exn:Abstract_interp.Error_Top range, ival
else (* Non-zero offset cannot represent anything here *)
raise Abstract_interp.Error_Top
@@ -245,6 +268,11 @@ struct
| `Top, _ | _, `Top -> `Top
| `Value o1, `Value o2 -> `Value (TypedOffset.append o1 o2)
+ let add_index oracle base exp =
+ match base with
+ | `Top -> `Top
+ | `Value base -> `Value (TypedOffset.add_index oracle base exp)
+
let join o1 o2 =
match o1, o2 with
| `Top, _ | _, `Top -> `Top
diff --git a/src/kernel_services/abstract_interp/abstract_offset.mli b/src/kernel_services/abstract_interp/abstract_offset.mli
index 5b2dc622609..64638b2bd04 100644
--- a/src/kernel_services/abstract_interp/abstract_offset.mli
+++ b/src/kernel_services/abstract_interp/abstract_offset.mli
@@ -26,6 +26,7 @@ sig
val pretty : Format.formatter -> t -> unit
val append : t -> t -> t (* Does not check that the appened offset fits *)
+ val add_index : (Cil_types.exp -> Int_val.t) -> t -> Cil_types.exp -> t
val join : t -> t -> t
val of_cil_offset : (Cil_types.exp -> Int_val.t) -> Cil_types.typ -> Cil_types.offset -> t
val of_ival : base_typ:Cil_types.typ -> typ:Cil_types.typ -> Ival.t -> t
diff --git a/src/plugins/value/domains/multidim_domain.ml b/src/plugins/value/domains/multidim_domain.ml
index a6df4575f06..112b20da720 100644
--- a/src/plugins/value/domains/multidim_domain.ml
+++ b/src/plugins/value/domains/multidim_domain.ml
@@ -141,13 +141,23 @@ struct
| Var vi ->
Map.singleton (Base.of_varinfo vi) offset
| Mem exp ->
+ let exp, index = match exp.enode with
+ | BinOp (PlusPI, e1, e2, _typ) ->
+ e1, Some e2
+ | _ -> exp, None
+ in
let add base ival map =
let offset' : Offset.t =
match Base.typeof base with
| None -> `Top
| Some base_typ ->
let typ = Cil.typeOf_pointed (Cil.typeOf exp) in
- Offset.(append (of_ival ~base_typ ~typ ival) offset)
+ let base_offset = Offset.of_ival ~base_typ ~typ ival in
+ let base_offset = match index with
+ | None -> base_offset
+ | Some exp -> Offset.add_index oracle' base_offset exp
+ in
+ Offset.append base_offset offset
in
Map.add base offset' map
in
diff --git a/tests/value/multidim.c b/tests/value/multidim.c
index 9fea8b14e58..16853e329c4 100644
--- a/tests/value/multidim.c
+++ b/tests/value/multidim.c
@@ -158,6 +158,17 @@ void main7() {
}
}
+void main8(void) {
+ int t[10] = {0};
+ int *p = t;
+
+ for (int i = 0 ; i < 10 ; i++) {
+ *(p + i) = 1;
+ }
+
+ Frama_C_domain_show_each(t);
+}
+
void main(s x) {
main1(x);
main2();
@@ -166,4 +177,5 @@ void main(s x) {
main5();
main6();
main7();
+ main8();
}
diff --git a/tests/value/oracle/multidim.res.oracle b/tests/value/oracle/multidim.res.oracle
index 4bf906a8671..9d11b591920 100644
--- a/tests/value/oracle/multidim.res.oracle
+++ b/tests/value/oracle/multidim.res.oracle
@@ -9,7 +9,7 @@
z[0..3] ∈ {0}
nondet ∈ [--..--]
[eva] computing for function main1 <- main.
- Called from multidim.c:162.
+ Called from multidim.c:173.
[eva] multidim.c:39:
Frama_C_domain_show_each:
x : # cvalue: .t1[0].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
@@ -86,7 +86,7 @@
[eva] Recording results for main1
[eva] Done for function main1
[eva] computing for function main2 <- main.
- Called from multidim.c:163.
+ Called from multidim.c:174.
[eva] multidim.c:55: starting to merge loop iterations
[eva:alarm] multidim.c:58: Warning: check got status unknown.
[eva] multidim.c:59:
@@ -96,7 +96,7 @@
[eva] Recording results for main2
[eva] Done for function main2
[eva] computing for function main3 <- main.
- Called from multidim.c:164.
+ Called from multidim.c:175.
[eva] multidim.c:64: starting to merge loop iterations
[eva] multidim.c:63: starting to merge loop iterations
[kernel] multidim.c:65:
@@ -137,7 +137,7 @@
[kernel] multidim.c:66: more than 1(28) elements to enumerate. Approximating.
[eva] Done for function main3
[eva] computing for function main4 <- main.
- Called from multidim.c:165.
+ Called from multidim.c:176.
[eva:loop-unroll:partial] multidim.c:81: loop not completely unrolled
[eva] multidim.c:81: starting to merge loop iterations
[eva] multidim.c:83: starting to merge loop iterations
@@ -148,7 +148,7 @@
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main5 <- main.
- Called from multidim.c:166.
+ Called from multidim.c:177.
[eva] multidim.c:96: starting to merge loop iterations
[eva] multidim.c:106:
Frama_C_domain_show_each:
@@ -163,7 +163,7 @@
[eva] Recording results for main5
[eva] Done for function main5
[eva] computing for function main6 <- main.
- Called from multidim.c:167.
+ Called from multidim.c:178.
[eva] multidim.c:114: Trace partitioning superposing up to 100 states
[eva] multidim.c:118:
Frama_C_domain_show_each:
@@ -181,7 +181,7 @@
[eva] Recording results for main6
[eva] Done for function main6
[eva] computing for function main7 <- main.
- Called from multidim.c:168.
+ Called from multidim.c:179.
[eva] multidim.c:134: starting to merge loop iterations
[kernel] multidim.c:136:
more than 1(1000) locations to update in array. Approximating.
@@ -215,6 +215,15 @@
[kernel] multidim.c:136: more than 1(1000) elements to enumerate. Approximating.
[kernel] multidim.c:137: more than 1(1000) elements to enumerate. Approximating.
[eva] Done for function main7
+[eva] computing for function main8 <- main.
+ Called from multidim.c:180.
+[eva] multidim.c:165: starting to merge loop iterations
+[eva] multidim.c:169:
+ Frama_C_domain_show_each:
+ t : # cvalue: {0; 1}
+ # multidim: { [0 .. 9] = {1}, [10 .. 9] = {0} }
+[eva] Recording results for main8
+[eva] Done for function main8
[eva] Recording results for main
[eva] done for function main
[kernel] multidim.c:50: more than 1(28) elements to enumerate. Approximating.
@@ -245,6 +254,9 @@
t[0].typ ∈ {1; 2} or UNINITIALIZED
{[0].val; [1..999]} ∈ [--..--] or UNINITIALIZED
j ∈ [0..999]
+[eva:final-states] Values at end of function main8:
+ t[0..9] ∈ {0; 1}
+ p ∈ {{ &t[0] }}
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
z[0..3] ∈ [--..--]
@@ -276,6 +288,8 @@
[kernel] multidim.c:141:
more than 1(1000) dependencies to update. Approximating.
[from] Done for function main7
+[from] Computing for function main8
+[from] Done for function main8
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
@@ -300,6 +314,8 @@
NO EFFECTS
[from] Function main7:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] Function main8:
+ NO EFFECTS
[from] Function main:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
z[0..3] FROM \nothing
@@ -332,6 +348,10 @@
Frama_C_entropy_source; t[0..999]; i; j
[inout] Inputs for function main7:
Frama_C_entropy_source; nondet
+[inout] Out (internal) for function main8:
+ t[0..9]; p; i
+[inout] Inputs for function main8:
+ \nothing
[inout] Out (internal) for function main:
Frama_C_entropy_source; z[0..3]
[inout] Inputs for function main:
--
GitLab