diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2017-05-24 16:32:47 +0100 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2017-07-19 18:15:20 +0100 |
commit | 8e8732d482e42e363f0f4c51794ed966701371e7 (patch) | |
tree | 35ae38f61a0dbe865c931841a559b0d4553a838a /lib/Core/Executor.h | |
parent | 7c4fdd012317eb92352fc7ded53a553ed762719f (diff) | |
download | klee-8e8732d482e42e363f0f4c51794ed966701371e7.tar.gz |
Implement basic support for vectorized instructions.
We use LLVM's Scalarizer pass to remove most vectorized code so that the Executor only needs to support the InsertElement and ExtractElement instructions. This pass was not available in LLVM 3.4 so to support that LLVM version the pass has been back ported. To check that the Executor is not receiving vector operand types that it can't handle assertions have been added. There are a few limitations to this implementation. * The InsertElement and ExtractElement index cannot be symbolic. * There is no support for LLVM < 3.4.
Diffstat (limited to 'lib/Core/Executor.h')
-rw-r--r-- | lib/Core/Executor.h | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index c3f6e705..b3bb6864 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -105,6 +105,7 @@ public: enum TerminateReason { Abort, Assert, + BadVectorAccess, Exec, External, Free, |