Unexpected type cast generated by frontend
The frontend will generate weird type cast, which further breaks the verification. A mini example to illustrate the issue:
[[rc::parameters("x : Z")]]
[[rc::args("x @ int<i16>")]]
[[rc::requires("{x ≠ min_int i16}")]]
[[rc::returns("{-x} @ int<i16>")]]
int16_t not_int_i16(int16_t x) {
return -x;
}
The generated code:
Definition impl_not_int_i16 : function := {|
f_args := [
("x", it_layout i16)
];
f_local_vars := [
];
f_init := "#0";
f_code := (
<[ "#0" :=
locinfo: loc_155 ;
Return (LocInfoE loc_156 (
UnOp (CastOp $ IntOp i16) (IntOp i32) ( (* <-- bug : i32 *)
LocInfoE loc_156 (UnOp NegOp (IntOp i16) (LocInfoE loc_157 (
use{it_layout i16} (LocInfoE loc_158 ("x"))))))))
]> $∅
)%E
|}.
In the comment line: i32
is incorrect for the cast operation: the subexpression -x
actually has type i16
.
Another example with implicit type cast:
[[rc::returns("void")]]
void test_bits() {
uint16_t mask = 0x00f0;
uint32_t a = 0x12345678;
uint32_t clearing_bits = a & ~mask; // <- type cast
assert(clearing_bits == 0x12345608);
}
Type cast is expected when evaluating a & (~mask)
: the second operand needs be extended to u32
. The generated code:
Definition impl_test_bits : function := {|
f_args := [
];
f_local_vars := [
("mask", it_layout u16);
("clearing_bits", it_layout u32);
("a", it_layout u32)
];
f_init := "#0";
f_code := (
<[ "#0" :=
"mask" <-{ it_layout u16 }
LocInfoE loc_175 (UnOp (CastOp $ IntOp u16) (IntOp i32) (
LocInfoE loc_175 (i2v 240 i32))) ;
"a" <-{ it_layout u32 }
LocInfoE loc_172 (UnOp (CastOp $ IntOp u32) (IntOp i32) (
LocInfoE loc_172 (i2v 305419896 i32))) ;
"clearing_bits" <-{ it_layout u32 }
LocInfoE loc_164 ((LocInfoE loc_165 (use{it_layout u32} (
LocInfoE loc_166 ("a"))))
&{IntOp u32, IntOp u32}
(LocInfoE loc_167 (UnOp (CastOp $ IntOp u32) (IntOp i32) ( (* <-- bug : i32 *)
LocInfoE loc_167 (UnOp NotIntOp (IntOp u16) (
LocInfoE loc_168 (use{it_layout u16} (LocInfoE loc_169 ("mask"))))))))) ;
Return (VOID)
]> $∅
)%E
|}.
So far I haven't found the same issue on binary operators, but only on unary operators (-
and ~
).