diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-02-21 14:01:51 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-02-21 14:01:51 +0100 |
| commit | 1e867c804ed11200c8ed1a55a71f416977249363 (patch) | |
| tree | f2acbb3d45d27b403840ef35b38b0159285f2ab6 | |
| parent | a83df40c59f8b3c50581304fb6c0d3913acf15c7 (diff) | |
| download | compcert-kvx-1e867c804ed11200c8ed1a55a71f416977249363.tar.gz compcert-kvx-1e867c804ed11200c8ed1a55a71f416977249363.zip | |
Added check for large arrays.
The check tests whether the size calculation of an array overflows
or the array covers half of the available address space and reports
an error in this case.
Bug 21034
| -rw-r--r-- | cparser/Cutil.ml | 11 | ||||
| -rw-r--r-- | cparser/Cutil.mli | 2 | ||||
| -rw-r--r-- | cparser/Elab.ml | 1 |
3 files changed, 14 insertions, 0 deletions
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 124560e5..586b4a92 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -642,6 +642,17 @@ let int_representable v nbits sgn = else 0L <= v && v < Int64.shift_left 1L nbits +let valid_array_size env ty v = + match sizeof env ty with + | None -> true (* Incomplete type should be caught later *) + | Some sz -> + let sz = Int64.of_int sz in + let ptr_bits = !Machine.config.sizeof_ptr * 8 - 1 in + if sz = 0L || v <= (Int64.div Int64.max_int sz) then + int_representable (Int64.mul sz v) ptr_bits true + else + false + (* Type of a function definition *) let fundef_typ fd = diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index 715cc123..79975dcf 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -237,6 +237,8 @@ val field_of_dot_access: Env.t -> typ -> string -> field (* Return the field info for a [x.field] access *) val field_of_arrow_access: Env.t -> typ -> string -> field (* Return the field info for a [x->field] access *) +val valid_array_size: Env.t -> typ -> int64 -> bool + (* Test whether the array size fits in half of the address space *) (* Constructors *) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 07351c46..8b38f4c7 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -658,6 +658,7 @@ and elab_type_declarator keep_ty loc env ty kr_ok = function if n < 0L then error loc "size of array is negative"; if n = 0L then warning loc Zero_length_array "zero size arrays are an extension"; + if not (Cutil.valid_array_size env ty n) then error loc "size of array is too large"; Some n | None -> error loc "size of array is not a compile-time constant"; |