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.

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

Crash when reserved keywords are used in 3d #108

Open
Smfakhoury opened this issue Nov 3, 2023 · 0 comments
Open

Crash when reserved keywords are used in 3d #108

Smfakhoury opened this issue Nov 3, 2023 · 0 comments

Comments

@Smfakhoury
Copy link

Everparse crashes when encountering 3d code that uses reserved keywords as identifier names.

Sample 3d code using 'type' identifier:

typedef UINT32BE START;

typedef struct _REPLY{
    UINT32BE requestor_id;
    UINT32BE response_id;
} REPLY;

typedef struct _CLOSE{
    UINT32BE requestor_id;
    UINT32BE response_id;
} CLOSE;

casetype _PAYLOAD(UINT8 type){
    switch(type){
        case 0: START message;
        case 1: REPLY message;
        case 2: CLOSE message;
    }
} PAYLOAD;

entrypoint 
typedef struct _MESSAGES{
    UINT8 type {type == 0 || type == 1 || type == 2};
    UINT32BE length;
    PAYLOAD(type) messages[:byte-size length];

} MESSAGES;

Crashes with the following:

Processing files: ./examples/Sample.3d
Writing file ./Sample.fst
Writing file ./Sample.fsti
Writing file ./SampleWrapper.c
Writing file ./SampleWrapper.h
Running: /home/sfakhoury/everparse/everparse/bin/fstar.exe --print_in_place --odir . --cache_dir . --include /home/sfakhoury/everparse/everparse/src/3d/prelude/buffer --include . --already_cached Prims,LowStar,FStar,LowParse,C,EverParse3d.\*,Spec --include /home/sfakhoury/everparse/everparse/src/lowparse --include /home/sfakhoury/everparse/everparse/krmllib --include /home/sfakhoury/everparse/everparse/krmllib/obj --include /home/sfakhoury/everparse/everparse/src/3d/prelude --cmi --warn_error +241 ./Sample.fsti
Running: /home/sfakhoury/everparse/everparse/bin/fstar.exe --print_in_place --odir . --cache_dir . --include /home/sfakhoury/everparse/everparse/src/3d/prelude/buffer --include . --already_cached Prims,LowStar,FStar,LowParse,C,EverParse3d.\*,Spec --include /home/sfakhoury/everparse/everparse/src/lowparse --include /home/sfakhoury/everparse/everparse/krmllib --include /home/sfakhoury/everparse/everparse/krmllib/obj --include /home/sfakhoury/everparse/everparse/src/3d/prelude --cmi --warn_error +241 ./Sample.fst
* Error 168 at ./Sample.fst(166,22-166,22):
  - Syntax error

1 error was reported (see above)

exit 1

Line 166 in Sample.fst:

let def__PAYLOAD (type:(___UINT8 )) = ( (T_cases (type = 0uy) (T_with_comment "message" (T_denoted "message" (DT_IType UInt32BE)) "Validating field message") (T_cases (type = 1uy) (T_with_comment "message" (T_denoted "message" (dtyp__REPLY )) "Validating field message") (T_cases (type = 2uy) (T_with_comment "message" (T_denoted "message" (dtyp__CLOSE )) "Validating field message") (T_false "_x_0")))) <: Tot (typ _ _ _ _) by (T.norm [delta_attr [`%specialize]; zeta; iota; primops]; T.smt()))

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant