Tracking bit status information in goblint

[edwintorok]

Maybe I am doing something wrong but the congruence analysis doesn't seem to be able to track this.

Here I am getting a random value, telling goblint to assume the state of the LSB, and then immediately assert it, and goblint says the assertion status is unknown (in a real program of course the assertion would be far away from the assume call):
https://gist.github.com/edwintorok/8c6f3de4f717a3145945705cdcbe863b

(I could attempt to implement an analysis specific to tracking the LSB bit, similar to the sign analysis, but if goblint already has code to handle something similar I'd prefer to reuse or perhaps fix that part. For context: tracking the state of this bit is useful for OCaml C stubs where Is_block() and Is_long() macros check the bit).

[michael-schwarz]

Thank you, I'll have a look! This should definitely be possible for the congruence domain (after some small tweaks).

[sim642]

Besides implementing bitand in the congruence domain, __goblint_assume(x&1) also requires specific changes to BaseInvariant to actually assume that information.

[edwintorok]

I tried using modulo (see updated gist), which seems to have some more code, but perhaps needs some improvement too for assume?
BTW I don't have to use assume, if there is another way to tell goblint the status of the low bit I'd be happy to change my code to do that (the goal is to tell goblint that memory allocated by OCaml is aligned to at least 2 bytes or not, when using OCaml integers).

[michael-schwarz]

What already works on the master branch is if the program is rewritten to explicitly use x % 2 == 1, as in this modified example:

//PARAM: --enable ana.int.congruence --set sem.int.signed_overflow assume_none
#include <goblint.h>

int foo(long x)
{
  __goblint_assume(x%2 == 1);
  __goblint_check(x%2 == 1);
}

int main()
{
  foo(__VERIFIER_nondet_int());
}