diff --git a/src/plugins/value/domains/cvalue/builtins_string.ml b/src/plugins/value/domains/cvalue/builtins_string.ml
index 9a474137e2f8c36eb5616461674397fa3d080d5f..b4ac08862493c3272bd84e284c68b5995b20ba74 100644
--- a/src/plugins/value/domains/cvalue/builtins_string.ml
+++ b/src/plugins/value/domains/cvalue/builtins_string.ml
@@ -59,6 +59,9 @@ let pos_min_int ival =
| None -> Integer.zero
| Some i -> Integer.(max zero i)
+let make_interval ~min ~max =
+ Ival.inject_interval ~min:(Some min) ~max:(Some max)
+
(* Backward reduction of an ival against an integer.*)
let backward_comp_left comp ival integer =
Ival.backward_comp_int_left comp ival (Ival.inject_singleton integer)
@@ -145,95 +148,80 @@ let read_char kind offset cvalue acc =
let new_acc = read_one_char kind ~offset ~from:acc.from cvalue in
{ new_acc with read = join acc.read new_acc.read }
-(* Reads the [offsetmap] character by character, starting from [index], with a
- period of [kind.size], until reaching [max]. Precise but inefficient. *)
-let rec search_each_index kind ~validity ~index ~max offsetmap acc =
- let offsets = Ival.inject_singleton index in
+(* Searches the range [min..max] of the [offsetmap], that contains a repeated
+ value of size [v_size]. *)
+let search_offsetmap_range kind offsetmap validity ~min ~max ~v_size acc =
let size = kind.size in
- let cvalue = Cvalue.V_Offsetmap.find ~validity ~offsets ~size offsetmap in
- let acc = read_char kind offsets cvalue acc in
- let index = Integer.add index size in
- if acc.stop || Integer.gt index max
- then acc
- else search_each_index kind ~validity ~index ~max offsetmap acc
-
-(* Reads at once the characters of size [kind.size] in the range [min..max] in
- the [offsetmap], that contains the repeated value [v] of size [v_size].
- Assumes that [min] and [max] match the start and the end of the values. *)
-let search_range kind ~min ~max (v, v_size, _v_shift) acc =
- let make_interval ~min ~max =
- Ival.inject_interval ~min:(Some min) ~max:(Some max)
- in
- (* Case where only one read is needed. *)
- if Cvalue.V_Or_Uninitialized.is_isotropic v || Integer.equal kind.size v_size
- then
- let offset = make_interval ~min ~max ~rem:Integer.zero ~modu:kind.size in
- read_char kind offset v acc
- else
- (* The value [v] contains [nb_chars] characters: need [nb_chars] reads. *)
- let nb_chars = Integer.e_div v_size kind.size in
- (* Reads the [count]-nth character in [v]. *)
- let rec do_one_char count ~max res =
- let start = Integer.mul kind.size count in
- let min = Integer.add min start in
- if Integer.ge count nb_chars || Integer.gt min max
+ (* Reads will repeat themselves every [modu] bits. *)
+ let modu = Integer.ppcm v_size size in
+ let max_reads = Integer.(to_int (e_div modu size)) in
+ (* Performs [max_reads] consecutive reads from offsets {[min] + k[modu]},
+ bound by [max]. *)
+ let search_until ~max acc =
+ let rec read_index count ~min res =
+ let rem = Integer.e_rem min modu in
+ let offsets = make_interval ~min ~max ~rem ~modu in
+ let cvalue = Cvalue.V_Offsetmap.find ~validity ~offsets ~size offsetmap in
+ (* Be careful to not use this result [t] for the reads of the next
+ characters, as the reduction of [acc.from] assumes that the reads at
+ [offset] are consecutive, which is not the case here. Thus, we always
+ read with the initial [acc], and accumulate the result in [res]. *)
+ let t = read_char kind offsets cvalue acc in
+ let read = join res.read t.read in
+ (* At the end, all the reads are indeed consecutive, and we can
+ use the narrow of the [from] for the next ranges of the offsetmap. *)
+ let from = Ival.narrow res.from t.from in
+ let res = { read; from; stop = res.stop || t.stop; } in
+ let min = Integer.add min kind.size in
+ if (Ival.is_singleton_int offsets && res.stop)
+ || Integer.gt min max || count >= max_reads
then res
- else
- let stop = Integer.(add start (pred kind.size)) in
- let _, cvalue =
- Cvalue.V_Or_Uninitialized.extract_bits
- ~topify:Origin.K_Misalign_read ~start ~stop ~size:v_size v
- in
- let rem = Integer.mul count kind.size in
- let offset = make_interval ~min ~max ~rem ~modu:v_size in
- (* Be careful to not use this result [t] for the reads of the next
- characters, as the reduction of [acc.from] assumes that the reads at
- [offset] are consecutive, which is not the case here. Thus, we always
- read with the initial [acc], and accumulate the result in [res]. *)
- let t = read_char kind offset cvalue acc in
- let read = join res.read t.read in
- (* At the end, the [nb_chars] reads are indeed consecutive, and we can
- use the narrow of the [from] for the next ranges of the offsetmap. *)
- let from = Ival.narrow res.from t.from in
- let res = { read; from; stop = res.stop || t.stop; } in
- do_one_char (Integer.succ count) ~max res
- in
- (* The maximal offset we are sure to read. *)
- let sure_offset = Integer.max (the_max_int acc.from) min in
- let sure_max = Integer.add sure_offset v_size in
- (* If one of the read characters stops the search, the other characters will
- lead to imprecise results — as they are all periodic until [max]. Thus we
- perform a first read until the maximal sure read offset. *)
- let acc =
- if Integer.lt sure_max max
- then do_one_char Integer.zero ~max:sure_max acc
- else acc
+ else read_index (count + 1) ~min res
in
- if acc.stop then acc else do_one_char Integer.zero ~max acc
+ read_index 1 ~min acc
+ in
+ (* The maximal offset we are sure to read from. *)
+ let sure_offset = Integer.max min (the_max_int acc.from) in
+ let sure_max = Integer.pred (Integer.add sure_offset modu) in
+ (* If one of the read characters stops the search, the other characters will
+ lead to imprecise results — as they are all periodic until [max]. Thus we
+ perform a first read of the range until the maximal sure read offset. *)
+ let acc =
+ if Integer.lt sure_max max
+ then search_until ~max:sure_max acc
+ else acc
+ in
+ if acc.stop then acc else search_until ~max acc
(* Folds the [offsetmap] from [start] to [max]. *)
-let fold_offsm kind ~validity ~start ~max offsetmap acc =
+let fold_offsm kind ~validity ~start ~max ~rem offsetmap acc =
let modu = kind.size in
let process_range (start, max) (v, v_size, v_shift) acc =
if acc.stop then acc else
- let index = Integer.round_up_to_r ~min:start ~r:Integer.zero ~modu in
- let v_start = Abstract_interp.Rel.add_abs start v_shift in
- (* Process the whole range at once when:
- - the ending cut is aligned with the reads, meaning that no read
- overlaps between two ranges of the offsetmap.
- - and either the value is isotropic, or the reads are aligned with the
- repeated values. *)
- if Integer.is_zero (Integer.e_rem (Integer.succ max) modu) &&
- (Cvalue.V_Or_Uninitialized.is_isotropic v ||
- Integer.(equal index v_start && is_zero (e_rem v_size kind.size)))
- then search_range kind ~min:index ~max (v, v_size, v_shift) acc
- else search_each_index kind ~validity ~index ~max offsetmap acc
+ let min = Integer.round_up_to_r ~min:start ~r:rem ~modu in
+ if Integer.gt min max then acc else
+ let v_start = Abstract_interp.Rel.add_abs start v_shift in
+ (* Only one read of the value is needed when:
+ - the ending cut is aligned with the reads, meaning that no read
+ overlaps between two ranges of the offsetmap.
+ - and either the value is isotropic, or the repeated value has the
+ same size than the reads. *)
+ if Integer.equal rem (Integer.e_rem (Integer.succ max) modu) &&
+ (Cvalue.V_Or_Uninitialized.is_isotropic v ||
+ Integer.equal min v_start && Integer.equal v_size kind.size)
+ then
+ let offset = make_interval ~min ~max ~rem ~modu in
+ read_char kind offset v acc
+ else
+ (* Otherwise, search the range by reading the offsetmap for each
+ required offset. Less efficient, but equally precise. *)
+ search_offsetmap_range kind offsetmap validity ~min ~max ~v_size acc
in
Cvalue.V_Offsetmap.fold_between
~entire:false (start, max) process_range offsetmap acc
(* Performs the search in the [offsetmap]. *)
-let search_offsm kind ~validity ~offset offsetmap =
+let search_offsm kind ~validity ~offset ~rem offsetmap =
let start = pos_min_int offset in
(* Compute the maximal bit that can be read in the offsetmap. *)
let base_max = match Base.valid_range validity with
@@ -251,7 +239,7 @@ let search_offsm kind ~validity ~offset offsetmap =
in
(* Starts the search with an empty accumulator. *)
let acc = { read = empty; from = offset; stop = false } in
- let acc = fold_offsm kind ~validity ~start ~max offsetmap acc in
+ let acc = fold_offsm kind ~validity ~start ~max ~rem offsetmap acc in
(* Alarm if the search does not stop before the end of the offsetmap. *)
if not acc.stop && Integer.gt (Integer.add max kind.size) base_max
then { acc.read with alarm = true }
@@ -273,9 +261,14 @@ let search_base kind ~offset base state =
| `Top -> assert false
| `Value offsetmap ->
let validity = Base.validity base in
- let search_one_char offset char =
+ let search_one_rem ~offset ~char ~rem acc =
let kind = { kind with search = char } in
- search_offsm kind ~validity ~offset offsetmap
+ let res = search_offsm kind ~validity ~offset ~rem offsetmap in
+ join acc res
+ in
+ let search_one_char offset char =
+ let rems = Ival.scale_rem ~pos:true kind.size offset in
+ Ival.fold_int (fun rem -> search_one_rem ~offset ~char ~rem) rems empty
in
let search_one_offset offset =
search_by_folding kind.search (search_one_char offset)
@@ -346,7 +339,12 @@ let reduce_by_validity ~size cvalue =
let loc_bits = Locations.loc_bytes_to_loc_bits cvalue in
let loc = Locations.make_loc loc_bits (Int_Base.inject size) in
if Locations.(is_valid Read loc)
- then loc.Locations.loc, true
+ then
+ let is_aligned _base ival =
+ Ival.is_zero (Ival.scale_rem ~pos:true size ival)
+ in
+ let valid = Locations.Location_Bits.for_all is_aligned loc_bits in
+ loc.Locations.loc, valid
else
let valid_loc = Locations.(valid_part Read ~bitfield:true loc) in
valid_loc.Locations.loc, false
diff --git a/tests/builtins/oracle/wcslen.res.oracle b/tests/builtins/oracle/wcslen.res.oracle
index 784bf02c5cf4f24b9aa67db81b8cf442ed7c0e06..00a752d3a13c96865b01c5993f4439c578fb0b19 100644
--- a/tests/builtins/oracle/wcslen.res.oracle
+++ b/tests/builtins/oracle/wcslen.res.oracle
@@ -31,7 +31,7 @@
[11] ∈ {100}
nondet ∈ [--..--]
[eva] computing for function small_sets <- main.
- Called from tests/builtins/wcslen.c:339.
+ Called from tests/builtins/wcslen.c:370.
[eva] tests/builtins/wcslen.c:60: Call to builtin wcslen
[eva] tests/builtins/wcslen.c:60:
function wcslen: precondition 'valid_string_s' got status valid.
@@ -55,7 +55,7 @@
[eva] Recording results for small_sets
[eva] Done for function small_sets
[eva] computing for function zero_termination <- main.
- Called from tests/builtins/wcslen.c:340.
+ Called from tests/builtins/wcslen.c:371.
[eva] tests/builtins/wcslen.c:89: Call to builtin wcslen
[eva:alarm] tests/builtins/wcslen.c:89: Warning:
function wcslen: precondition 'valid_string_s' got status unknown.
@@ -69,7 +69,7 @@
[eva] Recording results for zero_termination
[eva] Done for function zero_termination
[eva] computing for function wcslen_initialization <- main.
- Called from tests/builtins/wcslen.c:341.
+ Called from tests/builtins/wcslen.c:372.
[eva] tests/builtins/wcslen.c:105: Call to builtin wcslen
[eva:alarm] tests/builtins/wcslen.c:105: Warning:
function wcslen: precondition 'valid_string_s' got status unknown.
@@ -88,7 +88,7 @@
[eva] Recording results for wcslen_initialization
[eva] Done for function wcslen_initialization
[eva] computing for function wcslen_large <- main.
- Called from tests/builtins/wcslen.c:342.
+ Called from tests/builtins/wcslen.c:373.
[eva] computing for function init_array_nondet <- wcslen_large <- main.
Called from tests/builtins/wcslen.c:168.
[eva] tests/builtins/wcslen.c:161: Call to builtin memset
@@ -152,7 +152,7 @@
[eva] Recording results for wcslen_large
[eva] Done for function wcslen_large
[eva] computing for function wcslen_large_uninit <- main.
- Called from tests/builtins/wcslen.c:343.
+ Called from tests/builtins/wcslen.c:374.
[eva] computing for function init_array_nondet <- wcslen_large_uninit <- main.
Called from tests/builtins/wcslen.c:197.
[eva] tests/builtins/wcslen.c:161: Call to builtin memset
@@ -193,7 +193,7 @@
[eva] Recording results for wcslen_large_uninit
[eva] Done for function wcslen_large_uninit
[eva] computing for function misc <- main.
- Called from tests/builtins/wcslen.c:344.
+ Called from tests/builtins/wcslen.c:375.
[eva] tests/builtins/wcslen.c:241: Call to builtin wcslen
[eva:alarm] tests/builtins/wcslen.c:241: Warning:
function wcslen: precondition 'valid_string_s' got status invalid.
@@ -245,14 +245,14 @@
[eva] Recording results for misc
[eva] Done for function misc
[eva] computing for function bitfields <- main.
- Called from tests/builtins/wcslen.c:345.
+ Called from tests/builtins/wcslen.c:376.
[eva] tests/builtins/wcslen.c:140: Call to builtin wcslen
[eva:alarm] tests/builtins/wcslen.c:140: Warning:
function wcslen: precondition 'valid_string_s' got status invalid.
[eva] Recording results for bitfields
[eva] Done for function bitfields
[eva] computing for function bitfields2 <- main.
- Called from tests/builtins/wcslen.c:346.
+ Called from tests/builtins/wcslen.c:377.
[eva] tests/builtins/wcslen.c:155: Call to builtin wcslen
[eva] tests/builtins/wcslen.c:155:
function wcslen: precondition 'valid_string_s' got status valid.
@@ -260,7 +260,7 @@
[eva] Recording results for bitfields2
[eva] Done for function bitfields2
[eva] computing for function escaping <- main.
- Called from tests/builtins/wcslen.c:347.
+ Called from tests/builtins/wcslen.c:378.
[eva:alarm] tests/builtins/wcslen.c:222: Warning:
pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva:alarm] tests/builtins/wcslen.c:222: Warning:
@@ -282,7 +282,7 @@
[eva] Recording results for escaping
[eva] Done for function escaping
[eva] computing for function big_array <- main.
- Called from tests/builtins/wcslen.c:348.
+ Called from tests/builtins/wcslen.c:379.
[eva:alarm] tests/builtins/wcslen.c:287: Warning:
out of bounds write. assert \valid(p);
[eva:alarm] tests/builtins/wcslen.c:291: Warning:
@@ -312,7 +312,7 @@
[eva] Recording results for big_array
[eva] Done for function big_array
[eva] computing for function negative_offsets <- main.
- Called from tests/builtins/wcslen.c:349.
+ Called from tests/builtins/wcslen.c:380.
[eva] tests/builtins/wcslen.c:314: starting to merge loop iterations
[eva] computing for function Frama_C_interval <- negative_offsets <- main.
Called from tests/builtins/wcslen.c:318.
@@ -364,6 +364,32 @@
function wcslen: precondition 'valid_string_s' got status unknown.
[eva] Recording results for negative_offsets
[eva] Done for function negative_offsets
+[eva] computing for function misaligned_string <- main.
+ Called from tests/builtins/wcslen.c:381.
+[eva] tests/builtins/wcslen.c:345: assertion got status valid.
+[eva] tests/builtins/wcslen.c:346: Call to builtin wcslen
+[eva] tests/builtins/wcslen.c:346:
+ function wcslen: precondition 'valid_string_s' got status valid.
+[eva] computing for function Frama_C_interval <- misaligned_string <- main.
+ Called from tests/builtins/wcslen.c:350.
+[eva] tests/builtins/wcslen.c:350:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva:alarm] tests/builtins/wcslen.c:351: Warning:
+ out of bounds write. assert \valid((char *)((wchar_t *)b) + i);
+[eva:alarm] tests/builtins/wcslen.c:352: Warning: assertion got status unknown.
+[eva] tests/builtins/wcslen.c:353: Call to builtin wcslen
+[eva:alarm] tests/builtins/wcslen.c:353: Warning:
+ function wcslen: precondition 'valid_string_s' got status unknown.
+[eva:alarm] tests/builtins/wcslen.c:361: Warning: assertion got status unknown.
+[eva] tests/builtins/wcslen.c:362: Call to builtin wcslen
+[eva:alarm] tests/builtins/wcslen.c:362: Warning:
+ function wcslen: precondition 'valid_string_s' got status unknown.
+[eva] tests/builtins/wcslen.c:365: Call to builtin wcslen
+[eva:alarm] tests/builtins/wcslen.c:365: Warning:
+ function wcslen: precondition 'valid_string_s' got status invalid.
+[eva] Recording results for misaligned_string
+[eva] Done for function misaligned_string
[eva] Recording results for main
[eva] done for function main
[scope:rm_asserts] removing 3 assertion(s)
@@ -405,6 +431,24 @@
[1..3] ∈ ESCAPINGADDR
z1 ∈ {0}
z2 ∈ {0}
+[eva:final-states] Values at end of function misaligned_string:
+ Frama_C_entropy_source ∈ [--..--]
+ a[0][bits 0 to 7] ∈ {1}
+ [0][bits 8 to 31] ∈ {0}
+ [1] ∈ {1}
+ [2] ∈ {0}
+ a_length ∈ {2}
+ b[0..9999999]# ∈ {0; 17} repeated %8
+ i ∈ [0..39999999]
+ b_length ∈ [0..9999999]
+ c[0][bits 0 to 7] ∈ {0}
+ {[0][bits 8 to 31]#; [1][bits 0 to 7]#} ∈ {1}
+ {[1][bits 8 to 31]#; [2][bits 0 to 7]#} ∈ {2}
+ {[2][bits 8 to 31]; [3][bits 0 to 7]} ∈ {0}
+ {[3][bits 8 to 31]#; [4][bits 0 to 7]#} ∈ {4}
+ [4][bits 8 to 31] ∈ {0}
+ p ∈ {{ &c + {1} }}
+ c_length ∈ {2}
[eva:final-states] Values at end of function misc:
Frama_C_entropy_source ∈ [--..--]
loc_str ∈ {{ L"Bonjour Monde\n" }}
@@ -524,9 +568,11 @@
[from] Done for function bitfields2
[from] Computing for function escaping
[from] Done for function escaping
-[from] Computing for function misc
-[from] Computing for function Frama_C_interval <-misc
+[from] Computing for function misaligned_string
+[from] Computing for function Frama_C_interval <-misaligned_string
[from] Done for function Frama_C_interval
+[from] Done for function misaligned_string
+[from] Computing for function misc
[from] Done for function misc
[from] Computing for function negative_offsets
[from] Done for function negative_offsets
@@ -560,7 +606,8 @@
non_terminated2[2..3]; empty_or_uninitialized[0];
uninitialized[0]; s[0..1]; t[0..3]; s; s; a[3..99]; a[3..99];
s[0..3]; loc_char_array[0..4]; x[0..3]; maybe_init[0..1];
- t[0..999999]; u[0..199]; r[0..200]; buf[0..99];
+ t[0..999999]; u[0..199]; r[0..200]; buf[0..99]; a[0..2];
+ b[0..9999999]; c{[0][bits 8 to 31]; [1..3]; [4][bits 0 to 7]};
L"Hello World\n"[bits 0 to 415];
L"abc\000\000\000abc"[bits 0 to 319]; L""; L"a"[bits 0 to 63];
L"aa"[bits 0 to 95]; L"aaa"[bits 0 to 127];
@@ -582,6 +629,8 @@
NO EFFECTS
[from] Function escaping:
NO EFFECTS
+[from] Function misaligned_string:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] Function misc:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] Function negative_offsets:
@@ -620,6 +669,11 @@
s[0..3]; z1; tmp; z2; tmp_0
[inout] Inputs for function escaping:
nondet
+[inout] Out (internal) for function misaligned_string:
+ Frama_C_entropy_source; a[0..2]; a_length; b[0..9999999]; i; b_length;
+ c[0..4]; p; c_length
+[inout] Inputs for function misaligned_string:
+ Frama_C_entropy_source; nondet
[inout] Out (internal) for function misc:
Frama_C_entropy_source; loc_str; loc_char_array[3]; sz1; sz2; sz3;
sz4; sz5; sz6; sz7; sz8; x[0..3]; z[0..3]; i; str; s1; tmp; s2; tmp_0;
diff --git a/tests/builtins/wcslen.c b/tests/builtins/wcslen.c
index dea7cd1aad9aba23f6b081452fb1dee572a146fb..183e2f2a2daac8ffd817e7afe4ae3beb968bc4c9 100644
--- a/tests/builtins/wcslen.c
+++ b/tests/builtins/wcslen.c
@@ -335,6 +335,37 @@ void negative_offsets() {
wchar_t dest[100 * 2];
}
+#define MAX 10000000
+
+void misaligned_string () {
+ // Read an offsetmap with a value range smaller than the read characters.
+ wchar_t a[3] = {0};
+ *(char *)a = 1;
+ a[1] = 1;
+ //@ assert valid_read_wstring(&a[0]);
+ unsigned int a_length = wcslen(&a[0]);
+ /* Read an offsetmap with repeated values smaller than the searched
+ characters: test a performance issue. */
+ wchar_t b[MAX] = {0};
+ int i = Frama_C_interval(0, MAX * 4);
+ *((char *)b + i) = (char)17;
+ //@ assert valid_read_wstring(&b[0]);
+ unsigned int b_length = wcslen(&b[0]);
+ /* Read an offsetmap through a misaligned pointer. */
+ wchar_t c[5] = {0};
+ wchar_t *p = (wchar_t *)( (char *)c + 1);
+ *p = 1;
+ *(p+1) = 2;
+ *(p+2) = 0; // If we accept the string pointed by p, its length should be 2.
+ *(p+3) = 4;
+ //@ assert valid_read_wstring(p);
+ unsigned int c_length = wcslen(p);
+ if (nondet) {
+ *(p+2) = 3; // The string pointed by p cannot be valid here.
+ c_length = wcslen(p);
+ }
+}
+
int main (int c) {
small_sets();
zero_termination();
@@ -347,5 +378,6 @@ int main (int c) {
escaping();
big_array();
negative_offsets();
+ misaligned_string();
return 0;
}