From a2e86c94c798c10363d48581feabde5bbddf46eb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 17 Jun 2024 15:14:40 +0200
Subject: [PATCH] [kernel/modules] fix long type parsing
---
src/kernel_internals/parsing/logic_lexer.mll | 3 +-
src/kernel_internals/parsing/logic_parser.mly | 51 ++++++++++++-------
.../ast_queries/logic_parse_string.ml | 4 +-
3 files changed, 37 insertions(+), 21 deletions(-)
diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index a7ccd95245..f9384a540b 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -267,8 +267,7 @@
end
let longident lexbuf =
- let s = lexeme lexbuf in
- if Logic_env.typename_status s then TYPENAME s else LONGIDENT s
+ let s = lexeme lexbuf in LONGIDENT s
(* Update lexer buffer. *)
let update_line_pos lexbuf line =
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 87c9b3a511..a0113cf7b5 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -558,13 +558,13 @@ lexpr_inner:
| RESULT { info $sloc PLresult }
| SEPARATED LPAR ne_lexpr_list RPAR
{ info $sloc (PLseparated $3) }
-| full_identifier LPAR ne_lexpr_list RPAR
+| symbol_identifier LPAR ne_lexpr_list RPAR
{ info $sloc (PLapp ($1, [], $3)) }
-| full_identifier LBRACE ne_label_args RBRACE LPAR ne_lexpr_list RPAR
+| symbol_identifier LBRACE ne_label_args RBRACE LPAR ne_lexpr_list RPAR
{ info $sloc (PLapp ($1, $3, $6)) }
-| full_identifier LBRACE ne_label_args RBRACE
+| symbol_identifier LBRACE ne_label_args RBRACE
{ info $sloc (PLapp ($1, $3, [])) }
-| full_identifier { info $sloc (PLvar $1) }
+| symbol_identifier { info $sloc (PLvar $1) }
| PI { info $sloc (PLvar "\\pi") }
| lexpr_inner GTGT lexpr_inner { info $sloc (PLbinop ($1, Brshift, $3))}
| lexpr_inner LTLT lexpr_inner { info $sloc (PLbinop ($1, Blshift, $3))}
@@ -579,18 +579,22 @@ lexpr_inner:
| EMPTY { info $sloc PLempty }
| BSUNION LPAR lexpr_list RPAR { info $sloc (PLunion $3) }
| INTER LPAR lexpr_list RPAR { info $sloc (PLinter $3) }
-| LBRACE lexpr_list RBRACE
- { info $sloc (PLset ($2)) }
-| LBRACE lexpr PIPE binders RBRACE
+| LBRACE RBRACE
+ { info $sloc (PLset []) }
+| LBRACE lexpr_inner RBRACE
+ { info $sloc (PLset [$2]) }
+| LBRACE lexpr_inner COMMA lexpr_list RBRACE
+ { info $sloc (PLset ($2 :: $4)) }
+| LBRACE lexpr_inner PIPE binders RBRACE
{ info $sloc (PLcomprehension ($2,$4,None)) }
-| LBRACE lexpr PIPE binders SEMICOLON lexpr RBRACE
+| LBRACE lexpr_inner PIPE binders SEMICOLON lexpr RBRACE
{ info $sloc (PLcomprehension ($2,$4,Some $6)) }
/* Aggregated object initialization */
| LBRACE field_init RBRACE
{ info $sloc (PLinitField($2)) }
| LBRACE array_init RBRACE
{ info $sloc (PLinitIndex($2)) }
-| LBRACE lexpr WITH update RBRACE
+| LBRACE lexpr_inner WITH update RBRACE
{ List.fold_left
(fun a (path,upd_val) -> info $sloc (PLupdate(a,path,upd_val))) $2 $4 }
/*
@@ -683,7 +687,7 @@ binders_reentrance:
;
decl_spec:
-| type_spec(typename) var_spec { ($1, let (modif, name) = $2 in (modif $1, name)) }
+| type_spec(typesymbol) var_spec { ($1, let (modif, name) = $2 in (modif $1, name)) }
;
var_spec:
@@ -761,10 +765,15 @@ logic_type_gen(tname):
typename:
| name = TYPENAME { name }
+;
+
+typesymbol:
+| name = TYPENAME { name }
+| name = LONGIDENT { name }
/* TODO treat the case of an ACSL keyword that is also a typedef */
;
-logic_type: logic_type_gen(typename) { $1 }
+logic_type: logic_type_gen(typesymbol) { $1 }
cv:
CONST { cv_const }
@@ -772,16 +781,16 @@ cv:
| BSGHOST { cv_ghost }
;
-type_spec_cv(tname):
- type_spec(tname) cv_after { $2 $1 }
-| cv type_spec_cv(tname) { LTattribute ($2, $1) }
+type_spec_cv:
+ type_spec(TYPENAME) cv_after { $2 $1 }
+| cv type_spec_cv { LTattribute ($2, $1) }
cv_after:
/* empty */ { fun t -> t }
| cv cv_after { fun t -> $2 (LTattribute (t,$1)) }
cast_logic_type:
- | type_spec_cv(TYPENAME) abs_spec_cv_option { $2 $1 }
+ | type_spec_cv abs_spec_cv_option { $2 $1 }
;
logic_rt_type:
@@ -902,9 +911,13 @@ ne_logic_type_list(tname):
| l = separated_nonempty_list(COMMA,logic_type_gen(tname)) { l }
;
+symbol_identifier:
+| id = full_identifier { id }
+| name = LONGIDENT { name }
+;
+
full_identifier:
| id = identifier { id }
-| id = LONGIDENT { id }
| ADMIT { "admit" }
| ALLOCATES { "allocates" }
| ASSERT { "assert" }
@@ -1866,12 +1879,14 @@ any_identifier:
identifier_or_typename:
| TYPENAME { $1 }
+| LONGIDENT { $1 }
| full_identifier { $1 }
-
+;
identifier_or_typename_full: /* allowed as C field names */
| is_acsl_typename { $1 }
-| identifier_or_typename { $1 }
+| TYPENAME { $1 }
+| full_identifier { $1 }
;
identifier: /* part included into 'identifier_or_typename', but duplicated to avoid parsing conflicts */
diff --git a/src/kernel_services/ast_queries/logic_parse_string.ml b/src/kernel_services/ast_queries/logic_parse_string.ml
index b6b6e27373..b37125a59c 100644
--- a/src/kernel_services/ast_queries/logic_parse_string.ml
+++ b/src/kernel_services/ast_queries/logic_parse_string.ml
@@ -122,7 +122,9 @@ let sync_typedefs () =
Logic_env.reset_typenames ();
Globals.Types.iter_types
(fun name _ ns ->
- if ns = Logic_typing.Typedef then Logic_env.add_typename name)
+ if ns = Logic_typing.Typedef then
+ try ignore @@ String.index name ':' with Not_found ->
+ Logic_env.add_typename name)
let wrap f parsetree loc =
match parsetree with
--
GitLab