-
Notifications
You must be signed in to change notification settings - Fork 2k
/
Copy pathsledge-help.txt
419 lines (326 loc) · 19.7 KB
/
sledge-help.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
SLEdge static analyzer
sledge SUBCOMMAND
The [-trace <spec>] argument of each subcommand enables debug tracing according to <spec>, which is a sequence of module and function names separated by + or -. For example, M-M.f enables all tracing in the M module except the M.f function. The <spec> value * enables all debug tracing.
=== subcommands ===
buck . integration with Buck
. bitcode . report bitcode files in buck target
. link . link buck target to LLVM bitcode
llvm . integration with LLVM
. analyze . analyze LLVM bitcode
. translate . translate LLVM bitcode to LLAIR
. disassemble . translate LLVM bitcode to LLAIR and print in
textual form
analyze . analyze LLAIR code
validate . validate goal trace witness
disassemble . print LLAIR code in textual form
smt . process SMT-LIB benchmarks
version . print version information
help . explain a given subcommand (perhaps recursively)
====== sledge buck ======
integration with Buck
sledge buck SUBCOMMAND
Code can be provided by a buck build target, such as //fully/qualified/build:target. The mechanism used to integrate with buck uses the arguments passed to the linker, so the target must specify a binary that will be linked, not for instance a library archive. Sledge passes the --config sledge.build=True flag to buck, which can be used to configure buck targets for sledge.
=== subcommands ===
bitcode . report bitcode files in buck target
link . link buck target to LLVM bitcode
help . explain a given subcommand (perhaps recursively)
====== sledge buck bitcode ======
report bitcode files in buck target
sledge buck bitcode <target>
Build a buck target and report the included bitcode files.
=== flags ===
[-append-report] . append to report file
[-colors] . enable printing in colors
[-margin <cols>] . wrap debug tracing at <cols> columns
[-modules <file>] . write list of bitcode files to <file>, or to
standard output if <file> is `-`
[-report <file>] . write report sexp to <file>, or to standard error
if "-"
[-trace <spec>] . enable debug tracing
[-unbuffered] . disable buffering of stdout and stderr
[-help], -? . print this help text and exit
====== sledge buck link ======
link buck target to LLVM bitcode
sledge buck link <target>
Link code in a buck target to a single LLVM bitcode module. This also internalizes all symbols except `main` and removes dead code.
=== flags ===
-bitcode-output <file> . write linked bitcode to <file>
[-append-report] . append to report file
[-colors] . enable printing in colors
[-fuzzer] . add a harness for libFuzzer targets
[-margin <cols>] . wrap debug tracing at <cols> columns
[-modules <file>] . write list of bitcode files to <file>, or to
standard output if <file> is `-`
[-report <file>] . write report sexp to <file>, or to standard error
if "-"
[-trace <spec>] . enable debug tracing
[-unbuffered] . disable buffering of stdout and stderr
[-help], -? . print this help text and exit
====== sledge llvm ======
integration with LLVM
sledge llvm SUBCOMMAND
=== subcommands ===
analyze . analyze LLVM bitcode
translate . translate LLVM bitcode to LLAIR
disassemble . translate LLVM bitcode to LLAIR and print in
textual form
help . explain a given subcommand (perhaps recursively)
====== sledge llvm analyze ======
analyze LLVM bitcode
sledge llvm analyze <input>
Analyze LLVM bitcode. This is a convenience wrapper for the sequence `sledge llvm translate`; `sledge analyze`.
=== flags ===
[-O0] . optimization level 0
[-O1] . optimization level 1
[-O2] . optimization level 2
[-O3] . optimization level 3
[-Os] . like -O2 with extra optimizations for size
[-Oz] . like -Os but reduces code size further (default)
[-append-report] . append to report file
[-cct-schedule-points] . context switch only at cct_point calls
[-colors] . enable printing in colors
[-domain <string>] . select abstract domain; must be one of "sh"
(default, symbolic heap domain), "globals"
(used-globals domain), or "unit" (unit domain)
(can be: globals, itv, sh, unit)
[-dump-bitcode <file>] . write transformed LLVM bitcode to <file>
[-dump-query <int>] . dump solver query <int> and halt
[-dump-simplify <int>] . dump simplify query <int> and halt
[-dump-witness <file>] . dump goal witness trace to <file>
[-function-summaries] . use function summaries (in development)
[-goal-trace <file>] . specify a trace to try to explore, in the form of
a file containing one LLVM function name per
line. If provided, translation avoids inlining
traced functions and analysis prioritizes trace
progress. When an execution is found that visits
each function in order, terminate if
"Stop.on_reached_goal" is being traced.
[-llair-output <file>] . write generated textual LLAIR to <file>, or to
standard output if "-"
[-loop-bound <int>], -bound
. limit execution exploration to <int> loop
iterations, a negative bound is never hit and
leads to unbounded exploration
[-margin <cols>] . wrap debug tracing at <cols> columns
[-max-disjuncts <int>] . set an upper bound on the number of
constant-return summary disjuncts in the distance
heuristic pre-analysis. If set to 0, disable
constant propagation entirely; if set to a
negative number, allow unboundedly-many disjuncts
[-no-internalize] . do not internalize all functions except the entry
points specified in the config file
[-no-simplify-states] . do not simplify states during symbolic execution
[-no-strong-infer-frame] . do not fallback to Z3 before failing infer_frame
queries
[-normalize-states] . normalize states during symbolic execution
[-output <file>] . write generated binary LLAIR to <file>
[-preanalyze-globals] . pre-analyze global variables used by each
function
[-report <file>] . write report sexp to <file>, or to standard error
if "-"
[-sample] . randomly sample execution paths
[-seed <int>] . specify random number generator seed
[-stats] . output performance statistics to stderr
[-switch-bound <int>], -yield
. limit execution exploration to <int> context
switches, a negative bound is never hit and leads
to unbounded exploration
[-trace <spec>] . enable debug tracing
[-unbuffered] . disable buffering of stdout and stderr
[-help], -? . print this help text and exit
====== sledge llvm translate ======
translate LLVM bitcode to LLAIR
sledge llvm translate <input>
Translate LLVM bitcode to LLAIR. The <input> file must contain LLVM bitcode in either binary (.bc) or textual (.ll) form.
=== flags ===
[-O0] . optimization level 0
[-O1] . optimization level 1
[-O2] . optimization level 2
[-O3] . optimization level 3
[-Os] . like -O2 with extra optimizations for size
[-Oz] . like -Os but reduces code size further (default)
[-append-report] . append to report file
[-colors] . enable printing in colors
[-dump-bitcode <file>] . write transformed LLVM bitcode to <file>
[-goal-trace <file>] . specify a trace to try to explore, in the form of
a file containing one LLVM function name per
line. If provided, translation avoids inlining
traced functions and analysis prioritizes trace
progress. When an execution is found that visits
each function in order, terminate if
"Stop.on_reached_goal" is being traced.
[-llair-output <file>] . write generated textual LLAIR to <file>, or to
standard output if "-"
[-margin <cols>] . wrap debug tracing at <cols> columns
[-max-disjuncts <int>] . set an upper bound on the number of
constant-return summary disjuncts in the distance
heuristic pre-analysis. If set to 0, disable
constant propagation entirely; if set to a
negative number, allow unboundedly-many disjuncts
[-no-internalize] . do not internalize all functions except the entry
points specified in the config file
[-output <file>] . write generated binary LLAIR to <file>
[-report <file>] . write report sexp to <file>, or to standard error
if "-"
[-trace <spec>] . enable debug tracing
[-unbuffered] . disable buffering of stdout and stderr
[-help], -? . print this help text and exit
====== sledge llvm disassemble ======
translate LLVM bitcode to LLAIR and print in textual form
sledge llvm disassemble <input>
The <input> file must be LLVM bitcode.
=== flags ===
[-O0] . optimization level 0
[-O1] . optimization level 1
[-O2] . optimization level 2
[-O3] . optimization level 3
[-Os] . like -O2 with extra optimizations for size
[-Oz] . like -Os but reduces code size further (default)
[-append-report] . append to report file
[-colors] . enable printing in colors
[-dump-bitcode <file>] . write transformed LLVM bitcode to <file>
[-goal-trace <file>] . specify a trace to try to explore, in the form of
a file containing one LLVM function name per
line. If provided, translation avoids inlining
traced functions and analysis prioritizes trace
progress. When an execution is found that visits
each function in order, terminate if
"Stop.on_reached_goal" is being traced.
[-llair-output <file>] . write generated textual LLAIR to <file>, or to
standard output if "-"
[-margin <cols>] . wrap debug tracing at <cols> columns
[-max-disjuncts <int>] . set an upper bound on the number of
constant-return summary disjuncts in the distance
heuristic pre-analysis. If set to 0, disable
constant propagation entirely; if set to a
negative number, allow unboundedly-many disjuncts
[-no-internalize] . do not internalize all functions except the entry
points specified in the config file
[-output <file>] . write generated binary LLAIR to <file>
[-report <file>] . write report sexp to <file>, or to standard error
if "-"
[-trace <spec>] . enable debug tracing
[-unbuffered] . disable buffering of stdout and stderr
[-help], -? . print this help text and exit
====== sledge analyze ======
analyze LLAIR code
sledge analyze <input>
The <input> file must be binary LLAIR, such as produced by `sledge translate`.
=== flags ===
[-append-report] . append to report file
[-cct-schedule-points] . context switch only at cct_point calls
[-colors] . enable printing in colors
[-domain <string>] . select abstract domain; must be one of "sh"
(default, symbolic heap domain), "globals"
(used-globals domain), or "unit" (unit domain)
(can be: globals, itv, sh, unit)
[-dump-query <int>] . dump solver query <int> and halt
[-dump-simplify <int>] . dump simplify query <int> and halt
[-dump-witness <file>] . dump goal witness trace to <file>
[-function-summaries] . use function summaries (in development)
[-goal-trace <file>] . specify a trace to try to explore, in the form of
a file containing one LLVM function name per
line. If provided, translation avoids inlining
traced functions and analysis prioritizes trace
progress. When an execution is found that visits
each function in order, terminate if
"Stop.on_reached_goal" is being traced.
[-llair-output <file>] . write generated textual LLAIR to <file>, or to
standard output if "-"
[-loop-bound <int>], -bound
. limit execution exploration to <int> loop
iterations, a negative bound is never hit and
leads to unbounded exploration
[-margin <cols>] . wrap debug tracing at <cols> columns
[-max-disjuncts <int>] . set an upper bound on the number of
constant-return summary disjuncts in the distance
heuristic pre-analysis. If set to 0, disable
constant propagation entirely; if set to a
negative number, allow unboundedly-many disjuncts
[-no-simplify-states] . do not simplify states during symbolic execution
[-no-strong-infer-frame] . do not fallback to Z3 before failing infer_frame
queries
[-normalize-states] . normalize states during symbolic execution
[-preanalyze-globals] . pre-analyze global variables used by each
function
[-report <file>] . write report sexp to <file>, or to standard error
if "-"
[-sample] . randomly sample execution paths
[-seed <int>] . specify random number generator seed
[-stats] . output performance statistics to stderr
[-switch-bound <int>], -yield
. limit execution exploration to <int> context
switches, a negative bound is never hit and leads
to unbounded exploration
[-trace <spec>] . enable debug tracing
[-unbuffered] . disable buffering of stdout and stderr
[-help], -? . print this help text and exit
====== sledge validate ======
validate goal trace witness
sledge validate <input>
The <input> file must have been produced by `sledge analyze -dump-witness`.
=== flags ===
[-append-report] . append to report file
[-colors] . enable printing in colors
[-jobs <int>], -j . use the given number of parallel processes
[-margin <cols>] . wrap debug tracing at <cols> columns
[-report <file>] . write report sexp to <file>, or to standard error
if "-"
[-trace <spec>] . enable debug tracing
[-unbuffered] . disable buffering of stdout and stderr
[-help], -? . print this help text and exit
====== sledge disassemble ======
print LLAIR code in textual form
sledge disassemble <input>
The <input> file must be LLAIR code, as produced by `sledge llvm translate`.
=== flags ===
[-append-report] . append to report file
[-colors] . enable printing in colors
[-goal-trace <file>] . specify a trace to try to explore, in the form of
a file containing one LLVM function name per
line. If provided, translation avoids inlining
traced functions and analysis prioritizes trace
progress. When an execution is found that visits
each function in order, terminate if
"Stop.on_reached_goal" is being traced.
[-llair-output <file>] . write generated textual LLAIR to <file>, or to
standard output if "-"
[-margin <cols>] . wrap debug tracing at <cols> columns
[-max-disjuncts <int>] . set an upper bound on the number of
constant-return summary disjuncts in the distance
heuristic pre-analysis. If set to 0, disable
constant propagation entirely; if set to a
negative number, allow unboundedly-many disjuncts
[-report <file>] . write report sexp to <file>, or to standard error
if "-"
[-trace <spec>] . enable debug tracing
[-unbuffered] . disable buffering of stdout and stderr
[-help], -? . print this help text and exit
====== sledge smt ======
process SMT-LIB benchmarks
sledge smt <input>
The <input> file is interpreted as an SMT-LIB 2 benchmark.
=== flags ===
[-append-report] . append to report file
[-colors] . enable printing in colors
[-margin <cols>] . wrap debug tracing at <cols> columns
[-report <file>] . write report sexp to <file>, or to standard error
if "-"
[-trace <spec>] . enable debug tracing
[-unbuffered] . disable buffering of stdout and stderr
[-help], -? . print this help text and exit
====== sledge version ======
print version information
sledge version
=== flags ===
[-build-info] . print build info for this build
[-version] . print the version of this build
[-help], -? . print this help text and exit
====== sledge help ======
explain a given subcommand (perhaps recursively)
sledge help [SUBCOMMAND]
=== flags ===
[-expand-dots] . expand subcommands in recursive help
[-flags] . show flags as well in recursive help
[-recursive] . show subcommands of subcommands, etc.
[-help], -? . print this help text and exit