diff --git a/src/kernel_services/abstract_interp/abstract_memory.ml b/src/kernel_services/abstract_interp/abstract_memory.ml
index 687d64d5f8fdce1870017ab5e3e0bd03e8fccc3a..3e2538f1a5972be3fca6a4f9dcb8ea5f4fc46864 100644
--- a/src/kernel_services/abstract_interp/abstract_memory.ml
+++ b/src/kernel_services/abstract_interp/abstract_memory.ml
@@ -41,7 +41,7 @@ let pp_iter
?(pre=format_of_string "{@;<1 2>")
?(sep=format_of_string ",@;<1 2>")
?(suf=format_of_string "@ }")
- ?(format=format_of_string"@[<hv>%a@]")
+ ?(format=format_of_string "@[<hv>%a@]")
iter pp fmt v =
let need_sep = ref false in
Format.fprintf fmt pre;
@@ -49,10 +49,9 @@ let pp_iter
if !need_sep then Format.fprintf fmt sep else need_sep := true;
Format.fprintf fmt format pp v;
) v;
- Format.fprintf fmt suf;
-;;
+ Format.fprintf fmt suf
-let pp_iter2 ?pre ?sep ?suf ?(format=format_of_string "%a%a")
+let pp_iter2 ?pre ?sep ?suf ?(format=format_of_string "@[<hv>%a%a@]")
iter2 pp_key pp_val fmt v =
let iter f = iter2 (fun k v -> f (k,v)) in
let pp fmt (k,v) = Format.fprintf fmt format pp_key k pp_val v in
@@ -247,7 +246,7 @@ struct
type submemory = M.t
let pretty fmt m =
- pp_iter2 ~format:".%a%a" FieldMap.iter Field.pretty M.pretty fmt m.fields
+ pp_iter2 ~format:"@[<hv>.%a%a@]" FieldMap.iter Field.pretty M.pretty fmt m.fields
let hash m =
Hashtbl.hash (m.padding, FieldMap.hash m.fields)
@@ -440,10 +439,14 @@ struct
| Const _ -> Some b
| Exp (e, j) ->
let l = linearity vi e in
- Some (Exp (e, Integer.(sub j (mul l i))))
- | Ptroffset (e, b, j) ->
+ if Integer.is_zero l
+ then Some b
+ else Option.map (fun i -> Exp (e, Integer.(sub j (mul l i)))) i
+ | Ptroffset (e, base, j) ->
let l = linearity vi e in
- Some (Ptroffset (e, b, Integer.(sub j (mul l i))))
+ if Integer.is_zero l
+ then Some b
+ else Option.map (fun i -> Ptroffset (e, base, Integer.(sub j (mul l i)))) i
with NonLinear -> None
(* Stupid oracle built from an Ival oracle *)
@@ -506,7 +509,7 @@ sig
val is_included : t -> t -> bool
val unify : oracle:bioracle -> (submemory -> submemory -> submemory) ->
t -> t -> t
- val singleton : bit -> bound -> bound -> submemory -> t
+ val single : bit -> bound -> bound -> submemory -> t
val read :
oracle:(Cil_types.exp -> Ival.t) ->
(submemory -> 'a) -> ('a -> 'a -> 'a) -> t -> bound -> 'a
@@ -722,7 +725,7 @@ struct
padding = Bit.join p1 p2 ;
}
- let singleton padding lindex uindex value =
+ let single padding lindex uindex value =
{
padding ;
start = lindex ;
@@ -757,7 +760,7 @@ struct
1. reinforcement without loss
2. weak update without singularization
3. update reduces the number of segments to 3 *)
- let write ~oracle f m lindex uindex =
+ let write ~oracle f m lindex uindex = (* lindex < uindex *)
let (<=) b1 b2 = match Bound.cmp ~oracle b1 b2 with
| Lower | Equal -> true
| Greater | Uncomparable -> false
@@ -765,26 +768,39 @@ struct
| Greater | Equal -> true
| Lower | Uncomparable -> false
in
+ (* (start,head) : segmentation kept identical below the write indexes,
+ head is a list in reverse order
+ (l,v,u) : the segment (l,u) beeing overwriten with previous value v
+
+ head = (_,l) :: _
+ *)
let rec aux_before l s =
+ (* Format.printf "aux before: %a@." pretty_segments (l,s); *)
if lindex >= l
then aux_below l [] l s
else aux_over lindex [] lindex (M.of_raw m.padding) l s
- and aux_below start head l = function (* l < index *)
+ and aux_below start head l = fun t ->
+ (* Format.printf "aux_below: %a [%a] %a@." pretty_segments (start,head) Bound.pretty l pretty_segments (l,t); *)
+ match t with (* l <= lindex *)
| [] ->
aux_end start head l (M.of_raw m.padding) uindex []
| (v,u) :: t ->
if lindex >= u
then aux_below start ((v,u) :: head) u t
else aux_over start head l v u t
- and aux_over start head l v u = function (* l >= index *)
- | [] ->
- aux_end start head l (M.smash ~oracle v (M.of_raw m.padding)) uindex []
- | ((v',u') :: t) as s ->
- if uindex <= u'
- then aux_end start head l v u s
- (* TODO: do not smash if the slices are covered by the write *)
- else aux_over start head l (M.smash ~oracle v v') u' t
- and aux_end start head l v u tail =
+ and aux_over start head l v u s = (* l <= lindex *)
+ (* Format.printf "aux_over: %a [%a,%a,%a] %a@." pretty_segments (start,head) Bound.pretty l M.pretty v Bound.pretty u pretty_segments (u,s); *)
+ if uindex <= u then
+ aux_end start head l v u s
+ else
+ match s with
+ | [] ->
+ aux_end start head l (M.smash ~oracle v (M.of_raw m.padding)) uindex []
+ | (v',u') :: t ->
+ (* TODO: do not smash if the slices are covered by the write *)
+ aux_over start head l (M.smash ~oracle v v') u' t
+ and aux_end start head l v u tail = (* l <= lindex < uindex <= u*)
+ (* Format.printf "aux_end: %a [%a,%a,%a] %a@." pretty_segments (start,head) Bound.pretty l M.pretty v Bound.pretty u pretty_segments (u,tail); *)
let tail' =
(if is_empty_segment ~oracle l lindex then [] else [(v,lindex)]) @
[(f v,uindex)] @
@@ -803,7 +819,7 @@ struct
let rec aux acc = function
| [] -> acc
| (v,u) :: t ->
- match Option.bind x (fun x -> Bound.incr vi x u) with
+ match Bound.incr vi x u with
| Some u -> aux ((v,u) :: acc) t
| None ->
match t with
@@ -814,7 +830,7 @@ struct
| (v',u') :: t -> aux ((M.smash ~oracle v v',u') :: acc) t
in
let start, segments =
- match Option.bind x (fun x -> Bound.incr vi x m.start) with
+ match Bound.incr vi x m.start with
| Some start -> start, m.segments
| None ->
match m.segments with
@@ -905,7 +921,8 @@ struct
Format.fprintf fmt "%a" A.pretty a.array_value
let pretty fmt m = pp ~root:false fmt m
- let pretty_root fmt m = pp ~root:true fmt m
+ let pretty_root fmt m =
+ Format.fprintf fmt "@[<hv>%a@]" (pp ~root:true) m
let rec hash m = match m with
| Raw b -> Hashtbl.hash (
@@ -1114,21 +1131,20 @@ struct
let l, u = Int_val.min_and_max index in
let l = Option.get l and u = Option.get u in (* TODO: handle exceptions *)
Bound.of_integer l, Bound.of_integer u,
- weak || Integer.(equal (succ l) u)
+ weak || Integer.equal l u
| Some e ->
let b = Bound.of_exp e in
- b, Bound.succ b, weak
+ b, b, weak
in
match m with
| Array a when are_typ_compatible a.array_cell_type elem_type ->
- let array_value =
- A.write ~oracle (aux ~weak offset') a.array_value lindex uindex
- in
+ let array_value = A.write ~oracle (aux ~weak offset') a.array_value
+ lindex (Bound.succ uindex) in
Array { a with array_value }
| _ ->
let b = raw m in
let new_value = aux ~weak offset' (Raw b) in
- let array_value = A.singleton b lindex uindex new_value in
+ let array_value = A.single b lindex (Bound.succ uindex) new_value in
Array { array_cell_type = elem_type ; array_value }
in aux
@@ -1169,19 +1185,30 @@ struct
read ~oracle to_value V.join loc m
let extract ~oracle (m : t) (loc : location) : t =
- read ~oracle (fun _typ x -> x) (smash ~oracle) loc m
+ let r = read ~oracle (fun _typ x -> x) (smash ~oracle) loc m in
+ (* Format.printf "extract %a in %a : %a@." TypedOffset.pretty loc pretty m pretty r; *)
+ r
let set ~oracle ~weak m offset new_v =
let f ~weak typ m =
of_value typ (if weak then V.join (to_value typ m) new_v else new_v)
in
- write ~oracle ~weak f offset m
+ let r = write ~oracle ~weak f offset m in
+ (* Format.printf "%a <- %a : %a@." TypedOffset.pretty offset V.pretty new_v pretty r; *)
+ r
+
+ let join ~oracle m1 m2 =
+ let r = join ~oracle m1 m2 in
+ (* Format.printf "%a join %a : %a@." pretty m1 pretty m2 pretty r; *)
+ r
let reinforce ~oracle f m offset =
let f' ~weak typ m =
if weak then m else of_value typ (f (to_value typ m))
in
- write ~oracle ~weak:false f' offset m
+ let r = write ~oracle ~weak:false f' offset m in
+ (* Format.printf "reinforce at %a : %a@." TypedOffset.pretty offset pretty r; *)
+ r
let erase ~oracle ~weak m offset b =
let f ~weak _typ m =
diff --git a/tests/value/multidim.c b/tests/value/multidim.c
index c958cd19a1464b6a8d9cea7759a06fa802661df5..9d941f69452fa42871d135f382cf46cd4e51234d 100644
--- a/tests/value/multidim.c
+++ b/tests/value/multidim.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +"-eva-msg-key d-multidim -eva-domains multidim -eva-plevel 0"
+ STDOPT: +"-eva-msg-key d-multidim -eva-domains multidim -eva-plevel 1"
*/
#include "__fc_builtin.h"
#define N 4
@@ -42,14 +42,13 @@ void main(s x) {
/* The multidim domain wont infer anything except the structure from the
assign: it considers x can contain anything including pointers, and thus no
reduction is done by are_finite */
- //@ assert \are_finite(x.t1[..].f) && \are_finite(x.t2[..].f);
+ //@ admit \are_finite(x.t1[..].f) && \are_finite(x.t2[..].f);
Frama_C_domain_show_each(x);
f();
- Frama_C_domain_show_each(z);
-
+ Frama_C_domain_show_each(z);
/* The multidim domain doesn't implement forward logic yet */
- //@ assert \are_finite(z[..].t1[..].f) && \are_finite(z[..].t2[..].f);
+ //@ check \are_finite(z[..].t1[..].f) && \are_finite(z[..].t2[..].f);
for (int i = 0 ; i < M ; i ++) {
for (int j = 0 ; j < N ; j ++) {
@@ -64,3 +63,15 @@ void main(s x) {
Frama_C_domain_show_each(t1);
}
+
+void main2(void) {
+ int t[10] = {0};
+ Frama_C_domain_show_each_begin(t);
+ for (int i = 0 ; i < 10 ; i++) {
+ Frama_C_domain_show_each_before(i, t);
+ t[i] = 1;
+ Frama_C_domain_show_each_after(i, t);
+ }
+ Frama_C_domain_show_each(t);
+ //@ check t[0..9] == 1;
+}
diff --git a/tests/value/oracle/multidim.res.oracle b/tests/value/oracle/multidim.res.oracle
index fb1fde102da153e21bf7c4e8e714252e6f351a6c..9e283f9be301248921b7903f324c2d945be798bb 100644
--- a/tests/value/oracle/multidim.res.oracle
+++ b/tests/value/oracle/multidim.res.oracle
@@ -10,24 +10,36 @@
z[0..3] ∈ {0}
w[0..3] ∈ {0}
nondet ∈ [--..--]
-[kernel] multidim.c:33: too many locations to update in array. Approximating.
[eva] multidim.c:40:
Frama_C_domain_show_each:
x : # cvalue: .t1[0].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
.t1[0].i ∈ [--..--]
.t1[1].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
.t1[1].i ∈ [--..--]
- .t1[2..3]{.f#; .i#} ∈ [0..18446744073701163007] repeated %64
+ .t1[2].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ .t1[2].i ∈ [--..--]
+ .t1[3].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ .t1[3].i ∈ [--..--]
.t2[0].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
.t2[0].i ∈ [--..--]
.t2[1].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
.t2[1].i ∈ [--..--]
- .t2[2..3]{.f#; .i#} ∈ [0..18446744073701163007] repeated %64
+ .t2[2].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ .t2[2].i ∈ [--..--]
+ .t2[3].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ .t2[3].i ∈ [--..--]
# multidim: T
y1 : # cvalue: .t1[0].f ∈ {3.}
{.t1{[0].i; [1..3]}; .t2[0..3]} ∈ {0}
- # multidim: { .t1[0] = { .f = [0. .. 3.], .i = {0} }, .t2[0..3] = {
- .f = {0}, .i = {0} } }
+ # multidim: {
+ .t1[0] = { .f = {3.}, .i = {0} },
+ .t2{
+ [0] = { .f = {0}, .i = {0} },
+ [1] = { .f = {0}, .i = {0} },
+ [2] = { .f = {0}, .i = {0} },
+ [3] = { .f = {0}, .i = {0} }
+ }
+ }
y2 : # cvalue: .t1[0].f ∈ {4.} or UNINITIALIZED
{.t1{[0].i; [1..3]}; .t2[0..3]} ∈ UNINITIALIZED
# multidim: { .t1[0] = { .f = {4.} } }
@@ -35,21 +47,28 @@
# multidim: 0
w : # cvalue: {0}
# multidim: 0
-[eva:alarm] multidim.c:45: Warning: assertion got status unknown.
[eva] multidim.c:46:
Frama_C_domain_show_each:
x : # cvalue: .t1[0].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
.t1[0].i ∈ [--..--]
.t1[1].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
.t1[1].i ∈ [--..--]
- .t1[2..3]{.f#; .i#} ∈ [0..18446744073701163007] repeated %64
+ .t1[2].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ .t1[2].i ∈ [--..--]
+ .t1[3].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ .t1[3].i ∈ [--..--]
.t2[0].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
.t2[0].i ∈ [--..--]
.t2[1].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
.t2[1].i ∈ [--..--]
- .t2[2..3]{.f#; .i#} ∈ [0..18446744073701163007] repeated %64
- # multidim: { .t1[0..2] = { .f = {{ ANYTHING }} }, .t2[0..2] = {
- .f = {{ ANYTHING }} } }
+ .t2[2].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ .t2[2].i ∈ [--..--]
+ .t2[3].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ .t2[3].i ∈ [--..--]
+ # multidim: {
+ .t1[0..3] = { .f = {{ ANYTHING }} },
+ .t2[0..3] = { .f = {{ ANYTHING }} }
+ }
[eva] computing for function f <- main.
Called from multidim.c:48.
[eva] using specification for function f
@@ -57,47 +76,53 @@
[eva] multidim.c:49:
Frama_C_domain_show_each:
z : # cvalue: [--..--]
- # multidim: [0..2] = { .t1[0..2] = { .f = T }, .t2[0..2] = {
- .f = [-3.40282346639e+38 .. 3.40282346639e+38] } }
-[eva:alarm] multidim.c:52: Warning: assertion got status unknown.
-[eva] multidim.c:55: starting to merge loop iterations
+ # multidim: [0..3] = {
+ .t1[0..3] = {
+ .f = [-3.40282346639e+38 .. 3.40282346639e+38]
+ },
+ .t2[0..3] = {
+ .f = [-3.40282346639e+38 .. 3.40282346639e+38]
+ }
+ }
+[eva:alarm] multidim.c:51: Warning: check got status unknown.
[eva] multidim.c:54: starting to merge loop iterations
+[eva] multidim.c:53: starting to merge loop iterations
+[kernel] multidim.c:55:
+ more than 1(20) locations to update in array. Approximating.
[kernel] multidim.c:56:
- more than 0(20) locations to update in array. Approximating.
-[kernel] multidim.c:57:
- more than 0(20) locations to update in array. Approximating.
+ more than 1(20) locations to update in array. Approximating.
+[kernel] multidim.c:55:
+ more than 1(28) locations to update in array. Approximating.
[kernel] multidim.c:56:
- more than 0(28) locations to update in array. Approximating.
-[kernel] multidim.c:57:
- more than 0(28) locations to update in array. Approximating.
-[eva] multidim.c:61:
+ more than 1(28) locations to update in array. Approximating.
+[eva] multidim.c:60:
Frama_C_domain_show_each:
w : # cvalue: [0].t1[0].f ∈ [0. .. 2.]
{[0]{.t1{[0].i; [1..3]}; .t2[0..3]}; [1..2]; [3].t1{[0..2]; [3].f}} ∈
[--..--]
[3].t1[3].i ∈ {0; 2}
[3].t2[0..3] ∈ {0}
- # multidim: [0..3] = { .t1[0..3] = { .f = [0. .. 2.], .i = {0; 2} } }
+ # multidim: [0..3] = { .t1[-1..3] = { .f = [0. .. 2.], .i = {0; 2} } }
[eva] computing for function Frama_C_interval <- main.
- Called from multidim.c:63.
+ Called from multidim.c:62.
[eva] using specification for function Frama_C_interval
-[eva] multidim.c:63:
+[eva] multidim.c:62:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- main.
- Called from multidim.c:63.
-[eva] multidim.c:63:
+ Called from multidim.c:62.
+[eva] multidim.c:62:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
-[eva] multidim.c:65:
+[eva] multidim.c:64:
Frama_C_domain_show_each:
t1 : # cvalue: [--..--]
- # multidim: [--..--]
+ # multidim: T
[eva] Recording results for main
-[kernel] multidim.c:56: more than 0(28) elements to enumerate. Approximating.
-[kernel] multidim.c:57: more than 0(28) elements to enumerate. Approximating.
+[kernel] multidim.c:55: more than 1(28) elements to enumerate. Approximating.
+[kernel] multidim.c:56: more than 1(28) elements to enumerate. Approximating.
[eva] done for function main
-[kernel] multidim.c:52: more than 0(28) elements to enumerate. Approximating.
+[kernel] multidim.c:51: more than 1(28) elements to enumerate. Approximating.
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
@@ -115,8 +140,8 @@
[from] Computing for function main
[from] Computing for function f <-main
[from] Done for function f
-[kernel] multidim.c:56: more than 0(28) dependencies to update. Approximating.
-[kernel] multidim.c:57: more than 0(28) dependencies to update. Approximating.
+[kernel] multidim.c:55: more than 1(28) dependencies to update. Approximating.
+[kernel] multidim.c:56: more than 1(28) dependencies to update. Approximating.
[from] Computing for function Frama_C_interval <-main
[from] Done for function Frama_C_interval
[from] Done for function main