This is regarding the overflow of int(also perhaps ptroffs) type.
Currently, Imp only imposes intrange_64 condition on int for only certain cases (comparison, system call arguments).
For memory offset, load/store(by Imp), alloc(by Mem).
For CompCert compilation, overflow is handled by performing modular arithmetics. Therefore, there are some valid programs in Imp, but executes UB if intrange_64 is checked upon pargs(as @alxest mentioned).
f (x: int) { return x + 1; }
main () {a = f(INTMAX + 1); print(a); }
What we want is to erase all the overflow checks (extra assume (intrange_64))s) from 0-level specs(MutF0.v).
Some possible solutions:
Have two types: Tint: checks overflow, Tz: does not.
Include intrange_64 condition in Tint type, following CompCert.
The second one needs more work, including fixing the compiler.
This is regarding the overflow of
int(also perhapsptroffs) type. Currently, Imp only imposesintrange_64condition onintfor only certain cases (comparison, system call arguments). For memory offset, load/store(by Imp), alloc(by Mem). For CompCert compilation, overflow is handled by performing modular arithmetics. Therefore, there are some valid programs in Imp, but executes UB ifintrange_64is checked upon pargs(as @alxest mentioned).What we want is to erase all the overflow checks (extra
assume (intrange_64))s) from 0-level specs(MutF0.v). Some possible solutions:Tint: checks overflow,Tz: does not.intrange_64condition inTinttype, following CompCert. The second one needs more work, including fixing the compiler.