jasmin-lang · eponier · Feb 3, 2026 · Jan 30, 2026 · Jan 30, 2026 · Jan 27, 2026
diff --git a/changes/01-feature/1375-literal-arrays.md b/changes/01-feature/1375-literal-arrays.md
@@ -0,0 +1,3 @@
+- Byte arrays can occur as literal values as string constants (`"abcd"`) or as
+  a sequence of expressions (e.g., `{ 1, 2, 3 }`)
+  ([PR 1375](https://github.com/jasmin-lang/jasmin/pull/1375)).
diff --git a/compiler/examples/extraction-unit-tests/.gitignore b/compiler/examples/extraction-unit-tests/.gitignore
@@ -2,3 +2,6 @@ add_in_mem.ec
 gcd.ec
 loops.ec
 sdiv.ec
+string.ec
+Array2.ec
+BArray2.ec
diff --git a/compiler/examples/extraction-unit-tests/proofs.ec b/compiler/examples/extraction-unit-tests/proofs.ec
@@ -5,6 +5,7 @@ require Gcd.
 require Loops.
 require Sdiv.
 require Add_in_mem.
+require String.
 
 lemma loops_forty_correct : hoare [ Loops.M.forty: true ==> res = W32.of_int 40 ].
 proof. by proc; unroll for ^while; auto. qed.
@@ -42,6 +43,11 @@ proof.
   by rewrite gcd0z.
 qed.
 
+(* ------------------------------------------------ *)
+hoare string_correct :
+  String.M.main : true ==> res = W32.of_int 1075839235.
+proof. by proc; auto => />; rewrite to_uint_eq !(to_uintD, to_uint_shl, of_uintK). qed.
+
 (* ------------------------------------------------ *)
 
 op to_list (m:global_mem_t) (p len : int) =

diff --git a/compiler/examples/extraction-unit-tests/string.jazz b/compiler/examples/extraction-unit-tests/string.jazz
@@ -0,0 +1,13 @@
+export fn main() -> reg u32 {
+  global u8[2] x = "@ ";
+  global u8[2] y = { 1, 3 };
+  reg u32 r = 0;
+  r += (32u)x[0];
+  r <<= 8;
+  r += (32u)x[1];
+  r <<= 8;
+  r += (32u)y[0];
+  r <<= 8;
+  r += (32u)y[1];
+  return r;
+}
diff --git a/compiler/src/alias.ml b/compiler/src/alias.ml
@@ -207,6 +207,7 @@ let slice_of_pexpr a =
   | Parr_init _ -> None
   | Pvar x -> Some (normalize_gvar a x)
   | Psub (aa, ws, len, x, i) -> Some (normalize_asub a aa ws len x i)
+  | PappN (Oarray _, _) -> hierror_no_loc "stack literal arrays are not supported"
   | (Pconst _ | Pbool _ | Pget _ | Pload _ | Papp1 _ | Papp2 _ | PappN _ ) -> assert false
   | Pif _ -> hierror_no_loc "conditional move of (ptr) arrays is not supported yet"
 

diff --git a/compiler/src/latex_printer.ml b/compiler/src/latex_printer.ml
@@ -55,8 +55,6 @@ let pp_string fmt s =
   | '^' -> caret fmt ()
   | c -> F.fprintf fmt "%c" c
 
-let pp_loc_string fmt s = L.unloc s |> pp_string fmt
-
 let pp_cc =
     pp_opt (fun fmt x -> F.fprintf fmt "%a " kw (match x with `Inline -> "inline" | `Export -> "export"))
 
@@ -195,6 +193,12 @@ and pp_expr_rec prio fmt pe =
   | PEFetch me -> pp_mem_access fmt me
   | PEpack (vs,es) ->
     F.fprintf fmt "(%a)[@[%a@]]" pp_svsize vs (pp_list ",@ " pp_expr) es
+  | PEarray es ->
+    F.fprintf fmt "%a @[%a@] %a"
+      openbrace ()
+      (pp_list ",@ " pp_expr) es
+      closebrace ()
+  | PEstring s -> pp_string fmt s
   | PEBool b -> F.fprintf fmt "%s" (if b then "true" else "false")
   | PEInt i -> F.fprintf fmt "%s" i
   | PECall (f, args) -> F.fprintf fmt "%a(%a)" pp_var f (pp_list ", " pp_expr) args
@@ -392,20 +396,11 @@ let pp_param fmt { ppa_ty ; ppa_name ; ppa_init } =
     dname (L.unloc ppa_name)
     pp_expr ppa_init
 
-let pp_pgexpr fmt = function
-  | GEword e -> pp_expr fmt e
-  | GEarray es ->
-    F.fprintf fmt "%a @[%a@] %a"
-      openbrace ()
-      (pp_list ",@ " pp_expr) es
-      closebrace ()
-  | GEstring e -> pp_loc_string fmt e
-
 let pp_global fmt { pgd_type ; pgd_name ; pgd_val } =
   F.fprintf fmt "%a %a = %a;"
     pp_type pgd_type
     dname (L.unloc pgd_name)
-    pp_pgexpr pgd_val
+    pp_expr pgd_val
 
 let pp_path fmt s =
   F.fprintf fmt "%S " (L.unloc s)

diff --git a/compiler/src/parser.mly b/compiler/src/parser.mly
@@ -289,6 +289,10 @@ pexpr_r:
 | ct=parens(svsize) LBRACKET es=rtuple1(pexpr) RBRACKET
     { PEpack(ct,es) }
 
+| e = STRING { PEstring e }
+
+| LBRACE es = rtuple1(pexpr) RBRACE { PEarray es }
+
 | ct=parens(cast) e=pexpr %prec BANG
     { PEOp1 (`Cast(ct), e) }
 
@@ -486,13 +490,8 @@ pparam:
     { { ppa_ty = ty; ppa_name = x; ppa_init = pe; } }
 
 (* -------------------------------------------------------------------- *)
-pgexpr:
-| e=pexpr { GEword e }
-| LBRACE es = rtuple1(pexpr) RBRACE { GEarray es }
-| e=loc(STRING) { GEstring e }
-
 pglobal:
-| pgd_type=ptype pgd_name=ident EQ pgd_val=pgexpr SEMICOLON
+| pgd_type=ptype pgd_name=ident EQ pgd_val=pexpr SEMICOLON
   { { pgd_type ; pgd_name ; pgd_val  } }
 
 (* -------------------------------------------------------------------- *)

diff --git a/compiler/src/pretyping.ml b/compiler/src/pretyping.ml
@@ -35,9 +35,6 @@ type tyerror =
   | TypeNotFound        of A.symbol
   | InvalidTypeAlias    of A.symbol L.located option * P.epty
   | InvalidCast         of P.epty pair
-  | InvalidTypeForGlobal of P.epty
-  | GlobArrayNotWord
-  | GlobWordNotArray
   | EqOpWithNoLValue
   | CallNotAllowed
   | PrimNotAllowed
@@ -105,16 +102,6 @@ let pp_tyerror fmt (code : tyerror) =
     F.fprintf fmt "can not implicitly cast %a into %a"
       pp_eptype t1 pp_eptype t2
 
-  | InvalidTypeForGlobal ty ->
-      F.fprintf fmt "globals should have type word; found: ‘%a’"
-        pp_eptype ty
-
-  | GlobArrayNotWord ->
-    F.fprintf fmt "the definition is an array and not a word"
-
-  | GlobWordNotArray ->
-    F.fprintf fmt "the definition is a word and not an array"
-
   | InvalidOperator o ->
     F.fprintf fmt "invalid operator %s"
       (match o with
@@ -266,7 +253,7 @@ module Env : sig
   val exit_namespace : 'asm env -> 'asm env
 
   module Vars : sig
-    val push_global   : 'asm env -> (P.pvar * P.epty * P.pexpr_ P.ggexpr ) -> 'asm env
+    val push_global   : 'asm env -> (P.pvar * P.epty * P.pexpr) -> 'asm env
     val push_param    : 'asm env -> (P.pvar * P.epty * P.pexpr) -> 'asm env
     val push_local    : 'asm env -> P.pvar * P.epty -> 'asm env
     val push_implicit : 'asm env -> P.pvar * P.epty -> 'asm env
@@ -1225,6 +1212,12 @@ let word_of_wint wint_of_word ws (cast : W.signedness option) e =
     e, P.etwi s ws
 *)
 
+(* -------------------------------------------------------------------- *)
+let array_of_string s =
+  s |> String.to_list |> List.map @@ fun c ->
+  c |> Char.code |> Z.of_int |> fun z ->
+  P.(Papp1 (op_word_of_int(Word, W.Unsigned, W.U8), Pconst z))
+
 (* -------------------------------------------------------------------- *)
 let rec tt_expr pd ?(mode=`AllVar) (env : 'asm Env.env) pe =
   match L.unloc pe with
@@ -1357,6 +1350,18 @@ let rec tt_expr pd ?(mode=`AllVar) (env : 'asm Env.env) pe =
     if alen <> len then rs_tyerror ~loc (PackWrongLength (len, alen));
     P.PappN (E.Opack (sz, pz), args), P.etw sz
 
+  | S.PEarray es ->
+     let loc = L.loc pe in
+     let es = List.map (tt_expr ~mode pd env) es in
+     let es = List.map (fun (e, ty) -> cast loc e ty (ETword (None, U8))) es in
+     let len = Conv.pos_of_int (List.length es) in
+     P.PappN (E.Oarray len, es), P.(ETarr (U8, PE (Pconst (Conv.z_of_pos len))))
+
+  | S.PEstring s ->
+     let es = array_of_string s in
+     let len = Conv.pos_of_int (List.length es) in
+     P.PappN (E.Oarray len, es), P.(ETarr (U8, PE (Pconst (Conv.z_of_pos len))))
+
   | S.PEIf (pe1, pe2, pe3) ->
     let e1, ty1 = tt_expr ~mode pd env pe1 in
     let e2, ty2 = tt_expr ~mode pd env pe2 in
@@ -2315,47 +2320,11 @@ let tt_fundef arch_info (env0 : 'asm Env.env) loc (pf : S.pfundef) : 'asm Env.en
   Env.Funs.push env0 fdef {fs_tin; fs_tout}
 
 (* -------------------------------------------------------------------- *)
-let tt_global_def pd env (gd:S.gpexpr) =
-  let f e =
-    let pe,ety = tt_expr ~mode:`AllVar pd env e in
-    (L.mk_loc e.pl_loc pe, ety) in
-  let array_of_string s =
-    L.unloc s |> String.to_list |> List.map @@ fun c ->
-    c |> Char.code |> Z.of_int |> fun z ->
-    P.(L.mk_loc (L.loc s) (Papp1 (op_word_of_int(Word, W.Unsigned, W.U8), Pconst z)), P.etw U8) in
-  match gd with
-  | S.GEword e ->
-    `Word (f e)
-  | S.GEarray es ->
-    `Array (List.map f es)
-  | S.GEstring e ->
-    `Array (array_of_string e)
-
 let tt_global pd (env : 'asm Env.env) _loc (gd: S.pglobal) : 'asm Env.env =
 
-  let open P in
-  let mk_pe ws (pe,ety) =
-    match ety with
-    | P.ETword(wk, ews) when wk = None && Utils0.cmp_le Wsize.wsize_cmp ws ews ->
-      L.unloc pe
-    | P.ETint -> Papp1 (op_word_of_int(Word, W.Unsigned, ws), L.unloc pe)
-    | _ -> rs_tyerror ~loc:(L.loc pe) (TypeMismatch (ety, P.etw ws))
-    in
-
-  let ty, d =
-    match tt_type pd env gd.S.pgd_type, tt_global_def pd env gd.S.pgd_val with
-    | P.ETword(None, ws) as ty, `Word (pe,ety) ->
-      let pe = mk_pe ws (pe,ety) in
-      ty, P.GEword pe
-    | (P.ETint | P.ETbool | P.ETword _), `Array _ ->
-      rs_tyerror ~loc:(L.loc gd.S.pgd_type) GlobArrayNotWord
-    | P.ETarr(ws, _n) as ty, `Array es ->
-      let pes = List.map (mk_pe ws) es in
-      ty, P.GEarray pes
-    | P.ETarr _, `Word _ ->
-      rs_tyerror ~loc:(L.loc gd.S.pgd_type) GlobWordNotArray
-    | ty,_ -> rs_tyerror ~loc:(L.loc gd.S.pgd_type) (InvalidTypeForGlobal ty)
-  in
+  let ty = tt_type pd env gd.S.pgd_type in
+  let d, dty = tt_expr ~mode:`AllVar pd env gd.S.pgd_val in
+  let d = cast (L.loc gd.S.pgd_name) d dty ty in
 
   let x = mk_var (L.unloc gd.S.pgd_name) W.Global ty (L.loc gd.S.pgd_name) [] in
 

diff --git a/compiler/src/printer.ml b/compiler/src/printer.ml
@@ -54,6 +54,8 @@ let pp_ge ~debug (pp_len: 'len pp) (pp_var: 'len gvar pp) : 'len gexpr pp =
     F.fprintf fmt "@[(%du%n)[%a]@]" (List.length es) (int_of_pe pe) (pp_list ",@ " (pp_expr NoAssoc priority_min)) es
   | PappN (Ocombine_flags c, es) ->
     F.fprintf fmt "@[%s(%a)@]" (string_of_combine_flags c) (pp_list ",@ " (pp_expr NoAssoc priority_min)) es
+  | PappN (E.Oarray len, es) ->
+     F.fprintf fmt "/* %du8 */ @[{ %a }@]" (Conv.int_of_pos len) (pp_list ",@ " (pp_expr NoAssoc priority_min)) es
   | Pif(_, e,e1,e2) ->
      let p = priority_ternary in
      optparent fmt prio side p "%a ? %a : %a" (pp_expr Left p) e (pp_expr NoAssoc p) e1 (pp_expr Right p) e2
@@ -268,10 +270,6 @@ let pp_gfun ~debug (pp_size:F.formatter -> 'size -> unit) pp_opn pp_var fmt fd =
 
 let pp_noinfo _ _ = ()
 
-let pp_gexpr ~debug pp_len pp_var fmt = function
-  | GEword e -> pp_ge ~debug pp_len pp_var fmt e
-  | GEarray es -> Format.fprintf fmt "{@[%a@]}" (pp_ges ~debug pp_len pp_var) es
-
 let pp_pitem ~debug pp_len pp_opn pp_var =
   let aux fmt = function
    | MIfun fd -> pp_gfun ~debug pp_len pp_opn pp_var fmt fd
@@ -283,7 +281,7 @@ let pp_pitem ~debug pp_len pp_opn pp_var =
       F.fprintf fmt "%a %a = %a;"
         (pp_gtype pp_len) x.v_ty
         pp_var x
-        (pp_gexpr ~debug pp_len pp_var) e
+        (pp_ge ~debug pp_len pp_var) e
  in
   aux
 

diff --git a/compiler/src/prog.ml b/compiler/src/prog.ml
@@ -125,14 +125,10 @@ type ('len, 'info, 'asm) gfunc = {
     f_ret  : 'len gvar_i list
   }
 
-type 'len ggexpr =
-  | GEword of 'len gexpr
-  | GEarray of 'len gexprs
-
 type ('len, 'info, 'asm) gmod_item =
   | MIfun   of ('len, 'info, 'asm) gfunc
   | MIparam of ('len gvar * 'len gexpr)
-  | MIglobal of ('len gvar * 'len ggexpr)
+  | MIglobal of ('len gvar * 'len gexpr)
 
 type ('len, 'info, 'asm) gprog = ('len, 'info, 'asm) gmod_item list
    (* first declaration occur at the end (i.e reverse order) *)

diff --git a/compiler/src/prog.mli b/compiler/src/prog.mli
@@ -92,14 +92,10 @@ type ('len, 'info, 'asm) gfunc = {
     f_ret  : 'len gvar_i list
   }
 
-type 'len ggexpr =
-  | GEword of 'len gexpr
-  | GEarray of 'len gexprs
-
 type ('len, 'info, 'asm) gmod_item =
   | MIfun   of ('len, 'info, 'asm) gfunc
   | MIparam of ('len gvar * 'len gexpr)
-  | MIglobal of ('len gvar * 'len ggexpr)
+  | MIglobal of ('len gvar * 'len gexpr)
 
 type ('len, 'info, 'asm) gprog = ('len, 'info, 'asm) gmod_item list
    (* first declaration occur at the end (i.e reverse order) *)

diff --git a/compiler/src/subst.ml b/compiler/src/subst.ml
@@ -122,10 +122,6 @@ let psubst_v subst =
     | _      -> e in
   aux
 
-let psubst_ge f = function
-  | GEword e -> GEword (psubst_e f e)
-  | GEarray es -> GEarray (List.map (psubst_e f) es)
-
 let psubst_prog (prog:('info, 'asm) pprog) =
   let subst = ref (Mpv.empty : pexpr Mpv.t) in
   let rec aux = function
@@ -142,7 +138,7 @@ let psubst_prog (prog:('info, 'asm) pprog) =
         let v =
           gsubst_gvar f {gv = L.mk_loc L._dummy v; gs = Expr.Sglob} in
         assert (not (is_gkvar v)); L.unloc v.gv in
-      let e = psubst_ge f e in
+      let e = psubst_e f e in
       subst := Mpv.add v (Pvar (gkglob (L.mk_loc L._dummy v'))) !subst;
       (v', e) :: g, p
     | MIfun fc :: items ->
@@ -249,10 +245,7 @@ let isubst_prog glob prog =
         gsubst_gvar subst_v {gv = L.mk_loc L._dummy x; gs = Expr.Sglob} in
       assert (not (is_gkvar x)); L.unloc x.gv in
 
-    let gd =
-      match gd with
-      | GEword e -> GEword (gsubst_e isubst_len subst_v e)
-      | GEarray es -> GEarray (List.map (gsubst_e isubst_len subst_v) es) in
+    let gd = gsubst_e isubst_len subst_v gd in
     x, gd in
   let glob = List.map isubst_glob glob in
 
@@ -334,20 +327,20 @@ let remove_params (prog : ('info, 'asm) pprog) =
   let doglob (x, e) =
     let gv =
       match x.v_ty, e with
-      | Bty (U ws), GEword e ->
+      | Bty (U ws), e ->
         begin try Global.Gword (ws, mk_word ws e)
         with NotAConstantExpr ->
-          hierror ~loc:x.v_dloc "the expression assigned to global variable %a must evaluate to a constant"
+          hierror ~loc:x.v_dloc "the expression assigned to global variable %a must evaluate to a constant word"
             (Printer.pp_var ~debug:false) x
         end
-      | Arr (_ws, n), GEarray es when List.length es <> n ->
+      | Arr (_ws, n), PappN (E.Oarray _len, es) when List.length es <> n ->
          let m = List.length es in
          hierror ~loc:x.v_dloc "array size mismatch for global variable %a: %d %s given (%d expected)"
            (Printer.pp_var ~debug:false) x
            (List.length es)
            (if m > 1 then "values" else "value")
            n
-      | Arr (ws, n), GEarray es ->
+      | Arr (ws, n), PappN (E.Oarray _len, es) ->
         let p = Conv.pos_of_int (n * size_of_ws ws) in
         let mk_word_i i e =
           try mk_word ws e
@@ -358,7 +351,11 @@ let remove_params (prog : ('info, 'asm) pprog) =
         in
         let t = Warray_.WArray.of_list ws (List.mapi mk_word_i es) in
         Global.Garr(p, t)
-      | _, _ -> assert false in
+      | Arr _, _ -> hierror ~loc:x.v_dloc "ill-typed global array"
+      | Bty (Bool | Int), _ ->
+         hierror ~loc:x.v_dloc "globals should have type word; found: ‘%a’"
+           PrintCommon.pp_ty x.v_ty
+    in
     add_glob x gv;
     x, gv
   in

diff --git a/compiler/src/syntax.ml b/compiler/src/syntax.ml
@@ -172,6 +172,8 @@ type pexpr_r =
   | PEGet    of [`Aligned|`Unaligned] option * arr_access * swsize L.located option * pident * pexpr * pexpr option
   | PEFetch  of mem_access
   | PEpack   of svsize * pexpr list
+  | PEarray of pexpr list
+  | PEstring of string
   | PEBool   of bool
   | PEInt    of int_representation
   | PECall   of pident * pexpr list
@@ -318,12 +320,7 @@ type pfundef = {
 }
 
 (* -------------------------------------------------------------------- *)
-type gpexpr =
-  | GEword  of pexpr
-  | GEarray of pexpr list
-  | GEstring of string L.located
-
-type pglobal = { pgd_type: ptype; pgd_name: pident ; pgd_val: gpexpr }
+type pglobal = { pgd_type: ptype; pgd_name: pident ; pgd_val: pexpr }
 
 (* -------------------------------------------------------------------- *)
 type pexec = {