From f400b776af83719cb4556312447811e14b595cb6 Mon Sep 17 00:00:00 2001
From: Hadrien Renaud <hadrien.renaud2@arm.com>
Date: Tue, 22 Oct 2024 11:32:53 +0100
Subject: [PATCH] [asl] Prevent use of empty slices on integers and bitvectors.

---
 asllib/Typing.ml                                         | 8 ++++++++
 asllib/error.ml                                          | 9 +++++++--
 .../regressions.t/empty-setter-called-with-slices.asl    | 8 ++++----
 asllib/tests/regressions.t/run.t                         | 7 ++++++-
 4 files changed, 25 insertions(+), 7 deletions(-)

diff --git a/asllib/Typing.ml b/asllib/Typing.ml
index f37d9c86c..8ae2ba27e 100644
--- a/asllib/Typing.ml
+++ b/asllib/Typing.ml
@@ -1722,6 +1722,10 @@ module Annotate (C : ANNOTATE_CONFIG) : S = struct
             match struct_t_e'.desc with
             (* Begin ESlice *)
             | T_Int _ | T_Bits _ ->
+                let+ () =
+                  check_true (not (list_is_empty slices)) @@ fun () ->
+                  fatal_from loc Error.EmptySlice
+                in
                 let w = slices_width env slices in
                 (* TODO: check that:
                    - Rule SNQJ: An expression or subexpression which
@@ -1970,6 +1974,10 @@ module Annotate (C : ANNOTATE_CONFIG) : S = struct
             in
             let slices2 = best_effort slices (annotate_slices env) in
             let+ () = check_disjoint_slices le env slices2 in
+            let+ () =
+              check_true (not (list_is_empty slices)) @@ fun () ->
+              fatal_from le Error.EmptySlice
+            in
             LE_Slice (le2, slices2) |> here |: TypingRule.LESlice
         (* End *)
         (* Begin LESetArray *)
diff --git a/asllib/error.ml b/asllib/error.ml
index f88316eee..d5d11e7c4 100644
--- a/asllib/error.ml
+++ b/asllib/error.ml
@@ -32,6 +32,7 @@ type error_desc =
   | MissingField of string list * ty
   | BadSlices of error_handling_time * slice list * int
   | BadSlice of slice
+  | EmptySlice
   | TypeInferenceNeeded
   | UndefinedIdentifier of identifier
   | MismatchedReturnValue of string
@@ -149,6 +150,10 @@ module PPrint = struct
           pp_ty ty
           (pp_print_list ~pp_sep:pp_print_space pp_print_string)
           fields
+    | EmptySlice ->
+        pp_print_text f
+          "ASL Static Error: cannot slice with empty slicing operator. This \
+           might also be due to an incorrect getter/setter invocation."
     | BadSlices (t, slices, length) ->
         fprintf f
           "ASL %s error: Cannot extract from bitvector of length %d slice %a."
@@ -220,8 +225,8 @@ module PPrint = struct
           "ASL Typing error:@ cannot@ declare@ already@ declared@ element@ %S."
           x
     | BadReturnStmt None ->
-        fprintf f
-          "ASL Typing error:@ cannot@ return@ something@ from@ a@ procedure."
+        pp_print_text f
+          "ASL Typing error: cannot return something from a procedure."
     | UnexpectedSideEffect s -> fprintf f "Unexpected side-effect: %s" s
     | UncaughtException s -> fprintf f "Uncaught exception: %s" s
     | OverlappingSlices slices ->
diff --git a/asllib/tests/regressions.t/empty-setter-called-with-slices.asl b/asllib/tests/regressions.t/empty-setter-called-with-slices.asl
index eb2b2dfe1..453a6d5e2 100644
--- a/asllib/tests/regressions.t/empty-setter-called-with-slices.asl
+++ b/asllib/tests/regressions.t/empty-setter-called-with-slices.asl
@@ -1,16 +1,16 @@
-getter f1 => integer
+getter f1 => bits(4)
 begin
-  return 4;
+  return '0000';
 end
 
-setter f1 = v: integer
+setter f1 = v: bits(4)
 begin
   pass;
 end
 
 func main () => integer
 begin
-  f1[] = 4;
+  f1[] = '';
   
   return 0;
 end
diff --git a/asllib/tests/regressions.t/run.t b/asllib/tests/regressions.t/run.t
index 299d06eb5..98d9154d2 100644
--- a/asllib/tests/regressions.t/run.t
+++ b/asllib/tests/regressions.t/run.t
@@ -367,6 +367,10 @@ Base values
 
 Empty getters/setters
   $ aslref empty-getter-called-with-slices.asl
+  File empty-getter-called-with-slices.asl, line 8, characters 10 to 14:
+  ASL Static Error: cannot slice with empty slicing operator. This might also
+    be due to an incorrect getter/setter invocation.
+  [1]
   $ aslref empty-getter-called-with-slices-2.asl
   File empty-getter-called-with-slices-2.asl, line 8, characters 10 to 14:
   ASL Typing error: boolean does not subtype any of: integer, bits(-).
@@ -389,7 +393,8 @@ Empty getters/setters
   [1]
   $ aslref empty-setter-called-with-slices.asl
   File empty-setter-called-with-slices.asl, line 13, characters 2 to 6:
-  ASL Typing error: a subtype of bits(-) was expected, provided integer.
+  ASL Static Error: cannot slice with empty slicing operator. This might also
+    be due to an incorrect getter/setter invocation.
   [1]
   $ aslref nonempty-setter-called-without-slices.asl
   File nonempty-setter-called-without-slices.asl, line 13, characters 2 to 4: