klee
klee.h
Go to the documentation of this file.
1/*===-- klee.h --------------------------------------------------*- C++ -*-===//
2//
3// The KLEE Symbolic Virtual Machine
4//
5// This file is distributed under the University of Illinois Open Source
6// License. See LICENSE.TXT for details.
7//
8//===----------------------------------------------------------------------===*/
9
10#ifndef KLEE_H
11#define KLEE_H
12
13#include "stdint.h"
14#include "stddef.h"
15
16#ifdef __cplusplus
17extern "C" {
18#endif
19
20 /* Add an accesible memory object at a user specified location. It
21 * is the users responsibility to make sure that these memory
22 * objects do not overlap. These memory objects will also
23 * (obviously) not correctly interact with external function
24 * calls.
25 */
26 void klee_define_fixed_object(void *addr, size_t nbytes);
27
28 /* klee_make_symbolic - Make the contents of the object pointer to by \arg
29 * addr symbolic.
30 *
31 * \arg addr - The start of the object.
32 * \arg nbytes - The number of bytes to make symbolic; currently this *must*
33 * be the entire contents of the object.
34 * \arg name - A name used for identifying the object in messages, output
35 * files, etc. If NULL, object is called "unnamed".
36 */
37 void klee_make_symbolic(void *addr, size_t nbytes, const char *name);
38
39 /* klee_range - Construct a symbolic value in the signed interval
40 * [begin,end).
41 *
42 * \arg name - A name used for identifying the object in messages, output
43 * files, etc. If NULL, object is called "unnamed".
44 */
45 int klee_range(int begin, int end, const char *name);
46
47 /* klee_int - Construct an unconstrained symbolic integer.
48 *
49 * \arg name - An optional name, used for identifying the object in messages,
50 * output files, etc.
51 */
52 int klee_int(const char *name);
53
54 /* klee_silent_exit - Terminate the current KLEE process without generating a
55 * test file.
56 */
58 void klee_silent_exit(int status);
59
60 /* klee_abort - Abort the current KLEE process. */
62 void klee_abort(void);
63
64 /* klee_report_error - Report a user defined error and terminate the current
65 * KLEE process.
66 *
67 * \arg file - The filename to report in the error message.
68 * \arg line - The line number to report in the error message.
69 * \arg message - A string to include in the error message.
70 * \arg suffix - The suffix to use for error files.
71 */
73 void klee_report_error(const char *file,
74 int line,
75 const char *message,
76 const char *suffix);
77
78 /* called by checking code to get size of memory. */
79 size_t klee_get_obj_size(void *ptr);
80
81 /* print the tree associated w/ a given expression. */
82 void klee_print_expr(const char *msg, ...);
83
84 /* NB: this *does not* fork n times and return [0,n) in children.
85 * It makes n be symbolic and returns: caller must compare N times.
86 */
87 uintptr_t klee_choose(uintptr_t n);
88
89 /* special klee assert macro. this assert should be used when path consistency
90 * across platforms is desired (e.g., in tests).
91 * NB: __assert_fail is a klee "special" function
92 */
93# define klee_assert(expr) \
94 ((expr) \
95 ? (void) (0) \
96 : __assert_fail (#expr, __FILE__, __LINE__, __PRETTY_FUNCTION__)) \
97
98 /* Return true if the given value is symbolic (represented by an
99 * expression) in the current state. This is primarily for debugging
100 * and writing tests but can also be used to enable prints in replay
101 * mode.
102 */
103 unsigned klee_is_symbolic(uintptr_t n);
104
105
106 /* Return true if replaying a concrete test case using the libkleeRuntime library
107 * Return false if executing symbolically in KLEE.
108 */
109 unsigned klee_is_replay(void);
110
111
112 /* The following intrinsics are primarily intended for internal use
113 and may have peculiar semantics. */
114
115 void klee_assume(uintptr_t condition);
116 void klee_warning(const char *message);
117 void klee_warning_once(const char *message);
118 void klee_prefer_cex(void *object, uintptr_t condition);
119 void klee_posix_prefer_cex(void *object, uintptr_t condition);
120 void klee_mark_global(void *object);
121
122 /* Return a possible constant value for the input expression. This
123 allows programs to forcibly concretize values on their own. */
124#define KLEE_GET_VALUE_PROTO(suffix, type) type klee_get_value##suffix(type expr)
125
129 KLEE_GET_VALUE_PROTO(ll, long long);
130 KLEE_GET_VALUE_PROTO(_i32, int32_t);
131 KLEE_GET_VALUE_PROTO(_i64, int64_t);
132
133#undef KLEE_GET_VALUE_PROTO
134
135 /* Ensure that memory in the range [address, address+size) is
136 accessible to the program. If some byte in the range is not
137 accessible an error will be generated and the state
138 terminated.
139
140 The current implementation requires both address and size to be
141 constants and that the range lie within a single object. */
142 void klee_check_memory_access(const void *address, size_t size);
143
144 /* Enable/disable forking. */
145 void klee_set_forking(unsigned enable);
146
147 /* Print stack trace. */
149
150 /* Print range for given argument and tagged with name */
151 void klee_print_range(const char * name, int arg );
152
153 /* Open a merge */
154 void klee_open_merge(void);
155
156 /* Merge all paths of the state that went through klee_open_merge */
158
159 /* Get errno value of the current state */
160 int klee_get_errno(void);
161#ifdef __cplusplus
162}
163#endif
164
165#endif /* KLEE_H */
void klee_report_error(const char *file, int line, const char *message, const char *suffix)
Definition: klee-replay.c:512
void klee_mark_global(void *object)
Definition: klee-replay.c:517
int const char * message
Definition: klee.h:75
void klee_open_merge(void)
void klee_posix_prefer_cex(void *object, uintptr_t condition)
Definition: klee-replay.c:455
int line
Definition: klee.h:74
uintptr_t klee_choose(uintptr_t n)
void klee_warning_once(const char *message)
int klee_int(const char *name)
void klee_stack_trace(void)
void klee_print_expr(const char *msg,...)
void klee_prefer_cex(void *object, uintptr_t condition)
Definition: klee-replay.c:451
void klee_check_memory_access(const void *address, size_t size)
size_t klee_get_obj_size(void *ptr)
int klee_get_errno(void)
Definition: klee-replay.c:428
int const char const char * suffix
Definition: klee.h:76
unsigned klee_is_symbolic(uintptr_t n)
Definition: klee-replay.c:447
void klee_print_range(const char *name, int arg)
unsigned klee_is_replay(void)
void klee_close_merge(void)
#define KLEE_GET_VALUE_PROTO(suffix, type)
Definition: klee.h:124
int klee_range(int begin, int end, const char *name)
Definition: klee-replay.c:489
void klee_warning(const char *message)
void klee_make_symbolic(void *addr, size_t nbytes, const char *name)
Definition: klee-replay.c:459
__attribute__((noreturn)) void klee_silent_exit(int status)
void klee_define_fixed_object(void *addr, size_t nbytes)
void klee_assume(uintptr_t condition)
Definition: klee-replay.c:440
void klee_set_forking(unsigned enable)
void noreturn
Definition: ErrorHandling.h:29