search

goblint / cil

C Intermediate Language
https://goblint.github.io/cil/
Other
40 stars 16 forks source link

add support for `__int128`, `__int128_t`, `__uint128_t` #49

Closed vogler closed 2 years ago

vogler commented 2 years ago

Closes #41. I left some TODOs where I wasn't sure. Esp. if long long is already 128 bit on the machine, do we then want ikind ILongLong or IInt128?

(This machine-dependent ambiguity is a source of errors if one does not use CIL's functions but assumes e.g. long long to be of a certain size - might be better to let CIL just emit concrete int sizes like int32_t.)

vogler commented 2 years ago

Works as intended. The Parse error for fields starting with __ was just due to a typo in the typedef.

MaskRay commented 2 years ago

__int128_t and __uint128_t are also recognized as built-in types.

In particular, Nim generated C uses __uint128_t (e.g. with import tables) which I need to produce a self-contained C source file.

vogler commented 2 years ago

Mh, the lexer/parser is a bit hard to understand. I just wanted to return two tokens UNSIGNED INT128 for __uint128_t, but then how should the lexer's state be adjusted? Alternative would be an extra token, but that would require some special handling outside of the type_spec rule, which is also messy. https://github.com/goblint/cil/blob/7a912ddd2325f915c4bbbbf04534b9f82bb4832a/src/frontc/cparser.mly#L959

@MaskRay For now you can use the option cppflags to include a header file with typedefs for __int128_t and __uint128_t like done here: https://github.com/goblint/analyzer/pull/311/files

vogler commented 2 years ago

Added them as built-in named types on init and handled in cabs2cil. Should be fine to merge now.