Merge pull request #998 from HadrienRenaud/asl-fix-setter-bug

[asl] fix setter bug

Some expressions were not annotated during setter expansion, this is now fixed.

asllib/PP.ml

@@ -126,7 +126,7 @@ let rec pp_expr f e =
   | E_GetField (e, x) -> fprintf f "@[%a@,.%s@]" pp_expr e x
   | E_GetFields (e, xs) ->
       fprintf f "@[%a@,.[@[%a@]]@]" pp_expr e (pp_comma_list pp_print_string) xs
-  | E_GetItem (e, i) -> fprintf f "@[%a@,.item%d]" pp_expr e i
+  | E_GetItem (e, i) -> fprintf f "@[%a@,.item%d@]" pp_expr e i
   | E_Record (ty, li) ->
       let pp_one f (x, e) = fprintf f "@[<h>%s =@ %a@]" x pp_expr e in
       fprintf f "@[<hv>%a {@ %a@;<1 -2>}@]" pp_ty ty (pp_comma_list pp_one) li

asllib/Typing.ml

@@ -46,6 +46,14 @@ let rec list_mapi2 f i l1 l2 =
       r :: list_mapi2 f (i + 1) l1 l2
   | _, _ -> invalid_arg "List.map2"
 
+let rec list_mapi3 f i l1 l2 l3 =
+  match (l1, l2, l3) with
+  | [], [], [] -> []
+  | a1 :: l1, a2 :: l2, a3 :: l3 ->
+      let r = f i a1 a2 a3 in
+      r :: list_mapi3 f (i + 1) l1 l2 l3
+  | _, _, _ -> invalid_arg "List.mapi3"
+
 (* Begin ReduceConstants *)
 let reduce_constants env e =
   let open StaticInterpreter in
@@ -2512,9 +2520,10 @@ module Annotate (C : ANNOTATE_CONFIG) : S = struct
     let loc = to_pos le in
     let here d = add_pos_from loc d in
     (if false then (fun o ->
-       Format.eprintf "@[Setter@ @[%a@ = %a@]@ gave %a@.@]" PP.pp_lexpr le
-         PP.pp_expr e
-         (Format.pp_print_option PP.pp_stmt)
+       let none f () = Format.fprintf f "no reduction." in
+       Format.eprintf "@[<2>Setter@ @[%a@ = %a@]@ gave @[%a@]@.@]" PP.pp_lexpr
+         le PP.pp_expr e
+         (Format.pp_print_option ~none PP.pp_stmt)
          o;
        o)
      else Fun.id)
@@ -2571,11 +2580,13 @@ module Annotate (C : ANNOTATE_CONFIG) : S = struct
             if List.for_all Option.is_none subs then None
             else
               let s0 = S_Decl (LDK_Let, ldi_x, Some e) |> here in
-              let produce_one i sub_le = function
-                | None -> S_Assign (sub_le, sub_e i, V1) |> here
+              let produce_one i sub_le t_sub_e_i = function
+                | None ->
+                    let sub_le' = annotate_lexpr env sub_le t_sub_e_i in
+                    S_Assign (sub_le', sub_e i, V1) |> here
                 | Some s -> s
               in
-              list_mapi2 produce_one 0 les subs
+              list_mapi3 produce_one 0 les t_es subs
               |> List.cons s0 |> stmt_from_list |> Option.some
         | _ -> None)
     | LE_Var x ->

asllib/tests/regressions.t/run.t

@@ -392,6 +392,10 @@ Empty getters/setters
   [1]
   $ aslref setter_subfield.asl
   $ aslref setter_sub_tuple.asl
+  File setter_sub_tuple.asl, line 21, characters 15 to 16:
+  ASL Typing error: a subtype of integer {0} was expected, provided integer.
+  [1]
+  $ aslref setter_sub_tuple_02.asl
   $ aslref setter_subslice.asl
   $ aslref getter_subfield.asl
   $ aslref getter_sub_tuple.asl

asllib/tests/regressions.t/setter_sub_tuple_02.asl

@@ -0,0 +1,26 @@
+type MyBV of bits(8) { [5] bitfield };
+
+getter F => MyBV
+begin
+  return Zeros(8) as MyBV;
+end
+
+setter F = v: MyBV
+begin
+  assert v[0] == '0';
+end
+
+func foo () => (bit, integer)
+begin
+  return ('0', 1);
+end
+
+func main () => integer
+begin
+  var x: integer = 0;
+  (F.bitfield, x) = foo();
+  assert x == 1;
+
+  return 0;
+end
+