Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Separating the C and CN parsing #342

Draft
wants to merge 7 commits into
base: master
Choose a base branch
from
Draft

Separating the C and CN parsing #342

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
7b20666
Adding a CN lexer and a copy of the CN grammar.
kmemarian Jun 22, 2024
c0c2dd0
Adding a separate module for CN's tokens (and using it in the new Lex…
kmemarian Jun 22, 2024
579220b
CN: renaming some tokens, the CN_ prefixes are no longer needed
kmemarian Jun 22, 2024
44e5a05
CN: polishing token declarations in the parser
kmemarian Jun 22, 2024
58ce851
CN: using the new lexer/parser -- BREAKING CN (no parsing of ctypes) …
kmemarian Jun 22, 2024
e6d2c3b
Removing CN parts from the C lexer
kmemarian Jun 22, 2024
c96a1ad
CN: first attempt at dealing with C type-names in the new CN parser
kmemarian Jun 22, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions backend/cn/parse.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ let fiddle_at_hack string =
fix ss

let debug_tokens loc string =
let (toks, pos) = C_parser_driver.diagnostic_get_tokens ~inside_cn:true loc string in
let (toks, pos) = C_parser_driver.diagnostic_get_cn_tokens loc string in
let pp_int_pair (x, y) = Pp.(parens (int x ^^ comma ^^^ int y)) in
Pp.item "failed to parse tokens" (Pp.braces (Pp.list Pp.string toks))
^/^ Pp.item "(line, col)" (Pp.braces (Pp.list pp_int_pair pos))
Expand All @@ -54,13 +54,13 @@ let parse parser_start (loc, string) =
let cn_statements annots =
annots
|> get_cerb_magic_attr
|> ListM.concat_mapM (parse C_parser.cn_statements)
|> ListM.concat_mapM (parse Cn_parser.cn_statements)

let function_spec (Attrs attributes) =
let@ conditions =
[Aattrs (Attrs (List.rev attributes))]
|> get_cerb_magic_attr
|> ListM.concat_mapM (parse C_parser.function_spec) in
|> ListM.concat_mapM (parse Cn_parser.function_spec) in
ListM.fold_leftM (fun acc cond ->
match cond, acc with
| (Cn.CN_trusted loc), (_, [], [], [], []) ->
Expand All @@ -86,7 +86,7 @@ let loop_spec attrs =
[Aattrs attrs]
|> get_cerb_magic_attr
|> ListM.concat_mapM (fun (loc, arg) ->
let@ (Cn.CN_inv (_loc, conds)) = parse C_parser.loop_spec (loc, arg) in
let@ (Cn.CN_inv (_loc, conds)) = parse Cn_parser.loop_spec (loc, arg) in
return conds)


98 changes: 2 additions & 96 deletions parsers/c/c_lexer.mll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ open Tokens
exception Error of Errors.cparser_cause

type flags = {
inside_cn : bool;
magic_comment_char : char;
at_magic_comments : bool;
}
Expand Down Expand Up @@ -91,74 +90,6 @@ let lexicon: (string, token) Hashtbl.t =
let add (key, builder) = Hashtbl.add lexicon key builder in
List.iter add keywords; lexicon


(* BEGIN CN *)
let cn_keywords: (string * Tokens.token) list = [
"good" , CN_GOOD;
"bool" , CN_BOOL;
"boolean" , CN_BOOL;
"CN_bool" , CN_BOOL;
"integer" , CN_INTEGER;
"u8" , CN_BITS (`U,8);
"u16" , CN_BITS (`U,16);
"u32" , CN_BITS (`U,32);
"u64" , CN_BITS (`U,64);
"u128" , CN_BITS (`U,128);
"i8" , CN_BITS (`I,8);
"i16" , CN_BITS (`I,16);
"i32" , CN_BITS (`I,32);
"i64" , CN_BITS (`I,64);
"i128" , CN_BITS (`I,128);
"real" , CN_REAL;
"pointer" , CN_POINTER;
"alloc_id" , CN_ALLOC_ID;
"map" , CN_MAP;
"list" , CN_LIST;
"tuple" , CN_TUPLE;
"set" , CN_SET;
"let" , CN_LET;
"take" , CN_TAKE;
"Owned" , CN_OWNED;
"Block" , CN_BLOCK;
"each" , CN_EACH;
"NULL" , CN_NULL;
"true" , CN_TRUE;
"false" , CN_FALSE;
"requires" , CN_REQUIRES;
"ensures" , CN_ENSURES;
"inv" , CN_INV;
"accesses" , CN_ACCESSES;
"trusted" , CN_TRUSTED;
"cn_function" , CN_FUNCTION;
"spec" , CN_SPEC;
"unchanged" , CN_UNCHANGED;
"pack" , CN_PACK;
"unpack" , CN_UNPACK;
"instantiate" , CN_INSTANTIATE;
"print" , CN_PRINT;
"split_case" , CN_SPLIT_CASE;
"extract" , CN_EXTRACT;
"array_shift" , CN_ARRAY_SHIFT;
"member_shift" , CN_MEMBER_SHIFT;
"have" , CN_HAVE;
"unfold" , CN_UNFOLD;
"apply" , CN_APPLY;
"match" , CN_MATCH;
"predicate" , CN_PREDICATE;
"function" , CN_FUNCTION;
"lemma" , CN_LEMMA;
"datatype" , CN_DATATYPE;
"type_synonym" , CN_TYPE_SYNONYM;
"_" , CN_WILD;
]

let cn_lexicon: (string, token) Hashtbl.t =
let cn_lexicon = Hashtbl.create 0 in
let add (key, builder) = Hashtbl.add cn_lexicon key builder in
List.iter add cn_keywords; cn_lexicon
(* END CN *)


let lex_comment remainder lexbuf =
let ch = lexeme_char lexbuf 0 in
if ch = '\n' then new_line lexbuf;
Expand Down Expand Up @@ -339,9 +270,6 @@ let whitespace_char = [' ' '\t' (*'\n'*) '\012' '\r']
let lbrack_lbrack = '[' whitespace_char* '['
(*let rbrack_rbrack = ']' whitespace_char* ']'*)

(* For CN *)
let cn_integer_width = ("8" | "16" | "32" | "64" | "128")

(* ========================================================================== *)

rule s_char_sequence = parse
Expand Down Expand Up @@ -437,12 +365,6 @@ and initial flags = parse
{ CONSTANT (Cabs.CabsInteger_const (str, Some Cabs.CabsSuffix_UL)) }
| (integer_constant as str) long_long_suffix unsigned_suffix
{ CONSTANT (Cabs.CabsInteger_const (str, Some Cabs.CabsSuffix_ULL)) }
(* For CN. Copying and adjusting Kayvan's code from above. *)
| (integer_constant as str) 'u' (cn_integer_width as n)
{ CN_CONSTANT (str, `U, int_of_string n) }
| (integer_constant as str) 'i' (cn_integer_width as n)
{ CN_CONSTANT (str, `I, int_of_string n) }
(* /For CN. *)
| (integer_constant as str)
{ CONSTANT (Cabs.CabsInteger_const (str, None)) }

Expand Down Expand Up @@ -550,26 +472,10 @@ and initial flags = parse
| "|||" { PIPES }
| "}-}" { RBRACES }

(* copied over from backend/cn/assertion_lexer.mll *)
| ['A'-'Z']['0'-'9' 'A'-'Z' 'a'-'z' '_']* as id
{
if flags.inside_cn then
try Hashtbl.find cn_lexicon id
with Not_found ->
UNAME id
else
UNAME id
}

| identifier as id
{ try
Hashtbl.find lexicon id
with Not_found ->
if flags.inside_cn then
try Hashtbl.find cn_lexicon id
with Not_found ->
LNAME id
else
LNAME id
}
| eof
Expand All @@ -586,7 +492,7 @@ type lexer_state =

let lexer_state = ref LSRegular

let lexer : inside_cn:bool -> lexbuf -> token = fun ~inside_cn lexbuf ->
let lexer : lexbuf -> token = fun lexbuf ->
match !lexer_state with
| LSRegular ->
let at_magic_comments = Switches.(has_switch SW_at_magic_comments) in
Expand All @@ -595,7 +501,7 @@ let lexer : inside_cn:bool -> lexbuf -> token = fun ~inside_cn lexbuf ->
then '$'
else '@'
in
begin match initial { inside_cn; at_magic_comments; magic_comment_char } lexbuf with
begin match initial { at_magic_comments; magic_comment_char } lexbuf with
| LNAME i as tok -> lexer_state := LSIdentifier i; tok
| UNAME i as tok -> lexer_state := LSIdentifier i; tok
| _ as tok -> lexer_state := LSRegular; tok
Expand Down
5 changes: 5 additions & 0 deletions parsers/c/c_parser.mly
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -316,6 +316,7 @@ type asm_qualifier =
located_string_literal

%start<Cerb_frontend.Cabs.translation_unit> translation_unit
%start<Cerb_frontend.Cabs.type_name> type_name_eof
%start function_spec
%start loop_spec
%start cn_statements
Expand Down Expand Up @@ -1778,6 +1779,10 @@ balanced_token:
{ strs }
;

type_name_eof:
| ty= type_name EOF
{ ty }

(* BEGIN CN *)
(* CN assertion language *****************************************************)
(*
Expand Down
16 changes: 9 additions & 7 deletions parsers/c/c_parser_driver.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
open Cerb_frontend
[@@@warning "-33"] open Cn_lexer (* TODO: working-in-progress. this is to get the module built *)

let after_before_msg offset buffer (lexbuf : Lexing.lexbuf) =
let show_token (start, curr) =
Expand Down Expand Up @@ -50,21 +51,22 @@ let start_pos = function
| Loc_regions ((loc, _) :: _, _) -> Some loc
| _ -> None

let diagnostic_get_tokens ~inside_cn loc string =
(* TODO(K): move this to the CN backend *)
let diagnostic_get_cn_tokens loc string =
(* `C_lexer.magic_token' ensures `loc` is a region *)
let start_pos = Option.get @@ start_pos loc in
let lexbuf = Lexing.from_string string in
let rec relex (toks, pos) =
try
match C_lexer.lexer ~inside_cn lexbuf with
| Tokens.EOF -> (List.rev ("EOF" :: toks), List.rev pos)
match Cn_lexer.lexer lexbuf with
| Cn_tokens.EOF -> (List.rev ("EOF" :: toks), List.rev pos)
| t ->
let Lexing.{ pos_lnum; pos_bol; pos_cnum; _ } = lexbuf.lex_start_p in
let (line, col) =
(* the first line needs to have columns shifted by /*@ but the rest do not *)
let col_off = if pos_lnum > 1 then 1 else start_pos.pos_cnum - start_pos.pos_bol + 1 in
(pos_lnum + start_pos.pos_lnum, col_off + pos_cnum - pos_bol) in
relex (Tokens.string_of_token t :: toks, (line, col) :: pos)
relex (Cn_tokens.string_of_token t :: toks, (line, col) :: pos)
with
C_lexer.Error err ->
(List.rev (Pp_errors.string_of_cparser_cause err :: toks), List.rev pos)
Expand All @@ -79,7 +81,7 @@ let parse_loc_string parse (loc, str) =
Lexing.set_filename lexbuf (Option.value ~default:"<none>" (Cerb_location.get_filename loc));
handle
parse
(MenhirLib.ErrorReports.wrap (C_lexer.lexer ~inside_cn:true))
(MenhirLib.ErrorReports.wrap (Cn_lexer.lexer))
~offset:start_pos.pos_cnum
lexbuf

Expand Down Expand Up @@ -114,7 +116,7 @@ let update_enclosing_region payload_region xs =
let magic_comments_to_cn_toplevel (Cabs.TUnit decls) =
let magic_comments_to_cn_toplevel = function
| Cabs.EDecl_magic (loc, str) ->
parse_loc_string C_parser.cn_toplevel (loc, str)
parse_loc_string Cn_parser.cn_toplevel (loc, str)
|> Exception.except_fmap (update_enclosing_region loc)
| decl ->
Exception.except_return [decl] in
Expand All @@ -125,7 +127,7 @@ let magic_comments_to_cn_toplevel (Cabs.TUnit decls) =
let parse_with_magic_comments lexbuf =
handle
C_parser.translation_unit
(MenhirLib.ErrorReports.wrap (C_lexer.lexer ~inside_cn:false))
(MenhirLib.ErrorReports.wrap (C_lexer.lexer))
~offset:0
lexbuf

Expand Down
Loading
Loading