RefinedC issueshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/issues2021-05-31T07:16:50Zhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/issues/39refinedc frontend should be more flexible about placement of verification files2021-05-31T07:16:50ZMichael Sammlerrefinedc frontend should be more flexible about placement of verification filesFrom #37:
Running the README instructions, I figured simply naming it `test.c` would be OK, but I got the following error:
```
refinedc check test.c
refinedc: internal error, uncaught exception:
(Invalid_argument "String.sub ...From #37:
Running the README instructions, I figured simply naming it `test.c` would be OK, but I got the following error:
```
refinedc check test.c
refinedc: internal error, uncaught exception:
(Invalid_argument "String.sub / Bytes.sub")
Raised at Stdlib.invalid_arg in file "stdlib.ml", line 30, characters 20-45
Called from Stdlib__string.sub in file "string.ml" (inlined), line 47, characters 2-23
Called from Dune__exe__Extra.Filename.relative_path in file "frontend/extra.ml", line 105, characters 6-62
Called from Dune__exe__Main.run in file "frontend/main.ml", line 163, characters 28-70
Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 25, characters 19-24
Called from Cmdliner.Term.run in file "cmdliner.ml", line 117, characters 32-39
make: *** [Makefile:9: check] Error 125
```
Creating `src` and moving `test.c` into it fixed the issue, but the original error was very difficult to reason about (would have been impossible to understand had I not been following the readme) and seems like a strange limitation to have in the first place.
It's certainly going to cause some headache for contributors to our project - at this point, I will have to wrap the entire verification task inside a Dockerfile, which is pretty unfortunate DX given that our codebase does not follow the `src` pattern and Docker is a hefty, intrusive and brittle dependency. Further, even if it did follow the `src` hierarchy, it would add some cruft to the directory hierarchy. I would much rather specify (ideally from the command line) where directories should be placed/checked, and which files I'm interested in verifying.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/issues/38refinedc init does not support directory names containing hyphens2021-05-31T13:08:56ZMichael Sammlerrefinedc init does not support directory names containing hyphensFrom #37:
> `refinedc init` choked on a hyphen in the pathname. Seems like Coq is to blame here but it would be nice if this wasn't a limitation seeing as how there's really no reason for it.
>
> Renaming the project directory to someth...From #37:
> `refinedc init` choked on a hyphen in the pathname. Seems like Coq is to blame here but it would be nice if this wasn't a limitation seeing as how there's really no reason for it.
>
> Renaming the project directory to something without the `-`'s allowed it to work, but this will certainly block us from using RefinedC without a Docker image and file renaming hacks.
Maybe we should change all letters except `[a-zA-Z_]` into `_` for the name of the Coq module? (Of course, one needs to check whether there are other problems as well.)https://gitlab.rts.mpi-sws.org/iris/refinedc/-/issues/34Unexpected type cast generated by frontend2021-03-04T09:51:34ZFengmin ZhuUnexpected type cast generated by frontendThe frontend will generate weird type cast, which further breaks the verification. A mini example to illustrate the issue:
```c
[[rc::parameters("x : Z")]]
[[rc::args("x @ int<i16>")]]
[[rc::requires("{x ≠ min_int i16}")]]
[[rc::returns...The frontend will generate weird type cast, which further breaks the verification. A mini example to illustrate the issue:
```c
[[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:
```coq
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:
```c
[[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:
```coq
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 `~`).