Indirect jumps lead to incorrect assumptions

bmourad01 commented 2 years ago

Consider the following BIL program:

{
  if (f1) {
    #56 := v1
    jmp #56
  }
  else {
    v1 := mem[sp + 8, el]:u64
  }
  #1 := mem[sp, el]:u64
  sp := sp + 8
  #56 := #1
  jmp #56
}

We would expect that the final value of #56 will be conditional, summarized by the postcondition:

(ite (= init_f10 #b0)
     (concat (select init_mem0 (bvadd #x0000000000000007 init_sp0))
             (select init_mem0 (bvadd #x0000000000000006 init_sp0))
             (select init_mem0 (bvadd #x0000000000000005 init_sp0))
             (select init_mem0 (bvadd #x0000000000000004 init_sp0))
             (select init_mem0 (bvadd #x0000000000000003 init_sp0))
             (select init_mem0 (bvadd #x0000000000000002 init_sp0))
             (select init_mem0 (bvadd #x0000000000000001 init_sp0))
             (select init_mem0 init_sp0))
     init_v10)

However, this is not how WP treats it in BIR:

00000016: sub sub_%00000016()

00000007:
0000000d: when f1 goto %00000008
0000000e: goto %00000009

00000009:
0000000a: v1 := mem[sp + 8, el]:u64
00000011: goto %0000000f

00000008:
0000000b: #56 := v1
0000000c: goto #56
00000010: goto %0000000f

0000000f:
00000012: #1 := mem[sp, el]:u64
00000013: sp := sp + 8
00000014: #56 := #1
00000015: goto #56

And indeed, it seems to treat the goto #56 at tid 0000000c as a no-op, which results in our goal above being refuted.

A solution would be to tighten assumptions about the behavior of indirect jumps (perhaps here?)

bmourad01 commented 2 years ago

On second thought, maybe it's an issue with the Bil_to_bir implementation: https://github.com/draperlaboratory/cbat_tools/blob/119528b8f3465e2fff04658af27dff876263aad5/wp/lib/bap_wp/src/bil_to_bir.ml#L53

It seems to insert the goto %0000000f in the block 00000008 even though 0000000f is not reachable from this block.

Perhaps a fix would be to just run a pass on the generated blocks and remove all jump terms that occur after an unconditional jump within a given block.

codyroux commented 2 years ago

Yes, indirect jumps are treated as a "goto exit" currently. I built in a handler for them (here: https://github.com/draperlaboratory/cbat_tools/blob/119528b8f3465e2fff04658af27dff876263aad5/wp/lib/bap_wp/src/precondition.ml#L419), but I'm not sure what the best way to populate it is.

draperlaboratory / cbat_tools

Indirect jumps lead to incorrect assumptions #351