[CN] Implement bitvector ops (and, or, xor)

[dc-mak]

Related: https://github.com/rems-project/cerberus/issues/243

Estimated work: few days. Needed for VIP test cases.

[scuellar]

I'm trying to learn more about the CN codebase and this seems like a good first issue to tackle. If you are not wokring on it, is it ok if I take it?

Also, @dc-mak , would it be possible to have enough permissions for me to assign issues to myself and make PRs from my fork?

[cp526]

@scuellar That would be great! If Dhruv is not already working on this, @dc-mak?

Very happy to help if you run into questions, just ping me.

[dc-mak]

I'm managed to do "and" (https://github.com/rems-project/cerberus/commit/8eb2bb921d205fd20d2022f22574788e70eb3ba7, and https://github.com/rems-project/cerberus/commit/6c6bdf979fd59dc6067df26bf646429da6c62fd7) but "or" and "xor" are still remaining, so feel free!

You may like to look at https://github.com/rems-project/cerberus/commit/1d7618d0e723a878ab0feea6e6c443f454010226 and https://github.com/rems-project/cerberus/commit/673ab10be9d548898a5da15f9935e9db3c809e76 too - these implement unary bitwise complement from scratch, so will be similar.

[dc-mak]

@scuellar any updates on this, including an ETA?

[scuellar]

@jprider63 will be taking over for me while I'm out the next month. He might take over this once he's up to speed, but we might want to unassign this in case someone wants to tackle this in the meantime.

[jprider63]

Hi @dc-mak. I'm just starting to learn the codebase, but I'm happy to take on this issue to dive in.

[cp526]

Sounds good! Happy to chat if you run into questions.

[dc-mak]

It looks like BW_Xor was partially implemented by https://github.com/rems-project/cerberus/commit/2b30e70b1d975937ee1e73e8643dce18b6036ae7 but we still need support for it in the spec language:

18:18 ➜  cerberus git:(cn-sundry-fixes) ✗ cat tmp.c && cn verify tmp.c
int f(int x, int y)
    /*@ ensures return == x ^ y; @*/
{
    return x ^ y;
}
tmp.c:2:29: error: unexpected token after 'x' and before '^'
Please add error message for state 939 to parsers/c/c_parser_error.messages
    /*@ ensures return == x ^ y; @*/
                            ^

[jprider63]

It looks like BW_Or was already implemented as well. I've opened a PR (#501) that adds xor and or to the parser.

@cp526 or @dc-mak, it'd be great if we could meet to go over this together, introduce me to the code, and show me how to properly add/run tests. I currently get a bunch of errors when I run ./tests/run-cn.sh.

[dc-mak]

Happy to have a chat and take a look. Just in case you've not seen this, you can also look at the following:

• https://github.com/rems-project/cerberus/blob/master/backend/cn/CONTRIBUTING.md
• https://github.com/rems-project/cerberus/blob/master/backend/cn/ONBOARDING.md
• https://github.com/rems-project/cerberus/blob/master/.github/workflows/ci.yml (for running tests)

The onboarding doc contains links to a video walkthrough too. I believe @cp526 did a separate walkthrough with @bcpierce00 at some point after that, but I don't know if it was recorded - certainly the insights from it did/should have made their way into the docs. PRs on those welcome too!

[dc-mak]

Closed by #501 (https://github.com/rems-project/cerberus/commit/d8973873556150c53a2910abaa4ff252944791a3 and https://github.com/rems-project/cerberus/commit/84c212beb15c14f1826e15af2040c240d338822)