diff --git a/compiler/src/functionAnnotations.ml b/compiler/src/functionAnnotations.ml new file mode 100644 index 0000000000..e3fcfeee51 --- /dev/null +++ b/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; + } diff --git a/compiler/src/functionAnnotations.mli b/compiler/src/functionAnnotations.mli new file mode 100644 index 0000000000..c29fc93e70 --- /dev/null +++ b/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. *) diff --git a/compiler/src/latex_printer.ml b/compiler/src/latex_printer.ml index 93bba7395a..885966417d 100644 --- a/compiler/src/latex_printer.ml +++ b/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 "@[%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) diff --git a/compiler/src/parser.mly b/compiler/src/parser.mly index 4f05cb06df..4119c20976 100644 --- a/compiler/src/parser.mly +++ b/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 } diff --git a/compiler/src/pretyping.ml b/compiler/src/pretyping.ml index 7304550945..0767985977 100644 --- a/compiler/src/pretyping.ml +++ b/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 diff --git a/compiler/src/syntax.ml b/compiler/src/syntax.ml index 95c7a6b67b..490dd4cfe6 100644 --- a/compiler/src/syntax.ml +++ b/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; }