From 7a6bb90048db7a254e959b1e3c308bac5fe6c418 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 11 Oct 2015 17:43:59 +0200 Subject: Use Coq strings instead of idents to name external and builtin functions. The AST.ident type represents source-level identifiers as unique positive numbers. However, the mapping identifiers <-> AST.ident differs between runs of CompCert on different source files. This is problematic when we need to produce or recognize external functions and builtin functions with fixed names, for example: * in $ARCH/Machregs.v to define the register conventions for builtin functions; * in the VST program logic from Princeton to treat thread primitives specially. So far, we used AST.ident_of_string to recover the ident associated with a string. However, this function is defined in OCaml and doesn't execute within Coq. This is a problem both for VST and for future executability of CompCert within Coq. This commit replaces "ident" by "string" in the arguments of EF_external, EF_builtin, EF_inline_asm, EF_annot, and EF_annot_val. This provides stable names for externals and builtins, as needed. For inline asm and annotations, it's a matter of taste, but using strings feels more natural. EF_debug keeps using idents, since some kinds of EF_debug annotations talk about program variables. --- backend/CMparser.mly | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'backend/CMparser.mly') diff --git a/backend/CMparser.mly b/backend/CMparser.mly index b48a486e..41bd35a1 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -35,9 +35,9 @@ type ef_token = let mkef sg toks = match toks with | [EFT_tok "extern"; EFT_string s] -> - EF_external(intern_string s, sg) + EF_external(coqstring_of_camlstring s, sg) | [EFT_tok "builtin"; EFT_string s] -> - EF_builtin(intern_string s, sg) + EF_builtin(coqstring_of_camlstring s, sg) | [EFT_tok "volatile"; EFT_tok "load"; EFT_chunk c] -> EF_vload c | [EFT_tok "volatile"; EFT_tok "store"; EFT_chunk c] -> @@ -49,12 +49,12 @@ let mkef sg toks = | [EFT_tok "memcpy"; EFT_tok "size"; EFT_int sz; EFT_tok "align"; EFT_int al] -> EF_memcpy(Z.of_sint32 sz, Z.of_sint32 al) | [EFT_tok "annot"; EFT_string txt] -> - EF_annot(intern_string txt, sg.sig_args) + EF_annot(coqstring_of_camlstring txt, sg.sig_args) | [EFT_tok "annot_val"; EFT_string txt] -> if sg.sig_args = [] then raise Parsing.Parse_error; - EF_annot_val(intern_string txt, List.hd sg.sig_args) + EF_annot_val(coqstring_of_camlstring txt, List.hd sg.sig_args) | [EFT_tok "inline_asm"; EFT_string txt] -> - EF_inline_asm(intern_string txt, sg, []) + EF_inline_asm(coqstring_of_camlstring txt, sg, []) | _ -> raise Parsing.Parse_error @@ -473,7 +473,7 @@ proc: fn_stackspace = $8; fn_body = $10 })) } | EXTERN STRINGLIT COLON signature - { (intern_string $2, Gfun(External(EF_external(intern_string $2,$4)))) } + { (intern_string $2, Gfun(External(EF_external(coqstring_of_camlstring $2,$4)))) } | EXTERN STRINGLIT EQUAL eftoks COLON signature { (intern_string $2, Gfun(External(mkef $6 $4))) } ; -- cgit From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- backend/CMparser.mly | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'backend/CMparser.mly') diff --git a/backend/CMparser.mly b/backend/CMparser.mly index 41bd35a1..5f189e7b 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -13,7 +13,7 @@ /* */ /* *********************************************************************/ -/* Note that this compiles a superset of the language defined by the AST, +/* Note that this compiles a superset of the language defined by the AST, including function calls in expressions, matches, while statements, etc. */ %{ @@ -123,7 +123,7 @@ let mkeval e = let c1 = convert_rexpr e1 in let cl = convert_rexpr_list el in prepend_seq !convert_accu (Scall(None, sg, c1, cl)) - | Rbuiltin(sg, pef, el) -> + | Rbuiltin(sg, pef, el) -> let ef = mkef sg pef in let cl = convert_rexpr_list el in prepend_seq !convert_accu (Sbuiltin(None, ef, cl)) @@ -322,9 +322,9 @@ let mkmatch expr cases = %token LESSLESSL %token LONG %token LONGLIT -%token LONGOFINT +%token LONGOFINT %token LONGOFINTU -%token LONGOFFLOAT +%token LONGOFFLOAT %token LONGUOFFLOAT %token LOOP %token LPAREN @@ -375,7 +375,7 @@ let mkmatch expr cases = %left CARET CARETL %left AMPERSAND AMPERSANDL %left EQUALEQUAL BANGEQUAL LESS LESSEQUAL GREATER GREATEREQUAL EQUALEQUALU BANGEQUALU LESSU LESSEQUALU GREATERU GREATEREQUALU EQUALEQUALF BANGEQUALF LESSF LESSEQUALF GREATERF GREATEREQUALF EQUALEQUALL BANGEQUALL LESSL LESSEQUALL GREATERL GREATEREQUALL EQUALEQUALLU BANGEQUALLU LESSLU LESSEQUALLU GREATERLU GREATEREQUALLU -%left LESSLESS GREATERGREATER GREATERGREATERU LESSLESSL GREATERGREATERL GREATERGREATERLU +%left LESSLESS GREATERGREATER GREATERGREATERU LESSLESSL GREATERGREATERL GREATERGREATERLU %left PLUS PLUSF PLUSL MINUS MINUSF MINUSL %left STAR SLASH PERCENT STARF SLASHF SLASHU PERCENTU STARL SLASHL SLASHLU PERCENTL PERCENTLU %nonassoc BANG TILDE TILDEL p_uminus ABSF INTOFFLOAT INTUOFFLOAT FLOATOFINT FLOATOFINTU INT8S INT8U INT16S INT16U FLOAT32 INTOFLONG LONGOFINT LONGOFINTU LONGOFFLOAT LONGUOFFLOAT FLOATOFLONG FLOATOFLONGU @@ -432,12 +432,12 @@ init_data_list: /* empty */ { [] } | init_data_list_1 { $1 } ; - + init_data_list_1: init_data { [$1] } | init_data_list_1 COMMA init_data { $3 :: $1 } ; - + init_data: INT8 INTLIT { Init_int8 (coqint_of_camlint $2) } | INT16 INTLIT { Init_int16 (coqint_of_camlint $2) } @@ -453,7 +453,7 @@ init_data: | LBRACKET INTLIT RBRACKET { Init_space (Z.of_sint32 $2) } | INTLIT LPAREN STRINGLIT RPAREN { Init_addrof (intern_string $3, coqint_of_camlint $1) } ; - + /* Procedures */ proc: @@ -472,14 +472,14 @@ proc: fn_vars = List.rev (tmp @ $9); fn_stackspace = $8; fn_body = $10 })) } - | EXTERN STRINGLIT COLON signature + | EXTERN STRINGLIT COLON signature { (intern_string $2, Gfun(External(EF_external(coqstring_of_camlstring $2,$4)))) } | EXTERN STRINGLIT EQUAL eftoks COLON signature { (intern_string $2, Gfun(External(mkef $6 $4))) } ; signature: - type_ + type_ { {sig_args = []; sig_res = Some $1; sig_cc = cc_default} } | VOID { {sig_args = []; sig_res = None; sig_cc = cc_default} } -- cgit