Add cast kinds #199
Add cast kinds #199
Conversation
There was a problem hiding this comment.
Pull request overview
This PR adds a new castkind type to CIL's AST to distinguish between different types of cast operations. The CastE expression constructor is updated from CastE(typ, exp) to CastE(castkind, typ, exp), allowing the AST to preserve information about why a cast was inserted (e.g., explicit cast, integer promotion, arithmetic conversion, etc.). This addresses issue #179.
Key changes:
- Introduces a new
castkindtype with 9 variants:Explicit,IntegerPromotion,DefaultArgumentPromotion,ArithmeticConversion,ConditionalConversion,PointerConversion,Implicit,Internal, andUnknown - Updates all
CastEpattern matches and constructor calls throughout the codebase to include the cast kind parameter - Modifies
mkCastandmkCastTfunctions to require a~kindparameter, ensuring cast kinds are specified at all call sites
Reviewed changes
Copilot reviewed 11 out of 11 changed files in this pull request and generated 6 comments.
Show a summary per file
| File | Description |
|---|---|
| src/cil.mli | Defines the new castkind type and updates CastE, mkCast, mkCastT signatures |
| src/cil.ml | Implements castkind type, updates CastE handling in all expression functions, adds d_castkind pretty-printer |
| src/frontc/cabs2cil.ml | Updates all cast operations to use appropriate cast kinds (Explicit, IntegerPromotion, ArithmeticConversion, etc.) |
| src/mergecil.ml | Updates CastE pattern matches in equality checking to accommodate new parameter |
| src/expcompare.ml | Updates expression comparison to include cast kind in equality checks, updates cast stripping functions |
| src/check.ml | Updates type checking for CastE with TODO for validating cast kinds |
| src/formatparse.mly | Updates parser to use Explicit kind for user casts, Unknown for internal casts |
| src/formatcil.ml | Updates test code to include Unknown cast kind |
| src/ext/pta/ptranal.ml | Updates pointer analysis to handle new CastE structure |
| src/ext/dataslicing/dataslicing.ml | Updates data slicing to preserve cast kinds |
| src/ext/zrapp/rmciltmps.ml | Updates temporary removal to use Unknown cast kind |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| let e' = | ||
| let te = typeOf e in | ||
| let _, zte = castTo intType te zero in | ||
| let _, zte = castTo ~kind:Unknown intType te zero in |
There was a problem hiding this comment.
It seems to me that this case is entirely unreachable. Adding an exception here does not crash Goblint on any of its test at least.
Closes #179.
TODO
~kind:Unknown-s? I don't know what they should be, so maybe just leave for now. TheUnknownkind will probably get used in Goblint as well.