SWEET Help
SWEET version 7934 (2018-09-12)
Executing command ‘help’.
Options available for SWEET version 7934.
-i,–input-files=<file-name(s)> Specifies the code to be analyzed.
Meaning of <file-name(s)>: The name of the file(s) to analyze. In case of
multiple files to be linked together (only for alf), these should be separated
by , (comma).
Parameters:
lang= The language of the code. can be one of:
auto - (default) Makes assumptions based on the file suffix.
alf - One or more ALF file(s).
cfg - File containing set of control-flow graphs. Useful for
trace-based flow hypothesis generation (see -ae rtf).
func= The start function for all analyses. By default the
root function is the start function.
annot= Reads a file with abstract annotations. Use the help 'help
topic=annot' option to learn more about the format of the
annotation file.
outannot= Reads a file with output annotations specifications.
The resulting output annotations are written to a file named: the
file base name of file-name with the suffix ".out" appended.
merged_output= Control if the values in the output annotations are merged
or not. can be one of:
yes - The values in the output annotations are merged.
no - The values in the output annotations are not merged, but
instead given as discrete values separated by 'OR'.
unmangle Unmangle identifiers. Useful to make linking of several ALF files
possible. Removes the :: suffix which melmac appends to
all identifiers
rde Remove duplicate exports. When having functions that are exported
from several ALF files all but one definition of the function are
removed. Which definition to keep is unspecified, since it is
assumed that all definitions are identical. Default off.
-c,–check-statically Check the parsed program for consistency.
Parameters:
size= Checks if the sizes of expressions are consistent, and if there
are unsupported constructs in the program. can be one of:
on - (default) Turns on this check
off - Turns off this check
connected= Checks if the call graph is connected, i.e. if there is an
unumbigous start point for the analysis. can be one of:
on - (default) Turns on this check
off - Turns off this check
extref= Checks if there are any unresolved external references in the
program (like calls to external functions or accesses to external
global variables). can be one of:
on - (default) Turns on this check
off - Turns off this check
fcall= Checks that (non-function-pointer) function calls are made with
right amount of parameters, that each function has at least one
return statement, that all return statements has the same amount
of parameters, and that calls and returns are consistent in terms
of parameters. can be one of:
on - (default) Turns on this check
off - Turns off this check
-m,–map-file Loads a file mapping from statements to corresponding C-source
code.
Parameters:
file= Specifies the file name of the map file. If this parameter
is not given, the base name of the program file with the suffix
".map" will be used. In case more than one program file is given
to -i, the corresponding .map files are assumed to be named as the
base names of the program files, with ".map" appended. This
parameter should then not be given. Meaning of : The
name of the map file.
rcs Read C sources - Open C files specified in the map file and read
C-lines from them to internal mappings.
c Check map file content. Controls that each basic block has a
corresponding c source reference in the map file.
pal= Print .map file after linking.
Analyses
-do,–domain Configures the domain to be used by SWEET.
Parameters:
type= The domain to be used for integers and offsets in pointers.
can be one of:
int - (default) Intervals
clp - Circular Linear Progressions
floats= How to handle floats. can be one of:
top - (default) All calculations of floating point values
result in TOP (safe).
est - A best effort analysis that tries to estimate
floating-point values rather than returning TOP, even
though the analysis may be unsound (due to different
floating point value representation on the host and on the
target).
reuse= Specifies that reuse (i.e. 'copy-on-write') of internal parts of
abstract states should be used. Instead of always making deep
copies of internal objects the states are allowed to share these
objects. The actual copying takes place when a state wants to
update its particular object. Saves memory and execution time for
both VA and AE. If one or more options except 'all' or 'none' is
given other one options will be turned off. Alternatives marked
with '*' only concerns the AE. can be one or more:
all - (default)
none -
f - Frames
c - Frame collections
e - Variable environments
r - Recorders*
h - Recorder holders*
edo Only read/write at offsets evenly dividable by size of previously
read/written values.
noglobinitSkips the global init section. Initial values will be top or
restricted by annotations.
-ae,–abstract-execution Run abstract execution to produce flow facts.
Parameters:
ffg= The flow fact generators (ffgs) to use. Given using four
dimensions (as a four letter string): 1. bounds derived: upper
(u), lower and upper (l), infeasible (i). 2. entities kept track
of: headers (h), nodes (n), edges (e), call-edges (c),
loop-body-begin-edges (b). 3. combination of entities: single
(s), pairs (p), paths (n). 4. flow fact context: each iteration
(e), all iterations (a), scope (s), function (f), program (p).
can be one or more:
uhss - (default) Upper header bounds in scope context (default
on, but must be given if ffg is used). (u)
lhss - Lower header node bounds in scope context. (l)
uhsf - Upper header node bounds in function context. (u)
lhsf - Lower header node bounds in function context. (l)
uhsp - Upper header node bounds in program context. (u)
lhsp - Lower header node bounds in program context. (l)
uhpf - Upper bounds for header pairs in function context. (u)
lhpf - Lower bounds for header pairs in function context. (l)
uhpp - Upper bounds for header pairs in program context. (u)
lhpp - Lower bounds for header pairs in program context. (l)
unss - Upper bounds for nodes in scope context. (u)
lnss - Lower bounds for nodes in scope context. (l)
unsf - Upper bounds for nodes in function context. (u)
lnsf - Lower bounds for nodes in function context. (l)
unsp - Upper bounds for nodes in program context. (u)
lnsp - Lower bounds for nodes in program context. (l)
inse - Nodes never taken for individual iterations of scope. (u)
insa - Nodes never taken for all iterations of scope. (u)
unps - Upper bounds for node pairs in scope-context. (u)
lnps - Lower bounds for node pairs in scope context. (l)
unpf - Upper bounds for node pairs in function-context. (u)
lnpf - Lower bounds for node pairs in function context. (l)
unpp - Upper bounds for node pairs in program-context. (u)
lnpp - Lower bounds for node pairs in program context. (l)
inpa - Excluding node pairs for all iterations of scope (ie.
nodes never executed together for any iteration) (u). If
no merging is used also reports on node pairs that must be
taken together (ie. each iteration either none or both
nodes must be taken).
uess - Upper bounds for edges in scope context. (u)
less - Lower bounds for edges in scope context. (l)
uesf - Upper bounds for edges in function context. (u)
lesf - Lower bounds for edges in function context. (l)
uesp - Upper bounds for edges in program context. (u)
lesp - Lower bounds for edges in program context. (l)
ucsf - Upper bounds for call edges in function context. (u)
lcsf - Lower bounds for call edges in function context. (l)
ucsp - Upper bounds for call edges in program context. (u)
lcsp - Lower bounds for call edges in program context. (l)
ubns - Upper bounds for sum of loop body begin edges in scope
context (i.e. an upper bound on the number of times the
loop body can be taken for each entry of the loop). (u)
lbns - Lower bounds for sum of loop body begin edges in scope
context (i.e. bounds on the number of times the loop body
can be taken for each entry of the loop). (l)
all - All ffgs should be used, i.e. both (u) and (l) ffgs
allnoinse - All ffgs except inse (since inse may give problems in
low-sweet
ub - Upper bounds ffgs should be used. Includes ffgs marked
with (u).
lb - Lower bounds ffgs should be used. Includes ffgs marked
with (l).
merge= The merge points to be used. can be one or more:
all - (default) All merge points (fe,fe,le,be,je).
none - No merging should be used.
fe - Each function entry point.
fr - Each function return point.
le - Each loop exit edge.
be - Each back-edge.
je - Each point of joining edges.
df Execute in a depth first manner rather than breadth first manner.
usm Use unordered state merge strategy.
op Optimized single path execution.
debug= Turns on debugging. can be one of:
inter - Interactive debugger
trace - Prints a trace to the file debug_msgs.txt
tc= Type counting. Reports for each type its number of occurrences
during the execution. can be one or more:
all - Use all type countings, i.e gn,op,st,sp.
gn - Generic nodes, i.e. i.e. nodes in ALF syntax tree.
op - Operators, i.e. add, sub, ...
st - Statements, i.e. store, call, ...
sp - Statement pairs, i.e. <store,store>, <store,call>, ...
scp - Simple count printout, prints counts as integers on a
single line (is actually no counter report, just a
printout directive)
css Check single state, i.e., throw run-time error if more than one
state is generated during AE. Mostly for debugging purposes.
ene Extended handling of equal and not equal condition.
ft= How to handle the fall-through state. can be one of:
c - (default) Continue with the fall-through state if it is
not bottom (C standard, used by melmac).
n - Do not continue with the fall-through state (new ALF
standard since late 2011).
w - Do not continue with the fall-through state and warn if
it is not bottom - this may be due to overestimations.
vola= How to handle volatiles. If volatiles occur in the program and AE
is run this flag must be set. can be one of:
i - Ignore volatile keyword in frame initializations. Treat
volatile declared frames as normal frames.
t - Set all volatile frames to top values. All writes to
frame will be ignored.
isi Ignore stores to integer addresses. Stores where the address is a
concrete integer value are skipped, and therefore have no effect
on the program state. Normally, such addresses are interpreted as
TOP addresses, which results in that the stored value is stored to
all locations in all memory frames, after first being LUBed with
the value already stored at each location. This option is useful
when analyzing code that contains stores to absolute memory
addresses, for example, when memory-mapped I/O is used. With this
option turned on, the analysis makes the unsafe assumption that
these memory locations are disjoint from the memory locations used
by regular variables in the program. Note that loads from such
addresses are not skipped and will return TOP values, but that
would happen in the normal case as well.
pu Process undefined functions, which means that calls to undefined
functions will simply not be made. Further, all undefined global
variables will initially be set to TOP, but become updated
according to writes made during the AE analysis. Option must be
set if AE should be run on code containing imports to functions
that are not provided.
gtf= Generate trace file, i.e., print the names's of the CFG
nodes taken during execution. Throws, similar to ccs, a run-time
error if more than one state is generated during AE.
rtf= Read trace from file and runs AE according to trace. A trace
file can consist of several traces. A trace is a space-separated
list of node names. Each trace ends with a semicolon.
aac= Generate BCET and WCET estimate using ALF AST construct
costs. The input file holds the ALF AST construct costs. Requires
tc parameter to be set. Only cost for code constructs set by tc
will be used in BCET/WCET calc.
aacpaths If set the aac option will also generate a BCET and WCET path
based on the ALF AST construct costs. The paths will be printed
to screen and are lists of basic block names. Can only be used
together with aac.
oaac= Old version of aac. Has same tc requirement.
bbc= Generate BCET and WCET estimate using basic block and edges
cost table. The input file holds the cost lookup table for basic
blocks and edges. Table rows should be on form BBID COST (node
with single cost) or BBID COST1 COST2 (node with lower and upper
cost) or BBID1 BBID2 COST (edge with single cost) or BBID1 BBID2
COST1 COST2 (edge with lower and upper cost). BBID is a string not
starting with a number or a minus. COST is a (potentially
negative) integer.
bbcpaths If set the bbc option will also generate a BCET and WCET path
based on the BB cost lookup table. The paths will be printed to
screen and are lists of basic block names. Can only be used
together with bbc.
-td,–timing-database Create a timing database (tdb) for basic blocks of ALF
program based on cost lookup table (clt) holding timing costs for
ALF code constructs.
Parameters:
i= Specifies the name of the input clt file to read timing
for ALF code constructs from. If no file name is given default
timing values will be used.
o= Specifies the name of an output tdb file to which the
result will be written to. If no file name is given the result
will be written to stdout.
-va,–value-analysis Runs value analysis (on nodes in scope graph).
Parameters:
a= The analysis processing algorithm to use. can be one of:
n - (default) Use worklist and process in optimal node order.
l - Use worklist but do not derive/use node ordering.
j - Use chaotic (Jacobi) fixpoint analysis.
fp= The fixpoint passes to use. can be one of:
wn - (default) Widening followed by narrowing.
w - Widening only.
n - Narrowing only.
c - Classic fixpoint analysis (no narrowing or widening).
wnp= The widening and narrowing points to use. can be one of:
l - (default) Do wid and nar before last stmt in loop header.
b - Do wid and nar at back edges.
f - Do wid and nar before first stmt in loop header.
ft= How to handle the fall-through state. can be one of:
c - (default) Continue with the fall-through state if it is
not bottom (C standard, used by melmac).
n - Do not continue with the fall-through state (new ALF
standard since late 2011).
w - Do not continue with the fall-through state and warn if
it is not bottom - this may be due to overestimations.
p= Print value analysis to txt files. Generated files will be named
as _AlfValueAnalysis__.txt where i is iteration and f is
fixpoint pass. can be one of:
r - Only the final result is printed (least detailed).
f - The result after each fixpoint pass is printed.
i - The result of each iteration is printed (most detailed).
d= Draw value analysis to dot files. Generated files will be named as
_AlfValueAnalysis__.dot where i is iteration and f is
fixpoint pass. can be one of:
r - Only the final result is printed (least detailed).
f - The result after each fixpoint pass is printed.
i - The result of each iteration is printed (most detailed).
-du,–def-use-analysis Derives defines and uses of statements.
Parameters:
p Print DU analysis result to txt files. Generated files will be
named _ALFDUAnalysis.txt.
-rd,–reaching-definitions-analysis Runs reaching definitions.
Parameters:
a= The analysis processing algorithm to use. can be one of:
n - (default) Use worklist and process in optimal node order.
l - Use worklist but do not derive/use node ordering.
j - Use chaotic (Jacobi) fixpoint analysis.
p= Print RD analysis to txt files. Generated files will be named as
_ALFRDAnalysis_.txt where i is iteration. can be one of:
r - Only the final result is printed.
i - The result of each iteration is printed.
d= Draw RD analysis to dot files. Generated files will be named as
_ALFRDAnalysis_.dot where i is iteration. can be one of:
r - Only the final result is printed.
i - The result of each iteration is printed.
-pdg,–program-dependency-graph Derives a program dependency graph (PDG). Also
derives other intermediate graphs, such as program control-flow
graph (PCFG), program control-dependency graph (PCDG), program
data-dependency graph (PDDG), as well as a def-use analysis (DU).
See below for how to draw (-d) and print (-p) the graphs.
-sl,–slice Derive a slice based on a program dependency graph (PDG).
Parameters:
ent= The code entity/entities to start the slicing upon. Can not be
used together with lab or var. can be one of:
c - Conditions (includes loop exit conds).
l - Loop exit conditions.
g - Global variables.
i - Call graph root function input variables.
r - Call graph root function return stmts.
lab=<label(s)> Labels of code entities to start the slice upon. A comma
separated list of strings. Can be statement label(s) or function
name(s). If function name all statements in the function will be
in the start slice. Can not be used together with ent or vars.
var=<variables(s)> Variables to start the slice upon. If several variables
have the same name (due to local and global scoping) only one of
them will be selected. If dir=f all code and data potentially
affected by var(s) are derived. This is made by first deriving all
statements which may use the var(s) and then do a forward from
these statements. If dir=b all code and data potentially affecting
var(s) are derived. This is made by first deriving all statements
where var(s) may be defined. We then do a backward slice upon
these nodes. Can not be used together with ent or vars.
mul= How to slice upon multiple entities. can be one of:
t - (default) One single slice together on all entities.
i - Individual slices on each selected entity.
dir= The slicing direction to use. can be one of:
b - (default) Backward, derives all statements and variables
which may affect the selected entity.
f - Forward, derives all statements and variables which may
be affected by the selected entity.
p= Print slice result(s) to txt file(s). Generated file(s) will be
named _ALFSlicing_<ent/lab>_.txt. can be one or more:
all - Print all (stmts, funcs, global, local, and scoped vars).
s - Print labels of the statements.
f - Print names of the functions.
g - Print the global variables.
l - Print the local variables (using just their names).
v - Print the local variables with scope info (using func.var
or func.scope.var naming).
inv Invert the slice before printing it, i.e., report what parts were
removed from the slice as opposed to what parts remain in the
slice. This is the recommended setting when using source code
mappings (with –map-file), unless the provided map files are
guaranteed to include mappings for all statements in the source
code. Otherwise, if some source code statements do not have a
mapping, it will appear as though they were sliced away since they
are not included in the printed slice.
d Draw slice result(s) to dot file(s) as PDG graph. Generated
file(s) will be named ALFSlicing<ent/lab/var>_
.dot.
Outputs
-f,–flow-facts Generates flow fact file(s). The generated flow facts depend on
the flow fact generation algorithms used in the AE. Requires that
the AE has been run using a fully context-sensitive scope graph.
Parameters:
csl= Specifies the largest call string length that should be used for
generated flow information. Value should be either the keyword
'full' or a decimal integer >= 0. If csl value is not given zero
context-sensitivity will be used.
lang= The format of the produced flow facts. can be one or more:
ff - (default) Flow fact format, see sweet -h topic=ffg.
sg - Scope graph - includes both flow facts and a CFG.
rapita - The RAPITA format.
ais - The AIS format.
tcd - Produces a dummy tcd-file (containing only basic blocks,
no statements)
o= Specifies the flow fact file base name. By default base name
of the input file will be used. Meaning of : The output
file's base name.
co The result is printed to the console rather than to a disk file.
-p,–print-textually Print data in a textual format.
Parameters:
g= The data structures(s) to be printed. can be one or more:
cfg - (default) Control flow graph
cfgd - Control flow graph with debug info
pa - Pointer analysis
cg - Call graph
sg - Scope graph
sym - Symbol table
ast - Abstract syntax tree of the program
astl - Abstract syntax tree of the program after linkage
expl - Exported symbols after linkage.
impl - Imported symbols after linkage.
o= Specifies the graph file base name.The file name ending will
indicate the file content. If not set content will be printed to
stdout. Meaning of : The output file's base name.
co The result is printed to the console rather than to a disk file.
-d,–dot-print Print program graph(s) to dot file(s).
Parameters:
g= The graph(s) to be printed. can be one or more:
cfg - (default) Control flow graph
cfgc - Control flow graph, nodes annotated with C-code if
mappings are available. Depends on optional loaded C-code
mappings.
cg - Call graph
rsg - Reduced scope graph - cfg nodes are basic blocks
fsg - Full scope graph - cfg nodes are statements
sgh - Scope graph hierarchy - no cfg nodes are shown.
pdg - Program dependency graph (requires -pdg)
pcfg - Program control-flow graph (requires -pdg)
pcdg - Program control dependency graph (requires -pdg)
pddg - Program data dependency graph (requires -pdg)
file= Specifies the base name of the file where to print the
graph(s). A string indicating the format of the file will be
appended + a '.dot' suffix. If not given, the program file base
name will be used. Meaning of : The name of the output
file(s).
function= The name of the function where to start the
print-out. This parameter only applies to the printing of scope
graphs. Meaning of : The name of the function.
max_levels= The maximum number of levels that will be printed.
This parameter only applies to the printing of scope graphs.
Meaning of: The maximum number of levels.
dag Prints a scope graph generated in DAG form rather than as a
context sensitive graph. This parameter only applies to the
printing of scope graphs.
tt The nodes in the graph will be labelled using integers, and the
node names will appear as tool tips. This will make the graph more
dense.Currently only notified by the scope hierarchy.
-at,–annotation-templates= Tries to generate abstract annotation
templates for each imported and referenced identifiers (i.e.,
reference to undefined entity). References not possible to make
templates for it will output error messages to the console. The
annotation value will be set to TOP in case the type is known,
else the value is left to fill in manually. Other uncertenties may
be found as comments in the file. NOTE! In case of unresolved
references, the function may in general be able to update any
existing global variable, and it's the user's responsibility to
use the annotation. Information will be provided on the source
code level if label-to-C-source mapping is provided (option -m)
Meaning of : The name of the generated file.
-ct,–cost-lookup-table-template= Generate cost lookup table
template. Members of selected types are printed with zero value.
Parameters:
types= The ALF types to include in the printout. If not given all types
will be used. can be one or more:
all - All types, i.e pr+gn+op+st+sp.
pr - Program run, a basic cost for each program run.
gn - Generic nodes, i.e. nodes in ALF syntax tree.
op - Operators, i.e. add, sub, ...
st - Statements, i.e. store, call, ...
sp - Statement pairs, i.e. <store,store>, <store,call>, ...
-fi,–function-information=<func-name(s)> Extract call-graphs for selected
functions and print info.
Meaning of <func-name(s)>: A comma-separated list of function names. For each
function given, its corresponding call-graph will be derived. The call-graph
includes all functions reachable from the given function. Info will then be
derived and printed to different files according to the p parameter with
appropriate names, namely:
.alf ,.imports,
.exports, and .template.annot. All functions must be
reachable from the current root function in the call-graph.
Parameters:
p= The things to be printed. If not given all printouts will be used.
can be one or more:
all - (default) All types, i.e. alf+imp+exp+at++info.
alf - ALF program, result is written to .alf
imp - Imports, result is written to .imports
exp - Exports, result is written to .exports
at - Annot template, result is written to
.template.annots
map - Map, result is written to .map. Will only
produce result when -m is used. Note: inly implemented for
melmac code.
info - Extra info file for statistics on files content.
d= The (path and) directory to which all files produced by this
option will be written. If not given all files will be stored in
the directory in which SWEET is run.
Other
-----
-cs,--code-statistics Produces various information about the code structure.
Parameters:
o= The (path and) file to which the information will be printed.
If no file name is given the result will be printed to stdout.
-v,--version Shows the build version and date.
-h,--help Shows help text.
Parameters:
topic= Help topic, i.e., what to show help text on. can be one of:
option - (default) Shows help on SWEET's parameters and options
annot - Shows help on SWEET's input annotation language
ffg - Shows help on flow fact generation using AE. Also gives
an introduction to SWEET's (context-sensitive
valid-at-entry-of) flow fact format.
trace - Shows help on flow hypotheses generation using traces.
s Use syntax high lighting on help text.
