From d2e32a2e2c11bfd0c3559d01fcdfe49b30defd85 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Fri, 3 Feb 2023 12:05:56 +0100 Subject: [PATCH] Checksafety: soundly handle ArrayInit --- CHANGELOG.md | 5 ++- compiler/safety/fail/array_init.jazz | 10 +++++ compiler/safety/success/parr_init.jazz | 47 ++++++++++++++++++++++++ compiler/src/safety/safetyAbsExpr.ml | 28 +++++++++++--- compiler/src/safety/safetyAbsExpr.mli | 4 +- compiler/src/safety/safetyInterpreter.ml | 4 ++ 6 files changed, 89 insertions(+), 9 deletions(-) create mode 100644 compiler/safety/fail/array_init.jazz create mode 100644 compiler/safety/success/parr_init.jazz diff --git a/CHANGELOG.md b/CHANGELOG.md index 53b98ff6e..33120a772 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -59,8 +59,9 @@ ([PR #313](https://github.com/jasmin-lang/jasmin/pull/313); fixes [#310](https://github.com/jasmin-lang/jasmin/issues/310)). -- Fix to the safety checker - ([PR #315](https://github.com/jasmin-lang/jasmin/pull/315); +- Fixes to the safety checker + ([PR #315](https://github.com/jasmin-lang/jasmin/pull/315), + ([PR #343](https://github.com/jasmin-lang/jasmin/pull/343); fixes [#314](https://github.com/jasmin-lang/jasmin/issues/314)). - Safety checker better handles integer shift operators diff --git a/compiler/safety/fail/array_init.jazz b/compiler/safety/fail/array_init.jazz new file mode 100644 index 000000000..246404e76 --- /dev/null +++ b/compiler/safety/fail/array_init.jazz @@ -0,0 +1,10 @@ +export +fn bad_read() -> reg u64 { + stack u64[2] t; + reg u64 r; + t[0] = 42; + t[1] = 33; + ArrayInit(t); + r = t[0]; + return r; +} diff --git a/compiler/safety/success/parr_init.jazz b/compiler/safety/success/parr_init.jazz new file mode 100644 index 000000000..63647c5b6 --- /dev/null +++ b/compiler/safety/success/parr_init.jazz @@ -0,0 +1,47 @@ +export +fn reg_arr_init() -> reg u64 { + reg u64 r; + reg u64[1] a; + ArrayInit(a); + a[0] = 1; + r = a[0]; + return r; +} + +export +fn stack_arr_init() -> reg u64 { + reg u64 r; + stack u64[1] a; + ArrayInit(a); + a[0] = 1; + r = a[0]; + return r; +} + +export +fn slice_arr_init() -> reg u64 { + reg u64 r; + stack u64[2] a; + reg ptr u64[1] s; + a[1] = 1; + s = a[0:1]; + ArrayInit(s); + r = a[1]; + return r; +} + +export +fn slices_arr_init(reg u64 b) -> reg u64 { + reg u64 r; + stack u64[4] a; + reg ptr u64[1] s; + if b >s 0 { + s = a[0:1]; + } else { + s = a[1:1]; + } + ArrayInit(s); + a[0] = 1; + r = a[0]; + return r; +} diff --git a/compiler/src/safety/safetyAbsExpr.ml b/compiler/src/safety/safetyAbsExpr.ml index 6229491fe..d64e9ebb4 100644 --- a/compiler/src/safety/safetyAbsExpr.ml +++ b/compiler/src/safety/safetyAbsExpr.ml @@ -1128,6 +1128,27 @@ module AbsExpr (AbsDom : AbsNumBoolType) = struct (u8_blast_var ~blast_arrays:true eiv) ) a vevs + (* The variables representing the contents of an array *) + let array_contents lhs_arr = + lhs_arr |> arr_full_range |> List.map (fun y -> Mlocal y) + + (* The variables representing the contents of a slice *) + let slice_contents x ws n = + List.init (size_of_ws ws) (fun i -> Mlocal (AarraySlice (x, U8, n + i))) + + let remove_array_contents_mv abs = + function + | Mlocal (Aarray x) -> array_contents x |> AbsDom.remove_vars abs + | Mlocal (AarraySlice (x, ws, n)) -> slice_contents x ws n |> AbsDom.remove_vars abs + | _ -> assert false + + let abs_forget_array_contents abs mi lv = + match mvar_of_lvar abs mi lv with + | MLnone -> abs + | MLvar(_, mv) -> remove_array_contents_mv abs mv + | MLvars(_, mvs) -> List.fold_left remove_array_contents_mv abs mvs + | MLasub(_, _ms) -> failwith "Not implemented (explicit array init of a slice)" + (* Array slice assignment. Does the numerical assignments. Remark: array elements do not need to be tracked in the point-to abstraction. *) @@ -1139,12 +1160,7 @@ module AbsExpr (AbsDom : AbsNumBoolType) = struct assign_slice_aux abs lhs rhs (* If any offset is unknown, we need to forget the array content. *) - | _, _ -> - let lhs_arr = lhs.ms_v in - let mvs = arr_full_range lhs_arr - |> List.map (fun y -> Mlocal y) in - AbsDom.forget_list abs mvs - + | _, _ -> array_contents lhs.ms_v |> AbsDom.forget_list abs let omvar_is_offset = function | MLvar (_, MvarOffset _) -> true diff --git a/compiler/src/safety/safetyAbsExpr.mli b/compiler/src/safety/safetyAbsExpr.mli index 4408d7540..0c6b05000 100644 --- a/compiler/src/safety/safetyAbsExpr.mli +++ b/compiler/src/safety/safetyAbsExpr.mli @@ -74,7 +74,9 @@ module AbsExpr (AbsDom : SafetyInterfaces.AbsNumBoolType) : sig AbsDom.t -> 'a gty -> mvar -> minfo option -> expr -> AbsDom.t val a_init_mlv_no_array : mlvar -> AbsDom.t -> AbsDom.t - + + val abs_forget_array_contents : AbsDom.t -> minfo -> lval -> AbsDom.t + val abs_assign : AbsDom.t -> ty -> mlvar -> expr -> AbsDom.t val abs_assign_opn : diff --git a/compiler/src/safety/safetyInterpreter.ml b/compiler/src/safety/safetyInterpreter.ml index 886b9487e..976539098 100644 --- a/compiler/src/safety/safetyInterpreter.ml +++ b/compiler/src/safety/safetyInterpreter.ml @@ -1600,6 +1600,10 @@ end = struct let cr = { ginstr with i_desc = Cassgn (lv, tag, Bty (U sz), er) } in aeval_if asmOp ginstr c [cl] [cr] state + | Cassgn (lv, _, _, Parr_init _) -> + let abs = AbsExpr.abs_forget_array_contents state.abs ginstr.i_info lv in + { state with abs } + | Copn ([ lv ], _, Ocopy _, [ e ]) | Cassgn (lv, _, _, e) -> let abs = AbsExpr.abs_assign