Parser: allow expressions in annotations

compiler/src/functionAnnotations.ml

@@ -0,0 +1,89 @@
+open Utils
+open Prog
+
+(* -------------------------------------------------------------------- *)
+let rec pannot_to_annotations (pannot : Syntax.pannotations) : Annotations.annotations =
+  List.map pannot_to_annotation pannot
+
+and pannot_to_annotation ((id, pattri) : Syntax.pannotation) : Annotations.annotation =
+  (id, Option.map pattri_to_attribute pattri)
+
+and pattri_to_attribute (pattri: Syntax.pattribute) : Annotations.attribute =
+  let loc = L.loc pattri in
+  L.mk_loc loc (pattri_to_simple_attribute (L.unloc pattri))
+
+and pattri_to_simple_attribute (pattri: Syntax.psimple_attribute) : Annotations.simple_attribute =
+  match pattri with
+  | PAstring s -> Astring s
+  | PAws ws -> Aws ws
+  | PAstruct s -> Astruct (pannot_to_annotations s)
+  | PAexpr e ->
+      match L.unloc e with
+      | PEVar id -> Aid (L.unloc id)
+      | PEInt ir -> Aint (Syntax.parse_int ir)
+      | PEOp1 (`Neg None, {L.pl_desc = PEInt ir}) -> Aint (Z.neg (Syntax.parse_int ir))
+      | _ ->
+        hierror ~kind:"syntax" ~loc:(Lone (L.loc e))
+          "complex expressions not allowed in annotations"
+
+(* -------------------------------------------------------------------- *)
+let process_f_annot loc funname f_cc annot =
+  let open FInfo in
+
+  let annot = pannot_to_annotations annot in
+  let mk_ra = Annot.filter_string_list None ["stack", OnStack; "reg", OnReg] in
+
+  let retaddr_kind =
+    let kind = Annot.ensure_uniq1 "returnaddress" mk_ra annot in
+    if kind <> None && not (FInfo.is_subroutine f_cc) then
+      hierror
+        ~loc:(Lone loc)
+        ~funname
+        ~kind:"unexpected annotation"
+        "returnaddress only applies to subroutines";
+    kind
+  in
+
+  let stack_zero_strategy =
+
+    let strategy =
+      let mk_szs = Annot.filter_string_list None Glob_options.stack_zero_strategies in
+      let strategy = Annot.ensure_uniq1 "stackzero" mk_szs annot in
+      if strategy <> None && not (FInfo.is_export f_cc) then
+        hierror
+          ~loc:(Lone loc)
+          ~funname
+          ~kind:"unexpected annotation"
+          "stackzero only applies to export functions";
+      if Option.is_none strategy then
+        !Glob_options.stack_zero_strategy
+      else
+        strategy
+    in
+
+    let size =
+      let size = Annot.ensure_uniq1 "stackzerosize" (Annot.wsize None) annot in
+      if Option.is_none size then
+        !Glob_options.stack_zero_size
+      else
+        size
+    in
+
+    match strategy, size with
+    | None, None -> None
+    | None, Some _ ->
+        warning Always
+          (L.i_loc0 loc)
+          "\"stackzerosize\" is ignored, since you did not specify a strategy with attribute \"stackzero\"";
+        None
+    | Some szs, _ -> Some (szs, size)
+  in
+
+  { retaddr_kind;
+    stack_allocation_size = Annot.ensure_uniq1 "stackallocsize" (Annot.pos_int None) annot;
+    stack_size            = Annot.ensure_uniq1 "stacksize"      (Annot.pos_int None) annot;
+    stack_align           = Annot.ensure_uniq1 "stackalign"     (Annot.wsize None)   annot;
+    max_call_depth        = Annot.ensure_uniq1 "calldepth"      (Annot.pos_int None) annot;
+    stack_zero_strategy;
+    f_user_annot          = annot;
+  }

compiler/src/functionAnnotations.mli

@@ -0,0 +1,11 @@
+val pannot_to_annotations : Syntax.pannotations -> Annotations.annotations
+(** Remove expressions from annotations. Raises [HiError] when it encounters too
+    complex expressions. *)
+
+val process_f_annot :
+  Location.t ->
+  string ->
+  FInfo.call_conv ->
+  Syntax.pannotations ->
+  FInfo.f_annot
+(** Extracts a few well-known attributes from the annotation of a function. *)

compiler/src/latex_printer.ml

@@ -171,12 +171,10 @@ let pp_aligned =
 
 let rec pp_simple_attribute fmt a =
   match L.unloc a with
-  | Aint i -> Z.pp_print fmt i
-  | Aid s -> pannot fmt s
-  | Astring s -> pannot fmt (Format.asprintf "%a" pp_string s)
-  | Aws ws -> Format.fprintf fmt "%a" ptype (string_of_wsize ws)
-  | Astruct struct_ -> Format.fprintf fmt "(%a)" pp_struct_attribute struct_
-
+  | PAstring s -> pannot fmt (Format.asprintf "%a" pp_string s)
+  | PAws ws -> Format.fprintf fmt "%a" ptype (string_of_wsize ws)
+  | PAstruct struct_ -> Format.fprintf fmt "\\{%a\\}" pp_struct_attribute struct_
+  | PAexpr e -> pp_expr fmt e
 and pp_struct_attribute fmt struct_ =
   Format.fprintf fmt "@[<hov 2>%a@]" (pp_list ",@ " pp_annotation) struct_
 
@@ -187,19 +185,12 @@ and pp_attribute fmt = function
 and pp_annotation fmt (id, atr) =
   Format.fprintf fmt "%a%a" pp_attribute_key (L.unloc id) pp_attribute atr
 
-let pp_top_annotations fmt annot =
-  match annot with
-  | []  -> ()
-  | [a] -> Format.fprintf fmt "@[%a%a\\\\@]\n" sharp () pp_annotation a
-  | _   -> Format.fprintf fmt "#[%a]" pp_struct_attribute annot
-
-let pp_inline_annotations fmt annot =
+and pp_annotations fmt annot =
   match annot with
   | []  -> ()
-  | [a] -> Format.fprintf fmt "%a%a " sharp () pp_annotation a
   | _   -> Format.fprintf fmt "#[%a]" pp_struct_attribute annot
 
-let rec pp_expr_rec prio fmt pe =
+and pp_expr_rec prio fmt pe =
   match L.unloc pe with
   | PEParens e -> pp_expr_rec prio fmt e
   | PEVar x -> pp_var fmt x
@@ -267,7 +258,7 @@ let pp_sto_ty fmt (sto, ty) =
   F.fprintf fmt "%a %a" pp_storage sto pp_type ty
 
 let pp_annot_sto_ty fmt (annot, stoty) =
-  F.fprintf fmt "%a%a" pp_inline_annotations annot pp_sto_ty stoty
+  F.fprintf fmt "%a%a" pp_annotations annot pp_sto_ty stoty
 
 let pp_args fmt (sty, xs) =
   F.fprintf
@@ -281,7 +272,7 @@ let pp_varinit fmt v =
   F.fprintf fmt "%a = %a" pp_var x pp_expr e
 
 let pp_annot_args fmt  (annot, args) =
-  F.fprintf fmt "%a%a" pp_inline_annotations annot pp_args args
+  F.fprintf fmt "%a%a" pp_annotations annot pp_args args
 
 let pp_rty =
   pp_opt
@@ -312,7 +303,7 @@ let pp_sidecond fmt =
   F.fprintf fmt " %a %a" kw "if" pp_expr
 
 let rec pp_instr depth fmt (annot, p) =
-  if annot <> [] then F.fprintf fmt "%a%a" indent depth pp_top_annotations annot;
+  if annot <> [] then F.fprintf fmt "%a%a" indent depth pp_annotations annot;
   indent fmt depth;
   match L.unloc p with
   | PIdecl (sty, vds) -> F.fprintf fmt "%a %a;" pp_sto_ty sty (pp_list " " pp_var) vds
@@ -390,7 +381,7 @@ let pp_fundef fmt { pdf_cc ; pdf_name ; pdf_args ; pdf_rty ; pdf_body ; pdf_anno
   F.fprintf
     fmt
     "%a%a%a %a(%a)%a %a"
-    pp_top_annotations pdf_annot
+    pp_annotations pdf_annot
     pp_cc pdf_cc
     kw "fn"
     dname (L.unloc pdf_name)

compiler/src/parser.mly

@@ -125,20 +125,15 @@ annotationlabel:
   | id=loc(keyword) { id }
   | s=loc(STRING) { s }
 
-int:
-  | i=INT       { Syntax.parse_int i }
-  | MINUS i=INT { Z.neg (Syntax.parse_int i ) }
-
 simple_attribute:
-  | i=int          { Aint i    }
-  | id=NID         { Aid id    }
-  | s=STRING       { Astring s }
-  | s=keyword      { Astring s }
-  | ws=utype       { Aws (fst ws) }
+  | e=pexpr        { PAexpr e}
+  | s=STRING       { PAstring s }
+  | s=keyword      { PAstring s }
+  | ws=utype       { PAws (fst ws) }
 
 attribute:
   | EQ ap=loc(simple_attribute) { ap }
-  | EQ s=loc(braces(struct_annot)) { Location.mk_loc (Location.loc s) (Astruct (Location.unloc s)) }
+  | EQ s=loc(braces(struct_annot)) { Location.mk_loc (Location.loc s) (PAstruct (Location.unloc s)) }
 
 annotation:
   | k=annotationlabel v=attribute? { k, v }

compiler/src/pretyping.ml

@@ -1,5 +1,6 @@
 (* -------------------------------------------------------------------- *)
 open Utils
+open FunctionAnnotations
 module Path = BatPathGen.OfString
 module F = Format
 module L = Location
@@ -1754,6 +1755,7 @@ type ('a, 'b, 'c, 'd, 'e, 'f, 'g) arch_info = {
 }
 
 let tt_lvalues arch_info env loc (pimp, pls) implicit tys =
+  let pimp = Option.map (fun pimp -> L.mk_loc (L.loc pimp) (pannot_to_annotations (L.unloc pimp))) pimp in
   let loc = loc_of_tuples loc (List.map P.L.loc pls) in
 
   let combines =
@@ -1930,11 +1932,12 @@ let assign_from_decl decl =
   (None, [d]), `Raw, e, None
 
 let tt_annot_paramdecls dfl_writable pd env (annot, (ty,vs)) =
-  let aty = annot, ty in
+  let aty = pannot_to_annotations annot, ty in
   let vars = List.map (fun v -> aty, v) vs in
   tt_vardecls_push dfl_writable pd env vars
 
-let rec tt_instr arch_info (env : 'asm Env.env) ((annot,pi) : S.pinstr) : 'asm Env.env * (unit, 'asm) P.pinstr list  =
+let rec tt_instr arch_info (env : 'asm Env.env) ((pannot,pi) : S.pinstr) : 'asm Env.env * (unit, 'asm) P.pinstr list  =
+  let annot = pannot_to_annotations pannot in
   let mk_i ?(annot=annot) instr =
     { P.i_desc = instr; P.i_loc = L.of_loc pi; P.i_info = (); P.i_annot = annot} in
   let default_tag = if Annotations.has_symbol "keep" annot then E.AT_keep else E.AT_none in
@@ -2222,69 +2225,6 @@ let tt_call_conv _loc params returns cc =
     else
       FInfo.Export
 
-(* -------------------------------------------------------------------- *)
-
-let process_f_annot loc funname f_cc annot =
-  let open FInfo in
-
-  let mk_ra = Annot.filter_string_list None ["stack", OnStack; "reg", OnReg] in
-
-  let retaddr_kind =
-    let kind = Annot.ensure_uniq1 "returnaddress" mk_ra annot in
-    if kind <> None && not (FInfo.is_subroutine f_cc) then
-      hierror
-        ~loc:(Lone loc)
-        ~funname
-        ~kind:"unexpected annotation"
-        "returnaddress only applies to subroutines";
-    kind
-  in
-
-  let stack_zero_strategy =
-
-    let strategy =
-      let mk_szs = Annot.filter_string_list None Glob_options.stack_zero_strategies in
-      let strategy = Annot.ensure_uniq1 "stackzero" mk_szs annot in
-      if strategy <> None && not (FInfo.is_export f_cc) then
-        hierror
-          ~loc:(Lone loc)
-          ~funname
-          ~kind:"unexpected annotation"
-          "stackzero only applies to export functions";
-      if Option.is_none strategy then
-        !Glob_options.stack_zero_strategy
-      else
-        strategy
-    in
-
-    let size =
-      let size = Annot.ensure_uniq1 "stackzerosize" (Annot.wsize None) annot in
-      if Option.is_none size then
-        !Glob_options.stack_zero_size
-      else
-        size
-    in
-
-    match strategy, size with
-    | None, None -> None
-    | None, Some _ ->
-        warning Always
-          (L.i_loc0 loc)
-          "\"stackzerosize\" is ignored, since you did not specify a strategy with attribute \"stackzero\"";
-        None
-    | Some szs, _ -> Some (szs, size)
-  in
-
-  { retaddr_kind;
-    stack_allocation_size = Annot.ensure_uniq1 "stackallocsize" (Annot.pos_int None) annot;
-    stack_size            = Annot.ensure_uniq1 "stacksize"      (Annot.pos_int None) annot;
-    stack_align           = Annot.ensure_uniq1 "stackalign"     (Annot.wsize None)   annot;
-    max_call_depth        = Annot.ensure_uniq1 "calldepth"      (Annot.pos_int None) annot;
-    stack_zero_strategy;
-    f_user_annot          = annot;
-  }
-
-
 (* -------------------------------------------------------------------- *)
 (* Compute the set of declared variables                                *)
 let rec add_reserved_i env (_,i) =
@@ -2350,6 +2290,7 @@ let tt_fundef arch_info (env0 : 'asm Env.env) loc (pf : S.pfundef) : 'asm Env.en
     env, List.flatten args in
   let fs_tout = Option.map_default (List.map (tt_type arch_info.pd env |- snd |- snd)) [] pf.pdf_rty in
   let ret_annot = Option.map_default (List.map fst) [] pf.pdf_rty in
+  let ret_annot = List.map pannot_to_annotations ret_annot in
   let body, ret_loc, xret = tt_funbody arch_info envb pf.pdf_body in
   let f_args = List.map (fun x -> L.mk_loc (L.loc x) (fst (L.unloc x))) args in
   let fs_tin = List.map (fun x -> snd (L.unloc x)) args in

compiler/src/syntax.ml

@@ -185,6 +185,19 @@ and pexpr = pexpr_r L.located
 
 and mem_access = [ `Aligned | `Unaligned ] option * swsize L.located option * pexpr
 
+(* -------------------------------------------------------------------- *)
+type psimple_attribute =
+  | PAstring of string
+  | PAws     of wsize
+  | PAstruct of pannotations
+  | PAexpr   of pexpr
+
+and pattribute = psimple_attribute Location.located
+
+and pannotation = pident * pattribute option
+
+and pannotations = pannotation list
+
 (* -------------------------------------------------------------------- *)
 and psizetype = TypeWsize of swsize | TypeSizeAlias of pident
 and ptype_r = TBool | TInt | TWord of swsize | TArray of psizetype * pexpr | TAlias of pident
@@ -197,7 +210,7 @@ type pstorage = [ `Reg of ptr | `Stack of ptr | `Inline | `Global]
 
 (* -------------------------------------------------------------------- *)
 type pstotype = pstorage * ptype
-type annot_pstotype = annotations * pstotype
+type annot_pstotype = pannotations * pstotype
 (* -------------------------------------------------------------------- *)
 type plvalue_r =
   | PLIgnore
@@ -227,7 +240,7 @@ type peqop = [
 (* -------------------------------------------------------------------- *)
 type align = [`Align | `NoAlign]
 
-type plvals = annotations L.located option * plvalue list
+type plvals = pannotations L.located option * plvalue list
 
 
 type vardecls = pstotype * pident list
@@ -251,7 +264,7 @@ type pinstr_r =
 and pblock_r = pinstr list
 and fordir   = [ `Down | `Up ]
 
-and pinstr = annotations * pinstr_r L.located
+and pinstr = pannotations * pinstr_r L.located
 and pblock = pblock_r L.located
 
 let string_of_sizetype =
@@ -296,11 +309,11 @@ type pcall_conv = [
 type paramdecls = pstotype * pident list
 
 type pfundef = {
-  pdf_annot : annotations;
+  pdf_annot : pannotations;
   pdf_cc   : pcall_conv option;
   pdf_name : pident;
-  pdf_args : (annotations * paramdecls) list;
-  pdf_rty  : (annotations * pstotype) list option;
+  pdf_args : (pannotations * paramdecls) list;
+  pdf_rty  : (pannotations * pstotype) list option;
   pdf_body : pfunbody;
 }