diff --git a/.make-clean-stamp b/.make-clean-stamp
index 1e8b314962144c26d5e0e50fd29d2ca327864913..7f8f011eb73d6043d2e6db9d2c101195ae2801f2 100644
--- a/.make-clean-stamp
+++ b/.make-clean-stamp
@@ -1 +1 @@
-6
+7
diff --git a/Makefile b/Makefile
index a43ef03e10c0b48c1109d0bdb1f5708aa1e9d677..d1fda9f3240d09efbdd3bfb50ccf9c5e27728a66 100644
--- a/Makefile
+++ b/Makefile
@@ -803,6 +803,7 @@ KERNEL_CMO= \
src/memory_state/path_lattice.cmo \
src/memory_state/int_Interv.cmo \
src/memory_state/int_Interv_Map.cmo \
+ src/memory_state/tr_offset.cmo \
src/memory_state/new_offsetmap.cmo \
src/memory_state/offsetmap.cmo \
src/memory_state/offsetmap_bitwise.cmo \
diff --git a/src/memory_state/new_offsetmap.ml b/src/memory_state/new_offsetmap.ml
index 247874bf8c644befb068b023480c7f917f224b1b..05ed8e59f129689271004d86db4ec847cd7f2550 100644
--- a/src/memory_state/new_offsetmap.ml
+++ b/src/memory_state/new_offsetmap.ml
@@ -1156,69 +1156,10 @@ module Make (V : Lattice_With_Isotropy.S) = struct
(** Joining two trees with possible overlapping intervals *)
let join t1 t2 = merge f_join Int.zero t1 Int.zero t2 ;;
-
-
- (* Poached from orginal offsetmap
- *)
- type interval_or_set =
- | Set of Ival.O.t
- | Interval of
- Abstract_interp.Int.t * Abstract_interp.Int.t * Abstract_interp.Int.t
-
- let empty_interval_or_set = Set (Ival.O.empty)
-
- open CilE
-
- let reduce_ival_by_bound ~read ~with_alarms ival size bound_min bound_max =
- let max_in_bound =
- Abstract_interp.Int.succ (Abstract_interp.Int.sub bound_max size) in
- let is_in_bound x = match x with
- | Ival.Top (mn,mx,r,m) ->
- let out, new_mn =
- match mn with
- | Some mn when (Abstract_interp.Int.ge mn bound_min) -> false, mn
- | _ ->
- true,
- (Abstract_interp.Int.round_up_to_r ~r ~modu:m ~min:bound_min)
- in
- let out, new_mx =
- match mx with
- | Some mx when (Abstract_interp.Int.le mx max_in_bound) -> out, mx
- | _ ->
- true,
- (Abstract_interp.Int.round_down_to_r ~r ~modu:m
- ~max:max_in_bound)
- in
- if out then
- (if read
- then warn_mem_read with_alarms
- else warn_mem_write with_alarms);
- if Abstract_interp.Int.le new_mn new_mx
- then Interval(new_mn, new_mx, m)
- else empty_interval_or_set
- | _ -> assert false
- in
- match ival with
- | Ival.Top (_mn,_mx,_r,_m) -> is_in_bound ival
- | Ival.Float _ -> is_in_bound Ival.top
- | Ival.Set s ->
- Set(Ival.O.fold
- (fun offset acc ->
- let pseudo_interval =
- Ival.Top(Some offset,
- Some offset,
- Abstract_interp.Int.zero,
- Abstract_interp.Int.one)
- in
- match is_in_bound pseudo_interval with
- Interval _ -> Ival.O.add offset acc
- | _ -> acc)
- s
- Ival.O.empty)
- ;;
-
- (* Given an integer i -- the ith bit, find the interval it belongs to (thus its node)
- Returns: the zipper to navigate from the root to the node found and the node itself
+ (* Given an integer i,
+ find the interval the ith bit belongs to (thus its node)
+ Returns: the zipper to navigate from the root to the node found,
+ and the node itself
*)
exception Bit_Not_found
let find_bit_offset i zipper offset tree =
@@ -1407,8 +1348,9 @@ module Make (V : Lattice_With_Isotropy.S) = struct
let period_read_ahead = Int.from_big_int period_read_ahead in
let z, cur_off, root = find_bit offset64 tree in
match root with
- | Empty -> assert false
- (* Not_found has been raised by_find_bit in this case *)
+ | Empty ->
+ (* Bit_Not_found has been raised by find_bit in this case *)
+ assert false
| Node (max, _, _, _, _subr, rrel, m, v, _) ->
let r = Int.pos_rem (Int.add rrel cur_off) m in
let isize = Int.pred (Int.add offset64 size64) in
@@ -1457,26 +1399,17 @@ module Make (V : Lattice_With_Isotropy.S) = struct
(*
Finds the value associated to a set of bit offsets represented as an ival
*)
- let find_ival ~conflate_bottom ~validity ~with_alarms offsets tree size =
+ let find_ival ~conflate_bottom ~validity ~with_alarms ival tree size =
let filtered_by_bound =
- match validity with
- | Base.Known (bound_min,bound_max)
- | Base.Unknown (bound_min,bound_max)
- | Base.Periodic (bound_min,bound_max,_) ->
- reduce_ival_by_bound ~read:true ~with_alarms
- offsets size bound_min bound_max
- | Base.All -> begin
- match offsets with
- | Ival.Top (Some mn,Some mx,_r,m) -> Interval(mn, mx, m)
- | Ival.Top (None,_,_,_) | Ival.Top (_,None,_,_) |
- Ival.Float _ ->
- raise Not_found (* return top *)
- | Ival.Set o -> Set o
- end
+ try
+ Tr_offset.filter_by_bound_for_reading
+ ~with_alarms ival size validity
+ with
+ Tr_offset.Unbounded -> raise Not_found (* return top *)
in
let result =
match filtered_by_bound with
- | Interval(mn, mx, m) ->
+ | Tr_offset.Interval(mn, mx, m) ->
let r = Abstract_interp.Int.pos_rem mn m in
let mn = ref mn in
let acc = ref V.bottom in
@@ -1497,7 +1430,7 @@ module Make (V : Lattice_With_Isotropy.S) = struct
Abstract_interp.Int.max naive_next aligned_b
done;
!acc
- | Set s ->
+ | Tr_offset.Set s ->
Ival.O.fold
(fun offset acc ->
let _, new_value =
@@ -1506,13 +1439,16 @@ module Make (V : Lattice_With_Isotropy.S) = struct
in
let result = V.join acc new_value in
if V.equal result V.top then raise Not_found;
- result;
- ) s V.bottom
+ result)
+ s
+ V.bottom
+ | Tr_offset.Imprecise(_mn, _mx) ->
+ assert false
in result
;;
- (* Keep the tree under a given limit offset *)
+ (* Keep the part of the tree under a given limit offset *)
let rec keep_below offset curr_off tree =
match tree with
diff --git a/src/memory_state/offsetmap.ml b/src/memory_state/offsetmap.ml
index 80684984aeb4cf09871790f1ad8477056ed8c8cc..88bf93c4c97c280599eac9fce2eddae8e0e8c984 100644
--- a/src/memory_state/offsetmap.ml
+++ b/src/memory_state/offsetmap.ml
@@ -20,7 +20,6 @@
(* *)
(**************************************************************************)
-(* Offsets encoding *)
open Abstract_interp
open Abstract_value
open CilE
@@ -1220,135 +1219,6 @@ let reciprocal_image m base =
else
add_approximate_including_spaces mn mx r m size v existing_offsetmap
- type interval_or_set =
- Set of Ival.O.t
- | Interval of Int.t * Int.t * Int.t
- | Imprecise of Int.t * Int.t
-
- let empty_interval_or_set = Set (Ival.O.empty)
-
- exception Unbounded
-
- let reduce_ival_by_bound ival size validity =
- let pred_size = Int.pred size in
- match validity with
- | Base.All -> begin (* no clipping can be performed *)
- match ival with
- | Ival.Top (Some mn,Some mx,_r,m) ->
- let result =
- if Int.lt m size
- then Imprecise(mn, Int.add mx pred_size)
- else Interval(mn, mx, m)
- in
- true, (false, result)
- | Ival.Top (None,_,_,_)
- | Ival.Top (_,None,_,_)
- | Ival.Float _ ->
- raise Unbounded
- | Ival.Set o -> true, (false, Set o)
- end
- | Base.Known (bound_min, bound_max) | Base.Unknown (bound_min, bound_max)
- | Base.Periodic (bound_min, bound_max, _) ->
- let max_in_bound = Int.sub bound_max pred_size in
- let is_in_bound x = match x with
- | Ival.Top (mn,mx,r,modu) ->
- let out, new_mn =
- match mn with
- | Some mn when (Int.ge mn bound_min) -> false, mn
- | _ -> true, Int.round_up_to_r ~r ~modu ~min:bound_min
- in
- let out, new_mx =
- match mx with
- | Some mx when (Int.le mx max_in_bound) -> out, mx
- | _ -> true, Int.round_down_to_r ~r ~modu ~max:max_in_bound
- in
- let itv_or_set =
- if Int.le new_mn new_mx
- then begin
- if Int.lt modu size
- then Imprecise(new_mn, Int.add new_mx pred_size)
- else Interval(new_mn, new_mx, modu)
- end
- else empty_interval_or_set
- in
- out, itv_or_set
- | _ -> assert false
- in
- let out, reduced_bounds as result =
- begin match ival with
- | Ival.Top (_mn,_mx,_r,_m) -> is_in_bound ival
- | Ival.Float _ -> is_in_bound Ival.top
- | Ival.Set s ->
- let out, set =
- Ival.O.fold
- (fun offset (out_acc, reduced_acc) ->
- let pseudo_interval =
- Ival.Top(Some offset, Some offset,Int.zero, Int.one)
- in
- let out, _reduced = is_in_bound pseudo_interval in
- out || out_acc,
- if out
- then reduced_acc
- else Ival.O.add offset reduced_acc)
- s
- (false, Ival.O.empty)
- in
- (out, Set set)
- end
- in
- match validity with
- | Base.Periodic(_, _, p) ->
- assert (Int.is_zero bound_min);
- let reduced_bounds =
- match reduced_bounds with
- | Imprecise (mn, mx) ->
- if Int.equal (Int.pos_div mn p) (Int.pos_div mx p)
- then Imprecise (Int.pos_rem mn p, Int.pos_rem mx p)
- else Imprecise (bound_min, Int.pred p)
- | Set s ->
- let treat_offset offset acc =
- let new_offset = Int.pos_rem offset p in
- if Int.gt (Int.add new_offset size) p
- then raise Unbounded
- else
-(* Format.printf "old offset: %a mx: %a period: %a new: %a@."
- Int.pretty offset
- Int.pretty bound_max
- Int.pretty p
- Int.pretty new_offset; *)
- Ival.O.add new_offset acc
- in
- begin
- try
- Set (Ival.O.fold treat_offset s Ival.O.empty)
- with Unbounded -> Imprecise (bound_min, Int.pred p)
- end
- | Interval(lb, _ub, mo) ->
- if Int.is_zero (Int.pos_rem mo p)
- then Set (Ival.O.singleton (Int.pos_rem lb p))
- else begin
- Format.printf "Interval %a %a %a@."
- Int.pretty lb
- Int.pretty _ub
- Int.pretty mo;
- Imprecise (bound_min, Int.pred p)
- end
- in
- false, (out, reduced_bounds)
- | _ -> true, result
-
- let filter_by_bound_for_reading ~with_alarms ival size validity =
- let _, (out, filtered_by_bound) = reduce_ival_by_bound ival size validity in
- if out then warn_mem_read with_alarms;
- filtered_by_bound
-
- let filter_by_bound_for_writing ~exact ~with_alarms ival size validity =
- let still_exact, (out, filtered_by_bound) =
- reduce_ival_by_bound ival size validity
- in
- if out then warn_mem_write with_alarms;
- (exact && still_exact), filtered_by_bound
-
let create_initial ~v ~modu =
let vv = if V.is_isotropic v then Int.zero,Int.one,v
else Int.zero,modu,v
@@ -1361,7 +1231,7 @@ let reciprocal_image m base =
let r =
try
let filtered_by_bound =
- filter_by_bound_for_reading ~with_alarms offsets size validity
+ Tr_offset.filter_by_bound_for_reading ~with_alarms offsets size validity
in
let inform = ref false in
let value = ref V.bottom in
@@ -1379,9 +1249,9 @@ let reciprocal_image m base =
else read_ahead
in
begin match filtered_by_bound with
- | Imprecise (mn, mx) ->
+ | Tr_offset.Imprecise (mn, mx) ->
value := find_imprecise mn mx offsetmap
- | Interval (mn, mx, m) ->
+ | Tr_offset.Interval (mn, mx, m) ->
assert(Int.gt m pred_size);
let current = ref mn in
let r = Int.pos_rem mn m in
@@ -1400,7 +1270,7 @@ let reciprocal_image m base =
in
current := cursor
done;
- | Set s ->
+ | Tr_offset.Set s ->
(*Format.eprintf "find_ival(Set) %a@." Ival.pretty (Ival.Set s);*)
Ival.O.iter (fun x -> ignore (find_and_accumulate x Int.zero)) s;
end;
@@ -1413,7 +1283,7 @@ let reciprocal_image m base =
"extracting bits of a pointer";
end;
!value
- with Unbounded -> V.top
+ with Tr_offset.Unbounded -> V.top
in
if M.is_empty offsetmap && not (V.equal V.top r) then
Kernel.debug ~once:true "%a+%a, size %a, %s, validity %a, result %a"
@@ -1458,7 +1328,7 @@ let reciprocal_image m base =
pretty offsetmap_orig; *)
try
let exact, reduced =
- filter_by_bound_for_writing ~with_alarms ~exact offsets size validity
+ Tr_offset.filter_by_bound_for_writing ~with_alarms ~exact offsets size validity
in
let fold_set s =
Ival.O.fold
@@ -1474,10 +1344,10 @@ let reciprocal_image m base =
offsetmap_orig
in
match reduced with
- | Imprecise (mn, mx) ->
+ | Tr_offset.Imprecise (mn, mx) ->
let v = V.topify_misaligned_read_origin v in
add_imprecise mn mx v offsetmap_orig
- | Interval(mn, mx, m) ->
+ | Tr_offset.Interval(mn, mx, m) ->
begin
let res =
add_top_binding_offsetmap
@@ -1527,13 +1397,13 @@ let reciprocal_image m base =
res
end
- | Set o when not (Ival.O.is_empty o) -> fold_set o
- | Set _ ->
+ | Tr_offset.Set o when not (Ival.O.is_empty o) -> fold_set o
+ | Tr_offset.Set _ ->
if exact
then raise Result_is_bottom
else offsetmap_orig
with
- Unbounded ->
+ Tr_offset.Unbounded ->
(match with_alarms.imprecision_tracing with
| Aignore -> ()
| Acall f -> f ()
@@ -1652,7 +1522,7 @@ let reciprocal_image m base =
offsetmap;*)
try
let filtered_by_bound =
- filter_by_bound_for_reading ~with_alarms offsets size validity
+ Tr_offset.filter_by_bound_for_reading ~with_alarms offsets size validity
in
let pred_size = Int.pred size in
let i0 = Int.zero, pred_size in
@@ -1667,14 +1537,14 @@ let reciprocal_image m base =
read_ahead
in
begin match filtered_by_bound with
- | Imprecise(mn ,mx) ->
+ | Tr_offset.Imprecise(mn ,mx) ->
let v = find_imprecise mn mx offsetmap in
value :=
add_if_not_default
i0
(Int.zero, Int.one, v)
empty
- | Interval(mn, mx, m) ->
+ | Tr_offset.Interval(mn, mx, m) ->
assert (Int.gt m pred_size);
let current = ref mn in
let r = Int.pos_rem mn m in
@@ -1693,12 +1563,12 @@ let reciprocal_image m base =
in
current := cursor
done;
- | Set s ->
+ | Tr_offset.Set s ->
(*Format.eprintf "find_ival(Set) %a@." Ival.pretty (Ival.Set s);*)
Ival.O.iter (fun x -> ignore (find_and_accumulate x Int.zero)) s;
end;
!value
- with Unbounded -> empty
+ with Tr_offset.Unbounded -> empty
let copy_offsmap from start stop =
snd (copy_offsmap from start stop Int.zero)
diff --git a/src/memory_state/tr_offset.ml b/src/memory_state/tr_offset.ml
new file mode 100644
index 0000000000000000000000000000000000000000..5cd99cab85fc1b38487d470e988f3d03e1551436
--- /dev/null
+++ b/src/memory_state/tr_offset.ml
@@ -0,0 +1,140 @@
+open Abstract_interp
+open Abstract_value
+open CilE
+
+type t =
+ Set of Ival.O.t
+ | Interval of Int.t * Int.t * Int.t
+ | Imprecise of Int.t * Int.t
+
+exception Unbounded
+
+let empty = Set (Ival.O.empty)
+
+let reduce_ival_by_bound ival size validity =
+ let pred_size = Int.pred size in
+ match validity with
+ | Base.All -> begin (* no clipping can be performed *)
+ match ival with
+ | Ival.Top (Some mn,Some mx,_r,m) ->
+ let result =
+ if Int.lt m size
+ then Imprecise(mn, Int.add mx pred_size)
+ else Interval(mn, mx, m)
+ in
+ true, (false, result)
+ | Ival.Top (None,_,_,_)
+ | Ival.Top (_,None,_,_)
+ | Ival.Float _ ->
+ raise Unbounded
+ | Ival.Set o -> true, (false, Set o)
+ end
+ | Base.Known (bound_min, bound_max) | Base.Unknown (bound_min, bound_max)
+ | Base.Periodic (bound_min, bound_max, _) ->
+ let max_in_bound = Int.sub bound_max pred_size in
+ let is_in_bound x = match x with
+ | Ival.Top (mn,mx,r,modu) ->
+ let out, new_mn =
+ match mn with
+ | Some mn when (Int.ge mn bound_min) -> false, mn
+ | _ -> true, Int.round_up_to_r ~r ~modu ~min:bound_min
+ in
+ let out, new_mx =
+ match mx with
+ | Some mx when (Int.le mx max_in_bound) -> out, mx
+ | _ -> true, Int.round_down_to_r ~r ~modu ~max:max_in_bound
+ in
+ let itv_or_set =
+ if Int.le new_mn new_mx
+ then begin
+ if Int.lt modu size
+ then Imprecise(new_mn, Int.add new_mx pred_size)
+ else Interval(new_mn, new_mx, modu)
+ end
+ else empty
+ in
+ out, itv_or_set
+ | _ -> assert false
+ in
+ let out, reduced_bounds as result =
+ begin match ival with
+ | Ival.Top (_mn,_mx,_r,_m) -> is_in_bound ival
+ | Ival.Float _ -> is_in_bound Ival.top
+ | Ival.Set s ->
+ let out, set =
+ Ival.O.fold
+ (fun offset (out_acc, reduced_acc) ->
+ let pseudo_interval =
+ Ival.Top(Some offset, Some offset,Int.zero, Int.one)
+ in
+ let out, _reduced = is_in_bound pseudo_interval in
+ out || out_acc,
+ if out
+ then reduced_acc
+ else Ival.O.add offset reduced_acc)
+ s
+ (false, Ival.O.empty)
+ in
+ (out, Set set)
+ end
+ in
+ match validity with
+ | Base.Periodic(_, _, p) ->
+ assert (Int.is_zero bound_min);
+ let reduced_bounds =
+ match reduced_bounds with
+ | Imprecise (mn, mx) ->
+ if Int.equal (Int.pos_div mn p) (Int.pos_div mx p)
+ then Imprecise (Int.pos_rem mn p, Int.pos_rem mx p)
+ else Imprecise (bound_min, Int.pred p)
+ | Set s ->
+ let treat_offset offset acc =
+ let new_offset = Int.pos_rem offset p in
+ if Int.gt (Int.add new_offset size) p
+ then raise Unbounded
+ else
+ (* Format.printf "old offset: %a mx: %a period: %a new: %a@."
+ Int.pretty offset
+ Int.pretty bound_max
+ Int.pretty p
+ Int.pretty new_offset; *)
+ Ival.O.add new_offset acc
+ in
+ begin
+ try
+ Set (Ival.O.fold treat_offset s Ival.O.empty)
+ with Unbounded -> Imprecise (bound_min, Int.pred p)
+ end
+ | Interval(lb, _ub, mo) ->
+ if Int.is_zero (Int.pos_rem mo p)
+ then Set (Ival.O.singleton (Int.pos_rem lb p))
+ else begin
+ Format.printf "Interval %a %a %a@."
+ Int.pretty lb
+ Int.pretty _ub
+ Int.pretty mo;
+ Imprecise (bound_min, Int.pred p)
+ end
+ in
+ false, (out, reduced_bounds)
+ | _ -> true, result
+
+ let filter_by_bound_for_reading ~with_alarms ival size validity =
+ let _, (out, filtered_by_bound) = reduce_ival_by_bound ival size validity in
+ if out then warn_mem_read with_alarms;
+ filtered_by_bound
+
+ let filter_by_bound_for_writing ~exact ~with_alarms ival size validity =
+ let still_exact, (out, filtered_by_bound) =
+ reduce_ival_by_bound ival size validity
+ in
+ if out then warn_mem_write with_alarms;
+ (exact && still_exact), filtered_by_bound
+
+
+
+(*
+Local Variables:
+compile-command: "make -C ../.."
+End:
+*)