From 4b477f8108a2a92012ff138725f6c6f26ccb23e5 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 29 Aug 2013 17:30:33 +0100 Subject: Implemented runtime check for overshift (controllable with --check-overshift command line argument). Overshift is where a Shl, AShr or LShr has a shift width greater than the bit width of the first operand. This is undefined behaviour in LLVM so we report this as an error. --- runtime/Intrinsic/klee_overshift_check.c | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) create mode 100644 runtime/Intrinsic/klee_overshift_check.c (limited to 'runtime') diff --git a/runtime/Intrinsic/klee_overshift_check.c b/runtime/Intrinsic/klee_overshift_check.c new file mode 100644 index 00000000..c0cb6102 --- /dev/null +++ b/runtime/Intrinsic/klee_overshift_check.c @@ -0,0 +1,31 @@ +//===-- klee_overshift_check.c ---------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include + +/* This instrumentation call is used to check for overshifting. + * If we do try to do x << y or x >> y + * where + * bitWidth = sizeof(x)*8 + * shift = y + * + * then we can detect overshifting (which has undefined behaviour). + */ +void klee_overshift_check(unsigned long long bitWidth, unsigned long long shift) { + if (shift >= bitWidth) { + /* Maybe we shouldn't throw an error because + * overshifting can be non-fatal? Perhaps + * we should generate a test case but carry + * on executing the state with a warning? + */ + klee_report_error("IGNORED", 0 /*Ignored */, "overshift error", "overshift.err"); + } +} + + -- cgit 1.4.1