Example Configuration Guide

User Manual:

Open the PDF directly: View PDF .
Page Count: 14

Download
Open PDF In Browser	View PDF

Examples for the ASSUME Static Code
Analysis Tool Exchange Format
Introduction
About this document
This document his a guhide to the ASSUME stathic code analyshis tool exchange format examples
ExampleConfiguration.xml and ExampleReport.xml.

Goals and design policies
In the frst stage of deshignhing the ASSUME SCA (stathic code analyshis) tool exchange format, we ahim to provhide a
common confgurathion and report format for SCA tools. To thhis end, the configuration format must allow the
spechifcathion of analyshis tasks as hindependent from the spechifcs of hindhivhidual tools as posshible. For example, a
common means of spechifyhing the hinterpretathion of programs needs to be establhished. Also, the SCA tool confgurathion
should fachilhitate the spechifcathion of machhine-hindependent confgurathions, e.g. hhidhing dhiferences hin the concrete paths
of source code fles. As a secondary goal, the confgurathion should be spechifable hin a modular way, fachilhitathing the
reuse of confgurathions. Whith the report format, we ahim to establhish a common hhierarchy of check categorhies whith
accompanyhing check semanthics, makhing results obtahined from dhiferent tools dhirectly comparable. Fhinally, the formats
need to be extenshible, allowhing the addhithion of language support and analyshis feature confgurathion opthions at a later
stage.
For the format deshign, we therefore use a set of guhidhing polhichies:
•

Common semanthics, e.g. for checks, are defned as needed, but should be based on the semanthics used by
exhisthing SCA tools where no confhicts arhise.

•

Te format may allow tool-dependent confgurathion, but the volume of necessary tool-dependent
confgurathion should be mhinhimhized. Users should be able to spechify analyshis tasks whithout any tool-spechifc
confgurathion at all.

•

Te format may allow the spechifcathion of local confgurathion, e.g. fle paths, but needs to provhide means to
the user to create confgurathions where any local sethings are as hisolated from the rest of the confgurathion as
posshible.

•

Te format should conshist of lhightwehight, reusable structures. Language-dependent structures should be
hisolated and thehir hintegrathion hinto the format must allow the addhithion of new language-dependent structures
whithout breakhing backward compathibhilhity.

•

Confgurathions should be composed of small, reusable and extenshible parts, whhich may be aggregated to
form a complete SCA tool confgurathion.

Feedback
Te format is work in progress, and feedback (to felhix.kutzner@khit.edu) is highly welcome.

Notation
Within XML code, italic serif-typed text <> is a placeholder for an element described in section X.
1

2

Confguration
In this section, we present most aspects of the confguration format’s current state by example (see the fle
ExampleConfiguration.xml).

Top-level structure
A confguration consists of three major parts:
1.

the common confguration (belonging to the global confguration) describing confguration items for all analysis
tools and independent of machines executing the analysis tools,

2.

the optional tool-specifc confguration (also belonging to the global confguration) allowing users to confgure
analysis tool behaviour which cannot currently be specifed in the common confguration,

3.

the local confguration, which is intended to allow users to specify e.g. concrete directory replacements for the
rsp. placeholders used in the other parts of the confguration.

For now, the confguration schema is designed with the usage of XInclude in mind: place the global and local
confgurations in separate fles and create a confguration fle by including both. Ten, users of the confguration only
need to supply a customized local confguration fle. Te high-level structure of a confguration fle is given in the
following XML snippet, with asef standing for “ASSUME SCA tool exchange format”:




<>
<>
<>
<>
<>
<>
<>

<>

<>


Global confguration
Meta information
Ushing the opthional metadata element, users may store a descrhipthion of the confgurathion fle.
<>=

Felix Kutzner (KIT)

3

Hardware targets
To keep confgurathion fles modular, most bhits of the confgurathion are stored hin enthithies hidenthifable by name, whhich
can then be combhined to spechify a concrete analyshis confgurathion. We frst present Hardware targets, whhich are
descrhipthions of the hardware on whhich the code to be analyzed his hintended to run:
<>=





Language targets
Language targets are named enthithies descrhibhing how to hinterpret source code expressed hin a ghiven programmhing
language. Currently, the format only supports C language targets. However, the confgurathion format his deshigned whith
extenshibhilhity hin mhind: new language targets, e.g. for C++, may be hintroduced at a later stage whithout afecthing exhisthing
confgurathion fles.
<>=












A C language subtarget extends another C language (sub)target whith addhithional preprocessor defnhithions, hinclude
dhirectory paths, and hindhivhidual hinclude fles needhing to be prepended to all C source code fles whhich are analyzed
ushing thhis subtarget. For example, thhis way comphiler-spechifc header fles may be prepended to the fles under
analyshis. Fhile and dhirectory paths need to be spechifed as URIs. Whithhin URIs, substrhings matchhing $_[A-Z]*_$ are
placeholders for concrete paths spechifed hin the local confgurathion. Include dhirectorhies and fles are used hin the order
4

of thehir appearance whithhin the language targets. Vhia the insertionMode atrhibute, hit may be spechifed whether the lhist
of hinclude dhirectorhies rsp. fles needs to be prepended or appended to the subtarget parent’s lhist of hinclude dhirectorhies
rsp. fles (hif applhicable).





$_LIBINCLUDES_$





Te bashic hidea his to have a generhic C language target and more concrete language targets vhia subtargets:


$_EXAMPLEMODULEPATH_$/include



Note: Te LanguageTargets lhist his not the only place hin whhich language subtarget elements may occur. For example,
whithhin source code modules, language subtargets may be spechifed for hindhivhidual fles (extendhing the language target
whhich would otherwhise be used to hinterpret that fle).

Source code modules
Source code module elements are named enthithies descrhibhing sets of fles needhing to be analyzed. Users may spechify an
opthional root URI, relathive to whhich relathive SourceFile URIs are hinterpreted. Whithhin source code modules, source fles
are hidenthifable by an ID. Source code module elements may also contahin hinformathion about whhich parts of the source
code needs to be stubbed.
<>=




Needhing further preprocessor defnhithions and header fles not vhishible to other source code fles, the fle dodgycode.c
has an hindhivhidual C language subtarget (extendhing the language target whhich would otherwhise be used to hinterpret
that fle):





5













Suppose the module ExampleModule requhires functhion stubs. Shince the spechifcathion of stubs his language-dependent,
the format ofers an opthional RequiredCStubs element whithhin source code modules. Tere are three ways of requhirhing a
C functhion to be stubbed: requhirhing a visibility controlled stub means that the stub generator should create a skeleton
stub for each vhishibhilhity-controllhing macro hidenthifer spechifed hin the VisibilityControllingSymbols lhist, controllhing
thehir vhishibhilhity vhia correspondhing #ifdef dhirecthives. Requhirhing a universal stub means requhirhing a shingle stub skeleton
to be generated, whithout the stub’s vhishibhilhity behing controlled vhia #ifdef dhirecthives. Furthermore, autogen stubs should
not be himplemented hin source code fles, but be generated on-the-fy be the analyshis tool. (Note that the analyshis tool
only needs to hinterpret autogen stubs; the other hinformathion may be used for manual stub himplementathion or by stub
skeleton generators.)
Stubbed functhions are hidenthifed vhia URIs. For the C programmhing language, the URI namespace cstub his used, whose
structure we defne as follows:
•

Functhions func havhing external lhinkage are descrhibed by cstub://globalscope/func.

•

Functhions func havhing hinternal lhinkage for the fle whith ID fleID whithhin source code module module are
descrhibed by cstub://flescope/module/fleID/func.

Stubs for functhions whith external lhinkage may be asshigned to groups. Stub generators should place all stubs of a group
hinto the same fle.













For each stub URI, at most one correspondhing stub entry may be present hin a RequiredCStubs element.
A stub module generated ushing the stub spechifcathion ghiven hin ExampleModule mhight look lhike thhis:


All stubs of the group posix_io are himplemented hin the fle groups/posix_io.c. Te stubs himplemented hin a ghiven
source code fle are lhisted whithhin a ImplementsStubs element:

6



cstub://globalscope/open
cstub://globalscope/read
cstub://globalscope/write


Te stub fancy_rng was not asshigned to a group, so hit his placed hin an hindhivhidual fle:

cstub://globalscope/fancy_rng

Fhinally, the stathic functhion read_from_kbd has a locathion correspondhing to hits stub URI:


cstub://filescope/ExampleModule/2/read_from_kbd




Havhing a module ExampleModule_stubs himplementhing the stubs for ExampleModule, we can create a thhird module
composed of the former two. To complhicate thhings, suppose that our thhird module contahins a fle himplementhing the
functhion fancy_rng, whhich his also himplemented hin the stub module.





We hinclude all fles from ExampleModule:

We also hinclude all of ExampleModule_stubs, however excludhing all fles himplementhing the stub
cstub://globalscope/fancy_rng:



Alternathively, we could have used an  element to spechify a fle to be excluded
from the hinclushion. (Shince the requhired module may requhire further modules, hit his necessary to spechify the module
name as well as the fle’s hidenthifer whithhin that module.)




Note: A language target extenshion may also be spechifed at source module level. If so, the language target used for a
source fle extends the lanugage target of the rsp. source module, whhich hin turn extends the language target used for
the analyshis task.

7

Execution model targets
Execution model targets are named enthithies spechifyhing how sofware his executed, hie. synchronous/asynchronous
executhion and entry pohints:
<>=



main




Check targets
Check targets are named enthithies hin whhich the user can confgure requhirements for checks, e.g. whhich runthime or
MISRA checks need to be supported by the stathic analyshis tool. Note that the stathic code analyshis tool should perform
all of the checks spechifed hin the check target used for analyshis, and that hit must note devhiathions from thhis
confgurathion hin the report (unsupported checks, unsupported fahilure handlhing modes).
<>=








Analysis tasks
Analysis tasks are named enthithies representhing combhinathions of hardware targets, source code modules, language
targets, check targets and executhion model targets, thereby complething a confgurathion (modulo tool-spechifc sethings).
For example, to analyze the source code module ExampleModule_joined for the archhitecture x86-64 as well as for PPC,
the user mhight create the followhing analyshis tasks:
<>=



PPC32
ExampleModule_joined
LT for ExampleModule
BasicChecks
ExampleExecModel



x86-64
ExampleModule_joined
LT for ExampleModule
8

BasicChecks
ExampleExecModel



Tool-specifc confguration
Some aspects of the confgurathion are too tool-spechifc to be spechifed hin a common confgurathion: for example, thime
and memory lhimhits mhight be spechifed ushing dhiferent granularhithies, and some sethings such as loop bounds are
dependent on the fundamental approach of the analyshis tool. Users may provhide tool confgurations contahinhing bashic
parameters such as addhithional command lhine arguments for the analyshis tool and language target extenshions
contahinhing e.g. further C preprocessor defnhithions (for a ghiven source code fle, the tool-spechifc language target
extenshion extends the language target whhich would otherwhise be used for the fle. If the fle has an hindhivhidual
language target, the tool-spechifc language target extends that target and his used hinstead).
<>=



PPC32
x86_64









Te content of the ToolSpecificConfiguration element his not defned whithhin thhis confgurathion format, relyhing on the
vendors of hindhivhidual analyshis tools to do so. For example, hin the case of QPR Verhify, such a
ToolSpecificConfiguration mhight look lhike thhis:

40




Local confguration
Fhinally, the local confguration element contahins replacement rules for URI substrhings, whhich need to be applhied to all
URIs occurhing hin the global part of the confgurathion. For thhis example, a local confgurathion mhight have the followhing
rules:
<>=






9







10

Reports
In this section, we present most aspects of the current state of the report format by example (see ExampleReport.xml).

Top-level structure
A report consists of six major parts:
1.

a copy of the confguration used to obtain the results (see section „Confguration“),

2.

a collection of execution reports,

3.

a collection of source code fle descriptions,

4.

a collection of source code location descriptions,

5.

a collection of check results,

6.

and a collection of failure traces.

Te high-level structure of a report fle is given as follows:


<>
<>
<>
<>
<>
<>


Execution report collection
An execution report his a named enthity detahilhing whhich confgurathion has been used to confgure the analyshis tool and
contahins hinformathion about the analyshis tool executhion, such as warnhings. (Note: the concept of source code locathions,
one of whhich his referenced hin the followhing example snhippet, his explahined hin a later secthion.)
<>=





  
  


11

Source storage collection
To allow the hidenthifcathion of hindhivhidual source fles as well as e.g. hinclude fles not explhichitly spechifed hin the
confgurathion’s source code modules, reports contahin a separate collecthion of source fle descrhipthions – a lhist of
unhiquely hidenthifable File elements. Where posshible, fles are hidenthifed whith thehir correspondhing source-module-level
descrhipthions vhia the module name and thehir ID whithhin that module. Moreover, a hash sum can be stored for each
source fle (computed ushing MD5 unless otherwhise spechifed ushing the hashAlg atrhibute). Te source fle descrhipthions
contahin language-dependent data: for example, a C source fle may be fagged as preprocessed, whhile a C header fle
has an hinclude dhirectory atrhibute. (Agahin, source fle descrhipthions for other languages can be added whithout breakhing
backward compathibhilhity.)
<>=











12


Source code stored outshide of fles, e.g. hin preprocessor defnhithions, can also be hidenthifed:





Source location collection
Te source locathion collecthion contahins locations hidenthifyhing places whithhin the fles descrhibed hin the source fle
collecthion. Te format supports multhiple approaches of hidenthifyhing such places: the C-spechifc one (hincludhing support
for macro expanshion) his recommended for hidenthifyhing locathions hin C source code. Addhithionally, support his provhided for
plahintext fle/lhine/column and fle/lhine locathion spechifcathions. Fhinally, ranges hin source code can be spechifed ushing a
spechial locathion type.
<>=

A bashic C soure code locathion (whithout need for macro expanshion) his ghiven by a fle/lhine/column trhiple:

If a CRealLocation reshides whithhin a preprocessor defnhithion, the lhine number his requhired to be 1.

C macro expanshions are represented by macro locations, conshisthing of a spellhing locathion ID (the locathion whithhin the
macro defnhithion) and the expanshion locathion ID (the locathion where the macro his expanded).

xsi:type="asef:CsourceRealLocation"
storageID="3" lineNo="1" colNo="1"/>
xsi:type="asef:CsourceMacroLocation"
spellingLocID="10" expansionLocID="11"/>

Ranges can be spechifed ushing a beghin and an end locathion ID:

xsi:type="asef:CsourceRealLocation"
storageID="2" lineNo="22" colNo="20"/>
xsi:type="asef:RangeLocation"
beginLocID="20" endLocID="21"/>

Fhinally, locathions can be spechifed hin plahintext fles:


13




Check result collection
Te check result collecthion contahins a Check element for each performed check. We plan to establhish a common set of
check categorhies (contahinhing e.g. the category numeric.divbyzero), onto whhich the tool-spechifc check categorhies (e.g.
Polyspace‘s ZDV category) can be mapped. Te check result (safe, unsafe or undechided) his ghiven hin the check
element‘s status atrhibute. Te tool may provhide further detahils, e.g. reasons for an undechided status, hin the
statusSupplement atrhibute. Furthermore, the tool‘s hinternal check category and status are provhided ushing the
internalCategory rsp. internalStatus atrhibutes. Fhinally, the analyshis tool may provhide free-form hinformathion about the
result hin the annotation feld.
<>=



1


12


22




Failure trace collection
Fhinally, the fahilure trace collecthion provhides addhithional hinformathion about the fahiled checks. However, thhis secthion
remahins to be deshigned.
<>=




14



---

Source Exif Data:

File Type                       : PDF
File Type Extension             : pdf
MIME Type                       : application/pdf
PDF Version                     : 1.4
Linearized                      : No
Page Count                      : 14
Language                        : en-US
Creator                         : Writer
Producer                        : LibreOffice 5.1
Create Date                     : 2017:02:14 17:40:31+01:00

EXIF Metadata provided by EXIF.tools