Merge branch 'issue-392'

StanfordPL · Jan 9, 2015 · 749f383 · 749f383
2 parents d8bb2a5 + 8cde157
commit 749f383
Show file tree

Hide file tree

Showing 4 changed files with 21 additions and 38 deletions.
diff --git a/src/symstate/state.cc b/src/symstate/state.cc
@@ -284,7 +284,7 @@ std::vector<SymBool> SymState::equality_constraints(const SymState& other, const
 template <typename T>
 SymBitVector SymState::get_addr(M<T> memory) const {
 
-  SymBitVector address = SymBitVector::constant(64, memory.get_disp());
+  SymBitVector address = SymBitVector::constant(32, memory.get_disp()).extend(64);
 
   if(memory.contains_base()) {
     address = address + lookup(memory.get_base());

diff --git a/src/validator/handlers/lea_handler.cc b/src/validator/handlers/lea_handler.cc
@@ -46,38 +46,7 @@ void LeaHandler::build_circuit(const x64asm::Instruction& instr, SymState& state
   uint16_t width = dest.size();
 
   // Compute the memory address
-  // This is slightly different than the default method because it truncates
-  // all the values to width for a slightly smaller circuit
-  SymBitVector address = SymBitVector::constant(width, memory.get_disp());
-
-  if(memory.contains_base()) {
-    address = address + state[memory.get_base()][width-1][0];
-  }
-
-  if(memory.contains_index()) {
-    auto index = state[memory.get_index()][width-1][0];
-
-    switch(memory.get_scale()) {
-    case Scale::TIMES_1:
-      address = address + index;
-      break;
-
-    case Scale::TIMES_2:
-      address = address + (index << SymBitVector::constant(width, 1));
-      break;
-
-    case Scale::TIMES_4:
-      address = address + (index << SymBitVector::constant(width, 2));
-      break;
-
-    case Scale::TIMES_8:
-      address = address + (index << SymBitVector::constant(width, 3));
-      break;
-
-    default:
-      assert(false);
-    }
-  }
+  SymBitVector address = state.get_addr(memory)[width-1][0];
 
   // Set the destination value; takes care of perserving other bits and setting other bits to zero
   state.set(dest, address);

diff --git a/tests/validator/fuzz.h b/tests/validator/fuzz.h
@@ -75,27 +75,26 @@ TEST_F(ValidatorFuzzTest, RandomInstructionRandomState) {
   std::stringstream sample;
   sample << ".sample:" << std::endl;
   sample << "movq (%rax), %r13" << std::endl;
-  /*
   sample << "movq 0x16(%r8), %r13" << std::endl;
   sample << "movq 0x64(%rdx), %r13" << std::endl;
-  sample << "movq 0x64(%rax, %rcx, 4), %r13" << std::endl;
+  sample << "movq -0x64(%rax, %rcx, 4), %r13" << std::endl;
   sample << "movq 0x64(%rsp, %rdx, 8), %r13" << std::endl;
   sample << "movl (%rax), %r13d" << std::endl;
-  sample << "movl 0x16(%r8), %r13d" << std::endl;
+  sample << "movl -0x16(%r8), %r13d" << std::endl;
   sample << "movl 0x64(%rdx), %r13d" << std::endl;
   sample << "movl 0x64(%rax, %rcx, 4), %r13d" << std::endl;
   sample << "movl 0x64(%rsp, %rdx, 8), %r13d" << std::endl;
   sample << "movw (%rax), %r13w" << std::endl;
   sample << "movw 0x16(%r8), %r13w" << std::endl;
   sample << "movw 0x64(%rdx), %r13w" << std::endl;
   sample << "movw 0x64(%rax, %rcx, 4), %r13w" << std::endl;
-  sample << "movw 0x64(%rsp, %rdx, 8), %r13w" << std::endl;
+  sample << "movw -0x64(%rsp, %rdx, 8), %r13w" << std::endl;
   sample << "movb (%rax), %r13b" << std::endl;
   sample << "movb 0x16(%r8), %r13b" << std::endl;
   sample << "movb 0x64(%rdx), %r13b" << std::endl;
   sample << "movb 0x64(%rax, %rcx, 4), %r13b" << std::endl;
   sample << "movb 0x64(%rsp, %rdx, 8), %r13b" << std::endl;
-  */
+
   x64asm::Code target;
   sample >> target;
 

diff --git a/tests/validator/handlers/lea.h b/tests/validator/handlers/lea.h
@@ -128,3 +128,18 @@ TEST_F(ValidatorLeaTest, Issue239Scale4) {
   assert_equiv();
 
 }
+
+TEST_F(ValidatorLeaTest, Issue392NegativeOffset) {
+
+  target_ << "leaq -0x10(%rax), %rdx" << std::endl;
+  target_ << "retq" << std::endl;
+
+  rewrite_ << "addq $-0x10, %rax" << std::endl;
+  rewrite_ << "movq %rax, %rdx" << std::endl;
+  rewrite_ << "retq" << std::endl;
+
+  set_live_outs(x64asm::RegSet::empty() + x64asm::rdx);
+  assert_equiv();
+
+}
+