Skip to content

Commit

Permalink
fixes signed division and tweak both division representations (#962)
Browse files Browse the repository at this point in the history
* fixes indentation

* fixes signed division and tweak both division representations

The signed division operation was improperly encoded in BAP since long
time ago (probably since re-introduction of x86 in 0.9.x, back in
2014). As reported by @icemonster (#961), the overflow check was
incorrectly treating singed integers and any signed division by a
negative number was triggering the division error exception.

A small history research showed that in BAP 0.8 the overflow check
was commented out for signed division, with a corresponding (and
wrong) comment that it should be implemented and how it should be
implemented. It looks like later, during porting this code was
uncommented.

The new implementation implements a correct check as well as tweaks
the code so that it now produces a more compact and readable code, as
well as the lifting code is also now more readable and looks more like
a specification.

Here is the code generated for the signed divsion:
```

$ bap-mc 'f7 7d f8' --show-insn=asm --show-bil
idivl -0x8(%rbp)
{
  #1 := if high:1[mem[RBP - 8, el]:u32]
          then pad:64[mem[RBP - 8, el]:u32] | 0xFFFFFFFF00000000
          else pad:64[mem[RBP - 8, el]:u32]
  #2 := low:32[RDX].low:32[RAX]
  if (#1 = 0) {
    cpuexn (0)
  }
  else {
    #3 := #2 /$ #1
    #4 := #2 %$ #1
    if (0x7FFFFFFFFFFFFFFF <$ #3 | #3 <$ 0x8000000000000000) {
      cpuexn (0)
    }
    else {
      #5 := low:32[#4].low:32[#3]
      RAX := pad:64[extract:31:0[#5]]
      RDX := pad:64[extract:63:32[#5]]
    }
  }
  CF := unknown[bits]:u1
  OF := unknown[bits]:u1
  SF := unknown[bits]:u1
  ZF := unknown[bits]:u1
  AF := unknown[bits]:u1
  PF := unknown[bits]:u1
}
```

and for the unsigned one

```
bap-mc 'f7 75 f8' --show-insn=asm --show-bil
divl -0x8(%rbp)
{
  #1 := pad:64[mem[RBP - 8, el]:u32]
  #2 := low:32[RDX].low:32[RAX]
  if (#1 = 0) {
    cpuexn (0)
  }
  else {
    #3 := #2 / #1
    #4 := #2 % #1
    if (high:32[#3] = 0) {
      #5 := low:32[#4].low:32[#3]
      RAX := pad:64[extract:31:0[#5]]
      RDX := pad:64[extract:63:32[#5]]
    }
    else {
      cpuexn (0)
    }
  }
  CF := unknown[bits]:u1
  OF := unknown[bits]:u1
  SF := unknown[bits]:u1
  ZF := unknown[bits]:u1
  AF := unknown[bits]:u1
  PF := unknown[bits]:u1
}
```

a small smoke test was implemented as C program,
```c
 #include <stdio.h>
 #include <limits.h>

int stest(const char *msg, int dividend, int divisor, int expected) {
    int result = dividend / divisor;
    if (result == expected)
        puts("PASS");
    else
        puts(msg);
}

unsigned utest(const char *msg, unsigned dividend, unsigned divisor, unsigned expected) {
    unsigned result = dividend / divisor;
    if (result == expected)
        puts("PASS");
    else
        puts(msg);
}

int main(int argc, char const *argv[])
{
    stest("10 / -1 <> -10", 10,-1,-10);
    stest("10 / -2 <> -5", 10,-2,-5);
    stest("10 / -10 <> -1", 10,-10,-1);
    stest("10 / 1 <> 10", 10,1,10);
    stest("10 / 2 <> 5", 10,2,5);
    stest("10 / 10 <> 1", 10,10,1);
    utest("10 / 10 <> 1", 10,10,1);
    utest("10 / 1 <> 10", 10,1,10);
    utest("10 / 100 <> 0", 10,100,0);
    utest("10 / UINT_MAX <> 0", 10,UINT_MAX,0);
    stest("10 / 0 is #defined", 10,0,10);
    puts("FAIL");               /* this should not be reached */
}
```

which correctly yields all passes when run with `bap ./example --run`.

Note, this test doesn't really cover the overflow check when an actual
overflow happens, because I don't know how to force a C compiler to
generate code that will lead to an integer overflow from the
division. If anyone knows, please tell me :)

* switches CI to trusty

it looks like that they have switched to Xenial by default on this week.
  • Loading branch information
ivg authored Jul 31, 2019
1 parent 52d625c commit 3b02362
Show file tree
Hide file tree
Showing 2 changed files with 1,245 additions and 1,226 deletions.
2 changes: 2 additions & 0 deletions .travis.yml
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
language: c
dist: trusty


sudo: required

Expand Down
Loading

0 comments on commit 3b02362

Please sign in to comment.