@@ -22,9 +22,9 @@ def klee_options(
22
22
write_ktests ,
23
23
):
24
24
if max_time and int (max_time ) > 30 :
25
- MAX_SOLVER_TIME = 10
25
+ MAX_SOLVER_TIME = 15
26
26
else :
27
- MAX_SOLVER_TIME = 5
27
+ MAX_SOLVER_TIME = 10
28
28
cmd = [
29
29
"--strip-unwanted-calls" , # removes llvm.dbg.* instructions, exponentially reduces time on some benchmarks
30
30
"--delete-dead-loops=false" , # without this optimizer removes some code, which decreases coverage
@@ -33,10 +33,11 @@ def klee_options(
33
33
"--external-calls=all" ,
34
34
"--use-forked-solver=false" ,
35
35
# "--solver-backend=stp",
36
- "--solver-backend=z3-tree" ,
36
+ # "--solver-backend=z3-tree",
37
+ "--solver-backend=bitwuzla-tree" ,
37
38
"--max-solvers-approx-tree-inc=16" ,
38
39
f"--max-memory={ int (max_memory * 0.9 )} " , # Just use half of the memory in case we have to fork
39
- "--optimize " ,
40
+ "--libc=klee " ,
40
41
"--skip-not-lazy-initialized" ,
41
42
f"--output-dir={ test_output_dir } " , # Output files into specific directory
42
43
"--output-source=false" , # Do not output assembly.ll - it can be too large
@@ -53,7 +54,6 @@ def klee_options(
53
54
# "--libc=uclibc",
54
55
# "--posix-runtime",
55
56
"--fp-runtime" ,
56
- "--x86FP-as-x87FP80=false" ,
57
57
# "--max-sym-array-size=4096",
58
58
"--symbolic-allocation-threshold=8192" ,
59
59
"--uninit-memory-test-multiplier=10" ,
@@ -68,19 +68,21 @@ def klee_options(
68
68
"--allocate-determ" ,
69
69
f"--allocate-determ-size={ min (int (max_memory * 0.6 ), 3 * 1024 )} " ,
70
70
"--allocate-determ-start-address=0x00030000000" ,
71
+ "--x86FP-as-x87FP80" ,
71
72
]
72
73
73
74
if f_err :
74
75
cmd += [
75
- "--use-alpha-equivalence=false" ,
76
+ "--optimize=true" ,
77
+ "--use-alpha-equivalence=true" ,
76
78
"--function-call-reproduce=reach_error" ,
77
- "--dump-states-on-halt-with-function-call-reproduce" ,
78
79
# "--max-cycles=0",
79
80
# "--tc-type=bug",
80
81
"--dump-states-on-halt=unreached" , # Explicitly do not dump states
81
82
"--exit-on-error-type=Assert" , # Only generate test cases of type assert
82
83
# "--dump-test-case-type=Assert", # Only dump test cases of type assert
83
84
"--search=dfs" ,
85
+ "--search=bfs" ,
84
86
# "--search=nurs:covnew", "--search=random-path","--search=dfs", "--use-batching-search",
85
87
# "--search=distance","--search=random-path","--use-batching-search",
86
88
# "--target-assert", # Target
@@ -97,8 +99,10 @@ def klee_options(
97
99
98
100
if f_cov :
99
101
cmd += [
102
+ "--optimize=false" ,
100
103
"--mem-trigger-cof" , # Start on the fly tests generation after approaching memory cup
101
104
"--use-alpha-equivalence=true" ,
105
+ "--optimize-aggressive=false" ,
102
106
"--track-coverage=all" , # Only branches and only instructions are wrong in real life. E.g., ternary operators are sometimes counted as different branches, while we stick to look at them as a single instruction from a single branch
103
107
"--use-iterative-deepening-search=max-cycles" ,
104
108
f"--max-solver-time={ MAX_SOLVER_TIME } s" ,
@@ -273,6 +277,7 @@ class KLEEF(object):
273
277
274
278
def run (self ):
275
279
test_output_dir = self .test_results_path / self .source .name
280
+ test_output_dir = self .test_results_path
276
281
# Clean-up from previous runs if needed
277
282
shutil .rmtree (test_output_dir , ignore_errors = True )
278
283
0 commit comments