LLVM Intrinsics handling

[ireneGP]

Hello,

I am writing to model check some LLVM IR code generated from a reverse engineering tool, and in my code some Intrinsics are used everywhere, such as llvm.bswap.i256 and llvm.ctlz.i256. And they are "declared" in my IR program:

; Function Attrs: nounwind readnone
declare i160 @llvm.bswap.i160(i160) #1

After some debugging, I figured that when Smack goes through the usage of such intrinsics, the behavior becomes quite wired (e.g., generating a false positive or so).

So my question is, in my case (since I didn't compile certain C code into LLVM IR), am I expected to implement such Intrinsics by myself? At this moment it seems problematic to just leave the declaration there.

[keram88]

Hello,

Without a definition, calls to these functions will produce non-deterministic values, so you will get false positives. We plan to support more intrinsics, but you could edit the input files to have definitions in the meantime.

Intrinsics cannot be defined directly within LLVM files, so you would need to rename the functions.

Alternatively, you can define them directly in the Boogie file:

E.g., insert:

procedure  llvm.bswap.i32($i0: bv32)
  returns ($r: bv32) {
  assume $r[8:0] == $i0[32:24] &&
         $r[16:8] == $i0[24:16] &&
         $r[24:16] == $i0[16:8] &&
         $r[32:24] == $i0[8:0];
  return;
}

into input.bpl generated from:
smack --bit-precise input.ll -bpl output.bpl -t

Then run:
smack output.bpl

I wrote this python script to generate drop-in bswap procedures (8-256 bits) in Boogie:

for bw in range(8,256+8,8):
  print "procedure  llvm.bswap.i{}($i0: bv{})\nreturns ($r: bv{}) {{\nassume".format(bw,bw,bw);
  for i in range(0,bw,8):
      print "$r[{}:{}] == $i0[{}:{}] {}".format(i+8,i,bw-i,bw-i-8,"&&" if i != bw-8 else ";")
  print """return;\n}"""

I'm not sure about a good way to implement ctlz.

[ireneGP]

@keram88 Thank you so much! I appreciate it a lot. Let me see how to extend here.

[ireneGP]

@keram88

Hello, I tried to use the bit-wise reasoning (previously I didn't go that far but use the default option), but got a large number of exceptions as follows:

/opt/test/data/smack_data/smack_data2/a-cQN3bT.bpl(2482,11): Error: use of undeclared function: $store.bytes.bv160
/opt/test/data/smack_data/smack_data2/a-cQN3bT.bpl(2540,11): Error: use of undeclared function: $zext.bv1.bv256
/opt/test/data/smack_data/smack_data2/a-cQN3bT.bpl(2544,11): Error: use of undeclared function: $zext.bv1.bv256
/opt/test/data/smack_data/smack_data2/a-cQN3bT.bpl(2591,11): Error: use of undeclared function: $s
tore.bytes.bv160
/opt/test/data/smack_data/smack_data2/a-cQN3bT.bpl(2608,11): Error: use of undeclared function: $s
tore.bytes.bv160
/opt/test/data/smack_data/smack_data2/a-cQN3bT.bpl(2670,11): Error: use of undeclared function: $z
ext.bv1.bv256
/opt/test/data/smack_data/smack_data2/a-cQN3bT.bpl(2674,11): Error: use of undeclared function: $z
ext.bv1.bv256

It seems that when using the bitwise reasoning, operations regarding 256-bit are not defined.

Do you think it is feasible to avoid the bit-wise reasoning but also define those llvm instrinct? Thanks a lot for your advice!

[keram88]

Hello,
It is somewhat possible to model (or approximate) some of these programs in the default (integer) theory:
Some bitwise operations are easily modeled, e.g., x = y & 0x11 => = y%4 and x = y>>1 => x = y/2. Other operations like byte-swap and count-leading-zeros don't seem to have analogs that map so nicely without effectively writing bit-vector versions of them. Some operations such as loading the upper 16 bits of a 32-bit int as a short don't work Smack's memory model. Whether this works depends on the program.

Other things you can try:
Add higher bit-width functions to Smack:
In the source change the file share/smack/include/smack-macros.h as follows
Define store.bytes by changing the DECLARE_UNSAFE_STORES macro body to:
EVAL(COMBINE(8,256,DEC_BYTE,DECLARE_UNSAFE_STORE))
and do the same for DECLARE_UNSAFE_LOADS.
share/smack/lib/smack.c has the definitions for zext and can extrapolate for the ones you need.

This may not make sense in this case, but you can also try reducing the bitwidth of the program down to 128 bits or lower.

Generally, you can just declare declare missing functions and they will produce nondeterministic values, then if you get false bugs, you can provide definitions if they are used to produce the values flowing into your assertions.

[zvonimir]

@ireneGP : Any chance you could attach your ll file here so that we can reproduce this on our end? The errors you are getting are not what I would expect to see since we are supporting 256 bits wide integers. Thanks!

[ireneGP]

@zvonimir Sure thing. Thanks a lot for looking into this. Let me download the ll file when I have access to one of our internal server.

On the other hand, just want to sync with you that I am using the develop branch of smack, with commit 71e0ad0.

Also, would switching from the default config into bit-wise reasoning slow down smack a lot? My main issue is still about "processing time". If that would largely slow down smack, I guess I will just find some (sound but imprecise) work around to handle the lack of intrinct implementations.

[zvonimir]

In short, yes, based on our experience so far, bit-precise reasoning typically does slow down SMACK, sometimes a lot. That is typically true in general for all verifiers. We are actively working on improving that aspect of SMACK. Note though that 256 bits wide integers are pretty wide and hence hard on SMT solvers.
Now, it is hard to say how SMACK will behave on your code since that depends on the kinds of properties you are trying to verify and so on. We'll just have to try it and see.

[shaobo-he]

It appears that we should give a warning once a call to an unhandled LLVM instrinsic is encountered. Generally these calls lead to false alarms.

[shaobo-he]

A Todo list to handle LLVM intriniscs.

• issue Handle LLVM Half Precision Floating-Point Intrinsics #436
• Standard C Library Intrinsics (at least llvm.fabs.* in pull request Upgraded LLVM version to 4.0.1 #444)
• Bit Manipulation Intrinsics (required by Rust)

[shaobo-he]

Closed via #464 and #451.