From a46b8059ba5f8b5759813d142018478d4b72db71 Mon Sep 17 00:00:00 2001 From: Daniel Schemmel Date: Thu, 23 Mar 2023 16:49:08 +0000 Subject: remove include/klee/Support/IntEvaluation.h --- include/klee/Support/IntEvaluation.h | 164 ----------------------------------- 1 file changed, 164 deletions(-) delete mode 100644 include/klee/Support/IntEvaluation.h (limited to 'include') diff --git a/include/klee/Support/IntEvaluation.h b/include/klee/Support/IntEvaluation.h deleted file mode 100644 index 0e9a40d6..00000000 --- a/include/klee/Support/IntEvaluation.h +++ /dev/null @@ -1,164 +0,0 @@ -//===-- IntEvaluation.h -----------------------------------------*- C++ -*-===// -// -// The KLEE Symbolic Virtual Machine -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// - -#ifndef KLEE_INTEVALUATION_H -#define KLEE_INTEVALUATION_H - -#include "klee/ADT/Bits.h" - -#define MAX_BITS (sizeof(uint64_t) * 8) - -// ASSUMPTION: invalid bits in each uint64_t are 0. the trade-off here is -// between making trunc/zext/sext fast and making operations that depend -// on the invalid bits being 0 fast. - -namespace klee { -namespace ints { - -// add of l and r -inline uint64_t add(uint64_t l, uint64_t r, unsigned inWidth) { - return bits64::truncateToNBits(l + r, inWidth); -} - -// difference of l and r -inline uint64_t sub(uint64_t l, uint64_t r, unsigned inWidth) { - return bits64::truncateToNBits(l - r, inWidth); -} - -// product of l and r -inline uint64_t mul(uint64_t l, uint64_t r, unsigned inWidth) { - return bits64::truncateToNBits(l * r, inWidth); -} - -// truncation of l to outWidth bits -inline uint64_t trunc(uint64_t l, unsigned outWidth, unsigned inWidth) { - return bits64::truncateToNBits(l, outWidth); -} - -// zero-extension of l from inWidth to outWidth bits -inline uint64_t zext(uint64_t l, unsigned outWidth, unsigned inWidth) { - return l; -} - -// sign-extension of l from inWidth to outWidth bits -inline uint64_t sext(uint64_t l, unsigned outWidth, unsigned inWidth) { - uint32_t numInvalidBits = MAX_BITS - inWidth; - return bits64::truncateToNBits(((int64_t)(l << numInvalidBits)) >> numInvalidBits, outWidth); -} - -// unsigned divide of l by r -inline uint64_t udiv(uint64_t l, uint64_t r, unsigned inWidth) { - return bits64::truncateToNBits(l / r, inWidth); -} - -// unsigned mod of l by r -inline uint64_t urem(uint64_t l, uint64_t r, unsigned inWidth) { - return bits64::truncateToNBits(l % r, inWidth); -} - -// signed divide of l by r -inline uint64_t sdiv(uint64_t l, uint64_t r, unsigned inWidth) { - // sign extend operands so that signed operation on 64-bits works correctly - int64_t sl = sext(l, MAX_BITS, inWidth); - int64_t sr = sext(r, MAX_BITS, inWidth); - return bits64::truncateToNBits(sl / sr, inWidth); -} - -// signed mod of l by r -inline uint64_t srem(uint64_t l, uint64_t r, unsigned inWidth) { - // sign extend operands so that signed operation on 64-bits works correctly - int64_t sl = sext(l, MAX_BITS, inWidth); - int64_t sr = sext(r, MAX_BITS, inWidth); - return bits64::truncateToNBits(sl % sr, inWidth); -} - -// arithmetic shift right of l by r bits -inline uint64_t ashr(uint64_t l, uint64_t shift, unsigned inWidth) { - int64_t sl = sext(l, MAX_BITS, inWidth); - return bits64::truncateToNBits(sl >> shift, inWidth); -} - -// logical shift right of l by r bits -inline uint64_t lshr(uint64_t l, uint64_t shift, unsigned inWidth) { - return l >> shift; -} - -// shift left of l by r bits -inline uint64_t shl(uint64_t l, uint64_t shift, unsigned inWidth) { - return bits64::truncateToNBits(l << shift, inWidth); -} - -// logical AND of l and r -inline uint64_t land(uint64_t l, uint64_t r, unsigned inWidth) { - return l & r; -} - -// logical OR of l and r -inline uint64_t lor(uint64_t l, uint64_t r, unsigned inWidth) { - return l | r; -} - -// logical XOR of l and r -inline uint64_t lxor(uint64_t l, uint64_t r, unsigned inWidth) { - return l ^ r; -} - -// comparison operations -inline uint64_t eq(uint64_t l, uint64_t r, unsigned inWidth) { - return l == r; -} - -inline uint64_t ne(uint64_t l, uint64_t r, unsigned inWidth) { - return l != r; -} - -inline uint64_t ult(uint64_t l, uint64_t r, unsigned inWidth) { - return l < r; -} - -inline uint64_t ule(uint64_t l, uint64_t r, unsigned inWidth) { - return l <= r; -} - -inline uint64_t ugt(uint64_t l, uint64_t r, unsigned inWidth) { - return l > r; -} - -inline uint64_t uge(uint64_t l, uint64_t r, unsigned inWidth) { - return l >= r; -} - -inline uint64_t slt(uint64_t l, uint64_t r, unsigned inWidth) { - int64_t sl = sext(l, MAX_BITS, inWidth); - int64_t sr = sext(r, MAX_BITS, inWidth); - return sl < sr; -} - -inline uint64_t sle(uint64_t l, uint64_t r, unsigned inWidth) { - int64_t sl = sext(l, MAX_BITS, inWidth); - int64_t sr = sext(r, MAX_BITS, inWidth); - return sl <= sr; -} - -inline uint64_t sgt(uint64_t l, uint64_t r, unsigned inWidth) { - int64_t sl = sext(l, MAX_BITS, inWidth); - int64_t sr = sext(r, MAX_BITS, inWidth); - return sl > sr; -} - -inline uint64_t sge(uint64_t l, uint64_t r, unsigned inWidth) { - int64_t sl = sext(l, MAX_BITS, inWidth); - int64_t sr = sext(r, MAX_BITS, inWidth); - return sl >= sr; -} - -} // end namespace ints -} // end namespace klee - -#endif /* KLEE_INTEVALUATION_H */ -- cgit 1.4.1