about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--include/klee/Expr.h3
-rw-r--r--lib/Core/Executor.cpp6
-rw-r--r--lib/Core/Memory.cpp116
-rw-r--r--lib/Expr/Expr.cpp9
4 files changed, 63 insertions, 71 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index 92b322f2..9df9a699 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -792,9 +792,6 @@ public:
   /// Creates an ExtractExpr with the given bit offset and width
   static ref<Expr> create(ref<Expr> e, unsigned bitOff, Width w);
 
-  /// Creates an ExtractExpr with the given byte offset and width
-  static ref<Expr> createByteOff(ref<Expr> e, unsigned byteOff, Width w=Expr::Int8);
-
   Width getWidth() const { return width; }
   Kind getKind() const { return Extract; }
 
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 88ced236..005499eb 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -1854,9 +1854,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     // Conversion
   case Instruction::Trunc: {
     CastInst *ci = cast<CastInst>(i);
-    ref<Expr> result = ExtractExpr::createByteOff(eval(ki, 0, state).value,
-						  0,
-						  Expr::getWidthForLLVMType(ci->getType()));
+    ref<Expr> result = ExtractExpr::create(eval(ki, 0, state).value,
+                                           0,
+                                           Expr::getWidthForLLVMType(ci->getType()));
     bindLocal(ki, state, result);
     break;
   }
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index 05c226d3..d2c1dd0e 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -455,11 +455,11 @@ ref<Expr> ObjectState::read(unsigned offset, Expr::Width width) const {
 }
 
 ref<Expr> ObjectState::read1(unsigned offset) const {
-  return ExtractExpr::createByteOff(read8(offset), 0, Expr::Bool);
+  return ExtractExpr::create(read8(offset), 0, Expr::Bool);
 }
 
 ref<Expr> ObjectState::read1(ref<Expr> offset) const {
-  return ExtractExpr::createByteOff(read8(offset), 0, Expr::Bool);
+  return ExtractExpr::create(read8(offset), 0, Expr::Bool);
 }
 
 ref<Expr> ObjectState::read16(unsigned offset) const {
@@ -676,11 +676,11 @@ void ObjectState::write16(unsigned offset, uint16_t value) {
 
 void ObjectState::write16(unsigned offset, ref<Expr> value) {
   if (kMachineByteOrder == machine::MSB) {
-    write8(offset+0, ExtractExpr::createByteOff(value, 1));
-    write8(offset+1, ExtractExpr::createByteOff(value, 0));
+    write8(offset+0, ExtractExpr::create(value, 8, Expr::Int8));
+    write8(offset+1, ExtractExpr::create(value, 0, Expr::Int8));
   } else {
-    write8(offset+1, ExtractExpr::createByteOff(value, 1));
-    write8(offset+0, ExtractExpr::createByteOff(value, 0));
+    write8(offset+1, ExtractExpr::create(value, 8, Expr::Int8));
+    write8(offset+0, ExtractExpr::create(value, 0, Expr::Int8));
   }
 }
 
@@ -689,17 +689,17 @@ void ObjectState::write16(ref<Expr> offset, ref<Expr> value) {
   if (kMachineByteOrder == machine::MSB) {
     write8(AddExpr::create(offset,
                            ConstantExpr::create(0, kMachinePointerType)), 
-           ExtractExpr::createByteOff(value,1));
+           ExtractExpr::create(value, 8, Expr::Int8));
     write8(AddExpr::create(offset,
                            ConstantExpr::create(0, kMachinePointerType)), 
-           ExtractExpr::createByteOff(value,0));
+           ExtractExpr::create(value, 0, Expr::Int8));
   } else {
     write8(AddExpr::create(offset,
                            ConstantExpr::create(1, kMachinePointerType)), 
-           ExtractExpr::createByteOff(value,1));
+           ExtractExpr::create(value, 8, Expr::Int8));
     write8(AddExpr::create(offset,
                            ConstantExpr::create(0, kMachinePointerType)), 
-           ExtractExpr::createByteOff(value,0));
+           ExtractExpr::create(value, 0, Expr::Int8));
   }
 }
 
@@ -719,15 +719,15 @@ void ObjectState::write32(unsigned offset, uint32_t value) {
 
 void ObjectState::write32(unsigned offset, ref<Expr> value) {
   if (kMachineByteOrder == machine::MSB) {
-    write8(offset+0, ExtractExpr::createByteOff(value, 3));
-    write8(offset+1, ExtractExpr::createByteOff(value, 2));
-    write8(offset+2, ExtractExpr::createByteOff(value, 1));
-    write8(offset+3, ExtractExpr::createByteOff(value, 0));
+    write8(offset+0, ExtractExpr::create(value, 24, Expr::Int8));
+    write8(offset+1, ExtractExpr::create(value, 16, Expr::Int8));
+    write8(offset+2, ExtractExpr::create(value, 8, Expr::Int8));
+    write8(offset+3, ExtractExpr::create(value, 0, Expr::Int8));
   } else {
-    write8(offset+3, ExtractExpr::createByteOff(value, 3));
-    write8(offset+2, ExtractExpr::createByteOff(value, 2));
-    write8(offset+1, ExtractExpr::createByteOff(value, 1));
-    write8(offset+0, ExtractExpr::createByteOff(value, 0));
+    write8(offset+3, ExtractExpr::create(value, 24, Expr::Int8));
+    write8(offset+2, ExtractExpr::create(value, 16, Expr::Int8));
+    write8(offset+1, ExtractExpr::create(value, 8, Expr::Int8));
+    write8(offset+0, ExtractExpr::create(value, 0, Expr::Int8));
   }
 }
 
@@ -735,29 +735,29 @@ void ObjectState::write32(ref<Expr> offset, ref<Expr> value) {
   if (kMachineByteOrder == machine::MSB) {
     write8(AddExpr::create(offset,
                            ConstantExpr::create(0, kMachinePointerType)), 
-           ExtractExpr::createByteOff(value,3));
+           ExtractExpr::create(value, 24, Expr::Int8));
     write8(AddExpr::create(offset,
                            ConstantExpr::create(1, kMachinePointerType)), 
-           ExtractExpr::createByteOff(value,2));
+           ExtractExpr::create(value, 16, Expr::Int8));
     write8(AddExpr::create(offset,
                            ConstantExpr::create(2, kMachinePointerType)), 
-           ExtractExpr::createByteOff(value,1));
+           ExtractExpr::create(value, 8, Expr::Int8));
     write8(AddExpr::create(offset,
                            ConstantExpr::create(3, kMachinePointerType)), 
-           ExtractExpr::createByteOff(value,0));
+           ExtractExpr::create(value, 0, Expr::Int8));
   } else {
     write8(AddExpr::create(offset,
                            ConstantExpr::create(3, kMachinePointerType)), 
-           ExtractExpr::createByteOff(value,3));
+           ExtractExpr::create(value, 24, Expr::Int8));
     write8(AddExpr::create(offset,
                            ConstantExpr::create(2, kMachinePointerType)), 
-           ExtractExpr::createByteOff(value,2));
+           ExtractExpr::create(value, 16, Expr::Int8));
     write8(AddExpr::create(offset,
                            ConstantExpr::create(1, kMachinePointerType)), 
-           ExtractExpr::createByteOff(value,1));
+           ExtractExpr::create(value, 8, Expr::Int8));
     write8(AddExpr::create(offset,
                            ConstantExpr::create(0, kMachinePointerType)), 
-           ExtractExpr::createByteOff(value,0));
+           ExtractExpr::create(value, 0, Expr::Int8));
   }
 }
 
@@ -785,23 +785,23 @@ void ObjectState::write64(unsigned offset, uint64_t value) {
 
 void ObjectState::write64(unsigned offset, ref<Expr> value) {
   if (kMachineByteOrder == machine::MSB) {
-    write8(offset+0, ExtractExpr::createByteOff(value, 7));
-    write8(offset+1, ExtractExpr::createByteOff(value, 6));
-    write8(offset+2, ExtractExpr::createByteOff(value, 5));
-    write8(offset+3, ExtractExpr::createByteOff(value, 4));
-    write8(offset+4, ExtractExpr::createByteOff(value, 3));
-    write8(offset+5, ExtractExpr::createByteOff(value, 2));
-    write8(offset+6, ExtractExpr::createByteOff(value, 1));
-    write8(offset+7, ExtractExpr::createByteOff(value, 0));
+    write8(offset+0, ExtractExpr::create(value, 56, Expr::Int8));
+    write8(offset+1, ExtractExpr::create(value, 48, Expr::Int8));
+    write8(offset+2, ExtractExpr::create(value, 40, Expr::Int8));
+    write8(offset+3, ExtractExpr::create(value, 32, Expr::Int8));
+    write8(offset+4, ExtractExpr::create(value, 24, Expr::Int8));
+    write8(offset+5, ExtractExpr::create(value, 16, Expr::Int8));
+    write8(offset+6, ExtractExpr::create(value, 8, Expr::Int8));
+    write8(offset+7, ExtractExpr::create(value, 0, Expr::Int8));
   } else {
-    write8(offset+7, ExtractExpr::createByteOff(value, 7));
-    write8(offset+6, ExtractExpr::createByteOff(value, 6));
-    write8(offset+5, ExtractExpr::createByteOff(value, 5));
-    write8(offset+4, ExtractExpr::createByteOff(value, 4));
-    write8(offset+3, ExtractExpr::createByteOff(value, 3));
-    write8(offset+2, ExtractExpr::createByteOff(value, 2));
-    write8(offset+1, ExtractExpr::createByteOff(value, 1));
-    write8(offset+0, ExtractExpr::createByteOff(value, 0));
+    write8(offset+7, ExtractExpr::create(value, 56, Expr::Int8));
+    write8(offset+6, ExtractExpr::create(value, 48, Expr::Int8));
+    write8(offset+5, ExtractExpr::create(value, 40, Expr::Int8));
+    write8(offset+4, ExtractExpr::create(value, 32, Expr::Int8));
+    write8(offset+3, ExtractExpr::create(value, 24, Expr::Int8));
+    write8(offset+2, ExtractExpr::create(value, 16, Expr::Int8));
+    write8(offset+1, ExtractExpr::create(value, 8, Expr::Int8));
+    write8(offset+0, ExtractExpr::create(value, 0, Expr::Int8));
   }
 }
 
@@ -809,53 +809,53 @@ void ObjectState::write64(ref<Expr> offset, ref<Expr> value) {
   if (kMachineByteOrder == machine::MSB) {
     write8(AddExpr::create(offset,
                            ConstantExpr::create(0, kMachinePointerType)), 
-           ExtractExpr::createByteOff(value,7));
+           ExtractExpr::create(value, 56, Expr::Int8));
     write8(AddExpr::create(offset,
                            ConstantExpr::create(1, kMachinePointerType)), 
-           ExtractExpr::createByteOff(value,6));
+           ExtractExpr::create(value, 48, Expr::Int8));
     write8(AddExpr::create(offset,
                            ConstantExpr::create(2, kMachinePointerType)), 
-           ExtractExpr::createByteOff(value,5));
+           ExtractExpr::create(value, 40, Expr::Int8));
     write8(AddExpr::create(offset,
                            ConstantExpr::create(3, kMachinePointerType)), 
-           ExtractExpr::createByteOff(value,4));
+           ExtractExpr::create(value, 32, Expr::Int8));
     write8(AddExpr::create(offset,
                            ConstantExpr::create(4, kMachinePointerType)), 
-           ExtractExpr::createByteOff(value,3));
+           ExtractExpr::create(value, 24, Expr::Int8));
     write8(AddExpr::create(offset,
                            ConstantExpr::create(5, kMachinePointerType)), 
-           ExtractExpr::createByteOff(value,2));
+           ExtractExpr::create(value, 16, Expr::Int8));
     write8(AddExpr::create(offset,
                            ConstantExpr::create(6, kMachinePointerType)), 
-           ExtractExpr::createByteOff(value,1));
+           ExtractExpr::create(value, 8, Expr::Int8));
     write8(AddExpr::create(offset,
                            ConstantExpr::create(7, kMachinePointerType)), 
-           ExtractExpr::createByteOff(value,0));
+           ExtractExpr::create(value, 0, Expr::Int8));
   } else {
     write8(AddExpr::create(offset,
                            ConstantExpr::create(7, kMachinePointerType)), 
-           ExtractExpr::createByteOff(value,7));
+           ExtractExpr::create(value, 56, Expr::Int8));
     write8(AddExpr::create(offset,
                            ConstantExpr::create(6, kMachinePointerType)), 
-           ExtractExpr::createByteOff(value,6));
+           ExtractExpr::create(value, 48, Expr::Int8));
     write8(AddExpr::create(offset,
                            ConstantExpr::create(5, kMachinePointerType)), 
-           ExtractExpr::createByteOff(value,5));
+           ExtractExpr::create(value, 40, Expr::Int8));
     write8(AddExpr::create(offset,
                            ConstantExpr::create(4, kMachinePointerType)), 
-           ExtractExpr::createByteOff(value,4));
+           ExtractExpr::create(value, 32, Expr::Int8));
     write8(AddExpr::create(offset,
                            ConstantExpr::create(3, kMachinePointerType)), 
-           ExtractExpr::createByteOff(value,3));
+           ExtractExpr::create(value, 24, Expr::Int8));
     write8(AddExpr::create(offset,
                            ConstantExpr::create(2, kMachinePointerType)), 
-           ExtractExpr::createByteOff(value,2));
+           ExtractExpr::create(value, 16, Expr::Int8));
     write8(AddExpr::create(offset,
                            ConstantExpr::create(1, kMachinePointerType)), 
-           ExtractExpr::createByteOff(value,1));
+           ExtractExpr::create(value, 8, Expr::Int8));
     write8(AddExpr::create(offset,
                            ConstantExpr::create(0, kMachinePointerType)), 
-           ExtractExpr::createByteOff(value,0));
+           ExtractExpr::create(value, 0, Expr::Int8));
   }
 }
 
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index e82285dd..5ef71d8c 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -669,11 +669,6 @@ ref<Expr> ExtractExpr::create(ref<Expr> expr, unsigned off, Width w) {
   return ExtractExpr::alloc(expr, off, w);
 }
 
-
-ref<Expr> ExtractExpr::createByteOff(ref<Expr> expr, unsigned offset, Width bits) {
-  return ExtractExpr::create(expr, 8*offset, bits);
-}
-
 /***/
 
 ref<Expr> ZExtExpr::create(const ref<Expr> &e, Width w) {
@@ -681,7 +676,7 @@ ref<Expr> ZExtExpr::create(const ref<Expr> &e, Width w) {
   if (w == kBits) {
     return e;
   } else if (w < kBits) { // trunc
-    return ExtractExpr::createByteOff(e, 0, w);
+    return ExtractExpr::create(e, 0, w);
   } else if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e)) {
     return CE->ZExt(w);
   } else {
@@ -694,7 +689,7 @@ ref<Expr> SExtExpr::create(const ref<Expr> &e, Width w) {
   if (w == kBits) {
     return e;
   } else if (w < kBits) { // trunc
-    return ExtractExpr::createByteOff(e, 0, w);
+    return ExtractExpr::create(e, 0, w);
   } else if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e)) {
     return CE->SExt(w);
   } else {
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-23 11:36:29 +0000