conflicting behavior loop unrolling flag

[DieracDelta]

Prematurely terminating loops using cbat's --num-unroll flag results in UNSAT when SAT is expected. A minimal working example would be:

int foo(uint8_t i){
  int k = 0;
  while(k < 3){
    k++;
  }
  return i;
}

I compiled this on gcc 5.4.0 with cc -O0 -g -Wall -Wpedantic -o main main.c. I invoked cbat with commit e13386c9173c15dbde22e13271e783e44b021e7d with bap on c93b5d8.

The cbat invocations used are:

  # invocation 1
  bap wp \
    --func=foo \
    --num-unroll=3 \
    --postcond="(assert (not (= RAX #x0000000000000005)))" \
    --no-byteweight \
    -- main

and

  # invocation 2
  bap wp \
    --func=foo \
    --num-unroll=3 \
    --postcond="(assert (not (= RAX #x0000000000000005)))" \
    --no-byteweight \
    -- main

Invocation 1 returns with

SAT!

Model:
    ZF  |->  0x0
    SF  |->  0x0
    RSP |->  0x000000003f800082
    RDI |->  0x0000000000000005
    RBP |->  0x0000000000000000
    RAX |->  0x0000000000000000
    PF  |->  0x0
    OF  |->  0x0
    CF  |->  0x0
    AF  |->  0x0
    mem_orig |-> [
        else |-> 0x00]
    mem_mod = mem_orig

This is as expected, since an argument (RDI) of 5, when returned, makes RAX become 5.

However, when we change the num-unroll flag to 2 as in invocation 2, we would also expect RDI to be 5 in a SAT countermodel. However, this is not the observed behavior, as cbat returns UNSAT.

The cfg for foo is:

digraph {
node[shape=box];

subgraph "cluster_foo" {
  label="foo"

  "\%00000413"[label="\@foo
0000041a: #46 := RBP\l0000041d: RSP := RSP - 8\l00000420: mem := mem with [RSP, el]:u64 <- #46\l00000427: RBP := RSP\l0000042e: RAX := pad:64[low:32[RDI]]\l00000435: mem := mem with [RBP - 0x14] <- low:8[RAX]\l0000043c: mem := mem with [RBP - 4, el]:u32 <- 0\l"]
  "\%00000440"[label="\%00000440
00000450: #47 := mem[RBP - 4, el]:u32 - 2\l00000453: CF := mem[RBP - 4, el]:u32 < 2\l00000456: OF := high:1[(mem[RBP - 4, el]:u32 ^ 2) & (mem[RBP - 4, el]:u32 ^ #47)]\l00000459: AF := 0x10 = (0x10 & (#47 ^ mem[RBP - 4, el]:u32 ^ 2))\l0000045c: PF := ~low:1[let $1 = #47 >> 4 ^ #47 in let $2 = $1 >> 2 ^ $1 in\l$2 >> 1 ^ $2]\l0000045f: SF := high:1[#47]\l00000462: ZF := 0 = #47\l"]
  "\%00000494"[label="\%00000494
00000499: RAX := pad:64[pad:32[mem[RBP - 0x14]]]\l000004a1: RBP := mem[RSP, el]:u64\l000004a4: RSP := RSP + 8\l000004ad: #52 := mem[RSP, el]:u64\l000004b0: RSP := RSP + 8\l000004b4: call #52 with noreturn\l"]
  "\%00000466"[label="\%00000466
0000047d: #49 := mem[RBP - 4, el]:u32\l00000480: mem := mem with [RBP - 4, el]:u32 <- mem[RBP - 4, el]:u32 + 1\l00000483: CF := mem[RBP - 4, el]:u32 < #49\l00000486: OF := ~high:1[#49] & (high:1[#49] | high:1[mem[RBP - 4, el]:u32]) & ~(\lhigh:1[#49] & high:1[mem[RBP - 4, el]:u32])\l00000489: AF := 0x10 = (0x10 & (mem[RBP - 4, el]:u32 ^ #49 ^ 1))\l0000048c: PF := ~low:1[let $1 = mem[RBP - 4, el]:u32 >> 4 ^ mem[RBP - 4, el]:u32 in\llet $2 = $1 >> 2 ^ $1 in $2 >> 1 ^ $2]\l0000048f: SF := high:1[mem[RBP - 4, el]:u32]\l00000492: ZF := 0 = mem[RBP - 4, el]:u32\l"]
  "\%00000413" -> "\%00000440"
  "\%00000440" -> "\%00000466"[label="ZF | (SF | OF) & ~(SF & OF)"]
  "\%00000440" -> "\%00000494"[label="~(ZF | (SF | OF) & ~(SF & OF))"]
  "\%00000466" -> "\%00000440"
}
}

[DieracDelta]

For easy access, I've pushed the example and the script to run it here.

[fortunac]

Fixed in #312