au-ts / cogent

Cogent Project
https://trustworthy.systems/projects/TS/cogent.pml
Other
158 stars 26 forks source link

Wrong generated custom getter for a simple layout (making autocorres generate a fail) #381

Closed amblafont closed 3 years ago

amblafont commented 4 years ago
type Example =  {  field1 : U32 }  layout record {  field1: 77b at 44b }

main : Example -> Example
main r { field1 } = r {  field1  }

generates the getter

static inline u32 d2_get_field1(t1 *b)
{
    return (u32) d3_get_field1_part0(b) << 0U | (u32) d4_get_field1_part1(b) <<
        20U | (u32) d5_get_field1_part2(b) << 52U;
}

This << 52U makes autocorres generate a fail.

amblafont commented 3 years ago

This issue is not so troublesome, as it disappears when the layout size matches exactly the type (i.e. 32b instead of 77b in the example above), as pointed out by @zilinc.

zilinc commented 3 years ago

typecheck fixed by 467b5dd3d