[asl] Prevent use of empty slices on integers and bitvectors.

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 *)

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 ->

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

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: