Submi ed o:
PROLE 2015
© Ma ía Alpuen e, Daniel Pa do & Alicia Villanue a
This wo k is licensed unde he
C ea i e Commons A ibu ion License.
In e ing Speci ica ions in he K amewo k ∗
Wo k in P og ess
Ma ía Alpuen e Daniel Pa do Alicia Villanue a
DSIC, Uni e si a Poli ècnica de València
Camino de Ve a s/n
46022 Valencia, Spain
{alpuen e,dapa pon, illanue}@dsic.up .es
Despi e i s many unques ionable bene i s, o mal speci ica ions a e no widely used in indus ial
so wa e de elopmen . In o de o educe he ime and e o equi ed o w i e o mal speci ica ions,
in his pape we p opose a echnique o au oma ically disco e ing speci ica ions om eal code.
The p oposed me hodology elies on he symbolic execu ion capabili ies ecen ly p o ided by he
K amewo k ha we exploi o au oma ically in e o mal speci ica ions om p og ams ha a e
w i en in a non– i ial agmen o C, called KERNELC. Roughly speaking, ou symbolic analysis
o KERNELC p og ams explains he execu ion o a (modi ie ) unc ion by using o he (obse e )
ou ines in he p og am. We implemen ed ou echnique in he au oma ed ool KINDSPEC 2.0, which
gene a es axioms ha desc ibe he p ecise inpu /ou pu beha io o C ou ines ha handle poin e -
based s uc u es (i.e., esul alues and s a e change). We desc ibe he implemen a ion o ou sys em
and discuss he di e ences w. . . ou p e ious wo k on in e ing speci ica ions om C code.
1 In oduc ion
Fo mal speci ica ions can be used o a ious so wa e enginee ing ac i i ies anging om documen ing
so wa e o au oma ed debugging, e i ica ion, and es -case gene a ion. Howe e , he e a e a a ie y
o easons why so wa e companies do no cu en ly conside o mal speci ica ion o be cos -e ec i e
o apply; hese include ime, complexi y, and ool suppo . Speci ica ion in e ence can help o mi iga e
hese p oblems and is also use ul o legacy p og am unde s anding and malwa e deob usca ion [5].
This pape desc ibes ou ongoing wo k in de eloping a speci ica ion in e ence sys em o heap-
manipula ing p og ams ha a e w i en in a non- i ial agmen o C called KERNELC [21], which
includes unc ions, s uc u es, poin e s, and I/O p imi i es. We ely on he ( ew i ing logic) seman ic
amewo k K[20], which acili a es he de elopmen o execu able seman ics o p og amming languages
and also allows o mal analysis ools o he de ined languages o be de i ed wi h minimal e o .
A language de ini ion in Kessen ially consis s o h ee pa s: he BNF language syn ax (anno a ed
wi h Kspeci ic a ibu es), he s uc u e o p og am con igu a ions, and he seman ic ules. Simila ly o
he classic ope a ional seman ics, p og am con igu a ions con ain an encoding o he en i onmen , he
heap, s acks, e c. and a e ep esen ed as algeb aic da a ypes in K. P og am con igu a ions o ganize he
s a e in uni s called cells, which a e labeled and can be nes ed.
Fo example, ollowing he Kno a ion, he p og am con igu a ion
h (in ,0)ikhx7→ xien hx7→ (in ,5)iheap c g (1)
∗This wo k has been pa ially suppo ed by he EU (FEDER) and he Spanish MINECO e . TIN2013-45732-C4 (DAMAS),
and by Gene ali a Valenciana e . PROMETEOII/2015/013. D. Pa do is suppo ed by FPU-ME g an FPU14/01830.
models he inal s a e o a compu a ion whose e u n alue is he in ege 0 (s o ed in he kcell, which
con ains he cu en code o be un), while p og am a iable x(s o ed in he en cell) has he alue 5
(s o ed in he memo y add ess gi en by xin he heap cell, whe e in o ma ion abou poin e s and da a
s uc u es is eco ded). Va iables ep esen ing symbolic memo y add esses a e w i en in sans-se i on .
In K, he con igu a ion (1) is a iendly ep esen a ion o he e m
<c g>
<k> (in ,0) </k>
<en > x => poin e (x) </en >
<heap> poin e (x) => (in ,5) </heap>
</c g>
Symbolic execu ion (SE) is a well-known p og am analysis echnique ha allows he p og am o be ex-
ecu ed using symbolic inpu alues ins ead o ac ual (conc e e) da a so ha i execu es he p og am by
manipula ing p og am exp essions in ol ing he symbolic alues [16,19]. Unlike conc e e execu ion,
whe e he pa h aken is de e mined by he inpu , in symbolic execu ion he p og am can ake any easible
pa h. Tha pa h is gi en by a logical cons ain on pas and p esen alues o he a iables, called pa h
condi ion because i is o med by cons ain s ha a e accumula ed on he pa h aken by he execu ion o
each he cu en p og am poin . Each symbolic execu ion pa h s ands o many ac ual p og am uns (in
ac , o exac ly he se o uns whose conc e e alues sa is y he logical cons ain s). One o he adi-
ional d awbacks o SE-based echniques is he high cos o decision p ocedu es o sol e pa h condi ions.
Recen ly, SE has ound enewed in e es due in pa o he huge ecen ad ances in decision p ocedu es
o logical sa is iabili y.
Kseman ics is adi ionally1compiled in o Maude [7] o execu ion, debugging, and model checking.
Kimplemen s eachabili y logic in he same way ha Maude implemen s ew i ing logic. In eachabili y
logic, a pa icula class o i s -o de o mulas wi h equali y (encoded as (boolean) e ms wi h logical
a iables and cons ain s o e hem) is used. These o mulas, called pa e ns, speci y hose conc e e
con igu a ions ha ma ch he pa e n algeb aic s uc u e and sa is y i s cons ain s. Since pa e ns allow
logical a iables and cons ain s o e hem, by using pa e ns, K ew i ing becomes symbolic execu ion
wi h he seman ic ules o he language [3]. The SMT sol e Z3 [18] is used in K o checking he
sa is iabili y o he pa h cons ain s.
Symbolic execu ion in K elies on an au oma ed ans o ma ion o bo h Kcon igu a ions and K
ules in o co esponding symbolic Kcon igu a ions (i.e., pa e ns) and symbolic K ules ha cap u e
all equi ed symbolic ing edien s: symbolic alues o da a s uc u e ields and p og am a iables; pa h
condi ions ha cons ain he a iables in cells; mul iple b anches when a condi ion is eached du ing
execu ion, e c. The ans o med, symbolic ules de ine how symbolic con igu a ions a e ew i en du ing
compu a ion. Roughly speaking, each da a s uc u e ield and p og am a iable o iginally holds an ini ial,
symbolic alue. Then, by symbolically execu ing a p og am s a emen , he con igu a ion cells (such as k,
en and heap in he example abo e) a e upda ed by mapping ields and a iables o new symbolic alues
ha a e ep esen ed as symbolic exp essions, while he pa h condi ions (s o ed in he pa h-condi ion cell)
a e co espondingly upda ed a each b anching poin .
Fo ins ance, he ollowing pa e n
*h (in ,0)ik
h··· x7→ x,s7→ s···ien
h··· s7→ (size 7→ ?s.size,capaci y 7→ ?s.capaci y)···iheap +c gs6=NULL ∧?s.size >0pa h-condi ion
1K’s backend is cu en ly being po ed in o Ja a, and K4.0 is expec ed o be eleased when he Ja a backend is deemed a
sui able comple e eplacemen o Maude.
speci ies he se o con igu a ions as ollows: (1) he kcell con ains he in ege alue 0; (2) in he en
cell, p og am a iable x(in ypog aphic on ) is associa ed o he memo y add ess xand sis bound o he
poin e s; and (3) in he heap cell, he ield size o scon ains he symbolic alue ?s.size (symbolic alues
a e p eceded by a ques ion ma k). Finally, sis no null and he alue o i s size ield is g ea e han 0.
In his pape , we edesign he echnique o [1] o disco e ing speci ica ions o heap-manipula ing
p og ams by adap ing he symbolic in as uc u e o K o suppo he speci ica ion in e ence p ocess
o KERNELC p og ams. Speci ica ion in e ence is he ask o disco e ing high-le el speci ica ions ha
closely desc ibe he p og am beha io . Gi en a p og am P, he speci ica ion disco e y p oblem o P
is ypically desc ibed as he p oblem o in e ing a likely speci ica ion o e e y unc ion min P ha
uses I/O p imi i es and/o modi ies he s a e o encapsula ed, dynamic da a s uc u es de ined in he
p og am. Following he s anda d e minology, any such unc ion mis called a modi ie . The in ended
speci ica ion o mis o be cleanly exp essed by using any combina ion o he non-modi ie unc ions
o P(i.e., unc ions, called obse e s), which inspec he p og am s a e and e u n alues exp essing
some in o ma ion abou he encapsula ed da a. Howe e , because he C language does no en o ce da a
encapsula ion, we canno assume pu i y o any unc ion: e e y unc ion in he p og am can po en ially
change he execu ion s a e, including he heap componen o he s a e. In o he wo ds, any unc ion
can po en ially be a modi ie ; hence we simply de ine an obse e as any unc ion whose e u n ype is
di e en om oid (i.e., po en ially exp esses a p ope y conce ning he inal heap con en s o he e u n
alue o he unc ion call).
The key idea behind ou in e ence me hodology was o iginally desc ibed in [1]. Gi en a modi ie
p ocedu e o which we desi e o ob ain a speci ica ion, we s a om an ini ial symbolic s a e sand
symbolically e alua e mon s o ob ain as a esul a se o pai s (s,s0)o ini ial and inal symbolic s a es,
espec i ely. Then, he obse e me hods in he p og am a e used o explain he compu ed inal symbolic
s a es. This is achie ed by analyzing he esul s o he symbolic execu ion o each obse e me hod
owhen i is ed wi h (sui able in o ma ion ha is easily ex ac ed om) sand s0. Mo e p ecisely, o
each pai (s,s0)o ini ial and inal s a es, a p e/pos s a emen is syn hesized whe e he p econdi ion is
exp essed in e ms o he obse e s ha explain he ini ial s a e s, whe eas he pos condi ion con ains he
obse e s ha explain he inal s a e s0. To exp ess a (pa ial) obse a ional abs ac ion o explana ion
o ( he cons ain s in) a gi en s a e in e ms o he obse e o, ou c i e ion is ha ocompu es he same
symbolic alues a he end o all i s symbolic execu ion b anches.
In con as o [1], in his wo k we ely on he newly de ined symbolic machine y o K, while [1]
was buil on a symbolic in as uc u e o KERNELC ha we manually de eloped in a qui e ad-hoc
and e o p one way, by eusing some spa e ea u es o he o mal e i ie Ma chC [23]. This s a egic
echnological change will allow us o de ine a gene ic and mo e obus amewo k o he in e ence o
speci ica ions o languages de ined wi hin he K amewo k. Also di e en ly om [1], he e we ully use
he lazy ini ializa ion app oach o [2] in o de o deal wi h complex da a s uc u es and poin e s, which
we e only pa ially adop ed in ou p e ious wo k. Wi h lazy ini ializa ion, he i s ime an unini ialized
ield o e e ence is accessed, ins ead o conside ing all he possible ins ances o hese da a s uc u es,
he execu ion is non-de e minis ically b anched by simply ini ializing he ield o he di e en scena ios:
he ield is null, poin s o a new objec wi h unini ialized ields, o poin s o an al eady c ea ed objec .
Con ibu ions We summa ize he main con ibu ions o his pape as ollows:
• In he cu en Ksys em, we e isi he app oach o ex ac ligh weigh speci ica ions om heap-
manipula ing code o [1], which consis s o a symbolic analysis ha explo es and summa izes he
beha io o a modi ie ou ine by using o he a ailable ou ines in he p og am, called obse e s.
This co esponds o he p ima y mo i a ion o his wo k: o mig a e he speci ica ion disco e y
echnique o [1] o he holis ic amewo k o he la es K elease, which is based on symbolic
execu ion, whe eas [1] elied on he Ma chC e i ica ion in as uc u e o he old Kpla o m,
which is cu en ly unsuppo ed.
• We adap he symbolic mechanism o K o deal wi h KERNELC, also adap ing and implemen ing
he lazy ini ializa ion echnique o manipula ing complex KERNELC inpu da a.
• We implemen ou speci ica ion in e ence echnique in he KINDSPEC 2.0 sys em, which ully
builds on he capabili ies o he SMT sol e Z3 [18] o no only p o e he (accumula ed pa h)
cons ain s as in Kbu also o inc emen ally simpli y hem on he ly.
Mo eo e , he syn hesized p e/pos axioms a e u he simpli ied ( o be gi en mo e compac ep-
esen a ion) and a e e en ually p esen ed in a mo e iendly suga ed o m ha abs ac s om any
implemen a ion de ails.
Rela ed wo k The wide in e es in p og am speci ica ions as helpe s o o he analysis, alida ion,
and e i ica ion p ocesses ha e esul ed in nume ous app oaches o (semi-)au oma ic compu a ion o
di e en kinds o speci ica ions. Speci ica ions can be p ope y o ien ed (i.e., desc ibed by p e-/pos
condi ions o unc ional code); s a e ul (i.e., desc ibed by some o m o s a e machine); o in ensional
(i.e., desc ibed by axioms), and can ake he o m o con ac s, in e aces, summa ies, assump ions,
in a ian s, p ope ies, componen abs ac ions, p ocess models, ules, g aphs, au oma a, e c. In his wo k,
we ocus on inpu -ou pu ela ions: gi en a p econdi ion o he s a e, we in e which modi ica ions
in he s a e a e implied, and we exp ess he ela ions as logical implica ions ha euse he p og am
unc ions hemsel es, hus imp o ing comp ehension since he use is acquain ed wi h hem. A ho ough
compa ison wi h he ela ed li e a u e can be ound in [1]. He e we only y o co e hose lines o
esea ch ha ha e in luenced ou wo k he mos .
Ou axioma ic ep esen a ion is inspi ed by [25], which elies on a model checke o symbolic exe-
cu ion and gene a es ei he Spec# speci ica ions o pa ame e ized uni es s. In con as o [25], we ake
ad an age o Ksymbolic capabili ies o gene a e simple and mo e accu a e o mulas ha a oid eason-
ing wi h he global heap because he di e en pieces o he heap ha a e eachable om he unc ion
a gumen add esses a e kep sepa a e. Unlike ou symbolic app oach, Daikon [10] and DIDUCE [13]
de ec p og am in a ian s by ex ensi e es ing. Also, Henkel and Diwan [14] dynamically disco e spec-
i ica ions o in e aces o Ja a classes by gene alizing he esul s o au oma ed es s uns as an algeb aic
speci ica ion. QUICKSPEC [6] elies on he au oma ed es ing ool QuickCheck o dis ill gene al laws ha
a Haskell p og am sa is ies. Whe eas Daikon disco e s in a ian s ha hold a exis ing p og am poin s,
QUICKSPEC disco e s equa ions be ween a bi a y e ms ha a e cons uc ed using an API, simila ly o
[14]. ABSSPEC [4] is a seman ic-based in e ence me hod ha elies on abs ac in e p e a ion and gen-
e a es laws o Cu y p og ams in he s yle o QUICKSPEC. A di e en abs ac in e p e a ion app oach
o in e app oxima e speci ica ions is [24]. A combina ion o symbolic execu ion wi h dynamic es ing
is used in Dysy [8]. An al e na i e app oach is based on induc i e ma ching lea ning: a he han using
es cases o alida e a en a i e speci ica ion, hey a e used as examples o induce he speci ica ion (e.g.,
[26,12]). Finally, Ghezzi e al. [11] in e speci ica ions o con aine -like classes and exp ess hem as
ini e s a e au oma a ha a e supplemen ed wi h g aph ans o ma ion ules.
This wo k imp o es exis ing app oaches in he li e a u e in se e al ways. Thanks o he handling
o MAUDE’s (hence K’s) equa ional a ibu es [7], algeb aic laws such as associa i i y, commu a i i y,
o iden i y a e na u ally suppo ed in ou app oach, which 1) leads o simple and mo e e icien spec-
i ica ions, and 2) makes i easy o eason abou yped da a s uc u es such as lis s (lis conca ena ion is
associa i e wi h iden i y elemen nil), mul ise s (bag inse ion is associa i e-commu a i e wi h iden i y
/0), and se s (se inse ion is associa i e-commu a i e-idempo en wi h iden i y /0). As a u he ad an age
w. . . [25], in ou amewo k, he co ec ness o he deli e ed speci ica ions can be au oma ically ensu ed
by using he exis ing K o mal ools [20]. Since ou app oach is gene ic and no ied o he Kseman ics
speci ica ion o KERNELC, we expec he me hodology de eloped in his wo k o be easily ex endable
o o he languages o which a Kseman ics is gi en.
Plan o he Pape . In Sec ion 2, we summa ize he key concep s o he K amewo k ha a e c ucial
o his wo k. Sec ion 3in oduces a unning example ha is used as a case s udy h oughou he pape
o discuss he adequacy and e ec i eness o he p oposed in e ence me hodology. Sec ion 4p esen s
how we had o adap he symbolic machine y o K o suppo speci ica ion disco e y. Finally, Sec ion 5
desc ibes ou speci ica ion in e ence p ocedu e and discusses di ec ions o u u e wo k.
2 The KF amewo k
In his sec ion, we ecall he undamen al concep s o he Kseman ic amewo k [22].
K[22] is a amewo k o enginee ing language seman ics. Gi en a syn ax and a seman ics o a
language, Kgene a es a pa se , an in e p e e , and o mal analysis ools such as model checke s and
deduc i e heo em p o e s a no addi ional cos . I also suppo s a ious backends, such as Maude and,
expe imen ally, Coq. In o he wo ds, language seman ics de ined in Kcan be ansla ed in o Maude o
Coq de ini ions. Comple e o mal p og am seman ics o Scheme, Ja a 1.4, Ja aSc ip , Py hon, Ve ilog,
and C a e cu en ly a ailable in K[20,22].
P og am con igu a ions a e ep esen ed in Kas po en ially nes ed s uc u es o labeled cells (o
con aine s) ha ep esen he p og am s a e. They include a compu a ion s ack o con inua ion (named k),
en i onmen s (en ,heap), and a call s ack (s ack), among o he s. Kcells can be lis s, maps, (mul i)se s
o compu a ions, o a mul ise o o he cells. Compu a ions ca y “compu a ional meaning” as special
nes ed lis s uc u es ha sequen ialize compu a ional asks, such as agmen s o a p og am. The pa o
he Kcon igu a ion s uc u e o he KERNELC seman ics ha is ele an o his wo k is shown below.
hKikhMapien hLis is ackhMapiheap c g
Rules in Ks a e how con igu a ions ( e ms) e ol e h oughou he compu a ion. Simila ly o con-
igu a ions, ules can also be g aphically ep esen ed and a e spli in wo le els. Changes in he cu en
con igu a ion (which is shown in he uppe le el) a e explici ly ep esen ed by unde lining he pa o
he con igu a ion ha changes. The new alue ha subs i u es he one ha changes is w i en below he
unde lined pa .
As an example, we show he KERNELC ule o assigning a alue Vo ype T o he a iable X. This
ule uses h ee cells: k,en , and heap. The en cell is a mapping o a iable names o hei memo y
posi ions, whe eas he heap cell binds he ac i e memo y posi ions o he ac ual alues. Meanwhile, he
kcell ep esen s a s ack o compu a ions wai ing o be un, wi h he le -mos (i.e., op) elemen o he
s ack being he nex compu a ion o be unde aken.
hX= (T,V)··· ikh··· X7→ X··· ien h··· X7→ _··· iheap
(T,V) (T,V)
This ule s a es ha , i he nex pending compu a ion (which may be a pa o he e alua ion o a
bigge exp ession) consis s o an assignmen X= (T,V), hen we look o Xin he en i onmen (X7→ _)
and we upda e he associa ed mapping in he memo y wi h he new alue Vo ype T( (T,V)). The
alue (T,V)is kep a he op o he s ack (i migh be used in he e alua ion o he bigge exp ession).
The es o he cell’s con en in he ule does no unde go any modi ica ion ( his is ep esen ed by he ···
ca d). This example ule e eals a use ul ea u e o K: « ules only need o men ion he minimum pa
o he con igu a ion ha is ele an o hei ope a ion». Tha is, only he cells ead o changed by he
ule ha e o be speci ied, and, wi hin a cell, i is possible o omi pa s o i by simply w i ing “··· ”. Fo
example, he ule abo e emphasizes he in e es in: he ins uc ion X= (T,V)only a he beginning o
he kcell, and he mapping om a iable X o i s memo y poin e Xa any posi ion in he en cell. Excep
o he sub e ms ha a e explici ly iden i ied, upon a iable assignmen e e y hing is kep unchanged.
The (desuga ed) K ule o KERNELC a iable assignmen is
ule <k> X = (T,V) => (T,V) ...</k>
<en >... X |-> poin e (X) ...</en >
<heap>... poin e (X) |-> (_ => (T,V)) ...</heap>
whe e he unde sco e s ands o an anonymous a iable. The ellipses a e also pa o he desuga ed K
syn ax and a e used o eplace he unnecessa y pa s o he cells. Hence, also in he desuga ed ule, he
de elope s ypically only men ion he in o ma ion ha is absolu ely necessa y in hei ules.
3 Running Example
Ou in e ence echnique elies on he classi ica ion scheme de eloped in [17] o da a abs ac ions, whe e
a unc ion (me hod) may be ei he a cons uc o , a modi ie o an obse e . A cons uc o e u ns a new
objec o he class om sc a ch (i.e., wi hou aking he objec as an inpu pa ame e ). A modi ie al e s
an exis ing class ins ance (i.e., i changes he s a e o one o mo e o he da a a ibu es in he ins ance).
An obse e inspec s he objec and e u ns a alue cha ac e izing one o mo e o i s s a e a ibu es. We
do no assume he adi ional p emise o [17] ha s a es ha obse e unc ions do no cause side e ec s
on he s a e. This is because we wan o apply ou echnique o any p og am, which may be w i en by
hi d-pa y so wa e p oduce s ha may no ollow he obse e pu i y discipline.
Le us in oduce he leading example ha we use o desc ibe he in e ence me hodology de eloped
in his pape : a KERNELC implemen a ion o an abs ac da a ype o ep esen ing doubly-linked lis s.
Since he whole example includes a o al o 13 me hods, due o space es ic ions we ha e chosen o
commen on jus one modi ie and i e obse e me hods (o which 2 a e bo h modi ie s and obse e s).
Example 1 In he KERNELCp og am o Figu e 1, we ep esen a doubly-linked lis as a da a s uc u e
(s uc Lis ) ha con ains some con en ( ield da a), a poin e o he p e ious elemen in he lis ( ield
p e ), and ano he poin e o he succesi e elemen in he lis ( ield nex ).
A call append(lis ,d) o he append unc ion p oceeds as ollows: i s , a new node new_node is
alloca ed in memo y; i is illed wi h he alue dand i s nex poin e is ini ialized o NULL since i will
become he las i em in he lis . Nex , he unc ion checks ha he p o ided lis lis is no NULL, in which
case i binds he nex poin e o he inal elemen o he lis o he newly c ea ed node, and he p e
poin e o he new node o he inal node o lis , hen e u ns he poin e o he whole esul ing lis .
O he wise, when he inpu lis lis is null, hen he p e poin e o new_node is ini ialized o NULL and
he esul ing ull- ledged lis ha consis s o one single elemen is simply e u ned.
The obse e unc ion leng h a e ses he lis by isi ing e e y node in o de o coun he numbe
o elemen s in he lis . The obse e unc ion head e u ns he da a ield o he i s node o he lis ;
las deli e s he da a ield o he las node o he lis , which is done by i s in oking e e se(lis ) o
#include <s dlib.h>
s uc Lis {
oid* da a;
s uc Lis * nex ;
s uc Lis * p e ;
};
s uc Lis * append(s uc Lis * lis , oid* d)
{
s uc Lis * new_node;
s uc Lis * inal;
new_node = (s uc Lis *) malloc(sizeo (
s uc Lis ));
new_node->da a = d;
new_node->nex = NULL;
i (lis != NULL) {
inal = lis ;
i ( inal != NULL) {
while ( inal->nex != NULL)
inal = inal->nex ;
}
inal->nex = new_node;
new_node->p e = inal;
e u n lis ;
}
else {
new_node->p e = NULL;
lis = new_node;
e u n lis ;
}
}
in leng h(s uc Lis * lis ) {
in len;
len = 0;
while (lis != NULL) {
len = len + 1;
lis = lis ->nex ;
}
e u n len;
}
s uc Lis * e e se(s uc Lis * lis ) {
s uc Lis * inal;
inal = NULL;
while (lis != NULL) {
inal = lis ;
lis = inal->nex ;
inal->nex = inal->p e ;
inal->p e = lis ;
}
e u n inal;
}
oid* head(s uc Lis * lis ) {
i (lis != NULL) {
while (lis ->p e != NULL)
lis = lis ->p e ;
}
e u n lis ->da a;
}
s uc Lis * las (s uc Lis * lis ) {
s uc Lis * e e sed;
e e sed = e e se(lis );
e u n head( e e sed);
}
in ind(s uc Lis * lis , oid* d) {
in ound;
ound = 0;
while (lis != NULL && !( ound)) {
i (lis ->da a == d)
ound = 1;
else
lis = lis ->nex ;
}
e u n ound;
}
s uc Lis * ini (s uc Lis * lis ) {
s uc Lis * aux;
i (lis != NULL) {
i (lis ->nex != NULL) {
aux = lis ->nex ;
while (aux->nex ->nex != NULL)
aux = aux->nex ;
aux->nex = NULL;
}
else
lis = NULL;
e u n lis ;
}
Figu e 1: KERNELC implemen a ion o a doubly-linked lis .
compu e a mi o ed e sion o he pa ame e lis and hen accessing he da a ield o i s i s node. The
unc ion ini (lis ) e u ns he same lis a e emo ing he las i em o he lis . Finally, he obse e
ind looks o he p o ided d alue in he lis , and e u ns 1(which s ands o ue) i he d alue is
ound; o he wise, he alue 0(which s ands o alse) is e u ned.
F om he p og am code o Example 1, o each modi ie unc ion m, we aim o syn hesize an ax-
ioma ic speci ica ion ha consis s o a se o implica ion o mulas 1⇒ 2, whe e 1and 2a e conjunc-
ions o equa ions o he o m l= . The le -hand side lo each equa ion can be ei he
• a call o an obse e unc ion and hen ep esen s he e u n alue o ha call;
• he keywo d e , and hen ep esen s he alue e u ned by he modi ie unc ion mbeing ob-
se ed.
In o mally, he s a emen s on he le -hand and igh -hand sides o he symbol ⇒a e espec i ely
sa is ied be o e and a e he execu ion o a unc ion call o m. We adop he s anda d p imed no a ion o
ep esen ing a iable alues a e he execu ion.
Example 2 Conside again he p og am o Example 1. The speci ica ion o he (modi ie ) unc ion
append ha inse s an elemen da he end o he lis lis is shown in Figu e 2. The speci ica ion
leng h(lis ) = 0∧
e e se(lis ) = NULL ∧
ind(lis ,d) = 0∧
ini (lis ) = NULL ∧
las (lis ) = NULL
⇒
leng h(lis 0) = 1∧
e e se(lis 0) = lis ∧
ind(lis 0,d) = 1∧
ini (lis 0) = NULL ∧
las (lis 0) = d∧
e =lis 0
leng h(lis ) = x∧
leng h(lis )>0⇒
leng h(lis 0) = x+1∧
ind(lis 0,d) = 1∧
las (lis 0) = d∧
e =lis 0
Figu e 2: Expec ed speci ica ion o he append(lis ,d) unc ion call.
consis s o wo implica ions s a ing he condi ions ha a e sa is ied be o e and a e he execu ion o a
symbolic unc ion call append(lis ,d). The i s o mula can be ead as ollows: i , be o e execu ing
append(lis ,d), he esul o unning leng h(lis ) is equal o 0, a call o ind(lis ,d) e u ns 0
(since no alue can be ound in an emp y lis ) and he esul s o execu ing e e se(lis ),ini (lis ),
and las (lis ) a e all NULL (i.e., he lis is emp y), hen, a e execu ing append(lis ,d), he leng h
o he augmen ed lis is 1, he e e sed lis coincides wi h he lis i sel , he alue dcan now be ound in
he lis , he ini segmen o he lis is NULL, he las elemen is he inse ed alue and he call e u ns he
poin e o he (augmen ed) lis . The second o mula ep esen s he gene al case: gi en a lis wi h an
a bi a y (posi i e) size x, he call append(lis ,d) causes he leng h o be inc eased by 1, he inse ed
alue is ound in he lis , in pa icula i is e u ned by he las obse e , and he (augmen ed) lis is
e u ned. Since he append unc ion does no es ic he inse ion o he cases in which he d alue is
s ill no inside he lis , we canno assume ind o e u n 0 be o e unning he modi ie unc ion append.
No e ha any implica ion o mula in he speci ica ion may con ain mul iple ac s (in he p e- o pos -
condi ion) ha e e o unc ion calls ha a e assumed o be un independen ly unde he same ini ial
condi ions. This a oids making any assump ions abou unc ion pu i y o side-e ec s.
4 Symbolic Execu ion in he KF amewo k
Symbolic execu ion consis s o execu ing p og ams wi h symbolic alues ins ead o conc e e alues.
I p oceeds like s anda d execu ion excep ha , when a unc ion o ou ine is called, symbolic alues
a e assigned o he ac ual pa ame e s o he call and compu ed alues become symbolic exp essions
ha eco d all ope a ions being applied. When symbolic execu ion eaches a condi ional con ol low
s a emen , e e y possible execu ion pa h om his execu ion poin mus be explo ed. In o de o keep
ack o he explo ed execu ion pa hs, symbolic execu ion also eco ds he assumed (symbolic) condi ions
on he p og am inpu s ha de e mine each execu ion pa h in he so-called pa h condi ions (one pe
possible b anch), which a e emp y a he beginning o he execu ion. A pa h condi ion consis s o he
se o cons ain s ha he a gumen s o a gi en unc ion mus sa is y in o de o a conc e e execu ion o
he unc ion o ollow he conside ed pa h. Wi hou loss o gene ali y, we assume ha he symbolically
execu ed unc ions access no global a iables; hey could be easily modeled by passing hem as addi ional
unc ion a gumen s.
Example 3 Conside again he append unc ion o Example 1. Assume ha he inpu alues o he
ac ual pa ame e s lis and da e he symbolic poin e lis and he symbolic alue ?d, espec i ely. Then,
when he symbolic execu ion eaches he i s i s a emen in he code, i explo es he wo pa hs a ising
om conside ing bo h he sa is ac ion and non-sa is ac ion o he gua d in he condi ional b anching
s a emen . The pa h condi ion o he i s b anch is upda ed wi h he cons ain lis 6=NULL, whe eas
lis =NULL is added o he pa h condi ion in he second b anch.
To summa ize, symbolic execu ion can be ep esen ed as a ee-like s uc u e whe e each b anch
co esponds o a possible execu ion pa h and has an associa ed pa h condi ion. The success ul pa hs
a e hose leading o a inal (symbolic) con igu a ion ha encloses a sa is iable pa h cons ain and ha
ypically s o es a (symbolic) compu ed esul .
Fo he symbolic execu ion o KERNELC p og ams, we mus pay a en ion o poin e de e e ence
and ini ializa ion. In C, a s uc u ed da a ype (s uc ) is an agg ega e ype ha is used o comp ise a
nonemp y se o sequen ially alloca ed membe objec s2, called ields, each o which has a name and a
ype. When a s uc alue is c ea ed, C uses he add ess o i s i s ield o e e o he whole s uc u e.
In o de o access a speci ic ield o he gi en s uc u e ype, C compu es ’s add ess by adding an
o se ( he sum o he sizes o each p eceding ield in he de ini ion) o he add ess o he whole s uc u e.
In ou symbolic se ing, he poin e a i hme ics and memo y layou machine y a e abs ac ed by 1)
using symbolic a iables as add esses, and 2) mapping each s uc u e objec in o a single elemen o
he heap cell ha g oups all objec ields (and associa ed alues). A speci ic ield is hen accessed by
combining he iden i ie s o bo h he s uc u e objec and he ield name.
Example 4 Conside he s uc u e ype Lis o Example 1. The ollowing con igu a ion eco ds a lis
a iable lwi h: 1) he in ege 7 in i s da a ield; 2) a e e ence (poin e ) named i s _node as he alue
o i s p e ield; and 3) a e e ence (poin e ) hi d_node as he alue o i s nex ield:
. . . hl7→ lien h··· l7→ (da a 7→ (in ,7),p e 7→ i s _node,nex 7→ hi d_node)···iheap . . . c g
In o de o access a ield o he lis l(e.g., i s da a ield), he co esponding index is compu ed by
jux aposing he iden i ie o he da a ield o he poin e l, hus mimicking how he conc e e access would
be done in C(i.e., l->da a).
2An objec in C is a egion o da a s o age in he execu ion en i onmen .
[8] C. Csallne , N. Tillmann & Y. Sma agdakis (2008): DySy: Dynamic Symbolic Execu ion o In a ian In e -
ence. In: P oc. 30 h In ’l Con . on So wa e Enginee ing (ICSE), ACM, pp. 281–290. 1
[9] C. Ellison & G. Ro¸su (2012): An Execu able Fo mal Seman ics o C wi h Applica ions. In: P oc. o he 39 h
Symp. on P inciples o P og amming Languages (POPL), ACM, pp. 533–544. 4
[10] M. D. E ns , J. H. Pe kins, P. J. Guo, S. McCaman , C. Pacheco, M. S. Tschan z & C. Xiao (2007): The
Daikon Sys em o Dynamic De ec ion o Likely In a ian s.Sci. Compu . P og am. 69(1-3), pp. 35–45. 1
[11] C. Ghezzi, A. Mocci & M. Monga (2009): Syn hesizing In ensional Beha io Models by G aph T ans o ma-
ion. In: P oc. 3s In ’l Con . on So wa e Enginee ing (ICSE), IEEE, pp. 430–440. 1
[12] D. Giannakopoulou & C. S. Pasa eanu (2009): In e ace Gene a ion and Composi ional Ve i ica ion in Ja a-
Pa h inde . In: P oc. 12 h In’l Con . on Fundamen al App oaches o So wa e Enginee ing (FASE),LNCS
5503, Sp inge , pp. 94–108. 1
[13] S. Hangal & M. S. Lam (2002): T acking down So wa e Bugs using Au oma ic Anomaly De ec ion. In: P oc.
22 d In ’l Con . on So wa e Enginee ing (ICSE), ACM, pp. 291–301. 1
[14] J. Henkel & A. Diwan (2003): Disco e ing Algeb aic Speci ica ions om Ja a Classes. In: P oc. o Eu opean
Con . on Objec -O ien ed P og amming (ECOOP), pp. 431–456. 1
[15] S. Khu shid, C. S. Pasa eanu & W. Visse (2003): Gene alized Symbolic Execu ion o Model Checking and
Tes ing. In: P oc. o he 9 h In ’l Con . on Tools and Algo i hms o he Cons uc ion and Analysis o Sys ems
(TACAS), pp. 553–568. 4
[16] J. C. King (1976): Symbolic execu ion and p og am es ing.Commun. ACM 19(7), pp. 385–394. 1
[17] B. Lisko & J. Gu ag (1986): Abs ac ion and speci ica ion in p og am de elopmen . MIT P ess. 3
[18] L. M. de Mou a & B. Nikolaj (2008): Z3: An E icien SMT Sol e . In: 14 h In ’l Con . on Tools and
Algo i hms o he Cons uc ion and Analysis o Sys ems (TACAS), pp. 337–340. 1,1,4.1
[19] C. S. Pasa eanu & W. Visse (2009): A Su ey o new T ends in Symbolic Execu ion o So wa e Tes ing and
Analysis.In e na ional Jou nal on So wa e Tools o Technology T ans e 11(4), pp. 339–353. 1
[20] G. Ro¸su (2015): F om Rew i ing Logic, o P og amming Language Seman ics, o P og am Ve i ica ion. In:
Logic, Rew i ing, and Concu ency - Fes sch i Symp. in Hono o José Mesegue , LNCS, Sp inge . To
appea . 1,1,2
[21] G. Ro¸su, W. Schul e & T.-F. Se banu a (2009): Run ime Ve i ica ion o C Memo y Sa e y. In: Run ime
Ve i ica ion (RV),LNCS 5779, pp. 132–152. 1
[22] G. Ro¸su & T.-F. Se banu a (2010): An O e iew o he KSeman ic F amewo k.J. Log. Algeb . P og am.
79(6), pp. 397–434. 2
[23] G. Ro¸su & A. S e anescu (2011): Ma ching Logic: A New P og am Ve i ica ion App oach. In: P oc. o he
33 d In ’l Con . on So wa e Enginee ing, ICSE 2011, ACM, pp. 868–871. 1
[24] M. Taghdi i & D.Jackson (2007): In e ing Speci ica ions o De ec E o s in Code.Au om. So w. Eng.
14(1), pp. 87–121. 1
[25] N. Tillmann, F. Chen & W. Schul e (2006): Disco e ing Likely Me hod Speci ica ions. In: P oc. 8 h In ’l
Con . on Fo mal Enginee ing Me hods (ICFEM),LNCS 4260, Sp inge , pp. 717–736. 1
[26] J. Whaley, M. C. Ma in & M. S. Lam (2002): Au oma ic ex ac ion o objec -o ien ed componen in e aces.
In: P oc. o he In ’l Symp. on So wa e Tes ing and Analysis (ISSTA), pp. 218–228. 1
