Incorrect rewrite of a simple program

[anuragsiy7504]

Hello,

I am trying to optimise the following program:

#include <stdio.h>
#include <cstdlib>
#include <stddef.h>
#include <stdint.h>


int count(int var) {
  int res;
  for(res = 0; res < var; res++);
  return res;
}

int main() {
  int val = 100000;
  int res = count(val);

  printf("%d\n", res);
  return 0;
}

The Function extracted by stoke is:

  .text
  .globl _Z5counti
  .type _Z5counti, @function

#! file-offset 0x566
#! rip-offset  0x400566
#! capacity    26 bytes

# Text              #  Line  RIP       Bytes  Opcode
._Z5counti:         #        0x400566  0      OPC=<label>
  movl %edi, %eax   #  1     0x400566  2      OPC=movl_r32_r32
  testl %edi, %edi  #  2     0x400568  2      OPC=testl_r32_r32
  jle .L_40057a     #  3     0x40056a  2      OPC=jle_label
  movl $0x0, %edx   #  4     0x40056c  5      OPC=movl_r32_imm32
.L_400571:          #        0x400571  0      OPC=<label>
  addl $0x1, %edx   #  5     0x400571  3      OPC=addl_r32_imm8
  cmpl %eax, %edx   #  6     0x400574  2      OPC=cmpl_r32_r32
  jne .L_400571     #  7     0x400576  2      OPC=jne_label
  nop               #  8     0x400578  1      OPC=nop
  retq              #  9     0x400579  1      OPC=retq
.L_40057a:          #        0x40057a  0      OPC=<label>
  movl $0x0, %eax   #  10    0x40057a  5      OPC=movl_r32_imm32
  retq              #  11    0x40057f  1      OPC=retq

.size _Z5counti, .-_Z5counti

The rewrite discovered by stoke is:

  .text
  .globl _Z5counti
  .type _Z5counti, @function

#! file-offset 0x566
#! rip-offset  0x400566
#! capacity    26 bytes

# Text                    #  Line  RIP       Bytes  Opcode
._Z5counti:               #        0x400566  0      OPC=<label>
  lzcntl %edi, %edx       #  1     0x400566  4      OPC=lzcntl_r32_r32
  bzhil %edx, %edi, %eax  #  2     0x40056a  5      OPC=bzhil_r32_r32_r32
  retq                    #  3     0x40056f  1      OPC=retq

.size _Z5counti, .-_Z5counti

The stoke debug verify command :
stoke debug verify --def_in "{ %edi }" --live_out "{ %eax }" --target bins/_Z5counti.s --rewrite result.s --abi_check --strategy bounded --bound 64

Returns : Equivalent: yes

But on incorporating the rewrite into the original program produces incorrect results.
Is my understanding correct here?

[stefanheule]

What is the input that produces incorrect result (what's the input, what is the expected output, and what output do you see instead)?

Without having looked too much at your code, it is definitely possible for bounded verification to say the rewrite is equivalent when it is not equivalent for all possible inputs. In particular, as the name suggest, the strategy explores a bounded set of executions, so any execution beyond this bound remain completely unchecked.

[bchurchill]

Your verification strategy isn't doing anything -- the bounded verifier can't look at that loop because it's doing too many iterations. Berkeley

…

On Mon, Nov 4, 2019, 10:57 Stefan Heule ***@***.***> wrote: What is the input that produces incorrect result (what's the input, what is the expected output, and what output do you see instead)? Without having looked too much at your code, it is definitely possible for bounded verification to say the rewrite is equivalent when it is not equivalent for all possible inputs. In particular, as the name suggest, the strategy explores a *bounded* set of executions, so any execution beyond this bound remain completely unchecked. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#1008?email_source=notifications&email_token=AAE4N2N5SLGH3GQ56WCG64TQSBIAFA5CNFSM4JIVR4V2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEC76R6A#issuecomment-549447928>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAE4N2NJQFQZGAMKFXBICETQSBIAFANCNFSM4JIVR4VQ> .

[anuragsiy7504]

The input to the loop is 10000.
Should I increase the --bound flag to the verifier?

I am trying to find out if stoke can optimize cases which look complex to begin with but are actually very simple.

In this case, the input program has a loop, but it can be replaced with a simple instruction.

[anuragsiy7504]

Any help here?
I even tried the following verification command:
stoke debug verify --def_in "{ %edi }" --live_out "{ %eax }" --target bins/_Z5counti.s --rewrite result.s --abi_check --strategy bounded --bound 1024

Still got the output "yes"

[bchurchill]

I haven't had time to analyze this carefully but my guess is that this verification problem is one where bounded validators cannot "see" the difference between the two programs. Bounded verification is inherently unsound. What's the smallest input that demonstrates the two programs are different? My guess is that it's greater than the bounds you've tried, and hence the validator can't find it. To optimize such a program, I'd suggest adding more test cases, especially including tests with different bit patterns.

…

On Mon, Nov 11, 2019, 21:38 anuragsiy7504 ***@***.***> wrote: Any help here? I even tried the following verification command: stoke debug verify --def_in "{ %edi }" --live_out "{ %eax }" --target bins/_Z5counti.s --rewrite result.s --abi_check --strategy bounded --bound 1024 Still got the output "yes" — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#1008?email_source=notifications&email_token=AAE4N2JBEFKLZ5Z7RUJAOPLQTI6N5A5CNFSM4JIVR4V2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEDZC6YI#issuecomment-552742753>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAE4N2ODX4X5FHHRB7QVZSLQTI6N5ANCNFSM4JIVR4VQ> .

[anuragsiy7504]

Any number which is greater than 16bits, leads to a mismatch.
I used the stoke_tcgen to generate test cases.

[bchurchill]

Exactly -- in order for the bounded verifier to see the programs are not equivalent, the bound needs to be greater than 2^16. That's because if the bound is B it only checks inputs that finish withing B loop iterations. You could try setting the bound to 66,000 or something like that, but usually that will take too long. Fortunately this is a simple example so it might actually scale find, but for complex programs sometimes we can't even push it past bound 2! This is a good example of why the bounded validator isn't sound. There's some discussion of this general phenomenon in the ASPLOS 2017 paper: stoke uses test cases to find a fast program on those particular tests, and this can lead to over fitting. We use a bounded validator to then find new test cases to add. But, even if the rewrite passes the bounded validator, we need a sound validator to fully verify equivalence.

…

On Sat, Nov 16, 2019, 06:06 anuragsiy7504 ***@***.***> wrote: Any number which is greater than 16bits, leads to a mismatch. I used the stoke_tcgen to generate test cases. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#1008?email_source=notifications&email_token=AAE4N2IRU2TD3OD5AHV73FDQT747HA5CNFSM4JIVR4V2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEEHSJII#issuecomment-554640545>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAE4N2OYPOZCAYN7KGCQBNLQT747HANCNFSM4JIVR4VQ> .