Skip to content

UnsignedInteger problem

Jump to bottom
lzx-center edited this page Mar 31, 2022 · 2 revisions

Smack前端进行整数翻译，会出现错误。 具体例子如下:

int main(){
    char *i = malloc(11*sizeof(char));
    char *j = i + 3;
    *j = 'b';
    char* l = j - 2;
    char load = *l;
    // free(i);
}

翻译出来的bpl为：

onst main: ref;
axiom (main == $sub.ref(0, 1032));
procedure {:entrypoint} main()
  returns ($r: i32)
{
  var $p0: ref8;
  var $p1: ref8;
  var $i2: i64;
  var $p3: ref8;
  var $i4: i8;
$bb0:
  call {:cexpr "smack:entry:main"} boogie_si_record_ref(main);
  call $p0 := malloc(11);
  $p1 := $add.ref($p0, $mul.ref(3, 1));
  $M.0 := $store.i8($M.0, $p1, 98);
  $i2 := $add.i64(3, 18446744073709551614);
  $p3 := $add.ref($p0, $mul.ref($i2, 1));
  $i4 := $load.i8($M.0, $p3);
  call {:cexpr "load"} boogie_si_record_i8($i4);
  $r := 0;
  return;
}

这其中有一个问题

  1. 会出现：$i2 := $add.i64(3, 18446744073709551614);的情况，也即将负数当成无符号数来进行处理了。

下面是个问题的原因

https://github.com/SpencerL-Y/SESL/blob/master/lib/smack/SmackRep.cpp#L963 问题主要在这个文件：

        bool isUnsignedInst = false;
        if (opcode == llvm::Instruction::SDiv || opcode == llvm::Instruction::SRem) {
            isUnsigned = false;
        } else if (opcode == llvm::Instruction::UDiv ||
                   opcode == llvm::Instruction::URem ||
                   opcode == llvm::Instruction::Sub) {
            isUnsignedInst = true;
            isUnsigned = true;
        }

        return Expr::fn(opName(fn, {t}), expr(lhs, isUnsigned, isUnsignedInst),
                        expr(rhs, isUnsigned, isUnsignedInst));

这里，lhs和rhs用的同一个isUnsigned，如果op是减法，isUnsigned是true。因为二者共用isUnsigned，所以就会出现上面那种情况。 所以加个判断，判断一下二者的符号即可。 即将这种情况下的expr(rhs, isUnsigned, isUnsignedInst)变成expr(rhs, false, isUnsignedInst)问题就能解决。

Clone this wiki locally