After SATIrE, ROSE, and PAG are installed
several commands and scripts are available. Use the command
newanalysis [-u]
for creating a new analyzer. First create a directory to hold the files of your analysis, <AnalysisName>.
Change to this directory and create two files, <AnalysisName>.set and <AnalysisName>.optla; in that directory.
Then run the command newanalysis. This command creates all required additional files that are necessary for generating the analyzer and compiling it.
You may rerun newanalysis any time. It never overwrites any .set or .optla file. It only (re)generates the files Makefile, main.h, main.C, and main-support.C that are required for building a complete analyzer.
If you need to modify the generated files main.h or main.C when creating an advanced analyzer, you can run newanalysis with option '-u' to ensure that main.C and main.h are not overwritten, if they already exist in the directory.
The analysis is specified such that it ensures that the input program is indeed a C++SL1 program (a subset of C++). Therefore it also demonstrates what C++ language constructs are in C++SL1 and how they are restricted.
If you want to create the analyzer sl1rd then you must run the following commands:The analysis is specified such that it ensures that the input program is indeed a C++SL2 program (a subset of C++). Therefore it also demonstrates what C++ language constructs are in C++SL2 and how we restrict them in this example. It also shows which ICFG nodes are relevant for considering function calls.
or run aisee without argument, activate the menu with the right-mouse button, select menu 'load file', and select the file <AnalysisName>_result.gdl in the dialog.
If you rerun the analyzer with a different cpp input file, the file <AnalysisName>_result.gdl is overwritten with the new analysis result. You can re-load and display <AnalysisName>_result.gdl by hitting 'g' (you do not need to re-select the file, nor do you need to exit aisee)
The basic aisee commands are:Use the command line option '--help' to get the following description
Usage: analyzer [OPTION]... <filename1> <filename2> ...
Frond End options:
--language=c++|c99|c89 select input language [default=c++]
--frontend-warnings show Front End warnings when parsing file(s)
--no-frontend-warnings do not show Front End warnings when parsing
file(s) [default]
-I<path> specify path for include files
--input-binary-ast=<FILENAME> read AST from binary file instead of a source file
Analysis options:
--callstringlength=<num> set callstring length to <num> [default=0]
--callstringinfinite select infinite callstring (for non-recursive
programs only)
--cfgordering=<num> set ordering that is used by the iteration
algorithm where
<num> = 1 : dfs preorder [default]
2 : bfs preorder
3 : reversed dfs postorder
4 : bfs postorder
5 : topsort scc dfs preorder
6 : topsort scc bfs preorder
7 : topsort scc reversed bfs
dfs postorder
8 : topsort scc bfs postorder
--check-ast run all ROSE tests for checking
whether ROSE-AST is correct
--no-check-ast do not run ROSE AST tests
--analysis-files=all|cl analyse all source files or only those
specified on the command line (cl)
--analysis-annotation annotate analysis results in AST and output
--no-analysis-annotation do not annotate analysis results in AST
--number-expressions number expressions and types in the ICFG
--no-number-expressions do not number expressions and types in the ICFG
--pag-memsize-mb=<num> allocate <num> MB of memory for PAG analysis
--pag-memsize-perc=<num> allocate <num>% of system memory (autodetected)
--pag-memsize-grow=<num> grow memory if less than <num>% are free after GC
--run-pointsto-analysis run a points-to analysis on the ICFG
--resolve-funcptr-calls resolve indirect calls using pointer analysis
Output options:
--statistics output analyzer statistics on stdout
--no-statistics do not show analyzer statistics on stdout
--verbose output analyzer info on stdout
--no-verbose do not print analyzer info on stdout
--output-text print analysis results for each statement
--output-collectedfuncs print all functions that are collected for
the icfg generation
--output-source=<FILENAME> generate source file with annotated
analysis results for each statement
--output-term=<FILENAME> generate Prolog term representation of input
program AST
--output-icfg=<FILENAME> output icfg of input program
--output-binary-ast=<FILENAME> write AST to binary file
--help print this help message on stdout
--help-rose print the ROSE help message on stdout
Multiple input/output files options:
--output-sourceprefix=<PREFIX> generate for each input file one output file
with prefixed name
GDL output options:
--gdl-preinfo output analysis info before cfg nodes
--no-gdl-preinfo do not output analysis info before cfg nodes
--gdl-postinfo output analysis info after cfg nodes
--no-gdl-postinfo do not output analysis info after cfg nodes
--gdl-nodeformat=FORMAT where FORMAT=varid|varname|exprid|exprsource
|asttext|no-varid|no-varname
|no-exprid|no-exprsource|no-asttext
the format can be specified multiple times to
have different formats printed at the same node
The output is only affected if VariableId
and/or ExpressionId is used in the carrier type
--output-gdl=<FILENAME> output program as gdl graph
--output-gdlanim=<DIRNAME> output animation gdl files in
directory <dirname>
Default options: --language=c++ --no-gdl-preinfo --gdl-postinfo
--callstringlength=0 --cfg-ordering=1
--no-check-ast --no-check-icfg
--number-expressions --pag-memsize-mb=5
--pag-memsize-grow=30 --no-statistics
--analysis-files=all --analyis-annotation
--verbose --gdl-nodeformat=no-asttext
--gdl-nodeformat=no-varid --gdl-nodeformat=varname
--gdl-nodeformat=no-exprid
--gdl-nodeformat=exprsource
In the TRANSFER section you can access the label of the respective cfg-node by using the variable label. If you want to use a label in a support function you must pass the label as an argument from the transfer function to the support function.
If VarRefExp(var) is matched then var can be converted to a value of type str with val-aststring(var).
If VariableSymbol(var) is matched then var can be converted to a value of type str with val-aststring(var).
If "IntVal(value)" is matched then "value" can be converted to a value of type "snum" with "val-astint(value)". Similar functions exist for the other types of integer and floating point constants. The names of the corresponding AST data types are given in the syn file.
ExprStatement(exp), _:
Each expression (not subexpression!) is bound to exp and can be matched with other patterns.
There exists one exception: Expressions in boolean expressions where temporary variables were introduced for dealing with short-circuit evaluation must be matched with LogicalIf(exp).
| Declaration | Description |
|---|---|
| varsym_varid :: VariableSymbolNT -> VariableId; | maps a variable symbol to its VariableId |
| varref_varid :: Expression -> VariableId; | maps a VarRefExp to its VariableId; it is an error to call this with any other subtype of Expression! |
| expr_exprid :: Expression -> ExpressionId; | maps the expression to its ExpressionId |
| exprid_expr :: ExpressionId -> Expression; | maps the expression identifier to the actual expression it represents |
| is_tmpvarid :: VariableId -> bool; | determines whether the variable identifier refers to a temporary variable introduced by SATIrE (for logical values, function return values, etc.) |
| varid_str :: VariableId -> str; | gives the name of the variable with the given identifier |
| exprid_str :: ExpressionId -> str; | gives the string representation of the expression with the given identifier |
| varid_exprid :: VariableId -> ExpressionId; | maps a variable identifier to an expression identifier which denotes a VarRefExp for that variable |
| type_typeid :: Type -> TypeId; | convert a type to its corresponding TypeId |
| typeid_type :: TypeId -> Type; | convert a type identifier to the actual type it represents |
| typeid_str :: TypeId -> str; | convert a type identifier to a string representation of the type |
| exprid_typeid :: ExpressionId -> TypeId; | get the type identifier for a given expression identifier |
| add_tmpvarid :: TypeId -> VariableId; | creates a new, unique temporary variable of the given type; this function returns different values for each call |
| stmt_asttext :: Statement -> str; | returns a string representing the structure of the given statement in a format very similar to PAG's pattern syntax |
| expr_asttext :: Expression -> str; | returns a string representing the structure of the given expression in a format very similar to PAG's pattern syntax |
| varid_has_location :: VariableId -> bool; | determines whether a variable has a corresponding abstract memory location |
| varid_location :: VariableId -> Location; | determine the abstract memory location corresponding to a variable; program variables have locations, SATIrE's temporary variables do not |
| exprid_has_location :: ExpressionId -> bool; | determine whether the expression allows to access an abstract memory location |
| exprid_location :: ExpressionId -> Location; | determine the abstract memory location corresponding to an expression, this can be a simple variable reference, but also a pointer dereference or other more complex expression; expressions that denote one of SATIrE's temporary variables, or expressions that do not denote an object in memory (an "lvalue") do not have locations |
| location_varsyms :: Location -> *VariableSymbolNT; | returns the list of program variables stored in the given location |
| may_be_aliased :: Location -> bool; | determines whether the given location may be "aliased", i.e., whether some other location may hold a pointer to it |
| is_ptr_location :: Location -> bool; | determines whether the given location contains a pointer to some other location |
| dereference :: Location -> Location; | returns the pointed-to location of a given location that holds a pointer |
SATIrE provides declarations and definitions for these functions.
Use the command line option '--callstringlength <num>' with your generated analyzer to set the call string to an arbitrary length <num>. Alternatively you can also set the callstring length to infinite with '--callstringinfinite' for non-recursive programs.
If PAG reports a parse error in file analysis.set it means that your *.set file has a parsing error. It does not report the correct file name.
Use the tool cpp2dot for generating a dot-file which contains a description of the ROSE-AST. Use the tool dotty for displaying the dot-file (=the AST). You can also use cpp2ps for generating a postscript file, or cpp2pdf for generating a pdf file (the thumbnails show the AST structure, each page the information of the AST node)
Example: cpp2dot test1.C test1.dot; dotty test1.dot
Example: cpp2ps test1.C test1.ps; gv test1.ps
Example: cpp2pdf test1.C test1.pdf; xpdf test1.pdf
