Model arbitrary integer size

[shaobo-he]

It appears that LLVM generates arbitrary size integers. One examples is ldv-linux-3.16-rc1/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--net--xen-netfront.ko-entry_point_true-unreach-call.cil.out.c in svcomp repo. Variables with type i24 occur in function netback_changed.

[michael-emmi]

Why was this called a bug? Should Clang/LLVM not be allowed to use i24?

[michael-emmi]

After further trial, I guess that it was called a bug because SMACK does not generate declarations for i24.

[michael-emmi]

Hi Shaobo,
Could you figure out whether Clang/LLVM may actually generate arbitrary iX for 1 <= X <= 64?

So far I have only seen X such that X = 1 or 1 < X <= 64 and X % 8 == 0.

[shaobo-he]

Hi Mike,

Yes, I could. If bit-field is used, then LLVM may represent bit-field as arbitrary integer such as i24. I'm not quite sure about this, but take the program I mentioned as an example. In that program, a structure called _ddebug contains bit-field. Its definition is,

struct _ddebug {
char const *modname ;
char const *function ;
char const *filename ;
char const *format ;
unsigned int lineno : 18 ;
unsigned char flags ;
};

It seems to me that field lineno and flags are packed into an integer size memory area so that lineno takes the first three bytes (24 bits) and flags takes the last byte. That's why we got i24. The operations on lineno are to load three bytes into an i24 variable first and use masks to manipulate on the first 18 bits.

I wonder if there is a flag for clang to desugar them into byte-level operations.

[michael-emmi]

Last time I checked, 24 % 8 = 0.

So I repeat: are you aware of Clang/LLVM generating an integer type which is not i1 nor divisible by 8?

[shaobo-he]

My bad... No, I'm not aware of.

[shaobo-he]

The only chance that not-divisible-by-eight integer size is generated is via struct packing, I guess. But it looks like LLVM has packed structs into fields divisible by 8. What do you propose to fix it?

[shaobo-he]

I compiled GNU coreutils 6.11 with clang and wrote an LLVM pass to check if there are not-divisible-by-eight operands in each instruction. And I got i52, i14, etc.

[shaobo-he]

I changed one of the clang flag from "O3" to "O0" and there were no not-divisible-by-eight operands. I guess that it's kind of safe to assume that all integer sizes are divisible by eight since SMACK uses "O0".

[zvonimir]

Yeah, we have to use O0. Moving away from O0 causes all sorts of other
problems too, and some of them are not trivial to resolve. So for now, O0
it is, in which case we are fine. Thanks for exploring this!

http://zvonimir.info
http://soarlab.org/

On Wed, May 6, 2015 at 3:36 PM, Shaobo notifications@github.com wrote:

I changed one of the clang flag from "O3" to "O0" and there were no
not-divisible-by-eight operands.

—
Reply to this email directly or view it on GitHub
#86 (comment).

[shaobo-he]

No problem. If you guys need any other information such as ptrtoint/inttoptr use cases to facilitate the development, please feel free to email me.

[shaobo-he]

Hi guys,

I'm working on generating SVCOMP boogie benchmarks and i24 appears again.
I'll try to make a list of the files containing these types to facilitate debuging.

[michael-emmi]

I cannot reproduce this. Please specify the exact commands and branch used to generate a BPL file with i24 types.

[shaobo-he]

In svcomp2016 branch, try:
smack.py ldv-linux-3.16-rc1/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--net--xen-netfront.ko-entry_point_true-unreach-call.cil.out.c --svcomp --error-witness a.graphxml under svcomp root directory.

[shaobo-he]

Also for this example (I don't know if it is a valid C program),
http://www.cs.utah.edu/~shaobo/test.c
I got i40. Can you reproduce it?

[michael-emmi]

Let’s just include the program here for our records:

#include <stdio.h>
#include <assert.h>
struct _ddebug { 
//char const   *modname ;
//char const   *function ;
//char const   *filename ;
//char const   *format ;
unsigned int lineno : 18 ;
unsigned int test_1 : 14 ;
unsigned int test_2 : 2  ;
unsigned char flags ;
};

int
main (void)
{
  struct _ddebug d;
  char *evil;
  memset(&d, 0, sizeof(d));
  d.lineno = 1U;
  d.test_1 = 2U;
  d.test_2 = 3U;
  evil = (char *)&d;
  *evil = 0U;
  printf("Size is %d\n", sizeof(d));
  printf("Size of unsigned int is %d\n", sizeof(unsigned int));
  printf("offset is %lu\n", (unsigned long) (&d.flags) - (unsigned long) (&d));
  d.test_2 = 1U;
  assert(d.lineno == 0U);
}

[zvonimir]

We are adding new integer bit-widths on-demand, as we encounter the need to support a new bit-width. I think that at this point we are supporting a good enough subset.